Define different function for concrete playback (no user impact)

[celinval]

Description of changes:

Split the definitions of functions that have specific logic for concrete playback to avoid generating code for unused logic.

Background: While upgrading the toolchain to nightly-2023-04-16, I noticed a few new warnings regarding caller location and the size of the model was much bigger in some case. The MIR file was going from a couple hundreds of lines to 20k+ lines.

It looks like the if cfg!() is no longer being propagated and the concrete playback code is increasing the logic that the compiler detects as reachable.

Resolved issues:

Related to #2383 and PR #2406

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

We might want to split the code like we've done with the macro one to make it a bit easier to maintain but for now, I'm jut unblocking the toolchain update.

Testing:

• How is this change tested? Current tests

• Is this a refactor change? Yes

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tautschnig]

Notes on the alleged performance regression: The resulting GOTO binaries are (as one should expect from the changes in this PR) the same, with one exception: the numbers in Kani-generated s2n_quic_core:::alloc[[:digit:]]+::init differ, which in turn means that their invocation order from __CPROVER_initialize will differ. This, in turn, results in SAT formulae that are equisatisfiable but not exactly the same (they will have the same number of variables and clauses, but there is a renaming between the variables). Such differences mean that the SAT solver will happen to make different decisions. Take a look at the following data (using CaDiCaL to further reduce possible noise from the system):

model-checking:main	celinval:issue-2383-playback
Runtime Symex: 6.64313s	Runtime Symex: 6.41786s
size of program expression: 177676 steps	size of program expression: 177676 steps
slicing removed 101675 assignments	slicing removed 101675 assignments
Generated 10049 VCC(s), 7355 remaining after simplification	Generated 10049 VCC(s), 7355 remaining after simplification
Runtime Postprocess Equation: 0.24202s	Runtime Postprocess Equation: 0.224713s
Passing problem to propositional reduction	Passing problem to propositional reduction
converting SSA	converting SSA
Runtime Convert SSA: 2.57943s	Runtime Convert SSA: 2.55088s
Running propositional reduction	Running propositional reduction
Post-processing	Post-processing
Runtime Post-process: 7.78618s	Runtime Post-process: 7.82671s
Solving with CaDiCaL sc2021	Solving with CaDiCaL sc2021
1846920 variables, 24318135 clauses	1846920 variables, 24318135 clauses
SAT checker: instance is SATISFIABLE	SAT checker: instance is SATISFIABLE
Runtime Solver: 8.27705s	Runtime Solver: 8.33516s
Runtime decision procedure: 10.8814s	Runtime decision procedure: 10.9116s
Running propositional reduction	Running propositional reduction
Solving with CaDiCaL sc2021	Solving with CaDiCaL sc2021
1846920 variables, 24318136 clauses	1846920 variables, 24318136 clauses
SAT checker: instance is SATISFIABLE	SAT checker: instance is SATISFIABLE
Runtime Solver: 3.83114s	Runtime Solver: 3.94184s
Runtime decision procedure: 3.85865s	Runtime decision procedure: 3.97045s
Running propositional reduction	Running propositional reduction
Solving with CaDiCaL sc2021	Solving with CaDiCaL sc2021
1846920 variables, 24318137 clauses	1846920 variables, 24318137 clauses
SAT checker: instance is SATISFIABLE	SAT checker: instance is SATISFIABLE
Runtime Solver: 53.2559s	Runtime Solver: 8.55057s
Runtime decision procedure: 53.3403s	Runtime decision procedure: 8.6407s
Running propositional reduction	Running propositional reduction
Solving with CaDiCaL sc2021	Solving with CaDiCaL sc2021
1846920 variables, 24318138 clauses	1846920 variables, 24318138 clauses
SAT checker: instance is SATISFIABLE	SAT checker: instance is SATISFIABLE
Runtime Solver: 3.421s	Runtime Solver: 62.0962s
Runtime decision procedure: 3.43368s	Runtime decision procedure: 62.1679s
Running propositional reduction	Running propositional reduction
Solving with CaDiCaL sc2021	Solving with CaDiCaL sc2021
1846920 variables, 24318139 clauses	1846920 variables, 24318139 clauses
SAT checker: instance is UNSATISFIABLE	SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.281313s	Runtime Solver: 0.17613s
Runtime decision procedure: 0.29297s	Runtime decision procedure: 0.179646s

I have highlighted the (only significant) differences. So unless we find a way to make Kani's choice of names deterministic there might not be much we can do to also have deterministic SAT solver performance.

[celinval]

Thanks @tautschnig for your thorough analysis. That's exactly what I was afraid of. Not sure what's the best course of action. Any suggestions?

[tautschnig]

Thanks @tautschnig for your thorough analysis. That's exactly what I was afraid of. Not sure what's the best course of action. Any suggestions?

As per the discussion that happened out of band in the meantime: let's keep collecting data for the time being, no obvious reason that this specific PR ought to be blocked.