cprover
smt2_conv.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: SMT Backend
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "smt2_conv.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/bitvector_expr.h>
16 #include <util/c_types.h>
17 #include <util/config.h>
18 #include <util/expr_iterator.h>
19 #include <util/expr_util.h>
20 #include <util/fixedbv.h>
21 #include <util/format_expr.h>
22 #include <util/ieee_float.h>
23 #include <util/invariant.h>
24 #include <util/mathematical_expr.h>
25 #include <util/pointer_expr.h>
27 #include <util/range.h>
28 #include <util/std_expr.h>
29 #include <util/std_types.h>
30 #include <util/string2int.h>
31 #include <util/string_constant.h>
32 
38 
39 // Mark different kinds of error conditions
40 
41 // Unexpected types and other combinations not implemented and not
42 // expected to be needed
43 #define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
44 
45 // General todos
46 #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
47 
49  const namespacet &_ns,
50  const std::string &_benchmark,
51  const std::string &_notes,
52  const std::string &_logic,
53  solvert _solver,
54  std::ostream &_out)
55  : use_FPA_theory(false),
56  use_datatypes(false),
57  use_array_of_bool(false),
58  emit_set_logic(true),
59  ns(_ns),
60  out(_out),
61  benchmark(_benchmark),
62  notes(_notes),
63  logic(_logic),
64  solver(_solver),
65  boolbv_width(_ns),
66  pointer_logic(_ns),
67  no_boolean_variables(0)
68 {
69  // We set some defaults differently
70  // for some solvers.
71 
72  switch(solver)
73  {
74  case solvert::GENERIC:
75  break;
76 
77  case solvert::BOOLECTOR:
78  break;
79 
81  use_array_of_bool = true;
82  emit_set_logic = false;
83  break;
84 
85  case solvert::CVC3:
86  break;
87 
88  case solvert::CVC4:
89  break;
90 
91  case solvert::MATHSAT:
92  break;
93 
94  case solvert::YICES:
95  break;
96 
97  case solvert::Z3:
98  use_array_of_bool = true;
99  emit_set_logic = false;
100  use_datatypes = true;
101  break;
102  }
103 
104  write_header();
105 }
106 
108 {
109  return "SMT2";
110 }
111 
112 void smt2_convt::print_assignment(std::ostream &os) const
113 {
114  // Boolean stuff
115 
116  for(std::size_t v=0; v<boolean_assignment.size(); v++)
117  os << "b" << v << "=" << boolean_assignment[v] << "\n";
118 
119  // others
120 }
121 
123 {
124  if(l.is_true())
125  return tvt(true);
126  if(l.is_false())
127  return tvt(false);
128 
129  INVARIANT(
130  l.var_no() < boolean_assignment.size(),
131  "variable number shall be within bounds");
132  return tvt(boolean_assignment[l.var_no()]^l.sign());
133 }
134 
136 {
137  out << "; SMT 2" << "\n";
138 
139  switch(solver)
140  {
141  // clang-format off
142  case solvert::GENERIC: break;
143  case solvert::BOOLECTOR: out << "; Generated for Boolector\n"; break;
145  out << "; Generated for the CPROVER SMT2 solver\n"; break;
146  case solvert::CVC3: out << "; Generated for CVC 3\n"; break;
147  case solvert::CVC4: out << "; Generated for CVC 4\n"; break;
148  case solvert::MATHSAT: out << "; Generated for MathSAT\n"; break;
149  case solvert::YICES: out << "; Generated for Yices\n"; break;
150  case solvert::Z3: out << "; Generated for Z3\n"; break;
151  // clang-format on
152  }
153 
154  out << "(set-info :source \"" << notes << "\")" << "\n";
155 
156  out << "(set-option :produce-models true)" << "\n";
157 
158  // We use a broad mixture of logics, so on some solvers
159  // its better not to declare here.
160  // set-logic should come after setting options
161  if(emit_set_logic && !logic.empty())
162  out << "(set-logic " << logic << ")" << "\n";
163 }
164 
165 void smt2_convt::write_footer(std::ostream &os)
166 {
167  os << "\n";
168 
169  // add the assumptions, if any
170  if(!assumptions.empty())
171  {
172  os << "; assumptions\n";
173 
174  for(const auto &assumption : assumptions)
175  {
176  os << "(assert ";
177  convert_literal(to_literal_expr(assumption).get_literal());
178  os << ")"
179  << "\n";
180  }
181  }
182 
183  // fix up the object sizes
184  for(const auto &object : object_sizes)
185  define_object_size(object.second, object.first);
186 
187  os << "(check-sat)"
188  << "\n";
189  os << "\n";
190 
192  {
193  for(const auto &id : smt2_identifiers)
194  os << "(get-value (|" << id << "|))"
195  << "\n";
196  }
197 
198  os << "\n";
199 
200  os << "(exit)\n";
201 
202  os << "; end of SMT2 file"
203  << "\n";
204 }
205 
207  const irep_idt &id,
208  const exprt &expr)
209 {
210  PRECONDITION(expr.id() == ID_object_size);
211  const exprt &ptr = to_unary_expr(expr).op();
212  std::size_t size_width = boolbv_width(expr.type());
213  std::size_t pointer_width = boolbv_width(ptr.type());
214  std::size_t number = 0;
215  std::size_t h=pointer_width-1;
216  std::size_t l=pointer_width-config.bv_encoding.object_bits;
217 
218  for(const auto &o : pointer_logic.objects)
219  {
220  const typet &type = o.type();
221  auto size_expr = size_of_expr(type, ns);
222  const auto object_size =
223  numeric_cast<mp_integer>(size_expr.value_or(nil_exprt()));
224 
225  if(
226  (o.id() != ID_symbol && o.id() != ID_string_constant) ||
227  !size_expr.has_value() || !object_size.has_value())
228  {
229  ++number;
230  continue;
231  }
232 
233  out << "(assert (implies (= " <<
234  "((_ extract " << h << " " << l << ") ";
235  convert_expr(ptr);
236  out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))"
237  << "(= " << id << " (_ bv" << *object_size << " " << size_width
238  << "))))\n";
239 
240  ++number;
241  }
242 }
243 
245 {
246  write_footer(out);
247  out.flush();
249 }
250 
251 exprt smt2_convt::get(const exprt &expr) const
252 {
253  if(expr.id()==ID_symbol)
254  {
255  const irep_idt &id=to_symbol_expr(expr).get_identifier();
256 
257  identifier_mapt::const_iterator it=identifier_map.find(id);
258 
259  if(it!=identifier_map.end())
260  return it->second.value;
261  }
262  else if(expr.id()==ID_nondet_symbol)
263  {
265 
266  identifier_mapt::const_iterator it=identifier_map.find(id);
267 
268  if(it!=identifier_map.end())
269  return it->second.value;
270  }
271  else if(expr.id()==ID_member)
272  {
273  const member_exprt &member_expr=to_member_expr(expr);
274  exprt tmp=get(member_expr.struct_op());
275  if(tmp.is_nil())
276  return nil_exprt();
277  return member_exprt(tmp, member_expr.get_component_name(), expr.type());
278  }
279  else if(expr.id() == ID_literal)
280  {
281  auto l = to_literal_expr(expr).get_literal();
282  if(l_get(l).is_true())
283  return true_exprt();
284  else
285  return false_exprt();
286  }
287  else if(expr.id() == ID_not)
288  {
289  auto op = get(to_not_expr(expr).op());
290  if(op.is_true())
291  return false_exprt();
292  else if(op.is_false())
293  return true_exprt();
294  }
295  else if(expr.is_constant())
296  return expr;
297 
298  return nil_exprt();
299 }
300 
302  const irept &src,
303  const typet &type)
304 {
305  // See http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf for the
306  // syntax of SMTlib2 literals.
307  //
308  // A literal expression is one of the following forms:
309  //
310  // * Numeral -- this is a natural number in decimal and is of the form:
311  // 0|([1-9][0-9]*)
312  // * Decimal -- this is a decimal expansion of a real number of the form:
313  // (0|[1-9][0-9]*)[.]([0-9]+)
314  // * Binary -- this is a natural number in binary and is of the form:
315  // #b[01]+
316  // * Hex -- this is a natural number in hexadecimal and is of the form:
317  // #x[0-9a-fA-F]+
318  //
319  // Right now I'm not parsing decimals. It'd be nice if we had a real YACC
320  // parser here, but whatever.
321 
322  mp_integer value;
323 
324  if(!src.id().empty())
325  {
326  const std::string &s=src.id_string();
327 
328  if(s.size()>=2 && s[0]=='#' && s[1]=='b')
329  {
330  // Binary #b010101
331  value=string2integer(s.substr(2), 2);
332  }
333  else if(s.size()>=2 && s[0]=='#' && s[1]=='x')
334  {
335  // Hex #x012345
336  value=string2integer(s.substr(2), 16);
337  }
338  else
339  {
340  // Numeral
341  value=string2integer(s);
342  }
343  }
344  else if(src.get_sub().size()==2 &&
345  src.get_sub()[0].id()=="-") // (- 100)
346  {
347  value=-string2integer(src.get_sub()[1].id_string());
348  }
349  else if(src.get_sub().size()==3 &&
350  src.get_sub()[0].id()=="_" &&
351  // (_ bvDECIMAL_VALUE SIZE)
352  src.get_sub()[1].id_string().substr(0, 2)=="bv")
353  {
354  value=string2integer(src.get_sub()[1].id_string().substr(2));
355  }
356  else if(src.get_sub().size()==4 &&
357  src.get_sub()[0].id()=="fp") // (fp signbv exponentbv significandbv)
358  {
359  if(type.id()==ID_floatbv)
360  {
361  const floatbv_typet &floatbv_type=to_floatbv_type(type);
364  parse_literal(src.get_sub()[2], unsignedbv_typet(floatbv_type.get_e()));
365  constant_exprt s3 =
366  parse_literal(src.get_sub()[3], unsignedbv_typet(floatbv_type.get_f()));
367 
368  const auto s1_int = numeric_cast_v<mp_integer>(s1);
369  const auto s2_int = numeric_cast_v<mp_integer>(s2);
370  const auto s3_int = numeric_cast_v<mp_integer>(s3);
371 
372  // stitch the bits together
373  value = bitwise_or(
374  s1_int << (floatbv_type.get_e() + floatbv_type.get_f()),
375  bitwise_or((s2_int << floatbv_type.get_f()), s3_int));
376  }
377  else
378  value=0;
379  }
380  else if(src.get_sub().size()==4 &&
381  src.get_sub()[0].id()=="_" &&
382  src.get_sub()[1].id()=="+oo") // (_ +oo e s)
383  {
384  std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
385  std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
387  }
388  else if(src.get_sub().size()==4 &&
389  src.get_sub()[0].id()=="_" &&
390  src.get_sub()[1].id()=="-oo") // (_ -oo e s)
391  {
392  std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
393  std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
395  }
396  else if(src.get_sub().size()==4 &&
397  src.get_sub()[0].id()=="_" &&
398  src.get_sub()[1].id()=="NaN") // (_ NaN e s)
399  {
400  std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
401  std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
402  return ieee_floatt::NaN(ieee_float_spect(s, e)).to_expr();
403  }
404 
405  if(type.id()==ID_signedbv ||
406  type.id()==ID_unsignedbv ||
407  type.id()==ID_c_enum ||
408  type.id()==ID_c_bool)
409  {
410  return from_integer(value, type);
411  }
412  else if(type.id()==ID_c_enum_tag)
413  {
414  constant_exprt result =
416 
417  // restore the c_enum_tag type
418  result.type() = type;
419  return result;
420  }
421  else if(type.id()==ID_fixedbv ||
422  type.id()==ID_floatbv)
423  {
424  std::size_t width=boolbv_width(type);
425  return constant_exprt(integer2bvrep(value, width), type);
426  }
427  else if(type.id()==ID_integer ||
428  type.id()==ID_range)
429  {
430  return from_integer(value, type);
431  }
432  else
433  INVARIANT(
434  false,
435  "smt2_convt::parse_literal should not be of unsupported type " +
436  type.id_string());
437 }
438 
440  const irept &src,
441  const array_typet &type)
442 {
443  if(src.get_sub().size()==4 && src.get_sub()[0].id()=="store")
444  {
445  // (store array index value)
446  if(src.get_sub().size()!=4)
447  return nil_exprt();
448 
449  exprt array=parse_array(src.get_sub()[1], type);
450  exprt index=parse_rec(src.get_sub()[2], type.size().type());
451  exprt value=parse_rec(src.get_sub()[3], type.subtype());
452 
453  return with_exprt(array, index, value);
454  }
455  else if(src.get_sub().size()==2 &&
456  src.get_sub()[0].get_sub().size()==3 &&
457  src.get_sub()[0].get_sub()[0].id()=="as" &&
458  src.get_sub()[0].get_sub()[1].id()=="const")
459  {
460  // This is produced by Z3.
461  // ((as const (Array (_ BitVec 64) (_ BitVec 8))) #x00)))
462  exprt value=parse_rec(src.get_sub()[1], type.subtype());
463  return array_of_exprt(value, type);
464  }
465  else
466  return nil_exprt();
467 }
468 
470  const irept &src,
471  const union_typet &type)
472 {
473  // these are always flat
474  PRECONDITION(!type.components().empty());
475  const union_typet::componentt &first=type.components().front();
476  std::size_t width=boolbv_width(type);
477  exprt value = parse_rec(src, unsignedbv_typet(width));
478  if(value.is_nil())
479  return nil_exprt();
480  const typecast_exprt converted(value, first.type());
481  return union_exprt(first.get_name(), converted, type);
482 }
483 
486 {
487  const struct_typet::componentst &components =
488  type.components();
489 
490  struct_exprt result(exprt::operandst(components.size(), nil_exprt()), type);
491 
492  if(components.empty())
493  return result;
494 
495  if(use_datatypes)
496  {
497  // Structs look like:
498  // (mk-struct.1 <component0> <component1> ... <componentN>)
499 
500  if(src.get_sub().size()!=components.size()+1)
501  return result; // give up
502 
503  for(std::size_t i=0; i<components.size(); i++)
504  {
505  const struct_typet::componentt &c=components[i];
506  result.operands()[i]=parse_rec(src.get_sub()[i+1], c.type());
507  }
508  }
509  else
510  {
511  // These are just flattened, i.e., we expect to see a monster bit vector.
512  std::size_t total_width=boolbv_width(type);
513  const auto l = parse_literal(src, unsignedbv_typet(total_width));
514 
515  const irep_idt binary =
516  integer2binary(numeric_cast_v<mp_integer>(l), total_width);
517 
518  CHECK_RETURN(binary.size() == total_width);
519 
520  std::size_t offset=0;
521 
522  for(std::size_t i=0; i<components.size(); i++)
523  {
524  std::size_t component_width=boolbv_width(components[i].type());
525 
526  INVARIANT(
527  offset + component_width <= total_width,
528  "struct component bits shall be within struct bit vector");
529 
530  std::string component_binary=
531  "#b"+id2string(binary).substr(
532  total_width-offset-component_width, component_width);
533 
534  result.operands()[i]=
535  parse_rec(irept(component_binary), components[i].type());
536 
537  offset+=component_width;
538  }
539  }
540 
541  return result;
542 }
543 
544 exprt smt2_convt::parse_rec(const irept &src, const typet &type)
545 {
546  if(
547  type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
548  type.id() == ID_integer || type.id() == ID_rational ||
549  type.id() == ID_real || type.id() == ID_c_enum ||
550  type.id() == ID_c_enum_tag || type.id() == ID_fixedbv ||
551  type.id() == ID_floatbv)
552  {
553  return parse_literal(src, type);
554  }
555  else if(type.id()==ID_bool)
556  {
557  if(src.id()==ID_1 || src.id()==ID_true)
558  return true_exprt();
559  else if(src.id()==ID_0 || src.id()==ID_false)
560  return false_exprt();
561  }
562  else if(type.id()==ID_pointer)
563  {
564  // these come in as bit-vector literals
565  std::size_t width=boolbv_width(type);
566  constant_exprt bv_expr = parse_literal(src, unsignedbv_typet(width));
567 
568  mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
569 
570  // split into object and offset
573  ptr.object = numeric_cast_v<std::size_t>(v / pow);
574  ptr.offset=v%pow;
575  return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
576  }
577  else if(type.id()==ID_struct)
578  {
579  return parse_struct(src, to_struct_type(type));
580  }
581  else if(type.id() == ID_struct_tag)
582  {
583  auto struct_expr =
585  // restore the tag type
586  struct_expr.type() = type;
587  return std::move(struct_expr);
588  }
589  else if(type.id()==ID_union)
590  {
591  return parse_union(src, to_union_type(type));
592  }
593  else if(type.id() == ID_union_tag)
594  {
595  auto union_expr = parse_union(src, ns.follow_tag(to_union_tag_type(type)));
596  // restore the tag type
597  union_expr.type() = type;
598  return union_expr;
599  }
600  else if(type.id()==ID_array)
601  {
602  return parse_array(src, to_array_type(type));
603  }
604 
605  return nil_exprt();
606 }
607 
609  const exprt &expr,
610  const pointer_typet &result_type)
611 {
612  if(expr.id()==ID_symbol ||
613  expr.id()==ID_constant ||
614  expr.id()==ID_string_constant ||
615  expr.id()==ID_label)
616  {
617  out
618  << "(concat (_ bv"
619  << pointer_logic.add_object(expr) << " "
620  << config.bv_encoding.object_bits << ")"
621  << " (_ bv0 "
622  << boolbv_width(result_type)-config.bv_encoding.object_bits << "))";
623  }
624  else if(expr.id()==ID_index)
625  {
626  const index_exprt &index_expr = to_index_expr(expr);
627 
628  const exprt &array = index_expr.array();
629  const exprt &index = index_expr.index();
630 
631  if(index.is_zero())
632  {
633  if(array.type().id()==ID_pointer)
634  convert_expr(array);
635  else if(array.type().id()==ID_array)
636  convert_address_of_rec(array, result_type);
637  else
638  UNREACHABLE;
639  }
640  else
641  {
642  // this is really pointer arithmetic
643  index_exprt new_index_expr = index_expr;
644  new_index_expr.index() = from_integer(0, index.type());
645 
646  address_of_exprt address_of_expr(
647  new_index_expr,
648  pointer_type(array.type().subtype()));
649 
650  plus_exprt plus_expr{address_of_expr, index};
651 
652  convert_expr(plus_expr);
653  }
654  }
655  else if(expr.id()==ID_member)
656  {
657  const member_exprt &member_expr=to_member_expr(expr);
658 
659  const exprt &struct_op=member_expr.struct_op();
660  const typet &struct_op_type = struct_op.type();
661 
663  struct_op_type.id() == ID_struct || struct_op_type.id() == ID_struct_tag,
664  "member expression operand shall have struct type");
665 
666  const struct_typet &struct_type = to_struct_type(ns.follow(struct_op_type));
667 
668  const irep_idt &component_name = member_expr.get_component_name();
669 
670  const auto offset = member_offset(struct_type, component_name, ns);
671  CHECK_RETURN(offset.has_value() && *offset >= 0);
672 
674 
675  // pointer arithmetic
676  out << "(bvadd ";
677  convert_address_of_rec(struct_op, result_type);
679  out << ")"; // bvadd
680  }
681  else if(expr.id()==ID_if)
682  {
683  const if_exprt &if_expr = to_if_expr(expr);
684 
685  out << "(ite ";
686  convert_expr(if_expr.cond());
687  out << " ";
688  convert_address_of_rec(if_expr.true_case(), result_type);
689  out << " ";
690  convert_address_of_rec(if_expr.false_case(), result_type);
691  out << ")";
692  }
693  else
694  INVARIANT(
695  false,
696  "operand of address of expression should not be of kind " +
697  expr.id_string());
698 }
699 
701 {
702  PRECONDITION(expr.type().id() == ID_bool);
703 
704  // Three cases where no new handle is needed.
705 
706  if(expr.is_true())
707  return const_literal(true);
708  else if(expr.is_false())
709  return const_literal(false);
710  else if(expr.id()==ID_literal)
711  return to_literal_expr(expr).get_literal();
712 
713  // Need a new handle
714 
715  out << "\n";
716 
717  exprt prepared_expr = prepare_for_convert_expr(expr);
718 
719  literalt l(no_boolean_variables, false);
721 
722  out << "; convert\n";
723  out << "(define-fun ";
724  convert_literal(l);
725  out << " () Bool ";
726  convert_expr(prepared_expr);
727  out << ")" << "\n";
728 
729  return l;
730 }
731 
733 {
734  // We can only improve Booleans.
735  if(expr.type().id() != ID_bool)
736  return expr;
737 
738  return literal_exprt(convert(expr));
739 }
740 
742 {
743  if(l==const_literal(false))
744  out << "false";
745  else if(l==const_literal(true))
746  out << "true";
747  else
748  {
749  if(l.sign())
750  out << "(not ";
751 
752  out << "|B" << l.var_no() << "|";
753 
754  if(l.sign())
755  out << ")";
756 
757  smt2_identifiers.insert("B"+std::to_string(l.var_no()));
758  }
759 }
760 
762 {
764 }
765 
766 void smt2_convt::push(const std::vector<exprt> &_assumptions)
767 {
768  INVARIANT(assumptions.empty(), "nested contexts are not supported");
769 
770  assumptions = _assumptions;
771 }
772 
774 {
775  assumptions.clear();
776 }
777 
778 std::string smt2_convt::convert_identifier(const irep_idt &identifier)
779 {
780  // Backslashes are disallowed in quoted symbols just for simplicity.
781  // Otherwise, for Common Lisp compatibility they would have to be treated
782  // as escaping symbols.
783 
784  std::string result;
785 
786  for(std::size_t i=0; i<identifier.size(); i++)
787  {
788  char ch=identifier[i];
789 
790  switch(ch)
791  {
792  case '|':
793  case '\\':
794  case '&': // we use the & for escaping
795  result+='&';
796  result+=std::to_string(ch);
797  result+=';';
798  break;
799 
800  case '$': // $ _is_ allowed
801  default:
802  result+=ch;
803  }
804  }
805 
806  return result;
807 }
808 
809 std::string smt2_convt::type2id(const typet &type) const
810 {
811  if(type.id()==ID_floatbv)
812  {
813  ieee_float_spect spec(to_floatbv_type(type));
814  return "f"+std::to_string(spec.width())+"_"+std::to_string(spec.f);
815  }
816  else if(type.id()==ID_unsignedbv)
817  {
818  return "u"+std::to_string(to_unsignedbv_type(type).get_width());
819  }
820  else if(type.id()==ID_c_bool)
821  {
822  return "u"+std::to_string(to_c_bool_type(type).get_width());
823  }
824  else if(type.id()==ID_signedbv)
825  {
826  return "s"+std::to_string(to_signedbv_type(type).get_width());
827  }
828  else if(type.id()==ID_bool)
829  {
830  return "b";
831  }
832  else if(type.id()==ID_c_enum_tag)
833  {
834  return type2id(ns.follow_tag(to_c_enum_tag_type(type)).subtype());
835  }
836  else if(type.id() == ID_pointer)
837  {
838  return "p" + std::to_string(to_pointer_type(type).get_width());
839  }
840  else
841  {
842  UNREACHABLE;
843  }
844 }
845 
846 std::string smt2_convt::floatbv_suffix(const exprt &expr) const
847 {
848  PRECONDITION(!expr.operands().empty());
849  return "_" + type2id(to_multi_ary_expr(expr).op0().type()) + "->" +
850  type2id(expr.type());
851 }
852 
854 {
856 
857  if(expr.id()==ID_symbol)
858  {
859  const irep_idt &id = to_symbol_expr(expr).get_identifier();
860  out << '|' << convert_identifier(id) << '|';
861  return;
862  }
863 
864  if(expr.id()==ID_smt2_symbol)
865  {
866  const irep_idt &id = to_smt2_symbol(expr).get_identifier();
867  out << id;
868  return;
869  }
870 
871  INVARIANT(
872  !expr.operands().empty(), "non-symbol expressions shall have operands");
873 
874  out << "(|float_bv." << expr.id()
875  << floatbv_suffix(expr)
876  << '|';
877 
878  forall_operands(it, expr)
879  {
880  out << ' ';
881  convert_expr(*it);
882  }
883 
884  out << ')';
885 }
886 
888 {
889  // huge monster case split over expression id
890  if(expr.id()==ID_symbol)
891  {
892  const irep_idt &id = to_symbol_expr(expr).get_identifier();
893  DATA_INVARIANT(!id.empty(), "symbol must have identifier");
894  out << '|' << convert_identifier(id) << '|';
895  }
896  else if(expr.id()==ID_nondet_symbol)
897  {
898  const irep_idt &id = to_nondet_symbol_expr(expr).get_identifier();
899  DATA_INVARIANT(!id.empty(), "nondet symbol must have identifier");
900  out << '|' << convert_identifier("nondet_"+id2string(id)) << '|';
901  }
902  else if(expr.id()==ID_smt2_symbol)
903  {
904  const irep_idt &id = to_smt2_symbol(expr).get_identifier();
905  DATA_INVARIANT(!id.empty(), "smt2 symbol must have identifier");
906  out << id;
907  }
908  else if(expr.id()==ID_typecast)
909  {
911  }
912  else if(expr.id()==ID_floatbv_typecast)
913  {
915  }
916  else if(expr.id()==ID_struct)
917  {
919  }
920  else if(expr.id()==ID_union)
921  {
923  }
924  else if(expr.id()==ID_constant)
925  {
927  }
928  else if(expr.id() == ID_concatenation && expr.operands().size() == 1)
929  {
931  expr.type() == expr.operands().front().type(),
932  "concatenation over a single operand should have matching types",
933  expr.pretty());
934 
935  convert_expr(expr.operands().front());
936  }
937  else if(expr.id()==ID_concatenation ||
938  expr.id()==ID_bitand ||
939  expr.id()==ID_bitor ||
940  expr.id()==ID_bitxor ||
941  expr.id()==ID_bitnand ||
942  expr.id()==ID_bitnor)
943  {
945  expr.operands().size() >= 2,
946  "given expression should have at least two operands",
947  expr.id_string());
948 
949  out << "(";
950 
951  if(expr.id()==ID_concatenation)
952  out << "concat";
953  else if(expr.id()==ID_bitand)
954  out << "bvand";
955  else if(expr.id()==ID_bitor)
956  out << "bvor";
957  else if(expr.id()==ID_bitxor)
958  out << "bvxor";
959  else if(expr.id()==ID_bitnand)
960  out << "bvnand";
961  else if(expr.id()==ID_bitnor)
962  out << "bvnor";
963 
964  forall_operands(it, expr)
965  {
966  out << " ";
967  flatten2bv(*it);
968  }
969 
970  out << ")";
971  }
972  else if(expr.id()==ID_bitnot)
973  {
974  const bitnot_exprt &bitnot_expr = to_bitnot_expr(expr);
975 
976  if(bitnot_expr.type().id() == ID_vector)
977  {
978  if(use_datatypes)
979  {
980  const std::string &smt_typename = datatype_map.at(bitnot_expr.type());
981 
982  // extract elements
983  const vector_typet &vector_type = to_vector_type(bitnot_expr.type());
984 
985  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
986 
987  out << "(let ((?vectorop ";
988  convert_expr(bitnot_expr.op());
989  out << ")) ";
990 
991  out << "(mk-" << smt_typename;
992 
993  typet index_type=vector_type.size().type();
994 
995  // do bitnot component-by-component
996  for(mp_integer i=0; i!=size; ++i)
997  {
998  out << " (bvnot (" << smt_typename << "." << (size-i-1)
999  << " ?vectorop))";
1000  }
1001 
1002  out << "))"; // mk-, let
1003  }
1004  else
1005  SMT2_TODO("bitnot for vectors");
1006  }
1007  else
1008  {
1009  out << "(bvnot ";
1010  convert_expr(bitnot_expr.op());
1011  out << ")";
1012  }
1013  }
1014  else if(expr.id()==ID_unary_minus)
1015  {
1016  const unary_minus_exprt &unary_minus_expr = to_unary_minus_expr(expr);
1017 
1018  if(
1019  unary_minus_expr.type().id() == ID_rational ||
1020  unary_minus_expr.type().id() == ID_integer ||
1021  unary_minus_expr.type().id() == ID_real)
1022  {
1023  out << "(- ";
1024  convert_expr(unary_minus_expr.op());
1025  out << ")";
1026  }
1027  else if(unary_minus_expr.type().id() == ID_floatbv)
1028  {
1029  // this has no rounding mode
1030  if(use_FPA_theory)
1031  {
1032  out << "(fp.neg ";
1033  convert_expr(unary_minus_expr.op());
1034  out << ")";
1035  }
1036  else
1037  convert_floatbv(unary_minus_expr);
1038  }
1039  else if(unary_minus_expr.type().id() == ID_vector)
1040  {
1041  if(use_datatypes)
1042  {
1043  const std::string &smt_typename =
1044  datatype_map.at(unary_minus_expr.type());
1045 
1046  // extract elements
1047  const vector_typet &vector_type =
1048  to_vector_type(unary_minus_expr.type());
1049 
1050  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
1051 
1052  out << "(let ((?vectorop ";
1053  convert_expr(unary_minus_expr.op());
1054  out << ")) ";
1055 
1056  out << "(mk-" << smt_typename;
1057 
1058  typet index_type=vector_type.size().type();
1059 
1060  // negate component-by-component
1061  for(mp_integer i=0; i!=size; ++i)
1062  {
1063  out << " (bvneg (" << smt_typename << "." << (size-i-1)
1064  << " ?vectorop))";
1065  }
1066 
1067  out << "))"; // mk-, let
1068  }
1069  else
1070  SMT2_TODO("unary minus for vector");
1071  }
1072  else
1073  {
1074  out << "(bvneg ";
1075  convert_expr(unary_minus_expr.op());
1076  out << ")";
1077  }
1078  }
1079  else if(expr.id()==ID_unary_plus)
1080  {
1081  // A no-op (apart from type promotion)
1082  convert_expr(to_unary_plus_expr(expr).op());
1083  }
1084  else if(expr.id()==ID_sign)
1085  {
1086  const sign_exprt &sign_expr = to_sign_expr(expr);
1087 
1088  const typet &op_type = sign_expr.op().type();
1089 
1090  if(op_type.id()==ID_floatbv)
1091  {
1092  if(use_FPA_theory)
1093  {
1094  out << "(fp.isNegative ";
1095  convert_expr(sign_expr.op());
1096  out << ")";
1097  }
1098  else
1099  convert_floatbv(sign_expr);
1100  }
1101  else if(op_type.id()==ID_signedbv)
1102  {
1103  std::size_t op_width=to_signedbv_type(op_type).get_width();
1104 
1105  out << "(bvslt ";
1106  convert_expr(sign_expr.op());
1107  out << " (_ bv0 " << op_width << "))";
1108  }
1109  else
1111  false,
1112  "sign should not be applied to unsupported type",
1113  sign_expr.type().id_string());
1114  }
1115  else if(expr.id()==ID_if)
1116  {
1117  const if_exprt &if_expr = to_if_expr(expr);
1118 
1119  out << "(ite ";
1120  convert_expr(if_expr.cond());
1121  out << " ";
1122  convert_expr(if_expr.true_case());
1123  out << " ";
1124  convert_expr(if_expr.false_case());
1125  out << ")";
1126  }
1127  else if(expr.id()==ID_and ||
1128  expr.id()==ID_or ||
1129  expr.id()==ID_xor)
1130  {
1132  expr.type().id() == ID_bool,
1133  "logical and, or, and xor expressions should have Boolean type");
1135  expr.operands().size() >= 2,
1136  "logical and, or, and xor expressions should have at least two operands");
1137 
1138  out << "(" << expr.id();
1139  forall_operands(it, expr)
1140  {
1141  out << " ";
1142  convert_expr(*it);
1143  }
1144  out << ")";
1145  }
1146  else if(expr.id()==ID_implies)
1147  {
1148  const implies_exprt &implies_expr = to_implies_expr(expr);
1149 
1151  implies_expr.type().id() == ID_bool,
1152  "implies expression should have Boolean type");
1153 
1154  out << "(=> ";
1155  convert_expr(implies_expr.op0());
1156  out << " ";
1157  convert_expr(implies_expr.op1());
1158  out << ")";
1159  }
1160  else if(expr.id()==ID_not)
1161  {
1162  const not_exprt &not_expr = to_not_expr(expr);
1163 
1165  not_expr.type().id() == ID_bool,
1166  "not expression should have Boolean type");
1167 
1168  out << "(not ";
1169  convert_expr(not_expr.op());
1170  out << ")";
1171  }
1172  else if(expr.id() == ID_equal)
1173  {
1174  const equal_exprt &equal_expr = to_equal_expr(expr);
1175 
1177  equal_expr.op0().type() == equal_expr.op1().type(),
1178  "operands of equal expression shall have same type");
1179 
1180  out << "(= ";
1181  convert_expr(equal_expr.op0());
1182  out << " ";
1183  convert_expr(equal_expr.op1());
1184  out << ")";
1185  }
1186  else if(expr.id() == ID_notequal)
1187  {
1188  const notequal_exprt &notequal_expr = to_notequal_expr(expr);
1189 
1191  notequal_expr.op0().type() == notequal_expr.op1().type(),
1192  "operands of not equal expression shall have same type");
1193 
1194  out << "(not (= ";
1195  convert_expr(notequal_expr.op0());
1196  out << " ";
1197  convert_expr(notequal_expr.op1());
1198  out << "))";
1199  }
1200  else if(expr.id()==ID_ieee_float_equal ||
1201  expr.id()==ID_ieee_float_notequal)
1202  {
1203  // These are not the same as (= A B)
1204  // because of NaN and negative zero.
1205  const auto &rel_expr = to_binary_relation_expr(expr);
1206 
1208  rel_expr.lhs().type() == rel_expr.rhs().type(),
1209  "operands of float equal and not equal expressions shall have same type");
1210 
1211  // The FPA theory properly treats NaN and negative zero.
1212  if(use_FPA_theory)
1213  {
1214  if(rel_expr.id() == ID_ieee_float_notequal)
1215  out << "(not ";
1216 
1217  out << "(fp.eq ";
1218  convert_expr(rel_expr.lhs());
1219  out << " ";
1220  convert_expr(rel_expr.rhs());
1221  out << ")";
1222 
1223  if(rel_expr.id() == ID_ieee_float_notequal)
1224  out << ")";
1225  }
1226  else
1227  convert_floatbv(expr);
1228  }
1229  else if(expr.id()==ID_le ||
1230  expr.id()==ID_lt ||
1231  expr.id()==ID_ge ||
1232  expr.id()==ID_gt)
1233  {
1235  }
1236  else if(expr.id()==ID_plus)
1237  {
1238  convert_plus(to_plus_expr(expr));
1239  }
1240  else if(expr.id()==ID_floatbv_plus)
1241  {
1243  }
1244  else if(expr.id()==ID_minus)
1245  {
1247  }
1248  else if(expr.id()==ID_floatbv_minus)
1249  {
1251  }
1252  else if(expr.id()==ID_div)
1253  {
1254  convert_div(to_div_expr(expr));
1255  }
1256  else if(expr.id()==ID_floatbv_div)
1257  {
1259  }
1260  else if(expr.id()==ID_mod)
1261  {
1262  convert_mod(to_mod_expr(expr));
1263  }
1264  else if(expr.id()==ID_mult)
1265  {
1266  convert_mult(to_mult_expr(expr));
1267  }
1268  else if(expr.id()==ID_floatbv_mult)
1269  {
1271  }
1272  else if(expr.id()==ID_address_of)
1273  {
1274  const address_of_exprt &address_of_expr = to_address_of_expr(expr);
1276  address_of_expr.object(), to_pointer_type(address_of_expr.type()));
1277  }
1278  else if(expr.id()==ID_array_of)
1279  {
1280  const array_of_exprt &array_of_expr = to_array_of_expr(expr);
1281 
1283  array_of_expr.type().id() == ID_array,
1284  "array of expression shall have array type");
1285 
1286  defined_expressionst::const_iterator it =
1287  defined_expressions.find(array_of_expr);
1288  CHECK_RETURN(it != defined_expressions.end());
1289  out << it->second;
1290  }
1291  else if(expr.id()==ID_index)
1292  {
1294  }
1295  else if(expr.id()==ID_ashr ||
1296  expr.id()==ID_lshr ||
1297  expr.id()==ID_shl)
1298  {
1299  const shift_exprt &shift_expr = to_shift_expr(expr);
1300  const typet &type = shift_expr.type();
1301 
1302  if(type.id()==ID_unsignedbv ||
1303  type.id()==ID_signedbv ||
1304  type.id()==ID_bv)
1305  {
1306  if(shift_expr.id() == ID_ashr)
1307  out << "(bvashr ";
1308  else if(shift_expr.id() == ID_lshr)
1309  out << "(bvlshr ";
1310  else if(shift_expr.id() == ID_shl)
1311  out << "(bvshl ";
1312  else
1313  UNREACHABLE;
1314 
1315  convert_expr(shift_expr.op());
1316  out << " ";
1317 
1318  // SMT2 requires the shift distance to have the same width as
1319  // the value that is shifted -- odd!
1320 
1321  if(shift_expr.distance().type().id() == ID_integer)
1322  {
1323  const mp_integer i =
1324  numeric_cast_v<mp_integer>(to_constant_expr(shift_expr.distance()));
1325 
1326  // shift distance must be bit vector
1327  std::size_t width_op0 = boolbv_width(shift_expr.op().type());
1328  exprt tmp=from_integer(i, unsignedbv_typet(width_op0));
1329  convert_expr(tmp);
1330  }
1331  else if(
1332  shift_expr.distance().type().id() == ID_signedbv ||
1333  shift_expr.distance().type().id() == ID_unsignedbv ||
1334  shift_expr.distance().type().id() == ID_c_enum ||
1335  shift_expr.distance().type().id() == ID_c_bool)
1336  {
1337  std::size_t width_op0 = boolbv_width(shift_expr.op().type());
1338  std::size_t width_op1 = boolbv_width(shift_expr.distance().type());
1339 
1340  if(width_op0==width_op1)
1341  convert_expr(shift_expr.distance());
1342  else if(width_op0>width_op1)
1343  {
1344  out << "((_ zero_extend " << width_op0-width_op1 << ") ";
1345  convert_expr(shift_expr.distance());
1346  out << ")"; // zero_extend
1347  }
1348  else // width_op0<width_op1
1349  {
1350  out << "((_ extract " << width_op0-1 << " 0) ";
1351  convert_expr(shift_expr.distance());
1352  out << ")"; // extract
1353  }
1354  }
1355  else
1357  "unsupported distance type for " + shift_expr.id_string() + ": " +
1358  type.id_string());
1359 
1360  out << ")"; // bv*sh
1361  }
1362  else
1364  "unsupported type for " + shift_expr.id_string() + ": " +
1365  type.id_string());
1366  }
1367  else if(expr.id() == ID_rol || expr.id() == ID_ror)
1368  {
1369  const shift_exprt &shift_expr = to_shift_expr(expr);
1370  const typet &type = shift_expr.type();
1371 
1372  if(
1373  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
1374  type.id() == ID_bv)
1375  {
1376  // SMT-LIB offers rotate_left and rotate_right, but these require a
1377  // constant distance.
1378  if(shift_expr.id() == ID_rol)
1379  out << "((_ rotate_left";
1380  else if(shift_expr.id() == ID_ror)
1381  out << "((_ rotate_right";
1382  else
1383  UNREACHABLE;
1384 
1385  out << ' ';
1386 
1387  auto distance_int_op = numeric_cast<mp_integer>(shift_expr.distance());
1388 
1389  if(distance_int_op.has_value())
1390  {
1391  out << distance_int_op.value();
1392  }
1393  else
1395  "distance type for " + shift_expr.id_string() + "must be constant");
1396 
1397  out << ") ";
1398  convert_expr(shift_expr.op());
1399 
1400  out << ")"; // rotate_*
1401  }
1402  else
1404  "unsupported type for " + shift_expr.id_string() + ": " +
1405  type.id_string());
1406  }
1407  else if(expr.id()==ID_with)
1408  {
1409  convert_with(to_with_expr(expr));
1410  }
1411  else if(expr.id()==ID_update)
1412  {
1413  convert_update(expr);
1414  }
1415  else if(expr.id()==ID_member)
1416  {
1418  }
1419  else if(expr.id()==ID_pointer_offset)
1420  {
1421  const auto &op = to_unary_expr(expr).op();
1422 
1424  op.type().id() == ID_pointer,
1425  "operand of pointer offset expression shall be of pointer type");
1426 
1427  std::size_t offset_bits =
1429  std::size_t result_width=boolbv_width(expr.type());
1430 
1431  // max extract width
1432  if(offset_bits>result_width)
1433  offset_bits=result_width;
1434 
1435  // too few bits?
1436  if(result_width>offset_bits)
1437  out << "((_ zero_extend " << result_width-offset_bits << ") ";
1438 
1439  out << "((_ extract " << offset_bits-1 << " 0) ";
1440  convert_expr(op);
1441  out << ")";
1442 
1443  if(result_width>offset_bits)
1444  out << ")"; // zero_extend
1445  }
1446  else if(expr.id()==ID_pointer_object)
1447  {
1448  const auto &op = to_unary_expr(expr).op();
1449 
1451  op.type().id() == ID_pointer,
1452  "pointer object expressions should be of pointer type");
1453 
1454  std::size_t ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
1455  std::size_t pointer_width = boolbv_width(op.type());
1456 
1457  if(ext>0)
1458  out << "((_ zero_extend " << ext << ") ";
1459 
1460  out << "((_ extract "
1461  << pointer_width-1 << " "
1462  << pointer_width-config.bv_encoding.object_bits << ") ";
1463  convert_expr(op);
1464  out << ")";
1465 
1466  if(ext>0)
1467  out << ")"; // zero_extend
1468  }
1469  else if(expr.id() == ID_is_dynamic_object)
1470  {
1472  }
1473  else if(expr.id() == ID_is_invalid_pointer)
1474  {
1475  const auto &op = to_unary_expr(expr).op();
1476  std::size_t pointer_width = boolbv_width(op.type());
1477  out << "(= ((_ extract "
1478  << pointer_width-1 << " "
1479  << pointer_width-config.bv_encoding.object_bits << ") ";
1480  convert_expr(op);
1481  out << ") (_ bv" << pointer_logic.get_invalid_object()
1482  << " " << config.bv_encoding.object_bits << "))";
1483  }
1484  else if(expr.id()==ID_string_constant)
1485  {
1486  defined_expressionst::const_iterator it=defined_expressions.find(expr);
1487  CHECK_RETURN(it != defined_expressions.end());
1488  out << it->second;
1489  }
1490  else if(expr.id()==ID_extractbit)
1491  {
1492  const extractbit_exprt &extractbit_expr = to_extractbit_expr(expr);
1493 
1494  if(extractbit_expr.index().is_constant())
1495  {
1496  const mp_integer i =
1497  numeric_cast_v<mp_integer>(to_constant_expr(extractbit_expr.index()));
1498 
1499  out << "(= ((_ extract " << i << " " << i << ") ";
1500  flatten2bv(extractbit_expr.src());
1501  out << ") #b1)";
1502  }
1503  else
1504  {
1505  out << "(= ((_ extract 0 0) ";
1506  // the arguments of the shift need to have the same width
1507  out << "(bvlshr ";
1508  flatten2bv(extractbit_expr.src());
1509  typecast_exprt tmp(extractbit_expr.index(), extractbit_expr.src().type());
1510  convert_expr(tmp);
1511  out << ")) bin1)"; // bvlshr, extract, =
1512  }
1513  }
1514  else if(expr.id()==ID_extractbits)
1515  {
1516  const extractbits_exprt &extractbits_expr = to_extractbits_expr(expr);
1517 
1518  if(
1519  extractbits_expr.upper().is_constant() &&
1520  extractbits_expr.lower().is_constant())
1521  {
1522  mp_integer op1_i =
1523  numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.upper()));
1524  mp_integer op2_i =
1525  numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.lower()));
1526 
1527  if(op2_i>op1_i)
1528  std::swap(op1_i, op2_i);
1529 
1530  // now op1_i>=op2_i
1531 
1532  out << "((_ extract " << op1_i << " " << op2_i << ") ";
1533  flatten2bv(extractbits_expr.src());
1534  out << ")";
1535  }
1536  else
1537  {
1538  #if 0
1539  out << "(= ((_ extract 0 0) ";
1540  // the arguments of the shift need to have the same width
1541  out << "(bvlshr ";
1542  convert_expr(expr.op0());
1543  typecast_exprt tmp(expr.op0().type());
1544  tmp.op0()=expr.op1();
1545  convert_expr(tmp);
1546  out << ")) bin1)"; // bvlshr, extract, =
1547  #endif
1548  SMT2_TODO("smt2: extractbits with non-constant index");
1549  }
1550  }
1551  else if(expr.id()==ID_replication)
1552  {
1553  const replication_exprt &replication_expr = to_replication_expr(expr);
1554 
1555  mp_integer times = numeric_cast_v<mp_integer>(replication_expr.times());
1556 
1557  out << "((_ repeat " << times << ") ";
1558  flatten2bv(replication_expr.op());
1559  out << ")";
1560  }
1561  else if(expr.id()==ID_byte_extract_little_endian ||
1562  expr.id()==ID_byte_extract_big_endian)
1563  {
1564  INVARIANT(
1565  false, "byte_extract ops should be lowered in prepare_for_convert_expr");
1566  }
1567  else if(expr.id()==ID_byte_update_little_endian ||
1568  expr.id()==ID_byte_update_big_endian)
1569  {
1570  INVARIANT(
1571  false, "byte_update ops should be lowered in prepare_for_convert_expr");
1572  }
1573  else if(expr.id()==ID_width)
1574  {
1575  std::size_t result_width=boolbv_width(expr.type());
1576  CHECK_RETURN(result_width != 0);
1577 
1578  std::size_t op_width = boolbv_width(to_unary_expr(expr).op().type());
1579  CHECK_RETURN(op_width != 0);
1580 
1581  out << "(_ bv" << op_width/8
1582  << " " << result_width << ")";
1583  }
1584  else if(expr.id()==ID_abs)
1585  {
1586  const abs_exprt &abs_expr = to_abs_expr(expr);
1587 
1588  const typet &type = abs_expr.type();
1589 
1590  if(type.id()==ID_signedbv)
1591  {
1592  std::size_t result_width = to_signedbv_type(type).get_width();
1593 
1594  out << "(ite (bvslt ";
1595  convert_expr(abs_expr.op());
1596  out << " (_ bv0 " << result_width << ")) ";
1597  out << "(bvneg ";
1598  convert_expr(abs_expr.op());
1599  out << ") ";
1600  convert_expr(abs_expr.op());
1601  out << ")";
1602  }
1603  else if(type.id()==ID_fixedbv)
1604  {
1605  std::size_t result_width=to_fixedbv_type(type).get_width();
1606 
1607  out << "(ite (bvslt ";
1608  convert_expr(abs_expr.op());
1609  out << " (_ bv0 " << result_width << ")) ";
1610  out << "(bvneg ";
1611  convert_expr(abs_expr.op());
1612  out << ") ";
1613  convert_expr(abs_expr.op());
1614  out << ")";
1615  }
1616  else if(type.id()==ID_floatbv)
1617  {
1618  if(use_FPA_theory)
1619  {
1620  out << "(fp.abs ";
1621  convert_expr(abs_expr.op());
1622  out << ")";
1623  }
1624  else
1625  convert_floatbv(abs_expr);
1626  }
1627  else
1628  UNREACHABLE;
1629  }
1630  else if(expr.id()==ID_isnan)
1631  {
1632  const isnan_exprt &isnan_expr = to_isnan_expr(expr);
1633 
1634  const typet &op_type = isnan_expr.op().type();
1635 
1636  if(op_type.id()==ID_fixedbv)
1637  out << "false";
1638  else if(op_type.id()==ID_floatbv)
1639  {
1640  if(use_FPA_theory)
1641  {
1642  out << "(fp.isNaN ";
1643  convert_expr(isnan_expr.op());
1644  out << ")";
1645  }
1646  else
1647  convert_floatbv(isnan_expr);
1648  }
1649  else
1650  UNREACHABLE;
1651  }
1652  else if(expr.id()==ID_isfinite)
1653  {
1654  const isfinite_exprt &isfinite_expr = to_isfinite_expr(expr);
1655 
1656  const typet &op_type = isfinite_expr.op().type();
1657 
1658  if(op_type.id()==ID_fixedbv)
1659  out << "true";
1660  else if(op_type.id()==ID_floatbv)
1661  {
1662  if(use_FPA_theory)
1663  {
1664  out << "(and ";
1665 
1666  out << "(not (fp.isNaN ";
1667  convert_expr(isfinite_expr.op());
1668  out << "))";
1669 
1670  out << "(not (fp.isInf ";
1671  convert_expr(isfinite_expr.op());
1672  out << "))";
1673 
1674  out << ")";
1675  }
1676  else
1677  convert_floatbv(isfinite_expr);
1678  }
1679  else
1680  UNREACHABLE;
1681  }
1682  else if(expr.id()==ID_isinf)
1683  {
1684  const isinf_exprt &isinf_expr = to_isinf_expr(expr);
1685 
1686  const typet &op_type = isinf_expr.op().type();
1687 
1688  if(op_type.id()==ID_fixedbv)
1689  out << "false";
1690  else if(op_type.id()==ID_floatbv)
1691  {
1692  if(use_FPA_theory)
1693  {
1694  out << "(fp.isInfinite ";
1695  convert_expr(isinf_expr.op());
1696  out << ")";
1697  }
1698  else
1699  convert_floatbv(isinf_expr);
1700  }
1701  else
1702  UNREACHABLE;
1703  }
1704  else if(expr.id()==ID_isnormal)
1705  {
1706  const isnormal_exprt &isnormal_expr = to_isnormal_expr(expr);
1707 
1708  const typet &op_type = isnormal_expr.op().type();
1709 
1710  if(op_type.id()==ID_fixedbv)
1711  out << "true";
1712  else if(op_type.id()==ID_floatbv)
1713  {
1714  if(use_FPA_theory)
1715  {
1716  out << "(fp.isNormal ";
1717  convert_expr(isnormal_expr.op());
1718  out << ")";
1719  }
1720  else
1721  convert_floatbv(isnormal_expr);
1722  }
1723  else
1724  UNREACHABLE;
1725  }
1726  else if(expr.id()==ID_overflow_plus ||
1727  expr.id()==ID_overflow_minus)
1728  {
1729  const auto &op0 = to_binary_expr(expr).op0();
1730  const auto &op1 = to_binary_expr(expr).op1();
1731 
1733  expr.type().id() == ID_bool,
1734  "overflow plus and overflow minus expressions shall be of Boolean type");
1735 
1736  bool subtract=expr.id()==ID_overflow_minus;
1737  const typet &op_type = op0.type();
1738  std::size_t width=boolbv_width(op_type);
1739 
1740  if(op_type.id()==ID_signedbv)
1741  {
1742  // an overflow occurs if the top two bits of the extended sum differ
1743  out << "(let ((?sum (";
1744  out << (subtract?"bvsub":"bvadd");
1745  out << " ((_ sign_extend 1) ";
1746  convert_expr(op0);
1747  out << ")";
1748  out << " ((_ sign_extend 1) ";
1749  convert_expr(op1);
1750  out << ")))) "; // sign_extend, bvadd/sub let2
1751  out << "(not (= "
1752  "((_ extract " << width << " " << width << ") ?sum) "
1753  "((_ extract " << (width-1) << " " << (width-1) << ") ?sum)";
1754  out << ")))"; // =, not, let
1755  }
1756  else if(op_type.id()==ID_unsignedbv ||
1757  op_type.id()==ID_pointer)
1758  {
1759  // overflow is simply carry-out
1760  out << "(= ";
1761  out << "((_ extract " << width << " " << width << ") ";
1762  out << "(" << (subtract?"bvsub":"bvadd");
1763  out << " ((_ zero_extend 1) ";
1764  convert_expr(op0);
1765  out << ")";
1766  out << " ((_ zero_extend 1) ";
1767  convert_expr(op1);
1768  out << ")))"; // zero_extend, bvsub/bvadd, extract
1769  out << " #b1)"; // =
1770  }
1771  else
1773  false,
1774  "overflow check should not be performed on unsupported type",
1775  op_type.id_string());
1776  }
1777  else if(expr.id()==ID_overflow_mult)
1778  {
1779  const auto &op0 = to_binary_expr(expr).op0();
1780  const auto &op1 = to_binary_expr(expr).op1();
1781 
1783  expr.type().id() == ID_bool,
1784  "overflow mult expression shall be of Boolean type");
1785 
1786  // No better idea than to multiply with double the bits and then compare
1787  // with max value.
1788 
1789  const typet &op_type = op0.type();
1790  std::size_t width=boolbv_width(op_type);
1791 
1792  if(op_type.id()==ID_signedbv)
1793  {
1794  out << "(let ( (prod (bvmul ((_ sign_extend " << width << ") ";
1795  convert_expr(op0);
1796  out << ") ((_ sign_extend " << width << ") ";
1797  convert_expr(op1);
1798  out << ")) )) ";
1799  out << "(or (bvsge prod (_ bv" << power(2, width-1) << " "
1800  << width*2 << "))";
1801  out << " (bvslt prod (bvneg (_ bv" << power(2, width-1) << " "
1802  << width*2 << ")))))";
1803  }
1804  else if(op_type.id()==ID_unsignedbv)
1805  {
1806  out << "(bvuge (bvmul ((_ zero_extend " << width << ") ";
1807  convert_expr(op0);
1808  out << ") ((_ zero_extend " << width << ") ";
1809  convert_expr(op1);
1810  out << ")) (_ bv" << power(2, width) << " " << width*2 << "))";
1811  }
1812  else
1814  false,
1815  "overflow check should not be performed on unsupported type",
1816  op_type.id_string());
1817  }
1818  else if(expr.id()==ID_array)
1819  {
1820  defined_expressionst::const_iterator it=defined_expressions.find(expr);
1821  CHECK_RETURN(it != defined_expressions.end());
1822  out << it->second;
1823  }
1824  else if(expr.id()==ID_literal)
1825  {
1826  convert_literal(to_literal_expr(expr).get_literal());
1827  }
1828  else if(expr.id()==ID_forall ||
1829  expr.id()==ID_exists)
1830  {
1831  const quantifier_exprt &quantifier_expr = to_quantifier_expr(expr);
1832 
1834  // NOLINTNEXTLINE(readability/throw)
1835  throw "MathSAT does not support quantifiers";
1836 
1837  if(quantifier_expr.id() == ID_forall)
1838  out << "(forall ";
1839  else if(quantifier_expr.id() == ID_exists)
1840  out << "(exists ";
1841 
1842  exprt bound = quantifier_expr.symbol();
1843 
1844  out << "((";
1845  convert_expr(bound);
1846  out << " ";
1847  convert_type(bound.type());
1848  out << ")) ";
1849 
1850  convert_expr(quantifier_expr.where());
1851 
1852  out << ")";
1853  }
1854  else if(expr.id()==ID_vector)
1855  {
1856  const vector_exprt &vector_expr = to_vector_expr(expr);
1857  const vector_typet &vector_type = to_vector_type(vector_expr.type());
1858 
1859  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
1860 
1862  size == vector_expr.operands().size(),
1863  "size indicated by type shall be equal to the number of operands");
1864 
1865  if(use_datatypes)
1866  {
1867  const std::string &smt_typename = datatype_map.at(vector_type);
1868 
1869  out << "(mk-" << smt_typename;
1870  }
1871  else
1872  out << "(concat";
1873 
1874  // build component-by-component
1875  forall_operands(it, vector_expr)
1876  {
1877  out << " ";
1878  convert_expr(*it);
1879  }
1880 
1881  out << ")"; // mk-... or concat
1882  }
1883  else if(expr.id()==ID_object_size)
1884  {
1885  out << object_sizes[expr];
1886  }
1887  else if(expr.id()==ID_let)
1888  {
1889  const let_exprt &let_expr=to_let_expr(expr);
1890  const auto &variables = let_expr.variables();
1891  const auto &values = let_expr.values();
1892 
1893  out << "(let (";
1894  bool first = true;
1895 
1896  for(auto &binding : make_range(variables).zip(values))
1897  {
1898  if(first)
1899  first = false;
1900  else
1901  out << ' ';
1902 
1903  out << '(';
1904  convert_expr(binding.first);
1905  out << ' ';
1906  convert_expr(binding.second);
1907  out << ')';
1908  }
1909 
1910  out << ") "; // bindings
1911 
1912  convert_expr(let_expr.where());
1913  out << ')'; // let
1914  }
1915  else if(expr.id()==ID_constraint_select_one)
1916  {
1918  "smt2_convt::convert_expr: '" + expr.id_string() +
1919  "' is not yet supported");
1920  }
1921  else if(expr.id() == ID_bswap)
1922  {
1923  const bswap_exprt &bswap_expr = to_bswap_expr(expr);
1924 
1926  bswap_expr.op().type() == bswap_expr.type(),
1927  "operand of byte swap expression shall have same type as the expression");
1928 
1929  // first 'let' the operand
1930  out << "(let ((bswap_op ";
1931  convert_expr(bswap_expr.op());
1932  out << ")) ";
1933 
1934  if(
1935  bswap_expr.type().id() == ID_signedbv ||
1936  bswap_expr.type().id() == ID_unsignedbv)
1937  {
1938  const std::size_t width =
1939  to_bitvector_type(bswap_expr.type()).get_width();
1940 
1941  const std::size_t bits_per_byte = bswap_expr.get_bits_per_byte();
1942 
1943  // width must be multiple of bytes
1945  width % bits_per_byte == 0,
1946  "bit width indicated by type of bswap expression should be a multiple "
1947  "of the number of bits per byte");
1948 
1949  const std::size_t bytes = width / bits_per_byte;
1950 
1951  if(bytes <= 1)
1952  out << "bswap_op";
1953  else
1954  {
1955  // do a parallel 'let' for each byte
1956  out << "(let (";
1957 
1958  for(std::size_t byte = 0; byte < bytes; byte++)
1959  {
1960  if(byte != 0)
1961  out << ' ';
1962  out << "(bswap_byte_" << byte << ' ';
1963  out << "((_ extract " << (byte * bits_per_byte + (bits_per_byte - 1))
1964  << " " << (byte * bits_per_byte) << ") bswap_op)";
1965  out << ')';
1966  }
1967 
1968  out << ") ";
1969 
1970  // now stitch back together with 'concat'
1971  out << "(concat";
1972 
1973  for(std::size_t byte = 0; byte < bytes; byte++)
1974  out << " bswap_byte_" << byte;
1975 
1976  out << ')'; // concat
1977  out << ')'; // let bswap_byte_*
1978  }
1979  }
1980  else
1981  UNEXPECTEDCASE("bswap must get bitvector operand");
1982 
1983  out << ')'; // let bswap_op
1984  }
1985  else if(expr.id() == ID_popcount)
1986  {
1987  exprt lowered = lower_popcount(to_popcount_expr(expr), ns);
1988  convert_expr(lowered);
1989  }
1990  else
1992  false,
1993  "smt2_convt::convert_expr should not be applied to unsupported type",
1994  expr.id_string());
1995 }
1996 
1998 {
1999  const exprt &src = expr.op();
2000 
2001  typet dest_type = expr.type();
2002  if(dest_type.id()==ID_c_enum_tag)
2003  dest_type=ns.follow_tag(to_c_enum_tag_type(dest_type));
2004 
2005  typet src_type = src.type();
2006  if(src_type.id()==ID_c_enum_tag)
2007  src_type=ns.follow_tag(to_c_enum_tag_type(src_type));
2008 
2009  if(dest_type.id()==ID_bool)
2010  {
2011  // this is comparison with zero
2012  if(src_type.id()==ID_signedbv ||
2013  src_type.id()==ID_unsignedbv ||
2014  src_type.id()==ID_c_bool ||
2015  src_type.id()==ID_fixedbv ||
2016  src_type.id()==ID_pointer ||
2017  src_type.id()==ID_integer)
2018  {
2019  out << "(not (= ";
2020  convert_expr(src);
2021  out << " ";
2022  convert_expr(from_integer(0, src_type));
2023  out << "))";
2024  }
2025  else if(src_type.id()==ID_floatbv)
2026  {
2027  if(use_FPA_theory)
2028  {
2029  out << "(not (fp.isZero ";
2030  convert_expr(src);
2031  out << "))";
2032  }
2033  else
2034  convert_floatbv(expr);
2035  }
2036  else
2037  {
2038  UNEXPECTEDCASE("TODO typecast1 "+src_type.id_string()+" -> bool");
2039  }
2040  }
2041  else if(dest_type.id()==ID_c_bool)
2042  {
2043  std::size_t to_width=boolbv_width(dest_type);
2044  out << "(ite ";
2045  out << "(not (= ";
2046  convert_expr(src);
2047  out << " ";
2048  convert_expr(from_integer(0, src_type));
2049  out << ")) "; // not, =
2050  out << " (_ bv1 " << to_width << ")";
2051  out << " (_ bv0 " << to_width << ")";
2052  out << ")"; // ite
2053  }
2054  else if(dest_type.id()==ID_signedbv ||
2055  dest_type.id()==ID_unsignedbv ||
2056  dest_type.id()==ID_c_enum ||
2057  dest_type.id()==ID_bv)
2058  {
2059  std::size_t to_width=boolbv_width(dest_type);
2060 
2061  if(src_type.id()==ID_signedbv || // from signedbv
2062  src_type.id()==ID_unsignedbv || // from unsigedbv
2063  src_type.id()==ID_c_bool ||
2064  src_type.id()==ID_c_enum ||
2065  src_type.id()==ID_bv)
2066  {
2067  std::size_t from_width=boolbv_width(src_type);
2068 
2069  if(from_width==to_width)
2070  convert_expr(src); // ignore
2071  else if(from_width<to_width) // extend
2072  {
2073  if(src_type.id()==ID_signedbv)
2074  out << "((_ sign_extend ";
2075  else
2076  out << "((_ zero_extend ";
2077 
2078  out << (to_width-from_width)
2079  << ") "; // ind
2080  convert_expr(src);
2081  out << ")";
2082  }
2083  else // chop off extra bits
2084  {
2085  out << "((_ extract " << (to_width-1) << " 0) ";
2086  convert_expr(src);
2087  out << ")";
2088  }
2089  }
2090  else if(src_type.id()==ID_fixedbv) // from fixedbv to int
2091  {
2092  const fixedbv_typet &fixedbv_type=to_fixedbv_type(src_type);
2093 
2094  std::size_t from_width=fixedbv_type.get_width();
2095  std::size_t from_integer_bits=fixedbv_type.get_integer_bits();
2096  std::size_t from_fraction_bits=fixedbv_type.get_fraction_bits();
2097 
2098  // we might need to round up in case of negative numbers
2099  // e.g., (int)(-1.00001)==1
2100 
2101  out << "(let ((?tcop ";
2102  convert_expr(src);
2103  out << ")) ";
2104 
2105  out << "(bvadd ";
2106 
2107  if(to_width>from_integer_bits)
2108  {
2109  out << "((_ sign_extend "
2110  << (to_width-from_integer_bits) << ") ";
2111  out << "((_ extract " << (from_width-1) << " "
2112  << from_fraction_bits << ") ";
2113  convert_expr(src);
2114  out << "))";
2115  }
2116  else
2117  {
2118  out << "((_ extract " << (from_fraction_bits+to_width-1)
2119  << " " << from_fraction_bits << ") ";
2120  convert_expr(src);
2121  out << ")";
2122  }
2123 
2124  out << " (ite (and ";
2125 
2126  // some fraction bit is not zero
2127  out << "(not (= ((_ extract " << (from_fraction_bits-1) << " 0) ?tcop) "
2128  "(_ bv0 " << from_fraction_bits << ")))";
2129 
2130  // number negative
2131  out << " (= ((_ extract " << (from_width-1) << " " << (from_width-1)
2132  << ") ?tcop) #b1)";
2133 
2134  out << ")"; // and
2135 
2136  out << " (_ bv1 " << to_width << ") (_ bv0 " << to_width << "))"; // ite
2137  out << ")"; // bvadd
2138  out << ")"; // let
2139  }
2140  else if(src_type.id()==ID_floatbv) // from floatbv to int
2141  {
2142  if(dest_type.id()==ID_bv)
2143  {
2144  // this is _NOT_ a semantic conversion, but bit-wise
2145 
2146  if(use_FPA_theory)
2147  {
2148  // This conversion is non-trivial as it requires creating a
2149  // new bit-vector variable and then asserting that it converts
2150  // to the required floating-point number.
2151  SMT2_TODO("bit-wise floatbv to bv");
2152  }
2153  else
2154  {
2155  // straight-forward if width matches
2156  convert_expr(src);
2157  }
2158  }
2159  else if(dest_type.id()==ID_signedbv)
2160  {
2161  // this should be floatbv_typecast, not typecast
2163  "typecast unexpected "+src_type.id_string()+" -> "+
2164  dest_type.id_string());
2165  }
2166  else if(dest_type.id()==ID_unsignedbv)
2167  {
2168  // this should be floatbv_typecast, not typecast
2170  "typecast unexpected "+src_type.id_string()+" -> "+
2171  dest_type.id_string());
2172  }
2173  }
2174  else if(src_type.id()==ID_bool) // from boolean to int
2175  {
2176  out << "(ite ";
2177  convert_expr(src);
2178 
2179  if(dest_type.id()==ID_fixedbv)
2180  {
2181  fixedbv_spect spec(to_fixedbv_type(dest_type));
2182  out << " (concat (_ bv1 "
2183  << spec.integer_bits << ") " <<
2184  "(_ bv0 " << spec.get_fraction_bits() << ")) " <<
2185  "(_ bv0 " << spec.width << ")";
2186  }
2187  else
2188  {
2189  out << " (_ bv1 " << to_width << ")";
2190  out << " (_ bv0 " << to_width << ")";
2191  }
2192 
2193  out << ")";
2194  }
2195  else if(src_type.id()==ID_pointer) // from pointer to int
2196  {
2197  std::size_t from_width=boolbv_width(src_type);
2198 
2199  if(from_width<to_width) // extend
2200  {
2201  out << "((_ sign_extend ";
2202  out << (to_width-from_width)
2203  << ") ";
2204  convert_expr(src);
2205  out << ")";
2206  }
2207  else // chop off extra bits
2208  {
2209  out << "((_ extract " << (to_width-1) << " 0) ";
2210  convert_expr(src);
2211  out << ")";
2212  }
2213  }
2214  else if(src_type.id()==ID_integer) // from integer to bit-vector
2215  {
2216  // must be constant
2217  if(src.is_constant())
2218  {
2219  mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(src));
2220  out << "(_ bv" << i << " " << to_width << ")";
2221  }
2222  else
2223  SMT2_TODO("can't convert non-constant integer to bitvector");
2224  }
2225  else if(
2226  src_type.id() == ID_struct ||
2227  src_type.id() == ID_struct_tag) // flatten a struct to a bit-vector
2228  {
2229  if(use_datatypes)
2230  {
2231  INVARIANT(
2232  boolbv_width(src_type) == boolbv_width(dest_type),
2233  "bit vector with of source and destination type shall be equal");
2234  flatten2bv(src);
2235  }
2236  else
2237  {
2238  INVARIANT(
2239  boolbv_width(src_type) == boolbv_width(dest_type),
2240  "bit vector with of source and destination type shall be equal");
2241  convert_expr(src); // nothing else to do!
2242  }
2243  }
2244  else if(
2245  src_type.id() == ID_union ||
2246  src_type.id() == ID_union_tag) // flatten a union
2247  {
2248  INVARIANT(
2249  boolbv_width(src_type) == boolbv_width(dest_type),
2250  "bit vector with of source and destination type shall be equal");
2251  convert_expr(src); // nothing else to do!
2252  }
2253  else if(src_type.id()==ID_c_bit_field)
2254  {
2255  std::size_t from_width=boolbv_width(src_type);
2256 
2257  if(from_width==to_width)
2258  convert_expr(src); // ignore
2259  else
2260  {
2262  typecast_exprt tmp(typecast_exprt(src, t), dest_type);
2263  convert_typecast(tmp);
2264  }
2265  }
2266  else
2267  {
2268  std::ostringstream e_str;
2269  e_str << src_type.id() << " -> " << dest_type.id()
2270  << " src == " << format(src);
2271  UNEXPECTEDCASE("TODO typecast2 " + e_str.str());
2272  }
2273  }
2274  else if(dest_type.id()==ID_fixedbv) // to fixedbv
2275  {
2276  const fixedbv_typet &fixedbv_type=to_fixedbv_type(dest_type);
2277  std::size_t to_fraction_bits=fixedbv_type.get_fraction_bits();
2278  std::size_t to_integer_bits=fixedbv_type.get_integer_bits();
2279 
2280  if(src_type.id()==ID_unsignedbv ||
2281  src_type.id()==ID_signedbv ||
2282  src_type.id()==ID_c_enum)
2283  {
2284  // integer to fixedbv
2285 
2286  std::size_t from_width=to_bitvector_type(src_type).get_width();
2287  out << "(concat ";
2288 
2289  if(from_width==to_integer_bits)
2290  convert_expr(src);
2291  else if(from_width>to_integer_bits)
2292  {
2293  // too many integer bits
2294  out << "((_ extract " << (to_integer_bits-1) << " 0) ";
2295  convert_expr(src);
2296  out << ")";
2297  }
2298  else
2299  {
2300  // too few integer bits
2301  INVARIANT(
2302  from_width < to_integer_bits,
2303  "from_width should be smaller than to_integer_bits as other case "
2304  "have been handled above");
2305  if(dest_type.id()==ID_unsignedbv)
2306  {
2307  out << "(_ zero_extend "
2308  << (to_integer_bits-from_width) << ") ";
2309  convert_expr(src);
2310  out << ")";
2311  }
2312  else
2313  {
2314  out << "((_ sign_extend "
2315  << (to_integer_bits-from_width) << ") ";
2316  convert_expr(src);
2317  out << ")";
2318  }
2319  }
2320 
2321  out << "(_ bv0 " << to_fraction_bits << ")";
2322  out << ")"; // concat
2323  }
2324  else if(src_type.id()==ID_bool) // bool to fixedbv
2325  {
2326  out << "(concat (concat"
2327  << " (_ bv0 " << (to_integer_bits-1) << ") ";
2328  flatten2bv(src); // produces #b0 or #b1
2329  out << ") (_ bv0 "
2330  << to_fraction_bits
2331  << "))";
2332  }
2333  else if(src_type.id()==ID_fixedbv) // fixedbv to fixedbv
2334  {
2335  const fixedbv_typet &from_fixedbv_type=to_fixedbv_type(src_type);
2336  std::size_t from_fraction_bits=from_fixedbv_type.get_fraction_bits();
2337  std::size_t from_integer_bits=from_fixedbv_type.get_integer_bits();
2338  std::size_t from_width=from_fixedbv_type.get_width();
2339 
2340  out << "(let ((?tcop ";
2341  convert_expr(src);
2342  out << ")) ";
2343 
2344  out << "(concat ";
2345 
2346  if(to_integer_bits<=from_integer_bits)
2347  {
2348  out << "((_ extract "
2349  << (from_fraction_bits+to_integer_bits-1) << " "
2350  << from_fraction_bits
2351  << ") ?tcop)";
2352  }
2353  else
2354  {
2355  INVARIANT(
2356  to_integer_bits > from_integer_bits,
2357  "to_integer_bits should be greater than from_integer_bits as the"
2358  "other case has been handled above");
2359  out << "((_ sign_extend "
2360  << (to_integer_bits-from_integer_bits)
2361  << ") ((_ extract "
2362  << (from_width-1) << " "
2363  << from_fraction_bits
2364  << ") ?tcop))";
2365  }
2366 
2367  out << " ";
2368 
2369  if(to_fraction_bits<=from_fraction_bits)
2370  {
2371  out << "((_ extract "
2372  << (from_fraction_bits-1) << " "
2373  << (from_fraction_bits-to_fraction_bits)
2374  << ") ?tcop)";
2375  }
2376  else
2377  {
2378  INVARIANT(
2379  to_fraction_bits > from_fraction_bits,
2380  "to_fraction_bits should be greater than from_fraction_bits as the"
2381  "other case has been handled above");
2382  out << "(concat ((_ extract "
2383  << (from_fraction_bits-1) << " 0) ";
2384  convert_expr(src);
2385  out << ")"
2386  << " (_ bv0 " << to_fraction_bits-from_fraction_bits
2387  << "))";
2388  }
2389 
2390  out << "))"; // concat, let
2391  }
2392  else
2393  UNEXPECTEDCASE("unexpected typecast to fixedbv");
2394  }
2395  else if(dest_type.id()==ID_pointer)
2396  {
2397  std::size_t to_width=boolbv_width(dest_type);
2398 
2399  if(src_type.id()==ID_pointer) // pointer to pointer
2400  {
2401  // this just passes through
2402  convert_expr(src);
2403  }
2404  else if(
2405  src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv ||
2406  src_type.id() == ID_bv)
2407  {
2408  // integer to pointer
2409 
2410  std::size_t from_width=boolbv_width(src_type);
2411 
2412  if(from_width==to_width)
2413  convert_expr(src);
2414  else if(from_width<to_width)
2415  {
2416  out << "((_ sign_extend "
2417  << (to_width-from_width)
2418  << ") ";
2419  convert_expr(src);
2420  out << ")"; // sign_extend
2421  }
2422  else // from_width>to_width
2423  {
2424  out << "((_ extract " << to_width << " 0) ";
2425  convert_expr(src);
2426  out << ")"; // extract
2427  }
2428  }
2429  else
2430  UNEXPECTEDCASE("TODO typecast3 "+src_type.id_string()+" -> pointer");
2431  }
2432  else if(dest_type.id()==ID_range)
2433  {
2434  SMT2_TODO("range typecast");
2435  }
2436  else if(dest_type.id()==ID_floatbv)
2437  {
2438  // Typecast from integer to floating-point should have be been
2439  // converted to ID_floatbv_typecast during symbolic execution,
2440  // adding the rounding mode. See
2441  // smt2_convt::convert_floatbv_typecast.
2442  // The exception is bool and c_bool to float.
2443  const auto &dest_floatbv_type = to_floatbv_type(dest_type);
2444 
2445  if(src_type.id()==ID_bool)
2446  {
2447  constant_exprt val(irep_idt(), dest_type);
2448 
2449  ieee_floatt a(dest_floatbv_type);
2450 
2451  mp_integer significand;
2452  mp_integer exponent;
2453 
2454  out << "(ite ";
2455  convert_expr(src);
2456  out << " ";
2457 
2458  significand = 1;
2459  exponent = 0;
2460  a.build(significand, exponent);
2461  val.set_value(integer2bvrep(a.pack(), a.spec.width()));
2462 
2463  convert_constant(val);
2464  out << " ";
2465 
2466  significand = 0;
2467  exponent = 0;
2468  a.build(significand, exponent);
2469  val.set_value(integer2bvrep(a.pack(), a.spec.width()));
2470 
2471  convert_constant(val);
2472  out << ")";
2473  }
2474  else if(src_type.id()==ID_c_bool)
2475  {
2476  // turn into proper bool
2477  const typecast_exprt tmp(src, bool_typet());
2478  convert_typecast(typecast_exprt(tmp, dest_type));
2479  }
2480  else if(src_type.id() == ID_bv)
2481  {
2482  if(to_bv_type(src_type).get_width() != dest_floatbv_type.get_width())
2483  {
2484  UNEXPECTEDCASE("Typecast bv -> float with wrong width");
2485  }
2486 
2487  if(use_FPA_theory)
2488  {
2489  out << "((_ to_fp " << dest_floatbv_type.get_e() << " "
2490  << dest_floatbv_type.get_f() + 1 << ") ";
2491  convert_expr(src);
2492  out << ')';
2493  }
2494  else
2495  convert_expr(src);
2496  }
2497  else
2498  UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float");
2499  }
2500  else if(dest_type.id()==ID_integer)
2501  {
2502  if(src_type.id()==ID_bool)
2503  {
2504  out << "(ite ";
2505  convert_expr(src);
2506  out <<" 1 0)";
2507  }
2508  else
2509  UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> integer");
2510  }
2511  else if(dest_type.id()==ID_c_bit_field)
2512  {
2513  std::size_t from_width=boolbv_width(src_type);
2514  std::size_t to_width=boolbv_width(dest_type);
2515 
2516  if(from_width==to_width)
2517  convert_expr(src); // ignore
2518  else
2519  {
2521  typecast_exprt tmp(typecast_exprt(src, t), dest_type);
2522  convert_typecast(tmp);
2523  }
2524  }
2525  else
2527  "TODO typecast8 "+src_type.id_string()+" -> "+dest_type.id_string());
2528 }
2529 
2531 {
2532  const exprt &src=expr.op();
2533  // const exprt &rounding_mode=expr.rounding_mode();
2534  const typet &src_type=src.type();
2535  const typet &dest_type=expr.type();
2536 
2537  if(dest_type.id()==ID_floatbv)
2538  {
2539  if(src_type.id()==ID_floatbv)
2540  {
2541  // float to float
2542 
2543  /* ISO 9899:1999
2544  * 6.3.1.5 Real floating types
2545  * 1 When a float is promoted to double or long double, or a
2546  * double is promoted to long double, its value is unchanged.
2547  *
2548  * 2 When a double is demoted to float, a long double is
2549  * demoted to double or float, or a value being represented in
2550  * greater precision and range than required by its semantic
2551  * type (see 6.3.1.8) is explicitly converted to its semantic
2552  * type, if the value being converted can be represented
2553  * exactly in the new type, it is unchanged. If the value
2554  * being converted is in the range of values that can be
2555  * represented but cannot be represented exactly, the result
2556  * is either the nearest higher or nearest lower representable
2557  * value, chosen in an implementation-defined manner. If the
2558  * value being converted is outside the range of values that
2559  * can be represented, the behavior is undefined.
2560  */
2561 
2562  const floatbv_typet &dst=to_floatbv_type(dest_type);
2563 
2564  if(use_FPA_theory)
2565  {
2566  out << "((_ to_fp " << dst.get_e() << " "
2567  << dst.get_f() + 1 << ") ";
2569  out << " ";
2570  convert_expr(src);
2571  out << ")";
2572  }
2573  else
2574  convert_floatbv(expr);
2575  }
2576  else if(src_type.id()==ID_unsignedbv)
2577  {
2578  // unsigned to float
2579 
2580  /* ISO 9899:1999
2581  * 6.3.1.4 Real floating and integer
2582  * 2 When a value of integer type is converted to a real
2583  * floating type, if the value being converted can be
2584  * represented exactly in the new type, it is unchanged. If the
2585  * value being converted is in the range of values that can be
2586  * represented but cannot be represented exactly, the result is
2587  * either the nearest higher or nearest lower representable
2588  * value, chosen in an implementation-defined manner. If the
2589  * value being converted is outside the range of values that can
2590  * be represented, the behavior is undefined.
2591  */
2592 
2593  const floatbv_typet &dst=to_floatbv_type(dest_type);
2594 
2595  if(use_FPA_theory)
2596  {
2597  out << "((_ to_fp_unsigned " << dst.get_e() << " "
2598  << dst.get_f() + 1 << ") ";
2600  out << " ";
2601  convert_expr(src);
2602  out << ")";
2603  }
2604  else
2605  convert_floatbv(expr);
2606  }
2607  else if(src_type.id()==ID_signedbv)
2608  {
2609  // signed to float
2610 
2611  const floatbv_typet &dst=to_floatbv_type(dest_type);
2612 
2613  if(use_FPA_theory)
2614  {
2615  out << "((_ to_fp " << dst.get_e() << " "
2616  << dst.get_f() + 1 << ") ";
2618  out << " ";
2619  convert_expr(src);
2620  out << ")";
2621  }
2622  else
2623  convert_floatbv(expr);
2624  }
2625  else if(src_type.id()==ID_c_enum_tag)
2626  {
2627  // enum to float
2628 
2629  // We first convert to 'underlying type'
2630  floatbv_typecast_exprt tmp=expr;
2631  tmp.op()=
2633  src,
2634  ns.follow_tag(to_c_enum_tag_type(src_type)).subtype());
2636  }
2637  else
2639  "TODO typecast11 "+src_type.id_string()+" -> "+dest_type.id_string());
2640  }
2641  else if(dest_type.id()==ID_signedbv)
2642  {
2643  if(use_FPA_theory)
2644  {
2645  std::size_t dest_width=to_signedbv_type(dest_type).get_width();
2646  out << "((_ fp.to_sbv " << dest_width << ") ";
2648  out << " ";
2649  convert_expr(src);
2650  out << ")";
2651  }
2652  else
2653  convert_floatbv(expr);
2654  }
2655  else if(dest_type.id()==ID_unsignedbv)
2656  {
2657  if(use_FPA_theory)
2658  {
2659  std::size_t dest_width=to_unsignedbv_type(dest_type).get_width();
2660  out << "((_ fp.to_ubv " << dest_width << ") ";
2662  out << " ";
2663  convert_expr(src);
2664  out << ")";
2665  }
2666  else
2667  convert_floatbv(expr);
2668  }
2669  else
2670  {
2672  "TODO typecast12 "+src_type.id_string()+" -> "+dest_type.id_string());
2673  }
2674 }
2675 
2677 {
2678  const struct_typet &struct_type = to_struct_type(ns.follow(expr.type()));
2679 
2680  const struct_typet::componentst &components=
2681  struct_type.components();
2682 
2684  components.size() == expr.operands().size(),
2685  "number of struct components as indicated by the struct type shall be equal"
2686  "to the number of operands of the struct expression");
2687 
2688  DATA_INVARIANT(!components.empty(), "struct shall have struct components");
2689 
2690  if(use_datatypes)
2691  {
2692  const std::string &smt_typename = datatype_map.at(struct_type);
2693 
2694  // use the constructor for the Z3 datatype
2695  out << "(mk-" << smt_typename;
2696 
2697  std::size_t i=0;
2698  for(struct_typet::componentst::const_iterator
2699  it=components.begin();
2700  it!=components.end();
2701  it++, i++)
2702  {
2703  out << " ";
2704  convert_expr(expr.operands()[i]);
2705  }
2706 
2707  out << ")";
2708  }
2709  else
2710  {
2711  if(components.size()==1)
2712  convert_expr(expr.op0());
2713  else
2714  {
2715  // SMT-LIB 2 concat is binary only
2716  for(std::size_t i=components.size(); i>1; i--)
2717  {
2718  out << "(concat ";
2719 
2720  exprt op=expr.operands()[i-1];
2721 
2722  // may need to flatten array-theory arrays in there
2723  if(op.type().id() == ID_array)
2724  flatten_array(op);
2725  else
2726  convert_expr(op);
2727 
2728  out << " ";
2729  }
2730 
2731  convert_expr(expr.op0());
2732 
2733  for(std::size_t i=1; i<components.size(); i++)
2734  out << ")";
2735  }
2736  }
2737 }
2738 
2741 {
2742  const array_typet &array_type = to_array_type(expr.type());
2743  const auto &size_expr = array_type.size();
2744  PRECONDITION(size_expr.id() == ID_constant);
2745 
2746  mp_integer size = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
2747  CHECK_RETURN_WITH_DIAGNOSTICS(size != 0, "can't convert zero-sized array");
2748 
2749  out << "(let ((?far ";
2750  convert_expr(expr);
2751  out << ")) ";
2752 
2753  for(mp_integer i=size; i!=0; --i)
2754  {
2755  if(i!=1)
2756  out << "(concat ";
2757  out << "(select ?far ";
2758  convert_expr(from_integer(i-1, array_type.size().type()));
2759  out << ")";
2760  if(i!=1)
2761  out << " ";
2762  }
2763 
2764  // close the many parentheses
2765  for(mp_integer i=size; i>1; --i)
2766  out << ")";
2767 
2768  out << ")"; // let
2769 }
2770 
2772 {
2773  const union_typet &union_type = to_union_type(ns.follow(expr.type()));
2774  const exprt &op=expr.op();
2775 
2776  std::size_t total_width=boolbv_width(union_type);
2778  total_width != 0, "failed to get union width for union");
2779 
2780  std::size_t member_width=boolbv_width(op.type());
2782  member_width != 0, "failed to get union member width for union");
2783 
2784  if(total_width==member_width)
2785  {
2786  flatten2bv(op);
2787  }
2788  else
2789  {
2790  // we will pad with zeros, but non-det would be better
2791  INVARIANT(
2792  total_width > member_width,
2793  "total_width should be greater than member_width as member_width can be"
2794  "at most as large as total_width and the other case has been handled "
2795  "above");
2796  out << "(concat ";
2797  out << "(_ bv0 "
2798  << (total_width-member_width) << ") ";
2799  flatten2bv(op);
2800  out << ")";
2801  }
2802 }
2803 
2805 {
2806  const typet &expr_type=expr.type();
2807 
2808  if(expr_type.id()==ID_unsignedbv ||
2809  expr_type.id()==ID_signedbv ||
2810  expr_type.id()==ID_bv ||
2811  expr_type.id()==ID_c_enum ||
2812  expr_type.id()==ID_c_enum_tag ||
2813  expr_type.id()==ID_c_bool ||
2814  expr_type.id()==ID_c_bit_field)
2815  {
2816  const std::size_t width = boolbv_width(expr_type);
2817 
2818  const mp_integer value = bvrep2integer(expr.get_value(), width, false);
2819 
2820  out << "(_ bv" << value
2821  << " " << width << ")";
2822  }
2823  else if(expr_type.id()==ID_fixedbv)
2824  {
2825  const fixedbv_spect spec(to_fixedbv_type(expr_type));
2826 
2827  const mp_integer v = bvrep2integer(expr.get_value(), spec.width, false);
2828 
2829  out << "(_ bv" << v << " " << spec.width << ")";
2830  }
2831  else if(expr_type.id()==ID_floatbv)
2832  {
2833  const floatbv_typet &floatbv_type=
2834  to_floatbv_type(expr_type);
2835 
2836  if(use_FPA_theory)
2837  {
2838  /* CBMC stores floating point literals in the most
2839  computationally useful form; biased exponents and
2840  significands including the hidden bit. Thus some encoding
2841  is needed to get to IEEE-754 style representations. */
2842 
2843  ieee_floatt v=ieee_floatt(expr);
2844  size_t e=floatbv_type.get_e();
2845  size_t f=floatbv_type.get_f()+1;
2846 
2847  /* Should be sufficient, but not currently supported by mathsat */
2848  #if 0
2849  mp_integer binary = v.pack();
2850 
2851  out << "((_ to_fp " << e << " " << f << ")"
2852  << " #b" << integer2binary(v.pack(), v.spec.width()) << ")";
2853  #endif
2854 
2855  if(v.is_NaN())
2856  {
2857  out << "(_ NaN " << e << " " << f << ")";
2858  }
2859  else if(v.is_infinity())
2860  {
2861  if(v.get_sign())
2862  out << "(_ -oo " << e << " " << f << ")";
2863  else
2864  out << "(_ +oo " << e << " " << f << ")";
2865  }
2866  else
2867  {
2868  // Zero, normal or subnormal
2869 
2870  mp_integer binary = v.pack();
2871  std::string binaryString(integer2binary(v.pack(), v.spec.width()));
2872 
2873  out << "(fp "
2874  << "#b" << binaryString.substr(0, 1) << " "
2875  << "#b" << binaryString.substr(1, e) << " "
2876  << "#b" << binaryString.substr(1+e, f-1) << ")";
2877  }
2878  }
2879  else
2880  {
2881  // produce corresponding bit-vector
2882  const ieee_float_spect spec(floatbv_type);
2883  const mp_integer v = bvrep2integer(expr.get_value(), spec.width(), false);
2884  out << "(_ bv" << v << " " << spec.width() << ")";
2885  }
2886  }
2887  else if(expr_type.id()==ID_pointer)
2888  {
2889  const irep_idt &value = expr.get_value();
2890 
2891  if(value==ID_NULL)
2892  {
2893  out << "(_ bv0 " << boolbv_width(expr_type)
2894  << ")";
2895  }
2896  else
2897  UNEXPECTEDCASE("unknown pointer constant: "+id2string(value));
2898  }
2899  else if(expr_type.id()==ID_bool)
2900  {
2901  if(expr.is_true())
2902  out << "true";
2903  else if(expr.is_false())
2904  out << "false";
2905  else
2906  UNEXPECTEDCASE("unknown Boolean constant");
2907  }
2908  else if(expr_type.id()==ID_array)
2909  {
2910  defined_expressionst::const_iterator it=defined_expressions.find(expr);
2911  CHECK_RETURN(it != defined_expressions.end());
2912  out << it->second;
2913  }
2914  else if(expr_type.id()==ID_rational)
2915  {
2916  std::string value=id2string(expr.get_value());
2917  size_t pos=value.find("/");
2918 
2919  if(pos==std::string::npos)
2920  out << value << ".0";
2921  else
2922  {
2923  out << "(/ " << value.substr(0, pos) << ".0 "
2924  << value.substr(pos+1) << ".0)";
2925  }
2926  }
2927  else if(expr_type.id()==ID_integer)
2928  {
2929  out << expr.get_value();
2930  }
2931  else
2932  UNEXPECTEDCASE("unknown constant: "+expr_type.id_string());
2933 }
2934 
2936 {
2937  if(expr.type().id()==ID_unsignedbv ||
2938  expr.type().id()==ID_signedbv)
2939  {
2940  if(expr.type().id()==ID_unsignedbv)
2941  out << "(bvurem ";
2942  else
2943  out << "(bvsrem ";
2944 
2945  convert_expr(expr.op0());
2946  out << " ";
2947  convert_expr(expr.op1());
2948  out << ")";
2949  }
2950  else
2951  UNEXPECTEDCASE("unsupported type for mod: "+expr.type().id_string());
2952 }
2953 
2955 {
2956  std::vector<std::size_t> dynamic_objects;
2957  pointer_logic.get_dynamic_objects(dynamic_objects);
2958 
2959  if(dynamic_objects.empty())
2960  out << "false";
2961  else
2962  {
2963  std::size_t pointer_width = boolbv_width(expr.op().type());
2964 
2965  out << "(let ((?obj ((_ extract "
2966  << pointer_width-1 << " "
2967  << pointer_width-config.bv_encoding.object_bits << ") ";
2968  convert_expr(expr.op());
2969  out << "))) ";
2970 
2971  if(dynamic_objects.size()==1)
2972  {
2973  out << "(= (_ bv" << dynamic_objects.front()
2974  << " " << config.bv_encoding.object_bits << ") ?obj)";
2975  }
2976  else
2977  {
2978  out << "(or";
2979 
2980  for(const auto &object : dynamic_objects)
2981  out << " (= (_ bv" << object
2982  << " " << config.bv_encoding.object_bits << ") ?obj)";
2983 
2984  out << ")"; // or
2985  }
2986 
2987  out << ")"; // let
2988  }
2989 }
2990 
2992 {
2993  const typet &op_type=expr.op0().type();
2994 
2995  if(op_type.id()==ID_unsignedbv ||
2996  op_type.id()==ID_pointer ||
2997  op_type.id()==ID_bv)
2998  {
2999  out << "(";
3000  if(expr.id()==ID_le)
3001  out << "bvule";
3002  else if(expr.id()==ID_lt)
3003  out << "bvult";
3004  else if(expr.id()==ID_ge)
3005  out << "bvuge";
3006  else if(expr.id()==ID_gt)
3007  out << "bvugt";
3008 
3009  out << " ";
3010  convert_expr(expr.op0());
3011  out << " ";
3012  convert_expr(expr.op1());
3013  out << ")";
3014  }
3015  else if(op_type.id()==ID_signedbv ||
3016  op_type.id()==ID_fixedbv)
3017  {
3018  out << "(";
3019  if(expr.id()==ID_le)
3020  out << "bvsle";
3021  else if(expr.id()==ID_lt)
3022  out << "bvslt";
3023  else if(expr.id()==ID_ge)
3024  out << "bvsge";
3025  else if(expr.id()==ID_gt)
3026  out << "bvsgt";
3027 
3028  out << " ";
3029  convert_expr(expr.op0());
3030  out << " ";
3031  convert_expr(expr.op1());
3032  out << ")";
3033  }
3034  else if(op_type.id()==ID_floatbv)
3035  {
3036  if(use_FPA_theory)
3037  {
3038  out << "(";
3039  if(expr.id()==ID_le)
3040  out << "fp.leq";
3041  else if(expr.id()==ID_lt)
3042  out << "fp.lt";
3043  else if(expr.id()==ID_ge)
3044  out << "fp.geq";
3045  else if(expr.id()==ID_gt)
3046  out << "fp.gt";
3047 
3048  out << " ";
3049  convert_expr(expr.op0());
3050  out << " ";
3051  convert_expr(expr.op1());
3052  out << ")";
3053  }
3054  else
3055  convert_floatbv(expr);
3056  }
3057  else if(op_type.id()==ID_rational ||
3058  op_type.id()==ID_integer)
3059  {
3060  out << "(";
3061  out << expr.id();
3062 
3063  out << " ";
3064  convert_expr(expr.op0());
3065  out << " ";
3066  convert_expr(expr.op1());
3067  out << ")";
3068  }
3069  else
3071  "unsupported type for "+expr.id_string()+": "+op_type.id_string());
3072 }
3073 
3075 {
3076  if(
3077  expr.type().id() == ID_rational || expr.type().id() == ID_integer ||
3078  expr.type().id() == ID_real)
3079  {
3080  // these are multi-ary in SMT-LIB2
3081  out << "(+";
3082 
3083  for(const auto &op : expr.operands())
3084  {
3085  out << ' ';
3086  convert_expr(op);
3087  }
3088 
3089  out << ')';
3090  }
3091  else if(
3092  expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv ||
3093  expr.type().id() == ID_fixedbv)
3094  {
3095  // These could be chained, i.e., need not be binary,
3096  // but at least MathSat doesn't like that.
3097  if(expr.operands().size() == 2)
3098  {
3099  out << "(bvadd ";
3100  convert_expr(expr.op0());
3101  out << " ";
3102  convert_expr(expr.op1());
3103  out << ")";
3104  }
3105  else
3106  {
3108  }
3109  }
3110  else if(expr.type().id() == ID_floatbv)
3111  {
3112  // Floating-point additions should have be been converted
3113  // to ID_floatbv_plus during symbolic execution, adding
3114  // the rounding mode. See smt2_convt::convert_floatbv_plus.
3115  UNREACHABLE;
3116  }
3117  else if(expr.type().id() == ID_pointer)
3118  {
3119  if(expr.operands().size() == 2)
3120  {
3121  exprt p = expr.op0(), i = expr.op1();
3122 
3123  if(p.type().id() != ID_pointer)
3124  p.swap(i);
3125 
3127  p.type().id() == ID_pointer,
3128  "one of the operands should have pointer type");
3129 
3130  const auto element_size = pointer_offset_size(expr.type().subtype(), ns);
3131  CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3132 
3133  out << "(bvadd ";
3134  convert_expr(p);
3135  out << " ";
3136 
3137  if(*element_size >= 2)
3138  {
3139  out << "(bvmul ";
3140  convert_expr(i);
3141  out << " (_ bv" << *element_size << " " << boolbv_width(expr.type())
3142  << "))";
3143  }
3144  else
3145  convert_expr(i);
3146 
3147  out << ')';
3148  }
3149  else
3150  {
3152  }
3153  }
3154  else if(expr.type().id() == ID_vector)
3155  {
3156  const vector_typet &vector_type = to_vector_type(expr.type());
3157 
3158  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
3159 
3160  typet index_type = vector_type.size().type();
3161 
3162  if(use_datatypes)
3163  {
3164  const std::string &smt_typename = datatype_map.at(vector_type);
3165 
3166  out << "(mk-" << smt_typename;
3167  }
3168  else
3169  out << "(concat";
3170 
3171  // add component-by-component
3172  for(mp_integer i = 0; i != size; ++i)
3173  {
3174  exprt::operandst summands;
3175  summands.reserve(expr.operands().size());
3176  for(const auto &op : expr.operands())
3177  summands.push_back(index_exprt(
3178  op, from_integer(size - i - 1, index_type), vector_type.subtype()));
3179 
3180  plus_exprt tmp(std::move(summands), vector_type.subtype());
3181 
3182  out << " ";
3183  convert_expr(tmp);
3184  }
3185 
3186  out << ")"; // mk-... or concat
3187  }
3188  else
3189  UNEXPECTEDCASE("unsupported type for +: " + expr.type().id_string());
3190 }
3191 
3197 {
3199 
3200  /* CProver uses the x86 numbering of the rounding-mode
3201  * 0 == FE_TONEAREST
3202  * 1 == FE_DOWNWARD
3203  * 2 == FE_UPWARD
3204  * 3 == FE_TOWARDZERO
3205  * These literal values must be used rather than the macros
3206  * the macros from fenv.h to avoid portability problems.
3207  */
3208 
3209  if(expr.id()==ID_constant)
3210  {
3211  const constant_exprt &cexpr=to_constant_expr(expr);
3212 
3213  mp_integer value = numeric_cast_v<mp_integer>(cexpr);
3214 
3215  if(value==0)
3216  out << "roundNearestTiesToEven";
3217  else if(value==1)
3218  out << "roundTowardNegative";
3219  else if(value==2)
3220  out << "roundTowardPositive";
3221  else if(value==3)
3222  out << "roundTowardZero";
3223  else
3225  false,
3226  "Rounding mode should have value 0, 1, 2, or 3",
3227  id2string(cexpr.get_value()));
3228  }
3229  else
3230  {
3231  std::size_t width=to_bitvector_type(expr.type()).get_width();
3232 
3233  // Need to make the choice above part of the model
3234  out << "(ite (= (_ bv0 " << width << ") ";
3235  convert_expr(expr);
3236  out << ") roundNearestTiesToEven ";
3237 
3238  out << "(ite (= (_ bv1 " << width << ") ";
3239  convert_expr(expr);
3240  out << ") roundTowardNegative ";
3241 
3242  out << "(ite (= (_ bv2 " << width << ") ";
3243  convert_expr(expr);
3244  out << ") roundTowardPositive ";
3245 
3246  // TODO: add some kind of error checking here
3247  out << "roundTowardZero";
3248 
3249  out << ")))";
3250  }
3251 }
3252 
3254 {
3255  const typet &type=expr.type();
3256 
3257  PRECONDITION(
3258  type.id() == ID_floatbv ||
3259  (type.id() == ID_complex && type.subtype().id() == ID_floatbv) ||
3260  (type.id() == ID_vector && type.subtype().id() == ID_floatbv));
3261 
3262  if(use_FPA_theory)
3263  {
3264  if(type.id()==ID_floatbv)
3265  {
3266  out << "(fp.add ";
3268  out << " ";
3269  convert_expr(expr.lhs());
3270  out << " ";
3271  convert_expr(expr.rhs());
3272  out << ")";
3273  }
3274  else if(type.id()==ID_complex)
3275  {
3276  SMT2_TODO("+ for floatbv complex");
3277  }
3278  else if(type.id()==ID_vector)
3279  {
3280  SMT2_TODO("+ for floatbv vector");
3281  }
3282  else
3284  false,
3285  "type should not be one of the unsupported types",
3286  type.id_string());
3287  }
3288  else
3289  convert_floatbv(expr);
3290 }
3291 
3293 {
3294  if(expr.type().id()==ID_integer)
3295  {
3296  out << "(- ";
3297  convert_expr(expr.op0());
3298  out << " ";
3299  convert_expr(expr.op1());
3300  out << ")";
3301  }
3302  else if(expr.type().id()==ID_unsignedbv ||
3303  expr.type().id()==ID_signedbv ||
3304  expr.type().id()==ID_fixedbv)
3305  {
3306  if(expr.op0().type().id()==ID_pointer &&
3307  expr.op1().type().id()==ID_pointer)
3308  {
3309  // Pointer difference
3310  auto element_size = pointer_offset_size(expr.op0().type().subtype(), ns);
3311  CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3312 
3313  if(*element_size >= 2)
3314  out << "(bvsdiv ";
3315 
3316  INVARIANT(
3317  boolbv_width(expr.op0().type()) == boolbv_width(expr.type()),
3318  "bitvector width of operand shall be equal to the bitvector width of "
3319  "the expression");
3320 
3321  out << "(bvsub ";
3322  convert_expr(expr.op0());
3323  out << " ";
3324  convert_expr(expr.op1());
3325  out << ")";
3326 
3327  if(*element_size >= 2)
3328  out << " (_ bv" << *element_size << " " << boolbv_width(expr.type())
3329  << "))";
3330  }
3331  else
3332  {
3333  out << "(bvsub ";
3334  convert_expr(expr.op0());
3335  out << " ";
3336  convert_expr(expr.op1());
3337  out << ")";
3338  }
3339  }
3340  else if(expr.type().id()==ID_floatbv)
3341  {
3342  // Floating-point subtraction should have be been converted
3343  // to ID_floatbv_minus during symbolic execution, adding
3344  // the rounding mode. See smt2_convt::convert_floatbv_minus.
3345  UNREACHABLE;
3346  }
3347  else if(expr.type().id()==ID_pointer)
3348  {
3349  SMT2_TODO("pointer subtraction");
3350  }
3351  else if(expr.type().id()==ID_vector)
3352  {
3353  const vector_typet &vector_type=to_vector_type(expr.type());
3354 
3355  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
3356 
3357  typet index_type=vector_type.size().type();
3358 
3359  if(use_datatypes)
3360  {
3361  const std::string &smt_typename = datatype_map.at(vector_type);
3362 
3363  out << "(mk-" << smt_typename;
3364  }
3365  else
3366  out << "(concat";
3367 
3368  // subtract component-by-component
3369  for(mp_integer i=0; i!=size; ++i)
3370  {
3371  exprt tmp(ID_minus, vector_type.subtype());
3372  forall_operands(it, expr)
3373  tmp.copy_to_operands(
3374  index_exprt(
3375  *it,
3376  from_integer(size-i-1, index_type),
3377  vector_type.subtype()));
3378 
3379  out << " ";
3380  convert_expr(tmp);
3381  }
3382 
3383  out << ")"; // mk-... or concat
3384  }
3385  else
3386  UNEXPECTEDCASE("unsupported type for -: "+expr.type().id_string());
3387 }
3388 
3390 {
3392  expr.type().id() == ID_floatbv,
3393  "type of ieee floating point expression shall be floatbv");
3394 
3395  if(use_FPA_theory)
3396  {
3397  out << "(fp.sub ";
3399  out << " ";
3400  convert_expr(expr.lhs());
3401  out << " ";
3402  convert_expr(expr.rhs());
3403  out << ")";
3404  }
3405  else
3406  convert_floatbv(expr);
3407 }
3408 
3410 {
3411  if(expr.type().id()==ID_unsignedbv ||
3412  expr.type().id()==ID_signedbv)
3413  {
3414  if(expr.type().id()==ID_unsignedbv)
3415  out << "(bvudiv ";
3416  else
3417  out << "(bvsdiv ";
3418 
3419  convert_expr(expr.op0());
3420  out << " ";
3421  convert_expr(expr.op1());
3422  out << ")";
3423  }
3424  else if(expr.type().id()==ID_fixedbv)
3425  {
3426  fixedbv_spect spec(to_fixedbv_type(expr.type()));
3427  std::size_t fraction_bits=spec.get_fraction_bits();
3428 
3429  out << "((_ extract " << spec.width-1 << " 0) ";
3430  out << "(bvsdiv ";
3431 
3432  out << "(concat ";
3433  convert_expr(expr.op0());
3434  out << " (_ bv0 " << fraction_bits << ")) ";
3435 
3436  out << "((_ sign_extend " << fraction_bits << ") ";
3437  convert_expr(expr.op1());
3438  out << ")";
3439 
3440  out << "))";
3441  }
3442  else if(expr.type().id()==ID_floatbv)
3443  {
3444  // Floating-point division should have be been converted
3445  // to ID_floatbv_div during symbolic execution, adding
3446  // the rounding mode. See smt2_convt::convert_floatbv_div.
3447  UNREACHABLE;
3448  }
3449  else
3450  UNEXPECTEDCASE("unsupported type for /: "+expr.type().id_string());
3451 }
3452 
3454 {
3456  expr.type().id() == ID_floatbv,
3457  "type of ieee floating point expression shall be floatbv");
3458 
3459  if(use_FPA_theory)
3460  {
3461  out << "(fp.div ";
3463  out << " ";
3464  convert_expr(expr.lhs());
3465  out << " ";
3466  convert_expr(expr.rhs());
3467  out << ")";
3468  }
3469  else
3470  convert_floatbv(expr);
3471 }
3472 
3474 {
3475  // re-write to binary if needed
3476  if(expr.operands().size()>2)
3477  {
3478  // strip last operand
3479  exprt tmp=expr;
3480  tmp.operands().pop_back();
3481 
3482  // recursive call
3483  return convert_mult(mult_exprt(tmp, expr.operands().back()));
3484  }
3485 
3486  INVARIANT(
3487  expr.operands().size() == 2,
3488  "expression should have been converted to a variant with two operands");
3489 
3490  if(expr.type().id()==ID_unsignedbv ||
3491  expr.type().id()==ID_signedbv)
3492  {
3493  // Note that bvmul is really unsigned,
3494  // but this is irrelevant as we chop-off any extra result
3495  // bits.
3496  out << "(bvmul ";
3497  convert_expr(expr.op0());
3498  out << " ";
3499  convert_expr(expr.op1());
3500  out << ")";
3501  }
3502  else if(expr.type().id()==ID_floatbv)
3503  {
3504  // Floating-point multiplication should have be been converted
3505  // to ID_floatbv_mult during symbolic execution, adding
3506  // the rounding mode. See smt2_convt::convert_floatbv_mult.
3507  UNREACHABLE;
3508  }
3509  else if(expr.type().id()==ID_fixedbv)
3510  {
3511  fixedbv_spect spec(to_fixedbv_type(expr.type()));
3512  std::size_t fraction_bits=spec.get_fraction_bits();
3513 
3514  out << "((_ extract "
3515  << spec.width+fraction_bits-1 << " "
3516  << fraction_bits << ") ";
3517 
3518  out << "(bvmul ";
3519 
3520  out << "((_ sign_extend " << fraction_bits << ") ";
3521  convert_expr(expr.op0());
3522  out << ") ";
3523 
3524  out << "((_ sign_extend " << fraction_bits << ") ";
3525  convert_expr(expr.op1());
3526  out << ")";
3527 
3528  out << "))"; // bvmul, extract
3529  }
3530  else if(expr.type().id()==ID_rational ||
3531  expr.type().id()==ID_integer ||
3532  expr.type().id()==ID_real)
3533  {
3534  out << "(*";
3535 
3536  forall_operands(it, expr)
3537  {
3538  out << " ";
3539  convert_expr(*it);
3540  }
3541 
3542  out << ")";
3543  }
3544  else
3545  UNEXPECTEDCASE("unsupported type for *: "+expr.type().id_string());
3546 }
3547 
3549 {
3551  expr.type().id() == ID_floatbv,
3552  "type of ieee floating point expression shall be floatbv");
3553 
3554  if(use_FPA_theory)
3555  {
3556  out << "(fp.mul ";
3558  out << " ";
3559  convert_expr(expr.lhs());
3560  out << " ";
3561  convert_expr(expr.rhs());
3562  out << ")";
3563  }
3564  else
3565  convert_floatbv(expr);
3566 }
3567 
3569 {
3570  // get rid of "with" that has more than three operands
3571 
3572  if(expr.operands().size()>3)
3573  {
3574  std::size_t s=expr.operands().size();
3575 
3576  // strip off the trailing two operands
3577  with_exprt tmp = expr;
3578  tmp.operands().resize(s-2);
3579 
3580  with_exprt new_with_expr(
3581  tmp, expr.operands()[s - 2], expr.operands().back());
3582 
3583  // recursive call
3584  return convert_with(new_with_expr);
3585  }
3586 
3587  INVARIANT(
3588  expr.operands().size() == 3,
3589  "with expression should have been converted to a version with three "
3590  "operands above");
3591 
3592  const typet &expr_type = expr.type();
3593 
3594  if(expr_type.id()==ID_array)
3595  {
3596  const array_typet &array_type=to_array_type(expr_type);
3597 
3598  if(use_array_theory(expr))
3599  {
3600  out << "(store ";
3601  convert_expr(expr.old());
3602  out << " ";
3603  convert_expr(typecast_exprt(expr.where(), array_type.size().type()));
3604  out << " ";
3605  convert_expr(expr.new_value());
3606  out << ")";
3607  }
3608  else
3609  {
3610  // fixed-width
3611  std::size_t array_width=boolbv_width(array_type);
3612  std::size_t sub_width=boolbv_width(array_type.subtype());
3613  std::size_t index_width=boolbv_width(expr.where().type());
3614 
3615  // We mask out the updated bits with AND,
3616  // and then OR-in the shifted new value.
3617 
3618  out << "(let ((distance? ";
3619  out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
3620 
3621  // SMT2 says that the shift distance needs to be as wide
3622  // as the stuff we are shifting.
3623  if(array_width>index_width)
3624  {
3625  out << "((_ zero_extend " << array_width-index_width << ") ";
3626  convert_expr(expr.where());
3627  out << ")";
3628  }
3629  else
3630  {
3631  out << "((_ extract " << array_width-1 << " 0) ";
3632  convert_expr(expr.where());
3633  out << ")";
3634  }
3635 
3636  out << "))) "; // bvmul, distance?
3637 
3638  out << "(bvor ";
3639  out << "(bvand ";
3640  out << "(bvnot ";
3641  out << "(bvshl (_ bv" << power(2, sub_width) - 1 << " " << array_width
3642  << ") ";
3643  out << "distance?)) "; // bvnot, bvlshl
3644  convert_expr(expr.old());
3645  out << ") "; // bvand
3646  out << "(bvshl ";
3647  out << "((_ zero_extend " << array_width-sub_width << ") ";
3648  convert_expr(expr.new_value());
3649  out << ") distance?)))"; // zero_extend, bvshl, bvor, let
3650  }
3651  }
3652  else if(expr_type.id() == ID_struct || expr_type.id() == ID_struct_tag)
3653  {
3654  const struct_typet &struct_type = to_struct_type(ns.follow(expr_type));
3655 
3656  const exprt &index = expr.where();
3657  const exprt &value = expr.new_value();
3658 
3659  const irep_idt &component_name=index.get(ID_component_name);
3660 
3661  INVARIANT(
3662  struct_type.has_component(component_name),
3663  "struct should have accessed component");
3664 
3665  if(use_datatypes)
3666  {
3667  const std::string &smt_typename = datatype_map.at(expr_type);
3668 
3669  out << "(update-" << smt_typename << "." << component_name << " ";
3670  convert_expr(expr.old());
3671  out << " ";
3672  convert_expr(value);
3673  out << ")";
3674  }
3675  else
3676  {
3677  std::size_t struct_width=boolbv_width(struct_type);
3678 
3679  // figure out the offset and width of the member
3681  boolbv_width.get_member(struct_type, component_name);
3682 
3683  out << "(let ((?withop ";
3684  convert_expr(expr.old());
3685  out << ")) ";
3686 
3687  if(m.width==struct_width)
3688  {
3689  // the struct is the same as the member, no concat needed,
3690  // ?withop won't be used
3691  convert_expr(value);
3692  }
3693  else if(m.offset==0)
3694  {
3695  // the member is at the beginning
3696  out << "(concat "
3697  << "((_ extract " << (struct_width-1) << " "
3698  << m.width << ") ?withop) ";
3699  convert_expr(value);
3700  out << ")"; // concat
3701  }
3702  else if(m.offset+m.width==struct_width)
3703  {
3704  // the member is at the end
3705  out << "(concat ";
3706  convert_expr(value);
3707  out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))";
3708  }
3709  else
3710  {
3711  // most general case, need two concat-s
3712  out << "(concat (concat "
3713  << "((_ extract " << (struct_width-1) << " "
3714  << (m.offset+m.width) << ") ?withop) ";
3715  convert_expr(value);
3716  out << ") ((_ extract " << (m.offset-1) << " 0) ?withop)";
3717  out << ")"; // concat
3718  }
3719 
3720  out << ")"; // let ?withop
3721  }
3722  }
3723  else if(expr_type.id() == ID_union || expr_type.id() == ID_union_tag)
3724  {
3725  const union_typet &union_type = to_union_type(ns.follow(expr_type));
3726 
3727  const exprt &value = expr.new_value();
3728 
3729  std::size_t total_width=boolbv_width(union_type);
3731  total_width != 0, "failed to get union width for with");
3732 
3733  std::size_t member_width=boolbv_width(value.type());
3735  member_width != 0, "failed to get union member width for with");
3736 
3737  if(total_width==member_width)
3738  {
3739  flatten2bv(value);
3740  }
3741  else
3742  {
3743  INVARIANT(
3744  total_width > member_width,
3745  "total width should be greater than member_width as member_width is at "
3746  "most as large as total_width and the other case has been handled "
3747  "above");
3748  out << "(concat ";
3749  out << "((_ extract "
3750  << (total_width-1)
3751  << " " << member_width << ") ";
3752  convert_expr(expr.old());
3753  out << ") ";
3754  flatten2bv(value);
3755  out << ")";
3756  }
3757  }
3758  else if(expr_type.id()==ID_bv ||
3759  expr_type.id()==ID_unsignedbv ||
3760  expr_type.id()==ID_signedbv)
3761  {
3762  // Update bits in a bit-vector. We will use masking and shifts.
3763 
3764  std::size_t total_width=boolbv_width(expr_type);
3766  total_width != 0, "failed to get total width");
3767 
3768  const exprt &index=expr.operands()[1];
3769  const exprt &value=expr.operands()[2];
3770 
3771  std::size_t value_width=boolbv_width(value.type());
3773  value_width != 0, "failed to get value width");
3774 
3775  typecast_exprt index_tc(index, expr_type);
3776 
3777  // TODO: SMT2-ify
3778  SMT2_TODO("SMT2-ify");
3779 
3780 #if 0
3781  out << "(bvor ";
3782  out << "(band ";
3783 
3784  // the mask to get rid of the old bits
3785  out << " (bvnot (bvshl";
3786 
3787  out << " (concat";
3788  out << " (repeat[" << total_width-value_width << "] bv0[1])";
3789  out << " (repeat[" << value_width << "] bv1[1])";
3790  out << ")"; // concat
3791 
3792  // shift it to the index
3793  convert_expr(index_tc);
3794  out << "))"; // bvshl, bvot
3795 
3796  out << ")"; // bvand
3797 
3798  // the new value
3799  out << " (bvshl ";
3800  convert_expr(value);
3801 
3802  // shift it to the index
3803  convert_expr(index_tc);
3804  out << ")"; // bvshl
3805 
3806  out << ")"; // bvor
3807 #endif
3808  }
3809  else
3811  "with expects struct, union, or array type, but got "+
3812  expr.type().id_string());
3813 }
3814 
3816 {
3817  PRECONDITION(expr.operands().size() == 3);
3818 
3819  SMT2_TODO("smt2_convt::convert_update to be implemented");
3820 }
3821 
3823 {
3824  const typet &array_op_type = expr.array().type();
3825 
3826  if(array_op_type.id()==ID_array)
3827  {
3828  const array_typet &array_type=to_array_type(array_op_type);
3829 
3830  if(use_array_theory(expr.array()))
3831  {
3832  if(expr.type().id() == ID_bool && !use_array_of_bool)
3833  {
3834  out << "(= ";
3835  out << "(select ";
3836  convert_expr(expr.array());
3837  out << " ";
3838  convert_expr(typecast_exprt(expr.index(), array_type.size().type()));
3839  out << ")";
3840  out << " #b1 #b0)";
3841  }
3842  else
3843  {
3844  out << "(select ";
3845  convert_expr(expr.array());
3846  out << " ";
3847  convert_expr(typecast_exprt(expr.index(), array_type.size().type()));
3848  out << ")";
3849  }
3850  }
3851  else
3852  {
3853  // fixed size
3854  std::size_t array_width=boolbv_width(array_type);
3855  CHECK_RETURN(array_width != 0);
3856 
3857  unflatten(wheret::BEGIN, array_type.subtype());
3858 
3859  std::size_t sub_width=boolbv_width(array_type.subtype());
3860  std::size_t index_width=boolbv_width(expr.index().type());
3861 
3862  out << "((_ extract " << sub_width-1 << " 0) ";
3863  out << "(bvlshr ";
3864  convert_expr(expr.array());
3865  out << " ";
3866  out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
3867 
3868  // SMT2 says that the shift distance must be the same as
3869  // the width of what we shift.
3870  if(array_width>index_width)
3871  {
3872  out << "((_ zero_extend " << array_width-index_width << ") ";
3873  convert_expr(expr.index());
3874  out << ")"; // zero_extend
3875  }
3876  else
3877  {
3878  out << "((_ extract " << array_width-1 << " 0) ";
3879  convert_expr(expr.index());
3880  out << ")"; // extract
3881  }
3882 
3883  out << ")))"; // mult, bvlshr, extract
3884 
3885  unflatten(wheret::END, array_type.subtype());
3886  }
3887  }
3888  else if(array_op_type.id()==ID_vector)
3889  {
3890  const vector_typet &vector_type=to_vector_type(array_op_type);
3891 
3892  if(use_datatypes)
3893  {
3894  const std::string &smt_typename = datatype_map.at(vector_type);
3895 
3896  // this is easy for constant indicies
3897 
3898  const auto index_int = numeric_cast<mp_integer>(expr.index());
3899  if(!index_int.has_value())
3900  {
3901  SMT2_TODO("non-constant index on vectors");
3902  }
3903  else
3904  {
3905  out << "(" << smt_typename << "." << *index_int << " ";
3906  convert_expr(expr.array());
3907  out << ")";
3908  }
3909  }
3910  else
3911  {
3912  SMT2_TODO("index on vectors");
3913  }
3914  }
3915  else
3916  INVARIANT(
3917  false, "index with unsupported array type: " + array_op_type.id_string());
3918 }
3919 
3921 {
3922  const member_exprt &member_expr=to_member_expr(expr);
3923  const exprt &struct_op=member_expr.struct_op();
3924  const typet &struct_op_type = struct_op.type();
3925  const irep_idt &name=member_expr.get_component_name();
3926 
3927  if(struct_op_type.id() == ID_struct || struct_op_type.id() == ID_struct_tag)
3928  {
3929  const struct_typet &struct_type = to_struct_type(ns.follow(struct_op_type));
3930 
3931  INVARIANT(
3932  struct_type.has_component(name), "struct should have accessed component");
3933 
3934  if(use_datatypes)
3935  {
3936  const std::string &smt_typename = datatype_map.at(struct_type);
3937 
3938  out << "(" << smt_typename << "."
3939  << struct_type.get_component(name).get_name()
3940  << " ";
3941  convert_expr(struct_op);
3942  out << ")";
3943  }
3944  else
3945  {
3946  // we extract
3947  const std::size_t member_width = boolbv_width(expr.type());
3948  const auto member_offset = member_offset_bits(struct_type, name, ns);
3949 
3951  member_offset.has_value(), "failed to get struct member offset");
3952 
3953  out << "((_ extract " << (member_offset.value() + member_width - 1) << " "
3954  << member_offset.value() << ") ";
3955  convert_expr(struct_op);
3956  out << ")";
3957  }
3958  }
3959  else if(
3960  struct_op_type.id() == ID_union || struct_op_type.id() == ID_union_tag)
3961  {
3962  std::size_t width=boolbv_width(expr.type());
3964  width != 0, "failed to get union member width");
3965 
3966  unflatten(wheret::BEGIN, expr.type());
3967 
3968  out << "((_ extract "
3969  << (width-1)
3970  << " 0) ";
3971  convert_expr(struct_op);
3972  out << ")";
3973 
3974  unflatten(wheret::END, expr.type());
3975  }
3976  else
3978  "convert_member on an unexpected type "+struct_op_type.id_string());
3979 }
3980 
3982 {
3983  const typet &type = expr.type();
3984 
3985  if(type.id()==ID_bool)
3986  {
3987  out << "(ite ";
3988  convert_expr(expr); // this returns a Bool
3989  out << " #b1 #b0)"; // this is a one-bit bit-vector
3990  }
3991  else if(type.id()==ID_vector)
3992  {
3993  if(use_datatypes)
3994  {
3995  const std::string &smt_typename = datatype_map.at(type);
3996 
3997  // concatenate elements
3998  const vector_typet &vector_type=to_vector_type(type);
3999 
4000  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
4001 
4002  out << "(let ((?vflop ";
4003  convert_expr(expr);
4004  out << ")) ";
4005 
4006  out << "(concat";
4007 
4008  for(mp_integer i=0; i!=size; ++i)
4009  {
4010  out << " (" << smt_typename << "." << i << " ?vflop)";
4011  }
4012 
4013  out << "))"; // concat, let
4014  }
4015  else
4016  convert_expr(expr); // already a bv
4017  }
4018  else if(type.id()==ID_array)
4019  {
4020  convert_expr(expr);
4021  }
4022  else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4023  {
4024  if(use_datatypes)
4025  {
4026  const std::string &smt_typename = datatype_map.at(type);
4027 
4028  // concatenate elements
4029  const struct_typet &struct_type = to_struct_type(ns.follow(type));
4030 
4031  out << "(let ((?sflop ";
4032  convert_expr(expr);
4033  out << ")) ";
4034 
4035  const struct_typet::componentst &components=
4036  struct_type.components();
4037 
4038  // SMT-LIB 2 concat is binary only
4039  for(std::size_t i=components.size(); i>1; i--)
4040  {
4041  out << "(concat (" << smt_typename << "."
4042  << components[i-1].get_name() << " ?sflop)";
4043 
4044  out << " ";
4045  }
4046 
4047  out << "(" << smt_typename << "."
4048  << components[0].get_name() << " ?sflop)";
4049 
4050  for(std::size_t i=1; i<components.size(); i++)
4051  out << ")"; // concat
4052 
4053  out << ")"; // let
4054  }
4055  else
4056  convert_expr(expr);
4057  }
4058  else if(type.id()==ID_floatbv)
4059  {
4060  INVARIANT(
4061  !use_FPA_theory,
4062  "floatbv expressions should be flattened when using FPA theory");
4063 
4064  convert_expr(expr);
4065  }
4066  else
4067  convert_expr(expr);
4068 }
4069 
4071  wheret where,
4072  const typet &type,
4073  unsigned nesting)
4074 {
4075  if(type.id()==ID_bool)
4076  {
4077  if(where==wheret::BEGIN)
4078  out << "(= "; // produces a bool
4079  else
4080  out << " #b1)";
4081  }
4082  else if(type.id()==ID_vector)
4083  {
4084  if(use_datatypes)
4085  {
4086  const std::string &smt_typename = datatype_map.at(type);
4087 
4088  // extract elements
4089  const vector_typet &vector_type=to_vector_type(type);
4090 
4091  std::size_t subtype_width=boolbv_width(vector_type.subtype());
4092 
4093  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
4094 
4095  if(where==wheret::BEGIN)
4096  out << "(let ((?ufop" << nesting << " ";
4097  else
4098  {
4099  out << ")) ";
4100 
4101  out << "(mk-" << smt_typename;
4102 
4103  std::size_t offset=0;
4104 
4105  for(mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4106  {
4107  out << " ";
4108  unflatten(wheret::BEGIN, vector_type.subtype(), nesting+1);
4109  out << "((_ extract " << offset+subtype_width-1 << " "
4110  << offset << ") ?ufop" << nesting << ")";
4111  unflatten(wheret::END, vector_type.subtype(), nesting+1);
4112  }
4113 
4114  out << "))"; // mk-, let
4115  }
4116  }
4117  else
4118  {
4119  // nop, already a bv
4120  }
4121  }
4122  else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4123  {
4124  if(use_datatypes)
4125  {
4126  // extract members
4127  if(where==wheret::BEGIN)
4128  out << "(let ((?ufop" << nesting << " ";
4129  else
4130  {
4131  out << ")) ";
4132 
4133  const std::string &smt_typename = datatype_map.at(type);
4134 
4135  out << "(mk-" << smt_typename;
4136 
4137  const struct_typet &struct_type = to_struct_type(ns.follow(type));
4138 
4139  const struct_typet::componentst &components=
4140  struct_type.components();
4141 
4142  std::size_t offset=0;
4143 
4144  std::size_t i=0;
4145  for(struct_typet::componentst::const_iterator
4146  it=components.begin();
4147  it!=components.end();
4148  it++, i++)
4149  {
4150  std::size_t member_width=boolbv_width(it->type());
4151 
4152  out << " ";
4153  unflatten(wheret::BEGIN, it->type(), nesting+1);
4154  out << "((_ extract " << offset+member_width-1 << " "
4155  << offset << ") ?ufop" << nesting << ")";
4156  unflatten(wheret::END, it->type(), nesting+1);
4157  offset+=member_width;
4158  }
4159 
4160  out << "))"; // mk-, let
4161  }
4162  }
4163  else
4164  {
4165  // nop, already a bv
4166  }
4167  }
4168  else
4169  {
4170  // nop
4171  }
4172 }
4173 
4174 void smt2_convt::set_to(const exprt &expr, bool value)
4175 {
4176  PRECONDITION(expr.type().id() == ID_bool);
4177 
4178  if(expr.id()==ID_and && value)
4179  {
4180  forall_operands(it, expr)
4181  set_to(*it, true);
4182  return;
4183  }
4184 
4185  if(expr.id()==ID_or && !value)
4186  {
4187  forall_operands(it, expr)
4188  set_to(*it, false);
4189  return;
4190  }
4191 
4192  if(expr.id()==ID_not)
4193  {
4194  return set_to(to_not_expr(expr).op(), !value);
4195  }
4196 
4197  out << "\n";
4198 
4199  // special treatment for "set_to(a=b, true)" where
4200  // a is a new symbol
4201 
4202  if(expr.id() == ID_equal && value)
4203  {
4204  const equal_exprt &equal_expr=to_equal_expr(expr);
4205 
4206  if(equal_expr.lhs().id()==ID_symbol)
4207  {
4208  const irep_idt &identifier=
4209  to_symbol_expr(equal_expr.lhs()).get_identifier();
4210 
4211  if(identifier_map.find(identifier)==identifier_map.end())
4212  {
4213  identifiert &id=identifier_map[identifier];
4214  CHECK_RETURN(id.type.is_nil());
4215 
4216  id.type=equal_expr.lhs().type();
4217  find_symbols(id.type);
4218  exprt prepared_rhs = prepare_for_convert_expr(equal_expr.rhs());
4219 
4220  std::string smt2_identifier=convert_identifier(identifier);
4221  smt2_identifiers.insert(smt2_identifier);
4222 
4223  out << "; set_to true (equal)\n";
4224  out << "(define-fun |" << smt2_identifier << "| () ";
4225 
4226  convert_type(equal_expr.lhs().type());
4227  out << " ";
4228  convert_expr(prepared_rhs);
4229 
4230  out << ")" << "\n";
4231  return; // done
4232  }
4233  }
4234  }
4235 
4236  exprt prepared_expr = prepare_for_convert_expr(expr);
4237 
4238 #if 0
4239  out << "; CONV: "
4240  << format(expr) << "\n";
4241 #endif
4242 
4243  out << "; set_to " << (value?"true":"false") << "\n"
4244  << "(assert ";
4245 
4246  if(!value)
4247  {
4248  out << "(not ";
4249  convert_expr(prepared_expr);
4250  out << ")";
4251  }
4252  else
4253  convert_expr(prepared_expr);
4254 
4255  out << ")" << "\n"; // assert
4256 
4257  return;
4258 }
4259 
4267 {
4268  exprt lowered_expr = expr;
4269 
4270  for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end();
4271  it != itend;
4272  ++it)
4273  {
4274  if(
4275  it->id() == ID_byte_extract_little_endian ||
4276  it->id() == ID_byte_extract_big_endian)
4277  {
4278  it.mutate() = lower_byte_extract(to_byte_extract_expr(*it), ns);
4279  }
4280  else if(
4281  it->id() == ID_byte_update_little_endian ||
4282  it->id() == ID_byte_update_big_endian)
4283  {
4284  it.mutate() = lower_byte_update(to_byte_update_expr(*it), ns);
4285  }
4286  }
4287 
4288  return lowered_expr;
4289 }
4290 
4299 {
4300  // First, replace byte operators, because they may introduce new array
4301  // expressions that must be seen by find_symbols:
4302  exprt lowered_expr = lower_byte_operators(expr);
4303  INVARIANT(
4304  !has_byte_operator(lowered_expr),
4305  "lower_byte_operators should remove all byte operators");
4306 
4307  // Now create symbols for all composite expressions present in lowered_expr:
4308  find_symbols(lowered_expr);
4309 
4310  return lowered_expr;
4311 }
4312 
4314 {
4315  // recursive call on type
4316  find_symbols(expr.type());
4317 
4318  if(expr.id() == ID_exists || expr.id() == ID_forall)
4319  {
4320  // do not declare the quantified symbol, but record
4321  // as 'bound symbol'
4322  const auto &q_expr = to_quantifier_expr(expr);
4323  const auto identifier = q_expr.symbol().get_identifier();
4324  identifiert &id = identifier_map[identifier];
4325  id.type = q_expr.symbol().type();
4326  id.is_bound = true;
4327  find_symbols(q_expr.where());
4328  return;
4329  }
4330 
4331  // recursive call on operands
4332  forall_operands(it, expr)
4333  find_symbols(*it);
4334 
4335  if(expr.id()==ID_symbol ||
4336  expr.id()==ID_nondet_symbol)
4337  {
4338  // we don't track function-typed symbols
4339  if(expr.type().id()==ID_code)
4340  return;
4341 
4342  irep_idt identifier;
4343 
4344  if(expr.id()==ID_symbol)
4345  identifier=to_symbol_expr(expr).get_identifier();
4346  else
4347  identifier="nondet_"+
4348  id2string(to_nondet_symbol_expr(expr).get_identifier());
4349 
4350  identifiert &id=identifier_map[identifier];
4351 
4352  if(id.type.is_nil())
4353  {
4354  id.type=expr.type();
4355 
4356  std::string smt2_identifier=convert_identifier(identifier);
4357  smt2_identifiers.insert(smt2_identifier);
4358 
4359  out << "; find_symbols\n";
4360  out << "(declare-fun |"
4361  << smt2_identifier
4362  << "| () ";
4363  convert_type(expr.type());
4364  out << ")" << "\n";
4365  }
4366  }
4367  else if(expr.id()==ID_array_of)
4368  {
4369  if(defined_expressions.find(expr)==defined_expressions.end())
4370  {
4371  const irep_idt id =
4372  "array_of." + std::to_string(defined_expressions.size());
4373  out << "; the following is a substitute for lambda i. x" << "\n";
4374  out << "(declare-fun " << id << " () ";
4375  convert_type(expr.type());
4376  out << ")" << "\n";
4377 
4378  // use a quantifier instead of the lambda
4379  #if 0 // not really working in any solver yet!
4380  out << "(assert (forall ((i ";
4381  convert_type(array_index_type());
4382  out << ")) (= (select " << id << " i) ";
4383  convert_expr(expr.op0());
4384  out << ")))" << "\n";
4385  #endif
4386 
4387  defined_expressions[expr]=id;
4388  }
4389  }
4390  else if(expr.id()==ID_array)
4391  {
4392  if(defined_expressions.find(expr)==defined_expressions.end())
4393  {
4394  const array_typet &array_type=to_array_type(expr.type());
4395 
4396  const irep_idt id = "array." + std::to_string(defined_expressions.size());
4397  out << "; the following is a substitute for an array constructor" << "\n";
4398  out << "(declare-fun " << id << " () ";
4399  convert_type(array_type);
4400  out << ")" << "\n";
4401 
4402  for(std::size_t i=0; i<expr.operands().size(); i++)
4403  {
4404  out << "(assert (= (select " << id << " ";
4405  convert_expr(from_integer(i, array_type.size().type()));
4406  out << ") "; // select
4407  convert_expr(expr.operands()[i]);
4408  out << "))" << "\n"; // =, assert
4409  }
4410 
4411  defined_expressions[expr]=id;
4412  }
4413  }
4414  else if(expr.id()==ID_string_constant)
4415  {
4416  if(defined_expressions.find(expr)==defined_expressions.end())
4417  {
4418  // introduce a temporary array.
4420  const array_typet &array_type=to_array_type(tmp.type());
4421 
4422  const irep_idt id =
4423  "string." + std::to_string(defined_expressions.size());
4424  out << "; the following is a substitute for a string" << "\n";
4425  out << "(declare-fun " << id << " () ";
4426  convert_type(array_type);
4427  out << ")" << "\n";
4428 
4429  for(std::size_t i=0; i<tmp.operands().size(); i++)
4430  {
4431  out << "(assert (= (select " << id;
4432  convert_expr(from_integer(i, array_type.size().type()));
4433  out << ") "; // select
4434  convert_expr(tmp.operands()[i]);
4435  out << "))" << "\n";
4436  }
4437 
4438  defined_expressions[expr]=id;
4439  }
4440  }
4441  else if(expr.id() == ID_object_size)
4442  {
4443  const exprt &op = to_unary_expr(expr).op();
4444 
4445  if(op.type().id()==ID_pointer)
4446  {
4447  if(object_sizes.find(expr)==object_sizes.end())
4448  {
4449  const irep_idt id =
4450  "object_size." + std::to_string(object_sizes.size());
4451  out << "(declare-fun " << id << " () ";
4452  convert_type(expr.type());
4453  out << ")" << "\n";
4454 
4455  object_sizes[expr]=id;
4456  }
4457  }
4458  }
4459  // clang-format off
4460  else if(!use_FPA_theory &&
4461  expr.operands().size() >= 1 &&
4462  (expr.id() == ID_floatbv_plus ||
4463  expr.id() == ID_floatbv_minus ||
4464  expr.id() == ID_floatbv_mult ||
4465  expr.id() == ID_floatbv_div ||
4466  expr.id() == ID_floatbv_typecast ||
4467  expr.id() == ID_ieee_float_equal ||
4468  expr.id() == ID_ieee_float_notequal ||
4469  ((expr.id() == ID_lt ||
4470  expr.id() == ID_gt ||
4471  expr.id() == ID_le ||
4472  expr.id() == ID_ge ||
4473  expr.id() == ID_isnan ||
4474  expr.id() == ID_isnormal ||
4475  expr.id() == ID_isfinite ||
4476  expr.id() == ID_isinf ||
4477  expr.id() == ID_sign ||
4478  expr.id() == ID_unary_minus ||
4479  expr.id() == ID_typecast ||
4480  expr.id() == ID_abs) &&
4481  to_multi_ary_expr(expr).op0().type().id() == ID_floatbv)))
4482  // clang-format on
4483  {
4484  irep_idt function=
4485  "|float_bv."+expr.id_string()+floatbv_suffix(expr)+"|";
4486 
4487  if(bvfp_set.insert(function).second)
4488  {
4489  out << "; this is a model for " << expr.id() << " : "
4490  << type2id(to_multi_ary_expr(expr).op0().type()) << " -> "
4491  << type2id(expr.type()) << "\n"
4492  << "(define-fun " << function << " (";
4493 
4494  for(std::size_t i = 0; i < expr.operands().size(); i++)
4495  {
4496  if(i!=0)
4497  out << " ";
4498  out << "(op" << i << ' ';
4499  convert_type(expr.operands()[i].type());
4500  out << ')';
4501  }
4502 
4503  out << ") ";
4504  convert_type(expr.type()); // return type
4505  out << ' ';
4506 
4507  exprt tmp1=expr;
4508  for(std::size_t i = 0; i < tmp1.operands().size(); i++)
4509  tmp1.operands()[i]=
4510  smt2_symbolt("op"+std::to_string(i), tmp1.operands()[i].type());
4511 
4512  exprt tmp2=float_bv(tmp1);
4513  tmp2=letify(tmp2);
4514  CHECK_RETURN(!tmp2.is_nil());
4515 
4516  convert_expr(tmp2);
4517 
4518  out << ")\n"; // define-fun
4519  }
4520  }
4521 }
4522 
4524 {
4525  const typet &type = expr.type();
4526  PRECONDITION(type.id()==ID_array);
4527 
4528  if(use_datatypes)
4529  {
4530  return true; // always use array theory when we have datatypes
4531  }
4532  else
4533  {
4534  // arrays inside structs get flattened
4535  if(expr.id()==ID_with)
4536  return use_array_theory(to_with_expr(expr).old());
4537  else if(expr.id()==ID_member)
4538  return false;
4539  else
4540  return true;
4541  }
4542 }
4543 
4545 {
4546  if(type.id()==ID_array)
4547  {
4548  const array_typet &array_type=to_array_type(type);
4549  CHECK_RETURN(array_type.size().is_not_nil());
4550 
4551  // we always use array theory for top-level arrays
4552  const typet &subtype = array_type.subtype();
4553 
4554  out << "(Array ";
4555  convert_type(array_type.size().type());
4556  out << " ";
4557 
4558  if(subtype.id()==ID_bool && !use_array_of_bool)
4559  out << "(_ BitVec 1)";
4560  else
4561  convert_type(array_type.subtype());
4562 
4563  out << ")";
4564  }
4565  else if(type.id()==ID_bool)
4566  {
4567  out << "Bool";
4568  }
4569  else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4570  {
4571  if(use_datatypes)
4572  {
4573  out << datatype_map.at(type);
4574  }
4575  else
4576  {
4577  std::size_t width=boolbv_width(type);
4579  width != 0, "failed to get width of struct");
4580 
4581  out << "(_ BitVec " << width << ")";
4582  }
4583  }
4584  else if(type.id()==ID_vector)
4585  {
4586  if(use_datatypes)
4587  {
4588  out << datatype_map.at(type);
4589  }
4590  else
4591  {
4592  std::size_t width=boolbv_width(type);
4594  width != 0, "failed to get width of vector");
4595 
4596  out << "(_ BitVec " << width << ")";
4597  }
4598  }
4599  else if(type.id()==ID_code)
4600  {
4601  // These may appear in structs.
4602  // We replace this by "Bool" in order to keep the same
4603  // member count.
4604  out << "Bool";
4605  }
4606  else if(type.id() == ID_union || type.id() == ID_union_tag)
4607  {
4608  std::size_t width=boolbv_width(type);
4609  CHECK_RETURN_WITH_DIAGNOSTICS(width != 0, "failed to get width of union");
4610 
4611  out << "(_ BitVec " << width << ")";
4612  }
4613  else if(type.id()==ID_pointer)
4614  {
4615  out << "(_ BitVec "
4616  << boolbv_width(type) << ")";
4617  }
4618  else if(type.id()==ID_bv ||
4619  type.id()==ID_fixedbv ||
4620  type.id()==ID_unsignedbv ||
4621  type.id()==ID_signedbv ||
4622  type.id()==ID_c_bool)
4623  {
4624  out << "(_ BitVec "
4625  << to_bitvector_type(type).get_width() << ")";
4626  }
4627  else if(type.id()==ID_c_enum)
4628  {
4629  // these have a subtype
4630  out << "(_ BitVec "
4631  << to_bitvector_type(type.subtype()).get_width() << ")";
4632  }
4633  else if(type.id()==ID_c_enum_tag)
4634  {
4636  }
4637  else if(type.id()==ID_floatbv)
4638  {
4639  const floatbv_typet &floatbv_type=to_floatbv_type(type);
4640 
4641  if(use_FPA_theory)
4642  out << "(_ FloatingPoint "
4643  << floatbv_type.get_e() << " "
4644  << floatbv_type.get_f() + 1 << ")";
4645  else
4646  out << "(_ BitVec "
4647  << floatbv_type.get_width() << ")";
4648  }
4649  else if(type.id()==ID_rational ||
4650  type.id()==ID_real)
4651  out << "Real";
4652  else if(type.id()==ID_integer)
4653  out << "Int";
4654  else if(type.id()==ID_complex)
4655  {
4656  if(use_datatypes)
4657  {
4658  out << datatype_map.at(type);
4659  }
4660  else
4661  {
4662  std::size_t width=boolbv_width(type);
4664  width != 0, "failed to get width of complex");
4665 
4666  out << "(_ BitVec " << width << ")";
4667  }
4668  }
4669  else if(type.id()==ID_c_bit_field)
4670  {
4672  }
4673  else
4674  {
4675  UNEXPECTEDCASE("unsupported type: "+type.id_string());
4676  }
4677 }
4678 
4680 {
4681  std::set<irep_idt> recstack;
4682  find_symbols_rec(type, recstack);
4683 }
4684 
4686  const typet &type,
4687  std::set<irep_idt> &recstack)
4688 {
4689  if(type.id()==ID_array)
4690  {
4691  const array_typet &array_type=to_array_type(type);
4692  find_symbols(array_type.size());
4693  find_symbols_rec(array_type.subtype(), recstack);
4694  }
4695  else if(type.id()==ID_complex)
4696  {
4697  find_symbols_rec(type.subtype(), recstack);
4698 
4699  if(use_datatypes &&
4700  datatype_map.find(type)==datatype_map.end())
4701  {
4702  const std::string smt_typename =
4703  "complex." + std::to_string(datatype_map.size());
4704  datatype_map[type] = smt_typename;
4705 
4706  out << "(declare-datatypes () ((" << smt_typename << " "
4707  << "(mk-" << smt_typename;
4708 
4709  out << " (" << smt_typename << ".imag ";
4710  convert_type(type.subtype());
4711  out << ")";
4712 
4713  out << " (" << smt_typename << ".real ";
4714  convert_type(type.subtype());
4715  out << ")";
4716 
4717  out << "))))\n";
4718  }
4719  }
4720  else if(type.id()==ID_vector)
4721  {
4722  find_symbols_rec(type.subtype(), recstack);
4723 
4724  if(use_datatypes &&
4725  datatype_map.find(type)==datatype_map.end())
4726  {
4727  const vector_typet &vector_type=to_vector_type(type);
4728 
4729  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
4730 
4731  const std::string smt_typename =
4732  "vector." + std::to_string(datatype_map.size());
4733  datatype_map[type] = smt_typename;
4734 
4735  out << "(declare-datatypes () ((" << smt_typename << " "
4736  << "(mk-" << smt_typename;
4737 
4738  for(mp_integer i=0; i!=size; ++i)
4739  {
4740  out << " (" << smt_typename << "." << i << " ";
4741  convert_type(type.subtype());
4742  out << ")";
4743  }
4744 
4745  out << "))))\n";
4746  }
4747  }
4748  else if(type.id() == ID_struct)
4749  {
4750  // Cater for mutually recursive struct types
4751  bool need_decl=false;
4752  if(use_datatypes &&
4753  datatype_map.find(type)==datatype_map.end())
4754  {
4755  const std::string smt_typename =
4756  "struct." + std::to_string(datatype_map.size());
4757  datatype_map[type] = smt_typename;
4758  need_decl=true;
4759  }
4760 
4761  const struct_typet::componentst &components =
4762  to_struct_type(type).components();
4763 
4764  for(const auto &component : components)
4765  find_symbols_rec(component.type(), recstack);
4766 
4767  // Declare the corresponding SMT type if we haven't already.
4768  if(need_decl)
4769  {
4770  const std::string &smt_typename = datatype_map.at(type);
4771 
4772  // We're going to create a datatype named something like `struct.0'.
4773  // It's going to have a single constructor named `mk-struct.0' with an
4774  // argument for each member of the struct. The declaration that
4775  // creates this type looks like:
4776  //
4777  // (declare-datatypes () ((struct.0 (mk-struct.0
4778  // (struct.0.component1 type1)
4779  // ...
4780  // (struct.0.componentN typeN)))))
4781  out << "(declare-datatypes () ((" << smt_typename << " "
4782  << "(mk-" << smt_typename << " ";
4783 
4784  for(const auto &component : components)
4785  {
4786  out << "(" << smt_typename << "." << component.get_name()
4787  << " ";
4788  convert_type(component.type());
4789  out << ") ";
4790  }
4791 
4792  out << "))))" << "\n";
4793 
4794  // Let's also declare convenience functions to update individual
4795  // members of the struct whil we're at it. The functions are
4796  // named like `update-struct.0.component1'. Their declarations
4797  // look like:
4798  //
4799  // (declare-fun update-struct.0.component1
4800  // ((s struct.0) ; first arg -- the struct to update
4801  // (v type1)) ; second arg -- the value to update
4802  // struct.0 ; the output type
4803  // (mk-struct.0 ; build the new struct...
4804  // v ; the updated value
4805  // (struct.0.component2 s) ; retain the other members
4806  // ...
4807  // (struct.0.componentN s)))
4808 
4809  for(struct_union_typet::componentst::const_iterator
4810  it=components.begin();
4811  it!=components.end();
4812  ++it)
4813  {
4815  out << "(define-fun update-" << smt_typename << "."
4816  << component.get_name() << " "
4817  << "((s " << smt_typename << ") "
4818  << "(v ";
4819  convert_type(component.type());
4820  out << ")) " << smt_typename << " "
4821  << "(mk-" << smt_typename
4822  << " ";
4823 
4824  for(struct_union_typet::componentst::const_iterator
4825  it2=components.begin();
4826  it2!=components.end();
4827  ++it2)
4828  {
4829  if(it==it2)
4830  out << "v ";
4831  else
4832  {
4833  out << "(" << smt_typename << "."
4834  << it2->get_name() << " s) ";
4835  }
4836  }
4837 
4838  out << "))" << "\n";
4839  }
4840 
4841  out << "\n";
4842  }
4843  }
4844  else if(type.id() == ID_union)
4845  {
4846  const union_typet::componentst &components =
4847  to_union_type(type).components();
4848 
4849  for(const auto &component : components)
4850  find_symbols_rec(component.type(), recstack);
4851  }
4852  else if(type.id()==ID_code)
4853  {
4854  const code_typet::parameterst &parameters=
4855  to_code_type(type).parameters();
4856  for(const auto &param : parameters)
4857  find_symbols_rec(param.type(), recstack);
4858 
4859  find_symbols_rec(to_code_type(type).return_type(), recstack);
4860  }
4861  else if(type.id()==ID_pointer)
4862  {
4863  find_symbols_rec(type.subtype(), recstack);
4864  }
4865  else if(type.id() == ID_struct_tag)
4866  {
4867  const auto &struct_tag = to_struct_tag_type(type);
4868  const irep_idt &id = struct_tag.get_identifier();
4869 
4870  if(recstack.find(id) == recstack.end())
4871  {
4872  recstack.insert(id);
4873  find_symbols_rec(ns.follow_tag(struct_tag), recstack);
4874  }
4875  }
4876  else if(type.id() == ID_union_tag)
4877  {
4878  const auto &union_tag = to_union_tag_type(type);
4879  const irep_idt &id = union_tag.get_identifier();
4880 
4881  if(recstack.find(id) == recstack.end())
4882  {
4883  recstack.insert(id);
4884  find_symbols_rec(ns.follow_tag(union_tag), recstack);
4885  }
4886  }
4887 }
4888 
4890 {
4891  return number_of_solver_calls;
4892 }
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
int16_t s2
Definition: bytecode_info.h:60
int8_t s1
Definition: bytecode_info.h:59
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
bitvector_typet index_type()
Definition: c_types.cpp:16
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Absolute value.
Definition: std_expr.h:347
Operator to return the address of an object.
Definition: pointer_expr.h:200
exprt & object()
Definition: pointer_expr.h:209
Array constructor from single element.
Definition: std_expr.h:1317
const array_typet & type() const
Definition: std_expr.h:1324
Arrays with given size.
Definition: std_types.h:968
const exprt & size() const
Definition: std_types.h:976
exprt & op1()
Definition: expr.h:106
exprt & lhs()
Definition: std_expr.h:581
exprt & op0()
Definition: expr.h:103
exprt & rhs()
Definition: std_expr.h:591
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
exprt & where()
Definition: std_expr.h:2803
Bit-wise negation of bit-vectors.
std::size_t get_width() const
Definition: std_types.h:1048
The Boolean type.
Definition: std_types.h:37
const membert & get_member(const struct_typet &type, const irep_idt &member) const
The byte swap expression.
std::size_t get_bits_per_byte() const
std::vector< parametert > parameterst
Definition: std_types.h:746
const parameterst & parameters() const
Definition: std_types.h:860
struct configt::bv_encodingt bv_encoding
A constant literal expression.
Definition: std_expr.h:2668
const irep_idt & get_value() const
Definition: std_expr.h:2676
void set_value(const irep_idt &value)
Definition: std_expr.h:2681
resultt
Result of running the decision procedure.
Division.
Definition: std_expr.h:981
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
size_t size() const
Definition: dstring.h:104
Equality.
Definition: std_expr.h:1140
exprt & op0()
Definition: expr.h:103
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
exprt & op1()
Definition: expr.h:106
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:133
depth_iteratort depth_end()
Definition: expr.cpp:281
depth_iteratort depth_begin()
Definition: expr.cpp:279
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
exprt & op0()
Definition: expr.h:103
operandst & operands()
Definition: expr.h:96
Extracts a single bit of a bit-vector operand.
Extracts a sub-range of a bit-vector operand.
The Boolean constant false.
Definition: std_expr.h:2726
std::size_t integer_bits
Definition: fixedbv.h:22
std::size_t width
Definition: fixedbv.h:22
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: std_types.h:1325
std::size_t get_fraction_bits() const
Definition: std_types.h:1331
std::size_t get_integer_bits() const
Definition: std_types.cpp:35
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1386
std::size_t get_f() const
Definition: std_types.cpp:42
std::size_t get_e() const
Definition: std_types.h:1392
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
exprt & rounding_mode()
Definition: floatbv_expr.h:395
std::size_t f
Definition: ieee_float.h:30
std::size_t width() const
Definition: ieee_float.h:54
ieee_float_spect spec
Definition: ieee_float.h:134
bool is_NaN() const
Definition: ieee_float.h:237
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
bool get_sign() const
Definition: ieee_float.h:236
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:200
static ieee_floatt NaN(const ieee_float_spect &_spec)
Definition: ieee_float.h:197
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:203
bool is_infinity() const
Definition: ieee_float.h:238
mp_integer pack() const
Definition: ieee_float.cpp:370
void build(const mp_integer &exp, const mp_integer &frac)
Definition: ieee_float.cpp:468
The trinary if-then-else operator.
Definition: std_expr.h:2087
exprt & true_case()
Definition: std_expr.h:2114
exprt & false_case()
Definition: std_expr.h:2124
exprt & cond()
Definition: std_expr.h:2104
Boolean implication.
Definition: std_expr.h:1898
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
subt & get_sub()
Definition: irep.h:466
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
const std::string & id_string() const
Definition: irep.h:410
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:452
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
bool is_nil() const
Definition: irep.h:387
Evaluates to true if the operand is finite.
Definition: floatbv_expr.h:176
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
Evaluates to true if the operand is NaN.
Definition: floatbv_expr.h:88
Evaluates to true if the operand is a normal number.
Definition: floatbv_expr.h:220
A let expression.
Definition: std_expr.h:2816
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:2909
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:2897
operandst & values()
Definition: std_expr.h:2886
literalt get_literal() const
Definition: literal_expr.h:26
bool is_true() const
Definition: literal.h:156
bool sign() const
Definition: literal.h:88
var_not var_no() const
Definition: literal.h:83
bool is_false() const
Definition: literal.h:161
Extract member of struct or union.
Definition: std_expr.h:2528
const exprt & struct_op() const
Definition: std_expr.h:2558
irep_idt get_component_name() const
Definition: std_expr.h:2542
Binary minus.
Definition: std_expr.h:890
Modulo.
Definition: std_expr.h:1050
Binary multiplication Associativity is not specified.
Definition: std_expr.h:936
exprt & op1()
Definition: std_expr.h:767
exprt & op0()
Definition: std_expr.h:761
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The NIL expression.
Definition: std_expr.h:2735
const irep_idt & get_identifier() const
Definition: std_expr.h:238
Boolean negation.
Definition: std_expr.h:2042
Disequality.
Definition: std_expr.h:1198
The plus expression Associativity is not specified.
Definition: std_expr.h:831
void get_dynamic_objects(std::vector< std::size_t > &objects) const
std::size_t get_invalid_object() const
Definition: pointer_logic.h:64
numberingt< exprt, irep_hash > objects
Definition: pointer_logic.h:26
std::size_t add_object(const exprt &expr)
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
A base class for quantifier expressions.
symbol_exprt & symbol()
Bit-vector replication.
constant_exprt & times()
A base class for shift and rotate operators.
exprt & distance()
exprt & op()
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:507
const irep_idt & get_identifier() const
Definition: smt2_conv.h:165
void convert_relation(const binary_relation_exprt &)
Definition: smt2_conv.cpp:2991
void convert_type(const typet &)
Definition: smt2_conv.cpp:4544
void unflatten(wheret, const typet &, unsigned nesting=0)
Definition: smt2_conv.cpp:4070
bool use_array_theory(const exprt &)
Definition: smt2_conv.cpp:4523
void find_symbols(const exprt &expr)
Definition: smt2_conv.cpp:4313
std::size_t number_of_solver_calls
Definition: smt2_conv.h:91
void convert_typecast(const typecast_exprt &expr)
Definition: smt2_conv.cpp:1997
tvt l_get(literalt l) const
Definition: smt2_conv.cpp:122
void convert_update(const exprt &expr)
Definition: smt2_conv.cpp:3815
bool use_FPA_theory
Definition: smt2_conv.h:60
std::set< irep_idt > bvfp_set
Definition: smt2_conv.h:156
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
Definition: smt2_conv.cpp:608
void push() override
Unimplemented.
Definition: smt2_conv.cpp:761
void convert_is_dynamic_object(const unary_exprt &)
Definition: smt2_conv.cpp:2954
void convert_literal(const literalt)
Definition: smt2_conv.cpp:741
void convert_floatbv_div(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3453
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
Definition: smt2_conv.cpp:4889
const namespacet & ns
Definition: smt2_conv.h:83
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3548
boolbv_widtht boolbv_width
Definition: smt2_conv.h:89
void convert_constant(const constant_exprt &expr)
Definition: smt2_conv.cpp:2804
std::string floatbv_suffix(const exprt &) const
Definition: smt2_conv.cpp:846
void flatten2bv(const exprt &)
Definition: smt2_conv.cpp:3981
std::string notes
Definition: smt2_conv.h:85
void convert_div(const div_exprt &expr)
Definition: smt2_conv.cpp:3409
std::ostream & out
Definition: smt2_conv.h:84
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
Definition: smt2_conv.cpp:4266
std::string type2id(const typet &) const
Definition: smt2_conv.cpp:809
bool emit_set_logic
Definition: smt2_conv.h:63
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
Definition: smt2_conv.cpp:3196
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: smt2_conv.cpp:2530
struct_exprt parse_struct(const irept &s, const struct_typet &type)
Definition: smt2_conv.cpp:485
std::string logic
Definition: smt2_conv.h:85
void convert_mult(const mult_exprt &expr)
Definition: smt2_conv.cpp:3473
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
Definition: smt2_conv.cpp:4298
void define_object_size(const irep_idt &id, const exprt &expr)
Definition: smt2_conv.cpp:206
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: smt2_conv.cpp:251
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: smt2_conv.cpp:107
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3389
bool use_datatypes
Definition: smt2_conv.h:61
datatype_mapt datatype_map
Definition: smt2_conv.h:213
void convert_mod(const mod_exprt &expr)
Definition: smt2_conv.cpp:2935
std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:778
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3253
void convert_struct(const struct_exprt &expr)
Definition: smt2_conv.cpp:2676
smt2_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
Definition: smt2_conv.cpp:48
void convert_member(const member_exprt &expr)
Definition: smt2_conv.cpp:3920
void convert_index(const index_exprt &expr)
Definition: smt2_conv.cpp:3822
pointer_logict pointer_logic
Definition: smt2_conv.h:186
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
Definition: smt2_conv.cpp:732
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: smt2_conv.cpp:112
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: smt2_conv.cpp:4174
defined_expressionst object_sizes
Definition: smt2_conv.h:224
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:544
void write_footer(std::ostream &)
Definition: smt2_conv.cpp:165
void convert_union(const union_exprt &expr)
Definition: smt2_conv.cpp:2771
exprt parse_union(const irept &s, const union_typet &type)
Definition: smt2_conv.cpp:469
exprt parse_array(const irept &s, const array_typet &type)
Definition: smt2_conv.cpp:439
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:231
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
Definition: smt2_conv.cpp:2740
void convert_with(const with_exprt &expr)
Definition: smt2_conv.cpp:3568
letifyt letify
Definition: smt2_conv.h:143
bool use_array_of_bool
Definition: smt2_conv.h:62
std::vector< exprt > assumptions
Definition: smt2_conv.h:88
void convert_plus(const plus_exprt &expr)
Definition: smt2_conv.cpp:3074
defined_expressionst defined_expressions
Definition: smt2_conv.h:222
void pop() override
Currently, only implements a single stack element (no nested contexts)
Definition: smt2_conv.cpp:773
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt2_conv.cpp:4685
void write_header()
Definition: smt2_conv.cpp:135
solvert solver
Definition: smt2_conv.h:86
identifier_mapt identifier_map
Definition: smt2_conv.h:208
void convert_minus(const minus_exprt &expr)
Definition: smt2_conv.cpp:3292
void convert_expr(const exprt &)
Definition: smt2_conv.cpp:887
constant_exprt parse_literal(const irept &, const typet &type)
Definition: smt2_conv.cpp:301
std::size_t no_boolean_variables
Definition: smt2_conv.h:230
smt2_identifierst smt2_identifiers
Definition: smt2_conv.h:227
void convert_floatbv(const exprt &expr)
Definition: smt2_conv.cpp:853
resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: smt2_conv.cpp:244
literalt convert(const exprt &expr)
Definition: smt2_conv.cpp:700
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
Definition: smt2_conv.h:171
array_exprt to_array_expr() const
convert string into array constant
Struct constructor from list of elements.
Definition: std_expr.h:1583
Structure type, corresponds to C style structs.
Definition: std_types.h:226
const irep_idt & get_name() const
Definition: std_types.h:74
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:67
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:152
const componentst & components() const
Definition: std_types.h:142
std::vector< componentt > componentst
Definition: std_types.h:135
const irep_idt & get_identifier() const
Definition: std_expr.h:110
The Boolean constant true.
Definition: std_expr.h:2717
Definition: threeval.h:20
Semantic type conversion.
Definition: std_expr.h:1781
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
Generic base class for unary expressions.
Definition: std_expr.h:282
const exprt & op() const
Definition: std_expr.h:294
The unary minus expression.
Definition: std_expr.h:391
Union constructor from single element.
Definition: std_expr.h:1517
The union type.
Definition: std_types.h:393
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
Vector constructor from list of elements.
Definition: std_expr.h:1481
The vector type.
Definition: std_types.h:1764
const constant_exprt & size() const
Definition: std_types.cpp:282
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
exprt & old()
Definition: std_expr.h:2183
exprt & new_value()
Definition: std_expr.h:2203
exprt & where()
Definition: std_expr.h:2193
configt config
Definition: config.cpp:24
#define forall_operands(it, expr)
Definition: expr.h:18
Forward depth-first search iterators These iterators' copy operations are expensive,...
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
Definition: popcount.cpp:17
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:37
Deprecated expression utility functions.
exprt float_bv(const exprt &src)
Definition: float_bv.h:189
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: floatbv_expr.h:245
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: floatbv_expr.h:113
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: floatbv_expr.h:425
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: floatbv_expr.h:201
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: floatbv_expr.h:157
static format_containert< T > format(const T &o)
Definition: format.h:37
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:205
bool is_true(const literalt &l)
Definition: literal.h:198
literalt const_literal(bool value)
Definition: literal.h:188
literalt pos(literalt a)
Definition: literal.h:194
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
Definition: literal_expr.h:44
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
Definition: mp_arith.cpp:218
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
BigInt mp_integer
Definition: mp_arith.h:19
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Pointer Logic.
exprt object_size(const exprt &pointer)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
#define SMT2_TODO(S)
Definition: smt2_conv.cpp:46
#define UNEXPECTEDCASE(S)
Definition: smt2_conv.cpp:43
int solver(std::istream &in)
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
bool has_byte_operator(const exprt &src)
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define UNIMPLEMENTED
Definition: invariant.h:523
#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
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:497
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:512
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
API to expression classes.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1223
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:2940
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:465
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1075
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2067
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1563
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:421
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1030
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:915
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1501
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:816
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2235
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1606
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1362
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1180
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:870
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:261
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:1923
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:532
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:371
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:724
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:961
Pre-defined types.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1789
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1431
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1305
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1096
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:563
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: std_types.h:1478
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:430
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1369
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:729
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:523
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: std_types.h:1650
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1255
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: std_types.h:1146
std::size_t unsafe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:43
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::size_t object_bits
Definition: config.h:256