Merge pull request #2872 from mgudemann/feature/generalize_nondet_switch

Make `generate_nondet_switch` available in CBMC

Author: tautschnig

jbmc/src/java_bytecode/Makefile

@@ -36,7 +36,6 @@ 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/java_entry_point.cpp

@@ -22,8 +22,8 @@ Author: Daniel Kroening, [email protected]
 #include "java_object_factory.h"
 #include "java_string_literals.h"
 #include "java_utils.h"
-#include "nondet.h"
 #include <util/fresh_symbol.h>
+#include <util/nondet.h>
 
 #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"
 
@@ -402,6 +402,7 @@ exprt::operandst java_build_arguments(
           id2string(function.name) + "_" + std::to_string(param_number),
           cases,
           java_int_type(),
+          ID_java,
           function.location,
           symbol_table));
     }

src/util/Makefile

@@ -45,6 +45,7 @@ SRC = arith_tools.cpp \
       message.cpp \
       mp_arith.cpp \
       namespace.cpp \
+      nondet.cpp \
       options.cpp \
       parse_options.cpp \
       parser.cpp \

jbmc/src/java_bytecode/nondet.cpp renamed to src/util/nondet.cpp

@@ -1,14 +1,13 @@
 /*******************************************************************\
 
-Module: Non-deterministic object init and choice for JBMC
+Module: Non-deterministic object init and choice for CBMC
 
  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>
@@ -23,7 +22,8 @@ Module: Non-deterministic object init and choice for JBMC
 /// ```
 /// \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 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 source_location: The location to mark the generated int with.
@@ -37,21 +37,18 @@ symbol_exprt generate_nondet_int(
   const int64_t 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)
 {
   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",
-                                        source_location,
-                                        ID_java,
-                                        symbol_table)
-                                        .symbol_expr();
+  const symbol_exprt &nondet_symbol =
+    get_fresh_aux_symbol(
+      int_type, name_prefix, "nondet_int", source_location, mode, symbol_table)
+      .symbol_expr();
   instructions.add(code_declt(nondet_symbol));
 
   // Assign the symbol any non deterministic integer value.
@@ -77,7 +74,7 @@ symbol_exprt generate_nondet_int(
 }
 
 /// Pick nondeterministically between imperative actions 'switch_cases'.
-/// \param name_prefix: Name prefix for fresh symbols
+/// \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.
@@ -89,6 +86,7 @@ code_blockt generate_nondet_switch(
   const irep_idt &name_prefix,
   const alternate_casest &switch_cases,
   const typet &int_type,
+  const irep_idt &mode,
   const source_locationt &source_location,
   symbol_table_baset &symbol_table)
 {
@@ -105,14 +103,15 @@ code_blockt generate_nondet_switch(
     switch_cases.size() - 1,
     id2string(name_prefix),
     int_type,
+    mode,
     source_location,
     symbol_table,
     result_block);
 
   result_switch.value() = switch_value;
 
   code_blockt switch_block;
-  int64_t case_number = 0;
+  size_t case_number = 0;
   for(const auto &switch_case : switch_cases)
   {
     code_blockt this_block;

jbmc/src/java_bytecode/nondet.h renamed to src/util/nondet.h

@@ -18,6 +18,7 @@ symbol_exprt generate_nondet_int(
   int64_t 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);
@@ -28,6 +29,7 @@ code_blockt generate_nondet_switch(
   const irep_idt &name_prefix,
   const alternate_casest &switch_cases,
   const typet &int_type,
+  const irep_idt &mode,
   const source_locationt &source_location,
   symbol_table_baset &symbol_table);