ConstantRange::multiply sometimes computes a set which does not include some possible values. Here are some klee generated test cases: ERROR: Found invalid values! A = 1 is in LHS = [1, 0), and B = 0 is in RHS = [0, 2), but A mul B = 0 is not in (LHS mul RHS) = [0, 0) ERROR: Found invalid values! A = 1 is in LHS = [0, 2), and B = 1 is in RHS = [1, 0), but A mul B = 1 is not in (LHS mul RHS) = [0, 0) ERROR: Found invalid values! A = 2 is in LHS = [1, 6), and B = 7 is in RHS = [6, 2), but A mul B = 14 is not in (LHS mul RHS) = [6, 6) ERROR: Found invalid values! A = 1 is in LHS = [1, 6), and B = 7 is in RHS = [6, 2), but A mul B = 7 is not in (LHS mul RHS) = [6, 6) ERROR: Found invalid values! A = 10 is in LHS = [6, 14), and B = 11 is in RHS = [11, 6), but A mul B = 14 is not in (LHS mul RHS) = [2, 2) ERROR: Found invalid values! A = 2 is in LHS = [2, 8), and B = 4 is in RHS = [4, 2), but A mul B = 8 is not in (LHS mul RHS) = [8, 8) ERROR: Found invalid values! A = 3 is in LHS = [1, 0), and B = 3 is in RHS = [2, 0), but A mul B = 9 is not in (LHS mul RHS) = [2, 2)
I added a fast fix in r75444 which should prevent the below cases, but won't provide minimal answers in a whole ton of cases that it ought to. Multiply needs to be rethought...
unionWith has some problems; they all take the form that the upper limit is a feasible value: -- ERROR: Found invalid values! A = 1 is in LHS = [14, 1) or A = 1 is in RHS = [0, 8), but A is not in (LHS union RHS) = [8, 1) ERROR: Found invalid values! A = 3 is in LHS = [2, 10) or A = 3 is in RHS = [10, 1), but A is not in (LHS union RHS) = [10, 1) ERROR: Found invalid values! A = 1 is in LHS = [0, 2) or A = 1 is in RHS = [3, 0), but A is not in (LHS union RHS) = [2, 0) ERROR: Found invalid values! A = 2 is in LHS = [2, 6) or A = 2 is in RHS = [6, 0), but A is not in (LHS union RHS) = [6, 0) ERROR: Found invalid values! A = 0 is in LHS = [0, 4) or A = 0 is in RHS = [6, 0), but A is not in (LHS union RHS) = [4, 0) ERROR: Found invalid values! A = 3 is in LHS = [2, 7) or A = 3 is in RHS = [15, 1), but A is not in (LHS union RHS) = [15, 3) --
Nevermind, they don't all take that form, I looked too quickly.
intersectWith has problems, we should probably remove it and use maximalIntersectWith. Test cases: -- ERROR: Found invalid values! A = 4 is in LHS = [4, 2) and in RHS = [6, 5), but A is not in (LHS intersect RHS) = [6, 2) ERROR: Found invalid values! A = 4 is in LHS = [4, 2) and in RHS = [6, 5), but A is not in (LHS intersect RHS) = [6, 2) ERROR: Found invalid values! A = 10 is in LHS = [8, 5) and in RHS = [12, 11), but A is not in (LHS intersect RHS) = [12, 5) ERROR: Found invalid values! A = 4 is in LHS = [4, 2) and in RHS = [6, 5), but A is not in (LHS intersect RHS) = [6, 2) ERROR: Found invalid values! A = 5 is in LHS = [7, 6) and in RHS = [4, 3), but A is not in (LHS intersect RHS) = [7, 3) ERROR: Found invalid values! A = 4 is in LHS = [7, 5) and in RHS = [4, 0), but A is not in (LHS intersect RHS) = [7, 0) ERROR: Found invalid values! A = 5 is in LHS = [7, 6) and in RHS = [4, 3), but A is not in (LHS intersect RHS) = [7, 3) ERROR: Found invalid values! A = 5 is in LHS = [7, 6) and in RHS = [4, 3), but A is not in (LHS intersect RHS) = [7, 3) ERROR: Found invalid values! A = 4 is in LHS = [7, 5) and in RHS = [4, 0), but A is not in (LHS intersect RHS) = [7, 0) ERROR: Found invalid values! A = 4 is in LHS = [7, 5) and in RHS = [4, 0), but A is not in (LHS intersect RHS) = [7, 0) -- Keep in mind all examples are computed with 4 bits.
Here is a signExtend failure: -- ERROR: Found invalid values! A = 7 is in LHS = [15, 15), and A.sext(26) = 7 is not in LHS.signExtend(26) = [67108856, 7) --
And two sgt errors: -- ERROR: Found invalid values! A = 7 and LHS = [7, 0), but A sgt (LHS.getSignedMax() = 15) ERROR: Found invalid values! A = 7 and LHS = [7, 6), but A sgt (LHS.getSignedMax() = 5) --
Created attachment 3189 [details] klee driver for testing ConstantRange
This has been fixed somewhere along the way. I can confirm that it I can reproduce it with the version before r75444, but with the current release (LLVM 10.0) it is not reproducible (all tests pass, including the attached test case).