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

Use itree SpecM monad instead of CompM in Heapster #1778

Merged
merged 93 commits into from
Dec 10, 2022
Merged
Changes from 1 commit
Commits
Show all changes
93 commits
Select commit Hold shift + click to select a range
661c442
began defining SpecM in Prelude.sawcore
lag47 Jul 12, 2022
f852a35
added some SpecM definitions
lag47 Jul 19, 2022
cba7658
wrote new interface for SpecM
lag47 Jul 22, 2022
7f1b785
fixed haddock syntax errors
lag47 Jul 29, 2022
b501146
further refactored SpecM
lag47 Aug 5, 2022
6e783f7
partially rewrote saw translation
Aug 16, 2022
92fb1f9
new draft of multiFixS function signature
Aug 17, 2022
1e8e7b3
refactored MultiFixSBodiesS
lag47 Aug 19, 2022
211fac9
implementing SAW functions
lag47 Aug 22, 2022
bed9ee8
updated documentation
lag47 Aug 24, 2022
f0a4895
Merge branch 'master' into heapster-itree
Aug 25, 2022
0e5bd0e
updated the SAW core prelude with the new versions of the SpecM opera…
Aug 26, 2022
be309ca
Added VoidEvRetType for defining the evRetType of a Void to the SAW c…
Aug 26, 2022
8b6a93c
renamed CallS to callS
Aug 31, 2022
f195a8f
added the more general identOpenTerm
Aug 31, 2022
4ecf85d
partially finished changing the translation to generate SpecM computa…
Aug 31, 2022
3eea089
almost done changing the translation to generate SpecM computations i…
Sep 1, 2022
b5eb9f1
got the new translation to SpecM to compile, yay!
Sep 2, 2022
c434a4c
fixed some small bugs in the SAW core translation
Sep 2, 2022
a074cbc
changed more of the CompM operations in the translation to use the co…
Sep 6, 2022
3d90681
fixed the type of errorS
Sep 6, 2022
fbbc4c3
added translations for the SpecM operations
Sep 6, 2022
4e0c3f9
updated sawLet to use sort 1 instead of sort 0
Sep 6, 2022
0b2d854
whoops, updated the SAW translation to use retS instead of returnS
Sep 6, 2022
c5d8962
fixed up references to EnTree specs
Sep 7, 2022
9a596bb
Merge branch 'master' into heapster-itree
Oct 4, 2022
f355421
changed the SpecM monad to be a sort 0 instead of a sort 1
Oct 5, 2022
bebfce2
Merge branch 'master' into heapster-itree
Oct 6, 2022
48f53a5
removed the old LetRecType1 type, and updated LetRecType to reference…
Oct 6, 2022
13d26b9
changed some uses of errorM to errorS; added a workaround for issue #…
Oct 6, 2022
4af67c3
replaced uses of LetRecTypes with List1 LetRecType in the SpecM stuff…
Oct 6, 2022
354f285
Merge branch 'master' into heapster-itree
Oct 6, 2022
a991178
removed workaround for issue #1748
Oct 6, 2022
9b19195
fixed mallocSpec in the linked list example to use a SpecM type
Oct 6, 2022
6ad6fa5
changed the translation of functions to always use the empty FunStack
Oct 8, 2022
fb7e632
whoops, fixed Prelude.EmptyFunStack to the correct Prelude.emptyFunStack
Oct 11, 2022
00e56cb
fixed some examples to use SpecM instead of CompM
Oct 11, 2022
7ed4c4a
fixed the translations of lowned rules to always use the empty FunStack
Oct 11, 2022
49ecbb1
updated all examples to work with the new SpecM monad
Oct 12, 2022
e172e9a
Changed SpecM to take in a single EvType argument instead of two sepa…
Oct 12, 2022
4a07629
added QuantType instances to SAWCoreScaffolding.v
Oct 13, 2022
620c5f8
moved QuantType instances to a new file, SpecMExtra.v; updated the tr…
Oct 13, 2022
bec4e69
updated mbox example to work with the new translation
Oct 13, 2022
085e608
updated examples to use the new VoidEv single argument instead of the…
Oct 13, 2022
eafdee7
updated the Prelude to the new definitions of CallS and MultiFixS
Oct 20, 2022
c269957
Updated to the new version of the CallS and MultiFixS combinators, th…
Oct 21, 2022
c81daf7
added SpecM versions of mapBVVecM and appendCastBVVecM, and updated t…
Nov 3, 2022
da763a5
whoops, forgot to change appendCastBVVecM in one spot in the translation
Nov 3, 2022
54c7e58
whoops, forgot to change mapBVVecM to mapBVVecS
Nov 3, 2022
d973782
first try at entree is_elem_spec_ref
m-yac Nov 8, 2022
ea28b0b
update mbox_proofs header with entrees
m-yac Nov 9, 2022
83f4ddc
Merge branch 'master' into heapster-itree
Nov 11, 2022
91954fc
get mbox_free_chain_spec_ref working
m-yac Nov 16, 2022
409b1bb
prove mbox_concat/mbox_concat_chains_spec_ref
m-yac Nov 17, 2022
5cd47ad
add alternate mbox_concat_chains_spec_ref
m-yac Nov 17, 2022
366c077
add mbox_detach_spec_ref
m-yac Nov 17, 2022
d540e52
add mbox_drop_spec_ref
m-yac Nov 17, 2022
9c609ab
fixed up mbox proofs to work with updated entree-specs automation
Nov 18, 2022
a361a65
Revert "fixed up mbox proofs to work with updated entree-specs automa…
m-yac Nov 18, 2022
3e6e12b
Proofs for mbox_len
RyanGlScott Nov 18, 2022
80f8565
Merge branch 'heapster-itree' of https://github.com/GaloisInc/saw-scr…
m-yac Nov 18, 2022
41e5a5b
update proofs with latest automation
m-yac Nov 18, 2022
bf26c67
Merge branch 'master' into heapster-itree
Nov 18, 2022
aec2ac4
add maybe automation, start on mbox_randomize
m-yac Nov 18, 2022
63b3a79
Make mbox_len_spec_ref* proofs work with latest entree-specs
RyanGlScott Nov 22, 2022
0e1e995
mbox_copy_spec_ref
RyanGlScott Nov 23, 2022
183e923
Another way to prove mbox_copy, beginnings of mbox_copy_chain
RyanGlScott Nov 23, 2022
031d9a4
update proofs with latest ex and shelve automation
m-yac Nov 24, 2022
c1f05e6
Simplify mbox_copy_spec_ref__alt slightly, some progress on mbox_copy…
RyanGlScott Nov 27, 2022
03fb5d0
update mbox auto with change to 999 RelGoal hint
m-yac Nov 28, 2022
7c40584
don't greedily destruct Mboxes for now
m-yac Nov 28, 2022
f73203a
More progress on mbox_copy_chain and mbox_split_at
RyanGlScott Nov 29, 2022
faaa363
add timing commands
m-yac Nov 29, 2022
64b1355
update proofs with less `cbn`s change
m-yac Nov 29, 2022
269f3e5
add sawLet automation
m-yac Nov 29, 2022
aba8237
mbox_split_at_spec_ref is proven!
RyanGlScott Nov 29, 2022
4759cd2
More progress on mbox_copy_chain
RyanGlScott Nov 29, 2022
ab0e39c
use eithers instead of either, update proofs
m-yac Nov 30, 2022
26f44ac
added heapster_set_event_type command, along with the io example to u…
Nov 30, 2022
0e9eed5
Merge branch 'heapster-itree' of github.com:GaloisInc/saw-script into…
Nov 30, 2022
290db7e
Complete proof of mbox_copy_chain
RyanGlScott Nov 30, 2022
e4a40b3
mbox_detach_from_end proofs
RyanGlScott Nov 30, 2022
fac87aa
prove mbox_randomize_spec_ref
m-yac Dec 1, 2022
ac18311
small tweaks to the hello world example
Dec 2, 2022
1a077f4
Merge branch 'heapster-itree' of github.com:GaloisInc/saw-script into…
Dec 2, 2022
c862d47
translateCurryLocalPermImpl: Don't force the use of an EmptyFunStack
RyanGlScott Dec 8, 2022
c2385cc
clean up + update mbox_proofs, linked_list_proofs
m-yac Dec 9, 2022
2f1d08b
get `make` passing (rust typechecking fails)
m-yac Dec 9, 2022
bbac0b2
Merge branch 'master' into heapster-itree
m-yac Dec 9, 2022
eabdf2d
Merge branch 'master' into heapster-itree
RyanGlScott Dec 9, 2022
d2d9f01
Install entree-specs as a Coq dependency
RyanGlScott Dec 9, 2022
b91d94e
update proofs with latest changes to saw-core-coq
m-yac Dec 9, 2022
52eca30
incorperate Haddock suggestions from @RyanGlScott
m-yac Dec 9, 2022
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
got the new translation to SpecM to compile, yay!
Eddy Westbrook committed Sep 2, 2022
commit b5eb9f16ab1ea37f42d6c7bc5e5cf3126c4834f3
18 changes: 18 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
Original file line number Diff line number Diff line change
@@ -2543,6 +2543,16 @@ pattern ValPerm_LLVMBlockShape sh <- ValPerm_Conj [Perm_LLVMBlockShape sh]
where
ValPerm_LLVMBlockShape sh = ValPerm_Conj [Perm_LLVMBlockShape sh]

