Skip to content

Commit 37106b6

Browse files
author
thk123
committed
Added check for a type being a valid formed Java array
Essentially serves to programatically document what is expected of a Java array type when represented in GOTO.
1 parent 5c9eb59 commit 37106b6

File tree

2 files changed

+49
-0
lines changed

2 files changed

+49
-0
lines changed

src/java_bytecode/java_types.cpp

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -314,3 +314,50 @@ symbol_typet java_classname(const std::string &id)
314314

315315
return symbol_type;
316316
}
317+
318+
/// Programmatic documentation of the structure of a Java array (of either
319+
/// primitives or references) type.
320+
/// A Java array is represented in GOTO in the following way:
321+
/// A struct component with a tag like java::array[type] where type is either
322+
/// a primitive like int, or reference.
323+
/// The struct has precisely three components:
324+
/// 1. \@java.lang.Object: of type struct {java.lang.Object} containing the base
325+
/// class data
326+
/// 2. length: of type Java integer - the length of the array
327+
/// 3. data: of type pointer to either pointer to a primitive type, or pointer
328+
/// to pointer to empty (i.e. a void**) pointing to the contents of the array
329+
/// \param type: A type that might represent a Java array
330+
/// \return True if it is a Java array type, false otherwise
331+
bool is_valid_java_array(const struct_typet &type)
332+
{
333+
bool correct_num_components=type.components().size()==3;
334+
if(!correct_num_components)
335+
return false;
336+
337+
// First component, the base class (Object) data
338+
const struct_union_typet::componentt base_class_component=
339+
type.components()[0];
340+
341+
bool base_component_valid=true;
342+
base_component_valid&=base_class_component.get_name()=="@java.lang.Object";
343+
base_component_valid&=base_class_component.type().id()==ID_struct;
344+
base_component_valid&=
345+
base_class_component.type().get_string(ID_tag)=="java.lang.Object";
346+
347+
bool length_component_valid=true;
348+
const struct_union_typet::componentt length_component=
349+
type.components()[1];
350+
length_component_valid&=length_component.get_name()=="length";
351+
length_component_valid&=length_component.type()==java_int_type();
352+
353+
bool data_component_valid=true;
354+
const struct_union_typet::componentt data_component=
355+
type.components()[2];
356+
data_component_valid&=data_component.get_name()=="data";
357+
data_component_valid&=data_component.type().id()==ID_pointer;
358+
359+
return correct_num_components &&
360+
base_component_valid &&
361+
length_component_valid &&
362+
data_component_valid;
363+
}

src/java_bytecode/java_types.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,4 +74,6 @@ exprt java_bytecode_promotion(const exprt &);
7474

7575
bool is_java_array_tag(const irep_idt& tag);
7676

77+
bool is_valid_java_array(const struct_typet &type);
78+
7779
#endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H

0 commit comments

Comments
 (0)