{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Analysis.Fixpoint (
forwardFixpoint,
forwardFixpoint',
ScopedReg(..),
lookupAbstractScopedRegValue,
lookupAbstractScopedRegValueByIndex,
Ignore(..),
Domain(..),
IterationStrategy(..),
Interpretation(..),
PointAbstraction(..),
RefSet,
emptyRefSet,
paGlobals,
paRegisters,
lookupAbstractRegValue,
modifyAbstractRegValue,
cfgWeakTopologicalOrdering,
Pointed(..),
pointed
) where
import Control.Applicative
import Control.Lens.Operators ( (^.), (%=), (.~), (&), (%~) )
import qualified Control.Monad.State.Strict as St
import qualified Data.Functor.Identity as I
import Data.Kind
import qualified Data.Set as S
import Text.Printf
import Prelude
import Data.Parameterized.Classes
import qualified Data.Parameterized.Context as PU
import qualified Data.Parameterized.Map as PM
import qualified Data.Parameterized.TraversableFC as PU
import Lang.Crucible.CFG.Core
import Lang.Crucible.CFG.Extension
import Lang.Crucible.Analysis.Fixpoint.Components
data WideningStrategy = WideningStrategy (Int -> Bool)
data WideningOperator dom = WideningOperator (forall tp . dom tp -> dom tp -> dom tp)
data IterationStrategy (dom :: CrucibleType -> Type) where
WTO :: IterationStrategy dom
WTOWidening :: (Int -> Bool) -> (forall tp . dom tp -> dom tp -> dom tp) -> IterationStrategy dom
Worklist :: IterationStrategy dom
data Domain (dom :: CrucibleType -> Type) =
Domain { forall (dom :: CrucibleType -> Type).
Domain dom -> forall (tp :: CrucibleType). dom tp
domTop :: forall tp . dom tp
, forall (dom :: CrucibleType -> Type).
Domain dom -> forall (tp :: CrucibleType). dom tp
domBottom :: forall tp . dom tp
, forall (dom :: CrucibleType -> Type).
Domain dom
-> forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
domJoin :: forall tp . dom tp -> dom tp -> dom tp
, forall (dom :: CrucibleType -> Type).
Domain dom -> IterationStrategy dom
domIter :: IterationStrategy dom
, forall (dom :: CrucibleType -> Type).
Domain dom -> forall (tp :: CrucibleType). dom tp -> dom tp -> Bool
domEq :: forall tp . dom tp -> dom tp -> Bool
}
data Interpretation ext (dom :: CrucibleType -> Type) =
Interpretation { forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
ScopedReg
-> TypeRepr tp
-> Expr ext ctx tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
interpExpr :: forall blocks ctx tp
. ScopedReg
-> TypeRepr tp
-> Expr ext ctx tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
, forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
ScopedReg
-> StmtExtension ext (Reg ctx) tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
interpExt :: forall blocks ctx tp
. ScopedReg
-> StmtExtension ext (Reg ctx) tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
, forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
(ret :: CrucibleType).
CtxRepr args
-> TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> dom (FunctionHandleType args ret)
-> Assignment dom args
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom ret)
interpCall :: forall blocks ctx args ret
. CtxRepr args
-> TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> dom (FunctionHandleType args ret)
-> PU.Assignment dom args
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom ret)
, forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
GlobalVar tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
interpReadGlobal :: forall blocks ctx tp
. GlobalVar tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
, forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
GlobalVar tp
-> Reg ctx tp
-> PointAbstraction blocks dom ctx
-> Maybe (PointAbstraction blocks dom ctx)
interpWriteGlobal :: forall blocks ctx tp
. GlobalVar tp
-> Reg ctx tp
-> PointAbstraction blocks dom ctx
-> Maybe (PointAbstraction blocks dom ctx)
, forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType).
Reg ctx BoolType
-> dom BoolType
-> JumpTarget blocks ctx
-> JumpTarget blocks ctx
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx),
Maybe (PointAbstraction blocks dom ctx))
interpBr :: forall blocks ctx
. Reg ctx BoolType
-> dom BoolType
-> JumpTarget blocks ctx
-> JumpTarget blocks ctx
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), Maybe (PointAbstraction blocks dom ctx))
, forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypeRepr tp
-> Reg ctx (MaybeType tp)
-> dom (MaybeType tp)
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp,
Maybe (PointAbstraction blocks dom ctx))
interpMaybe :: forall blocks ctx tp
. TypeRepr tp
-> Reg ctx (MaybeType tp)
-> dom (MaybeType tp)
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp, Maybe (PointAbstraction blocks dom ctx))
}
data PointAbstraction blocks dom ctx =
PointAbstraction { forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
PointAbstraction blocks dom ctx -> MapF GlobalVar dom
_paGlobals :: PM.MapF GlobalVar dom
, forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
PointAbstraction blocks dom ctx -> Assignment dom ctx
_paRegisters :: PU.Assignment dom ctx
, forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
PointAbstraction blocks dom ctx -> MapF (RefStmtId blocks) dom
_paRefs :: PM.MapF (RefStmtId blocks) dom
, forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
PointAbstraction blocks dom ctx -> Assignment (RefSet blocks) ctx
_paRegisterRefs :: PU.Assignment (RefSet blocks) ctx
}
newtype RefStmtId blocks tp = RefStmtId (StmtId blocks (ReferenceType tp))
data StmtId blocks tp = StmtId (TypeRepr tp) (Some (BlockID blocks)) Int
deriving (Int -> StmtId blocks tp -> ShowS
[StmtId blocks tp] -> ShowS
StmtId blocks tp -> String
(Int -> StmtId blocks tp -> ShowS)
-> (StmtId blocks tp -> String)
-> ([StmtId blocks tp] -> ShowS)
-> Show (StmtId blocks tp)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
Int -> StmtId blocks tp -> ShowS
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
[StmtId blocks tp] -> ShowS
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
StmtId blocks tp -> String
$cshowsPrec :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
Int -> StmtId blocks tp -> ShowS
showsPrec :: Int -> StmtId blocks tp -> ShowS
$cshow :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
StmtId blocks tp -> String
show :: StmtId blocks tp -> String
$cshowList :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
[StmtId blocks tp] -> ShowS
showList :: [StmtId blocks tp] -> ShowS
Show)
instance Eq (StmtId blocks tp) where
StmtId TypeRepr tp
tp1 Some (BlockID blocks)
bid1 Int
ix1 == :: StmtId blocks tp -> StmtId blocks tp -> Bool
== StmtId TypeRepr tp
tp2 Some (BlockID blocks)
bid2 Int
ix2 =
case TypeRepr tp -> TypeRepr tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr tp
tp1 TypeRepr tp
tp2 of
Maybe (tp :~: tp)
Nothing -> Bool
False
Just tp :~: tp
Refl -> (Some (BlockID blocks)
bid1, Int
ix1) (Some (BlockID blocks), Int)
-> (Some (BlockID blocks), Int) -> Bool
forall a. Eq a => a -> a -> Bool
== (Some (BlockID blocks)
bid2, Int
ix2)
instance Ord (StmtId blocks tp) where
compare :: StmtId blocks tp -> StmtId blocks tp -> Ordering
compare (StmtId TypeRepr tp
tp1 Some (BlockID blocks)
bid1 Int
ix1) (StmtId TypeRepr tp
tp2 Some (BlockID blocks)
bid2 Int
ix2) =
case OrderingF tp tp -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (TypeRepr tp -> TypeRepr tp -> OrderingF tp tp
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
TypeRepr x -> TypeRepr y -> OrderingF x y
compareF TypeRepr tp
tp1 TypeRepr tp
tp2) of
Ordering
LT -> Ordering
LT
Ordering
GT -> Ordering
GT
Ordering
EQ -> (Some (BlockID blocks), Int)
-> (Some (BlockID blocks), Int) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Some (BlockID blocks)
bid1, Int
ix1) (Some (BlockID blocks)
bid2, Int
ix2)
instance TestEquality (RefStmtId blocks) where
testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
RefStmtId blocks a -> RefStmtId blocks b -> Maybe (a :~: b)
testEquality (RefStmtId (StmtId TypeRepr (ReferenceType a)
tp1 (Some BlockID blocks x
bid1) Int
idx1)) (RefStmtId (StmtId TypeRepr (ReferenceType b)
tp2 (Some BlockID blocks x
bid2) Int
idx2)) = do
ReferenceType a :~: ReferenceType b
Refl <- TypeRepr (ReferenceType a)
-> TypeRepr (ReferenceType b)
-> Maybe (ReferenceType a :~: ReferenceType b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr (ReferenceType a)
tp1 TypeRepr (ReferenceType b)
tp2
x :~: x
Refl <- BlockID blocks x -> BlockID blocks x -> Maybe (x :~: x)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
BlockID blocks a -> BlockID blocks b -> Maybe (a :~: b)
testEquality BlockID blocks x
bid1 BlockID blocks x
bid2
case Int
idx1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
idx2 of
Bool
True -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((a :~: b) -> Maybe (a :~: b)) -> (a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$! a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
Bool
False -> Maybe (a :~: b)
forall a. Maybe a
Nothing
instance OrdF (RefStmtId blocks) where
compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
RefStmtId blocks x -> RefStmtId blocks y -> OrderingF x y
compareF (RefStmtId (StmtId TypeRepr (ReferenceType x)
tp1 (Some BlockID blocks x
bid1) Int
idx1)) (RefStmtId (StmtId TypeRepr (ReferenceType y)
tp2 (Some BlockID blocks x
bid2) Int
idx2)) =
case TypeRepr (ReferenceType x)
-> TypeRepr (ReferenceType y)
-> OrderingF (ReferenceType x) (ReferenceType y)
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
TypeRepr x -> TypeRepr y -> OrderingF x y
compareF TypeRepr (ReferenceType x)
tp1 TypeRepr (ReferenceType y)
tp2 of
OrderingF (ReferenceType x) (ReferenceType y)
EQF ->
case BlockID blocks x -> BlockID blocks x -> OrderingF x x
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType).
BlockID blocks x -> BlockID blocks y -> OrderingF x y
compareF BlockID blocks x
bid1 BlockID blocks x
bid2 of
OrderingF x x
EQF ->
case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
idx1 Int
idx2 of
Ordering
LT -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
Ordering
GT -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
Ordering
EQ -> OrderingF x x
OrderingF x y
forall {k} (x :: k). OrderingF x x
EQF
OrderingF x x
LTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
OrderingF x x
GTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
OrderingF (ReferenceType x) (ReferenceType y)
LTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
OrderingF (ReferenceType x) (ReferenceType y)
GTF -> OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
newtype RefSet blocks tp = RefSet (S.Set (StmtId blocks tp))
emptyRefSet :: RefSet blocks tp
emptyRefSet :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
RefSet blocks tp
emptyRefSet = Set (StmtId blocks tp) -> RefSet blocks tp
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
Set (StmtId blocks tp) -> RefSet blocks tp
RefSet Set (StmtId blocks tp)
forall a. Set a
S.empty
unionRefSets :: RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp
unionRefSets :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp
unionRefSets (RefSet Set (StmtId blocks tp)
s1) (RefSet Set (StmtId blocks tp)
s2) = Set (StmtId blocks tp) -> RefSet blocks tp
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
Set (StmtId blocks tp) -> RefSet blocks tp
RefSet (Set (StmtId blocks tp)
s1 Set (StmtId blocks tp)
-> Set (StmtId blocks tp) -> Set (StmtId blocks tp)
forall a. Ord a => Set a -> Set a -> Set a
`S.union` Set (StmtId blocks tp)
s2)
instance ShowF dom => Show (PointAbstraction blocks dom ctx) where
show :: PointAbstraction blocks dom ctx -> String
show PointAbstraction blocks dom ctx
pa = Assignment dom ctx -> String
forall a. Show a => a -> String
show (PointAbstraction blocks dom ctx -> Assignment dom ctx
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
PointAbstraction blocks dom ctx -> Assignment dom ctx
_paRegisters PointAbstraction blocks dom ctx
pa)
instance ShowF dom => ShowF (PointAbstraction blocks dom)
lookupAbstractRegValue :: PointAbstraction blocks dom ctx -> Reg ctx tp -> dom tp
lookupAbstractRegValue :: forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType)
(tp :: CrucibleType).
PointAbstraction blocks dom ctx -> Reg ctx tp -> dom tp
lookupAbstractRegValue PointAbstraction blocks dom ctx
pa (Reg Index ctx tp
ix) = (PointAbstraction blocks dom ctx
pa PointAbstraction blocks dom ctx
-> Getting
(Assignment dom ctx)
(PointAbstraction blocks dom ctx)
(Assignment dom ctx)
-> Assignment dom ctx
forall s a. s -> Getting a s a -> a
^. Getting
(Assignment dom ctx)
(PointAbstraction blocks dom ctx)
(Assignment dom ctx)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Functor f =>
(Assignment dom ctx -> f (Assignment dom ctx))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRegisters) Assignment dom ctx -> Index ctx tp -> dom tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
PU.! Index ctx tp
ix
modifyAbstractRegValue :: PointAbstraction blocks dom ctx
-> Reg ctx tp
-> (dom tp -> dom tp)
-> PointAbstraction blocks dom ctx
modifyAbstractRegValue :: forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType)
(tp :: CrucibleType).
PointAbstraction blocks dom ctx
-> Reg ctx tp
-> (dom tp -> dom tp)
-> PointAbstraction blocks dom ctx
modifyAbstractRegValue PointAbstraction blocks dom ctx
pa (Reg Index ctx tp
ix) dom tp -> dom tp
f = PointAbstraction blocks dom ctx
pa PointAbstraction blocks dom ctx
-> (PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx)
-> PointAbstraction blocks dom ctx
forall a b. a -> (a -> b) -> b
& (Assignment dom ctx -> Identity (Assignment dom ctx))
-> PointAbstraction blocks dom ctx
-> Identity (PointAbstraction blocks dom ctx)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Functor f =>
(Assignment dom ctx -> f (Assignment dom ctx))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRegisters ((Assignment dom ctx -> Identity (Assignment dom ctx))
-> PointAbstraction blocks dom ctx
-> Identity (PointAbstraction blocks dom ctx))
-> ((dom tp -> Identity (dom tp))
-> Assignment dom ctx -> Identity (Assignment dom ctx))
-> (dom tp -> Identity (dom tp))
-> PointAbstraction blocks dom ctx
-> Identity (PointAbstraction blocks dom ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IndexF (Assignment dom ctx) tp
-> Traversal'
(Assignment dom ctx) (IxValueF (Assignment dom ctx) tp)
forall k m (x :: k).
IxedF k m =>
IndexF m x -> Traversal' m (IxValueF m x)
forall (x :: CrucibleType).
IndexF (Assignment dom ctx) x
-> Traversal'
(Assignment dom ctx) (IxValueF (Assignment dom ctx) x)
ixF IndexF (Assignment dom ctx) tp
Index ctx tp
ix ((dom tp -> Identity (dom tp))
-> PointAbstraction blocks dom ctx
-> Identity (PointAbstraction blocks dom ctx))
-> (dom tp -> dom tp)
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ dom tp -> dom tp
f
data FunctionAbstraction (dom :: CrucibleType -> Type) blocks ret =
FunctionAbstraction { forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
FunctionAbstraction dom blocks ret
-> Assignment (PointAbstraction blocks dom) blocks
_faEntryRegs :: PU.Assignment (PointAbstraction blocks dom) blocks
, forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
FunctionAbstraction dom blocks ret
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
_faExitRegs :: PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
, forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
FunctionAbstraction dom blocks ret -> dom ret
_faRet :: dom ret
}
data IterationState (dom :: CrucibleType -> Type) blocks ret =
IterationState { forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
IterationState dom blocks ret -> FunctionAbstraction dom blocks ret
_isFuncAbstr :: FunctionAbstraction dom blocks ret
, forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
IterationState dom blocks ret -> dom ret
_isRetAbstr :: dom ret
, forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
IterationState dom blocks ret -> Set (Some (BlockID blocks))
_processedOnce :: S.Set (Some (BlockID blocks))
}
newtype M (dom :: CrucibleType -> Type) blocks ret a = M { forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a.
M dom blocks ret a -> State (IterationState dom blocks ret) a
runM :: St.State (IterationState dom blocks ret) a }
deriving (St.MonadState (IterationState dom blocks ret), Applicative (M dom blocks ret)
Applicative (M dom blocks ret) =>
(forall a b.
M dom blocks ret a
-> (a -> M dom blocks ret b) -> M dom blocks ret b)
-> (forall a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret b)
-> (forall a. a -> M dom blocks ret a)
-> Monad (M dom blocks ret)
forall a. a -> M dom blocks ret a
forall a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret b
forall a b.
M dom blocks ret a
-> (a -> M dom blocks ret b) -> M dom blocks ret b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
Applicative (M dom blocks ret)
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a.
a -> M dom blocks ret a
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret b
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
M dom blocks ret a
-> (a -> M dom blocks ret b) -> M dom blocks ret b
$c>>= :: forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
M dom blocks ret a
-> (a -> M dom blocks ret b) -> M dom blocks ret b
>>= :: forall a b.
M dom blocks ret a
-> (a -> M dom blocks ret b) -> M dom blocks ret b
$c>> :: forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret b
>> :: forall a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret b
$creturn :: forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a.
a -> M dom blocks ret a
return :: forall a. a -> M dom blocks ret a
Monad, Functor (M dom blocks ret)
Functor (M dom blocks ret) =>
(forall a. a -> M dom blocks ret a)
-> (forall a b.
M dom blocks ret (a -> b)
-> M dom blocks ret a -> M dom blocks ret b)
-> (forall a b c.
(a -> b -> c)
-> M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret c)
-> (forall a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret b)
-> (forall a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret a)
-> Applicative (M dom blocks ret)
forall a. a -> M dom blocks ret a
forall a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret a
forall a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret b
forall a b.
M dom blocks ret (a -> b)
-> M dom blocks ret a -> M dom blocks ret b
forall a b c.
(a -> b -> c)
-> M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
Functor (M dom blocks ret)
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a.
a -> M dom blocks ret a
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret a
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret b
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
M dom blocks ret (a -> b)
-> M dom blocks ret a -> M dom blocks ret b
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b c.
(a -> b -> c)
-> M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret c
$cpure :: forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a.
a -> M dom blocks ret a
pure :: forall a. a -> M dom blocks ret a
$c<*> :: forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
M dom blocks ret (a -> b)
-> M dom blocks ret a -> M dom blocks ret b
<*> :: forall a b.
M dom blocks ret (a -> b)
-> M dom blocks ret a -> M dom blocks ret b
$cliftA2 :: forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b c.
(a -> b -> c)
-> M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret c
liftA2 :: forall a b c.
(a -> b -> c)
-> M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret c
$c*> :: forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret b
*> :: forall a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret b
$c<* :: forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret a
<* :: forall a b.
M dom blocks ret a -> M dom blocks ret b -> M dom blocks ret a
Applicative, (forall a b. (a -> b) -> M dom blocks ret a -> M dom blocks ret b)
-> (forall a b. a -> M dom blocks ret b -> M dom blocks ret a)
-> Functor (M dom blocks ret)
forall a b. a -> M dom blocks ret b -> M dom blocks ret a
forall a b. (a -> b) -> M dom blocks ret a -> M dom blocks ret b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
a -> M dom blocks ret b -> M dom blocks ret a
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
(a -> b) -> M dom blocks ret a -> M dom blocks ret b
$cfmap :: forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
(a -> b) -> M dom blocks ret a -> M dom blocks ret b
fmap :: forall a b. (a -> b) -> M dom blocks ret a -> M dom blocks ret b
$c<$ :: forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a b.
a -> M dom blocks ret b -> M dom blocks ret a
<$ :: forall a b. a -> M dom blocks ret b -> M dom blocks ret a
Functor)
extendRegisters :: dom tp -> PointAbstraction blocks dom ctx -> PointAbstraction blocks dom (ctx ::> tp)
extendRegisters :: forall (dom :: CrucibleType -> Type) (tp :: CrucibleType)
(blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
dom tp
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom (ctx ::> tp)
extendRegisters dom tp
domVal PointAbstraction blocks dom ctx
pa =
PointAbstraction blocks dom ctx
pa { _paRegisters = PU.extend (_paRegisters pa) domVal
, _paRegisterRefs = PU.extend (_paRegisterRefs pa) emptyRefSet
}
joinPointAbstractions :: forall blocks (dom :: CrucibleType -> Type) ctx
. Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions :: forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions Domain dom
dom = (forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp)
-> (forall (tp :: CrucibleType).
RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp)
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
(forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp)
-> (forall (tp :: CrucibleType).
RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp)
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
zipPAWith (Domain dom
-> forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
forall (dom :: CrucibleType -> Type).
Domain dom
-> forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
domJoin Domain dom
dom) RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp
forall (tp :: CrucibleType).
RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp
unionRefSets
zipPAWith :: forall blocks (dom :: CrucibleType -> Type) ctx
. (forall tp . dom tp -> dom tp -> dom tp)
-> (forall tp . RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp)
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
zipPAWith :: forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
(forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp)
-> (forall (tp :: CrucibleType).
RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp)
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
zipPAWith forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
domOp forall (tp :: CrucibleType).
RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp
refSetOp PointAbstraction blocks dom ctx
pa1 PointAbstraction blocks dom ctx
pa2 =
PointAbstraction blocks dom ctx
pa1 { _paRegisters = PU.zipWith domOp (pa1 ^. paRegisters) (pa2 ^. paRegisters)
, _paGlobals = I.runIdentity $ do
PM.mergeWithKeyM (\GlobalVar tp
_ dom tp
a dom tp
b -> Maybe (dom tp) -> Identity (Maybe (dom tp))
forall a. a -> Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (dom tp -> Maybe (dom tp)
forall a. a -> Maybe a
Just (dom tp -> dom tp -> dom tp
forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
domOp dom tp
a dom tp
b))) return return (pa1 ^. paGlobals) (pa2 ^. paGlobals)
, _paRefs = I.runIdentity $ do
PM.mergeWithKeyM (\RefStmtId blocks tp
_ dom tp
a dom tp
b -> Maybe (dom tp) -> Identity (Maybe (dom tp))
forall a. a -> Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (dom tp -> Maybe (dom tp)
forall a. a -> Maybe a
Just (dom tp -> dom tp -> dom tp
forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
domOp dom tp
a dom tp
b))) return return (pa1 ^. paRefs) (pa2 ^. paRefs)
, _paRegisterRefs = PU.zipWith refSetOp (pa1 ^. paRegisterRefs) (pa2 ^. paRegisterRefs)
}
equalPointAbstractions :: forall blocks (dom :: CrucibleType -> Type) ctx
. Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> Bool
equalPointAbstractions :: forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> Bool
equalPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx
pa1 PointAbstraction blocks dom ctx
pa2 =
(forall (x :: CrucibleType). Bool -> Ignore Bool x -> Bool)
-> forall (x :: Ctx CrucibleType).
Bool -> Assignment (Ignore Bool) x -> Bool
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). b -> f x -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: CrucibleType -> Type) b.
(forall (x :: CrucibleType). b -> f x -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment f x -> b
PU.foldlFC (\Bool
a (Ignore Bool
b) -> Bool
a Bool -> Bool -> Bool
&& Bool
b) Bool
True Assignment (Ignore Bool) ctx
pointwiseEqualRegs Bool -> Bool -> Bool
&& Bool
equalGlobals
where
checkGlobal :: Pair GlobalVar dom -> Pair GlobalVar dom -> Bool
checkGlobal (PM.Pair GlobalVar tp
gv1 dom tp
d1) (PM.Pair GlobalVar tp
gv2 dom tp
d2) =
case GlobalVar tp -> GlobalVar tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
GlobalVar a -> GlobalVar b -> Maybe (a :~: b)
PM.testEquality GlobalVar tp
gv1 GlobalVar tp
gv2 of
Just tp :~: tp
Refl -> Domain dom -> forall (tp :: CrucibleType). dom tp -> dom tp -> Bool
forall (dom :: CrucibleType -> Type).
Domain dom -> forall (tp :: CrucibleType). dom tp -> dom tp -> Bool
domEq Domain dom
dom dom tp
d1 dom tp
dom tp
d2
Maybe (tp :~: tp)
Nothing -> Bool
False
equalGlobals :: Bool
equalGlobals = [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Pair GlobalVar dom -> Pair GlobalVar dom -> Bool)
-> [Pair GlobalVar dom] -> [Pair GlobalVar dom] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Pair GlobalVar dom -> Pair GlobalVar dom -> Bool
checkGlobal (MapF GlobalVar dom -> [Pair GlobalVar dom]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Pair k2 a]
PM.toList (PointAbstraction blocks dom ctx
pa1 PointAbstraction blocks dom ctx
-> Getting
(MapF GlobalVar dom)
(PointAbstraction blocks dom ctx)
(MapF GlobalVar dom)
-> MapF GlobalVar dom
forall s a. s -> Getting a s a -> a
^. Getting
(MapF GlobalVar dom)
(PointAbstraction blocks dom ctx)
(MapF GlobalVar dom)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
Functor f =>
(MapF GlobalVar dom -> f (MapF GlobalVar dom))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paGlobals)) (MapF GlobalVar dom -> [Pair GlobalVar dom]
forall {k1} (k2 :: k1 -> Type) (a :: k1 -> Type).
MapF k2 a -> [Pair k2 a]
PM.toList (PointAbstraction blocks dom ctx
pa2 PointAbstraction blocks dom ctx
-> Getting
(MapF GlobalVar dom)
(PointAbstraction blocks dom ctx)
(MapF GlobalVar dom)
-> MapF GlobalVar dom
forall s a. s -> Getting a s a -> a
^. Getting
(MapF GlobalVar dom)
(PointAbstraction blocks dom ctx)
(MapF GlobalVar dom)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
Functor f =>
(MapF GlobalVar dom -> f (MapF GlobalVar dom))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paGlobals))
pointwiseEqualRegs :: Assignment (Ignore Bool) ctx
pointwiseEqualRegs = (forall (x :: CrucibleType). dom x -> dom x -> Ignore Bool x)
-> Assignment dom ctx
-> Assignment dom ctx
-> Assignment (Ignore Bool) ctx
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
(a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
PU.zipWith (\dom x
a dom x
b -> Bool -> Ignore Bool x
forall k a (b :: k). a -> Ignore a b
Ignore (Domain dom -> forall (tp :: CrucibleType). dom tp -> dom tp -> Bool
forall (dom :: CrucibleType -> Type).
Domain dom -> forall (tp :: CrucibleType). dom tp -> dom tp -> Bool
domEq Domain dom
dom dom x
a dom x
b)) (PointAbstraction blocks dom ctx
pa1 PointAbstraction blocks dom ctx
-> Getting
(Assignment dom ctx)
(PointAbstraction blocks dom ctx)
(Assignment dom ctx)
-> Assignment dom ctx
forall s a. s -> Getting a s a -> a
^. Getting
(Assignment dom ctx)
(PointAbstraction blocks dom ctx)
(Assignment dom ctx)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Functor f =>
(Assignment dom ctx -> f (Assignment dom ctx))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRegisters) (PointAbstraction blocks dom ctx
pa2 PointAbstraction blocks dom ctx
-> Getting
(Assignment dom ctx)
(PointAbstraction blocks dom ctx)
(Assignment dom ctx)
-> Assignment dom ctx
forall s a. s -> Getting a s a -> a
^. Getting
(Assignment dom ctx)
(PointAbstraction blocks dom ctx)
(Assignment dom ctx)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Functor f =>
(Assignment dom ctx -> f (Assignment dom ctx))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRegisters)
data ScopedReg where
ScopedReg :: BlockID blocks ctx1 -> Reg ctx2 tp -> ScopedReg
instance Show ScopedReg where
show :: ScopedReg -> String
show (ScopedReg BlockID blocks ctx1
b Reg ctx2 tp
r) = String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"\"%s:%s\"" (BlockID blocks ctx1 -> String
forall a. Show a => a -> String
show BlockID blocks ctx1
b) (Reg ctx2 tp -> String
forall a. Show a => a -> String
show Reg ctx2 tp
r)
instance Eq ScopedReg where
ScopedReg
sr1 == :: ScopedReg -> ScopedReg -> Bool
== ScopedReg
sr2 =
ScopedReg -> (Int, Int)
scopedRegIndexVals ScopedReg
sr1 (Int, Int) -> (Int, Int) -> Bool
forall a. Eq a => a -> a -> Bool
== ScopedReg -> (Int, Int)
scopedRegIndexVals ScopedReg
sr2
instance Ord ScopedReg where
ScopedReg
sr1 compare :: ScopedReg -> ScopedReg -> Ordering
`compare` ScopedReg
sr2 =
ScopedReg -> (Int, Int)
scopedRegIndexVals ScopedReg
sr1 (Int, Int) -> (Int, Int) -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` ScopedReg -> (Int, Int)
scopedRegIndexVals ScopedReg
sr2
scopedRegIndexVals :: ScopedReg -> (Int, Int)
scopedRegIndexVals :: ScopedReg -> (Int, Int)
scopedRegIndexVals (ScopedReg BlockID blocks ctx1
b Reg ctx2 tp
r) = (BlockID blocks ctx1 -> Int
forall (ctx :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID ctx tp -> Int
blockIDIndexVal BlockID blocks ctx1
b, Reg ctx2 tp -> Int
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Int
regIndexVal Reg ctx2 tp
r)
blockIDIndexVal :: BlockID ctx tp -> Int
blockIDIndexVal :: forall (ctx :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID ctx tp -> Int
blockIDIndexVal = Index ctx tp -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
PU.indexVal (Index ctx tp -> Int)
-> (BlockID ctx tp -> Index ctx tp) -> BlockID ctx tp -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlockID ctx tp -> Index ctx tp
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex
regIndexVal :: Reg ctx tp -> Int
regIndexVal :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Int
regIndexVal = Index ctx tp -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
PU.indexVal (Index ctx tp -> Int)
-> (Reg ctx tp -> Index ctx tp) -> Reg ctx tp -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reg ctx tp -> Index ctx tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
regIndex
lookupAbstractScopedRegValue :: ScopedReg
-> PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> Maybe (Some dom)
lookupAbstractScopedRegValue :: forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type).
ScopedReg
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> Maybe (Some dom)
lookupAbstractScopedRegValue ScopedReg
sr Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
ass =
(Int, Int)
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> Maybe (Some dom)
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type).
(Int, Int)
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> Maybe (Some dom)
lookupAbstractScopedRegValueByIndex (ScopedReg -> (Int, Int)
scopedRegIndexVals ScopedReg
sr) Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
ass
lookupAbstractScopedRegValueByIndex :: (Int, Int)
-> PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> Maybe (Some dom)
lookupAbstractScopedRegValueByIndex :: forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type).
(Int, Int)
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> Maybe (Some dom)
lookupAbstractScopedRegValueByIndex (Int
b, Int
r) Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
ass = do
Some (Ignore (Some PointAbstraction blocks dom x
pa)) <- Int
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> Maybe (Some (Ignore (Some (PointAbstraction blocks dom))))
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Int -> Assignment f ctx -> Maybe (Some f)
assignmentLookupByIndex Int
b Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
ass
Int -> Assignment dom x -> Maybe (Some dom)
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Int -> Assignment f ctx -> Maybe (Some f)
assignmentLookupByIndex Int
r (PointAbstraction blocks dom x
pa PointAbstraction blocks dom x
-> Getting
(Assignment dom x)
(PointAbstraction blocks dom x)
(Assignment dom x)
-> Assignment dom x
forall s a. s -> Getting a s a -> a
^. Getting
(Assignment dom x)
(PointAbstraction blocks dom x)
(Assignment dom x)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Functor f =>
(Assignment dom ctx -> f (Assignment dom ctx))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRegisters)
assignmentLookupByIndex :: Int -> PU.Assignment f ctx -> Maybe (Some f)
assignmentLookupByIndex :: forall {k} (f :: k -> Type) (ctx :: Ctx k).
Int -> Assignment f ctx -> Maybe (Some f)
assignmentLookupByIndex Int
i Assignment f ctx
ass =
let sz :: Size ctx
sz = Assignment f ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
PU.size Assignment f ctx
ass
in case Int -> Size ctx -> Maybe (Some (Index ctx))
forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
PU.intIndex Int
i Size ctx
sz of
Maybe (Some (Index ctx))
Nothing -> Maybe (Some f)
forall a. Maybe a
Nothing
Just (Some Index ctx x
ix) -> Some f -> Maybe (Some f)
forall a. a -> Maybe a
Just (f x -> Some f
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Assignment f ctx
ass Assignment f ctx -> Index ctx x -> f x
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
PU.! Index ctx x
ix))
transfer :: forall ext dom blocks ret ctx
. Domain dom
-> Interpretation ext dom
-> TypeRepr ret
-> Block ext blocks ret ctx
-> PointAbstraction blocks dom ctx
-> M dom blocks ret (S.Set (Some (BlockID blocks)))
transfer :: forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Domain dom
-> Interpretation ext dom
-> TypeRepr ret
-> Block ext blocks ret ctx
-> PointAbstraction blocks dom ctx
-> M dom blocks ret (Set (Some (BlockID blocks)))
transfer Domain dom
dom Interpretation ext dom
interp TypeRepr ret
retRepr Block ext blocks ret ctx
blk = Size ctx
-> StmtSeq ext blocks ret ctx
-> PointAbstraction blocks dom ctx
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
Size ctx'
-> StmtSeq ext blocks ret ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferSeq Size ctx
blockInputSize (Block ext blocks ret ctx -> StmtSeq ext blocks ret ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> StmtSeq ext blocks ret ctx
_blockStmts Block ext blocks ret ctx
blk)
where
blockInputSize :: PU.Size ctx
blockInputSize :: Size ctx
blockInputSize = Assignment TypeRepr ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
PU.size (Assignment TypeRepr ctx -> Size ctx)
-> Assignment TypeRepr ctx -> Size ctx
forall a b. (a -> b) -> a -> b
$ Block ext blocks ret ctx -> Assignment TypeRepr ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs Block ext blocks ret ctx
blk
lookupReg :: Reg ctx tp -> PointAbstraction blocks dom ctx -> dom tp
lookupReg = (PointAbstraction blocks dom ctx -> Reg ctx tp -> dom tp)
-> Reg ctx tp -> PointAbstraction blocks dom ctx -> dom tp
forall a b c. (a -> b -> c) -> b -> a -> c
flip PointAbstraction blocks dom ctx -> Reg ctx tp -> dom tp
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType)
(tp :: CrucibleType).
PointAbstraction blocks dom ctx -> Reg ctx tp -> dom tp
lookupAbstractRegValue
transferSeq :: forall ctx'
. PU.Size ctx'
-> StmtSeq ext blocks ret ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (S.Set (Some (BlockID blocks)))
transferSeq :: forall (ctx' :: Ctx CrucibleType).
Size ctx'
-> StmtSeq ext blocks ret ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferSeq Size ctx'
sz (ConsStmt ProgramLoc
_loc Stmt ext ctx' ctx'
stmt StmtSeq ext blocks ret ctx'
ss) =
Size ctx'
-> StmtSeq ext blocks ret ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
Size ctx'
-> StmtSeq ext blocks ret ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferSeq (Size ctx' -> Stmt ext ctx' ctx' -> Size ctx'
forall (ctx :: Ctx CrucibleType) ext (ctx' :: Ctx CrucibleType).
Size ctx -> Stmt ext ctx ctx' -> Size ctx'
nextStmtHeight Size ctx'
sz Stmt ext ctx' ctx'
stmt) StmtSeq ext blocks ret ctx'
ss (PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks))))
-> (PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx')
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Size ctx'
-> Stmt ext ctx' ctx'
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
forall (ctx1 :: Ctx CrucibleType) (ctx2 :: Ctx CrucibleType).
Size ctx1
-> Stmt ext ctx1 ctx2
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx2
transferStmt Size ctx'
sz Stmt ext ctx' ctx'
stmt
transferSeq Size ctx'
_sz (TermStmt ProgramLoc
_loc TermStmt blocks ret ctx'
term) = TermStmt blocks ret ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
TermStmt blocks ret ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferTerm TermStmt blocks ret ctx'
term
transferStmt :: forall ctx1 ctx2
. PU.Size ctx1
-> Stmt ext ctx1 ctx2
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx2
transferStmt :: forall (ctx1 :: Ctx CrucibleType) (ctx2 :: Ctx CrucibleType).
Size ctx1
-> Stmt ext ctx1 ctx2
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx2
transferStmt Size ctx1
sz Stmt ext ctx1 ctx2
s PointAbstraction blocks dom ctx1
assignment =
case Stmt ext ctx1 ctx2
s of
SetReg (TypeRepr tp
tp :: TypeRepr tp) Expr ext ctx1 tp
ex ->
let reg :: Reg (ctx1 ::> tp) tp
reg :: Reg (ctx1 '::> tp) tp
reg = Index (ctx1 '::> tp) tp -> Reg (ctx1 '::> tp) tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Index ctx tp -> Reg ctx tp
Reg (Size ctx1 -> Index (ctx1 '::> tp) tp
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
PU.nextIndex Size ctx1
sz)
scopedReg :: ScopedReg
scopedReg = BlockID blocks ctx -> Reg (ctx1 '::> tp) tp -> ScopedReg
forall (blocks :: Ctx (Ctx CrucibleType))
(ctx1 :: Ctx CrucibleType) (ctx2 :: Ctx CrucibleType)
(tp :: CrucibleType).
BlockID blocks ctx1 -> Reg ctx2 tp -> ScopedReg
ScopedReg (Block ext blocks ret ctx -> BlockID blocks ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret ctx
blk) Reg (ctx1 '::> tp) tp
reg
(Maybe (PointAbstraction blocks dom ctx1)
assignment', dom tp
absVal) = Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
ScopedReg
-> TypeRepr tp
-> Expr ext ctx tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
ScopedReg
-> TypeRepr tp
-> Expr ext ctx tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
interpExpr Interpretation ext dom
interp ScopedReg
scopedReg TypeRepr tp
tp Expr ext ctx1 tp
ex PointAbstraction blocks dom ctx1
assignment
assignment'' :: PointAbstraction blocks dom ctx1
assignment'' = PointAbstraction blocks dom ctx1
-> (PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1)
-> Maybe (PointAbstraction blocks dom ctx1)
-> PointAbstraction blocks dom ctx1
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PointAbstraction blocks dom ctx1
assignment (Domain dom
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx1
assignment) Maybe (PointAbstraction blocks dom ctx1)
assignment'
in dom tp
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom (ctx1 '::> tp)
forall (dom :: CrucibleType -> Type) (tp :: CrucibleType)
(blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
dom tp
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom (ctx ::> tp)
extendRegisters dom tp
absVal PointAbstraction blocks dom ctx1
assignment''
ExtendAssign (StmtExtension ext (Reg ctx1) tp
estmt :: StmtExtension ext (Reg ctx1) tp) ->
let reg :: Reg (ctx1 ::> tp) tp
reg :: Reg (ctx1 '::> tp) tp
reg = Index (ctx1 '::> tp) tp -> Reg (ctx1 '::> tp) tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Index ctx tp -> Reg ctx tp
Reg (Size ctx1 -> Index (ctx1 '::> tp) tp
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
PU.nextIndex Size ctx1
sz)
scopedReg :: ScopedReg
scopedReg = BlockID blocks ctx -> Reg (ctx1 '::> tp) tp -> ScopedReg
forall (blocks :: Ctx (Ctx CrucibleType))
(ctx1 :: Ctx CrucibleType) (ctx2 :: Ctx CrucibleType)
(tp :: CrucibleType).
BlockID blocks ctx1 -> Reg ctx2 tp -> ScopedReg
ScopedReg (Block ext blocks ret ctx -> BlockID blocks ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret ctx
blk) Reg (ctx1 '::> tp) tp
reg
(Maybe (PointAbstraction blocks dom ctx1)
assignment', dom tp
absVal) = Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
ScopedReg
-> StmtExtension ext (Reg ctx) tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
ScopedReg
-> StmtExtension ext (Reg ctx) tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
interpExt Interpretation ext dom
interp ScopedReg
scopedReg StmtExtension ext (Reg ctx1) tp
estmt PointAbstraction blocks dom ctx1
assignment
assignment'' :: PointAbstraction blocks dom ctx1
assignment'' = PointAbstraction blocks dom ctx1
-> (PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1)
-> Maybe (PointAbstraction blocks dom ctx1)
-> PointAbstraction blocks dom ctx1
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PointAbstraction blocks dom ctx1
assignment (Domain dom
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx1
assignment) Maybe (PointAbstraction blocks dom ctx1)
assignment'
in dom tp
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom (ctx1 '::> tp)
forall (dom :: CrucibleType -> Type) (tp :: CrucibleType)
(blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
dom tp
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom (ctx ::> tp)
extendRegisters dom tp
absVal PointAbstraction blocks dom ctx1
assignment''
Print Reg ctx1 (StringType Unicode)
_reg -> PointAbstraction blocks dom ctx1
PointAbstraction blocks dom ctx2
assignment
CallHandle TypeRepr ret
retTp Reg ctx1 (FunctionHandleType args ret)
funcHandle CtxRepr args
argTps Assignment (Reg ctx1) args
actuals ->
let actualsAbstractions :: Assignment dom args
actualsAbstractions = (forall (x :: CrucibleType). TypeRepr x -> Reg ctx1 x -> dom x)
-> CtxRepr args
-> Assignment (Reg ctx1) args
-> Assignment dom args
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
(a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
PU.zipWith (\TypeRepr x
_ Reg ctx1 x
act -> Reg ctx1 x -> PointAbstraction blocks dom ctx1 -> dom x
forall {ctx :: Ctx CrucibleType} {tp :: CrucibleType}
{blocks :: Ctx (Ctx CrucibleType)} {dom :: CrucibleType -> Type}.
Reg ctx tp -> PointAbstraction blocks dom ctx -> dom tp
lookupReg Reg ctx1 x
act PointAbstraction blocks dom ctx1
assignment) CtxRepr args
argTps Assignment (Reg ctx1) args
actuals
funcAbstraction :: dom (FunctionHandleType args ret)
funcAbstraction = Reg ctx1 (FunctionHandleType args ret)
-> PointAbstraction blocks dom ctx1
-> dom (FunctionHandleType args ret)
forall {ctx :: Ctx CrucibleType} {tp :: CrucibleType}
{blocks :: Ctx (Ctx CrucibleType)} {dom :: CrucibleType -> Type}.
Reg ctx tp -> PointAbstraction blocks dom ctx -> dom tp
lookupReg Reg ctx1 (FunctionHandleType args ret)
funcHandle PointAbstraction blocks dom ctx1
assignment
(Maybe (PointAbstraction blocks dom ctx1)
assignment', dom ret
absVal) = Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
(ret :: CrucibleType).
CtxRepr args
-> TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> dom (FunctionHandleType args ret)
-> Assignment dom args
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom ret)
forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
(ret :: CrucibleType).
CtxRepr args
-> TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> dom (FunctionHandleType args ret)
-> Assignment dom args
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom ret)
interpCall Interpretation ext dom
interp CtxRepr args
argTps TypeRepr ret
retTp Reg ctx1 (FunctionHandleType args ret)
funcHandle dom (FunctionHandleType args ret)
funcAbstraction Assignment dom args
actualsAbstractions PointAbstraction blocks dom ctx1
assignment
assignment'' :: PointAbstraction blocks dom ctx1
assignment'' = PointAbstraction blocks dom ctx1
-> (PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1)
-> Maybe (PointAbstraction blocks dom ctx1)
-> PointAbstraction blocks dom ctx1
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PointAbstraction blocks dom ctx1
assignment (Domain dom
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx1
assignment) Maybe (PointAbstraction blocks dom ctx1)
assignment'
in dom ret
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom (ctx1 '::> ret)
forall (dom :: CrucibleType -> Type) (tp :: CrucibleType)
(blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
dom tp
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom (ctx ::> tp)
extendRegisters dom ret
absVal PointAbstraction blocks dom ctx1
assignment''
Assert Reg ctx1 BoolType
_ Reg ctx1 (StringType Unicode)
_ -> PointAbstraction blocks dom ctx1
PointAbstraction blocks dom ctx2
assignment
Assume Reg ctx1 BoolType
_ Reg ctx1 (StringType Unicode)
_ -> PointAbstraction blocks dom ctx1
PointAbstraction blocks dom ctx2
assignment
ReadGlobal GlobalVar tp
gv ->
let (Maybe (PointAbstraction blocks dom ctx1)
assignment', dom tp
absVal) = Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
GlobalVar tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
GlobalVar tp
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp)
interpReadGlobal Interpretation ext dom
interp GlobalVar tp
gv PointAbstraction blocks dom ctx1
assignment
assignment'' :: PointAbstraction blocks dom ctx1
assignment'' = PointAbstraction blocks dom ctx1
-> (PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1)
-> Maybe (PointAbstraction blocks dom ctx1)
-> PointAbstraction blocks dom ctx1
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PointAbstraction blocks dom ctx1
assignment (Domain dom
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom ctx1
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx1
assignment) Maybe (PointAbstraction blocks dom ctx1)
assignment'
in dom tp
-> PointAbstraction blocks dom ctx1
-> PointAbstraction blocks dom (ctx1 '::> tp)
forall (dom :: CrucibleType -> Type) (tp :: CrucibleType)
(blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
dom tp
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom (ctx ::> tp)
extendRegisters dom tp
absVal PointAbstraction blocks dom ctx1
assignment''
WriteGlobal GlobalVar tp
gv Reg ctx1 tp
reg ->
let assignment' :: Maybe (PointAbstraction blocks dom ctx1)
assignment' = Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
GlobalVar tp
-> Reg ctx tp
-> PointAbstraction blocks dom ctx
-> Maybe (PointAbstraction blocks dom ctx)
forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
GlobalVar tp
-> Reg ctx tp
-> PointAbstraction blocks dom ctx
-> Maybe (PointAbstraction blocks dom ctx)
interpWriteGlobal Interpretation ext dom
interp GlobalVar tp
gv Reg ctx1 tp
reg PointAbstraction blocks dom ctx1
assignment
in PointAbstraction blocks dom ctx2
-> (PointAbstraction blocks dom ctx2
-> PointAbstraction blocks dom ctx2)
-> Maybe (PointAbstraction blocks dom ctx2)
-> PointAbstraction blocks dom ctx2
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PointAbstraction blocks dom ctx1
PointAbstraction blocks dom ctx2
assignment (Domain dom
-> PointAbstraction blocks dom ctx2
-> PointAbstraction blocks dom ctx2
-> PointAbstraction blocks dom ctx2
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx1
PointAbstraction blocks dom ctx2
assignment) Maybe (PointAbstraction blocks dom ctx1)
Maybe (PointAbstraction blocks dom ctx2)
assignment'
FreshConstant{} -> String -> PointAbstraction blocks dom ctx2
forall a. HasCallStack => String -> a
error String
"transferStmt: FreshConstant not supported"
FreshFloat{} -> String -> PointAbstraction blocks dom ctx2
forall a. HasCallStack => String -> a
error String
"transferStmt: FreshFloat not supported"
FreshNat{} -> String -> PointAbstraction blocks dom ctx2
forall a. HasCallStack => String -> a
error String
"transferStmt: FreshNat not supported"
NewEmptyRefCell{} -> String -> PointAbstraction blocks dom ctx2
forall a. HasCallStack => String -> a
error String
"transferStmt: NewEmptyRefCell not supported"
NewRefCell {} -> String -> PointAbstraction blocks dom ctx2
forall a. HasCallStack => String -> a
error String
"transferStmt: NewRefCell not supported"
ReadRefCell {} -> String -> PointAbstraction blocks dom ctx2
forall a. HasCallStack => String -> a
error String
"transferStmt: ReadRefCell not supported"
WriteRefCell {} -> String -> PointAbstraction blocks dom ctx2
forall a. HasCallStack => String -> a
error String
"transferStmt: WriteRefCell not supported"
DropRefCell {} -> String -> PointAbstraction blocks dom ctx2
forall a. HasCallStack => String -> a
error String
"transferStmt: DropRefCell not supported"
transferTerm :: forall ctx'
. TermStmt blocks ret ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (S.Set (Some (BlockID blocks)))
transferTerm :: forall (ctx' :: Ctx CrucibleType).
TermStmt blocks ret ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferTerm TermStmt blocks ret ctx'
s PointAbstraction blocks dom ctx'
assignment = do
let BlockID Index blocks ctx
srcIdx = Block ext blocks ret ctx -> BlockID blocks ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret ctx
blk
(FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
Functor f =>
(FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
isFuncAbstr ((FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret))
-> (FunctionAbstraction dom blocks ret
-> FunctionAbstraction dom blocks ret)
-> M dom blocks ret ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= ((Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> Identity
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret)
forall (f :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
Functor f =>
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> f (Assignment
(Ignore (Some (PointAbstraction blocks dom))) blocks))
-> FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret)
faExitRegs ((Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> Identity
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> ((IxValueF
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks)
ctx
-> Identity (Ignore (Some (PointAbstraction blocks dom)) ctx))
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> Identity
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks))
-> (IxValueF
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks)
ctx
-> Identity (Ignore (Some (PointAbstraction blocks dom)) ctx))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IndexF
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks)
ctx
-> Traversal'
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks)
(IxValueF
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks)
ctx)
forall k m (x :: k).
IxedF k m =>
IndexF m x -> Traversal' m (IxValueF m x)
forall (x :: Ctx CrucibleType).
IndexF
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks) x
-> Traversal'
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks)
(IxValueF
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks)
x)
ixF IndexF
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks)
ctx
Index blocks ctx
srcIdx ((IxValueF
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks)
ctx
-> Identity (Ignore (Some (PointAbstraction blocks dom)) ctx))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> Ignore (Some (PointAbstraction blocks dom)) ctx
-> FunctionAbstraction dom blocks ret
-> FunctionAbstraction dom blocks ret
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Some (PointAbstraction blocks dom)
-> Ignore (Some (PointAbstraction blocks dom)) ctx
forall k a (b :: k). a -> Ignore a b
Ignore (PointAbstraction blocks dom ctx'
-> Some (PointAbstraction blocks dom)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some PointAbstraction blocks dom ctx'
assignment))
case TermStmt blocks ret ctx'
s of
ErrorStmt {} -> Set (Some (BlockID blocks))
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Set (Some (BlockID blocks))
forall a. Set a
S.empty
Jump JumpTarget blocks ctx'
target -> JumpTarget blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
JumpTarget blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferJump JumpTarget blocks ctx'
target PointAbstraction blocks dom ctx'
assignment
Br Reg ctx' BoolType
condReg JumpTarget blocks ctx'
target1 JumpTarget blocks ctx'
target2 -> do
let condAbst :: dom BoolType
condAbst = Reg ctx' BoolType
-> PointAbstraction blocks dom ctx' -> dom BoolType
forall {ctx :: Ctx CrucibleType} {tp :: CrucibleType}
{blocks :: Ctx (Ctx CrucibleType)} {dom :: CrucibleType -> Type}.
Reg ctx tp -> PointAbstraction blocks dom ctx -> dom tp
lookupReg Reg ctx' BoolType
condReg PointAbstraction blocks dom ctx'
assignment
(Maybe (PointAbstraction blocks dom ctx')
d1, Maybe (PointAbstraction blocks dom ctx')
d2) = Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType).
Reg ctx BoolType
-> dom BoolType
-> JumpTarget blocks ctx
-> JumpTarget blocks ctx
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx),
Maybe (PointAbstraction blocks dom ctx))
forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType).
Reg ctx BoolType
-> dom BoolType
-> JumpTarget blocks ctx
-> JumpTarget blocks ctx
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx),
Maybe (PointAbstraction blocks dom ctx))
interpBr Interpretation ext dom
interp Reg ctx' BoolType
condReg dom BoolType
condAbst JumpTarget blocks ctx'
target1 JumpTarget blocks ctx'
target2 PointAbstraction blocks dom ctx'
assignment
d1' :: PointAbstraction blocks dom ctx'
d1' = PointAbstraction blocks dom ctx'
-> (PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx')
-> Maybe (PointAbstraction blocks dom ctx')
-> PointAbstraction blocks dom ctx'
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PointAbstraction blocks dom ctx'
assignment (Domain dom
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx'
assignment) Maybe (PointAbstraction blocks dom ctx')
d1
d2' :: PointAbstraction blocks dom ctx'
d2' = PointAbstraction blocks dom ctx'
-> (PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx')
-> Maybe (PointAbstraction blocks dom ctx')
-> PointAbstraction blocks dom ctx'
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PointAbstraction blocks dom ctx'
assignment (Domain dom
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx'
assignment) Maybe (PointAbstraction blocks dom ctx')
d2
Set (Some (BlockID blocks))
s1 <- JumpTarget blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
JumpTarget blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferJump JumpTarget blocks ctx'
target1 PointAbstraction blocks dom ctx'
d1'
Set (Some (BlockID blocks))
s2 <- JumpTarget blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
JumpTarget blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferJump JumpTarget blocks ctx'
target2 PointAbstraction blocks dom ctx'
d2'
Set (Some (BlockID blocks))
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Set (Some (BlockID blocks))
-> Set (Some (BlockID blocks)) -> Set (Some (BlockID blocks))
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (Some (BlockID blocks))
s1 Set (Some (BlockID blocks))
s2)
MaybeBranch TypeRepr tp
tp Reg ctx' (MaybeType tp)
mreg SwitchTarget blocks ctx' tp
swTarget JumpTarget blocks ctx'
jmpTarget -> do
let condAbst :: dom (MaybeType tp)
condAbst = Reg ctx' (MaybeType tp)
-> PointAbstraction blocks dom ctx' -> dom (MaybeType tp)
forall {ctx :: Ctx CrucibleType} {tp :: CrucibleType}
{blocks :: Ctx (Ctx CrucibleType)} {dom :: CrucibleType -> Type}.
Reg ctx tp -> PointAbstraction blocks dom ctx -> dom tp
lookupReg Reg ctx' (MaybeType tp)
mreg PointAbstraction blocks dom ctx'
assignment
(Maybe (PointAbstraction blocks dom ctx')
d1, dom tp
mAbstraction, Maybe (PointAbstraction blocks dom ctx')
d2) = Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypeRepr tp
-> Reg ctx (MaybeType tp)
-> dom (MaybeType tp)
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp,
Maybe (PointAbstraction blocks dom ctx))
forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypeRepr tp
-> Reg ctx (MaybeType tp)
-> dom (MaybeType tp)
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom tp,
Maybe (PointAbstraction blocks dom ctx))
interpMaybe Interpretation ext dom
interp TypeRepr tp
tp Reg ctx' (MaybeType tp)
mreg dom (MaybeType tp)
condAbst PointAbstraction blocks dom ctx'
assignment
d1' :: PointAbstraction blocks dom ctx'
d1' = PointAbstraction blocks dom ctx'
-> (PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx')
-> Maybe (PointAbstraction blocks dom ctx')
-> PointAbstraction blocks dom ctx'
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PointAbstraction blocks dom ctx'
assignment (Domain dom
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx'
assignment) Maybe (PointAbstraction blocks dom ctx')
d1
d2' :: PointAbstraction blocks dom ctx'
d2' = PointAbstraction blocks dom ctx'
-> (PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx')
-> Maybe (PointAbstraction blocks dom ctx')
-> PointAbstraction blocks dom ctx'
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PointAbstraction blocks dom ctx'
assignment (Domain dom
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx'
assignment) Maybe (PointAbstraction blocks dom ctx')
d2
Set (Some (BlockID blocks))
s1 <- SwitchTarget blocks ctx' tp
-> dom tp
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType) (tp :: CrucibleType).
SwitchTarget blocks ctx' tp
-> dom tp
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferSwitch SwitchTarget blocks ctx' tp
swTarget dom tp
mAbstraction PointAbstraction blocks dom ctx'
d1'
Set (Some (BlockID blocks))
s2 <- JumpTarget blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
JumpTarget blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferJump JumpTarget blocks ctx'
jmpTarget PointAbstraction blocks dom ctx'
d2'
Set (Some (BlockID blocks))
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Set (Some (BlockID blocks))
-> Set (Some (BlockID blocks)) -> Set (Some (BlockID blocks))
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (Some (BlockID blocks))
s1 Set (Some (BlockID blocks))
s2)
Return Reg ctx' ret
reg -> do
let absVal :: dom ret
absVal = Reg ctx' ret -> PointAbstraction blocks dom ctx' -> dom ret
forall {ctx :: Ctx CrucibleType} {tp :: CrucibleType}
{blocks :: Ctx (Ctx CrucibleType)} {dom :: CrucibleType -> Type}.
Reg ctx tp -> PointAbstraction blocks dom ctx -> dom tp
lookupReg Reg ctx' ret
reg PointAbstraction blocks dom ctx'
assignment
(dom ret -> Identity (dom ret))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(ret :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Functor f =>
(dom ret -> f (dom ret))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
isRetAbstr ((dom ret -> Identity (dom ret))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret))
-> (dom ret -> dom ret) -> M dom blocks ret ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= Domain dom
-> forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
forall (dom :: CrucibleType -> Type).
Domain dom
-> forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
domJoin Domain dom
dom dom ret
absVal
Set (Some (BlockID blocks))
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Set (Some (BlockID blocks))
forall a. Set a
S.empty
TailCall Reg ctx' (FunctionHandleType args ret)
fn CtxRepr args
callArgs Assignment (Reg ctx') args
actuals -> do
let argAbstractions :: Assignment dom args
argAbstractions = (forall (x :: CrucibleType). TypeRepr x -> Reg ctx' x -> dom x)
-> CtxRepr args
-> Assignment (Reg ctx') args
-> Assignment dom args
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
(a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
PU.zipWith (\TypeRepr x
_tp Reg ctx' x
act -> Reg ctx' x -> PointAbstraction blocks dom ctx' -> dom x
forall {ctx :: Ctx CrucibleType} {tp :: CrucibleType}
{blocks :: Ctx (Ctx CrucibleType)} {dom :: CrucibleType -> Type}.
Reg ctx tp -> PointAbstraction blocks dom ctx -> dom tp
lookupReg Reg ctx' x
act PointAbstraction blocks dom ctx'
assignment) CtxRepr args
callArgs Assignment (Reg ctx') args
actuals
callee :: dom (FunctionHandleType args ret)
callee = Reg ctx' (FunctionHandleType args ret)
-> PointAbstraction blocks dom ctx'
-> dom (FunctionHandleType args ret)
forall {ctx :: Ctx CrucibleType} {tp :: CrucibleType}
{blocks :: Ctx (Ctx CrucibleType)} {dom :: CrucibleType -> Type}.
Reg ctx tp -> PointAbstraction blocks dom ctx -> dom tp
lookupReg Reg ctx' (FunctionHandleType args ret)
fn PointAbstraction blocks dom ctx'
assignment
(Maybe (PointAbstraction blocks dom ctx')
_assignment', dom ret
absVal) = Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
(ret :: CrucibleType).
CtxRepr args
-> TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> dom (FunctionHandleType args ret)
-> Assignment dom args
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom ret)
forall ext (dom :: CrucibleType -> Type).
Interpretation ext dom
-> forall (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
(ret :: CrucibleType).
CtxRepr args
-> TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> dom (FunctionHandleType args ret)
-> Assignment dom args
-> PointAbstraction blocks dom ctx
-> (Maybe (PointAbstraction blocks dom ctx), dom ret)
interpCall Interpretation ext dom
interp CtxRepr args
callArgs TypeRepr ret
retRepr Reg ctx' (FunctionHandleType args ret)
fn dom (FunctionHandleType args ret)
callee Assignment dom args
argAbstractions PointAbstraction blocks dom ctx'
assignment
(dom ret -> Identity (dom ret))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(ret :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Functor f =>
(dom ret -> f (dom ret))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
isRetAbstr ((dom ret -> Identity (dom ret))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret))
-> (dom ret -> dom ret) -> M dom blocks ret ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= Domain dom
-> forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
forall (dom :: CrucibleType -> Type).
Domain dom
-> forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
domJoin Domain dom
dom dom ret
absVal
Set (Some (BlockID blocks))
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Set (Some (BlockID blocks))
forall a. Set a
S.empty
VariantElim {} -> String -> M dom blocks ret (Set (Some (BlockID blocks)))
forall a. HasCallStack => String -> a
error String
"transferTerm: VariantElim terminator not supported"
transferJump :: forall ctx'
. JumpTarget blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (S.Set (Some (BlockID blocks)))
transferJump :: forall (ctx' :: Ctx CrucibleType).
JumpTarget blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferJump (JumpTarget BlockID blocks args
target CtxRepr args
argsTps Assignment (Reg ctx') args
actuals) PointAbstraction blocks dom ctx'
assignment = do
let blockAbstr0 :: PointAbstraction blocks dom args
blockAbstr0 = PointAbstraction blocks dom ctx'
assignment { _paRegisters = PU.zipWith (\TypeRepr x
_tp Reg ctx' x
act -> Reg ctx' x -> PointAbstraction blocks dom ctx' -> dom x
forall {ctx :: Ctx CrucibleType} {tp :: CrucibleType}
{blocks :: Ctx (Ctx CrucibleType)} {dom :: CrucibleType -> Type}.
Reg ctx tp -> PointAbstraction blocks dom ctx -> dom tp
lookupReg Reg ctx' x
act PointAbstraction blocks dom ctx'
assignment) argsTps actuals
, _paRegisterRefs = PU.zipWith (\TypeRepr x
_tp Reg ctx' x
act -> Reg ctx' x -> PointAbstraction blocks dom ctx' -> RefSet blocks x
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType)
(blocks :: Ctx (Ctx CrucibleType)) (dom :: CrucibleType -> Type).
Reg ctx tp -> PointAbstraction blocks dom ctx -> RefSet blocks tp
lookupRegRefs Reg ctx' x
act PointAbstraction blocks dom ctx'
assignment) argsTps actuals
}
BlockID blocks args
-> PointAbstraction blocks dom args
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
BlockID blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferTarget BlockID blocks args
target PointAbstraction blocks dom args
blockAbstr0
transferSwitch :: forall ctx' tp
. SwitchTarget blocks ctx' tp
-> dom tp
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (S.Set (Some (BlockID blocks)))
transferSwitch :: forall (ctx' :: Ctx CrucibleType) (tp :: CrucibleType).
SwitchTarget blocks ctx' tp
-> dom tp
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferSwitch (SwitchTarget BlockID blocks (args ::> tp)
target CtxRepr args
argTps Assignment (Reg ctx') args
actuals) dom tp
domVal PointAbstraction blocks dom ctx'
assignment = do
let argRegAbstractions :: Assignment dom args
argRegAbstractions = (forall (x :: CrucibleType). TypeRepr x -> Reg ctx' x -> dom x)
-> CtxRepr args
-> Assignment (Reg ctx') args
-> Assignment dom args
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
(a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
PU.zipWith (\TypeRepr x
_ Reg ctx' x
act -> Reg ctx' x -> PointAbstraction blocks dom ctx' -> dom x
forall {ctx :: Ctx CrucibleType} {tp :: CrucibleType}
{blocks :: Ctx (Ctx CrucibleType)} {dom :: CrucibleType -> Type}.
Reg ctx tp -> PointAbstraction blocks dom ctx -> dom tp
lookupReg Reg ctx' x
act PointAbstraction blocks dom ctx'
assignment) CtxRepr args
argTps Assignment (Reg ctx') args
actuals
argRegRefAbstractions :: Assignment (RefSet blocks) args
argRegRefAbstractions = (forall (x :: CrucibleType).
TypeRepr x -> Reg ctx' x -> RefSet blocks x)
-> CtxRepr args
-> Assignment (Reg ctx') args
-> Assignment (RefSet blocks) args
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
(a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
PU.zipWith (\TypeRepr x
_ Reg ctx' x
act -> Reg ctx' x -> PointAbstraction blocks dom ctx' -> RefSet blocks x
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType)
(blocks :: Ctx (Ctx CrucibleType)) (dom :: CrucibleType -> Type).
Reg ctx tp -> PointAbstraction blocks dom ctx -> RefSet blocks tp
lookupRegRefs Reg ctx' x
act PointAbstraction blocks dom ctx'
assignment) CtxRepr args
argTps Assignment (Reg ctx') args
actuals
blockAbstr0 :: PointAbstraction blocks dom (args ::> tp)
blockAbstr0 = PointAbstraction blocks dom ctx'
assignment { _paRegisters = PU.extend argRegAbstractions domVal
, _paRegisterRefs = PU.extend argRegRefAbstractions emptyRefSet
}
BlockID blocks (args ::> tp)
-> PointAbstraction blocks dom (args ::> tp)
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
BlockID blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferTarget BlockID blocks (args ::> tp)
target PointAbstraction blocks dom (args ::> tp)
blockAbstr0
transferTarget :: forall ctx'
. BlockID blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (S.Set (Some (BlockID blocks)))
transferTarget :: forall (ctx' :: Ctx CrucibleType).
BlockID blocks ctx'
-> PointAbstraction blocks dom ctx'
-> M dom blocks ret (Set (Some (BlockID blocks)))
transferTarget target :: BlockID blocks ctx'
target@(BlockID Index blocks ctx'
idx) PointAbstraction blocks dom ctx'
assignment = do
PointAbstraction blocks dom ctx'
old <- Index blocks ctx'
-> M dom blocks ret (PointAbstraction blocks dom ctx')
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(tp :: Ctx CrucibleType).
Index blocks tp
-> M dom blocks ret (PointAbstraction blocks dom tp)
lookupAssignment Index blocks ctx'
idx
Bool
haveVisited <- BlockID blocks ctx' -> M dom blocks ret Bool
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
BlockID blocks ctx -> M dom blocks ret Bool
isVisited BlockID blocks ctx'
target
let new :: PointAbstraction blocks dom ctx'
new = Domain dom
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
joinPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx'
old PointAbstraction blocks dom ctx'
assignment
case Bool
haveVisited Bool -> Bool -> Bool
&& Domain dom
-> PointAbstraction blocks dom ctx'
-> PointAbstraction blocks dom ctx'
-> Bool
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> Bool
equalPointAbstractions Domain dom
dom PointAbstraction blocks dom ctx'
old PointAbstraction blocks dom ctx'
new of
Bool
True -> Set (Some (BlockID blocks))
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Set (Some (BlockID blocks))
forall a. Set a
S.empty
Bool
False -> do
BlockID blocks ctx' -> M dom blocks ret ()
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
BlockID blocks ctx -> M dom blocks ret ()
markVisited BlockID blocks ctx'
target
(FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
Functor f =>
(FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
isFuncAbstr ((FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret))
-> (FunctionAbstraction dom blocks ret
-> FunctionAbstraction dom blocks ret)
-> M dom blocks ret ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= ((Assignment (PointAbstraction blocks dom) blocks
-> Identity (Assignment (PointAbstraction blocks dom) blocks))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret)
forall (f :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
Functor f =>
(Assignment (PointAbstraction blocks dom) blocks
-> f (Assignment (PointAbstraction blocks dom) blocks))
-> FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret)
faEntryRegs ((Assignment (PointAbstraction blocks dom) blocks
-> Identity (Assignment (PointAbstraction blocks dom) blocks))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> ((IxValueF
(Assignment (PointAbstraction blocks dom) blocks) ctx'
-> Identity (PointAbstraction blocks dom ctx'))
-> Assignment (PointAbstraction blocks dom) blocks
-> Identity (Assignment (PointAbstraction blocks dom) blocks))
-> (IxValueF (Assignment (PointAbstraction blocks dom) blocks) ctx'
-> Identity (PointAbstraction blocks dom ctx'))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IndexF (Assignment (PointAbstraction blocks dom) blocks) ctx'
-> Traversal'
(Assignment (PointAbstraction blocks dom) blocks)
(IxValueF (Assignment (PointAbstraction blocks dom) blocks) ctx')
forall k m (x :: k).
IxedF k m =>
IndexF m x -> Traversal' m (IxValueF m x)
forall (x :: Ctx CrucibleType).
IndexF (Assignment (PointAbstraction blocks dom) blocks) x
-> Traversal'
(Assignment (PointAbstraction blocks dom) blocks)
(IxValueF (Assignment (PointAbstraction blocks dom) blocks) x)
ixF IndexF (Assignment (PointAbstraction blocks dom) blocks) ctx'
Index blocks ctx'
idx ((IxValueF (Assignment (PointAbstraction blocks dom) blocks) ctx'
-> Identity (PointAbstraction blocks dom ctx'))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> PointAbstraction blocks dom ctx'
-> FunctionAbstraction dom blocks ret
-> FunctionAbstraction dom blocks ret
forall s t a b. ASetter s t a b -> b -> s -> t
.~ PointAbstraction blocks dom ctx'
new)
Set (Some (BlockID blocks))
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some (BlockID blocks) -> Set (Some (BlockID blocks))
forall a. a -> Set a
S.singleton (BlockID blocks ctx' -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks ctx'
target))
markVisited :: BlockID blocks ctx -> M dom blocks ret ()
markVisited :: forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
BlockID blocks ctx -> M dom blocks ret ()
markVisited BlockID blocks ctx
bid = do
(Set (Some (BlockID blocks))
-> Identity (Set (Some (BlockID blocks))))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret)
forall (f :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
Functor f =>
(Set (Some (BlockID blocks)) -> f (Set (Some (BlockID blocks))))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
processedOnce ((Set (Some (BlockID blocks))
-> Identity (Set (Some (BlockID blocks))))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret))
-> (Set (Some (BlockID blocks)) -> Set (Some (BlockID blocks)))
-> M dom blocks ret ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= Some (BlockID blocks)
-> Set (Some (BlockID blocks)) -> Set (Some (BlockID blocks))
forall a. Ord a => a -> Set a -> Set a
S.insert (BlockID blocks ctx -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks ctx
bid)
isVisited :: BlockID blocks ctx -> M dom blocks ret Bool
isVisited :: forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
BlockID blocks ctx -> M dom blocks ret Bool
isVisited BlockID blocks ctx
bid = do
Set (Some (BlockID blocks))
s <- (IterationState dom blocks ret -> Set (Some (BlockID blocks)))
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall s (m :: Type -> Type) a. MonadState s m => (s -> a) -> m a
St.gets IterationState dom blocks ret -> Set (Some (BlockID blocks))
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
IterationState dom blocks ret -> Set (Some (BlockID blocks))
_processedOnce
Bool -> M dom blocks ret Bool
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BlockID blocks ctx -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks ctx
bid Some (BlockID blocks) -> Set (Some (BlockID blocks)) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (Some (BlockID blocks))
s)
forwardFixpoint' :: forall ext dom blocks ret init
. Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> PM.MapF GlobalVar dom
-> PU.Assignment dom init
-> ( PU.Assignment (PointAbstraction blocks dom) blocks
, PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
, dom ret )
forwardFixpoint' :: forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(init :: Ctx CrucibleType).
Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> MapF GlobalVar dom
-> Assignment dom init
-> (Assignment (PointAbstraction blocks dom) blocks,
Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks,
dom ret)
forwardFixpoint' Domain dom
dom Interpretation ext dom
interp CFG ext blocks init ret
cfg MapF GlobalVar dom
globals0 Assignment dom init
assignment0 =
let BlockID Index blocks init
idx = CFG ext blocks init ret -> BlockID blocks init
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockID blocks init
cfgEntryBlockID CFG ext blocks init ret
cfg
pa0 :: PointAbstraction blocks dom init
pa0 = PointAbstraction { _paGlobals :: MapF GlobalVar dom
_paGlobals = MapF GlobalVar dom
globals0
, _paRegisters :: Assignment dom init
_paRegisters = Assignment dom init
assignment0
, _paRefs :: MapF (RefStmtId blocks) dom
_paRefs = MapF (RefStmtId blocks) dom
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
PM.empty
, _paRegisterRefs :: Assignment (RefSet blocks) init
_paRegisterRefs = (forall (x :: CrucibleType). dom x -> RefSet blocks x)
-> forall (x :: Ctx CrucibleType).
Assignment dom x -> Assignment (RefSet blocks) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
PU.fmapFC (RefSet blocks x -> dom x -> RefSet blocks x
forall a b. a -> b -> a
const RefSet blocks x
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
RefSet blocks tp
emptyRefSet) Assignment dom init
assignment0
}
freshAssignment :: PU.Index blocks ctx -> PointAbstraction blocks dom ctx
freshAssignment :: forall (ctx :: Ctx CrucibleType).
Index blocks ctx -> PointAbstraction blocks dom ctx
freshAssignment Index blocks ctx
i =
PointAbstraction { _paRegisters :: Assignment dom ctx
_paRegisters = (forall (x :: CrucibleType). TypeRepr x -> dom x)
-> forall (x :: Ctx CrucibleType).
Assignment TypeRepr x -> Assignment dom x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
PU.fmapFC (dom x -> TypeRepr x -> dom x
forall a b. a -> b -> a
const (Domain dom -> forall (tp :: CrucibleType). dom tp
forall (dom :: CrucibleType -> Type).
Domain dom -> forall (tp :: CrucibleType). dom tp
domBottom Domain dom
dom)) (Block ext blocks ret ctx -> Assignment TypeRepr ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs (BlockID blocks ctx
-> BlockMap ext blocks ret -> Block ext blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType))
(args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock (Index blocks ctx -> BlockID blocks ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID Index blocks ctx
i) (CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
cfg)))
, _paRegisterRefs :: Assignment (RefSet blocks) ctx
_paRegisterRefs = (forall (x :: CrucibleType). TypeRepr x -> RefSet blocks x)
-> forall (x :: Ctx CrucibleType).
Assignment TypeRepr x -> Assignment (RefSet blocks) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
PU.fmapFC (RefSet blocks x -> TypeRepr x -> RefSet blocks x
forall a b. a -> b -> a
const RefSet blocks x
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
RefSet blocks tp
emptyRefSet) (Block ext blocks ret ctx -> Assignment TypeRepr ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs (BlockID blocks ctx
-> BlockMap ext blocks ret -> Block ext blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType))
(args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock (Index blocks ctx -> BlockID blocks ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID Index blocks ctx
i) (CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
cfg)))
, _paGlobals :: MapF GlobalVar dom
_paGlobals = MapF GlobalVar dom
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
PM.empty
, _paRefs :: MapF (RefStmtId blocks) dom
_paRefs = MapF (RefStmtId blocks) dom
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
PM.empty
}
emptyFreshAssignment :: PU.Index blocks ctx -> Ignore (Some (PointAbstraction blocks dom)) ctx
emptyFreshAssignment :: forall (ctx :: Ctx CrucibleType).
Index blocks ctx -> Ignore (Some (PointAbstraction blocks dom)) ctx
emptyFreshAssignment Index blocks ctx
_i =
Some (PointAbstraction blocks dom)
-> Ignore (Some (PointAbstraction blocks dom)) ctx
forall k a (b :: k). a -> Ignore a b
Ignore (PointAbstraction blocks dom EmptyCtx
-> Some (PointAbstraction blocks dom)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (PointAbstraction { _paRegisters :: Assignment dom EmptyCtx
_paRegisters = Assignment dom EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
PU.empty
, _paGlobals :: MapF GlobalVar dom
_paGlobals = MapF GlobalVar dom
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
PM.empty
, _paRefs :: MapF (RefStmtId blocks) dom
_paRefs = MapF (RefStmtId blocks) dom
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
PM.empty
, _paRegisterRefs :: Assignment (RefSet blocks) EmptyCtx
_paRegisterRefs = Assignment (RefSet blocks) EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
PU.empty
}))
s0 :: IterationState dom blocks ret
s0 = IterationState { _isRetAbstr :: dom ret
_isRetAbstr = Domain dom -> forall (tp :: CrucibleType). dom tp
forall (dom :: CrucibleType -> Type).
Domain dom -> forall (tp :: CrucibleType). dom tp
domBottom Domain dom
dom
, _isFuncAbstr :: FunctionAbstraction dom blocks ret
_isFuncAbstr =
FunctionAbstraction { _faEntryRegs :: Assignment (PointAbstraction blocks dom) blocks
_faEntryRegs =
Size blocks
-> (forall (ctx :: Ctx CrucibleType).
Index blocks ctx -> PointAbstraction blocks dom ctx)
-> Assignment (PointAbstraction blocks dom) blocks
forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
PU.generate (BlockMap ext blocks ret -> Size blocks
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
PU.size (CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
cfg)) Index blocks tp -> PointAbstraction blocks dom tp
forall (ctx :: Ctx CrucibleType).
Index blocks ctx -> PointAbstraction blocks dom ctx
freshAssignment
Assignment (PointAbstraction blocks dom) blocks
-> (Assignment (PointAbstraction blocks dom) blocks
-> Assignment (PointAbstraction blocks dom) blocks)
-> Assignment (PointAbstraction blocks dom) blocks
forall a b. a -> (a -> b) -> b
& IndexF (Assignment (PointAbstraction blocks dom) blocks) init
-> Traversal'
(Assignment (PointAbstraction blocks dom) blocks)
(IxValueF (Assignment (PointAbstraction blocks dom) blocks) init)
forall k m (x :: k).
IxedF k m =>
IndexF m x -> Traversal' m (IxValueF m x)
forall (x :: Ctx CrucibleType).
IndexF (Assignment (PointAbstraction blocks dom) blocks) x
-> Traversal'
(Assignment (PointAbstraction blocks dom) blocks)
(IxValueF (Assignment (PointAbstraction blocks dom) blocks) x)
ixF IndexF (Assignment (PointAbstraction blocks dom) blocks) init
Index blocks init
idx ((IxValueF (Assignment (PointAbstraction blocks dom) blocks) init
-> Identity (PointAbstraction blocks dom init))
-> Assignment (PointAbstraction blocks dom) blocks
-> Identity (Assignment (PointAbstraction blocks dom) blocks))
-> PointAbstraction blocks dom init
-> Assignment (PointAbstraction blocks dom) blocks
-> Assignment (PointAbstraction blocks dom) blocks
forall s t a b. ASetter s t a b -> b -> s -> t
.~ PointAbstraction blocks dom init
pa0
, _faExitRegs :: Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
_faExitRegs = Size blocks
-> (forall (ctx :: Ctx CrucibleType).
Index blocks ctx
-> Ignore (Some (PointAbstraction blocks dom)) ctx)
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
PU.generate (BlockMap ext blocks ret -> Size blocks
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
PU.size (CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
cfg)) Index blocks tp -> Ignore (Some (PointAbstraction blocks dom)) tp
forall (ctx :: Ctx CrucibleType).
Index blocks ctx -> Ignore (Some (PointAbstraction blocks dom)) ctx
emptyFreshAssignment
, _faRet :: dom ret
_faRet = Domain dom -> forall (tp :: CrucibleType). dom tp
forall (dom :: CrucibleType -> Type).
Domain dom -> forall (tp :: CrucibleType). dom tp
domBottom Domain dom
dom
}
, _processedOnce :: Set (Some (BlockID blocks))
_processedOnce = Set (Some (BlockID blocks))
forall a. Set a
S.empty
}
iterStrat :: Interpretation ext dom
-> CFG ext blocks init ret -> M dom blocks ret ()
iterStrat = Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
forall (dom :: CrucibleType -> Type) ext
(blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType)
(ret :: CrucibleType).
Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
iterationStrategy Domain dom
dom
abstr' :: IterationState dom blocks ret
abstr' = State (IterationState dom blocks ret) ()
-> IterationState dom blocks ret -> IterationState dom blocks ret
forall s a. State s a -> s -> s
St.execState (M dom blocks ret () -> State (IterationState dom blocks ret) ()
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) a.
M dom blocks ret a -> State (IterationState dom blocks ret) a
runM (Interpretation ext dom
-> CFG ext blocks init ret -> M dom blocks ret ()
iterStrat Interpretation ext dom
interp CFG ext blocks init ret
cfg)) IterationState dom blocks ret
s0
in ( FunctionAbstraction dom blocks ret
-> Assignment (PointAbstraction blocks dom) blocks
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
FunctionAbstraction dom blocks ret
-> Assignment (PointAbstraction blocks dom) blocks
_faEntryRegs (IterationState dom blocks ret -> FunctionAbstraction dom blocks ret
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
IterationState dom blocks ret -> FunctionAbstraction dom blocks ret
_isFuncAbstr IterationState dom blocks ret
abstr')
, FunctionAbstraction dom blocks ret
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
FunctionAbstraction dom blocks ret
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
_faExitRegs (IterationState dom blocks ret -> FunctionAbstraction dom blocks ret
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
IterationState dom blocks ret -> FunctionAbstraction dom blocks ret
_isFuncAbstr IterationState dom blocks ret
abstr')
, IterationState dom blocks ret -> dom ret
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
IterationState dom blocks ret -> dom ret
_isRetAbstr IterationState dom blocks ret
abstr' )
forwardFixpoint :: forall ext dom blocks ret init
. Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> PM.MapF GlobalVar dom
-> PU.Assignment dom init
-> (PU.Assignment (PointAbstraction blocks dom) blocks, dom ret)
forwardFixpoint :: forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(init :: Ctx CrucibleType).
Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> MapF GlobalVar dom
-> Assignment dom init
-> (Assignment (PointAbstraction blocks dom) blocks, dom ret)
forwardFixpoint Domain dom
dom Interpretation ext dom
interp CFG ext blocks init ret
cfg MapF GlobalVar dom
globals0 Assignment dom init
assignment0 =
let (Assignment (PointAbstraction blocks dom) blocks
ass, Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
_, dom ret
ret) = Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> MapF GlobalVar dom
-> Assignment dom init
-> (Assignment (PointAbstraction blocks dom) blocks,
Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks,
dom ret)
forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(init :: Ctx CrucibleType).
Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> MapF GlobalVar dom
-> Assignment dom init
-> (Assignment (PointAbstraction blocks dom) blocks,
Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks,
dom ret)
forwardFixpoint' Domain dom
dom Interpretation ext dom
interp CFG ext blocks init ret
cfg MapF GlobalVar dom
globals0 Assignment dom init
assignment0
in (Assignment (PointAbstraction blocks dom) blocks
ass, dom ret
ret)
iterationStrategy :: Domain dom -> (Interpretation ext dom -> CFG ext blocks init ret -> M dom blocks ret ())
iterationStrategy :: forall (dom :: CrucibleType -> Type) ext
(blocks :: Ctx (Ctx CrucibleType)) (init :: Ctx CrucibleType)
(ret :: CrucibleType).
Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
iterationStrategy Domain dom
dom =
case Domain dom -> IterationStrategy dom
forall (dom :: CrucibleType -> Type).
Domain dom -> IterationStrategy dom
domIter Domain dom
dom of
WTOWidening Int -> Bool
s forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
op -> Maybe (WideningStrategy, WideningOperator dom)
-> Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(init :: Ctx CrucibleType).
Maybe (WideningStrategy, WideningOperator dom)
-> Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
wtoIteration ((WideningStrategy, WideningOperator dom)
-> Maybe (WideningStrategy, WideningOperator dom)
forall a. a -> Maybe a
Just ((Int -> Bool) -> WideningStrategy
WideningStrategy Int -> Bool
s, (forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp)
-> WideningOperator dom
forall {k} (dom :: k -> Type).
(forall (tp :: k). dom tp -> dom tp -> dom tp)
-> WideningOperator dom
WideningOperator dom tp -> dom tp -> dom tp
forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
op)) Domain dom
dom
IterationStrategy dom
WTO -> Maybe (WideningStrategy, WideningOperator dom)
-> Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(init :: Ctx CrucibleType).
Maybe (WideningStrategy, WideningOperator dom)
-> Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
wtoIteration Maybe (WideningStrategy, WideningOperator dom)
forall a. Maybe a
Nothing Domain dom
dom
IterationStrategy dom
Worklist -> Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(init :: Ctx CrucibleType).
Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
worklistIteration Domain dom
dom
worklistIteration :: forall ext dom blocks ret init
. Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
worklistIteration :: forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(init :: Ctx CrucibleType).
Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
worklistIteration Domain dom
dom Interpretation ext dom
interp CFG ext blocks init ret
cfg =
Set (Some (BlockID blocks)) -> M dom blocks ret ()
loop (Some (BlockID blocks) -> Set (Some (BlockID blocks))
forall a. a -> Set a
S.singleton (BlockID blocks init -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (CFG ext blocks init ret -> BlockID blocks init
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockID blocks init
cfgEntryBlockID CFG ext blocks init ret
cfg)))
where
loop :: Set (Some (BlockID blocks)) -> M dom blocks ret ()
loop Set (Some (BlockID blocks))
worklist =
case Set (Some (BlockID blocks))
-> Maybe (Some (BlockID blocks), Set (Some (BlockID blocks)))
forall a. Set a -> Maybe (a, Set a)
S.minView Set (Some (BlockID blocks))
worklist of
Maybe (Some (BlockID blocks), Set (Some (BlockID blocks)))
Nothing -> () -> M dom blocks ret ()
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
Just (Some target :: BlockID blocks x
target@(BlockID Index blocks x
idx), Set (Some (BlockID blocks))
worklist') -> do
PointAbstraction blocks dom x
assignment <- Index blocks x -> M dom blocks ret (PointAbstraction blocks dom x)
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(tp :: Ctx CrucibleType).
Index blocks tp
-> M dom blocks ret (PointAbstraction blocks dom tp)
lookupAssignment Index blocks x
idx
Block ext blocks ret x
-> PointAbstraction blocks dom x
-> Set (Some (BlockID blocks))
-> M dom blocks ret ()
forall (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx
-> PointAbstraction blocks dom ctx
-> Set (Some (BlockID blocks))
-> M dom blocks ret ()
visit (BlockID blocks x
-> BlockMap ext blocks ret -> Block ext blocks ret x
forall (blocks :: Ctx (Ctx CrucibleType))
(args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock BlockID blocks x
target (CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
cfg)) PointAbstraction blocks dom x
assignment Set (Some (BlockID blocks))
worklist'
visit :: Block ext blocks ret ctx
-> PointAbstraction blocks dom ctx
-> S.Set (Some (BlockID blocks))
-> M dom blocks ret ()
visit :: forall (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx
-> PointAbstraction blocks dom ctx
-> Set (Some (BlockID blocks))
-> M dom blocks ret ()
visit Block ext blocks ret ctx
blk PointAbstraction blocks dom ctx
startingAssignment Set (Some (BlockID blocks))
worklist' = do
Set (Some (BlockID blocks))
s <- Domain dom
-> Interpretation ext dom
-> TypeRepr ret
-> Block ext blocks ret ctx
-> PointAbstraction blocks dom ctx
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Domain dom
-> Interpretation ext dom
-> TypeRepr ret
-> Block ext blocks ret ctx
-> PointAbstraction blocks dom ctx
-> M dom blocks ret (Set (Some (BlockID blocks)))
transfer Domain dom
dom Interpretation ext dom
interp (CFG ext blocks init ret -> TypeRepr ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> TypeRepr ret
cfgReturnType CFG ext blocks init ret
cfg) Block ext blocks ret ctx
blk PointAbstraction blocks dom ctx
startingAssignment
Set (Some (BlockID blocks)) -> M dom blocks ret ()
loop (Set (Some (BlockID blocks))
-> Set (Some (BlockID blocks)) -> Set (Some (BlockID blocks))
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (Some (BlockID blocks))
s Set (Some (BlockID blocks))
worklist')
wtoIteration :: forall ext dom blocks ret init
. Maybe (WideningStrategy, WideningOperator dom)
-> Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
wtoIteration :: forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(init :: Ctx CrucibleType).
Maybe (WideningStrategy, WideningOperator dom)
-> Domain dom
-> Interpretation ext dom
-> CFG ext blocks init ret
-> M dom blocks ret ()
wtoIteration Maybe (WideningStrategy, WideningOperator dom)
mWiden Domain dom
dom Interpretation ext dom
interp CFG ext blocks init ret
cfg = [WTOComponent (Some (BlockID blocks))] -> M dom blocks ret ()
loop (CFG ext blocks init ret -> [WTOComponent (Some (BlockID blocks))]
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> [WTOComponent (Some (BlockID blocks))]
cfgWeakTopologicalOrdering CFG ext blocks init ret
cfg)
where
loop :: [WTOComponent (Some (BlockID blocks))] -> M dom blocks ret ()
loop [] = () -> M dom blocks ret ()
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
loop (Vertex (Some bid :: BlockID blocks x
bid@(BlockID Index blocks x
idx)) : [WTOComponent (Some (BlockID blocks))]
rest) = do
PointAbstraction blocks dom x
assignment <- Index blocks x -> M dom blocks ret (PointAbstraction blocks dom x)
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(tp :: Ctx CrucibleType).
Index blocks tp
-> M dom blocks ret (PointAbstraction blocks dom tp)
lookupAssignment Index blocks x
idx
let blk :: Block ext blocks ret x
blk = BlockID blocks x
-> BlockMap ext blocks ret -> Block ext blocks ret x
forall (blocks :: Ctx (Ctx CrucibleType))
(args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock BlockID blocks x
bid (CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
cfg)
Set (Some (BlockID blocks))
_ <- Domain dom
-> Interpretation ext dom
-> TypeRepr ret
-> Block ext blocks ret x
-> PointAbstraction blocks dom x
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Domain dom
-> Interpretation ext dom
-> TypeRepr ret
-> Block ext blocks ret ctx
-> PointAbstraction blocks dom ctx
-> M dom blocks ret (Set (Some (BlockID blocks)))
transfer Domain dom
dom Interpretation ext dom
interp (CFG ext blocks init ret -> TypeRepr ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> TypeRepr ret
cfgReturnType CFG ext blocks init ret
cfg) Block ext blocks ret x
blk PointAbstraction blocks dom x
assignment
[WTOComponent (Some (BlockID blocks))] -> M dom blocks ret ()
loop [WTOComponent (Some (BlockID blocks))]
rest
loop (SCC (SCCData { wtoHead :: forall n. SCC n -> n
wtoHead = Some (BlockID blocks)
hbid, wtoComps :: forall n. SCC n -> [WTOComponent n]
wtoComps = [WTOComponent (Some (BlockID blocks))]
comps }) : [WTOComponent (Some (BlockID blocks))]
rest) = do
Some (BlockID blocks)
-> [WTOComponent (Some (BlockID blocks))]
-> Int
-> M dom blocks ret ()
processSCC Some (BlockID blocks)
hbid [WTOComponent (Some (BlockID blocks))]
comps Int
0
[WTOComponent (Some (BlockID blocks))] -> M dom blocks ret ()
loop [WTOComponent (Some (BlockID blocks))]
rest
processSCC :: Some (BlockID blocks)
-> [WTOComponent (Some (BlockID blocks))]
-> Int
-> M dom blocks ret ()
processSCC (Some hbid :: BlockID blocks x
hbid@(BlockID Index blocks x
idx)) [WTOComponent (Some (BlockID blocks))]
comps Int
iterNum = do
PointAbstraction blocks dom x
headInput0 <- Index blocks x -> M dom blocks ret (PointAbstraction blocks dom x)
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(tp :: Ctx CrucibleType).
Index blocks tp
-> M dom blocks ret (PointAbstraction blocks dom tp)
lookupAssignment Index blocks x
idx
let headBlock :: Block ext blocks ret x
headBlock = BlockID blocks x
-> BlockMap ext blocks ret -> Block ext blocks ret x
forall (blocks :: Ctx (Ctx CrucibleType))
(args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock BlockID blocks x
hbid (CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
cfg)
Set (Some (BlockID blocks))
_ <- Domain dom
-> Interpretation ext dom
-> TypeRepr ret
-> Block ext blocks ret x
-> PointAbstraction blocks dom x
-> M dom blocks ret (Set (Some (BlockID blocks)))
forall ext (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Domain dom
-> Interpretation ext dom
-> TypeRepr ret
-> Block ext blocks ret ctx
-> PointAbstraction blocks dom ctx
-> M dom blocks ret (Set (Some (BlockID blocks)))
transfer Domain dom
dom Interpretation ext dom
interp (CFG ext blocks init ret -> TypeRepr ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> TypeRepr ret
cfgReturnType CFG ext blocks init ret
cfg) Block ext blocks ret x
headBlock PointAbstraction blocks dom x
headInput0
[WTOComponent (Some (BlockID blocks))] -> M dom blocks ret ()
loop [WTOComponent (Some (BlockID blocks))]
comps
PointAbstraction blocks dom x
headInput1 <- Index blocks x -> M dom blocks ret (PointAbstraction blocks dom x)
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(tp :: Ctx CrucibleType).
Index blocks tp
-> M dom blocks ret (PointAbstraction blocks dom tp)
lookupAssignment Index blocks x
idx
case Domain dom
-> PointAbstraction blocks dom x
-> PointAbstraction blocks dom x
-> Bool
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Domain dom
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> Bool
equalPointAbstractions Domain dom
dom PointAbstraction blocks dom x
headInput0 PointAbstraction blocks dom x
headInput1 of
Bool
True -> () -> M dom blocks ret ()
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
Bool
False -> do
case Maybe (WideningStrategy, WideningOperator dom)
mWiden of
Just (WideningStrategy Int -> Bool
strat, WideningOperator forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
widen)
| Int -> Bool
strat Int
iterNum -> do
let headInputW :: PointAbstraction blocks dom x
headInputW = (forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp)
-> (forall (tp :: CrucibleType).
RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp)
-> PointAbstraction blocks dom x
-> PointAbstraction blocks dom x
-> PointAbstraction blocks dom x
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
(forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp)
-> (forall (tp :: CrucibleType).
RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp)
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
-> PointAbstraction blocks dom ctx
zipPAWith dom tp -> dom tp -> dom tp
forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
widen RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: CrucibleType).
RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp
forall (tp :: CrucibleType).
RefSet blocks tp -> RefSet blocks tp -> RefSet blocks tp
unionRefSets PointAbstraction blocks dom x
headInput0 PointAbstraction blocks dom x
headInput1
(FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
Functor f =>
(FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
isFuncAbstr ((FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> Identity (IterationState dom blocks ret))
-> (FunctionAbstraction dom blocks ret
-> FunctionAbstraction dom blocks ret)
-> M dom blocks ret ()
forall s (m :: Type -> Type) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= ((Assignment (PointAbstraction blocks dom) blocks
-> Identity (Assignment (PointAbstraction blocks dom) blocks))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret)
forall (f :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
Functor f =>
(Assignment (PointAbstraction blocks dom) blocks
-> f (Assignment (PointAbstraction blocks dom) blocks))
-> FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret)
faEntryRegs ((Assignment (PointAbstraction blocks dom) blocks
-> Identity (Assignment (PointAbstraction blocks dom) blocks))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> ((IxValueF (Assignment (PointAbstraction blocks dom) blocks) x
-> Identity (PointAbstraction blocks dom x))
-> Assignment (PointAbstraction blocks dom) blocks
-> Identity (Assignment (PointAbstraction blocks dom) blocks))
-> (IxValueF (Assignment (PointAbstraction blocks dom) blocks) x
-> Identity (PointAbstraction blocks dom x))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IndexF (Assignment (PointAbstraction blocks dom) blocks) x
-> Traversal'
(Assignment (PointAbstraction blocks dom) blocks)
(IxValueF (Assignment (PointAbstraction blocks dom) blocks) x)
forall k m (x :: k).
IxedF k m =>
IndexF m x -> Traversal' m (IxValueF m x)
forall (x :: Ctx CrucibleType).
IndexF (Assignment (PointAbstraction blocks dom) blocks) x
-> Traversal'
(Assignment (PointAbstraction blocks dom) blocks)
(IxValueF (Assignment (PointAbstraction blocks dom) blocks) x)
ixF IndexF (Assignment (PointAbstraction blocks dom) blocks) x
Index blocks x
idx ((IxValueF (Assignment (PointAbstraction blocks dom) blocks) x
-> Identity (PointAbstraction blocks dom x))
-> FunctionAbstraction dom blocks ret
-> Identity (FunctionAbstraction dom blocks ret))
-> PointAbstraction blocks dom x
-> FunctionAbstraction dom blocks ret
-> FunctionAbstraction dom blocks ret
forall s t a b. ASetter s t a b -> b -> s -> t
.~ PointAbstraction blocks dom x
headInputW)
Maybe (WideningStrategy, WideningOperator dom)
_ -> () -> M dom blocks ret ()
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
Some (BlockID blocks)
-> [WTOComponent (Some (BlockID blocks))]
-> Int
-> M dom blocks ret ()
processSCC (BlockID blocks x -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks x
hbid) [WTOComponent (Some (BlockID blocks))]
comps (Int
iterNum Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
lookupAssignment :: forall dom blocks ret tp
. PU.Index blocks tp
-> M dom blocks ret (PointAbstraction blocks dom tp)
lookupAssignment :: forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(tp :: Ctx CrucibleType).
Index blocks tp
-> M dom blocks ret (PointAbstraction blocks dom tp)
lookupAssignment Index blocks tp
idx = do
IterationState dom blocks ret
abstr <- M dom blocks ret (IterationState dom blocks ret)
forall s (m :: Type -> Type). MonadState s m => m s
St.get
PointAbstraction blocks dom tp
-> M dom blocks ret (PointAbstraction blocks dom tp)
forall a. a -> M dom blocks ret a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((IterationState dom blocks ret
abstr IterationState dom blocks ret
-> Getting
(Assignment (PointAbstraction blocks dom) blocks)
(IterationState dom blocks ret)
(Assignment (PointAbstraction blocks dom) blocks)
-> Assignment (PointAbstraction blocks dom) blocks
forall s a. s -> Getting a s a -> a
^. (FunctionAbstraction dom blocks ret
-> Const
(Assignment (PointAbstraction blocks dom) blocks)
(FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> Const
(Assignment (PointAbstraction blocks dom) blocks)
(IterationState dom blocks ret)
forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
Functor f =>
(FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
isFuncAbstr ((FunctionAbstraction dom blocks ret
-> Const
(Assignment (PointAbstraction blocks dom) blocks)
(FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> Const
(Assignment (PointAbstraction blocks dom) blocks)
(IterationState dom blocks ret))
-> ((Assignment (PointAbstraction blocks dom) blocks
-> Const
(Assignment (PointAbstraction blocks dom) blocks)
(Assignment (PointAbstraction blocks dom) blocks))
-> FunctionAbstraction dom blocks ret
-> Const
(Assignment (PointAbstraction blocks dom) blocks)
(FunctionAbstraction dom blocks ret))
-> Getting
(Assignment (PointAbstraction blocks dom) blocks)
(IterationState dom blocks ret)
(Assignment (PointAbstraction blocks dom) blocks)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Assignment (PointAbstraction blocks dom) blocks
-> Const
(Assignment (PointAbstraction blocks dom) blocks)
(Assignment (PointAbstraction blocks dom) blocks))
-> FunctionAbstraction dom blocks ret
-> Const
(Assignment (PointAbstraction blocks dom) blocks)
(FunctionAbstraction dom blocks ret)
forall (f :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
Functor f =>
(Assignment (PointAbstraction blocks dom) blocks
-> f (Assignment (PointAbstraction blocks dom) blocks))
-> FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret)
faEntryRegs) Assignment (PointAbstraction blocks dom) blocks
-> Index blocks tp -> PointAbstraction blocks dom tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
PU.! Index blocks tp
idx)
lookupRegRefs :: Reg ctx tp -> PointAbstraction blocks dom ctx -> RefSet blocks tp
lookupRegRefs :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType)
(blocks :: Ctx (Ctx CrucibleType)) (dom :: CrucibleType -> Type).
Reg ctx tp -> PointAbstraction blocks dom ctx -> RefSet blocks tp
lookupRegRefs Reg ctx tp
reg PointAbstraction blocks dom ctx
assignment = (PointAbstraction blocks dom ctx
assignment PointAbstraction blocks dom ctx
-> Getting
(Assignment (RefSet blocks) ctx)
(PointAbstraction blocks dom ctx)
(Assignment (RefSet blocks) ctx)
-> Assignment (RefSet blocks) ctx
forall s a. s -> Getting a s a -> a
^. Getting
(Assignment (RefSet blocks) ctx)
(PointAbstraction blocks dom ctx)
(Assignment (RefSet blocks) ctx)
forall (f :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (dom :: CrucibleType -> Type).
Functor f =>
(Assignment (RefSet blocks) ctx
-> f (Assignment (RefSet blocks) ctx))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRegisterRefs) Assignment (RefSet blocks) ctx -> Index ctx tp -> RefSet blocks tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
PU.! Reg ctx tp -> Index ctx tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
regIndex Reg ctx tp
reg
newtype Ignore a (b::k) = Ignore { forall k a (b :: k). Ignore a b -> a
_ignoreOut :: a }
deriving (Ignore a b -> Ignore a b -> Bool
(Ignore a b -> Ignore a b -> Bool)
-> (Ignore a b -> Ignore a b -> Bool) -> Eq (Ignore a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a k (b :: k). Eq a => Ignore a b -> Ignore a b -> Bool
$c== :: forall a k (b :: k). Eq a => Ignore a b -> Ignore a b -> Bool
== :: Ignore a b -> Ignore a b -> Bool
$c/= :: forall a k (b :: k). Eq a => Ignore a b -> Ignore a b -> Bool
/= :: Ignore a b -> Ignore a b -> Bool
Eq, Eq (Ignore a b)
Eq (Ignore a b) =>
(Ignore a b -> Ignore a b -> Ordering)
-> (Ignore a b -> Ignore a b -> Bool)
-> (Ignore a b -> Ignore a b -> Bool)
-> (Ignore a b -> Ignore a b -> Bool)
-> (Ignore a b -> Ignore a b -> Bool)
-> (Ignore a b -> Ignore a b -> Ignore a b)
-> (Ignore a b -> Ignore a b -> Ignore a b)
-> Ord (Ignore a b)
Ignore a b -> Ignore a b -> Bool
Ignore a b -> Ignore a b -> Ordering
Ignore a b -> Ignore a b -> Ignore a b
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
forall a k (b :: k). Ord a => Eq (Ignore a b)
forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Bool
forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Ordering
forall a k (b :: k).
Ord a =>
Ignore a b -> Ignore a b -> Ignore a b
$ccompare :: forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Ordering
compare :: Ignore a b -> Ignore a b -> Ordering
$c< :: forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Bool
< :: Ignore a b -> Ignore a b -> Bool
$c<= :: forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Bool
<= :: Ignore a b -> Ignore a b -> Bool
$c> :: forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Bool
> :: Ignore a b -> Ignore a b -> Bool
$c>= :: forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Bool
>= :: Ignore a b -> Ignore a b -> Bool
$cmax :: forall a k (b :: k).
Ord a =>
Ignore a b -> Ignore a b -> Ignore a b
max :: Ignore a b -> Ignore a b -> Ignore a b
$cmin :: forall a k (b :: k).
Ord a =>
Ignore a b -> Ignore a b -> Ignore a b
min :: Ignore a b -> Ignore a b -> Ignore a b
Ord)
instance Show a => Show (Ignore a tp) where
show :: Ignore a tp -> String
show (Ignore a
x) = a -> String
forall a. Show a => a -> String
show a
x
instance Show a => ShowF (Ignore a)
paGlobals :: (Functor f)
=> (PM.MapF GlobalVar dom -> f (PM.MapF GlobalVar dom))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paGlobals :: forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
Functor f =>
(MapF GlobalVar dom -> f (MapF GlobalVar dom))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paGlobals MapF GlobalVar dom -> f (MapF GlobalVar dom)
f PointAbstraction blocks dom ctx
pa = (\MapF GlobalVar dom
a -> PointAbstraction blocks dom ctx
pa { _paGlobals = a }) (MapF GlobalVar dom -> PointAbstraction blocks dom ctx)
-> f (MapF GlobalVar dom) -> f (PointAbstraction blocks dom ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> MapF GlobalVar dom -> f (MapF GlobalVar dom)
f (PointAbstraction blocks dom ctx -> MapF GlobalVar dom
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
PointAbstraction blocks dom ctx -> MapF GlobalVar dom
_paGlobals PointAbstraction blocks dom ctx
pa)
paRegisters :: (Functor f)
=> (PU.Assignment dom ctx -> f (PU.Assignment dom ctx))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRegisters :: forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Functor f =>
(Assignment dom ctx -> f (Assignment dom ctx))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRegisters Assignment dom ctx -> f (Assignment dom ctx)
f PointAbstraction blocks dom ctx
pa = (\Assignment dom ctx
a -> PointAbstraction blocks dom ctx
pa { _paRegisters = a }) (Assignment dom ctx -> PointAbstraction blocks dom ctx)
-> f (Assignment dom ctx) -> f (PointAbstraction blocks dom ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Assignment dom ctx -> f (Assignment dom ctx)
f (PointAbstraction blocks dom ctx -> Assignment dom ctx
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
PointAbstraction blocks dom ctx -> Assignment dom ctx
_paRegisters PointAbstraction blocks dom ctx
pa)
paRegisterRefs :: (Functor f)
=> (PU.Assignment (RefSet blocks) ctx -> f (PU.Assignment (RefSet blocks) ctx))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRegisterRefs :: forall (f :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
(ctx :: Ctx CrucibleType) (dom :: CrucibleType -> Type).
Functor f =>
(Assignment (RefSet blocks) ctx
-> f (Assignment (RefSet blocks) ctx))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRegisterRefs Assignment (RefSet blocks) ctx
-> f (Assignment (RefSet blocks) ctx)
f PointAbstraction blocks dom ctx
pa = (\Assignment (RefSet blocks) ctx
a -> PointAbstraction blocks dom ctx
pa { _paRegisterRefs = a }) (Assignment (RefSet blocks) ctx -> PointAbstraction blocks dom ctx)
-> f (Assignment (RefSet blocks) ctx)
-> f (PointAbstraction blocks dom ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Assignment (RefSet blocks) ctx
-> f (Assignment (RefSet blocks) ctx)
f (PointAbstraction blocks dom ctx -> Assignment (RefSet blocks) ctx
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
PointAbstraction blocks dom ctx -> Assignment (RefSet blocks) ctx
_paRegisterRefs PointAbstraction blocks dom ctx
pa)
paRefs :: (Functor f)
=> (PM.MapF (RefStmtId blocks) dom -> f (PM.MapF (RefStmtId blocks) dom))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRefs :: forall (f :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
Functor f =>
(MapF (RefStmtId blocks) dom -> f (MapF (RefStmtId blocks) dom))
-> PointAbstraction blocks dom ctx
-> f (PointAbstraction blocks dom ctx)
paRefs MapF (RefStmtId blocks) dom -> f (MapF (RefStmtId blocks) dom)
f PointAbstraction blocks dom ctx
pa = (\MapF (RefStmtId blocks) dom
a -> PointAbstraction blocks dom ctx
pa { _paRefs = a }) (MapF (RefStmtId blocks) dom -> PointAbstraction blocks dom ctx)
-> f (MapF (RefStmtId blocks) dom)
-> f (PointAbstraction blocks dom ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> MapF (RefStmtId blocks) dom -> f (MapF (RefStmtId blocks) dom)
f (PointAbstraction blocks dom ctx -> MapF (RefStmtId blocks) dom
forall (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ctx :: Ctx CrucibleType).
PointAbstraction blocks dom ctx -> MapF (RefStmtId blocks) dom
_paRefs PointAbstraction blocks dom ctx
pa)
faEntryRegs :: (Functor f)
=> (PU.Assignment (PointAbstraction blocks dom) blocks -> f (PU.Assignment (PointAbstraction blocks dom) blocks))
-> FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret)
faEntryRegs :: forall (f :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
Functor f =>
(Assignment (PointAbstraction blocks dom) blocks
-> f (Assignment (PointAbstraction blocks dom) blocks))
-> FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret)
faEntryRegs Assignment (PointAbstraction blocks dom) blocks
-> f (Assignment (PointAbstraction blocks dom) blocks)
f FunctionAbstraction dom blocks ret
fa = (\Assignment (PointAbstraction blocks dom) blocks
a -> FunctionAbstraction dom blocks ret
fa { _faEntryRegs = a }) (Assignment (PointAbstraction blocks dom) blocks
-> FunctionAbstraction dom blocks ret)
-> f (Assignment (PointAbstraction blocks dom) blocks)
-> f (FunctionAbstraction dom blocks ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Assignment (PointAbstraction blocks dom) blocks
-> f (Assignment (PointAbstraction blocks dom) blocks)
f (FunctionAbstraction dom blocks ret
-> Assignment (PointAbstraction blocks dom) blocks
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
FunctionAbstraction dom blocks ret
-> Assignment (PointAbstraction blocks dom) blocks
_faEntryRegs FunctionAbstraction dom blocks ret
fa)
faExitRegs :: (Functor f)
=> (PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks -> f (PU.Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks))
-> FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret)
faExitRegs :: forall (f :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
Functor f =>
(Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> f (Assignment
(Ignore (Some (PointAbstraction blocks dom))) blocks))
-> FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret)
faExitRegs Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> f (Assignment
(Ignore (Some (PointAbstraction blocks dom))) blocks)
f FunctionAbstraction dom blocks ret
fa = (\Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
a -> FunctionAbstraction dom blocks ret
fa { _faExitRegs = a }) (Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> FunctionAbstraction dom blocks ret)
-> f (Assignment
(Ignore (Some (PointAbstraction blocks dom))) blocks)
-> f (FunctionAbstraction dom blocks ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
-> f (Assignment
(Ignore (Some (PointAbstraction blocks dom))) blocks)
f (FunctionAbstraction dom blocks ret
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
FunctionAbstraction dom blocks ret
-> Assignment (Ignore (Some (PointAbstraction blocks dom))) blocks
_faExitRegs FunctionAbstraction dom blocks ret
fa)
isFuncAbstr :: (Functor f)
=> (FunctionAbstraction dom blocks ret -> f (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
isFuncAbstr :: forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
Functor f =>
(FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
isFuncAbstr FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret)
f IterationState dom blocks ret
is = (\FunctionAbstraction dom blocks ret
a -> IterationState dom blocks ret
is { _isFuncAbstr = a }) (FunctionAbstraction dom blocks ret
-> IterationState dom blocks ret)
-> f (FunctionAbstraction dom blocks ret)
-> f (IterationState dom blocks ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> FunctionAbstraction dom blocks ret
-> f (FunctionAbstraction dom blocks ret)
f (IterationState dom blocks ret -> FunctionAbstraction dom blocks ret
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
IterationState dom blocks ret -> FunctionAbstraction dom blocks ret
_isFuncAbstr IterationState dom blocks ret
is)
isRetAbstr :: (Functor f) => (dom ret -> f (dom ret)) -> IterationState dom blocks ret -> f (IterationState dom blocks ret)
isRetAbstr :: forall (f :: Type -> Type) (dom :: CrucibleType -> Type)
(ret :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Functor f =>
(dom ret -> f (dom ret))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
isRetAbstr dom ret -> f (dom ret)
f IterationState dom blocks ret
is = (\dom ret
a -> IterationState dom blocks ret
is { _isRetAbstr = a }) (dom ret -> IterationState dom blocks ret)
-> f (dom ret) -> f (IterationState dom blocks ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> dom ret -> f (dom ret)
f (IterationState dom blocks ret -> dom ret
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
IterationState dom blocks ret -> dom ret
_isRetAbstr IterationState dom blocks ret
is)
processedOnce :: (Functor f)
=> (S.Set (Some (BlockID blocks)) -> f (S.Set (Some (BlockID blocks))))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
processedOnce :: forall (f :: Type -> Type) (blocks :: Ctx (Ctx CrucibleType))
(dom :: CrucibleType -> Type) (ret :: CrucibleType).
Functor f =>
(Set (Some (BlockID blocks)) -> f (Set (Some (BlockID blocks))))
-> IterationState dom blocks ret
-> f (IterationState dom blocks ret)
processedOnce Set (Some (BlockID blocks)) -> f (Set (Some (BlockID blocks)))
f IterationState dom blocks ret
is = (\Set (Some (BlockID blocks))
a -> IterationState dom blocks ret
is { _processedOnce = a}) (Set (Some (BlockID blocks)) -> IterationState dom blocks ret)
-> f (Set (Some (BlockID blocks)))
-> f (IterationState dom blocks ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Set (Some (BlockID blocks)) -> f (Set (Some (BlockID blocks)))
f (IterationState dom blocks ret -> Set (Some (BlockID blocks))
forall (dom :: CrucibleType -> Type)
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
IterationState dom blocks ret -> Set (Some (BlockID blocks))
_processedOnce IterationState dom blocks ret
is)
data Pointed dom (tp :: CrucibleType) where
Top :: Pointed a tp
Pointed :: dom tp -> Pointed dom tp
Bottom :: Pointed dom tp
deriving instance (Eq (dom tp)) => Eq (Pointed dom tp)
instance ShowF dom => Show (Pointed dom tp) where
show :: Pointed dom tp -> String
show Pointed dom tp
Top = String
"Top"
show Pointed dom tp
Bottom = String
"Bottom"
show (Pointed dom tp
p) = dom tp -> String
forall k (f :: k -> Type) (tp :: k). ShowF f => f tp -> String
forall (tp :: CrucibleType). dom tp -> String
showF dom tp
p
instance ShowF dom => ShowF (Pointed dom)
pointed :: (forall tp . dom tp -> dom tp -> Pointed dom tp)
-> (forall tp . dom tp -> dom tp -> Bool)
-> IterationStrategy (Pointed dom)
-> Domain (Pointed dom)
pointed :: forall (dom :: CrucibleType -> Type).
(forall (tp :: CrucibleType). dom tp -> dom tp -> Pointed dom tp)
-> (forall (tp :: CrucibleType). dom tp -> dom tp -> Bool)
-> IterationStrategy (Pointed dom)
-> Domain (Pointed dom)
pointed forall (tp :: CrucibleType). dom tp -> dom tp -> Pointed dom tp
j forall (tp :: CrucibleType). dom tp -> dom tp -> Bool
eq IterationStrategy (Pointed dom)
iterStrat =
Domain { domTop :: forall (tp :: CrucibleType). Pointed dom tp
domTop = Pointed dom tp
forall (tp :: CrucibleType). Pointed dom tp
forall (a :: CrucibleType -> Type) (tp :: CrucibleType).
Pointed a tp
Top
, domBottom :: forall (tp :: CrucibleType). Pointed dom tp
domBottom = Pointed dom tp
forall (tp :: CrucibleType). Pointed dom tp
forall (a :: CrucibleType -> Type) (tp :: CrucibleType).
Pointed a tp
Bottom
, domJoin :: forall (tp :: CrucibleType).
Pointed dom tp -> Pointed dom tp -> Pointed dom tp
domJoin = (dom tp -> dom tp -> Pointed dom tp)
-> Pointed dom tp -> Pointed dom tp -> Pointed dom tp
forall {a :: CrucibleType -> Type} {tp :: CrucibleType}.
(a tp -> a tp -> Pointed a tp)
-> Pointed a tp -> Pointed a tp -> Pointed a tp
pointedJoin dom tp -> dom tp -> Pointed dom tp
forall (tp :: CrucibleType). dom tp -> dom tp -> Pointed dom tp
j
, domEq :: forall (tp :: CrucibleType).
Pointed dom tp -> Pointed dom tp -> Bool
domEq = (dom tp -> dom tp -> Bool)
-> Pointed dom tp -> Pointed dom tp -> Bool
forall {dom :: CrucibleType -> Type} {tp :: CrucibleType}
{dom :: CrucibleType -> Type} {tp :: CrucibleType}.
(dom tp -> dom tp -> Bool)
-> Pointed dom tp -> Pointed dom tp -> Bool
pointedEq dom tp -> dom tp -> Bool
forall (tp :: CrucibleType). dom tp -> dom tp -> Bool
eq
, domIter :: IterationStrategy (Pointed dom)
domIter = IterationStrategy (Pointed dom)
iterStrat
}
where
pointedJoin :: (a tp -> a tp -> Pointed a tp)
-> Pointed a tp -> Pointed a tp -> Pointed a tp
pointedJoin a tp -> a tp -> Pointed a tp
_ Pointed a tp
Top Pointed a tp
_ = Pointed a tp
forall (a :: CrucibleType -> Type) (tp :: CrucibleType).
Pointed a tp
Top
pointedJoin a tp -> a tp -> Pointed a tp
_ Pointed a tp
_ Pointed a tp
Top = Pointed a tp
forall (a :: CrucibleType -> Type) (tp :: CrucibleType).
Pointed a tp
Top
pointedJoin a tp -> a tp -> Pointed a tp
_ Pointed a tp
Bottom Pointed a tp
a = Pointed a tp
a
pointedJoin a tp -> a tp -> Pointed a tp
_ Pointed a tp
a Pointed a tp
Bottom = Pointed a tp
a
pointedJoin a tp -> a tp -> Pointed a tp
j' (Pointed a tp
p1) (Pointed a tp
p2) = a tp -> a tp -> Pointed a tp
j' a tp
p1 a tp
p2
pointedEq :: (dom tp -> dom tp -> Bool)
-> Pointed dom tp -> Pointed dom tp -> Bool
pointedEq dom tp -> dom tp -> Bool
_ Pointed dom tp
Top Pointed dom tp
Top = Bool
True
pointedEq dom tp -> dom tp -> Bool
_ Pointed dom tp
Bottom Pointed dom tp
Bottom = Bool
True
pointedEq dom tp -> dom tp -> Bool
eq' (Pointed dom tp
p1) (Pointed dom tp
p2) = dom tp -> dom tp -> Bool
eq' dom tp
p1 dom tp
p2
pointedEq dom tp -> dom tp -> Bool
_ Pointed dom tp
_ Pointed dom tp
_ = Bool
False