mem_ssa: defs + cheated property statements#169
Merged
charles-cooper merged 3 commits intomainfrom Mar 4, 2026
Merged
Conversation
Port of vyper/venom/analysis/mem_ssa.py to HOL4.
LLVM-style Memory SSA tracks memory state versions through the program.
Definitions (memSSADefsScript.sml, 515 LOC):
Types: mssa_node (MnDef/MnUse/MnPhi), mssa_state (flat map representation)
Phase 1: collect defs/uses via bp_get_read/write_location
Phase 2: insert MemPhi at dominance frontiers (worklist, fuel-based)
Phase 3: connect reaching definitions (backward scan + idom walk)
Phase 4: remove redundant phis (all-same operands)
Queries: clobber walk (completely_contains check), aliased walk (may_alias)
Three instantiations: memory/storage/transient via addr_space parameter
Properties (7 cheats):
wf_mssa (composite: mssa_ids_valid, mssa_edges_valid,
mssa_inst_maps_consistent, mssa_reaching_complete)
mssa_build_wf, mssa_reaching_def_exists_and_valid,
mssa_reaching_def_dominates, mssa_phi_at_frontier,
mssa_no_redundant_phis, mssa_reaching_acyclic, mssa_clobber_sound
In Python, the visited set is a mutable OrderedSet shared across all recursive calls through phi operands. When walking operand A visits a node, operand B's walk sees it as already visited. The original HOL port passed the same visited snapshot to each operand independently — updates from one operand's walk didn't propagate to siblings. This could produce different clobber results on diamond-shaped def chains. Fix: thread (result, updated_visited) through both walks and their phi collection helpers. mem_ssa_collect_phi_clobbers and mem_ssa_collect_phi_aliased now accept and return the visited set. The aliased walk also threads visited between from_here and from_chain computations within a single node.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
co-authored by claude opus 4.6
Port of
vyper/venom/analysis/mem_ssa.pyto HOL4. LLVM-style Memory SSA tracks memory state versions through the program — each store creates a new version (MemDef), each load reads a version (MemUse), join points get MemPhi nodes.Files
defs/memSSADefsScript.smlproofs/memSSAProofsScript.smlmemSSAPropsScript.smlDefinitions
All definitions use
mem_ssa_prefix.mssa_node(MnDef/MnUse/MnPhi),mem_ssa_state(flat map: access_id 0 = LiveOnEntry sentinel)bp_get_read/write_locationmem_ssa_get_clobbered(clobber walk),mem_ssa_get_aliased(alias walk)memory_ssa_analyze,storage_ssa_analyze,transient_ssa_analyzeProperties (7 cheats)
mem_ssa_build_wfmem_ssa_reaching_def_exists_and_validmem_ssa_reaching_def_dominatesmem_ssa_phi_at_frontiermem_ssa_no_redundant_phismem_ssa_reaching_acyclicmem_ssa_clobber_soundWell-formedness decomposed into named sub-predicates:
mem_ssa_ids_valid,mem_ssa_edges_valid,mem_ssa_inst_maps_consistent,mem_ssa_reaching_complete.Dependencies
Ancestors:
memAliasDefs,dominatorDefs(defs);dominatorAnalysisProps,cfgAnalysisProps,memAliasProps(proofs).Consumer
dead_store_eliminationpass (future).