cleanup array theory solver #1145

kroening · 2017-07-16T16:17:41Z

Use ranged for
Use full index_exprt constructors
Cleaned out unused method prototype

tautschnig

See detailed comments; also I don't see how this PR delivers on "Use full index_exprt constructors" or
"Cleaned out unused method prototype".

tautschnig · 2017-07-17T06:28:13Z

src/solvers/flattening/arrays.cpp

+    for(const auto & i2 : i1.second)
+      std::cout << "Index set (" << i1.first << " = "
+                << arrays.find_number(i1.first) << " = "
+                << from_expr(ns, "", arrays[arrays.find_number(i1.first)])
                << "): "
                << from_expr(ns, "", *i2) << '\n';


This no longer compiles, it should be i2 instead of *i2

tautschnig · 2017-07-17T06:29:15Z

src/solvers/flattening/arrays.cpp

-      array_equalities.begin();
-      it!=array_equalities.end();
-      it++)
+  for(const auto & it : array_equalities)


Please use a name different from it as this isn't an iterator anymore (and avoid the space after & for consistency)

tautschnig · 2017-07-17T06:30:07Z

src/solvers/flattening/arrays.cpp

-        it=update_indices.begin();
-        it!=update_indices.end(); it++)
-      update_index_map(*it);
+    for(const auto & it : update_indices)


See above (not an iterator, space)

tautschnig · 2017-07-17T06:30:55Z

src/solvers/flattening/arrays.cpp

-      it=index_set.begin();
-      it!=index_set.end();
-      it++)
+  for(const auto & it : index_set)


See above (not an iterator, space)

tautschnig · 2017-07-17T06:32:35Z

src/solvers/flattening/arrays.cpp

-      it=index_set.begin();
-      it!=index_set.end();
-      it++)
+  for(const auto & it : index_set)
  {
    index_exprt index_expr1;


index_exprt index_expr1(array_equality.f1, it); instead of the multi-step assignment.

tautschnig · 2017-07-17T06:34:06Z

src/solvers/flattening/arrays.cpp

-      it=index_set.begin();
-      it!=index_set.end();
-      it++)
+  for(const auto & it : index_set)


See above (not an iterator, space); specifically use other_index to avoid the useless assignment below.

tautschnig · 2017-07-17T06:34:25Z

src/solvers/flattening/arrays.cpp

  {
-    exprt other_index=*it;
+    exprt other_index=it;


See above (multiple)

tautschnig · 2017-07-17T06:34:48Z

src/solvers/flattening/arrays.cpp

-      it=index_set.begin();
-      it!=index_set.end();
-      it++)
+  for(const auto & it : index_set)


tautschnig · 2017-07-17T06:34:57Z

src/solvers/flattening/arrays.cpp

  {
    index_exprt index_expr1;
    index_expr1.type()=ns.follow(expr.type()).subtype();
    index_expr1.array()=expr;
-    index_expr1.index()=*it;
+    index_expr1.index()=it;


tautschnig · 2017-07-17T06:37:50Z

src/solvers/flattening/arrays.cpp

-      it=index_set.begin();
-      it!=index_set.end();
-      it++)
+  for(const auto & it : index_set)


kroening · 2017-07-17T10:26:27Z

Many thanks, should now be all done.

tautschnig · 2017-07-17T10:27:31Z

Many thanks, should now be all done.

The linter isn't quite happy yet? (Stray whitespace at end of line.)

tautschnig · 2017-07-17T10:29:01Z

src/solvers/flattening/arrays.cpp

-    index_expr.type()=array_type.subtype();
-    index_expr.array()=a.op0();
-    index_expr.index()=a.op1();
+    index_exprt index_expr(a.op0(), a.op1(), array_type.subtype());


Nit picking: the third operand is unnecessary. Also: would it be possible to use to_with_expr above so that the rather anonymous a.op0() and a.op1() become more readable?

tautschnig · 2017-07-17T10:31:23Z

src/solvers/flattening/arrays.cpp

-    index_expr.type()=array_type.subtype();
-    index_expr.array()=a.op0();
-    index_expr.index()=a.op1();
+    index_exprt index_expr(a.op0(), a.op1(), array_type.subtype());


Same nit pick: the third operand...

tautschnig · 2017-07-17T10:32:08Z

src/solvers/flattening/arrays.cpp

-            index_expr1.type()=ns.follow(arrays[i].type()).subtype();
-            index_expr1.array()=arrays[i];
-            index_expr1.index()=*i1;
+            const typet &subtype=ns.follow(arrays[i].type()).subtype();


As above: I believe this is unnecessary.

There is a subtle difference here: the array type is anticipated to be a symbol, and the index_exprt() constructor doesn't consider that case.

I am hoping that the front-end doesn't generate these any more, which should be checked, followed by a clean-out of the ns.follow() expressions.

Wouldn't later bitvector conversion do any such namespace lookups anyway (if needed)? (Anyhow I do agree that the front-end should not even be generating any symbol types for arrays.)

No, the arrays handled by the array theory solver won't get touched by bitvector conversion.

