Generalizing crucible_points_to beyond equality testing

[AndrewTolmach]

Currently, there seems to be no way to characterize a post-state LLVM location except by giving its value precisely using crucible_points_to. But sometimes this is quite inconvenient, because we may not know an exact characterization of the value. This is particularly problematic when we have a Cryptol model using types that are not isomorphic to the corresponding C types. So it would be nice to have a more general mechanism for specifying the desired post-state.

Here's an example of the problem:
C treats any non-zero value as True. We'd like to show that f() always sets y to a True value, but we can only check whether it sets y to a particular value (here 1). This doesn't work if the initial value of y is any non-zero value other than 1.

f.c:

typedef char bool;
bool y;
void f() {
  if (y == 0)
    y = 1;
}

f.saw:

m <- llvm_load_module "f.bc";
print m;
load_crucible_llvm_module "f.bc";
crucible_llvm_verify "f" [] false 
           do { y <- crucible_fresh_var "y" (llvm_int 8); 
                crucible_points_to (crucible_global "y") (crucible_term y); 
                crucible_execute_func []; 
                crucible_points_to (crucible_global "y") (crucible_term {{(zero #[True]) : [8]}});
	      }
           abc;

Results:

Loading module Cryptol
Loading file "/Users/andrewtolmach/experiments/f.saw"
Module: f.bc
Types:

Globals:
  @y = common global i8

External references:

Definitions:
  void @f()

Subgoal failed: @f points-to assertion
SolverStats {solverStatsSolvers = fromList ["ABC"], solverStatsGoalSize = 57}
("y",128)
saw: user error ("crucible_llvm_verify" (/Users/andrewtolmach/experiments/f.saw:4:1):
Proof failed.)

[brianhuffman]

Once we implement support for crucible_fresh_var in the post-state section of a spec (#182) then we'll be able to write something like this:

crucible_llvm_verify "f" [] false 
           do {
                y <- crucible_fresh_var "y" (llvm_int 8); 
                crucible_points_to (crucible_global "y") (crucible_term y); 
                crucible_execute_func [];
                y_new <- crucible_fresh_var "y_new" (llvm_int 8);
                crucible_points_to (crucible_global "y") (crucible_term y_new);
                crucible_postcond {{ y_new > 0 }};
	      }
           abc;

[brianhuffman]

We should be able to close this once we add the above example as a regression test.

[sauclovian-g]

This is fixed, we just need to add the test and that should get done already.