@@ -269,6 +269,10 @@ bool ai_baset::visit(
269
269
{
270
270
bool new_data=false ;
271
271
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;
272
276
273
277
// Function call and end are special cases
274
278
if (l->is_function_call ())
@@ -325,11 +329,27 @@ bool ai_baset::visit_edge(
325
329
const namespacet &ns,
326
330
working_sett &working_set)
327
331
{
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
+
328
337
// Has history taught us not to step here...
329
338
auto next =
330
339
p->step (to_l, *(storage->abstract_traces_before (to_l)), caller_history);
331
340
if (next.first == ai_history_baset::step_statust::BLOCKED)
341
+ {
342
+ log.progress () << " blocked by history" << messaget::eom;
332
343
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
+ }
333
353
trace_ptrt to_p = next.second ;
334
354
335
355
// Abstract domains are mutable so we must copy before we transform
@@ -339,21 +359,50 @@ bool ai_baset::visit_edge(
339
359
statet &new_values = *tmp_state;
340
360
341
361
// Apply transformer
362
+ log.progress () << " applying transformer... " ;
342
363
new_values.transform (function_id, p, to_function_id, to_p, *this , ns);
343
364
344
365
// Expanding a domain means that it has to be analysed again
345
366
// Likewise if the history insists that it is a new trace
346
367
// (assuming it is actually reachable).
368
+ log.progress () << " merging... " ;
369
+ bool return_value = false ;
347
370
if (
348
371
merge (new_values, p, to_p) ||
349
372
(next.first == ai_history_baset::step_statust::NEW &&
350
373
!new_values.is_bottom ()))
351
374
{
352
375
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;
354
382
}
355
383
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;
357
406
}
358
407
359
408
bool ai_baset::visit_edge_function_call (
@@ -366,6 +415,11 @@ bool ai_baset::visit_edge_function_call(
366
415
const goto_functionst &,
367
416
const namespacet &ns)
368
417
{
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
+
369
423
// The default implementation is not interprocedural
370
424
// so the effects of the call are approximated but nothing else
371
425
return visit_edge (
@@ -391,6 +445,10 @@ bool ai_baset::visit_function_call(
391
445
392
446
PRECONDITION (l_call->is_function_call ());
393
447
448
+ messaget log (message_handler);
449
+ log.progress () << " ai_baset::visit_function_call at "
450
+ << l_call->location_number << messaget::eom;
451
+
394
452
locationt l_return = std::next (l_call);
395
453
396
454
// operator() allows analysis of a single goto_program independently
@@ -405,6 +463,8 @@ bool ai_baset::visit_function_call(
405
463
const irep_idt &callee_function_id =
406
464
to_symbol_expr (callee_expression).get_identifier ();
407
465
466
+ log.progress () << " Calling " << callee_function_id << messaget::eom;
467
+
408
468
goto_functionst::function_mapt::const_iterator it =
409
469
goto_functions.function_map .find (callee_function_id);
410
470
@@ -464,6 +524,10 @@ bool ai_baset::visit_end_function(
464
524
locationt l = p->current_location ();
465
525
PRECONDITION (l->is_end_function ());
466
526
527
+ messaget log (message_handler);
528
+ log.progress () << " ai_baset::visit_end_function " << function_id
529
+ << messaget::eom;
530
+
467
531
// Do nothing
468
532
return false ;
469
533
}
@@ -478,6 +542,11 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
478
542
const goto_functionst &goto_functions,
479
543
const namespacet &ns)
480
544
{
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
+
481
550
// This is the edge from call site to function head.
482
551
{
483
552
locationt l_begin = callee.instructions .begin ();
@@ -495,6 +564,9 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
495
564
ns,
496
565
catch_working_set);
497
566
567
+ log.progress () << " Handle " << callee_function_id << " recursively"
568
+ << messaget::eom;
569
+
498
570
// do we need to do/re-do the fixedpoint of the body?
499
571
if (new_data)
500
572
fixedpoint (
@@ -507,6 +579,8 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
507
579
508
580
// This is the edge from function end to return site.
509
581
{
582
+ log.progress () << " Handle return edges" << messaget::eom;
583
+
510
584
// get location at end of the procedure we have called
511
585
locationt l_end = --callee.instructions .end ();
512
586
DATA_INVARIANT (
0 commit comments