Skip to content

Parse java arrays in annotations properly #2619

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 1 commit into from
Aug 17, 2018
Merged

Parse java arrays in annotations properly #2619

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
33 changes: 15 additions & 18 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 @@ -126,7 +126,7 @@ class java_bytecode_parsert:public parsert
void rRuntimeAnnotation_attribute(annotationst &);
void rRuntimeAnnotation(annotationt &);
void relement_value_pairs(annotationt::element_value_pairst &);
void relement_value_pair(annotationt::element_value_pairt &);
exprt get_relement_value();
void rmethod_attribute(methodt &method);
void rfield_attribute(fieldt &);
void rcode_attribute(methodt &method);
Expand Down Expand Up @@ -1511,16 +1511,17 @@ void java_bytecode_parsert::relement_value_pairs(
{
u2 element_name_index=read_u2();
element_value_pair.element_name=pool_entry(element_name_index).s;

relement_value_pair(element_value_pair);
element_value_pair.value = get_relement_value();
}
}

/// Corresponds to the element_value structure
/// Described in Java 8 specification 4.7.16.1
/// https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html#jvms-4.7.16.1
Copy link
Contributor

Choose a reason for hiding this comment

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

You might choose to document here what is supports

/// Currently supports:
/// - classes
/// - arrays
/// - all constants (byte, char, double, float, int, long, short and boolean)
/// (enum type and annotation types not yet supported).

void java_bytecode_parsert::relement_value_pair(
annotationt::element_value_pairt &element_value_pair)
/// \returns An exprt that represents the particular value of annotations field.
/// This is usually one of: a byte, number of some sort, string, character,
/// enum, Class type, array or another annotation.
exprt java_bytecode_parsert::get_relement_value()
{
u1 tag=read_u1();

Expand All @@ -1531,50 +1532,46 @@ void java_bytecode_parsert::relement_value_pair(
UNUSED_u2(type_name_index);
UNUSED_u2(const_name_index);
// todo: enum
return exprt();
Copy link
Contributor

Choose a reason for hiding this comment

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

Would it make sense to return an optionalt<exprt> to make it clear it is not useful (and in callsite, only store if it has a value)

Copy link
Contributor

Choose a reason for hiding this comment

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

Probably not, as this should be implemented properly instead in a subsequent PR.

}
break;

case 'c':
{
u2 class_info_index = read_u2();
element_value_pair.value = symbol_exprt(pool_entry(class_info_index).s);
return symbol_exprt(pool_entry(class_info_index).s);
}
break;

case '@':
{
// TODO: return this wrapped in an exprt
// another annotation, recursively
annotationt annotation;
rRuntimeAnnotation(annotation);
return exprt();
}
break;

case '[':
{
array_exprt values;
u2 num_values=read_u2();
for(std::size_t i=0; i<num_values; i++)
{
annotationt::element_value_pairt element_value;
relement_value_pair(element_value); // recursive call
values.operands().push_back(get_relement_value());
}
return values;
}
break;

case 's':
{
u2 const_value_index=read_u2();
element_value_pair.value=string_constantt(
pool_entry(const_value_index).s);
return string_constantt(pool_entry(const_value_index).s);
}
break;

default:
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 be tempted to stick an invariant that the char is one of B, C, D, F, I, J, S, Z to catch out any future changes in the spec.

{
u2 const_value_index=read_u2();
element_value_pair.value=constant(const_value_index);
return constant(const_value_index);
}

break;
}
}

Expand Down
Binary file added jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithStringArray.class
View file
Open in desktop
Binary file not shown.
3 changes: 3 additions & 0 deletions jbmc/unit/java_bytecode/java_bytecode_parser/AnnotationWithStringArray.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
public @interface AnnotationWithStringArray {
String[] value() default {};
}
Binary file added jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithArrayAnnotation.class
View file
Open in desktop
Binary file not shown.
3 changes: 3 additions & 0 deletions jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithArrayAnnotation.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
@AnnotationWithStringArray({"Dave", "Another Dave"})
public class ClassWithArrayAnnotation {
}
25 changes: 25 additions & 0 deletions jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,5 +91,30 @@ SCENARIO(
REQUIRE(java_type == void_type());
}
}
WHEN("Parsing an annotation with an array field.")
{
const symbol_tablet &new_symbol_table = load_java_class(
"ClassWithArrayAnnotation", "./java_bytecode/java_bytecode_parser");

THEN("The annotation should store an array of type string.")
{
const symbolt &class_symbol =
Copy link
Contributor

Choose a reason for hiding this comment

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

Nit: lookup_ref when immediately dereferencing

*new_symbol_table.lookup("java::ClassWithArrayAnnotation");
const std::vector<java_annotationt> &java_annotations =
to_annotated_type(class_symbol.type).get_annotations();
Copy link
Contributor

Choose a reason for hiding this comment

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

Nit: in require_types you can add a method called require_annotated_type that would look like:

annotated_typet require_annotated_type(const typet &type)
{
  REQUIRE(can_cast_type<annotted_typet>(type);
  return to_annotated_typet(type);
}

As the above line, if the type isn't annotated_typet will abort the unit test making it harder to see what went wrong.

java_bytecode_parse_treet::annotationst annotations;
convert_java_annotations(java_annotations, annotations);
REQUIRE(annotations.size() == 1);
const auto &annotation = annotations.front();
const auto &element_value_pair = annotation.element_value_pairs.front();
const auto &array = to_array_expr(element_value_pair.value);
Copy link
Contributor

Choose a reason for hiding this comment

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

Ditto here, it would be nice to add and use require_array which would go in require_expr.h for same reason.


REQUIRE(array.operands().size() == 2);
const auto &dave = array.op0().get(ID_value);
Copy link
Contributor

Choose a reason for hiding this comment

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

Nit: avoid direct access, though I don't know what you can convert to, is it a constant_exprt?

const auto &another_dave = array.op1().get(ID_value);
REQUIRE(id2string(dave) == "Dave");
REQUIRE(id2string(another_dave) == "Another Dave");
}
}
}
}