------------------------------------------------------------------------
-- |
-- Module      : Lang.Crucible.Analysis.ForwardDataflow
-- Description : Forward dataflow analysis framework based on Kildall's algorithm
-- Copyright   : (c) Galois, Inc 2015
-- License     : BSD3
-- Maintainer  : Rob Dockins <rdockins@galois.com>
-- Stability   : provisional
--
-- This module defines a generic framework for forward dataflow analysis,
-- with some additional control-flow data on the side.
--
-- We calculate a fixpoint of a given analysis via the straightforward
-- method of iterating the transfer function until no more updates occur.
--
-- Our current method for doing this is quite naive, and more efficient
-- methods exist.
------------------------------------------------------------------------

{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}

module Lang.Crucible.Analysis.ForwardDataflow
{-# DEPRECATED "Lang.Crucible.Analysis.Fixpoint is a better implementation of these ideas" #-}
where

import           Control.Lens
import           Control.Monad.State.Strict
import           Data.Kind
import           Data.Parameterized.Context ( Assignment )
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.TraversableFC
import           Data.Set (Set)
import qualified Data.Set as Set
import           Prelude hiding (foldr)
import           Prettyprinter


import           Lang.Crucible.Types
import           Lang.Crucible.CFG.Core
import           Lang.Crucible.CFG.Expr

import qualified Debug.Trace as Debug

-----------------------
data SymDom = Dead | Symbolic | Concrete
  deriving (SymDom -> SymDom -> Bool
(SymDom -> SymDom -> Bool)
-> (SymDom -> SymDom -> Bool) -> Eq SymDom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SymDom -> SymDom -> Bool
== :: SymDom -> SymDom -> Bool
$c/= :: SymDom -> SymDom -> Bool
/= :: SymDom -> SymDom -> Bool
Eq, Eq SymDom
Eq SymDom =>
(SymDom -> SymDom -> Ordering)
-> (SymDom -> SymDom -> Bool)
-> (SymDom -> SymDom -> Bool)
-> (SymDom -> SymDom -> Bool)
-> (SymDom -> SymDom -> Bool)
-> (SymDom -> SymDom -> SymDom)
-> (SymDom -> SymDom -> SymDom)
-> Ord SymDom
SymDom -> SymDom -> Bool
SymDom -> SymDom -> Ordering
SymDom -> SymDom -> SymDom
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
$ccompare :: SymDom -> SymDom -> Ordering
compare :: SymDom -> SymDom -> Ordering
$c< :: SymDom -> SymDom -> Bool
< :: SymDom -> SymDom -> Bool
$c<= :: SymDom -> SymDom -> Bool
<= :: SymDom -> SymDom -> Bool
$c> :: SymDom -> SymDom -> Bool
> :: SymDom -> SymDom -> Bool
$c>= :: SymDom -> SymDom -> Bool
>= :: SymDom -> SymDom -> Bool
$cmax :: SymDom -> SymDom -> SymDom
max :: SymDom -> SymDom -> SymDom
$cmin :: SymDom -> SymDom -> SymDom
min :: SymDom -> SymDom -> SymDom
Ord, Int -> SymDom -> ShowS
[SymDom] -> ShowS
SymDom -> String
(Int -> SymDom -> ShowS)
-> (SymDom -> String) -> ([SymDom] -> ShowS) -> Show SymDom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SymDom -> ShowS
showsPrec :: Int -> SymDom -> ShowS
$cshow :: SymDom -> String
show :: SymDom -> String
$cshowList :: [SymDom] -> ShowS
showList :: [SymDom] -> ShowS
Show)

symbolicResults
   :: IsSyntaxExtension ext
   => CFG ext blocks init ret
   -- -> Assignment (Ignore SymDom) init
   -> String
   -- -> (Assignment (KildallPair (Assignment (Ignore SymDom)) SymDom) blocks, Ignore SymDom ret, SymDom)
symbolicResults :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext blocks init ret -> String
symbolicResults CFG ext blocks init ret
cfg = (Assignment
   (KildallPair (Assignment (Ignore SymDom)) SymDom) blocks,
 Ignore SymDom ret, SymDom)
-> String
forall a. Show a => a -> String
show ((Assignment
    (KildallPair (Assignment (Ignore SymDom)) SymDom) blocks,
  Ignore SymDom ret, SymDom)
 -> String)
-> (Assignment
      (KildallPair (Assignment (Ignore SymDom)) SymDom) blocks,
    Ignore SymDom ret, SymDom)
-> String
forall a b. (a -> b) -> a -> b
$ KildallForward ext blocks (Ignore SymDom) SymDom
-> CFG ext blocks init ret
-> (Assignment (Ignore SymDom) init, SymDom)
-> (Assignment
      (KildallPair (Assignment (Ignore SymDom)) SymDom) blocks,
    Ignore SymDom ret, SymDom)
forall ext (a :: CrucibleType -> Type) c
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (init :: Ctx CrucibleType).
KildallForward ext blocks a c
-> CFG ext blocks init ret
-> (Assignment a init, c)
-> (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
kildall_forward KildallForward ext blocks (Ignore SymDom) SymDom
forall ext (blocks :: Ctx (Ctx CrucibleType)).
IsSyntaxExtension ext =>
KildallForward ext blocks (Ignore SymDom) SymDom
symbolicAnalysis CFG ext blocks init ret
cfg (Assignment (Ignore SymDom) init
begin, SymDom
Concrete)
 where sz :: Size init
sz = Assignment TypeRepr init -> Size init
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size (Block ext blocks ret init -> Assignment TypeRepr init
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs (BlockID blocks init
-> BlockMap ext blocks ret -> Block ext blocks ret init
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock (CFG ext blocks init ret -> BlockID blocks init
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockID blocks init
cfgEntryBlockID CFG ext blocks init ret
cfg) (CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
cfg)))
       begin :: Assignment (Ignore SymDom) init
begin = Size init
-> (forall (tp :: CrucibleType). Index init tp -> Ignore SymDom tp)
-> Assignment (Ignore SymDom) init
forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
Ctx.generate Size init
sz (\Index init tp
_ -> SymDom -> Ignore SymDom tp
forall k a (b :: k). a -> Ignore a b
Ignore SymDom
Symbolic)


symlub :: SymDom -> SymDom -> SymDom
symlub :: SymDom -> SymDom -> SymDom
symlub SymDom
Dead SymDom
x = SymDom
x
symlub SymDom
x SymDom
Dead = SymDom
x
symlub SymDom
Symbolic SymDom
_ = SymDom
Symbolic
symlub SymDom
_ SymDom
Symbolic = SymDom
Symbolic
symlub SymDom
Concrete SymDom
Concrete = SymDom
Concrete

sym_reg_transfer :: Reg ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom
sym_reg_transfer :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom
sym_reg_transfer Reg ctx tp
reg Assignment (Ignore SymDom) ctx
asgn = Ignore SymDom tp -> SymDom
forall k a (b :: k). Ignore a b -> a
ignoreOut (Ignore SymDom tp -> SymDom) -> Ignore SymDom tp -> SymDom
forall a b. (a -> b) -> a -> b
$ Assignment (Ignore SymDom) ctx
asgn Assignment (Ignore SymDom) ctx -> Index ctx tp -> Ignore SymDom tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! (Reg ctx tp -> Index ctx tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
regIndex Reg ctx tp
reg)

sym_expr_transfer :: IsSyntaxExtension ext => Expr ext ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom
sym_expr_transfer :: forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
IsSyntaxExtension ext =>
Expr ext ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom
sym_expr_transfer (App App ext (Reg ctx) tp
a) Assignment (Ignore SymDom) ctx
asgn
  = (forall (x :: CrucibleType). Reg ctx x -> SymDom -> SymDom)
-> SymDom -> App ext (Reg ctx) tp -> SymDom
forall ext (f :: CrucibleType -> Type) r (tp :: CrucibleType).
TraversableFC (ExprExtension ext) =>
(forall (x :: CrucibleType). f x -> r -> r)
-> r -> App ext f tp -> r
foldApp (\Reg ctx x
r SymDom
z -> SymDom -> SymDom -> SymDom
symlub SymDom
z (SymDom -> SymDom) -> SymDom -> SymDom
forall a b. (a -> b) -> a -> b
$ Reg ctx x -> Assignment (Ignore SymDom) ctx -> SymDom
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom
sym_reg_transfer Reg ctx x
r Assignment (Ignore SymDom) ctx
asgn) SymDom
Dead App ext (Reg ctx) tp
a

-- FIXME this whole shabang is bogus, and should be replace by something that works...
-- we assume every function other than "matlabFunctionHandle" returns a symbolic
-- output, but does not have control flow that depends on symbolic data...
sym_call_transfer
  :: CtxRepr args
  -> TypeRepr ret
  -> Reg ctx (FunctionHandleType args ret)
  -> Ignore SymDom (FunctionHandleType args ret)
  -> Assignment a args
  -> Ignore SymDom ret
sym_call_transfer :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType) (a :: CrucibleType -> Type).
CtxRepr args
-> TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> Ignore SymDom (FunctionHandleType args ret)
-> Assignment a args
-> Ignore SymDom ret
sym_call_transfer CtxRepr args
_ TypeRepr ret
_ Reg ctx (FunctionHandleType args ret)
ex Ignore SymDom (FunctionHandleType args ret)
_ Assignment a args
_
  = String -> Ignore SymDom ret -> Ignore SymDom ret
forall a. String -> a -> a
Debug.trace (Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Reg ctx (FunctionHandleType args ret) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Reg ctx (FunctionHandleType args ret) -> Doc ann
pretty Reg ctx (FunctionHandleType args ret)
ex) (Ignore SymDom ret -> Ignore SymDom ret)
-> Ignore SymDom ret -> Ignore SymDom ret
forall a b. (a -> b) -> a -> b
$ SymDom -> Ignore SymDom ret
forall k a (b :: k). a -> Ignore a b
Ignore SymDom
Symbolic

symbolicAnalysis :: IsSyntaxExtension ext => KildallForward ext blocks (Ignore SymDom) SymDom
symbolicAnalysis :: forall ext (blocks :: Ctx (Ctx CrucibleType)).
IsSyntaxExtension ext =>
KildallForward ext blocks (Ignore SymDom) SymDom
symbolicAnalysis =
  KildallForward
  { kfwd_lub :: forall (tp :: CrucibleType).
Ignore SymDom tp -> Ignore SymDom tp -> Ignore SymDom tp
kfwd_lub = \(Ignore SymDom
x) (Ignore SymDom
y) -> SymDom -> Ignore SymDom tp
forall k a (b :: k). a -> Ignore a b
Ignore (SymDom -> SymDom -> SymDom
symlub SymDom
x SymDom
y)
  , kfwd_bot :: forall (tp :: CrucibleType). Ignore SymDom tp
kfwd_bot = SymDom -> Ignore SymDom tp
forall k a (b :: k). a -> Ignore a b
Ignore SymDom
Dead
  , kfwd_club :: SymDom -> SymDom -> SymDom
kfwd_club = SymDom -> SymDom -> SymDom
symlub
  , kfwd_cbot :: SymDom
kfwd_cbot = SymDom
Dead
  , kfwd_same :: forall (tp :: CrucibleType).
Ignore SymDom tp -> Ignore SymDom tp -> Bool
kfwd_same = \(Ignore SymDom
x) (Ignore SymDom
y) -> SymDom
x SymDom -> SymDom -> Bool
forall a. Eq a => a -> a -> Bool
== SymDom
y
  , kfwd_csame :: SymDom -> SymDom -> Bool
kfwd_csame = \SymDom
x SymDom
y -> SymDom
x SymDom -> SymDom -> Bool
forall a. Eq a => a -> a -> Bool
== SymDom
y
  , kfwd_br :: forall (ctx :: Ctx CrucibleType).
Reg ctx BoolType
-> Ignore SymDom BoolType -> SymDom -> (SymDom, SymDom)
kfwd_br = \Reg ctx BoolType
_ (Ignore SymDom
x) SymDom
y -> let z :: SymDom
z = SymDom -> SymDom -> SymDom
symlub SymDom
x SymDom
y in (SymDom
z, SymDom
z)
  , kfwd_maybe :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypeRepr tp
-> Reg ctx (MaybeType tp)
-> Ignore SymDom (MaybeType tp)
-> SymDom
-> (SymDom, Ignore SymDom tp, SymDom)
kfwd_maybe = \TypeRepr tp
_ Reg ctx (MaybeType tp)
_ (Ignore SymDom
x) SymDom
y -> let z :: SymDom
z = SymDom -> SymDom -> SymDom
symlub SymDom
x SymDom
y in (SymDom
z, SymDom -> Ignore SymDom tp
forall k a (b :: k). a -> Ignore a b
Ignore SymDom
x, SymDom
z)
  , kfwd_reg :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypeRepr tp
-> Reg ctx tp -> Assignment (Ignore SymDom) ctx -> Ignore SymDom tp
kfwd_reg  = \TypeRepr tp
_ Reg ctx tp
ex Assignment (Ignore SymDom) ctx
asgn -> SymDom -> Ignore SymDom tp
forall k a (b :: k). a -> Ignore a b
Ignore (SymDom -> Ignore SymDom tp) -> SymDom -> Ignore SymDom tp
forall a b. (a -> b) -> a -> b
$ Reg ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom
sym_reg_transfer Reg ctx tp
ex Assignment (Ignore SymDom) ctx
asgn
  , kfwd_expr :: forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
TypeRepr tp
-> Expr ext ctx tp
-> Assignment (Ignore SymDom) ctx
-> Ignore SymDom tp
kfwd_expr = \TypeRepr tp
_ Expr ext ctx tp
ex Assignment (Ignore SymDom) ctx
asgn -> SymDom -> Ignore SymDom tp
forall k a (b :: k). a -> Ignore a b
Ignore (SymDom -> Ignore SymDom tp) -> SymDom -> Ignore SymDom tp
forall a b. (a -> b) -> a -> b
$ Expr ext ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom
forall ext (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
IsSyntaxExtension ext =>
Expr ext ctx tp -> Assignment (Ignore SymDom) ctx -> SymDom
sym_expr_transfer Expr ext ctx tp
ex Assignment (Ignore SymDom) ctx
asgn
  , kfwd_call :: forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
CtxRepr args
-> TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> Ignore SymDom (FunctionHandleType args ret)
-> Assignment (Ignore SymDom) args
-> Ignore SymDom ret
kfwd_call = CtxRepr args
-> TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> Ignore SymDom (FunctionHandleType args ret)
-> Assignment (Ignore SymDom) args
-> Ignore SymDom ret
forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
CtxRepr args
-> TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> Ignore SymDom (FunctionHandleType args ret)
-> Assignment (Ignore SymDom) args
-> Ignore SymDom ret
forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType) (a :: CrucibleType -> Type).
CtxRepr args
-> TypeRepr ret
-> Reg ctx (FunctionHandleType args ret)
-> Ignore SymDom (FunctionHandleType args ret)
-> Assignment a args
-> Ignore SymDom ret
sym_call_transfer
  , kfwd_rdglobal :: forall (tp :: CrucibleType). GlobalVar tp -> Ignore SymDom tp
kfwd_rdglobal = \GlobalVar tp
_ -> SymDom -> Ignore SymDom tp
forall k a (b :: k). a -> Ignore a b
Ignore SymDom
Symbolic
             -- FIXME, here we make the totally pessimistic assumption
             -- that every global variable read is symbolic
  , kfwd_onentry :: forall (ctx :: Ctx CrucibleType).
BlockID blocks ctx
-> (Assignment (Ignore SymDom) ctx, SymDom)
-> (Assignment (Ignore SymDom) ctx, SymDom)
kfwd_onentry = \BlockID blocks ctx
_ (Assignment (Ignore SymDom) ctx, SymDom)
x -> (Assignment (Ignore SymDom) ctx, SymDom)
x
  }

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

data KildallPair (a::k -> Type) (c :: Type) (tp::k) = KP (a tp) c

instance (ShowF a, Show c) => Show (KildallPair a c tp) where
  show :: KildallPair a c tp -> String
show (KP a tp
x c
y) = String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a tp -> String
forall (tp :: k). a tp -> String
forall k (f :: k -> Type) (tp :: k). ShowF f => f tp -> String
showF a tp
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ c -> String
forall a. Show a => a -> String
show c
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

instance (ShowF a, Show c) => ShowF (KildallPair a c)

newtype Ignore a (b::k) = Ignore { forall k a (b :: k). Ignore a b -> a
ignoreOut :: a }
 deriving (Ignore a b -> Ignore a b -> Bool
(Ignore a b -> Ignore a b -> Bool)
-> (Ignore a b -> Ignore a b -> Bool) -> Eq (Ignore a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a k (b :: k). Eq a => Ignore a b -> Ignore a b -> Bool
$c== :: forall a k (b :: k). Eq a => Ignore a b -> Ignore a b -> Bool
== :: Ignore a b -> Ignore a b -> Bool
$c/= :: forall a k (b :: k). Eq a => Ignore a b -> Ignore a b -> Bool
/= :: Ignore a b -> Ignore a b -> Bool
Eq, Eq (Ignore a b)
Eq (Ignore a b) =>
(Ignore a b -> Ignore a b -> Ordering)
-> (Ignore a b -> Ignore a b -> Bool)
-> (Ignore a b -> Ignore a b -> Bool)
-> (Ignore a b -> Ignore a b -> Bool)
-> (Ignore a b -> Ignore a b -> Bool)
-> (Ignore a b -> Ignore a b -> Ignore a b)
-> (Ignore a b -> Ignore a b -> Ignore a b)
-> Ord (Ignore a b)
Ignore a b -> Ignore a b -> Bool
Ignore a b -> Ignore a b -> Ordering
Ignore a b -> Ignore a b -> Ignore a b
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a k (b :: k). Ord a => Eq (Ignore a b)
forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Bool
forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Ordering
forall a k (b :: k).
Ord a =>
Ignore a b -> Ignore a b -> Ignore a b
$ccompare :: forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Ordering
compare :: Ignore a b -> Ignore a b -> Ordering
$c< :: forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Bool
< :: Ignore a b -> Ignore a b -> Bool
$c<= :: forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Bool
<= :: Ignore a b -> Ignore a b -> Bool
$c> :: forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Bool
> :: Ignore a b -> Ignore a b -> Bool
$c>= :: forall a k (b :: k). Ord a => Ignore a b -> Ignore a b -> Bool
>= :: Ignore a b -> Ignore a b -> Bool
$cmax :: forall a k (b :: k).
Ord a =>
Ignore a b -> Ignore a b -> Ignore a b
max :: Ignore a b -> Ignore a b -> Ignore a b
$cmin :: forall a k (b :: k).
Ord a =>
Ignore a b -> Ignore a b -> Ignore a b
min :: Ignore a b -> Ignore a b -> Ignore a b
Ord)

instance Show a => Show (Ignore a tp) where
  show :: Ignore a tp -> String
show (Ignore a
x) = a -> String
forall a. Show a => a -> String
show a
x

instance Show a => ShowF (Ignore a)


data KildallForward ext blocks (a :: CrucibleType -> Type) c
  = KildallForward
    { forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (tp :: CrucibleType). a tp -> a tp -> a tp
kfwd_lub      :: forall tp. a tp -> a tp -> a tp
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> forall (tp :: CrucibleType). a tp
kfwd_bot      :: forall tp. a tp
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> c -> c -> c
kfwd_club     :: c -> c -> c
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> c
kfwd_cbot     :: c
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (tp :: CrucibleType). a tp -> a tp -> Bool
kfwd_same     :: forall tp. a tp -> a tp -> Bool
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> c -> c -> Bool
kfwd_csame    :: c -> c -> Bool
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType).
   Reg ctx BoolType -> a BoolType -> c -> (c, c)
kfwd_br       :: forall ctx. Reg ctx BoolType -> a BoolType -> c -> (c, c)
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp
   -> Reg ctx (MaybeType tp) -> a (MaybeType tp) -> c -> (c, a tp, c)
kfwd_maybe    :: forall ctx tp. TypeRepr tp -> Reg ctx (MaybeType tp) -> a (MaybeType tp) -> c -> (c, a tp, c)
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
kfwd_reg      :: !(forall ctx tp. TypeRepr tp -> Reg ctx tp  -> Assignment a ctx -> a tp)
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Expr ext ctx tp -> Assignment a ctx -> a tp
kfwd_expr     :: !(forall ctx tp. TypeRepr tp -> Expr ext ctx tp -> Assignment a ctx -> a tp)
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
          (ret :: CrucibleType).
   CtxRepr args
   -> TypeRepr ret
   -> Reg ctx (FunctionHandleType args ret)
   -> a (FunctionHandleType args ret)
   -> Assignment a args
   -> a ret
kfwd_call     :: forall ctx args ret. CtxRepr args
                                         -> TypeRepr ret
                                         -> Reg ctx (FunctionHandleType args ret)
                                         -> a (FunctionHandleType args ret)
                                         -> Assignment a args
                                         -> a ret
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (tp :: CrucibleType). GlobalVar tp -> a tp
kfwd_rdglobal :: forall tp. GlobalVar tp -> a tp
    , forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType).
   BlockID blocks ctx
   -> (Assignment a ctx, c) -> (Assignment a ctx, c)
kfwd_onentry  :: forall ctx. BlockID blocks ctx -> (Assignment a ctx, c) -> (Assignment a ctx, c)
    }

