Factor out goto model processing and default options #2049

karkhaz · 2018-04-12T12:23:38Z

This PR introduces a static method for setting CBCM's default options, and makes two of cbmc_parse_optiont's methods static (for getting and processing a goto-model). This is so that clients that wish to emulate CBMC's functionality can do so by calling into these static methods, rather than duplicating code that is currently scattered through the file.

tautschnig

This refactoring is great, and my requests-for-more-work are all only possible because you started this line of work. Sorry that it means there is even more work to do... @peterschrammel @kroening could you comment on whether some of that work is also useful to simplify/reduce redundancy with other *_parse_optionst instances?

tautschnig · 2018-04-12T12:35:10Z

src/cbmc/cbmc_parse_options.cpp

@@ -111,6 +130,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
  if(cmdline.isset("paths"))
    options.set_option("paths", true);

+  cbmc_parse_optionst::set_default_options(options);
+


Nit pick: may I suggest to move this up by three lines to be the very first step before doing if(cmdline.isset...?

tautschnig · 2018-04-12T12:39:03Z

src/cbmc/cbmc_parse_options.cpp

+  options.set_option("simplify-if", true);
+
+  // Default false
+  options.set_option("stop-on-fail", false);


Could you please add unwinding-assertions, partial-loops, slice-formula in here and refactor their current command-line/options code to use if(cmdline.isset...)?

tautschnig · 2018-04-12T12:44:13Z

src/cbmc/cbmc_parse_options.cpp

-  const optionst &options)
+  goto_modelt &goto_model,
+  const optionst &options,
+  const cmdlinet &cmdline,


Your change highlights one existing poor design: this function should not be using cmdline anymore, anything it cares about ought to have been placed in options. Could you please clean this up as well?

tautschnig · 2018-04-12T12:55:58Z

src/cbmc/cbmc_parse_options.cpp

+  const cmdlinet &cmdline,
+  messaget &log,
+  ui_message_handlert &ui_message_handler,
+  message_handlert &mh)


mh and ui_message_handler will actually be the same in the context of cbmc_parse_optionst, and both of which you'd get by doing log.get_message_handler(). What you wouldn't be able to get, though, is ui_message_handler.get_ui() so maybe pass that in addition to just a messaget?

tautschnig · 2018-04-12T12:56:34Z

src/cbmc/cbmc_parse_options.cpp

+  const optionst &options,
+  const cmdlinet &cmdline,
+  messaget &log,
+  message_handlert &mh)


As above: just pass log, and obtain mh via log.get_message_handler().

karkhaz · 2018-04-12T15:33:28Z

Just pushed some changes. Please could you confirm that the hunk at cbmc_parse_options.cpp:224 captures the right intention? I think this is a bit more explicit than before, even, since the code before would silently ignore --unwinding-assertions if --cover is passed...but perhaps that behaviour is intentional?

At the severe risk of creating more work for myself...there are queries to cmdline scattered everywhere, for example in process_goto_program. Many of the cmdline options that are being queried never even get an option set for them. Arguably, I could go on a crusade to get rid of all lookups to cmdline after the initial setting of options, so that the only object we ever pass around is options. On the other hand, since options is used fairly deep inside CBMC (at least inside symex, maybe even later) perhaps it makes sense to keep it as small as possible? Some of the cmdline options that are queried in the front-end only make sense in the front end, e.g. --version, --show-goto-functions etc and perhaps it's a waste of lookup time to drag them all over the rest of the program. I don't have strong opinions either way, let me know what your preference is.

I think eventually it might be desirable to avoid passing options around to deep code as well as cmdline. I've opened #2050 based on a discussion @tautschnig and I had about something unrelated.

There was previously no public interface to check whether an option had been set in an optionst object; this meant that clients were instead using the isset() method of cmdlinet. This change allows us to set the options from the cmdlinet near the beginning of the front-end, and not refer to the cmdlinet afterward.

CBMC parse options that have default values are all set in a single place---a static method that may also be called from any client that needs to emulate CBMC's default options (e.g. unit tests). Previous to this commit, there were a lot of if(cmdline.isset("no-foo")) options.set_option("foo", false); else options.set_option("foo", true); This commit removes all the else cases.

karkhaz · 2018-04-12T17:55:49Z

