llvm_conditional_points_to in postcondition does not respect condition

[RyanGlScott]

Given this C code:

// test.c
#include <stdint.h>

void test(uint8_t *x) {}

I would expect this SAW spec to succeed:

// test.saw
let test_spec = do {
  p <- llvm_alloc (llvm_int 8);
  x <- llvm_fresh_var "x" (llvm_int 8);
  llvm_points_to p (llvm_term x);

  llvm_execute_func [p];

  llvm_conditional_points_to {{ x == 1 }} p (llvm_term {{ 1 : [8] }});
};

m <- llvm_load_module "test.bc";
llvm_verify m "test" [] false test_spec z3;

Surprisingly, this isn't the case:

$ ~/Software/saw-1.0/bin/saw test.saw



[14:04:51.963] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[14:04:52.037] Verifying test ...
[14:04:52.038] Simulating test ...
[14:04:52.039] Checking proof obligations test ...
[14:04:52.054] Subgoal failed: test /home/ryanscott/Documents/Hacking/SAW/test.saw:13:1: error: in llvm_points_to
Literal equality postcondition

[14:04:52.054] SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 226}
[14:04:52.054] ----------Counterexample----------
[14:04:52.054]   x: 254
[14:04:52.054] ----------------------------------
[14:04:52.054] Stack trace:
"llvm_verify" (/home/ryanscott/Documents/Hacking/SAW/test.saw:13:1-13:12)
Proof failed.

The counterexample given (x: 254) doesn't make much sense, since that should fail the condition x == 1 and therefore cause the point-to check against 1 : [8] to never occur. What is going on?

My hunch is that the code here is responsible:

saw-script/src/SAWScript/Crucible/LLVM/Override.hs

Lines 1612 to 1619 in 9a390f3

	pred_' <- case maybe_cond of
	Just cond -> do
	cond' <- instantiateExtResolveSAWPred sc cc (ttTerm cond)
	liftIO $ W4.impliesPred sym cond' pred_
	Nothing -> return pred_
	addAssert pred_' md $ Crucible.SimError loc $
	Crucible.AssertFailureSimError (show $ PP.vcat badLoadSummary) ""
	pure Nothing <* matchArg opts sc cc spec prepost md res_val memTy val'

This asserts a condition involving the validity of reading from the pointer's memory in a conditional points-to statement, and this does indeed take the condition into account. After this, however, it unconditionally calls matchArg on the right-hand side value. This is almost certainly wrong, as we should only be doing this matching step if the condition holds.

Fixing this will likely require some refactoring of how matchArg works such that it returns a symbolic predicate representing whether the match succeeds or not. That we, we can properly construct an implication involving the condition term.

[RyanGlScott]

I took a closer look at the code in question. For the most part, I think it would be straightforward to refactor matchArg to return a Pred, as the "leaves" of matchArg typically call out to addAssert. We could change this so that we return the Pred in the code here and then construct an implication involving cond'.

There is one complication: one of the leaves of matchArg calls out to addTermEq (here) rather than addAssert. addTermEq doesn't take a raw Pred as an argument, so it's not obvious to me what the best way to make this function return one. In fact, this code used to use addAssert, but it was changed to addTermEq in #1078. @andreistefanescu, do you think it would be possible to refactor this code to make it return a Pred?