CONTRACTS: Documenting semantic of loop invariant synthesizers #7089

qinheping · 2022-08-31T07:40:58Z

This PR contains only documentations. It explain the semantic of the loop-invariant synthesizer interface and the enumerative synthesizer. The motivating discussion is in the PR#7007.

Yes, my original goals of this enumerative_loop_invariant_synthesizert were the scale B: synthesis with guarantees/hard constraints. You are right that there can be varied guarantees other than only B---all checks success.
So I think for the base class, we only expect the returned exprt are loop invariants in the sense that

the instrumented loop invariant checks success no matter other assertions fail or success---so we just ignore even if an assertion is false in the loop;

the base-case is from the whole program with a main function as entry.

Derived classes can have their own guarantees. Each derived class should specify what the users can expect about the returned loop invariants. And users can choose which synthesizer to use with options under the --synthesize-loop-invariants flag.

codecov · 2022-08-31T08:48:57Z

Codecov Report

Base: 77.86% // Head: 77.88% // Increases project coverage by +0.02% 🎉

Coverage data is based on head (83b85eb) compared to base (787b3c1).
Patch coverage: 89.28% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7089      +/-   ##
===========================================
+ Coverage    77.86%   77.88%   +0.02%     
===========================================
  Files         1574     1576       +2     
  Lines       181363   181855     +492     
===========================================
+ Hits        141223   141644     +421     
- Misses       40140    40211      +71

Impacted Files	Coverage Δ
src/goto-instrument/contracts/contracts.h	`100.00% <ø> (ø)`
...nthesizer/enumerative_loop_invariant_synthesizer.h	`100.00% <ø> (ø)`
...ment/synthesizer/loop_invariant_synthesizer_base.h	`100.00% <ø> (ø)`
src/goto-instrument/contracts/cfg_info.h	`84.21% <82.35%> (-3.47%)`	⬇️
src/ansi-c/c_expr.h	`100.00% <100.00%> (ø)`
src/ansi-c/c_typecheck_code.cpp	`77.15% <100.00%> (ø)`
src/goto-instrument/contracts/contracts.cpp	`96.29% <100.00%> (+1.97%)`	⬆️
src/cpp/cpp_template_type.h	`52.94% <0.00%> (-11.35%)`	⬇️
src/util/pointer_expr.h	`80.83% <0.00%> (-7.29%)`	⬇️
... and 91 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

feliperodri · 2022-08-31T17:27:56Z

@Herbping @SaswatPadhi @remi-delmas-3000 maybe we should create a folder inside docs named contracts and add all .md files with documentation for code contracts in there instead of keeping adding multiple files with "contracts" prefix. We can then update the CODEOWNERS list of that folder.

doc/cprover-manual/loop-invariant-synthesizer.md

feliperodri · 2022-08-31T17:36:31Z

doc/cprover-manual/loop-invariant-synthesizer.md

+assertions fail or success;
+2. the base-case is from the whole GOTO program with a main 
+function as the entry point.
+


Could you provide an example here?

I find these two points somewhat unclear. An example might help, as Felipe mentioned, especially for point 1.

I would probably just remove point 2. "main function" need not be the entrypoint for CBMC (can be overriden), and the base case is no different from any other symex path -- the path constraint along a path that reaches the loop head is the base case.

It might be worth adding a pointer to semantics of loop invariants (contracts-invariants.md#semantics), which already covers the induction principle.

The first point I want to make here is that we only care about if the invariant is inductive, but not other checks (even if there is assert(0); in the loop). The purpose of the second point is to distinguish: 1) the invariants are inductive for any inputs of the function, and 2) the invariants are inductive for only paths in the given GOTO binary.

As an example, k == 1 is an inductive invariant in the following program. However, it is not always inductive if we only consider the function foo---it doesn't hold when the parameter k is not 1.

void foo(int k) { for(int i = 0; i < 5; i++) { if(k != 1) k = 2; } } void main() { foo(1); }

You are right that the semantics of loop invariants is enough to illustrate the point. I will update the text and add a link to the semantics of loop invariants.

I still few this section needs an example. Take a small program, check the program with pointer checks enable using a bound, synthesize the invariant, check the problem again without the bound. One of the most important part of the documentation is to walk potential users and future developers in the process of how to use this tool.

I like the idea of examples. It would also be good to discuss what the initial state is as part of defining / saying they are inductive.

If the invariants are inferred in the context of a proof harness that does not fully cover the input space of the function that contains the loop, is there a risk that we could assume the invariant in a different context where it could actually not hold without realizing it?
Or would we attempt to re-prove the inferred invariant in each context in which the function that contains the loop gets called ?

It could happen but it should not be silent as the check for whether it is a loop invariant should fail in the new context. I presume we have tests for "__CPROVER_invariant that aren't actually true?

src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h

doc/cprover-manual/loop-invariant-synthesizer.md

SaswatPadhi

Requesting some more clarification on a few things.

SaswatPadhi · 2022-08-31T18:29:38Z

doc/cprover-manual/loop-invariant-synthesizer.md

+assertions fail or success;
+2. the base-case is from the whole GOTO program with a main 
+function as the entry point.
+