kildall_transfer
   :: forall ext a c blocks ret ctx
    . KildallForward ext blocks a c
   -> TypeRepr ret
   -> Block ext blocks ret ctx
   -> (Assignment a ctx, c)
   -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))
kildall_transfer :: forall ext (a :: CrucibleType -> Type) c
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
KildallForward ext blocks a c
-> TypeRepr ret
-> Block ext blocks ret ctx
-> (Assignment a ctx, c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
kildall_transfer KildallForward ext blocks a c
analysis TypeRepr ret
retRepr Block ext blocks ret ctx
blk = StmtSeq ext blocks ret ctx
-> (Assignment a ctx, c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
StmtSeq ext blocks ret ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_seq (Block ext blocks ret ctx -> StmtSeq ext blocks ret ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> StmtSeq ext blocks ret ctx
_blockStmts Block ext blocks ret ctx
blk)
 where transfer_seq :: forall ctx'
                     . StmtSeq ext blocks ret ctx'
                    -> (Assignment a ctx', c)
                    -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))

       transfer_seq :: forall (ctx' :: Ctx CrucibleType).
StmtSeq ext blocks ret ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_seq (ConsStmt ProgramLoc
_loc Stmt ext ctx' ctx'
stmt StmtSeq ext blocks ret ctx'
ss) (Assignment a ctx', c)
x = StmtSeq ext blocks ret ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
StmtSeq ext blocks ret ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_seq StmtSeq ext blocks ret ctx'
ss (Stmt ext ctx' ctx'
-> (Assignment a ctx', c) -> (Assignment a ctx', c)
forall (ctx1 :: Ctx CrucibleType) (ctx2 :: Ctx CrucibleType).
Stmt ext ctx1 ctx2
-> (Assignment a ctx1, c) -> (Assignment a ctx2, c)
transfer_stmt Stmt ext ctx' ctx'
stmt (Assignment a ctx', c)
x)
       transfer_seq (TermStmt ProgramLoc
_loc TermStmt blocks ret ctx'
term) (Assignment a ctx', c)
x = TermStmt blocks ret ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
TermStmt blocks ret ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_term TermStmt blocks ret ctx'
term (Assignment a ctx', c)
x

       transfer_stmt :: forall ctx1 ctx2. Stmt ext ctx1 ctx2 -> (Assignment a ctx1, c) -> (Assignment a ctx2, c)
       transfer_stmt :: forall (ctx1 :: Ctx CrucibleType) (ctx2 :: Ctx CrucibleType).
Stmt ext ctx1 ctx2
-> (Assignment a ctx1, c) -> (Assignment a ctx2, c)
transfer_stmt (SetReg TypeRepr tp
tp Expr ext ctx1 tp
ex) (Assignment a ctx1
asgn, c
c) = (Assignment a ctx1 -> a tp -> Assignment a (ctx1 '::> tp)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
Ctx.extend Assignment a ctx1
asgn (KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Expr ext ctx tp -> Assignment a ctx -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Expr ext ctx tp -> Assignment a ctx -> a tp
kfwd_expr KildallForward ext blocks a c
analysis TypeRepr tp
tp Expr ext ctx1 tp
ex Assignment a ctx1
asgn), c
c)
       transfer_stmt (CallHandle TypeRepr ret
rettp Reg ctx1 (FunctionHandleType args ret)
ex CtxRepr args
argstp Assignment (Reg ctx1) args
actuals) (Assignment a ctx1
asgn, c
c) =
           let xs :: Assignment a args
xs = (forall (x :: CrucibleType). TypeRepr x -> Reg ctx1 x -> a x)
-> CtxRepr args -> Assignment (Reg ctx1) args -> Assignment a args
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
       (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
Ctx.zipWith (\TypeRepr x
tp Reg ctx1 x
act -> KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
kfwd_reg KildallForward ext blocks a c
analysis TypeRepr x
tp Reg ctx1 x
act Assignment a ctx1
asgn) CtxRepr args
argstp Assignment (Reg ctx1) args
actuals
               ex_sh :: a (FunctionHandleType args ret)
ex_sh = KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
kfwd_reg KildallForward ext blocks a c
analysis (CtxRepr args
-> TypeRepr ret -> TypeRepr (FunctionHandleType args ret)
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr ctx
-> TypeRepr ret -> TypeRepr ('FunctionHandleType ctx ret)
FunctionHandleRepr CtxRepr args
argstp TypeRepr ret
rettp) Reg ctx1 (FunctionHandleType args ret)
ex Assignment a ctx1
asgn
               a' :: a ret
a' = KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
          (ret :: CrucibleType).
   CtxRepr args
   -> TypeRepr ret
   -> Reg ctx (FunctionHandleType args ret)
   -> a (FunctionHandleType args ret)
   -> Assignment a args
   -> a ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
          (ret :: CrucibleType).
   CtxRepr args
   -> TypeRepr ret
   -> Reg ctx (FunctionHandleType args ret)
   -> a (FunctionHandleType args ret)
   -> Assignment a args
   -> a ret
kfwd_call KildallForward ext blocks a c
analysis CtxRepr args
argstp TypeRepr ret
rettp Reg ctx1 (FunctionHandleType args ret)
ex a (FunctionHandleType args ret)
ex_sh Assignment a args
xs
            in (Assignment a ctx1 -> a ret -> Assignment a (ctx1 '::> ret)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
Ctx.extend Assignment a ctx1
asgn a ret
a', c
c)
       transfer_stmt (Print Reg ctx1 (StringType Unicode)
_) (Assignment a ctx1, c)
asgn = (Assignment a ctx1, c)
(Assignment a ctx2, c)
asgn
       transfer_stmt (ReadGlobal GlobalVar tp
gv) (Assignment a ctx1
asgn, c
c) = (Assignment a ctx1 -> a tp -> Assignment a (ctx1 '::> tp)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
Ctx.extend Assignment a ctx1
asgn (KildallForward ext blocks a c
-> forall (tp :: CrucibleType). GlobalVar tp -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (tp :: CrucibleType). GlobalVar tp -> a tp
kfwd_rdglobal KildallForward ext blocks a c
analysis GlobalVar tp
gv), c
c)
       transfer_stmt FreshConstant{} (Assignment a ctx1, c)
_ = String -> (Assignment a ctx2, c)
forall a. HasCallStack => String -> a
error String
"forward dataflow: fresh constant!"
       transfer_stmt FreshFloat{} (Assignment a ctx1, c)
_ = String -> (Assignment a ctx2, c)
forall a. HasCallStack => String -> a
error String
"forward dataflow: fresh float!"
       transfer_stmt FreshNat{} (Assignment a ctx1, c)
_ = String -> (Assignment a ctx2, c)
forall a. HasCallStack => String -> a
error String
"forward dataflow: fresh nat!"
       transfer_stmt ExtendAssign{} (Assignment a ctx1, c)
_ = String -> (Assignment a ctx2, c)
forall a. HasCallStack => String -> a
error String
"extension statement!"
       transfer_stmt NewRefCell{} (Assignment a ctx1, c)
_ = String -> (Assignment a ctx2, c)
forall a. HasCallStack => String -> a
error String
"forward dataflow: reference cell!"
       transfer_stmt NewEmptyRefCell{} (Assignment a ctx1, c)
_ = String -> (Assignment a ctx2, c)
forall a. HasCallStack => String -> a
error String
"forward dataflow: reference cell!"
       transfer_stmt ReadRefCell{} (Assignment a ctx1, c)
_ = String -> (Assignment a ctx2, c)
forall a. HasCallStack => String -> a
error String
"forward dataflow: reference cell!"
       transfer_stmt WriteRefCell{} (Assignment a ctx1, c)
_ = String -> (Assignment a ctx2, c)
forall a. HasCallStack => String -> a
error String
"forward dataflow: reference cell!"
       transfer_stmt DropRefCell{} (Assignment a ctx1, c)
_ = String -> (Assignment a ctx2, c)
forall a. HasCallStack => String -> a
error String
"forward dataflow: reference cell!"
       transfer_stmt (WriteGlobal GlobalVar tp
_ Reg ctx1 tp
_) (Assignment a ctx1, c)
asgnc = (Assignment a ctx1, c)
(Assignment a ctx2, c)
asgnc -- FIXME? need to check something here, perhaps?
       transfer_stmt (Assert Reg ctx1 BoolType
_ Reg ctx1 (StringType Unicode)
_) (Assignment a ctx1, c)
asgnc = (Assignment a ctx1, c)
(Assignment a ctx2, c)
asgnc -- FIXME? is it useful to remember assertions some way?
       transfer_stmt (Assume Reg ctx1 BoolType
_ Reg ctx1 (StringType Unicode)
_) (Assignment a ctx1, c)
asgnc = (Assignment a ctx1, c)
(Assignment a ctx2, c)
asgnc -- FIXME? is it useful to remember assertions some way?

       transfer_term :: forall ctx'
                      . TermStmt blocks ret ctx'
                     -> (Assignment a ctx', c)
                     -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))

       transfer_term :: forall (ctx' :: Ctx CrucibleType).
TermStmt blocks ret ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_term (ErrorStmt Reg ctx' (StringType Unicode)
_) (Assignment a ctx', c)
_ = Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall a.
a
-> StateT
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     Identity
     a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Set (Some (BlockID blocks))
forall a. Set a
Set.empty

       transfer_term (Jump JumpTarget blocks ctx'
tgt) (Assignment a ctx', c)
x = JumpTarget blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
JumpTarget blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_jump JumpTarget blocks ctx'
tgt (Assignment a ctx', c)
x

       transfer_term (Br Reg ctx' BoolType
ex JumpTarget blocks ctx'
tgt1 JumpTarget blocks ctx'
tgt2) (Assignment a ctx'
asgn,c
c) = do
           let a :: a BoolType
a = KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
kfwd_reg KildallForward ext blocks a c
analysis TypeRepr BoolType
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr Reg ctx' BoolType
ex Assignment a ctx'
asgn
           let (c
c1,c
c2) = KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType).
   Reg ctx BoolType -> a BoolType -> c -> (c, c)
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType).
   Reg ctx BoolType -> a BoolType -> c -> (c, c)
kfwd_br KildallForward ext blocks a c
analysis Reg ctx' BoolType
ex a BoolType
a c
c
           Set (Some (BlockID blocks))
s1 <- JumpTarget blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
JumpTarget blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_jump JumpTarget blocks ctx'
tgt1 (Assignment a ctx'
asgn,c
c1)
           Set (Some (BlockID blocks))
s2 <- JumpTarget blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
JumpTarget blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_jump JumpTarget blocks ctx'
tgt2 (Assignment a ctx'
asgn,c
c2)
           Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall a.
a
-> StateT
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     Identity
     a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Set (Some (BlockID blocks))
-> Set (Some (BlockID blocks)) -> Set (Some (BlockID blocks))
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Some (BlockID blocks))
s1 Set (Some (BlockID blocks))
s2)

       transfer_term (Return Reg ctx' ret
ex) (Assignment a ctx'
asgn, c
c) = do
           let a :: a ret
a = KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
kfwd_reg KildallForward ext blocks a c
analysis TypeRepr ret
retRepr Reg ctx' ret
ex Assignment a ctx'
asgn
           ((Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
 -> (Assignment (KildallPair (Assignment a) c) blocks, a ret, c))
-> StateT
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     Identity
     ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (\ (Assignment (KildallPair (Assignment a) c) blocks
x,a ret
r,c
rc) -> (Assignment (KildallPair (Assignment a) c) blocks
x, KildallForward ext blocks a c
-> forall (tp :: CrucibleType). a tp -> a tp -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (tp :: CrucibleType). a tp -> a tp -> a tp
kfwd_lub KildallForward ext blocks a c
analysis a ret
r a ret
a, KildallForward ext blocks a c -> c -> c -> c
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> c -> c -> c
kfwd_club KildallForward ext blocks a c
analysis c
rc c
c))
           Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall a.
a
-> StateT
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     Identity
     a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Set (Some (BlockID blocks))
forall a. Set a
Set.empty

       transfer_term (TailCall Reg ctx' (FunctionHandleType args ret)
fn CtxRepr args
callargs Assignment (Reg ctx') args
actuals) (Assignment a ctx'
asgn, c
c) = do
           let xs :: Assignment a args
xs = (forall (x :: CrucibleType). TypeRepr x -> Reg ctx' x -> a x)
-> CtxRepr args -> Assignment (Reg ctx') args -> Assignment a args
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
       (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
Ctx.zipWith (\TypeRepr x
tp Reg ctx' x
act -> KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
kfwd_reg KildallForward ext blocks a c
analysis TypeRepr x
tp Reg ctx' x
act Assignment a ctx'
asgn) CtxRepr args
callargs Assignment (Reg ctx') args
actuals
           let fn_sh :: a (FunctionHandleType args ret)
fn_sh = KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
kfwd_reg KildallForward ext blocks a c
analysis (CtxRepr args
-> TypeRepr ret -> TypeRepr (FunctionHandleType args ret)
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr ctx
-> TypeRepr ret -> TypeRepr ('FunctionHandleType ctx ret)
FunctionHandleRepr CtxRepr args
callargs TypeRepr ret
retRepr) Reg ctx' (FunctionHandleType args ret)
fn Assignment a ctx'
asgn
           let a' :: a ret
a' = KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
          (ret :: CrucibleType).
   CtxRepr args
   -> TypeRepr ret
   -> Reg ctx (FunctionHandleType args ret)
   -> a (FunctionHandleType args ret)
   -> Assignment a args
   -> a ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (args :: Ctx CrucibleType)
          (ret :: CrucibleType).
   CtxRepr args
   -> TypeRepr ret
   -> Reg ctx (FunctionHandleType args ret)
   -> a (FunctionHandleType args ret)
   -> Assignment a args
   -> a ret
kfwd_call KildallForward ext blocks a c
analysis CtxRepr args
callargs TypeRepr ret
retRepr Reg ctx' (FunctionHandleType args ret)
fn a (FunctionHandleType args ret)
fn_sh Assignment a args
xs
           ((Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
 -> (Assignment (KildallPair (Assignment a) c) blocks, a ret, c))
-> StateT
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     Identity
     ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (\ (Assignment (KildallPair (Assignment a) c) blocks
x,a ret
r,c
rc) -> (Assignment (KildallPair (Assignment a) c) blocks
x, KildallForward ext blocks a c
-> forall (tp :: CrucibleType). a tp -> a tp -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (tp :: CrucibleType). a tp -> a tp -> a tp
kfwd_lub KildallForward ext blocks a c
analysis a ret
r a ret
a', KildallForward ext blocks a c -> c -> c -> c
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> c -> c -> c
kfwd_club KildallForward ext blocks a c
analysis c
rc c
c))
           Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall a.
a
-> StateT
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     Identity
     a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Set (Some (BlockID blocks))
forall a. Set a
Set.empty

       transfer_term (MaybeBranch TypeRepr tp
tp Reg ctx' (MaybeType tp)
ex SwitchTarget blocks ctx' tp
swtgt JumpTarget blocks ctx'
jmptgt) (Assignment a ctx'
asgn, c
c) = do
           let a :: a (MaybeType tp)
a = KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
kfwd_reg KildallForward ext blocks a c
analysis (TypeRepr tp -> TypeRepr (MaybeType tp)
forall (tp1 :: CrucibleType).
TypeRepr tp1 -> TypeRepr ('MaybeType tp1)
MaybeRepr TypeRepr tp
tp) Reg ctx' (MaybeType tp)
ex Assignment a ctx'
asgn
           let (c
c1, a tp
a1, c
c2) = KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp
   -> Reg ctx (MaybeType tp) -> a (MaybeType tp) -> c -> (c, a tp, c)
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp
   -> Reg ctx (MaybeType tp) -> a (MaybeType tp) -> c -> (c, a tp, c)
kfwd_maybe KildallForward ext blocks a c
analysis TypeRepr tp
tp Reg ctx' (MaybeType tp)
ex a (MaybeType tp)
a c
c
           Set (Some (BlockID blocks))
s1 <- SwitchTarget blocks ctx' tp
-> a tp
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType) (tp :: CrucibleType).
SwitchTarget blocks ctx' tp
-> a tp
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_switch SwitchTarget blocks ctx' tp
swtgt a tp
a1 (Assignment a ctx'
asgn, c
c1)
           Set (Some (BlockID blocks))
s2 <- JumpTarget blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
JumpTarget blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_jump JumpTarget blocks ctx'
jmptgt (Assignment a ctx'
asgn, c
c2)
           Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall a.
a
-> StateT
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     Identity
     a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Set (Some (BlockID blocks))
-> Set (Some (BlockID blocks)) -> Set (Some (BlockID blocks))
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Some (BlockID blocks))
s1 Set (Some (BlockID blocks))
s2)

       transfer_term (VariantElim CtxRepr varctx
_ctx Reg ctx' (VariantType varctx)
_ex Assignment (SwitchTarget blocks ctx') varctx
_switch) (Assignment a ctx'
_asgn, c
_c) = do
           String
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall a. HasCallStack => String -> a
error String
"FIXME: transfer_term for VariantElim not implemented"

       transfer_switch :: forall ctx' tp
                        . SwitchTarget blocks ctx' tp
                       -> a tp
                       -> (Assignment a ctx', c)
                       -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))
       transfer_switch :: forall (ctx' :: Ctx CrucibleType) (tp :: CrucibleType).
SwitchTarget blocks ctx' tp
-> a tp
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_switch (SwitchTarget BlockID blocks (args ::> tp)
tgt CtxRepr args
argstp Assignment (Reg ctx') args
actuals) a tp
a1 (Assignment a ctx'
asgn, c
c) = do
           let xs :: Assignment a args
xs = (forall (x :: CrucibleType). TypeRepr x -> Reg ctx' x -> a x)
-> CtxRepr args -> Assignment (Reg ctx') args -> Assignment a args
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
       (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
Ctx.zipWith (\TypeRepr x
tp Reg ctx' x
act -> KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
kfwd_reg KildallForward ext blocks a c
analysis TypeRepr x
tp Reg ctx' x
act Assignment a ctx'
asgn) CtxRepr args
argstp Assignment (Reg ctx') args
actuals
           let xs' :: Assignment a (args ::> tp)
xs' = Assignment a args -> a tp -> Assignment a (args ::> tp)
forall {k} (f :: k -> Type) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
Ctx.extend Assignment a args
xs a tp
a1
           BlockID blocks (args ::> tp)
-> (Assignment a (args ::> tp), c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
BlockID blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_target BlockID blocks (args ::> tp)
tgt (Assignment a (args ::> tp)
xs', c
c)

       transfer_jump :: forall ctx'
                      . JumpTarget blocks ctx'
                     -> (Assignment a ctx', c)
                     -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))

       transfer_jump :: forall (ctx' :: Ctx CrucibleType).
JumpTarget blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_jump (JumpTarget BlockID blocks args
tgt CtxRepr args
argstp Assignment (Reg ctx') args
actuals) (Assignment a ctx'
asgn, c
c) = do
           let xs :: Assignment a args
xs = (forall (x :: CrucibleType). TypeRepr x -> Reg ctx' x -> a x)
-> CtxRepr args -> Assignment (Reg ctx') args -> Assignment a args
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
       (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
Ctx.zipWith (\TypeRepr x
tp Reg ctx' x
act -> KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
   TypeRepr tp -> Reg ctx tp -> Assignment a ctx -> a tp
kfwd_reg KildallForward ext blocks a c
analysis TypeRepr x
tp Reg ctx' x
act Assignment a ctx'
asgn) CtxRepr args
argstp Assignment (Reg ctx') args
actuals
           BlockID blocks args
-> (Assignment a args, c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall (ctx' :: Ctx CrucibleType).
BlockID blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_target BlockID blocks args
tgt (Assignment a args
xs, c
c)

       transfer_target :: forall ctx'
                        . BlockID blocks ctx'
                       -> (Assignment a ctx', c)
                       -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) (Set (Some (BlockID blocks)))
       transfer_target :: forall (ctx' :: Ctx CrucibleType).
BlockID blocks ctx'
-> (Assignment a ctx', c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
transfer_target tgt :: BlockID blocks ctx'
tgt@(BlockID Index blocks ctx'
idx) (Assignment a ctx'
asgn, c
c) = do
           (Assignment (KildallPair (Assignment a) c) blocks
x,a ret
r,c
rc) <- StateT
  (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
  Identity
  (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
forall s (m :: Type -> Type). MonadState s m => m s
get
           let KP Assignment a ctx'
old c
oldc = Assignment (KildallPair (Assignment a) c) blocks
x Assignment (KildallPair (Assignment a) c) blocks
-> Index blocks ctx' -> KildallPair (Assignment a) c ctx'
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index blocks ctx'
idx
           let new :: Assignment a ctx'
new = (forall (tp :: CrucibleType). a tp -> a tp -> a tp)
-> Assignment a ctx' -> Assignment a ctx' -> Assignment a ctx'
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
       (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
Ctx.zipWith (\a x
a a x
b -> KildallForward ext blocks a c
-> forall (tp :: CrucibleType). a tp -> a tp -> a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (tp :: CrucibleType). a tp -> a tp -> a tp
kfwd_lub KildallForward ext blocks a c
analysis a x
a a x
b) Assignment a ctx'
old Assignment a ctx'
asgn
           let zipsame :: Assignment (Ignore Bool) ctx'
zipsame = (forall (x :: CrucibleType). a x -> a x -> Ignore Bool x)
-> Assignment a ctx'
-> Assignment a ctx'
-> Assignment (Ignore Bool) ctx'
forall {k} (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
       (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
Ctx.zipWith (\a x
a a x
b -> Bool -> Ignore Bool x
forall k a (b :: k). a -> Ignore a b
Ignore (Bool -> Ignore Bool x) -> Bool -> Ignore Bool x
forall a b. (a -> b) -> a -> b
$ KildallForward ext blocks a c
-> forall (tp :: CrucibleType). a tp -> a tp -> Bool
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (tp :: CrucibleType). a tp -> a tp -> Bool
kfwd_same KildallForward ext blocks a c
analysis a x
a a x
b) Assignment a ctx'
old Assignment a ctx'
new
           let samex :: Bool
samex = (forall (x :: CrucibleType). Bool -> Ignore Bool x -> Bool)
-> forall (x :: Ctx CrucibleType).
   Bool -> Assignment (Ignore Bool) x -> Bool
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type) b.
FoldableFC t =>
(forall (x :: k). b -> f x -> b)
-> forall (x :: l). b -> t f x -> b
forall (f :: CrucibleType -> Type) b.
(forall (x :: CrucibleType). b -> f x -> b)
-> forall (x :: Ctx CrucibleType). b -> Assignment f x -> b
foldlFC (\Bool
a (Ignore Bool
b) -> Bool
a Bool -> Bool -> Bool
&& Bool
b) Bool
True Assignment (Ignore Bool) ctx'
zipsame
           let newc :: c
newc = KildallForward ext blocks a c -> c -> c -> c
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> c -> c -> c
kfwd_club KildallForward ext blocks a c
analysis c
c c
oldc
           let same :: Bool
same = Bool
samex Bool -> Bool -> Bool
&& KildallForward ext blocks a c -> c -> c -> Bool
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> c -> c -> Bool
kfwd_csame KildallForward ext blocks a c
analysis c
oldc c
newc
           if Bool
same
               then Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall a.
a
-> StateT
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     Identity
     a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Set (Some (BlockID blocks))
forall a. Set a
Set.empty
               else do (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
-> StateT
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     Identity
     ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put (Assignment (KildallPair (Assignment a) c) blocks
x Assignment (KildallPair (Assignment a) c) blocks
-> (Assignment (KildallPair (Assignment a) c) blocks
    -> Assignment (KildallPair (Assignment a) c) blocks)
-> Assignment (KildallPair (Assignment a) c) blocks
forall a b. a -> (a -> b) -> b
& IndexF (Assignment (KildallPair (Assignment a) c) blocks) ctx'
-> Traversal'
     (Assignment (KildallPair (Assignment a) c) blocks)
     (IxValueF (Assignment (KildallPair (Assignment a) c) blocks) ctx')
forall k m (x :: k).
IxedF k m =>
IndexF m x -> Traversal' m (IxValueF m x)
forall (x :: Ctx CrucibleType).
IndexF (Assignment (KildallPair (Assignment a) c) blocks) x
-> Traversal'
     (Assignment (KildallPair (Assignment a) c) blocks)
     (IxValueF (Assignment (KildallPair (Assignment a) c) blocks) x)
ixF IndexF (Assignment (KildallPair (Assignment a) c) blocks) ctx'
Index blocks ctx'
idx ((IxValueF (Assignment (KildallPair (Assignment a) c) blocks) ctx'
  -> Identity (KildallPair (Assignment a) c ctx'))
 -> Assignment (KildallPair (Assignment a) c) blocks
 -> Identity (Assignment (KildallPair (Assignment a) c) blocks))
-> KildallPair (Assignment a) c ctx'
-> Assignment (KildallPair (Assignment a) c) blocks
-> Assignment (KildallPair (Assignment a) c) blocks
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Assignment a ctx' -> c -> KildallPair (Assignment a) c ctx'
forall k (a :: k -> Type) c (tp :: k).
a tp -> c -> KildallPair a c tp
KP Assignment a ctx'
new c
newc, a ret
r, c
rc)
                       Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall a.
a
-> StateT
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     Identity
     a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Some (BlockID blocks) -> Set (Some (BlockID blocks))
forall a. a -> Set a
Set.singleton (BlockID blocks ctx' -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks ctx'
tgt))



kildall_forward
  :: forall ext a c blocks ret init
   . KildallForward ext blocks a c
  -> CFG ext blocks init ret
  -> (Assignment a init, c)
  -> (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
kildall_forward :: forall ext (a :: CrucibleType -> Type) c
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (init :: Ctx CrucibleType).
KildallForward ext blocks a c
-> CFG ext blocks init ret
-> (Assignment a init, c)
-> (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
kildall_forward KildallForward ext blocks a c
analysis CFG ext blocks init ret
cfg (Assignment a init
asgn0,c
c0) =
    let initblk :: BlockID blocks init
initblk@(BlockID Index blocks init
idx) = CFG ext blocks init ret -> BlockID blocks init
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockID blocks init
cfgEntryBlockID CFG ext blocks init ret
cfg

        freshAsgn :: Ctx.Index blocks ctx -> Assignment a ctx
        freshAsgn :: forall (ctx :: Ctx CrucibleType).
Index blocks ctx -> Assignment a ctx
freshAsgn Index blocks ctx
i = (forall (x :: CrucibleType). TypeRepr x -> a x)
-> forall (x :: Ctx CrucibleType).
   Assignment TypeRepr x -> Assignment a 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 (\TypeRepr x
_ -> KildallForward ext blocks a c -> forall (tp :: CrucibleType). a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> forall (tp :: CrucibleType). a tp
kfwd_bot KildallForward ext blocks a c
analysis)
                             (Block ext blocks ret ctx -> Assignment TypeRepr ctx
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
blockInputs (BlockID blocks ctx
-> BlockMap ext blocks ret -> Block ext blocks ret ctx
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock (Index blocks ctx -> BlockID blocks ctx
forall (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType).
Index blocks tp -> BlockID blocks tp
BlockID Index blocks ctx
i) (CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
cfg)))

     in State
  (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) ()
-> (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
-> (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
forall s a. State s a -> s -> s
execState (Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) ()
loop (Some (BlockID blocks) -> Set (Some (BlockID blocks))
forall a. a -> Set a
Set.singleton (BlockID blocks init -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks init
initblk)))
                  ( Size blocks
-> (forall {tp :: Ctx CrucibleType}.
    Index blocks tp -> KildallPair (Assignment a) c tp)
-> Assignment (KildallPair (Assignment a) c) blocks
forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
Ctx.generate (BlockMap ext blocks ret -> Size blocks
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size (CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
cfg)) ((forall {tp :: Ctx CrucibleType}.
  Index blocks tp -> KildallPair (Assignment a) c tp)
 -> Assignment (KildallPair (Assignment a) c) blocks)
-> (forall {tp :: Ctx CrucibleType}.
    Index blocks tp -> KildallPair (Assignment a) c tp)
-> Assignment (KildallPair (Assignment a) c) blocks
forall a b. (a -> b) -> a -> b
$ \Index blocks tp
i ->
                      case Index blocks tp -> Index blocks init -> Maybe (tp :~: init)
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 tp
i Index blocks init
idx of
                        Just tp :~: init
Refl -> Assignment a tp -> c -> KildallPair (Assignment a) c tp
forall k (a :: k -> Type) c (tp :: k).
a tp -> c -> KildallPair a c tp
KP Assignment a init
Assignment a tp
asgn0 c
c0
                        Maybe (tp :~: init)
Nothing -> Assignment a tp -> c -> KildallPair (Assignment a) c tp
forall k (a :: k -> Type) c (tp :: k).
a tp -> c -> KildallPair a c tp
KP (Index blocks tp -> Assignment a tp
forall (ctx :: Ctx CrucibleType).
Index blocks ctx -> Assignment a ctx
freshAsgn Index blocks tp
i) (KildallForward ext blocks a c -> c
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> c
kfwd_cbot KildallForward ext blocks a c
analysis)
                  , KildallForward ext blocks a c -> forall (tp :: CrucibleType). a tp
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> forall (tp :: CrucibleType). a tp
kfwd_bot KildallForward ext blocks a c
analysis
                  , KildallForward ext blocks a c -> c
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c -> c
kfwd_cbot KildallForward ext blocks a c
analysis
                  )

  where visit :: Block ext blocks ret ctx
              -> (Assignment a ctx, c)
              -> Set (Some (BlockID blocks))
              -> State (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) ()
        visit :: forall (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx
-> (Assignment a ctx, c)
-> Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) ()
visit Block ext blocks ret ctx
blk (Assignment a ctx, c)
start Set (Some (BlockID blocks))
worklist = do
            Set (Some (BlockID blocks))
s <- KildallForward ext blocks a c
-> TypeRepr ret
-> Block ext blocks ret ctx
-> (Assignment a ctx, c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
forall ext (a :: CrucibleType -> Type) c
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
KildallForward ext blocks a c
-> TypeRepr ret
-> Block ext blocks ret ctx
-> (Assignment a ctx, c)
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     (Set (Some (BlockID blocks)))
kildall_transfer KildallForward ext blocks a c
analysis (CFG ext blocks init ret -> TypeRepr ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> TypeRepr ret
cfgReturnType CFG ext blocks init ret
cfg) Block ext blocks ret ctx
blk (Assignment a ctx, c)
start
            Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) ()
loop (Set (Some (BlockID blocks))
-> Set (Some (BlockID blocks)) -> Set (Some (BlockID blocks))
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Some (BlockID blocks))
s Set (Some (BlockID blocks))
worklist)

        loop :: Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) ()
loop Set (Some (BlockID blocks))
worklist =
           case Set (Some (BlockID blocks))
-> Maybe (Some (BlockID blocks), Set (Some (BlockID blocks)))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Some (BlockID blocks))
worklist of
              Maybe (Some (BlockID blocks), Set (Some (BlockID blocks)))
Nothing -> ()
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) ()
forall a.
a
-> StateT
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
     Identity
     a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
              Just (Some tgt :: BlockID blocks x
tgt@(BlockID Index blocks x
idx), Set (Some (BlockID blocks))
worklist') ->
                  do (Assignment (KildallPair (Assignment a) c) blocks
x,a ret
_,c
_) <- StateT
  (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
  Identity
  (Assignment (KildallPair (Assignment a) c) blocks, a ret, c)
forall s (m :: Type -> Type). MonadState s m => m s
get
                     let (KP Assignment a x
a c
c) = Assignment (KildallPair (Assignment a) c) blocks
x Assignment (KildallPair (Assignment a) c) blocks
-> Index blocks x -> KildallPair (Assignment a) c x
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index blocks x
idx
                         (Assignment a x
a',c
c') = KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType).
   BlockID blocks ctx
   -> (Assignment a ctx, c) -> (Assignment a ctx, c)
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (a :: CrucibleType -> Type) c.
KildallForward ext blocks a c
-> forall (ctx :: Ctx CrucibleType).
   BlockID blocks ctx
   -> (Assignment a ctx, c) -> (Assignment a ctx, c)
kfwd_onentry KildallForward ext blocks a c
analysis BlockID blocks x
tgt (Assignment a x
a,c
c)
                     Block ext blocks ret x
-> (Assignment a x, c)
-> Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) ()
forall (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx
-> (Assignment a ctx, c)
-> Set (Some (BlockID blocks))
-> State
     (Assignment (KildallPair (Assignment a) c) blocks, a ret, c) ()
visit (BlockID blocks x
-> BlockMap ext blocks ret -> Block ext blocks ret x
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
getBlock BlockID blocks x
tgt (CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
cfg)) (Assignment a x
a',c
c') Set (Some (BlockID blocks))
worklist'