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.

Sign up for GitHub

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: Generate definitions for recursive function frames #1804

Merged
merged 2 commits into from
Jan 23, 2023
Merged

Heapster: Generate definitions for recursive function frames #1804

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4f3657d
changed the way Heapster extracted specs are generated so that the fu…
Jan 19, 2023
e4b37c0
Merge branch 'master' into heapster/frame-def
Jan 19, 2023
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
19 changes: 15 additions & 4 deletions heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5142,6 +5142,11 @@ lrtsOpenTerm lrts =
(ctorOpenTerm "Prelude.Nil1" [tp])
lrts

-- | Make the type @List1 LetRecType@ of recursive function frames
frameTypeOpenTerm :: OpenTerm
frameTypeOpenTerm = dataTypeOpenTerm "Prelude.List1" [dataTypeOpenTerm
"Prelude.LetRecType" []]

-- | FIXME HERE NOW: docs
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it finally time to fix this FIXME? :)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's probably a job for the Fixmen, who answer the age-old question: who fixes the FIXMEs?

Seriously, though, there are a lot of FIXMEs that need to be updated, and this commit is probably not the time...

tcTranslateAddCFGs ::
HasPtrWidth w => SharedContext -> ModuleName -> PermEnv -> ChecksFlag ->
Expand All @@ -5164,16 +5169,22 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
("With type:\n" ++ permPrettyString emptyPPInfo fun_perm) $
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
-- function are in that list
-- Next, generate a frame, i.e., 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 function are in that list, and make a definition for the frame
let gen_lrts_ixs (i::Natural) (SomeTypedCFG _ _ tcfg : tcfgs') =
let lrts = translateCFGLRTs env tcfg in
(i, lrts) : gen_lrts_ixs (i + fromIntegral (length lrts)) tcfgs'
gen_lrts_ixs _ [] = []
let (fun_ixs, lrtss) = unzip $ gen_lrts_ixs 0 tcfgs
let lrts = concat lrtss
let frame = lrtsOpenTerm lrts
frame_tm <- completeNormOpenTerm sc $ lrtsOpenTerm lrts
let frame_ident =
mkSafeIdent mod_name (someCFGAndPermToName (head cfgs_and_perms)
++ "__frame")
frame_tp <- completeNormOpenTerm sc frameTypeOpenTerm
scInsertDef sc mod_name frame_ident frame_tp frame_tm
let frame = globalOpenTerm frame_ident
let stack = singleFunStack frame

-- Now, generate a SAW core tuple of all the bodies of mutually recursive
Expand Down