Partial cleanup in solver code #1810

romainbrenguier · 2018-02-08T09:26:20Z

This regroup several commits that do only small refactoring changes in the solver module.
The goal is to improve clarity and use the same conventions as elsewhere (for instance use invariant
instead of assert or throw).

LAJW

These are all great changes, I cannot approve them enough.

tautschnig

Most of the changes are great, some need review as indicated. (A common theme: please don't remove blank lines that serve as conceptual separators. Wedon'tpaysomeper-linepriceandwhitespaceisreallyusefultohumanreaders.)

The request-for-changes is for a bit that I haven't seen any comment on: what are the performance differences?

tautschnig · 2018-02-08T12:49:24Z

src/solvers/prop/prop_conv.h

  bool use_cache;
  bool equality_propagation;
  bool freeze_all; // freezing variables (for incremental solving)
+  virtual optionalt<literalt> literal(const exprt &expr) const;


I don't know why this line was moved, but certainly the comment must move together with it.

I moved it back

tautschnig · 2018-02-08T12:56:05Z

src/solvers/prop/prop_conv.h

-    use_cache(true),
-    equality_propagation(true),
-    freeze_all(false),
-    post_processing_done(false),


" Initialize at declaration instead of construction

This avoids having to initialize them the same way in all constructors."

There just seems to be a single constructor - what sort of story is being made up here?!

Should another constructor be added in the future (copy, move, default, overload of existing constructor), we'll have one set of default arguments, and the user won't have to repeat himself. Also, they're much easier to look up now - they're just when the values are declared. No need to dig through the .cpp file looking for the constructor that isn't there.

I get your point, but I don't want to be lied to in the commit message.

They will always be initialised upon construction, the declaration is just a syntactic construct.

There just is one constructor at this time, so don't use the plural.

If the commit message said what your comment said, all would be well.

I updated the commit message.

tautschnig · 2018-02-08T13:00:36Z

src/solvers/prop/prop_conv.h

@@ -110,14 +110,14 @@ class prop_conv_solvert:public prop_convt

  virtual void clear_cache() { cache.clear();}

-  typedef std::map<irep_idt, literalt> symbolst;
-  typedef std::unordered_map<exprt, literalt, irep_hash> cachet;


Please don't do this. Type names also carry useful information about what a data structure is intended to hold/do.

typedefs do the opposite. Especially when concealing standard data structure, such as map. When reading code using typedefs this way one might think that cachet and symbolst is a user-defined class that needs special treatment. When explicitly written as std:::vector or std::map the interface and structure of the variable becomes obvious. The name of the variable should signify intent, not the type alias.

As you please.

symbolst is not great here, but cachet actually conveys intent.
Unless the typedef is only used once, I'm strongly in favour of using typedefs, in particular at interfaces.
If you think that typedefs hide information then you should use an IDE that solves that problem for you.

Yeah; even if used once, these can still be worth having.

I think symbolst is misleading (you would expect a vector of symbolt). cachet does carry the intent but it's already present in the variable name (cache).

tautschnig · 2018-02-08T13:19:45Z

src/solvers/flattening/boolbv.cpp

+  if(auto s = numeric_cast<mp_integer>(size))
+    return unbounded_array == unbounded_arrayt::U_AUTO &&
+           *s > MAX_FLATTENED_ARRAY_SIZE;
+  return true;


To be honest, I don't see how this is a "simplification". I'd much more accept that if you really gathered all the bits together. How about this:

if(type.id()==ID_symbol) return is_unbounded_array(ns.follow(type)); const exprt &size=to_array_type(type).size(); return type.id() == ID_array && (unbounded_array == unbounded_arrayt::U_ALL || !(auto s = numeric_cast<mp_integer>(size)) || (unbounded_array == unbounded_arrayt::U_AUTO && *s > MAX_FLATTENED_ARRAY_SIZE));

return (auto s = func()) && s > 0) is not valid C++. if-declarations are allowed, but not this.

Ok, thanks, so just declare s beforehand and just do the assignment in there.

Yeah; not sure this change is actually a simplification. Also -- what problem is this solving?

Changed according to Michael's comment.

tautschnig · 2018-02-08T13:21:17Z

src/solvers/flattening/boolbv.cpp

  bv_sub.resize(bv.size());

  for(std::size_t i=0; i<bv.size(); i++)
    bv_sub[i].id(std::to_string(bv[i].get()));
