Short circuit

[guipublic]

Description

Summary of changes

This PR fixes an issue related to IF statements where instructions under conditional statement would fail if the condition were true. With the example from the added test case, you can see it can happen that array expressions are out-of-bound in a condition that is not met. In that case, when we know that the expression is failing (at compile time), which can be because of:

• index out of bound
• divide by 0
• false constraint
  We short circuit the block by replacing it with a constraint failing if the block assumption is true.

The PR is now finalised:

• I could extend the short-circuit when we merge blocks
• I delete the instructions that were short-circuited in case they are used afterward.
• The find_join method is fixed, it was working for trees and it is now adapted to the CFG.

Note that divide-by-0 is not triggering a short circuit because it is handled by the constant folding. We should allow it when it is under an assumption and it will be handled as a short-circuit, but this can be done in another PR.

Test additions / changes

Regression test case is added to 9_conditional

[guipublic]

I create a draft for now because I want to investigate if block can be further 'short-circuit' during merge block

[kevaundray]

For future tasks, as noted in your description, please create issues when this gets merged

[jfecher]

I'd normally like the issue introduced by this PR (Location::dummy) to be fixed before merging it, but it seems this PR has a bugfix that is useful for users to have merged in. I've went ahead and created two issues relating to this PR (#471 and #472) that we can work on later.