-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Analysis.Fixpoint
-- Description      : Abstract interpretation over SSA function CFGs
-- Copyright        : (c) Galois, Inc 2015
-- License          : BSD3
-- Maintainer       : Tristan Ravitch <tristan@galois.com>
-- Stability        : provisional
--
--  Abstract interpretation over the Crucible IR
--
--  Supports widening with an iteration order based on weak
--  topological orderings.  Some basic tests on hand-written IR
--  programs are included.
------------------------------------------------------------------------

{-# 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 (
  -- * Entry point
  forwardFixpoint,
  forwardFixpoint',
  ScopedReg(..),
  lookupAbstractScopedRegValue,
  lookupAbstractScopedRegValueByIndex,
  Ignore(..),
  -- * Abstract Domains
  Domain(..),
  IterationStrategy(..),
  Interpretation(..),
  PointAbstraction(..),
  RefSet,
  emptyRefSet,
  paGlobals,
  paRegisters,
  lookupAbstractRegValue,
  modifyAbstractRegValue,
  cfgWeakTopologicalOrdering,
  -- * Pointed domains
  -- $pointed
  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

-- | A wrapper around widening strategies
data WideningStrategy = WideningStrategy (Int -> Bool)

-- | A wrapper around widening operators.  This is mostly here to
-- avoid requiring impredicative types later.
data WideningOperator dom = WideningOperator (forall tp . dom tp -> dom tp -> dom tp)

-- | The iteration strategies available for computing fixed points.
--
-- Algorithmically, the best strategies seem to be based on Weak
-- Topological Orders (WTOs).  The WTO approach also naturally
-- supports widening (with a specified widening strategy and widening
-- operator).
--
-- A simple worklist approach is also available.
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

-- | A domain of abstract values, parameterized by a term type
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
         }

-- | Transfer functions for each statement type
--
-- Interpretation functions for some statement types --
-- e.g. @interpExpr@ and @interpExt@ -- receive 'ScopedReg' arguments
-- corresponding to the SSA tmp that the result of the interpreted
-- statement get assigned to. Some interpretation functions that could
-- receive this argument do not -- e.g. @interpCall@ -- because
-- conathan didn't have a use for that.
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))
                 }

-- | This abstraction contains the abstract values of each register at
-- the program point represented by the abstraction.  It also contains
-- a map of abstractions for all of the global variables currently
-- known.
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
                   -- ^ In this map, the keys are really just the 'StmtId's in
                   -- '_paRegisterRefs', but with a newtype wrapper that unwraps
                   -- a level of their 'ReferenceType` type rep.
                   , 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
                   -- ^ This mapping records the *set* of references (named by
                   -- allocation site) that each register could hold.
                   }

-- | This is a wrapper around 'StmtId' that exposes the underlying type of a
-- 'ReferenceType', and is needed to define the abstract value we carry around.
newtype RefStmtId blocks tp = RefStmtId (StmtId blocks (ReferenceType tp))

-- | This type names an allocation site in a program.
--
-- Allocation sites are named by their basic block and their index into that
-- containing basic block.  We have to carry around the type repr for inspection
-- later (especially in instances).
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

-- | This is a wrapper around a set of 'StmtId's that name allocation sites of
-- references.  We need the wrapper to correctly position the @tp@ type
-- parameter so that we can put them in an 'PU.Assignment'.
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)

-- | Look up the abstract value of a register at a program point
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

-- | Modify the abstract value of a register at a program point
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

-- | The `FunctionAbstraction` contains the abstractions for the entry
-- point of each basic block in the function, as well as the final
-- abstract value for the returned register.
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
                        -- ^ Mapping from blocks to point abstractions
                        -- at entry to 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
                        -- ^ Mapping from blocks to point abstractions
                        -- at exit from blocks. Blocks are indexed by
                        -- their entry context, but not by there exit
                        -- contexts, so we wrap the point abstraction
                        -- in @Ignore . Some@ to hide the context of
                        -- SSA tmps at exit.
                      , forall (dom :: CrucibleType -> Type)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
FunctionAbstraction dom blocks ret -> dom ret
_faRet :: dom ret
                        -- ^ Abstract value at return from function.
                      }

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)

-- | Extend the abstraction with a domain value for the next register.
--
-- The set of references that the register can point to is set to the empty set
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
     }

-- | Join two point abstractions using the join operation of the domain.
--
-- We join registers pointwise.  For globals, we explicitly call join
-- when the global is in both maps.  If a global is only in one map,
-- there is an implicit join with bottom, which always results in the
-- same element.  Since it is a no-op, we just skip it and keep the
-- one present element.
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)
      }

-- | Compare two point abstractions for equality.
--
-- Note that the globals maps are converted to a list and the lists
-- are checked for equality.  This should be safe if order is
-- preserved properly in the list functions...
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)

----------------------------------------------------------------

-- | A CFG-scoped SSA temp register.
--
-- We don't care about the type params yet, hence the
-- existential quantification. We may want to look up the instruction
-- corresponding to a 'ScopedReg' after analysis though, and we'll
-- surely want to compare 'ScopedReg's for equality, and use them to
-- look up values in point abstractions after analysis.
data ScopedReg where
  ScopedReg :: BlockID blocks ctx1 -> Reg ctx2 tp -> ScopedReg
-- The pretty-show library can't parse the derived version, because it
-- doesn't like bare "%" and/or "$" in atoms.
{- deriving instance Show 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

----------------------------------------------------------------

-- | Lookup the abstract value of scoped reg in an exit assignment.
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

-- | Lookup the abstract value of scoped reg -- specified by 0-based
-- int indices -- in an exit assignment.
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)

