Supports nested quantifiers in function contracts #5968

ArenBabikian · 2021-03-22T23:15:45Z

This PR adds support for nested quantified expressions in function contracts. It is a direct extension to #5959

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.

martin-cs

Has potential but I think some changes may be needed.

src/ansi-c/c_typecheck_base.cpp

src/ansi-c/parser.y

src/goto-instrument/code_contracts.cpp

src/util/std_expr.h

codecov · 2021-04-02T16:14:30Z

Codecov Report

Merging #5968 (9c9de7b) into develop (72d84b8) will increase coverage by 0.12%.
The diff coverage is 59.37%.

❗ Current head 9c9de7b differs from pull request most recent head 33b412b. Consider uploading reports for the commit 33b412b to get more accurate results

@@             Coverage Diff             @@
##           develop    #5968      +/-   ##
===========================================
+ Coverage    74.02%   74.14%   +0.12%     
===========================================
  Files         1444     1444              
  Lines       157307   157341      +34     
===========================================
+ Hits        116441   116656     +215     
+ Misses       40866    40685     -181

Impacted Files	Coverage Δ
src/goto-instrument/code_contracts.h	`94.11% <ø> (ø)`
src/solvers/smt2/smt2_conv.h	`100.00% <ø> (ø)`
src/solvers/smt2/smt2_conv.cpp	`60.07% <22.22%> (+0.12%)`	⬆️
src/goto-harness/goto_harness_parse_options.cpp	`68.37% <60.00%> (-0.05%)`	⬇️
src/goto-instrument/code_contracts.cpp	`84.41% <100.00%> (+0.87%)`	⬆️
src/ansi-c/literals/convert_character_literal.cpp	`31.70% <0.00%> (-19.52%)`	⬇️
src/goto-programs/read_goto_binary.cpp	`30.84% <0.00%> (-16.83%)`	⬇️
src/ansi-c/c_typecheck_type.cpp	`62.96% <0.00%> (-13.43%)`	⬇️
src/util/mp_arith.cpp	`41.55% <0.00%> (-9.10%)`	⬇️
src/util/std_types.cpp	`83.95% <0.00%> (-4.94%)`	⬇️
... and 29 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 d98b56b...33b412b. Read the comment docs.

src/goto-instrument/code_contracts.cpp

regression/contracts/quantifiers-nested-01/test.desc

feliperodri

LGTM module the requested changes from @SaswatPadhi

src/goto-instrument/code_contracts.cpp

martin-cs

Looks good in principle but please can you use the appropriate exprt types rather than just pulling things out of the operators array.

src/goto-instrument/code_contracts.cpp

SaswatPadhi

Approving since it's not a blocker, but it would be nice to use const references (const T &) in place of copies (T) wherever possible.

src/goto-instrument/code_contracts.cpp

SaswatPadhi · 2021-04-09T14:44:14Z

src/goto-instrument/code_contracts.cpp

