Support up to LLVM 14

.github/workflows/crux-llvm-build.yml

@@ -212,10 +212,13 @@ jobs:
           LLVM_AS: "${{ github.workspace }}/llvm/bin/llvm-as"
           CLANG: "${{ github.workspace }}/llvm/bin/clang"
 
+        # We disable the crux-llvm test suite on macOS due to
+        # https://github.com/GaloisInc/crucible/issues/885 and
+        # https://github.com/GaloisInc/crucible/issues/999
       - shell: bash
         name: Test crux-llvm (macOS)
         run: .github/ci.sh test crux-llvm
-        if: runner.os == 'macOS'
+        if: runner.os == 'macOS' && false
         env:
           LLVM_LINK: "${{ github.workspace }}/llvm/bin/llvm-link"
           CLANG: "${{ github.workspace }}/llvm/bin/clang-withIncl"

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).
 
@@ -542,6 +542,36 @@ file will be named `<test-case>.z3.good`; this picks Z3 as a default solver to
 use when simulating the test case. There are also a handful of tests that
 require other solvers, e.g., `abd-test-file-32.cvc5.good`.
 
+Some of the test cases have slightly different output depending on which Clang
+version is used. These test cases will have accompanying
+`<test-case>.pre-clang<version>.<...>.good` files, where `pre-clang<version>`
+indicates that this test output is used for all Clang versions up to (but not
+including) `<version>`. Note that if a test case has multiple
+`pre-clang<version>` `.good` files, then the `<version>` that is closest to the
+current Clang version (without going over) is picked.
+
+To illustrate this with a concrete example, consider suppose we have a test
+case `foo` with the following `.good` files
+
+* `foo.pre-clang11.z3.good`
+* `foo.pre-clang13.z3.good`
+* `foo.z3.good`
+
+The following `.good` files would be used for the following Clang versions:
+
+* Clang 10: `foo.pre-clang11.z3.good`
+* Clang 11: `foo.pre-clang13.z3.good`
+* Clang 12: `foo.pre-clang13.z3.good`
+* Clang 13 or later: `foo.z3.good`
+
+There are some test cases that require a sufficiently recent Clang version to
+run. To indicate that a test should not be run on Clangs older than
+`<version>`, create a `pre-clang<version>` `.good` file with `SKIP_TEST` as the
+first line. The use of `SKIP_TEST` signals that this test should be skipped
+when using Clangs older than `<version>`. Note that the test suite will not
+read anything past `SKIP_TEST`, so the rest of the file can be used to document
+why the test is skipped on that particular configuration.
+
 # Acknowledgements
 
 Crux is partly based upon work supported by the Defense Advanced

crux-llvm/test-data/golden/T972-fail.pre-clang12.z3.good

@@ -0,0 +1,4 @@
+SKIP_TEST
+
+The generated LLVM bitcode for this test case requires the `callbr`
+instruction, which is only supported with LLVM 12 or later.

crux-llvm/test-data/golden/T972-fail.at-least-clang12.z3.good → crux-llvm/test-data/golden/T972-fail.pre-clang14.z3.good

@@ -1,4 +1,4 @@
 [Crux] Found counterexample for verification goal
