Calculate the functions whose corresponding Java methods
may throw an
(atj-shallow-fns-that-may-throw fns-to-translate call-graph) → 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
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.
Function:
(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:
(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)