Show properties for goto-diff

regression/goto-diff/java-properties/new/Test.java

@@ -0,0 +1,19 @@
+public class Test {
+
+  private static Test static_test = null;
+  private Test test = new Test();
+
+  public Test() {
+  }
+
+  public int foo(int x) {
+    if (x > 10) {
+      return x;
+    } else {
+      return x * 10;
+    }
+  }
+
+  public void newfun() {
+  }
+}

regression/goto-diff/java-properties/old/Test.java

@@ -0,0 +1,19 @@
+public class Test {
+
+  private static Test static_test = new Test();
+  private Test test = null;
+
+  public Test() {
+  }
+
+  public int foo(int x) {
+    if (x > 10) {
+      return x;
+    } else {
+      return x * 10;
+    }
+  }
+
+  public void obsolete() {
+  }
+}

regression/goto-diff/java-properties/test.desc

@@ -0,0 +1,10 @@
+CORE
+new.jar
+old.jar --json-ui --show-properties --cover location
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+  "deletedFunctions": \[\n    {\n      "name": "java::Test\.obsolete:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "18",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.obsolete:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "0",\n            "file": "Test\.java",\n            "function": "java::Test\.obsolete:\(\)V",\n            "line": "18"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.obsolete:\(\)V",\n        "line": "18"\n      }\n    }\n  ],\n  "modifiedFunctions": \[\n    {\n      "name": "java::Test\.<init>:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "6",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "1",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "6"\n          }\n        },\n        {\n          "class": "coverage",\n          "coveredLines": "4",\n          "description": "block 2",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.2",\n          "sourceLocation": {\n            "bytecodeIndex": "3",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "4"\n          }\n        },\n        {\n          "class": "coverage",\n          "coveredLines": "4",\n          "description": "block 3",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.3",\n          "sourceLocation": {\n            "bytecodeIndex": "5",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "4"\n          }\n        },\n        {\n          "class": "coverage",\n          "coveredLines": "4,7",\n          "description": "block 4",\n          "expression": "false",\n          "name": "java::Test\.<init>:\(\)V\.coverage\.4",\n          "sourceLocation": {\n            "bytecodeIndex": "6",\n            "file": "Test\.java",\n            "function": "java::Test\.<init>:\(\)V",\n            "line": "4"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.<init>:\(\)V",\n        "line": "6"\n      }\n    },\n    {\n      "name": "java::Test\.<clinit>:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "3",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.<clinit>:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "1",\n            "file": "Test\.java",\n            "function": "java::Test\.<clinit>:\(\)V",\n            "line": "3"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.<clinit>:\(\)V",\n        "line": "3"\n      }\n    }\n  ],\n  "newFunctions": \[\n    {\n      "name": "java::Test\.newfun:\(\)V",\n      "properties": \[\n        {\n          "class": "coverage",\n          "coveredLines": "18",\n          "description": "block 1",\n          "expression": "false",\n          "name": "java::Test\.newfun:\(\)V\.coverage\.1",\n          "sourceLocation": {\n            "bytecodeIndex": "0",\n            "file": "Test\.java",\n            "function": "java::Test\.newfun:\(\)V",\n            "line": "18"\n          }\n        }\n      ],\n      "sourceLocation": {\n        "file": "Test\.java",\n        "function": "java::Test\.newfun:\(\)V",\n        "line": "18"\n      }\n    }\n  ],\n
+--
+^warning: ignoring

src/cbmc/cbmc_parse_options.cpp

