provethem.in

#!/usr/bin/env 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.
#
# Mariano Moscato (04/26/2021)
# National Institute of Aerospace
#
# Script for batch proving several libraries in PVS 
#

use Getopt::Long qw(GetOptionsFromString);
use File::Basename;
use Term::ANSIColor qw(:constants);
use Cwd;
use File::Temp qw/ tempdir /;

$Term::ANSIColor::AUTORESET = 1;

$PVSPATH="@PVSPATH@";

@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)' 2> /dev/null | grep PROOFLITEVERSION`;
  $VERSION =~ s/^.*PROOFLITEVERSION (.*)[\r\n]*$/\1/;
}

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

$usageln
<option> is
  --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>
  --do=<dir1>,..,<dirn>   process libraries <dir1>,...,<dirn>
  --from=<dir>            prove all libraries from <dir>, inclusive.
  --to=<dir>              prove all libraries to <dir>, inclusive.

  --top <th>              use <th>.pvs instead of top.pvs as top theory  

  --force                 force iteratelibs to go even if there is a proveit error

  --lisp <lisp>           specify lisp version; <lisp> is one of allegro,cmulisp
			  
  --out <outfile>         save output to <outfile>
  
  --no-color              do not use colors

  --dry-run               process <file> but do not call proveit

  --verbose               print summary information for all theories
  --version               print version information and exit
  
  --addpath               add current directory to PVS_LIBRARY_PATH (default when --clearpath)
  --clearpath             clear PVS_LIBRARY_PATH 

  --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.
  --typecheck-only        typecheck but do not prove the libraries
  --execute <command>     execute Unix <command> on all libraries. Command 
                          may refer to \%DIR\% and \%FILE\%

  --disable <o1,...on>    disable external oracles o1,...,on.
  --disable-oracles       disable any external oracle
  --enable <o1,..,on>     enable external oracles o1,..,on. Overwrite --disable

  --dir <dir>             use <dir> as default directory of summary files
  --ext <ext>             use <ext> as default extension of summary files

  --log                   log all information generated by PVS in <file>.log 


File <file> is an ordered list of libraries to be processed by proveit. If <file>
is not provided, the file name all-libraries 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 provided, an output file is not created when
the options -clean-*, -execute, or --dry-run are given.
EOF
  exit;
}

GetOptions('addpath'=>\$addpath2,
           'clean-only'=>\$clean2,
	   'clean-all'=>\$cleanall2,
	   'clearpath'=>\$clearpath2,
           'dir=s'=>\$dir2,
	   'disable=s'=>\@disable2,
           'disable-oracles'=>\$disableoracles2,
	   'ext=s'=>\$ext2,
           'lisp=s'=>\$lisp2,
	   'log' => \$log2,
           'enable=s'=>\@enable2,
           'typecheck-only'=>\$typecheckonly2,
	   'after=s'=>\$after2,
           'before=s'=>\$before2,
	   'but=s'=>\@but2,
	   'no-color'=>\$no_color2,
           'do=s'=>\@do2,
           'execute=s'=>\$execute2,
	   'force'=>\$force2,
           'from=s'=>\$from2,
	   'help'=>\$help,
           'out=s'=>\$out2,
	   'dry-run'=>\$dryrun2,
           'to=s'=>\$to2,
           'top=s'=>\$top2,
	   'verbose'=>\$verbose2,
           'version'=>\$version,
	   'debug'=>\$debug,
	   'action-name=s'=>\$act,
	   'ret-val-label=s'=>\%ret_val_labels,
	   'no-printout'=>\$no_printout,	   
	  ) or exit 1;

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

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

$top = "top" if !$top;


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

usage if $help;

