A new implementation for assigns clauses #6377

feliperodri · 2021-10-01T14:25:12Z

This change is a complete rewrite of the assigns clause, based on a new formalization. Each assigns clause target is modeled as a "conditional address range" (CAR) that is an address range guarded by a validity condition.

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).
n/a ~~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-10-03T03:48:17Z

Codecov Report

Merging #6377 (a307396) into develop (3f48b6e) will increase coverage by 0.00%.
The diff coverage is 97.35%.

@@           Coverage Diff            @@
##           develop    #6377   +/-   ##
========================================
  Coverage    75.90%   75.91%           
========================================
  Files         1517     1517           
  Lines       163893   163936   +43     
========================================
+ Hits        124406   124451   +45     
+ Misses       39487    39485    -2

Impacted Files	Coverage Δ
src/ansi-c/ansi_c_convert_type.cpp	`78.78% <ø> (-0.21%)`	⬇️
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/utils.h	`100.00% <ø> (ø)`
src/goto-instrument/havoc_utils.h	`100.00% <ø> (ø)`
src/ansi-c/c_typecheck_base.cpp	`78.24% <50.00%> (-0.52%)`	⬇️
src/goto-instrument/contracts/assigns.cpp	`98.73% <98.55%> (+0.29%)`	⬆️
src/goto-instrument/contracts/assigns.h	`100.00% <100.00%> (ø)`
src/goto-instrument/contracts/contracts.cpp	`95.91% <100.00%> (+0.13%)`	⬆️
src/goto-instrument/contracts/utils.cpp	`91.83% <100.00%> (+0.72%)`	⬆️
src/util/simplify_expr_int.cpp	`84.14% <0.00%> (+0.10%)`	⬆️
... and 3 more

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 a03d382...a307396. Read the comment docs.

SaswatPadhi · 2021-10-03T16:54:31Z

Depends on #6371 -- must be merged after that is merged.

src/goto-instrument/contracts/utils.h

src/ansi-c/ansi_c_convert_type.cpp

regression/contracts/assigns_enforce_23/main.c

regression/contracts/assigns_enforce_23/test.desc

src/goto-instrument/contracts/contracts.cpp

feliperodri · 2021-10-03T17:03:42Z

src/goto-instrument/contracts/contracts.cpp

+      // TODO: Fix this.
+      // The CAR snapshot should be made only once at the beginning.


This comment should map to a GitHub issue and we should add the link here

TODO: <link>

src/goto-instrument/contracts/assigns.cpp

feliperodri · 2021-10-03T17:06:45Z

src/goto-instrument/contracts/assigns.cpp

+  // FIXME: Refactor these checks out to a common function that can be
+  // used both in compilation and instrumentation stages


This should map to a GitHub issue, and we should add the link here.

feliperodri

@SaswatPadhi only minor comments. Approved.

feliperodri · 2021-10-03T21:15:11Z

src/ansi-c/ansi_c_convert_type.cpp

@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]

 #include <util/c_types.h>
 #include <util/config.h>
-#include <util/expr_util.h>
+#include <util/std_code.h>


Why do we need this include?

feliperodri · 2021-10-03T21:17:04Z

src/goto-instrument/contracts/assigns.cpp

+  // FIXME: Refactor these checks out to a common function that can be
+  // used both in compilation and instrumentation stages


Are we tracking this request somewhere?

feliperodri · 2021-10-03T21:18:21Z

src/goto-instrument/contracts/assigns.cpp

+        typecast_exprt::conditional_cast(arg, pointer_type(char_type())),
+        pointer_offset(arg)},


Shall we add a comment about why do we cast this to char here?

src/goto-instrument/contracts/assigns.cpp

src/goto-instrument/contracts/assigns.h

src/goto-instrument/contracts/contracts.cpp

src/goto-instrument/contracts/utils.cpp

feliperodri · 2021-10-03T21:32:02Z

regression/contracts/assigns_enforce_elvis_5/test.desc

@@ -8,3 +8,5 @@ main.c
 --
 Check that Elvis operator expressions of form '(cond ? *if_true : *if_false)'
 are supported in assigns clauses.
+
+BUG: `is_lvalue` in goto is not consistent with `target.get_bool(ID_C_lvalue)`.


We should open a GitHub issue for this bug. This is outside the contract implementation.

This change is a complete rewrite of the assigns clause, based on a new formalization. Each assigns clause target represents a "conditional address range" (CAR) that an address range guarded by a validity constraint. In this commit we also add support for __CPROVER_POINTER_OBJECT expressions in assigns clauses.

SaswatPadhi

Approving on behalf of @feliperodri.

kroening · 2021-10-04T07:28:53Z

regression/contracts/assigns_enforce_18/test.desc

