-
Notifications
You must be signed in to change notification settings - Fork 18
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore: Split out the finishing tactic aspect of simp_mem into mem_ome…
…ga [2/?] (#231) This helps control how aggressive `simp_mem` is, since `simp_mem` now no longer closes memory goals, but rather expects the user to manually invoke `mem_omega` when necessary. Another impact of this change is that we split `mem_omega` into two tactics: `mem_omega` that does not expose `pairwiseSeparate` goals, and `mem_omega!`, which does. This also helps control the performance of `mem_omega`, and hopefully, this ensures that the user is careful before exposing a full `O(n^2)` set of constraints to the user. --- I was hoping that we would see a major performance difference. We do see some evidence for improvement in the `Experiments/MemoryAliasing.lean` (the numbers are extremely consistent across runs: ``` ### Old timings lake build Proofs.Experiments.MemoryAliasing 2.86s user 0.34s system 92% cpu 3.466 total ### New timings lake build Proofs.Experiments.MemoryAliasing 2.76s user 0.33s system 92% cpu 3.332 total ``` --- However, on the much larger `Memcpy.lean`, these types of considerations seem to just not matter: ``` ### Old timings lake build Proofs.Experiments.Memcpy.MemCpyVCG 31.79s user 0.81s system 99% cpu 32.878 total ### New timings lake build Proofs.Experiments.Memcpy.MemCpyVCG 32.79s user 0.80s system 99% cpu 33.870 total ``` This is a tad disappointing, but such is life. Onward to the next refactor. This is stacked on top of #230
- Loading branch information
Showing
11 changed files
with
266 additions
and
116 deletions.
There are no files selected for viewing
This file contains 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
This file contains 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,137 @@ | ||
| /- | ||
| Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Author(s): Siddharth Bhat | ||
| In this file, we define proof automation for separation conditions of memory. | ||
| References: | ||
| - https://github.com/leanprover/lean4/blob/240ebff549a2cf557f9abe9568f5de885f13e50d/src/Lean/Elab/Tactic/Omega/OmegaM.lean | ||
| - https://github.com/leanprover/lean4/blob/240ebff549a2cf557f9abe9568f5de885f13e50d/src/Lean/Elab/Tactic/Omega/Frontend.lean | ||
| -/ | ||
| import Arm | ||
| import Arm.Memory.MemoryProofs | ||
| import Arm.BitVec | ||
| import Arm.Memory.Attr | ||
| import Arm.Memory.AddressNormalization | ||
| import Lean | ||
| import Lean.Meta.Tactic.Rewrite | ||
| import Lean.Meta.Tactic.Rewrites | ||
| import Lean.Elab.Tactic.Conv | ||
| import Lean.Elab.Tactic.Conv.Basic | ||
| import Tactics.Simp | ||
| import Tactics.BvOmegaBench | ||
| import Arm.Memory.Common | ||
|
|
||
| open Lean Meta Elab Tactic Memory | ||
|
|
||
| namespace MemOmega | ||
|
|
||
| structure Config where | ||
| /-- | ||
| If true, then MemOmega will explode uses of pairwiseSeparate [mem₁, ... memₙ] | ||
| into O(n^2) separation conditions. | ||
| -/ | ||
| explodePairwiseSeparate : Bool := false | ||
|
|
||
| /-- Edit the config for mem_omega! -/ | ||
| def Config.mkBang (c : Config) : Config := | ||
| { c with explodePairwiseSeparate := true } | ||
|
|
||
| /-- Context for the `SimpMemM` monad, containing the user configurable options. -/ | ||
| structure Context where | ||
| /-- User configurable options for `simp_mem`. -/ | ||
| cfg : Config | ||
| /-- Cache of `bv_toNat` simp context. -/ | ||
| bvToNatSimpCtx : Simp.Context | ||
| /-- Cache of `bv_toNat` simprocs. -/ | ||
| bvToNatSimprocs : Array Simp.Simprocs | ||
|
|
||
|
|
||
| namespace Context | ||
|
|
||
| def init (cfg : Config) : MetaM Context := do | ||
| let (bvToNatSimpCtx, bvToNatSimprocs) ← | ||
| LNSymSimpContext | ||
| (config := {failIfUnchanged := false}) | ||
| -- Also use `mem_{legal', subset', separate'}.iff_omega to unfold definitions that | ||
| -- occur inside compound expressions, such as (mem_subset' .. ∨ mem_subset' ..) | ||
| -- (thms := #[``mem_legal'.iff_omega, ``mem_subset'.iff_omega, ``mem_separate'.iff_omega]) | ||
| (simp_attrs := #[`bv_toNat]) | ||
| (useDefaultSimprocs := false) | ||
| return {cfg, bvToNatSimpCtx, bvToNatSimprocs} | ||
| end Context | ||
|
|
||
| abbrev MemOmegaM := (ReaderT Context TacticM) | ||
|
|
||
| namespace MemOmegaM | ||
|
|
||
| def run (ctx : Context) (x : MemOmegaM α) : TacticM α := ReaderT.run x ctx | ||
|
|
||
| end MemOmegaM | ||
|
|
||
| def memOmegaTac : MemOmegaM Unit := do | ||
| let g ← getMainGoal | ||
| g.withContext do | ||
| /- We need to explode all pairwise separate hyps -/ | ||
| let rawHyps ← getLocalHyps | ||
| let mut hyps := #[] | ||
| -- extract out structed values for all hyps. | ||
| for h in rawHyps do | ||
| hyps ← hypothesisOfExpr h hyps | ||
|
|
||
| -- only enable pairwise constraints if it is enabled. | ||
| let isPairwiseEnabled := (← readThe Context).cfg.explodePairwiseSeparate | ||
| hyps := hyps.filter (!·.isPairwiseSeparate || isPairwiseEnabled) | ||
|
|
||
| -- used specialized procedure that doesn't unfold everything for the easy case. | ||
| if ← closeMemSideCondition (← getMainGoal) (← readThe Context).bvToNatSimpCtx (← readThe Context).bvToNatSimprocs hyps then | ||
| return () | ||
| else | ||
| -- in the bad case, just rip through everything. | ||
| -- let _ ← Hypothesis.addOmegaFactsOfHyps (hyps.toList.filter (fun h => h.isPairwiseSeparate)) #[] | ||
| let _ ← Hypothesis.addOmegaFactsOfHyps hyps.toList #[] | ||
|
|
||
| TacticM.withTraceNode' m!"Reducion to omega" do | ||
| try | ||
| TacticM.traceLargeMsg m!"goal (Note: can be large)" m!"{← getMainGoal}" | ||
| omega (← readThe Context).bvToNatSimpCtx (← readThe Context).bvToNatSimprocs | ||
| trace[simp_mem.info] "{checkEmoji} `omega` succeeded." | ||
| catch e => | ||
| trace[simp_mem.info] "{crossEmoji} `omega` failed with error:\n{e.toMessageData}" | ||
|
|
||
|
|
||
| /-- | ||
| Allow elaboration of `MemOmegaConfig` arguments to tactics. | ||
| -/ | ||
| declare_config_elab elabMemOmegaConfig MemOmega.Config | ||
|
|
||
| /-- | ||
| The `mem_omega` tactic is a finishing tactic which is used to dispatch memory side conditions. | ||
| Broadly, the algorithm works as follows: | ||
| - It scans the set of hypotheses for `mem_separate`, `mem_subset`, and `mem_legal` hypotheses, and turns them into `omega` based information. | ||
| - It calls `omega` as a finishing tactic to close the current goal state. | ||
| - Cruicially, it **does not unfold** `pairwiseSeparate` constraints. We expect the user to do so. If they want `pairwiseSeparate` unfolded, then please use `mem_omega!`. | ||
| -/ | ||
| syntax (name := mem_omega) "mem_omega" (Lean.Parser.Tactic.config)? : tactic | ||
|
|
||
| /-- | ||
| The `mem_omega!` tactic is a finishing tactic, that is a more aggressive variant of `mem_omega`. | ||
| -/ | ||
| syntax (name := mem_omega_bang) "mem_omega!" (Lean.Parser.Tactic.config)? : tactic | ||
|
|
||
| @[tactic mem_omega] | ||
| def evalMemOmega : Tactic := fun | ||
| | `(tactic| mem_omega $[$cfg]?) => do | ||
| let cfg ← elabMemOmegaConfig (mkOptionalNode cfg) | ||
| memOmegaTac.run (← Context.init cfg) | ||
| | _ => throwUnsupportedSyntax | ||
|
|
||
| @[tactic mem_omega_bang] | ||
| def evalMemOmegaBang : Tactic := fun | ||
| | `(tactic| mem_omega! $[$cfg]?) => do | ||
| let cfg ← elabMemOmegaConfig (mkOptionalNode cfg) | ||
| memOmegaTac.run (← Context.init cfg.mkBang) | ||
| | _ => throwUnsupportedSyntax | ||
|
|
||
| end MemOmega |
This file contains 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
Oops, something went wrong.