genrules

#! /usr/bin/env python

# --------------------------------------------------------------------
import sys, os, re, time, json, xml.etree.ElementTree as etree

# --------------------------------------------------------------------
MSBUILD = 'http://schemas.microsoft.com/developer/msbuild/2003'

### do not remove failing entries! comment them out instead. 
FS7DEFAULT = [
  'TLSError',
  'Nonce',
  'TLSConstants',
  'RSAKey',
  'DHGroup',
  'PMS',
  'HASH',
  'HMAC',
  'Sig',
# 'UntrustedCert',
#  'Cert',
  'TLSInfo',
# 'TLSExtensions',
# 'TLSPRF',
  'Range',
  'DataStream',
  'AppFragment',
  'HSFragment',
  'TLSFragment',
  'StatefulPlain',
  'LHAEPlain',
  'MAC_SHA256',
  'MAC_SHA1',
  'MAC',
  'Encode',
# 'ENC_RC4',
  'ENC',
# 'AEAD_GCM',
  'LHAE',
  'StatefulLHAE',
  'Record',
  'Alert',
  'PRF',
  'KEF',
  'DH',
  'RSA',
  'SessionDB',
  'HandshakeMessages',
  'Handshake',
  'AppData',
  'Dispatch',
  'TLS',
  'UTLS',
]

MKHEADER = '''\
include ../../Makefile.config

ifndef F7PATH
$(error F7PATH is not set)
endif
ifeq ($(buildtype),cygwin)
F7PATH   := $(shell cygpath -u $$F7PATH)
F7PATH_W := $(shell cygpath -m $(F7PATH))
else
F7PATH_W  = $(F7PATH)
endif

lib7      = $(F7PATH)/samples/lib/fs7-interfaces/
libperv   = $(lib7)pervasives.fs7 $(lib7)tuples.fs7
libfs7    = $(lib7)pi.fs7 $(lib7)formulas.fs7
lib7_w    = $(F7PATH_W)/samples/lib/fs7-interfaces/
lperv     = -pervasives $(lib7_w)pervasives.fs7 -tuples $(lib7_w)tuples.fs7
libfs7_w    = $(lib7_w)pi.fs7 $(lib7_w)formulas.fs7
f7timeout = 20
f7defs    = avoid verify ideal

f7 = $(F7PATH)/bin/f7.exe
# removed --verbose for automated testing
override f7flags += \
  -z3exe $(F7PATH_W)/bin/$(z3exe) \
  -timeout $(f7timeout) $(patsubst %%,--define %%,$(f7defs)) \
  -nokindcheck $(lperv) $(libfs7_w)

xunit ?= xunit.xml

.PHONY: default clean check-xunit regen

-include Makefile.tc7

# default verification targets 
default: %(fs7default)s

#==Categories of .fs7 files==
#
# trusted: these files are not supposed to be verified, but we rely on
# their .fs7 files for verification:
#
#   Base: all modules in the Platform project
#
#   CoreCrypto wrappers: RSAKeys DHGroup HASH HMAC TLSPRF
#
#   Key management: Cert, SessionDB
#
#
# idealizing: these are .fs7 files for .fs files with #ideal flags
# this flag is used to define ideal variants of the modules
#
#   Sig MAC_SHA256 MAC_SHA1 ENC LHAE PRF KEF RSA DH
#
# the Makefile rules by default verify with --define ideal; additional
# typing is needed for some modules: Encode and LHAE are typechecked
# against multiple flags
#
#
# protocol: these .fs7 files verify the trunk of TLS building on
# the cryptographic guarantees provided by the interfaces of idealized
# modules:
# 
#   DataStream, AppFragment, HSFragment, TLSFragment, StatefulPlain,
#   LHAEPlain, StatefulLHAE, Record, Alert, Handshake, AppData,
#   Dispatch, TLS, UTLS

#==Useful optons for make==
help:
	@echo "make f7flags='myflags' <filename>.tc7"
	@echo "make f7flags='-checkonly <Module_name>.<function_name>' <filename>.tc7: checks one function"
	@echo "make f7flags='-help' <filename>.tc7: prints F7 flags"
	@echo "make f7timeout=<int> <filename>.tc7"

clean:
	rm -f *.smp *.tc7 *.why

regen:
	./genrules \\
	  -I ../../libs/Platform/Platform.fsproj \\
	  -I ../../libs/CoreCrypto/CoreCrypto.fsproj \\
	    tls.fsproj > Makefile.tls-lib.$$ \\
	|| { rm -f Makefile.tls-lib.$$; false; }
	mv Makefile.tls-lib.$$ Makefile
''' % dict(fs7default = ' '.join([x + '.tc7' for x in FS7DEFAULT]))

