From 37d88f070afc52e68e31514113b978496fbb1ba7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 30 Jun 2026 23:21:00 -0500 Subject: [PATCH] Remove 'prog.code s = some bs' argument to `eval` --- lean/Main.lean | 4 +- lean/Spa/Analysis/Forward.lean | 46 ++++-------------- lean/Spa/Analysis/Forward/Adapters.lean | 54 +++++++++++---------- lean/Spa/Analysis/Forward/Evaluation.lean | 10 ++-- lean/Spa/Analysis/Reaching.lean | 57 ++++++++++++----------- 5 files changed, 78 insertions(+), 93 deletions(-) diff --git a/lean/Main.lean b/lean/Main.lean index 7b327c5..56a15e8 100644 --- a/lean/Main.lean +++ b/lean/Main.lean @@ -1,5 +1,6 @@ import Spa.Analysis.Sign import Spa.Analysis.Constant +import Spa.Analysis.Reaching import Spa.Language.Notation namespace Spa @@ -32,4 +33,5 @@ end Spa def main : IO Unit := IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++ - Spa.SignAnalysis.output Spa.testProgram) + Spa.SignAnalysis.output Spa.testProgram ++ "\n" ++ + Spa.ReachingAnalysis.output Spa.testProgram) diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean index f51dc8f..28961cf 100644 --- a/lean/Spa/Analysis/Forward.lean +++ b/lean/Spa/Analysis/Forward.lean @@ -9,22 +9,12 @@ namespace Forward variable {L : Type} [FiniteHeightLattice L] {prog : Program} [E : StmtEvaluator L prog] -def evalStmtOrNone (s : prog.State) (o : Option BasicStmt) (hco : prog.code s = o) - (vs : VariableValues L prog) : VariableValues L prog := - o.elimEq vs (fun bs h => E.eval s bs (hco.trans h)) - -lemma evalStmtOrNone_mono (s : prog.State) (o : Option BasicStmt) - (hco : prog.code s = o) : Monotone (evalStmtOrNone (L := L) s o hco) := - elimEq_self_mono o (fun bs h vs => E.eval s bs (hco.trans h) vs) - (fun bs h => E.eval_mono s bs (hco.trans h)) - def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) : - VariableValues L prog := - evalStmtOrNone s (prog.code s) rfl (variablesAt s sv) + VariableValues L prog := E.eval s (variablesAt s sv) lemma updateVariablesForState_mono (s : prog.State) : Monotone (updateVariablesForState (L := L) s) := fun _ _ hle => - evalStmtOrNone_mono s (prog.code s) rfl (variablesAt_le hle s) + E.eval_mono s (variablesAt_le hle s) def updateAll (sv : StateVariables L prog) : StateVariables L prog := FiniteMap.generalizedUpdate id updateVariablesForState @@ -65,32 +55,25 @@ lemma joinForKey_initialState : class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program) [E : StmtEvaluator L prog] [S : StateInterpretation L prog] where - step : (s : prog.State) → {ρ₁ ρ₂ : Env} → {bs : BasicStmt} → - prog.code s = some bs → EvalBasicStmt ρ₁ bs ρ₂ → S.St ρ₁ → S.St ρ₂ - valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env} {bs : BasicStmt} + step : (s : prog.State) → {ρ₁ ρ₂ : Env} → EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → S.St ρ₁ → S.St ρ₂ + valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env} {vs : VariableValues L prog} {st : S.St ρ₁}, - (hcode : prog.code s = some bs) → (hbs : EvalBasicStmt ρ₁ bs ρ₂) → ⟦ vs ⟧ ρ₁ st → - ⟦ E.eval s bs hcode vs ⟧ ρ₂ (step s hcode hbs st) + (hbs : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) → ⟦ vs ⟧ ρ₁ st → + ⟦ E.eval s vs ⟧ ρ₂ (step s hbs st) botV_init : ⟦ botV L prog ⟧ [] S.init instance [LatticeInterpretation L] [ValidStmtEvaluator L prog] : ValidStateEvaluator L prog where - step := by intro _ _ _ _ _ _ _; exact PUnit.unit - valid := by intro _ _ _ _ _ _ hcode hbs hvs; exact ValidStmtEvaluator.valid hcode hbs hvs + step := by intro _ _ _ _ _; exact PUnit.unit + valid := by intro _ _ _ _ _ hbs hvs; exact ValidStmtEvaluator.valid hbs hvs botV_init := by intro k l _ v hmem; cases hmem section variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog] -noncomputable def stepStmtOrNone (s : prog.State) {ρ₁ ρ₂ : Env} : - (o : Option BasicStmt) → prog.code s = o → EvalBasicStmtOpt ρ₁ o ρ₂ → - S.St ρ₁ → S.St ρ₂ - | none, _, .none, st => st - | some _, hco, .some hbs, st => V.step s hco hbs st - noncomputable def stepNode (s : prog.State) {ρ₁ ρ₂ : Env} (h : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) (st : S.St ρ₁) : S.St ρ₂ := - stepStmtOrNone s (prog.code s) rfl h st + V.step s h st noncomputable def stepTraceState : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} → @@ -121,15 +104,6 @@ inductive Reaches : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} → Reaches rest (stepNode s₁ hnode st₁) s ρin ρout stin stout → Reaches (.edge hnode hedge rest) st₁ s ρin ρout stin stout -omit [DecidableEq L] in -lemma evalStmtOrNone_valid {s : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁} - {vs : VariableValues L prog} (o : Option BasicStmt) (hco : prog.code s = o) - (he : EvalBasicStmtOpt ρ₁ o ρ₂) (hvs : ⟦ vs ⟧ ρ₁ st) : - ⟦ evalStmtOrNone s o hco vs ⟧ ρ₂ (stepStmtOrNone s o hco he st) := by - cases he with - | none => exact hvs - | some hbs => exact V.valid s hco hbs hvs - omit [DecidableEq L] in lemma updateAll_matches {s : prog.State} {sv : StateVariables L prog} {ρ₁ ρ₂ : Env} {st : S.St ρ₁} @@ -137,7 +111,7 @@ lemma updateAll_matches {s : prog.State} {sv : StateVariables L prog} (hvs : ⟦ variablesAt s sv ⟧ ρ₁ st) : ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ (stepNode s hnode st) := by rw [variablesAt_updateAll] - exact evalStmtOrNone_valid (prog.code s) rfl hnode hvs + exact V.valid s hnode hvs lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁} (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st) diff --git a/lean/Spa/Analysis/Forward/Adapters.lean b/lean/Spa/Analysis/Forward/Adapters.lean index 8baeea4..281f2ef 100644 --- a/lean/Spa/Analysis/Forward/Adapters.lean +++ b/lean/Spa/Analysis/Forward/Adapters.lean @@ -14,44 +14,50 @@ lemma updateVariablesFromExpression_mono (k : String) (e : Expr) : Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) := FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e) -def evalBasicStmt (s : prog.State) (bs : BasicStmt) (_h : prog.code s = some bs) +def evalBasicStmt (bs : BasicStmt) (vs : VariableValues L prog) : VariableValues L prog := match bs with | .assign k e => updateVariablesFromExpression k e vs | .noop => vs -lemma evalBasicStmt_mono (s : prog.State) (bs : BasicStmt) (h : prog.code s = some bs) : - Monotone (evalBasicStmt (L := L) (prog := prog) s bs h) := by +lemma evalBasicStmt_mono (bs : BasicStmt) : + Monotone (evalBasicStmt (L := L) (prog := prog) bs) := by cases bs with | assign k e => exact updateVariablesFromExpression_mono k e | noop => exact monotone_id +def evalBasicStmtOpt (obs : Option BasicStmt) + (vs : VariableValues L prog) : VariableValues L prog := + match obs with + | none => vs + | some bs => evalBasicStmt bs vs + +lemma evalBasicStmtOpt_mono (obs : Option BasicStmt) : + Monotone (evalBasicStmtOpt (L := L) (prog := prog) obs) := by + cases obs <;> unfold evalBasicStmtOpt + · exact monotone_id + · apply evalBasicStmt_mono + instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog := - ⟨evalBasicStmt, evalBasicStmt_mono⟩ + ⟨evalBasicStmtOpt ∘ prog.code, + by intro s; simp; exact (evalBasicStmtOpt_mono (prog.code s))⟩ instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L] [ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by constructor - intro s vs ρ₁ ρ₂ bs hcode hbs hvs - cases hbs with - | noop => exact hvs - | assign k e v hev => - intro k' l hk'l v' hv' - cases hv' with - | here => - have hk'l₀ : (k, l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id - (fun _ vs => E.eval e vs) [k] vs := hk'l - have hl := FiniteMap.generalizedUpdate_mem_eq (f := id) - (g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hk'l₀ - rw [hl] - exact ValidExprEvaluator.valid hev hvs - | there _ _ _ _ _ hne hmem' => - have hk'l₀ : (k', l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id - (fun _ vs => E.eval e vs) [k] vs := hk'l - have hk'l' : (k', l) ∈ (id vs : VariableValues L prog) := - FiniteMap.generalizedUpdate_not_mem_backward - (fun hmem => hne (List.mem_singleton.mp hmem)) hk'l₀ - exact hvs _ _ hk'l' _ hmem' + simp [StmtEvaluator.eval, evalBasicStmtOpt] + intro s vs ρ₁ ρ₂; generalize prog.code s = obs; intro hev hvs + rcases hev with _ | @⟨_,bs,hev⟩ <;> try simpa + rcases hev with _ | @⟨k, e, v, hev⟩ <;> try simpa + intros k' l' hkl' v' hρ + rcases hρ with _ | ⟨_,_,_,_,_,hne,hmem⟩ <;> simp [evalBasicStmt] at hkl' + · have hl := FiniteMap.generalizedUpdate_mem_eq (f := id) + (g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hkl' + rewrite [hl]; simp + exact ValidExprEvaluator.valid hev hvs + · have hl := FiniteMap.generalizedUpdate_not_mem_backward + (fun hmem => hne (List.mem_singleton.mp hmem)) hkl' + apply hvs _ _ hl _ hmem end Forward diff --git a/lean/Spa/Analysis/Forward/Evaluation.lean b/lean/Spa/Analysis/Forward/Evaluation.lean index c55b121..b248cd2 100644 --- a/lean/Spa/Analysis/Forward/Evaluation.lean +++ b/lean/Spa/Analysis/Forward/Evaluation.lean @@ -7,9 +7,8 @@ namespace Forward variable (L : Type) [Lattice L] (prog : Program) class StmtEvaluator where - eval : (s : prog.State) → (bs : BasicStmt) → prog.code s = some bs → - VariableValues L prog → VariableValues L prog - eval_mono : ∀ s bs h, Monotone (eval s bs h) + eval : prog.State → VariableValues L prog → VariableValues L prog + eval_mono : ∀ s, Monotone (eval s) class ExprEvaluator where eval : Expr → VariableValues L prog → L @@ -22,9 +21,8 @@ class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] : class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] : Prop where - valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env} - {bs : BasicStmt} (hcode : prog.code s = some bs), - EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ () → ⟦ E.eval s bs hcode vs ⟧ ρ₂ () + valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}, + EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ () → ⟦ E.eval s vs ⟧ ρ₂ () end Forward diff --git a/lean/Spa/Analysis/Reaching.lean b/lean/Spa/Analysis/Reaching.lean index fdbd202..cc87122 100644 --- a/lean/Spa/Analysis/Reaching.lean +++ b/lean/Spa/Analysis/Reaching.lean @@ -19,23 +19,23 @@ namespace ReachingAnalysis variable (prog : Program) -def genSet (s : prog.State) {bs : BasicStmt} (h : prog.code s = some bs) : - DefSet prog := - {prog.nodeIdOfNonempty s h} +def genSet (s : prog.State) : DefSet prog := (prog.nodeIdOf s).elim {} (fun x => {x}) -def eval (s : prog.State) : - (bs : BasicStmt) → prog.code s = some bs → - VariableValues (DefSet prog) prog → VariableValues (DefSet prog) prog - | .assign k _, h, vs => - FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s h) [k] vs - | .noop, _, vs => vs +def eval (s : prog.State) (vs : VariableValues (DefSet prog) prog) : VariableValues (DefSet prog) prog := + match prog.code s with + | none => vs + | some bs => + match bs with + | .assign k _ => FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s) [k] vs + | .noop => vs -lemma eval_mono (s : prog.State) (bs : BasicStmt) (h : prog.code s = some bs) : - Monotone (eval prog s bs h) := by - cases bs with - | assign k e => - exact FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const) - | noop => exact monotone_id +lemma eval_mono (s : prog.State) : + Monotone (eval prog s) := by + intros vs₁ vs₂ hle + unfold eval; split <;> try simpa + split <;> try simpa + apply FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const) + assumption instance stmtEvaluator : StmtEvaluator (DefSet prog) prog := ⟨eval prog, eval_mono prog⟩ @@ -45,18 +45,18 @@ def output : String := inductive Run (prog : Program) where | nil : Run prog - | cons (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs) + | cons (s : prog.State) (bs : BasicStmt) (rest : Run prog) : Run prog @[aesop unsafe cases] inductive LastAssign (prog : Program) (x : String) : Run prog → prog.NodeId → Prop | here (s : prog.State) (e : Expr) (hc : prog.code s = some (.assign x e)) (rest : Run prog) : - LastAssign prog x (Run.cons s (.assign x e) hc rest) (prog.nodeIdOfNonempty s hc) + LastAssign prog x (Run.cons s (.assign x e) rest) (prog.nodeIdOfNonempty s hc) | there (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs) (rest : Run prog) {n : prog.NodeId} : (∀ e, bs ≠ .assign x e) → LastAssign prog x rest n → - LastAssign prog x (Run.cons s bs hc rest) n + LastAssign prog x (Run.cons s bs rest) n instance stateInterp : StateInterpretation (DefSet prog) prog where St := fun _ => Run prog @@ -72,22 +72,27 @@ instance stateInterp : StateInterpretation (DefSet prog) prog where obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_inf hmem aesop (add simp Finset.mem_inter) +private def stepAt (s : prog.State) (obs : Option BasicStmt) { ρ₁ ρ₂ : Env} : EvalBasicStmtOpt ρ₁ obs ρ₂ → Run prog → Run prog + | .none, rest => rest + | .some (bs := bs) _, rest => Run.cons s bs rest + instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where - step := by intro s _ _ bs hcode _ rest; exact Run.cons s bs hcode rest + step := fun s ρ₁ ρ₂ => stepAt prog s (prog.code s) valid := by - intro s ρ₁ ρ₂ bs vs st hcode hbs hvs + simp [StmtEvaluator.eval, eval]; + intro s ρ₁ ρ₂ vs; generalize prog.code s = obs; intro hst hbs hvs + rcases hbs with _ | @⟨_, bs, hbs⟩; try (simpa [stepAt]) cases hbs with | noop => intro x assigners hmem n hla; aesop | assign x e v hev => - intro k assigners hmem n hla - have hmem2 : (k, assigners) ∈ - FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s hcode) [x] vs := hmem + simp; intro k assigners hmem n hla by_cases hx : k = x · subst hx - have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem2 - aesop (add simp [genSet, Finset.mem_singleton]) + have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem + rcases hla + <;> simp [Program.nodeIdOfNonempty, hd, genSet, Option.get] <;> aesop · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward - (fun hc => hx (List.mem_singleton.mp hc)) hmem2 + (fun hc => hx (List.mem_singleton.mp hc)) hmem aesop botV_init := by intro x assigners _ n hla; cases hla