From 990210f37c534a2b3bb91b937e5bd6c800e21cbd Mon Sep 17 00:00:00 2001 From: ploc <ploc@garoche.net> Date: Tue, 16 May 2017 16:57:34 +0200 Subject: [PATCH] Improved include folders behaviors: - allow multiple -I dir, will be used in order (first one declared is first used) - when declaring a global library #open <foo>, foo is first checked in local folders, than in global one (install path). This does not apply to local libraries opened with #open "foo". --- src/backends/C/c_backend_header.ml | 4 +- src/backends/C/c_backend_main.ml | 2 +- src/backends/Horn/horn_backend.ml | 2 +- src/compiler_common.ml | 8 +++- src/corelang.ml | 2 +- src/lusic.ml | 22 +++++------ src/machine_code.ml | 2 +- src/main_lustre_compiler.ml | 2 +- src/main_lustre_testgen.ml | 2 +- src/modules.ml | 9 ++--- src/options.ml | 60 ++++++++++++++++++++++++++---- src/utils.ml | 6 --- 12 files changed, 82 insertions(+), 39 deletions(-) diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml index 2f26e687..e9f8fcda 100644 --- a/src/backends/C/c_backend_header.ml +++ b/src/backends/C/c_backend_header.ml @@ -40,9 +40,9 @@ let print_import_standard fmt = fprintf fmt "#include <mpfr.h>@." end; if !Options.cpp then - fprintf fmt "#include \"%s/arrow.hpp\"@.@." !Options.include_dir + fprintf fmt "#include \"%s/arrow.hpp\"@.@." arrow_top_decl.top_decl_owner else - fprintf fmt "#include \"%s/arrow.h\"@.@." !Options.include_dir + fprintf fmt "#include \"%s/arrow.h\"@.@." arrow_top_decl.top_decl_owner end diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml index 340618c9..7fd49d41 100644 --- a/src/backends/C/c_backend_main.ml +++ b/src/backends/C/c_backend_main.ml @@ -178,7 +178,7 @@ let print_main_code fmt basename m = let print_main_header fmt = fprintf fmt (if !Options.cpp then "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.hpp\"@." else "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@.") - !Options.include_dir + (Options.core_dependency "io_frontend") let print_main_c main_fmt main_machine basename prog machines _ (*dependencies*) = print_main_header main_fmt; diff --git a/src/backends/Horn/horn_backend.ml b/src/backends/Horn/horn_backend.ml index cd2bfe8b..2ad664dd 100644 --- a/src/backends/Horn/horn_backend.ml +++ b/src/backends/Horn/horn_backend.ml @@ -85,7 +85,7 @@ let print_dep fmt prog = List.iter (fun dep -> let (local, s) = Corelang.dependency_of_top dep in - let basename = ((if local then !Options.dest_dir else !Options.include_dir)) ^ s ^ ".smt2" in + let basename = (Options.name_dependency (local, s)) ^ ".smt2" in Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename); let horn = load_file basename in fprintf fmt "@.%s@." horn; diff --git a/src/compiler_common.ml b/src/compiler_common.ml index 637fda84..688b2724 100644 --- a/src/compiler_common.ml +++ b/src/compiler_common.ml @@ -232,7 +232,7 @@ let import_dependencies prog = List.fold_left (fun (compilation_dep, type_env, clock_env) dep -> let (local, s) = Corelang.dependency_of_top dep in - let basename = Modules.name_dependency (local, s) in + let basename = Options.name_dependency (local, s) in Log.report ~level:1 (fun fmt -> Format.fprintf fmt " Library %s@ " basename); let lusic = Modules.import_dependency dep.top_decl_loc (local, s) in (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "");*) @@ -249,4 +249,10 @@ let import_dependencies prog = deps end +let track_exception () = + if !Options.track_exceptions + then (Printexc.print_backtrace stdout; flush stdout) + else () + + diff --git a/src/corelang.ml b/src/corelang.ml index 324a97d5..af764c71 100755 --- a/src/corelang.ml +++ b/src/corelang.ml @@ -241,7 +241,7 @@ let is_imported_node td = (* alias and type definition table *) -let mktop = mktop_decl Location.dummy_loc !Options.include_dir false +let mktop = mktop_decl Location.dummy_loc !Options.dest_dir false let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int}) let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool}) diff --git a/src/lusic.ml b/src/lusic.ml index 76ed1611..72506aec 100644 --- a/src/lusic.ml +++ b/src/lusic.ml @@ -31,17 +31,17 @@ module Header = C_backend_header.Main (HeaderMod) (* extracts a header from a program representing module owner = dirname/basename *) let extract_header dirname basename prog = let owner = dirname ^ "/" ^ basename in - List.fold_right - (fun decl header -> - (*Format.eprintf "Lusic.extract_header: header = %B, owner = %s, decl_owner = %s@." decl.top_decl_itf owner decl.top_decl_owner;*) - if decl.top_decl_itf || decl.top_decl_owner <> owner then header else - match decl.top_decl_desc with - | Node nd -> { decl with top_decl_desc = ImportedNode (Corelang.get_node_interface nd) } :: header - | ImportedNode _ -> header - | Const _ - | TypeDef _ - | Open _ -> decl :: header) - prog [] + List.fold_right + (fun decl header -> + (*Format.eprintf "Lusic.extract_header: header = %B, owner = %s, decl_owner = %s@." decl.top_decl_itf owner decl.top_decl_owner;*) + if decl.top_decl_itf || decl.top_decl_owner <> owner then header else + match decl.top_decl_desc with + | Node nd -> { decl with top_decl_desc = ImportedNode (Corelang.get_node_interface nd) } :: header + | ImportedNode _ -> header + | Const _ + | TypeDef _ + | Open _ -> decl :: header) + prog [] let check_obsolete lusic basename = if lusic.obsolete then raise (Error (Location.dummy_loc, Wrong_number basename)) diff --git a/src/machine_code.ml b/src/machine_code.ml index 68095ca0..93aabec8 100644 --- a/src/machine_code.ml +++ b/src/machine_code.ml @@ -181,7 +181,7 @@ let arrow_desc = let arrow_top_decl = { top_decl_desc = Node arrow_desc; - top_decl_owner = !Options.include_dir; + top_decl_owner = (Options.core_dependency "arrow"); top_decl_itf = false; top_decl_loc = Location.dummy_loc } diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml index d88bc288..f2824c1e 100644 --- a/src/main_lustre_compiler.ml +++ b/src/main_lustre_compiler.ml @@ -473,7 +473,7 @@ let _ = | Corelang.Error _ (*| Task_set.Error _*) | Causality.Error _ -> exit 1 | Sys_error msg -> (eprintf "Failure: %s@." msg) - | exc -> (Utils.track_exception (); raise exc) + | exc -> (track_exception (); raise exc) (* Local Variables: *) (* compile-command:"make -C .." *) diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml index 44603557..6979999a 100644 --- a/src/main_lustre_testgen.ml +++ b/src/main_lustre_testgen.ml @@ -172,7 +172,7 @@ let _ = | Corelang.Error _ (*| Task_set.Error _*) | Causality.Error _ -> exit 1 | Sys_error msg -> (eprintf "Failure: %s@." msg) - | exc -> (Utils.track_exception (); raise exc) + | exc -> (track_exception (); raise exc) (* Local Variables: *) (* compile-command:"make -C .." *) diff --git a/src/modules.ml b/src/modules.ml index 28fe5e6a..4928fd38 100644 --- a/src/modules.ml +++ b/src/modules.ml @@ -113,11 +113,8 @@ let add_const itf name value = | _ -> assert false with Not_found -> Hashtbl.add consts_table name value -let name_dependency (local, dep) = - ((if local then !Options.dest_dir else !Options.include_dir) ^ "/") ^ dep - let import_dependency_aux loc (local, dep) = - let basename = name_dependency (local, dep) in + let basename = Options.name_dependency (local, dep) in let extension = ".lusic" in try let lusic = Lusic.read_lusic basename extension in @@ -161,7 +158,7 @@ let rec load_header_rec imported header = | Const c -> (add_const true c.const_id decl; imported) | TypeDef tdef -> (add_type true tdef.tydef_id decl; imported) | Open (local, dep) -> - let basename = name_dependency (local, dep) in + let basename = Options.name_dependency (local, dep) in if ISet.mem basename imported then imported else let lusic = import_dependency_aux decl.top_decl_loc (local, dep) in load_header_rec (ISet.add basename imported) lusic.Lusic.contents @@ -186,7 +183,7 @@ let rec load_program_rec imported program = | Const c -> (add_const false c.const_id decl; imported) | TypeDef tdef -> (add_type false tdef.tydef_id decl; imported) | Open (local, dep) -> - let basename = name_dependency (local, dep) in + let basename = Options.name_dependency (local, dep) in if ISet.mem basename imported then imported else let lusic = import_dependency_aux decl.top_decl_loc (local, dep) in load_header_rec (ISet.add basename imported) lusic.Lusic.contents diff --git a/src/options.ml b/src/options.ml index ebc1cb7e..29dd8583 100755 --- a/src/options.ml +++ b/src/options.ml @@ -11,18 +11,19 @@ let version = Version.number let codename = Version.codename -let include_dir = ref "." -let include_path = -if (!include_dir != ".") then Version.prefix ^ !include_dir -else Version.include_path +let include_dirs = ref ["."] +(* let include_path = *) +(* if (!include_dir <> ".") then Version.prefix ^ !include_dir *) +(* else Version.include_path *) let print_version () = Format.printf "Lustrec compiler, version %s (%s)@." version codename; - Format.printf "Include directory: %s@." include_path; - Format.printf "User selected include directory: %s@." !include_dir + Format.printf "Standard lib: %s@." Version.include_path; + Format.printf "User provided include directory: @[<h>%a@]@." + (Utils.fprintf_list ~sep:"@ " Format.pp_print_string) !include_dirs let main_node = ref "" let static_mem = ref true @@ -61,6 +62,51 @@ let nb_mutants = ref 1000 let gen_mcdc = ref false let no_mutation_suffix = ref false +let add_include_dir dir = + let removed_slash_suffix = + let len = String.length dir in + if dir.[len-1] = '/' then + String.sub dir 0 (len - 1) + else + dir + in + include_dirs := removed_slash_suffix :: !include_dirs + + +(** Solving the path of required library: + If local: look in the folders described in !Options.include_dirs + If non local: look first as a local, then in Version.include_path: + ie. in Version.include_path::!Options.include_dirs + Note that in options.ml, include folder are added as heads. One need to + perform a fold_right to respect the order +*) +let search_lib_path (local, full_file_name) = + let paths = (if local then !include_dirs else Version.include_path::!include_dirs) in + let name = + List.fold_right (fun dir res -> + match res with Some _ -> res + | None -> + let path_to_lib = dir ^ "/" ^ full_file_name in + if Sys.file_exists path_to_lib then + Some dir + else + None + ) + paths + None + in + match name with + | None -> Format.eprintf "Unable to find library %s in paths %a@.@?" full_file_name (Utils.fprintf_list ~sep:", " Format.pp_print_string) paths;raise Not_found + | Some s -> s + +(* Search for path of core libs (without lusic: arrow and io_frontend *) +let core_dependency lib_name = + search_lib_path (false, lib_name ^ ".h") + +let name_dependency (local, dep) = + let dir = search_lib_path (false, dep ^ ".lusic") in + dir ^ "/" ^ dep + let set_mpfr prec = if prec > 0 then ( mpfr := true; @@ -72,7 +118,7 @@ let set_mpfr prec = let common_options = [ "-d", Arg.Set_string dest_dir, "uses the specified \x1b[4mdirectory\x1b[0m as root for generated/imported object and C files <default: .>"; - "-I", Arg.Set_string include_dir, "sets include \x1b[4mdirectory\x1b[0m"; + "-I", Arg.String add_include_dir, "sets include \x1b[4mdirectory\x1b[0m"; "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node"; "-print-types", Arg.Set print_types, "prints node types"; "-print-clocks", Arg.Set print_clocks, "prints node clocks"; diff --git a/src/utils.ml b/src/utils.ml index 849df152..c5a33c45 100755 --- a/src/utils.ml +++ b/src/utils.ml @@ -347,12 +347,6 @@ let var_id_cpt = ref 0 let get_new_id () = incr var_id_cpt;!var_id_cpt -let track_exception () = - if !Options.track_exceptions - then (Printexc.print_backtrace stdout; flush stdout) - else () - - (* for lexing purposes *) (* Update line number for location info *) -- GitLab