#!/usr/bin/python
from collections import defaultdict
from datetime import datetime
import os
import re
import string
import subprocess
import sys
benchmarks = {
'benchmarks/text-0.11.2.3': [ 'Data/Text.hs'
, 'Data/Text/Array.hs'
, 'Data/Text/Encoding.hs'
, 'Data/Text/Foreign.hs'
, 'Data/Text/Fusion.hs'
, 'Data/Text/Fusion/Size.hs'
, 'Data/Text/Internal.hs'
, 'Data/Text/Lazy.hs'
, 'Data/Text/Lazy/Builder.hs'
, 'Data/Text/Lazy/Encoding.hs'
, 'Data/Text/Lazy/Fusion.hs'
, 'Data/Text/Lazy/Internal.hs'
, 'Data/Text/Lazy/Search.hs'
, 'Data/Text/Private.hs'
, 'Data/Text/Search.hs'
, 'Data/Text/Unsafe.hs'
, 'Data/Text/UnsafeChar.hs' ],
'benchmarks/bytestring-0.9.2.1': [ 'Data/ByteString.T.hs'
, 'Data/ByteString/Char8.hs'
, 'Data/ByteString/Fusion.T.hs'
, 'Data/ByteString/Internal.hs'
, 'Data/ByteString/Lazy.hs'
# , 'Data/ByteString/LazyZip.hs'
, 'Data/ByteString/Lazy/Char8.hs'
, 'Data/ByteString/Lazy/Internal.hs'
, 'Data/ByteString/Unsafe.hs' ],
'benchmarks/vector-algorithms-0.5.4.2': [ 'Data/Vector/Algorithms/AmericanFlag.hs'
, 'Data/Vector/Algorithms/Combinators.hs'
, 'Data/Vector/Algorithms/Common.hs'
, 'Data/Vector/Algorithms/Heap.hs'
, 'Data/Vector/Algorithms/Insertion.hs'
, 'Data/Vector/Algorithms/Intro.hs'
, 'Data/Vector/Algorithms/Merge.hs'
, 'Data/Vector/Algorithms/Optimal.hs'
, 'Data/Vector/Algorithms/Radix.hs'
, 'Data/Vector/Algorithms/Search.hs' ],
'benchmarks/esop2013-submission': [ 'Base.hs', 'Splay.hs' ],
'benchmarks/hscolour-1.20.0.0': [ 'Language/Haskell/HsColour.hs'
, 'Language/Haskell/HsColour/ACSS.hs'
, 'Language/Haskell/HsColour/Anchors.hs'
, 'Language/Haskell/HsColour/ANSI.hs'
, 'Language/Haskell/HsColour/Classify.hs'
, 'Language/Haskell/HsColour/ColourHighlight.hs'
, 'Language/Haskell/HsColour/Colourise.hs'
, 'Language/Haskell/HsColour/CSS.hs'
, 'Language/Haskell/HsColour/General.hs'
, 'Language/Haskell/HsColour/HTML.hs'
, 'Language/Haskell/HsColour/InlineCSS.hs'
, 'Language/Haskell/HsColour/LaTeX.hs'
, 'Language/Haskell/HsColour/MIRC.hs'
, 'Language/Haskell/HsColour/Options.hs'
, 'Language/Haskell/HsColour/Output.hs'
, 'Language/Haskell/HsColour/TTY.hs' ],
'benchmarks/xmonad': [ 'XMonad/StackSet.hs' ],
'include': [ 'GHC/List.lhs' ],
'.': [ 'benchmarks/base-4.5.1.0/Data/List.hs' ]
}
def time(fn):
start = datetime.now()
with open(fn+'.log', 'w') as out:
subprocess.call(['liquid', '--smtsolver', 'z3mem', fn], stdout=out, stderr=out)
return (datetime.now() - start).total_seconds()
def errors(fn):
with open(fn+'.log') as fd:
log = fd.readlines()
unsafes = [l for l in log if l.startswith('**** UNSAFE:')]
return unsafes
def sloc(scripts,fn):
return int(subprocess.check_output(
'%s/haskell_count %s | tail -n1' % (scripts, fn), shell=True))
def lines(anns):
return sum(map(lambda x:(1+x.count('\n')), anns))
def recs(fn):
out = subprocess.check_output('liquid-count-binders %s 2>/dev/null' % fn, shell=True)
return [int(n) for n in re.findall('(\d+)', out)]
def find(rx, str):
return [(str[a.start():(3+string.find(str,"@-}", a.start()))])
for a in list(re.finditer(rx, str))]
qualif_re = '{-@ qualif'
other = 'import|include|invariant|embed|Decrease|LAZYVAR|Strict|Lazy'
other_re = '{-@ (%s)' % other
spec_re = '{-@ (?!(%s|qualif|LIQUID))' % other
dec_re = '{-@ Decrease'
div_re = '{-@ (Strict|Lazy)'
wit_re = '{- LIQUID WITNESS'
mod_re = '^module ([\w\.]+)'
def combine(x, y):
return {k:x[k] + y[k] for k in y.keys()}
def texify(fn, metrics):
return '\\texttt{%s} & %d & %d / %d & %d / %d & %d / %d & %d & %d & %d & %d & %d \\\\\n' % (
fn, metrics['sloc'], metrics['specs'], metrics['specs_lines'],
metrics['others'], metrics['others_lines'],
metrics['qualifs'], metrics['qualifs_lines'],
metrics['funs'], metrics['recfuns'], metrics['divs'],
metrics['hints'], metrics['time'])
def texify_term(fn, metrics):
return '\\texttt{%s} & %d & %d & %d & %d & %d & %d & %d \\\\\n' % (
fn, metrics['sloc'], metrics['errs'],
metrics['funs'], metrics['recfuns'], metrics['divs'],
metrics['hints'], metrics['time'])
def main():
if len(sys.argv) >= 2 and sys.argv[1] == '--only-term':
print 'ONLY COLLECTING TERMINATION DATA!'
colformat = '|l|rr|rrrr|r|'
headers = ['Module', 'LOC', 'Err', 'Fun', 'Rec', 'Div', 'Hint', 'Time']
pptex = texify_term
else:
colformat = '|l|rrrr|rrrr|r|'
headers = ['Module', 'LOC', 'Specs', 'Annot', 'Qualif',
'Fun', 'Rec', 'Div', 'Hint', 'Time']
pptex = texify
results = {}
pwd = os.getcwd()
for d, fs in benchmarks.iteritems():
os.chdir(d)
results[d] = {}
for fn in fs:
print fn
f_res = {}
f_res['time'] = time(fn)
f_res['sloc'] = sloc(os.path.join(pwd,'scripts'),fn)
[fs,rs,rfs] = recs(fn)
f_res['funs'] = fs
f_res['recs'] = rs
f_res['recfuns'] = rfs
errs = set(errors(fn))
import pprint
pprint.pprint(errs)
f_res['errs'] = len(errs)
str = (open(fn, 'r')).read()
mod = re.search(mod_re, str, re.M).group(1)
specs = find(spec_re, str)
f_res['specs'] = len(specs)
f_res['specs_lines'] = lines(specs)
qualifs = find(qualif_re, str)
f_res['qualifs'] = len(qualifs)
f_res['qualifs_lines'] = lines(qualifs)
others = find(other_re, str)
f_res['others'] = len(others)
f_res['others_lines'] = lines(others)
f_res['divs'] = len(re.findall(div_re, str))
f_res['hints'] = len(re.findall(wit_re, str)) + len(re.findall(dec_re, str))
results[d][mod] = f_res
os.chdir(pwd)
with open('metrics.tex', 'w') as out:
out.write('\\begin{tabular}{%s}\n' % colformat)
out.write('\\hline\n')
out.write(' & '.join('\\textbf{%s}' % h for h in headers) + '\\\\\n')
out.write('\\hline\\hline\n')
totals = defaultdict(int)
for d, fs in results.iteritems():
dirtotals = defaultdict(int)
for fn, metrics in sorted(fs.iteritems()):
out.write(pptex(fn, metrics))
dirtotals = combine(dirtotals, metrics)
out.write(pptex(d, dirtotals))
out.write('\\hline\n\n')
totals = combine(totals, dirtotals)
out.write(pptex('Total', totals))
out.write('\\hline\n\\end{tabular}\n')
if __name__ == '__main__':
main()