crux-llvm 0.12 → 0.13
raw patch · 7 files changed
+39/−20 lines, 7 filesdep +microlensdep +microlens-mtldep +microlens-thdep −lensdep ~basedep ~crux
Dependencies added: microlens, microlens-mtl, microlens-th
Dependencies removed: lens
Dependency ranges changed: base, crux
Files
- CHANGELOG.md +6/−0
- README.md +1/−1
- crux-llvm.cabal +9/−4
- for-ide/Main.hs +3/−1
- src/Crux/LLVM/Config.hs +6/−3
- src/Crux/LLVM/Simulate.hs +13/−10
- test/Test.hs +1/−1
CHANGELOG.md view
@@ -1,3 +1,9 @@+# 0.13 -- 2026-09-10++* Add support for GHC 9.12 (at 9.12.2) and bump from 9.10.1 to 9.10.3.+* Support LLVM 22.+* **BREAKING**: `explainFailure` now takes a `FloatModeRepr` argument.+ # 0.12 -- 2026-01-29 # 0.11 -- 2025-11-09
README.md view
@@ -50,7 +50,7 @@ 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 21 are likely to+convenient. Finally, LLVM versions from 3.6 through 22 are likely to work well, and any failures with versions in that range should be [reported as bugs](https://github.com/GaloisInc/crucible/issues).
crux-llvm.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: crux-llvm-Version: 0.12+Version: 0.13 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.21+ build-depends: base >= 4.8 && < 4.22 , bytestring , containers , crucible@@ -64,7 +64,7 @@ , crux , directory , filepath- , lens+ , microlens , process , text , what4@@ -88,7 +88,6 @@ ghc-options: -Wall -Werror=ambiguous-fields- -Werror=compat-unqualified-imports -Werror=deferred-type-errors -Werror=deprecated-flags -Werror=deprecations@@ -160,6 +159,10 @@ -Werror=deprecated-type-abstractions -Werror=incomplete-record-selectors + if impl(ghc < 9.12)+ ghc-options:+ -Werror=compat-unqualified-imports+ common testdefs build-depends: tasty >= 0.10 , tasty-hunit >= 0.10@@ -190,6 +193,7 @@ logict, llvm-pretty, llvm-pretty-bc-parser >= 0.5,+ microlens-mtl, mtl, parameterized-utils, prettyprinter >= 1.7.0@@ -223,6 +227,7 @@ aeson, crux-llvm, lumberjack,+ microlens-th, websockets >= 0.12 main-is: Main.hs
for-ide/Main.hs view
@@ -4,7 +4,6 @@ module Main (main) where -import Control.Lens (makeLenses, set, view) import Crux (OutputConfig) import qualified Crux import Crux.Config.Common (OutputOptions)@@ -16,6 +15,9 @@ ) import qualified Data.Aeson as JSON import Data.Text as Text (Text, unpack)+import Lens.Micro (set)+import Lens.Micro.Extras (view)+import Lens.Micro.TH (makeLenses) import qualified Lumberjack as LJ import qualified Network.WebSockets as WS import Paths_crux_llvm (version)
src/Crux/LLVM/Config.hs view
@@ -9,6 +9,7 @@ import Control.Exception ( Exception, displayException, throwIO ) import Control.Monad ( guard ) import Control.Monad.State ( liftIO, MonadIO )+import Data.List (intercalate) import qualified Data.Text as Text import System.Directory ( doesDirectoryExist ) import System.Environment ( getExecutablePath )@@ -46,7 +47,7 @@ ppCError err = case err of NoFiles -> "crux-llvm requires at least one input file." EnvError msg -> msg- BadFun fnName isMain -> unlines $+ BadFun fnName isMain -> ofLines $ [ "The '" ++ fnName ++ "' function should have no arguments"] ++ [ "Enable `supply-main-arguments` to relax this restriction" | isMain@@ -54,14 +55,16 @@ MissingFun x -> "Cannot find code for " ++ show x LLVMParseError e -> LLVM.formatError e ClangError n sout serr ->- unlines $ [ "`clang` compilation failed."+ ofLines $ [ "`clang` compilation failed." , "*** Exit code: " ++ show n , "*** Standard out:" ] ++ [ " " ++ l | l <- lines sout ] ++ [ "*** Standard error:" ] ++ [ " " ++ l | l <- lines serr ]-+ where+ -- Contrast with `Prelude.unlines`, which appends a trailing newline+ ofLines = intercalate "\n" throwCError :: MonadIO m => CError -> m b throwCError e = liftIO (throwIO e)
src/Crux/LLVM/Simulate.hs view
@@ -16,21 +16,23 @@ module Crux.LLVM.Simulate where -import qualified Control.Lens as Lens import Control.Monad (unless)-import Data.String (fromString)-import qualified Data.Map.Strict as Map+import Control.Monad.IO.Class (liftIO) import Data.IORef import qualified Data.List as List+import qualified Data.Map.Strict as Map import Data.Maybe ( fromMaybe ) import qualified Data.Parameterized.Map as MapF import Data.Sequence (Seq)+import Data.String (fromString) import qualified Data.Traversable as T-import Control.Lens ((&), (%~), (%=), (^.), use, view)-import Control.Monad.IO.Class (liftIO) import Data.Text as Text (Text, pack) import Data.Void (Void) import GHC.Exts ( proxy# )+import qualified Lens.Micro as Lens+import Lens.Micro ((&), (%~), (^.))+import Lens.Micro.Extras (view)+import Lens.Micro.Mtl ((%=), use) import System.IO (stdout) @@ -193,7 +195,7 @@ LLVMOptions -> Crux.SimulatorCallbacks msgs st Crux.Types.CruxSimulationResult simulateLLVMFile llvm_file llvmOpts =- Crux.SimulatorCallbacks $+ Crux.SimulatorCallbacks $ \fm -> do bbMapRef <- newIORef (Map.empty :: LLVMAnnMap sym) let ?recordLLVMAnnotation = \callStack an bb ->@@ -205,7 +207,7 @@ do halloc <- newHandleAllocator setupFileSim halloc llvm_file llvmOpts bak maybeOnline , Crux.onErrorHook =- \bak -> return (explainFailure (backendGetSym bak) bbMapRef)+ \bak -> return (explainFailure (backendGetSym bak) fm bbMapRef) , Crux.resultHook = \_sym result -> return result } @@ -424,13 +426,14 @@ detailLimit = 10 explainFailure :: IsSymInterface sym- => sym ~ WEB.ExprBuilder t st fs+ => sym ~ WEB.ExprBuilder t st (WEB.Flags fm) => sym+ -> WEB.FloatModeRepr fm -> IORef (LLVMAnnMap sym) -> Crux.Explainer sym t ann-explainFailure sym bbMapRef evalFn gl =+explainFailure sym fm bbMapRef evalFn gl = do bb <- readIORef bbMapRef- ex <- explainCex sym bb evalFn >>= \f -> f (gl ^. labeledPred)+ ex <- explainCex sym fm bb evalFn >>= \f -> f (gl ^. labeledPred) let details = case ex of NoExplanation -> mempty
test/Test.hs view
@@ -6,7 +6,6 @@ module Main (main) where import Control.Exception ( SomeException, catches, try, Handler(..), IOException )-import Control.Lens ( (^?), _Right ) import Control.Monad ( unless, when ) import Data.Bifunctor ( first ) import qualified Data.ByteString.Lazy as BSIO@@ -18,6 +17,7 @@ import qualified Data.Version as Version import Data.Versions ( Versioning, versioning, prettyV, major ) import qualified GHC.IO.Exception as GE+import Lens.Micro ((^?), _Right) import Numeric.Natural import System.Environment ( withArgs, lookupEnv ) import System.Exit ( ExitCode(..) )