Merge pull request #5478 from natasha-jeppu/array_theory

CBMC additional profiling info: Count and report all array constraints added during postprocessing

Author: tautschnig

regression/cbmc/array-constraint/main.c

@@ -0,0 +1,12 @@
+#include <stdlib.h>
+int main()
+{
+  size_t array_size;
+  int a[array_size];
+
+  unsigned int index;
+  a[index] = 1;
+
+  assert(a[index] == 1);
+  return 0;
+}

regression/cbmc/array-constraint/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-array-constraints
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+To test output for --show-array-constraints option that displays the count and list of all array constraints added during post processing in json format.

regression/cbmc/array-constraint/test_json.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--show-array-constraints --json-ui
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+\{\n\s*"arrayConstraints": \{\n\s*"arrayEquality": \[.*\],\n\s*"arrayWith": \[.*\]\n\s*\},\n\s*"numOfConstraints": 4\n\s*\}
+--
+--
+To test output for --show-array-constraints option that displays the count and list of all array constraints added during post processing in json format.

regression/cbmc/array-constraint/test_xml.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-array-constraints --xml-ui
+^EXIT=1$
+^SIGNAL=0$
+--
+--
+To test output for --show-array-constraints option that displays the count and list of all array constraints added during post processing in json format.

src/cbmc/cbmc_parse_options.cpp

@@ -123,6 +123,7 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("simplify-if", true);
   options.set_option("show-goto-symex-steps", false);
   options.set_option("show-points-to-sets", false);
+  options.set_option("show-array-constraints", false);
 
   // Other default
   options.set_option("arrays-uf", "auto");
@@ -348,6 +349,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("dimacs"))
     options.set_option("dimacs", true);
 
+  if(cmdline.isset("show-array-constraints"))
+    options.set_option("show-array-constraints", true);
+
   if(cmdline.isset("refine-arrays"))
   {
     options.set_option("refine", true);
@@ -577,6 +581,17 @@ int cbmc_parse_optionst::doit()
     }
   }
 
+  if(cmdline.isset("show-array-constraints"))
+  {
+    if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
+    {
+      log.error() << "--show-array-constraints supports only"
+                     " json output. Use --json-ui."
+                  << messaget::eom;
+      return CPROVER_EXIT_USAGE_ERROR;
+    }
+  }
+
   register_languages();
 
   // configure gcc, if required
@@ -1155,6 +1170,9 @@ void cbmc_parse_optionst::help()
     HELP_TIMESTAMP
     " --write-solver-stats-to json-file\n"
     "                              collect the solver query complexity\n"
+    " --show-array-constraints     show array theory constraints added\n"
+    "                              during post processing.\n"
+    "                              Requires --json-ui.\n"
     "\n";
   // clang-format on
 }

src/cbmc/cbmc_parse_options.h

@@ -47,6 +47,7 @@ class optionst;
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):(test-preprocessor)" \
   "(write-solver-stats-to):"  \
+  "(show-array-constraints)"  \
   "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
   "(object-bits):" \
   OPT_GOTO_CHECK \

src/goto-checker/solver_factory.cpp

@@ -219,8 +219,10 @@ std::unique_ptr<solver_factoryt::solvert> solver_factoryt::get_default()
     solver->set_prop(make_satcheck_prop<satcheckt>(message_handler, options));
   }
 
-  auto bv_pointers =
-    util_make_unique<bv_pointerst>(ns, solver->prop(), message_handler);
+  bool get_array_constraints =
+    options.get_bool_option("show-array-constraints");
+  auto bv_pointers = util_make_unique<bv_pointerst>(
+    ns, solver->prop(), message_handler, get_array_constraints);
 
   if(options.get_option("arrays-uf") == "never")
     bv_pointers->unbounded_array = bv_pointerst::unbounded_arrayt::U_NONE;

src/solvers/flattening/arrays.cpp

@@ -10,10 +10,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/format_expr.h>
+#include <util/json_irep.h>
+#include <util/message.h>
 #include <util/namespace.h>
 #include <util/replace_expr.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
+#include <util/ui_message.h>
 
 #include <solvers/prop/prop.h>
 
