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 
19 
20 // Parameters
21 #define MAX_INTEGER_UNDERAPPROX 3
22 #define MAX_FLOAT_UNDERAPPROX 10
23 
25 {
26  // if it's a constant already, give up
27  if(!l.is_constant())
28  over_assumptions.push_back(l);
29 }
30 
32 {
33  // if it's a constant already, give up
34  if(!l.is_constant())
35  under_assumptions.push_back(l);
36 }
37 
39 {
41  return SUB::convert_floatbv_op(expr);
42 
43  if(ns.follow(expr.type()).id()!=ID_floatbv ||
44  expr.operands().size()!=3)
45  return SUB::convert_floatbv_op(expr);
46 
47  bvt bv;
48  add_approximation(expr, bv);
49  return bv;
50 }
51 
53 {
54  if(!do_arithmetic_refinement || 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=ns.follow(expr.type());
63 
64  assert(operands.size()>=2);
65 
66  if(operands.size()>2)
67  return convert_mult(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;
75  approximationt &a=add_approximation(expr, 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);
84  literalt res_zero=bv_utils.is_zero(a.result_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);
91  literalt res_op0=bv_utils.equal(a.op0_bv, a.result_bv);
92  literalt res_op1=bv_utils.equal(a.op1_bv, a.result_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(!do_arithmetic_refinement || 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  assert(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(!do_arithmetic_refinement || 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  assert(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
154  assert(0);
155 
157 }
158 
162 {
163  // get values
164  get_values(a);
165 
166  // see if the satisfying assignment is spurious in any way
167 
168  const typet &type=ns.follow(a.expr.type());
169 
170  if(type.id()==ID_floatbv)
171  {
172  // these are all trinary
173  assert(a.expr.operands().size()==3);
174 
175  if(a.over_state==MAX_STATE)
176  return;
177 
178  ieee_float_spect spec(to_floatbv_type(type));
179  ieee_floatt o0(spec), o1(spec);
180 
181  o0.unpack(a.op0_value);
182  o1.unpack(a.op1_value);
183 
184  // get actual rounding mode
185  mp_integer rounding_mode_int;
186  exprt rounding_mode_expr = get(a.expr.op2());
187  to_integer(rounding_mode_expr, rounding_mode_int);
188  ieee_floatt::rounding_modet rounding_mode =
189  (ieee_floatt::rounding_modet)integer2ulong(rounding_mode_int);
190 
191  ieee_floatt result=o0;
192  o0.rounding_mode=rounding_mode;
193  o1.rounding_mode=rounding_mode;
194  result.rounding_mode=rounding_mode;
195 
196  if(a.expr.id()==ID_floatbv_plus)
197  result+=o1;
198  else if(a.expr.id()==ID_floatbv_minus)
199  result-=o1;
200  else if(a.expr.id()==ID_floatbv_mult)
201  result*=o1;
202  else if(a.expr.id()==ID_floatbv_div)
203  result/=o1;
204  else
205  assert(false);
206 
207  if(result.pack()==a.result_value) // ok
208  return;
209 
210  #ifdef DEBUG
211  ieee_floatt rr(spec);
212  rr.unpack(a.result_value);
213 
214  debug() << "S1: " << o0 << " " << a.expr.id() << " " << o1
215  << " != " << rr << eom;
216  debug() << "S2: " << integer2binary(a.op0_value, spec.width())
217  << " " << a.expr.id() << " " <<
218  integer2binary(a.op1_value, spec.width())
219  << "!=" << integer2binary(a.result_value, spec.width()) << eom;
220  debug() << "S3: " << integer2binary(a.op0_value, spec.width())
221  << " " << a.expr.id() << " " <<
222  integer2binary(a.op1_value, spec.width())
223  << "==" << integer2binary(result.pack(), spec.width()) << eom;
224  #endif
225 
226  // if(a.over_state==1) { debug() << "DISAGREEMENT!\n"; exit(1); }
227 
229  {
230  bvt r;
231  float_utilst float_utils(prop);
232  float_utils.spec=spec;
233  float_utils.rounding_mode_bits.set(rounding_mode);
234 
235  literalt op0_equal=
236  bv_utils.equal(a.op0_bv, float_utils.build_constant(o0));
237 
238  literalt op1_equal=
239  bv_utils.equal(a.op1_bv, float_utils.build_constant(o1));
240 
241  literalt result_equal=
242  bv_utils.equal(a.result_bv, float_utils.build_constant(result));
243 
244  literalt op0_and_op1_equal=
245  prop.land(op0_equal, op1_equal);
246 
248  prop.limplies(op0_and_op1_equal, result_equal));
249  }
250  else
251  {
252  // give up
253  // remove any previous over-approximation
254  a.over_assumptions.clear();
256 
257  bvt r;
258  float_utilst float_utils(prop);
259  float_utils.spec=spec;
260  float_utils.rounding_mode_bits.set(rounding_mode);
261 
262  bvt op0=a.op0_bv, op1=a.op1_bv, res=a.result_bv;
263 
264  if(a.expr.id()==ID_floatbv_plus)
265  r=float_utils.add(op0, op1);
266  else if(a.expr.id()==ID_floatbv_minus)
267  r=float_utils.sub(op0, op1);
268  else if(a.expr.id()==ID_floatbv_mult)
269  r=float_utils.mul(op0, op1);
270  else if(a.expr.id()==ID_floatbv_div)
271  r=float_utils.div(op0, op1);
272  else
273  assert(0);
274 
275  assert(r.size()==res.size());
276  bv_utils.set_equal(r, res);
277  }
278  }
279  else if(type.id()==ID_signedbv ||
280  type.id()==ID_unsignedbv)
281  {
282  // these are all binary
283  assert(a.expr.operands().size()==2);
284 
285  // already full interpretation?
286  if(a.over_state>0)
287  return;
288 
289  bv_spect spec(type);
290  bv_arithmetict o0(spec), o1(spec);
291  o0.unpack(a.op0_value);
292  o1.unpack(a.op1_value);
293 
294  // division by zero is never spurious
295 
296  if((a.expr.id()==ID_div || a.expr.id()==ID_mod) &&
297  o1==0)
298  return;
299 
300  if(a.expr.id()==ID_mult)
301  o0*=o1;
302  else if(a.expr.id()==ID_div)
303  o0/=o1;
304  else if(a.expr.id()==ID_mod)
305  o0%=o1;
306  else
307  assert(false);
308 
309  if(o0.pack()==a.result_value) // ok
310  return;
311 
312  if(a.over_state==0)
313  {
314  // we give up right away and add the full interpretation
315  bvt r;
316  if(a.expr.id()==ID_mult)
317  {
319  a.op0_bv, a.op1_bv,
320  a.expr.type().id()==ID_signedbv?
323  }
324  else if(a.expr.id()==ID_div)
325  {
326  r=bv_utils.divider(
327  a.op0_bv, a.op1_bv,
328  a.expr.type().id()==ID_signedbv?
331  }
332  else if(a.expr.id()==ID_mod)
333  {
335  a.op0_bv, a.op1_bv,
336  a.expr.type().id()==ID_signedbv?
339  }
340  else
341  assert(0);
342 
344  }
345  else
346  assert(0);
347  }
348  else if(type.id()==ID_fixedbv)
349  {
350  // TODO: not implemented
351  assert(0);
352  }
353  else
354  {
355  assert(0);
356  }
357 
358  status() << "Found spurious `" << a.as_string()
359  << "' (state " << a.over_state << ")" << eom;
360 
361  progress=true;
362  if(a.over_state<MAX_STATE)
363  a.over_state++;
364 }
365 
369 {
370  // part of the conflict?
371  if(!is_in_conflict(a))
372  return;
373 
374  status() << "Found assumption for `" << a.as_string()
375  << "' in proof (state " << a.under_state << ")" << eom;
376 
377  assert(!a.under_assumptions.empty());
378 
379  a.under_assumptions.clear();
380 
381  if(a.expr.type().id()==ID_floatbv)
382  {
383  const floatbv_typet &floatbv_type=to_floatbv_type(a.expr.type());
384  ieee_float_spect spec(floatbv_type);
385 
386  a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
387 
388  float_utilst float_utils(prop);
389  float_utils.spec=spec;
390 
391  // the fraction without hidden bit
392  const bvt fraction0=float_utils.get_fraction(a.op0_bv);
393  const bvt fraction1=float_utils.get_fraction(a.op1_bv);
394 
395  if(a.under_state==0)
396  {
397  // we first set sign and exponent free,
398  // but keep the fraction zero
399 
400  for(std::size_t i=0; i<fraction0.size(); i++)
401  a.add_under_assumption(!fraction0[i]);
402 
403  for(std::size_t i=0; i<fraction1.size(); i++)
404  a.add_under_assumption(!fraction1[i]);
405  }
406  else
407  {
408  // now fraction: make this grow quadratically
409  unsigned x=a.under_state*a.under_state;
410 
411  if(x>=MAX_FLOAT_UNDERAPPROX && x>=a.result_bv.size())
412  {
413  // make it free altogether, this guarantees progress
414  }
415  else
416  {
417  // set x bits of both exponent and mantissa free
418  // need to start with most-significant bits
419 
420  #if 0
421  for(std::size_t i=x; i<fraction0.size(); i++)
422  a.add_under_assumption(!fraction0[fraction0.size()-i-1]);
423 
424  for(std::size_t i=x; i<fraction1.size(); i++)
425  a.add_under_assumption(!fraction1[fraction1.size()-i-1]);
426  #endif
427  }
428  }
429  }
430  else
431  {
432  unsigned x=a.under_state+1;
433 
434  if(x>=MAX_INTEGER_UNDERAPPROX && x>=a.result_bv.size())
435  {
436  // make it free altogether, this guarantees progress
437  }
438  else
439  {
440  // set x least-significant bits free
441  a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
442 
443  for(std::size_t i=x; i<a.op0_bv.size(); i++)
444  a.add_under_assumption(!a.op0_bv[i]);
445 
446  for(std::size_t i=x; i<a.op1_bv.size(); i++)
447  a.add_under_assumption(!a.op1_bv[i]);
448  }
449  }
450 
451  a.under_state++;
452  progress=true;
453 }
454 
457 {
458  for(std::size_t i=0; i<a.under_assumptions.size(); i++)
460  return true;
461 
462  return false;
463 }
464 
466 {
467  a.over_state=a.under_state=0;
468 
469  a.under_assumptions.reserve(a.op0_bv.size()+a.op1_bv.size());
470 
471  // initially, we force the operands to be all zero
472 
473  for(std::size_t i=0; i<a.op0_bv.size(); i++)
474  a.add_under_assumption(!a.op0_bv[i]);
475 
476  for(std::size_t i=0; i<a.op1_bv.size(); i++)
477  a.add_under_assumption(!a.op1_bv[i]);
478 }
479 
482  const exprt &expr, bvt &bv)
483 {
484  approximations.push_back(approximationt(approximations.size()));
485  approximationt &a=approximations.back(); // stable!
486 
487  std::size_t width=boolbv_width(expr.type());
488  assert(width!=0);
489 
490  a.expr=expr;
491  a.result_bv=prop.new_variables(width);
492  a.no_operands=expr.operands().size();
494 
495  if(a.no_operands==1)
496  {
497  a.op0_bv=convert_bv(expr.op0());
498  set_frozen(a.op0_bv);
499  }
500  else if(a.no_operands==2)
501  {
502  a.op0_bv=convert_bv(expr.op0());
503  a.op1_bv=convert_bv(expr.op1());
504  set_frozen(a.op0_bv);
505  set_frozen(a.op1_bv);
506  }
507  else if(a.no_operands==3)
508  {
509  a.op0_bv=convert_bv(expr.op0());
510  a.op1_bv=convert_bv(expr.op1());
511  a.op2_bv=convert_bv(expr.op2());
512  set_frozen(a.op0_bv);
513  set_frozen(a.op1_bv);
514  set_frozen(a.op2_bv);
515  }
516  else
517  assert(false);
518 
519  bv=a.result_bv;
520 
521  initialize(a);
522 
523  return a;
524 }
525 
527 {
528  #if 0
529  return from_expr(expr);
530  #else
531  return std::to_string(id_nr)+"/"+id2string(expr.id());
532  #endif
533 }
The type of an expression.
Definition: type.h:20
mstreamt & result()
Definition: message.h:233
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
approximationt & add_approximation(const exprt &expr, bvt &bv)
bvt remainder(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:90
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:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_in_conflict(approximationt &approximation)
check if an under-approximation is part of the conflict
exprt & op0()
Definition: expr.h:84
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1255
mp_integer::ullong_t integer2ulong(const mp_integer &n)
Definition: mp_arith.cpp:189
mstreamt & status()
Definition: message.h:238
Deprecated expression utility functions.
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.h:83
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1089
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)
approximationst approximations
Definition: bv_refinement.h:83
virtual literalt lor(literalt a, literalt b)=0
virtual void set_frozen(literalt a) override
Definition: prop_conv.h:91
typet & type()
Definition: expr.h:60
literalt is_zero(const bvt &op)
Definition: bv_utils.h:137
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
void initialize(approximationt &approximation)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:47
virtual bvt convert_mult(const exprt &expr)
Definition: boolbv_mult.cpp:13
virtual bvt convert_floatbv_op(const exprt &expr)
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:854
void unpack(const mp_integer &i)
Definition: ieee_float.cpp:312
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
virtual bvt mul(const bvt &src1, const bvt &src2)
bool do_arithmetic_refinement
Definition: bv_refinement.h:41
virtual bvt convert_floatbv_op(const exprt &expr)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
Definition: bv_utils.cpp:791
exprt & op1()
Definition: expr.h:87
virtual bvt convert_mult(const exprt &expr)
const namespacet & ns
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:128
virtual bvt convert_mod(const mod_exprt &expr)
std::vector< exprt > operandst
Definition: expr.h:49
unsigned max_node_refinement
Definition: bv_refinement.h:38
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:78
ieee_float_spect spec
Definition: float_utils.h:86
void get_values(approximationt &approximation)
mstreamt & debug()
Definition: message.h:253
literalt is_one(const bvt &op)
Definition: bv_utils.cpp:26
virtual void check_SAT()
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:46
mp_integer pack() const
Definition: ieee_float.cpp:367
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
virtual bvt convert_div(const div_exprt &expr)
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
#define MAX_FLOAT_UNDERAPPROX
mstreamt & progress()
Definition: message.h:248
void set(const ieee_floatt::rounding_modet mode)
Definition: float_utils.h:37
rounding_modet rounding_mode
Definition: ieee_float.h:121
exprt & op2()
Definition: expr.h:90
Abstraction Refinement Loop.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
std::size_t width() const
Definition: ieee_float.h:50
bvt sub(const bvt &src1, const bvt &src2)
Definition: float_utils.h:114
virtual bvt convert_div(const div_exprt &expr)
Definition: boolbv_div.cpp:13
virtual bool is_in_conflict(literalt l) const
Definition: prop.cpp:31
operandst & operands()
Definition: expr.h:70
#define MAX_INTEGER_UNDERAPPROX
virtual void check_UNSAT()
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:29
std::vector< literalt > bvt
Definition: literal.h:197
void unpack(const mp_integer &i)
binary modulo
Definition: std_expr.h:902
bvt build_constant(const ieee_floatt &)