Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add size_of annotation to help CBMC's allocator #2395

Merged
merged 1 commit into from
Apr 25, 2023
Merged

Add size_of annotation to help CBMC's allocator #2395

merged 1 commit into from
Apr 25, 2023

Conversation

tautschnig
Copy link
Member

@tautschnig tautschnig commented Apr 20, 2023 •
edited
Loading

Description of changes:

CBMC's heap allocator will produce objects that aren't just a byte array when a prior call to size_of was involved in computing the number of bytes to be allocated via malloc/calloc/realloc. This, in turn, permits type-safe member accesses to heap-allocated objects. This should speed up copying as well as all other operations on the resulting object (which will then not have to go through byte extract/byte update operations).

It also seems that there no longer is a "size_of" intrinsic.

Resolved issues:

Fixes: #1286

Related RFC:

n/a

Call-outs:

n/a

Testing:

  • How is this change tested? Locally reviewed CBMC's --program-only output on some Vector examples.

  • Is this a refactor change? No.

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • n/a 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.

@tautschnig tautschnig requested a review from a team as a code owner April 20, 2023 11:48
@tautschnig tautschnig mentioned this pull request Apr 20, 2023
Open
@tautschnig tautschnig force-pushed the sizeof-tracking branch 3 times, most recently from a7f1712 to d3bc70b Compare April 21, 2023 15:16
adpaco-aws
adpaco-aws reviewed Apr 21, 2023
View reviewed changes
Copy link
Contributor

@adpaco-aws adpaco-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for this detailed explanation, @tautschnig ! A few questions.

cprover_bindings/src/goto_program/expr.rs Show resolved Hide resolved
cprover_bindings/src/irep/to_irep.rs Show resolved Hide resolved
kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs Show resolved Hide resolved
@tautschnig tautschnig force-pushed the sizeof-tracking branch 3 times, most recently from aaf2d64 to 293a50a Compare April 24, 2023 07:37
@tautschnig
Copy link
Member Author

With thanks to @karkhaz for making this happen, and with the hope that this isn't just about some GitHub runner anomaly (but at least the numbers stack up with my local experiment):

  s2n-quic/quic/s2n-quic-core/slice::tests::vectored_copy_fuzz_test:
    variants:
      kani_new:
        metrics:
          solver_runtime: 74.86000000000001
          success: true
          symex_runtime: 7.85538
          verification_time: 93.35263
      kani_old:
        metrics:
          solver_runtime: 178.3941
          success: true
          symex_runtime: 7.67614
          verification_time: 196.657

@adpaco-aws
Copy link
Contributor

adpaco-aws commented Apr 24, 2023 •
edited
Loading

It's looking great, @tautschnig ! Just wondering if you think we should add any more tests to the performance regression or not. Is vectored_copy_fuzz_test already in there?

zhassan-aws
zhassan-aws approved these changes Apr 24, 2023
View reviewed changes
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @tautschnig!

One small point. The OP says:

Fixes: #1781

But #1781 seems unrelated?

@tautschnig
Add size_of annotation to help CBMC's allocator
fbd263b 
CBMC's heap allocator will produce objects that aren't just a byte array
when a prior call to `size_of` was involved in computing the number of
bytes to be allocated via malloc/calloc/realloc. This, in turn, permits
type-safe member accesses to heap-allocated objects. This should speed
up copying as well as all other operations on the resulting object
(which will then not have to go through byte extract/byte update
operations).

It also seems that there no longer is a "size_of" intrinsic.

Fixes: model-checking#1286
@tautschnig
Copy link
Member Author

Thanks @tautschnig!

One small point. The OP says:

Fixes: #1781

But #1781 seems unrelated?

My apologies, looks like I wrongly inferred this from #1286 (comment). I just confirmed that (as expected) #1781 is not fixed.

@tautschnig
Copy link
Member Author

It's looking great, @tautschnig ! Just wondering if you think we should add any more tests to the performance regression or not. Is vectored_copy_fuzz_test already in there?

That test is already there.

@tautschnig tautschnig merged commit b5c116d into model-checking:main Apr 25, 2023
@tautschnig tautschnig deleted the sizeof-tracking branch April 25, 2023 12:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@adpaco-aws adpaco-aws adpaco-aws left review comments

@zhassan-aws zhassan-aws zhassan-aws approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

MPSC Channel test case times out.
3 participants
@tautschnig @adpaco-aws @zhassan-aws