New goto checker interfaces [blocks: 3579] #3564

peterschrammel · 2018-12-12T11:07:05Z

This will replace safety_checkert and property_checkert, and become the basis for breaking up the bmct monolith.
Based on #3557. Review only last commit.

I'm not happy with the naming of goto_checkert, which doesn't intuitively describe what it is doing - hoping for better suggestions from the reviewers.

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.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: c54e65f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94498702
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 1968915).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/94899319
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

romainbrenguier

Some naming suggestions, otherwise looks fine

romainbrenguier · 2018-12-17T10:10:15Z

src/goto-checker/goto_checker.h

+  /// subsequent call to operator().
+  /// `goto_checkert` derivatives shall be implemented in a way such
+  /// that repeated calls to operator() shall return the next FAILed
+  /// property until eventually not returning any FAILing properties.


This last sentence is not clear, since the operator does not return a property.
And this sounds like something we would want to be enforced by the interface.

romainbrenguier · 2018-12-17T11:36:52Z

src/goto-checker/goto_verifier.h

+/// a goto model. It typically uses, but doesn't have to use, a
+/// `goto_checkert` to iteratively determine the verification result
+/// of each property.
+class goto_verifiert


I think checker and verifier can easily be confused and the difference in meaning is not clear. I also can't find a very good naming for this two classes. Maybe this class is the one that should be goto_checker and the other one could be named something like incremental_goto_checker? since it's only checking until the next counter-example is found.

+1 - I also believe, but am not really sure, that the incremental nature is the difference? If this is correct, then the naming proposed by @romainbrenguier seems good; if it isn't, then the documentation needs to be revisited.

Going with incremental_goto_checkert due to lack of more intuitive names.

romainbrenguier · 2018-12-17T11:43:37Z

src/goto-checker/properties.cpp

