Add --strip-static flag to goto-instrument

This flag allows the user to supply a list of functions that will have
the `file_local` attribute removed.
This is aimed at users wishing to verify static (in the C sense)
functions. Using this flag ensures that those functions are visible
outside the compilation unit.

Author: karkhaz

regression/goto-cc-static/CMakeLists.txt

@@ -5,5 +5,5 @@ else()
 endif()
 
 add_test_pl_tests(
-    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> ${is_windows}"
 )

regression/goto-cc-static/chain.sh

@@ -1,21 +1,17 @@
 #!/usr/bin/env bash
 
 goto_cc=$1
-cbmc=$2
+goto_instrument=$2
 is_windows=$3
 
 to_keep=""
 if [ $# -gt 3 ]; then
-  if [ $4!='' ]; then
+  if [[ $4 != '' ]]; then
     to_keep="--keep-implementations $4"
+    strip_static="--strip-static $4"
   fi
 fi
 
-cbmc_options=""
-if [ $# -gt 4 ]; then
-  cbmc_options=${*:5:$#-5}
-fi
-
 name=${*:$#}
 name=${name%.c}
 
@@ -26,4 +22,10 @@ else
   "${goto_cc}" ${to_keep} "${name}.c" -o "${name}.gb"
 fi
 
-"${cbmc}" ${cbmc_options} "${name}.gb" ${cbmc_options}
+if [[ "$to_keep" = '' ]]; then
+  cp "${name}.gb" "${name}-mod.gb"
+else
+  ${goto_instrument} ${strip_static} "${name}.gb" "${name}-mod.gb"
+fi
+
+"${goto_instrument}" --show-symbol-table "${name}-mod.gb" "${name}-mod-2.gb"

regression/goto-cc-static/keep_static-1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-foo --show-symbol-table
+foo
 
 ^EXIT=0$
 ^SIGNAL=0$

regression/goto-cc-static/keep_static-2/test.desc

@@ -1,6 +1,5 @@
 CORE
 main.c
-main --show-symbol-table
 
 ^EXIT=0$
 ^SIGNAL=0$

regression/goto-cc-static/keep_static-3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-foo,bar --show-symbol-table
+foo,bar
 
 ^EXIT=0$
 ^SIGNAL=0$

regression/goto-cc-static/keep_static-4/main.c

@@ -0,0 +1,8 @@
+static int foo()
+{
+  return 3;
+}
+
+int main()
+{
+}

regression/goto-cc-static/keep_static-4/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+foo
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+Symbol......: foo\nPretty name.: .+\nModule......: .+\nBase name...: .+\nMode........: .+\nType........: .+\nValue.......: .+\nFlags.......: lvalue
+--
+Symbol......: foo\nPretty name.: .+\nModule......: .+\nBase name...: .+\nMode........: .+\nType........: .+\nValue.......: .+\nFlags.......: .*file_local.*
+--

src/goto-instrument/Makefile

@@ -60,6 +60,7 @@ SRC = accelerate/accelerate.cpp \
       source_lines.cpp \
       splice_call.cpp \
       stack_depth.cpp \
+      strip_static.cpp \
       thread_instrumentation.cpp \
       undefined_functions.cpp \
       uninitialized.cpp \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -232,6 +232,22 @@ int goto_instrument_parse_optionst::doit()
       }
     }
 
+    if(cmdline.isset("strip-static"))
+    {
+      std::list<std::string> funs_to_strip =
+        cmdline.get_comma_separated_values("strip-static");
+      if(funs_to_strip.empty())
+      {
+        error() << "Provide a comma-delimited list of functions to remove"
+                   " the static attribute from"
+                << eom;
+        return CPROVER_EXIT_USAGE_ERROR;
+      }
+
+      static_strippert ss(goto_model, *this);
+      ss.strip_statics_from_funs(funs_to_strip);
+    }
+
     if(cmdline.isset("show-threaded"))
     {
       namespacet ns(goto_model.symbol_table);
@@ -1668,6 +1684,7 @@ void goto_instrument_parse_optionst::help()
     " --remove-function-pointers   replace function pointers by case statement over function calls\n" // NOLINT(*)
     HELP_REMOVE_CALLS_NO_BODY
     HELP_REMOVE_CONST_FUNCTION_POINTERS
+    HELP_STRIP_STATIC
     " --add-library                add models of C library functions\n"
     " --model-argc-argv <n>        model up to <n> command line arguments\n"
     // NOLINTNEXTLINE(whitespace/line_length)

src/goto-instrument/goto_instrument_parse_options.h

@@ -33,6 +33,7 @@ Author: Daniel Kroening, [email protected]
 #include "generate_function_bodies.h"
 
 #include "count_eloc.h"
+#include "strip_static.h"
 
 // clang-format off
 #define GOTO_INSTRUMENT_OPTIONS \
@@ -83,6 +84,7 @@ Author: Daniel Kroening, [email protected]
   "(show-symbol-table)(show-points-to)(show-rw-set)" \
   "(cav11)" \
   OPT_TIMESTAMP \
+  OPT_STRIP_STATIC \
   "(show-natural-loops)(accelerate)(havoc-loops)" \
   "(error-label):(string-abstraction)" \
   "(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \

src/goto-instrument/strip_static.cpp

@@ -0,0 +1,36 @@
+/*******************************************************************\
+
+Module: Strip static
+
+Author: Kareem Khazem <[email protected]>
+
+\*******************************************************************/
+
+#include "strip_static.h"
+
+bool static_strippert::strip_statics_from_funs(
+  const std::list<std::string> &funs)
+{
+  bool fail = false;
+
+  for(const auto fun : funs)
+  {
+    if(!model.symbol_table.has_symbol(fun))
+    {
+      log.error() << "Could not find symbol '" << fun << "' to remove static"
+                  << log.eom;
+      fail = true;
+      continue;
+    }
+    symbolt &sym = model.symbol_table.get_writeable_ref(fun);
+    if(!sym.is_file_local)
+    {
+      log.warning() << "Not removing static attribute from symbol '" << fun
+                    << "': symbol is already externally visible" << log.eom;
+      continue;
+    }
+    sym.is_file_local = false;
+  }
+
+  return fail;
+}

src/goto-instrument/strip_static.h

@@ -0,0 +1,37 @@
+/// \file strip_static.h
+/// \brief Remove static attribute from functions
+/// \author Kareem Khazem <[email protected]>
+
+#ifndef CPROVER_GOTO_INSTRUMENT_STRIP_STATIC_H
+#define CPROVER_GOTO_INSTRUMENT_STRIP_STATIC_H
+
+#include <goto-programs/goto_model.h>
+#include <util/message.h>
+
+#include <forward_list>
+#include <string>
+
+/// \brief Remove static attribute from functions
+class static_strippert
+{
+public:
+  explicit static_strippert(goto_modelt &goto_model, messaget &log)
+    : model(goto_model), log(log)
+  {
+  }
+
+  /// \brief Removes the static attribute from functions
+  ///
+  /// \return `true` on failure, `false` otherwise
+  bool strip_statics_from_funs(const std::list<std::string> &);
+
+protected:
+  goto_modelt &model;
+  messaget &log;
+};
+
+#define OPT_STRIP_STATIC "(strip-static):"
+#define HELP_STRIP_STATIC                                                      \
+  " --strip-static fun[,fun...]  remove static from functions\n"
+
+#endif /* CPROVER_GOTO_INSTRUMENT_STRIP_STATIC_H */