Fix havocking of dependent assigns clause targets #6540

remi-delmas-3000 · 2021-12-21T00:43:14Z

The first commit fixes a minor issue with history variables (allow history variables for constant and typecast expressions).

The second commit fixes missing declarations for return value variables introduced during replacement of function calls by contracts.

The third commit fixes a problem with assigns clause havocking when replacing calls by contracts.

When replacing a function call by its contract, we would directly havoc the targets of the assigns clause in an unspecified order. If the assigns clause contained dependent targets such as assigns(s->ptr, *(s->ptr)), havocking s->ptr before *s->ptr would lead to errors and incorrect results.

We now introduce independent snapshot variables storing the address of each target and havoc them in a second time to avoid this dependency on the ordering of havoc instructions.

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.

codecov · 2021-12-21T01:52:47Z

Codecov Report

Merging #6540 (22c020b) into develop (6642254) will increase coverage by 0.00%.
The diff coverage is 95.38%.

@@            Coverage Diff            @@
##           develop    #6540    +/-   ##
=========================================
  Coverage    75.99%   75.99%            
=========================================
  Files         1578     1579     +1     
  Lines       180944   181103   +159     
=========================================
+ Hits        137500   137621   +121     
- Misses       43444    43482    +38

Impacted Files	Coverage Δ
src/goto-instrument/contracts/assigns.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/utils.cpp	`89.47% <78.57%> (-4.56%)`	⬇️
src/goto-instrument/contracts/assigns.cpp	`95.83% <90.00%> (-0.60%)`	⬇️
...trument/contracts/havoc_assigns_clause_targets.cpp	`98.07% <98.07%> (ø)`
src/goto-instrument/contracts/contracts.cpp	`91.28% <98.85%> (-3.83%)`	⬇️
src/goto-instrument/contracts/utils.h	`100.00% <100.00%> (ø)`
src/analyses/dirty.h	`100.00% <0.00%> (ø)`
src/analyses/locals.h	`100.00% <0.00%> (+14.28%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 95d8c91...22c020b. Read the comment docs.

tautschnig · 2021-12-21T14:55:26Z

src/goto-instrument/contracts/contracts.cpp

+    const auto &id = parameter.id();
    if(
-      parameter.id() == ID_dereference || parameter.id() == ID_member ||
-      parameter.id() == ID_symbol || parameter.id() == ID_ptrmember)
+      id == ID_dereference || id == ID_member || id == ID_symbol ||
+      id == ID_ptrmember || id == ID_constant || id == ID_typecast)
    {


Is there a test that demonstrates the need for this?

The tests added in this PR will fail without this.

added specific tests

tautschnig · 2021-12-21T14:56:43Z

regression/contracts/assigns_replace_08/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[foo.\d+\] line \d+ Check that \*z is assignable: FAILURE$
+\[foo.\d+\] line \d+ Check that \*z assigned by replaced bar is assignable: FAILURE$


I'm struggling to parse this - should it perhaps say "replaced function bar?"

How about Check that \*z is assignable (function bar replacement): ?

tautschnig · 2021-12-21T14:59:43Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.h

+#include <util/namespace.h>
+#include <util/symbol_table.h>


Forward declarations (class namespacet;, class symbol_tablet;) will do the trick here. (This is to reduce compilation times where possible.)

tautschnig · 2021-12-21T15:00:32Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.h

+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
+
+#include <set>


This isn't used here.

tautschnig · 2021-12-21T15:00:59Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.h

+
+#include <set>
+
+#include <goto-programs/goto_program.h>


I think you'll only need #include <util/expr.h>, everything else can be forward-declared.

indeed this works

tautschnig · 2021-12-21T15:07:09Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

+    const auto &size = size_of_expr(target.type(), ns);
+
+    INVARIANT(
+      size.has_value(),


Please move this into the INVARIANT to avoid a situation where size ends up as an unused value (when completely disabling invariants). That is: INVARIANT(size_of_expr(target.type(), ns).has_value(), ...)

tautschnig · 2021-12-21T15:08:47Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

+      "`sizeof` must always be computable on assignable assigns clause "
+      "targets.");
+
+    return address_of_exprt{target, pointer_type(target.type())};


Wouldn't is_assignable be true for something like a[5], but taking the address thereof would not actually be the "base address" (or at least not how I'd understand that term).

This computes the start address of the thing that gets assigned. If contract assigns a[5] the base address of the thing that gets assigned is &(a[5]). If the contract says it assigns __CPROVER_pointer_object(a[5]) then the base address will be the address pointed to by a-5.

I'd then find something along the lines of "build_address_of" a more natural function name, but this might be a matter of personal preference.

As a side, note that address_of_exprt has a convenience constructor that takes just the object, i.e., the above is equivalent to address_of_exprt{target}. The constructor will create the pointer type from the type of target.

renamed to build_address_of

tautschnig · 2021-12-21T15:10:45Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

+  dest.add(goto_programt::make_decl(target_valid_var));
+
+  dest.add(goto_programt::make_decl(target_snapshot_var));
+
+  dest.add(goto_programt::make_assignment(
+    target_valid_var, all_dereferences_are_valid(target_pointer, ns)));
+
+  dest.add(goto_programt::make_assignment(
+    target_snapshot_var,
+    null_pointer_exprt{to_pointer_type(target_pointer.type())}));


For debugging purposes it would be helpful if all these had source locations that relate them in some way to the location a snapshot is taken at. Hmm, you're doing this after the fact. That's a bit confusing, in my opinion.

tautschnig · 2021-12-21T15:12:24Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

+  goto_programt skip_program;
+  const auto skip_target = skip_program.add(goto_programt::make_skip());
+
+  dest.add(goto_programt::make_goto(skip_target, not_exprt{target_valid_var}));
+
+  dest.add(goto_programt::make_assignment(target_snapshot_var, target_pointer));
+
+  dest.destructive_append(skip_program);


You could use insert_before_swap to avoid the skip_program. But then it probably doesn't make a whole lot of a difference.

it seems less natural, since after inserting the skip statement in dest, you would have to use a mix of insert_before_swap and skip_target++ or to insert instructions in reverse, or to create another program and insert_before_swap and then ++ the skip_target

tautschnig · 2021-12-21T15:14:08Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

+    codet code(ID_havoc_object);
+    code.add_to_operands(target_snapshot_var);


codet code(ID_havoc_object, {target_snapshot_var}); would avoid the two-step construction.

feliperodri

Only minor comments.

feliperodri · 2021-12-21T15:57:02Z

regression/contracts/assigns_replace_08/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[foo.\d+\] line \d+ Check that \*z is assignable: FAILURE$
+\[foo.\d+\] line \d+ Check that \*z assigned by replaced bar is assignable: FAILURE$


How about Check that \*z is assignable (function bar replacement): ?

feliperodri · 2021-12-21T16:07:18Z

regression/contracts/assigns_replace_havoc_dependent_targets/vect.h

+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&


Why do you need to check whether v->size is smaller than __CPROVER_max_malloc_size? Haven't this problem been solved (see #6130)?

Whatever the behaviour of CBMC is when this bound is exceeded, I want to avoid it in this example.

feliperodri · 2021-12-21T16:08:04Z

src/goto-instrument/contracts/contracts.cpp

-    havoc_assigns_targetst havoc_gen(assigns, ns);
-    havoc_gen.append_full_havoc_code(location, havoc_instructions);
+    // Havoc all targets in the assigns clause
+    // TODO handle local statics possibly touched by this function


Is there a issue to track this?

feliperodri · 2021-12-21T16:09:15Z

src/goto-instrument/contracts/contracts.cpp

+    // Havoc all targets in the assigns clause
+    // TODO handle local statics possibly touched by this function


nit:

Suggested change

// Havoc all targets in the assigns clause

// TODO handle local statics possibly touched by this function

// Havoc all targets in the assigns clause.

// TODO: handle local statics possibly touched by this function.

feliperodri · 2021-12-21T16:14:57Z

regression/contracts/assigns_replace_havoc_dependent_targets_fail/enforce.desc

+^SIGNAL=0$
+--
+--
+Verifies the contract being replaced in `replace_resize_vec.desc`.


Is that the correct file name? I didn't find it.

feliperodri · 2021-12-21T16:16:16Z

regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h

+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&


See #6130.

Hasn't this problem been fixed? Why do you need v->size <= __CPROVER_max_malloc_size here?

Whatever the behaviour of CBMC is when this bound is exceeded, I want to avoid it in this example.

feliperodri · 2021-12-21T16:18:17Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.h

+/// ```
+/// typedef struct vect { int *arr; int size; } vect;
+/// void resize(vect *v)
+/// __CPOVER_assigns(v->arr, v->size, __CPROVER_POINTER_OBJECT(v->arr))


