{- |
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 Control.Lens
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 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 :: Simple 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
bBlock 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
bBlock 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
bBlock 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 BreakpointName (Some (BlockID blocks))
cfgBreakpoints :: !(Bimap BreakpointName (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