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