Catch and handle gracefully when concrete evaluation produces an error

[pennyannn]

Problem:

Say there is a user-declared primitive in Cryptol specification. The primitive doesn't have a definition. During override matching phase, the primitive is being concretely evaluated because its arguments could be reduced to concrete values.

Observation:

This causes SAW to fail and exit the REPL with the following error message:

[19:10:56.690] Run-time error: Cannot evaluate neutral term
cryptol:/.../the_primitive

What is done:

This PR fixes the problem by catching the error produced by concrete evaluation and gracefully return Nothing instead of causing SAW to fail. By doing this, the terms that could not be reduced to concrete values are treated as non-ground terms.

[RyanGlScott]

Hi @pennyannn!

Can you explain the motivation behind this PR a bit further? In particular, what specific problem is this patch addressing? Do you have a test case that shows SAW doing something wrong that is corrected by this patch?

[pennyannn]

Hi @RyanGlScott

Here's a small example showing the problem.

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

Run run.sh and the output is:

[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

[RyanGlScott]

Thanks @pennyannn, that's very helpful context.

Before getting into the particulars of this PR, it might be helpful to go over why this particular SAW spec fails to verify. At first glance, it does seem like this should work, since you are very careful to treat the Cryptol prim function as uninterpreted by using the w4_unint_z3 ["prim"] tactic. But despite this, SAW nevertheless tries to evaluate it during simulation, which is surprising. What is going on?

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, but there are ways to restructure things such that avoid driving the heuristics into overly eager concretization. One way is to make your foo function more general:

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

Note that x has made made into an additional argument. Now, if you define your foo specification like so:

let foo_spec = do {
  ptr <- llvm_alloc i32;
  x <- llvm_fresh_var "a" i32;
  
  llvm_execute_func [ptr, llvm_term x];
  
  // Optional
  // llvm_points_to ptr (llvm_term {{ prim x }});
  llvm_return (llvm_term {{ 1 : [32]}});
};

Then the verification succeeds, since when SAW sees the function application Cryptol:/Primitive/prim x during simulation, it won't attempt to concretize it due to x being symbolic. This is a technique that is frequently used in https://github.com/awslabs/aws-lc-verification to write SAW specifications defined in terms of the Cryptol error function (which is similar in spirit to using a Cryptol primitive).

If changing the C code isn't an option, another way you can make this work is by changing prim to a fresh_symbolic constant rather than a Cryptol function:

// import "Primitive.cry";
prim <- fresh_symbolic "prim" {| [32] -> [32] |};

// The rest of primitive.saw stays as before...

fresh_symbolic allocates a top-level parameter than can be used across multiple specs. Importantly, SAW won't crash when trying to concretize it during symbolic execution.

(Sorry for the exposition dump, but this stuff is rather subtle.)

---

Returning to the topic of your PR, my understanding of your changes is that whenever SAW crashes when trying to concretize a SAWCore Term, the exception will be caught, and a symbolic term will instead be returned. In effect, this achieves the same end goal as using something like fresh_symbolic, but it's much less obvious. It's hard to predict all of the consequences of this change—for instance, it's possible that this would swallow errors in other types of programs that really are meant to fail.

For this reason, I'm rather leery about this change, as I think this could have unforeseen consequences down the line. My inclination is to instead have users be more explicit about their intentions when using uninterpreted functions, by using fresh_symbolic or otherwise. What do you think?

[pennyannn]

Thanks for the detailed explanation! However, I don't think the proposed changes will satisfy my needs.

Changing the C code that much is not an option like you predicted. If I understand correctly, the second option will not declare prim as a primitive in Cryptol. Note that I simplified the example. In the real use case, the prim is used in other specifications in the Cryptol file. Also, we reply on primitive in Cryptol being translated into a Variable in a Section in Coq.

Your understanding of the PR is correct. How would you rather make the change to SAW so that it will solve the problem but won't have unpredictable consequences? I'm thinking maybe there should be a user interface that specifies certain function to be exceptions to concrete evaluation. Then inside concrete evaluation, it will not try to evaluate those function calls. What about this solution?

[RyanGlScott]

I'm thinking maybe there should be a user interface that specifies certain function to be exceptions to concrete evaluation. Then inside concrete evaluation, it will not try to evaluate those function calls.

Truth be told, I don't actually know off-hand which part of the symbolic execution engine is responsible for implementing the aforementioned heuristics, so it's difficult to say if it would be straightforward to do this.

That being said, if you need something that works in today's SAW, then something like this ought to suffice:

module Primitive where

primitive prim : () -> [32] -> [32]

u <- fresh_symbolic "u" {| () |};

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

  crucible_execute_func [(crucible_term a)];

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

...

Here, I've added an additional () argument to prim's Cryptol definition. This way, you can continue to refer to prim in Cryptol specifications, but you'd have to supply an additional () argument when applying it. On the SAW side, this means passing a symbolic () argument to ensure that the overall application remains opaque to the simulator.

[pennyannn]

That's an interesting proposal. Let me try it out and get back to you!

[pennyannn]

Hi @RyanGlScott, the last proposal works for us. I defined a function prim_wrapper and override prim in C with prim_wrapper. Then I defined a rewrite rule that rewrites prim_wrapper back to prim. This way, I get away with the concrete evaluation in override step and the Coq proof will use prim instead of prim_wrapper. See the following:

primitive.saw

import "Primitive.cry";

m <- llvm_load_module "primitive.bc";

let i32 = llvm_int 32;
u <- fresh_symbolic "u" {| () |};

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

  crucible_execute_func [(crucible_term a)];

  crucible_return (crucible_term {{ prim_wrapper u 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]}});
};

prim_wrapper_prim_equiv <-
prove_print
(w4_unint_z3 ["prim"])
(rewrite (cryptol_ss ()) {{ \x y -> (prim_wrapper x y) == (prim y) }});

crucible_llvm_verify m "foo"
[prim_spec_ov]
true
foo_spec
(do {
simplify (addsimps [prim_wrapper_prim_equiv] empty_ss);
w4_unint_z3 ["prim"];
});

Primitive.cry

module Primitive where

primitive prim : [32] -> [32]

prim_wrapper : () -> [32] -> [32]
prim_wrapper _ x = prim x

Thank you so much for your help!

[pennyannn]

Closing because issue is resolved with a workaround.

[RyanGlScott]

Great, thank you for confirming. For what it's worth, I do think that SAW ought to be able to handle something like your original example, given that SAW's symbolic evaluator already has knowledge about what things should be left uninterpreted. I'll open a separate issue to track this.

[RyanGlScott]

I've opened #1906 for this.