$file = shift;
if (!$file) {
  if ( -f 'all-libraries' ) {
    $file = 'all-libraries';
  } elsif ( -f 'all-theories' ) {
    print "*** Warning: all-theories is no longer supported as default input file name, please rename it as all-libraries.\n";
    $file = 'all-theories';
  } else {
    $file = 'all-libraries';
    
    print "*** Warning: input file not found. Generating $file file...\n";

    opendir(current_directory, ".");
    my @files = readdir(current_directory);
    closedir(current_directory);

    my %lib_deps;
    my @all_libraries=();
    foreach my $file_in_dir (@files) {
      # skip . and ..
      next if($file_in_dir =~ /^\.$/);
      next if($file_in_dir =~ /^\.\.$/);

      if (-d $file_in_dir) {
	my @files_in_subdir = glob ("$file_in_dir/*.pvs");

	# Only take into considerations folders that have at least one pvs file
	if ( scalar @files_in_subdir > 0) {
	  push(@all_libraries,$file_in_dir);

	  # look into the pvsbin/top.dep file to check dependencies
	  $depfile = "$file_in_dir/pvsbin/$top.dep";
	  if (-f $depfile) {
	    open (DEPFILE,"$depfile");
	    while (<DEPFILE>) {
	      $line = $_;
	      last if $line =~ /:/;
	      if ($line =~ /^\[WSS\].*$/) {
		@list = split /\//,$line;
		if (scalar(@list) >= 2) {
		  my $deplib=$list[scalar(@list)-2];
		  push(@{$lib_deps{$file_in_dir}}, $deplib);
		} else {
		  print "*** Warning: Cannot check library order. Obsolete dep file for library $lib? Try regenerating it.\n";
		}
	      }
	    }
	    close (DEPFILE);
	  } else {
	    print "*** Warning: File $depfile not found.\n";
	  } 
	}
      }
    }

    # Order the arrays of libraries in function
    # of its dependencies.
    my $lib_cmp = sub($$) {
      my $a = $_[0];
      my $b = $_[1];
      my $result=0;
      if (exists $lib_deps{$a} && grep { $b eq $_ } @{$lib_deps{$a}}){
	$result=1;
      } elsif (exists $lib_deps{$b} && grep { $a eq $_ } @{$lib_deps{$b}}){
	$result=-1;
      } 
      return $result;
    };
    @all_libraries = sort {$lib_cmp->($a,$b)} @all_libraries;

    # Finally, print the list into the all-libraries file.
    open (all_libraries_file,">$file");
    my $datestring = localtime();
    print all_libraries_file "# This file was generated automatically by iterateblis on $datestring \n";
    print all_libraries_file join("\n",@all_libraries), "\n";
    close(all_libraries_file);

    print "done\n";
  }
} elsif ( ! -f $file ) {
    die "File $file not found\n";
}

die "$usageln\n" if shift; 

my $can_accept_in_file_global_options=1;

my @all_theories=();
open (all_theories_file,$file) || die "File $file not found\n";
while (<all_theories_file>) {
  $line = $_;
  $line =~ s/\#.*$//;
  $line = trim($line);

  if ($line =~ m/^-.*$/) {
    die "ERROR: global options misplaced ",
      "(line ",${\*all_theories_file}->input_line_number,
      " in $file)" unless ($can_accept_in_file_global_options);
    GetOptionsFromString($line,
			 'addpath'=>\$addpath,
			 'clean-only'=>\$clean,
			 'clean-all'=>\$cleanall,
			 'clearpath'=>\$clearpath,
			 'dir=s'=>\$dir,
			 'disable=s'=>\@disable,
			 'disable-oracles'=>\$disableoracles,
			 'ext=s'=>\$ext,
			 'lisp=s'=>\$lisp,
			 'log' => \$log,
			 'enable=s'=>\@enable,
			 'typecheck-only'=>\$typecheckonly,
			 'after=s'=>\$after,
			 'before=s'=>\$before,
			 'but=s'=>\@but,
			 'no-color'=>\$no_color,
			 'do=s'=>\@do,
			 'execute=s'=>\$execute,
			 'force'=>\$force,
			 'from=s'=>\$from,
			 'out=s'=>\$out,
			 'dry-run'=>\$dryrun,
			 'to=s'=>\$to,
			 'top=s'=>\$top,
			 'verbose'=>\$verbose) or exit 1;
  } elsif ($line) {
    $can_accept_in_file_global_options=0;
    @list = split /:/,$line;
    $lib = trim($list[0]);
    push(@all_theories,$lib);
    $overopts .= " ".$list[1] if !$lib && $list[1];
  }
}
close(all_theories_file);

