Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

heapster-saw: Export block entry-point and implication error information for IDE ingestion #1442

Open
wants to merge 34 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
34 commits
Select commit Hold shift + click to select a range
3a9c13b
add basic IDE logging, start error cleanup
Jun 28, 2021
bfd0566
clean up additional implication errors
Jun 28, 2021
49f72e4
add structure to stmt fail in line with impl fail
Jun 29, 2021
716a2e1
redesign error message types, pipe through to log
Jul 7, 2021
9283f0e
fix default heapster environments missing ioref
Jul 8, 2021
1e427a4
carry more information through on most common implication error
Jul 9, 2021
059ab7b
Merge branch 'heapster-ide-info' of github.com:GaloisInc/saw-script i…
Jul 9, 2021
6fef67a
remove Some from error constructor
Jul 9, 2021
f3b76bb
Merge branch 'master' into heapster-ide-info
glguy Jul 26, 2021
e2c9cd6
Export valueperms in full json detail
glguy Jul 28, 2021
b59adb9
Avoid generating orphan ToJSON instances and using Given
glguy Jul 28, 2021
65ae7dd
refine jsonexport instances
glguy Jul 28, 2021
931d802
Document JSONExport
glguy Jul 28, 2021
2ad2225
Remove need for passing undefined
glguy Jul 30, 2021
ce3313b
JSONExport support for PermImpls
glguy Jul 30, 2021
df114c1
export entrypoint and caller ID information
Aug 12, 2021
8875708
cleanup imports, 80 char columns
Aug 12, 2021
5f12cc4
heapster: export function name for IDE
Aug 12, 2021
cb7c57c
heapster-saw: LogEntry with names and structure
glguy Aug 19, 2021
e768f1f
Incorporate names from bindings in JsonExport
glguy Aug 20, 2021
f60affd
Merge remote-tracking branch 'origin/master' into heapster-ide-info
glguy Aug 20, 2021
51665d7
Update PPInfo while exporting
glguy Aug 23, 2021
dc70b93
checkpoint
glguy Aug 27, 2021
f0c7747
Use types to generate names for pretty permissions where possible
glguy Aug 27, 2021
e634949
Checkpoint
glguy Aug 28, 2021
b284fc4
Checkpoint
glguy Aug 28, 2021
491c38f
Update cabal file
glguy Aug 30, 2021
4454faf
Merge branch 'master' into glguy/heapster-ide-info
Aug 30, 2021
3d0ae00
user the error prefix when logging errors for IDE
Aug 31, 2021
4e4cc4b
revert commented error prefix code
Aug 31, 2021
f60e26b
Change Mb' to NMb
glguy Aug 31, 2021
f34cabb
Merge branch 'glguy/heapster-ide-info' of github.com:GaloisInc/saw-sc…
glguy Aug 31, 2021
24d7122
Comments and more consistent naming
glguy Aug 31, 2021
2ac547b
Merge branch 'master' of github.com:GaloisInc/saw-script into heapste…
glguy Aug 31, 2021
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Change Mb' to NMb
  • Loading branch information
glguy committed Aug 31, 2021
commit f60e26b8a17b1824a9829771303e31c0e4ed8220
10 changes: 5 additions & 5 deletions heapster-saw/src/Verifier/SAW/Heapster/GenMonad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -111,12 +111,12 @@ gopenBinding f_ret mb_a =

