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  {
23  operands.size() == 2,
24  "expression " + expr.id_string() + " should have two operands");
25 
26  const bvt &bv0=convert_bv(operands[0]);
27  const bvt &bv1=convert_bv(operands[1]);
28 
29  if(bv0.size()!=bv1.size())
30  return SUB::convert_rest(expr);
31 
33  expr.op0().type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
35 
36  return expr.id()==ID_overflow_minus?
37  bv_utils.overflow_sub(bv0, bv1, rep):
38  bv_utils.overflow_add(bv0, bv1, rep);
39  }
40  else if(expr.id()==ID_overflow_mult)
41  {
43  operands.size() == 2,
44  "overflow_mult expression should have two operands");
45 
46  if(operands[0].type().id()!=ID_unsignedbv &&
47  operands[0].type().id()!=ID_signedbv)
48  return SUB::convert_rest(expr);
49 
50  bvt bv0=convert_bv(operands[0]);
51  bvt bv1 = convert_bv(operands[1], bv0.size());
52 
54  operands[0].type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
56 
58  operands[0].type() == operands[1].type(),
59  "operands of overflow_mult expression shall have same type");
60 
61  std::size_t old_size=bv0.size();
62  std::size_t new_size=old_size*2;
63 
64  // sign/zero extension
65  bv0=bv_utils.extension(bv0, new_size, rep);
66  bv1=bv_utils.extension(bv1, new_size, rep);
67 
68  bvt result=bv_utils.multiplier(bv0, bv1, rep);
69 
71  {
72  bvt bv_overflow;
73  bv_overflow.reserve(old_size);
74 
75  // get top result bits
76  for(std::size_t i=old_size; i<result.size(); i++)
77  bv_overflow.push_back(result[i]);
78 
79  return prop.lor(bv_overflow);
80  }
81  else
82  {
83  bvt bv_overflow;
84  bv_overflow.reserve(old_size);
85 
86  // get top result bits, plus one more
87  DATA_INVARIANT(old_size!=0, "zero-size operand");
88  for(std::size_t i=old_size-1; i<result.size(); i++)
89  bv_overflow.push_back(result[i]);
90 
91  // these need to be either all 1's or all 0's
92  literalt all_one=prop.land(bv_overflow);
93  literalt all_zero=!prop.lor(bv_overflow);
94  return !prop.lor(all_one, all_zero);
95  }
96  }
97  else if(expr.id() == ID_overflow_shl)
98  {
100  operands.size() == 2, "overflow_shl expression should have two operands");
101 
102  const bvt &bv0=convert_bv(operands[0]);
103  const bvt &bv1=convert_bv(operands[1]);
104 
105  std::size_t old_size = bv0.size();
106  std::size_t new_size = old_size * 2;
107 
109  operands[0].type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
111 
112  bvt bv_ext=bv_utils.extension(bv0, new_size, rep);
113 
115 
116  // a negative shift is undefined; yet this isn't an overflow
117  literalt neg_shift =
118  operands[1].type().id() == ID_unsignedbv ?
119  const_literal(false) :
120  bv1.back(); // sign bit
121 
122  // an undefined shift of a non-zero value always results in overflow; the
123  // use of unsigned comparision is safe here as we cover the signed negative
124  // case via neg_shift
125  literalt undef =
126  bv_utils.rel(
127  bv1,
128  ID_gt,
129  bv_utils.build_constant(old_size, bv1.size()),
131 
132  literalt overflow;
133 
135  {
136  // get top result bits
137  result.erase(result.begin(), result.begin() + old_size);
138 
139  // one of the top bits is non-zero
140  overflow=prop.lor(result);
141  }
142  else
143  {
144  // get top result bits plus sign bit
145  DATA_INVARIANT(old_size != 0, "zero-size operand");
146  result.erase(result.begin(), result.begin() + old_size - 1);
147 
148  // the sign bit has changed
149  literalt sign_change=!prop.lequal(bv0.back(), result.front());
150 
151  // these need to be either all 1's or all 0's
152  literalt all_one=prop.land(result);
153  literalt all_zero=!prop.lor(result);
154 
155  overflow=prop.lor(sign_change, !prop.lor(all_one, all_zero));
156  }
157 
158  // a negative shift isn't an overflow; else check the conditions built
159  // above
160  return
161  prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow));
162  }
163  else if(expr.id()==ID_overflow_unary_minus)
164  {
166  operands.size() == 1,
167  "overflow_unary_minus expression should have one operand");
168 
169  const bvt &bv=convert_bv(operands[0]);
170 
171  return bv_utils.overflow_negate(bv);
172  }
173 
174  return SUB::convert_rest(expr);
175 }
bv_utilst::shiftt::SHIFT_LEFT
@ SHIFT_LEFT
boolbvt::convert_overflow
virtual literalt convert_overflow(const exprt &expr)
Definition: boolbv_overflow.cpp:15
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
bvt
std::vector< literalt > bvt
Definition: literal.h:200
prefix.h
bv_utilst::representationt::UNSIGNED
@ UNSIGNED
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:84
invariant.h
propt::lor
virtual literalt lor(literalt a, literalt b)=0
propt::land
virtual literalt land(literalt a, literalt b)=0
bv_utilst::shift
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:481
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
messaget::result
mstreamt & result() const
Definition: message.h:396
bv_utilst::representationt::SIGNED
@ SIGNED
bv_utilst::representationt
representationt
Definition: bv_utils.h:31
bv_utilst::overflow_sub
literalt overflow_sub(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:391
irept::id_string
const std::string & id_string() const
Definition: irep.h:262
const_literal
literalt const_literal(bool value)
Definition: literal.h:187
bv_utilst::overflow_add
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:367
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:330
bv_utilst::build_constant
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
propt::lequal
virtual literalt lequal(literalt a, literalt b)=0
bv_utilst::rel
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
Definition: bv_utils.cpp:1293
bv_utilst::overflow_negate
literalt overflow_negate(const bvt &op)
Definition: bv_utils.cpp:547
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:95
bv_utilst::extension
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:109
literalt
Definition: literal.h:24
bv_utilst::multiplier
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:812
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:78
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152