{- |
Module           : Lang.Crucible.CFG.Core
Description      : SSA-based control flow graphs
Copyright        : (c) Galois, Inc 2014-2016
License          : BSD3
Maintainer       : Joe Hendrix <jhendrix@galois.com>

Define a SSA-based control flow graph data structure using a side-effect free
expression syntax.

Unlike usual SSA forms, we do not use phi-functions, but instead rely on an
argument-passing formulation for basic blocks.  In this form, concrete values
are bound to formal parameters instead of using phi-functions that switch
on the place from which you jumped.
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ParallelListComp #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Lang.Crucible.CFG.Core
  ( -- * CFG
    CFG(..)
  , SomeCFG(..)
  , HasSomeCFG(..)
  , AnyCFG(..)
  , ppCFG
  , ppCFG'
  , cfgArgTypes
  , cfgReturnType
  , CFGPostdom

    -- * Blocks
  , BlockMap
  , getBlock
  , extendBlockMap

  , BlockID(..)
  , extendBlockID
  , extendBlockID'

  , Block(..)
  , blockLoc
  , blockStmts
  , withBlockTermStmt
  , nextBlocks

    -- * Jump targets
  , JumpTarget(..)
  , extendJumpTarget
  , jumpTargetID
  , SwitchTarget(..)
  , switchTargetID
  , extendSwitchTarget

    -- * Statements
  , StmtSeq(..)
  , firstStmtLoc
  , stmtSeqTermStmt
  , Stmt(..)
  , ppStmt
  , nextStmtHeight

  , applyEmbeddingStmt

  , TermStmt(..)
  , termStmtNextBlocks

    -- * Expressions
  , Expr(..)
  , Reg(..)
  , extendReg
  , lastReg

    -- * Re-exports
  , module Lang.Crucible.Types
  , module Lang.Crucible.CFG.Common
  , module Data.Parameterized.Classes
  , module Data.Parameterized.Some
  ) where

import Control.Applicative
import Data.Bimap (Bimap)
import Data.Maybe (fromMaybe)
import Data.Kind (Type)
import Data.Parameterized.Classes
import Data.Parameterized.Map (Pair(..))
import Data.Parameterized.Some
import Data.Parameterized.TraversableFC
import Data.String
import Lens.Micro ((^.), Lens', lens)
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.Types
import Lang.Crucible.Utils.PrettyPrint

#ifdef UNSAFE_OPS
-- We deliberately import Context.Unsafe as it is the only one that supports
-- the unsafe coerces between an index and its extension.
import Data.Parameterized.Context as Ctx hiding (Assignment)
import Data.Parameterized.Context.Unsafe as Ctx (Assignment)
import Unsafe.Coerce
#else
import Data.Parameterized.Context as Ctx
#endif

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

-- | A temporary register identifier introduced during translation.
--   These are unique to the current function.  The `ctx` parameter
--   is a context containing the types of all the temporary registers
--   currently in scope, and the `tp` parameter indicates the type
--   of this register (which necessarily appears somewhere in `ctx`)
newtype Reg (ctx :: Ctx CrucibleType) (tp :: CrucibleType) = Reg { forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
regIndex :: Ctx.Index ctx tp }
  deriving (Reg ctx tp -> Reg ctx tp -> Bool
(Reg ctx tp -> Reg ctx tp -> Bool)
-> (Reg ctx tp -> Reg ctx tp -> Bool) -> Eq (Reg ctx tp)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Bool
$c== :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Bool
== :: Reg ctx tp -> Reg ctx tp -> Bool
$c/= :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Bool
/= :: Reg ctx tp -> Reg ctx tp -> Bool
Eq, (forall (a :: CrucibleType) (b :: CrucibleType).
 Reg ctx a -> Reg ctx b -> Maybe (a :~: b))
-> TestEquality (Reg ctx)
forall {k} (f :: k -> Type).
(forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b))
-> TestEquality f
forall (ctx :: Ctx CrucibleType) (a :: CrucibleType)
       (b :: CrucibleType).
Reg ctx a -> Reg ctx b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Reg ctx a -> Reg ctx b -> Maybe (a :~: b)
$ctestEquality :: forall (ctx :: Ctx CrucibleType) (a :: CrucibleType)
       (b :: CrucibleType).
Reg ctx a -> Reg ctx b -> Maybe (a :~: b)
testEquality :: forall (a :: CrucibleType) (b :: CrucibleType).
Reg ctx a -> Reg ctx b -> Maybe (a :~: b)
TestEquality, Eq (Reg ctx tp)
Eq (Reg ctx tp) =>
(Reg ctx tp -> Reg ctx tp -> Ordering)
-> (Reg ctx tp -> Reg ctx tp -> Bool)
-> (Reg ctx tp -> Reg ctx tp -> Bool)
-> (Reg ctx tp -> Reg ctx tp -> Bool)
-> (Reg ctx tp -> Reg ctx tp -> Bool)
-> (Reg ctx tp -> Reg ctx tp -> Reg ctx tp)
-> (Reg ctx tp -> Reg ctx tp -> Reg ctx tp)
-> Ord (Reg ctx tp)
Reg ctx tp -> Reg ctx tp -> Bool
Reg ctx tp -> Reg ctx tp -> Ordering
Reg ctx tp -> Reg ctx tp -> Reg ctx tp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Eq (Reg ctx tp)
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Bool
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Ordering
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Reg ctx tp
$ccompare :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Ordering
compare :: Reg ctx tp -> Reg ctx tp -> Ordering
$c< :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Bool
< :: Reg ctx tp -> Reg ctx tp -> Bool
$c<= :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Bool
<= :: Reg ctx tp -> Reg ctx tp -> Bool
$c> :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Bool
> :: Reg ctx tp -> Reg ctx tp -> Bool
$c>= :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Bool
>= :: Reg ctx tp -> Reg ctx tp -> Bool
$cmax :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Reg ctx tp
max :: Reg ctx tp -> Reg ctx tp -> Reg ctx tp
$cmin :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Reg ctx tp -> Reg ctx tp
min :: Reg ctx tp -> Reg ctx tp -> Reg ctx tp
Ord, TestEquality (Reg ctx)
TestEquality (Reg ctx) =>
(forall (x :: CrucibleType) (y :: CrucibleType).
 Reg ctx x -> Reg ctx y -> OrderingF x y)
-> (forall (x :: CrucibleType) (y :: CrucibleType).
    Reg ctx x -> Reg ctx y -> Bool)
-> (forall (x :: CrucibleType) (y :: CrucibleType).
    Reg ctx x -> Reg ctx y -> Bool)
-> (forall (x :: CrucibleType) (y :: CrucibleType).
    Reg ctx x -> Reg ctx y -> Bool)
-> (forall (x :: CrucibleType) (y :: CrucibleType).
    Reg ctx x -> Reg ctx y -> Bool)
-> OrdF (Reg ctx)
forall k (ktp :: k -> Type).
TestEquality ktp =>
(forall (x :: k) (y :: k). ktp x -> ktp y -> OrderingF x y)
-> (forall (x :: k) (y :: k). ktp x -> ktp y -> Bool)
-> (forall (x :: k) (y :: k). ktp x -> ktp y -> Bool)
-> (forall (x :: k) (y :: k). ktp x -> ktp y -> Bool)
-> (forall (x :: k) (y :: k). ktp x -> ktp y -> Bool)
-> OrdF ktp
forall (ctx :: Ctx CrucibleType). TestEquality (Reg ctx)
forall (ctx :: Ctx CrucibleType) (x :: CrucibleType)
       (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> Bool
forall (ctx :: Ctx CrucibleType) (x :: CrucibleType)
       (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> OrderingF x y
forall (x :: CrucibleType) (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> Bool
forall (x :: CrucibleType) (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> OrderingF x y
$ccompareF :: forall (ctx :: Ctx CrucibleType) (x :: CrucibleType)
       (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> OrderingF x y
compareF :: forall (x :: CrucibleType) (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> OrderingF x y
$cleqF :: forall (ctx :: Ctx CrucibleType) (x :: CrucibleType)
       (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> Bool
leqF :: forall (x :: CrucibleType) (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> Bool
$cltF :: forall (ctx :: Ctx CrucibleType) (x :: CrucibleType)
       (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> Bool
ltF :: forall (x :: CrucibleType) (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> Bool
$cgeqF :: forall (ctx :: Ctx CrucibleType) (x :: CrucibleType)
       (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> Bool
geqF :: forall (x :: CrucibleType) (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> Bool
$cgtF :: forall (ctx :: Ctx CrucibleType) (x :: CrucibleType)
       (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> Bool
gtF :: forall (x :: CrucibleType) (y :: CrucibleType).
Reg ctx x -> Reg ctx y -> Bool
OrdF)

instance Show (Reg ctx tp) where
  show :: Reg ctx tp -> String
show (Reg Index ctx tp
i) = Char
'$' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show (Index ctx tp -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal Index ctx tp
i)

instance ShowF (Reg ctx)

instance Pretty (Reg ctx tp) where
  pretty :: forall ann. Reg ctx tp -> Doc ann
pretty (Reg Index ctx tp
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
<> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Index ctx tp -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal Index ctx tp
i)

instance ApplyEmbedding' Reg where
  applyEmbedding' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
CtxEmbedding ctx ctx' -> Reg ctx v -> Reg ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe Reg ctx v
r = Index ctx' v -> Reg ctx' v
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Index ctx tp -> Reg ctx tp
Reg (Index ctx' v -> Reg ctx' v) -> Index ctx' v -> Reg ctx' v
forall a b. (a -> b) -> a -> b
$ CtxEmbedding ctx ctx' -> Index ctx v -> Index ctx' v
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ApplyEmbedding' f =>
CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
CtxEmbedding ctx ctx' -> Index ctx v -> Index ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe (Reg ctx v -> Index ctx v
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
regIndex Reg ctx v
r)

instance ExtendContext' Reg where
  extendContext' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
Diff ctx ctx' -> Reg ctx v -> Reg ctx' v
extendContext' Diff ctx ctx'
diff Reg ctx v
r = Index ctx' v -> Reg ctx' v
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Index ctx tp -> Reg ctx tp
Reg (Index ctx' v -> Reg ctx' v) -> Index ctx' v -> Reg ctx' v
forall a b. (a -> b) -> a -> b
$ Diff ctx ctx' -> Index ctx v -> Index ctx' v
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ExtendContext' f =>
Diff ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
Diff ctx ctx' -> Index ctx v -> Index ctx' v
extendContext' Diff ctx ctx'
diff (Reg ctx v -> Index ctx v
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
regIndex Reg ctx v
r)

-- | Finds the value of the most-recently introduced register in scope.
lastReg :: KnownContext ctx => Reg (ctx ::> tp) tp
lastReg :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
KnownContext ctx =>
Reg (ctx ::> tp) tp
lastReg = Index (ctx ::> tp) tp -> Reg (ctx ::> tp) tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Index ctx tp -> Reg ctx tp
Reg (Size ctx -> Index (ctx ::> tp) tp
forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size ctx
forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize)

-- | Extend the set of registers in scope for a given register value
--   without changing its index or type.
extendReg :: Reg ctx tp -> Reg (ctx ::> r) tp
extendReg :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType)
       (r :: CrucibleType).
Reg ctx tp -> Reg (ctx ::> r) tp
extendReg = Index (ctx ::> r) tp -> Reg (ctx ::> r) tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Index ctx tp -> Reg ctx tp
Reg (Index (ctx ::> r) tp -> Reg (ctx ::> r) tp)
-> (Reg ctx tp -> Index (ctx ::> r) tp)
-> Reg ctx tp
-> Reg (ctx ::> r) tp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index ctx tp -> Index (ctx ::> r) tp
forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
KnownDiff l r =>
Index l tp -> Index r tp
extendIndex (Index ctx tp -> Index (ctx ::> r) tp)
-> (Reg ctx tp -> Index ctx tp)
-> Reg ctx tp
-> Index (ctx ::> r) tp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reg ctx tp -> Index ctx tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
regIndex

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

-- | An expression is just an App applied to some registers.
newtype Expr ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType)
      = App (App ext (Reg ctx) tp)

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

instance PrettyApp (ExprExtension ext) => Pretty (Expr ext ctx tp) where
  pretty :: forall ann. Expr ext ctx tp -> Doc ann
pretty (App App ext (Reg ctx) tp
a) = (forall (x :: CrucibleType). Reg ctx x -> Doc ann)
-> forall (x :: CrucibleType). App ext (Reg ctx) 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 Reg ctx x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx x -> Doc ann
forall (x :: CrucibleType). Reg ctx x -> Doc ann
pretty App ext (Reg ctx) tp
a

ppAssignment :: Assignment (Reg ctx) args -> [Doc ann]
ppAssignment :: forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType) ann.
Assignment (Reg ctx) args -> [Doc ann]
ppAssignment = (forall (x :: CrucibleType). Reg ctx x -> Doc ann)
-> forall (x :: Ctx CrucibleType).
   Assignment (Reg ctx) 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 Reg ctx x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx x -> Doc ann
forall (x :: CrucibleType). Reg ctx x -> Doc ann
pretty

instance ( TraversableFC (ExprExtension ext)
         ) => ApplyEmbedding' (Expr ext) where
  applyEmbedding' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
CtxEmbedding ctx ctx' -> Expr ext ctx v -> Expr ext ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe (App App ext (Reg ctx) v
e) = App ext (Reg ctx') v -> Expr ext ctx' v
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
App ext (Reg ctx) tp -> Expr ext ctx tp
App ((forall (u :: CrucibleType). Reg ctx u -> Reg ctx' u)
-> App ext (Reg ctx) v -> App ext (Reg ctx') v
forall ext (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (tp :: CrucibleType).
TraversableFC (ExprExtension ext) =>
(forall (u :: CrucibleType). f u -> g u)
-> App ext f tp -> App ext g tp
mapApp (CtxEmbedding ctx ctx' -> Reg ctx u -> Reg ctx' u
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ApplyEmbedding' f =>
CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
CtxEmbedding ctx ctx' -> Reg ctx v -> Reg ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe) App ext (Reg ctx) v
e)

instance ( TraversableFC (ExprExtension ext)
         ) => ExtendContext' (Expr ext) where
  extendContext' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
Diff ctx ctx' -> Expr ext ctx v -> Expr ext ctx' v
extendContext' Diff ctx ctx'
diff (App App ext (Reg ctx) v
e) = App ext (Reg ctx') v -> Expr ext ctx' v
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
App ext (Reg ctx) tp -> Expr ext ctx tp
App ((forall (u :: CrucibleType). Reg ctx u -> Reg ctx' u)
-> App ext (Reg ctx) v -> App ext (Reg ctx') v
forall ext (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (tp :: CrucibleType).
TraversableFC (ExprExtension ext) =>
(forall (u :: CrucibleType). f u -> g u)
-> App ext f tp -> App ext g tp
mapApp (Diff ctx ctx' -> Reg ctx u -> Reg ctx' u
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ExtendContext' f =>
Diff ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
Diff ctx ctx' -> Reg ctx v -> Reg ctx' v
extendContext' Diff ctx ctx'
diff) App ext (Reg ctx) v
e)

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

-- | A `BlockID` uniquely identifies a block in a control-flow graph.
--   Each block has an associated context, indicating the formal arguments
--   it expects to find in registers from its calling locations.
newtype BlockID (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType)
      = BlockID { forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex :: Ctx.Index blocks tp }
  deriving (BlockID blocks tp -> BlockID blocks tp -> Bool
(BlockID blocks tp -> BlockID blocks tp -> Bool)
-> (BlockID blocks tp -> BlockID blocks tp -> Bool)
-> Eq (BlockID blocks tp)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> Bool
$c== :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> Bool
== :: BlockID blocks tp -> BlockID blocks tp -> Bool
$c/= :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> Bool
/= :: BlockID blocks tp -> BlockID blocks tp -> Bool
Eq, Eq (BlockID blocks tp)
Eq (BlockID blocks tp) =>
(BlockID blocks tp -> BlockID blocks tp -> Ordering)
-> (BlockID blocks tp -> BlockID blocks tp -> Bool)
-> (BlockID blocks tp -> BlockID blocks tp -> Bool)
-> (BlockID blocks tp -> BlockID blocks tp -> Bool)
-> (BlockID blocks tp -> BlockID blocks tp -> Bool)
-> (BlockID blocks tp -> BlockID blocks tp -> BlockID blocks tp)
-> (BlockID blocks tp -> BlockID blocks tp -> BlockID blocks tp)
-> Ord (BlockID blocks tp)
BlockID blocks tp -> BlockID blocks tp -> Bool
BlockID blocks tp -> BlockID blocks tp -> Ordering
BlockID blocks tp -> BlockID blocks tp -> BlockID blocks tp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Eq (BlockID blocks tp)
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> Bool
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> Ordering
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> BlockID blocks tp
$ccompare :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> Ordering
compare :: BlockID blocks tp -> BlockID blocks tp -> Ordering
$c< :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> Bool
< :: BlockID blocks tp -> BlockID blocks tp -> Bool
$c<= :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> Bool
<= :: BlockID blocks tp -> BlockID blocks tp -> Bool
$c> :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> Bool
> :: BlockID blocks tp -> BlockID blocks tp -> Bool
$c>= :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> Bool
>= :: BlockID blocks tp -> BlockID blocks tp -> Bool
$cmax :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> BlockID blocks tp
max :: BlockID blocks tp -> BlockID blocks tp -> BlockID blocks tp
$cmin :: forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> BlockID blocks tp -> BlockID blocks tp
min :: BlockID blocks tp -> BlockID blocks tp -> BlockID blocks tp
Ord)

instance TestEquality (BlockID blocks) where
  testEquality :: forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
BlockID blocks a -> BlockID blocks b -> Maybe (a :~: b)
testEquality (BlockID Index blocks a
x) (BlockID Index blocks b
y) = Index blocks a -> Index blocks b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
Index blocks a -> Index blocks b -> Maybe (a :~: b)
testEquality Index blocks a
x Index blocks b
y

instance OrdF (BlockID blocks) where
  compareF :: forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType).
BlockID blocks x -> BlockID blocks y -> OrderingF x y
compareF (BlockID Index blocks x
x) (BlockID Index blocks y
y) = Index blocks x -> Index blocks y -> OrderingF x y
forall k (ktp :: k -> Type) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
forall (x :: Ctx CrucibleType) (y :: Ctx CrucibleType).
Index blocks x -> Index blocks y -> OrderingF x y
compareF Index blocks x
x Index blocks y
y

instance Pretty (BlockID blocks tp) where
  pretty :: forall ann. BlockID blocks tp -> Doc ann
pretty (BlockID Index blocks tp
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
<> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Index blocks tp -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal Index blocks tp
i)

instance Show (BlockID blocks ctx) where
  show :: BlockID blocks ctx -> String
show (BlockID Index blocks ctx
i) = Char
'%' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show (Index blocks ctx -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal Index blocks ctx
i)

instance ShowF (BlockID blocks)

extendBlockID :: KnownDiff l r => BlockID l tp -> BlockID r tp
extendBlockID :: forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
KnownDiff l r =>
BlockID l tp -> BlockID r tp
extendBlockID = Index r tp -> BlockID r tp
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID (Index r tp -> BlockID r tp)
-> (BlockID l tp -> Index r tp) -> BlockID l tp -> BlockID r tp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index l tp -> Index r tp
forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
KnownDiff l r =>
Index l tp -> Index r tp
extendIndex (Index l tp -> Index r tp)
-> (BlockID l tp -> Index l tp) -> BlockID l tp -> Index r tp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlockID l tp -> Index l tp
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex

extendBlockID' :: Diff l r -> BlockID l tp -> BlockID r tp
extendBlockID' :: forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
Diff l r -> BlockID l tp -> BlockID r tp
extendBlockID' Diff l r
e = Index r tp -> BlockID r tp
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID (Index r tp -> BlockID r tp)
-> (BlockID l tp -> Index r tp) -> BlockID l tp -> BlockID r tp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Diff l r -> Index l tp -> Index r tp
forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' Diff l r
e (Index l tp -> Index r tp)
-> (BlockID l tp -> Index l tp) -> BlockID l tp -> Index r tp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlockID l tp -> Index l tp
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex

------------------------------------------------------------------------
-- JumpTarget

-- | Target for jump and branch statements
data JumpTarget blocks ctx where
     JumpTarget :: !(BlockID blocks args)            -- BlockID to jump to
                -> !(CtxRepr args)                   -- expected argument types
                -> !(Assignment (Reg ctx) args) -- jump target actual arguments
                -> JumpTarget blocks ctx

instance Pretty (JumpTarget blocks ctx) where
  pretty :: forall ann. JumpTarget blocks ctx -> Doc ann
pretty (JumpTarget BlockID blocks args
tgt CtxRepr args
_ Assignment (Reg ctx) args
a) = BlockID blocks args -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BlockID blocks args -> Doc ann
pretty BlockID blocks args
tgt 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 (f :: Type -> Type) ann.
Foldable f =>
f (Doc ann) -> Doc ann
commas (Assignment (Reg ctx) args -> [Doc ann]
forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType) ann.
Assignment (Reg ctx) args -> [Doc ann]
ppAssignment Assignment (Reg ctx) args
a))

jumpTargetID :: JumpTarget blocks ctx -> Some (BlockID blocks)
jumpTargetID :: forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
JumpTarget blocks ctx -> Some (BlockID blocks)
jumpTargetID (JumpTarget BlockID blocks args
tgt CtxRepr args
_ Assignment (Reg ctx) args
_) = BlockID blocks args -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks args
tgt

extendJumpTarget :: Diff blocks' blocks -> JumpTarget blocks' ctx -> JumpTarget blocks ctx
extendJumpTarget :: forall (blocks' :: Ctx (Ctx CrucibleType))
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType).
Diff blocks' blocks
-> JumpTarget blocks' ctx -> JumpTarget blocks ctx
extendJumpTarget Diff blocks' blocks
diff (JumpTarget BlockID blocks' args
b CtxRepr args
tps Assignment (Reg ctx) args
a) = BlockID blocks args
-> CtxRepr args
-> Assignment (Reg ctx) args
-> JumpTarget blocks ctx
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx' :: Ctx CrucibleType) (ctx :: Ctx CrucibleType).
BlockID blocks ctx'
-> CtxRepr ctx'
-> Assignment (Reg ctx) ctx'
-> JumpTarget blocks ctx
JumpTarget (Diff blocks' blocks -> BlockID blocks' args -> BlockID blocks args
forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
Diff l r -> BlockID l tp -> BlockID r tp
extendBlockID' Diff blocks' blocks
diff BlockID blocks' args
b) CtxRepr args
tps Assignment (Reg ctx) args
a

instance ApplyEmbedding (JumpTarget blocks) where
  applyEmbedding :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'
-> JumpTarget blocks ctx -> JumpTarget blocks ctx'
applyEmbedding CtxEmbedding ctx ctx'
ctxe (JumpTarget BlockID blocks args
dest CtxRepr args
tys Assignment (Reg ctx) args
args) =
    BlockID blocks args
-> CtxRepr args
-> Assignment (Reg ctx') args
-> JumpTarget blocks ctx'
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx' :: Ctx CrucibleType) (ctx :: Ctx CrucibleType).
BlockID blocks ctx'
-> CtxRepr ctx'
-> Assignment (Reg ctx) ctx'
-> JumpTarget blocks ctx
JumpTarget BlockID blocks args
dest CtxRepr args
tys ((forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Reg ctx) x -> Assignment (Reg ctx') x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC (CtxEmbedding ctx ctx' -> Reg ctx x -> Reg ctx' x
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ApplyEmbedding' f =>
CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
CtxEmbedding ctx ctx' -> Reg ctx v -> Reg ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe) Assignment (Reg ctx) args
args)

instance ExtendContext (JumpTarget blocks) where
  extendContext :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
Diff ctx ctx' -> JumpTarget blocks ctx -> JumpTarget blocks ctx'
extendContext Diff ctx ctx'
diff (JumpTarget BlockID blocks args
dest CtxRepr args
tys Assignment (Reg ctx) args
args) =
    BlockID blocks args
-> CtxRepr args
-> Assignment (Reg ctx') args
-> JumpTarget blocks ctx'
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx' :: Ctx CrucibleType) (ctx :: Ctx CrucibleType).
BlockID blocks ctx'
-> CtxRepr ctx'
-> Assignment (Reg ctx) ctx'
-> JumpTarget blocks ctx
JumpTarget BlockID blocks args
dest CtxRepr args
tys ((forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Reg ctx) x -> Assignment (Reg ctx') x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC (Diff ctx ctx' -> Reg ctx x -> Reg ctx' x
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ExtendContext' f =>
Diff ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
Diff ctx ctx' -> Reg ctx v -> Reg ctx' v
extendContext' Diff ctx ctx'
diff) Assignment (Reg ctx) args
args)

------------------------------------------------------------------------
-- SwitchTarget

-- | Target for a switch statement.
data SwitchTarget blocks ctx tp where
  SwitchTarget :: !(BlockID blocks (args ::> tp))   -- BlockID to jump to
               -> !(CtxRepr args)                   -- expected argument types
               -> !(Assignment (Reg ctx) args) -- switch target actual arguments
               -> SwitchTarget blocks ctx tp

switchTargetID :: SwitchTarget blocks ctx tp -> Some (BlockID blocks)
switchTargetID :: forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
SwitchTarget blocks ctx tp -> Some (BlockID blocks)
switchTargetID (SwitchTarget BlockID blocks (args ::> tp)
tgt CtxRepr args
_ Assignment (Reg ctx) args
_) = BlockID blocks (args ::> tp) -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks (args ::> tp)
tgt

ppCase :: String -> SwitchTarget blocks ctx tp -> Doc ann
ppCase :: forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) ann.
String -> SwitchTarget blocks ctx tp -> Doc ann
ppCase String
nm (SwitchTarget BlockID blocks (args ::> tp)
tgt CtxRepr args
_ Assignment (Reg ctx) args
a) =
  String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
nm Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"->" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> BlockID blocks (args ::> tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BlockID blocks (args ::> tp) -> Doc ann
pretty BlockID blocks (args ::> tp)
tgt 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 (f :: Type -> Type) ann.
Foldable f =>
f (Doc ann) -> Doc ann
commas (Assignment (Reg ctx) args -> [Doc ann]
forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType) ann.
Assignment (Reg ctx) args -> [Doc ann]
ppAssignment Assignment (Reg ctx) args
a))

extendSwitchTarget :: Diff blocks' blocks
                   -> SwitchTarget blocks' ctx tp
                   -> SwitchTarget blocks ctx tp
extendSwitchTarget :: forall (blocks' :: Ctx (Ctx CrucibleType))
       (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
Diff blocks' blocks
-> SwitchTarget blocks' ctx tp -> SwitchTarget blocks ctx tp
extendSwitchTarget Diff blocks' blocks
diff (SwitchTarget BlockID blocks' (args ::> tp)
b CtxRepr args
tps Assignment (Reg ctx) args
a) =
    BlockID blocks (args ::> tp)
-> CtxRepr args
-> Assignment (Reg ctx) args
-> SwitchTarget blocks ctx tp
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx' :: Ctx CrucibleType) (tp :: CrucibleType)
       (ctx :: Ctx CrucibleType).
BlockID blocks (ctx' ::> tp)
-> CtxRepr ctx'
-> Assignment (Reg ctx) ctx'
-> SwitchTarget blocks ctx tp
SwitchTarget (Diff blocks' blocks
-> BlockID blocks' (args ::> tp) -> BlockID blocks (args ::> tp)
forall (l :: Ctx (Ctx CrucibleType)) (r :: Ctx (Ctx CrucibleType))
       (tp :: Ctx CrucibleType).
Diff l r -> BlockID l tp -> BlockID r tp
extendBlockID' Diff blocks' blocks
diff BlockID blocks' (args ::> tp)
b) CtxRepr args
tps Assignment (Reg ctx) args
a

instance ApplyEmbedding' (SwitchTarget blocks) where
  applyEmbedding' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
CtxEmbedding ctx ctx'
-> SwitchTarget blocks ctx v -> SwitchTarget blocks ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe (SwitchTarget BlockID blocks (args ::> v)
dest CtxRepr args
tys Assignment (Reg ctx) args
args) =
    BlockID blocks (args ::> v)
-> CtxRepr args
-> Assignment (Reg ctx') args
-> SwitchTarget blocks ctx' v
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx' :: Ctx CrucibleType) (tp :: CrucibleType)
       (ctx :: Ctx CrucibleType).
BlockID blocks (ctx' ::> tp)
-> CtxRepr ctx'
-> Assignment (Reg ctx) ctx'
-> SwitchTarget blocks ctx tp
SwitchTarget BlockID blocks (args ::> v)
dest CtxRepr args
tys ((forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Reg ctx) x -> Assignment (Reg ctx') x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC (CtxEmbedding ctx ctx' -> Reg ctx x -> Reg ctx' x
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ApplyEmbedding' f =>
CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
CtxEmbedding ctx ctx' -> Reg ctx v -> Reg ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe) Assignment (Reg ctx) args
args)

instance ExtendContext' (SwitchTarget blocks) where
  extendContext' :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
Diff ctx ctx'
-> SwitchTarget blocks ctx v -> SwitchTarget blocks ctx' v
extendContext' Diff ctx ctx'
diff (SwitchTarget BlockID blocks (args ::> v)
dest CtxRepr args
tys Assignment (Reg ctx) args
args) =
    BlockID blocks (args ::> v)
-> CtxRepr args
-> Assignment (Reg ctx') args
-> SwitchTarget blocks ctx' v
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx' :: Ctx CrucibleType) (tp :: CrucibleType)
       (ctx :: Ctx CrucibleType).
BlockID blocks (ctx' ::> tp)
-> CtxRepr ctx'
-> Assignment (Reg ctx) ctx'
-> SwitchTarget blocks ctx tp
SwitchTarget BlockID blocks (args ::> v)
dest CtxRepr args
tys ((forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Reg ctx) x -> Assignment (Reg ctx') x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC (Diff ctx ctx' -> Reg ctx x -> Reg ctx' x
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ExtendContext' f =>
Diff ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
Diff ctx ctx' -> Reg ctx v -> Reg ctx' v
extendContext' Diff ctx ctx'
diff) Assignment (Reg ctx) args
args)


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

-- | A sequential statement that does not affect the
-- program location within the current block or leave the current
-- block.
data Stmt ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) where
  -- Assign the value of a register
  SetReg :: !(TypeRepr tp)
         -> !(Expr ext ctx tp)
         -> Stmt ext ctx (ctx ::> tp)

  -- Assign a register via an extension statement
  ExtendAssign :: !(StmtExtension ext (Reg ctx) tp)
               -> Stmt ext ctx (ctx ::> tp)

  -- Statement used for evaluating function calls
  CallHandle :: !(TypeRepr ret)                          -- The type of the return value(s)
             -> !(Reg ctx (FunctionHandleType args ret)) -- The function handle to call
             -> !(CtxRepr args)                          -- The expected types of the arguments
             -> !(Assignment (Reg ctx) args)             -- The actual arguments to the call
             -> Stmt ext ctx (ctx ::> ret)

  -- Print a message out to the console
  Print :: !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx

  -- Read a global variable.
  ReadGlobal :: !(GlobalVar tp)
             -> Stmt ext ctx (ctx ::> tp)

  -- Write to a global variable.
  WriteGlobal :: !(GlobalVar tp)
              -> !(Reg ctx tp)
              -> Stmt ext ctx ctx

  -- Create a fresh constant
  FreshConstant :: !(BaseTypeRepr bt)
                -> !(Maybe SolverSymbol)
                -> Stmt ext ctx (ctx ::> BaseToType bt)

  -- Create a fresh floating-point constant
  FreshFloat :: !(FloatInfoRepr fi)
             -> !(Maybe SolverSymbol)
             -> Stmt ext ctx (ctx ::> FloatType fi)

  -- Create a fresh natural number constant
  FreshNat :: !(Maybe SolverSymbol)
           -> Stmt  ext ctx (ctx ::> NatType)

  -- Allocate a new reference cell
  NewRefCell :: !(TypeRepr tp)
             -> !(Reg ctx tp)
             -> Stmt ext ctx (ctx ::> ReferenceType tp)

  -- Allocate a new, unassigned reference cell
  NewEmptyRefCell :: !(TypeRepr tp)
                  -> Stmt ext ctx (ctx ::> ReferenceType tp)

  -- Read the current value of a reference cell
  ReadRefCell :: !(Reg ctx (ReferenceType tp))
              -> Stmt ext ctx (ctx ::> tp)

  -- Write the current value of a reference cell
  WriteRefCell :: !(Reg ctx (ReferenceType tp))
               -> !(Reg ctx tp)
               -> Stmt ext ctx ctx

  -- Deallocate the storage associated with a reference cell
  DropRefCell  :: !(Reg ctx (ReferenceType tp))
               -> Stmt ext ctx ctx

  -- Assert a boolean condition.  If the condition fails, print the given string.
  Assert :: !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx

  -- Assume a boolean condition, remembering the given string as the 'reason' for this assumption.
  Assume :: !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx

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

data TermStmt blocks (ret :: CrucibleType) (ctx :: Ctx CrucibleType) where
  -- Jump to the given jump target
  Jump :: !(JumpTarget blocks ctx)
       -> TermStmt blocks ret ctx

  -- Branch on condition.  If true, jump to the first jump target; otherwise
  -- jump to the second jump target.
  Br :: !(Reg ctx BoolType)
     -> !(JumpTarget blocks ctx)
     -> !(JumpTarget blocks ctx)
     -> TermStmt blocks ret ctx

  -- Switch on whether this is a maybe value.  Jump to the switch target if
  -- the maybe value is a "Some".  Otherwise (if "Nothing"), jump to the jump target.
  MaybeBranch :: !(TypeRepr tp)
              -> !(Reg ctx (MaybeType tp))
              -> !(SwitchTarget blocks ctx tp)
              -> !(JumpTarget blocks ctx)
              -> TermStmt blocks rtp ctx

  -- Switch on a variant value.  Examine the tag of the variant
  -- and jump to the appropriate switch target.
  VariantElim :: !(CtxRepr varctx)
              -> !(Reg ctx (VariantType varctx))
              -> !(Assignment (SwitchTarget blocks ctx) varctx)
              -> TermStmt blocks ret ctx

  -- Return from function, providing the return value(s).
  Return :: !(Reg ctx ret)
         -> TermStmt blocks ret ctx

  -- End block with a tail call.
  TailCall :: !(Reg ctx (FunctionHandleType args ret))
           -> !(CtxRepr args)
           -> !(Assignment (Reg ctx) args)
           -> TermStmt blocks ret ctx

  -- Block ends with an error.
  ErrorStmt :: !(Reg ctx (StringType Unicode)) -> TermStmt blocks ret ctx

#ifndef UNSAFE_OPS
extendTermStmt :: Diff blocks' blocks -> TermStmt blocks' ret ctx -> TermStmt blocks ret ctx
extendTermStmt diff (Jump tgt) = Jump (extendJumpTarget diff tgt)
extendTermStmt diff (Br c x y) = Br c (extendJumpTarget diff x) (extendJumpTarget diff y)
extendTermStmt diff (MaybeBranch tp c x y) =
  MaybeBranch tp c (extendSwitchTarget diff x) (extendJumpTarget diff y)
extendTermStmt diff (VariantElim ctx e asgn) =
  VariantElim ctx e (fmapFC (extendSwitchTarget diff) asgn)
extendTermStmt _diff (Return e) = Return e
extendTermStmt _diff (TailCall h tps args) = TailCall h tps args
extendTermStmt _diff (ErrorStmt e) = ErrorStmt e
#endif

-- | Return the set of possible next blocks from a TermStmt
termStmtNextBlocks :: TermStmt b ret ctx -> Maybe [Some (BlockID b)]
termStmtNextBlocks :: forall (b :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TermStmt b ret ctx -> Maybe [Some (BlockID b)]
termStmtNextBlocks TermStmt b ret ctx
s0 =
  case TermStmt b ret ctx
s0 of
    Jump JumpTarget b ctx
tgt             -> [Some (BlockID b)] -> Maybe [Some (BlockID b)]
forall a. a -> Maybe a
Just [ JumpTarget b ctx -> Some (BlockID b)
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
JumpTarget blocks ctx -> Some (BlockID blocks)
jumpTargetID JumpTarget b ctx
tgt ]
    Br          Reg ctx BoolType
_ JumpTarget b ctx
x JumpTarget b ctx
y    -> [Some (BlockID b)] -> Maybe [Some (BlockID b)]
forall a. a -> Maybe a
Just [ JumpTarget b ctx -> Some (BlockID b)
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
JumpTarget blocks ctx -> Some (BlockID blocks)
jumpTargetID JumpTarget b ctx
x, JumpTarget b ctx -> Some (BlockID b)
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
JumpTarget blocks ctx -> Some (BlockID blocks)
jumpTargetID JumpTarget b ctx
y ]
    MaybeBranch TypeRepr tp
_ Reg ctx (MaybeType tp)
_ SwitchTarget b ctx tp
x JumpTarget b ctx
y  -> [Some (BlockID b)] -> Maybe [Some (BlockID b)]
forall a. a -> Maybe a
Just [ SwitchTarget b ctx tp -> Some (BlockID b)
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
SwitchTarget blocks ctx tp -> Some (BlockID blocks)
switchTargetID SwitchTarget b ctx tp
x, JumpTarget b ctx -> Some (BlockID b)
forall (blocks :: Ctx (Ctx CrucibleType))
       (ctx :: Ctx CrucibleType).
JumpTarget blocks ctx -> Some (BlockID blocks)
jumpTargetID JumpTarget b ctx
y ]
    VariantElim CtxRepr varctx
_ Reg ctx (VariantType varctx)
_ Assignment (SwitchTarget b ctx) varctx
a    -> [Some (BlockID b)] -> Maybe [Some (BlockID b)]
forall a. a -> Maybe a
Just ((forall (x :: CrucibleType).
 SwitchTarget b ctx x -> Some (BlockID b))
-> forall (x :: Ctx CrucibleType).
   Assignment (SwitchTarget b ctx) x -> [Some (BlockID b)]
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 SwitchTarget b ctx x -> Some (BlockID b)
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
SwitchTarget blocks ctx tp -> Some (BlockID blocks)
forall (x :: CrucibleType).
SwitchTarget b ctx x -> Some (BlockID b)
switchTargetID Assignment (SwitchTarget b ctx) varctx
a)
    Return      Reg ctx ret
_        -> Maybe [Some (BlockID b)]
forall a. Maybe a
Nothing
    TailCall    Reg ctx (FunctionHandleType args ret)
_ CtxRepr args
_ Assignment (Reg ctx) args
_    -> Maybe [Some (BlockID b)]
forall a. Maybe a
Nothing
    ErrorStmt   Reg ctx (StringType Unicode)
_        -> [Some (BlockID b)] -> Maybe [Some (BlockID b)]
forall a. a -> Maybe a
Just []

instance Pretty (TermStmt blocks ret ctx) where
 pretty :: forall ann. TermStmt blocks ret ctx -> Doc ann
pretty TermStmt blocks ret ctx
s =
  case TermStmt blocks ret ctx
s of
    Jump JumpTarget blocks ctx
b   -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"jump" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> JumpTarget blocks ctx -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. JumpTarget blocks ctx -> Doc ann
pretty JumpTarget blocks ctx
b
    Br Reg ctx BoolType
e JumpTarget blocks ctx
x JumpTarget blocks ctx
y -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"br"  Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Reg ctx BoolType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx BoolType -> Doc ann
pretty Reg ctx BoolType
e Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> JumpTarget blocks ctx -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. JumpTarget blocks ctx -> Doc ann
pretty JumpTarget blocks ctx
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> JumpTarget blocks ctx -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. JumpTarget blocks ctx -> Doc ann
pretty JumpTarget blocks ctx
y
    MaybeBranch TypeRepr tp
_ Reg ctx (MaybeType tp)
e SwitchTarget blocks ctx tp
j JumpTarget blocks ctx
n ->
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
      [ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"maybeBranch" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Reg ctx (MaybeType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (MaybeType tp) -> Doc ann
pretty Reg ctx (MaybeType tp)
e Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
forall ann. Doc ann
lbrace
      , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
          [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ String -> SwitchTarget blocks ctx tp -> Doc ann
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) ann.
String -> SwitchTarget blocks ctx tp -> Doc ann
ppCase String
"Just" SwitchTarget blocks ctx tp
j
               , String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"Nothing ->" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> JumpTarget blocks ctx -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. JumpTarget blocks ctx -> Doc ann
pretty JumpTarget blocks ctx
n
               , Doc ann
forall ann. Doc ann
rbrace
               ]
      ]
    VariantElim CtxRepr varctx
_ Reg ctx (VariantType varctx)
e Assignment (SwitchTarget blocks ctx) varctx
asgn ->
      let branches :: [Doc ann]
branches =
              [ String -> Doc ann
f (Int -> String
forall a. Show a => a -> String
show Int
i) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
semi
              | Int
i <- [(Int
0::Int) .. ]
              | String -> Doc ann
f <- (forall (x :: CrucibleType).
 SwitchTarget blocks ctx x -> String -> Doc ann)
-> forall (x :: Ctx CrucibleType).
   Assignment (SwitchTarget blocks ctx) x -> [String -> 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 (\SwitchTarget blocks ctx x
tgt String
nm -> String -> SwitchTarget blocks ctx x -> Doc ann
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType) ann.
String -> SwitchTarget blocks ctx tp -> Doc ann
ppCase String
nm SwitchTarget blocks ctx x
tgt) Assignment (SwitchTarget blocks ctx) varctx
asgn
              ] in
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
      [ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"vswitch" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Reg ctx (VariantType varctx) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (VariantType varctx) -> Doc ann
pretty Reg ctx (VariantType varctx)
e Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
forall ann. Doc ann
lbrace
      , 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 [Doc ann]
branches)
      , Doc ann
forall ann. Doc ann
rbrace
      ]
    Return Reg ctx ret
e ->
      String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"return"
       Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Reg ctx ret -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx ret -> Doc ann
pretty Reg ctx ret
e
    TailCall Reg ctx (FunctionHandleType args ret)
h CtxRepr args
_ Assignment (Reg ctx) args
args ->
      String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"tailCall"
       Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Reg ctx (FunctionHandleType args ret) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (FunctionHandleType args ret) -> Doc ann
pretty Reg ctx (FunctionHandleType args ret)
h
       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 (f :: Type -> Type) ann.
Foldable f =>
f (Doc ann) -> Doc ann
commas (Assignment (Reg ctx) args -> [Doc ann]
forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType) ann.
Assignment (Reg ctx) args -> [Doc ann]
ppAssignment Assignment (Reg ctx) args
args))
    ErrorStmt Reg ctx (StringType Unicode)
msg ->
      String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"error" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Reg ctx (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (StringType Unicode) -> Doc ann
pretty Reg ctx (StringType Unicode)
msg


applyEmbeddingStmt :: forall ext ctx ctx' sctx.
                      TraverseExt ext =>
                      CtxEmbedding ctx ctx' ->
                      Stmt ext ctx sctx ->
                      Pair (Stmt ext ctx') (CtxEmbedding sctx)
applyEmbeddingStmt :: forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (sctx :: Ctx CrucibleType).
TraverseExt ext =>
CtxEmbedding ctx ctx'
-> Stmt ext ctx sctx -> Pair (Stmt ext ctx') (CtxEmbedding sctx)
applyEmbeddingStmt CtxEmbedding ctx ctx'
ctxe Stmt ext ctx sctx
stmt =
  case Stmt ext ctx sctx
stmt of
    SetReg TypeRepr tp
tp Expr ext ctx tp
e -> Stmt ext ctx' (ctx' ::> tp)
-> CtxEmbedding sctx (ctx' ::> tp)
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (TypeRepr tp -> Expr ext ctx' tp -> Stmt ext ctx' (ctx' ::> tp)
forall (ctx' :: CrucibleType) ext (ctx :: Ctx CrucibleType).
TypeRepr ctx' -> Expr ext ctx ctx' -> Stmt ext ctx (ctx ::> ctx')
SetReg TypeRepr tp
tp (CtxEmbedding ctx ctx' -> Expr ext ctx tp -> Expr ext ctx' tp
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ApplyEmbedding' f =>
CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
CtxEmbedding ctx ctx' -> Expr ext ctx v -> Expr ext ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe Expr ext ctx tp
e))
                        (CtxEmbedding ctx ctx' -> CtxEmbedding (ctx '::> tp) (ctx' ::> tp)
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe)

    ExtendAssign StmtExtension ext (Reg ctx) tp
estmt ->
       Stmt ext ctx' (ctx' ::> tp)
-> CtxEmbedding sctx (ctx' ::> tp)
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (StmtExtension ext (Reg ctx') tp -> Stmt ext ctx' (ctx' ::> tp)
forall ext (ctx :: Ctx CrucibleType) (ctx' :: CrucibleType).
StmtExtension ext (Reg ctx) ctx' -> Stmt ext ctx (ctx ::> ctx')
ExtendAssign ((forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x)
-> forall (x :: CrucibleType).
   StmtExtension ext (Reg ctx) x -> StmtExtension ext (Reg ctx') x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType).
   StmtExtension ext f x -> StmtExtension ext g x
fmapFC (CtxEmbedding ctx ctx' -> Reg ctx x -> Reg ctx' x
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ApplyEmbedding' f =>
CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
CtxEmbedding ctx ctx' -> Reg ctx v -> Reg ctx' v
Ctx.applyEmbedding' CtxEmbedding ctx ctx'
ctxe) StmtExtension ext (Reg ctx) tp
estmt))
            (CtxEmbedding ctx ctx' -> CtxEmbedding (ctx '::> tp) (ctx' ::> tp)
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
Ctx.extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe)

    CallHandle TypeRepr ret
ret Reg ctx (FunctionHandleType args ret)
hdl CtxRepr args
tys Assignment (Reg ctx) args
args ->
      Stmt ext ctx' (ctx' ::> ret)
-> CtxEmbedding sctx (ctx' ::> ret)
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (TypeRepr ret
-> Reg ctx' (FunctionHandleType args ret)
-> CtxRepr args
-> Assignment (Reg ctx') args
-> Stmt ext ctx' (ctx' ::> ret)
forall (ctx' :: CrucibleType) (ctx :: Ctx CrucibleType)
       (args :: Ctx CrucibleType) ext.
TypeRepr ctx'
-> Reg ctx (FunctionHandleType args ctx')
-> CtxRepr args
-> Assignment (Reg ctx) args
-> Stmt ext ctx (ctx ::> ctx')
CallHandle TypeRepr ret
ret (Reg ctx (FunctionHandleType args ret)
-> Reg ctx' (FunctionHandleType args ret)
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx (FunctionHandleType args ret)
hdl) CtxRepr args
tys ((forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Reg ctx) x -> Assignment (Reg ctx') x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC Reg ctx x -> Reg ctx' x
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Assignment (Reg ctx) args
args))
           (CtxEmbedding ctx ctx' -> CtxEmbedding (ctx '::> ret) (ctx' ::> ret)
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe)

    Print Reg ctx (StringType Unicode)
str -> Stmt ext ctx' ctx'
-> CtxEmbedding sctx ctx'
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (Reg ctx' (StringType Unicode) -> Stmt ext ctx' ctx'
forall (ctx :: Ctx CrucibleType) ext.
Reg ctx (StringType Unicode) -> Stmt ext ctx ctx
Print (Reg ctx (StringType Unicode) -> Reg ctx' (StringType Unicode)
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx (StringType Unicode)
str)) CtxEmbedding ctx ctx'
CtxEmbedding sctx ctx'
ctxe

    ReadGlobal GlobalVar tp
var -> Stmt ext ctx' (ctx' ::> tp)
-> CtxEmbedding sctx (ctx' ::> tp)
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (GlobalVar tp -> Stmt ext ctx' (ctx' ::> tp)
forall (ctx' :: CrucibleType) ext (ctx :: Ctx CrucibleType).
GlobalVar ctx' -> Stmt ext ctx (ctx ::> ctx')
ReadGlobal GlobalVar tp
var)
                           (CtxEmbedding ctx ctx' -> CtxEmbedding (ctx '::> tp) (ctx' ::> tp)
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe)

    WriteGlobal GlobalVar tp
var Reg ctx tp
r -> Stmt ext ctx' ctx'
-> CtxEmbedding sctx ctx'
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (GlobalVar tp -> Reg ctx' tp -> Stmt ext ctx' ctx'
forall (ctx' :: CrucibleType) (ctx :: Ctx CrucibleType) ext.
GlobalVar ctx' -> Reg ctx ctx' -> Stmt ext ctx ctx
WriteGlobal GlobalVar tp
var (Reg ctx tp -> Reg ctx' tp
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx tp
r)) CtxEmbedding ctx ctx'
CtxEmbedding sctx ctx'
ctxe

    FreshConstant BaseTypeRepr bt
bt Maybe SolverSymbol
nm -> Stmt ext ctx' (ctx' ::> BaseToType bt)
-> CtxEmbedding sctx (ctx' ::> BaseToType bt)
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (BaseTypeRepr bt
-> Maybe SolverSymbol -> Stmt ext ctx' (ctx' ::> BaseToType bt)
forall (ctx' :: BaseType) ext (ctx :: Ctx CrucibleType).
BaseTypeRepr ctx'
-> Maybe SolverSymbol -> Stmt ext ctx (ctx ::> BaseToType ctx')
FreshConstant BaseTypeRepr bt
bt Maybe SolverSymbol
nm)
                                (CtxEmbedding ctx ctx'
-> CtxEmbedding (ctx '::> BaseToType bt) (ctx' ::> BaseToType bt)
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
Ctx.extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe)

    FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
nm -> Stmt ext ctx' (ctx' ::> FloatType fi)
-> CtxEmbedding sctx (ctx' ::> FloatType fi)
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (FloatInfoRepr fi
-> Maybe SolverSymbol -> Stmt ext ctx' (ctx' ::> FloatType fi)
forall (ctx' :: FloatInfo) ext (ctx :: Ctx CrucibleType).
FloatInfoRepr ctx'
-> Maybe SolverSymbol -> Stmt ext ctx (ctx ::> FloatType ctx')
FreshFloat FloatInfoRepr fi
fi Maybe SolverSymbol
nm)
                             (CtxEmbedding ctx ctx'
-> CtxEmbedding (ctx '::> FloatType fi) (ctx' ::> FloatType fi)
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
Ctx.extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe)

    FreshNat Maybe SolverSymbol
nm -> Stmt ext ctx' (ctx' ::> NatType)
-> CtxEmbedding sctx (ctx' ::> NatType)
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (Maybe SolverSymbol -> Stmt ext ctx' (ctx' ::> NatType)
forall ext (ctx :: Ctx CrucibleType).
Maybe SolverSymbol -> Stmt ext ctx (ctx ::> NatType)
FreshNat Maybe SolverSymbol
nm) (CtxEmbedding ctx ctx'
-> CtxEmbedding (ctx '::> NatType) (ctx' ::> NatType)
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
Ctx.extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe)

    NewRefCell TypeRepr tp
tp Reg ctx tp
r -> Stmt ext ctx' (ctx' ::> ReferenceType tp)
-> CtxEmbedding sctx (ctx' ::> ReferenceType tp)
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (TypeRepr tp
-> Reg ctx' tp -> Stmt ext ctx' (ctx' ::> ReferenceType tp)
forall (ctx' :: CrucibleType) (ctx :: Ctx CrucibleType) ext.
TypeRepr ctx'
-> Reg ctx ctx' -> Stmt ext ctx (ctx ::> ReferenceType ctx')
NewRefCell TypeRepr tp
tp (Reg ctx tp -> Reg ctx' tp
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx tp
r))
                            (CtxEmbedding ctx ctx'
-> CtxEmbedding
     (ctx '::> ReferenceType tp) (ctx' ::> ReferenceType tp)
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
Ctx.extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe)
    NewEmptyRefCell TypeRepr tp
tp -> Stmt ext ctx' (ctx' ::> ReferenceType tp)
-> CtxEmbedding sctx (ctx' ::> ReferenceType tp)
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (TypeRepr tp -> Stmt ext ctx' (ctx' ::> ReferenceType tp)
forall (ctx' :: CrucibleType) ext (ctx :: Ctx CrucibleType).
TypeRepr ctx' -> Stmt ext ctx (ctx ::> ReferenceType ctx')
NewEmptyRefCell TypeRepr tp
tp)
                               (CtxEmbedding ctx ctx'
-> CtxEmbedding
     (ctx '::> ReferenceType tp) (ctx' ::> ReferenceType tp)
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
Ctx.extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe)
    ReadRefCell Reg ctx (ReferenceType tp)
r     -> Stmt ext ctx' (ctx' ::> tp)
-> CtxEmbedding sctx (ctx' ::> tp)
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (Reg ctx' (ReferenceType tp) -> Stmt ext ctx' (ctx' ::> tp)
forall (ctx :: Ctx CrucibleType) (ctx' :: CrucibleType) ext.
Reg ctx (ReferenceType ctx') -> Stmt ext ctx (ctx ::> ctx')
ReadRefCell (Reg ctx (ReferenceType tp) -> Reg ctx' (ReferenceType tp)
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx (ReferenceType tp)
r))
                              (CtxEmbedding ctx ctx' -> CtxEmbedding (ctx '::> tp) (ctx' ::> tp)
forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
Ctx.extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe)
    WriteRefCell Reg ctx (ReferenceType tp)
r Reg ctx tp
r' -> Stmt ext ctx' ctx'
-> CtxEmbedding sctx ctx'
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (Reg ctx' (ReferenceType tp) -> Reg ctx' tp -> Stmt ext ctx' ctx'
forall (ctx :: Ctx CrucibleType) (ctx' :: CrucibleType) ext.
Reg ctx (ReferenceType ctx') -> Reg ctx ctx' -> Stmt ext ctx ctx
WriteRefCell (Reg ctx (ReferenceType tp) -> Reg ctx' (ReferenceType tp)
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx (ReferenceType tp)
r) (Reg ctx tp -> Reg ctx' tp
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx tp
r')) CtxEmbedding ctx ctx'
CtxEmbedding sctx ctx'
ctxe
    DropRefCell Reg ctx (ReferenceType tp)
r     -> Stmt ext ctx' ctx'
-> CtxEmbedding sctx ctx'
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (Reg ctx' (ReferenceType tp) -> Stmt ext ctx' ctx'
forall (ctx :: Ctx CrucibleType) (ctx' :: CrucibleType) ext.
Reg ctx (ReferenceType ctx') -> Stmt ext ctx ctx
DropRefCell (Reg ctx (ReferenceType tp) -> Reg ctx' (ReferenceType tp)
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx (ReferenceType tp)
r)) CtxEmbedding ctx ctx'
CtxEmbedding sctx ctx'
ctxe
    Assert Reg ctx BoolType
b Reg ctx (StringType Unicode)
str      -> Stmt ext ctx' ctx'
-> CtxEmbedding sctx ctx'
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (Reg ctx' BoolType
-> Reg ctx' (StringType Unicode) -> Stmt ext ctx' ctx'
forall (ctx :: Ctx CrucibleType) ext.
Reg ctx BoolType
-> Reg ctx (StringType Unicode) -> Stmt ext ctx ctx
Assert (Reg ctx BoolType -> Reg ctx' BoolType
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx BoolType
b) (Reg ctx (StringType Unicode) -> Reg ctx' (StringType Unicode)
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx (StringType Unicode)
str)) CtxEmbedding ctx ctx'
CtxEmbedding sctx ctx'
ctxe
    Assume Reg ctx BoolType
b Reg ctx (StringType Unicode)
str      -> Stmt ext ctx' ctx'
-> CtxEmbedding sctx ctx'
-> Pair (Stmt ext ctx') (CtxEmbedding sctx)
forall {k} (a :: k -> Type) (tp :: k) (b :: k -> Type).
a tp -> b tp -> Pair a b
Pair (Reg ctx' BoolType
-> Reg ctx' (StringType Unicode) -> Stmt ext ctx' ctx'
forall (ctx :: Ctx CrucibleType) ext.
Reg ctx BoolType
-> Reg ctx (StringType Unicode) -> Stmt ext ctx ctx
Assume (Reg ctx BoolType -> Reg ctx' BoolType
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx BoolType
b) (Reg ctx (StringType Unicode) -> Reg ctx' (StringType Unicode)
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg Reg ctx (StringType Unicode)
str)) CtxEmbedding ctx ctx'
CtxEmbedding sctx ctx'
ctxe
  where
    reg :: forall tp. Reg ctx tp -> Reg ctx' tp
    reg :: forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
reg = CtxEmbedding ctx ctx' -> Reg ctx tp -> Reg ctx' tp
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ApplyEmbedding' f =>
CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: CrucibleType).
CtxEmbedding ctx ctx' -> Reg ctx v -> Reg ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe


instance ApplyEmbedding (TermStmt blocks ret) where
  applyEmbedding :: forall ctx ctx'.
                    CtxEmbedding ctx ctx'
                    -> TermStmt blocks ret ctx
                    -> TermStmt blocks ret ctx'
  applyEmbedding :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'
-> TermStmt blocks ret ctx -> TermStmt blocks ret ctx'
applyEmbedding CtxEmbedding ctx ctx'
ctxe TermStmt blocks ret ctx
term =
    case TermStmt blocks ret ctx
term of
      Jump JumpTarget blocks ctx
jt -> JumpTarget blocks ctx' -> TermStmt blocks ret ctx'
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
Jump (JumpTarget blocks ctx -> JumpTarget blocks ctx'
forall (f :: Ctx CrucibleType -> Type).
ApplyEmbedding f =>
f ctx -> f ctx'
apC JumpTarget blocks ctx
jt)
      Br Reg ctx BoolType
b JumpTarget blocks ctx
jtl JumpTarget blocks ctx
jtr -> Reg ctx' BoolType
-> JumpTarget blocks ctx'
-> JumpTarget blocks ctx'
-> TermStmt blocks ret ctx'
forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
Reg ctx BoolType
-> JumpTarget blocks ctx
-> JumpTarget blocks ctx
-> TermStmt blocks ret ctx
Br (Reg ctx BoolType -> Reg ctx' BoolType
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ApplyEmbedding' f =>
f ctx v -> f ctx' v
apC' Reg ctx BoolType
b) (JumpTarget blocks ctx -> JumpTarget blocks ctx'
forall (f :: Ctx CrucibleType -> Type).
ApplyEmbedding f =>
f ctx -> f ctx'
apC JumpTarget blocks ctx
jtl) (JumpTarget blocks ctx -> JumpTarget blocks ctx'
forall (f :: Ctx CrucibleType -> Type).
ApplyEmbedding f =>
f ctx -> f ctx'
apC JumpTarget blocks ctx
jtr)
      MaybeBranch TypeRepr tp
tp Reg ctx (MaybeType tp)
b SwitchTarget blocks ctx tp
swt JumpTarget blocks ctx
jt    -> TypeRepr tp
-> Reg ctx' (MaybeType tp)
-> SwitchTarget blocks ctx' tp
-> JumpTarget blocks ctx'
-> TermStmt blocks ret ctx'
forall (ctx' :: CrucibleType) (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (rtp :: CrucibleType).
TypeRepr ctx'
-> Reg ctx (MaybeType ctx')
-> SwitchTarget blocks ctx ctx'
-> JumpTarget blocks ctx
-> TermStmt blocks rtp ctx
MaybeBranch TypeRepr tp
tp (Reg ctx (MaybeType tp) -> Reg ctx' (MaybeType tp)
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ApplyEmbedding' f =>
f ctx v -> f ctx' v
apC' Reg ctx (MaybeType tp)
b) (SwitchTarget blocks ctx tp -> SwitchTarget blocks ctx' tp
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ApplyEmbedding' f =>
f ctx v -> f ctx' v
apC' SwitchTarget blocks ctx tp
swt) (JumpTarget blocks ctx -> JumpTarget blocks ctx'
forall (f :: Ctx CrucibleType -> Type).
ApplyEmbedding f =>
f ctx -> f ctx'
apC JumpTarget blocks ctx
jt)
      VariantElim CtxRepr varctx
repr Reg ctx (VariantType varctx)
r Assignment (SwitchTarget blocks ctx) varctx
targets -> CtxRepr varctx
-> Reg ctx' (VariantType varctx)
-> Assignment (SwitchTarget blocks ctx') varctx
-> TermStmt blocks ret ctx'
forall (ctx' :: Ctx CrucibleType) (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
CtxRepr ctx'
-> Reg ctx (VariantType ctx')
-> Assignment (SwitchTarget blocks ctx) ctx'
-> TermStmt blocks ret ctx
VariantElim CtxRepr varctx
repr (Reg ctx (VariantType varctx) -> Reg ctx' (VariantType varctx)
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ApplyEmbedding' f =>
f ctx v -> f ctx' v
apC' Reg ctx (VariantType varctx)
r) ((forall (x :: CrucibleType).
 SwitchTarget blocks ctx x -> SwitchTarget blocks ctx' x)
-> forall (x :: Ctx CrucibleType).
   Assignment (SwitchTarget blocks ctx) x
   -> Assignment (SwitchTarget blocks ctx') x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC SwitchTarget blocks ctx x -> SwitchTarget blocks ctx' x
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ApplyEmbedding' f =>
f ctx v -> f ctx' v
forall (x :: CrucibleType).
SwitchTarget blocks ctx x -> SwitchTarget blocks ctx' x
apC' Assignment (SwitchTarget blocks ctx) varctx
targets)
      Return Reg ctx ret
r -> Reg ctx' ret -> TermStmt blocks ret ctx'
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
Reg ctx ret -> TermStmt blocks ret ctx
Return (Reg ctx ret -> Reg ctx' ret
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ApplyEmbedding' f =>
f ctx v -> f ctx' v
apC' Reg ctx ret
r)
      TailCall Reg ctx (FunctionHandleType args ret)
hdl CtxRepr args
tys Assignment (Reg ctx) args
args -> Reg ctx' (FunctionHandleType args ret)
-> CtxRepr args
-> Assignment (Reg ctx') args
-> TermStmt blocks ret ctx'
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (ret :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Reg ctx (FunctionHandleType ctx' ret)
-> CtxRepr ctx'
-> Assignment (Reg ctx) ctx'
-> TermStmt blocks ret ctx
TailCall (Reg ctx (FunctionHandleType args ret)
-> Reg ctx' (FunctionHandleType args ret)
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ApplyEmbedding' f =>
f ctx v -> f ctx' v
apC' Reg ctx (FunctionHandleType args ret)
hdl) CtxRepr args
tys ((forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Reg ctx) x -> Assignment (Reg ctx') x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC Reg ctx x -> Reg ctx' x
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ApplyEmbedding' f =>
f ctx v -> f ctx' v
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
apC' Assignment (Reg ctx) args
args)
      ErrorStmt Reg ctx (StringType Unicode)
r -> Reg ctx' (StringType Unicode) -> TermStmt blocks ret ctx'
forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
Reg ctx (StringType Unicode) -> TermStmt blocks ret ctx
ErrorStmt (Reg ctx (StringType Unicode) -> Reg ctx' (StringType Unicode)
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ApplyEmbedding' f =>
f ctx v -> f ctx' v
apC' Reg ctx (StringType Unicode)
r)
    where
      apC' :: forall f v. ApplyEmbedding' f => f ctx v -> f ctx' v
      apC' :: forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ApplyEmbedding' f =>
f ctx v -> f ctx' v
apC' = CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ApplyEmbedding' f =>
CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: k').
CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe

      apC :: forall f. ApplyEmbedding  f => f ctx -> f ctx'
      apC :: forall (f :: Ctx CrucibleType -> Type).
ApplyEmbedding f =>
f ctx -> f ctx'
apC  = CtxEmbedding ctx ctx' -> f ctx -> f ctx'
forall k (f :: Ctx k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k).
ApplyEmbedding f =>
CtxEmbedding ctx ctx' -> f ctx -> f ctx'
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
CtxEmbedding ctx ctx' -> f ctx -> f ctx'
applyEmbedding  CtxEmbedding ctx ctx'
ctxe

instance ExtendContext (TermStmt blocks ret) where
  extendContext :: forall ctx ctx'.
                    Diff ctx ctx'
                    -> TermStmt blocks ret ctx
                    -> TermStmt blocks ret ctx'
  extendContext :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
Diff ctx ctx'
-> TermStmt blocks ret ctx -> TermStmt blocks ret ctx'
extendContext Diff ctx ctx'
diff TermStmt blocks ret ctx
term =
    case TermStmt blocks ret ctx
term of
      Jump JumpTarget blocks ctx
jt -> JumpTarget blocks ctx' -> TermStmt blocks ret ctx'
forall (blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType)
       (ret :: CrucibleType).
JumpTarget blocks ctx -> TermStmt blocks ret ctx
Jump (JumpTarget blocks ctx -> JumpTarget blocks ctx'
forall (f :: Ctx CrucibleType -> Type).
ExtendContext f =>
f ctx -> f ctx'
extC JumpTarget blocks ctx
jt)
      Br Reg ctx BoolType
b JumpTarget blocks ctx
jtl JumpTarget blocks ctx
jtr -> Reg ctx' BoolType
-> JumpTarget blocks ctx'
-> JumpTarget blocks ctx'
-> TermStmt blocks ret ctx'
forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
Reg ctx BoolType
-> JumpTarget blocks ctx
-> JumpTarget blocks ctx
-> TermStmt blocks ret ctx
Br (Reg ctx BoolType -> Reg ctx' BoolType
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ExtendContext' f =>
f ctx v -> f ctx' v
extC' Reg ctx BoolType
b) (JumpTarget blocks ctx -> JumpTarget blocks ctx'
forall (f :: Ctx CrucibleType -> Type).
ExtendContext f =>
f ctx -> f ctx'
extC JumpTarget blocks ctx
jtl) (JumpTarget blocks ctx -> JumpTarget blocks ctx'
forall (f :: Ctx CrucibleType -> Type).
ExtendContext f =>
f ctx -> f ctx'
extC JumpTarget blocks ctx
jtr)
      MaybeBranch TypeRepr tp
tp Reg ctx (MaybeType tp)
b SwitchTarget blocks ctx tp
swt JumpTarget blocks ctx
jt    -> TypeRepr tp
-> Reg ctx' (MaybeType tp)
-> SwitchTarget blocks ctx' tp
-> JumpTarget blocks ctx'
-> TermStmt blocks ret ctx'
forall (ctx' :: CrucibleType) (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (rtp :: CrucibleType).
TypeRepr ctx'
-> Reg ctx (MaybeType ctx')
-> SwitchTarget blocks ctx ctx'
-> JumpTarget blocks ctx
-> TermStmt blocks rtp ctx
MaybeBranch TypeRepr tp
tp (Reg ctx (MaybeType tp) -> Reg ctx' (MaybeType tp)
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ExtendContext' f =>
f ctx v -> f ctx' v
extC' Reg ctx (MaybeType tp)
b) (SwitchTarget blocks ctx tp -> SwitchTarget blocks ctx' tp
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ExtendContext' f =>
f ctx v -> f ctx' v
extC' SwitchTarget blocks ctx tp
swt) (JumpTarget blocks ctx -> JumpTarget blocks ctx'
forall (f :: Ctx CrucibleType -> Type).
ExtendContext f =>
f ctx -> f ctx'
extC JumpTarget blocks ctx
jt)
      VariantElim CtxRepr varctx
repr Reg ctx (VariantType varctx)
r Assignment (SwitchTarget blocks ctx) varctx
targets -> CtxRepr varctx
-> Reg ctx' (VariantType varctx)
-> Assignment (SwitchTarget blocks ctx') varctx
-> TermStmt blocks ret ctx'
forall (ctx' :: Ctx CrucibleType) (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
CtxRepr ctx'
-> Reg ctx (VariantType ctx')
-> Assignment (SwitchTarget blocks ctx) ctx'
-> TermStmt blocks ret ctx
VariantElim CtxRepr varctx
repr (Reg ctx (VariantType varctx) -> Reg ctx' (VariantType varctx)
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ExtendContext' f =>
f ctx v -> f ctx' v
extC' Reg ctx (VariantType varctx)
r) ((forall (x :: CrucibleType).
 SwitchTarget blocks ctx x -> SwitchTarget blocks ctx' x)
-> forall (x :: Ctx CrucibleType).
   Assignment (SwitchTarget blocks ctx) x
   -> Assignment (SwitchTarget blocks ctx') x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC SwitchTarget blocks ctx x -> SwitchTarget blocks ctx' x
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ExtendContext' f =>
f ctx v -> f ctx' v
forall (x :: CrucibleType).
SwitchTarget blocks ctx x -> SwitchTarget blocks ctx' x
extC' Assignment (SwitchTarget blocks ctx) varctx
targets)
      Return Reg ctx ret
r -> Reg ctx' ret -> TermStmt blocks ret ctx'
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
Reg ctx ret -> TermStmt blocks ret ctx
Return (Reg ctx ret -> Reg ctx' ret
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ExtendContext' f =>
f ctx v -> f ctx' v
extC' Reg ctx ret
r)
      TailCall Reg ctx (FunctionHandleType args ret)
hdl CtxRepr args
tys Assignment (Reg ctx) args
args -> Reg ctx' (FunctionHandleType args ret)
-> CtxRepr args
-> Assignment (Reg ctx') args
-> TermStmt blocks ret ctx'
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (ret :: CrucibleType) (blocks :: Ctx (Ctx CrucibleType)).
Reg ctx (FunctionHandleType ctx' ret)
-> CtxRepr ctx'
-> Assignment (Reg ctx) ctx'
-> TermStmt blocks ret ctx
TailCall (Reg ctx (FunctionHandleType args ret)
-> Reg ctx' (FunctionHandleType args ret)
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ExtendContext' f =>
f ctx v -> f ctx' v
extC' Reg ctx (FunctionHandleType args ret)
hdl) CtxRepr args
tys ((forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x)
-> forall (x :: Ctx CrucibleType).
   Assignment (Reg ctx) x -> Assignment (Reg ctx') x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: Ctx CrucibleType). Assignment f x -> Assignment g x
fmapFC Reg ctx x -> Reg ctx' x
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ExtendContext' f =>
f ctx v -> f ctx' v
forall (x :: CrucibleType). Reg ctx x -> Reg ctx' x
extC' Assignment (Reg ctx) args
args)
      ErrorStmt Reg ctx (StringType Unicode)
r -> Reg ctx' (StringType Unicode) -> TermStmt blocks ret ctx'
forall (ctx :: Ctx CrucibleType) (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType).
Reg ctx (StringType Unicode) -> TermStmt blocks ret ctx
ErrorStmt (Reg ctx (StringType Unicode) -> Reg ctx' (StringType Unicode)
forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ExtendContext' f =>
f ctx v -> f ctx' v
extC' Reg ctx (StringType Unicode)
r)
    where
      extC' :: forall f v. ExtendContext' f => f ctx v -> f ctx' v
      extC' :: forall {k'} (f :: Ctx CrucibleType -> k' -> Type) (v :: k').
ExtendContext' f =>
f ctx v -> f ctx' v
extC' = Diff ctx ctx' -> f ctx v -> f ctx' v
forall k k' (f :: Ctx k -> k' -> Type) (ctx :: Ctx k)
       (ctx' :: Ctx k) (v :: k').
ExtendContext' f =>
Diff ctx ctx' -> f ctx v -> f ctx' v
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (v :: k').
Diff ctx ctx' -> f ctx v -> f ctx' v
extendContext' Diff ctx ctx'
diff

      extC :: forall f. ExtendContext  f => f ctx -> f ctx'
      extC :: forall (f :: Ctx CrucibleType -> Type).
ExtendContext f =>
f ctx -> f ctx'
extC  = Diff ctx ctx' -> f ctx -> f ctx'
forall k (f :: Ctx k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k).
ExtendContext f =>
Diff ctx ctx' -> f ctx -> f ctx'
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
Diff ctx ctx' -> f ctx -> f ctx'
extendContext  Diff ctx ctx'
diff


------------------------------------------------------------------------
-- StmtSeq

-- | A sequence of straight-line program statements that end with
--   a terminating statement (return, jump, etc).
data StmtSeq ext blocks (ret :: CrucibleType) ctx where
  ConsStmt :: !ProgramLoc
           -> !(Stmt ext ctx ctx')
           -> !(StmtSeq ext blocks ret ctx')
           -> StmtSeq ext blocks ret ctx
  TermStmt :: !ProgramLoc
           -> !(TermStmt blocks ret ctx)
           -> (StmtSeq ext blocks ret ctx)

-- | Return the location of a statement.
firstStmtLoc :: StmtSeq ext b r ctx -> ProgramLoc
firstStmtLoc :: forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
       (ctx :: Ctx CrucibleType).
StmtSeq ext b r ctx -> ProgramLoc
firstStmtLoc (ConsStmt ProgramLoc
pl Stmt ext ctx ctx'
_ StmtSeq ext b r ctx'
_) = ProgramLoc
pl
firstStmtLoc (TermStmt ProgramLoc
pl TermStmt b r ctx
_) = ProgramLoc
pl

-- | A lens-like operation that gives one access to program location and term statement,
-- and allows the terminal statement to be replaced with an arbitrary sequence of
-- statements.
stmtSeqTermStmt :: Functor f
                => (forall ctx
                    . (ProgramLoc, TermStmt b ret ctx)
                    -> f (StmtSeq ext b' ret ctx))
                -> StmtSeq ext b ret args
                -> f (StmtSeq ext b' ret args)
stmtSeqTermStmt :: forall (f :: Type -> Type) (b :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) ext (b' :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
Functor f =>
(forall (ctx :: Ctx CrucibleType).
 (ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx))
-> StmtSeq ext b ret args -> f (StmtSeq ext b' ret args)
stmtSeqTermStmt forall (ctx :: Ctx CrucibleType).
(ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx)
f (ConsStmt ProgramLoc
l Stmt ext args ctx'
s StmtSeq ext b ret ctx'
t) = ProgramLoc
-> Stmt ext args ctx'
-> StmtSeq ext b' ret ctx'
-> StmtSeq ext b' ret args
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
ConsStmt ProgramLoc
l Stmt ext args ctx'
s (StmtSeq ext b' ret ctx' -> StmtSeq ext b' ret args)
-> f (StmtSeq ext b' ret ctx') -> f (StmtSeq ext b' ret args)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (ctx :: Ctx CrucibleType).
 (ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx))
-> StmtSeq ext b ret ctx' -> f (StmtSeq ext b' ret ctx')
forall (f :: Type -> Type) (b :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) ext (b' :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
Functor f =>
(forall (ctx :: Ctx CrucibleType).
 (ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx))
-> StmtSeq ext b ret args -> f (StmtSeq ext b' ret args)
stmtSeqTermStmt (ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx)
forall (ctx :: Ctx CrucibleType).
(ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx)
f StmtSeq ext b ret ctx'
t
stmtSeqTermStmt forall (ctx :: Ctx CrucibleType).
(ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx)
f (TermStmt ProgramLoc
p TermStmt b ret args
t) = (ProgramLoc, TermStmt b ret args) -> f (StmtSeq ext b' ret args)
forall (ctx :: Ctx CrucibleType).
(ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx)
f (ProgramLoc
p, TermStmt b ret args
t)

ppReg :: Size ctx -> Doc ann
ppReg :: forall {k} (ctx :: Ctx k) ann. Size ctx -> Doc ann
ppReg Size ctx
h = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"$" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Size ctx -> Int
forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
h)

nextStmtHeight :: Size ctx -> Stmt ext ctx ctx' -> Size ctx'
nextStmtHeight :: forall (ctx :: Ctx CrucibleType) ext (ctx' :: Ctx CrucibleType).
Size ctx -> Stmt ext ctx ctx' -> Size ctx'
nextStmtHeight Size ctx
h Stmt ext ctx ctx'
s =
  case Stmt ext ctx ctx'
s of
    SetReg{} -> Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
h
    ExtendAssign{} -> Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
h
    CallHandle{} -> Size ctx -> Size (ctx '::> ret)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
h
    Print{} -> Size ctx
Size ctx'
h
    ReadGlobal{} -> Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
h
    WriteGlobal{} -> Size ctx
Size ctx'
h
    FreshConstant{} -> Size ctx -> Size (ctx '::> BaseToType bt)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
Ctx.incSize Size ctx
h
    FreshFloat{} -> Size ctx -> Size (ctx '::> FloatType fi)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
Ctx.incSize Size ctx
h
    FreshNat{} -> Size ctx -> Size (ctx '::> NatType)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
Ctx.incSize Size ctx
h
    NewRefCell{} -> Size ctx -> Size (ctx '::> ReferenceType tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
Ctx.incSize Size ctx
h
    NewEmptyRefCell{} ->Size ctx -> Size (ctx '::> ReferenceType tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
Ctx.incSize Size ctx
h
    ReadRefCell{} -> Size ctx -> Size (ctx '::> tp)
forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
Ctx.incSize Size ctx
h
    WriteRefCell{} -> Size ctx
Size ctx'
h
    DropRefCell{}  -> Size ctx
Size ctx'
h
    Assert{} -> Size ctx
Size ctx'
h
    Assume{} -> Size ctx
Size ctx'
h

ppStmt :: PrettyExt ext => Size ctx -> Stmt ext ctx ctx' -> Doc ann
ppStmt :: forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       ann.
PrettyExt ext =>
Size ctx -> Stmt ext ctx ctx' -> Doc ann
ppStmt Size ctx
r Stmt ext ctx ctx'
s =
  case Stmt ext ctx ctx'
s of
    SetReg TypeRepr tp
_ Expr ext ctx tp
e -> Size ctx -> Doc ann
forall {k} (ctx :: Ctx k) ann. Size ctx -> Doc ann
ppReg Size ctx
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Expr ext ctx tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Expr ext ctx tp -> Doc ann
pretty Expr ext ctx tp
e
    ExtendAssign StmtExtension ext (Reg ctx) tp
s' -> Size ctx -> Doc ann
forall {k} (ctx :: Ctx k) ann. Size ctx -> Doc ann
ppReg Size ctx
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (forall (x :: CrucibleType). Reg ctx x -> Doc ann)
-> forall (x :: CrucibleType).
   StmtExtension ext (Reg ctx) 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 Reg ctx x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx x -> Doc ann
forall (x :: CrucibleType). Reg ctx x -> Doc ann
pretty StmtExtension ext (Reg ctx) tp
s'
    CallHandle TypeRepr ret
_ Reg ctx (FunctionHandleType args ret)
h CtxRepr args
_ Assignment (Reg ctx) args
args ->
      Size ctx -> Doc ann
forall {k} (ctx :: Ctx k) ann. Size ctx -> Doc ann
ppReg Size ctx
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"= call"
              Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Reg ctx (FunctionHandleType args ret) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (FunctionHandleType args ret) -> Doc ann
pretty Reg ctx (FunctionHandleType args ret)
h 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 (f :: Type -> Type) ann.
Foldable f =>
f (Doc ann) -> Doc ann
commas (Assignment (Reg ctx) args -> [Doc ann]
forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType) ann.
Assignment (Reg ctx) args -> [Doc ann]
ppAssignment Assignment (Reg ctx) args
args))
               Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
";"
    Print Reg ctx (StringType Unicode)
msg -> String -> [Doc ann] -> Doc ann
forall ann. String -> [Doc ann] -> Doc ann
ppFn String
"print" [ Reg ctx (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (StringType Unicode) -> Doc ann
pretty Reg ctx (StringType Unicode)
msg ]
    ReadGlobal GlobalVar tp
v -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"read" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Size ctx -> Doc ann
forall {k} (ctx :: Ctx k) ann. Size ctx -> Doc ann
ppReg Size ctx
r 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
v
    WriteGlobal GlobalVar tp
v Reg ctx tp
e -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"write" 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
v Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Reg ctx tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx tp -> Doc ann
pretty Reg ctx tp
e
    -- TODO: replace viaShow once we have instance Pretty SolverSymbol
    FreshConstant BaseTypeRepr bt
bt Maybe SolverSymbol
nm -> Size ctx -> Doc ann
forall {k} (ctx :: Ctx k) ann. Size ctx -> Doc ann
ppReg Size ctx
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"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 -> Size ctx -> Doc ann
forall {k} (ctx :: Ctx k) ann. Size ctx -> Doc ann
ppReg Size ctx
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"fresh-float" 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 -> Size ctx -> Doc ann
forall {k} (ctx :: Ctx k) ann. Size ctx -> Doc ann
ppReg Size ctx
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"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
    NewRefCell TypeRepr tp
_ Reg ctx tp
e -> Size ctx -> Doc ann
forall {k} (ctx :: Ctx k) ann. Size ctx -> Doc ann
ppReg Size ctx
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> [Doc ann] -> Doc ann
forall ann. String -> [Doc ann] -> Doc ann
ppFn String
"newref" [ Reg ctx tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx tp -> Doc ann
pretty Reg ctx tp
e ]
    NewEmptyRefCell TypeRepr tp
tp -> Size ctx -> Doc ann
forall {k} (ctx :: Ctx k) ann. Size ctx -> Doc ann
ppReg Size ctx
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> [Doc ann] -> Doc ann
forall ann. String -> [Doc ann] -> Doc ann
ppFn String
"emptyref" [ TypeRepr tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TypeRepr tp -> Doc ann
pretty TypeRepr tp
tp ]
    ReadRefCell Reg ctx (ReferenceType tp)
e -> Size ctx -> Doc ann
forall {k} (ctx :: Ctx k) ann. Size ctx -> Doc ann
ppReg Size ctx
r Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"= !" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Reg ctx (ReferenceType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (ReferenceType tp) -> Doc ann
pretty Reg ctx (ReferenceType tp)
e
    WriteRefCell Reg ctx (ReferenceType tp)
r1 Reg ctx tp
r2 -> Reg ctx (ReferenceType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (ReferenceType tp) -> Doc ann
pretty Reg ctx (ReferenceType tp)
r1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
":=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Reg ctx tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx tp -> Doc ann
pretty Reg ctx tp
r2
    DropRefCell Reg ctx (ReferenceType tp)
r1 -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"drop" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Reg ctx (ReferenceType tp) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (ReferenceType tp) -> Doc ann
pretty Reg ctx (ReferenceType tp)
r1
    Assert Reg ctx BoolType
c Reg ctx (StringType Unicode)
e -> String -> [Doc ann] -> Doc ann
forall ann. String -> [Doc ann] -> Doc ann
ppFn String
"assert" [ Reg ctx BoolType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx BoolType -> Doc ann
pretty Reg ctx BoolType
c, Reg ctx (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (StringType Unicode) -> Doc ann
pretty Reg ctx (StringType Unicode)
e ]
    Assume Reg ctx BoolType
c Reg ctx (StringType Unicode)
e -> String -> [Doc ann] -> Doc ann
forall ann. String -> [Doc ann] -> Doc ann
ppFn String
"assume" [ Reg ctx BoolType -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx BoolType -> Doc ann
pretty Reg ctx BoolType
c, Reg ctx (StringType Unicode) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (StringType Unicode) -> Doc ann
pretty Reg ctx (StringType Unicode)
e ]

prefixLineNum :: Bool -> ProgramLoc -> Doc ann -> Doc ann
prefixLineNum :: forall ann. Bool -> ProgramLoc -> Doc ann -> Doc ann
prefixLineNum Bool
True ProgramLoc
pl Doc ann
d = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"%" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Position -> Doc ann
forall ann. Position -> Doc ann
ppNoFileName (ProgramLoc -> Position
plSourceLoc ProgramLoc
pl), Doc ann
d]
prefixLineNum Bool
False ProgramLoc
_ Doc ann
d = Doc ann
d

ppStmtSeq :: PrettyExt ext => Bool -> Size ctx -> StmtSeq ext blocks ret ctx -> Doc ann
ppStmtSeq :: forall ext (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> Size ctx -> StmtSeq ext blocks ret ctx -> Doc ann
ppStmtSeq Bool
ppLineNum Size ctx
h (ConsStmt ProgramLoc
pl Stmt ext ctx ctx'
s StmtSeq ext blocks ret ctx'
r) =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat
  [ Bool -> ProgramLoc -> Doc ann -> Doc ann
forall ann. Bool -> ProgramLoc -> Doc ann -> Doc ann
prefixLineNum Bool
ppLineNum ProgramLoc
pl (Size ctx -> Stmt ext ctx ctx' -> Doc ann
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       ann.
PrettyExt ext =>
Size ctx -> Stmt ext ctx ctx' -> Doc ann
ppStmt Size ctx
h Stmt ext ctx ctx'
s)
  , Bool -> Size ctx' -> StmtSeq ext blocks ret ctx' -> Doc ann
forall ext (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> Size ctx -> StmtSeq ext blocks ret ctx -> Doc ann
ppStmtSeq Bool
ppLineNum (Size ctx -> Stmt ext ctx ctx' -> Size ctx'
forall (ctx :: Ctx CrucibleType) ext (ctx' :: Ctx CrucibleType).
Size ctx -> Stmt ext ctx ctx' -> Size ctx'
nextStmtHeight Size ctx
h Stmt ext ctx ctx'
s) StmtSeq ext blocks ret ctx'
r
  ]
ppStmtSeq Bool
ppLineNum Size ctx
_ (TermStmt ProgramLoc
pl TermStmt blocks ret ctx
s) =
  Bool -> ProgramLoc -> Doc ann -> Doc ann
forall ann. Bool -> ProgramLoc -> Doc ann -> Doc ann
prefixLineNum Bool
ppLineNum ProgramLoc
pl (TermStmt blocks ret ctx -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TermStmt blocks ret ctx -> Doc ann
pretty TermStmt blocks ret ctx
s)


#ifndef UNSAFE_OPS
extendStmtSeq :: Diff blocks' blocks -> StmtSeq ext blocks' ret ctx -> StmtSeq ext blocks ret ctx
extendStmtSeq diff (ConsStmt p s l) = ConsStmt p s (extendStmtSeq diff l)
extendStmtSeq diff (TermStmt p s) = TermStmt p (extendTermStmt diff s)
#endif


instance TraverseExt ext => ApplyEmbedding (StmtSeq ext blocks ret) where
  applyEmbedding :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'
-> StmtSeq ext blocks ret ctx -> StmtSeq ext blocks ret ctx'
applyEmbedding CtxEmbedding ctx ctx'
ctxe (ConsStmt ProgramLoc
loc Stmt ext ctx ctx'
stmt StmtSeq ext blocks ret ctx'
rest) =
    case CtxEmbedding ctx ctx'
-> Stmt ext ctx ctx' -> Pair (Stmt ext ctx') (CtxEmbedding ctx')
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (sctx :: Ctx CrucibleType).
TraverseExt ext =>
CtxEmbedding ctx ctx'
-> Stmt ext ctx sctx -> Pair (Stmt ext ctx') (CtxEmbedding sctx)
applyEmbeddingStmt CtxEmbedding ctx ctx'
ctxe Stmt ext ctx ctx'
stmt of
      Pair Stmt ext ctx' tp
stmt' CtxEmbedding ctx' tp
ctxe' -> ProgramLoc
-> Stmt ext ctx' tp
-> StmtSeq ext blocks ret tp
-> StmtSeq ext blocks ret ctx'
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
ProgramLoc
-> Stmt ext ctx ctx'
-> StmtSeq ext blocks ret ctx'
-> StmtSeq ext blocks ret ctx
ConsStmt ProgramLoc
loc Stmt ext ctx' tp
stmt' (CtxEmbedding ctx' tp
-> StmtSeq ext blocks ret ctx' -> StmtSeq ext blocks ret tp
forall k (f :: Ctx k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k).
ApplyEmbedding f =>
CtxEmbedding ctx ctx' -> f ctx -> f ctx'
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'
-> StmtSeq ext blocks ret ctx -> StmtSeq ext blocks ret ctx'
applyEmbedding CtxEmbedding ctx' tp
ctxe' StmtSeq ext blocks ret ctx'
rest)
  applyEmbedding CtxEmbedding ctx ctx'
ctxe (TermStmt ProgramLoc
loc TermStmt blocks ret ctx
term) =
    ProgramLoc
-> TermStmt blocks ret ctx' -> StmtSeq ext blocks ret ctx'
forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType) ext.
ProgramLoc -> TermStmt blocks ret ctx -> StmtSeq ext blocks ret ctx
TermStmt ProgramLoc
loc (CtxEmbedding ctx ctx'
-> TermStmt blocks ret ctx -> TermStmt blocks ret ctx'
forall k (f :: Ctx k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k).
ApplyEmbedding f =>
CtxEmbedding ctx ctx' -> f ctx -> f ctx'
forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
CtxEmbedding ctx ctx'
-> TermStmt blocks ret ctx -> TermStmt blocks ret ctx'
applyEmbedding CtxEmbedding ctx ctx'
ctxe TermStmt blocks ret ctx
term)



------------------------------------------------------------------------
-- CFGPostdom

-- | Postdominator information about a CFG.  The assignment maps each block
--   to the postdominators of the given block.  The postdominators are ordered
--   with nearest postdominator first.
type CFGPostdom blocks = Assignment (Const [Some (BlockID blocks)]) blocks

emptyCFGPostdomInfo :: Size blocks -> CFGPostdom blocks
emptyCFGPostdomInfo :: forall (blocks :: Ctx (Ctx CrucibleType)).
Size blocks -> CFGPostdom blocks
emptyCFGPostdomInfo Size blocks
sz = Size blocks
-> (forall (tp :: Ctx CrucibleType).
    Const [Some (BlockID blocks)] tp)
-> Assignment (Const [Some (BlockID blocks)]) blocks
forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx -> (forall (tp :: k). f tp) -> Assignment f ctx
Ctx.replicate Size blocks
sz ([Some (BlockID blocks)] -> Const [Some (BlockID blocks)] tp
forall {k} a (b :: k). a -> Const a b
Const [])


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

-- | A basic block within a function.
data Block ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ctx
   = Block { forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID        :: !(BlockID blocks ctx)
             -- ^ The unique identifier of this block
           , forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs    :: !(CtxRepr ctx)
             -- ^ The expected types of the formal arguments to this block
           , forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> StmtSeq ext blocks ret ctx
_blockStmts    :: !(StmtSeq ext blocks ret ctx)
             -- ^ The sequence of statements in this block
           }

blockStmts :: Lens' (Block ext b r c) (StmtSeq ext b r c)
blockStmts :: forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
       (c :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(StmtSeq ext b r c -> f (StmtSeq ext b r c))
-> Block ext b r c -> f (Block ext b r c)
blockStmts = (Block ext b r c -> StmtSeq ext b r c)
-> (Block ext b r c -> StmtSeq ext b r c -> Block ext b r c)
-> Lens
     (Block ext b r c)
     (Block ext b r c)
     (StmtSeq ext b r c)
     (StmtSeq ext b r c)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens Block ext b r c -> StmtSeq ext b r c
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> StmtSeq ext blocks ret ctx
_blockStmts (\Block ext b r c
b StmtSeq ext b r c
s -> Block ext b r c
b { _blockStmts = s })

-- | Return location of start of block.
blockLoc :: Block ext blocks ret ctx -> ProgramLoc
blockLoc :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> ProgramLoc
blockLoc Block ext blocks ret ctx
b = StmtSeq ext blocks ret ctx -> ProgramLoc
forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
       (ctx :: Ctx CrucibleType).
StmtSeq ext b r ctx -> ProgramLoc
firstStmtLoc (Block ext blocks ret ctx
b Block ext blocks ret ctx
-> Getting
     (StmtSeq ext blocks ret ctx)
     (Block ext blocks ret ctx)
     (StmtSeq ext blocks ret ctx)
-> StmtSeq ext blocks ret ctx
forall s a. s -> Getting a s a -> a
^. Getting
  (StmtSeq ext blocks ret ctx)
  (Block ext blocks ret ctx)
  (StmtSeq ext blocks ret ctx)
forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
       (c :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(StmtSeq ext b r c -> f (StmtSeq ext b r c))
-> Block ext b r c -> f (Block ext b r c)
blockStmts)

-- | Get the terminal statement of a basic block.  This is implemented
-- in a CPS style due to the block context.
withBlockTermStmt :: Block ext blocks ret args
                  -> (forall ctx . ProgramLoc -> TermStmt blocks ret ctx -> r)
                  -> r
withBlockTermStmt :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (args :: Ctx CrucibleType) r.
Block ext blocks ret args
-> (forall (ctx :: Ctx CrucibleType).
    ProgramLoc -> TermStmt blocks ret ctx -> r)
-> r
withBlockTermStmt Block ext blocks ret args
b forall (ctx :: Ctx CrucibleType).
ProgramLoc -> TermStmt blocks ret ctx -> r
f = Const r (StmtSeq ext Any ret args) -> r
forall {k} a (b :: k). Const a b -> a
getConst ((forall (ctx :: Ctx CrucibleType).
 (ProgramLoc, TermStmt blocks ret ctx)
 -> Const r (StmtSeq ext Any ret ctx))
-> StmtSeq ext blocks ret args
-> Const r (StmtSeq ext Any ret args)
forall (f :: Type -> Type) (b :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) ext (b' :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType).
Functor f =>
(forall (ctx :: Ctx CrucibleType).
 (ProgramLoc, TermStmt b ret ctx) -> f (StmtSeq ext b' ret ctx))
-> StmtSeq ext b ret args -> f (StmtSeq ext b' ret args)
stmtSeqTermStmt (r -> Const r (StmtSeq ext Any ret ctx)
forall {k} a (b :: k). a -> Const a b
Const (r -> Const r (StmtSeq ext Any ret ctx))
-> ((ProgramLoc, TermStmt blocks ret ctx) -> r)
-> (ProgramLoc, TermStmt blocks ret ctx)
-> Const r (StmtSeq ext Any ret ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProgramLoc -> TermStmt blocks ret ctx -> r)
-> (ProgramLoc, TermStmt blocks ret ctx) -> r
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ProgramLoc -> TermStmt blocks ret ctx -> r
forall (ctx :: Ctx CrucibleType).
ProgramLoc -> TermStmt blocks ret ctx -> r
f) (Block ext blocks ret args
b Block ext blocks ret args
-> Getting
     (StmtSeq ext blocks ret args)
     (Block ext blocks ret args)
     (StmtSeq ext blocks ret args)
-> StmtSeq ext blocks ret args
forall s a. s -> Getting a s a -> a
^. Getting
  (StmtSeq ext blocks ret args)
  (Block ext blocks ret args)
  (StmtSeq ext blocks ret args)
forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
       (c :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(StmtSeq ext b r c -> f (StmtSeq ext b r c))
-> Block ext b r c -> f (Block ext b r c)
blockStmts))

nextBlocks :: Block ext b r a -> [Some (BlockID b)]
nextBlocks :: forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
       (a :: Ctx CrucibleType).
Block ext b r a -> [Some (BlockID b)]
nextBlocks Block ext b r a
b =
  Block ext b r a
-> (forall (ctx :: Ctx CrucibleType).
    ProgramLoc -> TermStmt b r ctx -> [Some (BlockID b)])
-> [Some (BlockID b)]
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (args :: Ctx CrucibleType) r.
Block ext blocks ret args
-> (forall (ctx :: Ctx CrucibleType).
    ProgramLoc -> TermStmt blocks ret ctx -> r)
-> r
withBlockTermStmt Block ext b r a
b (\ProgramLoc
_ TermStmt b r ctx
s -> [Some (BlockID b)]
-> Maybe [Some (BlockID b)] -> [Some (BlockID b)]
forall a. a -> Maybe a -> a
fromMaybe [] (TermStmt b r ctx -> Maybe [Some (BlockID b)]
forall (b :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
TermStmt b ret ctx -> Maybe [Some (BlockID b)]
termStmtNextBlocks TermStmt b r ctx
s))


blockInputCount :: Block ext blocks ret ctx -> Size ctx
blockInputCount :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> Size ctx
blockInputCount Block ext blocks ret ctx
b = Assignment TypeRepr ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size (Block ext blocks ret ctx -> Assignment TypeRepr ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs Block ext blocks ret ctx
b)

ppBlock :: PrettyExt ext
        => Bool
           -- ^ Print line numbers.
        -> Bool
           -- ^ Print block args. Note that you can infer the number
           -- of block args from the first SSA temp register assigned
           -- to in the block: if the block has @n@ args, then the
           -- first register it assigns to will be @$n@.
        -> Maybe (CFGPostdom blocks)
           -- ^ Optionally print postdom info.
        -> Block ext blocks ret ctx
           -- ^ Block to print.
        -> Doc ann
ppBlock :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType) ann.
PrettyExt ext =>
Bool
-> Bool
-> Maybe (CFGPostdom blocks)
-> Block ext blocks ret ctx
-> Doc ann
ppBlock Bool
ppLineNumbers Bool
ppBlockArgs Maybe (CFGPostdom blocks)
mPda Block ext blocks ret ctx
b = do
  let stmts :: Doc ann
stmts = Bool -> Size ctx -> StmtSeq ext blocks ret ctx -> Doc ann
forall ext (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> Size ctx -> StmtSeq ext blocks ret ctx -> Doc ann
ppStmtSeq Bool
ppLineNumbers (Block ext blocks ret ctx -> Size ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> Size ctx
blockInputCount Block ext blocks ret ctx
b) (Block ext blocks ret ctx
b Block ext blocks ret ctx
-> Getting
     (StmtSeq ext blocks ret ctx)
     (Block ext blocks ret ctx)
     (StmtSeq ext blocks ret ctx)
-> StmtSeq ext blocks ret ctx
forall s a. s -> Getting a s a -> a
^. Getting
  (StmtSeq ext blocks ret ctx)
  (Block ext blocks ret ctx)
  (StmtSeq ext blocks ret ctx)
forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
       (c :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(StmtSeq ext b r c -> f (StmtSeq ext b r c))
-> Block ext b r c -> f (Block ext b r c)
blockStmts)
  let mPostdom :: Maybe (Doc ann)
mPostdom = ((CFGPostdom blocks -> Doc ann)
 -> Maybe (CFGPostdom blocks) -> Maybe (Doc ann))
-> Maybe (CFGPostdom blocks)
-> (CFGPostdom blocks -> Doc ann)
-> Maybe (Doc ann)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (CFGPostdom blocks -> Doc ann)
-> Maybe (CFGPostdom blocks) -> Maybe (Doc ann)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe (CFGPostdom blocks)
mPda ((CFGPostdom blocks -> Doc ann) -> Maybe (Doc ann))
-> (CFGPostdom blocks -> Doc ann) -> Maybe (Doc ann)
forall a b. (a -> b) -> a -> b
$ \ CFGPostdom blocks
pda ->
        let Const [Some (BlockID blocks)]
pd = CFGPostdom blocks
pda CFGPostdom blocks
-> Index blocks ctx -> Const [Some (BlockID blocks)] ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! BlockID blocks ctx -> Index blocks ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
BlockID blocks tp -> Index blocks tp
blockIDIndex (Block ext blocks ret ctx -> BlockID blocks ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret ctx
b)
        in if [Some (BlockID blocks)] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
Prelude.null [Some (BlockID blocks)]
pd
           then String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"% no postdom"
           else String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"% postdom" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ((forall (tp :: Ctx CrucibleType). BlockID blocks tp -> Doc ann)
-> Some (BlockID blocks) -> Doc ann
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome BlockID blocks tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BlockID blocks tp -> Doc ann
forall (tp :: Ctx CrucibleType). BlockID blocks tp -> Doc ann
pretty (Some (BlockID blocks) -> Doc ann)
-> [Some (BlockID blocks)] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Some (BlockID blocks)]
pd)
  let numArgs :: Int
numArgs = Assignment TypeRepr ctx -> Int
forall {k} {l} (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (x :: l).
FoldableFC t =>
t f x -> Int
lengthFC (Block ext blocks ret ctx -> Assignment TypeRepr ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs Block ext blocks ret ctx
b)
  let argList :: [Doc ann]
argList = [ 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
<> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
n | Int
n <- [Int
0 .. Int
numArgsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]
  let args :: Doc ann
args = Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep Doc ann
forall ann. Doc ann
lparen Doc ann
forall ann. Doc ann
rparen Doc ann
forall ann. Doc ann
comma [Doc ann]
argList
  let block :: Doc ann
block = BlockID blocks ctx -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. BlockID blocks ctx -> Doc ann
pretty (Block ext blocks ret ctx -> BlockID blocks ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> BlockID blocks ctx
blockID Block ext blocks ret ctx
b) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<>
              if Bool
ppBlockArgs then Doc ann
args else Doc ann
forall a. Monoid a => a
mempty
  let body :: Doc ann
body = case Maybe (Doc ann)
mPostdom of
        Maybe (Doc ann)
Nothing -> Doc ann
stmts
        Just Doc ann
postdom -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [Doc ann
stmts, Doc ann
postdom]
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [Doc ann
block, Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 Doc ann
body]

instance PrettyExt ext => Show (Block ext blocks ret args) where
  show :: Block ext blocks ret args -> String
show Block ext blocks ret args
blk = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Bool
-> Bool
-> Maybe (CFGPostdom blocks)
-> Block ext blocks ret args
-> Doc Any
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType) ann.
PrettyExt ext =>
Bool
-> Bool
-> Maybe (CFGPostdom blocks)
-> Block ext blocks ret ctx
-> Doc ann
ppBlock Bool
False Bool
False Maybe (CFGPostdom blocks)
forall a. Maybe a
Nothing Block ext blocks ret args
blk

instance PrettyExt ext => ShowF (Block ext blocks ret)

#ifndef UNSAFE_OPS
extendBlock :: Block ext blocks ret ctx -> Block ext (blocks ::> new) ret ctx
extendBlock b =
  Block { blockID = extendBlockID (blockID b)
        , blockInputs = blockInputs b
        , _blockStmts = extendStmtSeq knownDiff (b^.blockStmts)
        }
#endif

------------------------------------------------------------------------
-- BlockMap

-- | A mapping from block indices to CFG blocks
type BlockMap ext blocks ret = Assignment (Block ext blocks ret) blocks

getBlock :: BlockID blocks args
         -> BlockMap ext blocks ret
         -> Block ext blocks ret args
getBlock :: forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock (BlockID Index blocks args
i) BlockMap ext blocks ret
m = BlockMap ext blocks ret
m BlockMap ext blocks ret
-> Index blocks args -> Block ext blocks ret args
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index blocks args
i

extendBlockMap :: Assignment (Block ext blocks ret) b
               -> Assignment (Block ext (blocks ::> args) ret) b
#ifdef UNSAFE_OPS
extendBlockMap :: forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (b :: Ctx (Ctx CrucibleType)) (args :: Ctx CrucibleType).
Assignment (Block ext blocks ret) b
-> Assignment (Block ext (blocks ::> args) ret) b
extendBlockMap = Assignment (Block ext blocks ret) b
-> Assignment (Block ext (blocks ::> args) ret) b
forall a b. a -> b
unsafeCoerce
#else
extendBlockMap = fmapFC extendBlock
#endif
------------------------------------------------------------------------
-- CFG

-- | A CFG consists of:
--
-- * a function handle, uniquely identifying the function this CFG
-- implements;
--
-- * a block map, representing the main CFG data structure;
--
-- * and the identifier of the function entry point.
--
-- The @blocks@ type parameter maps each block identifier to the
-- formal arguments it expects.  The @init@ type parameter identifies
-- the formal arguments of the function represented by this control-flow graph,
-- which correspond to the formal arguments of the CFG entry point.
-- The @ret@ type parameter indicates the return type of the function.
data CFG (ext :: Type)
         (blocks :: Ctx (Ctx CrucibleType))
         (init :: Ctx CrucibleType)
         (ret :: CrucibleType)
   = CFG { forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgHandle :: FnHandle init ret
         , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap :: !(BlockMap ext blocks ret)
         , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockID blocks init
cfgEntryBlockID :: !(BlockID blocks init)
         , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Bimap CutpointName (Some (BlockID blocks))
cfgCutpoints :: !(Bimap CutpointName (Some (BlockID blocks)))
         }

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

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

-- | Class for types that embed a CFG of some sort.
class HasSomeCFG f ext init ret | f -> ext, f -> init, f -> ret where
  getCFG :: f b -> SomeCFG ext init ret

instance PrettyExt ext => Show (CFG ext blocks init ret) where
  show :: CFG ext blocks init ret -> String
show CFG ext blocks init ret
g = Doc Any -> String
forall a. Show a => a -> String
show (Bool -> CFG ext blocks init ret -> Doc Any
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> CFG ext blocks init ret -> Doc ann
ppCFG Bool
True CFG ext blocks init ret
g)

-- | Pretty print a CFG.
ppCFG :: PrettyExt ext
      => Bool -- ^ Flag indicates if we should print line numbers
      -> CFG ext blocks init ret
      -> Doc ann
ppCFG :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> CFG ext blocks init ret -> Doc ann
ppCFG Bool
lineNumbers CFG ext blocks init ret
g = Bool -> CFGPostdom blocks -> CFG ext blocks init ret -> Doc ann
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> CFGPostdom blocks -> CFG ext blocks init ret -> Doc ann
ppCFG' Bool
lineNumbers (Size blocks -> CFGPostdom blocks
forall (blocks :: Ctx (Ctx CrucibleType)).
Size blocks -> CFGPostdom blocks
emptyCFGPostdomInfo Size blocks
sz) CFG ext blocks init ret
g
  where sz :: Size blocks
sz = Assignment (Block ext blocks ret) blocks -> Size blocks
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size (CFG ext blocks init ret -> Assignment (Block ext blocks ret) blocks
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
g)

-- | Pretty print CFG with postdom information.
ppCFG' :: PrettyExt ext
       => Bool -- ^ Flag indicates if we should print line numbers
       -> CFGPostdom blocks
       -> CFG ext blocks init ret
       -> Doc ann
ppCFG' :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> CFGPostdom blocks -> CFG ext blocks init ret -> Doc ann
ppCFG' Bool
lineNumbers CFGPostdom blocks
pdInfo CFG ext blocks init ret
g = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ((forall (x :: Ctx CrucibleType). Block ext blocks ret x -> Doc ann)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment (Block ext blocks ret) 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 :: Ctx CrucibleType -> Type) a.
(forall (x :: Ctx CrucibleType). f x -> a)
-> forall (x :: Ctx (Ctx CrucibleType)). Assignment f x -> [a]
toListFC (Bool
-> Bool
-> Maybe (CFGPostdom blocks)
-> Block ext blocks ret x
-> Doc ann
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType) ann.
PrettyExt ext =>
Bool
-> Bool
-> Maybe (CFGPostdom blocks)
-> Block ext blocks ret ctx
-> Doc ann
ppBlock Bool
lineNumbers Bool
blockArgs (CFGPostdom blocks -> Maybe (CFGPostdom blocks)
forall a. a -> Maybe a
Just CFGPostdom blocks
pdInfo)) (CFG ext blocks init ret -> Assignment (Block ext blocks ret) blocks
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
g))
  where blockArgs :: Bool
blockArgs = Bool
False

-- | Control flow graph with some blocks.  This data type closes
--   existentially over the @blocks@ type parameter.
data SomeCFG ext (init :: Ctx CrucibleType) (ret :: CrucibleType) where
  SomeCFG :: CFG ext blocks init ret -> SomeCFG ext init ret

instance PrettyExt ext => Show (SomeCFG ext i r)
  where show :: SomeCFG ext i r -> String
show SomeCFG ext i r
cfg = case SomeCFG ext i r
cfg of SomeCFG CFG ext blocks i r
c -> CFG ext blocks i r -> String
forall a. Show a => a -> String
show CFG ext blocks i r
c

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