diff --git a/sledge/.gitignore b/sledge/.gitignore index d878b83d7..d89a6cdba 100644 --- a/sledge/.gitignore +++ b/sledge/.gitignore @@ -3,6 +3,7 @@ /llvm/ /model/dune /src/dune +/src/config/dune /src/import/dune /src/llair/dune /src/symbheap/dune diff --git a/sledge/src/config.ml b/sledge/src/config/config.ml similarity index 92% rename from sledge/src/config.ml rename to sledge/src/config/config.ml index a27e7df85..a349a0add 100644 --- a/sledge/src/config.ml +++ b/sledge/src/config/config.ml @@ -30,6 +30,9 @@ let contents = let find key = Yojson.Basic.Util.(to_string_option (member key contents)) +let find_list key = + Yojson.Basic.Util.(filter_string (to_list (member key contents))) + let find_exn key = match find key with | Some data -> data diff --git a/sledge/src/config.mli b/sledge/src/config/config.mli similarity index 88% rename from sledge/src/config.mli rename to sledge/src/config/config.mli index 6b44087d4..587679da5 100644 --- a/sledge/src/config.mli +++ b/sledge/src/config/config.mli @@ -9,3 +9,4 @@ val find : string -> string option val find_exn : string -> string +val find_list : string -> string list diff --git a/sledge/src/config/dune.in b/sledge/src/config/dune.in new file mode 100644 index 000000000..49195e9d4 --- /dev/null +++ b/sledge/src/config/dune.in @@ -0,0 +1,22 @@ +(* -*- tuareg -*- *) +(* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +let deps = ["import"] + +;; +Jbuild_plugin.V1.send +@@ Format.sprintf + {| +(library + (name config) + (public_name llair.config) + %s + (libraries yojson %s)) +|} + (flags `lib deps) + (libraries deps) diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 72491a141..8018a4340 100644 --- a/sledge/src/control.ml +++ b/sledge/src/control.ml @@ -385,8 +385,9 @@ let exec_block : let harness : Llair.t -> (int -> Work.t) option = fun pgm -> - List.find_map ["__llair_main"; "_Z12__llair_mainv"; "main"] - ~f:(fun name -> Llair.Func.find pgm.functions (Var.program name)) + let entry_points = Config.find_list "entry_points" in + List.find_map entry_points ~f:(fun name -> + Llair.Func.find pgm.functions (Var.program name) ) |> function | Some {entry= {params= []} as block} -> Some diff --git a/sledge/src/dune.in b/sledge/src/dune.in index edac33e36..2287e9a89 100644 --- a/sledge/src/dune.in +++ b/sledge/src/dune.in @@ -6,7 +6,7 @@ * LICENSE file in the root directory of this source tree. *) -let deps = ["import"; "llair_"; "symbheap"] +let deps = ["import"; "llair_"; "symbheap"; "config"] ;; Jbuild_plugin.V1.send @@ -22,7 +22,7 @@ Jbuild_plugin.V1.send (public_name sledge) (package sledge) %s - (libraries shexp.process yojson %s)) + (libraries shexp.process %s)) |} (flags `exe deps) (libraries deps) diff --git a/sledge/src/llair/dune.in b/sledge/src/llair/dune.in index 9b1ec3f8f..f245c3c3f 100644 --- a/sledge/src/llair/dune.in +++ b/sledge/src/llair/dune.in @@ -6,7 +6,7 @@ * LICENSE file in the root directory of this source tree. *) -let deps = ["model"; "import"; "trace"] +let deps = ["model"; "import"; "trace"; "config"] ;; Jbuild_plugin.V1.send diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index 4b52951b7..728e6ab90 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -1323,10 +1323,9 @@ let xlate_function : x -> Llvm.llvalue -> Llair.func = let transform : Llvm.llmodule -> unit = fun llmodule -> let pm = Llvm.PassManager.create () in + let entry_points = Config.find_list "entry_points" in Llvm_ipo.add_internalize_predicate pm (fun fn -> - List.exists - ["__llair_main"; "_Z12__llair_mainv"; "main"] - ~f:(String.equal fn) ) ; + List.exists entry_points ~f:(String.equal fn) ) ; Llvm_ipo.add_global_dce pm ; Llvm_ipo.add_global_optimizer pm ; Llvm_scalar_opts.add_lower_atomic pm ; diff --git a/sledge/src/sledge_buck.ml b/sledge/src/sledge_buck.ml index 7552a7a20..d49d17990 100644 --- a/sledge/src/sledge_buck.ml +++ b/sledge/src/sledge_buck.ml @@ -136,8 +136,10 @@ let llvm_link_opt ~output modules = eval ~context ( run (Lazy.force llvm_bin ^ "llvm-link") - ( "-internalize" :: "-internalize-public-api-list=main" :: "-o=-" - :: modules ) + ( "-internalize" + :: ( "-internalize-public-api-list=" + ^ String.concat ~sep:"," (Config.find_list "entry_points") ) + :: "-o=-" :: modules ) |- run (Lazy.force llvm_bin ^ "opt") ["-o=" ^ output; "-globaldce"; "-globalopt"] )