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 <algorithm>
12 #include <map>
13 #include <set>
14 
15 #include <util/arith_tools.h>
16 #include <util/magic.h>
17 #include <util/mp_arith.h>
18 #include <util/prefix.h>
19 #include <util/replace_expr.h>
20 #include <util/std_expr.h>
21 #include <util/std_types.h>
22 #include <util/string2int.h>
23 #include <util/string_constant.h>
24 #include <util/symbol.h>
25 #include <util/threeval.h>
26 
27 #include "boolbv_type.h"
28 
31 
33  const exprt &expr,
34  const std::size_t bit,
35  literalt &dest) const
36 {
37  if(expr.type().id()==ID_bool)
38  {
39  INVARIANT(
40  bit == 0,
41  "boolean expressions shall be represented by a single bit and hence the "
42  "only valid bit index is 0");
43  return prop_conv_solvert::literal(to_symbol_expr(expr), dest);
44  }
45  else
46  {
47  if(expr.id()==ID_symbol ||
48  expr.id()==ID_nondet_symbol)
49  {
50  const irep_idt &identifier=expr.get(ID_identifier);
51 
52  boolbv_mapt::mappingt::const_iterator it_m=
53  map.mapping.find(identifier);
54 
55  if(it_m==map.mapping.end())
56  return true;
57 
58  const boolbv_mapt::map_entryt &map_entry=it_m->second;
59 
60  INVARIANT(
61  bit < map_entry.literal_map.size(), "bit index shall be within bounds");
62  if(!map_entry.literal_map[bit].is_set)
63  return true;
64 
65  dest=map_entry.literal_map[bit].l;
66  return false;
67  }
68  else if(expr.id()==ID_index)
69  {
70  const index_exprt &index_expr=to_index_expr(expr);
71 
72  std::size_t element_width=boolbv_width(index_expr.type());
73  CHECK_RETURN(element_width != 0);
74 
75  mp_integer index = numeric_cast_v<mp_integer>(index_expr.index());
76 
77  std::size_t offset = numeric_cast_v<std::size_t>(index * element_width);
78 
79  return literal(index_expr.array(), bit+offset, dest);
80  }
81  else if(expr.id()==ID_member)
82  {
83  const member_exprt &member_expr=to_member_expr(expr);
84 
85  const struct_typet::componentst &components=
86  to_struct_type(expr.type()).components();
87  const irep_idt &component_name=member_expr.get_component_name();
88 
89  std::size_t offset=0;
90 
91  for(const auto &c : components)
92  {
93  const typet &subtype = c.type();
94 
95  if(c.get_name() == component_name)
96  return literal(expr.op0(), bit+offset, dest);
97 
98  std::size_t element_width=boolbv_width(subtype);
99  CHECK_RETURN(element_width != 0);
100 
101  offset+=element_width;
102  }
103 
104  INVARIANT(false, "struct type should have accessed component");
105  }
106  }
107 
108  INVARIANT(false, "expression should have a corresponding literal");
109 }
110 
111 const bvt &
113 {
114  // check cache first
115  std::pair<bv_cachet::iterator, bool> cache_result=
116  bv_cache.insert(std::make_pair(expr, bvt()));
117  if(!cache_result.second)
118  {
119  return cache_result.first->second;
120  }
121 
122  // Iterators into hash_maps supposedly stay stable
123  // even though we are inserting more elements recursively.
124 
125  const bvt &bv = convert_bitvector(expr);
126 
128  !expected_width || bv.size() == *expected_width,
129  "bitvector width shall match the indicated expected width",
130  expr.find_source_location(),
132 
133  cache_result.first->second = bv;
134 
135  // check
136  forall_literals(it, cache_result.first->second)
137  {
138  if(freeze_all && !it->is_constant())
139  prop.set_frozen(*it);
140 
142  it->var_no() != literalt::unused_var_no(),
143  "variable number must be different from the unused variable number",
144  expr.find_source_location(),
146  }
147 
148  return cache_result.first->second;
149 }
150 
152 {
153  ignoring(expr);
154 
155  // try to make it free bits
156  std::size_t width=boolbv_width(expr.type());
157  return prop.new_variables(width);
158 }
159 
169 {
170  if(expr.type().id()==ID_bool)
171  {
172  bvt bv;
173  bv.resize(1);
174  bv[0]=convert(expr);
175  return bv;
176  }
177 
178  if(expr.id()==ID_index)
179  return convert_index(to_index_expr(expr));
180  else if(expr.id()==ID_constraint_select_one)
181  return convert_constraint_select_one(expr);
182  else if(expr.id()==ID_member)
183  return convert_member(to_member_expr(expr));
184  else if(expr.id()==ID_with)
185  return convert_with(expr);
186  else if(expr.id()==ID_update)
187  return convert_update(expr);
188  else if(expr.id()==ID_width)
189  {
190  std::size_t result_width=boolbv_width(expr.type());
191 
192  if(result_width==0)
193  return conversion_failed(expr);
194 
195  if(expr.operands().size()!=1)
196  return conversion_failed(expr);
197 
198  std::size_t op_width=boolbv_width(expr.op0().type());
199 
200  if(op_width==0)
201  return conversion_failed(expr);
202 
203  if(expr.type().id()==ID_unsignedbv ||
204  expr.type().id()==ID_signedbv)
205  return bv_utils.build_constant(op_width/8, result_width);
206  }
207  else if(expr.id()==ID_case)
208  return convert_case(expr);
209  else if(expr.id()==ID_cond)
210  return convert_cond(to_cond_expr(expr));
211  else if(expr.id()==ID_if)
212  return convert_if(to_if_expr(expr));
213  else if(expr.id()==ID_constant)
214  return convert_constant(to_constant_expr(expr));
215  else if(expr.id()==ID_typecast)
217  else if(expr.id()==ID_symbol)
218  return convert_symbol(to_symbol_expr(expr));
219  else if(expr.id()==ID_bv_literals)
220  return convert_bv_literals(expr);
221  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
222  expr.id()=="no-overflow-plus" ||
223  expr.id()=="no-overflow-minus")
224  return convert_add_sub(expr);
225  else if(expr.id() == ID_mult)
226  return convert_mult(to_mult_expr(expr));
227  else if(expr.id()==ID_div)
228  return convert_div(to_div_expr(expr));
229  else if(expr.id()==ID_mod)
230  return convert_mod(to_mod_expr(expr));
231  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr ||
232  expr.id()==ID_rol || expr.id()==ID_ror)
233  return convert_shift(to_shift_expr(expr));
234  else if(expr.id()==ID_floatbv_plus || expr.id()==ID_floatbv_minus ||
235  expr.id()==ID_floatbv_mult || expr.id()==ID_floatbv_div ||
236  expr.id()==ID_floatbv_rem)
237  return convert_floatbv_op(expr);
238  else if(expr.id()==ID_floatbv_typecast)
240  else if(expr.id()==ID_concatenation)
242  else if(expr.id()==ID_replication)
244  else if(expr.id()==ID_extractbits)
246  else if(expr.id()==ID_bitnot || expr.id()==ID_bitand ||
247  expr.id()==ID_bitor || expr.id()==ID_bitxor ||
248  expr.id()==ID_bitxnor || expr.id()==ID_bitnor ||
249  expr.id()==ID_bitnand)
250  return convert_bitwise(expr);
251  else if(expr.id() == ID_unary_minus)
253  else if(expr.id()==ID_unary_plus)
254  {
255  return convert_bitvector(to_unary_plus_expr(expr).op());
256  }
257  else if(expr.id()==ID_abs)
258  return convert_abs(to_abs_expr(expr));
259  else if(expr.id() == ID_bswap)
260  return convert_bswap(to_bswap_expr(expr));
261  else if(expr.id()==ID_byte_extract_little_endian ||
262  expr.id()==ID_byte_extract_big_endian)
264  else if(expr.id()==ID_byte_update_little_endian ||
265  expr.id()==ID_byte_update_big_endian)
267  else if(expr.id()==ID_nondet_symbol ||
268  expr.id()=="quant_symbol")
269  return convert_symbol(expr);
270  else if(expr.id()==ID_struct)
271  return convert_struct(to_struct_expr(expr));
272  else if(expr.id()==ID_union)
273  return convert_union(to_union_expr(expr));
274  else if(expr.id()==ID_string_constant)
275  return convert_bitvector(
277  else if(expr.id()==ID_array)
278  return convert_array(expr);
279  else if(expr.id()==ID_vector)
280  return convert_vector(to_vector_expr(expr));
281  else if(expr.id()==ID_complex)
282  return convert_complex(to_complex_expr(expr));
283  else if(expr.id()==ID_complex_real)
285  else if(expr.id()==ID_complex_imag)
287  else if(expr.id()==ID_lambda)
288  return convert_lambda(expr);
289  else if(expr.id()==ID_array_of)
290  return convert_array_of(to_array_of_expr(expr));
291  else if(expr.id()==ID_let)
292  return convert_let(to_let_expr(expr));
293  else if(expr.id()==ID_function_application)
296  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
297  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
298  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
299  return convert_bv_reduction(to_unary_expr(expr));
300  else if(expr.id()==ID_not)
301  return convert_not(to_not_expr(expr));
302  else if(expr.id()==ID_power)
303  return convert_power(to_binary_expr(expr));
304  else if(expr.id() == ID_popcount)
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 
318  expr.operands().size() == 2, "lambda expression should have 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  const auto size = numeric_cast<mp_integer>(array_size);
327 
328  if(!size.has_value())
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  INVARIANT(
346  *size * tmp.size() == width,
347  "total bitvector width shall equal the number of operands times the size "
348  "per operand");
349 
350  std::size_t offset = numeric_cast_v<std::size_t>(i * tmp.size());
351 
352  for(std::size_t j=0; j<tmp.size(); j++)
353  bv[offset+j]=tmp[j];
354  }
355 
356  return bv;
357 }
358 
360 {
361  std::size_t width=boolbv_width(expr.type());
362 
363  if(width==0)
364  return conversion_failed(expr);
365 
366  bvt bv;
367  bv.resize(width);
368 
369  const irept::subt &bv_sub=expr.find(ID_bv).get_sub();
370 
371  if(bv_sub.size()!=width)
372  throw "bv_literals with wrong size";
373 
374  for(std::size_t i=0; i<width; i++)
375  bv[i].set(unsafe_string2unsigned(id2string(bv_sub[i].id())));
376 
377  return bv;
378 }
379 
381 {
382  const typet &type=expr.type();
383  std::size_t width=boolbv_width(type);
384 
385  bvt bv;
386  bv.resize(width);
387 
388  const irep_idt &identifier = expr.get(ID_identifier);
389  CHECK_RETURN(!identifier.empty());
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 
401  std::all_of(
402  bv.begin(),
403  bv.end(),
404  [this](const literalt &l) {
405  return l.var_no() < prop.no_variables() || l.is_constant();
406  }),
407  "variable number of non-constant literals should be within bounds",
408  id2string(identifier));
409  }
410 
411  return bv;
412 }
413 
414 
416  const function_application_exprt &expr)
417 {
418  // record
419  functions.record(expr);
420 
421  // make it free bits
422  return prop.new_variables(boolbv_width(expr.type()));
423 }
424 
425 
427 {
428  PRECONDITION(expr.type().id() == ID_bool);
429  const exprt::operandst &operands=expr.operands();
430 
431  if(expr.id()==ID_typecast)
432  return convert_typecast(to_typecast_expr(expr));
433  else if(expr.id()==ID_equal)
434  return convert_equality(to_equal_expr(expr));
435  else if(expr.id()==ID_verilog_case_equality ||
436  expr.id()==ID_verilog_case_inequality)
438  else if(expr.id()==ID_notequal)
439  {
440  DATA_INVARIANT(expr.operands().size() == 2, "notequal expects two operands");
441  return !convert_equality(equal_exprt(expr.op0(), expr.op1()));
442  }
443  else if(expr.id()==ID_ieee_float_equal ||
444  expr.id()==ID_ieee_float_notequal)
445  return convert_ieee_float_rel(expr);
446  else if(expr.id()==ID_le || expr.id()==ID_ge ||
447  expr.id()==ID_lt || expr.id()==ID_gt)
448  return convert_bv_rel(expr);
449  else if(expr.id()==ID_extractbit)
451  else if(expr.id()==ID_forall)
453  else if(expr.id()==ID_exists)
455  else if(expr.id()==ID_let)
456  {
457  bvt bv=convert_let(to_let_expr(expr));
458 
459  DATA_INVARIANT(bv.size()==1,
460  "convert_let must return 1-bit vector for boolean let");
461 
462  return bv[0];
463  }
464  else if(expr.id()==ID_index)
465  {
466  bvt bv=convert_index(to_index_expr(expr));
467  CHECK_RETURN(bv.size() == 1);
468  return bv[0];
469  }
470  else if(expr.id()==ID_member)
471  {
473  CHECK_RETURN(bv.size() == 1);
474  return bv[0];
475  }
476  else if(expr.id()==ID_case)
477  {
478  bvt bv=convert_case(expr);
479  CHECK_RETURN(bv.size() == 1);
480  return bv[0];
481  }
482  else if(expr.id()==ID_cond)
483  {
484  bvt bv = convert_cond(to_cond_expr(expr));
485  CHECK_RETURN(bv.size() == 1);
486  return bv[0];
487  }
488  else if(expr.id()==ID_sign)
489  {
490  DATA_INVARIANT(expr.operands().size() == 1, "sign expects one operand");
491  const bvt &bv=convert_bv(operands[0]);
492  CHECK_RETURN(!bv.empty());
493  const irep_idt type_id = operands[0].type().id();
494  if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
495  return bv[bv.size()-1];
496  if(type_id == ID_unsignedbv)
497  return const_literal(false);
498  }
499  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
500  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
501  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
502  return convert_reduction(to_unary_expr(expr));
503  else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
504  return convert_onehot(to_unary_expr(expr));
505  else if(has_prefix(expr.id_string(), "overflow-"))
506  return convert_overflow(expr);
507  else if(expr.id()==ID_isnan)
508  {
509  DATA_INVARIANT(expr.operands().size() == 1, "isnan expects one operand");
510  const bvt &bv=convert_bv(operands[0]);
511 
512  if(expr.op0().type().id()==ID_floatbv)
513  {
514  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
515  return float_utils.is_NaN(bv);
516  }
517  else if(expr.op0().type().id() == ID_fixedbv)
518  return const_literal(false);
519  }
520  else if(expr.id()==ID_isfinite)
521  {
522  DATA_INVARIANT(expr.operands().size() == 1, "isfinite expects one operand");
523  const bvt &bv=convert_bv(operands[0]);
524  if(expr.op0().type().id()==ID_floatbv)
525  {
526  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
527  return prop.land(
528  !float_utils.is_infinity(bv),
529  !float_utils.is_NaN(bv));
530  }
531  else if(expr.op0().type().id() == ID_fixedbv)
532  return const_literal(true);
533  }
534  else if(expr.id()==ID_isinf)
535  {
536  DATA_INVARIANT(expr.operands().size() == 1, "isinf expects one operand");
537  const bvt &bv=convert_bv(operands[0]);
538  if(expr.op0().type().id()==ID_floatbv)
539  {
540  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
541  return float_utils.is_infinity(bv);
542  }
543  else if(expr.op0().type().id() == ID_fixedbv)
544  return const_literal(false);
545  }
546  else if(expr.id()==ID_isnormal)
547  {
548  DATA_INVARIANT(expr.operands().size() == 1, "isnormal expects one operand");
549  if(expr.op0().type().id()==ID_floatbv)
550  {
551  const bvt &bv = convert_bv(operands[0]);
552  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
553  return float_utils.is_normal(bv);
554  }
555  else if(expr.op0().type().id() == ID_fixedbv)
556  return const_literal(true);
557  }
558 
559  return SUB::convert_rest(expr);
560 }
561 
563 {
565  return true;
566 
567  const typet &type=ns.follow(expr.lhs().type());
568 
569  if(expr.lhs().id()==ID_symbol &&
570  type==ns.follow(expr.rhs().type()) &&
571  type.id()!=ID_bool)
572  {
573  // see if it is an unbounded array
574  if(is_unbounded_array(type))
575  return true;
576 
577  const bvt &bv1=convert_bv(expr.rhs());
578 
579  const irep_idt &identifier=
580  to_symbol_expr(expr.lhs()).get_identifier();
581 
582  map.set_literals(identifier, type, bv1);
583 
584  if(freeze_all)
585  set_frozen(bv1);
586 
587  return false;
588  }
589 
590  return true;
591 }
592 
593 void boolbvt::set_to(const exprt &expr, bool value)
594 {
595  PRECONDITION(expr.type().id() == ID_bool);
596 
597  const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
598  if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))
599  return;
600  SUB::set_to(expr, value);
601 }
602 
603 exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
604 {
605  exprt dest(ID_bv_literals, type);
606  irept::subt &bv_sub=dest.add(ID_bv).get_sub();
607  bv_sub.resize(bv.size());
608 
609  for(std::size_t i=0; i<bv.size(); i++)
610  bv_sub[i].id(std::to_string(bv[i].get()));
611  return dest;
612 }
613 
615 {
616  const std::size_t width = boolbv_width(type);
617  PRECONDITION(width != 0);
618  bvt bv(width);
619  for(auto &lit : bv)
620  lit = prop.new_variable();
621  return make_bv_expr(type, bv);
622 }
623 
624 bool boolbvt::is_unbounded_array(const typet &type) const
625 {
626  if(type.id() == ID_symbol_type)
627  return is_unbounded_array(ns.follow(type));
628 
629  if(type.id()!=ID_array)
630  return false;
631 
633  return true;
634 
635  const exprt &size=to_array_type(type).size();
636 
637  mp_integer s;
638  if(to_integer(size, s))
639  return true;
640 
643  return true;
644 
645  return false;
646 }
647 
648 void boolbvt::print_assignment(std::ostream &out) const
649 {
651  for(const auto &pair : map.mapping)
652  out << pair.first << "=" << pair.second.get_value(prop) << '\n';
653 }
654 
656 {
657  const struct_typet::componentst &components = src.components();
658  offset_mapt dest;
659  dest.reserve(components.size());
660  std::size_t offset = 0;
661  for(const auto &comp : components)
662  {
663  dest.push_back(offset);
664  offset += boolbv_width(comp.type());
665  }
666  return dest;
667 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:49
The type of an expression, extends irept.
Definition: type.h:27
void print_assignment(std::ostream &out) const override
Definition: boolbv.cpp:648
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:252
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
virtual bvt convert_with(const exprt &expr)
Definition: boolbv_with.cpp:19
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: std_expr.h:600
bv_utilst bv_utils
Definition: boolbv.h:95
virtual literalt convert_ieee_float_rel(const exprt &expr)
BigInt mp_integer
Definition: mp_arith.h:22
virtual bvt convert_array_of(const array_of_exprt &expr)
virtual bvt convert_bv_reduction(const unary_exprt &expr)
literal_mapt literal_map
Definition: boolbv_map.h:53
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Application of (mathematical) function.
Definition: std_expr.h:4481
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
Symbol table entry.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1309
bool equality_propagation
Definition: prop_conv.h:112
exprt & op0()
Definition: expr.h:84
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1257
std::vector< irept > subt
Definition: irep.h:160
virtual literalt convert_onehot(const unary_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:540
virtual literalt convert_overflow(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:69
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
Definition: boolbv.h:92
virtual literalt convert_equality(const equal_exprt &expr)
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:624
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:359
std::vector< componentt > componentst
Definition: std_types.h:203
virtual bvt convert_struct(const struct_exprt &expr)
const componentst & components() const
Definition: std_types.h:205
virtual bvt convert_function_application(const function_application_exprt &expr)
Definition: boolbv.cpp:415
virtual bvt convert_lambda(const exprt &expr)
Definition: boolbv.cpp:310
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:2102
typet & type()
Return the type of the expression.
Definition: expr.h:68
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
Magic numbers used throughout the codebase.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
Structure type, corresponds to C style structs.
Definition: std_types.h:276
void set_to(const exprt &expr, bool value) override
Definition: prop_conv.cpp:364
virtual bvt convert_constant(const constant_exprt &expr)
#define forall_literals(it, bv)
Definition: literal.h:202
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:380
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4683
subt & get_sub()
Definition: irep.h:317
Extract member of struct or union.
Definition: std_expr.h:3890
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Equality.
Definition: std_expr.h:1484
virtual bvt convert_update(const exprt &expr)
literalt is_normal(const bvt &)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:259
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
virtual bvt convert_abs(const abs_exprt &expr)
Definition: boolbv_abs.cpp:17
void print_assignment(std::ostream &out) const override
Definition: prop_conv.cpp:509
virtual literalt new_variable()=0
virtual literalt convert_bv_rel(const exprt &expr)
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:4893
virtual bvt convert_cond(const cond_exprt &)
Definition: boolbv_cond.cpp:13
mappingt mapping
Definition: boolbv_map.h:59
virtual bvt convert_add_sub(const exprt &expr)
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Definition: std_expr.h:3050
virtual literalt convert_reduction(const unary_exprt &expr)
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: std_expr.h:4589
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1820
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: std_expr.h:3127
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:229
virtual bvt convert_complex_real(const complex_real_exprt &expr)
virtual bvt convert_bswap(const bswap_exprt &expr)
virtual bvt convert_complex(const complex_exprt &expr)
functionst functions
Definition: boolbv.h:98
virtual size_t no_variables() const =0
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:126
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:655
nonstd::optional< T > optionalt
Definition: optional.h:35
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1709
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
Definition: boolbv.cpp:168
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:123
API to expression classes.
virtual bvt convert_floatbv_op(const exprt &expr)
exprt & op1()
Definition: expr.h:87
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: std_expr.h:4523
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: std_expr.h:3225
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:948
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition: boolbv.cpp:562
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
Definition: boolbv.cpp:32
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const exprt & size() const
Definition: std_types.h:1010
virtual void set_frozen(literalt)
Definition: prop.h:111
const namespacet & ns
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
virtual bvt convert_union(const union_exprt &expr)
array_exprt to_array_expr() const
convert string into array constant
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: std_expr.h:4746
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
virtual bvt convert_extractbits(const extractbits_exprt &expr)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1942
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:426
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2378
virtual bvt convert_let(const let_exprt &)
Definition: boolbv_let.cpp:14
std::vector< exprt > operandst
Definition: expr.h:57
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:12
virtual bvt convert_concatenation(const concatenation_exprt &expr)
literalt is_infinity(const bvt &)
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1181
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 &)
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
Definition: popcount.cpp:16
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: std_expr.h:4840
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1519
virtual exprt make_free_bv_expr(const typet &type)
Definition: boolbv.cpp:614
virtual bvt convert_complex_imag(const complex_imag_exprt &expr)
Pre-defined types.
virtual bvt convert_constraint_select_one(const exprt &expr)
void record(const function_application_exprt &function_application)
Definition: functions.cpp:14
unbounded_arrayt unbounded_array
Definition: boolbv.h:78
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2917
exprt & index()
Definition: std_expr.h:1631
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
virtual bvt convert_vector(const vector_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:118
bool literal(const symbol_exprt &expr, literalt &literal) const
Definition: prop_conv.cpp:36
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:2011
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1890
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
irep_idt get_component_name() const
Definition: std_expr.h:3915
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:3328
irept & add(const irep_namet &name)
Definition: irep.cpp:305
virtual bvt convert_member(const member_exprt &expr)
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:414
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:330
void set_frozen(literalt a) override
Definition: prop_conv.h:90
const std::string & id_string() const
Definition: irep.h:262
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:439
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
Definition: boolbv_map.cpp:86
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:810
boolbv_mapt map
Definition: boolbv.h:101
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
virtual bvt convert_div(const div_exprt &expr)
Definition: boolbv_div.cpp:13
virtual exprt make_bv_expr(const typet &type, const bvt &bv)
Definition: boolbv.cpp:603
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
void set_to(const exprt &expr, bool value) override
Definition: boolbv.cpp:593
virtual literalt convert_extractbit(const extractbit_exprt &expr)
const std::size_t MAX_FLATTENED_ARRAY_SIZE
Definition: magic.h:11
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:395
operandst & operands()
Definition: expr.h:78
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:454
virtual literalt convert_quantifier(const quantifier_exprt &expr)
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:2055
bool empty() const
Definition: dstring.h:75
exprt & array()
Definition: std_expr.h:1621
virtual bvt convert_mult(const mult_exprt &expr)
Definition: boolbv_mult.cpp:13
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
std::vector< literalt > bvt
Definition: literal.h:200
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)
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:496
virtual bvt convert_power(const binary_exprt &expr)
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:91
Array index operator.
Definition: std_expr.h:1595