Merge pull request #5475 from natasha-jeppu/pointer-alias

CBMC additional profiling info: Pointer dereference, points-to set metric

Author: danielsn

regression/cbmc/points-to-sets/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  unsigned int value;
+  int *p = (int *)value;
+
+  *p = *p + 1;
+  assert(1);
+  return 0;
+}

regression/cbmc/points-to-sets/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--show-points-to-sets
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format.
+xml-ui and plain output not supported.

regression/cbmc/points-to-sets/test_json.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--show-points-to-sets --json-ui
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\},\n\s*\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\}
+--
+--
+To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format.
+xml-ui and plain output not supported.

regression/cbmc/points-to-sets/test_xml.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--show-points-to-sets --xml-ui
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format.
+xml-ui and plain output not supported.

src/cbmc/cbmc_parse_options.cpp

@@ -122,6 +122,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("simplify", true);
   options.set_option("simplify-if", true);
   options.set_option("show-goto-symex-steps", false);
+  options.set_option("show-points-to-sets", false);
 
   // Other default
   options.set_option("arrays-uf", "auto");
@@ -520,6 +521,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("show-goto-symex-steps"))
     options.set_option("show-goto-symex-steps", true);
 
+  if(cmdline.isset("show-points-to-sets"))
+    options.set_option("show-points-to-sets", true);
+
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 }
 
@@ -562,6 +566,17 @@ int cbmc_parse_optionst::doit()
     return CPROVER_EXIT_USAGE_ERROR;
   }
 
+  if(cmdline.isset("show-points-to-sets"))
+  {
+    if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
+    {
+      log.error() << "--show-points-to-sets supports only"
+                     " json output. Use --json-ui."
+                  << messaget::eom;
+      return CPROVER_EXIT_USAGE_ERROR;
+    }
+  }
+
   register_languages();
 
   // configure gcc, if required

src/goto-checker/bmc_util.h

@@ -177,6 +177,7 @@ void run_property_decider(
   "(show-loops)" \
   "(show-vcc)" \
   "(show-goto-symex-steps)" \
+  "(show-points-to-sets)" \
   "(slice-formula)" \
   "(unwinding-assertions)" \
   "(no-unwinding-assertions)" \
@@ -203,6 +204,8 @@ void run_property_decider(
   " --show-symex-strategies      list strategies for use with --paths\n" \
   " --show-goto-symex-steps      show which steps symex travels, includes " \
   "                              diagnostic information\n" \
+  " --show-points-to-sets        show points-to sets for\n" \
+  "                              pointer dereference. Requires --json-ui.\n" \
   " --program-only               only show program expression\n" \
   " --show-byte-ops              show all byte extracts and updates\n" \
   " --show-loops                 show the loops in the program\n" \

src/goto-symex/symex_clean_expr.cpp

@@ -134,9 +134,9 @@ void goto_symext::process_array_expr(statet &state, exprt &expr)
   symex_dereference_statet symex_dereference_state(state, ns);
 
   value_set_dereferencet dereference(
-    ns, state.symbol_table, symex_dereference_state, language_mode, false);
+    ns, state.symbol_table, symex_dereference_state, language_mode, false, log);
 
-  expr = dereference.dereference(expr);
+  expr = dereference.dereference(expr, symex_config.show_points_to_sets);
   lift_lets(state, expr);
 
   ::process_array_expr(expr, symex_config.simplify_opt, ns);

src/goto-symex/symex_config.h

@@ -46,6 +46,7 @@ struct symex_configt final
   /// \brief Prints out the path that symex is actively taking during execution,
   /// includes diagnostic information about call stack and guard size.
   bool show_symex_steps;
+  bool show_points_to_sets;
 
   /// Maximum sizes for which field sensitivity will be applied to array cells
   std::size_t max_field_sensitivity_array_size;

src/goto-symex/symex_dereference.cpp

@@ -264,10 +264,12 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
       state.symbol_table,
       symex_dereference_state,
       language_mode,
-      expr_is_not_null);
+      expr_is_not_null,
+      log);
 
     // std::cout << "**** " << format(tmp1) << '\n';
