crux 0.7.2 → 0.9
raw patch · 10 files changed
Files
- CHANGELOG.md +12/−0
- crux.buildinfo.json +5/−0
- crux.cabal +7/−2
- src/Crux.hs +51/−24
- src/Crux/Config/Solver.hs +8/−5
- src/Crux/GitHash.hs +29/−0
- src/Crux/Log.hs +19/−5
- src/Crux/Model.hs +111/−4
- src/Crux/UI/JS.hs +35/−11
- src/Crux/Version.hs +87/−1
CHANGELOG.md view
@@ -1,3 +1,15 @@+# 0.9 -- 2026-01-29++# 0.8 -- 2025-11-09++* We now support running simulations with custom users state.+ For this reason, some of the Crux types now have an additional `st`+ parameter.++* `showBVLiteral` has been renamed to `showBVLiteralSigned` and+ two additional functions `showBVLiteralUnsigned` and `showBVLiteralDecimal`+ were added to improve printing of bit vectors+ # 0.7.2 -- 2025-03-21 * Add support for the Bitwuzla SMT solver.
+ crux.buildinfo.json view
@@ -0,0 +1,5 @@+{+ "hash": null,+ "branch": null,+ "dirty": null+}
crux.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: crux-Version: 0.7.2+Version: 0.9 Copyright: (c) Galois, Inc. 2018-2022 Author: sweirich@galois.com Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com@@ -18,6 +18,7 @@ the source language. extra-doc-files: CHANGELOG.md+extra-source-files: crux.buildinfo.json source-repository head type: git@@ -39,8 +40,10 @@ crucible-debug, crucible-syntax, directory,+ file-embed ^>= 0.0.16, filepath, generic-lens,+ githash ^>= 0.1.7, lens, libBF >= 0.6 && < 0.7, lumberjack >= 1.0 && < 1.1,@@ -60,7 +63,8 @@ config-schema >= 1.2.2.0, semigroupoids, xml,- yaml >= 0.11 && < 0.12+ yaml >= 0.11 && < 0.12,+ rme-what4 ^>= 0.1, hs-source-dirs: src @@ -86,6 +90,7 @@ Crux.Version other-modules:+ Crux.GitHash, Crux.UI.Jquery, Crux.UI.IndexHtml Paths_crux
src/Crux.hs view
@@ -12,6 +12,9 @@ module Crux ( runSimulator+ , runSimulatorWithUserState+ , InitUserState(..)+ , noInitUserState , postprocessSimResult , loadOptions , mkOutputConfig@@ -54,7 +57,6 @@ import System.IO ( Handle, hPutStr, stdout, stderr ) import Data.Parameterized.Classes-import qualified Data.Parameterized.Map as MapF import Data.Parameterized.Nonce (newIONonceGenerator, NonceGenerator) import Data.Parameterized.Some ( Some(..) ) @@ -85,6 +87,7 @@ import What4.Solver.CVC5 (cvc5Timeout) import What4.Solver.Yices (yicesEnableMCSat, yicesGoalTimeout) import What4.Solver.Z3 (z3Timeout)+import Data.RME.What4 (rmeAdapter) import Crux.Config import Crux.Config.Common@@ -98,13 +101,20 @@ import Crux.Report import Crux.Types -pattern RunnableState :: forall sym . () => forall ext personality . (IsSyntaxExtension ext) => ExecState (personality sym) sym ext (RegEntry sym UnitType) -> RunnableState sym+pattern RunnableState ::+ forall sym. () =>+ forall ext personality.+ ( IsSyntaxExtension ext+ , Debug.HasContext (personality sym) Void sym ext UnitType+ ) =>+ ExecState (personality sym) sym ext (RegEntry sym UnitType) ->+ RunnableState sym pattern RunnableState es = RunnableStateWithExtensions es [] -- | A crucible @ExecState@ that is ready to be passed into the simulator. -- This will usually, but not necessarily, be an @InitialState@. data RunnableState sym where- RunnableStateWithExtensions :: (IsSyntaxExtension ext)+ RunnableStateWithExtensions :: (IsSyntaxExtension ext, Debug.HasContext (personality sym) Void sym ext UnitType) => ExecState (personality sym) sym ext (RegEntry sym UnitType) -> [ExecutionFeature (personality sym) sym ext (RegEntry sym UnitType)] -> RunnableState sym@@ -121,10 +131,10 @@ -- * When simulation ends, regardless of the outcome, to interpret the results. -- -- All of these callbacks have access to the symbolic backend.-newtype SimulatorCallbacks msgs r+newtype SimulatorCallbacks msgs st r = SimulatorCallbacks { getSimulatorCallbacks ::- forall sym bak t st fs.+ forall sym bak t fs. ( IsSymBackend sym bak , Logs msgs , sym ~ WE.ExprBuilder t st fs@@ -562,6 +572,7 @@ case solverOff of CCS.Boolector -> k WS.boolectorAdapter CCS.DReal -> k WS.drealAdapter+ CCS.RME -> k rmeAdapter CCS.SolverOnline CCS.CVC4 -> k WS.cvc4Adapter CCS.SolverOnline CCS.CVC5 -> k WS.cvc5Adapter CCS.SolverOnline CCS.STP -> k WS.stpAdapter@@ -576,6 +587,16 @@ base adapters = k adapters go nextOff withAdapters adapters = withSolverAdapter nextOff (\adapter -> withAdapters (adapter:adapters)) ++{- | Create a fresh user state.+We use this to create a fresh user input when we create a new simulator. -}+newtype InitUserState s =+ InitUserState { initUserState :: forall t. IO (s t) }++-- | A helper to use when we don't have interesting user state.+noInitUserState :: InitUserState WE.EmptyExprBuilderState+noInitUserState = InitUserState { initUserState = pure WE.EmptyExprBuilderState }+ -- | Parse through all of the user-provided options and start up the verification process -- -- This figures out which solvers need to be run, and in which modes. It takes@@ -586,23 +607,39 @@ Logs msgs => SupportsCruxLogMessage msgs => CruxOptions ->- SimulatorCallbacks msgs r ->+ SimulatorCallbacks msgs WE.EmptyExprBuilderState r -> IO r-runSimulator cruxOpts simCallback = do+runSimulator = runSimulatorWithUserState noInitUserState++-- | Parse through all of the user-provided options and start up the verification process+--+-- This figures out which solvers need to be run, and in which modes. It takes+-- as arguments some of the results of common setup code. It also tries to+-- minimize code duplication between the different verification paths (e.g.,+-- online vs offline solving).+runSimulatorWithUserState ::+ Logs msgs =>+ SupportsCruxLogMessage msgs =>+ InitUserState st ->+ CruxOptions ->+ SimulatorCallbacks msgs st r ->+ IO r+runSimulatorWithUserState mkUser cruxOpts simCallback = do sayCrux (Log.Checking (inputFiles cruxOpts)) createDirectoryIfMissing True (outDir cruxOpts) Some (nonceGen :: NonceGenerator IO s) <- newIONonceGenerator+ userState <- initUserState mkUser case CCS.parseSolverConfig cruxOpts of Right (CCS.SingleOnlineSolver onSolver) ->- withSelectedOnlineBackend cruxOpts nonceGen onSolver Nothing WE.EmptyExprBuilderState $ \bak -> do+ withSelectedOnlineBackend cruxOpts nonceGen onSolver Nothing userState $ \bak -> do let monline = Just (SomeOnlineSolver bak) setupSolver cruxOpts (pathSatSolverOutput cruxOpts) (backendGetSym bak) (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts bak monline doSimWithResults cruxOpts simCallback bak execFeatures profInfo monline (proveGoalsOnline bak) Right (CCS.OnlineSolverWithOfflineGoals onSolver offSolver) ->- withSelectedOnlineBackend cruxOpts nonceGen onSolver Nothing WE.EmptyExprBuilderState $ \bak -> do+ withSelectedOnlineBackend cruxOpts nonceGen onSolver Nothing userState $ \bak -> do let monline = Just (SomeOnlineSolver bak) setupSolver cruxOpts (pathSatSolverOutput cruxOpts) (backendGetSym bak) (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts bak monline@@ -616,9 +653,9 @@ doSimWithResults cruxOpts simCallback bak execFeatures profInfo monline (proveGoalsOffline [adapter]) Right (CCS.OnlyOfflineSolvers offSolvers) ->- withFloatRepr (WE.EmptyExprBuilderState @s) cruxOpts offSolvers $ \floatRepr -> do+ withFloatRepr userState cruxOpts offSolvers $ \floatRepr -> do withSolverAdapters offSolvers $ \adapters -> do- sym <- WE.newExprBuilder floatRepr WE.EmptyExprBuilderState nonceGen+ sym <- WE.newExprBuilder floatRepr userState nonceGen bak <- CBS.newSimpleBackend sym setupSolver cruxOpts Nothing sym -- Since we have a bare SimpleBackend here, we have to initialize it@@ -631,7 +668,7 @@ -- This case is probably the most complicated because it needs two -- separate online solvers. The two must agree on the floating point -- mode.- withSelectedOnlineBackend cruxOpts nonceGen pathSolver Nothing WE.EmptyExprBuilderState $ \pathSatBak -> do+ withSelectedOnlineBackend cruxOpts nonceGen pathSolver Nothing userState $ \pathSatBak -> do let sym = backendGetSym pathSatBak setupSolver cruxOpts (pathSatSolverOutput cruxOpts) sym (execFeatures, profInfo) <- setupExecutionFeatures cruxOpts pathSatBak (Just (SomeOnlineSolver pathSatBak))@@ -657,7 +694,7 @@ Logs msgs => SupportsCruxLogMessage msgs => CruxOptions ->- SimulatorCallbacks msgs r ->+ SimulatorCallbacks msgs st r -> bak -> [GenericExecutionFeature sym] -> ProfData sym ->@@ -690,17 +727,7 @@ if debugging then do let ?parserHooks = Syn.ParserHooks Applicative.empty Applicative.empty- let cExts = Debug.voidExts- inps <- Debug.defaultDebuggerInputs cExts- dbg <-- Debug.debugger- cExts- Debug.voidImpl- (Debug.IntrinsicPrinters MapF.empty)- inps- Debug.defaultDebuggerOutputs- UnitRepr- pure [dbg]+ pure [Debug.debugger Debug.voidImpl] else pure [] -- execute the simulator
src/Crux/Config/Solver.hs view
@@ -25,7 +25,7 @@ data SolverOnline = Yices | Z3 | CVC4 | CVC5 | STP | Bitwuzla deriving (Eq, Ord, Show)-data SolverOffline = SolverOnline SolverOnline | Boolector | DReal+data SolverOffline = SolverOnline SolverOnline | Boolector | DReal | RME deriving (Eq, Ord, Show) class HasDefaultFloatRepr solver where@@ -50,6 +50,7 @@ case s of SolverOnline s' -> withDefaultFloatRepr st s' k Boolector -> k WEB.FloatUninterpretedRepr+ RME -> k WEB.FloatUninterpretedRepr DReal -> k WEB.FloatRealRepr -- | Test to see if an online and offline solver are actually the same@@ -106,31 +107,33 @@ invalid :: String -> Validated a invalid rsn = Invalid [rsn] --- | Boolector and DReal only support offline solving (for our purposes), so+-- | Boolector, RME and DReal only support offline solving (for our purposes), so -- attempt to parse them from the given string asOnlyOfflineSolver :: String -> Validated SolverOffline asOnlyOfflineSolver s = case s of "dreal" -> pure DReal "boolector" -> pure Boolector- _ -> invalid (printf "%s is not an offline-only solver (expected dreal or boolector)" s)+ "rme" -> pure RME+ _ -> invalid (printf "%s is not an offline-only solver (expected dreal, rme or boolector)" s) -- | Solvers that can be used in offline mode asAnyOfflineSolver :: String -> Validated SolverOffline asAnyOfflineSolver s = case s of "dreal" -> pure DReal "boolector" -> pure Boolector+ "rme" -> pure RME "z3" -> pure (SolverOnline Z3) "yices" -> pure (SolverOnline Yices) "cvc4" -> pure (SolverOnline CVC4) "cvc5" -> pure (SolverOnline CVC5) "stp" -> pure (SolverOnline STP) "bitwuzla" -> pure (SolverOnline Bitwuzla)- _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, stp, or bitwuzla)" s)+ _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, stp, rme, or bitwuzla)" s) asManyOfflineSolvers :: String -> Validated [SolverOffline] asManyOfflineSolvers s- | s == "all" = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp,bitwuzla"+ | s == "all" = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp,bitwuzla,rme" | length solvers > 1 = traverse asAnyOfflineSolver solvers | otherwise = invalid (printf "%s is not a valid solver list (expected 'all' or a comma separated list of solvers)" s) where
+ src/Crux/GitHash.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE TemplateHaskell #-}++-- | These are placed in their own module to minimize the cost of recompilation+-- due to Template Haskell.+module Crux.GitHash (hash, branch, dirty, unknown) where++import GitHash (GitInfo, giBranch, giDirty, giHash, tGitInfoCwdTry)++gitInfo :: Either String GitInfo+gitInfo = $$tGitInfoCwdTry++hash :: String+hash = case gitInfo of+ Left _ -> unknown+ Right gi -> giHash gi++branch :: String+branch = case gitInfo of+ Left _ -> unknown+ Right gi -> giBranch gi++dirty :: Bool+dirty = case gitInfo of+ Left _ -> False+ Right gi -> giDirty gi++-- | What to report if we are unable to determine git-related information.+unknown :: String+unknown = "UNKNOWN"
src/Crux/Log.hs view
@@ -44,6 +44,7 @@ import Control.Lens ( Getter, view ) import qualified Data.Aeson as JSON import Data.Aeson.TH ( deriveToJSON )+import qualified Data.List as List import qualified Data.Text as T import Data.Text.IO as TIO ( hPutStr, hPutStrLn ) import Data.Version ( Version, showVersion )@@ -59,7 +60,8 @@ import Crux.Types ( CruxSimulationResult, ProvedGoals, SayLevel(..), SayWhat(..) )-import Crux.Version ( version )+import Crux.Version+ ( commitBranch, commitDirty, commitHash, version ) import Lang.Crucible.Backend ( ProofGoal(..), ProofObligation ) import What4.Expr.Builder ( ExprBuilder ) import What4.LabeledPred ( labeledPred, labeledPredMsg )@@ -129,7 +131,9 @@ | StartedGoal Integer | TotalPathsExplored Word64 | UnsupportedTimeoutFor String -- ^ name of the backend- | Version T.Text Version+ | Version+ T.Text -- ^ name of the backend+ Version -- ^ backend-specific version deriving (Generic) $(deriveToJSON JSON.defaultOptions ''CruxLogMessage)@@ -220,13 +224,23 @@ cruxLogMessageToSayWhat (Version nm ver) = cruxOK ( T.pack- ( unwords+ ( List.intercalate+ "\n"+ [ unwords [ "version: " <> version <> ",", T.unpack nm,- "version: " <> (showVersion ver)+ "version: " <> showVersion ver ]- )+ , "Git commit " <> commitHash+ , " branch " <> commitBranch <> dirtyLab+ ]+ ) )+ where+ dirtyLab :: String+ dirtyLab+ | commitDirty = " (non-committed files present during build)"+ | otherwise = "" -- | Main function used to log/output a general text message of some kind say ::
src/Crux/Model.hs view
@@ -1,6 +1,7 @@ -- | This file is almost exactly the same as crucible-c/src/Model.hs {-# Language DataKinds #-}+{-# Language OverloadedStrings #-} {-# Language PolyKinds #-} {-# Language Rank2Types #-} {-# Language TypeFamilies #-}@@ -19,6 +20,8 @@ import qualified Numeric as N import LibBF (BigFloat) import qualified LibBF as BF+import qualified Prettyprinter as PP+import Prettyprinter (Doc) import Lang.Crucible.Types @@ -34,14 +37,25 @@ toDouble :: Rational -> Double toDouble = fromRational --showBVLiteral :: (1 <= w) => NatRepr w -> BV w -> String-showBVLiteral w bv =+showBVLiteralSigned :: (1 <= w) => NatRepr w -> BV w -> String+showBVLiteralSigned w bv = (if x < 0 then "-0x" else "0x") ++ N.showHex i (if natValue w == 64 then "L" else "") where x = BV.asSigned w bv i = abs x +showBVLiteralUnsigned :: (1 <= w) => NatRepr w -> BV w -> String+showBVLiteralUnsigned w bv =+ "0x" ++ N.showHex i (if natValue w == 64 then "L" else "")+ where+ i = BV.asUnsigned bv++showBVLiteralDecimal :: (1 <= w) => NatRepr w -> BV w -> String+showBVLiteralDecimal w bv =+ show x+ where+ x = BV.asSigned w bv+ showFloatLiteral :: BigFloat -> String showFloatLiteral x | BF.bfIsNaN x = "NAN"@@ -58,10 +72,14 @@ -- NB, 53 bits of precision for double | otherwise = BF.bfToString 16 (BF.showFree (Just 53) <> BF.addPrefix) x +showBoolLiteral :: Bool -> String+showBoolLiteral b = if b then "true" else "false"+ valsJS :: BaseTypeRepr ty -> Vals ty -> IO [JS] valsJS ty (Vals xs) = let showEnt = case ty of- BaseBVRepr n -> showEnt' (showBVLiteral n) n+ -- NOTE: Keep these cases in sync with those in 'prettyVals'.+ BaseBVRepr n -> showBVEnt n BaseFloatRepr (FloatingPointPrecisionRepr eb sb) | Just Refl <- testEquality eb (knownNat @8) , Just Refl <- testEquality sb (knownNat @24)@@ -71,6 +89,7 @@ , Just Refl <- testEquality sb (knownNat @53) -> showEnt' showDoubleLiteral (64 :: Int) BaseRealRepr -> showEnt' (show . toDouble) (knownNat @64)+ BaseBoolRepr -> showBoolEnt _ -> error ("Type not implemented: " ++ show ty) in mapM showEnt xs@@ -86,6 +105,94 @@ , "bits" ~> jsStr (show n) ] + showBVEnt :: (1 <= w) => NatRepr w -> Entry (BV w) -> IO JS+ showBVEnt n e = do+ l <- fromMaybe jsNull <$> jsLoc (entryLoc e)+ pure $ jsObj+ [ "name" ~> jsStr (entryName e)+ , "loc" ~> l+ , "val" ~> jsStr (showBVLiteralSigned n (entryValue e))+ , "val-unsigned" ~> jsStr (showBVLiteralUnsigned n (entryValue e))+ , "val-decimal" ~> jsStr (showBVLiteralDecimal n (entryValue e))+ , "bits" ~> jsStr (show n)+ ]++ showBoolEnt :: Entry Bool -> IO JS+ showBoolEnt e = do+ do l <- fromMaybe jsNull <$> jsLoc (entryLoc e)+ pure $ jsObj+ [ "name" ~> jsStr (entryName e)+ , "loc" ~> l+ , "val" ~> jsStr (showBoolLiteral (entryValue e))+ ]+ modelJS :: ModelView -> IO JS modelJS m = jsList . concat <$> sequence (MapF.foldrWithKey (\k v xs -> valsJS k v : xs) [] (modelVals m))++-- Pretty-print all entries in a model for a given base type.+prettyVals :: BaseTypeRepr ty -> Vals ty -> [Doc ann]+prettyVals ty (Vals xs) =+ let ppEnt = case ty of+ -- NOTE: Keep these cases in sync with those in 'valsJS'.+ BaseBVRepr n -> prettyBVEnt n++ BaseFloatRepr (FloatingPointPrecisionRepr eb sb)+ | Just Refl <- testEquality eb (knownNat @8)+ , Just Refl <- testEquality sb (knownNat @24)+ -> prettyEnt' showFloatLiteral++ BaseFloatRepr (FloatingPointPrecisionRepr eb sb)+ | Just Refl <- testEquality eb (knownNat @11)+ , Just Refl <- testEquality sb (knownNat @53)+ -> prettyEnt' showDoubleLiteral++ BaseRealRepr ->+ -- same semantics as valsJS: print reals via toDouble+ prettyEnt' (show . toDouble)++ BaseBoolRepr ->+ prettyEnt' showBoolLiteral++ _ ->+ error ("Type not implemented: " ++ show ty)+ in+ map ppEnt xs++-- Generic entry printer for "simple" values.+prettyEnt' :: (a -> String) -> Entry a -> Doc ann+prettyEnt' repr e =+ PP.hsep+ [ PP.pretty (entryName e)+ , "="+ , PP.pretty (repr (entryValue e))+ ]++-- Bitvector entries: signed, unsigned, decimal on a single line.+prettyBVEnt :: (1 <= w) => NatRepr w -> Entry (BV w) -> Doc ann+prettyBVEnt n e =+ let v = entryValue e+ sg = showBVLiteralSigned n v+ un = showBVLiteralUnsigned n v+ dec = showBVLiteralDecimal n v+ in+ PP.hsep+ [ PP.pretty (entryName e)+ , "="+ , PP.pretty sg+ , "(signed),"+ , PP.pretty un+ , "(unsigned),"+ , PP.pretty dec+ , "(decimal)"+ ]++-- Human-readable model as a Prettyprinter 'Doc'.+prettyModel :: ModelView -> Doc ann+prettyModel m =+ PP.vsep+ (MapF.foldrWithKey+ (\ty vals docs -> prettyVals ty vals ++ docs)+ []+ (modelVals m)+ )
src/Crux/UI/JS.hs view
@@ -3,27 +3,51 @@ -- | Utilites for generating JSON module Crux.UI.JS where -import Data.Text(unpack)+import Data.Text(unpack, Text)+import qualified Data.Text as Text+import Numeric import Data.List(intercalate) import Data.Maybe(fromMaybe) import System.Directory( canonicalizePath ) import What4.ProgramLoc +-- | 'jsLoc' takes a program location and renders it as a JavaScript string.+-- This returns @Nothing@ if it is unclear how to render the program location. jsLoc :: ProgramLoc -> IO (Maybe JS) jsLoc x = case plSourceLoc x of- SourcePos f l c ->- do let fstr = unpack f- fabsolute <-- if | null fstr -> pure ""- | otherwise -> canonicalizePath fstr- pure $ Just $ jsObj- [ "file" ~> jsStr fabsolute- , "line" ~> jsStr (show l)- , "col" ~> jsStr (show c)- ]+ SourcePos fname l c -> parsePos fname l c+ -- Attempt to parse `OtherPos` in case it is in fact a code span:+ --+ -- * This case is necessary because of the particular shape of source+ -- spans that arise from `mir-json`+ -- (e.g., `test/symb_eval/num/checked_mul.rs:6:5: 6:12:`), which will+ -- always be represented as `OtherPos`.+ -- * While `crux` doesn't have the machinery to represent the entire+ -- source span in its UI framework, we can still achieve partial results+ -- by parsing the first location from the source span+ -- (e.g., `the test/symb_eval/num/checked_mul.rs:6:5:` bit). This does+ -- not show the entire span, but it is still better than nothing.+ OtherPos s+ | fname : line : col : _rest <- Text.split (==':') s+ , (l,[]):_ <- readDec (Text.unpack (Text.strip line))+ , (c,[]):_ <- readDec (Text.unpack (Text.strip col)) ->+ parsePos fname l c _ -> pure Nothing+ where+ parsePos :: Text -> Int -> Int -> IO (Maybe JS)+ parsePos f l c = do+ let fstr = unpack f+ fabsolute <-+ if null fstr+ then pure ""+ else canonicalizePath fstr+ pure $ Just $ jsObj+ [ "file" ~> jsStr fabsolute+ , "line" ~> jsStr (show l)+ , "col" ~> jsStr (show c)+ ] -------------------------------------------------------------------------------- newtype JS = JS { renderJS :: String }
src/Crux/Version.hs view
@@ -1,9 +1,95 @@-module Crux.Version where+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TemplateHaskell #-} +module Crux.Version+ ( version+ , commitHash+ , commitBranch+ , commitDirty+ ) where++import qualified Data.Aeson as Aeson+import qualified Data.Aeson.KeyMap as KeyMap+import qualified Data.ByteString as BS+import Data.FileEmbed (embedFileRelative)+import qualified Data.Text as Text import Data.Version (showVersion) import qualified Paths_crux (version) +import qualified Crux.GitHash as GitHash+ version :: String version = showVersion Paths_crux.version +commitHash :: String+commitHash+ | hash /= GitHash.unknown =+ hash+ -- See Note [crux.buildinfo.json]+ | Just buildinfoVal <- Aeson.decodeStrict buildinfo+ , Just (Aeson.String buildinfoHash) <- KeyMap.lookup "hash" buildinfoVal =+ Text.unpack buildinfoHash+ | otherwise =+ GitHash.unknown+ where+ hash = GitHash.hash +commitBranch :: String+commitBranch+ | branch /= GitHash.unknown =+ branch+ -- See Note [crux.buildinfo.json]+ | Just buildinfoVal <- Aeson.decodeStrict buildinfo+ , Just (Aeson.String buildinfoCommit) <- KeyMap.lookup "branch" buildinfoVal =+ Text.unpack buildinfoCommit+ | otherwise =+ GitHash.unknown+ where+ branch = GitHash.branch++commitDirty :: Bool+commitDirty+ | dirty =+ dirty+ -- See Note [crux.buildinfo.json]+ | Just buildinfoVal <- Aeson.decodeStrict buildinfo+ , Just (Aeson.Bool buildinfoDirty) <- KeyMap.lookup "dirty" buildinfoVal =+ buildinfoDirty+ | otherwise =+ False+ where+ dirty = GitHash.dirty++-- Helper, not exported+--+-- See Note [crux.buildinfo.json]+buildinfo :: BS.ByteString+buildinfo = $(embedFileRelative "crux.buildinfo.json")++{-+Note [crux.buildinfo.json]+~~~~~~~~~~~~~~~~~~~~~~~~~~+By default, we determine the git commit hash, branch, and dirty information+using the githash library, which invokes git at compile time to query the+relevant information in the .git subdirectory. This works well for local+developments where the git binary and the .git subdirectory are both readily+available. It does not work so well for building in a Docker image, as we+intentionally do not copy over the .git subdirectory into the image to prevent+spurious cache invalidations caused by the contents of .git changing (which+they do, quite often).++As an alternative to githash, we also employ a convention where a build system+can create a crux.buildinfo.json file locally which contains the necessary+git-related information. The schema for this file is:++ {+ "hash": <string>,+ "branch": <string>,+ "dirty": <bool>+ }++This way, a build system (which has access to git/.git) can write this+information to a file, proceed to build the Docker image (which does not have+access to git/.git), and then have all of the expected information embedded+into the output of --version.+-}