Merge pull request #1890 from GaloisInc/bb/glob-manual-example

Fix global variable example in manual

doc/manual/manual.md

@@ -2451,7 +2451,7 @@ verification](#compositional-verification).
 To understand the issues surrounding global variables, consider the following C
 code:
 
-<!-- This should (partially) match intTests/test0036_globals/test.c -->
+<!-- This matches intTests/test0036_globals/test-signed.c -->
 ~~~
 int x = 0;
 
@@ -2468,7 +2468,7 @@ int g(int z) {
 
 One might initially write the following specifications for `f` and `g`:
 
-<!-- This should (partially) match intTests/test0036_globals/test-fail.saw -->
+<!-- This matches intTests/test0036_globals/test-signed-fail.saw -->
 ~~~
 m <- llvm_load_module "./test.bc";
 
@@ -2499,19 +2499,21 @@ To deal with this, we can use the following function:
 Given this function, the specifications for `f` and `g` can make this
 reliance on the initial value of `x` explicit:
 
-<!-- This should (partially) match intTests/test0036_globals/test.saw -->
+<!-- This matches intTests/test0036_globals/test-signed.saw -->
 ~~~
 m <- llvm_load_module "./test.bc";
 
 
 let init_global name = do {
+  llvm_alloc_global name;
   llvm_points_to (llvm_global name)
                  (llvm_global_initializer name);
 };
 
 f_spec <- llvm_verify m "f" [] true (do {
     y <- llvm_fresh_var "y" (llvm_int 32);
     init_global "x";
+    llvm_precond {{ y < 2^^31 - 1 }};
     llvm_execute_func [llvm_term y];
     llvm_return (llvm_term {{ 1 + y : [32] }});
 }) abc;
@@ -2521,7 +2523,9 @@ which initializes `x` to whatever it is initialized to in the C code at
 the beginning of verification. This specification is now safe for
 compositional verification: SAW won't use the specification `f_spec`
 unless it can determine that `x` still has its initial value at the
-point of a call to `f`.
+point of a call to `f`. This specification also constrains `y` to prevent
+signed integer overflow resulting from the `x + y` expression in `f`,
+which is undefined behavior in C.
 
 ## Preconditions and Postconditions
 

intTests/test0036_global/Makefile

@@ -1,6 +1,6 @@
 CC = clang
 CFLAGS = -g -emit-llvm -frecord-command-line
-OUTPUT_FILES = test-O1.bc test-O2.bc test-O1.ll test-O2.ll
+OUTPUT_FILES = test-O1.bc test-O2.bc test-O1.ll test-O2.ll test-signed.bc
 
 all: $(OUTPUT_FILES)
 
@@ -12,6 +12,8 @@ test-O2.bc : test.c
 	$(CC) $(CFLAGS) -O2 -c $< -o $@
 test-O2.ll : test.c
 	$(CC) $(CFLAGS) -O2 -S $< -o $@
+test-signed.bc : test.c
+	$(CC) $(CFLAGS) -O0 -c $< -o $@
 
 .PHONY: clean
 clean:

intTests/test0036_global/test-signed-fail.saw

@@ -0,0 +1,13 @@
+m <- llvm_load_module "test-signed.bc";
+
+f_spec <- llvm_verify m "f" [] true (do {
+    y <- llvm_fresh_var "y" (llvm_int 32);
+    llvm_execute_func [llvm_term y];
+    llvm_return (llvm_term {{ 1 + y : [32] }});
+}) abc;
+
+g_spec <- llvm_llvm_verify m "g" [] true (do {
+    z <- llvm_fresh_var "z" (llvm_int 32);
+    llvm_execute_func [llvm_term z];
+    llvm_return (llvm_term {{ 2 + z : [32] }});
+}) abc;

intTests/test0036_global/test-signed.c

@@ -0,0 +1,11 @@
+int x = 0;
+
+int f(int y) {
+  x = x + 1;
+  return x + y;
+}
+
+int g(int z) {
+  x = x + 2;
+  return x + z;
+}

intTests/test0036_global/test-signed.saw

@@ -0,0 +1,16 @@
+m <- llvm_load_module "test-signed.bc";
+
+
+let init_global name = do {
+  llvm_alloc_global name;
+  llvm_points_to (llvm_global name)
+                 (llvm_global_initializer name);
+};
+
+f_spec <- llvm_verify m "f" [] true (do {
+    y <- llvm_fresh_var "y" (llvm_int 32);
+    init_global "x";
+    llvm_precond {{ y < 2^^31 - 1 }};
+    llvm_execute_func [llvm_term y];
+    llvm_return (llvm_term {{ 1 + y : [32] }});
+}) abc;

intTests/test0036_global/test.sh

@@ -8,7 +8,9 @@ set -e
 $SAW test-appropriate-overrides.saw
 $SAW test-global-initializer.saw
 $SAW test-sketchy-overrides-O2.saw
+$SAW test-signed.saw
 
 # These tests should fail
 ! $SAW test-no-init.saw
 ! $SAW test-sketchy-overrides-O1.saw
+! $SAW test-signed-fail.saw