Merge pull request #1266 from tautschnig/array-debugging

[develop->master] Array debugging

Author: Daniel Kroening

src/solvers/flattening/arrays.cpp

@@ -8,9 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "arrays.h"
 
-#include <cassert>
-#include <iostream>
-
 #include <langapi/language_util.h>
 
 #include <util/std_expr.h>
@@ -21,6 +18,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/prop/prop.h>
 
+#ifdef DEBUG
+#include <iostream>
+#endif
+
 arrayst::arrayst(
   const namespacet &_ns,
   propt &_prop):equalityt(_ns, _prop)
@@ -48,11 +49,15 @@ literalt arrayst::record_array_equality(
   // check types
   if(!base_type_eq(op0.type(), op1.type(), ns))
   {
-    std::cout << equality.pretty() << '\n';
-    throw "record_array_equality got equality without matching types";
+    prop.error() << equality.pretty() << messaget::eom;
+    DATA_INVARIANT(
+      false,
+      "record_array_equality got equality without matching types");
   }
 
-  assert(ns.follow(op0.type()).id()==ID_array);
+  DATA_INVARIANT(
+    ns.follow(op0.type()).id()==ID_array,
+    "record_array_equality parameter should be array-typed");
 
   array_equalities.push_back(array_equalityt());
 
@@ -113,8 +118,8 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, with_expr.old().type(), ns))
     {
-      std::cout << a.pretty() << '\n';
-      throw "collect_arrays got 'with' without matching types";
+      prop.error() << a.pretty() << messaget::eom;
+      DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
     }
 
     arrays.make_union(a, with_expr.old());
@@ -131,8 +136,10 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, update_expr.old().type(), ns))
     {
-      std::cout << a.pretty() << '\n';
-      throw "collect_arrays got 'update' without matching types";
+      prop.error() << a.pretty() << messaget::eom;
+      DATA_INVARIANT(
+        false,
+        "collect_arrays got 'update' without matching types");
     }
 
     arrays.make_union(a, update_expr.old());
