Show properties in goto-diff

Shows properties for each new/modified/deleted function.
For now, for modified functions all properties are shown
regardless of whether they are affected by the
modification or not.

src/goto-diff/goto_diff.h

@@ -19,43 +19,57 @@ Author: Peter Schrammel
 
 #include <ostream>
 
+class optionst;
+
 class goto_difft:public messaget
 {
 public:
-  explicit goto_difft(
+  goto_difft(
     const goto_modelt &_goto_model1,
     const goto_modelt &_goto_model2,
-    message_handlert &_message_handler
-    )
-    :
-    messaget(_message_handler),
-    goto_model1(_goto_model1),
-    goto_model2(_goto_model2),
-    ui(ui_message_handlert::uit::PLAIN),
-    total_functions_count(0)
-     {}
+    const optionst &_options,
+    message_handlert &_message_handler)
+    : messaget(_message_handler),
+      goto_model1(_goto_model1),
+      goto_model2(_goto_model2),
+      options(_options),
+      ui(ui_message_handlert::uit::PLAIN),
+      total_functions_count(0)
+  {
+  }
 
   virtual bool operator()()=0;
 
   void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
 
-  virtual std::ostream &output_functions(std::ostream &out) const;
+  virtual void output_functions() const;
 
 protected:
   const goto_modelt &goto_model1;
   const goto_modelt &goto_model2;
+  const optionst &options;
   ui_message_handlert::uit ui;
 
   unsigned total_functions_count;
   typedef std::set<irep_idt> irep_id_sett;
   irep_id_sett new_functions, modified_functions, deleted_functions;
 
-  void convert_function_group(
+  void output_function_group(
+    const std::string &group_name,
+    const irep_id_sett &function_group,
+    const goto_modelt &goto_model) const;
+  void output_function(
+    const irep_idt &function_name,
+    const goto_modelt &goto_model) const;
+
+  void convert_function_group_json(
     json_arrayt &result,
-    const irep_id_sett &function_group) const;
-  void convert_function(
+    const irep_id_sett &function_group,
+    const goto_modelt &goto_model) const;
+  void convert_function_json(
     json_objectt &result,
-    const irep_idt &function_name) const;
+    const irep_idt &function_name,
+    const goto_modelt &goto_model) const;
 };
 
 #endif // CPROVER_GOTO_DIFF_GOTO_DIFF_H

src/goto-diff/goto_diff_base.cpp

@@ -11,95 +11,142 @@ Author: Peter Schrammel
 
 #include "goto_diff.h"
 
+#include <goto-programs/show_properties.h>
+
 #include <util/json_expr.h>
+#include <util/options.h>
 