@@ -168,23 +169,56 @@ void code_contractst::add_quantified_variable(
  replace_symbolt &replace,


Could we use const exprt& expression?

Currently, I do not think that it is possible. But I the medium/long term, we should get rid of this parameter entirely.

src/goto-instrument/code_contracts.cpp

martin-cs

Approve subject to the requested corrections.

Where possible use the named / most specific accessor functions. This is to avoid the need to rummage around in the irept formatting. In most cases it is just stylistic but in the case of quantifiers it is covering a bug.

src/goto-instrument/code_contracts.cpp

martin-cs · 2021-04-09T15:59:22Z

src/goto-instrument/code_contracts.cpp

+    // 1. get quantified symbol
+    quantifier_exprt quantifier_expression = to_quantifier_expr(expression);
+    exprt tuple = quantifier_expression.operands().at(0);
+    exprt quantified_variable = tuple.operands().at(0);


The other ones I have flagged are style but here it really matters, you should use variables() and where() so that you can handle the case of multiple quantified variables.

I have made the modification as requested. However, I would like to point out that currently, it seems like quantifier expressions with multiple variables are not fully handled (or used, at least). This can be fixed in a separate PR.

Yes, in my experience, most call sites use .symbol() in place of .variables() and expect a quantifier over a single variable. But thanks for the fix here. Looks good to me and we could add a regression test later once we handle multi-variable quantification properly.

src/goto-instrument/code_contracts.cpp

This adds support for nested quantifiers in funtion contracts. We recursively handle quantifiers that are nested within other quantifiers or within Boolean connectives.

ArenBabikian mentioned this pull request Mar 24, 2021

Supports quantifiers in function contracts #5959

Merged

7 tasks

martin-cs reviewed Mar 28, 2021

View reviewed changes

src/ansi-c/c_typecheck_base.cpp Outdated Show resolved Hide resolved

src/ansi-c/parser.y Outdated Show resolved Hide resolved

src/goto-instrument/code_contracts.cpp Outdated Show resolved Hide resolved

src/util/std_expr.h Outdated Show resolved Hide resolved

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

feliperodri assigned ArenBabikian Mar 29, 2021

ArenBabikian force-pushed the contracts-quantifiers-nested branch 2 times, most recently from dcfb077 to 202359e Compare April 2, 2021 14:25

ArenBabikian marked this pull request as ready for review April 2, 2021 14:40

ArenBabikian requested review from chrisr-diffblue, peterschrammel and smowton as code owners April 2, 2021 14:40

SaswatPadhi suggested changes Apr 2, 2021

View reviewed changes

src/goto-instrument/code_contracts.cpp Outdated Show resolved Hide resolved

regression/contracts/quantifiers-nested-01/test.desc Outdated Show resolved Hide resolved

feliperodri approved these changes Apr 2, 2021

View reviewed changes

src/goto-instrument/code_contracts.cpp Outdated Show resolved Hide resolved

ArenBabikian mentioned this pull request Apr 5, 2021

Allow quantifiers within loop invariants #6012

Merged

7 tasks

martin-cs requested changes Apr 6, 2021

View reviewed changes

ArenBabikian force-pushed the contracts-quantifiers-nested branch 2 times, most recently from fbeef9e to 9c925b9 Compare April 9, 2021 14:25

SaswatPadhi approved these changes Apr 9, 2021

View reviewed changes

martin-cs reviewed Apr 9, 2021

View reviewed changes

src/goto-instrument/code_contracts.cpp Outdated Show resolved Hide resolved

martin-cs approved these changes Apr 9, 2021

View reviewed changes

ArenBabikian force-pushed the contracts-quantifiers-nested branch 3 times, most recently from 7e02564 to 4e6f2a7 Compare April 9, 2021 19:43

Add support for nested quantifiers in function contracts

33b412b

This adds support for nested quantifiers in funtion contracts. We recursively handle quantifiers that are nested within other quantifiers or within Boolean connectives.

ArenBabikian force-pushed the contracts-quantifiers-nested branch from 4e6f2a7 to 33b412b Compare April 9, 2021 19:49

SaswatPadhi merged commit d79e5f0 into diffblue:develop Apr 9, 2021

ArenBabikian deleted the contracts-quantifiers-nested branch April 12, 2021 12:58

		@@ -168,23 +169,56 @@ void code_contractst::add_quantified_variable(
		replace_symbolt &replace,

Supports nested quantifiers in function contracts #5968

Supports nested quantifiers in function contracts #5968

Uh oh!

Conversation

ArenBabikian commented Mar 22, 2021

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

codecov bot commented Apr 2, 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!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

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!

SaswatPadhi Apr 9, 2021

Choose a reason for hiding this comment

Uh oh!

ArenBabikian Apr 9, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

martin-cs Apr 9, 2021

Choose a reason for hiding this comment

Uh oh!

ArenBabikian Apr 9, 2021

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi Apr 9, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

codecov bot commented Apr 2, 2021 •

edited

Loading