@@ -151,15 +158,15 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, if_expr.true_case().type(), ns))
     {
-      std::cout << a.pretty() << '\n';
-      throw "collect_arrays got if without matching types";
+      prop.error() << a.pretty() << messaget::eom;
+      DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
     // check types
     if(!base_type_eq(array_type, if_expr.false_case().type(), ns))
     {
-      std::cout << a.pretty() << '\n';
-      throw "collect_arrays got if without matching types";
+      prop.error() << a.pretty() << messaget::eom;
+      DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
     arrays.make_union(a, if_expr.true_case());
@@ -175,9 +182,10 @@ void arrayst::collect_arrays(const exprt &a)
   }
   else if(a.id()==ID_member)
   {
-    if(to_member_expr(a).struct_op().id()!=ID_symbol)
-      throw
-        "unexpected array expression: member with `"+a.op0().id_string()+"'";
+    DATA_INVARIANT(
+      to_member_expr(a).struct_op().id()==ID_symbol,
+      ("unexpected array expression: member with `"+
+       a.op0().id_string()+"'").c_str());
   }
   else if(a.id()==ID_constant ||
           a.id()==ID_array ||
@@ -190,20 +198,24 @@ void arrayst::collect_arrays(const exprt &a)
   else if(a.id()==ID_byte_update_little_endian ||
           a.id()==ID_byte_update_big_endian)
   {
-    assert(0);
+    DATA_INVARIANT(
+      false,
+      "byte_update should be removed before collect_arrays");
   }
   else if(a.id()==ID_typecast)
   {
     // cast between array types?
-    assert(a.operands().size()==1);
+    DATA_INVARIANT(
+      a.operands().size()==1,
+      "typecast must have one operand");
 
-    if(a.op0().type().id()==ID_array)
-    {
-      arrays.make_union(a, a.op0());
-      collect_arrays(a.op0());
-    }
-    else
-      throw "unexpected array type cast from "+a.op0().type().id_string();
+    DATA_INVARIANT(
+      a.op0().type().id()==ID_array,
+      ("unexpected array type cast from "+
+       a.op0().type().id_string()).c_str());
+
+    arrays.make_union(a, a.op0());
+    collect_arrays(a.op0());
   }
   else if(a.id()==ID_index)
   {
@@ -212,7 +224,12 @@ void arrayst::collect_arrays(const exprt &a)
     collect_arrays(a.op0());
   }
   else
-    throw "unexpected array expression (collect_arrays): `"+a.id_string()+"'";
+  {
+    DATA_INVARIANT(
+      false,
+      ("unexpected array expression (collect_arrays): `"+
+       a.id_string()+"'").c_str());
+  }
 }
 
 /// adds array constraints (refine=true...lazily for the refinement loop)
@@ -280,7 +297,7 @@ void arrayst::add_array_Ackermann_constraints()
 {
   // this is quadratic!
 
-#if 0
+#ifdef DEBUG
   std::cout << "arrays.size(): " << arrays.size() << '\n';
 #endif
 
@@ -289,7 +306,7 @@ void arrayst::add_array_Ackermann_constraints()
   {
     const index_sett &index_set=index_map[arrays.find_number(i)];
 
-#if 0
+#ifdef DEBUG
     std::cout << "index_set.size(): " << index_set.size() << '\n';
 #endif
 
@@ -349,7 +366,7 @@ void arrayst::update_index_map(std::size_t i)
     return;
 
   std::size_t root_number=arrays.find_number(i);
-  assert(root_number!=i);
+  INVARIANT(root_number!=i, "is_root_number incorrect?");
 
   index_sett &root_index_set=index_map[root_number];
   index_sett &index_set=index_map[i];
@@ -407,7 +424,9 @@ void arrayst::add_array_constraints_equality(
     const typet &subtype2=ns.follow(array_equality.f2.type()).subtype();
     index_exprt index_expr2(array_equality.f2, index, subtype2);
 
-    assert(index_expr1.type()==index_expr2.type());
+    DATA_INVARIANT(
+      index_expr1.type()==index_expr2.type(),
+      "array elements should all have same type");
 
     array_equalityt equal;
     equal.f1 = index_expr1;
@@ -449,12 +468,14 @@ void arrayst::add_array_constraints(
   else if(expr.id()==ID_byte_update_little_endian ||
           expr.id()==ID_byte_update_big_endian)
   {
-    assert(0);
+    INVARIANT(false, "byte_update should be removed before arrayst");
   }
   else if(expr.id()==ID_typecast)
   {
     // we got a=(type[])b
-    assert(expr.operands().size()==1);
+    DATA_INVARIANT(
+      expr.operands().size()==1,
+      "typecast should have one operand");
 
     // add a[i]=b[i]
     for(const auto &index : index_set)
@@ -463,7 +484,9 @@ void arrayst::add_array_constraints(
       index_exprt index_expr1(expr, index, subtype);
       index_exprt index_expr2(expr.op0(), index, subtype);
 
-      assert(index_expr1.type()==index_expr2.type());
+      DATA_INVARIANT(
+        index_expr1.type()==index_expr2.type(),
+        "array elements should all have same type");
 
       // add constraint
       lazy_constraintt lazy(lazy_typet::ARRAY_TYPECAST,
@@ -475,9 +498,12 @@ void arrayst::add_array_constraints(
   {
   }
   else
-    throw
-      "unexpected array expression (add_array_constraints): `"+
-        expr.id_string()+"'";
+  {
+    DATA_INVARIANT(
+      false,
+      ("unexpected array expression (add_array_constraints): `"+
+       expr.id_string()+"'").c_str());
+  }
 }
 
 void arrayst::add_array_constraints_with(
@@ -495,8 +521,10 @@ void arrayst::add_array_constraints_with(
 
     if(index_expr.type()!=value.type())
     {
-      std::cout << expr.pretty() << '\n';
-      assert(false);
+      prop.error() << expr.pretty() << messaget::eom;
+      DATA_INVARIANT(
+        false,
+        "with-expression operand should match array element type");
     }
 
     lazy_constraintt lazy(
@@ -563,8 +591,10 @@ void arrayst::add_array_constraints_update(
 
     if(index_expr.type()!=value.type())
     {
-      std::cout << expr.pretty() << '\n';
-      assert(false);
+      prop.error() << expr.pretty() << messaget::eom;
+      DATA_INVARIANT(
+        false,
+        "update operand should match array element type");
     }
 
     set_to_true(equal_exprt(index_expr, value));
@@ -619,7 +649,9 @@ void arrayst::add_array_constraints_array_of(
     const typet &subtype=ns.follow(expr.type()).subtype();
     index_exprt index_expr(expr, index, subtype);
 
-    assert(base_type_eq(index_expr.type(), expr.op0().type(), ns));
+    DATA_INVARIANT(
+      base_type_eq(index_expr.type(), expr.op0().type(), ns),
+      "array_of operand type should match array element type");
 
     // add constraint
     lazy_constraintt lazy(