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,
920 (void)message_handler;
926 const symbol_exprt arg(params[0].get_identifier(), params[0].type());
933 type.
return_type(), loc, function_id, symbol_table, code);
942 std::vector<exprt> condition_list;
943 std::vector<refined_string_exprt> string_expr_list;
948 ID_cprover_string_of_float_scientific_notation_func,
953 string_expr_list.push_back(sci_notation);
960 ID_cprover_string_concat_func,
961 {minus_sign, sci_notation},
965 string_expr_list.push_back(neg_sci_notation);
971 string_expr_list.push_back(nan);
978 string_expr_list.push_back(infinity);
984 string_expr_list.push_back(minus_infinity);
992 string_expr_list.push_back(zero_string);
1000 string_expr_list.push_back(minus_zero_string);
1014 condition_list.push_back(is_simple_float);
1017 ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code);
1018 string_expr_list.push_back(simple_notation);
1024 condition_list.push_back(is_neg_simple_float);
1027 ID_cprover_string_concat_func,
1028 {minus_sign, simple_notation},
1032 string_expr_list.push_back(neg_simple_notation);
1036 string_expr_list.size()==condition_list.size(),
1037 "number of created strings should correspond to number of conditions");
1042 str, string_expr_list[0], symbol_table,
true);
1043 for(std::size_t i=1; i<condition_list.size(); i++)
1048 str, string_expr_list[i], symbol_table,
true),
1051 code.
add(tmp_code, loc);
1085 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1087 params.erase(params.begin());
1130 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1151 function_id, type, loc, symbol_table,
false);
1176 const symbol_exprt obj(params[0].get_identifier(), params[0].type());
1187 ID_cprover_string_literal_func,
1196 ID_cprover_string_substring_func,
1205 string_ptr_type, loc, function_id, symbol_table, code);
1208 string1, string_expr1, symbol_table,
true),
1237 function_id, args, type.
return_type(), symbol_table),
1275 type.
return_type(), loc, function_id, symbol_table, code);
1278 str, string_expr, symbol_table,
true),
1308 (void)message_handler;
1322 string_expr, arg0, loc, symbol_table, code);
1326 type.
return_type(), loc, function_id, symbol_table, code);
1329 str, string_expr, symbol_table,
true),
1358 (void)message_handler;
1372 string_expr, arg1, loc, symbol_table, copy_constructor_body);
1376 copy_constructor_body.
add(
1378 arg_this, string_expr, symbol_table,
true),
1381 return copy_constructor_body;
1404 (void)message_handler;
1421 if(map->count(function_id) != 0)
1427 template <
typename TMap,
typename TContainer>
1431 std::is_same<
typename TMap::key_type,
1432 typename TContainer::value_type>::value,
1433 "TContainer value_type doesn't match TMap key_type");
1437 std::inserter(container, container.begin()),
1438 [](
const typename TMap::value_type &pair) { return pair.first; });
1442 std::unordered_set<irep_idt> &methods)
const
1472 it_id->second, type, loc, symbol_table);
1477 it_id->second, type, loc, symbol_table);
1482 it_id->second, type, loc, symbol_table);
1487 it_id->second, type, loc, symbol_table);
1493 return it->second(type, loc, function_id, symbol_table, message_handler);
1508 string_types = std::unordered_set<irep_idt>{
"java.lang.String",
1509 "java.lang.StringBuilder",
1510 "java.lang.CharSequence",
1511 "java.lang.StringBuffer"};
1526 [
"java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
1527 "lang/CharSequence;II)"
1528 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1532 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"] =
1533 ID_cprover_string_char_at_func;
1535 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
1536 ID_cprover_string_char_at_func;
1538 [
"java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1539 ID_cprover_string_code_point_at_func;
1541 [
"java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1542 ID_cprover_string_code_point_before_func;
1544 [
"java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1545 ID_cprover_string_code_point_count_func;
1547 [
"java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
1548 "lang/StringBuffer;"] = ID_cprover_string_delete_func;
1550 [
"java::org.cprover.CProverString.delete:(Ljava/lang/"
1551 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
1552 ID_cprover_string_delete_func;
1554 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1555 "StringBuffer;I)Ljava/lang/StringBuffer;"] =
1556 ID_cprover_string_delete_char_at_func;
1558 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
1559 "StringBuilder;I)Ljava/lang/StringBuilder;"] =
1560 ID_cprover_string_delete_char_at_func;
1562 std::string format_signature =
"java::org.cprover.CProverString.format:(";
1564 format_signature +=
"Ljava/lang/String;";
1565 format_signature +=
")Ljava/lang/String;";
1567 ID_cprover_string_format_func;
1570 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
1571 "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
1573 [
"java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
1574 "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
1576 [
"java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1577 "StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
1579 [
"java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
1580 "StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
1582 [
"java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
1583 ID_cprover_string_set_length_func;
1585 [
"java::org.cprover.CProverString.setLength:(Ljava/lang/"
1586 "StringBuilder;I)V"] = ID_cprover_string_set_length_func;
1588 [
"java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
1589 "lang/CharSequence;"] = ID_cprover_string_substring_func;
1593 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;I)"
1594 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1596 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;II)"
1597 "Ljava/lang/String;"] = ID_cprover_string_substring_func;
1599 [
"java::org.cprover.CProverString.substring:(Ljava/Lang/"
1600 "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
1602 [
"java::org.cprover.CProverString.toString:(I)Ljava/lang/String;"] =
1603 ID_cprover_string_of_int_func;
1605 [
"java::org.cprover.CProverString.toString:(II)Ljava/lang/String;"] =
1606 ID_cprover_string_of_int_func;
1608 [
"java::org.cprover.CProverString.toString:(J)Ljava/lang/String;"] =
1609 ID_cprover_string_of_long_func;
1611 [
"java::org.cprover.CProverString.toString:(JI)Ljava/lang/String;"] =
1612 ID_cprover_string_of_long_func;
1614 [
"java::org.cprover.CProverString.toString:(F)Ljava/lang/String;"] =
1618 std::placeholders::_1,
1619 std::placeholders::_2,
1620 std::placeholders::_3,
1621 std::placeholders::_4,
1622 std::placeholders::_5);
1624 [
"java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
1625 ID_cprover_string_parse_int_func;
1627 [
"java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
1628 ID_cprover_string_parse_int_func;
1630 [
"java::org.cprover.CProverString.isValidInt:(Ljava/lang/String;I)Z"] =
1631 ID_cprover_string_is_valid_int_func;
1633 [
"java::org.cprover.CProverString.isValidLong:(Ljava/lang/String;I)Z"] =
1634 ID_cprover_string_is_valid_long_func;
1641 std::placeholders::_1,
1642 std::placeholders::_2,
1643 std::placeholders::_3,
1644 std::placeholders::_4,
1645 std::placeholders::_5);
1647 [
"java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1650 std::placeholders::_1,
1651 std::placeholders::_2,
1652 std::placeholders::_3,
1653 std::placeholders::_4,
1654 std::placeholders::_5);
1656 [
"java::java.lang.String.<init>:()V"]=
1657 ID_cprover_string_empty_string_func;
1660 [
"java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1661 ID_cprover_string_compare_to_func;
1663 [
"java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1664 ID_cprover_string_concat_func;
1666 [
"java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1667 ID_cprover_string_contains_func;
1669 [
"java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1670 ID_cprover_string_endswith_func;
1672 [
"java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1673 ID_cprover_string_equals_ignore_case_func;
1676 [
"java::java.lang.String.indexOf:(I)I"]=
1677 ID_cprover_string_index_of_func;
1679 [
"java::java.lang.String.indexOf:(II)I"]=
1680 ID_cprover_string_index_of_func;
1682 [
"java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1683 ID_cprover_string_index_of_func;
1685 [
"java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1686 ID_cprover_string_index_of_func;
1688 [
"java::java.lang.String.isEmpty:()Z"]=
1689 ID_cprover_string_is_empty_func;
1691 [
"java::java.lang.String.lastIndexOf:(I)I"]=
1692 ID_cprover_string_last_index_of_func;
1694 [
"java::java.lang.String.lastIndexOf:(II)I"]=
1695 ID_cprover_string_last_index_of_func;
1697 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1698 ID_cprover_string_last_index_of_func;
1700 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1701 ID_cprover_string_last_index_of_func;
1705 std::placeholders::_1,
1706 std::placeholders::_2,
1707 std::placeholders::_3,
1708 std::placeholders::_4,
1709 std::placeholders::_5);
1711 [
"java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1712 ID_cprover_string_replace_func;
1714 [
"java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]=
1715 ID_cprover_string_replace_func;
1717 [
"java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1718 ID_cprover_string_startswith_func;
1720 [
"java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1721 ID_cprover_string_startswith_func;
1723 [
"java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1724 ID_cprover_string_to_lower_case_func;
1729 std::placeholders::_1,
1730 std::placeholders::_2,
1731 std::placeholders::_3,
1732 std::placeholders::_4,
1733 std::placeholders::_5);
1735 [
"java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
1736 ID_cprover_string_to_upper_case_func;
1738 [
"java::java.lang.String.trim:()Ljava/lang/String;"]=
1739 ID_cprover_string_trim_func;
1743 [
"java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
1746 std::placeholders::_1,
1747 std::placeholders::_2,
1748 std::placeholders::_3,
1749 std::placeholders::_4,
1750 std::placeholders::_5);
1752 [
"java::java.lang.StringBuilder.<init>:(Ljava/lang/CharSequence;)V"] =
1756 std::placeholders::_1,
1757 std::placeholders::_2,
1758 std::placeholders::_3,
1759 std::placeholders::_4,
1760 std::placeholders::_5);
1762 [
"java::java.lang.StringBuilder.<init>:()V"]=
1763 ID_cprover_string_empty_string_func;
1765 [
"java::java.lang.StringBuilder.<init>:(I)V"] =
1766 ID_cprover_string_empty_string_func;
1769 [
"java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
1770 ID_cprover_string_concat_char_func;
1772 [
"java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
1773 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1775 [
"java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
1776 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1778 [
"java::java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)"
1779 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
1781 [
"java::java.lang.StringBuilder.appendCodePoint:(I)"
1782 "Ljava/lang/StringBuilder;"]=
1783 ID_cprover_string_concat_code_point_func;
1785 [
"java::java.lang.StringBuilder.charAt:(I)C"]=
1786 ID_cprover_string_char_at_func;
1788 [
"java::java.lang.StringBuilder.codePointAt:(I)I"]=
1789 ID_cprover_string_code_point_at_func;
1791 [
"java::java.lang.StringBuilder.codePointBefore:(I)I"]=
1792 ID_cprover_string_code_point_before_func;
1794 [
"java::java.lang.StringBuilder.codePointCount:(II)I"]=
1795 ID_cprover_string_code_point_count_func;
1799 std::placeholders::_1,
1800 std::placeholders::_2,
1801 std::placeholders::_3,
1802 std::placeholders::_4,
1803 std::placeholders::_5);
1805 [
"java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
1806 ID_cprover_string_substring_func;
1808 [
"java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
1809 ID_cprover_string_substring_func;
1811 [
"java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
1814 std::placeholders::_1,
1815 std::placeholders::_2,
1816 std::placeholders::_3,
1817 std::placeholders::_4,
1818 std::placeholders::_5);
1822 [
"java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
1825 std::placeholders::_1,
1826 std::placeholders::_2,
1827 std::placeholders::_3,
1828 std::placeholders::_4,
1829 std::placeholders::_5);
1831 [
"java::java.lang.StringBuffer.<init>:()V"]=
1832 ID_cprover_string_empty_string_func;
1835 [
"java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
1836 ID_cprover_string_concat_char_func;
1838 [
"java::java.lang.StringBuffer.append:(Ljava/lang/String;)"
1839 "Ljava/lang/StringBuffer;"]=
1840 ID_cprover_string_concat_func;
1842 [
"java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)"
1843 "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
1845 [
"java::java.lang.StringBuffer.appendCodePoint:(I)"
1846 "Ljava/lang/StringBuffer;"]=
1847 ID_cprover_string_concat_code_point_func;
1849 [
"java::java.lang.StringBuffer.codePointAt:(I)I"]=
1850 ID_cprover_string_code_point_at_func;
1852 [
"java::java.lang.StringBuffer.codePointBefore:(I)I"]=
1853 ID_cprover_string_code_point_before_func;
1855 [
"java::java.lang.StringBuffer.codePointCount:(II)I"]=
1856 ID_cprover_string_code_point_count_func;
1858 [
"java::java.lang.StringBuffer.length:()I"]=
1861 [
"java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
1862 ID_cprover_string_substring_func;
1864 [
"java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
1867 std::placeholders::_1,
1868 std::placeholders::_2,
1869 std::placeholders::_3,
1870 std::placeholders::_4,
1871 std::placeholders::_5);
1875 [
"java::java.lang.CharSequence.charAt:(I)C"]=
1876 ID_cprover_string_char_at_func;
1878 [
"java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
1881 std::placeholders::_1,
1882 std::placeholders::_2,
1883 std::placeholders::_3,
1884 std::placeholders::_4,
1885 std::placeholders::_5);
1887 [
"java::java.lang.CharSequence.length:()I"]=
1892 [
"java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
1893 ID_cprover_string_of_int_hex_func;
1895 [
"java::org.cprover.CProver.classIdentifier:("
1896 "Ljava/lang/Object;)Ljava/lang/String;"] =
1900 std::placeholders::_1,
1901 std::placeholders::_2,
1902 std::placeholders::_3,
1903 std::placeholders::_4,
1904 std::placeholders::_5);