Merge pull request #6285 from martin-cs/feature/ai-logging

Feature/ai logging

Author: martin-cs

regression/goto-analyzer/logging/main.c

@@ -0,0 +1,48 @@
+#include <assert.h>
+
+int global;
+
+int f00(int x)
+{
+  return global + x;
+}
+
+int main(void)
+{
+  int local;
+  unsigned int nondet;
+
+  local = 1;
+  global = 1;
+
+  assert(local == global);
+
+  if(nondet)
+  {
+    local = 2;
+  }
+  if(nondet)
+  {
+    global = 2;
+  }
+
+  assert(local == global);
+
+  do
+  {
+    local = 3;
+    global = 3;
+  } while(nondet-- > 0);
+
+  assert(local == global);
+
+  local = 4;
+  global = 4;
+
+  local = f00(1);
+  global = f00(1);
+
+  assert(local == global);
+
+  return 0;
+}

regression/goto-analyzer/logging/test-recursive-interprocedural-10.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--verify --recursive-interprocedural --vsd --loop-unwind-and-branching 10 --one-domain-per-history --verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1] line \d+ assertion local == global: SUCCESS$
+^\[main\.assertion\.2] line \d+ assertion local == global: UNKNOWN$
+^\[main\.assertion\.3] line \d+ assertion local == global: SUCCESS$
+^\[main\.assertion\.4] line \d+ assertion local == global: UNKNOWN$
+^ai_baset::visit \d+ in main$
+^ai_baset::visit_edge from \d+ to \d+\.\.\. gives a new history\.\.\. applying transformer\.\.\. merging\.\.\. result queued\.$
+^ai_baset::visit_function_call at \d+$
+^ai_baset::visit_end_function main$
+^ai_recursive_interproceduralt::visit_edge_function_call from \d+ to \d+$
+^p = local_control_flow_history : location \d+
+^global \(\) -> 0 @ \[\d+\]$
+--
+^warning: ignoring

regression/goto-analyzer/logging/test-recursive-interprocedural-8.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--verify --recursive-interprocedural --vsd --loop-unwind-and-branching 10 --one-domain-per-history --verbosity 8
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1] line \d+ assertion local == global: SUCCESS$
+^\[main\.assertion\.2] line \d+ assertion local == global: UNKNOWN$
+^\[main\.assertion\.3] line \d+ assertion local == global: SUCCESS$
+^\[main\.assertion\.4] line \d+ assertion local == global: UNKNOWN$
+--
+^warning: ignoring
+^p = local_control_flow_history : location \d+
+^global \(\) -> 0 @ \[\d+\]$
+^ai_baset::visit \d+ in main$
+^ai_baset::visit_edge from \d+ to \d+\.\.\. gives a new history\.\.\. applying transformer\.\.\. merging\.\.\. result queued\.$
+^ai_baset::visit_function_call at \d+$
+^ai_baset::visit_end_function main$
+^ai_recursive_interproceduralt::visit_edge_function_call from \d+ to \d+$

regression/goto-analyzer/logging/test-recursive-interprocedural-9.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--verify --recursive-interprocedural --vsd --loop-unwind-and-branching 10 --one-domain-per-history --verbosity 9
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1] line \d+ assertion local == global: SUCCESS$
+^\[main\.assertion\.2] line \d+ assertion local == global: UNKNOWN$
+^\[main\.assertion\.3] line \d+ assertion local == global: SUCCESS$
+^\[main\.assertion\.4] line \d+ assertion local == global: UNKNOWN$
+^ai_baset::visit \d+ in main$
+^ai_baset::visit_edge from \d+ to \d+\.\.\. gives a new history\.\.\. applying transformer\.\.\. merging\.\.\. result queued\.$
+^ai_baset::visit_function_call at \d+$
+^ai_baset::visit_end_function main$
+^ai_recursive_interproceduralt::visit_edge_function_call from \d+ to \d+$
+--
+^warning: ignoring
+^p = local_control_flow_history : location \d+
+^global \(\) -> 0 @ \[\d+\]$

