BST - Failing series of partial specs when removing imprecision

[icmccorm]

Description

BST has a total of 157 partial specifications in a single path, where #157 is fully specified. Everything is verifying, but each partial specification from #145 - 149, 155-156 is failing at runtime (stress level 2) with the following error

Error: Field access runtime check failed for struct Node.left

The following source files can be used to recreate this issue. Specifically, compiling imprecise_checked.c0 after modifying the value for stressCaptured on line 329 from 0 to some nonzero value will recreate the failures described below:

• imprecise.c0 - partial spec #145, which fails at runtime.
• imprecise_checked.c0 - #145 after verification, with checks inserted.
• previous.c0 partial spec #144, which succeeds at runtime
• previous_checked.c0 #144 after verification, with checks inserted.
• bsterr.csv - list of all failing partial specs with the level ID and component type added.

Source

The source of the error varies as the workload parameter is changed because a different, random set of nodes are added for each workload value. We have yet to document the location of each failure for every partial spec, but for #145, the original failure at workload level 2 occurs within bst:

void bst(struct Node* root, int min, int max, struct OwnedFields* _ownedFields)
{
  if (root == NULL)
  {
    assert(true);
  }
  else
  {
    assertAcc(_ownedFields, root != NULL ? root->_id : -1, 1, "Field access runtime check failed for struct Node.left");

Changing the parameter from 2 to 20 results in the following runtime check failing at line 519 in tree_add_helper:

assertAcc(_ownedFields, root != NULL ? root->_id : -1, 2, "Field access runtime check failed for struct Node.right4");

Changing the parameter to 23 results in a different runtime check failing within tree_add_helper at line 494:

assertAcc(_ownedFields, root != NULL ? root->_id : -1, 1, "Field access runtime check failed for struct Node.left6");

Contents

Partial spec #145 is created by completing the predicate tree

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

This causes imprecision to be removed from the completed specs of the following methods:

• create_tree
• add
• contains
• tree_remove
• tree_max
• tree_min

The following predicates are still imprecise:

• bstRemove
• treeRemove

The following methods are still imprecise:

• main
• 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
• tree_remove_lemma
• create_tree_helper
• tree_add_helper
• tree_main_lemma
• tree_main_lemma_bst
• tree_max_helper
• tree_max_lemma