+  return dest;


Nit pick: a blank line before returnwould help readability.

I'd say removing double blank lines before this for loop would.

tautschnig · 2018-02-08T13:32:23Z

src/solvers/flattening/boolbv.cpp

-        << it.second.get_value(prop) << '\n';
-  }
+  for(const auto &pair : map.mapping)
+    out << pair.first << "=" << pair.second.get_value(prop) << '\n';


The commit message doesn't really reflect what happened here (which mainly is renaming it -> pair (which is good).

I changed the commit message: d400deb

tautschnig · 2018-02-08T13:33:34Z

src/solvers/flattening/boolbv_abs.cpp

  if(width==0)
    return conversion_failed(expr);
-


Please stop removing blank lines that clearly separate steps. Code readability matters. Really.

tautschnig · 2018-02-08T13:44:08Z

src/solvers/flattening/boolbv_index.cpp

-#ifdef COMPACT_EQUAL_CONST
-      bv_utils.equal_const_register(convert_bv(index));  // Definitely
-      bv_utils.equal_const_register(convert_bv(result)); // Maybe
-#endif


Where is this gone?

tautschnig · 2018-02-08T13:46:51Z

src/solvers/flattening/boolbv_index.cpp

-
-#ifdef COMPACT_EQUAL_CONST
-      bv_utils.equal_const_register(convert_bv(index));  // Definitely
-#endif


Again, where is this gone?

tautschnig · 2018-02-08T13:46:59Z

src/solvers/flattening/boolbv_index.cpp

-
-#ifdef COMPACT_EQUAL_CONST
-      bv_utils.equal_const_register(convert_bv(index));  // Definitely
-#endif


martin-cs · 2018-02-08T14:20:34Z

I'll try to work through the commits as some of these are "yes, we should have done this years ago" and others seem problematic. As for the white-space removal -- I though the whole point of the long and bloody campaign to get clang-format working was so that we didn't have to argue about this. I'll check how many of my patch sets are broken by these changes as well.

peterschrammel · 2018-02-14T22:27:14Z

src/solvers/flattening/boolbv_mult.cpp

  const exprt &op0=expr.op0();
-
-  bool no_overflow=expr.id()=="no-overflow-mult";
+  const bool no_overflow = expr.id() == "no-overflow-mult";


Would be good to add an irepid for this.

Actually it does not seem any exprt gets this id anywhere. So it may be better to just remove it. And same thing with the other no-overflows

@kroening Is there code elsewhere that generates no-overflow variants of the arithmetic expressions?

If there isn't then there should be; it is useful to know whether overflow matters or not / can be ignored. Especially for multiplication.

peterschrammel · 2018-02-14T22:33:15Z

src/solvers/prop/prop_conv.h

+  {
+    prop.set_frozen(a);
+  }
+  void set_assumptions(const bvt &_assumptions) override


the formatting of these one-line functions is inconsistent

Also unnecessary IMHO.

martin-cs

About half of this patch set is brilliant and changes we should have made ages ago and we really should merge. Then there is a fair amount of reformatting and whitespace changes plus a few API changes which are wrong IMHO.

martin-cs · 2018-02-15T14:11:58Z

src/solvers/flattening/boolbv.cpp

-  const exprt &expr,
-  const std::size_t bit,
-  literalt &dest) const
+optionalt<literalt>


I don't see why this change is needed. If there is a real error then an exception should be thrown. If not then returning constant literals is acceptable.

The function is not returning a constant literal when there is an error, it is just leaving dest untouched. So this is not changing the behavior of the function, just making the interface clearer.

May I suggest a different route: please just #ifdef 0 this code. Whether you change the interface to an optionalt I don't care as much then. (Background: I wanted to figure out whether throwing an exception would be fine. I couldn't tell, because the code is never used.)

Not sure I get your comment. If I #ifdef 0 the function when cbmc will not build because get_bool is called from somewhere.

Sorry, this is not about get_bool, but about literal (both boolbvt::literal and prop_convt::literal).

martin-cs · 2018-02-15T14:13:14Z

src/solvers/prop/prop_conv.h

@@ -128,7 +128,7 @@ class prop_conv_solvert:public prop_convt
  bool post_processing_done;

  // get a _boolean_ value from counterexample if not valid
-  virtual bool get_bool(const exprt &expr, tvt &value) const;
+  virtual optionalt<tvt> get_bool(const exprt &expr) const;


