Open RyanGlScott opened 6 months ago
Admittedly, this example is rather contrived, but it would be natural to write something like
g2_spec
if the function took some ghost state as an argument.
Actually, I just realized that adding ghost state makes this error go away. That is, if you write this:
// test.saw
m <- llvm_load_module "test.bc";
ghost <- llvm_declare_ghost_state "ghost";
let g1_spec = do {
x <- llvm_fresh_var "x" (llvm_int 32);
llvm_ghost_value ghost x;
llvm_execute_func [llvm_term x];
llvm_return (llvm_term x);
};
let g2_spec = do {
x <- llvm_fresh_var "x" (llvm_int 32);
y <- llvm_fresh_var "y" (llvm_int 32);
llvm_precond {{ x == y }};
llvm_ghost_value ghost y;
llvm_execute_func [llvm_term x];
llvm_return (llvm_term y);
};
let f_spec = do {
x <- llvm_fresh_var "x" (llvm_int 32);
llvm_ghost_value ghost x;
llvm_execute_func [llvm_term x];
llvm_return (llvm_term x);
};
g1_ov <- llvm_unsafe_assume_spec m "g" g1_spec;
g2_ov <- llvm_unsafe_assume_spec m "g" g2_spec;
llvm_verify m "f" [g1_ov] false f_spec z3;
llvm_verify m "f" [g2_ov] false f_spec z3;
Then both calls to llvm_verify
succeed. It would still be nice if the original specs worked on their own, however.
This kind of spec also arises naturally if you have a bunch of inputs and a bunch of outputs, and some of the outputs are equal to some of the inputs.
Here is a slightly more exotic variant of the program above:
// test.c
#include <stdint.h>
void g(uint32_t x) {}
void f(uint32_t x) {
g(x);
}
// Test.cry
newtype T = { runT : [32] }
runT_ : T -> [32]
runT_ t = t.runT
// test.saw
enable_experimental;
m <- llvm_load_module "test.bc";
import "Test.cry";
let g1_spec = do {
y <- llvm_fresh_cryptol_var "y" {| T |};
llvm_execute_func [llvm_term {{ y.runT }}];
};
let g2_spec = do {
y <- llvm_fresh_cryptol_var "y" {| T |};
llvm_execute_func [llvm_term {{ runT_ y }}];
};
let f_spec = do {
x <- llvm_fresh_var "x" (llvm_int 32);
llvm_execute_func [llvm_term x];
};
g1_ov <- llvm_unsafe_assume_spec m "g" g1_spec;
g2_ov <- llvm_unsafe_assume_spec m "g" g2_spec;
llvm_verify m "f" [g1_ov] false f_spec z3;
llvm_verify m "f" [g2_ov] false f_spec z3;
g1_spec
and g2_spec
are almost identical, except that g1_spec
uses a direct Cryptol record accessor, whereas g2_spec
has one more level of indirection via a Cryptol function. Despite the two specs' similarities, only g1_spec
can be used as a compositional override when verifying f_spec
:
$ ~/Software/saw-1.1/bin/saw test.saw
[20:51:22.982] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[20:51:23.092] Assume override g
[20:51:23.131] Assume override g
[20:51:23.131] Verifying f ...
[20:51:23.131] Simulating f ...
[20:51:23.131] Registering overrides for `g`
[20:51:23.131] variant `Symbol "g"`
[20:51:23.132] Matching 1 overrides of g ...
[20:51:23.132] Branching on 1 override variants of g ...
[20:51:23.132] Applied override! g
[20:51:23.132] Checking proof obligations f ...
[20:51:23.132] Proof succeeded! f
[20:51:23.132] Verifying f ...
[20:51:23.132] Simulating f ...
[20:51:23.132] Registering overrides for `g`
[20:51:23.132] variant `Symbol "g"`
[20:51:23.132] Matching 1 overrides of g ...
[20:51:23.133] Stack trace:
"llvm_verify" (/home/ryanscott/Documents/Hacking/SAW/test.saw:26:1-26:12)
Symbolic execution failed.
Abort due to assertion failure:
test.c:7:3: error: in f
All overrides failed during structural matching:
* Name: g
Location: /home/ryanscott/Documents/Hacking/SAW/test.saw:23:10
Argument types:
- i32
Return type: <void>
Arguments:
- symbolic integer: width = 32
at /home/ryanscott/Documents/Hacking/SAW/test.saw:23:10
Fresh variable(s) not reachable via points-tos from function inputs/outputs:
fresh:y#934 : Main::T
Stack frame f
Allocations:
StackAlloc 4 0x4:[64] Mutable 4-byte-aligned test.c:6:17
Writes:
Indexed chunk:
4 |-> *(4, 0x0:[64]) := c@24:bv
Base memory
Allocations:
GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [defined function ] f
GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [defined function ] g
GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.declare
Upon a closer inspection, the discrepancy in https://github.com/GaloisInc/saw-script/issues/2035#issuecomment-1971938335 is perhaps not that unreasonable. After typechecking, Cryptol desugars T
to [32]
, and y.runT
will desugar to just y
. This means that g1_spec
is morally equivalent to:
let g1_spec = do {
y <- llvm_fresh_var "y" (llvm_int 32);
// llvm_execute_func [llvm_term y];
llvm_execute_func [llvm_term y];
};
And that is quite straightforward.
What makes g2_spec
not as straightforward is that we have to match the term {{ runT_ y }}
, where runT_
is a function. The only way to know if y
is reachable in this instance is to know that runT_ y
uniquely determines y
. It does in this case, but this would require a more sophisticated analysis in general to handle arbitrary functions. Moreover, we don't want to conclude that y
is reachable if we were matching against, say, const 42 y
.
It might be possible to deal with the most irritating manifestations of this issue by, if you run into a function, just trying to unfold it and see if that gives something tractable.
But that's quite different from reasoning about equalities. Or worse (as came up on Formal VerSo this week) equivalences that are not strict equality.
I suspect that unfolding functions would only work in the most trivial of scenarios, where f x
unfolds directly to x
(e.g., the contrived test case in https://github.com/GaloisInc/saw-script/issues/2035#issuecomment-1971938335). Most interesting functions f
will be more complex than this, and SAW doesn't really have the machinery to reason about this.
Generally speaking, if you write llvm_execute_func [llvm_term y]
, SAW expects y
to be a concrete term or a bare symbolic variable. SAW wasn't really built with the expectation that y
would be a compound term such as f x
, and that is where the challenge lies.
Yes and no; remember that case was contrived because exactly the same thing came up in reality (in Formal VerSo, for anyone following along at home). But also, it was deep inside a nontrivial Cryptol model, where the modularity of private newtypes and accessor functions has some value.
IDK, it might be time to revisit that expectation because the things involved in that case (multiple different representations of the same values, so you have to be able to reason across their equivalences) isn't entirely uncommon in a lot of contexts. :-|
Given this C program:
And this SAW file:
Verifying
f
by usingg1_ov
as an override works, as expected:If you uncomment the
llvm_verify m "f" [g2_ov] false f_spec z3;
line, however, that does not work:This is surprising, as
g2_spec
out to be equivalent tog1_spec
. SAW is complaining that the fresh variabley
is not reachable from the function inputs, but it ought to be reachable via thex == y
precondition. Sadly, SAW doesn't look at preconditions when reasoning about fresh variable reachability, but it really ought to.You might ask: why would you ever write
g2_spec
when you could instead writeg1_spec
? Admittedly, this example is rather contrived, but it would be natural to write something likeg2_spec
if the function took some ghost state as an argument.