Remove config dependency from CVC and DPLIB solvers

Author: tautschnig

src/solvers/cvc/cvc_conv.cpp

@@ -13,9 +13,9 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
-#include <util/config.h>
 #include <util/find_symbols.h>
 #include <util/pointer_offset_size.h>
 #include <util/string2int.h>
@@ -159,8 +159,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
     {
       out << "(# object:="
           << pointer_logic.get_null_object()
-          << ", offset:="
-          << bin_zero(config.ansi_c.pointer_width) << " #)";
+          << ", offset:=";
+      convert_expr(from_integer(0, size_type()));
+      out << " #)";
     }
     else
       throw "unknown pointer constant: "+id2string(value);
@@ -176,7 +177,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
   }
   else if(expr.type().id()==ID_array)
   {
-    out << "ARRAY (i: " << array_index_type() << "):";
+    out << "ARRAY (i: ";
+    convert_type(index_type());
+    out << "):";
 
     assert(!expr.operands().empty());
 
@@ -188,7 +191,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
       else
         out << "\n  ELSIF ";
 
-      out << "i=" << array_index(i) << " THEN ";
+      out << "i=";
+      convert_expr(from_integer(i, index_type()));
+      out << " THEN ";
       convert_array_value(*it);
       i++;
     }
@@ -247,7 +252,7 @@ void cvc_convt::convert_plus_expr(const exprt &expr)
       out << "(LET P: " << cvc_pointer_type() << " = ";
       convert_expr(*p);
       out << " IN P WITH .offset:=BVPLUS("
-          << config.ansi_c.pointer_width
+          << pointer_offset_bits(pointer_type(void_type()), ns)
           << ", P.offset, ";
       convert_expr(*i);
       out << "))";
@@ -487,52 +492,24 @@ void cvc_convt::convert_literal(const literalt l)
     out << ")";
 }
 
-std::string cvc_convt::bin_zero(unsigned bits)
+std::string cvc_convt::cvc_pointer_type() const
 {
-  assert(bits!=0);
-  std::string result="0bin";
-  while(bits!=0)
-  {
-    result+='0';
-    bits--;
-  }
-  return result;
-}
-
-std::string cvc_convt::cvc_pointer_type()
-{
-  assert(config.ansi_c.pointer_width!=0);
-  return "[# object: INT, offset: BITVECTOR("+
-         std::to_string(config.ansi_c.pointer_width)+") #]";
-}
-
-std::string cvc_convt::array_index_type()
-{
-  return std::string("BITVECTOR(")+
-         std::to_string(32)+")";
-}
-
-typet cvc_convt::gen_array_index_type()
-{
-  typet t(ID_signedbv);
-  t.set(ID_width, 32);
-  return t;
-}
-
-std::string cvc_convt::array_index(unsigned i)
-{
-  return "0bin"+integer2binary(i, config.ansi_c.int_width);
+  return
+    "[# object: INT, offset: BITVECTOR("+
+    std::to_string(
+      integer2size_t(
+        pointer_offset_bits(pointer_type(void_type()), ns)))+") #]";
 }
 
 void cvc_convt::convert_array_index(const exprt &expr)
 {
-  if(expr.type()==gen_array_index_type())
+  if(expr.type()==index_type())
   {
     convert_expr(expr);
   }
   else
   {
-    exprt tmp(ID_typecast, gen_array_index_type());
+    exprt tmp(ID_typecast, index_type());
     tmp.copy_to_operands(expr);
     convert_expr(tmp);
   }
@@ -547,8 +524,9 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
     out
       << "(# object:="
       << pointer_logic.add_object(expr)
-      << ", offset:="
-      << bin_zero(config.ansi_c.pointer_width) << " #)";
+      << ", offset:=";
+    convert_expr(from_integer(0, size_type()));
+    out << " #)";
   }
   else if(expr.id()==ID_index)
   {
@@ -581,7 +559,7 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
         assert(false);
 
       out << " IN P WITH .offset:=BVPLUS("
-                   << config.ansi_c.pointer_width
+                   << pointer_offset_bits(pointer_type(void_type()), ns)
                    << ", P.offset, ";
       convert_expr(index);
       out << "))";
@@ -609,13 +587,10 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
       ns);
     assert(offset>=0);
 
-    typet index_type(ID_unsignedbv);
-    index_type.set(ID_width, config.ansi_c.pointer_width);
-
-    exprt index=from_integer(offset, index_type);
+    exprt index=from_integer(offset, size_type());
 
     out << " IN P WITH .offset:=BVPLUS("
-                 << config.ansi_c.pointer_width
+                 << pointer_offset_bits(pointer_type(void_type()), ns)
                  << ", P.offset, ";
     convert_expr(index);
     out << "))";
@@ -1035,7 +1010,9 @@ void cvc_convt::convert_expr(const exprt &expr)
   {
     assert(expr.type().id()==ID_array);
     assert(expr.operands().size()==1);
-    out << "(ARRAY (i: " << array_index_type() << "): ";
+    out << "(ARRAY (i: ";
+    convert_type(index_type());
+    out << "): ";
     convert_array_value(expr.op0());
     out << ")";
   }
@@ -1273,8 +1250,9 @@ void cvc_convt::convert_type(const typet &type)
   {
     const array_typet &array_type=to_array_type(type);
 
-    out << "ARRAY " << array_index_type()
-                 << " OF ";
+    out << "ARRAY ";
+    convert_type(index_type());
+    out << " OF ";
 
     if(array_type.subtype().id()==ID_bool)
       out << "BITVECTOR(1)";

src/solvers/cvc/cvc_conv.h

@@ -79,11 +79,7 @@ class cvc_convt:public prop_convt
   void convert_array_value(const exprt &expr);
   void convert_as_bv(const exprt &expr);
   void convert_array_index(const exprt &expr);
-  static typet gen_array_index_type();
-  static std::string bin_zero(unsigned bits);
-  static std::string array_index_type();
-  static std::string array_index(unsigned i);
-  static std::string cvc_pointer_type();
+  std::string cvc_pointer_type() const;
 };
 
 #endif // CPROVER_SOLVERS_CVC_CVC_CONV_H