Merge pull request #1740 from smowton/smowton/feature/adjust_float_expressions_per_function

JBMC: adjust float expressions per function

Author: smowton

src/analyses/goto_check.cpp

@@ -1753,10 +1753,11 @@ void goto_checkt::goto_check(
 void goto_check(
   const namespacet &ns,
   const optionst &options,
+  const irep_idt &mode,
   goto_functionst::goto_functiont &goto_function)
 {
   goto_checkt goto_check(ns, options);
-  goto_check.goto_check(goto_function, irep_idt());
+  goto_check.goto_check(goto_function, mode);
 }
 
 void goto_check(

src/analyses/goto_check.h

@@ -26,6 +26,7 @@ void goto_check(
 void goto_check(
   const namespacet &ns,
   const optionst &options,
+  const irep_idt &mode,
   goto_functionst::goto_functiont &goto_function);
 
 void goto_check(

src/goto-programs/convert_nondet.cpp

@@ -130,6 +130,20 @@ void convert_nondet(
   }
 }
 
+void convert_nondet(
+  goto_model_functiont &function,
+  message_handlert &message_handler,
+  const object_factory_parameterst &object_factory_parameters)
+{
+  convert_nondet(
+    function.get_goto_function().body,
+    function.get_symbol_table(),
+    message_handler,
+    object_factory_parameters);
+
+  function.compute_location_numbers();
+}
+
 void convert_nondet(
   goto_functionst &goto_functions,
   symbol_tablet &symbol_table,

src/goto-programs/convert_nondet.h

@@ -17,6 +17,7 @@ Author: Reuben Thomas, [email protected]
 class goto_functionst;
 class symbol_tablet;
 class goto_modelt;
+class goto_model_functiont;
 class message_handlert;
 struct object_factory_parameterst;
 
@@ -38,4 +39,15 @@ void convert_nondet(
   message_handlert &,
   const object_factory_parameterst &object_factory_parameters);
 
+/// Replace calls to nondet library functions with an internal nondet
+/// representation.
+/// \param function: goto program to modify
+/// \param message_handler: For error logging.
+/// \param object_factory_parameters: Parameters for the generation of nondet
+///   objects.
+void convert_nondet(
+  goto_model_functiont &function,
+  message_handlert &message_handler,
+  const object_factory_parameterst &object_factory_parameters);
+
 #endif

src/goto-programs/lazy_goto_model.h

@@ -64,8 +64,9 @@ class lazy_goto_modelt : public can_produce_functiont
     message_handlert &message_handler)
   {
     return lazy_goto_modelt(
-      [&handler] (goto_model_functiont &fun, const can_produce_functiont &cpf) { // NOLINT(*)
-        handler.process_goto_function(fun, cpf);
+      [&handler, &options]
+      (goto_model_functiont &fun, const can_produce_functiont &cpf) { // NOLINT(*)
+        handler.process_goto_function(fun, cpf, options);
       },
       [&handler, &options] (goto_modelt &goto_model) -> bool { // NOLINT(*)
         return handler.process_goto_functions(goto_model, options);

src/goto-programs/replace_java_nondet.cpp

@@ -235,6 +235,16 @@ static void replace_java_nondet(goto_programt &goto_program)
   }
 }
 
+void replace_java_nondet(goto_model_functiont &function)
+{
+  goto_programt &program = function.get_goto_function().body;
+  replace_java_nondet(program);
+
+  function.compute_location_numbers();
+
+  remove_skip(program);
+}
+
 void replace_java_nondet(goto_functionst &goto_functions)
 {
   for(auto &goto_program : goto_functions.function_map)

src/goto-programs/replace_java_nondet.h

@@ -14,6 +14,7 @@ Author: Reuben Thomas, [email protected]
 
 class goto_modelt;
 class goto_functionst;
+class goto_model_functiont;
 
 /// Replace calls to nondet library functions with an internal nondet
 /// representation.
@@ -22,4 +23,9 @@ void replace_java_nondet(goto_modelt &);
 
 void replace_java_nondet(goto_functionst &);
 
+/// Replace calls to nondet library functions with an internal nondet
+/// representation in a single function.
+/// \param function: The goto program to modify.
+void replace_java_nondet(goto_model_functiont &function);
+
 #endif

src/jbmc/jbmc_parse_options.cpp

@@ -643,9 +643,11 @@ int jbmc_parse_optionst::get_goto_program(
 
 void jbmc_parse_optionst::process_goto_function(
   goto_model_functiont &function,
-  const can_produce_functiont &available_functions)
+  const can_produce_functiont &available_functions,
+  const optionst &options)
 {
   symbol_tablet &symbol_table = function.get_symbol_table();
+  namespacet ns(symbol_table);
   goto_functionst::goto_functiont &goto_function = function.get_goto_function();
   try
   {
@@ -664,6 +666,36 @@ void jbmc_parse_optionst::process_goto_function(
       };
 
     remove_returns(function, function_is_stub);
+
+    replace_java_nondet(function);
+
+    // Similar removal of java nondet statements:
+    // TODO Should really get this from java_bytecode_language somehow, but we
+    // don't have an instance of that here.
+    object_factory_parameterst factory_params;
+    factory_params.max_nondet_array_length=
+      cmdline.isset("java-max-input-array-length")
+        ? std::stoul(cmdline.get_value("java-max-input-array-length"))
+        : MAX_NONDET_ARRAY_LENGTH_DEFAULT;
+    factory_params.max_nondet_string_length=
+      cmdline.isset("string-max-input-length")
+        ? std::stoul(cmdline.get_value("string-max-input-length"))
+        : MAX_NONDET_STRING_LENGTH;
+    factory_params.max_nondet_tree_depth=
+      cmdline.isset("java-max-input-tree-depth")
+        ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
+        : MAX_NONDET_TREE_DEPTH;
+
+    convert_nondet(
+      function,
+      get_message_handler(),
+      factory_params);
+
+    // add generic checks
+    goto_check(ns, options, ID_java, function.get_goto_function());
+
+    // checks don't know about adjusted float expressions
+    adjust_float_expressions(goto_function, ns);
   }
 
   catch(const char *e)
@@ -701,37 +733,6 @@ bool jbmc_parse_optionst::process_goto_functions(
     // instrument library preconditions
     instrument_preconditions(goto_model);
 
-    // Similar removal of java nondet statements:
-    // TODO Should really get this from java_bytecode_language somehow, but we
-    // don't have an instance of that here.
-    object_factory_parameterst factory_params;
-    factory_params.max_nondet_array_length=
-      cmdline.isset("java-max-input-array-length")
-        ? std::stoul(cmdline.get_value("java-max-input-array-length"))
-        : MAX_NONDET_ARRAY_LENGTH_DEFAULT;
-    factory_params.max_nondet_string_length=
-      cmdline.isset("string-max-input-length")
-        ? std::stoul(cmdline.get_value("string-max-input-length"))
-        : MAX_NONDET_STRING_LENGTH;
-    factory_params.max_nondet_tree_depth=
-      cmdline.isset("java-max-input-tree-depth")
-        ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
-        : MAX_NONDET_TREE_DEPTH;
-
-    replace_java_nondet(goto_model);
-
-    convert_nondet(
-      goto_model,
-      get_message_handler(),
-      factory_params);
-
-    // add generic checks
-    status() << "Generic Property Instrumentation" << eom;
-    goto_check(options, goto_model);
-
-    // checks don't know about adjusted float expressions
-    adjust_float_expressions(goto_model);
-
     // ignore default/user-specified initialization
     // of variables with static lifetime
     if(cmdline.isset("nondet-static"))

src/jbmc/jbmc_parse_options.h

@@ -86,7 +86,8 @@ class jbmc_parse_optionst:
 
   void process_goto_function(
     goto_model_functiont &function,
-    const can_produce_functiont &);
+    const can_produce_functiont &,
+    const optionst &);
   bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
 
 protected: