From 0bf28f0673a6eb79ee3f7dea8325b49c1644440d Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sat, 6 Apr 2019 20:29:07 +0100
Subject: [PATCH 1/2] introduce java_class_typet::componentt
This enables Java-specific extensions to components of Java classes (e.g.,
'native', 'final').
---
.../java_bytecode_convert_class.cpp | 8 ++--
jbmc/src/java_bytecode/java_types.h | 37 ++++++++++++++++++-
2 files changed, 40 insertions(+), 5 deletions(-)
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index 5580caa8862..1b5bc8a7862 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -375,7 +375,7 @@ void java_bytecode_convert_classt::convert(
{
class_type.add_base(base);
}
- class_typet::componentt base_class_field;
+ java_class_typet::componentt base_class_field;
base_class_field.type() = class_type.bases().at(0).type();
base_class_field.set_name("@" + id2string(c.super_class));
base_class_field.set_base_name("@" + id2string(c.super_class));
@@ -798,18 +798,18 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
class_type.set_name(struct_tag_type_identifier);
class_type.components().reserve(3);
- class_typet::componentt base_class_component(
+ java_class_typet::componentt base_class_component(
"@java.lang.Object", struct_tag_typet("java::java.lang.Object"));
base_class_component.set_pretty_name("@java.lang.Object");
base_class_component.set_base_name("@java.lang.Object");
class_type.components().push_back(base_class_component);
- class_typet::componentt length_component("length", java_int_type());
+ java_class_typet::componentt length_component("length", java_int_type());
length_component.set_pretty_name("length");
length_component.set_base_name("length");
class_type.components().push_back(length_component);
- class_typet::componentt data_component(
+ java_class_typet::componentt data_component(
"data", java_reference_type(java_type_from_char(l)));
data_component.set_pretty_name("data");
data_component.set_base_name("data");
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index 7b39f917c3b..b55dae20712 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -101,7 +101,42 @@ inline bool can_cast_type<annotated_typet>(const typet &)
class java_class_typet:public class_typet
{
- public:
+public:
+ class componentt : public class_typet::componentt
+ {
+ public:
+ componentt() = default;
+
+ componentt(const irep_idt &_name, typet _type)
+ : class_typet::componentt(_name, std::move(_type))
+ {
+ }
+
+ /// is a method 'native'?
+ bool get_is_native() const
+ {
+ return get_bool(ID_is_native_method);
+ }
+
+ /// marks a method as 'native'
+ void set_is_native(const bool is_native)
+ {
+ set(ID_is_native_method, is_native);
+ }
+ };
+
+ 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 irep_idt &get_access() const
{
return get(ID_access);
From 809c5a3a227a4315ba222e66e680bd1b7f8abb93 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sat, 6 Apr 2019 21:06:57 +0100
Subject: [PATCH 2/2] move is_final to java component type
'final' is a field modifier for Java, and has no meaning in C or C++. It
should thus move to java_class_typet::componentt.
---
.../java_bytecode_convert_class.cpp | 4 ++--
.../java_bytecode/java_bytecode_language.cpp | 2 +-
jbmc/src/java_bytecode/java_types.h | 18 ++++++++++++++++
jbmc/unit/java-testing-utils/require_type.cpp | 21 ++++++++++++++++++-
jbmc/unit/java-testing-utils/require_type.h | 4 ++++
.../java_bytecode_language/language.cpp | 6 +++---
src/util/std_types.h | 10 ---------
7 files changed, 48 insertions(+), 17 deletions(-)
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index 1b5bc8a7862..b87fc9c2280 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -740,10 +740,10 @@ void java_bytecode_convert_classt::convert(
}
else
{
- class_typet &class_type=to_class_type(class_symbol.type);
+ auto &class_type = to_java_class_type(class_symbol.type);
class_type.components().emplace_back();
- class_typet::componentt &component=class_type.components().back();
+ auto &component = class_type.components().back();
component.set_name(f.name);
component.set_base_name(f.name);
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index da84fe35975..31f286026f6 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -332,7 +332,7 @@ static void infer_opaque_type_fields(
symbolt &writable_class_symbol =
symbol_table.get_writeable_ref(class_symbol_id);
auto &components =
- to_struct_type(writable_class_symbol.type).components();
+ to_java_class_type(writable_class_symbol.type).components();
components.emplace_back(component_name, fieldref.type());
components.back().set_base_name(component_name);
components.back().set_pretty_name(component_name);
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index b55dae20712..b738f9fdd16 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -112,6 +112,18 @@ class java_class_typet:public class_typet
{
}
+ /// is a method or field 'final'?
+ bool get_is_final() const
+ {
+ return get_bool(ID_final);
+ }
+
+ /// is a method or field 'final'?
+ void set_is_final(const bool is_final)
+ {
+ set(ID_final, is_final);
+ }
+
/// is a method 'native'?
bool get_is_native() const
{
@@ -137,6 +149,12 @@ class java_class_typet:public class_typet
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));
+ }
+
const irep_idt &get_access() const
{
return get(ID_access);
diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp
index 893cfb8dc7b..9c8e682fa8b 100644
--- a/jbmc/unit/java-testing-utils/require_type.cpp
+++ b/jbmc/unit/java-testing-utils/require_type.cpp
@@ -30,11 +30,30 @@ pointer_typet require_type::require_pointer(
return pointer;
}
+/// Checks that a class has a component with a specific name
+/// \param java_class_type: The class that should have the component
+/// \param component_name: The name of the component
+/// \return The component with the specified name
+java_class_typet::componentt require_type::require_component(
+ const java_class_typet &java_class_type,
+ const irep_idt &component_name)
+{
+ const auto &component = std::find_if(
+ java_class_type.components().begin(),
+ java_class_type.components().end(),
+ [&component_name](const java_class_typet::componentt &component) {
+ return component.get_name() == component_name;
+ });
+
+ REQUIRE(component != java_class_type.components().end());
+ return *component;
+}
+
/// Checks a struct like type has a component with a specific name
/// \param struct_type: The structure that should have the component
/// \param component_name: The name of the component
/// \return The component with the specified name
-struct_union_typet::componentt require_type::require_component(
+struct_typet::componentt require_type::require_component(
const struct_typet &struct_type,
const irep_idt &component_name)
{
diff --git a/jbmc/unit/java-testing-utils/require_type.h b/jbmc/unit/java-testing-utils/require_type.h
index 14ae5c47f7b..d0d8912453f 100644
--- a/jbmc/unit/java-testing-utils/require_type.h
+++ b/jbmc/unit/java-testing-utils/require_type.h
@@ -32,6 +32,10 @@ const pointer_typet require_pointer_to_tag(
const typet &type,
const irep_idt &identifier = irep_idt());
+java_class_typet::componentt require_component(
+ const java_class_typet &java_class_type,
+ const irep_idt &component_name);
+
struct_typet::componentt require_component(
const struct_typet &struct_type,
const irep_idt &component_name);
diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp
index 1b9f7d8c9b6..ada4c440109 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_language/language.cpp
@@ -36,9 +36,9 @@ SCENARIO(
{
const symbolt &opaque_class_symbol =
symbol_table.lookup_ref(opaque_class_prefix);
- const struct_typet &opaque_class_struct =
- to_struct_type(opaque_class_symbol.type);
- const struct_union_typet::componentt &field =
+ const auto &opaque_class_struct =
+ to_java_class_type(opaque_class_symbol.type);
+ const auto &field =
require_type::require_component(opaque_class_struct, "field2");
REQUIRE(field.get_is_final());
}
diff --git a/src/util/std_types.h b/src/util/std_types.h
index 85390988cc3..93210340ed5 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -123,16 +123,6 @@ class struct_union_typet:public typet
{
return set(ID_C_is_padding, is_padding);
}
-
- bool get_is_final() const
- {
- return get_bool(ID_final);
- }
-
- void set_is_final(const bool is_final)
- {
- set(ID_final, is_final);
- }
};
typedef std::vector<componentt> componentst;