cprover
Loading...
Searching...
No Matches
refine_arithmetic.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "bv_refinement.h"
10
11#include <util/arith_tools.h>
13#include <util/bv_arithmetic.h>
14#include <util/expr_util.h>
15#include <util/floatbv_expr.h>
16#include <util/ieee_float.h>
17
20
21// Parameters
22#define MAX_INTEGER_UNDERAPPROX 3
23#define MAX_FLOAT_UNDERAPPROX 10
24
26{
27 // if it's a constant already, give up
28 if(!l.is_constant())
29 over_assumptions.push_back(literal_exprt(l));
30}
31
33{
34 // if it's a constant already, give up
35 if(!l.is_constant())
36 under_assumptions.push_back(literal_exprt(l));
37}
38
40{
42 return SUB::convert_floatbv_op(expr);
43
44 if(expr.type().id() != ID_floatbv)
45 return SUB::convert_floatbv_op(expr);
46
47 bvt bv;
48 add_approximation(expr, bv);
49 return bv;
50}
51
53{
54 if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
55 return SUB::convert_mult(expr);
56
57 // we catch any multiplication
58 // unless it involves a constant
59
60 const exprt::operandst &operands=expr.operands();
61
62 const typet &type = expr.type();
63
64 PRECONDITION(operands.size()>=2);
65
66 if(operands.size()>2)
67 return convert_mult(to_mult_expr(make_binary(expr))); // make binary
68
69 // we keep multiplication by a constant for integers
70 if(type.id()!=ID_floatbv)
71 if(operands[0].is_constant() || operands[1].is_constant())
72 return SUB::convert_mult(expr);
73
74 bvt bv;
76
77 // initially, we have a partial interpretation for integers
78 if(type.id()==ID_signedbv ||
79 type.id()==ID_unsignedbv)
80 {
81 // x*0==0 and 0*x==0
82 literalt op0_zero=bv_utils.is_zero(a.op0_bv);
83 literalt op1_zero=bv_utils.is_zero(a.op1_bv);
86 prop.limplies(prop.lor(op0_zero, op1_zero), res_zero));
87
88 // x*1==x and 1*x==x
89 literalt op0_one=bv_utils.is_one(a.op0_bv);
90 literalt op1_one=bv_utils.is_one(a.op1_bv);
93 prop.l_set_to_true(prop.limplies(op0_one, res_op1));
94 prop.l_set_to_true(prop.limplies(op1_one, res_op0));
95 }
96
97 return bv;
98}
99
101{
102 if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
103 return SUB::convert_div(expr);
104
105 // we catch any division
106 // unless it's integer division by a constant
107
108 PRECONDITION(expr.operands().size()==2);
109
110 if(expr.op1().is_constant())
111 return SUB::convert_div(expr);
112
113 bvt bv;
114 add_approximation(expr, bv);
115 return bv;
116}
117
119{
120 if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
121 return SUB::convert_mod(expr);
122
123 // we catch any mod
124 // unless it's integer + constant
125
126 PRECONDITION(expr.operands().size()==2);
127
128 if(expr.op1().is_constant())
129 return SUB::convert_mod(expr);
130
131 bvt bv;
132 add_approximation(expr, bv);
133 return bv;
134}
135
137{
138 std::size_t o=a.expr.operands().size();
139
140 if(o==1)
142 else if(o==2)
143 {
146 }
147 else if(o==3)
148 {
152 }
153 else
155
157}
158
162{
163 // see if the satisfying assignment is spurious in any way
164
165 const typet &type = a.expr.type();
166
167 if(type.id()==ID_floatbv)
168 {
169 const auto &float_op = to_ieee_float_op_expr(a.expr);
170
171 if(a.over_state==MAX_STATE)
172 return;
173
175 ieee_floatt o0(spec), o1(spec);
176
177 o0.unpack(a.op0_value);
178 o1.unpack(a.op1_value);
179
180 // get actual rounding mode
181 constant_exprt rounding_mode_expr =
182 to_constant_expr(get(float_op.rounding_mode()));
183 const std::size_t rounding_mode_int =
184 numeric_cast_v<std::size_t>(rounding_mode_expr);
185 ieee_floatt::rounding_modet rounding_mode =
186 (ieee_floatt::rounding_modet)rounding_mode_int;
187
188 ieee_floatt result=o0;
189 o0.rounding_mode=rounding_mode;
190 o1.rounding_mode=rounding_mode;
191 result.rounding_mode=rounding_mode;
192
193 if(a.expr.id()==ID_floatbv_plus)
194 result+=o1;
195 else if(a.expr.id()==ID_floatbv_minus)
196 result-=o1;
197 else if(a.expr.id()==ID_floatbv_mult)
198 result*=o1;
199 else if(a.expr.id()==ID_floatbv_div)
200 result/=o1;
201 else
203
204 if(result.pack()==a.result_value) // ok
205 return;
206
207#ifdef DEBUG
208 ieee_floatt rr(spec);
209 rr.unpack(a.result_value);
210
211 log.debug() << "S1: " << o0 << " " << a.expr.id() << " " << o1
212 << " != " << rr << messaget::eom;
213 log.debug() << "S2: " << integer2binary(a.op0_value, spec.width()) << " "
214 << a.expr.id() << " "
215 << integer2binary(a.op1_value, spec.width())
216 << "!=" << integer2binary(a.result_value, spec.width())
217 << messaget::eom;
218 log.debug() << "S3: " << integer2binary(a.op0_value, spec.width()) << " "
219 << a.expr.id() << " "
220 << integer2binary(a.op1_value, spec.width())
221 << "==" << integer2binary(result.pack(), spec.width())
222 << messaget::eom;
223#endif
224
226 {
227 bvt r;
228 float_utilst float_utils(prop);
229 float_utils.spec=spec;
230 float_utils.rounding_mode_bits.set(rounding_mode);
231
232 literalt op0_equal=
233 bv_utils.equal(a.op0_bv, float_utils.build_constant(o0));
234
235 literalt op1_equal=
236 bv_utils.equal(a.op1_bv, float_utils.build_constant(o1));
237
238 literalt result_equal=
239 bv_utils.equal(a.result_bv, float_utils.build_constant(result));
240
241 literalt op0_and_op1_equal=
242 prop.land(op0_equal, op1_equal);
243
245 prop.limplies(op0_and_op1_equal, result_equal));
246 }
247 else
248 {
249 // give up
250 // remove any previous over-approximation
251 a.over_assumptions.clear();
253
254 bvt r;
255 float_utilst float_utils(prop);
256 float_utils.spec=spec;
257 float_utils.rounding_mode_bits.set(rounding_mode);
258
259 bvt op0=a.op0_bv, op1=a.op1_bv, res=a.result_bv;
260
261 if(a.expr.id()==ID_floatbv_plus)
262 r=float_utils.add(op0, op1);
263 else if(a.expr.id()==ID_floatbv_minus)
264 r=float_utils.sub(op0, op1);
265 else if(a.expr.id()==ID_floatbv_mult)
266 r=float_utils.mul(op0, op1);
267 else if(a.expr.id()==ID_floatbv_div)
268 r=float_utils.div(op0, op1);
269 else
271
272 CHECK_RETURN(r.size()==res.size());
273 bv_utils.set_equal(r, res);
274 }
275 }
276 else if(type.id()==ID_signedbv ||
277 type.id()==ID_unsignedbv)
278 {
279 // these are all binary
280 INVARIANT(
281 a.expr.operands().size() == 2, "all (un)signedbv typed exprs are binary");
282
283 // already full interpretation?
284 if(a.over_state>0)
285 return;
286
287 bv_spect spec(type);
288 bv_arithmetict o0(spec), o1(spec);
289 o0.unpack(a.op0_value);
290 o1.unpack(a.op1_value);
291
292 // division by zero is never spurious
293
294 if((a.expr.id()==ID_div || a.expr.id()==ID_mod) &&
295 o1==0)
296 return;
297
298 if(a.expr.id()==ID_mult)
299 o0*=o1;
300 else if(a.expr.id()==ID_div)
301 o0/=o1;
302 else if(a.expr.id()==ID_mod)
303 o0%=o1;
304 else
306
307 if(o0.pack()==a.result_value) // ok
308 return;
309
310 if(a.over_state==0)
311 {
312 // we give up right away and add the full interpretation
313 bvt r;
314 if(a.expr.id()==ID_mult)
315 {
317 a.op0_bv, a.op1_bv,
318 a.expr.type().id()==ID_signedbv?
321 }
322 else if(a.expr.id()==ID_div)
323 {
325 a.op0_bv, a.op1_bv,
326 a.expr.type().id()==ID_signedbv?
329 }
330 else if(a.expr.id()==ID_mod)
331 {
333 a.op0_bv, a.op1_bv,
334 a.expr.type().id()==ID_signedbv?
337 }
338 else
340
342 }
343 else
345 }
346 else if(type.id()==ID_fixedbv)
347 {
348 // TODO: not implemented
349 TODO;
350 }
351 else
352 {
354 }
355
356 log.status() << "Found spurious '" << a.as_string() << "' (state "
357 << a.over_state << ")" << messaget::eom;
358
359 progress=true;
361 a.over_state++;
362}
363
367{
368 // part of the conflict?
369 if(!this->conflicts_with(a))
370 return;
371
372 log.status() << "Found assumption for '" << a.as_string()
373 << "' in proof (state " << a.under_state << ")" << messaget::eom;
374
376
377 a.under_assumptions.clear();
378
379 if(a.expr.type().id()==ID_floatbv)
380 {
381 const floatbv_typet &floatbv_type=to_floatbv_type(a.expr.type());
382 ieee_float_spect spec(floatbv_type);
383
384 a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
385
386 float_utilst float_utils(prop);
387 float_utils.spec=spec;
388
389 // the fraction without hidden bit
390 const bvt fraction0=float_utils.get_fraction(a.op0_bv);
391 const bvt fraction1=float_utils.get_fraction(a.op1_bv);
392
393 if(a.under_state==0)
394 {
395 // we first set sign and exponent free,
396 // but keep the fraction zero
397
398 for(std::size_t i=0; i<fraction0.size(); i++)
399 a.add_under_assumption(!fraction0[i]);
400
401 for(std::size_t i=0; i<fraction1.size(); i++)
402 a.add_under_assumption(!fraction1[i]);
403 }
404 else
405 {
406 // now fraction: make this grow quadratically
407 unsigned x=a.under_state*a.under_state;
408
409 if(x>=MAX_FLOAT_UNDERAPPROX && x>=a.result_bv.size())
410 {
411 // make it free altogether, this guarantees progress
412 }
413 else
414 {
415 // set x bits of both exponent and mantissa free
416 // need to start with most-significant bits
417
418 #if 0
419 for(std::size_t i=x; i<fraction0.size(); i++)
420 a.add_under_assumption(!fraction0[fraction0.size()-i-1]);
421
422 for(std::size_t i=x; i<fraction1.size(); i++)
423 a.add_under_assumption(!fraction1[fraction1.size()-i-1]);
424 #endif
425 }
426 }
427 }
428 else
429 {
430 unsigned x=a.under_state+1;
431
432 if(x>=MAX_INTEGER_UNDERAPPROX && x>=a.result_bv.size())
433 {
434 // make it free altogether, this guarantees progress
435 }
436 else
437 {
438 // set x least-significant bits free
439 a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
440
441 for(std::size_t i=x; i<a.op0_bv.size(); i++)
443
444 for(std::size_t i=x; i<a.op1_bv.size(); i++)
446 }
447 }
448
449 a.under_state++;
450 progress=true;
451}
452
455{
456 for(std::size_t i=0; i<a.under_assumptions.size(); i++)
457 {
460 {
461 return true;
462 }
463 }
464
465 return false;
466}
467
469{
471
472 a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
473
474 // initially, we force the operands to be all zero
475
476 for(std::size_t i=0; i<a.op0_bv.size(); i++)
478
479 for(std::size_t i=0; i<a.op1_bv.size(); i++)
481}
482
485 const exprt &expr, bvt &bv)
486{
489
490 std::size_t width=boolbv_width(expr.type());
491 PRECONDITION(width!=0);
492
493 a.expr=expr;
495 a.no_operands=expr.operands().size();
497
498 if(a.no_operands==1)
499 {
500 a.op0_bv = convert_bv(to_unary_expr(expr).op());
502 }
503 else if(a.no_operands==2)
504 {
505 a.op0_bv = convert_bv(to_binary_expr(expr).op0());
506 a.op1_bv = convert_bv(to_binary_expr(expr).op1());
509 }
510 else if(a.no_operands==3)
511 {
512 a.op0_bv = convert_bv(to_multi_ary_expr(expr).op0());
513 a.op1_bv = convert_bv(to_multi_ary_expr(expr).op1());
514 a.op2_bv = convert_bv(to_multi_ary_expr(expr).op2());
518 }
519 else
521
522 bv=a.result_bv;
523
524 initialize(a);
525
526 return a;
527}
528
530{
531 return std::to_string(id_nr)+"/"+id2string(expr.id());
532}
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
Pre-defined bitvector types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Abstraction Refinement Loop.
#define MAX_STATE
messaget log
Definition arrays.h:57
exprt & op1()
Definition expr.h:136
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:39
virtual bvt convert_mod(const mod_exprt &expr)
virtual bvt convert_mult(const mult_exprt &expr)
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
virtual bvt convert_div(const div_exprt &expr)
bv_utilst bv_utils
Definition boolbv.h:117
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:102
mp_integer get_value(const bvt &bv)
Definition boolbv.h:90
void unpack(const mp_integer &i)
bvt convert_mult(const mult_exprt &expr) override
bvt convert_div(const div_exprt &expr) override
bool conflicts_with(approximationt &approximation)
check if an under-approximation is part of the conflict
approximationt & add_approximation(const exprt &expr, bvt &bv)
void get_values(approximationt &approximation)
bvt convert_mod(const mod_exprt &expr) override
bvt convert_floatbv_op(const ieee_float_op_exprt &) override
void initialize(approximationt &approximation)
std::list< approximationt > approximations
void set_equal(const bvt &a, const bvt &b)
Definition bv_utils.cpp:34
literalt is_zero(const bvt &op)
Definition bv_utils.h:143
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
literalt is_one(const bvt &op)
Definition bv_utils.cpp:25
bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:96
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition bv_utils.h:89
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
A constant literal expression.
Definition std_expr.h:2995
Division.
Definition std_expr.h:1157
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
bvt build_constant(const ieee_floatt &)
virtual bvt mul(const bvt &src1, const bvt &src2)
bvt get_fraction(const bvt &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
virtual bvt div(const bvt &src1, const bvt &src2)
bvt add(const bvt &src1, const bvt &src2)
bvt sub(const bvt &src1, const bvt &src2)
ieee_float_spect spec
Definition float_utils.h:88
rounding_mode_bitst rounding_mode_bits
Definition float_utils.h:67
Fixed-width bit-vector with IEEE floating-point interpretation.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
std::size_t width() const
Definition ieee_float.h:50
void unpack(const mp_integer &i)
rounding_modet rounding_mode
Definition ieee_float.h:132
mp_integer pack() const
const irep_idt & id() const
Definition irep.h:388
literalt get_literal() const
bool is_constant() const
Definition literal.h:166
mstreamt & debug() const
Definition message.h:421
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1228
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
void set_frozen(literalt)
void l_set_to_true(literalt a)
Definition prop.h:52
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition prop.cpp:30
virtual literalt lor(literalt a, literalt b)=0
virtual bool is_in_conflict(literalt l) const =0
Returns true if an assumption is in the final conflict.
The type of an expression, extends irept.
Definition type.h:29
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition expr_util.cpp:38
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
static int8_t r
Definition irep_hash.h:60
std::vector< literalt > bvt
Definition literal.h:201
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition mp_arith.cpp:64
#define MAX_INTEGER_UNDERAPPROX
#define MAX_FLOAT_UNDERAPPROX
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define TODO
Definition invariant.h:557
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1137
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:987
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3050
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:29
std::vector< exprt > over_assumptions
std::vector< exprt > under_assumptions
unsigned max_node_refinement
Max number of times we refine a formula node.
bool refine_arithmetic
Enable arithmetic refinement.
void set(const ieee_floatt::rounding_modet mode)
Definition float_utils.h:37