39 if(type.
id() == ID_struct_tag)
41 else if(type.
id() == ID_struct)
52 const typet &type,
const std::string &tag)
62 if(type.
id()==ID_pointer)
93 if(type.
id()==ID_pointer)
116 if(type.
id()==ID_pointer)
139 if(type.
id()==ID_pointer)
162 if(type.
id()==ID_pointer)
181 std::vector<irep_idt>
188 std::vector<irep_idt> bases;
190 if(class_name !=
"java.lang.CharSequence")
192 bases.push_back(
"java.io.Serializable");
193 bases.push_back(
"java.lang.CharSequence");
195 if(class_name ==
"java.lang.String")
196 bases.push_back(
"java.lang.Comparable");
198 if(class_name ==
"java.lang.StringBuilder" ||
199 class_name ==
"java.lang.StringBuffer")
200 bases.push_back(
"java.lang.AbstractStringBuilder");
212 string_type.
set_tag(class_name);
215 string_type.
components()[0].set_name(
"@java.lang.Object");
216 string_type.
components()[0].set_pretty_name(
"@java.lang.Object");
219 string_type.
components()[1].set_name(
"length");
220 string_type.
components()[1].set_pretty_name(
"length");
223 string_type.
components()[2].set_pretty_name(
"data");
229 for(
const irep_idt &base_name : bases)
234 symbolt *string_symbol=
nullptr;
235 symbol_table.
move(tmp_string_symbol, string_symbol);
238 string_symbol->
type=string_type;
240 string_symbol->
mode = ID_java;
255 "cprover_string_array",
256 "cprover_string_array",
278 for(
const auto &p : params)
302 const exprt &expr_to_process,
311 string_expr, expr_to_process,
loc, symbol_table, init_code);
333 for(
const auto &p : operands)
364 const exprt &op0=operands[0];
365 const exprt &op1 = operands[1];
388 if(type.
id() == ID_struct_tag)
408 if(type.
id() == ID_struct_tag)
447 const exprt &array_pointer,
458 array_data.type(),
"char_array",
"char_array",
loc, ID_java, symbol_table);
471 string_expr.
content(), inf_array, symbol_table,
loc, code);
488 type,
"cprover_string",
"cprover_string",
loc, ID_java, symbol_table);
506 "cprover_string_length",
507 "cprover_string_length",
515 "cprover_string_content",
516 "cprover_string_content",
546 exprt nondet_array_expr =
553 array_pointer, nondet_array_expr, symbol_table,
loc, code);
556 nondet_array_expr, str.
length(), symbol_table,
loc, code);
598 function_name, arguments, lhs.
type(), symbol_table);
618 function_name, arguments, type, symbol_table);
651 "nondet_infinite_array_pointer",
673 const exprt &pointer,
688 auto return_expr = return_sym.symbol_expr();
693 ID_cprover_associate_array_to_pointer_func,
725 ID_cprover_associate_length_to_array_func,
742 const exprt &pointer,
752 const auto return_expr = return_sym.symbol_expr();
758 ID_cprover_string_constrain_characters_func,
759 {length, pointer, char_set_expr},
790 std::string(
"return_code_") + function_name.
c_str(),
791 std::string(
"return_code_") + function_name.
c_str(),
795 const auto return_code = return_code_sym.
symbol_expr();
803 args.push_back(string_expr.
length());
804 args.push_back(string_expr.
content());
805 args.insert(args.end(), arguments.begin(), arguments.end());
810 return_code, function_name, args, symbol_table),
830 const exprt &rhs_array,
831 const exprt &rhs_length,
841 const symbolt &jlo_symbol = *symbol_table.
lookup(
"java::java.lang.Object");
849 struct_rhs.copy_to_operands(rhs_length);
850 struct_rhs.copy_to_operands(rhs_array);
919 rhs_length.
set(ID_mode, ID_java);
939 const std::string &s,
946 ID_cprover_string_literal_func, {expr},
loc, symbol_table, code);
964 const symbol_exprt arg(params[0].get_identifier(), params[0].type());
980 std::vector<exprt> condition_list;
981 std::vector<refined_string_exprt> string_expr_list;
986 ID_cprover_string_of_float_scientific_notation_func,
991 string_expr_list.push_back(sci_notation);
998 ID_cprover_string_concat_func,
999 {minus_sign, sci_notation},
1003 string_expr_list.push_back(neg_sci_notation);
1009 string_expr_list.push_back(nan);
1016 string_expr_list.push_back(infinity);
1022 string_expr_list.push_back(minus_infinity);
1037 condition_list.push_back(is_simple_float);
1040 ID_cprover_string_of_float_func, {arg},
loc, symbol_table, code);
1041 string_expr_list.push_back(simple_notation);
1047 condition_list.push_back(is_neg_simple_float);
1050 ID_cprover_string_concat_func,
1051 {minus_sign, simple_notation},
1055 string_expr_list.push_back(neg_simple_notation);
1059 string_expr_list.size()==condition_list.size(),
1060 "number of created strings should correspond to number of conditions");
1065 str, string_expr_list[0], symbol_table,
true);
1066 for(std::size_t i=1; i<condition_list.size(); i++)
1071 str, string_expr_list[i], symbol_table,
true),
1107 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1109 params.erase(params.begin());
1151 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1172 function_name, type,
loc, symbol_table,
false);
1196 const exprt &
object,
1205 if(type_name==ID_boolean)
1210 else if(type_name==ID_char)
1215 else if(type_name==ID_byte)
1220 else if(type_name==ID_short)
1225 else if(type_name==ID_int)
1230 else if(type_name==ID_long)
1235 else if(type_name==ID_float)
1240 else if(type_name==ID_double)
1245 else if(type_name==ID_void)
1250 DATA_INVARIANT(object_type.has_value(),
"must have symbol for primitive");
1253 std::string aux_name=
"tmp_"+
id2string(type_name);
1255 value_type, aux_name, aux_name,
loc, ID_java, symbol_table);
1261 const auto maybe_symbol =
1262 symbol_table.
lookup(object_type->get_identifier()))
1279 warning() << object_type->get_identifier()
1280 <<
" not available to format function" <<
eom;
1300 member_exprt data_member(deref_objs,
"data", pointer_of_pointer);
1304 data_pointer_plus_index, data_pointer_plus_index.type().subtype());
1350 std::list<exprt> field_exprs;
1351 for(
const auto & comp : structured_type.
components())
1353 const irep_idt &name=comp.get_name();
1354 const typet &type=comp.type();
1356 if(name!=
"string_expr")
1358 std::string tmp_name=
"tmp_"+
id2string(name);
1360 type,
id2string(function_id), tmp_name,
loc, ID_java, symbol_table);
1361 auto field_symbol_expr = field_symbol.
symbol_expr();
1362 field_expr = field_symbol_expr;
1369 field_exprs.push_back(field_expr);
1384 arg_i, symbol_table,
loc, function_id, code);
1395 for(
const auto &comp : structured_type.
components())
1397 const irep_idt &name=comp.get_name();
1398 exprt field_expr=field_exprs.front();
1399 field_exprs.pop_front();
1401 if(name==
"string_expr")
1413 else if(name==ID_int || name==ID_float || name==ID_char || name==ID_boolean)
1416 arg_i, name,
loc, symbol_table, code_not_null);
1417 if(value.has_value())
1428 code.
add(code_not_null,
loc);
1429 return arg_i_struct;
1454 INVARIANT(args.size()==2,
"String.format should have two arguments");
1461 structured_type.components().emplace_back(ID_int,
java_int_type());
1462 structured_type.components().emplace_back(ID_float,
java_float_type());
1463 structured_type.components().emplace_back(ID_char,
java_char_type());
1466 structured_type.components().emplace_back(
"hashcode",
java_int_type());
1468 structured_type.components().emplace_back(
"date_time",
java_int_type());
1472 std::vector<exprt> processed_args;
1473 processed_args.push_back(args[0]);
1475 processed_args.push_back(
1477 args[1], i, structured_type,
loc, function_id, symbol_table, code));
1480 ID_cprover_string_format_func, processed_args,
loc, symbol_table, code);
1485 java_string, string_expr, symbol_table,
true),
1511 const symbol_exprt this_obj(params[0].get_identifier(), params[0].type());
1521 class_type,
"class_symbol",
"class_symbol",
loc, ID_java, symbol_table);
1528 "@class_identifier",
1533 ID_cprover_string_literal_func,
1542 ID_cprover_string_substring_func,
1550 symbol_table.lookup_ref(
"java::java.lang.String").type);
1552 string_ptr_type,
loc, function_id, symbol_table, code);
1555 string1, string_expr1, symbol_table,
true),
1562 "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"),
1566 fun_call.function().type()=fun_type;
1595 function_name, args, type.
return_type(), symbol_table),
1636 str, string_expr, symbol_table,
true),
1674 string_expr, arg0,
loc, symbol_table, code);
1681 str, string_expr, symbol_table,
true),
1717 symbol_exprt arg1(params[1].get_identifier(), params[1].type());
1719 string_expr, arg1,
loc, symbol_table, code);
1722 symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1725 arg_this, string_expr, symbol_table,
true),
1751 symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1756 ret.add_source_location() =
loc;
1765 if(map->count(function_id) != 0)
1771 template <
typename TMap,
typename TContainer>
1775 std::is_same<
typename TMap::key_type,
1776 typename TContainer::value_type>::value,
1777 "TContainer value_type doesn't match TMap key_type");
1781 std::inserter(container, container.begin()),
1782 [](
const typename TMap::value_type &pair) {
return pair.first; });
1786 std::unordered_set<irep_idt> &methods)
const 1814 it_id->second, type,
loc, symbol_table);
1819 it_id->second, type,
loc, symbol_table);
1824 it_id->second, type,
loc, symbol_table);
1829 it_id->second, type,
loc, symbol_table);
1835 return it->second(type,
loc, function_id, symbol_table);
1850 string_types = std::unordered_set<irep_idt>{
"java.lang.String",
1851 "java.lang.StringBuilder",
1852 "java.lang.CharSequence",
1853 "java.lang.StringBuffer"};
1871 std::placeholders::_1,
1872 std::placeholders::_2,
1873 std::placeholders::_3,
1874 std::placeholders::_4);
1876 [
"java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1879 std::placeholders::_1,
1880 std::placeholders::_2,
1881 std::placeholders::_3,
1882 std::placeholders::_4);
1884 [
"java::java.lang.String.<init>:()V"]=
1885 ID_cprover_string_empty_string_func;
1890 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
1891 ID_cprover_string_char_at_func;
1893 [
"java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1894 ID_cprover_string_code_point_at_func;
1896 [
"java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1897 ID_cprover_string_code_point_before_func;
1899 [
"java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1900 ID_cprover_string_code_point_count_func;
1902 [
"java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1903 ID_cprover_string_compare_to_func;
1905 [
"java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1906 ID_cprover_string_concat_func;
1908 [
"java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1909 ID_cprover_string_contains_func;
1911 [
"java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
1912 ID_cprover_string_endswith_func;
1914 [
"java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
1915 ID_cprover_string_equals_ignore_case_func;
1917 [
"java::java.lang.String.format:(Ljava/lang/String;[Ljava/lang/Object;)" 1918 "Ljava/lang/String;"] =
1922 std::placeholders::_1,
1923 std::placeholders::_2,
1924 std::placeholders::_3,
1925 std::placeholders::_4);
1927 [
"java::java.lang.String.hashCode:()I"]=
1928 ID_cprover_string_hash_code_func;
1930 [
"java::java.lang.String.indexOf:(I)I"]=
1931 ID_cprover_string_index_of_func;
1933 [
"java::java.lang.String.indexOf:(II)I"]=
1934 ID_cprover_string_index_of_func;
1936 [
"java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
1937 ID_cprover_string_index_of_func;
1939 [
"java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
1940 ID_cprover_string_index_of_func;
1942 [
"java::java.lang.String.intern:()Ljava/lang/String;"]=
1943 ID_cprover_string_intern_func;
1945 [
"java::java.lang.String.isEmpty:()Z"]=
1946 ID_cprover_string_is_empty_func;
1948 [
"java::java.lang.String.lastIndexOf:(I)I"]=
1949 ID_cprover_string_last_index_of_func;
1951 [
"java::java.lang.String.lastIndexOf:(II)I"]=
1952 ID_cprover_string_last_index_of_func;
1954 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
1955 ID_cprover_string_last_index_of_func;
1957 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
1958 ID_cprover_string_last_index_of_func;
1962 std::placeholders::_1,
1963 std::placeholders::_2,
1964 std::placeholders::_3,
1965 std::placeholders::_4);
1967 [
"java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/" 1968 "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
1970 [
"java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
1971 ID_cprover_string_replace_func;
1973 [
"java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]=
1974 ID_cprover_string_replace_func;
1976 [
"java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
1977 ID_cprover_string_startswith_func;
1979 [
"java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
1980 ID_cprover_string_startswith_func;
1982 [
"java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/" 1983 "lang/CharSequence;"] = ID_cprover_string_substring_func;
1987 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;II)" 1988 "Ljava/lang/String;"]=
1989 ID_cprover_string_substring_func;
1991 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;I)" 1992 "Ljava/lang/String;"]=
1993 ID_cprover_string_substring_func;
1995 [
"java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
1996 ID_cprover_string_to_lower_case_func;
2001 std::placeholders::_1,
2002 std::placeholders::_2,
2003 std::placeholders::_3,
2004 std::placeholders::_4);
2006 [
"java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
2007 ID_cprover_string_to_upper_case_func;
2009 [
"java::java.lang.String.trim:()Ljava/lang/String;"]=
2010 ID_cprover_string_trim_func;
2012 [
"java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]=
2013 ID_cprover_string_of_bool_func;
2015 [
"java::java.lang.String.valueOf:(C)Ljava/lang/String;"]=
2016 ID_cprover_string_of_char_func;
2021 std::placeholders::_1,
2022 std::placeholders::_2,
2023 std::placeholders::_3,
2024 std::placeholders::_4);
2029 std::placeholders::_1,
2030 std::placeholders::_2,
2031 std::placeholders::_3,
2032 std::placeholders::_4);
2034 [
"java::java.lang.String.valueOf:(I)Ljava/lang/String;"]=
2035 ID_cprover_string_of_int_func;
2037 [
"java::java.lang.String.valueOf:(J)Ljava/lang/String;"]=
2038 ID_cprover_string_of_long_func;
2042 [
"java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
2045 std::placeholders::_1,
2046 std::placeholders::_2,
2047 std::placeholders::_3,
2048 std::placeholders::_4);
2050 [
"java::java.lang.StringBuilder.<init>:()V"]=
2051 ID_cprover_string_empty_string_func;
2054 [
"java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
2055 ID_cprover_string_concat_char_func;
2057 [
"java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] =
2058 ID_cprover_string_concat_double_func;
2060 [
"java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/" 2061 "lang/CharSequence;II)" 2062 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2064 [
"java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)" 2065 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2067 [
"java::java.lang.StringBuilder.append:(Ljava/lang/String;)" 2068 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2070 [
"java::java.lang.StringBuilder.appendCodePoint:(I)" 2071 "Ljava/lang/StringBuilder;"]=
2072 ID_cprover_string_concat_code_point_func;
2074 [
"java::java.lang.StringBuilder.charAt:(I)C"]=
2075 ID_cprover_string_char_at_func;
2077 [
"java::java.lang.StringBuilder.codePointAt:(I)I"]=
2078 ID_cprover_string_code_point_at_func;
2080 [
"java::java.lang.StringBuilder.codePointBefore:(I)I"]=
2081 ID_cprover_string_code_point_before_func;
2083 [
"java::java.lang.StringBuilder.codePointCount:(II)I"]=
2084 ID_cprover_string_code_point_count_func;
2086 [
"java::org.cprover.CProverString.delete:(Ljava/lang/" 2087 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2088 ID_cprover_string_delete_func;
2090 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" 2091 "StringBuilder;I)Ljava/lang/StringBuilder;"] =
2092 ID_cprover_string_delete_char_at_func;
2094 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2095 "StringBuilder;IC)Ljava/lang/StringBuilder;"] =
2096 ID_cprover_string_insert_char_func;
2098 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2099 "StringBuilder;IZ)Ljava/lang/StringBuilder;"] =
2100 ID_cprover_string_insert_bool_func;
2102 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2103 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2104 ID_cprover_string_insert_int_func;
2106 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2107 "StringBuilder;IJ)Ljava/lang/StringBuilder;"] =
2108 ID_cprover_string_insert_long_func;
2110 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/" 2111 "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
2115 std::placeholders::_1,
2116 std::placeholders::_2,
2117 std::placeholders::_3,
2118 std::placeholders::_4);
2120 [
"java::java.lang.StringBuilder.setCharAt:(IC)V"]=
2121 ID_cprover_string_char_set_func;
2123 [
"java::java.lang.StringBuilder.setLength:(I)V"]=
2124 ID_cprover_string_set_length_func;
2126 [
"java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
2127 ID_cprover_string_substring_func;
2129 [
"java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
2130 ID_cprover_string_substring_func;
2132 [
"java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
2135 std::placeholders::_1,
2136 std::placeholders::_2,
2137 std::placeholders::_3,
2138 std::placeholders::_4);
2142 [
"java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
2145 std::placeholders::_1,
2146 std::placeholders::_2,
2147 std::placeholders::_3,
2148 std::placeholders::_4);
2150 [
"java::java.lang.StringBuffer.<init>:()V"]=
2151 ID_cprover_string_empty_string_func;
2154 [
"java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
2155 ID_cprover_string_concat_char_func;
2157 [
"java::java.lang.StringBuffer.append:(D)Ljava/lang/StringBuffer;"]=
2158 ID_cprover_string_concat_double_func;
2160 [
"java::java.lang.StringBuffer.append:(F)Ljava/lang/StringBuffer;"]=
2161 ID_cprover_string_concat_float_func;
2163 [
"java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"]=
2164 ID_cprover_string_concat_int_func;
2166 [
"java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]=
2167 ID_cprover_string_concat_long_func;
2169 [
"java::java.lang.StringBuffer.append:(Ljava/lang/String;)" 2170 "Ljava/lang/StringBuffer;"]=
2171 ID_cprover_string_concat_func;
2173 [
"java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)" 2174 "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
2176 [
"java::java.lang.StringBuffer.appendCodePoint:(I)" 2177 "Ljava/lang/StringBuffer;"]=
2178 ID_cprover_string_concat_code_point_func;
2180 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
2181 ID_cprover_string_char_at_func;
2183 [
"java::java.lang.StringBuffer.codePointAt:(I)I"]=
2184 ID_cprover_string_code_point_at_func;
2186 [
"java::java.lang.StringBuffer.codePointBefore:(I)I"]=
2187 ID_cprover_string_code_point_before_func;
2189 [
"java::java.lang.StringBuffer.codePointCount:(II)I"]=
2190 ID_cprover_string_code_point_count_func;
2192 [
"java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/" 2193 "lang/StringBuffer;"] = ID_cprover_string_delete_func;
2195 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" 2196 "StringBufferI)Ljava/lang/StringBuffer;"] =
2197 ID_cprover_string_delete_char_at_func;
2199 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IC)Ljava/" 2200 "lang/StringBuffer;"] = ID_cprover_string_insert_char_func;
2202 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;II)Ljava/" 2203 "lang/StringBuffer;"] = ID_cprover_string_insert_int_func;
2205 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IJ)Ljava/" 2206 "lang/StringBuffer;"] = ID_cprover_string_insert_long_func;
2208 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;ILjava/" 2209 "lang/String;)Ljava/lang/StringBuffer;"] = ID_cprover_string_insert_func;
2211 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IZ)Ljava/" 2212 "lang/StringBuffer;"] = ID_cprover_string_insert_bool_func;
2214 [
"java::java.lang.StringBuffer.length:()I"]=
2217 [
"java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
2218 ID_cprover_string_char_set_func;
2220 [
"java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] =
2221 ID_cprover_string_set_length_func;
2223 [
"java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
2224 ID_cprover_string_substring_func;
2226 [
"java::org.cprover.CProverString.substring:(Ljava/Lang/" 2227 "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
2229 [
"java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
2232 std::placeholders::_1,
2233 std::placeholders::_2,
2234 std::placeholders::_3,
2235 std::placeholders::_4);
2239 [
"java::java.lang.CharSequence.charAt:(I)C"]=
2240 ID_cprover_string_char_at_func;
2242 [
"java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
2245 std::placeholders::_1,
2246 std::placeholders::_2,
2247 std::placeholders::_3,
2248 std::placeholders::_4);
2250 [
"java::java.lang.CharSequence.length:()I"]=
2258 std::placeholders::_1,
2259 std::placeholders::_2,
2260 std::placeholders::_3,
2261 std::placeholders::_4);
2263 [
"java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
2264 ID_cprover_string_parse_int_func;
2266 [
"java::java.lang.Integer.parseInt:(Ljava/lang/String;I)I"]=
2267 ID_cprover_string_parse_int_func;
2269 [
"java::java.lang.Long.parseLong:(Ljava/lang/String;)J"]=
2270 ID_cprover_string_parse_int_func;
2272 [
"java::java.lang.Long.parseLong:(Ljava/lang/String;I)J"]=
2273 ID_cprover_string_parse_int_func;
2275 [
"java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
2276 ID_cprover_string_of_int_hex_func;
2278 [
"java::java.lang.Integer.toString:(I)Ljava/lang/String;"]=
2279 ID_cprover_string_of_int_func;
2281 [
"java::java.lang.Integer.toString:(II)Ljava/lang/String;"]=
2282 ID_cprover_string_of_int_func;
2284 [
"java::java.lang.Long.toString:(J)Ljava/lang/String;"]=
2285 ID_cprover_string_of_int_func;
2287 [
"java::java.lang.Long.toString:(JI)Ljava/lang/String;"]=
2288 ID_cprover_string_of_int_func;
2293 std::placeholders::_1,
2294 std::placeholders::_2,
2295 std::placeholders::_3,
2296 std::placeholders::_4);
const irep_idt & get_name() const
The type of an expression, extends irept.
irep_idt name
The unique identifier.
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...
static codet code_assign_function_application(const exprt &lhs, const irep_idt &function_name, const exprt::operandst &arguments, symbol_table_baset &symbol_table)
assign the result of a function call
static typet string_length_type()
Semantic type conversion.
const typet & component_type(const irep_idt &component_name) const
static bool is_constructor(const irep_idt &method_name)
refined_string_exprt string_literal_to_string_expr(const std::string &s, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Create a string expression whose value is given by a literal.
static bool is_java_string_type(const typet &type)
const irep_idt & get_identifier() const
A base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
pointer_typet pointer_type(const typet &subtype)
id_mapt cprover_equivalent_to_java_assign_function
dereference_exprt checked_dereference(const exprt &expr, const typet &type)
Dereference an expression and flag it for a null-pointer check.
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...
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)
Produce code for an assignment of a string expr to a Java string.
static bool is_java_string_pointer_type(const typet &type)
typet java_boolean_type()
constant_exprt to_expr() const
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
code_blockt make_init_function_from_call(const irep_idt &function_name, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool is_constructor=true)
Generate the goto code for string initialization.
symbol_exprt fresh_array(const typet &type, const source_locationt &loc, symbol_tablet &symbol_table)
add a symbol in the table with static lifetime and name containing cprover_string_array and given typ...
irep_idt mode
Language mode.
Evaluates to true if the operand is infinite.
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)
Provide code for the String.valueOf(F) function.
reference_typet java_reference_type(const typet &subtype)
const exprt & content() const
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Type for string expressions used by the string solver.
const refined_string_typet refined_string_type
codet code_return_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
return the result of a function call
Fresh auxiliary symbol creation.
The null pointer constant.
std::vector< parametert > parameterst
refined_string_exprt decl_string_expr(const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Add declaration of a refined string expr whose content and length are fresh symbols.
const componentst & components() const
dereference_exprt get_object_at_index(const exprt &argv, std::size_t index)
Helper for format function.
The trinary if-then-else operator.
A struct tag type, i.e., struct_typet with an identifier.
static bool is_java_char_sequence_pointer_type(const typet &type)
irep_idt pretty_name
Language-specific display name.
typet & type()
Return the type of the expression.
std::unordered_set< irep_idt > string_types
code_blockt make_function_from_call(const irep_idt &function_name, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Provide code for a function that calls a function from the solver and simply returns it...
A constant literal expression.
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
#define CHECK_RETURN(CONDITION)
Structure type, corresponds to C style structs.
refined_string_exprt string_expr_of_function(const irep_idt &function_name, const exprt::operandst &arguments, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primit...
id_mapt cprover_equivalent_to_java_constructor
void set_access(const irep_idt &access)
static exprt get_length(const exprt &expr, const symbol_tablet &symbol_table)
access length member
static const typet & get_data_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the data component.
static bool is_java_string_buffer_pointer_type(const typet &type)
void add_character_set_constraint(const exprt &pointer, const exprt &length, const irep_idt &char_set, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver which ensures all characters belong to the character s...
Extract member of struct or union.
void change_spec(const ieee_float_spect &dest_spec)
mstreamt & warning() const
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 irep_idt & id() const
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table)
Should be called to provide code for string functions that are used in the code but for which no impl...
static bool is_java_string_builder_type(const typet &type)
Evaluates to true if the operand is NaN.
An expression denoting infinity.
void add(const codet &code)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
A codet representing the declaration of a local variable.
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
exprt make_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
Create a function application expression.
symbol_exprt fresh_string(const typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
add a symbol with static lifetime and name containing cprover_string and given type ...
Operator to dereference a pointer.
nonstd::optional< T > optionalt
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)
Generates code for the String.length method.
const std::array< id_mapt *, 5 > id_maps
API to expression classes.
id_mapt cprover_equivalent_to_java_assign_and_return_function
std::unordered_map< irep_idt, irep_idt > id_mapt
code_blockt make_string_returning_function_from_call(const irep_idt &function_name, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Provide code for a function that calls a function from the solver and return the string_expr result a...
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)
Generates code for a constructor of a string object from another string object.
code_blockt make_assign_function_from_call(const irep_idt &function_name, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Call a cprover internal function and assign the result to object this.
refined_string_exprt & to_string_expr(exprt &expr)
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)
Generates code for a function which copies a string object to a new string object.
optionalt< symbol_exprt > get_primitive_value_of_object(const exprt &object, irep_idt type_name, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Adds to the code an assignment of the form type_name tmp_type_name tmp_type_name = ((Classname*)arg_i...
#define PRECONDITION(CONDITION)
A side_effect_exprt that returns a non-deterministically chosen value.
void set_tag(const irep_idt &tag)
void from_float(const float f)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
void add_base(const struct_tag_typet &base)
Add a base class/struct.
const exprt & size() const
codet representation of a function call statement.
The plus expression Associativity is not specified.
static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating object of size size and assigning it to lhs
id_mapt cprover_equivalent_to_java_function
exprt::operandst process_parameters(const java_method_typet::parameterst ¶ms, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
calls string_refine_preprocesst::process_operands with a list of parameters.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
void initialize_known_type_table()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Operator to return the address of an object.
static bool is_java_char_array_pointer_type(const typet &type)
exprt::operandst process_operands(const exprt::operandst &operands, const source_locationt &loc, 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...
The unary minus expression.
The Boolean constant false.
bool implements_function(const irep_idt &function_id) const
std::vector< exprt > operandst
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 irep_idt get_tag(const typet &type)
struct_exprt make_argument_for_format(const exprt &argv, std::size_t index, const struct_typet &structured_type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
Helper for format function.
An assumption, which must hold in subsequent code.
String expressions for the string solver.
void add_keys_to_container(const TMap &map, TContainer &container)
static bool is_java_char_array_type(const typet &type)
code_blockt make_string_format_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Used to provide code for the Java String.format function.
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
exprt allocate_dynamic_object_with_decl(const exprt &target_expr, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &output_code)
Generates code for allocating a dynamic object.
const java_method_typet & to_java_method_type(const typet &type)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Base class for all expressions.
const parameterst & parameters() const
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
irep_idt base_name
Base (non-scoped) name.
The symbol table base class interface.
refined_string_exprt replace_char_array(const exprt &array_pointer, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
we declare a new cprover_string whose contents is deduced from the char array.
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
const source_locationt & source_location() const
character_refine_preprocesst character_preprocess
#define UNREACHABLE
This should be used to mark dead code.
irept & add(const irep_namet &name)
const exprt & length() const
void add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table)
Add to the symbol table type declaration for a String-like Java class.
code_blockt make_assign_and_return_function_from_call(const irep_idt &function_name, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Call a cprover internal function, assign the result to object this and return it. ...
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
static bool java_type_matches_tag(const typet &type, const std::string &tag)
std::unordered_map< irep_idt, conversion_functiont > conversion_table
A codet representing sequential composition of program statements.
static bool implements_java_char_sequence_pointer(const typet &type)
static const typet & get_length_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the length component.
codet representation of an if-then-else statement.
static bool is_java_string_buffer_type(const typet &type)
Expression to hold a symbol (variable)
const char * c_str() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Data structure for representing an arbitrary statement in a program.
codet representation of a "return from a function" statement.
void add_array_to_length_association(const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that the actual length of array is le...
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
An expression containing a side effect.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
static bool is_java_string_builder_pointer_type(const typet &type)
id_mapt cprover_equivalent_to_java_string_returning_function
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)
Struct constructor from list of elements.
code_blockt make_object_get_class_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Used to provide our own implementation of the java.lang.Object.getClass() function.
const irep_idt & get_identifier() const
const typet & return_type() const
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
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)
Produce code for an assignemnt of a string expr to a Java string.
A codet representing an assignment in the program.
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...
exprt::operandst process_equals_function_operands(const exprt::operandst &operands, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
Converts the operands of the equals function to string expressions and outputs these conversions...
void set(const irep_namet &name, const irep_idt &value)
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
refined_string_exprt convert_exprt_to_string_exprt(const exprt &deref, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
Creates a string_exprt from the input exprt representing a char sequence.
static bool is_java_char_sequence_type(const typet &type)
static exprt get_data(const exprt &expr, const symbol_tablet &symbol_table)
access data member
Produce code for simple implementation of String Java libraries.