-- | Name-binding in the generalized continuation monad (FIXME: explain)
gopenBinding' ::
(Mb' ctx (m b1) -> m r2) ->
Mb' ctx b2 ->
(NMb ctx (m b1) -> m r2) ->
NMb ctx b2 ->
GenStateContT s b1 s r2 m (RAssign Name ctx, b2)
gopenBinding' f_ret mb_a =
gcaptureCC \k ->
f_ret $ flip nuMultiWithElim1' mb_a $ \names a ->
f_ret $ flip nuMultiWithElim1N mb_a $ \names a ->
k (names, a)

-- | Name-binding in the generalized continuation monad (FIXME: explain)
Expand All @@ -129,9 +129,9 @@ startBinding tps f_ret = gcaptureCC (f_ret . nuMulti tps)
-- | Name-binding in the generalized continuation monad (FIXME: explain)
startBinding' ::
RAssign StringF ctx ->
(Mb' ctx (m r1) -> m r2) ->
(NMb ctx (m r1) -> m r2) ->
GenStateContT s r1 s r2 m (RAssign Name ctx)
startBinding' tps f_ret = gcaptureCC (f_ret . nuMulti' tps)
startBinding' tps f_ret = gcaptureCC (f_ret . nuMultiN tps)

addReader :: GenStateContT s1 r1 s2 r2 m a -> GenStateContT s1 r1 s2 r2 (ReaderT e m) a
addReader (GenStateContT m) =
Expand Down
8 changes: 4 additions & 4 deletions heapster-saw/src/Verifier/SAW/Heapster/IDESupport.hs
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ instance (PermCheckExtC ext)
=> ExtractLogEntries
(TypedEntry TransPhase ext blocks tops ret args ghosts) where
extractLogEntries te = do
let loc = mbLift' $ fmap getFirstProgramLocTS (typedEntryBody te)
let loc = nmbLift $ fmap getFirstProgramLocTS (typedEntryBody te)
withLoc loc (nmbExtractLogEntries (typedEntryBody te))
let entryId = mkLogEntryID $ typedEntryID te
let callers = callerIDs $ typedEntryCallers te
Expand Down Expand Up @@ -198,7 +198,7 @@ instance (PermCheckExtC ext)
mapM_ (\(Some te) -> extractLogEntries te) $ _typedBlockEntries tb

nmbExtractLogEntries
:: ExtractLogEntries a => Mb' (ctx :: RList CrucibleType) a -> ExtractionM ()
:: ExtractLogEntries a => NMb (ctx :: RList CrucibleType) a -> ExtractionM ()
nmbExtractLogEntries mb_a =
ReaderT $ \(ppi, loc, fname) ->
tell $ mbLift $ flip nuMultiWithElim1 (_mbBinding mb_a) $ \ns x ->
Expand Down Expand Up @@ -259,7 +259,7 @@ getFirstProgramLocBM block =
-> Maybe ProgramLoc
helper ste = case ste of
Some TypedEntry { typedEntryBody = stmts } ->
Just $ mbLift' $ fmap getFirstProgramLocTS stmts
Just $ nmbLift $ fmap getFirstProgramLocTS stmts

-- | From the sequence, get the first program location we encounter, which
-- should correspond to the permissions for the entry point we want to log
Expand All @@ -285,7 +285,7 @@ getFirstProgramLocMBPI
getFirstProgramLocMBPI MbPermImpls_Nil =
error "Error finding program location for IDE log"
getFirstProgramLocMBPI (MbPermImpls_Cons _ _ pis) =
mbLift' $ fmap getFirstProgramLocPI pis
nmbLift $ fmap getFirstProgramLocPI pis

-- | Print a `ProgramLoc` in a way that is useful for an IDE, i.e., machine
-- readable
Expand Down
44 changes: 22 additions & 22 deletions heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1361,7 +1361,7 @@ data MbPermImpls r bs_pss where
MbPermImpls_Nil :: MbPermImpls r RNil
MbPermImpls_Cons :: CruCtx bs ->
!(MbPermImpls r bs_pss) ->
!(Mb' bs (PermImpl r ps)) ->
!(NMb bs (PermImpl r ps)) ->
MbPermImpls r (bs_pss :> '(bs,ps))

-- | A local implication, from an input to an output permission set
Expand Down Expand Up @@ -1409,7 +1409,7 @@ permImplStep impl1@(Impl1_Fail _) mb_impls = PermImpl_Step impl1 mb_impls
-- Catch --> call the permImplCatch function
permImplStep Impl1_Catch ((MbPermImpls_Cons _
(MbPermImpls_Cons _ _ mb_pimpl1) mb_pimpl2)) =
permImplCatch (elimEmptyMb' mb_pimpl1) (elimEmptyMb' mb_pimpl2)
permImplCatch (elimEmptyNMb mb_pimpl1) (elimEmptyNMb mb_pimpl2)

-- Unary rules applied to failure --> failures
--
Expand Down Expand Up @@ -1519,12 +1519,12 @@ permImplCatch pimpl1@(PermImpl_Step (Impl1_Fail _) _) pimpl2 =
permImplCatch (PermImpl_Step Impl1_Catch
(MbPermImpls_Cons _
(MbPermImpls_Cons _ _ mb_pimpl_1a) mb_pimpl_1b)) pimpl2 =
permImplCatch (elimEmptyMb' mb_pimpl_1a) $
permImplCatch (elimEmptyMb' mb_pimpl_1b) pimpl2
permImplCatch (elimEmptyNMb mb_pimpl_1a) $
permImplCatch (elimEmptyNMb mb_pimpl_1b) pimpl2
permImplCatch pimpl1 pimpl2 =
PermImpl_Step Impl1_Catch $
MbPermImpls_Cons knownRepr (MbPermImpls_Cons knownRepr MbPermImpls_Nil $ emptyMb' pimpl1) $
emptyMb' pimpl2
MbPermImpls_Cons knownRepr (MbPermImpls_Cons knownRepr MbPermImpls_Nil $ emptyNMb pimpl1) $
emptyNMb pimpl2


-- | Test if a 'PermImpl' "succeeds", meaning there is at least one non-failing
Expand All @@ -1537,40 +1537,40 @@ permImplSucceeds (PermImpl_Done _) = 2
permImplSucceeds (PermImpl_Step (Impl1_Fail _) _) = 0
permImplSucceeds (PermImpl_Step Impl1_Catch
(MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2)) =
max (mbLift' $ fmap permImplSucceeds mb_impl1)
(mbLift' $ fmap permImplSucceeds mb_impl2)
max (nmbLift $ fmap permImplSucceeds mb_impl1)
(nmbLift $ fmap permImplSucceeds mb_impl2)
permImplSucceeds (PermImpl_Step (Impl1_Push _ _) (MbPermImpls_Cons _ _ mb_impl)) =
mbLift' $ fmap permImplSucceeds mb_impl
nmbLift $ fmap permImplSucceeds mb_impl
permImplSucceeds (PermImpl_Step (Impl1_Pop _ _) (MbPermImpls_Cons _ _ mb_impl)) =
mbLift' $ fmap permImplSucceeds mb_impl
nmbLift $ fmap permImplSucceeds mb_impl
permImplSucceeds (PermImpl_Step (Impl1_ElimOr _ _ _)
(MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2)) =
max (mbLift' (fmap permImplSucceeds mb_impl1))
(mbLift' (fmap permImplSucceeds mb_impl2))
max (nmbLift (fmap permImplSucceeds mb_impl1))
(nmbLift (fmap permImplSucceeds mb_impl2))
permImplSucceeds (PermImpl_Step (Impl1_ElimExists _ _)
(MbPermImpls_Cons _ _ mb_impl)) =
mbLift' $ fmap permImplSucceeds mb_impl
nmbLift $ fmap permImplSucceeds mb_impl
permImplSucceeds (PermImpl_Step (Impl1_Simpl _ _)
(MbPermImpls_Cons _ _ mb_impl)) =
mbLift' $ fmap permImplSucceeds mb_impl
nmbLift $ fmap permImplSucceeds mb_impl
permImplSucceeds (PermImpl_Step (Impl1_LetBind _ _)
(MbPermImpls_Cons _ _ mb_impl)) =
mbLift' $ fmap permImplSucceeds mb_impl
nmbLift $ fmap permImplSucceeds mb_impl
permImplSucceeds (PermImpl_Step (Impl1_ElimStructField _ _ _ _)
(MbPermImpls_Cons _ _ mb_impl)) =
mbLift' $ fmap permImplSucceeds mb_impl
nmbLift $ fmap permImplSucceeds mb_impl
permImplSucceeds (PermImpl_Step (Impl1_ElimLLVMFieldContents _ _)
(MbPermImpls_Cons _ _ mb_impl)) =
mbLift' $ fmap permImplSucceeds mb_impl
nmbLift $ fmap permImplSucceeds mb_impl
permImplSucceeds (PermImpl_Step (Impl1_ElimLLVMBlockToEq _ _)
(MbPermImpls_Cons _ _ mb_impl)) =
mbLift' $ fmap permImplSucceeds mb_impl
nmbLift $ fmap permImplSucceeds mb_impl
permImplSucceeds (PermImpl_Step Impl1_BeginLifetime
(MbPermImpls_Cons _ _ mb_impl)) =
mbLift' $ fmap permImplSucceeds mb_impl
nmbLift $ fmap permImplSucceeds mb_impl
permImplSucceeds (PermImpl_Step (Impl1_TryProveBVProp _ _ _)
(MbPermImpls_Cons _ _ mb_impl)) =
mbLift' $ fmap permImplSucceeds mb_impl
nmbLift $ fmap permImplSucceeds mb_impl

-- | Test if a 'PermImpl' fails, meaning 'permImplSucceeds' returns 0
permImplFails :: PermImpl r ps -> Bool
Expand Down Expand Up @@ -2651,7 +2651,7 @@ instance (NuMatchingAny1 r, SubstVar PermVarSubst m,
[nuMP| MbPermImpls_Nil |] -> return MbPermImpls_Nil
[nuMP| MbPermImpls_Cons mpx mb_impl mb_impls' |] ->
let px = mbLift mpx in
MbPermImpls_Cons px <$> genSubst s mb_impl <*> genSubstMb' (cruCtxProxies px) s mb_impls'
MbPermImpls_Cons px <$> genSubst s mb_impl <*> genSubstNMb (cruCtxProxies px) s mb_impls'

-- FIXME: shouldn't need the SubstVar PermVarSubst m assumption...
instance SubstVar PermVarSubst m =>
Expand Down Expand Up @@ -3079,7 +3079,7 @@ implApplyImpl1 impl1 mb_ms =
helper MbPermSets_Nil _ = gabortM (return MbPermImpls_Nil)
helper (MbPermSets_Cons mbperms ctx mbperm) (args :>: Impl1Cont f) =
state (\s -> s & implStatePPInfo %%~ ppInfoAllocateTypedExprNames ctx) >>>= \n ->
gparallel (\m1 m2 -> MbPermImpls_Cons ctx <$> m1 <*> (Mb' n <$> m2))
gparallel (\m1 m2 -> MbPermImpls_Cons ctx <$> m1 <*> (NMb n <$> m2))
(helper mbperms args)
(gopenBinding strongMbM mbperm >>>= \(ns, perms') ->
gmodify (set implStatePerms perms' .
Expand Down
2 changes: 1 addition & 1 deletion heapster-saw/src/Verifier/SAW/Heapster/JSONExport.hs
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ instance JsonExport a => JsonExport (Mb (ctx :: RList CrucibleType) a) where
("body", jsonExport body)
]

instance JsonExport a => JsonExport (Mb' (ctx :: RList CrucibleType) a) where
instance JsonExport a => JsonExport (NMb (ctx :: RList CrucibleType) a) where
jsonExport mb = mbLift $ flip nuMultiWithElim1 (_mbBinding mb) $ \names body ->
let ?ppi = ppInfoApplyAllocation names (_mbNames mb) ?ppi in
object [
Expand Down
51 changes: 24 additions & 27 deletions heapster-saw/src/Verifier/SAW/Heapster/NamedMb.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,53 +14,50 @@ import Control.Lens

newtype StringF a = StringF { unStringF :: String }

type Binding' c = Mb' (RNil :> c)
type Binding' c = NMb (RNil :> c)

data Mb' ctx a = Mb'
data NMb ctx a = NMb
{ _mbNames :: RAssign StringF ctx
, _mbBinding :: Mb ctx a
}
deriving Functor

mbBinding :: Lens (Mb' ctx a) (Mb' ctx b) (Mb ctx a) (Mb ctx b)
mbBinding f x = Mb' (_mbNames x) <$> f (_mbBinding x)
mbBinding :: Lens (NMb ctx a) (NMb ctx b) (Mb ctx a) (Mb ctx b)
mbBinding f x = NMb (_mbNames x) <$> f (_mbBinding x)

nuMulti' :: RAssign StringF ctx -> (RAssign Name ctx -> b) -> Mb' ctx b
nuMulti' tps f = Mb'
nuMultiN :: RAssign StringF ctx -> (RAssign Name ctx -> b) -> NMb ctx b
nuMultiN tps f = NMb
{ _mbNames = tps
, _mbBinding = nuMulti (mapRAssign (const Proxy) tps) f
}

nuMultiWithElim1' :: (RAssign Name ctx -> arg -> b) -> Mb' ctx arg -> Mb' ctx b
nuMultiWithElim1' = over mbBinding . nuMultiWithElim1
nuMultiWithElim1N :: (RAssign Name ctx -> arg -> b) -> NMb ctx arg -> NMb ctx b
nuMultiWithElim1N = over mbBinding . nuMultiWithElim1

strongMbM' :: MonadStrongBind m => Mb' ctx (m a) -> m (Mb' ctx a)
strongMbM' = traverseOf mbBinding strongMbM
strongNMbM :: MonadStrongBind m => NMb ctx (m a) -> m (NMb ctx a)
strongNMbM = traverseOf mbBinding strongMbM

mbM' :: (MonadBind m, NuMatching a) => Mb' ctx (m a) -> m (Mb' ctx a)
mbM' = traverseOf mbBinding mbM
nmbM :: (MonadBind m, NuMatching a) => NMb ctx (m a) -> m (NMb ctx a)
nmbM = traverseOf mbBinding mbM

mbSwap' :: RAssign Proxy ctx -> Mb' ctx' (Mb' ctx a) -> Mb' ctx (Mb' ctx' a)
mbSwap' p (Mb' names' body') = Mb' names' <$> mbSink p body'
nmbSwap :: RAssign Proxy ctx -> NMb ctx' (NMb ctx a) -> NMb ctx (NMb ctx' a)
nmbSwap p (NMb names' body') = NMb names' <$> nmbSink p body'

mbSink :: RAssign Proxy ctx -> Mb ctx' (Mb' ctx a) -> Mb' ctx (Mb ctx' a)
mbSink p m =
Mb'
nmbSink :: RAssign Proxy ctx -> Mb ctx' (NMb ctx a) -> NMb ctx (Mb ctx' a)
nmbSink p m =
NMb
{ _mbNames = mbLift (_mbNames <$> m)
, _mbBinding = mbSwap p (_mbBinding <$> m)
}

mbCombine' :: RAssign Proxy c2 -> Mb' c1 (Mb' c2 a) -> Mb' (c1 :++: c2) a
mbCombine' = undefined
nmbLift :: Liftable a => NMb ctx a -> a
nmbLift = views mbBinding mbLift

mbLift' :: Liftable a => Mb' ctx a -> a
mbLift' = views mbBinding mbLift
elimEmptyNMb :: NMb RNil a -> a
elimEmptyNMb = views mbBinding elimEmptyMb

elimEmptyMb' :: Mb' RNil a -> a
elimEmptyMb' = views mbBinding elimEmptyMb

emptyMb' :: a -> Mb' RNil a
emptyMb' = Mb' MNil . emptyMb
emptyNMb :: a -> NMb RNil a
emptyNMb = NMb MNil . emptyMb

mkNuMatching [t| forall a. StringF a |]
instance NuMatchingAny1 StringF where
Expand All @@ -72,4 +69,4 @@ instance Liftable (StringF a) where
instance LiftableAny1 StringF where
mbLiftAny1 = mbLift

mkNuMatching [t| forall ctx a. NuMatching a => Mb' ctx a |]
mkNuMatching [t| forall ctx a. NuMatching a => NMb ctx a |]
30 changes: 15 additions & 15 deletions heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4426,7 +4426,7 @@ distPermsTail =
-- | The lens for the nth permission in a 'DistPerms' stack
nthVarPerm :: Member ps a -> ExprVar a -> Lens' (DistPerms ps) (ValuePerm a)
nthVarPerm Member_Base x = distPermsHead x
nthVarPerm (Member_Step memb') x = distPermsTail . nthVarPerm memb' x
nthVarPerm (Member_Step meNMb) x = distPermsTail . nthVarPerm meNMb x

-- | Test if a permission can be copied, i.e., whether @p -o p*p@. This is true
-- iff @p@ does not contain any 'Write' modalities, any frame permissions, or
Expand Down Expand Up @@ -4967,27 +4967,27 @@ genSubstMb ::
s ctx' -> Mb ctx' (Mb ctx a) -> m (Mb ctx a)
genSubstMb p s mbmb = mbM (fmap (genSubst s) (mbSwap p mbmb))

genSubstMb' ::
genSubstNMb ::
Substable s a m =>
NuMatching a =>
RAssign Proxy ctx ->
s ctx' -> Mb ctx' (Mb' ctx a) -> m (Mb' ctx a)
genSubstMb' p s mbmb = mbM' (fmap (genSubst s) (swapHelper p mbmb))
s ctx' -> Mb ctx' (NMb ctx a) -> m (NMb ctx a)
genSubstNMb p s mbmb = nmbM (fmap (genSubst s) (swapHelper p mbmb))

swapHelper :: RAssign Proxy b -> Mb a (Mb' b c) -> Mb' b (Mb a c)
swapHelper p m = Mb' ns (mbSwap p bs)
swapHelper :: RAssign Proxy b -> Mb a (NMb b c) -> NMb b (Mb a c)
swapHelper p m = NMb ns (mbSwap p bs)
where
ns = mbLift (fmap _mbNames m)
bs = fmap _mbBinding m

instance {-# INCOHERENT #-} (Given (RAssign Proxy ctx), Substable s a m, NuMatching a) => Substable s (Mb' ctx a) m where
genSubst = genSubstMb' given
instance {-# INCOHERENT #-} (Given (RAssign Proxy ctx), Substable s a m, NuMatching a) => Substable s (NMb ctx a) m where
genSubst = genSubstNMb given

instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Mb' RNil a) m where
genSubst = genSubstMb' RL.typeCtxProxies
instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (NMb RNil a) m where
genSubst = genSubstNMb RL.typeCtxProxies

instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Binding' c a) m where
genSubst = genSubstMb' RL.typeCtxProxies
genSubst = genSubstNMb RL.typeCtxProxies


instance SubstVar s m => Substable s (Member ctx a) m where
Expand Down Expand Up @@ -5626,8 +5626,8 @@ instance AbstractVars (Name (a :: CrucibleType)) where
abstractPEVars ns1 ns2 (n :: Name a)
| Just memb <- memberElem n ns2
= return ( $(mkClosed
[| \prxs1 prxs2 memb' ->
nuMulti prxs1 (const $ nuMulti prxs2 (RL.get memb')) |])
[| \prxs1 prxs2 meNMb ->
nuMulti prxs1 (const $ nuMulti prxs2 (RL.get meNMb)) |])
`clApply` closedProxies ns1 `clApply` closedProxies ns2
`clApply` toClosed memb)
abstractPEVars _ _ _ = Nothing
Expand All @@ -5636,9 +5636,9 @@ instance AbstractVars (Name (a :: Type)) where
abstractPEVars ns1 ns2 (n :: Name a)
| Just memb <- memberElem n ns1
= return ( $(mkClosed
[| \prxs1 prxs2 memb' ->
[| \prxs1 prxs2 meNMb ->
nuMulti prxs1 $ \ns ->
nuMulti prxs2 (const $ RL.get memb' ns) |])
nuMulti prxs2 (const $ RL.get meNMb ns) |])
`clApply` closedProxies ns1 `clApply` closedProxies ns2
`clApply` toClosed memb)
abstractPEVars _ _ _ = Nothing
Expand Down
14 changes: 7 additions & 7 deletions heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs
Original file line number Diff line number Diff line change
Expand Up @@ -760,7 +760,7 @@ data TypedStmtSeq ext blocks tops ret ps_in where
TypedConsStmt :: !ProgramLoc ->
!(TypedStmt ext rets ps_in ps_next) ->
!(RAssign Proxy rets) ->
!(Mb' rets (TypedStmtSeq ext blocks tops ret ps_next)) ->
!(NMb rets (TypedStmtSeq ext blocks tops ret ps_next)) ->
TypedStmtSeq ext blocks tops ret ps_in

-- | Typed version of 'TermStmt', which terminates the current block
Expand Down Expand Up @@ -1209,7 +1209,7 @@ data TypedEntry phase ext blocks tops ret args ghosts =
typedEntryPermsOut :: !(MbValuePerms (tops :> ret)),
-- | The type-checked body of the entrypoint
typedEntryBody :: !(TransData phase
(Mb' ((tops :++: args) :++: ghosts)
(NMb ((tops :++: args) :++: ghosts)
(TypedStmtSeq ext blocks tops ret
((tops :++: args) :++: ghosts))))
}
Expand Down Expand Up @@ -1939,7 +1939,7 @@ runPermCheckM ::
DistPerms ((tops :++: args) :++: ghosts) ->
PermCheckM ext cblocks blocks tops ret () ps_out r ((tops :++: args)
:++: ghosts) ()) ->
TopPermCheckM ext cblocks blocks tops ret (Mb' ((tops :++: args) :++: ghosts) r)
TopPermCheckM ext cblocks blocks tops ret (NMb ((tops :++: args) :++: ghosts) r)
runPermCheckM names entryID args ghosts mb_perms_in m =
get >>= \(TopPermCheckState {..}) ->
let args_prxs = cruCtxProxies args
Expand All @@ -1951,8 +1951,8 @@ runPermCheckM names entryID args ghosts mb_perms_in m =
z <- state (allocateDebugNames' (Just "ghost") (noNames' ghosts) ghosts)
pure (x `rappend` y `rappend` z)
in
liftInnerToTopM $ strongMbM' $
flip nuMultiWithElim1' (Mb' dbgs (mbValuePermsToDistPerms mb_perms_in)) $ \ns perms_in ->
liftInnerToTopM $ strongNMbM $
flip nuMultiWithElim1N (NMb dbgs (mbValuePermsToDistPerms mb_perms_in)) $ \ns perms_in ->
let (tops_args, ghosts_ns) = RL.split Proxy ghosts_prxs ns
(tops_ns, args_ns) = RL.split Proxy args_prxs tops_args
st1 = emptyPermCheckState (distPermSet perms_in) tops_ns entryID local_names
Expand Down Expand Up @@ -2596,7 +2596,7 @@ emitStmt ::
emitStmt tps names loc stmt =
let pxys = cruCtxProxies tps in
allocateDebugNames Nothing names tps >>>= \debugs ->
startBinding' debugs (fmap (TypedConsStmt loc stmt pxys) . strongMbM') >>>= \ns ->
startBinding' debugs (fmap (TypedConsStmt loc stmt pxys) . strongNMbM) >>>= \ns ->
modify (\st -> st { stPPInfo = ppInfoApplyAllocation ns debugs (stPPInfo st)}) >>>
setVarTypes ns tps >>>
gmodify (modifySTCurPerms (applyTypedStmt stmt ns)) >>>
Expand Down Expand Up @@ -3982,7 +3982,7 @@ tcBlockEntryBody ::
Block ext cblocks ret args ->
TypedEntry TCPhase ext blocks tops ret (CtxToRList args) ghosts ->
TopPermCheckM ext cblocks blocks tops ret
(Mb' ((tops :++: CtxToRList args) :++: ghosts)
(NMb ((tops :++: CtxToRList args) :++: ghosts)
(TypedStmtSeq ext blocks tops ret ((tops :++: CtxToRList args) :++: ghosts)))
tcBlockEntryBody names blk entry@(TypedEntry {..}) =
runPermCheckM names typedEntryID typedEntryArgs typedEntryGhosts typedEntryPermsIn $
Expand Down