crucible 0.7.1 → 0.7.2

raw patch · 9 files changed

+392/−144 lines, 9 filesdep ~parameterized-utilsdep ~tasty-hunitdep ~what4new-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: parameterized-utils, tasty-hunit, what4

API changes (from Hackage documentation)

Files

• CHANGELOG.md +7/−0
• crucible.cabal +9/−4
• src/Lang/Crucible/Backend.hs +32/−13
• src/Lang/Crucible/Backend/Goals.hs +146/−0
• src/Lang/Crucible/Backend/Online.hs +26/−5
• src/Lang/Crucible/Backend/ProofGoals.hs +2/−116
• src/Lang/Crucible/Backend/Simple.hs +0/−5
• src/Lang/Crucible/Types.hs +94/−1
• test/helpers/Main.hs +76/−0

@@ -1,3 +1,10 @@+# 0.7.2 -- 2025-03-21++* Add support for Bitwuzla as an online SMT solver backend.+* Add a function `ppTypeRepr` to `Lang.Crucible.Types` for pretty-printing+  `TypeRepr`s. Modify the `Pretty` instance to use this function.+* Add an `EqF TypeRepr` instance.+ # 0.7.1 -- 2024-08-30  * Add support for GHC 9.8

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          crucible-Version:       0.7.1+Version:       0.7.2 Author:        Galois Inc. Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com Copyright:     (c) Galois, Inc 2014-2022@@ -14,7 +14,7 @@   (SSA) form control flow graphs, and a symbolic simulation engine for executing   programs expressed in this format.  It also provides support for communicating with   a variety of SAT and SMT solvers, including Z3, CVC4, Yices, STP, and dReal.-extra-source-files: CHANGELOG.md+extra-doc-files: CHANGELOG.md  source-repository head   type:     git@@ -65,7 +65,7 @@     transformers,     unordered-containers,     vector,-    what4 >= 0.4+    what4 >= 1.6.1    default-extensions:      NondecreasingIndentation@@ -85,6 +85,7 @@     Lang.Crucible.Analysis.Reachable     Lang.Crucible.Backend     Lang.Crucible.Backend.AssumptionStack+    Lang.Crucible.Backend.Goals     Lang.Crucible.Backend.ProofGoals     Lang.Crucible.Backend.Online     Lang.Crucible.Backend.Prove@@ -167,6 +168,10 @@   build-depends: base,                  hspec >= 2.5,                  crucible,+                 lens,                  panic >= 0.3,+                 parameterized-utils,                  tasty >= 0.10,-                 tasty-hspec >= 1.1+                 tasty-hspec >= 1.1,+                 tasty-hunit,+                 what4

@@ -16,13 +16,11 @@ 'Lang.Crucible.Backend.Online.OnlineBackend' is designed to be used with an online solver. -The 'AS.AssumptionStack' tracks the assumptions that are in scope for each-assertion, accounting for the branching and merging structure of programs.  The-symbolic simulator manages the 'AS.AssumptionStack'. After symbolic simulation-completes, the caller should traverse the 'AS.AssumptionStack' (or use-combinators like 'AS.proofGoalsToList') to discharge the resulting proof-obligations with a solver backend.-+The backend tracks the assumptions that are in scope for each assertion,+accounting for the branching and merging structure of programs. After+symbolic simulation completes, the caller should traverse the collected+'ProofObligations'  (via 'getProofObligations') to discharge the resulting proof+obligations with a solver backend. See also "Lang.Crucible.Backend.Prove". -} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-}@@ -208,6 +206,20 @@ --   type is expected to satisfy the `IsSymInterface` constraints, which --   provide access to the What4 expression language. A @sym@ is uniquely --   determined by a @bak@.+--+--+--   == Note [Pushes and pops]+--+--   This class provides methods for pushing ('pushAssumptionFrame')+--   and popping ('popAssumptionFrame', 'popUntilAssumptionFrame',+--   'popAssumptionFrameAndObligations') frames. Pushes and pops must be+--   well-bracketed. In particular, @popAssumptionFrame*@ are required to throw+--   an exception if the provided frame identifier does not match the top of+--   the stack.+--+--   It is relatively easy to end up with ill-bracketed pushes and pops in the+--   presence of exceptions. When diagnosing such issues, consider popping+--   frames using methods such as 'Control.Exception.try'. class (IsSymInterface sym, HasSymInterface sym bak) => IsSymBackend sym bak | bak -> sym where    ----------------------------------------------------------------------@@ -219,9 +231,9 @@   pushAssumptionFrame :: bak -> IO AS.FrameIdentifier    -- | Pop an assumption frame from the stack.  The collected assumptions-  --   in this frame are returned.  Pops are required to be well-bracketed-  --   with pushes.  In particular, if the given frame identifier is not-  --   the identifier of the top frame on the stack, an error will be raised.+  --   in this frame are returned.+  --+  --   This may throw an exception, see Note [Pushes and pops].   popAssumptionFrame :: bak -> AS.FrameIdentifier -> IO (Assumptions sym)    -- | Pop all assumption frames up to and including the frame with the given@@ -231,9 +243,12 @@    -- | Pop an assumption frame from the stack.  The collected assummptions   --   in this frame are returned, along with any proof obligations that were-  --   incurred while the frame was active. Pops are required to be well-bracketed-  --   with pushes.  In particular, if the given frame identifier is not-  --   the identifier of the top frame on the stack, an error will be raised.+  --   incurred while the frame was active.+  --+  --   Note that the returned 'ProofObligation's only include assumptions from+  --   the popped frame, not all frames above it.+  --+  --   This may throw an exception, see Note [Pushes and pops].   popAssumptionFrameAndObligations ::     bak -> AS.FrameIdentifier -> IO (Assumptions sym, ProofObligations sym) @@ -249,6 +264,10 @@   -- | Get the current path condition as a predicate.  This consists of the conjunction   --   of all the assumptions currently in scope.   getPathCondition :: bak -> IO (Pred sym)+  getPathCondition bak = do+    let sym = backendGetSym bak+    ps <- collectAssumptions bak+    assumptionsPred sym ps    -- | Collect all the assumptions currently in scope   collectAssumptions :: bak -> IO (Assumptions sym)

