-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.CFG.Reg
-- Description      : Provides a representation of Crucible programs using
--                    mutable registers rather than SSA.
-- Copyright        : (c) Galois, Inc 2014-2016
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- This module defines CFGs that feature mutable registers, in
-- contrast to the Core CFGs ("Lang.Crucible.CFG.Core"), which are in
-- SSA form. Register CFGs can be translated into SSA CFGs using the
-- "Lang.Crucible.CFG.SSAConversion" module.
--
-- Module "Lang.Crucible.CFG.Generator" provides a high-level monadic
-- interface for producing register CFGs.
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Lang.Crucible.CFG.Reg
  ( -- * CFG
    CFG(..)
  , cfgEntryBlock
  , cfgInputTypes
  , cfgArgTypes
  , cfgReturnType
  , substCFG
  , SomeCFG(..)
  , AnyCFG(..)
  , Label(..)
  , substLabel
  , LambdaLabel(..)
  , substLambdaLabel
  , BlockID(..)
  , substBlockID
  , Reg(..)
  , substReg
  , traverseCFG

    -- * Atoms
  , Atom(..)
  , substAtom
  , AtomSource(..)
  , substAtomSource
  , mkInputAtoms
  , AtomValue(..)
  , typeOfAtomValue
  , substAtomValue

    -- * Values
  , Value(..)
  , typeOfValue
  , substValue
  , ValueSet
  , substValueSet

    -- * Blocks
  , Block
  , mkBlock
  , blockID
  , blockStmts
  , blockTerm
  , blockExtraInputs
  , blockKnownInputs
  , blockAssignedValues
  , substBlock

    -- * Statements
  , Stmt(..)
  , substStmt, substPosdStmt, mapStmtAtom
  , TermStmt(..)
  , termStmtInputs
  , termNextLabels
  , substTermStmt, substPosdTermStmt
  , foldStmtInputs

    -- * Expressions
  , Expr(..)
  , exprType
  , substExpr

    -- * Re-exports
  , module Lang.Crucible.CFG.Common
  ) where

import qualified Data.Foldable as Fold
import           Data.Kind (Type)
import qualified Data.Map.Strict as Map
import           Data.Maybe (fromMaybe)
import           Data.Parameterized.Classes
import           Data.Parameterized.Context as Ctx
import           Data.Parameterized.Nonce
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC
import           Data.Sequence (Seq)
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.String
import           Data.Word (Word64)
import           Prettyprinter

import           What4.ProgramLoc
import           What4.Symbol

import           Lang.Crucible.CFG.Common
import           Lang.Crucible.CFG.Expr
import           Lang.Crucible.FunctionHandle
import           Lang.Crucible.Panic (panic)
import           Lang.Crucible.Syntax (IsExpr(..))
import           Lang.Crucible.Types

-- | Print list of documents separated by commas and spaces.
commas :: [Doc ann] -> Doc ann
commas :: forall ann. [Doc ann] -> Doc ann
commas [Doc ann]
l = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hcat (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate (Doc ann
forall ann. Doc ann
comma Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
' ') [Doc ann]
l)

------------------------------------------------------------------------
-- Label

-- | A label for a block that does not expect an input.
newtype Label s = Label { forall s. Label s -> Nonce s UnitType
labelId :: Nonce s UnitType }

labelInt :: Label s -> Word64
labelInt :: forall s. Label s -> Word64
labelInt = Nonce s UnitType -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Nonce s UnitType -> Word64)
-> (Label s -> Nonce s UnitType) -> Label s -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label s -> Nonce s UnitType
forall s. Label s -> Nonce s UnitType
labelId

instance Eq (Label s) where
  Label Nonce s UnitType
i == :: Label s -> Label s -> Bool
== Label Nonce s UnitType
j = Nonce s UnitType
i Nonce s UnitType -> Nonce s UnitType -> Bool
forall a. Eq a => a -> a -> Bool
== Nonce s UnitType
j

instance Ord (Label s) where
  Label Nonce s UnitType
i compare :: Label s -> Label s -> Ordering
`compare` Label Nonce s UnitType
j = Nonce s UnitType
i Nonce s UnitType -> Nonce s UnitType -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Nonce s UnitType
j

instance Show (Label s) where
  show :: Label s -> String
show (Label Nonce s UnitType
i) = Char
'%' Char -> ShowS
forall a. a -> [a] -> [a]
: Word64 -> String
forall a. Show a => a -> String
show (Nonce s UnitType -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue Nonce s UnitType
i)

instance Pretty (Label s) where
  pretty :: forall ann. Label s -> Doc ann
pretty (Label Nonce s UnitType
i) = Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'%' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall ann. Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Nonce s UnitType -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue Nonce s UnitType
i)

substLabel :: Functor m
           => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
           -> Label s
           -> m (Label s')
substLabel :: forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
l = Nonce s' UnitType -> Label s'
forall s. Nonce s UnitType -> Label s
Label (Nonce s' UnitType -> Label s')
-> m (Nonce s' UnitType) -> m (Label s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Nonce s UnitType -> m (Nonce s' UnitType)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Label s -> Nonce s UnitType
forall s. Label s -> Nonce s UnitType
labelId Label s
l)

------------------------------------------------------------------------
-- LambdaLabel

-- | A label for a block that expects an argument of a specific type.
data LambdaLabel (s :: Type) (tp :: CrucibleType)
   = LambdaLabel
      { forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId :: !(Nonce s tp)
        -- ^ Nonce that uniquely identifies this label within the CFG.
      , forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom :: Atom s tp
        -- ^ The atom to store the output result in.
        --
        -- Note. This must be lazy to break a recursive cycle.
      }

lambdaInt :: LambdaLabel s tp -> Word64
lambdaInt :: forall s (tp :: CrucibleType). LambdaLabel s tp -> Word64
lambdaInt = Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Nonce s tp -> Word64)
-> (LambdaLabel s tp -> Nonce s tp) -> LambdaLabel s tp -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LambdaLabel s tp -> Nonce s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId

instance Show (LambdaLabel s tp) where
  show :: LambdaLabel s tp -> String
show LambdaLabel s tp
l = Char
'%' Char -> ShowS
forall a. a -> [a] -> [a]
: Word64 -> String
forall a. Show a => a -> String
show (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (LambdaLabel s tp -> Nonce s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s tp
l))

instance Pretty (LambdaLabel s tp) where
  pretty :: forall ann. LambdaLabel s tp -> Doc ann
pretty LambdaLabel s tp
l = Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'%' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall ann. Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (LambdaLabel s tp -> Nonce s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s tp
l))

