Make convert_bv return a reference instead of writing to parameter

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@1054 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/solvers/flattening/boolbv.cpp

@@ -136,32 +136,28 @@ Function: boolbvt::convert_bv
 
 \*******************************************************************/
 
-void boolbvt::convert_bv(const exprt &expr, bvt &bv)
+const bvt& boolbvt::convert_bv(const exprt &expr)
 {
   // check cache first
-  
+  std::pair<bv_cachet::iterator, bool> cache_result=
+    bv_cache.insert(std::make_pair(expr, bvt()));
+  if(!cache_result.second)
   {
-    bv_cachet::const_iterator cache_result=bv_cache.find(expr);
-    if(cache_result!=bv_cache.end())
-    {
-      //std::cerr << "Cache hit on " << expr << "\n";
-      bv=cache_result->second;
-      return;
-    }
+    //std::cerr << "Cache hit on " << expr << "\n";
+    return cache_result.first->second;
   }
 
-  convert_bitvector(expr, bv);
+  convert_bitvector(expr, cache_result.first->second);
 
   // check
-  forall_literals(it, bv)
+  forall_literals(it, cache_result.first->second)
     if(it->var_no()==literalt::unused_var_no())
     {
       std::cout << "unused_var_no: " << expr.pretty() << std::endl;
       assert(false);
     }
 
-  // insert into cache
-  bv_cache.insert(std::pair<const exprt, bvt>(expr, bv));
+  return cache_result.first->second;
 }
 
 /*******************************************************************\
@@ -370,26 +366,24 @@ void boolbvt::convert_array(const exprt &expr, bvt &bv)
   if(width==0)
     return conversion_failed(expr, bv);
 
-  bv.resize(width);
+  bv.reserve(width);
 
   if(expr.type().id()==ID_array)
   {
-    unsigned op_width=width/expr.operands().size();
-    unsigned offset=0;
+    assert(expr.has_operands());
+    const exprt::operandst &operands=expr.operands();
+    assert(!operands.empty());
+    unsigned op_width=width/operands.size();
 
-    forall_operands(it, expr)
+    forall_expr(it, operands)
     {
-      bvt tmp;
-
-      convert_bv(*it, tmp);
+      const bvt &tmp=convert_bv(*it);
 
       if(tmp.size()!=op_width)
         throw "convert_array: unexpected operand width";
 
-      for(unsigned j=0; j<op_width; j++)
-        bv[offset+j]=tmp[j];
-
-      offset+=op_width;
+      forall_literals(it2, tmp)
+        bv.push_back(*it2);
     }   
 
     return;
@@ -440,8 +434,7 @@ void boolbvt::convert_lambda(const exprt &expr, bvt &bv)
     exprt expr(expr.op1());
     replace_expr(expr.op0(), counter, expr);
 
-    bvt tmp;
-    convert_bv(expr, tmp);
+    const bvt &tmp=convert_bv(expr);
 
     unsigned offset=integer2long(i*tmp.size());
 
@@ -614,8 +607,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
     if(expr.operands().size()!=1)
       throw "sign expects one operand";
 
-    bvt bv;
-    convert_bv(operands[0], bv);
+    const bvt &bv=convert_bv(operands[0]);
 
     if(bv.size()<1)
       throw "sign operator takes one non-empty operand";
@@ -640,8 +632,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
     if(expr.operands().size()!=1)
       throw "isnan expects one operand";
 
-    bvt bv;
-    convert_bv(operands[0], bv);
+    const bvt &bv=convert_bv(operands[0]);
 
     if(expr.op0().type().id()==ID_floatbv)
     {
@@ -659,8 +650,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
     if(expr.operands().size()!=1)
       throw "isfinite expects one operand";
 
-    bvt bv;
-    convert_bv(operands[0], bv);
+    const bvt &bv=convert_bv(operands[0]);
 
     if(expr.op0().type().id()==ID_floatbv)
     {
@@ -680,8 +670,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
     if(expr.operands().size()!=1)
       throw "isinf expects one operand";
 
-    bvt bv;
-    convert_bv(operands[0], bv);
+    const bvt &bv=convert_bv(operands[0]);
 
     if(expr.op0().type().id()==ID_floatbv)
     {
@@ -699,8 +688,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
     if(expr.operands().size()!=1)
       throw "isnormal expects one operand";
 
-    bvt bv;
-    convert_bv(operands[0], bv);
+    const bvt &bv=convert_bv(operands[0]);
 
     if(expr.op0().type().id()==ID_floatbv)
     {
@@ -747,11 +735,10 @@ bool boolbvt::boolbv_set_equality_to_true(const exprt &expr)
       if(is_unbounded_array(type))
         return true;
 
-      bvt bv1;
-      convert_bv(operands[1], bv1);
+      const bvt &bv1=convert_bv(operands[1]);
 
       const irep_idt &identifier=
-        operands[0].get(ID_identifier);
+        to_symbol_expr(operands[0]).get_identifier();
 
       for(unsigned i=0; i<bv1.size(); i++)
         map.set_literal(identifier, i, type, bv1[i]);

src/solvers/flattening/boolbv.h

@@ -42,7 +42,7 @@ class boolbvt:public arrayst
   {
   }
 
-  virtual void convert_bv(const exprt &expr, bvt &bv); // check cache
+  virtual const bvt& convert_bv(const exprt &expr); // check cache
   virtual void convert_bitvector(const exprt &expr, bvt &bv); // no cache
 
   // overloading

src/solvers/flattening/boolbv_abs.cpp

@@ -41,8 +41,7 @@ void boolbvt::convert_abs(const exprt &expr, bvt &bv)
 
   const exprt &op0=expr.op0();
 
-  bvt op_bv;
-  convert_bv(op0, op_bv);
+  const bvt &op_bv=convert_bv(op0);
 
   if(op0.type()!=expr.type())
     return conversion_failed(expr, bv);

src/solvers/flattening/boolbv_add_sub.cpp

@@ -58,7 +58,7 @@ void boolbvt::convert_add_sub(const exprt &expr, bvt &bv)
     throw "add/sub with mixed types";
   }
 
-  convert_bv(op0, bv);
+  bv=convert_bv(op0);
 
   if(bv.size()!=width)
     throw "convert_add_sub: unexpected operand 0 width";
@@ -87,8 +87,7 @@ void boolbvt::convert_add_sub(const exprt &expr, bvt &bv)
       throw "add/sub with mixed types";
     }
 
-    bvt op;
-    convert_bv(*it, op);
+    const bvt &op=convert_bv(*it);
 
     if(op.size()!=width)
       throw "convert_add_sub: unexpected operand width";

src/solvers/flattening/boolbv_array_of.cpp

@@ -48,8 +48,7 @@ void boolbvt::convert_array_of(const exprt &expr, bvt &bv)
   if(to_integer(array_size, size))
     return conversion_failed(expr, bv);
 
-  bvt tmp;
-  convert_bv(expr.op0(), tmp);
+  const bvt &tmp=convert_bv(expr.op0());
 
   bv.resize(width);
 

src/solvers/flattening/boolbv_bitwise.cpp

@@ -34,8 +34,7 @@ void boolbvt::convert_bitwise(const exprt &expr, bvt &bv)
 
     const exprt &op0=expr.op0();
 
-    bvt op_bv;
-    convert_bv(op0, op_bv);
+    const bvt &op_bv=convert_bv(op0);
 
     bv.resize(width);
 
@@ -57,9 +56,7 @@ void boolbvt::convert_bitwise(const exprt &expr, bvt &bv)
 
     forall_operands(it, expr)
     {
-      bvt op;
-
-      convert_bv(*it, op);
+      const bvt &op=convert_bv(*it);
 
       if(op.size()!=width)
         throw "convert_bitwise: unexpected operand width";

src/solvers/flattening/boolbv_bv_rel.cpp

@@ -37,10 +37,8 @@ literalt boolbvt::convert_bv_rel(const exprt &expr)
     const exprt &op0=expr.op0();
     const exprt &op1=expr.op1();
 
-    bvt bv0, bv1;
-
-    convert_bv(op0, bv0);
-    convert_bv(op1, bv1);
+    const bvt &bv0=convert_bv(op0);
+    const bvt &bv1=convert_bv(op1);
 
     bvtypet bvtype0=get_bvtype(op0.type());
     bvtypet bvtype1=get_bvtype(op1.type());

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -36,7 +36,7 @@ void boolbvt::convert_byte_extract(const exprt &expr, bvt &bv)
   if(is_unbounded_array(expr.op0().type()))
   {
     exprt tmp=flatten_byte_extract(expr, ns);
-    convert_bv(tmp, bv);
+    bv=convert_bv(tmp);
     return;
   }
 
@@ -59,8 +59,7 @@ void boolbvt::convert_byte_extract(const exprt &expr, bvt &bv)
 
   // first do op0
 
-  bvt op0_bv;  
-  convert_bv(op0, op0_bv);
+  const bvt &op0_bv=convert_bv(op0);
 
   // see if the byte number is constant
 

src/solvers/flattening/boolbv_byte_update.cpp

@@ -45,10 +45,9 @@ void boolbvt::convert_byte_update(const exprt &expr, bvt &bv)
   else
     assert(false);
 
-  convert_bv(op0, bv);
+  bv=convert_bv(op0);
 
-  bvt op2_bv;
-  convert_bv(op2, op2_bv);
+  const bvt &op2_bv=convert_bv(op2);
   unsigned update_width=op2_bv.size();
   unsigned byte_width=8;
 

src/solvers/flattening/boolbv_case.cpp

@@ -50,9 +50,7 @@ void boolbvt::convert_case(const exprt &expr, bvt &bv)
 
   forall_operands(it, expr)
   {
-    bvt op;
-
-    convert_bv(*it, op);
+    bvt op=convert_bv(*it);
 
     switch(what)
     {

src/solvers/flattening/boolbv_concatenation.cpp

@@ -37,9 +37,7 @@ void boolbvt::convert_concatenation(const exprt &expr, bvt &bv)
 
   forall_expr(it, operands)
   {
-    bvt op;
-
-    convert_bv(*it, op);
+    const bvt &op=convert_bv(*it);
 
     if(op.size()>offset)
       throw "concatenation operand width too big";

src/solvers/flattening/boolbv_cond.cpp

@@ -60,9 +60,7 @@ void boolbvt::convert_cond(const exprt &expr, bvt &bv)
       }
       else
       {
-        bvt op;
-
-        convert_bv(*it, op);
+        const bvt &op=convert_bv(*it);
 
         if(bv.size()!=op.size())
         {
@@ -94,9 +92,7 @@ void boolbvt::convert_cond(const exprt &expr, bvt &bv)
 
       literalt cond_literal=convert(cond);
 
-      bvt op;
-
-      convert_bv(value, op);
+      const bvt &op=convert_bv(value);
 
       if(bv.size()!=op.size())
         throw "unexpected operand size in convert_cond";

src/solvers/flattening/boolbv_constant.cpp

@@ -36,9 +36,7 @@ void boolbvt::convert_constant(const exprt &expr, bvt &bv)
 
     forall_operands(it, expr)
     {
-      bvt tmp;
-
-      convert_bv(*it, tmp);
+      const bvt &tmp=convert_bv(*it);
 
       if(tmp.size()!=op_width)
         throw "convert_constant: unexpected operand width";

src/solvers/flattening/boolbv_constraint_select_one.cpp

@@ -36,11 +36,10 @@ void boolbvt::convert_constraint_select_one(const exprt &expr, bvt &bv)
   if(prop.has_set_to())
   {
     std::vector<bvt> op_bv;
-    op_bv.resize(expr.operands().size());
+    op_bv.reserve(expr.operands().size());
 
-    unsigned i=0;
     forall_operands(it, expr)
-      convert_bv(*it, op_bv[i++]);
+      op_bv.push_back(convert_bv(*it));
 
     bv=op_bv[0];
 
@@ -70,8 +69,7 @@ void boolbvt::convert_constraint_select_one(const exprt &expr, bvt &bv)
     unsigned op_nr=0;
     forall_operands(it, expr)
     {
-      bvt op_bv;
-      convert_bv(*it, op_bv);
+      const bvt &op_bv=convert_bv(*it);
 
       if(op_nr==0)
         bv=op_bv;

src/solvers/flattening/boolbv_div.cpp

@@ -46,10 +46,8 @@ void boolbvt::convert_div(const exprt &expr, bvt &bv)
      expr.op1().type().id()!=expr.type().id())
     return conversion_failed(expr, bv);
 
-  bvt op0, op1;
-
-  convert_bv(expr.op0(), op0);
-  convert_bv(expr.op1(), op1);
+  bvt op0=convert_bv(expr.op0());
+  bvt op1=convert_bv(expr.op1());
 
   if(op0.size()!=width ||
      op1.size()!=width)

src/solvers/flattening/boolbv_equality.cpp

@@ -54,10 +54,8 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
     return record_array_equality(expr);
   }
 
-  bvt bv0, bv1;
-  
-  convert_bv(expr.lhs(), bv0);
-  convert_bv(expr.rhs(), bv1);
+  const bvt &bv0=convert_bv(expr.lhs());
+  const bvt &bv1=convert_bv(expr.rhs());
 
   if(bv0.size()!=bv1.size())
   {

src/solvers/flattening/boolbv_extractbit.cpp

@@ -33,8 +33,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
   if(operands.size()!=2)
     throw "extractbit takes two operands";
 
-  bvt bv0;
-  convert_bv(operands[0], bv0);
+  const bvt &bv0=convert_bv(operands[0]);
 
   // constant?
   if(operands[1].is_constant())

src/solvers/flattening/boolbv_extractbits.cpp

@@ -39,9 +39,7 @@ void boolbvt::convert_extractbits(const extractbits_exprt &expr, bvt &bv)
     throw "extractbits takes three operands";
 
   mp_integer o1, o2;
-  bvt bv0;
-
-  convert_bv(expr.op0(), bv0);
+  const bvt &bv0=convert_bv(expr.op0());
 
   // We only do constants for now.
   // Should implement a shift here.