@@ -26,11 +29,17 @@ Author: Daniel Kroening, kroening@kroening.com
 arrayst::arrayst(
   const namespacet &_ns,
   propt &_prop,
-  message_handlert &message_handler)
-  : equalityt(_prop, message_handler), ns(_ns)
+  message_handlert &_message_handler,
+  bool _get_array_constraints)
+  : equalityt(_prop, _message_handler),
+    ns(_ns),
+    log(_message_handler),
+    message_handler(_message_handler)
 {
   lazy_arrays = false;        // will be set to true when --refine is used
   incremental_cache = false;  // for incremental solving
+  // get_array_constraints is true when --show-array-constraints is used
+  get_array_constraints = _get_array_constraints;
 }
 
 void arrayst::record_array_index(const index_exprt &index)
@@ -365,6 +374,7 @@ void arrayst::add_array_Ackermann_constraints()
             lazy_constraintt lazy(lazy_typet::ARRAY_ACKERMANN,
               implies_exprt(literal_exprt(indices_equal_lit), values_equal));
             add_array_constraint(lazy, true); // added lazily
+            array_constraint_count[constraint_typet::ARRAY_ACKERMANN]++;
 
 #if 0 // old code for adding, not significantly faster
             prop.lcnf(!indices_equal_lit, convert(values_equal));
@@ -451,6 +461,7 @@ void arrayst::add_array_constraints_equality(
     // equality constraints are not added lazily
     // convert must be done to guarantee correct update of the index_set
     prop.lcnf(!array_equality.l, convert(equality_expr));
+    array_constraint_count[constraint_typet::ARRAY_EQUALITY]++;
   }
 }
 
@@ -511,6 +522,7 @@ void arrayst::add_array_constraints(
       lazy_constraintt lazy(lazy_typet::ARRAY_TYPECAST,
         equal_exprt(index_expr1, index_expr2));
       add_array_constraint(lazy, false); // added immediately
+      array_constraint_count[constraint_typet::ARRAY_TYPECAST]++;
     }
   }
   else if(expr.id()==ID_index)
@@ -549,6 +561,7 @@ void arrayst::add_array_constraints_with(
     lazy_constraintt lazy(
       lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
     add_array_constraint(lazy, false); // added immediately
+    array_constraint_count[constraint_typet::ARRAY_WITH]++;
 
     updated_indices.insert(index);
   }
@@ -582,7 +595,9 @@ void arrayst::add_array_constraints_with(
         // add constraint
         lazy_constraintt lazy(lazy_typet::ARRAY_WITH, or_exprt(equality_expr,
                                 literal_exprt(guard_lit)));
+
         add_array_constraint(lazy, false); // added immediately
+        array_constraint_count[constraint_typet::ARRAY_WITH]++;
 
 #if 0 // old code for adding, not significantly faster
         {
@@ -678,6 +693,7 @@ void arrayst::add_array_constraints_array_of(
     lazy_constraintt lazy(
       lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.what()));
     add_array_constraint(lazy, false); // added immediately
+    array_constraint_count[constraint_typet::ARRAY_OF]++;
   }
 }
 
@@ -713,6 +729,7 @@ void arrayst::add_array_constraints_array_constant(
       lazy_constraintt lazy{lazy_typet::ARRAY_CONSTANT,
                             equal_exprt{index_expr, v}};
       add_array_constraint(lazy, false); // added immediately
+      array_constraint_count[constraint_typet::ARRAY_CONSTANT]++;
     }
     else
     {
@@ -755,6 +772,7 @@ void arrayst::add_array_constraints_array_constant(
           implies_exprt{index_constraint,
                         equal_exprt{index_expr, operands[range.first]}}};
         add_array_constraint(lazy, true); // added lazily
+        array_constraint_count[constraint_typet::ARRAY_CONSTANT]++;
       }
     }
   }
@@ -778,7 +796,9 @@ void arrayst::add_array_constraints_comprehension(
     lazy_constraintt lazy(
       lazy_typet::ARRAY_COMPREHENSION,
       equal_exprt(index_expr, comprehension_body));
+
     add_array_constraint(lazy, false); // added immediately
+    array_constraint_count[constraint_typet::ARRAY_COMPREHENSION]++;
   }
 }
 
@@ -806,6 +826,7 @@ void arrayst::add_array_constraints_if(
                             or_exprt(literal_exprt(!cond_lit),
                               equal_exprt(index_expr1, index_expr2)));
     add_array_constraint(lazy, false); // added immediately
+    array_constraint_count[constraint_typet::ARRAY_IF]++;
 
 #if 0 // old code for adding, not significantly faster
     prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
