Fix assert!() and panic!() code generation by celinval · Pull Request #687 · model-checking/kani

celinval · 2021-12-10T00:04:44Z

Description of changes:

I refactored how we codegen panic statements so it now it terminate the program per its spec. I have also removed the hack we had to try to get the assert location.

Since we currently do not support stack unwinding, the panic codegen will always terminate immediately and it will not try to unwind the stack. I added an option to RMC to force the compiler to use abort as the panic strategy and a check to rmc codegen that will fail if the user tries to override that.

Another note is that we currently do not support #[track_caller] and I have not changed that.

This change fixes #67, fixes #466, fixes #543, and fixes #636. This change also mitigates #545.

Resolved issues:

Resolves #67
Resolves #466
Resolves #543
Resolves #636

Call-outs:

I split this into two commits. One with the changes to the compiler and new test cases. The second commit is adjustments to our existing tests.

Testing:

How is this change tested? New and old test cases.
Is this a refactor change? Yes

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.

I refactored how we codegen panic statements so it now it terminate the program per its spec. I have also removed the hack we had to try to get the assert location. Since we currently do not support stack unwinding, the panic codegen will always terminate immediately and it will not try to unwind the stack. I added an option to RMC to force the compiler to use abort as the panic strategy and a check to rmc codegen that will fail if the user tries to override that. Another note is that we currently do not support `#[track_caller]` and I have not changed that. This change fixes #67, fixes model-checking#466, fixes model-checking#543, and fixes model-checking#636. This change also mitigates model-checking#545.

danielsn · 2021-12-10T00:22:55Z

compiler/cbmc/src/goto_program/stmt.rs

        )
    }

+    pub fn assume_false(loc: Location) -> Self {


doc comment

I'm actually removing this since I am adding a builtin abort()

compiler/rustc_codegen_rmc/src/codegen/span.rs

danielsn · 2021-12-10T00:24:37Z

compiler/rustc_codegen_rmc/src/codegen/statement.rs

+                        }
+                    }
+                } else {
+                    tracing::error!(?values, "Oh no");


More informative message please?

ooops... That was a debug statement. =)

I'll remove it!

danielsn · 2021-12-10T00:25:15Z

compiler/rustc_codegen_rmc/src/codegen/statement.rs

+        );
+        if let Some(values) = fargs[0].struct_expr_values() {
+            if !values.is_empty() {
+                if let ExprValue::AddressOf(msg_value) = values[0].value() {


Are there any other times we might want to do this? Could be a utility function?

I don't know. I figured that this code has a lot of assumptions about the format of the input, so I was thinking about leaving here for now and pulled it out if we start seeing this pattern in other places.

I think Jai had a utility function that does this in his first PR (that's still open). Maybe just steal it from there?

danielsn · 2021-12-10T00:25:51Z

compiler/rustc_codegen_rmc/src/codegen/statement.rs

+    pub fn codegen_fatal_error(&self, msg: &str, span: Option<Span>) -> Stmt {
+        let loc = self.codegen_caller_span(&span);
+        Stmt::block(
+            vec![Stmt::assert_false(msg, loc.clone()), Stmt::assume_false(loc.clone())],


should we assume(false) or abort()

That's a good question. What do you think? I can try it out with abort and see how CBMC behaves.

I replaced this by calling abort() instead of assume(false), but I still see this message on CBMC output:

aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 0

So I don't think it will make much difference. I'll use abort() to improve readability.

danielsn · 2021-12-10T00:27:10Z

compiler/rustc_codegen_rmc/src/overrides/hooks.rs

+        Some(def_id) == tcx.lang_items().panic_fn()
+            || Some(def_id) == tcx.lang_items().panic_display()
+            || Some(def_id) == tcx.lang_items().begin_panic_fn()


danielsn · 2021-12-10T00:27:42Z

compiler/rustc_codegen_rmc/src/overrides/hooks.rs

-            loc,
-        )
+        let msg = format!(
+            "a panicking function {} is invoked",


I wonder if we can give a clearer message here

Sure. Can I do it in a follow up PR since this will likely impact a lot of expected tests. I think this PR is already big enough.

danielsn · 2021-12-10T00:30:13Z

src/test/expected/binop/main.rs

@@ -56,19 +56,22 @@ fn ibxor_test(a: i32, b: i32, correct: i32, wrong: i32) {
 }

 fn main() {


IS this to prevent one failure from hiding others?

Yes. Otherwise everything passed after iadd_test() because the checks become unreachable.

danielsn · 2021-12-10T00:30:48Z

src/test/expected/float-nan/main.rs

+    match rmc::nondet::<u8>() {
+        // at this point, f == 0.0
+        // should succeed
+        0 => assert!(1.0 / f != 0.0 / f),
+        // should succeed
+        1 => assert!(!(1.0 / f == 0.0 / f)),
+        // should fail
+        2 => assert!(1.0 / f == 0.0 / f),
+        // should fail
+        3 => assert!(0.0 / f == 0.0 / f),
+        // should suceed
+        _ => assert!(0.0 / f != 0.0 / f),
+    }


would it make sense to have a macro for this pattern

I figured it wasn't worth the effort. There are a few differences in them and a macro would probably make it harder to read.

I wonder if we should have the original, primitive cbmc assert available still.

Then our tests could still be straight-line code, just using rmc::assert() instead of assert!

I was thinking about adding a function rmc::check() that had the behaviour you mentioned. What do you think? I would prefer not having two types of assert.

That said, I would prefer adding it in a different PR.

Also, once we have the #[proof] attribute integrated, we should be able to easily split tests like this into multiple harnesses in the same file.

I'm cool with a different name (brainstorming: rmc::probe? check also seems good) and in a follow up PR.

I created #695 to capture the work.

danielsn · 2021-12-10T00:31:15Z

src/test/rmc/DynTrait/dyn_fn_param_fail.rs


 pub fn unit_to_u32() -> u32 {
-    assert!(false);
+    if rmc::nondet::<bool>() {


do we need the turbofish here

Oh... that's a good point. I guess because it's inside an if, we probably don't. Let me check.

was it necessary?

tedinski · 2021-12-10T21:24:22Z

compiler/rustc_codegen_rmc/src/codegen/statement.rs

+        );
+        if let Some(values) = fargs[0].struct_expr_values() {
+            if !values.is_empty() {
+                if let ExprValue::AddressOf(msg_value) = values[0].value() {


I think Jai had a utility function that does this in his first PR (that's still open). Maybe just steal it from there?

tedinski · 2021-12-10T21:31:02Z

src/test/rmc/Options/check_tests.rs

 // Note: We need to provide the compile-flags because compile test runs rustc directly and via rmc.

-// compile-flags: --test
+// compile-flags: --test --C panic=abort


Is this needed?

Let me double check. I think you are correct though.

was it necessary?

compiler/rustc_codegen_rmc/src/codegen/span.rs

tedinski · 2021-12-10T21:34:27Z

src/test/expected/float-nan/main.rs

+    match rmc::nondet::<u8>() {
+        // at this point, f == 0.0
+        // should succeed
+        0 => assert!(1.0 / f != 0.0 / f),
+        // should succeed
+        1 => assert!(!(1.0 / f == 0.0 / f)),
+        // should fail
+        2 => assert!(1.0 / f == 0.0 / f),
+        // should fail
+        3 => assert!(0.0 / f == 0.0 / f),
+        // should suceed
+        _ => assert!(0.0 / f != 0.0 / f),
+    }


I wonder if we should have the original, primitive cbmc assert available still.

Then our tests could still be straight-line code, just using rmc::assert() instead of assert!

- Use abort instead of assume(false). - Add better method doc. - Create utility function to extract string constant. - Add fixme test and link to issue to add support to stack unwind.

tedinski

I think this is good to merge. I really want rmc::check or whatever we call it, but whenever we get to it I guess. :)

There were two very minor things I didn't see addressed that I added comments to, also.

tedinski · 2021-12-13T23:10:02Z

src/test/rmc/DynTrait/dyn_fn_param_fail.rs


 pub fn unit_to_u32() -> u32 {
-    assert!(false);
+    if rmc::nondet::<bool>() {


was it necessary?

tedinski · 2021-12-13T23:10:10Z

src/test/rmc/Options/check_tests.rs

 // Note: We need to provide the compile-flags because compile test runs rustc directly and via rmc.

-// compile-flags: --test
+// compile-flags: --test --C panic=abort


was it necessary?

celinval · 2021-12-14T19:58:34Z

I think this is good to merge. I really want rmc::check or whatever we call it, but whenever we get to it I guess. :)

There were two very minor things I didn't see addressed that I added comments to, also.

My bad. I had missed them. Thanks for pointing it out.

I refactored how we codegen panic statements so it now it terminate the program per its spec. I have also removed the hack we had to try to get the assert location. Since we currently do not support stack unwinding, the panic codegen will always terminate immediately and it will not try to unwind the stack. I added an option to RMC to force the compiler to use abort as the panic strategy and a check to rmc codegen that will fail if the user tries to override that. Another note is that we currently do not support `#[track_caller]` and I have not changed that. This change fixes model-checking#67, fixes model-checking#466, fixes model-checking#543, and fixes model-checking#636. This change also mitigates model-checking#545.

I refactored how we codegen panic statements so it now it terminate the program per its spec. I have also removed the hack we had to try to get the assert location. Since we currently do not support stack unwinding, the panic codegen will always terminate immediately and it will not try to unwind the stack. I added an option to RMC to force the compiler to use abort as the panic strategy and a check to rmc codegen that will fail if the user tries to override that. Another note is that we currently do not support `#[track_caller]` and I have not changed that. This change fixes #67, fixes #466, fixes #543, and fixes #636. This change also mitigates #545.

celinval added 2 commits December 9, 2021 16:01

Correct tests that dependend on the wrong assert behavior

1822891

celinval requested a review from a team as a code owner December 10, 2021 00:04

danielsn reviewed Dec 10, 2021

View reviewed changes

tedinski reviewed Dec 10, 2021

View reviewed changes

celinval added 2 commits December 10, 2021 16:47

Address PR comments.

8cf30c2

- Use abort instead of assume(false). - Add better method doc. - Create utility function to extract string constant. - Add fixme test and link to issue to add support to stack unwind.

Merge remote-tracking branch 'origin/main' into issue-636

10cf2f1

tedinski approved these changes Dec 13, 2021

View reviewed changes

tedinski mentioned this pull request Dec 13, 2021

Remove "assertion failed" from successful assertions #562

Closed

4 tasks

celinval mentioned this pull request Dec 14, 2021

Add non-fatal failure check to rmc prelude #695

Closed

Cleanup redundant test code per PR feedback

c7d12d2

danielsn approved these changes Dec 14, 2021

View reviewed changes

celinval merged commit 625990c into model-checking:main Dec 14, 2021

celinval deleted the issue-636 branch December 14, 2021 21:04

		@@ -56,19 +56,22 @@ fn ibxor_test(a: i32, b: i32, correct: i32, wrong: i32) {
		}

		fn main() {

Conversation

celinval commented Dec 10, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

celinval Dec 10, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tedinski left a comment

celinval commented Dec 10, 2021 •

edited

Loading

celinval Dec 10, 2021 •

edited

Loading