#!/usr/bin/env perl
java.lang.NullPointerException
# provethem.in
# Release: ProofLite-6.0.9 (3/14/14)
java.lang.NullPointerException
# Contact: Cesar Munoz (cesar.a.munoz@nasa.gov)
# NASA Langley Research Center
# http://shemesh.larc.nasa.gov/people/cam/ProofLite
java.lang.NullPointerException
# Copyright (c) 2011-2012 United States Government as represented by
# the National Aeronautics and Space Administration.  No copyright
# is claimed in the United States under Title 17, U.S.Code. All Other
# Rights Reserved.
java.lang.NullPointerException
# Script for batch proving several libraries in PVS 
java.lang.NullPointerException

use Getopt::Long;
use File::Basename;
use Term::ANSIColor qw(:constants);
use Cwd;

$Term::ANSIColor::AUTORESET = 1;

$PVSPATH="@PVSPATH@";

@prelude = ("bitvector", "finite_sets");

$OUTPUT_AUTOFLUSH=1;
$VERSION="ProofLite-6.0.9 (3/14/14)";
$PROVEIT="$PVSPATH/proveit";
$PROVETHEMVERSION="provethem - $VERSION";

$usageln = "Usage: provethem [--help | <option> ...] <file>";

sub usage() {
  print <<EOF;
$PROVETHEMVERSION -- runs proveit on several libraries

$usageln
<option> is
  --addpath               consider the current directory as part of 
                          PVS_LIBRARY_PATH
  --after=<dir>           prove all libraries after <dir>, exclusive.
  --before=<dir>          prove all libraries before <dir>, exclusive.
  --but=<dir1>,..,<dirn>  do not process libraries <dir1>,...,<dirn>
  --color                 do not use colors
  --cleanbin              clean binary files but do not prove the libraries
  --clearpath             consider an empty PVS_LIBRARY_PATH
  --dir <dir>             use <dir> as default directory of summary files
  --do=<dir1>,..,<dirn>   process libraries <dir1>,...,<dirn>
  --disable <o1,...on>    disable external oracles o1,...,on.
  --disable-oracles       disable any external oracle
  --enable <o1,..,on>     enable external oracles o1,..,on. Overwrite --disable
  --ext <ext>             use <ext> as default extension of summary files
  --execute <command>     execute Unix <command> on all libraries. Command 
                          may refer to \%DIR\% and \%FILE\%
  --force                 force provethem to go even if there is a proveit error
  --from=<dir>            prove all libraries from <dir>, inclusive.
  --lisp <lisp>           specify lisp version; <lisp> is one of allegro,cmulisp
  --log                   log all information generated by PVS in <file>.log 
  --out <outfile>         save output to <outfile>
  --test                  process <file> but do not call proveit
  --to=<dir>              prove all libraries to <dir>, inclusive.
  --top <th>              use <th>.pvs instead of top.pvs as top theory  
  --typecheck-only        typecheck but do not prove the libraries
  --verbose               print summary information for all theories
  --version               print version information and exit

File <file> is an ordered list of libraries to be processed by proveit.  Each
line in <file> has the form <lib> [: <options>], where <lib> is a directory
name and <options> are paramters to proveit. If <lib> is empty, options apply
to all libraries thenceforth.  Output is saved in <outfile>,  which can be
specified using the option -out.  Otherwise, a default name having the
form <file><postfix>.summaries is used.
The <postfix> depends on the options -do,-but,-from,-to,-after,-before
given to the script.
Unless the option -out is explictly use, an output file is not created when
the options -cleanbin, -execute or -test are given.
EOF
  exit;
}

$color = 1;

GetOptions('addpath'=>\$addpath,
           'after=s'=>\$after,
           'before=s'=>\$before,
    'but=s'=>\@but,
    'cleanbin'=>\$cleanbin,
    'clearpath'=>\$clearpath,
    'color!'=>\$color,
           'dir=s'=>\$dir,
    'do=s'=>\@do,
           'disable=s'=>\@disable,
           'disable-oracles'=>\$disableoracles,
    'execute=s'=>\$execute,
    'ext=s'=>\$ext,
    'force'=>\$force,
           'from=s'=>\$from,
    'help'=>\$help,
           'lisp=s'=>\$lisp,
    'log!' => \$log,
    'out=s'=>\$out,
    'test'=>\$test,
           'to=s'=>\$to,
    'top=s'=>\$top,
           'enable=s'=>\@enable,
           'typecheck-only'=>\$typecheckonly,
    'verbose'=>\$verbose,
           'version'=>\$version) or exit 1;

