dynamic gradual guarantee broken at a conditional

[JonathanAldrich]

The attached file avl-bug2.c0.txt is a version of a correctly running c0 program with //@requires ?; added to functions that should need it, and then some bits commented out (harmlessly, I think). Running with -x yields the error:

sbt:gvc0> run -x avl.c0
[info] running (fork) gvc.Main -x avl.c0
[error] c0rt: avl.verified.c0: 79.3-79.27: assert failed
[error] Nonzero exit code returned from runner: 134
[error] (Compile / run) Nonzero exit code returned from runner: 134
[error] Total time: 3 s, completed May 20, 2022, 10:16:27 PM

It appears that an assertion that node != NULL is being generated just before the statement if (node == NULL) in the insert function. Since insert is called with NULL, this fails.

[jennalwise]

Since return statements in C0 are translated into assignments to result in .vpr, the backend verifier will analyze the program statements after the assignment if they exist. This creates the aforementioned assert run-time check in the .vpr file created from avl-bug2.c0. Below is a snippet from the viper file:

method insert(node: Ref, key: Int) returns ($result: Ref)
  requires ? && true
{
  var balance: Int
  var _: Ref
  var _1: Int
  if (node == null) {
    _ := newNode(key)
    $result := _
  }
  _1 := height(node)
  node.Node$height := _1
  balance := getBalance(node)
  $result := node
}

Then, what happens is when the branch for node == null is taken, verification proceeds in the true branch and instead of returning execution at the end (which is the expectation for the semantics of the original c0 program) verification continues to the program statements following the if statement under the node == null assumption. This is a problem due to the dereference node.Node$height following the if statement. Therefore, static verification fails down this path. Verification succeeds down the node != null path, and so the backend correctly creates an optimistic run-time check for node != null before the if to force execution down the path that does not fail statically. So, supporting arbitrary return will solve this issue.

Conrad and I had a few conversations about this and I thought this was handled properly, but looks like that is not the case.