From 6d0776fb5f7369843904383abe87ed9937120757 Mon Sep 17 00:00:00 2001 From: Polgreen Date: Tue, 31 Jul 2018 08:53:33 +0200 Subject: [PATCH 1/2] if function is not in the function map, treat as if it has no body For the call graph, we add the function to the call graph but do not try to look for function calls in the body. For slicing global inits, we do not try to look in the function body for symbols. This fixes issue https://github.com/diffblue/cbmc/issues/2631 --- .../goto-instrument/assembly_call_graph_test/main.c | 12 ++++++++++++ .../assembly_call_graph_test/test.desc | 11 +++++++++++ src/analyses/call_graph.cpp | 9 +++++++-- src/goto-programs/slice_global_inits.cpp | 12 ++++++++---- 4 files changed, 38 insertions(+), 6 deletions(-) create mode 100644 regression/goto-instrument/assembly_call_graph_test/main.c create mode 100644 regression/goto-instrument/assembly_call_graph_test/test.desc diff --git a/regression/goto-instrument/assembly_call_graph_test/main.c b/regression/goto-instrument/assembly_call_graph_test/main.c new file mode 100644 index 00000000000..6705ea7a726 --- /dev/null +++ b/regression/goto-instrument/assembly_call_graph_test/main.c @@ -0,0 +1,12 @@ +void* thr(void * arg) { +#ifdef __GNUC__ +__asm__ __volatile__ ("mfence": : :"memory"); +#elif defined(_MSC_VER) +__asm mfence; +#endif +} + +int main() +{ + thr(0); +} diff --git a/regression/goto-instrument/assembly_call_graph_test/test.desc b/regression/goto-instrument/assembly_call_graph_test/test.desc new file mode 100644 index 00000000000..655514fbb22 --- /dev/null +++ b/regression/goto-instrument/assembly_call_graph_test/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--reachable-call-graph +main -> thr +__CPROVER__start -> __CPROVER_initialize +__CPROVER__start -> main +thr -> __asm_mfence +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp index 881348279f2..6354ec41485 100644 --- a/src/analyses/call_graph.cpp +++ b/src/analyses/call_graph.cpp @@ -84,11 +84,16 @@ call_grapht::call_grapht( { irep_idt function=pending_stack.top(); pending_stack.pop(); - const goto_programt &goto_program= - goto_functions.function_map.at(function).body; nodes.insert(function); + // if function is not in function_map, assume function has no body + const auto &it = goto_functions.function_map.find(function); + if(it == goto_functions.function_map.end()) + continue; + + const goto_programt &goto_program = it->second.body; + forall_callsites( goto_program, [&](goto_programt::const_targett i_it, const irep_idt &callee) diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index 0c51b77fca8..ed50376570c 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -52,13 +52,17 @@ void slice_global_inits(goto_modelt &goto_model) const irep_idt &id = directed_graph[node_idx].function; if(id == INITIALIZE_FUNCTION) continue; - const goto_functionst::goto_functiont &goto_function - =goto_functions.function_map.at(id); - const goto_programt &goto_program=goto_function.body; + + // assume function has no body if it is not in the function map + const auto &it = goto_functions.function_map.find(id); + if(it == goto_functions.function_map.end()) + continue; + + const goto_programt &goto_program = it->second.body; forall_goto_program_instructions(i_it, goto_program) { - const codet &code=i_it->code; + const codet &code = i_it->code; find_symbols(code, symbols, true, false); const exprt &expr = i_it->guard; find_symbols(expr, symbols, true, false); From ea2d3933e3d858cb2ac5a2e444a2c74ebdad0ad8 Mon Sep 17 00:00:00 2001 From: Polgreen Date: Tue, 31 Jul 2018 13:14:57 +0200 Subject: [PATCH 2/2] Make test work on windows This is a hack, but "__asm__ __volatile__ ("mfence": : :"memory");" doesn't compile on windows and the way CBMC handles "__asm mfence" needs to be fixed. Currently "__asm mfence" is not recognised as a function by CBMC. --- .../goto-instrument/assembly_call_graph_test/main.c | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/regression/goto-instrument/assembly_call_graph_test/main.c b/regression/goto-instrument/assembly_call_graph_test/main.c index 6705ea7a726..afc2bbc5c3c 100644 --- a/regression/goto-instrument/assembly_call_graph_test/main.c +++ b/regression/goto-instrument/assembly_call_graph_test/main.c @@ -1,8 +1,16 @@ +// This is a hack to make the test pass on windows. The way CBMC on +// windows handles assembly code needs to be fixed. +// CBMC doesn't recognise __asm mfence as a function. + +#ifndef __GNUC__ +void __asm_mfence(); +#endif + void* thr(void * arg) { #ifdef __GNUC__ __asm__ __volatile__ ("mfence": : :"memory"); -#elif defined(_MSC_VER) -__asm mfence; +#else +__asm_mfence(); #endif }