# --------------------------------------------------------------------
class Object(object):
    def __init__(self, **kw):
        self.__dict__.update(kw)

# --------------------------------------------------------------------
def _options(args):
    from optparse import OptionParser

    parser = OptionParser(usage = "%prog: [options] file.fsproj...")
    parser.add_option('-m', '--mode',
                      action  = 'store',
                      default = 'makefile',
                      metavar = 'MODE',
                      help    = 'set output mode to MODE')
    parser.add_option('-I', None,
                      dest    = 'includes',
                      action  = 'append',
                      default = [],
                      metavar = 'FSPROJ',
                      help    = 'Add project contents for FSI/FS7')

    options, args = parser.parse_args(args)

    if len(args) != 1:
        parser.error('exactly one .fsproj file must be given')

    options.fsproj = args[0]

    return options

# --------------------------------------------------------------------
class TopoSortCycleException(Exception):
    pass

def topoiter1(D, k, sk, seen = None):
    seen = dict() if seen is None else seen
    flag = seen.get(k, 0)

    if flag < 0:
        print [k] + sk
        raise TopoSortCycleException()
    if flag > 0:
        return

    seen[k] = -1
    for x in D.get(k, []):
        for y in topoiter1(D, x, [k] + sk, seen):
            yield y
    seen[k] = 1

    yield k

def topoiter(D):
    seen = dict()
    for k in D.iterkeys():
        for x in topoiter1(D, k, [], seen):
            yield x

# --------------------------------------------------------------------
class FS7Deps(object):
    @staticmethod
    def by_parsing(fsproj, included):
        srcfiles = dict()
        lowfiles = []
        infsproj = []

        for (i, fsp) in enumerate(included + [fsproj]):
            wext   = ['.fs', '.fs7', '.fsi'] if i == len(included) else ['.fs7', '.fsi']
            files  = os.listdir(fsp.srcdir)
            files  = [x for x in files if \
                         os.path.splitext(x)[1].lower() in  wext]
            files  = [(x.lower(), (x, fsp.srcdir)) for x in files]
            srcfiles.update(dict(files))
            lowfiles.extend([x.lower() for x in fsp.files])
            if i == len(included):
                infsproj.extend([x.lower() for x in fsp.files])

        alldeps  = dict()

        for (i, fsp) in enumerate(included + [fsproj]):
            wext = ['.fs', '.fs7', '.fsi'] if i == len(included) else ['.fs7', '.fsi']
            for name in fsp.files:
                modules = set()
                for ext in wext:
                    if (name.lower() + ext) not in srcfiles:
                        continue
                    contents = srcfiles[name.lower() + ext][0]
                    contents = open(os.path.join(fsp.srcdir, contents), 'r').read()
                    contents = re.sub(r'\(\*(?:.|\r|\n)*?\*\)', '', contents, 0)
                    contents = re.sub(r'".*?"', '', contents)
                    contents = contents.splitlines()
                    contents = [re.sub(r'//.*', '', x) for x in contents]
                    contents = [re.sub(r'\s+', ' ', x.strip()) for x in contents]
        
                    for line in contents:
                        m = re.search(r'^open (\w+)', line)
                        if m is not None:
                            modules.add(m.group(1).lower())
                        else:
                            for m in re.finditer(r'(\w+?)\.\w+', line):
                                modules.add(m.group(1).lower())
                if name.lower() in modules:
                    modules.remove(name.lower())

                alldeps[name.lower()] = list(modules.intersection(lowfiles))

        for name in topoiter(alldeps):
            for d in alldeps[name][:]: # copy
                for x in alldeps[d]:
                    if x not in alldeps[name]:
                        alldeps[name].insert(0, x)

        # Reorder using user ordering
        for name in alldeps.iterkeys():
            alldeps[name] = [x for x in lowfiles if x in alldeps[name]]
        alldeps = [(x, alldeps[x]) for x in infsproj \
                       if x in alldeps and (x + '.fs7') in srcfiles]

        # Go back to FS name (with correct case)
        def _norm(x, y):
            def _norm1(x):
                x = x + ('.fs7' if (x + '.fs7' in srcfiles) else '.fsi')
                x = srcfiles[x]
                if x[1] != os.path.curdir:
                    x = os.path.join(x[1], x[0])
                else:
                    x = x[0]
                return x
            realname = os.path.splitext(_norm1(x))[0]
            realdeps = [_norm1(z) for z in y]
            return (realname, realdeps)

        return [_norm(x, y) for (x, y) in alldeps]

