44 if(type.
id() == ID_struct_tag)
46 else if(type.
id() == ID_struct)
57 const typet &type,
const std::string &tag)
67 if(type.
id()==ID_pointer)
98 if(type.
id()==ID_pointer)
121 if(type.
id()==ID_pointer)
144 if(type.
id()==ID_pointer)
167 if(type.
id()==ID_pointer)
193 std::vector<irep_idt> bases;
199 class_name ==
"java.lang.StringBuilder" ||
200 class_name ==
"java.lang.StringBuffer")
201 bases.push_back(
"java.lang.AbstractStringBuilder");
203 bases.push_back(
"java.lang.Object");
206 if(class_name !=
"java.lang.CharSequence")
208 bases.push_back(
"java.io.Serializable");
209 bases.push_back(
"java.lang.CharSequence");
211 if(class_name ==
"java.lang.String")
212 bases.push_back(
"java.lang.Comparable");
226 symbolt *string_symbol =
nullptr;
227 bool already_exists = symbol_table.
move(tmp_string_symbol, string_symbol);
241 new_string_type.
set_tag(class_name);
242 new_string_type.
set_name(class_symbol_name);
246 for(
const irep_idt &base_name : bases)
252 string_symbol->
type = new_string_type;
257 string_type.components().resize(3);
261 string_type.components()[0].set_name(supertype_component_name);
262 string_type.components()[0].set_pretty_name(supertype_component_name);
263 string_type.components()[0].type() = supertype;
264 string_type.components()[1].set_name(
"length");
265 string_type.components()[1].set_pretty_name(
"length");
267 string_type.components()[2].set_name(
"data");
268 string_type.components()[2].set_pretty_name(
"data");
288 for(
const auto &p : params)
289 ops.emplace_back(
symbol_exprt(p.get_identifier(), p.type()));
310 const exprt &expr_to_process,
320 string_expr, expr_to_process, loc, symbol_table, init_code);
345 for(
const auto &p : operands)
352 p, loc, symbol_table, function_id, init_code));
371 if(type.
id() == ID_struct_tag)
391 if(type.
id() == ID_struct_tag)
432 const exprt &array_pointer,
443 array_data.
type(),
"char_array", loc, function_id, symbol_table);
456 string_expr.
content(), inf_array, symbol_table, loc, function_id, code);
494 index_type,
"cprover_string_length", loc, function_id, symbol_table);
498 array_type,
"cprover_string_content", loc, function_id, symbol_table);
525 const exprt nondet_array_expr =
532 array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
535 nondet_array_expr, str.
length(), symbol_table, loc, function_id, code);
587 function_id, arguments, lhs.
type(), symbol_table));
625 "nondet_infinite_array_pointer",
636 return std::move(
data);
648 const exprt &pointer,
658 java_int_type(),
"return_array", loc, function_id, symbol_table);
664 ID_cprover_associate_array_to_pointer_func,
687 java_int_type(),
"return_array", loc, function_id, symbol_table);
693 ID_cprover_associate_length_to_array_func,
711 const exprt &pointer,
721 java_int_type(),
"cnstr_added", loc, function_id, symbol_table);
728 ID_cprover_string_constrain_characters_func,
729 {length, pointer, char_set_expr},
760 std::string(
"return_code_") + function_id.
c_str(),
764 const auto return_code = return_code_sym.
symbol_expr();
765 code.
add(code_declt(return_code), loc);
767 const refined_string_exprt string_expr =
772 args.push_back(string_expr.
length());
773 args.push_back(string_expr.
content());
774 args.insert(args.end(), arguments.begin(), arguments.end());
779 return_code, function_id, args, symbol_table),
799 const exprt &rhs_array,
800 const exprt &rhs_length,
810 namespacet ns(symbol_table);
811 const struct_typet &lhs_type =
814 lhs_type.
components().front().type(), source_locationt{}, ns);
817 struct_exprt struct_rhs(
818 {zero_base_object, rhs_length, rhs_array}, deref.
type());
824 {code_assignt(
get_length(deref, symbol_table), rhs_length),
825 code_assignt(
get_data(deref, symbol_table), rhs_array)});
873 auto rhs_length = if_exprt(
877 rhs_length.
set(ID_mode, ID_java);
880 code.
add(code_assignt(lhs.
length(), rhs_length), loc);
881 exprt data_as_array =
get_data(deref, symbol_table);
882 code.
add(code_assignt{lhs.
content(), std::move(data_as_array)}, loc);
897 const std::string &s,
903 ID_cprover_string_literal_func,
904 {constant_exprt{s, string_typet{}}},
924 (void)message_handler;
930 const symbol_exprt arg(params[0].get_identifier(), params[0].type());
937 type.
return_type(), loc, function_id, symbol_table, code);
941 ieee_float_valuet zero_float(float_spec);
942 zero_float.from_float(0.0);
943 const constant_exprt zero = zero_float.to_expr();
946 std::vector<exprt> condition_list;
947 std::vector<refined_string_exprt> string_expr_list;
950 condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero));
952 ID_cprover_string_of_float_scientific_notation_func,
957 string_expr_list.push_back(sci_notation);
960 condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero));
961 const refined_string_exprt minus_sign =
964 ID_cprover_string_concat_func,
965 {minus_sign, sci_notation},
969 string_expr_list.push_back(neg_sci_notation);
972 condition_list.push_back(isnan_exprt(arg));
973 const refined_string_exprt nan =
975 string_expr_list.push_back(nan);
978 extractbit_exprt is_neg(arg, float_spec.
width()-1);
979 condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg)));
980 const refined_string_exprt infinity =
982 string_expr_list.push_back(infinity);
985 condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg));
986 const refined_string_exprt minus_infinity =
988 string_expr_list.push_back(minus_infinity);
993 condition_list.push_back(equal_exprt(arg, zero));
994 const refined_string_exprt zero_string =
996 string_expr_list.push_back(zero_string);
999 ieee_float_valuet minus_zero_float(float_spec);
1000 minus_zero_float.from_float(-0.0f);
1001 condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
1002 const refined_string_exprt minus_zero_string =
1004 string_expr_list.push_back(minus_zero_string);
1008 ieee_floatt bound_inf_float(float_spec, rm);
1009 ieee_floatt bound_sup_float(float_spec, rm);
1010 bound_inf_float.from_float(1e-3f);
1011 bound_sup_float.from_float(1e7f);
1012 bound_inf_float.change_spec(float_spec);
1013 bound_sup_float.change_spec(float_spec);
1014 const constant_exprt bound_inf = bound_inf_float.to_expr();
1015 const constant_exprt bound_sup = bound_sup_float.to_expr();
1017 const and_exprt is_simple_float{binary_relation_exprt(arg, ID_ge, bound_inf),
1018 binary_relation_exprt(arg, ID_lt, bound_sup)};
1019 condition_list.push_back(is_simple_float);
1022 ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
1023 string_expr_list.push_back(simple_notation);
1026 const and_exprt is_neg_simple_float{
1027 binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)),
1028 binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup))};
1029 condition_list.push_back(is_neg_simple_float);
1032 ID_cprover_string_concat_func,
1033 {minus_sign, simple_notation},
1037 string_expr_list.push_back(neg_simple_notation);
1041 string_expr_list.size()==condition_list.size(),
1042 "number of created strings should correspond to number of conditions");
1047 str, string_expr_list[0], symbol_table,
true);
1048 for(std::size_t i=1; i<condition_list.size(); i++)
1050 tmp_code = code_ifthenelset(
1053 str, string_expr_list[i], symbol_table,
true),
1056 code.
add(tmp_code, loc);
1059 code.
add(code_returnt(str), loc);
1090 const symbol_exprt
arg_this(params[0].get_identifier(), params[0].type());
1092 params.erase(params.begin());
1102 const refined_string_exprt string_expr =
1135 const symbol_exprt
arg_this(params[0].get_identifier(), params[0].type());
1156 function_id, type, loc, symbol_table,
false);
1181 const symbol_exprt obj(params[0].get_identifier(), params[0].type());
1187 const member_exprt class_identifier{
1192 ID_cprover_string_literal_func,
1201 ID_cprover_string_substring_func,
1208 const typet &string_ptr_type = type.
return_type();
1210 string_ptr_type, loc, function_id, symbol_table, code);
1213 string1, string_expr1, symbol_table,
true),
1217 code.
add(code_returnt{string1}, loc);
1242 function_id, args, type.
return_type(), symbol_table),
1275 const refined_string_exprt string_expr =
1280 type.
return_type(), loc, function_id, symbol_table, code);
1283 str, string_expr, symbol_table,
true),
1287 code.
add(code_returnt(str), loc);
1313 (void)message_handler;
1319 const refined_string_exprt string_expr =
1323 const java_method_typet::parametert &op = type.
parameters()[0];
1327 string_expr, arg0, loc, symbol_table, code);
1331 type.
return_type(), loc, function_id, symbol_table, code);
1334 str, string_expr, symbol_table,
true),
1338 code.
add(code_returnt(str), loc);
1363 (void)message_handler;
1368 const refined_string_exprt string_expr =
1375 const symbol_exprt arg1{params[1].get_identifier(), params[1].type()};
1383 arg_this, string_expr, symbol_table,
true),
1409 (void)message_handler;
1426 if(map->count(function_id) != 0)
1432template <
typename TMap,
typename TContainer>
1436 std::is_same<
typename TMap::key_type,
1437 typename TContainer::value_type>::value,
1438 "TContainer value_type doesn't match TMap key_type");
1442 std::inserter(container, container.begin()),
1443 [](
const typename TMap::value_type &pair) { return pair.first; });
1447 std::unordered_set<irep_idt> &methods)
const
1477 it_id->second, type, loc, symbol_table);
1482 it_id->second, type, loc, symbol_table);
1487 it_id->second, type, loc, symbol_table);
1492 it_id->second, type, loc, symbol_table);
1498 return it->second(type, loc, function_id, symbol_table, message_handler);
1513 string_types = std::unordered_set<irep_idt>{
"java.lang.String",
1514 "java.lang.StringBuilder",
1515 "java.lang.CharSequence",
1516 "java.lang.StringBuffer"};
1531 [
"java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1532 "lang/CharSequence;II)"
1533 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1537 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"] =
1538 ID_cprover_string_char_at_func;
1540 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1541 ID_cprover_string_char_at_func;
1543 [
"java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1544 ID_cprover_string_code_point_at_func;
1546 [
"java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1547 ID_cprover_string_code_point_before_func;
1549 [
"java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1550 ID_cprover_string_code_point_count_func;
1552 [
"java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1553 "lang/StringBuffer;"] = ID_cprover_string_delete_func;
1555 [
"java::org.cprover.CProverString.delete:(Ljava/lang/"
1556 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
1557 ID_cprover_string_delete_func;
1559 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1560 "StringBuffer;I)Ljava/lang/StringBuffer;"] =
1561 ID_cprover_string_delete_char_at_func;
1563 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1564 "StringBuilder;I)Ljava/lang/StringBuilder;"] =
1565 ID_cprover_string_delete_char_at_func;
1567 std::string format_signature =
"java::org.cprover.CProverString.format:(";
1569 format_signature +=
"Ljava/lang/String;";
1570 format_signature +=
")Ljava/lang/String;";
1572 ID_cprover_string_format_func;
1575 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1576 "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
1578 [
"java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1579 "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
1581 [
"java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1582 "StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
1584 [
"java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1585 "StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
1587 [
"java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
1588 ID_cprover_string_set_length_func;
1590 [
"java::org.cprover.CProverString.setLength:(Ljava/lang/"
1591 "StringBuilder;I)V"] = ID_cprover_string_set_length_func;
1593 [
"java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1594 "lang/CharSequence;"] = ID_cprover_string_substring_func;
1598 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1599 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1601 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1602 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1604 [
"java::org.cprover.CProverString.substring:(Ljava/Lang/"
1605 "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
1607 [
"java::org.cprover.CProverString.toString:(I)Ljava/lang/String;"] =
1608 ID_cprover_string_of_int_func;
1610 [
"java::org.cprover.CProverString.toString:(II)Ljava/lang/String;"] =
1611 ID_cprover_string_of_int_func;
1613 [
"java::org.cprover.CProverString.toString:(J)Ljava/lang/String;"] =
1614 ID_cprover_string_of_long_func;
1616 [
"java::org.cprover.CProverString.toString:(JI)Ljava/lang/String;"] =
1617 ID_cprover_string_of_long_func;
1619 [
"java::org.cprover.CProverString.toString:(F)Ljava/lang/String;"] =
1623 std::placeholders::_1,
1624 std::placeholders::_2,
1625 std::placeholders::_3,
1626 std::placeholders::_4,
1627 std::placeholders::_5);
1629 [
"java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
1630 ID_cprover_string_parse_int_func;
1632 [
"java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
1633 ID_cprover_string_parse_int_func;
1635 [
"java::org.cprover.CProverString.isValidInt:(Ljava/lang/String;I)Z"] =
1636 ID_cprover_string_is_valid_int_func;
1638 [
"java::org.cprover.CProverString.isValidLong:(Ljava/lang/String;I)Z"] =
1639 ID_cprover_string_is_valid_long_func;
1646 std::placeholders::_1,
1647 std::placeholders::_2,
1648 std::placeholders::_3,
1649 std::placeholders::_4,
1650 std::placeholders::_5);
1652 [
"java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1655 std::placeholders::_1,
1656 std::placeholders::_2,
1657 std::placeholders::_3,
1658 std::placeholders::_4,
1659 std::placeholders::_5);
1661 [
"java::java.lang.String.<init>:()V"]=
1662 ID_cprover_string_empty_string_func;
1665 [
"java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1666 ID_cprover_string_compare_to_func;
1668 [
"java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1669 ID_cprover_string_concat_func;
1671 [
"java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1672 ID_cprover_string_contains_func;
1674 [
"java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1675 ID_cprover_string_endswith_func;
1677 [
"java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1678 ID_cprover_string_equals_ignore_case_func;
1681 [
"java::java.lang.String.indexOf:(I)I"]=
1682 ID_cprover_string_index_of_func;
1684 [
"java::java.lang.String.indexOf:(II)I"]=
1685 ID_cprover_string_index_of_func;
1687 [
"java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1688 ID_cprover_string_index_of_func;
1690 [
"java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1691 ID_cprover_string_index_of_func;
1693 [
"java::java.lang.String.isEmpty:()Z"]=
1694 ID_cprover_string_is_empty_func;
1696 [
"java::java.lang.String.lastIndexOf:(I)I"]=
1697 ID_cprover_string_last_index_of_func;
1699 [
"java::java.lang.String.lastIndexOf:(II)I"]=
1700 ID_cprover_string_last_index_of_func;
1702 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1703 ID_cprover_string_last_index_of_func;
1705 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1706 ID_cprover_string_last_index_of_func;
1710 std::placeholders::_1,
1711 std::placeholders::_2,
1712 std::placeholders::_3,
1713 std::placeholders::_4,
1714 std::placeholders::_5);
1716 [
"java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1717 ID_cprover_string_replace_func;
1719 [
"java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]=
1720 ID_cprover_string_replace_func;
1722 [
"java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1723 ID_cprover_string_startswith_func;
1725 [
"java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1726 ID_cprover_string_startswith_func;
1728 [
"java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1729 ID_cprover_string_to_lower_case_func;
1734 std::placeholders::_1,
1735 std::placeholders::_2,
1736 std::placeholders::_3,
1737 std::placeholders::_4,
1738 std::placeholders::_5);
1740 [
"java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
1741 ID_cprover_string_to_upper_case_func;
1743 [
"java::java.lang.String.trim:()Ljava/lang/String;"]=
1744 ID_cprover_string_trim_func;
1748 [
"java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
1751 std::placeholders::_1,
1752 std::placeholders::_2,
1753 std::placeholders::_3,
1754 std::placeholders::_4,
1755 std::placeholders::_5);
1757 [
"java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
1761 std::placeholders::_1,
1762 std::placeholders::_2,
1763 std::placeholders::_3,
1764 std::placeholders::_4,
1765 std::placeholders::_5);
1767 [
"java::java.lang.StringBuilder.<init>:()V"]=
1768 ID_cprover_string_empty_string_func;
1770 [
"java::java.lang.StringBuilder.<init>:(I)V"] =
1771 ID_cprover_string_empty_string_func;
1774 [
"java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1775 ID_cprover_string_concat_char_func;
1777 [
"java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1778 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1780 [
"java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1781 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1783 [
"java::java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1784 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1786 [
"java::java.lang.StringBuilder.appendCodePoint:(I)"
1787 "Ljava/lang/StringBuilder;"]=
1788 ID_cprover_string_concat_code_point_func;
1790 [
"java::java.lang.StringBuilder.charAt:(I)C"]=
1791 ID_cprover_string_char_at_func;
1793 [
"java::java.lang.StringBuilder.codePointAt:(I)I"]=
1794 ID_cprover_string_code_point_at_func;
1796 [
"java::java.lang.StringBuilder.codePointBefore:(I)I"]=
1797 ID_cprover_string_code_point_before_func;
1799 [
"java::java.lang.StringBuilder.codePointCount:(II)I"]=
1800 ID_cprover_string_code_point_count_func;
1804 std::placeholders::_1,
1805 std::placeholders::_2,
1806 std::placeholders::_3,
1807 std::placeholders::_4,
1808 std::placeholders::_5);
1810 [
"java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1811 ID_cprover_string_substring_func;
1813 [
"java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1814 ID_cprover_string_substring_func;
1816 [
"java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
1819 std::placeholders::_1,
1820 std::placeholders::_2,
1821 std::placeholders::_3,
1822 std::placeholders::_4,
1823 std::placeholders::_5);
1827 [
"java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
1830 std::placeholders::_1,
1831 std::placeholders::_2,
1832 std::placeholders::_3,
1833 std::placeholders::_4,
1834 std::placeholders::_5);
1836 [
"java::java.lang.StringBuffer.<init>:()V"]=
1837 ID_cprover_string_empty_string_func;
1840 [
"java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
1841 ID_cprover_string_concat_char_func;
1843 [
"java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
1844 "Ljava/lang/StringBuffer;"]=
1845 ID_cprover_string_concat_func;
1847 [
"java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1848 "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
1850 [
"java::java.lang.StringBuffer.appendCodePoint:(I)"
1851 "Ljava/lang/StringBuffer;"]=
1852 ID_cprover_string_concat_code_point_func;
1854 [
"java::java.lang.StringBuffer.codePointAt:(I)I"]=
1855 ID_cprover_string_code_point_at_func;
1857 [
"java::java.lang.StringBuffer.codePointBefore:(I)I"]=
1858 ID_cprover_string_code_point_before_func;
1860 [
"java::java.lang.StringBuffer.codePointCount:(II)I"]=
1861 ID_cprover_string_code_point_count_func;
1863 [
"java::java.lang.StringBuffer.length:()I"]=
1866 [
"java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
1867 ID_cprover_string_substring_func;
1869 [
"java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
1872 std::placeholders::_1,
1873 std::placeholders::_2,
1874 std::placeholders::_3,
1875 std::placeholders::_4,
1876 std::placeholders::_5);
1880 [
"java::java.lang.CharSequence.charAt:(I)C"]=
1881 ID_cprover_string_char_at_func;
1883 [
"java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
1886 std::placeholders::_1,
1887 std::placeholders::_2,
1888 std::placeholders::_3,
1889 std::placeholders::_4,
1890 std::placeholders::_5);
1892 [
"java::java.lang.CharSequence.length:()I"]=
1897 [
"java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1898 ID_cprover_string_of_int_hex_func;
1900 [
"java::org.cprover.CProver.classIdentifier:("
1901 "Ljava/lang/Object;)Ljava/lang/String;"] =
1905 std::placeholders::_1,
1906 std::placeholders::_2,
1907 std::placeholders::_3,
1908 std::placeholders::_4,
1909 std::placeholders::_5);
code_frontend_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating an object of size size and assigning it to lhs
static std::pair< symbol_exprt, code_with_references_listt > nondet_length(allocate_objectst &allocate, source_locationt loc)
Declare a non-deterministic length expression.
API to expression classes for bitvectors.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
pointer_typet pointer_type(const typet &subtype)
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const struct_tag_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct.
Extract class identifier.
#define JAVA_CLASS_IDENTIFIER_FIELD_NAME
Operator to return the address of an object.
exprt allocate_dynamic_object(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generate the same code as allocate_dynamic_object_symbol, but return a dereference_exprt that derefer...
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
const exprt & size() const
A goto_instruction_codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
A codet representing sequential composition of program statements.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
void add(const codet &code)
A goto_instruction_codet representing the declaration of a local variable.
goto_instruction_codet representation of a "return from afunction" statement.
const irep_idt & get_identifier() const
const parameterst & parameters() const
const typet & return_type() const
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
Operator to dereference a pointer.
const char * c_str() const
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
source_locationt & add_source_location()
std::size_t width() const
An expression denoting infinity.
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
const componentst & components() const
void set_name(const irep_idt &name)
Set the name of the struct, which can be used to look up its symbol in the symbol table.
void set_access(const irep_idt &access)
std::vector< parametert > parameterst
code_blockt make_float_to_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
std::unordered_map< irep_idt, irep_idt > id_mapt
code_blockt make_string_returning_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
code_returnt make_string_length_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Generates code for the String.length method.
const refined_string_typet refined_string_type
refined_string_exprt string_literal_to_string_expr(const std::string &s, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
codet code_assign_components_to_java_string(const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table, bool is_constructor)
refined_string_exprt convert_exprt_to_string_exprt(const exprt &deref, const source_locationt &loc, symbol_table_baset &symbol_table, const irep_idt &function_name, code_blockt &init_code)
Creates a string_exprt from the input exprt representing a char sequence.
id_mapt cprover_equivalent_to_java_string_returning_function
code_blockt make_assign_and_return_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
static bool implements_java_char_sequence_pointer(const typet &type)
id_mapt cprover_equivalent_to_java_assign_and_return_function
std::unordered_map< irep_idt, conversion_functiont > conversion_table
refined_string_exprt string_expr_of_function(const irep_idt &function_id, const exprt::operandst &arguments, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
code_blockt make_class_identifier_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
static bool is_java_char_sequence_type(const typet &type)
static bool is_java_string_buffer_type(const typet &type)
bool implements_function(const irep_idt &function_id) const
code_blockt make_copy_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
std::vector< irep_idt > get_string_type_base_classes(const irep_idt &class_name)
Gets the base classes for known String and String-related types, or returns an empty list for other t...
static bool is_java_char_array_pointer_type(const typet &type)
id_mapt cprover_equivalent_to_java_function
refined_string_exprt make_nondet_string_expr(const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
add symbols with prefix cprover_string_length and cprover_string_data and construct a string_expr fro...
code_blockt make_assign_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
void add_string_type(const irep_idt &class_name, symbol_table_baset &symbol_table)
Add to the symbol table type declaration for a String-like Java class.
exprt allocate_fresh_string(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
declare a new String and allocate it
static bool is_java_string_pointer_type(const typet &type)
refined_string_exprt replace_char_array(const exprt &array_pointer, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &code)
we declare a new cprover_string whose contents is deduced from the char array.
static bool is_java_string_builder_pointer_type(const typet &type)
exprt::operandst process_parameters(const java_method_typet::parameterst ¶ms, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code)
calls string_refine_preprocesst::process_operands with a list of parameters.
static bool is_java_char_sequence_pointer_type(const typet &type)
id_mapt cprover_equivalent_to_java_constructor
static bool is_java_char_array_type(const typet &type)
code_blockt make_init_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool is_constructor=true)
character_refine_preprocesst character_preprocess
static bool is_java_string_builder_type(const typet &type)
code_blockt make_function_from_call(const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
std::unordered_set< irep_idt > string_types
codet code_assign_string_expr_to_java_string(const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table, bool is_constructor)
static bool is_java_string_buffer_pointer_type(const typet &type)
codet code_return_function_application(const irep_idt &function_id, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
return the result of a function call
symbol_exprt fresh_string(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
add a symbol with static lifetime and name containing cprover_string and given type
code_blockt make_copy_constructor_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
id_mapt cprover_equivalent_to_java_assign_function
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
exprt::operandst process_operands(const exprt::operandst &operands, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code)
for each expression that is of a type implementing strings, we declare a new cprover_string whose con...
static bool is_java_string_type(const typet &type)
const std::array< id_mapt *, 5 > id_maps
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler)
Should be called to provide code for string functions that are used in the code but for which no impl...
static bool java_type_matches_tag(const typet &type, const std::string &tag)
void initialize_known_type_table()
refined_string_exprt decl_string_expr(const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
Add declaration of a refined string expr whose content and length are fresh symbols.
void code_assign_java_string_to_string_expr(const refined_string_exprt &lhs, const exprt &rhs, const source_locationt &loc, const symbol_table_baset &symbol_table, code_blockt &code)
Extract member of struct or union.
The null pointer constant.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
const exprt & length() const
const exprt & content() const
A side_effect_exprt that returns a non-deterministically chosen value.
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
void add_base(const struct_tag_typet &base)
Add a base class/struct.
const typet & component_type(const irep_idt &component_name) const
void set_tag(const irep_idt &tag)
const componentst & components() const
Expression to hold a symbol (variable)
The symbol table base class interface.
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
const irep_idt & get_identifier() const
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
The type of an expression, extends irept.
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
API to expression classes for floating-point arithmetic.
const std::string & id2string(const irep_idt &d)
static bool is_constructor(const irep_idt &method_name)
return copy_constructor_body
static irep_idt get_tag(const typet &type)
static typet string_length_type()
void add_keys_to_container(const TMap &map, TContainer &container)
void add_character_set_constraint(const exprt &pointer, const exprt &length, const irep_idt &char_range, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver which ensures all characters belong to the character s...
static codet code_assign_function_application(const exprt &lhs, const irep_idt &function_id, const exprt::operandst &arguments, symbol_table_baset &symbol_table)
assign the result of a function call
static const typet & get_data_type(const typet &type, const symbol_table_baset &symbol_table)
Finds the type of the data component.
void add_array_to_length_association(const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that the actual length of array is le...
static exprt get_data(const exprt &expr, const symbol_table_baset &symbol_table)
access data member
static exprt get_length(const exprt &expr, const symbol_table_baset &symbol_table)
access length member
exprt make_nondet_infinite_char_array(symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Declare a fresh symbol of type array of character with infinite size.
const symbol_exprt arg_this
Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primit...
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
static const typet & get_length_type(const typet &type, const symbol_table_baset &symbol_table)
Finds the type of the length component.
Produce code for simple implementation of String Java libraries.
void add_array_to_length_association(const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that the actual length of array is le...
exprt make_nondet_infinite_char_array(symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Declare a fresh symbol of type array of character with infinite size.
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
signedbv_typet java_int_type()
unsignedbv_typet java_char_type()
const java_method_typet & to_java_method_type(const typet &type)
const java_class_typet & to_java_class_type(const typet &type)
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
dereference_exprt checked_dereference(const exprt &expr)
Dereference an expression and flag it for a null-pointer check.
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &range, symbol_table_baset &symbol_table)
Create a (mathematical) function application expression.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Type for string expressions used by the string solver.
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
String expressions for the string solver.