Open RyanGlScott opened 10 months ago
This issue can also be observed with postconditions, not just preconditions:
// test.c
#include "stdint.h"
void foo (uint8_t x) {}
void bar (uint8_t x) {
foo(x);
}
// test.saw
m <- llvm_load_module "test.bc";
let spec_ghost ghost = do {
x <- llvm_fresh_var "x" (llvm_int 8);
llvm_execute_func [llvm_term x];
ghost_post <- llvm_fresh_var "ghost_post" (llvm_int 8);
llvm_postcond {{ghost_post == x}};
llvm_ghost_value ghost ghost_post;
};
ghost <- declare_ghost_state "ghost";
ghost_ov <- llvm_unsafe_assume_spec m "foo" (spec_ghost ghost);
ghost_res <- llvm_verify m "bar" [ghost_ov] true (spec_ghost ghost) z3;
This succeeds. If you swap the order of the llvm_postcond
and llvm_ghost_value
statements, however:
m <- llvm_load_module "test.bc";
let spec_ghost ghost = do {
x <- llvm_fresh_var "x" (llvm_int 8);
llvm_execute_func [llvm_term x];
ghost_post <- llvm_fresh_var "ghost_post" (llvm_int 8);
llvm_ghost_value ghost ghost_post;
llvm_postcond {{ghost_post == x}};
};
ghost <- declare_ghost_state "ghost";
ghost_ov <- llvm_unsafe_assume_spec m "foo" (spec_ghost ghost);
ghost_res <- llvm_verify m "bar" [ghost_ov] true (spec_ghost ghost) z3;
Then verification fails:
$ ~/Software/saw-1.1/bin/saw test.saw
[16:35:22.855] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[16:35:22.882] Assume override foo
[16:35:22.920] Verifying bar ...
[16:35:22.932] Simulating bar ...
[16:35:22.933] Registering overrides for `foo`
[16:35:22.933] variant `Symbol "foo"`
[16:35:22.934] Matching 1 overrides of foo ...
[16:35:22.934] Branching on 1 override variants of foo ...
[16:35:22.935] Applied override! foo
[16:35:22.935] Checking proof obligations bar ...
[16:35:22.952] Subgoal failed: bar /home/ryanscott/Documents/Hacking/SAW/test.saw:16:14: error: in llvm_postcond
postcondition
[16:35:22.952] SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 223}
[16:35:22.953] ----------Counterexample----------
[16:35:22.953] x: 1
[16:35:22.953] ghost_post: 254
[16:35:22.953] ghost_post: 1
[16:35:22.953] ----------------------------------
[16:35:22.953] Stack trace:
"llvm_verify" (/home/ryanscott/Documents/Hacking/SAW/test.saw:16:14-16:25)
Proof failed.
This suggests a similar fix: always run llvm_ghost_value
postconditions after all other postconditions.
Consider this example, courtesy of @qsctr:
This looks plausible, but if you run it, SAW will fail to verify
get2_spec
:This counterexample is bewildering. How can
get::ghost
be4294967253
whenget
's preconditions requireget::ghost
to be42
? It gets even weirder when you realize that if you make this small change toget_spec
:Then verification succeeds! This flies in the face of usual SAW conventions, where the order of preconditions should not matter.
The reason that this happens is somewhat technical. Currently, SAW happens to process each precondition in a spec from top to bottom. Processing a precondition like
llvm_precond {{ x == g }}
extends a variable substitution that SAW maintains such thatg
will map tox
. Therefore, if you process thellvm_ghost_value ghost g
afterwards, then SAW will mapg
tox
, making it as though you had writtenllvm_ghost_value ghost x
. SAW knows how to link this back to the argument to theget
function, and all is well.If the two preconditions are written in the opposite order, however, then when SAW processes
llvm_ghost_value ghost g
first, it has no idea thatg
is related tox
in any way. As such, it will allowg
to be any value whatsoever, and indeed, symbolic execution will happily pick4294967253
as its value. Bad bad bad!Really, we should always run
llvm_ghost_value
preconditions after all other preconditions, as running the other preconditions may introduce important variable equalities that are essential to making compositional overrides (such asget
) apply successfully. This special-casing ofllvm_ghost_value
makes sense if you think of ghost values as a type of argument to the function, and indeed, we already special-case the handling of ordinary function arguments (viallvm_execute_func
).Although the example above uses the LLVM backend, there is nothing inherently LLVM-specific about it, and the bug will also apply to the JVM and MIR backends after #1958 lands.