		Search-engine friendly clone of the ACL2 documentation.

Dead-code-eliminator

Statements/blocks/cases/fundefs-dead

Mutually recursive functions to eliminate dead code in statements, blocks, cases, and function definitions.

Definitions and Theorems

Function: statement-dead

(defun statement-dead (stmt)
 (declare (xargs :guard (statementp stmt)))
 (let ((__function__ 'statement-dead))
  (declare (ignorable __function__))
  (statement-case
   stmt
   :block (statement-block (block-dead stmt.get))
   :variable-single (statement-fix stmt)
   :variable-multi (statement-fix stmt)
   :assign-single (statement-fix stmt)
   :assign-multi (statement-fix stmt)
   :funcall (statement-fix stmt)
   :if (make-statement-if :test stmt.test
                          :body (block-dead stmt.body))
   :for (make-statement-for :init (block-dead stmt.init)
                            :test stmt.test
                            :update (block-dead stmt.update)
                            :body (block-dead stmt.body))
   :switch
   (make-statement-switch :target stmt.target
                          :cases (swcase-list-dead stmt.cases)
                          :default (block-option-dead stmt.default))
   :leave (statement-leave)
   :break (statement-break)
   :continue (statement-continue)
   :fundef (statement-fundef (fundef-dead stmt.get)))))

Function: statement-list-dead

(defun statement-list-dead (stmts)
  (declare (xargs :guard (statement-listp stmts)))
  (let ((__function__ 'statement-list-dead))
    (declare (ignorable __function__))
    (b* (((when (endp stmts)) nil)
         (stmt (car stmts))
         (new-stmt (statement-dead stmt))
         ((when (or (statement-case stmt :leave)
                    (statement-case stmt :break)
                    (statement-case stmt :continue)))
          (list new-stmt)))
      (cons new-stmt
            (statement-list-dead (cdr stmts))))))

Function: block-dead

(defun block-dead (block)
  (declare (xargs :guard (blockp block)))
  (let ((__function__ 'block-dead))
    (declare (ignorable __function__))
    (block (statement-list-dead (block->statements block)))))

Function: block-option-dead

(defun block-option-dead (block?)
  (declare (xargs :guard (block-optionp block?)))
  (let ((__function__ 'block-option-dead))
    (declare (ignorable __function__))
    (block-option-case block?
                       :some (block-dead block?.val)
                       :none nil)))

Function: swcase-dead

(defun swcase-dead (case)
  (declare (xargs :guard (swcasep case)))
  (let ((__function__ 'swcase-dead))
    (declare (ignorable __function__))
    (make-swcase :value (swcase->value case)
                 :body (block-dead (swcase->body case)))))

Function: swcase-list-dead

(defun swcase-list-dead (cases)
  (declare (xargs :guard (swcase-listp cases)))
  (let ((__function__ 'swcase-list-dead))
    (declare (ignorable __function__))
    (cond ((endp cases) nil)
          (t (cons (swcase-dead (car cases))
                   (swcase-list-dead (cdr cases)))))))

Function: fundef-dead

(defun fundef-dead (fundef)
  (declare (xargs :guard (fundefp fundef)))
  (let ((__function__ 'fundef-dead))
    (declare (ignorable __function__))
    (make-fundef :name (fundef->name fundef)
                 :inputs (fundef->inputs fundef)
                 :outputs (fundef->outputs fundef)
                 :body (block-dead (fundef->body fundef)))))

Theorem: return-type-of-statement-dead.new-stmt

(defthm return-type-of-statement-dead.new-stmt
  (b* ((?new-stmt (statement-dead stmt)))
    (statementp new-stmt))
  :rule-classes :rewrite)

Theorem: return-type-of-statement-list-dead.new-stmt

(defthm return-type-of-statement-list-dead.new-stmt
  (b* ((?new-stmt (statement-list-dead stmts)))
    (statement-listp new-stmt))
  :rule-classes :rewrite)

Theorem: return-type-of-block-dead.new-block

(defthm return-type-of-block-dead.new-block
  (b* ((?new-block (block-dead block)))
    (blockp new-block))
  :rule-classes :rewrite)

Theorem: return-type-of-block-option-dead.new-block?

(defthm return-type-of-block-option-dead.new-block?
  (b* ((?new-block? (block-option-dead block?)))
    (block-optionp new-block?))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-dead.new-case

(defthm return-type-of-swcase-dead.new-case
  (b* ((?new-case (swcase-dead case)))
    (swcasep new-case))
  :rule-classes :rewrite)

Theorem: return-type-of-swcase-list-dead.new-cases

(defthm return-type-of-swcase-list-dead.new-cases
  (b* ((?new-cases (swcase-list-dead cases)))
    (swcase-listp new-cases))
  :rule-classes :rewrite)

Theorem: return-type-of-fundef-dead.new-fdef

(defthm return-type-of-fundef-dead.new-fdef
  (b* ((?new-fdef (fundef-dead fundef)))
    (fundefp new-fdef))
  :rule-classes :rewrite)

Theorem: statement-dead-of-statement-fix-stmt

(defthm statement-dead-of-statement-fix-stmt
  (equal (statement-dead (statement-fix stmt))
         (statement-dead stmt)))

Theorem: statement-list-dead-of-statement-list-fix-stmts

(defthm statement-list-dead-of-statement-list-fix-stmts
  (equal (statement-list-dead (statement-list-fix stmts))
         (statement-list-dead stmts)))

Theorem: block-dead-of-block-fix-block

(defthm block-dead-of-block-fix-block
  (equal (block-dead (block-fix block))
         (block-dead block)))

Theorem: block-option-dead-of-block-option-fix-block?

(defthm block-option-dead-of-block-option-fix-block?
  (equal (block-option-dead (block-option-fix block?))
         (block-option-dead block?)))

Theorem: swcase-dead-of-swcase-fix-case

(defthm swcase-dead-of-swcase-fix-case
  (equal (swcase-dead (swcase-fix case))
         (swcase-dead case)))

Theorem: swcase-list-dead-of-swcase-list-fix-cases

(defthm swcase-list-dead-of-swcase-list-fix-cases
  (equal (swcase-list-dead (swcase-list-fix cases))
         (swcase-list-dead cases)))

Theorem: fundef-dead-of-fundef-fix-fundef

(defthm fundef-dead-of-fundef-fix-fundef
  (equal (fundef-dead (fundef-fix fundef))
         (fundef-dead fundef)))

Theorem: statement-dead-statement-equiv-congruence-on-stmt

(defthm statement-dead-statement-equiv-congruence-on-stmt
  (implies (statement-equiv stmt stmt-equiv)
           (equal (statement-dead stmt)
                  (statement-dead stmt-equiv)))
  :rule-classes :congruence)

Theorem: statement-list-dead-statement-list-equiv-congruence-on-stmts

(defthm statement-list-dead-statement-list-equiv-congruence-on-stmts
  (implies (statement-list-equiv stmts stmts-equiv)
           (equal (statement-list-dead stmts)
                  (statement-list-dead stmts-equiv)))
  :rule-classes :congruence)

Theorem: block-dead-block-equiv-congruence-on-block

(defthm block-dead-block-equiv-congruence-on-block
  (implies (block-equiv block block-equiv)
           (equal (block-dead block)
                  (block-dead block-equiv)))
  :rule-classes :congruence)

Theorem: block-option-dead-block-option-equiv-congruence-on-block?

(defthm block-option-dead-block-option-equiv-congruence-on-block?
  (implies (block-option-equiv block? block?-equiv)
           (equal (block-option-dead block?)
                  (block-option-dead block?-equiv)))
  :rule-classes :congruence)

Theorem: swcase-dead-swcase-equiv-congruence-on-case

(defthm swcase-dead-swcase-equiv-congruence-on-case
  (implies (swcase-equiv case case-equiv)
           (equal (swcase-dead case)
                  (swcase-dead case-equiv)))
  :rule-classes :congruence)

Theorem: swcase-list-dead-swcase-list-equiv-congruence-on-cases

(defthm swcase-list-dead-swcase-list-equiv-congruence-on-cases
  (implies (swcase-list-equiv cases cases-equiv)
           (equal (swcase-list-dead cases)
                  (swcase-list-dead cases-equiv)))
  :rule-classes :congruence)

Theorem: fundef-dead-fundef-equiv-congruence-on-fundef

(defthm fundef-dead-fundef-equiv-congruence-on-fundef
  (implies (fundef-equiv fundef fundef-equiv)
           (equal (fundef-dead fundef)
                  (fundef-dead fundef-equiv)))
  :rule-classes :congruence)

Theorem: statement-kind-of-statement-dead

(defthm statement-kind-of-statement-dead
  (equal (statement-kind (statement-dead stmt))
         (statement-kind stmt)))

Theorem: block->statements-of-block-dead

(defthm block->statements-of-block-dead
  (equal (block->statements (block-dead block))
         (statement-list-dead (block->statements block))))

Theorem: block-option-dead-iff

(defthm block-option-dead-iff
  (iff (block-option-dead block?) block?))

Theorem: swcase->value-of-swcase-dead

(defthm swcase->value-of-swcase-dead
  (equal (swcase->value (swcase-dead case))
         (swcase->value case)))

Theorem: consp-of-swcase-list-dead

(defthm consp-of-swcase-list-dead
  (equal (consp (swcase-list-dead cases))
         (consp cases)))

Theorem: fundef->name-of-fundef-dead

(defthm fundef->name-of-fundef-dead
  (equal (fundef->name (fundef-dead fdef))
         (fundef->name fdef)))

Subtopics

Statement-list-dead: Eliminate dead code in lists of statements.
Statement-dead: Eliminate dead code in statements.
Block-dead: Eliminate dead code in blocks.
Swcase-list-dead: Eliminate dead code in lists of switch cases.
Block-option-dead: Eliminate dead code in optional blocks.
Swcase-dead: Eliminate dead code in switch cases.
Fundef-dead: Eliminate dead code in function definitions.