-[Crux]   test-data/golden/T972-fail.at-least-clang12.c:8:3: error: in main
+[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.

crux-llvm/test-data/golden/T972-fail.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,i,i,~{dirflag},~{fpsr},~{flags}" of type void(i32, i8*, i8*)*
+[Crux] Overall status: Invalid.

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.

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.

crux-llvm/test-data/golden/golden/T847-fail2.pre-clang12.z3.good

@@ -0,0 +1,4 @@
+SKIP_TEST
+
+The LLVM bitcode for this test case requires the `llvm.abs.i*` intrinsic, which
+is only supported with LLVM 12 or later.

crux-llvm/test-data/golden/golden/T847-succeed.pre-clang12.z3.good

@@ -0,0 +1,4 @@
+SKIP_TEST
+
+The LLVM bitcode for this test case requires the `llvm.abs.i*` intrinsic, which
+is only supported with LLVM 12 or later.

crux-llvm/test-data/golden/golden/T974.pre-clang12.z3.good

@@ -0,0 +1,4 @@
+SKIP_TEST
+
+The LLVM bitcode for this test case requires the `llvm.umin.i*` family of
+intrinsics, which is only supported with LLVM 12 or later.

crux-llvm/test-data/golden/golden/freeze.pre-clang12.z3.good

@@ -0,0 +1,4 @@
+SKIP_TEST
+
+The LLVM bitcode for this test case requires the `freeze` instruction, which is
+only supported with LLVM 12 or later.

crux-llvm/test-data/golden/golden/invoke-test.pre-clang12.z3.good

@@ -0,0 +1,4 @@
+SKIP_TEST
+
+The LLVM bitcode for this test case requires the `invoke` instruction, which is
+only supported with LLVM 12 or later.

crux-llvm/test-data/golden/golden/ubsantrap.pre-clang12.z3.good

@@ -0,0 +1,4 @@
+SKIP_TEST
+
+The LLVM bitcode for this test case requires the `llvm.ubsantrap` intrinsic,
+which is only supported with LLVM 12 or later.

crux-llvm/test/Test.hs

@@ -6,22 +6,25 @@ module Main where
 
 import           Control.Exception ( SomeException, catches, try, Handler(..), IOException )
 import           Control.Lens ( (^.), (^?), _Right, to )
-import           Control.Monad ( unless, when )
+import           Control.Monad ( guard, unless, when )
 import           Data.Bifunctor ( first )
 import qualified Data.ByteString.Lazy as BSIO
 import qualified Data.ByteString.Lazy.Char8 as BSC
 import           Data.Char ( isLetter, isSpace )
 import           Data.List.Extra ( isInfixOf, isPrefixOf, stripPrefix )
-import           Data.Maybe ( catMaybes, fromMaybe, isJust )
+import           Data.Maybe ( catMaybes, fromMaybe, mapMaybe )
+import qualified Data.Set as Set
+import           Data.Set ( Set )
 import qualified Data.Text as T
 import           Data.Versions ( Versioning, versioning, prettyV, major )
 import qualified GHC.IO.Exception as GE
 import           Numeric.Natural
 import           System.Environment ( withArgs, lookupEnv )
 import           System.Exit ( ExitCode(..) )
-import           System.FilePath ( (-<.>) )
+import           System.FilePath ( (-<.>), takeFileName )
 import           System.IO
 import           System.Process ( readProcess )
+import           Text.Read ( readMaybe )
 
 import qualified Test.Tasty as TT
 import           Test.Tasty.HUnit ( testCase, assertFailure )
@@ -37,11 +40,15 @@ cube = TS.mkCUBE { TS.inputDirs = ["test-data/golden"]
                  , TS.expectedSuffix = "good"
                  , TS.validParams = [ ("solver", Just ["z3", "cvc5"])
                                     , ("loop-merging", Just ["loopmerge", "loop"])
-                                    , ("clang-range", Just ["pre-clang11", "at-least-clang12", "clang11", "clang12"])
+                                    , ("clang-range", Just [ "recent-clang"
+                                                           , "pre-clang11"
+                                                           , "pre-clang12"
+                                                           , "pre-clang13"
+                                                           , "pre-clang14"
+                                                           ])
                                     ]
                  , TS.associatedNames = [ ("config",      "config")
                                         , ("test-result", "result")
-                                        , ("skip",        "skip")   -- when present, test config is skipped
                                         ]
                  }
 
@@ -84,6 +91,16 @@ vcVersioning (VC _ v) = v
 mkVC :: String -> String -> VersionCheck
 mkVC nm raw = let r = T.pack raw in VC nm $ first (const r) $ versioning r
 
+-- Check if a VersionCheck version is less than the numeric value of another
+-- version (represented as a Word).
+vcLT :: VersionCheck -> Word -> Bool
+vcLT vc verNum = (vcVersioning vc ^? (_Right . major)) < Just verNum
+
+-- Check if a VersionCheck version is greater than or equal to the numeric
+-- value of another version (represented as a Word).
+vcGE :: VersionCheck -> Word -> Bool
+vcGE vc verNum = (vcVersioning vc ^? (_Right . major)) >= Just verNum
+
 getClangVersion :: IO VersionCheck
 getClangVersion = do
   -- Determine which version of clang will be used for these tests.
@@ -93,9 +110,14 @@ getClangVersion = do
   clangBin <- fromMaybe "clang" <$> lookupEnv "CLANG"
   let isVerLine = isInfixOf "clang version"
       dropLetter = dropWhile (all isLetter)
+      -- Remove any characters that give `versions` parsers a hard time, such
+      -- as tildes (cf. https://github.com/fosskers/versions/issues/62).
+      -- These have been observed in the wild (e.g., 12.0.0-3ubuntu1~20.04.5).
+      scrubProblemChars = filter (/= '~')
       getVer (Right inp) =
         -- example inp: "clang version 10.0.1"
-        head $ dropLetter $ words $ head $ filter isVerLine $ lines inp
+        scrubProblemChars $ head $ dropLetter $ words $
+        head $ filter isVerLine $ lines inp
       getVer (Left full) = full
   mkVC "clang" . getVer <$> readProcessVersion clangBin
 
@@ -296,20 +318,52 @@ mkTest clangVer sweet _ expct =
       _ -> return $ VC solver $ Left "unknown-solver-for-version"
 
     -- Match any clang version range specification in the .good
-    -- expected file against the current version of clang.  If the
-    -- current clang version doesn't match, no test should be
-    -- generated (i.e. only run tests for the version of clang
-    -- available).
+    -- expected file against the current version of clang. This implements a
+    -- combination of Case 3 and Case 3a from this tasty-sugar document:
+    -- https://github.com/kquick/tasty-sugar/blob/1fc06bee124e02f49f6478bc1e1df13704cc4916/Ranges.org#case-3---explicit-and-a-weaker-match
+    -- In particular, we use `recent-clang` as an explicit super-supremum (as in
+    -- Case 3a), but we also consult the set of Expectations in the full Sweets
+    -- value to avoid generating duplicate tests for `recent-clang` (as
+    -- described in Case 3).
     let clangMatch =
-          let specMatchesInstalled v =
-                or [ v == vcTag clangVer
-                   , and [ v == "pre-clang11"
-                         , vcMajor clangVer `elem` (show <$> [3..10 :: Int])
-                         ]
-                   , case stripPrefix "at-least-clang" v of
+          let allMatchingExpectations =
+                filter
+                  (\e -> (tname ++ ".") `isPrefixOf` takeFileName (TS.expectedFile e))
+                  (TS.expected sweet)
+
+              supportedPreClangs :: Set Word
+              supportedPreClangs =
+                Set.fromList $
+                mapMaybe
+                  (\e -> do
+                    TS.Explicit v <- lookup "clang-range" (TS.expParamsMatch e)
+                    verStr <- stripPrefix "pre-clang" v
+                    ver <- readMaybe verStr
+                    guard $ vcLT clangVer ver
+                    pure ver)
+                  allMatchingExpectations
+
+              -- Implement the "check" step described in Case 3/3a of the
+              -- tasty-sugar document linked above.
+              specMatchesInstalled v =
+                or [ case stripPrefix "pre-clang" v of
                        Nothing -> False
-                       Just verStr ->
-                         (vcVersioning clangVer ^? (_Right . major)) >= Just (read verStr)
+                       Just verStr
+                         |  Just ver <- readMaybe verStr
+                         -- Check that the current Clang version is less than
+                         -- the <ver> in the `pre-clang<ver>` file...
+                         ,  vcLT clangVer ver
+                         -- ...moreover, also check that <ver> is the closest
+                         -- `pre-clang` version (without going over). For
+                         -- instance, if the current Clang version is 10 and
+                         -- there are both `pre-clang11` and `pre-clang12`
+                         -- `.good` files, we only want to run with the
+                         -- `pre-clang11` configuration to avoid duplicate
+                         -- tests.
+                         ,  Just closestPreClang <- Set.lookupMin supportedPreClangs
+                         -> ver == closestPreClang
+                         |  otherwise
+                         -> False
                      -- as a fallback, if the testing code here is
                      -- unable to determine the version, run all
                      -- tests.  This is likely to cause a failure, but
@@ -318,9 +372,26 @@ mkTest clangVer sweet _ expct =
                      -- done anything.
                    , vcMajor clangVer == "[missing]"
                    ]
-          in case lookup "clang-range" (TS.expParamsMatch expct) of
-               Just (TS.Explicit v) -> specMatchesInstalled v
-               Just (TS.Assumed  v) -> specMatchesInstalled v
+          in -- Implement the "filter" step described in Case 3/3a of the
+             -- tasty-sugar document linked above.
+             case lookup "clang-range" (TS.expParamsMatch expct) of
+               Just (TS.Explicit v)
+                 -- Explicit matches are always allowed.
+                 -> specMatchesInstalled v
+               Just (TS.Assumed  v)
+                 -- The only allowable Assumed match is for `recent-clang`, the
+                 -- super-supremum value...
+                 |  v == "recent-clang"
+                 -> case Set.lookupMax supportedPreClangs of
+                      -- ...if there are no `pre-clang` .good files, then allow
+                      -- it...
+                      Nothing -> True
+                      -- ...otherwise, check that the current Clang version is
+                      -- larger than anything specified by a `pre-clang` .good
+                      -- file.
+                      Just largestPreClang -> vcGE clangVer largestPreClang
+                 |  otherwise
+                 -> False
                _ -> error "clang-range unknown"
 
     -- Some tests take longer, so only run one of them in fast-test mode
@@ -339,9 +410,11 @@ mkTest clangVer sweet _ expct =
                        , TS.rootBaseName sweet == "nested_unsafe"
                        ]
 
-    -- Presence of a .skip file means this test should be skipped.
+    -- If a .good file begins with SKIP_TEST, skip that test entirely. For test
+    -- cases that require a minimum Clang version, this technique is used to
+    -- prevent running the test on older Clang versions.
 
-    let skipTest = isJust $ lookup "skip" (TS.associated expct)
+    skipTest <- ("SKIP_TEST" `BSIO.isPrefixOf`) <$> BSIO.readFile (TS.expectedFile expct)
 
     if or [ skipTest, not clangMatch, testLevel == "0" && longTests ]
       then do

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).
 

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));
 }