Don't concretize applications of uninterpreted functions in SAW's symbolic simulator

[RyanGlScott]

Consider this SAW spec, which was taken from #1903:

primitive.c

int prim(int a){
  return a;
}

int foo(int* y){
  int x = 1;
  *y = prim(x);
  return 1;
}

Primitive.cry

module Primitive where

primitive prim : [32] -> [32]

primitive.saw

import "Primitive.cry";

m <- llvm_load_module "primitive.bc";

let i32 = llvm_int 32;

let prim_spec = do {
  a <- crucible_fresh_var "a" i32;

  crucible_execute_func [(crucible_term a)];

  crucible_return (crucible_term {{ prim a }});
};

prim_spec_ov <- crucible_llvm_unsafe_assume_spec
m
"prim"
prim_spec;

let foo_spec = do {
  ptr <- llvm_alloc i32;
  crucible_execute_func [ptr];
  crucible_return (crucible_term {{ 1 : [32]}});
};

crucible_llvm_verify m "foo"
[prim_spec_ov]
true
foo_spec
(do {
print_goal;
w4_unint_z3 ["prim"];
});

run.sh

clang -g -O0 -c -emit-llvm -o primitive.bc primitive.c
# clang -S -g -O0 -c -emit-llvm primitive.c
saw primitive.saw

This spec is very careful to mark prim as uninterpreted, and as such, one would expect this spec to verify successfully. Unfortunately, this is not actually the case in practice, which you can see if you invoke run.sh:

[22:26:36.971] Loading file "../primitive/primitive.saw"
[22:26:37.067] Assume override prim
[22:26:37.109] Verifying foo ...
[22:26:37.124] Simulating foo ...
[22:26:37.125] Registering overrides for `prim`
[22:26:37.125]   variant `Symbol "prim"`
[22:26:37.125] Matching 1 overrides of  prim ...
[22:26:37.126] Branching on 1 override variants of prim ...
[22:26:37.126] Run-time error: Cannot evaluate neutral term
cryptol:/Primitive/prim

The reason this happens is because when SAW performs symbolic execution, it frequently attempts to concretize certain terms. This is often a huge win for performance, as evaluating concrete terms is much faster than evaluating symbolic ones. But there is a tension between concretization and uninterpreted functions: if you attempt to concretize things too much, you might accidentally evaluate something that was never meant to be evaluated, since as a Cryptol primitive.

As such, SAW uses heuristics to figure out when to concretize terms or not, and these heuristics aren't perfect. In particular, whenever it sees a function application f x (where x is a free variable), it will only concretize the application if x is itself a concrete term. In the case of your program, you have:

  int x = 1;
  *y = prim(x);

After that gets translated to SAWCore, that looks something like:

... Cryptol:/Primitive/prim 1 ...

Here, SAW sees a function applied to a concrete term 1, so it tries to concretize the function application. But Cryptol:/Primitive/prim was never meant to be evaluated, and so SAW crashes at simulation time.

This is all rather unfortunate, especially since it is affecting SAW proofs in the wild. There are ways to restructure the Cryptol code slightly to work around the issue, such as the workaround from https://github.com/GaloisInc/saw-script/pull/1903#issuecomment-1675141693, but it would be far better if SAW "just worked" here. After all, SAW already has knowledge about what functions are uninterpreted during symbolic execution, so this knowledge ought to extend to the heuristics that SAW uses when concretizing function applications.

This ticket exists to track this idea.

[RyanGlScott]

@eddywestbrook and I looked at this some. Given that "Cannot evaluate neutral term" is an error message that is thrown by the concrete evaluator, the most likely place where the aforementioned heuristics are implemented is here:

https://github.com/GaloisInc/saw-script/blob/e0e94c6044e832081e28af8e9bdbf9a130caca48/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs#L735-L740

This code checks for closed SAWCore terms (i.e., terms without any symbolic content) by checking if they are free of any ExtCns. My original thought was to extend this code to make it aware of any uninterpreted functions that the user declared via a tactic like w4_unint_z3. This wouldn't work, however, as this code is run as part of simulating the C code, which happens before the w4_unint_z3 tactic is ever invoked. You can see this for yourself by replacing the call to w4_unint_z3 ["prim"] in the program above with something like admit "Admitted"—you'll still get the same error if you do.

In light of this, perhaps we should try a different approach: refine the heuristics above to check if tm contains a primitive (e.g., prim), and if so, don't attempt to concretely evaluate it. We'd need to be careful about this, since there are some Cryptol primitives that SAW does attach computational content to, and we would still want to evaluate those. Luckily, I believe all of those constants are listed in constMap, so I believe this should be relatively simple to check for.

[andreistefanescu]

My preference would be to properly handle the exception. Depending on evaluation, the term may evaluate to a concrete value even if it contains an undefined primitive.

[RyanGlScott]

Indeed, that is another option worth considering.

For what it's worth, I discovered that the use of evalSharedTerm in https://github.com/GaloisInc/saw-script/issues/1906#issuecomment-1679387599 is not where the Cannot evaluate neutral term error is coming from in the test case above. I haven't figured out which evalSharedTerm is actually the culprit.