#!/usr/bin/env perl

use warnings;
use strict;
use Term::ANSIColor;
use Cwd 'abs_path';
use File::Basename;
use Time::HiRes;

my $SELF = abs_path( $0 );
my $SELFDIR = dirname( abs_path( $0 ) );
my $ESBMC = "$SELFDIR/esbmc";

if ( @ARGV == 0 ) {
    my $driver_checsum = `sha1sum $SELF\n`;
    chomp $driver_checsum;
    $driver_checsum =~ s/^([0-9a-f]*)\s+.*$/$1/;
    print( "driver checksum: $driver_checsum\n" );
    print( "driver: $SELF\n" );
    my $version = `$ESBMC --version`;
    chomp $version;
    $version =~ m,ESBMC version ([0-9.]*) ,;
    my $esbmc_checsum = `sha1sum $ESBMC\n`;
    chomp $esbmc_checsum;
    $esbmc_checsum =~ s/^([0-9a-f]*)\s+.*$/$1/;
    print "checksum: $esbmc_checsum\n";
    print "build type: Release\n";
    exit 0;
}

open( my $handle, "<", $ARGV[0] );

my @cmds;

while ( <$handle> ) {
    chomp;
    if ( /^cc/ || /^verify/ || /^expect/ || /^\s*$/ ) {
        push( @cmds, $_ );
    } elsif ( /^#/ ) {
    } else {
        die "invalid input $_\n" unless /^\s/;
        $cmds[-1] .= $_;
    }
}

sub eat {
    my ( $ref, $pos ) = @_;
    splice @{$ref}, $pos;
}

sub eat2 {
    my ( $ref, $pos ) = @_;
    splice @{$ref}, $pos, 2;
}

sub invalid {
    my ( $ref ) = @_;
    die "invalid option ${$ref}\n";
}

sub replace {
    my ( $by, $join ) = @_;
    return sub {
        my ( $ref, $pos ) = @_;
        if ( $join ) {
            my $v = $ref->[ $pos + 1 ];
            splice @{$ref}, $pos, 2, "$by$v";
        } else {
            $ref->[ $pos ] = $by;
        }
    }
}

my %invalid = ( "--lart" => 1
              , "--vfslimit" => 1
              , "--capture" => 1
              , "--stdin" => 1
              );

my %ignored = ( "--symbolic" => 1
              , "--ceds" => 1
              , "--solver" => 1
              , "--sequential" => 1
              , "--disable-static-reduction" => 1
              );

my @verifyopts = ( "--deadlock-check", "--timeout", "2h", "--boolector",
                   "--unroll-loops", "--unwind", "128", "--no-unwinding-assertions",
                   "-D__FILE__=unknown", "-D__LINE__=0" );

my @cppverifyopts = ( "-I", "$SELFDIR/../share/esbmc/cpplibrary/" );

sub verify {
    my @args = @_;

    for ( my $i = 0; $i < @args; $i++ ) {
        my $a = $args[ $i ];
        next if ( exists $ignored{ $a } );
        die "upsupported command $a" if  exists $invalid{ $a };
        if ( $a eq "-r" || $a eq "--report" || $a eq "--num-callers" || $a eq "--autotrace" || $a eq "-T" || $a eq "--threads" ) {
            $i++;
            next;
        } elsif ( $a eq "-o" ) {
            $i++;
            my $val = $args[ $i ];
            if ( $val eq "nofail:malloc" ) {
                push @verifyopts, "--force-malloc-success";
            } else {
                die "invalid -o $val\n";
            }
        } elsif ( $a eq "--max-time" ) {
            push @verifyopts, "--timeout", $args[ $i + 1 ];
            $i++;
        } elsif ( $a eq "--max-memory" ) {
            push @verifyopts, "--memlimit", $args[ $i + 1 ];
            $i++;
        } elsif ( $a eq "-std=c++14" || $a =~ /^-std=/ || $a =~ /^-C,(.*)/ || $a =~ /\.bc$/ ) {
            print STDERR "WARNING: ignoring $a\n"
        } else {
            push @verifyopts, $a;
        }
    }
}

sub cc {
    my @args = @_;

    for ( my $i = 0; $i < @args; $i++ ) {
        my $a = $args[ $i ];

        if ( $a eq "-c" || $a eq "--dont-link" ) {
            die "--dont-link not supported for ESBMC\n"
        } elsif ( $a =~ /^-C,(.*)/ ) {
        } elsif ( $a eq "-o" ) {
            $i++;
        } elsif ( $a =~ /^-std=/ || $a =~ /^-O/ ) {
            print STDERR "WARNING: ignoring $a\n";
        } elsif ( -f $a ) {
            push @verifyopts, $a;
        } elsif ( $a =~ m,^(-I|-isystem)([^/].*)$, ) {
            push @verifyopts, "-I $2";
        } elsif ( ($a eq "-I" || $a eq "-isystem") && $args[ $i + 1 ] =~ m,^/, ) {
            my $a2 = $args[ $i + 1 ];
            push @verifyopts, "-I $a2";
            $i++;
        } else {
            push @verifyopts, $a;
        }
    }
}

for my $cmd ( @cmds ) {
    if ( $cmd =~ /^cc\s+(.*)$/ ) {
        cc( split( /\s+/, $1 ) );
    } elsif ( $cmd =~ /^verify\s+(.*)$/ ) {
        verify( split( /\s+/, $1  ) );
    } elsif ( $cmd =~ /^expect\s/ ) {
        print "WARNING: expect is ignored\n";
    } elsif ( $cmd =~ /^\s*$/ ) {
    } else {
        die "invalid command $cmd\n";
    }
}

my $cpp = 0;
for my $f ( @verifyopts ) {
    next if $cpp;
    if ( $f =~ /\.cpp$/ ) {
        $cpp = 1;
        push @verifyopts, @cppverifyopts;
    }
}

print "+ @verifyopts\n";
open( my $report, ">", "report.yaml" );

my $status = undef;
my $finished = undef;

if ( open( my $out, "-|" ) ) {
	while ( <$out> ) {
		chomp;
		my $line = $_;
		if ( $line eq "VERIFICATION SUCCESSFUL" ) {
			$status = 1;
		} elsif ( $line eq "VERIFICATION FAILED" ) {
			$status = 0;
		} elsif ( $line =~ /^search time: (.*)$/ ) {
            print $report "timers:\n  search: $1\n";
        } elsif ( $line =~ "finished: yes" && !defined( $finished ) ) {
            $finished = 1;
        } elsif ( $line eq "Timed out" ) {
            $finished = 0;
        }
	}
	close $out;
} else {
    my $start = Time::HiRes::gettimeofday();
    my $result = system( $ESBMC, @verifyopts );
    my $end = Time::HiRes::gettimeofday();
    print( "search time: " . ($end - $start) . "\n" );
    my $r = $?;
    if ( $result == 0 || ($r & 255) == 0 && ($r >> 8) == 1 ) {
        print( "finished: yes\n" );
    } else {
        print( "finished: no\n" );
    }
    exit;
}

if ( !$finished ) {
    print $report ( "property holds: unknown\n" );
} elsif ( $status ) {
    print $report ( "property holds: yes\n" );
} else {
    print $report ( "property holds: no\n" );
}