I find these two points somewhat unclear. An example might help, as Felipe mentioned, especially for point 1.

I would probably just remove point 2. "main function" need not be the entrypoint for CBMC (can be overriden), and the base case is no different from any other symex path -- the path constraint along a path that reaches the loop head is the base case.

It might be worth adding a pointer to semantics of loop invariants (contracts-invariants.md#semantics), which already covers the induction principle.

doc/cprover-manual/loop-invariant-synthesizer.md

feliperodri · 2022-09-01T18:59:09Z

src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h

-/// It handles `goto_model` containing only checks instrumented by
-/// `goto-instrument` with the `--pointer-check` flag.
+/// It is designed for `goto_model` containing only checks instrumented by
+/// `goto-instrument` with the `--pointer-check` flag. H


Suggested change

/// `goto-instrument` with the `--pointer-check` flag. H

/// `goto-instrument` with the `--pointer-check` flag.

Mistakenly marked as resolved?

doc/cprover-manual/loop-invariant-synthesizer.md

feliperodri · 2022-09-01T19:21:40Z

doc/cprover-manual/loop-invariant-synthesizer.md

+assertions fail or success;
+2. the base-case is from the whole GOTO program with a main 
+function as the entry point.
+


I still few this section needs an example. Take a small program, check the program with pointer checks enable using a bound, synthesize the invariant, check the problem again without the bound. One of the most important part of the documentation is to walk potential users and future developers in the process of how to use this tool.

tautschnig · 2022-09-02T09:12:23Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1146,7 +1146,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
    goto_model.goto_functions.update();
  }

-  if(cmdline.isset("synthesize-loop-invariants"))
+  if(cmdline.isset("synthesize-loop-invariants-enumerative"))


It seems this commit has more than just "documentation?" I'd recommend to factor out the actual code changes into a commit of their own, even if that makes it just a 3-or-so lines commit.

+1 what @tautschnig says.

doc/cprover-manual/loop-invariant-synthesizer.md

tautschnig · 2022-09-02T09:29:09Z

doc/cprover-manual/loop-invariant-synthesizer.md

+This is a loop invariant synthesizer built in goto-instrument that 
+synthesize [loop invariants](contracts-invariants.md) for a 
+pre-existing GOTO binary, annotate the invariant clause into 
+the GOTO binary, and produce an annotated binary as output.


Is it really most important to talk about goto-instrument here? I'd expect that users first want to know a sentence about what loop invariants are (and, specifically, what kinds of loop invariants are being synthesized - inductive ones?), and then what capabilities/limitations this synthesizer has (it's an undecidable problem).

martin-cs · 2022-09-02T13:42:41Z

doc/cprover-manual/loop-invariant-synthesizer.md

+assertions fail or success;
+2. the base-case is from the whole GOTO program with a main 
+function as the entry point.
+


I like the idea of examples. It would also be good to discuss what the initial state is as part of defining / saying they are inductive.

martin-cs · 2022-09-02T13:43:54Z

doc/cprover-manual/loop-invariant-synthesizer.md

+
+Strategy         | Flag                                           | Guarantees
+-----------------|------------------------------------------------|----
+Enumerative      | --synthesize-loop-invariants-enumerative       | All checks will succeeded in the annotated GOTO binary


What happens if the asserts (I presume that is what you mean by checks) are false?

martin-cs · 2022-09-02T13:45:12Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1146,7 +1146,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
    goto_model.goto_functions.update();
  }

-  if(cmdline.isset("synthesize-loop-invariants"))
+  if(cmdline.isset("synthesize-loop-invariants-enumerative"))


+1 what @tautschnig says.

martin-cs · 2022-09-02T13:46:07Z

src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h

-/// It handles `goto_model` containing only checks instrumented by
-/// `goto-instrument` with the `--pointer-check` flag.
+/// It is designed for `goto_model` containing only checks instrumented by
+/// `goto-instrument` with the `--pointer-check` flag. H


Mistakenly marked as resolved?

kroening · 2022-09-02T16:07:58Z

On the manual: Please keep in mind that the "CPROVER Manual" is meant to be a beginners' tutorial, and not a reference manual. May I suggest finding a different place for documenting this functionality.

tautschnig · 2022-09-02T20:09:40Z

On the manual: Please keep in mind that the "CPROVER Manual" is meant to be a beginners' tutorial, and not a reference manual. May I suggest finding a different place for documenting this functionality.

Perhaps we could move the entire contracts-related documentation from that manual to the man pages? I would rather not see us open yet another place that users need to go to in order to find documentation.

feliperodri · 2022-09-02T20:15:37Z

On the manual: Please keep in mind that the "CPROVER Manual" is meant to be a beginners' tutorial, and not a reference manual. May I suggest finding a different place for documenting this functionality.

Perhaps we could move the entire contracts-related documentation from that manual to the man pages? I would rather not see us open yet another place that users need to go to in order to find documentation.

I agree with @tautschnig about not creating another place that users need to go to. However, I think the CPROVER Documentation generated using Doxygen would be a better place than the man pages, right?

qinheping · 2022-09-02T21:41:46Z

