{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
module Lang.Crucible.Backend
( IsSymBackend(..)
, IsSymInterface
, HasSymInterface(..)
, SomeBackend(..)
, CrucibleAssumption(..)
, CrucibleEvent(..)
, CrucibleAssumptions(..)
, Assumption
, Assertion
, Assumptions
, concretizeEvents
, ppEvent
, singleEvent
, singleAssumption
, trivialAssumption
, impossibleAssumption
, ppAssumption
, assumptionLoc
, eventLoc
, mergeAssumptions
, assumptionPred
, forgetAssumption
, assumptionsPred
, flattenAssumptions
, assumptionsTopLevelLocs
, ProofObligation
, ProofObligations
, AssumptionState
, assert
, LabeledPred(..)
, labeledPred
, labeledPredMsg
, AS.AssumptionStack
, AS.FrameIdentifier
, PG.ProofGoal(..)
, PG.Goals(..)
, PG.goalsToList
, AbortExecReason(..)
, abortExecBecause
, ppAbortExecReason
, throwUnsupported
, addAssertion
, addDurableAssertion
, addAssertionM
, addFailedAssertion
, assertIsInteger
, readPartExpr
, ppProofObligation
, backendOptions
, assertThenAssumeConfigOption
) where
import Control.Exception(Exception(..), throwIO)
import Control.Lens ((^.), Traversal, folded)
import Control.Monad
import Control.Monad.IO.Class
import Data.Kind (Type)
import Data.Foldable (toList)
import Data.Functor.Identity
import Data.Functor.Const
import qualified Data.Sequence as Seq
import Data.Sequence (Seq)
import qualified Prettyprinter as PP
import GHC.Stack
import What4.Concrete
import What4.Config
import What4.Interface
import What4.InterpretedFloatingPoint
import What4.LabeledPred
import What4.Partial
import What4.ProgramLoc
import What4.Expr (GroundValue, GroundValueWrapper(..))
import qualified Lang.Crucible.Backend.AssumptionStack as AS
import qualified Lang.Crucible.Backend.ProofGoals as PG
import Lang.Crucible.Simulator.SimError
data CrucibleAssumption (e :: BaseType -> Type)
= GenericAssumption ProgramLoc String (e BaseBoolType)
| BranchCondition ProgramLoc (Maybe ProgramLoc) (e BaseBoolType)
| AssumingNoError SimError (e BaseBoolType)
data CrucibleEvent (e :: BaseType -> Type) where
CreateVariableEvent ::
ProgramLoc ->
String ->
BaseTypeRepr tp ->
e tp ->
CrucibleEvent e
LocationReachedEvent ::
ProgramLoc ->
CrucibleEvent e
ppEvent :: IsExpr e => CrucibleEvent e -> PP.Doc ann
ppEvent :: forall (e :: BaseType -> Type) ann.
IsExpr e =>
CrucibleEvent e -> Doc ann
ppEvent (CreateVariableEvent ProgramLoc
loc String
nm BaseTypeRepr tp
_tpr e tp
v) =
Doc ann
"create var" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
nm Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> e tp -> Doc ann
forall (tp :: BaseType) ann. e tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr e tp
v Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
"at" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Position -> Doc ann
PP.pretty (ProgramLoc -> Position
plSourceLoc ProgramLoc
loc)
ppEvent (LocationReachedEvent ProgramLoc
loc) =
Doc ann
"reached" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Position -> Doc ann
PP.pretty (ProgramLoc -> Position
plSourceLoc ProgramLoc
loc) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
"in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> FunctionName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FunctionName -> Doc ann
PP.pretty (ProgramLoc -> FunctionName
plFunction ProgramLoc
loc)
eventLoc :: CrucibleEvent e -> ProgramLoc
eventLoc :: forall (e :: BaseType -> Type). CrucibleEvent e -> ProgramLoc
eventLoc (CreateVariableEvent ProgramLoc
loc String
_ BaseTypeRepr tp
_ e tp
_) = ProgramLoc
loc
eventLoc (LocationReachedEvent ProgramLoc
loc) = ProgramLoc
loc
assumptionLoc :: CrucibleAssumption e -> ProgramLoc
assumptionLoc :: forall (e :: BaseType -> Type). CrucibleAssumption e -> ProgramLoc
assumptionLoc CrucibleAssumption e
r =
case CrucibleAssumption e
r of
GenericAssumption ProgramLoc
l String
_ e BaseBoolType
_ -> ProgramLoc
l
BranchCondition ProgramLoc
l Maybe ProgramLoc
_ e BaseBoolType
_ -> ProgramLoc
l
AssumingNoError SimError
s e BaseBoolType
_ -> SimError -> ProgramLoc
simErrorLoc SimError
s
assumptionPred :: CrucibleAssumption e -> e BaseBoolType
assumptionPred :: forall (e :: BaseType -> Type).
CrucibleAssumption e -> e BaseBoolType
assumptionPred (AssumingNoError SimError
_ e BaseBoolType
p) = e BaseBoolType
p
assumptionPred (BranchCondition ProgramLoc
_ Maybe ProgramLoc
_ e BaseBoolType
p) = e BaseBoolType
p
assumptionPred (GenericAssumption ProgramLoc
_ String
_ e BaseBoolType
p) = e BaseBoolType
p
impossibleAssumption :: IsExpr e => CrucibleAssumption e -> Maybe AbortExecReason
impossibleAssumption :: forall (e :: BaseType -> Type).
IsExpr e =>
CrucibleAssumption e -> Maybe AbortExecReason
impossibleAssumption (AssumingNoError SimError
err e BaseBoolType
p)
| Just Bool
False <- e BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred e BaseBoolType
p = AbortExecReason -> Maybe AbortExecReason
forall a. a -> Maybe a
Just (SimError -> AbortExecReason
AssertionFailure SimError
err)
impossibleAssumption (BranchCondition ProgramLoc
loc Maybe ProgramLoc
_ e BaseBoolType
p)
| Just Bool
False <- e BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred e BaseBoolType
p = AbortExecReason -> Maybe AbortExecReason
forall a. a -> Maybe a
Just (ProgramLoc -> AbortExecReason
InfeasibleBranch ProgramLoc
loc)
impossibleAssumption (GenericAssumption ProgramLoc
loc String
_ e BaseBoolType
p)
| Just Bool
False <- e BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred e BaseBoolType
p = AbortExecReason -> Maybe AbortExecReason
forall a. a -> Maybe a
Just (ProgramLoc -> AbortExecReason
InfeasibleBranch ProgramLoc
loc)
impossibleAssumption CrucibleAssumption e
_ = Maybe AbortExecReason
forall a. Maybe a
Nothing
forgetAssumption :: CrucibleAssumption e -> CrucibleAssumption (Const ())
forgetAssumption :: forall (e :: BaseType -> Type).
CrucibleAssumption e -> CrucibleAssumption (Const ())
forgetAssumption = Identity (CrucibleAssumption (Const ()))
-> CrucibleAssumption (Const ())
forall a. Identity a -> a
runIdentity (Identity (CrucibleAssumption (Const ()))
-> CrucibleAssumption (Const ()))
-> (CrucibleAssumption e
-> Identity (CrucibleAssumption (Const ())))
-> CrucibleAssumption e
-> CrucibleAssumption (Const ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e BaseBoolType -> Identity (Const () BaseBoolType))
-> CrucibleAssumption e -> Identity (CrucibleAssumption (Const ()))
forall (e :: BaseType -> Type) (e' :: BaseType -> Type)
(f :: Type -> Type).
Applicative f =>
(e BaseBoolType -> f (e' BaseBoolType))
-> CrucibleAssumption e -> f (CrucibleAssumption e')
traverseAssumption (\e BaseBoolType
_ -> Const () BaseBoolType -> Identity (Const () BaseBoolType)
forall a. a -> Identity a
Identity (() -> Const () BaseBoolType
forall {k} a (b :: k). a -> Const a b
Const ()))
traverseAssumption :: Traversal (CrucibleAssumption e) (CrucibleAssumption e') (e BaseBoolType) (e' BaseBoolType)
traverseAssumption :: forall (e :: BaseType -> Type) (e' :: BaseType -> Type)
(f :: Type -> Type).
Applicative f =>
(e BaseBoolType -> f (e' BaseBoolType))
-> CrucibleAssumption e -> f (CrucibleAssumption e')
traverseAssumption e BaseBoolType -> f (e' BaseBoolType)
f = \case
GenericAssumption ProgramLoc
loc String
msg e BaseBoolType
p -> ProgramLoc -> String -> e' BaseBoolType -> CrucibleAssumption e'
forall (e :: BaseType -> Type).
ProgramLoc -> String -> e BaseBoolType -> CrucibleAssumption e
GenericAssumption ProgramLoc
loc String
msg (e' BaseBoolType -> CrucibleAssumption e')
-> f (e' BaseBoolType) -> f (CrucibleAssumption e')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e BaseBoolType -> f (e' BaseBoolType)
f e BaseBoolType
p
BranchCondition ProgramLoc
l Maybe ProgramLoc
t e BaseBoolType
p -> ProgramLoc
-> Maybe ProgramLoc -> e' BaseBoolType -> CrucibleAssumption e'
forall (e :: BaseType -> Type).
ProgramLoc
-> Maybe ProgramLoc -> e BaseBoolType -> CrucibleAssumption e
BranchCondition ProgramLoc
l Maybe ProgramLoc
t (e' BaseBoolType -> CrucibleAssumption e')
-> f (e' BaseBoolType) -> f (CrucibleAssumption e')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e BaseBoolType -> f (e' BaseBoolType)
f e BaseBoolType
p
AssumingNoError SimError
err e BaseBoolType
p -> SimError -> e' BaseBoolType -> CrucibleAssumption e'
forall (e :: BaseType -> Type).
SimError -> e BaseBoolType -> CrucibleAssumption e
AssumingNoError SimError
err (e' BaseBoolType -> CrucibleAssumption e')
-> f (e' BaseBoolType) -> f (CrucibleAssumption e')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e BaseBoolType -> f (e' BaseBoolType)
f e BaseBoolType
p
data CrucibleAssumptions (e :: BaseType -> Type) where
SingleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e
SingleEvent :: CrucibleEvent e -> CrucibleAssumptions e
ManyAssumptions :: Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
MergeAssumptions ::
e BaseBoolType ->
CrucibleAssumptions e ->
CrucibleAssumptions e ->
CrucibleAssumptions e
instance Semigroup (CrucibleAssumptions e) where
ManyAssumptions Seq (CrucibleAssumptions e)
xs <> :: CrucibleAssumptions e
-> CrucibleAssumptions e -> CrucibleAssumptions e
<> ManyAssumptions Seq (CrucibleAssumptions e)
ys = Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
forall (e :: BaseType -> Type).
Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
ManyAssumptions (Seq (CrucibleAssumptions e)
xs Seq (CrucibleAssumptions e)
-> Seq (CrucibleAssumptions e) -> Seq (CrucibleAssumptions e)
forall a. Semigroup a => a -> a -> a
<> Seq (CrucibleAssumptions e)
ys)
ManyAssumptions Seq (CrucibleAssumptions e)
xs <> CrucibleAssumptions e
y = Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
forall (e :: BaseType -> Type).
Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
ManyAssumptions (Seq (CrucibleAssumptions e)
xs Seq (CrucibleAssumptions e)
-> CrucibleAssumptions e -> Seq (CrucibleAssumptions e)
forall a. Seq a -> a -> Seq a
Seq.|> CrucibleAssumptions e
y)
CrucibleAssumptions e
x <> ManyAssumptions Seq (CrucibleAssumptions e)
ys = Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
forall (e :: BaseType -> Type).
Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
ManyAssumptions (CrucibleAssumptions e
x CrucibleAssumptions e
-> Seq (CrucibleAssumptions e) -> Seq (CrucibleAssumptions e)
forall a. a -> Seq a -> Seq a
Seq.<| Seq (CrucibleAssumptions e)
ys)
CrucibleAssumptions e
x <> CrucibleAssumptions e
y = Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
forall (e :: BaseType -> Type).
Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
ManyAssumptions ([CrucibleAssumptions e] -> Seq (CrucibleAssumptions e)
forall a. [a] -> Seq a
Seq.fromList [CrucibleAssumptions e
x,CrucibleAssumptions e
y])
instance Monoid (CrucibleAssumptions e) where
mempty :: CrucibleAssumptions e
mempty = Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
forall (e :: BaseType -> Type).
Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
ManyAssumptions Seq (CrucibleAssumptions e)
forall a. Monoid a => a
mempty
singleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e
singleAssumption :: forall (e :: BaseType -> Type).
CrucibleAssumption e -> CrucibleAssumptions e
singleAssumption CrucibleAssumption e
x = CrucibleAssumption e -> CrucibleAssumptions e
forall (e :: BaseType -> Type).
CrucibleAssumption e -> CrucibleAssumptions e
SingleAssumption CrucibleAssumption e
x
singleEvent :: CrucibleEvent e -> CrucibleAssumptions e
singleEvent :: forall (e :: BaseType -> Type).
CrucibleEvent e -> CrucibleAssumptions e
singleEvent CrucibleEvent e
x = CrucibleEvent e -> CrucibleAssumptions e
forall (e :: BaseType -> Type).
CrucibleEvent e -> CrucibleAssumptions e
SingleEvent CrucibleEvent e
x
assumptionsTopLevelLocs :: CrucibleAssumptions e -> [ProgramLoc]
assumptionsTopLevelLocs :: forall (e :: BaseType -> Type).
CrucibleAssumptions e -> [ProgramLoc]
assumptionsTopLevelLocs (SingleEvent CrucibleEvent e
e) = [CrucibleEvent e -> ProgramLoc
forall (e :: BaseType -> Type). CrucibleEvent e -> ProgramLoc
eventLoc CrucibleEvent e
e]
assumptionsTopLevelLocs (SingleAssumption CrucibleAssumption e
a) = [CrucibleAssumption e -> ProgramLoc
forall (e :: BaseType -> Type). CrucibleAssumption e -> ProgramLoc
assumptionLoc CrucibleAssumption e
a]
assumptionsTopLevelLocs (ManyAssumptions Seq (CrucibleAssumptions e)
as) = (CrucibleAssumptions e -> [ProgramLoc])
-> Seq (CrucibleAssumptions e) -> [ProgramLoc]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap CrucibleAssumptions e -> [ProgramLoc]
forall (e :: BaseType -> Type).
CrucibleAssumptions e -> [ProgramLoc]
assumptionsTopLevelLocs Seq (CrucibleAssumptions e)
as
assumptionsTopLevelLocs MergeAssumptions{} = []
assumptionsPred :: IsExprBuilder sym => sym -> Assumptions sym -> IO (Pred sym)
assumptionsPred :: forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
assumptionsPred sym
sym (SingleEvent CrucibleEvent (SymExpr sym)
_) =
SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym)
assumptionsPred sym
_sym (SingleAssumption CrucibleAssumption (SymExpr sym)
a) =
SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (CrucibleAssumption (SymExpr sym) -> SymExpr sym BaseBoolType
forall (e :: BaseType -> Type).
CrucibleAssumption e -> e BaseBoolType
assumptionPred CrucibleAssumption (SymExpr sym)
a)
assumptionsPred sym
sym (ManyAssumptions Seq (CrucibleAssumptions (SymExpr sym))
xs) =
sym
-> Fold (Seq (SymExpr sym BaseBoolType)) (SymExpr sym BaseBoolType)
-> Seq (SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType)
forall sym s.
IsExprBuilder sym =>
sym -> Fold s (Pred sym) -> s -> IO (Pred sym)
andAllOf sym
sym (SymExpr sym BaseBoolType -> f (SymExpr sym BaseBoolType))
-> Seq (SymExpr sym BaseBoolType)
-> f (Seq (SymExpr sym BaseBoolType))
Fold (Seq (SymExpr sym BaseBoolType)) (SymExpr sym BaseBoolType)
forall (f :: Type -> Type) a. Foldable f => IndexedFold Int (f a) a
IndexedFold
Int (Seq (SymExpr sym BaseBoolType)) (SymExpr sym BaseBoolType)
folded (Seq (SymExpr sym BaseBoolType) -> IO (SymExpr sym BaseBoolType))
-> IO (Seq (SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< (CrucibleAssumptions (SymExpr sym)
-> IO (SymExpr sym BaseBoolType))
-> Seq (CrucibleAssumptions (SymExpr sym))
-> IO (Seq (SymExpr sym BaseBoolType))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Seq a -> f (Seq b)
traverse (sym
-> CrucibleAssumptions (SymExpr sym)
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
assumptionsPred sym
sym) Seq (CrucibleAssumptions (SymExpr sym))
xs
assumptionsPred sym
sym (MergeAssumptions SymExpr sym BaseBoolType
c CrucibleAssumptions (SymExpr sym)
xs CrucibleAssumptions (SymExpr sym)
ys) =
do SymExpr sym BaseBoolType
xs' <- sym
-> CrucibleAssumptions (SymExpr sym)
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
assumptionsPred sym
sym CrucibleAssumptions (SymExpr sym)
xs
SymExpr sym BaseBoolType
ys' <- sym
-> CrucibleAssumptions (SymExpr sym)
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO (Pred sym)
assumptionsPred sym
sym CrucibleAssumptions (SymExpr sym)
ys
sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
sym SymExpr sym BaseBoolType
c SymExpr sym BaseBoolType
xs' SymExpr sym BaseBoolType
ys'
traverseEvent :: Applicative m =>
(forall tp. e tp -> m (e' tp)) ->
CrucibleEvent e -> m (CrucibleEvent e')
traverseEvent :: forall (m :: Type -> Type) (e :: BaseType -> Type)
(e' :: BaseType -> Type).
Applicative m =>
(forall (tp :: BaseType). e tp -> m (e' tp))
-> CrucibleEvent e -> m (CrucibleEvent e')
traverseEvent forall (tp :: BaseType). e tp -> m (e' tp)
f (CreateVariableEvent ProgramLoc
loc String
nm BaseTypeRepr tp
tpr e tp
v) = ProgramLoc
-> String -> BaseTypeRepr tp -> e' tp -> CrucibleEvent e'
forall (tp :: BaseType) (e :: BaseType -> Type).
ProgramLoc -> String -> BaseTypeRepr tp -> e tp -> CrucibleEvent e
CreateVariableEvent ProgramLoc
loc String
nm BaseTypeRepr tp
tpr (e' tp -> CrucibleEvent e') -> m (e' tp) -> m (CrucibleEvent e')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e tp -> m (e' tp)
forall (tp :: BaseType). e tp -> m (e' tp)
f e tp
v
traverseEvent forall (tp :: BaseType). e tp -> m (e' tp)
_ (LocationReachedEvent ProgramLoc
loc) = CrucibleEvent e' -> m (CrucibleEvent e')
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ProgramLoc -> CrucibleEvent e'
forall (e :: BaseType -> Type). ProgramLoc -> CrucibleEvent e
LocationReachedEvent ProgramLoc
loc)
concretizeEvents ::
IsExpr e =>
(forall tp. e tp -> IO (GroundValue tp)) ->
CrucibleAssumptions e ->
IO [CrucibleEvent GroundValueWrapper]
concretizeEvents :: forall (e :: BaseType -> Type).
IsExpr e =>
(forall (tp :: BaseType). e tp -> IO (GroundValue tp))
-> CrucibleAssumptions e -> IO [CrucibleEvent GroundValueWrapper]
concretizeEvents forall (tp :: BaseType). e tp -> IO (GroundValue tp)
f = CrucibleAssumptions e -> IO [CrucibleEvent GroundValueWrapper]
loop
where
loop :: CrucibleAssumptions e -> IO [CrucibleEvent GroundValueWrapper]
loop (SingleEvent CrucibleEvent e
e) =
do CrucibleEvent GroundValueWrapper
e' <- (forall (tp :: BaseType). e tp -> IO (GroundValueWrapper tp))
-> CrucibleEvent e -> IO (CrucibleEvent GroundValueWrapper)
forall (m :: Type -> Type) (e :: BaseType -> Type)
(e' :: BaseType -> Type).
Applicative m =>
(forall (tp :: BaseType). e tp -> m (e' tp))
-> CrucibleEvent e -> m (CrucibleEvent e')
traverseEvent (\e tp
v -> GroundValue tp -> GroundValueWrapper tp
forall (tp :: BaseType). GroundValue tp -> GroundValueWrapper tp
GVW (GroundValue tp -> GroundValueWrapper tp)
-> IO (GroundValue tp) -> IO (GroundValueWrapper tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e tp -> IO (GroundValue tp)
forall (tp :: BaseType). e tp -> IO (GroundValue tp)
f e tp
v) CrucibleEvent e
e
[CrucibleEvent GroundValueWrapper]
-> IO [CrucibleEvent GroundValueWrapper]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [CrucibleEvent GroundValueWrapper
e']
loop (SingleAssumption CrucibleAssumption e
_) = [CrucibleEvent GroundValueWrapper]
-> IO [CrucibleEvent GroundValueWrapper]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return []
loop (ManyAssumptions Seq (CrucibleAssumptions e)
as) = Seq [CrucibleEvent GroundValueWrapper]
-> [CrucibleEvent GroundValueWrapper]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat (Seq [CrucibleEvent GroundValueWrapper]
-> [CrucibleEvent GroundValueWrapper])
-> IO (Seq [CrucibleEvent GroundValueWrapper])
-> IO [CrucibleEvent GroundValueWrapper]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (CrucibleAssumptions e -> IO [CrucibleEvent GroundValueWrapper])
-> Seq (CrucibleAssumptions e)
-> IO (Seq [CrucibleEvent GroundValueWrapper])
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Seq a -> f (Seq b)
traverse CrucibleAssumptions e -> IO [CrucibleEvent GroundValueWrapper]
loop Seq (CrucibleAssumptions e)
as
loop (MergeAssumptions e BaseBoolType
p CrucibleAssumptions e
xs CrucibleAssumptions e
ys) =
do Bool
b <- e BaseBoolType -> IO (GroundValue BaseBoolType)
forall (tp :: BaseType). e tp -> IO (GroundValue tp)
f e BaseBoolType
p
if Bool
b then CrucibleAssumptions e -> IO [CrucibleEvent GroundValueWrapper]
loop CrucibleAssumptions e
xs else CrucibleAssumptions e -> IO [CrucibleEvent GroundValueWrapper]
loop CrucibleAssumptions e
ys
flattenAssumptions :: IsExprBuilder sym => sym -> Assumptions sym -> IO [Assumption sym]
flattenAssumptions :: forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO [Assumption sym]
flattenAssumptions sym
sym = Maybe (SymExpr sym BaseBoolType)
-> CrucibleAssumptions (SymExpr sym)
-> IO [CrucibleAssumption (SymExpr sym)]
loop Maybe (SymExpr sym BaseBoolType)
forall a. Maybe a
Nothing
where
loop :: Maybe (SymExpr sym BaseBoolType)
-> CrucibleAssumptions (SymExpr sym)
-> IO [CrucibleAssumption (SymExpr sym)]
loop Maybe (SymExpr sym BaseBoolType)
_mz (SingleEvent CrucibleEvent (SymExpr sym)
_) = [CrucibleAssumption (SymExpr sym)]
-> IO [CrucibleAssumption (SymExpr sym)]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return []
loop Maybe (SymExpr sym BaseBoolType)
mz (SingleAssumption CrucibleAssumption (SymExpr sym)
a) =
do CrucibleAssumption (SymExpr sym)
a' <- IO (CrucibleAssumption (SymExpr sym))
-> (SymExpr sym BaseBoolType
-> IO (CrucibleAssumption (SymExpr sym)))
-> Maybe (SymExpr sym BaseBoolType)
-> IO (CrucibleAssumption (SymExpr sym))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (CrucibleAssumption (SymExpr sym)
-> IO (CrucibleAssumption (SymExpr sym))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CrucibleAssumption (SymExpr sym)
a) (\SymExpr sym BaseBoolType
z -> (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> CrucibleAssumption (SymExpr sym)
-> IO (CrucibleAssumption (SymExpr sym))
forall (e :: BaseType -> Type) (e' :: BaseType -> Type)
(f :: Type -> Type).
Applicative f =>
(e BaseBoolType -> f (e' BaseBoolType))
-> CrucibleAssumption e -> f (CrucibleAssumption e')
traverseAssumption (sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
impliesPred sym
sym SymExpr sym BaseBoolType
z) CrucibleAssumption (SymExpr sym)
a) Maybe (SymExpr sym BaseBoolType)
mz
if CrucibleAssumption (SymExpr sym) -> Bool
forall (e :: BaseType -> Type).
IsExpr e =>
CrucibleAssumption e -> Bool
trivialAssumption CrucibleAssumption (SymExpr sym)
a' then [CrucibleAssumption (SymExpr sym)]
-> IO [CrucibleAssumption (SymExpr sym)]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [] else [CrucibleAssumption (SymExpr sym)]
-> IO [CrucibleAssumption (SymExpr sym)]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return [CrucibleAssumption (SymExpr sym)
a']
loop Maybe (SymExpr sym BaseBoolType)
mz (ManyAssumptions Seq (CrucibleAssumptions (SymExpr sym))
as) =
Seq [CrucibleAssumption (SymExpr sym)]
-> [CrucibleAssumption (SymExpr sym)]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat (Seq [CrucibleAssumption (SymExpr sym)]
-> [CrucibleAssumption (SymExpr sym)])
-> IO (Seq [CrucibleAssumption (SymExpr sym)])
-> IO [CrucibleAssumption (SymExpr sym)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (CrucibleAssumptions (SymExpr sym)
-> IO [CrucibleAssumption (SymExpr sym)])
-> Seq (CrucibleAssumptions (SymExpr sym))
-> IO (Seq [CrucibleAssumption (SymExpr sym)])
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Seq a -> f (Seq b)
traverse (Maybe (SymExpr sym BaseBoolType)
-> CrucibleAssumptions (SymExpr sym)
-> IO [CrucibleAssumption (SymExpr sym)]
loop Maybe (SymExpr sym BaseBoolType)
mz) Seq (CrucibleAssumptions (SymExpr sym))
as
loop Maybe (SymExpr sym BaseBoolType)
mz (MergeAssumptions SymExpr sym BaseBoolType
p CrucibleAssumptions (SymExpr sym)
xs CrucibleAssumptions (SymExpr sym)
ys) =
do SymExpr sym BaseBoolType
pnot <- sym -> SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym SymExpr sym BaseBoolType
p
SymExpr sym BaseBoolType
px <- IO (SymExpr sym BaseBoolType)
-> (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> Maybe (SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymExpr sym BaseBoolType
p) (sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym SymExpr sym BaseBoolType
p) Maybe (SymExpr sym BaseBoolType)
mz
SymExpr sym BaseBoolType
py <- IO (SymExpr sym BaseBoolType)
-> (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType))
-> Maybe (SymExpr sym BaseBoolType)
-> IO (SymExpr sym BaseBoolType)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SymExpr sym BaseBoolType -> IO (SymExpr sym BaseBoolType)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymExpr sym BaseBoolType
pnot) (sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym SymExpr sym BaseBoolType
pnot) Maybe (SymExpr sym BaseBoolType)
mz
[CrucibleAssumption (SymExpr sym)]
xs' <- Maybe (SymExpr sym BaseBoolType)
-> CrucibleAssumptions (SymExpr sym)
-> IO [CrucibleAssumption (SymExpr sym)]
loop (SymExpr sym BaseBoolType -> Maybe (SymExpr sym BaseBoolType)
forall a. a -> Maybe a
Just SymExpr sym BaseBoolType
px) CrucibleAssumptions (SymExpr sym)
xs
[CrucibleAssumption (SymExpr sym)]
ys' <- Maybe (SymExpr sym BaseBoolType)
-> CrucibleAssumptions (SymExpr sym)
-> IO [CrucibleAssumption (SymExpr sym)]
loop (SymExpr sym BaseBoolType -> Maybe (SymExpr sym BaseBoolType)
forall a. a -> Maybe a
Just SymExpr sym BaseBoolType
py) CrucibleAssumptions (SymExpr sym)
ys
[CrucibleAssumption (SymExpr sym)]
-> IO [CrucibleAssumption (SymExpr sym)]
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([CrucibleAssumption (SymExpr sym)]
xs' [CrucibleAssumption (SymExpr sym)]
-> [CrucibleAssumption (SymExpr sym)]
-> [CrucibleAssumption (SymExpr sym)]
forall a. Semigroup a => a -> a -> a
<> [CrucibleAssumption (SymExpr sym)]
ys')
mergeAssumptions ::
IsExprBuilder sym =>
sym ->
Pred sym ->
Assumptions sym ->
Assumptions sym ->
IO (Assumptions sym)
mergeAssumptions :: forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> Assumptions sym
-> Assumptions sym
-> IO (Assumptions sym)
mergeAssumptions sym
_sym Pred sym
p Assumptions sym
thens Assumptions sym
elses =
Assumptions sym -> IO (Assumptions sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym -> Assumptions sym -> Assumptions sym -> Assumptions sym
forall (e :: BaseType -> Type).
e BaseBoolType
-> CrucibleAssumptions e
-> CrucibleAssumptions e
-> CrucibleAssumptions e
MergeAssumptions Pred sym
p Assumptions sym
thens Assumptions sym
elses)
type Assertion sym = LabeledPred (Pred sym) SimError
type Assumption sym = CrucibleAssumption (SymExpr sym)
type Assumptions sym = CrucibleAssumptions (SymExpr sym)
type ProofObligation sym = AS.ProofGoal (Assumptions sym) (Assertion sym)
type ProofObligations sym = Maybe (AS.Goals (Assumptions sym) (Assertion sym))
type AssumptionState sym = PG.GoalCollector (Assumptions sym) (Assertion sym)
data AbortExecReason =
InfeasibleBranch ProgramLoc
| AssertionFailure SimError
| VariantOptionsExhausted ProgramLoc
| EarlyExit ProgramLoc
deriving Int -> AbortExecReason -> ShowS
[AbortExecReason] -> ShowS
AbortExecReason -> String
(Int -> AbortExecReason -> ShowS)
-> (AbortExecReason -> String)
-> ([AbortExecReason] -> ShowS)
-> Show AbortExecReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AbortExecReason -> ShowS
showsPrec :: Int -> AbortExecReason -> ShowS
$cshow :: AbortExecReason -> String
show :: AbortExecReason -> String
$cshowList :: [AbortExecReason] -> ShowS
showList :: [AbortExecReason] -> ShowS
Show
instance Exception AbortExecReason
ppAbortExecReason :: AbortExecReason -> PP.Doc ann
ppAbortExecReason :: forall ann. AbortExecReason -> Doc ann
ppAbortExecReason AbortExecReason
e =
case AbortExecReason
e of
InfeasibleBranch ProgramLoc
l -> ProgramLoc -> Doc ann -> Doc ann
forall ann. ProgramLoc -> Doc ann -> Doc ann
ppLocated ProgramLoc
l Doc ann
"Executing branch was discovered to be infeasible."
AssertionFailure SimError
err ->
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
[ Doc ann
"Abort due to assertion failure:"
, Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 (SimError -> Doc ann
forall ann. SimError -> Doc ann
ppSimError SimError
err)
]
VariantOptionsExhausted ProgramLoc
l -> ProgramLoc -> Doc ann -> Doc ann
forall ann. ProgramLoc -> Doc ann -> Doc ann
ppLocated ProgramLoc
l Doc ann
"Variant options exhausted."
EarlyExit ProgramLoc
l -> ProgramLoc -> Doc ann -> Doc ann
forall ann. ProgramLoc -> Doc ann -> Doc ann
ppLocated ProgramLoc
l Doc ann
"Program exited early."
ppAssumption :: (forall tp. e tp -> PP.Doc ann) -> CrucibleAssumption e -> PP.Doc ann
ppAssumption :: forall (e :: BaseType -> Type) ann.
(forall (tp :: BaseType). e tp -> Doc ann)
-> CrucibleAssumption e -> Doc ann
ppAssumption forall (tp :: BaseType). e tp -> Doc ann
ppDoc CrucibleAssumption e
e =
case CrucibleAssumption e
e of
GenericAssumption ProgramLoc
l String
msg e BaseBoolType
p ->
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep [ ProgramLoc -> Doc ann -> Doc ann
forall ann. ProgramLoc -> Doc ann -> Doc ann
ppLocated ProgramLoc
l (String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty String
msg)
, e BaseBoolType -> Doc ann
forall (tp :: BaseType). e tp -> Doc ann
ppDoc e BaseBoolType
p
]
BranchCondition ProgramLoc
l Maybe ProgramLoc
Nothing e BaseBoolType
p ->
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep [ Doc ann
"The branch in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> ProgramLoc -> Doc ann
forall ann. ProgramLoc -> Doc ann
ppFn ProgramLoc
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
"at" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> ProgramLoc -> Doc ann
forall ann. ProgramLoc -> Doc ann
ppLoc ProgramLoc
l
, e BaseBoolType -> Doc ann
forall (tp :: BaseType). e tp -> Doc ann
ppDoc e BaseBoolType
p
]
BranchCondition ProgramLoc
l (Just ProgramLoc
t) e BaseBoolType
p ->
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep [ Doc ann
"The branch in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> ProgramLoc -> Doc ann
forall ann. ProgramLoc -> Doc ann
ppFn ProgramLoc
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
"from" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> ProgramLoc -> Doc ann
forall ann. ProgramLoc -> Doc ann
ppLoc ProgramLoc
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
"to" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> ProgramLoc -> Doc ann
forall ann. ProgramLoc -> Doc ann
ppLoc ProgramLoc
t
, e BaseBoolType -> Doc ann
forall (tp :: BaseType). e tp -> Doc ann
ppDoc e BaseBoolType
p
]
AssumingNoError SimError
simErr e BaseBoolType
p ->
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep [ Doc ann
"Assuming the following error does not occur:"
, Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 (SimError -> Doc ann
forall ann. SimError -> Doc ann
ppSimError SimError
simErr)
, e BaseBoolType -> Doc ann
forall (tp :: BaseType). e tp -> Doc ann
ppDoc e BaseBoolType
p
]
throwUnsupported :: (IsExprBuilder sym, MonadIO m, HasCallStack) => sym -> String -> m a
throwUnsupported :: forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m, HasCallStack) =>
sym -> String -> m a
throwUnsupported sym
sym String
msg = IO a -> m a
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$
do ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
SimError -> IO a
forall e a. Exception e => e -> IO a
throwIO (SimError -> IO a) -> SimError -> IO a
forall a b. (a -> b) -> a -> b
$ ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc (SimErrorReason -> SimError) -> SimErrorReason -> SimError
forall a b. (a -> b) -> a -> b
$ CallStack -> String -> SimErrorReason
Unsupported CallStack
HasCallStack => CallStack
callStack String
msg
trivialAssumption :: IsExpr e => CrucibleAssumption e -> Bool
trivialAssumption :: forall (e :: BaseType -> Type).
IsExpr e =>
CrucibleAssumption e -> Bool
trivialAssumption CrucibleAssumption e
a = e BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred (CrucibleAssumption e -> e BaseBoolType
forall (e :: BaseType -> Type).
CrucibleAssumption e -> e BaseBoolType
assumptionPred CrucibleAssumption e
a) Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
ppLocated :: ProgramLoc -> PP.Doc ann -> PP.Doc ann
ppLocated :: forall ann. ProgramLoc -> Doc ann -> Doc ann
ppLocated ProgramLoc
l Doc ann
x = Doc ann
"in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> ProgramLoc -> Doc ann
forall ann. ProgramLoc -> Doc ann
ppFn ProgramLoc
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> ProgramLoc -> Doc ann
forall ann. ProgramLoc -> Doc ann
ppLoc ProgramLoc
l Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
x
ppFn :: ProgramLoc -> PP.Doc ann
ppFn :: forall ann. ProgramLoc -> Doc ann
ppFn ProgramLoc
l = FunctionName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FunctionName -> Doc ann
PP.pretty (ProgramLoc -> FunctionName
plFunction ProgramLoc
l)
ppLoc :: ProgramLoc -> PP.Doc ann
ppLoc :: forall ann. ProgramLoc -> Doc ann
ppLoc ProgramLoc
l = Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Position -> Doc ann
PP.pretty (ProgramLoc -> Position
plSourceLoc ProgramLoc
l)
type IsSymInterface sym =
( IsSymExprBuilder sym
, IsInterpretedFloatSymExprBuilder sym
)
data SomeBackend sym =
forall bak. IsSymBackend sym bak => SomeBackend bak
class HasSymInterface sym bak | bak -> sym where
backendGetSym :: bak -> sym
class (IsSymInterface sym, HasSymInterface sym bak) => IsSymBackend sym bak | bak -> sym where
pushAssumptionFrame :: bak -> IO AS.FrameIdentifier
popAssumptionFrame :: bak -> AS.FrameIdentifier -> IO (Assumptions sym)
popUntilAssumptionFrame :: bak -> AS.FrameIdentifier -> IO ()
popAssumptionFrameAndObligations ::
bak -> AS.FrameIdentifier -> IO (Assumptions sym, ProofObligations sym)
addAssumption :: bak -> Assumption sym -> IO ()
addAssumptions :: bak -> Assumptions sym -> IO ()
getPathCondition :: bak -> IO (Pred sym)
collectAssumptions :: bak -> IO (Assumptions sym)
addProofObligation :: bak -> Assertion sym -> IO ()
addProofObligation bak
bak Assertion sym
a =
case SymExpr sym BaseBoolType -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred (Assertion sym
a Assertion sym
-> Getting
(SymExpr sym BaseBoolType)
(Assertion sym)
(SymExpr sym BaseBoolType)
-> SymExpr sym BaseBoolType
forall s a. s -> Getting a s a -> a
^. Getting
(SymExpr sym BaseBoolType)
(Assertion sym)
(SymExpr sym BaseBoolType)
forall pred msg pred' (f :: Type -> Type).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
labeledPred) of
Just Bool
True -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
Maybe Bool
_ -> bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableProofObligation bak
bak Assertion sym
a
addDurableProofObligation :: bak -> Assertion sym -> IO ()
getProofObligations :: bak -> IO (ProofObligations sym)
clearProofObligations :: bak -> IO ()
saveAssumptionState :: bak -> IO (AssumptionState sym)
restoreAssumptionState :: bak -> AssumptionState sym -> IO ()
resetAssumptionState :: bak -> IO ()
resetAssumptionState bak
bak = bak -> AssumptionState sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> AssumptionState sym -> IO ()
restoreAssumptionState bak
bak AssumptionState sym
forall asmp goal. GoalCollector asmp goal
PG.emptyGoalCollector
assertThenAssumeConfigOption :: ConfigOption BaseBoolType
assertThenAssumeConfigOption :: ConfigOption BaseBoolType
assertThenAssumeConfigOption = BaseTypeRepr BaseBoolType -> String -> ConfigOption BaseBoolType
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr BaseBoolType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"assertThenAssume"
assertThenAssumeOption :: ConfigDesc
assertThenAssumeOption :: ConfigDesc
assertThenAssumeOption = ConfigOption BaseBoolType
-> OptionStyle BaseBoolType
-> Maybe (Doc Void)
-> Maybe (ConcreteVal BaseBoolType)
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
ConfigOption BaseBoolType
assertThenAssumeConfigOption
OptionStyle BaseBoolType
boolOptSty
(Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Assume a predicate after asserting it.")
(ConcreteVal BaseBoolType -> Maybe (ConcreteVal BaseBoolType)
forall a. a -> Maybe a
Just (Bool -> ConcreteVal BaseBoolType
ConcreteBool Bool
False))
backendOptions :: [ConfigDesc]
backendOptions :: [ConfigDesc]
backendOptions = [ConfigDesc
assertThenAssumeOption]
addAssertion ::
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addAssertion :: forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addAssertion bak
bak Assertion sym
a =
do bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addProofObligation bak
bak Assertion sym
a
bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
assumeAssertion bak
bak Assertion sym
a
addDurableAssertion :: IsSymBackend sym bak => bak -> Assertion sym -> IO ()
addDurableAssertion :: forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableAssertion bak
bak Assertion sym
a =
do bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addDurableProofObligation bak
bak Assertion sym
a
bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
assumeAssertion bak
bak Assertion sym
a
assumeAssertion :: IsSymBackend sym bak => bak -> Assertion sym -> IO ()
assumeAssertion :: forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
assumeAssertion bak
bak (LabeledPred Pred sym
p SimError
msg) =
do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
Bool
assert_then_assume_opt <- OptionSetting BaseBoolType -> IO Bool
forall (tp :: BaseType) a. Opt tp a => OptionSetting tp -> IO a
getOpt
(OptionSetting BaseBoolType -> IO Bool)
-> IO (OptionSetting BaseBoolType) -> IO Bool
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConfigOption BaseBoolType
-> Config -> IO (OptionSetting BaseBoolType)
forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
assertThenAssumeConfigOption (sym -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration sym
sym)
Bool -> IO () -> IO ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when Bool
assert_then_assume_opt (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
bak -> Assumption sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assumption sym -> IO ()
addAssumption bak
bak (SimError -> Pred sym -> Assumption sym
forall (e :: BaseType -> Type).
SimError -> e BaseBoolType -> CrucibleAssumption e
AssumingNoError SimError
msg Pred sym
p)
abortExecBecause :: AbortExecReason -> IO a
abortExecBecause :: forall a. AbortExecReason -> IO a
abortExecBecause AbortExecReason
err = AbortExecReason -> IO a
forall e a. Exception e => e -> IO a
throwIO AbortExecReason
err
assert ::
IsSymBackend sym bak =>
bak ->
Pred sym ->
SimErrorReason ->
IO ()
assert :: forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak Pred sym
p SimErrorReason
msg =
do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addAssertion bak
bak (Pred sym -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred Pred sym
p (ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc SimErrorReason
msg))
addFailedAssertion :: IsSymBackend sym bak => bak -> SimErrorReason -> IO a
addFailedAssertion :: forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak SimErrorReason
msg =
do let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
let err :: SimError
err = ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc SimErrorReason
msg
bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addProofObligation bak
bak (SymExpr sym BaseBoolType -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred (sym -> SymExpr sym BaseBoolType
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym) SimError
err)
AbortExecReason -> IO a
forall a. AbortExecReason -> IO a
abortExecBecause (SimError -> AbortExecReason
AssertionFailure SimError
err)
addAssertionM ::
IsSymBackend sym bak =>
bak ->
IO (Pred sym) ->
SimErrorReason ->
IO ()
addAssertionM :: forall sym bak.
IsSymBackend sym bak =>
bak -> IO (Pred sym) -> SimErrorReason -> IO ()
addAssertionM bak
bak IO (Pred sym)
pf SimErrorReason
msg = do
Pred sym
p <- IO (Pred sym)
pf
bak -> Pred sym -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Pred sym -> SimErrorReason -> IO ()
assert bak
bak Pred sym
p SimErrorReason
msg
assertIsInteger ::
IsSymBackend sym bak =>
bak ->
SymReal sym ->
SimErrorReason ->
IO ()
assertIsInteger :: forall sym bak.
IsSymBackend sym bak =>
bak -> SymReal sym -> SimErrorReason -> IO ()
assertIsInteger bak
bak SymReal sym
v SimErrorReason
msg = do
let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
bak -> IO (Pred sym) -> SimErrorReason -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> IO (Pred sym) -> SimErrorReason -> IO ()
addAssertionM bak
bak (sym -> SymReal sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymReal sym -> IO (Pred sym)
isInteger sym
sym SymReal sym
v) SimErrorReason
msg
readPartExpr ::
IsSymBackend sym bak =>
bak ->
PartExpr (Pred sym) v ->
SimErrorReason ->
IO v
readPartExpr :: forall sym bak v.
IsSymBackend sym bak =>
bak -> PartExpr (Pred sym) v -> SimErrorReason -> IO v
readPartExpr bak
bak PartExpr (SymExpr sym BaseBoolType) v
Unassigned SimErrorReason
msg = do
bak -> SimErrorReason -> IO v
forall sym bak a.
IsSymBackend sym bak =>
bak -> SimErrorReason -> IO a
addFailedAssertion bak
bak SimErrorReason
msg
readPartExpr bak
bak (PE SymExpr sym BaseBoolType
p v
v) SimErrorReason
msg = do
let sym :: sym
sym = bak -> sym
forall sym bak. HasSymInterface sym bak => bak -> sym
backendGetSym bak
bak
ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
bak -> Assertion sym -> IO ()
forall sym bak.
IsSymBackend sym bak =>
bak -> Assertion sym -> IO ()
addAssertion bak
bak (SymExpr sym BaseBoolType -> SimError -> Assertion sym
forall pred msg. pred -> msg -> LabeledPred pred msg
LabeledPred SymExpr sym BaseBoolType
p (ProgramLoc -> SimErrorReason -> SimError
SimError ProgramLoc
loc SimErrorReason
msg))
v -> IO v
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return v
v
ppProofObligation :: IsExprBuilder sym => sym -> ProofObligation sym -> IO (PP.Doc ann)
ppProofObligation :: forall sym ann.
IsExprBuilder sym =>
sym -> ProofObligation sym -> IO (Doc ann)
ppProofObligation sym
sym (AS.ProofGoal Assumptions sym
asmps Assertion sym
gl) =
do [CrucibleAssumption (SymExpr sym)]
as <- sym -> Assumptions sym -> IO [CrucibleAssumption (SymExpr sym)]
forall sym.
IsExprBuilder sym =>
sym -> Assumptions sym -> IO [Assumption sym]
flattenAssumptions sym
sym Assumptions sym
asmps
Doc ann -> IO (Doc ann)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Doc ann -> IO (Doc ann)) -> Doc ann -> IO (Doc ann)
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep
[ if [CrucibleAssumption (SymExpr sym)] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [CrucibleAssumption (SymExpr sym)]
as then Doc ann
forall a. Monoid a => a
mempty else
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat (Doc ann
"Assuming:" Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (CrucibleAssumption (SymExpr sym) -> [Doc ann])
-> [CrucibleAssumption (SymExpr sym)] -> [Doc ann]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap CrucibleAssumption (SymExpr sym) -> [Doc ann]
forall {e :: BaseType -> Type} {ann}.
IsExpr e =>
CrucibleAssumption e -> [Doc ann]
ppAsm ([CrucibleAssumption (SymExpr sym)]
-> [CrucibleAssumption (SymExpr sym)]
forall a. [a] -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList [CrucibleAssumption (SymExpr sym)]
as))
, Doc ann
"Prove:"
, Doc ann
ppGl
]
where
ppAsm :: CrucibleAssumption e -> [Doc ann]
ppAsm CrucibleAssumption e
asm
| Bool -> Bool
not (CrucibleAssumption e -> Bool
forall (e :: BaseType -> Type).
IsExpr e =>
CrucibleAssumption e -> Bool
trivialAssumption CrucibleAssumption e
asm) = [Doc ann
"* " Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
PP.<> Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.hang Int
2 ((forall (tp :: BaseType). e tp -> Doc ann)
-> CrucibleAssumption e -> Doc ann
forall (e :: BaseType -> Type) ann.
(forall (tp :: BaseType). e tp -> Doc ann)
-> CrucibleAssumption e -> Doc ann
ppAssumption e tp -> Doc ann
forall (tp :: BaseType). e tp -> Doc ann
forall (tp :: BaseType) ann. e tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr CrucibleAssumption e
asm)]
| Bool
otherwise = []
ppGl :: Doc ann
ppGl =
Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.indent Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep [SimError -> Doc ann
forall ann. SimError -> Doc ann
ppSimError (Assertion sym
glAssertion sym
-> Getting SimError (Assertion sym) SimError -> SimError
forall s a. s -> Getting a s a -> a
^.Getting SimError (Assertion sym) SimError
forall pred msg msg' (f :: Type -> Type).
Functor f =>
(msg -> f msg')
-> LabeledPred pred msg -> f (LabeledPred pred msg')
labeledPredMsg), SymExpr sym BaseBoolType -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr (Assertion sym
glAssertion sym
-> Getting
(SymExpr sym BaseBoolType)
(Assertion sym)
(SymExpr sym BaseBoolType)
-> SymExpr sym BaseBoolType
forall s a. s -> Getting a s a -> a
^.Getting
(SymExpr sym BaseBoolType)
(Assertion sym)
(SymExpr sym BaseBoolType)
forall pred msg pred' (f :: Type -> Type).
Functor f =>
(pred -> f pred')
-> LabeledPred pred msg -> f (LabeledPred pred' msg)
labeledPred)]