#
# Command-line options overrides input file options
#

sub override_scalar_option {
  my ($arg_name,$arg,$arg2) = @_;

  if ($arg2 && $arg ne $arg2) {
    print "*** Warning: overriding $arg_name option in $file by $arg2.\n" if $arg;
    $arg=$arg2;
  }
  return $arg;
}

sub clean_scalar_option {
  my ($arg_name,$arg,$cond) = @_;
  if ($cond) {
    print "*** Warning: omitting $arg_name option in $file overriden by command-line option.\n" if $arg;
    $arg = "";
  }
  return $arg;
}

# - scope
$after=override_scalar_option("--after",$after,$after2);
$before=override_scalar_option("--before",$before,$before2);
$from=override_scalar_option("--from",$from,$from2);
$to=override_scalar_option("--to",$to,$to2);
$top=override_scalar_option("--top",$top,$top2);
$addpath=override_scalar_option("--addpath",$addpath,$addpath2);
$clean=override_scalar_option("--clean",$clean,$clean2);
$cleanall=override_scalar_option("--cleanall",$cleanall,$cleanall2);
$clearpath=override_scalar_option("--clearpath",$clearpath,$clearpath2);
$dir=override_scalar_option("--dir",$dir,$dir2);
$ext=override_scalar_option("--ext",$ext,$ext2);
$lisp=override_scalar_option("--lisp",$lisp,$lisp2);
$log=override_scalar_option("--log",$log,$log2);
$typecheckonly=override_scalar_option("--typecheck-only",$typecheckonly,$typecheckonly2);

$disableoracles=override_scalar_option("--disable-oracles",$disableoracles,$disableoracles2);

@enablelist = split /,/,join(',',@do);
@enablelist2 = split /,/,join(',',@do2);
@disablelist = split /,/,join(',',@but);
@disablelist2 = split /,/,join(',',@but2);
@disablelist=@disablelist2 if @disablelist2;
if (!@disablelist2 && @disablelist && @enablelist2) {
  my @disable_tmp;
  foreach $e (@disablelist) {
    if (grep( /^$e$/, @enablelist2 )) {
      print "*** Warning: overriding '--disable $e' in $file since it is included in --enable command-line option.\n"
    } else {
      push @disable_tmp, $e;
    }
  }
  @disablelist=@disable_tmp;
}

@enablelist=@enablelist2 if @enablelist2;
if (!@enablelist2 && @enablelist && @disablelist2) {
  my @enable_tmp;
  foreach $e (@enablelist) {
    if (grep( /^$e$/, @disablelist2 )) {
      print "*** Warning: overriding '--enable $e' in $file since it is included in --disable command-line option.\n"
    } else {
      push @enable_tmp, $e;
    }
  }
  @enablelist=@enable_tmp;
}

@dolist = split /,/,join(',',@do);
@dolist2 = split /,/,join(',',@do2);
@butlist = split /,/,join(',',@but);
@butlist2 = split /,/,join(',',@but2);

@butlist=@butlist2 if @butlist2;
if (!@butlist2 && @butlist && @dolist2) {
  my @but_tmp;
  foreach $e (@butlist) {
    if (grep( /^$e$/, @dolist2 )) {
      print "*** Warning: overriding '--but $e' in $file since it is included in --do command-line option.\n"
    } else {
      push @but_tmp, $e;
    }
  }
  @butlist=@but_tmp;
}

@dolist=@dolist2 if @dolist2;
if (!@dolist2 && @dolist && @butlist2) {
  my @do_tmp;
  foreach $e (@dolist) {
    if (grep( /^$e$/, @butlist2 )) {
      print "*** Warning: overriding '--do $e' in $file since it is included in --but command-line option.\n"
    } else {
      push @do_tmp, $e;
    }
  }
  @dolist=@do_tmp;
}

