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 <util/bitvector_types.h>
12 #include <util/invariant.h>
13 
15 
17 {
19  expr.id() == ID_plus || expr.id() == ID_minus ||
20  expr.id() == "no-overflow-plus" || expr.id() == "no-overflow-minus");
21 
22  const typet &type = expr.type();
23 
24  if(type.id()!=ID_unsignedbv &&
25  type.id()!=ID_signedbv &&
26  type.id()!=ID_fixedbv &&
27  type.id()!=ID_floatbv &&
28  type.id()!=ID_range &&
29  type.id()!=ID_complex &&
30  type.id()!=ID_vector)
31  return conversion_failed(expr);
32 
33  std::size_t width=boolbv_width(type);
34 
35  if(width==0)
36  return conversion_failed(expr);
37 
38  const exprt::operandst &operands=expr.operands();
39 
41  !operands.empty(),
42  "operator " + expr.id_string() + " takes at least one operand");
43 
44  const exprt &op0 = to_multi_ary_expr(expr).op0();
46  op0.type() == type, "add/sub with mixed types:\n" + expr.pretty());
47 
48  bvt bv = convert_bv(op0, width);
49 
50  bool subtract=(expr.id()==ID_minus ||
51  expr.id()=="no-overflow-minus");
52 
53  bool no_overflow=(expr.id()=="no-overflow-plus" ||
54  expr.id()=="no-overflow-minus");
55 
56  typet arithmetic_type = (type.id() == ID_vector || type.id() == ID_complex)
58  : type;
59 
61  (arithmetic_type.id()==ID_signedbv ||
62  arithmetic_type.id()==ID_fixedbv)?bv_utilst::representationt::SIGNED:
64 
65  for(exprt::operandst::const_iterator
66  it=operands.begin()+1;
67  it!=operands.end(); it++)
68  {
70  it->type() == type, "add/sub with mixed types:\n" + expr.pretty());
71 
72  const bvt &op = convert_bv(*it, width);
73 
74  if(type.id()==ID_vector || type.id()==ID_complex)
75  {
76  std::size_t sub_width =
77  boolbv_width(to_type_with_subtype(type).subtype());
78 
79  INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
80  INVARIANT(
81  width % sub_width == 0,
82  "total vector bit width shall be a multiple of the element bit width");
83 
84  std::size_t size=width/sub_width;
85  bv.resize(width);
86 
87  for(std::size_t i=0; i<size; i++)
88  {
89  bvt tmp_op;
90  tmp_op.resize(sub_width);
91 
92  for(std::size_t j=0; j<tmp_op.size(); j++)
93  {
94  const std::size_t index = i * sub_width + j;
95  INVARIANT(index < op.size(), "bit index shall be within bounds");
96  tmp_op[j] = op[index];
97  }
98 
99  bvt tmp_result;
100  tmp_result.resize(sub_width);
101 
102  for(std::size_t j=0; j<tmp_result.size(); j++)
103  {
104  const std::size_t index = i * sub_width + j;
105  INVARIANT(index < bv.size(), "bit index shall be within bounds");
106  tmp_result[j] = bv[index];
107  }
108 
109  if(to_type_with_subtype(type).subtype().id() == ID_floatbv)
110  {
111  // needs to change due to rounding mode
112  float_utilst float_utils(
113  prop, to_floatbv_type(to_type_with_subtype(type).subtype()));
114  tmp_result=float_utils.add_sub(tmp_result, tmp_op, subtract);
115  }
116  else
117  tmp_result=bv_utils.add_sub(tmp_result, tmp_op, subtract);
118 
119  INVARIANT(
120  tmp_result.size() == sub_width,
121  "applying the add/sub operation shall not change the bitwidth");
122 
123  for(std::size_t j=0; j<tmp_result.size(); j++)
124  {
125  const std::size_t index = i * sub_width + j;
126  INVARIANT(index < bv.size(), "bit index shall be within bounds");
127  bv[index] = tmp_result[j];
128  }
129  }
130  }
131  else if(type.id()==ID_floatbv)
132  {
133  // needs to change due to rounding mode
134  float_utilst float_utils(prop, to_floatbv_type(arithmetic_type));
135  bv=float_utils.add_sub(bv, op, subtract);
136  }
137  else if(no_overflow)
138  bv=bv_utils.add_sub_no_overflow(bv, op, subtract, rep);
139  else
140  bv=bv_utils.add_sub(bv, op, subtract);
141  }
142 
143  return bv;
144 }
Pre-defined bitvector types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
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:40
virtual bvt convert_add_sub(const exprt &expr)
bv_utilst bv_utils
Definition: boolbv.h:114
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:84
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:99
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition: bv_utils.cpp:324
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition: bv_utils.cpp:335
representationt
Definition: bv_utils.h:28
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const std::string & id_string() const
Definition: irep.h:399
const irep_idt & id() const
Definition: irep.h:396
exprt & op0()
Definition: std_expr.h:844
const typet & subtype() const
Definition: type.h:156
The type of an expression, extends irept.
Definition: type.h:29
std::vector< literalt > bvt
Definition: literal.h:201
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177