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);
226 string_type.
components()[0].set_name(
"@java.lang.Object");
227 string_type.
components()[0].set_pretty_name(
"@java.lang.Object");
229 string_type.
components()[1].set_name(
"length");
230 string_type.
components()[1].set_pretty_name(
"length");
233 string_type.
components()[2].set_pretty_name(
"data");
239 for(
const irep_idt &base_name : bases)
244 symbolt *string_symbol=
nullptr;
245 symbol_table.
move(tmp_string_symbol, string_symbol);
248 string_symbol->
type=string_type;
250 string_symbol->
mode = ID_java;
265 "cprover_string_array",
266 "cprover_string_array",
288 for(
const auto &p : params)
312 const exprt &expr_to_process,
321 string_expr, expr_to_process,
loc, symbol_table, init_code);
343 for(
const auto &p : operands)
374 const exprt &op0=operands[0];
375 const exprt &op1 = operands[1];
397 if(type.
id()==ID_symbol)
416 if(type.
id()==ID_symbol)
454 const exprt &array_pointer,
465 array_data.type(),
"char_array",
"char_array",
loc, ID_java, symbol_table);
478 string_expr.
content(), inf_array, symbol_table,
loc, code);
495 type,
"cprover_string",
"cprover_string",
loc, ID_java, symbol_table);
513 "cprover_string_length",
514 "cprover_string_length",
522 "cprover_string_content",
523 "cprover_string_content",
552 exprt nondet_array_expr =
559 array_pointer, nondet_array_expr, symbol_table,
loc, code);
562 nondet_array_expr, str.
length(), symbol_table,
loc, code);
603 array, symbol_table,
loc, function_id, code);
623 function_name, arguments, lhs.
type(), symbol_table);
643 function_name, arguments, type, symbol_table);
662 "nondet_infinite_array",
663 "nondet_infinite_array",
682 const exprt &pointer,
697 exprt return_expr = return_sym.symbol_expr();
702 ID_cprover_associate_array_to_pointer_func,
734 ID_cprover_associate_length_to_array_func,
751 const exprt &pointer,
761 const exprt return_expr = return_sym.symbol_expr();
767 ID_cprover_string_constrain_characters_func,
768 {length, pointer, char_set_expr},
799 std::string(
"return_code_") + function_name.
c_str(),
800 std::string(
"return_code_") + function_name.
c_str(),
812 args.push_back(string_expr.
length());
813 args.push_back(string_expr.
content());
814 args.insert(args.end(), arguments.begin(), arguments.end());
819 return_code, function_name, args, symbol_table),
836 const exprt &rhs_array,
837 const exprt &rhs_length,
844 const symbolt &jlo_symbol=*symbol_table.
lookup(
"java::java.lang.Object");
852 struct_rhs.copy_to_operands(rhs_length);
853 struct_rhs.copy_to_operands(rhs_array);
909 rhs_length.
set(ID_mode, ID_java);
929 const std::string &s,
936 ID_cprover_string_literal_func, {expr},
loc, symbol_table, code);
983 return_type,
"string_equals",
"str_eq",
loc, ID_java, symbol_table);
989 ID_cprover_string_equal_func, args, return_type, symbol_table);
992 return instance_case;
1013 const symbol_exprt arg(params[0].get_identifier(), params[0].type());
1029 std::vector<exprt> condition_list;
1030 std::vector<refined_string_exprt> string_expr_list;
1035 ID_cprover_string_of_float_scientific_notation_func,
1040 string_expr_list.push_back(sci_notation);
1047 ID_cprover_string_concat_func,
1048 {minus_sign, sci_notation},
1052 string_expr_list.push_back(neg_sci_notation);
1058 string_expr_list.push_back(nan);
1065 string_expr_list.push_back(infinity);
1071 string_expr_list.push_back(minus_infinity);
1086 condition_list.push_back(is_simple_float);
1089 ID_cprover_string_of_float_func, {arg},
loc, symbol_table, code);
1090 string_expr_list.push_back(simple_notation);
1096 condition_list.push_back(is_neg_simple_float);
1099 ID_cprover_string_concat_func,
1100 {minus_sign, simple_notation},
1104 string_expr_list.push_back(neg_simple_notation);
1108 string_expr_list.size()==condition_list.size(),
1109 "number of created strings should correspond to number of conditions");
1114 str, string_expr_list[0], symbol_table);
1115 for(std::size_t i=1; i<condition_list.size(); i++)
1118 ife.
cond()=condition_list[i];
1120 str, string_expr_list[i], symbol_table);
1152 bool ignore_first_arg)
1158 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1159 if(ignore_first_arg)
1160 params.erase(params.begin());
1201 const symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1222 function_name, type,
loc, symbol_table,
false);
1246 const exprt &
object,
1255 if(type_name==ID_boolean)
1260 else if(type_name==ID_char)
1265 else if(type_name==ID_byte)
1270 else if(type_name==ID_short)
1275 else if(type_name==ID_int)
1280 else if(type_name==ID_long)
1285 else if(type_name==ID_float)
1290 else if(type_name==ID_double)
1295 else if(type_name==ID_void)
1300 DATA_INVARIANT(object_type.has_value(),
"must have symbol for primitive");
1303 std::string aux_name=
"tmp_"+
id2string(type_name);
1305 value_type, aux_name, aux_name,
loc, ID_java, symbol_table);
1311 const auto maybe_symbol =
1312 symbol_table.
lookup(object_type->get_identifier()))
1329 warning() << object_type->get_identifier()
1330 <<
" not available to format function" <<
eom;
1350 member_exprt data_member(deref_objs,
"data", pointer_of_pointer);
1354 data_pointer_plus_index, data_pointer_plus_index.type().subtype());
1355 return data_at_index;
1403 std::list<exprt> field_exprs;
1404 for(
const auto & comp : structured_type.
components())
1406 const irep_idt &name=comp.get_name();
1407 const typet &type=comp.type();
1409 if(name!=
"string_expr")
1411 std::string tmp_name=
"tmp_"+
id2string(name);
1413 type,
id2string(function_id), tmp_name,
loc, ID_java, symbol_table);
1421 field_exprs.push_back(field_expr);
1436 arg_i, symbol_table,
loc, function_id, code);
1451 for(
const auto &comp : structured_type.
components())
1453 const irep_idt &name=comp.get_name();
1454 exprt field_expr=field_exprs.front();
1455 field_exprs.pop_front();
1457 if(name==
"string_expr")
1469 else if(name==ID_int || name==ID_float || name==ID_char || name==ID_boolean)
1472 arg_i, name,
loc, symbol_table, code_not_null);
1481 code.
add(code_not_null,
loc);
1482 return arg_i_struct;
1506 INVARIANT(args.size()==2,
"String.format should have two arguments");
1513 structured_type.components().emplace_back(ID_int,
java_int_type());
1514 structured_type.components().emplace_back(ID_float,
java_float_type());
1515 structured_type.components().emplace_back(ID_char,
java_char_type());
1518 structured_type.components().emplace_back(
"hashcode",
java_int_type());
1520 structured_type.components().emplace_back(
"date_time",
java_int_type());
1524 std::vector<exprt> processed_args;
1525 processed_args.push_back(args[0]);
1527 processed_args.push_back(
1529 args[1], i, structured_type,
loc, function_id, symbol_table, code));
1532 ID_cprover_string_format_func, processed_args,
loc, symbol_table, code);
1537 java_string, string_expr, symbol_table),
1562 const symbol_exprt this_obj(params[0].get_identifier(), params[0].type());
1572 class_type,
"class_symbol",
"class_symbol",
loc, ID_java, symbol_table);
1579 "@class_identifier",
1584 ID_cprover_string_literal_func,
1593 ID_cprover_string_substring_func,
1601 symbol_table.lookup_ref(
"java::java.lang.String").type);
1603 string_ptr_type,
loc, function_id, symbol_table, code);
1611 "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
1612 fun_call.
lhs()=class1;
1613 fun_call.
arguments().push_back(string1);
1644 function_name, args, type.
return_type(), symbol_table),
1720 string_expr, arg0,
loc, symbol_table, code);
1759 symbol_exprt arg1(params[1].get_identifier(), params[1].type());
1761 string_expr, arg1,
loc, symbol_table, code);
1764 symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1794 args.size() == 4,
"process_parameters preserves number of arguments");
1803 ID_cprover_string_substring_func,
1804 {args[1], args[2],
plus_exprt(args[2], args[3])},
1810 symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1835 symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
1845 if(map->count(function_id) != 0)
1851 template <
typename TMap,
typename TContainer>
1855 std::is_same<
typename TMap::key_type,
1856 typename TContainer::value_type>::value,
1857 "TContainer value_type doesn't match TMap key_type");
1861 std::inserter(container, container.begin()),
1862 [](
const typename TMap::value_type &pair) {
return pair.first; });
1866 std::unordered_set<irep_idt> &methods)
const 1896 it_id->second, type,
loc, symbol_table);
1901 it_id->second, type,
loc, symbol_table);
1906 it_id->second, type,
loc, symbol_table);
1911 it_id->second, type,
loc, symbol_table);
1915 return it->second(type,
loc, function_id, symbol_table);
1932 string_types = std::unordered_set<irep_idt>{
"java.lang.String",
1933 "java.lang.StringBuilder",
1934 "java.lang.CharSequence",
1935 "java.lang.StringBuffer"};
1953 std::placeholders::_1,
1954 std::placeholders::_2,
1955 std::placeholders::_3,
1956 std::placeholders::_4);
1958 [
"java::java.lang.String.<init>:(Ljava/lang/StringBuilder;)V"] = std::bind(
1961 std::placeholders::_1,
1962 std::placeholders::_2,
1963 std::placeholders::_3,
1964 std::placeholders::_4);
1968 std::placeholders::_1,
1969 std::placeholders::_2,
1970 std::placeholders::_3,
1971 std::placeholders::_4);
1973 [
"java::java.lang.String.<init>:()V"]=
1974 ID_cprover_string_empty_string_func;
1979 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
1980 ID_cprover_string_char_at_func;
1982 [
"java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
1983 ID_cprover_string_code_point_at_func;
1985 [
"java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
1986 ID_cprover_string_code_point_before_func;
1988 [
"java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
1989 ID_cprover_string_code_point_count_func;
1991 [
"java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
1992 ID_cprover_string_compare_to_func;
1994 [
"java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]=
1995 ID_cprover_string_concat_func;
1997 [
"java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
1998 ID_cprover_string_contains_func;
2000 [
"java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]=
2001 ID_cprover_string_copy_func;
2003 [
"java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]=
2004 ID_cprover_string_copy_func;
2006 [
"java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
2007 ID_cprover_string_endswith_func;
2013 std::placeholders::_1,
2014 std::placeholders::_2,
2015 std::placeholders::_3,
2016 std::placeholders::_4);
2018 [
"java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]=
2019 ID_cprover_string_equals_ignore_case_func;
2021 [
"java::java.lang.String.format:(Ljava/lang/String;[Ljava/lang/Object;)" 2022 "Ljava/lang/String;"] =
2026 std::placeholders::_1,
2027 std::placeholders::_2,
2028 std::placeholders::_3,
2029 std::placeholders::_4);
2031 [
"java::java.lang.String.hashCode:()I"]=
2032 ID_cprover_string_hash_code_func;
2034 [
"java::java.lang.String.indexOf:(I)I"]=
2035 ID_cprover_string_index_of_func;
2037 [
"java::java.lang.String.indexOf:(II)I"]=
2038 ID_cprover_string_index_of_func;
2040 [
"java::java.lang.String.indexOf:(Ljava/lang/String;)I"]=
2041 ID_cprover_string_index_of_func;
2043 [
"java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]=
2044 ID_cprover_string_index_of_func;
2046 [
"java::java.lang.String.intern:()Ljava/lang/String;"]=
2047 ID_cprover_string_intern_func;
2049 [
"java::java.lang.String.isEmpty:()Z"]=
2050 ID_cprover_string_is_empty_func;
2052 [
"java::java.lang.String.lastIndexOf:(I)I"]=
2053 ID_cprover_string_last_index_of_func;
2055 [
"java::java.lang.String.lastIndexOf:(II)I"]=
2056 ID_cprover_string_last_index_of_func;
2058 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]=
2059 ID_cprover_string_last_index_of_func;
2061 [
"java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]=
2062 ID_cprover_string_last_index_of_func;
2066 std::placeholders::_1,
2067 std::placeholders::_2,
2068 std::placeholders::_3,
2069 std::placeholders::_4);
2071 [
"java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/" 2072 "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
2074 [
"java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
2075 ID_cprover_string_replace_func;
2077 [
"java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]=
2078 ID_cprover_string_replace_func;
2080 [
"java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]=
2081 ID_cprover_string_startswith_func;
2083 [
"java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
2084 ID_cprover_string_startswith_func;
2086 [
"java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/" 2087 "lang/CharSequence;"] = ID_cprover_string_substring_func;
2091 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;II)" 2092 "Ljava/lang/String;"]=
2093 ID_cprover_string_substring_func;
2095 [
"java::org.cprover.CProverString.substring:(Ljava/lang/String;I)" 2096 "Ljava/lang/String;"]=
2097 ID_cprover_string_substring_func;
2099 [
"java::java.lang.String.toLowerCase:()Ljava/lang/String;"]=
2100 ID_cprover_string_to_lower_case_func;
2105 std::placeholders::_1,
2106 std::placeholders::_2,
2107 std::placeholders::_3,
2108 std::placeholders::_4);
2110 [
"java::java.lang.String.toUpperCase:()Ljava/lang/String;"]=
2111 ID_cprover_string_to_upper_case_func;
2113 [
"java::java.lang.String.trim:()Ljava/lang/String;"]=
2114 ID_cprover_string_trim_func;
2116 [
"java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]=
2117 ID_cprover_string_of_bool_func;
2119 [
"java::java.lang.String.valueOf:(C)Ljava/lang/String;"]=
2120 ID_cprover_string_of_char_func;
2125 std::placeholders::_1,
2126 std::placeholders::_2,
2127 std::placeholders::_3,
2128 std::placeholders::_4);
2133 std::placeholders::_1,
2134 std::placeholders::_2,
2135 std::placeholders::_3,
2136 std::placeholders::_4);
2138 [
"java::java.lang.String.valueOf:(I)Ljava/lang/String;"]=
2139 ID_cprover_string_of_int_func;
2141 [
"java::java.lang.String.valueOf:(J)Ljava/lang/String;"]=
2142 ID_cprover_string_of_long_func;
2146 [
"java::java.lang.StringBuilder.<init>:(Ljava/lang/String;)V"] = std::bind(
2149 std::placeholders::_1,
2150 std::placeholders::_2,
2151 std::placeholders::_3,
2152 std::placeholders::_4);
2154 [
"java::java.lang.StringBuilder.<init>:()V"]=
2155 ID_cprover_string_empty_string_func;
2158 [
"java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
2159 ID_cprover_string_concat_char_func;
2161 [
"java::java.lang.StringBuilder.append:([C)Ljava/lang/StringBuilder;"] =
2162 ID_cprover_string_concat_func;
2164 [
"java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] =
2165 ID_cprover_string_concat_double_func;
2167 [
"java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/" 2168 "lang/CharSequence;II)" 2169 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2171 [
"java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)" 2172 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2174 [
"java::java.lang.StringBuilder.append:(Ljava/lang/String;)" 2175 "Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2177 [
"java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;"]=
2178 ID_cprover_string_concat_bool_func;
2180 [
"java::java.lang.StringBuilder.appendCodePoint:(I)" 2181 "Ljava/lang/StringBuilder;"]=
2182 ID_cprover_string_concat_code_point_func;
2184 [
"java::java.lang.StringBuilder.charAt:(I)C"]=
2185 ID_cprover_string_char_at_func;
2187 [
"java::java.lang.StringBuilder.codePointAt:(I)I"]=
2188 ID_cprover_string_code_point_at_func;
2190 [
"java::java.lang.StringBuilder.codePointBefore:(I)I"]=
2191 ID_cprover_string_code_point_before_func;
2193 [
"java::java.lang.StringBuilder.codePointCount:(II)I"]=
2194 ID_cprover_string_code_point_count_func;
2196 [
"java::org.cprover.CProverString.delete:(Ljava/lang/" 2197 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2198 ID_cprover_string_delete_func;
2200 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" 2201 "StringBuilder;I)Ljava/lang/StringBuilder;"] =
2202 ID_cprover_string_delete_char_at_func;
2204 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2205 "StringBuilder;IC)Ljava/lang/StringBuilder;"] =
2206 ID_cprover_string_insert_char_func;
2208 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2209 "StringBuilder;IZ)Ljava/lang/StringBuilder;"] =
2210 ID_cprover_string_insert_bool_func;
2212 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2213 "StringBuilder;II)Ljava/lang/StringBuilder;"] =
2214 ID_cprover_string_insert_int_func;
2216 [
"java::org.cprover.CProverString.insert:(Ljava/lang/" 2217 "StringBuilder;IJ)Ljava/lang/StringBuilder;"] =
2218 ID_cprover_string_insert_long_func;
2220 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/" 2221 "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
2225 std::placeholders::_1,
2226 std::placeholders::_2,
2227 std::placeholders::_3,
2228 std::placeholders::_4);
2230 [
"java::java.lang.StringBuilder.setCharAt:(IC)V"]=
2231 ID_cprover_string_char_set_func;
2233 [
"java::java.lang.StringBuilder.setLength:(I)V"]=
2234 ID_cprover_string_set_length_func;
2236 [
"java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]=
2237 ID_cprover_string_substring_func;
2239 [
"java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]=
2240 ID_cprover_string_substring_func;
2242 [
"java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind(
2245 std::placeholders::_1,
2246 std::placeholders::_2,
2247 std::placeholders::_3,
2248 std::placeholders::_4);
2252 [
"java::java.lang.StringBuffer.<init>:(Ljava/lang/String;)V"] = std::bind(
2255 std::placeholders::_1,
2256 std::placeholders::_2,
2257 std::placeholders::_3,
2258 std::placeholders::_4);
2260 [
"java::java.lang.StringBuffer.<init>:()V"]=
2261 ID_cprover_string_empty_string_func;
2264 [
"java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]=
2265 ID_cprover_string_concat_char_func;
2267 [
"java::java.lang.StringBuffer.append:(D)Ljava/lang/StringBuffer;"]=
2268 ID_cprover_string_concat_double_func;
2270 [
"java::java.lang.StringBuffer.append:(F)Ljava/lang/StringBuffer;"]=
2271 ID_cprover_string_concat_float_func;
2273 [
"java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"]=
2274 ID_cprover_string_concat_int_func;
2276 [
"java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]=
2277 ID_cprover_string_concat_long_func;
2279 [
"java::java.lang.StringBuffer.append:(Ljava/lang/String;)" 2280 "Ljava/lang/StringBuffer;"]=
2281 ID_cprover_string_concat_func;
2283 [
"java::java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)" 2284 "Ljava/lang/StringBuffer;"] = ID_cprover_string_concat_func;
2286 [
"java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;"] =
2287 ID_cprover_string_concat_bool_func;
2289 [
"java::java.lang.StringBuffer.appendCodePoint:(I)" 2290 "Ljava/lang/StringBuffer;"]=
2291 ID_cprover_string_concat_code_point_func;
2293 [
"java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
2294 ID_cprover_string_char_at_func;
2296 [
"java::java.lang.StringBuffer.codePointAt:(I)I"]=
2297 ID_cprover_string_code_point_at_func;
2299 [
"java::java.lang.StringBuffer.codePointBefore:(I)I"]=
2300 ID_cprover_string_code_point_before_func;
2302 [
"java::java.lang.StringBuffer.codePointCount:(II)I"]=
2303 ID_cprover_string_code_point_count_func;
2305 [
"java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/" 2306 "lang/StringBuffer;"] = ID_cprover_string_delete_func;
2308 [
"java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/" 2309 "StringBufferI)Ljava/lang/StringBuffer;"] =
2310 ID_cprover_string_delete_char_at_func;
2312 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IC)Ljava/" 2313 "lang/StringBuffer;"] = ID_cprover_string_insert_char_func;
2315 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;II)Ljava/" 2316 "lang/StringBuffer;"] = ID_cprover_string_insert_int_func;
2318 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IJ)Ljava/" 2319 "lang/StringBuffer;"] = ID_cprover_string_insert_long_func;
2321 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;ILjava/" 2322 "lang/String;)Ljava/lang/StringBuffer;"] = ID_cprover_string_insert_func;
2324 [
"java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IZ)Ljava/" 2325 "lang/StringBuffer;"] = ID_cprover_string_insert_bool_func;
2327 [
"java::java.lang.StringBuffer.length:()I"]=
2330 [
"java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
2331 ID_cprover_string_char_set_func;
2333 [
"java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] =
2334 ID_cprover_string_set_length_func;
2336 [
"java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
2337 ID_cprover_string_substring_func;
2339 [
"java::org.cprover.CProverString.substring:(Ljava/Lang/" 2340 "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
2342 [
"java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind(
2345 std::placeholders::_1,
2346 std::placeholders::_2,
2347 std::placeholders::_3,
2348 std::placeholders::_4);
2352 [
"java::java.lang.CharSequence.charAt:(I)C"]=
2353 ID_cprover_string_char_at_func;
2355 [
"java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind(
2358 std::placeholders::_1,
2359 std::placeholders::_2,
2360 std::placeholders::_3,
2361 std::placeholders::_4);
2363 [
"java::java.lang.CharSequence.length:()I"]=
2371 std::placeholders::_1,
2372 std::placeholders::_2,
2373 std::placeholders::_3,
2374 std::placeholders::_4);
2376 [
"java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
2377 ID_cprover_string_parse_int_func;
2379 [
"java::java.lang.Integer.parseInt:(Ljava/lang/String;I)I"]=
2380 ID_cprover_string_parse_int_func;
2382 [
"java::java.lang.Long.parseLong:(Ljava/lang/String;)J"]=
2383 ID_cprover_string_parse_int_func;
2385 [
"java::java.lang.Long.parseLong:(Ljava/lang/String;I)J"]=
2386 ID_cprover_string_parse_int_func;
2388 [
"java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
2389 ID_cprover_string_of_int_hex_func;
2391 [
"java::java.lang.Integer.toString:(I)Ljava/lang/String;"]=
2392 ID_cprover_string_of_int_func;
2394 [
"java::java.lang.Integer.toString:(II)Ljava/lang/String;"]=
2395 ID_cprover_string_of_int_func;
2397 [
"java::java.lang.Long.toString:(J)Ljava/lang/String;"]=
2398 ID_cprover_string_of_int_func;
2400 [
"java::java.lang.Long.toString:(JI)Ljava/lang/String;"]=
2401 ID_cprover_string_of_int_func;
2406 std::placeholders::_1,
2407 std::placeholders::_2,
2408 std::placeholders::_3,
2409 std::placeholders::_4);
codet make_copy_string_code(const code_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.
const irep_idt & get_name() const
The type of an expression.
irep_idt name
The unique identifier.
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)
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
exprt make_argument_for_format(const exprt &argv, int 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 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.
codet make_assign_function_from_call(const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Call a cprover internal function and assign the result to object this.
constant_exprt to_expr() const
codet make_init_from_array_code(const code_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.
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)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
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 make_assign_and_return_function_from_call(const irep_idt &function_name, const code_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. ...
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.
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
codet make_float_to_string_code(const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Provide code for the String.valueOf(F) function.
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.
codet make_copy_constructor_code(const code_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.
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
exprt::operandst process_parameters(const code_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.
refined_string_exprt & to_string_expr(exprt &expr)
#define PRECONDITION(CONDITION)
codet make_init_function_from_call(const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool ignore_first_arg=true)
Generate the goto code for string initialization.
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
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
void initialize_known_type_table()
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 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
void java_root_class_init(struct_exprt &jlo, const struct_typet &root_type, const bool lock, const irep_idt &class_identifier)
Adds members for an object of the root class (usually java.lang.Object).
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
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.
codet make_string_format_code(const code_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.
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.
codet make_function_from_call(const irep_idt &function_name, const code_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...
const parameterst & parameters() const
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
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
character_refine_preprocesst character_preprocess
codet make_object_get_class_code(const code_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.
irept & add(const irep_namet &name)
const exprt & length() const
codet make_string_length_code(const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for the String.length method.
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.
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)
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
const codet & else_case() const
const irep_idt & get_identifier() const
exprt get_object_at_index(const exprt &argv, int index)
Helper for format function.
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.
codet make_equals_function_code(const code_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.
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...
codet make_string_returning_function_from_call(const irep_idt &function_name, const code_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...