Move replace_java_nondet to java_bytecode

Author: peterschrammel

src/goto-programs/Makefile

@@ -50,7 +50,6 @@ SRC = basic_blocks.cpp \
       remove_unused_functions.cpp \
       remove_vector.cpp \
       remove_virtual_functions.cpp \
-      replace_java_nondet.cpp \
       generate_function_bodies.cpp \
       resolve_inherited_component.cpp \
       safety_checker.cpp \

src/java_bytecode/Makefile

@@ -31,6 +31,7 @@ SRC = bytecode_info.cpp \
       java_types.cpp \
       java_utils.cpp \
       mz_zip_archive.cpp \
+      replace_java_nondet.cpp \
       remove_exceptions.cpp \
       remove_instanceof.cpp \
       select_pointer_type.cpp \

src/goto-programs/replace_java_nondet.cpp renamed to src/java_bytecode/replace_java_nondet.cpp

@@ -9,38 +9,51 @@ Author: Reuben Thomas, [email protected]
 /// \file
 /// Replace Java Nondet expressions
 
-#include "goto-programs/replace_java_nondet.h"
-#include "goto-programs/goto_convert.h"
-#include "goto-programs/goto_model.h"
-#include "goto-programs/remove_skip.h"
-
-#include "util/irep_ids.h"
+#include "replace_java_nondet.h"
 
 #include <algorithm>
 #include <regex>
 
