CONTRACTS: Hotfix for is_fresh performance #7425

remi-delmas-3000 · 2022-12-09T21:03:34Z

This is a hotfix for a performance regression introduced by control flow branches and malloc failure modes.

Solves a major performance issue and aligns the
behavior of is_fresh with that of malloc with
respect to size assertions/assumptions.

malloc is now inlined in the body of
__CPROVER_contract_is_fresh and the
failure logic is simplified in assumption
contexts.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

feliperodri · 2022-12-09T22:01:38Z

regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_pass/vect.h

@@ -11,8 +11,8 @@ void resize_vec(vect *v, size_t incr)
  // clang-format off
 __CPROVER_requires(
  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size < __CPROVER_max_malloc_size &&


IMHO, It seems counter-productive to ask users to add an extra assumption in their contracts to make sure the size will be smaller than the maximum malloc size for CBMC. This is outside of the scope of this PR, but we should have a separate discussion why this is necessary in general.

I'm with Felipe on this one. Within CBMC if it is fresh it must also be within that size because malloc can only produce things of that size without failing, so I think world would be a better place if we just moved this into the is_fresh predicate - it can return false if the size is too big.
Also, then when we change the memory model we don't have to change all the assumptions in proofs to get rid of this.

codecov · 2022-12-09T22:39:22Z

Codecov Report

Base: 78.39% // Head: 78.38% // Decreases project coverage by -0.01% ⚠️

Coverage data is based on head (3a1a5ac) compared to base (b03d870).
Patch has no changes to coverable lines.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7425      +/-   ##
===========================================
- Coverage    78.39%   78.38%   -0.02%     
===========================================
  Files         1655     1655              
  Lines       190281   190304      +23     
===========================================
- Hits        149172   149166       -6     
- Misses       41109    41138      +29

Impacted Files	Coverage Δ
...o-instrument/contracts/dynamic-frames/dfcc_utils.h	`0.00% <0.00%> (-100.00%)`	⬇️
...ent/contracts/dynamic-frames/dfcc_spec_functions.h	`0.00% <0.00%> (-100.00%)`	⬇️
...t/contracts/dynamic-frames/dfcc_contract_handler.h	`0.00% <0.00%> (-100.00%)`	⬇️
...racts/dynamic-frames/dfcc_lift_memory_predicates.h	`0.00% <0.00%> (-100.00%)`	⬇️
...contracts/dynamic-frames/dfcc_contract_handler.cpp	`71.64% <0.00%> (-28.36%)`	⬇️
...ment/contracts/dynamic-frames/dfcc_swap_and_wrap.h	`83.33% <0.00%> (-16.67%)`	⬇️
src/goto-programs/goto_program.cpp	`80.24% <0.00%> (-1.56%)`	⬇️
...strument/contracts/dynamic-frames/dfcc_library.cpp	`95.04% <0.00%> (-0.50%)`	⬇️
src/ansi-c/c_typecheck_base.cpp	`83.10% <0.00%> (-0.20%)`	⬇️
src/goto-instrument/contracts/contracts.cpp	`95.38% <0.00%> (-0.02%)`	⬇️
... and 4 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

jimgrundy · 2022-12-10T00:12:32Z

regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_pass/vect.h

@@ -11,8 +11,8 @@ void resize_vec(vect *v, size_t incr)
  // clang-format off
 __CPROVER_requires(
  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size < __CPROVER_max_malloc_size &&


I'm with Felipe on this one. Within CBMC if it is fresh it must also be within that size because malloc can only produce things of that size without failing, so I think world would be a better place if we just moved this into the is_fresh predicate - it can return false if the size is too big.
Also, then when we change the memory model we don't have to change all the assumptions in proofs to get rid of this.

remi-delmas-3000 · 2022-12-10T00:58:15Z

I'm with Felipe on this one. Within CBMC if it is fresh it must also be within that size because malloc can only produce things of that size without failing, so I think world would be a better place if we just moved this into the is_fresh predicate - it can return false if the size is too big. Also, then when we change the memory model we don't have to change all the assumptions in proofs to get rid of this.

Agreed, but moving this check inside the predicate thereby adding a control flow branch is what caused the drastic performance degradation we observed.

With CBMC the pointer model is also leaking its implementation details:

Right now, without malloc failure modes, CBMC lets you allocate up to SIZE_MAX but trying to access it will result in a OOB failure:

#include <stdlib.h>
int main()
{
  size_t size;

  char *a = malloc(size);
  if(a && size > 0) {
    assert(size <= __CPROVER_max_malloc_size);
    a[size-1] = 0;
  }
}

❯ cbmc toto.c --pointer-check

** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 28 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 33 max allocation may fail: SUCCESS

toto.c function main
[main.assertion.1] line 8 assertion size <= __CPROVER_max_malloc_size: FAILURE
[main.pointer_dereference.1] line 9 dereference failure: pointer NULL in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.2] line 9 dereference failure: pointer invalid in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.3] line 9 dereference failure: deallocated dynamic object in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.4] line 9 dereference failure: dead object in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.5] line 9 dereference failure: pointer outside object bounds in a[(signed long int)(size - (unsigned long int)1)]: FAILURE
[main.pointer_dereference.6] line 9 dereference failure: invalid integer address in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS

