Check if statements, blocks, cases, and function definitions are safe.
These are checked in the context of
a variable table for visible and accessible variables
A successful check returns
a set of possible modes in which execution may complete.
The set of modes is used to check the conditions on
the occurrence of
Function:
(defun check-safe-statement (stmt varset funtab) (declare (xargs :guard (and (statementp stmt) (identifier-setp varset) (funtablep funtab)))) (let ((__function__ 'check-safe-statement)) (declare (ignorable __function__)) (statement-case stmt :block (b* (((okf modes) (check-safe-block stmt.get varset funtab))) (make-vars+modes :vars (identifier-set-fix varset) :modes modes)) :variable-single (b* (((okf varset) (check-safe-variable-single stmt.name stmt.init varset funtab))) (make-vars+modes :vars varset :modes (insert (mode-regular) nil))) :variable-multi (b* (((okf varset) (check-safe-variable-multi stmt.names stmt.init varset funtab))) (make-vars+modes :vars varset :modes (insert (mode-regular) nil))) :assign-single (b* (((okf &) (check-safe-assign-single stmt.target stmt.value varset funtab))) (make-vars+modes :vars (identifier-set-fix varset) :modes (insert (mode-regular) nil))) :assign-multi (b* (((okf &) (check-safe-assign-multi stmt.targets stmt.value varset funtab))) (make-vars+modes :vars (identifier-set-fix varset) :modes (insert (mode-regular) nil))) :funcall (b* (((okf results) (check-safe-funcall stmt.get varset funtab)) ((unless (= results 0)) (reserrf (list :discarded-values stmt.get)))) (make-vars+modes :vars (identifier-set-fix varset) :modes (insert (mode-regular) nil))) :if (b* (((okf results) (check-safe-expression stmt.test varset funtab)) ((unless (= results 1)) (reserrf (list :multi-valued-if-test stmt.test))) ((okf modes) (check-safe-block stmt.body varset funtab))) (make-vars+modes :vars (identifier-set-fix varset) :modes (insert (mode-regular) modes))) :for (b* ((stmts (block->statements stmt.init)) ((okf funtab) (add-funtypes (statements-to-fundefs stmts) funtab)) ((okf varsmodes) (check-safe-statement-list stmts varset funtab)) (varset1 (vars+modes->vars varsmodes)) (init-modes (vars+modes->modes varsmodes)) ((when (in (mode-break) init-modes)) (reserrf (list :break-in-loop-init stmt.init))) ((when (in (mode-continue) init-modes)) (reserrf (list :continue-in-loop-init stmt.init))) ((okf results) (check-safe-expression stmt.test varset1 funtab)) ((unless (= results 1)) (reserrf (list :multi-valued-for-test stmt.test))) ((okf update-modes) (check-safe-block stmt.update varset1 funtab)) ((when (in (mode-break) update-modes)) (reserrf (list :break-in-loop-update stmt.update))) ((when (in (mode-continue) update-modes)) (reserrf (list :continue-in-loop-update stmt.update))) ((okf body-modes) (check-safe-block stmt.body varset1 funtab)) (modes (if (or (in (mode-leave) init-modes) (in (mode-leave) update-modes) (in (mode-leave) body-modes)) (insert (mode-leave) (insert (mode-regular) nil)) (insert (mode-regular) nil)))) (make-vars+modes :vars (identifier-set-fix varset) :modes modes)) :switch (b* (((okf results) (check-safe-expression stmt.target varset funtab)) ((unless (= results 1)) (reserrf (list :multi-valued-switch-target stmt.target))) ((unless (or (consp stmt.cases) stmt.default)) (reserrf (list :no-cases-in-switch (statement-fix stmt)))) ((unless (no-duplicatesp-equal (swcase-list->value-list stmt.cases))) (reserrf (list :duplicate-switch-cases (statement-fix stmt)))) ((okf cases-modes) (check-safe-swcase-list stmt.cases varset funtab)) ((okf default-modes) (check-safe-block-option stmt.default varset funtab))) (make-vars+modes :vars (identifier-set-fix varset) :modes (union cases-modes default-modes))) :leave (make-vars+modes :vars (identifier-set-fix varset) :modes (insert (mode-leave) nil)) :break (make-vars+modes :vars (identifier-set-fix varset) :modes (insert (mode-break) nil)) :continue (make-vars+modes :vars (identifier-set-fix varset) :modes (insert (mode-continue) nil)) :fundef (b* (((okf &) (check-safe-fundef stmt.get funtab))) (make-vars+modes :vars (identifier-set-fix varset) :modes (insert (mode-regular) nil))))))
Function:
(defun check-safe-statement-list (stmts varset funtab) (declare (xargs :guard (and (statement-listp stmts) (identifier-setp varset) (funtablep funtab)))) (let ((__function__ 'check-safe-statement-list)) (declare (ignorable __function__)) (b* (((when (endp stmts)) (make-vars+modes :vars (identifier-set-fix varset) :modes (insert (mode-regular) nil))) ((okf varsmodes) (check-safe-statement (car stmts) varset funtab)) (varset (vars+modes->vars varsmodes)) (first-modes (vars+modes->modes varsmodes)) ((okf varsmodes) (check-safe-statement-list (cdr stmts) varset funtab)) (varset (vars+modes->vars varsmodes)) (rest-modes (vars+modes->modes varsmodes)) (modes (if (in (mode-regular) first-modes) (union first-modes rest-modes) first-modes))) (make-vars+modes :vars varset :modes modes))))
Function:
(defun check-safe-block (block varset funtab) (declare (xargs :guard (and (blockp block) (identifier-setp varset) (funtablep funtab)))) (let ((__function__ 'check-safe-block)) (declare (ignorable __function__)) (b* ((stmts (block->statements block)) ((okf funtab) (add-funtypes (statements-to-fundefs stmts) funtab)) ((okf varsmodes) (check-safe-statement-list stmts varset funtab))) (vars+modes->modes varsmodes))))
Function:
(defun check-safe-block-option (block? varset funtab) (declare (xargs :guard (and (block-optionp block?) (identifier-setp varset) (funtablep funtab)))) (let ((__function__ 'check-safe-block-option)) (declare (ignorable __function__)) (block-option-case block? :none (insert (mode-regular) nil) :some (check-safe-block (block-option-some->val block?) varset funtab))))
Function:
(defun check-safe-swcase (case varset funtab) (declare (xargs :guard (and (swcasep case) (identifier-setp varset) (funtablep funtab)))) (let ((__function__ 'check-safe-swcase)) (declare (ignorable __function__)) (b* (((swcase case) case) ((okf &) (check-safe-literal case.value))) (check-safe-block case.body varset funtab))))
Function:
(defun check-safe-swcase-list (cases varset funtab) (declare (xargs :guard (and (swcase-listp cases) (identifier-setp varset) (funtablep funtab)))) (let ((__function__ 'check-safe-swcase-list)) (declare (ignorable __function__)) (b* (((when (endp cases)) nil) ((okf first-modes) (check-safe-swcase (car cases) varset funtab)) ((okf rest-modes) (check-safe-swcase-list (cdr cases) varset funtab))) (union first-modes rest-modes))))
Function:
(defun check-safe-fundef (fundef funtab) (declare (xargs :guard (and (fundefp fundef) (funtablep funtab)))) (let ((__function__ 'check-safe-fundef)) (declare (ignorable __function__)) (b* (((fundef fundef) fundef) ((okf varset) (add-vars fundef.inputs nil)) ((okf varset) (add-vars fundef.outputs varset)) ((okf modes) (check-safe-block fundef.body varset funtab)) ((when (in (mode-break) modes)) (reserrf (list :break-from-function (fundef-fix fundef)))) ((when (in (mode-continue) modes)) (reserrf (list :continue-from-function (fundef-fix fundef))))) nil)))
Theorem:
(defthm return-type-of-check-safe-statement.varsmodes (b* ((?varsmodes (check-safe-statement stmt varset funtab))) (vars+modes-resultp varsmodes)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-safe-statement-list.varsmodes (b* ((?varsmodes (check-safe-statement-list stmts varset funtab))) (vars+modes-resultp varsmodes)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-safe-block.modes (b* ((?modes (check-safe-block block varset funtab))) (mode-set-resultp modes)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-safe-block-option.modes (b* ((?modes (check-safe-block-option block? varset funtab))) (mode-set-resultp modes)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-safe-swcase.modes (b* ((?modes (check-safe-swcase case varset funtab))) (mode-set-resultp modes)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-safe-swcase-list.modes (b* ((?modes (check-safe-swcase-list cases varset funtab))) (mode-set-resultp modes)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-safe-fundef._ (b* ((?_ (check-safe-fundef fundef funtab))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm check-safe-statement-of-statement-fix-stmt (equal (check-safe-statement (statement-fix stmt) varset funtab) (check-safe-statement stmt varset funtab)))
Theorem:
(defthm check-safe-statement-of-identifier-set-fix-varset (equal (check-safe-statement stmt (identifier-set-fix varset) funtab) (check-safe-statement stmt varset funtab)))
Theorem:
(defthm check-safe-statement-of-funtable-fix-funtab (equal (check-safe-statement stmt varset (funtable-fix funtab)) (check-safe-statement stmt varset funtab)))
Theorem:
(defthm check-safe-statement-list-of-statement-list-fix-stmts (equal (check-safe-statement-list (statement-list-fix stmts) varset funtab) (check-safe-statement-list stmts varset funtab)))
Theorem:
(defthm check-safe-statement-list-of-identifier-set-fix-varset (equal (check-safe-statement-list stmts (identifier-set-fix varset) funtab) (check-safe-statement-list stmts varset funtab)))
Theorem:
(defthm check-safe-statement-list-of-funtable-fix-funtab (equal (check-safe-statement-list stmts varset (funtable-fix funtab)) (check-safe-statement-list stmts varset funtab)))
Theorem:
(defthm check-safe-block-of-block-fix-block (equal (check-safe-block (block-fix block) varset funtab) (check-safe-block block varset funtab)))
Theorem:
(defthm check-safe-block-of-identifier-set-fix-varset (equal (check-safe-block block (identifier-set-fix varset) funtab) (check-safe-block block varset funtab)))
Theorem:
(defthm check-safe-block-of-funtable-fix-funtab (equal (check-safe-block block varset (funtable-fix funtab)) (check-safe-block block varset funtab)))
Theorem:
(defthm check-safe-block-option-of-block-option-fix-block? (equal (check-safe-block-option (block-option-fix block?) varset funtab) (check-safe-block-option block? varset funtab)))
Theorem:
(defthm check-safe-block-option-of-identifier-set-fix-varset (equal (check-safe-block-option block? (identifier-set-fix varset) funtab) (check-safe-block-option block? varset funtab)))
Theorem:
(defthm check-safe-block-option-of-funtable-fix-funtab (equal (check-safe-block-option block? varset (funtable-fix funtab)) (check-safe-block-option block? varset funtab)))
Theorem:
(defthm check-safe-swcase-of-swcase-fix-case (equal (check-safe-swcase (swcase-fix case) varset funtab) (check-safe-swcase case varset funtab)))
Theorem:
(defthm check-safe-swcase-of-identifier-set-fix-varset (equal (check-safe-swcase case (identifier-set-fix varset) funtab) (check-safe-swcase case varset funtab)))
Theorem:
(defthm check-safe-swcase-of-funtable-fix-funtab (equal (check-safe-swcase case varset (funtable-fix funtab)) (check-safe-swcase case varset funtab)))
Theorem:
(defthm check-safe-swcase-list-of-swcase-list-fix-cases (equal (check-safe-swcase-list (swcase-list-fix cases) varset funtab) (check-safe-swcase-list cases varset funtab)))
Theorem:
(defthm check-safe-swcase-list-of-identifier-set-fix-varset (equal (check-safe-swcase-list cases (identifier-set-fix varset) funtab) (check-safe-swcase-list cases varset funtab)))
Theorem:
(defthm check-safe-swcase-list-of-funtable-fix-funtab (equal (check-safe-swcase-list cases varset (funtable-fix funtab)) (check-safe-swcase-list cases varset funtab)))
Theorem:
(defthm check-safe-fundef-of-fundef-fix-fundef (equal (check-safe-fundef (fundef-fix fundef) funtab) (check-safe-fundef fundef funtab)))
Theorem:
(defthm check-safe-fundef-of-funtable-fix-funtab (equal (check-safe-fundef fundef (funtable-fix funtab)) (check-safe-fundef fundef funtab)))
Theorem:
(defthm check-safe-statement-statement-equiv-congruence-on-stmt (implies (statement-equiv stmt stmt-equiv) (equal (check-safe-statement stmt varset funtab) (check-safe-statement stmt-equiv varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-statement-identifier-set-equiv-congruence-on-varset (implies (identifier-set-equiv varset varset-equiv) (equal (check-safe-statement stmt varset funtab) (check-safe-statement stmt varset-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-statement-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (check-safe-statement stmt varset funtab) (check-safe-statement stmt varset funtab-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-safe-statement-list-statement-list-equiv-congruence-on-stmts (implies (statement-list-equiv stmts stmts-equiv) (equal (check-safe-statement-list stmts varset funtab) (check-safe-statement-list stmts-equiv varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-statement-list-identifier-set-equiv-congruence-on-varset (implies (identifier-set-equiv varset varset-equiv) (equal (check-safe-statement-list stmts varset funtab) (check-safe-statement-list stmts varset-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-statement-list-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (check-safe-statement-list stmts varset funtab) (check-safe-statement-list stmts varset funtab-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-safe-block-block-equiv-congruence-on-block (implies (block-equiv block block-equiv) (equal (check-safe-block block varset funtab) (check-safe-block block-equiv varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-block-identifier-set-equiv-congruence-on-varset (implies (identifier-set-equiv varset varset-equiv) (equal (check-safe-block block varset funtab) (check-safe-block block varset-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-block-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (check-safe-block block varset funtab) (check-safe-block block varset funtab-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-safe-block-option-block-option-equiv-congruence-on-block? (implies (block-option-equiv block? block?-equiv) (equal (check-safe-block-option block? varset funtab) (check-safe-block-option block?-equiv varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-block-option-identifier-set-equiv-congruence-on-varset (implies (identifier-set-equiv varset varset-equiv) (equal (check-safe-block-option block? varset funtab) (check-safe-block-option block? varset-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-block-option-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (check-safe-block-option block? varset funtab) (check-safe-block-option block? varset funtab-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-safe-swcase-swcase-equiv-congruence-on-case (implies (swcase-equiv case case-equiv) (equal (check-safe-swcase case varset funtab) (check-safe-swcase case-equiv varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-swcase-identifier-set-equiv-congruence-on-varset (implies (identifier-set-equiv varset varset-equiv) (equal (check-safe-swcase case varset funtab) (check-safe-swcase case varset-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-swcase-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (check-safe-swcase case varset funtab) (check-safe-swcase case varset funtab-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-safe-swcase-list-swcase-list-equiv-congruence-on-cases (implies (swcase-list-equiv cases cases-equiv) (equal (check-safe-swcase-list cases varset funtab) (check-safe-swcase-list cases-equiv varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-swcase-list-identifier-set-equiv-congruence-on-varset (implies (identifier-set-equiv varset varset-equiv) (equal (check-safe-swcase-list cases varset funtab) (check-safe-swcase-list cases varset-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-swcase-list-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (check-safe-swcase-list cases varset funtab) (check-safe-swcase-list cases varset funtab-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-safe-fundef-fundef-equiv-congruence-on-fundef (implies (fundef-equiv fundef fundef-equiv) (equal (check-safe-fundef fundef funtab) (check-safe-fundef fundef-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-fundef-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (check-safe-fundef fundef funtab) (check-safe-fundef fundef funtab-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-safe-block-option-when-blockp (implies (blockp block) (equal (check-safe-block-option block varset funtab) (check-safe-block block varset funtab))))