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 <cassert>
12 
13 #include <util/prefix.h>
14 #include <util/string2int.h>
15 
17 {
18  const exprt::operandst &operands=expr.operands();
19 
20  if(expr.id()==ID_overflow_plus ||
21  expr.id()==ID_overflow_minus)
22  {
23  if(operands.size()!=2)
24  throw "operator "+expr.id_string()+" takes 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  {
42  if(operands.size()!=2)
43  throw "operator "+expr.id_string()+" takes two operands";
44 
45  if(operands[0].type().id()!=ID_unsignedbv &&
46  operands[0].type().id()!=ID_signedbv)
47  return SUB::convert_rest(expr);
48 
49  bvt bv0=convert_bv(operands[0]);
50  bvt bv1=convert_bv(operands[1]);
51 
52  if(bv0.size()!=bv1.size())
53  throw "operand size mismatch on overflow-*";
54 
56  operands[0].type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
58 
59  if(operands[0].type()!=operands[1].type())
60  throw "operand type mismatch on overflow-*";
61 
62  assert(bv0.size()==bv1.size());
63  std::size_t old_size=bv0.size();
64  std::size_t new_size=old_size*2;
65 
66  // sign/zero extension
67  bv0=bv_utils.extension(bv0, new_size, rep);
68  bv1=bv_utils.extension(bv1, new_size, rep);
69 
70  bvt result=bv_utils.multiplier(bv0, bv1, rep);
71 
73  {
74  bvt bv_overflow;
75  bv_overflow.reserve(old_size);
76 
77  // get top result bits
78  for(std::size_t i=old_size; i<result.size(); i++)
79  bv_overflow.push_back(result[i]);
80 
81  return prop.lor(bv_overflow);
82  }
83  else
84  {
85  bvt bv_overflow;
86  bv_overflow.reserve(old_size);
87 
88  // get top result bits, plus one more
89  assert(old_size!=0);
90  for(std::size_t i=old_size-1; i<result.size(); i++)
91  bv_overflow.push_back(result[i]);
92 
93  // these need to be either all 1's or all 0's
94  literalt all_one=prop.land(bv_overflow);
95  literalt all_zero=!prop.lor(bv_overflow);
96  return !prop.lor(all_one, all_zero);
97  }
98  }
99  else if(expr.id()==ID_overflow_unary_minus)
100  {
101  if(operands.size()!=1)
102  throw "operator "+expr.id_string()+" takes one operand";
103 
104  const bvt &bv=convert_bv(operands[0]);
105 
106  return bv_utils.overflow_negate(bv);
107  }
108  else if(has_prefix(expr.id_string(), "overflow-typecast-"))
109  {
110  std::size_t bits=unsafe_string2unsigned(id2string(expr.id()).substr(18));
111 
112  const exprt::operandst &operands=expr.operands();
113 
114  if(operands.size()!=1)
115  throw "operator "+expr.id_string()+" takes one operand";
116 
117  const exprt &op=operands[0];
118 
119  const bvt &bv=convert_bv(op);
120 
121  if(bits>=bv.size() || bits==0)
122  throw "overflow-typecast got wrong number of bits";
123 
124  // signed or unsigned?
125  if(op.type().id()==ID_signedbv)
126  {
127  bvt tmp_bv;
128  for(std::size_t i=bits; i<bv.size(); i++)
129  tmp_bv.push_back(prop.lxor(bv[bits-1], bv[i]));
130 
131  return prop.lor(tmp_bv);
132  }
133  else
134  {
135  bvt tmp_bv;
136  for(std::size_t i=bits; i<bv.size(); i++)
137  tmp_bv.push_back(bv[i]);
138 
139  return prop.lor(tmp_bv);
140  }
141  }
142 
143  return SUB::convert_rest(expr);
144 }
mstreamt & result()
Definition: message.h:233
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:44
exprt & op0()
Definition: expr.h:84
virtual literalt convert_overflow(const exprt &expr)
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
virtual literalt lor(literalt a, literalt b)=0
representationt
Definition: bv_utils.h:31
typet & type()
Definition: expr.h:60
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:527
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
virtual literalt lxor(literalt a, literalt b)=0
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:791
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
Base class for all expressions.
Definition: expr.h:46
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:337
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
literalt overflow_add(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:367
operandst & operands()
Definition: expr.h:70
std::vector< literalt > bvt
Definition: literal.h:197