Support up to LLVM 14

This adds support for LLVM versions up to 14 by: * Bumping the `llvm-pretty` submodule to bring in the changes from GaloisInc/llvm-pretty#109. * Bumping the `llvm-pretty-bc-parser` submodule to bring in the changes from GaloisInc/llvm-pretty-bc-parser#219. * Updating the test output in `crux-llvm` and `uc-crux-llvm`'s test suites accordingly.
GaloisInc · Apr 20, 2023 · 43a6767 · 43a6767
1 parent 221e1c1
commit 43a6767
Show file tree

Hide file tree

Showing 10 changed files with 31 additions and 9 deletions.
diff --git a/crux-llvm/README.md b/crux-llvm/README.md
@@ -46,7 +46,7 @@ We have tested `crux-llvm` most heavily with GHC 8.10.7, GHC 9.2.7, GHC 9.4.4,
 and `cabal` version 3.8.1.0. We recommend Yices 2.6.x, and Z3
 4.8.x. Technically, only one of Yices or Z3 is required, and CVC4 is
 also supported. However, in practice, having both tends to be
-convenient. Finally, LLVM versions from 3.6 through 11 are likely to
+convenient. Finally, LLVM versions from 3.6 through 14 are likely to
 work well, and any failures with versions in that range should be
 [reported as bugs](https://github.com/GaloisInc/crucible/issues).
 

diff --git a/crux-llvm/test-data/golden/T972-fail.pre-clang14.z3.good b/crux-llvm/test-data/golden/T972-fail.pre-clang14.z3.good
@@ -0,0 +1,4 @@
+[Crux] Found counterexample for verification goal
+[Crux]   test-data/golden/T972-fail.c:8:3: error: in main
+[Crux]   unsupported LLVM value: ValAsm True False "testl $0, $0; jne ${1:l};" "r,X,X,~{dirflag},~{fpsr},~{flags}" of type void(i32, i8*, i8*)*
+[Crux] Overall status: Invalid.
diff --git a/crux-llvm/test-data/golden/T972-fail.z3.good b/crux-llvm/test-data/golden/T972-fail.z3.good
@@ -1,4 +1,4 @@
 [Crux] Found counterexample for verification goal
 [Crux]   test-data/golden/T972-fail.c:8:3: error: in main
-[Crux]   unsupported LLVM value: ValAsm True False "testl $0, $0; jne ${1:l};" "r,X,X,~{dirflag},~{fpsr},~{flags}" of type void(i32, i8*, i8*)*
+[Crux]   unsupported LLVM value: ValAsm True False "testl $0, $0; jne ${1:l};" "r,i,i,~{dirflag},~{fpsr},~{flags}" of type void(i32, i8*, i8*)*
 [Crux] Overall status: Invalid.
diff --git a/crux-llvm/test-data/golden/abd-test-file-32.cvc5.good b/crux-llvm/test-data/golden/abd-test-file-32.cvc5.good
@@ -3,7 +3,7 @@
 [Crux]   crucible_assert
 [Crux] 
 [Crux]   One of the following 3 fact(s) would entail the goal
-[Crux]   * (bvult x #b00000000000000000000000000000001)
-[Crux]   * (bvult #b00000000000000000000000001100100 x)
-[Crux]   * (= #b00000000000000000000000000000001 x)
+[Crux]   * (= x #b00000000000000000000000000000001)
+[Crux]   * (= x #b00000000000000000000000000000000)
+[Crux]   * (bvult x #b00000000000000000000000001100011)
 [Crux] Overall status: Invalid.
diff --git a/crux-llvm/test-data/golden/abd-test-file-32.pre-clang13.cvc5.good b/crux-llvm/test-data/golden/abd-test-file-32.pre-clang13.cvc5.good
@@ -0,0 +1,9 @@
+[Crux] Found counterexample for verification goal
+[Crux]   test-data/golden/abd-test-file-32.c:11:0: error: in main
+[Crux]   crucible_assert
+[Crux] 
+[Crux]   One of the following 3 fact(s) would entail the goal
+[Crux]   * (bvult x #b00000000000000000000000000000001)
+[Crux]   * (bvult #b00000000000000000000000001100100 x)
+[Crux]   * (= #b00000000000000000000000000000001 x)
+[Crux] Overall status: Invalid.
diff --git a/crux-llvm/test/Test.hs b/crux-llvm/test/Test.hs
@@ -43,6 +43,8 @@ cube = TS.mkCUBE { TS.inputDirs = ["test-data/golden"]
                                     , ("clang-range", Just [ "recent-clang"
                                                            , "pre-clang11"
                                                            , "pre-clang12"
+                                                           , "pre-clang13"
+                                                           , "pre-clang14"
                                                            ])
                                     ]
                  , TS.associatedNames = [ ("config",      "config")

diff --git a/dependencies/llvm-pretty b/dependencies/llvm-pretty
diff --git a/dependencies/llvm-pretty-bc-parser b/dependencies/llvm-pretty-bc-parser
diff --git a/uc-crux-llvm/README.md b/uc-crux-llvm/README.md
@@ -129,7 +129,7 @@ Before running `uc-crux-llvm`, you'll need to install the following software:
 
 We recommend Yices 2.6.x, and Z3 4.8.x. Technically, only one of Yices or Z3 is
 required, and CVC4 will work, as well. However, in practice, having both tends
-to be convenient. Finally, LLVM versions from 3.6 through 10 are likely to work
+to be convenient. Finally, LLVM versions from 3.6 through 14 are likely to work
 well, and any failures with versions in that range should be considered
 [bugs](https://github.com/GaloisInc/crucible/issues).
 

diff --git a/uc-crux-llvm/test/programs/read_global_neg_offset_strlen.c b/uc-crux-llvm/test/programs/read_global_neg_offset_strlen.c
@@ -1,5 +1,12 @@
 #include <string.h>
 char str[] = "str";
+// We mark this function as noinline to ensure that LLVM 14+ does not
+// over-optimize the call site in read_global_neg_offset_strlen and produce a
+// getelementptr expression with an out-of-bounds index. This would cause
+// crucible-llvm to abort before it has a chance to report the undefined
+// behavior in subtracting 1 from a global pointer, which is the ultimate goal
+// of this test case.
+char *minus_1(char *ptr) __attribute__((noinline)) { return ptr - 1; }
 int read_global_neg_offset_strlen() {
-  return strlen(str - 1);
+  return strlen(minus_1(str));
 }
+2 −1		.github/workflows/llvm-quick-fuzz.yml
+5 −1		README.md
+1 −0		disasm-test/Main.hs
+10 −0		disasm-test/tests/btf-tag-dicompositetype.at-least-llvm14.ll
+10 −0		disasm-test/tests/btf-tag-diderivedtype.at-least-llvm14.ll
+15 −0		disasm-test/tests/btf-tag-diglobalvariable.at-least-llvm14.ll
+14 −0		disasm-test/tests/btf-tag-dilocalvariable.at-least-llvm14.ll
+15 −0		disasm-test/tests/btf-tag-disubprogram.at-least-llvm14.ll
+4 −0		disasm-test/tests/diderivedtype-address-space.at-least-llvm14.ll
+32 −0		disasm-test/tests/dilocalvariable.at-least-llvm14.ll
+1 −1		llvm-pretty
+31 −10		src/Data/LLVM/BitCode/IR/Metadata.hs