Check the additional shadowing constraints on statements, blocks, cases, and function definitions.
We recursively visit statements, blocks, etc., accumulating all the variables declared so far, which form all the visible variables, both accessible and inaccessble. We check that each declared variable is not already visible.
Note that these checks overlap with the safety checks, for what concerns visible and accessible variables, while they are additional checks for what concerns visible but inaccessible variables. Restricting the checks to just visible but inaccessible variables would be more complicated than checking all the visible variables.
Function:
(defun check-shadow-statement (stmt vars) (declare (xargs :guard (and (statementp stmt) (identifier-setp vars)))) (let ((__function__ 'check-shadow-statement)) (declare (ignorable __function__)) (statement-case stmt :block (b* (((okf &) (check-shadow-block stmt.get vars))) (identifier-set-fix vars)) :variable-single (if (in stmt.name (identifier-set-fix vars)) (reserrf (list :shadowed-var stmt.name)) (insert stmt.name (identifier-set-fix vars))) :variable-multi (b* ((declared (mergesort stmt.names)) (shadowed (intersect declared (identifier-set-fix vars)))) (if (emptyp shadowed) (union declared (identifier-set-fix vars)) (reserrf (list :shadowed-vars shadowed)))) :assign-single (identifier-set-fix vars) :assign-multi (identifier-set-fix vars) :funcall (identifier-set-fix vars) :if (b* (((okf &) (check-shadow-block stmt.body vars))) (identifier-set-fix vars)) :for (b* ((stmts (block->statements stmt.init)) ((okf vars1) (check-shadow-statement-list stmts vars)) ((okf &) (check-shadow-block stmt.update vars1)) ((okf &) (check-shadow-block stmt.body vars1))) (identifier-set-fix vars)) :switch (b* (((okf &) (check-shadow-swcase-list stmt.cases vars)) ((okf &) (check-shadow-block-option stmt.default vars))) (identifier-set-fix vars)) :leave (identifier-set-fix vars) :break (identifier-set-fix vars) :continue (identifier-set-fix vars) :fundef (b* (((okf &) (check-shadow-fundef stmt.get vars))) (identifier-set-fix vars)))))
Function:
(defun check-shadow-statement-list (stmts vars) (declare (xargs :guard (and (statement-listp stmts) (identifier-setp vars)))) (let ((__function__ 'check-shadow-statement-list)) (declare (ignorable __function__)) (b* (((when (endp stmts)) (identifier-set-fix vars)) ((okf vars) (check-shadow-statement (car stmts) vars)) ((okf vars) (check-shadow-statement-list (cdr stmts) vars))) vars)))
Function:
(defun check-shadow-block (block vars) (declare (xargs :guard (and (blockp block) (identifier-setp vars)))) (let ((__function__ 'check-shadow-block)) (declare (ignorable __function__)) (b* (((okf &) (check-shadow-statement-list (block->statements block) vars))) nil)))
Function:
(defun check-shadow-block-option (block? vars) (declare (xargs :guard (and (block-optionp block?) (identifier-setp vars)))) (let ((__function__ 'check-shadow-block-option)) (declare (ignorable __function__)) (block-option-case block? :none nil :some (check-shadow-block block?.val vars))))
Function:
(defun check-shadow-swcase (case vars) (declare (xargs :guard (and (swcasep case) (identifier-setp vars)))) (let ((__function__ 'check-shadow-swcase)) (declare (ignorable __function__)) (check-shadow-block (swcase->body case) vars)))
Function:
(defun check-shadow-swcase-list (cases vars) (declare (xargs :guard (and (swcase-listp cases) (identifier-setp vars)))) (let ((__function__ 'check-shadow-swcase-list)) (declare (ignorable __function__)) (b* (((when (endp cases)) nil) ((okf &) (check-shadow-swcase (car cases) vars)) ((okf &) (check-shadow-swcase-list (cdr cases) vars))) nil)))
Function:
(defun check-shadow-fundef (fundef vars) (declare (xargs :guard (and (fundefp fundef) (identifier-setp vars)))) (let ((__function__ 'check-shadow-fundef)) (declare (ignorable __function__)) (b* ((inputs (fundef->inputs fundef)) (outputs (fundef->outputs fundef)) (declared (mergesort (append inputs outputs))) (shadowed (intersect declared (identifier-set-fix vars))) ((unless (emptyp shadowed)) (reserrf (list :shadowed-vars shadowed))) (vars (union (identifier-set-fix vars) declared))) (check-shadow-block (fundef->body fundef) vars))))
Theorem:
(defthm return-type-of-check-shadow-statement.new-vars (b* ((?new-vars (check-shadow-statement stmt vars))) (identifier-set-resultp new-vars)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-shadow-statement-list.new-vars (b* ((?new-vars (check-shadow-statement-list stmts vars))) (identifier-set-resultp new-vars)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-shadow-block._ (b* ((?_ (check-shadow-block block vars))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-shadow-block-option._ (b* ((?_ (check-shadow-block-option block? vars))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-shadow-swcase._ (b* ((?_ (check-shadow-swcase case vars))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-shadow-swcase-list._ (b* ((?_ (check-shadow-swcase-list cases vars))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-check-shadow-fundef._ (b* ((?_ (check-shadow-fundef fundef vars))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm check-shadow-statement-of-statement-fix-stmt (equal (check-shadow-statement (statement-fix stmt) vars) (check-shadow-statement stmt vars)))
Theorem:
(defthm check-shadow-statement-of-identifier-set-fix-vars (equal (check-shadow-statement stmt (identifier-set-fix vars)) (check-shadow-statement stmt vars)))
Theorem:
(defthm check-shadow-statement-list-of-statement-list-fix-stmts (equal (check-shadow-statement-list (statement-list-fix stmts) vars) (check-shadow-statement-list stmts vars)))
Theorem:
(defthm check-shadow-statement-list-of-identifier-set-fix-vars (equal (check-shadow-statement-list stmts (identifier-set-fix vars)) (check-shadow-statement-list stmts vars)))
Theorem:
(defthm check-shadow-block-of-block-fix-block (equal (check-shadow-block (block-fix block) vars) (check-shadow-block block vars)))
Theorem:
(defthm check-shadow-block-of-identifier-set-fix-vars (equal (check-shadow-block block (identifier-set-fix vars)) (check-shadow-block block vars)))
Theorem:
(defthm check-shadow-block-option-of-block-option-fix-block? (equal (check-shadow-block-option (block-option-fix block?) vars) (check-shadow-block-option block? vars)))
Theorem:
(defthm check-shadow-block-option-of-identifier-set-fix-vars (equal (check-shadow-block-option block? (identifier-set-fix vars)) (check-shadow-block-option block? vars)))
Theorem:
(defthm check-shadow-swcase-of-swcase-fix-case (equal (check-shadow-swcase (swcase-fix case) vars) (check-shadow-swcase case vars)))
Theorem:
(defthm check-shadow-swcase-of-identifier-set-fix-vars (equal (check-shadow-swcase case (identifier-set-fix vars)) (check-shadow-swcase case vars)))
Theorem:
(defthm check-shadow-swcase-list-of-swcase-list-fix-cases (equal (check-shadow-swcase-list (swcase-list-fix cases) vars) (check-shadow-swcase-list cases vars)))
Theorem:
(defthm check-shadow-swcase-list-of-identifier-set-fix-vars (equal (check-shadow-swcase-list cases (identifier-set-fix vars)) (check-shadow-swcase-list cases vars)))
Theorem:
(defthm check-shadow-fundef-of-fundef-fix-fundef (equal (check-shadow-fundef (fundef-fix fundef) vars) (check-shadow-fundef fundef vars)))
Theorem:
(defthm check-shadow-fundef-of-identifier-set-fix-vars (equal (check-shadow-fundef fundef (identifier-set-fix vars)) (check-shadow-fundef fundef vars)))
Theorem:
(defthm check-shadow-statement-statement-equiv-congruence-on-stmt (implies (statement-equiv stmt stmt-equiv) (equal (check-shadow-statement stmt vars) (check-shadow-statement stmt-equiv vars))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-statement-identifier-set-equiv-congruence-on-vars (implies (identifier-set-equiv vars vars-equiv) (equal (check-shadow-statement stmt vars) (check-shadow-statement stmt vars-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-statement-list-statement-list-equiv-congruence-on-stmts (implies (statement-list-equiv stmts stmts-equiv) (equal (check-shadow-statement-list stmts vars) (check-shadow-statement-list stmts-equiv vars))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-statement-list-identifier-set-equiv-congruence-on-vars (implies (identifier-set-equiv vars vars-equiv) (equal (check-shadow-statement-list stmts vars) (check-shadow-statement-list stmts vars-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-block-block-equiv-congruence-on-block (implies (block-equiv block block-equiv) (equal (check-shadow-block block vars) (check-shadow-block block-equiv vars))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-block-identifier-set-equiv-congruence-on-vars (implies (identifier-set-equiv vars vars-equiv) (equal (check-shadow-block block vars) (check-shadow-block block vars-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-block-option-block-option-equiv-congruence-on-block? (implies (block-option-equiv block? block?-equiv) (equal (check-shadow-block-option block? vars) (check-shadow-block-option block?-equiv vars))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-block-option-identifier-set-equiv-congruence-on-vars (implies (identifier-set-equiv vars vars-equiv) (equal (check-shadow-block-option block? vars) (check-shadow-block-option block? vars-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-swcase-swcase-equiv-congruence-on-case (implies (swcase-equiv case case-equiv) (equal (check-shadow-swcase case vars) (check-shadow-swcase case-equiv vars))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-swcase-identifier-set-equiv-congruence-on-vars (implies (identifier-set-equiv vars vars-equiv) (equal (check-shadow-swcase case vars) (check-shadow-swcase case vars-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-swcase-list-swcase-list-equiv-congruence-on-cases (implies (swcase-list-equiv cases cases-equiv) (equal (check-shadow-swcase-list cases vars) (check-shadow-swcase-list cases-equiv vars))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-swcase-list-identifier-set-equiv-congruence-on-vars (implies (identifier-set-equiv vars vars-equiv) (equal (check-shadow-swcase-list cases vars) (check-shadow-swcase-list cases vars-equiv))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-fundef-fundef-equiv-congruence-on-fundef (implies (fundef-equiv fundef fundef-equiv) (equal (check-shadow-fundef fundef vars) (check-shadow-fundef fundef-equiv vars))) :rule-classes :congruence)
Theorem:
(defthm check-shadow-fundef-identifier-set-equiv-congruence-on-vars (implies (identifier-set-equiv vars vars-equiv) (equal (check-shadow-fundef fundef vars) (check-shadow-fundef fundef vars-equiv))) :rule-classes :congruence)