Erasing unread definitions of an obligation program

deadDefElim live ss removes from the statement list ss every init x : T := e (or init x : T := *) whose variable no later statement mentions, whatever T and e. "Later" is the rest of the statement's list after erasure, and, for a statement of a branch or block body, also everything after the enclosing statement (live, the identifiers mentioned after the list); for a statement of the then branch of an ite, it also includes the else branch after erasure. The rest of a list is processed before its head, a branch or block body after the rest of its enclosing list, and the else branch of an ite before its then branch, so one pass reaches the fixpoint: no remaining init has an unmentioned variable. No other statement is removed or changed.

Erasing an unread init never removes a failure (DeadDefElimCorrect).

deadDefElim recomputes the identifiers of the rest of a list at each statement. deadDefElimH computes the same list (deadDefElimH_eq in DeadDefElimProps) in one backward pass that carries the identifiers mentioned later in one hash set.

For Core, Core.DeadDefElim.deadDefElimProgram runs deadDefElimH on every structured procedure body, and Core.deadDefElimPipelinePhase is the pipeline phase that runs it (DeadDefElimCoreCorrect).

Key definitions: erasable, deadDefElim, deadDefElimS, deadDefElimH, Core.DeadDefElim.deadDefElimProgram, Core.deadDefElimPipelinePhase.

def Imperative.DeadDefElim.erasable {P : PureExpr} [BEq P.Ident] (live : List P.Ident) : Stmt P (CmdExt P) → Bool

Is s an init whose variable is not in live?

Equations

• Imperative.DeadDefElim.erasable live (Imperative.Stmt.cmd (Imperative.CmdExt.cmd (Imperative.Cmd.init x_1 ty e md))) = !live.contains x_1
• Imperative.DeadDefElim.erasable live x✝ = false

def Imperative.DeadDefElim.deadDefElim {P : PureExpr} [BEq P.Ident] [HasFvars P] (live : List P.Ident) : List (Stmt P (CmdExt P)) → List (Stmt P (CmdExt P))

The statement list without its unread inits, live being the identifiers mentioned after the list.

Equations

• One or more equations did not get rendered due to their size.
• Imperative.DeadDefElim.deadDefElim live [] = []

def Imperative.DeadDefElim.deadDefElimS {P : PureExpr} [BEq P.Ident] [HasFvars P] (live : List P.Ident) : Stmt P (CmdExt P) → Stmt P (CmdExt P)

The statement with the unread inits of its branches or body removed, live being the identifiers mentioned after it; the then branch of an ite is processed with the identifiers of the processed else branch added.

Equations

• One or more equations did not get rendered due to their size.
• Imperative.DeadDefElim.deadDefElimS live (Imperative.Stmt.block l ss md) = Imperative.Stmt.block l (Imperative.DeadDefElim.deadDefElim live ss) md
• Imperative.DeadDefElim.deadDefElimS live x✝ = x✝

def Imperative.DeadDefElim.insertFV {P : PureExpr} [BEq P.Ident] [HasFvars P] [Hashable P.Ident] (h : Std.HashSet P.Ident) (e : P.Expr) : Std.HashSet P.Ident

Insert the free variables of an expression.

Equations

• Imperative.DeadDefElim.insertFV h e = List.foldl (fun (x1 : Std.HashSet P.Ident) (x2 : P.Ident) => x1.insert x2) h (Imperative.HasFvars.getFvars e)

def Imperative.DeadDefElim.insertGuard {P : PureExpr} [BEq P.Ident] [HasFvars P] [Hashable P.Ident] (h : Std.HashSet P.Ident) : ExprOrNondet P → Std.HashSet P.Ident

Insert the free variables of a guard (ExprOrNondet.getVars).

Equations

• Imperative.DeadDefElim.insertGuard h (Imperative.ExprOrNondet.det e) = Imperative.DeadDefElim.insertFV h e
• Imperative.DeadDefElim.insertGuard h Imperative.ExprOrNondet.nondet = h

def Imperative.DeadDefElim.insertCallArg {P : PureExpr} [BEq P.Ident] [HasFvars P] [Hashable P.Ident] (h : Std.HashSet P.Ident) : CallArg P → Std.HashSet P.Ident

Insert the identifiers of a call argument: the free variables of an input expression, the variable of an input-output or output argument.

Equations

• Imperative.DeadDefElim.insertCallArg h (Imperative.CallArg.inArg e) = Imperative.DeadDefElim.insertFV h e
• Imperative.DeadDefElim.insertCallArg h (Imperative.CallArg.inoutArg x_1) = h.insert x_1
• Imperative.DeadDefElim.insertCallArg h (Imperative.CallArg.outArg x_1) = h.insert x_1

def Imperative.DeadDefElim.insertCmd {P : PureExpr} [BEq P.Ident] [HasFvars P] [Hashable P.Ident] (h : Std.HashSet P.Ident) : CmdExt P → Std.HashSet P.Ident

Insert the identifiers of a kept command (Stmt.idents of the command).

Equations

