Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
jennalwise opened this issue Nov 15, 2023 · 3 comments
Labels
enhancement New feature or request

Comments

@jennalwise
Copy link
Member

jennalwise commented Nov 15, 2023

Related to what is going on in issue #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 jennalwise added the bug Something isn't working label Nov 15, 2023
@jennalwise
Copy link
Member Author

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
Copy link
Member Author

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
Copy link
Member Author

jennalwise commented Nov 16, 2023

Hacky solution implemented here: 8a9cc41
Print stmts for testing removed after here: 02f885f

@jennalwise jennalwise added enhancement New feature or request and removed bug Something isn't working labels Nov 16, 2023
@jennalwise jennalwise reopened this Nov 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant