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()==ID_string_constant)
1387  {
1388  defined_expressionst::const_iterator it=defined_expressions.find(expr);
1389  assert(it!=defined_expressions.end());
1390  out << it->second;
1391  }
1392  else if(expr.id()==ID_extractbit)
1393  {
1394  assert(expr.operands().size()==2);
1395 
1396  if(expr.op1().is_constant())
1397  {
1398  mp_integer i;
1399  if(to_integer(expr.op1(), i))
1400  INVALIDEXPR("extractbit: to_integer failed");
1401 
1402  out << "(= ((_ extract " << i << " " << i << ") ";
1403  flatten2bv(expr.op0());
1404  out << ") #b1)";
1405  }
1406  else
1407  {
1408  out << "(= ((_ extract 0 0) ";
1409  // the arguments of the shift need to have the same width
1410  out << "(bvlshr ";
1411  flatten2bv(expr.op0());
1412  typecast_exprt tmp(expr.op0().type());
1413  tmp.op0()=expr.op1();
1414  convert_expr(tmp);
1415  out << ")) bin1)"; // bvlshr, extract, =
1416  }
1417  }
1418  else if(expr.id()==ID_extractbits)
1419  {
1420  assert(expr.operands().size()==3);
1421 
1422  if(expr.op1().is_constant() &&
1423  expr.op2().is_constant())
1424  {
1425  mp_integer op1_i, op2_i;
1426  if(to_integer(expr.op1(), op1_i))
1427  INVALIDEXPR("extractbits: to_integer failed");
1428 
1429  if(to_integer(expr.op2(), op2_i))
1430  INVALIDEXPR("extractbits: to_integer failed");
1431 
1432  if(op2_i>op1_i)
1433  std::swap(op1_i, op2_i);
1434 
1435  // now op1_i>=op2_i
1436 
1437  out << "((_ extract " << op1_i << " " << op2_i << ") ";
1438  flatten2bv(expr.op0());
1439  out << ")";
1440  }
1441  else
1442  {
1443  #if 0
1444  out << "(= ((_ extract 0 0) ";
1445  // the arguments of the shift need to have the same width
1446  out << "(bvlshr ";
1447  convert_expr(expr.op0());
1448  typecast_exprt tmp(expr.op0().type());
1449  tmp.op0()=expr.op1();
1450  convert_expr(tmp);
1451  out << ")) bin1)"; // bvlshr, extract, =
1452  #endif
1453  SMT2_TODO("smt2: extractbits with non-constant index");
1454  }
1455  }
1456  else if(expr.id()==ID_replication)
1457  {
1458  assert(expr.operands().size()==2);
1459 
1460  mp_integer times;
1461  if(to_integer(expr.op0(), times))
1462  INVALIDEXPR("replication takes constant as first parameter");
1463 
1464  out << "((_ repeat " << times << ") ";
1465  flatten2bv(expr.op1());
1466  out << ")";
1467  }
1468  else if(expr.id()==ID_byte_extract_little_endian ||
1469  expr.id()==ID_byte_extract_big_endian)
1470  {
1472  }
1473  else if(expr.id()==ID_byte_update_little_endian ||
1474  expr.id()==ID_byte_update_big_endian)
1475  {
1477  }
1478  else if(expr.id()==ID_width)
1479  {
1481 
1482  std::size_t result_width=boolbv_width(expr.type());
1483 
1484  if(result_width==0)
1485  INVALIDEXPR("conversion failed");
1486 
1487  if(expr.operands().size()!=1)
1488  INVALIDEXPR("width expects 1 operand");
1489 
1490  std::size_t op_width=boolbv_width(expr.op0().type());
1491 
1492  if(op_width==0)
1493  INVALIDEXPR("conversion failed");
1494 
1495  out << "(_ bv" << op_width/8
1496  << " " << result_width << ")";
1497  }
1498  else if(expr.id()==ID_abs)
1499  {
1500  assert(expr.operands().size()==1);
1501 
1502  const typet &type=expr.type();
1503 
1504  if(type.id()==ID_signedbv)
1505  {
1506  std::size_t result_width = to_signedbv_type(type).get_width();
1507 
1508  out << "(ite (bvslt ";
1509  convert_expr(expr.op0());
1510  out << " (_ bv0 " << result_width << ")) ";
1511  out << "(bvneg ";
1512  convert_expr(expr.op0());
1513  out << ") ";
1514  convert_expr(expr.op0());
1515  out << ")";
1516  }
1517  else if(type.id()==ID_fixedbv)
1518  {
1519  std::size_t result_width=to_fixedbv_type(type).get_width();
1520 
1521  out << "(ite (bvslt ";
1522  convert_expr(expr.op0());
1523  out << " (_ bv0 " << result_width << ")) ";
1524  out << "(bvneg ";
1525  convert_expr(expr.op0());
1526  out << ") ";
1527  convert_expr(expr.op0());
1528  out << ")";
1529  }
1530  else if(type.id()==ID_floatbv)
1531  {
1532  if(use_FPA_theory)
1533  {
1534  out << "(fp.abs ";
1535  convert_expr(expr.op0());
1536  out << ")";
1537  }
1538  else
1539  convert_floatbv(expr);
1540  }
1541  else
1542  UNEXPECTEDCASE("abs with unsupported operand type");
1543  }
1544  else if(expr.id()==ID_isnan)
1545  {
1546  assert(expr.operands().size()==1);
1547 
1548  const typet &op_type=expr.op0().type();
1549 
1550  if(op_type.id()==ID_fixedbv)
1551  out << "false";
1552  else if(op_type.id()==ID_floatbv)
1553  {
1554  if(use_FPA_theory)
1555  {
1556  out << "(fp.isNaN ";
1557  convert_expr(expr.op0());
1558  out << ")";
1559  }
1560  else
1561  convert_floatbv(expr);
1562  }
1563  else
1564  UNEXPECTEDCASE("isnan with unsupported operand type");
1565  }
1566  else if(expr.id()==ID_isfinite)
1567  {
1568  if(expr.operands().size()!=1)
1569  INVALIDEXPR("isfinite expects one operand");
1570 
1571  const typet &op_type=expr.op0().type();
1572 
1573  if(op_type.id()==ID_fixedbv)
1574  out << "true";
1575  else if(op_type.id()==ID_floatbv)
1576  {
1577  if(use_FPA_theory)
1578  {
1579  out << "(and ";
1580 
1581  out << "(not (fp.isNaN ";
1582  convert_expr(expr.op0());
1583  out << "))";
1584 
1585  out << "(not (fp.isInf ";
1586  convert_expr(expr.op0());
1587  out << "))";
1588 
1589  out << ")";
1590  }
1591  else
1592  convert_floatbv(expr);
1593  }
1594  else
1595  UNEXPECTEDCASE("isfinite with unsupported operand type");
1596  }
1597  else if(expr.id()==ID_isinf)
1598  {
1599  if(expr.operands().size()!=1)
1600  INVALIDEXPR("isinf expects one operand");
1601 
1602  const typet &op_type=expr.op0().type();
1603 
1604  if(op_type.id()==ID_fixedbv)
1605  out << "false";
1606  else if(op_type.id()==ID_floatbv)
1607  {
1608  if(use_FPA_theory)
1609  {
1610  out << "(fp.isInfinite ";
1611  convert_expr(expr.op0());
1612  out << ")";
1613  }
1614  else
1615  convert_floatbv(expr);
1616  }
1617  else
1618  UNEXPECTEDCASE("isinf with unsupported operand type");
1619  }
1620  else if(expr.id()==ID_isnormal)
1621  {
1622  if(expr.operands().size()!=1)
1623  INVALIDEXPR("isnormal expects one operand");
1624 
1625  const typet &op_type=expr.op0().type();
1626 
1627  if(op_type.id()==ID_fixedbv)
1628  out << "true";
1629  else if(op_type.id()==ID_floatbv)
1630  {
1631  if(use_FPA_theory)
1632  {
1633  out << "(fp.isNormal ";
1634  convert_expr(expr.op0());
1635  out << ")";
1636  }
1637  else
1638  convert_floatbv(expr);
1639  }
1640  else
1641  UNEXPECTEDCASE("isnormal with unsupported operand type");
1642  }
1643  else if(expr.id()==ID_overflow_plus ||
1644  expr.id()==ID_overflow_minus)
1645  {
1646  assert(expr.operands().size()==2);
1647  assert(expr.type().id()==ID_bool);
1648 
1649  bool subtract=expr.id()==ID_overflow_minus;
1650  const typet &op_type=expr.op0().type();
1651  std::size_t width=boolbv_width(op_type);
1652 
1653  if(op_type.id()==ID_signedbv)
1654  {
1655  // an overflow occurs if the top two bits of the extended sum differ
1656  out << "(let ((?sum (";
1657  out << (subtract?"bvsub":"bvadd");
1658  out << " ((_ sign_extend 1) ";
1659  convert_expr(expr.op0());
1660  out << ")";
1661  out << " ((_ sign_extend 1) ";
1662  convert_expr(expr.op1());
1663  out << ")))) "; // sign_extend, bvadd/sub let2
1664  out << "(not (= "
1665  "((_ extract " << width << " " << width << ") ?sum) "
1666  "((_ extract " << (width-1) << " " << (width-1) << ") ?sum)";
1667  out << ")))"; // =, not, let
1668  }
1669  else if(op_type.id()==ID_unsignedbv ||
1670  op_type.id()==ID_pointer)
1671  {
1672  // overflow is simply carry-out
1673  out << "(= ";
1674  out << "((_ extract " << width << " " << width << ") ";
1675  out << "(" << (subtract?"bvsub":"bvadd");
1676  out << " ((_ zero_extend 1) ";
1677  convert_expr(expr.op0());
1678  out << ")";
1679  out << " ((_ zero_extend 1) ";
1680  convert_expr(expr.op1());
1681  out << ")))"; // zero_extend, bvsub/bvadd, extract
1682  out << " #b1)"; // =
1683  }
1684  else
1685  UNEXPECTEDCASE("overflow check on unknown type: "+op_type.id_string());
1686  }
1687  else if(expr.id()==ID_overflow_mult)
1688  {
1689  assert(expr.operands().size()==2);
1690 
1691  // No better idea than to multiply with double the bits and then compare
1692  // with max value.
1693 
1694  const typet &op_type=expr.op0().type();
1695  std::size_t width=boolbv_width(op_type);
1696 
1697  if(op_type.id()==ID_signedbv)
1698  {
1699  out << "(let ( (prod (bvmul ((_ sign_extend " << width << ") ";
1700  convert_expr(expr.op0());
1701  out << ") ((_ sign_extend " << width << ") ";
1702  convert_expr(expr.op1());
1703  out << ")) )) ";
1704  out << "(or (bvsge prod (_ bv" << power(2, width-1) << " "
1705  << width*2 << "))";
1706  out << " (bvslt prod (bvneg (_ bv" << power(2, width-1) << " "
1707  << width*2 << ")))))";
1708  }
1709  else if(op_type.id()==ID_unsignedbv)
1710  {
1711  out << "(bvuge (bvmul ((_ zero_extend " << width << ") ";
1712  convert_expr(expr.op0());
1713  out << ") ((_ zero_extend " << width << ") ";
1714  convert_expr(expr.op1());
1715  out << ")) (_ bv" << power(2, width) << " " << width*2 << "))";
1716  }
1717  else
1718  UNEXPECTEDCASE("overflow-* check on unknown type: "+op_type.id_string());
1719  }
1720  else if(expr.id()==ID_array)
1721  {
1722  defined_expressionst::const_iterator it=defined_expressions.find(expr);
1723  assert(it!=defined_expressions.end());
1724  out << it->second;
1725  }
1726  else if(expr.id()==ID_literal)
1727  {
1728  convert_literal(to_literal_expr(expr).get_literal());
1729  }
1730  else if(expr.id()==ID_forall ||
1731  expr.id()==ID_exists)
1732  {
1734  // NOLINTNEXTLINE(readability/throw)
1735  throw "MathSAT does not support quantifiers";
1736 
1737  if(expr.id()==ID_forall)
1738  out << "(forall ";
1739  else if(expr.id()==ID_exists)
1740  out << "(exists ";
1741 
1742  exprt bound=expr.op0();
1743 
1744  out << "((";
1745  convert_expr(bound);
1746  out << " ";
1747  convert_type(bound.type());
1748  out << ")) ";
1749 
1750  convert_expr(expr.op1());
1751 
1752  out << ")";
1753  }
1754  else if(expr.id()==ID_vector)
1755  {
1756  const vector_typet &vector_type=to_vector_type(expr.type());
1757 
1758  mp_integer size;
1759  if(to_integer(vector_type.size(), size))
1760  INVALIDEXPR("failed to convert vector size to constant");
1761 
1762  assert(size==expr.operands().size());
1763 
1764  if(use_datatypes)
1765  {
1766  assert(datatype_map.find(vector_type)!=datatype_map.end());
1767 
1768  const std::string smt_typename=
1769  datatype_map.find(vector_type)->second;
1770 
1771  out << "(mk-" << smt_typename;
1772  }
1773  else
1774  out << "(concat";
1775 
1776  // build component-by-component
1777  forall_operands(it, expr)
1778  {
1779  out << " ";
1780  convert_expr(*it);
1781  }
1782 
1783  out << ")"; // mk-... or concat
1784  }
1785  else if(expr.id()==ID_object_size)
1786  {
1787  out << object_sizes[expr];
1788  }
1789  else if(expr.id()==ID_let)
1790  {
1791  const let_exprt &let_expr=to_let_expr(expr);
1792  out << "(let ((";
1793  convert_expr(let_expr.symbol());
1794  out << ' ';
1795  convert_expr(let_expr.value());
1796  out << ")) ";
1797  convert_expr(let_expr.where());
1798  out << ')'; // let
1799  }
1800  else if(expr.id()==ID_constraint_select_one)
1801  {
1803  "smt2_convt::convert_expr: `"+expr.id_string()+
1804  "' is not yet supported");
1805  }
1806  else if(expr.id() == ID_bswap)
1807  {
1808  if(expr.operands().size() != 1)
1809  INVALIDEXPR("bswap gets one operand");
1810 
1811  if(expr.op0().type() != expr.type())
1812  INVALIDEXPR("bswap gets one operand with same type");
1813 
1814  // first 'let' the operand
1815  out << "(let ((bswap_op ";
1816  convert_expr(expr.op0());
1817  out << ")) ";
1818 
1819  if(expr.type().id() == ID_signedbv || expr.type().id() == ID_unsignedbv)
1820  {
1821  const std::size_t width = to_bitvector_type(expr.type()).get_width();
1822 
1823  // width must be multiple of bytes
1824  if(width % 8 != 0)
1825  INVALIDEXPR("bswap must get bytes");
1826 
1827  const std::size_t bytes = width / 8;
1828 
1829  if(bytes <= 1)
1830  out << "bswap_op";
1831  else
1832  {
1833  // do a parallel 'let' for each byte
1834  out << "(let (";
1835 
1836  for(std::size_t byte = 0; byte < bytes; byte++)
1837  {
1838  if(byte != 0)
1839  out << ' ';
1840  out << "(bswap_byte_" << byte << ' ';
1841  out << "((_ extract " << (byte * 8 + 7) << " " << (byte * 8)
1842  << ") bswap_op)";
1843  out << ')';
1844  }
1845 
1846  out << ") ";
1847 
1848  // now stitch back together with 'concat'
1849  out << "(concat";
1850 
1851  for(std::size_t byte = 0; byte < bytes; byte++)
1852  out << " bswap_byte_" << byte;
1853 
1854  out << ')'; // concat
1855  out << ')'; // let bswap_byte_*
1856  }
1857  }
1858  else
1859  UNEXPECTEDCASE("bswap must get bitvector operand");
1860 
1861  out << ')'; // let bswap_op
1862  }
1863  else if(expr.id() == ID_popcount)
1864  {
1865  exprt lowered = lower_popcount(to_popcount_expr(expr), ns);
1866  convert_expr(lowered);
1867  }
1868  else
1870  "smt2_convt::convert_expr: `"+expr.id_string()+"' is unsupported");
1871 }
1872 
1874 {
1875  assert(expr.operands().size()==1);
1876  const exprt &src=expr.op0();
1877 
1878  typet dest_type=ns.follow(expr.type());
1879  if(dest_type.id()==ID_c_enum_tag)
1880  dest_type=ns.follow_tag(to_c_enum_tag_type(dest_type));
1881 
1882  typet src_type=ns.follow(src.type());
1883  if(src_type.id()==ID_c_enum_tag)
1884  src_type=ns.follow_tag(to_c_enum_tag_type(src_type));
1885 
1886  if(dest_type.id()==ID_bool)
1887  {
1888  // this is comparison with zero
1889  if(src_type.id()==ID_signedbv ||
1890  src_type.id()==ID_unsignedbv ||
1891  src_type.id()==ID_c_bool ||
1892  src_type.id()==ID_fixedbv ||
1893  src_type.id()==ID_pointer ||
1894  src_type.id()==ID_integer)
1895  {
1896  out << "(not (= ";
1897  convert_expr(src);
1898  out << " ";
1899  convert_expr(from_integer(0, src_type));
1900  out << "))";
1901  }
1902  else if(src_type.id()==ID_floatbv)
1903  {
1904  if(use_FPA_theory)
1905  {
1906  out << "(not (fp.isZero ";
1907  convert_expr(src);
1908  out << "))";
1909  }
1910  else
1911  convert_floatbv(expr);
1912  }
1913  else
1914  {
1915  UNEXPECTEDCASE("TODO typecast1 "+src_type.id_string()+" -> bool");
1916  }
1917  }
1918  else if(dest_type.id()==ID_c_bool)
1919  {
1920  std::size_t to_width=boolbv_width(dest_type);
1921  out << "(ite ";
1922  out << "(not (= ";
1923  convert_expr(src);
1924  out << " ";
1925  convert_expr(from_integer(0, src_type));
1926  out << ")) "; // not, =
1927  out << " (_ bv1 " << to_width << ")";
1928  out << " (_ bv0 " << to_width << ")";
1929  out << ")"; // ite
1930  }
1931  else if(dest_type.id()==ID_signedbv ||
1932  dest_type.id()==ID_unsignedbv ||
1933  dest_type.id()==ID_c_enum ||
1934  dest_type.id()==ID_bv)
1935  {
1936  std::size_t to_width=boolbv_width(dest_type);
1937 
1938  if(src_type.id()==ID_signedbv || // from signedbv
1939  src_type.id()==ID_unsignedbv || // from unsigedbv
1940  src_type.id()==ID_c_bool ||
1941  src_type.id()==ID_c_enum ||
1942  src_type.id()==ID_bv)
1943  {
1944  std::size_t from_width=boolbv_width(src_type);
1945 
1946  if(from_width==to_width)
1947  convert_expr(src); // ignore
1948  else if(from_width<to_width) // extend
1949  {
1950  if(src_type.id()==ID_signedbv)
1951  out << "((_ sign_extend ";
1952  else
1953  out << "((_ zero_extend ";
1954 
1955  out << (to_width-from_width)
1956  << ") "; // ind
1957  convert_expr(src);
1958  out << ")";
1959  }
1960  else // chop off extra bits
1961  {
1962  out << "((_ extract " << (to_width-1) << " 0) ";
1963  convert_expr(src);
1964  out << ")";
1965  }
1966  }
1967  else if(src_type.id()==ID_fixedbv) // from fixedbv to int
1968  {
1969  const fixedbv_typet &fixedbv_type=to_fixedbv_type(src_type);
1970 
1971  std::size_t from_width=fixedbv_type.get_width();
1972  std::size_t from_integer_bits=fixedbv_type.get_integer_bits();
1973  std::size_t from_fraction_bits=fixedbv_type.get_fraction_bits();
1974 
1975  // we might need to round up in case of negative numbers
1976  // e.g., (int)(-1.00001)==1
1977 
1978  out << "(let ((?tcop ";
1979  convert_expr(src);
1980  out << ")) ";
1981 
1982  out << "(bvadd ";
1983 
1984  if(to_width>from_integer_bits)
1985  {
1986  out << "((_ sign_extend "
1987  << (to_width-from_integer_bits) << ") ";
1988  out << "((_ extract " << (from_width-1) << " "
1989  << from_fraction_bits << ") ";
1990  convert_expr(src);
1991  out << "))";
1992  }
1993  else
1994  {
1995  out << "((_ extract " << (from_fraction_bits+to_width-1)
1996  << " " << from_fraction_bits << ") ";
1997  convert_expr(src);
1998  out << ")";
1999  }
2000 
2001  out << " (ite (and ";
2002 
2003  // some faction bit is not zero
2004  out << "(not (= ((_ extract " << (from_fraction_bits-1) << " 0) ?tcop) "
2005  "(_ bv0 " << from_fraction_bits << ")))";
2006 
2007  // number negative
2008  out << " (= ((_ extract " << (from_width-1) << " " << (from_width-1)
2009  << ") ?tcop) #b1)";
2010 
2011  out << ")"; // and
2012 
2013  out << " (_ bv1 " << to_width << ") (_ bv0 " << to_width << "))"; // ite
2014  out << ")"; // bvadd
2015  out << ")"; // let
2016  }
2017  else if(src_type.id()==ID_floatbv) // from floatbv to int
2018  {
2019  if(dest_type.id()==ID_bv)
2020  {
2021  // this is _NOT_ a semantic conversion, but bit-wise
2022 
2023  if(use_FPA_theory)
2024  {
2025  // This conversion is non-trivial as it requires creating a
2026  // new bit-vector variable and then asserting that it converts
2027  // to the required floating-point number.
2028  SMT2_TODO("bit-wise floatbv to bv");
2029  }
2030  else
2031  {
2032  // straight-forward if width matches
2033  convert_expr(src);
2034  }
2035  }
2036  else if(dest_type.id()==ID_signedbv)
2037  {
2038  // this should be floatbv_typecast, not typecast
2040  "typecast unexpected "+src_type.id_string()+" -> "+
2041  dest_type.id_string());
2042  }
2043  else if(dest_type.id()==ID_unsignedbv)
2044  {
2045  // this should be floatbv_typecast, not typecast
2047  "typecast unexpected "+src_type.id_string()+" -> "+
2048  dest_type.id_string());
2049  }
2050  }
2051  else if(src_type.id()==ID_bool) // from boolean to int
2052  {
2053  out << "(ite ";
2054  convert_expr(src);
2055 
2056  if(dest_type.id()==ID_fixedbv)
2057  {
2058  fixedbv_spect spec(to_fixedbv_type(dest_type));
2059  out << " (concat (_ bv1 "
2060  << spec.integer_bits << ") " <<
2061  "(_ bv0 " << spec.get_fraction_bits() << ")) " <<
2062  "(_ bv0 " << spec.width << ")";
2063  }
2064  else
2065  {
2066  out << " (_ bv1 " << to_width << ")";
2067  out << " (_ bv0 " << to_width << ")";
2068  }
2069 
2070  out << ")";
2071  }
2072  else if(src_type.id()==ID_pointer) // from pointer to int
2073  {
2074  std::size_t from_width=boolbv_width(src_type);
2075 
2076  if(from_width<to_width) // extend
2077  {
2078  out << "((_ sign_extend ";
2079  out << (to_width-from_width)
2080  << ") ";
2081  convert_expr(src);
2082  out << ")";
2083  }
2084  else // chop off extra bits
2085  {
2086  out << "((_ extract " << (to_width-1) << " 0) ";
2087  convert_expr(src);
2088  out << ")";
2089  }
2090  }
2091  else if(src_type.id()==ID_integer) // from integer to bit-vector
2092  {
2093  // must be constant
2094  if(src.is_constant())
2095  {
2096  mp_integer i;
2097  to_integer(src, i);
2098  out << "(_ bv" << i << " " << to_width << ")";
2099  }
2100  else
2101  SMT2_TODO("can't convert non-constant integer to bitvector");
2102  }
2103  else if(src_type.id()==ID_struct) // flatten a struct to a bit-vector
2104  {
2105  if(use_datatypes)
2106  {
2107  assert(boolbv_width(src_type)==boolbv_width(dest_type));
2108  flatten2bv(src);
2109  }
2110  else
2111  {
2112  assert(boolbv_width(src_type)==boolbv_width(dest_type));
2113  convert_expr(src); // nothing else to do!
2114  }
2115  }
2116  else if(src_type.id()==ID_union) // flatten a union
2117  {
2118  assert(boolbv_width(src_type)==boolbv_width(dest_type));
2119  convert_expr(src); // nothing else to do!
2120  }
2121  else if(src_type.id()==ID_c_bit_field)
2122  {
2123  std::size_t from_width=boolbv_width(src_type);
2124 
2125  if(from_width==to_width)
2126  convert_expr(src); // ignore
2127  else
2128  {
2130  typecast_exprt tmp(typecast_exprt(src, t), dest_type);
2131  convert_typecast(tmp);
2132  }
2133  }
2134  else
2135  {
2136  std::ostringstream e_str;
2137  e_str << src_type.id() << " -> " << dest_type.id()
2138  << " src == " << format(src);
2139  UNEXPECTEDCASE("TODO typecast2 " + e_str.str());
2140  }
2141  }
2142  else if(dest_type.id()==ID_fixedbv) // to fixedbv
2143  {
2144  const fixedbv_typet &fixedbv_type=to_fixedbv_type(dest_type);
2145  std::size_t to_fraction_bits=fixedbv_type.get_fraction_bits();
2146  std::size_t to_integer_bits=fixedbv_type.get_integer_bits();
2147 
2148  if(src_type.id()==ID_unsignedbv ||
2149  src_type.id()==ID_signedbv ||
2150  src_type.id()==ID_c_enum)
2151  {
2152  // integer to fixedbv
2153 
2154  std::size_t from_width=to_bitvector_type(src_type).get_width();
2155  out << "(concat ";
2156 
2157  if(from_width==to_integer_bits)
2158  convert_expr(src);
2159  else if(from_width>to_integer_bits)
2160  {
2161  // too many integer bits
2162  out << "((_ extract " << (to_integer_bits-1) << " 0) ";
2163  convert_expr(src);
2164  out << ")";
2165  }
2166  else
2167  {
2168  // too few integer bits
2169  assert(from_width<to_integer_bits);
2170  if(dest_type.id()==ID_unsignedbv)
2171  {
2172  out << "(_ zero_extend "
2173  << (to_integer_bits-from_width) << ") ";
2174  convert_expr(src);
2175  out << ")";
2176  }
2177  else
2178  {
2179  out << "((_ sign_extend "
2180  << (to_integer_bits-from_width) << ") ";
2181  convert_expr(src);
2182  out << ")";
2183  }
2184  }
2185 
2186  out << "(_ bv0 " << to_fraction_bits << ")";
2187  out << ")"; // concat
2188  }
2189  else if(src_type.id()==ID_bool) // bool to fixedbv
2190  {
2191  out << "(concat (concat"
2192  << " (_ bv0 " << (to_integer_bits-1) << ") ";
2193  flatten2bv(src); // produces #b0 or #b1
2194  out << ") (_ bv0 "
2195  << to_fraction_bits
2196  << "))";
2197  }
2198  else if(src_type.id()==ID_fixedbv) // fixedbv to fixedbv
2199  {
2200  const fixedbv_typet &from_fixedbv_type=to_fixedbv_type(src_type);
2201  std::size_t from_fraction_bits=from_fixedbv_type.get_fraction_bits();
2202  std::size_t from_integer_bits=from_fixedbv_type.get_integer_bits();
2203  std::size_t from_width=from_fixedbv_type.get_width();
2204 
2205  out << "(let ((?tcop ";
2206  convert_expr(src);
2207  out << ")) ";
2208 
2209  out << "(concat ";
2210 
2211  if(to_integer_bits<=from_integer_bits)
2212  {
2213  out << "((_ extract "
2214  << (from_fraction_bits+to_integer_bits-1) << " "
2215  << from_fraction_bits
2216  << ") ?tcop)";
2217  }
2218  else
2219  {
2220  assert(to_integer_bits>from_integer_bits);
2221  out << "((_ sign_extend "
2222  << (to_integer_bits-from_integer_bits)
2223  << ") ((_ extract "
2224  << (from_width-1) << " "
2225  << from_fraction_bits
2226  << ") ?tcop))";
2227  }
2228 
2229  out << " ";
2230 
2231  if(to_fraction_bits<=from_fraction_bits)
2232  {
2233  out << "((_ extract "
2234  << (from_fraction_bits-1) << " "
2235  << (from_fraction_bits-to_fraction_bits)
2236  << ") ?tcop)";
2237  }
2238  else
2239  {
2240  assert(to_fraction_bits>from_fraction_bits);
2241  out << "(concat ((_ extract "
2242  << (from_fraction_bits-1) << " 0) ";
2243  convert_expr(src);
2244  out << ")"
2245  << " (_ bv0 " << to_fraction_bits-from_fraction_bits
2246  << "))";
2247  }
2248 
2249  out << "))"; // concat, let
2250  }
2251  else
2252  UNEXPECTEDCASE("unexpected typecast to fixedbv");
2253  }
2254  else if(dest_type.id()==ID_pointer)
2255  {
2256  std::size_t to_width=boolbv_width(dest_type);
2257 
2258  if(src_type.id()==ID_pointer) // pointer to pointer
2259  {
2260  // this just passes through
2261  convert_expr(src);
2262  }
2263  else if(src_type.id()==ID_unsignedbv ||
2264  src_type.id()==ID_signedbv)
2265  {
2266  // integer to pointer
2267 
2268  std::size_t from_width=boolbv_width(src_type);
2269 
2270  if(from_width==to_width)
2271  convert_expr(src);
2272  else if(from_width<to_width)
2273  {
2274  out << "((_ sign_extend "
2275  << (to_width-from_width)
2276  << ") ";
2277  convert_expr(src);
2278  out << ")"; // sign_extend
2279  }
2280  else // from_width>to_width
2281  {
2282  out << "((_ extract " << to_width << " 0) ";
2283  convert_expr(src);
2284  out << ")"; // extract
2285  }
2286  }
2287  else
2288  UNEXPECTEDCASE("TODO typecast3 "+src_type.id_string()+" -> pointer");
2289  }
2290  else if(dest_type.id()==ID_range)
2291  {
2292  SMT2_TODO("range typecast");
2293  }
2294  else if(dest_type.id()==ID_floatbv)
2295  {
2296  // Typecast from integer to floating-point should have be been
2297  // converted to ID_floatbv_typecast during symbolic execution,
2298  // adding the rounding mode. See
2299  // smt2_convt::convert_floatbv_typecast.
2300  // The exception is bool and c_bool to float.
2301 
2302  if(src_type.id()==ID_bool)
2303  {
2304  constant_exprt val(dest_type);
2305 
2306  ieee_floatt a(to_floatbv_type(dest_type));
2307 
2308  mp_integer significand;
2309  mp_integer exponent;
2310 
2311  out << "(ite ";
2312  convert_expr(src);
2313  out << " ";
2314 
2315  significand = 1;
2316  exponent = 0;
2317  a.build(significand, exponent);
2318  val.set(ID_value, integer2binary(a.pack(), a.spec.width()));
2319 
2320  convert_constant(val);
2321  out << " ";
2322 
2323  significand = 0;
2324  exponent = 0;
2325  a.build(significand, exponent);
2326  val.set(ID_value, integer2binary(a.pack(), a.spec.width()));
2327 
2328  convert_constant(val);
2329  out << ")";
2330  }
2331  else if(src_type.id()==ID_c_bool)
2332  {
2333  // turn into proper bool
2334  const typecast_exprt tmp(src, bool_typet());
2335  convert_typecast(typecast_exprt(tmp, dest_type));
2336  }
2337  else
2338  UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float");
2339  }
2340  else if(dest_type.id()==ID_integer)
2341  {
2342  if(src_type.id()==ID_bool)
2343  {
2344  out << "(ite ";
2345  convert_expr(src);
2346  out <<" 1 0)";
2347  }
2348  else
2349  UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> integer");
2350  }
2351  else if(dest_type.id()==ID_c_bit_field)
2352  {
2353  std::size_t from_width=boolbv_width(src_type);
2354  std::size_t to_width=boolbv_width(dest_type);
2355 
2356  if(from_width==to_width)
2357  convert_expr(src); // ignore
2358  else
2359  {
2361  typecast_exprt tmp(typecast_exprt(src, t), dest_type);
2362  convert_typecast(tmp);
2363  }
2364  }
2365  else
2367  "TODO typecast8 "+src_type.id_string()+" -> "+dest_type.id_string());
2368 }
2369 
2371 {
2372  const exprt &src=expr.op();
2373  // const exprt &rounding_mode=expr.rounding_mode();
2374  const typet &src_type=src.type();
2375  const typet &dest_type=expr.type();
2376 
2377  if(dest_type.id()==ID_floatbv)
2378  {
2379  if(src_type.id()==ID_floatbv)
2380  {
2381  // float to float
2382 
2383  /* ISO 9899:1999
2384  * 6.3.1.5 Real floating types
2385  * 1 When a float is promoted to double or long double, or a
2386  * double is promoted to long double, its value is unchanged.
2387  *
2388  * 2 When a double is demoted to float, a long double is
2389  * demoted to double or float, or a value being represented in
2390  * greater precision and range than required by its semantic
2391  * type (see 6.3.1.8) is explicitly converted to its semantic
2392  * type, if the value being converted can be represented
2393  * exactly in the new type, it is unchanged. If the value
2394  * being converted is in the range of values that can be
2395  * represented but cannot be represented exactly, the result
2396  * is either the nearest higher or nearest lower representable
2397  * value, chosen in an implementation-defined manner. If the
2398  * value being converted is outside the range of values that
2399  * can be represented, the behavior is undefined.
2400  */
2401 
2402  const floatbv_typet &dst=to_floatbv_type(dest_type);
2403 
2404  if(use_FPA_theory)
2405  {
2406  out << "((_ to_fp " << dst.get_e() << " "
2407  << dst.get_f() + 1 << ") ";
2409  out << " ";
2410  convert_expr(src);
2411  out << ")";
2412  }
2413  else
2414  convert_floatbv(expr);
2415  }
2416  else if(src_type.id()==ID_unsignedbv)
2417  {
2418  // unsigned to float
2419 
2420  /* ISO 9899:1999
2421  * 6.3.1.4 Real floating and integer
2422  * 2 When a value of integer type is converted to a real
2423  * floating type, if the value being converted can be
2424  * represented exactly in the new type, it is unchanged. If the
2425  * value being converted is in the range of values that can be
2426  * represented but cannot be represented exactly, the result is
2427  * either the nearest higher or nearest lower representable
2428  * value, chosen in an implementation-defined manner. If the
2429  * value being converted is outside the range of values that can
2430  * be represented, the behavior is undefined.
2431  */
2432 
2433  const floatbv_typet &dst=to_floatbv_type(dest_type);
2434 
2435  if(use_FPA_theory)
2436  {
2437  out << "((_ to_fp_unsigned " << dst.get_e() << " "
2438  << dst.get_f() + 1 << ") ";
2440  out << " ";
2441  convert_expr(src);
2442  out << ")";
2443  }
2444  else
2445  convert_floatbv(expr);
2446  }
2447  else if(src_type.id()==ID_signedbv)
2448  {
2449  // signed to float
2450 
2451  const floatbv_typet &dst=to_floatbv_type(dest_type);
2452 
2453  if(use_FPA_theory)
2454  {
2455  out << "((_ to_fp " << dst.get_e() << " "
2456  << dst.get_f() + 1 << ") ";
2458  out << " ";
2459  convert_expr(src);
2460  out << ")";
2461  }
2462  else
2463  convert_floatbv(expr);
2464  }
2465  else if(src_type.id()==ID_c_enum_tag)
2466  {
2467  // enum to float
2468 
2469  // We first convert to 'underlying type'
2470  floatbv_typecast_exprt tmp=expr;
2471  tmp.op()=
2473  src,
2474  ns.follow_tag(to_c_enum_tag_type(src_type)).subtype());
2476  }
2477  else
2479  "TODO typecast11 "+src_type.id_string()+" -> "+dest_type.id_string());
2480  }
2481  else if(dest_type.id()==ID_signedbv)
2482  {
2483  if(use_FPA_theory)
2484  {
2485  std::size_t dest_width=to_signedbv_type(dest_type).get_width();
2486  out << "((_ fp.to_sbv " << dest_width << ") ";
2488  out << " ";
2489  convert_expr(src);
2490  out << ")";
2491  }
2492  else
2493  convert_floatbv(expr);
2494  }
2495  else if(dest_type.id()==ID_unsignedbv)
2496  {
2497  if(use_FPA_theory)
2498  {
2499  std::size_t dest_width=to_unsignedbv_type(dest_type).get_width();
2500  out << "((_ fp.to_ubv " << dest_width << ") ";
2502  out << " ";
2503  convert_expr(src);
2504  out << ")";
2505  }
2506  else
2507  convert_floatbv(expr);
2508  }
2509  else
2510  {
2512  "TODO typecast12 "+src_type.id_string()+" -> "+dest_type.id_string());
2513  }
2514 }
2515 
2517 {
2518  const struct_typet &struct_type=to_struct_type(expr.type());
2519 
2520  const struct_typet::componentst &components=
2521  struct_type.components();
2522 
2523  assert(components.size()==expr.operands().size());
2524 
2525  assert(!components.empty());
2526 
2527  if(use_datatypes)
2528  {
2529  assert(datatype_map.find(struct_type)!=datatype_map.end());
2530  const std::string smt_typename =
2531  datatype_map.find(struct_type)->second;
2532 
2533  // use the constructor for the Z3 datatype
2534  out << "(mk-" << smt_typename;
2535 
2536  std::size_t i=0;
2537  for(struct_typet::componentst::const_iterator
2538  it=components.begin();
2539  it!=components.end();
2540  it++, i++)
2541  {
2542  out << " ";
2543  convert_expr(expr.operands()[i]);
2544  }
2545 
2546  out << ")";
2547  }
2548  else
2549  {
2550  if(components.size()==1)
2551  convert_expr(expr.op0());
2552  else
2553  {
2554  // SMT-LIB 2 concat is binary only
2555  for(std::size_t i=components.size(); i>1; i--)
2556  {
2557  out << "(concat ";
2558 
2559  exprt op=expr.operands()[i-1];
2560 
2561  // may need to flatten array-theory arrays in there
2562  if(ns.follow(op.type()).id()==ID_array)
2563  flatten_array(op);
2564  else
2565  convert_expr(op);
2566 
2567  out << " ";
2568  }
2569 
2570  convert_expr(expr.op0());
2571 
2572  for(std::size_t i=1; i<components.size(); i++)
2573  out << ")";
2574  }
2575  }
2576 }
2577 
2580 {
2581  const array_typet &array_type=
2582  to_array_type(ns.follow(expr.type()));
2583 
2584  mp_integer size;
2585  if(to_integer(array_type.size(), size))
2586  INVALIDEXPR("failed to convert array size for flattening");
2587 
2588  if(size==0)
2589  INVALIDEXPR("can't convert zero-sized array");
2590 
2591  out << "(let ((?far ";
2592  convert_expr(expr);
2593  out << ")) ";
2594 
2595  for(mp_integer i=size; i!=0; --i)
2596  {
2597  if(i!=1)
2598  out << "(concat ";
2599  out << "(select ?far ";
2600  convert_expr(from_integer(i-1, array_type.size().type()));
2601  out << ")";
2602  if(i!=1)
2603  out << " ";
2604  }
2605 
2606  // close the many parentheses
2607  for(mp_integer i=size; i>1; --i)
2608  out << ")";
2609 
2610  out << ")"; // let
2611 }
2612 
2614 {
2615  const union_typet &union_type=to_union_type(expr.type());
2616  const exprt &op=expr.op();
2617 
2619 
2620  std::size_t total_width=boolbv_width(union_type);
2621 
2622  if(total_width==0)
2623  INVALIDEXPR("failed to get union width for union");
2624 
2625  std::size_t member_width=boolbv_width(op.type());
2626 
2627  if(member_width==0)
2628  INVALIDEXPR("failed to get union member width for union");
2629 
2630  if(total_width==member_width)
2631  {
2632  flatten2bv(op);
2633  }
2634  else
2635  {
2636  // we will pad with zeros, but non-det would be better
2637  assert(total_width>member_width);
2638  out << "(concat ";
2639  out << "(_ bv0 "
2640  << (total_width-member_width) << ") ";
2641  flatten2bv(op);
2642  out << ")";
2643  }
2644 }
2645 
2647 {
2648  const typet &expr_type=expr.type();
2649 
2650  if(expr_type.id()==ID_unsignedbv ||
2651  expr_type.id()==ID_signedbv ||
2652  expr_type.id()==ID_bv ||
2653  expr_type.id()==ID_c_enum ||
2654  expr_type.id()==ID_c_enum_tag ||
2655  expr_type.id()==ID_c_bool ||
2656  expr_type.id()==ID_incomplete_c_enum ||
2657  expr_type.id()==ID_c_bit_field)
2658  {
2659  mp_integer value=binary2integer(id2string(expr.get_value()), false);
2660 
2661  std::size_t width=boolbv_width(expr_type);
2662 
2663  out << "(_ bv" << value
2664  << " " << width << ")";
2665  }
2666  else if(expr_type.id()==ID_fixedbv)
2667  {
2668  fixedbv_spect spec(to_fixedbv_type(expr_type));
2669 
2670  std::string v_str=id2string(expr.get_value());
2671  mp_integer v=binary2integer(v_str, false);
2672 
2673  out << "(_ bv" << v << " " << spec.width << ")";
2674  }
2675  else if(expr_type.id()==ID_floatbv)
2676  {
2677  const floatbv_typet &floatbv_type=
2678  to_floatbv_type(expr_type);
2679 
2680  if(use_FPA_theory)
2681  {
2682  /* CBMC stores floating point literals in the most
2683  computationally useful form; biased exponents and
2684  significands including the hidden bit. Thus some encoding
2685  is needed to get to IEEE-754 style representations. */
2686 
2687  ieee_floatt v=ieee_floatt(expr);
2688  size_t e=floatbv_type.get_e();
2689  size_t f=floatbv_type.get_f()+1;
2690 
2691  /* Should be sufficient, but not currently supported by mathsat */
2692  #if 0
2693  mp_integer binary = v.pack();
2694 
2695  out << "((_ to_fp " << e << " " << f << ")"
2696  << " #b" << integer2binary(v.pack(), v.spec.width()) << ")";
2697  #endif
2698 
2699  if(v.is_NaN())
2700  {
2701  out << "(_ NaN " << e << " " << f << ")";
2702  }
2703  else if(v.is_infinity())
2704  {
2705  if(v.get_sign())
2706  out << "(_ -oo " << e << " " << f << ")";
2707  else
2708  out << "(_ +oo " << e << " " << f << ")";
2709  }
2710  else
2711  {
2712  // Zero, normal or subnormal
2713 
2714  mp_integer binary = v.pack();
2715  std::string binaryString(integer2binary(v.pack(), v.spec.width()));
2716 
2717  out << "(fp "
2718  << "#b" << binaryString.substr(0, 1) << " "
2719  << "#b" << binaryString.substr(1, e) << " "
2720  << "#b" << binaryString.substr(1+e, f-1) << ")";
2721  }
2722  }
2723  else
2724  {
2725  // produce corresponding bit-vector
2726  ieee_float_spect spec(floatbv_type);
2727 
2729  id2string(expr.get_value()), false);
2730 
2731  out << "(_ bv" << v << " " << spec.width() << ")";
2732  }
2733  }
2734  else if(expr_type.id()==ID_pointer)
2735  {
2736  const irep_idt &value=expr.get(ID_value);
2737 
2738  if(value==ID_NULL)
2739  {
2740  out << "(_ bv0 " << boolbv_width(expr_type)
2741  << ")";
2742  }
2743  else
2744  UNEXPECTEDCASE("unknown pointer constant: "+id2string(value));
2745  }
2746  else if(expr_type.id()==ID_bool)
2747  {
2748  if(expr.is_true())
2749  out << "true";
2750  else if(expr.is_false())
2751  out << "false";
2752  else
2753  UNEXPECTEDCASE("unknown boolean constant");
2754  }
2755  else if(expr_type.id()==ID_array)
2756  {
2757  defined_expressionst::const_iterator it=defined_expressions.find(expr);
2758  assert(it!=defined_expressions.end());
2759  out << it->second;
2760  }
2761  else if(expr_type.id()==ID_rational)
2762  {
2763  std::string value=id2string(expr.get_value());
2764  size_t pos=value.find("/");
2765 
2766  if(pos==std::string::npos)
2767  out << value << ".0";
2768  else
2769  {
2770  out << "(/ " << value.substr(0, pos) << ".0 "
2771  << value.substr(pos+1) << ".0)";
2772  }
2773  }
2774  else if(expr_type.id()==ID_integer)
2775  {
2776  out << expr.get_value();
2777  }
2778  else
2779  UNEXPECTEDCASE("unknown constant: "+expr_type.id_string());
2780 }
2781 
2783 {
2784  assert(expr.operands().size()==2);
2785 
2786  if(expr.type().id()==ID_unsignedbv ||
2787  expr.type().id()==ID_signedbv)
2788  {
2789  if(expr.type().id()==ID_unsignedbv)
2790  out << "(bvurem ";
2791  else
2792  out << "(bvsrem ";
2793 
2794  convert_expr(expr.op0());
2795  out << " ";
2796  convert_expr(expr.op1());
2797  out << ")";
2798  }
2799  else
2800  UNEXPECTEDCASE("unsupported type for mod: "+expr.type().id_string());
2801 }
2802 
2804 {
2805  std::vector<std::size_t> dynamic_objects;
2806  pointer_logic.get_dynamic_objects(dynamic_objects);
2807 
2808  assert(expr.operands().size()==1);
2809 
2810  if(dynamic_objects.empty())
2811  out << "false";
2812  else
2813  {
2814  std::size_t pointer_width=boolbv_width(expr.op0().type());
2815 
2816  out << "(let ((?obj ((_ extract "
2817  << pointer_width-1 << " "
2818  << pointer_width-config.bv_encoding.object_bits << ") ";
2819  convert_expr(expr.op0());
2820  out << "))) ";
2821 
2822  if(dynamic_objects.size()==1)
2823  {
2824  out << "(= (_ bv" << dynamic_objects.front()
2825  << " " << config.bv_encoding.object_bits << ") ?obj)";
2826  }
2827  else
2828  {
2829  out << "(or";
2830 
2831  for(const auto &object : dynamic_objects)
2832  out << " (= (_ bv" << object
2833  << " " << config.bv_encoding.object_bits << ") ?obj)";
2834 
2835  out << ")"; // or
2836  }
2837 
2838  out << ")"; // let
2839  }
2840 }
2841 
2843 {
2844  assert(expr.operands().size()==2);
2845 
2846  const typet &op_type=expr.op0().type();
2847 
2848  if(op_type.id()==ID_unsignedbv ||
2849  op_type.id()==ID_pointer ||
2850  op_type.id()==ID_bv)
2851  {
2852  out << "(";
2853  if(expr.id()==ID_le)
2854  out << "bvule";
2855  else if(expr.id()==ID_lt)
2856  out << "bvult";
2857  else if(expr.id()==ID_ge)
2858  out << "bvuge";
2859  else if(expr.id()==ID_gt)
2860  out << "bvugt";
2861 
2862  out << " ";
2863  convert_expr(expr.op0());
2864  out << " ";
2865  convert_expr(expr.op1());
2866  out << ")";
2867  }
2868  else if(op_type.id()==ID_signedbv ||
2869  op_type.id()==ID_fixedbv)
2870  {
2871  out << "(";
2872  if(expr.id()==ID_le)
2873  out << "bvsle";
2874  else if(expr.id()==ID_lt)
2875  out << "bvslt";
2876  else if(expr.id()==ID_ge)
2877  out << "bvsge";
2878  else if(expr.id()==ID_gt)
2879  out << "bvsgt";
2880 
2881  out << " ";
2882  convert_expr(expr.op0());
2883  out << " ";
2884  convert_expr(expr.op1());
2885  out << ")";
2886  }
2887  else if(op_type.id()==ID_floatbv)
2888  {
2889  if(use_FPA_theory)
2890  {
2891  out << "(";
2892  if(expr.id()==ID_le)
2893  out << "fp.leq";
2894  else if(expr.id()==ID_lt)
2895  out << "fp.lt";
2896  else if(expr.id()==ID_ge)
2897  out << "fp.geq";
2898  else if(expr.id()==ID_gt)
2899  out << "fp.gt";
2900 
2901  out << " ";
2902  convert_expr(expr.op0());
2903  out << " ";
2904  convert_expr(expr.op1());
2905  out << ")";
2906  }
2907  else
2908  convert_floatbv(expr);
2909  }
2910  else if(op_type.id()==ID_rational ||
2911  op_type.id()==ID_integer)
2912  {
2913  out << "(";
2914  out << expr.id();
2915 
2916  out << " ";
2917  convert_expr(expr.op0());
2918  out << " ";
2919  convert_expr(expr.op1());
2920  out << ")";
2921  }
2922  else
2924  "unsupported type for "+expr.id_string()+": "+op_type.id_string());
2925 }
2926 
2928 {
2929  if(expr.operands().empty())
2930  {
2931  INVALIDEXPR("No operands to plus");
2932  }
2933  else if(expr.operands().size()==1)
2934  {
2935  convert_expr(expr.op0());
2936  }
2937  else
2938  {
2939  if(expr.type().id()==ID_rational ||
2940  expr.type().id()==ID_integer ||
2941  expr.type().id()==ID_real)
2942  {
2943  // these are multi-ary in SMT-LIB2
2944  out << "(+";
2945 
2946  for(const auto &op : expr.operands())
2947  {
2948  out << ' ';
2949  convert_expr(op);
2950  }
2951 
2952  out << ')';
2953  }
2954  else if(expr.type().id()==ID_unsignedbv ||
2955  expr.type().id()==ID_signedbv ||
2956  expr.type().id()==ID_fixedbv)
2957  {
2958  // These could be chained, i.e., need not be binary,
2959  // but at least MathSat doesn't like that.
2960  if(expr.operands().size()==2)
2961  {
2962  out << "(bvadd ";
2963  convert_expr(expr.op0());
2964  out << " ";
2965  convert_expr(expr.op1());
2966  out << ")";
2967  }
2968  else
2969  {
2971  }
2972  }
2973  else if(expr.type().id()==ID_floatbv)
2974  {
2975  // Floating-point additions should have be been converted
2976  // to ID_floatbv_plus during symbolic execution, adding
2977  // the rounding mode. See smt2_convt::convert_floatbv_plus.
2978  UNREACHABLE;
2979  }
2980  else if(expr.type().id()==ID_pointer)
2981  {
2982  if(expr.operands().size()==2)
2983  {
2984  exprt p=expr.op0(), i=expr.op1();
2985 
2986  if(p.type().id()!=ID_pointer)
2987  p.swap(i);
2988 
2989  if(p.type().id()!=ID_pointer)
2990  INVALIDEXPR("unexpected mixture in pointer arithmetic");
2991 
2992  mp_integer element_size=
2993  pointer_offset_size(expr.type().subtype(), ns);
2994  CHECK_RETURN(element_size>0);
2995 
2996  out << "(bvadd ";
2997  convert_expr(p);
2998  out << " ";
2999 
3000  if(element_size>=2)
3001  {
3002  out << "(bvmul ";
3003  convert_expr(i);
3004  out << " (_ bv" << element_size
3005  << " " << boolbv_width(expr.type()) << "))";
3006  }
3007  else
3008  convert_expr(i);
3009 
3010  out << ')';
3011  }
3012  else
3013  {
3015  }
3016  }
3017  else if(expr.type().id()==ID_vector)
3018  {
3019  const vector_typet &vector_type=to_vector_type(expr.type());
3020 
3021  mp_integer size;
3022  if(to_integer(vector_type.size(), size))
3023  INVALIDEXPR("failed to convert vector size to constant");
3024 
3025  typet index_type=vector_type.size().type();
3026 
3027  if(use_datatypes)
3028  {
3029  assert(datatype_map.find(vector_type)!=datatype_map.end());
3030 
3031  const std::string smt_typename=
3032  datatype_map.find(vector_type)->second;
3033 
3034  out << "(mk-" << smt_typename;
3035  }
3036  else
3037  out << "(concat";
3038 
3039  // add component-by-component
3040  for(mp_integer i=0; i!=size; ++i)
3041  {
3042  exprt tmp(ID_plus, vector_type.subtype());
3043  forall_operands(it, expr)
3044  tmp.copy_to_operands(
3045  index_exprt(
3046  *it,
3047  from_integer(size-i-1, index_type),
3048  vector_type.subtype()));
3049 
3050  out << " ";
3051  convert_expr(tmp);
3052  }
3053 
3054  out << ")"; // mk-... or concat
3055  }
3056  else
3057  UNEXPECTEDCASE("unsupported type for +: "+expr.type().id_string());
3058  }
3059 }
3060 
3066 {
3067  assert(use_FPA_theory);
3068 
3069  /* CProver uses the x86 numbering of the rounding-mode
3070  * 0 == FE_TONEAREST
3071  * 1 == FE_DOWNWARD
3072  * 2 == FE_UPWARD
3073  * 3 == FE_TOWARDZERO
3074  * These literal values must be used rather than the macros
3075  * the macros from fenv.h to avoid portability problems.
3076  */
3077 
3078  if(expr.id()==ID_constant)
3079  {
3080  const constant_exprt &cexpr=to_constant_expr(expr);
3081 
3082  mp_integer value=binary2integer(id2string(cexpr.get_value()), false);
3083 
3084  if(value==0)
3085  out << "roundNearestTiesToEven";
3086  else if(value==1)
3087  out << "roundTowardNegative";
3088  else if(value==2)
3089  out << "roundTowardPositive";
3090  else if(value==3)
3091  out << "roundTowardZero";
3092  else
3093  INVALIDEXPR(
3094  "Unknown constant rounding mode with value "+
3095  id2string(cexpr.get_value()));
3096  }
3097  else
3098  {
3099  std::size_t width=to_bitvector_type(expr.type()).get_width();
3100 
3101  // Need to make the choice above part of the model
3102  out << "(ite (= (_ bv0 " << width << ") ";
3103  convert_expr(expr);
3104  out << ") roundNearestTiesToEven ";
3105 
3106  out << "(ite (= (_ bv1 " << width << ") ";
3107  convert_expr(expr);
3108  out << ") roundTowardNegative ";
3109 
3110  out << "(ite (= (_ bv2 " << width << ") ";
3111  convert_expr(expr);
3112  out << ") roundTowardPositive ";
3113 
3114  // TODO: add some kind of error checking here
3115  out << "roundTowardZero";
3116 
3117  out << ")))";
3118  }
3119 }
3120 
3122 {
3123  const typet &type=expr.type();
3124 
3125  assert(expr.operands().size()==3);
3126  assert(type.id()==ID_floatbv ||
3127  (type.id()==ID_complex && type.subtype().id()==ID_floatbv) ||
3128  (type.id()==ID_vector && type.subtype().id()==ID_floatbv));
3129 
3130  if(use_FPA_theory)
3131  {
3132  if(type.id()==ID_floatbv)
3133  {
3134  out << "(fp.add ";
3136  out << " ";
3137  convert_expr(expr.op0());
3138  out << " ";
3139  convert_expr(expr.op1());
3140  out << ")";
3141  }
3142  else if(type.id()==ID_complex)
3143  {
3144  SMT2_TODO("+ for floatbv complex");
3145  }
3146  else if(type.id()==ID_vector)
3147  {
3148  SMT2_TODO("+ for floatbv vector");
3149  }
3150  else
3151  UNEXPECTEDCASE("unsupported type for +: "+type.id_string());
3152  }
3153  else
3154  convert_floatbv(expr);
3155 }
3156 
3158 {
3159  assert(expr.operands().size()==2);
3160 
3161  if(expr.type().id()==ID_integer)
3162  {
3163  out << "(- ";
3164  convert_expr(expr.op0());
3165  out << " ";
3166  convert_expr(expr.op1());
3167  out << ")";
3168  }
3169  else if(expr.type().id()==ID_unsignedbv ||
3170  expr.type().id()==ID_signedbv ||
3171  expr.type().id()==ID_fixedbv)
3172  {
3173  if(expr.op0().type().id()==ID_pointer &&
3174  expr.op1().type().id()==ID_pointer)
3175  {
3176  // Pointer difference.
3177  mp_integer element_size=
3178  pointer_offset_size(expr.op0().type().subtype(), ns);
3179  assert(element_size>0);
3180 
3181  if(element_size>=2)
3182  out << "(bvsdiv ";
3183 
3184  assert(boolbv_width(expr.op0().type())==boolbv_width(expr.type()));
3185 
3186  out << "(bvsub ";
3187  convert_expr(expr.op0());
3188  out << " ";
3189  convert_expr(expr.op1());
3190  out << ")";
3191 
3192  if(element_size>=2)
3193  out << " (_ bv" << element_size
3194  << " " << boolbv_width(expr.type()) << "))";
3195  }
3196  else
3197  {
3198  out << "(bvsub ";
3199  convert_expr(expr.op0());
3200  out << " ";
3201  convert_expr(expr.op1());
3202  out << ")";
3203  }
3204  }
3205  else if(expr.type().id()==ID_floatbv)
3206  {
3207  // Floating-point subtraction should have be been converted
3208  // to ID_floatbv_minus during symbolic execution, adding
3209  // the rounding mode. See smt2_convt::convert_floatbv_minus.
3210  UNREACHABLE;
3211  }
3212  else if(expr.type().id()==ID_pointer)
3213  {
3214  SMT2_TODO("pointer subtraction");
3215  }
3216  else if(expr.type().id()==ID_vector)
3217  {
3218  const vector_typet &vector_type=to_vector_type(expr.type());
3219 
3220  mp_integer size;
3221  if(to_integer(vector_type.size(), size))
3222  INVALIDEXPR("failed to convert vector size to constant");
3223 
3224  typet index_type=vector_type.size().type();
3225 
3226  if(use_datatypes)
3227  {
3228  assert(datatype_map.find(vector_type)!=datatype_map.end());
3229 
3230  const std::string smt_typename=
3231  datatype_map.find(vector_type)->second;
3232 
3233  out << "(mk-" << smt_typename;
3234  }
3235  else
3236  out << "(concat";
3237 
3238  // subtract component-by-component
3239  for(mp_integer i=0; i!=size; ++i)
3240  {
3241  exprt tmp(ID_minus, vector_type.subtype());
3242  forall_operands(it, expr)
3243  tmp.copy_to_operands(
3244  index_exprt(
3245  *it,
3246  from_integer(size-i-1, index_type),
3247  vector_type.subtype()));
3248 
3249  out << " ";
3250  convert_expr(tmp);
3251  }
3252 
3253  out << ")"; // mk-... or concat
3254  }
3255  else
3256  UNEXPECTEDCASE("unsupported type for -: "+expr.type().id_string());
3257 }
3258 
3260 {
3261  assert(expr.operands().size()==3);
3262  assert(expr.type().id()==ID_floatbv);
3263 
3264  if(use_FPA_theory)
3265  {
3266  out << "(fp.sub ";
3268  out << " ";
3269  convert_expr(expr.op0());
3270  out << " ";
3271  convert_expr(expr.op1());
3272  out << ")";
3273  }
3274  else
3275  convert_floatbv(expr);
3276 }
3277 
3279 {
3280  assert(expr.operands().size()==2);
3281 
3282  if(expr.type().id()==ID_unsignedbv ||
3283  expr.type().id()==ID_signedbv)
3284  {
3285  if(expr.type().id()==ID_unsignedbv)
3286  out << "(bvudiv ";
3287  else
3288  out << "(bvsdiv ";
3289 
3290  convert_expr(expr.op0());
3291  out << " ";
3292  convert_expr(expr.op1());
3293  out << ")";
3294  }
3295  else if(expr.type().id()==ID_fixedbv)
3296  {
3297  fixedbv_spect spec(to_fixedbv_type(expr.type()));
3298  std::size_t fraction_bits=spec.get_fraction_bits();
3299 
3300  out << "((_ extract " << spec.width-1 << " 0) ";
3301  out << "(bvsdiv ";
3302 
3303  out << "(concat ";
3304  convert_expr(expr.op0());
3305  out << " (_ bv0 " << fraction_bits << ")) ";
3306 
3307  out << "((_ sign_extend " << fraction_bits << ") ";
3308  convert_expr(expr.op1());
3309  out << ")";
3310 
3311  out << "))";
3312  }
3313  else if(expr.type().id()==ID_floatbv)
3314  {
3315  // Floating-point division should have be been converted
3316  // to ID_floatbv_div during symbolic execution, adding
3317  // the rounding mode. See smt2_convt::convert_floatbv_div.
3318  UNREACHABLE;
3319  }
3320  else
3321  UNEXPECTEDCASE("unsupported type for /: "+expr.type().id_string());
3322 }
3323 
3325 {
3326  assert(expr.operands().size()==3);
3327  assert(expr.type().id()==ID_floatbv);
3328 
3329  if(use_FPA_theory)
3330  {
3331  out << "(fp.div ";
3333  out << " ";
3334  convert_expr(expr.op0());
3335  out << " ";
3336  convert_expr(expr.op1());
3337  out << ")";
3338  }
3339  else
3340  convert_floatbv(expr);
3341 }
3342 
3344 {
3345  assert(expr.operands().size()>=2);
3346 
3347  // re-write to binary if needed
3348  if(expr.operands().size()>2)
3349  {
3350  // strip last operand
3351  exprt tmp=expr;
3352  tmp.operands().pop_back();
3353 
3354  // recursive call
3355  return convert_mult(mult_exprt(tmp, expr.operands().back()));
3356  }
3357 
3358  assert(expr.operands().size()==2);
3359 
3360  if(expr.type().id()==ID_unsignedbv ||
3361  expr.type().id()==ID_signedbv)
3362  {
3363  // Note that bvmul is really unsigned,
3364  // but this is irrelevant as we chop-off any extra result
3365  // bits.
3366  out << "(bvmul ";
3367  convert_expr(expr.op0());
3368  out << " ";
3369  convert_expr(expr.op1());
3370  out << ")";
3371  }
3372  else if(expr.type().id()==ID_floatbv)
3373  {
3374  // Floating-point multiplication should have be been converted
3375  // to ID_floatbv_mult during symbolic execution, adding
3376  // the rounding mode. See smt2_convt::convert_floatbv_mult.
3377  UNREACHABLE;
3378  }
3379  else if(expr.type().id()==ID_fixedbv)
3380  {
3381  fixedbv_spect spec(to_fixedbv_type(expr.type()));
3382  std::size_t fraction_bits=spec.get_fraction_bits();
3383 
3384  out << "((_ extract "
3385  << spec.width+fraction_bits-1 << " "
3386  << fraction_bits << ") ";
3387 
3388  out << "(bvmul ";
3389 
3390  out << "((_ sign_extend " << fraction_bits << ") ";
3391  convert_expr(expr.op0());
3392  out << ") ";
3393 
3394  out << "((_ sign_extend " << fraction_bits << ") ";
3395  convert_expr(expr.op1());
3396  out << ")";
3397 
3398  out << "))"; // bvmul, extract
3399  }
3400  else if(expr.type().id()==ID_rational ||
3401  expr.type().id()==ID_integer ||
3402  expr.type().id()==ID_real)
3403  {
3404  out << "(*";
3405 
3406  forall_operands(it, expr)
3407  {
3408  out << " ";
3409  convert_expr(*it);
3410  }
3411 
3412  out << ")";
3413  }
3414  else
3415  UNEXPECTEDCASE("unsupported type for *: "+expr.type().id_string());
3416 }
3417 
3419 {
3420  assert(expr.operands().size()==3);
3421  assert(expr.type().id()==ID_floatbv);
3422 
3423  if(use_FPA_theory)
3424  {
3425  out << "(fp.mul ";
3427  out << " ";
3428  convert_expr(expr.op0());
3429  out << " ";
3430  convert_expr(expr.op1());
3431  out << ")";
3432  }
3433  else
3434  convert_floatbv(expr);
3435 }
3436 
3438 {
3439  // get rid of "with" that has more than three operands
3440 
3441  assert(expr.operands().size()>=3);
3442 
3443  if(expr.operands().size()>3)
3444  {
3445  std::size_t s=expr.operands().size();
3446 
3447  // strip of the trailing two operands
3448  exprt tmp=expr;
3449  tmp.operands().resize(s-2);
3450 
3451  with_exprt new_with_expr;
3452  assert(new_with_expr.operands().size()==3);
3453  new_with_expr.type()=expr.type();
3454  new_with_expr.old()=tmp;
3455  new_with_expr.where()=expr.operands()[s-2];
3456  new_with_expr.new_value()=expr.operands()[s-1];
3457 
3458  // recursive call
3459  return convert_with(new_with_expr);
3460  }
3461 
3462  const typet &expr_type=ns.follow(expr.type());
3463 
3464  if(expr_type.id()==ID_array)
3465  {
3466  const array_typet &array_type=to_array_type(expr_type);
3467 
3468  if(use_array_theory(expr))
3469  {
3470  out << "(store ";
3471  convert_expr(expr.old());
3472  out << " ";
3473  convert_expr(typecast_exprt(expr.where(), array_type.size().type()));
3474  out << " ";
3475  convert_expr(expr.new_value());
3476  out << ")";
3477  }
3478  else
3479  {
3480  // fixed-width
3481  std::size_t array_width=boolbv_width(array_type);
3482  std::size_t sub_width=boolbv_width(array_type.subtype());
3483  std::size_t index_width=boolbv_width(expr.where().type());
3484 
3485  // We mask out the updated bit with AND,
3486  // and then OR-in the shifted new value.
3487 
3488  out << "(let ((distance? ";
3489  out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
3490 
3491  // SMT2 says that the shift distance needs to be as wide
3492  // as the stuff we are shifting.
3493  if(array_width>index_width)
3494  {
3495  out << "((_ zero_extend " << array_width-index_width << ") ";
3496  convert_expr(expr.where());
3497  out << ")";
3498  }
3499  else
3500  {
3501  out << "((_ extract " << array_width-1 << " 0) ";
3502  convert_expr(expr.where());
3503  out << ")";
3504  }
3505 
3506  out << "))) "; // bvmul, distance?
3507 
3508  out << "(bvor ";
3509  out << "(bvand ";
3510  out << "(bvlshr (_ bv" << power(2, array_width)-1 << " "
3511  << array_width << ") ";
3512  out << "distance?) ";
3513  convert_expr(expr.old());
3514  out << ") "; // bvand
3515  out << "(bvlshr ";
3516  out << "((_ zero_extend " << array_width-sub_width << ") ";
3517  convert_expr(expr.new_value());
3518  out << ") distance?)))"; // zero_extend, bvlshr, bvor, let
3519  }
3520  }
3521  else if(expr_type.id()==ID_struct)
3522  {
3523  const struct_typet &struct_type=to_struct_type(expr_type);
3524 
3525  const exprt &index=expr.op1();
3526  const exprt &value=expr.op2();
3527 
3528  const irep_idt &component_name=index.get(ID_component_name);
3529 
3530  if(!struct_type.has_component(component_name))
3531  INVALIDEXPR("with failed to find component in struct");
3532 
3533  if(use_datatypes)
3534  {
3535  assert(datatype_map.find(expr_type)!=datatype_map.end());
3536  const std::string smt_typename=
3537  datatype_map.find(expr_type)->second;
3538 
3539  out << "(update-" << smt_typename << "." << component_name << " ";
3540  convert_expr(expr.op0());
3541  out << " ";
3542  convert_expr(value);
3543  out << ")";
3544  }
3545  else
3546  {
3547  std::size_t struct_width=boolbv_width(struct_type);
3548 
3549  // figure out the offset and width of the member
3551  boolbv_width.get_member(struct_type, component_name);
3552 
3553  out << "(let ((?withop ";
3554  convert_expr(expr.op0());
3555  out << ")) ";
3556 
3557  if(m.width==struct_width)
3558  {
3559  // the struct is the same as the member, no concat needed
3560  out << "?withop";
3561  }
3562  else if(m.offset==0)
3563  {
3564  // the member is at the beginning
3565  out << "(concat "
3566  << "((_ extract " << (struct_width-1) << " "
3567  << m.width << ") ?withop) ";
3568  convert_expr(value);
3569  out << ")"; // concat
3570  }
3571  else if(m.offset+m.width==struct_width)
3572  {
3573  // the member is at the end
3574  out << "(concat ";
3575  convert_expr(value);
3576  out << "((_ extract " << (m.offset-1) << " 0) ?withop))";
3577  }
3578  else
3579  {
3580  // most general case, need two concat-s
3581  out << "(concat (concat "
3582  << "((_ extract " << (struct_width-1) << " "
3583  << (m.offset+m.width) << ") ?withop) ";
3584  convert_expr(value);
3585  out << ") ((_ extract " << (m.offset-1) << " 0) ?withop)";
3586  out << ")"; // concat
3587  }
3588 
3589  out << ")"; // let ?withop
3590  }
3591  }
3592  else if(expr_type.id()==ID_union)
3593  {
3594  const union_typet &union_type=to_union_type(expr_type);
3595 
3596  const exprt &value=expr.op2();
3597 
3599 
3600  std::size_t total_width=boolbv_width(union_type);
3601 
3602  if(total_width==0)
3603  INVALIDEXPR("failed to get union width for with");
3604 
3605  std::size_t member_width=boolbv_width(value.type());
3606 
3607  if(member_width==0)
3608  INVALIDEXPR("failed to get union member width for with");
3609 
3610  if(total_width==member_width)
3611  {
3612  flatten2bv(value);
3613  }
3614  else
3615  {
3616  assert(total_width>member_width);
3617  out << "(concat ";
3618  out << "((_ extract "
3619  << (total_width-1)
3620  << " " << member_width << ") ";
3621  convert_expr(expr.op0());
3622  out << ") ";
3623  flatten2bv(value);
3624  out << ")";
3625  }
3626  }
3627  else if(expr_type.id()==ID_bv ||
3628  expr_type.id()==ID_unsignedbv ||
3629  expr_type.id()==ID_signedbv)
3630  {
3631  // Update bits in a bit-vector. We will use masking and shifts.
3632 
3633  std::size_t total_width=boolbv_width(expr_type);
3634 
3635  if(total_width==0)
3636  INVALIDEXPR("failed to get total width");
3637 
3638  assert(expr.operands().size()==3);
3639  const exprt &index=expr.operands()[1];
3640  const exprt &value=expr.operands()[2];
3641 
3642  std::size_t value_width=boolbv_width(value.type());
3643 
3644  if(value_width==0)
3645  INVALIDEXPR("failed to get value width");
3646 
3647  typecast_exprt index_tc(index, expr_type);
3648 
3649  // TODO: SMT2-ify
3650  SMT2_TODO("SMT2-ify");
3651 
3652 #if 0
3653  out << "(bvor ";
3654  out << "(band ";
3655 
3656  // the mask to get rid of the old bits
3657  out << " (bvnot (bvshl";
3658 
3659  out << " (concat";
3660  out << " (repeat[" << total_width-value_width << "] bv0[1])";
3661  out << " (repeat[" << value_width << "] bv1[1])";
3662  out << ")"; // concat
3663 
3664  // shift it to the index
3665  convert_expr(index_tc);
3666  out << "))"; // bvshl, bvot
3667 
3668  out << ")"; // bvand
3669 
3670  // the new value
3671  out << " (bvshl ";
3672  convert_expr(value);
3673 
3674  // shift it to the index
3675  convert_expr(index_tc);
3676  out << ")"; // bvshl
3677 
3678  out << ")"; // bvor
3679 #endif
3680  }
3681  else
3683  "with expects struct, union, or array type, but got "+
3684  expr.type().id_string());
3685 }
3686 
3688 {
3689  assert(expr.operands().size()==3);
3690 
3691  SMT2_TODO("smt2_convt::convert_update to be implemented");
3692 }
3693 
3695 {
3696  assert(expr.operands().size()==2);
3697 
3698  const typet &array_op_type=ns.follow(expr.array().type());
3699 
3700  if(array_op_type.id()==ID_array)
3701  {
3702  const array_typet &array_type=to_array_type(array_op_type);
3703 
3704  if(use_array_theory(expr.array()))
3705  {
3706  if(ns.follow(expr.type()).id()==ID_bool && !use_array_of_bool)
3707  {
3708  out << "(= ";
3709  out << "(select ";
3710  convert_expr(expr.array());
3711  out << " ";
3712  convert_expr(typecast_exprt(expr.index(), array_type.size().type()));
3713  out << ")";
3714  out << " #b1 #b0)";
3715  }
3716  else
3717  {
3718  out << "(select ";
3719  convert_expr(expr.array());
3720  out << " ";
3721  convert_expr(typecast_exprt(expr.index(), array_type.size().type()));
3722  out << ")";
3723  }
3724  }
3725  else
3726  {
3727  // fixed size
3728  std::size_t array_width=boolbv_width(array_type);
3729  assert(array_width!=0);
3730 
3731  unflatten(wheret::BEGIN, array_type.subtype());
3732 
3733  std::size_t sub_width=boolbv_width(array_type.subtype());
3734  std::size_t index_width=boolbv_width(expr.index().type());
3735 
3736  out << "((_ extract " << sub_width-1 << " 0) ";
3737  out << "(bvlshr ";
3738  convert_expr(expr.array());
3739  out << " ";
3740  out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
3741 
3742  // SMT2 says that the shift distance must be the same as
3743  // the width of what we shift.
3744  if(array_width>index_width)
3745  {
3746  out << "((_ zero_extend " << array_width-index_width << ") ";
3747  convert_expr(expr.index());
3748  out << ")"; // zero_extend
3749  }
3750  else
3751  {
3752  out << "((_ extract " << array_width-1 << " 0) ";
3753  convert_expr(expr.index());
3754  out << ")"; // extract
3755  }
3756 
3757  out << ")))"; // mult, bvlshr, extract
3758 
3759  unflatten(wheret::END, array_type.subtype());
3760  }
3761  }
3762  else if(array_op_type.id()==ID_vector)
3763  {
3764  const vector_typet &vector_type=to_vector_type(array_op_type);
3765 
3766  if(use_datatypes)
3767  {
3768  assert(datatype_map.find(vector_type)!=datatype_map.end());
3769  const std::string smt_typename=
3770  datatype_map.find(vector_type)->second;
3771 
3772  // this is easy for constant indicies
3773 
3774  mp_integer index_int;
3775  if(to_integer(expr.index(), index_int))
3776  {
3777  SMT2_TODO("non-constant index on vectors");
3778  }
3779  else
3780  {
3781  out << "(" << smt_typename << "." << index_int << " ";
3782  convert_expr(expr.array());
3783  out << ")";
3784  }
3785  }
3786  else
3787  {
3788  SMT2_TODO("index on vectors");
3789  }
3790  }
3791  else
3793  "index with unsupported array type: "+array_op_type.id_string());
3794 }
3795 
3797 {
3798  assert(expr.operands().size()==1);
3799 
3800  const member_exprt &member_expr=to_member_expr(expr);
3801  const exprt &struct_op=member_expr.struct_op();
3802  const typet &struct_op_type=ns.follow(struct_op.type());
3803  const irep_idt &name=member_expr.get_component_name();
3804 
3805  if(struct_op_type.id()==ID_struct)
3806  {
3807  const struct_typet &struct_type=
3808  to_struct_type(struct_op_type);
3809 
3810  if(!struct_type.has_component(name))
3811  INVALIDEXPR("failed to find struct member");
3812 
3813  if(use_datatypes)
3814  {
3815  assert(datatype_map.find(struct_type)!=datatype_map.end());
3816  const std::string smt_typename=
3817  datatype_map.find(struct_type)->second;
3818 
3819  out << "(" << smt_typename << "."
3820  << struct_type.get_component(name).get_name()
3821  << " ";
3822  convert_expr(struct_op);
3823  out << ")";
3824  }
3825  else
3826  {
3827  // we extract
3828  std::size_t member_width=boolbv_width(expr.type());
3829  mp_integer member_offset=::member_offset(struct_type, name, ns);
3830  if(member_offset==-1)
3831  INVALIDEXPR("failed to get struct member offset");
3832 
3833  out << "((_ extract " << (member_offset*8+member_width-1)
3834  << " " << member_offset*8 << ") ";
3835  convert_expr(struct_op);
3836  out << ")";
3837  }
3838  }
3839  else if(struct_op_type.id()==ID_union)
3840  {
3841  std::size_t width=boolbv_width(expr.type());
3842 
3843  if(width==0)
3844  INVALIDEXPR("failed to get union member width");
3845 
3846  unflatten(wheret::BEGIN, expr.type());
3847 
3848  out << "((_ extract "
3849  << (width-1)
3850  << " 0) ";
3851  convert_expr(struct_op);
3852  out << ")";
3853 
3854  unflatten(wheret::END, expr.type());
3855  }
3856  else
3858  "convert_member on an unexpected type "+struct_op_type.id_string());
3859 }
3860 
3862 {
3863  const typet &type=ns.follow(expr.type());
3864 
3865  if(type.id()==ID_bool)
3866  {
3867  out << "(ite ";
3868  convert_expr(expr); // this returns a Bool
3869  out << " #b1 #b0)"; // this is a one-bit bit-vector
3870  }
3871  else if(type.id()==ID_vector)
3872  {
3873  if(use_datatypes)
3874  {
3875  assert(datatype_map.find(type)!=datatype_map.end());
3876 
3877  const std::string smt_typename=
3878  datatype_map.find(type)->second;
3879 
3880  // concatenate elements
3881  const vector_typet &vector_type=to_vector_type(type);
3882 
3883  mp_integer size;
3884  if(to_integer(vector_type.size(), size))
3885  INVALIDEXPR("failed to convert vector size to constant");
3886 
3887  out << "(let ((?vflop ";
3888  convert_expr(expr);
3889  out << ")) ";
3890 
3891  out << "(concat";
3892 
3893  for(mp_integer i=0; i!=size; ++i)
3894  {
3895  out << " (" << smt_typename << "." << i << " ?vflop)";
3896  }
3897 
3898  out << "))"; // concat, let
3899  }
3900  else
3901  convert_expr(expr); // already a bv
3902  }
3903  else if(type.id()==ID_array)
3904  {
3905  convert_expr(expr);
3906  }
3907  else if(type.id()==ID_struct)
3908  {
3909  if(use_datatypes)
3910  {
3911  assert(datatype_map.find(type)!=datatype_map.end());
3912 
3913  const std::string smt_typename=
3914  datatype_map.find(type)->second;
3915 
3916  // concatenate elements
3917  const struct_typet &struct_type=to_struct_type(type);
3918 
3919  out << "(let ((?sflop ";
3920  convert_expr(expr);
3921  out << ")) ";
3922 
3923  const struct_typet::componentst &components=
3924  struct_type.components();
3925 
3926  // SMT-LIB 2 concat is binary only
3927  for(std::size_t i=components.size(); i>1; i--)
3928  {
3929  out << "(concat (" << smt_typename << "."
3930  << components[i-1].get_name() << " ?sflop)";
3931 
3932  out << " ";
3933  }
3934 
3935  out << "(" << smt_typename << "."
3936  << components[0].get_name() << " ?sflop)";
3937 
3938  for(std::size_t i=1; i<components.size(); i++)
3939  out << ")"; // concat
3940 
3941  out << ")"; // let
3942  }
3943  else
3944  convert_expr(expr);
3945  }
3946  else if(type.id()==ID_floatbv)
3947  {
3948  if(use_FPA_theory)
3949  INVALIDEXPR("need to flatten floatbv in FPA theory");
3950  else
3951  convert_expr(expr); // good as is
3952  }
3953  else
3954  convert_expr(expr);
3955 }
3956 
3958  wheret where,
3959  const typet &type,
3960  unsigned nesting)
3961 {
3962  if(type.id()==ID_symbol)
3963  return unflatten(where, ns.follow(type));
3964 
3965  if(type.id()==ID_bool)
3966  {
3967  if(where==wheret::BEGIN)
3968  out << "(= "; // produces a bool
3969  else
3970  out << " #b1)";
3971  }
3972  else if(type.id()==ID_vector)
3973  {
3974  if(use_datatypes)
3975  {
3976  assert(datatype_map.find(type)!=datatype_map.end());
3977 
3978  const std::string smt_typename=
3979  datatype_map.find(type)->second;
3980 
3981  // extract elements
3982  const vector_typet &vector_type=to_vector_type(type);
3983 
3984  std::size_t subtype_width=boolbv_width(vector_type.subtype());
3985 
3986  mp_integer size;
3987  if(to_integer(vector_type.size(), size))
3988  INVALIDEXPR("failed to convert vector size to constant");
3989 
3990  if(where==wheret::BEGIN)
3991  out << "(let ((?ufop" << nesting << " ";
3992  else
3993  {
3994  out << ")) ";
3995 
3996  out << "(mk-" << smt_typename;
3997 
3998  std::size_t offset=0;
3999 
4000  for(mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4001  {
4002  out << " ";
4003  unflatten(wheret::BEGIN, vector_type.subtype(), nesting+1);
4004  out << "((_ extract " << offset+subtype_width-1 << " "
4005  << offset << ") ?ufop" << nesting << ")";
4006  unflatten(wheret::END, vector_type.subtype(), nesting+1);
4007  }
4008 
4009  out << "))"; // mk-, let
4010  }
4011  }
4012  else
4013  {
4014  // nop, already a bv
4015  }
4016  }
4017  else if(type.id()==ID_struct)
4018  {
4019  if(use_datatypes)
4020  {
4021  // extract members
4022  if(where==wheret::BEGIN)
4023  out << "(let ((?ufop" << nesting << " ";
4024  else
4025  {
4026  out << ")) ";
4027 
4028  assert(datatype_map.find(type)!=datatype_map.end());
4029 
4030  const std::string smt_typename=
4031  datatype_map.find(type)->second;
4032 
4033  out << "(mk-" << smt_typename;
4034 
4035  const struct_typet &struct_type=to_struct_type(type);
4036 
4037  const struct_typet::componentst &components=
4038  struct_type.components();
4039 
4040  std::size_t offset=0;
4041 
4042  std::size_t i=0;
4043  for(struct_typet::componentst::const_iterator
4044  it=components.begin();
4045  it!=components.end();
4046  it++, i++)
4047  {
4048  std::size_t member_width=boolbv_width(it->type());
4049 
4050  out << " ";
4051  unflatten(wheret::BEGIN, it->type(), nesting+1);
4052  out << "((_ extract " << offset+member_width-1 << " "
4053  << offset << ") ?ufop" << nesting << ")";
4054  unflatten(wheret::END, it->type(), nesting+1);
4055  offset+=member_width;
4056  }
4057 
4058  out << "))"; // mk-, let
4059  }
4060  }
4061  else
4062  {
4063  // nop, already a bv
4064  }
4065  }
4066  else
4067  {
4068  // nop
4069  }
4070 }
4071 
4073 {
4074  UNREACHABLE;
4075 }
4076 
4077 void smt2_convt::set_to(const exprt &expr, bool value)
4078 {
4079  if(expr.id()==ID_and && value)
4080  {
4081  forall_operands(it, expr)
4082  set_to(*it, true);
4083  return;
4084  }
4085 
4086  if(expr.id()==ID_or && !value)
4087  {
4088  forall_operands(it, expr)
4089  set_to(*it, false);
4090  return;
4091  }
4092 
4093  if(expr.id()==ID_not)
4094  {
4095  assert(expr.operands().size()==1);
4096  return set_to(expr.op0(), !value);
4097  }
4098 
4099  out << "\n";
4100 
4101  assert(expr.type().id()==ID_bool);
4102 
4103  // special treatment for "set_to(a=b, true)" where
4104  // a is a new symbol
4105 
4106  if(expr.id()==ID_equal && value==true)
4107  {
4108  const equal_exprt &equal_expr=to_equal_expr(expr);
4109 
4110  if(equal_expr.lhs().id()==ID_symbol)
4111  {
4112  const irep_idt &identifier=
4113  to_symbol_expr(equal_expr.lhs()).get_identifier();
4114 
4115  if(identifier_map.find(identifier)==identifier_map.end())
4116  {
4117  identifiert &id=identifier_map[identifier];
4118 
4119  assert(id.type.is_nil());
4120 
4121  id.type=equal_expr.lhs().type();
4122  find_symbols(id.type);
4123  find_symbols(equal_expr.rhs());
4124 
4125  std::string smt2_identifier=convert_identifier(identifier);
4126  smt2_identifiers.insert(smt2_identifier);
4127 
4128  out << "; set_to true (equal)\n";
4129  out << "(define-fun |" << smt2_identifier << "| () ";
4130 
4131  convert_type(equal_expr.lhs().type());
4132  out << " ";
4133  convert_expr(equal_expr.rhs());
4134 
4135  out << ")" << "\n";
4136  return; // done
4137  }
4138  }
4139  }
4140 
4141  find_symbols(expr);
4142 
4143  #if 0
4144  out << "; CONV: "
4145  << format(expr) << "\n";
4146  #endif
4147 
4148  out << "; set_to " << (value?"true":"false") << "\n"
4149  << "(assert ";
4150 
4151  if(!value)
4152  {
4153  out << "(not ";
4154  convert_expr(expr);
4155  out << ")";
4156  }
4157  else
4158  convert_expr(expr);
4159 
4160  out << ")" << "\n"; // assert
4161 
4162  return;
4163 }
4164 
4166 {
4167  // recursive call on type
4168  find_symbols(expr.type());
4169 
4170  // recursive call on operands
4171  forall_operands(it, expr)
4172  find_symbols(*it);
4173 
4174  if(expr.id()==ID_symbol ||
4175  expr.id()==ID_nondet_symbol)
4176  {
4177  // we don't track function-typed symbols
4178  if(expr.type().id()==ID_code)
4179  return;
4180 
4181  irep_idt identifier;
4182 
4183  if(expr.id()==ID_symbol)
4184  identifier=to_symbol_expr(expr).get_identifier();
4185  else
4186  identifier="nondet_"+
4187  id2string(to_nondet_symbol_expr(expr).get_identifier());
4188 
4189  identifiert &id=identifier_map[identifier];
4190 
4191  if(id.type.is_nil())
4192  {
4193  id.type=expr.type();
4194 
4195  std::string smt2_identifier=convert_identifier(identifier);
4196  smt2_identifiers.insert(smt2_identifier);
4197 
4198  out << "; find_symbols\n";
4199  out << "(declare-fun |"
4200  << smt2_identifier
4201  << "| () ";
4202  convert_type(expr.type());
4203  out << ")" << "\n";
4204  }
4205  }
4206  else if(expr.id()==ID_array_of)
4207  {
4208  if(defined_expressions.find(expr)==defined_expressions.end())
4209  {
4210  irep_idt id="array_of."+std::to_string(defined_expressions.size());
4211  out << "; the following is a substitute for lambda i. x" << "\n";
4212  out << "(declare-fun " << id << " () ";
4213  convert_type(expr.type());
4214  out << ")" << "\n";
4215 
4216  // use a quantifier instead of the lambda
4217  #if 0 // not really working in any solver yet!
4218  out << "(assert (forall ((i ";
4219  convert_type(array_index_type());
4220  out << ")) (= (select " << id << " i) ";
4221  convert_expr(expr.op0());
4222  out << ")))" << "\n";
4223  #endif
4224 
4225  defined_expressions[expr]=id;
4226  }
4227  }
4228  else if(expr.id()==ID_array)
4229  {
4230  if(defined_expressions.find(expr)==defined_expressions.end())
4231  {
4232  const array_typet &array_type=to_array_type(expr.type());
4233 
4234  irep_idt id="array."+std::to_string(defined_expressions.size());
4235  out << "; the following is a substitute for an array constructor" << "\n";
4236  out << "(declare-fun " << id << " () ";
4237  convert_type(array_type);
4238  out << ")" << "\n";
4239 
4240  for(std::size_t i=0; i<expr.operands().size(); i++)
4241  {
4242  out << "(assert (= (select " << id << " ";
4243  convert_expr(from_integer(i, array_type.size().type()));
4244  out << ") "; // select
4245  convert_expr(expr.operands()[i]);
4246  out << "))" << "\n"; // =, assert
4247  }
4248 
4249  defined_expressions[expr]=id;
4250  }
4251  }
4252  else if(expr.id()==ID_string_constant)
4253  {
4254  if(defined_expressions.find(expr)==defined_expressions.end())
4255  {
4256  // introduce a temporary array.
4258  const array_typet &array_type=to_array_type(tmp.type());
4259 
4260  irep_idt id="string."+std::to_string(defined_expressions.size());
4261  out << "; the following is a substitute for a string" << "\n";
4262  out << "(declare-fun " << id << " () ";
4263  convert_type(array_type);
4264  out << ")" << "\n";
4265 
4266  for(std::size_t i=0; i<tmp.operands().size(); i++)
4267  {
4268  out << "(assert (= (select " << id;
4269  convert_expr(from_integer(i, array_type.size().type()));
4270  out << ") "; // select
4271  convert_expr(tmp.operands()[i]);
4272  out << "))" << "\n";
4273  }
4274 
4275  defined_expressions[expr]=id;
4276  }
4277  }
4278  else if(expr.id()==ID_object_size &&
4279  expr.operands().size()==1)
4280  {
4281  const exprt &op = expr.op0();
4282 
4283  if(op.type().id()==ID_pointer)
4284  {
4285  if(object_sizes.find(expr)==object_sizes.end())
4286  {
4287  irep_idt id="object_size."+std::to_string(object_sizes.size());
4288  out << "(declare-fun " << id << " () ";
4289  convert_type(expr.type());
4290  out << ")" << "\n";
4291 
4292  object_sizes[expr]=id;
4293  }
4294  }
4295  }
4296  else if(!use_FPA_theory &&
4297  expr.operands().size()>=1 &&
4298  (expr.id()==ID_floatbv_plus ||
4299  expr.id()==ID_floatbv_minus ||
4300  expr.id()==ID_floatbv_mult ||
4301  expr.id()==ID_floatbv_div ||
4302  expr.id()==ID_floatbv_typecast ||
4303  expr.id()==ID_ieee_float_equal ||
4304  expr.id()==ID_ieee_float_notequal ||
4305  ((expr.id()==ID_lt ||
4306  expr.id()==ID_gt ||
4307  expr.id()==ID_le ||
4308  expr.id()==ID_ge ||
4309  expr.id()==ID_isnan ||
4310  expr.id()==ID_isnormal ||
4311  expr.id()==ID_isfinite ||
4312  expr.id()==ID_isinf ||
4313  expr.id()==ID_sign ||
4314  expr.id()==ID_unary_minus ||
4315  expr.id()==ID_typecast ||
4316  expr.id()==ID_abs) &&
4317  expr.op0().type().id()==ID_floatbv)))
4318  {
4319  irep_idt function=
4320  "|float_bv."+expr.id_string()+floatbv_suffix(expr)+"|";
4321 
4322  if(bvfp_set.insert(function).second)
4323  {
4324  out << "; this is a model for " << expr.id()
4325  << " : " << type2id(expr.op0().type())
4326  << " -> " << type2id(expr.type()) << "\n"
4327  << "(define-fun " << function << " (";
4328 
4329  for(std::size_t i = 0; i < expr.operands().size(); i++)
4330  {
4331  if(i!=0)
4332  out << " ";
4333  out << "(op" << i << ' ';
4334  convert_type(expr.operands()[i].type());
4335  out << ')';
4336  }
4337 
4338  out << ") ";
4339  convert_type(expr.type()); // return type
4340  out << ' ';
4341 
4342  exprt tmp1=expr;
4343  for(std::size_t i = 0; i < tmp1.operands().size(); i++)
4344  tmp1.operands()[i]=
4345  smt2_symbolt("op"+std::to_string(i), tmp1.operands()[i].type());
4346 
4347  exprt tmp2=float_bv(tmp1);
4348  tmp2=letify(tmp2);
4349 
4350  assert(!tmp2.is_nil());
4351  convert_expr(tmp2);
4352 
4353  out << ")\n"; // define-fun
4354  }
4355  }
4356 }
4357 
4359 {
4360  const typet &type=ns.follow(expr.type());
4361  PRECONDITION(type.id()==ID_array);
4362  // const array_typet &array_type=to_array_type(ns.follow(expr.type()));
4363 
4364  if(use_datatypes)
4365  {
4366  return true; // always use array theory when we have datatypes
4367  }
4368  else
4369  {
4370  // arrays inside structs get flattened
4371  if(expr.id()==ID_with)
4372  return use_array_theory(to_with_expr(expr).old());
4373  else if(expr.id()==ID_member)
4374  return false;
4375  else
4376  return true;
4377  }
4378 }
4379 
4381 {
4382  if(type.id()==ID_array)
4383  {
4384  const array_typet &array_type=to_array_type(type);
4385 
4386  // we always use array theory for top-level arrays
4387  const typet &subtype=ns.follow(array_type.subtype());
4388 
4389  out << "(Array ";
4390  assert(array_type.size().is_not_nil());
4391  convert_type(array_type.size().type());
4392  out << " ";
4393 
4394  if(subtype.id()==ID_bool && !use_array_of_bool)
4395  out << "(_ BitVec 1)";
4396  else
4397  convert_type(array_type.subtype());
4398 
4399  out << ")";
4400  }
4401  else if(type.id()==ID_bool)
4402  {
4403  out << "Bool";
4404  }
4405  else if(type.id()==ID_struct)
4406  {
4407  if(use_datatypes)
4408  {
4409  assert(datatype_map.find(type)!=datatype_map.end());
4410  out << datatype_map.find(type)->second;
4411  }
4412  else
4413  {
4414  std::size_t width=boolbv_width(type);
4415 
4416  if(width==0)
4417  INVALIDEXPR("failed to get width of struct");
4418 
4419  out << "(_ BitVec " << width << ")";
4420  }
4421  }
4422  else if(type.id()==ID_vector)
4423  {
4424  if(use_datatypes)
4425  {
4426  assert(datatype_map.find(type)!=datatype_map.end());
4427  out << datatype_map.find(type)->second;
4428  }
4429  else
4430  {
4432 
4433  std::size_t width=boolbv_width(type);
4434 
4435  if(width==0)
4436  INVALIDEXPR("failed to get width of vector");
4437 
4438  out << "(_ BitVec " << width << ")";
4439  }
4440  }
4441  else if(type.id()==ID_code)
4442  {
4443  // These may appear in structs.
4444  // We replace this by "Bool" in order to keep the same
4445  // member count.
4446  out << "Bool";
4447  }
4448  else if(type.id()==ID_union)
4449  {
4451 
4452  std::size_t width=boolbv_width(type);
4453 
4454  if(width==0)
4455  INVALIDEXPR("failed to get width of union");
4456 
4457  out << "(_ BitVec " << width << ")";
4458  }
4459  else if(type.id()==ID_pointer)
4460  {
4461  out << "(_ BitVec "
4462  << boolbv_width(type) << ")";
4463  }
4464  else if(type.id()==ID_bv ||
4465  type.id()==ID_fixedbv ||
4466  type.id()==ID_unsignedbv ||
4467  type.id()==ID_signedbv ||
4468  type.id()==ID_c_bool)
4469  {
4470  out << "(_ BitVec "
4471  << to_bitvector_type(type).get_width() << ")";
4472  }
4473  else if(type.id()==ID_c_enum)
4474  {
4475  // these have a subtype
4476  out << "(_ BitVec "
4477  << to_bitvector_type(type.subtype()).get_width() << ")";
4478  }
4479  else if(type.id()==ID_c_enum_tag)
4480  {
4482  }
4483  else if(type.id()==ID_floatbv)
4484  {
4485  const floatbv_typet &floatbv_type=to_floatbv_type(type);
4486 
4487  if(use_FPA_theory)
4488  out << "(_ FloatingPoint "
4489  << floatbv_type.get_e() << " "
4490  << floatbv_type.get_f() + 1 << ")";
4491  else
4492  out << "(_ BitVec "
4493  << floatbv_type.get_width() << ")";
4494  }
4495  else if(type.id()==ID_rational ||
4496  type.id()==ID_real)
4497  out << "Real";
4498  else if(type.id()==ID_integer)
4499  out << "Int";
4500  else if(type.id()==ID_symbol)
4501  convert_type(ns.follow(type));
4502  else if(type.id()==ID_complex)
4503  {
4504  if(use_datatypes)
4505  {
4506  assert(datatype_map.find(type)!=datatype_map.end());
4507  out << datatype_map.find(type)->second;
4508  }
4509  else
4510  {
4512 
4513  std::size_t width=boolbv_width(type);
4514 
4515  if(width==0)
4516  INVALIDEXPR("failed to get width of complex");
4517 
4518  out << "(_ BitVec " << width << ")";
4519  }
4520  }
4521  else if(type.id()==ID_c_bit_field)
4522  {
4524  }
4525  else
4526  {
4527  UNEXPECTEDCASE("unsupported type: "+type.id_string());
4528  }
4529 }
4530 
4532 {
4533  std::set<irep_idt> recstack;
4534  find_symbols_rec(type, recstack);
4535 }
4536 
4538  const typet &type,
4539  std::set<irep_idt> &recstack)
4540 {
4541  if(type.id()==ID_array)
4542  {
4543  const array_typet &array_type=to_array_type(type);
4544  find_symbols(array_type.size());
4545  find_symbols_rec(array_type.subtype(), recstack);
4546  }
4547  else if(type.id()==ID_incomplete_array)
4548  {
4549  find_symbols_rec(type.subtype(), recstack);
4550  }
4551  else if(type.id()==ID_complex)
4552  {
4553  find_symbols_rec(type.subtype(), recstack);
4554 
4555  if(use_datatypes &&
4556  datatype_map.find(type)==datatype_map.end())
4557  {
4558  std::string smt_typename = "complex."+std::to_string(datatype_map.size());
4559  datatype_map[type] = smt_typename;
4560 
4561  out << "(declare-datatypes () ((" << smt_typename << " "
4562  << "(mk-" << smt_typename;
4563 
4564  out << " (" << smt_typename << ".imag ";
4565  convert_type(type.subtype());
4566  out << ")";
4567 
4568  out << " (" << smt_typename << ".real ";
4569  convert_type(type.subtype());
4570  out << ")";
4571 
4572  out << "))))\n";
4573  }
4574  }
4575  else if(type.id()==ID_vector)
4576  {
4577  find_symbols_rec(type.subtype(), recstack);
4578 
4579  if(use_datatypes &&
4580  datatype_map.find(type)==datatype_map.end())
4581  {
4582  const vector_typet &vector_type=to_vector_type(type);
4583 
4584  mp_integer size;
4585  if(to_integer(vector_type.size(), size))
4586  INVALIDEXPR("failed to convert vector size to constant");
4587 
4588  std::string smt_typename = "vector."+std::to_string(datatype_map.size());
4589  datatype_map[type] = smt_typename;
4590 
4591  out << "(declare-datatypes () ((" << smt_typename << " "
4592  << "(mk-" << smt_typename;
4593 
4594  for(mp_integer i=0; i!=size; ++i)
4595  {
4596  out << " (" << smt_typename << "." << i << " ";
4597  convert_type(type.subtype());
4598  out << ")";
4599  }
4600 
4601  out << "))))\n";
4602  }
4603  }
4604  else if(type.id()==ID_struct)
4605  {
4606  // Cater for mutually recursive struct types
4607  bool need_decl=false;
4608  if(use_datatypes &&
4609  datatype_map.find(type)==datatype_map.end())
4610  {
4611  std::string smt_typename = "struct."+std::to_string(datatype_map.size());
4612  datatype_map[type] = smt_typename;
4613  need_decl=true;
4614  }
4615 
4616  const struct_typet::componentst &components=
4617  to_struct_type(type).components();
4618 
4619  for(const auto &component : components)
4620  find_symbols_rec(component.type(), recstack);
4621 
4622  // Declare the corresponding SMT type if we haven't already.
4623  if(need_decl)
4624  {
4625  std::string smt_typename = datatype_map[type];
4626 
4627  // We're going to create a datatype named something like `struct.0'.
4628  // It's going to have a single constructor named `mk-struct.0' with an
4629  // argument for each member of the struct. The declaration that
4630  // creates this type looks like:
4631  //
4632  // (declare-datatypes () ((struct.0 (mk-struct.0
4633  // (struct.0.component1 type1)
4634  // ...
4635  // (struct.0.componentN typeN)))))
4636  out << "(declare-datatypes () ((" << smt_typename << " "
4637  << "(mk-" << smt_typename << " ";
4638 
4639  for(const auto &component : components)
4640  {
4641  out << "(" << smt_typename << "." << component.get_name()
4642  << " ";
4643  convert_type(component.type());
4644  out << ") ";
4645  }
4646 
4647  out << "))))" << "\n";
4648 
4649  // Let's also declare convenience functions to update individual
4650  // members of the struct whil we're at it. The functions are
4651  // named like `update-struct.0.component1'. Their declarations
4652  // look like:
4653  //
4654  // (declare-fun update-struct.0.component1
4655  // ((s struct.0) ; first arg -- the struct to update
4656  // (v type1)) ; second arg -- the value to update
4657  // struct.0 ; the output type
4658  // (mk-struct.0 ; build the new struct...
4659  // v ; the updated value
4660  // (struct.0.component2 s) ; retain the other members
4661  // ...
4662  // (struct.0.componentN s)))
4663 
4664  for(struct_union_typet::componentst::const_iterator
4665  it=components.begin();
4666  it!=components.end();
4667  ++it)
4668  {
4669  const struct_union_typet::componentt &component=*it;
4670  out << "(define-fun update-" << smt_typename << "."
4671  << component.get_name() << " "
4672  << "((s " << smt_typename << ") "
4673  << "(v ";
4674  convert_type(component.type());
4675  out << ")) " << smt_typename << " "
4676  << "(mk-" << smt_typename
4677  << " ";
4678 
4679  for(struct_union_typet::componentst::const_iterator
4680  it2=components.begin();
4681  it2!=components.end();
4682  ++it2)
4683  {
4684  if(it==it2)
4685  out << "v ";
4686  else
4687  {
4688  out << "(" << smt_typename << "."
4689  << it2->get_name() << " s) ";
4690  }
4691  }
4692 
4693  out << "))" << "\n";
4694  }
4695 
4696  out << "\n";
4697  }
4698  }
4699  else if(type.id()==ID_union)
4700  {
4701  const union_typet::componentst &components=
4702  to_union_type(type).components();
4703 
4704  for(const auto &component : components)
4705  find_symbols_rec(component.type(), recstack);
4706  }
4707  else if(type.id()==ID_code)
4708  {
4709  const code_typet::parameterst &parameters=
4710  to_code_type(type).parameters();
4711  for(const auto &param : parameters)
4712  find_symbols_rec(param.type(), recstack);
4713 
4714  find_symbols_rec(to_code_type(type).return_type(), recstack);
4715  }
4716  else if(type.id()==ID_pointer)
4717  {
4718  find_symbols_rec(type.subtype(), recstack);
4719  }
4720  else if(type.id()==ID_symbol)
4721  {
4722  const symbol_typet &st=to_symbol_type(type);
4723  const irep_idt &id=st.get_identifier();
4724 
4725  if(recstack.find(id)==recstack.end())
4726  {
4727  recstack.insert(id);
4728  find_symbols_rec(ns.follow(type), recstack);
4729  }
4730  }
4731 }
4732 
4734 {
4735  seen_expressionst map;
4736  std::vector<exprt> let_order;
4737 
4738  collect_bindings(expr, map, let_order);
4739 
4740  return letify_rec(expr, let_order, map, 0);
4741 }
4742 
4744  exprt &expr,
4745  std::vector<exprt> &let_order,
4746  const seen_expressionst &map,
4747  std::size_t i)
4748 {
4749  if(i>=let_order.size())
4750  return substitute_let(expr, map);
4751 
4752  exprt current=let_order[i];
4753  assert(map.find(current)!=map.end());
4754 
4755  if(map.find(current)->second.count < LET_COUNT)
4756  return letify_rec(expr, let_order, map, i+1);
4757 
4758  let_exprt let;
4759 
4760  let.symbol() = map.find(current)->second.let_symbol;
4761  let.value() = substitute_let(current, map);
4762  let.where() = letify_rec(expr, let_order, map, i+1);
4763 
4764  return let;
4765 }
4766 
4768  exprt &expr,
4769  seen_expressionst &map,
4770  std::vector<exprt> &let_order)
4771 {
4772  seen_expressionst::iterator it = map.find(expr);
4773 
4774  if(it!=map.end())
4775  {
4776  let_count_idt &count_id=it->second;
4777  ++(count_id.count);
4778  return;
4779  }
4780 
4781  // do not letify things with no children
4782  if(expr.operands().empty())
4783  return;
4784 
4785  Forall_operands(it, expr)
4786  collect_bindings(*it, map, let_order);
4787 
4788  assert(map.find(expr)==map.end());
4789 
4790  symbol_exprt let=
4791  symbol_exprt("_let_"+std::to_string(++let_id_count), expr.type());
4792 
4793  map.insert(std::make_pair(expr, let_count_idt(1, let)));
4794 
4795  let_order.push_back(expr);
4796 }
4797 
4799  exprt &expr,
4800  const seen_expressionst &map)
4801 {
4802  if(expr.operands().empty())
4803  return expr;
4804 
4805  let_visitort lv(map);
4806 
4807  Forall_operands(it, expr)
4808  it->visit(lv);
4809 
4810  return expr;
4811 }
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:3957
The type of an expression.
Definition: type.h:22
std::size_t get_e() const
Definition: std_types.h:1358
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:1229
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:3861
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: smt2_conv.cpp:2370
exprt parse_array(const irept &s, const array_typet &type)
Definition: smt2_conv.cpp:339
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
exprt letify(exprt &expr)
Definition: smt2_conv.cpp:4733
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:1296
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:1159
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1351
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:1873
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:993
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3121
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:2646
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:3687
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:4439
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:3476
exprt & new_value()
Definition: std_expr.h:3496
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:2927
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:4422
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
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:2579
configt config
Definition: config.cpp:23
identifier_mapt identifier_map
Definition: smt2_conv.h:293
void convert_type(const typet &)
Definition: smt2_conv.cpp:4380
#define forall_literals(it, bv)
Definition: literal.h:202
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:80
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:4358
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
Definition: std_expr.h:4753
subt & get_sub()
Definition: irep.h:317
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:1561
Extract member of struct or union.
Definition: std_expr.h:3869
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3418
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
exprt & where()
Definition: std_expr.h:4732
equality
Definition: std_expr.h:1354
exprt substitute_let(exprt &expr, const seen_expressionst &map)
Definition: smt2_conv.cpp:4798
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:4373
void convert_mult(const mult_exprt &expr)
Definition: smt2_conv.cpp:3343
void convert_relation(const exprt &expr)
Definition: smt2_conv.cpp:2842
exprt object_size(const exprt &pointer)
const irep_idt & id() const
Definition: irep.h:259
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:4486
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:2782
The NIL expression.
Definition: std_expr.h:4508
void convert_floatbv_div(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3324
void convert_struct(const struct_exprt &expr)
Definition: smt2_conv.cpp:2516
The pointer type.
Definition: std_types.h:1435
std::size_t get_fraction_bits() const
Definition: std_types.h:1320
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
Definition: smt2_conv.cpp:3065
void convert_div(const div_exprt &expr)
Definition: smt2_conv.cpp:3278
A constant-size array type.
Definition: std_types.h:1638
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:164
API to expression classes.
void convert_index(const index_exprt &expr)
Definition: smt2_conv.cpp:3694
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:4743
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:1648
Left shift.
Definition: std_expr.h:2848
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt2_conv.cpp:4537
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1669
const exprt & size() const
Definition: std_types.h:1023
Base class for tree-like data structures with sharing.
Definition: irep.h:156
#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:3157
size_t size() const
Definition: dstring.h:89
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::string floatbv_suffix(const exprt &) const
Definition: smt2_conv.cpp:827
Operator to return the address of an object.
Definition: std_expr.h:3168
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:4463
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: std_types.h:1313
The boolean constant false.
Definition: std_expr.h:4497
bool is_constant() const
Definition: expr.cpp:119
std::size_t get_width() const
Definition: std_types.h:1138
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:199
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:1254
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:4916
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
Definition: std_expr.h:3517
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:4722
#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:1382
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:1343
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:2803
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:1054
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:3909
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:3459
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:4072
irep_idt get_component_name() const
Definition: std_expr.h:3893
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
#define UNREACHABLE
Definition: invariant.h:271
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:4165
std::size_t no_boolean_variables
Definition: smt2_conv.h:315
void convert_member(const member_exprt &expr)
Definition: smt2_conv.cpp:3796
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:445
const std::string & id_string() const
Definition: irep.h:262
void swap(irept &irep)
Definition: irep.h:303
#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:1013
void convert_union(const union_exprt &expr)
Definition: smt2_conv.cpp:2613
virtual void set_to(const exprt &expr, bool value)
Definition: smt2_conv.cpp:4077
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:3437
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:1411
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:1459
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:4712
std::size_t width() const
Definition: ieee_float.h:54
dstringt irep_idt
Definition: irep.h:32
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:3486
Base Type Computation.
A let expression.
Definition: std_expr.h:4703
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:278
#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:1193
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:4314
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:35
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:286
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:3259
void collect_bindings(exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
Definition: smt2_conv.cpp:4767
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