Skip to content

Java class typet methodt #4618

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
May 7, 2019
Merged

Java class typet methodt #4618

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6863048
move java_method_typet
May 4, 2019
5cb4d38
introduce java_class_typet::methodt
May 4, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
264 changes: 155 additions & 109 deletions jbmc/src/java_bytecode/java_types.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,102 @@ inline bool can_cast_type<annotated_typet>(const typet &)
return true;
}

class java_method_typet : public code_typet
{
public:
using code_typet::parameterst;
using code_typet::parametert;

/// Constructs a new code type, i.e. method type
/// \param _parameters: the vector of method parameters
/// \param _return_type: the return type
java_method_typet(parameterst &&_parameters, typet &&_return_type)
: code_typet(std::move(_parameters), std::move(_return_type))
{
set(ID_C_java_method_type, true);
}

/// Constructs a new code type, i.e. method type
/// \param _parameters: the vector of method parameters
/// \param _return_type: the return type
java_method_typet(parameterst &&_parameters, const typet &_return_type)
: code_typet(std::move(_parameters), _return_type)
{
set(ID_C_java_method_type, true);
}

const std::vector<irep_idt> throws_exceptions() const
{
std::vector<irep_idt> exceptions;
for(const auto &e : find(ID_exceptions_thrown_list).get_sub())
exceptions.push_back(e.id());
return exceptions;
}

void add_throws_exceptions(irep_idt exception)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

exception, singular

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed, but note that this is just moving existing code around. Will do a separate PR.

{
add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
}

bool get_is_final() const
{
return get_bool(ID_final);
}

void set_is_final(bool is_final)
{
set(ID_final, is_final);
}

bool get_native() const
{
return get_bool(ID_is_native_method);
}

void set_native(bool is_native)
{
set(ID_is_native_method, is_native);
}

bool get_is_varargs() const
{
return get_bool(ID_is_varargs_method);
}

void set_is_varargs(bool is_varargs)
{
set(ID_is_varargs_method, is_varargs);
}

bool is_synthetic() const
{
return get_bool(ID_synthetic);
}

void set_is_synthetic(bool is_synthetic)
{
set(ID_synthetic, is_synthetic);
}
};

template <>
inline bool can_cast_type<java_method_typet>(const typet &type)
{
return type.id() == ID_code && type.get_bool(ID_C_java_method_type);
}

inline const java_method_typet &to_java_method_type(const typet &type)
{
PRECONDITION(can_cast_type<java_method_typet>(type));
return static_cast<const java_method_typet &>(type);
}

inline java_method_typet &to_java_method_type(typet &type)
{
PRECONDITION(can_cast_type<java_method_typet>(type));
return static_cast<java_method_typet &>(type);
}

class java_class_typet:public class_typet
{
public:
Expand All @@ -112,13 +208,65 @@ class java_class_typet:public class_typet
{
}

/// is a method or field 'final'?
/// is a field 'final'?
bool get_is_final() const
{
return get_bool(ID_final);
}

/// is a field 'final'?
void set_is_final(const bool is_final)
{
set(ID_final, is_final);
}
};

using componentst = std::vector<componentt>;

const componentst &components() const
{
return (const componentst &)(find(ID_components).get_sub());
}

componentst &components()
{
return (componentst &)(add(ID_components).get_sub());
}

const componentt &get_component(const irep_idt &component_name) const
{
return static_cast<const componentt &>(
class_typet::get_component(component_name));
}

class methodt : public class_typet::methodt
{
public:
methodt() = delete;

methodt(const irep_idt &_name, java_method_typet _type)
: class_typet::methodt(_name, std::move(_type))
{
}

const java_method_typet &type() const
{
return static_cast<const java_method_typet &>(
class_typet::methodt::type());
}

java_method_typet &type()
{
return static_cast<java_method_typet &>(class_typet::methodt::type());
}

/// is a method 'final'?
bool get_is_final() const
{
return get_bool(ID_final);
}

/// is a method or field 'final'?
/// is a method 'final'?
void set_is_final(const bool is_final)
{
set(ID_final, is_final);
Expand All @@ -137,22 +285,16 @@ class java_class_typet:public class_typet
}
};

using componentst = std::vector<componentt>;
using methodst = std::vector<methodt>;

const componentst &components() const
const methodst &methods() const
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are there any users for this? It'd be good to include at least some in this PR so doesn't get deleted Perhaps a unit test for checking that a java class when loaded has the methods set?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Coming!

{
return (const componentst &)(find(ID_components).get_sub());
return (const methodst &)(find(ID_methods).get_sub());
}

componentst &components()
methodst &methods()
{
return (componentst &)(add(ID_components).get_sub());
}

const componentt &get_component(const irep_idt &component_name) const
{
return static_cast<const componentt &>(
class_typet::get_component(component_name));
return (methodst &)(add(ID_methods).get_sub());
}

using static_membert = componentt;
Expand Down Expand Up @@ -352,102 +494,6 @@ inline bool can_cast_type<java_class_typet>(const typet &type)
return can_cast_type<class_typet>(type);
}

class java_method_typet : public code_typet
{
public:
using code_typet::parameterst;
using code_typet::parametert;

/// Constructs a new code type, i.e. method type
/// \param _parameters: the vector of method parameters
/// \param _return_type: the return type
java_method_typet(parameterst &&_parameters, typet &&_return_type)
: code_typet(std::move(_parameters), std::move(_return_type))
{
set(ID_C_java_method_type, true);
}

/// Constructs a new code type, i.e. method type
/// \param _parameters: the vector of method parameters
/// \param _return_type: the return type
java_method_typet(parameterst &&_parameters, const typet &_return_type)
: code_typet(std::move(_parameters), _return_type)
{
set(ID_C_java_method_type, true);
}

const std::vector<irep_idt> throws_exceptions() const
{
std::vector<irep_idt> exceptions;
for(const auto &e : find(ID_exceptions_thrown_list).get_sub())
exceptions.push_back(e.id());
return exceptions;
}

void add_throws_exceptions(irep_idt exception)
{
add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
}

bool get_is_final() const
{
return get_bool(ID_final);
}

void set_is_final(bool is_final)
{
set(ID_final, is_final);
}

bool get_native() const
{
return get_bool(ID_is_native_method);
}

void set_native(bool is_native)
{
set(ID_is_native_method, is_native);
}

bool get_is_varargs() const
{
return get_bool(ID_is_varargs_method);
}

void set_is_varargs(bool is_varargs)
{
set(ID_is_varargs_method, is_varargs);
}

bool is_synthetic() const
{
return get_bool(ID_synthetic);
}

void set_is_synthetic(bool is_synthetic)
{
set(ID_synthetic, is_synthetic);
}
};

template <>
inline bool can_cast_type<java_method_typet>(const typet &type)
{
return type.id() == ID_code && type.get_bool(ID_C_java_method_type);
}

inline const java_method_typet &to_java_method_type(const typet &type)
{
PRECONDITION(can_cast_type<java_method_typet>(type));
return static_cast<const java_method_typet &>(type);
}

inline java_method_typet &to_java_method_type(typet &type)
{
PRECONDITION(can_cast_type<java_method_typet>(type));
return static_cast<java_method_typet &>(type);
}

/// This is a specialization of reference_typet.
/// The subtype is guaranteed to be a struct_tag_typet.
class java_reference_typet : public reference_typet
Expand Down