#!/bin/sh
#
# proveit.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 in PVS
#
PVSPATH=@PVSPATH@
VERSION="ProofLite-6.0.9 (3/14/14)"
export PROVEITVERSION="proveit - $VERSION"
#-------------------------------------------------
# Nothing below this line should need modification
#
# Extension for proof status summary file
EXT=.summary
# PVS directory of binary files
PVSBIN=pvsbin
LISPFORCE=t
LISPIMPORT=nil
LISPSCRIPTS=t
LISPTRACES=nil
LISPTXTPROOFS=nil
LISPTEXPROOFS=nil
LISPTYPECHECK=nil
LISPDEPENDENCIES=nil
PRELUDEXT=
DISABLE=
ENABLE=
CLEAN=
LOG=
QUIET=
DEBUG=
OUTDIR=
TOP=top
NOFILE=yes
reset_vars() {
FILENOTFOUND=
ARG=
OPTS=
OUTFILE=
LOGFILE=
PVSCONTEXT=
PVSFILE=
THFS=
THEORIES=
LISPDEPENDENCIES=nil
}
all_opt() {
if [ -z "$FILENOTFOUND" ]; then
QUIET=yes
if [ -z "$CLEAN" ]; then
CLEAN=yes
fi
if [ "$CLEAN" = "only" ]; then
QUIET=
fi
LISPIMPORT=t
LISPSCRIPTS=nil
fi
}
# $ARG has the general form
# <dir> | <file>[.pvs] | [<dir>@]<thf1>,..,<thfn>, where
# <thfi> has the form <th>[.<f1>:..:<fm>]
compile_infile_name() {
# If <dir>, set context to <dir> and pvsfile to top.pvs
if [ -d $ARG ]; then
PVSCONTEXT=$ARG
if [ -z "$OUTFILE" ]; then
OUTFILE=$ARG$EXT
fi
PVSFILE=`basename $TOP .pvs`
if [ -f $PVSCONTEXT/$PVSFILE.pvs ]; then
all_opt
else
FILENOTFOUND="$PVSCONTEXT/$PVSFILE.pvs"
fi
LISPDEPENDENCIES=t
# If <file>, set context to its dirname and pvsfile to its base name
else
PVSCONTEXT=`dirname $ARG`
PVSFILE=`basename $ARG .pvs`
if [ ! -f $PVSCONTEXT/$PVSFILE.pvs ]; then
case $ARG in
*@*) predir=`echo $ARG | sed -e "s/\([^@]*\)@.*/\1/"`
THFS=`echo $ARG | sed -e "s/[^@]*@//"`
if [ -z "$predir" ]; then
PVSCONTEXT="."
else
if [ -d "$predir" ]; then
PVSCONTEXT=$predir
else
echo "Error: $predir is not a directory"
exit 1
fi
fi
if [ "$THFS" ]; then
PVSFILE=$THFS
THEORIES=`echo $THFS | sed -e "s/\..*,/,/g" -e "s/\..*//"`
else
echo "Error: At least one theory has to be specified in $ARG"
exit 1
fi;;
*) FILENOTFOUND="$PVSCONTEXT/$PVSFILE.pvs"
if [ -z "$NOFILE" ]; then
echo "Error: File $FILENOTFOUND not found"
exit;
fi;;
esac
fi
fi
}
strip_ext() {
echo "$1" | sed -e "s/\(.*\)\..*/\1/g"
}
# If necessary, set the name of the output file
#
compile_outfile_names() {
dir=$OUTDIR
if [ -z "$OUTFILE" ]; then
if [ -z "$dir" ]; then
dir=$PVSCONTEXT
fi
OUTFILE=$PVSFILE$EXT
else
if [ -z "$dir" ]; then
dir=`dirname $OUTFILE`
fi
fi
base=`basename $OUTFILE`
BASEOUT=`strip_ext $base`
if [ "$BASEOUT" = $base ]; then
base=$BASEOUT$EXT
fi
OUTFILE=$dir/$base
LOGFILE=$dir/$BASEOUT.log
if [ "$LISPTYPECHECK" = "t" ]; then
OUTFILE=$OUTFILE-tc
LOGFILE=$LOGFILE
fi
}
# Translate a list l1,...,ln into (l1 .. ln)
list_to_lisp() {
if [ -z "$1" ]
then
echo nil
else
echo "(\"$1\")" | sed -e "s/,/\" \"/g"
fi
}
# append e l = e,le. Check for the special case when l is empty
append() {
if [ -z "$2" ]; then
echo "$1"
else
echo "$2,$1"
fi
}
# Take care of the optional cleaning
#
cleanup() {
if [ "$CLEAN" ]
then
if [ -z "$QUIET" ]
then
echo "Removing $PVSCONTEXT/.pvscontext $PVSCONTEXT/$PVSBIN/ $OUTFILE $LOGFILE"
fi
rm -r -f $PVSCONTEXT/.pvscontext $PVSCONTEXT/$PVSBIN/*.* $OUTFILE $LOGFILE
fi
}
# Help print command
#
usage() {
echo "NAME
$PROVEITVERSION -- runs PVS in batch mode
SYNOPSIS
proveit <option> ... <dir> | <file>[.pvs] | [<ctxt>]@<thf1>,..,<thfn> ...
where <thfi> has the form <th>[.<f1>:..:<fm>]
DESCRIPTION
If directory <dir> is provided, prove all theories imported in
<dir>/top.pvs. If a PVS <file> is provided, prove all theories
defined in it. The proof status is saved in the working directory in
a file that can be specified using the option -out. Otherwise, a
default name of the form <dir>$EXT or <file>$EXT is used depending
on the given options.
TYPICAL USE
* If <dir> is a library, e.g., there is a file <dir>/top.pvs that
imports all other theories in <dir>, then type: \$proveit <dir>
* If <file>.pvs is a regular PVS file, then type: \$proveit <file>
* If <file>.pvs is a regular PVS file and want to reprove all
formulas, including those in imported files, then type:
\$proveit -a <file>
ADVANCED USE
In the more general form, a context, a list of theories, and a list of
formulas are specified using the syntax <[ctxt]@thf1,..,thfn>, where <ctxt>
is a directory and each <thfi> has the form <th[.f1:..:fm]> with <th> being a
theory and <f1:..:fn> a list of formulas in <th>. Only formulas specified
this way are proven by PVS. In this case, the proof status is saved
in <th.f1:..:fm>$EXT in <ctxt>. For example, to prove formulas <f1> and
<f2> in theory <theory> in the current context, type:
\$proveit @<theory>.<f1>:<f2>
OPTIONS
Options are processed in the order they appear. One letter options can be
combined.
-a|--all equivalent to -ciq -p Field
-c|--clean remove bin files and .pvscontext
-C|--clean-only clean but do not typecheck or prove the theory
-d|--dir <dir> use <dir> as default directory of summary files
--dependencies compute theory dependencies and save them in pvsbin/<outfile>.dep.
By default, dependencies are computed when proving a directory
--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> use <ext> as default extension of summary files
-f|--force force proof reruns (default)
~f|--no-force don't force proof reruns
-h|--help print this message
-i|--importchain prove chain of imported theories (set --no-scripts)
~i|--no-importchain don't prove chain of imported theories (default)
--lisp <lisp> specify lisp version; <lisp> is one of allegro,cmulisp
-l|--log log all information generated by PVS in <outfile>.log
~l|--no-log don't log PVS information (default)
-o|--out <outfile> save the proof status summary in <outfile>
-p|--prelude-ext <p1,..,pn> load prelude extensions p1,..,pn
~p|--no-prelude-ext don't load any prelude extension
-q|--quiet print only untried and unfinished proofs per theory,
and grand total
-s|--scripts install ProofLite scripts (default)
~s|--no-scripts don't install ProofLite scripts
--tex generate LaTeX proof files in directory pvstex
--no-tex don't generate LaTeX proof files (default)
--txt generate text proof files in directory pvstxt
--no-txt don't generate text proof files (default)
-t|--top <th> use <th>.pvs instead of top.pvs when proving a directory
--traces include proof traces in log file
--no-traces don't include proof traces in log file (default)
-T|--typecheck-only typecheck but do not prove the theory
-v|--verbose print proof status information per theory and grand
total (default)
--version print version information and exit
SEE ALSO
provethem -- for iterating proveit on a list of directories
"
}
# Print error output
error_output() {
sed -i.bak -n -e '/^<pvserror/,/^<\/pvserror/p'\
-e '/^Restored .*/d'\
-e '/^\*\*\* /p'\
-e '/^Typechecking/h'\
-e '/^Typechecking/ !{
/^Typecheck error/ {
p;g;p
}
/^Typecheck error/! {
/^PVS file .* is not/h
/^PVS file .* is not/!H
}
}'\
-e '/Proof summary/,/Grand Totals/p' $OUTFILE
if [ -z "$QUIET" ]; then
cat $OUTFILE | \
sed -e "s+^<pvserror msg=\"\(.*\)\">+\1 ($ARG)+" \
-e 's/"//g' -e '/^<\/pvserror>/d' \
-e '/^\*\*\*.*/d'
else
cat $OUTFILE | \
sed -n -e "s+^<pvserror msg=\"\(.*\)\">+\1 ($ARG)+p" \
-e "s/^\"\(.*\)\"$/\1/p" -e "/^Typecheck error/p"
fi
if [ "$LOG" ]; then
mv -f $OUTFILE.bak $LOGFILE
else
rm $OUTFILE.bak
fi
}
# Pretty print PVS output
pvs_output() {
sed -i.bak -n -e '/File .*\.pvs typechecked/p'\
-e '/^\*\*\* /p'\
-e '/Proof summary/,/Grand Totals/p' $OUTFILE
cat $OUTFILE | quiet_output
if [ "$LOG" ]; then
mv -f $OUTFILE.bak $LOGFILE
else
rm $OUTFILE.bak
fi
}
# quiet output
quiet_output() {
if [ -z "$QUIET" ]
then
sed -n -e '/File/p'\
-e '/Proof summary/h'\
-e '/Proof summary/ !{
/unfinished/H
/unchecked/H
/untried/H
}'\
-e '/Theory totals/ {
i\
x;p;g;p
}' \
-e '/^Grand Totals:/ {
i\
p
}'
else
sed -n -e '/Proof summary/h'\
-e '/Proof summary/ !{
/unfinished/H
/unchecked/H
/untried/H
}'\
-e '/Theory totals/ {
H;g
/\.\.\.\./p
}'\
-e '/^Grand Totals:/p'
fi
}
process_opts() {
while [ $# -gt 0 ]
do
case $1 in
-a|all|--all)
all_opt;;
-c|-clean|--clean)
CLEAN=yes;;
-C|-Clean|--Clean|-clean-only|--clean-only)
QUIET=
CLEAN=only;;
~c|-no-clean|--no-clean)
CLEAN=;;
-dep|--dep|-dependencies|--dependencies)
LISPDEPENDENCIES=t;;
-f|-force|--force)
LISPFORCE=t;;
~f|-no-force|--no-force)
LISPFORCE=nil;;
-i|-importchain|--importchain)
LISPSCRIPTS=nil
LISPIMPORT=t;;
~i|-no-importchain|--no-importchain)
LISPIMPORT=nil;;
-s|-scripts|--scripts)
LISPSCRIPTS=t;;
~s|-no-scripts|--no-scripts)
LISPSCRIPTS=nil;;
-T|-Typecheck|--Typecheck|-typecheck-only|--typecheck-only)
LISPTYPECHECK=t;;
-traces|--traces)
LOG=yes
LISPTRACES=t;;
-no-traces|--no-traces)
LISPTRACES=nil;;
-txt|--txt)
LISPTXTPROOFS=t;;
-no-txt|--no-txt)
LISPTXTPROOFS=nil;;
-tex|--tex)
LISPTEXPROOFS=t;;
-no-tex|--no-tex)
LISPTEXPROOFS=nil;;
-l|-log|--log)
LOG=yes;;
~l|-no-log|--no-log)
LOG=;;
~p|-no-prelude-ext|--no-prelude-ext)
PRELUDEXT=;;
-q|-quiet|--quiet)
QUIET=yes;;
-v|-verbose|--verbose)
QUIET=;;
--*)
usage
echo "Error: $1 is not a valid option"
exit 1;;
-*)
opts=`echo "$1" | sed -e s/-//g -e "s/\(.\)/\1 /g"`
for opt in $opts; do
case $opt in
a)
all_opt;;
c)
CLEAN=yes;;
C)
QUIET=
CLEAN=only;;
f)
LISPFORCE=t;;
s)
LISPSCRIPTS=t;;
v)
QUIET=;;
i)
LISPSCRIPTS=nil
LISPIMPORT=t;;
l)
LOG=yes;;
q)
QUIET=yes;;
T)
LISPTYPECHECK=t;;
*)
usage
echo "Error: -$opt is not a valid option"
exit 1;;
esac
done;;
~*)
opts=`echo "$1" | sed -e s/~//g -e "s/\(.\)/\1 /g"`
for opt in $opts; do
case $opt in
c)
CLEAN=;;
f)
LISPFORCE=nil;;
i)
LISPIMPORT=nil;;
s)
LISPSCRIPTS=nil;;
l)
LOG=;;
p)
PRELUDEXT=;;
*)
usage
echo "Error: ~$opt is not a valid option"
exit 1;;
esac
done
esac
shift
done
}
# Main Function
proveit() {
compile_infile_name
if [ "$CLEAN" = "only" ]; then
cleanup
else
process_opts $OPTS
if [ "$DEBUG" ]; then
QUIET=
LOG=y
fi
compile_outfile_names
cleanup
if [ "$FILENOTFOUND" ]; then
if [ -z "$CLEAN" ]; then
echo "Error: File $FILENOTFOUND not found"
fi
exit 1
fi
echo Processing $PVSCONTEXT/$PVSFILE.pvs. Writing output to file $OUTFILE
if [ "$LOG" ]; then
echo "Logging PVS information in $LOGFILE"
fi
if [ -z "$QUIET" ]; then
if [ "$PRELUDEXT" ]; then
echo "Loading prelude extensions: $PRELUDEXT"
fi
if [ "$DISABLE" ]; then
if [ "$DISABLE" = "_" ]; then
echo "Disabling any external oracle"
else
echo "Disabling oracles: $DISABLE"
fi
fi
if [ "$ENABLE" ]; then
echo "Enabling oracles: $ENABLE"
fi
if [ "$LISPIMPORT" = "t" ]; then
echo "Proving chain of imported theories"
fi
if [ "$LISPDEPENDENCIES" ]; then
echo "Saving theory dependencies in directory pvsbin"
fi
if [ "$LISPSCRIPTS" != "t" ]; then
echo "ProofLite scripts won't be installed"
fi
if [ "$LISPFORCE" != "t" ]; then
echo "Proofs won't be forced"
fi
if [ "$LISPTRACES" = "t" ]; then
echo "Including proof traces in output file"
fi
if [ "$LISPTXTPROOFS" = "t" ]; then
echo "Generating text proof files in directory pvstxt"
fi
if [ "$LISPTEXPROOFS" = "t" ]; then
echo "Generating LaTeX proof files in directory pvstex"
fi
fi
export PROVEITPVSCONTEXT="$PVSCONTEXT"
export PROVEITPVSFILE="$PVSFILE"
export PROVEITBASEOUT="$BASEOUT"
export PROVEITLISPIMPORT="$LISPIMPORT"
export PROVEITLISPSCRIPTS="$LISPSCRIPTS"
export PROVEITLISPTRACES="$LISPTRACES"
export PROVEITLISPFORCE="$LISPFORCE"
export PROVEITLISPTYPECHECK="$LISPTYPECHECK"
export PROVEITLISPTXTPROOFS="$LISPTXTPROOFS"
export PROVEITLISPTEXPROOFS="$LISPTEXPROOFS"
export PROVEITLISPDEPENDENCIES="$LISPDEPENDENCIES"
export PROVEITLISPPRELUDEXT="`list_to_lisp $PRELUDEXT`"
export PROVEITLISPDISABLE="`list_to_lisp $DISABLE`"
export PROVEITLISPENABLE="`list_to_lisp $ENABLE`"
export PROVEITLISPTHFS="`list_to_lisp $THFS`"
export PROVEITLISPTHEORIES="`list_to_lisp $THEORIES`"
if [ "$DEBUG" ]; then
echo "PROVEITVERSION: $PROVEITVERSION"
echo "OUTFILE: $OUTFILE"
echo "LOGFILE: $LOGFILE"
echo "PROVEITPVSCONTEXT: $PROVEITPVSCONTEXT"
echo "PROVEITPVSFILE: $PROVEITPVSFILE"
echo "PROVEITBASEOUT: $PROVEITBASEOUT"
echo "PROVEITLISPIMPORT: $PROVEITLISPIMPORT"
echo "PROVEITLISPSCRIPTS: $PROVEITLISPSCRIPTS"
echo "PROVEITLISPTRACES: $PROVEITLISPTRACES"
echo "PROVEITLISPFORCE: $PROVEITLISPFORCE"
echo "PROVEITLISPTYPECHECK: $PROVEITLISPTYPECHECK"
echo "PROVEITLISPTXTPROOFS: $PROVEITLISPTXTPROOFS"
echo "PROVEITLISPTEXPROOFS: $PROVEITLISPTEXPROOFS"
echo "PROVEITLISPDEPENDENCIES: $PROVEITLISPDEPENDENCIES"
echo "PROVEITLISPPRELUDEXT: $PROVEITLISPPRELUDEXT"
echo "PROVEITLISPDISABLE: $PROVEITLISPDISABLE"
echo "PROVEITLISPENABLE: $PROVEITLISPENABLE"
echo "PROVEITLISPTHFS: $PROVEITLISPTHFS"
echo "PROVEITLISPTHEORIES: $PROVEITLISPTHEORIES"
fi
$PVSPATH/pvs -raw $PVSLISP -E "(proveit)" > $OUTFILE
if [ $? = 0 ]; then
error_output
exit 1
fi
pvs_output
fi
reset_vars
}
# ... and go!
#
reset_vars
while [ $# -gt 0 ]
do
case $1 in
--debug)
DEBUG=yes;;
-h|-help|--help)
usage
exit 0;;
-version|--version)
echo $PROVEITVERSION
exit 0;;
.*)
EXT=$1;;
-lisp|--lisp)
case $2 in
allegro)
LISP='allegro';;
cmulisp)
LISP='cmulisp'
PVSBIN='PVSBIN';;
sbclisp)
LISP='sbclisp'
PVSBIN='PVSBIN';;
*)
echo "Error: Only allegro, cmulisp, and sbcl are currently available"
exit 1;;
esac
if [ "$LISP" ]; then
PVSLISP="-lisp $LISP"
fi
shift;;
-d|-dir|--dir)
if [ -d "$2" ]; then
OUTDIR=$2
else
echo "Error: $2 is not a directory"
exit 1
fi
shift;;
-t|-top|--top)
TOP=$2
shift;;
-C|-Clean|--Clean|-clean-only|--clean-only)
QUIET=
CLEAN=only;;
-o|-out|--out)
if [ -d "$2" ]; then
echo "Error: $2 is a directory"
exit 1
else
OUTFILE=$2
fi
shift;;
-p|-prelude-ext|--prelude-ext)
PRELUDEXT=`append $2 $PRELUDEXT`
shift;;
-disable|--disable)
DISABLE=`append $2 $DISABLE`
shift;;
-disable-oracles|--disable-oracles)
DISABLE="_";;
-enable|--enable)
ENABLE=`append $2 $ENABLE`
shift;;
-*|~*) OPTS="$OPTS $1";;
*) ARG=$1
NOFILE=
proveit
esac
shift
done
if [ "$NOFILE" ]; then
ARG=$TOP.pvs
if [ -f $ARG -o "$CLEAN" = "only" ]; then
proveit
else
echo "Usage: proveit [--help | <option> ...] <file>.pvs"
fi
fi
exit 0
