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