Again; this doesn't seem broken and so doesn't need to be fixed. If someone gives a true expression in then it is perfectly OK to give a true literal back.

Again, this doesn't change the behavior. The interface as it was before is confusing because you would think that the result of get_bool is the returned bool, while in fact it is stored in tvt &value (your comment makes me think you are confused yourself). Using optional makes it much clearer that it's actually a tvt which is the result.

(note to myself) the documentation should be updated.

martin-cs · 2018-02-15T14:14:32Z

src/solvers/prop/prop_conv.cpp

@@ -305,29 +305,13 @@ literalt prop_conv_solvert::convert_rest(const exprt &expr)

 bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr)
 {
-  if(!equality_propagation)
+  if(!equality_propagation || expr.lhs().id() != ID_symbol)


Why is this changed -- what problem does this solve?

Maybe it's subjective but I find the second version much more readable.
The problems were missing const, uninformative result variable name, confusing fall through in the case of result.second being false.

martin-cs · 2018-02-15T14:17:06Z

src/solvers/prop/prop_conv.cpp


    bvt bv;
-


Whitespace changes should be in their own commit.

I reverted this change

martin-cs · 2018-02-15T14:18:34Z

src/solvers/prop/prop_conv.h

@@ -110,14 +110,14 @@ class prop_conv_solvert:public prop_convt

  virtual void clear_cache() { cache.clear();}

-  typedef std::map<irep_idt, literalt> symbolst;
-  typedef std::unordered_map<exprt, literalt, irep_hash> cachet;


Yeah; even if used once, these can still be worth having.

martin-cs · 2018-02-15T14:48:16Z

src/solvers/flattening/boolbv_mult.cpp

-      if(op.size()!=width)
-        throw "convert_mult: unexpected operand width";
-
+      INVARIANT(op.size() == width, "convert_mult: unexpected operand width");


DATA_INVARIANT

or CHECK_RETURN, but not just a plain INVARIANT

martin-cs · 2018-02-15T14:48:25Z

src/solvers/flattening/boolbv_mult.cpp

-    if(op0.type()!=expr.type())
-      throw "multiplication with mixed types";
-
+    INVARIANT(op0.type() == expr.type(), "multiplication with mixed types");


DATA_INVARIANT

martin-cs · 2018-02-15T14:48:35Z

src/solvers/flattening/boolbv_mult.cpp

-    if(bv.size()!=width)
-      throw "convert_mult: unexpected operand width";
-
+    INVARIANT(bv.size() == width, "convert_mult: unexpected operand width");


DATA_INVARIANT

I'm not sure about this one, it's more like we are checking that convert_bv did its work correctly.

OK, CHECK_RETURN then.

martin-cs · 2018-02-15T14:48:43Z

src/solvers/flattening/boolbv_mult.cpp

-      if(it->type()!=expr.type())
-        throw "multiplication with mixed types";
-
+      INVARIANT(it->type() == expr.type(), "multiplication with mixed types");


DATA_INVARIANT

Actually CHECK_RETURN.

martin-cs · 2018-02-15T14:49:27Z

src/solvers/prop/prop_conv.h

+  {
+    prop.set_frozen(a);
+  }
+  void set_assumptions(const bvt &_assumptions) override


Also unnecessary IMHO.

tautschnig

In addition to my comment below, on the discussion of get_bool: it's probably not on a hot path so changing the interface isn't that a big deal. Actually it just has a single user in prop_conv_solvert::get.

Edit: shouldn't get_bool just 1. throw an exception if the expression type is not ID_bool and 2. return TV_UNKNOWN in all those cases where it presently returns true?

tautschnig · 2018-02-23T11:04:32Z

src/solvers/flattening/boolbv.cpp

-  const exprt &expr,
-  const std::size_t bit,
-  literalt &dest) const
+optionalt<literalt>


May I suggest a different route: please just #ifdef 0 this code. Whether you change the interface to an optionalt I don't care as much then. (Background: I wanted to figure out whether throwing an exception would be fine. I couldn't tell, because the code is never used.)

martin-cs · 2018-03-01T16:08:03Z

@romainbrenguier (author), @tautschnig (reviewer), @peterschrammel (other owner) how should we handle this? As it's now 43 commits it seems a little unwieldy and I'm worried that the majority of patches which are fine might get forgotten while we discuss the few controversial ones. Would it be entirely implausible to think of a meeting with three of us to work through and merge things?

