What is a safe overapproximation of an OTHER instruction

[martin-cs]

To the best of my knowledge, what an OTHER instruction does is not well documented. goto-programs/goto_program.h:132 says:

"Execute the code (an instance of codet of kind ID_fence, ID_printf, ID_array_copy, ID_array_set, ID_input, ID_output, ...)."

goto-symex/symex_other.cpp:77 seems to have one of the most comprehensive lists of possibilities including ID_output (so it can manipulate the external environment), ID_decl (marked as UNREACHABLE -- no idea what this once was supposed to do), ID_nondet ("like skip"), ID_asm ("we ignore this for now"), ID_array_{copy,replace,set,equal}, ID_user_specified_{predicate,parameter_predicates,return_predicates} (???). Elsewhere there are references to ID_skip (???), ID_printf (not clear why this is different to ID_output), ID_havoc_object, {set,clear}_{may,must}, ID_expression and various fences.

Possibly relevant to #3191 maybe we should have an actual explicit list of what it could be?

To get the abstract domains to handle OTHER correctly it would be good to be clear exactly what we can assume about them.

*. It seems likely that they "read" from any variable they include ( analyses/goto_rw.cpp:784 seems to think so ).
*. In some cases they can "write" to some of the variables they include. This does not seem well supported in the various abstract domains.
*. Some instructions can modify the external state of the program so they have to be considered for anything concurrent.
*. I have yet to see that they change the flow of control, although frankly, ID_asm makes me nervous.
*. I am unsure as to whether they can affect termination or run-time. Are the CPROVER model of fences guaranteed to return? Is ID_output blocking?

Thoughts, opinions, pointers to specific behaviours in the code, historical reminiscences, suggestions, etc. all most welcome.

[tautschnig]

Thanks a lot for bringing this up. I am wondering whether at some point we should just remove this? Of course OTHER adds a lot of flexibility, but it might be at the expense of soundness. For a program analysis framework the latter may be rather important. I am leaning towards making all of these function calls? Something like __CPROVER_asm, etc? The downside of that approach would be that it's less explicit that something really weird is going on in that statement, but in many cases dealing with an undefined function should be similar to dealing with an undefined statement.

[martin-cs]

At the moment I am deeply skeptical that all of the uses of OTHER are correctly handled by all analysis tools. TBH I'm not confident that we even know all of the uses for it. All of the uses I know of can be replaced with magic functions. Given that we already have some magic functions ( __CPROVER_malloc, etc.) and there seems little motivation for changing these into instructions, perhaps the questions should be:

1. What does having an OTHER instruction gain us beyond having magic functions?

2. Is it possible to give some semantic limits on what OTHER can do so that we don't need to enumerate all cases in all analyses? Are these in any way different from the guarantees given by an unknown function call?

3. Does anyone have the time / motivation to write a de-OTHER-ing patch?

[peterschrammel]

I'd get rid of OTHER altogether and replace the remaining (meaningful and well-defined) uses by magic functions.

[martin-cs]

@smowton ?
@chrisr-diffblue ?

[martin-cs]

#2548 suggests that we rely on having over approximations for OTHER but I have no idea if they are sound or not.

[tautschnig]

... and 7b51b0c from #2548 makes clear that we didn't quite expect those in a number of places.