Yes, this code should be obsolete; symbol types are only to be generated for structs (and should eventually get replaced by struct_tag types).

Hmm, wouldn't prop.l_set_to_true(convert(...)) eventually see those equalities?

Yes, but that will then eventually pass it to the array decision procedure, without rewriting the types.

Sorry, I was on the wrong track, it's completely irrelevant what the later steps do or don't do as picking the subtype() of a symbol type wouldn't work (which the constructor uses).

For the C front-end, the only place that introduces symbol types is c_typecheck_baset::typecheck_compound_type.

As per #1148 this will be cleaned up in one go at a later stage. Removing all further comments about the use of ns.follow.

tautschnig · 2017-07-17T10:32:53Z

src/solvers/flattening/arrays.cpp

+      std::cout << "Index set (" << index_entry.first << " = "
+                << arrays.find_number(index_entry.first) << " = "
+                << from_expr(ns, "",
+                            arrays[arrays.find_number(index_entry.first)])


The indent here is a bit strange

tautschnig · 2017-07-17T10:35:21Z

src/solvers/flattening/arrays.cpp

-      it=index_set.begin();
-      it!=index_set.end();
-      it++)
+  for(auto other_index : index_set)


for(const auto &other_index : index_set) (to make sure this does not introduce any copies)

That won't work, as other_index may be changed later on; i.e., the copy is intentional.

My apologies, I should have looked at more context.

tautschnig · 2017-07-18T09:15:43Z

src/solvers/flattening/arrays.cpp

-      index_expr2.index()=*it;
+      const typet &subtype=ns.follow(expr.type()).subtype();
+      index_exprt index_expr1(expr, index, subtype);
+      index_exprt index_expr2(expr.op0(), index, subtype);

      assert(index_expr1.type()==index_expr2.type());


I note that this assertion is trivially true at present (and had been trivially true before), but wouldn't necessarily be so if the third argument to the constructors were omitted.

Removed the very trivial assertions.

tautschnig · 2017-07-19T07:19:36Z

src/solvers/flattening/arrays.cpp

@@ -111,21 +111,20 @@ void arrayst::collect_arrays(const exprt &a)
    if(a.operands().size()!=3)


This check is now unnecessary given the use of to_with_expr (which does that check).

Indeed, gone

tautschnig · 2017-07-19T07:20:48Z

src/solvers/flattening/arrays.cpp

-    index_expr.type()=array_type.subtype();
-    index_expr.array()=a.op0();
-    index_expr.index()=a.op1();
+    index_exprt index_expr(a.op0(), a.op1());


Please use update_exprt (to_update_expr)

tautschnig · 2017-07-19T07:26:38Z

src/solvers/flattening/arrays.cpp

@@ -564,17 +524,9 @@ void arrayst::add_array_constraints_with(

      if(guard_lit!=const_literal(true))


Just curious: would it also make sense to special-case guard_lit==const_literal(false)?

That case should not exist.

Why is that the case?

tautschnig · 2017-07-19T07:28:05Z

I'm sorry that I keep suggesting/requesting more changes - this code just appears to have so much room for cleanup...

kroening requested review from tautschnig and martin-cs July 16, 2017 16:17

kroening force-pushed the array_cleanup branch from 1c30d9a to 3695855 Compare July 16, 2017 16:42

tautschnig requested changes Jul 17, 2017

View reviewed changes

kroening force-pushed the array_cleanup branch 3 times, most recently from 78ce76d to 7f29114 Compare July 17, 2017 10:26

kroening force-pushed the array_cleanup branch from 7f29114 to 22df291 Compare July 17, 2017 10:27

tautschnig reviewed Jul 17, 2017

View reviewed changes

kroening force-pushed the array_cleanup branch from 22df291 to 996c0d3 Compare July 17, 2017 19:07

tautschnig reviewed Jul 18, 2017

View reviewed changes

kroening force-pushed the array_cleanup branch from 996c0d3 to 6eb1977 Compare July 18, 2017 20:00

tautschnig reviewed Jul 19, 2017

View reviewed changes

tautschnig added the cleanup label Jul 19, 2017

cleanup array theory solver

f4c79a6

kroening force-pushed the array_cleanup branch from 6eb1977 to f4c79a6 Compare July 19, 2017 11:56

tautschnig approved these changes Jul 19, 2017

View reviewed changes

tautschnig merged commit 4577401 into master Jul 20, 2017

tautschnig deleted the array_cleanup branch July 20, 2017 18:24

tautschnig mentioned this pull request Aug 3, 2017

Merge master 2017-08-03 #1204

Merged

		@@ -111,21 +111,20 @@ void arrayst::collect_arrays(const exprt &a)
		if(a.operands().size()!=3)

		@@ -564,17 +524,9 @@ void arrayst::add_array_constraints_with(

		if(guard_lit!=const_literal(true))

cleanup array theory solver #1145

cleanup array theory solver #1145

Uh oh!

Conversation

kroening commented Jul 16, 2017

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!

kroening commented Jul 17, 2017

Uh oh!

tautschnig commented Jul 17, 2017

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!

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!

tautschnig commented Jul 19, 2017