CBMC
Loading...
Searching...
No Matches
Classes | Functions | Variables
java_object_factory.cpp File Reference
#include "java_object_factory.h"
#include <util/arith_tools.h>
#include <util/array_element_from_pointer.h>
#include <util/expr_initializer.h>
#include <util/fresh_symbol.h>
#include <util/interval_constraint.h>
#include <util/message.h>
#include <util/nondet_bool.h>
#include <util/symbol_table_base.h>
#include <goto-programs/class_identifier.h>
#include <goto-programs/goto_functions.h>
#include "generic_parameter_specialization_map_keys.h"
#include "java_object_factory_parameters.h"
#include "java_static_initializers.h"
#include "java_string_library_preprocess.h"
#include "java_string_literals.h"
#include "java_utils.h"
#include "select_pointer_type.h"
+ Include dependency graph for java_object_factory.cpp:

Go to the source code of this file.

Classes

class   java_object_factoryt
 
class   recursion_set_entryt
  Recursion-set entry owner class. More...
 

Functions

static irep_idt  integer_interval_to_string (const integer_intervalt &interval)
  Converts and integer_intervalt to a a string of the for [lower]-[upper].
 
void  initialize_nondet_string_fields (struct_exprt &struct_expr, code_blockt &code, const std::size_t &min_nondet_string_length, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable, allocate_objectst &allocate_objects)
  Initialise length and data fields for a nondeterministic String structure.
 
alternate_casest  get_string_input_values_code (const exprt &expr, const std::list< std::string > &string_input_values, symbol_table_baset &symbol_table)
  Creates an alternate_casest vector in which each item contains an assignment of a string from string_input_values (or more precisely the literal symbol corresponding to the string) to expr.
 
static code_blockt  assume_expr_integral (const exprt &expr, const typet &type, const source_locationt &location, const allocate_local_symbolt &allocate_local_symbol)
  Generate code block that verifies that an expression of type float or double has integral value.
 
static void  allocate_nondet_length_array (code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type, const allocate_local_symbolt &allocate_local_symbol, const source_locationt &location)
  Allocates a fresh array and emits an assignment writing to lhs the address of the new array.
 
static void  array_primitive_init_code (code_blockt &assignments, const exprt &init_array_expr, const typet &element_type, const exprt &max_length_expr, const source_locationt &location, const allocate_local_symbolt &allocate_local_symbol)
  Create code to nondeterministically initialize arrays of primitive type.
 
static void  array_loop_init_code (code_blockt &assignments, const exprt &init_array_expr, const exprt &length_expr, const typet &element_type, const exprt &max_length_expr, update_in_placet update_in_place, const source_locationt &location, const array_element_generatort &element_generator, const allocate_local_symbolt &allocate_local_symbol, const symbol_table_baset &symbol_table)
  Create code to nondeterministically initialize each element of an array in a loop.
 
code_blockt  gen_nondet_array_init (const exprt &expr, update_in_placet update_in_place, const source_locationt &location, const array_element_generatort &element_generator, const allocate_local_symbolt &allocate_local_symbol, const symbol_table_baset &symbol_table, const size_t max_nondet_array_length)
  Synthesize GOTO for generating a array of nondet length to be stored in the expr.
 
static void  assert_type_consistency (const code_blockt &assignments)
 
exprt  object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, lifetimet lifetime, const source_locationt &loc, const select_pointer_typet &pointer_type_selector, message_handlert &log)
  Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing the the argument expr passed to that function, we create a static global object of type type and non-deterministically initialize it.
 
void  gen_nondet_init (const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
  Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects as necessary and nondet-initializing their members, or if MAY_ or MUST_UPDATE_IN_PLACE is set, re-initializing already-allocated objects.
 
exprt  object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, const java_object_factory_parameterst &object_factory_parameters, lifetimet lifetime, const source_locationt &location, message_handlert &log)
  Call object_factory() above with a default (identity) pointer_type_selector.
 
void  gen_nondet_init (const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, update_in_placet update_in_place, message_handlert &log)
  Call gen_nondet_init() above with a default (identity) pointer_type_selector.
 

Variables

const integer_intervalt  printable_char_range (' ', '~')
  Interval that represents the printable character range range U+0020-U+007E, i.e.
 

Function Documentation

◆  allocate_nondet_length_array()

static void allocate_nondet_length_array ( code_blockt &  assignments,
const exprt &  lhs,
const exprt &  max_length_expr,
const typet &  element_type,
const allocate_local_symbolt &  allocate_local_symbol,
const source_locationt &  location 
)
static

Allocates a fresh array and emits an assignment writing to lhs the address of the new array.

Single-use at the moment, but useful to keep as a separate function for downstream branches.

Parameters
[out] assignments Code is emitted here.
lhs Symbol to assign the new array structure.
max_length_expr Maximum length of the new array (minimum is fixed at zero for now).
element_type Actual element type of the array (the array for all reference types will have void* type, but this will be annotated as the true member type).
allocate_local_symbol A function to generate a new local symbol and add it to the symbol table
location Source location associated with nondet-initialization.

