test0036_global is fragile due to undocumented assumptions #1155
Labels
documentation
Issues involving documentation
subsystem: crucible-llvm
Issues related to LLVM bitcode verification with crucible-llvm
test assets
Issues involving test programs or other test assets
Comments
RyanGlScott
added
documentation
|
I'm in favor of repairing the test, probably by changing the ints to be unsigned (signed overflow is just a distraction here) and adding postconditions for the globals. |
|
Perhaps both are useful to capture: fixing the test for the non-optimized version, and documenting that the optimized version does not fail, along with some more details on why it doesn't. The latter helps capture both (a) the behavior of optimization is documented and can be referred to as an example, and (b) if the optimization behavior changes, we will be alerted to that fact by this test now failing. |
|
I tried the following naïve fix: diff --git a/intTests/test0036_global/test.c b/intTests/test0036_global/test.c
index 5980bc52..1212d461 100644
--- a/intTests/test0036_global/test.c
+++ b/intTests/test0036_global/test.c
@@ -1,15 +1,15 @@
-int x = 0;
+unsigned int x = 0;
-int f(int y) {
+unsigned int f(unsigned int y) {
x = x + 1;
return x + y;
}
-int g(int z) {
+unsigned int g(unsigned int z) {
x = x + 2;
return x + z;
}
-int h(int w) {
+unsigned int h(unsigned int w) {
return g(f(w));
}
diff --git a/intTests/test0036_global/test.saw b/intTests/test0036_global/test.saw
index 07ee72d8..ba56a9a4 100644
--- a/intTests/test0036_global/test.saw
+++ b/intTests/test0036_global/test.saw
@@ -10,6 +10,7 @@ f_spec <- llvm_verify m "f" [] true (do {
y <- llvm_fresh_var "y" (llvm_int 32);
init_global "x";
llvm_execute_func [llvm_term y];
+ llvm_points_to (llvm_global "x") (llvm_term {{ 1 : [32] }});
llvm_return (llvm_term {{ 1 + y : [32] }});
}) abc;
@@ -17,6 +18,7 @@ g_spec <- llvm_verify m "g" [] true (do {
z <- llvm_fresh_var "z" (llvm_int 32);
init_global "x";
llvm_execute_func [llvm_term z];
+ llvm_points_to (llvm_global "x") (llvm_term {{ 2 : [32] }});
llvm_return (llvm_term {{ 2 + z : [32] }});
}) abc;
@@ -26,5 +28,6 @@ llvm_verify m "h" [f_spec, g_spec] true (do {
w <- llvm_fresh_var "w" (llvm_int 32);
init_global "x";
llvm_execute_func [llvm_term w];
+ llvm_points_to (llvm_global "x") (llvm_term {{ 3 : [32] }});
llvm_return (llvm_term {{ 4 + w : [32] }});
}) abc;However, that still doesn't verify: I thought that it would, given this comment: saw-script/intTests/test0036_global/test.saw Lines 23 to 25 in 99a0dad However, the fact that |
RyanGlScott
added a commit
that referenced
this issue
May 7, 2021
Previously, `test0036_global` only passed by sheer accident, as the overrides it was registering would have failed to apply at a lower optimization level. To make sure that all of the relevant code paths are exercised, this patch reworks `test0036_global` such that: * There are now separate `.saw` files for testing different properties when `test.c` is compiled at `-O1` or `-O2`. I've also checked in the relevant `.ll` files so that the difference between the generated `.bc` files at different optimization settings can be examined. For more details, consult the `README` in the `test0036_global` directory. * `test.c` now uses `unsigned int`s instead of `int`s to avoid complicating things with signed overflow. Fixes #1155.
|
I took some liberties in reworking |
sauclovian-g
added
test assets
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I was recently perplexed because I wrote a SAW spec that was almost identical to that of
intTests/test0036_global, but while the spec intest0036_globalverified successfully, mine was rejected. In fact, I discovered thattest0036_globalonly seemed to work if used thetest.bcfile that was checked into thesaw-scriptrepo. If I recompiledtest.bclike so:And then ran
saw test.saw, it would fail thusly:At first, I thought this was simply because the checked-in
test.bcfile was compiled with-fno-strict-overflowflag (this wasn't written down anywhere, so I couldn't be sure). To test this hypothesis, I again recompiledtest.bc, this time like so:This time, however,
saw test.sawfailed for an entirely different reason:And indeed,
test.sawuses anllvm_points_toprecondition onllvm_global "x"without a corresponding postcondition. So why does the checked-in version oftest.bcnot trigger this error? Some further debugging reveals that the optimization level is likely the culprit. If I compiletest.bcusing the-O2flag like so:Then
saw test.sawpasses. But this is horribly delicate! Iftest.sawis relying on optimizations in order to succeed, then we should either:test0036_global/test.sawso that it passes regardless of what combination of optimization flags and/or-fno-strict-overflowis used, ortest0036_global/README.I'd personally favor (1) over (2), but I could be convinced of (2) with a persuasive argument. Regardless of which approach we go with, we should also update the SAW manual, which includes an example very similar to
test0036_global/test.saw, to reflect our new understanding.The text was updated successfully, but these errors were encountered: