Override assert macro by zhassan-aws · Pull Request #797 · model-checking/kani

zhassan-aws · 2022-02-04T16:31:15Z

Description of changes:

Override the assert macro via calling a new kani::assert function that is implemented in codegen (via a hook). This gives us control over the implementation of the macro and allows us to inject any additional checks (e.g. reachability).

For assertions with a message, e.g. assert!(a == b, "a and b have the values {} and {}, respectively", a, b), it produces "a and b have the values {} and {}, respectively", a, b instead of the current This is a placeholder message; Kani doesn't support message formatted at runtime.

Resolved issues:

Call-outs:

The handling of assertions with messages results in bypassing some compile-time checks. See #803 for details.

Testing:

How is this change tested? Current regressions
Is this a refactor change? No

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.

celinval · 2022-02-04T22:27:38Z

library/std/src/lib.rs

+        kani::assert($cond, concat!("assertion: ", stringify!($cond)));
+    };
+    ($cond:expr, $($arg:tt)+) => {
+        kani::assert($cond, concat!("assertion: ", stringify!($($arg)+)));


I guess in the future we should ensure that any variable access is valid for message arguments. Can you please add a fixme comment and an issue capturing that?

You mean that the variable implements the Display trait for example?

Yeah, something like that. However, I was just checking, it looks like the message side of the expression only executes if the condition fails. So I don't think it's that important.

I see. In some sense, kani would be more lenient than rustc. For example, for

fn main() { assert!(1 + 1 == 3, "Bad arithmetic: {}", foo); }

rustc reports:

$ rustc no_display.rs error[E0425]: cannot find value `foo` in this scope --> no_display.rs:2:47 | 2 | assert!(1 + 1 == 3, "Bad arithmetic: {}", foo); | ^^^ not found in this scope

whereas with this PR, kani doesn't complain:

$ kani no_display.rs CBMC version 5.48.0 (cbmc-5.48.0) 64-bit x86_64 linux Reading GOTO program from file no_display.goto Generating GOTO Program Adding CPROVER library (x86_64) Removal of function pointers and virtual functions Generic Property Instrumentation Running with 16 object bits, 48 offset bits (user-specified) Starting Bounded Model Checking Runtime Symex: 0.00102581s size of program expression: 75 steps simple slicing removed 3 assignments Generated 3 VCC(s), 1 remaining after simplification Runtime Postprocess Equation: 7.25e-06s Passing problem to propositional reduction converting SSA Runtime Convert SSA: 0.000213004s Running propositional reduction Post-processing Runtime Post-process: 2.594e-05s Solving with MiniSAT 2.2.1 with simplifier 100 variables, 33 clauses SAT checker: instance is SATISFIABLE Runtime Solver: 9.1981e-05s Runtime decision procedure: 0.000343287s ** Results: [assertion.1] Code generation sanity check: Correct CBMC vtable size for StructTag("tag-_4317141983261250885") (MIR type Closure(DefId(2:9147 ~ std[2f3c]::rt::lang_start::{closure#0}), [(), i8, extern "rust-call" fn(()) -> i32, (fn(),)])). Please report failures: https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS [pointer_primitives.1] dead object in OBJECT_SIZE(&temp_0): SUCCESS /home/ubuntu/examples/no_display.rs function main [main.assertion.1] line 2 assertion: "Bad arithmetic: {}", foo: FAILURE ** 1 of 3 failed (2 iterations) VERIFICATION FAILED

I'll file an issue and add a comment.

celinval · 2022-02-04T22:35:40Z

src/kani-compiler/rustc_codegen_kani/src/overrides/hooks.rs

+            vec![
+                Stmt::decl(tmp.clone(), Some(cond), loc.clone()),
+                Stmt::assert(tmp.clone(), &msg, caller_loc.clone()),
+                Stmt::assume(tmp, loc.clone()),


I'm assuming the assumption here is to abort when the assertion fails, right?

Yes, this is to maintain the current semantics of assert, which are currently roughly implemented as:

if !cond { assert(false); abort(); } // cond must be true here

Can you use the original method codegen_fatal_error() instead?

As far as I understand, codegen_fatal_error is meant for a panic statement, which unconditionally fails, whereas here, there is a condition involved.

The alternative I was considering is to do something similar to how rustc expands the assert macro, e.g.

cond.not().if_then_else(codegen_fatal_error(...), None)

However, based on @danielsn's feedback, with an "if", we lose the structure of the original assert.

Gotcha. I was just hoping that we could encapsulate and formalized what an assert in the rust / kani world means, which is different from the goto-c semantics. But we can do that in a follow up PR.

Maybe we can do that when we fix codegen TerminatorKind::Assert().

celinval · 2022-02-04T22:41:59Z

library/std/src/lib.rs

+/// assert!(a + b == c, "The sum of {} and {} is {}", a, b, c);
+/// ```
+/// the assert message will be:
+/// assertion "The sum of {} and {} is {}", 1, 1, 2


Why not keep it compatible with the std message?

You mean remove the assertion: prefix? If so, the reason I added this prefix is to make it easy to match a reachability check with its assert. If not, can you clarify what you mean?

The std library adds "assertion failed:" prefix to things that don't have a message. So I was wondering if we should match that.

Not sure I understand how you are planning to match the check with its assert though.

Makes sense. The matching should be doable without the assertion: prefix. I'll remove it.

celinval · 2022-02-04T22:43:52Z

src/kani-compiler/rustc_codegen_kani/src/overrides/hooks.rs

+        let msg = fargs.remove(0);
+        let msg = utils::extract_const_message(&msg).unwrap();
+        let target = target.unwrap();
+        let loc = tcx.codegen_span_option(span);


Have you checked how the trace looks like in viewer? I'm wondering if this will look weird since we are using two different locations.

The trace does look a bit weird in viewer (notice the missing files/lines):

Step 38: Function foo, File reach.rs, Line 4 assert!(x < 4); var_5 = FALSE Step 39: Function MISSING, File MISSING, Line 0 temp_0 = FALSE Step 40: Function MISSING, File MISSING, Line 0 temp_0 = FALSE Step 41: Function foo, File reach.rs, Line 4 assert!(x < 4); failure: foo.assertion.1: assertion: x < 4

I'll see if changing all the locations to the "caller" location fixes it.

Cool. BTW, the MISSING is a different problem. We should chat with @markrtuttle about this. Viewer doesn't seem to handle files that are not inside the current folder.

…ro skips some compile checks

zhassan-aws requested a review from a team as a code owner February 4, 2022 16:31

celinval reviewed Feb 4, 2022

View reviewed changes

zhassan-aws added 2 commits February 7, 2022 10:59

Override the assert macro through a kani hook

9ae4c87

Updated regressions

7671f08

zhassan-aws force-pushed the override-assert branch 2 times, most recently from db21be9 to f7e360c Compare February 7, 2022 21:01

Aligned message for assert macro with that of std

97ae95e

zhassan-aws force-pushed the override-assert branch from f7e360c to 97ae95e Compare February 7, 2022 21:04

zhassan-aws mentioned this pull request Feb 7, 2022

Kani's assert macro implementation bypasses some compile-time checks #803

Closed

zhassan-aws added 2 commits February 7, 2022 13:22

Added a comment that clarifies that the second form of the assert mac…

74514ad

…ro skips some compile checks

Use assert location for all modeling code generated

10968f5

celinval approved these changes Feb 7, 2022

View reviewed changes

zhassan-aws merged commit ade82fd into model-checking:main Feb 8, 2022

zhassan-aws deleted the override-assert branch February 8, 2022 00:10

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022

Override assert macro (model-checking#797)

386e7b5

tedinski pushed a commit that referenced this pull request Apr 27, 2022

Override assert macro (#797)

7b8dda2

Conversation

zhassan-aws commented Feb 4, 2022 • 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!

zhassan-aws Feb 7, 2022 • 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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

zhassan-aws commented Feb 4, 2022 •

edited

Loading

zhassan-aws Feb 7, 2022 •

edited

Loading