Merge pull request #5383 from hannes-steffenhagen-diffblue/fix/missing-decl-for-malloc-symbols

Make filter_goto_model remove file local symbols

Author: hannes-steffenhagen-diffblue

regression/CMakeLists.txt

@@ -53,6 +53,7 @@ add_subdirectory(statement-list)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(goto-harness)
+add_subdirectory(goto-harness-multi-file-project)
 add_subdirectory(goto-cc-file-local)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)

regression/goto-harness-multi-file-project/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_test_pl_tests(
+  "${CMAKE_CURRENT_LIST_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-harness> $<TARGET_FILE:cbmc>")

regression/goto-harness-multi-file-project/Makefile

@@ -0,0 +1,10 @@
+default: test
+
+test:
+	@../test.pl -e -p -c "../chain.sh \
+		../../../src/goto-cc/goto-cc \
+	  ../../../src/goto-harness/goto-harness \
+		../../../src/cbmc/cbmc"
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/goto-harness-multi-file-project/chain.sh

@@ -0,0 +1,28 @@
+#!/bin/bash
+
+set -x
+set -e
+goto_cc="$1"
+goto_harness="$2"
+cbmc="$3"
+goto_harness_args="${@:4:$#-4}"
+
+source_dir="$(pwd)"
+target_dir="$(mktemp -d)"
+
+# Compiling
+for file in "$source_dir"/*.c; do
+  file_name="$(basename "$file")"
+  "$goto_cc" -c "$file" -o "$target_dir"/"${file_name%.c}.o"
+done
+
+# Linking
+
+main_exe="$target_dir/main.gb"
+"$goto_cc" "$target_dir"/*.o -o "$main_exe"
+
+harness_out_file="$target_dir/harness.c"
+"$goto_harness" "$main_exe" "$harness_out_file" --harness-function-name harness $goto_harness_args
+cat "$harness_out_file"
+"$cbmc" "$main_exe" "$harness_out_file" --function harness
+

regression/goto-harness-multi-file-project/static_functions/main.c

@@ -0,0 +1,10 @@
+#include "service.h"
+
+// this isn't testing any interesting harness
+// properties so we just have a main function
+// with no parameters
+int main(void)
+{
+  service_t *service = get_default_service();
+  service_serve(service);
+}

regression/goto-harness-multi-file-project/static_functions/service.c

@@ -0,0 +1,31 @@
+#include "service.h"
+#include <assert.h>
+
+// contents of the struct
+// (mostly just a vtable)
+
+struct service
+{
+  void (*serve)(void);
+};
+
+void service_serve(service_t *service)
+{
+  service->serve();
+}
+
+static void default_serve(void)
+{
+  assert(0 && "default serve should fail so we can see it is being called");
+}
+
+// this static initialisation should not show up in output
+// in fact, there is a bit of a bug with dump-c where this
+// initialisation would appear but the default_serve function
+// would be omitted in certain cases.
+static service_t default_service = {.serve = default_serve};
+
+service_t *get_default_service(void)
+{
+  return &default_service;
+}

regression/goto-harness-multi-file-project/static_functions/service.h

@@ -0,0 +1,13 @@
+#include <stddef.h>
+
+// common pattern:
+// Some sort of interface defined over "abstract" type with hidden
+// implementation details, effectively C style OOP
+//
+// This is a straw example of course, but very reminiscent of patterns that
+// occur in real programs
+
+typedef struct service service_t;
+
+service_t *get_default_service(void);
+void service_serve(service_t *service);

regression/goto-harness-multi-file-project/static_functions/test.desc

@@ -0,0 +1,12 @@
+CORE
+dummy.c
+--function main --harness-type call-function
+\[default_serve\.assertion\.1\] line \d+ assertion 0 && \"default serve should fail so we can see it is being called\": FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+static void default_serve
+--
+When running the harness we should run into the assertion failure from the
+static default_serve function, but the harness C code should not contain this
+or any other static functions or variables.

src/goto-harness/goto_harness_parse_options.cpp

@@ -51,12 +51,35 @@ static void filter_goto_model(
   goto_modelt &goto_model_with_harness,
   const std::unordered_set<irep_idt> &goto_model_without_harness_symbols)
 {
-  for(auto &symbol : goto_model_with_harness.get_symbol_table())
+  for(auto const &symbol_id : goto_model_without_harness_symbols)
   {
-    if(
-      goto_model_without_harness_symbols.count(symbol.first) == 1 &&
-      symbol.second.is_function())
-      goto_model_with_harness.unload(symbol.first);
+    auto &symbol =
+      goto_model_with_harness.symbol_table.get_writeable_ref(symbol_id);
+    if(symbol.is_function())
+    {
+      // We don’t want bodies of functions that already existed in the
+      // symbol table (i.e. not generated by us)
+      goto_model_with_harness.unload(symbol_id);
+      if(symbol.is_file_local)
+      {
+        goto_model_with_harness.symbol_table.remove(symbol_id);
+      }
+    }
+    else if(!symbol.is_type && symbol.is_file_local)
+    {
+      // We don’t want file local symbols from an existing goto model
+      // except types / typedefs, which also apparently get marked
+      // file local sometimes.
+      goto_model_with_harness.symbol_table.remove(symbol_id);
+    }
+    else if(!symbol.is_type && symbol.is_static_lifetime)
+    {
+      // if it has static lifetime and is *not* a type it is a global variable
+      // We keep around other global variables in case we want to initialise
+      // them, but mark them as extern so we don't duplicate their definitions
+      symbol.value = nil_exprt{};
+      symbol.is_extern = true;
+    }
   }
 }