Properties of dead-definition elimination

deadDefElimH, one backward pass with one hash set, returns deadDefElim's list (deadDefElimH_eq): the hash set holds exactly the identifiers that deadDefElim recomputes.

Erasure keeps every property of all nested statements that does not look into branches or bodies (deadDefElim_allSubstmts), the order conditions Block.nondetIteLast and Block.onlyChecksAfterAssert (deadDefElim_nondetIteLast, deadDefElim_onlyChecksAfterAssert) and the reads of defined names Block.readsDefined (deadDefElim_readsDefined).

For Core statement lists, the facts the trace over-approximation (DeadDefElimCoreCorrect) is built from: the correspondence of final environments (DDOut); a Core run of a call-free configuration is a run over EvalE and back (star_evalE, star_core); and erasure keeps the initial-environment gate BlockInitEnvWF of a list without loops and calls (blockInitEnvWF_dd), through its defined variables (dd_definedVars), its init types (dd_initTypes) and def-use well-formedness (dd_defUse).

Key theorems: deadDefElimH_eq, deadDefElim_allSubstmts, deadDefElim_nondetIteLast, deadDefElim_onlyChecksAfterAssert, deadDefElim_readsDefined, star_evalE, star_core, blockInitEnvWF_dd.

Key definitions: Core.DeadDefElim.DDOut, Core.DeadDefElim.CallFree.

theorem Imperative.DeadDefElim.deadDefElimH_eq {P : PureExpr} [BEq P.Ident] [LawfulBEq P.Ident] [HasFvars P] [Hashable P.Ident] (live : List P.Ident) (ss : BigStep.PStmts P) : deadDefElimH live ss = deadDefElim live ss

The one-pass hash-set version deadDefElimH returns the list deadDefElim specifies.

Erasure keeps the order conditions and the reads of defined names

theorem Imperative.DeadDefElim.deadDefElim_allSubstmts {P : PureExpr} [BEq P.Ident] [HasFvars P] {f : Stmt P (CmdExt P) → Bool} (hite : ∀ (c : ExprOrNondet P) (t e t' e' : List (Stmt P (CmdExt P))) (md : MetaData P), f (Stmt.ite c t e md) = f (Stmt.ite c t' e' md)) (hblock : ∀ (l : String) (b b' : List (Stmt P (CmdExt P))) (md : MetaData P), f (Stmt.block l b md) = f (Stmt.block l b' md)) (live : List P.Ident) (ss : BigStep.PStmts P) : Block.allSubstmts f ss = true → Block.allSubstmts f (deadDefElim live ss) = true

Erasure keeps every property of all nested statements whose value on an ite or a block does not depend on its branches or body: if f holds of every statement of ss, nested ones included (Block.allSubstmts f), it holds of every statement of deadDefElim live ss.

theorem Imperative.DeadDefElim.deadDefElim_nondetIteLast {P : PureExpr} [BEq P.Ident] [HasFvars P] (live : List P.Ident) (ss : BigStep.PStmts P) : Block.nondetIteLast ss = true → Block.nondetIteLast (deadDefElim live ss) = true

Erasure keeps every nondeterministic ite last in its list (Block.nondetIteLast).

theorem Imperative.DeadDefElim.deadDefElim_onlyChecksAfterAssert {P : PureExpr} [BEq P.Ident] [HasFvars P] (live : List P.Ident) (ss : BigStep.PStmts P) : Block.onlyChecksAfterAssert ss = true → Block.onlyChecksAfterAssert (deadDefElim live ss) = true

Erasure keeps only checks after every assert (Block.onlyChecksAfterAssert).

theorem Imperative.DeadDefElim.deadDefElim_readsDefined {P : PureExpr} [BEq P.Ident] [LawfulBEq P.Ident] [HasFvars P] (live : List P.Ident) {D : List P.Ident} {ss : BigStep.PStmts P} (h : Block.readsDefined D ss = true) : Block.readsDefined D (deadDefElim live ss) = true

Erasure keeps the reads of defined names: if ss reads only names defined before each statement, starting from the defined names D (Block.readsDefined), so does deadDefElim live ss.

Final environments of the output

def Core.DeadDefElim.DDOut (ρ ρ' : Imperative.Env Expression) : Prop

The environment ρ' at the end of a run of the output of deadDefElim corresponds to the environment ρ at the end of the source run: same factory, and the store of ρ' is the store of ρ with some bindings removed.

Equations

• Core.DeadDefElim.DDOut ρ ρ' = (ρ'.factory = ρ.factory ∧ Imperative.StoreAgreement ρ'.store ρ.store)

Call-free Core runs are runs over EvalE

def Core.DeadDefElim.CallFree : Imperative.Config Expression Command → Prop

Every statement still to run in the configuration makes no procedure call.

Equations

• Core.DeadDefElim.CallFree (Imperative.Config.stmt s a) = (Core.Statements.noCalls [s] = true)
• Core.DeadDefElim.CallFree (Imperative.Config.stmts ss a) = (Core.Statements.noCalls ss = true)
• Core.DeadDefElim.CallFree (Imperative.Config.terminal a) = True
• Core.DeadDefElim.CallFree (Imperative.Config.exiting a a_1) = True
• Core.DeadDefElim.CallFree (Imperative.Config.block a a_1 c) = Core.DeadDefElim.CallFree c
• Core.DeadDefElim.CallFree (c.seq ss) = (Core.DeadDefElim.CallFree c ∧ Core.Statements.noCalls ss = true)

theorem Core.DeadDefElim.star_evalE {π : String → Option Procedure} {c c' : Imperative.Config Expression Command} {tr : List (Imperative.Event Expression)} (hs : (Logic.EventLang.coreBlock π).traceStar c tr c') (hI : CallFree c) : Imperative.StepStmtStarE Expression Imperative.BigStep.EvalE c tr c'

A Core run of a call-free configuration is a run over EvalE.

theorem Core.DeadDefElim.star_core (π : String → Option Procedure) {c c' : Imperative.Config Expression Command} {tr : List (Imperative.Event Expression)} (hs : Imperative.StepStmtStarE Expression Imperative.BigStep.EvalE c tr c') : (Logic.EventLang.coreBlock π).traceStar c tr c'

A run over EvalE is a Core run.

Initial-environment well-formedness of the output

theorem Core.DeadDefElim.blockInitEnvWF_dd {params : Logic.InitEnvWFParams} {ss : Statements} {ρ : Imperative.Env Expression} (hss : Imperative.Block.noLoops ss = true) (hnc : ss.noCalls = true) (h : Logic.BlockInitEnvWF params ss ρ) : Logic.BlockInitEnvWF params (Imperative.DeadDefElim.deadDefElim [] ss) ρ

The output of deadDefElim is well formed from every environment the input is: the gate BlockInitEnvWF of the input gives that of the output.