		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-stmt

Check a statement.

Signature
(check-stmt s funtab vartab tagenv) → stype
Arguments: s — Guard (stmtp s).; funtab — Guard (fun-tablep funtab).; vartab — Guard (var-tablep vartab).; tagenv — Guard (tag-envp tagenv).
Returns: stype — Type (types+vartab-resultp stype).

For now we only allow compound statements, expression statements, conditional statements, while statements, and return statements with expressions.

These ACL2 functions return either a pair consisting of a non-empty set of types and a variable table (see types+vartab-p), or an error.

For a compound statement, we add a block scope to the variable table and then we process the list of block items. There is no need to explicitly remove the scope when exiting the block, because we only use the extended variable table to check the items of the block. Anything that follows the block is checked with the variable table prior to the extension. In fact, a compound statement does not update the variable table: we return the original variable table.

As expression statements, we only allow function calls and simple assignments to variables, where the assigned expression must be a function call or pure. We only allow function calls with pure arguments (see check-expr-call).

For a conditional statement with both branches, after ensuring that the test expression has scalar type, we check the two branches, and take the union of their return types. We return the initial variable table, unchanged; any change in the branches is local to the branches.

We treat a conditional statement with just one branch as one whose else branch returns nothing.

For a while statement, we ensure that the test has a scalar type, and we check the body. We put together void and the return types from the body: the void accounts for the case in which the body is never executed (i.e. the test is initially false). We return the initial variable table, unchanged; any change in the body is local to the body.

For a return statement, we require an expression, and we return the singleton set with the type of the expression. The type must not be void [C17:6.3.2.2].

For a block item that is a declaration, we check the (object) declaration, requiring the initializer but without requiring it to be constant. We return the singleton set with void, because a declaration never returns a value and proceeds with the next block item.

For a block item that is a statement, we check the statement.

If a list of block items is empty, we return the singleton set with void (because execution then continues after the block) and the variable table unchanged. If the list of block items is a singleton, we check the first and only item, and return the result as the result of checking the singleton list; we need to treat the singleton case differently from the next, otherwise we would be always returning void as one of the types, because this is what the empty list of block items returns. If the list of block items has two or more items, we check the first item and the (non-empty) rest of the block. We return the union of (i) the return types from the first block item, minus void if present, and (ii) the return types from the rest of the block. The reason for removing void from the first set is that void just indicates that execution may go from the first block item to the rest of the block: it does not represent a possible return type of the whole block. Note that if void is not among the first item's return types, it means that the rest of the block is acually dead code: execution never proceeds past the first block item. Nonetheless, as explained above, we also checking the rest of the block, and we consider its possible return types. This is consistent with the fact that [C17] does not say anything any special treatment of this kind of dead code; it is also consistent with simple experiments with gcc on Mac, which show that code after a return is checked, not ignored.

Theorem: return-type-of-check-stmt.stype

(defthm return-type-of-check-stmt.stype
  (b* ((?stype (check-stmt s funtab vartab tagenv)))
    (types+vartab-resultp stype))
  :rule-classes :rewrite)

Theorem: return-type-of-check-block-item.stype

(defthm return-type-of-check-block-item.stype
  (b* ((?stype (check-block-item item funtab vartab tagenv)))
    (types+vartab-resultp stype))
  :rule-classes :rewrite)

Theorem: return-type-of-check-block-item-list.stype

(defthm return-type-of-check-block-item-list.stype
  (b* ((?stype (check-block-item-list items funtab vartab tagenv)))
    (types+vartab-resultp stype))
  :rule-classes :rewrite)

Theorem: check-stmt-of-stmt-fix-s

(defthm check-stmt-of-stmt-fix-s
  (equal (check-stmt (stmt-fix s)
                     funtab vartab tagenv)
         (check-stmt s funtab vartab tagenv)))

Theorem: check-stmt-of-fun-table-fix-funtab

(defthm check-stmt-of-fun-table-fix-funtab
  (equal (check-stmt s (fun-table-fix funtab)
                     vartab tagenv)
         (check-stmt s funtab vartab tagenv)))

Theorem: check-stmt-of-var-table-fix-vartab

(defthm check-stmt-of-var-table-fix-vartab
  (equal (check-stmt s funtab (var-table-fix vartab)
                     tagenv)
         (check-stmt s funtab vartab tagenv)))

Theorem: check-stmt-of-tag-env-fix-tagenv

(defthm check-stmt-of-tag-env-fix-tagenv
  (equal (check-stmt s funtab vartab (tag-env-fix tagenv))
         (check-stmt s funtab vartab tagenv)))

Theorem: check-block-item-of-block-item-fix-item

(defthm check-block-item-of-block-item-fix-item
  (equal (check-block-item (block-item-fix item)
                           funtab vartab tagenv)
         (check-block-item item funtab vartab tagenv)))

Theorem: check-block-item-of-fun-table-fix-funtab

(defthm check-block-item-of-fun-table-fix-funtab
  (equal (check-block-item item (fun-table-fix funtab)
                           vartab tagenv)
         (check-block-item item funtab vartab tagenv)))

Theorem: check-block-item-of-var-table-fix-vartab

(defthm check-block-item-of-var-table-fix-vartab
  (equal (check-block-item item funtab (var-table-fix vartab)
                           tagenv)
         (check-block-item item funtab vartab tagenv)))

Theorem: check-block-item-of-tag-env-fix-tagenv

(defthm check-block-item-of-tag-env-fix-tagenv
  (equal (check-block-item item funtab vartab (tag-env-fix tagenv))
         (check-block-item item funtab vartab tagenv)))

Theorem: check-block-item-list-of-block-item-list-fix-items

