Add a structured verification results class in the C++ API #7538

NlightNFotis · 2023-02-15T10:08:12Z

One-sentence Description

This PR is adding the capacity to the C++ API to provide the end-results of a verification engine run to a client in a structured format.

Review Guidance

The gist of this change is the addition of the libcprover-cpp/verification_result.h file, along with the associated infrastructure in all_properties_verifier_with_trace_storaget class (moving the traces from the verifier at the end of the verification engine run).
This was initially added in src/goto-checker/, but offline discussion with @peterschrammel identified that as a potentially disruptive change. It was then decided to move this closer to more experimental code in the C++ api, rather than keep it close to the solvers.
To support testing of this new capacity, a new helper function has been added in testing-utils/run_verification_engine.h - it clones the functionality of the C++ API verify_model() function with the aim to quickly do a verification engine run in a convenient package and produce back the verification results that we expect from the engine.

Checklist

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 · 2023-02-15T11:09:03Z

Codecov Report

Patch coverage: 92.79% and project coverage change: -0.15 ⚠️

Comparison is base (378c902) 78.51% compared to head (7c82b84) 78.37%.

❗ Current head 7c82b84 differs from pull request most recent head 35bf812. Consider uploading reports for the commit 35bf812 to get more accurate results

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7538      +/-   ##
===========================================
- Coverage    78.51%   78.37%   -0.15%     
===========================================
  Files         1671     1674       +3     
  Lines       191848   191938      +90     
===========================================
- Hits        150621   150422     -199     
- Misses       41227    41516     +289

Impacted Files	Coverage Δ
src/libcprover-cpp/api.h	`100.00% <ø> (ø)`
src/libcprover-cpp/verification_result.h	`0.00% <0.00%> (ø)`
src/libcprover-cpp/verification_result.cpp	`86.66% <86.66%> (ø)`
src/libcprover-cpp/api.cpp	`86.00% <95.83%> (+3.10%)`	⬆️
unit/libcprover-cpp/verification_resultt.cpp	`100.00% <100.00%> (ø)`

... and 23 files with indirect coverage changes

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 in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

martin-cs

I hate being That Guy but...

How does this fit with the goto_verifier / properties interface?

https://github.com/diffblue/cbmc/blob/develop/src/goto-checker/goto_verifier.h
https://github.com/diffblue/cbmc/blob/develop/src/goto-checker/properties.h

I know @peterschrammel did some work on setting this up as the future of "unified verification results". I did some work on getting the abstract interpreter to fit with it:

https://github.com/diffblue/cbmc/blob/develop/src/goto-analyzer/static_verifier.h

but it needs more work.

NlightNFotis · 2023-02-15T15:52:36Z

Hi Martin, @martin-cs

The motivation for this is to have an interface from which the API clients will be able to get the results of a run from the verification engine and inspect them.

With regards to goto_verifiert the long term plan is to refactor the operator() to be able to return these structured results (which is really a triple <resultt, propertiest, goto_trace_storaget> - we already have this information and accessors for these in the various subclasses) but this is slightly more involved and I want to build the functionality for the API first, both as a test-bed and as a capability for these APIs, in a non-invasive way.

It's worth mentioning that for now this only exists in one configuration, the one that is used by the test. The next PR will add support for this in the C++ API (under src/libcprover-cpp), and then it's going to be exported to the Rust API.

I need to sort out CI here first and then I will clean up the commit history and also provide some review guidance in the description above as to what changes were made and why.

Update: I have crossed out the part of the text that contains some invalid assumptions of mine after some discussion with Peter. The code will need some rework, so as it stands right now it doesn't reflect the final design.

NlightNFotis · 2023-02-16T16:46:13Z

Update:

I had a discussion with @peterschrammel offline about parts of the design and it contains some defects that I was oblivious too, which renders my previous comment invalid.

This is a change only for all_properties_goto_verifier_with_trace_storaget and can't affect objects from the goto_verifiert hierarchy that don't feature trace storage, so expanding the API of the class to support this would lead to an API design that's confusing.

I will rework the API to move the produce_results() method to the C++ directly rather than augment the interface of that specific verifier.

TGWDB · 2023-02-23T10:25:57Z

