From 07793424923176fe93e6accc43a9aec0abbb05c5 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Tue, 10 Jan 2017 15:55:08 +0000
Subject: [PATCH 1/4] Fixing simple linting errors in CVC

Mostly if statement clauses on a new line
---
 src/solvers/cvc/cvc_conv.cpp | 67 ++++++++++++++++++----------
 src/solvers/cvc/cvc_conv.h   |  3 +-
 src/solvers/cvc/cvc_dec.cpp  | 14 +++---
 src/solvers/cvc/cvc_prop.cpp | 84 +++++++++++++++++++++++-------------
 src/solvers/cvc/cvc_prop.h   |  5 ++-
 5 files changed, 112 insertions(+), 61 deletions(-)

diff --git a/src/solvers/cvc/cvc_conv.cpp b/src/solvers/cvc/cvc_conv.cpp
index 2a39409d5e3..aa854adf84c 100644
--- a/src/solvers/cvc/cvc_conv.cpp
+++ b/src/solvers/cvc/cvc_conv.cpp
@@ -58,8 +58,10 @@ Function: cvc_convt::l_get
 
 tvt cvc_convt::l_get(literalt l) const
 {
-  if(l.is_true()) return tvt(true);
-  if(l.is_false()) return tvt(false);
+  if(l.is_true())
+    return tvt(true);
+  if(l.is_false())
+    return tvt(false);
   assert(l.var_no()<boolean_assignment.size());
   return tvt(boolean_assignment[l.var_no()]^l.sign());
 }
@@ -290,7 +292,8 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
 
     mp_integer offset=member_offset(
       to_struct_type(struct_op.type()),
-      component_name, ns);
+      component_name,
+      ns);
 
     typet index_type(ID_unsignedbv);
     index_type.set(ID_width, config.ansi_c.pointer_width);
@@ -321,8 +324,6 @@ Function: cvc_convt::convert
 
 literalt cvc_convt::convert(const exprt &expr)
 {
-  //out << "%% E: " << expr << std::endl;
-
   if(expr.type().id()!=ID_bool)
   {
     std::string msg="cvc_convt::convert got "
@@ -556,17 +557,19 @@ void cvc_convt::convert_expr(const exprt &expr)
       }
       else
       {
-        throw "TODO typecast1 "+op.type().id_string()+" -> bool";
+        throw "todo typecast1 "+op.type().id_string()+" -> bool";
       }
     }
     else if(expr.type().id()==ID_signedbv ||
             expr.type().id()==ID_unsignedbv)
     {
-      unsigned to_width=unsafe_string2unsigned(id2string(expr.type().get(ID_width)));
+      unsigned to_width=
+        unsafe_string2unsigned(id2string(expr.type().get(ID_width)));
 
       if(op.type().id()==ID_signedbv)
       {
-        unsigned from_width=unsafe_string2unsigned(id2string(op.type().get(ID_width)));
+        unsigned from_width=
+          unsafe_string2unsigned(id2string(op.type().get(ID_width)));
 
         if(from_width==to_width)
           convert_expr(op);
@@ -585,7 +588,8 @@ void cvc_convt::convert_expr(const exprt &expr)
       }
       else if(op.type().id()==ID_unsignedbv)
       {
-        unsigned from_width=unsafe_string2unsigned(id2string(op.type().get(ID_width)));
+        unsigned from_width=
+          unsafe_string2unsigned(id2string(op.type().get(ID_width)));
 
         if(from_width==to_width)
           convert_expr(op);
@@ -633,7 +637,7 @@ void cvc_convt::convert_expr(const exprt &expr)
       }
       else
       {
-        throw "TODO typecast2 "+op.type().id_string()+
+        throw "todo typecast2 "+op.type().id_string()+
               " -> "+expr.type().id_string();
       }
     }
@@ -644,10 +648,10 @@ void cvc_convt::convert_expr(const exprt &expr)
         convert_expr(op);
       }
       else
-        throw "TODO typecast3 "+op.type().id_string()+" -> pointer";
+        throw "todo typecast3 "+op.type().id_string()+" -> pointer";
     }
     else
-      throw "TODO typecast4 ? -> "+expr.type().id_string();
+      throw "todo typecast4 ? -> "+expr.type().id_string();
   }
   else if(expr.id()==ID_struct)
   {
@@ -666,7 +670,9 @@ void cvc_convt::convert_expr(const exprt &expr)
         it!=components.end();
         it++, i++)
     {
-      if(i!=0) out << ", ";
+      if(i!=0)
+        out << ", ";
+
       out << it->get(ID_name);
       out << ":=";
       convert_expr(expr.operands()[i]);
@@ -897,13 +903,16 @@ void cvc_convt::convert_expr(const exprt &expr)
 
     if(expr.op0().type().id()==ID_bool)
     {
-      if(expr.id()==ID_notequal) out << "NOT (";
+      if(expr.id()==ID_notequal)
+        out << "NOT (";
+
       out << "(";
       convert_expr(expr.op0());
       out << ") <=> (";
       convert_expr(expr.op1());
       out << ")";
-      if(expr.id()==ID_notequal) out << ")";
+      if(expr.id()==ID_notequal)
+        out << ")";
     }
     else
     {
@@ -960,7 +969,10 @@ void cvc_convt::convert_expr(const exprt &expr)
       out << ")";
     }
     else
-      throw "unsupported type for "+expr.id_string()+": "+expr.type().id_string();
+    {
+      throw "unsupported type for "+expr.id_string()+": "+
+        expr.type().id_string();
+    }
   }
   else if(expr.id()==ID_plus)
   {
@@ -1154,7 +1166,10 @@ void cvc_convt::convert_expr(const exprt &expr)
       out << ")";
     }
     else
