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=ns.follow(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=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)?
58  ns.follow(type.subtype()):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 = boolbv_width(type.subtype());
77 
78  INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
79  INVARIANT(
80  width % sub_width == 0,
81  "total vector bit width shall be a multiple of the element bit width");
82 
83  std::size_t size=width/sub_width;
84  bv.resize(width);
85 
86  for(std::size_t i=0; i<size; i++)
87  {
88  bvt tmp_op;
89  tmp_op.resize(sub_width);
90 
91  for(std::size_t j=0; j<tmp_op.size(); j++)
92  {
93  const std::size_t index = i * sub_width + j;
94  INVARIANT(index < op.size(), "bit index shall be within bounds");
95  tmp_op[j] = op[index];
96  }
97 
98  bvt tmp_result;
99  tmp_result.resize(sub_width);
100 
101  for(std::size_t j=0; j<tmp_result.size(); j++)
102  {
103  const std::size_t index = i * sub_width + j;
104  INVARIANT(index < bv.size(), "bit index shall be within bounds");
105  tmp_result[j] = bv[index];
106  }
107 
108  if(type.subtype().id()==ID_floatbv)
109  {
110  // needs to change due to rounding mode
111  float_utilst float_utils(prop, to_floatbv_type(type.subtype()));
112  tmp_result=float_utils.add_sub(tmp_result, tmp_op, subtract);
113  }
114  else
115  tmp_result=bv_utils.add_sub(tmp_result, tmp_op, subtract);
116 
117  INVARIANT(
118  tmp_result.size() == sub_width,
119  "applying the add/sub operation shall not change the bitwidth");
120 
121  for(std::size_t j=0; j<tmp_result.size(); j++)
122  {
123  const std::size_t index = i * sub_width + j;
124  INVARIANT(index < bv.size(), "bit index shall be within bounds");
125  bv[index] = tmp_result[j];
126  }
127  }
128  }
129  else if(type.id()==ID_floatbv)
130  {
131  // needs to change due to rounding mode
132  float_utilst float_utils(prop, to_floatbv_type(arithmetic_type));
133  bv=float_utils.add_sub(bv, op, subtract);
134  }
135  else if(no_overflow)
136  bv=bv_utils.add_sub_no_overflow(bv, op, subtract, rep);
137  else
138  bv=bv_utils.add_sub(bv, op, subtract);
139  }
140 
141  return bv;
142 }
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
float_utilst::add_sub
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
Definition: float_utils.cpp:243
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
float_utilst
Definition: float_utils.h:17
typet
The type of an expression, extends irept.
Definition: type.h:27
float_utils.h
bvt
std::vector< literalt > bvt
Definition: literal.h:200
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
bv_utilst::representationt::UNSIGNED
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:84
invariant.h
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:68
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:92
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
bv_utilst::representationt::SIGNED
bv_utilst::representationt
representationt
Definition: bv_utils.h:31
std_types.h
irept::id_string
const std::string & id_string() const
Definition: irep.h:262
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
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
bv_utilst::add_sub
bvt add_sub(const bvt &op0, const bvt &op1, bool subtract)
Definition: bv_utils.cpp:339
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:95
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:78
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
validation_modet::INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152