{-|
Module      : Lang.Crucible.Backend.Assumptions
Copyright   : (c) Galois, Inc 2014-2024
License     : BSD3
Maintainer  : Langston Barrett <langston@galois.com>
-}

{-# 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 TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Lang.Crucible.Backend.Assumptions
  ( CrucibleAssumption(..)
  , CrucibleEvent(..)
  , CrucibleAssumptions(..)
  , Assumption
  , Assumptions

  , concretizeEvents
  , ppEvent
  , singleEvent
  , singleAssumption
  , trivialAssumption
  , ppAssumption
  , assumptionLoc
  , eventLoc
  , mergeAssumptions
  , assumptionPred
  , forgetAssumption
  , assumptionsPred
  , flattenAssumptions
  , assumptionsTopLevelLocs
  ) where


import           Control.Lens (Traversal, folded)
import           Data.Kind (Type)
import           Data.Functor.Identity
import           Data.Functor.Const
import qualified Data.Sequence as Seq
import           Data.Sequence (Seq)
import qualified Prettyprinter as PP

import           What4.Expr.Builder
import           What4.Interface
import           What4.ProgramLoc
import           What4.Expr (GroundValue, GroundValueWrapper(..))

import           Lang.Crucible.Simulator.SimError

type Assumption sym = CrucibleAssumption (SymExpr sym)
type Assumptions sym = CrucibleAssumptions (SymExpr sym)

-- | This type describes assumptions made at some point during program execution.
data CrucibleAssumption (e :: BaseType -> Type)
  = GenericAssumption ProgramLoc String (e BaseBoolType)
    -- ^ An unstructured description of the source of an assumption.

  | BranchCondition ProgramLoc (Maybe ProgramLoc) (e BaseBoolType)
    -- ^ This arose because we want to explore a specific path.
    -- The first location is the location of the branch predicate.
    -- The second one is the location of the branch target.

  | AssumingNoError SimError (e BaseBoolType)
    -- ^ An assumption justified by a proof of the impossibility of
    -- a certain simulator error.

-- | This type describes events we can track during program execution.
data CrucibleEvent (e :: BaseType -> Type) where
  -- | This event describes the creation of a symbolic variable.
  CreateVariableEvent ::
    ProgramLoc {- ^ location where the variable was created -} ->
    String {- ^ user-provided name for the variable -} ->
    BaseTypeRepr tp {- ^ type of the variable -} ->
    e tp {- ^ the variable expression -} ->
    CrucibleEvent e

  -- | This event describes reaching a particular program location.
  LocationReachedEvent ::
    ProgramLoc ->
    CrucibleEvent e

-- | Pretty print an event
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)

-- | Return the program location associated with an event
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

-- | Return the program location associated with an assumption
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

-- | Get the predicate associated with this assumption
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

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 ()))

-- | Check if an assumption is trivial (always true)
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

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

-- | This type tracks both logical assumptions and program events
--   that are relevant when evaluating proof obligations arising
--   from simulation.
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 {- ^ branch condition -} ->
    CrucibleAssumptions e {- ^ "then" assumptions -} ->
    CrucibleAssumptions e {- ^ "else" assumptions -} ->
    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

-- | Collect the program locations of all assumptions and
--   events that did not occur in the context of a symbolic branch.
--   These are locations that every program path represented by
--   this @CrucibleAssumptions@ structure must have passed through.
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{}   = []

-- | Compute the logical predicate corresponding to this collection of assumptions.
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)

-- | Given a ground evaluation function, compute a linear, ground-valued
--   sequence of events corresponding to this program run.
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

-- | Given a @CrucibleAssumptions@ structure, flatten all the muxed assumptions into
--   a flat sequence of assumptions that have been appropriately weakened.
--   Note, once these assumptions have been flattened, their order might no longer
--   strictly correspond to any concrete program run.
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')

-- | Merge the assumptions collected from the branches of a conditional.
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)

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
              ]
  where
    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)