$from =~ s/\/$//;
$to =~ s/\/$//;
$after =~ s/\/$//;
$before =~ s/\/$//;

sub trim($)
{
 my $string = shift;
 $string =~ s/^\s+//;
 $string =~ s/\s+$//;
 return $string;
}

if ($version) {
  print "$PROVETHEMVERSION\n";
  exit;
}

usage if $help;

$file = shift;
die "$usageln\n" if !$file || shift; 

@dolist = split /,/,join(',',@do);
foreach (@dolist) {
  $_ =~ s/\/$//;
}

@butlist = split /,/,join(',',@but);
foreach (@butlist) {
  $_ =~ s/\/$//;
}

$disablelist = join(',',@disable);
$enablelist = join(',',@enable);

die "$file is a directory\n" if -d $file;
open (INFILE,$file) || die "File $file doesn't exist\n";

if (!$out && !$cleanbin && !$execute && !$test) {
  my ($base,$path,$type) = fileparse($file,qr{\..*});  
  $out  = "$path$base";
  my $dol = join('_',@dolist);
  $out .= "-$dol" if $dol;
  my $butl = join('_',@butlist);
  $out .= "-but_$butl" if $butl;
  $out .= "-from_$from" if $from;
  $out .= "-to_$to" if $to;
  $out .= "-after_$after" if $after;
  $out .= "-before_$before" if $before;
  $out .= ".summaries";
  $out .= "-tc" if $typecheckonly;
}

open (OUTFILE,">$out") if $out;

$overopts .= " --Clean" if $cleanbin;
$overopts .= " --Typecheck" if $typecheckonly;
$overopts .= " --disable \"$disablelist\"" if $disablelist;
$overopts .= " --disable-oracles" if $disableoracles;
$overopts .= " --dir $dir" if $dir;
$overopts .= " .$ext" if $ext;
$overopts .= " --lisp $lisp" if $lisp;
$overopts .= " --top $top" if $top;
$overopts .= " --enable \"$enablelist\"" if $enablelist;
$overopts .= " --verbose" if $verbose;
if ($log) {
  $overopts .= " --log";
} else {
  $overopts .= " --no-log";
}

print "Processing $file";
print ". Output in $out" if $out;
print "\n";

$ENV{'PVS_LIBRARY_PATH'}="" if $clearpath;

if ($addpath) {
    $pwd=getcwd;
    $pvslibrarypath = $ENV{'PVS_LIBRARY_PATH'};
    if ($pvslibrarypath) {
 $ENV{'PVS_LIBRARY_PATH'}="$pwd:$pvslibrarypath";
    } else {
 $ENV{'PVS_LIBRARY_PATH'}=$pwd;
    }
}

$act = "Proving";
if ($execute) {
  print "Executing shell command \"$execute\" on library\n";
  print "The output of the execution is in $out\n" if $out;
} elsif ($cleanbin || $typecheckonly) {
  if ($cleanbin) {
    print "Removing binary files from library\n";
    $act = "Cleaning";
  } elsif ($typecheckonly) {
    print "Typechecking library\n";
    $act = "Typechecking";
  }
} else {
  my $pvslp = "PVS_LIBRARY_PATH=$ENV{PVS_LIBRARY_PATH}";
  print "$pvslp\n";
  $summary = "$pvslp\n";
}

$go = "ok" if !($from || $after || @do);

my $totalformulas = 0;
my $totalproofs = 0;
my @libraries=();

