From 1a52faebdcfe78e8b332051971bc354af3af63b4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 18:30:19 +0100 Subject: [PATCH] Remove dubious module dependencies in goto-programs - Move call_graph and does_remove_const from analyses to goto-programs - Move symex_target_equation graphml functions to goto-symex - Update module_dependencies.txt and build files accordingly - Refactor code to eliminate cross-module dependencies Fixes: #571 --- src/goto-checker/bmc_util.cpp | 3 +- src/goto-instrument/aggressive_slicer.cpp | 3 +- src/goto-instrument/aggressive_slicer.h | 9 +- .../goto_instrument_parse_options.cpp | 2 +- src/goto-programs/CMakeLists.txt | 2 +- src/goto-programs/Makefile | 3 + .../call_graph.cpp | 83 +++-- src/{analyses => goto-programs}/call_graph.h | 25 +- .../call_graph_helpers.cpp | 14 +- .../call_graph_helpers.h | 16 +- .../does_remove_const.cpp | 25 +- .../does_remove_const.h | 18 +- src/goto-programs/graphml_witness.cpp | 153 --------- src/goto-programs/graphml_witness.h | 2 - src/goto-programs/module_dependencies.txt | 2 - .../remove_function_pointers.cpp | 3 +- src/goto-programs/slice_global_inits.cpp | 2 +- src/goto-symex/Makefile | 1 + .../symex_target_equation_graphml_witness.cpp | 314 ++++++++++++++++++ .../symex_target_equation_graphml_witness.h | 71 ++++ unit/analyses/call_graph.cpp | 4 +- .../disconnect_unreachable_nodes_in_graph.cpp | 2 +- .../does_expr_lose_const.cpp | 2 +- .../does_type_preserve_const_correctness.cpp | 8 +- .../is_type_at_least_as_const_as.cpp | 8 +- 25 files changed, 501 insertions(+), 274 deletions(-) rename src/{analyses => goto-programs}/call_graph.cpp (83%) rename src/{analyses => goto-programs}/call_graph.h (94%) rename src/{analyses => goto-programs}/call_graph_helpers.cpp (90%) rename src/{analyses => goto-programs}/call_graph_helpers.h (89%) rename src/{analyses => goto-programs}/does_remove_const.cpp (93%) rename src/{analyses => goto-programs}/does_remove_const.h (60%) create mode 100644 src/goto-symex/symex_target_equation_graphml_witness.cpp create mode 100644 src/goto-symex/symex_target_equation_graphml_witness.h diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index d7ea8ada8c4..9ecb496fa54 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, Peter Schrammel #include #include #include +#include #include #include "goto_symex_property_decider.h" @@ -133,7 +134,7 @@ void output_graphml( if(graphml.empty()) return; - graphml_witnesst graphml_witness(ns); + symex_target_equation_graphml_witnesst graphml_witness(ns); graphml_witness(symex_target_equation); if(graphml == "-") diff --git a/src/goto-instrument/aggressive_slicer.cpp b/src/goto-instrument/aggressive_slicer.cpp index 46f092774b4..e99a6287c4f 100644 --- a/src/goto-instrument/aggressive_slicer.cpp +++ b/src/goto-instrument/aggressive_slicer.cpp @@ -13,13 +13,12 @@ Author: Elizabeth Polgreen, elizabeth.polgreen@cs.ox.ac.uk #include +#include #include #include #include -#include - #include "remove_function.h" void aggressive_slicert::note_functions_to_keep( diff --git a/src/goto-instrument/aggressive_slicer.h b/src/goto-instrument/aggressive_slicer.h index b5ebf25217d..2d8c1a90162 100644 --- a/src/goto-instrument/aggressive_slicer.h +++ b/src/goto-instrument/aggressive_slicer.h @@ -14,15 +14,14 @@ Author: Elizabeth Polgreen, polgreen@amazon.com #ifndef CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H #define CPROVER_GOTO_INSTRUMENT_AGGRESSIVE_SLICER_H -#include -#include - #include -#include - +#include #include +#include +#include + class message_handlert; /// \brief The aggressive slicer removes the body of all the functions except diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 570554155b4..2938a29ffbd 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -47,7 +48,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include diff --git a/src/goto-programs/CMakeLists.txt b/src/goto-programs/CMakeLists.txt index f0748416435..7e7d34eaa2f 100644 --- a/src/goto-programs/CMakeLists.txt +++ b/src/goto-programs/CMakeLists.txt @@ -3,4 +3,4 @@ add_library(goto-programs ${sources}) generic_includes(goto-programs) -target_link_libraries(goto-programs util assembler langapi analyses linking ansi-c) +target_link_libraries(goto-programs util assembler langapi linking ansi-c) diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index bacc92ac152..174e4c07089 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -1,7 +1,10 @@ SRC = adjust_float_expressions.cpp \ + call_graph.cpp \ + call_graph_helpers.cpp \ class_hierarchy.cpp \ class_identifier.cpp \ compute_called_functions.cpp \ + does_remove_const.cpp \ elf_reader.cpp \ ensure_one_backedge_per_target.cpp \ goto_check.cpp \ diff --git a/src/analyses/call_graph.cpp b/src/goto-programs/call_graph.cpp similarity index 83% rename from src/analyses/call_graph.cpp rename to src/goto-programs/call_graph.cpp index 543e68302a4..e984176813a 100644 --- a/src/analyses/call_graph.cpp +++ b/src/goto-programs/call_graph.cpp @@ -13,13 +13,13 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include "goto_model.h" /// Create empty call graph /// \param collect_callsites: if true, then each added graph edge will have /// the calling instruction recorded in `callsites` map. -call_grapht::call_grapht(bool collect_callsites): - collect_callsites(collect_callsites) +call_grapht::call_grapht(bool collect_callsites) + : collect_callsites(collect_callsites) { } @@ -27,8 +27,8 @@ call_grapht::call_grapht(bool collect_callsites): /// \param goto_model: model to search for callsites /// \param collect_callsites: if true, then each added graph edge will have /// the calling instruction recorded in `callsites` map. -call_grapht::call_grapht(const goto_modelt &goto_model, bool collect_callsites): - call_grapht(goto_model.goto_functions, collect_callsites) +call_grapht::call_grapht(const goto_modelt &goto_model, bool collect_callsites) + : call_grapht(goto_model.goto_functions, collect_callsites) { } @@ -37,8 +37,9 @@ call_grapht::call_grapht(const goto_modelt &goto_model, bool collect_callsites): /// \param collect_callsites: if true, then each added graph edge will have /// the calling instruction recorded in `callsites` map. call_grapht::call_grapht( - const goto_functionst &goto_functions, bool collect_callsites): - collect_callsites(collect_callsites) + const goto_functionst &goto_functions, + bool collect_callsites) + : collect_callsites(collect_callsites) { for(const auto &gf_entry : goto_functions.function_map) { @@ -75,15 +76,15 @@ static void forall_callsites( call_grapht::call_grapht( const goto_functionst &goto_functions, const irep_idt &root, - bool collect_callsites): - collect_callsites(collect_callsites) + bool collect_callsites) + : collect_callsites(collect_callsites) { std::stack> pending_stack; pending_stack.push(root); while(!pending_stack.empty()) { - irep_idt function=pending_stack.top(); + irep_idt function = pending_stack.top(); pending_stack.pop(); nodes.insert(function); @@ -97,13 +98,11 @@ call_grapht::call_grapht( forall_callsites( goto_program, - [&](goto_programt::const_targett i_it, const irep_idt &callee) - { + [&](goto_programt::const_targett i_it, const irep_idt &callee) { add(function, callee, i_it); - if(edges.find(callee)==edges.end()) + if(edges.find(callee) == edges.end()) pending_stack.push(callee); - } - ); // NOLINT + }); // NOLINT } } @@ -115,30 +114,23 @@ call_grapht::call_grapht( call_grapht::call_grapht( const goto_modelt &goto_model, const irep_idt &root, - bool collect_callsites): - call_grapht(goto_model.goto_functions, root, collect_callsites) + bool collect_callsites) + : call_grapht(goto_model.goto_functions, root, collect_callsites) { } -void call_grapht::add( - const irep_idt &function, - const goto_programt &body) +void call_grapht::add(const irep_idt &function, const goto_programt &body) { forall_callsites( - body, - [&](goto_programt::const_targett i_it, const irep_idt &callee) - { + body, [&](goto_programt::const_targett i_it, const irep_idt &callee) { add(function, callee, i_it); - } - ); // NOLINT + }); // NOLINT } /// Add edge /// \param caller: caller function /// \param callee: callee function -void call_grapht::add( - const irep_idt &caller, - const irep_idt &callee) +void call_grapht::add(const irep_idt &caller, const irep_idt &callee) { edges.insert({caller, callee}); nodes.insert(caller); @@ -181,19 +173,18 @@ class function_indicest public: std::unordered_map function_indices; - explicit function_indicest(call_grapht::directed_grapht &graph): - graph(graph) + explicit function_indicest(call_grapht::directed_grapht &graph) : graph(graph) { } node_indext operator[](const irep_idt &function) { - auto findit=function_indices.insert({function, 0}); + auto findit = function_indices.insert({function, 0}); if(findit.second) { - node_indext new_index=graph.add_node(); - findit.first->second=new_index; - graph[new_index].function=function; + node_indext new_index = graph.add_node(); + findit.first->second = new_index; + graph[new_index].function = function; } return findit.first->second; } @@ -218,19 +209,19 @@ call_grapht::directed_grapht call_grapht::get_directed_graph() const for(const auto &edge : edges) { - auto a_index=function_indices[edge.first]; - auto b_index=function_indices[edge.second]; + auto a_index = function_indices[edge.first]; + auto b_index = function_indices[edge.second]; // Check then create the edge like this to avoid copying the callsites // set once per parallel edge, which could be costly if there are many. if(!ret.has_edge(a_index, b_index)) { ret.add_edge(a_index, b_index); if(collect_callsites) - ret[a_index].out[b_index].callsites=callsites.at(edge); + ret[a_index].out[b_index].callsites = callsites.at(edge); } } - ret.nodes_by_name=std::move(function_indices.function_indices); + ret.nodes_by_name = std::move(function_indices.function_indices); return ret; } @@ -241,14 +232,14 @@ call_grapht::directed_grapht call_grapht::get_directed_graph() const std::string call_grapht::format_callsites(const edget &edge) const { PRECONDITION(collect_callsites); - std::string ret="{"; + std::string ret = "{"; for(const locationt &loc : callsites.at(edge)) { - if(ret.size()>1) - ret+=", "; - ret+=std::to_string(loc->location_number); + if(ret.size() > 1) + ret += ", "; + ret += std::to_string(loc->location_number); } - ret+='}'; + ret += '}'; return ret; } @@ -285,7 +276,7 @@ void call_grapht::output_xml(std::ostream &out) const // to the first interested XML user. if(collect_callsites) out << "\n"; + " If you need this, edit call_grapht::output_xml -->\n"; for(const auto &edge : edges) { out << " call_grapht::directed_grapht::get_node_index(const irep_idt &function) const { - auto findit=nodes_by_name.find(function); - if(findit==nodes_by_name.end()) + auto findit = nodes_by_name.find(function); + if(findit == nodes_by_name.end()) return std::optional(); else return findit->second; diff --git a/src/analyses/call_graph.h b/src/goto-programs/call_graph.h similarity index 94% rename from src/analyses/call_graph.h rename to src/goto-programs/call_graph.h index 630f277f306..d03b32fc327 100644 --- a/src/analyses/call_graph.h +++ b/src/goto-programs/call_graph.h @@ -9,17 +9,17 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Function Call Graphs -#ifndef CPROVER_ANALYSES_CALL_GRAPH_H -#define CPROVER_ANALYSES_CALL_GRAPH_H +#ifndef CPROVER_GOTO_PROGRAMS_CALL_GRAPH_H +#define CPROVER_GOTO_PROGRAMS_CALL_GRAPH_H + +#include + +#include "goto_program.h" #include #include #include -#include - -#include - class goto_functionst; class goto_modelt; @@ -43,9 +43,9 @@ class goto_modelt; class call_grapht { public: - explicit call_grapht(bool collect_callsites=false); - explicit call_grapht(const goto_modelt &, bool collect_callsites=false); - explicit call_grapht(const goto_functionst &, bool collect_callsites=false); + explicit call_grapht(bool collect_callsites = false); + explicit call_grapht(const goto_modelt &, bool collect_callsites = false); + explicit call_grapht(const goto_functionst &, bool collect_callsites = false); // These two functions build a call graph restricted to functions // reachable from the given root. @@ -79,7 +79,6 @@ class call_grapht bool collect_callsites); public: - void output_dot(std::ostream &out) const; void output(std::ostream &out) const; void output_xml(std::ostream &out) const; @@ -163,11 +162,11 @@ class call_grapht directed_grapht get_directed_graph() const; protected: - void add(const irep_idt &function, - const goto_programt &body); + void add(const irep_idt &function, const goto_programt &body); + private: bool collect_callsites; std::string format_callsites(const edget &edge) const; }; -#endif // CPROVER_ANALYSES_CALL_GRAPH_H +#endif // CPROVER_GOTO_PROGRAMS_CALL_GRAPH_H diff --git a/src/analyses/call_graph_helpers.cpp b/src/goto-programs/call_graph_helpers.cpp similarity index 90% rename from src/analyses/call_graph_helpers.cpp rename to src/goto-programs/call_graph_helpers.cpp index 0723e3eb181..55099171854 100644 --- a/src/analyses/call_graph_helpers.cpp +++ b/src/goto-programs/call_graph_helpers.cpp @@ -28,14 +28,14 @@ static std::set get_neighbours( return result; } -std::set get_callees( - const call_grapht::directed_grapht &graph, const irep_idt &function) +std::set +get_callees(const call_grapht::directed_grapht &graph, const irep_idt &function) { return get_neighbours(graph, function, true); } -std::set get_callers( - const call_grapht::directed_grapht &graph, const irep_idt &function) +std::set +get_callers(const call_grapht::directed_grapht &graph, const irep_idt &function) { return get_neighbours(graph, function, false); } @@ -60,13 +60,15 @@ static std::set get_connected_functions( } std::set get_reachable_functions( - const call_grapht::directed_grapht &graph, const irep_idt &function) + const call_grapht::directed_grapht &graph, + const irep_idt &function) { return get_connected_functions(graph, function, true); } std::set get_reaching_functions( - const call_grapht::directed_grapht &graph, const irep_idt &function) + const call_grapht::directed_grapht &graph, + const irep_idt &function) { return get_connected_functions(graph, function, false); } diff --git a/src/analyses/call_graph_helpers.h b/src/goto-programs/call_graph_helpers.h similarity index 89% rename from src/analyses/call_graph_helpers.h rename to src/goto-programs/call_graph_helpers.h index 202590e5543..2dbe82e18bd 100644 --- a/src/analyses/call_graph_helpers.h +++ b/src/goto-programs/call_graph_helpers.h @@ -9,8 +9,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com /// \file /// Function Call Graph Helpers -#ifndef CPROVER_ANALYSES_CALL_GRAPH_HELPERS_H -#define CPROVER_ANALYSES_CALL_GRAPH_HELPERS_H +#ifndef CPROVER_GOTO_PROGRAMS_CALL_GRAPH_HELPERS_H +#define CPROVER_GOTO_PROGRAMS_CALL_GRAPH_HELPERS_H #include "call_graph.h" @@ -26,28 +26,32 @@ Author: Chris Smowton, chris.smowton@diffblue.com /// \param function: function to query /// \return set of called functions std::set get_callees( - const call_grapht::directed_grapht &graph, const irep_idt &function); + const call_grapht::directed_grapht &graph, + const irep_idt &function); /// Get functions that call a given function /// \param graph: call graph /// \param function: function to query /// \return set of caller functions std::set get_callers( - const call_grapht::directed_grapht &graph, const irep_idt &function); + const call_grapht::directed_grapht &graph, + const irep_idt &function); /// Get functions reachable from a given function /// \param graph: call graph /// \param function: function to query /// \return set of reachable functions, including `function` std::set get_reachable_functions( - const call_grapht::directed_grapht &graph, const irep_idt &function); + const call_grapht::directed_grapht &graph, + const irep_idt &function); /// Get functions that can reach a given function /// \param graph: call graph /// \param function: function to query /// \return set of functions that can reach the target, including `function` std::set get_reaching_functions( - const call_grapht::directed_grapht &graph, const irep_idt &function); + const call_grapht::directed_grapht &graph, + const irep_idt &function); /// Get either callers or callees reachable from a given /// list of functions within N steps diff --git a/src/analyses/does_remove_const.cpp b/src/goto-programs/does_remove_const.cpp similarity index 93% rename from src/analyses/does_remove_const.cpp rename to src/goto-programs/does_remove_const.cpp index 8e88299fe3f..4cb5619f6e1 100644 --- a/src/analyses/does_remove_const.cpp +++ b/src/goto-programs/does_remove_const.cpp @@ -1,32 +1,33 @@ /*******************************************************************\ -Module: Analyses +Module: Goto Programs Author: Diffblue Ltd. \*******************************************************************/ /// \file -/// Analyses +/// Goto Programs #include "does_remove_const.h" -#include - #include +#include "goto_program.h" + /// A naive analysis to look for casts that remove const-ness from pointers. /// \param goto_program: the goto program to check does_remove_constt::does_remove_constt(const goto_programt &goto_program) : goto_program(goto_program) -{} +{ +} /// A naive analysis to look for casts that remove const-ness from pointers. /// \return Returns true if the program contains a const-removing cast std::pair does_remove_constt::operator()() const { for(const goto_programt::instructiont &instruction : - goto_program.instructions) + goto_program.instructions) { if(!instruction.is_assign()) { @@ -60,12 +61,12 @@ std::pair does_remove_constt::operator()() const /// ness is lost. bool does_remove_constt::does_expr_lose_const(const exprt &expr) const { - const typet &root_type=expr.type(); + const typet &root_type = expr.type(); // Look in each child that has the same type as the root for(const exprt &op : expr.operands()) { - const typet &op_type=op.type(); + const typet &op_type = op.type(); if(op_type == root_type) { // Is this child more const-qualified than the root @@ -112,9 +113,10 @@ bool does_remove_constt::does_expr_lose_const(const exprt &expr) const /// \return Returns true if a value of type source_type could be assigned into a /// a value of target_type without losing const-correctness bool does_remove_constt::does_type_preserve_const_correctness( - const typet *target_type, const typet *source_type) const + const typet *target_type, + const typet *source_type) const { - while(target_type->id()==ID_pointer) + while(target_type->id() == ID_pointer) { PRECONDITION(source_type->id() == ID_pointer); @@ -156,7 +158,8 @@ bool does_remove_constt::does_type_preserve_const_correctness( /// const qualified /// \return Returns true if type_more_const is at least as const as type_compare bool does_remove_constt::is_type_at_least_as_const_as( - const typet &type_more_const, const typet &type_compare) const + const typet &type_more_const, + const typet &type_compare) const { return !type_compare.get_bool(ID_C_constant) || type_more_const.get_bool(ID_C_constant); diff --git a/src/analyses/does_remove_const.h b/src/goto-programs/does_remove_const.h similarity index 60% rename from src/analyses/does_remove_const.h rename to src/goto-programs/does_remove_const.h index b5a682aed2c..41c19fcfec0 100644 --- a/src/analyses/does_remove_const.h +++ b/src/goto-programs/does_remove_const.h @@ -1,15 +1,15 @@ /*******************************************************************\ -Module: Analyses +Module: Goto Programs Author: Diffblue Ltd. \*******************************************************************/ /// \file -/// Analyses +/// Goto Programs -#ifndef CPROVER_ANALYSES_DOES_REMOVE_CONST_H -#define CPROVER_ANALYSES_DOES_REMOVE_CONST_H +#ifndef CPROVER_GOTO_PROGRAMS_DOES_REMOVE_CONST_H +#define CPROVER_GOTO_PROGRAMS_DOES_REMOVE_CONST_H #include @@ -22,20 +22,22 @@ class does_remove_constt { public: explicit does_remove_constt(const goto_programt &); - std::pair operator()() const; + std::pair operator()() const; private: bool does_expr_lose_const(const exprt &expr) const; bool is_type_at_least_as_const_as( - const typet &type_more_const, const typet &type_compare) const; + const typet &type_more_const, + const typet &type_compare) const; bool does_type_preserve_const_correctness( - const typet *target_type, const typet *source_type) const; + const typet *target_type, + const typet *source_type) const; const goto_programt &goto_program; friend class does_remove_const_testt; }; -#endif // CPROVER_ANALYSES_DOES_REMOVE_CONST_H +#endif // CPROVER_GOTO_PROGRAMS_DOES_REMOVE_CONST_H diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index 239922a2ab3..68de51b31f5 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -23,7 +23,6 @@ Author: Daniel Kroening #include #include -#include #include #include @@ -519,155 +518,3 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) it=next; } } - -/// proof witness -void graphml_witnesst::operator()(const symex_target_equationt &equation) -{ - graphml.key_values["sourcecodelang"]="C"; - - const graphmlt::node_indext sink=graphml.add_node(); - graphml[sink].node_name="sink"; - graphml[sink].is_violation=false; - graphml[sink].has_invariant=false; - - // step numbers start at 1 - std::vector step_to_node(equation.SSA_steps.size()+1, 0); - - std::size_t step_nr=1; - for(symex_target_equationt::SSA_stepst::const_iterator - it=equation.SSA_steps.begin(); - it!=equation.SSA_steps.end(); - it++, step_nr++) // we cannot replace this by a ranged for - { - const source_locationt &source_location = it->source.pc->source_location(); - - if( - it->hidden || - (!it->is_assignment() && !it->is_goto() && !it->is_assert()) || - (it->is_goto() && it->source.pc->condition() == true) || - source_location.is_nil() || source_location.is_built_in() || - source_location.get_line().empty()) - { - step_to_node[step_nr]=sink; - - continue; - } - - // skip declarations followed by an immediate assignment - symex_target_equationt::SSA_stepst::const_iterator next=it; - ++next; - if( - next != equation.SSA_steps.end() && next->is_assignment() && - it->ssa_full_lhs == next->ssa_full_lhs && - it->source.pc->source_location() == next->source.pc->source_location()) - { - step_to_node[step_nr]=sink; - - continue; - } - - const graphmlt::node_indext node=graphml.add_node(); - graphml[node].node_name= - std::to_string(it->source.pc->location_number)+"."+ - std::to_string(step_nr); - graphml[node].file=source_location.get_file(); - graphml[node].line=source_location.get_line(); - graphml[node].is_violation=false; - graphml[node].has_invariant=false; - - step_to_node[step_nr]=node; - } - - // build edges - step_nr=1; - for(symex_target_equationt::SSA_stepst::const_iterator - it=equation.SSA_steps.begin(); - it!=equation.SSA_steps.end(); - ) // no ++it - { - const std::size_t from=step_to_node[step_nr]; - - if(from==sink) - { - ++it; - ++step_nr; - continue; - } - - symex_target_equationt::SSA_stepst::const_iterator next=it; - std::size_t next_step_nr=step_nr; - for(++next, ++next_step_nr; - next!=equation.SSA_steps.end() && - (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc); - ++next, ++next_step_nr) - { - // advance - } - const std::size_t to= - next==equation.SSA_steps.end()? - sink:step_to_node[next_step_nr]; - - switch(it->type) - { - case goto_trace_stept::typet::ASSIGNMENT: - case goto_trace_stept::typet::ASSERT: - case goto_trace_stept::typet::GOTO: - case goto_trace_stept::typet::SPAWN: - { - xmlt edge( - "edge", - {{"source", graphml[from].node_name}, - {"target", graphml[to].node_name}}, - {}); - - { - xmlt &data_f = edge.new_element("data"); - data_f.set_attribute("key", "originfile"); - data_f.data = id2string(graphml[from].file); - - xmlt &data_l = edge.new_element("data"); - data_l.set_attribute("key", "startline"); - data_l.data = id2string(graphml[from].line); - } - - if( - (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() && - it->ssa_full_lhs.is_not_nil()) - { - irep_idt identifier = it->ssa_lhs.get_object_name(); - - graphml[to].has_invariant = true; - code_assignt assign(it->ssa_lhs, it->ssa_rhs); - graphml[to].invariant = convert_assign_rec(identifier, assign); - graphml[to].invariant_scope = id2string(it->source.function_id); - } - - graphml[to].in[from].xml_node = edge; - graphml[from].out[to].xml_node = edge; - - break; - } - - case goto_trace_stept::typet::DECL: - case goto_trace_stept::typet::FUNCTION_CALL: - case goto_trace_stept::typet::FUNCTION_RETURN: - case goto_trace_stept::typet::LOCATION: - case goto_trace_stept::typet::ASSUME: - case goto_trace_stept::typet::INPUT: - case goto_trace_stept::typet::OUTPUT: - case goto_trace_stept::typet::SHARED_READ: - case goto_trace_stept::typet::SHARED_WRITE: - case goto_trace_stept::typet::MEMORY_BARRIER: - case goto_trace_stept::typet::ATOMIC_BEGIN: - case goto_trace_stept::typet::ATOMIC_END: - case goto_trace_stept::typet::DEAD: - case goto_trace_stept::typet::CONSTRAINT: - case goto_trace_stept::typet::NONE: - // ignore - break; - } - - it=next; - step_nr=next_step_nr; - } -} diff --git a/src/goto-programs/graphml_witness.h b/src/goto-programs/graphml_witness.h index 3192f00a73f..4ae3c34fb81 100644 --- a/src/goto-programs/graphml_witness.h +++ b/src/goto-programs/graphml_witness.h @@ -18,7 +18,6 @@ class code_assignt; class exprt; class goto_tracet; class namespacet; -class symex_target_equationt; class graphml_witnesst { @@ -29,7 +28,6 @@ class graphml_witnesst } void operator()(const goto_tracet &goto_trace); - void operator()(const symex_target_equationt &equation); const graphmlt &graph() { diff --git a/src/goto-programs/module_dependencies.txt b/src/goto-programs/module_dependencies.txt index ed04acda91c..88a577340b9 100644 --- a/src/goto-programs/module_dependencies.txt +++ b/src/goto-programs/module_dependencies.txt @@ -1,8 +1,6 @@ -analyses # dubious - concerns call_graph and does_remove_const ansi-c # for GraphML witnesses architecture # system goto-programs -goto-symex # dubious - spurious inclusion of symex_target_equation in graphml_witness json langapi # should go away linking diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 1be6140690e..e562e8528a3 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -24,9 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - #include "compute_called_functions.h" +#include "does_remove_const.h" #include "goto_model.h" #include "remove_const_function_pointers.h" #include "remove_skip.h" diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp index 05d9287e03c..2d7fcece875 100644 --- a/src/goto-programs/slice_global_inits.cpp +++ b/src/goto-programs/slice_global_inits.cpp @@ -17,9 +17,9 @@ Date: December 2016 #include #include -#include #include +#include "call_graph.h" #include "goto_functions.h" #include "goto_model.h" diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile index ec56bb5e12c..faff5dce1bf 100644 --- a/src/goto-symex/Makefile +++ b/src/goto-symex/Makefile @@ -39,6 +39,7 @@ SRC = auto_objects.cpp \ symex_start_thread.cpp \ symex_target.cpp \ symex_target_equation.cpp \ + symex_target_equation_graphml_witness.cpp \ symex_throw.cpp \ complexity_limiter.cpp \ # Empty last line diff --git a/src/goto-symex/symex_target_equation_graphml_witness.cpp b/src/goto-symex/symex_target_equation_graphml_witness.cpp new file mode 100644 index 00000000000..215f4adc3fd --- /dev/null +++ b/src/goto-symex/symex_target_equation_graphml_witness.cpp @@ -0,0 +1,314 @@ +/*******************************************************************\ + +Module: Witnesses for Symex Target Equations + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Witnesses for Symex Target Equations + +#include "symex_target_equation_graphml_witness.h" + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include +#include + +#include +#include +#include +#include + +static std::string +expr_to_string(const namespacet &ns, const irep_idt &id, const exprt &expr) +{ + if(get_mode_from_identifier(ns, id) == ID_C) + return expr2c(expr, ns, expr2c_configurationt::clean_configuration); + else + return from_expr(ns, id, expr); +} + +void symex_target_equation_graphml_witnesst::remove_l0_l1(exprt &expr) +{ + if(expr.id() == ID_symbol) + { + if(is_ssa_expr(expr)) + expr = to_ssa_expr(expr).get_original_expr(); + else + { + std::string identifier = id2string(to_symbol_expr(expr).get_identifier()); + + std::string::size_type l0_l1 = identifier.find_first_of("!@"); + if(l0_l1 != std::string::npos) + { + identifier.resize(l0_l1); + to_symbol_expr(expr).set_identifier(identifier); + } + } + + return; + } + else if(expr.id() == ID_string_constant) + { + std::string output_string = expr_to_string(ns, "", expr); + if(!xmlt::is_printable_xml(output_string)) + expr = to_string_constant(expr).to_array_expr(); + } + + Forall_operands(it, expr) + remove_l0_l1(*it); +} + +std::string symex_target_equation_graphml_witnesst::convert_assign_rec( + const irep_idt &identifier, + const code_assignt &assign) +{ + const auto cit = cache.find({identifier.get_no(), &assign.read()}); + if(cit != cache.end()) + return cit->second; + + std::string result; + + if(assign.rhs().id() == ID_array_list) + { + const array_list_exprt &array_list = to_array_list_expr(assign.rhs()); + const auto &ops = array_list.operands(); + + for(std::size_t listidx = 0; listidx != ops.size(); listidx += 2) + { + const index_exprt index{assign.lhs(), ops[listidx]}; + if(!result.empty()) + result += ' '; + result += + convert_assign_rec(identifier, code_assignt{index, ops[listidx + 1]}); + } + } + else if(assign.rhs().id() == ID_array) + { + const array_typet &type = to_array_type(assign.rhs().type()); + auto size_opt = numeric_cast(to_constant_expr(type.size())); + + if(size_opt.has_value()) + { + for(std::size_t i = 0; i < size_opt.value(); i++) + { + const index_exprt index{ + assign.lhs(), from_integer(i, signedbv_typet(32))}; + if(!result.empty()) + result += ' '; + result += convert_assign_rec( + identifier, + code_assignt{index, to_array_expr(assign.rhs()).operands()[i]}); + } + } + else + { + result = expr_to_string(ns, identifier, assign.lhs()) + '=' + + expr_to_string(ns, identifier, assign.rhs()) + ';'; + } + } + else if(assign.rhs().id() == ID_struct) + { + const struct_typet &type = to_struct_type(assign.rhs().type()); + const struct_exprt::operandst &operands = + to_struct_expr(assign.rhs()).operands(); + + std::size_t i = 0; + for(const auto &c : type.components()) + { + const member_exprt member{assign.lhs(), c.get_name(), c.type()}; + + if(!result.empty()) + result += ' '; + result += + convert_assign_rec(identifier, code_assignt{member, operands[i]}); + i++; + } + } + else if(assign.rhs().id() == ID_union) + { + const union_typet &type = to_union_type(assign.rhs().type()); + const union_exprt &union_expr = to_union_expr(assign.rhs()); + + for(const auto &c : type.components()) + { + if(c.get_name() == union_expr.get_component_name()) + { + const member_exprt member{assign.lhs(), c.get_name(), c.type()}; + result = + convert_assign_rec(identifier, code_assignt{member, union_expr.op()}); + break; + } + } + } + else + { + result = expr_to_string(ns, identifier, assign.lhs()) + '=' + + expr_to_string(ns, identifier, assign.rhs()) + ';'; + } + + cache.emplace(std::make_pair(identifier.get_no(), &assign.read()), result); + + return result; +} + +/// proof witness +void symex_target_equation_graphml_witnesst::operator()( + const symex_target_equationt &equation) +{ + graphml.key_values["sourcecodelang"] = "C"; + + const graphmlt::node_indext sink = graphml.add_node(); + graphml[sink].node_name = "sink"; + graphml[sink].is_violation = false; + graphml[sink].has_invariant = false; + + // step numbers start at 1 + std::vector step_to_node(equation.SSA_steps.size() + 1, 0); + + std::size_t step_nr = 1; + for(symex_target_equationt::SSA_stepst::const_iterator it = + equation.SSA_steps.begin(); + it != equation.SSA_steps.end(); + it++, step_nr++) // we cannot replace this by a ranged for + { + const source_locationt &source_location = it->source.pc->source_location(); + + if( + it->hidden || + (!it->is_assignment() && !it->is_goto() && !it->is_assert()) || + (it->is_goto() && it->source.pc->condition() == true) || + source_location.is_nil() || source_location.is_built_in() || + source_location.get_line().empty()) + { + step_to_node[step_nr] = sink; + + continue; + } + + // skip declarations followed by an immediate assignment + symex_target_equationt::SSA_stepst::const_iterator next = it; + ++next; + if( + next != equation.SSA_steps.end() && next->is_assignment() && + it->ssa_full_lhs == next->ssa_full_lhs && + it->source.pc->source_location() == next->source.pc->source_location()) + { + step_to_node[step_nr] = sink; + + continue; + } + + const graphmlt::node_indext node = graphml.add_node(); + graphml[node].node_name = std::to_string(it->source.pc->location_number) + + "." + std::to_string(step_nr); + graphml[node].file = source_location.get_file(); + graphml[node].line = source_location.get_line(); + graphml[node].is_violation = false; + graphml[node].has_invariant = false; + + step_to_node[step_nr] = node; + } + + // build edges + step_nr = 1; + for(symex_target_equationt::SSA_stepst::const_iterator it = + equation.SSA_steps.begin(); + it != equation.SSA_steps.end();) // no ++it + { + const std::size_t from = step_to_node[step_nr]; + + if(from == sink) + { + ++it; + ++step_nr; + continue; + } + + symex_target_equationt::SSA_stepst::const_iterator next = it; + std::size_t next_step_nr = step_nr; + for(++next, ++next_step_nr; next != equation.SSA_steps.end() && + (step_to_node[next_step_nr] == sink || + it->source.pc == next->source.pc); + ++next, ++next_step_nr) + { + // advance + } + const std::size_t to = + next == equation.SSA_steps.end() ? sink : step_to_node[next_step_nr]; + + switch(it->type) + { + case goto_trace_stept::typet::ASSIGNMENT: + case goto_trace_stept::typet::ASSERT: + case goto_trace_stept::typet::GOTO: + case goto_trace_stept::typet::SPAWN: + { + xmlt edge( + "edge", + {{"source", graphml[from].node_name}, + {"target", graphml[to].node_name}}, + {}); + + { + xmlt &data_f = edge.new_element("data"); + data_f.set_attribute("key", "originfile"); + data_f.data = id2string(graphml[from].file); + + xmlt &data_l = edge.new_element("data"); + data_l.set_attribute("key", "startline"); + data_l.data = id2string(graphml[from].line); + } + + if( + (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() && + it->ssa_full_lhs.is_not_nil()) + { + irep_idt identifier = it->ssa_lhs.get_object_name(); + + graphml[to].has_invariant = true; + code_assignt assign(it->ssa_lhs, it->ssa_rhs); + graphml[to].invariant = convert_assign_rec(identifier, assign); + graphml[to].invariant_scope = id2string(it->source.function_id); + } + + graphml[to].in[from].xml_node = edge; + graphml[from].out[to].xml_node = edge; + + break; + } + + case goto_trace_stept::typet::DECL: + case goto_trace_stept::typet::FUNCTION_CALL: + case goto_trace_stept::typet::FUNCTION_RETURN: + case goto_trace_stept::typet::LOCATION: + case goto_trace_stept::typet::ASSUME: + case goto_trace_stept::typet::INPUT: + case goto_trace_stept::typet::OUTPUT: + case goto_trace_stept::typet::SHARED_READ: + case goto_trace_stept::typet::SHARED_WRITE: + case goto_trace_stept::typet::MEMORY_BARRIER: + case goto_trace_stept::typet::ATOMIC_BEGIN: + case goto_trace_stept::typet::ATOMIC_END: + case goto_trace_stept::typet::DEAD: + case goto_trace_stept::typet::CONSTRAINT: + case goto_trace_stept::typet::NONE: + // ignore + break; + } + + it = next; + step_nr = next_step_nr; + } +} diff --git a/src/goto-symex/symex_target_equation_graphml_witness.h b/src/goto-symex/symex_target_equation_graphml_witness.h new file mode 100644 index 00000000000..cf2338c5273 --- /dev/null +++ b/src/goto-symex/symex_target_equation_graphml_witness.h @@ -0,0 +1,71 @@ +/*******************************************************************\ + +Module: Witnesses for Symex Target Equations + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Witnesses for Symex Target Equations + +#ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_GRAPHML_WITNESS_H +#define CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_GRAPHML_WITNESS_H + +#include + +class code_assignt; +class exprt; +class namespacet; +class symex_target_equationt; + +/// Create a GraphML witness for a symex target equation +class symex_target_equation_graphml_witnesst +{ +public: + explicit symex_target_equation_graphml_witnesst(const namespacet &_ns) + : ns(_ns) + { + } + + void operator()(const symex_target_equationt &equation); + + const graphmlt &graph() + { + return graphml; + } + +protected: + const namespacet &ns; + graphmlt graphml; + + void remove_l0_l1(exprt &expr); + std::string + convert_assign_rec(const irep_idt &identifier, const code_assignt &assign); + + template + static void hash_combine(std::size_t &seed, const T &v) + { + std::hash hasher; + seed ^= hasher(v) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + } + + template + struct pair_hash // NOLINT(readability/identifiers) + { + std::size_t operator()(const std::pair &v) const + { + std::size_t seed = 0; + hash_combine(seed, v.first); + hash_combine(seed, v.second); + return seed; + } + }; + std::unordered_map< + std::pair, + std::string, + pair_hash> + cache; +}; + +#endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_GRAPHML_WITNESS_H diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp index d72b32ae765..b556fd703f6 100644 --- a/unit/analyses/call_graph.cpp +++ b/unit/analyses/call_graph.cpp @@ -8,10 +8,10 @@ Module: Unit test for call graph generation #include +#include +#include #include -#include -#include #include #include #include diff --git a/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp b/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp index b33b9b13258..326ea48c942 100644 --- a/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp +++ b/unit/analyses/disconnect_unreachable_nodes_in_graph.cpp @@ -8,9 +8,9 @@ Module: Unit test for graph class functions #include +#include #include -#include #include #include #include diff --git a/unit/analyses/does_remove_const/does_expr_lose_const.cpp b/unit/analyses/does_remove_const/does_expr_lose_const.cpp index 91b48bb592d..4b5a85b33b7 100644 --- a/unit/analyses/does_remove_const/does_expr_lose_const.cpp +++ b/unit/analyses/does_remove_const/does_expr_lose_const.cpp @@ -16,9 +16,9 @@ Author: Diffblue Ltd. #include #include +#include #include -#include #include #include #include diff --git a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp index 6dde902a93d..033b27aa550 100644 --- a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp +++ b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp @@ -9,19 +9,17 @@ Author: Diffblue Ltd. /// \file /// Does Remove Const Unit Tests -#include - #include #include #include #include -#include - +#include #include #include -#include +#include +#include SCENARIO("does_type_preserve_const_correctness", "[core][analyses][does_remove_const][does_type_preserve_const_correctness]") diff --git a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp index 0771edf69e9..cbc444131a5 100644 --- a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp +++ b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp @@ -9,19 +9,17 @@ Author: Diffblue Ltd. /// \file /// Does Remove Const Unit Tests -#include - #include #include #include #include -#include - +#include #include #include -#include +#include +#include SCENARIO("is_type_at_least_as_const", "[core][analyses][does_remove_const][is_type_at_least_as_const]")