begriffs open source - acsl-example/blob - scripts/prove.pl

   1 #!/usr/bin/perl
   2 use strict;
   3 use warnings;
   4 use JSON::PP;
   5 use File::Basename;
   6 use File::Path qw(make_path remove_tree);
   7
   8 sub usage {
   9     print "Usage: $0 <source.c> [extra_args...]\n";
  10     exit 1;
  11 }
  12
  13 sub parse_debug_summary {
  14     my $file = shift;
  15     my %results = (
  16         proved => 0, total => 0, timeouts => 0, failures => 0,
  17         warnings => [], failed_goals => [], timing => {}
  18     );
  19
  20     open my $fh, '<', $file or return \%results;
  21
  22     my $in_goal_section = 0;
  23     my $current_goal = '';
  24
  25     while (my $line = <$fh>) {
  26         chomp $line;
  27
  28         # Basic metrics
  29         if ($line =~ /Proved goals:\s+(\d+)\s+\/\s+(\d+)/) {
  30             $results{proved} = $1;
  31             $results{total} = $2;
  32         }
  33
  34         if ($line =~ /Timeout:\s+(\d+)/) { $results{timeouts} = $1; }
  35         if ($line =~ /Failure:\s+(\d+)/) { $results{failures} = $1; }
  36         if ($line =~ /Cache.*found:(\d+)/) { $results{cache_hits} = $1; }
  37
  38         # Timing info
  39         if ($line =~ /(Alt-Ergo|Coq|Z3|CVC4)\s+([\d\.]+):\s+(\d+)\s+\(([^)]+)\)/) {
  40             $results{timing}{$1} = {
  41                 goals => $3,
  42                 time_range => $4
  43             };
  44         }
  45
  46         if ($line =~ /Qed:\s+(\d+)\s+\(([^)]+)\)/) {
  47             $results{timing}{Qed} = {
  48                 goals => $1,
  49                 time_range => $2
  50             };
  51         }
  52
  53         # Warnings
  54         if ($line =~ /Warning: (.+)/) {
  55             push @{$results{warnings}}, $1;
  56         }
  57
  58         # Goal failure details
  59         if ($line =~ /^Goal (.+):$/) {
  60             $current_goal = $1;
  61             $in_goal_section = 1;
  62         }
  63
  64         if ($in_goal_section && $line =~ /Prover (.+) returns (Timeout|Failure)/) {
  65             push @{$results{failed_goals}}, {
  66                 goal => $current_goal,
  67                 prover => $1,
  68                 result => $2
  69             };
  70             $in_goal_section = 0;
  71         }
  72     }
  73
  74     close $fh;
  75     return \%results;
  76 }
  77
  78 sub format_time_range {
  79     my $range = shift;
  80     return $range unless $range =~ /(\d+)ms-(\d+)ms/;
  81
  82     my ($min, $max) = ($1, $2);
  83     if ($max < 1000) { return "${min}-${max}ms"; }
  84     if ($max < 10000) { return sprintf("%.1f-%.1fs", $min/1000, $max/1000); }
  85     return sprintf("%.0f-%.0fs", $min/1000, $max/1000);
  86 }
  87
  88 sub report_results {
  89     my ($progname, $results) = @_;
  90
  91     print "Verification: $progname\n";
  92     print "Goals: $results->{proved}/$results->{total} proved\n";
  93
  94     my $success = ($results->{proved} == $results->{total} &&
  95                    $results->{timeouts} == 0 && $results->{failures} == 0);
  96
  97     if ($success) {
  98         print "Status: SUCCESS\n";
  99     } else {
 100         print "Status: FAILURE";
 101         print " ($results->{timeouts} timeouts)" if $results->{timeouts};
 102         print " ($results->{failures} failures)" if $results->{failures};
 103         print "\n";
 104     }
 105
 106     # Performance summary
 107     if (%{$results->{timing}}) {
 108         print "\nProver performance:\n";
 109         for my $prover (sort keys %{$results->{timing}}) {
 110             my $t = $results->{timing}{$prover};
 111             my $time_str = format_time_range($t->{time_range});
 112             print "  $prover: $t->{goals} goals ($time_str)\n";
 113         }
 114     }
 115
 116     if ($results->{cache_hits}) {
 117         my $cache_rate = sprintf("%.0f%%",
 118             ($results->{cache_hits} / $results->{total}) * 100);
 119         print "Cache: $results->{cache_hits}/$results->{total} hits ($cache_rate)\n";
 120     }
 121
 122     # Issues
 123     if (@{$results->{warnings}}) {
 124         print "\nWarnings:\n";
 125         for my $warning (@{$results->{warnings}}) {
 126             print "  $warning\n";
 127         }
 128     }
 129
 130     if (@{$results->{failed_goals}}) {
 131         print "\nFailed goals:\n";
 132         for my $goal (@{$results->{failed_goals}}) {
 133             print "  $goal->{goal}: $goal->{result} ($goal->{prover})\n";
 134         }
 135
 136         # Show common failure patterns
 137         my %goal_types = ();
 138         for my $goal (@{$results->{failed_goals}}) {
 139             my $name = $goal->{goal};
 140             if ($name =~ /(lemma_\w+)/) { $goal_types{lemmas}++; }
 141             elsif ($name =~ /loop/) { $goal_types{loops}++; }
 142             elsif ($name =~ /postcondition/) { $goal_types{postconditions}++; }
 143             else { $goal_types{other}++; }
 144         }
 145
 146         if (%goal_types) {
 147             print "\nFailure breakdown:";
 148             for my $type (sort keys %goal_types) {
 149                 print " $goal_types{$type} $type";
 150             }
 151             print "\n";
 152         }
 153     }
 154
 155     print "\nFiles:\n";
 156     print "  Details: build/$progname/results/frama.log\n";
 157     print "  JSON: build/$progname/results/results.json\n";
 158     print "  Proofs: proof/$progname/interactive/*.v\n";
 159
 160     return $success;
 161 }
 162
 163 # Main execution
 164 @ARGV >= 1 or usage();
 165
 166 my $source_file = shift @ARGV;
 167 my $provers = 'alt-ergo,z3,coq';  # Let Frama-C handle prover fallback internally
 168 my @extra_args = @ARGV;  # Collect remaining arguments
 169
 170 my $progname = basename($source_file, '.c');
 171 die "Invalid program name '$progname'\n" if !$progname || $progname =~ /^\.\.?$/;
 172
 173 # Setup directories
 174 my $build_dir = "build/$progname";
 175 my $proof_dir = "proof/$progname";
 176 remove_tree($build_dir) if -d $build_dir;
 177 make_path("$build_dir/ast", "$build_dir/normalized",
 178           "$build_dir/obligations/typed", "$build_dir/results",
 179           $proof_dir);
 180
 181 # Run Frama-C with prover fallback (alt-ergo -> z3 -> coq)
 182 my $cmd = join(' ',
 183     'frama-c',
 184     '-verbose 2',
 185     '-debug 2',
 186     '-cpp-extra-args="-I inc"',
 187     "-save $build_dir/ast/" . basename($source_file) . ".sav",
 188     '-print',
 189     "-ocode $build_dir/normalized/program.c",
 190     '-wp',
 191     '-wp-rte',
 192     "-wp-out $build_dir/obligations",
 193     "-wp-session=$proof_dir",
 194     "-wp-interactive=update",
 195     "-wp-prover $provers",
 196     "-wp-report-json $build_dir/results/results.json",
 197     '-wp-status',
 198     @extra_args,  # Include extra arguments
 199     $source_file,
 200     "> $build_dir/results/frama.log 2>&1"
 201 );
 202
 203 system($cmd) == 0 or die "Frama-C failed. Check $build_dir/results/frama.log\n";
 204
 205 # Generate SMT2 files
 206 opendir my $dh, "$build_dir/obligations/typed";
 207 while (my $file = readdir($dh)) {
 208     next unless $file =~ /\.why$/;
 209     my $base = basename($file, '.why');
 210
 211     open my $in, '<', "$build_dir/obligations/typed/$file" or next;
 212     open my $out, '>', "$build_dir/obligations/typed/$base.smt2" or next;
 213     <$in>; # Skip first line
 214     print $out $_ while <$in>;
 215     close $in; close $out;
 216 }
 217 closedir $dh;
 218
 219 # Report results
 220 my $results = parse_debug_summary("$build_dir/results/frama.log");
 221 my $success = report_results($progname, $results);
 222
 223 exit($success ? 0 : 1);