+propertiest initialize_properties(const abstract_goto_modelt &goto_model)
+{
+  propertiest properties;
+  forall_goto_functions(it, goto_model.get_goto_functions())


⛏️ an ranged-for would be preferred here, to make explicit that it is used just to access the data and not for other iterator operations. 🐇

romainbrenguier · 2018-12-17T11:49:05Z

src/goto-checker/properties.cpp

+
+        const source_locationt &source_location = i_it->source_location;
+
+        irep_idt property_id = source_location.get_property_id();


⛏️ intermediary variable source_location is superfluous

romainbrenguier · 2018-12-17T11:49:14Z

src/goto-checker/properties.cpp

+
+        const source_locationt &source_location = i_it->source_location;
+
+        irep_idt property_id = source_location.get_property_id();


should be const

romainbrenguier · 2018-12-17T11:51:43Z

src/goto-checker/properties.h

+struct property_infot
+{
+  /// A pointer to the corresponding goto instruction
+  goto_programt::const_targett location;


The naming is a bit confusing as I would expect location to be a source_locationt. Could it be renamed to something like instruction_pointer?

Going with pc which is used in other classes such as goto_tracet.

src/goto-checker/goto_checker.h

src/goto-checker/goto_verifier.h

tautschnig · 2018-12-17T12:32:54Z

src/goto-checker/goto_checker.h

+/// the state of the analysis that it performs (e.g. goto-symex, solver, etc).
+/// It is not responsible for maintaining outcomes (e.g. property results,
+/// counterexamples, etc). However, an implementation may restrict the
+/// sets of properties it is asked to check (e.g. only sequences of subsets).


"subsets" of what?

Please check whether it's clearer now.

tautschnig · 2018-12-17T12:33:57Z

src/goto-checker/goto_checker.h

+/// one by one to the caller.
+/// An implementation of `goto_checkert` is responsible for maintaining
+/// the state of the analysis that it performs (e.g. goto-symex, solver, etc).
+/// It is not responsible for maintaining outcomes (e.g. property results,


Does "It" refer to the implementation? I'd use "An implementation of goto_checkert is not responsible for maintaining outcomes ..."

tautschnig · 2018-12-17T12:37:37Z

src/goto-checker/goto_verifier.h

+/// a goto model. It typically uses, but doesn't have to use, a
+/// `goto_checkert` to iteratively determine the verification result
+/// of each property.
+class goto_verifiert


+1 - I also believe, but am not really sure, that the incremental nature is the difference? If this is correct, then the naming proposed by @romainbrenguier seems good; if it isn't, then the documentation needs to be revisited.

smowton · 2018-12-17T13:44:41Z

src/goto-checker/goto_checker.h

+  {
+    /// The goto checker may be able to determine the results for more
+    /// properties if operator() is called again.
+    HAVE_MORE,


PARTIAL_RESULT?

smowton · 2018-12-17T14:13:37Z

src/goto-checker/goto_checker.h

+  };
+
+  /// Check whether the given properties with status UNKNOWN or newly
+  /// discovered properties hold


Newly discovered by the checker or by the caller?

Both, unfortunately.

Suggest adding that to the comment then

smowton · 2018-12-17T14:15:27Z

src/goto-checker/goto_checker.h

+  /// After returning DONE, another call to operator() with the same
+  /// properties will return DONE and leave the properties' results unchanged.
+  /// If there is a property with status FAIL then its counterexample
+  /// can be retrieved by calling `build_error_trace` before any


This sounds like it binds an implementation into an odd stateful implementation, how about just passing a boolean to operator() to indicate whether you want traces built or not?

That will not make it less stateful if you still have to call a function to retrieve the trace.

A bool should_build_trace together with optional<goto_tracet> has the problem of what to return when not buildlng a trace and the status is HAVE_MORE... an empty trace?

One could have two operators: one that returns optional<goto_tracet> and another one that returns a status. The caller can pick which one to use depending on whether they want traces or not.

I was envisaging something like std::pair<statust, optionalt<tracet>>, but option 3 sounds pretty good to me

Hm... having to decide whether I want a trace or not before actually knowing which property failed is a limitation for certain algorithms (e.g. synthesising invariants while checking properties: I don't need a counterexample when I fail due to a non-inductive invariant candidate, but I'd like to have the counterexample when a property fails).
So, I think the two operations should be separate. I'm not worried about the statefulness because it is quite natural.

smowton · 2018-12-17T14:17:49Z

src/goto-checker/properties.h

+/// The result status of a property
+enum class property_resultt
+{
+  /// The property was not reached (also used for initialization)


Not reached yet, I guess -- what's the difference between this and UNKNOWN?

It would rather be for unreachable assertions (for instance in methods that are loaded but not called from the entry point)

That seems the same as NOT_REACHABLE. Perhaps they should be NOT_REACHABLE and NOT_SATISFIABLE (can get there, but can't concurrently satisfy the condition)?

I'll add examples to clarify these notions.

Assume we run a path-symex that does at most 5 unwindings and stops
before exploring the else branch (*).

int main(int argc, char **argv) { if(argc < 0) assert(0); // NOT_REACHABLE assert(argc >= 0); // PASS if(argc < 5) { for(int i=0; i<10; i++) { assert(i == 2) // FAIL assert(i != 15); // UNKNOWN } } else // (*) { assert(0); // NOT_REACHED } }

How about NOT_REACHED -> NOT_CHECKED? NOT_REACHED and NOT_REACHABLE are so close to synonyms it will surely confuse.

smowton · 2018-12-17T14:20:15Z

Re: naming both the checker and the verifier sound like they might be checking internal consistency of a GOTO program, rather than checking whether its assertions can be violated. Like Romain though I don't have a better idea.

allredj

It would be good to apply Romain's comments, especially about the ranged for.

allredj · 2018-12-17T12:48:03Z

src/goto-checker/goto_checker.h

+  /// Check whether the given properties with status UNKNOWN or newly
+  /// discovered properties hold
+  /// \param [out] properties: Updates those properties whose
+  ///   results have been determined. Newly discovered properties are added.


⛏️ Argument descriptions should talk about the arguments themselves, not the function. Maybe rephrase to:
Properties updated to whether their results have been determined.

allredj · 2018-12-17T12:56:28Z

src/goto-checker/goto_checker.h

+  /// property until eventually not returning any FAILing properties.
+  virtual statust operator()(propertiest &properties) = 0;
+
+  /// This builds and returns the counterexample


⛏️ Redundant This

allredj · 2018-12-17T13:17:37Z

src/goto-checker/properties.cpp

+  UNREACHABLE;
+}
+
+/// Returns the properties in the goto model


⛏️ Returns -> Return

⛏️ And perhaps document that this function also initialises the properties (it's clear from the name, but it's confusing that the documentation doesn't match the function name).

allredj · 2018-12-17T16:00:35Z

src/goto-checker/properties.cpp

+  propertiest properties;
+  forall_goto_functions(it, goto_model.get_goto_functions())
+  {
+    if(!it->second.is_inlined() || it->first == goto_functionst::entry_point())


⛏️ Maybe document why we exclude all inlined functions except the entry point?

This is a good question. It seems legacy to me and we should be able to remove this filter.
The first condition used to be necessary in times where goto_partial_inline was used.
The second condition is unclear to me (is the entry point marked inlined?). @kroening, @tautschnig, any insights?

If the entry point were marked as inlined that would just seem wrong (and useless) to me. I'd suggest to remove this second part of the condition.

tautschnig · 2019-01-09T17:50:39Z

@peterschrammel Please send a ping when this one is ready for (re-)review.

peterschrammel · 2019-01-12T18:47:47Z

Please send a ping when this one is ready for (re-)review.

ping

tautschnig · 2019-01-12T19:14:33Z

src/goto-checker/goto_verifier.h

+
+/// An implementation of `goto_verifiert` checks all properties in
+/// a goto model. It typically uses, but doesn't have to use, a
+/// `goto_checkert` to iteratively determine the verification result


Should this be incremental_goto_checkert?

tautschnig · 2019-01-12T19:15:35Z

src/goto-checker/goto_verifier.h

+  {
+    return properties;
+  }
+


Needs a virtual ~goto_verifiert() = default;

tautschnig · 2019-01-12T19:21:03Z

src/goto-checker/incremental_goto_checker.cpp

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Goto Checker Interface


Nit-pick: add "Incremental"

tautschnig · 2019-01-12T19:21:40Z

src/goto-checker/incremental_goto_checker.h

+    FOUND_FAIL,
+    /// The goto checker has returned all results for the given set
+    /// of properties.
+    DONE


So what's the initial status to use then?

Why would you need an initial status?

There always has to be some "status" - otherwise it's a "result" I'd say?

Made naming of result vs status more consistent

tautschnig · 2019-01-12T19:22:44Z

src/goto-checker/incremental_goto_checker.h

+  virtual statust operator()(propertiest &properties) = 0;
+
+  /// Builds and returns the counterexample
+  virtual goto_tracet build_error_trace() const = 0;


Do we have move operators so that we can reasonably pass a goto_tracet by value?

Should be implicit

tautschnig · 2019-01-12T19:24:19Z

src/goto-checker/properties.cpp

+  for(const auto &function_pair : goto_functions.function_map)
+  {
+    if(!function_pair.second.is_inlined() ||
+      function_pair.first == goto_functionst::entry_point())


See comment on the earlier version: the second condition should be removed.

tautschnig · 2019-01-12T19:26:20Z

src/goto-checker/properties.cpp

+        property_infot &property =
+          properties[i_it->source_location.get_property_id()];
+        property.result = property_resultt::NOT_CHECKED;
+        property.pc = i_it;


A property_infot should have a constructor so that we can do
properties.emplace(i_it->source_location.get_property_id(), {property_resultt::NOT_CHECKED, i_it}); here.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: f1f62b2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97146777

incremental_goto_checkert: returns a trace or 'done' goto_verifiert: uses incremental_goto_checkert to check a set of properties property utilities

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: a1100e1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97160722

peterschrammel requested review from cesaro, chrisr-diffblue, cristina-david, kroening, pkesseli, smowton and tautschnig as code owners December 12, 2018 11:07

peterschrammel force-pushed the goto-checker-interfaces branch 2 times, most recently from 91f3b5b to c54e65f Compare December 12, 2018 13:37

allredj reviewed Dec 12, 2018

View reviewed changes

peterschrammel added the do not merge label Dec 12, 2018

peterschrammel assigned romainbrenguier Dec 12, 2018

peterschrammel mentioned this pull request Dec 12, 2018

Rip out the heart of bmct [depends: 3557, blocks: 3578, 3580, 3581] #3565

Merged

7 tasks

peterschrammel changed the title ~~New goto checker interfaces~~ New goto checker interfaces [blocks 3565] Dec 12, 2018

peterschrammel added the blocker label Dec 12, 2018

peterschrammel force-pushed the goto-checker-interfaces branch from c54e65f to d21bdf2 Compare December 16, 2018 16:24

peterschrammel changed the title ~~New goto checker interfaces [blocks 3565]~~ New goto checker interfaces [depends: 3557] Dec 16, 2018

peterschrammel added dependent - do not merge do not merge and removed do not merge blocker labels Dec 16, 2018

peterschrammel mentioned this pull request Dec 16, 2018

Add witness output to goto checker [blocks: 3583] #3579

Merged

7 tasks

peterschrammel changed the title ~~New goto checker interfaces [depends: 3557]~~ New goto checker interfaces [depends: 3557, blocks: 3579] Dec 16, 2018

peterschrammel added the blocker label Dec 16, 2018

peterschrammel force-pushed the goto-checker-interfaces branch from d21bdf2 to 1968915 Compare December 16, 2018 17:12

allredj reviewed Dec 16, 2018

View reviewed changes

peterschrammel added the Goto-checker label Dec 16, 2018

peterschrammel assigned smowton and tautschnig Dec 17, 2018

peterschrammel assigned kroening Dec 17, 2018

romainbrenguier approved these changes Dec 17, 2018

View reviewed changes

tautschnig reviewed Dec 17, 2018

View reviewed changes

tautschnig assigned peterschrammel and unassigned tautschnig and romainbrenguier Dec 17, 2018

smowton reviewed Dec 17, 2018

View reviewed changes

allredj approved these changes Dec 17, 2018

View reviewed changes

peterschrammel removed the dependent - do not merge label Jan 5, 2019

peterschrammel changed the title ~~New goto checker interfaces [depends: 3557, blocks: 3579]~~ New goto checker interfaces [blocks: 3579] Jan 9, 2019

peterschrammel force-pushed the goto-checker-interfaces branch from 1968915 to e209fce Compare January 12, 2019 18:41

tautschnig approved these changes Jan 12, 2019

View reviewed changes

tautschnig unassigned smowton and kroening Jan 12, 2019

peterschrammel force-pushed the goto-checker-interfaces branch from e209fce to f1f62b2 Compare January 12, 2019 23:08

allredj reviewed Jan 13, 2019

View reviewed changes

peterschrammel force-pushed the goto-checker-interfaces branch from f1f62b2 to badcae8 Compare January 13, 2019 10:36

Introduce goto checker interfaces

a1100e1

incremental_goto_checkert: returns a trace or 'done' goto_verifiert: uses incremental_goto_checkert to check a set of properties property utilities

peterschrammel force-pushed the goto-checker-interfaces branch from badcae8 to a1100e1 Compare January 13, 2019 10:37

allredj reviewed Jan 13, 2019

View reviewed changes

peterschrammel merged commit bbfd361 into diffblue:develop Jan 13, 2019

peterschrammel deleted the goto-checker-interfaces branch January 13, 2019 13:36


		const source_locationt &source_location = i_it->source_location;

		irep_idt property_id = source_location.get_property_id();

		@@ -0,0 +1,21 @@
		/*******************************************************************\

		Module: Goto Checker Interface

New goto checker interfaces [blocks: 3579] #3564

New goto checker interfaces [blocks: 3579] #3564

Uh oh!

Conversation

peterschrammel commented Dec 12, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier left a comment

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!

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!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

peterschrammel Jan 12, 2019 • 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!

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!

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!

Choose a reason for hiding this comment

Uh oh!

peterschrammel Dec 17, 2018 • 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!

peterschrammel Dec 17, 2018 • 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!

smowton commented Dec 17, 2018

Uh oh!

allredj left a comment

peterschrammel Jan 12, 2019 •

edited

Loading

peterschrammel Dec 17, 2018 •

edited

Loading

peterschrammel Dec 17, 2018 •

edited

Loading