From b7ed4c766d2ce69d23d91d1ce9a51366991c5674 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Sun, 11 Dec 2016 13:31:14 +0000 Subject: [PATCH 1/2] fix chain.sh to not require quotes in options in test.desc --- regression/goto-instrument/chain.sh | 16 +++++++++------- .../goto-instrument/restore-returns1/test.desc | 2 +- .../goto-instrument/restore-returns2/test.desc | 2 +- 3 files changed, 11 insertions(+), 9 deletions(-) diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh index 174e93ddc5d..ce2db004a7c 100755 --- a/regression/goto-instrument/chain.sh +++ b/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 diff --git a/regression/goto-instrument/restore-returns1/test.desc b/regression/goto-instrument/restore-returns1/test.desc index aecf983ef22..baea62d005a 100644 --- a/regression/goto-instrument/restore-returns1/test.desc +++ b/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$ -- diff --git a/regression/goto-instrument/restore-returns2/test.desc b/regression/goto-instrument/restore-returns2/test.desc index aecf983ef22..baea62d005a 100644 --- a/regression/goto-instrument/restore-returns2/test.desc +++ b/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$ -- From 2df6785fb84bd763be8370f1bf7e2f5e14922d57 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Sun, 11 Dec 2016 13:32:47 +0000 Subject: [PATCH 2/2] remove initializations of unused global variables --- .../slice-global-inits1/main.c | 42 ++++++ .../slice-global-inits1/test.desc | 13 ++ .../goto_instrument_parse_options.cpp | 9 ++ .../goto_instrument_parse_options.h | 2 +- src/goto-programs/Makefile | 3 +- src/goto-programs/slice_global_inits.cpp | 140 ++++++++++++++++++ src/goto-programs/slice_global_inits.h | 21 +++ 7 files changed, 228 insertions(+), 2 deletions(-) create mode 100644 regression/goto-instrument/slice-global-inits1/main.c create mode 100644 regression/goto-instrument/slice-global-inits1/test.desc create mode 100644 src/goto-programs/slice_global_inits.cpp create mode 100644 src/goto-programs/slice_global_inits.h diff --git a/regression/goto-instrument/slice-global-inits1/main.c b/regression/goto-instrument/slice-global-inits1/main.c new file mode 100644 index 00000000000..8ab123d1014 --- /dev/null +++ b/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; +} diff --git a/regression/goto-instrument/slice-global-inits1/test.desc b/regression/goto-instrument/slice-global-inits1/test.desc new file mode 100644 index 00000000000..6e8a7deedeb --- /dev/null +++ b/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 diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 23d681c5644..14549d17474 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -32,6 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -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" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 243a4c02f50..5c2c6bae3ac 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -50,7 +50,7 @@ Author: Daniel Kroening, kroening@kroening.com "(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)" \ diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 932508b0edf..f424f150640 100644 --- a/src/goto-programs/Makefile +++ b/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 .. diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp new file mode 100644 index 00000000000..a02c5b3f51f --- /dev/null +++ b/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 + +#include +#include +#include +#include +#include + +#include +#include + +#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 worklist; + hash_set_cont 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 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 &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(); +} diff --git a/src/goto-programs/slice_global_inits.h b/src/goto-programs/slice_global_inits.h new file mode 100644 index 00000000000..7907c31c49b --- /dev/null +++ b/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