Fix spurious overflow counter examples. (#558) #647

celinval · 2021-11-15T22:48:14Z

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:

How is this change tested?

I created a bunch of new tests.

Is this a refactor change?

I guess.

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

zhassan-aws · 2021-11-16T21:57:41Z

compiler/cbmc/src/goto_program/expr.rs

@@ -815,7 +815,7 @@ impl Expr {
                    && (lhs.typ.is_pointer() || lhs.typ.is_numeric() || lhs.typ.is_vector())
                    || (lhs.typ.is_pointer() && rhs.typ.is_integer())
            }
-            Plus => {
+            Plus | OverflowMinus | OverflowMult | OverflowPlus => {


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.

The argument types have to remain the same for each operation (i.e., OverflowMinus goes with Minus).

Makes sense. Do you know why the minus has different requirements?

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.

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

Looks great! The new tests are very good!

zhassan-aws · 2021-11-16T22:40:51Z

src/test/rmc/ArithOperators/wrapping.rs

+    let sum1 = a.wrapping_add(b);
+    let sum2 = a.checked_add(b);
+    assert!(sum0 == sum1);
+    assert!(sum1 >= a || sum2.is_none());


Do you want to add sum1 >= b as well?

adpaco-aws

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?

adpaco-aws · 2021-11-16T22:34:20Z

compiler/cbmc/src/goto_program/expr.rs

@@ -815,7 +815,7 @@ impl Expr {
                    && (lhs.typ.is_pointer() || lhs.typ.is_numeric() || lhs.typ.is_vector())
                    || (lhs.typ.is_pointer() && rhs.typ.is_integer())
            }
-            Plus => {
+            Plus | OverflowMinus | OverflowMult | OverflowPlus => {


The argument types have to remain the same for each operation (i.e., OverflowMinus goes with Minus).

compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs

adpaco-aws · 2021-11-16T22:43:51Z

compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs

+        // Intrinsics which encode a simple wrapping arithmetic operation
+        macro_rules! codegen_wrapping_op {
+            ($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b)) }};
+        }


A few lines below there is codegen_intrinsic_binop which does the same thing. Why did you add this?

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?

celinval · 2021-11-16T23:08:33Z

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?

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

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.

tedinski · 2021-11-18T16:35:04Z

Doesn't this mean we no longer spot overflows in unsafe code?

celinval · 2021-11-18T19:38:44Z

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.

celinval · 2021-11-19T06:04:57Z

This should be check_mul

I wonder how this test even passed. o.O

adpaco-aws · 2021-11-19T15:18:08Z

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.

…king#307)

…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.

celinval requested a review from a team as a code owner November 15, 2021 22:48

zhassan-aws reviewed Nov 16, 2021

View reviewed changes

zhassan-aws approved these changes Nov 16, 2021

View reviewed changes

adpaco-aws suggested changes Nov 16, 2021

View reviewed changes

celinval force-pushed the issue-558 branch from 323d76e to 63fa7a5 Compare November 17, 2021 07:34

adpaco-aws reviewed Nov 17, 2021

View reviewed changes

adpaco-aws approved these changes Nov 17, 2021

View reviewed changes

celinval added 4 commits November 22, 2021 14:57

Change overflow check to be generated by rmc (model-checking#558)

9632276

Remove flag from tests that had spurious counter examples (model-chec…

e67f604

…king#307)

Address PR comments

72f317d

Adding new test cases for unsafe operation.

f9dd8d4

celinval force-pushed the issue-558 branch from 7288849 to f9dd8d4 Compare November 22, 2021 22:58

Fix tests after sync with main branch

fb22b61

celinval force-pushed the issue-558 branch from 84486b9 to fb22b61 Compare November 23, 2021 08:15

celinval merged commit b04b7a9 into model-checking:main Nov 23, 2021

celinval deleted the issue-558 branch November 23, 2021 19:18

celinval mentioned this pull request Nov 23, 2021

Tracking issue: Tests with default checks disabled #307

Open

11 tasks

adpaco-aws mentioned this pull request Apr 19, 2022

Intrinsics Audit #727

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix spurious overflow counter examples. (#558) #647

Fix spurious overflow counter examples. (#558) #647

celinval commented Nov 15, 2021 •

edited

Loading

zhassan-aws Nov 16, 2021 •

edited

Loading

adpaco-aws Nov 16, 2021

celinval Nov 16, 2021 •

edited

Loading

adpaco-aws Nov 16, 2021

celinval Nov 17, 2021

zhassan-aws left a comment

zhassan-aws Nov 16, 2021

adpaco-aws left a comment

adpaco-aws Nov 16, 2021

adpaco-aws Nov 16, 2021

celinval Nov 16, 2021

celinval commented Nov 16, 2021

adpaco-aws left a comment

tedinski commented Nov 18, 2021

celinval commented Nov 18, 2021

celinval commented Nov 19, 2021

adpaco-aws commented Nov 19, 2021

Fix spurious overflow counter examples. (#558) #647

Fix spurious overflow counter examples. (#558) #647

Conversation

celinval commented Nov 15, 2021 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

zhassan-aws Nov 16, 2021 • edited Loading

Choose a reason for hiding this comment

adpaco-aws Nov 16, 2021

Choose a reason for hiding this comment

celinval Nov 16, 2021 • edited Loading

Choose a reason for hiding this comment

adpaco-aws Nov 16, 2021

Choose a reason for hiding this comment

celinval Nov 17, 2021

Choose a reason for hiding this comment

zhassan-aws left a comment

Choose a reason for hiding this comment

zhassan-aws Nov 16, 2021

Choose a reason for hiding this comment

adpaco-aws left a comment

Choose a reason for hiding this comment

adpaco-aws Nov 16, 2021

Choose a reason for hiding this comment

adpaco-aws Nov 16, 2021

Choose a reason for hiding this comment

celinval Nov 16, 2021

Choose a reason for hiding this comment

celinval commented Nov 16, 2021

adpaco-aws left a comment

Choose a reason for hiding this comment

tedinski commented Nov 18, 2021

celinval commented Nov 18, 2021

celinval commented Nov 19, 2021

adpaco-aws commented Nov 19, 2021

celinval commented Nov 15, 2021 •

edited

Loading

zhassan-aws Nov 16, 2021 •

edited

Loading

celinval Nov 16, 2021 •

edited

Loading