65 out <<
":source { " <<
source <<
" }" <<
"\n";
66 out <<
":status unknown" <<
"\n";
67 out <<
":logic " <<
logic <<
" ; SMT1" <<
"\n";
73 out <<
":formula true" <<
"\n";
74 out <<
") ; benchmark" <<
"\n";
79 if(expr.
id()==ID_symbol)
86 return it->second.value;
88 else if(expr.
id()==ID_member)
96 else if(expr.
id()==ID_index)
105 else if(expr.
id()==ID_constant)
107 else if(expr.
id()==ID_typecast)
120 const std::string &index,
121 const std::string &value,
122 bool in_struct)
const 124 if(type.
id()==ID_symbol)
127 if(type.
id()==ID_signedbv ||
128 type.
id()==ID_unsignedbv ||
130 type.
id()==ID_fixedbv)
137 else if(type.
id()==ID_bool)
144 else if(type.
id()==ID_pointer)
165 else if(type.
id()==ID_struct)
169 else if(type.
id()==ID_union)
173 else if(type.
id()==ID_array)
186 std::size_t sub_width=value.size()/size_int;
187 exprt array_list(ID_array, type);
188 array_list.
operands().resize(size_int);
190 std::size_t offset=value.size();
192 for(std::size_t i=0; i!=size_int; i++)
195 std::string sub_value=value.substr(offset, sub_width);
197 ce_value(subtype,
"", sub_value,
true);
203 else if(subtype.
id()==ID_array)
206 return ce_value(subtype,
"", value,
true);
222 exprt array_list(
"array-list", type);
241 if(expr.
type().
id()==ID_integer)
247 exprt tmp(ID_typecast, t);
256 if(expr.
id()==ID_symbol ||
257 expr.
id()==ID_constant ||
258 expr.
id()==ID_string_constant ||
267 else if(expr.
id()==ID_index)
270 throw "index takes two operands";
277 if(array.
type().
id()==ID_pointer)
279 else if(array.
type().
id()==ID_array)
287 exprt new_index_expr=expr;
297 address_of_expr.
type());
302 else if(expr.
id()==ID_member)
305 throw "member takes one operand";
312 if(struct_op_type.
id()==ID_struct)
332 else if(struct_op_type.
id()==ID_union)
338 throw "unexpected type of member operand";
340 else if(expr.
id()==ID_if)
353 throw "don't know how to take address of: "+expr.
id_string();
378 throw "byte_update takes constant as second operand";
383 throw "failed to get width of byte_update operand";
389 if(expr.
id()==ID_byte_update_little_endian)
392 upper = lower+op_w-1;
397 lower = max-(i*8+op_w-1);
408 out <<
" (extract[" << lower-1 <<
":0] ";
419 out <<
"(extract[" << max <<
":" << (upper+1) <<
"] ";
427 out <<
"(concat (concat";
428 out <<
" (extract[" << max <<
":" << (upper+1) <<
"] ";
434 out<<
" (extract[" << (lower-1) <<
":0] ";
444 assert(expr.
type().
id()==ID_bool);
452 else if(expr.
id()==ID_literal)
464 out <<
":extrapreds((";
468 out <<
":assumption ; convert " <<
"\n" 480 std::string s=
id2string(identifier), dest;
481 dest.reserve(s.size());
489 for(std::string::const_iterator
496 if(isalnum(ch) || ch==
'_')
500 std::string::const_iterator next_it(it);
502 if(next_it!=s.end() && *next_it==
':')
523 dest.append(std::to_string(ch));
533 if(expr.
id()==ID_symbol)
547 else if(expr.
id()==ID_nondet_symbol)
561 else if(expr.
id()==ID_literal)
565 else if(expr.
id()==ID_typecast)
569 else if(expr.
id()==ID_struct)
573 else if(expr.
id()==ID_union)
577 else if(expr.
id()==ID_constant)
581 else if(expr.
id()==ID_concatenation)
583 else if(expr.
id()==ID_bitand)
585 else if(expr.
id()==ID_bitor)
587 else if(expr.
id()==ID_bitxor)
589 else if(expr.
id()==ID_bitnand)
591 else if(expr.
id()==ID_bitnor)
593 else if(expr.
id()==ID_bitnot)
600 else if(expr.
id()==ID_unary_minus)
606 if(type.
id()==ID_rational)
612 else if(type.
id()==ID_integer)
625 else if(expr.
id()==ID_if)
630 if(expr.
op1().
type().
id()==ID_bool && !bool_as_bv)
631 out <<
"(if_then_else ";
642 else if(expr.
id()==ID_and ||
649 assert(type.
id()==ID_bool);
650 assert(operands.size()>=2);
655 out <<
"(" << expr.
id();
666 else if(expr.
id()==ID_implies)
670 assert(type.
id()==ID_bool);
685 else if(expr.
id()==ID_not)
701 else if(expr.
id()==ID_equal ||
702 expr.
id()==ID_notequal)
714 if(expr.
id()==ID_notequal)
726 if(expr.
id()==ID_notequal)
747 else if(expr.
id()==ID_le ||
754 else if(expr.
id()==ID_plus)
758 else if(expr.
id()==ID_floatbv_plus)
762 else if(expr.
id()==ID_minus)
766 else if(expr.
id()==ID_floatbv_minus)
770 else if(expr.
id()==ID_div)
774 else if(expr.
id()==ID_floatbv_div)
778 else if(expr.
id()==ID_mod)
782 else if(expr.
id()==ID_mult)
786 else if(expr.
id()==ID_floatbv_mult)
790 else if(expr.
id()==ID_address_of)
795 assert(type.
id()==ID_pointer);
798 else if(expr.
id()==
"implicit_address_of" ||
799 expr.
id()==
"reference_to")
804 else if(expr.
id()==ID_array_of)
806 assert(expr.
type().
id()==ID_array);
813 array_of_mapt::const_iterator it=
array_of_map.find(expr);
818 else if(expr.
id()==ID_index)
822 else if(expr.
id()==ID_ashr ||
823 expr.
id()==ID_lshr ||
830 if(type.
id()==ID_unsignedbv ||
831 type.
id()==ID_signedbv ||
833 type.
id()==ID_struct ||
836 if(expr.
id()==ID_ashr)
838 else if(expr.
id()==ID_lshr)
840 else if(expr.
id()==ID_shl)
854 if(width_op0==width_op1)
856 else if(width_op0>width_op1)
858 out <<
"(zero_extend[" << width_op0-width_op1 <<
"] ";
864 out <<
"(extract[" << width_op0-1 <<
":0] ";
872 throw "unsupported type for "+expr.
id_string()+
875 else if(expr.
id()==ID_with)
879 else if(expr.
id()==ID_update)
883 else if(expr.
id()==ID_member)
887 else if(expr.
id()==ID_pointer_offset)
890 assert(expr.
op0().
type().
id()==ID_pointer);
899 else if(expr.
id()==ID_pointer_object)
902 assert(expr.
op0().
type().
id()==ID_pointer);
907 out <<
"(zero_extend[" << ext <<
"] ";
919 else if(expr.
id()==
"is_dynamic_object")
923 else if(expr.
id()==ID_invalid_pointer)
928 assert(expr.
op0().
type().
id()==ID_pointer);
934 out <<
"(= (extract[" 944 else if(expr.
id()==
"pointer_object_has_type")
958 else if(expr.
id()==ID_string_constant)
966 else if(expr.
id()==ID_extractbit)
970 if(expr.
op0().
type().
id()==ID_unsignedbv ||
982 throw "extractbit: to_integer failed";
984 out <<
"(extract[" << i <<
":" << i <<
"] ";
990 out <<
"(extract[0:0] ";
1004 throw "unsupported type for "+expr.
id_string()+
1007 else if(expr.
id()==ID_replication)
1013 throw "replication takes constant as first parameter";
1015 out <<
"(repeat[" << times <<
"] ";
1019 else if(expr.
id()==ID_byte_extract_little_endian ||
1020 expr.
id()==ID_byte_extract_big_endian)
1024 else if(expr.
id()==ID_byte_update_little_endian ||
1025 expr.
id()==ID_byte_update_big_endian)
1029 else if(expr.
id()==ID_width)
1034 throw "conversion failed";
1037 throw "width expects 1 operand";
1042 throw "conversion failed";
1044 out <<
"bv" << op_width/8 <<
"[" << result_width <<
"]";
1046 else if(expr.
id()==ID_abs)
1056 throw "conversion failed";
1058 if(type.
id()==ID_signedbv ||
1059 type.
id()==ID_fixedbv)
1061 out <<
"(ite (bvslt ";
1063 out <<
" bv0[" << result_width <<
"]) ";
1070 else if(type.
id()==ID_floatbv)
1075 << (
power(2, result_width-1)-1)
1076 <<
"[" << result_width <<
"])";
1079 throw "abs with unsupported operand type";
1081 else if(expr.
id()==ID_isnan)
1089 if(op_type.id()==ID_fixedbv)
1096 throw "isnan with unsupported operand type";
1098 else if(expr.
id()==ID_isfinite)
1103 throw "isfinite expects one operand";
1107 if(op_type.
id()==ID_fixedbv)
1114 throw "isfinite with unsupported operand type";
1116 else if(expr.
id()==ID_isinf)
1121 throw "isinf expects one operand";
1125 if(op_type.
id()==ID_fixedbv)
1132 throw "isinf with unsupported operand type";
1134 else if(expr.
id()==ID_isnormal)
1139 throw "isnormal expects one operand";
1143 if(op_type.
id()==ID_fixedbv)
1150 throw "isnormal with unsupported operand type";
1152 else if(expr.
id()==ID_overflow_plus ||
1153 expr.
id()==ID_overflow_minus)
1158 bool subtract=expr.
id()==ID_overflow_minus;
1164 if(op_type.
id()==ID_signedbv)
1169 out <<
"(let (?sum (";
1170 out << (subtract?
"bvsub":
"bvadd");
1171 out <<
" (sign_extend[1] ";
1174 out <<
" (sign_extend[1] ";
1178 "(extract[" << width <<
":" << width <<
"] ?sum) " 1179 "(extract[" << (width-1) <<
":" << (width-1) <<
"] ?sum)";
1183 else if(op_type.
id()==ID_unsignedbv)
1187 out <<
"(extract[" << width <<
":" << width <<
"] ";
1188 out <<
"(" << (subtract?
"bvsub":
"bvadd");
1189 out <<
" (zero_extend[1] ";
1192 out <<
" (zero_extend[1] ";
1198 throw "overflow check on unknown type: "+op_type.
id_string();
1200 else if(expr.
id()==ID_overflow_mult)
1210 if(op_type.id()==ID_signedbv)
1212 out <<
"(let (?prod (bvmul (sign_extend[" << width <<
"] ";
1214 out <<
") (sign_extend[" << width <<
"] ";
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 <<
"])))";
1223 else if(op_type.id()==ID_unsignedbv)
1225 out <<
"(bvuge (bvmul (zero_extend[" << width <<
"] ";
1227 out <<
") (zero_extend[" << width <<
"] ";
1229 out <<
")) bv" <<
power(2, width) <<
"[" << width*2 <<
"])";
1232 throw "overflow-* check on unknown type: "+op_type.id_string();
1234 else if(expr.
id()==ID_forall || expr.
id()==ID_exists)
1239 out <<
"(" << expr.
id() <<
" (";
1244 if(bound.
type().
id()==ID_bool)
1255 else if(expr.
id()==ID_extractbits)
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)
1275 throw "extractbits: to_integer failed";
1278 throw "extractbits: to_integer failed";
1280 out <<
"(extract[" << op1_i <<
":" << op2_i <<
"] ";
1295 throw "smt1 todo: extractbits with variable bits";
1299 throw "unsupported type for "+expr.
id_string()+
1300 ": "+op_type.id_string();
1302 else if(expr.
id()==ID_array)
1310 assert(!operands.empty());
1329 else if(expr.
id()==ID_vector)
1336 throw "smt1_convt::convert_expr: `"+
1348 if(dest_type.
id()==ID_c_enum_tag)
1352 if(src_type.
id()==ID_c_enum_tag)
1355 if(dest_type.
id()==ID_bool)
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)
1378 throw "TODO typecast1 "+src_type.
id_string()+
" -> bool";
1384 else if(dest_type.
id()==ID_c_bool)
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)
1403 out <<
" bv1[" << to_width <<
"]";
1404 out <<
" bv0[" << to_width <<
"]";
1410 throw "TODO typecast1 "+src_type.
id_string()+
" -> bool";
1413 else if(dest_type.
id()==ID_signedbv ||
1414 dest_type.
id()==ID_unsignedbv ||
1415 dest_type.
id()==ID_c_enum)
1419 if(src_type.
id()==ID_signedbv ||
1420 src_type.
id()==ID_unsignedbv ||
1421 src_type.
id()==ID_c_bool ||
1422 src_type.
id()==ID_c_enum)
1426 if(from_width==to_width)
1428 else if(from_width<to_width)
1430 if(src_type.
id()==ID_signedbv)
1431 out <<
"(sign_extend[";
1433 out <<
"(zero_extend[";
1435 out << (to_width-from_width)
1442 out <<
"(extract[" << (to_width-1) <<
":0] ";
1447 else if(src_type.
id()==ID_fixedbv)
1451 std::size_t from_width=fixedbv_src_type.
get_width();
1455 if(to_width>from_integer_bits)
1457 out <<
"(sign_extend[" << (to_width-from_integer_bits) <<
"] ";
1458 out <<
"(extract[" << (from_width-1) <<
":" 1459 << from_fraction_bits <<
"] ";
1465 out <<
"(extract[" << (from_fraction_bits+to_width-1)
1466 <<
":" << from_fraction_bits <<
"] ";
1471 else if(src_type.
id()==ID_bool)
1476 if(dest_type.
id()==ID_fixedbv)
1481 "bv0[" << spec.
width <<
"]";
1485 out <<
" bv1[" << to_width <<
"]";
1486 out <<
" bv0[" << to_width <<
"]";
1491 else if(src_type.
id()==ID_pointer)
1495 if(from_width<to_width)
1497 out <<
"(zero_extend[";
1498 out << (to_width-from_width)
1505 out <<
"(extract[" << (to_width-1) <<
":0] ";
1510 else if(src_type.
id()==ID_integer)
1513 if(src.is_constant())
1517 out <<
"bv" << i <<
"[" << to_width <<
"]";
1520 throw "can't convert non-constant integer to bitvector";
1522 else if(src_type.
id()==ID_c_bit_field)
1526 if(from_width==to_width)
1538 throw "TODO typecast2 "+src_type.
id_string()+
1542 else if(dest_type.
id()==ID_fixedbv)
1548 if(src_type.
id()==ID_unsignedbv ||
1549 src_type.
id()==ID_signedbv ||
1550 src_type.
id()==ID_c_enum)
1558 if(from_width==to_integer_bits)
1560 else if(from_width>to_integer_bits)
1563 out <<
" (extract[" << (to_integer_bits-1) <<
":0] ";
1570 assert(from_width<to_integer_bits);
1571 if(dest_type.
id()==ID_unsignedbv)
1573 out <<
" (zero_extend[" 1574 << (to_integer_bits-from_width) <<
"] ";
1580 out <<
" (sign_extend[" 1581 << (to_integer_bits-from_width) <<
"] ";
1587 out <<
" bv0[" << to_fraction_bits <<
"]";
1590 else if(src_type.
id()==ID_bool)
1593 out <<
"(concat (concat bv0[" << (to_integer_bits-1) <<
"]" 1597 out <<
" bv0[" << to_fraction_bits <<
"]";
1600 else if(src_type.
id()==ID_fixedbv)
1606 std::size_t from_width=from_fixedbv_type.
get_width();
1611 if(to_integer_bits<=from_integer_bits)
1614 << (from_fraction_bits+to_integer_bits-1) <<
":" 1615 << from_fraction_bits
1622 assert(to_integer_bits>from_integer_bits);
1623 out <<
"(sign_extend[" 1624 << (to_integer_bits-from_integer_bits)
1626 << (from_width-1) <<
":" 1627 << from_fraction_bits
1635 if(to_fraction_bits<=from_fraction_bits)
1638 << (from_fraction_bits-1) <<
":" 1639 << (from_fraction_bits-to_fraction_bits)
1646 assert(to_fraction_bits>from_fraction_bits);
1647 out <<
"(concat (extract[" 1648 << (from_fraction_bits-1) <<
":0] ";
1651 <<
" bv0[" << to_fraction_bits-from_fraction_bits
1658 throw "unexpected typecast to fixedbv";
1660 else if(dest_type.
id()==ID_pointer)
1664 if(src_type.
id()==ID_pointer)
1669 else if(src_type.
id()==ID_unsignedbv ||
1670 src_type.
id()==ID_signedbv)
1674 if(from_width==to_width)
1676 else if(from_width<to_width)
1678 out <<
"(zero_extend[" 1679 << (to_width-from_width)
1695 throw "TODO typecast3 "+src_type.
id_string()+
" -> pointer";
1697 else if(dest_type.
id()==ID_range)
1700 throw "TODO range typecast";
1702 else if(dest_type.
id()==ID_c_bit_field)
1707 if(from_width==to_width)
1718 throw "TODO typecast4 ? -> "+dest_type.
id_string();
1728 assert(components.size()==expr.
operands().size());
1730 assert(!components.empty());
1732 if(components.size()==1)
1736 if(op.
type().
id()==ID_array)
1743 std::size_t nr_ops=0;
1745 for(std::size_t i=0; i<components.size(); i++)
1746 if(expr.
operands()[i].type().id()!=ID_code)
1749 for(std::size_t i=1; i<nr_ops; i++)
1753 for(std::size_t i=0; i<components.size(); i++)
1757 if(op.
type().
id()!=ID_code)
1762 if(op.
type().
id()==ID_array)
1786 throw "failed to get union width for union";
1789 throw "failed to get union member width for union";
1791 if(total_width==member_width)
1796 assert(total_width>member_width);
1798 out <<
"bv0[" << (total_width-member_width) <<
"] ";
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)
1819 throw "failed to convert bitvector constant";
1824 value=
power(2, width)+value;
1826 out <<
"bv" << value
1827 <<
"[" << width <<
"]";
1829 else if(expr.
type().
id()==ID_fixedbv)
1836 out <<
"bv" << v <<
"[" << spec.
width <<
"]";
1838 else if(expr.
type().
id()==ID_floatbv)
1845 out <<
"bv" << v <<
"[" << spec.
width() <<
"]";
1847 else if(expr.
type().
id()==ID_pointer)
1862 throw "unknown pointer constant: "+
id2string(value);
1864 else if(expr.
type().
id()==ID_bool)
1867 out << (bool_as_bv?
"bit1":
"true");
1869 out << (bool_as_bv?
"bit0":
"false");
1871 throw "unknown boolean constant";
1873 else if(expr.
type().
id()==ID_array)
1878 else if(expr.
type().
id()==ID_rational)
1881 size_t pos=value.find(
"/");
1883 if(
pos==std::string::npos)
1884 out << value <<
".0";
1887 out <<
"(/ " << value.substr(0,
pos) <<
".0 " 1888 << value.substr(
pos+1) <<
".0)";
1891 else if(expr.
type().
id()==ID_integer ||
1892 expr.
type().
id()==ID_natural)
1897 out <<
"(~ " << value.substr(1) <<
")";
1909 if(expr.
type().
id()==ID_unsignedbv ||
1910 expr.
type().
id()==ID_signedbv)
1912 if(expr.
type().
id()==ID_unsignedbv)
1930 std::vector<std::size_t> dynamic_objects;
1934 assert(expr.
op0().
type().
id()==ID_pointer);
1940 if(dynamic_objects.empty())
1946 out <<
"(let (?obj (extract[" 1952 if(dynamic_objects.size()==1)
1954 out <<
"(= bv" << dynamic_objects.front()
1961 for(
const auto &obj : dynamic_objects)
1962 out <<
" (= bv" << obj
1986 if(op_type.id()==ID_unsignedbv ||
1987 op_type.id()==ID_pointer)
1989 if(expr.
id()==ID_le)
1991 else if(expr.
id()==ID_lt)
1993 else if(expr.
id()==ID_ge)
1995 else if(expr.
id()==ID_gt)
2003 else if(op_type.id()==ID_signedbv ||
2004 op_type.id()==ID_fixedbv)
2006 if(expr.
id()==ID_le)
2008 else if(expr.
id()==ID_lt)
2010 else if(expr.
id()==ID_ge)
2012 else if(expr.
id()==ID_gt)
2020 else if(op_type.id()==ID_rational ||
2021 op_type.id()==ID_integer)
2031 throw "unsupported type for "+expr.
id_string()+
2032 ": "+op_type.id_string();
2044 if(expr.
type().
id()==ID_unsignedbv ||
2045 expr.
type().
id()==ID_signedbv ||
2046 expr.
type().
id()==ID_fixedbv)
2050 else if(expr.
type().
id()==ID_pointer)
2053 throw "pointer arithmetic with less than two operands";
2059 if(p.
type().
id()!=ID_pointer)
2062 if(p.
type().
id()!=ID_pointer)
2063 throw "unexpected mixture in pointer arithmetic";
2067 assert(element_size>0);
2081 out <<
" bv" << element_size
2094 exprt integer_sum(ID_plus, integer_type);
2098 if(it->type().id()==ID_pointer)
2105 if(it->type()!=integer_type)
2106 it->make_typecast(integer_type);
2112 else if(expr.
type().
id()==ID_rational ||
2113 expr.
type().
id()==ID_integer)
2124 assert(expr.
type().
id()==ID_floatbv);
2126 throw "todo: floatbv_plus";
2133 if(expr.
type().
id()==ID_unsignedbv ||
2134 expr.
type().
id()==ID_signedbv ||
2135 expr.
type().
id()==ID_fixedbv)
2155 else if(expr.
type().
id()==ID_pointer)
2171 assert(expr.
type().
id()==ID_floatbv);
2173 throw "todo: floatbv_minus";
2180 if(expr.
type().
id()==ID_unsignedbv ||
2181 expr.
type().
id()==ID_signedbv)
2183 if(expr.
type().
id()==ID_unsignedbv)
2193 else if(expr.
type().
id()==ID_fixedbv)
2198 out <<
"(extract[" << spec.
width-1 <<
":0] ";
2203 out <<
" bv0[" << fraction_bits <<
"]) ";
2205 out <<
"(sign_extend[" << fraction_bits <<
"] ";
2218 assert(expr.
type().
id()==ID_floatbv);
2220 throw "todo: floatbv_div";
2240 if(expr.
type().
id()==ID_unsignedbv ||
2241 expr.
type().
id()==ID_signedbv)
2252 else if(expr.
type().
id()==ID_fixedbv)
2258 out <<
"(extract[" << spec.
width+fraction_bits-1 <<
":" 2259 << fraction_bits <<
"] ";
2263 out <<
"(sign_extend[" << fraction_bits <<
"] ";
2267 out <<
"(sign_extend[" << fraction_bits <<
"] ";
2274 else if(expr.
type().
id()==ID_rational)
2289 assert(expr.
type().
id()==ID_floatbv);
2291 throw "todo: floatbv_mult";
2302 std::size_t s=expr.
operands().size();
2309 assert(new_with_expr.
operands().size()==3);
2311 new_with_expr.
old()=tmp;
2321 if(expr_type.
id()==ID_array)
2325 if(array.
id()==ID_member)
2341 throw "failed to get struct width";
2345 if(struct_op_type.
id()==ID_struct)
2348 else if(struct_op_type.
id()==ID_union)
2351 throw "failed to get offset";
2356 throw "failed to get struct member width";
2361 throw "failed to get struct width";
2363 std::size_t array_bits=(offset+width) - offset;
2374 out <<
"(extract[" << offset+width-1 <<
":" << offset <<
"] ";
2379 out <<
" (bvnot (bvshl";
2382 out <<
" (repeat[" << array_bits-elem_width <<
"] bv0[1])";
2383 out <<
" (repeat[" << elem_width <<
"] bv1[1])";
2390 out <<
" (extract[" << width-1 <<
":0]";
2399 out <<
" (bvshl (zero_extend[" << array_bits-elem_width <<
"] ";
2407 out <<
" (extract[" << width-1 <<
":0]";
2415 else if(array.
id()==ID_index)
2427 throw "failed to get width of 2nd dimension array";
2432 throw "failed to get array element width";
2446 out <<
" (bvnot (bvshl";
2449 out <<
" (repeat[" << width-elem_width <<
"] bv0[1])";
2450 out <<
" (repeat[" << elem_width <<
"] bv1[1])";
2457 out <<
" (extract[" << width-1 <<
":0]";
2466 out <<
" (bvshl (zero_extend[" << width-elem_width <<
"] ";
2473 out <<
" (extract[" << width-1 <<
":0]";
2497 else if(expr_type.
id()==ID_struct)
2507 throw "failed to get struct width for with";
2512 throw "failed to get member width for with";
2515 struct_type, index.
get(ID_component_name)).offset;
2517 if(total_width==width)
2521 if(offset+width!=total_width)
2524 out <<
" (extract[" << (total_width-1) <<
":" << (offset+width) <<
"] ";
2537 out <<
" (extract[" << (offset-1) <<
":0] ";
2543 if(offset+width!=total_width)
2547 else if(expr_type.
id()==ID_union)
2556 throw "failed to get union width for with";
2561 throw "failed to get union member width for with";
2563 if(total_width==member_width)
2567 assert(total_width>member_width);
2571 <<
":" << member_width <<
"] ";
2578 else if(expr_type.
id()==ID_bv ||
2579 expr_type.
id()==ID_unsignedbv ||
2580 expr_type.
id()==ID_signedbv)
2587 throw "failed to get total width";
2596 throw "failed to get value width";
2604 out <<
" (bvnot (bvshl";
2607 out <<
" (repeat[" << total_width-value_width <<
"] bv0[1])";
2608 out <<
" (repeat[" << value_width <<
"] bv1[1])";
2629 throw "with expects struct, union, or array type, " 2639 throw "smt1_convt::convert_update to be implemented";
2646 if(expr.
array().
id()==ID_member ||
2657 throw "failed to get array width";
2662 throw "failed to get struct width";
2664 out <<
"(extract[" << elem_width-1 <<
":0] ";
2670 out <<
" (extract[" << width-1 <<
":0]";
2698 const exprt &struct_op=member_expr.struct_op();
2700 const irep_idt &name=member_expr.get_component_name();
2705 if(struct_op_type.
id()==ID_struct)
2713 throw "failed to get struct member width";
2723 else if(struct_op_type.
id()==ID_union)
2728 throw "failed to get union member width";
2749 if(expr.
id()==ID_and && value)
2756 if(expr.
id()==ID_not)
2771 out <<
":assumption ; set_to " 2772 << (value?
"true":
"false") <<
"\n" 2775 assert(expr.
type().
id()==ID_bool);
2794 if(expr.
id()==ID_forall || expr.
id()==ID_exists)
2797 assert(expr.
op0().
id()==ID_symbol);
2808 if(expr.
id()==ID_symbol ||
2809 expr.
id()==ID_nondet_symbol)
2812 if(type.
id()==ID_code)
2817 if(expr.
id()==ID_symbol)
2820 identifier=
"nondet_"+expr.
get_string(ID_identifier);
2831 if(
id.type.
id()==ID_bool)
2833 out <<
":extrapreds((" 2839 out <<
":extrafuns((" 2843 out <<
"))" <<
"\n";
2847 else if(expr.
id()==ID_array_of)
2852 out <<
"; the following is a poor substitute for lambda i. x" <<
"\n";
2853 out <<
":extrafuns((" 2857 out <<
"))" <<
"\n";
2862 expr.
op0().
id()==ID_constant)
2872 out <<
":assumption (= (select " <<
id <<
" bv" 2883 else if(expr.
id()==ID_array)
2889 out <<
":extrafuns((" 2893 out <<
"))" <<
"\n";
2897 else if(expr.
id()==ID_string_constant)
2906 out <<
":extrafuns((" 2910 out <<
"))" <<
"\n";
2918 if(type.
id()==ID_array)
2927 throw "failed to get width of array subtype";
2929 out << width <<
"]";
2931 else if(type.
id()==ID_bool)
2935 else if(type.
id()==ID_struct ||
2936 type.
id()==ID_union)
2941 throw "failed to get width of struct/union";
2943 out <<
"BitVec[" << width <<
"]";
2945 else if(type.
id()==ID_pointer ||
2946 type.
id()==ID_reference)
2951 throw "failed to get width of pointer/reference";
2953 out <<
"BitVec[" << width <<
"]";
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)
2966 else if(type.
id()==ID_c_enum_tag)
2968 else if(type.
id()==ID_rational)
2970 else if(type.
id()==ID_integer)
2972 else if(type.
id()==ID_symbol)
2975 throw "unsupported type: "+type.
id_string();
2999 if(type.
id()==ID_bool && !bool_as_bv)
3006 if(type.
id()==ID_bool && !bool_as_bv)
3013 if(type.
id()==ID_bool && bool_as_bv)
3020 if(type.
id()==ID_bool && bool_as_bv)
3021 out <<
" bv1[1] bv0[1])";
3026 std::set<irep_idt> rec_stack;
3032 std::set<irep_idt> &recstack)
3034 if(type.
id()==ID_array)
3040 else if(type.
id()==ID_struct ||
3041 type.
id()==ID_union)
3046 for(
const auto &comp : components)
3049 else if(type.
id()==ID_code)
3054 for(
const auto ¶m : parameters)
3059 else if(type.
id()==ID_pointer)
3063 else if(type.
id()==ID_incomplete_array)
3067 else if(type.
id()==ID_symbol)
3072 if(recstack.find(
id)==recstack.end())
3074 recstack.insert(
id);
3082 const std::string &binary)
const 3089 throw "failed to get struct width";
3091 exprt e(ID_struct, type);
3092 e.
operands().resize(components.size());
3094 std::size_t index=binary.size();
3096 for(
const auto &comp : components)
3103 throw "failed to get component width";
3106 std::string cval=binary.substr(index, sub_size);
3116 const std::string &binary)
const 3121 throw "failed to get union width";
3127 std::size_t component_nr=0;
3134 const typet &sub_type=
ns.
follow(components[component_nr].type());
3136 assert(comp_width<=total_width);
3138 std::string cval=binary.substr(total_width-comp_width, comp_width);
3150 if(size.
id()!=ID_constant)
3151 throw "non-constant size array cannot be flattened";
3155 throw "array with non-constant size";
3160 throw "failed to get width of array subtype";
3163 out <<
" (let (?fbv ";
3196 std::size_t num_ops=expr.
operands().size();
3204 exprt::operandst::const_iterator it=
3207 for(std::size_t i=0; i<num_ops-1; ++i, ++it)
3209 out <<
"(" << op_string <<
" ";
3218 out << std::string(num_ops-1,
')');
const irept & get_nil_irep()
The type of an expression.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
std::size_t get_null_object() const
virtual void set_to(const exprt &expr, bool value)
const typet & follow(const typet &src) const
Fixed-width bit-vector with unsigned binary interpretation.
void convert_overflow(const exprt &expr)
std::size_t get_fraction_bits() const
pointer_logict pointer_logic
const std::string & id2string(const irep_idt &d)
void convert_type(const typet &type)
pointer_typet pointer_type(const typet &subtype)
void convert_mult(const mult_exprt &expr)
void convert_minus(const minus_exprt &expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
const minus_exprt & to_minus_expr(const exprt &expr)
Cast a generic exprt to a minus_exprt.
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)
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
std::size_t get_integer_bits() const
void copy_to_operands(const exprt &expr)
const irep_idt & get_identifier() const
#define forall_expr(it, expr)
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
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
std::vector< parametert > parameterst
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
const componentst & components() const
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...
void convert_floatbv_minus(const exprt &expr)
void get_dynamic_objects(std::vector< std::size_t > &objects) const
A constant literal expression.
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
void convert_byte_extract(const byte_extract_exprt &expr, bool bool_as_bv)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
virtual void print_assignment(std::ostream &out) const
void set_component_number(std::size_t component_number)
void find_symbols(const exprt &expr)
std::size_t get_invalid_object() const
Extract member of struct or union.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
identifier_mapt identifier_map
const typet & follow_tag(const union_tag_typet &src) const
virtual resultt dec_solve()
void convert_byte_update(const exprt &expr, bool bool_as_bv)
const irep_idt & id() const
void convert_div(const div_exprt &expr)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
const membert & get_member(const struct_typet &type, const irep_idt &member) const
void convert_union(const exprt &expr)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Expression classes for byte-level operators.
The boolean constant true.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
division (integer and real)
virtual literalt convert(const exprt &expr)
A reference into the symbol table.
A generic base class for binary expressions.
void convert_update(const exprt &expr)
void convert_index(const index_exprt &expr, bool bool_as_bv)
std::size_t get_fraction_bits() const
Fixed-width bit-vector with two's complement interpretation.
typet array_index_type() const
union constructor from single element
API to expression classes.
unsigned array_index_bits
const irep_idt & get(const irep_namet &name) const
boolbv_widtht boolbv_width
unsigned no_boolean_variables
const exprt & size() const
#define forall_operands(it, expr)
string2array_mapt string2array_map
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
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.
void convert_struct(const exprt &expr)
bitvector_typet index_type()
std::vector< bool > boolean_assignment
Operator to return the address of an object.
The unary minus expression.
void convert_plus(const plus_exprt &expr)
void convert_floatbv_plus(const exprt &expr)
virtual tvt l_get(literalt) const
Fixed-width bit-vector with signed fixed-point interpretation.
The boolean constant false.
std::size_t get_width() const
exprt pointer_expr(const pointert &pointer, const typet &type) const
void from_bool_end(const typet &type, bool bool_as_bv)
std::vector< exprt > operandst
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
void from_bv_begin(const typet &type, bool bool_as_bv)
void convert_member(const member_exprt &expr, bool bool_as_bv)
void from_bool_begin(const typet &type, bool bool_as_bv)
array_of_mapt array_of_map
unsigned integer2unsigned(const mp_integer &n)
virtual exprt get(const exprt &expr) const
literalt const_literal(bool value)
void convert_floatbv_mult(const exprt &expr)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
void convert_typecast(const typecast_exprt &expr, bool bool_as_bv)
void convert_constant(const constant_exprt &expr, bool bool_as_bv)
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
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
literalt get_literal() const
Base class for all expressions.
void convert_nary(const exprt &expr, const irep_idt op_string, bool bool_as_bv)
const exprt & struct_op() const
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void convert_literal(const literalt l)
void flatten_array(const exprt &op)
Operator to update elements in structs and arrays.
void convert_with(const exprt &expr)
irep_idt get_component_name() const
const plus_exprt & to_plus_expr(const exprt &expr)
Cast a generic exprt to a plus_exprt.
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
const mult_exprt & to_mult_expr(const exprt &expr)
Cast a generic exprt to a mult_exprt.
const std::string & get_string(const irep_namet &name) const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const std::string & id_string() const
void convert_relation(const exprt &expr, bool bool_as_bv)
#define Forall_operands(it, expr)
void convert_floatbv_div(const exprt &expr)
void set_component_name(const irep_idt &component_name)
exprt binary2struct(const struct_typet &type, const std::string &binary) const
void convert_mod(const mod_exprt &expr)
std::size_t width() const
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
const typet & subtype() const
exprt binary2union(const union_typet &type, const std::string &binary) const
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
std::size_t add_object(const exprt &expr)
const irept & find(const irep_namet &name) const
const irep_idt & get_identifier() const
void convert_is_dynamic_object(const exprt &expr, bool bool_as_bv)
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
void from_bv_end(const typet &type, bool bool_as_bv)
void set(const irep_namet &name, const irep_idt &value)
array_expr_mapt array_expr_map
void set_width(std::size_t width)
std::string convert_identifier(const irep_idt &identifier)
void array_index(const exprt &expr)
std::set< irep_idt > quantified_symbols
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.