cprover
smt1_conv.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: SMT Version 1 Backend
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "smt1_conv.h"
13 
14 #include <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/std_types.h>
18 #include <util/std_expr.h>
19 #include <util/fixedbv.h>
21 #include <util/base_type.h>
22 #include <util/ieee_float.h>
23 #include <util/byte_operators.h>
24 #include <util/c_types.h>
25 
26 #include <ansi-c/string_constant.h>
27 
28 #include <langapi/language_util.h>
29 
34 
35 void smt1_convt::print_assignment(std::ostream &out) const
36 {
37  // Boolean stuff
38 
39  for(std::size_t v=0; v<boolean_assignment.size(); v++)
40  out << "b" << v << "=" << boolean_assignment[v] << "\n";
41 
42  // others
43 }
44 
46 {
47  if(l.is_true())
48  return tvt(true);
49  if(l.is_false())
50  return tvt(false);
51  assert(l.var_no()<boolean_assignment.size());
52  return tvt(boolean_assignment[l.var_no()]^l.sign());
53 }
54 
56 {
57  write_footer();
58  out.flush();
60 }
61 
63 {
64  out << "(benchmark " << benchmark << "\n";
65  out << ":source { " << source << " }" << "\n";
66  out << ":status unknown" << "\n";
67  out << ":logic " << logic << " ; SMT1" << "\n";
68 }
69 
71 {
72  out << "\n";
73  out << ":formula true" << "\n";
74  out << ") ; benchmark" << "\n";
75 }
76 
77 exprt smt1_convt::get(const exprt &expr) const
78 {
79  if(expr.id()==ID_symbol)
80  {
81  const irep_idt &id=to_symbol_expr(expr).get_identifier();
82 
83  identifier_mapt::const_iterator it=identifier_map.find(id);
84 
85  if(it!=identifier_map.end())
86  return it->second.value;
87  }
88  else if(expr.id()==ID_member)
89  {
90  const member_exprt &member_expr=to_member_expr(expr);
91  exprt tmp=get(member_expr.struct_op());
92  if(tmp.is_nil())
93  return nil_exprt();
94  return member_exprt(tmp, member_expr.get_component_name(), expr.type());
95  }
96  else if(expr.id()==ID_index)
97  {
98  const index_exprt &index_expr=to_index_expr(expr);
99  exprt tmp_array=get(index_expr.array());
100  exprt tmp_index=get(index_expr.index());
101  if(tmp_array.is_nil() || tmp_index.is_nil())
102  return nil_exprt();
103  return index_exprt(tmp_array, tmp_index, expr.type());
104  }
105  else if(expr.id()==ID_constant)
106  return expr;
107  else if(expr.id()==ID_typecast)
108  {
109  exprt tmp=get(to_typecast_expr(expr).op());
110  if(tmp.is_nil())
111  return nil_exprt();
112  return typecast_exprt(tmp, expr.type());
113  }
114 
115  return nil_exprt();
116 }
117 
119  const typet &type,
120  const std::string &index,
121  const std::string &value,
122  bool in_struct) const
123 {
124  if(type.id()==ID_symbol)
125  return ce_value(ns.follow(type), index, value, in_struct);
126 
127  if(type.id()==ID_signedbv ||
128  type.id()==ID_unsignedbv ||
129  type.id()==ID_bv ||
130  type.id()==ID_fixedbv)
131  {
132  assert(value.size()==boolbv_width(type));
133  constant_exprt c(type);
134  c.set_value(value);
135  return c;
136  }
137  else if(type.id()==ID_bool)
138  {
139  if(value=="1")
140  return true_exprt();
141  else if(value=="0")
142  return false_exprt();
143  }
144  else if(type.id()==ID_pointer)
145  {
146  assert(value.size()==boolbv_width(type));
147 
148  constant_exprt result(type);
149  result.set_value(value);
150 
151  // add the elaborated expression as operand
152 
156  value.substr(0, BV_ADDR_BITS), false));
157 
158  p.offset=
159  binary2integer(value.substr(BV_ADDR_BITS, std::string::npos), true);
160 
161  result.copy_to_operands(pointer_logic.pointer_expr(p, type));
162 
163  return result;
164  }
165  else if(type.id()==ID_struct)
166  {
167  return binary2struct(to_struct_type(type), value);
168  }
169  else if(type.id()==ID_union)
170  {
171  return binary2union(to_union_type(type), value);
172  }
173  else if(type.id()==ID_array)
174  {
175  const typet &subtype=ns.follow(type.subtype());
176 
177  // arrays in structs are flat, no index
178  if(in_struct)
179  {
180  // we can only do fixed-size arrays
181  mp_integer size;
182 
183  if(!to_integer(to_array_type(type).size(), size))
184  {
185  std::size_t size_int=integer2unsigned(size);
186  std::size_t sub_width=value.size()/size_int;
187  exprt array_list(ID_array, type);
188  array_list.operands().resize(size_int);
189 
190  std::size_t offset=value.size();
191 
192  for(std::size_t i=0; i!=size_int; i++)
193  {
194  offset-=sub_width;
195  std::string sub_value=value.substr(offset, sub_width);
196  array_list.operands()[i]=
197  ce_value(subtype, "", sub_value, true);
198  }
199 
200  return array_list;
201  }
202  }
203  else if(subtype.id()==ID_array)
204  {
205  // a 2 dimensional array - second dimension is flattened
206  return ce_value(subtype, "", value, true);
207  }
208  else
209  {
210  exprt value_expr=ce_value(subtype, "", value, in_struct);
211 
212  if(index=="")
213  return nil_exprt();
214 
215  // use index, recusive call
216  exprt index_expr=
217  ce_value(signedbv_typet(index.size()), "", index, false);
218 
219  if(index_expr.is_nil())
220  return nil_exprt();
221 
222  exprt array_list("array-list", type);
223  array_list.copy_to_operands(index_expr, value_expr);
224 
225  return array_list;
226  }
227  }
228 
229  return nil_exprt();
230 }
231 
233 {
234  signedbv_typet t;
236  return t;
237 }
238 
240 {
241  if(expr.type().id()==ID_integer)
242  return convert_expr(expr, true);
243 
245  if(t==expr.type())
246  return convert_expr(expr, true);
247  exprt tmp(ID_typecast, t);
248  tmp.copy_to_operands(expr);
249  convert_expr(tmp, true);
250 }
251 
253  const exprt &expr,
254  const pointer_typet &result_type)
255 {
256  if(expr.id()==ID_symbol ||
257  expr.id()==ID_constant ||
258  expr.id()==ID_string_constant ||
259  expr.id()==ID_label)
260  {
261  out
262  << "(concat"
263  << " bv" << pointer_logic.add_object(expr) << "[" << BV_ADDR_BITS << "]"
264  << " bv0[" << boolbv_width(result_type)-BV_ADDR_BITS << "]"
265  << ")";
266  }
267  else if(expr.id()==ID_index)
268  {
269  if(expr.operands().size()!=2)
270  throw "index takes two operands";
271 
272  const exprt &array=to_index_expr(expr).array();
273  const exprt &index=to_index_expr(expr).index();
274 
275  if(index.is_zero())
276  {
277  if(array.type().id()==ID_pointer)
278  convert_expr(array, true);
279  else if(array.type().id()==ID_array)
280  convert_address_of_rec(array, result_type);
281  else
282  assert(false);
283  }
284  else
285  {
286  // this is really pointer arithmetic
287  exprt new_index_expr=expr;
288  new_index_expr.op1()=from_integer(0, index.type());
289 
290  address_of_exprt address_of_expr(
291  new_index_expr,
292  pointer_type(array.type().subtype()));
293 
294  plus_exprt plus_expr(
295  address_of_expr,
296  index,
297  address_of_expr.type());
298 
299  convert_expr(plus_expr, true);
300  }
301  }
302  else if(expr.id()==ID_member)
303  {
304  if(expr.operands().size()!=1)
305  throw "member takes one operand";
306 
307  const member_exprt &member_expr=to_member_expr(expr);
308 
309  const exprt &struct_op=member_expr.struct_op();
310  const typet &struct_op_type=ns.follow(struct_op.type());
311 
312  if(struct_op_type.id()==ID_struct)
313  {
314  const struct_typet &struct_type=
315  to_struct_type(struct_op_type);
316 
317  const irep_idt &component_name=
318  member_expr.get_component_name();
319 
320  mp_integer offset=member_offset(struct_type, component_name, ns);
321  assert(offset>=0);
322 
323  typet index_type(ID_unsignedbv);
324  index_type.set(ID_width, boolbv_width(result_type));
325 
326  out << "(bvadd ";
327  convert_address_of_rec(struct_op, result_type);
328  out << " ";
329  convert_expr(from_integer(offset, index_type), true);
330  out << ")";
331  }
332  else if(struct_op_type.id()==ID_union)
333  {
334  // these all have offset 0
335  convert_address_of_rec(struct_op, result_type);
336  }
337  else
338  throw "unexpected type of member operand";
339  }
340  else if(expr.id()==ID_if)
341  {
342  assert(expr.operands().size()==3);
343 
344  out << "(ite ";
345  convert_expr(expr.op0(), false);
346  out << " ";
347  convert_address_of_rec(expr.op1(), result_type);
348  out << " ";
349  convert_address_of_rec(expr.op2(), result_type);
350  out << ")";
351  }
352  else
353  throw "don't know how to take address of: "+expr.id_string();
354 }
355 
357  const byte_extract_exprt &expr,
358  bool bool_as_bv)
359 {
360  // we just run the flattener
361  exprt flattened_expr=flatten_byte_extract(expr, ns);
362  convert_expr(flattened_expr, bool_as_bv);
363 }
364 
366  const exprt &expr,
367  bool bool_as_bv)
368 {
369  assert(expr.operands().size()==3);
370 
371  // The situation: expr.op0 needs to be split in 3 parts
372  // |<--- L --->|<--- M --->|<--- R --->|
373  // where M is the expr.op1'th byte
374  // We need to output L expr.op2 R
375 
376  mp_integer i;
377  if(to_integer(expr.op1(), i))
378  throw "byte_update takes constant as second operand";
379 
380  std::size_t w=boolbv_width(expr.op0().type());
381 
382  if(w==0)
383  throw "failed to get width of byte_update operand";
384 
385  mp_integer upper, lower; // of the byte
386  mp_integer max=w-1;
387  std::size_t op_w = boolbv_width(expr.op2().type());
388 
389  if(expr.id()==ID_byte_update_little_endian)
390  {
391  lower = i*8;
392  upper = lower+op_w-1;
393  }
394  else
395  {
396  upper = max-(i*8);
397  lower = max-(i*8+op_w-1);
398  }
399 
400  if(upper==max)
401  {
402  if(lower==0) // there was only one byte
403  convert_expr(expr.op2(), true);
404  else // uppermost byte selected, only R needed
405  {
406  out << "(concat ";
407  convert_expr(expr.op2(), true);
408  out << " (extract[" << lower-1 << ":0] ";
409  convert_expr(expr.op0(), true);
410  out << ")"; // extract
411  out << ")"; // concat
412  }
413  }
414  else
415  {
416  if(lower==0) // lowermost byte selected, only L needed
417  {
418  out << "(concat ";
419  out << "(extract[" << max << ":" << (upper+1) << "] ";
420  convert_expr(expr.op0(), true);
421  out << ") ";
422  convert_expr(expr.op2(), true);
423  out << ")";
424  }
425  else // byte in the middle selected, L & R needed
426  {
427  out << "(concat (concat";
428  out << " (extract[" << max << ":" << (upper+1) << "] ";
429  convert_expr(expr.op0(), true);
430  out << ")"; // extract
431  out << " ";
432  convert_expr(expr.op2(), true);
433  out << ")"; // concat
434  out<< " (extract[" << (lower-1) << ":0] ";
435  convert_expr(expr.op0(), true);
436  out << ")"; // extract
437  out << ")"; // concat
438  }
439  }
440 }
441 
443 {
444  assert(expr.type().id()==ID_bool);
445 
446  // Trivial cases that don't need a new handle.
447 
448  if(expr.is_true())
449  return const_literal(true);
450  else if(expr.is_false())
451  return const_literal(false);
452  else if(expr.id()==ID_literal)
453  return to_literal_expr(expr).get_literal();
454 
455  // Ok, need new handle
456 
457  out << "\n";
458 
459  find_symbols(expr);
460 
461  literalt l(no_boolean_variables, false);
463 
464  out << ":extrapreds((";
465  convert_literal(l);
466  out << "))" << "\n";
467 
468  out << ":assumption ; convert " << "\n"
469  << " (iff ";
470  convert_literal(l);
471  out << " ";
472  convert_expr(expr, false);
473  out << ")" << "\n";
474 
475  return l;
476 }
477 
478 std::string smt1_convt::convert_identifier(const irep_idt &identifier)
479 {
480  std::string s=id2string(identifier), dest;
481  dest.reserve(s.size());
482 
483  // a sequence of letters, digits, dots (.), single quotes (’), and
484  // underscores (_), starting with a letter
485 
486  // MathSAT does not really seem to like the single quotes '
487  // so we avoid these.
488 
489  for(std::string::const_iterator
490  it=s.begin();
491  it!=s.end();
492  ++it)
493  {
494  char ch=*it;
495 
496  if(isalnum(ch) || ch=='_')
497  dest+=ch;
498  else if(ch==':')
499  {
500  std::string::const_iterator next_it(it);
501  ++next_it;
502  if(next_it!=s.end() && *next_it==':')
503  {
504  dest.append(".S");
505  it=next_it;
506  }
507  else
508  dest+=".C";
509  }
510  else if(ch=='#')
511  dest+=".H";
512  else if(ch=='$')
513  dest+=".D";
514  else if(ch=='!')
515  dest+=".E";
516  else if(ch=='.')
517  dest+="..";
518  else if(ch=='%')
519  dest+=".P";
520  else
521  {
522  dest+='.';
523  dest.append(std::to_string(ch));
524  dest+='.';
525  }
526  }
527 
528  return dest;
529 }
530 
531 void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv)
532 {
533  if(expr.id()==ID_symbol)
534  {
535  const typet &type=expr.type();
536 
538  assert(id!="");
539 
540  // boolean symbols may have to be converted
541  from_bool_begin(type, bool_as_bv);
542 
543  out << convert_identifier(id);
544 
545  from_bool_end(type, bool_as_bv);
546  }
547  else if(expr.id()==ID_nondet_symbol)
548  {
549  const typet &type=expr.type();
550 
551  irep_idt id=expr.get(ID_identifier);
552  assert(id!="");
553 
554  // boolean symbols may have to be converted
555  from_bool_begin(type, bool_as_bv);
556 
557  out << "nondet_" << convert_identifier(id);
558 
559  from_bool_end(type, bool_as_bv);
560  }
561  else if(expr.id()==ID_literal)
562  {
563  convert_literal(to_literal_expr(expr).get_literal());
564  }
565  else if(expr.id()==ID_typecast)
566  {
567  convert_typecast(to_typecast_expr(expr), bool_as_bv);
568  }
569  else if(expr.id()==ID_struct)
570  {
571  convert_struct(expr);
572  }
573  else if(expr.id()==ID_union)
574  {
575  convert_union(expr);
576  }
577  else if(expr.id()==ID_constant)
578  {
579  convert_constant(to_constant_expr(expr), bool_as_bv);
580  }
581  else if(expr.id()==ID_concatenation)
582  convert_nary(expr, "concat", true);
583  else if(expr.id()==ID_bitand)
584  convert_nary(expr, "bvand", true);
585  else if(expr.id()==ID_bitor)
586  convert_nary(expr, "bvor", true);
587  else if(expr.id()==ID_bitxor)
588  convert_nary(expr, "bvxor", true);
589  else if(expr.id()==ID_bitnand)
590  convert_nary(expr, "bvnand", true);
591  else if(expr.id()==ID_bitnor)
592  convert_nary(expr, "bvnor", true);
593  else if(expr.id()==ID_bitnot)
594  {
595  assert(expr.operands().size()==1);
596  out << "(bvnot ";
597  convert_expr(expr.op0(), true);
598  out << ")";
599  }
600  else if(expr.id()==ID_unary_minus)
601  {
602  const typet &type=expr.type();
603 
604  assert(expr.operands().size()==1);
605 
606  if(type.id()==ID_rational)
607  {
608  out << "(- ";
609  convert_expr(expr.op0(), true);
610  out << ")";
611  }
612  else if(type.id()==ID_integer)
613  {
614  out << "(~ ";
615  convert_expr(expr.op0(), true);
616  out << ")";
617  }
618  else
619  {
620  out << "(bvneg ";
621  convert_expr(expr.op0(), true);
622  out << ")";
623  }
624  }
625  else if(expr.id()==ID_if)
626  {
627  assert(expr.operands().size()==3);
628 
629  // The SMTLIB standard requires a different operator in a boolean context
630  if(expr.op1().type().id()==ID_bool && !bool_as_bv)
631  out << "(if_then_else ";
632  else
633  out << "(ite ";
634 
635  convert_expr(expr.op0(), false);
636  out << " ";
637  convert_expr(expr.op1(), bool_as_bv);
638  out << " ";
639  convert_expr(expr.op2(), bool_as_bv);
640  out << ")";
641  }
642  else if(expr.id()==ID_and ||
643  expr.id()==ID_or ||
644  expr.id()==ID_xor)
645  {
646  const typet &type=expr.type();
647  const exprt::operandst &operands=expr.operands();
648 
649  assert(type.id()==ID_bool);
650  assert(operands.size()>=2);
651 
652  // this may have to be converted
653  from_bool_begin(type, bool_as_bv);
654 
655  out << "(" << expr.id();
656  forall_expr(it, operands)
657  {
658  out << " ";
659  convert_expr(*it, false);
660  }
661  out << ")";
662 
663  // this may have to be converted
664  from_bool_end(type, bool_as_bv);
665  }
666  else if(expr.id()==ID_implies)
667  {
668  const typet &type=expr.type();
669 
670  assert(type.id()==ID_bool);
671  assert(expr.operands().size()==2);
672 
673  // this may have to be converted
674  from_bool_begin(type, bool_as_bv);
675 
676  out << "(implies ";
677  convert_expr(expr.op0(), false);
678  out << " ";
679  convert_expr(expr.op1(), false);
680  out << ")";
681 
682  // this may have to be converted
683  from_bool_end(type, bool_as_bv);
684  }
685  else if(expr.id()==ID_not)
686  {
687  const typet &type=expr.type();
688 
689  assert(expr.operands().size()==1);
690 
691  // this may have to be converted
692  from_bool_begin(type, bool_as_bv);
693 
694  out << "(not ";
695  convert_expr(expr.op0(), false);
696  out << ")";
697 
698  // this may have to be converted
699  from_bool_end(type, bool_as_bv);
700  }
701  else if(expr.id()==ID_equal ||
702  expr.id()==ID_notequal)
703  {
704  const typet &type=expr.type();
705 
706  assert(expr.operands().size()==2);
707  assert(base_type_eq(expr.op0().type(), expr.op1().type(), ns));
708 
709  // this may have to be converted
710  from_bool_begin(type, bool_as_bv);
711 
712  if(expr.op0().type().id()==ID_bool)
713  {
714  if(expr.id()==ID_notequal)
715  out << "(xor ";
716  else
717  out << "(iff ";
718 
719  convert_expr(expr.op0(), false);
720  out << " ";
721  convert_expr(expr.op1(), false);
722  out << ")";
723  }
724  else
725  {
726  if(expr.id()==ID_notequal)
727  {
728  out << "(not (= ";
729  convert_expr(expr.op0(), true);
730  out << " ";
731  convert_expr(expr.op1(), true);
732  out << "))";
733  }
734  else
735  {
736  out << "(= ";
737  convert_expr(expr.op0(), true);
738  out << " ";
739  convert_expr(expr.op1(), true);
740  out << ")";
741  }
742  }
743 
744  // this may have to be converted
745  from_bool_end(type, bool_as_bv);
746  }
747  else if(expr.id()==ID_le ||
748  expr.id()==ID_lt ||
749  expr.id()==ID_ge ||
750  expr.id()==ID_gt)
751  {
752  convert_relation(expr, bool_as_bv);
753  }
754  else if(expr.id()==ID_plus)
755  {
756  convert_plus(to_plus_expr(expr));
757  }
758  else if(expr.id()==ID_floatbv_plus)
759  {
760  convert_floatbv_plus(expr);
761  }
762  else if(expr.id()==ID_minus)
763  {
765  }
766  else if(expr.id()==ID_floatbv_minus)
767  {
768  convert_floatbv_minus(expr);
769  }
770  else if(expr.id()==ID_div)
771  {
772  convert_div(to_div_expr(expr));
773  }
774  else if(expr.id()==ID_floatbv_div)
775  {
776  convert_floatbv_div(expr);
777  }
778  else if(expr.id()==ID_mod)
779  {
780  convert_mod(to_mod_expr(expr));
781  }
782  else if(expr.id()==ID_mult)
783  {
784  convert_mult(to_mult_expr(expr));
785  }
786  else if(expr.id()==ID_floatbv_mult)
787  {
788  convert_floatbv_mult(expr);
789  }
790  else if(expr.id()==ID_address_of)
791  {
792  const typet &type=expr.type();
793 
794  assert(expr.operands().size()==1);
795  assert(type.id()==ID_pointer);
797  }
798  else if(expr.id()=="implicit_address_of" ||
799  expr.id()=="reference_to")
800  {
801  // old stuff
802  assert(false);
803  }
804  else if(expr.id()==ID_array_of)
805  {
806  assert(expr.type().id()==ID_array);
807  assert(expr.operands().size()==1);
808 
809  // const array_typet &array_type=to_array_type(expr.type());
810 
811  // not really there in SMT, so we replace it
812  // this is an over-approximation
813  array_of_mapt::const_iterator it=array_of_map.find(expr);
814  assert(it!=array_of_map.end());
815 
816  out << it->second;
817  }
818  else if(expr.id()==ID_index)
819  {
820  convert_index(to_index_expr(expr), bool_as_bv);
821  }
822  else if(expr.id()==ID_ashr ||
823  expr.id()==ID_lshr ||
824  expr.id()==ID_shl)
825  {
826  const typet &type=expr.type();
827 
828  assert(expr.operands().size()==2);
829 
830  if(type.id()==ID_unsignedbv ||
831  type.id()==ID_signedbv ||
832  type.id()==ID_bv ||
833  type.id()==ID_struct ||
834  type.id()==ID_union)
835  {
836  if(expr.id()==ID_ashr)
837  out << "(bvashr ";
838  else if(expr.id()==ID_lshr)
839  out << "(bvlshr ";
840  else if(expr.id()==ID_shl)
841  out << "(bvshl ";
842  else
843  assert(false);
844 
845  convert_expr(expr.op0(), true);
846  out << " ";
847 
848  // SMT1 requires the shift distance to have the same width as
849  // the value that is shifted -- odd!
850 
851  std::size_t width_op0=boolbv_width(expr.op0().type());
852  std::size_t width_op1=boolbv_width(expr.op1().type());
853 
854  if(width_op0==width_op1)
855  convert_expr(expr.op1(), true);
856  else if(width_op0>width_op1)
857  {
858  out << "(zero_extend[" << width_op0-width_op1 << "] ";
859  convert_expr(expr.op1(), true);
860  out << ")"; // zero_extend
861  }
862  else // width_op0<width_op1
863  {
864  out << "(extract[" << width_op0-1 << ":0] ";
865  convert_expr(expr.op1(), true);
866  out << ")"; // extract
867  }
868 
869  out << ")";
870  }
871  else
872  throw "unsupported type for "+expr.id_string()+
873  ": "+type.id_string();
874  }
875  else if(expr.id()==ID_with)
876  {
877  convert_with(expr);
878  }
879  else if(expr.id()==ID_update)
880  {
881  convert_update(expr);
882  }
883  else if(expr.id()==ID_member)
884  {
885  convert_member(to_member_expr(expr), bool_as_bv);
886  }
887  else if(expr.id()==ID_pointer_offset)
888  {
889  assert(expr.operands().size()==1);
890  assert(expr.op0().type().id()==ID_pointer);
891  std::size_t op_width=boolbv_width(expr.op0().type());
892  out << "(zero_extend[" << BV_ADDR_BITS << "] (extract["
893  << (op_width-1-BV_ADDR_BITS)
894  << ":0] ";
895  convert_expr(expr.op0(), true);
896  out << "))";
897  assert(boolbv_width(expr.type())==op_width);
898  }
899  else if(expr.id()==ID_pointer_object)
900  {
901  assert(expr.operands().size()==1);
902  assert(expr.op0().type().id()==ID_pointer);
903  std::size_t op_width=boolbv_width(expr.op0().type());
904  signed int ext=boolbv_width(expr.type())-BV_ADDR_BITS;
905 
906  if(ext>0)
907  out << "(zero_extend[" << ext << "] ";
908 
909  out << "(extract["
910  << (op_width-1)
911  << ":"
912  << op_width-1-BV_ADDR_BITS << "] ";
913  convert_expr(expr.op0(), true);
914  out << ")";
915 
916  if(ext>0)
917  out << ")";
918  }
919  else if(expr.id()=="is_dynamic_object")
920  {
921  convert_is_dynamic_object(expr, bool_as_bv);
922  }
923  else if(expr.id()==ID_invalid_pointer)
924  {
925  const typet &type=expr.type();
926 
927  assert(expr.operands().size()==1);
928  assert(expr.op0().type().id()==ID_pointer);
929  std::size_t op_width=boolbv_width(expr.op0().type());
930 
931  // this may have to be converted
932  from_bool_begin(type, bool_as_bv);
933 
934  out << "(= (extract["
935  << (op_width-1)
936  << ":" << op_width-BV_ADDR_BITS << "] ";
937  convert_expr(expr.op0(), true);
938  out << ") bv" << pointer_logic.get_invalid_object()
939  << "[" << BV_ADDR_BITS << "])";
940 
941  // this may have to be converted
942  from_bool_end(type, bool_as_bv);
943  }
944  else if(expr.id()=="pointer_object_has_type")
945  {
946  const typet &type=expr.type();
947 
948  assert(expr.operands().size()==1);
949 
950  // this may have to be converted
951  from_bool_begin(type, bool_as_bv);
952 
953  out << "false"; // TODO
954 
955  // this may have to be converted
956  from_bool_end(type, bool_as_bv);
957  }
958  else if(expr.id()==ID_string_constant)
959  {
960  exprt tmp;
961  string2array_mapt::const_iterator fit=string2array_map.find(expr);
962  assert(fit!=string2array_map.end());
963 
964  convert_expr(fit->second, true);
965  }
966  else if(expr.id()==ID_extractbit)
967  {
968  assert(expr.operands().size()==2);
969 
970  if(expr.op0().type().id()==ID_unsignedbv ||
971  expr.op0().type().id()==ID_signedbv)
972  {
973  const typet &type=expr.type();
974 
975  // this may have to be converted
976  from_bv_begin(type, bool_as_bv);
977 
978  if(expr.op1().is_constant())
979  {
980  mp_integer i;
981  if(to_integer(expr.op1(), i))
982  throw "extractbit: to_integer failed";
983 
984  out << "(extract[" << i << ":" << i << "] ";
985  convert_expr(expr.op0(), true);
986  out << ")";
987  }
988  else
989  {
990  out << "(extract[0:0] ";
991  // the arguments of the shift need to have the same width
992  out << "(bvlshr ";
993  convert_expr(expr.op0(), true);
994  typecast_exprt tmp(expr.op0().type());
995  tmp.op0()=expr.op1();
996  convert_expr(tmp, true);
997  out << "))"; // bvlshr, extract
998  }
999 
1000  // this may have to be converted
1001  from_bv_end(type, bool_as_bv);
1002  }
1003  else
1004  throw "unsupported type for "+expr.id_string()+
1005  ": "+expr.op0().type().id_string();
1006  }
1007  else if(expr.id()==ID_replication)
1008  {
1009  assert(expr.operands().size()==2);
1010 
1011  mp_integer times;
1012  if(to_integer(expr.op0(), times))
1013  throw "replication takes constant as first parameter";
1014 
1015  out << "(repeat[" << times << "] ";
1016  convert_expr(expr.op1(), true); // this ensures we have a vector
1017  out << ")";
1018  }
1019  else if(expr.id()==ID_byte_extract_little_endian ||
1020  expr.id()==ID_byte_extract_big_endian)
1021  {
1022  convert_byte_extract(to_byte_extract_expr(expr), bool_as_bv);
1023  }
1024  else if(expr.id()==ID_byte_update_little_endian ||
1025  expr.id()==ID_byte_update_big_endian)
1026  {
1027  convert_byte_update(expr, bool_as_bv);
1028  }
1029  else if(expr.id()==ID_width)
1030  {
1031  std::size_t result_width=boolbv_width(expr.type());
1032 
1033  if(result_width==0)
1034  throw "conversion failed";
1035 
1036  if(expr.operands().size()!=1)
1037  throw "width expects 1 operand";
1038 
1039  std::size_t op_width=boolbv_width(expr.op0().type());
1040 
1041  if(op_width==0)
1042  throw "conversion failed";
1043 
1044  out << "bv" << op_width/8 << "[" << result_width << "]";
1045  }
1046  else if(expr.id()==ID_abs)
1047  {
1048  const typet &type=expr.type();
1049 
1050  assert(expr.operands().size()==1);
1051  const exprt &op0=expr.op0();
1052 
1053  std::size_t result_width=boolbv_width(type);
1054 
1055  if(result_width==0)
1056  throw "conversion failed";
1057 
1058  if(type.id()==ID_signedbv ||
1059  type.id()==ID_fixedbv)
1060  {
1061  out << "(ite (bvslt ";
1062  convert_expr(op0, true);
1063  out << " bv0[" << result_width << "]) ";
1064  out << "(bvneg ";
1065  convert_expr(op0, true);
1066  out << ") ";
1067  convert_expr(op0, true);
1068  out << ")";
1069  }
1070  else if(type.id()==ID_floatbv)
1071  {
1072  out << "(bvand ";
1073  convert_expr(op0, true);
1074  out << " bv"
1075  << (power(2, result_width-1)-1)
1076  << "[" << result_width << "])";
1077  }
1078  else
1079  throw "abs with unsupported operand type";
1080  }
1081  else if(expr.id()==ID_isnan)
1082  {
1083  const typet &type=expr.type();
1084 
1085  assert(expr.operands().size()==1);
1086 
1087  const typet &op_type=expr.op0().type();
1088 
1089  if(op_type.id()==ID_fixedbv)
1090  {
1091  from_bool_begin(type, bool_as_bv);
1092  out << "false";
1093  from_bool_end(type, bool_as_bv);
1094  }
1095  else
1096  throw "isnan with unsupported operand type";
1097  }
1098  else if(expr.id()==ID_isfinite)
1099  {
1100  const typet &type=expr.type();
1101 
1102  if(expr.operands().size()!=1)
1103  throw "isfinite expects one operand";
1104 
1105  const typet &op_type=expr.op0().type();
1106 
1107  if(op_type.id()==ID_fixedbv)
1108  {
1109  from_bool_begin(type, bool_as_bv);
1110  out << "true";
1111  from_bool_end(type, bool_as_bv);
1112  }
1113  else
1114  throw "isfinite with unsupported operand type";
1115  }
1116  else if(expr.id()==ID_isinf)
1117  {
1118  const typet &type=expr.type();
1119 
1120  if(expr.operands().size()!=1)
1121  throw "isinf expects one operand";
1122 
1123  const typet &op_type=expr.op0().type();
1124 
1125  if(op_type.id()==ID_fixedbv)
1126  {
1127  from_bool_begin(type, bool_as_bv);
1128  out << "false";
1129  from_bool_end(type, bool_as_bv);
1130  }
1131  else
1132  throw "isinf with unsupported operand type";
1133  }
1134  else if(expr.id()==ID_isnormal)
1135  {
1136  const typet &type=expr.type();
1137 
1138  if(expr.operands().size()!=1)
1139  throw "isnormal expects one operand";
1140 
1141  const typet &op_type=expr.op0().type();
1142 
1143  if(op_type.id()==ID_fixedbv)
1144  {
1145  from_bool_begin(type, bool_as_bv);
1146  out << "true";
1147  from_bool_end(type, bool_as_bv);
1148  }
1149  else
1150  throw "isnormal with unsupported operand type";
1151  }
1152  else if(expr.id()==ID_overflow_plus ||
1153  expr.id()==ID_overflow_minus)
1154  {
1155  const typet &type=expr.type();
1156 
1157  assert(expr.operands().size()==2);
1158  bool subtract=expr.id()==ID_overflow_minus;
1159 
1160  const typet &op_type=expr.op0().type();
1161 
1162  std::size_t width=boolbv_width(op_type);
1163 
1164  if(op_type.id()==ID_signedbv)
1165  {
1166  // an overflow occurs if the top two bits of the extended sum differ
1167 
1168  from_bool_begin(type, bool_as_bv);
1169  out << "(let (?sum (";
1170  out << (subtract?"bvsub":"bvadd");
1171  out << " (sign_extend[1] ";
1172  convert_expr(expr.op0(), true);
1173  out << ")";
1174  out << " (sign_extend[1] ";
1175  convert_expr(expr.op1(), true);
1176  out << "))) "; // sign_extend, bvadd/sub let2
1177  out << "(not (= "
1178  "(extract[" << width << ":" << width << "] ?sum) "
1179  "(extract[" << (width-1) << ":" << (width-1) << "] ?sum)";
1180  out << ")))"; // =, not, let
1181  from_bool_end(type, bool_as_bv);
1182  }
1183  else if(op_type.id()==ID_unsignedbv)
1184  {
1185  // overflow is simply carry-out
1186  from_bv_begin(type, bool_as_bv);
1187  out << "(extract[" << width << ":" << width << "] ";
1188  out << "(" << (subtract?"bvsub":"bvadd");
1189  out << " (zero_extend[1] ";
1190  convert_expr(expr.op0(), true);
1191  out << ")";
1192  out << " (zero_extend[1] ";
1193  convert_expr(expr.op1(), true);
1194  out << ")))"; // zero_extend, bvsub/bvadd, extract
1195  from_bv_end(type, bool_as_bv);
1196  }
1197  else
1198  throw "overflow check on unknown type: "+op_type.id_string();
1199  }
1200  else if(expr.id()==ID_overflow_mult)
1201  {
1202  assert(expr.operands().size()==2);
1203 
1204  // No better idea than to multiply with double the bits and then compare
1205  // with max value.
1206 
1207  const typet &op_type=expr.op0().type();
1208  std::size_t width=boolbv_width(op_type);
1209 
1210  if(op_type.id()==ID_signedbv)
1211  {
1212  out << "(let (?prod (bvmul (sign_extend[" << width << "] ";
1213  convert_expr(expr.op0(), true);
1214  out << ") (sign_extend[" << width << "] ";
1215  convert_expr(expr.op1(), true);
1216  out << "))) "; // sign_extend, bvmul, ?prod
1217  out << "(or (bvsge ?prod (bv" << power(2, width-1)
1218  << "[" << width*2 << "]))";
1219  out << " (bvslt ?prod (bvneg (bv" << power(2, width-1)
1220  << "[" << width*2 << "])))";
1221  out << "))"; // or, let
1222  }
1223  else if(op_type.id()==ID_unsignedbv)
1224  {
1225  out << "(bvuge (bvmul (zero_extend[" << width << "] ";
1226  convert_expr(expr.op0(), true);
1227  out << ") (zero_extend[" << width << "] ";
1228  convert_expr(expr.op1(), true);
1229  out << ")) bv" << power(2, width) << "[" << width*2 << "])";
1230  }
1231  else
1232  throw "overflow-* check on unknown type: "+op_type.id_string();
1233  }
1234  else if(expr.id()==ID_forall || expr.id()==ID_exists)
1235  {
1236  from_bv_begin(expr.type(), bool_as_bv);
1237 
1238  assert(expr.operands().size()==2);
1239  out << "(" << expr.id() << " (";
1240  exprt bound=expr.op0();
1241  convert_expr(bound, false);
1242  out << " ";
1243 
1244  if(bound.type().id()==ID_bool)
1245  out << "Bool";
1246  else
1247  convert_type(bound.type());
1248 
1249  out << ") ";
1250  convert_expr(expr.op1(), false);
1251  out << ")";
1252 
1253  from_bv_end(expr.type(), bool_as_bv);
1254  }
1255  else if(expr.id()==ID_extractbits)
1256  {
1257  assert(expr.operands().size()==3);
1258 
1259  const typet &op_type=ns.follow(expr.op0().type());
1260 
1261  if(op_type.id()==ID_unsignedbv ||
1262  op_type.id()==ID_signedbv ||
1263  op_type.id()==ID_bv ||
1264  op_type.id()==ID_fixedbv ||
1265  op_type.id()==ID_struct ||
1266  op_type.id()==ID_union ||
1267  op_type.id()==ID_vector)
1268  {
1269  if(expr.op1().is_constant() &&
1270  expr.op2().is_constant())
1271  {
1272  mp_integer op1_i, op2_i;
1273 
1274  if(to_integer(expr.op1(), op1_i))
1275  throw "extractbits: to_integer failed";
1276 
1277  if(to_integer(expr.op2(), op2_i))
1278  throw "extractbits: to_integer failed";
1279 
1280  out << "(extract[" << op1_i << ":" << op2_i << "] ";
1281  convert_expr(expr.op0(), true);
1282  out << ")";
1283  }
1284  else
1285  {
1286  #if 0
1287  out << "(extract[";
1288  convert_expr(expr.op1(), bool_as_bv);
1289  out << ":";
1290  convert_expr(expr.op2(), bool_as_bv);
1291  out << "] ";
1292  convert_expr(expr.op0(), bool_as_bv);
1293  out << ")";
1294  #endif
1295  throw "smt1 todo: extractbits with variable bits";
1296  }
1297  }
1298  else
1299  throw "unsupported type for "+expr.id_string()+
1300  ": "+op_type.id_string();
1301  }
1302  else if(expr.id()==ID_array)
1303  {
1304  const exprt::operandst &operands=expr.operands();
1305 
1306  // array constructor
1307  array_expr_mapt::const_iterator it=array_expr_map.find(expr);
1308  assert(it!=array_expr_map.end());
1309 
1310  assert(!operands.empty());
1311 
1312  forall_expr(it, operands)
1313  out << "(store ";
1314 
1315  out << it->second;
1316 
1317  std::size_t i=0;
1318  forall_expr(it, operands)
1319  {
1321  out << " ";
1322  convert_expr(index, true);
1323  out << " ";
1324  convert_expr(*it, true);
1325  out << ")";
1326  i++;
1327  }
1328  }
1329  else if(expr.id()==ID_vector)
1330  {
1331  // Vector constructor.
1332  // We flatten the vector by concatenating its elements.
1333  convert_nary(expr, "concat", bool_as_bv);
1334  }
1335  else
1336  throw "smt1_convt::convert_expr: `"+
1337  expr.id_string()+"' is unsupported";
1338 }
1339 
1341  const typecast_exprt &expr,
1342  bool bool_as_bv)
1343 {
1344  assert(expr.operands().size()==1);
1345  const exprt &src=expr.op0();
1346 
1347  typet dest_type=ns.follow(expr.type());
1348  if(dest_type.id()==ID_c_enum_tag)
1349  dest_type=ns.follow_tag(to_c_enum_tag_type(dest_type));
1350 
1351  typet src_type=ns.follow(src.type());
1352  if(src_type.id()==ID_c_enum_tag)
1353  src_type=ns.follow_tag(to_c_enum_tag_type(src_type));
1354 
1355  if(dest_type.id()==ID_bool)
1356  {
1357  // boolean typecasts may have to be converted
1358  from_bool_begin(dest_type, bool_as_bv);
1359 
1360  // this is comparison with zero
1361  if(src_type.id()==ID_signedbv ||
1362  src_type.id()==ID_unsignedbv ||
1363  src_type.id()==ID_fixedbv ||
1364  src_type.id()==ID_c_bit_field ||
1365  src_type.id()==ID_pointer)
1366  {
1367  out << "(not (= ";
1368  convert_expr(src, true);
1369  out << " ";
1370  convert_expr(
1371  from_integer(0, src_type),
1372  true);
1373  out << "))";
1374  }
1375  else
1376  {
1377  // NOLINTNEXTLINE(readability/throw)
1378  throw "TODO typecast1 "+src_type.id_string()+" -> bool";
1379  }
1380 
1381  // boolean typecasts may have to be converted
1382  from_bool_end(dest_type, bool_as_bv);
1383  }
1384  else if(dest_type.id()==ID_c_bool)
1385  {
1386  // this is comparison with zero
1387  if(src_type.id()==ID_signedbv ||
1388  src_type.id()==ID_unsignedbv ||
1389  src_type.id()==ID_fixedbv ||
1390  src_type.id()==ID_c_bit_field ||
1391  src_type.id()==ID_pointer)
1392  {
1393  std::size_t to_width=boolbv_width(dest_type);
1394 
1395  out << "(ite ";
1396  out << "(not (= ";
1397  convert_expr(src, true);
1398  out << " ";
1399  convert_expr(
1400  from_integer(0, src_type),
1401  true);
1402  out << ")) "; // not, =
1403  out << " bv1[" << to_width << "]";
1404  out << " bv0[" << to_width << "]";
1405  out << ")"; // ite
1406  }
1407  else
1408  {
1409  // NOLINTNEXTLINE(readability/throw)
1410  throw "TODO typecast1 "+src_type.id_string()+" -> bool";
1411  }
1412  }
1413  else if(dest_type.id()==ID_signedbv ||
1414  dest_type.id()==ID_unsignedbv ||
1415  dest_type.id()==ID_c_enum)
1416  {
1417  std::size_t to_width=boolbv_width(dest_type);
1418 
1419  if(src_type.id()==ID_signedbv || // from signedbv
1420  src_type.id()==ID_unsignedbv || // from unsigedbv
1421  src_type.id()==ID_c_bool ||
1422  src_type.id()==ID_c_enum)
1423  {
1424  std::size_t from_width=boolbv_width(src_type);
1425 
1426  if(from_width==to_width)
1427  convert_expr(src, true); // ignore
1428  else if(from_width<to_width) // extend
1429  {
1430  if(src_type.id()==ID_signedbv)
1431  out << "(sign_extend[";
1432  else
1433  out << "(zero_extend[";
1434 
1435  out << (to_width-from_width)
1436  << "] ";
1437  convert_expr(src, true);
1438  out << ")";
1439  }
1440  else // chop off extra bits
1441  {
1442  out << "(extract[" << (to_width-1) << ":0] ";
1443  convert_expr(src, true);
1444  out << ")";
1445  }
1446  }
1447  else if(src_type.id()==ID_fixedbv) // from fixedbv to integer
1448  {
1449  const fixedbv_typet &fixedbv_src_type=to_fixedbv_type(src_type);
1450 
1451  std::size_t from_width=fixedbv_src_type.get_width();
1452  std::size_t from_integer_bits=fixedbv_src_type.get_integer_bits();
1453  std::size_t from_fraction_bits=fixedbv_src_type.get_fraction_bits();
1454 
1455  if(to_width>from_integer_bits)
1456  {
1457  out << "(sign_extend[" << (to_width-from_integer_bits) << "] ";
1458  out << "(extract[" << (from_width-1) << ":"
1459  << from_fraction_bits << "] ";
1460  convert_expr(src, true);
1461  out << "))";
1462  }
1463  else
1464  {
1465  out << "(extract[" << (from_fraction_bits+to_width-1)
1466  << ":" << from_fraction_bits << "] ";
1467  convert_expr(src, true);
1468  out << ")";
1469  }
1470  }
1471  else if(src_type.id()==ID_bool) // from boolean
1472  {
1473  out << "(ite ";
1474  convert_expr(src, false);
1475 
1476  if(dest_type.id()==ID_fixedbv)
1477  {
1478  fixedbv_spect spec(to_fixedbv_type(expr.type()));
1479  out << " (concat bv1[" << spec.integer_bits << "] " <<
1480  "bv0[" << spec.get_fraction_bits() << "]) " <<
1481  "bv0[" << spec.width << "]";
1482  }
1483  else
1484  {
1485  out << " bv1[" << to_width << "]";
1486  out << " bv0[" << to_width << "]";
1487  }
1488 
1489  out << ")";
1490  }
1491  else if(src_type.id()==ID_pointer) // from pointer to int
1492  {
1493  std::size_t from_width=boolbv_width(src_type);
1494 
1495  if(from_width<to_width) // extend
1496  {
1497  out << "(zero_extend[";
1498  out << (to_width-from_width)
1499  << "] ";
1500  convert_expr(src, true);
1501  out << ")";
1502  }
1503  else // chop off extra bits
1504  {
1505  out << "(extract[" << (to_width-1) << ":0] ";
1506  convert_expr(src, true);
1507  out << ")";
1508  }
1509  }
1510  else if(src_type.id()==ID_integer) // from integer to bit-vector
1511  {
1512  // must be constant
1513  if(src.is_constant())
1514  {
1515  mp_integer i;
1516  to_integer(src, i);
1517  out << "bv" << i << "[" << to_width << "]";
1518  }
1519  else
1520  throw "can't convert non-constant integer to bitvector";
1521  }
1522  else if(src_type.id()==ID_c_bit_field)
1523  {
1524  std::size_t from_width=boolbv_width(src_type);
1525 
1526  if(from_width==to_width)
1527  convert_expr(src, bool_as_bv); // ignore
1528  else
1529  {
1531  typecast_exprt tmp(typecast_exprt(src, t), dest_type);
1532  convert_typecast(tmp, bool_as_bv);
1533  }
1534  }
1535  else
1536  {
1537  // NOLINTNEXTLINE(readability/throw)
1538  throw "TODO typecast2 "+src_type.id_string()+
1539  " -> "+dest_type.id_string();
1540  }
1541  }
1542  else if(dest_type.id()==ID_fixedbv) // to fixedbv
1543  {
1544  const fixedbv_typet &fixedbv_type=to_fixedbv_type(dest_type);
1545  std::size_t to_fraction_bits=fixedbv_type.get_fraction_bits();
1546  std::size_t to_integer_bits=fixedbv_type.get_integer_bits();
1547 
1548  if(src_type.id()==ID_unsignedbv ||
1549  src_type.id()==ID_signedbv ||
1550  src_type.id()==ID_c_enum)
1551  {
1552  // integer to fixedbv
1553  std::size_t from_width=to_bitvector_type(src_type).get_width();
1554 
1555  // we just concatenate a zero-valued fractional part
1556  out << "(concat";
1557 
1558  if(from_width==to_integer_bits)
1559  convert_expr(src, true);
1560  else if(from_width>to_integer_bits)
1561  {
1562  // too many integer bits, chop some off
1563  out << " (extract[" << (to_integer_bits-1) << ":0] ";
1564  convert_expr(src, true);
1565  out << ")";
1566  }
1567  else
1568  {
1569  // too few integer bits
1570  assert(from_width<to_integer_bits);
1571  if(dest_type.id()==ID_unsignedbv)
1572  {
1573  out << " (zero_extend["
1574  << (to_integer_bits-from_width) << "] ";
1575  convert_expr(src, true);
1576  out << ")";
1577  }
1578  else
1579  {
1580  out << " (sign_extend["
1581  << (to_integer_bits-from_width) << "] ";
1582  convert_expr(src, true);
1583  out << ")";
1584  }
1585  }
1586 
1587  out << " bv0[" << to_fraction_bits << "]";
1588  out << ")"; // concat
1589  }
1590  else if(src_type.id()==ID_bool)
1591  {
1592  // bool to fixedbv
1593  out << "(concat (concat bv0[" << (to_integer_bits-1) << "]"
1594  << " ";
1595  convert_expr(src, true); // this returns a 1-bit bit-vector
1596  out << ")"; // concat
1597  out << " bv0[" << to_fraction_bits << "]";
1598  out << ")"; // concat
1599  }
1600  else if(src_type.id()==ID_fixedbv)
1601  {
1602  // fixedbv to fixedbv
1603  const fixedbv_typet &from_fixedbv_type=to_fixedbv_type(src_type);
1604  std::size_t from_fraction_bits=from_fixedbv_type.get_fraction_bits();
1605  std::size_t from_integer_bits=from_fixedbv_type.get_integer_bits();
1606  std::size_t from_width=from_fixedbv_type.get_width();
1607 
1608  // let is only allowed in formulas...
1609  out << "(concat ";
1610 
1611  if(to_integer_bits<=from_integer_bits)
1612  {
1613  out << "(extract["
1614  << (from_fraction_bits+to_integer_bits-1) << ":"
1615  << from_fraction_bits
1616  << "] ";
1617  convert_expr(src, true);
1618  out << ")";
1619  }
1620  else
1621  {
1622  assert(to_integer_bits>from_integer_bits);
1623  out << "(sign_extend["
1624  << (to_integer_bits-from_integer_bits)
1625  << "] (extract["
1626  << (from_width-1) << ":"
1627  << from_fraction_bits
1628  << "] ";
1629  convert_expr(src, true);
1630  out << "))";
1631  }
1632 
1633  out << " ";
1634 
1635  if(to_fraction_bits<=from_fraction_bits)
1636  {
1637  out << "(extract["
1638  << (from_fraction_bits-1) << ":"
1639  << (from_fraction_bits-to_fraction_bits)
1640  << "] ";
1641  convert_expr(src, true);
1642  out << ")";
1643  }
1644  else
1645  {
1646  assert(to_fraction_bits>from_fraction_bits);
1647  out << "(concat (extract["
1648  << (from_fraction_bits-1) << ":0] ";
1649  convert_expr(src, true);
1650  out << ")"
1651  << " bv0[" << to_fraction_bits-from_fraction_bits
1652  << "])";
1653  }
1654 
1655  out << ")"; // concat
1656  }
1657  else
1658  throw "unexpected typecast to fixedbv";
1659  }
1660  else if(dest_type.id()==ID_pointer)
1661  {
1662  std::size_t to_width=boolbv_width(dest_type);
1663 
1664  if(src_type.id()==ID_pointer)
1665  {
1666  // this just passes through
1667  convert_expr(src, true);
1668  }
1669  else if(src_type.id()==ID_unsignedbv ||
1670  src_type.id()==ID_signedbv)
1671  {
1672  std::size_t from_width=boolbv_width(src_type);
1673 
1674  if(from_width==to_width)
1675  convert_expr(src, true); // pass through
1676  else if(from_width<to_width)
1677  {
1678  out << "(zero_extend["
1679  << (to_width-from_width)
1680  << "] ";
1681  convert_expr(src, true);
1682  out << ")"; // zero_extend
1683  }
1684  else // from_width>to_width
1685  {
1686  out << "(extract["
1687  << to_width
1688  << ":0] ";
1689  convert_expr(src, true);
1690  out << ")"; // extract
1691  }
1692  }
1693  else
1694  // NOLINTNEXTLINE(readability/throw)
1695  throw "TODO typecast3 "+src_type.id_string()+" -> pointer";
1696  }
1697  else if(dest_type.id()==ID_range)
1698  {
1699  // NOLINTNEXTLINE(readability/throw)
1700  throw "TODO range typecast";
1701  }
1702  else if(dest_type.id()==ID_c_bit_field)
1703  {
1704  std::size_t from_width=boolbv_width(src_type);
1705  std::size_t to_width=boolbv_width(dest_type);
1706 
1707  if(from_width==to_width)
1708  convert_expr(src, bool_as_bv); // ignore
1709  else
1710  {
1712  typecast_exprt tmp(typecast_exprt(src, t), dest_type);
1713  convert_typecast(tmp, bool_as_bv);
1714  }
1715  }
1716  else
1717  // NOLINTNEXTLINE(readability/throw)
1718  throw "TODO typecast4 ? -> "+dest_type.id_string();
1719 }
1720 
1722 {
1723  const struct_typet &struct_type=to_struct_type(expr.type());
1724 
1725  const struct_typet::componentst &components=
1726  struct_type.components();
1727 
1728  assert(components.size()==expr.operands().size());
1729 
1730  assert(!components.empty());
1731 
1732  if(components.size()==1)
1733  {
1734  const exprt &op=expr.op0();
1735 
1736  if(op.type().id()==ID_array)
1737  flatten_array(op);
1738  else
1739  convert_expr(op, true);
1740  }
1741  else
1742  {
1743  std::size_t nr_ops=0;
1744 
1745  for(std::size_t i=0; i<components.size(); i++)
1746  if(expr.operands()[i].type().id()!=ID_code)
1747  nr_ops++;
1748 
1749  for(std::size_t i=1; i<nr_ops; i++) // one less
1750  out << "(concat ";
1751 
1752  bool first=true;
1753  for(std::size_t i=0; i<components.size(); i++)
1754  {
1755  const exprt &op=expr.operands()[i];
1756 
1757  if(op.type().id()!=ID_code)
1758  {
1759  if(!first)
1760  out << " ";
1761 
1762  if(op.type().id()==ID_array)
1763  flatten_array(op);
1764  else
1765  convert_expr(op, true);
1766 
1767  if(!first)
1768  out << ")"; // concat
1769  first=false;
1770  }
1771  }
1772  }
1773 }
1774 
1776 {
1777  const union_typet &union_type=to_union_type(expr.type());
1778 
1779  assert(expr.operands().size()==1);
1780  const exprt &op=expr.op0();
1781 
1782  std::size_t total_width=boolbv_width(union_type);
1783  std::size_t member_width=boolbv_width(op.type());
1784 
1785  if(total_width==0)
1786  throw "failed to get union width for union";
1787 
1788  if(member_width==0)
1789  throw "failed to get union member width for union";
1790 
1791  if(total_width==member_width)
1792  convert_expr(op, true);
1793  else
1794  {
1795  // we will pad with zeros, but non-det would be better
1796  assert(total_width>member_width);
1797  out << "(concat ";
1798  out << "bv0[" << (total_width-member_width) << "] ";
1799  convert_expr(op, true);
1800  out << ")";
1801  }
1802 }
1803 
1805  const constant_exprt &expr,
1806  bool bool_as_bv)
1807 {
1808  if(expr.type().id()==ID_unsignedbv ||
1809  expr.type().id()==ID_signedbv ||
1810  expr.type().id()==ID_bv ||
1811  expr.type().id()==ID_c_enum ||
1812  expr.type().id()==ID_c_enum_tag ||
1813  expr.type().id()==ID_c_bool ||
1814  expr.type().id()==ID_c_bit_field)
1815  {
1816  mp_integer value;
1817 
1818  if(to_integer(expr, value))
1819  throw "failed to convert bitvector constant";
1820 
1821  std::size_t width=boolbv_width(expr.type());
1822 
1823  if(value<0)
1824  value=power(2, width)+value;
1825 
1826  out << "bv" << value
1827  << "[" << width << "]";
1828  }
1829  else if(expr.type().id()==ID_fixedbv)
1830  {
1831  fixedbv_spect spec(to_fixedbv_type(expr.type()));
1832 
1833  std::string v_str=expr.get_string(ID_value);
1834  mp_integer v=binary2integer(v_str, false);
1835 
1836  out << "bv" << v << "[" << spec.width << "]";
1837  }
1838  else if(expr.type().id()==ID_floatbv)
1839  {
1840  ieee_float_spect spec(to_floatbv_type(expr.type()));
1841 
1842  std::string v_str=expr.get_string(ID_value);
1843  mp_integer v=binary2integer(v_str, false);
1844 
1845  out << "bv" << v << "[" << spec.width() << "]";
1846  }
1847  else if(expr.type().id()==ID_pointer)
1848  {
1849  const irep_idt &value=expr.get(ID_value);
1850 
1851  if(value==ID_NULL)
1852  {
1853  assert(boolbv_width(expr.type())!=0);
1854  out << "(concat"
1855  << " bv" << pointer_logic.get_null_object()
1856  << "[" << BV_ADDR_BITS << "]"
1857  << " bv0[" << boolbv_width(expr.type())-BV_ADDR_BITS
1858  << "]"
1859  << ")"; // concat
1860  }
1861  else
1862  throw "unknown pointer constant: "+id2string(value);
1863  }
1864  else if(expr.type().id()==ID_bool)
1865  {
1866  if(expr.is_true())
1867  out << (bool_as_bv?"bit1":"true");
1868  else if(expr.is_false())
1869  out << (bool_as_bv?"bit0":"false");
1870  else
1871  throw "unknown boolean constant";
1872  }
1873  else if(expr.type().id()==ID_array)
1874  {
1875  // this should be the 'array' expression
1876  assert(false);
1877  }
1878  else if(expr.type().id()==ID_rational)
1879  {
1880  std::string value=expr.get_string(ID_value);
1881  size_t pos=value.find("/");
1882 
1883  if(pos==std::string::npos)
1884  out << value << ".0";
1885  else
1886  {
1887  out << "(/ " << value.substr(0, pos) << ".0 "
1888  << value.substr(pos+1) << ".0)";
1889  }
1890  }
1891  else if(expr.type().id()==ID_integer ||
1892  expr.type().id()==ID_natural)
1893  {
1894  std::string value=expr.get_string(ID_value);
1895 
1896  if(value[0]=='-')
1897  out << "(~ " << value.substr(1) << ")";
1898  else
1899  out << value;
1900  }
1901  else
1902  throw "unknown constant: "+expr.type().id_string();
1903 }
1904 
1906 {
1907  assert(expr.operands().size()==2);
1908 
1909  if(expr.type().id()==ID_unsignedbv ||
1910  expr.type().id()==ID_signedbv)
1911  {
1912  if(expr.type().id()==ID_unsignedbv)
1913  out << "(bvurem ";
1914  else
1915  out << "(bvsrem ";
1916 
1917  convert_expr(expr.op0(), true);
1918  out << " ";
1919  convert_expr(expr.op1(), true);
1920  out << ")";
1921  }
1922  else
1923  throw "unsupported type for mod: "+expr.type().id_string();
1924 }
1925 
1927  const exprt &expr,
1928  bool bool_as_bv)
1929 {
1930  std::vector<std::size_t> dynamic_objects;
1931  pointer_logic.get_dynamic_objects(dynamic_objects);
1932 
1933  assert(expr.operands().size()==1);
1934  assert(expr.op0().type().id()==ID_pointer);
1935  std::size_t op_width=boolbv_width(expr.op0().type());
1936 
1937  // this may have to be converted
1938  from_bool_begin(expr.type(), bool_as_bv);
1939 
1940  if(dynamic_objects.empty())
1941  out << "false";
1942  else
1943  {
1944  // let is only allowed in formulas
1945 
1946  out << "(let (?obj (extract["
1947  << (op_width-1)
1948  << ":" << op_width-BV_ADDR_BITS << "] ";
1949  convert_expr(expr.op0(), true);
1950  out << ")) ";
1951 
1952  if(dynamic_objects.size()==1)
1953  {
1954  out << "(= bv" << dynamic_objects.front()
1955  << "[" << BV_ADDR_BITS << "] ?obj)";
1956  }
1957  else
1958  {
1959  out << "(or";
1960 
1961  for(const auto &obj : dynamic_objects)
1962  out << " (= bv" << obj
1963  << "[" << BV_ADDR_BITS << "] ?obj)";
1964 
1965  out << ")"; // or
1966  }
1967 
1968  out << ")"; // let
1969  }
1970 
1971  // this may have to be converted
1972  from_bool_end(expr.type(), bool_as_bv);
1973 }
1974 
1975 void smt1_convt::convert_relation(const exprt &expr, bool bool_as_bv)
1976 {
1977  assert(expr.operands().size()==2);
1978 
1979  // this may have to be converted
1980  from_bool_begin(expr.type(), bool_as_bv);
1981 
1982  const typet &op_type=expr.op0().type();
1983 
1984  out << "(";
1985 
1986  if(op_type.id()==ID_unsignedbv ||
1987  op_type.id()==ID_pointer)
1988  {
1989  if(expr.id()==ID_le)
1990  out << "bvule";
1991  else if(expr.id()==ID_lt)
1992  out << "bvult";
1993  else if(expr.id()==ID_ge)
1994  out << "bvuge";
1995  else if(expr.id()==ID_gt)
1996  out << "bvugt";
1997 
1998  out << " ";
1999  convert_expr(expr.op0(), true);
2000  out << " ";
2001  convert_expr(expr.op1(), true);
2002  }
2003  else if(op_type.id()==ID_signedbv ||
2004  op_type.id()==ID_fixedbv)
2005  {
2006  if(expr.id()==ID_le)
2007  out << "bvsle";
2008  else if(expr.id()==ID_lt)
2009  out << "bvslt";
2010  else if(expr.id()==ID_ge)
2011  out << "bvsge";
2012  else if(expr.id()==ID_gt)
2013  out << "bvsgt";
2014 
2015  out << " ";
2016  convert_expr(expr.op0(), true);
2017  out << " ";
2018  convert_expr(expr.op1(), true);
2019  }
2020  else if(op_type.id()==ID_rational ||
2021  op_type.id()==ID_integer)
2022  {
2023  out << expr.id();
2024 
2025  out << " ";
2026  convert_expr(expr.op0(), true);
2027  out << " ";
2028  convert_expr(expr.op1(), true);
2029  }
2030  else
2031  throw "unsupported type for "+expr.id_string()+
2032  ": "+op_type.id_string();
2033 
2034  out << ")";
2035 
2036  // this may have to be converted
2037  from_bool_end(expr.type(), bool_as_bv);
2038 }
2039 
2041 {
2042  assert(expr.operands().size()>=2);
2043 
2044  if(expr.type().id()==ID_unsignedbv ||
2045  expr.type().id()==ID_signedbv ||
2046  expr.type().id()==ID_fixedbv)
2047  {
2048  convert_nary(expr, "bvadd", true);
2049  }
2050  else if(expr.type().id()==ID_pointer)
2051  {
2052  if(expr.operands().size()<2)
2053  throw "pointer arithmetic with less than two operands";
2054 
2055  if(expr.operands().size()==2)
2056  {
2057  exprt p=expr.op0(), i=expr.op1();
2058 
2059  if(p.type().id()!=ID_pointer)
2060  p.swap(i);
2061 
2062  if(p.type().id()!=ID_pointer)
2063  throw "unexpected mixture in pointer arithmetic";
2064 
2065  mp_integer element_size=
2066  pointer_offset_size(expr.type().subtype(), ns);
2067  assert(element_size>0);
2068 
2069  // adjust width if needed
2070  if(boolbv_width(i.type())!=boolbv_width(expr.type()))
2071  i.make_typecast(signedbv_typet(boolbv_width(expr.type())));
2072 
2073  out << "(bvadd ";
2074  convert_expr(p, true);
2075  out << " ";
2076 
2077  if(element_size>=2)
2078  {
2079  out << "(bvmul ";
2080  convert_expr(i, true);
2081  out << " bv" << element_size
2082  << "[" << boolbv_width(expr.type()) << "])";
2083  }
2084  else
2085  convert_expr(i, true);
2086 
2087  out << ")";
2088  }
2089  else
2090  {
2091  // more than two operands
2092  exprt p;
2093  typet integer_type=signedbv_typet(boolbv_width(expr.type()));
2094  exprt integer_sum(ID_plus, integer_type);
2095 
2096  forall_operands(it, expr)
2097  {
2098  if(it->type().id()==ID_pointer)
2099  p=*it;
2100  else
2101  integer_sum.copy_to_operands(*it);
2102  }
2103 
2104  Forall_operands(it, integer_sum)
2105  if(it->type()!=integer_type)
2106  it->make_typecast(integer_type);
2107 
2108  plus_exprt pointer_arithmetic(p, integer_sum, expr.type());
2109  convert_plus(pointer_arithmetic); // recursive call
2110  }
2111  }
2112  else if(expr.type().id()==ID_rational ||
2113  expr.type().id()==ID_integer)
2114  {
2115  convert_nary(expr, "+", true);
2116  }
2117  else
2118  throw "unsupported type for +: "+expr.type().id_string();
2119 }
2120 
2122 {
2123  assert(expr.operands().size()==3);
2124  assert(expr.type().id()==ID_floatbv);
2125 
2126  throw "todo: floatbv_plus";
2127 }
2128 
2130 {
2131  assert(expr.operands().size()==2);
2132 
2133  if(expr.type().id()==ID_unsignedbv ||
2134  expr.type().id()==ID_signedbv ||
2135  expr.type().id()==ID_fixedbv)
2136  {
2137  out << "(bvsub ";
2138 
2139  if(expr.op0().type().id()==ID_pointer)
2140  out << "(extract[" << boolbv_width(expr.op0().type())-1 << ":0] ";
2141  convert_expr(expr.op0(), true);
2142  if(expr.op0().type().id()==ID_pointer)
2143  out << ")";
2144 
2145  out << " ";
2146 
2147  if(expr.op1().type().id()==ID_pointer)
2148  out << "(extract[" << boolbv_width(expr.op1().type())-1 << ":0] ";
2149  convert_expr(expr.op1(), true);
2150  if(expr.op1().type().id()==ID_pointer)
2151  out << ")";
2152 
2153  out << ")";
2154  }
2155  else if(expr.type().id()==ID_pointer)
2156  {
2158  expr.op0(),
2159  "+",
2160  unary_minus_exprt(expr.op1(), expr.op1().type()),
2161  expr.type()),
2162  true);
2163  }
2164  else
2165  throw "unsupported type for -: "+expr.type().id_string();
2166 }
2167 
2169 {
2170  assert(expr.operands().size()==3);
2171  assert(expr.type().id()==ID_floatbv);
2172 
2173  throw "todo: floatbv_minus";
2174 }
2175 
2177 {
2178  assert(expr.operands().size()==2);
2179 
2180  if(expr.type().id()==ID_unsignedbv ||
2181  expr.type().id()==ID_signedbv)
2182  {
2183  if(expr.type().id()==ID_unsignedbv)
2184  out << "(bvudiv ";
2185  else
2186  out << "(bvsdiv ";
2187 
2188  convert_expr(expr.op0(), true);
2189  out << " ";
2190  convert_expr(expr.op1(), true);
2191  out << ")";
2192  }
2193  else if(expr.type().id()==ID_fixedbv)
2194  {
2195  fixedbv_spect spec(to_fixedbv_type(expr.type()));
2196  std::size_t fraction_bits=spec.get_fraction_bits();
2197 
2198  out << "(extract[" << spec.width-1 << ":0] ";
2199  out << "(bvsdiv ";
2200 
2201  out << "(concat ";
2202  convert_expr(expr.op0(), true);
2203  out << " bv0[" << fraction_bits << "]) ";
2204 
2205  out << "(sign_extend[" << fraction_bits << "] ";
2206  convert_expr(expr.op1(), true);
2207  out << ")";
2208 
2209  out << "))";
2210  }
2211  else
2212  throw "unsupported type for /: "+expr.type().id_string();
2213 }
2214 
2216 {
2217  assert(expr.operands().size()==3);
2218  assert(expr.type().id()==ID_floatbv);
2219 
2220  throw "todo: floatbv_div";
2221 }
2222 
2224 {
2225  assert(expr.operands().size()>=2);
2226 
2227  // re-write to binary if needed
2228  if(expr.operands().size()>2)
2229  {
2230  // strip last operand
2231  exprt tmp=expr;
2232  tmp.operands().pop_back();
2233 
2234  // recursive call
2235  return convert_mult(mult_exprt(tmp, expr.operands().back()));
2236  }
2237 
2238  assert(expr.operands().size()==2);
2239 
2240  if(expr.type().id()==ID_unsignedbv ||
2241  expr.type().id()==ID_signedbv)
2242  {
2243  // Note that bvmul is really unsigned,
2244  // but this is irrelevant as we chop-off any extra result
2245  // bits.
2246  out << "(bvmul ";
2247  convert_expr(expr.op0(), true);
2248  out << " ";
2249  convert_expr(expr.op1(), true);
2250  out << ")";
2251  }
2252  else if(expr.type().id()==ID_fixedbv)
2253  {
2254  fixedbv_spect spec(to_fixedbv_type(expr.type()));
2255  std::size_t fraction_bits=spec.get_fraction_bits();
2256 
2257  // strip away faction_bits off the result
2258  out << "(extract[" << spec.width+fraction_bits-1 << ":"
2259  << fraction_bits << "] ";
2260 
2261  out << "(bvmul ";
2262 
2263  out << "(sign_extend[" << fraction_bits << "] ";
2264  convert_expr(expr.op0(), true);
2265  out << ") ";
2266 
2267  out << "(sign_extend[" << fraction_bits << "] ";
2268  convert_expr(expr.op1(), true);
2269  out << ") ";
2270 
2271  out << ")"; // bvmul, fraction_bits+width wide
2272  out << ")"; // extract, width bits wide
2273  }
2274  else if(expr.type().id()==ID_rational)
2275  {
2276  out << "(* ";
2277  convert_expr(expr.op0(), true);
2278  out << " ";
2279  convert_expr(expr.op1(), true);
2280  out << ")";
2281  }
2282  else
2283  throw "unsupported type for *: "+expr.type().id_string();
2284 }
2285 
2287 {
2288  assert(expr.operands().size()==3);
2289  assert(expr.type().id()==ID_floatbv);
2290 
2291  throw "todo: floatbv_mult";
2292 }
2293 
2295 {
2296  // get rid of "with" that has more than three operands
2297 
2298  assert(expr.operands().size()>=3);
2299 
2300  if(expr.operands().size()>3)
2301  {
2302  std::size_t s=expr.operands().size();
2303 
2304  // strip of the trailing two operands
2305  exprt tmp=expr;
2306  tmp.operands().resize(s-2);
2307 
2308  with_exprt new_with_expr;
2309  assert(new_with_expr.operands().size()==3);
2310  new_with_expr.type()=expr.type();
2311  new_with_expr.old()=tmp;
2312  new_with_expr.where()=expr.operands()[s-2];
2313  new_with_expr.new_value()=expr.operands()[s-1];
2314 
2315  // recursive call
2316  return convert_with(new_with_expr);
2317  }
2318 
2319  const typet &expr_type=ns.follow(expr.type());
2320 
2321  if(expr_type.id()==ID_array)
2322  {
2323  const exprt &array=expr.op0();
2324 
2325  if(array.id()==ID_member)
2326  {
2327  // arrays in structs and unions are flattened!
2328 
2329  const typet &array_type=to_array_type(expr.type());
2330  const typet &elem_type=array_type.subtype();
2331 
2332  const member_exprt &member_expr=to_member_expr(array);
2333  const exprt &struct_op=member_expr.struct_op();
2334  const irep_idt &name=member_expr.get_component_name();
2335 
2336  const typet &struct_op_type=ns.follow(struct_op.type());
2337 
2338  std::size_t total_width=boolbv_width(struct_op_type);
2339 
2340  if(total_width==0)
2341  throw "failed to get struct width";
2342 
2343  std::size_t offset;
2344 
2345  if(struct_op_type.id()==ID_struct)
2346  offset=boolbv_width.get_member(
2347  to_struct_type(struct_op_type), name).offset;
2348  else if(struct_op_type.id()==ID_union)
2349  offset=0;
2350  else
2351  throw "failed to get offset";
2352 
2353  std::size_t width=boolbv_width(expr.type());
2354 
2355  if(width==0)
2356  throw "failed to get struct member width";
2357 
2358  std::size_t elem_width=boolbv_width(elem_type);
2359 
2360  if(elem_width==0)
2361  throw "failed to get struct width";
2362 
2363  std::size_t array_bits=(offset+width) - offset;
2364 
2365  assert(expr.operands().size()==3);
2366  const exprt &index=expr.operands()[1];
2367  const exprt &value=expr.operands()[2];
2368  typecast_exprt index_tc(index, array_index_type());
2369 
2370  out << "(bvor ";
2371  out << "(bvand ";
2372 
2373  // this gets us the array
2374  out << "(extract[" << offset+width-1 << ":" << offset << "] ";
2375  convert_expr(struct_op, true);
2376  out << ")";
2377 
2378  // the mask
2379  out << " (bvnot (bvshl";
2380 
2381  out << " (concat";
2382  out << " (repeat[" << array_bits-elem_width << "] bv0[1])";
2383  out << " (repeat[" << elem_width << "] bv1[1])";
2384  out << ")"; // concat
2385 
2386  // shift it to the index
2387  if(width>=array_index_bits)
2388  out << " (zero_extend[" << width-array_index_bits << "]";
2389  else
2390  out << " (extract[" << width-1 << ":0]";
2391  out << " (bvmul ";
2392  convert_expr(index_tc, true);
2393  out << " bv" << elem_width << "[" << array_index_bits << "]";
2394  out << "))))"; // bvmul, zero_extend, bvshl, bvneg
2395 
2396  out << ")"; // bvand
2397 
2398  // the new value
2399  out << " (bvshl (zero_extend[" << array_bits-elem_width << "] ";
2400  convert_expr(value, true);
2401 
2402  // shift it to the index
2403  out << ")";
2404  if(width>=array_index_bits)
2405  out << " (zero_extend[" << width-array_index_bits << "]";
2406  else
2407  out << " (extract[" << width-1 << ":0]";
2408  out << " (bvmul ";
2409  convert_expr(index_tc, true);
2410  out << " bv" << elem_width << "[" << array_index_bits << "]";
2411  out << ")))"; // bvmul, bvshl, ze
2412 
2413  out << ")"; // bvor
2414  }
2415  else if(array.id()==ID_index)
2416  {
2417  // arrays in structs are flattened!
2418 
2419  const typet &array_type=to_array_type(expr.type());
2420  const typet &elem_type=array_type.subtype();
2421 
2422  const index_exprt &index_expr=to_index_expr(array);
2423 
2424  std::size_t width=boolbv_width(expr.type());
2425 
2426  if(width==0)
2427  throw "failed to get width of 2nd dimension array";
2428 
2429  std::size_t elem_width=boolbv_width(elem_type);
2430 
2431  if(elem_width==0)
2432  throw "failed to get array element width";
2433 
2434  assert(expr.operands().size()==3);
2435  const exprt &index_2nd=expr.operands()[1];
2436  const exprt &value=expr.operands()[2];
2437  typecast_exprt index_tc(index_2nd, array_index_type());
2438 
2439  out << "(bvor ";
2440  out << "(bvand ";
2441 
2442  // this gets us the array
2443  convert_expr(index_expr, true);
2444 
2445  // the mask
2446  out << " (bvnot (bvshl";
2447 
2448  out << " (concat";
2449  out << " (repeat[" << width-elem_width << "] bv0[1])";
2450  out << " (repeat[" << elem_width << "] bv1[1])";
2451  out << ")"; // concat
2452 
2453  // shift it to the index
2454  if(width>=array_index_bits)
2455  out << " (zero_extend[" << width-array_index_bits << "]";
2456  else
2457  out << " (extract[" << width-1 << ":0]";
2458  out << " (bvmul ";
2459  convert_expr(index_tc, true);
2460  out << " bv" << elem_width << "[" << array_index_bits << "]";
2461  out << "))))"; // bvmul, zero_extend, bvshl, bvneg
2462 
2463  out << ")"; // bvand
2464 
2465  // the new value
2466  out << " (bvshl (zero_extend[" << width-elem_width << "] ";
2467  convert_expr(value, true);
2468  // shift it to the index
2469  out << ")";
2470  if(width>=array_index_bits)
2471  out << " (zero_extend[" << width-array_index_bits << "]";
2472  else
2473  out << " (extract[" << width-1 << ":0]";
2474  out << " (bvmul ";
2475  convert_expr(index_tc, true);
2476  out << " bv" << elem_width << "[" << array_index_bits << "]";
2477  out << ")))"; // bvmul, bvshl, ze
2478 
2479  out << ")"; // bvor
2480  }
2481  else
2482  {
2483  out << "(store ";
2484 
2485  convert_expr(expr.op0(), true);
2486 
2487  out << " ";
2488  array_index(expr.op1());
2489  out << " ";
2490 
2491  // Booleans are put as bv[1] into an array
2492  convert_expr(expr.op2(), true);
2493 
2494  out << ")";
2495  }
2496  }
2497  else if(expr_type.id()==ID_struct)
2498  {
2499  const struct_typet &struct_type=to_struct_type(expr_type);
2500 
2501  const exprt &index=expr.op1();
2502  const exprt &value=expr.op2();
2503 
2504  std::size_t total_width=boolbv_width(expr.type());
2505 
2506  if(total_width==0)
2507  throw "failed to get struct width for with";
2508 
2509  std::size_t width=boolbv_width(value.type());
2510 
2511  if(width==0)
2512  throw "failed to get member width for with";
2513 
2514  std::size_t offset=boolbv_width.get_member(
2515  struct_type, index.get(ID_component_name)).offset;
2516 
2517  if(total_width==width)
2518  convert_expr(value, true);
2519  else
2520  {
2521  if(offset+width!=total_width)
2522  {
2523  out << "(concat";
2524  out << " (extract[" << (total_width-1) << ":" << (offset+width) << "] ";
2525  convert_expr(expr.op0(), true);
2526  out << ")";
2527  }
2528 
2529  if(offset!=0)
2530  out << " (concat";
2531 
2532  out << " ";
2533  convert_expr(value, true);
2534 
2535  if(offset!=0)
2536  {
2537  out << " (extract[" << (offset-1) << ":0] ";
2538  convert_expr(expr.op0(), true);
2539  out << ")";
2540  out << ")"; // concat
2541  }
2542 
2543  if(offset+width!=total_width)
2544  out << ")"; // concat
2545  }
2546  }
2547  else if(expr_type.id()==ID_union)
2548  {
2549  const union_typet &union_type=to_union_type(expr_type);
2550 
2551  const exprt &value=expr.op2();
2552 
2553  std::size_t total_width=boolbv_width(union_type);
2554 
2555  if(total_width==0)
2556  throw "failed to get union width for with";
2557 
2558  std::size_t member_width=boolbv_width(value.type());
2559 
2560  if(member_width==0)
2561  throw "failed to get union member width for with";
2562 
2563  if(total_width==member_width)
2564  convert_expr(value, true);
2565  else
2566  {
2567  assert(total_width>member_width);
2568  out << "(concat ";
2569  out << "(extract["
2570  << (total_width-1)
2571  << ":" << member_width << "] ";
2572  convert_expr(expr.op0(), true);
2573  out << ") "; // extract
2574  convert_expr(value, true);
2575  out << ")"; // concat
2576  }
2577  }
2578  else if(expr_type.id()==ID_bv ||
2579  expr_type.id()==ID_unsignedbv ||
2580  expr_type.id()==ID_signedbv)
2581  {
2582  // Update bits in a bit-vector. We will use masking and shifts.
2583 
2584  std::size_t total_width=boolbv_width(expr_type);
2585 
2586  if(total_width==0)
2587  throw "failed to get total width";
2588 
2589  assert(expr.operands().size()==3);
2590  const exprt &index=expr.operands()[1];
2591  const exprt &value=expr.operands()[2];
2592 
2593  std::size_t value_width=boolbv_width(value.type());
2594 
2595  if(value_width==0)
2596  throw "failed to get value width";
2597 
2598  typecast_exprt index_tc(index, expr_type);
2599 
2600  out << "(bvor ";
2601  out << "(band ";
2602 
2603  // the mask to get rid of the old bits
2604  out << " (bvnot (bvshl";
2605 
2606  out << " (concat";
2607  out << " (repeat[" << total_width-value_width << "] bv0[1])";
2608  out << " (repeat[" << value_width << "] bv1[1])";
2609  out << ")"; // concat
2610 
2611  // shift it to the index
2612  convert_expr(index_tc, true);
2613  out << "))"; // bvshl, bvot
2614 
2615  out << ")"; // bvand
2616 
2617  // the new value
2618  out << " (bvshl ";
2619  convert_expr(value, true);
2620 
2621  // shift it to the index
2622  convert_expr(index_tc, true);
2623  out << ")"; // bvshl
2624 
2625  out << ")"; // bvor
2626  }
2627  else
2628  {
2629  throw "with expects struct, union, or array type, "
2630  "but got "+expr.type().id_string();
2631  }
2632 }
2633 
2635 {
2636  assert(expr.operands().size()==3);
2637 
2638  // todo
2639  throw "smt1_convt::convert_update to be implemented";
2640 }
2641 
2642 void smt1_convt::convert_index(const index_exprt &expr, bool bool_as_bv)
2643 {
2644  assert(expr.operands().size()==2);
2645 
2646  if(expr.array().id()==ID_member ||
2647  expr.array().id()==ID_index)
2648  {
2649  // arrays inside structs and 2-dimensional arrays
2650  // these were flattened
2651 
2652  const typet &array_type=to_array_type(expr.array().type());
2653  const typet &elem_type=array_type.subtype();
2654 
2655  std::size_t width=boolbv_width(expr.array().type());
2656  if(width==0)
2657  throw "failed to get array width";
2658 
2659  std::size_t elem_width=boolbv_width(elem_type);
2660 
2661  if(elem_width==0)
2662  throw "failed to get struct width";
2663 
2664  out << "(extract[" << elem_width-1 << ":0] ";
2665  out << "(bvlshr ";
2666  convert_expr(expr.array(), true);
2667  if(width>=array_index_bits)
2668  out << " (zero_extend[" << width-array_index_bits << "]";
2669  else
2670  out << " (extract[" << width-1 << ":0]";
2671  out << " (bvmul ";
2672  typecast_exprt index_tc(expr.index(), array_index_type());
2673  convert_expr(index_tc, true);
2674  out << " bv" << elem_width << "[" << array_index_bits << "]";
2675  out << "))))";
2676  }
2677  else
2678  {
2679  // Booleans out of arrays may have to be converted
2680  from_bv_begin(expr.type(), bool_as_bv);
2681 
2682  out << "(select ";
2683  convert_expr(expr.array(), true);
2684  out << " ";
2685  array_index(expr.index());
2686  out << ")";
2687 
2688  // Booleans out of arrays may have to be converted
2689  from_bv_end(expr.type(), bool_as_bv);
2690  }
2691 }
2692 
2693 void smt1_convt::convert_member(const member_exprt &expr, bool bool_as_bv)
2694 {
2695  assert(expr.operands().size()==1);
2696 
2697  const member_exprt &member_expr=to_member_expr(expr);
2698  const exprt &struct_op=member_expr.struct_op();
2699  const typet &struct_op_type=ns.follow(struct_op.type());
2700  const irep_idt &name=member_expr.get_component_name();
2701 
2702  // Booleans pulled out of structs may have to be converted
2703  from_bv_begin(expr.type(), bool_as_bv);
2704 
2705  if(struct_op_type.id()==ID_struct)
2706  {
2707  std::size_t offset=boolbv_width.get_member(
2708  to_struct_type(struct_op_type), name).offset;
2709 
2710  std::size_t width=boolbv_width(expr.type());
2711 
2712  if(width==0)
2713  throw "failed to get struct member width";
2714 
2715  out << "(extract["
2716  << (offset+width-1)
2717  << ":"
2718  << offset
2719  << "] ";
2720  convert_expr(struct_op, true);
2721  out << ")";
2722  }
2723  else if(struct_op_type.id()==ID_union)
2724  {
2725  std::size_t width=boolbv_width(expr.type());
2726 
2727  if(width==0)
2728  throw "failed to get union member width";
2729 
2730  out << "(extract["
2731  << (width-1)
2732  << ":0] ";
2733  convert_expr(struct_op, true);
2734  out << ")";
2735  }
2736  else
2737  assert(false);
2738 
2739  // Booleans pulled out of structs may have to be converted
2740  from_bv_end(expr.type(), bool_as_bv);
2741 }
2742 
2744 {
2745 }
2746 
2747 void smt1_convt::set_to(const exprt &expr, bool value)
2748 {
2749  if(expr.id()==ID_and && value)
2750  {
2751  forall_operands(it, expr)
2752  set_to(*it, true);
2753  return;
2754  }
2755 
2756  if(expr.id()==ID_not)
2757  {
2758  assert(expr.operands().size()==1);
2759  return set_to(expr.op0(), !value);
2760  }
2761 
2762  out << "\n";
2763 
2764  find_symbols(expr);
2765 
2766  #if 0
2767  out << "; CONV: "
2768  << from_expr(expr) << "\n";
2769  #endif
2770 
2771  out << ":assumption ; set_to "
2772  << (value?"true":"false") << "\n"
2773  << " ";
2774 
2775  assert(expr.type().id()==ID_bool);
2776 
2777  if(!value)
2778  {
2779  out << "(not ";
2780  convert_expr(expr, false);
2781  out << ")";
2782  }
2783  else
2784  convert_expr(expr, false);
2785 
2786  out << "\n";
2787 }
2788 
2790 {
2791  const typet &type=expr.type();
2792  find_symbols(type);
2793 
2794  if(expr.id()==ID_forall || expr.id()==ID_exists)
2795  {
2796  assert(expr.operands().size()==2);
2797  assert(expr.op0().id()==ID_symbol);
2798 
2799  const irep_idt &ident=expr.op0().get(ID_identifier);
2800  quantified_symbols.insert(ident);
2801  find_symbols(expr.op1());
2802  quantified_symbols.erase(ident);
2803  }
2804  else
2805  forall_operands(it, expr)
2806  find_symbols(*it);
2807 
2808  if(expr.id()==ID_symbol ||
2809  expr.id()==ID_nondet_symbol)
2810  {
2811  // we don't track function-typed symbols
2812  if(type.id()==ID_code)
2813  return;
2814 
2815  irep_idt identifier;
2816 
2817  if(expr.id()==ID_symbol)
2818  identifier=to_symbol_expr(expr).get_identifier();
2819  else
2820  identifier="nondet_"+expr.get_string(ID_identifier);
2821 
2822  if(quantified_symbols.find(identifier)!=quantified_symbols.end())
2823  return; // Symbol is quantified, i.e., it doesn't require declaration.
2824 
2825  identifiert &id=identifier_map[identifier];
2826 
2827  if(id.type.is_nil())
2828  {
2829  id.type=type;
2830 
2831  if(id.type.id()==ID_bool)
2832  {
2833  out << ":extrapreds(("
2834  << convert_identifier(identifier)
2835  << "))" << "\n";
2836  }
2837  else
2838  {
2839  out << ":extrafuns(("
2840  << convert_identifier(identifier)
2841  << " ";
2842  convert_type(type);
2843  out << "))" << "\n";
2844  }
2845  }
2846  }
2847  else if(expr.id()==ID_array_of)
2848  {
2849  if(array_of_map.find(expr)==array_of_map.end())
2850  {
2851  irep_idt id="array_of'"+std::to_string(array_of_map.size());
2852  out << "; the following is a poor substitute for lambda i. x" << "\n";
2853  out << ":extrafuns(("
2854  << id
2855  << " ";
2856  convert_type(type);
2857  out << "))" << "\n";
2858 
2859  // we can initialize array_ofs if they have
2860  // a constant size and a constant element
2861  if(type.find(ID_size)!=get_nil_irep() &&
2862  expr.op0().id()==ID_constant)
2863  {
2864  const array_typet &array_type=to_array_type(type);
2865  mp_integer size;
2866 
2867  if(!to_integer(array_type.size(), size))
2868  {
2869  // since we can't use quantifiers, let's enumerate...
2870  for(mp_integer i=0; i<size; ++i)
2871  {
2872  out << ":assumption (= (select " << id << " bv"
2873  << i << "[" << array_index_bits << "]) ";
2874  convert_expr(expr.op0(), true);
2875  out << ")" << "\n";
2876  }
2877  }
2878  }
2879 
2880  array_of_map[expr]=id;
2881  }
2882  }
2883  else if(expr.id()==ID_array)
2884  {
2885  if(array_expr_map.find(expr)==array_expr_map.end())
2886  {
2887  // introduce a temporary array.
2888  irep_idt id="array_init'"+std::to_string(array_expr_map.size());
2889  out << ":extrafuns(("
2890  << id
2891  << " ";
2892  convert_type(type);
2893  out << "))" << "\n";
2894  array_expr_map[expr]=id;
2895  }
2896  }
2897  else if(expr.id()==ID_string_constant)
2898  {
2899  if(string2array_map.find(expr)==string2array_map.end())
2900  {
2902  string2array_map[expr]=t;
2903 
2904  // introduce a temporary array.
2905  irep_idt id="string'"+std::to_string(array_expr_map.size());
2906  out << ":extrafuns(("
2907  << id
2908  << " ";
2909  convert_type(t.type());
2910  out << "))" << "\n";
2911  array_expr_map[t]=id;
2912  }
2913  }
2914 }
2915 
2917 {
2918  if(type.id()==ID_array)
2919  {
2920  const array_typet &array_type=to_array_type(type);
2921 
2922  out << "Array[" << array_index_bits << ":";
2923 
2924  std::size_t width=boolbv_width(array_type.subtype());
2925 
2926  if(width==0)
2927  throw "failed to get width of array subtype";
2928 
2929  out << width << "]";
2930  }
2931  else if(type.id()==ID_bool)
2932  {
2933  out << "BitVec[1]";
2934  }
2935  else if(type.id()==ID_struct ||
2936  type.id()==ID_union)
2937  {
2938  std::size_t width=boolbv_width(type);
2939 
2940  if(width==0)
2941  throw "failed to get width of struct/union";
2942 
2943  out << "BitVec[" << width << "]";
2944  }
2945  else if(type.id()==ID_pointer ||
2946  type.id()==ID_reference)
2947  {
2948  std::size_t width=boolbv_width(type);
2949 
2950  if(width==0)
2951  throw "failed to get width of pointer/reference";
2952 
2953  out << "BitVec[" << width << "]";
2954  }
2955  else if(type.id()==ID_bv ||
2956  type.id()==ID_floatbv ||
2957  type.id()==ID_fixedbv ||
2958  type.id()==ID_unsignedbv ||
2959  type.id()==ID_signedbv ||
2960  type.id()==ID_c_enum ||
2961  type.id()==ID_c_bool ||
2962  type.id()==ID_vector)
2963  {
2964  out << "BitVec[" << boolbv_width(type) << "]";
2965  }
2966  else if(type.id()==ID_c_enum_tag)
2968  else if(type.id()==ID_rational)
2969  out << "Real";
2970  else if(type.id()==ID_integer)
2971  out << "Int";
2972  else if(type.id()==ID_symbol)
2973  convert_type(ns.follow(type));
2974  else
2975  throw "unsupported type: "+type.id_string();
2976 }
2977 
2979 {
2980  if(l==const_literal(false))
2981  out << "false";
2982  else if(l==const_literal(true))
2983  out << "true";
2984  else
2985  {
2986  if(l.sign())
2987  out << "(not ";
2988 
2989  out << "B" << l.var_no();
2990 
2991  if(l.sign())
2992  out << ")";
2993  }
2994 }
2995 
2996 void smt1_convt::from_bv_begin(const typet &type, bool bool_as_bv)
2997 {
2998  // this turns bv[1] into a predicate if needed
2999  if(type.id()==ID_bool && !bool_as_bv)
3000  out << "(= ";
3001 }
3002 
3003 void smt1_convt::from_bv_end(const typet &type, bool bool_as_bv)
3004 {
3005  // this turns bv[1] into a predicate if needed
3006  if(type.id()==ID_bool && !bool_as_bv)
3007  out << " bv1[1])";
3008 }
3009 
3010 void smt1_convt::from_bool_begin(const typet &type, bool bool_as_bv)
3011 {
3012  // this turns a predicate into bv[1] if needed
3013  if(type.id()==ID_bool && bool_as_bv)
3014  out << "(ite ";
3015 }
3016 
3017 void smt1_convt::from_bool_end(const typet &type, bool bool_as_bv)
3018 {
3019  // this turns a predicate into bv[1] if needed
3020  if(type.id()==ID_bool && bool_as_bv)
3021  out << " bv1[1] bv0[1])";
3022 }
3023 
3025 {
3026  std::set<irep_idt> rec_stack;
3027  find_symbols_rec(type, rec_stack);
3028 }
3029 
3031  const typet &type,
3032  std::set<irep_idt> &recstack)
3033 {
3034  if(type.id()==ID_array)
3035  {
3036  const array_typet &array_type=to_array_type(type);
3037  find_symbols(array_type.size());
3038  find_symbols_rec(array_type.subtype(), recstack);
3039  }
3040  else if(type.id()==ID_struct ||
3041  type.id()==ID_union)
3042  {
3043  const struct_union_typet::componentst &components=
3045 
3046  for(const auto &comp : components)
3047  find_symbols_rec(comp.type(), recstack);
3048  }
3049  else if(type.id()==ID_code)
3050  {
3051  const code_typet::parameterst &parameters=
3052  to_code_type(type).parameters();
3053 
3054  for(const auto &param : parameters)
3055  find_symbols_rec(param.type(), recstack);
3056 
3057  find_symbols_rec(to_code_type(type).return_type(), recstack);
3058  }
3059  else if(type.id()==ID_pointer)
3060  {
3061  find_symbols_rec(type.subtype(), recstack);
3062  }
3063  else if(type.id()==ID_incomplete_array)
3064  {
3065  find_symbols_rec(type.subtype(), recstack);
3066  }
3067  else if(type.id()==ID_symbol)
3068  {
3069  const symbol_typet &st=to_symbol_type(type);
3070  const irep_idt &id=st.get_identifier();
3071 
3072  if(recstack.find(id)==recstack.end())
3073  {
3074  recstack.insert(id);
3075  find_symbols_rec(ns.follow(type), recstack);
3076  }
3077  }
3078 }
3079 
3081  const struct_typet &type,
3082  const std::string &binary) const
3083 {
3084  const struct_typet::componentst &components=type.components();
3085 
3086  std::size_t total_width=boolbv_width(type);
3087 
3088  if(total_width==0)
3089  throw "failed to get struct width";
3090 
3091  exprt e(ID_struct, type);
3092  e.operands().resize(components.size());
3093 
3094  std::size_t index=binary.size();
3095  std::size_t i=0;
3096  for(const auto &comp : components)
3097  {
3098  const typet &sub_type=ns.follow(comp.type());
3099 
3100  std::size_t sub_size=boolbv_width(sub_type);
3101 
3102  if(sub_size==0)
3103  throw "failed to get component width";
3104 
3105  index-=sub_size;
3106  std::string cval=binary.substr(index, sub_size);
3107 
3108  e.operands()[i++]=ce_value(sub_type, "", cval, true);
3109  }
3110 
3111  return e;
3112 }
3113 
3115  const union_typet &type,
3116  const std::string &binary) const
3117 {
3118  std::size_t total_width=boolbv_width(type);
3119 
3120  if(total_width==0)
3121  throw "failed to get union width";
3122 
3123  const union_typet::componentst &components=type.components();
3124 
3125  // Taking the first component should work.
3126  // Maybe a better idea is to take a largest component
3127  std::size_t component_nr=0;
3128 
3129  // construct a union expr
3130  union_exprt e(type);
3131  e.set_component_number(component_nr);
3132  e.set_component_name(components[component_nr].get_name());
3133 
3134  const typet &sub_type=ns.follow(components[component_nr].type());
3135  std::size_t comp_width=boolbv_width(sub_type);
3136  assert(comp_width<=total_width);
3137 
3138  std::string cval=binary.substr(total_width-comp_width, comp_width);
3139  e.op()=ce_value(sub_type, "", cval, true);
3140 
3141  return e;
3142 }
3143 
3145 {
3146  const array_typet array_type=to_array_type(op.type());
3147  const typet &elem_type=array_type.subtype();
3148  const exprt &size=array_type.size();
3149 
3150  if(size.id()!=ID_constant)
3151  throw "non-constant size array cannot be flattened";
3152 
3153  mp_integer sizei;
3154  if(to_integer(size, sizei))
3155  throw "array with non-constant size";
3156 
3157  std::size_t elem_width=boolbv_width(elem_type);
3158 
3159  if(elem_width==0)
3160  throw "failed to get width of array subtype";
3161 
3162  #if 0
3163  out << " (let (?fbv ";
3164  convert_expr(op, true);
3165  out << ")";
3166  #endif
3167 
3168  for(mp_integer i=1; i<sizei; ++i)
3169  out << "(concat ";
3170 
3171  for(mp_integer i=0; i<sizei; ++i)
3172  {
3173  out << " (select ";
3174  #if 0
3175  out << "?fbv";
3176  #else
3177  convert_expr(op, true);
3178  #endif
3179  out << " ";
3180  out << "bv" << i << "[" << array_index_bits << "]";
3181  out << ")";
3182  if(i!=0)
3183  out << ")"; // concat
3184  }
3185 
3186  #if 0
3187  out << ")"; // let
3188  #endif
3189 }
3190 
3192  const exprt &expr,
3193  const irep_idt op_string,
3194  bool bool_as_bv)
3195 {
3196  std::size_t num_ops=expr.operands().size();
3197 
3198  assert(num_ops>0);
3199 
3200  if(num_ops==1)
3201  convert_expr(expr.op0(), bool_as_bv);
3202  else
3203  {
3204  exprt::operandst::const_iterator it=
3205  expr.operands().begin();
3206 
3207  for(std::size_t i=0; i<num_ops-1; ++i, ++it)
3208  {
3209  out << "(" << op_string << " ";
3210  convert_expr(*it, bool_as_bv);
3211  out << " ";
3212  }
3213 
3214  // final one
3215  convert_expr(*it, bool_as_bv);
3216 
3217  // do the many closing parentheses
3218  out << std::string(num_ops-1, ')');
3219  }
3220 }
const irept & get_nil_irep()
Definition: irep.cpp:56
The type of an expression.
Definition: type.h:20
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
std::size_t get_null_object() const
Definition: pointer_logic.h:60
virtual void set_to(const exprt &expr, bool value)
Definition: smt1_conv.cpp:2747
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
void convert_overflow(const exprt &expr)
Definition: smt1_conv.cpp:2743
semantic type conversion
Definition: std_expr.h:1725
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
pointer_logict pointer_logic
Definition: smt1_conv.h:138
std::string source
Definition: smt1_conv.h:79
BigInt mp_integer
Definition: mp_arith.h:19
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void convert_type(const typet &type)
Definition: smt1_conv.cpp:2916
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
void convert_mult(const mult_exprt &expr)
Definition: smt1_conv.cpp:2223
void convert_minus(const minus_exprt &expr)
Definition: smt1_conv.cpp:2129
exprt & op0()
Definition: expr.h:84
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
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
void convert_expr(const exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:531
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
std::size_t get_integer_bits() const
Definition: std_types.cpp:15
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
const irep_idt & get_identifier() const
Definition: std_expr.h:120
#define forall_expr(it, expr)
Definition: expr.h:28
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
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
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 componentst & components() const
Definition: std_types.h:242
void write_footer()
Definition: smt1_conv.cpp:70
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
void convert_floatbv_minus(const exprt &expr)
Definition: smt1_conv.cpp:2168
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
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
std::string benchmark
Definition: smt1_conv.h:79
exprt & op()
Definition: std_expr.h:1739
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
void convert_byte_extract(const byte_extract_exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:356
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
virtual void print_assignment(std::ostream &out) const
Definition: smt1_conv.cpp:35
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1425
void find_symbols(const exprt &expr)
Definition: smt1_conv.cpp:2789
std::size_t get_invalid_object() const
Definition: pointer_logic.h:66
Extract member of struct or union.
Definition: std_expr.h:3214
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
identifier_mapt identifier_map
Definition: smt1_conv.h:173
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
virtual resultt dec_solve()
Definition: smt1_conv.cpp:55
void convert_byte_update(const exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:365
const irep_idt & id() const
Definition: irep.h:189
void convert_div(const div_exprt &expr)
Definition: smt1_conv.cpp:2176
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
const membert & get_member(const struct_typet &type, const irep_idt &member) const
void convert_union(const exprt &expr)
Definition: smt1_conv.cpp:1775
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
Expression classes for byte-level operators.
The boolean constant true.
Definition: std_expr.h:3742
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
virtual literalt convert(const exprt &expr)
Definition: smt1_conv.cpp:442
A reference into the symbol table.
Definition: std_types.h:109
A generic base class for binary expressions.
Definition: std_expr.h:471
void convert_update(const exprt &expr)
Definition: smt1_conv.cpp:2634
void convert_index(const index_exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:2642
The NIL expression.
Definition: std_expr.h:3764
The pointer type.
Definition: std_types.h:1343
std::size_t get_fraction_bits() const
Definition: std_types.h:1224
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1171
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.
std::string logic
Definition: smt1_conv.h:79
unsigned array_index_bits
Definition: smt1_conv.h:175
Definition: threeval.h:19
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
boolbv_widtht boolbv_width
Definition: smt1_conv.h:82
var_not var_no() const
Definition: literal.h:82
unsigned no_boolean_variables
Definition: smt1_conv.h:210
const exprt & size() const
Definition: std_types.h:915
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:702
const namespacet & ns
string2array_mapt string2array_map
Definition: smt1_conv.h:187
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
array_exprt to_array_expr() const
convert string into array constant
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
void convert_struct(const exprt &expr)
Definition: smt1_conv.cpp:1721
bitvector_typet index_type()
Definition: c_types.cpp:15
std::vector< bool > boolean_assignment
Definition: smt1_conv.h:211
Operator to return the address of an object.
Definition: std_expr.h:2593
The unary minus expression.
Definition: std_expr.h:346
void convert_plus(const plus_exprt &expr)
Definition: smt1_conv.cpp:2040
void convert_floatbv_plus(const exprt &expr)
Definition: smt1_conv.cpp:2121
virtual tvt l_get(literalt) const
Definition: smt1_conv.cpp:45
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
void from_bool_end(const typet &type, bool bool_as_bv)
Definition: smt1_conv.cpp:3017
std::vector< exprt > operandst
Definition: expr.h:49
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
void from_bv_begin(const typet &type, bool bool_as_bv)
Definition: smt1_conv.cpp:2996
Pointer Logic.
void convert_member(const member_exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:2693
void from_bool_begin(const typet &type, bool bool_as_bv)
Definition: smt1_conv.cpp:3010
array_of_mapt array_of_map
Definition: smt1_conv.h:179
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
virtual exprt get(const exprt &expr) const
Definition: smt1_conv.cpp:77
void write_header()
Definition: smt1_conv.cpp:62
literalt const_literal(bool value)
Definition: literal.h:187
void convert_floatbv_mult(const exprt &expr)
Definition: smt1_conv.cpp:2286
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1377
void convert_typecast(const typecast_exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:1340
API to type classes.
void convert_constant(const constant_exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:1804
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
Definition: std_expr.h:879
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1247
exprt & index()
Definition: std_expr.h:1208
const string_constantt & to_string_constant(const exprt &expr)
exprt ce_value(const typet &type, const std::string &index, const std::string &v, bool in_struct) const
Definition: smt1_conv.cpp:118
literalt get_literal() const
Definition: literal_expr.h:26
Base class for all expressions.
Definition: expr.h:46
void convert_nary(const exprt &expr, const irep_idt op_string, bool bool_as_bv)
Definition: smt1_conv.cpp:3191
std::size_t width
Definition: fixedbv.h:22
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
void convert_literal(const literalt l)
Definition: smt1_conv.cpp:2978
void flatten_array(const exprt &op)
Definition: smt1_conv.cpp:3144
Operator to update elements in structs and arrays.
Definition: std_expr.h:2861
void convert_with(const exprt &expr)
Definition: smt1_conv.cpp:2294
irep_idt get_component_name() const
Definition: std_expr.h:3249
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_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt1_conv.cpp:3030
const mult_exprt & to_mult_expr(const exprt &expr)
Cast a generic exprt to a mult_exprt.
Definition: std_expr.h:831
SMT Version 1 Backend.
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
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
void convert_relation(const exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:1975
#define Forall_operands(it, expr)
Definition: expr.h:23
void convert_floatbv_div(const exprt &expr)
Definition: smt1_conv.cpp:2215
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1415
bool is_zero() const
Definition: expr.cpp:236
arrays with given size
Definition: std_types.h:901
exprt binary2struct(const struct_typet &type, const std::string &binary) const
Definition: smt1_conv.cpp:3080
void convert_mod(const mod_exprt &expr)
Definition: smt1_conv.cpp:1905
binary minus
Definition: std_expr.h:758
std::ostream & out
Definition: smt1_conv.h:81
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
std::size_t width() const
Definition: ieee_float.h:50
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
Pointer Logic.
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
const typet & subtype() const
Definition: type.h:31
exprt binary2union(const union_typet &type, const std::string &binary) const
Definition: smt1_conv.cpp:3114
operandst & operands()
Definition: expr.h:70
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
std::size_t add_object(const exprt &expr)
exprt & array()
Definition: std_expr.h:1198
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const irep_idt & get_identifier() const
Definition: std_types.h:126
binary modulo
Definition: std_expr.h:902
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
void convert_is_dynamic_object(const exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:1926
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
Definition: smt1_conv.cpp:252
void from_bv_end(const typet &type, bool bool_as_bv)
Definition: smt1_conv.cpp:3003
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
array_expr_mapt array_expr_map
Definition: smt1_conv.h:183
#define BV_ADDR_BITS
Definition: pointer_logic.h:19
void set_width(std::size_t width)
Definition: std_types.h:1035
std::string convert_identifier(const irep_idt &identifier)
Definition: smt1_conv.cpp:478
void array_index(const exprt &expr)
Definition: smt1_conv.cpp:239
array index operator
Definition: std_expr.h:1170
std::set< irep_idt > quantified_symbols
Definition: smt1_conv.h:121
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