Skip to content

Replace use of deprecated nil_typet in java_type_from_string [blocks: #3800] #3929

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 3 commits into from
Feb 1, 2019
Merged

Replace use of deprecated nil_typet in java_type_from_string [blocks: #3800] #3929

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
08276eb
Replace use of deprecated nil_typet in java_type_from_string
tautschnig Jan 25, 2019
6f1084e
Address errors in handcrafted bytecode
Jan 31, 2019
8f71a23
Do not allow getting type from descriptor to fail
Jan 31, 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
Binary file modified jbmc/regression/jbmc/stack_var12/stack_typecast.class
View file
Open in desktop
Binary file not shown.
4 changes: 2 additions & 2 deletions jbmc/regression/jbmc/stack_var12/stack_typecast.j
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,14 @@

.method public <init>()V
aload_0
invokevirtual java/lang/Object/<init>()V
invokespecial java/lang/Object/<init>()V
return
.end method

.method public f()I
.limit stack 6
.limit locals 1
.var 0 is this stack_typecast from begin to end
.var 0 is this Lstack_typecast; from begin to end
.line 0
begin:

Expand Down
8 changes: 3 additions & 5 deletions jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -637,10 +637,8 @@ void java_bytecode_convert_classt::convert(
typet field_type;
if(f.signature.has_value())
{
field_type=java_type_from_string_with_exception(
f.descriptor,
f.signature,
id2string(class_symbol.name));
field_type = *java_type_from_string_with_exception(
Copy link
Member

Choose a reason for hiding this comment

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

Are we sure this has a value? (and other places)

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

As above: no idea, but it was previously used unchecked. There are a couple of places that failed this while running the regression tests, and those I have now guarded appropriately. I still think that this makes optionalt<typet> much better as at least you'd have a failing assertion instead of silently passing around a nil_typet that some later stage won't know how to deal with.

f.descriptor, f.signature, id2string(class_symbol.name));

/// this is for a free type variable, e.g., a field of the form `T f;`
if(is_java_generic_parameter(field_type))
Expand Down Expand Up @@ -670,7 +668,7 @@ void java_bytecode_convert_classt::convert(
}
}
else
field_type=java_type_from_string(f.descriptor);
field_type = *java_type_from_string(f.descriptor);

// is this a static field?
if(f.is_static)
Expand Down
41 changes: 16 additions & 25 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -259,21 +259,26 @@ java_method_typet member_type_lazy(

messaget message(message_handler);

typet member_type_from_descriptor=java_type_from_string(descriptor);
INVARIANT(member_type_from_descriptor.id()==ID_code, "Must be code type");
auto member_type_from_descriptor = java_type_from_string(descriptor);
INVARIANT(
member_type_from_descriptor.has_value() &&
member_type_from_descriptor->id() == ID_code,
"Must be code type");
if(signature.has_value())
{
try
{
typet member_type_from_signature=java_type_from_string(
signature.value(),
class_name);
INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type");
auto member_type_from_signature =
java_type_from_string(signature.value(), class_name);
INVARIANT(
Copy link
Contributor

Choose a reason for hiding this comment

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

I'd actually delete this, we're about to check both those things by deref'ing and casting

member_type_from_signature.has_value() &&
member_type_from_signature->id() == ID_code,
"Must be code type");
if(
to_java_method_type(member_type_from_signature).parameters().size() ==
to_java_method_type(member_type_from_descriptor).parameters().size())
to_java_method_type(*member_type_from_signature).parameters().size() ==
to_java_method_type(*member_type_from_descriptor).parameters().size())
{
return to_java_method_type(member_type_from_signature);
return to_java_method_type(*member_type_from_signature);
}
else
{
Expand All @@ -294,7 +299,7 @@ java_method_typet member_type_lazy(
<< message.eom;
}
}
return to_java_method_type(member_type_from_descriptor);
return to_java_method_type(*member_type_from_descriptor);
}

/// Retrieves the symbol of the lambda method associated with the given
Expand Down Expand Up @@ -460,24 +465,10 @@ void java_bytecode_convert_methodt::convert(
if(!is_parameter(v))
continue;

// Construct a fully qualified name for the parameter v,
// e.g. my.package.ClassName.myMethodName:(II)I::anIntParam, and then a
// symbol_exprt with the parameter and its type
typet t;
if(v.signature.has_value())
{
t=java_type_from_string_with_exception(
v.descriptor,
v.signature,
id2string(class_symbol.name));
}
else
t=java_type_from_string(v.descriptor);

std::ostringstream id_oss;
id_oss << method_id << "::" << v.name;
irep_idt identifier(id_oss.str());
symbol_exprt result(identifier, t);
symbol_exprt result = symbol_exprt::typeless(identifier);
Copy link
Contributor

Choose a reason for hiding this comment

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

❓ This change looks a little suspicious? Previously the type of the symbol was derived from the signature or descriptor, now is a typeless identifier?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

The type was sometimes nil_typet() (because trying to derive the type failed) and nobody noticed, because really the type of this is never used.

Copy link
Contributor

Choose a reason for hiding this comment

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

In that case could I suggest using an irep_idt instead of a symbol_exprt? Otherwise someone will surely assume that variables[n].type() is a sensible thing to look at.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

That would necessitate some refactoring of this code as the expression is also used to communicate ID_C_base_name.

result.set(ID_C_base_name, v.name);

// Create a new variablet in the variables vector; in fact this entry will
Expand Down
47 changes: 24 additions & 23 deletions jbmc/src/java_bytecode/java_bytecode_parser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ class java_bytecode_parsert:public parsert

const typet type_entry(u2 index)
{
return java_type_from_string(id2string(pool_entry(index).s));
return *java_type_from_string(id2string(pool_entry(index).s));
}

void populate_bytecode_mnemonics_table()
Expand Down Expand Up @@ -547,10 +547,8 @@ void java_bytecode_parsert::get_class_refs()
break;

case CONSTANT_NameAndType:
{
typet t=java_type_from_string(id2string(pool_entry(c.ref2).s));
get_class_refs_rec(t);
}
get_class_refs_rec(
*java_type_from_string(id2string(pool_entry(c.ref2).s)));
break;

default: {}
Expand All @@ -562,59 +560,63 @@ void java_bytecode_parsert::get_class_refs()
for(const auto &field : parse_tree.parsed_class.fields)
{
get_annotation_class_refs(field.annotations);
typet field_type;

if(field.signature.has_value())
{
field_type=java_type_from_string_with_exception(
typet field_type = *java_type_from_string_with_exception(
field.descriptor,
field.signature,
"java::"+id2string(parse_tree.parsed_class.name));
"java::" + id2string(parse_tree.parsed_class.name));

// add generic type args to class refs as dependencies, same below for
// method types and entries from the local variable type table
get_dependencies_from_generic_parameters(
field_type, parse_tree.class_refs);
get_class_refs_rec(field_type);
}
else
field_type=java_type_from_string(field.descriptor);

get_class_refs_rec(field_type);
{
get_class_refs_rec(*java_type_from_string(field.descriptor));
}
}

for(const auto &method : parse_tree.parsed_class.methods)
{
get_annotation_class_refs(method.annotations);
for(const auto &parameter_annotations : method.parameter_annotations)
get_annotation_class_refs(parameter_annotations);
typet method_type;

if(method.signature.has_value())
{
method_type=java_type_from_string_with_exception(
typet method_type = *java_type_from_string_with_exception(
method.descriptor,
method.signature,
"java::"+id2string(parse_tree.parsed_class.name));
"java::" + id2string(parse_tree.parsed_class.name));
get_dependencies_from_generic_parameters(
method_type, parse_tree.class_refs);
get_class_refs_rec(method_type);
}
else
method_type=java_type_from_string(method.descriptor);
{
get_class_refs_rec(*java_type_from_string(method.descriptor));
}

get_class_refs_rec(method_type);
for(const auto &var : method.local_variable_table)
{
typet var_type;
if(var.signature.has_value())
{
var_type=java_type_from_string_with_exception(
typet var_type = *java_type_from_string_with_exception(
var.descriptor,
var.signature,
"java::"+id2string(parse_tree.parsed_class.name));
"java::" + id2string(parse_tree.parsed_class.name));
get_dependencies_from_generic_parameters(
var_type, parse_tree.class_refs);
get_class_refs_rec(var_type);
}
else
var_type=java_type_from_string(var.descriptor);
get_class_refs_rec(var_type);
{
get_class_refs_rec(*java_type_from_string(var.descriptor));
}
}
}
}
Expand Down Expand Up @@ -672,8 +674,7 @@ void java_bytecode_parsert::get_annotation_value_class_refs(const exprt &value)
if(const auto &symbol_expr = expr_try_dynamic_cast<symbol_exprt>(value))
{
const irep_idt &value_id = symbol_expr->get_identifier();
const typet value_type = java_type_from_string(id2string(value_id));
get_class_refs_rec(value_type);
get_class_refs_rec(*java_type_from_string(id2string(value_id)));
}
else if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(value))
{
Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/java_entry_point.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -267,14 +267,14 @@ bool is_java_main(const symbolt &function)
{
bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD);
const java_method_typet &function_type = to_java_method_type(function.type);
const typet &string_array_type = java_type_from_string("[Ljava/lang/String;");
const auto string_array_type = java_type_from_string("[Ljava/lang/String;");
// checks whether the function is static and has a single String[] parameter
bool is_static = !function_type.has_this();
// this should be implied by the signature
const java_method_typet::parameterst &parameters = function_type.parameters();
bool has_correct_type = function_type.return_type().id() == ID_empty &&
parameters.size() == 1 &&
parameters[0].type().full_eq(string_array_type);
parameters[0].type().full_eq(*string_array_type);
bool public_access = function_type.get(ID_access) == ID_public;
return named_main && is_static && has_correct_type && public_access;
}
Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/java_local_variable_table.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -794,9 +794,9 @@ void java_bytecode_convert_methodt::setup_local_variables(
const std::string class_name = method_name.substr(0, class_name_end);

const typet t = v.var.signature.has_value()
? java_type_from_string_with_exception(
? *java_type_from_string_with_exception(
v.var.descriptor, v.var.signature, class_name)
: java_type_from_string(v.var.descriptor);
: *java_type_from_string(v.var.descriptor);

std::ostringstream id_oss;
id_oss << method_id << "::" << v.var.start_pc << "::" << v.var.name;
Expand Down
Loading