+#include <goto-programs/goto_convert.h>
+#include <goto-programs/goto_model.h>
+#include <goto-programs/remove_skip.h>
+
+#include <util/irep_ids.h>
+
 /// Holds information about any discovered nondet methods, with extreme type-
 /// safety.
 class nondet_instruction_infot final
 {
 public:
-  enum class is_nondett:bool { FALSE, TRUE };
-  enum class is_nullablet:bool { FALSE, TRUE };
+  enum class is_nondett : bool
+  {
+    FALSE,
+    TRUE
+  };
+  enum class is_nullablet : bool
+  {
+    FALSE,
+    TRUE
+  };
 
-  nondet_instruction_infot():
-    is_nondet(is_nondett::FALSE),
-    is_nullable(is_nullablet::FALSE)
+  nondet_instruction_infot()
+    : is_nondet(is_nondett::FALSE), is_nullable(is_nullablet::FALSE)
   {
   }
 
-  explicit nondet_instruction_infot(is_nullablet is_nullable):
-    is_nondet(is_nondett::TRUE),
-    is_nullable(is_nullable)
+  explicit nondet_instruction_infot(is_nullablet is_nullable)
+    : is_nondet(is_nondett::TRUE), is_nullable(is_nullable)
   {
   }
 
-  is_nondett get_instruction_type() const { return is_nondet; }
-  is_nullablet get_nullable_type() const { return is_nullable; }
+  is_nondett get_instruction_type() const
+  {
+    return is_nondet;
+  }
+  is_nullablet get_nullable_type() const
+  {
+    return is_nullable;
+  }
 
 private:
   is_nondett is_nondet;
@@ -52,11 +65,11 @@ class nondet_instruction_infot final
 /// \return A structure detailing whether the function call appears to be one of
 ///   our nondet library methods, and if so, whether or not it allows null
 ///   results.
-static nondet_instruction_infot is_nondet_returning_object(
-  const code_function_callt &function_call)
+static nondet_instruction_infot
+is_nondet_returning_object(const code_function_callt &function_call)
 {
-  const auto &function_symbol=to_symbol_expr(function_call.function());
-  const auto function_name=id2string(function_symbol.get_identifier());
+  const auto &function_symbol = to_symbol_expr(function_call.function());
+  const auto function_name = id2string(function_symbol.get_identifier());
   const std::regex reg(
     R"(.*org\.cprover\.CProver\.nondet)"
     R"((?:Boolean|Byte|Char|Short|Int|Long|Float|Double|With(out)?Null.*))");
@@ -74,51 +87,51 @@ static nondet_instruction_infot is_nondet_returning_object(
 /// recognised nondet library methods, and return some information about it.
 /// \param instr: A goto-program instruction to check.
 /// \return A structure detailing the properties of the nondet method.
-static nondet_instruction_infot get_nondet_instruction_info(
-  const goto_programt::const_targett &instr)
+static nondet_instruction_infot
+get_nondet_instruction_info(const goto_programt::const_targett &instr)
 {
-  if(!(instr->is_function_call() && instr->code.id()==ID_code))
+  if(!(instr->is_function_call() && instr->code.id() == ID_code))
   {
     return nondet_instruction_infot();
   }
-  const auto &code=to_code(instr->code);
-  if(code.get_statement()!=ID_function_call)
+  const auto &code = to_code(instr->code);
+  if(code.get_statement() != ID_function_call)
   {
     return nondet_instruction_infot();
   }
-  const auto &function_call=to_code_function_call(code);
+  const auto &function_call = to_code_function_call(code);
   return is_nondet_returning_object(function_call);
 }
 
 /// Return whether the expression is a symbol with the specified identifier.
 /// \param expr: The expression which may be a symbol.
 /// \param identifier: Some identifier.
 /// \return True if the expression is a symbol with the specified identifier.
-static bool is_symbol_with_id(const exprt& expr, const irep_idt& identifier)
+static bool is_symbol_with_id(const exprt &expr, const irep_idt &identifier)
 {
-  return expr.id()==ID_symbol &&
-         to_symbol_expr(expr).get_identifier()==identifier;
+  return expr.id() == ID_symbol &&
+         to_symbol_expr(expr).get_identifier() == identifier;
 }
 
 /// Return whether the expression is a typecast with the specified identifier.
 /// \param expr: The expression which may be a typecast.
 /// \param identifier: Some identifier.
 /// \return True if the expression is a typecast with one operand, and the
 ///   typecast's identifier matches the specified identifier.
-static bool is_typecast_with_id(const exprt& expr, const irep_idt& identifier)
+static bool is_typecast_with_id(const exprt &expr, const irep_idt &identifier)
 {
-  if(!(expr.id()==ID_typecast && expr.operands().size()==1))
+  if(!(expr.id() == ID_typecast && expr.operands().size() == 1))
   {
     return false;
   }
-  const auto &typecast=to_typecast_expr(expr);
-  if(!(typecast.op().id()==ID_symbol && !typecast.op().has_operands()))
+  const auto &typecast = to_typecast_expr(expr);
+  if(!(typecast.op().id() == ID_symbol && !typecast.op().has_operands()))
   {
     return false;
   }
-  const auto &op_symbol=to_symbol_expr(typecast.op());
+  const auto &op_symbol = to_symbol_expr(typecast.op());
   // Return whether the typecast has the expected operand
-  return op_symbol.get_identifier()==identifier;
+  return op_symbol.get_identifier() == identifier;
 }
 
 /// Return whether the instruction is an assignment, and the rhs is a symbol or
@@ -136,26 +149,14 @@ static bool is_assignment_from(
   {
     return false;
   }
-  const auto &rhs=to_code_assign(instr.code).rhs();
+  const auto &rhs = to_code_assign(instr.code).rhs();
   return is_symbol_with_id(rhs, identifier) ||
          is_typecast_with_id(rhs, identifier);
 }
 
 /// Given an iterator into a list of instructions, modify the list to replace
 /// 'nondet' library functions with CBMC-native nondet expressions, and return
-/// an iterator to the next instruction to check. It's important to note that
-/// this method also deals with the fact that in the GOTO program it assigns
-/// function return values to temporary variables, performs validation and then
-/// assigns the value into the actual variable.
-///
-/// Example:
-///
-///   return_tmp0=org.cprover.CProver.nondetWithoutNull:()Ljava/lang/Object;();
-///   ... Various validations of type and value here.
-///   obj = (<type-of-obj>)return_tmp0;
-///
-/// We're going to replace all of these lines with
-///   return_tmp0 = NONDET(<type-of-obj>)
+/// an iterator to the next instruction to check.
 /// \param goto_program: The goto program to modify.
 /// \param target: A single step of the goto program which may be erased and
 ///   replaced.
@@ -165,94 +166,67 @@ static goto_programt::targett check_and_replace_target(
   const goto_programt::targett &target)
 {
   // Check whether this is a nondet library method, and return if not
-  const auto instr_info=get_nondet_instruction_info(target);
-  const auto next_instr=std::next(target);
-  if(instr_info.get_instruction_type()==
-     nondet_instruction_infot::is_nondett::FALSE)
+  const auto instr_info = get_nondet_instruction_info(target);
+  const auto next_instr = std::next(target);
+  if(
+    instr_info.get_instruction_type() ==
+    nondet_instruction_infot::is_nondett::FALSE)
   {
     return next_instr;
   }
 
-  // If we haven't removed returns yet, our function call will have a variable
-  // on its left hand side.
-  const bool remove_returns_not_run =
-    to_code_function_call(target->code).lhs().is_not_nil();
-
-  irep_idt return_identifier;
-  if(remove_returns_not_run)
+  // Look at the next instruction, ensure that it is an assignment
+  assert(next_instr->is_assign());
+  // Get the name of the LHS of the assignment
+  const auto &next_instr_assign_lhs = to_code_assign(next_instr->code).lhs();
+  if(
+    !(next_instr_assign_lhs.id() == ID_symbol &&
+      !next_instr_assign_lhs.has_operands()))
   {
-    return_identifier =
-      to_symbol_expr(to_code_function_call(target->code).lhs())
-        .get_identifier();
-  }
-  else
-  {
-    // If not, we need to look at the next line instead.
-    DATA_INVARIANT(
-      next_instr->is_assign(),
-      "the code_function_callt for a nondet-returning library function should "
-      "either have a variable for the return value in its lhs() or the next "
-      "instruction should be an assignment of the return value to a temporary "
-      "variable");
-    const exprt &return_value_assignment =
-      to_code_assign(next_instr->code).lhs();
-
-    // If the assignment is null, return.
-    if(
-      !(return_value_assignment.id() == ID_symbol &&
-        !return_value_assignment.has_operands()))
-    {
-      return next_instr;
-    }
-
-    // Otherwise it's the temporary variable.
-    return_identifier =
-      to_symbol_expr(return_value_assignment).get_identifier();
+    return next_instr;
   }
+  const auto return_identifier =
+    to_symbol_expr(next_instr_assign_lhs).get_identifier();
+
+  auto &instructions = goto_program.instructions;
+  const auto end = instructions.end();
 
-  // Look for the assignment of the temporary return variable into our target
-  // variable.
-  const auto end = goto_program.instructions.end();
-  auto assignment_instruction = std::find_if(
+  // Look for an instruction where this name is on the RHS of an assignment
+  const auto matching_assignment = std::find_if(
     next_instr,
     end,
-    [&return_identifier](const goto_programt::instructiont &instr) {
+    [&return_identifier](
+      const goto_programt::instructiont &instr) { // NOLINT (*)
       return is_assignment_from(instr, return_identifier);
     });
 
-  INVARIANT(
-    assignment_instruction != end,
-    "failed to find assignment of the temporary return variable into our "
-    "target variable");
+  assert(matching_assignment != end);
 
   // Assume that the LHS of *this* assignment is the actual nondet variable
-  const auto &code_assign = to_code_assign(assignment_instruction->code);
-  const auto nondet_var=code_assign.lhs();
-  const auto source_loc=target->source_location;
+  const auto &code_assign = to_code_assign(matching_assignment->code);
+  const auto nondet_var = code_assign.lhs();
+  const auto source_loc = target->source_location;
 
   // Erase from the nondet function call to the assignment
-  const auto after_matching_assignment = std::next(assignment_instruction);
-  INVARIANT(
-    after_matching_assignment != end,
-    "goto_program missing END_FUNCTION instruction");
+  const auto after_matching_assignment = std::next(matching_assignment);
+  assert(after_matching_assignment != end);
 
   std::for_each(
     target,
     after_matching_assignment,
-    [](goto_programt::instructiont &instr)
-    {
+    [](goto_programt::instructiont &instr) { // NOLINT (*)
       instr.make_skip();
     });
 
-  const auto inserted=goto_program.insert_before(after_matching_assignment);
+  const auto inserted = goto_program.insert_before(after_matching_assignment);
   inserted->make_assignment();
   side_effect_expr_nondett inserted_expr(nondet_var.type());
   inserted_expr.set_nullable(
-    instr_info.get_nullable_type()==
+    instr_info.get_nullable_type() ==
     nondet_instruction_infot::is_nullablet::TRUE);
-  inserted->code=code_assignt(nondet_var, inserted_expr);
-  inserted->code.add_source_location()=source_loc;
-  inserted->source_location=source_loc;
+  inserted->code = code_assignt(nondet_var, inserted_expr);
+  inserted->code.add_source_location() = source_loc;
+  inserted->source_location = source_loc;
 
   goto_program.update();
 
@@ -265,13 +239,12 @@ static goto_programt::targett check_and_replace_target(
 /// \param goto_program: The goto program to modify.
 static void replace_java_nondet(goto_programt &goto_program)
 {
-  for(auto instruction_iterator=goto_program.instructions.begin(),
-        end=goto_program.instructions.end();
-      instruction_iterator!=end;)
+  for(auto instruction_iterator = goto_program.instructions.begin(),
+           end = goto_program.instructions.end();
+      instruction_iterator != end;)
   {
-    instruction_iterator=check_and_replace_target(
-      goto_program,
-      instruction_iterator);
+    instruction_iterator =
+      check_and_replace_target(goto_program, instruction_iterator);
   }
 }
 

src/goto-programs/replace_java_nondet.h renamed to src/java_bytecode/replace_java_nondet.h

@@ -9,8 +9,8 @@ Author: Reuben Thomas, [email protected]
 /// \file
 /// Replace Java Nondet expressions
 
-#ifndef CPROVER_GOTO_PROGRAMS_REPLACE_JAVA_NONDET_H
-#define CPROVER_GOTO_PROGRAMS_REPLACE_JAVA_NONDET_H
+#ifndef CPROVER_JAVA_BYTECODE_REPLACE_JAVA_NONDET_H
+#define CPROVER_JAVA_BYTECODE_REPLACE_JAVA_NONDET_H
 
 class goto_modelt;
 class goto_functionst;
@@ -28,4 +28,4 @@ void replace_java_nondet(goto_functionst &);
 /// \param function: The goto program to modify.
 void replace_java_nondet(goto_model_functiont &function);
 
-#endif
+#endif // CPROVER_JAVA_BYTECODE_REPLACE_JAVA_NONDET_H

src/jbmc/jbmc_parse_options.cpp

@@ -36,7 +36,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_asm.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_skip.h>
-#include <goto-programs/replace_java_nondet.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_symbol_table.h>
@@ -56,6 +55,7 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/remove_exceptions.h>
+#include <java_bytecode/replace_java_nondet.h>
 
 #include <cbmc/version.h>