@@ -0,0 +1,146 @@+{-|+Module      : Lang.Crucible.Backend.Goals+Copyright   : (c) Galois, Inc 2025+License     : BSD3++This module defines a data strucutre for storing a collection of+proof obligations, and the current state of assumptions.+-}++{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TupleSections #-}++module Lang.Crucible.Backend.Goals+  ( ProofGoal(..)+  , Goals(..)+  , goalsToList+  , assuming+  , proveAll+  , goalsConj+    -- * Traversals+  , traverseGoals+  , traverseOnlyGoals+  , traverseGoalsWithAssumptions+  , traverseGoalsSeq+  )+  where++import           Control.Monad.Reader (ReaderT(..), withReaderT)+import           Data.Functor.Const (Const(..))+import           Data.Sequence (Seq)+import qualified Data.Sequence as Seq++-- | A proof goal consists of a collection of assumptions+--   that were in scope when an assertion was made, together+--   with the given assertion.+data ProofGoal asmp goal =+  ProofGoal+  { proofAssumptions :: asmp+  , proofGoal        :: goal+  }++-- | A collection of goals, which can represent shared assumptions.+data Goals asmp goal =+    -- | Make an assumption that is in context for all the+    --   contained goals.+    Assuming asmp !(Goals asmp goal)++    -- | A proof obligation, to be proved in the context of+    --   all previously-made assumptions.+  | Prove goal++    -- | A conjunction of two goals.+  | ProveConj !(Goals asmp goal) !(Goals asmp goal)+    deriving Show++-- | Construct a goal that first assumes a collection of+--   assumptions and then states a goal.+assuming :: Monoid asmp => asmp -> Goals asmp goal -> Goals asmp goal+assuming as (Assuming bs g) = assuming (as <> bs) g+assuming as g = Assuming as g++-- | Construct a 'Goals' object from a collection of subgoals, all of+--   which are to be proved.  This yields 'Nothing' if the collection+--   of goals is empty, and otherwise builds a conjunction of all the+--   goals.  Note that there is no new sharing in the resulting structure.+proveAll :: Foldable t => t (Goals asmp goal) -> Maybe (Goals asmp goal)+proveAll = foldr f Nothing+ where+ f x Nothing  = Just $! x+ f x (Just y) = Just $! ProveConj x y++-- | Helper to conjoin two possibly trivial 'Goals' objects.+goalsConj :: Maybe (Goals asmp goal) -> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)+goalsConj Nothing y = y+goalsConj x Nothing = x+goalsConj (Just x) (Just y) = Just (ProveConj x y)++-- | Render the tree of goals as a list instead, duplicating+--   shared assumptions over each goal as necessary.+goalsToList :: Monoid asmp => Goals asmp goal -> [ProofGoal asmp goal]+goalsToList =+  getConst . traverseGoalsWithAssumptions+    (\as g -> Const [ProofGoal as g])++-- | Traverse the structure of a 'Goals' data structure.  The function for+--   visiting goals my decide to remove the goal from the structure.  If+--   no goals remain after the traversal, the resulting value will be a 'Nothing'.+--+--   In a call to 'traverseGoals assumeAction transformer goals', the+--   arguments are used as follows:+--+--   * 'traverseGoals' is an action is called every time we encounter+--     an 'Assuming' constructor.  The first argument is the original+--     sequence of assumptions.  The second argument is a continuation+--     action.  The result is a sequence of transformed assumptions+--     and the result of the continuation action.+--+--   * 'assumeAction' is a transformer action on goals.  Return+--     'Nothing' if you wish to remove the goal from the overall tree.+traverseGoals :: (Applicative f, Monoid asmp') =>+                 (forall a. asmp -> f a -> f (asmp', a))+              -> (goal -> f (Maybe goal'))+              -> Goals asmp goal+              -> f (Maybe (Goals asmp' goal'))+traverseGoals fas fgl = go+  where+  go (Prove gl)        = fmap Prove <$> fgl gl+  go (Assuming as gl)  = assuming' <$> fas as (go gl)+  go (ProveConj g1 g2) = goalsConj <$> go g1 <*> go g2++  assuming' (_, Nothing) = Nothing+  assuming' (as, Just g) = Just $! assuming as g+++traverseOnlyGoals :: (Applicative f, Monoid asmp) =>+  (goal -> f (Maybe goal')) ->+  Goals asmp goal -> f (Maybe (Goals asmp goal'))+traverseOnlyGoals f = traverseGoals (\as m -> (as,) <$> m) f++-- | Traverse a sequence of 'Goals' data structures.  See 'traverseGoals'+--   for an explanation of the action arguments.  The resulting sequence+--   may be shorter than the original if some 'Goals' become trivial.+traverseGoalsSeq :: (Applicative f, Monoid asmp') =>+  (forall a. asmp -> f a -> f (asmp', a)) ->+  (goal -> f (Maybe goal')) ->+  Seq (Goals asmp goal) -> f (Seq (Goals asmp' goal'))+traverseGoalsSeq fas fgl = go+  where+  go Seq.Empty      = pure Seq.Empty+  go (g Seq.:<| gs) = combine <$> traverseGoals fas fgl g <*> go gs++  combine Nothing gs  = gs+  combine (Just g) gs = g Seq.<| gs++-- | Visit every goal in a 'Goals' structure, remembering the sequence of+--   assumptions along the way to that goal.+traverseGoalsWithAssumptions :: (Applicative f, Monoid asmp) =>+  (asmp -> goal -> f (Maybe goal')) ->+  Goals asmp goal -> f (Maybe (Goals asmp goal'))++traverseGoalsWithAssumptions f gls =+   runReaderT (traverseGoals fas fgl gls) mempty+  where+  fas a m = (a,) <$> withReaderT (<> a) m+  fgl gl  = ReaderT $ \as -> f as gl+

@@ -52,6 +52,9 @@     -- ** Z3   , Z3OnlineBackend   , withZ3OnlineBackend+    -- ** Bitwuzla+  , BitwuzlaOnlineBackend+  , withBitwuzlaOnlineBackend     -- ** Boolector   , BoolectorOnlineBackend   , withBoolectorOnlineBackend@@ -92,6 +95,7 @@ import           What4.Protocol.SMTWriter as SMT import           What4.Protocol.SMTLib2 as SMT2 import           What4.SatResult+import qualified What4.Solver.Bitwuzla as Bitwuzla import qualified What4.Solver.Boolector as Boolector import qualified What4.Solver.CVC4 as CVC4 import qualified What4.Solver.CVC5 as CVC5@@ -272,6 +276,28 @@     do liftIO $ tryExtendConfig Z3.z3Options (getConfiguration sym)        action bak +type BitwuzlaOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Bitwuzla.Bitwuzla) scope st fs++-- | Do something with a Bitwuzla online backend.+--   The backend is only valid in the continuation.+--+--   The Bitwuzla configuration options will be automatically+--   installed into the backend configuration object.+--+--   > withBitwuzlaOnineBackend FloatRealRepr ng f'+withBitwuzlaOnlineBackend ::+  (MonadIO m, MonadMask m) =>+  B.ExprBuilder scope st fs ->+  UnsatFeatures ->+  ProblemFeatures ->+  (BitwuzlaOnlineBackend scope st fs -> m a) ->+  m a+withBitwuzlaOnlineBackend sym unsatFeat extraFeatures action =+  let feat = (SMT2.defaultFeatures Bitwuzla.Bitwuzla .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in+  withOnlineBackend sym feat $ \bak -> do+    liftIO $ tryExtendConfig Bitwuzla.bitwuzlaOptions (getConfiguration sym)+    action bak+ type BoolectorOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Boolector.Boolector) scope st fs  -- | Do something with a Boolector online backend.@@ -562,11 +588,6 @@         -- Add assertions to list        appendAssumptions as (assumptionStack bak)--  getPathCondition bak =-    do let sym = backendGetSym bak-       ps <- AS.collectAssumptions (assumptionStack bak)-       assumptionsPred sym ps    collectAssumptions bak =     AS.collectAssumptions (assumptionStack bak)

