Goto crossing scopes: fix scope tree entry of conditions

[tautschnig]

We must convert the condition of an if/then/else first to make sure any declarations produced by converting the condition have a suitable scope-tree node. Previously, gotos in either branch of the if-then-else were led to believe that declarations resulting from condition were not yet in scope. The feature from #8091 would, thus, result in a spurious loop back to the declaration to put it in scope before following the goto edge.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 78.33%. Comparing base (4eadc8a) to head (727982e).
Report is 1 commits behind head on develop.

❗ Current head 727982e differs from pull request most recent head 1f5950c

Please upload reports for the commit 1f5950c to get more accurate results.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8187      +/-   ##
===========================================
- Coverage    78.34%   78.33%   -0.02%     
===========================================
  Files         1722     1722              
  Lines       188394   188393       -1     
  Branches     18493    18430      -63     
===========================================
- Hits        147600   147569      -31     
- Misses       40794    40824      +30     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[kroening]

I find it odd that the order of conversion matters?

[tautschnig]

I find it odd that the order of conversion matters?

I'm with you in that I don't like that the order matters, but I can't claim to have a better solution to offer: the order (nowadays) matters, because we keep track of variable declarations in the scope stack (which now is a scope tree). That is, conversion has that side effect of updating the scope tree.

In absence of ideas on how to avoid this side effect I'd maintain that this PR here is the correct fix.

[kroening]

In absence of ideas on how to avoid this side effect I'd maintain that this PR here is the correct fix.

I'd really like to get rid of that side effect. If need be, I'd prefer to pass around that scope stack.

[tautschnig]

In absence of ideas on how to avoid this side effect I'd maintain that this PR here is the correct fix.

I'd really like to get rid of that side effect. If need be, I'd prefer to pass around that scope stack.

With apologies for taking this long to get back to this: I am still trying to figure out whether this can be done without making all of targetst target that object being passed around. Perhaps that's the right thing to do, but it will amount to touching approximately 160 places in goto_convert's code.

[kroening]

With apologies for taking this long to get back to this: I am still trying to figure out whether this can be done without making all of targetst target that object being passed around. Perhaps that's the right thing to do, but it will amount to touching approximately 160 places in goto_convert's code.

Do we want to do this in the C front-end instead? That's where scoping belongs.

[tautschnig]

With apologies for taking this long to get back to this: I am still trying to figure out whether this can be done without making all of targetst target that object being passed around. Perhaps that's the right thing to do, but it will amount to touching approximately 160 places in goto_convert's code.

Do we want to do this in the C front-end instead? That's where scoping belongs.

I equally thought that was the right choice. The challenge, however, is with goto instructions, where we’d need a frontend (codet) level control-flow graph. But maybe we should bite that bullet, it would also help with always_inline?

[kroening]

Approving with the understanding that this will be fixed post release of version 6.