Skip to content

De-duplicate "generate a nondet int in a given range" logic #4416

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 7 commits into from
Mar 22, 2019
Merged

De-duplicate "generate a nondet int in a given range" logic #4416

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
0d32a43
Move nondet documentation to header file
antlechner Mar 21, 2019
6278e42
Split generate_nondet_int into two functions
antlechner Mar 21, 2019
cbd00e6
Make precondition on min/max values less strict
antlechner Mar 22, 2019
9e243c9
Parameterize basename_prefix
antlechner Mar 21, 2019
f6e6ad6
Use allocate_objects to manage new symbol creation
antlechner Mar 21, 2019
eeb9f22
Tidy up includes
antlechner Mar 22, 2019
63d9f50
Remove duplicate helper function in object factory
antlechner Mar 21, 2019
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
72 changes: 10 additions & 62 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 @@ -160,13 +160,6 @@ class java_object_factoryt
size_t depth,
const source_locationt &location);

const symbol_exprt gen_nondet_int_init(
code_blockt &assignments,
const std::string &basename_prefix,
const exprt &min_length_expr,
const exprt &max_length_expr,
const source_locationt &location);

void gen_method_call_if_present(
code_blockt &assignments,
const exprt &instance_expr,
Expand Down Expand Up @@ -1103,53 +1096,6 @@ void java_object_factoryt::declare_created_symbols(code_blockt &init_code)
allocate_objects.declare_created_symbols(init_code);
}

/// Nondeterministically initializes an int i in the range min <= i <= max,
/// where min is the integer represented by `min_value_expr` and max is the
/// integer represented by `max_value_expr`.
/// \param [out] assignments: A code block that the initializing assignments
/// will be appended to.
/// \param basename_prefix: Used for naming the newly created symbol.
/// \param min_value_expr: Represents the minimum value for the integer.
/// \param max_value_expr: Represents the maximum value for the integer.
/// \param location: Source location associated with nondet-initialization.
/// \return A symbol expression for the resulting integer.
const symbol_exprt java_object_factoryt::gen_nondet_int_init(
code_blockt &assignments,
const std::string &basename_prefix,
const exprt &min_value_expr,
const exprt &max_value_expr,
const source_locationt &location)
{
PRECONDITION(min_value_expr.type() == max_value_expr.type());

const symbol_exprt &int_symbol_expr =
allocate_objects.allocate_automatic_local_object(
min_value_expr.type(), basename_prefix);

// Nondet-initialize it
gen_nondet_init(
assignments,
int_symbol_expr,
false, // is_sub
irep_idt(),
false, // skip_classid
lifetimet::AUTOMATIC_LOCAL, // immaterial, type is primitive
{}, // no override type
0, // depth is immaterial, always non-null
update_in_placet::NO_UPDATE_IN_PLACE,
location);

// Insert assumptions to bound its value
const auto min_assume_expr =
binary_relation_exprt(int_symbol_expr, ID_ge, min_value_expr);
const auto max_assume_expr =
binary_relation_exprt(int_symbol_expr, ID_le, max_value_expr);
assignments.add(code_assumet(min_assume_expr));
assignments.add(code_assumet(max_assume_expr));

return int_symbol_expr;
}