-    exprt tmp2 = dereference.dereference(tmp1);
+    exprt tmp2 =
+      dereference.dereference(tmp1, symex_config.show_points_to_sets);
     // std::cout << "**** " << format(tmp2) << '\n';
 
     expr.swap(tmp2);

src/goto-symex/symex_main.cpp

@@ -47,6 +47,7 @@ symex_configt::symex_configt(const optionst &options)
     debug_level(unsafe_string2int(options.get_option("debug-level"))),
     run_validation_checks(options.get_bool_option("validate-ssa-equation")),
     show_symex_steps(options.get_bool_option("show-goto-symex-steps")),
+    show_points_to_sets(options.get_bool_option("show-points-to-sets")),
     max_field_sensitivity_array_size(
       options.is_set("no-array-field-sensitivity")
         ? 0

src/pointer-analysis/goto_program_dereference.h

@@ -28,15 +28,24 @@ class goto_program_dereferencet:protected dereference_callbackt
   // for the final argument to value_set_dereferencet.
   // This means that language-inappropriate values such as
   // (struct A*)some_integer_value in Java, may be returned.
+  // Note: value_set_dereferencet requires a messaget instance
+  // as on of its arguments to display the points-to set
+  // during symex. Display is not done during goto-program
+  // conversion. To ensure this the display_points_to_sets
+  // parameter in value_set_dereferencet::dereference()
+  // is set to false by default and is not changed by the
+  // goto program conversion modules. Similarly, here we set
+  // _log to be a default messaget instance.
   goto_program_dereferencet(
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
     const optionst &_options,
-    value_setst &_value_sets)
+    value_setst &_value_sets,
+    const messaget &_log = messaget())
     : options(_options),
       ns(_ns),
       value_sets(_value_sets),
-      dereference(_ns, _new_symbol_table, *this, ID_nil, false)
+      dereference(_ns, _new_symbol_table, *this, ID_nil, false, _log)
   {
   }
 

src/pointer-analysis/value_set_dereference.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #ifdef DEBUG
 #include <iostream>
-#include <util/format_expr.h>
 #endif
 
 #include <util/arith_tools.h>
@@ -24,8 +23,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
+#include <util/format_expr.h>
 #include <util/format_type.h>
 #include <util/fresh_symbol.h>
+#include <util/json_irep.h>
 #include <util/options.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
@@ -60,7 +61,9 @@ static bool should_use_local_definition_for(const exprt &expr)
   return false;
 }
 
-exprt value_set_dereferencet::dereference(const exprt &pointer)
+exprt value_set_dereferencet::dereference(
+  const exprt &pointer,
+  bool display_points_to_sets)
 {
   if(pointer.type().id()!=ID_pointer)
     throw "dereference expected pointer type, but got "+
@@ -70,8 +73,9 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
   if(pointer.id()==ID_if)
   {
     const if_exprt &if_expr=to_if_expr(pointer);
-    exprt true_case = dereference(if_expr.true_case());
-    exprt false_case = dereference(if_expr.false_case());
+    exprt true_case = dereference(if_expr.true_case(), display_points_to_sets);
+    exprt false_case =
+      dereference(if_expr.false_case(), display_points_to_sets);
     return if_exprt(if_expr.cond(), true_case, false_case);
   }
   else if(pointer.id() == ID_typecast)
@@ -90,14 +94,26 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
       const auto &if_expr = to_if_expr(*underlying);
       return if_exprt(
         if_expr.cond(),
-        dereference(typecast_exprt(if_expr.true_case(), pointer.type())),
-        dereference(typecast_exprt(if_expr.false_case(), pointer.type())));
+        dereference(
+          typecast_exprt(if_expr.true_case(), pointer.type()),
+          display_points_to_sets),
+        dereference(
+          typecast_exprt(if_expr.false_case(), pointer.type()),
+          display_points_to_sets));
     }
   }
 
   // type of the object
   const typet &type=pointer.type().subtype();
 
+  json_objectt json_result;
+  if(display_points_to_sets)
+  {
+    std::stringstream ss;
+    ss << format(pointer);
+    json_result["Pointer"] = json_stringt(ss.str());
+  }
+
 #ifdef DEBUG
   std::cout << "value_set_dereferencet::dereference pointer=" << format(pointer)
             << '\n';
