Supports quantifiers in function contracts #5959

ArenBabikian · 2021-03-19T15:36:19Z

This PR adds support for quantified expressions in function contracts. The current implementation handles cases where a function contract is only composed of a single quantified expression. Additionally, nested quantified expressions are not yet supported.

This PR might be a continuation of #2278.
Additionally, #5968 is a follow-up to this PR.

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-03-19T16:57:49Z

Codecov Report

Merging #5959 (edeaf56) into develop (2459a7a) will decrease coverage by 0.96%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #5959      +/-   ##
===========================================
- Coverage    75.01%   74.05%   -0.97%     
===========================================
  Files         1431     1444      +13     
  Lines       155609   157328    +1719     
===========================================
- Hits        116732   116503     -229     
- Misses       38877    40825    +1948

Impacted Files	Coverage Δ
src/goto-instrument/code_contracts.h	`94.11% <ø> (ø)`
src/goto-instrument/code_contracts.cpp	`83.93% <100.00%> (+0.39%)`	⬆️
src/goto-programs/link_goto_model.cpp	`0.00% <0.00%> (-77.97%)`	⬇️
src/ansi-c/literals/convert_character_literal.cpp	`31.70% <0.00%> (-36.59%)`	⬇️
...rc/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp	`51.96% <0.00%> (-28.97%)`	⬇️
src/goto-programs/remove_returns.cpp	`74.84% <0.00%> (-24.53%)`	⬇️
src/ansi-c/c_typecheck_base.cpp	`55.37% <0.00%> (-22.87%)`	⬇️
src/ansi-c/scanner.l	`41.15% <0.00%> (-20.58%)`	⬇️
src/ansi-c/literals/convert_float_literal.cpp	`73.80% <0.00%> (-19.05%)`	⬇️
src/ansi-c/padding.cpp	`76.34% <0.00%> (-17.02%)`	⬇️
... and 98 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 2459a7a...edeaf56. Read the comment docs.

regression/contracts/function_check_02/test.desc

regression/contracts/quantifiers-exists-ensures-01/main.c

regression/contracts/quantifiers-exists-ensures-01/test.desc

regression/contracts/quantifiers-exists-ensures-02/test.desc

regression/contracts/quantifiers-exists-ensures-02/main.c

src/goto-instrument/code_contracts.cpp

src/goto-instrument/code_contracts.h

ArenBabikian · 2021-03-25T18:20:05Z

I have assess all code review comments with the exception of this comment about using INVARIANT() for handling quantifiers (I believe that in the medium-to-long-term, this would not be useful).

feliperodri

LGTM, I only spotted a few more typos and minor comments. Thank you for implementing all comments!!

regression/contracts/quantifiers-exists-ensures-01/test.desc

regression/contracts/quantifiers-exists-ensures-02/test.desc

regression/contracts/quantifiers-exists-requires-01/test.desc

regression/contracts/quantifiers-exists-requires-02/test.desc

regression/contracts/quantifiers-forall-both-01/test.desc

regression/contracts/quantifiers-forall-ensures-01/test.desc

regression/contracts/quantifiers-forall-ensures-02/test.desc

regression/contracts/quantifiers-forall-requires-01/test.desc

regression/contracts/quantifiers-forall-requires-02/test.desc

feliperodri · 2021-03-25T19:50:40Z

src/goto-instrument/code_contracts.cpp

+  // TODO Currently only works if the contract contains only a single
+  // quantified formula
+  // i.e. (1) the top-level element is a quantifier formula
+  // and (2) there are no inner quantifier formulae


Could you tag here the GitHub issue to track this comment?

martin-cs

Looks good. In the perfect world, the code changes and the regression tests would be in separate commits but don't worry about changing that unless you have to push a new version.

martin-cs · 2021-03-28T19:32:58Z

regression/contracts/quantifiers-exists-both-02/test.desc

