CSE: disable summaries when prank or expectRevert is active

[palinatolmach]

Follow up to #1008.

Starting with #1008, CSE summaries of functions that contain external calls are branching spuriously on foundry.set.expectrevert.1 and foundry.prank rules applying before the summary of the nested external call. The CSE execution also takes considerably longer (e.g., 5 minutes vs 30 seconds for functions like identity() and add(...).

This PR prevents this branching by disabling summaries when prank and expectRevert is active by setting <active> and <isRevertExpected> to false in the CSE initial configuration, instead of leaving them to be symbolic. This means that the summaries won't apply if the test has either of this cheatcodes enabled; further investigation is needed if we find out that the summaries need to be more general to cover these cases too.

Potential ways to achieve this could include additional constraints on CALLDEPTH_CELL, EXPECTEDDEPTH_CELL, DEPTH_CELL — the challenge is to make these constraints exhaustive enough to prevent spurious branches (attempted here), or refactoring the expectRevert and prank inclusion and processing logic by introducing cut-point rules that would handle that.

[ehildenb]

Would it work with condition added to LHS of the calldepth:

andBool notBool (ACTIVE_CELL orBool PRAKNDEPTH_CELL <Int CALLDEPTH_CELL)
andBool notBool (EXPECTED_REVERT_CELL orBool REVERTDEPTH_CELL <Int CALLDEPTH_CELL)

[ehildenb]

Let's also add a test of prank of a function f that calls g, so that we can examine the behavior of the interaction of pranking and CSE.

[palinatolmach]

I opened a separate PR (to make it easier to compare the output diffs and roll back to this implementation if needed) which adds these preconditions to the initial state during CSE:

andBool notBool (ACTIVE_CELL orBool PRANKDEPTH_CELL >=Int CALLDEPTH_CELL)
andBool notBool (EXPECTED_REVERT_CELL orBool REVERTDEPTH_CELL >=Int CALLDEPTH_CELL)

This may be incorrect, but, in the PR, I flipped the sign in notBool (... PRAKNDEPTH_CELL <Int CALLDEPTH_CELL) from @ehildenb's message, since the original condition led to spurious branching when applying g's summary in f—this was caused by repeatedly checking whether PRAKNDEPTH_CELL <Int CALLDEPTH_CELL + 1 at g's invocation. That made me think the logic should be reversed, i.e., a summary (especially a nested one) should actually apply iff PRAKNDEPTH_CELL <Int CALLDEPTH_CELL (not the negation of it). This also resolves the case of nested summary applications: if CALLDEPTH_CELL > PRANKDEPTH_CELL, then any deeper call (e.g. CALLDEPTH_CELL + 1) still satisfies the condition and allows the summary to apply.

This does fix some of the summaries that were affected by the change in the Haskell Backend, but I still need to inspect the remaining expected output updates and the output for two new tests using prank and expectRevert cheatcodes introduced in that PR.