/// Allocates a fresh array and emits an assignment writing to \p lhs the
/// address of the new array. Single-use at the moment, but useful to keep as a
/// separate function for downstream branches.
Expand All @@ -1172,12 +1118,13 @@ void java_object_factoryt::allocate_nondet_length_array(
const typet &element_type,
const source_locationt &location)
{
const auto &length_sym_expr = gen_nondet_int_init(
assignments,
"nondet_array_length",
const auto &length_sym_expr = generate_nondet_int(
from_integer(0, java_int_type()),
max_length_expr,
location);
"nondet_array_length",
location,
allocate_objects,
assignments);

side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), loc);
java_new_array.copy_to_operands(length_sym_expr);
Expand Down Expand Up @@ -1476,12 +1423,13 @@ bool java_object_factoryt::gen_nondet_enum_init(
const member_exprt enum_array_expr =
member_exprt(deref_expr, "data", comps[2].type());

const symbol_exprt &index_expr = gen_nondet_int_init(
assignments,
"enum_index_init",
const symbol_exprt &index_expr = generate_nondet_int(
from_integer(0, java_int_type()),
minus_exprt(length_expr, from_integer(1, java_int_type())),
location);
"enum_index_init",
location,
allocate_objects,
assignments);

// Generate statement using pointer arithmetic to access array element:
// expr = (expr.type())*(enum_array_expr + index_expr);
Expand Down
93 changes: 39 additions & 54 deletions src/util/nondet.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,48 +8,26 @@ Author: Diffblue Ltd.

#include "nondet.h"

#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/fresh_symbol.h>
#include <util/symbol.h>

/// Gets a fresh nondet choice in range (min_value, max_value). GOTO generated
/// resembles:
/// ```
/// int_type name_prefix::nondet_int = NONDET(int_type)
/// ASSUME(name_prefix::nondet_int >= min_value)
/// ASSUME(name_prefix::nondet_int <= max_value)
/// ```
/// \param min_value: Minimum value (inclusive) of returned int.
/// \param max_value: Maximum value (inclusive) of returned int.
/// \param name_prefix: Prefix for the fresh symbol name generated (should be
/// function id)
/// \param int_type: The type of the int used to non-deterministically choose
/// one of the switch cases.
/// \param mode: Mode (language) of the symbol to be generated.
/// \param source_location: The location to mark the generated int with.
/// \param symbol_table: The global symbol table.
/// \param [out] instructions: Output instructions are written to
/// 'instructions'. These declare, nondet-initialise and range-constrain (with
/// assume statements) a fresh integer.
/// \return Returns a symbol expression for the resulting integer.
#include "allocate_objects.h"
#include "arith_tools.h"
#include "c_types.h"
#include "fresh_symbol.h"
#include "symbol.h"

symbol_exprt generate_nondet_int(
const mp_integer &min_value,
const mp_integer &max_value,
const std::string &name_prefix,
const typet &int_type,
const irep_idt &mode,
const exprt &min_value_expr,
const exprt &max_value_expr,
const std::string &basename_prefix,
const source_locationt &source_location,
symbol_table_baset &symbol_table,
allocate_objectst &allocate_objects,
code_blockt &instructions)
{
PRECONDITION(min_value < max_value);
PRECONDITION(min_value_expr.type() == max_value_expr.type());
const typet &int_type = min_value_expr.type();

// Declare a symbol for the non deterministic integer.
const symbol_exprt &nondet_symbol =
get_fresh_aux_symbol(
int_type, name_prefix, "nondet_int", source_location, mode, symbol_table)
.symbol_expr();
allocate_objects.allocate_automatic_local_object(int_type, basename_prefix);
instructions.add(code_declt(nondet_symbol));

// Assign the symbol any non deterministic integer value.
Expand All @@ -60,30 +38,35 @@ symbol_exprt generate_nondet_int(
// Constrain the non deterministic integer with a lower bound of `min_value`.
// ASSUME(name_prefix::nondet_int >= min_value)
instructions.add(
code_assumet(
binary_predicate_exprt(
nondet_symbol, ID_ge, from_integer(min_value, int_type))));
code_assumet(binary_predicate_exprt(nondet_symbol, ID_ge, min_value_expr)));

// Constrain the non deterministic integer with an upper bound of `max_value`.
// ASSUME(name_prefix::nondet_int <= max_value)
instructions.add(
code_assumet(
binary_predicate_exprt(
nondet_symbol, ID_le, from_integer(max_value, int_type))));
code_assumet(binary_predicate_exprt(nondet_symbol, ID_le, max_value_expr)));

return nondet_symbol;
}

/// Pick nondeterministically between imperative actions 'switch_cases'.
/// \param name_prefix: Name prefix for fresh symbols (should be function id)
/// \param switch_cases: List of codet objects to execute in each switch case.
/// \param int_type: The type of the int used to non-deterministically choose
/// one of the switch cases.
/// \param mode: Mode (language) of the symbol to be generated.
/// \param source_location: The location to mark the generated int with.
/// \param symbol_table: The global symbol table.
/// \return Returns a nondet-switch choosing between switch_cases. The resulting
/// switch block has no default case.
symbol_exprt generate_nondet_int(
const mp_integer &min_value,
const mp_integer &max_value,
const std::string &basename_prefix,
const typet &int_type,
const source_locationt &source_location,
allocate_objectst &allocate_objects,
code_blockt &instructions)
{
PRECONDITION(min_value <= max_value);
return generate_nondet_int(
from_integer(min_value, int_type),
from_integer(max_value, int_type),
basename_prefix,
source_location,
allocate_objects,
instructions);
}