while (<INFILE>) {
  $line = $_;
  $line =~ s/\#.*$//;
  $line = trim($line);
  if ($line) {
    @list = split /:/,$line;
    $lib = trim($list[0]);
    $opts = trim($list[1]);
    if ($lib) {
      $go = "ok" if $from eq $lib;
      last if $before eq $lib;
      if (($go || grep { "$_" eq $lib } @dolist) && 
          !(grep { "$_" eq $lib } @butlist)) {
 $command = "";
 if ($execute) {
   if (-d $lib) {
     $pathlib = $lib;
     $baselib = "";
   } elsif (-f $lib) { 
     ($baselib,$pathlib,$typelib) = fileparse($lib,qr{\..*});  
     $baselib .= $typelib;
   } else {
     die "$lib is neither a file nor a directory\n";
   }
   ($exe = $execute) =~ s/\%DIR\%/$pathlib/g;
          $exe =~ s/\%FILE\%/$baselib/g;
   $command = "cd $pathlib;echo \"*** $lib\";$exe";
 } else {
   $command = "$PROVEIT $options $overopts $opts $lib";
 }
 if ($command) {
   if ($test) {
     print "$command\n";
   } else {
            $beginln = sprintf "%-25s",$lib;
     $beginln .= "[";
     print $beginln if !$execute;
     $proveout=`$command`;
     $fail = ($? != 0);
     print OUTFILE "$proveout\n" if $out;
     if ($execute) {
       print "$proveout" if !$out;
     } else {
       if ($fail) {
  $status = "FAIL";
  if ($color) {
    print DARK RED $status; 
  } else {
    print $status;
  }
  print ": $act]\n";
  $summary .= "$beginln$status: $act]\n";
       }
       last if !$force && $fail;
       if (!$fail) {
  if ($cleanbin || $typecheckonly) {
    $status = "OK";
    if ($color) {
      print DARK GREEN $status; 
    } else {
      print $status;
    }
    $endln = ": $act]\n";
  } elsif ($proveout =~ 
    m/Grand Totals: (\d+) proofs, (\d+) attempted, (\d+) succeeded/) {
    $totalformulas += $1;
    if ($1 eq $2 && $2 eq $3) {
      $totalproofs += $1;
      $status = "OK";
      if ($color) {
        print DARK GREEN $status; 
      } else {
        print $status;
      }
      $endln = ": $1 proofs]\n";
    } else {
      $status = "MISS";
      if ($color) {
        print DARK MAGENTA $status; 
      } else {
        print $status;
      }
      $totalproofs += $3;
      my $miss   = $1-$2;
      my $unsucc = $1-$3;
      my $comma = "";
      my $msguna = "";
      if ($miss) {
        $comma = ", ";
        $msguna = "$miss unattempted";
      }
      my $msguns = "$comma$unsucc unsuccessful" if $unsucc;
      $endln = ": $msguna$msguns / $1 formulas]\n";
    }
  } else {
    chomp $proveout;
    $endln = ": $proveout]\n";
  }
  print $endln;
  $summary .= "$beginln$status$endln";
  if (!$cleanbin) {
    $depfile = "$lib/pvsbin/$lib.dep";
    if (-f $depfile) {
      open (DEPFILE,"$depfile");
      while (<DEPFILE>) {
        $line = $_;
        last if $line =~ /:/;
        @list = split /\//,$line;
        if ($list[0] &&  !(grep {$_ eq $list[0]} @prelude) &&
     !grep {$_ eq $list[0]} @libraries) {
   print "*** Warning: Library $list[0] is out of order. It should appear before $lib in $file\n";
        }
      }
      close (DEPFILE);
    } else {
      print "*** Warning: File $depfile not found\n";
    } 
  }
       }
     }
   }
 }
      }
      push(@libraries,$lib) if !$execute && !$cleanbin;
      $go = "ok" if $after eq $lib;
      last if $to eq $lib;
    } else {
      $options .= " $opts";
    }
  }
}

if (!$cleanbin && !$typecheckonly && !$execute) {
  my $missed = $totalformulas-$totalproofs;
  my $mssg = "\n*** Grand Total: $totalproofs proofs / $totalformulas formulas. Missed: $missed formulas.\n";
  print $mssg;
  $summary .= $mssg;
}

close(INFILE);
if ($out) {
  print OUTFILE $summary;
  close(OUTFILE);
}