typo: __CPROVER_assigns

… expressions.

…eturn_value` variables introduced by contract replacement (these would previously appear as global variables).

tautschnig · 2021-12-22T14:33:00Z

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

+    auto res = minus_exprt{ptr, pointer_offset(ptr)};
+    res.type() = ptr.type();
+    return std::move(res);


Scratch my earlier comment, the following will actually do the right thing: return minus_exprt{ptr, pointer_offset(ptr)}; (the type of the minus_exprt will be ptr.type() when constructed in this way).

that works when there are dependencies between targets. We now take a snapshot of the target addresses if they are valid and havoc them in a second step if they are valid. Previously we were havocking targets directly in an arbitrary sequence, and havocking s->ptr before *(s->ptr) before __CPROVER_POINTER_OBJECT(s->ptr) would cause spurious errors.

remi-delmas-3000 · 2021-12-22T21:35:41Z

I took into account all pending comments, it should be good to go now.

tautschnig · 2021-12-22T21:50:31Z

Requires approval from @peterschrammel @martin-cs @chrisr-diffblue as a new file was added to goto-instrument/Makefile.

feliperodri

It needs code owner approval from @peterschrammel @chrisr-diffblue or @martin-cs.

feliperodri · 2022-01-05T15:35:26Z

regression/contracts/history-constant/main.c

@@ -0,0 +1,15 @@
+#include <stdio.h>


Why do we need this include?

feliperodri · 2022-01-05T15:35:38Z

regression/contracts/history-typecast/main.c

@@ -0,0 +1,23 @@
+#include <stdio.h>


Why do we need this include?

chrisr-diffblue

Approving the Makefile changes. Nothing to add beyond the other detailed reviews.

remi-delmas-3000 requested review from feliperodri, SaswatPadhi and tautschnig as code owners December 21, 2021 00:43

remi-delmas-3000 self-assigned this Dec 21, 2021

remi-delmas-3000 added aws Bugs or features of importance to AWS CBMC users aws-high bugfix Code Contracts Function and loop contracts labels Dec 21, 2021

remi-delmas-3000 force-pushed the havoc-dependent-targets branch 5 times, most recently from ee4780c to 5ac6ab4 Compare December 21, 2021 01:00

remi-delmas-3000 force-pushed the havoc-dependent-targets branch from 5ac6ab4 to ea923be Compare December 21, 2021 05:28

remi-delmas-3000 requested review from chrisr-diffblue, martin-cs and peterschrammel as code owners December 21, 2021 05:28

remi-delmas-3000 force-pushed the havoc-dependent-targets branch 2 times, most recently from b789494 to d6aa06a Compare December 21, 2021 14:49

tautschnig approved these changes Dec 21, 2021

View reviewed changes

remi-delmas-3000 force-pushed the havoc-dependent-targets branch from d6aa06a to ecb5269 Compare December 21, 2021 16:11

feliperodri approved these changes Dec 21, 2021

View reviewed changes

remi-delmas-3000 force-pushed the havoc-dependent-targets branch 2 times, most recently from 3ee6728 to 40e8121 Compare December 21, 2021 20:10

Remi Delmas added 2 commits December 21, 2021 20:13

Function contracts: allow history variables for typecast and constant…

9060de1

… expressions.

Function contracts: add missing DECL/DEAD instructions for `ignored_r…