Fixes #7499

thomasspriggs

Some initial comments rather than a complete review, given that this likely needs substantial work to deal with this comment -

🚫 API headers must not include internal headers, because this exposes implementation details as part of the public API.

thomasspriggs · 2023-03-01T18:17:22Z

src/libcprover-cpp/api.cpp

-    return;
+    // TODO: Make more robust.
+    // return;
+    INVARIANT(false, "process_goto_program failed");


I think return; on failure was already the correct behaviour, as errors are supposed to be reported via the log variable.

🤨 You gave this a thumbs up but haven't actioned it?

Using INVARIANT here is actually a really bad thing in terms of an API. This is because if the INVARIANT fails it will either abort the whole process which is undesirable if the consumer on the API can recover or it will throw an exception which may not be supported by the ABI being used to interface with the API.

This is no longer relevant, as marked outdated by the GitHub UI itself.

This change has been rolled back in b9b6cc4 - b9b6cc4#diff-122d9d2e65523b48e18239983a025b547f9509d43e638fea6acc71a926daed69R155

This still needs fixing in the produce_results function. This comment was in the verify_model function but the code is duplicated, so the fix needs doing in two places.

Good catch - my bad. I did a pattern replacement to avoid this issue, but for a strange kind of fashion this was missed.

src/libcprover-cpp/api.h

unit/testing-utils/message.h

src/libcprover-cpp/verification_result.h

unit/testing-utils/run_verification_engine.cpp

thomasspriggs · 2023-03-01T19:21:20Z

src/goto-checker/goto_trace_storage.h

+  /// @brief Copy constructor for the goto_trace_storaget class.
+  /// \warning Be advised that goto_traces can be large objects, so
+  ///          copying is not recommended, unless you know what you're doing.
+  goto_trace_storaget(const goto_trace_storaget &) = default;


I am not sure this is a good idea as it could lead to accidental copy construction of goto_trace_storaget which can be an extremely large data structure. Think multiple gigabytes...

See if I can change the class that manages this to be holding a unique pointer which can then be moved.

src/goto-checker/all_properties_verifier_with_trace_storage.h

thomasspriggs · 2023-03-01T19:41:41Z

src/libcprover-cpp/api.cpp

  implementation->message_handler =
    util_make_unique<null_message_handlert>(null_message_handlert{});
  implementation->options = options.to_engine_options();
+  implementation->options->set_option("trace", true);


⛏️ It might be worth adding a comment above this that all_properties_verifier_with_trace_storaget doesn't store traces without this.
🤔 Ultimately, all_properties_verifier_with_trace_storaget is a pretty small class which doesn't fit the needs of the API very well. So we are most likely better off writing our own version of it.

unit/testing-utils/message.h

peterschrammel · 2023-03-02T09:45:23Z

unit/testing-utils/run_verification_engine.cpp

+  return options;
+}
+
+verification_resultt run_verification_engine(goto_modelt &model)


Why doesn't use this the API function to test?

peterschrammel · 2023-03-02T09:47:01Z

src/libcprover-cpp/api.cpp

  verifier.report();
 }

+// TODO: This is a temporary function - it's basically `verify_model`, tweaked


💡 I'd prefer documentation in the .h file because this is where the interface is defined.

This is an actual TODO comment rather than documentation. It is explaining the need for clean-up rather than documenting what the function is supposed to be for. Therefore I would argue that this information belongs in the .cpp rather the header. There is a separate argument that there should be a doxygen block in the header which deprecates this function, explains the difference from the verify_model function and that the verify_model function should be used in preference. The is already a doxygen block in the header.

NlightNFotis · 2023-03-02T11:26:10Z

unit/libcprover-cpp/CMakeLists.txt

 target_include_directories(lib-unit
    PUBLIC
    ${CBMC_SOURCE_DIR}/libcprover-cpp
+    ${CBMC_SOURCE_DIR}/unit/testing-utils


See if it is to be removed - we don't want to expose symbols from the libcproverunit binary.

thomasspriggs · 2023-03-22T11:14:27Z

src/libcprover-cpp/verification_result.h

+class dstringt;
+struct property_infot;
+using propertiest = std::map<dstringt, property_infot>;
+enum class resultt;


⛏️ Seems like quite a generic symbol to introduce into the public global namespace.

thomasspriggs · 2023-03-22T11:20:50Z

src/libcprover-cpp/api.cpp

  verifier.report();
 }