** 2 of 9 failed (2 iterations)
VERIFICATION FAILED

Activating the --malloc-fail-null failure mode prevents the error but the size is implicitly restricted to be less than max_malloc_size. If there's another constraint on size that says it should be greater than max malloc size, we can have a implicit contradiction.

❯ cbmc toto.c --pointer-check --malloc-may-fail --malloc-fail-null

** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 28 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 33 max allocation may fail: SUCCESS

toto.c function main
[main.assertion.1] line 8 assertion size <= __CPROVER_max_malloc_size: SUCCESS
[main.pointer_dereference.1] line 9 dereference failure: pointer NULL in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.2] line 9 dereference failure: pointer invalid in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.3] line 9 dereference failure: deallocated dynamic object in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.4] line 9 dereference failure: dead object in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.5] line 9 dereference failure: pointer outside object bounds in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.6] line 9 dereference failure: invalid integer address in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS

** 0 of 9 failed (1 iterations)
VERIFICATION SUCCESSFUL

Last, the --malloc-fail-assert mode solves the OOB and imposes a hard limit on size, but also checks that size < max_malloc_size.

This is the behaviour I implemented for is_fresh in this PR: check the bound and assume it holds in the rest of the execution.

❯ cbmc toto.c --pointer-check --malloc-may-fail --malloc-fail-assert

** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 28 max allocation size exceeded: FAILURE
[malloc.assertion.2] line 33 max allocation may fail: FAILURE

toto.c function main
[main.assertion.1] line 8 assertion size <= __CPROVER_max_malloc_size: SUCCESS
[main.pointer_dereference.1] line 9 dereference failure: pointer NULL in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.2] line 9 dereference failure: pointer invalid in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.3] line 9 dereference failure: deallocated dynamic object in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.4] line 9 dereference failure: dead object in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.5] line 9 dereference failure: pointer outside object bounds in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS
[main.pointer_dereference.6] line 9 dereference failure: invalid integer address in a[(signed long int)(size - (unsigned long int)1)]: SUCCESS

** 2 of 9 failed (3 iterations)
VERIFICATION FAILED

EDIT: after thinking about it I could actually replicate these three behaviours in is_fresh depending on the switches to align it with malloc.

remi-delmas-3000 · 2022-12-10T17:28:33Z

The latest update solves the performance issue and proper handling of malloc failure modes to mirror that of malloc with respect to size limits. In particular, when using --malloc-may-fail --malloc-fail-null is fresh does not require the user to add explicit size limits, it just assumes them and continues execution. When --malloc-may-fail --malloc-fail-assert is used, an assertion is triggered if size is too big but execution continue assuming that the size is capped.
If no failure mode is active, is fresh does not check size limits and allocates an object up to SIZE_MAX, but any attempt to access this object beyond the maximum offset representable without overflow will trigger errors.

feliperodri

Thank you for addressing the issue with __CPROVER_max_malloc_size.

feliperodri · 2022-12-10T19:33:15Z

src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md

+
+1. **No failure mode** (no flags):
+  In this mode, `malloc` and `__CPROVER_is_fresh` never fail
+  and will accept a size parameter up to `SIZE_MAX` without triggerring errors.


Suggested change

and will accept a size parameter up to `SIZE_MAX` without triggerring errors.

and will accept a size parameter up to `SIZE_MAX` without triggering errors.

feliperodri · 2022-12-10T19:35:13Z

src/ansi-c/library/cprover_contracts.c

+
+    // record the object size for non-determistic bounds checking
+    __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
+    __CPROVER_malloc_is_new_array =


I've tested your new approach in some contracts and I get the following warning:

file <builtin-library-free> line 10: symbol '__CPROVER_malloc_is_new_array' already has an initial value

Is it something that could be suppressed? Does it affect the analysis?

With #6590 having been merged I'd suggest to use __CPROVER_bool __CPROVER_malloc_is_new_array = 0; instead of the extern declaration.

jimgrundy · 2022-12-10T19:47:10Z

Thank you for addressing the issue with __CPROVER_max_malloc_size.

What Felipe said! Thanks Remi.

tautschnig · 2022-12-12T13:20:54Z

I have created #7426 to track the (likely unrelated) CSmith failure.

tautschnig · 2022-12-12T13:23:00Z

src/ansi-c/library/cprover_contracts.c

+    // detect memory leaks
+    __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
+    __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;


Should uses of is_fresh really participate in memory-leak checking?

is_fresh allocates when assumed

in a requires clause of a contract being checked;

should not participate in leak checking because case 1. models what's provided by the open environmnent of the contract being checked.

in an ensures clause of a contract being used to abstract a call.

