ISLE: Language support for reasoning about recursion

[elliottt]

We've had a few issues recently with unbounded recursion in ISLE rules causing compilation time blowup: #7874 and #6968. As ISLE supports recursion, but unbounded recursion has caused some surprising behavior in the past, it would be nice if we had some tools to better reason about its use.

Feature

The straw-person feature I'd like to propose here is comes in two parts:

1. A new annotation for rule declarations (decl not rule), indicating the argument that is considered to be shrinking for the purpose of structural recursion,
2. The ISLE frontend is modified to analyze strongly connected components of decls, and all rules involved in cycles must have decls that include a structural recursion annotation.

Note one important detail: there's no analysis of whether or not structural recursion is actually happening on the annotated parameter, just that the annotation is present. The reason for this is that I believe forcing rule authors to think about how structural recursion happening by raising an error when the annotation is missing will be enough to avoid these sorts of cases. Additionally we could forbid structural recursion on specific types of arguments: forbidding structural recursion annotations on Value arguments would be a great way to avoid accidentally introducing exponential egraph rule behavior for large input functions.

More concretely, here's an example of what I'm thinking of, modifying the changes introduced in #7882:

(decl pure multi will_simplify_with_ireduce_rec ((:struct u8) Value) Value)
(rule (will_simplify_with_ireduce_rec _ x@(uextend _ _)) x)
(rule (will_simplify_with_ireduce_rec _ x@(sextend _ _)) x)
(rule (will_simplify_with_ireduce_rec _ x@(iconst _ _)) x)
(rule (will_simplify_with_ireduce_rec depth x@(unary_op _ _ a))
      (if-let _ (u8_lt 0 depth))
      (if-let _ (reducible_modular_op x))
      (if-let _ (will_simplify_with_ireduce_rec (u8_sub depth 1) a))
      x)
(rule (will_simplify_with_ireduce_rec depth x@(binary_op _ _ a b))
      (if-let _ (u8_lt 0 depth))
      (if-let _ (reducible_modular_op x))
      (if-let _ (will_simplify_with_ireduce_rec (u8_sub depth 1) a))
      (if-let _ (will_simplify_with_ireduce_rec (u8_sub depth 1) b))
      x)

;; Worst possible syntax here to forbid recursion through Value-typed arguments
(forbid_recursion Value)

The important parts in this example are the :struct annotation on the u8 parameter to will_simplify_with_ireduce_rec, and forbidding structural recursion on values of type Value.

There is already prior art for this sort of annotation in the coq theorem prover (though in that case the annotation is actually checked) where it's used to annotate recursive parameters when it's not obvious to the tool already.

Benefit

This would give us a mechanism for documenting structural recursion in ISLE rules as well as a way to forbid recursion on values whose structure we determine are problematic, providing a great place for user-friendly errors in the ISLE frontend.

Alternatives

An alternative proposal that @avanhatt had was to make fuel for recursive functions a language builtin, requiring the caller to explicitly provide fuel when calling a function from a recursive group. This would make it unavoidable that recursion would be finite in ISLE, and would include three changes:

1. As with the above approach, we would need to identify recursive rule groups by running strongly connected components
2. We would need to introduce a way to supply the fuel explicitly when calling into a recursive group
3. Codegen would need to change to support threading the fuel parameter through recursive functions

One open question here is if fuel would be threaded through generated functions, or passed in as an argument only. While the former would more accurately bound the number of calls in the recursive group, passing the recursion depth in only would be a simpler implementation choice, and may be fine for our purposes.

[github-actions]

Subscribe to Label Action

cc @cfallin, @fitzgen

This issue or pull request has been labeled: "isle"

Thus the following users have been cc'd because of the following labels:

• cfallin: isle
• fitzgen: isle

To subscribe or unsubscribe from this label, edit the .github/subscribe-to-label.json configuration file.

Learn more.