Definition at line 1138 of file java_object_factory.cpp.

◆  array_loop_init_code()

static void array_loop_init_code ( code_blockt &  assignments,
const exprt &  init_array_expr,
const exprt &  length_expr,
const typet &  element_type,
const exprt &  max_length_expr,
update_in_placet  update_in_place,
const source_locationt &  location,
const array_element_generatort &  element_generator,
const allocate_local_symbolt &  allocate_local_symbol,
const symbol_table_baset &  symbol_table 
)
static

Create code to nondeterministically initialize each element of an array in a loop.

The code produced is of the form (supposing an array of type OBJ):

struct OBJ **array_data_init;
GOTO 4
*malloc_site = {...};
malloc_site->value = NONDET(int);
GOTO 2
5: ...
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
ait()
Definition ai.h:569
@ NONDET
havocs the pointer to an nondet pointer
@ GOTO
Definition goto_program.h:33
Parameters
[out] assignments : Code block to which the initializing assignments will be appended.
init_array_expr : array data
length_expr : array length
element_type type of array elements
max_length_expr : max length, as specified by max-nondet-array-length
update_in_place NO_UPDATE_IN_PLACE: initialize expr from scratch MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_ and MUST_ cases. MUST_UPDATE_IN_PLACE: reinitialize an existing object
location Source location associated with nondet-initialization.
element_generator A function for generating the body of the loop which creates and assigns the element at the position.
allocate_local_symbol A function to generate a new local symbol and add it to the symbol table
symbol_table The symbol table.

Definition at line 1326 of file java_object_factory.cpp.

◆  array_primitive_init_code()

static void array_primitive_init_code ( code_blockt &  assignments,
const exprt &  init_array_expr,
const typet &  element_type,
const exprt &  max_length_expr,
const source_locationt &  location,
const allocate_local_symbolt &  allocate_local_symbol 
)
static

Create code to nondeterministically initialize arrays of primitive type.

The code produced is of the form (for an array of type TYPE):

Parameters
[out] assignments : Code block to which the initializing assignments will be appended.
init_array_expr : array data
element_type type of array elements
max_length_expr : the (constant) size to which initialise the array
location Source location associated with nondet-initialization.
allocate_local_symbol A function to generate a new local symbol and add it to the symbol table

Definition at line 1182 of file java_object_factory.cpp.

◆  assert_type_consistency()

static void assert_type_consistency ( const code_blockt &  assignments )
static

Definition at line 1517 of file java_object_factory.cpp.

◆  assume_expr_integral()

static code_blockt assume_expr_integral ( const exprt &  expr,
const typet &  type,
const source_locationt &  location,
const allocate_local_symbolt &  allocate_local_symbol 
)
static

Generate code block that verifies that an expression of type float or double has integral value.

For example, for a float expression floatVal we generate: int assume_integral_tmp; assume_integral_tmp = NONDET(int); ASSUME FLOAT_TYPECAST(assume_integral_tmp, float, __CPROVER_rounding_mode) == floatVal

Parameters
expr The expression we want to make an assumption on
type The type of the expression
location Source location associated with the expression
allocate_local_symbol A function to generate a new local symbol and add it to the symbol table
Returns
Code block constructing the auxiliary nondet integer and an assume statement that the integer is equal to the value of the expression

Definition at line 937 of file java_object_factory.cpp.

◆  gen_nondet_array_init()

code_blockt gen_nondet_array_init ( const exprt &  expr,
update_in_placet  update_in_place,
const source_locationt &  location,
const array_element_generatort &  element_generator,
const allocate_local_symbolt &  allocate_local_symbol,
const symbol_table_baset &  symbol_table,
size_t  max_nondet_array_length 
)

Synthesize GOTO for generating a array of nondet length to be stored in the expr.

Parameters
expr The array expression to initialize.
update_in_place Should the code allow the solver the freedom to leave the array as is.
location Source location to use for all synthesized code.
element_generator A function that creates a new element and assigns it to the provided expression.
allocate_local_symbol A function that creates a local symbol in the symbol table. See java_object_factoryt::assign_element for an example implementation.
symbol_table The symbol table.
max_nondet_array_length The maximum size the array can be.
Returns
The GOTO that approximates:
array_length = NONDET(int)
ASSUME(array_length < max_nondet_array_length)
expr = java_new_array(max_nondet_array_length)
expr->length = array_length
for (int i = 0; i < array_length; ++i)
@ ASSUME
Definition goto_program.h:34

Definition at line 1372 of file java_object_factory.cpp.

◆  gen_nondet_init() [1/2]

void gen_nondet_init ( const exprt &  expr,
code_blockt &  init_code,
symbol_table_baset &  symbol_table,
const source_locationt &  loc,
bool  skip_classid,
lifetimet  lifetime,
const java_object_factory_parameterst &  object_factory_parameters,
const select_pointer_typet &  pointer_type_selector,
update_in_placet  update_in_place,
message_handlert &  log 
)

Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects as necessary and nondet-initializing their members, or if MAY_ or MUST_UPDATE_IN_PLACE is set, re-initializing already-allocated objects.

