cprover
refine_arithmetic.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 "bv_refinement.h"
10 
11 #include <util/bv_arithmetic.h>
12 #include <util/ieee_float.h>
13 #include <util/expr_util.h>
14 #include <util/arith_tools.h>
15 
16 #include <langapi/language_util.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(l);
30 }
31 
33 {
34  // if it's a constant already, give up
35  if(!l.is_constant())
36  under_assumptions.push_back(l);
37 }
38 
40 {
42  return SUB::convert_floatbv_op(expr);
43 
44  if(ns.follow(expr.type()).id()!=ID_floatbv ||
45  expr.operands().size()!=3)
46  return SUB::convert_floatbv_op(expr);
47 
48  bvt bv;
49  add_approximation(expr, bv);
50  return bv;
51 }
52 
54 {
55  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
56  return SUB::convert_mult(expr);
57 
58  // we catch any multiplication
59  // unless it involves a constant
60 
61  const exprt::operandst &operands=expr.operands();
62 
63  const typet &type=ns.follow(expr.type());
64 
65  PRECONDITION(operands.size()>=2);
66 
67  if(operands.size()>2)
68  return convert_mult(make_binary(expr)); // make binary
69 
70  // we keep multiplication by a constant for integers
71  if(type.id()!=ID_floatbv)
72  if(operands[0].is_constant() || operands[1].is_constant())
73  return SUB::convert_mult(expr);
74 
75  bvt bv;
76  approximationt &a=add_approximation(expr, bv);
77 
78  // initially, we have a partial interpretation for integers
79  if(type.id()==ID_signedbv ||
80  type.id()==ID_unsignedbv)
81  {
82  // x*0==0 and 0*x==0
83  literalt op0_zero=bv_utils.is_zero(a.op0_bv);
84  literalt op1_zero=bv_utils.is_zero(a.op1_bv);
85  literalt res_zero=bv_utils.is_zero(a.result_bv);
87  prop.limplies(prop.lor(op0_zero, op1_zero), res_zero));
88 
89  // x*1==x and 1*x==x
90  literalt op0_one=bv_utils.is_one(a.op0_bv);
91  literalt op1_one=bv_utils.is_one(a.op1_bv);
92  literalt res_op0=bv_utils.equal(a.op0_bv, a.result_bv);
93  literalt res_op1=bv_utils.equal(a.op1_bv, a.result_bv);
94  prop.l_set_to_true(prop.limplies(op0_one, res_op1));
95  prop.l_set_to_true(prop.limplies(op1_one, res_op0));
96  }
97 
98  return bv;
99 }
100 
102 {
103  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
104  return SUB::convert_div(expr);
105 
106  // we catch any division
107  // unless it's integer division by a constant
108 
109  PRECONDITION(expr.operands().size()==2);
110 
111  if(expr.op1().is_constant())
112  return SUB::convert_div(expr);
113 
114  bvt bv;
115  add_approximation(expr, bv);
116  return bv;
117 }
118 
120 {
121  if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
122  return SUB::convert_mod(expr);
123 
124  // we catch any mod
125  // unless it's integer + constant
126 
127  PRECONDITION(expr.operands().size()==2);
128 
129  if(expr.op1().is_constant())
130  return SUB::convert_mod(expr);
131 
132  bvt bv;
133  add_approximation(expr, bv);
134  return bv;
135 }
136 
138 {
139  std::size_t o=a.expr.operands().size();
140 
141  if(o==1)
143  else if(o==2)
144  {
147  }
148  else if(o==3)
149  {
153  }
154  else
155  UNREACHABLE;
156 
158 }
159 
163 {
164  // get values
165  get_values(a);
166 
167  // see if the satisfying assignment is spurious in any way
168 
169  const typet &type=ns.follow(a.expr.type());
170 
171  if(type.id()==ID_floatbv)
172  {
173  // these are all ternary
174  INVARIANT(
175  a.expr.operands().size()==3,
176  string_refinement_invariantt("all floatbv typed exprs are ternary"));
177 
178  if(a.over_state==MAX_STATE)
179  return;
180 
181  ieee_float_spect spec(to_floatbv_type(type));
182  ieee_floatt o0(spec), o1(spec);
183 
184  o0.unpack(a.op0_value);
185  o1.unpack(a.op1_value);
186 
187  // get actual rounding mode
188  mp_integer rounding_mode_int;
189  exprt rounding_mode_expr = get(a.expr.op2());
190  to_integer(rounding_mode_expr, rounding_mode_int);
191  ieee_floatt::rounding_modet rounding_mode =
192  (ieee_floatt::rounding_modet)integer2ulong(rounding_mode_int);
193 
194  ieee_floatt result=o0;
195  o0.rounding_mode=rounding_mode;
196  o1.rounding_mode=rounding_mode;
197  result.rounding_mode=rounding_mode;
198 
199  if(a.expr.id()==ID_floatbv_plus)
200  result+=o1;
201  else if(a.expr.id()==ID_floatbv_minus)
202  result-=o1;
203  else if(a.expr.id()==ID_floatbv_mult)
204  result*=o1;
205  else if(a.expr.id()==ID_floatbv_div)
206  result/=o1;
207  else
208  UNREACHABLE;
209 
210  if(result.pack()==a.result_value) // ok
211  return;
212 
213  #ifdef DEBUG
214  ieee_floatt rr(spec);
215  rr.unpack(a.result_value);
216 
217  debug() << "S1: " << o0 << " " << a.expr.id() << " " << o1
218  << " != " << rr << eom;
219  debug() << "S2: " << integer2binary(a.op0_value, spec.width())
220  << " " << a.expr.id() << " " <<
221  integer2binary(a.op1_value, spec.width())
222  << "!=" << integer2binary(a.result_value, spec.width()) << eom;
223  debug() << "S3: " << integer2binary(a.op0_value, spec.width())
224  << " " << a.expr.id() << " " <<
225  integer2binary(a.op1_value, spec.width())
226  << "==" << integer2binary(result.pack(), spec.width()) << eom;
227  #endif
228 
230  {
231  bvt r;
232  float_utilst float_utils(prop);
233  float_utils.spec=spec;
234  float_utils.rounding_mode_bits.set(rounding_mode);
235 
236  literalt op0_equal=
237  bv_utils.equal(a.op0_bv, float_utils.build_constant(o0));
238 
239  literalt op1_equal=
240  bv_utils.equal(a.op1_bv, float_utils.build_constant(o1));
241 
242  literalt result_equal=
243  bv_utils.equal(a.result_bv, float_utils.build_constant(result));
244 
245  literalt op0_and_op1_equal=
246  prop.land(op0_equal, op1_equal);
247 
249  prop.limplies(op0_and_op1_equal, result_equal));
250  }
251  else
252  {
253  // give up
254  // remove any previous over-approximation
255  a.over_assumptions.clear();
257 
258  bvt r;
259  float_utilst float_utils(prop);
260  float_utils.spec=spec;
261  float_utils.rounding_mode_bits.set(rounding_mode);
262 
263  bvt op0=a.op0_bv, op1=a.op1_bv, res=a.result_bv;
264 
265  if(a.expr.id()==ID_floatbv_plus)
266  r=float_utils.add(op0, op1);
267  else if(a.expr.id()==ID_floatbv_minus)
268  r=float_utils.sub(op0, op1);
269  else if(a.expr.id()==ID_floatbv_mult)
270  r=float_utils.mul(op0, op1);
271  else if(a.expr.id()==ID_floatbv_div)
272  r=float_utils.div(op0, op1);
273  else
274  UNREACHABLE;
275 
276  CHECK_RETURN(r.size()==res.size());
277  bv_utils.set_equal(r, res);
278  }
279  }
280  else if(type.id()==ID_signedbv ||
281  type.id()==ID_unsignedbv)
282  {
283  // these are all binary
284  INVARIANT(
285  a.expr.operands().size()==2,
286  string_refinement_invariantt("all (un)signedbv typed exprs are binary"));
287 
288  // already full interpretation?
289  if(a.over_state>0)
290  return;
291 
292  bv_spect spec(type);
293  bv_arithmetict o0(spec), o1(spec);
294  o0.unpack(a.op0_value);
295  o1.unpack(a.op1_value);
296 
297  // division by zero is never spurious
298 
299  if((a.expr.id()==ID_div || a.expr.id()==ID_mod) &&
300  o1==0)
301  return;
302 
303  if(a.expr.id()==ID_mult)
304  o0*=o1;
305  else if(a.expr.id()==ID_div)
306  o0/=o1;
307  else if(a.expr.id()==ID_mod)
308  o0%=o1;
309  else
310  UNREACHABLE;
311 
312  if(o0.pack()==a.result_value) // ok
313  return;
314 
315  if(a.over_state==0)
316  {
317  // we give up right away and add the full interpretation
318  bvt r;
319  if(a.expr.id()==ID_mult)
320  {
322  a.op0_bv, a.op1_bv,
323  a.expr.type().id()==ID_signedbv?
326  }
327  else if(a.expr.id()==ID_div)
328  {
330  a.op0_bv, a.op1_bv,
331  a.expr.type().id()==ID_signedbv?
334  }
335  else if(a.expr.id()==ID_mod)
336  {
338  a.op0_bv, a.op1_bv,
339  a.expr.type().id()==ID_signedbv?
342  }
343  else
344  UNREACHABLE;
345 
347  }
348  else
349  UNREACHABLE;
350  }
351  else if(type.id()==ID_fixedbv)
352  {
353  // TODO: not implemented
354  TODO;
355  }
356  else
357  {
358  UNREACHABLE;
359  }
360 
361  status() << "Found spurious `" << a.as_string()
362  << "' (state " << a.over_state << ")" << eom;
363 
364  progress=true;
365  if(a.over_state<MAX_STATE)
366  a.over_state++;
367 }
368 
372 {
373  // part of the conflict?
374  if(!this->conflicts_with(a))
375  return;
376 
377  status() << "Found assumption for `" << a.as_string()
378  << "' in proof (state " << a.under_state << ")" << eom;
379 
380  PRECONDITION(!a.under_assumptions.empty());
381 
382  a.under_assumptions.clear();
383 
384  if(a.expr.type().id()==ID_floatbv)
385  {
386  const floatbv_typet &floatbv_type=to_floatbv_type(a.expr.type());
387  ieee_float_spect spec(floatbv_type);
388 
389  a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
390 
391  float_utilst float_utils(prop);
392  float_utils.spec=spec;
393 
394  // the fraction without hidden bit
395  const bvt fraction0=float_utils.get_fraction(a.op0_bv);
396  const bvt fraction1=float_utils.get_fraction(a.op1_bv);
397 
398  if(a.under_state==0)
399  {
400  // we first set sign and exponent free,
401  // but keep the fraction zero
402 
403  for(std::size_t i=0; i<fraction0.size(); i++)
404  a.add_under_assumption(!fraction0[i]);
405 
406  for(std::size_t i=0; i<fraction1.size(); i++)
407  a.add_under_assumption(!fraction1[i]);
408  }
409  else
410  {
411  // now fraction: make this grow quadratically
412  unsigned x=a.under_state*a.under_state;
413 
414  if(x>=MAX_FLOAT_UNDERAPPROX && x>=a.result_bv.size())
415  {
416  // make it free altogether, this guarantees progress
417  }
418  else
419  {
420  // set x bits of both exponent and mantissa free
421  // need to start with most-significant bits
422 
423  #if 0
424  for(std::size_t i=x; i<fraction0.size(); i++)
425  a.add_under_assumption(!fraction0[fraction0.size()-i-1]);
426 
427  for(std::size_t i=x; i<fraction1.size(); i++)
428  a.add_under_assumption(!fraction1[fraction1.size()-i-1]);
429  #endif
430  }
431  }
432  }
433  else
434  {
435  unsigned x=a.under_state+1;
436 
437  if(x>=MAX_INTEGER_UNDERAPPROX && x>=a.result_bv.size())
438  {
439  // make it free altogether, this guarantees progress
440  }
441  else
442  {
443  // set x least-significant bits free
444  a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
445 
446  for(std::size_t i=x; i<a.op0_bv.size(); i++)
447  a.add_under_assumption(!a.op0_bv[i]);
448 
449  for(std::size_t i=x; i<a.op1_bv.size(); i++)
450  a.add_under_assumption(!a.op1_bv[i]);
451  }
452  }
453 
454  a.under_state++;
455  progress=true;
456 }
457 
460 {
461  for(std::size_t i=0; i<a.under_assumptions.size(); i++)
463  return true;
464 
465  return false;
466 }
467 
469 {
470  a.over_state=a.under_state=0;
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++)
477  a.add_under_assumption(!a.op0_bv[i]);
478 
479  for(std::size_t i=0; i<a.op1_bv.size(); i++)
480  a.add_under_assumption(!a.op1_bv[i]);
481 }
482 
485  const exprt &expr, bvt &bv)
486 {
487  approximations.push_back(approximationt(approximations.size()));
488  approximationt &a=approximations.back();
489 
490  std::size_t width=boolbv_width(expr.type());
491  PRECONDITION(width!=0);
492 
493  a.expr=expr;
494  a.result_bv=prop.new_variables(width);
495  a.no_operands=expr.operands().size();
497 
498  if(a.no_operands==1)
499  {
500  a.op0_bv=convert_bv(expr.op0());
501  set_frozen(a.op0_bv);
502  }
503  else if(a.no_operands==2)
504  {
505  a.op0_bv=convert_bv(expr.op0());
506  a.op1_bv=convert_bv(expr.op1());
507  set_frozen(a.op0_bv);
508  set_frozen(a.op1_bv);
509  }
510  else if(a.no_operands==3)
511  {
512  a.op0_bv=convert_bv(expr.op0());
513  a.op1_bv=convert_bv(expr.op1());
514  a.op2_bv=convert_bv(expr.op2());
515  set_frozen(a.op0_bv);
516  set_frozen(a.op1_bv);
517  set_frozen(a.op2_bv);
518  }
519  else
520  UNREACHABLE;
521 
522  bv=a.result_bv;
523 
524  initialize(a);
525 
526  return a;
527 }
528 
530 {
531  #if 0
532  return from_expr(expr);
533  #else
534  return std::to_string(id_nr)+"/"+id2string(expr.id());
535  #endif
536 }
The type of an expression.
Definition: type.h:22
approximationt & add_approximation(const exprt &expr, bvt &bv)
bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:94
bv_utilst bv_utils
Definition: boolbv.h:93
static int8_t r
Definition: irep_hash.h:59
#define MAX_STATE
Definition: bv_refinement.h:19
BigInt mp_integer
Definition: mp_arith.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
exprt & op0()
Definition: expr.h:72
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1342
mstreamt & progress() const
Definition: message.h:327
mp_integer::ullong_t integer2ulong(const mp_integer &n)
Definition: mp_arith.cpp:189
Deprecated expression utility functions.
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:87
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1108
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:39
boolbv_widtht boolbv_width
Definition: boolbv.h:90
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::list< approximationt > approximations
virtual literalt lor(literalt a, literalt b)=0
typet & type()
Definition: expr.h:56
literalt is_zero(const bvt &op)
Definition: bv_utils.h:141
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void initialize(approximationt &approximation)
virtual literalt limplies(literalt a, literalt b)=0
bool conflicts_with(approximationt &approximation)
check if an under-approximation is part of the conflict
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
void l_set_to_true(literalt a)
Definition: prop.h:49
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:189
division (integer and real)
Definition: std_expr.h:1075
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:312
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
virtual bvt mul(const bvt &src1, const bvt &src2)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:810
exprt & op1()
Definition: expr.h:75
unsigned max_node_refinement
Max number of times we refine a formula node.
Definition: bv_refinement.h:28
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
bvt convert_mod(const mod_exprt &expr) override
const namespacet & ns
const typet & follow(const typet &) const
Definition: namespace.cpp:55
virtual bvt div(const bvt &src1, const bvt &src2)
void set_equal(const bvt &a, const bvt &b)
Definition: bv_utils.cpp:35
bvt get_fraction(const bvt &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
bool is_constant() const
Definition: expr.cpp:119
std::vector< exprt > operandst
Definition: expr.h:45
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:78
bvt convert_floatbv_op(const exprt &expr) override
ieee_float_spect spec
Definition: float_utils.h:86
bvt convert_mult(const exprt &expr) override
void get_values(approximationt &approximation)
literalt is_one(const bvt &op)
Definition: bv_utils.cpp:26
mstreamt & result() const
Definition: message.h:312
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1373
mstreamt & status() const
Definition: message.h:317
bool is_constant() const
Definition: literal.h:165
bvt add(const bvt &src1, const bvt &src2)
Definition: float_utils.h:109
rounding_mode_bitst rounding_mode_bits
Definition: float_utils.h:65
Base class for all expressions.
Definition: expr.h:42
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define TODO
Definition: invariant.h:265
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
#define UNREACHABLE
Definition: invariant.h:250
#define string_refinement_invariantt(reason)
bool refine_arithmetic
Enable arithmetic refinement.
Definition: bv_refinement.h:32
void set_frozen(literalt a) override
Definition: prop_conv.h:90
#define MAX_FLOAT_UNDERAPPROX
void set(const ieee_floatt::rounding_modet mode)
Definition: float_utils.h:37
rounding_modet rounding_mode
Definition: ieee_float.h:132
exprt & op2()
Definition: expr.h:78
Abstraction Refinement Loop.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
std::size_t width() const
Definition: ieee_float.h:54
mstreamt & debug() const
Definition: message.h:332
bvt sub(const bvt &src1, const bvt &src2)
Definition: float_utils.h:114
virtual bool is_in_conflict(literalt l) const
Definition: prop.cpp:31
operandst & operands()
Definition: expr.h:66
bvt convert_div(const div_exprt &expr) override
#define MAX_INTEGER_UNDERAPPROX
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:22
std::vector< literalt > bvt
Definition: literal.h:200
void unpack(const mp_integer &i)
binary modulo
Definition: std_expr.h:1133
bvt build_constant(const ieee_floatt &)