+// TODO: This is a temporary function - it's basically `verify_model`, tweaked


This is an actual TODO comment rather than documentation. It is explaining the need for clean-up rather than documenting what the function is supposed to be for. Therefore I would argue that this information belongs in the .cpp rather the header. There is a separate argument that there should be a doxygen block in the header which deprecates this function, explains the difference from the verify_model function and that the verify_model function should be used in preference. The is already a doxygen block in the header.

thomasspriggs · 2023-03-22T11:28:54Z

src/libcprover-cpp/api.cpp

-    return;
+    // TODO: Make more robust.
+    // return;
+    INVARIANT(false, "process_goto_program failed");


🤨 You gave this a thumbs up but haven't actioned it?

thomasspriggs · 2023-03-22T11:42:13Z

src/goto-checker/all_properties_verifier_with_trace_storage.h

-
 #include "bmc_util.h"
 #include "goto_trace_storage.h"
+#include "goto_verifier.h"


This reformatting appears to be the result of adding and removing things in the process of work on this PR. If you removed all the changes to this file, then you would not need as many code-owners to approve...

src/goto-checker/all_properties_verifier_with_trace_storage.h

thomasspriggs

I think we should fix the inclusion of private headers in the API unit test before merging as a continuation of the fix to avoid including private headers in the public API headers.

thomasspriggs · 2023-03-22T12:03:54Z

unit/testing-utils/module_dependencies.txt

 catch
 goto-programs
 langapi
+libcprover-cpp


I think the functionality related to testing src/libcprover-cpp should live in unit/libcprover-cpp not unit/testing-utils. This is particularly the case with the API, as it is desirable to be able to unit test the API without linking the API unit test binary to the rest of the code base on a #include level.

unit/libcprover-cpp/verification_resultt.cpp

thomasspriggs · 2023-03-22T12:14:05Z

src/libcprover-cpp/verification_result.cpp

