Adds the notion of a local write set to contracts #6331

feliperodri · 2021-09-03T19:04:24Z

Signed-off-by: Felipe R. Monteiro felisous@amazon.com

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-09-03T20:26:07Z

Codecov Report

Merging #6331 (ea82b03) into develop (aeba3f0) will increase coverage by 0.00%.
The diff coverage is 96.94%.

❗ Current head ea82b03 differs from pull request most recent head 39c62dd. Consider uploading reports for the commit 39c62dd to get more accurate results

@@           Coverage Diff            @@
##           develop    #6331   +/-   ##
========================================
  Coverage    75.89%   75.90%           
========================================
  Files         1515     1515           
  Lines       163972   163990   +18     
========================================
+ Hits        124444   124473   +29     
+ Misses       39528    39517   -11

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/assigns.cpp	`94.44% <94.59%> (-3.34%)`	⬇️
src/goto-instrument/contracts/assigns.h	`100.00% <100.00%> (ø)`
src/goto-instrument/contracts/contracts.cpp	`94.93% <100.00%> (+2.59%)`	⬆️
src/util/simplify_expr.cpp	`84.71% <100.00%> (ø)`
src/goto-programs/goto_program.h	`89.30% <0.00%> (-0.20%)`	⬇️
src/goto-checker/report_util.cpp	`62.31% <0.00%> (+0.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 14d35cc...39c62dd. Read the comment docs.

TGWDB

Good to have a regression test (and the test looks good), please put the information from the test description comment close to where it would be found/used by a developer (to explain why the code works the way it does).

regression/contracts/assigns_enforce_18/test.desc

feliperodri · 2021-09-13T13:17:25Z

@SaswatPadhi could you take another look at it?

SaswatPadhi

I am leaving some initial comments below, but I think we should discuss these two sets that are being maintained within assigns clause now. I think an assigns clause should just refer to the assigns clause on a function / loop -- it shouldn't be modified with other stuff.

We could create a separate class, may be called assignable_set, which would represent a union of the assigns clause + freely assignable local symbols. Let's discuss more offline.

regression/contracts/assigns_enforce_18/test.desc

src/goto-instrument/contracts/assigns.h

src/goto-instrument/contracts/assigns.cpp

SaswatPadhi · 2021-09-13T15:23:43Z

regression/contracts/assigns_validity_pointer_04/test.desc

 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
+^.* 1 of \d+ failed \(\d+ iteration.*\)$


Same comment. Why are we checking 1 out of "anything"?

Thanks for explaining offline. Resolving this.

For this case, it's OK to track 1 of "anything". Pointer primitive check can generate many properties to check and I want to make sure that there is only 1 failure: Check that z is assignable.

I am a little confused as to why only 1 assertion fails here though.

The assigns clause for foo doesn't have z, nor does it have *z. So shouldn't we fail 2 assertions:

the containment check @ assignment z = malloc...

the subset check @ call baz() in the next line (which has *z in the assign clause for baz but not foo)?

We discussed this offline. Two important points:

There is no containment check here, malloc is not treated as a normal function call.

There is a bug in checking the subset relation which is not stressed by this test case. We will address it on a separate PR.

There is no containment check here, malloc is not treated as a normal function call.

Hmm, but malloc just returns a fresh allocation, the left-hand side of the assignment in z = malloc..., i.e. the variable z, must be checked for containment in the assigns clause.

There is a bug in checking the subset relation which is not stressed by this test case. We will address it on a separate PR.

On digging a little bit deeper, I realized that the we don't actually need to separately check the assigns clause during replacement. We can go ahead and havoc directly, and those havocs would fail if something is not assignable in the calling context.

src/goto-instrument/contracts/assigns.cpp

Anything that is local, including local allocations are now tracked by our freely assignable set. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

SaswatPadhi

Some more comments.

src/goto-instrument/contracts/assigns.cpp

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

…bles Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

SaswatPadhi

Thanks! :) A few last comments

src/goto-instrument/contracts/assigns.cpp

SaswatPadhi · 2021-09-13T20:44:20Z

regression/contracts/assigns_enforce_19/main.c

+{
+  b = 1;
+  c = 2;
+  *points_to_b = 1;


Nice test case! We are now correctly looking at assignable (and freely assignable) "addresses" instead of symbols :)

src/goto-instrument/contracts/assigns.cpp

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

SaswatPadhi

Awesome 🎉

2 comments on the regression tests, but otherwise LGTM.

regression/contracts/assigns_enforce_18/test.desc

SaswatPadhi · 2021-09-13T21:47:17Z

regression/contracts/assigns_validity_pointer_04/test.desc

 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
+^.* 1 of \d+ failed \(\d+ iteration.*\)$


I am a little confused as to why only 1 assertion fails here though.

The assigns clause for foo doesn't have z, nor does it have *z. So shouldn't we fail 2 assertions:

the containment check @ assignment z = malloc...

the subset check @ call baz() in the next line (which has *z in the assign clause for baz but not foo)?

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

feliperodri added aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Sep 3, 2021

feliperodri self-assigned this Sep 3, 2021

feliperodri requested a review from SaswatPadhi September 3, 2021 19:04

feliperodri force-pushed the handle-free branch from 4f29797 to 1db3e27 Compare September 3, 2021 19:47

SaswatPadhi added the Tests label Sep 3, 2021

TGWDB requested changes Sep 6, 2021

View reviewed changes

regression/contracts/assigns_enforce_18/test.desc Outdated Show resolved Hide resolved

feliperodri force-pushed the handle-free branch from 1db3e27 to 90b82d1 Compare September 13, 2021 05:08

feliperodri requested a review from tautschnig as a code owner September 13, 2021 05:08

feliperodri changed the title ~~Adds regression test for contract enforcement~~ Removes deallocated objects from write set Sep 13, 2021

TGWDB approved these changes Sep 13, 2021

View reviewed changes

SaswatPadhi added bugfix and removed Tests labels Sep 13, 2021

SaswatPadhi suggested changes Sep 13, 2021

View reviewed changes

feliperodri added 2 commits September 13, 2021 16:42

Removes deallocated objects from write set

fba232b

Anything that is local, including local allocations are now tracked by our freely assignable set. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Removes unused methods from contracts module

c06ccf1

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

feliperodri force-pushed the handle-free branch from 90b82d1 to c06ccf1 Compare September 13, 2021 16:42

SaswatPadhi suggested changes Sep 13, 2021

View reviewed changes

src/goto-instrument/contracts/assigns.cpp Outdated Show resolved Hide resolved

src/goto-instrument/contracts/assigns.cpp Show resolved Hide resolved

src/goto-instrument/contracts/assigns.cpp Show resolved Hide resolved

feliperodri added 3 commits September 13, 2021 20:21

Better naming scheme in assigns clause class

52387ab

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Havoc local write set for loop contracts

c255a15

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Fix contract enforcement to work with (local and global) static varia…

e9cfb2c

…bles Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

feliperodri requested a review from SaswatPadhi September 13, 2021 20:26

feliperodri changed the title ~~Removes deallocated objects from write set~~ Adds the notion of a local write set to contracts Sep 13, 2021

SaswatPadhi reviewed Sep 13, 2021

View reviewed changes

Consider local write set in subset check

6d86395

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

feliperodri force-pushed the handle-free branch from 37bed13 to 6d86395 Compare September 13, 2021 21:38

feliperodri requested a review from SaswatPadhi September 13, 2021 21:38

SaswatPadhi approved these changes Sep 13, 2021

View reviewed changes

Check frame conditions on deallocating

39c62dd

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

feliperodri force-pushed the handle-free branch from ea82b03 to 39c62dd Compare September 14, 2021 18:27

feliperodri merged commit 7435884 into diffblue:develop Sep 14, 2021

feliperodri deleted the handle-free branch September 14, 2021 19:15

Adds the notion of a local write set to contracts #6331

Adds the notion of a local write set to contracts #6331

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

TGWDB left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

feliperodri commented Sep 13, 2021

Uh oh!

SaswatPadhi left a comment • 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!

Uh oh!

Uh oh!

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!

Uh oh!

Uh oh!

SaswatPadhi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

SaswatPadhi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

SaswatPadhi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

feliperodri commented Sep 3, 2021 •

edited

Loading

codecov bot commented Sep 3, 2021 •

edited

Loading

SaswatPadhi left a comment •

edited

Loading