Generate the correctness theorem for a C function.
(atc-gen-cfun-correct-thm fn typed-formals type affect prec-fns prec-tags prec-objs prog-const compst-var fenv-var limit-var fn-thms fn-fun-env-thm limit state) → (mv events print-event name)
In a computation state
The function
The guard of
We use a variable for the function environment,
which we equate to the translation unit's function environment
in a hypothesis.
Note that, when we execute the ACL2 code in this function,
we do not have the function environment
of the generated translation unit yet,
because we generate these correctness theorems
along with the function definitions that form the translation unit
(currently we could generate these theorems after the translation unit,
but we prefer to do them at the same time for easier future extensions,
in which we may generate ``smaller'' theorems,
possibly for subterms/subexpressions/substatements).
Thus, we cannot use a quoted constant for the function environment here.
The reason why we introduce a variable and equate it in the hypothesis,
as opposed to using
The limit passed to exec-fun is a variable, which is assumed (in a hypothesis of the generated theorem) to be no smaller than a value that is calculated by the code generation code as sufficient to run exec-fun to completion.
The proof is a symbolic execution of the generated translation unit,
which is a constant: see atc-symbolic-execution-rules.
The proof is carried out in the theory that consists of exactly
the general rules in *atc-all-rules*,
some structure-specific rules that are similar to
rules for arrays in *atc-all-rules*,
plus the definition of not (more on this below),
plus the definition of
Furthermore, we generate a
We also generate a hint to expand all lambdas (i.e. beta reduction). We found at least one instance in which ACL2's heuristics were preventing a lambda expansion that was preventing a proof.
Given that we pass correctness theorems for the called functions, we expect that the opener rule for exec-fun only applies to the call of the function that this theorem refers to, because the correctness theorems come later in the ACL2 history and thus are tried first.
We use b* bindings in parts of the theorem to make certain variable substitution. Using bindings results in more readable formulas, in general, than generating terms with the substitutions applied, particularly if the same substituted variable occurs more than once. With the bindings, we let ACL2 perform the substitution at proof time.
If
This theorem is not generated if
Function:
(defun atc-gen-cfun-correct-thm (fn typed-formals type affect prec-fns prec-tags prec-objs prog-const compst-var fenv-var limit-var fn-thms fn-fun-env-thm limit state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (atc-symbol-varinfo-alistp typed-formals) (typep type) (symbol-listp affect) (atc-symbol-fninfo-alistp prec-fns) (atc-string-taginfo-alistp prec-tags) (atc-string-objinfo-alistp prec-objs) (symbolp prog-const) (symbolp compst-var) (symbolp fenv-var) (symbolp limit-var) (symbol-symbol-alistp fn-thms) (symbolp fn-fun-env-thm) (pseudo-termp limit)))) (let ((__function__ 'atc-gen-cfun-correct-thm)) (declare (ignorable __function__)) (b* ((wrld (w state)) (name (cdr (assoc-eq fn fn-thms))) (formals (strip-cars typed-formals)) (result-var (if (type-case type :void) nil (genvar$ 'atc "RESULT" nil formals state))) ((mv formals-bindings hyps subst instantiation) (atc-gen-outer-bindings-and-hyps typed-formals compst-var nil prec-objs)) (diff-pointer-hyps (atc-gen-object-disjoint-hyps (strip-cdrs subst))) (hyps (cons 'and (cons (cons 'compustatep (cons compst-var 'nil)) (cons (cons 'equal (cons fenv-var (cons (cons 'init-fun-env (cons (cons 'preprocess (cons prog-const 'nil)) 'nil)) 'nil))) (cons (cons 'integerp (cons limit-var 'nil)) (cons (cons '>= (cons limit-var (cons limit 'nil))) (append hyps (append diff-pointer-hyps (cons (untranslate$ (uguard+ fn wrld) nil state) 'nil))))))))) (exec-fun-args (fsublis-var-lst subst (atc-filter-exec-fun-args formals prec-objs))) (affect-new (acl2::add-suffix-to-fn-lst affect "-NEW")) (fn-results (append (if (type-case type :void) nil (list result-var)) affect-new)) (fn-binder (if (endp (cdr fn-results)) (car fn-results) (cons 'mv fn-results))) (final-compst (atc-gen-cfun-final-compustate affect typed-formals subst compst-var prec-objs)) (concl (cons 'equal (cons (cons 'exec-fun (cons (cons 'ident (cons (symbol-name fn) 'nil)) (cons (cons 'list exec-fun-args) (cons compst-var (cons fenv-var (cons limit-var 'nil)))))) (cons (cons 'b* (cons (cons (cons fn-binder (cons (cons fn formals) 'nil)) 'nil) (cons (cons 'mv (cons result-var (cons final-compst 'nil))) 'nil))) 'nil)))) (formula (cons 'b* (cons formals-bindings (cons (cons 'implies (cons hyps (cons concl 'nil))) 'nil)))) (called-fns (all-fnnames (ubody+ fn wrld))) (not-error-thms (atc-string-taginfo-alist-to-not-error-thms prec-tags)) (valuep-thms (atc-string-taginfo-alist-to-valuep-thms prec-tags)) (value-kind-thms (atc-string-taginfo-alist-to-value-kind-thms prec-tags)) (result-thms (atc-symbol-fninfo-alist-to-result-thms prec-fns called-fns)) (struct-reader-return-thms (atc-string-taginfo-alist-to-reader-return-thms prec-tags)) (struct-writer-return-thms (atc-string-taginfo-alist-to-writer-return-thms prec-tags)) (correct-thms (atc-symbol-fninfo-alist-to-correct-thms prec-fns called-fns)) (measure-thms (atc-symbol-fninfo-alist-to-measure-nat-thms prec-fns (strip-cars prec-fns))) (type-prescriptions-called (loop$ for called in (strip-cars prec-fns) collect (cons ':t (cons called 'nil)))) (type-prescriptions-struct-readers (loop$ for reader in (atc-string-taginfo-alist-to-readers prec-tags) collect (cons ':t (cons reader 'nil)))) (type-of-value-thms (atc-string-taginfo-alist-to-type-of-value-thms prec-tags)) (flexiblep-thms (atc-string-taginfo-alist-to-flexiblep-thms prec-tags)) (member-read-thms (atc-string-taginfo-alist-to-member-read-thms prec-tags)) (member-write-thms (atc-string-taginfo-alist-to-member-write-thms prec-tags)) (extobj-recognizers (atc-string-objinfo-alist-to-recognizers prec-objs)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'union-theories (cons '(theory 'atc-all-rules) (cons (cons 'quote (cons (cons 'not-errorp-when-expr-valuep (append not-error-thms (append valuep-thms (append value-kind-thms (cons 'not (append result-thms (append struct-reader-return-thms (append struct-writer-return-thms (append type-of-value-thms (append flexiblep-thms (append member-read-thms (append member-write-thms (append type-prescriptions-called (append type-prescriptions-struct-readers (append extobj-recognizers (append correct-thms (append measure-thms (cons fn-fun-env-thm 'nil)))))))))))))))))) 'nil)) 'nil))) (cons ':use (cons (cons ':instance (cons (cons ':guard-theorem (cons fn 'nil)) (cons ':extra-bindings-ok (alist-to-doublets instantiation)))) '(:expand (:lambdas))))))) (cons (cons 'and (cons 'stable-under-simplificationp (cons (cons 'quote (cons (cons ':in-theory (cons (cons 'union-theories (cons '(theory 'atc-all-rules) (cons (cons 'quote (cons (cons fn (cons 'not-errorp-when-expr-valuep (append not-error-thms (append valuep-thms (append value-kind-thms (cons 'not (append result-thms (append struct-reader-return-thms (append struct-writer-return-thms (append type-of-value-thms (append flexiblep-thms (append member-read-thms (append member-write-thms (append type-prescriptions-called (append type-prescriptions-struct-readers (append extobj-recognizers (append correct-thms (append measure-thms (cons fn-fun-env-thm 'nil))))))))))))))))))) 'nil)) 'nil))) 'nil)) 'nil)) 'nil))) 'nil))) ((mv local-event exported-event) (evmac-generate-defthm name :formula formula :hints hints :enable nil)) (print-event (cons 'cw-event (cons '"~%~x0~|" (cons (cons 'quote (cons exported-event 'nil)) 'nil))))) (mv (list local-event exported-event) print-event name))))
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-cfun-correct-thm.events (b* (((mv ?events ?print-event ?name) (atc-gen-cfun-correct-thm fn typed-formals type affect prec-fns prec-tags prec-objs prog-const compst-var fenv-var limit-var fn-thms fn-fun-env-thm limit state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-formp-of-atc-gen-cfun-correct-thm.print-event (b* (((mv ?events ?print-event ?name) (atc-gen-cfun-correct-thm fn typed-formals type affect prec-fns prec-tags prec-objs prog-const compst-var fenv-var limit-var fn-thms fn-fun-env-thm limit state))) (pseudo-event-formp print-event)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-cfun-correct-thm.name (implies (symbol-symbol-alistp fn-thms) (b* (((mv ?events ?print-event ?name) (atc-gen-cfun-correct-thm fn typed-formals type affect prec-fns prec-tags prec-objs prog-const compst-var fenv-var limit-var fn-thms fn-fun-env-thm limit state))) (symbolp name))) :rule-classes :rewrite)