code_blockt generate_nondet_switch(
const irep_idt &name_prefix,
const alternate_casest &switch_cases,
Expand All @@ -99,14 +82,16 @@ code_blockt generate_nondet_switch(

code_blockt result_block;

allocate_objectst allocate_objects{
mode, source_location, name_prefix, symbol_table};

const symbol_exprt &switch_value = generate_nondet_int(
0,
switch_cases.size() - 1,
id2string(name_prefix),
"nondet_int",
int_type,
mode,
source_location,
symbol_table,
allocate_objects,
result_block);

code_blockt switch_block;
Expand Down
59 changes: 53 additions & 6 deletions src/util/nondet.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,22 +9,69 @@ Author: Diffblue Ltd.
#ifndef CPROVER_JAVA_BYTECODE_NONDET_H
#define CPROVER_JAVA_BYTECODE_NONDET_H

#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
#include "std_code.h"
#include "std_expr.h"

class allocate_objectst;
class symbol_table_baset;

/// Same as \ref generate_nondet_int(
/// const mp_integer &min_value,
Copy link
Collaborator

Choose a reason for hiding this comment

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

Does this multi-line \ref actually render correctly in Doxygen?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I tried it locally and it links to the right function, though only the generate_nondet_init part turns into a link. Some of the parameter types (like source_locationt) also appear as links to the Doxygen for those types.
If there is a better / more standard way of linking between overloaded functions, please let me know.

/// const mp_integer &max_value,
/// const std::string &name_prefix,
/// const typet &int_type,
/// const irep_idt &mode,
/// const source_locationt &source_location,
/// symbol_table_baset &symbol_table,
/// code_blockt &instructions)
/// except the minimum and maximum values are represented as exprts.
symbol_exprt generate_nondet_int(
const exprt &min_value_expr,
const exprt &max_value_expr,
const std::string &basename_prefix,
const source_locationt &source_location,
allocate_objectst &allocate_objects,
code_blockt &instructions);

/// Gets a fresh nondet choice in range (min_value, max_value). GOTO generated
/// resembles:
/// ```
/// int_type name_prefix::nondet_int = NONDET(int_type)
/// ASSUME(name_prefix::nondet_int >= min_value)
/// ASSUME(name_prefix::nondet_int <= max_value)
/// ```
/// \param min_value: Minimum value (inclusive) of returned int.
/// \param max_value: Maximum value (inclusive) of returned int.
/// \param basename_prefix: Basename prefix for the fresh symbol name generated.
/// \param int_type: The type of the int used to non-deterministically choose
/// one of the switch cases.
/// \param allocate_objects: Handles allocation of new objects.
/// \param source_location: The location to mark the generated int with.
/// \param [out] instructions: Output instructions are written to
/// 'instructions'. These declare, nondet-initialise and range-constrain (with
/// assume statements) a fresh integer.
/// \return Returns a symbol expression for the resulting integer.
symbol_exprt generate_nondet_int(
const mp_integer &min_value,
const mp_integer &max_value,
const std::string &name_prefix,
const std::string &basename_prefix,
const typet &int_type,
const irep_idt &mode,
const source_locationt &source_location,
symbol_table_baset &symbol_table,
allocate_objectst &allocate_objects,
code_blockt &instructions);

typedef std::vector<codet> alternate_casest;

/// Pick nondeterministically between imperative actions 'switch_cases'.
/// \param name_prefix: Name prefix for fresh symbols (should be function id)
/// \param switch_cases: List of codet objects to execute in each switch case.
/// \param int_type: The type of the int used to non-deterministically choose
/// one of the switch cases.
/// \param mode: Mode (language) of the symbol to be generated.
/// \param source_location: The location to mark the generated int with.
/// \param symbol_table: The global symbol table.
/// \return Returns a nondet-switch choosing between switch_cases. The resulting
/// switch block has no default case.
code_blockt generate_nondet_switch(
const irep_idt &name_prefix,
const alternate_casest &switch_cases,
Expand Down