Fix spurious overflow counter examples. (#558)#647
Fix spurious overflow counter examples. (#558)#647celinval merged 5 commits intomodel-checking:mainfrom
Conversation
There was a problem hiding this comment.
Do the cases here (e.g. LHS is a pointer and RHS is an integer) apply to overflow addition/subtraction/multiplication? EDIT: I see now that some of those cases apply to intrinsics.
There was a problem hiding this comment.
The argument types have to remain the same for each operation (i.e., OverflowMinus goes with Minus).
There was a problem hiding this comment.
Makes sense. Do you know why the minus has different requirements?
There was a problem hiding this comment.
Yes, minus allows both operands to be pointers because it is valid to compute offsets between them. This does not apply to plus because adding two pointers will likely result in another pointer to who-knows-where.
There was a problem hiding this comment.
Ah, I hadn't thought about that. Good point.
I removed the vector from the list since it doesn't look like CBMC overflow operation actually accepts C arrays.While trying to reproduce the issue to file a bug report, I noticed that CBMC was printing the following warning:
warning: ignoring overflow-*
* type: bool
0: array
* type: array
* #source_location: nil
* size: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 2
0: signedbv
* width: 8
0: constant
* type: signedbv
* width: 8
* value: 0
1: constant
* type: signedbv
* width: 8
* value: 0
1: array
* type: array
* #source_location: nil
* size: constant
* type: signedbv
* width: 64
* #c_type: signed_long_int
* value: 2
0: signedbv
* width: 8
0: constant
* type: signedbv
* width: 8
* value: 0
1: constant
* type: signedbv
* width: 8
* value: 0
zhassan-aws
left a comment
There was a problem hiding this comment.
Looks great! The new tests are very good!
There was a problem hiding this comment.
Do you want to add sum1 >= b as well?
adpaco-aws
left a comment
There was a problem hiding this comment.
The changes here heavily rely on -C overflow-checks=on. Can we add a check to our back-end to ensure the flag is always set?
There was a problem hiding this comment.
The argument types have to remain the same for each operation (i.e., OverflowMinus goes with Minus).
There was a problem hiding this comment.
A few lines below there is codegen_intrinsic_binop which does the same thing. Why did you add this?
There was a problem hiding this comment.
I was trying to make it explicit that this is a wrapping operation. To avoid others to inadvertently using the wrong operation in the future.
I could modify this to just call the binop one or remove this. Any preference?
Should we allow users to turn them off though? What if I add a check with a warning if the flag is off? |
adpaco-aws
left a comment
There was a problem hiding this comment.
Looking good! Of course, we can change the check in the near future to support other use cases, but I do not feel comfortable with our codegen depending on this flag and not requiring it.
|
Doesn't this mean we no longer spot overflows in unsafe code? |
That's a great question! I should definitely add test cases for that. We are still checking for overflow in unsafe code. Regular arithmetic operations are always checked no matter where they show up in the code. |
I wonder how this test even passed. o.O |
Probably because CBMC is not finding the function to verify and that is understood as a verification failure. |
…hecking#647) We cannot easily specify which arithmetic operations are wrapping ones to CBMC. Thus, CBMC was generating overflow checks for wrapping operations which were generating spurious failures. This change disables some of those CBMC checks. We replace them by using rustc overflow checks for regular operations and by explicitly adding checks to unchecked operations.
We cannot easily specify which arithmetic operations are wrapping ones to CBMC. Thus, CBMC was generating overflow checks for wrapping operations which were generating spurious failures. This change disables some of those CBMC checks. We replace them by using rustc overflow checks for regular operations and by explicitly adding checks to unchecked operations.
Description of changes:
RMC was treating all arithmetic operations as non-wrapping which was triggering a lot of spurious counter examples. Instead of relying on cbmc generated overflow checks, we are not explicitly encoding checks for non-wrapping operations.
Resolved issues:
Resolves #558
Call-outs:
I created #646 to track implementing more checks that we currently don't support. Except for shift left and division by 0, I believe CBMC doesn't have any mechanism to check them.
Testing:
I created a bunch of new tests.
I guess.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.