Remove initializations of unused global variables

regression/goto-instrument/chain.sh

@@ -1,12 +1,14 @@
 #!/bin/bash
 
-SRC=../../../src
+src=../../../src
+goto_cc=$src/goto-cc/goto-cc
+goto_instrument=$src/goto-instrument/goto-instrument
 
-GC=$SRC/goto-cc/goto-cc
-GI=$SRC/goto-instrument/goto-instrument
+name=${@:$#}
+name=${name%.c}
 
-OPTS=$1
-NAME=${2%.c}
+args=${@:1:$#-1}
+
+$goto_cc -o $name.gb $name.c
+$goto_instrument $args $name.gb
 
-$GC $NAME.c -o $NAME.gb
-$GI $OPTS $NAME.gb

regression/goto-instrument/restore-returns1/test.desc

@@ -1,6 +1,6 @@
 CORE
 ret.c
-"--escape-analysis --dump-c"
+--escape-analysis --dump-c
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/goto-instrument/restore-returns2/test.desc

@@ -1,6 +1,6 @@
 CORE
 ret.c
-"--escape-analysis --dump-c"
+--escape-analysis --dump-c
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/goto-instrument/slice-global-inits1/main.c

@@ -0,0 +1,42 @@
+
+int x;
+int y;
+
+int z;
+
+int a[10];
+
+typedef struct some_struct {
+  int a;
+  int b;
+} some_struct_t;
+
+some_struct_t s1;
+some_struct_t s2;
+
+void func1()
+{
+  s1.a = 7;
+}
+
+void func2()
+{
+  s2.a = 7;
+}
+
+void func3()
+{
+  func3();
+}
+
+int main()
+{
+  z = 1;
+  z = a[0];
+
+  func2();
+
+  func3();
+
+  return 0;
+}

regression/goto-instrument/slice-global-inits1/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--slice-global-inits --show-goto-functions
+z = 0;$
+a =
+s2 =
+^EXIT=0$
+^SIGNAL=0$
+--
+x = 0;$
+y = 0;$
+s1 =
+^warning: ignoring

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -32,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_asm.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/parameter_assignments.h>
+#include <goto-programs/slice_global_inits.h>
 
 #include <pointer-analysis/value_set_analysis.h>
 #include <pointer-analysis/goto_program_dereference.h>
@@ -1015,6 +1016,13 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     nondet_static(ns, goto_functions);
   }
 
+  if(cmdline.isset("slice-global-inits"))
+  {
+    status() << "Slicing away initializations of unused global variables"
+             << eom;
+    slice_global_inits(ns, goto_functions);
+  }
+
   if(cmdline.isset("string-abstraction"))
   {
     status() << "String Abstraction" << eom;
@@ -1371,6 +1379,7 @@ void goto_instrument_parse_optionst::help()
     " --reachability-slice         slice away instructions that can't reach assertions\n"
     " --full-slice                 slice away instructions that don't affect assertions\n"
     " --property id                slice with respect to specific property only\n"
+    " --slice-global-inits         slice away initializations of unused global variables\n"
     "\n"
     "Further transformations:\n"
     " --constant-propagator        propagate constants and simplify expressions\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -50,7 +50,7 @@ Author: Daniel Kroening, [email protected]
   "(custom-bitvector-analysis)" \
   "(show-struct-alignment)(interval-analysis)(show-intervals)" \
   "(show-uninitialized)(show-locations)" \
-  "(full-slice)(reachability-slice)" \
+  "(full-slice)(reachability-slice)(slice-global-inits)" \
   "(inline)(remove-function-pointers)" \
   "(show-claims)(show-properties)(property):" \
   "(show-symbol-table)(show-points-to)(show-rw-set)" \

src/goto-programs/Makefile

@@ -16,7 +16,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \
       remove_returns.cpp osx_fat_reader.cpp remove_complex.cpp \
       goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \
       graphml_witness.cpp remove_virtual_functions.cpp \
-      class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp
+      class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \
+      slice_global_inits.cpp
 
 INCLUDES= -I ..
 

src/goto-programs/slice_global_inits.cpp

@@ -0,0 +1,140 @@
+/*******************************************************************\
+
+Module: Remove initializations of unused global variables
+
+Author: Daniel Poetzl
+
+Date:   December 2016
+
+\*******************************************************************/
+
+#include <analyses/call_graph.h>
+
+#include <util/namespace.h>
+#include <util/std_expr.h>
+#include <util/cprover_prefix.h>
+#include <util/prefix.h>
+#include <util/hash_cont.h>
+
+#include <goto-programs/goto_functions.h>
+#include <goto-programs/remove_skip.h>
+
+#include "slice_global_inits.h"
+
+/*******************************************************************\
+
+Function: slice_global_inits
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void slice_global_inits(
+  const namespacet &ns,
+  goto_functionst &goto_functions)
+{
+  // gather all functions reachable from the entry point
+
+  call_grapht call_graph(goto_functions);
+  const call_grapht::grapht &graph=call_graph.graph;
+
+  std::list<irep_idt> worklist;
+  hash_set_cont<irep_idt, irep_id_hash> functions_reached;
+
+  const irep_idt entry_point=goto_functionst::entry_point();
+
+  goto_functionst::function_mapt::const_iterator e_it;
+  e_it=goto_functions.function_map.find(entry_point);
+
+  if(e_it==goto_functions.function_map.end())
+    throw "entry point not found";
+
+  worklist.push_back(entry_point);
+
+  do
+  {
+    const irep_idt id=worklist.front();
+    worklist.pop_front();
+
+    functions_reached.insert(id);
+
+    const auto &p=graph.equal_range(id);
+
+    for(auto it=p.first; it!=p.second; it++)
+    {
+      const irep_idt callee=it->second;
+
+      if(functions_reached.find(callee)==functions_reached.end())
+        worklist.push_back(callee);
+    }
+  } while(!worklist.empty());
+
+  const irep_idt initialize=CPROVER_PREFIX "initialize";
+  functions_reached.erase(initialize);
+
+  // gather all symbols used by reachable functions
+
+  class symbol_collectort:public const_expr_visitort
+  {
+  public:
+    virtual void operator()(const exprt &expr)
+    {
+      if(expr.id()==ID_symbol)
+      {
+        const symbol_exprt &symbol_expr=to_symbol_expr(expr);
+        const irep_idt id=symbol_expr.get_identifier();
+        symbols.insert(id);
+      }
+    }
+
+    hash_set_cont<irep_idt, irep_id_hash> symbols;
+  };
+
+  symbol_collectort visitor;
+
+  assert(!functions_reached.empty());
+
+  for(const irep_idt &id : functions_reached)
+  {
+    const goto_functionst::goto_functiont &goto_function
+      =goto_functions.function_map.at(id);
+    const goto_programt &goto_program=goto_function.body;
+
+    forall_goto_program_instructions(i_it, goto_program)
+    {
+      const codet &code=i_it->code;
+      code.visit(visitor);
+    }
+  }
+
+  const hash_set_cont<irep_idt, irep_id_hash> &symbols=visitor.symbols;
+
+  // now remove unnecessary initializations
+
+  goto_functionst::function_mapt::iterator f_it;
+  f_it=goto_functions.function_map.find(initialize);
+  assert(f_it!=goto_functions.function_map.end());
+
+  goto_programt &goto_program=f_it->second.body;
+
+  Forall_goto_program_instructions(i_it, goto_program)
+  {
+    if(i_it->is_assign())
+    {
+      const code_assignt &code_assign=to_code_assign(i_it->code);
+      const symbol_exprt &symbol_expr=to_symbol_expr(code_assign.lhs());
+      const irep_idt id=symbol_expr.get_identifier();
+
+      if(!has_prefix(id2string(id), CPROVER_PREFIX) &&
+         symbols.find(id)==symbols.end())
+        i_it->make_skip();
+    }
+  }
+
+  remove_skip(goto_functions);
+  goto_functions.update();
+}

src/goto-programs/slice_global_inits.h

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Remove initializations of unused global variables
+
+Author: Daniel Poetzl
+
+Date:   December 2016
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H
+#define CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H
+
+class goto_functionst;
+class namespacet;
+
+void slice_global_inits(
+  const namespacet &ns,
+  goto_functionst &goto_functions);
+
+#endif