#!/usr/bin/perl
#
# provethem.in
# Release: ProofLite-7.1.0 (11/05/20)
#
# Contact: Cesar Munoz (cesar.a.munoz@nasa.gov)
# NASA Langley Research Center
# http://shemesh.larc.nasa.gov/people/cam/ProofLite
#
# 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.
#
# Script for batch proving several libraries in PVS 
#

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

$Term::ANSIColor::AUTORESET = 1;

$PVSPATH=/usr/lib64/pvs

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

$OUTPUT_AUTOFLUSH=1;
$VERSION="";
$PROVEIT="$PVSPATH/proveit";

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

sub readVersion() {
  die "PVS could not be located. Please double check PVS installation.\n" if (system("type $PROVEIT > /dev/null 2>&1"));
  $VERSION = `$PVSPATH/pvs -raw -E '(format t "~&~%PROOFLITEVERSION ~a~%~%" *prooflite-version*)(bye)' | grep PROOFLITEVERSION`;
  $VERSION =~ s/^.*PROOFLITEVERSION (.*)[\r\n]*$/\1/;
}


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

$usageln
<option> is
  --addpath               add current directory to PVS_LIBRARY_PATH (default when --clearpath)
  --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
  --clean-only            remove .pvscontext and binary files in the pvsbin folder but 
                          do not prove the libraries. 
  --clean-all             remove .pvscontext and all files in the pvsbin folder but do 
                          not prove the libraries.
  --clearpath             clear 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. If <file>
is not provided, the file name all-theories is assumed. 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>.grandtotals 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 -clean-*, -execute or -test are given.
EOF
  exit;
}

$color = 1;

GetOptions('addpath'=>\$addpath,
           'after=s'=>\$after,
           'before=s'=>\$before,
	   'but=s'=>\@but,
	   'clean-only!'=>\$clean,
	   'cleanbin!'=>\$cleanbin,
	   'clean-all'=>\$cleanall,
	   '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;

die "Error --cleanbin option is not longer supported. Please use --clean-only instead.\n" if $cleanbin;

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

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

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

usage if $help;

$file = shift;
if (!$file) {
    $file = 'all-theories';
} elsif ( ! -f $file ) {
    die "File $file not found\n";
}

die "$usageln\n" if shift; 

my @all_theories=();
open (all_theories_file,$file) || die "File $file doesn't exist\n";
while (<all_theories_file>) {
  $line = $_;
  $line =~ s/\#.*$//;
  $line = trim($line);
  if ($line) {
    @list = split /:/,$line;
    $lib = trim($list[0]);
    push(@all_theories,$lib);
  }
}
close(all_theories_file);

@dolist = split /,/,join(',',@do);
foreach (@dolist) {
  $_ =~ s/\/$//;
  my $dolib = $_;
  die "ERROR: Library $dolib (mentioned in -do paremeter) not found in the current folder.\n" if(! -d $dolib);
  die "ERROR: Library $dolib (mentioned in -do paremeter) not found in the $file file.\n" if(! grep { $dolib eq $_ } @all_theories);
}


@butlist = split /,/,join(',',@but);
foreach (@butlist) {
  $_ =~ s/\/$//;
  my $butlib = $_;
  print "Warning: Library $butlib (mentioned in -but paremeter) not found in the current folder.\n" if(! -d $butlib);
  print "Warning: Library $butlib (mentioned in -but paremeter) not found in the $file file.\n" if(! grep { $butlib eq $_ } @all_theories);
}

$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 && !$cleanall && !$clean && !$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 .= ".grandtotals";
  $out .= "-tc" if $typecheckonly;
}

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

$overopts .= " --clean-only" if (! $cleanall) && $clean;
$overopts .= " --clean-all" if $cleanall;
$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;
$overopts .= " --log" if $log;

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

if ($clearpath) {
  $ENV{'PVS_LIBRARY_PATH'}="";
  $addpath=1;
}

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 ($cleanall || $clean || $typecheckonly) {
  if ($clean) {
    print "Removing .pvscontext and binary files from the pvsbin folder of each library\n";
    $act = "Cleaning";
  } elsif ($cleanall) {
    print "Removing .pvscontext and all files from the pvsbin folder of each 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=();
my $libs = 0;

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)) {
	$libs += 1;
	$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;
	    my $fail_msg;
	    if (! -d $lib) {
	      $fail = 1;
	      $fail_msg = "Library not found";
	      $proveout="Library $lib not found\n";
	      print OUTFILE "$proveout\n" if $out;
	    } else {
	      $proveout=`$command`;
	      $fail += $?;
	      print OUTFILE "$proveout\n" if $out;
	    }
	    if ($execute) {
	      print "$proveout" if !$out;
	    } else {
	      if ($fail > 0) {
		$status = "FAIL";
		if ($color) {
		  print DARK RED $status; 
		} else {
		  print $status;
		}
		if ($fail_msg) {
		  print ": $fail_msg]\n";
		  $summary .= "$beginln$status: $fail_msg]\n";
		} else {
		  print ": $act]\n";
		  $summary .= "$beginln$status: $act]\n";
		}
	      }
	      last if !$force && ($fail > 1);
	      if ($fail == 0) {
		if ($cleanall || $clean || $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 (!$cleanall && !$clean) {
		  $top = "top" if !$top;
		  $depfile = "$lib/pvsbin/$top.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) &&
			  -d $list[0] && -f "$list[0]/$top.pvs") {
			print `pwd`;
			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";
		  } 
		}
	      } else {
		$fail=0;
	      }
	    }
	  }
	}
      }
      push(@libraries,$lib) if !$execute && !$cleanall && !$clean;
      $go = "ok" if $after eq $lib;
      last if $to eq $lib;
    } else {
      $options .= " $opts";
    }
  }
}
 my $mssg = "\n";
if (!$cleanall && !$clean && !$typecheckonly && !$execute) {
  my $missed = $totalformulas-$totalproofs;
  $mssg .= "*** Grand Totals: $totalproofs proofs / $totalformulas formulas. Missed: $missed formulas.\n";
}
$mssg .= "*** Number of libraries: $libs\n"; 
print $mssg;
$summary .= $mssg;

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