@@ -825,9 +846,59 @@ void arrayst::add_array_constraints_if(
       or_exprt(literal_exprt(cond_lit),
       equal_exprt(index_expr1, index_expr2)));
     add_array_constraint(lazy, false); // added immediately
+    array_constraint_count[constraint_typet::ARRAY_IF]++;
 
 #if 0 // old code for adding, not significantly faster
     prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
 #endif
   }
 }
+
+std::string arrayst::enum_to_string(constraint_typet type)
+{
+  switch(type)
+  {
+  case constraint_typet::ARRAY_ACKERMANN:
+    return "arrayAckermann";
+  case constraint_typet::ARRAY_WITH:
+    return "arrayWith";
+  case constraint_typet::ARRAY_IF:
+    return "arrayIf";
+  case constraint_typet::ARRAY_OF:
+    return "arrayOf";
+  case constraint_typet::ARRAY_TYPECAST:
+    return "arrayTypecast";
+  case constraint_typet::ARRAY_CONSTANT:
+    return "arrayConstant";
+  case constraint_typet::ARRAY_COMPREHENSION:
+    return "arrayComprehension";
+  case constraint_typet::ARRAY_EQUALITY:
+    return "arrayEquality";
+  default:
+    UNREACHABLE;
+  }
+}
+
+void arrayst::display_array_constraint_count()
+{
+  json_objectt json_result;
+  json_objectt &json_array_theory =
+    json_result["arrayConstraints"].make_object();
+
+  size_t num_constraints = 0;
+
+  array_constraint_countt::iterator it = array_constraint_count.begin();
+  while(it != array_constraint_count.end())
+  {
+    std::string contraint_type_string = enum_to_string(it->first);
+    json_array_theory[contraint_type_string] =
+      json_numbert(std::to_string(it->second));
+
+    num_constraints += it->second;
+    it++;
+  }
+
+  json_result["numOfConstraints"] =
+    json_numbert(std::to_string(num_constraints));
+  log.status() << ",\n" << json_result;
+}

src/solvers/flattening/arrays.h

@@ -33,12 +33,15 @@ class arrayst:public equalityt
   arrayst(
     const namespacet &_ns,
     propt &_prop,
-    message_handlert &message_handler);
+    message_handlert &message_handler,
+    bool get_array_constraints = false);
 
   void post_process() override
   {
     post_process_arrays();
     SUB::post_process();
+    if(get_array_constraints)
+      display_array_constraint_count();
   }
 
   // NOLINTNEXTLINE(readability/identifiers)
@@ -49,6 +52,8 @@ class arrayst:public equalityt
 
 protected:
   const namespacet &ns;
+  messaget log;
+  message_handlert &message_handler;
 
   virtual void post_process_arrays()
   {
@@ -103,10 +108,28 @@ class arrayst:public equalityt
 
   bool lazy_arrays;
   bool incremental_cache;
+  bool get_array_constraints;
   std::list<lazy_constraintt> lazy_array_constraints;
   void add_array_constraint(const lazy_constraintt &lazy, bool refine = true);
   std::map<exprt, bool> expr_map;
 
+  enum class constraint_typet
+  {
+    ARRAY_ACKERMANN,
+    ARRAY_WITH,
+    ARRAY_IF,
+    ARRAY_OF,
+    ARRAY_TYPECAST,
+    ARRAY_CONSTANT,
+    ARRAY_COMPREHENSION,
+    ARRAY_EQUALITY
+  };
+
+  typedef std::map<constraint_typet, size_t> array_constraint_countt;
+  array_constraint_countt array_constraint_count;
+  void display_array_constraint_count();
+  std::string enum_to_string(constraint_typet);
+
   // adds all the constraints eagerly
   void add_array_constraints();
   void add_array_Ackermann_constraints();

src/solvers/flattening/boolbv.h

@@ -37,8 +37,9 @@ class boolbvt:public arrayst
   boolbvt(
     const namespacet &_ns,
     propt &_prop,
-    message_handlert &message_handler)
-    : arrayst(_ns, _prop, message_handler),
+    message_handlert &message_handler,
+    bool get_array_constraints = false)
+    : arrayst(_ns, _prop, message_handler, get_array_constraints),
       unbounded_array(unbounded_arrayt::U_NONE),
       boolbv_width(_ns),
       bv_utils(_prop),