search

gradual-verification / gvc0

Gradually Verified C0
6 stars 5 forks source link

Method not marked as containing imprecision when it has an imprecise pre or postcondition #41

Closed jennalwise closed 2 years ago

jennalwise commented 2 years ago

https://drive.google.com/file/d/1zo85HiRcqZbFFRQGldL255NzOKrztM16/view?usp=sharing is failing with the error: 

[error] Error: Field access runtime check failed for struct Node.left
[error] Nonzero exit code returned from runner: 1
[error] (Compile / run) Nonzero exit code returned from runner: 1

It turns out that tree_add does not contain the correct code for passing permissions back and forth from tree_add_helper. The incorrect code looks like this:

struct Node* tree_add(struct Node* root, int x, struct OwnedFields* _ownedFields)
{
  struct Node* res = NULL;
  struct OwnedFields* _tempFields = NULL;
  struct OwnedFields* _tempFields1 = NULL;
  res = NULL;
  _tempFields = initOwnedFields(_ownedFields->instanceCounter);
  assert(-2147483647 <= x);
  bst(root, -2147483647, 2147483647, _ownedFields);
  sep_bst(root, -2147483647, 2147483647, _tempFields);
  _tempFields1 = initOwnedFields(_ownedFields->instanceCounter);
  res = tree_add_helper(root, x, -2147483647, 2147483647, _tempFields1);
  return res;
}

We see that a tempfield variable is created to gather permissions from tree_add_helper (which is should since tree_add_helper requires permission tracking). However, tree_add_helper's contract is precise, so permissions computed from the precondition must be passed to tree_add_helper and the postcondition must be analyzed to return permissions back from tree_add_helper. None of this code is injected above. That is because as coded here, https://github.com/gradual-verification/gvc0/blob/26398e36e0ad37c4eb9b64ecaac94cf3d842cd5f/src/main/scala/gvc/weaver/Checker.scala#L294, permissions from the precondition (postcondition) of tree_add_helper are only computed and sent to (returned from) tree_add_helper when tree_add needsToTrackPrecisePerms. Currently, this flag is only set to true if tree_add contains imprecision in its body. However, it should also be set to true if it contains imprecision in its contract. That is, the definition of needsToTrackPrecisePerms must be updated to include these additional cases to fix the above bug.

jennalwise commented 2 years ago

Fixed in this commit: https://github.com/gradual-verification/gvc0/commit/26398e36e0ad37c4eb9b64ecaac94cf3d842cd5f