27 const std::string src,
28 const std::string class_name_prefix,
29 const char opening_bracket,
30 const char closing_bracket);
92 std::string subtype_str;
96 case 'b': subtype_str=
"byte";
break;
97 case 'f': subtype_str=
"float";
break;
98 case 'd': subtype_str=
"double";
break;
99 case 'i': subtype_str=
"int";
break;
100 case 'c': subtype_str=
"char";
break;
101 case 's': subtype_str=
"short";
break;
102 case 'z': subtype_str=
"boolean";
break;
103 case 'v': subtype_str=
"void";
break;
104 case 'j': subtype_str=
"long";
break;
105 case 'l': subtype_str=
"long";
break;
106 case 'a': subtype_str=
"reference";
break;
109 std::cout <<
"Unrecognised subtype str: " << subtype << std::endl;
114 irep_idt class_name=
"array["+subtype_str+
"]";
117 symbol_type.
set(ID_C_base_name, class_name);
130 "Symbol should have array tag");
131 return array_type.
find_type(ID_C_element_type);
182 if(new_type==expr.
type())
198 const std::string &type_arguments,
199 const std::string &class_name_prefix)
203 PRECONDITION(type_arguments[type_arguments.size() - 1] ==
'>');
208 std::vector<typet> type_arguments_types =
216 type_arguments_types.begin(),
217 type_arguments_types.end(),
222 is_reference(type),
"All generic type arguments should be references");
233 std::string class_name = src;
234 std::size_t f_pos = class_name.find(
'<', 1);
236 while(f_pos != std::string::npos)
239 if(e_pos == std::string::npos)
242 "Failed to find generic signature closing delimiter (or recursive " 248 class_name.erase(f_pos, e_pos - f_pos + 1);
251 f_pos = class_name.find(
'<', f_pos + 1);
268 std::string class_name = src.substr(1, src.size() - 2);
272 std::replace(class_name.begin(), class_name.end(),
'.',
'$');
273 std::replace(class_name.begin(), class_name.end(),
'/',
'.');
290 const std::string src,
291 const std::string class_name_prefix,
292 const char opening_bracket,
293 const char closing_bracket)
301 std::vector<typet> type_list;
302 for(std::size_t i = 1; i < src.size() - 1; i++)
305 while(i < src.size())
315 else if(src[i] ==
'[')
319 else if(src[i] ==
'T')
320 i = src.find(
';', i);
329 std::string sub_str = src.substr(start, i - start + 1);
333 type_list.push_back(new_type);
354 std::string identifier =
"java::" + container_class;
356 symbol_type.
set(ID_C_base_name, container_class);
358 std::size_t f_pos = src.find(
'<', 1);
359 if(f_pos != std::string::npos)
366 if(e_pos == std::string::npos)
368 "Parsing type with unmatched generic bracket: " + src);
371 result, src.substr(f_pos, e_pos - f_pos + 1), class_name_prefix);
374 f_pos = src.find(
'<', e_pos + 1);
375 }
while(f_pos != std::string::npos);
391 const std::string src,
392 size_t starting_point)
395 size_t next_semi_colon = src.find(
';', starting_point);
397 next_semi_colon != std::string::npos,
398 "There must be a semi-colon somewhere in the input");
399 size_t next_angle_bracket = src.find(
'<', starting_point);
401 while(next_angle_bracket < next_semi_colon)
406 end_bracket != std::string::npos,
"Must find matching angle bracket");
408 next_semi_colon = src.find(
';', end_bracket + 1);
409 next_angle_bracket = src.find(
'<', end_bracket + 1);
412 return next_semi_colon;
429 const std::string &src,
430 const std::string &class_name_prefix)
460 if(closing_generic==std::string::npos)
463 "Failed to find generic signature closing delimiter");
470 const size_t colon_pos = src.find(
':');
471 if(colon_pos != std::string::npos && colon_pos < closing_generic)
474 "Cannot currently parse bounds on generic types");
478 src.substr(closing_generic+1, std::string::npos), class_name_prefix);
485 method_type.
id()==ID_code,
486 "This should correspond to method signatures only");
492 std::size_t e_pos=src.rfind(
')');
493 if(e_pos==std::string::npos)
497 std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
499 std::vector<typet> param_types =
507 std::back_inserter(parameters),
510 return code_typet(std::move(parameters), std::move(return_type));
519 char subtype_letter=src[1];
523 if(subtype_letter==
'L' ||
524 subtype_letter==
'[' ||
528 tmp.
subtype().
set(ID_C_element_type, subtype);
544 INVARIANT(src[src.size()-1]==
';',
"Generic type name must end on ';'.");
546 irep_idt type_var_name(class_name_prefix+
"::"+src.substr(1, src.size()-2));
560 std::cout << class_name_prefix << std::endl;
585 else if(
id==ID_unsignedbv)
587 else if(
id==ID_floatbv)
595 else if(
id==ID_c_bool)
611 const std::string &class_name,
612 const std::string &src)
618 src[0]==
'<' && signature_end!=std::string::npos,
619 "Class signature has unexpected format");
620 std::string signature(src.substr(1, signature_end-1));
622 if(signature.find(
";:")!=std::string::npos)
627 std::vector<typet> types;
628 size_t var_sep=signature.find(
';');
629 while(var_sep!=std::string::npos)
631 size_t bound_sep=signature.find(
':');
632 INVARIANT(bound_sep!=std::string::npos,
"No bound for type variable.");
636 if(signature[bound_sep + 1] ==
':')
639 signature[bound_sep + 2] !=
':',
"Unknown bound for type variable.");
643 std::string type_var_name(
644 "java::"+class_name+
"::"+signature.substr(0, bound_sep));
645 std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep));
651 types.push_back(type_var_type);
652 signature=signature.substr(var_sep+1, std::string::npos);
653 var_sep=signature.find(
';');
661 std::string result=src;
662 for(std::string::iterator it=result.begin(); it!=result.end(); it++)
670 if(!
id.empty() &&
id[0]==
'[')
673 std::string class_name=id;
676 irep_idt identifier=
"java::"+class_name;
678 symbol_type.
set(ID_C_base_name, class_name);
698 bool correct_num_components=type.
components().size()==3;
699 if(!correct_num_components)
706 bool base_component_valid=
true;
707 base_component_valid&=base_class_component.
get_name()==
"@java.lang.Object";
709 bool length_component_valid=
true;
712 length_component_valid&=length_component.
get_name()==
"length";
715 bool data_component_valid=
true;
718 data_component_valid&=data_component.
get_name()==
"data";
719 data_component_valid&=data_component.
type().
id()==ID_pointer;
721 return correct_num_components &&
722 base_component_valid &&
723 length_component_valid &&
724 data_component_valid;
735 bool arrays_with_same_element_type =
true;
737 type1.
id() == ID_pointer && type2.
id() == ID_pointer &&
743 subtype_symbol1.
get_identifier() == subtype_symbol2.get_identifier() &&
746 const typet &array_element_type1 =
748 const typet &array_element_type2 =
751 arrays_with_same_element_type =
755 return (type1 == type2 && arrays_with_same_element_type);
760 std::set<irep_idt> &refs)
770 else if(t.
id() == ID_pointer)
776 else if(t.
id() == ID_code)
785 else if(t.
id() == ID_symbol)
806 const std::string &signature,
807 std::set<irep_idt> &refs)
812 if(signature[0] ==
'<')
817 for(
const auto &t : types)
822 else if(signature.find(
'*') == std::string::npos)
843 std::set<irep_idt> &refs)
859 const std::string &base_ref,
860 const std::string &class_name_prefix)
863 set(ID_C_java_generic_symbol,
true);
869 "identifier of "+type.
pretty()+
"\n and identifier of type "+
870 gen_base_type.
subtype().
pretty()+
"\ncreated by java_type_from_string for "+
871 base_ref+
" should be equal");
885 const auto &type_variable = type.
get_name();
887 for(std::size_t i = 0; i < generics.size(); ++i)
922 const irep_idt &
id = symbol_type.get_identifier();
937 std::ostringstream result;
const irep_idt & get_name() const
The type of an expression.
Fixed-width bit-vector with unsigned binary interpretation.
const std::string & id2string(const irep_idt &d)
void get_dependencies_from_generic_parameters_rec(const typet &t, std::set< irep_idt > &refs)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
optionalt< size_t > generic_type_index(const java_generic_parametert &type) const
Check if this symbol has the given generic type.
void get_dependencies_from_generic_parameters(const std::string &signature, std::set< irep_idt > &refs)
Collect information about generic type parameters from a given signature.
typet java_boolean_type()
const reference_typet & to_reference_type(const typet &type)
Cast a generic typet to a reference_typet.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
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)
bool is_java_generic_parameter(const typet &type)
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>. ...
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
std::vector< parametert > parameterst
const java_generic_parametert & to_java_generic_parameter(const typet &type)
const componentst & components() const
An exception that is raised for unsupported class signature.
#define CHECK_RETURN(CONDITION)
reference_typet java_array_type(const char subtype)
bool is_java_array_tag(const irep_idt &tag)
See above.
bool is_valid_java_array(const struct_typet &type)
Programmatic documentation of the structure of a Java array (of either primitives or references) type...
reference_typet java_lang_object_type()
#define INVARIANT(CONDITION, REASON)
static ieee_float_spect double_precision()
class floatbv_typet to_type() const
size_t find_closing_delimiter(const std::string &src, size_t open_pos, char open_char, char close_char)
Finds the corresponding closing delimiter to the given opening delimiter.
bool equal_java_types(const typet &type1, const typet &type2)
Compares the types, including checking element types if both types are arrays.
const generic_type_argumentst & generic_type_arguments() const
const irep_idt & id() const
typet java_type_from_string(const std::string &src, const std::string &class_name_prefix)
Transforms a string representation of a Java type into an internal type representation thereof...
A reference into the symbol table.
reference_typet reference_type(const typet &subtype)
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
std::string erase_type_arguments(const std::string &src)
Take a signature string and remove everything in angle brackets allowing for the type to be parsed no...
Fixed-width bit-vector with two's complement interpretation.
typet java_type_from_char(char t)
nonstd::optional< T > optionalt
reference_typet build_class_name(const std::string &src, const std::string &class_name_prefix)
For parsing a class type reference.
API to expression classes.
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
std::string pretty_java_type(const typet &type)
static ieee_float_spect single_precision()
#define PRECONDITION(CONDITION)
bool has_prefix(const std::string &s, const std::string &prefix)
size_t find_closing_semi_colon_for_reference_type(const std::string src, size_t starting_point)
Finds the closing semi-colon ending a ClassTypeSignature that starts at starting_point.
const generic_typest & generic_types() const
bool is_reference_type(const char t)
std::size_t get_width() const
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
std::vector< typet > parse_list_types(const std::string src, const std::string class_name_prefix, const char opening_bracket, const char closing_bracket)
Given a substring of a descriptor or signature that contains one or more types parse out the individu...
const java_generic_typet & to_java_generic_type(const typet &type)
std::string gather_full_class_name(const std::string &src)
Returns the full class name, skipping over the generics.
static std::string slash_to_dot(const std::string &src)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Base class for all expressions.
const typet & find_type(const irep_namet &name) const
const parameterst & parameters() const
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>...
const irep_idt get_name() const
void base_type(typet &type, const namespacet &ns)
typet java_array_element_type(const symbol_typet &array_type)
Return the type of the elements of a given java array type.
typet java_bytecode_promotion(const typet &type)
Java does not support byte/short return types. These are always promoted.
bool is_java_generic_type(const typet &type)
std::vector< typet > java_generic_type_from_string(const std::string &class_name, const std::string &src)
Converts the content of a generic class type into a vector of Java types, that is each type variable ...
java_generic_symbol_typet(const symbol_typet &type, const std::string &base_ref, const std::string &class_name_prefix)
Construct a generic symbol type by extending the symbol type type with generic types extracted from t...
const typet & subtype() const
symbol_typet java_classname(const std::string &id)
const typet & return_type() const
const irep_idt & get_identifier() const
char java_char_from_type(const typet &type)
void set(const irep_namet &name, const irep_idt &value)
void add_generic_type_information(java_generic_typet &generic_type, const std::string &type_arguments, const std::string &class_name_prefix)
Take a list of generic type arguments and parse them into the generic type.
std::string pretty_signature(const code_typet &code_type)