#!/usr/bin/env perl

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

my $SELF = abs_path( $0 );
my $SELFDIR = dirname( abs_path( $0 ) );
my $DIVINE = "$SELFDIR/divine";

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 = split /\n/, `$DIVINE --version`;
    for my $v ( @version ) {
        if ( $v =~ /^Version:\s+(.*)\+(.*)/ ) {
            print "version: $1\n";
            print "checksum: $2\n";
        }
        if ( $v =~ /^Debug:\s+(.*)/ ) {
            if ( $1 eq "disabled" ) {
                print "build type: Debug\n";
            } else {
                print "build type: Release\n";
            }
        }
    }
    exit 0;
}

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

my @cmds;

while ( <$handle> ) {
    chomp;
    if ( /^cc/ || /^verify/ || /^expect/ || /^\s*$/ ) {
        push( @cmds, $_ );
    } 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 = ( "--symbolic" => 1
              , "--ceds" => 1
              , "--lart" => 1
              , "--vfslimit" => 1
              , "--capture" => 1
              , "--stdin" => 1
              , "--solver" => 1
              );

my @ccopts = ( "compile", "--llvm" );
my @cflags = ( "-U__unix__", "-Uunix", "-U__unix",
               "-U__linux", "-U__linux__", "-U__gnu_linux__",
               "-U__x86_64", "-U__x86_64__" );
my @verifyopts = ( "verify", "-n", "--shared", "--report=yaml:report.yaml", "--max-time=7200" );

sub verify {
    my @args = @_;

    for ( my $i = 0; $i < @args; $i++ ) {
        my $a = $args[ $i ];
        next if ( $a eq "--sequential" || $a eq "--disable-static-reduction" );
        die "upsupported command $a" if  exists $invalid{ $a };
        if ( $a eq "-r" || $a eq "--report" || $a eq "--num-callers" || $a eq "--autotrace" ) {
            $i++;
            next;
        } elsif ( $a eq "-o" ) {
            $i++;
            my $val = $args[ $i ];
            if ( $val eq "nofail:malloc" ) {
                push @cflags, "-include", "nofail-malloc.h";
            } else {
                die "invalid -o $val\n";
            }
        } elsif ( $a eq "-T" || $a eq "--threads" ) {
            push @verifyopts, "-w", $args[ $i + 1 ];
            $i++;
        } elsif ( $a eq "--max-time" || $a eq "--max-memory" ) {
            push @verifyopts, $a, $args[ $i + 1 ];
            $i++;
        } elsif ( $a eq "-std=c++14" ) {
            push @cflags, "-std=c++1y";
        } elsif ( $a =~ /^-std=/ ) {
            push @cflags, $a;
        } elsif ( $a =~ /^-C,(.*)/ ) {
            push @cflags, split( /,/, $1 );
        } 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" ) {
            push @ccopts, "--dont-link";
        } elsif ( $a =~ /^-C,(.*)/ ) {
            push @cflags, split( /,/, $1 );
        } elsif ( $a eq "-o" ) {
            push @ccopts, "-o", $args[ $i + 1 ];
            $i++;
        } elsif ( $a eq "-std=c++14" ) {
            push @cflags, "-std=c++1y";
        } elsif ( -f $a ) {
            push @ccopts, $a;
        } elsif ( $a =~ m,^(-I|-isystem)([^/].*)$, ) {
            push @cflags, "$1../$2";
        } elsif ( ($a eq "-I" || $a eq "-isystem") && $args[ $i + 1 ] =~ m,^/, ) {
            my $a2 = $args[ $i + 1 ];
            push @cflags, "$a../$a2";
            $i++;
        } else {
            push @cflags, $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";
    }
}

push @ccopts, "--cflags=" . join( " ", @cflags );
print "+ @ccopts\n";
system( $DIVINE, @ccopts ) == 0 or die "compile failed\n";

if ( grep( /^-w$/, @verifyopts ) == 0 ) {
    push @verifyopts, "-w", "4";
}
print "+ @verifyopts\n";
system( $DIVINE, @verifyopts ) == 0 or die "verify failed\n";