|
|
|---|
|
|
|
|---|
Generate the theorem about the result(s) of
(atc-gen-fn-result-thm fn type?
affect typed-formals prec-fns prec-tags
prec-objs names-to-avoid state)
→
(mv events name updated-names-to-avoid)This is a local theorem for now.
The restrictions on the form of the functions that ATC translates to C ensures that, under the guard, these functions always return C values. This is fairly easy to see, thinking of the different allowed forms of these functions' bodies:
This suggests a coarse but adequate proof strategy:
We use the theory consisting of
the definition of
In the absence of mbt, we would not need all of the guard as hypothesis, but only the part that constrains the formal parameters to be C values. These hypotheses are needed when the function returns them; when instead the function returns a representation of some operation, e.g. a call of sint-dec-const or add-sint-sint, these return C values unconditionally, so no hypotheses are needed. This is because ATC, when generating C code, ensures that the ACL2 terms follow the C typing rules, whether the terms are reachable under the guards or not. However, in the presence of mbt, we need the guard to exclude the `else' branches, which are otherwise unconstrained.
As explained in the user documentation,
an ACL2 function may return a combination of
an optional C result
and zero or more affected variables or arrays or structures.
We collect all of them.
The C result is determined from the optional C type of the function,
which is
If
Terms may appear during the proof of this theorem, where mv-nths are applied to lists (i.e. cons nests). So we add the rule
Theorem:
(defthm mv-nth-of-cons (implies (syntaxp (quotep acl2::n)) (equal (mv-nth acl2::n (cons acl2::a acl2::b)) (if (zp acl2::n) acl2::a (mv-nth (1- acl2::n) acl2::b)))))to the theory, in order to simplify those terms. We also enable the executable counterpart of zp to simplify the test in the right-hand side of that rule.
For each result of the function, we always generate an assertion about its C type.
We also generate assertions saying that the results are not
We also generate assertions saying that each array returned by the function has the same length as the corresponding input array. This is necessary for the correctness proofs of functions that call this function.
Function:
(defun atc-gen-fn-result-thm-aux1 (affect typed-formals) (declare (xargs :guard (and (symbol-listp affect) (atc-symbol-varinfo-alistp typed-formals)))) (let ((__function__ 'atc-gen-fn-result-thm-aux1)) (declare (ignorable __function__)) (cond ((endp affect) nil) (t (b* ((info (cdr (assoc-eq (car affect) typed-formals)))) (if (atc-var-infop info) (acons (car affect) (atc-var-info->type info) (atc-gen-fn-result-thm-aux1 (cdr affect) typed-formals)) (raise "Internal error: variable ~x0 not found in ~x1." (car affect) typed-formals)))))))
Theorem:
(defthm symbol-type-alistp-of-atc-gen-fn-result-thm-aux1 (implies (symbol-listp affect) (b* ((results (atc-gen-fn-result-thm-aux1 affect typed-formals))) (symbol-type-alistp results))) :rule-classes :rewrite)
Function:
(defun atc-gen-fn-result-thm-aux2 (results index? fn-call prec-tags) (declare (xargs :guard (and (symbol-type-alistp results) (maybe-natp index?) (pseudo-termp fn-call) (atc-string-taginfo-alistp prec-tags)))) (let ((__function__ 'atc-gen-fn-result-thm-aux2)) (declare (ignorable __function__)) (b* (((when (endp results)) nil) (theresult (if index? (cons 'mv-nth (cons index? (cons fn-call 'nil))) fn-call)) ((cons name type) (car results)) (type-conjunct (cons (atc-type-to-recognizer type prec-tags) (cons theresult 'nil))) (nonnil-conjunct? (and index? (list theresult))) (arraylength-conjunct? (b* (((unless (type-case type :array)) nil) (elemtype (type-array->of type)) ((unless (type-nonchar-integerp elemtype)) nil) (elemtype-array-length (pack (integer-type-to-fixtype elemtype) '-array-length))) (list (cons 'equal (cons (cons elemtype-array-length (cons theresult 'nil)) (cons (cons elemtype-array-length (cons name 'nil)) 'nil))))))) (append (list type-conjunct) nonnil-conjunct? arraylength-conjunct? (atc-gen-fn-result-thm-aux2 (cdr results) (and index? (1+ index?)) fn-call prec-tags)))))
Function:
(defun atc-gen-fn-result-thm (fn type? affect typed-formals prec-fns prec-tags prec-objs names-to-avoid state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (type-optionp type?) (symbol-listp affect) (atc-symbol-varinfo-alistp typed-formals) (atc-symbol-fninfo-alistp prec-fns) (atc-string-taginfo-alistp prec-tags) (atc-string-objinfo-alistp prec-objs) (symbol-listp names-to-avoid)))) (declare (xargs :guard (not (eq fn 'quote)))) (let ((__function__ 'atc-gen-fn-result-thm)) (declare (ignorable __function__)) (b* ((wrld (w state)) (results1 (and type? (not (type-case type? :void)) (list (cons nil type?)))) (results2 (atc-gen-fn-result-thm-aux1 affect typed-formals)) (results (append results1 results2)) ((unless (consp results)) (raise "Internal error: the function ~x0 has no results." fn) (mv nil nil names-to-avoid)) (formals (formals+ fn wrld)) (fn-call (cons fn formals)) (conjuncts (atc-gen-fn-result-thm-aux2 results (if (consp (cdr results)) 0 nil) fn-call prec-tags)) (conclusion (if (and (consp conjuncts) (not (consp (cdr conjuncts)))) (car conjuncts) (cons 'and conjuncts))) (name (add-suffix-to-fn fn (if (consp (cdr results)) "-RESULTS" "-RESULT"))) ((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix name nil names-to-avoid wrld)) (guard (untranslate$ (uguard+ fn wrld) t state)) (formula (cons 'implies (cons guard (cons conclusion 'nil)))) (hints (cons (cons '"Goal" (append (and (irecursivep+ fn wrld) (cons ':induct (cons fn-call 'nil))) (cons ':in-theory (cons (cons 'append (cons '*atc-integer-ops-1-return-rewrite-rules* (cons '*atc-integer-ops-2-return-rewrite-rules* (cons '*atc-integer-convs-return-rewrite-rules* (cons '*atc-array-read-return-rewrite-rules* (cons '*atc-array-write-return-rewrite-rules* (cons '*atc-integer-ops-1-type-prescription-rules* (cons '*atc-integer-ops-2-type-prescription-rules* (cons '*atc-integer-convs-type-prescription-rules* (cons '*atc-array-read-type-prescription-rules* (cons '*atc-array-write-type-prescription-rules* (cons '*atc-pointed-integers-type-prescription-rules* (cons '*atc-array-length-write-rules* (cons '*atc-wrapper-rules* (cons (cons 'quote (cons (cons '(:e tau-system) (cons fn (append (atc-symbol-fninfo-alist-to-result-thms prec-fns (all-fnnames (ubody+ fn wrld))) (append (atc-string-taginfo-alist-to-reader-return-thms prec-tags) (append (atc-string-taginfo-alist-to-writer-return-thms prec-tags) (append (atc-string-objinfo-alist-to-recognizers prec-objs) (cons 'sintp-of-sint-dec-const (cons 'sintp-of-sint-oct-const (cons 'sintp-of-sint-hex-const (cons 'uintp-of-uint-dec-const (cons 'uintp-of-uint-oct-const (cons 'uintp-of-uint-hex-const (cons 'slongp-of-slong-dec-const (cons 'slongp-of-slong-oct-const (cons 'slongp-of-slong-hex-const (cons 'ulongp-of-ulong-dec-const (cons 'ulongp-of-ulong-oct-const (cons 'ulongp-of-ulong-hex-const (cons 'sllongp-of-sllong-dec-const (cons 'sllongp-of-sllong-oct-const (cons 'sllongp-of-sllong-hex-const (cons 'ullongp-of-ullong-dec-const (cons 'ullongp-of-ullong-oct-const (cons 'ullongp-of-ullong-hex-const (cons 'scharp-of-schar-read (cons 'ucharp-of-uchar-read (cons 'sshortp-of-sshort-read (cons 'ushortp-of-ushort-read (cons 'sintp-of-sint-read (cons 'uintp-of-uint-read (cons 'slongp-of-slong-read (cons 'ulongp-of-ulong-read (cons 'sllongp-of-sllong-read (cons 'ullongp-of-ullong-read (cons 'scharp-of-schar-write (cons 'ucharp-of-uchar-write (cons 'sshortp-of-sshort-write (cons 'ushortp-of-ushort-write (cons 'sintp-of-sint-write (cons 'uintp-of-uint-write (cons 'slongp-of-slong-write (cons 'ulongp-of-ulong-write (cons 'sllongp-of-sllong-write (cons 'ullongp-of-ullong-write (cons '(:t sint-dec-const) (cons '(:t sint-oct-const) (cons '(:t sint-hex-const) (cons '(:t uint-dec-const) (cons '(:t uint-oct-const) (cons '(:t uint-hex-const) (cons '(:t slong-dec-const) (cons '(:t slong-oct-const) (cons '(:t slong-hex-const) (cons '(:t ulong-dec-const) (cons '(:t ulong-oct-const) (cons '(:t ulong-hex-const) (cons '(:t sllong-dec-const) (cons '(:t sllong-oct-const) (cons '(:t sllong-hex-const) (cons '(:t ullong-dec-const) (cons '(:t ullong-oct-const) (cons '(:t ullong-hex-const) (append (loop$ for reader in (atc-string-taginfo-alist-to-readers prec-tags) collect (cons ':t (cons reader 'nil))) (append (loop$ for writer in (atc-string-taginfo-alist-to-writers prec-tags) collect (cons ':t (cons writer 'nil))) (cons 'sintp-of-sint-from-boolean (cons 'mv-nth-of-cons (cons '(:e zp) (cons '(:e ucharp) (cons '(:e scharp) (cons '(:e ushortp) (cons '(:e sshortp) (cons '(:e uintp) (cons '(:e sintp) (cons '(:e ulongp) (cons '(:e slongp) (cons '(:e ullongp) (cons '(:e sllongp) (cons '(:e uchar-arrayp) (cons '(:e schar-arrayp) (cons '(:e ushort-arrayp) (cons '(:e sshort-arrayp) (cons '(:e uint-arrayp) (cons '(:e sint-arrayp) (cons '(:e ulong-arrayp) (cons '(:e slong-arrayp) (cons '(:e ullong-arrayp) (cons '(:e sllong-arrayp) (loop$ for recog in (atc-string-taginfo-alist-to-recognizers prec-tags) collect (cons ':e (cons recog 'nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 'nil)) 'nil))))))))))))))) 'nil)))) (cons (cons 'quote (cons (cons ':use (cons (cons ':guard-theorem (cons fn 'nil)) 'nil)) 'nil)) 'nil))) ((mv event &) (evmac-generate-defthm name :formula formula :hints hints :enable nil))) (mv (list event) name names-to-avoid))))
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-fn-result-thm.events (b* (((mv ?events ?name ?updated-names-to-avoid) (atc-gen-fn-result-thm fn type? affect typed-formals prec-fns prec-tags prec-objs names-to-avoid state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-fn-result-thm.name (b* (((mv ?events ?name ?updated-names-to-avoid) (atc-gen-fn-result-thm fn type? affect typed-formals prec-fns prec-tags prec-objs names-to-avoid state))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-fn-result-thm.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?events ?name ?updated-names-to-avoid) (atc-gen-fn-result-thm fn type? affect typed-formals prec-fns prec-tags prec-objs names-to-avoid state))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)