Update Heapster, Monadification, and MRSolver to handle high-order SpecM functions#2017

Merged

eddywestbrook merged 316 commits intomasterfrom heapster/higher-order-no-stack

Feb 9, 2024

+10,488-7,837

This pull request is big! We're only showing the most recent 250 commits

Commits on Aug 24, 2023

wrote translateCompletePureFun
Eddy Westbrook
committed
re-added translateCompleteFunPerm, with documentation reflecting the fact that it now generates a SpecDef type
Eddy Westbrook
committed

Commits on Aug 26, 2023

added helper functions to SAWTranslation.hs to support IRTTranslation.hs
Eddy Westbrook
committed
added the notion of pure vs impure type translations, to support IRTTranslation
Eddy Westbrook
committed
added psubstOfSubst
Eddy Westbrook
committed

Commits on Aug 27, 2023

added an OpenTermLike instance for OpenTerm itself
Eddy Westbrook
committed
Finished rewriting IRTTranslation.hs
Eddy Westbrook
committed
added one more import to HeapsterBuiltins.hs to get it to compile
Eddy Westbrook
committed
fixed some variable-binding issues in the definition of defineSpecOpenTerm
Eddy Westbrook
committed
added applyCallClos to the prelude
Eddy Westbrook
committed
fixed translation code that was only applying closures to apply and call them
Eddy Westbrook
committed
added the LRT_SpecM constructor to LRT output types
Eddy Westbrook
committed

Commits on Aug 28, 2023

fixed the translation of the folding and unfolding functions for recursive shapes and permissions to use exprCtxPureTypeTerms for the arguments, to match their definitions
Eddy Westbrook
committed

Commits on Aug 29, 2023

fixed importDefSpecTerm to turn the import into a SpecImp
Eddy Westbrook
committed
changed all uses of the LetRecType eliminator to use the explicit eliminator
Eddy Westbrook
committed
fixed permEnvAddGlobalSymFun to use a spec definition translation instead of a translation term
Eddy Westbrook
committed
fixed up call to importDefSpecTerm to use its new def
Eddy Westbrook
committed
removed old CompM Coq files from _CoqProject
Eddy Westbrook
committed
Got all the Coq export stuff for the prelude working
Eddy Westbrook
committed

Commits on Aug 31, 2023

Commits on Sep 1, 2023

added the termIsClosed function to test if a SAW core term is closed
Eddy Westbrook
committed
refactored the saw-core-coq translator so that all the local variable information is in a reader effect and not a state effect, making it clearer where in the translator code variables are bound; a…
Eddy Westbrook
committed
moved linked_list.sawcore to use the new SpecDef framework
Eddy Westbrook
committed
replaced llvmZeroInitValue with a new function translateZeroInit that directly translates an LLVM zero initializer to a Heapster permission + SAW core term, so that we use repeatBVVec in the SAW te…
Eddy Westbrook
committed
updated mbox_proofs.v after changes to the Coq translator
Eddy Westbrook
committed
renamed askTrr and localTrr to askTR and localTR
Eddy Westbrook
committed
replaced a number of equality tests on the free variables of terms against emptyBitSet with the new termIsClosed function
Eddy Westbrook
committed
replaced checkGroundTerm with the now standard termIsClosed function
Eddy Westbrook
committed
whoops, fixed a few lingering bugs related to using termIsClosed
Eddy Westbrook
committed
made a few fixes to make the code more readable
Eddy Westbrook
committed
a few more tweaks to make the code look nicer
Eddy Westbrook
committed
finished writing a comment on withSAWVar
Eddy Westbrook
committed
indentation change requested by review
Eddy Westbrook
committed
Merge branch 'master' into saw-core-coq/var-binding-fix
Eddy Westbrook
committed
Merge branch 'saw-core-coq/var-binding-fix' into heapster/higher-order
Eddy Westbrook
committed

Commits on Sep 28, 2023

started defining type descriptions; removed the old IRT stuff
Eddy Westbrook
committed

Commits on Sep 29, 2023

Defined tpElem and indElem
Eddy Westbrook
committed

Commits on Oct 1, 2023

Updated the SAW core prelude with the new definition of SpecM based on TpDescs
Eddy Westbrook
committed

Commits on Oct 3, 2023

renamed arithmetic kinds to expression kinds
Eddy Westbrook
committed

Commits on Oct 4, 2023

fixed a comment; added Tp_BVVec
Eddy Westbrook
committed
whoops, fixed the type of FixS
Eddy Westbrook
committed

Commits on Oct 13, 2023

