Add nondet.{h.cpp}

Author: Matthias Güdemann

jbmc/src/java_bytecode/Makefile

@@ -35,6 +35,7 @@ SRC = bytecode_info.cpp \
       java_utils.cpp \
       load_method_by_regex.cpp \
       mz_zip_archive.cpp \
+      nondet.cpp \
       remove_exceptions.cpp \
       remove_instanceof.cpp \
       remove_java_new.cpp \

jbmc/src/java_bytecode/nondet.cpp

@@ -0,0 +1,131 @@
+/*******************************************************************\
+
+Module: Non-deterministic object init and choice for JBMC
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include "nondet.h"
+
+#include <java_bytecode/java_types.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.
+/// \param int_type: The type of the int used to non-deterministically choose
+///   one of the switch cases.
+/// \param source_location: The location to mark the generated int with.
+/// \param symbol_table: The global symbol table.
+/// \param instructions [out]: 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 int64_t min_value,
+  const int64_t max_value,
+  const std::string &name_prefix,
+  const typet &int_type,
+  const source_locationt &source_location,
+  symbol_table_baset &symbol_table,
+  code_blockt &instructions)
+{
+  PRECONDITION(min_value < max_value);
+
+  // Declare a symbol for the non deterministic integer.
+  const symbol_exprt &nondet_symbol = get_fresh_aux_symbol(
+                                        int_type,
+                                        name_prefix + "::nondet_int",
+                                        "nondet_int",
+                                        source_location,
+                                        ID_java,
+                                        symbol_table)
+                                        .symbol_expr();
+  instructions.add(code_declt(nondet_symbol));
+
+  // Assign the symbol any non deterministic integer value.
+  //   int_type name_prefix::nondet_int = NONDET(int_type)
+  instructions.add(
+    code_assignt(nondet_symbol, side_effect_expr_nondett(int_type)));
+
+  // 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))));
+
+  // 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))));
+
+  return nondet_symbol;
+}
+
+/// Pick nondeterministically between imperative actions 'switch_cases'.
+/// \param name_prefix: Name prefix for fresh symbols
+/// \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 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,
+  const typet &int_type,
+  const source_locationt &source_location,
+  symbol_table_baset &symbol_table)
+{
+  PRECONDITION(!switch_cases.empty());
+
+  if(switch_cases.size() == 1)
+    return code_blockt({switch_cases[0]});
+
+  code_switcht result_switch;
+  code_blockt result_block;
+
+  const symbol_exprt &switch_value = generate_nondet_int(
+    0,
+    switch_cases.size() - 1,
+    id2string(name_prefix),
+    int_type,
+    source_location,
+    symbol_table,
+    result_block);
+
+  result_switch.value() = switch_value;
+
+  code_blockt switch_block;
+  int64_t case_number = 0;
+  for(const auto &switch_case : switch_cases)
+  {
+    code_blockt this_block;
+    this_block.add(switch_case);
+    this_block.add(code_breakt());
+    code_switch_caset this_case;
+    this_case.case_op() = from_integer(case_number, switch_value.type());
+    this_case.code() = this_block;
+    switch_block.move(this_case);
+    ++case_number;
+  }
+
+  result_switch.body() = switch_block;
+  result_block.move(result_switch);
+  return result_block;
+}

jbmc/src/java_bytecode/nondet.h

@@ -0,0 +1,34 @@
+/*******************************************************************\
+
+ Module: Non-deterministic object init and choice for JBMC
+
+ 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>
+
+symbol_exprt generate_nondet_int(
+  int64_t min_value,
+  int64_t max_value,
+  const std::string &name_prefix,
+  const typet &int_type,
+  const source_locationt &source_location,
+  symbol_table_baset &symbol_table,
+  code_blockt &instructions);
+
+typedef std::vector<codet> alternate_casest;
+
+code_blockt generate_nondet_switch(
+  const irep_idt &name_prefix,
+  const alternate_casest &switch_cases,
+  const typet &int_type,
+  const source_locationt &source_location,
+  symbol_table_baset &symbol_table);
+
+#endif // CPROVER_JAVA_BYTECODE_NONDET_H