sail.ml

(****************************************************************************)
(*     Sail                                                                 *)
(*                                                                          *)
(*  Sail and the Sail architecture models here, comprising all files and    *)
(*  directories except the ASL-derived Sail code in the aarch64 directory,  *)
(*  are subject to the BSD two-clause licence below.                        *)
(*                                                                          *)
(*  The ASL derived parts of the ARMv8.3 specification in                   *)
(*  aarch64/no_vector and aarch64/full are copyright ARM Ltd.               *)
(*                                                                          *)
(*  Copyright (c) 2013-2021                                                 *)
(*    Kathyrn Gray                                                          *)
(*    Shaked Flur                                                           *)
(*    Stephen Kell                                                          *)
(*    Gabriel Kerneis                                                       *)
(*    Robert Norton-Wright                                                  *)
(*    Christopher Pulte                                                     *)
(*    Peter Sewell                                                          *)
(*    Alasdair Armstrong                                                    *)
(*    Brian Campbell                                                        *)
(*    Thomas Bauereiss                                                      *)
(*    Anthony Fox                                                           *)
(*    Jon French                                                            *)
(*    Dominic Mulligan                                                      *)
(*    Stephen Kell                                                          *)
(*    Mark Wassell                                                          *)
(*    Alastair Reid (Arm Ltd)                                               *)
(*                                                                          *)
(*  All rights reserved.                                                    *)
(*                                                                          *)
(*  This work was partially supported by EPSRC grant EP/K008528/1 <a        *)
(*  href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous          *)
(*  Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA   *)
(*  KTF funding, and donations from Arm.  This project has received         *)
(*  funding from the European Research Council (ERC) under the European     *)
(*  Union’s Horizon 2020 research and innovation programme (grant           *)
(*  agreement No 789108, ELVER).                                            *)
(*                                                                          *)
(*  This software was developed by SRI International and the University of  *)
(*  Cambridge Computer Laboratory (Department of Computer Science and       *)
(*  Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV")        *)
(*  and FA8750-10-C-0237 ("CTSRD").                                         *)
(*                                                                          *)
(*  SPDX-License-Identifier: BSD-2-Clause                                   *)
(****************************************************************************)

open Libsail

open Interactive.State
open Sail_options

let opt_new_cli = ref false
let opt_free_arguments : string list ref = ref []
let opt_file_out : string option ref = ref None
let opt_just_check : bool ref = ref false
let opt_just_parse_project : bool ref = ref false
let opt_auto_interpreter_rewrites : bool ref = ref false
let opt_interactive_script : string option ref = ref None
let opt_splice : string list ref = ref []
let opt_print_version = ref false
let opt_require_version : string option ref = ref None
let opt_no_core = ref false
let opt_memo_z3 = ref true
let opt_memo_z3_path = ref "sail_smt_cache"
let opt_have_feature = ref None
let opt_all_modules = ref false
let opt_show_sail_dir = ref false
let opt_project_files : string list ref = ref []
let opt_variable_assignments : string list ref = ref []
let opt_model_config_file : string option ref = ref None
let opt_sail_config_file : string option ref = ref None
let opt_format = ref false
let opt_format_backup : string option ref = ref None
let opt_format_only : string list ref = ref []
let opt_format_emit : string ref = ref "file"
let opt_format_skip : string list ref = ref []
let opt_format_debug : bool ref = ref false
let opt_slice_instantiation_types : bool ref = ref false
let opt_output_schema_file : string option ref = ref None
let opt_warn_error : bool ref = ref false

let is_bytecode = Sys.backend_type = Bytecode

(* Allow calling all options as either -foo_bar, -foo-bar, or
   --foo-bar (for long options). The standard long-opt version
   --foo-bar is treated as the canonical choice. If !opt_new_cli is
   set we warn for any non-canonical options. *)
let rec fix_options = function
  | (flag, spec, doc) :: opts ->
      if flag = "-help" || flag = "--help" then (flag, spec, doc) :: fix_options opts
      else (
        let dash_flag = String.map (function '_' -> '-' | c -> c) flag in
        let canonical_flag = if String.length flag > 2 then "-" ^ dash_flag else dash_flag in
        let non_canonical spec =
          if !opt_new_cli then (
            let explanation =
              Printf.sprintf "Old style command line flag %s used, use %s instead" flag canonical_flag
            in
            Arg.Tuple
              [Arg.Unit (fun () -> Reporting.warn Version.v0_20_2 "Old style flag" Parse_ast.Unknown explanation); spec]
          )
          else spec
        in
        if canonical_flag = flag then (flag, spec, doc) :: fix_options opts
        else if dash_flag = flag then (flag, non_canonical spec, "") :: (canonical_flag, spec, doc) :: fix_options opts
        else
          (flag, non_canonical spec, "")
          :: (dash_flag, non_canonical spec, "")
          :: (canonical_flag, spec, doc) :: fix_options opts
      )
  | [] -> []

(* This function does roughly the same thing as Arg.align, except we
   can call it per target and it won't add additional -help
   options. *)
let target_align opts =
  let split_doc doc =
    if String.length doc > 0 then
      if doc.[0] = ' ' then ("", doc)
      else if doc.[0] = '\n' then ("", doc)
      else (
        match String.index_from_opt doc 0 ' ' with
        | Some n -> (String.sub doc 0 n, String.sub doc n (String.length doc - n))
        | None -> ("", doc)
      )
    else ("", "")
  in
  let opts = List.map (fun (flag, spec, doc) -> (flag, spec, split_doc doc)) opts in
  let alignment = List.fold_left (fun a (flag, _, (arg, _)) -> max a (String.length flag + String.length arg)) 0 opts in
  let opts =
    List.map
      (fun (flag, spec, (arg, doc)) ->
        if doc = "" then (flag, spec, arg)
        else (flag, spec, arg ^ String.make (max 0 (alignment - (String.length flag + String.length arg))) ' ' ^ doc)
      )
      opts
  in
  opts

(* Add a header to separate arguments from each plugin *)
let add_target_header plugin opts =
  let add_header (flag, spec, doc) =
    let desc =
      match Target.extract_registered () with
      | [] -> "plugin " ^ plugin
      | [name] -> "target " ^ name
      | names -> "targets " ^ Util.string_of_list ", " (fun x -> x) names
    in
    (flag, spec, doc ^ " \n\nOptions for " ^ desc)
  in
  Util.update_last add_header opts

let load_plugin opts plugin =
  try
    if is_bytecode then Dynlink.loadfile plugin else Dynlink.loadfile_private plugin;
    let plugin_opts = Target.extract_options () |> List.map Flag.to_arg |> fix_options |> target_align in
    opts := add_target_header plugin !opts @ plugin_opts
  with Dynlink.Error msg -> prerr_endline ("Failed to load plugin " ^ plugin ^ ": " ^ Dynlink.error_message msg)

let parse_instantiation inst =
  let open Ast_compare in
  let open Ast_util in
  let open Lexing in
  match String.split_on_char '=' inst with
  | abstract_type :: value ->
      let inline =
        match Preprocess.get_argv_position ~plus:1 with
        | Some p -> Some { p with pos_cnum = p.pos_cnum + String.length abstract_type + 1 }
        | None -> None
      in
      let value = String.concat "=" value in
      let abstract_type = mk_id (String.trim abstract_type) in
      let parse_value kind =
        let open Initial_check in
        parse_from_string ?inline value (fun (module Parse : PARSER) handle lexbuf ->
            to_ast_typ_arg kind initial_ctx (Parse.typ_eof (Lexer.token handle (ref [])) lexbuf)
        )
      in
      opt_instantiations := Bindings.add abstract_type parse_value !opt_instantiations
  | _ -> raise (Reporting.err_general Parse_ast.Unknown "Failed to parse command-line instantiate flag")

(* Version as a string, e.g. "1.2.3". *)
let version_string = Version.to_string Version.current

(* Full version string including Git branch & commit. *)
let version_full =
  let open Manifest in
  Printf.sprintf "Sail %s (%s @ %s)" version_string branch commit

let usage_msg = "Sail " ^ version_string ^ "\nusage: sail <options> <file1.sail> ... <fileN.sail>\n"

let help options = raise (Arg.Help (Arg.usage_string options usage_msg))

let rec options =
  ref
    [
      ("-o", Arg.String (fun f -> opt_file_out := Some f), "<prefix> select output filename prefix");
      ("-dir", Arg.Set opt_show_sail_dir, " show current Sail library directory");
      ( "-i",
        Arg.Tuple
          [
            Arg.Set Interactive.opt_interactive;
            Arg.Unit (fun () -> Preprocess.add_default_symbol "INTERACTIVE");
            Arg.Set opt_auto_interpreter_rewrites;
          ],
        " start interactive interpreter"
      );
      ( "-is",
        Arg.Tuple
          [
            Arg.Set Interactive.opt_interactive;
            Arg.Unit (fun () -> Preprocess.add_default_symbol "INTERACTIVE");
            Arg.Set opt_auto_interpreter_rewrites;
            Arg.String (fun s -> opt_interactive_script := Some s);
          ],
        "<filename> start interactive interpreter and execute commands in script"
      );
      ( "-iout",
        Arg.String Value.output_redirect,
        "<filename> print interpreter output to file. Can be passed multiple times, see :output_select command."
      );
      ( "-interact_custom",
        Arg.Set Interactive.opt_interactive,
        " drop to an interactive session after running Sail. Differs from -i in that it does not set up the \
         interpreter in the interactive shell."
      );
      ( "-project",
        Arg.String (fun file -> opt_project_files := !opt_project_files @ [file]),
        "<file> sail project file defining module structure"
      );
      ( "-variable",
        Arg.String (fun assignment -> opt_variable_assignments := assignment :: !opt_variable_assignments),
        "<variable=value> assign a module variable to a value"
      );
      ( "-instantiate",
        Arg.String (fun inst -> parse_instantiation inst),
        " <type variable=value> instantiate an abstract type variable"
      );
      ("-all_modules", Arg.Set opt_all_modules, " use all modules in project file");
      ("-list_files", Arg.Unit (fun () -> Frontend.opt_list_files := Some " "), " list files used in all project files");
      ( "-list_files_separated",
        Arg.String (fun sep -> Frontend.opt_list_files := Some sep),
        " list files used in all project files, with a provided separator"
      );
      ("-config", Arg.String (fun file -> opt_model_config_file := Some file), "<file> model configuration file");
      ("-sail_config", Arg.String (fun file -> opt_sail_config_file := Some file), "<file> sail configuration file");
      ( "-output-schema",
        Arg.String (fun file -> opt_output_schema_file := Some file),
        "<file> output configuration schema"
      );
      ("-fmt", Arg.Set opt_format, " format input source code");
      ( "-fmt_backup",
        Arg.String (fun suffix -> opt_format_backup := Some suffix),
        "<suffix> create backups of formatted files as 'file.suffix'"
      );
      ("-fmt_only", Arg.String (fun file -> opt_format_only := file :: !opt_format_only), "<file> format only this file");
      ( "-fmt_emit",
        Arg.String (fun output -> opt_format_emit := output),
        "[file(default)|stdout] update target file or just output to stdout"
      );
      ( "-fmt_skip",
        Arg.String (fun file -> opt_format_skip := file :: !opt_format_skip),
        "<file> skip formatting this file"
      );
      ("-fmt_debug", Arg.Bool (fun debug -> opt_format_debug := debug), "<bool> debug mode");
      ( "-slice_instantiation_types",
        Arg.Tuple [Arg.Set Type_check.opt_no_bitfield_expansion; Arg.Set opt_slice_instantiation_types],
        " (experimental) produce a Sail file containing all of the types that are used in instantiations"
      );
      ( "-D",
        Arg.String (fun symbol -> Preprocess.add_default_symbol symbol),
        "<symbol> define a symbol for the preprocessor, as $define does in the source code"
      );
      ("-no_warn", Arg.Clear Reporting.opt_warnings, " do not print warnings");
      ("-all_warnings", Arg.Set Reporting.opt_all_warnings, " print all warning messages");
      ("-warn_error", Arg.Set opt_warn_error, " promote warnings to errors, if below the required version");
      ( "-strict_var",
        Arg.Tuple [Arg.Unit (fun () -> Preprocess.add_default_symbol "STRICT_VAR"); Arg.Set Type_check.opt_strict_var],
        " require var expressions for variable declarations"
      );
      ( "-strict_bitvector",
        Arg.Tuple
          [
            Arg.Unit (fun () -> Preprocess.add_default_symbol "STRICT_BITVECTOR");
            Arg.Set Initial_check.opt_strict_bitvector;
          ],
        " require bitvectors to be indexed by naturals"
      );
      ( "-strict_exponentials",
        Arg.Tuple
          [
            Arg.Unit (fun () -> Preprocess.add_default_symbol "STRICT_EXPONENTIALS");
            Arg.Set Type_env.opt_strict_exponentials;
          ],
        " type level exponentials must have a non-negative argument"
      );
      ("-plugin", Arg.String (fun plugin -> load_plugin options plugin), "<file> load a Sail plugin");
      ("-just_check", Arg.Set opt_just_check, " terminate immediately after typechecking");
      ("-no_core", Arg.Set opt_no_core, " do not use any core definitions");
      ( "-memo_z3",
        Arg.Set opt_memo_z3,
        " memoize calls to z3, improving performance when typechecking repeatedly (default)"
      );
      ("-no_memo_z3", Arg.Clear opt_memo_z3, " do not memoize calls to z3");
      ( "-memo_z3_path",
        Arg.String (fun f -> opt_memo_z3_path := f),
        "path to cache z3 results (default 'sail_smt_cache')"
      );
      ( "-have_feature",
        Arg.String (fun symbol -> opt_have_feature := Some symbol),
        "<symbol> check if a feature symbol is set by default"
      );
      ("-no_color", Arg.Clear Util.opt_colors, " do not use terminal color codes in output");
      ( "-string_literal_type",
        Arg.Set Type_env.opt_string_literal_type,
        " use a separate string_literal type for string literals"
      );
      ( "-grouped_regstate",
        Arg.Set State.opt_type_grouped_regstate,
        " group registers with same type together in generated register state record"
      );
      (* Casts have been removed, preserved for backwards compatibility *)
      ("-enum_casts", Arg.Unit (fun () -> ()), "");
      ("-non_lexical_flow", Arg.Set Nl_flow.opt_nl_flow, " allow non-lexical flow typing");
      ( "-no_lexp_bounds_check",
        Arg.Set Type_check.opt_no_lexp_bounds_check,
        " turn off bounds checking for vector assignments in l-expressions"
      );
      ("-auto_mono", Arg.Set Rewrites.opt_auto_mono, " automatically infer how to monomorphise code");
      ("-mono_rewrites", Arg.Set Rewrites.opt_mono_rewrites, " turn on rewrites for combining bitvector operations");
      ( "-mono_split",
        Arg.String
          (fun s ->
            let l = String.split_on_char ':' s in
            match l with
            | [fn; var] -> Rewrites.opt_mono_split := (Arg (Ast_util.mk_id fn), var) :: !Rewrites.opt_mono_split
            | [filename; line; var] ->
                Rewrites.opt_mono_split := (Line (filename, int_of_string line), var) :: !Rewrites.opt_mono_split
            | _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable> or <function>:<variable>"))
          ),
        "<filename>:<line>:<variable> manually gives a case split for monomorphisation"
      );
      ( "-splice",
        Arg.String (fun s -> opt_splice := s :: !opt_splice),
        "<filename> add functions from file, replacing existing definitions where necessary"
      );
      ( "-smt_solver",
        Arg.String (fun s -> Constraint.set_solver (String.trim s)),
        "<solver> choose SMT solver. Supported solvers are z3 (default), alt-ergo, cvc4, mathsat, vampire and yices."
      );
      ( "-smt_linearize",
        Arg.Set Type_env.opt_smt_linearize,
        " (experimental) force linearization for constraints involving exponentials"
      );
      ("-Oconstant_fold", Arg.Set Constant_fold.optimize_constant_fold, " apply constant folding optimizations");
      ( "-Oaarch64_fast",
        Arg.Set Jib_compile.optimize_aarch64_fast_struct,
        " apply ARMv8.5 specific optimizations (potentially unsound in general)"
      );
      ("-Ofast_undefined", Arg.Set Initial_check.opt_fast_undefined, " turn on fast-undefined mode");
      ( "-const_prop_mutrec",
        Arg.String
          (fun name ->
            Constant_propagation_mutrec.targets := Ast_util.mk_id name :: !Constant_propagation_mutrec.targets
          ),
        " unroll function in a set of mutually recursive functions"
      );
      ( "-ddump_project_depgraph",
        Arg.String (fun file -> Project.opt_ddump_depgraph := Some file),
        " (debug) dump module dependency graph to a file"
      );
      ("-ddump_project_depgraph_reduced", Arg.Set Project.opt_ddump_depgraph_reduced, " (debug) dump reduced depgraph");
      ( "-ddump_project_depgraph_skip_deps",
        Arg.Set Project.opt_ddump_depgraph_skip_deps,
        " (debug) skip dependencies in depgraph"
      );
      ( "-ddump_project_depgraph_skip_reqs",
        Arg.Set Project.opt_ddump_depgraph_skip_reqs,
        " (debug) skip requires in depgraph"
      );
      ("-ddump_initial_ast", Arg.Set Frontend.opt_ddump_initial_ast, " (debug) dump the initial ast to stdout");
      ("-ddump_tc_ast", Arg.Set Frontend.opt_ddump_tc_ast, " (debug) dump the typechecked ast to stdout");
      ("-ddump_side_effect", Arg.Set Frontend.opt_ddump_side_effect, " (debug) dump side effect info");
      ("-dtc_verbose", Arg.Int Type_check.set_tc_debug, "<verbosity> (debug) verbose typechecker output: 0 is silent");
      ("-dsmt_verbose", Arg.Set Constraint.opt_smt_verbose, " (debug) print SMTLIB constraints sent to SMT solver");
      ( "-dcallgraph",
        Arg.String (fun str -> Callgraph.opt_debug_callgraph := Some str),
        "<file> (debug) dump callgraph to file"
      );
      ("-dallow_internal", Arg.Set Initial_check.opt_allow_internal, " (debug) allow special character # in identifiers");
      ("-dno_error_filenames", Arg.Set Error_format.opt_debug_no_filenames, " (debug) do not print filenames in errors");
      ( "-dprofile",
        Arg.Set Profile.opt_profile,
        " (debug) provide basic profiling information for rewriting passes within Sail"
      );
      ("-dno_cast", Arg.Unit (fun () -> ()), "");
      (* No longer does anything, preserved for backwards compatibility only *)
      ("-dallow_cast", Arg.Unit (fun () -> ()), "");
      ("-unroll_loops", Arg.Set Rewrites.opt_unroll_loops, " turn on rewrites for unrolling loops with constant bounds.");
      ( "-unroll_loops_max_iter",
        Arg.Int (fun n -> Rewrites.opt_unroll_loops_max_iter := n),
        "<nb_iter> Don't unroll loops if they have more than <nb_iter> iterations."
      );
      ( "-ddump_rewrite_ast",
        Arg.String
          (fun l ->
            Rewrites.opt_ddump_rewrite_ast := Some (l, 0);
            Specialize.opt_ddump_spec_ast := Some (l, 0)
          ),
        "<prefix> (debug) dump the ast after each rewriting step to <prefix>_<i>.lem"
      );
      ( "-dmono_all_split_errors",
        Arg.Set Rewrites.opt_dall_split_errors,
        " (debug) display all case split errors from monomorphisation, rather than one"
      );
      ( "-dmono_analysis",
        Arg.Set_int Rewrites.opt_dmono_analysis,
        "<verbosity> (debug) dump information about monomorphisation analysis: 0 silent, 3 max"
      );
      ("-dmono_continue", Arg.Set Rewrites.opt_dmono_continue, " (debug) continue despite monomorphisation errors");
      ("-dmono_limit", Arg.Set_int Monomorphise.opt_size_set_limit, " (debug) adjust maximum size of split allowed");
      ("-dpattern_warning_no_literals", Arg.Set Pattern_completeness.opt_debug_no_literals, "");
      ("-dsequential", Arg.Set Parmap.opt_sequential, " (debug) Run without any internal parallelism");
      ( "-dbacktrace",
        Arg.Int (fun l -> Reporting.opt_backtrace_length := l),
        "<length> (debug) length of backtrace to show when reporting unreachable code"
      );
      ("-just_parse_project", Arg.Set opt_just_parse_project, "");
      ( "-infer_effects",
        Arg.Unit (fun () -> Reporting.simple_warn Version.v0_20_2 "-infer_effects option is deprecated"),
        " (deprecated) ignored for compatibility with older versions; effects are always inferred now"
      );
      ( "-undefined_gen",
        Arg.Unit (fun () -> ()),
        " (deprecated) ignored as undefined generation is now always the same for all Sail backends"
      );
      ("-v", Arg.Set opt_print_version, " print version");
      ("-version", Arg.Set opt_print_version, " print version");
      ( "-require_version",
        Arg.String (fun ver -> opt_require_version := Some ver),
        "<min_version> exit with non-zero status if Sail version requirement is not met"
      );
      ("-verbose", Arg.Int (fun verbosity -> Util.opt_verbosity := verbosity), "<verbosity> produce verbose output");
      ( "-explain_all_variables",
        Arg.Set Type_error.opt_explain_all_variables,
        " explain all type variables in type error messages"
      );
      ("-explain_constraints", Arg.Set Type_error.opt_explain_constraints, " explain constraints in type error messages");
      ( "-explain_all_overloads",
        Arg.Set Type_error.opt_explain_all_overloads,
        " explain all possible overloading failures in type errors"
      );
      ( "-explain_verbose",
        Arg.Tuple [Arg.Set Type_error.opt_explain_all_variables; Arg.Set Type_error.opt_explain_constraints],
        " add the maximum amount of explanation to type errors"
      );
      ("-h", Arg.Unit (fun () -> help !options), " display this list of options. Also available as -help or --help");
      ("-help", Arg.Unit (fun () -> help !options), " display this list of options");
      ("--help", Arg.Unit (fun () -> help !options), " display this list of options");
    ]

let register_default_target () =
  Target.register ~name:"default" ~supports_abstract_types:true ~supports_runtime_config:true Target.empty_action

let parse_json_config_file file =
  if Sys.file_exists file then (
    let json =
      try Yojson.Safe.from_file ~fname:file ~lnum:0 file
      with Yojson.Json_error message ->
        raise
          (Reporting.err_general Parse_ast.Unknown (Printf.sprintf "Failed to parse configuration file:\n%s" message))
    in
    json
  )
  else raise (Reporting.err_general Parse_ast.Unknown (Printf.sprintf "Configuration file %s does not exist" file))

let get_model_config () =
  match !opt_model_config_file with Some file -> parse_json_config_file file | None -> `Assoc []

let run_sail (config : Yojson.Safe.t option) tgt =
  Target.run_pre_parse_hook tgt ();

  let project_files, frees =
    List.partition (fun free -> Filename.check_suffix free ".sail_project") !opt_free_arguments
  in

  let symbols, ctx, ast, env, effect_info =
    match (project_files, !opt_project_files) with
    | [], [] ->
        (* If there are no provided project files, we concatenate all
           the free file arguments into one big blob like before *)
        Frontend.load_files ~no_core:!opt_no_core ~target:tgt ~default_sail_dir:Locations.sail_dir !options
          Type_check.initial_env frees
    (* Allows project files from either free arguments via suffix, or
       from -project, but not both as the ordering between them would
       be unclear. *)
    | project_files, [] | [], project_files ->
        let variables = ref Util.StringMap.empty in
        List.iter
          (fun assignment ->
            if not (Project.parse_assignment ~variables assignment) then
              raise (Reporting.err_general Parse_ast.Unknown ("Could not parse assignment " ^ assignment))
          )
          !opt_variable_assignments;
        let modules = if !opt_all_modules then None else Some frees in
        Frontend.load_project ~no_core:!opt_no_core ~target:tgt ?modules ~options:!options ~variables
          ~just_parse:!opt_just_parse_project ~default_sail_dir:Locations.sail_dir project_files
    | _, _ ->
        raise
          (Reporting.err_general Parse_ast.Unknown
             "Module files (.sail_project) should either be specified with the appropriate option, or as free \
              arguments with the appropriate extension, but not both!"
          )
  in
  let config_json = get_model_config () in
  let ast, instantiation = Frontend.instantiate_abstract_types (Some tgt) config_json !opt_instantiations ast in
  let schema, ast = Config.rewrite_ast tgt env instantiation config_json ast in
  let ast, env = if Target.skip_initial_rewrite tgt then (ast, env) else Frontend.initial_rewrite effect_info env ast in
  let ast, env =
    match !opt_splice with
    | [] -> (ast, env)
    | files -> Splice.splice_files ctx ast (List.rev_map Sail_file.Path.actual files)
  in
  let effect_info = Effects.infer_side_effects (Target.asserts_termination tgt) ast in

  ( match !opt_output_schema_file with
  | None -> ()
  | Some file ->
      let out = Util.open_output_with_check file in
      Yojson.Safe.pretty_to_channel ~std:true out.channel schema;
      Util.close_output_with_check out
  );

  (* Don't show warnings during re-writing for now *)
  Reporting.suppressed_warning_info ();
  Reporting.opt_warnings := false;

  Target.run_pre_rewrites_hook tgt ast effect_info env;
  let ctx, ast, effect_info, env = Rewrites.rewrite ctx effect_info env (Target.rewrites tgt) ast in

  Target.action tgt !opt_file_out
    { symbols; ctx; ast; effect_info; env; options = !options; default_sail_dir = Locations.sail_dir; config };

  (symbols, ctx, ast, env, effect_info)

let run_sail_format (config : Yojson.Safe.t option) =
  let is_format_file f =
    match !opt_format_only with [] -> true | files -> List.exists (fun f' -> Sail_file.Path.to_string f = f') files
  in
  let is_skipped_file f =
    match !opt_format_skip with [] -> false | files -> List.exists (fun f' -> Sail_file.Path.to_string f = f') files
  in
  let module Config = struct
    let config =
      match config with
      | Some (`Assoc keys) ->
          List.assoc_opt "fmt" keys |> Option.map Format_sail.config_from_json
          |> Option.value ~default:Format_sail.default_config
      | Some _ -> raise (Reporting.err_general Parse_ast.Unknown "Invalid configuration file (must be a json object)")
      | None -> Format_sail.default_config
  end in
  let module Formatter = Format_sail.Make (Config) in
  let project_files, files =
    List.partition (fun free -> Filename.check_suffix free ".sail_project") !opt_free_arguments
  in

  (* Get all the files references by project files *)
  let referenced_files =
    List.map
      (fun project_file ->
        let root_directory = Filename.dirname project_file in
        let defs = Project.mk_root root_directory :: Initial_check.parse_project (Sail_file.Path.actual project_file) in

        let variables = ref Util.StringMap.empty in
        List.iter
          (fun assignment ->
            if not (Project.parse_assignment ~variables assignment) then
              raise (Reporting.err_general Parse_ast.Unknown ("Could not parse assignment " ^ assignment))
          )
          !opt_variable_assignments;
        let proj = Project.initialize_project_structure ~variables defs in
        Project.all_files proj
      )
      project_files
    |> List.concat |> List.map fst
  in

  let parsed_files =
    List.map (fun f -> (f, Initial_check.parse_file f)) (List.map Sail_file.Path.actual files @ referenced_files)
  in
  List.iter
    (fun (f, (comments, parse_ast)) ->
      let source = Sail_file.contents (Sail_file.open_file f) in
      if is_format_file f && not (is_skipped_file f) then (
        let formatted =
          Formatter.format_defs ~debug:!opt_format_debug (Sail_file.Path.to_string f) source comments parse_ast
        in
        ( match !opt_format_backup with
        | Some suffix ->
            let out_chan = open_out (Sail_file.Path.to_string f ^ "." ^ suffix) in
            output_string out_chan source;
            close_out out_chan
        | None -> ()
        );
        match !opt_format_emit with
        | "file" ->
            let file_info = Util.open_output_with_check (Sail_file.Path.to_string f) in
            output_string file_info.channel formatted;
            Util.close_output_with_check file_info
        | "stdout" ->
            output_string stdout formatted;
            flush stdout
        | _ -> raise (Failure "unknown format_emit option")
      )
    )
    parsed_files

let feature_check () =
  match !opt_have_feature with
  | None -> ()
  | Some symbol -> if Preprocess.have_symbol symbol (Preprocess.get_default_symbols ()) then exit 0 else exit 2

let get_plugin_dir () =
  match Sys.getenv_opt "SAIL_PLUGIN_DIR" with
  | Some path -> path :: Libsail_sites.Sites.plugins
  | None -> Libsail_sites.Sites.plugins

let rec find_file_above ?prev_inode_opt dir file =
  try
    let inode = (Unix.stat dir).st_ino in
    if Option.fold ~none:true ~some:(( <> ) inode) prev_inode_opt then (
      let filepath = Filename.concat dir file in
      if Sys.file_exists filepath then Some filepath
      else find_file_above ~prev_inode_opt:inode (dir ^ Filename.dir_sep ^ Filename.parent_dir_name) file
    )
    else None
  with Unix.Unix_error _ -> None

let get_implicit_config_file override_file =
  let check_exists file =
    if Sys.file_exists file then Some file
    else (
      Reporting.warn Version.v0_20_2 "" Parse_ast.Unknown (Printf.sprintf "Configuration file %s does not exist" file);
      None
    )
  in
  match override_file with
  | Some file -> check_exists file
  | None -> (
      match Sys.getenv_opt "SAIL_CONFIG" with
      | Some file -> check_exists file
      | None -> find_file_above (Sys.getcwd ()) "sail_config.json"
    )

let main () =
  (* let _ = Memtrace.start_tracing ~context:None ~sampling_rate:1e-6 ~filename:"trace.ctf" in *)
  if Option.is_some (Sys.getenv_opt "SAIL_NEW_CLI") then opt_new_cli := true;

  options := Arg.align (fix_options !options);

  let plugin_extension = if is_bytecode then ".cma" else ".cmxs" in
  ( match Sys.getenv_opt "SAIL_NO_PLUGINS" with
  | Some _ -> ()
  | None -> (
      match get_plugin_dir () with
      | dir :: _ ->
          List.iter
            (fun plugin ->
              let path = Filename.concat dir plugin in
              if Filename.extension plugin = plugin_extension then load_plugin options path
            )
            (Array.to_list (Sys.readdir dir))
      | [] -> ()
    )
  );

  let argv = Sail_file.sail_argv () in
  ( try Arg.parse_argv_dynamic argv options (fun s -> opt_free_arguments := !opt_free_arguments @ [s]) usage_msg with
  | Arg.Bad _ ->
      prerr_endline usage_msg;
      prerr_endline "Use 'sail --help' for a list of available arguments.";
      exit 1
  | Arg.Help msg ->
      prerr_endline msg;
      exit 0
  );

  let config = Option.map parse_json_config_file (get_implicit_config_file !opt_sail_config_file) in

  feature_check ();

  ( match !opt_require_version with
  | Some required_version ->
      let required_version_parsed =
        match Version.parse required_version with
        | Some v -> v
        | None -> raise (Reporting.err_general Unknown ("Couldn't parse required version '" ^ required_version ^ "'"))
      in
      if not (Version.check ~required:required_version_parsed ()) then (
        Printf.eprintf "Sail version %s is older than requested version %s" version_string required_version;
        exit 1
      );
      if !opt_warn_error then Reporting.opt_warn_error := Some required_version_parsed
  | None -> ()
  );

  if !opt_print_version then (
    print_endline version_full;
    exit 0
  );

  if !opt_show_sail_dir then (
    print_endline (Reporting.get_sail_dir Locations.sail_dir);
    exit 0
  );

  if !opt_format then (
    run_sail_format config;
    exit 0
  );

  let default_target = register_default_target () in

  if !opt_memo_z3 then Constraint.load_digests !opt_memo_z3_path;

  let symbols, ctx, ast, env, effect_info =
    match Target.get_the_target () with
    | Some target when not !opt_just_check -> run_sail config target
    | _ -> run_sail config default_target
  in

  if !opt_memo_z3 then Constraint.save_digests !opt_memo_z3_path;

  if !opt_slice_instantiation_types then (
    let sail_dir = Reporting.get_sail_dir Locations.sail_dir in
    let ast = Callgraph.slice_instantiation_types sail_dir ast in
    let filename = Option.value ~default:"out.sail" !opt_file_out in
    let chan = open_out filename in
    Pretty_print_sail.output_ast chan (Type_check.strip_ast ast);
    close_out chan
  );

  if !Interactive.opt_interactive then (
    let script =
      match !opt_interactive_script with
      | None -> []
      | Some file -> (
          let chan = open_in file in
          let lines = ref [] in
          try
            while true do
              let line = input_line chan in
              lines := line :: !lines
            done;
            []
          with End_of_file -> List.rev !lines
        )
    in
    Repl.start_repl ~commands:script ~auto_rewrites:!opt_auto_interpreter_rewrites ~config ~options:!options ~symbols
      ctx env effect_info ast
  )

let () =
  try
    try Parmap.toplevel_handler main with
    | Sys_error s -> raise (Reporting.err_general Parse_ast.Unknown s)
    | Failure s -> raise (Reporting.err_general Parse_ast.Unknown s)
  with Reporting.Fatal_error e ->
    Reporting.print_error e;
    if !opt_memo_z3 then Constraint.save_digests !opt_memo_z3_path else ();
    exit 1