+The current implementation cannot handle a structure such as
+__CPROVER_assume(__CPROVER_exists(int i; pred(i))), where i is
+not explicitly bounded to a predefined range (i.e. if at least
+one of its bound is only declared and not defined).


Have you tried the SMT back-end?

martin-cs · 2021-03-28T19:35:58Z

src/goto-instrument/code_contracts.cpp

+  // TODO Currently only works if the contract contains only a single
+  // quantified formula
+  // i.e. (1) the top-level element is a quantifier formula
+  // and (2) there are no inner quantifier formulae


I don't think it should be an INVARIANT because it can be triggered by user input. Some kind of warning / error and an issue would be amazing.

regression/contracts/quantifiers-forall-both-02/main.c

SaswatPadhi · 2021-03-28T22:33:41Z

regression/contracts/quantifiers-forall-both-02/main.c

+
+int main()
+{
+  int len, arr[8];


I think len should also be initialized (to 8).

Such a case is already tested for in the quantifiers-forall-both-01 test, and it works with the current implementation. The purpose of this test is in fact to check wether CBMC can handle cases where the range of the quantified variable is not explicitly set a priori.

This adds basic support for quantifiers in funtion contracts. Current support only handles cases where a function contract contains a single, non-nested quantified formula.

ArenBabikian mentioned this pull request Mar 22, 2021

Supports nested quantifiers in function contracts #5968

Merged

7 tasks

feliperodri assigned ArenBabikian Mar 24, 2021

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

ArenBabikian force-pushed the contracts-quantifiers-new branch from 5d3cffc to 70fc83f Compare March 24, 2021 16:05

ArenBabikian marked this pull request as ready for review March 24, 2021 16:25

ArenBabikian requested review from chrisr-diffblue, hannes-steffenhagen-diffblue, martin-cs, peterschrammel and smowton as code owners March 24, 2021 16:25

feliperodri requested changes Mar 24, 2021

View reviewed changes

feliperodri requested a review from tautschnig March 24, 2021 17:13

ArenBabikian force-pushed the contracts-quantifiers-new branch from 72c857a to 8a50d78 Compare March 25, 2021 19:33

feliperodri approved these changes Mar 25, 2021

View reviewed changes

ArenBabikian force-pushed the contracts-quantifiers-new branch from 8a50d78 to 1fe5bd8 Compare March 25, 2021 20:35

martin-cs approved these changes Mar 28, 2021

View reviewed changes

SaswatPadhi suggested changes Mar 28, 2021

View reviewed changes

regression/contracts/quantifiers-forall-both-02/main.c Show resolved Hide resolved

SaswatPadhi reviewed Mar 28, 2021

View reviewed changes

Add support for quantifiers in function contracts

edeaf56

This adds basic support for quantifiers in funtion contracts. Current support only handles cases where a function contract contains a single, non-nested quantified formula.

ArenBabikian force-pushed the contracts-quantifiers-new branch from 1fe5bd8 to edeaf56 Compare April 2, 2021 04:39

SaswatPadhi approved these changes Apr 2, 2021

View reviewed changes

SaswatPadhi merged commit d98b56b into diffblue:develop Apr 2, 2021

ArenBabikian deleted the contracts-quantifiers-new branch April 2, 2021 14:20

Supports quantifiers in function contracts #5959

Supports quantifiers in function contracts #5959

Uh oh!

Conversation

ArenBabikian commented Mar 19, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ArenBabikian commented Mar 25, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

feliperodri Mar 25, 2021

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs Mar 28, 2021

Choose a reason for hiding this comment

Uh oh!

martin-cs Mar 28, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!

SaswatPadhi Mar 28, 2021

Choose a reason for hiding this comment

Uh oh!

ArenBabikian Apr 2, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!

ArenBabikian commented Mar 19, 2021 •

edited

Loading

codecov bot commented Mar 19, 2021 •

edited

Loading

ArenBabikian commented Mar 25, 2021 •

edited

Loading