Add `goto-bmc`, a new tool to run only the verifier #7762

NlightNFotis · 2023-06-12T10:02:33Z

This adds a new tool, goto-bmc, which you can think of as CBMC-lite: its purpose is to run only the backend, on a binary that is produced to be symex-ready, i.e. have been lowered to a form that is accepted by symex without the need for any more transformations.

The aim of the addition of this tool is to contribute towards the efforts to make CBMC and all of the assorted tools more modularised, by providing access to the backend of CBMC without needing to bundle frontends, transformation passes, etc, so that usage or integration of the tool into other software or (CI/dev) pipelines becomes easier.

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-06-12T11:04:56Z

Codecov Report

Patch coverage: 98.43% and project coverage change: +0.53 🎉

Comparison is base (b1d78e2) 78.06% compared to head (4f5a3b0) 78.59%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7762      +/-   ##
===========================================
+ Coverage    78.06%   78.59%   +0.53%     
===========================================
  Files         1693     1696       +3     
  Lines       193308   193450     +142     
===========================================
+ Hits        150899   152049    +1150     
+ Misses       42409    41401    -1008

Impacted Files	Coverage Δ
src/libcprover-cpp/api.h	`100.00% <ø> (ø)`
src/libcprover-cpp/verification_result.h	`0.00% <ø> (ø)`
src/goto-bmc/goto_bmc_parse_options.cpp	`97.36% <97.36%> (ø)`
src/goto-bmc/goto_bmc_main.cpp	`100.00% <100.00%> (ø)`
src/goto-bmc/goto_bmc_parse_options.h	`100.00% <100.00%> (ø)`
src/libcprover-cpp/api.cpp	`90.00% <100.00%> (+2.34%)`	⬆️
src/libcprover-cpp/verification_result.cpp	`87.23% <100.00%> (+0.56%)`	⬆️

... and 68 files with indirect coverage changes

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

TGWDB · 2023-06-19T10:34:56Z

src/libcprover-cpp/api.h

@@ -98,7 +98,8 @@ struct api_sessiont

  /// Implement necessary transformations to reduce model to core-GOTO, before
  /// being fed to symex.
-  /// @return The function return `true` if it failed because CBMC produced an error.
+  /// @return The function return `true` if it failed because CBMC produced


return -> returns

TGWDB · 2023-06-19T10:35:59Z

src/libcprover-cpp/verification_result.cpp

+// FOTIS' note: Modelled after `result_to_exit_code` in
+// `src/goto-checker/properties.cpp`.


Should this be refactored to use the same code then?

We can't do that because the functions use different types as inputs.

We have two types that are equivalent, but one of them is internal to CBMC (goto-checker, really), and thus, we can't expose it to the C++ API (because of the internal headers issue), and the other is the C++ API equivalent, which is present in the headers for the API.

We have in the API (under verification_result.cpp) a function which does the translation from result_internal -> result_external, but we needed to have a function from result_external -> BMC_EXIT_CODE. This is the function that was modelled under the equivalent one from result_internal -> BMC_EXIT_CODE.

TGWDB · 2023-06-19T10:38:16Z

src/goto-bmc/goto_bmc_parse_options.cpp

+  int argc,
+  const char **argv)
+  : parse_options_baset(
+      CORE_CBMC_ONLY_OPTIONS,


symex-ready

These shouldn't be called symex-ready - they refer to the tool not the goto-binaries.

But they will need to be made consistent to the actual tool name, which we settled on goto-bmc (this is the name of the tool built). The references are artefacts from a previous change where we called the tool corebmc but settled on goto-bmc instead.

TGWDB · 2023-06-19T10:38:23Z

src/goto-bmc/goto_bmc_parse_options.cpp

+      CORE_CBMC_ONLY_OPTIONS,
+      argc,
+      argv,
+      std::string("CORE_CBMC_ONLY") + CBMC_VERSION)


symex-ready

Renamed to goto-bmc - Done.

TGWDB · 2023-06-19T10:38:33Z

src/goto-bmc/goto_bmc_parse_options.cpp

+  std::cout << api_message_get_string(message) << std::endl;
+}
+
+int core_cbmc_only_parse_optionst::doit()


symex-ready

TGWDB · 2023-06-19T10:40:21Z

src/goto-bmc/goto_bmc_parse_options.h

+class core_cbmc_only_parse_optionst : public parse_options_baset
+{
+public:
+  core_cbmc_only_parse_optionst(int argc, const char **argv);


symex-ready

TGWDB · 2023-06-19T10:40:26Z

src/goto-bmc/goto_bmc_parse_options.h

+  virtual int doit();
+};
+
+#endif // CPROVER_CORE_BMC_PARSE_OPTIONS_H


symex-ready

TGWDB · 2023-06-19T10:41:24Z

src/libcprover-cpp/api.h

+  /// Read a goto-binary from a given filename.
+  /// @warning Will error out if it reads a source file.
+  void read_goto_binary(std::string &file) const;


This should check that the goto binary is in symex-ready form. Of course the check is not implemented yet, but maybe this should be a comment or stub in the implementation?

We track this functionality, by having a negative test under regression/goto-bmc/goto-bmc-non-symex-ready-goto whose job is to fail when fed a non-symex-ready goto.

For now it fails with an invariant violation, so the error message leaves a lot to be desired, but when we fix the recognition of the symex-ready-goto binaries, this test is going to fail (because the invariant violation pattern is not going to be present in the output any more) and this will serve as our reminder to go back and fix that.

TGWDB · 2023-06-19T10:41:57Z

src/libcprover-cpp/api.h

+  void read_goto_binary(std::string &file) const;
+
+  /// True if file is goto-binary.
+  bool is_goto_binary(std::string &file) const;


Maybe here, -> is_symex_ready_goto_binary?

We don't want to do this, because we delegate to is_goto_binary from src/goto-programs/read_goto_binary.cpp which doesn't check the "level" of the goto-binary (whether transformations have been performed and which ones), so we can't really promise to give information we don't have.

TGWDB · 2023-06-19T10:42:06Z

src/libcprover-cpp/api.h

 private:
  std::unique_ptr<api_session_implementationt> implementation;
+
+  /// Implement necessary transformations to reduce model to core-GOTO, before


symex-ready

peterschrammel · 2023-06-20T13:50:57Z

src/libcprover-cpp/api.cpp

+  return run_verifier();
+}
+
+/// <FILL ME>


This was empty while we did some refactoring, acting as a reminder to fill in documentation once the code stabilised - it's filled in the next commit.

peterschrammel · 2023-06-20T13:57:10Z

src/goto-bmc/goto_bmc_parse_options.cpp

+{
+}
+
+void print_messages_to_stdout(


❓ What is this function for?
We should use log for printing messages.

The way the API works for now is it needs a callback to be passed to it, which it then calls to process messages from it.

This callback function needs to have a specific signature for it to be able to be registered with the API.

What we can do however, is change the references to std::cout to output things via the log instead.

Done in 755f0f5

Done in 755f0f5

Is that actually a good idea? With the new API the log exists inside the API layer but is not exposed. So by creating a log in the entry point doesn't that mean two instances of it exist at once?

peterschrammel · 2023-06-20T14:01:16Z

src/goto-bmc/module_dependencies.txt

@@ -0,0 +1,3 @@
+util
+libcprover-cpp
+goto-programs


Why this dependency? Shouldn't goto-bmc only depend on libcprover-cpp?

We need this because of the check inside src/goto-bmc/goto_bmc_parse_options.cpp:52 which has a call to is_goto_binary, defined under src/goto-programs/read_goto_binary.cpp

If you need it then the API needs to expose it, no?

I'm wrong, we already expose it in the API - we will change it to make it defer to the API (we already have this capability, probably lost the idea somewhere during refactoring)

esteffin

The log-handling function has to be fixed properly

src/goto-bmc/goto_bmc_parse_options.cpp

src/libcprover-cpp/api.h

src/libcprover-cpp/api.cpp

thomasspriggs · 2023-06-21T14:55:10Z

src/libcprover-cpp/api.h

@@ -79,11 +79,17 @@ struct api_sessiont
  /// Validate the loaded goto model
  void validate_goto_model() const;

-  // A simple API version information function.
+  /// A simple API version information function.


⛏️ Fix of existing documentation should be in a separate commit from the refactor, if the function is not changed as part of the refactor.

thomasspriggs · 2023-06-21T15:01:48Z

src/libcprover-cpp/api.h

 private:
  std::unique_ptr<api_session_implementationt> implementation;
+
+  /// <FILL ME>
+  bool preprocess_model() const;


💡 If this function is truly an implementation detail, then it would make sense to me for it to be a free function which is defined the .cpp only.
⛏️ If the plan is to eventually use this as part of the publicly facing API then it isn't following the existing code pattern, which is to use the call-back to indicate errors and to return a void result.

src/libcprover-cpp/api.cpp

thomasspriggs · 2023-06-21T19:04:26Z

src/libcprover-cpp/verification_result.h

@@ -80,4 +80,8 @@ struct verification_resultt
  std::unique_ptr<verification_result_implt> _impl;
 };