On the manual: Please keep in mind that the "CPROVER Manual" is meant to be a beginners' tutorial, and not a reference manual. May I suggest finding a different place for documenting this functionality.

Perhaps we could move the entire contracts-related documentation from that manual to the man pages? I would rather not see us open yet another place that users need to go to in order to find documentation.

I think we can put the semantic, syntax, and usage of contracts in the CPROVER Documentation generated using Doxygen as Felipe suggested; and put the tutorial and examples in the CBMC training material . We may also want to point to the training material from the reference manual so that users can find them easily.

feliperodri · 2022-09-06T15:58:38Z

On the manual: Please keep in mind that the "CPROVER Manual" is meant to be a beginners' tutorial, and not a reference manual. May I suggest finding a different place for documenting this functionality.

Perhaps we could move the entire contracts-related documentation from that manual to the man pages? I would rather not see us open yet another place that users need to go to in order to find documentation.

I think we can put the semantic, syntax, and usage of contracts in the CPROVER Documentation generated using Doxygen as Felipe suggested; and put the tutorial and examples in the CBMC training material . We may also want to point to the training material from the reference manual so that users can find them easily.

@jimgrundy @markrtuttle @SaswatPadhi @nwetzler any recommendations?

martin-cs · 2022-09-07T11:30:26Z

Linking to #7006

qinheping · 2022-09-26T16:33:56Z

This PR now contains only code comments explaining the semantic of the synthesizer. I will put the manual parts to the cbmc-documentation.
Can this PR be merged at this moment? @feliperodri @tautschnig

feliperodri

LGTM.

Comments have been addressed

feliperodri · 2022-09-28T15:58:27Z

@peterschrammel could you take another look at this PR?

martin-cs

Definitely an improvement, so, merge. I would still like some more extensive documentation and examples but that can be another PR>

qinheping requested review from martin-cs, chris-ryder, peterschrammel, kroening and tautschnig as code owners August 31, 2022 07:40

qinheping mentioned this pull request Aug 31, 2022

CONTRACTS: New classes for loop-invariant-synthesizer interface #7007

Merged

feliperodri added aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Aug 31, 2022

feliperodri added the documentation label Aug 31, 2022

feliperodri requested changes Aug 31, 2022

View reviewed changes

feliperodri requested a review from SaswatPadhi August 31, 2022 17:44

feliperodri added Synthesis Invariant synthesis and removed Code Contracts Function and loop contracts labels Aug 31, 2022

SaswatPadhi previously requested changes Aug 31, 2022

View reviewed changes

SaswatPadhi assigned qinheping Aug 31, 2022

qinheping force-pushed the manual-loop-invariant-synthesizer branch from 85bf8c2 to 3864e9e Compare September 1, 2022 17:48

feliperodri requested changes Sep 1, 2022

View reviewed changes

tautschnig self-assigned this Sep 2, 2022

tautschnig reviewed Sep 2, 2022

View reviewed changes

tautschnig removed their assignment Sep 2, 2022

martin-cs reviewed Sep 2, 2022

View reviewed changes

qinheping force-pushed the manual-loop-invariant-synthesizer branch from 3864e9e to bf6ba31 Compare September 2, 2022 20:16

Documenting semantic of loop invariant synthesizers

83b85eb

qinheping force-pushed the manual-loop-invariant-synthesizer branch from bf6ba31 to 83b85eb Compare September 26, 2022 16:29

feliperodri approved these changes Sep 26, 2022

View reviewed changes

nwetzler approved these changes Sep 28, 2022

View reviewed changes

tautschnig assigned peterschrammel and martin-cs and unassigned qinheping Sep 28, 2022

martin-cs approved these changes Sep 29, 2022

View reviewed changes

martin-cs merged commit 941a2c5 into diffblue:develop Sep 29, 2022

qinheping deleted the manual-loop-invariant-synthesizer branch January 18, 2023 21:54

qinheping restored the manual-loop-invariant-synthesizer branch January 18, 2023 21:54

qinheping deleted the manual-loop-invariant-synthesizer branch January 18, 2023 21:54

	/// `goto-instrument` with the `--pointer-check` flag. H
	/// `goto-instrument` with the `--pointer-check` flag.

CONTRACTS: Documenting semantic of loop invariant synthesizers #7089

CONTRACTS: Documenting semantic of loop invariant synthesizers #7089

Uh oh!

Conversation

qinheping commented Aug 31, 2022

Uh oh!

codecov bot commented Aug 31, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

feliperodri commented Aug 31, 2022

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

qinheping Sep 1, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

remi-delmas-3000 Sep 2, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

SaswatPadhi left a comment

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

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!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kroening commented Sep 2, 2022

Uh oh!

tautschnig commented Sep 2, 2022

Uh oh!

feliperodri commented Sep 2, 2022

Uh oh!

qinheping commented Sep 2, 2022

Uh oh!

feliperodri commented Sep 6, 2022

Uh oh!

martin-cs commented Sep 7, 2022

Uh oh!

codecov bot commented Aug 31, 2022 •

edited

Loading

qinheping Sep 1, 2022 •

edited

Loading

remi-delmas-3000 Sep 2, 2022 •

edited

Loading