+  auto dstringt_property = dstringt(property_id);
+  switch(_impl->get_properties().at(dstringt_property).status)
+  {
+  case property_statust::ERROR:


💡 I suggest making the error case the default case. This will avoid compile errors about reaching the end of non-void functions.

I prefer to keep the UNREACHABLE - this is to communicate intent about this being an exhaustive list.

It also guards against a new enum member being added but not being matched against properly, as it will fail fast and loud.

As I'd previously pointed out in one of my other comments on this PR, the standard INVARIANT / UNREACHABLE macros don't work in a useful fashion in this context. Therefore an alternative means of reporting the error is required. I suggest using a comment if you feel the need to explain the the default case should be unreachable and is therefore an error.

unit/libcprover-cpp/verification_resultt.cpp

thomasspriggs · 2023-03-22T16:53:46Z

src/libcprover-cpp/verification_result.cpp

+{
+}
+
+verification_resultt::~verification_resultt()


⛏️ This should be = default.

src/libcprover-cpp/verification_result.h

thomasspriggs · 2023-03-22T17:00:48Z

src/libcprover-cpp/verification_result.cpp

+#include <string>
+#include <vector>
+
+class verification_resultt::verification_result_implt


🤔 I think you can just make this class a struct, delete all the member functions and just use the fields directly. It would be far more straight-forward.

I'd rather keep the API here as it stands - to be a bit more defensive in case tighter access control (say, some form of translation of the types, or validation) is required in the future (which can be implemented transparently through the property methods).

If that ends up not being needed, the accessor methods should be able to be removed with little effort.

I disagree with your reasoning. "impl" means implementation detail; it is in the name. It shouldn't be intended to be part of the exposed API. Therefore the using a class to add accessibility restrictions to something which is already private by virtue of being declared in the .cpp only is overkill.

This is not a blocking comment, just an observation. So it can be left as-is for the moment if you prefer.

src/libcprover-cpp/verification_result.cpp

NlightNFotis added the do not review label Feb 15, 2023

NlightNFotis self-assigned this Feb 15, 2023

NlightNFotis force-pushed the structured_verification_results branch from 18a949c to d047179 Compare February 15, 2023 10:13

NlightNFotis force-pushed the structured_verification_results branch from 0590884 to 397531d Compare February 15, 2023 14:29

martin-cs reviewed Feb 15, 2023

View reviewed changes

NlightNFotis force-pushed the structured_verification_results branch 3 times, most recently from 2f63c98 to a79cff4 Compare March 1, 2023 15:31

NlightNFotis changed the title ~~Add a structured verification results class~~ Add a structured verification results class in the C++ API Mar 1, 2023

NlightNFotis removed the do not review label Mar 1, 2023

NlightNFotis force-pushed the structured_verification_results branch from a79cff4 to bb88d95 Compare March 1, 2023 15:50

NlightNFotis marked this pull request as ready for review March 1, 2023 15:50

NlightNFotis requested review from TGWDB, esteffin, kroening, peterschrammel, tautschnig and thomasspriggs as code owners March 1, 2023 15:50

thomasspriggs suggested changes Mar 1, 2023

View reviewed changes

peterschrammel reviewed Mar 2, 2023

View reviewed changes

NlightNFotis commented Mar 2, 2023

View reviewed changes

NlightNFotis force-pushed the structured_verification_results branch 3 times, most recently from bd6f91c to dad5fc7 Compare March 8, 2023 11:36

NlightNFotis force-pushed the structured_verification_results branch 2 times, most recently from 5acbb39 to b9b6cc4 Compare March 22, 2023 10:44

thomasspriggs reviewed Mar 22, 2023

View reviewed changes

thomasspriggs suggested changes Mar 22, 2023

View reviewed changes

NlightNFotis force-pushed the structured_verification_results branch from 833c276 to c3b1c4d Compare March 22, 2023 15:05

thomasspriggs reviewed Mar 22, 2023

View reviewed changes

unit/libcprover-cpp/verification_resultt.cpp Outdated Show resolved Hide resolved

thomasspriggs reviewed Mar 22, 2023

View reviewed changes

src/libcprover-cpp/verification_result.h Outdated Show resolved Hide resolved

thomasspriggs reviewed Mar 22, 2023

View reviewed changes

src/libcprover-cpp/verification_result.cpp Outdated Show resolved Hide resolved

NlightNFotis force-pushed the structured_verification_results branch 3 times, most recently from 75392a9 to 7c82b84 Compare March 30, 2023 10:26

thomasspriggs approved these changes Mar 30, 2023

View reviewed changes

Add a verification_resultt class and expose it to the C++ API.

35bf812

NlightNFotis force-pushed the structured_verification_results branch from 7c82b84 to 35bf812 Compare March 31, 2023 09:18

NlightNFotis enabled auto-merge March 31, 2023 10:10

NlightNFotis merged commit c43f13a into diffblue:develop Mar 31, 2023

Add a structured verification results class in the C++ API #7538

Add a structured verification results class in the C++ API #7538

Uh oh!

Conversation

NlightNFotis commented Feb 15, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

One-sentence Description

Review Guidance

Checklist

Uh oh!

codecov bot commented Feb 15, 2023 • 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!

NlightNFotis commented Feb 15, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

NlightNFotis commented Feb 16, 2023

Uh oh!

TGWDB commented Feb 23, 2023

Uh oh!

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

NlightNFotis Mar 22, 2023 • 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!

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!

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!

thomasspriggs Mar 22, 2023 • 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!

thomasspriggs Mar 22, 2023 • 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!

thomasspriggs Mar 22, 2023 • 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!

Uh oh!

thomasspriggs left a comment

Choose a reason for hiding this comment

Uh oh!

NlightNFotis commented Feb 15, 2023 •

edited

Loading

codecov bot commented Feb 15, 2023 •

edited

Loading

NlightNFotis commented Feb 15, 2023 •

edited

Loading

NlightNFotis Mar 22, 2023 •

edited

Loading

thomasspriggs Mar 22, 2023 •

edited

Loading

thomasspriggs Mar 22, 2023 •

edited

Loading

thomasspriggs Mar 22, 2023 •

edited

Loading

thomasspriggs Mar 30, 2023 •

edited

Loading