Parameters
expr Lvalue expression to initialize.
[out] init_code A code block where the initializing assignments will be appended to. It gets an instruction sequence to initialize or reinitialize expr and child objects it refers to.
symbol_table The symbol table, where new variables created as a result of emitting code to init_code will be inserted to. This includes any necessary temporaries, and if create_dyn_objs is false, any allocated objects.
loc Source location to which all generated code will be associated to.
skip_classid If true, skip initializing field @class_identifier.
lifetime Lifetime of the allocated objects (AUTOMATIC_LOCAL, STATIC_GLOBAL, or DYNAMIC)
object_factory_parameters Parameters for the generation of non deterministic objects.
pointer_type_selector The pointer_selector to use to resolve pointer types where required.
update_in_place NO_UPDATE_IN_PLACE: initialize expr from scratch MAY_UPDATE_IN_PLACE: generate a runtime nondet branch between the NO_ and MUST_ cases. MUST_UPDATE_IN_PLACE: reinitialize an existing object
log used to report object construction warnings and failures

Definition at line 1621 of file java_object_factory.cpp.

◆  gen_nondet_init() [2/2]

void gen_nondet_init ( const exprt &  expr,
code_blockt &  init_code,
symbol_table_baset &  symbol_table,
const source_locationt &  loc,
bool  skip_classid,
lifetimet  lifetime,
const java_object_factory_parameterst &  object_factory_parameters,
update_in_placet  update_in_place,
message_handlert &  log 
)

Call gen_nondet_init() above with a default (identity) pointer_type_selector.

Definition at line 1678 of file java_object_factory.cpp.

◆  get_string_input_values_code()

alternate_casest get_string_input_values_code ( const exprt &  expr,
const std::list< std::string > &  string_input_values,
symbol_table_baset &  symbol_table 
)

Creates an alternate_casest vector in which each item contains an assignment of a string from string_input_values (or more precisely the literal symbol corresponding to the string) to expr.

Parameters
expr Struct-typed lvalue expression to which we want to assign the strings.
string_input_values Strings to assign.
symbol_table The symbol table in which we'll lool up literal symbol
Returns
A vector that can be passed to generate_nondet_switch

Definition at line 725 of file java_object_factory.cpp.

◆  initialize_nondet_string_fields()

void initialize_nondet_string_fields ( struct_exprt &  struct_expr,
code_blockt &  code,
const std::size_t &  min_nondet_string_length,
const std::size_t &  max_nondet_string_length,
const source_locationt &  loc,
const irep_idt &  function_id,
symbol_table_baset &  symbol_table,
bool  printable,
allocate_objectst &  allocate_objects 
)

Initialise length and data fields for a nondeterministic String structure.

If the structure is not a nondeterministic structure, the call results in a precondition violation.

Parameters
[out] struct_expr struct that we initialize
code block to add pre-requisite declarations (e.g. to allocate a data array)
min_nondet_string_length minimum length of strings to initialize
max_nondet_string_length maximum length of strings to initialize
loc location in the source
function_id function ID to associate with auxiliary variables
symbol_table the symbol table
printable if true, the nondet string must consist of printable characters only
allocate_objects manages memory allocation and keeps track of the newly created symbols

The code produced is of the form:

Unit tests in unit/java_bytecode/java_object_factory/ ensure it is the case.

Definition at line 362 of file java_object_factory.cpp.

◆  integer_interval_to_string()

static irep_idt integer_interval_to_string ( const integer_intervalt &  interval )
static

Converts and integer_intervalt to a a string of the for [lower]-[upper].

Definition at line 314 of file java_object_factory.cpp.

◆  object_factory() [1/2]

exprt object_factory ( const typet &  type,
const irep_idt  base_name,
code_blockt &  init_code,
symbol_table_baset &  symbol_table,
const java_object_factory_parameterst &  object_factory_parameters,
lifetimet  lifetime,
const source_locationt &  location,
message_handlert &  log 
)

Call object_factory() above with a default (identity) pointer_type_selector.

Definition at line 1654 of file java_object_factory.cpp.

◆  object_factory() [2/2]

exprt object_factory ( const typet &  type,
const irep_idt  base_name,
code_blockt &  init_code,
symbol_table_baset &  symbol_table,
java_object_factory_parameterst  parameters,
lifetimet  lifetime,
const source_locationt &  loc,
const select_pointer_typet &  pointer_type_selector,
message_handlert &  log 
)

Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing the the argument expr passed to that function, we create a static global object of type type and non-deterministically initialize it.

See gen_nondet_init for a description of the parameters. The only new one is type, which is the type of the object to create.

Returns
The object created, the symbol_table gains any new symbols created, and init_code gains any instructions required to initialize either the returned value or its child objects

Definition at line 1544 of file java_object_factory.cpp.

Variable Documentation

◆  printable_char_range

const integer_intervalt printable_char_range(' ', '~') ( ' '  ,
'~'   
)

Interval that represents the printable character range range U+0020-U+007E, i.e.

' ' to '~'

AltStyle によって変換されたページ (->オリジナル) /