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