Multidimensional decreases clauses #6236

LongPham7 · 2021-07-19T18:47:29Z

This pull request is about the implementation of "multidimensional" decreases clauses. "One-dimensional" decreases clauses are already supported by the existing version of CBMC. We extend one-dimensional decreases clauses to multidimensional ones by admitting tuples of integer-typed functions. The syntax of a multidimensional decrease clause is __CPROVER_decreases(f1, ..., fn). We use the lexicographic order to compare two tuples.

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-07-19T20:31:54Z

Codecov Report

Merging #6236 (36f661e) into develop (0002950) will increase coverage by 8.77%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #6236      +/-   ##
===========================================
+ Coverage    67.40%   76.18%   +8.77%     
===========================================
  Files         1157     1478     +321     
  Lines        95236   161669   +66433     
===========================================
+ Hits         64197   123165   +58968     
- Misses       31039    38504    +7465

Flag	Coverage Δ
cproversmt2	`?`
regression	`?`
unit	`?`

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/util/string_container.cpp	`52.94% <0.00%> (-47.06%)`	⬇️
src/solvers/prop/prop.cpp	`42.85% <0.00%> (-41.76%)`	⬇️
src/solvers/flattening/boolbv_member.cpp	`53.65% <0.00%> (-38.65%)`	⬇️
src/cpp/cpp_storage_spec.cpp	`65.00% <0.00%> (-35.00%)`	⬇️
src/util/cmdline.h	`66.66% <0.00%> (-33.34%)`	⬇️
src/solvers/strings/array_pool.h	`66.66% <0.00%> (-33.34%)`	⬇️
src/solvers/strings/string_refinement.h	`66.66% <0.00%> (-33.34%)`	⬇️
...rs/strings/string_concatenation_builtin_function.h	`0.00% <0.00%> (-33.34%)`	⬇️
src/cbmc/c_test_input_generator.cpp	`60.00% <0.00%> (-30.33%)`	⬇️
src/analyses/local_cfg.h	`75.00% <0.00%> (-25.00%)`	⬇️
... and 1458 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 03213c1...36f661e. Read the comment docs.

martin-cs

Looks good apart from the code placement issue flagged.

src/util/std_expr.h

SaswatPadhi

Some general comments:

Please remove activate-multi-line-match from .desc files that don't need multi-line regex matching
Please only check regexes specific to the functionality you want to test (i.e. decreases clauses), because the other assertions (and especially their count, like ^.*0 of 5 failed $1 iterations$$) may change in future if we introduce additional default checks.

regression/contracts/variant_multidimensional_nested/test.desc

regression/contracts/variant_multidimensional_not_decreasing_fail/test.desc

SaswatPadhi · 2021-07-20T17:40:51Z

regression/contracts/variant_parsing_multiple_clauses_fail/test.desc

+decreases clause, it should be placed inside a single __CPROVER_decreases(...),
+where each component of the multidimensional decreases clause is separated by a
+comma. Hence, in this test, the correct syntax is 
+__CPROVER_decreases(N - i, 42).


Nice! :) These test.desc files are very well written.

Shouldn't we support multiple decreases clauses in the future?

It's unclear as of now.

__CPROVER_decreases is unlike the other contracts. You can arbitrarily reorder multiple ENSURES, REQUIRES, ASSIGNS, LOOP_INVARIANT clauses, but the order of expressions matters for DECREASES clauses. They are not a conjunction (or a set), but an ordered tuple.

Moreover,

__CPROVER_decreases(X) __CPROVER_decreases(Y)

reads as "both" X and Y monotonically decrease at each iteration, but for termination we simply need either one to monotonically decrease, and this sort of annotation would just be confusing.

src/ansi-c/parser.y

src/goto-instrument/code_contracts.cpp

src/util/std_expr.cpp

src/util/std_expr.h

src/util/std_expr.cpp

kroening · 2021-07-21T06:44:51Z

src/util/std_expr.cpp

+      binary_relation_exprt(small[i], ID_equal, large[i]);
+    consecutive_equalities[i] =
+      and_exprt(consecutive_equalities[i - 1], current_component_equality);
+  }


I would separate the creation of the equalities and the forming of the conjunction. In particular, we have a conjunction(...) helper, which takes exprt::operandst as argument.

If we use conjunction(...) to create conjunctions of equalities of all necessary lengths (i.e. from 1 up to the size of the multidimensional decreases clause), I believe it will take quadratic time in total. Of course, the size of multidimensional decreases clauses is usually small. So the algorithmic performance should not be a concern. Nonetheless, I think it is better to simply traverse the vector and incrementally build conjunctions of equalities, which will take linear time.

src/util/std_expr.cpp

regression/contracts/variant_missing_invariant_warning/test.desc

regression/contracts/variant_multidimensional_ackermann/test.desc

