# 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/Vale.Lib.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/Vale.Lib.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())),
  ('.fsti', BuildOptions(fstar_default_args())),

  ('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()))
]

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()