|
|
|
|
Quelle provethem.in
Sprache: unbekannt
|
|
#!/usr/bin/env perl
#
# provethem.in
# Release: ProofLite-6.0.9 (3/14/14)
#
# 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="@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);
}
[ Dauer der Verarbeitung: 0.6 Sekunden
(vorverarbeitet)
]
|
2026-03-28
|
|
|
|
|
