src/HOL/Mirabelle/lib/scripts/report.pl
changeset 32499 909a6447700a
child 32506 173fd51d06c9
equal deleted inserted replaced
32498:1132c7c13f36 32499:909a6447700a
       
     1 #
       
     2 # Author: Sascha Boehme
       
     3 #
       
     4 # Reports for Mirabelle
       
     5 #
       
     6 
       
     7 my $log_file = $ARGV[0];
       
     8 
       
     9 open(FILE, "<$log_file") || die "Cannot open file '$log_file'";
       
    10 my @lines = <FILE>;
       
    11 close(FILE);
       
    12 
       
    13 my $unhandled = 0;
       
    14 
       
    15 my $sh_calls = 0;
       
    16 my $sh_succeeded = 0;
       
    17 my $sh_time = 0;
       
    18 
       
    19 my $metis_calls = 0;
       
    20 my $metis_succeeded = 0;
       
    21 my $metis_time = 0;
       
    22 
       
    23 foreach (@lines) {
       
    24   if (m/^unhandled exception/) {
       
    25     $unhandled++;
       
    26   }
       
    27   if (m/^sledgehammer:/) {
       
    28     $sh_calls++;
       
    29   }
       
    30   if (m/^sledgehammer: succeeded \(([0-9]+)\)/) {
       
    31     $sh_succeeded++;
       
    32     $sh_time += $1;
       
    33   }
       
    34   if (m/^metis \(sledgehammer\):/) {
       
    35     $metis_calls++;
       
    36   }
       
    37   if (m/^metis \(sledgehammer\): succeeded \(([0-9]+)\)/) {
       
    38     $metis_succeeded++;
       
    39     $metis_time += $1;
       
    40   }
       
    41 }
       
    42 
       
    43 open(FILE, ">>$log_file") || die "Cannot open file '$log_file'";
       
    44 
       
    45 print FILE "\n\n\n";
       
    46 
       
    47 if ($unhandled > 0) {
       
    48   print FILE "Number of unhandled exceptions: $unhandled\n\n";
       
    49 }
       
    50 
       
    51 if ($sh_calls > 0) {
       
    52   my $percent = $sh_succeeded / $sh_calls * 100;
       
    53   my $time = $sh_time / 1000;
       
    54   print FILE "Total number of sledgehammer calls: $sh_calls\n";
       
    55   print FILE "Number of successful sledgehammer calls: $sh_succeeded\n";
       
    56   printf FILE "Percentage of successful sledgehammer calls: %.0f%%\n", $percent;
       
    57   print FILE "Total time for successful sledgehammer calls: $time seconds\n\n";
       
    58 }
       
    59 
       
    60 if ($metis_calls > 0) {
       
    61   my $percent = $metis_succeeded / $metis_calls * 100;
       
    62   my $time = $metis_time / 1000;
       
    63   print FILE "Total number of metis calls: $metis_calls\n";
       
    64   print FILE "Number of successful metis calls: $metis_succeeded\n";
       
    65   printf FILE "Percentage of successful metis calls: %.0f%%\n", $percent;
       
    66   print FILE "Total time for successful metis calls: $time seconds\n";
       
    67 }
       
    68 
       
    69 close(FILE);