-- | The conjunction of exactly 1 @llvmfunptr@ permission
pattern ValPerm_LLVMFunPtr :: () =>
(a ~ LLVMPointerType w, 1 <= w, KnownNat w) =>
TypeRepr (FunctionHandleType cargs ret) ->
ValuePerm (FunctionHandleType cargs ret) ->
ValuePerm a
pattern ValPerm_LLVMFunPtr tp p <- ValPerm_Conj [Perm_LLVMFunPtr tp p]
where
ValPerm_LLVMFunPtr tp p = ValPerm_Conj [Perm_LLVMFunPtr tp p]

-- | A single @lowned@ permission
pattern ValPerm_LOwned :: () => (a ~ LifetimeType) => [PermExpr LifetimeType] ->
CruCtx ps_in -> CruCtx ps_out ->
@@ -2585,6 +2595,14 @@ pattern ValPerm_Struct ps <- ValPerm_Conj [Perm_Struct ps]
pattern ValPerm_Any :: ValuePerm a
pattern ValPerm_Any = ValPerm_Conj [Perm_Any]

-- | A single function permission
pattern ValPerm_Fun :: () => (a ~ FunctionHandleType cargs ret) =>
FunPerm ghosts (CtxToRList cargs) gouts ret ->
ValuePerm a
pattern ValPerm_Fun fun_perm <- ValPerm_Conj [Perm_Fun fun_perm]
where
ValPerm_Fun fun_perm = ValPerm_Conj [Perm_Fun fun_perm]