romainbrenguier · 2018-03-02T09:07:48Z

@martin-cs what I could first do is make a separate PR with the non controversial commits, could you list the ones that you think are ready to go (or the opposite)? I would be ok with a meeting but when can it happen?

tautschnig · 2018-03-02T09:10:48Z

@romainbrenguier Would you mind merging the fix-ups into their corresponding commits so that we have a clean list to mark as (non-)controversial?

romainbrenguier · 2018-03-02T09:45:27Z

@tautschnig done

tautschnig · 2018-03-02T10:09:19Z

I'd list the following as straight forward:

Assert replaced by unreachable
Use ranged for
Renaming it to symbol
Initialize at declaration instead of construction
Remove virtual keyword where not needed (if restricted to what the commit subject says)
Replace throws by invariant or preconditions
Remove useless includes
Use auto for iterator types
Use standard algorithm for finding an element
Simplify dec_solve
Remove useless comments
Simplify loop in prop_conv::get
Remove useless virtual (though it should be squashed with "Remove virtual keyword" above)
Make make_(free_)bv_expr return exprt
Simplify boolbvt::set_to
Rename it to pair in boolbvt::print_assignment

The others vary in the amount of discussion required. Many of them include good changes mixed with unnecessary ones. All those that include changing throw ... -> INVARIANT should be discussed as there are design issues.

martin-cs · 2018-03-02T14:05:07Z

src/solvers/flattening/boolbv_bitwise.cpp

@@ -64,13 +55,13 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
          else if(expr.id()==ID_bitxnor)
            bv[i]=prop.lequal(bv[i], op[i]);
          else
-            throw "unexpected operand";
+            UNIMPLEMENTED;


Maybe UNHANDLED_CASE?

martin-cs · 2018-03-02T14:05:23Z

src/solvers/flattening/boolbv_bitwise.cpp

        }
      }
    }

    return bv;
  }

-  throw "unexpected bitwise operand";
+  UNIMPLEMENTED;


Maybe UNHANDLED_CASE?

martin-cs · 2018-03-02T14:07:46Z

src/solvers/flattening/boolbv_index.cpp

-        "__CPROVER_internal_actual_array_"+
-        std::to_string(actual_array_counter++);
+      const std::string identifier = "__CPROVER_internal_actual_array_" +
+                                     std::to_string(actual_array_counter++);


Use CPROVER_PREFIX

martin-cs · 2018-03-02T14:15:05Z

Things I feel are straight forward:
Assert replaced by unreachable
Use ranged for
Remove useless includes
Use auto for iterator types
Simplify loop in prop_conv::get
Remove useless virtual
Make make_(free_)bv_expr return exprt
Replacing throws by invariants in boolbv convert
Make build_offset_map return an offset_mapt
Rename it to pair in boolbvt::print_assignment
Remove useless throws in boolbvt::convert_index
Refactoring in boolbvt::convert_abs
Refactoring in boolbvt::convert_bitwise
Refactoring in boolbvt::convert_byte_extract

Things that I am ambivalent about and if @tautschnig thinks they are clear cut, then let's have them in:
Refactoring set_equality_to_true
Renaming it to symbol
Initialize at declaration instead of construction
Remove virtual keyword where not needed
Replace throws by invariant or preconditions
Use standard algorithm for finding an element
Simplify dec_solve
Remove useless comments
Rename SUB in baset
Simplify is_unbounded_array
Simplify boolbvt::set_to
Refactoring in boolbvt::convert_add_sub
Refactoring in boolbvt::convert_array_of
Refactoring in boolbvt::convert_index
Refactoring in boolbvt::convert_mult
Reformat one line functions

Things I think need more discussion:
Make literal return an optional
Make get_bool return a optional
Do not use typedef for types used only once
Refactoring in boolbvt::convert_array

HTH

romainbrenguier · 2018-03-20T08:14:10Z

@martin-cs @tautschnig thanks for making these lists of commits, here is a first PR in which I just selected the intersection of what Michael considers straightforward and what Martin considers straightforward or is ambivalent #1950
Sorry for the delay (I have other PRs to take care of and which were more urgent than this one)

martin-cs · 2018-03-20T08:20:42Z

No worries about the delay and that you for persevering. I'll have a look after today's deadline.

romainbrenguier · 2018-03-21T15:54:10Z

Another set of commits which Martin listed as straightforward #1956