-std::ostream &goto_difft::output_functions(std::ostream &out) const
+/// Output diff result
+void goto_difft::output_functions() const
 {
-  namespacet ns1(goto_model1.symbol_table);
-  namespacet ns2(goto_model2.symbol_table);
   switch(ui)
   {
     case ui_message_handlert::uit::PLAIN:
     {
-      out << "total number of functions: " << total_functions_count << "\n";
-      out << "new functions:\n";
-      for(irep_id_sett::const_iterator it=new_functions.begin();
-          it!=new_functions.end(); ++it)
-      {
-        const symbolt &symbol = ns2.lookup(*it);
-        out << "  " << symbol.location.get_file() << ": " << *it << "\n";
-      }
-
-      out << "modified functions:\n";
-      for(irep_id_sett::const_iterator it=modified_functions.begin();
-          it!=modified_functions.end(); ++it)
-      {
-        const symbolt &symbol = ns2.lookup(*it);
-        out << "  " << symbol.location.get_file() << ": " << *it << "\n";
-      }
-
-      out << "deleted functions:\n";
-      for(irep_id_sett::const_iterator it=deleted_functions.begin();
-          it!=deleted_functions.end(); ++it)
-      {
-        const symbolt &symbol = ns1.lookup(*it);
-        out << "  " << symbol.location.get_file() << ": " << *it << "\n";
-      }
+      result() << "total number of functions: " << total_functions_count
+               << '\n';
+      output_function_group("new functions", new_functions, goto_model2);
+      output_function_group(
+        "modified functions", modified_functions, goto_model2);
+      output_function_group(
+        "deleted functions", deleted_functions, goto_model1);
+      result() << eom;
       break;
     }
     case ui_message_handlert::uit::JSON_UI:
     {
       json_objectt json_result;
       json_result["totalNumberOfFunctions"]=
         json_stringt(std::to_string(total_functions_count));
-      convert_function_group
-        (json_result["newFunctions"].make_array(), new_functions);
-      convert_function_group(
-        json_result["modifiedFunctions"].make_array(), modified_functions);
-      convert_function_group(
-        json_result["deletedFunctions"].make_array(), deleted_functions);
-      out << ",\n" << json_result;
+      convert_function_group_json(
+        json_result["newFunctions"].make_array(), new_functions, goto_model2);
+      convert_function_group_json(
+        json_result["modifiedFunctions"].make_array(),
+        modified_functions,
+        goto_model2);
+      convert_function_group_json(
+        json_result["deletedFunctions"].make_array(),
+        deleted_functions,
+        goto_model1);
+      result() << json_result;
       break;
     }
     case ui_message_handlert::uit::XML_UI:
     {
-      out << "not supported yet";
+      error() << "XML output not supported yet" << eom;
     }
   }
-  return out;
 }
 
-void goto_difft::convert_function_group(
-  json_arrayt &result,
-  const irep_id_sett &function_group) const
+/// Output group of functions in plain text format
+/// \param group_name: the name of the group, e.g. "modified functions"
+/// \param function_group: set of function ids in the group
+/// \param goto_model: the goto model
+void goto_difft::output_function_group(
+  const std::string &group_name,
+  const irep_id_sett &function_group,
+  const goto_modelt &goto_model) const
 {
-  for(irep_id_sett::const_iterator it=function_group.begin();
-      it!=function_group.end(); ++it)
+  result() << group_name << ":\n";
+  for(const auto &function_name : function_group)
   {
-    convert_function(result.push_back(jsont()).make_object(), *it);
+    output_function(function_name, goto_model);
   }
 }
 
-void goto_difft::convert_function(
-  json_objectt &result,
-  const irep_idt &function_name) const
+/// Output function information in plain text format
+/// \param function_name: the function id
+/// \param goto_model: the goto model
+void goto_difft::output_function(
+  const irep_idt &function_name,
+  const goto_modelt &goto_model) const
+{
+  namespacet ns(goto_model.symbol_table);
+  const symbolt &symbol = ns.lookup(function_name);
+
+  result() << "  " << symbol.location.get_file() << ": " << function_name
+           << '\n';
+
+  if(options.get_bool_option("show-properties"))
+  {
+    const auto goto_function_it =
+      goto_model.goto_functions.function_map.find(function_name);
+    CHECK_RETURN(
+      goto_function_it != goto_model.goto_functions.function_map.end());
+    const goto_programt &goto_program = goto_function_it->second.body;
+
+    for(const auto &ins : goto_program.instructions)
+    {
+      if(!ins.is_assert())
+        continue;
+
+      const source_locationt &source_location = ins.source_location;
+      irep_idt property_id = source_location.get_property_id();
+      result() << "    " << property_id << '\n';
+    }
+  }
+}
+
+/// Convert a function group to JSON
+/// \param result: the JSON array to be populated
+/// \param function_group: set of function ids in the group
+/// \param goto_model: the goto model
+void goto_difft::convert_function_group_json(
+  json_arrayt &result,
+  const irep_id_sett &function_group,
+  const goto_modelt &goto_model) const
 {
-  // the function may be in goto_model1 or goto_model2
-  if(
-    goto_model1.goto_functions.function_map.find(function_name) !=
-    goto_model1.goto_functions.function_map.end())
+  for(const auto &function_name : function_group)
   {
-    const symbolt &symbol =
-      namespacet(goto_model1.symbol_table).lookup(function_name);
-    result["sourceLocation"] = json(symbol.location);
+    convert_function_json(
+      result.push_back(jsont()).make_object(), function_name, goto_model);
   }
-  else if(
-    goto_model2.goto_functions.function_map.find(function_name) !=
-    goto_model2.goto_functions.function_map.end())
+}
+
+/// Convert function information to JSON
+/// \param result: the JSON object to be populated
+/// \param function_name: the function id
+/// \param goto_model: the goto model
+void goto_difft::convert_function_json(
+  json_objectt &result,
+  const irep_idt &function_name,
+  const goto_modelt &goto_model) const
+{
+  namespacet ns(goto_model.symbol_table);
+  const symbolt &symbol = ns.lookup(function_name);
+
+  result["name"] = json_stringt(id2string(function_name));
+  result["sourceLocation"] = json(symbol.location);
+
+  if(options.get_bool_option("show-properties"))
   {
-    const symbolt &symbol =
-      namespacet(goto_model2.symbol_table).lookup(function_name);
-    result["sourceLocation"] = json(symbol.location);
+    const auto goto_function_it =
+      goto_model.goto_functions.function_map.find(function_name);
+    CHECK_RETURN(
+      goto_function_it != goto_model.goto_functions.function_map.end());
+    const goto_programt &goto_program = goto_function_it->second.body;
+
+    convert_properties_json(
+      result["properties"].make_array(), ns, function_name, goto_program);
   }
-  result["name"]=json_stringt(id2string(function_name));
 }