substLambdaLabel :: Applicative m
                 => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
                 -> LambdaLabel s tp
                 -> m (LambdaLabel s' tp)
substLambdaLabel :: forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f LambdaLabel s tp
ll =
  Nonce s' tp -> Atom s' tp -> LambdaLabel s' tp
forall s (tp :: CrucibleType).
Nonce s tp -> Atom s tp -> LambdaLabel s tp
LambdaLabel (Nonce s' tp -> Atom s' tp -> LambdaLabel s' tp)
-> m (Nonce s' tp) -> m (Atom s' tp -> LambdaLabel s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Nonce s tp -> m (Nonce s' tp)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (LambdaLabel s tp -> Nonce s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s tp
ll) m (Atom s' tp -> LambdaLabel s' tp)
-> m (Atom s' tp) -> m (LambdaLabel s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom LambdaLabel s tp
ll)

------------------------------------------------------------------------
-- BlockID

-- | A label for a block is either a standard label, or a label expecting an input.
data BlockID (s :: Type) where
  LabelID :: Label s -> BlockID s
  LambdaID :: LambdaLabel s tp -> BlockID s

instance Show (BlockID s) where
  show :: BlockID s -> String
show (LabelID Label s
l) = Label s -> String
forall a. Show a => a -> String
show Label s
l
  show (LambdaID LambdaLabel s tp
l) = LambdaLabel s tp -> String
forall a. Show a => a -> String
show LambdaLabel s tp
l

instance Eq (BlockID s) where
  LabelID Label s
x == :: BlockID s -> BlockID s -> Bool
== LabelID Label s
y = Label s
x Label s -> Label s -> Bool
forall a. Eq a => a -> a -> Bool
== Label s
y
  LambdaID LambdaLabel s tp
x == LambdaID LambdaLabel s tp
y = Maybe (tp :~: tp) -> Bool
forall a. Maybe a -> Bool
isJust (LambdaLabel s tp -> LambdaLabel s 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).
LambdaLabel s a -> LambdaLabel s b -> Maybe (a :~: b)
testEquality LambdaLabel s tp
x LambdaLabel s tp
y)
  BlockID s
_ == BlockID s
_ = Bool
False

instance Ord (BlockID s) where
  LabelID  Label s
x compare :: BlockID s -> BlockID s -> Ordering
`compare` LambdaID LambdaLabel s tp
y = Word64 -> Word64 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Label s -> Word64
forall s. Label s -> Word64
labelInt Label s
x) (LambdaLabel s tp -> Word64
forall s (tp :: CrucibleType). LambdaLabel s tp -> Word64
lambdaInt LambdaLabel s tp
y)
  LabelID  Label s
x `compare` LabelID  Label s
y = Label s -> Label s -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Label s
x Label s
y
  LambdaID LambdaLabel s tp
x `compare` LabelID  Label s
y = Word64 -> Word64 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (LambdaLabel s tp -> Word64
forall s (tp :: CrucibleType). LambdaLabel s tp -> Word64
lambdaInt LambdaLabel s tp
x) (Label s -> Word64
forall s. Label s -> Word64
labelInt Label s
y)
  LambdaID LambdaLabel s tp
x `compare` LambdaID LambdaLabel s tp
y = Word64 -> Word64 -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (LambdaLabel s tp -> Word64
forall s (tp :: CrucibleType). LambdaLabel s tp -> Word64
lambdaInt LambdaLabel s tp
x) (LambdaLabel s tp -> Word64
forall s (tp :: CrucibleType). LambdaLabel s tp -> Word64
lambdaInt LambdaLabel s tp
y)

substBlockID :: Applicative m
             => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
             -> BlockID s
             -> m (BlockID s')
substBlockID :: forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> BlockID s -> m (BlockID s')
substBlockID forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f BlockID s
bid =
  case BlockID s
bid of
    LabelID Label s
l -> Label s' -> BlockID s'
forall s. Label s -> BlockID s
LabelID (Label s' -> BlockID s') -> m (Label s') -> m (BlockID s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
l
    LambdaID LambdaLabel s tp
ll -> LambdaLabel s' tp -> BlockID s'
forall s (args :: CrucibleType). LambdaLabel s args -> BlockID s
LambdaID (LambdaLabel s' tp -> BlockID s')
-> m (LambdaLabel s' tp) -> m (BlockID s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f LambdaLabel s tp
ll

-----------------------------------------------------------------------
-- AtomSource

-- | Identifies what generated an atom.
data AtomSource s (tp :: CrucibleType)
   = Assigned
     -- | Input argument to function.  They are ordered before other
     -- inputs to a program.
   | FnInput
     -- | Value passed into a lambda label.  This must appear after
     -- other expressions.
   | LambdaArg !(LambdaLabel s tp)

substAtomSource :: Applicative m
                => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
                -> AtomSource s tp
                -> m (AtomSource s' tp)
substAtomSource :: forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomSource s tp -> m (AtomSource s' tp)
substAtomSource forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f AtomSource s tp
as =
  case AtomSource s tp
as of
    AtomSource s tp
Assigned -> AtomSource s' tp -> m (AtomSource s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure AtomSource s' tp
forall s (tp :: CrucibleType). AtomSource s tp
Assigned
    AtomSource s tp
FnInput -> AtomSource s' tp -> m (AtomSource s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure AtomSource s' tp
forall s (tp :: CrucibleType). AtomSource s tp
FnInput
    LambdaArg LambdaLabel s tp
ll -> LambdaLabel s' tp -> AtomSource s' tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> AtomSource s tp
LambdaArg (LambdaLabel s' tp -> AtomSource s' tp)
-> m (LambdaLabel s' tp) -> m (AtomSource s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f LambdaLabel s tp
ll

------------------------------------------------------------------------
-- Atom

-- | An expression in the control flow graph with a unique identifier.
-- Unlike registers, atoms must be assigned exactly once.
data Atom s (tp :: CrucibleType)
   = Atom { forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition :: !Position
            -- ^ Position where register was declared (used for debugging).
          , forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId :: !(Nonce s tp)
            -- ^ Unique identifier for atom.
          , forall s (tp :: CrucibleType). Atom s tp -> AtomSource s tp
atomSource :: !(AtomSource s tp)
            -- ^ How the atom expression was defined.
          , forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom :: !(TypeRepr tp)
          }

mkInputAtoms :: forall m s init
              . Monad m
             => NonceGenerator m s
             -> Position
             -> CtxRepr init
             -> m (Assignment (Atom s) init)
mkInputAtoms :: forall (m :: Type -> Type) s (init :: Ctx CrucibleType).
Monad m =>
NonceGenerator m s
-> Position -> CtxRepr init -> m (Assignment (Atom s) init)
mkInputAtoms NonceGenerator m s
ng Position
p CtxRepr init
argTypes = Size init
-> (forall (tp :: CrucibleType). Index init tp -> m (Atom s tp))
-> m (Assignment (Atom s) init)
forall {k} (m :: Type -> Type) (ctx :: Ctx k) (f :: k -> Type).
Applicative m =>
Size ctx
-> (forall (tp :: k). Index ctx tp -> m (f tp))
-> m (Assignment f ctx)
Ctx.generateM (CtxRepr init -> Size init
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size CtxRepr init
argTypes) Index init tp -> m (Atom s tp)
forall (tp :: CrucibleType). Index init tp -> m (Atom s tp)
f
  where f :: Index init tp -> m (Atom s tp)
        f :: forall (tp :: CrucibleType). Index init tp -> m (Atom s tp)
f Index init tp
i = do
          Nonce s tp
n <- NonceGenerator m s -> m (Nonce s tp)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator m s
ng
          Atom s tp -> m (Atom s tp)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Atom s tp -> m (Atom s tp)) -> Atom s tp -> m (Atom s tp)
forall a b. (a -> b) -> a -> b
$
            Atom { atomPosition :: Position
atomPosition = Position
p
                 , atomId :: Nonce s tp
atomId = Nonce s tp
n
                 , atomSource :: AtomSource s tp
atomSource = AtomSource s tp
forall s (tp :: CrucibleType). AtomSource s tp
FnInput
                 , typeOfAtom :: TypeRepr tp
typeOfAtom = CtxRepr init
argTypes CtxRepr init -> Index init tp -> TypeRepr tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index init tp
i
                 }

instance TestEquality (Atom s) where
  testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
Atom s a -> Atom s b -> Maybe (a :~: b)
testEquality Atom s a
x Atom s b
y = Nonce s a -> Nonce s b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Nonce s a -> Nonce s b -> Maybe (a :~: b)
testEquality (Atom s a -> Nonce s a
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s a
x) (Atom s b -> Nonce s b
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s b
y)

instance OrdF (Atom s) where
  compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
Atom s x -> Atom s y -> OrderingF x y
compareF Atom s x
x Atom s y
y = Nonce s x -> Nonce s y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Nonce s x -> Nonce s y -> OrderingF x y
compareF (Atom s x -> Nonce s x
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s x
x) (Atom s y -> Nonce s y
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s y
y)

instance Show (Atom s tp) where
  show :: Atom s tp -> String
show Atom s tp
a = Char
'$' Char -> ShowS
forall a. a -> [a] -> [a]
: Word64 -> String
forall a. Show a => a -> String
show (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Atom s tp -> Nonce s tp
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s tp
a))

instance Pretty (Atom s tp) where
  pretty :: forall ann. Atom s tp -> Doc ann
pretty Atom s tp
a = Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'$' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall ann. Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Atom s tp -> Nonce s tp
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s tp
a))


substAtom :: Applicative m
          => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
          -> Atom s tp
          -> m (Atom s' tp)
substAtom :: forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a =
  Position
-> Nonce s' tp -> AtomSource s' tp -> TypeRepr tp -> Atom s' tp
forall s (tp :: CrucibleType).
Position
-> Nonce s tp -> AtomSource s tp -> TypeRepr tp -> Atom s tp
Atom (Position
 -> Nonce s' tp -> AtomSource s' tp -> TypeRepr tp -> Atom s' tp)
-> m Position
-> m (Nonce s' tp -> AtomSource s' tp -> TypeRepr tp -> Atom s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Position -> m Position
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Atom s tp -> Position
forall s (tp :: CrucibleType). Atom s tp -> Position
atomPosition Atom s tp
a)
       m (Nonce s' tp -> AtomSource s' tp -> TypeRepr tp -> Atom s' tp)
-> m (Nonce s' tp)
-> m (AtomSource s' tp -> TypeRepr tp -> Atom s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Nonce s tp -> m (Nonce s' tp)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Atom s tp -> Nonce s tp
forall s (tp :: CrucibleType). Atom s tp -> Nonce s tp
atomId Atom s tp
a)
       m (AtomSource s' tp -> TypeRepr tp -> Atom s' tp)
-> m (AtomSource s' tp) -> m (TypeRepr tp -> Atom s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomSource s tp -> m (AtomSource s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomSource s tp -> m (AtomSource s' tp)
substAtomSource Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Atom s tp -> AtomSource s tp
forall s (tp :: CrucibleType). Atom s tp -> AtomSource s tp
atomSource Atom s tp
a)
       m (TypeRepr tp -> Atom s' tp) -> m (TypeRepr tp) -> m (Atom s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> TypeRepr tp -> m (TypeRepr tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a)

------------------------------------------------------------------------
-- Reg

-- | A mutable value in the control flow graph.
data Reg s (tp :: CrucibleType)
   = Reg { -- | Position where register was declared (used for debugging).
           forall s (tp :: CrucibleType). Reg s tp -> Position
regPosition :: !Position
           -- | Unique identifier for register.
         , forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId :: !(Nonce s tp)
           -- | Type of register.
         , forall s (tp :: CrucibleType). Reg s tp -> TypeRepr tp
typeOfReg :: !(TypeRepr tp)
         }

instance Pretty (Reg s tp) where
  pretty :: forall ann. Reg s tp -> Doc ann
pretty Reg s tp
r = Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'r' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall ann. Word64 -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Reg s tp -> Nonce s tp
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s tp
r))

instance Show (Reg s tp) where
  show :: Reg s tp -> String
show Reg s tp
r = Char
'r' Char -> ShowS
forall a. a -> [a] -> [a]
: Word64 -> String
forall a. Show a => a -> String
show (Nonce s tp -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue (Reg s tp -> Nonce s tp
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s tp
r))

instance ShowF (Reg s)

instance TestEquality (Reg s) where
  testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
Reg s a -> Reg s b -> Maybe (a :~: b)
testEquality Reg s a
x Reg s b
y = Nonce s a -> Nonce s b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Nonce s a -> Nonce s b -> Maybe (a :~: b)
testEquality (Reg s a -> Nonce s a
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s a
x) (Reg s b -> Nonce s b
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s b
y)

instance OrdF (Reg s) where
  compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
Reg s x -> Reg s y -> OrderingF x y
compareF Reg s x
x Reg s y
y = Nonce s x -> Nonce s y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Nonce s x -> Nonce s y -> OrderingF x y
compareF (Reg s x -> Nonce s x
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s x
x) (Reg s y -> Nonce s y
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s y
y)

substReg :: Applicative m
         => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
         -> Reg s tp
         -> m (Reg s' tp)
substReg :: forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
substReg forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Reg s tp
r =
  Position -> Nonce s' tp -> TypeRepr tp -> Reg s' tp
forall s (tp :: CrucibleType).
Position -> Nonce s tp -> TypeRepr tp -> Reg s tp
Reg (Position -> Nonce s' tp -> TypeRepr tp -> Reg s' tp)
-> m Position -> m (Nonce s' tp -> TypeRepr tp -> Reg s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Position -> m Position
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Reg s tp -> Position
forall s (tp :: CrucibleType). Reg s tp -> Position
regPosition Reg s tp
r)
      m (Nonce s' tp -> TypeRepr tp -> Reg s' tp)
-> m (Nonce s' tp) -> m (TypeRepr tp -> Reg s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Nonce s tp -> m (Nonce s' tp)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Reg s tp -> Nonce s tp
forall s (tp :: CrucibleType). Reg s tp -> Nonce s tp
regId Reg s tp
r)
      m (TypeRepr tp -> Reg s' tp) -> m (TypeRepr tp) -> m (Reg s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> TypeRepr tp -> m (TypeRepr tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Reg s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Reg s tp -> TypeRepr tp
typeOfReg Reg s tp
r)

------------------------------------------------------------------------
-- Primitive operations

instance TestEquality (LambdaLabel s) where
  testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
LambdaLabel s a -> LambdaLabel s b -> Maybe (a :~: b)
testEquality LambdaLabel s a
x LambdaLabel s b
y = Nonce s a -> Nonce s b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Nonce s a -> Nonce s b -> Maybe (a :~: b)
testEquality (LambdaLabel s a -> Nonce s a
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s a
x) (LambdaLabel s b -> Nonce s b
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s b
y)

instance OrdF (LambdaLabel s) where
  compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
LambdaLabel s x -> LambdaLabel s y -> OrderingF x y
compareF LambdaLabel s x
x LambdaLabel s y
y = Nonce s x -> Nonce s y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Nonce s x -> Nonce s y -> OrderingF x y
compareF (LambdaLabel s x -> Nonce s x
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s x
x) (LambdaLabel s y -> Nonce s y
forall s (tp :: CrucibleType). LambdaLabel s tp -> Nonce s tp
lambdaId LambdaLabel s y
y)

------------------------------------------------------------------------
-- SomeValue and ValueSet

-- | A value is either a register or an atom.
data Value s (tp :: CrucibleType)
   = RegValue  !(Reg s tp)
   | AtomValue !(Atom s tp)

instance TestEquality (Value s) where
  testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
Value s a -> Value s b -> Maybe (a :~: b)
testEquality (RegValue  Reg s a
x) (RegValue Reg s b
y)  = Reg s a -> Reg s b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Reg s a -> Reg s b -> Maybe (a :~: b)
testEquality Reg s a
x Reg s b
y
  testEquality (AtomValue Atom s a
x) (AtomValue Atom s b
y) = Atom s a -> Atom s b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Atom s a -> Atom s b -> Maybe (a :~: b)
testEquality Atom s a
x Atom s b
y
  testEquality Value s a
_ Value s b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance OrdF (Value s) where
  compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
Value s x -> Value s y -> OrderingF x y
compareF (RegValue Reg s x
x) (RegValue Reg s y
y) = Reg s x -> Reg s y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Reg s x -> Reg s y -> OrderingF x y
compareF Reg s x
x Reg s y
y
  compareF RegValue{} Value s y
_ = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF Value s x
_ RegValue{} = OrderingF x y
forall {k} (x :: k) (y :: k). OrderingF x y
GTF
  compareF (AtomValue Atom s x
x) (AtomValue Atom s y
y) = Atom s x -> Atom s y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Atom s x -> Atom s y -> OrderingF x y
compareF Atom s x
x Atom s y
y

instance Pretty (Value s tp) where
  pretty :: forall ann. Value s tp -> Doc ann
pretty (RegValue  Reg s tp
r) = Reg s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg s tp -> Doc ann
pretty Reg s tp
r
  pretty (AtomValue Atom s tp
a) = Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
a

instance Show (Value s tp) where
  show :: Value s tp -> String
show (RegValue  Reg s tp
r) = Reg s tp -> String
forall a. Show a => a -> String
show Reg s tp
r
  show (AtomValue Atom s tp
a) = Atom s tp -> String
forall a. Show a => a -> String
show Atom s tp
a

instance ShowF (Value s)

typeOfValue :: Value s tp -> TypeRepr tp
typeOfValue :: forall s (tp :: CrucibleType). Value s tp -> TypeRepr tp
typeOfValue (RegValue Reg s tp
r) = Reg s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Reg s tp -> TypeRepr tp
typeOfReg Reg s tp
r
typeOfValue (AtomValue Atom s tp
a) = Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a

substValue :: Applicative m
           => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
           -> Value s tp
           -> m (Value s' tp)
substValue :: forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Value s tp -> m (Value s' tp)
substValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Value s tp
v =
  case Value s tp
v of
    RegValue Reg s tp
r -> Reg s' tp -> Value s' tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue (Reg s' tp -> Value s' tp) -> m (Reg s' tp) -> m (Value s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
substReg Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Reg s tp
r
    AtomValue Atom s tp
a -> Atom s' tp -> Value s' tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue (Atom s' tp -> Value s' tp) -> m (Atom s' tp) -> m (Value s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a

substValueAtom :: Applicative m
           => (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
           -> Value s tp
           -> m (Value s tp)
substValueAtom :: forall (m :: Type -> Type) s (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Value s tp -> m (Value s tp)
substValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Value s tp
v =
  case Value s tp
v of
    RegValue Reg s tp
r -> Value s tp -> m (Value s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Value s tp -> m (Value s tp)) -> Value s tp -> m (Value s tp)
forall a b. (a -> b) -> a -> b
$ Reg s tp -> Value s tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue Reg s tp
r
    AtomValue Atom s tp
a -> Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue (Atom s tp -> Value s tp) -> m (Atom s tp) -> m (Value s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
a

-- | A set of values.
type ValueSet s = Set (Some (Value s))

substValueSet :: Applicative m
              => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
              -> ValueSet s
              -> m (ValueSet s')
substValueSet :: forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
substValueSet forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f ValueSet s
vs =
  [Some (Value s')] -> Set (Some (Value s'))
forall a. Ord a => [a] -> Set a
Set.fromList ([Some (Value s')] -> Set (Some (Value s')))
-> m [Some (Value s')] -> m (Set (Some (Value s')))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
    (Some (Value s) -> m (Some (Value s')))
-> [Some (Value s)] -> m [Some (Value s')]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(Some Value s x
v) -> Value s' x -> Some (Value s')
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Value s' x -> Some (Value s'))
-> m (Value s' x) -> m (Some (Value s'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Value s x -> m (Value s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Value s tp -> m (Value s' tp)
substValue Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Value s x
v) (ValueSet s -> [Some (Value s)]
forall a. Set a -> [a]
Set.toList ValueSet s
vs)

------------------------------------------------------------------------
-- Expr

-- | An expression in RTL representation.
--
-- The type arguments are:
--
--   [@ext@] the extensions currently in use (use @()@ for no extension)
--
--   [@s@] a dummy variable that should almost always be universally quantified
--
--   [@tp@] the Crucible type of the expression
data Expr ext s (tp :: CrucibleType)
  = App !(App ext (Expr ext s) tp)
    -- ^ An application of an expression
  | AtomExpr !(Atom s tp)
    -- ^ An evaluated expession

instance PrettyExt ext => Pretty (Expr ext s tp) where
  pretty :: forall ann. Expr ext s tp -> Doc ann
pretty (App App ext (Expr ext s) tp
a) = (forall (x :: CrucibleType). Expr ext s x -> Doc ann)
-> forall (x :: CrucibleType). App ext (Expr ext s) x -> Doc ann
forall k (app :: (k -> Type) -> k -> Type) (f :: k -> Type) ann.
PrettyApp app =>
(forall (x :: k). f x -> Doc ann)
-> forall (x :: k). app f x -> Doc ann
forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). App ext f x -> Doc ann
ppApp Expr ext s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Expr ext s x -> Doc ann
forall (x :: CrucibleType). Expr ext s x -> Doc ann
pretty App ext (Expr ext s) tp
a
  pretty (AtomExpr Atom s tp
a) = Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
a

instance PrettyExt ext => Show (Expr ext s tp) where
  show :: Expr ext s tp -> String
show Expr ext s tp
e = Doc Any -> String
forall a. Show a => a -> String
show (Expr ext s tp -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Expr ext s tp -> Doc ann
pretty Expr ext s tp
e)

instance PrettyExt ext => ShowF (Expr ext s)

instance TypeApp (ExprExtension ext) => IsExpr (Expr ext s) where
  type ExprExt (Expr ext s) = ext
  app :: forall (tp :: CrucibleType).
App (ExprExt (Expr ext s)) (Expr ext s) tp -> Expr ext s tp
app = App ext (Expr ext s) tp -> Expr ext s tp
App (ExprExt (Expr ext s)) (Expr ext s) tp -> Expr ext s tp
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App
  asApp :: forall (tp :: CrucibleType).
Expr ext s tp -> Maybe (App (ExprExt (Expr ext s)) (Expr ext s) tp)
asApp (App App ext (Expr ext s) tp
x) = App ext (Expr ext s) tp -> Maybe (App ext (Expr ext s) tp)
forall a. a -> Maybe a
Just App ext (Expr ext s) tp
x
  asApp Expr ext s tp
_ = Maybe (App ext (Expr ext s) tp)
Maybe (App (ExprExt (Expr ext s)) (Expr ext s) tp)
forall a. Maybe a
Nothing

  -- exprType :: Expr s tp -> TypeRepr tp
  exprType :: forall (tp :: CrucibleType). Expr ext s tp -> TypeRepr tp
exprType (App App ext (Expr ext s) tp
a)          = App ext (Expr ext s) tp -> TypeRepr tp
forall (f :: CrucibleType -> Type) (x :: CrucibleType).
App ext f x -> TypeRepr x
forall (app :: (CrucibleType -> Type) -> CrucibleType -> Type)
       (f :: CrucibleType -> Type) (x :: CrucibleType).
TypeApp app =>
app f x -> TypeRepr x
appType App ext (Expr ext s) tp
a
  exprType (AtomExpr Atom s tp
a)     = Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a

instance IsString (Expr ext s (StringType Unicode)) where
  fromString :: String -> Expr ext s (StringType Unicode)
fromString String
s = App ext (Expr ext s) (StringType Unicode)
-> Expr ext s (StringType Unicode)
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (StringLiteral Unicode -> App ext (Expr ext s) (StringType Unicode)
forall (si :: StringInfo) ext (f :: CrucibleType -> Type).
StringLiteral si -> App ext f ('BaseToType (BaseStringType si))
StringLit (String -> StringLiteral Unicode
forall a. IsString a => String -> a
fromString String
s))

substExpr :: ( Applicative m, TraverseExt ext )
          => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
          -> Expr ext s tp
          -> m (Expr ext s' tp)
substExpr :: forall (m :: Type -> Type) ext s s' (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Expr ext s tp -> m (Expr ext s' tp)
substExpr forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Expr ext s tp
expr =
  case Expr ext s tp
expr of
    App App ext (Expr ext s) tp
ap -> App ext (Expr ext s') tp -> Expr ext s' tp
forall ext s (tp :: CrucibleType).
App ext (Expr ext s) tp -> Expr ext s tp
App (App ext (Expr ext s') tp -> Expr ext s' tp)
-> m (App ext (Expr ext s') tp) -> m (Expr ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Expr ext s x -> m (Expr ext s' x))
-> forall (x :: CrucibleType).
   App ext (Expr ext s) x -> m (App ext (Expr ext s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType). App ext f x -> m (App ext g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Expr ext s x -> m (Expr ext s' x)
forall (m :: Type -> Type) ext s s' (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Expr ext s tp -> m (Expr ext s' tp)
substExpr Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) App ext (Expr ext s) tp
ap
    AtomExpr Atom s tp
a -> Atom s' tp -> Expr ext s' tp
forall ext s (tp :: CrucibleType). Atom s tp -> Expr ext s tp
AtomExpr (Atom s' tp -> Expr ext s' tp)
-> m (Atom s' tp) -> m (Expr ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a


------------------------------------------------------------------------
-- AtomValue

-- | The value of an assigned atom.
data AtomValue ext s (tp :: CrucibleType) where
  -- Evaluate an expression
  EvalApp :: !(App ext (Atom s) tp) -> AtomValue ext s tp
  -- Read a value from a register
  ReadReg :: !(Reg s tp) -> AtomValue ext s tp
  -- Evaluate an extension statement
  EvalExt :: !(StmtExtension ext (Atom s) tp) -> AtomValue ext s tp
  -- Read from a global vlalue
  ReadGlobal :: !(GlobalVar tp) -> AtomValue ext s tp
  -- Read from a reference cell
  ReadRef :: !(Atom s (ReferenceType tp)) -> AtomValue ext s tp
  -- Create a fresh reference cell
  NewRef :: !(Atom s tp) -> AtomValue ext s (ReferenceType tp)
  -- Create a fresh empty reference cell
  NewEmptyRef :: !(TypeRepr tp) -> AtomValue ext s (ReferenceType tp)
  -- Create a fresh uninterpreted constant of base type
  FreshConstant :: !(BaseTypeRepr bt) -> !(Maybe SolverSymbol) -> AtomValue ext s (BaseToType bt)
  -- Create a fresh uninterpreted constant of floating point type
  FreshFloat :: !(FloatInfoRepr fi) -> !(Maybe SolverSymbol) -> AtomValue ext s (FloatType fi)
  -- Create a fresh uninterpreted constant of natural number type
  FreshNat :: !(Maybe SolverSymbol) -> AtomValue ext s NatType

  Call :: !(Atom s (FunctionHandleType args ret))
       -> !(Assignment (Atom s) args)
       -> !(TypeRepr ret)
       -> AtomValue ext s ret

instance PrettyExt ext => Show (AtomValue ext s tp) where
  show :: AtomValue ext s tp -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (AtomValue ext s tp -> Doc Any) -> AtomValue ext s tp -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomValue ext s tp -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. AtomValue ext s tp -> Doc ann
pretty

instance PrettyExt ext => Pretty (AtomValue ext s tp) where
  pretty :: forall ann. AtomValue ext s tp -> Doc ann
pretty AtomValue ext s tp
v =
    case AtomValue ext s tp
v of
      EvalApp App ext (Atom s) tp
ap -> (forall (x :: CrucibleType). Atom s x -> Doc ann)
-> forall (x :: CrucibleType). App ext (Atom s) x -> Doc ann
forall k (app :: (k -> Type) -> k -> Type) (f :: k -> Type) ann.
PrettyApp app =>
(forall (x :: k). f x -> Doc ann)
-> forall (x :: k). app f x -> Doc ann
forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). App ext f x -> Doc ann
ppApp Atom s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s x -> Doc ann
forall (x :: CrucibleType). Atom s x -> Doc ann
pretty App ext (Atom s) tp
ap
      EvalExt StmtExtension ext (Atom s) tp
st -> (forall (x :: CrucibleType). Atom s x -> Doc ann)
-> forall (x :: CrucibleType).
   StmtExtension ext (Atom s) x -> Doc ann
forall k (app :: (k -> Type) -> k -> Type) (f :: k -> Type) ann.
PrettyApp app =>
(forall (x :: k). f x -> Doc ann)
-> forall (x :: k). app f x -> Doc ann
forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). StmtExtension ext f x -> Doc ann
ppApp Atom s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s x -> Doc ann
forall (x :: CrucibleType). Atom s x -> Doc ann
pretty StmtExtension ext (Atom s) tp
st
      ReadReg Reg s tp
r -> Reg s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg s tp -> Doc ann
pretty Reg s tp
r
      ReadGlobal GlobalVar tp
g -> Doc ann
"global" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. GlobalVar tp -> Doc ann
pretty GlobalVar tp
g
      ReadRef Atom s (ReferenceType tp)
r -> Doc ann
"!" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Atom s (ReferenceType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (ReferenceType tp) -> Doc ann
pretty Atom s (ReferenceType tp)
r
      NewRef Atom s tp
a -> Doc ann
"newref" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
a
      NewEmptyRef TypeRepr tp
tp -> Doc ann
"emptyref" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> TypeRepr tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeRepr tp -> Doc ann
pretty TypeRepr tp
tp
      -- TODO: replace viaShow once we have instance Pretty SolverSymbol
      FreshConstant BaseTypeRepr bt
bt Maybe SolverSymbol
nm -> Doc ann
"fresh" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> BaseTypeRepr bt -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BaseTypeRepr bt -> Doc ann
pretty BaseTypeRepr bt
bt Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
-> (SolverSymbol -> Doc ann) -> Maybe SolverSymbol -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
forall a. Monoid a => a
mempty SolverSymbol -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Maybe SolverSymbol
nm
      FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
nm -> Doc ann
"fresh" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FloatInfoRepr fi -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FloatInfoRepr fi -> Doc ann
pretty FloatInfoRepr fi
fi Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
-> (SolverSymbol -> Doc ann) -> Maybe SolverSymbol -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
forall a. Monoid a => a
mempty SolverSymbol -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Maybe SolverSymbol
nm
      FreshNat Maybe SolverSymbol
nm -> Doc ann
"fresh nat" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
-> (SolverSymbol -> Doc ann) -> Maybe SolverSymbol -> Doc ann
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc ann
forall a. Monoid a => a
mempty SolverSymbol -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Maybe SolverSymbol
nm
      Call Atom s (FunctionHandleType args tp)
f Assignment (Atom s) args
args TypeRepr tp
_ -> Atom s (FunctionHandleType args tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (FunctionHandleType args tp) -> Doc ann
pretty Atom s (FunctionHandleType args tp)
f Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
commas ((forall (x :: CrucibleType). Atom s x -> Doc ann)
-> forall (x :: Ctx CrucibleType).
   Assignment (Atom s) x -> [Doc ann]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> Type) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC Atom s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s x -> Doc ann
forall (x :: CrucibleType). Atom s x -> Doc ann
pretty Assignment (Atom s) args
args))

typeOfAtomValue :: (TypeApp (StmtExtension ext) , TypeApp (ExprExtension ext))
                => AtomValue ext s tp -> TypeRepr tp
typeOfAtomValue :: forall ext s (tp :: CrucibleType).
(TypeApp (StmtExtension ext), TypeApp (ExprExtension ext)) =>
AtomValue ext s tp -> TypeRepr tp
typeOfAtomValue AtomValue ext s tp
v =
  case AtomValue ext s tp
v of
    EvalApp App ext (Atom s) tp
a -> App ext (Atom s) tp -> TypeRepr tp
forall (f :: CrucibleType -> Type) (x :: CrucibleType).
App ext f x -> TypeRepr x
forall (app :: (CrucibleType -> Type) -> CrucibleType -> Type)
       (f :: CrucibleType -> Type) (x :: CrucibleType).
TypeApp app =>
app f x -> TypeRepr x
appType App ext (Atom s) tp
a
    EvalExt StmtExtension ext (Atom s) tp
stmt -> StmtExtension ext (Atom s) tp -> TypeRepr tp
forall (f :: CrucibleType -> Type) (x :: CrucibleType).
StmtExtension ext f x -> TypeRepr x
forall (app :: (CrucibleType -> Type) -> CrucibleType -> Type)
       (f :: CrucibleType -> Type) (x :: CrucibleType).
TypeApp app =>
app f x -> TypeRepr x
appType StmtExtension ext (Atom s) tp
stmt
    ReadReg Reg s tp
r -> Reg s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Reg s tp -> TypeRepr tp
typeOfReg Reg s tp
r
    ReadGlobal GlobalVar tp
r -> GlobalVar tp -> TypeRepr tp
forall (tp :: CrucibleType). GlobalVar tp -> TypeRepr tp
globalType GlobalVar tp
r
    ReadRef Atom s (ReferenceType tp)
r -> case Atom s (ReferenceType tp) -> TypeRepr (ReferenceType tp)
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s (ReferenceType tp)
r of
                   ReferenceRepr TypeRepr a
tpr -> TypeRepr tp
TypeRepr a
tpr
    NewRef Atom s tp
a -> TypeRepr tp -> TypeRepr ('ReferenceType tp)
forall (a :: CrucibleType).
TypeRepr a -> TypeRepr ('ReferenceType a)
ReferenceRepr (Atom s tp -> TypeRepr tp
forall s (tp :: CrucibleType). Atom s tp -> TypeRepr tp
typeOfAtom Atom s tp
a)
    NewEmptyRef TypeRepr tp
tp -> TypeRepr tp -> TypeRepr ('ReferenceType tp)
forall (a :: CrucibleType).
TypeRepr a -> TypeRepr ('ReferenceType a)
ReferenceRepr TypeRepr tp
tp
    FreshConstant BaseTypeRepr bt
bt Maybe SolverSymbol
_ -> BaseTypeRepr bt -> TypeRepr ('BaseToType bt)
forall (bt :: BaseType).
BaseTypeRepr bt -> TypeRepr (BaseToType bt)
baseToType BaseTypeRepr bt
bt
    FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
_ -> FloatInfoRepr fi -> TypeRepr ('FloatType fi)
forall (flt :: FloatInfo).
FloatInfoRepr flt -> TypeRepr ('FloatType flt)
FloatRepr FloatInfoRepr fi
fi
    FreshNat Maybe SolverSymbol
_ -> TypeRepr tp
TypeRepr 'NatType
NatRepr
    Call Atom s (FunctionHandleType args tp)
_ Assignment (Atom s) args
_ TypeRepr tp
r -> TypeRepr tp
r

-- | Fold over all values in an 'AtomValue'.
foldAtomValueInputs :: TraverseExt ext
                    => (forall x . Value s x -> b -> b)
                    -> AtomValue ext s tp -> b -> b
foldAtomValueInputs :: forall ext s b (tp :: CrucibleType).
TraverseExt ext =>
(forall (x :: CrucibleType). Value s x -> b -> b)
-> AtomValue ext s tp -> b -> b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (ReadReg Reg s tp
r)         b
b = Value s tp -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Reg s tp -> Value s tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue Reg s tp
r) b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (EvalExt StmtExtension ext (Atom s) tp
stmt)      b
b = (forall (x :: CrucibleType). Atom s x -> b -> b)
-> forall (x :: CrucibleType).
   b -> StmtExtension ext (Atom s) x -> b
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). f x -> b -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: CrucibleType -> Type) b.
(forall (x :: CrucibleType). f x -> b -> b)
-> forall (x :: CrucibleType). b -> StmtExtension ext f x -> b
foldrFC (Value s x -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Value s x -> b -> b)
-> (Atom s x -> Value s x) -> Atom s x -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom s x -> Value s x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue) b
b StmtExtension ext (Atom s) tp
stmt
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
_ (ReadGlobal GlobalVar tp
_)      b
b = b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (ReadRef Atom s (ReferenceType tp)
r)         b
b = Value s (ReferenceType tp) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (ReferenceType tp) -> Value s (ReferenceType tp)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (ReferenceType tp)
r) b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
_ (NewEmptyRef TypeRepr tp
_)     b
b = b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (NewRef Atom s tp
a)          b
b = Value s tp -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (EvalApp App ext (Atom s) tp
app0)      b
b = (forall (x :: CrucibleType). Atom s x -> b -> b)
-> b -> App ext (Atom s) tp -> b
forall ext (f :: CrucibleType -> Type) r (tp :: CrucibleType).
TraversableFC (ExprExtension ext) =>
(forall (x :: CrucibleType). f x -> r -> r)
-> r -> App ext f tp -> r
foldApp (Value s x -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Value s x -> b -> b)
-> (Atom s x -> Value s x) -> Atom s x -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom s x -> Value s x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue) b
b App ext (Atom s) tp
app0
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
_ (FreshConstant BaseTypeRepr bt
_ Maybe SolverSymbol
_) b
b = b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
_ (FreshFloat FloatInfoRepr fi
_ Maybe SolverSymbol
_)    b
b = b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
_ (FreshNat Maybe SolverSymbol
_)        b
b = b
b
foldAtomValueInputs forall (x :: CrucibleType). Value s x -> b -> b
f (Call Atom s (FunctionHandleType args tp)
g Assignment (Atom s) args
a TypeRepr tp
_)        b
b = Value s (FunctionHandleType args tp) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (FunctionHandleType args tp)
-> Value s (FunctionHandleType args tp)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (FunctionHandleType args tp)
g) ((forall (x :: CrucibleType). Atom s x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment (Atom s) x -> b
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). f x -> b -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: CrucibleType -> Type) b.
(forall (x :: CrucibleType). f x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment f x -> b
foldrFC' (Value s x -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Value s x -> b -> b)
-> (Atom s x -> Value s x) -> Atom s x -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom s x -> Value s x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue) b
b Assignment (Atom s) args
a)

substAtomValue :: ( Applicative m, TraverseExt ext )
               => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
               -> AtomValue ext s tp
               -> m (AtomValue ext s' tp)
substAtomValue :: forall (m :: Type -> Type) ext s s' (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomValue ext s tp -> m (AtomValue ext s' tp)
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (ReadReg Reg s tp
r) = Reg s' tp -> AtomValue ext s' tp
forall s (tp :: CrucibleType) ext. Reg s tp -> AtomValue ext s tp
ReadReg (Reg s' tp -> AtomValue ext s' tp)
-> m (Reg s' tp) -> m (AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
substReg Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Reg s tp
r
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (EvalExt StmtExtension ext (Atom s) tp
stmt) = StmtExtension ext (Atom s') tp -> AtomValue ext s' tp
forall ext s (tp :: CrucibleType).
StmtExtension ext (Atom s) tp -> AtomValue ext s tp
EvalExt (StmtExtension ext (Atom s') tp -> AtomValue ext s' tp)
-> m (StmtExtension ext (Atom s') tp) -> m (AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Atom s x -> m (Atom s' x))
-> forall (x :: CrucibleType).
   StmtExtension ext (Atom s) x -> m (StmtExtension ext (Atom s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType).
   StmtExtension ext f x -> m (StmtExtension ext g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s x -> m (Atom s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) StmtExtension ext (Atom s) tp
stmt
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
_ (ReadGlobal GlobalVar tp
g) = AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s' tp -> m (AtomValue ext s' tp))
-> AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a b. (a -> b) -> a -> b
$ GlobalVar tp -> AtomValue ext s' tp
forall (tp :: CrucibleType) ext s.
GlobalVar tp -> AtomValue ext s tp
ReadGlobal GlobalVar tp
g
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (ReadRef Atom s (ReferenceType tp)
r) = Atom s' (ReferenceType tp) -> AtomValue ext s' tp
forall s (tp :: CrucibleType) ext.
Atom s (ReferenceType tp) -> AtomValue ext s tp
ReadRef (Atom s' (ReferenceType tp) -> AtomValue ext s' tp)
-> m (Atom s' (ReferenceType tp)) -> m (AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (ReferenceType tp) -> m (Atom s' (ReferenceType tp))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (ReferenceType tp)
r
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
_ (NewEmptyRef TypeRepr tp
tp) = AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s' tp -> m (AtomValue ext s' tp))
-> AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a b. (a -> b) -> a -> b
$ TypeRepr tp -> AtomValue ext s' ('ReferenceType tp)
forall (args :: CrucibleType) ext s.
TypeRepr args -> AtomValue ext s (ReferenceType args)
NewEmptyRef TypeRepr tp
tp
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (NewRef Atom s tp
a) = Atom s' tp -> AtomValue ext s' tp
Atom s' tp -> AtomValue ext s' ('ReferenceType tp)
forall s (args :: CrucibleType) ext.
Atom s args -> AtomValue ext s (ReferenceType args)
NewRef (Atom s' tp -> AtomValue ext s' tp)
-> m (Atom s' tp) -> m (AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (EvalApp App ext (Atom s) tp
ap) = App ext (Atom s') tp -> AtomValue ext s' tp
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (App ext (Atom s') tp -> AtomValue ext s' tp)
-> m (App ext (Atom s') tp) -> m (AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Atom s x -> m (Atom s' x))
-> forall (x :: CrucibleType).
   App ext (Atom s) x -> m (App ext (Atom s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType). App ext f x -> m (App ext g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s x -> m (Atom s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) App ext (Atom s) tp
ap
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
_ (FreshConstant BaseTypeRepr bt
tp Maybe SolverSymbol
sym) = AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s' tp -> m (AtomValue ext s' tp))
-> AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr bt
-> Maybe SolverSymbol -> AtomValue ext s' ('BaseToType bt)
forall (args :: BaseType) ext s.
BaseTypeRepr args
-> Maybe SolverSymbol -> AtomValue ext s (BaseToType args)
FreshConstant BaseTypeRepr bt
tp Maybe SolverSymbol
sym
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
_ (FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
sym)    = AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s' tp -> m (AtomValue ext s' tp))
-> AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a b. (a -> b) -> a -> b
$ FloatInfoRepr fi
-> Maybe SolverSymbol -> AtomValue ext s' ('FloatType fi)
forall (args :: FloatInfo) ext s.
FloatInfoRepr args
-> Maybe SolverSymbol -> AtomValue ext s (FloatType args)
FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
sym
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
_ (FreshNat Maybe SolverSymbol
sym)         = AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s' tp -> m (AtomValue ext s' tp))
-> AtomValue ext s' tp -> m (AtomValue ext s' tp)
forall a b. (a -> b) -> a -> b
$ Maybe SolverSymbol -> AtomValue ext s' 'NatType
forall ext s. Maybe SolverSymbol -> AtomValue ext s 'NatType
FreshNat Maybe SolverSymbol
sym
substAtomValue forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Call Atom s (FunctionHandleType args tp)
g Assignment (Atom s) args
as TypeRepr tp
ret) = Atom s' (FunctionHandleType args tp)
-> Assignment (Atom s') args -> TypeRepr tp -> AtomValue ext s' tp
forall s (args :: Ctx CrucibleType) (ret :: CrucibleType) ext.
Atom s (FunctionHandleType args ret)
-> Assignment (Atom s) args -> TypeRepr ret -> AtomValue ext s ret
Call (Atom s' (FunctionHandleType args tp)
 -> Assignment (Atom s') args -> TypeRepr tp -> AtomValue ext s' tp)
-> m (Atom s' (FunctionHandleType args tp))
-> m (Assignment (Atom s') args
      -> TypeRepr tp -> AtomValue ext s' tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (FunctionHandleType args tp)
-> m (Atom s' (FunctionHandleType args tp))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (FunctionHandleType args tp)
g
                                        m (Assignment (Atom s') args -> TypeRepr tp -> AtomValue ext s' tp)
-> m (Assignment (Atom s') args)
-> m (TypeRepr tp -> AtomValue ext s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Atom s x -> m (Atom s' x))
-> forall (x :: Ctx CrucibleType).
   Assignment (Atom s) x -> m (Assignment (Atom s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> m (Assignment g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s x -> m (Atom s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) Assignment (Atom s) args
as
                                        m (TypeRepr tp -> AtomValue ext s' tp)
-> m (TypeRepr tp) -> m (AtomValue ext s' tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> TypeRepr tp -> m (TypeRepr tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TypeRepr tp
ret

mapAtomValueAtom :: ( Applicative m, TraverseExt ext )
               => (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
               -> AtomValue ext s tp
               -> m (AtomValue ext s tp)
mapAtomValueAtom :: forall (m :: Type -> Type) ext s (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (ReadReg Reg s tp
r) = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ Reg s tp -> AtomValue ext s tp
forall s (tp :: CrucibleType) ext. Reg s tp -> AtomValue ext s tp
ReadReg Reg s tp
r
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f (EvalExt StmtExtension ext (Atom s) tp
stmt) = StmtExtension ext (Atom s) tp -> AtomValue ext s tp
forall ext s (tp :: CrucibleType).
StmtExtension ext (Atom s) tp -> AtomValue ext s tp
EvalExt (StmtExtension ext (Atom s) tp -> AtomValue ext s tp)
-> m (StmtExtension ext (Atom s) tp) -> m (AtomValue ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> forall (x :: CrucibleType).
   StmtExtension ext (Atom s) x -> m (StmtExtension ext (Atom s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType).
   StmtExtension ext f x -> m (StmtExtension ext g x)
traverseFC Atom s x -> m (Atom s x)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f StmtExtension ext (Atom s) tp
stmt
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (ReadGlobal GlobalVar tp
g) = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ GlobalVar tp -> AtomValue ext s tp
forall (tp :: CrucibleType) ext s.
GlobalVar tp -> AtomValue ext s tp
ReadGlobal GlobalVar tp
g
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f (ReadRef Atom s (ReferenceType tp)
r) = Atom s (ReferenceType tp) -> AtomValue ext s tp
forall s (tp :: CrucibleType) ext.
Atom s (ReferenceType tp) -> AtomValue ext s tp
ReadRef (Atom s (ReferenceType tp) -> AtomValue ext s tp)
-> m (Atom s (ReferenceType tp)) -> m (AtomValue ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s (ReferenceType tp) -> m (Atom s (ReferenceType tp))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (ReferenceType tp)
r
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (NewEmptyRef TypeRepr tp
tp) = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ TypeRepr tp -> AtomValue ext s ('ReferenceType tp)
forall (args :: CrucibleType) ext s.
TypeRepr args -> AtomValue ext s (ReferenceType args)
NewEmptyRef TypeRepr tp
tp
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f (NewRef Atom s tp
a) = Atom s tp -> AtomValue ext s tp
Atom s tp -> AtomValue ext s ('ReferenceType tp)
forall s (args :: CrucibleType) ext.
Atom s args -> AtomValue ext s (ReferenceType args)
NewRef (Atom s tp -> AtomValue ext s tp)
-> m (Atom s tp) -> m (AtomValue ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
a
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f (EvalApp App ext (Atom s) tp
ap) = App ext (Atom s) tp -> AtomValue ext s tp
forall ext s (tp :: CrucibleType).
App ext (Atom s) tp -> AtomValue ext s tp
EvalApp (App ext (Atom s) tp -> AtomValue ext s tp)
-> m (App ext (Atom s) tp) -> m (AtomValue ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> forall (x :: CrucibleType).
   App ext (Atom s) x -> m (App ext (Atom s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType). App ext f x -> m (App ext g x)
traverseFC Atom s x -> m (Atom s x)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f App ext (Atom s) tp
ap
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (FreshConstant BaseTypeRepr bt
tp Maybe SolverSymbol
sym) = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ BaseTypeRepr bt
-> Maybe SolverSymbol -> AtomValue ext s ('BaseToType bt)
forall (args :: BaseType) ext s.
BaseTypeRepr args
-> Maybe SolverSymbol -> AtomValue ext s (BaseToType args)
FreshConstant BaseTypeRepr bt
tp Maybe SolverSymbol
sym
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
sym)    = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ FloatInfoRepr fi
-> Maybe SolverSymbol -> AtomValue ext s ('FloatType fi)
forall (args :: FloatInfo) ext s.
FloatInfoRepr args
-> Maybe SolverSymbol -> AtomValue ext s (FloatType args)
FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
sym
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
_ (FreshNat Maybe SolverSymbol
sym)         = AtomValue ext s tp -> m (AtomValue ext s tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (AtomValue ext s tp -> m (AtomValue ext s tp))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall a b. (a -> b) -> a -> b
$ Maybe SolverSymbol -> AtomValue ext s 'NatType
forall ext s. Maybe SolverSymbol -> AtomValue ext s 'NatType
FreshNat Maybe SolverSymbol
sym
mapAtomValueAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f (Call Atom s (FunctionHandleType args tp)
g Assignment (Atom s) args
as TypeRepr tp
ret) = Atom s (FunctionHandleType args tp)
-> Assignment (Atom s) args -> TypeRepr tp -> AtomValue ext s tp
forall s (args :: Ctx CrucibleType) (ret :: CrucibleType) ext.
Atom s (FunctionHandleType args ret)
-> Assignment (Atom s) args -> TypeRepr ret -> AtomValue ext s ret
Call (Atom s (FunctionHandleType args tp)
 -> Assignment (Atom s) args -> TypeRepr tp -> AtomValue ext s tp)
-> m (Atom s (FunctionHandleType args tp))
-> m (Assignment (Atom s) args
      -> TypeRepr tp -> AtomValue ext s tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s (FunctionHandleType args tp)
-> m (Atom s (FunctionHandleType args tp))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (FunctionHandleType args tp)
g
                                        m (Assignment (Atom s) args -> TypeRepr tp -> AtomValue ext s tp)
-> m (Assignment (Atom s) args)
-> m (TypeRepr tp -> AtomValue ext s tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> forall (x :: Ctx CrucibleType).
   Assignment (Atom s) x -> m (Assignment (Atom s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> m (Assignment g x)
traverseFC Atom s x -> m (Atom s x)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Assignment (Atom s) args
as
                                        m (TypeRepr tp -> AtomValue ext s tp)
-> m (TypeRepr tp) -> m (AtomValue ext s tp)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> TypeRepr tp -> m (TypeRepr tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TypeRepr tp
ret

ppAtomBinding :: PrettyExt ext => Atom s tp -> AtomValue ext s tp -> Doc ann
ppAtomBinding :: forall ext s (tp :: CrucibleType) ann.
PrettyExt ext =>
Atom s tp -> AtomValue ext s tp -> Doc ann
ppAtomBinding Atom s tp
a AtomValue ext s tp
v = Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> AtomValue ext s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. AtomValue ext s tp -> Doc ann
pretty AtomValue ext s tp
v

------------------------------------------------------------------------
-- Stmt

-- | Statement in control flow graph.
data Stmt ext s
   = forall tp . SetReg     !(Reg s tp)       !(Atom s tp)
   | forall tp . WriteGlobal  !(GlobalVar tp) !(Atom s tp)
   | forall tp . WriteRef !(Atom s (ReferenceType tp)) !(Atom s tp)
   | forall tp . DropRef  !(Atom s (ReferenceType tp))
   | forall tp . DefineAtom !(Atom s tp)      !(AtomValue ext s tp)
   | Print      !(Atom s (StringType Unicode))
     -- | Assert that the given expression is true.
   | Assert !(Atom s BoolType) !(Atom s (StringType Unicode))
     -- | Assume the given expression.
   | Assume !(Atom s BoolType) !(Atom s (StringType Unicode))
   | forall args . Breakpoint BreakpointName !(Assignment (Value s) args)

instance PrettyExt ext => Show (Stmt ext s) where
  show :: Stmt ext s -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (Stmt ext s -> Doc Any) -> Stmt ext s -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stmt ext s -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Stmt ext s -> Doc ann
pretty

instance PrettyExt ext => Pretty (Stmt ext s) where
  pretty :: forall ann. Stmt ext s -> Doc ann
pretty Stmt ext s
s =
    case Stmt ext s
s of
      SetReg Reg s tp
r Atom s tp
e     -> Reg s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg s tp -> Doc ann
pretty Reg s tp
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
e
      WriteGlobal GlobalVar tp
g Atom s tp
r  -> Doc ann
"global" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> GlobalVar tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. GlobalVar tp -> Doc ann
pretty GlobalVar tp
g Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
r
      WriteRef Atom s (ReferenceType tp)
r Atom s tp
v -> Doc ann
"ref" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (ReferenceType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (ReferenceType tp) -> Doc ann
pretty Atom s (ReferenceType tp)
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
v
      DropRef Atom s (ReferenceType tp)
r    -> Doc ann
"drop" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (ReferenceType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (ReferenceType tp) -> Doc ann
pretty Atom s (ReferenceType tp)
r
      DefineAtom Atom s tp
a AtomValue ext s tp
v -> Atom s tp -> AtomValue ext s tp -> Doc ann
forall ext s (tp :: CrucibleType) ann.
PrettyExt ext =>
Atom s tp -> AtomValue ext s tp -> Doc ann
ppAtomBinding Atom s tp
a AtomValue ext s tp
v
      Print  Atom s (StringType Unicode)
v   -> Doc ann
"print"  Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (StringType Unicode) -> Doc ann
pretty Atom s (StringType Unicode)
v
      Assert Atom s BoolType
c Atom s (StringType Unicode)
m -> Doc ann
"assert" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s BoolType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s BoolType -> Doc ann
pretty Atom s BoolType
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (StringType Unicode) -> Doc ann
pretty Atom s (StringType Unicode)
m
      Assume Atom s BoolType
c Atom s (StringType Unicode)
m -> Doc ann
"assume" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s BoolType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s BoolType -> Doc ann
pretty Atom s BoolType
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (StringType Unicode) -> Doc ann
pretty Atom s (StringType Unicode)
m
      Breakpoint BreakpointName
nm Assignment (Value s) args
args -> Doc ann
"breakpoint" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> BreakpointName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BreakpointName -> Doc ann
pretty BreakpointName
nm Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
commas ((forall (x :: CrucibleType). Value s x -> Doc ann)
-> forall (x :: Ctx CrucibleType).
   Assignment (Value s) x -> [Doc ann]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> Type) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC Value s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Value s x -> Doc ann
forall (x :: CrucibleType). Value s x -> Doc ann
pretty Assignment (Value s) args
args))

-- | Return local value assigned by this statement or @Nothing@ if this
-- does not modify a register.
stmtAssignedValue :: Stmt ext s -> Maybe (Some (Value s))
stmtAssignedValue :: forall ext s. Stmt ext s -> Maybe (Some (Value s))
stmtAssignedValue Stmt ext s
s =
  case Stmt ext s
s of
    SetReg Reg s tp
r Atom s tp
_ -> Some (Value s) -> Maybe (Some (Value s))
forall a. a -> Maybe a
Just (Value s tp -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Reg s tp -> Value s tp
forall s (tp :: CrucibleType). Reg s tp -> Value s tp
RegValue Reg s tp
r))
    DefineAtom Atom s tp
a AtomValue ext s tp
_ -> Some (Value s) -> Maybe (Some (Value s))
forall a. a -> Maybe a
Just (Value s tp -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a))
    WriteGlobal{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
    WriteRef{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
    DropRef{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
    Print{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
    Assert{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
    Assume{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing
    Breakpoint{} -> Maybe (Some (Value s))
forall a. Maybe a
Nothing

-- | Fold all registers that are inputs tostmt.
foldStmtInputs :: TraverseExt ext => (forall x . Value s x -> b -> b) -> Stmt ext s -> b -> b
foldStmtInputs :: forall ext s b.
TraverseExt ext =>
(forall (x :: CrucibleType). Value s x -> b -> b)
-> Stmt ext s -> b -> b
foldStmtInputs forall (x :: CrucibleType). Value s x -> b -> b
f Stmt ext s
s b
b =
  case Stmt ext s
s of
    SetReg Reg s tp
_ Atom s tp
e     -> Value s tp -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
e) b
b
    WriteGlobal GlobalVar tp
_ Atom s tp
a  -> Value s tp -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) b
b
    WriteRef Atom s (ReferenceType tp)
r Atom s tp
a -> Value s (ReferenceType tp) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (ReferenceType tp) -> Value s (ReferenceType tp)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (ReferenceType tp)
r) (Value s tp -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s tp
a) b
b)
    DropRef Atom s (ReferenceType tp)
r    -> Value s (ReferenceType tp) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (ReferenceType tp) -> Value s (ReferenceType tp)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (ReferenceType tp)
r) b
b
    DefineAtom Atom s tp
_ AtomValue ext s tp
v -> (forall (x :: CrucibleType). Value s x -> b -> b)
-> AtomValue ext s tp -> b -> b
forall ext s b (tp :: CrucibleType).
TraverseExt ext =>
(forall (x :: CrucibleType). Value s x -> b -> b)
-> AtomValue ext s tp -> b -> b
foldAtomValueInputs Value s x -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f AtomValue ext s tp
v b
b
    Print  Atom s (StringType Unicode)
e     -> Value s (StringType Unicode) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (StringType Unicode) -> Value s (StringType Unicode)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (StringType Unicode)
e) b
b
    Assert Atom s BoolType
c Atom s (StringType Unicode)
m   -> Value s BoolType -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s BoolType -> Value s BoolType
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s BoolType
c) (Value s (StringType Unicode) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (StringType Unicode) -> Value s (StringType Unicode)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (StringType Unicode)
m) b
b)
    Assume Atom s BoolType
c Atom s (StringType Unicode)
m   -> Value s BoolType -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s BoolType -> Value s BoolType
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s BoolType
c) (Value s (StringType Unicode) -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f (Atom s (StringType Unicode) -> Value s (StringType Unicode)
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue Atom s (StringType Unicode)
m) b
b)
    Breakpoint BreakpointName
_ Assignment (Value s) args
args -> (forall (x :: CrucibleType). Value s x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment (Value s) x -> b
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). f x -> b -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: CrucibleType -> Type) b.
(forall (x :: CrucibleType). f x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment f x -> b
foldrFC' Value s x -> b -> b
forall (x :: CrucibleType). Value s x -> b -> b
f b
b Assignment (Value s) args
args

substStmt :: ( Applicative m, TraverseExt ext )
          => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
          -> Stmt ext s
          -> m (Stmt ext s')
substStmt :: forall (m :: Type -> Type) ext s s'.
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Stmt ext s -> m (Stmt ext s')
substStmt forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Stmt ext s
s =
  case Stmt ext s
s of
    SetReg Reg s tp
r Atom s tp
e -> Reg s' tp -> Atom s' tp -> Stmt ext s'
forall ext s (tp :: CrucibleType).
Reg s tp -> Atom s tp -> Stmt ext s
SetReg (Reg s' tp -> Atom s' tp -> Stmt ext s')
-> m (Reg s' tp) -> m (Atom s' tp -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Reg s tp -> m (Reg s' tp)
substReg Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Reg s tp
r m (Atom s' tp -> Stmt ext s') -> m (Atom s' tp) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
e
    WriteGlobal GlobalVar tp
g Atom s tp
a -> GlobalVar tp -> Atom s' tp -> Stmt ext s'
forall ext s (tp :: CrucibleType).
GlobalVar tp -> Atom s tp -> Stmt ext s
WriteGlobal (GlobalVar tp -> Atom s' tp -> Stmt ext s')
-> m (GlobalVar tp) -> m (Atom s' tp -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalVar tp -> m (GlobalVar tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure GlobalVar tp
g m (Atom s' tp -> Stmt ext s') -> m (Atom s' tp) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a
    WriteRef Atom s (ReferenceType tp)
r Atom s tp
a -> Atom s' (ReferenceType tp) -> Atom s' tp -> Stmt ext s'
forall ext s (tp :: CrucibleType).
Atom s (ReferenceType tp) -> Atom s tp -> Stmt ext s
WriteRef (Atom s' (ReferenceType tp) -> Atom s' tp -> Stmt ext s')
-> m (Atom s' (ReferenceType tp)) -> m (Atom s' tp -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (ReferenceType tp) -> m (Atom s' (ReferenceType tp))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (ReferenceType tp)
r m (Atom s' tp -> Stmt ext s') -> m (Atom s' tp) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a
    DropRef Atom s (ReferenceType tp)
r -> Atom s' (ReferenceType tp) -> Stmt ext s'
forall ext s (tp :: CrucibleType).
Atom s (ReferenceType tp) -> Stmt ext s
DropRef (Atom s' (ReferenceType tp) -> Stmt ext s')
-> m (Atom s' (ReferenceType tp)) -> m (Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (ReferenceType tp) -> m (Atom s' (ReferenceType tp))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (ReferenceType tp)
r
    DefineAtom Atom s tp
a AtomValue ext s tp
v -> Atom s' tp -> AtomValue ext s' tp -> Stmt ext s'
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom (Atom s' tp -> AtomValue ext s' tp -> Stmt ext s')
-> m (Atom s' tp) -> m (AtomValue ext s' tp -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a m (AtomValue ext s' tp -> Stmt ext s')
-> m (AtomValue ext s' tp) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomValue ext s tp -> m (AtomValue ext s' tp)
forall (m :: Type -> Type) ext s s' (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> AtomValue ext s tp -> m (AtomValue ext s' tp)
substAtomValue Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f AtomValue ext s tp
v
    Print Atom s (StringType Unicode)
e -> Atom s' (StringType Unicode) -> Stmt ext s'
forall ext s. Atom s (StringType Unicode) -> Stmt ext s
Print (Atom s' (StringType Unicode) -> Stmt ext s')
-> m (Atom s' (StringType Unicode)) -> m (Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (StringType Unicode) -> m (Atom s' (StringType Unicode))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (StringType Unicode)
e
    Assert Atom s BoolType
c Atom s (StringType Unicode)
m -> Atom s' BoolType -> Atom s' (StringType Unicode) -> Stmt ext s'
forall ext s.
Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
Assert (Atom s' BoolType -> Atom s' (StringType Unicode) -> Stmt ext s')
-> m (Atom s' BoolType)
-> m (Atom s' (StringType Unicode) -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s BoolType -> m (Atom s' BoolType)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s BoolType
c m (Atom s' (StringType Unicode) -> Stmt ext s')
-> m (Atom s' (StringType Unicode)) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (StringType Unicode) -> m (Atom s' (StringType Unicode))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (StringType Unicode)
m
    Assume Atom s BoolType
c Atom s (StringType Unicode)
m -> Atom s' BoolType -> Atom s' (StringType Unicode) -> Stmt ext s'
forall ext s.
Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
Assume (Atom s' BoolType -> Atom s' (StringType Unicode) -> Stmt ext s')
-> m (Atom s' BoolType)
-> m (Atom s' (StringType Unicode) -> Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s BoolType -> m (Atom s' BoolType)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s BoolType
c m (Atom s' (StringType Unicode) -> Stmt ext s')
-> m (Atom s' (StringType Unicode)) -> m (Stmt ext s')
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (StringType Unicode) -> m (Atom s' (StringType Unicode))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (StringType Unicode)
m
    Breakpoint BreakpointName
nm Assignment (Value s) args
args -> BreakpointName -> Assignment (Value s') args -> Stmt ext s'
forall ext s (args :: Ctx CrucibleType).
BreakpointName -> Assignment (Value s) args -> Stmt ext s
Breakpoint BreakpointName
nm (Assignment (Value s') args -> Stmt ext s')
-> m (Assignment (Value s') args) -> m (Stmt ext s')
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Value s x -> m (Value s' x))
-> forall (x :: Ctx CrucibleType).
   Assignment (Value s) x -> m (Assignment (Value s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> m (Assignment g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Value s x -> m (Value s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Value s tp -> m (Value s' tp)
substValue Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) Assignment (Value s) args
args

mapStmtAtom :: ( Applicative m, TraverseExt ext )
          => (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
          -> Stmt ext s
          -> m (Stmt ext s)
mapStmtAtom :: forall (m :: Type -> Type) ext s.
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Stmt ext s -> m (Stmt ext s)
mapStmtAtom forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Stmt ext s
s =
  case Stmt ext s
s of
    SetReg Reg s tp
r Atom s tp
e -> Reg s tp -> Atom s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
Reg s tp -> Atom s tp -> Stmt ext s
SetReg Reg s tp
r (Atom s tp -> Stmt ext s) -> m (Atom s tp) -> m (Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
e
    WriteGlobal GlobalVar tp
g Atom s tp
a -> GlobalVar tp -> Atom s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
GlobalVar tp -> Atom s tp -> Stmt ext s
WriteGlobal (GlobalVar tp -> Atom s tp -> Stmt ext s)
-> m (GlobalVar tp) -> m (Atom s tp -> Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalVar tp -> m (GlobalVar tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure GlobalVar tp
g m (Atom s tp -> Stmt ext s) -> m (Atom s tp) -> m (Stmt ext s)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
a
    WriteRef Atom s (ReferenceType tp)
r Atom s tp
a -> Atom s (ReferenceType tp) -> Atom s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s (ReferenceType tp) -> Atom s tp -> Stmt ext s
WriteRef (Atom s (ReferenceType tp) -> Atom s tp -> Stmt ext s)
-> m (Atom s (ReferenceType tp)) -> m (Atom s tp -> Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s (ReferenceType tp) -> m (Atom s (ReferenceType tp))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (ReferenceType tp)
r m (Atom s tp -> Stmt ext s) -> m (Atom s tp) -> m (Stmt ext s)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
a
    DropRef Atom s (ReferenceType tp)
r -> Atom s (ReferenceType tp) -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s (ReferenceType tp) -> Stmt ext s
DropRef (Atom s (ReferenceType tp) -> Stmt ext s)
-> m (Atom s (ReferenceType tp)) -> m (Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s (ReferenceType tp) -> m (Atom s (ReferenceType tp))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (ReferenceType tp)
r
    DefineAtom Atom s tp
a AtomValue ext s tp
v -> Atom s tp -> AtomValue ext s tp -> Stmt ext s
forall ext s (tp :: CrucibleType).
Atom s tp -> AtomValue ext s tp -> Stmt ext s
DefineAtom (Atom s tp -> AtomValue ext s tp -> Stmt ext s)
-> m (Atom s tp) -> m (AtomValue ext s tp -> Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s tp -> m (Atom s tp)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s tp
a m (AtomValue ext s tp -> Stmt ext s)
-> m (AtomValue ext s tp) -> m (Stmt ext s)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
forall (m :: Type -> Type) ext s (tp :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> AtomValue ext s tp -> m (AtomValue ext s tp)
mapAtomValueAtom Atom s x -> m (Atom s x)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f AtomValue ext s tp
v
    Print Atom s (StringType Unicode)
e -> Atom s (StringType Unicode) -> Stmt ext s
forall ext s. Atom s (StringType Unicode) -> Stmt ext s
Print (Atom s (StringType Unicode) -> Stmt ext s)
-> m (Atom s (StringType Unicode)) -> m (Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s (StringType Unicode) -> m (Atom s (StringType Unicode))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (StringType Unicode)
e
    Assert Atom s BoolType
c Atom s (StringType Unicode)
m -> Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
forall ext s.
Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
Assert (Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s)
-> m (Atom s BoolType)
-> m (Atom s (StringType Unicode) -> Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s BoolType -> m (Atom s BoolType)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s BoolType
c m (Atom s (StringType Unicode) -> Stmt ext s)
-> m (Atom s (StringType Unicode)) -> m (Stmt ext s)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Atom s (StringType Unicode) -> m (Atom s (StringType Unicode))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (StringType Unicode)
m
    Assume Atom s BoolType
c Atom s (StringType Unicode)
m -> Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
forall ext s.
Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s
Assume (Atom s BoolType -> Atom s (StringType Unicode) -> Stmt ext s)
-> m (Atom s BoolType)
-> m (Atom s (StringType Unicode) -> Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Atom s BoolType -> m (Atom s BoolType)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s BoolType
c m (Atom s (StringType Unicode) -> Stmt ext s)
-> m (Atom s (StringType Unicode)) -> m (Stmt ext s)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Atom s (StringType Unicode) -> m (Atom s (StringType Unicode))
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f Atom s (StringType Unicode)
m
    Breakpoint BreakpointName
nm Assignment (Value s) args
args -> BreakpointName -> Assignment (Value s) args -> Stmt ext s
forall ext s (args :: Ctx CrucibleType).
BreakpointName -> Assignment (Value s) args -> Stmt ext s
Breakpoint BreakpointName
nm (Assignment (Value s) args -> Stmt ext s)
-> m (Assignment (Value s) args) -> m (Stmt ext s)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Value s x -> m (Value s x))
-> forall (x :: Ctx CrucibleType).
   Assignment (Value s) x -> m (Assignment (Value s) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> m (Assignment g x)
traverseFC ((forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Value s x -> m (Value s x)
forall (m :: Type -> Type) s (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Atom s x -> m (Atom s x))
-> Value s tp -> m (Value s tp)
substValueAtom Atom s x -> m (Atom s x)
forall (x :: CrucibleType). Atom s x -> m (Atom s x)
f) Assignment (Value s) args
args

substPosdStmt :: ( Applicative m, TraverseExt ext )
              => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
              -> Posd (Stmt ext s)
              -> m (Posd (Stmt ext s'))
substPosdStmt :: forall (m :: Type -> Type) ext s s'.
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (Stmt ext s) -> m (Posd (Stmt ext s'))
substPosdStmt forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Posd (Stmt ext s)
s =
  Position -> Stmt ext s' -> Posd (Stmt ext s')
forall v. Position -> v -> Posd v
Posd (Position -> Stmt ext s' -> Posd (Stmt ext s'))
-> m Position -> m (Stmt ext s' -> Posd (Stmt ext s'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Position -> m Position
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Posd (Stmt ext s) -> Position
forall v. Posd v -> Position
pos Posd (Stmt ext s)
s) m (Stmt ext s' -> Posd (Stmt ext s'))
-> m (Stmt ext s') -> m (Posd (Stmt ext s'))
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Stmt ext s -> m (Stmt ext s')
forall (m :: Type -> Type) ext s s'.
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Stmt ext s -> m (Stmt ext s')
substStmt Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val Posd (Stmt ext s)
s)

------------------------------------------------------------------------
-- TermStmt

-- | Statement that terminates a basic block in a control flow graph.
data TermStmt s (ret :: CrucibleType) where
  -- Jump to the given block.
  Jump :: !(Label s)
       -> TermStmt s ret
  -- Branch on condition.
  Br :: !(Atom s BoolType)
     -> !(Label s)
     -> !(Label s)
     -> TermStmt s ret
  -- Switch on whether this is a maybe value.
  MaybeBranch :: !(TypeRepr tp)
              -> !(Atom s (MaybeType tp))
              -> !(LambdaLabel s tp)
              -> !(Label s)
              -> TermStmt s ret

  -- Switch on a variant value.  Examine the tag of the variant
  -- and jump to the appropriate switch target.
  VariantElim :: !(CtxRepr varctx)
              -> !(Atom s (VariantType varctx))
              -> !(Ctx.Assignment (LambdaLabel s) varctx)
              -> TermStmt s ret

  -- Return from function.
  Return :: !(Atom s ret) -> TermStmt s ret

  -- End block with a tail call.
  TailCall :: !(Atom s (FunctionHandleType args ret))
           -> !(CtxRepr args)
           -> !(Ctx.Assignment (Atom s) args)
           -> TermStmt s ret

  -- Block ends because of a translation error.
  ErrorStmt :: !(Atom s (StringType Unicode)) -> TermStmt s ret

  -- Jump to the given block, and provide it the
  -- expression as input.
  Output :: !(LambdaLabel s tp)
         -> !(Atom s tp)
         -> TermStmt s ret

instance Show (TermStmt s ret) where
  show :: TermStmt s ret -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (TermStmt s ret -> Doc Any) -> TermStmt s ret -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermStmt s ret -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. TermStmt s ret -> Doc ann
pretty

instance Pretty (TermStmt s ret) where
  pretty :: forall ann. TermStmt s ret -> Doc ann
pretty TermStmt s ret
t0 =
    case TermStmt s ret
t0 of
      Jump Label s
l -> Doc ann
"jump" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Label s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Label s -> Doc ann
pretty Label s
l
      Br Atom s BoolType
c Label s
x Label s
y -> Doc ann
"branch" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s BoolType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s BoolType -> Doc ann
pretty Atom s BoolType
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Label s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Label s -> Doc ann
pretty Label s
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Label s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Label s -> Doc ann
pretty Label s
y
      MaybeBranch TypeRepr tp
_ Atom s (MaybeType tp)
c LambdaLabel s tp
j Label s
n -> Doc ann
"switchMaybe" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (MaybeType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (MaybeType tp) -> Doc ann
pretty Atom s (MaybeType tp)
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> LambdaLabel s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. LambdaLabel s tp -> Doc ann
pretty LambdaLabel s tp
j Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Label s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Label s -> Doc ann
pretty Label s
n
      VariantElim CtxRepr varctx
_ Atom s (VariantType varctx)
e Assignment (LambdaLabel s) varctx
l ->
        [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
        [ Doc ann
"switch" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (VariantType varctx) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (VariantType varctx) -> Doc ann
pretty Atom s (VariantType varctx)
e Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"{"
        , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ((forall (tp :: CrucibleType).
 String -> LambdaLabel s tp -> Doc ann)
-> Assignment (LambdaLabel s) varctx -> [Doc ann]
forall (tgt :: CrucibleType -> Type) (ctx :: Ctx CrucibleType) ann.
(forall (tp :: CrucibleType). String -> tgt tp -> Doc ann)
-> Assignment tgt ctx -> [Doc ann]
ppSwitch String -> LambdaLabel s tp -> Doc ann
forall {a} {a} {ann}. (Pretty a, Pretty a) => a -> a -> Doc ann
forall (tp :: CrucibleType). String -> LambdaLabel s tp -> Doc ann
pp Assignment (LambdaLabel s) varctx
l))
        , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ann
"}"
        ]
        where pp :: a -> a -> Doc ann
pp a
nm a
v = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
nm Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
v
      Return Atom s ret
e -> Doc ann
"return" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s ret -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s ret -> Doc ann
pretty Atom s ret
e
      TailCall Atom s (FunctionHandleType args ret)
f CtxRepr args
_ Assignment (Atom s) args
a -> Doc ann
"tail_call" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (FunctionHandleType args ret) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (FunctionHandleType args ret) -> Doc ann
pretty Atom s (FunctionHandleType args ret)
f Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens Doc ann
args
        where args :: Doc ann
args = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
commas ((forall (x :: CrucibleType). Atom s x -> Doc ann)
-> forall (x :: Ctx CrucibleType).
   Assignment (Atom s) x -> [Doc ann]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> Type) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC Atom s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s x -> Doc ann
forall (x :: CrucibleType). Atom s x -> Doc ann
pretty Assignment (Atom s) args
a)
      ErrorStmt Atom s (StringType Unicode)
e -> Doc ann
"error" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s (StringType Unicode) -> Doc ann
pretty Atom s (StringType Unicode)
e
      Output LambdaLabel s tp
l Atom s tp
e -> Doc ann
"output" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> LambdaLabel s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. LambdaLabel s tp -> Doc ann
pretty LambdaLabel s tp
l Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Atom s tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Atom s tp -> Doc ann
pretty Atom s tp
e


ppSwitch :: forall tgt ctx ann. (forall (tp :: CrucibleType). String -> tgt tp -> Doc ann) -> Ctx.Assignment tgt ctx -> [Doc ann]
ppSwitch :: forall (tgt :: CrucibleType -> Type) (ctx :: Ctx CrucibleType) ann.
(forall (tp :: CrucibleType). String -> tgt tp -> Doc ann)
-> Assignment tgt ctx -> [Doc ann]
ppSwitch forall (tp :: CrucibleType). String -> tgt tp -> Doc ann
pp Assignment tgt ctx
asgn = Size ctx
-> (forall (tp :: CrucibleType).
    [Doc ann] -> Index ctx tp -> [Doc ann])
-> [Doc ann]
-> [Doc ann]
forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
forIndex (Assignment tgt ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment tgt ctx
asgn) [Doc ann] -> Index ctx tp -> [Doc ann]
forall (tp :: CrucibleType). [Doc ann] -> Index ctx tp -> [Doc ann]
f [Doc ann]
forall a. Monoid a => a
mempty
  where f :: [Doc ann] -> Ctx.Index ctx (tp :: CrucibleType) -> [Doc ann]
        f :: forall (tp :: CrucibleType). [Doc ann] -> Index ctx tp -> [Doc ann]
f [Doc ann]
rs Index ctx tp
idx = [Doc ann]
rs [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
Prelude.++ [ String -> tgt tp -> Doc ann
forall (tp :: CrucibleType). String -> tgt tp -> Doc ann
pp (Int -> String
forall a. Show a => a -> String
show (Index ctx tp -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
Ctx.indexVal Index ctx tp
idx)) (Assignment tgt ctx
asgn Assignment tgt ctx -> Index ctx tp -> tgt tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
idx)]

-- | Provide all registers in term stmt to fold function.
foldTermStmtAtoms :: (forall x . Atom s x -> b -> b)
                  -> TermStmt s ret
                  -> b
                  -> b
foldTermStmtAtoms :: forall s b (ret :: CrucibleType).
(forall (x :: CrucibleType). Atom s x -> b -> b)
-> TermStmt s ret -> b -> b
foldTermStmtAtoms forall (x :: CrucibleType). Atom s x -> b -> b
f TermStmt s ret
stmt0 b
b =
  case TermStmt s ret
stmt0 of
    Jump Label s
_ -> b
b
    Output LambdaLabel s tp
_ Atom s tp
e -> Atom s tp -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s tp
e b
b
    Br Atom s BoolType
e Label s
_ Label s
_ -> Atom s BoolType -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s BoolType
e b
b
    MaybeBranch TypeRepr tp
_ Atom s (MaybeType tp)
e LambdaLabel s tp
_ Label s
_ -> Atom s (MaybeType tp) -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s (MaybeType tp)
e b
b
    VariantElim CtxRepr varctx
_ Atom s (VariantType varctx)
e Assignment (LambdaLabel s) varctx
_ -> Atom s (VariantType varctx) -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s (VariantType varctx)
e b
b
    Return Atom s ret
e -> Atom s ret -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s ret
e b
b
    TailCall Atom s (FunctionHandleType args ret)
fn CtxRepr args
_ Assignment (Atom s) args
a -> Atom s (FunctionHandleType args ret) -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s (FunctionHandleType args ret)
fn ((forall (x :: CrucibleType). Atom s x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment (Atom s) x -> b
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). f x -> b -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: CrucibleType -> Type) b.
(forall (x :: CrucibleType). f x -> b -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment f x -> b
foldrFC' Atom s x -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f b
b Assignment (Atom s) args
a)
    ErrorStmt Atom s (StringType Unicode)
e -> Atom s (StringType Unicode) -> b -> b
forall (x :: CrucibleType). Atom s x -> b -> b
f Atom s (StringType Unicode)
e b
b

substTermStmt :: Applicative m
              => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
              -> TermStmt s ret
              -> m (TermStmt s' ret)
substTermStmt :: forall (m :: Type -> Type) s s' (ret :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> TermStmt s ret -> m (TermStmt s' ret)
substTermStmt forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f TermStmt s ret
stmt =
  case TermStmt s ret
stmt of
    Jump Label s
l -> Label s' -> TermStmt s' ret
forall s (ret :: CrucibleType). Label s -> TermStmt s ret
Jump (Label s' -> TermStmt s' ret)
-> m (Label s') -> m (TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
l
    Output LambdaLabel s tp
ll Atom s tp
a -> LambdaLabel s' tp -> Atom s' tp -> TermStmt s' ret
forall s (args :: CrucibleType) (ret :: CrucibleType).
LambdaLabel s args -> Atom s args -> TermStmt s ret
Output (LambdaLabel s' tp -> Atom s' tp -> TermStmt s' ret)
-> m (LambdaLabel s' tp) -> m (Atom s' tp -> TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f LambdaLabel s tp
ll m (Atom s' tp -> TermStmt s' ret)
-> m (Atom s' tp) -> m (TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s tp
a
    Br Atom s BoolType
e Label s
c Label s
a -> Atom s' BoolType -> Label s' -> Label s' -> TermStmt s' ret
forall s (ret :: CrucibleType).
Atom s BoolType -> Label s -> Label s -> TermStmt s ret
Br (Atom s' BoolType -> Label s' -> Label s' -> TermStmt s' ret)
-> m (Atom s' BoolType)
-> m (Label s' -> Label s' -> TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s BoolType -> m (Atom s' BoolType)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s BoolType
e m (Label s' -> Label s' -> TermStmt s' ret)
-> m (Label s') -> m (Label s' -> TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
c m (Label s' -> TermStmt s' ret)
-> m (Label s') -> m (TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
a
    MaybeBranch TypeRepr tp
tp Atom s (MaybeType tp)
a LambdaLabel s tp
ll Label s
l -> TypeRepr tp
-> Atom s' (MaybeType tp)
-> LambdaLabel s' tp
-> Label s'
-> TermStmt s' ret
forall (args :: CrucibleType) s (ret :: CrucibleType).
TypeRepr args
-> Atom s (MaybeType args)
-> LambdaLabel s args
-> Label s
-> TermStmt s ret
MaybeBranch (TypeRepr tp
 -> Atom s' (MaybeType tp)
 -> LambdaLabel s' tp
 -> Label s'
 -> TermStmt s' ret)
-> m (TypeRepr tp)
-> m (Atom s' (MaybeType tp)
      -> LambdaLabel s' tp -> Label s' -> TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeRepr tp -> m (TypeRepr tp)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure TypeRepr tp
tp
                                         m (Atom s' (MaybeType tp)
   -> LambdaLabel s' tp -> Label s' -> TermStmt s' ret)
-> m (Atom s' (MaybeType tp))
-> m (LambdaLabel s' tp -> Label s' -> TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (MaybeType tp) -> m (Atom s' (MaybeType tp))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (MaybeType tp)
a
                                         m (LambdaLabel s' tp -> Label s' -> TermStmt s' ret)
-> m (LambdaLabel s' tp) -> m (Label s' -> TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f LambdaLabel s tp
ll
                                         m (Label s' -> TermStmt s' ret)
-> m (Label s') -> m (TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Label s
l
    VariantElim CtxRepr varctx
ctx Atom s (VariantType varctx)
a Assignment (LambdaLabel s) varctx
lls -> CtxRepr varctx
-> Atom s' (VariantType varctx)
-> Assignment (LambdaLabel s') varctx
-> TermStmt s' ret
forall (args :: Ctx CrucibleType) s (ret :: CrucibleType).
CtxRepr args
-> Atom s (VariantType args)
-> Assignment (LambdaLabel s) args
-> TermStmt s ret
VariantElim (CtxRepr varctx
 -> Atom s' (VariantType varctx)
 -> Assignment (LambdaLabel s') varctx
 -> TermStmt s' ret)
-> m (CtxRepr varctx)
-> m (Atom s' (VariantType varctx)
      -> Assignment (LambdaLabel s') varctx -> TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> CtxRepr varctx -> m (CtxRepr varctx)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CtxRepr varctx
ctx
                                         m (Atom s' (VariantType varctx)
   -> Assignment (LambdaLabel s') varctx -> TermStmt s' ret)
-> m (Atom s' (VariantType varctx))
-> m (Assignment (LambdaLabel s') varctx -> TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (VariantType varctx) -> m (Atom s' (VariantType varctx))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (VariantType varctx)
a
                                         m (Assignment (LambdaLabel s') varctx -> TermStmt s' ret)
-> m (Assignment (LambdaLabel s') varctx) -> m (TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType).
 LambdaLabel s x -> m (LambdaLabel s' x))
-> forall (x :: Ctx CrucibleType).
   Assignment (LambdaLabel s) x -> m (Assignment (LambdaLabel s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> m (Assignment g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s x -> m (LambdaLabel s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> LambdaLabel s tp -> m (LambdaLabel s' tp)
substLambdaLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) Assignment (LambdaLabel s) varctx
lls
    Return Atom s ret
e -> Atom s' ret -> TermStmt s' ret
forall s (ret :: CrucibleType). Atom s ret -> TermStmt s ret
Return (Atom s' ret -> TermStmt s' ret)
-> m (Atom s' ret) -> m (TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s ret -> m (Atom s' ret)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s ret
e
    TailCall Atom s (FunctionHandleType args ret)
fn CtxRepr args
ctx Assignment (Atom s) args
args -> Atom s' (FunctionHandleType args ret)
-> CtxRepr args -> Assignment (Atom s') args -> TermStmt s' ret
forall s (args :: Ctx CrucibleType) (ret :: CrucibleType).
Atom s (FunctionHandleType args ret)
-> CtxRepr args -> Assignment (Atom s) args -> TermStmt s ret
TailCall (Atom s' (FunctionHandleType args ret)
 -> CtxRepr args -> Assignment (Atom s') args -> TermStmt s' ret)
-> m (Atom s' (FunctionHandleType args ret))
-> m (CtxRepr args -> Assignment (Atom s') args -> TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (FunctionHandleType args ret)
-> m (Atom s' (FunctionHandleType args ret))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (FunctionHandleType args ret)
fn
                                     m (CtxRepr args -> Assignment (Atom s') args -> TermStmt s' ret)
-> m (CtxRepr args)
-> m (Assignment (Atom s') args -> TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> CtxRepr args -> m (CtxRepr args)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure CtxRepr args
ctx
                                     m (Assignment (Atom s') args -> TermStmt s' ret)
-> m (Assignment (Atom s') args) -> m (TermStmt s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Atom s x -> m (Atom s' x))
-> forall (x :: Ctx CrucibleType).
   Assignment (Atom s) x -> m (Assignment (Atom s') x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> m (Assignment g x)
traverseFC ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s x -> m (Atom s' x)
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) Assignment (Atom s) args
args
    ErrorStmt Atom s (StringType Unicode)
e -> Atom s' (StringType Unicode) -> TermStmt s' ret
forall s (ret :: CrucibleType).
Atom s (StringType Unicode) -> TermStmt s ret
ErrorStmt (Atom s' (StringType Unicode) -> TermStmt s' ret)
-> m (Atom s' (StringType Unicode)) -> m (TermStmt s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s (StringType Unicode) -> m (Atom s' (StringType Unicode))
forall (m :: Type -> Type) s s' (tp :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Atom s tp -> m (Atom s' tp)
substAtom Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Atom s (StringType Unicode)
e

substPosdTermStmt :: Applicative m
                  => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
                  -> Posd (TermStmt s ret)
                  -> m (Posd (TermStmt s' ret))
substPosdTermStmt :: forall (m :: Type -> Type) s s' (ret :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (TermStmt s ret) -> m (Posd (TermStmt s' ret))
substPosdTermStmt forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Posd (TermStmt s ret)
posd
  = Position -> TermStmt s' ret -> Posd (TermStmt s' ret)
forall v. Position -> v -> Posd v
Posd (Position -> TermStmt s' ret -> Posd (TermStmt s' ret))
-> m Position -> m (TermStmt s' ret -> Posd (TermStmt s' ret))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Position -> m Position
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Posd (TermStmt s ret) -> Position
forall v. Posd v -> Position
pos Posd (TermStmt s ret)
posd) m (TermStmt s' ret -> Posd (TermStmt s' ret))
-> m (TermStmt s' ret) -> m (Posd (TermStmt s' ret))
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> TermStmt s ret -> m (TermStmt s' ret)
forall (m :: Type -> Type) s s' (ret :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> TermStmt s ret -> m (TermStmt s' ret)
substTermStmt Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Posd (TermStmt s ret) -> TermStmt s ret
forall v. Posd v -> v
pos_val Posd (TermStmt s ret)
posd)

-- | Returns the set of registers appearing as inputs to a terminal
-- statement.
termStmtInputs :: TermStmt s ret
               -> ValueSet s
termStmtInputs :: forall s (ret :: CrucibleType). TermStmt s ret -> ValueSet s
termStmtInputs TermStmt s ret
stmt = (forall (x :: CrucibleType). Atom s x -> ValueSet s -> ValueSet s)
-> TermStmt s ret -> ValueSet s -> ValueSet s
forall s b (ret :: CrucibleType).
(forall (x :: CrucibleType). Atom s x -> b -> b)
-> TermStmt s ret -> b -> b
foldTermStmtAtoms (Some (Value s) -> ValueSet s -> ValueSet s
forall a. Ord a => a -> Set a -> Set a
Set.insert (Some (Value s) -> ValueSet s -> ValueSet s)
-> (Atom s x -> Some (Value s))
-> Atom s x
-> ValueSet s
-> ValueSet s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value s x -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Value s x -> Some (Value s))
-> (Atom s x -> Value s x) -> Atom s x -> Some (Value s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom s x -> Value s x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue) TermStmt s ret
stmt ValueSet s
forall a. Set a
Set.empty


-- | Returns the next labels for the given block.  Error statements
-- have no next labels, while return/tail call statements return 'Nothing'.
termNextLabels :: TermStmt s ret
               -> Maybe [BlockID s]
termNextLabels :: forall s (ret :: CrucibleType). TermStmt s ret -> Maybe [BlockID s]
termNextLabels TermStmt s ret
s0 =
  case TermStmt s ret
s0 of
    Jump Label s
l              -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just [Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
l]
    Output LambdaLabel s tp
l Atom s tp
_          -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just [LambdaLabel s tp -> BlockID s
forall s (args :: CrucibleType). LambdaLabel s args -> BlockID s
LambdaID LambdaLabel s tp
l]
    Br Atom s BoolType
_ Label s
x Label s
y            -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just [Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
x, Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
y]
    MaybeBranch TypeRepr tp
_ Atom s (MaybeType tp)
_ LambdaLabel s tp
x Label s
y -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just [LambdaLabel s tp -> BlockID s
forall s (args :: CrucibleType). LambdaLabel s args -> BlockID s
LambdaID LambdaLabel s tp
x, Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID Label s
y]
    VariantElim CtxRepr varctx
_ Atom s (VariantType varctx)
_ Assignment (LambdaLabel s) varctx
s   -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just ([BlockID s] -> Maybe [BlockID s])
-> [BlockID s] -> Maybe [BlockID s]
forall a b. (a -> b) -> a -> b
$ (forall (x :: CrucibleType). LambdaLabel s x -> BlockID s)
-> forall (x :: Ctx CrucibleType).
   Assignment (LambdaLabel s) x -> [BlockID s]
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> Type) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC LambdaLabel s x -> BlockID s
forall s (args :: CrucibleType). LambdaLabel s args -> BlockID s
forall (x :: CrucibleType). LambdaLabel s x -> BlockID s
LambdaID Assignment (LambdaLabel s) varctx
s
    Return Atom s ret
_            -> Maybe [BlockID s]
forall a. Maybe a
Nothing
    TailCall{}          -> Maybe [BlockID s]
forall a. Maybe a
Nothing
    ErrorStmt Atom s (StringType Unicode)
_         -> [BlockID s] -> Maybe [BlockID s]
forall a. a -> Maybe a
Just []


------------------------------------------------------------------------
-- Block

-- | A basic block within a function.
data Block ext s (ret :: CrucibleType)
   = Block { forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID           :: !(BlockID s)
           , forall ext s (ret :: CrucibleType).
Block ext s ret -> Seq (Posd (Stmt ext s))
blockStmts        :: !(Seq (Posd (Stmt ext s)))
           , forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm         :: !(Posd (TermStmt s ret))
           , forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockExtraInputs  :: !(ValueSet s)
             -- | Registers that are known to be needed as inputs for this block.
             -- For the first block, this includes the function arguments.
             -- It also includes registers read by this block before they are
             -- assigned.
             -- It does not include the lambda reg for lambda blocks.
           , forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockKnownInputs  :: !(ValueSet s)
             -- | Registers assigned by statements in block.
             -- This is a field so that its value can be memoized.
           , forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockAssignedValues :: !(ValueSet s)
           }

instance Eq (Block ext s ret) where
  Block ext s ret
x == :: Block ext s ret -> Block ext s ret -> Bool
== Block ext s ret
y = Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
x BlockID s -> BlockID s -> Bool
forall a. Eq a => a -> a -> Bool
== Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
y

instance Ord (Block ext s ret) where
  compare :: Block ext s ret -> Block ext s ret -> Ordering
compare Block ext s ret
x Block ext s ret
y = BlockID s -> BlockID s -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
x) (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
y)

instance PrettyExt ext => Show (Block ext s ret) where
  show :: Block ext s ret -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (Block ext s ret -> Doc Any) -> Block ext s ret -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block ext s ret -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Block ext s ret -> Doc ann
pretty

instance Pretty (ValueSet s) where
  pretty :: forall ann. ValueSet s -> Doc ann
pretty ValueSet s
vs = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
commas ((Some (Value s) -> Doc ann) -> [Some (Value s)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (\(Some Value s x
v) -> Value s x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Value s x -> Doc ann
pretty Value s x
v) (ValueSet s -> [Some (Value s)]
forall a. Set a -> [a]
Set.toList ValueSet s
vs))

instance PrettyExt ext => Pretty (Block ext s ret) where
  pretty :: forall ann. Block ext s ret -> Doc ann
pretty Block ext s ret
b = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [BlockID s -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b), Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ann
stmts]
    where stmts :: Doc ann
stmts = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat (Stmt ext s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Stmt ext s -> Doc ann
pretty (Stmt ext s -> Doc ann)
-> (Posd (Stmt ext s) -> Stmt ext s)
-> Posd (Stmt ext s)
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val (Posd (Stmt ext s) -> Doc ann) -> [Posd (Stmt ext s)] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (Posd (Stmt ext s)) -> [Posd (Stmt ext s)]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Fold.toList (Block ext s ret -> Seq (Posd (Stmt ext s))
forall ext s (ret :: CrucibleType).
Block ext s ret -> Seq (Posd (Stmt ext s))
blockStmts Block ext s ret
b))
                       , TermStmt s ret -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TermStmt s ret -> Doc ann
pretty (Posd (TermStmt s ret) -> TermStmt s ret
forall v. Posd v -> v
pos_val (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm Block ext s ret
b)) ]

mkBlock :: forall ext s ret
         . TraverseExt ext
        => BlockID s
        -> ValueSet s -- ^ Extra inputs to block (only non-empty for initial block)
        -> Seq (Posd (Stmt ext s))
        -> Posd (TermStmt s ret)
        -> Block ext s ret
mkBlock :: forall ext s (ret :: CrucibleType).
TraverseExt ext =>
BlockID s
-> ValueSet s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> Block ext s ret
mkBlock BlockID s
block_id ValueSet s
inputs Seq (Posd (Stmt ext s))
stmts Posd (TermStmt s ret)
term =
  Block { blockID :: BlockID s
blockID    = BlockID s
block_id
        , blockStmts :: Seq (Posd (Stmt ext s))
blockStmts = Seq (Posd (Stmt ext s))
stmts
        , blockTerm :: Posd (TermStmt s ret)
blockTerm  = Posd (TermStmt s ret)
term
        , blockExtraInputs :: ValueSet s
blockExtraInputs = ValueSet s
inputs
        , blockAssignedValues :: ValueSet s
blockAssignedValues = ValueSet s
assigned_values
        , blockKnownInputs :: ValueSet s
blockKnownInputs  = ValueSet s
all_input_values
        }
 where inputs_with_lambda :: ValueSet s
inputs_with_lambda =
         case BlockID s
block_id of
           LabelID{} -> ValueSet s
inputs
           LambdaID LambdaLabel s tp
l -> Some (Value s) -> ValueSet s -> ValueSet s
forall a. Ord a => a -> Set a -> Set a
Set.insert (Value s tp -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (Atom s tp -> Value s tp
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue (LambdaLabel s tp -> Atom s tp
forall s (tp :: CrucibleType). LambdaLabel s tp -> Atom s tp
lambdaAtom LambdaLabel s tp
l))) ValueSet s
inputs

       initState :: (ValueSet s, ValueSet s)
initState = (ValueSet s
inputs_with_lambda, ValueSet s
inputs)

       addUnassigned :: ValueSet s -> Value s x -> ValueSet s -> ValueSet s
       addUnassigned :: forall (x :: CrucibleType).
ValueSet s -> Value s x -> ValueSet s -> ValueSet s
addUnassigned ValueSet s
ar Value s x
r ValueSet s
s
         | Some (Value s) -> ValueSet s -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Value s x -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Value s x
r) ValueSet s
ar = ValueSet s
s
         | Bool
otherwise = Some (Value s) -> ValueSet s -> ValueSet s
forall a. Ord a => a -> Set a -> Set a
Set.insert (Value s x -> Some (Value s)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some Value s x
r) ValueSet s
s

       all_input_values :: ValueSet s
all_input_values
         = (forall (x :: CrucibleType). Atom s x -> ValueSet s -> ValueSet s)
-> TermStmt s ret -> ValueSet s -> ValueSet s
forall s b (ret :: CrucibleType).
(forall (x :: CrucibleType). Atom s x -> b -> b)
-> TermStmt s ret -> b -> b
foldTermStmtAtoms (ValueSet s -> Value s x -> ValueSet s -> ValueSet s
forall (x :: CrucibleType).
ValueSet s -> Value s x -> ValueSet s -> ValueSet s
addUnassigned ValueSet s
assigned_values (Value s x -> ValueSet s -> ValueSet s)
-> (Atom s x -> Value s x) -> Atom s x -> ValueSet s -> ValueSet s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Atom s x -> Value s x
forall s (tp :: CrucibleType). Atom s tp -> Value s tp
AtomValue)
                             (Posd (TermStmt s ret) -> TermStmt s ret
forall v. Posd v -> v
pos_val Posd (TermStmt s ret)
term)
                             ValueSet s
missing_values

       -- Function for inserting updating assigned regs, missing regs
       -- with statement.
       f :: (ValueSet s, ValueSet s) -> Posd (Stmt ext s) -> (ValueSet s, ValueSet s)
       f :: (ValueSet s, ValueSet s)
-> Posd (Stmt ext s) -> (ValueSet s, ValueSet s)
f (ValueSet s
ar, ValueSet s
mr) Posd (Stmt ext s)
s = (ValueSet s
ar', ValueSet s
mr')
         where ar' :: ValueSet s
ar' = case Stmt ext s -> Maybe (Some (Value s))
forall ext s. Stmt ext s -> Maybe (Some (Value s))
stmtAssignedValue (Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val Posd (Stmt ext s)
s) of
                       Maybe (Some (Value s))
Nothing -> ValueSet s
ar
                       Just  Some (Value s)
r -> Some (Value s) -> ValueSet s -> ValueSet s
forall a. Ord a => a -> Set a -> Set a
Set.insert Some (Value s)
r ValueSet s
ar
               mr' :: ValueSet s
mr' = (forall (x :: CrucibleType). Value s x -> ValueSet s -> ValueSet s)
-> Stmt ext s -> ValueSet s -> ValueSet s
forall ext s b.
TraverseExt ext =>
(forall (x :: CrucibleType). Value s x -> b -> b)
-> Stmt ext s -> b -> b
foldStmtInputs (ValueSet s -> Value s x -> ValueSet s -> ValueSet s
forall (x :: CrucibleType).
ValueSet s -> Value s x -> ValueSet s -> ValueSet s
addUnassigned ValueSet s
ar) (Posd (Stmt ext s) -> Stmt ext s
forall v. Posd v -> v
pos_val Posd (Stmt ext s)
s) ValueSet s
mr

       (ValueSet s
assigned_values, ValueSet s
missing_values) = ((ValueSet s, ValueSet s)
 -> Posd (Stmt ext s) -> (ValueSet s, ValueSet s))
-> (ValueSet s, ValueSet s)
-> Seq (Posd (Stmt ext s))
-> (ValueSet s, ValueSet s)
forall b a. (b -> a -> b) -> b -> Seq a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Fold.foldl' (ValueSet s, ValueSet s)
-> Posd (Stmt ext s) -> (ValueSet s, ValueSet s)
f (ValueSet s, ValueSet s)
initState Seq (Posd (Stmt ext s))
stmts

substBlock :: ( Applicative m, TraverseExt ext )
           => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
           -> Block ext s ret
           -> m (Block ext s' ret)
substBlock :: forall (m :: Type -> Type) ext s s' (ret :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Block ext s ret -> m (Block ext s' ret)
substBlock forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f Block ext s ret
b =
  BlockID s'
-> Seq (Posd (Stmt ext s'))
-> Posd (TermStmt s' ret)
-> ValueSet s'
-> ValueSet s'
-> ValueSet s'
-> Block ext s' ret
forall ext s (ret :: CrucibleType).
BlockID s
-> Seq (Posd (Stmt ext s))
-> Posd (TermStmt s ret)
-> ValueSet s
-> ValueSet s
-> ValueSet s
-> Block ext s ret
Block (BlockID s'
 -> Seq (Posd (Stmt ext s'))
 -> Posd (TermStmt s' ret)
 -> ValueSet s'
 -> ValueSet s'
 -> ValueSet s'
 -> Block ext s' ret)
-> m (BlockID s')
-> m (Seq (Posd (Stmt ext s'))
      -> Posd (TermStmt s' ret)
      -> ValueSet s'
      -> ValueSet s'
      -> ValueSet s'
      -> Block ext s' ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> BlockID s -> m (BlockID s')
forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> BlockID s -> m (BlockID s')
substBlockID Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b)
        m (Seq (Posd (Stmt ext s'))
   -> Posd (TermStmt s' ret)
   -> ValueSet s'
   -> ValueSet s'
   -> ValueSet s'
   -> Block ext s' ret)
-> m (Seq (Posd (Stmt ext s')))
-> m (Posd (TermStmt s' ret)
      -> ValueSet s' -> ValueSet s' -> ValueSet s' -> Block ext s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (Posd (Stmt ext s) -> m (Posd (Stmt ext s')))
-> Seq (Posd (Stmt ext s)) -> m (Seq (Posd (Stmt ext s')))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Seq a -> f (Seq b)
traverse ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (Stmt ext s) -> m (Posd (Stmt ext s'))
forall (m :: Type -> Type) ext s s'.
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (Stmt ext s) -> m (Posd (Stmt ext s'))
substPosdStmt Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) (Block ext s ret -> Seq (Posd (Stmt ext s))
forall ext s (ret :: CrucibleType).
Block ext s ret -> Seq (Posd (Stmt ext s))
blockStmts Block ext s ret
b)
        m (Posd (TermStmt s' ret)
   -> ValueSet s' -> ValueSet s' -> ValueSet s' -> Block ext s' ret)
-> m (Posd (TermStmt s' ret))
-> m (ValueSet s'
      -> ValueSet s' -> ValueSet s' -> Block ext s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (TermStmt s ret) -> m (Posd (TermStmt s' ret))
forall (m :: Type -> Type) s s' (ret :: CrucibleType).
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Posd (TermStmt s ret) -> m (Posd (TermStmt s' ret))
substPosdTermStmt Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm Block ext s ret
b)
        m (ValueSet s' -> ValueSet s' -> ValueSet s' -> Block ext s' ret)
-> m (ValueSet s')
-> m (ValueSet s' -> ValueSet s' -> Block ext s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
substValueSet Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockExtraInputs Block ext s ret
b)
        m (ValueSet s' -> ValueSet s' -> Block ext s' ret)
-> m (ValueSet s') -> m (ValueSet s' -> Block ext s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
substValueSet Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockKnownInputs Block ext s ret
b)
        m (ValueSet s' -> Block ext s' ret)
-> m (ValueSet s') -> m (Block ext s' ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
forall (m :: Type -> Type) s s'.
Applicative m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> ValueSet s -> m (ValueSet s')
substValueSet Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (Block ext s ret -> ValueSet s
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockAssignedValues Block ext s ret
b)

------------------------------------------------------------------------
-- CFG

-- | A CFG using registers instead of SSA form.
--
-- Parameter @ext@ is the syntax extension, @s@ is a phantom type
-- parameter identifying a particular CFG, @init@ is the list of input
-- types of the CFG, and @ret@ is the return type.
data CFG ext s (init :: Ctx CrucibleType) (ret :: CrucibleType)
   = CFG { forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle :: !(FnHandle init ret)
         , forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Label s
cfgEntryLabel :: !(Label s)
         , forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks :: ![Block ext s ret]
         }

cfgEntryBlock :: CFG ext s init ret -> Block ext s ret
cfgEntryBlock :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Block ext s ret
cfgEntryBlock CFG ext s init ret
g =
  Block ext s ret -> Maybe (Block ext s ret) -> Block ext s ret
forall a. a -> Maybe a -> a
fromMaybe
    (String -> Block ext s ret
forall a. HasCallStack => String -> a
error String
"Missing entry block")
    ((Block ext s ret -> Bool)
-> [Block ext s ret] -> Maybe (Block ext s ret)
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Maybe a
Fold.find (\Block ext s ret
b -> Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b BlockID s -> BlockID s -> Bool
forall a. Eq a => a -> a -> Bool
== Label s -> BlockID s
forall s. Label s -> BlockID s
LabelID (CFG ext s init ret -> Label s
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Label s
cfgEntryLabel CFG ext s init ret
g)) (CFG ext s init ret -> [Block ext s ret]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks CFG ext s init ret
g))

cfgInputTypes :: CFG ext s init ret -> CtxRepr init
cfgInputTypes :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> CtxRepr init
cfgInputTypes = CFG ext s init ret -> CtxRepr init
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> CtxRepr init
cfgArgTypes
{-# DEPRECATED cfgInputTypes "Use cfgArgTypes instead" #-}

cfgArgTypes :: CFG ext s init ret -> CtxRepr init
cfgArgTypes :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> CtxRepr init
cfgArgTypes CFG ext s init ret
g = FnHandle init ret -> CtxRepr init
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> CtxRepr args
handleArgTypes (CFG ext s init ret -> FnHandle init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle CFG ext s init ret
g)

cfgReturnType :: CFG ext s init ret -> TypeRepr ret
cfgReturnType :: forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> TypeRepr ret
cfgReturnType CFG ext s init ret
g = FnHandle init ret -> TypeRepr ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr ret
handleReturnType (CFG ext s init ret -> FnHandle init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle CFG ext s init ret
g)

-- | Rename all the atoms, labels, and other named things in the CFG.
-- Useful for rewriting, since the names can be generated from a nonce
-- generator the client controls (and can thus keep using to generate
-- fresh names).
substCFG :: ( Applicative m, TraverseExt ext )
         => (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
         -> CFG ext s init ret
         -> m (CFG ext s' init ret)
substCFG :: forall (m :: Type -> Type) ext s s' (init :: Ctx CrucibleType)
       (ret :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> CFG ext s init ret -> m (CFG ext s' init ret)
substCFG forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f CFG ext s init ret
cfg =
  FnHandle init ret
-> Label s' -> [Block ext s' ret] -> CFG ext s' init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle init ret
-> Label s -> [Block ext s ret] -> CFG ext s init ret
CFG (FnHandle init ret
 -> Label s' -> [Block ext s' ret] -> CFG ext s' init ret)
-> m (FnHandle init ret)
-> m (Label s' -> [Block ext s' ret] -> CFG ext s' init ret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> FnHandle init ret -> m (FnHandle init ret)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (CFG ext s init ret -> FnHandle init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle CFG ext s init ret
cfg)
      m (Label s' -> [Block ext s' ret] -> CFG ext s' init ret)
-> m (Label s') -> m ([Block ext s' ret] -> CFG ext s' init ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
forall (m :: Type -> Type) s s'.
Functor m =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Label s -> m (Label s')
substLabel Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f (CFG ext s init ret -> Label s
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Label s
cfgEntryLabel CFG ext s init ret
cfg)
      m ([Block ext s' ret] -> CFG ext s' init ret)
-> m [Block ext s' ret] -> m (CFG ext s' init ret)
forall a b. m (a -> b) -> m a -> m b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (Block ext s ret -> m (Block ext s' ret))
-> [Block ext s ret] -> m [Block ext s' ret]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Block ext s ret -> m (Block ext s' ret)
forall (m :: Type -> Type) ext s s' (ret :: CrucibleType).
(Applicative m, TraverseExt ext) =>
(forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x))
-> Block ext s ret -> m (Block ext s' ret)
substBlock Nonce s x -> m (Nonce s' x)
forall (x :: CrucibleType). Nonce s x -> m (Nonce s' x)
f) (CFG ext s init ret -> [Block ext s ret]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks CFG ext s init ret
cfg)

-- | Run a computation along all of the paths in a cfg, without taking backedges.
--
-- The computation has access to an environment that is specific to the current path
-- being explored, as well as a global environment that is maintained across the
-- entire computation.
traverseCFG :: ( Monad m, TraverseExt ext )
            => (genv -> penv -> Block ext s ret -> m (genv, penv))
            -> genv
            -> penv
            -> Block ext s ret
            -> CFG ext s init ret
            -> m genv
traverseCFG :: forall (m :: Type -> Type) ext genv penv s (ret :: CrucibleType)
       (init :: Ctx CrucibleType).
(Monad m, TraverseExt ext) =>
(genv -> penv -> Block ext s ret -> m (genv, penv))
-> genv -> penv -> Block ext s ret -> CFG ext s init ret -> m genv
traverseCFG genv -> penv -> Block ext s ret -> m (genv, penv)
f genv
genv0 penv
penv0 Block ext s ret
b0 CFG ext s init ret
cfg =
  (genv -> penv -> Block ext s ret -> m (genv, penv))
-> Map (BlockID s) (Block ext s ret)
-> genv
-> penv
-> Set (BlockID s)
-> Block ext s ret
-> m genv
forall (m :: Type -> Type) genv penv ext s (ret :: CrucibleType).
Monad m =>
(genv -> penv -> Block ext s ret -> m (genv, penv))
-> Map (BlockID s) (Block ext s ret)
-> genv
-> penv
-> Set (BlockID s)
-> Block ext s ret
-> m genv
traverseStep genv -> penv -> Block ext s ret -> m (genv, penv)
f Map (BlockID s) (Block ext s ret)
bmap0 genv
genv0 penv
penv0 Set (BlockID s)
forall a. Monoid a => a
mempty Block ext s ret
b0
  where
    bmap0 :: Map (BlockID s) (Block ext s ret)
bmap0 = [(BlockID s, Block ext s ret)] -> Map (BlockID s) (Block ext s ret)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
b, Block ext s ret
b) | Block ext s ret
b <- CFG ext s init ret -> [Block ext s ret]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks CFG ext s init ret
cfg ]

-- | Run a computation along all of the paths in a cfg, without taking backedges.
--
-- The computation has access to an environment that is specific to the current path
-- being explored, as well as a global environment that is maintained across the
-- entire computation.
--
-- Each step of the computation inspects the global- and
-- path-environments as well as the current block, and returns new
-- environments.
traverseStep :: forall m genv penv ext s ret.
                Monad m
             => (genv -> penv -> Block ext s ret -> m (genv, penv))
             -> Map.Map (BlockID s) (Block ext s ret)
             -> genv
             -> penv
             -> Set.Set (BlockID s)
             -> (Block ext s ret)
             -> m genv
traverseStep :: forall (m :: Type -> Type) genv penv ext s (ret :: CrucibleType).
Monad m =>
(genv -> penv -> Block ext s ret -> m (genv, penv))
-> Map (BlockID s) (Block ext s ret)
-> genv
-> penv
-> Set (BlockID s)
-> Block ext s ret
-> m genv
traverseStep genv -> penv -> Block ext s ret -> m (genv, penv)
f Map (BlockID s) (Block ext s ret)
bmap genv
genv penv
penv Set (BlockID s)
seen Block ext s ret
blk
  | Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
blk BlockID s -> Set (BlockID s) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (BlockID s)
seen =
    genv -> m genv
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return genv
genv
  | Bool
otherwise =
    do (genv
genv', penv
penv') <- genv -> penv -> Block ext s ret -> m (genv, penv)
f genv
genv penv
penv Block ext s ret
blk
       (genv -> BlockID s -> m genv) -> genv -> [BlockID s] -> m genv
forall (t :: Type -> Type) (m :: Type -> Type) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
Fold.foldlM (penv -> Set (BlockID s) -> genv -> BlockID s -> m genv
go penv
penv' (BlockID s -> Set (BlockID s) -> Set (BlockID s)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Block ext s ret -> BlockID s
forall ext s (ret :: CrucibleType). Block ext s ret -> BlockID s
blockID Block ext s ret
blk) Set (BlockID s)
seen)) genv
genv' [BlockID s]
next
  where
    next :: [BlockID s]
next = [BlockID s] -> Maybe [BlockID s] -> [BlockID s]
forall a. a -> Maybe a -> a
fromMaybe [] (TermStmt s ret -> Maybe [BlockID s]
forall s (ret :: CrucibleType). TermStmt s ret -> Maybe [BlockID s]
termNextLabels (Posd (TermStmt s ret) -> TermStmt s ret
forall v. Posd v -> v
pos_val (Block ext s ret -> Posd (TermStmt s ret)
forall ext s (ret :: CrucibleType).
Block ext s ret -> Posd (TermStmt s ret)
blockTerm Block ext s ret
blk)))

    go :: penv -> Set (BlockID s) -> genv -> BlockID s -> m genv
go penv
penv' Set (BlockID s)
seen' genv
genv' BlockID s
blkId
      | Just Block ext s ret
blk' <- BlockID s
-> Map (BlockID s) (Block ext s ret) -> Maybe (Block ext s ret)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BlockID s
blkId Map (BlockID s) (Block ext s ret)
bmap
      = (genv -> penv -> Block ext s ret -> m (genv, penv))
-> Map (BlockID s) (Block ext s ret)
-> genv
-> penv
-> Set (BlockID s)
-> Block ext s ret
-> m genv
forall (m :: Type -> Type) genv penv ext s (ret :: CrucibleType).
Monad m =>
(genv -> penv -> Block ext s ret -> m (genv, penv))
-> Map (BlockID s) (Block ext s ret)
-> genv
-> penv
-> Set (BlockID s)
-> Block ext s ret
-> m genv
traverseStep genv -> penv -> Block ext s ret -> m (genv, penv)
f Map (BlockID s) (Block ext s ret)
bmap genv
genv' penv
penv' Set (BlockID s)
seen' Block ext s ret
blk'
      | Bool
otherwise
      = String -> [String] -> m genv
forall a. HasCallStack => String -> [String] -> a
panic String
"Reg.traverseStep"
        [ String
"Block " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BlockID s -> String
forall a. Show a => a -> String
show BlockID s
blkId String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not found in block map" ]


instance PrettyExt ext => Show (CFG ext s init ret) where
  show :: CFG ext s init ret -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (CFG ext s init ret -> Doc Any) -> CFG ext s init ret -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CFG ext s init ret -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. CFG ext s init ret -> Doc ann
pretty

instance PrettyExt ext => Pretty (CFG ext s init ret) where
  pretty :: forall ann. CFG ext s init ret -> Doc ann
pretty CFG ext s init ret
g = do
    let nm :: Doc ann
nm = FunctionName -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (FnHandle init ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName (CFG ext s init ret -> FnHandle init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> FnHandle init ret
cfgHandle CFG ext s init ret
g))
    let args :: Doc ann
args =
          [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
commas ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (Some (Value s) -> Doc ann) -> [Some (Value s)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map ((forall (tp :: CrucibleType). Value s tp -> Doc ann)
-> Some (Value s) -> Doc ann
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome Value s tp -> Doc ann
forall a ann. Show a => a -> Doc ann
forall (tp :: CrucibleType). Value s tp -> Doc ann
viaShow) ([Some (Value s)] -> [Doc ann]) -> [Some (Value s)] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ Set (Some (Value s)) -> [Some (Value s)]
forall a. Set a -> [a]
Set.toList (Set (Some (Value s)) -> [Some (Value s)])
-> Set (Some (Value s)) -> [Some (Value s)]
forall a b. (a -> b) -> a -> b
$
          Block ext s ret -> Set (Some (Value s))
forall ext s (ret :: CrucibleType). Block ext s ret -> ValueSet s
blockExtraInputs (CFG ext s init ret -> Block ext s ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> Block ext s ret
cfgEntryBlock CFG ext s init ret
g)
    [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ TypeRepr ret -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeRepr ret -> Doc ann
pretty (CFG ext s init ret -> TypeRepr ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> TypeRepr ret
cfgReturnType CFG ext s init ret
g) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
nm Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens Doc ann
args
         , [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat (Block ext s ret -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Block ext s ret -> Doc ann
pretty (Block ext s ret -> Doc ann) -> [Block ext s ret] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> CFG ext s init ret -> [Block ext s ret]
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext s init ret -> [Block ext s ret]
cfgBlocks CFG ext s init ret
g) ]

------------------------------------------------------------------------
-- SomeCFG, AnyCFG

-- | 'SomeCFG' is a CFG with an arbitrary parameter 's'.
data SomeCFG ext init ret = forall s . SomeCFG !(CFG ext s init ret)

-- | Control flow graph.  This data type closes existentially
--   over all the type parameters except @ext@.
data AnyCFG ext where
  AnyCFG :: CFG ext blocks init ret
         -> AnyCFG ext

instance PrettyExt ext => Show (AnyCFG ext) where
  show :: AnyCFG ext -> String
show AnyCFG ext
cfg = case AnyCFG ext
cfg of AnyCFG CFG ext blocks init ret
c -> CFG ext blocks init ret -> String
forall a. Show a => a -> String
show CFG ext blocks init ret
c