@@ -534,7 +534,8 @@ int cbmc_parse_optionst::doit()
   if(cmdline.isset("show-claims") || // will go away
      cmdline.isset("show-properties")) // use this one
   {
-    show_properties(goto_model, ui_message_handler.get_ui());
+    show_properties(
+      goto_model, get_message_handler(), ui_message_handler.get_ui());
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -923,7 +924,7 @@ void cbmc_parse_optionst::help()
     " cbmc file.c ...              source file names\n"
     "\n"
     "Analysis options:\n"
-    " --show-properties            show the properties, but don't run analysis\n" // NOLINT(*)
+    HELP_SHOW_PROPERTIES
     " --symex-coverage-report f    generate a Cobertura XML coverage report in f\n" // NOLINT(*)
     " --property id                only check one specific property\n"
     " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -53,9 +53,9 @@ class optionst;
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
   "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
-  "(show-claims)(claim):(show-properties)" \
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \
@@ -72,7 +72,7 @@ class optionst;
   "(graphml-witness):" \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
-  "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
+  "(claim):(show-claims)(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 
 class cbmc_parse_optionst:

src/clobber/clobber_parse_options.cpp

@@ -150,7 +150,7 @@ int clobber_parse_optionst::doit()
 
     if(cmdline.isset("show-properties"))
     {
-      show_properties(goto_model, get_ui());
+      show_properties(goto_model, get_message_handler(), get_ui());
       return 0;
     }
 

src/clobber/clobber_parse_options.h

@@ -19,23 +19,27 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/goto_check.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_properties.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 
 class goto_functionst;
 class optionst;
 
+// clang-format off
 #define CLOBBER_OPTIONS \
   "(depth):(context-bound):(unwind):" \
   OPT_GOTO_CHECK \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
   "(no-assertions)(no-assumptions)" \
   "(error-label):(verbosity):(no-library)" \
   "(version)" \
   "(string-abstraction)" \
-  "(show-locs)(show-vcc)(show-properties)(show-trace)" \
+  "(show-locs)(show-vcc)(show-trace)" \
   "(property):" \
   JAVA_BYTECODE_LANGUAGE_OPTIONS
+// clang-format on
 
 class clobber_parse_optionst:
   public parse_options_baset,

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -592,7 +592,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
   if(cmdline.isset("show-properties"))
   {
-    show_properties(goto_model, get_ui());
+    show_properties(goto_model, get_message_handler(), get_ui());
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -815,6 +815,7 @@ void goto_analyzer_parse_optionst::help()
 
   std::cout << " * *\n";
 
+  // clang-format off
   std::cout <<
     "* *                Daniel Kroening, DiffBlue                * *\n"
     "* *                 [email protected]                   * *\n"
@@ -898,8 +899,7 @@ void goto_analyzer_parse_optionst::help()
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --show-properties            show the properties, but don't run analysis\n"
+    HELP_SHOW_PROPERTIES
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
@@ -908,4 +908,5 @@ void goto_analyzer_parse_optionst::help()
     " --version                    show version and exit\n"
     HELP_TIMESTAMP
     "\n";
+  // clang-format on
 }

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -109,6 +109,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_properties.h>
 
 #include <analyses/ai.h>
 #include <analyses/goto_check.h>
@@ -119,17 +120,19 @@ class bmct;
 class goto_functionst;
 class optionst;
 
+// clang-format off
 #define GOTO_ANALYSER_OPTIONS \
   OPT_FUNCTIONS \
   "D:I:(std89)(std99)(std11)" \
   "(classpath):(cp):(main-class):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
   OPT_GOTO_CHECK \
   "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)" \
-  "(show-properties)(show-reachable-properties)(property):" \
+  "(show-reachable-properties)(property):" \
   "(verbosity):(version)" \
   "(gcc)(arch):" \
   "(taint):(show-taint)" \
@@ -147,6 +150,7 @@ class optionst;
   "(location-sensitive)(concurrent)" \
   "(no-simplify-slicing)" \
   JAVA_BYTECODE_LANGUAGE_OPTIONS
+// clang-format on
 
 class goto_analyzer_parse_optionst:
   public parse_options_baset,

src/goto-diff/CMakeLists.txt

@@ -13,6 +13,7 @@ target_link_libraries(goto-diff-lib
     linking
     big-int
     pointer-analysis
+    goto-instrument-lib
     goto-programs
     assembler
     analyses

src/goto-diff/Makefile

@@ -15,6 +15,18 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../pointer-analysis/pointer-analysis$(LIBEXT) \
+      ../goto-instrument/cover$(OBJEXT) \
+      ../goto-instrument/cover_basic_blocks$(OBJEXT) \
+      ../goto-instrument/cover_filter$(OBJEXT) \
+      ../goto-instrument/cover_instrument_branch$(OBJEXT) \
+      ../goto-instrument/cover_instrument_condition$(OBJEXT) \
+      ../goto-instrument/cover_instrument_decision$(OBJEXT) \
+      ../goto-instrument/cover_instrument_location$(OBJEXT) \
+      ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
+      ../goto-instrument/cover_instrument_other$(OBJEXT) \
+      ../goto-instrument/cover_util$(OBJEXT) \
+      ../goto-symex/adjust_float_expressions$(OBJEXT) \
+      ../goto-symex/rewrite_union$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \

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