41 if(type.
id() == ID_struct_tag)
43 else if(type.
id() == ID_struct)
54 const typet &type,
const std::string &tag)
64 if(type.
id()==ID_pointer)
95 if(type.
id()==ID_pointer)
118 if(type.
id()==ID_pointer)
141 if(type.
id()==ID_pointer)
164 if(type.
id()==ID_pointer)
183 std::vector<irep_idt>
190 std::vector<irep_idt> bases;
196 class_name ==
"java.lang.StringBuilder" ||
197 class_name ==
"java.lang.StringBuffer")
198 bases.push_back(
"java.lang.AbstractStringBuilder");
200 bases.push_back(
"java.lang.Object");
203 if(class_name !=
"java.lang.CharSequence")
205 bases.push_back(
"java.io.Serializable");
206 bases.push_back(
"java.lang.CharSequence");
208 if(class_name ==
"java.lang.String")
209 bases.push_back(
"java.lang.Comparable");
222 tmp_string_symbol.
name = class_symbol_name;
223 symbolt *string_symbol =
nullptr;
224 bool already_exists = symbol_table.
move(tmp_string_symbol, string_symbol);
238 new_string_type.
set_tag(class_name);
239 new_string_type.
set_name(class_symbol_name);
243 for(
const irep_idt &base_name : bases)
249 string_symbol->
type = new_string_type;
251 string_symbol->
mode = ID_java;
256 string_type.components().resize(3);
260 string_type.components()[0].set_name(supertype_component_name);
261 string_type.components()[0].set_pretty_name(supertype_component_name);
262 string_type.components()[0].type() = supertype;
263 string_type.components()[1].set_name(
"length");
264 string_type.components()[1].set_pretty_name(
"length");
266 string_type.components()[2].set_name(
"data");
267 string_type.components()[2].set_pretty_name(
"data");
287 for(
const auto &p : params)
288 ops.emplace_back(
symbol_exprt(p.get_identifier(), p.type()));
309 const exprt &expr_to_process,
319 string_expr, expr_to_process, loc, symbol_table, init_code);
344 for(
const auto &p : operands)
351 p, loc, symbol_table, function_id, init_code));
370 if(type.
id() == ID_struct_tag)
390 if(type.
id() == ID_struct_tag)
430 const exprt &array_pointer,
441 array_data.
type(),
"char_array", loc, function_id, symbol_table);
454 string_expr.
content(), inf_array, symbol_table, loc, function_id, code);
492 index_type,
"cprover_string_length", loc, function_id, symbol_table);
496 array_type,
"cprover_string_content", loc, function_id, symbol_table);
523 const exprt nondet_array_expr =
530 array_pointer, nondet_array_expr, symbol_table, loc, function_id, code);
533 nondet_array_expr, str.
length(), symbol_table, loc, function_id, code);
584 function_id, arguments, lhs.
type(), symbol_table));
622 "nondet_infinite_array_pointer",
633 return std::move(
data);
645 const exprt &pointer,
655 java_int_type(),
"return_array", loc, function_id, symbol_table);
661 ID_cprover_associate_array_to_pointer_func,
684 java_int_type(),
"return_array", loc, function_id, symbol_table);
690 ID_cprover_associate_length_to_array_func,
708 const exprt &pointer,
718 java_int_type(),
"cnstr_added", loc, function_id, symbol_table);
725 ID_cprover_string_constrain_characters_func,
726 {length, pointer, char_set_expr},
757 std::string(
"return_code_") + function_id.
c_str(),
761 const auto return_code = return_code_sym.
symbol_expr();
769 args.push_back(string_expr.
length());
770 args.push_back(string_expr.
content());
771 args.insert(args.end(), arguments.begin(), arguments.end());
776 return_code, function_id, args, symbol_table),
796 const exprt &rhs_array,
797 const exprt &rhs_length,
814 {zero_base_object, rhs_length, rhs_array}, deref.
type());
873 rhs_length.set(ID_mode, ID_java);
893 const std::string &s,
899 ID_cprover_string_literal_func,
922 const symbol_exprt arg(params[0].get_identifier(), params[0].type());
929 type.
return_type(), loc, function_id, symbol_table, code);
938 std::vector<exprt> condition_list;
939 std::vector<refined_string_exprt> string_expr_list;
944 ID_cprover_string_of_float_scientific_notation_func,
949 string_expr_list.push_back(sci_notation);
956 ID_cprover_string_concat_func,
957 {minus_sign, sci_notation},
961 string_expr_list.push_back(neg_sci_notation);
967 string_expr_list.push_back(nan);
974 string_expr_list.push_back(infinity);
980 string_expr_list.push_back(minus_infinity);
988 string_expr_list.push_back(zero_string);
996 string_expr_list.push_back(minus_zero_string);
1010 condition_list.push_back(is_simple_float);
1013 ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
1014 string_expr_list.push_back(simple_notation);
1020 condition_list.push_back(is_neg_simple_float);
1023 ID_cprover_string_concat_func,
1024 {minus_sign, simple_notation},
1028 string_expr_list.push_back(neg_simple_notation);
1032 string_expr_list.size()==condition_list.size(),
1033 "number of created strings should correspond to number of conditions");
1038 str, string_expr_list[0], symbol_table,
true);
1039 for(std::size_t i=1; i<condition_list.size(); i++)
1044 str, string_expr_list[i], symbol_table,
true),
1047 code.
add(tmp_code, loc);
1081 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1083 params.erase(params.begin());
1126 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1147 function_id, type, loc, symbol_table,
false);
1170 const symbol_exprt obj(params[0].get_identifier(), params[0].type());
1181 ID_cprover_string_literal_func,
1190 ID_cprover_string_substring_func,
1199 string_ptr_type, loc, function_id, symbol_table, code);
1202 string1, string_expr1, symbol_table,
true),
1231 function_id, args, type.
return_type(), symbol_table),
1269 type.
return_type(), loc, function_id, symbol_table, code);
1272 str, string_expr, symbol_table,
true),
1312 string_expr, arg0, loc, symbol_table, code);
1316 type.
return_type(), loc, function_id, symbol_table, code);
1319 str, string_expr, symbol_table,
true),
1358 string_expr, arg1, loc, symbol_table, copy_constructor_body);
1362 copy_constructor_body.
add(
1364 arg_this, string_expr, symbol_table,
true),
1367 return copy_constructor_body;
1404 if(map->count(function_id) != 0)
1410 template <
typename TMap,
typename TContainer>
1414 std::is_same<
typename TMap::key_type,
1415 typename TContainer::value_type>::value,
1416 "TContainer value_type doesn't match TMap key_type");
1420 std::inserter(container, container.begin()),
1421 [](
const typename TMap::value_type &pair) { return pair.first; });
1425 std::unordered_set<irep_idt> &methods)
const
1453 it_id->second, type, loc, symbol_table);
1458 it_id->second, type, loc, symbol_table);
1463 it_id->second, type, loc, symbol_table);
1468 it_id->second, type, loc, symbol_table);
1474 return it->second(type, loc, function_id, symbol_table);
1489 string_types = std::unordered_set<irep_idt>{
"java.lang.String",
1490 "java.lang.StringBuilder",
1491 "java.lang.CharSequence",
1492 "java.lang.StringBuffer"};
1507 [
"java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1508 "lang/CharSequence;II)"
1509 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1513 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"] =
1514 ID_cprover_string_char_at_func;
1516 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1517 ID_cprover_string_char_at_func;
1519 [
"java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1520 ID_cprover_string_code_point_at_func;
1522 [
"java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1523 ID_cprover_string_code_point_before_func;
1525 [
"java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1526 ID_cprover_string_code_point_count_func;
1528 [
"java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1529 "lang/StringBuffer;"] = ID_cprover_string_delete_func;
1531 [
"java::org.cprover.CProverString.delete:(Ljava/lang/"
1532 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
1533 ID_cprover_string_delete_func;
1535 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1536 "StringBuffer;I)Ljava/lang/StringBuffer;"] =
1537 ID_cprover_string_delete_char_at_func;
1539 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1540 "StringBuilder;I)Ljava/lang/StringBuilder;"] =
1541 ID_cprover_string_delete_char_at_func;
1543 std::string format_signature =
"java::org.cprover.CProverString.format:(";
1545 format_signature +=
"Ljava/lang/String;";
1546 format_signature +=
")Ljava/lang/String;";
1548 ID_cprover_string_format_func;
1551 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1552 "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
1554 [
"java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1555 "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
1557 [
"java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1558 "StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
1560 [
"java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1561 "StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
1563 [
"java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
1564 ID_cprover_string_set_length_func;
1566 [
"java::org.cprover.CProverString.setLength:(Ljava/lang/"
1567 "StringBuilder;I)V"] = ID_cprover_string_set_length_func;
1569 [
"java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1570 "lang/CharSequence;"] = ID_cprover_string_substring_func;
1574 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1575 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1577 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1578 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1580 [
"java::org.cprover.CProverString.substring:(Ljava/Lang/"
1581 "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
1583 [
"java::org.cprover.CProverString.toString:(I)Ljava/lang/String;"] =
1584 ID_cprover_string_of_int_func;
1586 [
"java::org.cprover.CProverString.toString:(II)Ljava/lang/String;"] =
1587 ID_cprover_string_of_int_func;
1589 [
"java::org.cprover.CProverString.toString:(J)Ljava/lang/String;"] =
1590 ID_cprover_string_of_long_func;
1592 [
"java::org.cprover.CProverString.toString:(JI)Ljava/lang/String;"] =
1593 ID_cprover_string_of_long_func;
1595 [
"java::org.cprover.CProverString.toString:(F)Ljava/lang/String;"] =
1599 std::placeholders::_1,
1600 std::placeholders::_2,
1601 std::placeholders::_3,
1602 std::placeholders::_4);
1604 [
"java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
1605 ID_cprover_string_parse_int_func;
1607 [
"java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
1608 ID_cprover_string_parse_int_func;
1610 [
"java::org.cprover.CProverString.isValidInt:(Ljava/lang/String;I)Z"] =
1611 ID_cprover_string_is_valid_int_func;
1613 [
"java::org.cprover.CProverString.isValidLong:(Ljava/lang/String;I)Z"] =
1614 ID_cprover_string_is_valid_long_func;
1621 std::placeholders::_1,
1622 std::placeholders::_2,
1623 std::placeholders::_3,
1624 std::placeholders::_4);
1626 [
"java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1629 std::placeholders::_1,
1630 std::placeholders::_2,
1631 std::placeholders::_3,
1632 std::placeholders::_4);
1634 [
"java::java.lang.String.<init>:()V"]=
1635 ID_cprover_string_empty_string_func;
1638 [
"java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1639 ID_cprover_string_compare_to_func;
1641 [
"java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1642 ID_cprover_string_concat_func;
1644 [
"java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1645 ID_cprover_string_contains_func;
1647 [
"java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1648 ID_cprover_string_endswith_func;
1650 [
"java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1651 ID_cprover_string_equals_ignore_case_func;
1654 [
"java::java.lang.String.indexOf:(I)I"]=
1655 ID_cprover_string_index_of_func;
1657 [
"java::java.lang.String.indexOf:(II)I"]=
1658 ID_cprover_string_index_of_func;
1660 [
"java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1661 ID_cprover_string_index_of_func;
1663 [
"java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1664 ID_cprover_string_index_of_func;
1666 [
"java::java.lang.String.isEmpty:()Z"]=
1667 ID_cprover_string_is_empty_func;
1669 [
"java::java.lang.String.lastIndexOf:(I)I"]=
1670 ID_cprover_string_last_index_of_func;
1672 [
"java::java.lang.String.lastIndexOf:(II)I"]=
1673 ID_cprover_string_last_index_of_func;
1675 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1676 ID_cprover_string_last_index_of_func;
1678 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1679 ID_cprover_string_last_index_of_func;
1683 std::placeholders::_1,
1684 std::placeholders::_2,
1685 std::placeholders::_3,
1686 std::placeholders::_4);
1688 [
"java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1689 ID_cprover_string_replace_func;
1691 [
"java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]=
1692 ID_cprover_string_replace_func;
1694 [
"java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1695 ID_cprover_string_startswith_func;
1697 [
"java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1698 ID_cprover_string_startswith_func;
1700 [
"java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1701 ID_cprover_string_to_lower_case_func;
1706 std::placeholders::_1,
1707 std::placeholders::_2,
1708 std::placeholders::_3,
1709 std::placeholders::_4);
1711 [
"java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
1712 ID_cprover_string_to_upper_case_func;
1714 [
"java::java.lang.String.trim:()Ljava/lang/String;"]=
1715 ID_cprover_string_trim_func;
1719 [
"java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
1722 std::placeholders::_1,
1723 std::placeholders::_2,
1724 std::placeholders::_3,
1725 std::placeholders::_4);
1727 [
"java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
1731 std::placeholders::_1,
1732 std::placeholders::_2,
1733 std::placeholders::_3,
1734 std::placeholders::_4);
1736 [
"java::java.lang.StringBuilder.<init>:()V"]=
1737 ID_cprover_string_empty_string_func;
1739 [
"java::java.lang.StringBuilder.<init>:(I)V"] =
1740 ID_cprover_string_empty_string_func;
1743 [
"java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1744 ID_cprover_string_concat_char_func;
1746 [
"java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1747 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1749 [
"java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1750 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1752 [
"java::java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1753 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1755 [
"java::java.lang.StringBuilder.appendCodePoint:(I)"
1756 "Ljava/lang/StringBuilder;"]=
1757 ID_cprover_string_concat_code_point_func;
1759 [
"java::java.lang.StringBuilder.charAt:(I)C"]=
1760 ID_cprover_string_char_at_func;
1762 [
"java::java.lang.StringBuilder.codePointAt:(I)I"]=
1763 ID_cprover_string_code_point_at_func;
1765 [
"java::java.lang.StringBuilder.codePointBefore:(I)I"]=
1766 ID_cprover_string_code_point_before_func;
1768 [
"java::java.lang.StringBuilder.codePointCount:(II)I"]=
1769 ID_cprover_string_code_point_count_func;
1773 std::placeholders::_1,
1774 std::placeholders::_2,
1775 std::placeholders::_3,
1776 std::placeholders::_4);
1778 [
"java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1779 ID_cprover_string_substring_func;
1781 [
"java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1782 ID_cprover_string_substring_func;
1784 [
"java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
1787 std::placeholders::_1,
1788 std::placeholders::_2,
1789 std::placeholders::_3,
1790 std::placeholders::_4);
1794 [
"java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
1797 std::placeholders::_1,
1798 std::placeholders::_2,
1799 std::placeholders::_3,
1800 std::placeholders::_4);
1802 [
"java::java.lang.StringBuffer.<init>:()V"]=
1803 ID_cprover_string_empty_string_func;
1806 [
"java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
1807 ID_cprover_string_concat_char_func;
1809 [
"java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
1810 "Ljava/lang/StringBuffer;"]=
1811 ID_cprover_string_concat_func;
1813 [
"java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1814 "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
1816 [
"java::java.lang.StringBuffer.appendCodePoint:(I)"
1817 "Ljava/lang/StringBuffer;"]=
1818 ID_cprover_string_concat_code_point_func;
1820 [
"java::java.lang.StringBuffer.codePointAt:(I)I"]=
1821 ID_cprover_string_code_point_at_func;
1823 [
"java::java.lang.StringBuffer.codePointBefore:(I)I"]=
1824 ID_cprover_string_code_point_before_func;
1826 [
"java::java.lang.StringBuffer.codePointCount:(II)I"]=
1827 ID_cprover_string_code_point_count_func;
1829 [
"java::java.lang.StringBuffer.length:()I"]=
1832 [
"java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
1833 ID_cprover_string_substring_func;
1835 [
"java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
1838 std::placeholders::_1,
1839 std::placeholders::_2,
1840 std::placeholders::_3,
1841 std::placeholders::_4);
1845 [
"java::java.lang.CharSequence.charAt:(I)C"]=
1846 ID_cprover_string_char_at_func;
1848 [
"java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
1851 std::placeholders::_1,
1852 std::placeholders::_2,
1853 std::placeholders::_3,
1854 std::placeholders::_4);
1856 [
"java::java.lang.CharSequence.length:()I"]=
1861 [
"java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1862 ID_cprover_string_of_int_hex_func;
1864 "Ljava/lang/Object;)Ljava/lang/String;"] =
1868 std::placeholders::_1,
1869 std::placeholders::_2,
1870 std::placeholders::_3,
1871 std::placeholders::_4);