Revision 773e148c25d538ffb496a2f34648359863627a13 authored by Jay Bosamiya on 06 June 2019, 22:50:05 UTC, committed by Jay Bosamiya on 06 June 2019, 22:50:05 UTC
1 parent 61edaee
SConstruct
# This file requires Python version >= 3.6
# This file requires SCons version >= 3.00
# See ./INSTALL.md for more information
##################################################################################################
#
# Here are some background notes on SCons for anyone interested in reading or editing this file.
# See https://scons.org/documentation.html for more information.
#
# SCons is a build tool, like Make. Similar to Make, it builds a graph of dependencies and
# commands that should be run when files change. However, unlike Make, SCons does not have a
# specialized language to describe the graph. Instead, SCons runs a user-supplied Python script
# named "SConstruct" to construct the graph. After the script completes, the SCons engine
# uses the constructed graph to analyze dependencies and run commands. (Note that unlike Make,
# SCons's default dependency analysis uses file hashes rather than timestamps.)
#
# For example, consider the following Makefile:
#
# b.txt : a1.txt sub/a2.txt
# cmd1 a1.txt sub\\a2.txt > b.txt
# c.txt : b.txt
# cmd2 b.txt > c.txt
#
# The most direct SCons equivalent of this is the following Python code:
#
# Command('b.txt', ['a1.txt', 'sub/a2.txt'], 'cmd1 a1.txt sub\\a2.txt > b.txt')
# Command('c.txt', 'b.txt', 'cmd2 b.txt > c.txt')
#
# However, SCons encourages a more platform-neutral style, based on two concepts: nodes and
# environments. For example, the code above contains a string that is hard-wired to use
# Windows-style backslashes rather than Unix-style forward slashes. Instead of writing strings,
# SCons allows scripts to construct abstract "nodes" that can represent graph nodes such as files.
# SCons can then convert those nodes into paths with forward or backward slashes depending on
# the platform:
#
# # First construct File nodes for each file name (using forward slashes, even on Windows):
# a1 = File('a1.txt')
# a2 = File('sub/a2.txt')
# b = File('b.txt')
# c = File('c.txt')
# # Then let SCons convert the File nodes into strings:
# Command(b, [a1, a2], f'cmd1 {a1} {a2} > {b}')
# Command(c, b, f'cmd2 {b} > {c}')
#
# Scripts can say str(a1), a1.path, a1.abspath, etc. to convert a node to a string. The code
# above uses Python's f-strings (formatted string literals) to convert nodes to strings and embed
# them into larger strings ( https://docs.python.org/3/whatsnew/3.6.html#pep-498-formatted-string-literals ).
#
# SCons encourages scripts to write functions that accept and pass nodes rather than strings
# For example, the built-in SCons object-file generator will generate an object file node, whose
# actual string representation may be "foo.o" using Unix tools or "foo.obj" using Windows tools:
#
# foo_c = File('foo.c')
# foo_obj = Object(foo_c) # compile foo.c to foo.o or foo.obj
#
# (Note that "foo_obj = Object('foo.c')" is also ok, because most built-in SCons functions
# convert string names to nodes automatically.)
#
# In addition to encouraging platform independence, SCons tries to encourage independence from
# users' configurations. In particular, by default, it executes commands in a minimal
# environment with a minimal PATH, such as ['/usr/local/bin', '/bin', '/usr/bin'] on Unix.
# The Environment function creates a new minimal environment:
#
# env = Environment()
#
# Scripts can then customize various environments to change the PATH, change the default
# C/C++/Assembly tools, change the flags passed to various tools, etc:
#
# env.Append(CCFLAGS=['-O3', '-flto', '-g', '-DKRML_NOUINT128', '-std=c++11'])
# env.PrependENVPath('PATH', os.path.dirname(str(gmp_dll)))
#
# Built in top-level functions like "Command(...)" and "Object(...)" execute in a default
# environment. To run them in a custom environment, simply call them as methods of an
# environment object:
#
# env.Command(b, [a1, a2], f'cmd1 {a1} {a2} > {b}')
# env.Command(c, b, f'cmd2 {b} > {c}')
# foo_obj = env.Object(foo_c)
#
# SCons has many other features, but for simplicity, the code in this file uses SCons features
# sparingly, preferring Python features (such as f-strings) to SCons features (such as
# SCons's own string substitution for special variables like $SOURCES) when possible.
# Our hope is that this Python-centric style will be more approachable to newcomers.
#
##################################################################################################
import re
import sys
import os, os.path
import subprocess
import traceback
import pdb
import SCons.Util
import atexit
import platform
import fnmatch
import pathlib
import shutil
if sys.version_info < (3, 6):
print(f'Requires Python version >= 3.6, found version {sys.version_info}') # If the syntax of this line is invalid, the version of Python is probably older than 3.6
exit(1)
##################################################################################################
#
# Command-line options
#
##################################################################################################
if 'VALE_HOME' in os.environ:
vale_default_path = os.environ['VALE_HOME']
else:
vale_default_path = '../../vale'
if 'KREMLIN_HOME' in os.environ:
kremlin_default_path = os.environ['KREMLIN_HOME']
else:
kremlin_default_path = '../../kremlin'
if 'FSTAR_HOME' in os.environ:
fstar_default_path = os.environ['FSTAR_HOME']
else:
fstar_default_path = '../../FStar'
def AddOptYesNo(name, dest, default, help):
AddOption('--' + name, dest = dest, default = default, action = 'store_true', help = f'{help} (default {default})')
AddOption('--NO-' + name, dest = dest, default = default, action = 'store_false')
# Retrieve tool-specific command overrides passed in by the user
AddOption('--VALE-PATH', dest = 'vale_path', type = 'string', default = vale_default_path, action = 'store',
help = 'Specify the path to Vale tool')
AddOption('--KREMLIN-PATH', dest = 'kremlin_path', type = 'string', default = kremlin_default_path, action = 'store',
help = 'Specify the path to kreMLin')
AddOption('--FSTAR-PATH', dest = 'fstar_path', type = 'string', default = fstar_default_path, action = 'store',
help = 'Specify the path to F* tool')
AddOption('--FSTAR-Z3', dest = 'fstar_z3', type = 'string', default = '', action = 'store',
help = 'Specify the path to z3 or z3.exe for F*')
AddOptYesNo('FSTAR-MY-VERSION', dest = 'fstar_my_version', default = False,
help = 'Use version of F* that does not necessarily match .tested_fstar_version')
AddOptYesNo('Z3-MY-VERSION', dest = 'z3_my_version', default = False,
help = 'Use version of Z3 that does not necessarily match .tested_z3_version')
AddOptYesNo('VALE-MY-VERSION', dest = 'vale_my_version', default = False,
help = 'Use version of Vale that does not necessarily match .vale_version')
AddOptYesNo('RECORD-HINTS', dest = 'record_hints', default = False,
help = 'Record new F* .hints files into the hints directory')
AddOptYesNo('USE-HINTS', dest = 'use_hints', default = True,
help = 'Use F* .hints files from the hints directory')
AddOption('--FARGS', dest = 'fstar_user_args', type = 'string', default = [], action = 'append',
help = 'Supply temporary additional arguments to the F* compiler')
AddOption('--VARGS', dest = 'vale_user_args', type = 'string', default = [], action = 'append',
help = 'Supply temporary additional arguments to the Vale compiler')
AddOption('--KARGS', dest = 'kremlin_user_args', type = 'string', default = [], action = 'append',
help = 'Supply temporary additional arguments to the Kremlin compiler')
AddOption('--CARGS', dest = 'c_user_args', type = 'string', default = [], action = 'append',
help = 'Supply temporary additional arguments to the C compiler')
AddOption('--OPENSSL', dest = 'openssl_path', type = 'string', default = None, action = 'store',
help = 'Specify the path to the root of an OpenSSL source tree')
AddOption('--CACHE-DIR', dest = 'cache_dir', type = 'string', default = None, action = 'store',
help = 'Specify the SCons Shared Cache Directory')
AddOptYesNo('VERIFY', dest = 'verify', default = True,
help = 'Verify and compile, or compile only')
AddOption('--ONE', dest = 'single_vaf', type = 'string', default = None, action = 'store',
help = 'Only verify one specified .vaf file, and in that file, only verify procedures or verbatim blocks marked as {:verify}.')
AddOptYesNo('COLOR', dest = 'do_color', default = True,
help="Add color to build output")
AddOptYesNo('DUMP-ARGS', dest = 'dump_args', default = False,
help = "Print arguments that will be passed to the verification tools")
AddOptYesNo('FSTAR-EXTRACT', dest = 'fstar_extract', default = False,
help = "Generate .S and .asm files via F* extraction to OCaml")
AddOptYesNo('MIN-TEST', dest = 'min_test', default = False,
help = "Only run on a minimal set of test files")
AddOptYesNo('PROFILE', dest = 'profile', default = False,
help = "Turn on profile options to measure verification performance (note: --NO-USE-HINTS is recommended when profiling)")
is_help = GetOption('help')
vale_path = Dir(GetOption('vale_path')).abspath
kremlin_path = Dir(GetOption('kremlin_path')).abspath
fstar_path = Dir(GetOption('fstar_path')).abspath
fstar_user_args = GetOption('fstar_user_args')
vale_user_args = GetOption('vale_user_args')
kremlin_user_args = GetOption('kremlin_user_args')
c_user_args = GetOption('c_user_args')
openssl_path = GetOption('openssl_path')
fstar_my_version = GetOption('fstar_my_version')
z3_my_version = GetOption('z3_my_version')
vale_my_version = GetOption('vale_my_version')
fstar_extract = GetOption('fstar_extract')
record_hints = GetOption('record_hints')
use_hints = GetOption('use_hints')
do_color = GetOption('do_color')
dump_args = GetOption('dump_args')
single_vaf = GetOption('single_vaf')
is_single_vaf = not (single_vaf is None)
min_test = GetOption('min_test')
profile = GetOption('profile')
##################################################################################################
#
# Environment settings
#
##################################################################################################
common_env = Environment()
common_env.Append(CCFLAGS = c_user_args)
target_arch = 'x86'
if (sys.platform == 'win32' and os.getenv('PLATFORM') == 'X64') or platform.machine() == 'x86_64':
target_arch = 'amd64'
common_env['TARGET_ARCH'] = target_arch
mono = ''
if not is_help:
if sys.platform == 'win32':
import importlib.util
common_env.Replace(CCPDBFLAGS = '/Zi /Fd${TARGET.base}.pdb')
# Use kremlib.h without primitive support for uint128_t.
common_env.Append(CCFLAGS = ['/Ox', '/Gz', '/DKRML_NOUINT128'])
common_env.Append(LINKFLAGS = ['/DEBUG'])
if os.getenv('PLATFORM') == 'X64':
common_env['AS'] = 'ml64'
if 'SHELL' in os.environ and importlib.util.find_spec('win32job') != None and importlib.util.find_spec('win32api'):
# Special job handling for cygwin so that child processes exit when the parent process exits
import win32job
import win32api
hdl = win32job.CreateJobObject(None, "")
win32job.AssignProcessToJobObject(hdl, win32api.GetCurrentProcess())
extended_info = win32job.QueryInformationJobObject(None, win32job.JobObjectExtendedLimitInformation)
extended_info['BasicLimitInformation']['LimitFlags'] = win32job.JOB_OBJECT_LIMIT_KILL_ON_JOB_CLOSE
win32job.SetInformationJobObject(hdl, win32job.JobObjectExtendedLimitInformation, extended_info)
else:
common_env.Append(CCFLAGS = ['-O3', '-flto', '-g', '-DKRML_NOUINT128'])
common_env.Append(CXXFLAGS = ['-std=c++11']) # This option is C++ specific
mono = 'mono'
if sys.platform == 'win32':
# fstar.exe relies on libgmp-10.dll
gmp_dll = FindFile('libgmp-10.dll', os.environ['PATH'].split(';'))
if gmp_dll != None:
common_env.PrependENVPath('PATH', os.path.dirname(str(gmp_dll)))
# Helper class to specify per-file command-line options for verification.
class BuildOptions:
# First argument is mandatory (verification options); all others are optional named arguments
def __init__(self, args, vale_includes = None):
self.env = common_env.Clone()
self.verifier_flags = args
self.vale_includes = vale_includes
##################################################################################################
#
# Configuration settings
#
##################################################################################################
def fstar_default_args_nosmtencoding(relative=True):
cache_dir = 'obj/cache_checked'
cache_dir = cache_dir if relative else os.path.abspath(cache_dir)
return ('--max_fuel 1 --max_ifuel 1'
+ (' --initial_ifuel 1' if is_single_vaf else ' --initial_ifuel 0')
# The main purpose of --z3cliopt smt.QI.EAGER_THRESHOLD=100 is to make sure that matching loops get caught
# Don't remove unless you're sure you've used the axiom profiler to make sure you have no matching loops
+ ' --z3cliopt smt.arith.nl=false --z3cliopt smt.QI.EAGER_THRESHOLD=100 --z3cliopt smt.CASE_SPLIT=3'
+ ' --hint_info'
+ (' --use_hints --use_hint_hashes' if use_hints else '')
+ (' --cache_off' if record_hints else ' --cache_checked_modules')
+ ' --cache_dir ' + cache_dir
+ ' --use_extracted_interfaces true'
)
def fstar_default_args(relative=True):
return (fstar_default_args_nosmtencoding(relative)
+ ' --smtencoding.elim_box true --smtencoding.l_arith_repr native --smtencoding.nl_arith_repr wrapped'
)
fstar_record_hints = ' --record_hints' if record_hints else ''
vale_scons_args = '-disableVerify -omitUnverified' if is_single_vaf else ''
vale_includes = f'-include {File("code/lib/util/Operator.vaf")}'
if min_test:
verify_paths = [
'code/arch',
'code/lib',
'code/crypto/poly1305',
'code/thirdPartyPorts/OpenSSL/poly1305',
'specs',
]
else:
verify_paths = [
'code',
'specs',
]
class ExternalFile:
def __init__ (self, filename):
self.filename = filename
def obj_name(self):
return 'obj/external/' + os.path.basename(self.filename)
external_files = [
ExternalFile(f'{kremlin_path}/kremlib/C.Loops.fst'),
ExternalFile(f'{kremlin_path}/kremlib/Spec.Loops.fst'),
ExternalFile(f'{kremlin_path}/kremlib/FStar.Kremlin.Endianness.fst'),
ExternalFile('../specs/Spec.Hash.PadFinish.fst'),
ExternalFile('../specs/Spec.Hash.Lemmas0.fst'),
ExternalFile('../specs/Spec.Hash.Lemmas.fst'),
ExternalFile('../specs/derived/Spec.Hash.Incremental.fst'),
ExternalFile('../specs/Spec.SHA2.fst'),
ExternalFile('../specs/Spec.SHA2.fsti'),
ExternalFile('../specs/Spec.SHA2.Constants.fst'),
ExternalFile('../specs/Spec.SHA1.fsti'),
ExternalFile('../specs/Spec.SHA1.fst'),
ExternalFile('../specs/Spec.MD5.fst'),
ExternalFile('../specs/Spec.MD5.fsti'),
ExternalFile('../specs/Spec.Hash.fst'),
ExternalFile('../specs/Spec.Hash.Definitions.fst'),
ExternalFile('../lib/Lib.IntTypes.fst'),
ExternalFile('../lib/Lib.IntTypes.fsti'),
ExternalFile('../lib/Lib.ByteSequence.fst'),
ExternalFile('../lib/Lib.ByteSequence.fsti'),
ExternalFile('../lib/Lib.RawIntTypes.fst'),
ExternalFile('../lib/Lib.RawIntTypes.fsti'),
ExternalFile('../lib/Lib.LoopCombinators.fst'),
ExternalFile('../lib/Lib.LoopCombinators.fsti'),
ExternalFile('../lib/Lib.Sequence.fst'),
ExternalFile('../lib/Lib.Sequence.fsti'),
]
no_extraction_files = [File(x) for x in [
'obj/ml_out/CanonCommMonoid.ml',
'obj/ml_out/CanonCommSemiring.ml',
'obj/ml_out/X64_Poly1305_Math.ml',
'obj/ml_out/Vale_Tactics.ml',
'obj/ml_out/FastHybrid_helpers.ml',
'obj/ml_out/FastMul_helpers.ml',
'obj/ml_out/FastSqr_helpers.ml',
'obj/ml_out/FastUtil_helpers.ml',
]]
#
# Table of files we exclude from the minimal test suite
# (typically for performance reasons)
# Note that the entries below are prefixes of blacklisted files
#
min_test_suite_blacklist = [File(x) for x in [
'code/arch/x64/X64.Vale.InsSha.vaf'
]] + [Dir(x) for x in [
'code/arch/x64/interop/',
]]
manual_dependencies = {
}
#
# Table of special-case sources which requires non-default arguments
#
verify_options = [
('code/lib/util/Operator.vaf', BuildOptions(fstar_default_args(), vale_includes = '')),
# Special treatment for sensitive modules
# Disable verification by adding 'filename': None
# ('code/thirdPartyPorts/rfc7748/curve25519/x64/X64.FastSqr.vaf', None),
# Temporarily deactivate verification of the whole interop layer in scons, since the Makefile will check
('code/arch/x64/interop/*', None),
#('code/thirdPartyPorts/OpenSSL/sha/X64.SHA.vaf', None),
# ('code/arch/x64/interop/GCMencryptOpt_stdcalls.fst', BuildOptions(fstar_default_args_nosmtencoding())),
# ('code/arch/x64/interop/GCMencrypt_stdcalls.fst', BuildOptions(fstar_default_args_nosmtencoding())),
('code/*/*.fst', BuildOptions(fstar_default_args())),
('code/*/*.fsti', BuildOptions(fstar_default_args())),
('specs/*/*.fst', BuildOptions(fstar_default_args())),
('specs/*/*.fsti', BuildOptions(fstar_default_args())),
# .fst/.fsti files default to this set of options
('.fst', BuildOptions(fstar_default_args() + ' --use_two_phase_tc false')),
('.fsti', BuildOptions(fstar_default_args() + ' --use_two_phase_tc false')),
('code/arch/x64/X64.Leakage_Ins.fst', None),
('code/arch/x64/X64.Leakage_Ins_Xmm.fst', None),
('code/arch/x64/Views.fst', BuildOptions(fstar_default_args().replace('--smtencoding.nl_arith_repr wrapped', '--smtencoding.nl_arith_repr native'))),
('code/arch/x64/X64.Bytes_Semantics.fst', BuildOptions(fstar_default_args().replace('--smtencoding.nl_arith_repr wrapped', '--smtencoding.nl_arith_repr native'))),
('code/lib/collections/Collections.Lists.fst', BuildOptions(fstar_default_args().replace('--z3cliopt smt.QI.EAGER_THRESHOLD=100',''))),
('code/arch/x64/X64.Memory.fst', BuildOptions(fstar_default_args_nosmtencoding().replace('--use_extracted_interfaces true', '').replace('--z3cliopt smt.arith.nl=false', '') + '--smtencoding.elim_box true ')),
('code/arch/x64/X64.Memory_Sems.fst', BuildOptions(fstar_default_args_nosmtencoding().replace('--use_extracted_interfaces true', '').replace('--z3cliopt smt.arith.nl=false', '') + '--smtencoding.elim_box true ')),
('code/arch/x64/Interop.fst', BuildOptions(fstar_default_args_nosmtencoding().replace('--use_extracted_interfaces true', '').replace('--z3cliopt smt.QI.EAGER_THRESHOLD=100', '') + '--smtencoding.elim_box true ')),
('code/lib/util/BufferViewHelpers.fst' , BuildOptions(fstar_default_args_nosmtencoding().replace('--z3cliopt smt.arith.nl=false', ''))),
# We copy these files from F*'s library because we need to generate a .checked file for them,
# but we don't need to reverify them:
('obj/external/*.fsti', BuildOptions('--cache_checked_modules --admit_smt_queries true')),
('obj/external/*.fst', BuildOptions('--cache_checked_modules --admit_smt_queries true')),
# .vaf files default to this set of options when compiling .fst/.fsti
('.vaf', BuildOptions(fstar_default_args() + ' --use_two_phase_tc false'))
]
verify_options_dict = { k:v for (k,v) in verify_options}
# --NOVERIFY is intended for CI scenarios, where the Win32/x86 build is verified, so
# the other build flavors do not redundently re-verify the same results.
fstar_no_verify = ''
verify = GetOption('verify')
if not verify:
print('***\n*** WARNING: NOT VERIFYING ANY CODE\n***')
fstar_no_verify = '--admit_smt_queries true'
# Find Z3 for F*
found_z3 = False
if not is_help:
fstar_z3 = GetOption('fstar_z3')
if fstar_z3 == '':
fstar_z3 = File('tools/Z3/z3.exe').path if sys.platform == 'win32' else 'tools/Z3/z3'
if os.path.isfile(fstar_z3):
found_z3 = True
else:
if sys.platform == 'win32':
find_z3 = FindFile('z3.exe', os.environ['PATH'].split(';'))
else:
find_z3 = FindFile('z3', os.environ['PATH'].split(':'))
if find_z3 != None:
found_z3 = True
fstar_z3 = str(find_z3)
else:
found_z3 = True
fstar_z3_path = '--smt ' + (os.path.abspath(fstar_z3) if dump_args else fstar_z3)
else:
fstar_z3_path = ''
vale_exe = File(f'{vale_path}/bin/vale.exe')
import_fstar_types_exe = File(f'{vale_path}/bin/importFStarTypes.exe')
fstar_exe = File(f'{fstar_path}/bin/fstar.exe')
def add_from_os_env(env, name):
if name in os.environ:
env['ENV'][name] = os.environ[name]
ocaml_env = Environment()
add_from_os_env(ocaml_env, 'PATH')
add_from_os_env(ocaml_env, 'OCAMLPATH')
add_from_os_env(ocaml_env, 'OCAMLLIB')
add_from_os_env(ocaml_env, 'OCAML_TOPLEVEL_PATH')
add_from_os_env(ocaml_env, 'CAML_LD_LIBRARY_PATH')
##################################################################################################
#
# Global variables
#
##################################################################################################
all_modules = [] # string names of modules
src_include_paths = [] # string paths in sources where .fst, .fsti are found
obj_include_paths = [] # string paths in obj/, but omitting the 'obj/' prefix
ml_out_deps = {}
fsti_map = {} # map module names to .fsti File nodes (or .fst File nodes if no .fsti exists)
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_open_re = re.compile(r'open\s+([a-zA-Z0-9_.]+)')
vale_friend_re = re.compile(r'friend\s+([a-zA-Z0-9_.]+)')
vale_import_re = re.compile(r'module\s+[a-zA-Z0-9_]+\s*[=]\s*([a-zA-Z0-9_.]+)')
if (not sys.stdout.isatty()) or not do_color:
# No color if the output is not a terminal or user opts out
yellow = ''
red = ''
uncolor = ''
else:
yellow = '\033[93m'
red = '\033[91;40;38;5;217m'
uncolor = '\033[0m'
##################################################################################################
#
# Utility functions
#
##################################################################################################
def print_error(s):
print(f'{red}{s}{uncolor}')
def print_error_exit(s):
print_error(s)
Exit(1)
# Given a File node for dir/dir/.../m.extension, return m
def file_module_name(file):
name = file.name
name = name[:1].upper() + name[1:] # capitalize first letter, as expected for F* module names
return os.path.splitext(name)[0]
# Return '.vaf', '.fst', etc.
def file_extension(file):
return os.path.splitext(file.path)[1]
# Drop the '.vaf', '.fst', etc.
def file_drop_extension(file):
return os.path.splitext(file.path)[0]
# Given source File node, return File node in object directory
def to_obj_dir(file):
if str(file).startswith('obj'):
return file
else:
return File(f'obj/{file}')
def to_hint_file(file):
return File(f'../hints/{file.name}.hints')
def ml_out_file(sourcefile, suffix):
module_name = file_module_name(sourcefile).replace('.', '_')
return File(f'obj/ml_out/{module_name}{suffix}')
# Is the file from our own sources, rather than an external file (e.g., like an F* library file)?
def is_our_file(file):
path = file.path
return True in [path.startswith(str(Dir(p))) for p in ['obj'] + verify_paths]
def compute_include_paths(src_include_paths, obj_include_paths, obj_prefix):
return src_include_paths + [str(Dir('obj/external'))] + [str(Dir(f'{obj_prefix}/{x}')) for x in obj_include_paths]
def compute_includes(src_include_paths, obj_include_paths, obj_prefix, relative=True):
fstar_include_paths = compute_include_paths(src_include_paths, obj_include_paths, obj_prefix)
return " ".join(["--include " + (x if relative else os.path.abspath(x)) for x in fstar_include_paths])
def CopyFile(target, source):
Command(target, source, Copy(target, source))
return target
##################################################################################################
#
# Configuration and environment functions
#
##################################################################################################
# Helper to look up a BuildOptions matching a srcpath File node, from the
# verify_options[] list, falling back on a default if no specific override is present.
def get_build_options(srcnode):
srcpath = srcnode.path
srcpath = srcpath.replace('\\', '/') # switch to posix path separators
if srcpath in verify_options_dict: # Exact match
return verify_options_dict[srcpath]
else:
for key, options in verify_options: # Fuzzy match
if fnmatch.fnmatch (srcpath, key):
return options
ext = os.path.splitext(srcpath)[1]
if ext in verify_options_dict: # Exact extension match
return verify_options_dict[ext]
else:
return None
def on_black_list(file, list):
return True in [str(file).startswith(str(entry)) for entry in list]
def check_fstar_version():
import subprocess
fstar_version_file = ".tested_fstar_version"
if os.path.isfile(fstar_version_file):
with open(fstar_version_file, 'r') as myfile:
lines = myfile.read().splitlines()
version = lines[0]
cmd = [str(fstar_exe), '--version']
o = subprocess.check_output(cmd, stderr = subprocess.STDOUT).decode('ascii')
lines = o.splitlines()
for line in lines:
if '=' in line:
key, v = line.split('=', 1)
if key == 'commit' and v == version:
return
print_error(f'Expected F* version commit={version}, but fstar --version returned the following:')
for line in lines:
print_error(' ' + line)
print_error_exit(
f'Get F* version {version} from https://github.com/FStarLang/FStar,' +
f' modify .tested_fstar_version, or use the --FSTAR-MY-VERSION option to override.' +
f' (We try to update the F* version frequently; feel free to change .tested_fstar_version' +
f' to a more recent F* version as long as the build still succeeds with the new version.' +
f' We try to maintain the invariant that the build succeeds with the F* version in .tested_fstar_version.)' +
f' See ./INSTALL.md for more information.')
def check_z3_version(fstar_z3):
import subprocess
z3_version_file = ".tested_z3_version"
if os.path.isfile(z3_version_file):
with open(z3_version_file, 'r') as myfile:
lines = myfile.read().splitlines()
version = lines[0]
cmd = [fstar_z3, '--version']
o = subprocess.check_output(cmd, stderr = subprocess.STDOUT).decode('ascii')
lines = o.splitlines()
line = lines[0]
for word in line.split(' '):
if '.' in word:
if word == version:
return
break
print_error(f'Expected Z3 version {version}, but z3 --version returned the following:')
for line in lines:
print_error(' ' + line)
print_error_exit(
f'Get a recent Z3 executable from https://github.com/FStarLang/binaries/tree/master/z3-tested,' +
f' modify .tested_z3_version, or use the --Z3-MY-VERSION option to override.' +
f' (We rarely change the Z3 version; we strongly recommend using the expected version of Z3.)' +
f' See ./INSTALL.md for more information.')
def check_vale_version():
with open(".vale_version") as f:
version = f.read().splitlines()[0]
vale_version_file = f'{vale_path}/bin/.vale_version'
vale_version = '0.2.7 or older'
if os.path.isfile(vale_version_file):
with open(vale_version_file) as f:
vale_version = f.read().splitlines()[0]
if vale_version != version:
print_error(f'Expected Vale version {version}, but found Vale version {vale_version}')
print_error_exit(
f'Get version {version} from https://github.com/project-everest/vale/releases/download/v{version}/vale-release-{version}.zip,' +
f' modify .vale_version, or use the --VALE-MY-VERSION option to override.' +
f' See ./INSTALL.md for more information.')
def print_dump_args():
#print('Currently using the following F* args:')
options = fstar_default_args(relative=False)
if len(COMMAND_LINE_TARGETS) > 0:
options = get_build_options(File(COMMAND_LINE_TARGETS[0])).verifier_flags
#print("The options are: %s" % options.verifier_flags)
fstar_includes = compute_includes(src_include_paths, obj_include_paths, 'obj', relative=False)
for option in [fstar_z3_path, fstar_no_verify, fstar_includes, fstar_user_args, options]:
if len(option) > 0:
print(f'{option} ', end='')
print()
Exit(1)
# extract a string filename out of a build failure
def bf_to_filename(bf):
import SCons.Errors
if bf is None: # unknown targets product None in list
return '(unknown tgt)'
elif isinstance(bf, SCons.Errors.StopError):
return str(bf)
elif bf.node:
return str(bf.node)
elif bf.filename:
return bf.filename
return '(unknown failure)'
def report_verification_failures():
import time
from SCons.Script import GetBuildFailures
bf = GetBuildFailures()
if bf:
# bf is normally a list of build failures; if an element is None,
# it's because of a target that scons doesn't know anything about.
for x in bf:
if x is not None:
filename = bf_to_filename(x)
if filename.endswith('.tmp') and os.path.isfile(filename):
error_filename = filename[:-len('.tmp')] + '.error'
stderr_filename = filename[:-len('.tmp')] + '.stderr'
if os.path.isfile(error_filename):
os.remove(error_filename)
report_filename = stderr_filename if os.path.isfile(stderr_filename) else filename
print()
print(f'##### {red}Verification error{uncolor}')
print('Printing contents of ' + report_filename + ' #####')
with open (report_filename, 'r') as myfile:
lines = myfile.read().splitlines()
valeErrors = [line for line in lines if ("*****" in line)]
for line in lines:
if 'error was reported' in line or '(Error)' in line or ' failed' in line:
line = f'{red}{line}{uncolor}'
print(line)
print()
time.sleep(1)
os.rename(filename, error_filename)
if filename.endswith('.dump') and os.path.isfile(filename):
stderr_filename = filename[:-len('.dump')] + '.stderr'
report_filename = stderr_filename if os.path.isfile(stderr_filename) else filename
print()
print(f'##### {red}Verification error{uncolor}')
print('Printing contents of ' + report_filename + ' #####')
with open (report_filename, 'r') as myfile:
lines = myfile.read().splitlines()
valeErrors = [line for line in lines if ("*****" in line)]
for line in lines:
if 'error was reported' in line or '(Error)' in line or ' failed' in line:
line = f'{red}{line}{uncolor}'
print(line)
print()
time.sleep(1)
##################################################################################################
#
# File and module processing functions
#
##################################################################################################
def add_module_for_file(file):
global all_modules
m = file_module_name(file)
if m in all_modules:
print(f'error: found more than one instance of module {m} (all module names must be unique for include paths to work correctly)')
Exit(1)
all_modules.append(m)
def add_include_dir_for_file(include_paths, file):
d = str(file.dir)
if not (d in include_paths):
include_paths.append(d)
pathlib.Path(str(to_obj_dir(file).dir)).mkdir(parents = True, exist_ok = True)
def include_fstar_file(env, file):
options = get_build_options(file)
add_include_dir_for_file(src_include_paths, file)
if options != None:
if (file_extension(file) == ".fst"):
add_module_for_file(file)
fsti_map[file_module_name(file)] = file
def include_vale_file(env, file):
options = get_build_options(file)
add_include_dir_for_file(obj_include_paths, file)
dummy_dir = File(f'obj/dummies/{file_drop_extension(file)}').dir
pathlib.Path(str(dummy_dir)).mkdir(parents = True, exist_ok = True)
if options != None:
add_module_for_file(file)
module_name = file_module_name(file)
fsti_map[module_name] = f'{file_drop_extension(to_obj_dir(file))}.fsti'
for extension in ['.fst', '.fsti']:
# The F* dependency analysis runs before .vaf files are converted to .fst/.fsti files,
# so generate a dummy .fst/.fsti file pair for each .vaf file for the F* dependency analysis.
dummy_file = File(f'obj/dummies/{file_drop_extension(file)}{extension}')
pathlib.Path(str(dummy_file.dir)).mkdir(parents = True, exist_ok = True)
with open(str(dummy_file), 'w') as myfile:
myfile.write(f'module {module_name}' + '\n')
def add_ml_dependencies(targets, sources):
if fstar_extract:
sources_ml = [ml_out_file(File(x), '.ml') for x in sources if is_our_file(File(x))]
targets_ml = [ml_out_file(File(x), '.ml') for x in targets if is_our_file(File(x))]
sources_ml = [x for x in sources_ml if not (x in no_extraction_files)]
targets_ml = [x for x in targets_ml if not (x in no_extraction_files)]
sources_ml = [x for x in sources_ml if not (x in targets_ml)]
Depends(targets_ml, sources_ml)
for t in targets_ml:
if not (t in ml_out_deps):
ml_out_deps[t] = set()
for s in sources_ml:
ml_out_deps[t].add(s)
# Verify a .fst or .fsti file
def verify_fstar_file(options, targetfile, sourcefile, fstar_includes):
env = options.env
stderrfile = File(f'{targetfile}.stderr')
temptargetfile = File(f'{targetfile}.tmp')
temptargetfiles = [temptargetfile]
dumptargetfile = File(re.sub('\.verified$', '.dump', str(targetfile)))
hintfile = to_hint_file(sourcefile)
if min_test and on_black_list(sourcefile, min_test_suite_blacklist):
print(f'Skipping {sourcefile} because it is on min_test_suite_blacklist')
if record_hints:
temptargetfiles.append(hintfile)
elif use_hints and os.path.isfile(str(hintfile)):
Depends(temptargetfiles, hintfile)
env.Command(temptargetfiles, sourcefile,
f'{fstar_exe} {sourcefile} {options.verifier_flags} {fstar_z3_path} {fstar_no_verify}' +
f' {fstar_includes} {" ".join(fstar_user_args)} --hint_file {hintfile} {fstar_record_hints}' +
(f' --debug {file_module_name(File(sourcefile))} --debug_level print_normalized_terms' if profile else '') +
f' 1> {temptargetfile} 2> {stderrfile}')
CopyFile(targetfile, temptargetfile)
dump_module_flag = '--dump_module ' + file_module_name(sourcefile)
dump_flags = ('--print_implicits --print_universes --print_effect_args --print_full_names' +
' --print_bound_var_types --ugly ' + dump_module_flag)
env.Command(dumptargetfile, sourcefile,
f'{fstar_exe} {sourcefile} {options.verifier_flags} {fstar_z3_path} {fstar_no_verify} --admit_smt_queries true' +
f' {fstar_includes} {" ".join(fstar_user_args)}' +
f' {dump_flags} 1>{dumptargetfile} 2>{dumptargetfile}.stderr')
Depends(dumptargetfile, targetfile)
def extract_fstar_file(options, sourcefile, fstar_includes):
env = options.env
base_name = file_drop_extension(sourcefile)
module_name = file_module_name(sourcefile)
hintfile = to_hint_file(sourcefile)
mlfile = ml_out_file(sourcefile, '.ml')
Depends(mlfile, to_obj_dir(base_name + '.fst.verified'))
verifier_flags = options.verifier_flags.replace('--use_extracted_interfaces true', '')
return env.Command(mlfile, sourcefile,
f'{fstar_exe} {sourcefile} {verifier_flags} {fstar_z3_path} {fstar_no_verify} --admit_smt_queries true' +
f' {fstar_includes} {" ".join(fstar_user_args)}' +
f' --odir obj/ml_out --codegen OCaml --extract_module {module_name}')
# Process a .fst or .fsti file
def process_fstar_file(env, file, fstar_includes):
options = get_build_options(file)
if options != None:
target = File(f'{to_obj_dir(file)}.verified')
verify_fstar_file(options, target, file, fstar_includes)
if fstar_extract:
if file_extension(file) == '.fst':
if not (ml_out_file(file, '.ml') in no_extraction_files):
extract_fstar_file(options, file, fstar_includes)
def vale_dependency_scan(env, file):
if min_test and on_black_list(file, min_test_suite_blacklist):
print(f'Skipping {file} because it is on min_test_suite_blacklist')
return
contents = file.get_text_contents()
dirname = os.path.dirname(str(file))
vaf_includes = vale_include_re.findall(contents)
fst_includes = vale_open_re.findall(contents) + vale_import_re.findall(contents)
fst_friends = vale_friend_re.findall(contents)
obj_file_base = file_drop_extension(to_obj_dir(file))
vaf_dump_deps[str(file)] = set()
vaf_vaf_deps[str(file)] = set()
fst_fsti = [f'{obj_file_base}.fst', f'{obj_file_base}.fsti']
obj_tmp = [f'{obj_file_base}.fst.verified.tmp']
obj_tmps = [f'{obj_file_base}.fst.verified.tmp', f'{obj_file_base}.fsti.verified.tmp']
typesfile = File(f'{obj_file_base}.types.vaf')
for (attrs, inc) in vaf_includes:
if vale_fstar_re.search(attrs):
dumpsourcebase = to_obj_dir(File(f'{fsti_map[inc]}'))
dumpsourcefile = File(f'{dumpsourcebase}.dump')
if is_our_file(dumpsourcebase):
vaf_dump_deps[str(file)].add(str(dumpsourcefile))
else:
print_error_exit(f'TODO: not implemented: .vaf includes extern F* file {inc}')
else:
f = os.path.join('code' if vale_from_base_re.search(attrs) else dirname, inc)
# if A.vaf includes B.vaf, then manually establish these dependencies:
# A.fst.verified.tmp depends on B.fsti.verified
# A.fsti.verified.tmp depends on B.fsti.verified
vaf_vaf_deps[str(file)].add(str(File(f)))
f_base = file_drop_extension(to_obj_dir(File(f)))
f_fsti = File(f_base + '.fsti.verified')
Depends(obj_tmps, f_fsti)
add_ml_dependencies([obj_file_base + '.fst'], [f_base + '.fst'])
Depends(fst_fsti, typesfile)
for inc in fst_includes:
if inc in fsti_map:
Depends(obj_tmps, to_obj_dir(File(f'{fsti_map[inc]}.verified')))
add_ml_dependencies([obj_file_base + '.fst'], [fsti_map[inc]])
for inc in fst_friends:
if inc in fsti_map:
Depends(obj_tmp, re.sub('\.fsti$', '.fst.verified', str(to_obj_dir(fsti_map[inc]))))
add_ml_dependencies([obj_file_base + '.fst'], [fsti_map[inc]])
# Translate Vale .vaf to F* .fst/fsti pair
# Takes a source .vaf File node
# Returns list of File nodes representing the resulting .fst and .fsti files
def translate_vale_file(options, source_vaf):
env = options.env
target = file_drop_extension(to_obj_dir(source_vaf))
target_fst = File(target + '.fst')
target_fsti = File(target + '.fsti')
targets = [target_fst, target_fsti]
opt_vale_includes = vale_includes if options.vale_includes == None else options.vale_includes
types_include = ''
types_include = f'-include {target}.types.vaf'
env.Command(targets, source_vaf,
f'{mono} {vale_exe} -fstarText -quickMods -typecheck {types_include} {opt_vale_includes}' +
f' -in {source_vaf} -out {target_fst} -outi {target_fsti}' +
f' {vale_scons_args} {" ".join(vale_user_args)}')
return targets
# Process a .vaf file
def process_vale_file(env, file, fstar_includes):
options = get_build_options(file)
if options != None:
vale_dependency_scan(env, file)
fsts = translate_vale_file(options, file)
fst = fsts[0]
fsti = fsts[1]
fst_options = get_build_options(fst)
fsti_options = get_build_options(fsti)
target = file_drop_extension(to_obj_dir(file))
target_fst = f'{target}.fst.verified'
target_fsti = f'{target}.fsti.verified'
Depends(f'{target_fst}.tmp', target_fsti)
verify_fstar_file(fst_options, target_fst, fst, fstar_includes)
verify_fstar_file(fsti_options, target_fsti, fsti, fstar_includes)
if fstar_extract:
extract_fstar_file(fst_options, fst, fstar_includes)
def compute_module_types(env, source_vaf):
source_base = file_drop_extension(to_obj_dir(File(source_vaf)))
types_vaf = f'{source_base}.types.vaf'
done = set()
dumps = []
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)
dumps.append(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)
dumps_string = " ".join(['-in ' + str(x) for x in dumps])
Depends(types_vaf, import_fstar_types_exe)
Command(types_vaf, dumps, f'{mono} {import_fstar_types_exe} {dumps_string} -out {types_vaf} > {types_vaf}.errors')
def recursive_glob(env, pattern, strings = False):
matches = []
split = os.path.split(pattern) # [0] is the directory, [1] is the actual pattern
platform_directory = split[0] #os.path.normpath(split[0])
for d in os.listdir(platform_directory):
f = os.path.join(platform_directory, d)
if os.path.isdir(f):
if min_test and on_black_list(f, min_test_suite_blacklist):
print(f'Skipping {f} because it is on min_test_suite_blacklist')
else:
newpattern = os.path.join(split[0], d, split[1])
matches.append(recursive_glob(env, newpattern, strings))
files = env.Glob(pattern, strings=strings)
for f in files:
if min_test and on_black_list(f, min_test_suite_blacklist):
print(f'Skipping {f} because it is on min_test_suite_blacklist')
else:
matches.append(f)
return Flatten([File(x) for x in matches])
# Verify *.fst, *.fsti, *.vaf files in a list of directories. This enumerates
# all files in those trees, and creates verification targets for each,
# which in turn causes a dependency scan to verify all of their dependencies.
def process_files_in(env, directories):
fsts = []
fstis = []
vafs = []
for d in directories:
fsts.extend(recursive_glob(env, d + '/*.fst', strings = True))
fstis.extend(recursive_glob(env, d + '/*.fsti', strings = True))
vafs.extend(recursive_glob(env, d + '/*.vaf', strings = True))
# Compute include directories:
for file in fsts:
include_fstar_file(env, file)
for file in fstis:
include_fstar_file(env, file)
for file in external_files:
file_node = File(file.obj_name())
fsti_map[file_module_name(file_node)] = file_node
for file in vafs:
include_vale_file(env, file)
# Process and verify files:
fstar_include_paths = compute_include_paths(src_include_paths, obj_include_paths, 'obj')
fstar_includes = compute_includes(src_include_paths, obj_include_paths, 'obj')
if is_single_vaf:
process_vale_file(env, File(single_vaf), fstar_includes)
else:
for file in fsts:
process_fstar_file(env, file, fstar_includes)
for file in fstis:
process_fstar_file(env, file, fstar_includes)
for file in external_files:
process_fstar_file(env, File(file.obj_name()), fstar_includes)
for file in vafs:
process_vale_file(env, file, fstar_includes)
for target in manual_dependencies:
Depends(target, manual_dependencies[target])
def extract_assembly_code(env, output_base_name, main_file, alg_files, cmdline_file):
# OCaml depends on many libraries and executables; we have to assume they are in the user's PATH:
ocaml_env.PrependENVPath('OCAMLPATH', fstar_path + '/bin')
main_ml = ml_out_file(main_file, '.ml')
main_cmx = ml_out_file(main_file, '.cmx')
main_exe = ml_out_file(main_file, '.exe')
alg_mls = [ml_out_file(x, '.ml') for x in alg_files]
alg_cmxs = [ml_out_file(x, '.cmx') for x in alg_files]
cmdline_ml = ml_out_file(cmdline_file, '.ml')
cmdline_cmx = ml_out_file(cmdline_file, '.cmx')
#pointer_src = File('code/lib/util/FStar_Pointer_Base.ml')
#pointer_ml = ml_out_file(pointer_src, '.ml')
#pointer_cmx = ml_out_file(pointer_src, '.cmx')
#CopyFile(pointer_ml, pointer_src)
CopyFile(cmdline_ml, cmdline_file)
CopyFile(main_ml, main_file)
for alg_cmx in alg_cmxs:
Depends(cmdline_cmx, alg_cmx)
Depends(main_cmx, alg_cmx)
Depends(cmdline_cmx, cmdline_ml)
Depends(main_cmx, cmdline_cmx)
Depends(main_cmx, main_ml)
done = set()
cmxs = []
objs = []
ignore_warnings = [ "8", # Warning 8: this pattern-matching is not exhaustive.
"20", # Warning 20: this argument will not be used by the function.
"26"] # Warning 26: unused variable
ignore_warnings_str = "-w " + "".join(["-" + s for s in ignore_warnings])
def add_cmx(x_ml):
x_cmx = ml_out_file(x_ml, '.cmx')
x_obj = ml_out_file(x_ml, '.o')
cmx = ocaml_env.Command([x_cmx, x_obj], x_ml,
f'ocamlfind ocamlopt -c -package fstarlib -o {x_cmx} {x_ml} -I obj/ml_out {ignore_warnings_str}')
cmxs.append(cmx[0])
objs.append(x_obj)
Depends(main_exe, cmx[0])
Depends(main_exe, x_obj)
def collect_cmxs_in_order(x_ml):
if not (x_ml in done):
done.add(x_ml)
for y_ml in sorted(ml_out_deps[x_ml]): # sorting makes the order deterministic, so scons doesn't needlessly rebuild
# if x depends on y, y must appear first in ocaml link step
Depends(ml_out_file(x_ml, '.cmx'), ml_out_file(y_ml, '.cmx'))
collect_cmxs_in_order(y_ml)
add_cmx(x_ml)
for alg_ml in alg_mls:
collect_cmxs_in_order(alg_ml)
add_cmx(cmdline_ml)
add_cmx(main_ml)
cmxs_string = " ".join([str(cmx) for cmx in cmxs])
ocaml_env.Command(main_exe, cmxs + objs,
f'ocamlfind ocamlopt -linkpkg -package fstarlib {cmxs_string} -o {main_exe}')
# Run executable to generate assembly files:
output_target_base = 'obj/' + output_base_name
def generate_asm(suffix, assembler, os):
# TODO: cross-compilation support; note that platform.machine() does not
# produce a consistent string across OSes
target = output_target_base + "-x86_64" + suffix
return ocaml_env.Command(target, main_exe, f'{main_exe} {assembler} {os} > {target}')
masm_win = generate_asm('-msvc.asm', 'MASM', 'Win')
gcc_win = generate_asm('-mingw.S', 'GCC', 'Win')
gcc_linux = generate_asm('-linux.S', 'GCC', 'Linux')
gcc_macos = generate_asm('-darwin.S', 'GCC', 'MacOS')
if sys.platform.startswith('linux'):
return [gcc_linux, masm_win, gcc_win, gcc_macos]
elif sys.platform == 'win32':
return [masm_win, gcc_win, gcc_linux, gcc_macos]
elif sys.platform == 'cygwin':
return [gcc_win, masm_win, gcc_linux, gcc_macos]
elif sys.platform == 'darwin':
return [gcc_macos, gcc_win, masm_win, gcc_linux]
else:
print('Unsupported sys.platform value: ' + sys.platform)
##################################################################################################
#
# FStar dependency analysis
#
##################################################################################################
def compute_fstar_deps(env, src_directories, fstar_includes):
import subprocess
# find all .fst, .fsti files in src_directories
fst_files = []
for d in src_directories:
fst_files.extend(recursive_glob(env, d+'/*.fst', strings = True))
fst_files.extend(recursive_glob(env, d+'/*.fsti', strings = True))
# use fst_files to choose .fst and .fsti files that need dependency analysis
files = []
for f in fst_files:
options = get_build_options(f)
if options != None:
files.append(f)
# call fstar --dep make
includes = []
for include in fstar_includes:
includes += ["--include", include]
lines = []
depsBackupFile = 'obj/fstarDepsBackup.d'
args = ["--dep", "make"] + includes + files
cmd = [fstar_exe] + args
cmd = [str(x) for x in cmd]
#print(" ".join(cmd))
try:
if not dump_args:
print('F* dependency analysis starting')
o = subprocess.check_output(cmd, stderr = subprocess.STDOUT).decode('ascii')
if not dump_args:
print('F* dependency analysis finished')
except (subprocess.CalledProcessError) as e:
print(f'F* dependency analysis: error: {e.output}')
Exit(1)
fstar_deps_ok = True
lines = o.splitlines()
for line in lines:
if 'Warning:' in line:
print(line)
fstar_deps_ok = False
if len(line) == 0:
pass
elif '(Warning ' in line:
# example: "(Warning 307) logic qualifier is deprecated"
pass
else:
# lines are of the form:
# a1.fst a2.fst ... : b1.fst b2.fst ...
# we change this to:
# obj\...\a1.fst.verified obj\...\a2.fst.verified ... : b1.fst.verified b2.fst.verified ...
# we ignore targets that we will not verify (e.g. F* standard libraries)
targets, sources = line.split(': ', 1) # ': ', not ':', because of Windows drive letters
sources = sources.split()
targets = targets.split()
obj_name = str(Dir('obj'))
dummies_name = str(Dir('obj/dummies'))
sources = [str(File(x)).replace(dummies_name, obj_name) for x in sources]
targets = [str(File(x)).replace(dummies_name, obj_name) for x in targets]
for source in sources:
for target in targets:
if target.startswith('specs') and (source.startswith('obj') or source.startswith('code')) and not dump_args:
print(f'{yellow}Warning: file {target} in specs directory depends on file {source} outside specs directory{uncolor}')
sources_ver = [to_obj_dir(File(re.sub('\.fst$', '.fst.verified', re.sub('\.fsti$', '.fsti.verified', x)))) for x in sources if is_our_file(File(x))]
targets_ver = [to_obj_dir(File(re.sub('\.fst$', '.fst.verified.tmp', re.sub('\.fsti$', '.fsti.verified.tmp', x)))) for x in targets if is_our_file(File(x))]
Depends(targets_ver, sources_ver)
add_ml_dependencies(targets, sources)
# Computing types from F* files
# Dump F* types for for each of a1.fst a2.fst ... into a1.fst.dump, a2.fst.dump, ...
# Targets that we don't verify go in obj/external
for t in targets:
if is_our_file(File(t)):
dumptargetfile = str(to_obj_dir(t + '.dump'))
else:
# Compute types of an external module, assuming it was compiled with default arguments
dumptargetfile = 'obj/external/' + os.path.split(t)[1] + '.dump'
dump_module_flag = '--dump_module ' + file_module_name(File(t))
dump_flags = ('--print_implicits --print_universes --print_effect_args --print_full_names' +
' --print_bound_var_types --ugly ' + dump_module_flag)
env.Command(dumptargetfile, t,
f'{fstar_exe} {t} {fstar_z3_path} {fstar_no_verify} --admit_smt_queries true' +
f' {dump_flags} 1>{dumptargetfile} 2> {dumptargetfile}.stderr')
if not (dumptargetfile in dump_deps):
dump_deps[dumptargetfile] = set()
for s in sources:
if is_our_file(File(s)):
dump_deps[dumptargetfile].add(str(to_obj_dir(s + '.dump')))
else:
dump_deps[dumptargetfile].add('obj/external/' + os.path.split(s)[1] + '.dump')
if fstar_deps_ok:
# Save results in depsBackupFile
with open(depsBackupFile, 'w') as myfile:
for line in lines:
myfile.write(line + '\n')
else:
print('F* dependency analysis failed')
Exit(1)
##################################################################################################
#
# Top-level commands
#
##################################################################################################
if not is_help:
atexit.register(report_verification_failures)
env = common_env
# Create obj directory and any subdirectories needed during dependency analysis
# (SCons will create other subdirectories during build)
pathlib.Path('obj').mkdir(parents = True, exist_ok = True)
pathlib.Path('obj/external').mkdir(parents = True, exist_ok = True)
pathlib.Path('obj/cache_checked').mkdir(parents = True, exist_ok = True)
# Check F*, Z3, and Vale versions
if not fstar_my_version:
check_fstar_version()
if not z3_my_version:
if not found_z3:
print_error_exit('Could not find z3 executable. Either put z3 in your path, or put it in the directory tools/Z3/, or use the --FSTARZ3=<z3-executable> option.')
check_z3_version(fstar_z3)
if not vale_my_version:
check_vale_version()
# HACK: copy external files
for f in external_files:
source = f.filename
target = f.obj_name()
shutil.copy(source, target)
if not dump_args:
print('Processing source files')
process_files_in(env, verify_paths)
if not is_single_vaf:
compute_fstar_deps(env, verify_paths, compute_include_paths(src_include_paths, obj_include_paths, 'obj/dummies'))
for x in vaf_dump_deps:
compute_module_types(env, x)
if fstar_extract and not min_test:
# Build AES-GCM
aesgcm_asm = extract_assembly_code(env, 'aesgcm', File('code/crypto/aes/x64/Main.ml'),
[File('code/crypto/aes/x64/X64.GCMdecrypt.vaf')], File('code/lib/util/CmdLineParser.ml'))
cpuid_asm = extract_assembly_code(env, 'cpuid', File('code/lib/util/x64/CpuidMain.ml'),
[File('code/lib/util/x64/stdcalls/X64.Cpuidstdcall.vaf')], File('code/lib/util/CmdLineParser.ml'))
sha256_asm = extract_assembly_code(env, 'sha256', File('code/crypto/sha/ShaMain.ml'),
[File('code/thirdPartyPorts/OpenSSL/sha/X64.SHA.vaf')], File('code/lib/util/CmdLineParser.ml'))
curve25519_asm = extract_assembly_code(env, 'curve25519', File('code/crypto/ecc/curve25519/Main25519.ml'), [
File('code/thirdPartyPorts/rfc7748/curve25519/X64.FastUtil.vaf'),
File('code/thirdPartyPorts/rfc7748/curve25519/X64.FastHybrid.vaf'),
File('code/thirdPartyPorts/rfc7748/curve25519/X64.FastWide.vaf'),
File('code/thirdPartyPorts/rfc7748/curve25519/X64.FastSqr.vaf'),
File('code/thirdPartyPorts/rfc7748/curve25519/X64.FastMul.vaf')],
File('code/lib/util/CmdLineParser.ml'))
if env['TARGET_ARCH'] == 'amd64':
aesgcmasm_obj = env.Object('obj/aesgcmasm_openssl', aesgcm_asm[0])
aesgcmtest_src = File('code/crypto/aes/x64/TestAesGcm.cpp')
aesgcmtest_cpp = to_obj_dir(aesgcmtest_src)
CopyFile(aesgcmtest_cpp, aesgcmtest_src)
aesgcmtest_exe = env.Program(source = [aesgcmasm_obj, aesgcmtest_cpp], target = 'obj/TestAesGcm.exe')
sha256asm_obj = env.Object('obj/sha256asm_openssl', sha256_asm[0])
sha256test_src = File('code/crypto/sha/TestSha.cpp')
sha256test_cpp = to_obj_dir(sha256test_src)
CopyFile(sha256test_cpp, sha256test_src)
sha256test_exe = env.Program(source = [sha256asm_obj, sha256test_cpp], target = 'obj/TestSha.exe')
curve25519asm_obj = env.Object('obj/curve25519asm_openssl', curve25519_asm[0])
curve25519test_src = File('code/crypto/ecc/curve25519/test_ecc.c')
curve25519test_cpp = to_obj_dir(curve25519test_src)
CopyFile(curve25519test_cpp, curve25519test_src)
curve25519test_exe = env.Program(source = [curve25519asm_obj, curve25519test_cpp], target = 'obj/TestEcc.exe')
if dump_args:
print_dump_args()
Computing file changes ...