goto instrumentation for decreases clauses on loops #6197

LongPham7 · 2021-06-24T17:26:20Z

This pull request contains the full-fledged implementation of one-dimensional loop variants (also known as ranking functions). A loop variant is an integer expression (i) that is bounded below and (ii) strictly decreases after each iteration of a loop. We use loop variants to prove termination of loops.

A loop variant in C is converted to the following statements in the GOTO language:

Declarations of two temporary variables
Assign a loop variant to the first temporary variable at the "beginning" of a loop body
Assign a loop variant to the second temporary variable at the "end" of a loop body
Assert that the second temporary variable < first temporary variable
Discard the two temporary variables by the "dead" statements in the GOTO language.

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-06-24T19:08:24Z

Codecov Report

Merging #6197 (fa9bb89) into develop (0002950) will increase coverage by 7.50%.
The diff coverage is n/a.

❗ Current head fa9bb89 differs from pull request most recent head 00608b6. Consider uploading reports for the commit 00608b6 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6197      +/-   ##
===========================================
+ Coverage    67.40%   74.91%   +7.50%     
===========================================
  Files         1157     1456     +299     
  Lines        95236   161233   +65997     
===========================================
+ Hits         64197   120792   +56595     
- Misses       31039    40441    +9402

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/ansi-c/c_typecheck_base.cpp	`54.39% <0.00%> (-26.51%)`	⬇️
... and 1435 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 a7d4c3d...00608b6. Read the comment docs.

SaswatPadhi

Some initial comments below, and could you please:

fix the formatting issues? (see the build failures for details)
change the message Compare the old and new variant values to Check that loop variant monotonically decreases?

src/goto-programs/goto_program.h

src/goto-programs/goto_convert.cpp

src/goto-instrument/code_contracts.h

src/goto-instrument/code_contracts.cpp

src/goto-programs/goto_program.cpp

src/goto-instrument/code_contracts.cpp

src/goto-programs/goto_program.cpp

src/goto-instrument/code_contracts.cpp

martin-cs

Looks good apart from the things flagged.

src/goto-instrument/code_contracts.cpp

martin-cs · 2021-06-27T13:01:49Z

src/goto-instrument/code_contracts.cpp

+    // Generate: an assignment to store the loop variant before the loop entry
+    code_assignt old_variant_assignment{old_variant_symbol, variant};
+    old_variant_assignment.add_source_location() = loop_head->source_location;
+    converter.goto_convert(old_variant_assignment, havoc_code, mode);


@tautschnig is this use of goto_convert fitting with how and when / where it is supposed to be used?

regression/contracts/invar_check_multiple_loops/test.desc

SaswatPadhi

Couple of minor comments, but otherwise LGTM! Thanks for all the work!

src/goto-programs/goto_program.cpp

src/goto-programs/goto_convert_class.h

src/goto-programs/goto_convert.cpp

feliperodri

Thank you for tackling all comments!

kroening · 2021-07-02T13:55:17Z

src/goto-instrument/code_contracts.cpp

+      loop_head->source_location;
+    converter.goto_convert(monotonic_decreasing_assertion, havoc_code, mode);
+    havoc_code.instructions.back().source_location.set_comment(
+      "Check monotonicity of decreases clause");


"monotonicity" is perhaps not the right word. It might not be an intuitive description for a broader audience, and being pedantic, you need strict monotonicity to get termination.
How about "ranking function decreases"?

I think "ranking function" might also sound unfamiliar, plus we haven't used ranking function elsewhere (the annotation just reads __CPROVER_decreases).

How about simply, "Check decreases clause on loop iteration"?

Thanks a lot for both of your suggestions. I will change the comment to "Check decreases clause on loop iteration".

kroening · 2021-07-02T13:59:35Z

What should happen when there are multiple __CPROVER_decreases clauses for one loop?
You could make that a lexicographic ranking function.

SaswatPadhi · 2021-07-02T14:53:40Z

What should happen when there are multiple __CPROVER_decreases clauses for one loop?
You could make that a lexicographic ranking function.

Yes, this is a good point. Currently we don't allow multiple invariant and decreases annotations, but my proposal was also to treat multiple decreases clause annotations as tuples that would be compared lexicographically.

LongPham7 force-pushed the Long_internship branch 2 times, most recently from 1422b22 to a0ba201 Compare June 24, 2021 17:54

SaswatPadhi suggested changes Jun 24, 2021

View reviewed changes

SaswatPadhi assigned LongPham7 Jun 24, 2021

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

SaswatPadhi requested a review from feliperodri June 24, 2021 23:05

LongPham7 force-pushed the Long_internship branch 6 times, most recently from 6aa3322 to 002c618 Compare June 25, 2021 15:21

SaswatPadhi suggested changes Jun 25, 2021

View reviewed changes

LongPham7 force-pushed the Long_internship branch 2 times, most recently from 57a9915 to 0a227fb Compare June 25, 2021 22:22

martin-cs approved these changes Jun 27, 2021

View reviewed changes

LongPham7 force-pushed the Long_internship branch 8 times, most recently from 9c7f67b to 28aff8e Compare June 29, 2021 15:23

SaswatPadhi reviewed Jun 30, 2021

View reviewed changes

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

LongPham7 force-pushed the Long_internship branch 2 times, most recently from c86f3f4 to 17e3e0a Compare June 30, 2021 15:24

SaswatPadhi approved these changes Jun 30, 2021

View reviewed changes

src/goto-programs/goto_program.cpp Outdated Show resolved Hide resolved

src/goto-programs/goto_convert_class.h Outdated Show resolved Hide resolved

src/goto-programs/goto_convert.cpp Outdated Show resolved Hide resolved

SaswatPadhi changed the title ~~Full implementation of loop variants (aka ranking functions)~~ goto instrumentation for decreases clauses on loops Jun 30, 2021

LongPham7 force-pushed the Long_internship branch 3 times, most recently from 008519a to 99540f5 Compare June 30, 2021 16:10

SaswatPadhi marked this pull request as ready for review June 30, 2021 16:34

SaswatPadhi requested review from kroening, peterschrammel and tautschnig as code owners June 30, 2021 16:34

feliperodri approved these changes Jul 1, 2021

View reviewed changes

kroening reviewed Jul 2, 2021

View reviewed changes

kroening approved these changes Jul 2, 2021

View reviewed changes

Full implementation of loop variants

00608b6

LongPham7 force-pushed the Long_internship branch from 99540f5 to 00608b6 Compare July 2, 2021 16:51

SaswatPadhi merged commit 3e0007f into diffblue:develop Jul 2, 2021

goto instrumentation for decreases clauses on loops #6197

goto instrumentation for decreases clauses on loops #6197

Uh oh!

Conversation

LongPham7 commented Jun 24, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

Codecov Report

Uh oh!

SaswatPadhi 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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

martin-cs Jun 27, 2021

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!

Uh oh!

feliperodri left a comment

Choose a reason for hiding this comment

Uh oh!

kroening Jul 2, 2021

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi Jul 2, 2021

Choose a reason for hiding this comment

Uh oh!

LongPham7 Jul 2, 2021

Choose a reason for hiding this comment

Uh oh!

kroening commented Jul 2, 2021

Uh oh!

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

Uh oh!

Uh oh!

Uh oh!

LongPham7 commented Jun 24, 2021 •

edited

Loading

codecov bot commented Jun 24, 2021 •

edited

Loading

SaswatPadhi commented Jul 2, 2021 •

edited

Loading