cprover
boolbv_overflow.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/prefix.h>
13 #include <util/string2int.h>
14 
16 {
17  const exprt::operandst &operands=expr.operands();
18 
19  if(expr.id()==ID_overflow_plus ||
20  expr.id()==ID_overflow_minus)
21  {
22  if(operands.size()!=2)
23  throw "operator "+expr.id_string()+" takes two operands";
24 
25  const bvt &bv0=convert_bv(operands[0]);
26  const bvt &bv1=convert_bv(operands[1]);
27 
28  if(bv0.size()!=bv1.size())
29  return SUB::convert_rest(expr);
30 
32  expr.op0().type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
34 
35  return expr.id()==ID_overflow_minus?
36  bv_utils.overflow_sub(bv0, bv1, rep):
37  bv_utils.overflow_add(bv0, bv1, rep);
38  }
39  else if(expr.id()==ID_overflow_mult)
40  {
41  if(operands.size()!=2)
42  throw "operator "+expr.id_string()+" takes two operands";
43 
44  if(operands[0].type().id()!=ID_unsignedbv &&
45  operands[0].type().id()!=ID_signedbv)
46  return SUB::convert_rest(expr);
47 
48  bvt bv0=convert_bv(operands[0]);
49  bvt bv1=convert_bv(operands[1]);
50 
51  if(bv0.size()!=bv1.size())
52  throw "operand size mismatch on overflow-*";
53 
55  operands[0].type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
57 
58  if(operands[0].type()!=operands[1].type())
59  throw "operand type mismatch on overflow-*";
60 
61  DATA_INVARIANT(bv0.size()==bv1.size(), "operands size mismatch");
62  std::size_t old_size=bv0.size();
63  std::size_t new_size=old_size*2;
64 
65  // sign/zero extension
66  bv0=bv_utils.extension(bv0, new_size, rep);
67  bv1=bv_utils.extension(bv1, new_size, rep);
68 
69  bvt result=bv_utils.multiplier(bv0, bv1, rep);
70 
72  {
73  bvt bv_overflow;
74  bv_overflow.reserve(old_size);
75 
76  // get top result bits
77  for(std::size_t i=old_size; i<result.size(); i++)
78  bv_overflow.push_back(result[i]);
79 
80  return prop.lor(bv_overflow);
81  }
82  else
83  {
84  bvt bv_overflow;
85  bv_overflow.reserve(old_size);
86 
87  // get top result bits, plus one more
88  DATA_INVARIANT(old_size!=0, "zero-size operand");
89  for(std::size_t i=old_size-1; i<result.size(); i++)
90  bv_overflow.push_back(result[i]);
91 
92  // these need to be either all 1's or all 0's
93  literalt all_one=prop.land(bv_overflow);
94  literalt all_zero=!prop.lor(bv_overflow);
95  return !prop.lor(all_one, all_zero);
96  }
97  }
98  else if(expr.id() == ID_overflow_shl)
99  {
100  if(operands.size() != 2)
101  throw "operator " + expr.id_string() + " takes two operands";
102 
103  const bvt &bv0=convert_bv(operands[0]);
104  const bvt &bv1=convert_bv(operands[1]);
105 
106  std::size_t old_size = bv0.size();
107  std::size_t new_size = old_size * 2;
108 
110  operands[0].type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
112 
113  bvt bv_ext=bv_utils.extension(bv0, new_size, rep);
114 
116 
117  // a negative shift is undefined; yet this isn't an overflow
118  literalt neg_shift =
119  operands[1].type().id() == ID_unsignedbv ?
120  const_literal(false) :
121  bv1.back(); // sign bit
122 
123  // an undefined shift of a non-zero value always results in overflow; the
124  // use of unsigned comparision is safe here as we cover the signed negative
125  // case via neg_shift
126  literalt undef =
127  bv_utils.rel(
128  bv1,
129  ID_gt,
130  bv_utils.build_constant(old_size, bv1.size()),
132 
133  literalt overflow;
134 
136  {
137  // get top result bits
138  result.erase(result.begin(), result.begin() + old_size);
139 
140  // one of the top bits is non-zero
141  overflow=prop.lor(result);
142  }
143  else
144  {
145  // get top result bits plus sign bit
146  DATA_INVARIANT(old_size != 0, "zero-size operand");
147  result.erase(result.begin(), result.begin() + old_size - 1);
148 
149  // the sign bit has changed
150  literalt sign_change=!prop.lequal(bv0.back(), result.front());
151 
152  // these need to be either all 1's or all 0's
153  literalt all_one=prop.land(result);
154  literalt all_zero=!prop.lor(result);
155 
156  overflow=prop.lor(sign_change, !prop.lor(all_one, all_zero));
157  }
158 
159  // a negative shift isn't an overflow; else check the conditions built
160  // above
161  return
162  prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow));
163  }
164  else if(expr.id()==ID_overflow_unary_minus)
165  {
166  if(operands.size()!=1)
167  throw "operator "+expr.id_string()+" takes one operand";
168 
169  const bvt &bv=convert_bv(operands[0]);
170 
171  return bv_utils.overflow_negate(bv);
172  }
173  else if(has_prefix(expr.id_string(), "overflow-typecast-"))
174  {
175  std::size_t bits=unsafe_string2unsigned(id2string(expr.id()).substr(18));
176 
177  const exprt::operandst &operands=expr.operands();
178 
179  if(operands.size()!=1)
180  throw "operator "+expr.id_string()+" takes one operand";
181 
182  const exprt &op=operands[0];
183 
184  const bvt &bv=convert_bv(op);
185 
186  if(bits>=bv.size() || bits==0)
187  throw "overflow-typecast got wrong number of bits";
188 
189  // signed or unsigned?
190  if(op.type().id()==ID_signedbv)
191  {
192  bvt tmp_bv;
193  for(std::size_t i=bits; i<bv.size(); i++)
194  tmp_bv.push_back(prop.lxor(bv[bits-1], bv[i]));
195 
196  return prop.lor(tmp_bv);
197  }
198  else
199  {
200  bvt tmp_bv;
201  for(std::size_t i=bits; i<bv.size(); i++)
202  tmp_bv.push_back(bv[i]);
203 
204  return prop.lor(tmp_bv);
205  }
206  }
207 
208  return SUB::convert_rest(expr);
209 }
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:109
bv_utilst bv_utils
Definition: boolbv.h:93
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
exprt & op0()
Definition: expr.h:72
virtual literalt convert_overflow(const exprt &expr)
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:69
virtual literalt lor(literalt a, literalt b)=0
representationt
Definition: bv_utils.h:31
typet & type()
Definition: expr.h:56
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:189
literalt overflow_negate(const bvt &op)
Definition: bv_utils.cpp:546
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1281
virtual literalt lxor(literalt a, literalt b)=0
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:810
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
std::vector< exprt > operandst
Definition: expr.h:45
virtual literalt lequal(literalt a, literalt b)=0
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:480
literalt const_literal(bool value)
Definition: literal.h:187
mstreamt & result() const
Definition: message.h:312
Base class for all expressions.
Definition: expr.h:42
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:331
const std::string & id_string() const
Definition: irep.h:192
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:391
virtual literalt lselect(literalt a, literalt b, literalt c)=0
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:367
operandst & operands()
Definition: expr.h:66
std::vector< literalt > bvt
Definition: literal.h:200
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15