# --------------------------------------------------------------------
def _files_of_fsproj(fsproj, pure = True):
    wext = '.%s' % ('fs7' if pure else 'fsi',)

    with open(fsproj, 'r') as stream:
        doc = etree.parse(stream)

    files  = doc.findall('.//{0}ItemGroup/*'.format('{%s}' % (MSBUILD,)))
    files  = [x.get('Include') for x in files if x.get('Include') is not None]
    files  = [x for x in files if os.path.splitext(x)[1].lower() == wext]
    files  = [os.path.splitext(x)[0] for x in files]
    srcdir = os.path.dirname(fsproj) or os.path.curdir

    return Object(srcdir = srcdir, files = files)

# --------------------------------------------------------------------
def _main():
    options = _options(sys.argv[1:])

    fsprojs_ext = [_files_of_fsproj(x, False) for x in options.includes]
    fsproj      = _files_of_fsproj(options.fsproj)

    fs7deps    = FS7Deps.by_parsing(fsproj, fsprojs_ext)
    fs7deps_m  = dict(fs7deps)
    fs7default = [x for (x, _) in fs7deps if x in FS7DEFAULT]

    if options.mode == 'makefile':
        print "# -*- Makefile -*-"
        print "# Automatically generated by: %s" % (' '.join(sys.argv),)
        print "# Generated on %s" % (time.ctime(),)
        print "# Use [make regen] to regenerate this Makefile"
        print
        print MKHEADER
        print "# ----- BEGIN AUTO FS7 -----"
        for name, deps in fs7deps:
            fargs = dict(vname = re.sub('\W', '_', name),
                         name  = name,
                         mod   = name.lower(),
                         deps  = ' '.join(deps))
            print '%(name)s.tc7: $(libperv) $(libfs7) %(deps)s %(name)s.fs7 %(name)s.fs %(name)s.fs7' % fargs
            print '\t@echo '
            print '\t@echo Lemma $@'
            print '\t$(monoexe) $(f7) $(f7flags) $(f7flags_%(vname)s) -scripts %(name)s -why %(name)s.why %(deps)s %(name)s.fs7 %(name)s.fs | tee $@' % fargs
            print
        print 'check-xunit: clean'
        print '\t../scripts/xunit-tc7 --xunit=$(xunit) %s' % (' '.join(fs7default),)
        print "# ----- END AUTO FS7 -----"

    if options.mode == 'defaults':
        print ' '.join(fs7default)

    if options.mode == 'json':
        jsondata = dict()
        for name, deps in fs7deps:
            name = os.path.basename(name)
            deps = map(os.path.basename, deps)
            deps = [os.path.splitext(x)[0] for x in deps]
            jsondata[name] = deps
        print json.dumps(jsondata)

# --------------------------------------------------------------------
if __name__ == '__main__':
    _main()