c65d0ff

…eturn_value` variables introduced by contract replacement (these would previously appear as global variables).

remi-delmas-3000 force-pushed the havoc-dependent-targets branch from 40e8121 to 4e5adcf Compare December 21, 2021 20:20

tautschnig reviewed Dec 22, 2021

View reviewed changes

remi-delmas-3000 force-pushed the havoc-dependent-targets branch from 4e5adcf to 22c020b Compare December 22, 2021 21:35

tautschnig assigned peterschrammel, martin-cs and chrisr-diffblue and unassigned remi-delmas-3000 Dec 22, 2021

remi-delmas-3000 mentioned this pull request Dec 23, 2021

Function contracts: preliminary support for conditional targets in assigns clause checking #6546

Merged

7 tasks

feliperodri approved these changes Jan 5, 2022

View reviewed changes

chrisr-diffblue approved these changes Jan 5, 2022

View reviewed changes

tautschnig assigned remi-delmas-3000 and unassigned peterschrammel, martin-cs and chrisr-diffblue Jan 5, 2022

remi-delmas-3000 merged commit 8cd1447 into diffblue:develop Jan 5, 2022

		codet code(ID_havoc_object);
		code.add_to_operands(target_snapshot_var);

		// Havoc all targets in the assigns clause
		// TODO handle local statics possibly touched by this function

		#include <util/namespace.h>
		#include <util/symbol_table.h>


		#include <set>

		#include <goto-programs/goto_program.h>

Fix havocking of dependent assigns clause targets #6540

Fix havocking of dependent assigns clause targets #6540

Uh oh!

Conversation

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

Uh oh!

Uh oh!

codecov bot commented Dec 21, 2021 • 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!

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!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 Dec 21, 2021 • 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!

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!

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!

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!

remi-delmas-3000 Dec 21, 2021 • 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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

remi-delmas-3000 commented Dec 21, 2021 •

edited

Loading

codecov bot commented Dec 21, 2021 •

edited

Loading

remi-delmas-3000 Dec 21, 2021 •

edited

Loading

remi-delmas-3000 Dec 21, 2021 •

edited

Loading

remi-delmas-3000 Dec 21, 2021 •

edited

Loading