implemented lt as an astar-like algorithm

Co-authored-by: CF Bolz-Tereick <[email protected]>

rpython/jit/metainterp/optimizeopt/intrelational.py

@@ -145,25 +145,41 @@ def _make_lt(self, other):
                 assert isinstance(relation, BiggerOrEqual)
                 self.relations[index] = Bigger(other)
                 return
-        if self._known_le(other):
-            import pdb;pdb.set_trace()  # TODO: how to trigger this?
         self.relations.append(Bigger(other))
 
     def _known_lt(self, other):
-        todo = self.relations[:]
-        seen = dict()
-        seen_bigger = False
+        biggest_distance = self._astar(other)
+        return biggest_distance > 0
+
+    def _astar(self, other, cutoff=None):
+        todo = {self}
+        best_distance = {self: 0} # node -> best distance so far, from self
+        best_distance[other] = -1
         while todo:
-            relation = todo.pop()
-            interm = relation.other
-            seen_bigger = seen_bigger or type(relation) is Bigger
-            if interm in seen:
-                continue
-            if interm is other and seen_bigger:
-                return True
-            seen[interm] = None
-            todo.extend(interm.relations)
-        return False
+            # pick element from todo with biggest distance
+            # TODO: use a priority queue instead
+            best_distance_seen = -1
+            best = None
+            for current in todo:
+                if best_distance[current] > best_distance_seen:
+                    best_distance_seen = best_distance[current]
+                    best = current
+            if best is None:
+                current = todo.pop()
+            else:
+                todo.remove(best)
+                current = best
+            # found the goal?
+            for relation in current.relations:
+                tentative_score = best_distance[current] + relation.min_margin()
+                if tentative_score > best_distance.get(relation.other, -1):
+                    best_distance[relation.other] = tentative_score
+                    todo.add(relation.other)
+            # check cutoff
+            if cutoff is not None and best_distance[other] >= cutoff:
+                break
+
+        return best_distance[other]
 
     def _make_le(self, other):
         if other.known_lt(self):
@@ -194,16 +210,49 @@ def __str__(self):
         lines = self.pp()
         return '\n'.join(lines)
 
+    def pp(self, indent=0, indent_inc=2, seen=None):
+        raise NotImplementedError("abstract method")
+
+    def concrete_cmp(self, val1, val2):
+        """
+        Return True iff for the two concrete values
+        val1 and val2 and this relation R,
+        'val1 R val2' holds, False otherwise
+
+        Args:
+            val1 (int): left-hand-side concrete value to compare
+            val2 (int): right-hand-side concrete value to compare
+
+        Returns:
+            bool: True if 'val1 R val2', False otherwise
+        """
+        raise NotImplementedError("abstract method")
+
+    def min_margin(self):
+        """
+        Returns the minimum concrete value difference implied by this relation.
+
+        Returns:
+            int: minimum difference between two concrete values for this relation
+        """
+        raise NotImplementedError("abstract method")
+
 class Bigger(Relation):
     def concrete_cmp(self, val1, val2):
         return val1 < val2 # TODO: looks a bit irritating with respect to the class name now
 
+    def min_margin(self):
+        return 1
+
     def pp(self, indent=0, indent_inc=2, seen=None):
         return self.other.pp(indent, indent_inc, '<', seen=seen)
 
 class BiggerOrEqual(Relation):
     def concrete_cmp(self, val1, val2):
         return val1 <= val2
 
+    def min_margin(self):
+        return 0
+
     def pp(self, indent=0, indent_inc=2, seen=None):
         return self.other.pp(indent, indent_inc, '<=', seen=seen)

rpython/jit/metainterp/optimizeopt/test/test_intrelational.py

@@ -1,6 +1,6 @@
 import pytest
 from rpython.jit.metainterp.optimizeopt.intrelational import IntOrderInfo
-from rpython.jit.metainterp.optimizeopt.intutils import IntBound
+from rpython.jit.metainterp.optimizeopt.intutils import IntBound, MININT, MAXINT
 from rpython.jit.metainterp.optimize import InvalidLoop
 from rpython.jit.metainterp.optimizeopt.test.test_intbound import knownbits_and_bound_with_contained_number, ints
 
@@ -147,6 +147,51 @@ def test_make_le_then_make_lt():
     assert a.known_lt(b)
     assert len(a.relations) == 1
 
+def test_known_lt_takes_all_paths_into_account():
+    import itertools
+    for indexes in itertools.permutations([(0, 1, 'le'), (1, 2, 'le'), (0, 2, 'lt')], 3):
+        a = IntOrderInfo()
+        b = IntOrderInfo()
+        c = IntOrderInfo()
+        l = [a, b, c]
+        for i1, i2, kind in indexes:
+            if kind == 'le':
+                l[i1].make_le(l[i2])
+            else:
+                l[i1].make_lt(l[i2])
+        assert a.known_le(b)
+        assert b.known_le(c)
+        assert a.known_lt(c)
+
+def test_known_lt_takes_all_paths_into_account_diamond():
+    import itertools
+    #      a0
+    # <= /   \ <
+    #   b1    c2
+    # <= \   / <=
+    #      d3
+    for indexes in itertools.permutations([(0, 1, 'le'), (0, 2, 'lt'), (1, 3, 'le'), (2, 3, 'le')], 4):
+        a = IntOrderInfo()
+        b = IntOrderInfo()
+        c = IntOrderInfo()
+        d = IntOrderInfo()
+        l = [a, b, c, d]
+        for i1, i2, kind in indexes:
+            if kind == 'le':
+                l[i1].make_le(l[i2])
+            else:
+                l[i1].make_lt(l[i2])
+
+        assert a.known_lt(d)
+
+def test_known_lt_bug():
+    r1 = IntOrderInfo(IntBound(MININT, -1))
+    r2 = IntOrderInfo(IntBound(MININT, -1))
+    r1.make_le(r2)
+    r3 = IntOrderInfo(IntBound(MININT + 1, MAXINT))
+    r1.make_lt(r3)
+    assert not r1._known_lt(r2)
+
 @given(order_info_and_contained_number2)
 def test_known_any_random(args):
     ((r1, n1), (r2, n2)) = args
@@ -458,6 +503,33 @@ def make_le(self, a, b):
         if na <= nb:
             a.make_le(b)
 
+    @rule(a=orderinfos, b=orderinfos, target=orderinfos)
+    def add(self, a, b):
+        na = self.abstract_to_contrete[a]
+        nb = self.abstract_to_contrete[b]
+        c = a.abstract_add(b)
+        nc = intmask(na + nb)
+        self.abstract_to_contrete[c] = nc
+        return c
+
+    @rule(a=orderinfos, b=orderinfos, target=orderinfos)
+    def sub(self, a, b):
+        na = self.abstract_to_contrete[a]
+        nb = self.abstract_to_contrete[b]
+        c = a.abstract_sub(b)
+        nc = intmask(na - nb)
+        self.abstract_to_contrete[c] = nc
+        return c
+
+    @rule(a=orderinfos, b=orderinfos, target=orderinfos)
+    def mul(self, a, b):
+        na = self.abstract_to_contrete[a]
+        nb = self.abstract_to_contrete[b]
+        c = a.abstract_mul(b)
+        nc = intmask(na * nb)
+        self.abstract_to_contrete[c] = nc
+        return c
+
     @rule(a=orderinfos)
     def check_contains(self, a):
         assert a.contains(self.abstract_to_contrete)