28 while(bits!=0) { result+=
'0'; bits--; }
35 return "[# object: INT, offset: BITVECTOR("+
41 return std::string(
"SIGNED [")+std::to_string(32)+
"]";
72 if(expr.
id()==ID_symbol ||
73 expr.
id()==ID_constant ||
74 expr.
id()==ID_string_constant)
82 else if(expr.
id()==ID_index)
85 throw "index takes two operands";
92 if(array.
type().
id()==ID_pointer)
94 else if(array.
type().
id()==ID_array)
101 dplib_prop.out <<
"(LET P: ";
103 dplib_prop.out <<
" = ";
105 if(array.
type().
id()==ID_pointer)
107 else if(array.
type().
id()==ID_array)
112 dplib_prop.out <<
" IN P WITH .offset:=BVPLUS(" 116 dplib_prop.out <<
"))";
119 else if(expr.
id()==ID_member)
122 throw "member takes one operand";
126 dplib_prop.out <<
"(LET P: ";
128 dplib_prop.out <<
" = ";
144 dplib_prop.out <<
" IN P WITH .offset:=BVPLUS(" 148 dplib_prop.out <<
"))";
151 throw "don't know how to take address of: "+expr.
id_string();
162 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
166 dplib_prop.out <<
"ASSERT " << dplib_prop.dplib_literal(l) <<
" <=> (";
168 dplib_prop.out << ((expr.
id()==ID_equal)?
"=":
"/=");
170 dplib_prop.out <<
");\n";
178 for(std::string::const_iterator
179 it=identifier.begin();
180 it!=identifier.end();
185 if(isalnum(ch) || ch==
'$' || ch==
'?')
186 dplib_prop.out << ch;
189 std::string::const_iterator next_it(it);
191 if(next_it!=identifier.end() && *next_it==
':')
193 dplib_prop.out <<
"__";
198 dplib_prop.out <<
'_';
199 dplib_prop.out << int(ch);
200 dplib_prop.out <<
'_';
205 dplib_prop.out <<
'_';
206 dplib_prop.out << int(ch);
207 dplib_prop.out <<
'_';
214 if(expr.
type().
id()==ID_bool)
216 dplib_prop.out <<
"IF ";
218 dplib_prop.out <<
" THEN 0bin1 ELSE 0bin0 ENDIF";
231 if(expr.
id()==ID_symbol)
235 else if(expr.
id()==ID_nondet_symbol)
239 else if(expr.
id()==ID_typecast)
244 if(expr.
type().
id()==ID_bool)
246 if(op.type().id()==ID_signedbv ||
247 op.type().id()==ID_unsignedbv ||
248 op.type().id()==ID_pointer)
251 dplib_prop.out <<
"/=";
257 throw "TODO typecast1 "+op.type().id_string()+
" -> bool";
260 else if(expr.
type().
id()==ID_signedbv ||
261 expr.
type().
id()==ID_unsignedbv)
266 if(op.type().id()==ID_signedbv)
271 if(from_width==to_width)
273 else if(from_width<to_width)
275 dplib_prop.out <<
"SX(";
277 dplib_prop.out <<
", " << to_width <<
")";
281 dplib_prop.out <<
"(";
283 dplib_prop.out <<
")[" << (to_width-1) <<
":0]";
286 else if(op.type().id()==ID_unsignedbv)
291 if(from_width==to_width)
293 else if(from_width<to_width)
295 dplib_prop.out <<
"(0bin";
297 for(
unsigned i=from_width; i<to_width; i++)
298 dplib_prop.out <<
"0";
300 dplib_prop.out <<
" @ ";
302 dplib_prop.out <<
"(";
304 dplib_prop.out <<
"))";
308 dplib_prop.out <<
"(";
310 dplib_prop.out <<
")[" << (to_width-1) <<
":0]";
313 else if(op.type().id()==ID_bool)
317 dplib_prop.out <<
"(0bin";
319 for(
unsigned i=1; i<to_width; i++)
320 dplib_prop.out <<
"0";
322 dplib_prop.out <<
" @ ";
324 dplib_prop.out <<
"IF ";
326 dplib_prop.out <<
" THEN 0bin1 ELSE 0bin0 ENDIF)";
330 dplib_prop.out <<
"IF ";
332 dplib_prop.out <<
" THEN 0bin1 ELSE 0bin0 ENDIF";
338 throw "TODO typecast2 "+op.type().id_string()+
342 else if(expr.
type().
id()==ID_pointer)
344 if(op.type().id()==ID_pointer)
350 throw "TODO typecast3 "+op.type().id_string()+
" -> pointer";
356 else if(expr.
id()==ID_struct)
358 dplib_prop.out <<
"(# ";
365 assert(components.size()==expr.
operands().size());
368 for(struct_typet::componentst::const_iterator
369 it=components.begin();
370 it!=components.end();
374 dplib_prop.out <<
", ";
375 dplib_prop.out << it->get(ID_name);
376 dplib_prop.out <<
":=";
380 dplib_prop.out <<
" #)";
382 else if(expr.
id()==ID_constant)
384 if(expr.
type().
id()==ID_unsignedbv ||
385 expr.
type().
id()==ID_signedbv ||
388 dplib_prop.out <<
"0bin" << expr.
get(ID_value);
390 else if(expr.
type().
id()==ID_pointer)
396 dplib_prop.out <<
"(# object:=" 402 throw "unknown pointer constant: "+
id2string(value);
404 else if(expr.
type().
id()==ID_bool)
407 dplib_prop.out <<
"TRUE";
409 dplib_prop.out <<
"FALSE";
411 throw "unknown boolean constant";
413 else if(expr.
type().
id()==ID_array)
423 dplib_prop.out <<
"\n IF ";
425 dplib_prop.out <<
"\n ELSIF ";
427 dplib_prop.out <<
"i=" <<
array_index(i) <<
" THEN ";
432 dplib_prop.out <<
"\n ELSE ";
434 dplib_prop.out <<
"\n ENDIF";
436 else if(expr.
type().
id()==ID_integer ||
437 expr.
type().
id()==ID_natural ||
438 expr.
type().
id()==ID_range)
440 dplib_prop.out << expr.
get(ID_value);
445 else if(expr.
id()==ID_concatenation ||
446 expr.
id()==ID_bitand ||
449 dplib_prop.out <<
"(";
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 <<
" | ";
466 dplib_prop.out <<
")";
468 else if(expr.
id()==ID_bitxor)
478 dplib_prop.out <<
"BVXOR(";
480 dplib_prop.out <<
", ";
482 dplib_prop.out <<
")";
489 tmp.operands().resize(tmp.operands().size()-1);
491 dplib_prop.out <<
"BVXOR(";
493 dplib_prop.out <<
", ";
495 dplib_prop.out <<
")";
498 else if(expr.
id()==ID_bitnand)
502 dplib_prop.out <<
"BVNAND(";
504 dplib_prop.out <<
", ";
506 dplib_prop.out <<
")";
508 else if(expr.
id()==ID_bitnot)
511 dplib_prop.out <<
"~(";
513 dplib_prop.out <<
")";
515 else if(expr.
id()==ID_unary_minus)
518 if(expr.
type().
id()==ID_unsignedbv ||
519 expr.
type().
id()==ID_signedbv)
521 dplib_prop.out <<
"BVUMINUS(";
523 dplib_prop.out <<
")";
526 throw "unsupported type for unary-: "+expr.
type().
id_string();
528 else if(expr.
id()==ID_if)
531 dplib_prop.out <<
"IF ";
533 dplib_prop.out <<
" THEN ";
535 dplib_prop.out <<
" ELSE ";
537 dplib_prop.out <<
" ENDIF";
539 else if(expr.
id()==ID_and ||
543 assert(expr.
type().
id()==ID_bool);
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 ";
559 dplib_prop.out <<
"(";
561 dplib_prop.out <<
")";
571 else if(expr.
id()==ID_not)
574 dplib_prop.out <<
"NOT (";
576 dplib_prop.out <<
")";
578 else if(expr.
id()==ID_equal ||
579 expr.
id()==ID_notequal)
586 if(expr.
id()==ID_notequal)
587 dplib_prop.out <<
"NOT (";
588 dplib_prop.out <<
"(";
590 dplib_prop.out <<
") <=> (";
592 dplib_prop.out <<
")";
593 if(expr.
id()==ID_notequal)
594 dplib_prop.out <<
")";
598 dplib_prop.out <<
"(";
600 dplib_prop.out <<
")";
601 dplib_prop.out << (expr.
id()==ID_equal?
"=":
"/=");
602 dplib_prop.out <<
"(";
604 dplib_prop.out <<
")";
607 else if(expr.
id()==ID_le ||
616 if(op_type.id()==ID_unsignedbv)
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";
627 dplib_prop.out <<
"(";
629 dplib_prop.out <<
", ";
631 dplib_prop.out <<
")";
633 else if(op_type.id()==ID_signedbv)
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";
644 dplib_prop.out <<
"(";
646 dplib_prop.out <<
", ";
648 dplib_prop.out <<
")";
654 else if(expr.
id()==ID_plus)
658 if(expr.
type().
id()==ID_unsignedbv ||
659 expr.
type().
id()==ID_signedbv)
661 dplib_prop.out <<
"BVPLUS(" << expr.
type().
get(ID_width);
665 dplib_prop.out <<
", ";
669 dplib_prop.out <<
")";
671 else if(expr.
type().
id()==ID_pointer)
674 throw "pointer arithmetic with more than two operands";
683 else if(expr.
op1().
type().
id()==ID_pointer)
689 throw "unexpected mixture in pointer arithmetic";
693 dplib_prop.out <<
" IN P WITH .offset:=BVPLUS(" 697 dplib_prop.out <<
"))";
709 else if(expr.
id()==ID_minus)
713 if(expr.
type().
id()==ID_unsignedbv ||
714 expr.
type().
id()==ID_signedbv)
716 dplib_prop.out <<
"BVSUB(" << expr.
type().
get(ID_width) <<
", ";
718 dplib_prop.out <<
", ";
720 dplib_prop.out <<
")";
732 else if(expr.
id()==ID_div)
736 if(expr.
type().
id()==ID_unsignedbv ||
737 expr.
type().
id()==ID_signedbv)
739 if(expr.
type().
id()==ID_unsignedbv)
740 dplib_prop.out <<
"BVDIV";
742 dplib_prop.out <<
"SBVDIV";
744 dplib_prop.out <<
"(" << expr.
type().
get(ID_width) <<
", ";
746 dplib_prop.out <<
", ";
748 dplib_prop.out <<
")";
753 else if(expr.
id()==ID_mod)
757 if(expr.
type().
id()==ID_unsignedbv ||
758 expr.
type().
id()==ID_signedbv)
760 if(expr.
type().
id()==ID_unsignedbv)
761 dplib_prop.out <<
"BVMOD";
763 dplib_prop.out <<
"SBVMOD";
765 dplib_prop.out <<
"(" << expr.
type().
get(ID_width) <<
", ";
767 dplib_prop.out <<
", ";
769 dplib_prop.out <<
")";
774 else if(expr.
id()==ID_mult)
778 if(expr.
type().
id()==ID_unsignedbv ||
779 expr.
type().
id()==ID_signedbv)
781 dplib_prop.out <<
"BVMULT(" << expr.
type().
get(ID_width) <<
", ";
783 dplib_prop.out <<
", ";
785 dplib_prop.out <<
")";
797 else if(expr.
id()==ID_address_of ||
798 expr.
id()==
"reference_to")
801 assert(expr.
type().
id()==ID_pointer);
804 else if(expr.
id()==ID_array_of)
806 assert(expr.
type().
id()==ID_array);
810 dplib_prop.out <<
")";
812 else if(expr.
id()==ID_index)
815 dplib_prop.out <<
"(";
817 dplib_prop.out <<
")[";
819 dplib_prop.out <<
"]";
821 else if(expr.
id()==ID_ashr ||
822 expr.
id()==ID_lshr ||
827 if(expr.
type().
id()==ID_unsignedbv ||
828 expr.
type().
id()==ID_signedbv)
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";
839 dplib_prop.out <<
"(" << expr.
type().
get(ID_width) <<
", ";
841 dplib_prop.out <<
", ";
843 dplib_prop.out <<
")";
849 else if(expr.
id()==ID_with)
852 dplib_prop.out <<
"(";
854 dplib_prop.out <<
")";
856 for(
unsigned i=1; i<expr.
operands().size(); i+=2)
858 assert((i+1)<expr.
operands().size());
862 if(expr.
type().
id()==ID_struct)
864 dplib_prop.out <<
" WITH ." << index.get(ID_component_name);
865 dplib_prop.out <<
":=(";
867 dplib_prop.out <<
")";
869 else if(expr.
type().
id()==ID_union)
871 dplib_prop.out <<
" WITH ." << index.get(ID_component_name);
872 dplib_prop.out <<
":=(";
874 dplib_prop.out <<
")";
876 else if(expr.
type().
id()==ID_array)
878 dplib_prop.out <<
" WITH [";
880 dplib_prop.out <<
"]:=(";
882 dplib_prop.out <<
")";
886 "with expects struct or array type, but got "+
890 else if(expr.
id()==ID_member)
894 dplib_prop.out <<
".";
895 dplib_prop.out << expr.
get(ID_component_name);
897 else if(expr.
id()==ID_pointer_offset)
900 dplib_prop.out <<
"(";
902 dplib_prop.out <<
").offset";
905 else if(expr.
id()==ID_pointer_object)
908 dplib_prop.out <<
"(";
910 dplib_prop.out <<
").object";
914 else if(expr.
id()==ID_string_constant)
918 else if(expr.
id()==ID_extractbit)
922 if(expr.
op0().
type().
id()==ID_unsignedbv ||
929 throw "extractbit takes constant as second parameter";
931 dplib_prop.out <<
"[" << i <<
"]";
935 "unsupported type for "+expr.
id_string()+
": "+
938 else if(expr.
id()==ID_replication)
944 throw "replication takes constant as first parameter";
946 dplib_prop.out <<
"(LET v: BITVECTOR(1) = ";
950 dplib_prop.out <<
" IN ";
955 dplib_prop.out <<
"@";
956 dplib_prop.out <<
"v";
959 dplib_prop.out <<
")";
962 throw "convert_dplib_expr: "+expr.
id_string()+
" is unsupported";
967 if(value && expr.
id()==ID_and)
977 dplib_prop.out <<
"// set_to " << (value?
"true":
"false") <<
'\n';
979 if(expr.
id()==ID_equal && value)
983 if(expr.
op0().
id()==ID_symbol)
991 std::unordered_set<irep_idt, irep_id_hash> s_set;
995 if(s_set.find(identifier)==s_set.end())
1002 dplib_prop.out <<
": ";
1004 dplib_prop.out <<
" = ";
1007 dplib_prop.out <<
";\n\n";
1016 dplib_prop.out <<
"AXIOM ";
1019 dplib_prop.out <<
"! (";
1024 dplib_prop.out <<
")";
1026 dplib_prop.out <<
";\n\n";
1036 if(expr.
id()==ID_symbol)
1038 if(expr.
type().
id()==ID_code)
1041 const irep_idt &identifier=expr.
get(ID_identifier);
1045 if(
id.type.is_nil())
1047 id.type=expr.
type();
1050 dplib_prop.out <<
": ";
1052 dplib_prop.out <<
";\n";
1055 else if(expr.
id()==ID_nondet_symbol)
1057 if(expr.
type().
id()==ID_code)
1064 if(
id.type.is_nil())
1066 id.type=expr.
type();
1069 dplib_prop.out <<
": ";
1071 dplib_prop.out <<
";\n";
1078 if(type.
id()==ID_array)
1086 dplib_prop.out <<
"BITVECTOR(1)";
1090 else if(type.
id()==ID_bool)
1092 dplib_prop.out <<
"boolean";
1094 else if(type.
id()==ID_struct ||
1095 type.
id()==ID_union)
1099 dplib_prop.out <<
"[#";
1104 for(struct_typet::componentst::const_iterator
1105 it=components.begin();
1106 it!=components.end();
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 <<
": ";
1117 dplib_prop.out <<
" #]";
1119 else if(type.
id()==ID_pointer ||
1120 type.
id()==ID_reference)
1124 else if(type.
id()==ID_integer)
1126 dplib_prop.out <<
"int";
1128 else if(type.
id()==ID_signedbv)
1133 throw "zero-width vector type: "+type.
id_string();
1135 dplib_prop.out <<
"signed[" << width <<
"]";
1137 else if(type.
id()==ID_unsignedbv)
1142 throw "zero-width vector type: "+type.
id_string();
1144 dplib_prop.out <<
"unsigned[" << width <<
"]";
1146 else if(type.
id()==ID_bv)
1151 throw "zero-width vector type: "+type.
id_string();
1153 dplib_prop.out <<
"bv[" << width <<
"]";
1156 throw "unsupported type: "+type.
id_string();
1161 if(type.
id()==ID_array)
1166 else if(type.
id()==ID_struct ||
1167 type.
id()==ID_union)
static typet gen_array_index_type()
The type of an expression.
std::size_t get_null_object() const
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
void convert_as_bv(const exprt &expr)
void find_symbols(const exprt &expr)
virtual void convert_dplib_expr(const exprt &expr)
static std::string array_index_type()
unsigned unsafe_string2unsigned(const std::string &str, int base)
void copy_to_operands(const exprt &expr)
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
std::vector< componentt > componentst
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const componentst & components() const
void convert_array_value(const exprt &expr)
static std::string array_index(unsigned i)
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
static std::string bin_zero(unsigned bits)
static std::string dplib_pointer_type()
API to expression classes.
const irep_idt & get(const irep_namet &name) const
pointer_logict pointer_logic
identifier_mapt identifier_map
const exprt & size() const
#define forall_operands(it, expr)
bitvector_typet index_type()
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
const array_exprt & to_array_expr(const exprt &expr)
Cast a generic exprt to an array_exprt.
std::size_t get_width() const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
virtual literalt convert_rest(const exprt &expr)
virtual void convert_dplib_type(const typet &type)
const string_constantt & to_string_constant(const exprt &expr)
Base class for all expressions.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
void convert_identifier(const std::string &identifier)
irep_idt get_component_name() const
const std::string integer2binary(const mp_integer &n, std::size_t width)
virtual void set_to(const exprt &expr, bool value)
const std::string & get_string(const irep_namet &name) const
const std::string & id_string() const
virtual void convert_address_of_rec(const exprt &expr)
void convert_array_index(const exprt &expr)
const typet & subtype() const
std::size_t add_object(const exprt &expr)
void set(const irep_namet &name, const irep_idt &value)