updateExpected

UQ-PAC · Feb 28, 2024 · 37e4c14 · 37e4c14
1 parent 7429876
commit 37e4c14
Show file tree

Hide file tree

Showing 629 changed files with 155,918 additions and 0 deletions.
diff --git a/src/test/correct/arrays_simple/clang/arrays_simple_bap.expected b/src/test/correct/arrays_simple/clang/arrays_simple_bap.expected
@@ -0,0 +1,115 @@
+var {:extern} Gamma_R0: bool;
+var {:extern} Gamma_R31: bool;
+var {:extern} Gamma_R8: bool;
+var {:extern} Gamma_mem: [bv64]bool;
+var {:extern} Gamma_stack: [bv64]bool;
+var {:extern} R0: bv64;
+var {:extern} R31: bv64;
+var {:extern} R8: bv64;
+var {:extern} mem: [bv64]bv8;
+var {:extern} stack: [bv64]bv8;
+const {:extern} $_IO_stdin_used_addr: bv64;
+axiom ($_IO_stdin_used_addr == 1872bv64);
+function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:extern} gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function {:extern} gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function {:extern} memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function {:extern} memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function {:extern} memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function {:extern} {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure {:extern} rely();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+  free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+procedure {:extern} rely_transitive();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+
+implementation {:extern} rely_transitive()
+{
+  call rely();
+  call rely();
+}
+
+procedure {:extern} rely_reflexive();
+
+procedure {:extern} guarantee_reflexive();
+  modifies Gamma_mem, mem;
+
+procedure main();
+  modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
+  free requires (memory_load64_le(mem, 69664bv64) == 0bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free requires (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free requires (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free requires (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free ensures (Gamma_R31 == old(Gamma_R31));
+  free ensures (R31 == old(R31));
+  free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+implementation main()
+{
+  main_basil_entry:
+    assume {:captureState "main_basil_entry"} true;
+    goto lmain;
+  lmain:
+    assume {:captureState "lmain"} true;
+    R31, Gamma_R31 := bvadd64(R31, 18446744073709551584bv64), Gamma_R31;
+    R8, Gamma_R8 := 3bv64, true;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 20bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 20bv64), Gamma_R8);
+    assume {:captureState "%0000089b"} true;
+    R8, Gamma_R8 := 7bv64, true;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 28bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 28bv64), Gamma_R8);
+    assume {:captureState "%000008a8"} true;
+    R8, Gamma_R8 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 20bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 20bv64));
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 8bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 8bv64), Gamma_R8);
+    assume {:captureState "%000008b7"} true;
+    R0, Gamma_R0 := 0bv64, true;
+    R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
+    goto main_basil_return;
+  main_basil_return:
+    assume {:captureState "main_basil_return"} true;
+    return;
+}
+
diff --git a/src/test/correct/arrays_simple/clang/arrays_simple_gtirb.expected b/src/test/correct/arrays_simple/clang/arrays_simple_gtirb.expected
@@ -0,0 +1,115 @@
+var {:extern} Gamma_R0: bool;
+var {:extern} Gamma_R31: bool;
+var {:extern} Gamma_R8: bool;
+var {:extern} Gamma_mem: [bv64]bool;
+var {:extern} Gamma_stack: [bv64]bool;
+var {:extern} R0: bv64;
+var {:extern} R31: bv64;
+var {:extern} R8: bv64;
+var {:extern} mem: [bv64]bv8;
+var {:extern} stack: [bv64]bv8;
+const {:extern} $_IO_stdin_used_addr: bv64;
+axiom ($_IO_stdin_used_addr == 1872bv64);
+function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:extern} gamma_load32(gammaMap: [bv64]bool, index: bv64) returns (bool) {
+  (gammaMap[bvadd64(index, 3bv64)] && (gammaMap[bvadd64(index, 2bv64)] && (gammaMap[bvadd64(index, 1bv64)] && gammaMap[index])))
+}
+
+function {:extern} gamma_store32(gammaMap: [bv64]bool, index: bv64, value: bool) returns ([bv64]bool) {
+  gammaMap[index := value][bvadd64(index, 1bv64) := value][bvadd64(index, 2bv64) := value][bvadd64(index, 3bv64) := value]
+}
+
+function {:extern} memory_load32_le(memory: [bv64]bv8, index: bv64) returns (bv32) {
+  (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))
+}
+
+function {:extern} memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+function {:extern} memory_store32_le(memory: [bv64]bv8, index: bv64, value: bv32) returns ([bv64]bv8) {
+  memory[index := value[8:0]][bvadd64(index, 1bv64) := value[16:8]][bvadd64(index, 2bv64) := value[24:16]][bvadd64(index, 3bv64) := value[32:24]]
+}
+
+function {:extern} {:bvbuiltin "zero_extend 32"} zero_extend32_32(bv32) returns (bv64);
+procedure {:extern} rely();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+  free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+procedure {:extern} rely_transitive();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+
+implementation {:extern} rely_transitive()
+{
+  call rely();
+  call rely();
+}
+
+procedure {:extern} rely_reflexive();
+
+procedure {:extern} guarantee_reflexive();
+  modifies Gamma_mem, mem;
+
+procedure main();
+  modifies Gamma_R0, Gamma_R31, Gamma_R8, Gamma_stack, R0, R31, R8, stack;
+  free requires (memory_load64_le(mem, 69664bv64) == 0bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free requires (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free requires (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free requires (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free ensures (Gamma_R31 == old(Gamma_R31));
+  free ensures (R31 == old(R31));
+  free ensures (memory_load8_le(mem, 1872bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1873bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1874bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1875bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+implementation main()
+{
+  main_basil_entry:
+    assume {:captureState "main_basil_entry"} true;
+    goto $main$__0__$wJJVmeZaRYCZKfoXX5ihZw;
+  $main$__0__$wJJVmeZaRYCZKfoXX5ihZw:
+    assume {:captureState "$main$__0__$wJJVmeZaRYCZKfoXX5ihZw"} true;
+    R31, Gamma_R31 := bvadd64(bvadd64(R31, 18446744073709551583bv64), 1bv64), Gamma_R31;
+    R8, Gamma_R8 := 3bv64, true;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 20bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 20bv64), Gamma_R8);
+    assume {:captureState "1820$0"} true;
+    R8, Gamma_R8 := 7bv64, true;
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 28bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 28bv64), Gamma_R8);
+    assume {:captureState "1828$0"} true;
+    R8, Gamma_R8 := zero_extend32_32(memory_load32_le(stack, bvadd64(R31, 20bv64))), gamma_load32(Gamma_stack, bvadd64(R31, 20bv64));
+    stack, Gamma_stack := memory_store32_le(stack, bvadd64(R31, 8bv64), R8[32:0]), gamma_store32(Gamma_stack, bvadd64(R31, 8bv64), Gamma_R8);
+    assume {:captureState "1836$0"} true;
+    R0, Gamma_R0 := 0bv64, true;
+    R31, Gamma_R31 := bvadd64(R31, 32bv64), Gamma_R31;
+    goto main_basil_return;
+  main_basil_return:
+    assume {:captureState "main_basil_return"} true;
+    return;
+}
+
diff --git a/src/test/correct/arrays_simple/clang_O2/arrays_simple_bap.expected b/src/test/correct/arrays_simple/clang_O2/arrays_simple_bap.expected
@@ -0,0 +1,79 @@
+var {:extern} Gamma_R0: bool;
+var {:extern} Gamma_mem: [bv64]bool;
+var {:extern} R0: bv64;
+var {:extern} mem: [bv64]bv8;
+const {:extern} $_IO_stdin_used_addr: bv64;
+axiom ($_IO_stdin_used_addr == 1840bv64);
+function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:extern} memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+procedure {:extern} rely();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+  free ensures (memory_load8_le(mem, 1840bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1841bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1842bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1843bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+procedure {:extern} rely_transitive();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+
+implementation {:extern} rely_transitive()
+{
+  call rely();
+  call rely();
+}
+
+procedure {:extern} rely_reflexive();
+
+procedure {:extern} guarantee_reflexive();
+  modifies Gamma_mem, mem;
+
+procedure main();
+  modifies Gamma_R0, R0;
+  free requires (memory_load64_le(mem, 69664bv64) == 0bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free requires (memory_load8_le(mem, 1840bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1841bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1842bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1843bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free requires (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free requires (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free ensures (memory_load8_le(mem, 1840bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1841bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1842bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1843bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+implementation main()
+{
+  main_basil_entry:
+    assume {:captureState "main_basil_entry"} true;
+    goto lmain;
+  lmain:
+    assume {:captureState "lmain"} true;
+    R0, Gamma_R0 := 0bv64, true;
+    goto main_basil_return;
+  main_basil_return:
+    assume {:captureState "main_basil_return"} true;
+    return;
+}
+
diff --git a/src/test/correct/arrays_simple/clang_O2/arrays_simple_gtirb.expected b/src/test/correct/arrays_simple/clang_O2/arrays_simple_gtirb.expected
@@ -0,0 +1,79 @@
+var {:extern} Gamma_R0: bool;
+var {:extern} Gamma_mem: [bv64]bool;
+var {:extern} R0: bv64;
+var {:extern} mem: [bv64]bv8;
+const {:extern} $_IO_stdin_used_addr: bv64;
+axiom ($_IO_stdin_used_addr == 1840bv64);
+function {:extern} {:bvbuiltin "bvadd"} bvadd64(bv64, bv64) returns (bv64);
+function {:extern} memory_load64_le(memory: [bv64]bv8, index: bv64) returns (bv64) {
+  (memory[bvadd64(index, 7bv64)] ++ (memory[bvadd64(index, 6bv64)] ++ (memory[bvadd64(index, 5bv64)] ++ (memory[bvadd64(index, 4bv64)] ++ (memory[bvadd64(index, 3bv64)] ++ (memory[bvadd64(index, 2bv64)] ++ (memory[bvadd64(index, 1bv64)] ++ memory[index])))))))
+}
+
+function {:extern} memory_load8_le(memory: [bv64]bv8, index: bv64) returns (bv8) {
+  memory[index]
+}
+
+procedure {:extern} rely();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+  free ensures (memory_load8_le(mem, 1840bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1841bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1842bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1843bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+procedure {:extern} rely_transitive();
+  modifies Gamma_mem, mem;
+  ensures (mem == old(mem));
+  ensures (Gamma_mem == old(Gamma_mem));
+
+implementation {:extern} rely_transitive()
+{
+  call rely();
+  call rely();
+}
+
+procedure {:extern} rely_reflexive();
+
+procedure {:extern} guarantee_reflexive();
+  modifies Gamma_mem, mem;
+
+procedure main();
+  modifies Gamma_R0, R0;
+  free requires (memory_load64_le(mem, 69664bv64) == 0bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free requires (memory_load8_le(mem, 1840bv64) == 1bv8);
+  free requires (memory_load8_le(mem, 1841bv64) == 0bv8);
+  free requires (memory_load8_le(mem, 1842bv64) == 2bv8);
+  free requires (memory_load8_le(mem, 1843bv64) == 0bv8);
+  free requires (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free requires (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free requires (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free requires (memory_load64_le(mem, 69672bv64) == 69672bv64);
+  free ensures (memory_load8_le(mem, 1840bv64) == 1bv8);
+  free ensures (memory_load8_le(mem, 1841bv64) == 0bv8);
+  free ensures (memory_load8_le(mem, 1842bv64) == 2bv8);
+  free ensures (memory_load8_le(mem, 1843bv64) == 0bv8);
+  free ensures (memory_load64_le(mem, 69064bv64) == 1808bv64);
+  free ensures (memory_load64_le(mem, 69072bv64) == 1728bv64);
+  free ensures (memory_load64_le(mem, 69592bv64) == 1812bv64);
+  free ensures (memory_load64_le(mem, 69672bv64) == 69672bv64);
+
+implementation main()
+{
+  main_basil_entry:
+    assume {:captureState "main_basil_entry"} true;
+    goto $main$__0__$p4DIz51ISauZoyb4V6rBoA;
+  $main$__0__$p4DIz51ISauZoyb4V6rBoA:
+    assume {:captureState "$main$__0__$p4DIz51ISauZoyb4V6rBoA"} true;
+    R0, Gamma_R0 := 0bv64, true;
+    goto main_basil_return;
+  main_basil_return:
+    assume {:captureState "main_basil_return"} true;
+    return;
+}
+