		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-fun-rules

Rules for exec-fun.

The proofs generated by ATC are modularized so that there is one theorem per non-recursive target function. So we generally do not expand calls of exec-fun, except in the theorem for the function in question. We rely on the fact that the correctness theorems for the functions called by the function in question come after the following rule in the ACL2 history (because they are generated by ATC as part of the generated events), and thus take precedence over this rule: in other words, given theorems for the called functions, this rule is expected to apply only on the function in question, i.e. the one whose correctness theorem is being proved. Note that these theorems are generated only for non-recursive functions; the recursive functions represent loops, and their correctness theorems do not involve exec-fun.

Definitions and Theorems

Theorem: exec-fun-open-return

(defthm exec-fun-open-return
 (implies
      (and (not (zp limit))
           (equal info (fun-env-lookup fun fenv))
           info
           (equal scope
                  (init-scope (fun-info->params info)
                              args))
           (scopep scope)
           (equal sval+compst1
                  (exec-block-item-list
                       (fun-info->body info)
                       (push-frame (make-frame :function fun
                                               :scopes (list scope))
                                   compst)
                       fenv (1- limit)))
           (equal sval (mv-nth 0 sval+compst1))
           (equal compst1 (mv-nth 1 sval+compst1))
           (stmt-valuep sval)
           (stmt-value-case sval :return)
           (equal val? (stmt-value-return->value? sval))
           (equal (type-of-value-option val?)
                  (tyname-to-type (fun-info->result info))))
      (equal (exec-fun fun args compst fenv limit)
             (mv val? (pop-frame compst1)))))

Theorem: exec-fun-open-noreturn

(defthm exec-fun-open-noreturn
 (implies
      (and (not (zp limit))
           (equal info (fun-env-lookup fun fenv))
           info
           (equal scope
                  (init-scope (fun-info->params info)
                              args))
           (scopep scope)
           (equal sval+compst1
                  (exec-block-item-list
                       (fun-info->body info)
                       (push-frame (make-frame :function fun
                                               :scopes (list scope))
                                   compst)
                       fenv (1- limit)))
           (equal sval (mv-nth 0 sval+compst1))
           (equal compst1 (mv-nth 1 sval+compst1))
           (stmt-valuep sval)
           (stmt-value-case sval :none)
           (equal (type-void)
                  (tyname-to-type (fun-info->result info))))
      (equal (exec-fun fun args compst fenv limit)
             (mv nil (pop-frame compst1)))))