Partial specs #145-151 of BST failing at runtime with missing permission.

[icmccorm]

Description

Binary search tree produces 158 partial specs from a single path, and 7 are failing when imprecision is removed.

Removing Imprecision

When removing imprecision, we differentiate between "incomplete", "complete", "imprecise", and "precise" methods and predicates. A method or predicate is Incomplete if components from its complete, static specification are missing. Complete indicates that all components are present. Complete and incomplete specs are both still imprecise, meaning that a ? is present in every specification. A precise specification is complete, and has no ?. We only remove ? from a complete method or predicate if every predicate that it immediately depends on is complete.

Error Location

This description is limited to #145, with the assumption that finding what causes this error may lead to correcting the adjacent errors. Partial specification #145 is created from #144 when the predicate tree is made complete and precise by adding an instance of the predicate bst.

< //@predicate tree(struct Node* root) = ?;
---
> //@predicate tree(struct Node* root) = bst(root, -2147483647, 2147483647);

The error is caused by a failing runtime check for Node.right on line 610 of method tree_main_lemma_bst in the checked output from the verifier.

   ...
   _cond_2 = root == NULL;
    tree_main_lemma_bst(root->left, x, min, root->val - 1, _ownedFields);
    _tempFields = initOwnedFields(_ownedFields->instanceCounter);
    if (!_cond_1 && !_cond_2)
    {
      assertAcc(_ownedFields, root != NULL ? root->_id : -1, 2, "Field access runtime check failed for struct Node.right");

This leads to the following methods that were complete and imprecise in #144 being made precise in #145:

• create_tree
• tree_add
• tree_contains
• tree_max
• tree_min
• tree_remove

The following predicates are still imprecise in #145:

• treeRemove
• bstRemove

The following methods are still imprecise in #145

• create_tree_helper
• tree_add_helper
• tree_main_lemma
• tree_main_lemma_bst
• tree_max_helper
• tree_max_lemma
• tree_remove_helper
• tree_remove_lemma
• tree_remove_lemma_left
• tree_remove_lemma_left2
• tree_remove_lemma_max
• tree_remove_lemma_min
• tree_remove_lemma_right

Resources

The following .zip file contains the partial specs #144-151, both before and after verification, and the list of which components were added to create each one. Note that #144 succeeds, but #145-151 will all fail at workload 2.

replication.zip