crux 0.8.0.0 → 0.9

raw patch · 3 files changed

+87/−1 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +2/−0
• crux.cabal +1/−1
• src/Crux/Model.hs +84/−0

@@ -1,3 +1,5 @@+# 0.9 -- 2026-01-29+ # 0.8 -- 2025-11-09  * We now support running simulations with custom users state.

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crux-Version:       0.8.0.0+Version:       0.9 Copyright:     (c) Galois, Inc. 2018-2022 Author:        sweirich@galois.com Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com

@@ -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 @@ -69,9 +72,13 @@                                                -- 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+        -- NOTE: Keep these cases in sync with those in 'prettyVals'.         BaseBVRepr n -> showBVEnt n         BaseFloatRepr (FloatingPointPrecisionRepr eb sb)           | Just Refl <- testEquality eb (knownNat @8)@@ -82,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@@ -109,6 +117,82 @@       , "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)+    )