|
|
|
|
|
|
by 0x0
3749 days ago
|
|
|
> However, since it's a question about the implementation (does that instruction appear) rather than the function being computed (which may or may not fire missiles) On common architectures where code is data is code, this sounds hard to detect as the program could build a buffer of commands that end up firing the missile, without any obvious "fire the missile" sequence present in the binary? For example, the program could inflict a stack overflow on itself. |
|
|
Absolutely, the work-arounds are just that; they don't answer the original question.
In the case of "Is program P capable of firing missiles?", this will be 'yes' for many programs which don't fire missiles, so it's an over-approximation of missile-firing.
In the case of "Does program P contain the <fire missiles> instruction?", this could, as you say, under-approximate missile firing.
If the language allows running data as code, then we can handle this in a conservative way, i.e. 'Could program P execute a <fire missiles> instruction?', which would be true if P contains '<fire missiles>', true if P contains 'eval' (since the evaluated code could fire the missiles), etc. and false otherwise. We can make our questions (AKA our type systems) arbitrarily clever, but they will only ever approximate the answers to questions forbidden by Rice's theorem. Usually it's best to make conservative approximations, i.e. turning "does XYZ happen?" into "could XYZ happen?", assuming that it could, and only answering 'no' if we can prove otherwise.
As far as cases like 'the program could inflict a stack overflow on itself', these would all be handled in our model of the language (equivalent to the list of conditions I wrote above which affected whether we answer true or false). Again, this should be conservative, so it's likely that for edge-cases like 'inflicting a stack overflow on itself', there might not be much we can say about the program's behaviour; in which case we'd get a lot of 'yes' answers to our 'could XYZ happen?' questions, simply because we can't rule those things out.