Use 2's complement when computing the relative discriminant to avoid signed to unsigned overflow failures#995
Conversation
…signed to unsigned overflow failures
celinval
left a comment
There was a problem hiding this comment.
Thanks for doing this. Mostly small comments.
| .clone() | ||
| .cast_to(Type::unsigned_int(64)) | ||
| .le(Expr::int_constant(relative_max, Type::unsigned_int(64))) | ||
| .cast_to(Type::unsigned_int(128)) |
There was a problem hiding this comment.
Good point. It is not needed. I removed it and used relative_discr's type for relative_max.
| } else { | ||
| // This should be a wrapping sub. | ||
| niche_val.sub(Expr::int_constant(*niche_start, discr_ty.clone())) | ||
| // Compute "niche_val - niche_start" where "-" is |
There was a problem hiding this comment.
nit: can you move this to a different function to make this more readable
tests/kani/Enum/neg_discriminant.rs
Outdated
| let d = Some(Foo::D); | ||
| let e = Some(Foo::E); | ||
| let f = Some(Foo::F); | ||
| let _ = matches!(a, Some(Foo::A)); |
tests/kani/Enum/neg_discriminant.rs
Outdated
| } | ||
|
|
||
| #[kani::proof] | ||
| fn main() { |
There was a problem hiding this comment.
nit: I think we should stop using main() and add a more descriptive name to the harness now that we run them by default.
There was a problem hiding this comment.
Makes sense. Updated.
tests/kani/LexicographicCmp/main.rs
Outdated
| // This test checks that lexicographic comparison is handled correctly | ||
|
|
||
| #[kani::proof] | ||
| fn main() { |
There was a problem hiding this comment.
verify_lexicographic_comparison
There was a problem hiding this comment.
Done (used check_lexicographic_cmp).
| // } | ||
| let s64 = Type::signed_int(64); | ||
| let niche_val = niche_val.cast_to(s64.clone()); | ||
| let twos_complement: i64 = |
There was a problem hiding this comment.
Thanks for adding a function for a general 2's complement! This one is for a specific width though, so was simple enough.
…signed to unsigned overflow failures (model-checking#995)
…signed to unsigned overflow failures (#995)
Description of changes:
An overflow may occur when casting a signed value to an unsigned one in the computation of an enum discriminant. This overflow is intentional, but gets flagged by CBMC as a failure. This PR works around the issue by using the 2's complement to avoid overflow.
Resolved issues:
Resolves #356
Call-outs:
An alternative approach would be to use CBMC pragmas to turn off signed to unsigned overflow detection during the computation of the relative discriminant. We haven't had much success with the usage of such pragmas in the past though.
Testing:
How is this change tested? Two new tests are added.
Is this a refactor change? No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.