• Imperative.DeadDefElim.insertCmd h (Imperative.CmdExt.cmd (Imperative.Cmd.init x_1 ty (Imperative.ExprOrNondet.det e) md)) = Imperative.DeadDefElim.insertFV (h.insert x_1) e
• Imperative.DeadDefElim.insertCmd h (Imperative.CmdExt.cmd (Imperative.Cmd.set x_1 (Imperative.ExprOrNondet.det e) md)) = Imperative.DeadDefElim.insertFV (h.insert x_1) e
• Imperative.DeadDefElim.insertCmd h (Imperative.CmdExt.cmd (Imperative.Cmd.init x_1 ty Imperative.ExprOrNondet.nondet md)) = h.insert x_1
• Imperative.DeadDefElim.insertCmd h (Imperative.CmdExt.cmd (Imperative.Cmd.set x_1 Imperative.ExprOrNondet.nondet md)) = h.insert x_1
• Imperative.DeadDefElim.insertCmd h (Imperative.CmdExt.cmd (Imperative.Cmd.assume label e md)) = Imperative.DeadDefElim.insertFV h e
• Imperative.DeadDefElim.insertCmd h (Imperative.CmdExt.cmd (Imperative.Cmd.assert label e md)) = Imperative.DeadDefElim.insertFV h e
• Imperative.DeadDefElim.insertCmd h (Imperative.CmdExt.cmd (Imperative.Cmd.cover label e md)) = Imperative.DeadDefElim.insertFV h e
• Imperative.DeadDefElim.insertCmd h (Imperative.CmdExt.call procName args md) = List.foldl Imperative.DeadDefElim.insertCallArg h args

def Imperative.DeadDefElim.insertIdents {P : PureExpr} [BEq P.Ident] [HasFvars P] [Hashable P.Ident] (h : Std.HashSet P.Ident) : List (Stmt P (CmdExt P)) → Std.HashSet P.Ident

Insert every identifier of a statement list (Block.idents).

Equations

• Imperative.DeadDefElim.insertIdents h [] = h
• Imperative.DeadDefElim.insertIdents h (s :: rest) = Imperative.DeadDefElim.insertIdents (Imperative.DeadDefElim.insertIdent h s) rest

def Imperative.DeadDefElim.insertIdent {P : PureExpr} [BEq P.Ident] [HasFvars P] [Hashable P.Ident] (h : Std.HashSet P.Ident) : Stmt P (CmdExt P) → Std.HashSet P.Ident

Insert every identifier of a statement (Stmt.idents).

Equations

• One or more equations did not get rendered due to their size.
• Imperative.DeadDefElim.insertIdent h (Imperative.Stmt.cmd c) = Imperative.DeadDefElim.insertCmd h c
• Imperative.DeadDefElim.insertIdent h (Imperative.Stmt.block label ss md) = Imperative.DeadDefElim.insertIdents h ss
• Imperative.DeadDefElim.insertIdent h (Imperative.Stmt.exit label md) = h
• Imperative.DeadDefElim.insertIdent h (Imperative.Stmt.typeDecl tc md) = h

@[irreducible]

def Imperative.DeadDefElim.deadDefElimHL {P : PureExpr} [BEq P.Ident] [HasFvars P] [Hashable P.Ident] (h : Std.HashSet P.Ident) : List (Stmt P (CmdExt P)) → List (Stmt P (CmdExt P)) × Std.HashSet P.Ident

deadDefElim in one backward pass: h holds the identifiers mentioned after the list; the result is the processed list and h with the identifiers of the processed list added. The rest of a list is processed before its head, the else branch of an ite before its then branch; each kept statement adds its own identifiers once.

Equations

• One or more equations did not get rendered due to their size.
• Imperative.DeadDefElim.deadDefElimHL h [] = ([], h)

def Imperative.DeadDefElim.deadDefElimH {P : PureExpr} [BEq P.Ident] [HasFvars P] [Hashable P.Ident] (live : List P.Ident) (ss : List (Stmt P (CmdExt P))) : List (Stmt P (CmdExt P))

deadDefElim in one backward pass with one hash set (deadDefElimHL).

Equations

• Imperative.DeadDefElim.deadDefElimH live ss = (Imperative.DeadDefElim.deadDefElimHL (Std.HashSet.ofList live) ss).fst

The Core phase

def Core.DeadDefElim.deadDefElimDecl : Decl → Decl × Bool

The declaration with the unread inits of its structured procedure body removed, and whether that body changed.

Equations

• One or more equations did not get rendered due to their size.
• Core.DeadDefElim.deadDefElimDecl x✝ = (x✝, false)

def Core.DeadDefElim.deadDefElimProgram (p : Program) : Transform.CoreTransformM (Bool × Program)

The dead-definition transform. Every procedure of the program with the unread inits of its structured body removed, every other declaration unchanged, and whether some procedure body changed. It transforms each body once and leaves the transform state, cached analyses included, as it is.

Equations

• One or more equations did not get rendered due to their size.

def Core.deadDefElimPipelinePhase : PipelinePhase

The dead-definition elimination pipeline phase: removes from each procedure body the inits whose variable no later statement mentions (Core.DeadDefElim.deadDefElimProgram). It requires a program

• without calls (noCalls) and loops (noLoops): its correctness is established for call-free, loop-free procedure bodies only;
• whose function preconditions are already checked (noPrecondsFromFuncs): an erased init takes its unchecked preconditions with it;
• that is type-checked (typeAnnotated, which only typeCheck establishes): an erased init takes its type errors with it. It only deletes inits, so it keeps every fact of its input. No default pipeline runs it; a pipeline names it (Core.nameablePhases).

Equations

• One or more equations did not get rendered due to their size.