diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/crux.buildinfo.json b/crux.buildinfo.json new file mode 100644 --- /dev/null +++ b/crux.buildinfo.json @@ -0,0 +1,5 @@ +{ + "hash": null, + "branch": null, + "dirty": null +} diff --git a/crux.cabal b/crux.cabal --- a/crux.cabal +++ b/crux.cabal @@ -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 diff --git a/src/Crux.hs b/src/Crux.hs --- a/src/Crux.hs +++ b/src/Crux.hs @@ -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 diff --git a/src/Crux/Config/Solver.hs b/src/Crux/Config/Solver.hs --- a/src/Crux/Config/Solver.hs +++ b/src/Crux/Config/Solver.hs @@ -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 diff --git a/src/Crux/GitHash.hs b/src/Crux/GitHash.hs new file mode 100644 --- /dev/null +++ b/src/Crux/GitHash.hs @@ -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" diff --git a/src/Crux/Log.hs b/src/Crux/Log.hs --- a/src/Crux/Log.hs +++ b/src/Crux/Log.hs @@ -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 :: diff --git a/src/Crux/Model.hs b/src/Crux/Model.hs --- a/src/Crux/Model.hs +++ b/src/Crux/Model.hs @@ -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) + ) diff --git a/src/Crux/UI/JS.hs b/src/Crux/UI/JS.hs --- a/src/Crux/UI/JS.hs +++ b/src/Crux/UI/JS.hs @@ -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 } diff --git a/src/Crux/Version.hs b/src/Crux/Version.hs --- a/src/Crux/Version.hs +++ b/src/Crux/Version.hs @@ -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": , + "branch": , + "dirty": + } + +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. +-}