qbe

commit 2434d4eb3e039cde972d47923744225e67f98f06
parent 2f41ff03e2c6d1b16e9d4300315ca1c841e3970e
Author: Quentin Carbonneaux <quentin.carbonneaux@yale.edu>
Date:   Mon, 24 Oct 2016 13:46:27 -0400

fix bug in folding of w comparisons

The casting to uint32_t made the code for comparing
two signed words invalid.  Interestingly, this can
be fixed by casting to int32_t instead.  Because
sign extension is monotonic, all the unsigned
comparisons remain valid.

CVC4 can even check that for us:

x, y : BITVECTOR(32);
QUERY BVLT(SX(x, 64), SX(y, 64)) <=> BVLT(x, y);
QUERY BVLE(SX(x, 64), SX(y, 64)) <=> BVLE(x, y);
QUERY BVGT(SX(x, 64), SX(y, 64)) <=> BVGT(x, y);
QUERY BVGE(SX(x, 64), SX(y, 64)) <=> BVGE(x, y);

Diffstat:
M
fold.c
 | 
4
++--

1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/fold.c b/fold.c
@@ -385,8 +385,8 @@ foldint(Con *res, int op, int w, Con *cl, Con *cr)
 	default:
 		if (Ocmpw <= op && op <= Ocmpl1) {
 			if (op <= Ocmpw1) {
-				l.u = (uint32_t)l.u;
-				r.u = (uint32_t)r.u;
+				l.u = (int32_t)l.u;
+				r.u = (int32_t)r.u;
 			} else
 				op -= Ocmpl - Ocmpw;
 			switch (op - Ocmpw) {