		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-cfun-correct-thm

Generate the correctness theorem for a C function.

Signature
(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)
Arguments: fn — Guard (symbolp fn).; typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; type — Guard (typep type).; affect — Guard (symbol-listp affect).; prec-fns — Guard (atc-symbol-fninfo-alistp prec-fns).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; prec-objs — Guard (atc-string-objinfo-alistp prec-objs).; prog-const — Guard (symbolp prog-const).; compst-var — Guard (symbolp compst-var).; fenv-var — Guard (symbolp fenv-var).; limit-var — Guard (symbolp limit-var).; fn-thms — Guard (symbol-symbol-alistp fn-thms).; fn-fun-env-thm — Guard (symbolp fn-fun-env-thm).; limit — Guard (pseudo-termp limit).
Returns: events — Type (pseudo-event-form-listp events).; print-event — Type (pseudo-event-formp print-event).; name — Type (symbolp name), given (symbol-symbol-alistp fn-thms).

In a computation state compst, the execution of the C function is expressed by calling exec-fun on the name of fn, the formals of fn, the computation state compst, the function environment for the translation unit, and a suitably large limit (more on this below). In this generated theorem, the first result of exec-fun is equated to either (i) the first (possibly only) result of a call of fn when it represents a non-void C function, or (ii) nil when fn represents a void C function. The second result of exec-fun is equated to the computation state calculated by atc-gen-cfun-final-compustate.

The function fn returns an optional C result and zero or more modified arrays and structures. If it returns a C result (i.e. if the C function is not void), we bind a result variable to it; the value is nil if the C function is void. We also bind the formals that are arrays or structures to the (other or only) results of fn (if any). We actually use new variables for the latter, for greater clarity in the theorem formulation: the new variables are obtained by adding -NEW to the corresponding array and structure formals of fn; these new names should not cause any conflicts, because the names of the formals must be portable C identifiers.

The guard of fn is used as hypothesis, along with the fact that compst is a computation state.

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 (init-fun-env <program>) directly as argument of exec-fun, is that we want to use this theorem as a rewrite rule, and using a variable makes the rule easier to match with, in particular since the init-fun-env call gets rewritten via the theorem about init-fun-env.

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 fn (clearly), plus the theorems about the results of the functions called by fn, plust the type prescriptions of the functions called by fn, plus the correctness theorems of the functions called by fn, plus the theorems asserting that the measures of all the preceding recursive functions are naturals (we take all the measures, not just the ones of the directly called functions, because the limit bound may include a measure from an indirectly called function), plus the theorem about the current function in the function environment; here `called' means `directly called'. During symbolic execution, the initial limit for fn is progressively decremented, so by the time we get to functions called by fn it will have different symbolic values from the initial variable; thus, we need to match that to the variable limit in the correctness theorems for the callees, which are used as rewrite rules to turn calls of exec-fun into calls of the corresponding ACL2 functions. These will thus match the calls in the definition of fn, and the called functions can stay disabled in the proof. The theorems about the called functions' results are needed to exclude, in the proof, the case that these functions return errors. The type prescriptions of the callable functions are needed to discharge some proof subgoal that arise. We enable not because, without it, we have found at least one case in which some ACL2 heuristic defeats what should be a propositional inference; the issue is related to clausification, and enabling not seems to overcome the issue, at least in that case we found.

Furthermore, we generate a :use hint to augment the theorem's formula with the guard theorem of fn, with the pointer arguments replaced by the dereferenced arrays and structures. This is critical to ensure that the symbolic execution of the C operators does not split on the error cases: the fact that fn is guard-verified ensures that add-sint-sint and similar functions are always called on values such that the exact result fit into the type, which is the same condition under which the dynamic semantics does not error on the corresponding operators.

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 fn has conditional (i.e. ifs), the C function has corresponding (expression and statement) conditionals. During the proof, all these condtionals, in fn and in the C function, may cause case splits, which make the proof slow. In an attempt to improve speed, we perform the symbolic execution execution of the C function while keeping fn closed, so that fn does not cause case splits during the symbolic execution. Then, once we reach stability (see stable-under-simplificationp), we open fn, which may cause case splits, and complete the proof. The second part of the proof probably does not need all the rules from the first part, which for now we use for simplicity; so we should be able to use simpler hints there eventually.

This theorem is not generated if :proofs is nil.

Definitions and Theorems

Function: atc-gen-cfun-correct-thm

(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
                                '(return-type-of-stmt-value-none
                                  expr-value-optionp-when-expr-valuep
                                  (:e expr-value-optionp)
                                  expr-valuep-of-expr-value)))))))))))))))))))
              '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
                         (cons
                          'return-type-of-stmt-value-return
                          (cons
                           'return-type-of-stmt-value-none
                           (cons
                            'stmt-value-return->value?-of-stmt-value-return
                            (cons
                             'value-option-fix-when-value-optionp
                             (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
                                          '(return-type-of-stmt-value-none
                                            expr-value-optionp-when-expr-valuep
                                            (:e expr-value-optionp)
                                            expr-valuep-of-expr-value))))))))))))))))))))))))
                   '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: pseudo-event-form-listp-of-atc-gen-cfun-correct-thm.events

(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: pseudo-event-formp-of-atc-gen-cfun-correct-thm.print-event

(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: symbolp-of-atc-gen-cfun-correct-thm.name

(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)