dirtyt analysis and OTHER instructions ?

[remi-delmas-3000]

CBMC version: 5.63.0 (cbmc-5.63.0-41-g5a7a0a8801-dirty)
Operating system: macOS

dirtyt uses goto_programt::instructiont::apply to search for dirty symbols in instructions. goto_programt::instructiont::apply only visits the contents of an OTHER instruction if its statement attribute is an ID_expression :

void goto_programt::instructiont::apply(
  std::function<void(const exprt &)> f) const
{
  switch(_type)
  {
  case OTHER:
    if(get_other().get_statement() == ID_expression)
      f(to_code_expression(get_other()).expression());
    break;
 ....
}

Since OTHER operations can also have statement be equal to ID_array_set, ID_array_copy, ID_array_replace, ID_asm, etc. is it possible that dirtyt would miss anything of importance ?

[martin-cs]

Using OTHER for array copy and replace (rather than using builtin functions) feels like a mistake. It certainly wasn't implemented uniformly and the handling of OTHER is patchy at best. See #4323 for the last discussion of this. I think I agree with the conclusion that OTHER should be replaced or at least minimised, especially given the growth of use of builtin functions.

[tautschnig]

Notwithstanding what @martin-cs said: the changes in #7085 should be moved to the actual dirtyt implementation instead of code contracts rolling its own.

[martin-cs]

Agree with @tautschnig . Let's not have multiple copies of the same code again; it takes ages to de-duplicate them.

[jimgrundy]

So, who's moving this code then? Michael seems to be doing a bunch of stuff, should we assign Remi?

[remi-delmas-3000]

I can take the action. If things break as a result I might need help.

[remi-delmas-3000]

Notwithstanding what @martin-cs said: the changes in #7085 should be moved to the actual dirtyt implementation instead of code contracts rolling its own.

Could we also consider modifying goto_programt::instructiont::apply to traverse all subnodes of OTHER instructions and not just ID_expression ?

[martin-cs]

On Tue, 2022-09-06 at 13:59 -0700, Rémi Delmas wrote: I can take the action. If things break as a result I might need help.

Happy to help if needed.

[martin-cs]

Could we also consider modifying goto_programt::instructiont::apply to traverse all subnodes of OTHER instructions and not just ID_expression ?

Yes... unfortunately there is not a complete list of what this can be or what the intended semantics are. #4323 is my best attempt. To be honest, I think we should just remove OTHER or at least give it a semantics of "It is fine to ignore these" or "If you find an OTHER that you do not recognise, it could do *anything*, including havoc and non- termination".

[remi-delmas-3000]

Fixed by #7106