fixed indentation
Eddy Westbrook
committed
added the Sigmas type
Eddy Westbrook
committed
Working on rewriting SAWTranslation.hs to work with the new definition of SpecM
Eddy Westbrook
committed
Got the first portion of SAWTranslation.hs to compile with the new version of SpecM
Eddy Westbrook
committed

Commits on Oct 17, 2023

updated the translation of the implication rules to work with the new SpecM monad
Eddy Westbrook
committed
updated the translation of the EndLifetime rule
Eddy Westbrook
committed
Started translating recursive and opaque shapes
Eddy Westbrook
committed
updated the translations of shapes and permissions to also contain the translation of shapes and permissions to types, not just type descriptions; also updated the translation of shape expressions …
Eddy Westbrook
committed

Commits on Oct 18, 2023

added explicit substitutions to type descriptions, for use in translating named type descriptions
Eddy Westbrook
committed
updated the translation of Crucible expressions
Eddy Westbrook
committed
updated the translation of jump targets and statements
Eddy Westbrook
committed
whoops, just realized that lownedTransTerm needs to partially apply its function to the existing ps_extra
Eddy Westbrook
committed

Commits on Oct 19, 2023

Commits on Oct 20, 2023

defined translateCFGs in the new SpecM monad
Eddy Westbrook
committed
finished updating tcTranslateAddCFGs to the new SpecM
Eddy Westbrook
committed
finished updating the remaining top-level entrypoints in SAWTranslation.hs
Eddy Westbrook
committed

Commits on Oct 21, 2023

added the TranslateDescs instances for permissions and atomic permissions; define the translations for the folding and unfolding rules for recursive shapes and permissions
Eddy Westbrook
committed
changed recursive permissions to have a body with a permission variable free, similar to how recursive shapes work
Eddy Westbrook
committed
implemented translateCompleteFunType
Eddy Westbrook
committed
removed the no longer needed IRTTranslation.hs file
Eddy Westbrook
committed
started updating HeapsterBuiltins.hs to work with the new SpecM monad
Eddy Westbrook
committed

Commits on Oct 22, 2023

Commits on Oct 23, 2023

expanded the comments on SomePartialNamedShape
Eddy Westbrook
committed
updated more of HeapsterBuiltins.hs to work with the new SpecM
Eddy Westbrook
committed
finished updating SAW to the new SpecM monad!
Eddy Westbrook
committed
added varKindExpr for use in translating descriptions from expression variables
Eddy Westbrook
committed
fixed BV proofs to use the correct, non-monadic type to pass to the errorS combinator
Eddy Westbrook
committed

Commits on Oct 24, 2023

bug fix: the type description for an existential permission needs to handle the special case of an equality permission in the body of the existential
Eddy Westbrook
committed
implemented proveEqNat
Eddy Westbrook
committed
added a Tp_M constructor to the output type of function descriptions; changed pis to lambdas for generated functions; changed constants to use the more general constKindExpr function
Eddy Westbrook
committed
whoops, translateCallEntry should not pass in the top-level arguments as inputs
Eddy Westbrook
committed
removed some unused arguments; made some small cosmetic changes
Eddy Westbrook
committed
updated Coq translation to work with the new SpecM monad
Eddy Westbrook
committed
updated CryptolM.sawcore to work with the new SpecM monad
Eddy Westbrook
committed

Commits on Oct 25, 2023

Commits on Oct 26, 2023

re-enabled the ref_sum example in rust_data
Eddy Westbrook
committed
added projTupleOpenTerm' to OpenTerm.hs
Eddy Westbrook
committed
fixed the LLVM global translations in LLVMGlobalConst.hs to match the new translation of shapes as 0 or more types instead of a fixed 1 type
Eddy Westbrook
committed

Commits on Oct 27, 2023

changed transTerms to have a monadic version for permissions
Eddy Westbrook
committed
whoops, used pairTypeOpenTerm instead o9f pairOpenTerm in tupleOpenTerm'
Eddy Westbrook
committed
whoops, forgot to add a SpecM to the output type of LambdaS
Eddy Westbrook
committed
small bug fixes
Eddy Westbrook
committed
whoops, messed up the translation of the SImpl_LLVMArrayCellReturn rule when converting to monadic transTermsM
Eddy Westbrook
committed
bug fix in bindTransM to use lambdaTupleTransM; also added some FIXMEs for optimizing the translation of lifetimes
Eddy Westbrook
committed

Commits on Oct 28, 2023

Merge branch 'master' into heapster/higher-order-no-stack
Eddy Westbrook
committed
fixed projTupleOpenTerm' and its uses to be consistent
Eddy Westbrook
committed

Commits on Nov 2, 2023

make MRSolver debug commands uniformly named
m-yac
committed

Commits on Nov 3, 2023

warn on Heapster implication failures
m-yac
committed

