Add CBMC Response parsing and Display controlled output by jaisnan · Pull Request #665 · model-checking/kani

jaisnan · 2021-11-23T16:03:07Z

Description of changes:

The Old Output from rmc had non user friendly elements including -

Confusing output messages - See Can we remove "assertion failed" from successful assertions? #189
Uncontrolled output from CBMC
Visually unappealing

To solve all the above issues and to setup future features, the CBMC Parser can now -

Process the response blob that is thrown out by CBMC
Store it in temporary files for easy reading.
Restructure the blob to make it easily parseable
Display a controlled output depending on user inputted flags.

The flag --output-format provides the following options [old | terse| regular] and can be passed as following -

rmc test.rs --output-format regular

This is how the previous output from rmc looks like -

This is how the controlled output looks like -

This change also comes with a pipeline to easily add more styles of output in the future per user requirements and flag based inputs. One such option already provided is the '--terse' flag that displays a summarized output with error messages.

Since final output displays are subject to a lot of user experience feedback, the parser seperates out functionality from the result and can be easily changed to match customer tastes.

Call-outs:

Integrating CBMC Viewer into the parser
Introduce three new formats of output via optional flags including report, log format, machine readable format
Handle non Json CBMC outputs with viewer
Test suite for the parser and Data Classes for each output format.

Testing:

How is this change tested?
Tested using regression tests, all but "Expected" suite passes tests with new output, but it still needs it's own testing suite which is in development.
Is this a refactor change?
Refactor and UX/UI 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.

…output, providing flags "--terse" and "oldOutput" for alternate output styles.

This reverts commit 71b1701.

… incorrect Error Handling

scripts/rmc

celinval

Here are a few comments.. I'll keep reviewing the other files.

scripts/cbmc_json_parser.py

scripts/temp_json/.gitignore

scripts/rmc_flags.py

scripts/rmc.py

scripts/rmc

scripts/rmc_flags.py

scripts/rmc-regression.sh

…esolve autopep8 issues

scripts/rmc_flags.py

scripts/rmc

scripts/cbmc_json_parser.py

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

…Ubuntu, Removing Explcit output-format flag passing for DynTrait Rust tests

…Ubuntu, Removing Explcit output-format flag passing for DynTrait Rust tests w/fixed formatting issues

scripts/cbmc_json_parser.py

…ation for Functions

tedinski

The comments I have are about... comments. So I think this can be merged. Hopefully after those quick fixes. @celinval do you have any further comments?

scripts/cbmc_json_parser.py

celinval · 2021-12-10T00:14:27Z

The comments I have are about... comments. So I think this can be merged. Hopefully after those quick fixes. @celinval do you have any further comments?

I haven't done a last pass, but I think your review should be enough and I don't want to delay this any longer. Thanks for checking!

…ng#665) * Changing default output to Controlled Output after Parsing from CBMC output, providing flags "--terse" and "oldOutput" for alternate output styles. * Fix Magic Strings by Providing Enum; Provide Single flag Option and resolve autopep8 issues

* Changing default output to Controlled Output after Parsing from CBMC output, providing flags "--terse" and "oldOutput" for alternate output styles. * Fix Magic Strings by Providing Enum; Provide Single flag Option and resolve autopep8 issues

jaisnan added 5 commits October 18, 2021 18:15

fixes the "assertion failed" line

71b1701

Merge remote-tracking branch 'fork/main' into main

bc1edfa

Changing default output to Controlled Output after Parsing from CBMC …

c124eb8

…output, providing flags "--terse" and "oldOutput" for alternate output styles.

Revert "fixes the "assertion failed" line"

f0f221e

This reverts commit 71b1701.

Adding temp_dictionary for storing intermediate json files and Fixing…

b46ac2f

… incorrect Error Handling

jaisnan commented Nov 23, 2021

View reviewed changes

scripts/rmc Show resolved Hide resolved

jaisnan added 2 commits November 29, 2021 16:43

Passing all regression tests with old output as default

cb7ebd3

Fixed macOS colorama ModuleNotFoundError in regression test

da99f3d

celinval suggested changes Nov 29, 2021

View reviewed changes

celinval reviewed Nov 29, 2021

View reviewed changes

jaisnan and others added 7 commits November 29, 2021 19:35

Fix autopep8 issues

ae19179

Fix Magic Strings by Providing Enum; Provide Single flag Option and r…

7e6555e

…esolve autopep8 issues

Addressing Code Review Suggestions

c8a7e3e

Merge branch 'model-checking:main' into main

1f69d1f

Merge branch 'code-review-nov-30' into main

f3f42d1

fixing autopep8 issues

f4ab857

Changed Non CBMC Json Handling to raise Exception

dd01733

zhassan-aws reviewed Dec 3, 2021

View reviewed changes

jaisnan and others added 10 commits December 2, 2021 19:06

Update scripts/rmc_flags.py

026a1e7

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Update scripts/rmc

015ee73

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Update scripts/cbmc_json_parser.py

89f59d3

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Update scripts/cbmc_json_parser.py

5b046a2

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Update scripts/cbmc_json_parser.py

93ca4c1

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Update scripts/cbmc_json_parser.py

205c678

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

cleaning up dead code and redundant branches

9f68c7c

Merge branch 'main' of https://github.com/jaisnan/rmc into main

7477f22

Adding Citation for EnumAction, Explicit Dependency for Colorama for …

faa32c1

…Ubuntu, Removing Explcit output-format flag passing for DynTrait Rust tests

Adding Citation for EnumAction, Explicit Dependency for Colorama for …

06c259c

…Ubuntu, Removing Explcit output-format flag passing for DynTrait Rust tests w/fixed formatting issues

tedinski reviewed Dec 6, 2021

View reviewed changes

Add Documentation for deleting regression test cache

70bf446

jaisnan and others added 2 commits December 9, 2021 03:18

Simplifying Control Flow by removing JSON Caching and Adding Document…

014ed61

…ation for Functions

Merge branch 'model-checking:main' into main

c2323b9

tedinski approved these changes Dec 9, 2021

View reviewed changes

scripts/cbmc_json_parser.py Outdated Show resolved Hide resolved

scripts/cbmc_json_parser.py Outdated Show resolved Hide resolved

jaisnan marked this pull request as ready for review December 9, 2021 22:05

jaisnan requested a review from a team as a code owner December 9, 2021 22:05

jaisnan added 2 commits December 9, 2021 22:21

Fixing "extract_solver_information" example documentation

8a2e92b

Deleting dead code

8893682

jaisnan requested a review from celinval December 9, 2021 22:26

celinval approved these changes Dec 10, 2021

View reviewed changes

Merge branch 'main' into main

5c9a542

jaisnan merged commit f045d43 into model-checking:main Dec 10, 2021

tedinski mentioned this pull request Dec 13, 2021

Remove "assertion failed" from successful assertions #562

Closed

4 tasks

Conversation

jaisnan commented Nov 23, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Call-outs:

Testing:

Checklist

Uh oh!

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tedinski left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

celinval commented Dec 10, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

jaisnan commented Nov 23, 2021 •

edited

Loading