		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-code-generation

Atj-shallow-fns-that-may-throw

Calculate the functions whose corresponding Java methods may throw an Acl2UndefinedPackageException.

Signature
(atj-shallow-fns-that-may-throw fns-to-translate call-graph) → fns-that-may-throw
Arguments: fns-to-translate — Guard (symbol-listp fns-to-translate).; call-graph — Guard (symbol-symbollist-alistp call-graph).
Returns: fns-that-may-throw — Type (symbol-listp fns-that-may-throw).

Among the natively implemented ACL2 functions, pkg-witness and pkg-imports may cause errors (when called on non-existent packages); their corresponding Java methods may throw Acl2UndefinedPackageExceptions. Thus, any method that calls these methods, directly or indirectly, must declare that exception. The Java methods' call graph is the same as the ACL2 functions'; thus, we can look at the ACL2 call graph to determine which functions may cause non-existent package errors, and thus whose corresponding methods must declare the exception.

The call graph is in the format amenable to the dependency graph library. We use depgraph::transdeps to calculate all the functions in the call graph that call pkg-witness or pkg-imports directly or indirectly. But first, we need to invert the graph (via depgraph::invert), because the edges in our call graph go from callers to callees, while here we want to find all the functions that pkg-witness and pkg-imports are called by.

We return a list of the functions in the call graph that call pkg-witness and pkg-imports directly or indirectly. The result of depgraph::transdeps always includes the inputs pkg-witness and pkg-imports, even when these functions do not appear in the call graph. Thus, eliminate them from the result if they are not among the functions to translate.

Definitions and Theorems

Function: atj-shallow-fns-that-may-throw

(defun atj-shallow-fns-that-may-throw (fns-to-translate call-graph)
 (declare
      (xargs :guard (and (symbol-listp fns-to-translate)
                         (symbol-symbollist-alistp call-graph))))
 (let ((__function__ 'atj-shallow-fns-that-may-throw))
  (declare (ignorable __function__))
  (b*
   ((inv-call-graph (depgraph::invert call-graph))
    (callers (depgraph::transdeps (list 'pkg-witness 'pkg-imports)
                                  inv-call-graph))
    ((unless (symbol-listp callers))
     (raise
      "Internal error: ~
                callers ~x0 of PKG-WITNESS and PKG-IMPORTS are not all symbols."
      callers)))
   (intersection-eq callers fns-to-translate))))

Theorem: symbol-listp-of-atj-shallow-fns-that-may-throw

(defthm symbol-listp-of-atj-shallow-fns-that-may-throw
 (b*
  ((fns-that-may-throw
      (atj-shallow-fns-that-may-throw fns-to-translate call-graph)))
  (symbol-listp fns-that-may-throw))
 :rule-classes :rewrite)