Stop propt inheriting from messaget [blocks: #3800] #3249

romainbrenguier · 2018-10-30T06:40:13Z

No functional changes.
A propt object should not be used as a messaget so the messaget should
rather be a field.

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] 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.

tautschnig

Overall I think this is a very good idea.

The reason for me requesting changes is the (seemingly?) unrelated change as noted below.
More of a comment than a strict requirement: let's not do this set_message_handler game, but instead make the propt constructor take a message_handlert& and set things up in the constructor.

tautschnig · 2018-10-30T08:27:45Z

src/solvers/prop/prop_conv.h

@@ -117,7 +117,6 @@ class prop_conv_solvert:public prop_convt
  typedef std::map<irep_idt, literalt> symbolst;
  typedef std::unordered_map<exprt, literalt, irep_hash> cachet;

-  const cachet &get_cache() const { return cache; }


Unrelated change?

yes sorry, this shouldn't be in this PR

kroening · 2018-10-30T08:34:06Z

This will introduce a lot of noise, if done consistently, and the benefit isn't obvious?

tautschnig · 2018-10-30T08:40:52Z

To me, the benefit would be fixing a design flaw (the "is-a" relationship seems wrong), but maybe I'm missing something?

peterschrammel

I'm generally in favour of doing that if we do it across the entire code base. It's a lot of churn, but not really much breaking changes as we are mostly passing around message_handlert.
We should then also add a rule to the coding standard that (ui_)message_handlert is passed through the constructor instead of a setter and decide on a consistent name for the messaget member, eg one of message, msg, log or logger.

tautschnig · 2018-10-30T08:59:26Z

+1 to all that @peterschrammel said, but also I'd like to hear more from @kroening as he seemed to be less happy with the route being taken.

romainbrenguier · 2018-11-02T10:30:43Z

@peterschrammel I'm not sure why we have to do it across the whole code base at the same time? Is it just a naming issue? message is the natural name for an object of type messaget but maybe messaget is not well chosen, loggert would have been better.

martin-cs · 2018-11-06T14:05:18Z

Kind of agree with the discussion above. Let's be consistent; either inherit from or parameter to construction (do we ever swap the message output source? If not, let's just have it as part of the constructor), a slow migration seems painful. Is it worth doing ... unclear to me.

romainbrenguier · 2018-11-08T07:56:58Z

@martin-cs

Kind of agree with the discussion above. Let's be consistent; either inherit from or parameter to construction (do we ever swap the message output source? If not, let's just have it as part of the constructor), a slow migration seems painful. Is it worth doing ... unclear to me.

For me it's clearly worth doing. If someone is trying to understand this code, the first thing they see is what the class inherits from, then they wonder "why is a decision procedure a message?", then they dig into messaget and realize it doesn't really represent messages but still has no link with what a solver should intuitively do, and they are left confused before having learned anything useful about solvers.

tautschnig · 2018-11-08T08:11:15Z

From me to change my review to "approve" I'd ask for a proper constructor to be used, the member really shouldn't (need to) be public. As far as naming is concerned, let's try to set a precedent here: whatever is chosen here should make people happy and should over time be used elsewhere. (Personally I think something along the lines of logger is better, but mostly I'd just like to have consistency over time, whatever the name.)

romainbrenguier · 2018-11-09T10:44:47Z

@tautschnig I've added fixup commits to make the field protected, rename it to log (we use log in goto_symext already), and set the message handler through the constructor where needed. It's maybe better not to review commit by commit now as they will be squashed into just one.
Another point we may want to discuss is whether log should be mutable or not.

tautschnig

As stated below, I'd propose an even stricter regime and only keep constructors that pass the message handler.

tautschnig · 2018-11-09T10:47:42Z

src/solvers/prop/prop.h

@@ -21,10 +21,11 @@ Author: Daniel Kroening, [email protected]

 /*! \brief TO_BE_DOCUMENTED
 */