# - actions
$execute=override_scalar_option("--execute",$execute,$execute2);
# - misc
$no_color=override_scalar_option("--no-color",$no_color,$no_color2);
$force=override_scalar_option("--force",$force,$force2);
$out=override_scalar_option("--out",$out,$out2);
$dryrun=override_scalar_option("--dry-run",$dryrun,$dryrun2);
$verbose=override_scalar_option("--verbose",$verbose,$verbose2);
$checkdep= !$execute && !$clean && !$cleanall;

#
# Options check
#
sub check_arg_lib {
  my ($arg_name,$lib,$die_on_error) = @_;
  my $error_msg;
  if(! -d $lib) {
    $error_msg = "Library $lib (mentioned in $arg_name option)".
      " not found in the current folder.\n";
  } elsif (! grep { $lib eq $_ } @all_theories) {
    $error_msg = "Library $lib (mentioned in $arg_name option)".
      " not found in the $file file.\n";
  }

  if($error_msg){
    print "ERROR: " if $die_on_error;
    print "*** Warning: " unless $die_on_error;
    print $error_msg;
    exit 1 if $die_on_error;
  }
}

sub iteratelibs(){
  print "Executing shell command \"$execute\" on each library.\n" if $verbose;
  print "With overopts: $overopts.\n" if $verbose && $execute=~/\%OVEROPTS\%/;
  print "\n";
  while (<INFILE>) {
    $line = $_;
    $line =~ s/\#.*$//;
    $line = trim($line);

    # ommit command-line options
    next if ($line =~ m/^ *-.*$/);
    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;
	  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;
	  $exe =~ s/\%OVEROPTS\%/$overopts/g;
	  $exe =~ s/\%OPTS\%/$opts/g;
	  $command="";
	  $command .= "$exe";
	
	  if ($command) {
	    if ($dryrun) {
	      print "DRY-RUN: $command\n";
	    } else {
	      $beginln = sprintf "%-25s",$lib;
	      $beginln .= "$act... ";
	      print $beginln;
	      my $fail_msg;
	      my $warn_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 = ($? >> 8);
		
		print OUTFILE "$proveout\n" if $out;
		
		my @warnings = ($proveout =~ m/(Warning[:]? .*)/g);
		if (@warnings) {
		  $warn_msg = join("\n*** ",@warnings);
		}
	      
		my @errors = ($proveout =~ m/(Error[:]? .*)/g);
		if (@errors) {
		  $fail_msg = join("\n*** ",@errors);
		}
	      }

	      if ($fail > 0) {
		$status = "FAIL";
		my $custom_status=$ret_val_labels{$fail};
		$status=$custom_status if $custom_status;
		print "[";
		if ($no_color) {
		  print $status;
		} else {
		  print DARK RED $status; 
		}
		$fail_msg .= "($fail)" if $verbose;
		if ($fail_msg) {
		  print "]\n*** $fail_msg\n";
		  $summary .= "$beginln$status: $fail_msg]\n";
		} else {
		  print "]\n";
		  $summary .= "$beginln$status]\n";
		}
	      }
	    
	      if ($fail == 0) {
		$status = $ret_val_labels{0};
		$status = "OK" if ! $status;
		print "[";
		$beginln.= "[";
		if ($no_color) {
		  print $status;
		} else {
		  print DARK GREEN $status; 
		}
		$endln = "]\n";
		print $endln;
		print "\n$proveout\n" if $proveout && !$no_printout;
	      }
	      # Only print warnings if the proveout is not printed
	      # since warnings are already there.
	      print "*** $warn_msg\n" if $warn_msg && $no_printout;

	      $summary .= "$beginln$status$endln";
	    
	      $depfile = "$lib/pvsbin/$top.dep";
	      if (-f $depfile) {
		open (DEPFILE,"$depfile");
		while (<DEPFILE>) {
		  $line = $_;
		  last if $line =~ /:/;
		  if ($line =~ /^\[WSS\].*$/) {
		    @list = split /\//,$line;
		    if (scalar(@list) >= 2) {
		      my $deplib=$list[scalar(@list)-2];
		      if ($deplib && $deplib ne $lib && !(grep {$_ eq $deplib} @prelude) &&
			  !(grep {$_ eq $deplib} @libraries) &&
			  -d $deplib && -f "$deplib/$top.pvs") {
			print "*** Warning: Library $deplib is out of order. It should appear before $lib in $file\n";
		      } 
		    } else {
		      print "*** Warning: Cannot check library order. Obsolete dep file for library $lib? Try regenerating it.\n";
		    }
		  }
		}
		close (DEPFILE);
	      } elsif ( $checkdep ) {
		print "*** Warning: File $depfile not found.\n";
	      }
	      last if !$force && ($fail > 1) && !$ret_val_labels{$fail};
	    }
	  }
	}
	push(@libraries,$lib);
	$go = "ok" if $after eq $lib;
	last if $to eq $lib;
      } else {
	$options .= " $opts";
      }
    }
  }
  my $mssg = "\n";
  $mssg .= "*** Number of libraries: $libs\n"; 
  print $mssg;
  $summary .= $mssg;

  close(INFILE);

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


#
# Main
#

check_arg_lib("--from",$from,1) if $from;
check_arg_lib("--to",$to,1) if $to;
check_arg_lib("--before",$before,1) if $before;
check_arg_lib("--after",$after,1) if $after;

foreach (@dolist) {
  $_ =~ s/\/$//;
  my $dolib = $_;
  check_arg_lib("--do",$dolib,1);
}

foreach (@butlist) {
  $_ =~ s/\/$//;
  my $butlib = $_;
  check_arg_lib("--but",$butlib,0);
}

die "$file is a directory\n" if -d $file;

open (INFILE,$file) || die "File $file not found\n";

if (!$out && !$cleanall && !$clean && !$execute && !$dryrun) {
  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;

print "Working on libraries file: $file.\n";
print "Output in $out.\n" if $out && $verbose;

$act = "Proving" unless $act || ($exec ne "");
$act = "Processing" unless $act;

# Set global options
$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;

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

if ($clearpath) {
  print "Cleaning PVS_LIBRARY_PATH variable.\n";
  $ENV{'PVS_LIBRARY_PATH'}="";
  $addpath=1;
}

if ($addpath) {
    $pwd=getcwd;
    print "Adding $pwd to PVS_LIBRARY_PATH.\n";
    $pvslibrarypath = $ENV{'PVS_LIBRARY_PATH'};
    if ($pvslibrarypath) {
	$ENV{'PVS_LIBRARY_PATH'}="$pwd:$pvslibrarypath";
    } else {
	$ENV{'PVS_LIBRARY_PATH'}="$pwd";
    }
}

my @libraries=();
my $libs = 0;

if(!$execute){
  # If no command has been given, the command to iterate is
  # assumend to be proveit
  $execute="proveit %OVEROPTS% %OPTS% %DIR%";

  my $tmp_dir;
  
  if(!$out){
    $out="provethem.out";
    $tmp_dir = tempdir( CLEANUP => 1 );
    $out="$tmp_dir/$out";
  }

  $ret_val_labels{'142'}="MISS";

  $no_printout="t";
  
  iteratelibs();

  my $totalformulas = 0;
  my $totalproofs = 0;
  my $libs = 0;
  if(-f "$out") {
    open (TMPFILE,"$out") || die "File $out not found\n";
    while (<TMPFILE>) {
      my $line=$_;
      $line = trim($line);
      if ($line =~ m/Grand Totals: (\d+) proofs, (\d+) attempted, (\d+) succeeded \(([\d\.]+ s)\)/) {
	$totalformulas += $1;
	$totalproofs += $3;
	$libs += 1;
      }
    }  
    close(TMPFILE);
  }

  my $mssg = "";
  if (!$cleanall && !$clean && !$typecheckonly) {
    my $missed = $totalformulas-$totalproofs;
    $mssg .= "*** Grand Totals: $totalproofs proofs / $totalformulas formulas. Missed: $missed formula";
    $mssg .= "s" if $missed != 1;
    $mssg .= ".\n";
  }
  print $mssg;
  $summary .= $mssg;
} else {
  iteratelibs();  
}