regression/goto-analyzer/logging/test-three-way-merge-10.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--verify --three-way-merge --vsd --loop-unwind-and-branching 10 --one-domain-per-history --verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1] line \d+ assertion local == global: SUCCESS$
+^\[main\.assertion\.2] line \d+ assertion local == global: UNKNOWN$
+^\[main\.assertion\.3] line \d+ assertion local == global: SUCCESS$
+^\[main\.assertion\.4] line \d+ assertion local == global: SUCCESS$
+^ai_baset::visit \d+ in main$
+^ai_baset::visit_edge from \d+ to \d+\.\.\. gives a new history\.\.\. applying transformer\.\.\. merging\.\.\. result queued\.$
+^ai_baset::visit_function_call at \d+$
+^ai_baset::visit_end_function main$
+^ai_three_way_merget::visit_edge_function_call from \d+ to \d+$
+^ai_three_way_merget::visit_edge_function_call edge from \d+ to \d+\.\.\. gives a new history\.\.\. applying transformer\.\.\. three way merge\.\.\. merging\.\.\. result queued\.$
+^p = local_control_flow_history : location \d+
+^global \(\) -> 0 @ \[\d+\]$
+--
+^warning: ignoring

src/analyses/ai.cpp

@@ -269,6 +269,10 @@ bool ai_baset::visit(
 {
   bool new_data=false;
   locationt l = p->current_location();
+  messaget log(message_handler);
+
+  log.progress() << "ai_baset::visit " << l->location_number << " in "
+                 << function_id << messaget::eom;
 
   // Function call and end are special cases
   if(l->is_function_call())
@@ -325,11 +329,27 @@ bool ai_baset::visit_edge(
   const namespacet &ns,
   working_sett &working_set)
 {
+  messaget log(message_handler);
+  log.progress() << "ai_baset::visit_edge from "
+                 << p->current_location()->location_number << " to "
+                 << to_l->location_number << "... ";
+
   // Has history taught us not to step here...
   auto next =
     p->step(to_l, *(storage->abstract_traces_before(to_l)), caller_history);
   if(next.first == ai_history_baset::step_statust::BLOCKED)
+  {
+    log.progress() << "blocked by history" << messaget::eom;
     return false;
+  }
+  else if(next.first == ai_history_baset::step_statust::NEW)
+  {
+    log.progress() << "gives a new history... ";
+  }
+  else
+  {
+    log.progress() << "merges with existing history... ";
+  }
   trace_ptrt to_p = next.second;
 
   // Abstract domains are mutable so we must copy before we transform
@@ -339,21 +359,50 @@ bool ai_baset::visit_edge(
   statet &new_values = *tmp_state;
 
   // Apply transformer
+  log.progress() << "applying transformer... ";
   new_values.transform(function_id, p, to_function_id, to_p, *this, ns);
 
   // Expanding a domain means that it has to be analysed again
   // Likewise if the history insists that it is a new trace
   // (assuming it is actually reachable).
+  log.progress() << "merging... ";
+  bool return_value = false;
   if(
     merge(new_values, p, to_p) ||
     (next.first == ai_history_baset::step_statust::NEW &&
      !new_values.is_bottom()))
   {
     put_in_working_set(working_set, to_p);
-    return true;
+    log.progress() << "result queued." << messaget::eom;
+    return_value = true;
+  }
+  else
+  {
+    log.progress() << "domain unchanged." << messaget::eom;
   }
 
-  return false;
+  // Branch because printing some histories and domains can be expensive
+  // esp. if the output is then just discarded and this is a critical path.
+  if(message_handler.get_verbosity() >= messaget::message_levelt::M_DEBUG)
+  {
+    log.debug() << "p = ";
+    p->output(log.debug());
+    log.debug() << messaget::eom;
+
+    log.debug() << "current = ";
+    current.output(log.debug(), *this, ns);
+    log.debug() << messaget::eom;
+
+    log.debug() << "to_p = ";
+    to_p->output(log.debug());
+    log.debug() << messaget::eom;
+
+    log.debug() << "new_values = ";
+    new_values.output(log.debug(), *this, ns);
+    log.debug() << messaget::eom;
+  }
+
+  return return_value;
 }
 
 bool ai_baset::visit_edge_function_call(
@@ -366,6 +415,11 @@ bool ai_baset::visit_edge_function_call(
   const goto_functionst &,
   const namespacet &ns)
 {
+  messaget log(message_handler);
+  log.progress() << "ai_baset::visit_edge_function_call from "
+                 << p_call->current_location()->location_number << " to "
+                 << l_return->location_number << messaget::eom;
+
   // The default implementation is not interprocedural
   // so the effects of the call are approximated but nothing else
   return visit_edge(
@@ -391,6 +445,10 @@ bool ai_baset::visit_function_call(
 
   PRECONDITION(l_call->is_function_call());
 
+  messaget log(message_handler);
+  log.progress() << "ai_baset::visit_function_call at "
+                 << l_call->location_number << messaget::eom;
+
   locationt l_return = std::next(l_call);
 
   // operator() allows analysis of a single goto_program independently
@@ -405,6 +463,8 @@ bool ai_baset::visit_function_call(
       const irep_idt &callee_function_id =
         to_symbol_expr(callee_expression).get_identifier();
 
+      log.progress() << "Calling " << callee_function_id << messaget::eom;
+
       goto_functionst::function_mapt::const_iterator it =
         goto_functions.function_map.find(callee_function_id);
 
@@ -464,6 +524,10 @@ bool ai_baset::visit_end_function(
   locationt l = p->current_location();
   PRECONDITION(l->is_end_function());
 
+  messaget log(message_handler);
+  log.progress() << "ai_baset::visit_end_function " << function_id
+                 << messaget::eom;
+
   // Do nothing
   return false;
 }
@@ -478,6 +542,11 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
   const goto_functionst &goto_functions,
   const namespacet &ns)
 {
+  messaget log(message_handler);
+  log.progress() << "ai_recursive_interproceduralt::visit_edge_function_call"
+                 << " from " << p_call->current_location()->location_number
+                 << " to " << l_return->location_number << messaget::eom;
+
   // This is the edge from call site to function head.
   {
     locationt l_begin = callee.instructions.begin();
@@ -495,6 +564,9 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
       ns,
       catch_working_set);
 
+    log.progress() << "Handle " << callee_function_id << " recursively"
+                   << messaget::eom;
+
     // do we need to do/re-do the fixedpoint of the body?
     if(new_data)
       fixedpoint(
@@ -507,6 +579,8 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
 
   // This is the edge from function end to return site.
   {
+    log.progress() << "Handle return edges" << messaget::eom;
+
     // get location at end of the procedure we have called
     locationt l_end = --callee.instructions.end();
     DATA_INVARIANT(

src/analyses/ai.h

@@ -51,6 +51,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/deprecate.h>
 #include <util/json.h>
 #include <util/make_unique.h>
+#include <util/message.h>
 #include <util/xml.h>
 
 #include <goto-programs/goto_model.h>
@@ -127,10 +128,12 @@ class ai_baset
   ai_baset(
     std::unique_ptr<ai_history_factory_baset> &&hf,
     std::unique_ptr<ai_domain_factory_baset> &&df,
-    std::unique_ptr<ai_storage_baset> &&st)
+    std::unique_ptr<ai_storage_baset> &&st,
+    message_handlert &mh)
     : history_factory(std::move(hf)),
       domain_factory(std::move(df)),
-      storage(std::move(st))
+      storage(std::move(st)),
+      message_handler(mh)
   {
   }
 
@@ -515,6 +518,9 @@ class ai_baset
   {
     return storage->get_state(p, *domain_factory);
   }
+
+  // Logging
+  message_handlert &message_handler;
 };
 
 // Perform interprocedural analysis by simply recursing in the interpreter
@@ -525,8 +531,9 @@ class ai_recursive_interproceduralt : public ai_baset
   ai_recursive_interproceduralt(
     std::unique_ptr<ai_history_factory_baset> &&hf,
     std::unique_ptr<ai_domain_factory_baset> &&df,
-    std::unique_ptr<ai_storage_baset> &&st)
-    : ai_baset(std::move(hf), std::move(df), std::move(st))
+    std::unique_ptr<ai_storage_baset> &&st,
+    message_handlert &mh)
+    : ai_baset(std::move(hf), std::move(df), std::move(st), mh)
   {
   }
 
@@ -562,7 +569,8 @@ class ait : public ai_recursive_interproceduralt
         util_make_unique<
           ai_history_factory_default_constructort<ahistoricalt>>(),
         util_make_unique<ai_domain_factory_default_constructort<domainT>>(),
-        util_make_unique<location_sensitive_storaget>())
+        util_make_unique<location_sensitive_storaget>(),
+        no_logging)
   {
   }
 
@@ -571,7 +579,8 @@ class ait : public ai_recursive_interproceduralt
         util_make_unique<
           ai_history_factory_default_constructort<ahistoricalt>>(),
         std::move(df),
-        util_make_unique<location_sensitive_storaget>())
+        util_make_unique<location_sensitive_storaget>(),
+        no_logging)
   {
   }
 
@@ -613,6 +622,9 @@ class ait : public ai_recursive_interproceduralt
   /// This function exists to enforce that `domainT` is derived from
   /// \ref ai_domain_baset
   void dummy(const domainT &s) { const statet &x=s; (void)x; }
+
+  // To keep the old constructor interface we disable logging
+  null_message_handlert no_logging;
 };
 
 /// Base class for concurrency-aware abstract interpretation. See