cprover
boolbv_add_sub.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
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");
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