		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-fun-endstate

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

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

This is similar to atc-gen-cfun-final-compustate, which eventually will be removed in favor of this one, once the new modular proof approach works for every C function generated by ATC.

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 objects in the computation state. These are the objects 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 objects 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 objects affected by the body of the ACL2 function that represents the C function. We go through affect and we construct each nested write-object call, which needs both a pointer and an object. This is the case for objects in the heap; for objects in static storage, we generate a call of write-static-var, and there are no pointers involved.

We add the suffix -new to each variable because these will be bound to the final values of the variables in the theorems generated by the callers of this ACL2 function.

Definitions and Theorems

Function: atc-gen-fun-endstate

(defun atc-gen-fun-endstate
       (affect typed-formals compst-var prec-objs)
 (declare
      (xargs :guard (and (symbol-listp affect)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (symbolp compst-var)
                         (atc-string-objinfo-alistp prec-objs))))
 (let ((__function__ 'atc-gen-fun-endstate))
  (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))
    (var (add-suffix-to-fn formal "-NEW")))
   (if
    (consp (assoc-equal (symbol-name formal)
                        prec-objs))
    (cons
     'write-static-var
     (cons
      (cons 'ident
            (cons (symbol-name formal) 'nil))
      (cons
       var
       (cons
           (atc-gen-fun-endstate (cdr affect)
                                 typed-formals compst-var prec-objs)
           'nil))))
    (cons
     'write-object
     (cons
      (add-suffix-to-fn formal "-OBJDES")
      (cons
       var
       (cons
           (atc-gen-fun-endstate (cdr affect)
                                 typed-formals compst-var prec-objs)
           'nil))))))))