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