Generate a term representing the final computation state after the execution of a C loop.
(atc-gen-loop-final-compustate mod-vars typed-formals subst compst-var prec-objs) → 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
Function:
(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))))))))