Initial reworking of code contracts [depends-on: #3769, blocks: #2677] #2676

qaphla · 2018-08-03T14:02:09Z

The primary function of this change is to split the --apply-code-contracts pass into two separate passes, one of which uses (without checking) the contracts, and one of which checks and applies the contracts together. More details can be seen in the commit messages.

One key note from the commit messages:
While it is clear that applying contracts without checking them
is unsound, it is nevertheless useful in verifying large pieces
of software in a modular fashion. If we verify a function to
satisfy its specification from an arbitrary environment, then
we can avoid needing to check that function again by using
--apply-code-contracts.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 10e55d8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80887591
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

kroening · 2018-08-04T09:04:20Z

src/goto-instrument/goto_instrument_parse_options.cpp

+  if(cmdline.isset("check-code-contracts"))
+  {
+    status() << "Checking Code Contracts" << eom;
+    check_code_contracts(goto_model);
  }



Some comment for the "apply-code-contracts" case would be helpful -- it's now easy to be confused between apply-code-contracts and check-code-contracts

kroening · 2018-08-04T09:05:36Z

src/goto-instrument/loop_utils.cpp

@@ -107,3 +108,41 @@ void get_modifies(
    }
  }
 }
+
+// TODO handle aliasing at all
+void get_uses(


I would rename this to something more verbose, say "get_used_symbols", and also comment that you do include symbols whose address is taken.

kroening · 2018-08-04T09:06:21Z

src/goto-instrument/loop_utils.cpp

+  const local_may_aliast &local_may_alias,
+  const loopt &loop,
+  usest &uses)
+{


Also, C++ now has rvalue references, which implies that large data structures can be returned without copy. I'd consider returning directly here.

kroening · 2018-08-04T09:06:42Z

src/goto-instrument/loop_utils.h

@@ -17,13 +17,19 @@ Author: Daniel Kroening, [email protected]
 class local_may_aliast;

 typedef std::set<exprt> modifiest;
+typedef std::set<exprt> usest;
 typedef const natural_loops_mutablet::natural_loopt loopt;


Make this a set of symbols?

martin-cs · 2018-08-06T13:56:34Z

.gitignore

@@ -19,6 +19,8 @@ src/.settings/*
 # Visual Studio
 Debug/*
 Release/*
+#vi(m)
+*.swp



In the future I think this kind of thing would be better as an independent PR.

martin-cs · 2018-08-06T13:57:26Z

regression/contracts/function_check_mem_01/main.c

@@ -33,7 +33,7 @@ void foo(bar *x)
  __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar)))
 {
  x->x += 1;
-  return
+  return;


I'm a little concerned about why this wasn't caught earlier. Were these tests just not run?

This was a test that was introduced as KNOWNBUG (and presumably copied poorly from the original piece of code that inspired it).

martin-cs · 2018-08-06T14:04:13Z

src/goto-instrument/loop_utils.cpp

@@ -107,3 +108,41 @@ void get_modifies(
    }
  }
 }
+
+// TODO handle aliasing at all


:-\ This makes me a little nervous...

I'm working on removing this --- this function was introduced very briefly before it was removed and I thought that it hadn't made it into any of the pull requests. Next revision shouldn't have it (or any of the problems that came with it being very temporary).

martin-cs · 2018-08-06T14:05:04Z

src/goto-instrument/loop_utils.cpp

+      {
+        if((*it).id()==ID_symbol)
+        {
+          uses.insert(*it);


Would goto_rw be useful here?

See #2677 for a replacement of the local_may_alias analysis used in this version with goto_rw.

The previous implementation of code-contracts has a single flag --apply-code-contracts, which created checks to verify that the contracts are satisfied and also used the contracts to abstract out the portions of code which had contracts provided. This commit splits that process into two parts, one of which only uses the contracts, without checking that they hold (--apply-code-contracts) and the other of which (incomplete as of this commit) both checks and applies, in a similar manner to the existing method. While it is clear that applying contracts without checking them is unsound, it is nevertheless useful in verifying large pieces of software in a modular fashion. If we verify a function to satisfy its specification from an arbitrary environment, then we can avoid needing to check that function again by using --apply-code-contracts.

This commit completes the work started in the previous commit by revising the existing contract-handling code into the new pass --check-code-contracts, which first applies all contracts and then checks them. By applying the contracts before checking begins, this checks the relative correctness of each function/loop with respect to the functions called by/loops contained in it. Since there can be no infinite sequence of nested functions/loops, these relative correctness results together imply the correctness of the overall program. We take this approach rather than checking entirely without using contracts because it allows significant reuse of results --- a function that is called many times only needs to be checked once, and all of its invocations will be abstracted out by the contract application.

Several functions from the old implementation of code-contracts that were made dead by the previous commits are removed by this commit. Additionally, some variables which were formerly in use are no longer needed, and so are removed.

kroening · 2018-08-06T16:20:56Z

Apologies for bugging about the difference between "applying" and "checking" code contracts: How about "assume-code-contracts" -- this would make the difference clearer?

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 9d249ba).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/81044800
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: c3c6b8b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/81048563
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

qaphla · 2018-08-06T16:57:27Z

Would you suggest having assume/check as the pair, or assume/assert as a more closely matched pair?

kroening · 2018-08-07T07:30:28Z

assume/assert will likely be the most familiar choice for existing users!

TGWDB · 2023-05-03T15:22:31Z

Closing due to age (no further comment on PR content), please reopen with rebase on develop if you intent to continue this work.

qaphla requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, smowton and tautschnig as code owners August 3, 2018 14:02

qaphla mentioned this pull request Aug 3, 2018

Improvements to code contracts [depends-on: #2646, #2676, blocks: #2712] #2677

Closed

allredj reviewed Aug 3, 2018

View reviewed changes

kroening reviewed Aug 4, 2018

View reviewed changes

kroening approved these changes Aug 4, 2018

View reviewed changes

martin-cs reviewed Aug 6, 2018

View reviewed changes

qaphla force-pushed the contracts_part1 branch from 10e55d8 to 3156a11 Compare August 6, 2018 14:39

qaphla requested review from pkesseli and thk123 as code owners August 6, 2018 14:39

qaphla force-pushed the contracts_part1 branch from 3156a11 to 9d249ba Compare August 6, 2018 14:43

klaas added 3 commits August 6, 2018 11:20

Removes some dead code.

c3c6b8b

Several functions from the old implementation of code-contracts that were made dead by the previous commits are removed by this commit. Additionally, some variables which were formerly in use are no longer needed, and so are removed.

qaphla force-pushed the contracts_part1 branch from 9d249ba to c3c6b8b Compare August 6, 2018 15:30

allredj reviewed Aug 6, 2018

View reviewed changes

qaphla mentioned this pull request Aug 10, 2018

Contracts dependence on remove_returns [depends-on: #2677] #2712

Closed

tautschnig self-assigned this Nov 10, 2018

tautschnig changed the title ~~Initial reworking of code contracts~~ Initial reworking of code contracts [blocks: #2677] Nov 10, 2018

tautschnig added the blocker label Nov 10, 2018

tautschnig changed the title ~~Initial reworking of code contracts [blocks: #2677]~~ Initial reworking of code contracts [depends-on: #3769, blocks: #2677] Feb 25, 2019

tautschnig added the dependent - do not merge label Feb 25, 2019

TGWDB closed this May 3, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Initial reworking of code contracts [depends-on: #3769, blocks: #2677] #2676

Initial reworking of code contracts [depends-on: #3769, blocks: #2677] #2676

qaphla commented Aug 3, 2018

allredj left a comment

kroening Aug 4, 2018

kroening Aug 4, 2018

kroening Aug 4, 2018

kroening Aug 4, 2018

martin-cs Aug 6, 2018

martin-cs Aug 6, 2018

qaphla Aug 6, 2018

martin-cs Aug 6, 2018

qaphla Aug 6, 2018

martin-cs Aug 6, 2018

qaphla Aug 6, 2018

kroening commented Aug 6, 2018

allredj left a comment

allredj left a comment

qaphla commented Aug 6, 2018

kroening commented Aug 7, 2018

TGWDB commented May 3, 2023

Initial reworking of code contracts [depends-on: #3769, blocks: #2677] #2676

Initial reworking of code contracts [depends-on: #3769, blocks: #2677] #2676

Conversation

qaphla commented Aug 3, 2018

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

kroening commented Aug 6, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

qaphla commented Aug 6, 2018

kroening commented Aug 7, 2018

TGWDB commented May 3, 2023