Revision 4aa2697e433307fe5c25493c16d93f35ce9ca4d7 authored by Son HO on 01 September 2020, 11:59:04 UTC, committed by GitHub on 01 September 2020, 11:59:04 UTC
valedepend.py
# This file requires Python version >= 3.3
import re
import sys
import argparse
import os, os.path
import traceback
if sys.version_info < (3, 3):
print('Requires Python version >= 3.3, found version ' + sys.version_info)
exit(1)
##################################################################################################
#
# Command-line options
#
##################################################################################################
arg_parser = argparse.ArgumentParser()
arg_parser.add_argument('-in', action = 'append', dest = 'vaf_file', required = True)
arg_parser.add_argument('-include', action = 'append', dest = 'include_dir', required = False)
arg_parser.add_argument('-deps', action = 'store', dest = 'deps_file', required = False)
args = arg_parser.parse_args()
vaf_files = args.vaf_file
inc_dirs = [] if args.include_dir == None else args.include_dir
deps_file = args.deps_file
##################################################################################################
#
# Dependency analysis
#
##################################################################################################
deps = {} # map target names to source names
#commands = {} # map target names to commands (recipes)
dump_deps = {} # map F* type .dump file names x.dump to sets of .dump file names that x.dump depends on
vaf_dump_deps = {} # map .vaf file names x.vaf to sets of .dump file names that x.vaf depends on
vaf_vaf_deps = {} # map .vaf file names x.vaf to sets of y.vaf file names that x.vaf depends on
# match 'include {:attr1} ... {:attrn} "filename"'
# where attr may be 'verbatim' or 'from BASE'
vale_include_re = re.compile(r'include((?:\s*\{\:(?:\w|[ ])*\})*)\s*"(\S+)"', re.M)
vale_fstar_re = re.compile(r'\{\:\s*fstar\s*\}')
vale_from_base_re = re.compile(r'\{\:\s*from\s*BASE\s*\}')
vale_import_re = re.compile(r'module\s+[a-zA-Z0-9_]+\s*[=]\s*([a-zA-Z0-9_.]+)')
def norm(path):
p = os.path.normpath(path).replace('\\', '/')
if path.startswith('./') and not p.startswith('./'):
p = './' + p
return p
# Drop the '.vaf', '.fst', etc.
def file_drop_extension(file):
return norm(os.path.splitext(file)[0])
# Given source file name, return file name in object directory
def to_obj_dir(file):
file = norm(file)
return norm(os.path.join('obj', os.path.basename(file)))
def depends(target, source):
target = norm(target)
source = norm(source)
if not (target in deps):
deps[target] = []
if not source in deps[target]:
deps[target].append(source)
#def command(target, cmd):
# target = norm(target)
# if not (target in deps):
# deps[target] = []
# commands[target] = cmd
def find_fsti(module):
for d in inc_dirs:
for suffix in ('.fsti', '.fst', '.fsti.checked', '.fst.checked'):
if os.path.isfile(os.path.join(d, module + suffix)):
return norm(os.path.join(d, module + suffix.replace('.checked', '')))
raise Exception('Could not find fst/fsti for dependency ' + module)
def find_checked_file(fst_file):
fst_file = norm(fst_file)
checked_file = os.path.basename(fst_file) + '.checked'
for d in inc_dirs:
if os.path.isfile(os.path.join(d, checked_file)):
return norm(os.path.join(d, checked_file))
return to_obj_dir(fst_file + '.checked')
def make_dump(fst_file):
dump = to_obj_dir(fst_file + '.dump')
checked = find_checked_file(fst_file)
depends(dump, checked)
return dump
def vale_dependency_scan(vaf):
with open(vaf) as f:
contents = f.read()
dirname = norm(os.path.dirname(vaf))
vaf_includes = vale_include_re.findall(contents)
fst_includes = vale_import_re.findall(contents)
obj_file_base = file_drop_extension(to_obj_dir(vaf))
fst = obj_file_base + '.fst'
fsti = obj_file_base + '.fsti'
types_vaf = obj_file_base + '.types.vaf'
vaf_dump_deps[vaf] = set()
vaf_vaf_deps[vaf] = set()
depends(fst, vaf)
depends(fst, types_vaf)
depends(fsti, fst)
for (attrs, inc) in vaf_includes:
if vale_fstar_re.search(attrs):
vaf_dump_deps[vaf].add(make_dump(find_fsti(inc)))
else:
f = norm(os.path.join('code' if vale_from_base_re.search(attrs) else dirname, inc))
ffsti = to_obj_dir(file_drop_extension(f) + '.fsti')
depends(fst, ffsti)
vaf_vaf_deps[vaf].add(f)
def vale_types_command(source_vaf):
source_base = file_drop_extension(to_obj_dir(source_vaf))
types_vaf = source_base + '.types.vaf'
done = set()
def collect_dumps_in_order(x):
if not (x in done):
done.add(x)
for y in sorted(dump_deps[x]):
# if x depends on y, y must appear first
collect_dumps_in_order(y)
x_vaf = re.sub('\.dump$', '.types.vaf', x)
depends(types_vaf, x)
for vaf in sorted(vaf_vaf_deps[source_vaf] | {source_vaf}):
for x in sorted(vaf_dump_deps[vaf]):
collect_dumps_in_order(x)
def compute_fstar_deps():
with open(deps_file, "r") as lines:
for line in lines:
line = line.strip()
if 'Warning:' in line:
print(line)
continue
if len(line) == 0:
continue
if '(Warning ' in line:
# example: "(Warning 307) logic qualifier is deprecated"
continue
if line.endswith(':'):
line = line + ' '
# lines are of the form:
# a1.fst a2.fst ... : b1.fst b2.fst ...
targets, sources = line.split(': ', 1) # ': ', not ':', because of Windows drive letters
sources = sources.split()
targets = targets.split()
# Computing types from F* files
# Dump F* types for for each of a1.fst a2.fst ... into a1.fst.dump, a2.fst.dump, ...
for t in targets:
dumptargetfile = make_dump(t)
if not (dumptargetfile in dump_deps):
dump_deps[dumptargetfile] = set()
for s in sources:
dump_deps[dumptargetfile].add(make_dump(s))
for vaf in vaf_files:
try:
vale_dependency_scan(norm(vaf))
except Exception as e:
print('Error in file ' + vaf)
print(e)
print(traceback.format_exc())
exit(1)
if deps_file != None:
compute_fstar_deps()
for vaf in vaf_files:
try:
vale_types_command(norm(vaf))
except Exception as e:
print('Error in file ' + vaf)
print(e)
print(traceback.format_exc())
exit(1)
for target in sorted(deps.keys()):
print(target + " : " + " ".join(list(deps[target])))
# if (target in commands):
# print('\t' + commands[target])
print()
Computing file changes ...