Skip to content

Cleanup/java object factory #693

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 4 commits into from
Mar 25, 2017
+48 −105
Merged

Cleanup/java object factory #693

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2b09c0b
Remove unused variable and braces
Mar 24, 2017
a3f49a3
Move function comments to the right place
Mar 24, 2017
4c4ccc0
Remove variable that is always false
Mar 24, 2017
9a1dae0
Remove function that's only used once
Mar 24, 2017
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
141 changes: 48 additions & 93 deletions src/java_bytecode/java_object_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,18 +25,6 @@ Author: Daniel Kroening, [email protected]
#include "java_types.h"
#include "java_utils.h"

/*******************************************************************\

Function: gen_nondet_init

Inputs:

Outputs:

Purpose:

\*******************************************************************/

class java_object_factoryt:public messaget
{
code_blockt &init_code;
Expand Down Expand Up @@ -75,25 +63,20 @@ class java_object_factoryt:public messaget
bool is_sub,
irep_idt class_identifier,
const source_locationt &loc,
bool skip_classid,
bool create_dynamic_objects,
bool override=false,
const typet &override_type=empty_typet());
};


/*******************************************************************\

Function: gen_nondet_array_init
Function: java_object_factoryt::allocate_object

Inputs: the target expression, desired object type, source location
and Boolean whether to create a dynamic object
Inputs:

Outputs: the allocated object
Outputs:

Purpose: Returns false if we can't figure out the size of allocate_type.
allocate_type may differ from target_expr, e.g. for target_expr
having type int* and allocate_type being an int[10].
Purpose:

\*******************************************************************/

Expand Down Expand Up @@ -165,16 +148,33 @@ exprt java_object_factoryt::allocate_object(
}
}

// Override type says to ignore the LHS' real type, and init it with the given
// type regardless. Used at the moment for reference arrays, which are
// implemented as void* arrays but should be init'd as their true type with
// appropriate casts.
/*******************************************************************\

Function: java_object_factoryt::gen_nondet_init

Inputs:
expr -
is_sub -
class_identifier -
loc -
create_dynamic_objects -
override - Ignore the LHS' real type. Used at the moment for
reference arrays, which are implemented as void*
arrays but should be init'd as their true type with
appropriate casts.
override_type - Type to use if ignoring the LHS' real type

Outputs:

Purpose:

\*******************************************************************/

void java_object_factoryt::gen_nondet_init(
const exprt &expr,
bool is_sub,
irep_idt class_identifier,
const source_locationt &loc,
bool skip_classid,
bool create_dynamic_objects,
bool override,
const typet &override_type)
Expand Down Expand Up @@ -250,20 +250,17 @@ void java_object_factoryt::gen_nondet_init(
{
exprt allocated=
allocate_object(expr, subtype, loc, create_dynamic_objects);
{
exprt init_expr;
if(allocated.id()==ID_address_of)
init_expr=allocated.op0();
else
init_expr=dereference_exprt(allocated, allocated.type().subtype());
gen_nondet_init(
init_expr,
false,
"",
loc,
false,
create_dynamic_objects);
}
exprt init_expr;
if(allocated.id()==ID_address_of)
init_expr=allocated.op0();
else
init_expr=dereference_exprt(allocated, allocated.type().subtype());
gen_nondet_init(
init_expr,
false,
"",
loc,
create_dynamic_objects);
}

if(!assume_non_null)
Expand Down Expand Up @@ -297,9 +294,6 @@ void java_object_factoryt::gen_nondet_init(

if(name=="@class_identifier")
{
if(skip_classid)
continue;

irep_idt qualified_clsid="java::"+as_string(class_identifier);
constant_exprt ci(qualified_clsid, string_typet());
code_assignt code(me, ci);
Expand Down Expand Up @@ -327,7 +321,6 @@ void java_object_factoryt::gen_nondet_init(
_is_sub,
class_identifier,
loc,
false,
create_dynamic_objects);
}
}
Expand All @@ -345,7 +338,7 @@ void java_object_factoryt::gen_nondet_init(

/*******************************************************************\

Function: gen_nondet_array_init
Function: java_object_factoryt::gen_nondet_array_init

Inputs:

Expand Down Expand Up @@ -379,7 +372,7 @@ void java_object_factoryt::gen_nondet_array_init(
const auto &length_sym_expr=length_sym.symbol_expr();

// Initialize array with some undetermined length:
gen_nondet_init(length_sym_expr, false, irep_idt(), loc, false, false);
gen_nondet_init(length_sym_expr, false, irep_idt(), loc, false);

// Insert assumptions to bound its length:
binary_relation_exprt
Expand Down Expand Up @@ -464,7 +457,6 @@ void java_object_factoryt::gen_nondet_array_init(
false,
irep_idt(),
loc,
false,
true,
true,
element_type);
Expand All @@ -479,44 +471,6 @@ void java_object_factoryt::gen_nondet_array_init(

/*******************************************************************\

Function: gen_nondet_init

Inputs:

Outputs:

Purpose:

\*******************************************************************/

void gen_nondet_init(
const exprt &expr,
code_blockt &init_code,
symbol_tablet &symbol_table,
const source_locationt &loc,
bool skip_classid,
bool create_dyn_objs,
bool assume_non_null,
message_handlert &message_handler,
size_t max_nondet_array_length)
{
java_object_factoryt state(
init_code,
assume_non_null,
max_nondet_array_length,
symbol_table,
message_handler);
state.gen_nondet_init(
expr,
false,
"",
loc,
skip_classid,
create_dyn_objs);
}

/*******************************************************************\

Function: new_tmp_symbol

Inputs:
Expand Down Expand Up @@ -592,17 +546,18 @@ exprt object_factory(

exprt object=aux_symbol.symbol_expr();

const namespacet ns(symbol_table);
gen_nondet_init(
object,
java_object_factoryt state(
init_code,
!allow_null,
max_nondet_array_length,
symbol_table,
loc,
false,
message_handler);
state.gen_nondet_init(
object,
false,
!allow_null,
message_handler,
max_nondet_array_length);
"",
loc,
false);

return object;
}
Expand Down
12 changes: 0 additions & 12 deletions src/java_bytecode/java_object_factory.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,18 +22,6 @@ exprt object_factory(
const source_locationt &,
message_handlert &message_handler);

void gen_nondet_init(
const exprt &expr,
code_blockt &init_code,
symbol_tablet &symbol_table,
const source_locationt &,
bool skip_classid,
bool create_dynamic_objects,
bool assume_non_null,
message_handlert &message_handler,
size_t max_nondet_array_length=5);


exprt get_nondet_bool(const typet &);

symbolt &new_tmp_symbol(
Expand Down