+// Allow translation of `verifier_resultt` into a CPROVER_EXIT_CODES (so that


⛏️ The use of a plural CPROVER_EXIT_CODES suggests one result is turned into multiple codes.
🤔 Given that the API headers may be distributed without the rest of the project source, the reader maybe unaware of the existence of src/util/exit_codes.h. So maybe we should just call this a Command Line Interface (CLI) return value/exit code; especially given that the result is not strongly typed.

src/libcprover-cpp/api.cpp

src/goto-bmc/goto_bmc_parse_options.cpp

thomasspriggs · 2023-06-21T19:28:17Z

regression/goto-bmc/goto-bmc-non-symex-ready-goto/negative1/main.desc

@@ -1,7 +1,7 @@
 CORE
 main.c

-^EXIT=[127|134]$


⛏️ The commit title refers to moving tests, but this part is changing the test.

To be able to run the BMC part of CBMC (symex and the decision-procedure) the API `verify_model` function has been split in two separate steps: the lowering step that applies all the transformations to the core-goto program and the verification step that only runs symex and the decision-procedure.

Add a new `goto-bmc` executable to CBMC that reads a core-goto program from a given binary file and runs symex and the decision procedure. This has been done by using the API functionalities instead of addin a new argument to CBMC.

esteffin

Change requested has been fulfilled

In preparation for expanding the context beyond just the message stream.

This commit adds exiting on bad input files as is proper, instead of proceeding to further worse failures such as INVARIANT violations or even seg faults.

This would previously been left as a single unexpanded argument regardless of the number of arguments in the `.desc` file. For example `goto_bmc main.goto.symex_ready ''` in the case of no arguments specified. This should be expanded to match the number of arguments in the `options` variable. For example `goto_bmc main.goto.symex_ready` in the case of no arguments or `goto_bmc main.goto.symex_ready --argument1 --argument2` in the case of two arguments in the desc file.

Zero arguments should trigger an error as should files which fail the is_goto_binary check when a single file is specified.

Running `goto-bmc --help` was previously resulting in the tool exiting without displaying help text. This was due to the incomplete message being cached, but never sent to the console output before exiting.

The `parse_options_baset::main` function checks for a `--help` argument. It calls the `help()` member function and exits rather than calling `doit()` when this argument is specified. The duplicated code removed by this commit was misleading because it was never reached when the `--help` argument was specified.

thomasspriggs

The missing error handling has now been added.

Setting the `CODEOWNERS` file entry for `src/goto-bmc` folder.

thomasspriggs · 2023-07-05T11:34:51Z

CODEOWNERS

@@ -50,6 +50,7 @@
 # These files change frequently and changes are medium-risk

 /src/goto-analyzer/ @martin-cs @peterschrammel
+/src/goto-bmc/ @NlightNFotis @thomasspriggs @esteffin @TGWDB @peterschrammel


NlightNFotis self-assigned this Jun 12, 2023

NlightNFotis force-pushed the esteffin/verifier-only-entry-point branch from 3daedb9 to e993c8f Compare June 14, 2023 10:25

NlightNFotis marked this pull request as ready for review June 14, 2023 10:26

