Benchmarker producing wrong .verified files after generating correct source code permutations due to oddly constructed IRs

[jennalwise]

Related to what is going on in issue https://github.com/gradual-verification/gvc0/issues/58, the Benchmarker is reading in the benchmark source files and calling SelectVisitor on them to generate an IR and source program for a specified permutation of the fully specified benchmark.

The IR produced does not have all of the objects updated correctly based on changes for the permutation (issue 58 had previous struct objects attached to fields while new struct objects with the same values were added to the program.structs array; BaselineChecker modified program.structs with the expectation that the fields' structs would also be modified), and unfortunately BaselineChecker uses them expecting them to be consistent. This seems to affect more than issue 58 as I also found permutation 6455's .verified file from the Benchmarker to be incorrect:

void sortedSegHelper(struct Node* start, struct Node* end, int prev, int endVal, struct OwnedFields* _ownedFields)
{
  if (start == end)
  {
    if (end == NULL)
    {
      assert(true);
    }
    else
    {
      assert(endVal >= prev);
    }
  }
  else
  {
    assertAcc(_ownedFields, start != NULL ? start->_id : -1, 0, "Field access runtime check failed for struct Node.val");
    assertAcc(_ownedFields, start != NULL ? start->_id : -1, 1, "Field access runtime check failed for struct Node.next");
    assert(start->val >= prev);
    sortedSegHelper(start->next, end, start->val, endVal, _ownedFields);
  }
}

It implements checks for sortedSegHelper based on the complete specification of its predicate body from the original benchmark program. But, the permutation of 6455 requires an implementation of (this correct implementation comes from the .verified file produced by --dynamic mode, which doesn't call SelectVisitor on the IR---it reads the IR directly from the source file):

void sortedSegHelper(struct Node* start, struct Node* end, int prev, int endVal, struct OwnedFields* _ownedFields)
{
  if (start == end)
  {
    if (end == NULL)
    {
      assert(true);
    }
    else
    {
      assert(true);
    }
  }
  else
  {
    assert(true);
  }
}

The source file produced by SelectVisitor's IR is the correct permutation, but the IR itself is flawed in a way that BaselineChecker does not expect---it accidently uses the old not updated predicate body object, whereas the source file printing uses the new, correct object from a different entry point in the IR. I suspect this issue affects more than just struct sizes and predicate bodies.

[jennalwise]

Since debugging and fixing this with a better solution will take more time than I have. My plan is to implement a bit of a hacky solution for this bug for now (which should be fixed more properly later).

I am going to take the IR produced by SelectVisitor and output it to a temporary file (which is correctly generated by SelectVisitor). Then, read it back in and produce a fresh and thus consistent IR from it for verification---pretty much replicating the recreating benchmark files and sending them to --dynamic workflow in the benchmarker. After producing the fresh IR, I'll code the temp file to be deleted.

[jennalwise]

We should also add test cases that catch these issues after properly fixing this issue as well. Currently, we test SelectVisitor and BaselineChecker both in isolation, but not together: we test that SelectVisitor is giving back the correct permutations and BaselineChecker produces the right output, but we never test that chaining them together produces the correct outputs.

[jennalwise]

Hacky solution implemented here: https://github.com/gradual-verification/gvc0/commit/8a9cc4198f9ed268b808493b49af2915c74ec861 Print stmts for testing removed after here: https://github.com/gradual-verification/gvc0/commit/02f885fc094ca61f8ac1ccc7c93a7b0ae731d113