diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,8 @@ +# 0.9 -- 2024-08-30 + +* Add support for GHC 9.8 +* The type signatures in `Crux.LLVM.Overrides` now use fewer type parameters in the `OverrideTemplates` that they return, in accordance with downstream changes from `crucible-llvm`. + # 0.8 -- 2024-02-05 * Add support for LLVM bitcode files generated by Apple Clang on macOS. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -42,8 +42,8 @@ * `echo 'export PATH="/usr/local/opt/llvm/bin:$PATH"' >> ~/.bash_profile` * run `crux-llvm` in a new console to reload `.bash_profile` -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 +We have tested `crux-llvm` most heavily with GHC 9.4, GHC 9.6, GHC 9.8, +and `cabal` version 3.10. 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 16 are likely to diff --git a/crux-llvm.cabal b/crux-llvm.cabal --- a/crux-llvm.cabal +++ b/crux-llvm.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: crux-llvm -Version: 0.8 +Version: 0.9 Author: Galois Inc. Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com Copyright: (c) Galois, Inc 2014-2022 @@ -55,7 +55,7 @@ -Wincomplete-uni-patterns ghc-prof-options: -O2 default-language: Haskell2010 - build-depends: base >= 4.8 && < 4.19 + build-depends: base >= 4.8 && < 4.20 , bytestring , containers , crucible diff --git a/src/Crux/LLVM/Compile.hs b/src/Crux/LLVM/Compile.hs --- a/src/Crux/LLVM/Compile.hs +++ b/src/Crux/LLVM/Compile.hs @@ -30,6 +30,7 @@ import What4.Interface import What4.ProgramLoc +import Lang.Crucible.Panic ( panic ) import Lang.Crucible.Simulator.SimError import Crux @@ -124,13 +125,20 @@ Log.SupportsCruxLLVMLogMessage msgs => CruxOptions -> LLVMOptions -> IO FilePath genBitCode cruxOpts llvmOpts = - -- n.b. use of head here is OK because inputFiles should not be - -- empty (and was previously verified as such in CruxLLVMMain). if noCompile llvmOpts - then return (head (Crux.inputFiles cruxOpts)) + then return headInputFile else do - let ofn = "crux~" <> (takeFileName $ head $ Crux.inputFiles cruxOpts) -<.> ".bc" + let ofn = "crux~" <> takeFileName headInputFile -<.> ".bc" genBitCodeToFile ofn (Crux.inputFiles cruxOpts) cruxOpts llvmOpts False + where + -- n.b. the use of partiality here is OK because inputFiles should not be + -- empty (and was previously verified as such in CruxLLVMMain). + headInputFile = + case Crux.inputFiles cruxOpts of + inputFile:_ -> inputFile + [] -> panic + "genBitCode" + ["Unexpected empty list of files"] -- | Given the target filename and a list of input files, along with -- the crux and llvm options, bitcode-compile each input .c file and diff --git a/src/Crux/LLVM/Config.hs b/src/Crux/LLVM/Config.hs --- a/src/Crux/LLVM/Config.hs +++ b/src/Crux/LLVM/Config.hs @@ -208,6 +208,9 @@ , "'unstable-symbolic', which causes each read from uninitialized" , "memory to return a fresh symbolic value." ]) + noSatisfyingWriteFreshConstant <- + Crux.section "no-satisfying-write-fresh-constant" Crux.yesOrNoSpec True + "Make a fresh constant for the NoSatisfyingWrite annotation." return MemOptions{..} transOpts <- do laxArith <- diff --git a/src/Crux/LLVM/Overrides.hs b/src/Crux/LLVM/Overrides.hs --- a/src/Crux/LLVM/Overrides.hs +++ b/src/Crux/LLVM/Overrides.hs @@ -34,7 +34,7 @@ import What4.ProgramLoc( Position(..), ProgramLoc(..) ) import What4.Symbol(userSymbol, emptySymbol, safeSymbol) import What4.Interface - (freshConstant, bvLit, bvAdd, asBV, predToBV, + (freshConstant, bvLit, bvOne, bvAdd, asBV, predToBV, getCurrentProgramLoc, printSymExpr, arrayUpdate, bvIsNonzero) import Lang.Crucible.Types @@ -43,13 +43,14 @@ import Lang.Crucible.Simulator.ExecutionTree( printHandle ) import Lang.Crucible.Simulator.OverrideSim ( getContext + , getSymInterface , readGlobal , writeGlobal , ovrWithBackend ) import Lang.Crucible.Simulator.SimError (SimErrorReason(..),SimError(..)) import Lang.Crucible.Backend - ( IsSymInterface, IsSymBackend, addDurableAssertion + ( IsSymInterface, addDurableAssertion , addAssumption, LabeledPred(..), CrucibleAssumption(..) , backendGetSym ) @@ -82,7 +83,7 @@ ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) => Proxy# arch -> - [OverrideTemplate (personality sym) sym arch rtp l a] + [OverrideTemplate (personality sym) sym ext arch] cruxLLVMOverrides arch = [ basic_llvm_override $ [llvmOvr| i8 @crucible_int8_t( i8* ) |] @@ -146,7 +147,7 @@ , basic_llvm_override $ [llvmOvr| void @crucible_dump_memory( ) |] - (\mvar _sym _args -> + (\mvar _args -> do mem <- readGlobal mvar h <- printHandle <$> getContext liftIO (doDumpMem h mem)) @@ -157,7 +158,7 @@ ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) => Proxy# arch -> - [OverrideTemplate (personality sym) sym arch rtp l a] + [OverrideTemplate (personality sym) sym ext arch] cbmcOverrides arch = [ basic_llvm_override $ [llvmOvr| void @__CPROVER_assume( i32 ) |] @@ -259,7 +260,7 @@ svCompOverrides :: (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => - [OverrideTemplate (personality sym) sym arch rtp l a] + [OverrideTemplate (personality sym) sym ext arch] svCompOverrides = [ basic_llvm_override $ [llvmOvr| i64 @__VERIFIER_nondet_longlong() |] @@ -363,208 +364,200 @@ return (BS8.unpack (BS.pack bytes)) sv_comp_fresh_bits :: - (IsSymBackend sym bak, 1 <= w) => + (IsSymInterface sym, 1 <= w) => NatRepr w -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) EmptyCtx -> OverM personality sym ext (RegValue sym (BVType w)) -sv_comp_fresh_bits w _mvar _bak Empty = Crux.mkFresh (safeSymbol "X") (BaseBVRepr w) +sv_comp_fresh_bits w _mvar Empty = Crux.mkFresh (safeSymbol "X") (BaseBVRepr w) sv_comp_fresh_float :: - (IsSymBackend sym bak) => + IsSymInterface sym => FloatInfoRepr fi -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) EmptyCtx -> OverM personality sym ext (RegValue sym (FloatType fi)) -sv_comp_fresh_float fi _mvar _bak Empty = Crux.mkFreshFloat (safeSymbol "X") fi +sv_comp_fresh_float fi _mvar Empty = Crux.mkFreshFloat (safeSymbol "X") fi fresh_bits :: - ( ArchOk arch, HasLLVMAnn sym, IsSymBackend sym bak, 1 <= w + ( ArchOk arch, IsSymInterface sym, HasLLVMAnn sym, 1 <= w , ?memOpts :: MemOptions ) => Proxy# arch -> NatRepr w -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch) -> OverM personality sym ext (RegValue sym (BVType w)) -fresh_bits arch w mvar _ (Empty :> pName) = +fresh_bits arch w mvar (Empty :> pName) = do name <- lookupString arch mvar pName Crux.mkFresh (safeSymbol name) (BaseBVRepr w) fresh_float :: - ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym + ( ArchOk arch, IsSymInterface sym, HasLLVMAnn sym , ?memOpts :: MemOptions ) => Proxy# arch -> FloatInfoRepr fi -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch) -> OverM personality sym ext (RegValue sym (FloatType fi)) -fresh_float arch fi mvar _ (Empty :> pName) = +fresh_float arch fi mvar (Empty :> pName) = do name <- lookupString arch mvar pName Crux.mkFreshFloat (safeSymbol name) fi fresh_str :: - ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym + ( ArchOk arch, HasLLVMAnn sym , ?memOpts :: MemOptions ) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> BVType (ArchWidth arch)) -> OverM personality sym ext (RegValue sym (TPtr arch)) -fresh_str arch mvar bak (Empty :> pName :> maxLen) = - do let sym = backendGetSym bak - name <- lookupString arch mvar pName +fresh_str arch mvar (Empty :> pName :> maxLen) = + ovrWithBackend $ \bak -> do + let sym = backendGetSym bak + name <- lookupString arch mvar pName - -- Compute the allocation length, which is the requested length plus one - -- to hold the NUL terminator - one <- liftIO $ bvLit sym ?ptrWidth (BV.one ?ptrWidth) - -- maxLenBV <- liftIO $ projectLLVM_bv sym (regValue maxLen) - len <- liftIO $ bvAdd sym (regValue maxLen) one - mem0 <- readGlobal mvar + -- Compute the allocation length, which is the requested length plus one + -- to hold the NUL terminator + one <- liftIO $ bvOne sym ?ptrWidth + -- maxLenBV <- liftIO $ projectLLVM_bv sym (regValue maxLen) + len <- liftIO $ bvAdd sym (regValue maxLen) one + mem0 <- readGlobal mvar - -- Allocate memory to hold the string - (ptr, mem1) <- liftIO $ doMalloc bak HeapAlloc Mutable name mem0 len noAlignment + -- Allocate memory to hold the string + (ptr, mem1) <- liftIO $ doMalloc bak HeapAlloc Mutable name mem0 len noAlignment - -- Allocate contents for the string - we want to make each byte symbolic, - -- so we allocate a fresh array (which has unbounded length) with symbolic - -- contents and write it into our allocation. This write does not cover - -- the NUL terminator. - contentsName <- case userSymbol (name ++ "_contents") of - Left err -> fail (show err) - Right nm -> return nm - let arrayRep = BaseArrayRepr (Empty :> BaseBVRepr ?ptrWidth) (BaseBVRepr (knownNat @8)) - initContents <- liftIO $ freshConstant sym contentsName arrayRep - zeroByte <- liftIO $ bvLit sym (knownNat @8) (BV.zero knownNat) - -- Put the NUL terminator in place - initContentsZ <- liftIO $ arrayUpdate sym initContents (singleton (regValue maxLen)) zeroByte - mem2 <- liftIO $ doArrayConstStore bak mem1 ptr noAlignment initContentsZ len + -- Allocate contents for the string - we want to make each byte symbolic, + -- so we allocate a fresh array (which has unbounded length) with symbolic + -- contents and write it into our allocation. This write does not cover + -- the NUL terminator. + contentsName <- case userSymbol (name ++ "_contents") of + Left err -> fail (show err) + Right nm -> return nm + let arrayRep = BaseArrayRepr (Empty :> BaseBVRepr ?ptrWidth) (BaseBVRepr (knownNat @8)) + initContents <- liftIO $ freshConstant sym contentsName arrayRep + zeroByte <- liftIO $ bvLit sym (knownNat @8) (BV.zero knownNat) + -- Put the NUL terminator in place + initContentsZ <- liftIO $ arrayUpdate sym initContents (singleton (regValue maxLen)) zeroByte + mem2 <- liftIO $ doArrayConstStore bak mem1 ptr noAlignment initContentsZ len - writeGlobal mvar mem2 - return ptr + writeGlobal mvar mem2 + return ptr do_assume :: - ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym + ( ArchOk arch, HasLLVMAnn sym , ?memOpts :: MemOptions ) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TBits 8 ::> TPtr arch ::> TBits 32) -> OverM personality sym ext (RegValue sym UnitType) -do_assume arch mvar bak (Empty :> p :> pFile :> line) = - do let sym = backendGetSym bak - cond <- liftIO $ bvIsNonzero sym (regValue p) - file <- lookupString arch mvar pFile - l <- case asBV (regValue line) of - Just (BV.BV l) -> return (fromInteger l) - Nothing -> return 0 - let pos = SourcePos (T.pack file) l 0 - loc <- liftIO $ getCurrentProgramLoc sym - let loc' = loc{ plSourceLoc = pos } - liftIO $ addAssumption bak (GenericAssumption loc' "crucible_assume" cond) +do_assume arch mvar (Empty :> p :> pFile :> line) = + ovrWithBackend $ \bak -> do + let sym = backendGetSym bak + cond <- liftIO $ bvIsNonzero sym (regValue p) + file <- lookupString arch mvar pFile + l <- case asBV (regValue line) of + Just (BV.BV l) -> return (fromInteger l) + Nothing -> return 0 + let pos = SourcePos (T.pack file) l 0 + loc <- liftIO $ getCurrentProgramLoc sym + let loc' = loc{ plSourceLoc = pos } + liftIO $ addAssumption bak (GenericAssumption loc' "crucible_assume" cond) do_assert :: - ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym + ( ArchOk arch, HasLLVMAnn sym , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TBits 8 ::> TPtr arch ::> TBits 32) -> OverM personality sym ext (RegValue sym UnitType) -do_assert arch mvar bak (Empty :> p :> pFile :> line) = +do_assert arch mvar (Empty :> p :> pFile :> line) = when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $ - do let sym = backendGetSym bak - cond <- liftIO $ bvIsNonzero sym (regValue p) - file <- lookupString arch mvar pFile - l <- case asBV (regValue line) of - Just (BV.BV l) -> return (fromInteger l) - Nothing -> return 0 - let pos = SourcePos (T.pack file) l 0 - loc <- liftIO $ getCurrentProgramLoc sym - let loc' = loc{ plSourceLoc = pos } - let msg = GenericSimError "crucible_assert" - liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc' msg)) + ovrWithBackend $ \bak -> do + let sym = backendGetSym bak + cond <- liftIO $ bvIsNonzero sym (regValue p) + file <- lookupString arch mvar pFile + l <- case asBV (regValue line) of + Just (BV.BV l) -> return (fromInteger l) + Nothing -> return 0 + let pos = SourcePos (T.pack file) l 0 + loc <- liftIO $ getCurrentProgramLoc sym + let loc' = loc{ plSourceLoc = pos } + let msg = GenericSimError "crucible_assert" + liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc' msg)) -do_print_uint32 :: - (IsSymBackend sym bak) => +do_print_uint32 :: + IsSymInterface sym => GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TBits 32) -> OverM personality sym ext (RegValue sym UnitType) -do_print_uint32 _mvar _bak (Empty :> x) = +do_print_uint32 _mvar (Empty :> x) = do h <- printHandle <$> getContext liftIO $ hPutStrLn h (show (printSymExpr (regValue x))) do_havoc_memory :: - (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) => + (ArchOk arch, IsSymInterface sym, HasLLVMAnn sym) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> TBits (ArchWidth arch)) -> OverM personality sym ext (RegValue sym UnitType) -do_havoc_memory _ mvar bak (Empty :> ptr :> len) = - do let sym = backendGetSym bak - let tp = BaseArrayRepr (Empty :> BaseBVRepr ?ptrWidth) (BaseBVRepr (knownNat @8)) - mem <- readGlobal mvar - mem' <- liftIO $ do - arr <- freshConstant sym emptySymbol tp - doArrayStore bak mem (regValue ptr) noAlignment arr (regValue len) - writeGlobal mvar mem' +do_havoc_memory _ mvar (Empty :> ptr :> len) = + ovrWithBackend $ \bak -> + do let sym = backendGetSym bak + let tp = BaseArrayRepr (Empty :> BaseBVRepr ?ptrWidth) (BaseBVRepr (knownNat @8)) + mem <- readGlobal mvar + mem' <- liftIO $ do + arr <- freshConstant sym emptySymbol tp + doArrayStore bak mem (regValue ptr) noAlignment arr (regValue len) + writeGlobal mvar mem' cprover_assume :: - (IsSymBackend sym bak) => GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TBits 32) -> OverM personality sym ext (RegValue sym UnitType) -cprover_assume _mvar bak (Empty :> p) = liftIO $ - do let sym = backendGetSym bak - cond <- bvIsNonzero sym (regValue p) - loc <- getCurrentProgramLoc sym - addAssumption bak (GenericAssumption loc "__CPROVER_assume" cond) +cprover_assume _mvar (Empty :> p) = + ovrWithBackend $ \bak -> liftIO $ do + let sym = backendGetSym bak + cond <- bvIsNonzero sym (regValue p) + loc <- getCurrentProgramLoc sym + addAssumption bak (GenericAssumption loc "__CPROVER_assume" cond) cprover_assert :: - ( ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym + ( ArchOk arch, HasLLVMAnn sym , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TBits 32 ::> TPtr arch) -> OverM personality sym ext (RegValue sym UnitType) -cprover_assert arch mvar bak (Empty :> p :> pMsg) = +cprover_assert arch mvar (Empty :> p :> pMsg) = when (abnormalExitBehavior ?intrinsicsOpts == AlwaysFail) $ - do let sym = backendGetSym bak - cond <- liftIO $ bvIsNonzero sym (regValue p) - str <- lookupString arch mvar pMsg - loc <- liftIO $ getCurrentProgramLoc sym - let msg = AssertFailureSimError "__CPROVER_assert" str - liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc msg)) + ovrWithBackend $ \bak -> + do let sym = backendGetSym bak + cond <- liftIO $ bvIsNonzero sym (regValue p) + str <- lookupString arch mvar pMsg + loc <- liftIO $ getCurrentProgramLoc sym + let msg = AssertFailureSimError "__CPROVER_assert" str + liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc msg)) cprover_r_ok :: - (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) => + (ArchOk arch, IsSymInterface sym, HasLLVMAnn sym) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> BVType (ArchWidth arch)) -> OverM personality sym ext (RegValue sym (BVType 1)) -cprover_r_ok _ mvar bak (Empty :> (regValue -> p) :> (regValue -> sz)) = - do let sym = backendGetSym bak +cprover_r_ok _ mvar (Empty :> (regValue -> p) :> (regValue -> sz)) = + do sym <- getSymInterface mem <- readGlobal mvar x <- liftIO $ isAllocatedAlignedPointer sym PtrWidth noAlignment Immutable p (Just sz) mem liftIO $ predToBV sym x knownNat cprover_w_ok :: - (ArchOk arch, IsSymBackend sym bak, HasLLVMAnn sym) => + (ArchOk arch, IsSymInterface sym, HasLLVMAnn sym) => Proxy# arch -> GlobalVar Mem -> - bak -> Assignment (RegEntry sym) (EmptyCtx ::> TPtr arch ::> BVType (ArchWidth arch)) -> OverM personality sym ext (RegValue sym (BVType 1)) -cprover_w_ok _ mvar bak (Empty :> (regValue -> p) :> (regValue -> sz)) = - do let sym = backendGetSym bak +cprover_w_ok _ mvar (Empty :> (regValue -> p) :> (regValue -> sz)) = + do sym <- getSymInterface mem <- readGlobal mvar x <- liftIO $ isAllocatedAlignedPointer sym PtrWidth noAlignment Mutable p (Just sz) mem liftIO $ predToBV sym x knownNat diff --git a/src/Crux/LLVM/Simulate.hs b/src/Crux/LLVM/Simulate.hs --- a/src/Crux/LLVM/Simulate.hs +++ b/src/Crux/LLVM/Simulate.hs @@ -13,7 +13,6 @@ module Crux.LLVM.Simulate where -import qualified Data.BitVector.Sized as BV import Data.String (fromString) import qualified Data.Map.Strict as Map import Data.IORef @@ -37,7 +36,7 @@ -- what4 import qualified What4.Expr.Builder as WEB -import What4.Interface (bvLit, natLit) +import What4.Interface (bvLit, bvZero) -- crucible import Lang.Crucible.Backend @@ -66,8 +65,8 @@ ( Mem, MemImpl, mkMemVar, withPtrWidth, memAllocCount, memWriteCount , MemOptions(..), HasLLVMAnn, LLVMAnnMap , explainCex, CexExplanation(..), doAlloca - , pattern LLVMPointer, pattern LLVMPointerRepr, LLVMPointerType - , pattern PtrRepr, pattern PtrWidth + , pattern LLVMPointerRepr, LLVMPointerType + , pattern PtrRepr, pattern PtrWidth, llvmPointer_bv ) import Lang.Crucible.LLVM.MemModel.CallStack (ppCallStack) import Lang.Crucible.LLVM.MemType (MemType(..), SymType(..), i8, memTypeAlign, memTypeSize) @@ -140,13 +139,13 @@ ?memOpts = memOpts llvmOpts -- register the callable override functions - register_llvm_overrides llvm_module [] - (concat [ cruxLLVMOverrides proxy# - , svCompOverrides - , cbmcOverrides proxy# - , maybe [] symio_overrides fs0 - ]) - llvm_ctx + _ <- register_llvm_overrides llvm_module [] + (concat [ cruxLLVMOverrides proxy# + , svCompOverrides + , cbmcOverrides proxy# + , maybe [] symio_overrides fs0 + ]) + llvm_ctx -- register all the functions defined in the LLVM module registerLazyModule sayTranslationWarning mtrans @@ -339,7 +338,7 @@ mem <- case lookupGlobal memVar gs of Just mem -> pure mem Nothing -> fail "checkFun.checkMainWithArguments: Memory missing from global vars" - argc <- liftIO $ LLVMPointer <$> natLit sym 0 <*> bvLit sym w (BV.zero w) + argc <- liftIO $ llvmPointer_bv sym =<< bvZero sym w sz <- liftIO $ bvLit sym PtrWidth $ bytesToBV PtrWidth tp_sz (argv, mem') <- liftIO $ doAlloca bak mem sz alignment loc stateTree.actFrame.gpGlobals %= insertGlobal memVar mem' diff --git a/test/Test.hs b/test/Test.hs --- a/test/Test.hs +++ b/test/Test.hs @@ -12,7 +12,7 @@ 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 ) +import Data.List.Extra ( isInfixOf ) import Data.Maybe ( catMaybes, fromMaybe ) import qualified Data.Text as T import Data.Versions ( Versioning, versioning, prettyV, major ) @@ -21,6 +21,7 @@ import System.Environment ( withArgs, lookupEnv ) import System.Exit ( ExitCode(..) ) import System.FilePath ( (-<.>) ) +import qualified System.Info as Info import System.IO import System.Process ( readProcess ) import Text.Read ( readMaybe ) @@ -31,6 +32,8 @@ import Test.Tasty.HUnit ( testCase, assertFailure ) import qualified Test.Tasty.Sugar as TS +import qualified Lang.Crucible.Panic as P + import qualified CruxLLVMMain as C @@ -42,6 +45,7 @@ , TS.validParams = [ ("solver", Just ["z3", "cvc5"]) , ("loop-merging", Just ["loopmerge", "loop"]) , ("clang-range", Just [ "recent-clang" + , "pre-clang9" , "pre-clang11" , "pre-clang12" , "pre-clang13" @@ -101,7 +105,7 @@ getClangVersion = do -- Determine which version of clang will be used for these tests. -- An exception (E.g. in the readProcess if clang is not found) will - -- result in termination (test failure). Uses partial 'head' but + -- result in termination (test failure). Uses partiality, but -- this is just tests, and failure is captured. clangBin <- fromMaybe "clang" <$> lookupEnv "CLANG" let isVerLine = isInfixOf "clang version" @@ -110,10 +114,27 @@ -- 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 (/= '~') + + headVersionLine :: [String] -> String + headVersionLine ls = + case ls of + l:_ -> l + [] -> P.panic + "getClangVersion" + ["`clang --version` output does not contain line with version"] + + headVersionWord :: [String] -> String + headVersionWord ws = + case ws of + w:_ -> w + [] -> P.panic + "getClangVersion" + ["`clang --version` output does not contain numeric version"] + getVer (Right inp) = -- example inp: "clang version 10.0.1" - scrubProblemChars $ head $ dropLetter $ words $ - head $ filter isVerLine $ lines inp + scrubProblemChars $ headVersionWord $ dropLetter $ words $ + headVersionLine $ filter isVerLine $ lines inp getVer (Left full) = full mkVC "clang" . getVer <$> readProcessVersion clangBin @@ -121,9 +142,9 @@ getZ3Version = let getVer (Right inp) = -- example inp: "Z3 version 4.8.7 - 64 bit" - let w = words inp - in if and [ length w > 2, head w == "Z3" ] - then w !! 2 else "?" + case words inp of + "Z3":_:verNum:_ -> verNum + _ -> "?" getVer (Left full) = full in mkVC "z3" . getVer <$> readProcessVersion "z3" @@ -131,9 +152,9 @@ getYicesVersion = let getVer (Right inp) = -- example inp: "Yices 2.6.1\nCopyright ..." - let w = words inp - in if and [ length w > 1, head w == "Yices" ] - then w !! 1 else "?" + case words inp of + "Yices":verNum:_ -> verNum + _ -> "?" getVer (Left full) = full in mkVC "yices" . getVer <$> readProcessVersion "yices" @@ -141,11 +162,9 @@ getSTPVersion = let getVer (Right inp) = -- example inp: "STP version 2.3.3\n..." - let w = words inp - in if and [ length w > 2 - , head w == "STP" - , w !! 1 == "version" ] - then w !! 2 else "?" + case words inp of + "STP":"version":verNum:_ -> verNum + _ -> "?" getVer (Left full) = full in mkVC "stp" . getVer <$> readProcessVersion "stp" @@ -153,11 +172,9 @@ getCVC4Version = let getVer (Right inp) = -- example inp: "This is CVC4 version 1.8\ncompiled ..." - let w = words inp - in if and [ length w > 4 - , "This is CVC4 version" `isPrefixOf` inp - ] - then w !! 4 else "?" + case words inp of + "This":"is":"CVC4":"version":verNum:_ -> verNum + _ -> "?" getVer (Left full) = full in mkVC "cvc4" . getVer <$> readProcessVersion "cvc4" @@ -165,11 +182,9 @@ getCVC5Version = let getVer (Right inp) = -- example inp: "This is cvc5 version 1.0.2\ncompiled ..." - let w = words inp - in if and [ length w > 4 - , "This is cvc5 version" `isPrefixOf` inp - ] - then w !! 4 else "?" + case words inp of + "This":"is":"cvc5":"version":verNum:_ -> verNum + _ -> "?" getVer (Left full) = full in mkVC "cvc5" . getVer <$> readProcessVersion "cvc5" @@ -177,8 +192,9 @@ getBoolectorVersion = let getVer (Right inp) = -- example inp: "3.2.1" - let w = words inp - in if not (null w) then head w else "?" + case words inp of + verNum:_ -> verNum + [] -> "?" getVer (Left full) = full in mkVC "boolector" . getVer <$> readProcessVersion "boolector" @@ -375,13 +391,19 @@ , TS.rootBaseName sweet == "nested_unsafe" ] + -- T972-fail requires an x86-64 compiler, so skip it on non-x86-64 + -- architectures. + let skipX86_64Tests = + Info.arch /= "x86_64" && + TS.rootBaseName sweet == "T972-fail" + -- 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. skipTest <- ("SKIP_TEST" `BSIO.isPrefixOf`) <$> BSIO.readFile (TS.expectedFile expct) - if or [ skipTest, testLevel == "0" && longTests ] + if or [ skipTest, skipX86_64Tests, testLevel == "0" && longTests ] then do when (testLevel == "0" && longTests) $ putStrLn "*** Longer running test skipped; set CI_TEST_LEVEL=1 env var to enable"