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  const auto &index = index_expr.index();
76  PRECONDITION(index.id() == ID_constant);
77  mp_integer index_int =
78  numeric_cast_v<mp_integer>(to_constant_expr(index));
79 
80  std::size_t offset =
81  numeric_cast_v<std::size_t>(index_int * element_width);
82 
83  return literal(index_expr.array(), bit+offset, dest);
84  }
85  else if(expr.id()==ID_member)
86  {
87  const member_exprt &member_expr=to_member_expr(expr);
88 
89  const struct_typet::componentst &components=
90  to_struct_type(expr.type()).components();
91  const irep_idt &component_name=member_expr.get_component_name();
92 
93  std::size_t offset=0;
94 
95  for(const auto &c : components)
96  {
97  const typet &subtype = c.type();
98 
99  if(c.get_name() == component_name)
100  return literal(member_expr.struct_op(), bit + offset, dest);
101 
102  std::size_t element_width=boolbv_width(subtype);
103  CHECK_RETURN(element_width != 0);
104 
105  offset+=element_width;
106  }
107 
108  INVARIANT(false, "struct type should have accessed component");
109  }
110  }
111 
112  INVARIANT(false, "expression should have a corresponding literal");
113 }
114 
118 const bvt &
120 {
121  // check cache first
122  std::pair<bv_cachet::iterator, bool> cache_result=
123  bv_cache.insert(std::make_pair(expr, bvt()));
124  if(!cache_result.second)
125  {
126  return cache_result.first->second;
127  }
128 
129  // Iterators into hash_maps supposedly stay stable
130  // even though we are inserting more elements recursively.
131 
132  const bvt &bv = convert_bitvector(expr);
133 
135  !expected_width || bv.size() == *expected_width,
136  "bitvector width shall match the indicated expected width",
137  expr.find_source_location(),
139 
140  cache_result.first->second = bv;
141 
142  // check
143  forall_literals(it, cache_result.first->second)
144  {
145  if(freeze_all && !it->is_constant())
146  prop.set_frozen(*it);
147 
149  it->var_no() != literalt::unused_var_no(),
150  "variable number must be different from the unused variable number",
151  expr.find_source_location(),
153  }
154 
155  return cache_result.first->second;
156 }
157 
161 {
162  ignoring(expr);
163 
164  // try to make it free bits
165  std::size_t width=boolbv_width(expr.type());
166  return prop.new_variables(width);
167 }
168 
175 {
176  if(expr.type().id()==ID_bool)
177  {
178  bvt bv;
179  bv.resize(1);
180  bv[0]=convert(expr);
181  return bv;
182  }
183 
184  if(expr.id()==ID_index)
185  return convert_index(to_index_expr(expr));
186  else if(expr.id()==ID_constraint_select_one)
187  return convert_constraint_select_one(expr);
188  else if(expr.id()==ID_member)
189  return convert_member(to_member_expr(expr));
190  else if(expr.id()==ID_with)
191  return convert_with(to_with_expr(expr));
192  else if(expr.id()==ID_update)
193  return convert_update(to_update_expr(expr));
194  else if(expr.id()==ID_width)
195  {
196  std::size_t result_width=boolbv_width(expr.type());
197 
198  if(result_width==0)
199  return conversion_failed(expr);
200 
201  if(expr.operands().size()!=1)
202  return conversion_failed(expr);
203 
204  std::size_t op_width = boolbv_width(to_unary_expr(expr).op().type());
205 
206  if(op_width==0)
207  return conversion_failed(expr);
208 
209  if(expr.type().id()==ID_unsignedbv ||
210  expr.type().id()==ID_signedbv)
211  return bv_utils.build_constant(op_width/8, result_width);
212  }
213  else if(expr.id()==ID_case)
214  return convert_case(expr);
215  else if(expr.id()==ID_cond)
216  return convert_cond(to_cond_expr(expr));
217  else if(expr.id()==ID_if)
218  return convert_if(to_if_expr(expr));
219  else if(expr.id()==ID_constant)
220  return convert_constant(to_constant_expr(expr));
221  else if(expr.id()==ID_typecast)
223  else if(expr.id()==ID_symbol)
224  return convert_symbol(to_symbol_expr(expr));
225  else if(expr.id()==ID_bv_literals)
226  return convert_bv_literals(expr);
227  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
228  expr.id()=="no-overflow-plus" ||
229  expr.id()=="no-overflow-minus")
230  return convert_add_sub(expr);
231  else if(expr.id() == ID_mult)
232  return convert_mult(to_mult_expr(expr));
233  else if(expr.id()==ID_div)
234  return convert_div(to_div_expr(expr));
235  else if(expr.id()==ID_mod)
236  return convert_mod(to_mod_expr(expr));
237  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr ||
238  expr.id()==ID_rol || expr.id()==ID_ror)
239  return convert_shift(to_shift_expr(expr));
240  else if(expr.id()==ID_floatbv_plus || expr.id()==ID_floatbv_minus ||
241  expr.id()==ID_floatbv_mult || expr.id()==ID_floatbv_div ||
242  expr.id()==ID_floatbv_rem)
243  {
245  }
246  else if(expr.id()==ID_floatbv_typecast)
248  else if(expr.id()==ID_concatenation)
250  else if(expr.id()==ID_replication)
252  else if(expr.id()==ID_extractbits)
254  else if(expr.id()==ID_bitnot || expr.id()==ID_bitand ||
255  expr.id()==ID_bitor || expr.id()==ID_bitxor ||
256  expr.id()==ID_bitxnor || expr.id()==ID_bitnor ||
257  expr.id()==ID_bitnand)
258  return convert_bitwise(expr);
259  else if(expr.id() == ID_unary_minus)
261  else if(expr.id()==ID_unary_plus)
262  {
263  return convert_bitvector(to_unary_plus_expr(expr).op());
264  }
265  else if(expr.id()==ID_abs)
266  return convert_abs(to_abs_expr(expr));
267  else if(expr.id() == ID_bswap)
268  return convert_bswap(to_bswap_expr(expr));
269  else if(expr.id()==ID_byte_extract_little_endian ||
270  expr.id()==ID_byte_extract_big_endian)
272  else if(expr.id()==ID_byte_update_little_endian ||
273  expr.id()==ID_byte_update_big_endian)
275  else if(expr.id()==ID_nondet_symbol ||
276  expr.id()=="quant_symbol")
277  return convert_symbol(expr);
278  else if(expr.id()==ID_struct)
279  return convert_struct(to_struct_expr(expr));
280  else if(expr.id()==ID_union)
281  return convert_union(to_union_expr(expr));
282  else if(expr.id()==ID_string_constant)
283  return convert_bitvector(
285  else if(expr.id()==ID_array)
286  return convert_array(expr);
287  else if(expr.id()==ID_vector)
288  return convert_vector(to_vector_expr(expr));
289  else if(expr.id()==ID_complex)
290  return convert_complex(to_complex_expr(expr));
291  else if(expr.id()==ID_complex_real)
293  else if(expr.id()==ID_complex_imag)
295  else if(expr.id() == ID_array_comprehension)
297  else if(expr.id()==ID_array_of)
298  return convert_array_of(to_array_of_expr(expr));
299  else if(expr.id()==ID_let)
300  return convert_let(to_let_expr(expr));
301  else if(expr.id()==ID_function_application)
304  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
305  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
306  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
307  return convert_bv_reduction(to_unary_expr(expr));
308  else if(expr.id()==ID_not)
309  return convert_not(to_not_expr(expr));
310  else if(expr.id()==ID_power)
311  return convert_power(to_binary_expr(expr));
312  else if(expr.id() == ID_popcount)
314 
315  return conversion_failed(expr);
316 }
317 
319 {
320  std::size_t width=boolbv_width(expr.type());
321 
322  if(width==0)
323  return conversion_failed(expr);
324 
325  const exprt &array_size = expr.type().size();
326 
327  const auto size = numeric_cast<mp_integer>(array_size);
328 
329  if(!size.has_value())
330  return conversion_failed(expr);
331 
332  typet counter_type = expr.arg().type();
333 
334  bvt bv;
335  bv.resize(width);
336 
337  for(mp_integer i = 0; i < *size; ++i)
338  {
339  exprt counter=from_integer(i, counter_type);
340 
341  exprt body = expr.body();
342  replace_expr(expr.arg(), counter, body);
343 
344  const bvt &tmp = convert_bv(body);
345 
346  INVARIANT(
347  *size * tmp.size() == width,
348  "total bitvector width shall equal the number of operands times the size "
349  "per operand");
350 
351  std::size_t offset = numeric_cast_v<std::size_t>(i * tmp.size());
352 
353  for(std::size_t j=0; j<tmp.size(); j++)
354  bv[offset+j]=tmp[j];
355  }
356 
357  return bv;
358 }
359 
361 {
362  std::size_t width=boolbv_width(expr.type());
363 
364  if(width==0)
365  return conversion_failed(expr);
366 
367  bvt bv;
368  bv.resize(width);
369 
370  const irept::subt &bv_sub=expr.find(ID_bv).get_sub();
371 
372  if(bv_sub.size()!=width)
373  throw "bv_literals with wrong size";
374 
375  for(std::size_t i=0; i<width; i++)
376  bv[i].set(unsafe_string2unsigned(id2string(bv_sub[i].id())));
377 
378  return bv;
379 }
380 
382 {
383  const typet &type=expr.type();
384  std::size_t width=boolbv_width(type);
385 
386  bvt bv;
387  bv.resize(width);
388 
389  const irep_idt &identifier = expr.get(ID_identifier);
390  CHECK_RETURN(!identifier.empty());
391 
392  if(width==0)
393  {
394  // just put in map
395  map.get_map_entry(identifier, type);
396  }
397  else
398  {
399  map.get_literals(identifier, type, width, bv);
400 
402  std::all_of(
403  bv.begin(),
404  bv.end(),
405  [this](const literalt &l) {
406  return l.var_no() < prop.no_variables() || l.is_constant();
407  }),
408  "variable number of non-constant literals should be within bounds",
409  id2string(identifier));
410  }
411 
412  return bv;
413 }
414 
415 
417  const function_application_exprt &expr)
418 {
419  // record
420  functions.record(expr);
421 
422  // make it free bits
423  return prop.new_variables(boolbv_width(expr.type()));
424 }
425 
426 
428 {
429  PRECONDITION(expr.type().id() == ID_bool);
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  const auto &notequal_expr = to_notequal_expr(expr);
441  return !convert_equality(
442  equal_exprt(notequal_expr.lhs(), notequal_expr.rhs()));
443  }
444  else if(expr.id()==ID_ieee_float_equal ||
445  expr.id()==ID_ieee_float_notequal)
446  {
448  }
449  else if(expr.id()==ID_le || expr.id()==ID_ge ||
450  expr.id()==ID_lt || expr.id()==ID_gt)
451  {
453  }
454  else if(expr.id()==ID_extractbit)
456  else if(expr.id()==ID_forall)
458  else if(expr.id()==ID_exists)
460  else if(expr.id()==ID_let)
461  {
462  bvt bv=convert_let(to_let_expr(expr));
463 
464  DATA_INVARIANT(bv.size()==1,
465  "convert_let must return 1-bit vector for boolean let");
466 
467  return bv[0];
468  }
469  else if(expr.id()==ID_index)
470  {
471  bvt bv=convert_index(to_index_expr(expr));
472  CHECK_RETURN(bv.size() == 1);
473  return bv[0];
474  }
475  else if(expr.id()==ID_member)
476  {
478  CHECK_RETURN(bv.size() == 1);
479  return bv[0];
480  }
481  else if(expr.id()==ID_case)
482  {
483  bvt bv=convert_case(expr);
484  CHECK_RETURN(bv.size() == 1);
485  return bv[0];
486  }
487  else if(expr.id()==ID_cond)
488  {
489  bvt bv = convert_cond(to_cond_expr(expr));
490  CHECK_RETURN(bv.size() == 1);
491  return bv[0];
492  }
493  else if(expr.id()==ID_sign)
494  {
495  const auto &op = to_sign_expr(expr).op();
496  const bvt &bv = convert_bv(op);
497  CHECK_RETURN(!bv.empty());
498  const irep_idt type_id = op.type().id();
499  if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
500  return bv[bv.size()-1];
501  if(type_id == ID_unsignedbv)
502  return const_literal(false);
503  }
504  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
505  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
506  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
507  return convert_reduction(to_unary_expr(expr));
508  else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
509  return convert_onehot(to_unary_expr(expr));
510  else if(has_prefix(expr.id_string(), "overflow-"))
511  return convert_overflow(expr);
512  else if(expr.id()==ID_isnan)
513  {
514  const auto &op = to_unary_expr(expr).op();
515  const bvt &bv = convert_bv(op);
516 
517  if(op.type().id() == ID_floatbv)
518  {
519  float_utilst float_utils(prop, to_floatbv_type(op.type()));
520  return float_utils.is_NaN(bv);
521  }
522  else if(op.type().id() == ID_fixedbv)
523  return const_literal(false);
524  }
525  else if(expr.id()==ID_isfinite)
526  {
527  const auto &op = to_unary_expr(expr).op();
528  const bvt &bv = convert_bv(op);
529 
530  if(op.type().id() == ID_floatbv)
531  {
532  float_utilst float_utils(prop, to_floatbv_type(op.type()));
533  return prop.land(
534  !float_utils.is_infinity(bv),
535  !float_utils.is_NaN(bv));
536  }
537  else if(op.id() == ID_fixedbv)
538  return const_literal(true);
539  }
540  else if(expr.id()==ID_isinf)
541  {
542  const auto &op = to_unary_expr(expr).op();
543  const bvt &bv = convert_bv(op);
544 
545  if(op.type().id() == ID_floatbv)
546  {
547  float_utilst float_utils(prop, to_floatbv_type(op.type()));
548  return float_utils.is_infinity(bv);
549  }
550  else if(op.type().id() == ID_fixedbv)
551  return const_literal(false);
552  }
553  else if(expr.id()==ID_isnormal)
554  {
555  const auto &op = to_unary_expr(expr).op();
556 
557  if(op.type().id() == ID_floatbv)
558  {
559  const bvt &bv = convert_bv(op);
560  float_utilst float_utils(prop, to_floatbv_type(op.type()));
561  return float_utils.is_normal(bv);
562  }
563  else if(op.type().id() == ID_fixedbv)
564  return const_literal(true);
565  }
566 
567  return SUB::convert_rest(expr);
568 }
569 
571 {
573  return true;
574 
575  const typet &type = expr.lhs().type();
576 
577  if(
578  expr.lhs().id() == ID_symbol && type == expr.rhs().type() &&
579  type.id() != ID_bool)
580  {
581  // see if it is an unbounded array
582  if(is_unbounded_array(type))
583  return true;
584 
585  const bvt &bv1=convert_bv(expr.rhs());
586 
587  const irep_idt &identifier=
589 
590  map.set_literals(identifier, type, bv1);
591 
592  if(freeze_all)
593  set_frozen(bv1);
594 
595  return false;
596  }
597 
598  return true;
599 }
600 
601 void boolbvt::set_to(const exprt &expr, bool value)
602 {
603  PRECONDITION(expr.type().id() == ID_bool);
604 
605  const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
606  if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))
607  return;
608  SUB::set_to(expr, value);
609 }
610 
611 exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
612 {
613  exprt dest(ID_bv_literals, type);
614  irept::subt &bv_sub=dest.add(ID_bv).get_sub();
615  bv_sub.resize(bv.size());
616 
617  for(std::size_t i=0; i<bv.size(); i++)
618  bv_sub[i].id(std::to_string(bv[i].get()));
619  return dest;
620 }
621 
623 {
624  const std::size_t width = boolbv_width(type);
625  PRECONDITION(width != 0);
626  bvt bv(width);
627  for(auto &lit : bv)
628  lit = prop.new_variable();
629  return make_bv_expr(type, bv);
630 }
631 
632 bool boolbvt::is_unbounded_array(const typet &type) const
633 {
634  if(type.id()!=ID_array)
635  return false;
636 
638  return true;
639 
640  const exprt &size=to_array_type(type).size();
641 
642  const auto s = numeric_cast<mp_integer>(size);
643  if(!s.has_value())
644  return true;
645 
647  if(*s > MAX_FLATTENED_ARRAY_SIZE)
648  return true;
649 
650  return false;
651 }
652 
653 void boolbvt::print_assignment(std::ostream &out) const
654 {
656  for(const auto &pair : map.mapping)
657  out << pair.first << "=" << pair.second.get_value(prop) << '\n';
658 }
659 
661 {
662  const struct_typet::componentst &components = src.components();
663  offset_mapt dest;
664  dest.reserve(components.size());
665  std::size_t offset = 0;
666  for(const auto &comp : components)
667  {
668  dest.push_back(offset);
669  offset += boolbv_width(comp.type());
670  }
671  return dest;
672 }
to_popcount_expr
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: std_expr.h:4338
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
boolbvt::convert_bv_typecast
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
Definition: boolbv_typecast.cpp:20
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
boolbvt::convert_overflow
virtual literalt convert_overflow(const exprt &expr)
Definition: boolbv_overflow.cpp:15
boolbvt::unbounded_array
unbounded_arrayt unbounded_array
Definition: boolbv.h:81
to_array_comprehension_expr
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:4485
to_vector_expr
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1551
prop_conv_solvert::equality_propagation
bool equality_propagation
Definition: prop_conv_solver.h:76
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:3299
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
boolbvt::map
boolbv_mapt map
Definition: boolbv.h:104
boolbvt::convert_member
virtual bvt convert_member(const member_exprt &expr)
Definition: boolbv_member.cpp:11
boolbvt::convert_bv_rel
virtual literalt convert_bv_rel(const binary_relation_exprt &)
Flatten <, >, <= and >= expressions.
Definition: boolbv_bv_rel.cpp:18
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1080
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:641
boolbvt::convert_byte_update
virtual bvt convert_byte_update(const byte_update_exprt &expr)
Definition: boolbv_byte_update.cpp:20
boolbv_mapt::get_map_entry
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:49
arith_tools.h
mp_arith.h
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1462
boolbvt::convert_array_of
virtual bvt convert_array_of(const array_of_exprt &expr)
Flatten arrays constructed from a single element.
Definition: boolbv_array_of.cpp:16
boolbvt::convert_reduction
virtual literalt convert_reduction(const unary_exprt &expr)
Definition: boolbv_reduction.cpp:12
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
boolbvt::convert_cond
virtual bvt convert_cond(const cond_exprt &)
Definition: boolbv_cond.cpp:13
propt::new_variables
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
boolbvt::convert_bitvector
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:174
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
float_utilst
Definition: float_utils.h:18
typet
The type of an expression, extends irept.
Definition: type.h:29
float_utils.h
bvt
std::vector< literalt > bvt
Definition: literal.h:201
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
threeval.h
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
boolbvt::set_to
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Definition: boolbv.cpp:601
boolbvt::convert_complex
virtual bvt convert_complex(const complex_exprt &expr)
Definition: boolbv_complex.cpp:13
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
MAX_FLATTENED_ARRAY_SIZE
const std::size_t MAX_FLATTENED_ARRAY_SIZE
Definition: magic.h:11
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
boolbv_mapt::get_literals
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
Definition: boolbv_map.cpp:83
boolbvt::convert_mod
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
boolbv_type.h
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1412
boolbvt::convert_vector
virtual bvt convert_vector(const vector_exprt &expr)
Definition: boolbv_vector.cpp:12
prop_conv_solvert::freeze_all
bool freeze_all
Definition: prop_conv_solver.h:77
boolbvt::convert_symbol
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:381
propt::new_variable
virtual literalt new_variable()=0
string_constant.h
boolbvt::convert_index
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
Definition: boolbv_index.cpp:283
exprt
Base class for all expressions.
Definition: expr.h:53
to_complex_expr
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1721
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:631
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
boolbvt::literal
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
Definition: boolbv.cpp:32
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1613
boolbvt::convert_onehot
virtual literalt convert_onehot(const unary_exprt &expr)
Definition: boolbv_onehot.cpp:12
boolbvt::convert_abs
virtual bvt convert_abs(const abs_exprt &expr)
Definition: boolbv_abs.cpp:17
array_comprehension_exprt::arg
const symbol_exprt & arg() const
Definition: std_expr.h:4446
boolbv_mapt::map_entryt::literal_map
literal_mapt literal_map
Definition: boolbv_map.h:50
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
boolbvt::convert_union
virtual bvt convert_union(const union_exprt &expr)
Definition: boolbv_union.cpp:16
boolbvt::convert_case
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
forall_literals
#define forall_literals(it, bv)
Definition: literal.h:203
propt::land
virtual literalt land(literalt a, literalt b)=0
equal_exprt
Equality.
Definition: std_expr.h:1190
magic.h
Magic numbers used throughout the codebase.
array_comprehension_exprt::type
const array_typet & type() const
Definition: std_expr.h:4436
boolbvt::functions
functionst functions
Definition: boolbv.h:101
boolbvt::convert_add_sub
virtual bvt convert_add_sub(const exprt &expr)
Definition: boolbv_add_sub.cpp:16
boolbvt::unbounded_arrayt::U_AUTO
@ U_AUTO
boolbvt::convert_constant
virtual bvt convert_constant(const constant_exprt &expr)
Definition: boolbv_constant.cpp:13
literalt::unused_var_no
static var_not unused_var_no()
Definition: literal.h:176
boolbvt::convert_extractbit
virtual literalt convert_extractbit(const extractbit_exprt &expr)
Definition: boolbv_extractbit.cpp:19
boolbvt::convert_concatenation
virtual bvt convert_concatenation(const concatenation_exprt &expr)
Definition: boolbv_concatenation.cpp:13
prop_conv_solvert::ignoring
virtual void ignoring(const exprt &expr)
Definition: prop_conv_solver.cpp:467
expr_lowering.h
to_unary_plus_expr
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:452
to_complex_real_expr
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1766
float_utilst::is_infinity
literalt is_infinity(const bvt &)
Definition: float_utils.cpp:670
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
INVARIANT_WITH_DIAGNOSTICS
#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:438
to_concatenation_expr
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: std_expr.h:4095
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2543
array_typet::size
const exprt & size() const
Definition: std_types.h:973
boolbvt::convert_mult
virtual bvt convert_mult(const mult_exprt &expr)
Definition: boolbv_mult.cpp:13
boolbvt::convert_shift
virtual bvt convert_shift(const binary_exprt &expr)
Definition: boolbv_shift.cpp:15
boolbv_mapt::map_entryt
Definition: boolbv_map.h:41
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
prop_conv_solvert::literal
bool literal(const symbol_exprt &expr, literalt &literal) const
Definition: prop_conv_solver.cpp:59
prop_conv_solvert::set_frozen
void set_frozen(literalt)
Definition: prop_conv_solver.cpp:27
boolbvt::convert_byte_extract
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
Definition: boolbv_byte_extract.cpp:39
boolbvt::boolbv_set_equality_to_true
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition: boolbv.cpp:570
to_cond_expr
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:4396
boolbvt::convert_array
virtual bvt convert_array(const exprt &expr)
Flatten array.
Definition: boolbv_array.cpp:16
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbv_mapt::mapping
mappingt mapping
Definition: boolbv_map.h:56
float_utilst::is_normal
literalt is_normal(const bvt &)
Definition: float_utils.cpp:219
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1125
functionst::record
void record(const function_application_exprt &function_application)
Definition: functions.cpp:14
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
boolbvt::bv_cache
bv_cachet bv_cache
Definition: boolbv.h:121
boolbvt::convert_bv_literals
virtual bvt convert_bv_literals(const exprt &expr)
Definition: boolbv.cpp:360
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1011
boolbvt::convert_extractbits
virtual bvt convert_extractbits(const extractbits_exprt &expr)
Definition: boolbv_extractbits.cpp:13
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
lower_popcount
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
Definition: popcount.cpp:16
to_replication_expr
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Definition: std_expr.h:4044
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:127
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:231
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
boolbvt::convert_floatbv_typecast
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: boolbv_floatbv_op.cpp:18
boolbvt::convert_verilog_case_equality
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
Definition: boolbv_equality.cpp:60
arrayst::ns
const namespacet & ns
Definition: arrays.h:51
boolbvt::convert_if
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
boolbvt::convert_complex_real
virtual bvt convert_complex_real(const complex_real_exprt &expr)
Definition: boolbv_complex.cpp:41
std_types.h
Pre-defined types.
boolbvt::make_bv_expr
virtual exprt make_bv_expr(const typet &type, const bvt &bv)
Definition: boolbv.cpp:611
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4289
boolbvt::convert_ieee_float_rel
virtual literalt convert_ieee_float_rel(const binary_relation_exprt &)
Definition: boolbv_ieee_float_rel.cpp:17
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
array_comprehension_exprt::body
const exprt & body() const
Definition: std_expr.h:4456
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1273
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:408
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
to_ieee_float_op_expr
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: std_expr.h:3851
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
boolbvt::convert_bv_reduction
virtual bvt convert_bv_reduction(const unary_exprt &expr)
Definition: boolbv_reduction.cpp:53
float_utilst::is_NaN
literalt is_NaN(const bvt &)
Definition: float_utils.cpp:698
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:418
propt::set_frozen
virtual void set_frozen(literalt)
Definition: prop.h:114
dstringt::empty
bool empty() const
Definition: dstring.h:88
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
boolbvt::convert_constraint_select_one
virtual bvt convert_constraint_select_one(const exprt &expr)
Definition: boolbv_constraint_select_one.cpp:12
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:119
boolbvt::convert_bswap
virtual bvt convert_bswap(const bswap_exprt &expr)
Definition: boolbv_bswap.cpp:13
to_complex_imag_expr
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1811
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
to_bswap_expr
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: std_expr.h:515
boolbvt::make_free_bv_expr
virtual exprt make_free_bv_expr(const typet &type)
Definition: boolbv.cpp:622
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:168
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3112
sharing_treet< irept, std::map< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:182
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv_solver.cpp:349
irep_pretty_diagnosticst
Definition: irep.h:524
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
boolbvt::convert_let
virtual bvt convert_let(const let_exprt &)
Definition: boolbv_let.cpp:15
boolbvt::convert_bitwise
virtual bvt convert_bitwise(const exprt &expr)
Definition: boolbv_bitwise.cpp:12
bv_utilst::build_constant
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
boolbvt::convert_floatbv_op
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
Definition: boolbv_floatbv_op.cpp:82
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
boolbvt::convert_struct
virtual bvt convert_struct(const struct_exprt &expr)
Definition: boolbv_struct.cpp:13
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: std_expr.h:2766
to_quantifier_expr
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: mathematical_expr.h:322
to_sign_expr
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:582
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2868
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
to_floatbv_typecast_expr
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2116
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
boolbvt::unbounded_arrayt::U_ALL
@ U_ALL
literalt
Definition: literal.h:26
unsafe_string2unsigned
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:38
irept::get_sub
subt & get_sub()
Definition: irep.h:477
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1230
prop_conv_solvert::print_assignment
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: prop_conv_solver.cpp:527
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
boolbvt::convert_equality
virtual literalt convert_equality(const equal_exprt &expr)
Definition: boolbv_equality.cpp:16
boolbvt::convert_unary_minus
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
Definition: boolbv_unary_minus.cpp:20
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
boolbvt::convert_replication
virtual bvt convert_replication(const replication_exprt &expr)
Definition: boolbv_replication.cpp:13
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
boolbvt::convert_quantifier
virtual literalt convert_quantifier(const quantifier_exprt &expr)
Definition: boolbv_quantifier.cpp:205
boolbv.h
replace_expr.h
exprt::operands
operandst & operands()
Definition: expr.h:95
boolbvt::convert_array_comprehension
virtual bvt convert_array_comprehension(const array_comprehension_exprt &)
Definition: boolbv.cpp:318
index_exprt
Array index operator.
Definition: std_expr.h:1293
boolbvt::convert_not
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:12
boolbvt::convert_typecast
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
Definition: boolbv_typecast.cpp:614
boolbvt::offset_mapt
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:261
boolbvt::build_offset_map
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:660
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:4422
boolbvt::convert_rest
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:427
boolbvt::convert_power
virtual bvt convert_power(const binary_exprt &expr)
Definition: boolbv_power.cpp:12
std_expr.h
API to expression classes.
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:774
boolbvt::convert_function_application
virtual bvt convert_function_application(const function_application_exprt &expr)
Definition: boolbv.cpp:416
boolbvt::convert_div
virtual bvt convert_div(const div_exprt &expr)
Definition: boolbv_div.cpp:13
to_function_application_expr
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: mathematical_expr.h:250
boolbvt::print_assignment
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: boolbv.cpp:653
boolbvt::get
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: boolbv_get.cpp:22
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: std_expr.h:2677
prop_conv_solvert::set_to
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'current_context => expr' if value is true,...
Definition: prop_conv_solver.cpp:540
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1656
validation_modet::INVARIANT
@ INVARIANT
to_abs_expr
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:358
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131
boolbv_mapt::set_literals
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:123
boolbvt::convert_update
virtual bvt convert_update(const update_exprt &)
Definition: boolbv_update.cpp:13
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
boolbvt::convert_with
virtual bvt convert_with(const with_exprt &expr)
Definition: boolbv_with.cpp:18
boolbvt::convert_complex_imag
virtual bvt convert_complex_imag(const complex_imag_exprt &expr)
Definition: boolbv_complex.cpp:55