@@ -40,125 +40,11 @@   where  import           Control.Monad.Reader-import           Data.Functor.Const import           Data.Sequence (Seq) import qualified Data.Sequence as Seq-import           Data.Word---- | A proof goal consists of a collection of assumptions---   that were in scope when an assertion was made, together---   with the given assertion.-data ProofGoal asmp goal =-  ProofGoal-  { proofAssumptions :: asmp-  , proofGoal        :: goal-  }---- | A collection of goals, which can represent shared assumptions.-data Goals asmp goal =-    -- | Make an assumption that is in context for all the-    --   contained goals.-    Assuming asmp !(Goals asmp goal)--    -- | A proof obligation, to be proved in the context of-    --   all previously-made assumptions.-  | Prove goal--    -- | A conjunction of two goals.-  | ProveConj !(Goals asmp goal) !(Goals asmp goal)-    deriving Show---- | Construct a goal that first assumes a collection of---   assumptions and then states a goal.-assuming :: Monoid asmp => asmp -> Goals asmp goal -> Goals asmp goal-assuming as (Assuming bs g) = assuming (as <> bs) g-assuming as g = Assuming as g---- | Construct a 'Goals' object from a collection of subgoals, all of---   which are to be proved.  This yields 'Nothing' if the collection---   of goals is empty, and otherwise builds a conjunction of all the---   goals.  Note that there is no new sharing in the resulting structure.-proveAll :: Foldable t => t (Goals asmp goal) -> Maybe (Goals asmp goal)-proveAll = foldr f Nothing- where- f x Nothing  = Just $! x- f x (Just y) = Just $! ProveConj x y---- | Helper to conjoin two possibly trivial 'Goals' objects.-goalsConj :: Maybe (Goals asmp goal) -> Maybe (Goals asmp goal) -> Maybe (Goals asmp goal)-goalsConj Nothing y = y-goalsConj x Nothing = x-goalsConj (Just x) (Just y) = Just (ProveConj x y)---- | Render the tree of goals as a list instead, duplicating---   shared assumptions over each goal as necessary.-goalsToList :: Monoid asmp => Goals asmp goal -> [ProofGoal asmp goal]-goalsToList =-  getConst . traverseGoalsWithAssumptions-    (\as g -> Const [ProofGoal as g])---- | Traverse the structure of a 'Goals' data structure.  The function for---   visiting goals my decide to remove the goal from the structure.  If---   no goals remain after the traversal, the resulting value will be a 'Nothing'.------   In a call to 'traverseGoals assumeAction transformer goals', the---   arguments are used as follows:------   * 'traverseGoals' is an action is called every time we encounter---     an 'Assuming' constructor.  The first argument is the original---     sequence of assumptions.  The second argument is a continuation---     action.  The result is a sequence of transformed assumptions---     and the result of the continuation action.------   * 'assumeAction' is a transformer action on goals.  Return---     'Nothing' if you wish to remove the goal from the overall tree.-traverseGoals :: (Applicative f, Monoid asmp') =>-                 (forall a. asmp -> f a -> f (asmp', a))-              -> (goal -> f (Maybe goal'))-              -> Goals asmp goal-              -> f (Maybe (Goals asmp' goal'))-traverseGoals fas fgl = go-  where-  go (Prove gl)        = fmap Prove <$> fgl gl-  go (Assuming as gl)  = assuming' <$> fas as (go gl)-  go (ProveConj g1 g2) = goalsConj <$> go g1 <*> go g2--  assuming' (_, Nothing) = Nothing-  assuming' (as, Just g) = Just $! assuming as g---traverseOnlyGoals :: (Applicative f, Monoid asmp) =>-  (goal -> f (Maybe goal')) ->-  Goals asmp goal -> f (Maybe (Goals asmp goal'))-traverseOnlyGoals f = traverseGoals (\as m -> (as,) <$> m) f---- | Traverse a sequence of 'Goals' data structures.  See 'traverseGoals'---   for an explanation of the action arguments.  The resulting sequence---   may be shorter than the original if some 'Goals' become trivial.-traverseGoalsSeq :: (Applicative f, Monoid asmp') =>-  (forall a. asmp -> f a -> f (asmp', a)) ->-  (goal -> f (Maybe goal')) ->-  Seq (Goals asmp goal) -> f (Seq (Goals asmp' goal'))-traverseGoalsSeq fas fgl = go-  where-  go Seq.Empty      = pure Seq.Empty-  go (g Seq.:<| gs) = combine <$> traverseGoals fas fgl g <*> go gs--  combine Nothing gs  = gs-  combine (Just g) gs = g Seq.<| gs---- | Visit every goal in a 'Goals' structure, remembering the sequence of---   assumptions along the way to that goal.-traverseGoalsWithAssumptions :: (Applicative f, Monoid asmp) =>-  (asmp -> goal -> f (Maybe goal')) ->-  Goals asmp goal -> f (Maybe (Goals asmp goal'))--traverseGoalsWithAssumptions f gls =-   runReaderT (traverseGoals fas fgl gls) mempty-  where-  fas a m = (a,) <$> withReaderT (<> a) m-  fgl gl  = ReaderT $ \as -> f as gl+import           Data.Word (Word64) +import           Lang.Crucible.Backend.Goals  -- | A @FrameIdentifier@ is a value that identifies an --   an assumption frame.  These are expected to be unique

@@ -88,11 +88,6 @@   collectAssumptions bak =     AS.collectAssumptions (sbAssumptionStack bak) -  getPathCondition bak = do-    let sym = backendGetSym bak-    ps <- AS.collectAssumptions (sbAssumptionStack bak)-    assumptionsPred sym ps-   getProofObligations bak = do     AS.getProofObligations (sbAssumptionStack bak) 

@@ -32,6 +32,7 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}@@ -86,6 +87,8 @@     -- * Other stuff   , CtxRepr   , pattern KnownBV+  , ppTypeRepr+  , ppIntrinsicDefault      -- * Representation of Crucible types   , TypeRepr(..)@@ -98,6 +101,7 @@   , module What4.InterpretedFloatingPoint   ) where +import           Data.Functor.Identity (Identity(..)) import           Data.Hashable import           Data.Type.Equality import           GHC.TypeNats (Nat, KnownNat)@@ -107,6 +111,7 @@ import           Data.Parameterized.NatRepr import           Data.Parameterized.SymbolRepr import qualified Data.Parameterized.TH.GADT as U+import           Data.Parameterized.TraversableFC import           Prettyprinter  import           What4.BaseTypes@@ -455,8 +460,94 @@ instance Hashable (TypeRepr ty) where   hashWithSalt = $(U.structuralHashWithSalt [t|TypeRepr|] []) +-- Helper, not exported+prettyCtx ::+  Monad f =>+  -- | How to print 'IntrinsicRepr', see 'ppIntrinsicDefault'+  (forall s ctx'. SymbolRepr s -> CtxRepr ctx' -> f (Doc ann)) ->+  Ctx.Assignment TypeRepr ctx ->+  f (Doc ann)+-- The following specialization is used in the 'Pretty' instance and doesn't+-- need to generate code for (>>=), so it seems worth specializing for it.+{-# SPECIALIZE+  prettyCtx :: +    (forall s ctx. SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)) ->+    Ctx.Assignment TypeRepr tp ->+    Identity (Doc ann) #-}+prettyCtx f = fmap hsep . foldlMFC (\l t -> (:l) <$> ppTypeRepr f t) []++-- Helper, not exported+prettyBaseCtx :: Ctx.Assignment BaseTypeRepr ctx -> Doc ann+prettyBaseCtx = hsep . toListFC pretty++-- | Pretty-print a type.+--+-- Attempts to be consistent with the syntax provided in the @crucible-syntax@+-- package.+--+-- This is monadic mostly to allow failure, e.g., in case the caller finds an+-- intrinsic type that it doesn\'t expect.+ppTypeRepr ::+  Monad f =>+  -- | How to print 'IntrinsicRepr', see 'ppIntrinsicDefault'+  (forall s ctx. SymbolRepr s -> CtxRepr ctx -> f (Doc ann)) ->+  TypeRepr tp ->+  f (Doc ann)+-- The following specialization is used in the 'Pretty' instance and doesn't+-- need to generate code for (>>=), so it seems worth specializing for it.+{-# SPECIALIZE+  ppTypeRepr :: +    (forall s ctx. SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)) ->+    TypeRepr tp ->+    Identity (Doc ann) #-}+ppTypeRepr f x =+  case x of+    AnyRepr -> pure "Any"+    UnitRepr -> pure "Unit"+    BoolRepr -> pure "Bool"+    NatRepr -> pure "Nat"+    IntegerRepr -> pure "Integer"+    RealValRepr -> pure "RealVal"+    ComplexRealRepr -> pure "ComplexReal"+    BVRepr n -> pure (parens ("Bitvector" <+> viaShow n))+    IntrinsicRepr name tys -> f name tys+    RecursiveRepr name tys ->+      parens . (("Rec" <+> pretty (symbolRepr name)) <+>) <$> prettyCtx f tys+    FloatRepr fr -> pure (parens ("Float" <+> pretty fr))+    IEEEFloatRepr fr -> pure (parens ("IEEEFloat" <+> pretty fr))+    CharRepr -> pure "Char"+    StringRepr s -> pure (parens ("String" <+> pretty s))+    FunctionHandleRepr args ret ->+      (\args' ret' -> parens ("->" <+> args' <+> ret'))+      <$> prettyCtx f args+      <*> ppTypeRepr f ret+    MaybeRepr tp -> parens . ("Maybe" <+>) <$> ppTypeRepr f tp+    SequenceRepr s -> parens . ("Sequence" <+>) <$> ppTypeRepr f s+    VariantRepr variants -> parens . ("Variant" <+>) <$> prettyCtx f variants+    VectorRepr elems -> parens . ("Vector" <+>) <$> ppTypeRepr f elems+    StructRepr fields -> parens . ("Struct" <+>) <$> prettyCtx f fields+    ReferenceRepr t -> parens . ("Reference" <+>) <$> ppTypeRepr f t+    WordMapRepr n t -> pure (parens ("WorldMap" <+> viaShow n <+> pretty t))+    StringMapRepr s -> parens . ("StringMap" <+>) <$> ppTypeRepr f s+    SymbolicArrayRepr idxs a ->+      pure (parens ("SymbolicArray" <+> prettyBaseCtx idxs <+> pretty a))+    SymbolicStructRepr fields ->+      pure (parens ("SymbolicStruct" <+> prettyBaseCtx fields))++-- | A default printer for 'IntrinsicRepr', suitable for use with 'ppTypeRepr'.+ppIntrinsicDefault :: SymbolRepr s -> CtxRepr ctx -> Doc ann+ppIntrinsicDefault name tys = runIdentity (go name tys)+  where+  go :: forall ann s ctx. SymbolRepr s -> CtxRepr ctx -> Identity (Doc ann)+  go name' tys' =+    Identity $+      parens $+        pretty (symbolRepr name') <+> runIdentity (prettyCtx go tys')++-- | Pretty-print a type. Based on 'ppTypeRepr', using 'ppIntrinsicDefault'. instance Pretty (TypeRepr tp) where-  pretty = viaShow+  pretty =+    runIdentity . ppTypeRepr (\name tys -> Identity (ppIntrinsicDefault name tys))  instance Show (TypeRepr tp) where   showsPrec = $(U.structuralShowsPrec [t|TypeRepr|])@@ -479,6 +570,8 @@                   ) instance Eq (TypeRepr tp) where   x == y = isJust (testEquality x y)+instance EqF TypeRepr where+  eqF x y = isJust (testEquality x y)  instance OrdF TypeRepr where   compareF = $(U.structuralTypeOrd [t|TypeRepr|]

@@ -1,19 +1,95 @@ {-# LANGUAGE AllowAmbiguousTypes #-} module Main where +import Control.Lens ((^.)) import Data.List (isInfixOf)+import Data.Maybe (fromMaybe)  import Test.Hspec import Test.Tasty import Test.Tasty.Hspec (testSpec)+import qualified Test.Tasty.HUnit as TTH +import Data.Parameterized.Nonce (newIONonceGenerator)+import Data.Parameterized.Some (Some(Some))+import Lang.Crucible.Backend (SomeBackend(..))+import qualified Lang.Crucible.Backend as LCB+import Lang.Crucible.Backend.Simple (newSimpleBackend) import Lang.Crucible.Panic+import Lang.Crucible.Simulator.SimError (SimErrorReason(GenericSimError))+import What4.Expr (EmptyExprBuilderState(..))+import What4.Expr.Builder (newExprBuilder)+import qualified What4.Interface as W4I+import What4.FloatMode (FloatModeRepr(FloatIEEERepr))+import qualified What4.LabeledPred as W4L+import qualified What4.ProgramLoc as W4P  import qualified Panic as P  main :: IO () main =   defaultMain =<< panicTests++mkBackend :: IO (Some SomeBackend)+mkBackend = do+  Some nonceGen <- newIONonceGenerator+  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState nonceGen+  Some . SomeBackend <$> newSimpleBackend sym++assumePred ::+  LCB.IsSymBackend sym bak =>+  bak ->+  String ->+  W4I.Pred sym ->+  IO ()+assumePred bak msg p =+  LCB.addAssumption bak (LCB.GenericAssumption W4P.initializationLoc msg p)++backendTests :: TestTree+backendTests =+  testGroup+  "Backend"+  [ -- When popping an empty frame, the returned assumptions are just @True@+    TTH.testCase "push/pop nothing" $ do+      Some (SomeBackend bak) <- mkBackend+      asmps <- LCB.popAssumptionFrame bak =<< LCB.pushAssumptionFrame bak+      p <- LCB.assumptionsPred (LCB.backendGetSym bak) asmps+      Just True TTH.@=? W4I.asConstantPred p+    -- When popping a frame, the returned assumptions are the ones that were+    -- assumed in that frame+  , TTH.testCase "push/pop assumptions" $ do+      Some (SomeBackend bak) <- mkBackend+      let sym = LCB.backendGetSym bak+      a <- W4I.freshConstant sym (W4I.safeSymbol "a") W4I.BaseBoolRepr+      assumePred bak "assuming a" a+      frm <- LCB.pushAssumptionFrame bak+      b <- W4I.freshConstant sym (W4I.safeSymbol "b") W4I.BaseBoolRepr+      assumePred bak "assuming b" b+      p <- LCB.assumptionsPred sym =<< LCB.popAssumptionFrame bak frm+      pEqB <- W4I.eqPred sym p b+      Just True TTH.@=? W4I.asConstantPred pEqB+    -- When popping a frame, the returned obligations are the ones that were+    -- asserted in that frame.+  , TTH.testCase "push/pop obligations" $ do+      Some (SomeBackend bak) <- mkBackend+      let sym = LCB.backendGetSym bak+      a <- W4I.freshConstant sym (W4I.safeSymbol "a") W4I.BaseBoolRepr+      assumePred bak "assuming a" a+      b <- W4I.freshConstant sym (W4I.safeSymbol "b") W4I.BaseBoolRepr+      LCB.assert bak b (GenericSimError "asserting b")+      frm <- LCB.pushAssumptionFrame bak+      c <- W4I.freshConstant sym (W4I.safeSymbol "c") W4I.BaseBoolRepr+      assumePred bak "assuming c" c+      d <- W4I.freshConstant sym (W4I.safeSymbol "d") W4I.BaseBoolRepr+      LCB.assert bak c (GenericSimError "asserting d")+      (_asmps, mbGoals) <- LCB.popAssumptionFrameAndObligations bak frm+      [LCB.ProofGoal asmps gl] <- pure (fromMaybe [] (LCB.goalsToList <$> mbGoals))+      asmpsPred <- LCB.assumptionsPred sym asmps+      asmpsEqC <- W4I.eqPred sym c asmpsPred+      Just True TTH.@=? W4I.asConstantPred asmpsEqC+      goalEqD <- W4I.eqPred sym (gl ^. W4L.labeledPred) d+      Just True TTH.@=? W4I.asConstantPred goalEqD+  ]  panicTests :: IO TestTree panicTests =