diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/crucible.cabal b/crucible.cabal --- a/crucible.cabal +++ b/crucible.cabal @@ -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 diff --git a/src/Lang/Crucible/Backend.hs b/src/Lang/Crucible/Backend.hs --- a/src/Lang/Crucible/Backend.hs +++ b/src/Lang/Crucible/Backend.hs @@ -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) diff --git a/src/Lang/Crucible/Backend/Goals.hs b/src/Lang/Crucible/Backend/Goals.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Backend/Goals.hs @@ -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 + diff --git a/src/Lang/Crucible/Backend/Online.hs b/src/Lang/Crucible/Backend/Online.hs --- a/src/Lang/Crucible/Backend/Online.hs +++ b/src/Lang/Crucible/Backend/Online.hs @@ -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) diff --git a/src/Lang/Crucible/Backend/ProofGoals.hs b/src/Lang/Crucible/Backend/ProofGoals.hs --- a/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/src/Lang/Crucible/Backend/ProofGoals.hs @@ -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 diff --git a/src/Lang/Crucible/Backend/Simple.hs b/src/Lang/Crucible/Backend/Simple.hs --- a/src/Lang/Crucible/Backend/Simple.hs +++ b/src/Lang/Crucible/Backend/Simple.hs @@ -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) diff --git a/src/Lang/Crucible/Types.hs b/src/Lang/Crucible/Types.hs --- a/src/Lang/Crucible/Types.hs +++ b/src/Lang/Crucible/Types.hs @@ -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|] diff --git a/test/helpers/Main.hs b/test/helpers/Main.hs --- a/test/helpers/Main.hs +++ b/test/helpers/Main.hs @@ -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 =