Commit d51b790b authored by Simon Cruanes's avatar Simon Cruanes

outils de statistiques sur les résultats des prouveurs utilisés avec whyml3, en python+sqlite3

parent e82f52e2
#!/usr/bin/env python
#-*- coding: UTF-8 -*-
# ce script affiche le contenu de la base de données
import sys
import sqlite3
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)
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 -*-
# ce script affiche le contenu de la base de données
import sys
import sqlite3
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()
try:
dump = cursor.execute("select * from runs")
except:
print >> sys.stderr, "database %s non valide !" % db_file
sys.exit(1)
dump = dump.fetchall()
import lib
lib.print_columns(dump)
#!/usr/bin/env python
#-*- coding: UTF-8 -*-
# ce script cherche un but qui corresponde aux critères demandés
import sys
# connexion DB
import sqlite3
conn = sqlite3.connect("output.db")
cursor = conn.cursor()
# utilitaires
import lib
# les prouveurs
provers = cursor.execute("select distinct prover from runs").fetchall()
provers = [p[0] for p in provers]
# les 2 uplets de prouveurs
provers_combinaisons = [(p1,p2) for p1 in provers for p2 in provers if p1 < p2]
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 = "Timeout"
ORDER BY r1.file ASC""").fetchall()
tptp = ["spass", "eprover"]
# garder les lignes représentant une différence entre un tptp et un smt
diffs = [line for line in diffs if (line[2] in tptp) ^ (line[4] in tptp)]
# afficher
lib.print_columns(diffs)
#!/usr/bin/env python
#-*- coding: UTF-8 -*-
# utilitaires pour manipuler la BDD
import sys
def diff(cursor, prover1, prover2):
"trouve les (file,goal) dont le résultat est différent\
pour prover1 et prover2"
query = """SELECT distinct r1.file, r1.goal, r1.prover, r1.result, r2.prover, r2.result
FROM runs r1 JOIN runs r2
WHERE r1.prover = "%s" and r2.prover = "%s" 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 []
def print_columns(lines):
"affiche les colonnes bien alignées"
if len(lines) == 0:
return
column_width = len(lines[0])
widths = [0 for x in xrange(column_width)]
for line in lines:
for i in xrange(column_width-1):
widths[i] = max(widths[i], len(line[i]))
for line in lines:
for i in xrange(column_width-1):
assert(len(line[i]) <= widths[i])
print line[i].ljust(widths[i]+2, "."),
print line[-1]
#!/usr/bin/env python
#-*- coding: UTF-8 -*-
# ce script lance un prouveur sur un fichier .mlw (grâce à why3)
# et stocke la sortie dans la base output.db
import sys
from os import path
from subprocess import Popen, PIPE
import getopt
#------------------------------------------------
# parse les arguments
db_file = "output.db"
try:
opt, args = getopt.getopt(sys.argv[1:], "df:C:", [])
target_file = args[0]
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']
if '-C' in opt:
config_file = opt['-C']
else:
config_file = None
except:
print """usage:
process_file [-d] [-f file] [-C config_file] 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>"""
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()
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 whyml3 sur le fichier
def launch_whyml(target_file, prover):
target_file = path.abspath(target_file)
command_list = ["whyml3", "-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(".mlw")[0] + ".mlw")
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_whyml(target_file, prover)
lines = process_results(results)
process_lines(lines)
print_lines(lines)
# on y est !
for prover in provers:
process(prover)
#------------------------------------------------
# fermeture
cursor.close()
conn.commit()
conn.close()
print "sauvegarde effectuée"
#!/bin/sh
PROVERS="spass,eprover,z3,cvc3,simplify,alt-ergo,z3_simple,cvc3_simple,eprover_simple,spass_simple"
#TARGET_DIR="../bench/programs/good/"
TARGET_DIRS="../examples/programs/ ../bench/programs/good/"
for TARGET_DIR in $TARGET_DIRS; do
for target_file in $TARGET_DIR/*.mlw; do
echo ./process_file.py $@ "$target_file" "$PROVERS"
./process_file.py -C ../why.conf $@ "$target_file" "$PROVERS"
done
done
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment