		Search-engine friendly clone of the ACL2 documentation.

Atj-input-processing

Atj-worklist-iterate

Worklist algorithm iteration.

Signature
(atj-worklist-iterate worklist-gen worklist-chk collected-gen collected-chk call-graph deep$ guards$ ignore-whitelist$ verbose$ ctx state) → (mv erp result state)
Arguments: worklist-gen — Guard (symbol-listp worklist-gen).; worklist-chk — Guard (symbol-listp worklist-chk).; collected-gen — Guard (symbol-listp collected-gen).; collected-chk — Guard (symbol-listp collected-chk).; call-graph — Guard (symbol-symbollist-alistp call-graph).; deep$ — Guard (booleanp deep$).; guards$ — Guard (booleanp guards$).; ignore-whitelist$ — Guard (booleanp ignore-whitelist$).; verbose$ — Guard (booleanp verbose$).; ctx — Guard (ctxp ctx).
Returns: result — A tuple (fns new-call-graph) satisfying (typed-tuplep symbol-listp symbol-symbollist-alistp result).

See the overview of the worklist algorithm first.

The iteration ends when both worklists are empty. When that happens, we return the collected list of functions for which code must be generated. We also return a call graph of these functions, as an alist from each function to a list of its directly called functions.

We always pick the next function from worklist-gen, until it is empty; then we switch to worklist-chk. Since we start with all empty lists except worklist-gen (see the caller of this function), as we go through worklist-gen we may populate collected-gen and worklist-chk, but not collected-chk. When we go through worklist-chk, we may further populate collected-chk, but not worklist-gen or collected-gen.

Initial lists:
  (...) () () ()
After processing the first worklist:
  () (...) (...) ()
After processing the second worklist:
  () () (...) (...)

The iteration terminates because there is a finite number of functions in the ACL2 world, but for simplicity we leave this function in program mode to avoid having to articulate the termination proof for now.

When we encounter a function that is natively implemented in AIJ, we do not examine its body (which the ACL2 primitive functions, all of which are natively implemented in AIJ, do not have anyhow): we just remove it from the worklist, and, if gen? is t, we add it to collected-gen, i.e. we include among the functions for which code must be generated. When :deep is nil and :guards is t, we apply the same treatment to the functions in *atj-jprim-fns* and *atj-jprimarr-fns*.

If the function satisfies all the needed constraints, its name is printed when verbose mode is on. The caller of this function precedes this printing with a suitable message (see the caller).

It should be an invariant that there are no duplicate function symbols in the four lists (worklists and collected lists) altogether; i.e. each list is free of duplicates, and the lists are pairwise disjoint.

Note that since atj-collect-fns-in-term extends the worklists via cons, and since the fixpoint iteration picks the next function via car, we visit the call graph depth-first; the worklists are used as stacks.

Definitions and Theorems

Function: atj-worklist-iterate

(defun atj-worklist-iterate
       (worklist-gen worklist-chk collected-gen
                     collected-chk call-graph deep$ guards$
                     ignore-whitelist$ verbose$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-listp worklist-gen)
                             (symbol-listp worklist-chk)
                             (symbol-listp collected-gen)
                             (symbol-listp collected-chk)
                             (symbol-symbollist-alistp call-graph)
                             (booleanp deep$)
                             (booleanp guards$)
                             (booleanp ignore-whitelist$)
                             (booleanp verbose$)
                             (ctxp ctx))))
 (let ((__function__ 'atj-worklist-iterate))
  (declare (ignorable __function__))
  (b*
   (((when (and (endp worklist-gen)
                (endp worklist-chk)))
     (value (list collected-gen call-graph)))
    ((mv fn gen? worklist-gen worklist-chk)
     (if (consp worklist-gen)
         (mv (car worklist-gen)
             t (cdr worklist-gen)
             worklist-chk)
       (mv (car worklist-chk)
           nil worklist-gen (cdr worklist-chk))))
    ((when (or (aij-nativep fn)
               (and (not deep$)
                    guards$
                    (or (atj-jprim-fn-p fn)
                        (atj-jprimarr-fn-p fn)))))
     (b* (((mv collected-gen collected-chk)
           (if gen? (mv (cons fn collected-gen)
                        collected-chk)
             (mv collected-gen collected-chk))))
       (atj-worklist-iterate worklist-gen worklist-chk collected-gen
                             collected-chk call-graph deep$ guards$
                             ignore-whitelist$ verbose$ ctx state)))
    ((when (and (rawp fn state)
                (not ignore-whitelist$)
                (not (pure-raw-p fn))))
     (er-soft+
      ctx t nil
      "The function ~x0 has raw Lisp code ~
                   and is not in the whitelist; ~
                   therefore, code generation cannot proceed."
      fn))
    ((unless (no-stobjs-p fn (w state)))
     (er-soft+
      ctx t nil
      "The function ~x0 has input or output stobjs; ~
                   therefore, code generation cannot proceed."
      fn))
    (body (atj-fn-body fn (w state)))
    ((unless body)
     (er-soft+
      ctx t nil
      "The function ~x0 has no unnormalized body ~
                   and no suitable attachment; ~
                   therefore, code generation cannot proceed."
      fn))
    ((run-when verbose$) (cw "  ~x0~%" fn))
    ((mv collected-gen collected-chk)
     (if gen? (mv (cons fn collected-gen)
                  collected-chk)
       (mv collected-gen (cons fn collected-chk))))
    ((mv worklist-gen worklist-chk
         called-fns unsuppported-return-last?)
     (atj-collect-fns-in-term body gen? worklist-gen
                              worklist-chk nil collected-gen
                              collected-chk deep$ guards$))
    ((when unsuppported-return-last?)
     (er-soft+
      ctx t nil
      "The function RETURN-LAST is used ~
                   with an unsupported first argument; ~
                   therefore, code generation cannot proceed."))
    (call-graph (acons fn called-fns call-graph)))
   (atj-worklist-iterate worklist-gen worklist-chk collected-gen
                         collected-chk call-graph deep$ guards$
                         ignore-whitelist$ verbose$ ctx state))))