diff options
| author | Quentin Carbonneaux <quentin.carbonneaux@yale.edu> | 2016-10-24 13:46:27 -0400 |
|---|---|---|
| committer | Quentin Carbonneaux <quentin.carbonneaux@yale.edu> | 2016-10-24 13:46:27 -0400 |
| commit | 2434d4eb3e039cde972d47923744225e67f98f06 (patch) | |
| tree | 6cfb416b54207f4add69e30223ff06c5950ffbdf /fold.c | |
| parent | 2f41ff03e2c6d1b16e9d4300315ca1c841e3970e (diff) | |
| download | roux-2434d4eb3e039cde972d47923744225e67f98f06.tar.gz | |
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 (limited to 'fold.c')
| -rw-r--r-- | fold.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/fold.c b/fold.c index c2a7c12..a000ff4 100644 --- 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) { |