Commit 4d584469 authored by Andrei Paskevich's avatar Andrei Paskevich

remove why3bench and comparison, subsumed by why3session bench

parent 6b4d42fe
......@@ -843,62 +843,6 @@ install_no_local::
install_local:: bin/why3session
###############
# Bench
###############
ifeq (@enable_bench@,yes)
BENCH_FILES = worker db bench benchrc benchdb why3bench
BENCHMODULES := $(addprefix src/why3bench/, $(BENCH_FILES))
BENCHDEP = $(addsuffix .dep, $(BENCHMODULES))
BENCHCMO = $(addsuffix .cmo, $(BENCHMODULES))
BENCHCMX = $(addsuffix .cmx, $(BENCHMODULES))
$(BENCHDEP): DEPFLAGS += -I src/why3bench
$(BENCHCMO) $(BENCHCMX): INCLUDES += -I src/why3bench -I @SQLITE3LIB@
# build targets
byte: bin/why3bench.byte
opt: bin/why3bench.opt
bin/why3bench.opt bin/why3bench.byte: INCLUDES += -thread -I +threads -I @SQLITE3LIB@
bin/why3bench.opt bin/why3bench.byte: EXTLIBS += threads sqlite3
bin/why3bench.opt: lib/why3/why3.cmxa $(BENCHCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(OLINKFLAGS) $^
bin/why3bench.byte: lib/why3/why3.cma $(BENCHCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(BLINKFLAGS) $^
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
include $(BENCHDEP)
endif
depend: $(BENCHDEP)
clean::
rm -f src/why3bench/*.cm[iox] src/why3bench/*.o
rm -f src/why3bench/*.annot src/why3bench/*.dep src/why3bench/*~
rm -f bin/why3bench.byte bin/why3bench.opt bin/why3bench
clean_old_install::
rm -f $(BINDIR)/why3bench$(EXE)
install_no_local::
cp -f bin/why3bench.@OCAMLBEST@ $(TOOLDIR)/why3bench$(EXE)
install_local:: bin/why3bench
endif
##############
# Coq plugin
##############
......
==== Descriptif général : ====
Ensemble de scripts destinés à recueillir et analyser les résultats obtenus par whyml3 en fonction du fichier, du but et du prouveur utilisé. Les données peuvent être utilisées pour comparer les prouveurs entre eux, pour trouver les fichiers et buts sur lesquels les prouveurs ont des difficultés, etc.
==== Usage des scripts : ====
* run_all.sh : lance process_file.py avec tous les prouveurs sur tous les fichiers de ../examples/programs/ et ../bench/programs/good/.
* process_file.py : étant donné un fichier et une liste de prouveurs (séparés par des virgules), lance chaque prouveur sur le fichier par le biais de whyml3.
Les résultats sont stockés dans output.db (par défaut).
Un seul résultat est stocké pour un triplet (fichier, but, prouveur) donné.
* clear.py : vide la base dans output.db (avec confirmation).
* dump.py : affiche le contenu de la base, aligné par colonnes. Utile en combinaison avec grep.
* find.py : trouve les (fichier,but,prover1,result1,prover2,result2) tels que, sur le (fichier,but) concerné, les prouveurs prover1 et prover2 se comportent différemment.
Les résultats sont donnés pour pouvoir comparer les performances comparées des prouveurs sur des buts donnés.
* diff.py : prend une liste d'au moins 2 prouveurs (séparés par des virgules), et donne la liste des (fichier,but) sur lesquels ces prouveurs se comportent différemment.
* stats.py : recueille des statistiques variées sur tous les prouveurs de la base de données.
note : lib.py contient des fonctions utilitaires destinées aux scripts, mais aussi utilisables directement dans (i)python.
==== Exemple typique d'utilisation ====
En partant d'une base vide (fichier vide ou inexistant) :
$ ./run_all.sh
<logs divers, prend un certain temps>
$ ./dump.py
<contenu de la base>
$ ./stats.py
<ratio échecs/succès par prouveur>
<pour chaque couple de prouveur, nombre de buts sur lequel le premier a été meilleur que le second>
$ ./diff.py z3,cvc3
<buts sur lesquels z3 et cvc3 se comportent différemment>
$ ./diff.py z3,cvc3,z3_simple
<buts sur lesquels 2 de ces prouveurs ont des résultats différents>
$ ./clear.py # données trop confidentielles pour qu'on les laisse à disposition des concurrents !
[y/n] y
#!/usr/bin/env python
#-*- coding: UTF-8 -*-
# ce script affiche le contenu de la base de données
import sys
import sqlite3
# demander confirmation pour effacer la base
print "ceci va effacer la base de tests. Continuer ?"
while True:
confirm = raw_input("[y/n] ")
if confirm in ["y","yes","Y","Yes"]:
break
elif confirm in ["n","No","N","no"]:
sys.exit(0)
# on veut effacer la base. Pour cela, il faut d'abord s'y connecter.
conn = sqlite3.connect("output.db")
cursor = conn.cursor()
try:
cursor.execute("delete from runs")
cursor.close()
conn.commit()
conn.close()
except:
print >> sys.stderr, "database non valide !"
sys.exit(1)
print >> sys.stderr, "cleanup terminé !"
#!/usr/bin/env python
#-*- coding: UTF-8 -*-
import sys
# ce script donne la différence entre les résultats des prouveurs donnés
# en argument
if len(sys.argv) <= 1:
print """usage: ./diff prover1,prover2[,prover3,[...]]"""
sys.exit(0)
# parser les prouveurs
provers = sys.argv[1]
provers = [p.strip() for p in provers.split(",")]
if len(provers) <= 1:
print "erreur, il faut au moins 2 prouveurs !"
sys.exit(1)
print "compare les prouveurs", ", ".join(provers)
# se connecte à la DB
import sqlite3
db_file = "output.db"
conn = sqlite3.connect(db_file)
cursor = conn.cursor()
# utilise la lib pour calculer les différences
import lib
table = []
# comparer les couples de prouveurs. On évite les redondances en ne comparant
# un couple (p1,p2) que dans le sens p1<p2 (ordre lexicographique)
for p1, p2 in [(p1, p2) for p1 in provers for p2 in provers if p1 < p2]:
diffs = lib.diff(cursor, p1, p2)
table += diffs
# afficher les différences
lib.print_columns(table)
#!/usr/bin/env python
#-*- coding: UTF-8 -*-
# ce script affiche le contenu de la base de données
import sys
import sqlite3
# ouvrir la DB
db_file = "output.db"
if len(sys.argv) > 1:
db_file = sys.argv[1]
print >> sys.stderr, "utile la database", db_file
conn = sqlite3.connect(db_file)
cursor = conn.cursor()
# essayer de dumper la table runs (échoue si elle n'existe pas)
try:
dump = cursor.execute("select * from runs")
dump = dump.fetchall()
except:
print >> sys.stderr, "database %s non valide !" % db_file
sys.exit(1)
# afficher le dump
import lib
lib.print_columns(dump)
#!/usr/bin/env python
#-*- coding: UTF-8 -*-
# ce script cherche les (file,goal) pour lesquels un prouveur SMT et
# un prouveur TPTP ont des résultats différents.
import sys
# connexion DB
import sqlite3
conn = sqlite3.connect("output.db")
cursor = conn.cursor()
# utilitaires
import lib
# les prouveurs (demander à la DB)
provers = cursor.execute("select distinct prover from runs").fetchall()
provers = [p[0] for p in provers]
# les 2 uplets de prouveurs, sans redondances
provers_combinaisons = [(p1,p2) for p1 in provers for p2 in provers if p1 < p2]
# trouver les couples de prouveurs dont l'un échoue et l'autre réussit,
# pour chaque (fichier,but)
diffs = []
diffs = cursor.execute("""SELECT r1.file,r1.goal, r1.prover, r1.result, r2.prover, r2.result
FROM runs r1
INNER JOIN runs r2
WHERE r1.file = r2.file
AND r1.goal = r2.goal
AND r1.result = "Valid"
AND r2.result <> "Valid"
ORDER BY r1.file ASC""").fetchall()
# comment différencier un prouveur TPTP d'un prouveur SMT ?
tptp = ["spass", "eprover"]
def isTptp(x):
"x est-il le nom d'un prouveur tptp ?"
for t in tptp:
if x.find(t) >= 0:
return True
return False
# garder les lignes représentant une différence entre un tptp et un smt
diffs = [line for line in diffs if (isTptp(line[2]) ^ isTptp(line[4]))]
# afficher
lib.print_columns(diffs)
#!/usr/bin/env python
#-*- coding: UTF-8 -*-
# utilitaires pour manipuler la BDD
import sys
# différences de résultats entre les 2 prouveurs
def diff(cursor, prover1, prover2):
"trouve les (file,goal) dont le résultat est différent\
pour prover1 et prover2"
query = """SELECT r1.file, r1.goal, r1.prover, r1.result, r2.prover, r2.result
FROM runs r1
INNER JOIN runs r2
WHERE r1.prover = "%s" AND r2.prover = "%s"
AND r1.file = r2.file AND r1.goal = r2.goal
AND r1.result <> r2.result""" % \
(prover1, prover2)
try:
result = cursor.execute(query)
return result.fetchall()
except Exception, e:
print >> sys.stderr, "exception :", repr(e)
return []
# (file,goal) sur lesquels le premier prouveur est meilleur que le second
def superior(cursor, prover1, prover2):
"trouve les (file,goal) pour lesquels prover1 > prover2"
query = """SELECT distinct r1.file, r1.goal
FROM runs r1
INNER JOIN runs r2
WHERE r1.prover = "%s" AND r2.prover = "%s"
AND r1.file = r2.file AND r1.goal = r2.goal
AND r1.result = "Valid"
AND r2.result <> "Valid"
""" % (prover1, prover2)
try:
result = cursor.execute(query)
return result.fetchall()
except Exception, e:
print >> sys.stderr, "exception :", repr(e)
return None
# affichage aligné en colonnes
def print_columns(lines, sep = u"."):
"affiche les colonnes bien alignées"
sep = unicode(sep)
if len(lines) == 0:
return
column_width = len(lines[0])
widths = [0 for x in xrange(column_width)]
# calculer la largeur de chaque colonne (max des largeurs de ses éléments)
for line in lines:
for i in xrange(column_width-1):
widths[i] = max(widths[i], len(unicode(line[i])))
for line in lines:
for i in xrange(column_width-1):
assert(len(unicode(line[i])) <= widths[i])
item = unicode(line[i])
item = item.ljust(widths[i]+2, sep)
print item,
print line[-1]
# petite facilité
def print_sep():
"affiche une ligne de '-' pour séparer clairement des\
sections de l'affichage"
print "---------------------------------------------------------------"
# effacer la ligne courante du terminal
def erase_line(stream = sys.stdout):
"efface la ligne et revient au début"
stream.write("\033[2K\r")
stream.flush()
# récupéré sur le net, pour obtenir largeur et hauteur du terminal
def getTerminalSize():
"récupère la largeur et la hauteur du terminal"
# {{{
def ioctl_GWINSZ(fd):
try:
import fcntl, termios, struct, os
cr = struct.unpack('hh', fcntl.ioctl(fd, termios.TIOCGWINSZ, '1234'))
except:
return None
return cr
cr = ioctl_GWINSZ(0) or ioctl_GWINSZ(1) or ioctl_GWINSZ(2)
if not cr:
try:
fd = os.open(os.ctermid(), os.O_RDONLY)
cr = ioctl_GWINSZ(fd)
os.close(fd)
except:
pass
if not cr:
try:
cr = (env['LINES'], env['COLUMNS'])
except:
cr = (25, 80)
return int(cr[1]), int(cr[0])
# }}}
# tente d'affichier un tableau donné en entrée. Ce tableau
# est un dictionnaire (colonne,ligne) -> item qui doit vérifier
# la propriété suivante :
# pour tout (i,j) dans tab, (j,i) est aussi dans tab
def printTab(tab):
"affiche le tableau carré donné en entrée"
items = list(set( [unicode(x) for (x,y) in tab.keys()] )) # enlever doublons
for i in items:
tab[ (None,i) ] = i # pour la première ligne
max_width = 0
normal_sum = 0
for i in items:
max_width = max(max_width, len(i)+1)
normal_sum += len(i) + 1
width,height = getTerminalSize()
if max_width * (len(items)+1) >= width: # ça ne rentre pas
print >> sys.stderr, "terminal trop étroit"
max_width = width / (len(items) + 1)
def print_line(item):
if item != None:
sys.stdout.write(item[:max_width-1].ljust(max_width-1, " ")+"|")
else:
sys.stdout.write("x\y : x>y".ljust(max_width-1, " ")+"|")
for i in xrange(len(items)):
i = items[i]
if i == item:
sys.stdout.write("x".ljust(max_width, " "))
else:
num = unicode(tab[ (item,i) ])
sys.stdout.write(num[:max_width-1].ljust(max_width, " "))
sys.stdout.write("\n")
print "légende : [colonne] est meilleur que [ligne] sur [case] buts\n"
print_line(None)
for i in items:
print("-"*(len(items)+1)*max_width)
print_line(i)
for i in items:
try:
del tab[ (None,i) ]
except:
pass
#!/usr/bin/env python
#-*- coding: UTF-8 -*-
# ce script lance un prouveur sur un fichier .mlw (grâce à whyml3)
# et stocke la sortie dans la base output.db
# il peut aussi être utilisé avec why3 grâce à l'option -t
import sys
from os import path
from subprocess import Popen, PIPE
import getopt
#------------------------------------------------
# parse les arguments
try:
opt, args = getopt.getopt(sys.argv[1:], "df:C:t:", [])
target_file = args[0]
_,extension = path.splitext(target_file)
provers = args[1]
provers = provers.split(",")
opt = dict(opt)
if '-d' in opt:
debug = True
print >> sys.stderr, u"debug activé !"
else:
debug = False
if '-f' in opt:
db_file = opt['-f']
else:
db_file = "output.db"
if '-C' in opt:
config_file = opt['-C']
else:
config_file = None
if '-t' in opt:
tool = opt['-t']
else:
tool = "whyml3"
except:
print """usage:
process_file.py [-d] [-f file] [-C config_file] [-t tool] file prover[,prover[,prover...]]
-d : active le mode debug
-f <file> : stocke les résultats dans <file>
-C <file> : utilise le fichier de configuration <file>
-t <tool> : utilise <tool> pour les preuves (why, whyml...)"""
sys.exit(1)
print >> sys.stderr, "utilise le(s) prouveur(s) %s sur %s (db : %s)" % \
(provers, target_file, db_file)
#------------------------------------------------
# ouvre la DB
import sqlite3
conn = sqlite3.connect(db_file)
cursor = conn.cursor()
# si la table runs n'existe pas, la créer. Sinon, signaler qu'on a trouvé une base.
# le cas où la table existe mais n'est pas au bon format n'est pas traité.
try:
cursor.execute("""create table runs
(file string, goal string, prover string, result string, time float)""")
except sqlite3.OperationalError:
print >> sys.stderr, "base trouvée dans %s" % db_file
#------------------------------------------------
# lance [tool] sur le fichier pour récupérer les résultats
def launch_tool(target_file, prover):
target_file = path.abspath(target_file)
command_list = [tool, "-P", prover, "-a", "split_goal"]
if config_file:
command_list += ["-C", config_file]
command_list.append(target_file)
command = " ".join(command_list)
print >> sys.stderr, command
why_instance = Popen(command, shell=True, stdout=PIPE)
results = why_instance.communicate()[0]
return results
#------------------------------------------------
# parser la sortie
def getFile(x):
"récupère le nom de fichier"
return path.basename(x.partition(extension)[0] + extension)
def getGoal(x):
"récupère le nom du but"
return x.strip().split(" ")[-1]
def getResult(x):
"récupère le résultat"
return x.strip().partition(" ")[0]
def getTime(x):
"récupère le temps de calcul"
time = x.strip().partition(" ")[2]
try:
time = time[1:-2] # (0.02s) --> 0.02
time = float(time)
return time
except:
return 0
def process_results(results):
"traite les résultats bruts"
# découper en lignes
lines = results.splitlines()
# découper les lignes à ':'
lines = [line.partition(":") for line in lines]
# parser la partie gauche et la partie droite
lines = [(getFile(x), getGoal(x), getResult(y), getTime(y)) for (x,_,y) in lines]
return lines
#------------------------------------------------
# enregistrer dans la DB
def protect(x):
'ajoute des " autour de x'
return '"' + x + '"'
# pour se rappeler des buts précédents
cache = {}
def process_lines(lines):
"lit les lignes, et stocke le résultat dans la BDD"
for line in lines:
filename = line[0]
goal = line[1]
result = line[2]
time = line[3]
cur_index = cache.get((filename, goal, prover), None)
if cur_index == None:
cache[(filename, goal, prover)] = 0
else:
cache[(filename, goal, prover)] = cur_index+1
goal += str(cur_index)
filename = protect(filename)
goal = protect(goal)
cur_prover = protect(prover)
result = protect(result)
time = str(time)
delete_query = "delete from runs where file = %s and goal = %s and prover = %s" % \
(filename, goal, cur_prover)
if debug:
print delete_query
cursor.execute(delete_query)
query = "insert into runs values "
query += "("
query += ", ".join([filename, goal, cur_prover, result, time])
query += ")"
if debug:
print query
cursor.execute(query)
#---------------------------------------------------
# afficher les résultats
import lib
def print_lines(lines):
lib.print_columns(lines)
#---------------------------------------------------
# effectuer le traitement réel
def process(prover):
"toute la chaine de traitement pour un prouveur donné"
prover = prover.strip()
results = launch_tool(target_file, prover)
lines = process_results(results)
process_lines(lines)
print_lines(lines)