revised perf diff (raw v.s. F* extracted)

port_fstar_tdiff.py

import re

class PerfData:
	def __init__(self):
		self.data = {}
		self.duration = None
	
	def time(self,fn):
		return self.data[fn] * self.duration
	
	def per(self,fn):
		return self.data[fn]

def normalize_name(fn):
	fn = re.sub(r'_\d+$','',fn)
	fn = re.sub(r'\$\d+$','',fn)
	fn = re.sub(r'Node_storage_store_fstar','Node_storage',fn)
	fn = re.sub(r'Node_storage_load_fstar','Node_storage',fn)
	fn = re.sub(r'_fstar','',fn)
	return fn

def parse_perf_output(fn):
	data = open(fn,'r').read().split('\n')
	
	res = PerfData()
	for d in data:
		ma = re.match((
			r'^\s+((\d|\.)+)%' + 
			r'\s+((\d|\.)+)%' + 
			r'\s+([^\s]+)\s+' + 
			r'([^\s]+)\s+' + 
			r'\[\.\]\s([^\s]+)((\s*\(inlined\))?)$'
		),d)
		if ma is not None:
			command = ma.group(5)
			if command != 'benchmark.exe':
				continue
			per = float(ma.group(1)) / 100
			func = ma.group(7)
			func = normalize_name(func)
			if func in res.data.keys():
				cp = res.data[func]
				if cp >= per:
					continue
			res.data[func] = per
			continue
		
		ma = re.match(r'^# sample duration : ((\d|\.)+) ms$',d)
		if ma is not None:
			dur = float(ma.group(1))
			res.duration = dur / 1000
			continue
	
	return res

def diff_output_data(d1,d2):
	ks = set(d1.data.keys()) & set(d2.data.keys())

	diff = []
	for k in ks:
		d = d2.time(k) - d1.time(k)
		diff.append((d,k))
	
	diff = sorted(diff,key=lambda d: d[0])
	return diff
	
# perf record --call-graph=dwarf -- dune exec ./benchmark.exe million
# perf report --hide-unresolved --header --call-graph=no > o2
# Usage: python3 port_fstar_tdiff.py ~/plebeia-raw/plebeia/tests/benchmark/o ~/plebeia/tests/benchmark/o | less

import sys
print('basefile: %s, diff: %s' % (sys.argv[1],sys.argv[2]))
d1 = parse_perf_output(sys.argv[1])
d2 = parse_perf_output(sys.argv[2])

print('duration: %f' % d1.duration)
print('duration: %f' % d2.duration)
                        
diff = diff_output_data(d1,d2)
for d,name in diff:
	print("%3f [s]\t%3f [s]\t%3f [s]\t%s" % (d1.time(name),d2.time(name),d,name))