Partitioning predicates for smarter runtime check assertions

[janpaulpl]

For a more comprehensive overview of the problem, see this overleaf project explaining the process.

The avlja benchmark defines a predicate avlh of the form:

predicate avlh(struct Node *root, int height1) =
  root == NULL ?
    height1 == 0
	:
	  acc(root->left) && acc(root->right) && acc(root->key) &&
	  acc(root->leftHeight) && acc(root->rightHeight) &&
	  avlh(root->left, root->leftHeight) &&
	  avlh(root->right, root->rightHeight) &&
	  root->leftHeight - root->rightHeight < 2 &&
	  root->rightHeight - root->leftHeight < 2 &&
	  root->leftHeight >= 0 && root->rightHeight >= 0 &&
	  (root->leftHeight > root->rightHeight ?
	    height1 == root->leftHeight+1 :
		height1 == root->rightHeight+1)
	;

I suspect a common pattern for writing gradual specifications would be to have dynamic checks mostly everywhere but a static post-condition:

struct Node* insert(struct Node* node, int h, int key, struct Height *hp)
  //@ requires ?;
  //@ ensures ? && acc(hp->height) && avlh(\result, hp->height);
{

Currently, the verifier re-asserts equivalent checks for this avlh predicate which all get run, causing runtime overhead:

 if (!_cond_1 && !_cond_3 && !_cond_2 && !_cond_4 && _cond_7 && _cond_8 && !_cond_9 && !(node == NULL) || !_cond_1 && _cond_3 && !_cond_2 && !_cond_4 && _cond_7 && _cond_8 && !_cond_9 && !(node == NULL))
          {
            assert(_1 - node->leftHeight < 2);
            assert(node->leftHeight >= 0);
            avlh(node->right, _1, _ownedFields);
            avlh(_, node->leftHeight, _ownedFields);
          }

Both of these avlh checks are equivalent for a certain path in which the predicates line up as:

P(node->right, max(node->leftHeight, node->rightHeight)
P(OR(node->right, node->left), node->leftHeight)
---
P( node-> right, node->leftHeight)

Implementation pipeline

The implementation is broadly made up of 3 stages

• Slice construction: During the parsing phase of gvc0, predicates are partitioned into a list of sliced predicates.

  • Terms to calls: These sliced predicates have to be a valid runtime check instance. They're carried from gvc0 and saved under a node structure in Silicon. If there are recursive slices, these are unrolled only once.
  • Targeted files:
    • gvc0/.../parser/Slicer.scala
    • silicon/.../state/RuntimeChecks.sala

• Equivalence identification: Once we've formatted the sliced predicates as recognizable terms by Silicon, we want to identify when equivalent predicate calls happen to minimize their occurrence.

  • Path information: We have to keep track of the path condition to know which one we can discard and optimize. At first, we just assume every predicate call overlaps and needs optimization (this is a bucket of predicate calls). The construction for these checks is guarded by an if statement. The logical constructions are stored as terms (more specifically variables) which are to be called if necessary in the next step. This is relatively straightforward, if we see that condition two implies condition one, then we can take out the first condition entirely (in our case, we create a map for each of our sliced predicates, which are by default set to True and changed to False if the second condition does not imply the first one.
  • Computation for optimization: If the second check is enabled, and the first one has not happened, we do the check, otherwise we skip.
  • SMT Solver: We need an SMT solver to know if the code is actually needed, i.e., to change the default True values to False and resolve the if statement. Viper uses a wrapper for the Z3 SMT solver, which takes the terms as Lisp format. We parse our terms as a Lisp AST and feed it into these front ends.
  • Targeted files:
    • silicon/.../state/State.scala: Keeping track of the path condition metadata.
    • silicon/.../decider/PathConditions.scala: Actual path condition logic (identified with metadata from State.
    • silicon/.../state/RuntimeChecks.scala: Important data regarding each runtime check, here we get the predicates and dump them in the bucket.
    • silicon/.../state/Slicer.scala: Here we have the bucket of predicates and the tuple map. The information from State and RuntimeChecks come together.
    • silicon/.../state/SMTSlicer.scala: Parsing our terms as s-expressions.
    • silicon/.../decider/TermToSMTLib2Converter.scala: Wrapper functions that have to be extended to our terms.

• Replacement of runtime assertions: Finally, with a sound map for which runtime assertions to replace and which to replace them with, we can inject these assertions and replace the predicate calls.

  • Targeted files:
    • silicon/.../State.scala: Names of predicates that are being injected and their location.
    • silicon/.../Terms.scala: if terms to inject into the code to guard the constructions.
    • silicon/.../RuntimeChecks.scala: Position information for where to inject the terms.
    • silicon/.../Slicer.scala: Body for the if statements comes from the Map, those values set to True are valid assert expressions to feed into the if terms and inject at the position given from State.scala.

Note: This optimization will only work for logic predicates and not the acc logic. So really, we're just asserting predicates P6-P12. This optimization has to be addressed in a separate issue.

[janpaulpl]

Sub-issue: Unbounded recursion

Previously, I described that for recursive slices we will only unroll once, this is why:

It now seems like the introduction of unbounded recursive predicates plagues our static assertions. For example, in alvh we have two arguments to avlh(root -> left, root->leftHeight) and avlh(root->right, root->rightHeight) respectively. The optimization would have to unroll these predicates as well.

A possible approach could be following an equivalent loop transformation algorithm relative to our specifications. This would allow to assert a k in which the unfolding should stop, because all subsequent unfoldings would abide the specification equivalently.