@@ -269,6 +269,10 @@ bool ai_baset::visit(
269269{
270270 bool new_data=false ;
271271 locationt l = p->current_location ();
272+ messaget log (message_handler);
273+
274+ log.progress () << " ai_baset::visit " << l->location_number << " in "
275+ << function_id << messaget::eom;
272276
273277 // Function call and end are special cases
274278 if (l->is_function_call ())
@@ -325,11 +329,27 @@ bool ai_baset::visit_edge(
325329 const namespacet &ns,
326330 working_sett &working_set)
327331{
332+ messaget log (message_handler);
333+ log.progress () << " ai_baset::visit_edge from "
334+ << p->current_location ()->location_number << " to "
335+ << to_l->location_number << " ... " ;
336+
328337 // Has history taught us not to step here...
329338 auto next =
330339 p->step (to_l, *(storage->abstract_traces_before (to_l)), caller_history);
331340 if (next.first == ai_history_baset::step_statust::BLOCKED)
341+ {
342+ log.progress () << " blocked by history" << messaget::eom;
332343 return false ;
344+ }
345+ else if (next.first == ai_history_baset::step_statust::NEW)
346+ {
347+ log.progress () << " gives a new history... " ;
348+ }
349+ else
350+ {
351+ log.progress () << " merges with existing history... " ;
352+ }
333353 trace_ptrt to_p = next.second ;
334354
335355 // Abstract domains are mutable so we must copy before we transform
@@ -339,21 +359,50 @@ bool ai_baset::visit_edge(
339359 statet &new_values = *tmp_state;
340360
341361 // Apply transformer
362+ log.progress () << " applying transformer... " ;
342363 new_values.transform (function_id, p, to_function_id, to_p, *this , ns);
343364
344365 // Expanding a domain means that it has to be analysed again
345366 // Likewise if the history insists that it is a new trace
346367 // (assuming it is actually reachable).
368+ log.progress () << " merging... " ;
369+ bool return_value = false ;
347370 if (
348371 merge (new_values, p, to_p) ||
349372 (next.first == ai_history_baset::step_statust::NEW &&
350373 !new_values.is_bottom ()))
351374 {
352375 put_in_working_set (working_set, to_p);
353- return true ;
376+ log.progress () << " result queued." << messaget::eom;
377+ return_value = true ;
378+ }
379+ else
380+ {
381+ log.progress () << " domain unchanged." << messaget::eom;
354382 }
355383
356- return false ;
384+ // Branch because printing some histories and domains can be expensive
385+ // esp. if the output is then just discarded and this is a critical path.
386+ if (message_handler.get_verbosity () >= messaget::message_levelt::M_DEBUG)
387+ {
388+ log.debug () << " p = " ;
389+ p->output (log.debug ());
390+ log.debug () << messaget::eom;
391+
392+ log.debug () << " current = " ;
393+ current.output (log.debug (), *this , ns);
394+ log.debug () << messaget::eom;
395+
396+ log.debug () << " to_p = " ;
397+ to_p->output (log.debug ());
398+ log.debug () << messaget::eom;
399+
400+ log.debug () << " new_values = " ;
401+ new_values.output (log.debug (), *this , ns);
402+ log.debug () << messaget::eom;
403+ }
404+
405+ return return_value;
357406}
358407
359408bool ai_baset::visit_edge_function_call (
@@ -366,6 +415,11 @@ bool ai_baset::visit_edge_function_call(
366415 const goto_functionst &,
367416 const namespacet &ns)
368417{
418+ messaget log (message_handler);
419+ log.progress () << " ai_baset::visit_edge_function_call from "
420+ << p_call->current_location ()->location_number << " to "
421+ << l_return->location_number << messaget::eom;
422+
369423 // The default implementation is not interprocedural
370424 // so the effects of the call are approximated but nothing else
371425 return visit_edge (
@@ -391,6 +445,10 @@ bool ai_baset::visit_function_call(
391445
392446 PRECONDITION (l_call->is_function_call ());
393447
448+ messaget log (message_handler);
449+ log.progress () << " ai_baset::visit_function_call at "
450+ << l_call->location_number << messaget::eom;
451+
394452 locationt l_return = std::next (l_call);
395453
396454 // operator() allows analysis of a single goto_program independently
@@ -405,6 +463,8 @@ bool ai_baset::visit_function_call(
405463 const irep_idt &callee_function_id =
406464 to_symbol_expr (callee_expression).get_identifier ();
407465
466+ log.progress () << " Calling " << callee_function_id << messaget::eom;
467+
408468 goto_functionst::function_mapt::const_iterator it =
409469 goto_functions.function_map .find (callee_function_id);
410470
@@ -464,6 +524,10 @@ bool ai_baset::visit_end_function(
464524 locationt l = p->current_location ();
465525 PRECONDITION (l->is_end_function ());
466526
527+ messaget log (message_handler);
528+ log.progress () << " ai_baset::visit_end_function " << function_id
529+ << messaget::eom;
530+
467531 // Do nothing
468532 return false ;
469533}
@@ -478,6 +542,11 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
478542 const goto_functionst &goto_functions,
479543 const namespacet &ns)
480544{
545+ messaget log (message_handler);
546+ log.progress () << " ai_recursive_interproceduralt::visit_edge_function_call"
547+ << " from " << p_call->current_location ()->location_number
548+ << " to " << l_return->location_number << messaget::eom;
549+
481550 // This is the edge from call site to function head.
482551 {
483552 locationt l_begin = callee.instructions .begin ();
@@ -495,6 +564,9 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
495564 ns,
496565 catch_working_set);
497566
567+ log.progress () << " Handle " << callee_function_id << " recursively"
568+ << messaget::eom;
569+
498570 // do we need to do/re-do the fixedpoint of the body?
499571 if (new_data)
500572 fixedpoint (
@@ -507,6 +579,8 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
507579
508580 // This is the edge from function end to return site.
509581 {
582+ log.progress () << " Handle return edges" << messaget::eom;
583+
510584 // get location at end of the procedure we have called
511585 locationt l_end = --callee.instructions .end ();
512586 DATA_INVARIANT (
0 commit comments