Merge pull request #712 from GaloisInc/x86-mutable-globals

Support mutable globals during x86 verification

Author: chameco

intTests/test_llvm_x86_04/test.S

@@ -0,0 +1,15 @@
+section .bss
+global var
+var:    resq 1
+section .text
+global addvar
+addvar:
+        mov rax, [rdi]
+        mov rbx, var
+        add rax, 1
+        mov [rdi], rax
+        ret
+global _start
+_start:
+        mov rax, 60
+        syscall

intTests/test_llvm_x86_04/test.c

@@ -0,0 +1,12 @@
+#include <stdint.h>
+#include <stdio.h>
+
+extern uint64_t var;
+
+extern void addvar(uint64_t *i);
+
+void test() {
+	(void) var;
+	uint64_t i = 42;
+	addvar(&i);
+};

intTests/test_llvm_x86_04/test.saw

@@ -0,0 +1,19 @@
+enable_experimental;
+
+m <- llvm_load_module "test.bc";
+
+let addvar_setup = do {
+  crucible_alloc_global "var";
+  var <- crucible_fresh_var "var" (llvm_int 64);
+  crucible_points_to (crucible_global "var") (crucible_term {{ 2 : [64] }});
+
+  ptr <- crucible_alloc (llvm_int 64);
+  val <- crucible_fresh_var "val" (llvm_int 64);
+  crucible_points_to ptr (crucible_term val);
+
+  crucible_execute_func [ptr];
+
+  valprime <- crucible_fresh_var "_val" (llvm_int 64);
+  crucible_points_to ptr (crucible_term valprime);
+};
+crucible_llvm_verify_x86 m "./test" "addvar" [] false addvar_setup;

intTests/test_llvm_x86_04/test.sh

@@ -0,0 +1,6 @@
+set -e
+
+yasm -felf64 test.S
+ld test.o -o test
+clang -c -emit-llvm test.c
+$SAW test.saw