NlightNFotis requested review from a team, thomasspriggs, esteffin, TGWDB, peterschrammel, kroening and tautschnig as code owners June 14, 2023 10:26

NlightNFotis force-pushed the esteffin/verifier-only-entry-point branch 2 times, most recently from d3cd4ee to b23116a Compare June 19, 2023 10:37

TGWDB reviewed Jun 19, 2023

View reviewed changes

NlightNFotis force-pushed the esteffin/verifier-only-entry-point branch 5 times, most recently from 063e616 to dfde351 Compare June 19, 2023 15:00

TGWDB approved these changes Jun 19, 2023

View reviewed changes

peterschrammel reviewed Jun 20, 2023

View reviewed changes

esteffin suggested changes Jun 20, 2023

View reviewed changes

src/goto-bmc/goto_bmc_parse_options.cpp Outdated Show resolved Hide resolved

esteffin force-pushed the esteffin/verifier-only-entry-point branch 3 times, most recently from ea812bd to 5a1382a Compare June 21, 2023 14:36

thomasspriggs requested changes Jun 21, 2023

View reviewed changes

NlightNFotis force-pushed the esteffin/verifier-only-entry-point branch from 5a1382a to d98508a Compare June 26, 2023 16:37

esteffin and others added 3 commits June 26, 2023 17:39

Add goto-bmc executable.

727f434

Add a new `goto-bmc` executable to CBMC that reads a core-goto program from a given binary file and runs symex and the decision procedure. This has been done by using the API functionalities instead of addin a new argument to CBMC.

Add translation of final_result to CPROVER_EXIT_CODES

d032cae

Add regression tests for basic functionality of goto-bmc

edea1bc

NlightNFotis force-pushed the esteffin/verifier-only-entry-point branch from d98508a to edea1bc Compare June 26, 2023 16:40

esteffin approved these changes Jun 30, 2023

View reviewed changes

thomasspriggs added 10 commits July 4, 2023 17:03

Refactor call back function to accept a struct context

090b7be

In preparation for expanding the context beyond just the message stream.

Add file read error handling to goto_bmc

94d66bd

This commit adds exiting on bad input files as is proper, instead of proceeding to further worse failures such as INVARIANT violations or even seg faults.

Fix argument check

4322d61

Zero arguments should trigger an error as should files which fail the is_goto_binary check when a single file is specified.

Add tests of error handling on reading invalid goto binaries

192142b

Add tests for incorrect number of goto binaries specified

92d4e38

Add missing end of message in goto_bmc_parse_optionst::help

002eb9e

Running `goto-bmc --help` was previously resulting in the tool exiting without displaying help text. This was due to the incomplete message being cached, but never sent to the console output before exiting.

Add --version command line argument test

74cdc37

Add --help command line argument test

5a667fd

thomasspriggs approved these changes Jul 4, 2023

View reviewed changes

Set code owners for src/goto-bmc.

4f5a3b0

Setting the `CODEOWNERS` file entry for `src/goto-bmc` folder.

thomasspriggs reviewed Jul 5, 2023

View reviewed changes

esteffin requested a review from peterschrammel July 5, 2023 11:42

peterschrammel approved these changes Jul 6, 2023

View reviewed changes

esteffin merged commit 79d8a9c into diffblue:develop Jul 6, 2023
35 checks passed

		// FOTIS' note: Modelled after `result_to_exit_code` in
		// `src/goto-checker/properties.cpp`.

Add goto-bmc, a new tool to run only the verifier #7762

Add goto-bmc, a new tool to run only the verifier #7762

Conversation

NlightNFotis commented Jun 12, 2023

codecov bot commented Jun 12, 2023 • edited Loading

Codecov Report

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis Jun 19, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NlightNFotis Jun 20, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

esteffin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

esteffin left a comment

Choose a reason for hiding this comment

thomasspriggs left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Add `goto-bmc`, a new tool to run only the verifier #7762

Add `goto-bmc`, a new tool to run only the verifier #7762

codecov bot commented Jun 12, 2023 •

edited

Loading

NlightNFotis Jun 19, 2023 •

edited

Loading

NlightNFotis Jun 20, 2023 •

edited

Loading