		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-loop-final-compustate

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

Signature
(atc-gen-loop-final-compustate mod-vars typed-formals subst compst-var prec-objs) → term
Arguments: mod-vars — Guard (symbol-listp mod-vars).; 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 loop says that executing the loop on a generic computation state (satisfying conditions in the hypotheses of the theorem) yields a computation state obtained by modifying one or more variables and zero or more arrays in the computation state. These are the variables and arrays affected by the loop, which the correctness theorem binds to the results of the loop function, and which have corresponding named variables and heap arrays in the computation state. The modified computation state is expressed as a nest of write-var, write-static-var, and write-object calls. This ACL2 code here generates that nest.

Note that, in the correctness theorem, the new array variables are bound to the possibly modified arrays returned by the ACL2 function: these new array 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-loop-final-compustate

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