cprover
dplib_conv.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "dplib_conv.h"
10 
11 #include <cassert>
12 #include <cctype>
13 
14 #include <util/arith_tools.h>
15 #include <util/std_types.h>
16 #include <util/std_expr.h>
17 #include <util/config.h>
18 #include <util/find_symbols.h>
20 #include <util/string2int.h>
21 
22 #include <ansi-c/string_constant.h>
23 
24 std::string dplib_convt::bin_zero(unsigned bits)
25 {
26  assert(bits!=0);
27  std::string result="0bin";
28  while(bits!=0) { result+='0'; bits--; }
29  return result;
30 }
31 
33 {
34  assert(config.ansi_c.pointer_width!=0);
35  return "[# object: INT, offset: BITVECTOR("+
36  std::to_string(config.ansi_c.pointer_width)+") #]";
37 }
38 
40 {
41  return std::string("SIGNED [")+std::to_string(32)+"]";
42 }
43 
45 {
46  typet t(ID_signedbv);
47  t.set(ID_width, 32);
48  return t;
49 }
50 
51 std::string dplib_convt::array_index(unsigned i)
52 {
53  return "0bin"+integer2binary(i, config.ansi_c.int_width);
54 }
55 
57 {
58  if(expr.type()==gen_array_index_type())
59  {
60  convert_dplib_expr(expr);
61  }
62  else
63  {
64  exprt tmp(ID_typecast, gen_array_index_type());
65  tmp.copy_to_operands(expr);
66  convert_dplib_expr(tmp);
67  }
68 }
69 
71 {
72  if(expr.id()==ID_symbol ||
73  expr.id()==ID_constant ||
74  expr.id()==ID_string_constant)
75  {
76  dplib_prop.out
77  << "(# object:="
78  << pointer_logic.add_object(expr)
79  << ", offset:="
80  << bin_zero(config.ansi_c.pointer_width) << " #)";
81  }
82  else if(expr.id()==ID_index)
83  {
84  if(expr.operands().size()!=2)
85  throw "index takes two operands";
86 
87  const exprt &array=expr.op0();
88  const exprt &index=expr.op1();
89 
90  if(index.is_zero())
91  {
92  if(array.type().id()==ID_pointer)
93  convert_dplib_expr(array);
94  else if(array.type().id()==ID_array)
96  else
97  assert(false);
98  }
99  else
100  {
101  dplib_prop.out << "(LET P: ";
102  dplib_prop.out << dplib_pointer_type();
103  dplib_prop.out << " = ";
104 
105  if(array.type().id()==ID_pointer)
106  convert_dplib_expr(array);
107  else if(array.type().id()==ID_array)
108  convert_address_of_rec(array);
109  else
110  assert(false);
111 
112  dplib_prop.out << " IN P WITH .offset:=BVPLUS("
114  << ", P.offset, ";
115  convert_dplib_expr(index);
116  dplib_prop.out << "))";
117  }
118  }
119  else if(expr.id()==ID_member)
120  {
121  if(expr.operands().size()!=1)
122  throw "member takes one operand";
123 
124  const exprt &struct_op=expr.op0();
125 
126  dplib_prop.out << "(LET P: ";
127  dplib_prop.out << dplib_pointer_type();
128  dplib_prop.out << " = ";
129 
130  convert_address_of_rec(struct_op);
131 
132  const irep_idt &component_name=
134 
135  mp_integer offset=member_offset(ns,
136  to_struct_type(struct_op.type()), component_name);
137  assert(offset>=0);
138 
139  typet index_type(ID_unsignedbv);
140  index_type.set(ID_width, config.ansi_c.pointer_width);
141 
142  exprt index=from_integer(offset, index_type);
143 
144  dplib_prop.out << " IN P WITH .offset:=BVPLUS("
146  << ", P.offset, ";
147  convert_dplib_expr(index);
148  dplib_prop.out << "))";
149  }
150  else
151  throw "don't know how to take address of: "+expr.id_string();
152 }
153 
155 {
156  // dplib_prop.out << "%% E: " << expr << '\n';
157 
158  literalt l=prop.new_variable();
159 
160  find_symbols(expr);
161 
162  if(expr.id()==ID_equal || expr.id()==ID_notequal)
163  {
164  assert(expr.operands().size()==2);
165 
166  dplib_prop.out << "ASSERT " << dplib_prop.dplib_literal(l) << " <=> (";
167  convert_dplib_expr(expr.op0());
168  dplib_prop.out << ((expr.id()==ID_equal)?"=":"/=");
169  convert_dplib_expr(expr.op1());
170  dplib_prop.out << ");\n";
171  }
172 
173  return l;
174 }
175 
176 void dplib_convt::convert_identifier(const std::string &identifier)
177 {
178  for(std::string::const_iterator
179  it=identifier.begin();
180  it!=identifier.end();
181  it++)
182  {
183  char ch=*it;
184 
185  if(isalnum(ch) || ch=='$' || ch=='?')
186  dplib_prop.out << ch;
187  else if(ch==':')
188  {
189  std::string::const_iterator next_it(it);
190  next_it++;
191  if(next_it!=identifier.end() && *next_it==':')
192  {
193  dplib_prop.out << "__";
194  it=next_it;
195  }
196  else
197  {
198  dplib_prop.out << '_';
199  dplib_prop.out << int(ch);
200  dplib_prop.out << '_';
201  }
202  }
203  else
204  {
205  dplib_prop.out << '_';
206  dplib_prop.out << int(ch);
207  dplib_prop.out << '_';
208  }
209  }
210 }
211 
213 {
214  if(expr.type().id()==ID_bool)
215  {
216  dplib_prop.out << "IF ";
217  convert_dplib_expr(expr);
218  dplib_prop.out << " THEN 0bin1 ELSE 0bin0 ENDIF";
219  }
220  else
221  convert_dplib_expr(expr);
222 }
223 
225 {
226  convert_as_bv(expr);
227 }
228 
230 {
231  if(expr.id()==ID_symbol)
232  {
233  convert_identifier(expr.get_string(ID_identifier));
234  }
235  else if(expr.id()==ID_nondet_symbol)
236  {
237  convert_identifier("nondet$"+expr.get_string(ID_identifier));
238  }
239  else if(expr.id()==ID_typecast)
240  {
241  assert(expr.operands().size()==1);
242  const exprt &op=expr.op0();
243 
244  if(expr.type().id()==ID_bool)
245  {
246  if(op.type().id()==ID_signedbv ||
247  op.type().id()==ID_unsignedbv ||
248  op.type().id()==ID_pointer)
249  {
250  convert_dplib_expr(op);
251  dplib_prop.out << "/=";
252  convert_dplib_expr(from_integer(0, op.type()));
253  }
254  else
255  {
256  // NOLINTNEXTLINE(readability/throw)
257  throw "TODO typecast1 "+op.type().id_string()+" -> bool";
258  }
259  }
260  else if(expr.type().id()==ID_signedbv ||
261  expr.type().id()==ID_unsignedbv)
262  {
263  unsigned to_width=
264  unsafe_string2unsigned(id2string(expr.type().get(ID_width)));
265 
266  if(op.type().id()==ID_signedbv)
267  {
268  unsigned from_width=
269  unsafe_string2unsigned(id2string(op.type().get(ID_width)));
270 
271  if(from_width==to_width)
272  convert_dplib_expr(op);
273  else if(from_width<to_width)
274  {
275  dplib_prop.out << "SX(";
276  convert_dplib_expr(op);
277  dplib_prop.out << ", " << to_width << ")";
278  }
279  else
280  {
281  dplib_prop.out << "(";
282  convert_dplib_expr(op);
283  dplib_prop.out << ")[" << (to_width-1) << ":0]";
284  }
285  }
286  else if(op.type().id()==ID_unsignedbv)
287  {
288  unsigned from_width=
289  unsafe_string2unsigned(id2string(op.type().get(ID_width)));
290 
291  if(from_width==to_width)
292  convert_dplib_expr(op);
293  else if(from_width<to_width)
294  {
295  dplib_prop.out << "(0bin";
296 
297  for(unsigned i=from_width; i<to_width; i++)
298  dplib_prop.out << "0";
299 
300  dplib_prop.out << " @ ";
301 
302  dplib_prop.out << "(";
303  convert_dplib_expr(op);
304  dplib_prop.out << "))";
305  }
306  else
307  {
308  dplib_prop.out << "(";
309  convert_dplib_expr(op);
310  dplib_prop.out << ")[" << (to_width-1) << ":0]";
311  }
312  }
313  else if(op.type().id()==ID_bool)
314  {
315  if(to_width>1)
316  {
317  dplib_prop.out << "(0bin";
318 
319  for(unsigned i=1; i<to_width; i++)
320  dplib_prop.out << "0";
321 
322  dplib_prop.out << " @ ";
323 
324  dplib_prop.out << "IF ";
325  convert_dplib_expr(op);
326  dplib_prop.out << " THEN 0bin1 ELSE 0bin0 ENDIF)";
327  }
328  else
329  {
330  dplib_prop.out << "IF ";
331  convert_dplib_expr(op);
332  dplib_prop.out << " THEN 0bin1 ELSE 0bin0 ENDIF";
333  }
334  }
335  else
336  {
337  // NOLINTNEXTLINE(readability/throw)
338  throw "TODO typecast2 "+op.type().id_string()+
339  " -> "+expr.type().id_string();
340  }
341  }
342  else if(expr.type().id()==ID_pointer)
343  {
344  if(op.type().id()==ID_pointer)
345  {
346  convert_dplib_expr(op);
347  }
348  else
349  // NOLINTNEXTLINE(readability/throw)
350  throw "TODO typecast3 "+op.type().id_string()+" -> pointer";
351  }
352  else
353  // NOLINTNEXTLINE(readability/throw)
354  throw "TODO typecast4 ? -> "+expr.type().id_string();
355  }
356  else if(expr.id()==ID_struct)
357  {
358  dplib_prop.out << "(# ";
359 
360  const struct_typet &struct_type=to_struct_type(expr.type());
361 
362  const struct_typet::componentst &components=
363  struct_type.components();
364 
365  assert(components.size()==expr.operands().size());
366 
367  unsigned i=0;
368  for(struct_typet::componentst::const_iterator
369  it=components.begin();
370  it!=components.end();
371  it++, i++)
372  {
373  if(i!=0)
374  dplib_prop.out << ", ";
375  dplib_prop.out << it->get(ID_name);
376  dplib_prop.out << ":=";
377  convert_dplib_expr(expr.operands()[i]);
378  }
379 
380  dplib_prop.out << " #)";
381  }
382  else if(expr.id()==ID_constant)
383  {
384  if(expr.type().id()==ID_unsignedbv ||
385  expr.type().id()==ID_signedbv ||
386  expr.type().id()==ID_bv)
387  {
388  dplib_prop.out << "0bin" << expr.get(ID_value);
389  }
390  else if(expr.type().id()==ID_pointer)
391  {
392  const irep_idt &value=expr.get(ID_value);
393 
394  if(value=="NULL")
395  {
396  dplib_prop.out << "(# object:="
398  << ", offset:="
399  << bin_zero(config.ansi_c.pointer_width) << " #)";
400  }
401  else
402  throw "unknown pointer constant: "+id2string(value);
403  }
404  else if(expr.type().id()==ID_bool)
405  {
406  if(expr.is_true())
407  dplib_prop.out << "TRUE";
408  else if(expr.is_false())
409  dplib_prop.out << "FALSE";
410  else
411  throw "unknown boolean constant";
412  }
413  else if(expr.type().id()==ID_array)
414  {
415  dplib_prop.out << "ARRAY (i: " << array_index_type() << "):";
416 
417  assert(!expr.operands().empty());
418 
419  unsigned i=0;
420  forall_operands(it, expr)
421  {
422  if(i==0)
423  dplib_prop.out << "\n IF ";
424  else
425  dplib_prop.out << "\n ELSIF ";
426 
427  dplib_prop.out << "i=" << array_index(i) << " THEN ";
428  convert_array_value(*it);
429  i++;
430  }
431 
432  dplib_prop.out << "\n ELSE ";
433  convert_dplib_expr(expr.op0());
434  dplib_prop.out << "\n ENDIF";
435  }
436  else if(expr.type().id()==ID_integer ||
437  expr.type().id()==ID_natural ||
438  expr.type().id()==ID_range)
439  {
440  dplib_prop.out << expr.get(ID_value);
441  }
442  else
443  throw "unknown constant: "+expr.type().id_string();
444  }
445  else if(expr.id()==ID_concatenation ||
446  expr.id()==ID_bitand ||
447  expr.id()==ID_bitor)
448  {
449  dplib_prop.out << "(";
450 
451  forall_operands(it, expr)
452  {
453  if(it!=expr.operands().begin())
454  {
455  if(expr.id()==ID_concatenation)
456  dplib_prop.out << " @ ";
457  else if(expr.id()==ID_bitand)
458  dplib_prop.out << " & ";
459  else if(expr.id()==ID_bitor)
460  dplib_prop.out << " | ";
461  }
462 
463  convert_as_bv(*it);
464  }
465 
466  dplib_prop.out << ")";
467  }
468  else if(expr.id()==ID_bitxor)
469  {
470  assert(!expr.operands().empty());
471 
472  if(expr.operands().size()==1)
473  {
474  convert_dplib_expr(expr.op0());
475  }
476  else if(expr.operands().size()==2)
477  {
478  dplib_prop.out << "BVXOR(";
479  convert_dplib_expr(expr.op0());
480  dplib_prop.out << ", ";
481  convert_dplib_expr(expr.op1());
482  dplib_prop.out << ")";
483  }
484  else
485  {
486  assert(expr.operands().size()>=3);
487 
488  exprt tmp(expr);
489  tmp.operands().resize(tmp.operands().size()-1);
490 
491  dplib_prop.out << "BVXOR(";
492  convert_dplib_expr(tmp);
493  dplib_prop.out << ", ";
494  convert_dplib_expr(expr.operands().back());
495  dplib_prop.out << ")";
496  }
497  }
498  else if(expr.id()==ID_bitnand)
499  {
500  assert(expr.operands().size()==2);
501 
502  dplib_prop.out << "BVNAND(";
503  convert_dplib_expr(expr.op0());
504  dplib_prop.out << ", ";
505  convert_dplib_expr(expr.op1());
506  dplib_prop.out << ")";
507  }
508  else if(expr.id()==ID_bitnot)
509  {
510  assert(expr.operands().size()==1);
511  dplib_prop.out << "~(";
512  convert_dplib_expr(expr.op0());
513  dplib_prop.out << ")";
514  }
515  else if(expr.id()==ID_unary_minus)
516  {
517  assert(expr.operands().size()==1);
518  if(expr.type().id()==ID_unsignedbv ||
519  expr.type().id()==ID_signedbv)
520  {
521  dplib_prop.out << "BVUMINUS(";
522  convert_dplib_expr(expr.op0());
523  dplib_prop.out << ")";
524  }
525  else
526  throw "unsupported type for unary-: "+expr.type().id_string();
527  }
528  else if(expr.id()==ID_if)
529  {
530  assert(expr.operands().size()==3);
531  dplib_prop.out << "IF ";
532  convert_dplib_expr(expr.op0());
533  dplib_prop.out << " THEN ";
534  convert_dplib_expr(expr.op1());
535  dplib_prop.out << " ELSE ";
536  convert_dplib_expr(expr.op2());
537  dplib_prop.out << " ENDIF";
538  }
539  else if(expr.id()==ID_and ||
540  expr.id()==ID_or ||
541  expr.id()==ID_xor)
542  {
543  assert(expr.type().id()==ID_bool);
544 
545  if(expr.operands().size()>=2)
546  {
547  forall_operands(it, expr)
548  {
549  if(it!=expr.operands().begin())
550  {
551  if(expr.id()==ID_and)
552  dplib_prop.out << " AND ";
553  else if(expr.id()==ID_or)
554  dplib_prop.out << " OR ";
555  else if(expr.id()==ID_xor)
556  dplib_prop.out << " XOR ";
557  }
558 
559  dplib_prop.out << "(";
560  convert_dplib_expr(*it);
561  dplib_prop.out << ")";
562  }
563  }
564  else if(expr.operands().size()==1)
565  {
566  convert_dplib_expr(expr.op0());
567  }
568  else
569  assert(false);
570  }
571  else if(expr.id()==ID_not)
572  {
573  assert(expr.operands().size()==1);
574  dplib_prop.out << "NOT (";
575  convert_dplib_expr(expr.op0());
576  dplib_prop.out << ")";
577  }
578  else if(expr.id()==ID_equal ||
579  expr.id()==ID_notequal)
580  {
581  assert(expr.operands().size()==2);
582  assert(expr.op0().type()==expr.op1().type());
583 
584  if(expr.op0().type().id()==ID_bool)
585  {
586  if(expr.id()==ID_notequal)
587  dplib_prop.out << "NOT (";
588  dplib_prop.out << "(";
589  convert_dplib_expr(expr.op0());
590  dplib_prop.out << ") <=> (";
591  convert_dplib_expr(expr.op1());
592  dplib_prop.out << ")";
593  if(expr.id()==ID_notequal)
594  dplib_prop.out << ")";
595  }
596  else
597  {
598  dplib_prop.out << "(";
599  convert_dplib_expr(expr.op0());
600  dplib_prop.out << ")";
601  dplib_prop.out << (expr.id()==ID_equal?"=":"/=");
602  dplib_prop.out << "(";
603  convert_dplib_expr(expr.op1());
604  dplib_prop.out << ")";
605  }
606  }
607  else if(expr.id()==ID_le ||
608  expr.id()==ID_lt ||
609  expr.id()==ID_ge ||
610  expr.id()==ID_gt)
611  {
612  assert(expr.operands().size()==2);
613 
614  const typet &op_type=expr.op0().type();
615 
616  if(op_type.id()==ID_unsignedbv)
617  {
618  if(expr.id()==ID_le)
619  dplib_prop.out << "BVLE";
620  else if(expr.id()==ID_lt)
621  dplib_prop.out << "BVLT";
622  else if(expr.id()==ID_ge)
623  dplib_prop.out << "BVGE";
624  else if(expr.id()==ID_gt)
625  dplib_prop.out << "BVGT";
626 
627  dplib_prop.out << "(";
628  convert_dplib_expr(expr.op0());
629  dplib_prop.out << ", ";
630  convert_dplib_expr(expr.op1());
631  dplib_prop.out << ")";
632  }
633  else if(op_type.id()==ID_signedbv)
634  {
635  if(expr.id()==ID_le)
636  dplib_prop.out << "SBVLE";
637  else if(expr.id()==ID_lt)
638  dplib_prop.out << "SBVLT";
639  else if(expr.id()==ID_ge)
640  dplib_prop.out << "SBVGE";
641  else if(expr.id()==ID_gt)
642  dplib_prop.out << "SBVGT";
643 
644  dplib_prop.out << "(";
645  convert_dplib_expr(expr.op0());
646  dplib_prop.out << ", ";
647  convert_dplib_expr(expr.op1());
648  dplib_prop.out << ")";
649  }
650  else
651  throw
652  "unsupported type for "+expr.id_string()+": "+expr.type().id_string();
653  }
654  else if(expr.id()==ID_plus)
655  {
656  if(expr.operands().size()>=2)
657  {
658  if(expr.type().id()==ID_unsignedbv ||
659  expr.type().id()==ID_signedbv)
660  {
661  dplib_prop.out << "BVPLUS(" << expr.type().get(ID_width);
662 
663  forall_operands(it, expr)
664  {
665  dplib_prop.out << ", ";
666  convert_dplib_expr(*it);
667  }
668 
669  dplib_prop.out << ")";
670  }
671  else if(expr.type().id()==ID_pointer)
672  {
673  if(expr.operands().size()!=2)
674  throw "pointer arithmetic with more than two operands";
675 
676  const exprt *p, *i;
677 
678  if(expr.op0().type().id()==ID_pointer)
679  {
680  p=&expr.op0();
681  i=&expr.op1();
682  }
683  else if(expr.op1().type().id()==ID_pointer)
684  {
685  p=&expr.op1();
686  i=&expr.op0();
687  }
688  else
689  throw "unexpected mixture in pointer arithmetic";
690 
691  dplib_prop.out << "(LET P: " << dplib_pointer_type() << " = ";
692  convert_dplib_expr(*p);
693  dplib_prop.out << " IN P WITH .offset:=BVPLUS("
695  << ", P.offset, ";
696  convert_dplib_expr(*i);
697  dplib_prop.out << "))";
698  }
699  else
700  throw "unsupported type for +: "+expr.type().id_string();
701  }
702  else if(expr.operands().size()==1)
703  {
704  convert_dplib_expr(expr.op0());
705  }
706  else
707  assert(false);
708  }
709  else if(expr.id()==ID_minus)
710  {
711  if(expr.operands().size()==2)
712  {
713  if(expr.type().id()==ID_unsignedbv ||
714  expr.type().id()==ID_signedbv)
715  {
716  dplib_prop.out << "BVSUB(" << expr.type().get(ID_width) << ", ";
717  convert_dplib_expr(expr.op0());
718  dplib_prop.out << ", ";
719  convert_dplib_expr(expr.op1());
720  dplib_prop.out << ")";
721  }
722  else
723  throw "unsupported type for -: "+expr.type().id_string();
724  }
725  else if(expr.operands().size()==1)
726  {
727  convert_dplib_expr(expr.op0());
728  }
729  else
730  assert(false);
731  }
732  else if(expr.id()==ID_div)
733  {
734  assert(expr.operands().size()==2);
735 
736  if(expr.type().id()==ID_unsignedbv ||
737  expr.type().id()==ID_signedbv)
738  {
739  if(expr.type().id()==ID_unsignedbv)
740  dplib_prop.out << "BVDIV";
741  else
742  dplib_prop.out << "SBVDIV";
743 
744  dplib_prop.out << "(" << expr.type().get(ID_width) << ", ";
745  convert_dplib_expr(expr.op0());
746  dplib_prop.out << ", ";
747  convert_dplib_expr(expr.op1());
748  dplib_prop.out << ")";
749  }
750  else
751  throw "unsupported type for /: "+expr.type().id_string();
752  }
753  else if(expr.id()==ID_mod)
754  {
755  assert(expr.operands().size()==2);
756 
757  if(expr.type().id()==ID_unsignedbv ||
758  expr.type().id()==ID_signedbv)
759  {
760  if(expr.type().id()==ID_unsignedbv)
761  dplib_prop.out << "BVMOD";
762  else
763  dplib_prop.out << "SBVMOD";
764 
765  dplib_prop.out << "(" << expr.type().get(ID_width) << ", ";
766  convert_dplib_expr(expr.op0());
767  dplib_prop.out << ", ";
768  convert_dplib_expr(expr.op1());
769  dplib_prop.out << ")";
770  }
771  else
772  throw "unsupported type for mod: "+expr.type().id_string();
773  }
774  else if(expr.id()==ID_mult)
775  {
776  if(expr.operands().size()==2)
777  {
778  if(expr.type().id()==ID_unsignedbv ||
779  expr.type().id()==ID_signedbv)
780  {
781  dplib_prop.out << "BVMULT(" << expr.type().get(ID_width) << ", ";
782  convert_dplib_expr(expr.op0());
783  dplib_prop.out << ", ";
784  convert_dplib_expr(expr.op1());
785  dplib_prop.out << ")";
786  }
787  else
788  throw "unsupported type for *: "+expr.type().id_string();
789  }
790  else if(expr.operands().size()==1)
791  {
792  convert_dplib_expr(expr.op0());
793  }
794  else
795  assert(false);
796  }
797  else if(expr.id()==ID_address_of ||
798  expr.id()=="reference_to")
799  {
800  assert(expr.operands().size()==1);
801  assert(expr.type().id()==ID_pointer);
802  convert_address_of_rec(expr.op0());
803  }
804  else if(expr.id()==ID_array_of)
805  {
806  assert(expr.type().id()==ID_array);
807  assert(expr.operands().size()==1);
808  dplib_prop.out << "(ARRAY (i: " << array_index_type() << "): ";
809  convert_array_value(expr.op0());
810  dplib_prop.out << ")";
811  }
812  else if(expr.id()==ID_index)
813  {
814  assert(expr.operands().size()==2);
815  dplib_prop.out << "(";
816  convert_dplib_expr(expr.op0());
817  dplib_prop.out << ")[";
818  convert_array_index(expr.op1());
819  dplib_prop.out << "]";
820  }
821  else if(expr.id()==ID_ashr ||
822  expr.id()==ID_lshr ||
823  expr.id()==ID_shl)
824  {
825  assert(expr.operands().size()==2);
826 
827  if(expr.type().id()==ID_unsignedbv ||
828  expr.type().id()==ID_signedbv)
829  {
830  if(expr.id()==ID_ashr)
831  dplib_prop.out << "BVASHR";
832  else if(expr.id()==ID_lshr)
833  dplib_prop.out << "BVLSHR";
834  else if(expr.id()==ID_shl)
835  dplib_prop.out << "BVSHL";
836  else
837  assert(false);
838 
839  dplib_prop.out << "(" << expr.type().get(ID_width) << ", ";
840  convert_dplib_expr(expr.op0());
841  dplib_prop.out << ", ";
842  convert_dplib_expr(expr.op1());
843  dplib_prop.out << ")";
844  }
845  else
846  throw
847  "unsupported type for "+expr.id_string()+": "+expr.type().id_string();
848  }
849  else if(expr.id()==ID_with)
850  {
851  assert(expr.operands().size()>=1);
852  dplib_prop.out << "(";
853  convert_dplib_expr(expr.op0());
854  dplib_prop.out << ")";
855 
856  for(unsigned i=1; i<expr.operands().size(); i+=2)
857  {
858  assert((i+1)<expr.operands().size());
859  const exprt &index=expr.operands()[i];
860  const exprt &value=expr.operands()[i+1];
861 
862  if(expr.type().id()==ID_struct)
863  {
864  dplib_prop.out << " WITH ." << index.get(ID_component_name);
865  dplib_prop.out << ":=(";
866  convert_array_value(value);
867  dplib_prop.out << ")";
868  }
869  else if(expr.type().id()==ID_union)
870  {
871  dplib_prop.out << " WITH ." << index.get(ID_component_name);
872  dplib_prop.out << ":=(";
873  convert_array_value(value);
874  dplib_prop.out << ")";
875  }
876  else if(expr.type().id()==ID_array)
877  {
878  dplib_prop.out << " WITH [";
879  convert_array_index(index);
880  dplib_prop.out << "]:=(";
881  convert_array_value(value);
882  dplib_prop.out << ")";
883  }
884  else
885  throw
886  "with expects struct or array type, but got "+
887  expr.type().id_string();
888  }
889  }
890  else if(expr.id()==ID_member)
891  {
892  assert(expr.operands().size()==1);
893  convert_dplib_expr(expr.op0());
894  dplib_prop.out << ".";
895  dplib_prop.out << expr.get(ID_component_name);
896  }
897  else if(expr.id()==ID_pointer_offset)
898  {
899  assert(expr.operands().size()==1);
900  dplib_prop.out << "(";
901  convert_dplib_expr(expr.op0());
902  dplib_prop.out << ").offset";
903  }
904  #if 0
905  else if(expr.id()==ID_pointer_object)
906  {
907  assert(expr.operands().size()==1);
908  dplib_prop.out << "(";
909  convert_dplib_expr(expr.op0());
910  dplib_prop.out << ").object";
911  // TODO this has the wrong type
912  }
913  #endif
914  else if(expr.id()==ID_string_constant)
915  {
917  }
918  else if(expr.id()==ID_extractbit)
919  {
920  assert(expr.operands().size()==2);
921 
922  if(expr.op0().type().id()==ID_unsignedbv ||
923  expr.op0().type().id()==ID_signedbv)
924  {
925  convert_dplib_expr(expr.op0());
926 
927  mp_integer i;
928  if(to_integer(expr.op1(), i))
929  throw "extractbit takes constant as second parameter";
930 
931  dplib_prop.out << "[" << i << "]";
932  }
933  else
934  throw
935  "unsupported type for "+expr.id_string()+": "+
936  expr.op0().type().id_string();
937  }
938  else if(expr.id()==ID_replication)
939  {
940  assert(expr.operands().size()==2);
941 
942  mp_integer times;
943  if(to_integer(expr.op0(), times))
944  throw "replication takes constant as first parameter";
945 
946  dplib_prop.out << "(LET v: BITVECTOR(1) = ";
947 
948  convert_dplib_expr(expr.op1());
949 
950  dplib_prop.out << " IN ";
951 
952  for(mp_integer i=0; i<times; ++i)
953  {
954  if(i!=0)
955  dplib_prop.out << "@";
956  dplib_prop.out << "v";
957  }
958 
959  dplib_prop.out << ")";
960  }
961  else
962  throw "convert_dplib_expr: "+expr.id_string()+" is unsupported";
963 }
964 
965 void dplib_convt::set_to(const exprt &expr, bool value)
966 {
967  if(value && expr.id()==ID_and)
968  {
969  forall_operands(it, expr)
970  set_to(*it, true);
971  return;
972  }
973 
974  if(value && expr.is_true())
975  return;
976 
977  dplib_prop.out << "// set_to " << (value?"true":"false") << '\n';
978 
979  if(expr.id()==ID_equal && value)
980  {
981  assert(expr.operands().size()==2);
982 
983  if(expr.op0().id()==ID_symbol)
984  {
985  const irep_idt &identifier=expr.op0().get(ID_identifier);
986 
987  identifiert &id=identifier_map[identifier];
988 
989  if(id.type.is_nil())
990  {
991  std::unordered_set<irep_idt, irep_id_hash> s_set;
992 
993  ::find_symbols(expr.op1(), s_set);
994 
995  if(s_set.find(identifier)==s_set.end())
996  {
997  id.type=expr.op0().type();
998 
999  find_symbols(expr.op1());
1000 
1001  convert_identifier(id2string(identifier));
1002  dplib_prop.out << ": ";
1003  convert_dplib_type(expr.op0().type());
1004  dplib_prop.out << " = ";
1005  convert_dplib_expr(expr.op1());
1006 
1007  dplib_prop.out << ";\n\n";
1008  return;
1009  }
1010  }
1011  }
1012  }
1013 
1014  find_symbols(expr);
1015 
1016  dplib_prop.out << "AXIOM ";
1017 
1018  if(!value)
1019  dplib_prop.out << "! (";
1020 
1021  convert_dplib_expr(expr);
1022 
1023  if(!value)
1024  dplib_prop.out << ")";
1025 
1026  dplib_prop.out << ";\n\n";
1027 }
1028 
1030 {
1031  find_symbols(expr.type());
1032 
1033  forall_operands(it, expr)
1034  find_symbols(*it);
1035 
1036  if(expr.id()==ID_symbol)
1037  {
1038  if(expr.type().id()==ID_code)
1039  return;
1040 
1041  const irep_idt &identifier=expr.get(ID_identifier);
1042 
1043  identifiert &id=identifier_map[identifier];
1044 
1045  if(id.type.is_nil())
1046  {
1047  id.type=expr.type();
1048 
1049  convert_identifier(id2string(identifier));
1050  dplib_prop.out << ": ";
1051  convert_dplib_type(expr.type());
1052  dplib_prop.out << ";\n";
1053  }
1054  }
1055  else if(expr.id()==ID_nondet_symbol)
1056  {
1057  if(expr.type().id()==ID_code)
1058  return;
1059 
1060  const irep_idt identifier="nondet$"+expr.get_string(ID_identifier);
1061 
1062  identifiert &id=identifier_map[identifier];
1063 
1064  if(id.type.is_nil())
1065  {
1066  id.type=expr.type();
1067 
1068  convert_identifier(id2string(identifier));
1069  dplib_prop.out << ": ";
1070  convert_dplib_type(expr.type());
1071  dplib_prop.out << ";\n";
1072  }
1073  }
1074 }
1075 
1077 {
1078  if(type.id()==ID_array)
1079  {
1080  const array_typet &array_type=to_array_type(type);
1081 
1082  dplib_prop.out << "ARRAY " << array_index_type()
1083  << " OF ";
1084 
1085  if(array_type.subtype().id()==ID_bool)
1086  dplib_prop.out << "BITVECTOR(1)";
1087  else
1088  convert_dplib_type(array_type.subtype());
1089  }
1090  else if(type.id()==ID_bool)
1091  {
1092  dplib_prop.out << "boolean";
1093  }
1094  else if(type.id()==ID_struct ||
1095  type.id()==ID_union)
1096  {
1097  const struct_typet &struct_type=to_struct_type(type);
1098 
1099  dplib_prop.out << "[#";
1100 
1101  const struct_typet::componentst &components=
1102  struct_type.components();
1103 
1104  for(struct_typet::componentst::const_iterator
1105  it=components.begin();
1106  it!=components.end();
1107  it++)
1108  {
1109  if(it!=components.begin())
1110  dplib_prop.out << ",";
1111  dplib_prop.out << " ";
1112  dplib_prop.out << it->get(ID_name);
1113  dplib_prop.out << ": ";
1114  convert_dplib_type(it->type());
1115  }
1116 
1117  dplib_prop.out << " #]";
1118  }
1119  else if(type.id()==ID_pointer ||
1120  type.id()==ID_reference)
1121  {
1122  dplib_prop.out << dplib_pointer_type();
1123  }
1124  else if(type.id()==ID_integer)
1125  {
1126  dplib_prop.out << "int";
1127  }
1128  else if(type.id()==ID_signedbv)
1129  {
1130  unsigned width=to_signedbv_type(type).get_width();
1131 
1132  if(width==0)
1133  throw "zero-width vector type: "+type.id_string();
1134 
1135  dplib_prop.out << "signed[" << width << "]";
1136  }
1137  else if(type.id()==ID_unsignedbv)
1138  {
1139  unsigned width=to_unsignedbv_type(type).get_width();
1140 
1141  if(width==0)
1142  throw "zero-width vector type: "+type.id_string();
1143 
1144  dplib_prop.out << "unsigned[" << width << "]";
1145  }
1146  else if(type.id()==ID_bv)
1147  {
1148  unsigned width=to_bv_type(type).get_width();
1149 
1150  if(width==0)
1151  throw "zero-width vector type: "+type.id_string();
1152 
1153  dplib_prop.out << "bv[" << width << "]";
1154  }
1155  else
1156  throw "unsupported type: "+type.id_string();
1157 }
1158 
1160 {
1161  if(type.id()==ID_array)
1162  {
1163  const array_typet &array_type=to_array_type(type);
1164  find_symbols(array_type.size());
1165  }
1166  else if(type.id()==ID_struct ||
1167  type.id()==ID_union)
1168  {
1169  }
1170 }
static typet gen_array_index_type()
Definition: dplib_conv.cpp:44
The type of an expression.
Definition: type.h:20
std::size_t get_null_object() const
Definition: pointer_logic.h:60
mstreamt & result()
Definition: message.h:233
struct configt::ansi_ct ansi_c
BigInt mp_integer
Definition: mp_arith.h:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void convert_as_bv(const exprt &expr)
Definition: dplib_conv.cpp:212
unsigned int_width
Definition: config.h:30
void find_symbols(const exprt &expr)
exprt & op0()
Definition: expr.h:84
virtual void convert_dplib_expr(const exprt &expr)
Definition: dplib_conv.cpp:229
static std::string array_index_type()
Definition: dplib_conv.cpp:39
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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
const componentst & components() const
Definition: std_types.h:242
void convert_array_value(const exprt &expr)
Definition: dplib_conv.cpp:224
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
Structure type.
Definition: std_types.h:296
configt config
Definition: config.cpp:21
static std::string array_index(unsigned i)
Definition: dplib_conv.cpp:51
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
static std::string bin_zero(unsigned bits)
Definition: dplib_conv.cpp:24
static std::string dplib_pointer_type()
Definition: dplib_conv.cpp:32
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
pointer_logict pointer_logic
Definition: dplib_conv.h:40
identifier_mapt identifier_map
Definition: dplib_conv.h:70
const exprt & size() const
Definition: std_types.h:915
#define forall_operands(it, expr)
Definition: expr.h:17
const namespacet & ns
bitvector_typet index_type()
Definition: c_types.cpp:15
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1154
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
Definition: std_expr.h:1332
std::size_t get_width() const
Definition: std_types.h:1030
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Definition: std_types.h:1108
Pointer Logic.
virtual literalt convert_rest(const exprt &expr)
Definition: dplib_conv.cpp:154
API to type classes.
virtual void convert_dplib_type(const typet &type)
const string_constantt & to_string_constant(const exprt &expr)
Base class for all expressions.
Definition: expr.h:46
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
void convert_identifier(const std::string &identifier)
Definition: dplib_conv.cpp:176
irep_idt get_component_name() const
Definition: std_expr.h:3249
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
virtual void set_to(const exprt &expr, bool value)
Definition: dplib_conv.cpp:965
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const std::string & id_string() const
Definition: irep.h:192
bool is_zero() const
Definition: expr.cpp:236
arrays with given size
Definition: std_types.h:901
virtual void convert_address_of_rec(const exprt &expr)
Definition: dplib_conv.cpp:70
void convert_array_index(const exprt &expr)
Definition: dplib_conv.cpp:56
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
const typet & subtype() const
Definition: type.h:31
unsigned pointer_width
Definition: config.h:36
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::size_t add_object(const exprt &expr)
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214