cprover
boolbv.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 <cassert>
12 #include <map>
13 #include <set>
14 
15 #include <util/symbol.h>
16 #include <util/mp_arith.h>
17 #include <util/arith_tools.h>
18 #include <util/replace_expr.h>
19 #include <util/std_types.h>
20 #include <util/prefix.h>
21 #include <util/std_expr.h>
22 #include <util/threeval.h>
23 #include <util/string2int.h>
24 
25 #include <ansi-c/string_constant.h>
26 
27 #include "boolbv_type.h"
28 
29 #include "../floatbv/float_utils.h"
30 
32  const exprt &expr,
33  const std::size_t bit,
34  literalt &dest) const
35 {
36  if(expr.type().id()==ID_bool)
37  {
38  assert(bit==0);
39  return prop_conv_solvert::literal(expr, dest);
40  }
41  else
42  {
43  if(expr.id()==ID_symbol ||
44  expr.id()==ID_nondet_symbol)
45  {
46  const irep_idt &identifier=expr.get(ID_identifier);
47 
48  boolbv_mapt::mappingt::const_iterator it_m=
49  map.mapping.find(identifier);
50 
51  if(it_m==map.mapping.end())
52  return true;
53 
54  const boolbv_mapt::map_entryt &map_entry=it_m->second;
55 
56  assert(bit<map_entry.literal_map.size());
57  if(!map_entry.literal_map[bit].is_set)
58  return true;
59 
60  dest=map_entry.literal_map[bit].l;
61  return false;
62  }
63  else if(expr.id()==ID_index)
64  {
65  const index_exprt &index_expr=to_index_expr(expr);
66 
67  std::size_t element_width=boolbv_width(index_expr.type());
68 
69  if(element_width==0)
70  throw "literal expects a bit-vector type";
71 
72  mp_integer index;
73  if(to_integer(index_expr.index(), index))
74  throw "literal expects constant index";
75 
76  std::size_t offset=integer2unsigned(index*element_width);
77 
78  return literal(index_expr.array(), bit+offset, dest);
79  }
80  else if(expr.id()==ID_member)
81  {
82  const member_exprt &member_expr=to_member_expr(expr);
83 
84  const struct_typet::componentst &components=
85  to_struct_type(expr.type()).components();
86  const irep_idt &component_name=member_expr.get_component_name();
87 
88  std::size_t offset=0;
89 
90  for(struct_typet::componentst::const_iterator
91  it=components.begin();
92  it!=components.end();
93  it++)
94  {
95  const typet &subtype=it->type();
96 
97  if(it->get_name()==component_name)
98  return literal(expr.op0(), bit+offset, dest);
99 
100  std::size_t element_width=boolbv_width(subtype);
101 
102  if(element_width==0)
103  throw "literal expects a bit-vector type";
104 
105  offset+=element_width;
106  }
107 
108  throw "failed to find component";
109  }
110  }
111 
112  throw "found no literal for expression";
113 }
114 
115 const bvt &boolbvt::convert_bv(const exprt &expr)
116 {
117  // check cache first
118  std::pair<bv_cachet::iterator, bool> cache_result=
119  bv_cache.insert(std::make_pair(expr, bvt()));
120  if(!cache_result.second)
121  {
122  return cache_result.first->second;
123  }
124 
125  // Iterators into hash_maps supposedly stay stable
126  // even though we are inserting more elements recursively.
127 
128  cache_result.first->second=convert_bitvector(expr);
129 
130  // check
131  forall_literals(it, cache_result.first->second)
132  {
133  if(freeze_all && !it->is_constant())
134  prop.set_frozen(*it);
135  if(it->var_no()==literalt::unused_var_no())
136  {
137  error() << "unused_var_no: " << expr.pretty() << eom;
138  assert(false);
139  }
140  }
141 
142  return cache_result.first->second;
143 }
144 
146 {
147  ignoring(expr);
148 
149  // try to make it free bits
150  std::size_t width=boolbv_width(expr.type());
151  return prop.new_variables(width);
152 }
153 
155 {
156  if(expr.type().id()==ID_bool)
157  {
158  bvt bv;
159  bv.resize(1);
160  bv[0]=convert(expr);
161  return bv;
162  }
163 
164  if(expr.id()==ID_index)
165  return convert_index(to_index_expr(expr));
166  else if(expr.id()==ID_constraint_select_one)
167  return convert_constraint_select_one(expr);
168  else if(expr.id()==ID_member)
169  return convert_member(to_member_expr(expr));
170  else if(expr.id()==ID_with)
171  return convert_with(expr);
172  else if(expr.id()==ID_update)
173  return convert_update(expr);
174  else if(expr.id()==ID_width)
175  {
176  std::size_t result_width=boolbv_width(expr.type());
177 
178  if(result_width==0)
179  return conversion_failed(expr);
180 
181  if(expr.operands().size()!=1)
182  return conversion_failed(expr);
183 
184  std::size_t op_width=boolbv_width(expr.op0().type());
185 
186  if(op_width==0)
187  return conversion_failed(expr);
188 
189  if(expr.type().id()==ID_unsignedbv ||
190  expr.type().id()==ID_signedbv)
191  return bv_utils.build_constant(op_width/8, result_width);
192  }
193  else if(expr.id()==ID_case)
194  return convert_case(expr);
195  else if(expr.id()==ID_cond)
196  return convert_cond(expr);
197  else if(expr.id()==ID_if)
198  return convert_if(to_if_expr(expr));
199  else if(expr.id()==ID_constant)
200  return convert_constant(to_constant_expr(expr));
201  else if(expr.id()==ID_typecast)
203  else if(expr.id()==ID_symbol)
204  return convert_symbol(to_symbol_expr(expr));
205  else if(expr.id()==ID_bv_literals)
206  return convert_bv_literals(expr);
207  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
208  expr.id()=="no-overflow-plus" ||
209  expr.id()=="no-overflow-minus")
210  return convert_add_sub(expr);
211  else if(expr.id()==ID_mult ||
212  expr.id()=="no-overflow-mult")
213  return convert_mult(expr);
214  else if(expr.id()==ID_div)
215  return convert_div(to_div_expr(expr));
216  else if(expr.id()==ID_mod)
217  return convert_mod(to_mod_expr(expr));
218  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr)
219  return convert_shift(to_shift_expr(expr));
220  else if(expr.id()==ID_floatbv_plus || expr.id()==ID_floatbv_minus ||
221  expr.id()==ID_floatbv_mult || expr.id()==ID_floatbv_div ||
222  expr.id()==ID_floatbv_rem)
223  return convert_floatbv_op(expr);
224  else if(expr.id()==ID_floatbv_typecast)
226  else if(expr.id()==ID_concatenation)
227  return convert_concatenation(expr);
228  else if(expr.id()==ID_replication)
230  else if(expr.id()==ID_extractbits)
232  else if(expr.id()==ID_bitnot || expr.id()==ID_bitand ||
233  expr.id()==ID_bitor || expr.id()==ID_bitxor ||
234  expr.id()==ID_bitxnor || expr.id()==ID_bitnor ||
235  expr.id()==ID_bitnand)
236  return convert_bitwise(expr);
237  else if(expr.id()==ID_unary_minus ||
238  expr.id()=="no-overflow-unary-minus")
239  return convert_unary_minus(to_unary_expr(expr));
240  else if(expr.id()==ID_unary_plus)
241  {
242  assert(expr.operands().size()==1);
243  return convert_bitvector(expr.op0());
244  }
245  else if(expr.id()==ID_abs)
246  return convert_abs(expr);
247  else if(expr.id()==ID_byte_extract_little_endian ||
248  expr.id()==ID_byte_extract_big_endian)
250  else if(expr.id()==ID_byte_update_little_endian ||
251  expr.id()==ID_byte_update_big_endian)
253  else if(expr.id()==ID_nondet_symbol ||
254  expr.id()=="quant_symbol")
255  return convert_symbol(expr);
256  else if(expr.id()==ID_struct)
257  return convert_struct(to_struct_expr(expr));
258  else if(expr.id()==ID_union)
259  return convert_union(to_union_expr(expr));
260  else if(expr.id()==ID_string_constant)
261  return convert_bitvector(
263  else if(expr.id()==ID_array)
264  return convert_array(expr);
265  else if(expr.id()==ID_vector)
266  return convert_vector(expr);
267  else if(expr.id()==ID_complex)
268  return convert_complex(expr);
269  else if(expr.id()==ID_complex_real)
270  return convert_complex_real(expr);
271  else if(expr.id()==ID_complex_imag)
272  return convert_complex_imag(expr);
273  else if(expr.id()==ID_lambda)
274  return convert_lambda(expr);
275  else if(expr.id()==ID_array_of)
276  return convert_array_of(to_array_of_expr(expr));
277  else if(expr.id()==ID_let)
278  {
279  // const let_exprt &let_expr=to_let_expr(expr);
280  throw "let is todo";
281  }
282  else if(expr.id()==ID_function_application)
283  {
285  }
286  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
287  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
288  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
289  return convert_bv_reduction(to_unary_expr(expr));
290  else if(expr.id()==ID_not)
291  return convert_not(to_not_expr(expr));
292  else if(expr.id()==ID_power)
293  return convert_power(to_binary_expr(expr));
294  else if(expr.id()==ID_float_debug1 ||
295  expr.id()==ID_float_debug2)
296  {
297  assert(expr.operands().size()==2);
298  bvt bv0=convert_bitvector(expr.op0());
299  bvt bv1=convert_bitvector(expr.op1());
300  float_utilst float_utils(prop, to_floatbv_type(expr.type()));
301  bvt bv=expr.id()==ID_float_debug1?
302  float_utils.debug1(bv0, bv1):
303  float_utils.debug2(bv0, bv1);
304  return bv;
305  }
306 
307  return conversion_failed(expr);
308 }
309 
311 {
312  std::size_t width=boolbv_width(expr.type());
313 
314  if(width==0)
315  return conversion_failed(expr);
316 
317  if(expr.operands().size()!=2)
318  throw "lambda takes two operands";
319 
320  if(expr.type().id()!=ID_array)
321  return conversion_failed(expr);
322 
323  const exprt &array_size=
324  to_array_type(expr.type()).size();
325 
326  mp_integer size;
327 
328  if(to_integer(array_size, size))
329  return conversion_failed(expr);
330 
331  typet counter_type=expr.op0().type();
332 
333  bvt bv;
334  bv.resize(width);
335 
336  for(mp_integer i=0; i<size; ++i)
337  {
338  exprt counter=from_integer(i, counter_type);
339 
340  exprt expr_op1(expr.op1());
341  replace_expr(expr.op0(), counter, expr_op1);
342 
343  const bvt &tmp=convert_bv(expr_op1);
344 
345  std::size_t offset=integer2unsigned(i*tmp.size());
346 
347  if(size*tmp.size()!=width)
348  throw "convert_lambda: unexpected operand width";
349 
350  for(std::size_t j=0; j<tmp.size(); j++)
351  bv[offset+j]=tmp[j];
352  }
353 
354  return bv;
355 }
356 
358 {
359  std::size_t width=boolbv_width(expr.type());
360 
361  if(width==0)
362  return conversion_failed(expr);
363 
364  bvt bv;
365  bv.resize(width);
366 
367  const irept::subt &bv_sub=expr.find(ID_bv).get_sub();
368 
369  if(bv_sub.size()!=width)
370  throw "bv_literals with wrong size";
371 
372  for(std::size_t i=0; i<width; i++)
373  bv[i].set(unsafe_string2int(id2string(bv_sub[i].id())));
374 
375  return bv;
376 }
377 
379 {
380  const typet &type=expr.type();
381  std::size_t width=boolbv_width(type);
382 
383  bvt bv;
384  bv.resize(width);
385 
386  const irep_idt &identifier=expr.get(ID_identifier);
387 
388  if(identifier.empty())
389  throw "convert_symbol got empty identifier";
390 
391  if(width==0)
392  {
393  // just put in map
394  map.get_map_entry(identifier, type);
395  }
396  else
397  {
398  map.get_literals(identifier, type, width, bv);
399 
400  forall_literals(it, bv)
401  if(it->var_no()>=prop.no_variables() &&
402  !it->is_constant())
403  {
404  error() << identifier << eom;
405  assert(false);
406  }
407  }
408 
409  return bv;
410 }
411 
412 
414  const function_application_exprt &expr)
415 {
416  // record
417  functions.record(expr);
418 
419  // make it free bits
420  return prop.new_variables(boolbv_width(expr.type()));
421 }
422 
423 
425 {
426  if(expr.type().id()!=ID_bool)
427  {
428  error() << "boolbvt::convert_rest got non-boolean operand: "
429  << expr.pretty() << eom;
430  throw 0;
431  }
432 
433  const exprt::operandst &operands=expr.operands();
434 
435  if(expr.id()==ID_typecast)
436  return convert_typecast(to_typecast_expr(expr));
437  else if(expr.id()==ID_equal)
438  return convert_equality(to_equal_expr(expr));
439  else if(expr.id()==ID_verilog_case_equality ||
440  expr.id()==ID_verilog_case_inequality)
442  else if(expr.id()==ID_notequal)
443  {
444  if(expr.operands().size()!=2)
445  throw "notequal expects two operands";
446 
447  return !convert_equality(equal_exprt(expr.op0(), expr.op1()));
448  }
449  else if(expr.id()==ID_ieee_float_equal ||
450  expr.id()==ID_ieee_float_notequal)
451  return convert_ieee_float_rel(expr);
452  else if(expr.id()==ID_le || expr.id()==ID_ge ||
453  expr.id()==ID_lt || expr.id()==ID_gt)
454  return convert_bv_rel(expr);
455  else if(expr.id()==ID_extractbit)
457  else if(expr.id()==ID_forall)
458  return convert_quantifier(expr);
459  else if(expr.id()==ID_exists)
460  return convert_quantifier(expr);
461  else if(expr.id()==ID_index)
462  {
463  bvt bv=convert_index(to_index_expr(expr));
464 
465  if(bv.size()!=1)
466  throw "convert_index returned non-bool bitvector";
467 
468  return bv[0];
469  }
470  else if(expr.id()==ID_member)
471  {
473 
474  if(bv.size()!=1)
475  throw "convert_member returned non-bool bitvector";
476 
477  return bv[0];
478  }
479  else if(expr.id()==ID_case)
480  {
481  bvt bv=convert_case(expr);
482 
483  if(bv.size()!=1)
484  throw "convert_case returned non-bool bitvector";
485 
486  return bv[0];
487  }
488  else if(expr.id()==ID_cond)
489  {
490  bvt bv=convert_cond(expr);
491 
492  if(bv.size()!=1)
493  throw "convert_cond returned non-bool bitvector";
494 
495  return bv[0];
496  }
497  else if(expr.id()==ID_sign)
498  {
499  if(expr.operands().size()!=1)
500  throw "sign expects one operand";
501 
502  const bvt &bv=convert_bv(operands[0]);
503 
504  if(bv.empty())
505  throw "sign operator takes one non-empty operand";
506 
507  if(operands[0].type().id()==ID_signedbv)
508  return bv[bv.size()-1];
509  else if(operands[0].type().id()==ID_unsignedbv)
510  return const_literal(false);
511  else if(operands[0].type().id()==ID_fixedbv)
512  return bv[bv.size()-1];
513  else if(operands[0].type().id()==ID_floatbv)
514  return bv[bv.size()-1];
515  }
516  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
517  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
518  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
519  return convert_reduction(to_unary_expr(expr));
520  else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
521  return convert_onehot(to_unary_expr(expr));
522  else if(has_prefix(expr.id_string(), "overflow-"))
523  return convert_overflow(expr);
524  else if(expr.id()==ID_isnan)
525  {
526  if(expr.operands().size()!=1)
527  throw "isnan expects one operand";
528 
529  const bvt &bv=convert_bv(operands[0]);
530 
531  if(expr.op0().type().id()==ID_floatbv)
532  {
533  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
534  return float_utils.is_NaN(bv);
535  }
536  else if(expr.op0().type().id()==ID_fixedbv)
537  return const_literal(false);
538  }
539  else if(expr.id()==ID_isfinite)
540  {
541  if(expr.operands().size()!=1)
542  throw "isfinite expects one operand";
543 
544  const bvt &bv=convert_bv(operands[0]);
545 
546  if(expr.op0().type().id()==ID_floatbv)
547  {
548  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
549  return prop.land(
550  !float_utils.is_infinity(bv),
551  !float_utils.is_NaN(bv));
552  }
553  else if(expr.op0().type().id()==ID_fixedbv)
554  return const_literal(true);
555  }
556  else if(expr.id()==ID_isinf)
557  {
558  if(expr.operands().size()!=1)
559  throw "isinf expects one operand";
560 
561  const bvt &bv=convert_bv(operands[0]);
562 
563  if(expr.op0().type().id()==ID_floatbv)
564  {
565  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
566  return float_utils.is_infinity(bv);
567  }
568  else if(expr.op0().type().id()==ID_fixedbv)
569  return const_literal(false);
570  }
571  else if(expr.id()==ID_isnormal)
572  {
573  if(expr.operands().size()!=1)
574  throw "isnormal expects one operand";
575 
576  const bvt &bv=convert_bv(operands[0]);
577 
578  if(expr.op0().type().id()==ID_floatbv)
579  {
580  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
581  return float_utils.is_normal(bv);
582  }
583  else if(expr.op0().type().id()==ID_fixedbv)
584  return const_literal(true);
585  }
586 
587  return SUB::convert_rest(expr);
588 }
589 
591 {
593  return true;
594 
595  const typet &type=ns.follow(expr.lhs().type());
596 
597  if(expr.lhs().id()==ID_symbol &&
598  type==ns.follow(expr.rhs().type()) &&
599  type.id()!=ID_bool)
600  {
601  // see if it is an unbounded array
602  if(is_unbounded_array(type))
603  return true;
604 
605  const bvt &bv1=convert_bv(expr.rhs());
606 
607  const irep_idt &identifier=
608  to_symbol_expr(expr.lhs()).get_identifier();
609 
610  map.set_literals(identifier, type, bv1);
611 
612  if(freeze_all)
613  set_frozen(bv1);
614 
615  return false;
616  }
617 
618  return true;
619 }
620 
621 void boolbvt::set_to(const exprt &expr, bool value)
622 {
623  if(expr.type().id()!=ID_bool)
624  {
625  error() << "boolbvt::set_to got non-boolean operand: "
626  << expr.pretty() << eom;
627  throw 0;
628  }
629 
630  if(value)
631  {
632  if(expr.id()==ID_equal)
633  {
635  return;
636  }
637  }
638 
639  return SUB::set_to(expr, value);
640 }
641 
642 void boolbvt::make_bv_expr(const typet &type, const bvt &bv, exprt &dest)
643 {
644  dest=exprt(ID_bv_literals, type);
645  irept::subt &bv_sub=dest.add(ID_bv).get_sub();
646 
647  bv_sub.resize(bv.size());
648 
649  for(std::size_t i=0; i<bv.size(); i++)
650  bv_sub[i].id(std::to_string(bv[i].get()));
651 }
652 
653 void boolbvt::make_free_bv_expr(const typet &type, exprt &dest)
654 {
655  std::size_t width=boolbv_width(type);
656 
657  if(width==0)
658  {
659  error() << "failed to get width of " << type.pretty() << eom;
660  throw 0;
661  }
662 
663  bvt bv;
664  bv.resize(width);
665 
666  // make result free variables
667  Forall_literals(it, bv)
668  *it=prop.new_variable();
669 
670  make_bv_expr(type, bv, dest);
671 }
672 
673 bool boolbvt::is_unbounded_array(const typet &type) const
674 {
675  if(type.id()==ID_symbol)
676  return is_unbounded_array(ns.follow(type));
677 
678  if(type.id()!=ID_array)
679  return false;
680 
682  return true;
683 
684  const exprt &size=to_array_type(type).size();
685 
686  mp_integer s;
687  if(to_integer(size, s))
688  return true;
689 
691  if(s>1000) // magic number!
692  return true;
693 
694  return false;
695 }
696 
697 void boolbvt::print_assignment(std::ostream &out) const
698 {
699  for(boolbv_mapt::mappingt::const_iterator it=map.mapping.begin();
700  it!=map.mapping.end();
701  it++)
702  {
703  out << it->first << "="
704  << it->second.get_value(prop) << '\n';
705  }
706 }
707 
709 {
710  const struct_typet::componentst &components=
711  src.components();
712 
713  dest.resize(components.size());
714  std::size_t offset=0;
715  for(std::size_t i=0; i<components.size(); i++)
716  {
717  std::size_t comp_width=boolbv_width(components[i].type());
718  dest[i]=offset;
719  offset+=comp_width;
720  }
721 }
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
virtual bvt convert_complex_real(const exprt &expr)
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:49
The type of an expression.
Definition: type.h:20
void print_assignment(std::ostream &out) const override
Definition: boolbv.cpp:697
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:250
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
virtual bvt convert_with(const exprt &expr)
Definition: boolbv_with.cpp:18
virtual bvt convert_concatenation(const exprt &expr)
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
Definition: std_expr.h:3826
virtual bvt convert_abs(const exprt &expr)
Definition: boolbv_abs.cpp:17
bv_utilst bv_utils
Definition: boolbv.h:93
virtual literalt convert_ieee_float_rel(const exprt &expr)
BigInt mp_integer
Definition: mp_arith.h:19
virtual bvt convert_array_of(const array_of_exprt &expr)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast a generic exprt to an extractbits_exprt.
Definition: std_expr.h:2570
virtual bvt convert_bv_reduction(const unary_exprt &expr)
literal_mapt literal_map
Definition: boolbv_map.h:53
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
Definition: std_expr.h:1286
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
application of (mathematical) function
Definition: std_expr.h:3785
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
Symbol table entry.
virtual void set_frozen(literalt a)
Definition: prop.h:109
bool equality_propagation
Definition: prop_conv.h:107
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
std::vector< irept > subt
Definition: irep.h:91
virtual literalt convert_onehot(const unary_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual literalt convert_overflow(const exprt &expr)
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:39
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
Definition: boolbv.h:90
virtual literalt convert_equality(const equal_exprt &expr)
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:673
virtual bvt convert_replication(const replication_exprt &expr)
static var_not unused_var_no()
Definition: literal.h:175
virtual bvt convert_bv_literals(const exprt &expr)
Definition: boolbv.cpp:357
std::vector< componentt > componentst
Definition: std_types.h:240
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
Definition: std_expr.h:2280
virtual bvt convert_struct(const struct_exprt &expr)
const componentst & components() const
Definition: std_types.h:242
virtual bvt convert_function_application(const function_application_exprt &expr)
Definition: boolbv.cpp:413
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
Definition: std_expr.h:1487
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
Definition: std_expr.h:1105
virtual bvt convert_lambda(const exprt &expr)
Definition: boolbv.cpp:310
virtual void set_frozen(literalt a) override
Definition: prop_conv.h:91
typet & type()
Definition: expr.h:60
void build_offset_map(const struct_typet &src, offset_mapt &dest)
Definition: boolbv.cpp:708
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
Structure type.
Definition: std_types.h:296
virtual void set_to(const exprt &expr, bool value) override
Definition: prop_conv.cpp:371
virtual bool literal(const exprt &expr, literalt &literal) const
Definition: prop_conv.cpp:46
virtual bvt convert_constant(const constant_exprt &expr)
#define forall_literals(it, bv)
Definition: literal.h:199
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
Definition: std_expr.h:2482
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:378
subt & get_sub()
Definition: irep.h:245
virtual bvt convert_mult(const exprt &expr)
Definition: boolbv_mult.cpp:13
Extract member of struct or union.
Definition: std_expr.h:3214
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
equality
Definition: std_expr.h:1082
virtual bvt convert_complex(const exprt &expr)
virtual literalt convert_quantifier(const exprt &expr)
virtual bvt convert_update(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
literalt is_normal(const bvt &)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:189
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
virtual literalt new_variable()=0
virtual literalt convert_bv_rel(const exprt &expr)
#define Forall_literals(it, bv)
Definition: literal.h:203
mappingt mapping
Definition: boolbv_map.h:59
virtual bvt convert_add_sub(const exprt &expr)
virtual literalt convert_reduction(const unary_exprt &expr)
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
functionst functions
Definition: boolbv.h:96
virtual size_t no_variables() const =0
virtual void make_free_bv_expr(const typet &type, exprt &dest)
Definition: boolbv.cpp:653
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:121
virtual bvt convert_bitvector(const exprt &expr)
Definition: boolbv.cpp:154
API to expression classes.
virtual bvt convert_floatbv_op(const exprt &expr)
exprt & op1()
Definition: expr.h:87
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition: boolbv.cpp:590
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
Definition: boolbv.cpp:31
const exprt & size() const
Definition: std_types.h:915
const namespacet & ns
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
Definition: std_expr.h:927
virtual bvt convert_union(const union_exprt &expr)
array_exprt to_array_expr() const
convert string into array constant
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1441
virtual bvt convert_extractbits(const extractbits_exprt &expr)
virtual literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:424
virtual bvt convert_complex_imag(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast a generic exprt to a binary_exprt.
Definition: std_expr.h:524
virtual bvt convert_cond(const exprt &expr)
Definition: boolbv_cond.cpp:13
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:12
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
Definition: std_expr.h:2682
literalt is_infinity(const bvt &)
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
literalt const_literal(bool value)
Definition: literal.h:187
literalt is_NaN(const bvt &)
API to type classes.
virtual bvt convert_constraint_select_one(const exprt &expr)
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast a generic exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:1829
void record(const function_application_exprt &function_application)
Definition: functions.cpp:16
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
Definition: std_expr.h:879
unbounded_arrayt unbounded_array
Definition: boolbv.h:76
exprt & index()
Definition: std_expr.h:1208
virtual bvt convert_vector(const exprt &expr)
const string_constantt & to_string_constant(const exprt &expr)
virtual bvt convert_array(const exprt &expr)
bv_cachet bv_cache
Definition: boolbv.h:116
virtual void make_bv_expr(const typet &type, const bvt &bv, exprt &dest)
Definition: boolbv.cpp:642
Base class for all expressions.
Definition: expr.h:46
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
irep_idt get_component_name() const
Definition: std_expr.h:3249
irept & add(const irep_namet &name)
Definition: irep.cpp:306
virtual bvt convert_member(const member_exprt &expr)
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:337
const std::string & id_string() const
Definition: irep.h:192
mstreamt & error()
Definition: message.h:223
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast a generic exprt to a binary_relation_exprt.
Definition: std_expr.h:619
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
const replication_exprt & to_replication_expr(const exprt &expr)
Cast a generic exprt to a replication_exprt.
Definition: std_expr.h:2411
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
Definition: boolbv_map.cpp:84
boolbv_mapt map
Definition: boolbv.h:99
virtual bvt convert_unary_minus(const unary_exprt &expr)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
virtual bvt convert_div(const div_exprt &expr)
Definition: boolbv_div.cpp:13
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
void set_to(const exprt &expr, bool value) override
Definition: boolbv.cpp:621
virtual literalt convert_extractbit(const extractbit_exprt &expr)
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
virtual void ignoring(const exprt &expr)
Definition: prop_conv.cpp:470
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:61
bool empty() const
Definition: dstring.h:61
exprt & array()
Definition: std_expr.h:1198
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
std::vector< literalt > bvt
Definition: literal.h:197
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
virtual bvt convert_bitwise(const exprt &expr)
virtual bvt convert_power(const binary_exprt &expr)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast a generic exprt to a unary_exprt.
Definition: std_expr.h:279
array index operator
Definition: std_expr.h:1170