should participate in leak checking because it models an allocation happening in the user program, not the environment

Does that seem reasonable ?

Sounds good to me.

tautschnig · 2022-12-12T13:27:05Z

src/ansi-c/library/cprover_contracts.c

+
+    // record the object size for non-determistic bounds checking
+    __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
+    __CPROVER_malloc_is_new_array =


With #6590 having been merged I'd suggest to use __CPROVER_bool __CPROVER_malloc_is_new_array = 0; instead of the extern declaration.

tautschnig · 2022-12-12T13:29:03Z

src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md

@@ -129,6 +129,38 @@ int foo()
 }
 ```

+#### Influence of memory allocation failure modes flags in assumption contexts
+
+CBMC offers three memory allocation failure modes which result in different


Cross-ref to doc/cprover-manual/memory-primitives.md?

remi-delmas-3000 · 2022-12-12T14:58:56Z

With #6590 having been merged I'd suggest to use __CPROVER_bool __CPROVER_malloc_is_new_array = 0; instead of the extern declaration.

@tautschnig Should I also initialise other extern variables declared in cprover_contacts.c ?

extern __CPROVER_size_t __CPROVER_max_malloc_size;
extern const void *__CPROVER_alloca_object;
extern const void *__CPROVER_deallocated;
extern const void *__CPROVER_new_object;
extern const void *__CPROVER_memory_leak;

tautschnig · 2022-12-12T15:20:47Z

With #6590 having been merged I'd suggest to use __CPROVER_bool __CPROVER_malloc_is_new_array = 0; instead of the extern declaration.

@tautschnig Should I also initialise other extern variables declared in cprover_contacts.c ?
extern __CPROVER_size_t __CPROVER_max_malloc_size;
extern const void *__CPROVER_alloca_object;
extern const void *__CPROVER_deallocated;
extern const void *__CPROVER_new_object;
extern const void *__CPROVER_memory_leak;

Yes, with the exception of __CPROVER_deallocated (which is different from all the others, because its use is not limited to the library, but instead the symbol will also be used when expressing properties).

Solves a major performance issue and aligns the behavior of is_fresh with that of malloc with respect to size assertions/assumptions. malloc is now inlined in the body of `__CPROVER_contract_is_fresh` and the failure logic is simplified in assumption contexts.

remi-delmas-3000 requested review from kroening, tautschnig, chris-ryder and peterschrammel as code owners December 9, 2022 21:03

feliperodri added Performance Optimisations aws Bugs or features of importance to AWS CBMC users aws-high Code Contracts Function and loop contracts labels Dec 9, 2022

feliperodri changed the title ~~CONTRACTS: hotfix for is_fresh performance~~ CONTRACTS: Hotfix for is_fresh performance Dec 9, 2022

feliperodri approved these changes Dec 9, 2022

View reviewed changes

feliperodri assigned tautschnig Dec 9, 2022

jimgrundy approved these changes Dec 10, 2022

View reviewed changes

remi-delmas-3000 force-pushed the is-fresh-performance-hotfix branch from ec3be0f to cb543d5 Compare December 10, 2022 17:25

remi-delmas-3000 requested review from jimgrundy and feliperodri December 10, 2022 18:46

feliperodri approved these changes Dec 10, 2022

View reviewed changes

jimgrundy approved these changes Dec 10, 2022

View reviewed changes

tautschnig mentioned this pull request Dec 12, 2022

CSmith test with random seed 1670693558 results in invariant failure #7426

Closed

tautschnig approved these changes Dec 12, 2022

View reviewed changes

tautschnig assigned remi-delmas-3000 and unassigned tautschnig Dec 12, 2022

remi-delmas-3000 force-pushed the is-fresh-performance-hotfix branch from cb543d5 to 3a1a5ac Compare December 12, 2022 16:00

remi-delmas-3000 merged commit c1e2ed3 into diffblue:develop Dec 12, 2022

	and will accept a size parameter up to `SIZE_MAX` without triggerring errors.
	and will accept a size parameter up to `SIZE_MAX` without triggering errors.

CONTRACTS: Hotfix for is_fresh performance #7425

CONTRACTS: Hotfix for is_fresh performance #7425

Uh oh!

Conversation

remi-delmas-3000 commented Dec 9, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Dec 9, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 commented Dec 10, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

remi-delmas-3000 commented Dec 10, 2022

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jimgrundy commented Dec 10, 2022 • edited by feliperodri Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig commented Dec 12, 2022

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 commented Dec 12, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig commented Dec 12, 2022

Uh oh!

Uh oh!

remi-delmas-3000 commented Dec 9, 2022 •

edited

Loading

codecov bot commented Dec 9, 2022 •

edited

Loading

remi-delmas-3000 commented Dec 10, 2022 •

edited

Loading

jimgrundy commented Dec 10, 2022 •

edited by feliperodri

Loading

remi-delmas-3000 commented Dec 12, 2022 •

edited

Loading