From 3b76874834abb56fac91ca3b5af362b73c68b929 Mon Sep 17 00:00:00 2001
From: Jamey Sharp <jsharp@fastly.com>
Date: Tue, 29 Nov 2022 11:02:12 -0800
Subject: [PATCH] cranelift-isle: Fix representation for overlap checks (#5337)

Ulrich Weigand identified two bugs in this code due to it falsely
claiming there were unreachable rules in the s390x backend. The fixes
are:

- Add constraints for pure constructors.

I didn't notice that a constructor which is declared pure (which
currently implies that it is fallible), when used on the left-hand side
of a rule, can cause the rule to fail to match. Therefore, any
constructors on the left-hand side must be noted as additional
constraints on the rule, so that overlap checking can see them.

- Ignore subset-overlaps for rules with equality constraints

This eliminates false positives when checking for unreachable rules. It
introduces false negatives instead but we prefer to fail to detect an
error instead of claiming that valid input is wrong. We can implement a
more accurate check later.
---
 cranelift/isle/isle/src/trie_again.rs | 49 +++++++++++++++++++++++----
 1 file changed, 43 insertions(+), 6 deletions(-)

diff --git a/cranelift/isle/isle/src/trie_again.rs b/cranelift/isle/isle/src/trie_again.rs
index b0af04e926..ff046ece3a 100644
--- a/cranelift/isle/isle/src/trie_again.rs
+++ b/cranelift/isle/isle/src/trie_again.rs
@@ -212,9 +212,9 @@ impl Rule {
         // For the purpose of overlap checking, equality constraints act like other constraints, in
         // that they can cause rules to not overlap. However, because we don't have a concrete
         // pattern to compare, the analysis to prove that is complicated. For now, we approximate
-        // the result. If `small` has any of these nonlinear constraints, conservatively report that
-        // it is not a subset of `big`.
-        let mut subset = small.equals.is_empty();
+        // the result. If either rule has nonlinear constraints, conservatively report that neither
+        // is a subset of the other.
+        let mut subset = small.equals.is_empty() && big.equals.is_empty();
 
         for (binding, a) in small.constraints.iter() {
             if let Some(b) = big.constraints.get(binding) {
@@ -438,6 +438,32 @@ impl RuleSetBuilder {
             self.unreachable.push(e);
         }
     }
+
+    fn add_pattern_constraints(&mut self, expr: BindingId) {
+        match &self.rules.bindings[expr.index()] {
+            Binding::ConstInt { .. } | Binding::ConstPrim { .. } | Binding::Argument { .. } => {}
+            Binding::Constructor {
+                parameters: sources,
+                ..
+            }
+            | Binding::MakeVariant {
+                fields: sources, ..
+            } => {
+                for source in sources.to_vec() {
+                    self.add_pattern_constraints(source);
+                }
+            }
+            &Binding::Extractor {
+                parameter: source, ..
+            }
+            | &Binding::MatchVariant { source, .. }
+            | &Binding::MatchTuple { source, .. } => self.add_pattern_constraints(source),
+            &Binding::MatchSome { source } => {
+                self.set_constraint(source, Constraint::Some);
+                self.add_pattern_constraints(source);
+            }
+        }
+    }
 }
 
 impl sema::PatternVisitor for RuleSetBuilder {
@@ -540,13 +566,23 @@ impl sema::ExprVisitor for RuleSetBuilder {
         inputs: Vec<(BindingId, sema::TypeId)>,
         _ty: sema::TypeId,
         term: sema::TermId,
-        _infallible: bool,
+        infallible: bool,
         _multi: bool,
     ) -> BindingId {
-        self.dedup_binding(Binding::Constructor {
+        let source = self.dedup_binding(Binding::Constructor {
             term,
             parameters: inputs.into_iter().map(|(expr, _)| expr).collect(),
-        })
+        });
+
+        // If the constructor is fallible, build a pattern for `Some`, but not a constraint. If the
+        // constructor is on the right-hand side of a rule then its failure is not considered when
+        // deciding which rule to evaluate. Corresponding constraints are only added if this
+        // expression is subsequently used as a pattern; see `expr_as_pattern`.
+        if infallible {
+            source
+        } else {
+            self.dedup_binding(Binding::MatchSome { source })
+        }
     }
 }
 
@@ -572,6 +608,7 @@ impl sema::RuleVisitor for RuleSetBuilder {
     }
 
     fn expr_as_pattern(&mut self, expr: BindingId) -> BindingId {
+        self.add_pattern_constraints(expr);
         expr
     }