Skip to content

Recursive nondet init of pointers to structs [blocks: #3443] #3251

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 10 commits into from
Nov 27, 2018
Merged

Recursive nondet init of pointers to structs [blocks: #3443] #3251

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
493fcda
Move object factory parameters to util and add java object factory pa…
danpoe Oct 29, 2018
f0a7f1f
Add source location parameter to get_nondet_bool()
danpoe Oct 29, 2018
d92e817
Use get_nondet_bool() in the c nondet symbol factory
danpoe Oct 29, 2018
19effd3
Remove c_new_tmp_symbol
danpoe Oct 29, 2018
7f95dd8
Add c object factory parameters
danpoe Oct 29, 2018
d4e14c2
Parse c object factory options
danpoe Oct 29, 2018
fac59a8
Pass object factory parameters through to object factories
danpoe Oct 30, 2018
8722822
Add regression tests for nondet struct init
danpoe Oct 31, 2018
a481241
Add recursive nondet struct initialization
danpoe Oct 31, 2018
0b605ea
Update documentation of max_nondet_tree_depth object factory parameter
danpoe Nov 5, 2018
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
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ SRC = bytecode_info.cpp \
java_entry_point.cpp \
java_local_variable_table.cpp \
java_object_factory.cpp \
java_object_factory_parameters.cpp \
java_pointer_casts.cpp \
java_qualifiers.cpp \
java_root_class.cpp \
Expand All @@ -35,7 +36,6 @@ SRC = bytecode_info.cpp \
java_types.cpp \
java_utils.cpp \
load_method_by_regex.cpp \
object_factory_parameters.cpp \
mz_zip_archive.cpp \
remove_exceptions.cpp \
remove_instanceof.cpp \
Expand Down
16 changes: 8 additions & 8 deletions jbmc/src/java_bytecode/convert_java_nondet.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ static goto_programt get_gen_nondet_init_instructions(
const source_locationt &source_loc,
symbol_table_baset &symbol_table,
message_handlert &message_handler,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
const irep_idt &mode)
{
code_blockt gen_nondet_init_code;
Expand Down Expand Up @@ -82,7 +82,7 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
const goto_programt::targett &target,
symbol_table_baset &symbol_table,
message_handlert &message_handler,
object_factory_parameterst object_factory_parameters,
java_object_factory_parameterst object_factory_parameters,
const irep_idt &mode)
{
const auto next_instr = std::next(target);
Expand Down Expand Up @@ -172,7 +172,7 @@ void convert_nondet(
goto_programt &goto_program,
symbol_table_baset &symbol_table,
message_handlert &message_handler,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
const irep_idt &mode)
{
bool changed = false;
Expand Down Expand Up @@ -200,10 +200,10 @@ void convert_nondet(
void convert_nondet(
goto_model_functiont &function,
message_handlert &message_handler,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
const irep_idt &mode)
{
object_factory_parameterst parameters = object_factory_parameters;
java_object_factory_parameterst parameters = object_factory_parameters;
parameters.function_id = function.get_function_id();
convert_nondet(
function.get_goto_function().body,
Expand All @@ -219,7 +219,7 @@ void convert_nondet(
goto_functionst &goto_functions,
symbol_table_baset &symbol_table,
message_handlert &message_handler,
const object_factory_parameterst &object_factory_parameters)
const java_object_factory_parameterst &object_factory_parameters)
{
const namespacet ns(symbol_table);

Expand All @@ -229,7 +229,7 @@ void convert_nondet(

if(symbol.mode==ID_java)
{
object_factory_parameterst parameters = object_factory_parameters;
java_object_factory_parameterst parameters = object_factory_parameters;
parameters.function_id = f_it.first;
convert_nondet(
f_it.second.body,
Expand All @@ -248,7 +248,7 @@ void convert_nondet(
void convert_nondet(
goto_modelt &goto_model,
message_handlert &message_handler,
const object_factory_parameterst& object_factory_parameters)
const java_object_factory_parameterst &object_factory_parameters)
{
convert_nondet(
goto_model.goto_functions,
Expand Down
8 changes: 4 additions & 4 deletions jbmc/src/java_bytecode/convert_java_nondet.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ class symbol_table_baset;
class goto_modelt;
class goto_model_functiont;
class message_handlert;
struct object_factory_parameterst;
struct java_object_factory_parameterst;

/// Converts side_effect_exprt_nondett expressions using java_object_factory.
/// For example, NONDET(SomeClass *) may become a nondet choice between a null
Expand All @@ -40,12 +40,12 @@ void convert_nondet(
goto_functionst &goto_functions,
symbol_table_baset &symbol_table,
message_handlert &message_handler,
const object_factory_parameterst &object_factory_parameters);
const java_object_factory_parameterst &object_factory_parameters);

void convert_nondet(
goto_modelt &,
message_handlert &,
const object_factory_parameterst &object_factory_parameters);
const java_object_factory_parameterst &object_factory_parameters);

/// Converts side_effect_exprt_nondett expressions using java_object_factory.
/// For example, NONDET(SomeClass *) may become a nondet choice between a null
Expand All @@ -64,7 +64,7 @@ void convert_nondet(
void convert_nondet(
goto_model_functiont &function,
message_handlert &message_handler,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
const irep_idt &mode);

#endif // CPROVER_JAVA_BYTECODE_CONVERT_NONDET_H
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/java_bytecode_language.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,9 @@ Author: Daniel Kroening, [email protected]
#include "ci_lazy_methods.h"
#include "ci_lazy_methods_needed.h"
#include "java_class_loader.h"
#include "java_object_factory_parameters.h"
#include "java_static_initializers.h"
#include "java_string_library_preprocess.h"
#include "object_factory_parameters.h"
#include "select_pointer_type.h"
#include "synthetic_methods_map.h"

Expand Down Expand Up @@ -179,7 +179,7 @@ class java_bytecode_languaget:public languaget
java_class_loadert java_class_loader;
bool threading_support;
bool assume_inputs_non_null; // assume inputs variables to be non-null
object_factory_parameterst object_factory_parameters;
java_object_factory_parameterst object_factory_parameters;
size_t max_user_array_length; // max size for user code created arrays
method_bytecodet method_bytecode;
lazy_methods_modet lazy_methods_mode;
Expand Down
12 changes: 6 additions & 6 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 @@ -122,7 +122,7 @@ static void java_static_lifetime_init(
symbol_table_baset &symbol_table,
const source_locationt &source_location,
bool assume_init_pointers_not_null,
object_factory_parameterst object_factory_parameters,
java_object_factory_parameterst object_factory_parameters,
const select_pointer_typet &pointer_type_selector,
bool string_refinement_enabled,
message_handlert &message_handler)
Expand Down Expand Up @@ -218,7 +218,7 @@ static void java_static_lifetime_init(
is_non_null_library_global(sym.name) ||
assume_init_pointers_not_null;

object_factory_parameterst parameters = object_factory_parameters;
java_object_factory_parameterst parameters = object_factory_parameters;
if(not_allow_null && !is_class_model)
parameters.min_null_tree_depth = 1;

Expand Down Expand Up @@ -278,7 +278,7 @@ exprt::operandst java_build_arguments(
code_blockt &init_code,
symbol_table_baset &symbol_table,
bool assume_init_pointers_not_null,
object_factory_parameterst object_factory_parameters,
java_object_factory_parameterst object_factory_parameters,
const select_pointer_typet &pointer_type_selector)
{
const java_method_typet::parameterst &parameters =
Expand Down Expand Up @@ -307,7 +307,7 @@ exprt::operandst java_build_arguments(
// be null
bool is_this=(param_number==0) && parameters[param_number].get_this();

object_factory_parameterst parameters = object_factory_parameters;
java_object_factory_parameterst parameters = object_factory_parameters;
// only pointer must be non-null
if(assume_init_pointers_not_null || is_this)
parameters.min_null_tree_depth = 1;
Expand Down Expand Up @@ -598,7 +598,7 @@ bool java_entry_point(
message_handlert &message_handler,
bool assume_init_pointers_not_null,
bool assert_uncaught_exceptions,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector,
bool string_refinement_enabled)
{
Expand Down Expand Up @@ -654,7 +654,7 @@ bool generate_java_start_function(
message_handlert &message_handler,
bool assume_init_pointers_not_null,
bool assert_uncaught_exceptions,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector)
{
messaget message(message_handler);
Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/java_entry_point.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ bool java_entry_point(
class message_handlert &message_handler,
bool assume_init_pointers_not_null,
bool assert_uncaught_exceptions,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector,
bool string_refinement_enabled);

Expand Down Expand Up @@ -76,7 +76,7 @@ bool generate_java_start_function(
class message_handlert &message_handler,
bool assume_init_pointers_not_null,
bool assert_uncaught_exceptions,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector);

#endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H
14 changes: 7 additions & 7 deletions jbmc/src/java_bytecode/java_object_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ class java_object_factoryt
/// methods in this class.
const source_locationt &loc;

const object_factory_parameterst object_factory_parameters;
const java_object_factory_parameterst object_factory_parameters;

/// This is employed in conjunction with the depth above. Every time the
/// non-det generator visits a type, the type is added to this set. We forbid
Expand Down Expand Up @@ -83,7 +83,7 @@ class java_object_factoryt
java_object_factoryt(
std::vector<const symbolt *> &_symbols_created,
const source_locationt &loc,
const object_factory_parameterst _object_factory_parameters,
const java_object_factory_parameterst _object_factory_parameters,
symbol_table_baset &_symbol_table,
const select_pointer_typet &pointer_type_selector)
: symbols_created(_symbols_created),
Expand Down Expand Up @@ -1212,7 +1212,7 @@ void java_object_factoryt::gen_nondet_init(
{
// types different from pointer or structure:
// bool, int, float, byte, char, ...
exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type)
exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc)
: side_effect_expr_nondett(type, loc);
code_assignt assign(expr, rhs);
assign.add_source_location()=loc;
Expand Down Expand Up @@ -1536,7 +1536,7 @@ exprt object_factory(
const irep_idt base_name,
code_blockt &init_code,
symbol_table_baset &symbol_table,
object_factory_parameterst parameters,
java_object_factory_parameterst parameters,
allocation_typet alloc_type,
const source_locationt &loc,
const select_pointer_typet &pointer_type_selector)
Expand Down Expand Up @@ -1629,7 +1629,7 @@ void gen_nondet_init(
const source_locationt &loc,
bool skip_classid,
allocation_typet alloc_type,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector,
update_in_placet update_in_place)
{
Expand Down Expand Up @@ -1666,7 +1666,7 @@ exprt object_factory(
const irep_idt base_name,
code_blockt &init_code,
symbol_tablet &symbol_table,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
allocation_typet alloc_type,
const source_locationt &location)
{
Expand All @@ -1690,7 +1690,7 @@ void gen_nondet_init(
const source_locationt &loc,
bool skip_classid,
allocation_typet alloc_type,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
update_in_placet update_in_place)
{
select_pointer_typet pointer_type_selector;
Expand Down
8 changes: 4 additions & 4 deletions jbmc/src/java_bytecode/java_object_factory.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ exprt object_factory(
const irep_idt base_name,
code_blockt &init_code,
symbol_table_baset &symbol_table,
object_factory_parameterst parameters,
java_object_factory_parameterst parameters,
allocation_typet alloc_type,
const source_locationt &location,
const select_pointer_typet &pointer_type_selector);
Expand All @@ -104,7 +104,7 @@ exprt object_factory(
const irep_idt base_name,
code_blockt &init_code,
symbol_tablet &symbol_table,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
allocation_typet alloc_type,
const source_locationt &location);

Expand All @@ -122,7 +122,7 @@ void gen_nondet_init(
const source_locationt &loc,
bool skip_classid,
allocation_typet alloc_type,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector,
update_in_placet update_in_place);

Expand All @@ -133,7 +133,7 @@ void gen_nondet_init(
const source_locationt &loc,
bool skip_classid,
allocation_typet alloc_type,
const object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &object_factory_parameters,
update_in_placet update_in_place);

exprt allocate_dynamic_object(
Expand Down
16 changes: 16 additions & 0 deletions jbmc/src/java_bytecode/java_object_factory_parameters.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
/*******************************************************************\

Module:

Author: Daniel Poetzl

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

#include "java_object_factory_parameters.h"
Copy link
Contributor

Choose a reason for hiding this comment

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

Why is this in a commit called "move object factory parameters to util"?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Ok, renamed the commit to "Move object factory parameters to util and add java object factory parameters" (plus a body with some more details).


void parse_java_object_factory_options(
const cmdlinet &cmdline,
optionst &options)
{
parse_object_factory_options(cmdline, options);
}
33 changes: 33 additions & 0 deletions jbmc/src/java_bytecode/java_object_factory_parameters.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
/*******************************************************************\

Module:

Author: Daniel Poetzl

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

#ifndef CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_PARAMETERS_H
#define CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_PARAMETERS_H

#include <util/object_factory_parameters.h>

struct java_object_factory_parameterst final : public object_factory_parameterst
Copy link
Member

Choose a reason for hiding this comment

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

Why this if they are the same?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

This would be a place to add options in the future that are not common to both the C and Java object factory. For C at least we expect some special options (e.g., to indicate which length function argument corresponds to which array function arguments).

{
java_object_factory_parameterst()
{
}

explicit java_object_factory_parameterst(const optionst &options)
: object_factory_parameterst(options)
{
}
};

/// Parse the java object factory parameters from a given command line
/// \param cmdline Command line
/// \param [out] options The options object that will be updated
void parse_java_object_factory_options(
const cmdlinet &cmdline,
optionst &options);

#endif
Loading