Upgrade to CBMC 5.69.1 (with fixes) #1811

adpaco-aws · 2022-10-27T21:05:40Z

Description of changes:

NOTE: This PR initially upgraded CBMC to v5.68.0, but it was actually upgraded to v5.69.1 as part of the review process. Unfortunately, the commit was added without first editing the title.

Upgrades CBMC to v5.69.1 and changes Kani so that it conforms with the latest changes in CBMC:

Changes the type of Kani-generated CProver primitives to the integer type where appropriate (also adds required support to generate integer ireps). This change was forced by CBMC (see Updating to latest CBMC version requires update to architecture strings #1779)
Redefines C functions with void return types so they use type struct Unit instead. This is necessary because of stricter type-checking in CBMC (likely caused by Fix linking in case of function type conflict diffblue/cbmc#6547)
Always pushes --slice-formula, even in the cases where we didn't (opened Not using --slice-formula causes invariant violation in CBMC #1810 for debugging).
Moves the diamond dependency test into the cargo-kani suite. This was the last test failing, but it run its own compilation process so it was dubious. Moving into cargo-kani showed no issues.

Resolved issues:

Resolves #1779

Testing:

How is this change tested? Existing egression.
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.

Return `VoidUnit` (type `struct Unit`) instead in those functions

cprover_bindings/src/goto_program/typ.rs

tautschnig · 2022-10-27T21:19:18Z

cprover_bindings/src/goto_program/typ.rs

@@ -286,6 +289,7 @@ impl Type {
            CInteger(CIntType::Bool) => Some(mm.bool_width),
            CInteger(CIntType::Char) => Some(mm.char_width),
            CInteger(CIntType::Int) => Some(mm.int_width),
+            Integer => Some(mm.int_width),


This one is unbounded, it doesn’t have a bitwidth.

Done. Thanks!

Actually, do you think we should return None or just Some(x) where x is a large number?

Maybe we can have an "infinite" token? But Some(x) is semantically wrong for all x

danielsn · 2022-10-27T21:17:29Z

cprover_bindings/src/env.rs

@@ -58,7 +65,7 @@ pub fn machine_model_symbols(mm: &MachineModel) -> Vec<Symbol> {
        ),
        int_constant("__CPROVER_architecture_wchar_t_width", mm.wchar_t_width),
        int_constant("__CPROVER_architecture_word_size", mm.word_size),
-        int_constant("__CPROVER_rounding_mode", mm.rounding_mode),
+        int_constant_c_int("__CPROVER_rounding_mode", mm.rounding_mode),


Seriously? There is one remaining outlier? Is there an issue open to CBMC about that?

Couldn't find one, so I opened diffblue/cbmc#7282 (and pasted the issue there)

I'll comment on the CBMC issue, but indeed rounding mode is different.

cprover_bindings/src/goto_program/typ.rs

danielsn · 2022-10-27T21:23:00Z

kani-driver/src/call_cbmc.rs

+        // But for some reason, not pushing it causes a CBMC invariant violation
+        // since version 5.68.0.
+        // <https://github.com/model-checking/kani/issues/1810>
+        args.push("--slice-formula".into());


Does this mess with concrete playback?

Needs more investigation.

My understanding was that using --slice-formula with concrete playback may remove calls to kani::any() from the trace, which doesn't allow us to provide a counter-example (in that case, we just report a test couldn't be generated). But all tests we have for concrete playback and --visualize pass if we use --slice-formula.

danielsn · 2022-10-27T21:25:02Z

library/kani/kani_lib.c

+// Note: the Kani compiler changes `void` return types to the empty tuple `()`
+// AKA `VoidUnit`. Because of that, we need to declare its type `struct Unit`
+// and the extern instance `VoidUnit` here.


I'm not sure this is an accurate description. Rust () is not the same thing as void, and __rust_dealloc is extern Rust not extern C https://stdrs.dev/nightly/x86_64-unknown-linux-gnu/src/alloc/alloc.rs.html#37

OK, I've changed it to the same comment we use in the Kani compiler's typ.rs module:

/// Mapping unit to `void` works for functions with no return type but not for /// variables with type unit. We treat both uniformly by declaring an empty /// struct type: `struct Unit {}` and a global variable `struct Unit VoidUnit` /// returned by all void functions (both declared by the Kani compiler).

tautschnig · 2022-10-28T09:14:17Z

High-level note: you might consider upgrading to 5.69.1 right away, which will be out later on today (diffblue/cbmc#7283).

adpaco-aws · 2022-10-28T14:01:32Z

High-level note: you might consider upgrading to 5.69.1 right away, which will be out later on today (diffblue/cbmc#7283).

Tried now, but brew couldn't find it in CI. I'm rolling back to v5.68.0 for now.

tautschnig · 2022-10-28T20:03:55Z

High-level note: you might consider upgrading to 5.69.1 right away, which will be out later on today (diffblue/cbmc#7283).

Tried now, but brew couldn't find it in CI. I'm rolling back to v5.68.0 for now.

Please retry, should just be a matter of timing.

danielsn · 2022-10-28T20:57:26Z

tests/kani/ForeignItems/lib.c

@@ -48,7 +55,11 @@ struct Foo2 {

 uint32_t S = 12;

-void update_static() { S++; }
+struct Unit update_static()


This is something that ought to work once C-FFI is in place. We should have comments and a tracking ticket explaining that this is a workaround we want to remove

This reverts commit 3007e84.

adpaco-aws requested a review from a team as a code owner October 27, 2022 21:05

adpaco-aws added 7 commits October 27, 2022 21:08

Extend CPROVER API for integer and use in architectures

3d0bb10

Bump up CBMC version to 5.68.0

d0c177f

Use struct Unit instead of void in C functions

f53f57c

Return `VoidUnit` (type `struct Unit`) instead in those functions

Move diamond dependency test into cargo-kani suite

3f0c239

Always use --slice-formula

c94213a

Undo change in comment for transform_type_bool

04bf4ae

Move unit declarations and add comments

4815cd5

adpaco-aws force-pushed the integer-type branch from 51c2af0 to 4815cd5 Compare October 27, 2022 21:08

Format C file

d75819b

tautschnig reviewed Oct 27, 2022

View reviewed changes

danielsn reviewed Oct 27, 2022

View reviewed changes

adpaco-aws added 3 commits October 27, 2022 22:02

Add comment and ref to CBMC issue

b5fadab

Address comments about type attributes and comments

2b67629

Avoid unwrap in transform code

77083fe

Upgrade CBMC to v5.69.1

38e5f23

adpaco-aws changed the title ~~Upgrade to CBMC 5.68.0 (with fixes)~~ Upgrade to CBMC 5.69.1 (with fixes) Oct 28, 2022

adpaco-aws changed the title ~~Upgrade to CBMC 5.69.1 (with fixes)~~ Upgrade to CBMC 5.68.0 (with fixes) Oct 28, 2022

adpaco-aws force-pushed the integer-type branch from 85eb7a4 to 38e5f23 Compare October 28, 2022 20:45

danielsn reviewed Oct 28, 2022

View reviewed changes

adpaco-aws mentioned this pull request Oct 31, 2022

Unit types for external void functions shouldn't be needed #1817

Open

adpaco-aws added 2 commits October 31, 2022 14:37

Comment and ref. to issue on extern C functions

9b62f1f

Merge branch 'main' into integer-type

308ee14

adpaco-aws mentioned this pull request Oct 31, 2022

Formula for CBMC 5.69.1 is missing diffblue/cbmc#7286

Closed

danielsn approved these changes Oct 31, 2022

View reviewed changes

adpaco-aws mentioned this pull request Oct 31, 2022

Target directories should be cleaned before codegen #1821

Closed

Merge branch 'main' into integer-type

2a8e4ec

adpaco-aws merged commit 3007e84 into model-checking:main Nov 1, 2022

adpaco-aws added a commit that referenced this pull request Nov 1, 2022

Revert "Upgrade to CBMC 5.68.0 (with fixes) (#1811)"

e41f3b0

This reverts commit 3007e84.

adpaco-aws changed the title ~~Upgrade to CBMC 5.68.0 (with fixes)~~ Upgrade to CBMC 5.69.1 (with fixes) Nov 1, 2022

adpaco-aws self-assigned this Nov 1, 2022

zpzigi754 mentioned this pull request Nov 2, 2022

0.14 tar.gz file not found on the first execution of kani binary #1834

Closed

tedinski mentioned this pull request Dec 6, 2022

Move Diamond Dependency Bash script to tests/ for async running #1733

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Upgrade to CBMC 5.69.1 (with fixes) #1811

Upgrade to CBMC 5.69.1 (with fixes) #1811

adpaco-aws commented Oct 27, 2022 •

edited

Loading

tautschnig Oct 27, 2022

adpaco-aws Oct 27, 2022

adpaco-aws Oct 27, 2022

danielsn Oct 28, 2022

danielsn Oct 27, 2022

adpaco-aws Oct 27, 2022

tautschnig Oct 28, 2022

danielsn Oct 27, 2022

adpaco-aws Oct 27, 2022

danielsn Oct 27, 2022

adpaco-aws Oct 27, 2022

tautschnig commented Oct 28, 2022

adpaco-aws commented Oct 28, 2022

tautschnig commented Oct 28, 2022

danielsn Oct 28, 2022

Upgrade to CBMC 5.69.1 (with fixes) #1811

Upgrade to CBMC 5.69.1 (with fixes) #1811

Conversation

adpaco-aws commented Oct 27, 2022 • edited Loading

Description of changes:

Resolved issues:

Testing:

Checklist

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

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

tautschnig commented Oct 28, 2022

adpaco-aws commented Oct 28, 2022

tautschnig commented Oct 28, 2022

Choose a reason for hiding this comment

adpaco-aws commented Oct 27, 2022 •

edited

Loading