Replace CProver_Assert with Assert Statment; Adds Property Class by jaisnan · Pull Request #1002 · model-checking/kani

jaisnan · 2022-03-31T16:42:47Z

Description of changes:

Replaces old CProver_assert function calls with Assert Statements.
Adds new Location variant for cases where no location is detailed but property class is needed (subject to review).
Replaces assert_false function body with new assert_statement

Resolved issues:

Resolves #907

Call-outs:

This change potentially has far reaching consequences for the UI and could have some unintended consequences. Existing tests don't quite cover it.

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.

cprover_bindings/src/goto_program/stmt.rs

src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

src/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

tests/ui/Property-Class-UI/exact_div/expected

cprover_bindings/src/goto_program/location.rs

src/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

celinval · 2022-03-31T22:53:09Z

cprover_bindings/src/goto_program/stmt.rs

-                Stmt::assert(expect_true.clone(), &assert_msg, loc.clone()),
+                Stmt::assert_statement(
+                    expect_true.clone(),
+                    "sanity_check",


Is this meant to be hard-coded?

I couldn't come up with a better solution tbh. Open to suggestions about how to address property_class values in cprover_bindings. Maybe I can use the PropertyClass Enum values from codegen here?

No worries... I think we discussed that before, didn't we? Sorry

We agreed to separate the enum from cprover_bindings and place it in codegen, but beyond that i dont think we discussed about calling the enum from codegen again in cprover_bindings. I can do that but i feel like it would remove the seperation of logic, which is why i just hardcoded the string.

open to any suggestions regarding this.

danielsn · 2022-04-01T13:17:16Z

src/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

+    AssertFalse,
+    Assume,
    DefaultAssertion,
+    CustomProperty(String),


Should this be InternedString

i think so, will change it to use that.

Forgot to update this but we don't use InternedString on the codegen side of things so I just left it as String for now.

…nto Jaisnan-Issue-907

…isnan-Issue-907

…nto Jaisnan-Issue-907

zhassan-aws

A couple of minor comments, but overall looks good!

We probably need to classify some of the checks using their own property class, e.g. non-null virtual function, unreachable code, etc., but we can do that in later PRs.

cprover_bindings/src/goto_program/location.rs

src/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

…nto Jaisnan-Issue-907

…el-checking#1002) * Replace cprover_Asserts * Add Tests for Property Classes

* Replace cprover_Asserts * Add Tests for Property Classes

jaisnan added 5 commits March 31, 2022 16:15

Add comments and fix redundant code

de14edc

merge-1

6bdafa1

Replace cprover_Asserts-2

1ab7fc3

Fixed regression tests

dcd1530

Fix Warnings

3b81fa2

jaisnan requested a review from a team as a code owner March 31, 2022 16:42

jaisnan and others added 3 commits March 31, 2022 17:35

Clean up comments

ad8d089

Add Tests for Property Classes

b2083f3

Merge branch 'main' into Jaisnan-Issue-907

22a3e36

zhassan-aws reviewed Mar 31, 2022

View reviewed changes

celinval reviewed Mar 31, 2022

View reviewed changes

danielsn reviewed Apr 1, 2022

View reviewed changes

jaisnan and others added 8 commits April 4, 2022 22:09

Address PR comments

3ce1e4d

Merge branch 'Jaisnan-Issue-907' of https://github.com/jaisnan/kani i…

742704a

…nto Jaisnan-Issue-907

Merge branch 'main' of https://github.com/model-checking/kani into Ja…

0c81a20

…isnan-Issue-907

fix regression test

00d06fc

fix check regression errors

46a412f

Merge branch 'main' into Jaisnan-Issue-907

77f0554

change expected file for regression

04ba304

Merge branch 'Jaisnan-Issue-907' of https://github.com/jaisnan/kani i…

eae5666

…nto Jaisnan-Issue-907

jaisnan requested a review from zhassan-aws April 5, 2022 15:00

jaisnan and others added 9 commits April 5, 2022 11:00

Merge branch 'main' into Jaisnan-Issue-907

db8002c

Merge branch 'main' into Jaisnan-Issue-907

84074d8

Update NoneProperty to PropertyUnknownLocation

3caad10

Merge branch 'main' into Jaisnan-Issue-907

1bc3873

Merge branch 'main' into Jaisnan-Issue-907

70fa56c

update expected

056b226

Merge branch 'Jaisnan-Issue-907' of https://github.com/jaisnan/kani i…

13f330c

…nto Jaisnan-Issue-907

Merge branch 'main' into Jaisnan-Issue-907

a8e7c5f

Merge branch 'main' into Jaisnan-Issue-907

6c403b6

zhassan-aws approved these changes Apr 5, 2022

View reviewed changes

cprover_bindings/src/goto_program/location.rs Outdated Show resolved Hide resolved

src/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs Outdated Show resolved Hide resolved

src/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs Outdated Show resolved Hide resolved

jaisnan added 3 commits April 6, 2022 02:19

Addressing CR suggestions

c698933

Merge branch 'Jaisnan-Issue-907' of https://github.com/jaisnan/kani i…

eb7d6f2

…nto Jaisnan-Issue-907

Update comment

c90af04

jaisnan merged commit e86cb64 into model-checking:main Apr 6, 2022

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

Replace CProver_Assert with Assert Statment; Adds Property Class (mod…

76c3ea8

…el-checking#1002) * Replace cprover_Asserts * Add Tests for Property Classes

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

Replace CProver_Assert with Assert Statment; Adds Property Class (#1002)

670742e

* Replace cprover_Asserts * Add Tests for Property Classes

Conversation

jaisnan commented Mar 31, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Resolved issues:

Call-outs:

Checklist

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

celinval Mar 31, 2022

Choose a reason for hiding this comment

Uh oh!

jaisnan Mar 31, 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!

celinval Apr 1, 2022

Choose a reason for hiding this comment

Uh oh!

jaisnan Apr 1, 2022

Choose a reason for hiding this comment

Uh oh!

danielsn Apr 1, 2022

Choose a reason for hiding this comment

Uh oh!

jaisnan Apr 1, 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!

jaisnan Apr 5, 2022

Choose a reason for hiding this comment

Uh oh!

zhassan-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

jaisnan commented Mar 31, 2022 •

edited

Loading

jaisnan Mar 31, 2022 •

edited

Loading

jaisnan Apr 1, 2022 •

edited

Loading