All checks passed. I implemented your suggestion of changing cmdline lookups to options lookups, but there were several things passed on the command line that were not having an option set for them (property, reachability-slice{,-fb}, bounds-check, pointer-check, nondet-static) so I'm setting options for those now.

tautschnig · 2018-04-12T18:13:18Z

src/cbmc/cbmc_parse_options.cpp

+    options.set_option("bounds-check", true);
+
+  if(cmdline.isset("pointer-check"))
+    options.set_option("pointer-check", true);


"pointer-check" and "bounds-check" are actually covered by PARSE_OPTIONS_GOTO_CHECK below so those two can be skipped here.

tautschnig · 2018-04-12T18:15:21Z

src/cbmc/cbmc_parse_options.cpp

-      cmdline.isset("unwinding-assertions"));
+    error() << "--cover and --unwinding-assertions "
+            << "must not be given together" << eom;
+    exit(CPROVER_EXIT_USAGE_ERROR);


It's probably a good idea to communicate this to users explicitly.

tautschnig · 2018-04-12T18:18:08Z

src/cbmc/cbmc_parse_options.cpp

      nondet_static(goto_model);
    }

-    if(cmdline.isset("string-abstraction"))
+    if(options.get_bool_option("string-abstraction"))


I don't think this option is getting set above?

tautschnig · 2018-04-12T18:18:26Z

src/cbmc/cbmc_parse_options.cpp

