Remove dubious module dependencies in goto-programs

src/goto-checker/bmc_util.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, Peter Schrammel
 #include <goto-symex/memory_model_pso.h>
 #include <goto-symex/slice.h>
 #include <goto-symex/symex_target_equation.h>
+#include <goto-symex/symex_target_equation_graphml_witness.h>
 #include <solvers/decision_procedure.h>
 
 #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 == "-")

src/goto-instrument/aggressive_slicer.cpp

@@ -13,13 +13,12 @@ Author: Elizabeth Polgreen, elizabeth.polgreen@cs.ox.ac.uk
 
 #include <util/message.h>
 
+#include <goto-programs/call_graph_helpers.h>
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_properties.h>
 
 #include <linking/static_lifetime_init.h>
 
-#include <analyses/call_graph_helpers.h>
-
 #include "remove_function.h"
 
 void aggressive_slicert::note_functions_to_keep(

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 <list>
-#include <string>
-
 #include <util/irep.h>
 
-#include <analyses/call_graph.h>
-
+#include <goto-programs/call_graph.h>
 #include <goto-programs/goto_model.h>
 
+#include <list>
+#include <string>
+
 class message_handlert;
 
 /// \brief The aggressive slicer removes the body of all the functions except

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/unicode.h>
 #include <util/version.h>
 
+#include <goto-programs/call_graph.h>
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/ensure_one_backedge_per_target.h>
 #include <goto-programs/goto_check.h>
@@ -47,7 +48,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/write_goto_binary.h>
 
-#include <analyses/call_graph.h>
 #include <analyses/constant_propagator.h>
 #include <analyses/custom_bitvector_analysis.h>
 #include <analyses/dependence_graph.h>

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)

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 \

src/analyses/call_graph.cpp → src/goto-programs/call_graph.cpp

@@ -13,22 +13,22 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/xml.h>
 
-#include <goto-programs/goto_model.h>
+#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)
 {
 }
 
 /// Create complete call graph
 /// \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<irep_idt, std::vector<irep_idt>> 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<irep_idt, node_indext> 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 << "<!-- XML call-graph representation does not document callsites yet."
-      " If you need this, edit call_grapht::output_xml -->\n";
+           " If you need this, edit call_grapht::output_xml -->\n";
   for(const auto &edge : edges)
   {
     out << "<call_graph_edge caller=\"";
@@ -299,8 +290,8 @@ void call_grapht::output_xml(std::ostream &out) const
 std::optional<std::size_t>
 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<node_indext>();
   else
     return findit->second;

src/analyses/call_graph.h → 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 <util/graph.h>
+
+#include "goto_program.h"
 
 #include <iosfwd>
 #include <map>
 #include <unordered_set>
 
-#include <util/graph.h>
-
-#include <goto-programs/goto_program.h>
-
 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

src/analyses/call_graph_helpers.cpp → src/goto-programs/call_graph_helpers.cpp

@@ -28,14 +28,14 @@ static std::set<irep_idt> get_neighbours(
   return result;
 }
 
-std::set<irep_idt> get_callees(
-  const call_grapht::directed_grapht &graph, const irep_idt &function)
+std::set<irep_idt>
+get_callees(const call_grapht::directed_grapht &graph, const irep_idt &function)
 {
   return get_neighbours(graph, function, true);
 }
 
-std::set<irep_idt> get_callers(
-  const call_grapht::directed_grapht &graph, const irep_idt &function)
+std::set<irep_idt>
+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<irep_idt> get_connected_functions(
 }
 
 std::set<irep_idt> 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<irep_idt> 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);
 }