A few output improvements #976

celinval · 2022-03-23T22:04:18Z

Description of changes:

Disable reach assertions when running --visualize.
Fix the file path in the compiler to use local file path.
- Note that using the local file path is not recommended to generate artifacts that can be shared, but I don't this we have that use case today.
Try to be smart when displaying the file path to either do relative to current directory or to home.
- This makes the output much nicer when the file path is deep into the hierarchy.

Resolved issues:

Call-outs:

Here is an example of the new output:

Check 16: std::boxed::Box::<T, A>::into_unique.assertion.1                                                                                                                               
         - Status: SUCCESS                                                                                                                                                               
         - Description: "resume instruction"                                                                                                                                             
         - Location: ~/.rustup/toolchains/nightly-2022-03-09-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/boxed.rs:1087:5 in function std::boxed::Box::<T, A>::into_un
ique                                                                                                                                                                                     
                                                                                                                                                                                         
Check 17: same_file.assertion.2                                                                                                                                                          
         - Status: SUCCESS                                                                                                                                                               
         - Description: "assertion failed: cond"                                                             
         - Location: main.rs:13:5 in function same_file

Testing:

How is this change tested?
Is this a refactor change?

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-03-23T22:05:32Z

tests/ui/code-location/expected

@@ -0,0 +1,7 @@
+module/mod.rs:10:5 in function module::not_empty
+main.rs:13:5 in function same_file
+~/.rustup/toolchains


I'm not confident we should include this expectation, but this prevents us from inadvertently use remapped path. Open to suggestions.

RUSTUP_HOME can be overriden (see https://rust-lang.github.io/rustup/environment-variables.html), so in the current form, the test may fail for users who override it.

If you're trying to make sure the path is not of the form: /rustc/1eb72580d076935a3e590deb6e5813a5aef3eca4/library/core/src/mem/mod.rs, perhaps just check for toolchains/nightly-?

jaisnan · 2022-03-23T22:23:17Z

Could you add some screenshot or add an example output improvement to the description of this PR? (Maybe the same example as the test file so it's easier to suggest what to add to the expected file)

zhassan-aws · 2022-03-23T22:26:38Z

src/cargo-kani/src/args.rs

+
+    pub fn assertion_reach_checks(&self) -> bool {
+        // Turn them off when visualizing an error trace.
+        !self.no_assertion_reach_checks && !self.visualize


Thanks. I've been meaning to fix that.

zhassan-aws · 2022-03-24T00:05:58Z

scripts/cbmc_json_parser.py

+        if not self.filename:
+            return None
+
+        if not path.exists(self.filename):


Is this necessary for what comes after? Checking if the file exists can be expensive (since it involves an OS/filesystem operation) which can slow things down quite a bit if we're checking the path for every check.

I thought that this fixed an issue that I saw before, but I couldn't reproduce it. So I'm removing this. :)

I added a few tests to hopefully ensure that I didn't miss anything.

zhassan-aws · 2022-03-24T00:20:26Z

tests/ui/code-location/expected

@@ -0,0 +1,7 @@
+module/mod.rs:10:5 in function module::not_empty
+main.rs:13:5 in function same_file
+~/.rustup/toolchains


RUSTUP_HOME can be overriden (see https://rust-lang.github.io/rustup/environment-variables.html), so in the current form, the test may fail for users who override it.

If you're trying to make sure the path is not of the form: /rustc/1eb72580d076935a3e590deb6e5813a5aef3eca4/library/core/src/mem/mod.rs, perhaps just check for toolchains/nightly-?

Should we make it relative to the project dir instead??

Unfortunately, the output changes depending on the directory where the regression is running from, so we cannot check that logic.

zhassan-aws · 2022-03-28T22:43:24Z

scripts/test_parser.py

@@ -0,0 +1,102 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+import unittest


Much needed! Thanks for adding this unit test module!

Nit: should we renamed it to test_cbmc_parser.py to make it more clear?

* Disable reach assertions in visualize mode * Make file location relative to current dir * Add unit tests

celinval requested a review from a team as a code owner March 23, 2022 22:04

celinval commented Mar 23, 2022

View reviewed changes

zhassan-aws reviewed Mar 24, 2022

View reviewed changes

celinval added 5 commits March 28, 2022 15:04

Disable reach assertions in visualize mode

7bdbba2

Make file location relative to current dir.

5c3a8b4

Should we make it relative to the project dir instead??

Add test for this.

9ab8d90

Unfortunately, the output changes depending on the directory where the regression is running from, so we cannot check that logic.

Fix regression

157695a

Remove check if file exists and added unit tests

25bca14

celinval force-pushed the output-improvements branch from 9607350 to 25bca14 Compare March 28, 2022 22:04

celinval added 2 commits March 28, 2022 15:08

Update expected file

8202aba

Making one test more reliable

0a00fe2

zhassan-aws approved these changes Mar 28, 2022

View reviewed changes

celinval added 2 commits March 28, 2022 15:46

Rename test script

e6c52de

Merge branch 'main' into output-improvements

78b77fd

celinval merged commit 4ad542f into model-checking:main Mar 29, 2022

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

A few output improvements (model-checking#976)

6955c35

* Disable reach assertions in visualize mode * Make file location relative to current dir * Add unit tests

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

A few output improvements (model-checking#976)

ce9ec64

* Disable reach assertions in visualize mode * Make file location relative to current dir * Add unit tests

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

A few output improvements (model-checking#976)

b85c5d8

* Disable reach assertions in visualize mode * Make file location relative to current dir * Add unit tests

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

A few output improvements (#976)

c9abaf8

* Disable reach assertions in visualize mode * Make file location relative to current dir * Add unit tests

celinval mentioned this pull request Sep 29, 2023

Invalid path reported for Rust toolchain #2681

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

A few output improvements #976

A few output improvements #976

celinval commented Mar 23, 2022 •

edited

Loading

celinval Mar 23, 2022

zhassan-aws Mar 24, 2022

jaisnan commented Mar 23, 2022 •

edited

Loading

zhassan-aws Mar 23, 2022

zhassan-aws Mar 24, 2022

celinval Mar 28, 2022

zhassan-aws Mar 24, 2022

zhassan-aws Mar 28, 2022

celinval Mar 28, 2022

A few output improvements #976

A few output improvements #976

Conversation

celinval commented Mar 23, 2022 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jaisnan commented Mar 23, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval commented Mar 23, 2022 •

edited

Loading

jaisnan commented Mar 23, 2022 •

edited

Loading