@@ -777,21 +806,21 @@ bool cbmc_parse_optionst::process_goto_program(
    // add loop ids
    goto_model.goto_functions.compute_loop_numbers();

-    if(cmdline.isset("drop-unused-functions"))
+    if(options.get_bool_option("drop-unused-functions"))


This needs to be checked as well above, I think.

tautschnig · 2018-04-12T18:20:57Z

src/cbmc/cbmc_parse_options.cpp

      {
-        error() << "--reachability-slice and --reachability-slice-fb "
-                << "must not be given together" << eom;
+        log.error() << "--reachability-slice and --reachability-slice-fb "


May I suggest moving this options-collision checking up with the cmdline parsing? Errors should be flagged as early as possible.

karkhaz · 2018-04-12T19:18:57Z

sigh thanks for pointing these out. My strategy was to set the option for each command-line that was causing a test somewhere to fail. So all of the ones you pointed out don't have sufficient test coverage that it made a difference that I missed setting their option 😞 I now feel that this is fragile and prone to drift apart in the future---in both directions: where somebody misses setting an option, or where an option is accidentally set twice like in PARSE_OPTIONS_GOTO_CHECK. I don't really feel qualified to write tests to check for this.

I'll sort these out tomorrow, need to sleep now, but maybe I'll think of a more robust way of doing this (or I'd appreciate any suggestions). I've often fantasied about writing a new parse_optionst base class where everything would be specified in one single uniform place (flag, help text, action if the flag was passed)---similar to the path_choosert initializer in #1915, and shared between the cprover tools as needed. But not sure if that would be welcome, or a good use of time...

tautschnig · 2018-04-13T12:46:12Z

[...] I've often fantasied about writing a new parse_optionst base class where everything would be specified in one single uniform place [...]

Is #1521 of some help in this regard? Not that it specifies one single solution, but at least there is discussion - please do chime in!

Other than that: yes, better test coverage is needed, or really just a record of current test coverage. There has been some work on that, but AFAIK that got put on the backlog.

karkhaz · 2018-04-16T13:01:53Z

Comments are addressed, all checks are passing. I'll wait until I at least have a skeleton implementation before chiming in, I want to see if my ideas are practical.

(One other thing that I wanted to have is a command line interface that could dump itself as {ba,z}sh completion files, man pages, etc...there's already a script that does this, but it would be nice to do it programatically rather than parsing cmdline text, since then we could also pass type information to zsh completion and so on)

smowton · 2018-04-17T10:05:28Z

This looks great -- one question, to what degree can this be factored with JBMC?

karkhaz · 2018-04-17T15:56:28Z

@smowton my feeling is that it might end up becoming a mess of front-end specific checks if we used the same static method? E.g. JBMC needs a lazy_goto_modelt, the options are slightly different and may become more or less different over time, etc.

I haven't actually tried it, but it looks like there would have to be e.g. a static cbmc_doit and static jbmc_doit, which would each call into static bmc_doit that contains common code, but there are things that need to happen in the middle of those functions...I'm not sure that it's worth factoring front-end stuff into a single method is worth it just yet. Having a common BMC is fine IMO, but there seems to be too many small differences in front-end stuff to justify it...

smowton · 2018-04-17T15:59:25Z

Fair enough, leave it then

tautschnig · 2018-04-17T16:57:31Z

src/cbmc/cbmc_parse_options.cpp

+  options.set_option("simplify", true);
+  options.set_option("simplify-if", true);
+
+  // Default false


I am wondering: should this part actually be omitted completely? It does make a difference if the (new) is_set is used, but for get_bool_option setting them to false is as good as not setting them.

Edit: many other options also default to false, but are not being set here. I'm always after consistency...

CBMC's methods for getting a goto-model from a source file, and processing that goto-model to be ready for bounded model checking, are now static so that they can be called from clients that wish to set up a goto-model the same way that CBMC does.

karkhaz · 2018-04-18T21:03:35Z

@tautschnig I removed the default-false options.

karkhaz requested review from kroening, peterschrammel, smowton and tautschnig as code owners April 12, 2018 12:23

karkhaz mentioned this pull request Apr 12, 2018

Path exploration goodies #1915

Merged

tautschnig requested changes Apr 12, 2018

View reviewed changes

karkhaz force-pushed the kk-factor-goto-model-processing branch 2 times, most recently from 20594cf to 0859693 Compare April 12, 2018 15:18

karkhaz force-pushed the kk-factor-goto-model-processing branch from 0859693 to 85e8d63 Compare April 12, 2018 15:42

karkhaz force-pushed the kk-factor-goto-model-processing branch from 85e8d63 to 9af0a1c Compare April 12, 2018 16:44

karkhaz force-pushed the kk-factor-goto-model-processing branch from 9af0a1c to b7b9ad9 Compare April 12, 2018 17:23

tautschnig reviewed Apr 12, 2018

View reviewed changes

karkhaz force-pushed the kk-factor-goto-model-processing branch 2 times, most recently from 8aa1ea1 to 3e4a77e Compare April 15, 2018 21:50

smowton approved these changes Apr 17, 2018

View reviewed changes

tautschnig approved these changes Apr 17, 2018

View reviewed changes

karkhaz force-pushed the kk-factor-goto-model-processing branch from 3e4a77e to 014d151 Compare April 17, 2018 22:23

tautschnig merged commit 0bff19b into diffblue:develop Apr 18, 2018

karkhaz deleted the kk-factor-goto-model-processing branch April 18, 2018 21:10

tedinski mentioned this pull request Jan 6, 2022

"--cover and --unwinding-assertions must not be given together" #6561

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Factor out goto model processing and default options #2049

Factor out goto model processing and default options #2049

karkhaz commented Apr 12, 2018

tautschnig left a comment

tautschnig Apr 12, 2018

tautschnig Apr 12, 2018

tautschnig Apr 12, 2018

tautschnig Apr 12, 2018

tautschnig Apr 12, 2018

karkhaz commented Apr 12, 2018

karkhaz commented Apr 12, 2018

tautschnig Apr 12, 2018

tautschnig Apr 12, 2018

tautschnig Apr 12, 2018

tautschnig Apr 12, 2018

tautschnig Apr 12, 2018

karkhaz commented Apr 12, 2018

tautschnig commented Apr 13, 2018

karkhaz commented Apr 16, 2018

smowton commented Apr 17, 2018

karkhaz commented Apr 17, 2018

smowton commented Apr 17, 2018

tautschnig Apr 17, 2018 •

edited

Loading

karkhaz commented Apr 18, 2018

Factor out goto model processing and default options #2049

Factor out goto model processing and default options #2049

Conversation

karkhaz commented Apr 12, 2018

tautschnig 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

Choose a reason for hiding this comment

karkhaz commented Apr 12, 2018

karkhaz commented Apr 12, 2018

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

karkhaz commented Apr 12, 2018

tautschnig commented Apr 13, 2018

karkhaz commented Apr 16, 2018

smowton commented Apr 17, 2018

karkhaz commented Apr 17, 2018

smowton commented Apr 17, 2018

tautschnig Apr 17, 2018 • edited Loading

Choose a reason for hiding this comment

karkhaz commented Apr 18, 2018

tautschnig Apr 17, 2018 •

edited

Loading