-class propt:public messaget
+class propt
 {
 public:
  propt() { }


Hmm, don't you need to consume a message_handlert here?

I wasn't there before so adding one instead of constructing a new one could potentially change the behavior.

Yes, it makes things safer, so I'd happily take that change.

tautschnig · 2018-11-09T10:49:57Z

src/solvers/sat/dimacs_cnf.cpp

@@ -19,6 +19,11 @@ dimacs_cnft::dimacs_cnft():break_lines(false)
 {
 }

+dimacs_cnft::dimacs_cnft(message_handlert &message_handler) : dimacs_cnft()
+{
+  log.set_message_handler(message_handler);


This is going to be a bit painful, but let's please try to use the constructor all the way, i.e., it would be dimacs_cnft(message_handler) above.

That sounds like a good idea but this would go a bit beyond scope of a refactoring PR, and my initial statement "No functional changes." wouldn't be strictly true anymore.

Well, if we have no bugs (surely true) then it wouldn't entail any functional changes, because each time we construct a dimacs_cnft we surely also initialized its message handler.

It we leave it initialized, doesn't it just means that some messages wouldn't get printed? This would be difficult to detect. It's also a bit difficult to manually check, as a lot of classes inherit from dimacs_cnft...

I think any introduced functional change is a strict improvement here. Any class deriving should be forced to call a constructor that takes a message handler.

tautschnig · 2018-11-09T10:50:15Z

src/solvers/sat/dimacs_cnf.h

@@ -18,6 +18,7 @@ class dimacs_cnft:public cnf_clause_listt
 {
 public:
  dimacs_cnft();


Please remove this constructor.

allredj

⚠️
Diffblue compatibility check is currently unavailable.
Please create manual bump.
(cbmc commit: b7aeac9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90838766

LAJW

Magnificent

tautschnig

Approving for now (but needs a rebase), the changes I had requested will happen as part of #3800.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: de1a8f0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99395288

tautschnig · 2019-02-01T10:14:22Z

src/solvers/sat/satcheck_minisat2.cpp

@@ -238,21 +238,21 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()

        if(solver_result==l_True)
        {
-          messaget::status() <<
-            "SAT checker: instance is SATISFIABLE" << eom;
+          log.status() << "SAT checker: instance is SATISFIABLE"


Line 230 also needs to be updated (Windows build).

tautschnig · 2019-02-01T10:17:26Z

src/solvers/flattening/arrays.cpp

@@ -580,7 +580,7 @@ void arrayst::add_array_constraints_update(

    if(index_expr.type()!=value.type())
    {
-      prop.error() << expr.pretty() << messaget::eom;
+      prop.message.error() << expr.pretty() << messaget::eom;


This change (inside a #if 0 block) looks suspicious: I believe this should be just error().

No functional changes. A propt object should not be used as a messaget so the messaget should rather be a field.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 756b003).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99448369

romainbrenguier requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, smowton and tautschnig as code owners October 30, 2018 06:40

romainbrenguier added Solvers cleanup labels Oct 30, 2018

romainbrenguier force-pushed the refactor/propt-messaget branch from c372326 to 8d49b96 Compare October 30, 2018 06:46

tautschnig requested changes Oct 30, 2018

View reviewed changes

tautschnig assigned romainbrenguier Oct 30, 2018

peterschrammel reviewed Oct 30, 2018

View reviewed changes

romainbrenguier force-pushed the refactor/propt-messaget branch from 8d49b96 to b055e6b Compare October 30, 2018 08:59

romainbrenguier requested a review from LAJW October 30, 2018 09:04

romainbrenguier force-pushed the refactor/propt-messaget branch from b055e6b to 7af156d Compare November 2, 2018 10:35

romainbrenguier force-pushed the refactor/propt-messaget branch from 7af156d to b7aeac9 Compare November 9, 2018 09:57

tautschnig reviewed Nov 9, 2018

View reviewed changes

allredj reviewed Nov 9, 2018

View reviewed changes

LAJW approved these changes Nov 15, 2018

View reviewed changes

tautschnig added the blocker label Jan 24, 2019

tautschnig changed the title ~~Stop propt inheriting from messaget~~ Stop propt inheriting from messaget [blocks: #3800] Jan 24, 2019

tautschnig added the Needs rebase label Jan 24, 2019

tautschnig approved these changes Jan 24, 2019

View reviewed changes

romainbrenguier force-pushed the refactor/propt-messaget branch 3 times, most recently from 863c4d6 to de1a8f0 Compare February 1, 2019 08:20

romainbrenguier removed the Needs rebase label Feb 1, 2019

allredj reviewed Feb 1, 2019

View reviewed changes

tautschnig reviewed Feb 1, 2019

View reviewed changes

romainbrenguier force-pushed the refactor/propt-messaget branch from de1a8f0 to 2d9a3c1 Compare February 1, 2019 12:59

Stop propt inheriting from messaget

756b003

No functional changes. A propt object should not be used as a messaget so the messaget should rather be a field.

romainbrenguier force-pushed the refactor/propt-messaget branch from 2d9a3c1 to 756b003 Compare February 1, 2019 15:44

allredj reviewed Feb 1, 2019

View reviewed changes

tautschnig merged commit 4aa485f into diffblue:develop Feb 1, 2019

Stop propt inheriting from messaget [blocks: #3800] #3249

Stop propt inheriting from messaget [blocks: #3800] #3249

Uh oh!

Conversation

romainbrenguier commented Oct 30, 2018

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!

kroening commented Oct 30, 2018

Uh oh!

tautschnig commented Oct 30, 2018

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Oct 30, 2018

Uh oh!

romainbrenguier commented Nov 2, 2018

Uh oh!

martin-cs commented Nov 6, 2018

Uh oh!

romainbrenguier commented Nov 8, 2018

Uh oh!

tautschnig commented Nov 8, 2018

Uh oh!

romainbrenguier commented Nov 9, 2018

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

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

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

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!