pattern ValPerms_Nil :: () => (tps ~ RNil) => ValuePerms tps
pattern ValPerms_Nil = MNil

183 changes: 94 additions & 89 deletions heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
Original file line number Diff line number Diff line change
@@ -78,10 +78,6 @@ import Verifier.SAW.Heapster.Implication
import Verifier.SAW.Heapster.TypedCrucible

import GHC.Stack
import qualified Verifier.SAW.Prelude as Prelude
import GHC.Event (Event)
import Lang.Crucible.Simulator.CallFrame (frameBlockID)
import Data.Type.RList (mapRAssign)


-- | FIXME: document and move to Hobbits
@@ -717,14 +713,6 @@ instance (Translate info ctx a tr, NuMatching a) =>
Translate info ctx [a] [tr] where
translate = mapM translate . mbList

-- |- computes the application of a @SpecM@ function, i.e. @retS@, @bindS@, to given arguments,
-- automatically supplying the arguments for for event type, event encoding, and function stack
applyMultiSpecMTransM :: Ident -> [TypeTransM ctx OpenTerm] -> TypeTransM ctx OpenTerm
applyMultiSpecMTransM name args =
applyMultiTransM (return $ globalOpenTerm name) $
[askttiEventType, askttiEventEncoding, askttiFunStack] ++
args


----------------------------------------------------------------------
-- * Translating Types
@@ -884,10 +872,19 @@ lambdaExprCtx ctx m =
lambdaTransM "e" tptrans (\ectx -> inCtxTransM ectx m)

-- | Translate all types in a Crucible context and pi-abstract over them
piExprCtx :: TransInfo info => CruCtx ctx2 ->
TransM info (ctx :++: ctx2) OpenTerm ->
TransM info ctx OpenTerm
piExprCtx :: TransInfo info => CruCtx ctx ->
TransM info ctx OpenTerm ->
TransM info RNil OpenTerm
piExprCtx ctx m =
translateClosed ctx >>= \tptrans ->
piTransM "e" tptrans (\ectx -> inCtxTransM ectx m)