@@ -107,6 +123,22 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
   const std::vector<exprt> points_to_set =
     dereference_callback.get_value_set(pointer);
 
+  if(display_points_to_sets)
+  {
+    json_result["PointsToSetSize"] =
+      json_numbert(std::to_string(points_to_set.size()));
+
+    json_arrayt points_to_set_json;
+    for(auto p : points_to_set)
+    {
+      std::stringstream ss;
+      ss << format(p);
+      points_to_set_json.push_back(json_stringt(ss.str()));
+    }
+
+    json_result["PointsToSet"] = points_to_set_json;
+  }
+
 #ifdef DEBUG
   std::cout << "value_set_dereferencet::dereference points_to_set={";
   for(auto p : points_to_set)
@@ -135,6 +167,22 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
     compare_against_pointer = fresh_binder.symbol_expr();
   }
 
+  if(display_points_to_sets)
+  {
+    json_result["RetainedValuesSetSize"] =
+      json_numbert(std::to_string(points_to_set.size()));
+
+    json_arrayt retained_values_set_json;
+    for(auto &value : retained_values)
+    {
+      std::stringstream ss;
+      ss << format(value);
+      retained_values_set_json.push_back(json_stringt(ss.str()));
+    }
+
+    json_result["RetainedValuesSet"] = retained_values_set_json;
+  }
+
 #ifdef DEBUG
   std::cout << "value_set_dereferencet::dereference retained_values={";
   for(const auto &value : retained_values)
@@ -224,6 +272,15 @@ exprt value_set_dereferencet::dereference(const exprt &pointer)
   if(compare_against_pointer != pointer)
     value = let_exprt(to_symbol_expr(compare_against_pointer), pointer, value);
 
+  if(display_points_to_sets)
+  {
+    std::stringstream ss;
+    ss << format(value);
+    json_result["Value"] = json_stringt(ss.str());
+
+    log.status() << json_result;
+  }
+
 #ifdef DEBUG
   std::cout << "value_set_derefencet::dereference value=" << format(value)
             << '\n'

src/pointer-analysis/value_set_dereference.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <unordered_set>
 
+#include <util/message.h>
 #include <util/std_expr.h>
 
 #include "dereference_callback.h"
@@ -34,25 +35,29 @@ class value_set_dereferencet final
   ///   dereference failure
   /// \param _exclude_null_derefs: Ignore value-set entries that indicate a
   //    given dereference may follow a null pointer
+  /// \param _log: Messaget object for displaying points-to set
   value_set_dereferencet(
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
     dereference_callbackt &_dereference_callback,
     const irep_idt _language_mode,
-    bool _exclude_null_derefs):
-    ns(_ns),
-    new_symbol_table(_new_symbol_table),
-    dereference_callback(_dereference_callback),
-    language_mode(_language_mode),
-    exclude_null_derefs(_exclude_null_derefs)
+    bool _exclude_null_derefs,
+    const messaget &_log)
+    : ns(_ns),
+      new_symbol_table(_new_symbol_table),
+      dereference_callback(_dereference_callback),
+      language_mode(_language_mode),
+      exclude_null_derefs(_exclude_null_derefs),
+      log(_log)
   { }
 
   virtual ~value_set_dereferencet() { }
 
   /// Dereference the given pointer-expression. Any errors are
   /// reported to the callback method given in the constructor.
   /// \param pointer: A pointer-typed expression, to be dereferenced.
-  exprt dereference(const exprt &pointer);
+  /// \param display_points_to_sets: Display size and contents of points to sets
+  exprt dereference(const exprt &pointer, bool display_points_to_sets = false);
 
   /// Return value for `build_reference_to`; see that method for documentation.
   class valuet
@@ -105,6 +110,7 @@ class value_set_dereferencet final
   /// Flag indicating whether `value_set_dereferencet::dereference` should
   /// disregard an apparent attempt to dereference NULL
   const bool exclude_null_derefs;
+  const messaget &log;
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H