-      throw "unsupported type for "+expr.id_string()+": "+expr.type().id_string();
+    {
+      throw "unsupported type for "+expr.id_string()+": "+
+        expr.type().id_string();
+    }
   }
   else if(expr.id()==ID_with)
   {
@@ -1192,7 +1207,10 @@ void cvc_convt::convert_expr(const exprt &expr)
         out << ")";
       }
       else
-        throw "with expects struct or array type, but got "+expr.type().id_string();
+      {
+        throw "with expects struct or array type, but got "+
+          expr.type().id_string();
+      }
     }
   }
   else if(expr.id()==ID_member)
@@ -1216,7 +1234,7 @@ void cvc_convt::convert_expr(const exprt &expr)
     out << "(";
     convert_expr(expr.op0());
     out << ").object";
-    // TODO, this has the wrong type
+    // TODO(kroening) this has the wrong type
   }
   #endif
   else if(expr.id()==ID_string_constant)
@@ -1240,7 +1258,10 @@ void cvc_convt::convert_expr(const exprt &expr)
       out << "[" << i << ":" << i << "]=0bin1)";
     }
     else
-      throw "unsupported type for "+expr.id_string()+": "+expr.op0().type().id_string();
+    {
+      throw "unsupported type for "+expr.id_string()+": "+
+        expr.op0().type().id_string();
+    }
   }
   else if(expr.id()==ID_replication)
   {
@@ -1258,7 +1279,8 @@ void cvc_convt::convert_expr(const exprt &expr)
 
     for(mp_integer i=0; i<times; ++i)
     {
-      if(i!=0) out << "@";
+      if(i!=0)
+        out << "@";
       out << "v";
     }
 
@@ -1445,7 +1467,8 @@ void cvc_convt::convert_type(const typet &type)
         it!=components.end();
         it++)
     {
-      if(it!=components.begin()) out << ",";
+      if(it!=components.begin())
+        out << ",";
       out << " ";
       out << it->get(ID_name);
       out << ": ";
diff --git a/src/solvers/cvc/cvc_conv.h b/src/solvers/cvc/cvc_conv.h
index edf9720d0eb..a21009c3c10 100644
--- a/src/solvers/cvc/cvc_conv.h
+++ b/src/solvers/cvc/cvc_conv.h
@@ -16,8 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 class cvc_convt:public prop_convt
 {
 public:
-  cvc_convt(const namespacet &_ns,
-            std::ostream &_out):
+  cvc_convt(const namespacet &_ns, std::ostream &_out):
     prop_convt(_ns),
     out(_out),
     pointer_logic(_ns),
diff --git a/src/solvers/cvc/cvc_dec.cpp b/src/solvers/cvc/cvc_dec.cpp
index 3b174ac4c2f..b7fd3a2c3e2 100644
--- a/src/solvers/cvc/cvc_dec.cpp
+++ b/src/solvers/cvc/cvc_dec.cpp
@@ -99,7 +99,7 @@ decision_proceduret::resultt cvc_dect::dec_solve()
     "cvcl "+temp_out_filename+" > "+temp_result_filename+" 2>&1";
 
   int res=system(command.c_str());
-  assert(0 == res);
+  assert(0==res);
 
   status() << "Reading result from CVCL" << eom;
 
@@ -122,7 +122,8 @@ void cvc_dect::read_assert(std::istream &in, std::string &line)
 {
   // strip ASSERT
   line=std::string(line, strlen("ASSERT "), std::string::npos);
-  if(line=="") return;
+  if(line=="")
+    return;
 
   // bit-vector
   if(line[0]=='(')
@@ -134,7 +135,8 @@ void cvc_dect::read_assert(std::istream &in, std::string &line)
     std::string identifier=std::string(line, 1, pos-1);
 
     // get value
-    if(!std::getline(in, line)) return;
+    if(!std::getline(in, line))
+      return;
 
     // skip spaces
     pos=0;
@@ -142,7 +144,8 @@ void cvc_dect::read_assert(std::istream &in, std::string &line)
 
     // get final ")"
     std::string::size_type pos2=line.rfind(')');
-    if(pos2==std::string::npos) return;
+    if(pos2==std::string::npos)
+      return;
 
     std::string value=std::string(line, pos, pos2-pos);
 
@@ -162,7 +165,8 @@ void cvc_dect::read_assert(std::istream &in, std::string &line)
       value=false;
     }
 
-    if(line=="") return;
+    if(line=="")
+      return;
 
     if(line[0]=='l')
     {
diff --git a/src/solvers/cvc/cvc_prop.cpp b/src/solvers/cvc/cvc_prop.cpp
index d941e6c8235..27c499620ea 100644
--- a/src/solvers/cvc/cvc_prop.cpp
+++ b/src/solvers/cvc/cvc_prop.cpp
@@ -24,7 +24,7 @@ Function: cvc_propt::cvc_propt
 
 \*******************************************************************/
 
-cvc_propt::cvc_propt(std::ostream &_out):out(_out)
+explicit cvc_propt::cvc_propt(std::ostream &_out):out(_out)
 {
   _no_variables=0;
 }
@@ -47,7 +47,7 @@ cvc_propt::~cvc_propt()
 
 /*******************************************************************\
 
-Function:
+Function: cvc_propt::land
 
   Inputs:
 
@@ -67,7 +67,7 @@ void cvc_propt::land(literalt a, literalt b, literalt o)
 
 /*******************************************************************\
 
-Function:
+Function: cvc_propt::lor
 
   Inputs:
 
@@ -87,7 +87,7 @@ void cvc_propt::lor(literalt a, literalt b, literalt o)
 
 /*******************************************************************\
 
-Function:
+Function: cvc_propt::lxor
 
   Inputs:
 
@@ -107,7 +107,7 @@ void cvc_propt::lxor(literalt a, literalt b, literalt o)
 
 /*******************************************************************\
 
-Function:
+Function: cvc_propt::lnand
 
   Inputs:
 
@@ -127,7 +127,7 @@ void cvc_propt::lnand(literalt a, literalt b, literalt o)
 
 /*******************************************************************\
 
-Function:
+Function: cvc_propt::lnor
 
   Inputs:
 
@@ -205,7 +205,8 @@ literalt cvc_propt::land(const bvt &bv)
 
   forall_literals(it, bv)
   {
-    if(it!=bv.begin()) out << " AND ";
+    if(it!=bv.begin())
+      out << " AND ";
     out << cvc_literal(*it);
   }
 
@@ -234,7 +235,8 @@ literalt cvc_propt::lor(const bvt &bv)
 
   forall_literals(it, bv)
   {
-    if(it!=bv.begin()) out << " OR ";
+    if(it!=bv.begin())
+      out << " OR ";
     out << cvc_literal(*it);
   }
 
@@ -257,9 +259,12 @@ Function: cvc_propt::lxor
 
 literalt cvc_propt::lxor(const bvt &bv)
 {
-  if(bv.empty()) return const_literal(false);
-  if(bv.size()==1) return bv[0];
-  if(bv.size()==2) return lxor(bv[0], bv[1]);
+  if(bv.empty())
+    return const_literal(false);
+  if(bv.size()==1)
+    return bv[0];
+  if(bv.size()==2)
+    return lxor(bv[0], bv[1]);
 
   literalt literal=const_literal(false);
 
@@ -283,11 +288,16 @@ Function: cvc_propt::land
 
 literalt cvc_propt::land(literalt a, literalt b)
 {
-  if(a==const_literal(true)) return b;
-  if(b==const_literal(true)) return a;
-  if(a==const_literal(false)) return const_literal(false);
-  if(b==const_literal(false)) return const_literal(false);
-  if(a==b) return a;
+  if(a==const_literal(true))
+    return b;
+  if(b==const_literal(true))
+    return a;
+  if(a==const_literal(false))
+    return const_literal(false);
+  if(b==const_literal(false))
+    return const_literal(false);
+  if(a==b)
+    return a;
 
   out << "%% land" << std::endl;
 
@@ -313,11 +323,16 @@ Function: cvc_propt::lor
 
 literalt cvc_propt::lor(literalt a, literalt b)
 {
-  if(a==const_literal(false)) return b;
-  if(b==const_literal(false)) return a;
-  if(a==const_literal(true)) return const_literal(true);
-  if(b==const_literal(true)) return const_literal(true);
-  if(a==b) return a;
+  if(a==const_literal(false))
+    return b;
+  if(b==const_literal(false))
+    return a;
+  if(a==const_literal(true))
+    return const_literal(true);
+  if(b==const_literal(true))
+    return const_literal(true);
+  if(a==b)
+    return a;
 
   out << "%% lor" << std::endl;
 
@@ -343,10 +358,14 @@ Function: cvc_propt::lxor
 
 literalt cvc_propt::lxor(literalt a, literalt b)
 {
-  if(a==const_literal(false)) return b;
-  if(b==const_literal(false)) return a;
-  if(a==const_literal(true)) return !b;
-  if(b==const_literal(true)) return !a;
+  if(a==const_literal(false))
+    return b;
+  if(b==const_literal(false))
+    return a;
+  if(a==const_literal(true))
+    return !b;
+  if(b==const_literal(true))
+    return !a;
 
   out << "%% lxor" << std::endl;
 
@@ -440,9 +459,12 @@ Function: cvc_propt::lselect
 
 literalt cvc_propt::lselect(literalt a, literalt b, literalt c)
 {
-  if(a==const_literal(true)) return b;
-  if(a==const_literal(false)) return c;
-  if(b==c) return b;
+  if(a==const_literal(true))
+    return b;
+  if(a==const_literal(false))
+    return c;
+  if(b==c)
+    return b;
 
   out << "%% lselect" << std::endl;
 
@@ -512,7 +534,8 @@ Function: cvc_propt::lcnf
 
 void cvc_propt::lcnf(const bvt &bv)
 {
-  if(bv.empty()) return;
+  if(bv.empty())
+    return;
   bvt new_bv;
 
   std::set<literalt> s;
@@ -537,7 +560,8 @@ void cvc_propt::lcnf(const bvt &bv)
 
   for(bvt::const_iterator it=new_bv.begin(); it!=new_bv.end(); it++)
   {
-    if(it!=new_bv.begin()) out << " OR ";
+    if(it!=new_bv.begin())
+      out << " OR ";
     out << cvc_literal(*it);
   }
 
diff --git a/src/solvers/cvc/cvc_prop.h b/src/solvers/cvc/cvc_prop.h
index 2222b8c9e29..cc83906a3f7 100644
--- a/src/solvers/cvc/cvc_prop.h
+++ b/src/solvers/cvc/cvc_prop.h
@@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 class cvc_propt:virtual public propt
 {
 public:
-  cvc_propt(std::ostream &_out);
+  explicit cvc_propt(std::ostream &_out);
   virtual ~cvc_propt();
 
   virtual void land(literalt a, literalt b, literalt o);
@@ -52,7 +52,8 @@ class cvc_propt:virtual public propt
   virtual tvt l_get(literalt literal) const
   {
     unsigned v=literal.var_no();
-    if(v>=assignment.size()) return tvt(tvt::tv_enumt::TV_UNKNOWN);
+    if(v>=assignment.size())
+      return tvt(tvt::tv_enumt::TV_UNKNOWN);
     tvt r=assignment[v];
     return literal.sign()?!r:r;
   }

From cf63d46f77d2e5d98d502c919be43965b38a3832 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Tue, 10 Jan 2017 16:31:30 +0000
Subject: [PATCH 2/4] Split convert_expr into a collection of smaller functions

The convert_expr function was over 600 lines as so triggered the linter.
I have taken each substantial if clause and put them into individual
functions. The body of the function should remain unchanged.

Future improvements could include making it more functional in style so
that it isn't modifying the member variable out and instead returning
somehting. Also could use a dictionary of irep_idt->function to make the
function fewer lines and easier to see which types are handled.
---
 src/solvers/cvc/cvc_conv.cpp | 944 ++++++++++++++++++++---------------
 src/solvers/cvc/cvc_conv.h   |   9 +
 2 files changed, 559 insertions(+), 394 deletions(-)

diff --git a/src/solvers/cvc/cvc_conv.cpp b/src/solvers/cvc/cvc_conv.cpp
index aa854adf84c..8102f86754d 100644
--- a/src/solvers/cvc/cvc_conv.cpp
+++ b/src/solvers/cvc/cvc_conv.cpp
@@ -68,6 +68,543 @@ tvt cvc_convt::l_get(literalt l) const
 
 /*******************************************************************\
 
+Function: cvc_convt::convert_binary_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cvc_convt::convert_binary_expr(const exprt &expr, const exprt &op)
+{
+  unsigned to_width=
+    unsafe_string2unsigned(id2string(expr.type().get(ID_width)));
+
+  if(op.type().id()==ID_signedbv)
+  {
+    unsigned from_width=
+      unsafe_string2unsigned(id2string(op.type().get(ID_width)));
+
+    if(from_width==to_width)
+      convert_expr(op);
+    else if(from_width<to_width)
+    {
+      out << "SX(";
+      convert_expr(op);
+      out << ", " << to_width << ")";
+    }
+    else
+    {
+      out << "(";
+      convert_expr(op);
+      out << ")[" << (to_width-1) << ":0]";
+    }
+  }
+  else if(op.type().id()==ID_unsignedbv)
+  {
+    unsigned from_width=
+      unsafe_string2unsigned(id2string(op.type().get(ID_width)));
+
+    if(from_width==to_width)
+      convert_expr(op);
+    else if(from_width<to_width)
+    {
+      out << "(0bin";
+
+      for(unsigned i=from_width; i<to_width; i++)
+        out << "0";
+
+      out << " @ ";
+
+      out << "(";
+      convert_expr(op);
+      out << "))";
+    }
+    else
+    {
+      out << "(";
+      convert_expr(op);
+      out << ")[" << (to_width-1) << ":0]";
+    }
+  }
+  else if(op.type().id()==ID_bool)
+  {
+    if(to_width>1)
+    {
+      out << "(0bin";
+
+      for(unsigned i=1; i<to_width; i++)
+        out << "0";
+
+      out << " @ ";
+
+      out << "IF ";
+      convert_expr(op);
+      out << " THEN 0bin1 ELSE 0bin0 ENDIF)";
+    }
+    else
+    {
+      out << "IF ";
+      convert_expr(op);
+      out << " THEN 0bin1 ELSE 0bin0 ENDIF";
+    }
+  }
+  else
+  {
+    throw "todo typecast2 "+op.type().id_string()+
+      " -> "+expr.type().id_string();
+  }
+}
+
+/*******************************************************************\
+
+Function: cvc_convt::convert_constant_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cvc_convt::convert_constant_expr(const exprt &expr)
+{
+  if(expr.type().id()==ID_unsignedbv ||
+     expr.type().id()==ID_signedbv ||
+     expr.type().id()==ID_bv)
+  {
+    const irep_idt &value=expr.get(ID_value);
+
+    if(value.size()==8 ||
+       value.size()==16 ||
+       value.size()==32 ||
+       value.size()==64)
+    {
+      std::size_t w=value.size()/4;
+
+      mp_integer i=binary2integer(id2string(value), false);
+      std::string hex=integer2string(i, 16);
+
+      while(hex.size()<w)
+        hex="0"+hex;
+
+      out << "0hex" << hex;
+    }
+    else
+    {
+      out << "0bin" << value;
+    }
+  }
+  else if(expr.type().id()==ID_pointer)
+  {
+    const irep_idt &value=expr.get(ID_value);
+
+    if(value=="NULL")
+    {
+      out << "(# object:="
+          << pointer_logic.get_null_object()
+          << ", offset:="
+          << bin_zero(config.ansi_c.pointer_width) << " #)";
+    }
+    else
+      throw "unknown pointer constant: "+id2string(value);
+  }
+  else if(expr.type().id()==ID_bool)
+  {
+    if(expr.is_true())
+      out << "TRUE";
+    else if(expr.is_false())
+      out << "FALSE";
+    else
+      throw "unknown boolean constant";
+  }
+  else if(expr.type().id()==ID_array)
+  {
+    out << "ARRAY (i: " << array_index_type() << "):";
+
+    assert(!expr.operands().empty());
+
+    unsigned i=0;
+    forall_operands(it, expr)
+    {
+      if(i==0)
+        out << "\n  IF ";
+      else
+        out << "\n  ELSIF ";
+
+      out << "i=" << array_index(i) << " THEN ";
+      convert_array_value(*it);
+      i++;
+    }
+
+    out << "\n  ELSE ";
+    convert_expr(expr.op0());
+    out << "\n  ENDIF";
+  }
+  else if(expr.type().id()==ID_integer ||
+          expr.type().id()==ID_natural ||
+          expr.type().id()==ID_range)
+  {
+    out << expr.get(ID_value);
+  }
+  else
+    throw "unknown constant: "+expr.type().id_string();
+}
+
+/*******************************************************************\
+
+Function: cvc_convt::convert_plus_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cvc_convt::convert_plus_expr(const exprt &expr)
+{
+  if(expr.operands().size()>=2)
+  {
+    if(expr.type().id()==ID_unsignedbv ||
+       expr.type().id()==ID_signedbv)
+    {
+      out << "BVPLUS(" << expr.type().get(ID_width);
+
+      forall_operands(it, expr)
+      {
+        out << ", ";
+        convert_expr(*it);
+      }
+
+      out << ")";
+    }
+    else if(expr.type().id()==ID_pointer)
+    {
+      if(expr.operands().size()!=2)
+        throw "pointer arithmetic with more than two operands";
+
+      const exprt *p, *i;
+
+      if(expr.op0().type().id()==ID_pointer)
+      {
+        p=&expr.op0();
+        i=&expr.op1();
+      }
+      else if(expr.op1().type().id()==ID_pointer)
+      {
+        p=&expr.op1();
+        i=&expr.op0();
+      }
+      else
+        throw "unexpected mixture in pointer arithmetic";
+
+      out << "(LET P: " << cvc_pointer_type() << " = ";
+      convert_expr(*p);
+      out << " IN P WITH .offset:=BVPLUS("
+          << config.ansi_c.pointer_width
+          << ", P.offset, ";
+      convert_expr(*i);
+      out << "))";
+    }
+    else
+      throw "unsupported type for +: "+expr.type().id_string();
+  }
+  else if(expr.operands().size()==1)
+  {
+    convert_expr(expr.op0());
+  }
+  else
+    assert(false);
+}
+
+/*******************************************************************\
+
+Function: cvc_convt::convert_typecast_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cvc_convt::convert_typecast_expr(const exprt &expr)
+{
+  assert(expr.operands().size()==1);
+  const exprt &op=expr.op0();
+
+  if(expr.type().id()==ID_bool)
+  {
+    if(op.type().id()==ID_signedbv ||
+       op.type().id()==ID_unsignedbv ||
+       op.type().id()==ID_pointer)
+    {
+      convert_expr(op);
+      out << "/=";
+      convert_expr(gen_zero(op.type()));
+    }
+    else
+    {
+      throw "todo typecast1 "+op.type().id_string()+" -> bool";
+    }
+  }
+  else if(expr.type().id()==ID_signedbv ||
+          expr.type().id()==ID_unsignedbv)
+  {
+    convert_binary_expr(expr, op);
+  }
+  else if(expr.type().id()==ID_pointer)
+  {
+    if(op.type().id()==ID_pointer)
+    {
+      convert_expr(op);
+    }
+    else
+      throw "todo typecast3 "+op.type().id_string()+" -> pointer";
+  }
+  else
+    throw "todo typecast4 ? -> "+expr.type().id_string();
+}
+
+/*******************************************************************\
+
+Function: cvc_convt::convert_struct_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cvc_convt::convert_struct_expr(const exprt &expr)
+{
+  out << "(# ";
+
+  const struct_typet &struct_type=to_struct_type(expr.type());
+
+  const struct_typet::componentst &components=
+    struct_type.components();
+
+  assert(components.size()==expr.operands().size());
+
+  unsigned i=0;
+  for(const struct_union_typet::componentt &component : components)
+  {
+    if(i!=0)
+      out << ", ";
+
+    out << component.get(ID_name);
+    out << ":=";
+    convert_expr(expr.operands()[i]);
+    ++i;
+  }
+
+  out << " #)";
+}
+
+/*******************************************************************\
+
+Function: cvc_convt::convert_equality_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cvc_convt::convert_equality_expr(const exprt &expr)
+{
+  assert(expr.operands().size()==2);
+  assert(expr.op0().type()==expr.op1().type());
+
+  if(expr.op0().type().id()==ID_bool)
+  {
+    if(expr.id()==ID_notequal)
+      out << "NOT (";
+
+    out << "(";
+    convert_expr(expr.op0());
+    out << ") <=> (";
+    convert_expr(expr.op1());
+    out << ")";
+    if(expr.id()==ID_notequal)
+      out << ")";
+  }
+  else
+  {
+    out << "(";
+    convert_expr(expr.op0());
+    out << ")";
+    out << (expr.id()==ID_equal?"=":"/=");
+    out << "(";
+    convert_expr(expr.op1());
+    out << ")";
+  }
+}
+
+/*******************************************************************\
+
+Function: cvc_convt::convert_comparison_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cvc_convt::convert_comparison_expr(const exprt &expr)
+{
+  assert(expr.operands().size()==2);
+
+  const typet &op_type=expr.op0().type();
+
+  if(op_type.id()==ID_unsignedbv)
+  {
+    if(expr.id()==ID_le)
+      out << "BVLE";
+    else if(expr.id()==ID_lt)
+      out << "BVLT";
+    else if(expr.id()==ID_ge)
+      out << "BVGE";
+    else if(expr.id()==ID_gt)
+      out << "BVGT";
+
+    out << "(";
+    convert_expr(expr.op0());
+    out << ", ";
+    convert_expr(expr.op1());
+    out << ")";
+  }
+  else if(op_type.id()==ID_signedbv)
+  {
+    if(expr.id()==ID_le)
+      out << "SBVLE";
+    else if(expr.id()==ID_lt)
+      out << "SBVLT";
+    else if(expr.id()==ID_ge)
+      out << "SBVGE";
+    else if(expr.id()==ID_gt)
+      out << "SBVGT";
+
+    out << "(";
+    convert_expr(expr.op0());
+    out << ", ";
+    convert_expr(expr.op1());
+    out << ")";
+  }
+  else
+  {
+    throw "unsupported type for "+expr.id_string()+": "+
+      expr.type().id_string();
+  }
+}
+
+/*******************************************************************\
+
+Function: cvc_convt::convert_minus_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cvc_convt::convert_minus_expr(const exprt &expr)
+{
+  if(expr.operands().size()==2)
+  {
+    if(expr.type().id()==ID_unsignedbv ||
+       expr.type().id()==ID_signedbv)
+    {
+      out << "BVSUB(" << expr.type().get(ID_width) << ", ";
+      convert_expr(expr.op0());
+      out << ", ";
+      convert_expr(expr.op1());
+      out << ")";
+    }
+    else
+      throw "unsupported type for -: "+expr.type().id_string();
+  }
+  else if(expr.operands().size()==1)
+  {
+    convert_expr(expr.op0());
+  }
+  else
+    assert(false);
+}
+
+/*******************************************************************\
+
+Function: cvc_convt::convert_with_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void cvc_convt::convert_with_expr(const exprt &expr)
+{
+  assert(expr.operands().size()>=1);
+  out << "(";
+  convert_expr(expr.op0());
+  out << ")";
+
+  for(unsigned i=1; i<expr.operands().size(); i+=2)
+  {
+    assert((i+1)<expr.operands().size());
+    const exprt &index=expr.operands()[i];
+    const exprt &value=expr.operands()[i+1];
+
+    if(expr.type().id()==ID_struct)
+    {
+      out << " WITH ." << index.get(ID_component_name);
+      out << ":=(";
+      convert_array_value(value);
+      out << ")";
+    }
+    else if(expr.type().id()==ID_union)
+    {
+      out << " WITH ." << index.get(ID_component_name);
+      out << ":=(";
+      convert_array_value(value);
+      out << ")";
+    }
+    else if(expr.type().id()==ID_array)
+    {
+      out << " WITH [";
+      convert_array_index(index);
+      out << "]:=(";
+      convert_array_value(value);
+      out << ")";
+    }
+    else
+    {
+      throw "with expects struct or array type, but got "+
+        expr.type().id_string();
+    }
+  }
+}
+
+/*******************************************************************\
+
 Function: cvc_convt::convert_literal
 
   Inputs:
@@ -110,7 +647,11 @@ std::string cvc_convt::bin_zero(unsigned bits)
 {
   assert(bits!=0);
   std::string result="0bin";
-  while(bits!=0) { result+='0'; bits--; }
+  while(bits!=0)
+  {
+    result+='0';
+    bits--;
+  }
   return result;
 }
 
@@ -542,225 +1083,15 @@ void cvc_convt::convert_expr(const exprt &expr)
   }
   else if(expr.id()==ID_typecast)
   {
-    assert(expr.operands().size()==1);
-    const exprt &op=expr.op0();
-
-    if(expr.type().id()==ID_bool)
-    {
-      if(op.type().id()==ID_signedbv ||
-         op.type().id()==ID_unsignedbv ||
-         op.type().id()==ID_pointer)
-      {
-        convert_expr(op);
-        out << "/=";
-        convert_expr(gen_zero(op.type()));
-      }
-      else
-      {
-        throw "todo typecast1 "+op.type().id_string()+" -> bool";
-      }
-    }
-    else if(expr.type().id()==ID_signedbv ||
-            expr.type().id()==ID_unsignedbv)
-    {
-      unsigned to_width=
-        unsafe_string2unsigned(id2string(expr.type().get(ID_width)));
-
-      if(op.type().id()==ID_signedbv)
-      {
-        unsigned from_width=
-          unsafe_string2unsigned(id2string(op.type().get(ID_width)));
-
-        if(from_width==to_width)
-          convert_expr(op);
-        else if(from_width<to_width)
-        {
-          out << "SX(";
-          convert_expr(op);
-          out << ", " << to_width << ")";
-        }
-        else
-        {
-          out << "(";
-          convert_expr(op);
-          out << ")[" << (to_width-1) << ":0]";
-        }
-      }
-      else if(op.type().id()==ID_unsignedbv)
-      {
-        unsigned from_width=
-          unsafe_string2unsigned(id2string(op.type().get(ID_width)));
-
-        if(from_width==to_width)
-          convert_expr(op);
-        else if(from_width<to_width)
-        {
-          out << "(0bin";
-
-          for(unsigned i=from_width; i<to_width; i++)
-            out << "0";
-
-          out << " @ ";
-
-          out << "(";
-          convert_expr(op);
-          out << "))";
-        }
-        else
-        {
-          out << "(";
-          convert_expr(op);
-          out << ")[" << (to_width-1) << ":0]";
-        }
-      }
-      else if(op.type().id()==ID_bool)
-      {
-        if(to_width>1)
-        {
-          out << "(0bin";
-
-          for(unsigned i=1; i<to_width; i++)
-            out << "0";
-
-          out << " @ ";
-
-          out << "IF ";
-          convert_expr(op);
-          out << " THEN 0bin1 ELSE 0bin0 ENDIF)";
-        }
-        else
-        {
-          out << "IF ";
-          convert_expr(op);
-          out << " THEN 0bin1 ELSE 0bin0 ENDIF";
-        }
-      }
-      else
-      {
-        throw "todo typecast2 "+op.type().id_string()+
-              " -> "+expr.type().id_string();
-      }
-    }
-    else if(expr.type().id()==ID_pointer)
-    {
-      if(op.type().id()==ID_pointer)
-      {
-        convert_expr(op);
-      }
-      else
-        throw "todo typecast3 "+op.type().id_string()+" -> pointer";
-    }
-    else
-      throw "todo typecast4 ? -> "+expr.type().id_string();
+    convert_typecast_expr(expr);
   }
   else if(expr.id()==ID_struct)
   {
-    out << "(# ";
-
-    const struct_typet &struct_type=to_struct_type(expr.type());
-
-    const struct_typet::componentst &components=
-      struct_type.components();
-
-    assert(components.size()==expr.operands().size());
-
-    unsigned i=0;
-    for(struct_typet::componentst::const_iterator
-        it=components.begin();
-        it!=components.end();
-        it++, i++)
-    {
-      if(i!=0)
-        out << ", ";
-
-      out << it->get(ID_name);
-      out << ":=";
-      convert_expr(expr.operands()[i]);
-    }
-
-    out << " #)";
+    convert_struct_expr(expr);
   }
   else if(expr.id()==ID_constant)
   {
-    if(expr.type().id()==ID_unsignedbv ||
-       expr.type().id()==ID_signedbv ||
-       expr.type().id()==ID_bv)
-    {
-      const irep_idt &value=expr.get(ID_value);
-
-      if(value.size()==8 ||
-         value.size()==16 ||
-         value.size()==32 ||
-         value.size()==64)
-      {
-        std::size_t w=value.size()/4;
-
-        mp_integer i=binary2integer(id2string(value), false);
-        std::string hex=integer2string(i, 16);
-
-        while(hex.size()<w) hex="0"+hex;
-
-        out << "0hex" << hex;
-      }
-      else
-      {
-        out << "0bin" << value;
-      }
-    }
-    else if(expr.type().id()==ID_pointer)
-    {
-      const irep_idt &value=expr.get(ID_value);
-
-      if(value=="NULL")
-      {
-        out << "(# object:="
-                     << pointer_logic.get_null_object()
-                     << ", offset:="
-                     << bin_zero(config.ansi_c.pointer_width) << " #)";
-      }
-      else
-        throw "unknown pointer constant: "+id2string(value);
-    }
-    else if(expr.type().id()==ID_bool)
-    {
-      if(expr.is_true())
-        out << "TRUE";
-      else if(expr.is_false())
-        out << "FALSE";
-      else
-        throw "unknown boolean constant";
-    }
-    else if(expr.type().id()==ID_array)
-    {
-      out << "ARRAY (i: " << array_index_type() << "):";
-
-      assert(!expr.operands().empty());
-
-      unsigned i=0;
-      forall_operands(it, expr)
-      {
-        if(i==0)
-          out << "\n  IF ";
-        else
-          out << "\n  ELSIF ";
-
-        out << "i=" << array_index(i) << " THEN ";
-        convert_array_value(*it);
-        i++;
-      }
-
-      out << "\n  ELSE ";
-      convert_expr(expr.op0());
-      out << "\n  ENDIF";
-    }
-    else if(expr.type().id()==ID_integer ||
-            expr.type().id()==ID_natural ||
-            expr.type().id()==ID_range)
-    {
-      out << expr.get(ID_value);
-    }
-    else
-      throw "unknown constant: "+expr.type().id_string();
+    convert_constant_expr(expr);
   }
   else if(expr.id()==ID_concatenation ||
           expr.id()==ID_bitand ||
@@ -898,159 +1229,22 @@ void cvc_convt::convert_expr(const exprt &expr)
   else if(expr.id()==ID_equal ||
           expr.id()==ID_notequal)
   {
-    assert(expr.operands().size()==2);
-    assert(expr.op0().type()==expr.op1().type());
-
-    if(expr.op0().type().id()==ID_bool)
-    {
-      if(expr.id()==ID_notequal)
-        out << "NOT (";
-
-      out << "(";
-      convert_expr(expr.op0());
-      out << ") <=> (";
-      convert_expr(expr.op1());
-      out << ")";
-      if(expr.id()==ID_notequal)
-        out << ")";
-    }
-    else
-    {
-      out << "(";
-      convert_expr(expr.op0());
-      out << ")";
-      out << (expr.id()==ID_equal?"=":"/=");
-      out << "(";
-      convert_expr(expr.op1());
-      out << ")";
-    }
+    convert_equality_expr(expr);
   }
   else if(expr.id()==ID_le ||
           expr.id()==ID_lt ||
           expr.id()==ID_ge ||
           expr.id()==ID_gt)
   {
-    assert(expr.operands().size()==2);
-
-    const typet &op_type=expr.op0().type();
-
-    if(op_type.id()==ID_unsignedbv)
-    {
-      if(expr.id()==ID_le)
-        out << "BVLE";
-      else if(expr.id()==ID_lt)
-        out << "BVLT";
-      else if(expr.id()==ID_ge)
-        out << "BVGE";
-      else if(expr.id()==ID_gt)
-        out << "BVGT";
-
-      out << "(";
-      convert_expr(expr.op0());
-      out << ", ";
-      convert_expr(expr.op1());
-      out << ")";
-    }
-    else if(op_type.id()==ID_signedbv)
-    {
-      if(expr.id()==ID_le)
-        out << "SBVLE";
-      else if(expr.id()==ID_lt)
-        out << "SBVLT";
-      else if(expr.id()==ID_ge)
-        out << "SBVGE";
-      else if(expr.id()==ID_gt)
-        out << "SBVGT";
-
-      out << "(";
-      convert_expr(expr.op0());
-      out << ", ";
-      convert_expr(expr.op1());
-      out << ")";
-    }
-    else
-    {
-      throw "unsupported type for "+expr.id_string()+": "+
-        expr.type().id_string();
-    }
+    convert_comparison_expr(expr);
   }
   else if(expr.id()==ID_plus)
   {
-    if(expr.operands().size()>=2)
-    {
-      if(expr.type().id()==ID_unsignedbv ||
-         expr.type().id()==ID_signedbv)
-      {
-        out << "BVPLUS(" << expr.type().get(ID_width);
-
-        forall_operands(it, expr)
-        {
-          out << ", ";
-          convert_expr(*it);
-        }
-
-        out << ")";
-      }
-      else if(expr.type().id()==ID_pointer)
-      {
-        if(expr.operands().size()!=2)
-          throw "pointer arithmetic with more than two operands";
-
-        const exprt *p, *i;
-
-        if(expr.op0().type().id()==ID_pointer)
-        {
-          p=&expr.op0();
-          i=&expr.op1();
-        }
-        else if(expr.op1().type().id()==ID_pointer)
-        {
-          p=&expr.op1();
-          i=&expr.op0();
-        }
-        else
-          throw "unexpected mixture in pointer arithmetic";
-
-        out << "(LET P: " << cvc_pointer_type() << " = ";
-        convert_expr(*p);
-        out << " IN P WITH .offset:=BVPLUS("
-                     << config.ansi_c.pointer_width
-                     << ", P.offset, ";
-        convert_expr(*i);
-        out << "))";
-      }
-      else
-        throw "unsupported type for +: "+expr.type().id_string();
-    }
-    else if(expr.operands().size()==1)
-    {
-      convert_expr(expr.op0());
-    }
-    else
-      assert(false);
+    convert_plus_expr(expr);
   }
   else if(expr.id()==ID_minus)
   {
-    if(expr.operands().size()==2)
-    {
-      if(expr.type().id()==ID_unsignedbv ||
-         expr.type().id()==ID_signedbv)
-      {
-        out << "BVSUB(" << expr.type().get(ID_width) << ", ";
-        convert_expr(expr.op0());
-        out << ", ";
-        convert_expr(expr.op1());
-        out << ")";
-      }
-      else
-        throw "unsupported type for -: "+expr.type().id_string();
-    }
-    else if(expr.operands().size()==1)
-    {
-      convert_expr(expr.op0());
-    }
-    else
-      assert(false);
+    convert_minus_expr(expr);
   }
   else if(expr.id()==ID_div)
   {
@@ -1173,45 +1367,7 @@ void cvc_convt::convert_expr(const exprt &expr)
   }
   else if(expr.id()==ID_with)
   {
-    assert(expr.operands().size()>=1);
-    out << "(";
-    convert_expr(expr.op0());
-    out << ")";
-
-    for(unsigned i=1; i<expr.operands().size(); i+=2)
-    {
-      assert((i+1)<expr.operands().size());
-      const exprt &index=expr.operands()[i];
-      const exprt &value=expr.operands()[i+1];
-
-      if(expr.type().id()==ID_struct)
-      {
-        out << " WITH ." << index.get(ID_component_name);
-        out << ":=(";
-        convert_array_value(value);
-        out << ")";
-      }
-      else if(expr.type().id()==ID_union)
-      {
-        out << " WITH ." << index.get(ID_component_name);
-        out << ":=(";
-        convert_array_value(value);
-        out << ")";
-      }
-      else if(expr.type().id()==ID_array)
-      {
-        out << " WITH [";
-        convert_array_index(index);
-        out << "]:=(";
-        convert_array_value(value);
-        out << ")";
-      }
-      else
-      {
-        throw "with expects struct or array type, but got "+
-          expr.type().id_string();
-      }
-    }
+    convert_with_expr(expr);
   }
   else if(expr.id()==ID_member)
   {
diff --git a/src/solvers/cvc/cvc_conv.h b/src/solvers/cvc/cvc_conv.h
index a21009c3c10..7f1c37b5ee2 100644
--- a/src/solvers/cvc/cvc_conv.h
+++ b/src/solvers/cvc/cvc_conv.h
@@ -63,6 +63,15 @@ class cvc_convt:public prop_convt
 
 private:
   void convert_identifier(const std::string &identifier);
+  void convert_typecast_expr(const exprt &expr);
+  void convert_binary_expr(const exprt &expr, const exprt &op);
+  void convert_struct_expr(const exprt &expr);
+  void convert_constant_expr(const exprt &expr);
+  void convert_equality_expr(const exprt &expr);
+  void convert_comparison_expr(const exprt &expr);
+  void convert_plus_expr(const exprt &expr);
+  void convert_minus_expr(const exprt &expr);
+  void convert_with_expr(const exprt &expr);
   void convert_literal(const literalt l);
   void find_symbols(const exprt &expr);
   void find_symbols(const typet &type);

From c03c174eeeb33e3fe3958cf108985b3859c93f19 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Fri, 20 Jan 2017 14:22:40 +0000
Subject: [PATCH 3/4] Replaced loop with simpler expression

Previously we were piping a number of zeros inside a for loop. This can
be simply done use the string constructor.
---
 src/solvers/cvc/cvc_conv.cpp | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/solvers/cvc/cvc_conv.cpp b/src/solvers/cvc/cvc_conv.cpp
index 8102f86754d..a5cfa98aa78 100644
--- a/src/solvers/cvc/cvc_conv.cpp
+++ b/src/solvers/cvc/cvc_conv.cpp
@@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 #include <cctype>
+#include <string>
 
 #include <util/arith_tools.h>
 #include <util/std_types.h>
@@ -114,8 +115,8 @@ void cvc_convt::convert_binary_expr(const exprt &expr, const exprt &op)
     {
       out << "(0bin";
 
-      for(unsigned i=from_width; i<to_width; i++)
-        out << "0";
+      if(to_width > from_width)
+        out << std::string(to_width-from_width, '0');
 
       out << " @ ";
 
@@ -136,8 +137,8 @@ void cvc_convt::convert_binary_expr(const exprt &expr, const exprt &op)
     {
       out << "(0bin";
 
-      for(unsigned i=1; i<to_width; i++)
-        out << "0";
+      if(to_width > 1)
+        out << std::string(to_width-1, '0');
 
       out << " @ ";
 

From c9404cdfc1a33bd155c9322e2df5963a7428b77d Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Fri, 20 Jan 2017 14:24:05 +0000
Subject: [PATCH 4/4] Replaced a for loop with a ranged based for loop

---
 src/solvers/cvc/cvc_conv.cpp | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/src/solvers/cvc/cvc_conv.cpp b/src/solvers/cvc/cvc_conv.cpp
index a5cfa98aa78..6e01448d5e2 100644
--- a/src/solvers/cvc/cvc_conv.cpp
+++ b/src/solvers/cvc/cvc_conv.cpp
@@ -1619,17 +1619,15 @@ void cvc_convt::convert_type(const typet &type)
     const struct_typet::componentst &components=
       struct_type.components();
 
-    for(struct_typet::componentst::const_iterator
-        it=components.begin();
-        it!=components.end();
-        it++)
+    for(struct_typet::componentt component : components)
     {
-      if(it!=components.begin())
+      if(component!=components.front())
         out << ",";
+
       out << " ";
-      out << it->get(ID_name);
+      out << component.get_name();
       out << ": ";
-      convert_type(it->type());
+      convert_type(component.type());
     }
 
     out << " #]";