Update monadification and MR solver to work with the SpecM monad#1806

Merged

mergify[bot] merged 31 commits intomasterfrom heapster-itree-mr-solver-alt

Jan 26, 2023

+1,382-820

Commits on Dec 5, 2022

Updated MR solver to work with SpecM instead of CompM
Eddy Westbrook
committed

Commits on Dec 6, 2022

got some of the MR solver unit tests working
Eddy Westbrook
committed
changed mrFreshCallVars to normalize the frame argument
Eddy Westbrook
committed
fixed a bug in mrFreshCallVars where uvars were not getting properly abstracted out of callS body definitions
Eddy Westbrook
committed

Commits on Dec 7, 2022

changed CompFuns to keep around their event types and fun stacks
Eddy Westbrook
committed
added multiArgFixS
Eddy Westbrook
committed
started updating linked_list_mr_solver.saw
Eddy Westbrook
committed
updated the core algorithm of the monadifier to use SpecM
Eddy Westbrook
committed
fixed mrFreshCallVars to normalize the defs term; fixed a small printing bug
Eddy Westbrook
committed
updated the noErrors spec in linked_list_mr_solver.saw
Eddy Westbrook
committed

Commits on Dec 8, 2022

add debug output to missing mrProveRel case
m-yac
committed
un-comment a line that was accidentally commented by a previous commit
Eddy Westbrook
committed
fixed mrReplaceCallsWithTerms to use term lifting when it recurses into a variable binding
Eddy Westbrook
committed
Merge branch 'heapster-itree' into heapster-itree-mr-solver-alt
Eddy Westbrook
committed

Commits on Dec 10, 2022

updated the monadified versions of the cryptol primitives to use SpecM
Eddy Westbrook
committed

Commits on Dec 12, 2022

fixed some small bugs in CryptolM.sawcore
Eddy Westbrook
committed
added list1OpenTerm operator
Eddy Westbrook
committed

Commits on Dec 13, 2022

fixed fixMacro to push the new frame onto the function stack when recursing inside the function bodies
Eddy Westbrook
committed
fixed the fixMacro to wrk, I think...
Eddy Westbrook
committed
changed mrFreshVar to abstract over the current uvar context; added support to normComp for normalizing multiArgFixS
Eddy Westbrook
committed

Commits on Dec 14, 2022

updated the normalizer in SMT.hs to work with SpecM types
Eddy Westbrook
committed
Merge branch 'master' into heapster-itree-mr-solver-alt
Eddy Westbrook
committed

Commits on Jan 19, 2023

Merge branch 'master' into heapster-itree-mr-solver-alt
Eddy Westbrook
committed

Commits on Jan 25, 2023

Merge branch 'master' into heapster-itree-mr-solver-alt
Eddy Westbrook
committed
updated some of the monadification tests to work with SpecM
Eddy Westbrook
committed
commented out tests involving monadifying quantifiers, which don't quite work yet
Eddy Westbrook
committed
changed the set_monadification command to allow for monadifications that are polymorphic over the event type and fun stack params
Eddy Westbrook
committed
updated the monadification tests to succeed with the new SpecM monad
Eddy Westbrook
committed
resolve defined-but-not-used warnings in Solver.hs
m-yac
committed
update pinned commit to entree-specs
m-yac
committed
style tweak in constraints in Monadify.hs
m-yac
committed