From 61566caddf9f7b9e9f8bc77f50914ca5e359f648 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 16 May 2020 08:28:41 -0700 Subject: [PATCH] [ocamlformat] Set break-sequences = true Summary: Add `break-sequences = true` to .ocamlformat and reformat. Reviewed By: jvillard Differential Revision: D21583901 fbshipit-source-id: eb4ec836c --- infer/src/.ocamlformat | 1 + infer/src/IR/AccessPath.ml | 8 +- infer/src/IR/BiabductionModels.ml | 3 +- infer/src/IR/BuiltinDecl.ml | 6 +- infer/src/IR/Cfg.ml | 3 +- infer/src/IR/Errlog.ml | 3 +- infer/src/IR/HilExp.ml | 3 +- infer/src/IR/Ident.ml | 7 +- infer/src/IR/Io_infer.ml | 3 +- infer/src/IR/IssueLog.ml | 3 +- infer/src/IR/Localise.ml | 3 +- infer/src/IR/Tenv.ml | 6 +- infer/src/IR/inferconfig.ml | 3 +- infer/src/absint/ConcurrencyModels.ml | 7 +- infer/src/absint/DataFlow.ml | 3 +- infer/src/absint/PatternMatch.ml | 10 +- infer/src/al/ALDebugger.ml | 9 +- infer/src/al/CTL.ml | 3 +- infer/src/al/ctl_parser_types.ml | 9 +- infer/src/backend/CallGraph.ml | 14 +- infer/src/backend/InferAnalyze.ml | 13 +- infer/src/backend/ProcLocker.ml | 9 +- infer/src/backend/Procedures.ml | 3 +- infer/src/backend/RestartScheduler.ml | 6 +- infer/src/backend/SpecsFiles.ml | 4 +- infer/src/backend/Tasks.ml | 8 +- infer/src/backend/ondemand.ml | 7 +- infer/src/backend/printer.ml | 6 +- infer/src/base/CommandLineOption.ml | 3 +- infer/src/base/Config.ml | 18 +- infer/src/base/DB.ml | 6 +- infer/src/base/DBWriter.ml | 9 +- infer/src/base/Epilogues.ml | 10 +- infer/src/base/LineReader.ml | 7 +- infer/src/base/Logging.ml | 50 +++- infer/src/base/ProcessPool.ml | 9 +- infer/src/base/ScubaLogging.ml | 3 +- infer/src/base/SymOp.ml | 6 +- infer/src/base/TaskBar.ml | 3 +- infer/src/base/Utils.ml | 25 +- infer/src/biabduction/Abs.ml | 12 +- infer/src/biabduction/Absarray.ml | 27 +- infer/src/biabduction/Attribute.ml | 9 +- infer/src/biabduction/Builtin.ml | 4 +- infer/src/biabduction/Dom.ml | 273 +++++++++++++----- infer/src/biabduction/DotBiabduction.ml | 7 +- infer/src/biabduction/Paths.ml | 47 ++- infer/src/biabduction/Predicates.ml | 5 +- infer/src/biabduction/Prop.ml | 10 +- infer/src/biabduction/Prover.ml | 73 +++-- infer/src/biabduction/Rearrange.ml | 20 +- infer/src/biabduction/RetainCyclesType.ml | 3 +- infer/src/biabduction/State.ml | 5 +- infer/src/biabduction/SymExec.ml | 3 +- infer/src/biabduction/Tabulation.ml | 16 +- infer/src/biabduction/Timeout.ml | 9 +- infer/src/biabduction/errdesc.ml | 65 ++++- infer/src/biabduction/interproc.ml | 16 +- infer/src/bufferoverrun/absLoc.ml | 5 +- infer/src/bufferoverrun/bounds.ml | 14 +- .../bufferoverrun/bufferOverrunAnalysis.ml | 3 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 5 +- infer/src/bufferoverrun/symb.ml | 5 +- infer/src/checkers/NullabilityPreanalysis.ml | 3 +- infer/src/checkers/annotationReachability.ml | 3 +- infer/src/checkers/dominators.ml | 3 +- infer/src/checkers/uninit.ml | 3 +- infer/src/clang/cAst_utils.ml | 3 +- infer/src/clang/cMethod_trans.ml | 6 +- infer/src/clang/cScope.ml | 3 +- infer/src/cost/boundMap.ml | 3 +- infer/src/infer.ml | 11 +- infer/src/integration/IssuesTest.ml | 3 +- infer/src/integration/JsonReports.ml | 3 +- infer/src/integration/TraceBugs.ml | 3 +- infer/src/integration/XcodeBuild.ml | 3 +- infer/src/istd/IList.ml | 9 +- infer/src/istd/ImperativeUnionFind.ml | 6 +- infer/src/istd/LRUHashtbl.ml | 22 +- infer/src/istd/RecencyMap.ml | 3 +- infer/src/java/jFrontend.ml | 3 +- infer/src/java/jMain.ml | 3 +- infer/src/java/jTrans.ml | 3 +- infer/src/nullsafe/Initializers.ml | 7 +- infer/src/nullsafe/eradicateChecks.ml | 3 +- infer/src/nullsafe/typeCheck.ml | 3 +- infer/src/nullsafe/typeErr.ml | 6 +- infer/src/pulse/PulseAbstractValue.ml | 3 +- infer/src/topl/Topl.ml | 28 +- infer/src/topl/ToplAutomaton.ml | 6 +- infer/src/topl/ToplMonitor.ml | 4 +- infer/src/unit/LRUHashtblTests.ml | 7 +- infer/src/unit/analyzerTester.ml | 5 +- 93 files changed, 827 insertions(+), 292 deletions(-) diff --git a/infer/src/.ocamlformat b/infer/src/.ocamlformat index b62296da5..3b5aa47ea 100644 --- a/infer/src/.ocamlformat +++ b/infer/src/.ocamlformat @@ -1,5 +1,6 @@ profile = ocamlformat break-before-in = fit-or-vertical +break-sequences = true let-binding-spacing = sparse margin = 100 parse-docstrings = true diff --git a/infer/src/IR/AccessPath.ml b/infer/src/IR/AccessPath.ml index 85668405d..db10b88fa 100644 --- a/infer/src/IR/AccessPath.ml +++ b/infer/src/IR/AccessPath.ml @@ -29,13 +29,17 @@ module Raw = struct if Config.debug_level_analysis >= 3 then F.fprintf fmt ":%a" (Typ.pp Pp.text) typ - let pp_base fmt (pvar, typ) = Var.pp fmt pvar ; may_pp_typ fmt typ + let pp_base fmt (pvar, typ) = + Var.pp fmt pvar ; + may_pp_typ fmt typ + let rec pp_access fmt = function | FieldAccess field_name -> F.pp_print_string fmt (Fieldname.get_field_name field_name) | ArrayAccess (typ, []) -> - F.pp_print_string fmt "[_]" ; may_pp_typ fmt typ + F.pp_print_string fmt "[_]" ; + may_pp_typ fmt typ | ArrayAccess (typ, index_aps) -> F.fprintf fmt "[%a]" (PrettyPrintable.pp_collection ~pp_item:pp) index_aps ; may_pp_typ fmt typ diff --git a/infer/src/IR/BiabductionModels.ml b/infer/src/IR/BiabductionModels.ml index 53bff3021..cd2a16051 100644 --- a/infer/src/IR/BiabductionModels.ml +++ b/infer/src/IR/BiabductionModels.ml @@ -11,7 +11,8 @@ let scan_models () = let rec next_entry index dir = match Unix.readdir_opt dir with | None -> - Unix.closedir dir ; index + Unix.closedir dir ; + index | Some entry -> ( match String.chop_suffix entry ~suffix:Config.specs_files_suffix with | Some file_proc_name -> diff --git a/infer/src/IR/BuiltinDecl.ml b/infer/src/IR/BuiltinDecl.ml index bd40d29a8..03c99a6d6 100644 --- a/infer/src/IR/BuiltinDecl.ml +++ b/infer/src/IR/BuiltinDecl.ml @@ -15,7 +15,8 @@ let register pname = builtin_decls := Procname.Set.add pname !builtin_decls let create_procname name = let pname = Procname.from_string_c_fun name in - register pname ; pname + register pname ; + pname let create_objc_class_method class_name method_name parameters = @@ -25,7 +26,8 @@ let create_objc_class_method class_name method_name parameters = Procname.ObjC_Cpp (Procname.ObjC_Cpp.make tname method_name method_kind Typ.NoTemplate parameters) in - register pname ; pname + register pname ; + pname let is_declared pname = Procname.Set.mem pname !builtin_decls diff --git a/infer/src/IR/Cfg.ml b/infer/src/IR/Cfg.ml index bf4bbda46..248603f14 100644 --- a/infer/src/IR/Cfg.ml +++ b/infer/src/IR/Cfg.ml @@ -27,7 +27,8 @@ let iter_over_sorted_procs cfg ~f = let get_all_defined_proc_names cfg = let procs = ref [] in let f pname pdesc = if Procdesc.is_defined pdesc then procs := pname :: !procs in - Procname.Hash.iter f cfg ; !procs + Procname.Hash.iter f cfg ; + !procs (** Create a new procdesc *) diff --git a/infer/src/IR/Errlog.ml b/infer/src/IR/Errlog.ml index 1eb1088b5..f228be34a 100644 --- a/infer/src/IR/Errlog.ml +++ b/infer/src/IR/Errlog.ml @@ -276,6 +276,7 @@ let log_issue severity err_log ~loc ~node ~session ~ltr ~linters_def_file ~doc_u | Exceptions.Info | Exceptions.Advice | Exceptions.Like -> L.d_info in - d warn_str ; L.d_ln () ) + d warn_str ; + L.d_ln () ) in if should_print_now then print_now () diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index 77993d2e7..c0d959fd5 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -147,7 +147,8 @@ let pp_array_offset_opt pp_offset fmt = function let rec pp_access_expr fmt = function | Base (pvar, typ) -> - Var.pp fmt pvar ; may_pp_typ fmt typ + Var.pp fmt pvar ; + may_pp_typ fmt typ | FieldOffset (Dereference ae, fld) -> F.fprintf fmt "%a->%a" pp_access_expr ae Fieldname.pp fld | FieldOffset (ae, fld) -> diff --git a/infer/src/IR/Ident.ml b/infer/src/IR/Ident.ml index 9ddf4e7b2..3182c8c49 100644 --- a/infer/src/IR/Ident.ml +++ b/infer/src/IR/Ident.ml @@ -140,7 +140,9 @@ module NameGenerator = struct let stamp = NameHash.find !name_map name in NameHash.replace !name_map name (stamp + 1) ; stamp + 1 - with Caml.Not_found -> NameHash.add !name_map name 0 ; 0 + with Caml.Not_found -> + NameHash.add !name_map name 0 ; + 0 in {kind; name; stamp} @@ -261,4 +263,5 @@ let counts_of_sequence seq = let h = Hash.create (Sequence.length seq) in let get id = Option.value (Hash.find_opt h id) ~default:0 in let bump id = Hash.replace h id (1 + get id) in - Sequence.iter ~f:bump seq ; get + Sequence.iter ~f:bump seq ; + get diff --git a/infer/src/IR/Io_infer.ml b/infer/src/IR/Io_infer.ml index 76ac00792..7377fe1b4 100644 --- a/infer/src/IR/Io_infer.ml +++ b/infer/src/IR/Io_infer.ml @@ -56,7 +56,8 @@ h1 { font-size:14pt } |} in - F.pp_print_string fmt s ; (fd, fmt) + F.pp_print_string fmt s ; + (fd, fmt) (** Get the full html filename from a path *) diff --git a/infer/src/IR/IssueLog.ml b/infer/src/IR/IssueLog.ml index 46707b49a..15f26e83d 100644 --- a/infer/src/IR/IssueLog.ml +++ b/infer/src/IR/IssueLog.ml @@ -55,7 +55,8 @@ let load entry = (fun _ issues1 issues2 -> match (issues1, issues2) with | Some issues1, Some issues2 -> - Errlog.update issues1 issues2 ; Some issues1 + Errlog.update issues1 issues2 ; + Some issues1 | Some issues1, None -> Some issues1 | None, Some issues2 -> diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index dc03bea13..8533e4702 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -656,7 +656,8 @@ let desc_unary_minus_applied_to_unsigned_expression expr_str_opt typ_str loc = let expression = match expr_str_opt with | Some s -> - Tags.update tags Tags.value s ; "expression " ^ s + Tags.update tags Tags.value s ; + "expression " ^ s | None -> "an expression" in diff --git a/infer/src/IR/Tenv.ml b/infer/src/IR/Tenv.ml index 8ed42642f..5d0901c1c 100644 --- a/infer/src/IR/Tenv.ml +++ b/infer/src/IR/Tenv.ml @@ -113,7 +113,8 @@ let merge_per_file ~src ~dst = | Global, Global -> Global | FileLocal src_tenv, FileLocal dst_tenv -> - merge ~src:src_tenv ~dst:dst_tenv ; FileLocal dst_tenv + merge ~src:src_tenv ~dst:dst_tenv ; + FileLocal dst_tenv | Global, FileLocal _ | FileLocal _, Global -> L.die InternalError "Cannot merge Global tenv with FileLocal tenv" @@ -154,7 +155,8 @@ let store_debug_file tenv tenv_filename = let debug_filename = DB.filename_to_string (DB.filename_add_suffix tenv_filename ".debug") in let out_channel = Out_channel.create debug_filename in let fmt = Format.formatter_of_out_channel out_channel in - pp fmt tenv ; Out_channel.close out_channel + pp fmt tenv ; + Out_channel.close out_channel let store_debug_file_for_source source_file tenv = diff --git a/infer/src/IR/inferconfig.ml b/infer/src/IR/inferconfig.ml index 6738e7d4a..378449fdc 100644 --- a/infer/src/IR/inferconfig.ml +++ b/infer/src/IR/inferconfig.ml @@ -258,7 +258,8 @@ let patterns_of_json_with_key (json_key, json) = | Ok pattern -> pattern :: accu | Error msg -> - warn_user msg ; accu ) + warn_user msg ; + accu ) | `List l -> List.fold ~f:translate ~init:accu l | json -> diff --git a/infer/src/absint/ConcurrencyModels.ml b/infer/src/absint/ConcurrencyModels.ml index c974f18c9..1f35e4d5b 100644 --- a/infer/src/absint/ConcurrencyModels.ml +++ b/infer/src/absint/ConcurrencyModels.ml @@ -212,7 +212,12 @@ end = struct actuals in let guard_action ~f ~error = - match actuals with [guard] -> f guard | _ -> log_parse_error error ; NoEffect + match actuals with + | [guard] -> + f guard + | _ -> + log_parse_error error ; + NoEffect in let fst_arg = match actuals with x :: _ -> [x] | _ -> [] in if is_std_lock pname then Lock actuals diff --git a/infer/src/absint/DataFlow.ml b/infer/src/absint/DataFlow.ml index 471b5ed5b..aac7041f1 100644 --- a/infer/src/absint/DataFlow.ml +++ b/infer/src/absint/DataFlow.ml @@ -138,7 +138,8 @@ module MakeDF (St : DFStateType) : DF with type state = St.t = struct let init_set = S.singleton start_node in let init_statemap = let m = H.create 1 in - H.replace m start_node state ; m + H.replace m start_node state ; + m in { worklist= init_set ; pre_states= init_statemap diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml index 0c7d794f1..a9026f77a 100644 --- a/infer/src/absint/PatternMatch.ml +++ b/infer/src/absint/PatternMatch.ml @@ -318,7 +318,8 @@ let proc_calls resolve_attributes pdesc filter : (Procname.t * ProcAttributes.t) Instrs.iter ~f:(do_instruction node) instrs in let nodes = Procdesc.get_nodes pdesc in - List.iter ~f:do_node nodes ; List.rev !res + List.iter ~f:do_node nodes ; + List.rev !res let has_same_signature proc_name = @@ -370,7 +371,12 @@ let override_exists ?(check_current_type = true) f tenv proc_name = (* Only java supported at the moment *) let override_iter f tenv proc_name = - ignore (override_exists (fun pname -> f pname ; false) tenv proc_name) + ignore + (override_exists + (fun pname -> + f pname ; + false ) + tenv proc_name) let lookup_attributes tenv proc_name = diff --git a/infer/src/al/ALDebugger.ml b/infer/src/al/ALDebugger.ml index 34c510120..523df495c 100644 --- a/infer/src/al/ALDebugger.ml +++ b/infer/src/al/ALDebugger.ml @@ -194,7 +194,8 @@ module EvaluationTracker = struct stop_and_explain_step () ; {t with debugger_active= true} | true, _, _ -> - stop_and_explain_step () ; t + stop_and_explain_step () ; + t | _ -> t @@ -244,7 +245,8 @@ module EvaluationTracker = struct | Tree (node, children), ntd -> (Tree (node, evaluated_tree :: children), ntd) in - Stack.push t'.eval_stack parent ; t'.forest + Stack.push t'.eval_stack parent ; + t'.forest in {t' with forest= forest'} @@ -257,7 +259,8 @@ module EvaluationTracker = struct let open Ctl_parser_types in let buffer_content buf = let result = Buffer.contents buf in - Buffer.reset buf ; result + Buffer.reset buf ; + result in let dotty_of_tree cluster_id tree = let get_root tree = match tree with Tree (root, _) -> root in diff --git a/infer/src/al/CTL.ml b/infer/src/al/CTL.ml index 6dcda1f82..d9ad6c089 100644 --- a/infer/src/al/CTL.ml +++ b/infer/src/al/CTL.ml @@ -999,4 +999,5 @@ and eval_formula ?keep_witness f an lcxt : Ctl_parser_types.ast_node option = | InObjCClass (f1, f2) -> eval_InObjCClass an lcxt f1 f2 in - debug_eval_end res ; res + debug_eval_end res ; + res diff --git a/infer/src/al/ctl_parser_types.ml b/infer/src/al/ctl_parser_types.ml index 93c607973..5d73236c0 100644 --- a/infer/src/al/ctl_parser_types.ml +++ b/infer/src/al/ctl_parser_types.ml @@ -423,7 +423,8 @@ let builtin_equal (bi : Clang_ast_t.builtin_type_kind) (abi : builtin_kind) = | Some assoc_abi when equal_builtin_kind assoc_abi abi -> true | _ -> - display_equality_warning () ; false + display_equality_warning () ; + false let typename_to_string pointer = @@ -446,7 +447,8 @@ let rec pointer_type_equal p ap = | PointerType (_, qt), BuiltIn _ -> check_type_ptr qt.qt_type_ptr ap | _, _ -> - display_equality_warning () ; false + display_equality_warning () ; + false and objc_object_type_equal c_type abs_ctype = @@ -562,7 +564,8 @@ and c_type_equal c_type abs_ctype = | AttributedType (ti, _), TypeName _ -> ( match ti.ti_desugared_type with Some dt -> check_type_ptr dt abs_ctype | None -> false ) | _, _ -> - display_equality_warning () ; false + display_equality_warning () ; + false (* to be extended with more types *) diff --git a/infer/src/backend/CallGraph.ml b/infer/src/backend/CallGraph.ml index 4c40c7a56..ba2282c8b 100644 --- a/infer/src/backend/CallGraph.ml +++ b/infer/src/backend/CallGraph.ml @@ -52,7 +52,10 @@ module NodeMap = Caml.Hashtbl.Make (Int) [trim_id_map] makes the image equal to the domain of [node_map]. *) type t = {id_map: int IdMap.t; node_map: Node.t NodeMap.t} -let reset {id_map; node_map} = IdMap.reset id_map ; NodeMap.reset node_map +let reset {id_map; node_map} = + IdMap.reset id_map ; + NodeMap.reset node_map + let create initial_capacity = {id_map= IdMap.create initial_capacity; node_map= NodeMap.create initial_capacity} @@ -80,7 +83,8 @@ let get_or_set_id ({id_map} as graph) procname = match id_of_procname graph procname with | None -> let id = IdMap.length id_map in - IdMap.replace id_map procname id ; id + IdMap.replace id_map procname id ; + id | Some id -> id @@ -98,7 +102,8 @@ let get_or_init_node node_map id pname = node | None -> let new_node = Node.make id pname [] in - NodeMap.add node_map id new_node ; new_node + NodeMap.add node_map id new_node ; + new_node let add_edge ({node_map} as graph) ~pname ~successor_pname = @@ -135,7 +140,8 @@ let pp_dot fmt {node_map} = let to_dotty g filename = let outc = Filename.concat Config.results_dir filename |> Out_channel.create in let fmt = F.formatter_of_out_channel outc in - pp_dot fmt g ; Out_channel.close outc + pp_dot fmt g ; + Out_channel.close outc let iter_unflagged_leaves ~f g = diff --git a/infer/src/backend/InferAnalyze.ml b/infer/src/backend/InferAnalyze.ml index c1c17c04e..5058ca4e8 100644 --- a/infer/src/backend/InferAnalyze.ml +++ b/infer/src/backend/InferAnalyze.ml @@ -14,10 +14,15 @@ module L = Logging module CLOpt = CommandLineOption let clear_caches_except_lrus () = - Summary.OnDisk.clear_cache () ; Procname.SQLite.clear_cache () ; BufferOverrunUtils.clear_cache () + Summary.OnDisk.clear_cache () ; + Procname.SQLite.clear_cache () ; + BufferOverrunUtils.clear_cache () -let clear_caches () = Ondemand.LocalCache.clear () ; clear_caches_except_lrus () +let clear_caches () = + Ondemand.LocalCache.clear () ; + clear_caches_except_lrus () + let analyze_target : (TaskSchedulerTypes.target, Procname.t) Tasks.doer = let analyze_source_file exe_env source_file = @@ -173,7 +178,9 @@ let invalidate_changed_procedures changed_files = CallGraph.to_dotty reverse_callgraph "reverse_analysis_callgraph.dot" ; let invalidated_nodes = CallGraph.fold_flagged reverse_callgraph - ~f:(fun node acc -> SpecsFiles.delete node.pname ; acc + 1) + ~f:(fun node acc -> + SpecsFiles.delete node.pname ; + acc + 1 ) 0 in L.progress diff --git a/infer/src/backend/ProcLocker.ml b/infer/src/backend/ProcLocker.ml index d81bcace5..cf6c19320 100644 --- a/infer/src/backend/ProcLocker.ml +++ b/infer/src/backend/ProcLocker.ml @@ -15,7 +15,8 @@ let log_unlock_time = BackendStats.add_to_proc_locker_unlock_time let record_time_of ~f ~log_f = let ExecutionDuration.{result; execution_duration} = ExecutionDuration.timed_evaluate ~f in - log_f execution_duration ; result + log_f execution_duration ; + result let locks_dir = ResultsDir.get_path ProcnamesLocks @@ -24,7 +25,11 @@ let locks_target = locks_dir ^/ "locks_target" let create_file filename = Unix.openfile ~mode:[O_CREAT; O_RDONLY] filename |> Unix.close -let setup () = Utils.rmtree locks_dir ; Utils.create_dir locks_dir ; create_file locks_target +let setup () = + Utils.rmtree locks_dir ; + Utils.create_dir locks_dir ; + create_file locks_target + let clean () = () diff --git a/infer/src/backend/Procedures.ml b/infer/src/backend/Procedures.ml index 533ccca71..bdb093a0c 100644 --- a/infer/src/backend/Procedures.ml +++ b/infer/src/backend/Procedures.ml @@ -45,7 +45,8 @@ let select_proc_names_interactive ~filter = | Some n when 0 <= n && n < Array.length proc_names_array -> Some [proc_names_array.(n)] | _ -> - print_endline "Invalid input" ; ask_user_input () + print_endline "Invalid input" ; + ask_user_input () in ask_user_input () diff --git a/infer/src/backend/RestartScheduler.ml b/infer/src/backend/RestartScheduler.ml index b745b96f6..d21ebb589 100644 --- a/infer/src/backend/RestartScheduler.ml +++ b/infer/src/backend/RestartScheduler.ml @@ -24,7 +24,8 @@ let of_list (lst : work_with_dependency list) : ('a, Procname.t) ProcessPool.Tas let work_if_dependency_allows w = match w.need_to_finish with | Some pname when ProcLocker.is_locked pname -> - Queue.enqueue content w ; None + Queue.enqueue content w ; + None | None | Some _ -> Some w.work in @@ -107,7 +108,8 @@ let unlock pname = caller.callees_useful <- ExecutionDuration.add_duration_since caller.callees_useful start | None -> - add_to_useful_time start ; add_to_total_time start ) ; + add_to_useful_time start ; + add_to_total_time start ) ; ProcLocker.unlock pname ) diff --git a/infer/src/backend/SpecsFiles.ml b/infer/src/backend/SpecsFiles.ml index 70f2f1c04..749882d1c 100644 --- a/infer/src/backend/SpecsFiles.ml +++ b/infer/src/backend/SpecsFiles.ml @@ -43,7 +43,9 @@ let spec_files_from_cmdline () = if (not (Filename.check_suffix arg Config.specs_files_suffix)) && not (String.equal arg ".") then print_usage_exit ("file " ^ arg ^ ": arguments must be .specs files") ) Config.anon_args ; - if Config.test_filtering then (Inferconfig.test () ; L.exit 0) ; + if Config.test_filtering then ( + Inferconfig.test () ; + L.exit 0 ) ; if List.is_empty Config.anon_args then load_specfiles () else List.rev Config.anon_args ) else load_specfiles () diff --git a/infer/src/backend/Tasks.ml b/infer/src/backend/Tasks.ml index f6e9f4eee..461412792 100644 --- a/infer/src/backend/Tasks.ml +++ b/infer/src/backend/Tasks.ml @@ -9,7 +9,10 @@ open! IStd type ('a, 'b) doer = 'a -> 'b option -let fork_protect ~f x = BackendStats.reset () ; ForkUtils.protect ~f x +let fork_protect ~f x = + BackendStats.reset () ; + ForkUtils.protect ~f x + let with_new_db_connection ~f () = ResultsDatabase.new_database_connection () ; @@ -59,4 +62,5 @@ let run_sequentially ~(f : ('a, 'b) doer) (tasks : 'a list) : unit = TaskBar.refresh task_bar ; run_tasks () ) in - run_tasks () ; TaskBar.finish task_bar + run_tasks () ; + TaskBar.finish task_bar diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index c9ffff6f4..126cd1f33 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -179,7 +179,8 @@ let run_proc_analysis ~caller_pdesc callee_pdesc = if Config.debug_mode then DotCfg.emit_proc_desc (Procdesc.get_attributes callee_pdesc).translation_unit callee_pdesc ; let initial_callee_summary = Summary.OnDisk.reset callee_pdesc in - add_active callee_pname ; initial_callee_summary + add_active callee_pname ; + initial_callee_summary in let postprocess summary = decr nesting ; @@ -223,7 +224,9 @@ let run_proc_analysis ~caller_pdesc callee_pdesc = IExn.reraise_if exn ~f:(fun () -> match exn with | TaskSchedulerTypes.ProcnameAlreadyLocked _ -> - clear_actives () ; restore_global_state old_state ; true + clear_actives () ; + restore_global_state old_state ; + true | _ -> if not !logged_error then ( let source_file = attributes.ProcAttributes.translation_unit in diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index a2b10398b..0748f4dd4 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -162,7 +162,8 @@ end = struct with Caml.Not_found -> Hashtbl.add err_per_line err_data.loc.Location.line (String.Set.singleton err_str) in - Errlog.iter add_err err_log ; err_per_line + Errlog.iter add_err err_log ; + err_per_line (** Create error message for html file *) @@ -287,7 +288,8 @@ end = struct fun node -> let file = (Procdesc.Node.get_loc node).Location.file in if not (Hashtbl.mem written_files file) then ( - write_all_html_files file ; Hashtbl.add written_files file () ) + write_all_html_files file ; + Hashtbl.add written_files file () ) end (* =============== Printing functions =============== *) diff --git a/infer/src/base/CommandLineOption.ml b/infer/src/base/CommandLineOption.ml index 630604a5e..a61facc90 100644 --- a/infer/src/base/CommandLineOption.ml +++ b/infer/src/base/CommandLineOption.ml @@ -1001,7 +1001,8 @@ let parse_args ~usage initial_action ?initial_command args = anymore *) assert false in - parse_loop () ; curr_usage + parse_loop () ; + curr_usage let keep_args_file = ref false diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 01c4b7710..edd0e3a78 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -399,7 +399,8 @@ let implicit_sdk_root = | None -> let maybe_root = locate_sdk_root () in let putenv x = Unix.putenv ~key:infer_sdkroot_env_var ~data:x in - Option.iter ~f:putenv maybe_root ; maybe_root ) + Option.iter ~f:putenv maybe_root ; + maybe_root ) let startup_action = @@ -1067,7 +1068,9 @@ and ( biabduction_models_mode [only_cheap_debug] and (_ : int option ref) = CLOpt.mk_int_opt ~long:"debug-level" ~in_help:all_generic_manuals ~meta:"level" - ~f:(fun level -> set_debug_level level ; level) + ~f:(fun level -> + set_debug_level level ; + level ) {|Debug level (sets $(b,--bo-debug) $(i,level), $(b,--debug-level-analysis) $(i,level), $(b,--debug-level-capture) $(i,level), $(b,--debug-level-linters) $(i,level)): - 0: only basic debugging enabled - 1: verbose debugging enabled @@ -1167,7 +1170,8 @@ and () = CLOpt.mk_string_list ?deprecated ~long ~f:(fun issue_id -> let issue = IssueType.register_from_string issue_id in - IssueType.set_enabled issue b ; issue_id ) + IssueType.set_enabled issue b ; + issue_id ) ?default ~meta:"issue_type" ~default_to_string:(fun _ -> "") ~in_help:InferCommand.[(Report, manual_generic)] @@ -2370,7 +2374,8 @@ let post_parsing_initialization command_opt = ( match !version with | `Full when !buck -> (* Buck reads stderr in some versions, stdout in others *) - print_endline version_string ; prerr_endline version_string + print_endline version_string ; + prerr_endline version_string | `Javac when !buck -> (* print buck key *) let infer_version = @@ -3131,7 +3136,10 @@ let is_in_custom_symbols list_name symbol = false -let execution_id = Random.self_init () ; Random.int64 Int64.max_value +let execution_id = + Random.self_init () ; + Random.int64 Int64.max_value + let toplevel_results_dir = if CLOpt.is_originator then ( diff --git a/infer/src/base/DB.ml b/infer/src/base/DB.ml index 887e700fd..59e41b1bc 100644 --- a/infer/src/base/DB.ml +++ b/infer/src/base/DB.ml @@ -148,10 +148,12 @@ module Results_dir = struct let rec create = function | [] -> let fname = path_to_filename pk [] in - Utils.create_dir fname ; fname + Utils.create_dir fname ; + fname | name :: names -> let new_path = Filename.concat (create names) name in - Utils.create_dir new_path ; new_path + Utils.create_dir new_path ; + new_path in let filename, dir_path = match List.rev path with diff --git a/infer/src/base/DBWriter.ml b/infer/src/base/DBWriter.ml index ce072d483..b2cac7e63 100644 --- a/infer/src/base/DBWriter.ml +++ b/infer/src/base/DBWriter.ml @@ -288,7 +288,11 @@ module Server = struct the number of workers, though even that is a guess. *) Unix.listen socket ~backlog:Config.jobs ; L.debug Analysis Quiet "Sqlite write daemon: set up complete, waiting for connections@." ; - let shutdown () = in_results_dir ~f:(fun () -> Unix.close socket ; Unix.remove socket_name) in + let shutdown () = + in_results_dir ~f:(fun () -> + Unix.close socket ; + Unix.remove socket_name ) + in Utils.try_finally_swallow_timeout ~f:(fun () -> server_loop socket) ~finally:shutdown @@ -311,7 +315,8 @@ module Server = struct let start () = match Unix.fork () with | `In_the_child -> - ForkUtils.protect ~f:server () ; L.exit 0 + ForkUtils.protect ~f:server () ; + L.exit 0 | `In_the_parent _child_pid -> (* wait for socket to appear, try 5 times, with a 0.1 sec timeout each time ; choice of numbers is completely arbitrary *) diff --git a/infer/src/base/Epilogues.ml b/infer/src/base/Epilogues.ml index a6c2cf1cd..82ec3f7fa 100644 --- a/infer/src/base/Epilogues.ml +++ b/infer/src/base/Epilogues.ml @@ -19,7 +19,10 @@ let register callback_ref ~f ~description = (Unix.getpid ()) description Exn.pp exn in let g = !callback_ref in - callback_ref := fun () -> f_no_exn () ; g () + callback_ref := + fun () -> + f_no_exn () ; + g () let register_early ~f ~description = register early_callback ~f ~description @@ -30,7 +33,10 @@ let early () = !early_callback () let late () = !late_callback () -let run () = early () ; late () +let run () = + early () ; + late () + (* Run the epilogues when we get SIGINT (Control-C). *) let () = diff --git a/infer/src/base/LineReader.ml b/infer/src/base/LineReader.ml index a7d4e6b44..23038ba00 100644 --- a/infer/src/base/LineReader.ml +++ b/infer/src/base/LineReader.ml @@ -29,7 +29,9 @@ let read_file fname = lines := line :: !lines done ; assert false (* execution never reaches here *) - with End_of_file -> In_channel.close cin ; Array.of_list_rev !lines + with End_of_file -> + In_channel.close cin ; + Array.of_list_rev !lines let file_data (hash : t) fname = @@ -37,7 +39,8 @@ let file_data (hash : t) fname = with Caml.Not_found -> ( try let lines_arr = read_file (SourceFile.to_abs_path fname) in - Hashtbl.add hash fname lines_arr ; Some lines_arr + Hashtbl.add hash fname lines_arr ; + Some lines_arr with exn when SymOp.exn_not_failure exn -> None ) diff --git a/infer/src/base/Logging.ml b/infer/src/base/Logging.ml index 3f67c0833..0df5ec65f 100644 --- a/infer/src/base/Logging.ml +++ b/infer/src/base/Logging.ml @@ -30,11 +30,26 @@ let dup_formatter fmt1 fmt2 = let out_funs2 = F.pp_get_formatter_out_functions fmt2 () in let f = copy_formatter fmt1 in F.pp_set_formatter_out_functions f - { F.out_string= (fun s p n -> out_funs1.out_string s p n ; out_funs2.out_string s p n) - ; out_indent= (fun n -> out_funs1.out_indent n ; out_funs2.out_indent n) - ; out_flush= (fun () -> out_funs1.out_flush () ; out_funs2.out_flush ()) - ; out_newline= (fun () -> out_funs1.out_newline () ; out_funs2.out_newline ()) - ; out_spaces= (fun n -> out_funs1.out_spaces n ; out_funs2.out_spaces n) } ; + { F.out_string= + (fun s p n -> + out_funs1.out_string s p n ; + out_funs2.out_string s p n ) + ; out_indent= + (fun n -> + out_funs1.out_indent n ; + out_funs2.out_indent n ) + ; out_flush= + (fun () -> + out_funs1.out_flush () ; + out_funs2.out_flush () ) + ; out_newline= + (fun () -> + out_funs1.out_newline () ; + out_funs2.out_newline () ) + ; out_spaces= + (fun n -> + out_funs1.out_spaces n ; + out_funs2.out_spaces n ) } ; f @@ -73,13 +88,19 @@ let mk_file_formatter file_fmt category0 = print_prefix_if_newline () ; out_functions_orig.out_string s p n in - let out_indent n = print_prefix_if_newline () ; out_functions_orig.out_indent n in + let out_indent n = + print_prefix_if_newline () ; + out_functions_orig.out_indent n + in let out_newline () = print_prefix_if_newline () ; out_functions_orig.out_newline () ; is_newline := true in - let out_spaces n = print_prefix_if_newline () ; out_functions_orig.out_spaces n in + let out_spaces n = + print_prefix_if_newline () ; + out_functions_orig.out_spaces n + in F.pp_set_formatter_out_functions f {F.out_string; out_flush= out_functions_orig.out_flush; out_indent; out_newline; out_spaces} ; f @@ -163,7 +184,8 @@ let close_logs () = let close_fmt (_, formatters) = flush_formatters formatters in List.iter ~f:close_fmt !logging_formatters ; Option.iter !log_file ~f:(function file_fmt, chan -> - F.pp_print_flush file_fmt () ; Out_channel.close chan ) + F.pp_print_flush file_fmt () ; + Out_channel.close chan ) let () = Epilogues.register ~f:close_logs ~description:"flushing logs and closing log file" @@ -216,7 +238,8 @@ let log_task fmt = let task_progress ~f pp x = log_task "%a starting@." pp x ; let result = f () in - log_task "%a DONE@." pp x ; result + log_task "%a DONE@." pp x ; + result let user_warning fmt = log ~to_console:(not Config.quiet) user_warning_file_fmts fmt @@ -372,7 +395,8 @@ let reset_delayed_prints () = delayed_prints := new_delayed_prints () (** return the delayed prints *) let get_and_reset_delayed_prints () = let res = !delayed_prints in - reset_delayed_prints () ; res + reset_delayed_prints () ; + res let force_and_reset_delayed_prints f = @@ -394,7 +418,11 @@ let d_kfprintf ?color k f fmt = match color with | Some color when Config.write_html -> F.fprintf f "" (Pp.color_string color) ; - F.kfprintf (fun f -> F.pp_print_string f "" ; k f) f fmt + F.kfprintf + (fun f -> + F.pp_print_string f "" ; + k f ) + f fmt | _ -> F.kfprintf k f fmt diff --git a/infer/src/base/ProcessPool.ml b/infer/src/base/ProcessPool.ml index 21d2a0932..57c595ea2 100644 --- a/infer/src/base/ProcessPool.ml +++ b/infer/src/base/ProcessPool.ml @@ -308,7 +308,8 @@ let collect_results (pool : (_, 'final, _) t) = let wait_all pool = (* tell each alive worker to go home *) Array.iter pool.slots ~f:(fun {down_pipe} -> - marshal_to_pipe down_pipe GoHome ; Out_channel.close down_pipe ) ; + marshal_to_pipe down_pipe GoHome ; + Out_channel.close down_pipe ) ; let results = collect_results pool in (* wait(2) workers one by one; the order doesn't matter since we want to wait for all of them eventually anyway. *) @@ -458,10 +459,12 @@ let run pool = let buffer = Bytes.create buffer_size in (* wait for all children to run out of tasks *) while not (pool.tasks.is_empty () && all_children_idle pool) do - process_updates pool buffer ; TaskBar.refresh pool.task_bar + process_updates pool buffer ; + TaskBar.refresh pool.task_bar done ; let results = wait_all pool in - TaskBar.finish pool.task_bar ; results ) + TaskBar.finish pool.task_bar ; + results ) let run pool = diff --git a/infer/src/base/ScubaLogging.ml b/infer/src/base/ScubaLogging.ml index dedde1ccf..db1986d6b 100644 --- a/infer/src/base/ScubaLogging.ml +++ b/infer/src/base/ScubaLogging.ml @@ -75,7 +75,8 @@ let log_message ~label ~message = log_one (LogEntry.mk_string ~label ~message) let execute_with_time_logging label f = let ret_val, duration_ms = Utils.timeit ~f in let entry = LogEntry.mk_time ~label ~duration_ms in - log_one entry ; ret_val + log_one entry ; + ret_val let flush_log_events () = diff --git a/infer/src/base/SymOp.ml b/infer/src/base/SymOp.ml index dde00954f..5171e2b21 100644 --- a/infer/src/base/SymOp.ml +++ b/infer/src/base/SymOp.ml @@ -25,7 +25,8 @@ let exn_not_failure = function Analysis_failure_exe _ -> false | _ -> true let try_finally ~f ~finally = match f () with | r -> - finally () ; r + finally () ; + r | exception (Analysis_failure_exe _ as f_exn) -> IExn.reraise_after f_exn ~f:(fun () -> try finally () with _ -> (* swallow in favor of the original exception *) () ) @@ -112,7 +113,8 @@ let unset_wallclock_alarm () = !gs.last_wallclock <- None let check_wallclock_alarm () = match (!gs.last_wallclock, !wallclock_timeout_handler) with | Some alarm_time, Some handler when Float.(Unix.gettimeofday () >= alarm_time) -> - unset_wallclock_alarm () ; handler () + unset_wallclock_alarm () ; + handler () | _ -> () diff --git a/infer/src/base/TaskBar.ml b/infer/src/base/TaskBar.ml index 4ff9d5128..7b1de9ffa 100644 --- a/infer/src/base/TaskBar.ml +++ b/infer/src/base/TaskBar.ml @@ -144,7 +144,8 @@ let create ~jobs = ; tasks_done= 0 ; tasks_total= 0 } in - ANSITerminal.erase Below ; MultiLine task_bar + ANSITerminal.erase Below ; + MultiLine task_bar let update_status_multiline task_bar ~slot:job t0 status = diff --git a/infer/src/base/Utils.ml b/infer/src/base/Utils.ml index 41db5ffa8..c0b5a9640 100644 --- a/infer/src/base/Utils.ml +++ b/infer/src/base/Utils.ml @@ -66,7 +66,8 @@ let read_file fname = cleanup () ; Ok (List.rev !res) | Sys_error error -> - cleanup () ; Error error + cleanup () ; + Error error (** type for files used for printing *) @@ -223,7 +224,11 @@ let create_file_lock () = let with_file_lock ~file_lock:{file; oc; fd} ~f = - let finally () = Core.Unix.close fd ; Out_channel.close oc ; Core.Unix.remove file in + let finally () = + Core.Unix.close fd ; + Out_channel.close oc ; + Core.Unix.remove file + in try_finally_swallow_timeout ~f ~finally @@ -256,7 +261,10 @@ let echo_in chan_in = with_channel_in ~f:print_endline chan_in let with_process_in command read = let chan = Unix.open_process_in command in let f () = read chan in - let finally () = consume_in chan ; Unix.close_process_in chan in + let finally () = + consume_in chan ; + Unix.close_process_in chan + in do_finally_swallow_timeout ~f ~finally @@ -310,7 +318,10 @@ let realpath ?(warn_on_error = true) path = let devnull = lazy (Unix.openfile "/dev/null" ~mode:[Unix.O_WRONLY]) let suppress_stderr2 f2 x1 x2 = - let restore_stderr src = Unix.dup2 ~src ~dst:Unix.stderr ; Unix.close src in + let restore_stderr src = + Unix.dup2 ~src ~dst:Unix.stderr ; + Unix.close src + in let orig_stderr = Unix.dup Unix.stderr in Unix.dup2 ~src:(Lazy.force devnull) ~dst:Unix.stderr ; let f () = f2 x1 x2 in @@ -343,7 +354,8 @@ let rec rmtree name = then rmtree (name ^/ entry) ; rmdir dir | None -> - Unix.closedir dir ; Unix.rmdir name + Unix.closedir dir ; + Unix.rmdir name in rmdir dir | _ -> @@ -505,4 +517,5 @@ let zip_fold_filenames ~init ~f ~zip_filename = let file_in = Zip.open_in zip_filename in let collect acc (entry : Zip.entry) = f acc entry.filename in let result = List.fold ~f:collect ~init (Zip.entries file_in) in - Zip.close_in file_in ; result + Zip.close_in file_in ; + result diff --git a/infer/src/biabduction/Abs.ml b/infer/src/biabduction/Abs.ml index fa5744509..3e8d2a549 100644 --- a/infer/src/biabduction/Abs.ml +++ b/infer/src/biabduction/Abs.ml @@ -560,7 +560,8 @@ let discover_para_candidates tenv p = get_edges_sigma sigma_rest | Predicates.Hpointsto (root, se, te) :: sigma_rest -> let rec_flds = typ_get_recursive_flds tenv te in - get_edges_strexp rec_flds root se ; get_edges_sigma sigma_rest + get_edges_strexp rec_flds root se ; + get_edges_sigma sigma_rest in let rec find_all_consecutive_edges found edges_seen = function | [] -> @@ -610,7 +611,8 @@ let discover_para_dll_candidates tenv p = get_edges_sigma sigma_rest | Predicates.Hpointsto (root, se, te) :: sigma_rest -> let rec_flds = typ_get_recursive_flds tenv te in - get_edges_strexp rec_flds root se ; get_edges_sigma sigma_rest + get_edges_strexp rec_flds root se ; + get_edges_sigma sigma_rest in let rec find_all_consecutive_edges found edges_seen = function | [] -> @@ -859,7 +861,8 @@ let abs_rules_apply_lists tenv (p_in : Prop.normal Prop.t) : Prop.normal Prop.t let p1 = abs_rules_apply_rsets tenv old_rsets p_in in let p2 = discover_then_abstract p1 in let new_rules = old_rsets @ !new_rsets in - set_current_rules new_rules ; p2 + set_current_rules new_rules ; + p2 let abs_rules_apply tenv (p_in : Prop.normal Prop.t) : Prop.normal Prop.t = @@ -1065,7 +1068,8 @@ let check_junk {InterproceduralAnalysis.proc_desc; err_log; tenv} prop = | _ -> () ) ) in - List.iter ~f:do_entry entries ; !res + List.iter ~f:do_entry entries ; + !res in L.d_decrease_indent () ; let is_undefined = diff --git a/infer/src/biabduction/Absarray.ml b/infer/src/biabduction/Absarray.ml index 7bd3e1958..c5d231bc0 100644 --- a/infer/src/biabduction/Absarray.ml +++ b/infer/src/biabduction/Absarray.ml @@ -222,7 +222,8 @@ end = struct () ) ; iterate (hpred :: sigma_seen) sigma_rest in - iterate [] sigma ; !found + iterate [] sigma ; + !found (** Get the matched strexp *) @@ -508,16 +509,26 @@ let strexp_do_abstract tenv footprint_part p ((path, se_in, _) : StrexpMatch.str if Config.trace_absarray && not footprint_part then L.d_strln "strexp_do_abstract (nonfootprint)" ; let prune_and_blur d_keys keep blur path keep_keys blur_keys = let p2, changed2 = - if Config.trace_absarray then (L.d_str "keep " ; d_keys keep_keys ; L.d_ln ()) ; + if Config.trace_absarray then ( + L.d_str "keep " ; + d_keys keep_keys ; + L.d_ln () ) ; keep p path keep_keys in let p3, changed3 = if List.is_empty blur_keys then (p2, false) else ( - if Config.trace_absarray then (L.d_str "blur " ; d_keys blur_keys ; L.d_ln ()) ; + if Config.trace_absarray then ( + L.d_str "blur " ; + d_keys blur_keys ; + L.d_ln () ) ; blur p2 path blur_keys ) in - if Config.trace_absarray then (L.d_strln "Returns" ; Prop.d_prop p3 ; L.d_ln () ; L.d_ln ()) ; + if Config.trace_absarray then ( + L.d_strln "Returns" ; + Prop.d_prop p3 ; + L.d_ln () ; + L.d_ln () ) ; (p3, changed2 || changed3) in let prune_and_blur_indices = @@ -548,7 +559,10 @@ let strexp_do_abstract tenv footprint_part p ((path, se_in, _) : StrexpMatch.str let keep_ksel = List.filter ~f:should_keep ksel in let keep_keys = List.map ~f:fst keep_ksel in let keep_keys' = if List.is_empty keep_keys then default_keys else keep_keys in - if Config.trace_absarray then (L.d_str "keep " ; d_keys keep_keys' ; L.d_ln ()) ; + if Config.trace_absarray then ( + L.d_str "keep " ; + d_keys keep_keys' ; + L.d_ln () ) ; abstract keep_keys' [] in let do_array_reexecution esel = @@ -625,7 +639,8 @@ let check_after_array_abstraction tenv prop = in let check_sigma sigma = List.iter ~f:check_hpred sigma in (* check_footprint_pure prop; *) - check_sigma prop.Prop.sigma ; check_sigma prop.Prop.sigma_fp + check_sigma prop.Prop.sigma ; + check_sigma prop.Prop.sigma_fp (** Apply array abstraction and check the result *) diff --git a/infer/src/biabduction/Attribute.ml b/infer/src/biabduction/Attribute.ml index 573ef89b4..238f902c1 100644 --- a/infer/src/biabduction/Attribute.ml +++ b/infer/src/biabduction/Attribute.ml @@ -35,7 +35,8 @@ let add_or_replace_check_changed tenv check_attribute_change prop atom = let atom_map = function | (Predicates.Apred (att, exp :: _) | Anpred (att, exp :: _)) when Exp.equal nexp exp && attributes_in_same_category att att0 -> - check_attribute_change att att0 ; atom + check_attribute_change att att0 ; + atom | atom' -> atom' in @@ -57,7 +58,8 @@ let add_or_replace tenv prop atom = let get_all (prop : 'a Prop.t) = let res = ref [] in let do_atom a = if is_pred a then res := a :: !res in - List.iter ~f:do_atom prop.pi ; List.rev !res + List.iter ~f:do_atom prop.pi ; + List.rev !res (** Get the attribute associated to the expression, if any *) @@ -258,7 +260,8 @@ let find_arithmetic_problem tenv proc_node_session prop exp = | Exp.Lfield (e, _, _) -> walk e | Exp.Lindex (e1, e2) -> - walk e1 ; walk e2 + walk e1 ; + walk e2 | Exp.Sizeof {dynamic_length= None} -> () | Exp.Sizeof {dynamic_length= Some len} -> diff --git a/infer/src/biabduction/Builtin.ml b/infer/src/biabduction/Builtin.ml index 9f9a1707a..4d0f22775 100644 --- a/infer/src/biabduction/Builtin.ml +++ b/infer/src/biabduction/Builtin.ml @@ -38,7 +38,9 @@ let check_register_populated () = (** get the symbolic execution handler associated to the builtin function name *) let get name : t option = try Some (Procname.Hash.find builtin_functions name) - with Caml.Not_found -> check_register_populated () ; None + with Caml.Not_found -> + check_register_populated () ; + None (** register a builtin [Procname.t] and symbolic execution handler *) diff --git a/infer/src/biabduction/Dom.ml b/infer/src/biabduction/Dom.ml index b878d534c..7139cd9a7 100644 --- a/infer/src/biabduction/Dom.ml +++ b/infer/src/biabduction/Dom.ml @@ -29,10 +29,13 @@ let equal_sigma sigma1 sigma2 = | [], [] -> () | [], _ :: _ | _ :: _, [] -> - L.d_strln "failure reason 1" ; raise Predicates.JoinFail + L.d_strln "failure reason 1" ; + raise Predicates.JoinFail | hpred1 :: sigma1_rest', hpred2 :: sigma2_rest' -> if Predicates.equal_hpred hpred1 hpred2 then f sigma1_rest' sigma2_rest' - else (L.d_strln "failure reason 2" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 2" ; + raise Predicates.JoinFail ) in let sigma1_sorted = List.sort ~compare:Predicates.compare_hpred sigma1 in let sigma2_sorted = List.sort ~compare:Predicates.compare_hpred sigma2 in @@ -91,7 +94,10 @@ end = struct let lookup' tbl e default = match e with | Exp.Var _ -> ( - try Hashtbl.find tbl e with Caml.Not_found -> Hashtbl.replace tbl e default ; default ) + try Hashtbl.find tbl e + with Caml.Not_found -> + Hashtbl.replace tbl e default ; + default ) | _ -> assert false @@ -107,7 +113,8 @@ end = struct if Exp.equal e e' then e else let root = find' tbl e' in - Hashtbl.replace tbl e root ; root + Hashtbl.replace tbl e root ; + root | _ -> assert false @@ -119,7 +126,9 @@ end = struct let new_c = lookup_const' const_tbl new_r in let old_c = lookup_const' const_tbl old_r in let res_c = Exp.Set.union new_c old_c in - if Exp.Set.cardinal res_c > 1 then (L.d_strln "failure reason 3" ; raise Predicates.JoinFail) ; + if Exp.Set.cardinal res_c > 1 then ( + L.d_strln "failure reason 3" ; + raise Predicates.JoinFail ) ; Hashtbl.replace tbl old_r new_r ; Hashtbl.replace const_tbl new_r res_c @@ -127,7 +136,9 @@ end = struct let replace_const' tbl const_tbl e c = let r = find' tbl e in let set = Exp.Set.add c (lookup_const' const_tbl r) in - if Exp.Set.cardinal set > 1 then (L.d_strln "failure reason 4" ; raise Predicates.JoinFail) ; + if Exp.Set.cardinal set > 1 then ( + L.d_strln "failure reason 4" ; + raise Predicates.JoinFail ) ; Hashtbl.replace const_tbl r set @@ -145,15 +156,22 @@ end = struct | false, true -> replace_const' tbl const_tbl e' e | _ -> - L.d_strln "failure reason 5" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 5" ; + raise Predicates.JoinFail ) | Exp.Var id, Exp.Const _ | Exp.Var id, Exp.Lvar _ -> if can_rename id then replace_const' tbl const_tbl e e' - else (L.d_strln "failure reason 6" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 6" ; + raise Predicates.JoinFail ) | Exp.Const _, Exp.Var id' | Exp.Lvar _, Exp.Var id' -> if can_rename id' then replace_const' tbl const_tbl e' e - else (L.d_strln "failure reason 7" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 7" ; + raise Predicates.JoinFail ) | _ -> - if not (Exp.equal e e') then (L.d_strln "failure reason 8" ; raise Predicates.JoinFail) + if not (Exp.equal e e') then ( + L.d_strln "failure reason 8" ; + raise Predicates.JoinFail ) else () @@ -228,9 +246,15 @@ end = struct end module CheckJoinPre : InfoLossCheckerSig = struct - let init sigma1 sigma2 = NonInj.init () ; Dangling.init sigma1 sigma2 + let init sigma1 sigma2 = + NonInj.init () ; + Dangling.init sigma1 sigma2 + + + let final () = + NonInj.final () ; + Dangling.final () - let final () = NonInj.final () ; Dangling.final () let fail_case side e es = let side_op = opposite side in @@ -607,7 +631,8 @@ end = struct | _ -> () in - List.iter ~f !tbl ; List.rev !res + List.iter ~f !tbl ; + List.rev !res (* Return the triple whose side is [e], if it exists unique *) @@ -620,12 +645,14 @@ end = struct if todo then Todo.push t ; id | _ -> - L.d_strln "failure reason 9" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 9" ; + raise Predicates.JoinFail ) | Exp.Var _ | Exp.Const _ | Exp.Lvar _ -> if todo then Todo.push (e, e, e) ; e | _ -> - L.d_strln "failure reason 10" ; raise Predicates.JoinFail + L.d_strln "failure reason 10" ; + raise Predicates.JoinFail let lookup side e = lookup' false side e @@ -657,7 +684,8 @@ end = struct false in if find_duplicates sub_list_side_sorted then ( - L.d_strln "failure reason 11" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 11" ; + raise Predicates.JoinFail ) else Predicates.subst_of_list sub_list_side @@ -752,7 +780,10 @@ end = struct let get_other_atoms tenv side atom_in = let build_other_atoms construct side e = - if Config.trace_join then (L.d_str "build_other_atoms: " ; Exp.d_exp e ; L.d_ln ()) ; + if Config.trace_join then ( + L.d_str "build_other_atoms: " ; + Exp.d_exp e ; + L.d_ln () ) ; let others1 = get_others_direct_or_induced side e in let others2 = match others1 with None -> get_others_deep side e | Some _ -> others1 in match others2 with @@ -829,7 +860,9 @@ end = struct && not (Exp.free_vars e2 |> Sequence.exists ~f:can_rename) then if Exp.equal e1 e2 then e1 - else (L.d_strln "failure reason 13" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 13" ; + raise Predicates.JoinFail ) else match default_op with | ExtDefault e -> @@ -842,7 +875,9 @@ end = struct Exp.Var (Ident.create_fresh kind) in let entry = (e1, e2, e) in - push entry ; Todo.push entry ; e + push entry ; + Todo.push entry ; + e end (** {2 Functions for constructing fresh sil data types} *) @@ -917,12 +952,15 @@ let ident_partial_join (id1 : Ident.t) (id2 : Ident.t) = match (Ident.is_normal id1, Ident.is_normal id2) with | true, true -> if Ident.equal id1 id2 then Exp.Var id1 - else (L.d_strln "failure reason 14" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 14" ; + raise Predicates.JoinFail ) | true, _ | _, true -> Rename.extend (Exp.Var id1) (Exp.Var id2) Rename.ExtFresh | _ -> if not (ident_same_kind_primed_footprint id1 id2) then ( - L.d_strln "failure reason 15" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 15" ; + raise Predicates.JoinFail ) else let e1 = Exp.Var id1 in let e2 = Exp.Var id2 in @@ -933,7 +971,9 @@ let ident_partial_meet (id1 : Ident.t) (id2 : Ident.t) = match (Ident.is_normal id1, Ident.is_normal id2) with | true, true -> if Ident.equal id1 id2 then Exp.Var id1 - else (L.d_strln "failure reason 16" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 16" ; + raise Predicates.JoinFail ) | true, _ -> let e1, e2 = (Exp.Var id1, Exp.Var id2) in Rename.extend e1 e2 (Rename.ExtDefault e1) @@ -946,7 +986,9 @@ let ident_partial_meet (id1 : Ident.t) (id2 : Ident.t) = else if Ident.is_footprint id1 && Ident.equal id1 id2 then let e = Exp.Var id1 in Rename.extend e e (Rename.ExtDefault e) - else (L.d_strln "failure reason 17" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 17" ; + raise Predicates.JoinFail ) (** {2 Join and Meet for Exps} *) @@ -959,10 +1001,13 @@ let const_partial_join c1 c2 = let is_int = function Const.Cint _ -> true | _ -> false in if Const.equal c1 c2 then Exp.Const c1 else if Const.kind_equal c1 c2 && not (is_int c1) then ( - L.d_strln "failure reason 18" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 18" ; + raise Predicates.JoinFail ) else if !BiabductionConfig.abs_val >= 2 then FreshVarExp.get_fresh_exp (Exp.Const c1) (Exp.Const c2) - else (L.d_strln "failure reason 19" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 19" ; + raise Predicates.JoinFail ) let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t = @@ -971,12 +1016,16 @@ let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t = | Exp.Var id1, Exp.Var id2 -> ident_partial_join id1 id2 | Exp.Var id, Exp.Const _ | Exp.Const _, Exp.Var id -> - if Ident.is_normal id then (L.d_strln "failure reason 20" ; raise Predicates.JoinFail) + if Ident.is_normal id then ( + L.d_strln "failure reason 20" ; + raise Predicates.JoinFail ) else Rename.extend e1 e2 Rename.ExtFresh | Exp.Const c1, Exp.Const c2 -> const_partial_join c1 c2 | Exp.Var id, Exp.Lvar _ | Exp.Lvar _, Exp.Var id -> - if Ident.is_normal id then (L.d_strln "failure reason 21" ; raise Predicates.JoinFail) + if Ident.is_normal id then ( + L.d_strln "failure reason 21" ; + raise Predicates.JoinFail ) else Rename.extend e1 e2 Rename.ExtFresh | Exp.BinOp (Binop.PlusA _, Exp.Var id1, Exp.Const _), Exp.Var id2 | Exp.Var id1, Exp.BinOp (Binop.PlusA _, Exp.Var id2, Exp.Const _) @@ -993,13 +1042,16 @@ let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t = let e_res = Rename.extend (Exp.int c1') (Exp.Var id2) Rename.ExtFresh in Exp.BinOp (Binop.PlusA None, e_res, Exp.int c2) | Exp.Cast (t1, e1), Exp.Cast (t2, e2) -> - if not (Typ.equal t1 t2) then (L.d_strln "failure reason 22" ; raise Predicates.JoinFail) + if not (Typ.equal t1 t2) then ( + L.d_strln "failure reason 22" ; + raise Predicates.JoinFail ) else let e1'' = exp_partial_join e1 e2 in Exp.Cast (t1, e1'') | Exp.UnOp (unop1, e1, topt1), Exp.UnOp (unop2, e2, _) -> if not (Unop.equal unop1 unop2) then ( - L.d_strln "failure reason 23" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 23" ; + raise Predicates.JoinFail ) else Exp.UnOp (unop1, exp_partial_join e1 e2, topt1) (* should be topt1 = topt2 *) | Exp.BinOp (Binop.PlusPI, e1, e1'), Exp.BinOp (Binop.PlusPI, e2, e2') -> let e1'' = exp_partial_join e1 e2 in @@ -1013,18 +1065,21 @@ let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t = Exp.BinOp (Binop.PlusPI, e1'', e2'') | Exp.BinOp (binop1, e1, e1'), Exp.BinOp (binop2, e2, e2') -> if not (Binop.equal binop1 binop2) then ( - L.d_strln "failure reason 24" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 24" ; + raise Predicates.JoinFail ) else let e1'' = exp_partial_join e1 e2 in let e2'' = exp_partial_join e1' e2' in Exp.BinOp (binop1, e1'', e2'') | Exp.Lvar pvar1, Exp.Lvar pvar2 -> if not (Pvar.equal pvar1 pvar2) then ( - L.d_strln "failure reason 25" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 25" ; + raise Predicates.JoinFail ) else e1 | Exp.Lfield (e1, f1, t1), Exp.Lfield (e2, f2, _) -> if not (Fieldname.equal f1 f2) then ( - L.d_strln "failure reason 26" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 26" ; + raise Predicates.JoinFail ) else Exp.Lfield (exp_partial_join e1 e2, f1, t1) (* should be t1 = t2 *) | Exp.Lindex (e1, e1'), Exp.Lindex (e2, e2') -> let e1'' = exp_partial_join e1 e2 in @@ -1100,48 +1155,66 @@ let rec exp_partial_meet (e1 : Exp.t) (e2 : Exp.t) : Exp.t = ident_partial_meet id1 id2 | Exp.Var id, Exp.Const _ -> if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e2) - else (L.d_strln "failure reason 27" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 27" ; + raise Predicates.JoinFail ) | Exp.Const _, Exp.Var id -> if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e1) - else (L.d_strln "failure reason 28" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 28" ; + raise Predicates.JoinFail ) | Exp.Const c1, Exp.Const c2 -> - if Const.equal c1 c2 then e1 else (L.d_strln "failure reason 29" ; raise Predicates.JoinFail) + if Const.equal c1 c2 then e1 + else ( + L.d_strln "failure reason 29" ; + raise Predicates.JoinFail ) | Exp.Cast (t1, e1), Exp.Cast (t2, e2) -> - if not (Typ.equal t1 t2) then (L.d_strln "failure reason 30" ; raise Predicates.JoinFail) + if not (Typ.equal t1 t2) then ( + L.d_strln "failure reason 30" ; + raise Predicates.JoinFail ) else let e1'' = exp_partial_meet e1 e2 in Exp.Cast (t1, e1'') | Exp.UnOp (unop1, e1, topt1), Exp.UnOp (unop2, e2, _) -> if not (Unop.equal unop1 unop2) then ( - L.d_strln "failure reason 31" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 31" ; + raise Predicates.JoinFail ) else Exp.UnOp (unop1, exp_partial_meet e1 e2, topt1) (* should be topt1 = topt2 *) | Exp.BinOp (binop1, e1, e1'), Exp.BinOp (binop2, e2, e2') -> if not (Binop.equal binop1 binop2) then ( - L.d_strln "failure reason 32" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 32" ; + raise Predicates.JoinFail ) else let e1'' = exp_partial_meet e1 e2 in let e2'' = exp_partial_meet e1' e2' in Exp.BinOp (binop1, e1'', e2'') | Exp.Var id, Exp.Lvar _ -> if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e2) - else (L.d_strln "failure reason 33" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 33" ; + raise Predicates.JoinFail ) | Exp.Lvar _, Exp.Var id -> if not (Ident.is_normal id) then Rename.extend e1 e2 (Rename.ExtDefault e1) - else (L.d_strln "failure reason 34" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 34" ; + raise Predicates.JoinFail ) | Exp.Lvar pvar1, Exp.Lvar pvar2 -> if not (Pvar.equal pvar1 pvar2) then ( - L.d_strln "failure reason 35" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 35" ; + raise Predicates.JoinFail ) else e1 | Exp.Lfield (e1, f1, t1), Exp.Lfield (e2, f2, _) -> if not (Fieldname.equal f1 f2) then ( - L.d_strln "failure reason 36" ; raise Predicates.JoinFail ) + L.d_strln "failure reason 36" ; + raise Predicates.JoinFail ) else Exp.Lfield (exp_partial_meet e1 e2, f1, t1) (* should be t1 = t2 *) | Exp.Lindex (e1, e1'), Exp.Lindex (e2, e2') -> let e1'' = exp_partial_meet e1 e2 in let e2'' = exp_partial_meet e1' e2' in Exp.Lindex (e1'', e2'') | _ -> - L.d_strln "failure reason 37" ; raise Predicates.JoinFail + L.d_strln "failure reason 37" ; + raise Predicates.JoinFail let exp_list_partial_join = List.map2_exn ~f:exp_partial_join @@ -1159,7 +1232,8 @@ let rec strexp_partial_join mode (strexp1 : Predicates.strexp) (strexp2 : Predic | [], _ | _, [] -> ( match mode with | JoinState.Pre -> - L.d_strln "failure reason 42" ; raise Predicates.JoinFail + L.d_strln "failure reason 42" ; + raise Predicates.JoinFail | JoinState.Post -> Predicates.Estruct (List.rev acc, inst) ) | (fld1, se1) :: fld_se_list1', (fld2, se2) :: fld_se_list2' -> ( @@ -1171,7 +1245,8 @@ let rec strexp_partial_join mode (strexp1 : Predicates.strexp) (strexp2 : Predic else match mode with | JoinState.Pre -> - L.d_strln "failure reason 43" ; raise Predicates.JoinFail + L.d_strln "failure reason 43" ; + raise Predicates.JoinFail | JoinState.Post -> if comparison < 0 then f_fld_se_list inst mode acc fld_se_list1' fld_se_list2 else if comparison > 0 then f_fld_se_list inst mode acc fld_se_list1 fld_se_list2' @@ -1185,7 +1260,8 @@ let rec strexp_partial_join mode (strexp1 : Predicates.strexp) (strexp2 : Predic | [], _ | _, [] -> ( match mode with | JoinState.Pre -> - L.d_strln "failure reason 44" ; raise Predicates.JoinFail + L.d_strln "failure reason 44" ; + raise Predicates.JoinFail | JoinState.Post -> Predicates.Earray (len, List.rev idx_se_list_acc, inst) ) | (idx1, se1) :: idx_se_list1', (idx2, se2) :: idx_se_list2' -> @@ -1264,7 +1340,8 @@ let rec strexp_partial_meet (strexp1 : Predicates.strexp) (strexp2 : Predicates. let inst = Predicates.inst_partial_meet inst1 inst2 in f_idx_se_list inst len1 [] idx_se_list1 idx_se_list2 | _ -> - L.d_strln "failure reason 52" ; raise Predicates.JoinFail + L.d_strln "failure reason 52" ; + raise Predicates.JoinFail (** {2 Join and Meet for kind, hpara, hpara_dll} *) @@ -1281,28 +1358,36 @@ let hpara_partial_join tenv (hpara1 : Predicates.hpara) (hpara2 : Predicates.hpa Predicates.hpara = if Match.hpara_match_with_impl tenv true hpara2 hpara1 then hpara1 else if Match.hpara_match_with_impl tenv true hpara1 hpara2 then hpara2 - else (L.d_strln "failure reason 53" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 53" ; + raise Predicates.JoinFail ) let hpara_partial_meet tenv (hpara1 : Predicates.hpara) (hpara2 : Predicates.hpara) : Predicates.hpara = if Match.hpara_match_with_impl tenv true hpara2 hpara1 then hpara2 else if Match.hpara_match_with_impl tenv true hpara1 hpara2 then hpara1 - else (L.d_strln "failure reason 54" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 54" ; + raise Predicates.JoinFail ) let hpara_dll_partial_join tenv (hpara1 : Predicates.hpara_dll) (hpara2 : Predicates.hpara_dll) : Predicates.hpara_dll = if Match.hpara_dll_match_with_impl tenv true hpara2 hpara1 then hpara1 else if Match.hpara_dll_match_with_impl tenv true hpara1 hpara2 then hpara2 - else (L.d_strln "failure reason 55" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 55" ; + raise Predicates.JoinFail ) let hpara_dll_partial_meet tenv (hpara1 : Predicates.hpara_dll) (hpara2 : Predicates.hpara_dll) : Predicates.hpara_dll = if Match.hpara_dll_match_with_impl tenv true hpara2 hpara1 then hpara2 else if Match.hpara_dll_match_with_impl tenv true hpara1 hpara2 then hpara1 - else (L.d_strln "failure reason 56" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 56" ; + raise Predicates.JoinFail ) (** {2 Join and Meet for hpred} *) @@ -1327,7 +1412,9 @@ let hpred_partial_join tenv mode (todo : Exp.t * Exp.t * Exp.t) (hpred1 : Predic let iF', iB' = if fwd1 && fwd2 then (e, exp_partial_join iB1 iB2) else if (not fwd1) && not fwd2 then (exp_partial_join iF1 iF2, e) - else (L.d_strln "failure reason 57" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 57" ; + raise Predicates.JoinFail ) in let oF' = exp_partial_join oF1 oF2 in let oB' = exp_partial_join oB1 oB2 in @@ -1344,7 +1431,8 @@ let hpred_partial_meet tenv (todo : Exp.t * Exp.t * Exp.t) (hpred1 : Predicates. | Hpointsto (_, se1, te1), Hpointsto (_, se2, te2) when Exp.equal te1 te2 -> Prop.mk_ptsto tenv e (strexp_partial_meet se1 se2) te1 | Hpointsto _, _ | _, Hpointsto _ -> - L.d_strln "failure reason 58" ; raise Predicates.JoinFail + L.d_strln "failure reason 58" ; + raise Predicates.JoinFail | Hlseg (k1, hpara1, _, next1, shared1), Hlseg (k2, hpara2, _, next2, shared2) -> let hpara' = hpara_partial_meet tenv hpara1 hpara2 in let next' = exp_partial_meet next1 next2 in @@ -1358,7 +1446,9 @@ let hpred_partial_meet tenv (todo : Exp.t * Exp.t * Exp.t) (hpred1 : Predicates. let iF', iB' = if fwd1 && fwd2 then (e, exp_partial_meet iB1 iB2) else if (not fwd1) && not fwd2 then (exp_partial_meet iF1 iF2, e) - else (L.d_strln "failure reason 59" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 59" ; + raise Predicates.JoinFail ) in let oF' = exp_partial_meet oF1 oF2 in let oB' = exp_partial_meet oB1 oB2 in @@ -1426,7 +1516,8 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop let lookup_and_expand side e e' = match (Rename.get_others side e, side) with | None, _ -> - L.d_strln "failure reason 60" ; raise Predicates.JoinFail + L.d_strln "failure reason 60" ; + raise Predicates.JoinFail | Some (e_res, e_op), Lhs -> (e_res, exp_partial_join e' e_op) | Some (e_res, e_op), Rhs -> @@ -1487,7 +1578,9 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop 'todo' describes the start point. *) let cut_sigma side todo (target : Prop.sigma) (other : Prop.sigma) = let list_is_empty l = - if not (List.is_empty l) then (L.d_strln "failure reason 61" ; raise Predicates.JoinFail) + if not (List.is_empty l) then ( + L.d_strln "failure reason 61" ; + raise Predicates.JoinFail ) in let x = Todo.take () in Todo.push todo ; @@ -1504,7 +1597,8 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop sigma_renaming_check_rhs target res ; other' in - Todo.set x ; res + Todo.set x ; + res in let cut_lseg side todo lseg sigma = match (lseg : Predicates.hpred) with @@ -1551,15 +1645,20 @@ let rec sigma_partial_join' tenv mode (sigma_acc : Prop.sigma) (sigma1_in : Prop if (not Config.nelseg) || Predicates.equal_lseg_kind k Lseg_PE then let sigma_acc' = join_list_and_non Lhs e lseg e1 e2 :: sigma_acc in sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2 - else (L.d_strln "failure reason 62" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 62" ; + raise Predicates.JoinFail ) | None, Some (Predicates.Hlseg (k, _, _, _, _) as lseg) | None, Some (Predicates.Hdllseg (k, _, _, _, _, _, _) as lseg) -> if (not Config.nelseg) || Predicates.equal_lseg_kind k Lseg_PE then let sigma_acc' = join_list_and_non Rhs e lseg e2 e1 :: sigma_acc in sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2 - else (L.d_strln "failure reason 63" ; raise Predicates.JoinFail) + else ( + L.d_strln "failure reason 63" ; + raise Predicates.JoinFail ) | None, _ | _, None -> - L.d_strln "failure reason 64" ; raise Predicates.JoinFail + L.d_strln "failure reason 64" ; + raise Predicates.JoinFail | Some hpred1, Some hpred2 when same_pred hpred1 hpred2 -> let hpred_res1 = hpred_partial_join tenv mode todo_curr hpred1 hpred2 in sigma_partial_join' tenv mode (hpred_res1 :: sigma_acc) sigma1 sigma2 @@ -1622,7 +1721,9 @@ let sigma_partial_join tenv mode (sigma1 : Prop.sigma) (sigma2 : Prop.sigma) : SymOp.try_finally ~f:(fun () -> if Rename.check lost_little then (s1, s2, s3) - else (L.d_strln "failed Rename.check" ; raise Predicates.JoinFail) ) + else ( + L.d_strln "failed Rename.check" ; + raise Predicates.JoinFail ) ) ~finally:CheckJoin.final @@ -1663,7 +1764,8 @@ let rec sigma_partial_meet' tenv (sigma_acc : Prop.sigma) (sigma1_in : Prop.sigm let hpred' = hpred_partial_meet tenv todo_curr hpred1 hpred2 in sigma_partial_meet' tenv (hpred' :: sigma_acc) sigma1 sigma2 | Some _, Some _ -> - L.d_strln "failure reason 65" ; raise Predicates.JoinFail + L.d_strln "failure reason 65" ; + raise Predicates.JoinFail with Todo.Empty -> ( match (sigma1_in, sigma2_in) with | [], [] -> @@ -1799,20 +1901,33 @@ let pi_partial_join tenv mode (ep1 : Prop.exposed Prop.t) (ep2 : Prop.exposed Pr a' :: atom_list in if Config.trace_join then ( - L.d_str "pi1: " ; Prop.d_pi pi1 ; L.d_ln () ; L.d_str "pi2: " ; Prop.d_pi pi2 ; L.d_ln () ) ; + L.d_str "pi1: " ; + Prop.d_pi pi1 ; + L.d_ln () ; + L.d_str "pi2: " ; + Prop.d_pi pi2 ; + L.d_ln () ) ; let atom_list1 = let p2 = Prop.normalize tenv ep2 in List.fold ~f:(handle_atom_with_widening Lhs p2 pi2) ~init:[] pi1 in - if Config.trace_join then (L.d_str "atom_list1: " ; Prop.d_pi atom_list1 ; L.d_ln ()) ; + if Config.trace_join then ( + L.d_str "atom_list1: " ; + Prop.d_pi atom_list1 ; + L.d_ln () ) ; let atom_list2 = let p1 = Prop.normalize tenv ep1 in List.fold ~f:(handle_atom_with_widening Rhs p1 pi1) ~init:[] pi2 in - if Config.trace_join then (L.d_str "atom_list2: " ; Prop.d_pi atom_list2 ; L.d_ln ()) ; + if Config.trace_join then ( + L.d_str "atom_list2: " ; + Prop.d_pi atom_list2 ; + L.d_ln () ) ; let atom_list_combined = IList.inter ~cmp:Predicates.compare_atom atom_list1 atom_list2 in if Config.trace_join then ( - L.d_str "atom_list_combined: " ; Prop.d_pi atom_list_combined ; L.d_ln () ) ; + L.d_str "atom_list_combined: " ; + Prop.d_pi atom_list_combined ; + L.d_ln () ) ; atom_list_combined @@ -1862,7 +1977,9 @@ let eprop_partial_meet tenv (ep1 : 'a Prop.t) (ep2 : 'b Prop.t) : 'c Prop.t = let f e = Exp.free_vars e |> Sequence.for_all ~f:Ident.is_normal in Predicates.equal_subst sub1 sub2 && List.for_all ~f range1 in - if not (sub_check ()) then (L.d_strln "sub_check() failed" ; raise Predicates.JoinFail) + if not (sub_check ()) then ( + L.d_strln "sub_check() failed" ; + raise Predicates.JoinFail ) else let todos = List.map ~f:(fun x -> (x, x, x)) es in List.iter ~f:Todo.push todos ; @@ -1882,7 +1999,10 @@ let prop_partial_meet tenv p1 p2 = try SymOp.try_finally ~f:(fun () -> Some (eprop_partial_meet tenv p1 p2)) - ~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final ()) + ~finally:(fun () -> + Rename.final () ; + FreshVarExp.final () ; + Todo.final () ) with Predicates.JoinFail -> None @@ -1946,7 +2066,8 @@ let eprop_partial_join' tenv mode (ep1 : Prop.exposed Prop.t) (ep2 : Prop.expose in p_sub_sigma_pi | _ -> - L.d_strln "leftovers not empty" ; raise Predicates.JoinFail + L.d_strln "leftovers not empty" ; + raise Predicates.JoinFail let footprint_partial_join' tenv (p1 : Prop.normal Prop.t) (p2 : Prop.normal Prop.t) : @@ -1966,7 +2087,9 @@ let footprint_partial_join' tenv (p1 : Prop.normal Prop.t) (p2 : Prop.normal Pro let f a = Predicates.hpred_free_vars a |> Sequence.exists ~f:(fun a -> not (Ident.is_footprint a)) in - if List.exists ~f sigma_fp0 then (L.d_strln "failure reason 66" ; raise Predicates.JoinFail) ; + if List.exists ~f sigma_fp0 then ( + L.d_strln "failure reason 66" ; + raise Predicates.JoinFail ) ; sigma_fp0 in let ep1' = Prop.set p1 ~pi_fp ~sigma_fp in @@ -1996,7 +2119,10 @@ let prop_partial_join ({InterproceduralAnalysis.tenv; _} as analysis_data) mode let res = eprop_partial_join' tenv mode (Prop.expose p1') (Prop.expose p2') in if !BiabductionConfig.footprint then JoinState.set_footprint false ; Some res ) - ~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final ()) + ~finally:(fun () -> + Rename.final () ; + FreshVarExp.final () ; + Todo.final () ) with Predicates.JoinFail -> None ) | Some _ -> res_by_implication_only @@ -2009,7 +2135,10 @@ let eprop_partial_join tenv mode (ep1 : Prop.exposed Prop.t) (ep2 : Prop.exposed Todo.init () ; SymOp.try_finally ~f:(fun () -> eprop_partial_join' tenv mode ep1 ep2) - ~finally:(fun () -> Rename.final () ; FreshVarExp.final () ; Todo.final ()) + ~finally:(fun () -> + Rename.final () ; + FreshVarExp.final () ; + Todo.final () ) (** {2 Join and Meet for Propset} *) diff --git a/infer/src/biabduction/DotBiabduction.ml b/infer/src/biabduction/DotBiabduction.ml index 7a5901490..476b4e159 100644 --- a/infer/src/biabduction/DotBiabduction.ml +++ b/infer/src/biabduction/DotBiabduction.ml @@ -115,7 +115,9 @@ let strip_special_chars b = let replace st c c' = if Bytes.contains st c then ( let idx = String.index_exn (Bytes.to_string st) c in - try Bytes.set st idx c' ; st + try + Bytes.set st idx c' ; + st with Invalid_argument _ -> L.internal_error "@\n@\nstrip_special_chars: Invalid argument!@\n@." ; assert false ) @@ -423,7 +425,8 @@ let compute_fields_struct sigma = | [] -> () | Predicates.Hpointsto (_, se, _) :: s' -> - do_strexp se false ; fs s' + do_strexp se false ; + fs s' | _ :: s' -> fs s' in diff --git a/infer/src/biabduction/Paths.ml b/infer/src/biabduction/Paths.ml index 43c6ab56f..c48c14c80 100644 --- a/infer/src/biabduction/Paths.ml +++ b/infer/src/biabduction/Paths.ml @@ -172,13 +172,19 @@ end = struct | Pstart (_, stats) -> if not (stats_is_dummy stats) then set_dummy_stats stats | Pnode (_, _, _, path, stats, _) | Pcall (path, _, ExecSkipped _, stats) -> - if not (stats_is_dummy stats) then (reset_stats path ; set_dummy_stats stats) + if not (stats_is_dummy stats) then ( + reset_stats path ; + set_dummy_stats stats ) | Pjoin (path1, path2, stats) -> if not (stats_is_dummy stats) then ( - reset_stats path1 ; reset_stats path2 ; set_dummy_stats stats ) + reset_stats path1 ; + reset_stats path2 ; + set_dummy_stats stats ) | Pcall (path1, _, ExecCompleted path2, stats) -> if not (stats_is_dummy stats) then ( - reset_stats path1 ; reset_stats path2 ; set_dummy_stats stats ) + reset_stats path1 ; + reset_stats path2 ; + set_dummy_stats stats ) (** Iterate [f] over the path and compute the stats, assuming the invariant: all the stats are @@ -218,7 +224,8 @@ end = struct let stats2 = match do_calls with | true -> - compute_stats do_calls f path2 ; get_stats path2 + compute_stats do_calls f path2 ; + get_stats path2 | false -> {max_length= 0; linear_num= 0.0} in @@ -228,13 +235,17 @@ end = struct (* already found in call, no need to search before the call *) else f in - compute_stats do_calls f' path1 ; get_stats path1 + compute_stats do_calls f' path1 ; + get_stats path1 in stats.max_length <- stats1.max_length + stats2.max_length ; stats.linear_num <- stats1.linear_num ) | Pcall (path, _, ExecSkipped _, stats) -> if stats_is_dummy stats then ( - let stats1 = compute_stats do_calls f path ; get_stats path in + let stats1 = + compute_stats do_calls f path ; + get_stats path + in stats.max_length <- stats1.max_length ; stats.linear_num <- stats1.linear_num ) end @@ -295,7 +306,8 @@ end = struct doit (level + 1) session p2 next_exn_opt | Pcall (p, _, ExecSkipped _, _) -> let next_exn_opt = None in - doit level session p next_exn_opt ; f level path session prev_exn_opt + doit level session p next_exn_opt ; + f level path session prev_exn_opt in Invariant.compute_stats true filter path ; doit 0 0 path None ; @@ -407,7 +419,10 @@ end = struct add_delayed p | Pjoin (p1, p2, _) | Pcall (p1, _, ExecCompleted p2, _) -> (* delay paths occurring in a join *) - add_delayed p1 ; add_delayed p2 ; add_path p1 ; add_path p2 + add_delayed p1 ; + add_delayed p2 ; + add_path p1 ; + add_path p2 in let rec doit n fmt path = try @@ -430,9 +445,12 @@ end = struct let print_delayed () = if not (PathMap.is_empty !delayed) then ( let f path num = F.fprintf fmt "P%d = %a@\n" num (doit 1) path in - F.fprintf fmt "where@\n" ; PathMap.iter f !delayed ) + F.fprintf fmt "where@\n" ; + PathMap.iter f !delayed ) in - add_delayed path ; doit 0 fmt path ; print_delayed () + add_delayed path ; + doit 0 fmt path ; + print_delayed () let create_loc_trace path pos_opt : Errlog.loc_trace = @@ -606,7 +624,8 @@ end = struct let elements ps = let plist = ref [] in let f prop path = plist := (prop, path) :: !plist in - PropMap.iter f ps ; !plist + PropMap.iter f ps ; + !plist let to_proplist ps = List.map ~f:fst (elements ps) @@ -656,7 +675,8 @@ end = struct then res := PropMap.remove p !res with Caml.Not_found -> res := PropMap.remove p !res in - PropMap.iter rem ps2 ; !res + PropMap.iter rem ps2 ; + !res let is_empty = PropMap.is_empty @@ -670,7 +690,8 @@ end = struct let do_elem prop path = match f prop with None -> () | Some prop' -> res := add_renamed_prop prop' path !res in - iter do_elem ps ; !res + iter do_elem ps ; + !res let map f ps = map_option (fun p -> Some (f p)) ps diff --git a/infer/src/biabduction/Predicates.ml b/infer/src/biabduction/Predicates.ml index 376709c69..8bb12912f 100644 --- a/infer/src/biabduction/Predicates.ml +++ b/infer/src/biabduction/Predicates.ml @@ -1115,7 +1115,10 @@ let create_sharing_env () = {exph= Exp.Hash.create 3; hpredh= HpredInstHash.crea (** Return a canonical representation of the exp *) let exp_compact sh e = - try Exp.Hash.find sh.exph e with Caml.Not_found -> Exp.Hash.add sh.exph e e ; e + try Exp.Hash.find sh.exph e + with Caml.Not_found -> + Exp.Hash.add sh.exph e e ; + e let rec sexp_compact sh se = diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml index 99316313d..92d29e639 100644 --- a/infer/src/biabduction/Prop.ml +++ b/infer/src/biabduction/Prop.ml @@ -206,7 +206,9 @@ let d_pi_sigma pi sigma = let d_separator () = if (not (List.is_empty pi)) && not (List.is_empty sigma) then L.d_strln " *" in - d_pi pi ; d_separator () ; d_sigma sigma + d_pi pi ; + d_separator () ; + d_sigma sigma let pi_of_subst sub = @@ -539,7 +541,8 @@ let sigma_get_unsigned_exps sigma = | _ -> () in - List.iter ~f:do_hpred sigma ; !uexps + List.iter ~f:do_hpred sigma ; + !uexps (** Collapse consecutive indices that should be added. For instance, this function reduces @@ -1952,7 +1955,8 @@ let sigma_dfs_sort tenv sigma = in init () ; let sigma' = handle_sigma [] sigma in - final () ; sigma' + final () ; + sigma' let dfs_sort tenv p : sorted t = diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index 22f1a70af..d4daf017b 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -1044,7 +1044,12 @@ exception MISSING_EXC of string type check = Bounds_check | Class_cast_check of Exp.t * Exp.t * Exp.t let d_typings typings = - let d_elem (exp, texp) = Exp.d_exp exp ; L.d_str ": " ; Exp.d_texp_full texp ; L.d_str " " in + let d_elem (exp, texp) = + Exp.d_exp exp ; + L.d_str ": " ; + Exp.d_texp_full texp ; + L.d_str " " + in List.iter ~f:d_elem typings @@ -1187,9 +1192,16 @@ end = struct Prop.d_sub sub ; L.d_decrease_indent () ; if (not (List.is_empty !missing_pi)) && not (List.is_empty !missing_sigma) then ( - L.d_ln () ; Prop.d_pi !missing_pi ; L.d_strln "*" ; Prop.d_sigma !missing_sigma ) - else if not (List.is_empty !missing_pi) then (L.d_ln () ; Prop.d_pi !missing_pi) - else if not (List.is_empty !missing_sigma) then (L.d_ln () ; Prop.d_sigma !missing_sigma) ; + L.d_ln () ; + Prop.d_pi !missing_pi ; + L.d_strln "*" ; + Prop.d_sigma !missing_sigma ) + else if not (List.is_empty !missing_pi) then ( + L.d_ln () ; + Prop.d_pi !missing_pi ) + else if not (List.is_empty !missing_sigma) then ( + L.d_ln () ; + Prop.d_sigma !missing_sigma ) ; if not (List.is_empty !missing_fld) then ( L.d_ln () ; L.d_strln "MISSING FLD:" ; @@ -1212,7 +1224,11 @@ end = struct || (not (List.is_empty !missing_fld)) || (not (List.is_empty !missing_typ)) || not (Predicates.is_sub_empty sub) - then ( L.d_ln () ; L.d_str "[" ; d_missing_ sub ; L.d_str "]" ) + then ( + L.d_ln () ; + L.d_str "[" ; + d_missing_ sub ; + L.d_str "]" ) let d_frame_fld () = @@ -1261,15 +1277,24 @@ end = struct | EXC_FALSE -> () | EXC_FALSE_HPRED hpred -> - L.d_str " on " ; Predicates.d_hpred hpred + L.d_str " on " ; + Predicates.d_hpred hpred | EXC_FALSE_EXPS (e1, e2) -> - L.d_str " on " ; Exp.d_exp e1 ; L.d_str "," ; Exp.d_exp e2 + L.d_str " on " ; + Exp.d_exp e1 ; + L.d_str "," ; + Exp.d_exp e2 | EXC_FALSE_SEXPS (se1, se2) -> - L.d_str " on " ; Predicates.d_sexp se1 ; L.d_str "," ; Predicates.d_sexp se2 + L.d_str " on " ; + Predicates.d_sexp se1 ; + L.d_str "," ; + Predicates.d_sexp se2 | EXC_FALSE_ATOM a -> - L.d_str " on " ; Predicates.d_atom a + L.d_str " on " ; + Predicates.d_atom a | EXC_FALSE_SIGMA sigma -> - L.d_str " on " ; Prop.d_sigma sigma + L.d_str " on " ; + Prop.d_sigma sigma in L.d_ln () ; L.d_strln "$$$$$$$ Implication" ; @@ -1995,7 +2020,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 (Prop.prop_iter_to_prop tenv iter1'') sigma2 hpred2 ) in - L.d_decrease_indent () ; res + L.d_decrease_indent () ; + res | Predicates.Hdllseg (Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _ when Exp.equal (Predicates.exp_sub (fst subs) iF1) e2 -> (* Unroll dllseg forward *) @@ -2012,7 +2038,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 (Prop.prop_iter_to_prop tenv iter1'') sigma2 hpred2 ) in - L.d_decrease_indent () ; res + L.d_decrease_indent () ; + res | Predicates.Hdllseg (Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _ when Exp.equal (Predicates.exp_sub (fst subs) iB1) e2 -> (* Unroll dllseg backward *) @@ -2029,7 +2056,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 (Prop.prop_iter_to_prop tenv iter1'') sigma2 hpred2 ) in - L.d_decrease_indent () ; res + L.d_decrease_indent () ; + res | _ -> assert false ) ) ) | Predicates.Hlseg (k, para2, e2_, f2_, elist2_) -> ( @@ -2063,7 +2091,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 sigma_imply tenv calc_index_frame false subs prop1 para_inst2 ) in (* calc_missing is false as we're checking an instantiation of the original list *) - L.d_decrease_indent () ; res + L.d_decrease_indent () ; + res | Some iter1' -> ( let elist2 = List.map ~f:(fun e -> Predicates.exp_sub (snd subs) e) elist2_ in (* force instantiation of existentials *) @@ -2093,7 +2122,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 let _, para_inst3 = Predicates.hpara_instantiate para2 e2_ f2_ elist2 in sigma_imply tenv calc_index_frame calc_missing subs prop1 para_inst3 ) in - L.d_decrease_indent () ; res + L.d_decrease_indent () ; + res | Predicates.Hdllseg _ -> assert false ) ) ) | Predicates.Hdllseg (Lseg_PE, _, _, _, _, _, _) -> @@ -2142,7 +2172,8 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 sigma_imply tenv calc_index_frame false subs prop1 para_inst2 ) in (* calc_missing is false as we're checking an instantiation of the original list *) - L.d_decrease_indent () ; res + L.d_decrease_indent () ; + res | Some iter1' -> (* Only consider implications between identical listsegs for now *) let elist2 = List.map ~f:(fun e -> Predicates.exp_sub (snd subs) e) elist2 in @@ -2254,7 +2285,8 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * decrease_indent_when_exception (fun () -> hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2' ) in - L.d_decrease_indent () ; res + L.d_decrease_indent () ; + res with IMPL_EXC _ when calc_missing -> ( match is_constant_string_class subs hpred2' with | Some (s, is_string) -> @@ -2287,7 +2319,8 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 * decrease_indent_when_exception (fun () -> sigma_imply tenv calc_index_frame calc_missing subs' prop1' sigma2' ) in - L.d_decrease_indent () ; res + L.d_decrease_indent () ; + res in match hpred2 with | Predicates.Hpointsto (e2_, se2, t) -> @@ -2433,7 +2466,9 @@ let check_implication_base {InterproceduralAnalysis.proc_desc; err_log; tenv} ch L.d_decrease_indent () ; L.d_ln () ; if not (List.is_empty pi2_bcheck) then ( - L.d_str "pi2 bounds checks: " ; Prop.d_pi pi2_bcheck ; L.d_ln () ) ; + L.d_str "pi2 bounds checks: " ; + Prop.d_pi pi2_bcheck ; + L.d_ln () ) ; L.d_strln "returns" ; L.d_strln "sub1:" ; L.d_increase_indent () ; diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index 5738b4273..b2f27e573 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -69,7 +69,11 @@ let check_bad_index {InterproceduralAnalysis.proc_desc; err_log; tenv} pname p l (** Perform bounds checking *) let bounds_check analysis_data pname prop len e = if Config.trace_rearrange then ( - L.d_str "Bounds check index:" ; Exp.d_exp e ; L.d_str " len: " ; Exp.d_exp len ; L.d_ln () ) ; + L.d_str "Bounds check index:" ; + Exp.d_exp e ; + L.d_str " len: " ; + Exp.d_exp len ; + L.d_ln () ) ; check_bad_index analysis_data pname prop len e @@ -86,7 +90,10 @@ let rec create_struct_values analysis_data pname tenv orig_prop footprint_part k Predicates.d_offset_list off ; L.d_ln () ; L.d_ln () ) ; - let new_id () = incr max_stamp ; Ident.create kind !max_stamp in + let new_id () = + incr max_stamp ; + Ident.create kind !max_stamp + in let res = let fail t off pos = L.d_str "create_struct_values type:" ; @@ -190,7 +197,10 @@ let rec create_struct_values analysis_data pname tenv orig_prop footprint_part k function. *) let rec strexp_extend_values_ analysis_data pname tenv orig_prop footprint_part kind max_stamp se (typ : Typ.t) (off : Predicates.offset list) inst = - let new_id () = incr max_stamp ; Ident.create kind !max_stamp in + let new_id () = + incr max_stamp ; + Ident.create kind !max_stamp + in match (off, se, typ.desc) with | [], Predicates.Eexp _, _ | [], Predicates.Estruct _, _ -> [([], se, typ)] @@ -1007,7 +1017,9 @@ let check_type_size {InterproceduralAnalysis.proc_desc; err_log; tenv} pname pro BiabductionReporting.log_issue_deprecated_using_state proc_desc err_log Exceptions.Warning exn | None -> - L.d_str "texp: " ; Exp.d_texp_full texp ; L.d_ln () + L.d_str "texp: " ; + Exp.d_texp_full texp ; + L.d_ln () (** Exposes lexp |->- from iter. In case that it is not possible to * expose lexp |->-, this diff --git a/infer/src/biabduction/RetainCyclesType.ml b/infer/src/biabduction/RetainCyclesType.ml index 8f5de8f54..ba366c6ee 100644 --- a/infer/src/biabduction/RetainCyclesType.ml +++ b/infer/src/biabduction/RetainCyclesType.ml @@ -210,4 +210,5 @@ let pp_dotty fmt cycle = let write_dotty_to_file fname cycle = let chan = Out_channel.create fname in let fmt = Format.formatter_of_out_channel chan in - pp_dotty fmt cycle ; Out_channel.close chan + pp_dotty fmt cycle ; + Out_channel.close chan diff --git a/infer/src/biabduction/State.ml b/infer/src/biabduction/State.ml index 6457668b7..8495010e6 100644 --- a/infer/src/biabduction/State.ml +++ b/infer/src/biabduction/State.ml @@ -85,7 +85,10 @@ let instrs_normalize instrs = in let subst = let count = ref Int.min_value in - let gensym id = incr count ; Ident.set_stamp id !count in + let gensym id = + incr count ; + Ident.set_stamp id !count + in Predicates.subst_of_list (List.rev_map ~f:(fun id -> (id, Exp.Var (gensym id))) bound_ids) in let subst_and_add acc instr = Predicates.instr_sub subst instr :: acc in diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 14ae09547..07fb714ac 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -324,7 +324,8 @@ and prune_inter tenv ~positive condition1 condition2 prop = let res = ref Propset.empty in let pset1 = prune tenv ~positive condition1 prop in let do_p p = res := Propset.union (prune tenv ~positive condition2 p) !res in - Propset.iter do_p pset1 ; !res + Propset.iter do_p pset1 ; + !res and prune_union tenv ~positive condition1 condition2 prop = diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 80d0f4b5c..9fbf35528 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -806,7 +806,9 @@ let combine ({InterproceduralAnalysis.proc_desc= caller_pdesc; tenv; _} as analy Prop.d_sigma split.frame_fld ; L.d_ln () ; if not (List.is_empty split.frame_typ) then ( - L.d_strln "Frame typ:" ; Prover.d_typings split.frame_typ ; L.d_ln () ) ; + L.d_strln "Frame typ:" ; + Prover.d_typings split.frame_typ ; + L.d_ln () ) ; L.d_strln "Missing fld:" ; Prop.d_sigma split.missing_fld ; L.d_ln () ; @@ -926,7 +928,8 @@ let mk_actual_precondition tenv prop actual_params formal_params = ^ string_of_int (List.length formal_params) ^ ")" in - L.d_warning str ; L.d_ln () ) ; + L.d_warning str ; + L.d_ln () ) ; [] | _ :: _, [] -> raise (Exceptions.Wrong_argument_number __POS__) @@ -1249,7 +1252,11 @@ let exe_call_postprocess tenv ret_id callee_pname callee_attrs loc results = let deref_errors = List.filter ~f:(function Dereference_error _ -> true | _ -> false) invalid_res in - let print_pi pi = L.d_str "pi: " ; Prop.d_pi pi ; L.d_ln () in + let print_pi pi = + L.d_str "pi: " ; + Prop.d_pi pi ; + L.d_ln () + in let call_desc kind_opt = Localise.desc_precondition_not_met kind_opt callee_pname loc in let res_with_path_idents = if !BiabductionConfig.footprint then @@ -1325,7 +1332,8 @@ let exe_call_postprocess tenv ret_id callee_pname callee_attrs loc results = in State.add_diverging_states (Paths.PathSet.from_renamed_list incons_res) in - save_diverging_states () ; vr.vr_cons_res + save_diverging_states () ; + vr.vr_cons_res in List.map ~f:(fun (p, path) -> (prop_pure_to_footprint tenv p, path)) diff --git a/infer/src/biabduction/Timeout.ml b/infer/src/biabduction/Timeout.ml index 1bfcd1dc6..bacfc1c54 100644 --- a/infer/src/biabduction/Timeout.ml +++ b/infer/src/biabduction/Timeout.ml @@ -91,11 +91,16 @@ let () = ignore (Gc.create_alarm SymOp.check_wallclock_alarm) -let unwind () = unset_alarm () ; SymOp.unset_alarm () ; GlobalState.pop () +let unwind () = + unset_alarm () ; + SymOp.unset_alarm () ; + GlobalState.pop () + let suspend_existing_timeout ~keep_symop_total = let current_status = get_current_status ~keep_symop_total in - unset_alarm () ; GlobalState.push current_status + unset_alarm () ; + GlobalState.push current_status let resume_previous_timeout () = diff --git a/infer/src/biabduction/errdesc.ml b/infer/src/biabduction/errdesc.ml index 22b7827dd..029a9d6c0 100644 --- a/infer/src/biabduction/errdesc.ml +++ b/infer/src/biabduction/errdesc.ml @@ -165,7 +165,10 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option = let seen = Exp.Set.add e seen_ in match Prop.exp_normalize_noabs tenv Predicates.sub_empty e with | Exp.Const c -> - if verbose then (L.d_str "exp_lv_dexp: constant " ; Exp.d_exp e ; L.d_ln ()) ; + if verbose then ( + L.d_str "exp_lv_dexp: constant " ; + Exp.d_exp e ; + L.d_ln () ) ; Some (DExp.Dderef (DExp.Dconst c)) | Exp.BinOp (Binop.PlusPI, e1, e2) -> ( if verbose then ( @@ -225,7 +228,9 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option = Some (DExp.Darrow (de, f)) ) | Exp.Lfield (e1, f, _) -> ( if verbose then ( - L.d_str "exp_lv_dexp: Lfield " ; Exp.d_exp e1 ; L.d_printfln " %a" Fieldname.pp f ) ; + L.d_str "exp_lv_dexp: Lfield " ; + Exp.d_exp e1 ; + L.d_printfln " %a" Fieldname.pp f ) ; match exp_lv_dexp_ tenv seen node e1 with | None -> None @@ -233,7 +238,11 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option = Some (DExp.Ddot (de, f)) ) | Exp.Lindex (e1, e2) -> ( if verbose then ( - L.d_str "exp_lv_dexp: Lindex " ; Exp.d_exp e1 ; L.d_str " " ; Exp.d_exp e2 ; L.d_ln () ) ; + L.d_str "exp_lv_dexp: Lindex " ; + Exp.d_exp e1 ; + L.d_str " " ; + Exp.d_exp e2 ; + L.d_ln () ) ; match (exp_lv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with | None, _ -> None @@ -261,7 +270,10 @@ and exp_rv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option = let seen = Exp.Set.add e seen_ in match e with | Exp.Const c -> - if verbose then (L.d_str "exp_rv_dexp: constant " ; Exp.d_exp e ; L.d_ln ()) ; + if verbose then ( + L.d_str "exp_rv_dexp: constant " ; + Exp.d_exp e ; + L.d_ln () ) ; Some (DExp.Dconst c) | Exp.Lvar pv -> if verbose then ( @@ -279,7 +291,9 @@ and exp_rv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option = find_normal_variable_load_ tenv seen node id | Exp.Lfield (e1, f, _) -> ( if verbose then ( - L.d_str "exp_rv_dexp: Lfield " ; Exp.d_exp e1 ; L.d_printfln " %a" Fieldname.pp f ) ; + L.d_str "exp_rv_dexp: Lfield " ; + Exp.d_exp e1 ; + L.d_printfln " %a" Fieldname.pp f ) ; match exp_rv_dexp_ tenv seen node e1 with | None -> None @@ -287,31 +301,47 @@ and exp_rv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option = Some (DExp.Ddot (de, f)) ) | Exp.Lindex (e1, e2) -> ( if verbose then ( - L.d_str "exp_rv_dexp: Lindex " ; Exp.d_exp e1 ; L.d_str " " ; Exp.d_exp e2 ; L.d_ln () ) ; + L.d_str "exp_rv_dexp: Lindex " ; + Exp.d_exp e1 ; + L.d_str " " ; + Exp.d_exp e2 ; + L.d_ln () ) ; match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with | None, _ | _, None -> None | Some de1, Some de2 -> Some (DExp.Darray (de1, de2)) ) | Exp.BinOp (op, e1, e2) -> ( - if verbose then (L.d_str "exp_rv_dexp: BinOp " ; Exp.d_exp e ; L.d_ln ()) ; + if verbose then ( + L.d_str "exp_rv_dexp: BinOp " ; + Exp.d_exp e ; + L.d_ln () ) ; match (exp_rv_dexp_ tenv seen node e1, exp_rv_dexp_ tenv seen node e2) with | None, _ | _, None -> None | Some de1, Some de2 -> Some (DExp.Dbinop (op, de1, de2)) ) | Exp.UnOp (op, e1, _) -> ( - if verbose then (L.d_str "exp_rv_dexp: UnOp " ; Exp.d_exp e ; L.d_ln ()) ; + if verbose then ( + L.d_str "exp_rv_dexp: UnOp " ; + Exp.d_exp e ; + L.d_ln () ) ; match exp_rv_dexp_ tenv seen node e1 with | None -> None | Some de1 -> Some (DExp.Dunop (op, de1)) ) | Exp.Cast (_, e1) -> - if verbose then (L.d_str "exp_rv_dexp: Cast " ; Exp.d_exp e ; L.d_ln ()) ; + if verbose then ( + L.d_str "exp_rv_dexp: Cast " ; + Exp.d_exp e ; + L.d_ln () ) ; exp_rv_dexp_ tenv seen node e1 | Exp.Sizeof {typ; dynamic_length; subtype} -> - if verbose then (L.d_str "exp_rv_dexp: type " ; Exp.d_exp e ; L.d_ln ()) ; + if verbose then ( + L.d_str "exp_rv_dexp: type " ; + Exp.d_exp e ; + L.d_ln () ) ; Some (DExp.Dsizeof (typ, Option.bind dynamic_length ~f:(exp_rv_dexp_ tenv seen node), subtype)) | _ -> @@ -513,7 +543,10 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = (** find the dexp, if any, where the given value is stored also return the type of the value if found *) let vpath_find tenv prop exp_ : DExp.t option * Typ.t option = - if verbose then (L.d_str "in vpath_find exp:" ; Exp.d_exp exp_ ; L.d_ln ()) ; + if verbose then ( + L.d_str "in vpath_find exp:" ; + Exp.d_exp exp_ ; + L.d_ln () ) ; let rec find sigma_acc sigma_todo exp = let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) = match se with @@ -614,7 +647,12 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option = L.d_ln () | Some de, typo -> ( L.d_printf "vpath_find: found %a :" DExp.pp de ; - match typo with None -> L.d_str " No type" | Some typ -> Typ.d_full typ ; L.d_ln () ) ) ; + match typo with + | None -> + L.d_str " No type" + | Some typ -> + Typ.d_full typ ; + L.d_ln () ) ) ; res @@ -657,7 +695,8 @@ let explain_dexp_access prop dexp is_nullable = | _ -> () in - List.iter ~f:do_hpred sigma ; !res + List.iter ~f:do_hpred sigma ; + !res in let rec lookup_fld fsel f = match fsel with diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 94d984860..3967c308a 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -396,7 +396,9 @@ let forward_tabulate ({InterproceduralAnalysis.proc_desc; err_log; tenv; _} as a in ( match pre_opt with | Some pre -> - L.d_strln "Precondition:" ; Prop.d_prop pre ; L.d_ln () + L.d_strln "Precondition:" ; + Prop.d_prop pre ; + L.d_ln () | None -> () ) ; L.d_strln "SIL INSTR:" ; @@ -408,7 +410,11 @@ let forward_tabulate ({InterproceduralAnalysis.proc_desc; err_log; tenv; _} as a let exe_iter f pathset = let ps_size = Paths.PathSet.size pathset in let cnt = ref 0 in - let exe prop path = State.set_path path None ; incr cnt ; f prop path !cnt ps_size in + let exe prop path = + State.set_path path None ; + incr cnt ; + f prop path !cnt ps_size + in Paths.PathSet.iter exe pathset in let print_node_preamble curr_node pathset_todo = @@ -489,7 +495,8 @@ let remove_locals_formals_and_check {InterproceduralAnalysis.proc_desc; err_log; let exn = Exceptions.Stack_variable_address_escape (desc, __POS__) in BiabductionReporting.log_issue_deprecated_using_state proc_desc err_log Exceptions.Warning exn in - List.iter ~f:check_pvar pvars ; p' + List.iter ~f:check_pvar pvars ; + p' (** Collect the analysis results for the exit node. *) @@ -739,7 +746,8 @@ let execute_filter_prop ({InterproceduralAnalysis.tenv; _} as analysis_data) pro precondition in let spec = BiabductionSummary.{pre; posts; visited} in - L.d_decrease_indent () ; Some spec ) + L.d_decrease_indent () ; + Some spec ) with RE_EXE_ERROR -> AnalysisCallbacks.html_debug_new_node_session ~pp_name init_node ~f:(fun () -> L.d_printfln ~color:Red "#### [FUNCTION %a] ...ERROR" Procname.pp pname ; diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index fca695404..f89e8c0b3 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -242,7 +242,10 @@ module Loc = struct BufferOverrunField.pp ~pp_lhs:(pp_star ~paren:true) ~sep:"." fmt prefix last_field - and pp_star ~paren fmt l = pp_paren ~paren fmt l ; F.pp_print_string fmt ".*" + and pp_star ~paren fmt l = + pp_paren ~paren fmt l ; + F.pp_print_string fmt ".*" + let pp = pp_paren ~paren:false diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index fe1d92cd8..661ebc0be 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -74,8 +74,12 @@ module SymLinear = struct let c = (c :> Z.t) in let c = if is_beginning then c - else if Z.gt c Z.zero then (F.pp_print_string f " + " ; c) - else (F.pp_print_string f " - " ; Z.neg c) + else if Z.gt c Z.zero then ( + F.pp_print_string f " + " ; + c ) + else ( + F.pp_print_string f " - " ; + Z.neg c ) in if Z.(equal c one) then (Symb.Symbol.pp_mark ~markup) f s else if Z.(equal c minus_one) then F.fprintf f "-%a" (Symb.Symbol.pp_mark ~markup) s @@ -86,7 +90,11 @@ module SymLinear = struct fun ~markup ~is_beginning f x -> if M.is_empty x then if is_beginning then F.pp_print_string f "0" else () else - ( M.fold (fun s c is_beginning -> pp1 ~markup ~is_beginning f s c ; false) x is_beginning + ( M.fold + (fun s c is_beginning -> + pp1 ~markup ~is_beginning f s c ; + false ) + x is_beginning : bool ) |> ignore diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index f3630a9e5..a58299bae 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -463,7 +463,8 @@ let cached_compute_invariant_map = inv_map | None -> let inv_map = compute_invariant_map analysis_data in - cache_set pname inv_map ; inv_map + cache_set pname inv_map ; + inv_map let compute_summary : (Pvar.t * Typ.t) list -> CFG.t -> invariant_map -> memory_summary = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index a13ef9a97..c60a87f38 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -1431,7 +1431,10 @@ end module AliasRet = struct include AliasTargets - let pp : F.formatter -> t -> unit = fun fmt x -> F.pp_print_string fmt "ret=" ; pp fmt x + let pp : F.formatter -> t -> unit = + fun fmt x -> + F.pp_print_string fmt "ret=" ; + pp fmt x end module Alias = struct diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index 1927fce2f..e179bfe98 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -169,7 +169,10 @@ module SymbolPath = struct if paren then F.fprintf fmt ")" - and pp_star ~paren fmt p = pp_partial_paren ~paren fmt p ; F.pp_print_string fmt ".*" + and pp_star ~paren fmt p = + pp_partial_paren ~paren fmt p ; + F.pp_print_string fmt ".*" + let pp_partial = pp_partial_paren ~paren:false diff --git a/infer/src/checkers/NullabilityPreanalysis.ml b/infer/src/checkers/NullabilityPreanalysis.ml index 6ed62e5fd..53f1a4d1f 100644 --- a/infer/src/checkers/NullabilityPreanalysis.ml +++ b/infer/src/checkers/NullabilityPreanalysis.ml @@ -41,7 +41,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let exec_instr astate id_table _ instr = match instr with | Sil.Load {id; e= exp} -> - Ident.Hash.add id_table id exp ; astate + Ident.Hash.add id_table id exp ; + astate | Sil.Store {e1= Exp.Lfield (Exp.Var lhs_id, name, typ); typ= exp_typ; e2= rhs} -> ( match exp_typ.Typ.desc with (* block field of a ObjC class *) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index dd98795bc..2d402b99e 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -242,7 +242,8 @@ module CxxAnnotationSpecs = struct let debug_pred ~spec_name ~desc pred pname = L.d_printf "%s: Checking if `%a` is a %s... " spec_name Procname.pp pname desc ; let r = pred pname in - L.d_printf "%b %s.@." r desc ; r + L.d_printf "%b %s.@." r desc ; + r let at_least_one_nonempty ~src symbols symbol_regexps paths = diff --git a/infer/src/checkers/dominators.ml b/infer/src/checkers/dominators.ml index 64466374b..65c591ef3 100644 --- a/infer/src/checkers/dominators.ml +++ b/infer/src/checkers/dominators.ml @@ -27,7 +27,8 @@ let print_dominators cfg idom = [idom n] returns the immediate dominator of [n]. *) let get_idoms pdesc = let idom = GDoms.compute_idom pdesc (ProcCfg.Normal.start_node pdesc) in - print_dominators pdesc idom ; idom + print_dominators pdesc idom ; + idom (* make each node to be dominated by itself, i.e reflexive, unlike ocamlgraph *) diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index 53e7eb9ef..3b25f55bb 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -328,7 +328,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct () ) ; {astate with maybe_uninit_vars} | Assume (expr, _, _, loc) -> - check_hil_expr expr ~loc ; astate + check_hil_expr expr ~loc ; + astate | Metadata _ -> astate diff --git a/infer/src/clang/cAst_utils.ml b/infer/src/clang/cAst_utils.ml index 8e2ef7f49..7bd78a88f 100644 --- a/infer/src/clang/cAst_utils.ml +++ b/infer/src/clang/cAst_utils.ml @@ -336,7 +336,8 @@ let generate_key_stmt stmt = let _, stmts = Clang_ast_proj.get_stmt_tuple stmt in List.iter ~f:add_stmt stmts in - add_stmt stmt ; Buffer.contents buffer + add_stmt stmt ; + Buffer.contents buffer (* Generates a key for a declaration based on its name and the declaration tag. *) diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 18dfd842c..b8080d620 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -126,7 +126,8 @@ let should_create_procdesc cfg procname ~defined ~set_objc_accessor_attr = | previous_procdesc -> let is_defined_previous = Procdesc.is_defined previous_procdesc in if (defined || set_objc_accessor_attr) && not is_defined_previous then ( - Procname.Hash.remove cfg procname ; true ) + Procname.Hash.remove cfg procname ; + true ) else false | exception Caml.Not_found -> true @@ -264,7 +265,8 @@ let create_local_procdesc ?(set_objc_accessor_attr = false) trans_unit_ctx cfg t Procdesc.set_exit_node procdesc exit_node ) in if should_create_procdesc cfg proc_name ~defined ~set_objc_accessor_attr then ( - create_new_procdesc () ; true ) + create_new_procdesc () ; + true ) else false diff --git a/infer/src/clang/cScope.ml b/infer/src/clang/cScope.ml index 64cff2890..ff234cf25 100644 --- a/infer/src/clang/cScope.ml +++ b/infer/src/clang/cScope.ml @@ -203,7 +203,8 @@ module Variables = struct and visit_stmt_list stmt_list scope_map = List.fold stmt_list ~init:scope_map ~f:(fun scope_map stmt -> - L.debug Capture Verbose "@;" ; visit_stmt stmt scope_map ) + L.debug Capture Verbose "@;" ; + visit_stmt stmt scope_map ) let empty_scope = {current= []; current_kind= InitialScope; outers= []} diff --git a/infer/src/cost/boundMap.ml b/infer/src/cost/boundMap.ml index c9e8a30ef..8d1be4b94 100644 --- a/infer/src/cost/boundMap.ml +++ b/infer/src/cost/boundMap.ml @@ -83,7 +83,8 @@ let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map Node.IdMap.add node_id BasicCost.zero bound_map ) in let bound_map = NodeCFG.fold_nodes node_cfg ~f:compute_node_upper_bound ~init:Node.IdMap.empty in - print_upper_bound_map bound_map ; bound_map + print_upper_bound_map bound_map ; + bound_map let lookup_upperbound bound_map nid = diff --git a/infer/src/infer.ml b/infer/src/infer.ml index 6832bc138..dae5c6676 100644 --- a/infer/src/infer.ml +++ b/infer/src/infer.ml @@ -56,7 +56,9 @@ let setup () = if CLOpt.is_originator && (not Config.continue_capture) && not (Driver.is_analyze_mode driver_mode) - then ( db_start () ; SourceFiles.mark_all_stale () ) + then ( + db_start () ; + SourceFiles.mark_all_stale () ) | Explore -> ResultsDir.assert_results_dir "please run an infer analysis first" ) ; db_start () ; @@ -109,7 +111,9 @@ let log_environment_info () = | Some available_memory -> L.environment_info "Available memory at startup: %d MB@\n" available_memory ; ScubaLogging.log_count ~label:"startup_mem_avail_MB" ~value:available_memory ) ; - print_active_checkers () ; print_scheduler () ; print_cores_used () + print_active_checkers () ; + print_scheduler () ; + print_cores_used () let () = @@ -121,7 +125,8 @@ let () = | Ok () -> L.exit 0 | Error e -> - print_endline e ; L.exit 3 ) ; + print_endline e ; + L.exit 3 ) ; ( match Config.check_version with | Some check_version -> if not (String.equal check_version Version.versionString) then diff --git a/infer/src/integration/IssuesTest.ml b/infer/src/integration/IssuesTest.ml index c7cd1659e..305d2d9cc 100644 --- a/infer/src/integration/IssuesTest.ml +++ b/infer/src/integration/IssuesTest.ml @@ -80,7 +80,8 @@ let pp_custom_of_report fmt report fields = Option.iter nullsafe_extra ~f:(fun nullsafe_extra -> F.fprintf fmt "%s%a" (comma_separator index) pp_nullsafe_extra nullsafe_extra ) in - List.iteri ~f:pp_field fields ; F.fprintf fmt "@." + List.iteri ~f:pp_field fields ; + F.fprintf fmt "@." in List.iter ~f:(pp_custom_of_issue fmt) report diff --git a/infer/src/integration/JsonReports.ml b/infer/src/integration/JsonReports.ml index 41e2894dc..98a2e60b4 100644 --- a/infer/src/integration/JsonReports.ml +++ b/infer/src/integration/JsonReports.ml @@ -303,7 +303,8 @@ let write_lint_issues filters (issues_outf : Utils.outfile) linereader procname (** Process a summary *) let process_summary ~costs_outf summary issues_acc = - write_costs summary costs_outf ; collect_issues summary issues_acc + write_costs summary costs_outf ; + collect_issues summary issues_acc let process_all_summaries_and_issues ~issues_outf ~costs_outf = diff --git a/infer/src/integration/TraceBugs.ml b/infer/src/integration/TraceBugs.ml index 25d462576..1798c0055 100644 --- a/infer/src/integration/TraceBugs.ml +++ b/infer/src/integration/TraceBugs.ml @@ -19,7 +19,8 @@ let has_trace {Jsonbug_t.bug_trace; _} = not (List.is_empty bug_trace) let with_file_fmt file ~f = Utils.with_file_out file ~f:(fun outc -> let fmt = F.formatter_of_out_channel outc in - f fmt ; F.pp_print_flush fmt () ) + f fmt ; + F.pp_print_flush fmt () ) let pp_trace_item ~show_source_context fmt diff --git a/infer/src/integration/XcodeBuild.ml b/infer/src/integration/XcodeBuild.ml index 1f656e4d7..608b48814 100644 --- a/infer/src/integration/XcodeBuild.ml +++ b/infer/src/integration/XcodeBuild.ml @@ -44,7 +44,8 @@ let capture ~prog ~args = Utils.with_channel_in stderr_chan ~f:(L.progress "XCODEBUILD: %s@.") ; match Unix.waitpid pid with | Ok () -> - In_channel.close stdout_chan ; In_channel.close stderr_chan + In_channel.close stdout_chan ; + In_channel.close stderr_chan | Error _ as err -> L.die ExternalError "*** capture failed to execute: %s" (Unix.Exit_or_signal.to_string_hum err) diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml index 63a2d6bf3..9fb82d9f4 100644 --- a/infer/src/istd/IList.ml +++ b/infer/src/istd/IList.ml @@ -195,7 +195,14 @@ let pp_print_list ~max ?(pp_sep = Format.pp_print_cut) pp_v ppf = pp_v ppf v ; aux (n + 1) rest ) in - function [] -> () | [v] -> pp_v ppf v | v :: rest -> pp_v ppf v ; aux 1 rest + function + | [] -> + () + | [v] -> + pp_v ppf v + | v :: rest -> + pp_v ppf v ; + aux 1 rest let fold2_result ~init ~f l1 l2 = diff --git a/infer/src/istd/ImperativeUnionFind.ml b/infer/src/istd/ImperativeUnionFind.ml index 42a4e6a7b..24d475472 100644 --- a/infer/src/istd/ImperativeUnionFind.ml +++ b/infer/src/istd/ImperativeUnionFind.ml @@ -83,7 +83,8 @@ module Make (Set : Set) = struct set | None -> let set = Set.create (r :> Set.elt) in - H.replace t r set ; set + H.replace t r set ; + set let fold = H.fold @@ -146,7 +147,8 @@ module Make (Set : Set) = struct t.nb_iterators <- t.nb_iterators + 1 ; match IContainer.filter ~fold:Sets.fold ~filter:(is_still_a_repr t) t.sets ~init ~f with | result -> - after_fold t ; result + after_fold t ; + result | exception e -> (* Ensures [nb_iterators] is correct *) IExn.reraise_after ~f:(fun () -> after_fold t) e diff --git a/infer/src/istd/LRUHashtbl.ml b/infer/src/istd/LRUHashtbl.ml index b9177d13a..54b5fd1a1 100644 --- a/infer/src/istd/LRUHashtbl.ml +++ b/infer/src/istd/LRUHashtbl.ml @@ -67,7 +67,12 @@ module Make (Key : Hashtbl.HashedType) = struct let create ~initial_size ~max_size = {map= Hash.create initial_size; lru= LRU.create max_size} let find_opt {map; lru} k = - match Hash.find_opt map k with None -> None | Some (v, e) -> LRU.use lru e ; Some v + match Hash.find_opt map k with + | None -> + None + | Some (v, e) -> + LRU.use lru e ; + Some v let replace {map; lru} k v = @@ -78,7 +83,8 @@ module Make (Key : Hashtbl.HashedType) = struct Option.iter removed_key ~f:(Hash.remove map) ; n | Some (_, n) -> - LRU.use lru n ; n + LRU.use lru n ; + n in Hash.replace map k (v, n) @@ -88,10 +94,14 @@ module Make (Key : Hashtbl.HashedType) = struct | None -> () | Some (_, n) -> - LRU.remove lru n ; Hash.remove map k + LRU.remove lru n ; + Hash.remove map k + + let clear {map; lru} = + Hash.clear map ; + LRU.clear lru - let clear {map; lru} = Hash.clear map ; LRU.clear lru let pp ~pp_key ~pp_v f {map} = let is_first = ref true in @@ -99,7 +109,9 @@ module Make (Key : Hashtbl.HashedType) = struct if !is_first then is_first := false else F.pp_print_string f ", " ; F.fprintf f "%a->%a" pp_key key pp_v v in - F.pp_print_string f "{" ; Hash.iter pp_key_v map ; F.pp_print_string f "}" + F.pp_print_string f "{" ; + Hash.iter pp_key_v map ; + F.pp_print_string f "}" let bindings {map} = Seq.fold_left (fun acc (k, (v, _node)) -> (k, v) :: acc) [] (Hash.to_seq map) diff --git a/infer/src/istd/RecencyMap.ml b/infer/src/istd/RecencyMap.ml index c4e33e25a..ea93ee0cc 100644 --- a/infer/src/istd/RecencyMap.ml +++ b/infer/src/istd/RecencyMap.ml @@ -183,7 +183,8 @@ module Make | None -> None | Some _ as value_opt -> - incr count_old ; value_opt ) + incr count_old ; + value_opt ) map1.old map2.old in {count_new= !count_new; old; new_} diff --git a/infer/src/java/jFrontend.ml b/infer/src/java/jFrontend.ml index 894859f34..ff008e381 100644 --- a/infer/src/java/jFrontend.ml +++ b/infer/src/java/jFrontend.ml @@ -67,7 +67,8 @@ let add_edges (context : JContext.t) start_node exn_node exit_nodes method_body_ | JTrans.Instr node -> connect node pc | JTrans.Prune (node_true, node_false) -> - connect node_true pc ; connect node_false pc + connect node_true pc ; + connect node_false pc | JTrans.Loop (join_node, node_true, node_false) -> Procdesc.node_set_succs context.procdesc join_node ~normal:[node_true; node_false] ~exn:[] ; connect node_true pc ; diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index 970eb8fa7..0550f5542 100644 --- a/infer/src/java/jMain.ml +++ b/infer/src/java/jMain.ml @@ -44,7 +44,8 @@ let capture_libs program tenv = let fake_source_file = SourceFile.from_abs_path (JFrontend.path_of_cached_classname cn) in init_global_state fake_source_file ; let cfg = JFrontend.compute_class_icfg fake_source_file program tenv node in - store_icfg fake_source_file cfg ; JFrontend.cache_classname cn + store_icfg fake_source_file cfg ; + JFrontend.cache_classname cn in JBasics.ClassMap.iter (capture_class tenv) (JClasspath.get_classmap program) diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index c1aa1b909..149436a3a 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -102,7 +102,8 @@ let formals_from_signature program tenv cn ms kind = let method_name = JBasics.ms_name ms in let get_arg_name () = let arg = method_name ^ "_arg_" ^ string_of_int !counter in - incr counter ; Mangled.from_string arg + incr counter ; + Mangled.from_string arg in let collect l vt = let arg_name = get_arg_name () in diff --git a/infer/src/nullsafe/Initializers.ml b/infer/src/nullsafe/Initializers.ml index beb0267c4..e98eaf418 100644 --- a/infer/src/nullsafe/Initializers.ml +++ b/infer/src/nullsafe/Initializers.ml @@ -44,7 +44,8 @@ let final_typestates initializers_current_class tenv typecheck_proc = in List.iter ~f:do_called private_called in - List.iter ~f:do_proc initializers ; !res + List.iter ~f:do_proc initializers ; + !res in (* Get the initializers recursively called by computing a fixpoint. Start from the initializers of the current class and the current procedure. *) @@ -64,7 +65,9 @@ let final_typestates initializers_current_class tenv typecheck_proc = mark_seen initializers_new' ; if not (List.is_empty initializers_new') then fixpoint initializers_new' in - mark_seen initializers_base_case ; fixpoint initializers_base_case ; !res + mark_seen initializers_base_case ; + fixpoint initializers_base_case ; + !res in (* Get the final typestates of all the initializers. *) let final_typestates = ref [] in diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index c87ae5517..ec6ee0ea1 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -75,7 +75,8 @@ let check_condition_for_redundancy if Location.equal loc (Procdesc.Node.get_loc n) then Instrs.iter ~f:do_instr (Procdesc.Node.get_instrs n) in - Procdesc.iter_nodes do_node pdesc ; !throwable_found + Procdesc.iter_nodes do_node pdesc ; + !throwable_found in let from_try_with_resources () : bool = (* heuristic to check if the condition is the translation of try-with-resources *) diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index b7c39e73d..9f7c100cb 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -1213,7 +1213,8 @@ let typecheck_instr ({IntraproceduralAnalysis.proc_desc= curr_pdesc; tenv; _} as | _ -> typestate in - check_field_assign () ; typestate2 + check_field_assign () ; + typestate2 (* Java `new` operators *) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(_, typ)], _, _) when Procname.equal pn BuiltinDecl.__new || Procname.equal pn BuiltinDecl.__new_array -> diff --git a/infer/src/nullsafe/typeErr.ml b/infer/src/nullsafe/typeErr.ml index bf958514b..5dab1b504 100644 --- a/infer/src/nullsafe/typeErr.ml +++ b/infer/src/nullsafe/typeErr.ml @@ -52,7 +52,8 @@ module InstrRef : InstrRefT = struct let gen instr_ref_gen = let node, ir = instr_ref_gen in - incr ir ; (node, !ir) + incr ir ; + (node, !ir) end (* InstrRef *) @@ -357,7 +358,8 @@ let report_forall_issues_and_reset analysis_data ~nullsafe_mode = | None, _ -> () in - H.iter iter err_tbl ; reset () + H.iter iter err_tbl ; + reset () let get_errors () = diff --git a/infer/src/pulse/PulseAbstractValue.ml b/infer/src/pulse/PulseAbstractValue.ml index 2ec946c94..dfce7f461 100644 --- a/infer/src/pulse/PulseAbstractValue.ml +++ b/infer/src/pulse/PulseAbstractValue.ml @@ -17,7 +17,8 @@ let next_fresh = ref initial_next_fresh let mk_fresh () = let l = !next_fresh in - incr next_fresh ; l + incr next_fresh ; + l let pp f l = F.fprintf f "v%d" l diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index 8c75842a2..4afaea6f8 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -52,9 +52,11 @@ let evaluate_static_guard label_o (e_fun, arg_ts) = let name = Procname.hashable_name n in let re = Str.regexp label.ToplAst.procedure_name in let result = Str.string_match re name 0 in - tt " check name='%s'@\n" name ; result + tt " check name='%s'@\n" name ; + result | _ -> - tt " check name-unknown@\n" ; false + tt " check name-unknown@\n" ; + false in let pattern_len = Option.map ~f:List.length label.ToplAst.arguments in let match_args () = @@ -65,8 +67,16 @@ let evaluate_static_guard label_o (e_fun, arg_ts) = in tt "match name-pattern='%s' arg-len-pattern=%a@\n" label.ToplAst.procedure_name (Pp.option Int.pp) pattern_len ; - let log f = f () || (tt " match result FALSE@\n" ; false) in - log match_args && log match_name && (tt " match result TRUE@\n" ; true) + let log f = + f () + || + ( tt " match result FALSE@\n" ; + false ) + in + log match_args && log match_name + && + ( tt " match result TRUE@\n" ; + true ) in Option.value_map ~default:true ~f:evaluate_nonany label_o @@ -130,7 +140,11 @@ let add_types tenv = let record_predicate = ToplAst.( function - | Binop (_, v1, v2) -> record_value v1 ; record_value v2 | Value v -> record_value v) + | Binop (_, v1, v2) -> + record_value v1 ; + record_value v2 + | Value v -> + record_value v) in let record_assignment (reg, _) = record reg in let record_label label = @@ -163,7 +177,9 @@ let instrument tenv procdesc = let f _node = instrument_instruction in tt "instrument@\n" ; let _updated = Procdesc.replace_instrs_by procdesc ~f in - tt "add types@\n" ; add_types tenv ; tt "done@\n" ) + tt "add types@\n" ; + add_types tenv ; + tt "done@\n" ) (** [lookup_static_var var prop] expects [var] to have the form [Exp.Lfield (obj, fieldname)], and diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml index 1097dae2e..ab04209f9 100644 --- a/infer/src/topl/ToplAutomaton.ml +++ b/infer/src/topl/ToplAutomaton.ml @@ -101,7 +101,8 @@ let make properties = let vcount = Array.length states in let a = Array.create ~len:vcount [] in let f i t = a.(t.source) <- i :: a.(t.source) in - Array.iteri ~f transitions ; a + Array.iteri ~f transitions ; + a in let max_args = let llen l = Option.value_map ~default:0 ~f:List.length l.ToplAst.arguments in @@ -125,7 +126,8 @@ let make properties = in List.iter ~f:set_nondet nondet in - List.iter ~f properties ; a + List.iter ~f properties ; + a in let skips : bool array = (* TODO(rgrigore): Rename "anys"? *) diff --git a/infer/src/topl/ToplMonitor.ml b/infer/src/topl/ToplMonitor.ml index 74d508e00..e2c1f9da9 100644 --- a/infer/src/topl/ToplMonitor.ml +++ b/infer/src/topl/ToplMonitor.ml @@ -32,7 +32,9 @@ let formals_of_procname proc_name = let params = Procname.get_parameters proc_name in let new_arg_name = let n = ref (-1) in - fun () -> incr n ; ToplName.arg !n + fun () -> + incr n ; + ToplName.arg !n in let f t = let name = Mangled.from_string (new_arg_name ()) in diff --git a/infer/src/unit/LRUHashtblTests.ml b/infer/src/unit/LRUHashtblTests.ml index ecf660236..868f7b6db 100644 --- a/infer/src/unit/LRUHashtblTests.ml +++ b/infer/src/unit/LRUHashtblTests.ml @@ -14,7 +14,8 @@ let inputs = ; ( "singleton" , (fun () -> let map = LRUHash.create ~initial_size:5 ~max_size:3 in - LRUHash.replace map 0 10 ; map ) + LRUHash.replace map 0 10 ; + map ) , [(0, 10)] ) ; ( "LRU1" , (fun () -> @@ -23,7 +24,9 @@ let inputs = LRUHash.replace map 1 10 ; LRUHash.replace map 2 10 ; let (_ : int option) = LRUHash.find_opt map 1 in - LRUHash.replace map 3 10 ; LRUHash.replace map 4 10 ; map ) + LRUHash.replace map 3 10 ; + LRUHash.replace map 4 10 ; + map ) , [(1, 10); (3, 10); (4, 10)] ) ; ( "LRU2" , (fun () -> diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 257bbdc22..b44e511a8 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -57,7 +57,10 @@ module StructuredSil = struct let label_counter = ref 0 - let fresh_label () = incr label_counter ; !label_counter + let fresh_label () = + incr label_counter ; + !label_counter + let invariant inv_str = Invariant (inv_str, fresh_label ())