		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-find-affected

Find the variables affected by a term.

Signature
(atc-find-affected fn term typed-formals prec-fns wrld) → (mv erp affected)
Arguments: fn — Guard (symbolp fn).; term — Guard (pseudo-termp term).; typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; prec-fns — Guard (atc-symbol-fninfo-alistp prec-fns).; wrld — Guard (plist-worldp wrld).
Returns: affected — Type (symbol-listp affected), given (atc-symbol-varinfo-alistp typed-formals).

This is used on the body of each non-recursive target function fn, in order to determine the variables affected by it, according to the nomenclature in the user documentation. We visit the leaves of the term according to the if and let structure, and ensure that they all have the same form, which must be one of the following forms:

A call of a (recursive or non-recursive) target function fn0 that precedes fn in the list of targets. In this case, term affects the same variables as fn0. We use atc-check-cfun-call and atc-check-loop-call to check if the term is a call of a target function and to retrieve that function's affected variables: we pass nil as the variable-term alist, because it does not change the returned affected variables, which is the only thing we care about here, ignoring all the other results.
A formal parameter var of fn that either has pointer or array type or refers to an external object. In this case, term affects the list of variables (var).
A term ret that is not a call of fn0 as above and is not a formal parameter of fn that either has pointer or array type or refers to an external object. In this case, term affects no variables.
A term (mv var1 ... varn) where each vari is a formal parameter of the function that either has pointer or array type or refers to an external object. In this case, term affects the list of variables (var1 ... varn).
A term (mv ret var1 ... varn) where each vari is a formal parameter of the function that either has pointer or array type or refers to an external object, and ret is not. In this case, term affects the list of variables (var1 ... varn).

In checking that the terms at the leaves have the same form, we allow ret to vary, but the other parts must coincide.

When we encounter ifs with mbt tests, we recursively process the `then' branch, skipping the `else' branch. This is because only the `then' branch represents C code.

Definitions and Theorems

Function: atc-find-affected

(defun atc-find-affected (fn term typed-formals prec-fns wrld)
 (declare
      (xargs :guard (and (symbolp fn)
                         (pseudo-termp term)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (atc-symbol-fninfo-alistp prec-fns)
                         (plist-worldp wrld))))
 (let ((__function__ 'atc-find-affected))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((mv okp test then else)
     (fty-check-if-call term))
    ((when okp)
     (b* (((mv mbtp &) (check-mbt-call test))
          ((when mbtp)
           (atc-find-affected fn then typed-formals prec-fns wrld))
          ((erp then-affected)
           (atc-find-affected fn then typed-formals prec-fns wrld))
          ((erp else-affected)
           (atc-find-affected fn else typed-formals prec-fns wrld)))
      (if (equal then-affected else-affected)
          (retok then-affected)
       (reterr
        (msg
         "When generating code for function ~x0, ~
                   an IF branch affects variables ~x1, ~
                   while the other branch affects variables ~x2: ~
                   this is disallowed."
         fn then-affected else-affected)))))
    ((mv okp & body &)
     (fty-check-lambda-call term))
    ((when okp)
     (atc-find-affected fn body typed-formals prec-fns wrld))
    ((erp okp & & & & affected & & &)
     (atc-check-cfun-call term nil prec-fns wrld))
    ((when okp) (retok affected))
    ((mv okp & & & affected & &)
     (atc-check-loop-call term nil prec-fns))
    ((when okp) (retok affected))
    ((when (pseudo-term-case term :var))
     (b* ((var (pseudo-term-var->name term)))
       (if (atc-formal-affectablep var typed-formals)
           (retok (list var))
         (retok nil))))
    ((mv okp terms)
     (fty-check-list-call term))
    ((when okp)
     (cond
      ((and (symbol-listp terms)
            (atc-formal-affectable-listp terms typed-formals))
       (retok terms))
      ((and (symbol-listp (cdr terms))
            (atc-formal-affectable-listp (cdr terms)
                                         typed-formals))
       (retok (cdr terms)))
      (t
       (reterr
        (msg
         "When generating code for function ~x0, ~
                        a term ~x1 was encountered that ~
                        returns multiple values but they, ~
                        or at least all of them except the first one, ~
                        are not all formal parameters of ~x0 ~
                        of pointer or array type."
         fn term))))))
   (retok nil))))

Theorem: symbol-listp-of-atc-find-affected.affected

(defthm symbol-listp-of-atc-find-affected.affected
 (implies
     (atc-symbol-varinfo-alistp typed-formals)
     (b* (((mv acl2::?erp ?affected)
           (atc-find-affected fn term typed-formals prec-fns wrld)))
       (symbol-listp affected)))
 :rule-classes :rewrite)