b2/: simplified and corrected logic behind relop_redundant

We now generate the operator map algorithmically, which is a bit less
classy than solving the logical equations, but easier to get right.

Also renamed the somewhat vague "redundant" to "unreachable".

b2/Makefile

@@ -79,11 +79,17 @@ y.tab.o:	y.tab.c
 		$(CC) -c $(CFLAGS) $*.c -o $*.o
 		$(call MKDEP, $*)
 
+relop.o:	unreachable.inc
+
+unreachable.inc: genredmap.pl
+		$(GEN) ./$< 0 >$@ || { rm -f $@; exit 1; }
+
 -include $(OBJS:.o=.d)
 
 clean:
 		rm -f $(OBJS) $(OBJS:.o=.d)
 		rm -f lex.yy.c y.tab.c y.tab.h y.output
+		rm -f redmap.inc
 
 spotless:	clean
 		rm -f boom

b2/chr.c

@@ -83,12 +83,12 @@ static int comp(const void *a, enum relop op, const void *b, const void *user)
 }
 
 
-static void check_redundant(const struct field *f,
+static void check_unreachable(const struct field *f,
     const struct condition *c1, const struct condition *c2)
 {
-	if (relop_implies(c1->relop, c2->relop, &c1->value, &c2->value,
+	if (relop_unreachable(c1->relop, c2->relop, &c1->value, &c2->value,
 	    comp, f->fmt))
-		yywarn("redundant condition");
+		yywarn("unreachable condition");
 }
 
 
@@ -107,10 +107,10 @@ void field_finalize(struct field *field)
 	for (sel = field->sel; sel; sel = sel->next)
 		for (cond = sel->cond; cond; cond = cond->next) {
 			for (c2 = cond->next; c2; c2 = c2->next)
-				check_redundant(field, cond, c2);
+				check_unreachable(field, cond, c2);
 			for (s2 = sel->next; s2; s2 = s2->next)
 				for (c2 = s2->cond; c2; c2 = c2->next)
-					check_redundant(field, cond, c2);
+					check_unreachable(field, cond, c2);
 		}
 }
 

b2/genredmap.pl

@@ -0,0 +1,71 @@
+#!/usr/bin/perl
+#
+# genredmap.pl - Redundacy detector map generator
+#
+# Copyright 2012 by Werner Almesberger
+#
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+
+#
+# This script finds the relational operators op = f(opa, opb), for which
+# the following is true:
+# 
+# forall A, B: (A op B) -> forall X: !(X opa A) -> !(X opa B)
+#
+# In other words: if, with X a variable and A and B constants, we have a
+# cascade of the form
+#
+# if (X opa A) ...;
+# else if (X opa B) ...;
+#
+# and A op B is true, then the second branch will never be taken.
+#
+
+%op = (
+	"lt"	=> sub { $_[0] < $_[1] },
+	"le"	=> sub { $_[0] <= $_[1] },
+	"eq"	=> sub { $_[0] == $_[1] },
+	"ge"	=> sub { $_[0] >= $_[1] },
+	"gt"	=> sub { $_[0] > $_[1] },
+	
+);
+
+@ops = ("lt", "le", "eq", "ge", "gt");
+
+$always = 0;
+
+$a = 2;
+@v = (0, 1, 2, 3, 4);
+
+for $opa (@ops) {
+#next unless $opa eq "lt";
+	for $opb (@ops) {
+#next unless $opb eq "lt";
+		$best = 0;
+		OP: for $op (@ops) {
+			$hit = 0;
+			for $b (@v) {
+#print "($opa, $opb) $a $op $b\n";
+				next unless $op{$op}->($a, $b);
+				for $x (@v) {
+#print "  A: $x $opa $a\n";
+					next if $op{$opa}->($x, $a);
+#print "    B: $x $opb $b\n";
+					next OP
+					    if $op{$opb}->($x, $b) != $always;
+					$hit++;
+#print "    HIT ($hit)\n";
+				}
+			}
+			if ($hit > $best) {
+				$best = $hit;
+				$best_op = $op;
+			}
+		}
+		print "\t[idx_$opa][idx_$opb] = rel_$best_op,\n" if $best;
+	}
+}

b2/relop.c

@@ -19,33 +19,16 @@
 /*
  * Operator to use for
  *
- * forall X: (A op B) == ((X opa A) -> (X opb B))
+ * (A op B) -> forall X: !(X opa A) -> !(X opb B))
  *
- * For unlimited sets of values:
+ * This is for unlimited sets of values. For limited sets of values, we could
- *
+ * decide also in some edge cases, but let's save such sophistication for
- * opa ->  <   <=  ==  >=  >
+ * later.
- * opb 
- *  <      >=  >=  0   0   0
- *  <=     >   >=  0   0   0
- *  ==     >   >=  ==  <=  <
- *  >=     0   0   0   <=  <
- *  >      0   0   0   <=  <=
- *
- * For limited sets of values, we could decide also in some edge cases,
- * but let's save such sophistication for later.
  */
 
 
-static const enum relop implies_op[idx_n][idx_n] = {
+static const enum relop unreachable_op[idx_n][idx_n] = {
-	[idx_lt][idx_lt] = rel_ge,
+#include "unreachable.inc"
-	[idx_lt][idx_le] = rel_ge,
-
-	[idx_le][idx_lt] = rel_gt,
-	[idx_le][idx_le] = rel_ge,
-
-	[idx_eq][idx_lt] = rel_gt,
-	[idx_eq][idx_le] = rel_ge,
-	[idx_eq][idx_eq] = rel_eq,
 };
 
 
@@ -68,23 +51,13 @@ static int relop2index(enum relop op)
 }
 
 
-static enum relop swap_op(enum relop op)
+int relop_unreachable(enum relop opa, enum relop opb,
-{
+    const void *a, const void *b,
-	return idx_n-1-relop2index(op);
-}
-
-
-int relop_implies(enum relop opa, enum relop opb, const void *a, const void *b,
     int (*cmp)(const void *a, enum relop op, const void *b, const void *user),
     const void *user)
 {
-	if (opa <= opb)
+	return cmp(a,
-		return cmp(a,
+	    unreachable_op[relop2index(opa)][relop2index(opb)], b, user);
-		    implies_op[relop2index(opa)][relop2index(opb)], b, user);
-	else
-		return cmp(b,
-		    swap_op(implies_op[relop2index(opb)][relop2index(opa)]),
-		    a, user);
 }
 
 

b2/relop.h

@@ -35,10 +35,11 @@ enum relop {
 
 
 /*
- * relop_implies checks whether, for all X: (X opb A) -> (X opa B)
+ * relop_unreachable checks whether, for all X: !(X opb A) -> !(X opa B)
  */
 
-int relop_implies(enum relop opa, enum relop opb, const void *a, const void *b,
+int relop_unreachable(enum relop opa, enum relop opb,
+    const void *a, const void *b,
     int (*cmp)(const void *a, enum relop op, const void *b, const void *user),
     const void *user);
 void dump_relop(FILE *file, enum relop op);

b2/test/hierrul

@@ -69,7 +69,7 @@ p = <predation> {
 EOF
 
 expect <<EOF
-h:6: warning: redundant condition
+h:6: warning: unreachable condition
 p=<predation> {
     mouse: { X=* }
     cat: { Y=* }