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