src/goto-diff/goto_diff_parse_options.cpp

@@ -53,6 +53,8 @@ Author: Peter Schrammel
 
 #include <pointer-analysis/add_failed_symbols.h>
 
+#include <java_bytecode/java_bytecode_language.h>
+
 #include <langapi/mode.h>
 
 #include <cbmc/version.h>
@@ -234,6 +236,8 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
             << " must not be given together" << eom;
     exit(1);
   }
+
+  options.set_option("show-properties", cmdline.isset("show-properties"));
 }
 
 /// invoke main modules
@@ -331,10 +335,10 @@ int goto_diff_parse_optionst::doit()
     return CPROVER_EXIT_SUCCESS;
   }
 
-  syntactic_difft sd(goto_model1, goto_model2, get_message_handler());
+  syntactic_difft sd(goto_model1, goto_model2, options, get_message_handler());
   sd.set_ui(get_ui());
   sd();
-  sd.output_functions(std::cout);
+  sd.output_functions();
 
   return CPROVER_EXIT_SUCCESS;
 }
@@ -516,6 +520,7 @@ void goto_diff_parse_optionst::help()
     "\n"
     "Diff options:\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    HELP_SHOW_PROPERTIES
     " --syntactic                  do syntactic diff (default)\n"
     " -u | --unified               output unified diff\n"
     " --change-impact | \n"

src/goto-diff/goto_diff_parse_options.h

@@ -20,6 +20,7 @@ Author: Peter Schrammel
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_properties.h>
 
 #include "goto_diff_languages.h"
 
@@ -30,6 +31,7 @@ class optionst;
 #define GOTO_DIFF_OPTIONS \
   "(json-ui)" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
   OPT_GOTO_CHECK \
   "(cover):" \
   "(verbosity):(version)" \

src/goto-diff/syntactic_diff.h

@@ -16,12 +16,13 @@ Author: Peter Schrammel
 
 class syntactic_difft:public goto_difft
 {
- public:
-  explicit syntactic_difft(
+public:
+  syntactic_difft(
     const goto_modelt &_goto_model1,
     const goto_modelt &_goto_model2,
-    message_handlert &_message_handler):
-    goto_difft(_goto_model1, _goto_model2, _message_handler)
+    const optionst &_options,
+    message_handlert &_message_handler)
+    : goto_difft(_goto_model1, _goto_model2, _options, _message_handler)
   {
   }