		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-call-result-and-endstate

Generate a term representing the result value and a term representing the ending computation state of the execution of a C function call.

Signature
(atc-gen-call-result-and-endstate type affect inscope compst-var call) → (mv result new-compst)
Arguments: type — Return type of the C function.
Guard (typep type).; affect — Variables affected by the C function.
Guard (symbol-listp affect).; inscope — Guard (atc-symbol-varinfo-alist-listp inscope).; compst-var — Guard (symbolp compst-var).; call — An untranslated term.
Returns: result — An untranslated term.; new-compst — An untranslated term.

If no variables are affected, the computation state is unchanged, and the call is the result. (In this case the type is not void, but this is not an explicitly checked invariant in this code.)

Otherwise, if exactly one variable is affected, and additionally the function is void, we return nil as the result term, while the new computation state is obtained by updating the affected object with the call.

Otherwise, there are two cases. If the function is void, we return nil as result term, and as new computation state we return the nest of object updates for all the mv-nth components of the call, starting with index 0. If the function is not void, we return the mv-nth of index 0 of the call as result term, and as new computation state the nest of object updates with the mv-nth components starting with index 1. In either case, the nest is calculated by an auxiliary function.

Definitions and Theorems

Function: atc-gen-call-endstate

(defun atc-gen-call-endstate (affect inscope compst-var call index)
 (declare
      (xargs :guard (and (symbol-listp affect)
                         (atc-symbol-varinfo-alist-listp inscope)
                         (symbolp compst-var)
                         (natp index))))
 (let ((__function__ 'atc-gen-call-endstate))
  (declare (ignorable __function__))
  (b*
   (((when (endp affect)) compst-var)
    (var (car affect))
    (info (atc-get-var var inscope))
    ((when (not info))
     (raise "Internal error: variable ~x0 not found."
            var))
    (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 variable ~x0 ~
                   has type ~x1 and is not an external object."
      var type)))
   (if
    (atc-var-info->externalp info)
    (cons
     'update-static-var
     (cons
      (cons 'ident
            (cons (symbol-name var) 'nil))
      (cons
       (cons 'mv-nth
             (cons index (cons call 'nil)))
       (cons
          (atc-gen-call-endstate (cdr affect)
                                 inscope compst-var call (1+ index))
          'nil))))
    (cons
     'update-object
     (cons
      (add-suffix-to-fn var "-OBJDES")
      (cons
       (cons 'mv-nth
             (cons index (cons call 'nil)))
       (cons
          (atc-gen-call-endstate (cdr affect)
                                 inscope compst-var call (1+ index))
          'nil))))))))

Function: atc-gen-call-result-and-endstate

(defun atc-gen-call-result-and-endstate
       (type affect inscope compst-var call)
 (declare
      (xargs :guard (and (typep type)
                         (symbol-listp affect)
                         (atc-symbol-varinfo-alist-listp inscope)
                         (symbolp compst-var))))
 (let ((__function__ 'atc-gen-call-result-and-endstate))
  (declare (ignorable __function__))
  (b*
   (((when (endp affect))
     (mv call compst-var))
    ((when (and (endp (cdr affect))
                (type-case type :void)))
     (b*
      ((var (car affect))
       (info (atc-get-var var inscope))
       ((when (not info))
        (raise "Internal error: variable ~x0 not found."
               var)
        (mv nil nil))
       (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 variable ~x0 ~
                      has type ~x1 and is not an external object."
         var type)
        (mv nil nil))
       (new-compst
            (if (atc-var-info->externalp info)
                (cons 'update-static-var
                      (cons (cons 'ident
                                  (cons (symbol-name var) 'nil))
                            (cons call (cons compst-var 'nil))))
              (cons 'update-object
                    (cons (add-suffix-to-fn var "-OBJDES")
                          (cons call (cons compst-var 'nil)))))))
      (mv nil new-compst))))
   (if (type-case type :void)
       (mv nil
           (atc-gen-call-endstate affect inscope compst-var call 0))
    (mv
       (cons 'mv-nth
             (cons '0 (cons call 'nil)))
       (atc-gen-call-endstate affect inscope compst-var call 1))))))