martin-cs · 2018-05-17T19:13:49Z

@romainbrenguier My apologies this stalled; will pick up on #1956

This is clearer than a boolean signaling an error

The class actualy designated by this is a base class and not a subclass, so baset is clearer.

Factor out is_uniform function to reduce size of big function and make it clearer. Add const keyword where possible. Change assertions in INVARIANTS. Remove blank lines that are not helping clarity (for example between comments and instructions to which they apply). Use numeric_cast instead of to_integer.

romainbrenguier · 2018-09-28T06:45:04Z

Most commits have been merged via other PRs so I'm closing this one.

romainbrenguier requested a review from LAJW February 8, 2018 09:26

romainbrenguier requested review from kroening, martin-cs, peterschrammel, smowton and tautschnig as code owners February 8, 2018 09:26

romainbrenguier force-pushed the refactor/prop_conv branch from 7362161 to e9742ac Compare February 8, 2018 09:26

LAJW approved these changes Feb 8, 2018

View reviewed changes

romainbrenguier force-pushed the refactor/prop_conv branch 3 times, most recently from f200f2b to b0ead02 Compare February 8, 2018 12:19

tautschnig requested changes Feb 8, 2018

View reviewed changes

peterschrammel reviewed Feb 14, 2018

View reviewed changes

romainbrenguier force-pushed the refactor/prop_conv branch from d6e8668 to 1071652 Compare February 15, 2018 10:47

martin-cs requested changes Feb 15, 2018

View reviewed changes

tautschnig assigned romainbrenguier Feb 21, 2018

tautschnig reviewed Feb 23, 2018

View reviewed changes

romainbrenguier force-pushed the refactor/prop_conv branch 5 times, most recently from 1311f15 to bfeac6d Compare February 23, 2018 14:12

romainbrenguier force-pushed the refactor/prop_conv branch from bfeac6d to 58dc939 Compare March 2, 2018 09:45

martin-cs reviewed Mar 2, 2018

View reviewed changes

romainbrenguier force-pushed the refactor/prop_conv branch from 58dc939 to ee3ac60 Compare March 20, 2018 07:35

romainbrenguier mentioned this pull request Mar 20, 2018

Partial solver cleanup (straightforward changes) #1950

Merged

romainbrenguier force-pushed the refactor/prop_conv branch from ee3ac60 to c61a5d8 Compare March 21, 2018 15:20

romainbrenguier mentioned this pull request Mar 21, 2018

Partial solver cleanup (straightforward changes part 2) #1956

Merged

romainbrenguier added the Needs rebase label Jun 13, 2018

romainbrenguier added 10 commits June 13, 2018 09:42

Make literal return an optional

79cb900

This is clearer than a boolean signaling an error

Make get_bool return a optional

fd7af72

Refactoring set_equality_to_true

16ae7dd

Rename SUB in baset

eedf20e

The class actualy designated by this is a base class and not a subclass, so baset is clearer.

Simplify is_unbounded_array

444bf14

Refactoring in boolbvt::convert_add_sub

4c9364b

Refactoring in boolbvt::convert_array

2333436

Refactoring in boolbvt::convert_array_of

c41e26d

Refactoring in boolbvt::convert_mult

1e4e071

romainbrenguier force-pushed the refactor/prop_conv branch from c61a5d8 to 1e4e071 Compare June 13, 2018 08:47

romainbrenguier removed the Needs rebase label Jun 13, 2018

romainbrenguier closed this Sep 28, 2018

Partial cleanup in solver code #1810

Partial cleanup in solver code #1810

Conversation

romainbrenguier commented Feb 8, 2018

LAJW left a comment

Choose a reason for hiding this comment

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

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

LAJW Feb 8, 2018 • 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

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

martin-cs commented Feb 8, 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

Choose a reason for hiding this comment

martin-cs 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

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martin-cs commented Mar 1, 2018

romainbrenguier commented Mar 2, 2018

tautschnig commented Mar 2, 2018

romainbrenguier commented Mar 2, 2018

tautschnig commented Mar 2, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

martin-cs commented Mar 2, 2018

romainbrenguier commented Mar 20, 2018

martin-cs commented Mar 20, 2018 via email

romainbrenguier commented Mar 21, 2018

martin-cs commented May 17, 2018

LAJW Feb 8, 2018 •

edited

Loading

tautschnig left a comment •

edited

Loading