From a04e3586f90dc8dc56deac10a24169a471b75a1e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Cassiers?= Date: Wed, 5 Feb 2025 01:19:38 +0000 Subject: [PATCH] Add support for the -I parameter to jasmin2ec, jasmin-ct and jasmin2tex. This is now identical to jasminc's parameter, and merged with JASMINPATH. --- compiler/entry/commonCLI.ml | 12 ++++++++++-- compiler/entry/commonCLI.mli | 2 ++ compiler/entry/jasmin2ec.ml | 6 +++--- compiler/entry/jasmin2tex.ml | 6 +++--- compiler/entry/jasmin_ct.ml | 6 +++--- compiler/src/compile.ml | 7 ++----- compiler/src/compile.mli | 1 + compiler/src/glob_options.ml | 5 +++-- compiler/src/main_compiler.ml | 2 +- 9 files changed, 28 insertions(+), 19 deletions(-) diff --git a/compiler/entry/commonCLI.ml b/compiler/entry/commonCLI.ml index a0f9c8a5c..d02686a90 100644 --- a/compiler/entry/commonCLI.ml +++ b/compiler/entry/commonCLI.ml @@ -39,6 +39,14 @@ let call_conv = & opt call_conv Glob_options.Linux & info [ "call-conv"; "cc" ] ~docv:"OS" ~doc) +let idirs = + let doc = + "Bind ident to path for 'from ident require ...'" + in + let info = Arg.info [ "I" ] ~docv:"ident:path" ~doc in + let conv = Arg.pair ~sep:':' Arg.string Arg.dir in + Arg.value (Arg.opt_all conv [] info) + let warn = let doc = "Print warnings" in Arg.(value & flag & info [ "warn" ] ~doc) @@ -65,9 +73,9 @@ let parse_and_compile (type reg regx xreg rflag cond asm_op extra_op) and type rflag = rflag and type cond = cond and type asm_op = asm_op - and type extra_op = extra_op) pass file = + and type extra_op = extra_op) pass file idirs = let _env, pprog, _ast = - try Compile.parse_file Arch.arch_info file with + try Compile.parse_file Arch.arch_info file idirs with | Annot.AnnotationError (loc, code) -> hierror ~loc:(Lone loc) ~kind:"annotation error" "%t" code | Pretyping.TyError (loc, code) -> diff --git a/compiler/entry/commonCLI.mli b/compiler/entry/commonCLI.mli index 3a5091c2c..037ec674e 100644 --- a/compiler/entry/commonCLI.mli +++ b/compiler/entry/commonCLI.mli @@ -4,6 +4,7 @@ open Cmdliner val get_arch_module : Utils.architecture -> Glob_options.call_conv -> (module Arch_full.Arch) val arch : Utils.architecture Term.t val call_conv : Glob_options.call_conv Term.t +val idirs : (string * string) list Term.t val warn : bool Term.t val after_pass : Compiler.compiler_step Term.t @@ -18,6 +19,7 @@ val parse_and_compile : and type xreg = 'xreg) -> Compiler.compiler_step -> string -> + (string * string) list -> ( unit, ( 'reg, 'regx, diff --git a/compiler/entry/jasmin2ec.ml b/compiler/entry/jasmin2ec.ml index 0523d3912..9a3bf7bd5 100644 --- a/compiler/entry/jasmin2ec.ml +++ b/compiler/entry/jasmin2ec.ml @@ -32,11 +32,11 @@ let extract_to_file prog arch pd asmOp model amodel fnames array_dir outfile = -let parse_and_extract arch call_conv = +let parse_and_extract arch call_conv idirs = let module A = (val get_arch_module arch call_conv) in let extract model amodel functions array_dir output pass file = - let prog = parse_and_compile (module A) pass file in + let prog = parse_and_compile (module A) pass file (idirs @ Glob_options.env_idirs) in extract_to_file prog arch A.reg_size A.asmOp model amodel functions array_dir output @@ -122,6 +122,6 @@ let () = in Cmd.v info Term.( - const parse_and_extract $ arch $ call_conv $ model $ array_model + const parse_and_extract $ arch $ call_conv $ idirs $ model $ array_model $ functions $ array_dir $ output $ after_pass $ file $ warn) |> Cmd.eval |> exit diff --git a/compiler/entry/jasmin2tex.ml b/compiler/entry/jasmin2tex.ml index 186f499b3..ebdd6929e 100644 --- a/compiler/entry/jasmin2tex.ml +++ b/compiler/entry/jasmin2tex.ml @@ -3,10 +3,10 @@ open Cmdliner open CommonCLI open Utils -let parse_and_print arch call_conv = +let parse_and_print arch call_conv idirs = let module A = (val get_arch_module arch call_conv) in let parse file = - try Compile.parse_file A.arch_info file with + try Compile.parse_file A.arch_info file (idirs @ Glob_options.env_idirs) with | Annot.AnnotationError (loc, code) -> hierror ~loc:(Lone loc) ~kind:"annotation error" "%t" code | Pretyping.TyError (loc, code) -> @@ -54,6 +54,6 @@ let () = let info = Cmd.info "jasmin2tex" ~version:Glob_options.version_string ~doc ~man in - Cmd.v info Term.(const parse_and_print $ arch $ call_conv $ output $ file + Cmd.v info Term.(const parse_and_print $ arch $ call_conv $ idirs $ output $ file $ warn) |> Cmd.eval |> exit diff --git a/compiler/entry/jasmin_ct.ml b/compiler/entry/jasmin_ct.ml index 22480f517..450b778cc 100644 --- a/compiler/entry/jasmin_ct.ml +++ b/compiler/entry/jasmin_ct.ml @@ -3,10 +3,10 @@ open Cmdliner open CommonCLI open Utils -let parse_and_check arch call_conv = +let parse_and_check arch call_conv idirs = let module A = (val get_arch_module arch call_conv) in let check ~doit infer ct_list speculative pass file = - let prog = parse_and_compile (module A) pass file in + let prog = parse_and_compile (module A) pass file (idirs @ Glob_options.env_idirs) in if speculative then let prog = @@ -88,6 +88,6 @@ let () = in Cmd.v info Term.( - const parse_and_check $ arch $ call_conv $ infer $ slice $ speculative + const parse_and_check $ arch $ call_conv $ idirs $ infer $ slice $ speculative $ after_pass $ file $ doit $ warn) |> Cmd.eval |> exit diff --git a/compiler/src/compile.ml b/compiler/src/compile.ml index eb98c1ef3..9cb7ff4b0 100644 --- a/compiler/src/compile.ml +++ b/compiler/src/compile.ml @@ -11,11 +11,8 @@ let preprocess reg_size asmOp p = (* -------------------------------------------------------------------- *) -let parse_file arch_info fname = - let env = - List.fold_left Pretyping.Env.add_from Pretyping.Env.empty - !Glob_options.idirs - in +let parse_file arch_info fname idirs = + let env = List.fold_left Pretyping.Env.add_from Pretyping.Env.empty idirs in Pretyping.tt_program arch_info env fname (* -------------------------------------------------------------------- *) diff --git a/compiler/src/compile.mli b/compiler/src/compile.mli index 0c1c3ef5c..41fb9bd1f 100644 --- a/compiler/src/compile.mli +++ b/compiler/src/compile.mli @@ -15,6 +15,7 @@ val preprocess : wsize -> 'asm asmOp -> (unit, 'asm) pprog -> (unit, 'asm) prog val parse_file : ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Pretyping.arch_info -> string -> + (string * string) list -> ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Arch_extra.extended_op Pretyping.Env.env * ( unit, diff --git a/compiler/src/glob_options.ml b/compiler/src/glob_options.ml index 3227b1079..206065217 100644 --- a/compiler/src/glob_options.ml +++ b/compiler/src/glob_options.ml @@ -99,8 +99,9 @@ let set_color c = let parse_jasmin_path s = s |> String.split_on_char ':' |> List.map (String.split ~by:"=") -let idirs = - ref (try "JASMINPATH" |> Sys.getenv |> parse_jasmin_path with _ -> []) +let env_idirs = try "JASMINPATH" |> Sys.getenv |> parse_jasmin_path with _ -> [] + +let idirs = ref (env_idirs) let set_idirs s = match String.split_on_char ':' s with diff --git a/compiler/src/main_compiler.ml b/compiler/src/main_compiler.ml index 1262dfe6b..35713ffff 100644 --- a/compiler/src/main_compiler.ml +++ b/compiler/src/main_compiler.ml @@ -114,7 +114,7 @@ let main () = | None -> () in let env, pprog, _ast = - try Compile.parse_file Arch.arch_info infile + try Compile.parse_file Arch.arch_info infile !Glob_options.idirs with | Annot.AnnotationError (loc, code) -> hierror ~loc:(Lone loc) ~kind:"annotation error" "%t" code | Pretyping.TyError (loc, code) -> hierror ~loc:(Lone loc) ~kind:"typing error" "%a" Pretyping.pp_tyerror code