-- | Lookup a value in an assignment based on it's 0-based int index.
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))

----------------------------------------------------------------

-- | Apply the transfer functions from an interpretation to a block,
-- given a starting set of abstract values.
--
-- Return a set of blocks to visit later.
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

    -- We maintain the current 'Size' of the context so that we can
    -- compute the SSA temp register corresponding to the current
    -- statement.
    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''

        -- This statement aids in debugging the representation, but
        -- should not be a meaningful part of any analysis.  For now,
        -- skip it in the interpretation.  We could add a transfer
        -- function for it...
        --
        -- Note that this is not used to represent print statements in
        -- the language being represented.  This is a *crucible* level
        -- print.  This is actually apparent in the type of Print,
        -- which does not modify its context at all.
        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''

        -- FIXME: This would actually potentially be nice to
        -- capture. We would need to extend the context,
        -- though... maybe with a unit type.
        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"

    -- Transfer a block terminator statement.
    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
      -- Save the current point abstraction as the exit point
      -- abstraction since we won't be defining any more SSA tmps in
      -- this block.
      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
              -- assignment'' = maybe assignment (joinPointAbstractions dom assignment) assignment'

          -- We don't really have a place to put a modified assignment
          -- here, which is interesting.  There is no next block...
          (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

    -- Return the singleton set containing the target block if we
    -- haven't converged yet on the current block, and otherwise
    -- return an empty set while updating the function abstraction for
    -- the current block.
    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)

-- | Compute a fixed point via abstract interpretation over a control
-- flow graph ('CFG') given 1) an interpretation + domain, 2) initial
-- assignments of domain values to global variables, and 3) initial
-- assignments of domain values to function arguments.
--
-- This is an intraprocedural analysis.  To handle function calls, the
-- transfer function for call statements must know how to supply
-- summaries or compute an appropriate conservative approximation.
--
-- There are two results from the fixed point computation:
--
-- 1) For each block in the CFG, the abstraction computed at the *entry* to the block
--
-- 2) For each block in the CFG, the abstraction computed at the
-- *exit* from the block. The 'PU.Assignment' for these "exit"
-- abstractions ignores the @ctx@ index on the blocks, since that
-- context is for *entry* to the blocks.
--
-- 3) The final abstract value for the value returned by the function
forwardFixpoint' :: forall ext dom blocks ret init
                 . Domain dom
                -- ^ The domain of abstract values
                -> Interpretation ext dom
                -- ^ The transfer functions for each statement type
                -> CFG ext blocks init ret
                -- ^ The function to analyze
                -> PM.MapF GlobalVar dom
                -- ^ Assignments of abstract values to global variables at the function start
                -> PU.Assignment dom init
                -- ^ Assignments of abstract values to the function arguments
                -> ( 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' )

-- Preserve old interface for now; fix tests later if my generalization is the right one.
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)

-- | Inspect the 'Domain' definition to determine which iteration
-- strategy the caller requested.
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

-- | Iterate over blocks using a worklist (i.e., after a block is
-- processed and abstract values change, put the block successors on
-- the worklist).
--
-- The worklist is actually processed by taking the lowest-numbered
-- block in a set as the next work item.
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')

-- | Iterate over the blocks in the control flow graph in weak
-- topological order until a fixed point is reached.
--
-- The weak topological order essentially formalizes the idea of
-- breaking the graph on back edges and putting the result in
-- topological order.  The blocks that serve as loop heads are the
-- heads of their respective strongly connected components.  Those
-- block heads are suitable locations to apply widening operators
-- (which can be provided to this iterator).
wtoIteration :: forall ext dom blocks ret init
              . Maybe (WideningStrategy, WideningOperator dom)
              -- ^ An optional widening operator
             -> 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

    -- Process a single SCC until the input to the head node of the
    -- SCC stabilizes.  Applies widening if requested.
    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
      -- We process the SCC until the input to the head of the SCC stabilizes
      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
            -- TODO(conathan): figure out if we need to do something
            -- here with 'faExitRegs'?
            Just (WideningStrategy Int -> Bool
strat, WideningOperator forall (tp :: CrucibleType). dom tp -> dom tp -> dom tp
widen)
              | Int -> Bool
strat Int
iterNum -> do
                  -- TODO: is unionRefSets the right thing below?
                  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

-- | Turn a non paramaterized type into a parameterized type.
--
-- For when you want to use a @parameterized-utils@ style data
-- structure with a type that doesn't have a parameter.
--
-- The same definition as 'Control.Applicative.Const', but with a
-- different 'Show' instance.
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)

-- Lenses

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)

-- $pointed
--
-- The 'Pointed' type is a wrapper around another 'Domain' that
-- provides distinguished 'Top' and 'Bottom' elements.  Use of this
-- type is never required (domains can always define their own top and
-- bottom), but this1 wrapper can save some boring boilerplate.

-- | The Pointed wrapper that adds Top and Bottom elements
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)

-- | Construct a 'Pointed' 'Domain' from a pointed join function and
-- an equality test.
pointed :: (forall tp . dom tp -> dom tp -> Pointed dom tp)
        -- ^ Join of contained domain elements
        -> (forall tp . dom tp -> dom tp -> Bool)
        -- ^ Equality for domain elements
        -> 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
           -- TODO(conathan): test faExitRegs computation with WTO
           -- strategy. It was hardcoded to 'WTO' here before conathan
           -- added block-exit point abstractions.
         , 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