I'm not sure what claim is actually being made here, but decompilation of any particular compiler is trivially decidable: try every input program until you find the one that produces the observed output.
How do you know that you'll find a program that works? What if the program wasn't generated by the compiler and that compiler can't generate that particular sequence of instructions? At what point do you know, in general, "this instruction sequence isn't derivable from this compiler!"...?
You're right. I initially took the problem to be "given this (specific) compiler output, determine the corresponding compiler input." That seems like a reasonable interpretation of "decompiling". If the problem is instead "determine whether this chunk of machine code could have come from this compiler", then my proposed algorithm obviously doesn't work.
Iterating over all possible input 'programs' (including buggy ones) is easy, even if the language allows for multiple input files of different types.
=> if you can give an upper bound for the length of the source code of a binary of size N, you are all set. I do not see how to proof that such an upper bound exists, but it seems fairly reasonable that one must exist. I cannot really think of any real-world compiler that would need, say, more than a GB of source code for every bit of output (it is easy to design such a language, but it would be quite esoteric)
Well, I think "obviously" was right, since my algorithm would never terminate if no source is ever found that matches the generated binary (there are infinitely many possible programs for most idealized languages).
For your idea of modifying my algorithm to bail after some number of inputs have been checked, clearly there does exist a bound on the source length necessary to generate all possible binaries of size N, since there are only finitely many such binaries (and thus they can be produced by finitely many sources). But to turn this into an algorithm, you'd need a computable bound. For a language like C, I think such a bound probably exists and is a reasonable function of the input size. For a language like Coq, though, I doubt the bound would be computable. Basically, I think that there are programs that work for reasons that are very difficult to prove.
Also, I think we're far enough from practical that appeals to the real world are somewhat silly. Either we're interested in understanding the theoretical situation, in which case lack of real world examples doesn't help, or we're interested in practical decompilation, in which case this whole conversation is stupid.
How do you know that you'll find a program that works? What if the program wasn't generated by the compiler and that compiler can't generate that particular sequence of instructions? At what point do you know, in general, "this instruction sequence isn't derivable from this compiler!"...?