@@ -3,21 +3,18 @@ main.c
 --enforce-contract foo --enforce-contract bar --enforce-contract baz _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[bar.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
+^\[bar.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$


The new message is a downgrade in terms of user experience.

kroening · 2021-10-04T07:39:52Z

regression/contracts/assigns_enforce_23/main.c

+  // clang-format off
+__CPROVER_requires(b->size == 5)
+__CPROVER_assigns(__CPROVER_POINTER_OBJECT(b->buf))
+__CPROVER_assigns(__CPROVER_POINTER_OBJECT(value))


This overloaded use of __CPROVER_POINTER_OBJECT will confuse. I would advise to use a different identifier.

chrisr-diffblue · 2021-10-04T08:35:40Z

src/goto-instrument/contracts/utils.h

@@ -53,10 +53,10 @@ class havoc_if_validt : public havoc_utilst
 /// over all dereferenced pointer expressions *(pexpr_1), *(pexpr_2), ...
 /// found in the AST of `expr`.
 ///
-/// \param expr The expression that contains dereferences to be validated
-/// \param ns The namespace that defines all symbols appearing in `expr`
+/// \param expr: The expression that contains dereferences to be validated.


Extra docs are always nice :-) But the addition of ':' following parameter names is unusual and adds a bit of noise to the diff. Not a blocking comment at all - just an observation to be aware of.

I thought that's the convention in this repo (variable name followed by a colon in the docs). I saw that in several files, so changed this accordingly.
For example: https://github.com/diffblue/cbmc/blob/48893287099cb5780302fe9dc415eb6888354fd6/src/util/expr_cast.h

feliperodri added do not review aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Oct 1, 2021

feliperodri assigned SaswatPadhi and feliperodri Oct 1, 2021

SaswatPadhi force-pushed the car branch 5 times, most recently from 3808cdd to fdfbece Compare October 3, 2021 03:11

SaswatPadhi force-pushed the car branch from fdfbece to d447551 Compare October 3, 2021 04:44

SaswatPadhi changed the title ~~Conditional Address Ranges (CARs)~~ A new implementation for assigns clauses Oct 3, 2021

SaswatPadhi unassigned feliperodri Oct 3, 2021

SaswatPadhi added bugfix and removed do not review labels Oct 3, 2021

SaswatPadhi marked this pull request as ready for review October 3, 2021 06:03

SaswatPadhi requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, SaswatPadhi and tautschnig as code owners October 3, 2021 06:03

jimgrundy approved these changes Oct 3, 2021

View reviewed changes

SaswatPadhi changed the title ~~A new implementation for assigns clauses~~ A new implementation for assigns clauses [depends-on: #6371] Oct 3, 2021

SaswatPadhi added the dependent - do not merge label Oct 3, 2021

jimgrundy added the aws-high label Oct 3, 2021

feliperodri commented Oct 3, 2021

View reviewed changes

Refactor out new_tmp_symbol into utils

f6ea3ec

SaswatPadhi force-pushed the car branch from d447551 to 3d94a78 Compare October 3, 2021 21:08

SaswatPadhi removed the dependent - do not merge label Oct 3, 2021

SaswatPadhi force-pushed the car branch from 3d94a78 to a9b62e9 Compare October 3, 2021 21:21

feliperodri commented Oct 3, 2021

View reviewed changes

SaswatPadhi force-pushed the car branch from a9b62e9 to 3c02ee5 Compare October 3, 2021 22:11

SaswatPadhi approved these changes Oct 3, 2021

View reviewed changes

SaswatPadhi force-pushed the car branch from 3c02ee5 to 27ac569 Compare October 3, 2021 23:24

SaswatPadhi changed the title ~~A new implementation for assigns clauses [depends-on: #6371]~~ A new implementation for assigns clauses Oct 4, 2021

Fix CAR creation for local static symbols

a307396

SaswatPadhi force-pushed the car branch from 27ac569 to a307396 Compare October 4, 2021 00:19

kroening reviewed Oct 4, 2021

View reviewed changes

kroening approved these changes Oct 4, 2021

View reviewed changes

chrisr-diffblue approved these changes Oct 4, 2021

View reviewed changes

feliperodri merged commit 7e7d047 into diffblue:develop Oct 4, 2021

		// TODO: Fix this.
		// The CAR snapshot should be made only once at the beginning.

		// FIXME: Refactor these checks out to a common function that can be
		// used both in compilation and instrumentation stages

		typecast_exprt::conditional_cast(arg, pointer_type(char_type())),
		pointer_offset(arg)},

A new implementation for assigns clauses #6377

A new implementation for assigns clauses #6377

Uh oh!

Conversation

feliperodri commented Oct 1, 2021 • edited by SaswatPadhi Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Oct 3, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

SaswatPadhi commented Oct 3, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi 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!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

feliperodri commented Oct 1, 2021 •

edited by SaswatPadhi

Loading

codecov bot commented Oct 3, 2021 •

edited

Loading