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 struct_tag_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);
223 if(new_type==expr.
type())
239 const std::string &type_arguments,
240 const std::string &class_name_prefix)
244 PRECONDITION(type_arguments[type_arguments.size() - 1] ==
'>');
249 std::vector<typet> type_arguments_types =
257 type_arguments_types.begin(),
258 type_arguments_types.end(),
263 is_reference(type),
"All generic type arguments should be references");
274 std::string class_name = src;
275 std::size_t f_pos = class_name.find(
'<', 1);
277 while(f_pos != std::string::npos)
280 if(e_pos == std::string::npos)
283 "Failed to find generic signature closing delimiter (or recursive " 289 class_name.erase(f_pos, e_pos - f_pos + 1);
292 f_pos = class_name.find(
'<', f_pos + 1);
309 std::string class_name = src.substr(1, src.size() - 2);
313 std::replace(class_name.begin(), class_name.end(),
'.',
'$');
314 std::replace(class_name.begin(), class_name.end(),
'/',
'.');
331 const std::string src,
332 const std::string class_name_prefix,
333 const char opening_bracket,
334 const char closing_bracket)
338 std::vector<typet> type_list;
339 for(
const std::string &raw_type :
344 type_list.push_back(new_type);
358 const std::string src,
359 const char opening_bracket,
360 const char closing_bracket)
368 std::vector<std::string> type_list;
369 for(std::size_t i = 1; i < src.size() - 1; i++)
372 while(i < src.size())
382 else if(src[i] ==
'[')
386 else if(src[i] ==
'T')
387 i = src.find(
';', i);
396 std::string sub_str = src.substr(start, i - start + 1);
397 type_list.emplace_back(sub_str);
418 std::string identifier =
"java::" + container_class;
420 struct_tag_type.
set(ID_C_base_name, container_class);
422 std::size_t f_pos = src.find(
'<', 1);
423 if(f_pos != std::string::npos)
430 if(e_pos == std::string::npos)
432 "Parsing type with unmatched generic bracket: " + src);
435 result, src.substr(f_pos, e_pos - f_pos + 1), class_name_prefix);
438 f_pos = src.find(
'<', e_pos + 1);
439 }
while(f_pos != std::string::npos);
440 return std::move(result);
455 const std::string src,
456 size_t starting_point)
459 size_t next_semi_colon = src.find(
';', starting_point);
461 next_semi_colon != std::string::npos,
462 "There must be a semi-colon somewhere in the input");
463 size_t next_angle_bracket = src.find(
'<', starting_point);
465 while(next_angle_bracket < next_semi_colon)
470 end_bracket != std::string::npos,
"Must find matching angle bracket");
472 next_semi_colon = src.find(
';', end_bracket + 1);
473 next_angle_bracket = src.find(
'<', end_bracket + 1);
476 return next_semi_colon;
493 const std::string &src,
494 const std::string &class_name_prefix)
524 if(closing_generic==std::string::npos)
527 "Failed to find generic signature closing delimiter");
534 const size_t colon_pos = src.find(
':');
535 if(colon_pos != std::string::npos && colon_pos < closing_generic)
538 "Cannot currently parse bounds on generic types");
542 src.substr(closing_generic+1, std::string::npos), class_name_prefix);
549 method_type.
id()==ID_code,
550 "This should correspond to method signatures only");
556 std::size_t e_pos=src.rfind(
')');
557 if(e_pos==std::string::npos)
561 std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
563 std::vector<typet> param_types =
571 std::back_inserter(parameters),
583 char subtype_letter=src[1];
587 if(subtype_letter==
'L' ||
588 subtype_letter==
'[' ||
608 INVARIANT(src[src.size()-1]==
';',
"Generic type name must end on ';'.");
610 irep_idt type_var_name(class_name_prefix+
"::"+src.substr(1, src.size()-2));
625 std::cout << class_name_prefix << std::endl;
650 else if(
id==ID_unsignedbv)
652 else if(
id==ID_floatbv)
660 else if(
id==ID_c_bool)
676 const std::string &class_name,
677 const std::string &src)
683 src[0]==
'<' && signature_end!=std::string::npos,
684 "Class signature has unexpected format");
685 std::string signature(src.substr(1, signature_end-1));
687 if(signature.find(
";:")!=std::string::npos)
692 std::vector<typet> types;
693 size_t var_sep=signature.find(
';');
694 while(var_sep!=std::string::npos)
696 size_t bound_sep=signature.find(
':');
697 INVARIANT(bound_sep!=std::string::npos,
"No bound for type variable.");
701 if(signature[bound_sep + 1] ==
':')
704 signature[bound_sep + 2] !=
':',
"Unknown bound for type variable.");
708 std::string type_var_name(
709 "java::"+class_name+
"::"+signature.substr(0, bound_sep));
710 std::string bound_type(signature.substr(bound_sep+1, var_sep-bound_sep));
717 types.push_back(type_var_type);
718 signature=signature.substr(var_sep+1, std::string::npos);
719 var_sep=signature.find(
';');
727 std::string result=src;
728 for(std::string::iterator it=result.begin(); it!=result.end(); it++)
736 if(!
id.empty() &&
id[0]==
'[')
739 std::string class_name=id;
742 irep_idt identifier=
"java::"+class_name;
744 struct_tag_type.
set(ID_C_base_name, class_name);
746 return struct_tag_type;
764 bool correct_num_components=type.
components().size()==3;
765 if(!correct_num_components)
772 bool base_component_valid=
true;
773 base_component_valid&=base_class_component.
get_name()==
"@java.lang.Object";
775 bool length_component_valid=
true;
778 length_component_valid&=length_component.
get_name()==
"length";
781 bool data_component_valid=
true;
784 data_component_valid&=data_component.
get_name()==
"data";
785 data_component_valid&=data_component.
type().
id()==ID_pointer;
787 return correct_num_components &&
788 base_component_valid &&
789 length_component_valid &&
790 data_component_valid;
801 bool arrays_with_same_element_type =
true;
803 type1.
id() == ID_pointer && type2.
id() == ID_pointer &&
810 subtype_symbol1.get_identifier() == subtype_symbol2.get_identifier() &&
813 const typet &array_element_type1 =
815 const typet &array_element_type2 =
818 arrays_with_same_element_type =
822 return (type1 == type2 && arrays_with_same_element_type);
827 std::set<irep_idt> &refs)
837 else if(t.
id() == ID_pointer)
843 else if(t.
id() == ID_code)
852 else if(t.
id() == ID_struct_tag)
855 const irep_idt class_name(struct_tag_type.get_identifier());
873 const std::string &signature,
874 std::set<irep_idt> &refs)
879 if(signature[0] ==
'<')
884 for(
const auto &t : types)
889 else if(signature.find(
'*') == std::string::npos)
910 std::set<irep_idt> &refs)
926 const std::string &base_ref,
927 const std::string &class_name_prefix)
930 set(ID_C_java_generic_symbol,
true);
937 "identifier of " + type.
pretty() +
"\n and identifier of type " +
939 "\ncreated by java_type_from_string for " + base_ref +
954 const auto &type_variable = type.
get_name();
956 for(std::size_t i = 0; i < generics.size(); ++i)
993 const irep_idt &
id = struct_tag_type.get_identifier();
1009 std::ostringstream result;
1027 return result.str();
The void type, the same as empty_typet.
const irep_idt & get_name() const
The type of an expression, extends irept.
Fixed-width bit-vector with unsigned binary interpretation.
Semantic type conversion.
const irep_idt & get_identifier() const
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 typet to a signedbv_typet.
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 typet to a reference_typet.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
struct_tag_typet java_classname(const std::string &id)
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 typet & java_array_element_type(const struct_tag_typet &array_symbol)
Return a const reference to the element type of a given java array type.
std::vector< std::string > parse_raw_list_types(const std::string src, 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_parametert & to_java_generic_parameter(const typet &type)
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
const componentst & components() const
A struct tag type, i.e., struct_typet with an identifier.
const generic_typest & generic_types() const
typet & type()
Return the type of the expression.
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)
Structure type, corresponds to C style structs.
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
bool is_java_array_tag(const irep_idt &tag)
See above.
optionalt< size_t > generic_type_index(const java_generic_parametert &type) const
Check if this symbol has the given generic type.
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)
This macro uses the wrapper function 'invariant_violated_string'.
static ieee_float_spect double_precision()
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
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...
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)
Returns true if the type is a reference.
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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
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 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
#define UNREACHABLE
This should be used to mark dead code.
void base_type(typet &type, const namespacet &ns)
typet & add_type(const irep_namet &name)
The NIL type, i.e., an invalid type, no value.
bool can_cast_type< struct_tag_typet >(const typet &type)
Check whether a reference to a typet is a struct_tag_typet.
java_generic_struct_tag_typet(const struct_tag_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...
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 ...
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
const typet & return_type() 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.