crucible-llvm 0.7 → 0.7.1

raw patch · 7 files changed

+26/−10 lines, 7 filesdep ~crucibledep ~llvm-prettydep ~what4new-uploaderPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: crucible, llvm-pretty, what4

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• crucible-llvm.cabal +3/−3
• src/Lang/Crucible/LLVM/Intrinsics/Cast.hs +1/−1
• src/Lang/Crucible/LLVM/MemModel.hs +6/−0
• src/Lang/Crucible/LLVM/MemModel/Generic.hs +3/−2
• src/Lang/Crucible/LLVM/MemModel/Partial.hs +2/−2
• test/Tests.hs +6/−2

@@ -1,3 +1,8 @@+# 0.7.1 -- 2025-03-21++* Fix a bug in which the memory model would panic when attempting to unpack+  constant string literals.+ # 0.7 -- 2024-08-30  * Add support for GHC 9.8

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crucible-llvm-Version:       0.7+Version:       0.7.1 Author:        Galois Inc. Copyright:     (c) Galois, Inc 2014-2022 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com@@ -12,7 +12,7 @@ Description:    Library providing LLVM-specific extensions to the crucible core library    for Crucible-based simulation and verification of LLVM-compiled applications.-extra-source-files: CHANGELOG.md, README.md+extra-doc-files: CHANGELOG.md, README.md  source-repository head   type:     git@@ -44,7 +44,7 @@     extra,     lens,     itanium-abi >= 0.1.1.1 && < 0.2,-    llvm-pretty >= 0.12 && < 0.13,+    llvm-pretty >= 0.12.1 && < 0.14,     mtl,     parameterized-utils >= 2.1.5 && < 2.2,     pretty,

@@ -116,7 +116,7 @@   = let err =            AssertFailureSimError            "Found a pointer where a bitvector was expected"-           ("In the arguments or return value of" ++ Text.unpack (functionName fnm)) in+           ("In the arguments or return value of " ++ Text.unpack (functionName fnm)) in     Right (ValCast (liftIO . ptrToBv bak err)) castLLVMRet fnm bak (VectorRepr tp) (VectorRepr tp')   = do ValCast f <- castLLVMRet fnm bak tp tp'

@@ -1538,6 +1538,12 @@ unpackMemValue sym (VectorRepr tpr) (LLVMValArray _tp xs)   = traverse (unpackMemValue sym tpr) xs +-- LLVM string literals are syntactic shorthand for [<N> x i8] arrays, so we+-- defer to the LLVMValArray case above.+unpackMemValue sym tpr@(VectorRepr _) (LLVMValString str)+  = do explodedVal <- explodeStringValue sym str+       unpackMemValue sym tpr explodedVal+ unpackMemValue _sym ctp@(BVRepr _) lval@(LLVMValInt _ _) =     panic "MemModel.unpackMemValue"       [ "Cannot unpack an integer LLVM value to a crucible bitvector type"

@@ -1329,10 +1329,11 @@                              [ "Expected byte value when updating SMT array, but got:"                              , show v                              ]-                  Partial.Err _ ->+                  Partial.Err p ->                       panic "writeMemWithAllocationCheck"                              [ "Expected succesful byte load when updating SMT array"-                             , "but got an error instead"+                             , "but got an error instead:"+                             , show (printSymExpr p)                              ]        res_arr <- foldM storeArrayByteFn arr [0 .. (sz - 1)]

@@ -172,7 +172,7 @@        -- We expect at least one of the contained predicates to be false, so choose one       -- and explain that failure-      (asApp -> Just (ConjPred (viewBoolMap -> BoolMapTerms tms))) -> go (Fold.toList tms)+      (asApp -> Just (ConjPred (viewConjMap -> Conjuncts tms))) -> go (Fold.toList tms)         where         go [] = pure NoExplanation         go ((x,Positive):xs)@@ -223,7 +223,7 @@        -- under negative polarity, we expect all members of the disjunction to be false,       -- and we must construct an explanation for all of them-      (asApp -> Just (ConjPred (viewBoolMap -> BoolMapTerms tms))) -> go (Fold.toList tms) NoExplanation+      (asApp -> Just (ConjPred (viewConjMap -> Conjuncts tms))) -> go (Fold.toList tms) NoExplanation         where         go [] es = pure es         go ((x,Positive):xs) es =

@@ -43,6 +43,7 @@ import           System.Environment ( lookupEnv ) import           System.Exit ( ExitCode(..) ) import           System.FilePath ( (-<.>), splitExtension, splitFileName )+import qualified System.IO as IO import qualified System.Process as Proc  -- Modules being tested@@ -112,11 +113,14 @@ -- Mostly copied from crucible-c. parseLLVM :: FilePath -> IO (Either String Module) parseLLVM !file =-  parseBitCodeFromFile file >>=+  parseBitCodeFromFileWithWarnings file >>=     \case       Left err -> pure $ Left $ "Couldn't parse LLVM bitcode from file"                                 ++ file ++ "\n" ++ show err-      Right m  -> pure $ Right m+      Right (m, warnings) -> do+        unless (null warnings) $+          IO.hPrint IO.stderr $ ppParseWarnings warnings+        pure $ Right m  llvmTestIngredients :: [TR.Ingredient] llvmTestIngredients = includingOptions [ TO.Option (Proxy @(SomeSym LLVMAssembler))