Commits on Nov 6, 2023

Changed tpElemEnv to no longer use function indices at all
Eddy Westbrook
committed

Commits on Nov 7, 2023

moved SpecM and its related definitions to its own SAW core module
Eddy Westbrook
committed

Commits on Nov 8, 2023

updated Heapster to use the new version of SpecM that does not use FunIxs and is contained in a separate SpecM SAW core module
Eddy Westbrook
committed
whoops, forgot to update an identifier from the Prelude to the SpecM module
Eddy Westbrook
committed
small bug fixes in the translation
Eddy Westbrook
committed
updated Coq translation to work with the new definition of SpecM
Eddy Westbrook
committed
more small bug fixes to the translation
Eddy Westbrook
committed
bug fixes to get folding of inductive types to work properly
Eddy Westbrook
committed
updated the arrays and linked_list examples to work with the new version of SpecM
Eddy Westbrook
committed
whoops, tpElem needs to be applied to an event type
Eddy Westbrook
committed
uncommented a bunch of the old rust_data functions, and got them working
Eddy Westbrook
committed
changed translateCallEntry to not convert permissions to terms and then back again when it calls non-recursive entrypoints
Eddy Westbrook
committed

Commits on Nov 14, 2023

moved the SpecM OpenTerm operations to OpenTerm.hs
Eddy Westbrook
committed

Commits on Nov 15, 2023

Commits on Nov 19, 2023

started updating monadification to work with the new SpecM type
Eddy Westbrook
committed

Commits on Nov 20, 2023

Commits on Nov 21, 2023

mostly finished updating monadification, other than quantifying over event types
Eddy Westbrook
committed
changed the EventType type to hold an arbitrary term, rather than just an identifier, in order to support event type polymorphism in monadification
Eddy Westbrook
committed
added documentation for monadifyLambdas and monadifyEtaExpand
Eddy Westbrook
committed
updated comments to remove SpecMParams
Eddy Westbrook
committed

Commits on Nov 23, 2023

re-added an updated version of refinesS
Eddy Westbrook
committed
updated MR solver to work with the new definition of SpecM
Eddy Westbrook
committed
whoops, changed some identifiers from the Prelude to the new SpecM SAW core module; also made sure the SpecM and CryptolM modules are loaded when needed
Eddy Westbrook
committed
updated a use of EvType from the Prelude to the SpecM SAW core module
Eddy Westbrook
committed
whoops, forgot to monadify the bitvector type
Eddy Westbrook
committed

Commits on Nov 24, 2023

updated monadify example to work with the new SpecM
Eddy Westbrook
committed

Commits on Nov 25, 2023

whoops, forgot to update a number of SpecM identifiers to the new SpecM module
Eddy Westbrook
committed

Commits on Nov 26, 2023

added a case to the MR solver normalizer to recognize LetRecS terms
Eddy Westbrook
committed
whoops, updated two more identifiers to point to the new SpecM module
Eddy Westbrook
committed
small bug fixes
Eddy Westbrook
committed
updated SpecPrims to work with the new SpecM monad
Eddy Westbrook
committed
fixed the printing for NormComp and friends to have the correct number of underscores for the new SpecM
Eddy Westbrook
committed

Commits on Nov 27, 2023

removed the notion of an indescribable num expression, replacing it with just Num terms
Eddy Westbrook
committed
reordered to arguments of Tp_Seq to match the definition of Vec, seq, and mseq
Eddy Westbrook
committed
updated the SMT solver part of MR solver to use the new SpecM in the new SpecM SAW core module
Eddy Westbrook
committed
whoops, updated mrGetInvariant to use the new version of assertFiniteS
Eddy Westbrook
committed

Commits on Nov 30, 2023

Commits on Dec 1, 2023

Commits on Dec 4, 2023

added refinesS_eq combinator
Eddy Westbrook
committed
finished updating arrays_mr_solver.saw example to work
Eddy Westbrook
committed
updated mr_solver_unit_tests.saw example to work
Eddy Westbrook
committed

Commits on Dec 6, 2023

Commits on Dec 13, 2023

Commits on Dec 14, 2023

finished implementing injUnifyRepr
Eddy Westbrook
committed
fixed lifting bug in mrApplyRepr
Eddy Westbrook
committed
fixed mrTrySetAppliedEVar to correctly handle higher-order variables
Eddy Westbrook
committed
changed genBVVecNoPf to use gen instead of genBVVec
Eddy Westbrook
committed
changed the normalizer to prefer caller-supplied primitives over its default primitive implementations
Eddy Westbrook
committed
updated implementations of the primitives to work directly with gen and at
Eddy Westbrook
committed
fixed a lifting bug in generalizeCoIndHyp
Eddy Westbrook
committed
commented out the no-longer used cases of instUVar
Eddy Westbrook
committed
added evar lowering as part of mrProvable, to ensure evars over function variables do not become higher-order variables in SMT
Eddy Westbrook
committed
whoops, forgot to lift the arg0 repr in generalizeCoIndHyp
Eddy Westbrook
committed
added loop detection to proveCoIndHyp
Eddy Westbrook
committed
added calls to mrIndexBVVec in the mrProveRelH for vectors, though mrIndexBVVec is not yet defined...
Eddy Westbrook
committed