regression/contracts/variant_multidimensional_not_decreasing_fail1/main.c

regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc

regression/contracts/variant_multidimensional_not_decreasing_fail2/main.c

feliperodri · 2021-07-21T17:37:00Z

src/ansi-c/c_typecheck_code.cpp

-    typecheck_expr(variant);
-    implicit_typecast_arithmetic(variant);
+    for(auto &decreases_clause_component :
+        (static_cast<exprt &>(code.add(ID_C_spec_decreases)).operands()))


Are there any guarantees that this cast is safe? Take a look at this comment #5403 (comment).

Good catch. As suggested on the other thread, we should create "safe" accessors at some point.

However, currently, this issue also applies to invariant contracts, so may be we can table this change for a separate future PR and fix both together?

Thanks for the link. For now, I will just leave it as it is. When someone cleans up the code for loop invariants, then we will also clean the code for decreases clauses.

src/util/std_expr.h

src/goto-instrument/contracts/contracts.cpp

SaswatPadhi

Thanks for all the changes!

LGTM with a couple of nitpicks:

src/goto-instrument/contracts/contracts.cpp

feliperodri

Thank you for implementing all comments!

feliperodri · 2021-07-21T22:37:56Z

regression/contracts/variant_multidimensional_ackermann/test.desc

+It tests whether we can prove (only partially) the termination of the Ackermann
+function using a multidimensional decreases clause. 
+
+Note that this particular implementation of the Ackermann function contains
+both a while-loop and recursion. Therefore, to fully prove the termination of 
+the Ackermann function, we must prove both 
+(i) the termination of the while-loop and
+(ii) the termination of the recursion. 
+Because CBMC does not support termination proofs of recursions (yet), we cannot
+prove the latter, but the former. Hence, the termination proof in the code is
+only "partial."
+
+Furthermore, the Ackermann function has a function contract that the result
+is always non-negative. This post-condition is necessary for establishing
+the loop invariant. However, in this test, we do not enforce the function
+contract. Instead, we assume that the function contract is correct and use it
+(i.e. replace a recursive call of the Ackermann function with its contract). 
+
+We cannot verify/enforce the function contract of the Ackermann function, since
+CBMC does not support function contracts for recursively defined functions.
+As of now, CBMC only supports function contracts for non-recursive functions. 


Kudos for your bar-raising test descriptions! @LongPham7

LongPham7 force-pushed the Long_internship branch 6 times, most recently from 30f3be2 to f9f274c Compare July 19, 2021 19:31

martin-cs approved these changes Jul 20, 2021

View reviewed changes

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

SaswatPadhi assigned LongPham7 Jul 20, 2021

SaswatPadhi added aws Bugs or features of importance to AWS CBMC users enhancement labels Jul 20, 2021

SaswatPadhi suggested changes Jul 20, 2021

View reviewed changes

LongPham7 force-pushed the Long_internship branch 3 times, most recently from a801204 to 31fe7de Compare July 20, 2021 21:28

SaswatPadhi marked this pull request as ready for review July 20, 2021 23:18

SaswatPadhi requested review from chrisr-diffblue, feliperodri, kroening, peterschrammel and tautschnig as code owners July 20, 2021 23:18

kroening reviewed Jul 21, 2021

View reviewed changes

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

kroening reviewed Jul 21, 2021

View reviewed changes

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

kroening reviewed Jul 21, 2021

View reviewed changes

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

kroening reviewed Jul 21, 2021

View reviewed changes

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

LongPham7 force-pushed the Long_internship branch 3 times, most recently from bc56169 to 41a0198 Compare July 21, 2021 14:48

feliperodri requested changes Jul 21, 2021

View reviewed changes

feliperodri added the Code Contracts Function and loop contracts label Jul 21, 2021

LongPham7 force-pushed the Long_internship branch 3 times, most recently from 3ad043a to 048d022 Compare July 21, 2021 20:54

SaswatPadhi approved these changes Jul 21, 2021

View reviewed changes

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

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

Multidimensional decreases clauses

36f661e

LongPham7 force-pushed the Long_internship branch from 048d022 to 36f661e Compare July 21, 2021 21:52

feliperodri self-requested a review July 21, 2021 22:36

feliperodri approved these changes Jul 21, 2021

View reviewed changes

chrisr-diffblue approved these changes Jul 22, 2021

View reviewed changes

feliperodri merged commit 5592d7e into diffblue:develop Jul 22, 2021

Multidimensional decreases clauses #6236

Multidimensional decreases clauses #6236

Uh oh!

Conversation

LongPham7 commented Jul 19, 2021

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

martin-cs left a comment

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!

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!

Uh oh!

Uh oh!

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!

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!

SaswatPadhi left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

codecov bot commented Jul 19, 2021 •

edited

Loading