Merge pull request #5087 from xbauch/feature/better-harness

Improve harness generated code readability

Author: hannes-steffenhagen-diffblue

regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc

@@ -3,6 +3,6 @@ test.c
 --harness-type call-function --function is_prefix_of --treat-pointer-as-array string --treat-pointer-as-array prefix --associated-array-size string:string_size --associated-array-size prefix:prefix_size --max-array-size 5
 ^EXIT=10$
 ^SIGNAL=0$
-\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE
+\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE
 VERIFICATION FAILED
 --

regression/goto-harness/pointer-to-array-function-parameters/test.desc

@@ -1,8 +1,8 @@
 CORE
 test.c
 --harness-type call-function --function test --treat-pointer-as-array arr
-\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS
-\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)10\]: FAILURE
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)10\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
 --

src/goto-harness/function_call_harness_generator.cpp

@@ -10,15 +10,15 @@ Author: Diffblue Ltd.
 
 #include <util/allocate_objects.h>
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/exception_utils.h>
-#include <util/prefix.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
 #include <util/string_utils.h>
 #include <util/ui_message.h>
 
-#include <goto-programs/goto_convert.h>
+#include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_model.h>
 
 #include <algorithm>
@@ -54,6 +54,8 @@ struct function_call_harness_generatort::implt
   std::map<irep_idt, irep_idt> function_argument_to_associated_array_size;
   std::map<irep_idt, irep_idt> function_parameter_to_associated_array_size;
 
+  std::set<symbol_exprt> global_pointers;
+
   /// \see goto_harness_generatort::generate
   void generate(goto_modelt &goto_model, const irep_idt &harness_function_name);
   /// Iterate over the symbol table and generate initialisation code for
@@ -195,6 +197,11 @@ void function_call_harness_generatort::implt::generate(
 
   generate_nondet_globals(function_body);
   call_function(arguments, function_body);
+  for(const auto &global_pointer : global_pointers)
+  {
+    function_body.add(code_function_callt{
+      recursive_initialization->get_free_function(), {global_pointer}});
+  }
   add_harness_function_to_goto_model(std::move(function_body));
 }
 
@@ -213,10 +220,7 @@ void function_call_harness_generatort::implt::generate_nondet_globals(
     for(const auto &symbol_table_entry : *symbol_table)
     {
       const auto &symbol = symbol_table_entry.second;
-      if(
-        symbol.is_static_lifetime && symbol.is_lvalue &&
-        symbol.type.id() != ID_code &&
-        !has_prefix(id2string(symbol.name), CPROVER_PREFIX))
+      if(recursive_initialization->is_initialization_allowed(symbol))
       {
         globals.push_back(symbol.symbol_expr());
       }
@@ -232,7 +236,10 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for(
   code_blockt &block,
   const exprt &lhs)
 {
-  recursive_initialization->initialize(lhs, 0, {}, block);
+  recursive_initialization->initialize(
+    lhs, from_integer(0, signed_int_type()), block);
+  if(lhs.type().id() == ID_pointer)
+    global_pointers.insert(to_symbol_expr(lhs));
 }
 
 void function_call_harness_generatort::validate_options(
@@ -300,14 +307,7 @@ void function_call_harness_generatort::implt::
     symbol_table->lookup_ref(harness_function_name);
   goto_functions->function_map[harness_function_name].type =
     to_code_type(generated_harness.type);
-  auto &body = goto_functions->function_map[harness_function_name].body;
-  goto_convert(
-    static_cast<const codet &>(generated_harness.value),
-    *symbol_table,
-    body,
-    *message_handler,
-    function_to_call.mode);
-  body.add(goto_programt::make_end_function());
+  goto_convert(*symbol_table, *goto_functions, *message_handler);
 }
 
 code_function_callt::argumentst
@@ -377,6 +377,8 @@ void function_call_harness_generatort::implt::call_function(
   for(auto const &argument : arguments)
   {
     generate_initialisation_code_for(function_body, argument);
+    if(argument.type().id() == ID_pointer)
+      global_pointers.insert(to_symbol_expr(argument));
   }
   code_function_callt function_call{function_to_call.symbol_expr(),
                                     std::move(arguments)};

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -11,12 +11,14 @@ Author: Daniel Poetzl
 #include "memory_snapshot_harness_generator.h"
 #include "memory_snapshot_harness_generator_options.h"
 
-#include <goto-programs/goto_convert.h>
+#include <goto-programs/goto_convert_functions.h>
 
 #include <json/json_parser.h>
 
 #include <json-symtab-language/json_symbol_table.h>
 
+#include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/exception_utils.h>
 #include <util/fresh_symbol.h>
 #include <util/message.h>
@@ -231,7 +233,7 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
   for(auto pair : snapshot)
   {
     const auto name = id2string(pair.first);
-    if(name.find(CPROVER_PREFIX) != 0)
+    if(!has_prefix(name, CPROVER_PREFIX))
       ordered_snapshot_symbols.push_back(pair);
   }
 
@@ -249,7 +251,22 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
                pointer_depth(right.second.symbol_expr().type());
     });
 
-  code_blockt code;
+  code_blockt code{};
+
+  // add initialization for existing globals
+  for(const auto &pair : goto_model.symbol_table)
+  {
+    const auto &global_symbol = pair.second;
+    if(
+      global_symbol.is_static_lifetime && global_symbol.is_lvalue &&
+      global_symbol.type.id() != ID_code)
+    {
+      auto symeexr = global_symbol.symbol_expr();
+      if(symeexr.type() == global_symbol.value.type())
+        code.add(code_assignt{symeexr, global_symbol.value});
+    }
+  }
+
   for(const auto &pair : ordered_snapshot_symbols)
   {
     const symbolt &snapshot_symbol = pair.second;
@@ -275,7 +292,9 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
     else
     {
       recursive_initialization.initialize(
-        fresh_or_snapshot_symbol.symbol_expr(), 0, {}, code);
+        fresh_or_snapshot_symbol.symbol_expr(),
+        from_integer(0, size_type()),
+        code);
     }
   }
   return code;
@@ -316,12 +335,7 @@ void memory_snapshot_harness_generatort::
   harness_function.type = to_code_type(function.type);
 
   goto_convert(
-    to_code_block(to_code(function.value)),
-    goto_model.symbol_table,
-    harness_function.body,
-    message_handler,
-    function.mode);
-
+    goto_model.symbol_table, goto_model.goto_functions, message_handler);
   harness_function.body.add(goto_programt::make_end_function());
 }
 
@@ -379,6 +393,7 @@ void memory_snapshot_harness_generatort::generate(
 
   const symbolt *called_function_symbol =
     symbol_table.lookup(entry_location.function_name);
+  recursive_initialization_config.mode = called_function_symbol->mode;
 
   // introduce a symbol for a Boolean variable to indicate the point at which
   // the function initialisation is completed