{-# Language DeriveFunctor, RankNTypes, ConstraintKinds, TypeFamilies, ScopedTypeVariables, GADTs #-}
module Crux.Types where
import Data.Functor.Const
import Data.Parameterized.Map (MapF)
import Data.Sequence (Seq)
import Data.Text ( Text )
import Data.Void
import Prettyprinter
import What4.Expr (GroundValue,GroundValueWrapper)
import What4.Interface (Pred)
import What4.ProgramLoc
import Lang.Crucible.Backend
import Lang.Crucible.Simulator
import Lang.Crucible.Types
type SimCtxt personality sym p = SimContext (personality sym) sym p
type OverM personality sym ext a =
forall r args ret.
OverrideSim
(personality sym)
sym
ext
r
args
ret
a
type Fun personality sym ext args ret =
forall r.
OverrideSim
(personality sym)
sym
ext
r
args
ret
(RegValue sym ret)
data Result personality sym where
Result :: (ExecResult (personality sym) sym ext (RegEntry sym UnitType)) -> Result personality sym
data ProcessedGoals =
ProcessedGoals { ProcessedGoals -> Integer
totalProcessedGoals :: !Integer
, ProcessedGoals -> Integer
provedGoals :: !Integer
, ProcessedGoals -> Integer
disprovedGoals :: !Integer
, ProcessedGoals -> Integer
incompleteGoals :: !Integer
}
data ProofResult sym
= Proved [Either (Assumption sym) (Assertion sym)]
| NotProved (Doc Void) (Maybe (ModelView, [CrucibleEvent GroundValueWrapper])) [String]
type LPred sym = LabeledPred (Pred sym)
data ProvedGoals
= Branch ProvedGoals ProvedGoals
| NotProvedGoal
[CrucibleAssumption (Const ())]
SimError
(Doc Void)
[ProgramLoc]
(Maybe (ModelView, [CrucibleEvent GroundValueWrapper]))
[String]
| ProvedGoal
[CrucibleAssumption (Const ())]
SimError
[ProgramLoc]
Bool
data ProgramCompleteness
= ProgramComplete
| ProgramIncomplete
deriving (ProgramCompleteness -> ProgramCompleteness -> Bool
(ProgramCompleteness -> ProgramCompleteness -> Bool)
-> (ProgramCompleteness -> ProgramCompleteness -> Bool)
-> Eq ProgramCompleteness
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ProgramCompleteness -> ProgramCompleteness -> Bool
== :: ProgramCompleteness -> ProgramCompleteness -> Bool
$c/= :: ProgramCompleteness -> ProgramCompleteness -> Bool
/= :: ProgramCompleteness -> ProgramCompleteness -> Bool
Eq,Eq ProgramCompleteness
Eq ProgramCompleteness =>
(ProgramCompleteness -> ProgramCompleteness -> Ordering)
-> (ProgramCompleteness -> ProgramCompleteness -> Bool)
-> (ProgramCompleteness -> ProgramCompleteness -> Bool)
-> (ProgramCompleteness -> ProgramCompleteness -> Bool)
-> (ProgramCompleteness -> ProgramCompleteness -> Bool)
-> (ProgramCompleteness
-> ProgramCompleteness -> ProgramCompleteness)
-> (ProgramCompleteness
-> ProgramCompleteness -> ProgramCompleteness)
-> Ord ProgramCompleteness
ProgramCompleteness -> ProgramCompleteness -> Bool
ProgramCompleteness -> ProgramCompleteness -> Ordering
ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ProgramCompleteness -> ProgramCompleteness -> Ordering
compare :: ProgramCompleteness -> ProgramCompleteness -> Ordering
$c< :: ProgramCompleteness -> ProgramCompleteness -> Bool
< :: ProgramCompleteness -> ProgramCompleteness -> Bool
$c<= :: ProgramCompleteness -> ProgramCompleteness -> Bool
<= :: ProgramCompleteness -> ProgramCompleteness -> Bool
$c> :: ProgramCompleteness -> ProgramCompleteness -> Bool
> :: ProgramCompleteness -> ProgramCompleteness -> Bool
$c>= :: ProgramCompleteness -> ProgramCompleteness -> Bool
>= :: ProgramCompleteness -> ProgramCompleteness -> Bool
$cmax :: ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness
max :: ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness
$cmin :: ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness
min :: ProgramCompleteness -> ProgramCompleteness -> ProgramCompleteness
Ord,Int -> ProgramCompleteness -> ShowS
[ProgramCompleteness] -> ShowS
ProgramCompleteness -> String
(Int -> ProgramCompleteness -> ShowS)
-> (ProgramCompleteness -> String)
-> ([ProgramCompleteness] -> ShowS)
-> Show ProgramCompleteness
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProgramCompleteness -> ShowS
showsPrec :: Int -> ProgramCompleteness -> ShowS
$cshow :: ProgramCompleteness -> String
show :: ProgramCompleteness -> String
$cshowList :: [ProgramCompleteness] -> ShowS
showList :: [ProgramCompleteness] -> ShowS
Show)
data CruxSimulationResult =
CruxSimulationResult
{ CruxSimulationResult -> ProgramCompleteness
cruxSimResultCompleteness :: ProgramCompleteness
, CruxSimulationResult -> Seq (ProcessedGoals, ProvedGoals)
cruxSimResultGoals :: Seq (ProcessedGoals, ProvedGoals)
}
data Crux sym = CruxPersonality
newtype Vals ty = Vals [ Entry (GroundValue ty) ]
data Entry a = Entry { forall a. Entry a -> String
entryName :: String
, forall a. Entry a -> ProgramLoc
entryLoc :: ProgramLoc
, forall a. Entry a -> a
entryValue :: a
}
newtype ModelView = ModelView { ModelView -> MapF BaseTypeRepr Vals
modelVals :: MapF BaseTypeRepr Vals }
data SayWhat = SayWhat SayLevel Text Text
| SayMore SayWhat SayWhat
| SayNothing
data SayLevel = Noisily | Simply | OK | Warn | Fail deriving (SayLevel -> SayLevel -> Bool
(SayLevel -> SayLevel -> Bool)
-> (SayLevel -> SayLevel -> Bool) -> Eq SayLevel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SayLevel -> SayLevel -> Bool
== :: SayLevel -> SayLevel -> Bool
$c/= :: SayLevel -> SayLevel -> Bool
/= :: SayLevel -> SayLevel -> Bool
Eq, Eq SayLevel
Eq SayLevel =>
(SayLevel -> SayLevel -> Ordering)
-> (SayLevel -> SayLevel -> Bool)
-> (SayLevel -> SayLevel -> Bool)
-> (SayLevel -> SayLevel -> Bool)
-> (SayLevel -> SayLevel -> Bool)
-> (SayLevel -> SayLevel -> SayLevel)
-> (SayLevel -> SayLevel -> SayLevel)
-> Ord SayLevel
SayLevel -> SayLevel -> Bool
SayLevel -> SayLevel -> Ordering
SayLevel -> SayLevel -> SayLevel
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SayLevel -> SayLevel -> Ordering
compare :: SayLevel -> SayLevel -> Ordering
$c< :: SayLevel -> SayLevel -> Bool
< :: SayLevel -> SayLevel -> Bool
$c<= :: SayLevel -> SayLevel -> Bool
<= :: SayLevel -> SayLevel -> Bool
$c> :: SayLevel -> SayLevel -> Bool
> :: SayLevel -> SayLevel -> Bool
$c>= :: SayLevel -> SayLevel -> Bool
>= :: SayLevel -> SayLevel -> Bool
$cmax :: SayLevel -> SayLevel -> SayLevel
max :: SayLevel -> SayLevel -> SayLevel
$cmin :: SayLevel -> SayLevel -> SayLevel
min :: SayLevel -> SayLevel -> SayLevel
Ord)