cprover
boolbv_add_sub.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <util/invariant.h>
12 #include <util/std_types.h>
13 
15 
17 {
18  const typet &type=ns.follow(expr.type());
19 
20  if(type.id()!=ID_unsignedbv &&
21  type.id()!=ID_signedbv &&
22  type.id()!=ID_fixedbv &&
23  type.id()!=ID_floatbv &&
24  type.id()!=ID_range &&
25  type.id()!=ID_complex &&
26  type.id()!=ID_vector)
27  return conversion_failed(expr);
28 
29  std::size_t width=boolbv_width(type);
30 
31  if(width==0)
32  return conversion_failed(expr);
33 
34  const exprt::operandst &operands=expr.operands();
35 
36  if(operands.empty())
37  throw "operator "+expr.id_string()+" takes at least one operand";
38 
39  const exprt &op0=expr.op0();
41  op0.type() == type, "add/sub with mixed types:\n" + expr.pretty());
42 
43  bvt bv=convert_bv(op0);
44 
45  if(bv.size()!=width)
46  throw "convert_add_sub: unexpected operand 0 width";
47 
48  bool subtract=(expr.id()==ID_minus ||
49  expr.id()=="no-overflow-minus");
50 
51  bool no_overflow=(expr.id()=="no-overflow-plus" ||
52  expr.id()=="no-overflow-minus");
53 
54  typet arithmetic_type=
55  (type.id()==ID_vector || type.id()==ID_complex)?
56  ns.follow(type.subtype()):type;
57 
59  (arithmetic_type.id()==ID_signedbv ||
60  arithmetic_type.id()==ID_fixedbv)?bv_utilst::representationt::SIGNED:
62 
63  for(exprt::operandst::const_iterator
64  it=operands.begin()+1;
65  it!=operands.end(); it++)
66  {
68  it->type() == type, "add/sub with mixed types:\n" + expr.pretty());
69 
70  const bvt &op=convert_bv(*it);
71 
72  if(op.size()!=width)
73  throw "convert_add_sub: unexpected operand width";
74 
75  if(type.id()==ID_vector || type.id()==ID_complex)
76  {
77  const typet &subtype=ns.follow(type.subtype());
78 
79  std::size_t sub_width=boolbv_width(subtype);
80 
81  if(sub_width==0 || width%sub_width!=0)
82  throw "convert_add_sub: unexpected vector operand width";
83 
84  std::size_t size=width/sub_width;
85  bv.resize(width);
86 
87  for(std::size_t i=0; i<size; i++)
88  {
89  bvt tmp_op;
90  tmp_op.resize(sub_width);
91 
92  for(std::size_t j=0; j<tmp_op.size(); j++)
93  {
94  assert(i*sub_width+j<op.size());
95  tmp_op[j]=op[i*sub_width+j];
96  }
97 
98  bvt tmp_result;
99  tmp_result.resize(sub_width);
100 
101  for(std::size_t j=0; j<tmp_result.size(); j++)
102  {
103  assert(i*sub_width+j<bv.size());
104  tmp_result[j]=bv[i*sub_width+j];
105  }
106 
107  if(type.subtype().id()==ID_floatbv)
108  {
109  // needs to change due to rounding mode
110  float_utilst float_utils(prop, to_floatbv_type(subtype));
111  tmp_result=float_utils.add_sub(tmp_result, tmp_op, subtract);
112  }
113  else
114  tmp_result=bv_utils.add_sub(tmp_result, tmp_op, subtract);
115 
116  assert(tmp_result.size()==sub_width);
117 
118  for(std::size_t j=0; j<tmp_result.size(); j++)
119  {
120  assert(i*sub_width+j<bv.size());
121  bv[i*sub_width+j]=tmp_result[j];
122  }
123  }
124  }
125  else if(type.id()==ID_floatbv)
126  {
127  // needs to change due to rounding mode
128  float_utilst float_utils(prop, to_floatbv_type(arithmetic_type));
129  bv=float_utils.add_sub(bv, op, subtract);
130  }
131  else if(no_overflow)
132  bv=bv_utils.add_sub_no_overflow(bv, op, subtract, rep);
133  else
134  bv=bv_utils.add_sub(bv, op, subtract);
135  }
136 
137  return bv;
138 }
The type of an expression.
Definition: type.h:22
bv_utilst bv_utils
Definition: boolbv.h:93
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition: bv_utils.cpp:328
boolbv_widtht boolbv_width
Definition: boolbv.h:90
representationt
Definition: bv_utils.h:31
typet & type()
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:259
virtual bvt convert_add_sub(const exprt &expr)
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const namespacet & ns
const typet & follow(const typet &) const
Definition: namespace.cpp:55
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
std::vector< exprt > operandst
Definition: expr.h:45
API to type classes.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1382
Base class for all expressions.
Definition: expr.h:42
const std::string & id_string() const
Definition: irep.h:262
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
operandst & operands()
Definition: expr.h:66
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition: bv_utils.cpp:339
std::vector< literalt > bvt
Definition: literal.h:200