(defthm check-block-item-list-of-block-item-list-fix-items
  (equal (check-block-item-list (block-item-list-fix items)
                                funtab vartab tagenv)
         (check-block-item-list items funtab vartab tagenv)))

Theorem: check-block-item-list-of-fun-table-fix-funtab

(defthm check-block-item-list-of-fun-table-fix-funtab
  (equal (check-block-item-list items (fun-table-fix funtab)
                                vartab tagenv)
         (check-block-item-list items funtab vartab tagenv)))

Theorem: check-block-item-list-of-var-table-fix-vartab

(defthm check-block-item-list-of-var-table-fix-vartab
  (equal (check-block-item-list items funtab (var-table-fix vartab)
                                tagenv)
         (check-block-item-list items funtab vartab tagenv)))

Theorem: check-block-item-list-of-tag-env-fix-tagenv

(defthm check-block-item-list-of-tag-env-fix-tagenv
  (equal (check-block-item-list items
                                funtab vartab (tag-env-fix tagenv))
         (check-block-item-list items funtab vartab tagenv)))

Theorem: check-stmt-stmt-equiv-congruence-on-s

(defthm check-stmt-stmt-equiv-congruence-on-s
  (implies (stmt-equiv s s-equiv)
           (equal (check-stmt s funtab vartab tagenv)
                  (check-stmt s-equiv funtab vartab tagenv)))
  :rule-classes :congruence)

Theorem: check-stmt-fun-table-equiv-congruence-on-funtab

(defthm check-stmt-fun-table-equiv-congruence-on-funtab
  (implies (fun-table-equiv funtab funtab-equiv)
           (equal (check-stmt s funtab vartab tagenv)
                  (check-stmt s funtab-equiv vartab tagenv)))
  :rule-classes :congruence)

Theorem: check-stmt-var-table-equiv-congruence-on-vartab

(defthm check-stmt-var-table-equiv-congruence-on-vartab
  (implies (var-table-equiv vartab vartab-equiv)
           (equal (check-stmt s funtab vartab tagenv)
                  (check-stmt s funtab vartab-equiv tagenv)))
  :rule-classes :congruence)

Theorem: check-stmt-tag-env-equiv-congruence-on-tagenv

(defthm check-stmt-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (check-stmt s funtab vartab tagenv)
                  (check-stmt s funtab vartab tagenv-equiv)))
  :rule-classes :congruence)

Theorem: check-block-item-block-item-equiv-congruence-on-item

(defthm check-block-item-block-item-equiv-congruence-on-item
  (implies
       (block-item-equiv item item-equiv)
       (equal (check-block-item item funtab vartab tagenv)
              (check-block-item item-equiv funtab vartab tagenv)))
  :rule-classes :congruence)

Theorem: check-block-item-fun-table-equiv-congruence-on-funtab

(defthm check-block-item-fun-table-equiv-congruence-on-funtab
  (implies
       (fun-table-equiv funtab funtab-equiv)
       (equal (check-block-item item funtab vartab tagenv)
              (check-block-item item funtab-equiv vartab tagenv)))
  :rule-classes :congruence)

Theorem: check-block-item-var-table-equiv-congruence-on-vartab

(defthm check-block-item-var-table-equiv-congruence-on-vartab
  (implies
       (var-table-equiv vartab vartab-equiv)
       (equal (check-block-item item funtab vartab tagenv)
              (check-block-item item funtab vartab-equiv tagenv)))
  :rule-classes :congruence)

Theorem: check-block-item-tag-env-equiv-congruence-on-tagenv

(defthm check-block-item-tag-env-equiv-congruence-on-tagenv
  (implies
       (tag-env-equiv tagenv tagenv-equiv)
       (equal (check-block-item item funtab vartab tagenv)
              (check-block-item item funtab vartab tagenv-equiv)))
  :rule-classes :congruence)

Theorem: check-block-item-list-block-item-list-equiv-congruence-on-items

(defthm
    check-block-item-list-block-item-list-equiv-congruence-on-items
 (implies
   (block-item-list-equiv items items-equiv)
   (equal (check-block-item-list items funtab vartab tagenv)
          (check-block-item-list items-equiv funtab vartab tagenv)))
 :rule-classes :congruence)

Theorem: check-block-item-list-fun-table-equiv-congruence-on-funtab

(defthm check-block-item-list-fun-table-equiv-congruence-on-funtab
 (implies
   (fun-table-equiv funtab funtab-equiv)
   (equal (check-block-item-list items funtab vartab tagenv)
          (check-block-item-list items funtab-equiv vartab tagenv)))
 :rule-classes :congruence)

Theorem: check-block-item-list-var-table-equiv-congruence-on-vartab

(defthm check-block-item-list-var-table-equiv-congruence-on-vartab
 (implies
   (var-table-equiv vartab vartab-equiv)
   (equal (check-block-item-list items funtab vartab tagenv)
          (check-block-item-list items funtab vartab-equiv tagenv)))
 :rule-classes :congruence)

Theorem: check-block-item-list-tag-env-equiv-congruence-on-tagenv

(defthm check-block-item-list-tag-env-equiv-congruence-on-tagenv
 (implies
   (tag-env-equiv tagenv tagenv-equiv)
   (equal (check-block-item-list items funtab vartab tagenv)
          (check-block-item-list items funtab vartab tagenv-equiv)))
 :rule-classes :congruence)

Theorem: check-stmt-var-table-no-change

(defthm check-stmt-var-table-no-change
  (b* ((result (check-stmt s funtab vartab tagenv)))
    (implies (types+vartab-p result)
             (equal (types+vartab->variables result)
                    (var-table-fix vartab)))))

Subtopics

Check-block-item-list
Check-block-item