Merge pull request #747 from tautschnig/undefined-function-assume-false

goto-instrument: Replace calls to undefined functions by assume(false)

Author: kroening

CHANGELOG

@@ -1,3 +1,12 @@
+5.8
+===
+
+* GOTO-INSTRUMENT: New option --list-calls-args
+* GOTO-INSTRUMENT: New option --print-path-lenghts
+* GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions
+* GOTO-INSTRUMENT: New option --undefined-function-is-assume-false
+
+
 5.7
 ===
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -265,6 +265,54 @@ int goto_analyzer_parse_optionst::doit()
     return 0;
   }
 
+  if(cmdline.isset("unreachable-functions"))
+  {
+    const std::string json_file=cmdline.get_value("json");
+
+    if(json_file.empty())
+      unreachable_functions(goto_model, false, std::cout);
+    else if(json_file=="-")
+      unreachable_functions(goto_model, true, std::cout);
+    else
+    {
+      std::ofstream ofs(json_file);
+      if(!ofs)
+      {
+        error() << "Failed to open json output `"
+                << json_file << "'" << eom;
+        return 6;
+      }
+
+      unreachable_functions(goto_model, true, ofs);
+    }
+
+    return 0;
+  }
+
+  if(cmdline.isset("reachable-functions"))
+  {
+    const std::string json_file=cmdline.get_value("json");
+
+    if(json_file.empty())
+      reachable_functions(goto_model, false, std::cout);
+    else if(json_file=="-")
+      reachable_functions(goto_model, true, std::cout);
+    else
+    {
+      std::ofstream ofs(json_file);
+      if(!ofs)
+      {
+        error() << "Failed to open json output `"
+                << json_file << "'" << eom;
+        return 6;
+      }
+
+      reachable_functions(goto_model, true, ofs);
+    }
+
+    return 0;
+  }
+
   if(cmdline.isset("show-local-may-alias"))
   {
     namespacet ns(goto_model.symbol_table);
@@ -489,6 +537,10 @@ void goto_analyzer_parse_optionst::help()
     // NOLINTNEXTLINE(whitespace/line_length)
     " --taint file_name            perform taint analysis using rules in given file\n"
     " --unreachable-instructions   list dead code\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --unreachable-functions      list functions unreachable from the entry point\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --reachable-functions        list functions reachable from the entry point\n"
     " --intervals                  interval analysis\n"
     " --non-null                   non-null analysis\n"
     "\n"

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -36,7 +36,8 @@ class optionst;
   "(taint):(show-taint)" \
   "(show-local-may-alias)" \
   "(json):(xml):" \
-  "(unreachable-instructions)" \
+  "(unreachable-instructions)(unreachable-functions)" \
+  "(reachable-functions)" \
   "(intervals)(show-intervals)" \
   "(non-null)(show-non-null)"
 

src/goto-analyzer/unreachable_instructions.cpp

@@ -198,7 +198,12 @@ void unreachable_instructions(
     const goto_programt &goto_program=f_it->second.body;
     dead_mapt dead_map;
 
-    if(called.find(f_it->first)!=called.end())
+    const symbolt &decl=ns.lookup(f_it->first);
+
+    // f_it->first may be a link-time renamed version, use the
+    // base_name instead; do not list inlined functions
+    if(called.find(decl.base_name)!=called.end() ||
+       f_it->second.is_inlined())
       unreachable_instructions(goto_program, dead_map);
     else
       all_unreachable(goto_program, dead_map);
@@ -215,3 +220,150 @@ void unreachable_instructions(
   if(json && !json_result.array.empty())
     os << json_result << std::endl;
 }
+
+/*******************************************************************\
+
+Function: json_output_function
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void json_output_function(
+  const irep_idt &function,
+  const source_locationt &first_location,
+  const source_locationt &last_location,
+  json_arrayt &dest)
+{
+  json_objectt &entry=dest.push_back().make_object();
+
+  entry["function"]=json_stringt(id2string(function));
+  entry["file name"]=
+    json_stringt(concat_dir_file(
+        id2string(first_location.get_working_directory()),
+        id2string(first_location.get_file())));
+  entry["first line"]=
+    json_numbert(id2string(first_location.get_line()));
+  entry["last line"]=
+    json_numbert(id2string(last_location.get_line()));
+}
+
+/*******************************************************************\
+
+Function: list_functions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void list_functions(
+  const goto_modelt &goto_model,
+  const bool json,
+  std::ostream &os,
+  bool unreachable)
+{
+  json_arrayt json_result;
+
+  std::set<irep_idt> called;
+  compute_called_functions(goto_model, called);
+
+  const namespacet ns(goto_model.symbol_table);
+
+  forall_goto_functions(f_it, goto_model.goto_functions)
+  {
+    const symbolt &decl=ns.lookup(f_it->first);
+
+    // f_it->first may be a link-time renamed version, use the
+    // base_name instead; do not list inlined functions
+    if(unreachable ==
+       (called.find(decl.base_name)!=called.end() ||
+        f_it->second.is_inlined()))
+      continue;
+
+    source_locationt first_location=decl.location;
+
+    source_locationt last_location;
+    if(f_it->second.body_available())
+    {
+      const goto_programt &goto_program=f_it->second.body;
+
+      goto_programt::const_targett end_function=
+        goto_program.instructions.end();
+      --end_function;
+      assert(end_function->is_end_function());
+      last_location=end_function->source_location;
+    }
+    else
+      // completely ignore functions without a body, both for
+      // reachable and unreachable functions; we could also restrict
+      // this to macros/asm renaming
+      continue;
+
+    if(!json)
+    {
+      os << concat_dir_file(
+              id2string(first_location.get_working_directory()),
+              id2string(first_location.get_file())) << " "
+         << decl.base_name << " "
+         << first_location.get_line() << " "
+         << last_location.get_line() << "\n";
+    }
+    else
+      json_output_function(
+        decl.base_name,
+        first_location,
+        last_location,
+        json_result);
+  }
+
+  if(json && !json_result.array.empty())
+    os << json_result << std::endl;
+}
+
+/*******************************************************************\
+
+Function: unreachable_functions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void unreachable_functions(
+  const goto_modelt &goto_model,
+  const bool json,
+  std::ostream &os)
+{
+  list_functions(goto_model, json, os, true);
+}
+
+/*******************************************************************\
+
+Function: reachable_functions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void reachable_functions(
+  const goto_modelt &goto_model,
+  const bool json,
+  std::ostream &os)
+{
+  list_functions(goto_model, json, os, false);
+}

src/goto-analyzer/unreachable_instructions.h

@@ -20,4 +20,14 @@ void unreachable_instructions(
   const bool json,
   std::ostream &os);
 
+void unreachable_functions(
+  const goto_modelt &,
+  const bool json,
+  std::ostream &os);
+
+void reachable_functions(
+  const goto_modelt &,
+  const bool json,
+  std::ostream &os);
+
 #endif // CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H

src/goto-instrument/Makefile

@@ -23,7 +23,8 @@ SRC = goto_instrument_parse_options.cpp rw_set.cpp \
       wmm/event_graph.cpp wmm/pair_collection.cpp \
       goto_instrument_main.cpp horn_encoding.cpp \
       thread_instrumentation.cpp skip_loops.cpp loop_utils.cpp \
-      code_contracts.cpp cover.cpp model_argc_argv.cpp
+      code_contracts.cpp cover.cpp model_argc_argv.cpp \
+      undefined_functions.cpp
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \

src/goto-instrument/call_sequences.cpp

@@ -13,6 +13,7 @@ Date: April 2013
 #include <unordered_set>
 
 #include <util/std_expr.h>
+#include <util/simplify_expr.h>
 
 #include "call_sequences.h"
 
@@ -358,3 +359,83 @@ void check_call_sequence(const goto_functionst &goto_functions)
 
   check_call_sequencet(goto_functions, sequence)();
 }
+
+/*******************************************************************\
+
+Function: list_calls_and_arguments
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void list_calls_and_arguments(
+  const namespacet &ns,
+  const irep_idt &function,
+  const goto_programt &goto_program)
+{
+  forall_goto_program_instructions(i_it, goto_program)
+  {
+    if(!i_it->is_function_call())
+      continue;
+
+    const code_function_callt call=to_code_function_call(i_it->code);
+
+    const exprt &f=call.function();
+
+    if(f.id()!=ID_symbol)
+      continue;
+
+    const irep_idt &identifier=to_symbol_expr(f).get_identifier();
+    if(identifier=="__CPROVER_initialize")
+      continue;
+
+    std::string name=from_expr(ns, identifier, f);
+    std::string::size_type java_type_suffix=name.find(":(");
+    if(java_type_suffix!=std::string::npos)
+      name.erase(java_type_suffix);
+
+    std::cout << "found call to " << name;
+
+    if(!call.arguments().empty())
+    {
+      std::cout << " with arguments ";
+      for(exprt::operandst::const_iterator
+          it=call.arguments().begin();
+          it!=call.arguments().end();
+          ++it)
+      {
+        if(it!=call.arguments().begin())
+          std::cout << ", ";
+        std::cout << from_expr(ns, identifier, simplify_expr(*it, ns));
+      }
+    }
+
+    std::cout << '\n';
+  }
+}
+
+/*******************************************************************\
+
+Function: show_call_sequences
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void list_calls_and_arguments(
+  const namespacet &ns,
+  const goto_functionst &goto_functions)
+{
+  // do per function
+
+  forall_goto_functions(f_it, goto_functions)
+    list_calls_and_arguments(ns, f_it->first, f_it->second.body);
+}

src/goto-instrument/call_sequences.h

@@ -16,4 +16,8 @@ Date: September 2011
 void show_call_sequences(const goto_functionst &goto_functions);
 void check_call_sequence(const goto_functionst &goto_functions);
 
+void list_calls_and_arguments(
+  const namespacet &ns,
+  const goto_functionst &goto_functions);
+
 #endif // CPROVER_GOTO_INSTRUMENT_CALL_SEQUENCES_H