39 if(type.
id() == ID_symbol)
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)
193 std::vector<irep_idt>
200 std::vector<irep_idt> bases;
202 if(class_name !=
"java.lang.CharSequence")
204 bases.push_back(
"java.io.Serializable");
205 bases.push_back(
"java.lang.CharSequence");
207 if(class_name ==
"java.lang.String")
208 bases.push_back(
"java.lang.Comparable");
210 if(class_name ==
"java.lang.StringBuilder" ||
211 class_name ==
"java.lang.StringBuffer")
212 bases.push_back(
"java.lang.AbstractStringBuilder");
224 string_type.
set_tag(class_name);
227 string_type.
components()[0].set_name(
"@java.lang.Object");
228 string_type.
components()[0].set_pretty_name(
"@java.lang.Object");
230 string_type.
components()[1].set_name(
"length");
231 string_type.
components()[1].set_pretty_name(
"length");
234 string_type.
components()[2].set_pretty_name(
"data");
240 for(
const irep_idt &base_name : bases)
245 symbolt *string_symbol=
nullptr;
246 symbol_table.
move(tmp_string_symbol, string_symbol);
249 string_symbol->
type=string_type;
251 string_symbol->
mode = ID_java;
266 "cprover_string_array",
267 "cprover_string_array",
289 for(
const auto &p : params)
313 const exprt &expr_to_process,
322 string_expr, expr_to_process,
loc, symbol_table, init_code);
344 for(
const auto &p : operands)
375 const exprt &op0=operands[0];
376 const exprt &op1 = operands[1];
398 if(type.
id()==ID_symbol)
417 if(type.
id()==ID_symbol)
455 const exprt &array_pointer,
466 array_data.type(),
"char_array",
"char_array",
loc, ID_java, symbol_table);
479 string_expr.
content(), inf_array, symbol_table,
loc, code);
496 type,
"cprover_string",
"cprover_string",
loc, ID_java, symbol_table);
514 "cprover_string_length",
515 "cprover_string_length",
523 "cprover_string_content",
524 "cprover_string_content",
554 exprt nondet_array_expr =
561 array_pointer, nondet_array_expr, symbol_table,
loc, code);
564 nondet_array_expr, str.
length(), symbol_table,
loc, code);
605 array, symbol_table,
loc, function_id, code);
625 function_name, arguments, lhs.
type(), symbol_table);
645 function_name, arguments, type, symbol_table);
666 "nondet_infinite_array",
685 const exprt &pointer,
700 exprt return_expr = return_sym.symbol_expr();
705 ID_cprover_associate_array_to_pointer_func,
737 ID_cprover_associate_length_to_array_func,
754 const exprt &pointer,
764 const exprt return_expr = return_sym.symbol_expr();
770 ID_cprover_string_constrain_characters_func,
771 {length, pointer, char_set_expr},
802 std::string(
"return_code_") + function_name.
c_str(),
803 std::string(
"return_code_") + function_name.
c_str(),
815 args.push_back(string_expr.
length());
816 args.push_back(string_expr.
content());
817 args.insert(args.end(), arguments.begin(), arguments.end());
822 return_code, function_name, args, symbol_table),
839 const exprt &rhs_array,
840 const exprt &rhs_length,
847 const symbolt &jlo_symbol=*symbol_table.
lookup(
"java::java.lang.Object");
855 struct_rhs.copy_to_operands(rhs_length);
856 struct_rhs.copy_to_operands(rhs_array);
912 rhs_length.
set(ID_mode, ID_java);
932 const std::string &s,
939 ID_cprover_string_literal_func, {expr},
loc, symbol_table, code);
998 ID_cprover_string_equal_func, args, return_type, symbol_table);
1001 return instance_case;
1022 const symbol_exprt arg(params[0].get_identifier(), params[0].type());
1038 std::vector<exprt> condition_list;
1039 std::vector<refined_string_exprt> string_expr_list;
1044 ID_cprover_string_of_float_scientific_notation_func,
1049 string_expr_list.push_back(sci_notation);
1056 ID_cprover_string_concat_func,
1057 {minus_sign, sci_notation},
1061 string_expr_list.push_back(neg_sci_notation);
1067 string_expr_list.push_back(nan);
1074 string_expr_list.push_back(infinity);
1080 string_expr_list.push_back(minus_infinity);
1095 condition_list.push_back(is_simple_float);
1098 ID_cprover_string_of_float_func, {arg},
loc, symbol_table, code);
1099 string_expr_list.push_back(simple_notation);
1105 condition_list.push_back(is_neg_simple_float);
1108 ID_cprover_string_concat_func,
1109 {minus_sign, simple_notation},
1113 string_expr_list.push_back(neg_simple_notation);
1117 string_expr_list.size()==condition_list.size(),
1118 "number of created strings should correspond to number of conditions");
1123 str, string_expr_list[0], symbol_table);
1124 for(std::size_t i=1; i<condition_list.size(); i++)
1127 ife.
cond()=condition_list[i];
1129 str, string_expr_list[i], symbol_table);
1161 bool ignore_first_arg)
1167 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1168 if(ignore_first_arg)
1169 params.erase(params.begin());
1210 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1231 function_name, type,
loc, symbol_table,
false);
1255 const exprt &
object,
1264 if(type_name==ID_boolean)
1269 else if(type_name==ID_char)
1274 else if(type_name==ID_byte)
1279 else if(type_name==ID_short)
1284 else if(type_name==ID_int)
1289 else if(type_name==ID_long)
1294 else if(type_name==ID_float)
1299 else if(type_name==ID_double)
1304 else if(type_name==ID_void)
1309 DATA_INVARIANT(object_type.has_value(),
"must have symbol for primitive");
1312 std::string aux_name=
"tmp_"+
id2string(type_name);
1314 value_type, aux_name, aux_name,
loc, ID_java, symbol_table);
1320 const auto maybe_symbol =
1321 symbol_table.
lookup(object_type->get_identifier()))
1338 warning() << object_type->get_identifier()
1339 <<
" not available to format function" <<
eom;
1359 member_exprt data_member(deref_objs,
"data", pointer_of_pointer);
1363 data_pointer_plus_index, data_pointer_plus_index.type().subtype());
1364 return data_at_index;
1412 std::list<exprt> field_exprs;
1413 for(
const auto & comp : structured_type.
components())
1415 const irep_idt &name=comp.get_name();
1416 const typet &type=comp.type();
1418 if(name!=
"string_expr")
1420 std::string tmp_name=
"tmp_"+
id2string(name);
1422 type,
id2string(function_id), tmp_name,
loc, ID_java, symbol_table);
1430 field_exprs.push_back(field_expr);
1445 arg_i, symbol_table,
loc, function_id, code);
1460 for(
const auto &comp : structured_type.
components())
1462 const irep_idt &name=comp.get_name();
1463 exprt field_expr=field_exprs.front();
1464 field_exprs.pop_front();
1466 if(name==
"string_expr")
1478 else if(name==ID_int || name==ID_float || name==ID_char || name==ID_boolean)
1481 arg_i, name,
loc, symbol_table, code_not_null);
1490 code.
add(code_not_null,
loc);
1491 return arg_i_struct;
1515 INVARIANT(args.size()==2,
"String.format should have two arguments");
1522 structured_type.components().emplace_back(ID_int,
java_int_type());
1523 structured_type.components().emplace_back(ID_float,
java_float_type());
1524 structured_type.components().emplace_back(ID_char,
java_char_type());
1527 structured_type.components().emplace_back(
"hashcode",
java_int_type());
1529 structured_type.components().emplace_back(
"date_time",
java_int_type());
1533 std::vector<exprt> processed_args;
1534 processed_args.push_back(args[0]);
1536 processed_args.push_back(
1538 args[1], i, structured_type,
loc, function_id, symbol_table, code));
1541 ID_cprover_string_format_func, processed_args,
loc, symbol_table, code);
1546 java_string, string_expr, symbol_table),
1571 const symbol_exprt this_obj(params[0].get_identifier(), params[0].type());
1581 class_type,
"class_symbol",
"class_symbol",
loc, ID_java, symbol_table);
1588 "@class_identifier",
1593 ID_cprover_string_literal_func,
1602 ID_cprover_string_substring_func,
1610 symbol_table.lookup_ref(
"java::java.lang.String").type);
1612 string_ptr_type,
loc, function_id, symbol_table, code);
1620 "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
1621 fun_call.
lhs()=class1;
1622 fun_call.
arguments().push_back(string1);
1654 function_name, args, type.
return_type(), symbol_table),
1730 string_expr, arg0,
loc, symbol_table, code);
1772 symbol_exprt arg1(params[1].get_identifier(), params[1].type());
1774 string_expr, arg1,
loc, symbol_table, code);
1777 symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1810 args.size() == 4,
"process_parameters preserves number of arguments");
1819 ID_cprover_string_substring_func,
1820 {args[1], args[2],
plus_exprt(args[2], args[3])},
1826 symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1854 symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1859 ret.add_source_location() =
loc;
1868 if(map->count(function_id) != 0)
1874 template <
typename TMap,
typename TContainer>
1878 std::is_same<
typename TMap::key_type,
1879 typename TContainer::value_type>::value,
1880 "TContainer value_type doesn't match TMap key_type");
1884 std::inserter(container, container.begin()),
1885 [](
const typename TMap::value_type &pair) {
return pair.first; });
1889 std::unordered_set<irep_idt> &methods)
const 1919 it_id->second, type,
loc, symbol_table);
1924 it_id->second, type,
loc, symbol_table);
1929 it_id->second, type,
loc, symbol_table);
1934 it_id->second, type,
loc, symbol_table);
1938 return it->second(type,
loc, function_id, symbol_table);
1955 string_types = std::unordered_set<irep_idt>{
"java.lang.String",
1956 "java.lang.StringBuilder",
1957 "java.lang.CharSequence",
1958 "java.lang.StringBuffer"};
1976 std::placeholders::_1,
1977 std::placeholders::_2,
1978 std::placeholders::_3,
1979 std::placeholders::_4);
1981 [
"java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1984 std::placeholders::_1,
1985 std::placeholders::_2,
1986 std::placeholders::_3,
1987 std::placeholders::_4);
1991 std::placeholders::_1,
1992 std::placeholders::_2,
1993 std::placeholders::_3,
1994 std::placeholders::_4);
1996 [
"java::java.lang.String.<init>:()V"]=
1997 ID_cprover_string_empty_string_func;
2002 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
2003 ID_cprover_string_char_at_func;
2005 [
"java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
2006 ID_cprover_string_code_point_at_func;
2008 [
"java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
2009 ID_cprover_string_code_point_before_func;
2011 [
"java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
2012 ID_cprover_string_code_point_count_func;
2014 [
"java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
2015 ID_cprover_string_compare_to_func;
2017 [
"java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
2018 ID_cprover_string_concat_func;
2020 [
"java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
2021 ID_cprover_string_contains_func;
2023 [
"java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]=
2024 ID_cprover_string_copy_func;
2026 [
"java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]=
2027 ID_cprover_string_copy_func;
2029 [
"java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
2030 ID_cprover_string_endswith_func;
2036 std::placeholders::_1,
2037 std::placeholders::_2,
2038 std::placeholders::_3,
2039 std::placeholders::_4);
2041 [
"java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
2042 ID_cprover_string_equals_ignore_case_func;
2044 [
"java::java.lang.String.format:(Ljava/lang/String;[Ljava/lang/Object;)" 2045 "Ljava/lang/String;"] =
2049 std::placeholders::_1,
2050 std::placeholders::_2,
2051 std::placeholders::_3,
2052 std::placeholders::_4);
2054 [
"java::java.lang.String.hashCode:()I"]=
2055 ID_cprover_string_hash_code_func;
2057 [
"java::java.lang.String.indexOf:(I)I"]=
2058 ID_cprover_string_index_of_func;
2060 [
"java::java.lang.String.indexOf:(II)I"]=
2061 ID_cprover_string_index_of_func;
2063 [
"java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
2064 ID_cprover_string_index_of_func;
2066 [
"java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
2067 ID_cprover_string_index_of_func;
2069 [
"java::java.lang.String.intern:()Ljava/lang/String;"]=
2070 ID_cprover_string_intern_func;
2072 [
"java::java.lang.String.isEmpty:()Z"]=
2073 ID_cprover_string_is_empty_func;
2075 [
"java::java.lang.String.lastIndexOf:(I)I"]=
2076 ID_cprover_string_last_index_of_func;
2078 [
"java::java.lang.String.lastIndexOf:(II)I"]=
2079 ID_cprover_string_last_index_of_func;
2081 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
2082 ID_cprover_string_last_index_of_func;
2084 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
2085 ID_cprover_string_last_index_of_func;
2089 std::placeholders::_1,
2090 std::placeholders::_2,
2091 std::placeholders::_3,
2092 std::placeholders::_4);
2094 [
"java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/" 2095 "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
2097 [
"java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
2098 ID_cprover_string_replace_func;
2100 [
"java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]=
2101 ID_cprover_string_replace_func;
2103 [
"java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
2104 ID_cprover_string_startswith_func;
2106 [
"java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
2107 ID_cprover_string_startswith_func;
2109 [
"java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/" 2110 "lang/CharSequence;"] = ID_cprover_string_substring_func;
2114 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;II)" 2115 "Ljava/lang/String;"]=
2116 ID_cprover_string_substring_func;
2118 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;I)" 2119 "Ljava/lang/String;"]=
2120 ID_cprover_string_substring_func;
2122 [
"java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
2123 ID_cprover_string_to_lower_case_func;
2128 std::placeholders::_1,
2129 std::placeholders::_2,
2130 std::placeholders::_3,
2131 std::placeholders::_4);
2133 [
"java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
2134 ID_cprover_string_to_upper_case_func;
2136 [
"java::java.lang.String.trim:()Ljava/lang/String;"]=
2137 ID_cprover_string_trim_func;
2139 [
"java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]=
2140 ID_cprover_string_of_bool_func;
2142 [
"java::java.lang.String.valueOf:(C)Ljava/lang/String;"]=
2143 ID_cprover_string_of_char_func;
2148 std::placeholders::_1,
2149 std::placeholders::_2,
2150 std::placeholders::_3,
2151 std::placeholders::_4);
2156 std::placeholders::_1,
2157 std::placeholders::_2,
2158 std::placeholders::_3,
2159 std::placeholders::_4);
2161 [
"java::java.lang.String.valueOf:(I)Ljava/lang/String;"]=
2162 ID_cprover_string_of_int_func;
2164 [
"java::java.lang.String.valueOf:(J)Ljava/lang/String;"]=
2165 ID_cprover_string_of_long_func;
2169 [
"java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
2172 std::placeholders::_1,
2173 std::placeholders::_2,
2174 std::placeholders::_3,
2175 std::placeholders::_4);
2177 [
"java::java.lang.StringBuilder.<init>:()V"]=
2178 ID_cprover_string_empty_string_func;
2181 [
"java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
2182 ID_cprover_string_concat_char_func;
2184 [
"java::java.lang.StringBuilder.append:([C)Ljava/lang/StringBuilder;"] =
2185 ID_cprover_string_concat_func;
2187 [
"java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] =
2188 ID_cprover_string_concat_double_func;
2190 [
"java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/" 2191 "lang/CharSequence;II)" 2192 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2194 [
"java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)" 2195 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2197 [
"java::java.lang.StringBuilder.append:(Ljava/lang/String;)" 2198 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2200 [
"java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;"]=
2201 ID_cprover_string_concat_bool_func;
2203 [
"java::java.lang.StringBuilder.appendCodePoint:(I)" 2204 "Ljava/lang/StringBuilder;"]=
2205 ID_cprover_string_concat_code_point_func;
2207 [
"java::java.lang.StringBuilder.charAt:(I)C"]=
2208 ID_cprover_string_char_at_func;
2210 [
"java::java.lang.StringBuilder.codePointAt:(I)I"]=
2211 ID_cprover_string_code_point_at_func;
2213 [
"java::java.lang.StringBuilder.codePointBefore:(I)I"]=
2214 ID_cprover_string_code_point_before_func;
2216 [
"java::java.lang.StringBuilder.codePointCount:(II)I"]=
2217 ID_cprover_string_code_point_count_func;
2219 [
"java::org.cprover.CProverString.delete:(Ljava/lang/" 2220 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2221 ID_cprover_string_delete_func;
2223 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" 2224 "StringBuilder;I)Ljava/lang/StringBuilder;"] =
2225 ID_cprover_string_delete_char_at_func;
2227 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2228 "StringBuilder;IC)Ljava/lang/StringBuilder;"] =
2229 ID_cprover_string_insert_char_func;
2231 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2232 "StringBuilder;IZ)Ljava/lang/StringBuilder;"] =
2233 ID_cprover_string_insert_bool_func;
2235 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2236 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2237 ID_cprover_string_insert_int_func;
2239 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2240 "StringBuilder;IJ)Ljava/lang/StringBuilder;"] =
2241 ID_cprover_string_insert_long_func;
2243 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/" 2244 "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
2248 std::placeholders::_1,
2249 std::placeholders::_2,
2250 std::placeholders::_3,
2251 std::placeholders::_4);
2253 [
"java::java.lang.StringBuilder.setCharAt:(IC)V"]=
2254 ID_cprover_string_char_set_func;
2256 [
"java::java.lang.StringBuilder.setLength:(I)V"]=
2257 ID_cprover_string_set_length_func;
2259 [
"java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
2260 ID_cprover_string_substring_func;
2262 [
"java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
2263 ID_cprover_string_substring_func;
2265 [
"java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
2268 std::placeholders::_1,
2269 std::placeholders::_2,
2270 std::placeholders::_3,
2271 std::placeholders::_4);
2275 [
"java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
2278 std::placeholders::_1,
2279 std::placeholders::_2,
2280 std::placeholders::_3,
2281 std::placeholders::_4);
2283 [
"java::java.lang.StringBuffer.<init>:()V"]=
2284 ID_cprover_string_empty_string_func;
2287 [
"java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
2288 ID_cprover_string_concat_char_func;
2290 [
"java::java.lang.StringBuffer.append:(D)Ljava/lang/StringBuffer;"]=
2291 ID_cprover_string_concat_double_func;
2293 [
"java::java.lang.StringBuffer.append:(F)Ljava/lang/StringBuffer;"]=
2294 ID_cprover_string_concat_float_func;
2296 [
"java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"]=
2297 ID_cprover_string_concat_int_func;
2299 [
"java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]=
2300 ID_cprover_string_concat_long_func;
2302 [
"java::java.lang.StringBuffer.append:(Ljava/lang/String;)" 2303 "Ljava/lang/StringBuffer;"]=
2304 ID_cprover_string_concat_func;
2306 [
"java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)" 2307 "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
2309 [
"java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;"] =
2310 ID_cprover_string_concat_bool_func;
2312 [
"java::java.lang.StringBuffer.appendCodePoint:(I)" 2313 "Ljava/lang/StringBuffer;"]=
2314 ID_cprover_string_concat_code_point_func;
2316 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
2317 ID_cprover_string_char_at_func;
2319 [
"java::java.lang.StringBuffer.codePointAt:(I)I"]=
2320 ID_cprover_string_code_point_at_func;
2322 [
"java::java.lang.StringBuffer.codePointBefore:(I)I"]=
2323 ID_cprover_string_code_point_before_func;
2325 [
"java::java.lang.StringBuffer.codePointCount:(II)I"]=
2326 ID_cprover_string_code_point_count_func;
2328 [
"java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/" 2329 "lang/StringBuffer;"] = ID_cprover_string_delete_func;
2331 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" 2332 "StringBufferI)Ljava/lang/StringBuffer;"] =
2333 ID_cprover_string_delete_char_at_func;
2335 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IC)Ljava/" 2336 "lang/StringBuffer;"] = ID_cprover_string_insert_char_func;
2338 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;II)Ljava/" 2339 "lang/StringBuffer;"] = ID_cprover_string_insert_int_func;
2341 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IJ)Ljava/" 2342 "lang/StringBuffer;"] = ID_cprover_string_insert_long_func;
2344 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;ILjava/" 2345 "lang/String;)Ljava/lang/StringBuffer;"] = ID_cprover_string_insert_func;
2347 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IZ)Ljava/" 2348 "lang/StringBuffer;"] = ID_cprover_string_insert_bool_func;
2350 [
"java::java.lang.StringBuffer.length:()I"]=
2353 [
"java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
2354 ID_cprover_string_char_set_func;
2356 [
"java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] =
2357 ID_cprover_string_set_length_func;
2359 [
"java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
2360 ID_cprover_string_substring_func;
2362 [
"java::org.cprover.CProverString.substring:(Ljava/Lang/" 2363 "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
2365 [
"java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
2368 std::placeholders::_1,
2369 std::placeholders::_2,
2370 std::placeholders::_3,
2371 std::placeholders::_4);
2375 [
"java::java.lang.CharSequence.charAt:(I)C"]=
2376 ID_cprover_string_char_at_func;
2378 [
"java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
2381 std::placeholders::_1,
2382 std::placeholders::_2,
2383 std::placeholders::_3,
2384 std::placeholders::_4);
2386 [
"java::java.lang.CharSequence.length:()I"]=
2394 std::placeholders::_1,
2395 std::placeholders::_2,
2396 std::placeholders::_3,
2397 std::placeholders::_4);
2399 [
"java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
2400 ID_cprover_string_parse_int_func;
2402 [
"java::java.lang.Integer.parseInt:(Ljava/lang/String;I)I"]=
2403 ID_cprover_string_parse_int_func;
2405 [
"java::java.lang.Long.parseLong:(Ljava/lang/String;)J"]=
2406 ID_cprover_string_parse_int_func;
2408 [
"java::java.lang.Long.parseLong:(Ljava/lang/String;I)J"]=
2409 ID_cprover_string_parse_int_func;
2411 [
"java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
2412 ID_cprover_string_of_int_hex_func;
2414 [
"java::java.lang.Integer.toString:(I)Ljava/lang/String;"]=
2415 ID_cprover_string_of_int_func;
2417 [
"java::java.lang.Integer.toString:(II)Ljava/lang/String;"]=
2418 ID_cprover_string_of_int_func;
2420 [
"java::java.lang.Long.toString:(J)Ljava/lang/String;"]=
2421 ID_cprover_string_of_int_func;
2423 [
"java::java.lang.Long.toString:(JI)Ljava/lang/String;"]=
2424 ID_cprover_string_of_int_func;
2429 std::placeholders::_1,
2430 std::placeholders::_2,
2431 std::placeholders::_3,
2432 std::placeholders::_4);
const irep_idt & get_name() const
The type of an expression.
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...
const codet & then_case() const
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
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)
codet make_equals_function_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.equals(Object) function.
A generic 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...
static bool is_java_string_pointer_type(const typet &type)
typet java_boolean_type()
static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the data component.
constant_exprt to_expr() const
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
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.
const exprt & cond() const
Evaluates to true if the operand is infinite.
irep_idt get_tag(const typet &type)
reference_typet java_reference_type(const typet &subtype)
const exprt & content() const
void copy_to_operands(const exprt &expr)
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.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
The null pointer constant.
codet 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.
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
The trinary if-then-else operator.
static bool is_java_char_sequence_pointer_type(const typet &type)
typet string_data_type(const symbol_tablet &symbol_table)
irep_idt pretty_name
Language-specific display name.
std::unordered_set< irep_idt > string_types
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
A constant literal expression.
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
#define CHECK_RETURN(CONDITION)
static mstreamt & eom(mstreamt &m)
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 bool is_java_string_buffer_pointer_type(const typet &type)
#define INVARIANT(CONDITION, REASON)
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
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 reference into the symbol table.
A 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.
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
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
codet 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.
refined_string_exprt & to_string_expr(exprt &expr)
exprt get_object_at_index(const exprt &argv, std::size_t index)
Helper for format function.
#define PRECONDITION(CONDITION)
A side effect that returns a non-deterministically chosen value.
void set_tag(const irep_idt &tag)
void from_float(const float f)
typet string_length_type()
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 generic 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...
typet component_type(const irep_idt &component_name) const
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.
codet 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.
codet make_init_from_array_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 constructor from a char array.
codet code_assign_string_expr_to_java_string(const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table)
Produce code for an assignemnt of a string expr to a Java string.
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
codet 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.
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)
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.
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.
const java_method_typet & to_java_method_type(const typet &type)
static typet get_length_type(const typet &type, const symbol_tablet &symbol_table)
Finds the type of the length component.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
exprt 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...
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.
std::size_t component_number(const irep_idt &component_name) const
codet 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.
codet 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...
codet 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.
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
character_refine_preprocesst character_preprocess
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.
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
static bool implements_java_char_sequence_pointer(const typet &type)
exprt allocate_fresh_array(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_tablet &symbol_table, code_blockt &code)
declare a new character array and allocate it
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 generic typet to a pointer_typet.
codet 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.
A statement in a programming language.
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)
codet 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...
codet 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. ...
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
codet 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 ignore_first_arg=true)
Generate the goto code for string initialization.
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
const codet & else_case() const
const irep_idt & get_identifier() const
const typet & return_type() const
codet code_assign_components_to_java_string(const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table)
Produce code for an assignment of a string expr to a Java string.
const irep_idt & get_identifier() const
void add_base(const typet &base)
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
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.
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...