Migrate Reaching.lean to projections via a generic Trace.steps
Finish the projection migration for reaching definitions by replacing the accumulator-style runOfTrace*From definitions and their hand-rolled re-association lemmas with a single analysis-agnostic projection: Trace.steps / Traceₗ.steps, the chronological List of executed (index, statement) pairs. Its four simp lemmas are one-line inductions, with all re-association falling out of mathlib's List.append_assoc and List.reverse_append. Run is now an abbrev for List (State × BasicStmt) (latest-first, so LastAssign keeps its first-match structure) and runOfTrace is just steps.reverse. Also hoist the generic reaches_final_post into Forward.lean, letting analyze_correct' be stated directly about S.Post (prog.trace hrun). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
@@ -131,6 +131,15 @@ def reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
|
||||
| .edge hnode hedge rest =>
|
||||
let ⟨ρin, r'⟩ := reaches_final rest; ⟨ρin, .edge_there hnode hedge _ r'⟩
|
||||
|
||||
omit [DecidableEq L] in
|
||||
/-- Reaching the final node covers the whole trace. -/
|
||||
@[simp] lemma reaches_final_post {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
|
||||
(tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
|
||||
(reaches_final tr).2.post = tr := by
|
||||
induction tr with
|
||||
| single hnode => rfl
|
||||
| edge hnode hedge rest ih => simp [reaches_final, Reaches.post, ih]
|
||||
|
||||
variable (L prog) in
|
||||
/-- Soundness at every program point reached during execution: for any node `s` visited
|
||||
by the run `hrun` (witnessed by `hr`), the analysis result over-approximates both the
|
||||
@@ -148,11 +157,9 @@ theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
|
||||
variable (L prog) in
|
||||
theorem analyze_correct'
|
||||
{ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
|
||||
⟦ variablesAt prog.finalState (result L prog) ⟧ (S.Post (reaches_final (prog.trace hrun)).2.post) := by
|
||||
let idk₀ := prog.trace hrun
|
||||
have ⟨_, idk₁⟩ := reaches_final idk₀
|
||||
have ⟨_, idk₂⟩ := analyze_correct_at L prog hrun idk₁
|
||||
assumption
|
||||
⟦ variablesAt prog.finalState (result L prog) ⟧ (S.Post (prog.trace hrun)) := by
|
||||
have h := (analyze_correct_at L prog hrun (reaches_final (prog.trace hrun)).2).2
|
||||
rwa [reaches_final_post] at h
|
||||
|
||||
end
|
||||
|
||||
|
||||
@@ -43,69 +43,91 @@ instance stmtEvaluator : StmtEvaluator (DefSet prog) prog :=
|
||||
def output : String :=
|
||||
show' (result (DefSet prog) prog)
|
||||
|
||||
inductive Run (prog : Program) where
|
||||
| nil : Run prog
|
||||
| cons (s : prog.State) (bs : BasicStmt)
|
||||
(rest : Run prog) : Run prog
|
||||
/-- The statements a trace executed, paired with the state each executed at,
|
||||
most recent first (matching `LastAssign`, which scans for the most recent
|
||||
assignment). This is `Trace.steps` (chronological) reversed, so facts about
|
||||
concatenating traces reduce to mathlib's `List.append`/`List.reverse` lemmas. -/
|
||||
abbrev Run (prog : Program) : Type := List (prog.State × BasicStmt)
|
||||
|
||||
@[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) rest) (prog.nodeIdOfNonempty s hc)
|
||||
LastAssign prog x ((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 rest) n
|
||||
LastAssign prog x ((s, bs) :: rest) n
|
||||
|
||||
def runOfTraceₗ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
|
||||
(tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog :=
|
||||
tr.steps.reverse
|
||||
|
||||
def runOfTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
|
||||
(tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog :=
|
||||
tr.steps.reverse
|
||||
|
||||
instance stateInterp : StateInterpretation (DefSet prog) prog where
|
||||
St := fun _ => Run prog
|
||||
init := Run.nil
|
||||
interp vs _ run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs →
|
||||
Proj := Run prog
|
||||
Pre := @runOfTraceₗ prog
|
||||
Post := @runOfTrace prog
|
||||
|
||||
interp vs run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs →
|
||||
∀ (n : prog.NodeId), LastAssign prog x run n → n ∈ assigners
|
||||
interp_sup := by
|
||||
intro vs₁ vs₂ ρ run h x assigners hmem n hla
|
||||
intro vs₁ vs₂ run h x assigners hmem n hla
|
||||
obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
|
||||
aesop (add simp Finset.mem_union)
|
||||
interp_inf := by
|
||||
intro vs₁ vs₂ ρ run h x assigners hmem n hla
|
||||
intro vs₁ vs₂ run h x assigners hmem n hla
|
||||
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
|
||||
post_pre := by
|
||||
intro vs s₁ s₂ s₃ ρ₁ ρ₂ tr hedge hvs
|
||||
simpa [runOfTrace, runOfTraceₗ] using hvs
|
||||
|
||||
private lemma valid_step (s : prog.State) {ρ₁ ρ₂ : Env}
|
||||
{obs : Option BasicStmt} (hcode : prog.code s = obs)
|
||||
(hbs : EvalBasicStmtOpt ρ₁ obs ρ₂)
|
||||
{vs : VariableValues (DefSet prog) prog} {run : Run prog}
|
||||
(hvs : ⟦vs⟧ run) :
|
||||
⟦eval prog s vs⟧ ((hbs.steps s).reverse ++ run) := by
|
||||
cases hbs with
|
||||
| none => simpa [eval, hcode, EvalBasicStmtOpt.steps] using hvs
|
||||
| some hbs =>
|
||||
cases hbs with
|
||||
| noop =>
|
||||
simp [eval, hcode, EvalBasicStmtOpt.steps]
|
||||
intro x assigners hmem n hla; aesop
|
||||
| assign x e v hev =>
|
||||
simp [eval, hcode, EvalBasicStmtOpt.steps]; intro k assigners hmem n hla
|
||||
by_cases hx : k = x
|
||||
· subst hx
|
||||
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)) hmem
|
||||
aesop
|
||||
|
||||
instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where
|
||||
step := fun s ρ₁ ρ₂ => stepAt prog s (prog.code s)
|
||||
valid := by
|
||||
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 =>
|
||||
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) 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)) hmem
|
||||
aesop
|
||||
intro s₁ s₂ ρ₁ ρ₂ ρ₃ vs tr hbs hvs
|
||||
show ⟦eval prog s₂ vs⟧ (runOfTrace prog (tr ++ hbs))
|
||||
simpa [runOfTrace, runOfTraceₗ] using valid_step prog s₂ rfl hbs hvs
|
||||
botV_init := by intro x assigners _ n hla; cases hla
|
||||
|
||||
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
|
||||
⟦ variablesAt prog.finalState (result (DefSet prog) prog) ⟧ ρ
|
||||
(stepTraceState (prog.trace hrun) (stateInterp prog).init) :=
|
||||
Forward.analyze_correct_state (DefSet prog) prog hrun
|
||||
⟦ variablesAt prog.finalState (result (DefSet prog) prog) ⟧
|
||||
(runOfTrace prog (prog.trace hrun)) :=
|
||||
Forward.analyze_correct' (DefSet prog) prog hrun
|
||||
|
||||
theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
|
||||
{s : prog.State} {ρin ρout : Env} {stin : Run prog} {stout : Run prog}
|
||||
(hr : Reaches (prog.trace hrun) (stateInterp prog).init s ρin ρout stin stout) :
|
||||
⟦ joinForKey s (result (DefSet prog) prog) ⟧ ρin stin
|
||||
∧ ⟦ variablesAt s (result (DefSet prog) prog) ⟧ ρout stout :=
|
||||
{s : prog.State} {ρin ρout : Env}
|
||||
(hr : Reaches (prog.trace hrun) s ρin ρout) :
|
||||
⟦ joinForKey s (result (DefSet prog) prog) ⟧ (runOfTraceₗ prog hr.pre)
|
||||
∧ ⟦ variablesAt s (result (DefSet prog) prog) ⟧ (runOfTrace prog hr.post) :=
|
||||
Forward.analyze_correct_at (DefSet prog) prog hrun hr
|
||||
|
||||
end ReachingAnalysis
|
||||
|
||||
@@ -136,6 +136,61 @@ instance instHAppendTraceTraceR {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ
|
||||
HAppend (Trace g idx₁ idx₂ ρ₁ ρ₂) (Traceᵣ g idx₂ idx₃ ρ₂ ρ₃) (Trace g idx₁ idx₃ ρ₁ ρ₃) where
|
||||
hAppend := Trace.appendRight
|
||||
|
||||
/-!
|
||||
|
||||
## Trace Steps
|
||||
|
||||
Analyses that care about *which statements executed* (e.g. reaching
|
||||
definitions) need to project a trace down to its list of executed statements.
|
||||
Defining that projection here, once, as a chronological mathlib `List` means
|
||||
all the re-association facts about concatenating traces come for free from
|
||||
`List.append_assoc` and friends, instead of being re-proven per analysis. -/
|
||||
|
||||
/-- The (index, statement) pairs executed by a single optional-statement step:
|
||||
none if the node is empty, and the node's statement otherwise. -/
|
||||
def EvalBasicStmtOpt.steps {α : Type*} (idx : α) {ρ₁ ρ₂ : Env} {obs : Option BasicStmt} :
|
||||
EvalBasicStmtOpt ρ₁ obs ρ₂ → List (α × BasicStmt)
|
||||
| .none => []
|
||||
| .some (bs := bs) _ => [(idx, bs)]
|
||||
|
||||
/-- The statements executed by a left-open trace, in chronological order. -/
|
||||
def Traceₗ.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} :
|
||||
Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt)
|
||||
| .nil => []
|
||||
| .cons (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps
|
||||
|
||||
/-- The statements executed by a trace, in chronological order. -/
|
||||
def Trace.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} :
|
||||
Trace g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt)
|
||||
| .single (idx := idx) hnode => hnode.steps idx
|
||||
| .edge (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps
|
||||
|
||||
@[simp] lemma Traceₗ.steps_append {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
|
||||
{ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
|
||||
(tr₂ : Traceₗ g idx₂ idx₃ ρ₂ ρ₃) :
|
||||
(tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by
|
||||
show (tr₁.append tr₂).steps = _
|
||||
induction tr₁ <;> simp [Traceₗ.append, Traceₗ.steps, *]
|
||||
|
||||
@[simp] lemma Traceₗ.steps_appendTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
|
||||
{ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
|
||||
(tr₂ : Trace g idx₂ idx₃ ρ₂ ρ₃) :
|
||||
(tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by
|
||||
show (tr₁.appendTrace tr₂).steps = _
|
||||
induction tr₁ <;> simp [Traceₗ.appendTrace, Traceₗ.steps, Trace.steps, *]
|
||||
|
||||
@[simp] lemma Traceₗ.steps_appendStep {g : Graph} {idx₁ idx₂ : g.Index}
|
||||
{ρ₁ ρ₂ ρ₃ : Env} (tr : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
|
||||
(hbs : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) :
|
||||
(tr ++ hbs).steps = tr.steps ++ hbs.steps idx₂ :=
|
||||
Traceₗ.steps_appendTrace tr (Trace.single hbs)
|
||||
|
||||
@[simp] lemma Trace.steps_addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
|
||||
{ρ₁ ρ₂ : Env} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂)
|
||||
(hedge : (idx₂, idx₃) ∈ g.edges) :
|
||||
(tr.addEdge hedge).steps = tr.steps := by
|
||||
induction tr <;> simp [Trace.addEdge, Trace.steps, Traceₗ.steps, *]
|
||||
|
||||
@[simp] lemma Traceₗ.append_addEdge {g : Graph}
|
||||
{idx₁ idx₂ idx₃ idx₄ : g.Index} {ρ₁ ρ₂ ρ₃ ρ₄ : Env}
|
||||
(trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
|
||||
|
||||
Reference in New Issue
Block a user