#!/usr/bin/perl
use strict;
use warnings;
use JSON::PP;
use File::Basename;
use File::Path qw(make_path remove_tree);

sub usage {
    print "Usage: $0 <source.c> [extra_args...]\n";
    exit 1;
}

sub parse_debug_summary {
    my $file = shift;
    my %results = (
        proved => 0, total => 0, timeouts => 0, failures => 0,
        warnings => [], failed_goals => [], timing => {}
    );
    
    open my $fh, '<', $file or return \%results;
    
    my $in_goal_section = 0;
    my $current_goal = '';
    
    while (my $line = <$fh>) {
        chomp $line;
        
        # Basic metrics
        if ($line =~ /Proved goals:\s+(\d+)\s+\/\s+(\d+)/) {
            $results{proved} = $1;
            $results{total} = $2;
        }
        
        if ($line =~ /Timeout:\s+(\d+)/) { $results{timeouts} = $1; }
        if ($line =~ /Failure:\s+(\d+)/) { $results{failures} = $1; }
        if ($line =~ /Cache.*found:(\d+)/) { $results{cache_hits} = $1; }
        
        # Timing info
        if ($line =~ /(Alt-Ergo|Coq|Z3|CVC4)\s+([\d\.]+):\s+(\d+)\s+\(([^)]+)\)/) {
            $results{timing}{$1} = {
                goals => $3,
                time_range => $4
            };
        }
        
        if ($line =~ /Qed:\s+(\d+)\s+\(([^)]+)\)/) {
            $results{timing}{Qed} = {
                goals => $1,
                time_range => $2
            };
        }
        
        # Warnings
        if ($line =~ /Warning: (.+)/) {
            push @{$results{warnings}}, $1;
        }
        
        # Goal failure details
        if ($line =~ /^Goal (.+):$/) {
            $current_goal = $1;
            $in_goal_section = 1;
        }
        
        if ($in_goal_section && $line =~ /Prover (.+) returns (Timeout|Failure)/) {
            push @{$results{failed_goals}}, {
                goal => $current_goal,
                prover => $1,
                result => $2
            };
            $in_goal_section = 0;
        }
    }
    
    close $fh;
    return \%results;
}

sub format_time_range {
    my $range = shift;
    return $range unless $range =~ /(\d+)ms-(\d+)ms/;
    
    my ($min, $max) = ($1, $2);
    if ($max < 1000) { return "${min}-${max}ms"; }
    if ($max < 10000) { return sprintf("%.1f-%.1fs", $min/1000, $max/1000); }
    return sprintf("%.0f-%.0fs", $min/1000, $max/1000);
}

sub report_results {
    my ($progname, $results) = @_;
    
    print "Verification: $progname\n";
    print "Goals: $results->{proved}/$results->{total} proved\n";
    
    my $success = ($results->{proved} == $results->{total} && 
                   $results->{timeouts} == 0 && $results->{failures} == 0);
    
    if ($success) {
        print "Status: SUCCESS\n";
    } else {
        print "Status: FAILURE";
        print " ($results->{timeouts} timeouts)" if $results->{timeouts};
        print " ($results->{failures} failures)" if $results->{failures};
        print "\n";
    }
    
    # Performance summary
    if (%{$results->{timing}}) {
        print "\nProver performance:\n";
        for my $prover (sort keys %{$results->{timing}}) {
            my $t = $results->{timing}{$prover};
            my $time_str = format_time_range($t->{time_range});
            print "  $prover: $t->{goals} goals ($time_str)\n";
        }
    }
    
    if ($results->{cache_hits}) {
        my $cache_rate = sprintf("%.0f%%", 
            ($results->{cache_hits} / $results->{total}) * 100);
        print "Cache: $results->{cache_hits}/$results->{total} hits ($cache_rate)\n";
    }
    
    # Issues
    if (@{$results->{warnings}}) {
        print "\nWarnings:\n";
        for my $warning (@{$results->{warnings}}) {
            print "  $warning\n";
        }
    }
    
    if (@{$results->{failed_goals}}) {
        print "\nFailed goals:\n";
        for my $goal (@{$results->{failed_goals}}) {
            print "  $goal->{goal}: $goal->{result} ($goal->{prover})\n";
        }
        
        # Show common failure patterns
        my %goal_types = ();
        for my $goal (@{$results->{failed_goals}}) {
            my $name = $goal->{goal};
            if ($name =~ /(lemma_\w+)/) { $goal_types{lemmas}++; }
            elsif ($name =~ /loop/) { $goal_types{loops}++; }
            elsif ($name =~ /postcondition/) { $goal_types{postconditions}++; }
            else { $goal_types{other}++; }
        }
        
        if (%goal_types) {
            print "\nFailure breakdown:";
            for my $type (sort keys %goal_types) {
                print " $goal_types{$type} $type";
            }
            print "\n";
        }
    }
    
    print "\nFiles:\n";
    print "  Details: build/$progname/results/frama.log\n";
    print "  JSON: build/$progname/results/results.json\n";
    print "  Proofs: proof/$progname/interactive/*.v\n";
    
    return $success;
}

# Main execution
@ARGV >= 1 or usage();

my $source_file = shift @ARGV;
my $prover = 'coq';
my @extra_args = @ARGV;  # Collect remaining arguments

my $progname = basename($source_file, '.c');
die "Invalid program name '$progname'\n" if !$progname || $progname =~ /^\.\.?$/;

# Setup directories  
my $build_dir = "build/$progname";
my $proof_dir = "proof/$progname";
remove_tree($build_dir) if -d $build_dir;
make_path("$build_dir/ast", "$build_dir/normalized", 
          "$build_dir/obligations/typed", "$build_dir/results",
          $proof_dir);

# Run Frama-C
my $cmd = join(' ',
    'frama-c',
    '-verbose 2',
    '-debug 2',
    '-cpp-extra-args="-I inc"',
    "-save $build_dir/ast/" . basename($source_file) . ".sav",
    '-print',
    "-ocode $build_dir/normalized/program.c", 
    '-wp',
    "-wp-out $build_dir/obligations",
    "-wp-session=$proof_dir",
    "-wp-interactive=update",
    "-wp-prover $prover",
    "-wp-report-json $build_dir/results/results.json",
    '-wp-status',
    @extra_args,  # Include extra arguments
    $source_file,
    "> $build_dir/results/frama.log 2>&1"
);

system($cmd) == 0 or die "Frama-C failed. Check $build_dir/results/frama.log\n";

# Generate SMT2 files
opendir my $dh, "$build_dir/obligations/typed";
while (my $file = readdir($dh)) {
    next unless $file =~ /\.why$/;
    my $base = basename($file, '.why');
    
    open my $in, '<', "$build_dir/obligations/typed/$file" or next;
    open my $out, '>', "$build_dir/obligations/typed/$base.smt2" or next;
    <$in>; # Skip first line
    print $out $_ while <$in>;
    close $in; close $out;
}
closedir $dh;

# Report results
my $results = parse_debug_summary("$build_dir/results/frama.log");
my $success = report_results($progname, $results);

exit($success ? 0 : 1);