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/invariant.h>
12 #include <util/std_types.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 =
57  (type.id() == ID_vector || type.id() == ID_complex) ? type.subtype() : type;
58 
60  (arithmetic_type.id()==ID_signedbv ||
61  arithmetic_type.id()==ID_fixedbv)?bv_utilst::representationt::SIGNED:
63 
64  for(exprt::operandst::const_iterator
65  it=operands.begin()+1;
66  it!=operands.end(); it++)
67  {
69  it->type() == type, "add/sub with mixed types:\n" + expr.pretty());
70 
71  const bvt &op = convert_bv(*it, width);
72 
73  if(type.id()==ID_vector || type.id()==ID_complex)
74  {
75  std::size_t sub_width = boolbv_width(type.subtype());
76 
77  INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
78  INVARIANT(
79  width % sub_width == 0,
80  "total vector bit width shall be a multiple of the element bit width");
81 
82  std::size_t size=width/sub_width;
83  bv.resize(width);
84 
85  for(std::size_t i=0; i<size; i++)
86  {
87  bvt tmp_op;
88  tmp_op.resize(sub_width);
89 
90  for(std::size_t j=0; j<tmp_op.size(); j++)
91  {
92  const std::size_t index = i * sub_width + j;
93  INVARIANT(index < op.size(), "bit index shall be within bounds");
94  tmp_op[j] = op[index];
95  }
96 
97  bvt tmp_result;
98  tmp_result.resize(sub_width);
99 
100  for(std::size_t j=0; j<tmp_result.size(); j++)
101  {
102  const std::size_t index = i * sub_width + j;
103  INVARIANT(index < bv.size(), "bit index shall be within bounds");
104  tmp_result[j] = bv[index];
105  }
106 
107  if(type.subtype().id()==ID_floatbv)
108  {
109  // needs to change due to rounding mode
110  float_utilst float_utils(prop, to_floatbv_type(type.subtype()));
111  tmp_result=float_utils.add_sub(tmp_result, tmp_op, subtract);
112  }
113  else
114  tmp_result=bv_utils.add_sub(tmp_result, tmp_op, subtract);
115 
116  INVARIANT(
117  tmp_result.size() == sub_width,
118  "applying the add/sub operation shall not change the bitwidth");
119 
120  for(std::size_t j=0; j<tmp_result.size(); j++)
121  {
122  const std::size_t index = i * sub_width + j;
123  INVARIANT(index < bv.size(), "bit index shall be within bounds");
124  bv[index] = tmp_result[j];
125  }
126  }
127  }
128  else if(type.id()==ID_floatbv)
129  {
130  // needs to change due to rounding mode
131  float_utilst float_utils(prop, to_floatbv_type(arithmetic_type));
132  bv=float_utils.add_sub(bv, op, subtract);
133  }
134  else if(no_overflow)
135  bv=bv_utils.add_sub_no_overflow(bv, op, subtract, rep);
136  else
137  bv=bv_utils.add_sub(bv, op, subtract);
138  }
139 
140  return bv;
141 }
typet::subtype
const typet & subtype() const
Definition: type.h:47
float_utilst::add_sub
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
Definition: float_utils.cpp:243
float_utilst
Definition: float_utils.h:18
typet
The type of an expression, extends irept.
Definition: type.h:29
float_utils.h
bvt
std::vector< literalt > bvt
Definition: literal.h:201
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
bv_utilst::representationt::UNSIGNED
@ UNSIGNED
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
boolbvt::convert_add_sub
virtual bvt convert_add_sub(const exprt &expr)
Definition: boolbv_add_sub.cpp:16
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
bv_utilst::representationt
representationt
Definition: bv_utils.h:31
std_types.h
Pre-defined types.
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
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
bv_utilst::add_sub
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition: bv_utils.cpp:339
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:95
bv_utilst::add_sub_no_overflow
bvt add_sub_no_overflow(const bvt &op0, const bvt &op1, bool subtract, representationt rep)
Definition: bv_utils.cpp:328
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:866
validation_modet::INVARIANT
@ INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131