-- | Like 'piExprCtx' but append the newly bound variables to the current
-- context, rather than running in the empty context
piExprCtxApp :: TransInfo info => CruCtx ctx2 ->
TransM info (ctx :++: ctx2) OpenTerm ->
TransM info ctx OpenTerm
piExprCtxApp ctx m =
translateClosed ctx >>= \tptrans ->
piTransM "e" tptrans (\ectx -> inExtMultiTransM ectx m)

@@ -1989,7 +1986,7 @@ instance TransInfo info =>
case RL.appendAssoc ctx tops_prxs rets_prxs of
Refl ->
-- FIXME HERE NOW: change to SpecM
piExprCtx tops $
piExprCtxApp tops $
piPermCtx (mbCombine tops_prxs perms_in) $ \_ ->
applyTransM (return $ globalOpenTerm "Prelude.CompM") $
translateRetType rets $
@@ -2145,7 +2142,7 @@ impTransM :: forall ctx ps ext blocks tops rets a.
ImpTransM ext blocks tops rets ps ctx a ->
TypeTransM ctx a
impTransM pvars pctx mapTrans stack retType =
withInfoM $ \(TypeTransInfo ectx penv pflag evctx) ->
withInfoM $ \(TypeTransInfo ectx penv pflag) ->
ImpTransInfo { itiExprCtx = ectx,
itiPermCtx = RL.map (const $ PTrans_True) ectx,
itiPermStack = pctx,
@@ -2162,7 +2159,7 @@ impTransM pvars pctx mapTrans stack retType =
tpTransM :: TypeTransM ctx a -> ImpTransM ext blocks tops rets ps ctx a
tpTransM =
withInfoM (\(ImpTransInfo {..}) ->
TypeTransInfo itiExprCtx itiPermEnv itiChecksFlag itiEntreeEventType)
TypeTransInfo itiExprCtx itiPermEnv itiChecksFlag)

-- | Run an implication translation computation in an "empty" environment, where
-- there are no variables in scope and no permissions held anywhere
@@ -4472,7 +4469,7 @@ translateStmt loc mb_stmt m = case mbMatch mb_stmt of
ectx_outer <- itiExprCtx <$> ask
funStack <- itiFunStack <$> ask
let (f, rec_p) = case f_trans of
PTrans_Conj [APTrans_Fun _ rec_p f_trm] -> (f_trm, rec_p)
PTrans_Conj [APTrans_Fun _ rec_p' f_trm] -> (f_trm, rec_p')
_ -> error "translateStmt: TypedCall: unexpected function permission"
let rets = mbLift $ mbMapCl $(mkClosed [| funPermRets |]) fun_perm
let rets_prxs = cruCtxProxies rets
@@ -4641,22 +4638,23 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
withKnownNat ?ptrWidth $
inExtTransM ETrans_LLVM $
do env <- infoEnv <$> ask
ptrans <- translate $ extMb p
let w :: NatRepr w = knownRepr
case lookupGlobalSymbol env (mbLift gsym) w of
Nothing -> error ("translateLLVMStmt: TypedLLVMResolveGlobal: "
++ " no translation of symbol "
++ globalSymbolName (mbLift gsym))
Just (_, True, [t])
| [nuP| Perm_LLVMFunPtr fun_tp (Perm_Fun fun_perm) |] <- p ->
let p = PTrans_Conj [APTrans_LLVMFunPtr (mbLift fun_tp) $
APTrans_Fun fun_perm True t] in
withPermStackM (:>: Member_Base) (:>: p) m
| [nuP| ValPerm_LLVMFunPtr fun_tp (ValPerm_Fun fun_perm) |] <- p ->
let ptrans = PTrans_Conj [APTrans_LLVMFunPtr (mbLift fun_tp) $
PTrans_Conj [APTrans_Fun
fun_perm True t]] in
withPermStackM (:>: Member_Base) (:>: extPermTrans ptrans) m
Just (_, True, _) ->
error ("translateLLVMStmt: TypedLLVMResolveGlobal: "
++ " unexpected recursive call translation for symbol "
++ globalSymbolName (mbLift gsym))
Just (_, False, ts) ->
translate (extMb p) >>= \ptrans ->
withPermStackM (:>: Member_Base) (:>: typeTransF ptrans ts) m

