From e1d4aad487b296f4885b77348ed6dc193fbc9c4e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 12 Oct 2018 08:10:14 -0700 Subject: [PATCH] [ocamlformat] upgrade ocamlformat to 0.8 Reviewed By: mbouaziz Differential Revision: D10359577 fbshipit-source-id: e7f5286e3 --- .ocamlformat | 3 ++- .ocamlformat.hash | 2 +- Makefile | 4 ++- infer/src/IR/HilExp.ml | 1 + infer/src/base/Config.ml | 6 ++--- infer/src/base/Die.mli | 7 ++--- infer/src/base/RunState.ml | 4 +-- infer/src/biabduction/Rearrange.mli | 5 ++-- infer/src/checkers/control.ml | 1 + infer/src/checkers/dominators.ml | 1 + infer/src/checkers/uninitDomain.ml | 3 ++- infer/src/clang/Capture.ml | 3 ++- infer/src/clang/ClangWrapper.ml | 4 +-- infer/src/clang/cTL.ml | 10 +++++++ infer/src/clang/cType_to_sil_type.ml | 6 +++++ infer/src/clang/clang_ast_extend.ml | 2 ++ infer/src/clang/tableaux.ml | 8 +++--- infer/src/concurrency/RacerD.ml | 7 ++--- infer/src/concurrency/RacerDDomain.ml | 4 +-- infer/src/unit/TaintTests.ml | 6 ++--- sledge/src/config.ml | 5 ++++ sledge/src/import/import.ml | 6 +++++ sledge/src/llair/exp.ml | 23 ++++++++++++++++ sledge/src/llair/frontend.ml | 38 +++++++++++++++++++++++++++ sledge/src/llair/llair.ml | 24 +++++++++++++++++ sledge/src/llair/loc.ml | 1 + sledge/src/llair/typ.ml | 9 +++++++ sledge/src/ppx_trace/ppx_trace.ml | 3 +++ sledge/src/sledge.ml | 1 + sledge/src/trace/trace.ml | 4 +++ 30 files changed, 171 insertions(+), 30 deletions(-) diff --git a/.ocamlformat b/.ocamlformat index 4609ccff9..e4b3bac91 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,3 +1,4 @@ +let-binding-spacing = sparse break-cases = nested margin = 100 -version = 0.7 +version = 0.8 diff --git a/.ocamlformat.hash b/.ocamlformat.hash index 93746c860..b82d648e7 100644 --- a/.ocamlformat.hash +++ b/.ocamlformat.hash @@ -1 +1 @@ -b3ed72b3997cb7712e54f90d47128d6dd8e18f53 +e2cf2fd21fdc2f79840ddf994403a0c2469b6bfd diff --git a/Makefile b/Makefile index 3ca3aa31a..e1b6ed822 100644 --- a/Makefile +++ b/Makefile @@ -684,7 +684,7 @@ endif # This is a magical version number that doesn't reinstall the world when added on top of what we # have in opam.lock. To upgrade this version number, manually try to install several utop versions # until you find one that doesn't recompile the world. TODO(t20828442): get rid of magic -OPAM_DEV_DEPS = ocamlformat.$$(grep version .ocamlformat | cut -d ' ' -f 3) ocp-indent merlin utop.2.2.0 webbrowser +OPAM_DEV_DEPS = ocp-indent merlin utop.2.2.0 webbrowser ifneq ($(EMACS),no) OPAM_DEV_DEPS += tuareg @@ -697,6 +697,8 @@ devsetup: Makefile.autoconf OPAMSWITCH=$(OPAMSWITCH); $(OPAM) install --yes --no-checksum user-setup $(OPAM_DEV_DEPS)) $(QUIET)echo '$(TERM_INFO)*** Running `opam config setup -a`$(TERM_RESET)' >&2 $(QUIET)OPAMSWITCH=$(OPAMSWITCH); $(OPAM) config --yes setup -a + $(QUIET)$(call silent_on_success,installing ocamlformat,\ + OPAMSWITCH=$(OPAMSWITCH); $(OPAM) pin add --yes ocamlformat.$$(grep version .ocamlformat | cut -d ' ' -f 3) https://github.com/ocaml-ppx/ocamlformat.git#$$(grep version .ocamlformat | cut -d ' ' -f 3)-opam1) $(QUIET)echo '$(TERM_INFO)*** Running `opam user-setup`$(TERM_RESET)' >&2 $(QUIET)OPAMSWITCH=$(OPAMSWITCH); OPAMYES=1; $(OPAM) user-setup install $(QUIET)if [ "$(PLATFORM)" = "Darwin" ] && [ x"$(GNU_SED)" = x"no" ]; then \ diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index 1269b02ee..ff6a38d5f 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -210,6 +210,7 @@ let rec eval_arithmetic_binop op e1 e2 = | _ -> None + and eval = function | Constant c -> Some c diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 3828cbe54..317f8146b 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1187,9 +1187,9 @@ and () = "Do not show reports coming from this type of issue. Each checker can report a range of \ issue types. This option provides fine-grained filtering over which types of issue should \ be reported once the checkers have run. In particular, note that disabling issue types \ - does not make the corresponding checker not run.\n \ - By default, the following issue types are disabled: %s.\n\n \ - See also $(b,--report-issue-type).\n" + does not make the corresponding checker not run.\n\ + \ By default, the following issue types are disabled: %s.\n\n\ + \ See also $(b,--report-issue-type).\n" (String.concat ~sep:", " disabled_issues_ids)) ; mk true ~long:"enable-issue-type" ~deprecated:["enable_checks"; "-enable-checks"] diff --git a/infer/src/base/Die.mli b/infer/src/base/Die.mli index fee443233..9c0703726 100644 --- a/infer/src/base/Die.mli +++ b/infer/src/base/Die.mli @@ -7,9 +7,10 @@ open! IStd -(* WARNING: ONLY USE IF Logging IS NOT AVAILABLE TO YOU FOR SOME REASON (e.g., inside Config). *) - -exception InferExternalError of string +exception + (* WARNING: ONLY USE IF Logging IS NOT AVAILABLE TO YOU FOR SOME REASON (e.g., inside Config). *) + InferExternalError of + string exception InferInternalError of string diff --git a/infer/src/base/RunState.ml b/infer/src/base/RunState.ml index c6b2c168e..8a81e70bd 100644 --- a/infer/src/base/RunState.ml +++ b/infer/src/base/RunState.ml @@ -45,8 +45,8 @@ let load_and_validate () = Error (Printf.sprintf "'%s' already exists but it is not an empty directory and it does not look like an \ - infer results directory:\n \ - %s\n\ + infer results directory:\n\ + \ %s\n\ Was it created using an older version of infer?" Config.results_dir err_msg) ) msg diff --git a/infer/src/biabduction/Rearrange.mli b/infer/src/biabduction/Rearrange.mli index 930a2072b..db123c6f6 100644 --- a/infer/src/biabduction/Rearrange.mli +++ b/infer/src/biabduction/Rearrange.mli @@ -10,9 +10,8 @@ open! IStd (** Re-arrangement and extension of structures with fresh variables *) -(* TODO: this description is not clear *) - -exception ARRAY_ACCESS +exception (* TODO: this description is not clear *) + ARRAY_ACCESS val is_only_pt_by_fld_or_param_nonnull : Procdesc.t -> Tenv.t -> Prop.normal Prop.t -> Exp.t -> bool diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index 1a81e7361..bc3b98ef3 100644 --- a/infer/src/checkers/control.ml +++ b/infer/src/checkers/control.ml @@ -8,6 +8,7 @@ open! IStd module F = Format module L = Logging + (* forward dependency analysis for computing set of variables that affect the looping behavior of the program diff --git a/infer/src/checkers/dominators.ml b/infer/src/checkers/dominators.ml index 62db7afa3..d70965a1f 100644 --- a/infer/src/checkers/dominators.ml +++ b/infer/src/checkers/dominators.ml @@ -8,6 +8,7 @@ open! IStd open Graph module L = Logging module CFG = ProcCfg.Normal + (* Use ocamlgraph's dominators functor to get the dominators *) module GDoms = Dominator.Make (ProcCfg.MakeOcamlGraph (CFG)) diff --git a/infer/src/checkers/uninitDomain.ml b/infer/src/checkers/uninitDomain.ml index 82494b525..714a26653 100644 --- a/infer/src/checkers/uninitDomain.ml +++ b/infer/src/checkers/uninitDomain.ml @@ -148,5 +148,6 @@ module Summary = struct post = set of uninit local variables of the procedure *) type t = Domain.t prepost - let pp fmt {pre; post} = F.fprintf fmt "@\n Pre: %a @\nPost: %a @\n" Domain.pp pre Domain.pp post + let pp fmt {pre; post} = + F.fprintf fmt "@\n Pre: %a @\nPost: %a @\n" Domain.pp pre Domain.pp post end diff --git a/infer/src/clang/Capture.ml b/infer/src/clang/Capture.ml index 22de3ecd5..a92420c5f 100644 --- a/infer/src/clang/Capture.ml +++ b/infer/src/clang/Capture.ml @@ -160,7 +160,8 @@ let cc1_capture clang_cmd = else if Config.skip_analysis_in_path_skips_compilation && CLocation.is_file_blacklisted source_path then ( - L.(debug Capture Quiet) "@\n Skip compilation and analysis of source file %s@\n@\n" source_path ; + L.(debug Capture Quiet) + "@\n Skip compilation and analysis of source file %s@\n@\n" source_path ; () ) else match Config.clang_biniou_file with diff --git a/infer/src/clang/ClangWrapper.ml b/infer/src/clang/ClangWrapper.ml index bbaa70ff0..cb5d8f745 100644 --- a/infer/src/clang/ClangWrapper.ml +++ b/infer/src/clang/ClangWrapper.ml @@ -180,7 +180,7 @@ let exe ~prog ~args = files. *) L.(debug Capture Quiet) "WARNING: `clang -### ` returned an empty set of commands to run and no error. Will \ - run the original command directly:@\n \ - %s@\n" + run the original command directly:@\n\ + \ %s@\n" (String.concat ~sep:" " @@ (prog :: args)) ; Process.create_process_and_wait ~prog ~args ) diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 78bbecd6d..4144337f8 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -1165,6 +1165,7 @@ let rec eval_Atomic pred_name_ args an lcxt = | _ -> L.(die ExternalError) "Undefined Predicate or wrong set of arguments: '%s'" pred_name + and eval_AND an lcxt f1 f2 = match eval_formula f1 an lcxt with | Some witness1 -> ( @@ -1176,6 +1177,7 @@ and eval_AND an lcxt f1 f2 = | None (* we short-circuit the AND evaluation *) -> None + and eval_OR an lcxt f1 f2 = choose_witness_opt (eval_formula f1 an lcxt) (eval_formula f2 an lcxt) and eval_Implies an lcxt f1 f2 = @@ -1183,6 +1185,7 @@ and eval_Implies an lcxt f1 f2 = let witness2 = eval_formula f2 an lcxt in choose_witness_opt witness1 witness2 + (* an, lcxt |= EF phi <=> an, lcxt |= phi or exists an' in Successors(st): an', lcxt |= EF phi @@ -1203,6 +1206,7 @@ and eval_EF phi an lcxt trans = List.fold_left (Ctl_parser_types.get_direct_successor_nodes an) ~init:witness_opt ~f:(fun acc node -> choose_witness_opt (eval_EF phi node lcxt trans) acc ) + (* an, lcxt |= EX phi <=> exists an' in Successors(st): an', lcxt |= phi That is: a (an, lcxt) satifies EX phi if and only if @@ -1227,6 +1231,7 @@ and eval_EX phi an lcxt trans = | _ -> witness_opt + (* an, lcxt |= E(phi1 U phi2) evaluated using the equivalence an, lcxt |= E(phi1 U phi2) <=> an, lcxt |= phi2 or (phi1 and EX(E(phi1 U phi2))) @@ -1237,6 +1242,7 @@ and eval_EU phi1 phi2 an lcxt trans = let f = Or (phi2, And (phi1, EX (trans, EU (trans, phi1, phi2)))) in eval_formula f an lcxt + (* an |= A(phi1 U phi2) evaluated using the equivalence an |= A(phi1 U phi2) <=> an |= phi2 or (phi1 and AX(A(phi1 U phi2))) @@ -1246,6 +1252,7 @@ and eval_AU phi1 phi2 an lcxt trans = let f = Or (phi2, And (phi1, AX (trans, AU (trans, phi1, phi2)))) in eval_formula f an lcxt + (* an, lcxt |= InNode[node_type_list] phi <=> an is a node of type in node_type_list and an satifies phi *) @@ -1263,6 +1270,7 @@ and in_node node_type_list phi an lctx = List.fold_left node_type_list ~init:None ~f:(fun acc node -> choose_witness_opt (holds_for_one_node node) acc ) + (* Intuitive meaning: (an,lcxt) satifies EH[Classes] phi if the node an is among the declaration specified by the list Classes and there exists a super class in its hierarchy whose declaration satisfy phi. @@ -1275,6 +1283,7 @@ and eval_EH classes phi an lcxt = let f = ET (classes, None, EX (Some Super, EF (Some Super, phi))) in eval_formula f an lcxt + (* an, lcxt |= ET[T][->l]phi <=> eventually we reach a node an' such that an' is among the types defined in T and: @@ -1295,6 +1304,7 @@ and eval_ET tl trs phi an lcxt = in eval_formula f an lcxt + (* Formulas are evaluated on a AST node an and a linter context lcxt *) and eval_formula f an lcxt : Ctl_parser_types.ast_node option = debug_eval_begin (debug_create_payload an f lcxt) ; diff --git a/infer/src/clang/cType_to_sil_type.ml b/infer/src/clang/cType_to_sil_type.ml index f17beb048..fdfcb570e 100644 --- a/infer/src/clang/cType_to_sil_type.ml +++ b/infer/src/clang/cType_to_sil_type.ml @@ -98,6 +98,7 @@ let rec build_array_type translate_decl tenv (qual_type : Clang_ast_t.qual_type) let stride = Option.map ~f:IntLit.of_int stride_opt in Typ.Tarray {elt= array_type; length; stride} + and type_desc_of_attr_type translate_decl tenv type_info attr_info = match type_info.Clang_ast_t.ti_desugared_type with | Some type_ptr -> ( @@ -110,6 +111,7 @@ and type_desc_of_attr_type translate_decl tenv type_info attr_info = | None -> Typ.Tvoid + and type_desc_of_c_type translate_decl tenv c_type : Typ.desc = let open Clang_ast_t in match c_type with @@ -167,6 +169,7 @@ and type_desc_of_c_type translate_decl tenv c_type : Typ.desc = | None -> Typ.Tvoid ) + and decl_ptr_to_type_desc translate_decl tenv decl_ptr : Typ.desc = let open Clang_ast_t in let typ = Clang_ast_extend.DeclPtr decl_ptr in @@ -194,6 +197,7 @@ and decl_ptr_to_type_desc translate_decl tenv decl_ptr : Typ.desc = (Clang_ast_j.string_of_pointer decl_ptr) ; Typ.Tvoid ) + and clang_type_ptr_to_type_desc translate_decl tenv type_ptr = try Clang_ast_extend.TypePointerMap.find type_ptr !CFrontend_config.sil_types_map with Caml.Not_found -> ( @@ -205,6 +209,7 @@ and clang_type_ptr_to_type_desc translate_decl tenv type_ptr = | _ -> Typ.Tvoid ) + and type_ptr_to_type_desc translate_decl tenv type_ptr : Typ.desc = match type_ptr with | Clang_ast_types.TypePtr.Ptr _ -> @@ -226,6 +231,7 @@ and type_ptr_to_type_desc translate_decl tenv type_ptr : Typ.desc = | _ -> L.(die InternalError) "unknown variant for type_ptr" + and qual_type_to_sil_type translate_decl tenv qual_type = let desc = type_ptr_to_type_desc translate_decl tenv qual_type.Clang_ast_t.qt_type_ptr in let quals = Typ.mk_type_quals ~is_const:qual_type.Clang_ast_t.qt_is_const () in diff --git a/infer/src/clang/clang_ast_extend.ml b/infer/src/clang/clang_ast_extend.ml index a214bb32c..2e3e17533 100644 --- a/infer/src/clang/clang_ast_extend.ml +++ b/infer/src/clang/clang_ast_extend.ml @@ -6,6 +6,7 @@ *) open! IStd + (* This module adds more variants to some types in AST The implementation extends default one from the facebook-clang-plugins repository *) @@ -88,6 +89,7 @@ module TypePointerOrd = struct L.(die InternalError) "unexpected type_ptr variants: %s, %s" (type_ptr_to_string t1) (type_ptr_to_string t2) + and compare_qual_type (qt1 : Clang_ast_t.qual_type) (qt2 : Clang_ast_t.qual_type) = if phys_equal qt1 qt2 then 0 else diff --git a/infer/src/clang/tableaux.ml b/infer/src/clang/tableaux.ml index be62ba470..ad60d5731 100644 --- a/infer/src/clang/tableaux.ml +++ b/infer/src/clang/tableaux.ml @@ -254,10 +254,10 @@ let add_valid_formulae an checker lcxt cl = add_in_set phi acc_set | AG _ | AX _ | AF _ | AU _ | EH _ | ET _ | Implies _ -> Logging.die InternalError - "@\n \ - We should not have operators AG, AX, AF, AU, EH, ET.\n \ - Failing with formula @\n \ - %a@\n" + "@\n\ + \ We should not have operators AG, AX, AF, AU, EH, ET.\n\ + \ Failing with formula @\n\ + \ %a@\n" CTL.Debug.pp_formula phi | _ -> acc_set diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index ea77f0ebc..f2b00decf 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -742,7 +742,8 @@ let get_reporting_explanation_java report_kind tenv pname thread = if is_thread_safe_method pname tenv then Some (F.asprintf - "@\n Reporting because current method is annotated %a or overrides an annotated method." + "@\n\ + \ Reporting because current method is annotated %a or overrides an annotated method." MF.pp_monospaced "@ThreadSafe") else match FbThreadSafety.get_fbthreadsafe_class_annot pname tenv with @@ -788,8 +789,8 @@ let get_reporting_explanation_java report_kind tenv pname thread = else ( IssueType.thread_safety_violation , F.asprintf - "@\n \ - Reporting because another access to the same memory occurs on a background thread, \ + "@\n\ + \ Reporting because another access to the same memory occurs on a background thread, \ although this access may not." ) diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 141978922..1ea23849d 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -698,8 +698,8 @@ let pp_summary fmt {threads; locks; accesses; return_ownership; return_attribute let pp fmt {threads; locks; accesses; ownership; attribute_map; wobbly_paths} = F.fprintf fmt "Threads: %a, Locks: %a @\n\ - Accesses %a @\n \ - Ownership: %a @\n\ + Accesses %a @\n\ + \ Ownership: %a @\n\ Attributes: %a @\n\ Non-stable Paths: %a@\n" ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 40c3e8c7f..39b3cbd94 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -137,9 +137,9 @@ let tests = ; read_field_to_id "read_id" "base_id" "f" ; var_assign_id "var" "read_id" ; invariant - "{ base_id$0.f* => (SOURCE -> ?),\n \ - ret_id$0* => (SOURCE -> ?),\n \ - var* => (SOURCE -> ?) }" ] ) + "{ base_id$0.f* => (SOURCE -> ?),\n\ + \ ret_id$0* => (SOURCE -> ?),\n\ + \ var* => (SOURCE -> ?) }" ] ) ; ( "source flows to var then cleared" , [ assign_to_source "ret_id" ; var_assign_id "var" "ret_id" diff --git a/sledge/src/config.ml b/sledge/src/config.ml index 888737e05..c4713de9d 100644 --- a/sledge/src/config.ml +++ b/sledge/src/config.ml @@ -39,6 +39,7 @@ end = struct let (Arg (trm, set)) = List.fold_right ~f:pair args ~init in Term.app (Term.const set) trm + let args : arg list ref = ref [] let mk ~default arg = @@ -47,6 +48,7 @@ end = struct args := Arg (arg, set) :: !args ; var + let parse info validate = match Term.eval (Term.(ret (const validate $ tuple !args)), info) with | `Ok () -> () @@ -60,14 +62,17 @@ let input = mk ~default:"" Arg.(required & pos ~rev:true 0 (some string) None & info []) + let output = let default = None in mk ~default Arg.(value & opt (some string) default & info ["o"; "output"]) + let trace_all = let default = false in mk ~default Arg.(value & flag & info ["t"; "trace-all"]) + let info = Term.info "sledge" ~version:Version.version let validate () = `Ok () diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml index 94aefa3ea..88f8bde45 100644 --- a/sledge/src/import/import.ml +++ b/sledge/src/import/import.ml @@ -43,11 +43,13 @@ let option_fmt fmt pp ff = function | Some x -> Format.fprintf ff fmt pp x | None -> () + let rec list_fmt sep pp ff = function | [] -> () | [x] -> pp ff x | x :: xs -> Format.fprintf ff "%a%( %)%a" pp x sep (list_fmt sep pp) xs + let vector_fmt sep pp ff v = list_fmt sep pp ff (Vector.to_list v) let warn fmt = @@ -60,6 +62,7 @@ let warn fmt = Format.pp_force_newline ff () ) ff fmt + let raisef exn fmt = let bt = Caml.Printexc.get_raw_backtrace () in let ff = Format.str_formatter in @@ -72,6 +75,7 @@ let raisef exn fmt = Caml.Printexc.raise_with_backtrace exn bt ) ff fmt + exception Unimplemented of string let todo fmt = raisef (fun msg -> Unimplemented msg) fmt @@ -82,10 +86,12 @@ let assertf cnd fmt = if not cnd then fail fmt else Format.ikfprintf (fun _ () -> ()) Format.str_formatter fmt + let checkf cnd fmt = if not cnd then fail fmt else Format.ikfprintf (fun _ () -> true) Format.str_formatter fmt + type 'a or_error = ('a, exn * Caml.Printexc.raw_backtrace) Result.t let or_error f x () = diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index cb929c0f4..e11783ae3 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -70,6 +70,7 @@ let uncurry exp = in uncurry_ [] exp + let rec fmt ff exp = let pf fmt = Format.pp_open_box ff 2 ; @@ -125,6 +126,7 @@ let rec fmt ff exp = | Rem, [x; y] -> pf "(%a@ %% %a)" fmt x fmt y | URem, [x; y] -> pf "(%a@ u%% %a)" fmt x fmt y + (** Queries *) let rec typ_of : t -> Typ.t = function[@warning "p"] @@ -172,6 +174,7 @@ let rec typ_of : t -> Typ.t = function[@warning "p"] typ_of arg | AppN {op} -> typ_of op + let valid_fld fld elts = 0 <= fld && fld < Vector.length elts (** Re-exported modules *) @@ -220,6 +223,7 @@ module Global = struct (option_fmt " =@ @[%a@]" fmt) init + let fmt = fmt let mk ?init ?(loc = Loc.none) name typ = @@ -228,6 +232,7 @@ module Global = struct Typ.equal typ (Typ.mkPointer ~elt:(typ_of exp)) ) ) ; Global {name; init; typ; loc} + let of_exp e = match e with Global _ -> Some e | _ -> None let name = function[@warning "p"] Global {name} -> name @@ -249,6 +254,7 @@ let locate loc exp = | AppN {op; args} -> AppN {op; args; loc} | _ -> exp + let mkApp1 op arg = App {op; arg; loc= Loc.none} let mkApp2 op x y = mkApp1 (mkApp1 op x) y @@ -265,12 +271,14 @@ let mkNondet (typ : Typ.t) msg = assert (match typ with Function _ -> false | _ -> true) ; Nondet {typ; loc= Loc.none; msg} + let mkLabel ~parent ~name = Label {parent; name; loc= Loc.none} let mkNull (typ : Typ.t) = assert (match typ with Opaque _ | Function _ -> false | _ -> true) ; Null {typ} + let mkPtrFld ~ptr ~fld = assert ( match typ_of ptr with @@ -278,6 +286,7 @@ let mkPtrFld ~ptr ~fld = | _ -> false ) ; mkApp1 (PtrFld {fld}) ptr + let mkPtrIdx ~ptr ~idx = assert ( match (typ_of ptr, typ_of idx) with @@ -285,6 +294,7 @@ let mkPtrIdx ~ptr ~idx = | _ -> false ) ; mkApp2 PtrIdx ptr idx + let mkPrjFld ~agg ~fld = assert ( match typ_of agg with @@ -292,6 +302,7 @@ let mkPrjFld ~agg ~fld = | _ -> false ) ; mkApp1 (PrjFld {fld}) agg + let mkPrjIdx ~arr ~idx = assert ( match (typ_of arr, typ_of idx) with @@ -299,6 +310,7 @@ let mkPrjIdx ~arr ~idx = | _ -> false ) ; mkApp2 PrjIdx arr idx + let mkUpdFld ~agg ~elt ~fld = assert ( match typ_of agg with @@ -307,6 +319,7 @@ let mkUpdFld ~agg ~elt ~fld = | _ -> false ) ; mkApp2 (UpdFld {fld}) agg elt + let mkUpdIdx ~arr ~elt ~idx = assert ( match (typ_of arr, typ_of idx) with @@ -314,6 +327,7 @@ let mkUpdIdx ~arr ~elt ~idx = | _ -> false ) ; mkApp3 UpdIdx arr elt idx + let mkInteger data (typ : Typ.t) = assert ( let in_range num bits = @@ -324,12 +338,14 @@ let mkInteger data (typ : Typ.t) = match typ with Integer {bits} -> in_range data bits | _ -> false ) ; Integer {data; typ} + let mkBool b = mkInteger (Z.of_int (Bool.to_int b)) Typ.i1 let mkFloat data (typ : Typ.t) = assert (match typ with Float _ -> true | _ -> false) ; Float {data; typ} + let mkArray elts (typ : Typ.t) = assert ( match typ with @@ -339,6 +355,7 @@ let mkArray elts (typ : Typ.t) = | _ -> false ) ; mkAppN (Array {typ}) elts + let mkStruct elts (typ : Typ.t) = assert ( match typ with @@ -348,6 +365,7 @@ let mkStruct elts (typ : Typ.t) = | _ -> false ) ; mkAppN (Struct {typ}) elts + let mkStruct_rec key = let memo_id = Hashtbl.create key () in let dummy = Null {typ= Typ.mkBytes} in @@ -373,14 +391,17 @@ let mkStruct_rec key = in Staged.stage mkStruct_ + let mkCast exp typ = assert (Typ.compatible (typ_of exp) typ) ; mkApp1 (Cast {typ}) exp + let mkConv exp ?(signed = false) typ = assert (Typ.compatible (typ_of exp) typ) ; mkApp1 (Conv {signed; typ}) exp + let mkSelect ~cnd ~thn ~els = assert ( match (typ_of cnd, typ_of thn, typ_of els) with @@ -390,6 +411,7 @@ let mkSelect ~cnd ~thn ~els = | _ -> false ) ; mkApp3 Select cnd thn els + let binop op x y = assertf (let typ = typ_of x in @@ -404,6 +426,7 @@ let binop op x y = "ill-typed: %a" fmt (mkApp2 op x y) () ; mkApp2 op x y + let mkEq = binop Eq let mkNe = binop Ne diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index ac5864785..05a651ccc 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -14,6 +14,7 @@ let fmt_llvalue ff t = Format.pp_print_string ff (Llvm.string_of_llvalue t) let fmt_llblock ff t = Format.pp_print_string ff (Llvm.string_of_llvalue (Llvm.value_of_block t)) + (* gather debug locations *) let (scan_locs : Llvm.llmodule -> unit), (find_loc : Llvm.llvalue -> Loc.t) = @@ -81,6 +82,7 @@ let (scan_locs : Llvm.llmodule -> unit), (find_loc : Llvm.llvalue -> Loc.t) in (scan_locs, find_loc) + let ( (scan_names : Llvm.llmodule -> unit) , (find_name : Llvm.llvalue -> string) ) = let name_tbl = Hashtbl.Poly.create () in @@ -156,12 +158,15 @@ let ( (scan_names : Llvm.llmodule -> unit) let find_name v = Hashtbl.find_exn name_tbl v in (scan_names, find_name) + let label_of_block : Llvm.llbasicblock -> string = fun blk -> find_name (Llvm.value_of_block blk) + let anon_struct_name : (Llvm.lltype, string) Hashtbl.t = Hashtbl.Poly.create () + let struct_name : Llvm.lltype -> string = fun llt -> match Llvm.struct_name llt with @@ -170,6 +175,7 @@ let struct_name : Llvm.lltype -> string = Hashtbl.find_or_add anon_struct_name llt ~default:(fun () -> Int.to_string (Hashtbl.length anon_struct_name) ) + let memo_type : (Llvm.lltype, Typ.t) Hashtbl.t = Hashtbl.Poly.create () let rec xlate_type : Llvm.lltype -> Typ.t = @@ -226,12 +232,14 @@ let rec xlate_type : Llvm.lltype -> Typ.t = |> [%Trace.retn fun pf -> pf "%a" Typ.fmt_defn] ) + and xlate_type_opt : Llvm.lltype -> Typ.t option = fun llt -> match Llvm.classify_type llt with | Void -> None | _ -> Some (xlate_type llt) + let rec is_zero : Exp.t -> bool = fun exp -> match exp with @@ -241,9 +249,11 @@ let rec is_zero : Exp.t -> bool = | App {op; arg} -> is_zero op && is_zero arg | _ -> false + let suffix_after_space : string -> string = fun str -> String.slice str (String.rindex_exn str ' ' + 1) 0 + let xlate_int : Llvm.llvalue -> Exp.t = fun llv -> let typ = xlate_type (Llvm.type_of llv) in @@ -254,12 +264,14 @@ let xlate_int : Llvm.llvalue -> Exp.t = in Exp.mkInteger data typ + let xlate_float : Llvm.llvalue -> Exp.t = fun llv -> let typ = xlate_type (Llvm.type_of llv) in let data = suffix_after_space (Llvm.string_of_llvalue llv) in Exp.mkFloat data typ + let xlate_name_opt : Llvm.llvalue -> Var.t option = fun instr -> Option.map @@ -269,9 +281,11 @@ let xlate_name_opt : Llvm.llvalue -> Var.t option = let loc = find_loc instr in Var.mk name typ ~loc ) + let xlate_name : Llvm.llvalue -> Var.t = fun instr -> Option.value_exn (xlate_name_opt instr) + let xlate_intrinsic_exp : string -> (Exp.t -> Exp.t) option = fun name -> let i32 = Typ.mkInteger ~bits:32 in @@ -279,6 +293,7 @@ let xlate_intrinsic_exp : string -> (Exp.t -> Exp.t) option = | "llvm.eh.typeid.for" -> Some (fun arg -> Exp.mkCast arg i32) | _ -> None + let memo_value : (Llvm.llvalue, Exp.t) Hashtbl.t = Hashtbl.Poly.create () module Llvalue = struct @@ -368,6 +383,7 @@ let rec xlate_value : Llvm.llvalue -> Exp.t = typ' fmt_llvalue llv () ; pf "%a" Exp.fmt exp] ) + and xlate_opcode : Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = fun llv opcode -> [%Trace.call fun pf -> pf "%a" fmt_llvalue llv] @@ -529,6 +545,7 @@ and xlate_opcode : Llvm.llvalue -> Llvm.Opcode.t -> Exp.t = fmt_llvalue llv () ; pf "%a" Exp.fmt exp] + and xlate_global : Llvm.llvalue -> Global.t = fun llg -> let init = @@ -540,6 +557,7 @@ and xlate_global : Llvm.llvalue -> Global.t = let g = xlate_name llg in Global.mk (Var.name g) (Var.typ g) ~loc:(Var.loc g) ?init + let xlate_global : Llvm.llvalue -> Global.t = fun llg -> [%Trace.call fun pf -> pf "%a" fmt_llvalue llg] @@ -548,6 +566,7 @@ let xlate_global : Llvm.llvalue -> Global.t = |> [%Trace.retn fun pf -> pf "%a" Global.fmt] + type pop_thunk = Loc.t -> Llair.inst list let pop_stack_frame_of_function : @@ -580,6 +599,7 @@ let pop_stack_frame_of_function : in pop + (** construct the types involved in landingpads: i32, std::type_info*, and __cxa_exception *) let landingpad_typs : Llvm.llvalue -> Typ.t * Typ.t * Typ.t = @@ -607,12 +627,14 @@ let landingpad_typs : Llvm.llvalue -> Typ.t * Typ.t * Typ.t = let cxa_exception = Llvm.struct_type llcontext [|tip; dtor|] in (i32, xlate_type tip, xlate_type cxa_exception) + (** construct the argument of a landingpad block, mainly fix the encoding scheme for landingpad instruction name to block arg name *) let landingpad_arg : Llvm.llvalue -> Var.t = fun instr -> Var.mk (find_name instr ^ ".exc") Typ.i8p ~loc:(find_loc instr) + (** [rev_map_phis ~f blk] returns [(retn_arg, rev_args, pos)] by rev_mapping over the prefix of [PHI] instructions at the beginning of [blk]. [retn_arg], if any, is [f] applied to the [PHI] instruction which takes @@ -669,6 +691,7 @@ let rev_map_phis : in block_args_ false None [] (Llvm.instr_begin blk) + (** [trampoline_args jump_instr dest_block] is the actual arguments to which the translation of [dest_block] should be partially-applied, to yield a trampoline accepting the return parameter of the block and then jumping @@ -681,6 +704,7 @@ let trampoline_args : Llvm.llvalue -> Llvm.llbasicblock -> Exp.t vector = if Poly.equal pred src then Some (xlate_value arg) else None ) ) |> snd3 |> Vector.of_list_rev + (** [unique_pred blk] is the unique predecessor of [blk], or [None] if there are 0 or >1 predecessors. *) let unique_pred : Llvm.llbasicblock -> Llvm.llvalue option = @@ -692,11 +716,13 @@ let unique_pred : Llvm.llbasicblock -> Llvm.llvalue option = | Some _ -> None ) | None -> None + (** [return_formal_is_used instr] holds if the return value of [instr] is used anywhere. *) let return_formal_is_used : Llvm.llvalue -> bool = fun instr -> Option.is_some (Llvm.use_begin instr) + (** [need_return_trampoline instr blk] holds when the return formal of [instr] is used, but the returned to block [blk] does not take it as an argument (e.g. if it has multiple predecessors and no PHI node). *) @@ -706,6 +732,7 @@ let need_return_trampoline : Llvm.llvalue -> Llvm.llbasicblock -> bool = && Option.is_none (unique_pred blk) && return_formal_is_used instr + (** [unique_used_invoke_pred blk] is the unique predecessor of [blk], if it is an [Invoke] instruction, whose return value is used. *) let unique_used_invoke_pred : Llvm.llbasicblock -> 'a option = @@ -716,6 +743,7 @@ let unique_used_invoke_pred : Llvm.llbasicblock -> 'a option = Some instr | _ -> None + (** formal parameters accepted by a block *) let block_formals : Llvm.llbasicblock -> Var.t list * _ Llvm.llpos = fun blk -> @@ -734,6 +762,7 @@ let block_formals : Llvm.llbasicblock -> Var.t list * _ Llvm.llpos = (List.rev_append rev_args (Option.to_list instr_arg), pos) | At_end blk -> fail "block_formals: %a" fmt_llblock blk () + (** actual arguments passed by a jump to a block *) let jump_args : Llvm.llvalue -> Llvm.llbasicblock -> Exp.t vector = fun jmp dst -> @@ -752,6 +781,7 @@ let jump_args : Llvm.llvalue -> Llvm.llbasicblock -> Exp.t vector = in Vector.of_list (List.rev_append rev_args (Option.to_list retn_arg)) + (** An LLVM instruction is translated to a sequence of LLAIR instructions and a terminator, plus some additional blocks to which it may refer (that is, essentially a function body). These are needed since LLVM and @@ -774,6 +804,7 @@ let fmt_code ff (insts, term, blocks) = (list_fmt "@ " Llair.Block.fmt) blocks + let rec xlate_func_name llv = match Llvm.classify_value llv with | Function -> @@ -788,6 +819,7 @@ let rec xlate_func_name llv = | InlineAsm -> todo "inline asm: %a" fmt_llvalue llv () | _ -> fail "unknown function: %a" fmt_llvalue llv () + let xlate_instr : pop_thunk -> Llvm.llvalue @@ -1173,6 +1205,7 @@ let xlate_instr : fail "xlate_instr: %a" fmt_llvalue instr () | PHI | Invalid | Invalid2 | UserOp1 | UserOp2 -> assert false + let rec xlate_instrs : pop_thunk -> _ Llvm.llpos -> code = fun pop -> function | Before instrI -> @@ -1183,6 +1216,7 @@ let rec xlate_instrs : pop_thunk -> _ Llvm.llpos -> code = (instsI, termI, blocksI @ blocksJN) ) | At_end blk -> fail "xlate_instrs: %a" fmt_llblock blk () + let xlate_block : pop_thunk -> Llvm.llbasicblock -> Llair.block list = fun pop blk -> [%Trace.call fun pf -> pf "%a" fmt_llblock blk] @@ -1196,6 +1230,7 @@ let xlate_block : pop_thunk -> Llvm.llbasicblock -> Llair.block list = |> [%Trace.retn fun pf blocks -> pf "%s" (List.hd_exn blocks).Llair.lbl] + let xlate_function : Llvm.llvalue -> Llair.func = fun llf -> [%Trace.call fun pf -> pf "%a" fmt_llvalue llf] @@ -1234,6 +1269,7 @@ let xlate_function : Llvm.llvalue -> Llair.func = |> [%Trace.retn fun pf -> pf "@\n%a" Llair.Func.fmt] + let transform : Llvm.llmodule -> unit = fun llmodule -> let pm = Llvm.PassManager.create () in @@ -1245,6 +1281,7 @@ let transform : Llvm.llmodule -> unit = Llvm.PassManager.run_module llmodule pm |> (ignore : bool -> _) ; Llvm.PassManager.dispose pm + exception Invalid_llvm of string let invalid_llvm : string -> 'a = @@ -1256,6 +1293,7 @@ let invalid_llvm : string -> 'a = Format.printf "@\n%s@\n" msg ; raise (Invalid_llvm first_line) + let translate : string -> Llair.t = fun file -> [%Trace.call fun pf -> pf "%s" file] diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index 60950df1c..20f0927e8 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -66,9 +66,11 @@ let rec dummy_block = ; parent= dummy_func ; sort_index= 0 } + and dummy_func = {name= Global.mk "dummy" Typ.i8p; entry= dummy_block; cfg= Vector.empty} + module Inst = struct type t = inst @@ -79,6 +81,7 @@ module Inst = struct | _ -> false ) ; Load {reg; ptr; loc} + let mkStore ~ptr ~exp ~loc = assert ( match Exp.typ ptr with @@ -86,6 +89,7 @@ module Inst = struct | _ -> false ) ; Store {ptr; exp; loc} + let mkMemcpy ~dst ~src ~len ~loc = assert ( match (Exp.typ dst, Exp.typ src, Exp.typ len) with @@ -94,6 +98,7 @@ module Inst = struct | _ -> false ) ; Memcpy {dst; src; len; loc} + let mkMemmov ~dst ~src ~len ~loc = assert ( match (Exp.typ dst, Exp.typ src, Exp.typ len) with @@ -102,6 +107,7 @@ module Inst = struct | _ -> false ) ; Memmov {dst; src; len; loc} + let mkMemset ~dst ~byt ~len ~loc = assert ( match (Exp.typ dst, Exp.typ byt, Exp.typ len) with @@ -109,6 +115,7 @@ module Inst = struct | _ -> false ) ; Memset {dst; byt; len; loc} + let mkAlloc ~reg ~num ~loc = assert ( match (Var.typ reg, Exp.typ num) with @@ -116,6 +123,7 @@ module Inst = struct | _ -> false ) ; Alloc {reg; num; loc} + let mkFree ~ptr ~loc = assert ( match Exp.typ ptr with @@ -123,10 +131,12 @@ module Inst = struct | _ -> false ) ; Free {ptr; loc} + let mkNondet ~reg ~msg ~loc = assert (Option.for_all ~f:(Var.typ >> Typ.is_sized) reg) ; Nondet {reg; msg; loc} + let fmt ff inst = let pf fmt = Format.fprintf ff fmt in match inst with @@ -151,9 +161,11 @@ let fmt_cmnd = vector_fmt "@ " Inst.fmt let fmt_args fmt_arg ff args = Format.fprintf ff "@ (@[%a@])" (vector_fmt ",@ " fmt_arg) args + let fmt_param ff var = Format.fprintf ff "%a %a" Typ.fmt (Var.typ var) Var.fmt var + module Jump = struct type t = jump @@ -172,6 +184,7 @@ module Term = struct assert (match Exp.typ key with Integer _ -> true | _ -> false) ; Switch {key; tbl; els; loc} + let mkISwitch ~ptr ~tbl ~loc = assert ( match Exp.typ ptr with @@ -179,6 +192,7 @@ module Term = struct | _ -> false ) ; ISwitch {ptr; tbl; loc} + let mkCall ~func ~args ~return ~throw ~ignore_result ~loc = assert ( match Exp.typ func with @@ -193,6 +207,7 @@ module Term = struct ; ignore_result ; loc } + let mkReturn ~exp ~loc = Return {exp; loc} let mkThrow ~exc ~loc = Throw {exc; loc} @@ -239,6 +254,7 @@ module Block = struct ) ; {dummy_block with lbl; params; cmnd; term} + (* blocks in a [t] are uniquely identified by [sort_index] *) let compare x y = Int.compare x.sort_index y.sort_index @@ -257,15 +273,18 @@ module Func = struct let find functions func = Vector.find functions ~f:(fun {name} -> Global.equal func name) + let is_undefined = function | {entry= {cmnd; term= Unreachable}} -> Vector.is_empty cmnd | _ -> false + let fold_term {entry; cfg} ~init ~f = let fold_block {term} ~init ~f = f init term in Vector.fold cfg ~init:(fold_block entry ~init ~f) ~f:(fun z k -> fold_block k ~init:z ~f ) + let mk ~name ~entry ~cfg = let func = {name; entry; cfg} in let resolve_parent_and_jumps block = @@ -330,6 +349,7 @@ module Func = struct true ) ; func + let mk_undefined ~name ~params = let entry = Block.mk ~lbl:"" ~params ~cmnd:Vector.empty ~term:Term.mkUnreachable @@ -337,6 +357,7 @@ module Func = struct let cfg = Vector.empty in mk ~name ~entry ~cfg + let fmt ff ({name; entry= {params; cmnd; term; sort_index}; cfg} as func) = let fmt_if cnd str ff = if cnd then Format.fprintf ff str in @@ -363,6 +384,7 @@ module Block_id = struct [%compare: string * Global.t] (x.lbl, x.parent.name) (y.lbl, y.parent.name) + let hash b = Hashtbl.hash (b.lbl, b.parent.name) end @@ -442,6 +464,7 @@ let set_derived_metadata functions = sort_functions functions ; Vector.of_array functions + let mk ~typ_defns ~globals ~functions = assert ( (not @@ -462,6 +485,7 @@ let mk ~typ_defns ~globals ~functions = ; globals= Vector.of_list_rev globals ; functions= set_derived_metadata functions } + let fmt ff {typ_defns; globals; functions} = Format.fprintf ff "@[@[%a@]@ @ @ @[%a@]@ @ @ @[%a@]@]" (list_fmt "@\n@\n" Typ.fmt_defn) diff --git a/sledge/src/llair/loc.ml b/sledge/src/llair/loc.ml index 0dcae9b19..0911df1c9 100644 --- a/sledge/src/llair/loc.ml +++ b/sledge/src/llair/loc.ml @@ -15,6 +15,7 @@ let none = {dir= ""; file= ""; line= 0; col= 0} let mk ?(dir = none.dir) ?(file = none.file) ?(col = none.col) ~line = {dir; file; line; col} + let fmt ff {dir; file; line; col} = Format.pp_print_string ff dir ; if not (String.is_empty dir) then diff --git a/sledge/src/llair/typ.ml b/sledge/src/llair/typ.ml index 8f41a7c15..3aee5e7f4 100644 --- a/sledge/src/llair/typ.ml +++ b/sledge/src/llair/typ.ml @@ -45,6 +45,7 @@ let rec fmt ff typ = | Struct {name} | Opaque {name} -> Format.fprintf ff "@[%%%s@]" name | Bytes -> Format.fprintf ff "bytes" + and fmts ff typs = vector_fmt ",@ " fmt ff typs let fmt_defn ff = function @@ -54,6 +55,7 @@ let fmt_defn ff = function | Opaque {name} -> Format.fprintf ff "@[<2>%%%s =@ opaque@]" name | typ -> fmt ff typ + let is_sized = function | Function _ | Bytes -> false | Integer _ | Float _ | Pointer _ | Array _ | Tuple _ | Struct _ -> true @@ -62,12 +64,14 @@ let is_sized = function as they are not sized but may become sized through linking. *) true + let rec prim_bit_size_of = function | Integer {bits} | Float {bits} -> Some bits | Array {elt; len} -> Option.map (prim_bit_size_of elt) ~f:(fun n -> n * len) | Opaque _ | Function _ | Pointer _ | Tuple _ | Struct _ | Bytes -> None + let rec compatible t0 t1 = match (t0, t1, prim_bit_size_of t0, prim_bit_size_of t1) with | ( (Integer _ | Float _ | Pointer _) @@ -86,11 +90,13 @@ let rec compatible t0 t1 = true | _ -> false + let mkFunction ~return ~args = assert ( Option.for_all ~f:is_sized return && Vector.for_all ~f:is_sized args ) ; Function {return; args} + let mkInteger ~bits = Integer {bits} let mkFloat ~bits ~enc = Float {bits; enc} @@ -101,12 +107,14 @@ let mkArray ~elt ~len = assert (is_sized elt) ; Array {elt; len} + let defns : (string, t) Hashtbl.t = Hashtbl.create (module String) () let mkTuple ~packed elts = assert (Vector.for_all ~f:is_sized elts) ; Tuple {elts; packed} + let mkStruct ~name ~packed elt_thks = match Hashtbl.find defns name with | Some typ -> typ @@ -124,6 +132,7 @@ let mkStruct ~name ~packed elt_thks = elts.(i) <- elt ) ; typ + let mkOpaque ~name = Opaque {name} let mkBytes = Bytes diff --git a/sledge/src/ppx_trace/ppx_trace.ml b/sledge/src/ppx_trace/ppx_trace.ml index 3872fb85d..55b7bd015 100644 --- a/sledge/src/ppx_trace/ppx_trace.ml +++ b/sledge/src/ppx_trace/ppx_trace.ml @@ -54,6 +54,7 @@ let rec get_fun_name pat = (Selected_ast.To_ocaml.copy_pattern p) ) pat + let vb_stack_with, vb_stack_top = let stack = ref [] in let with_ x ~f = @@ -65,6 +66,7 @@ let vb_stack_with, vb_stack_top = let top () = List.hd_exn !stack in (with_, top) + let mapper = let value_binding (m : Ast_mapper.mapper) vb = vb_stack_with vb.pvb_pat ~f:(fun () -> @@ -113,6 +115,7 @@ let mapper = in {Ast_mapper.default_mapper with expr; value_binding} + let impl = Selected_ast.Ast.map_structure mapper ;; diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml index 3f6630350..6a0f345a9 100644 --- a/sledge/src/sledge.ml +++ b/sledge/src/sledge.ml @@ -32,5 +32,6 @@ let main ~input ~output = (Caml.Printexc.to_string exn) ) ; Caml.Printexc.raise_with_backtrace exn bt + ;; Config.run main diff --git a/sledge/src/trace/trace.ml b/sledge/src/trace/trace.ml index 0d2ed4e6a..43c5500af 100644 --- a/sledge/src/trace/trace.ml +++ b/sledge/src/trace/trace.ml @@ -26,6 +26,7 @@ let init ~trace_all:ta = Caml.at_exit flush ; trace_all := ta + (* selective tracing not yet implemented *) let enabled _ = !trace_all @@ -35,18 +36,21 @@ let info mod_name fun_name fmt = Format.kfprintf (fun ff -> Format.fprintf ff "@]") ff fmt ) else Format.ifprintf ff fmt + let incf rev_prefix name fmt = if enabled (name :: rev_prefix) then ( Format.fprintf ff "@\n@[<2>@[( %s: " name ; Format.kfprintf (fun ff -> Format.fprintf ff "@]") ff fmt ) else Format.ifprintf ff fmt + let decf rev_prefix name fmt = if enabled (name :: rev_prefix) then ( Format.fprintf ff "@]@\n@[<2>) %s:@ " name ; Format.kfprintf (fun ff -> Format.fprintf ff "@]") ff fmt ) else Format.ifprintf ff fmt + let call mod_name fun_name k = k (incf [mod_name] fun_name) let retn mod_name fun_name k result =