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