[nuMP| TypedLLVMIte _ mb_r1 _ _ |] ->
@@ -4807,15 +4805,17 @@ translateEntryLRT env entry@(TypedEntry {..}) =
-- entrypoints in a 'TypedBlockMap' that will be bound as recursive functions
translateBlockMapLRTs :: PermEnv ->
TypedBlockMap TransPhase ext blocks tops rets ->
TypeTransM ctx [OpenTerm]
translateBlockMapLRTs env = mapBlockMapLetRec (translateEntryLRT env)
[OpenTerm]
translateBlockMapLRTs env blkMap =
mapBlockMapLetRec (translateEntryLRT env) blkMap

-- | Return a @LetRecType1@ value for the translation of the function permission
-- of a CFG
translateCFGInitLRT :: PermEnv -> TypedCFG ext blocks ghosts inits gouts ret ->
OpenTerm
translateCFGInitLRT env (tpcfgFunPerm ->
(FunPerm ghosts args gouts ret perms_in perms_out)) =
translateCFGInitEntryLRT :: PermEnv ->
TypedCFG ext blocks ghosts inits gouts ret ->
OpenTerm
translateCFGInitEntryLRT env (tpcfgFunPerm ->
(FunPerm ghosts args gouts ret perms_in perms_out)) =
runNilTypeTransM env noChecks $
translateClosed (appendCruCtx ghosts args) >>= \ctx_trans ->
piLRTTransM "arg" ctx_trans $ \ectx ->
@@ -4829,17 +4829,17 @@ translateCFGInitLRT env (tpcfgFunPerm ->
translateCFGLRTs :: PermEnv -> TypedCFG ext blocks ghosts inits gouts ret ->
[OpenTerm]
translateCFGLRTs env cfg =
translateCFGInitEntryLRT env cfg : translateBlockMapLRTs (tpcfgBlockMap cfg)
translateCFGInitEntryLRT env cfg :
translateBlockMapLRTs env (tpcfgBlockMap cfg)


-- | Apply the @callS@ operation to a recursive function stack, top-level frame
-- of recursive functions, and natural number index @i@ into that frame, to get
-- a call to the @i@th function in that frame
applyCallS :: OpenTerm -> OpenTerm -> Int ->
Some (TypedEntry TransPhase ext blocks tops rets args) ->
TypeTransM ctx OpenTerm
applyCallS :: OpenTerm -> OpenTerm -> Int -> TypeTransM ctx OpenTerm
applyCallS prev_stack frame i =
applyEventOpM (globalOpenTerm "Prelude.callS") [prev_stack, frame, i]
applyEventOpM (globalOpenTerm "Prelude.callS") [prev_stack, frame,
natOpenTerm (fromIntegral i)]

-- | FIXME HERE NOW: docs
translateTypedEntry ::
@@ -4850,7 +4850,7 @@ translateTypedEntry prev_stack frame (Some entry) =
if typedEntryHasMultiInDegree entry then
do i <- get
put (i+1)
call_tm <- applyCallS prev_stack frame i
call_tm <- lift $ applyCallS prev_stack frame i
return (Some (TypedEntryTrans entry $ Just call_tm))
else return $ Some (TypedEntryTrans entry Nothing)

@@ -4867,10 +4867,9 @@ translateTypedBlock prev_stack frame blk =
-- | Translate a @TypedBlockMap@ to a @TypedBlockMapTrans@ by generating
-- @CallS@ calls for each of the entrypoints that represents a recursive call
translateTypedBlockMap ::
OpenTerm -> OpenTerm -> Int ->
TypedBlockMap TransPhase ext blocks tops rets ->
OpenTerm -> OpenTerm -> TypedBlockMap TransPhase ext blocks tops rets ->
StateT Int (TypeTransM ctx) (TypedBlockMapTrans ext blocks tops rets)
translateTypedBlockMap prev_stack frame start_ix blkMap =
translateTypedBlockMap prev_stack frame blkMap =
traverseRAssign (translateTypedBlock prev_stack frame) blkMap

-- | Translate the typed statements of an entrypoint to a function
@@ -4884,7 +4883,6 @@ translateEntryBody :: PermCheckExtC ext =>
TypedEntry TransPhase ext blocks tops rets args ghosts ->
TypeTransM RNil OpenTerm
translateEntryBody stack mapTrans entry =
let stack = pushFunStackOpenTerm frame prev_stack in
lambdaExprCtx (typedEntryAllArgs entry) $
lambdaPermCtx (typedEntryPermsIn entry) $ \pctx ->
do retType <- translateEntryRetType entry
@@ -4897,23 +4895,24 @@ translateBlockMapBodies :: PermCheckExtC ext => OpenTerm ->
TypedBlockMapTrans ext blocks tops rets ->
TypedBlockMap TransPhase ext blocks tops rets ->
TypeTransM RNil [OpenTerm]
translateBlockMapBodies stack mapTrans =
sequence $ mapBlockMapLetRec (translateEntryBody stack mapTrans)
translateBlockMapBodies stack mapTrans blkMap =
sequence $ mapBlockMapLetRec (translateEntryBody stack mapTrans) blkMap

-- | FIXME HERE NOW: docs
translateCFGInitEntryBody :: PermCheckExtC ext => OpenTerm ->
TypedBlockMapTrans ext blocks tops rets ->
TypedCFG ext blocks ghosts inits gouts ret ->
TypeTransM RNil OpenTerm
translateCFGInitEntryBody stack mapTrans cfg =
translateCFGInitEntryBody ::
PermCheckExtC ext => OpenTerm ->
TypedBlockMapTrans ext blocks (ghosts :++: inits) (gouts :> ret) ->
TypedCFG ext blocks ghosts inits gouts ret ->
TypeTransM RNil OpenTerm
translateCFGInitEntryBody stack mapTrans (cfg :: TypedCFG ext blocks ghosts inits gouts ret) =
let fun_perm = tpcfgFunPerm cfg
h = tpcfgHandle cfg
ctx = typedFnHandleAllArgs h
inits = typedFnHandleArgs h
ghosts = typedFnHandleGhosts h
retTypes = typedFnHandleRetTypes h in
lambdaExprCtx ctx $
translateRetType retTypes (tpcfgOutputPerms cfg) >>= \retTypeTrans ->
lambdaPermCtx (funPermIns fun_perm) $ \pctx ->

-- Extend the expr context to contain another copy of the initial arguments
-- inits, since the initial entrypoint for the entire function takes two
@@ -4922,20 +4921,13 @@ translateCFGInitEntryBody stack mapTrans cfg =
-- the same as those top-level arguments and so get eq perms to relate them
inExtMultiTransCopyLastM ghosts (cruCtxProxies inits) $

let all_membs = RL.members (cruCtxProxies $ appendCruCtx ctx inits)
inits_membs =
snd $ RL.split ghosts (cruCtxProxies inits) $
fst $ RL.split ctx (cruCtxProxies inits) all_membs
inits_eq_perms = eqPermTransCtx all_membs inits_membs
all_pctx = RL.append pctx inits_eq_perms
px = RL.map (\_ -> Proxy) all_pctx
lambdaPermCtx (funPermToBlockInputs fun_perm) $ \pctx ->
let all_membs = RL.members pctx
all_px = RL.map (\_ -> Proxy) pctx
init_entry = lookupEntryTransCast (tpcfgEntryID cfg) CruCtxNil mapTrans in
impTransM all_membs all_pctx mapTrans stack retTypeTrans
(assertPermStackEqM "translateCFG" (mbValuePermsToDistPerms $
funPermToBlockInputs fun_perm)
>>
translateCallEntry "CFG" init_entry (nuMulti all_px id) (nuMulti all_px $
const MNil))
impTransM all_membs pctx mapTrans stack retTypeTrans $
translateCallEntry "CFG" init_entry (nuMulti all_px id) (nuMulti all_px $
const MNil)

-- | FIXME HERE NOW: docs
translateCFGBodies :: PermCheckExtC ext => OpenTerm -> OpenTerm -> Int ->
@@ -4946,7 +4938,7 @@ translateCFGBodies prev_stack frame start_ix cfg =
let stack = pushFunStackOpenTerm frame prev_stack
mapTrans <-
evalStateT (translateTypedBlockMap prev_stack frame blkMap) (start_ix+1)
bodies <- translateBlockMapBodies stack mapTrans
bodies <- translateBlockMapBodies stack mapTrans blkMap
init_body <- translateCFGInitEntryBody stack mapTrans cfg
return (init_body : bodies)

@@ -4982,11 +4974,11 @@ translateCFG :: PermEnv -> OpenTerm -> OpenTerm -> Int ->
TypedCFG ext blocks ghosts inits gouts ret ->
OpenTerm
translateCFG env frame bodiesF i cfg =
lambdaCFGArgs (\args prev_stack ->
applyEventOpM (globalOpenTerm "Prelude.multiFixS")
([prev_stack, frame, applyOpenTerm bodiesF prev_stack,
natOpenTerm (fromIntegral i)]
++ args))
lambdaCFGArgs env cfg (\args prev_stack ->
applyEventOpM (globalOpenTerm "Prelude.multiFixS")
([prev_stack, frame, applyOpenTerm bodiesF prev_stack,
natOpenTerm (fromIntegral i)]
++ args))


----------------------------------------------------------------------
@@ -5015,6 +5007,21 @@ someCFGAndPermSym (SomeCFGAndPerm sym _ _ _) = sym
someCFGAndPermToName :: SomeCFGAndPerm ext -> String
someCFGAndPermToName (SomeCFGAndPerm _ nm _ _) = nm

-- | Helper function to build an LLVM function permission from a 'FunPerm'
mkPtrFunPerm :: HasPtrWidth w => FunPerm ghosts args gouts ret ->
ValuePerm (LLVMPointerType w)
mkPtrFunPerm fun_perm =
withKnownNat ?ptrWidth $ ValPerm_Conj1 $ mkPermLLVMFunPtr ?ptrWidth fun_perm

-- | Map a 'SomeCFGAndPerm' to a 'PermEnvGlobalEntry' with no translation, i.e.,
-- with an 'error' term for the translation
someCFGAndPermGlobalEntry :: HasPtrWidth w => SomeCFGAndPerm ext ->
PermEnvGlobalEntry
someCFGAndPermGlobalEntry (SomeCFGAndPerm sym _ _ fun_perm) =
withKnownNat ?ptrWidth $
PermEnvGlobalEntry sym (mkPtrFunPerm fun_perm) True $
error "someCFGAndPermGlobalEntry: unexpected translation during type-checking"

-- | Convert the 'FunPerm' of a 'SomeCFGAndPerm' to an inductive @LetRecType@
-- description of the SAW core type it translates to
someCFGAndPermLRT :: PermEnv -> SomeCFGAndPerm ext -> OpenTerm
@@ -5033,9 +5040,7 @@ someCFGAndPermLRT env (SomeCFGAndPerm _ _ _
-- pointer values
someTypedCFGPtrPerm :: HasPtrWidth w => SomeTypedCFG LLVM ->
ValuePerm (LLVMPointerType w)
someTypedCFGPtrPerm (SomeTypedCFG _ _ cfg) =
withKnownNat ?ptrWidth $ ValPerm_Conj1 $ mkPermLLVMFunPtr ?ptrWidth $
tpcfgFunPerm cfg
someTypedCFGPtrPerm (SomeTypedCFG _ _ cfg) = mkPtrFunPerm $ tpcfgFunPerm cfg

-- | Transform a list of 'OpenTerm' values of type @tp@ into a @List2 tp@
list2OpenTerm :: OpenTerm -> [OpenTerm] -> OpenTerm
@@ -5046,22 +5051,29 @@ list2OpenTerm tp trms =

-- | Make a term of type @LetRecTypes1@ from a list of @LetRecType@ terms
lrtsOpenTerm :: [OpenTerm] -> OpenTerm
lrtsOpenTerm = list2OpenTerm (dataTypeOpenTerm "Prelude.LetRecType1")
lrtsOpenTerm = list2OpenTerm (dataTypeOpenTerm "Prelude.LetRecType1" [])

-- | FIXME HERE NOW: docs
tcTranslateAddCFGs ::
HasPtrWidth w => SharedContext -> ModuleName -> PermEnv -> ChecksFlag ->
EndianForm -> DebugLevel -> [SomeCFGAndPerm LLVM] ->
IO PermEnv
tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
withKnownNat ?ptrWidth $
do
-- First, we type-check all the CFGs, mapping them to SomeTypedCFGs
-- First, we type-check all the CFGs, mapping them to SomeTypedCFGs; this
-- uses a temporary PermEnv where all the function symbols being
-- type-checked are assigned their permissions, but no translation yet
let tmp_env1 =
permEnvAddGlobalSyms env $
map someCFGAndPermGlobalEntry cfgs_and_perms
let tcfgs =
flip map cfgs_and_perms $ \(SomeCFGAndPerm gsym nm cfg fun_perm) ->
debugTraceTraceLvl dlevel ("Type-checking " ++ show sym) $
SomeTypedCFG gsym nm $
debugTraceTraceLvl dlevel ("Type-checking " ++ show gsym) $
debugTrace verboseDebugLevel dlevel
("With type:\n" ++ permPrettyString emptyPPInfo fun_perm) $
tcCFG ?ptrWidth env' endianness dlevel fun_perm cfg
tcCFG ?ptrWidth tmp_env1 endianness dlevel fun_perm cfg

-- Next, generate a list of all the LetRecTypes in all of the functions,
-- along with a list of indices into that list of where the LRTs of each
@@ -5072,7 +5084,6 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
gen_lrts_ixs _ [] = []
let (fun_ixs, lrtss) = unzip $ gen_lrts_ixs 0 tcfgs
let lrts = concat lrtss
let fun_lrts = map head lrtss
let frame = lrtsOpenTerm lrts

-- Now, generate a SAW core lambda that takes in the previous stack and
@@ -5087,13 +5098,13 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
-- lambda for prev_stack
do tmp_env <-
permEnvAddGlobalSyms env <$>
zipWithM (\some_tpcfg@(SomeTypedCFG sym _ cfg) i ->
zipWithM (\some_tpcfg@(SomeTypedCFG sym _ _) i ->
do call_tm <- applyCallS prev_stack frame i
let fun_p = someTypedCFGPtrPerm some_tpcfg
return $ PermEnvGlobalEntry sym fun_p True [call_tm])
tcfgs fun_ixs
bodiess <-
local (\info -> into { ttiPermEnv = tmp_env }) $
local (\info -> info { ttiPermEnv = tmp_env }) $
zipWithM (\i (SomeTypedCFG _ _ cfg) ->
translateCFGBodies prev_stack frame i cfg) fun_ixs tcfgs
return $ tupleOpenTerm $ concat bodiess
@@ -5106,7 +5117,7 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
completeNormOpenTerm sc $
runNilTypeTransM env checks $ piFunStackM $ \prev_stack ->
let stack = pushFunStackOpenTerm prev_stack frame in
applyEventOpM "Prelude.LRTsTuple" [stack, frame]
applyEventOpM (globalOpenTerm "Prelude.LRTsTuple") [stack, frame]
scInsertDef sc mod_name bodiesF_ident bodiesF_tp bodiesF_tm
let bodiesF = globalOpenTerm bodiesF_ident

@@ -5116,17 +5127,15 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
zipWithM
(\(SomeTypedCFG sym nm cfg) i ->
do tp <-
completeNormOpenTerm sc $ piCFGArgs env cfg $ \args prev_stack ->
completeNormOpenTerm sc $ piCFGArgs env cfg $ \_ prev_stack ->
let fun_perm = tpcfgFunPerm cfg in
translateRetType (funPermRets fun_perm) (funPermOuts fun_perm) >>=
specMTypeTransM prev_stack
tm <- completeNormOpenTerm sc $
translateCFG env frame bodiesF i cfg
let ident = mkSafeIdent mod_name nm
scInsertDef sc mod_name ident tp tm
let perm =
withKnownNat ?ptrWidth $ ValPerm_Conj1 $
mkPermLLVMFunPtr ?ptrWidth $ tpcfgFunPerm cfg
let perm = mkPtrFunPerm $ tpcfgFunPerm cfg
return $ PermEnvGlobalEntry sym perm False [globalOpenTerm ident])
tcfgs fun_ixs
return $ permEnvAddGlobalSyms env new_entries
@@ -5156,8 +5165,7 @@ translateCompleteTypeInCtx :: SharedContext -> PermEnv ->
translateCompleteTypeInCtx sc env args ret =
completeNormOpenTerm sc $
runNilTypeTransM env noChecks (piExprCtx args (typeTransType1 <$>
translate ret'))
where ret' = mbCombine (cruCtxProxies args) . emptyMb $ ret
translate ret))

-- | Translate an input list of 'ValuePerms' and an output 'ValuePerm' to a SAW
-- core function type in a manner similar to 'translateCompleteFunPerm', except
@@ -5169,8 +5177,5 @@ translateCompletePureFun :: SharedContext -> PermEnv
-> IO Term
translateCompletePureFun sc env ctx args ret =
completeNormOpenTerm sc $ runNilTypeTransM env noChecks $
piExprCtx ctx $ piPermCtx args' $ const $
typeTransTupleType <$> translate ret'
where args' = mbCombine pxys . emptyMb $ args
ret' = mbCombine pxys . emptyMb $ ret
pxys = cruCtxProxies ctx
piExprCtx ctx $ piPermCtx args $ const $
typeTransTupleType <$> translate ret