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  if(expr.id()==ID_overflow_plus ||
18  expr.id()==ID_overflow_minus)
19  {
20  const auto &overflow_expr = to_binary_expr(expr);
21 
22  const bvt &bv0 = convert_bv(overflow_expr.lhs());
23  const bvt &bv1 = convert_bv(overflow_expr.rhs());
24 
25  if(bv0.size()!=bv1.size())
26  return SUB::convert_rest(expr);
27 
29  overflow_expr.lhs().type().id() == ID_signedbv
32 
33  return expr.id()==ID_overflow_minus?
34  bv_utils.overflow_sub(bv0, bv1, rep):
35  bv_utils.overflow_add(bv0, bv1, rep);
36  }
37  else if(expr.id()==ID_overflow_mult)
38  {
39  const auto &overflow_expr = to_binary_expr(expr);
40 
41  if(
42  overflow_expr.lhs().type().id() != ID_unsignedbv &&
43  overflow_expr.lhs().type().id() != ID_signedbv)
44  return SUB::convert_rest(expr);
45 
46  bvt bv0 = convert_bv(overflow_expr.lhs());
47  bvt bv1 = convert_bv(overflow_expr.rhs(), bv0.size());
48 
50  overflow_expr.lhs().type().id() == ID_signedbv
53 
55  overflow_expr.lhs().type() == overflow_expr.rhs().type(),
56  "operands of overflow_mult expression shall have same type");
57 
58  std::size_t old_size=bv0.size();
59  std::size_t new_size=old_size*2;
60 
61  // sign/zero extension
62  bv0=bv_utils.extension(bv0, new_size, rep);
63  bv1=bv_utils.extension(bv1, new_size, rep);
64 
65  bvt result=bv_utils.multiplier(bv0, bv1, rep);
66 
68  {
69  bvt bv_overflow;
70  bv_overflow.reserve(old_size);
71 
72  // get top result bits
73  for(std::size_t i=old_size; i<result.size(); i++)
74  bv_overflow.push_back(result[i]);
75 
76  return prop.lor(bv_overflow);
77  }
78  else
79  {
80  bvt bv_overflow;
81  bv_overflow.reserve(old_size);
82 
83  // get top result bits, plus one more
84  DATA_INVARIANT(old_size!=0, "zero-size operand");
85  for(std::size_t i=old_size-1; i<result.size(); i++)
86  bv_overflow.push_back(result[i]);
87 
88  // these need to be either all 1's or all 0's
89  literalt all_one=prop.land(bv_overflow);
90  literalt all_zero=!prop.lor(bv_overflow);
91  return !prop.lor(all_one, all_zero);
92  }
93  }
94  else if(expr.id() == ID_overflow_shl)
95  {
96  const auto &overflow_expr = to_binary_expr(expr);
97 
98  const bvt &bv0 = convert_bv(overflow_expr.lhs());
99  const bvt &bv1 = convert_bv(overflow_expr.rhs());
100 
101  std::size_t old_size = bv0.size();
102  std::size_t new_size = old_size * 2;
103 
105  overflow_expr.lhs().type().id() == ID_signedbv
108 
109  bvt bv_ext=bv_utils.extension(bv0, new_size, rep);
110 
111  bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::SHIFT_LEFT, bv1);
112 
113  // a negative shift is undefined; yet this isn't an overflow
114  literalt neg_shift = overflow_expr.lhs().type().id() == ID_unsignedbv
115  ? const_literal(false)
116  : bv1.back(); // sign bit
117 
118  // an undefined shift of a non-zero value always results in overflow; the
119  // use of unsigned comparision is safe here as we cover the signed negative
120  // case via neg_shift
121  literalt undef =
122  bv_utils.rel(
123  bv1,
124  ID_gt,
125  bv_utils.build_constant(old_size, bv1.size()),
127 
128  literalt overflow;
129 
131  {
132  // get top result bits
133  result.erase(result.begin(), result.begin() + old_size);
134 
135  // one of the top bits is non-zero
136  overflow=prop.lor(result);
137  }
138  else
139  {
140  // get top result bits plus sign bit
141  DATA_INVARIANT(old_size != 0, "zero-size operand");
142  result.erase(result.begin(), result.begin() + old_size - 1);
143 
144  // the sign bit has changed
145  literalt sign_change=!prop.lequal(bv0.back(), result.front());
146 
147  // these need to be either all 1's or all 0's
148  literalt all_one=prop.land(result);
149  literalt all_zero=!prop.lor(result);
150 
151  overflow=prop.lor(sign_change, !prop.lor(all_one, all_zero));
152  }
153 
154  // a negative shift isn't an overflow; else check the conditions built
155  // above
156  return
157  prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow));
158  }
159  else if(expr.id()==ID_overflow_unary_minus)
160  {
161  const auto &overflow_expr = to_unary_expr(expr);
162 
163  const bvt &bv = convert_bv(overflow_expr.op());
164 
165  return bv_utils.overflow_negate(bv);
166  }
167 
168  return SUB::convert_rest(expr);
169 }
bv_utilst::shiftt::SHIFT_LEFT
@ SHIFT_LEFT
boolbvt::convert_overflow
virtual literalt convert_overflow(const exprt &expr)
Definition: boolbv_overflow.cpp:15
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
bvt
std::vector< literalt > bvt
Definition: literal.h:201
prefix.h
bv_utilst::representationt::UNSIGNED
@ UNSIGNED
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
propt::lor
virtual literalt lor(literalt a, literalt b)=0
propt::land
virtual literalt land(literalt a, literalt b)=0
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
bv_utilst::shift
bvt shift(const bvt &op, const shiftt shift, std::size_t distance)
Definition: bv_utils.cpp:481
string2int.h
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:511
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
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
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:418
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:119
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv_solver.cpp:349
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:1290
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:98
bv_utilst::extension
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
Definition: bv_utils.cpp:109
literalt
Definition: literal.h:26
bv_utilst::multiplier
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:810
boolbv.h
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131