{-# 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(..)
, SomeCFG(..)
, HasSomeCFG(..)
, AnyCFG(..)
, ppCFG
, ppCFG'
, cfgArgTypes
, cfgReturnType
, CFGPostdom
, BlockMap
, getBlock
, extendBlockMap
, BlockID(..)
, extendBlockID
, extendBlockID'
, Block(..)
, blockLoc
, blockStmts
, withBlockTermStmt
, nextBlocks
, JumpTarget(..)
, extendJumpTarget
, jumpTargetID
, SwitchTarget(..)
, switchTargetID
, extendSwitchTarget
, StmtSeq(..)
, firstStmtLoc
, stmtSeqTermStmt
, Stmt(..)
, ppStmt
, nextStmtHeight
, applyEmbeddingStmt
, TermStmt(..)
, termStmtNextBlocks
, Expr(..)
, Reg(..)
, extendReg
, lastReg
, 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
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
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)
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)
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
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)
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
data JumpTarget blocks ctx where
JumpTarget :: !(BlockID blocks args)
-> !(CtxRepr args)
-> !(Assignment (Reg ctx) args)
-> 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)
data SwitchTarget blocks ctx tp where
SwitchTarget :: !(BlockID blocks (args ::> tp))
-> !(CtxRepr args)
-> !(Assignment (Reg ctx) args)
-> 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)
data Stmt ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) where
SetReg :: !(TypeRepr tp)
-> !(Expr ext ctx tp)
-> Stmt ext ctx (ctx ::> tp)
ExtendAssign :: !(StmtExtension ext (Reg ctx) tp)
-> Stmt ext ctx (ctx ::> tp)
CallHandle :: !(TypeRepr ret)
-> !(Reg ctx (FunctionHandleType args ret))
-> !(CtxRepr args)
-> !(Assignment (Reg ctx) args)
-> Stmt ext ctx (ctx ::> ret)
Print :: !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
ReadGlobal :: !(GlobalVar tp)
-> Stmt ext ctx (ctx ::> tp)
WriteGlobal :: !(GlobalVar tp)
-> !(Reg ctx tp)
-> Stmt ext ctx ctx
FreshConstant :: !(BaseTypeRepr bt)
-> !(Maybe SolverSymbol)
-> Stmt ext ctx (ctx ::> BaseToType bt)
FreshFloat :: !(FloatInfoRepr fi)
-> !(Maybe SolverSymbol)
-> Stmt ext ctx (ctx ::> FloatType fi)
FreshNat :: !(Maybe SolverSymbol)
-> Stmt ext ctx (ctx ::> NatType)
NewRefCell :: !(TypeRepr tp)
-> !(Reg ctx tp)
-> Stmt ext ctx (ctx ::> ReferenceType tp)
NewEmptyRefCell :: !(TypeRepr tp)
-> Stmt ext ctx (ctx ::> ReferenceType tp)
ReadRefCell :: !(Reg ctx (ReferenceType tp))
-> Stmt ext ctx (ctx ::> tp)
WriteRefCell :: !(Reg ctx (ReferenceType tp))
-> !(Reg ctx tp)
-> Stmt ext ctx ctx
DropRefCell :: !(Reg ctx (ReferenceType tp))
-> Stmt ext ctx ctx
Assert :: !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
Assume :: !(Reg ctx BoolType) -> !(Reg ctx (StringType Unicode)) -> Stmt ext ctx ctx
data TermStmt blocks (ret :: CrucibleType) (ctx :: Ctx CrucibleType) where
Jump :: !(JumpTarget blocks ctx)
-> TermStmt blocks ret ctx
Br :: !(Reg ctx BoolType)
-> !(JumpTarget blocks ctx)
-> !(JumpTarget blocks ctx)
-> TermStmt blocks ret ctx
MaybeBranch :: !(TypeRepr tp)
-> !(Reg ctx (MaybeType tp))
-> !(SwitchTarget blocks ctx tp)
-> !(JumpTarget blocks ctx)
-> TermStmt blocks rtp ctx
VariantElim :: !(CtxRepr varctx)
-> !(Reg ctx (VariantType varctx))
-> !(Assignment (SwitchTarget blocks ctx) varctx)
-> TermStmt blocks ret ctx
Return :: !(Reg ctx ret)
-> TermStmt blocks ret ctx
TailCall :: !(Reg ctx (FunctionHandleType args ret))
-> !(CtxRepr args)
-> !(Assignment (Reg ctx) args)
-> TermStmt blocks ret ctx
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
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
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)
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
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
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)
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 [])
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)
, forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs :: !(CtxRepr ctx)
, 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)
}
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 })
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)
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
-> Bool
-> Maybe (CFGPostdom blocks)
-> Block ext blocks ret ctx
-> 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
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
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 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)
ppCFG :: PrettyExt ext
=> Bool
-> 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)
ppCFG' :: PrettyExt ext
=> Bool
-> 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
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
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