[cse] Precondition Refinement

Background

Presently, the CSE initiates symbolic execution from the call graph's leaf nodes progressing towards the root (enabled by the --cse option). The contract execution commences either from the symbolic values of its parameters or from the state post-execution of the constructor (using --run-constructor). This approach results in overly abstract initial states for the functions, making it exceedingly time-consuming to determine the final states of the functions. Consequently, this prevents us from synthesizing reusable function summaries.

Running Example

Using DualGovernance.activateNextState() as an example, the ActivateNextStateTest.testActivateNextStateTermination serves as a test harness for this function. The current situation is as follows:

1. kontrol prove ActivateNextStateTest.testActivateNextStateTermination: The proof is successful. The process starts from the root of the call graph, executing the constructor and setUp before running testActivateNextStateTermination, and finally invoking activateNextState.
2. Adding cse with kontrol prove ActivateNextStateTest.testActivateNextStateTermination --cse: The proof fails. This failure occurs because DualGovernance.activateNextState() is symbolically executed without calling the constructor and setUp, resulting in a PROOF-FAILED outcome for DualGovernance.activateNextState(). Consequently, ActivateNextStateTest.testActivateNextStateTermination inherits this failure when it uses the summary, leading to its own failure. This indicates that we should not execute activateNextState from the most abstract state to obtain its summary, i.e., kontrol prove DualGovernance.activateNextState.
3. Adding --run-constructor with kontrol prove DualGovernance.activateNextState: Verification out-of-time or out-of-memory. While the function inputs are correctly configured by the constructor, the state includes improbable and unreasonable conditions that can arise during function calls. The excessive branching states prevent termination. Even if termination is achieved, the final state obtained through minimize_proof and node merging remains too abstract, causing the verification to fail.

Solution

To address the above problem, precondition refinement is necessary: more reasonable constraints should be provided for the initial state of the function. The following approaches can be considered. Given the simplicity of the activateNextState example, the first approach should suffice to resolve the issue:

1. Modify the current --cse option to run the constructor and setUp before executing functions from the leaf to the root of the call graph.
2. Introduce a new method to specify preconditions for each contract function, where the initial state is derived from these preconditions.

Additionally, function summaries should do the following before being included as lemmas:

1. Ensure the summary can be used by removing any context unrelated to the callee contract and function, such as the test contract loaded during setUp.
2. Improve rewrite efficiency by minimizing summaries using minimize_proof and node merging.

Result / Expected

Upon the successful implementation of minimize_proof with node merging (issue #703), all tests within ActivateNextStateTest are expected to be verified within seconds or minutes.