27 const std::string src,
28 const std::string class_name_prefix,
29 const char opening_bracket,
30 const char closing_bracket);
96 std::string subtype_str;
100 case 'b': subtype_str=
"byte";
break;
101 case 'f': subtype_str=
"float";
break;
102 case 'd': subtype_str=
"double";
break;
103 case 'i': subtype_str=
"int";
break;
104 case 'c': subtype_str=
"char";
break;
105 case 's': subtype_str=
"short";
break;
106 case 'z': subtype_str=
"boolean";
break;
107 case 'v': subtype_str=
"void";
break;
108 case 'j': subtype_str=
"long";
break;
109 case 'l': subtype_str=
"long";
break;
110 case 'a': subtype_str=
"reference";
break;
113 std::cout <<
"Unrecognised subtype str: " << subtype << std::endl;
118 irep_idt class_name=
"array["+subtype_str+
"]";
121 symbol_type.
set(ID_C_base_name, class_name);
133 "Symbol should have array tag");
134 return array_symbol.
find_type(ID_element_type);
143 "Symbol should have array tag");
144 return array_symbol.
add_type(ID_element_type);
224 if(new_type==expr.
type())
240 const std::string &type_arguments,
241 const std::string &class_name_prefix)
245 PRECONDITION(type_arguments[type_arguments.size() - 1] ==
'>');
250 std::vector<typet> type_arguments_types =
258 type_arguments_types.begin(),
259 type_arguments_types.end(),
264 is_reference(type),
"All generic type arguments should be references");
275 std::string class_name = src;
276 std::size_t f_pos = class_name.find(
'<', 1);
278 while(f_pos != std::string::npos)
281 if(e_pos == std::string::npos)
284 "Failed to find generic signature closing delimiter (or recursive " 290 class_name.erase(f_pos, e_pos - f_pos + 1);
293 f_pos = class_name.find(
'<', f_pos + 1);
310 std::string class_name = src.substr(1, src.size() - 2);
314 std::replace(class_name.begin(), class_name.end(),
'.',
'$');
315 std::replace(class_name.begin(), class_name.end(),
'/',
'.');
332 const std::string src,
333 const std::string class_name_prefix,
334 const char opening_bracket,
335 const char closing_bracket)
343 std::vector<typet> type_list;
344 for(std::size_t i = 1; i < src.size() - 1; i++)
347 while(i < src.size())
357 else if(src[i] ==
'[')
361 else if(src[i] ==
'T')
362 i = src.find(
';', i);
371 std::string sub_str = src.substr(start, i - start + 1);
375 type_list.push_back(new_type);
396 std::string identifier =
"java::" + container_class;
398 symbol_type.
set(ID_C_base_name, container_class);
400 std::size_t f_pos = src.find(
'<', 1);
401 if(f_pos != std::string::npos)
408 if(e_pos == std::string::npos)
410 "Parsing type with unmatched generic bracket: " + src);
413 result, src.substr(f_pos, e_pos - f_pos + 1), class_name_prefix);
416 f_pos = src.find(
'<', e_pos + 1);
417 }
while(f_pos != std::string::npos);
433 const std::string src,
434 size_t starting_point)
437 size_t next_semi_colon = src.find(
';', starting_point);
439 next_semi_colon != std::string::npos,
440 "There must be a semi-colon somewhere in the input");
441 size_t next_angle_bracket = src.find(
'<', starting_point);
443 while(next_angle_bracket < next_semi_colon)
448 end_bracket != std::string::npos,
"Must find matching angle bracket");
450 next_semi_colon = src.find(
';', end_bracket + 1);
451 next_angle_bracket = src.find(
'<', end_bracket + 1);
454 return next_semi_colon;
471 const std::string &src,
472 const std::string &class_name_prefix)
502 if(closing_generic==std::string::npos)
505 "Failed to find generic signature closing delimiter");
512 const size_t colon_pos = src.find(
':');
513 if(colon_pos != std::string::npos && colon_pos < closing_generic)
516 "Cannot currently parse bounds on generic types");
520 src.substr(closing_generic+1, std::string::npos), class_name_prefix);
527 method_type.
id()==ID_code,
528 "This should correspond to method signatures only");
534 std::size_t e_pos=src.rfind(
')');
535 if(e_pos==std::string::npos)
539 std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
541 std::vector<typet> param_types =
549 std::back_inserter(parameters),
561 char subtype_letter=src[1];
565 if(subtype_letter==
'L' ||
566 subtype_letter==
'[' ||
586 INVARIANT(src[src.size()-1]==
';',
"Generic type name must end on ';'.");
588 irep_idt type_var_name(class_name_prefix+
"::"+src.substr(1, src.size()-2));
602 std::cout << class_name_prefix << std::endl;
627 else if(
id==ID_unsignedbv)
629 else if(
id==ID_floatbv)
637 else if(
id==ID_c_bool)
653 const std::string &class_name,
654 const std::string &src)
660 src[0]==
'<' && signature_end!=std::string::npos,
661 "Class signature has unexpected format");
662 std::string signature(src.substr(1, signature_end-1));
664 if(signature.find(
";:")!=std::string::npos)
669 std::vector<typet> types;
670 size_t var_sep=signature.find(
';');
671 while(var_sep!=std::string::npos)
673 size_t bound_sep=signature.find(
':');
674 INVARIANT(bound_sep!=std::string::npos,
"No bound for type variable.");
678 if(signature[bound_sep + 1] ==
':')
681 signature[bound_sep + 2] !=
':',
"Unknown bound for type variable.");
685 std::string type_var_name(
686 "java::"+class_name+
"::"+signature.substr(0, bound_sep));
687 std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep));
693 types.push_back(type_var_type);
694 signature=signature.substr(var_sep+1, std::string::npos);
695 var_sep=signature.find(
';');
703 std::string result=src;
704 for(std::string::iterator it=result.begin(); it!=result.end(); it++)
712 if(!
id.empty() &&
id[0]==
'[')
715 std::string class_name=id;
718 irep_idt identifier=
"java::"+class_name;
720 symbol_type.
set(ID_C_base_name, class_name);
740 bool correct_num_components=type.
components().size()==3;
741 if(!correct_num_components)
748 bool base_component_valid=
true;
749 base_component_valid&=base_class_component.
get_name()==
"@java.lang.Object";
751 bool length_component_valid=
true;
754 length_component_valid&=length_component.
get_name()==
"length";
757 bool data_component_valid=
true;
760 data_component_valid&=data_component.
get_name()==
"data";
761 data_component_valid&=data_component.
type().
id()==ID_pointer;
763 return correct_num_components &&
764 base_component_valid &&
765 length_component_valid &&
766 data_component_valid;
777 bool arrays_with_same_element_type =
true;
779 type1.
id() == ID_pointer && type2.
id() == ID_pointer &&
785 subtype_symbol1.
get_identifier() == subtype_symbol2.get_identifier() &&
788 const typet &array_element_type1 =
790 const typet &array_element_type2 =
793 arrays_with_same_element_type =
797 return (type1 == type2 && arrays_with_same_element_type);
802 std::set<irep_idt> &refs)
812 else if(t.
id() == ID_pointer)
818 else if(t.
id() == ID_code)
827 else if(t.
id() == ID_symbol)
848 const std::string &signature,
849 std::set<irep_idt> &refs)
854 if(signature[0] ==
'<')
859 for(
const auto &t : types)
864 else if(signature.find(
'*') == std::string::npos)
885 std::set<irep_idt> &refs)
901 const std::string &base_ref,
902 const std::string &class_name_prefix)
905 set(ID_C_java_generic_symbol,
true);
911 "identifier of "+type.
pretty()+
"\n and identifier of type "+
912 gen_base_type.
subtype().
pretty()+
"\ncreated by java_type_from_string for "+
913 base_ref+
" should be equal");
927 const auto &type_variable = type.
get_name();
929 for(std::size_t i = 0; i < generics.size(); ++i)
964 const irep_idt &
id = symbol_type.get_identifier();
979 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)
std::vector< parametert > parameterst
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
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.
const typet & java_array_element_type(const symbol_typet &array_symbol)
Return a const reference to the element type of a given java array type.
const java_generic_parametert & to_java_generic_parameter(const typet &type)
const componentst & components() const
An exception that is raised for unsupported class signature.
bool is_multidim_java_array_type(const typet &type)
Checks whether the given type is a multi-dimensional array pointer type,.
#define CHECK_RETURN(CONDITION)
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
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()
bool can_cast_type< pointer_typet >(const typet &type)
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)
Constructs a type indicated by the given character:
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.
bool is_java_array_type(const typet &type)
Checks whether the given type is an array pointer type.
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)
std::string pretty_signature(const java_method_typet &method_type)
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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.
const java_method_typet & to_java_method_type(const typet &type)
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 & add_type(const irep_namet &name)
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
#define DATA_INVARIANT(CONDITION, REASON)
symbol_typet java_classname(const std::string &id)
const typet & return_type() const
bool can_cast_type< symbol_typet >(const typet &type)
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.