Commits on Dec 17, 2023

Merge branch 'mrsolver-dilithium' into heapster/higher-order-no-stack
m-yac
committed

Commits on Dec 18, 2023

changed heapster_init_env to add an import of the SpecM SAW core module instead of Prelude when it creates a SAW core module
Eddy Westbrook
committed
updated the docs for heapster_define_reachability_perm
Eddy Westbrook
committed
started updating mbox example to work with the new SpecM monad...
Eddy Westbrook
committed

Commits on Dec 20, 2023

Commits on Dec 24, 2023

Merge branch 'heapster/higher-order-no-stack' of github.com:GaloisInc/saw-script into heapster/higher-order-no-stack
Eddy Westbrook
committed

Commits on Dec 26, 2023

Commits on Dec 28, 2023

Commits on Dec 29, 2023

added more debug info for translating LLVM globals
Eddy Westbrook
committed
whoops, fixed the translation of sequence shapes where both sides have no empty translations
Eddy Westbrook
committed
updated permEnvAddGlobalConst to fit with the new translation of memblock permissions to have 0 or 1 terms
Eddy Westbrook
committed
added parsing support for tuple shapes
Eddy Westbrook
committed
added an explicit tuple shape to the type of memcpy in rust_data.saw
Eddy Westbrook
committed

Commits on Jan 1, 2024

Commits on Jan 16, 2024

Commits on Jan 23, 2024

Commits on Feb 2, 2024

Merge branch 'master' into heapster/higher-order-no-stack
Eddy Westbrook
committed
updated the commit number for the entree-specs repo
Eddy Westbrook
committed

Commits on Feb 3, 2024

removed references to functions that are no longer used from unfold_bv_funs
Eddy Westbrook
committed
removing unsafeAsserts from the definition of iteWithProof because the unsafeAssert Coq tactic is currently defined *after* the translation to Coq of the Prelude
Eddy Westbrook
committed
changed the Coq translations of tcAdd and tcMul to be written by hand in SpecM.v instead of automatically generated
Eddy Westbrook
committed
changed SpecM.v to rely on CryptolPrimitivesForSAWCore.v rather than the other way around, so that it can use the generated Num operations like tcAdd and tcMul
Eddy Westbrook
committed
fixed up the imports for the heapster_export_coq command
Eddy Westbrook
committed
added MR solver support for the iteWithProof combinator
Eddy Westbrook
committed
changed all the examples to import SpecM instead of the SAW core Prelude
Eddy Westbrook
committed
added checks to heapster_define_opaque_perm and heapster_define_opaque_llvmshape to make sure the user-supplied type and type description match
Eddy Westbrook
committed
updated global_var example to work
Eddy Westbrook
committed
added more info to the error message when a type does not match a type description
Eddy Westbrook
committed

Commits on Feb 6, 2024

updated checkTypeAgreesWithDesc, since the previous version was incorrect
Eddy Westbrook
committed
updated memcpy example to work with the new SpecM
Eddy Westbrook
committed
updated ListDescType to the correct version to agree with ListDesc, now that Heapster checks that these agree
Eddy Westbrook
committed
started updating the string_set example, but ended up commenting most of it out
Eddy Westbrook
committed
commented out stuff that does not work in the Heapster examples for now
Eddy Westbrook
committed

Commits on Feb 8, 2024

added an override for iteWithProof when calling into SMT
Eddy Westbrook
committed
added tracing for terms being inserted by Heapster commands when the debug level is at least 2
Eddy Westbrook
committed
removed iso_recursive example, since it is now superseded by the linked_list example
Eddy Westbrook
committed

Commits on Feb 9, 2024

whoops, forgot to remove the iso_recursive example from the _CoqProject
Eddy Westbrook
committed
simplified memcpy permissions to help with translation
Eddy Westbrook
committed
commented out all the _proofs.v files from the _CoqProject
Eddy Westbrook
committed
updated rust_lifetimes example to work with the new SpecM
Eddy Westbrook
committed
commented out the processBlocks function from the sha512 example because it currently has a panic
Eddy Westbrook
committed
updated io example to work with the new SpecM
Eddy Westbrook
committed