New API for getting goto models #1339

kroening · 2017-09-03T17:05:14Z

This offers a new API for generating goto models from cmdlinet

peterschrammel · 2017-09-04T07:52:13Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -527,7 +528,7 @@ int goto_instrument_parse_optionst::doit()

    if(cmdline.isset("list-symbols"))
    {
-      show_symbol_table(true);
+      show_symbol_table(symbol_table, get_ui());


--list-symbols seems to be an alias of --show-symbol-table. I suggest to factorise the calls and deprecate one of the options if not needed anymore.

The behaviour of "list-symbols" and "show-symbol-table" ought to be different - I believe the above change thus introduces a bug.

Having read the rest of the PR: this should be show_symbol_table_brief instead.

peterschrammel · 2017-09-04T07:54:39Z

src/goto-instrument/goto_instrument_parse_options.h

@@ -116,7 +115,13 @@ class goto_instrument_parse_optionst:
  bool partial_inlining_done;
  bool remove_returns_done;

+  symbol_tablet symbol_table;


why not goto_modelt as done in cbmc_parse_options.h ?

Done, big job.

tautschnig · 2017-09-04T15:24:05Z

src/cbmc/bmc.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <list>
 #include <map>

+#include <util/ui_message.h>
 #include <util/options.h>


As you do lexicographic sorting of includes elsewhere: do this here as well?

tautschnig · 2017-09-04T15:27:33Z

src/cbmc/cbmc_parse_options.cpp


-  expr_listt bmc_constraints;
+    language->show_parse(std::cout);


Can this entire "show-parse-tree" handling be moved to a separate function so that it can easily be used from other tools accepting source files? At least symex come to my mind.

Yes, but seems independent job.

tautschnig · 2017-09-04T15:30:04Z

src/cbmc/cbmc_parse_options.cpp

-      symbol_table,
-      goto_functions,
+      goto_model.symbol_table,
+      goto_model.goto_functions,


The API of remove_static_init_loops should be changed to accept a goto_modelt. (Which is pretty trivial, because this is the only invocation.)

tautschnig · 2017-09-04T15:31:34Z

src/cbmc/cbmc_parse_options.cpp

+    options,
+    goto_model.symbol_table,
+    get_message_handler());
+  cbmc_solvers.set_ui(ui_message_handler.get_ui());


This looks pretty weird -- why is both get_message_handler as well as ui_message_handler being used here?

That is to expected -- a message handler is not necessarily a ui_message_handler

More general questions:

Should all occurrences of separate passing ui_message_handlert::uit and message_handlert be replaced by passing a ui_message_handlert ? What is the current use case of having them separate?

Would it make sense to introduce a ui_messaget that provides a set/get_ui() ?

tautschnig · 2017-09-04T15:35:03Z

src/cbmc/cbmc_parse_options.h

-  }
-
+  void register_languages();
+  void get_command_line_options(optionst &options);


If the parameter name is removed elsewhere, it seems safe to do so here as well.

tautschnig · 2017-09-04T15:36:09Z

src/goto-cc/gcc_mode.h

@@ -18,6 +18,8 @@ Date: June 2006

 #include "goto_cc_mode.h"

+#include <set>


No use of std::set in this file?!

const std::map<std::string, std::setstd::string> arch_map;

tautschnig · 2017-09-04T15:39:04Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -527,7 +528,7 @@ int goto_instrument_parse_optionst::doit()

    if(cmdline.isset("list-symbols"))
    {
-      show_symbol_table(true);
+      show_symbol_table(symbol_table, get_ui());


Having read the rest of the PR: this should be show_symbol_table_brief instead.

08f269c Merge pull request diffblue#1388 from smowton/merge-develop-20170914 e3f3abd Merge remote-tracking branch 'upstream/develop' into merge-develop-20170914 4df244c Merge pull request diffblue#1383 from reuk/reuk/sync-projects f25db0a Merge pull request diffblue#189 from diffblue/smowton/fix/remove_debug_code 1fae64c Remove stray use of overlay_map 1264b4d Re-enable old function signatures for test-gen compat e54c0e9 Merge pull request diffblue#338 from thk123/bug/function-flag-on-goto-program 63c9a1e Merge pull request diffblue#1374 from reuk/reuk/maintain-pointer-invariants 00e4555 Fix up CMake build (unrelated) 81f1300 Use PRECONDITION in std_types.h a9806c0 Ensure pointer invariants are maintained a46ad62 Regenerate malformed binary blobs f77822b Merge pull request diffblue#1380 from diffblue/remove-musketeer 22f06fd Correcting windows build 3ede81b Merge pull request diffblue#1293 from reuk/cmake-develop 92a52a5 Corrected doxygen errors c6f1430 Ensure symex and goto-analyzer regenerate functions e37d3d5 Disable failing test in the symex directory 15b89fc Weaked the tests for pointer-function-parameters dee89b0 Fixing the method to work with java_bytecode 1ccd1a2 Add support for using the --function flag to goto-analyze and symex 0732580 Adding missing overrides 71dec3d Use ID_main as the default name for entry function 2aea88d Made generate_start_function abstract f0d6d72 Refactored the regenerate function into goto-programs 71e6800 Added regression test for using --function on a GOTO program 94b7185 Implemented generate_start_function for Java cd416bc Call generate_start_function only when regenerating the start function ee5fb93 Protect against invalid function label 2a3d876 Adding explanatory comment f347a22 Cause a regeneration of the entry method if a --function is provided 69d05a9 Merge pull request diffblue#1382 from pkesseli/bugfix/language-opaque-stubs d45325c Merge pull request diffblue#1378 from thk123/bugfix/fix-symex-appveyor 444f256 Add initial value to languaget::generate_opaque_stubs 91e733d Manually disable some failing tests 41bafc0 Merge pull request diffblue#1375 from pkesseli/bugfix/uncaught-exceptions-invariant a31f1d9 remove musketeer af8d46f Reverting manually commited fixes e73a884 Attempt to fix the symex appveyor build 0496142 Account for replaced functions in exceptions_map 2816b80 revert symex regression until Appvoyer works 6a2fd50 added symex to Appveyor build a2834d0 Map wrappers: forward more of the std::map interface 0a668ae Merge commit '6f386e5eeffa223e7213b596403085f8b497023e' into pull-support-20170908-2 8cd4490 Merge pull request diffblue#1373 from diffblue/symex-trace-fix 5d2d07b enable symex regression testing 5195d24 avoid confusion between SSA lhs and full lhs during assignment 430218f option is now --trace 746bff5 remove_returns missing in symex 211355d comments on test 3896110 output statements 8fc714d use __CPROVER_assert 728ac5b Merge pull request diffblue#1367 from reuk/reuk/disable-alpine-in-travis 73b4357 Merge pull request diffblue#1339 from diffblue/initialize_goto_model 4febd10 Merge pull request diffblue#1364 from diffblue/phread-create-fix 0cfd7b0 Remove PRE_COMMAND scaffolding 04b4f63 Merge pull request diffblue#186 from diffblue/cleanup/misc 577fa6c Tightened up usage of maps 8782103 Merge pull request diffblue#1365 from smowton/smowton/feature/more_map_forwarding 4dde3c5 Disable glucose in Travis 91684da Clean up CMake files after diffblue#1321 7d4e9b5 Make CMake release flags similar to Makefile build 5ee349f Control SAT library from makefiles ad486f8 Set up glucose externalproject 5afa929 Quote paths in flex/bison commands 9afbced Disable 32-bit builds in Travis d953327 Enable caching for CMake builds (hopefully) 6251055 Fix and refactor library_check target 3c36aa5 Enable CMake in Travis f6e4968 Enable running tests from CMake e609bbb Add CMake howto to COMPILING file 22c2ab9 Add CMakeLists 6facf74 Map wrappers: forward more of the std::map interface b846858 Merge pull request diffblue#1291 from LAJW/optional 3ddd377 clean-out ill-modeled optimization in string comparisons 95c5e63 Disable Alpine in Travis fe60e60 pthread_create arguments null/nonnull fix 7d30cde missing copyright header 8c4ff7b remove spurious references to langapi/language_ui.h e4498ca brief list of symbols, from language_uit fc4d44a use goto_modelt 9469552 use initialize_goto_model in CBMC/goto-analyse/etc 40fe0f8 simplify API of goto_convert 40557df Used range iterators d4e89fd Tidy up symbol_tablet::move c125146 Merge pull request diffblue#1245 from tautschnig/run-diagnostic 435c0bf Merge pull request diffblue#1321 from reuk/reuk/remove-unused-files 08a4077 Make the child process that failed to execvp exit 4928f69 Diagnostic output if run/execve fails 5863a75 Merge pull request diffblue#1333 from tautschnig/remove-c_sizeof 498718f Code readability 2217501 Remove unused files 1c8d81a Merge pull request diffblue#1356 from smowton/smowton/feature/test_pl_add_dry_run 56b5e25 Merge pull request diffblue#1358 from thk123/feature/decrease-message-spam 359a3e3 Modified verbosity for loaded message 296349c Add dry-run mode to test.pl f6d94cf clean out an unused method 3613ebc When possible, update array types before typechecking initializer 3273bf5 Fix type casts from initializer lists to arrays of unspecified size 1fa569f sizeof(*(void*)) is sizeof(char) d79067e Remove long-deprecated c_sizeof in favour of size_of_expr et al. 254f133 Merge pull request diffblue#1323 from janmroczkowski/janmroczkowski/goto_modelt-output-const 388a25e Make uncaught_exceptions_analysis.output const 211fcc2 Make path_nodet.output const 9be84ea Make automatont.output const 567eaa7 Make basic_blockst.output const ebbbf5f Make goto_modelt.output const ae584df Move optional unit tests into util directory 4dbf939 Manually fix optional 43d0602 Add unit tests for nonstd::optional 8584bb0 Add nonstd/optional.hpp library 281e384 Workaround for travis performing shallow clones with wrong branch git-subtree-dir: cbmc git-subtree-split: 08f269c

kroening requested a review from tautschnig September 3, 2017 17:05

kroening changed the title ~~Initialize goto model~~ New API for getting goto models Sep 3, 2017

kroening added the enhancement label Sep 3, 2017

kroening mentioned this pull request Sep 3, 2017

[depends: #1339] Get goto model #1285

Closed

peterschrammel reviewed Sep 4, 2017

View reviewed changes

tautschnig self-assigned this Sep 4, 2017

tautschnig reviewed Sep 4, 2017

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Sep 4, 2017

kroening force-pushed the initialize_goto_model branch 5 times, most recently from c7f83bc to 5fb0a74 Compare September 5, 2017 18:38

tautschnig mentioned this pull request Sep 6, 2017

Make message streams accept XML and JSON data #1349

Merged

kroening force-pushed the initialize_goto_model branch 4 times, most recently from c41c552 to d7d7138 Compare September 7, 2017 12:16

kroening assigned tautschnig and peterschrammel and unassigned kroening Sep 8, 2017

Daniel Kroening added 6 commits September 8, 2017 14:55

simplify API of goto_convert

40fe0f8

use initialize_goto_model in CBMC/goto-analyse/etc

9469552

use goto_modelt

fc4d44a

brief list of symbols, from language_uit

e4498ca

remove spurious references to langapi/language_ui.h

8c4ff7b

missing copyright header

7d30cde

kroening force-pushed the initialize_goto_model branch from 3f77308 to 7d30cde Compare September 8, 2017 13:55

kroening merged commit 73b4357 into develop Sep 11, 2017

kroening deleted the initialize_goto_model branch October 12, 2017 15:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

New API for getting goto models #1339

New API for getting goto models #1339

kroening commented Sep 3, 2017

peterschrammel Sep 4, 2017

tautschnig Sep 4, 2017

tautschnig Sep 4, 2017

kroening Sep 5, 2017

peterschrammel Sep 4, 2017

kroening Sep 5, 2017

tautschnig Sep 4, 2017

kroening Sep 5, 2017

tautschnig Sep 4, 2017

kroening Sep 5, 2017

tautschnig Sep 4, 2017

kroening Sep 5, 2017

tautschnig Sep 4, 2017

kroening Sep 5, 2017

peterschrammel Sep 8, 2017 •

edited

Loading

tautschnig Sep 4, 2017

tautschnig Sep 4, 2017

kroening Sep 5, 2017

tautschnig Sep 4, 2017

		@@ -18,6 +18,8 @@ Date: June 2006

		#include "goto_cc_mode.h"

		#include <set>

New API for getting goto models #1339

New API for getting goto models #1339

Conversation

kroening commented Sep 3, 2017

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel Sep 8, 2017 • 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

peterschrammel Sep 8, 2017 •

edited

Loading