Merge pull request #4416 from antlechner/antonia/nondet-int-refactor

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

Author: antlechner

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -156,13 +156,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,
@@ -1089,53 +1082,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.
@@ -1158,12 +1104,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);
@@ -1462,12 +1409,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);

src/util/nondet.cpp

@@ -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.
@@ -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,
@@ -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;

src/util/nondet.h

@@ -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,
+///   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,