Merge pull request diffblue#259 from diffblue/smowton/feature/virtual_callsite_specialiser

Add CSVSA and its specializer

Author: smowton

.travis.yml

@@ -92,7 +92,8 @@ jobs:
       before_install:
           #we create symlink to non-ccache gcc, to be used in tests
         - mkdir bin ; ln -s /usr/bin/gcc bin/gcc
-        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache ant python3
+        - HOMEBREW_NO_AUTO_UPDATE=1 brew tap discoteq/discoteq # for flock
+        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache ant python3 flock
         - pip3 install -q pytest --user
         - export PATH=$HOME/.local/bin:/usr/local/opt/ccache/libexec:$PATH
       env:
@@ -108,7 +109,8 @@ jobs:
       compiler: clang
       cache: ccache
       before_install:
-        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache ant python3
+        - HOMEBREW_NO_AUTO_UPDATE=1 brew tap discoteq/discoteq # for flock
+        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache ant python3 flock
         - pip3 install -q pytest --user
         - export PATH=$HOME/.local/bin:/usr/local/opt/ccache/libexec:$PATH
       env:

cbmc/src/analyses/call_graph.cpp

@@ -42,8 +42,10 @@ call_grapht::call_grapht(
 {
   forall_goto_functions(f_it, goto_functions)
   {
-    const goto_programt &body=f_it->second.body;
-    add(f_it->first, body);
+    const irep_idt &function_name = f_it->first;
+    const goto_programt &body = f_it->second.body;
+    nodes.insert(function_name);
+    add(function_name, body);
   }
 }
 
@@ -85,12 +87,14 @@ call_grapht::call_grapht(
     const goto_programt &goto_program=
       goto_functions.function_map.at(function).body;
 
+    nodes.insert(function);
+
     forall_callsites(
       goto_program,
       [&](goto_programt::const_targett i_it, const irep_idt &callee)
       {
         add(function, callee, i_it);
-        if(graph.find(callee)==graph.end())
+        if(edges.find(callee)==edges.end())
           pending_stack.push(callee);
       }
     ); // NOLINT
@@ -130,7 +134,9 @@ void call_grapht::add(
   const irep_idt &caller,
   const irep_idt &callee)
 {
-  graph.insert(std::pair<irep_idt, irep_idt>(caller, callee));
+  edges.insert({caller, callee});
+  nodes.insert(caller);
+  nodes.insert(callee);
 }
 
 /// Add edge with optional callsite information
@@ -153,7 +159,8 @@ void call_grapht::add(
 call_grapht call_grapht::get_inverted() const
 {
   call_grapht result;
-  for(const auto &caller_callee : graph)
+  result.nodes = nodes;
+  for(const auto &caller_callee : edges)
     result.add(caller_callee.second, caller_callee.first);
   return result;
 }
@@ -198,7 +205,12 @@ call_grapht::directed_grapht call_grapht::get_directed_graph() const
   call_grapht::directed_grapht ret;
   function_indicest function_indices(ret);
 
-  for(const auto &edge : graph)
+  // To make sure we include unreachable functions we first create indices
+  // for all nodes in the graph
+  for(const irep_idt &function_name : nodes)
+    function_indices[function_name];
+
+  for(const auto &edge : edges)
   {
     auto a_index=function_indices[edge.first];
     auto b_index=function_indices[edge.second];
@@ -238,7 +250,7 @@ void call_grapht::output_dot(std::ostream &out) const
 {
   out << "digraph call_graph {\n";
 
-  for(const auto &edge : graph)
+  for(const auto &edge : edges)
   {
     out << "  \"" << edge.first << "\" -> "
         << "\"" << edge.second << "\" "
@@ -253,7 +265,7 @@ void call_grapht::output_dot(std::ostream &out) const
 
 void call_grapht::output(std::ostream &out) const
 {
-  for(const auto &edge : graph)
+  for(const auto &edge : edges)
   {
     out << edge.first << " -> " << edge.second << "\n";
     if(collect_callsites)
@@ -268,7 +280,7 @@ void call_grapht::output_xml(std::ostream &out) const
   if(collect_callsites)
     out << "<!-- XML call-graph representation does not document callsites yet."
       " If you need this, edit call_grapht::output_xml -->\n";
-  for(const auto &edge : graph)
+  for(const auto &edge : edges)
   {
     out << "<call_graph_edge caller=\"";
     xmlt::escape_attribute(id2string(edge.first), out);
@@ -297,7 +309,7 @@ void find_leaves_below_function(
   if(to_avoid.count(function)!=0UL)
     return;
   to_avoid.insert(function);
-  const auto range = call_graph.graph.equal_range(function);
+  const auto range = call_graph.edges.equal_range(function);
   if(range.first==range.second)
     output.insert(function);
   else
@@ -344,7 +356,7 @@ void find_nearest_common_callees(
   }
 
   std::map<irep_idt, std::size_t> counting;
-  for(const auto &elem : call_graph.graph)
+  for(const auto &elem : call_graph.edges)
   {
     counting[elem.first]=0U;
     counting[elem.second]=0U;
@@ -362,7 +374,7 @@ void find_nearest_common_callees(
   for(const auto &elem : counting)
     if(elem.second!=0U)
     {
-      const auto range = call_graph.graph.equal_range(elem.first);
+      const auto range = call_graph.edges.equal_range(elem.first);
       if(range.first==range.second)
         leaves.insert(elem.first);
     }
@@ -372,7 +384,7 @@ void find_nearest_common_callees(
       output.insert(elem.first);
     else if(elem.second!=0U && elem.second<functions.size())
     {
-      const auto range = call_graph.graph.equal_range(elem.first);
+      const auto range = call_graph.edges.equal_range(elem.first);
       for(auto it=range.first; it!=range.second; ++it)
       {
         auto cit=counting.find(it->second);
@@ -393,7 +405,7 @@ bool exists_direct_call(
   const irep_idt &callee)
 {
   const auto range =
-    call_graph.graph.equal_range(caller);
+    call_graph.edges.equal_range(caller);
   for(auto it=range.first; it!=range.second; ++it)
     if(callee==it->second)
       return true;
@@ -420,7 +432,7 @@ bool exists_direct_or_indirect_call(
   if(exists_direct_call(call_graph, caller, callee))
     return ignored_functions.count(callee)==0UL;
   const auto range =
-    call_graph.graph.equal_range(caller);
+    call_graph.edges.equal_range(caller);
   for(auto it=range.first; it!=range.second; ++it)
     if(exists_direct_or_indirect_call(
          call_graph,

cbmc/src/analyses/call_graph.h

@@ -63,13 +63,17 @@ class call_grapht
   void output(std::ostream &out) const;
   void output_xml(std::ostream &out) const;
 
-  /// Type of the call graph. Note parallel edges (e.g. A having two callsites
-  /// both targeting B) result in multiple graph edges.
-  typedef std::multimap<irep_idt, irep_idt> grapht;
+  /// Type of the nodes in the call graph.
+  typedef std::unordered_set<irep_idt, irep_id_hash> nodest;
 
-  /// Type of a call graph edge in `grapht`
+  /// Type of the edges in the call graph. Note parallel edges (e.g. A having
+  /// two callsites both targeting B) result in multiple graph edges.
+  typedef std::multimap<irep_idt, irep_idt> edgest;
+
+  /// Type of a call graph edge in `edgest`
   typedef std::pair<irep_idt, irep_idt> edget;
 
+
   /// Type of a callsite stored in member `callsites`
   typedef goto_programt::const_targett locationt;
 
@@ -85,7 +89,8 @@ class call_grapht
   /// backward compatibility; use `get_directed_graph()` to get a generic
   /// directed graph representation that provides more graph algorithms
   /// (shortest path, SCCs and so on).
-  grapht graph;
+  edgest edges;
+  nodest nodes;
 
   /// Map from call-graph edges to a set of callsites that make the given call.
   callsitest callsites;

cbmc/src/analyses/static_analysis.h

@@ -92,6 +92,9 @@ class domain_baset
   // this computes the join between "this" and "b"
   // return true if "this" has changed
 
+  bool has_been_seen() const { return seen; }
+  void set_seen() { seen=true; }
+
 protected:
   bool seen;
 
@@ -282,7 +285,7 @@ class static_analysis_baset
   virtual void generate_state(locationt l)=0;
   virtual statet &get_state(locationt l)=0;
   virtual const statet &get_state(locationt l) const=0;
-  virtual std::unique_ptr<statet> make_temporary_state(statet &s)=0;
+  virtual std::unique_ptr<statet> make_temporary_state(const statet &s)=0;
 
   typedef domain_baset::expr_sett expr_sett;
 
@@ -364,9 +367,9 @@ class static_analysist:public static_analysis_baset
     return static_cast<T &>(a).merge(static_cast<const T &>(b), to);
   }
 
-  virtual std::unique_ptr<statet> make_temporary_state(statet &s)
+  virtual std::unique_ptr<statet> make_temporary_state(const statet &s)
   {
-    return util_make_unique<T>(static_cast<T &>(s));
+    return util_make_unique<T>(static_cast<const T &>(s));
   }
 
   virtual void generate_state(locationt l)

cbmc/src/goto-programs/dead_code_elimination.cpp

@@ -0,0 +1,76 @@
+/*******************************************************************\
+
+Module: Dead code elimination
+
+Author: Chris Smowton, [email protected]
+
+Date:   March 2018
+
+\*******************************************************************/
+
+/// \file
+/// Dead code elimination
+
+#include "dead_code_elimination.h"
+
+/// Replace all unreachable instructions in a program with SKIPs
+/// \param goto_program: program to process
+static void remove_dead_code(goto_programt &goto_program)
+{
+  std::unordered_set<unsigned> live_location_numbers;
+
+  if(goto_program.empty())
+    return;
+
+  // Mark live locations:
+  std::vector<goto_programt::const_targett> worklist;
+  worklist.push_back(goto_program.instructions.begin());
+
+  while(!worklist.empty())
+  {
+    goto_programt::const_targett next_instruction = worklist.back();
+    worklist.pop_back();
+
+    auto insert_result =
+      live_location_numbers.insert(next_instruction->location_number);
+    // Already marked live?
+    if(!insert_result.second)
+      continue;
+
+    for(auto &target : next_instruction->targets)
+    {
+      if(!live_location_numbers.count(target->location_number))
+        worklist.push_back(target);
+    }
+
+    bool may_fall_through =
+      next_instruction->type != END_FUNCTION &&
+      (next_instruction->targets.empty() ||
+       (next_instruction->type == GOTO && !next_instruction->guard.is_true()));
+
+    if(may_fall_through)
+    {
+      auto successor = std::next(next_instruction);
+      if(!live_location_numbers.count(successor->location_number))
+        worklist.push_back(successor);
+    }
+  }
+
+  // Kill locations not marked:
+  for(auto &instruction : goto_program.instructions)
+  {
+    if(instruction.type != END_FUNCTION &&
+       !live_location_numbers.count(instruction.location_number))
+    {
+      instruction.make_skip();
+    }
+  }
+}
+
+/// Replace all unreachable instructions in a model's function map with SKIPs
+/// \param goto_model: model to process
+void remove_dead_code(goto_modelt &goto_model)
+{
+  for(auto &id_and_function : goto_model.goto_functions.function_map)
+    remove_dead_code(id_and_function.second.body);
+}

cbmc/src/goto-programs/dead_code_elimination.h

@@ -0,0 +1,19 @@
+/*******************************************************************\
+
+Module: Remove dead code (function-local)
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+/// \file
+/// Remove dead code (function-local)
+
+#ifndef CPROVER_GOTO_PROGRAMS_DEAD_CODE_ELIMINATION_H
+#define CPROVER_GOTO_PROGRAMS_DEAD_CODE_ELIMINATION_H
+
+#include <goto-programs/goto_model.h>
+
+void remove_dead_code(goto_modelt &goto_model);
+
+#endif