		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-cfun-final-compustate

Generate a term representing the final computation state after the execution of a C function.

Signature
(atc-gen-cfun-final-compustate affect typed-formals subst compst-var prec-objs) → term
Arguments: affect — Guard (symbol-listp affect).; typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; subst — Guard (symbol-symbol-alistp subst).; compst-var — Guard (symbolp compst-var).; prec-objs — Guard (atc-string-objinfo-alistp prec-objs).
Returns: term — An untranslated term.

The correctness theorem of a C function says that executing the function on a generic computation state (satisfying conditions in the hypotheses of the theorem) and on generic arguments yields an optional result (absent if the function is void) and a computation state obtained by modifying zero or more arrays and structures in the computation state. These are the arrays and structures affected by the C function, which the correctness theorem binds to the results of the ACL2 function that represents the C function. The modified computation state is expressed as a nest of write-object and write-static-var calls, based on whether the affected object are in the heap or in static storage. This ACL2 code here generates that nest.

The parameter affect passed to this code consists of the formals of fn that represent arrays and structures affected by the body of the ACL2 function that represents the C function. The parameter subst is the result of atc-gen-outer-bindings-and-hyps that maps array and structure formals of the ACL2 function to the corresponding pointer variables used by the correctness theorems. Thus, we go through affect, looking up the corresponding pointer variables in subst, and we construct each nested write-object call, which needs both a pointer and an array or structure; we distinguish between arrays and structures via the types of the formals. This is the case for arrays and structures in the heap; for arrays in static storage, we generate a call of write-static-var, and there are no pointers involved.

Note that, in the correctness theorem, the new array and structure variables are bound to the possibly modified arrays and structures returned by the ACL2 function: these new array and structure variables are obtained by adding -NEW to the corresponding formals of the ACL2 function; these new names should not cause any conflicts, because the names of the formals must be portable C identifiers.

Definitions and Theorems

Function: atc-gen-cfun-final-compustate

(defun atc-gen-cfun-final-compustate
       (affect typed-formals
               subst compst-var prec-objs)
 (declare
      (xargs :guard (and (symbol-listp affect)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (symbol-symbol-alistp subst)
                         (symbolp compst-var)
                         (atc-string-objinfo-alistp prec-objs))))
 (let ((__function__ 'atc-gen-cfun-final-compustate))
  (declare (ignorable __function__))
  (b*
   (((when (endp affect)) compst-var)
    (formal (car affect))
    (info (cdr (assoc-eq formal typed-formals)))
    ((when (not info))
     (raise "Internal error: formal ~x0 not found."
            formal))
    (type (atc-var-info->type info))
    ((unless (or (type-case type :pointer)
                 (type-case type :array)
                 (atc-var-info->externalp info)))
     (raise
      "Internal error:
                affected formal ~x0 has type ~x1 and is not an external object."
      formal type)))
   (if
    (consp (assoc-equal (symbol-name formal)
                        prec-objs))
    (cons
     'write-static-var
     (cons
      (cons 'ident
            (cons (symbol-name formal) 'nil))
      (cons
       (add-suffix-to-fn formal "-NEW")
       (cons
          (atc-gen-cfun-final-compustate (cdr affect)
                                         typed-formals
                                         subst compst-var prec-objs)
          'nil))))
    (cons
     'write-object
     (cons
      (cons 'value-pointer->designator
            (cons (cdr (assoc-eq formal subst))
                  'nil))
      (cons
       (add-suffix-to-fn formal "-NEW")
       (cons
          (atc-gen-cfun-final-compustate (cdr affect)
                                         typed-formals
                                         subst compst-var prec-objs)
          'nil))))))))