Clean-up message_handler of parse_options_baset #4521

romainbrenguier · 2019-04-12T07:43:22Z

~~Based on #4520~~

The message handler field was owned by the classes inheriting from
parse_options_baset which lead to strange patterns where the handler
reference was initialized using a reference to a field which was not
constructed yet.
This is cleaner and avoid some reference duplication.

Each commit message has a non-empty body, explaining why the change was made.
[na] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[na] 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).
[na] 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: 2db3a82).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108107188
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: a76ee1f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108108467
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 0e56317).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108123437
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

tautschnig

The second commit alone is worth merging this as soon as possible, but I really think we should not need to use std::unique_ptr here.

tautschnig · 2019-04-12T23:22:44Z

src/util/parse_options.h

@@ -35,6 +37,7 @@ class parse_options_baset
  virtual ~parse_options_baset() { }

 protected:
+  std::unique_ptr<ui_message_handlert> message_handler;


Why can't this just be a stack-allocated member?

tautschnig · 2019-04-12T23:24:14Z

src/util/parse_options.cpp

 {
  std::string optstring=std::string("?h(help)")+_optstring;
  parse_result=cmdline.parse(argc, argv, optstring.c_str());
+  message_handler = util_make_unique<ui_message_handlert>(cmdline, program);
+  log = messaget{*message_handler};


I really think that message_handler should be a full member (see also comment below) and the constructor should do : message_handler(cmdline, program), log(message_handler)

I've done the change now. The reason I didn't do it originally was that it required a bit of reordering because the command line needs to be parsed before the object is constructed, but the change is actually not too bad.

tautschnig

I think this is a nice bit of cleanup, but I suppose you didn't quite expect to be opening a can of worms. See various notes below.

tautschnig · 2019-04-15T10:03:58Z

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -174,7 +173,7 @@ class janalyzer_parse_optionst : public parse_options_baset

  ui_message_handlert::uit get_ui()
  {
-    return ui_message_handler.get_ui();
+    return message_handler.get_ui();


Is this method (janalyzer_parse_optionst::get_ui) actually used?

I think it's not useful anyway...

Maybe just add a commit that removes those?

tautschnig · 2019-04-15T10:04:37Z

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -564,7 +566,7 @@ int jbmc_parse_optionst::doit()
    if(cmdline.isset("show-properties"))
    {
      show_properties(
-        goto_model, log.get_message_handler(), ui_message_handler.get_ui());
+        goto_model, log.get_message_handler(), message_handler.get_ui());


🍌 Are log.get_message_handler() and message_handler actually different?

I hope not. But I will check.

Message_handler and ui shouldn't be passed separately.

tautschnig · 2019-04-15T10:05:22Z

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -800,7 +802,7 @@ int jbmc_parse_optionst::get_goto_program(
      show_goto_functions(
        *goto_model,
        log.get_message_handler(),
-        ui_message_handler.get_ui(),
+        message_handler.get_ui(),


🍌 Again, are log.get_message_handler() and message_handler different? It looks quite confusing.

tautschnig · 2019-04-15T10:06:59Z

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -943,7 +944,7 @@ bool jbmc_parse_optionst::show_loaded_functions(
    show_properties(
      ns,
      log.get_message_handler(),
-      ui_message_handler.get_ui(),
+      message_handler.get_ui(),


tautschnig · 2019-04-15T10:07:10Z

jbmc/src/jbmc/jbmc_parse_options.cpp

-      ui_message_handler,
-      ui_message_handler.get_ui(),
+      message_handler,
+      message_handler.get_ui(),


Relates to 🍌

tautschnig · 2019-04-15T10:10:42Z

src/goto-harness/goto_harness_main.cpp

@@ -10,6 +10,6 @@ Author: Diffblue Ltd.

 int main(int argc, const char *argv[])
 {
-  auto parse_options = goto_harness_parse_optionst(argc, argv);
+  goto_harness_parse_optionst parse_options{argc, argv};
  return parse_options.main();


While at it, go one step further and do return goto_harness_parse_optionst{argc, argv}.main();?

tautschnig · 2019-04-15T10:10:58Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -617,7 +617,7 @@ int goto_instrument_parse_optionst::doit()
      show_goto_functions(
        goto_model,
        log.get_message_handler(),
-        ui_message_handler.get_ui(),
+        message_handler.get_ui(),


No need to pass message_handler and ui separately.

tautschnig · 2019-04-15T10:11:30Z

src/goto-instrument/goto_instrument_parse_options.h

@@ -150,7 +148,7 @@ class goto_instrument_parse_optionst : public parse_options_baset

  ui_message_handlert::uit get_ui()
  {
-    return ui_message_handler.get_ui();
+    return message_handler.get_ui();


Is goto_instrument_parse_optionst::get_ui actually used?

tautschnig · 2019-04-15T10:11:43Z

src/util/parse_options.h

@@ -10,10 +10,12 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_PARSE_OPTIONS_H
 #define CPROVER_UTIL_PARSE_OPTIONS_H

+#include <memory>


No longer needed

tautschnig · 2019-04-15T10:13:26Z

src/util/parse_options.h

 protected:
+  ui_message_handlert message_handler;


I think you could reduce the size of the diff quite a bit by just naming this ui_message_handler.

I also have a slight preference for ui_message_handler in order to distinguish it from a plain message_handler.

peterschrammel · 2019-04-16T08:14:12Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -616,7 +617,7 @@ int goto_instrument_parse_optionst::doit()
    {
      show_goto_functions(
        goto_model,
-        log.get_message_handler(),
+        ui_message_handler,
        ui_message_handler.get_ui(),


No need to pass the ui separately (several occurrences).

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 79b4117).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108645501
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

romainbrenguier · 2019-04-17T10:51:19Z

@peterschrammel I removed the unnecessary arguments

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 46ec583).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108672915
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

ui_message_handler.get_ui() already does the same thing, and is more explicit.

The message handler field was owned by the classes inheriting from parse_options_baset which lead to strange patterns where the handler reference was initialized using a reference to a field which was not constructed yet. This is cleaner and avoid some reference duplications.

Now the log field gets initialized before parse_options_baset is constructed so there is no danger as described in the comment.

The calls will always return a reference to the field ui_message_handler which can be accessed directly instead.

The messaget can be constructed from the message_handler.

This is more precise on the type of message handler we are expecting and makes the ui argument redundant.

This removes the need for passing a seperate ui argument.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 262cc35).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108712914
Status will be re-evaluated on next push.
Common spurious failures include: 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); compatibility was already broken by an earlier merge.

romainbrenguier added do not merge In progress do not review labels Apr 12, 2019

romainbrenguier requested review from cesaro, chrisr-diffblue, cristina-david, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners April 12, 2019 07:43

romainbrenguier self-assigned this Apr 12, 2019

romainbrenguier force-pushed the clean-up/parse-options-messages branch 3 times, most recently from 2db3a82 to a76ee1f Compare April 12, 2019 10:44

allredj reviewed Apr 12, 2019

View reviewed changes

romainbrenguier force-pushed the clean-up/parse-options-messages branch from a76ee1f to 0e56317 Compare April 12, 2019 12:50

romainbrenguier removed do not merge In progress do not review labels Apr 12, 2019

romainbrenguier removed their assignment Apr 12, 2019

allredj reviewed Apr 12, 2019

View reviewed changes

tautschnig reviewed Apr 12, 2019

View reviewed changes

tautschnig assigned romainbrenguier Apr 12, 2019

tautschnig added the cleanup label Apr 12, 2019

romainbrenguier force-pushed the clean-up/parse-options-messages branch from 0e56317 to aac8b2a Compare April 15, 2019 09:19

romainbrenguier force-pushed the clean-up/parse-options-messages branch 2 times, most recently from edfa668 to 14a57e6 Compare April 15, 2019 09:56

tautschnig approved these changes Apr 15, 2019

View reviewed changes

romainbrenguier force-pushed the clean-up/parse-options-messages branch from 14a57e6 to 3245e75 Compare April 16, 2019 08:09

peterschrammel reviewed Apr 16, 2019

View reviewed changes

romainbrenguier force-pushed the clean-up/parse-options-messages branch 2 times, most recently from 79b4117 to 5845d01 Compare April 17, 2019 08:15

tautschnig assigned peterschrammel Apr 17, 2019

allredj reviewed Apr 17, 2019

View reviewed changes

romainbrenguier force-pushed the clean-up/parse-options-messages branch from f075f24 to 46ec583 Compare April 17, 2019 09:55

allredj reviewed Apr 17, 2019

View reviewed changes

romainbrenguier added 7 commits April 17, 2019 14:18

Remove redundant get_ui() method

4268bee

ui_message_handler.get_ui() already does the same thing, and is more explicit.

Remove comment made unecessary

0d9f751

Now the log field gets initialized before parse_options_baset is constructed so there is no danger as described in the comment.

Replace log.get_message_handler() calls

edd2c65

The calls will always return a reference to the field ui_message_handler which can be accessed directly instead.

Remove unecessary log argument in cbmc_parse_optionst

1d09894

The messaget can be constructed from the message_handler.

Show properties take a ui_message_handlert

747e13b

This is more precise on the type of message handler we are expecting and makes the ui argument redundant.

show_goto_functions takes a ui_message_handler

262cc35

This removes the need for passing a seperate ui argument.

romainbrenguier force-pushed the clean-up/parse-options-messages branch from 46ec583 to 262cc35 Compare April 17, 2019 13:38

allredj reviewed Apr 17, 2019

View reviewed changes

peterschrammel approved these changes Apr 18, 2019

View reviewed changes

tautschnig merged commit d535b09 into diffblue:develop Apr 18, 2019

romainbrenguier deleted the clean-up/parse-options-messages branch April 18, 2019 07:54

Clean-up message_handler of parse_options_baset #4521

Clean-up message_handler of parse_options_baset #4521

Uh oh!

Conversation

romainbrenguier commented Apr 12, 2019 • edited by peterschrammel Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

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

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

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Apr 17, 2019

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!

Uh oh!

romainbrenguier commented Apr 12, 2019 •

edited by peterschrammel

Loading