From dd8b8e6d2ed76b8c40bf086137b88732070a0a31 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 14 Oct 2016 10:04:23 -0700 Subject: [PATCH] [reason] reformat with new version of reason Summary: Converted by executing: ``` cd infer/src find . -name "*.re" -or -name "*.rei" -exec ../../scripts/reup.sh {} \; ``` and fixed a few broken comments. Reviewed By: jvillard Differential Revision: D4021262 fbshipit-source-id: 0223287 --- infer/src/IR/Annot.re | 3 +- infer/src/IR/Annot.rei | 3 +- infer/src/IR/AttributesTable.re | 37 +++-- infer/src/IR/AttributesTable.rei | 5 +- infer/src/IR/Binop.re | 4 +- infer/src/IR/Binop.rei | 4 +- infer/src/IR/CallFlags.re | 7 +- infer/src/IR/CallFlags.rei | 1 - infer/src/IR/Cfg.re | 173 ++++++++++++------------ infer/src/IR/Cfg.rei | 15 ++- infer/src/IR/Cg.re | 7 +- infer/src/IR/Cg.rei | 2 +- infer/src/IR/Const.re | 14 +- infer/src/IR/Const.rei | 14 +- infer/src/IR/Csu.re | 17 ++- infer/src/IR/Csu.rei | 15 ++- infer/src/IR/DecompiledExp.re | 25 ++-- infer/src/IR/DecompiledExp.rei | 25 ++-- infer/src/IR/Exp.re | 41 ++---- infer/src/IR/Exp.rei | 24 ++-- infer/src/IR/Ident.re | 13 +- infer/src/IR/Ident.rei | 4 +- infer/src/IR/IntLit.re | 1 - infer/src/IR/IntLit.rei | 1 - infer/src/IR/Location.re | 4 - infer/src/IR/Location.rei | 4 - infer/src/IR/Mangled.re | 1 - infer/src/IR/Mangled.rei | 2 +- infer/src/IR/PredSymb.re | 49 +++---- infer/src/IR/PredSymb.rei | 34 +++-- infer/src/IR/ProcAttributes.re | 8 +- infer/src/IR/ProcAttributes.rei | 8 +- infer/src/IR/Procname.re | 61 ++++----- infer/src/IR/Procname.rei | 13 +- infer/src/IR/Pvar.re | 11 +- infer/src/IR/Pvar.rei | 1 - infer/src/IR/Sil.re | 91 +++++++------ infer/src/IR/Sil.rei | 64 +++++---- infer/src/IR/StructTyp.re | 4 +- infer/src/IR/StructTyp.rei | 1 - infer/src/IR/Subtype.re | 8 +- infer/src/IR/Subtype.rei | 1 - infer/src/IR/Tenv.re | 5 +- infer/src/IR/Tenv.rei | 4 - infer/src/IR/Typ.re | 13 +- infer/src/IR/Typ.rei | 13 +- infer/src/IR/Typename.re | 7 +- infer/src/IR/Typename.rei | 8 +- infer/src/IR/Unop.re | 1 - infer/src/IR/Unop.rei | 1 - infer/src/backend/InferAnalyze.re | 1 - infer/src/backend/InferAnalyze.rei | 2 - infer/src/backend/InferPrint.re | 138 ++++++++++--------- infer/src/backend/PropUtil.re | 187 +++++++++++++------------- infer/src/backend/PropUtil.rei | 4 - infer/src/base/StatisticsToolbox.re | 6 +- infer/src/base/StatisticsToolbox.rei | 4 - infer/src/clang/Capture.re | 18 ++- infer/src/clang/Capture.rei | 1 - infer/src/clang/ClangCommand.re | 80 +++++------ infer/src/clang/ClangCommand.rei | 9 +- infer/src/clang/InferClang.re | 17 +-- infer/src/scripts/StatsAggregator.re | 16 +-- infer/src/scripts/StatsAggregator.rei | 4 - infer/src/scripts/checkCopyright.ml | 4 +- scripts/reup.sh | 16 +++ 66 files changed, 673 insertions(+), 706 deletions(-) create mode 100755 scripts/reup.sh diff --git a/infer/src/IR/Annot.re b/infer/src/IR/Annot.re index f8e52106d..92918530d 100644 --- a/infer/src/IR/Annot.re +++ b/infer/src/IR/Annot.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -48,6 +47,7 @@ let module Map = PrettyPrintable.MakePPMap { }; let module Item = { + /** Annotation for one item: a list of annotations with visibility. */ type nonrec t = list (t, bool); @@ -90,6 +90,7 @@ let module Class = { }; let module Method = { + /** Annotation for a method: return value and list of parameters. */ type t = (Item.t, list Item.t); diff --git a/infer/src/IR/Annot.rei b/infer/src/IR/Annot.rei index f5a93b596..34c3b352e 100644 --- a/infer/src/IR/Annot.rei +++ b/infer/src/IR/Annot.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -35,6 +34,7 @@ let pp: F.formatter => t => unit; let module Map: PrettyPrintable.PPMap with type key = t; let module Item: { + /** Annotation for one item: a list of annotations with visibility. */ type nonrec t = list (t, bool); @@ -55,6 +55,7 @@ let module Item: { let module Class: {let objc: Item.t; let cpp: Item.t;}; let module Method: { + /** Annotation for a method: return value and list of parameters. */ type t = (Item.t, list Item.t); diff --git a/infer/src/IR/AttributesTable.re b/infer/src/IR/AttributesTable.re index 81749d267..370a99253 100644 --- a/infer/src/IR/AttributesTable.re +++ b/infer/src/IR/AttributesTable.re @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2015 - present Facebook, Inc. * All rights reserved. * @@ -9,7 +6,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; let module F = Format; @@ -48,19 +44,20 @@ let res_dir_attr_filename pname => { let store_attributes (proc_attributes: ProcAttributes.t) => { let proc_name = proc_attributes.proc_name; let attributes_file = res_dir_attr_filename proc_name; - let should_write = not (DB.file_exists attributes_file) || ( - switch (Serialization.from_file serializer attributes_file) { - | None => true - | Some proc_attributes_on_disk => - let higher_rank_than_on_disk () => - proc_attributes.is_defined && + let should_write = + not (DB.file_exists attributes_file) || ( + switch (Serialization.from_file serializer attributes_file) { + | None => true + | Some proc_attributes_on_disk => + let higher_rank_than_on_disk () => + proc_attributes.is_defined && DB.source_file_compare proc_attributes.loc.file proc_attributes_on_disk.loc.file > 0; - let becomes_defined = proc_attributes.is_defined && not proc_attributes_on_disk.is_defined; - /* Only overwrite the attribute file if the procedure becomes defined - or its associated file has higher rank (alphabetically) than on disk. */ - becomes_defined || higher_rank_than_on_disk () - } - ); + let becomes_defined = proc_attributes.is_defined && not proc_attributes_on_disk.is_defined; + /* Only overwrite the attribute file if the procedure becomes defined + or its associated file has higher rank (alphabetically) than on disk. */ + becomes_defined || higher_rank_than_on_disk () + } + ); if should_write { Serialization.to_file serializer attributes_file proc_attributes } @@ -132,13 +129,12 @@ let to_json at => { ("num_bindings", `Int at.num_bindings), ("num_buckets", `Int at.num_buckets), ("max_bucket_length", `Int at.max_bucket_length) - ] - @ extra_field + ] @ extra_field ) }; let from_json json => { - let open! Yojson.Basic.Util; + open! Yojson.Basic.Util; { num_bindings: json |> member "num_bindings" |> to_int, num_buckets: json |> member "num_buckets" |> to_int, @@ -165,7 +161,8 @@ let stats () => { let stats = Procname.Hash.stats attr_tbl; let {Hashtbl.num_bindings: num_bindings, num_buckets, max_bucket_length} = stats; let serialized_size_kb = - Config.developer_mode ? Some (Marshal.data_size (Marshal.to_bytes attr_tbl []) 0 / 1024) : None; + Config.developer_mode ? + Some (Marshal.data_size (Marshal.to_bytes attr_tbl []) 0 / 1024) : None; {num_bindings, num_buckets, max_bucket_length, serialized_size_kb} }; diff --git a/infer/src/IR/AttributesTable.rei b/infer/src/IR/AttributesTable.rei index 016bd56ed..50515c6e9 100644 --- a/infer/src/IR/AttributesTable.rei +++ b/infer/src/IR/AttributesTable.rei @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2015 - present Facebook, Inc. * All rights reserved. * @@ -9,8 +6,8 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ -/** Module to manage the table of attributes. */ +/** Module to manage the table of attributes. */ open! Utils; diff --git a/infer/src/IR/Binop.re b/infer/src/IR/Binop.re index c345ff1fc..0139fa94d 100644 --- a/infer/src/IR/Binop.re +++ b/infer/src/IR/Binop.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -43,8 +42,7 @@ type t = | BOr /** inclusive-or */ | LAnd /** logical and. Does not always evaluate both operands. */ | LOr /** logical or. Does not always evaluate both operands. */ - | PtrFld /** field offset via pointer to field: takes the address of a - Csu.t and a Cptr_to_fld constant to form an Lfield expression (see prop.ml) */; + | PtrFld /** field offset via pointer to field: takes the address of a Csu.t and a Cptr_to_fld constant to form an Lfield expression (see prop.ml) */; let compare o1 o2 => switch (o1, o2) { diff --git a/infer/src/IR/Binop.rei b/infer/src/IR/Binop.rei index 48510ff5b..5155ff701 100644 --- a/infer/src/IR/Binop.rei +++ b/infer/src/IR/Binop.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -43,8 +42,7 @@ type t = | BOr /** inclusive-or */ | LAnd /** logical and. Does not always evaluate both operands. */ | LOr /** logical or. Does not always evaluate both operands. */ - | PtrFld /** field offset via pointer to field: takes the address of a - Csu.t and a Cptr_to_fld constant to form an Lfield expression (see prop.ml) */; + | PtrFld /** field offset via pointer to field: takes the address of a Csu.t and a Cptr_to_fld constant to form an Lfield expression (see prop.ml) */; let equal: t => t => bool; diff --git a/infer/src/IR/CallFlags.re b/infer/src/IR/CallFlags.re index 3ddee7557..b2daa88b0 100644 --- a/infer/src/IR/CallFlags.re +++ b/infer/src/IR/CallFlags.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -31,9 +30,9 @@ type t = { let compare cflag1 cflag2 => bool_compare cflag1.cf_virtual cflag2.cf_virtual |> - next bool_compare cflag1.cf_interface cflag2.cf_interface |> - next bool_compare cflag1.cf_noreturn cflag2.cf_noreturn |> - next bool_compare cflag1.cf_is_objc_block cflag2.cf_is_objc_block; + next bool_compare cflag1.cf_interface cflag2.cf_interface |> + next bool_compare cflag1.cf_noreturn cflag2.cf_noreturn |> + next bool_compare cflag1.cf_is_objc_block cflag2.cf_is_objc_block; let pp f cf => { if cf.cf_virtual { diff --git a/infer/src/IR/CallFlags.rei b/infer/src/IR/CallFlags.rei index 0de3632cd..c595f917a 100644 --- a/infer/src/IR/CallFlags.rei +++ b/infer/src/IR/CallFlags.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index 266b5ea0e..b7104eb3f 100644 --- a/infer/src/IR/Cfg.re +++ b/infer/src/IR/Cfg.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; let module L = Logging; @@ -22,12 +21,12 @@ let module F = Format; let module Node = { type id = int; type nodekind = - | Start_node of proc_desc - | Exit_node of proc_desc - | Stmt_node of string + | Start_node proc_desc + | Exit_node proc_desc + | Stmt_node string | Join_node - | Prune_node of bool Sil.if_kind string /** (true/false branch, if_kind, comment) */ - | Skip_node of string + | Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */ + | Skip_node string /** a node */ and t = { /** unique id of the node */ @@ -84,59 +83,56 @@ let module Node = { /** compute the list of procedures added or changed in [cfg_new] over [cfg_old] */ let mark_unchanged_pdescs cfg_new cfg_old => { - let pdescs_eq pd1 pd2 => + let pdescs_eq pd1 pd2 => { /* map of exp names in pd1 -> exp names in pd2 */ - { - let exp_map = ref Exp.Map.empty; - /* map of node id's in pd1 -> node id's in pd2 */ - let id_map = ref IntMap.empty; - /* formals are the same if their types are the same */ - let formals_eq formals1 formals2 => - IList.equal (fun (_, typ1) (_, typ2) => Typ.compare typ1 typ2) formals1 formals2; - let nodes_eq n1s n2s => - /* nodes are the same if they have the same id, instructions, and succs/preds up to renaming - with [exp_map] and [id_map] */ - { - let node_eq n1 n2 => { - let id_compare n1 n2 => { - let (id1, id2) = (n1.nd_id, n2.nd_id); - try { - let id1_mapping = IntMap.find id1 !id_map; - Pervasives.compare id1_mapping id2 - } { - | Not_found => - /* assume id's are equal and enforce by adding to [id_map] */ - id_map := IntMap.add id1 id2 !id_map; - 0 - } - }; - let instrs_eq instrs1 instrs2 => - IList.equal - ( - fun i1 i2 => { - let (n, exp_map') = Sil.instr_compare_structural i1 i2 !exp_map; - exp_map := exp_map'; - n - } - ) - instrs1 - instrs2; - id_compare n1 n2 == 0 && - IList.equal id_compare n1.nd_succs n2.nd_succs && - IList.equal id_compare n1.nd_preds n2.nd_preds && - instrs_eq n1.nd_instrs n2.nd_instrs - }; - try (IList.for_all2 node_eq n1s n2s) { - | Invalid_argument _ => false + let exp_map = ref Exp.Map.empty; + /* map of node id's in pd1 -> node id's in pd2 */ + let id_map = ref IntMap.empty; + /* formals are the same if their types are the same */ + let formals_eq formals1 formals2 => + IList.equal (fun (_, typ1) (_, typ2) => Typ.compare typ1 typ2) formals1 formals2; + let nodes_eq n1s n2s => { + /* nodes are the same if they have the same id, instructions, and succs/preds up to renaming + with [exp_map] and [id_map] */ + let node_eq n1 n2 => { + let id_compare n1 n2 => { + let (id1, id2) = (n1.nd_id, n2.nd_id); + try { + let id1_mapping = IntMap.find id1 !id_map; + Pervasives.compare id1_mapping id2 + } { + | Not_found => + /* assume id's are equal and enforce by adding to [id_map] */ + id_map := IntMap.add id1 id2 !id_map; + 0 } }; - let att1 = pd1.pd_attributes - and att2 = pd2.pd_attributes; - att1.ProcAttributes.is_defined == att2.ProcAttributes.is_defined && - Typ.equal att1.ProcAttributes.ret_type att2.ProcAttributes.ret_type && - formals_eq att1.ProcAttributes.formals att2.ProcAttributes.formals && - nodes_eq pd1.pd_nodes pd2.pd_nodes + let instrs_eq instrs1 instrs2 => + IList.equal + ( + fun i1 i2 => { + let (n, exp_map') = Sil.instr_compare_structural i1 i2 !exp_map; + exp_map := exp_map'; + n + } + ) + instrs1 + instrs2; + id_compare n1 n2 == 0 && + IList.equal id_compare n1.nd_succs n2.nd_succs && + IList.equal id_compare n1.nd_preds n2.nd_preds && instrs_eq n1.nd_instrs n2.nd_instrs + }; + try (IList.for_all2 node_eq n1s n2s) { + | Invalid_argument _ => false + } }; + let att1 = pd1.pd_attributes + and att2 = pd2.pd_attributes; + att1.ProcAttributes.is_defined == att2.ProcAttributes.is_defined && + Typ.equal att1.ProcAttributes.ret_type att2.ProcAttributes.ret_type && + formals_eq att1.ProcAttributes.formals att2.ProcAttributes.formals && + nodes_eq pd1.pd_nodes pd2.pd_nodes + }; let old_procs = cfg_old.name_pdesc_tbl; let new_procs = cfg_new.name_pdesc_tbl; let mark_pdesc_if_unchanged pname new_pdesc => @@ -145,7 +141,7 @@ let module Node = { let changed = /* in continue_capture mode keep the old changed bit */ Config.continue_capture && old_pdesc.pd_attributes.ProcAttributes.changed || - not (pdescs_eq old_pdesc new_pdesc); + not (pdescs_eq old_pdesc new_pdesc); new_pdesc.pd_attributes.changed = changed } { | Not_found => () @@ -394,7 +390,8 @@ let module Node = { /** Replace the instructions to be executed. */ let replace_instrs node instrs => node.nd_instrs = instrs; - let proc_desc_get_ret_var pdesc => Pvar.get_ret_pvar pdesc.pd_attributes.ProcAttributes.proc_name; + let proc_desc_get_ret_var pdesc => + Pvar.get_ret_pvar pdesc.pd_attributes.ProcAttributes.proc_name; /** Add declarations for local variables and return variable to the node */ let add_locals_ret_declaration node locals => { @@ -480,7 +477,8 @@ let module Node = { /** Return [true] iff the procedure is defined, and not just declared */ let proc_desc_is_defined proc_desc => proc_desc.pd_attributes.ProcAttributes.is_defined; - let proc_desc_is_java_synchroinized proc_desc => proc_desc.pd_attributes.ProcAttributes.is_java_synchronized_method; + let proc_desc_is_java_synchroinized proc_desc => + proc_desc.pd_attributes.ProcAttributes.is_java_synchronized_method; let proc_desc_get_loc proc_desc => proc_desc.pd_attributes.ProcAttributes.loc; /** Return name and type of formal parameters */ @@ -513,7 +511,8 @@ let module Node = { proc_desc.pd_attributes.ProcAttributes.locals @ new_locals; /** check or indicate if we have performed preanalysis on the CFG */ - let proc_desc_did_preanalysis proc_desc => proc_desc.pd_attributes.ProcAttributes.did_preanalysis; + let proc_desc_did_preanalysis proc_desc => + proc_desc.pd_attributes.ProcAttributes.did_preanalysis; let proc_desc_signal_did_preanalysis proc_desc => proc_desc.pd_attributes.ProcAttributes.did_preanalysis = true; @@ -593,7 +592,8 @@ let module Node = { IList.fold_left f acc (IList.rev (proc_desc_get_nodes proc_desc)); let proc_desc_fold_calls f acc pdesc => { let do_node a node => - IList.fold_left (fun b callee_pname => f b (callee_pname, get_loc node)) a (get_callees node); + IList.fold_left + (fun b callee_pname => f b (callee_pname, get_loc node)) a (get_callees node); IList.fold_left do_node acc (proc_desc_get_nodes pdesc) }; @@ -826,6 +826,7 @@ let module Procdesc = { }; /* =============== END of module Procdesc =============== */ + /** Hash table with nodes as keys. */ let module NodeHash = Hashtbl.Make Node; @@ -920,12 +921,11 @@ let save_source_files cfg => { let dest_file_str = DB.filename_to_string dest_file; let needs_copy = Node.proc_desc_is_defined pdesc && - Sys.file_exists source_file_str && - ( - not (Sys.file_exists dest_file_str) || - DB.file_modified_time (DB.filename_from_string source_file_str) > - DB.file_modified_time dest_file - ); + Sys.file_exists source_file_str && ( + not (Sys.file_exists dest_file_str) || + DB.file_modified_time (DB.filename_from_string source_file_str) > + DB.file_modified_time dest_file + ); if needs_copy { switch (copy_file source_file_str dest_file_str) { | Some _ => () @@ -982,11 +982,7 @@ let inline_synthetic_method ret_id etl proc_desc loc_call :option Sil.instr => { /* getter for static fields */ let instr' = Sil.Load ret_id (Exp.Lfield (Exp.Lvar pvar) fn ft) bt loc_call; found instr instr' - | ( - Sil.Store (Exp.Lfield _ fn ft) bt _ _, - _, - [(e1, _), (e2, _)] /* setter for fields */ - ) => + | (Sil.Store (Exp.Lfield _ fn ft) bt _ _, _, [(e1, _), (e2, _)] /* setter for fields */) => let instr' = Sil.Store (Exp.Lfield e1 fn ft) bt e2 loc_call; found instr instr' | (Sil.Store (Exp.Lfield (Exp.Lvar pvar) fn ft) bt _ _, _, [(e1, _)]) when Pvar.is_global pvar => @@ -1087,22 +1083,21 @@ let store_cfg_to_file (name, typ) where name is a parameter. The resulting proc desc is isomorphic but all the type of the parameters are replaced in the instructions according to the list. The virtual calls are also replaced to match the parameter types */ -let specialize_types callee_proc_desc resolved_proc_name args => - /** TODO (#9333890): This currently only works when the callee is defined in the same file. - Add support to search for the callee procedure description in the execution environment */ - { - let callee_attributes = Procdesc.get_attributes callee_proc_desc; - let resolved_formals = - IList.fold_left2 - (fun accu (name, _) (_, arg_typ) => [(name, arg_typ), ...accu]) - [] - callee_attributes.ProcAttributes.formals - args |> IList.rev; - let resolved_attributes = { - ...callee_attributes, - ProcAttributes.formals: resolved_formals, - proc_name: resolved_proc_name - }; - AttributesTable.store_attributes resolved_attributes; - Procdesc.specialize_types callee_proc_desc resolved_attributes resolved_formals +let specialize_types callee_proc_desc resolved_proc_name args => { + /* TODO (#9333890): This currently only works when the callee is defined in the same file. + Add support to search for the callee procedure description in the execution environment */ + let callee_attributes = Procdesc.get_attributes callee_proc_desc; + let resolved_formals = + IList.fold_left2 + (fun accu (name, _) (_, arg_typ) => [(name, arg_typ), ...accu]) + [] + callee_attributes.ProcAttributes.formals + args |> IList.rev; + let resolved_attributes = { + ...callee_attributes, + ProcAttributes.formals: resolved_formals, + proc_name: resolved_proc_name }; + AttributesTable.store_attributes resolved_attributes; + Procdesc.specialize_types callee_proc_desc resolved_attributes resolved_formals +}; diff --git a/infer/src/IR/Cfg.rei b/infer/src/IR/Cfg.rei index 8f595b0ba..794f382c6 100644 --- a/infer/src/IR/Cfg.rei +++ b/infer/src/IR/Cfg.rei @@ -10,11 +10,11 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; /** Control Flow Graph for Interprocedural Analysis */ + /** {2 ADT node and proc_desc} */ type node; @@ -32,6 +32,7 @@ let store_cfg_to_file: /** proc description */ let module Procdesc: { + /** proc description */ type t; @@ -49,6 +50,7 @@ let module Procdesc: { /** [remove cfg name remove_nodes] remove the procdesc [name] from the control flow graph [cfg]. */ + /** It also removes all the nodes from the procedure from the cfg if remove_nodes is true */ let remove: cfg => Procname.t => bool => unit; @@ -138,12 +140,12 @@ let module Node: { /** kind of cfg node */ type nodekind = - | Start_node of Procdesc.t - | Exit_node of Procdesc.t - | Stmt_node of string + | Start_node Procdesc.t + | Exit_node Procdesc.t + | Stmt_node string | Join_node - | Prune_node of bool Sil.if_kind string /** (true/false branch, if_kind, comment) */ - | Skip_node of string; + | Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */ + | Skip_node string; /** kind of Stmt_node for an exception handler. */ let exn_handler_kind: nodekind; @@ -286,6 +288,7 @@ let pp_node_list: Format.formatter => list Node.t => unit; /** {2 Functions for manipulating an interprocedural CFG} */ + /** Iterate over all the procdesc's */ let iter_proc_desc: cfg => (Procname.t => Procdesc.t => unit) => unit; diff --git a/infer/src/IR/Cg.re b/infer/src/IR/Cg.re index 8ba75cbf3..5deb6c9f2 100644 --- a/infer/src/IR/Cg.re +++ b/infer/src/IR/Cg.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -235,10 +234,8 @@ let get_edges (g: t) :list ((node, int), (node, int)) => { let f node info => Procname.Set.iter ( - fun nto => edges := [ - (node_get_num_ancestors g node, node_get_num_ancestors g nto), - ...!edges - ] + fun nto => + edges := [(node_get_num_ancestors g node, node_get_num_ancestors g nto), ...!edges] ) info.children; node_map_iter f g; diff --git a/infer/src/IR/Cg.rei b/infer/src/IR/Cg.rei index d4106faf8..2e2974164 100644 --- a/infer/src/IR/Cg.rei +++ b/infer/src/IR/Cg.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -29,6 +28,7 @@ type t; /** the type of a call graph */ [n1] is the parent and [n2] is the child. Node [n1] is dependent on [n2] if there is a path from [n1] to [n2] using the child relationship. */ + /** [add_edge cg f t] adds an edge from [f] to [t] in the call graph [cg]. The nodes are also added as undefined, unless already present. */ let add_edge: t => Procname.t => Procname.t => unit; diff --git a/infer/src/IR/Const.re b/infer/src/IR/Const.re index 898c2946e..8fde16d39 100644 --- a/infer/src/IR/Const.re +++ b/infer/src/IR/Const.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -20,13 +19,12 @@ let module L = Logging; let module F = Format; type t = - | Cint of IntLit.t /** integer constants */ - | Cfun of Procname.t /** function names */ - | Cstr of string /** string constants */ - | Cfloat of float /** float constants */ - | Cclass of Ident.name /** class constant */ - | Cptr_to_fld of Ident.fieldname Typ.t /** pointer to field constant, - and type of the surrounding Csu.t type */; + | Cint IntLit.t /** integer constants */ + | Cfun Procname.t /** function names */ + | Cstr string /** string constants */ + | Cfloat float /** float constants */ + | Cclass Ident.name /** class constant */ + | Cptr_to_fld Ident.fieldname Typ.t /** pointer to field constant, and type of the surrounding Csu.t type */; let compare (c1: t) (c2: t) :int => switch (c1, c2) { diff --git a/infer/src/IR/Const.rei b/infer/src/IR/Const.rei index da4905967..321e06f89 100644 --- a/infer/src/IR/Const.rei +++ b/infer/src/IR/Const.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -22,13 +21,12 @@ let module F = Format; /** Constants */ type t = - | Cint of IntLit.t /** integer constants */ - | Cfun of Procname.t /** function names */ - | Cstr of string /** string constants */ - | Cfloat of float /** float constants */ - | Cclass of Ident.name /** class constant */ - | Cptr_to_fld of Ident.fieldname Typ.t /** pointer to field constant, - and type of the surrounding Csu.t type */; + | Cint IntLit.t /** integer constants */ + | Cfun Procname.t /** function names */ + | Cstr string /** string constants */ + | Cfloat float /** float constants */ + | Cclass Ident.name /** class constant */ + | Cptr_to_fld Ident.fieldname Typ.t /** pointer to field constant, and type of the surrounding Csu.t type */; let compare: t => t => int; diff --git a/infer/src/IR/Csu.re b/infer/src/IR/Csu.re index 82da96564..dcba9cdd2 100644 --- a/infer/src/IR/Csu.re +++ b/infer/src/IR/Csu.re @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2015 - present Facebook, Inc. * All rights reserved. * @@ -9,16 +6,22 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; /** Internal representation of data structure for Java, Objective-C and C++ classes, C-style structs struct and union, And Objective C protocol */ -type class_kind = | CPP | Java | Objc; - -type t = | Class of class_kind | Struct | Union | Protocol; +type class_kind = + | CPP + | Java + | Objc; + +type t = + | Class class_kind + | Struct + | Union + | Protocol; let name = fun diff --git a/infer/src/IR/Csu.rei b/infer/src/IR/Csu.rei index 70675e89d..649777aea 100644 --- a/infer/src/IR/Csu.rei +++ b/infer/src/IR/Csu.rei @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2015 - present Facebook, Inc. * All rights reserved. * @@ -9,16 +6,22 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; /** Internal representation of data structure for Java, Objective-C and C++ classes, C-style structs struct and union, And Objective C protocol */ -type class_kind = | CPP | Java | Objc; +type class_kind = + | CPP + | Java + | Objc; -type t = | Class of class_kind | Struct | Union | Protocol; +type t = + | Class class_kind + | Struct + | Union + | Protocol; let name: t => string; diff --git a/infer/src/IR/DecompiledExp.re b/infer/src/IR/DecompiledExp.re index d4e5ac4a9..196c07b33 100644 --- a/infer/src/IR/DecompiledExp.re +++ b/infer/src/IR/DecompiledExp.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -22,19 +21,19 @@ let module F = Format; /** expression representing the result of decompilation */ type t = - | Darray of t t - | Dbinop of Binop.t t t - | Dconst of Const.t - | Dsizeof of Typ.t (option t) Subtype.t - | Dderef of t - | Dfcall of t (list t) Location.t CallFlags.t - | Darrow of t Ident.fieldname - | Ddot of t Ident.fieldname - | Dpvar of Pvar.t - | Dpvaraddr of Pvar.t - | Dunop of Unop.t t + | Darray t t + | Dbinop Binop.t t t + | Dconst Const.t + | Dsizeof Typ.t (option t) Subtype.t + | Dderef t + | Dfcall t (list t) Location.t CallFlags.t + | Darrow t Ident.fieldname + | Ddot t Ident.fieldname + | Dpvar Pvar.t + | Dpvaraddr Pvar.t + | Dunop Unop.t t | Dunknown - | Dretcall of t (list t) Location.t CallFlags.t; + | Dretcall t (list t) Location.t CallFlags.t; /** Value paths: identify an occurrence of a value in a symbolic heap diff --git a/infer/src/IR/DecompiledExp.rei b/infer/src/IR/DecompiledExp.rei index 3d8cf2341..c141cca91 100644 --- a/infer/src/IR/DecompiledExp.rei +++ b/infer/src/IR/DecompiledExp.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -22,19 +21,19 @@ let module F = Format; /** expression representing the result of decompilation */ type t = - | Darray of t t - | Dbinop of Binop.t t t - | Dconst of Const.t - | Dsizeof of Typ.t (option t) Subtype.t - | Dderef of t - | Dfcall of t (list t) Location.t CallFlags.t - | Darrow of t Ident.fieldname - | Ddot of t Ident.fieldname - | Dpvar of Pvar.t - | Dpvaraddr of Pvar.t - | Dunop of Unop.t t + | Darray t t + | Dbinop Binop.t t t + | Dconst Const.t + | Dsizeof Typ.t (option t) Subtype.t + | Dderef t + | Dfcall t (list t) Location.t CallFlags.t + | Darrow t Ident.fieldname + | Ddot t Ident.fieldname + | Dpvar Pvar.t + | Dpvaraddr Pvar.t + | Dunop Unop.t t | Dunknown - | Dretcall of t (list t) Location.t CallFlags.t; + | Dretcall t (list t) Location.t CallFlags.t; /** Value paths: identify an occurrence of a value in a symbolic heap diff --git a/infer/src/IR/Exp.re b/infer/src/IR/Exp.re index 231706953..3c215c668 100644 --- a/infer/src/IR/Exp.re +++ b/infer/src/IR/Exp.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -25,31 +24,31 @@ and dynamic_length = option t /** Program expressions. */ and t = /** Pure variable: it is not an lvalue */ - | Var of Ident.t + | Var Ident.t /** Unary operator with type of the result if known */ - | UnOp of Unop.t t (option Typ.t) + | UnOp Unop.t t (option Typ.t) /** Binary operator */ - | BinOp of Binop.t t t + | BinOp Binop.t t t /** Exception */ - | Exn of t + | Exn t /** Anonymous function */ - | Closure of closure + | Closure closure /** Constants */ - | Const of Const.t + | Const Const.t /** Type cast */ - | Cast of Typ.t t + | Cast Typ.t t /** The address of a program variable */ - | Lvar of Pvar.t + | Lvar Pvar.t /** A field offset, the type is the surrounding struct type */ - | Lfield of t Ident.fieldname Typ.t + | Lfield t Ident.fieldname Typ.t /** An array index offset: [exp1\[exp2\]] */ - | Lindex of t t + | Lindex t t /** A sizeof expression. [Sizeof (Tarray elt (Some static_length)) (Some dynamic_length)] represents the size of an array value consisting of [dynamic_length] elements of type [elt]. The [dynamic_length], tracked by symbolic execution, may differ from the [static_length] obtained from the type definition, e.g. when an array is over-allocated. For struct types, the [dynamic_length] is that of the final extensible array, if any. */ - | Sizeof of Typ.t dynamic_length Subtype.t; + | Sizeof Typ.t dynamic_length Subtype.t; /** Compare expressions. Variables come before other expressions. */ @@ -209,6 +208,7 @@ let is_zero = /** {2 Utility Functions for Expressions} */ + /** Turn an expression representing a type into the type it represents If not a sizeof, return the default type if given, otherwise raise an exception */ let texp_to_typ default_opt => @@ -243,15 +243,7 @@ let rec pointer_arith = | _ => false; let get_undefined footprint => - Var ( - Ident.create_fresh ( - if footprint { - Ident.kfootprint - } else { - Ident.kprimed - } - ) - ); + Var (Ident.create_fresh (if footprint {Ident.kfootprint} else {Ident.kprimed})); /** Create integer constant */ @@ -279,12 +271,7 @@ let minus_one = int IntLit.minus_one; /** Create integer constant corresponding to the boolean value */ -let bool b => - if b { - one - } else { - zero - }; +let bool b => if b {one} else {zero}; /** Create expresstion [e1 == e2] */ diff --git a/infer/src/IR/Exp.rei b/infer/src/IR/Exp.rei index 0352bc3c9..d847cd8db 100644 --- a/infer/src/IR/Exp.rei +++ b/infer/src/IR/Exp.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -25,31 +24,31 @@ and dynamic_length = option t /** Program expressions. */ and t = /** Pure variable: it is not an lvalue */ - | Var of Ident.t + | Var Ident.t /** Unary operator with type of the result if known */ - | UnOp of Unop.t t (option Typ.t) + | UnOp Unop.t t (option Typ.t) /** Binary operator */ - | BinOp of Binop.t t t + | BinOp Binop.t t t /** Exception */ - | Exn of t + | Exn t /** Anonymous function */ - | Closure of closure + | Closure closure /** Constants */ - | Const of Const.t + | Const Const.t /** Type cast */ - | Cast of Typ.t t + | Cast Typ.t t /** The address of a program variable */ - | Lvar of Pvar.t + | Lvar Pvar.t /** A field offset, the type is the surrounding struct type */ - | Lfield of t Ident.fieldname Typ.t + | Lfield t Ident.fieldname Typ.t /** An array index offset: [exp1\[exp2\]] */ - | Lindex of t t + | Lindex t t /** A sizeof expression. [Sizeof (Tarray elt (Some static_length)) (Some dynamic_length)] represents the size of an array value consisting of [dynamic_length] elements of type [elt]. The [dynamic_length], tracked by symbolic execution, may differ from the [static_length] obtained from the type definition, e.g. when an array is over-allocated. For struct types, the [dynamic_length] is that of the final extensible array, if any. */ - | Sizeof of Typ.t dynamic_length Subtype.t; + | Sizeof Typ.t dynamic_length Subtype.t; /** Comparison for expressions. */ @@ -89,6 +88,7 @@ let is_zero: t => bool; /** {2 Utility Functions for Expressions} */ + /** Turn an expression representing a type into the type it represents If not a sizeof, return the default type if given, otherwise raise an exception */ let texp_to_typ: option Typ.t => t => Typ.t; diff --git a/infer/src/IR/Ident.re b/infer/src/IR/Ident.re index 186d979f0..41fdd5e48 100644 --- a/infer/src/IR/Ident.re +++ b/infer/src/IR/Ident.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -74,8 +73,9 @@ let compare i1 i2 => { } }; -let equal i1 i2 => i1.stamp === i2.stamp && i1.kind === i2.kind && name_equal i1.name i2.name -/* most unlikely first */; +let equal i1 i2 => + i1.stamp === i2.stamp && + i1.kind === i2.kind && name_equal i1.name i2.name /* most unlikely first */; let fieldname_equal fn1 fn2 => fieldname_compare fn1 fn2 == 0; @@ -208,8 +208,8 @@ let java_fieldname_is_outer_instance fn => { let this_len = String.length this; let zero_to_nine s => s >= "0" && s <= "9"; fn_len > this_len && - String.sub fn (fn_len - this_len - 1) this_len == this && - zero_to_nine (String.sub fn (fn_len - 1) 1) + String.sub fn (fn_len - this_len - 1) this_len == this && + zero_to_nine (String.sub fn (fn_len - 1) 1) }; let fieldname_offset fn => fn.fpos; @@ -224,6 +224,7 @@ let fieldname_is_hidden fn => fieldname_equal fn fieldname_hidden; /** {2 Functions and Hash Tables for Managing Stamps} */ + /** Set the stamp of the identifier */ let set_stamp i stamp => {...i, stamp}; @@ -331,6 +332,7 @@ let create_footprint name stamp => create_with_stamp kfootprint name stamp; /** {2 Functions for Identifiers} */ + /** Get a name of an identifier */ let get_name id => id.name; @@ -367,6 +369,7 @@ let create_path pathstring => /** {2 Pretty Printing} */ + /** Convert an identifier to a string. */ let to_string id => if (id.kind === knone) { diff --git a/infer/src/IR/Ident.rei b/infer/src/IR/Ident.rei index 10a281244..4e2ebfa70 100644 --- a/infer/src/IR/Ident.rei +++ b/infer/src/IR/Ident.rei @@ -10,11 +10,11 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; /** Identifiers: program variables and logical variables */ + /** Program and logical variables. */ type t; @@ -211,6 +211,7 @@ let set_stamp: t => int => t; /** {2 Comparision Functions} */ + /** Comparison for names. */ let name_compare: name => name => int; @@ -248,6 +249,7 @@ let ident_list_equal: list t => list t => bool; /** {2 Pretty Printing} */ + /** Pretty print a name. */ let pp_name: Format.formatter => name => unit; diff --git a/infer/src/IR/IntLit.re b/infer/src/IR/IntLit.re index 1a73aa8cd..a432567bc 100644 --- a/infer/src/IR/IntLit.re +++ b/infer/src/IR/IntLit.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; let module F = Format; diff --git a/infer/src/IR/IntLit.rei b/infer/src/IR/IntLit.rei index 342e6b2de..e878a6869 100644 --- a/infer/src/IR/IntLit.rei +++ b/infer/src/IR/IntLit.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; let module F = Format; diff --git a/infer/src/IR/Location.re b/infer/src/IR/Location.re index dee99aa6b..098218cf0 100644 --- a/infer/src/IR/Location.re +++ b/infer/src/IR/Location.re @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2015 - present Facebook, Inc. * All rights reserved. * @@ -9,7 +6,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; let module F = Format; diff --git a/infer/src/IR/Location.rei b/infer/src/IR/Location.rei index da2c18b25..fa2dcfbac 100644 --- a/infer/src/IR/Location.rei +++ b/infer/src/IR/Location.rei @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2015 - present Facebook, Inc. * All rights reserved. * @@ -9,7 +6,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/IR/Mangled.re b/infer/src/IR/Mangled.re index bbafc4e9a..1cd33c12b 100644 --- a/infer/src/IR/Mangled.re +++ b/infer/src/IR/Mangled.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/IR/Mangled.rei b/infer/src/IR/Mangled.rei index eb1d53062..b387d511c 100644 --- a/infer/src/IR/Mangled.rei +++ b/infer/src/IR/Mangled.rei @@ -10,11 +10,11 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; /** Module for Mangled Names */ + /** Type of mangled names */ type t; diff --git a/infer/src/IR/PredSymb.re b/infer/src/IR/PredSymb.re index dd341b1f2..c12076ede 100644 --- a/infer/src/IR/PredSymb.re +++ b/infer/src/IR/PredSymb.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -20,11 +19,15 @@ let module L = Logging; let module F = Format; type func_attribute = - | FA_sentinel of int int /** __attribute__((sentinel(int, int))) */; + | FA_sentinel int int /** __attribute__((sentinel(int, int))) */; /** Visibility modifiers. */ -type access = | Default | Public | Private | Protected; +type access = + | Default + | Public + | Private + | Protected; /** Return the value of the FA_sentinel attribute in [attr_list] if it is found */ @@ -51,7 +54,11 @@ let mem_kind_compare mk1 mk2 => int_compare (mem_kind_to_num mk1) (mem_kind_to_n /** resource that can be allocated */ -type resource = | Rmemory of mem_kind | Rfile | Rignore | Rlock; +type resource = + | Rmemory mem_kind + | Rfile + | Rignore + | Rlock; let resource_compare r1 r2 => { let res_to_num = @@ -65,7 +72,9 @@ let resource_compare r1 r2 => { /** kind of resource action */ -type res_act_kind = | Racquire | Rrelease; +type res_act_kind = + | Racquire + | Rrelease; let res_act_kind_compare rak1 rak2 => switch (rak1, rak2) { @@ -161,21 +170,21 @@ type res_action = { attribute to an expression, that expression should be the first argument, optionally followed by additional related expressions. */ type t = - | Aresource of res_action /** resource acquire/release */ + | Aresource res_action /** resource acquire/release */ | Aautorelease - | Adangling of dangling_kind /** dangling pointer */ + | Adangling dangling_kind /** dangling pointer */ /** undefined value obtained by calling the given procedure, plus its return value annots */ - | Aundef of Procname.t Annot.Item.t Location.t path_pos - | Ataint of taint_info - | Auntaint of taint_info + | Aundef Procname.t Annot.Item.t Location.t path_pos + | Ataint taint_info + | Auntaint taint_info | Alocked | Aunlocked /** value appeared in second argument of division at given path position */ - | Adiv0 of path_pos + | Adiv0 path_pos /** attributed exp is null due to a call to a method with given path as null receiver */ | Aobjc_null /** value was returned from a call to the given procedure, plus the annots of the return value */ - | Aretval of Procname.t Annot.Item.t + | Aretval Procname.t Annot.Item.t /** denotes an object registered as an observers to a notification center */ | Aobserver /** denotes an object unsubscribed from observers of a notification center */ @@ -324,12 +333,9 @@ let to_string pe => "" }; name ^ - Binop.str pe Lt ^ - Procname.to_string ra.ra_pname ^ - ":" ^ - string_of_int ra.ra_loc.Location.line ^ - Binop.str pe Gt ^ - str_vpath + Binop.str pe Lt ^ + Procname.to_string ra.ra_pname ^ + ":" ^ string_of_int ra.ra_loc.Location.line ^ Binop.str pe Gt ^ str_vpath } | Aautorelease => "AUTORELEASE" | Adangling dk => { @@ -343,11 +349,8 @@ let to_string pe => } | Aundef pn _ loc _ => "UND" ^ - Binop.str pe Lt ^ - Procname.to_string pn ^ - Binop.str pe Gt ^ - ":" ^ - string_of_int loc.Location.line + Binop.str pe Lt ^ + Procname.to_string pn ^ Binop.str pe Gt ^ ":" ^ string_of_int loc.Location.line | Ataint {taint_source} => "TAINTED[" ^ Procname.to_string taint_source ^ "]" | Auntaint _ => "UNTAINTED" | Alocked => "LOCKED" diff --git a/infer/src/IR/PredSymb.rei b/infer/src/IR/PredSymb.rei index 8f2732938..789a58af0 100644 --- a/infer/src/IR/PredSymb.rei +++ b/infer/src/IR/PredSymb.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -21,7 +20,8 @@ let module F = Format; /** {2 Programs and Types} */ -type func_attribute = | FA_sentinel of int int; +type func_attribute = + | FA_sentinel int int; /** Return the value of the FA_sentinel attribute in [attr_list] if it is found */ @@ -29,7 +29,11 @@ let get_sentinel_func_attribute_value: list func_attribute => option (int, int); /** Visibility modifiers. */ -type access = | Default | Public | Private | Protected; +type access = + | Default + | Public + | Private + | Protected; type mem_kind = | Mmalloc /** memory allocated with malloc */ @@ -41,13 +45,19 @@ let mem_kind_compare: mem_kind => mem_kind => int; /** resource that can be allocated */ -type resource = | Rmemory of mem_kind | Rfile | Rignore | Rlock; +type resource = + | Rmemory mem_kind + | Rfile + | Rignore + | Rlock; let resource_compare: resource => resource => int; /** kind of resource action */ -type res_act_kind = | Racquire | Rrelease; +type res_act_kind = + | Racquire + | Rrelease; let res_act_kind_compare: res_act_kind => res_act_kind => int; @@ -96,21 +106,21 @@ type res_action = { attribute to an expression, that expression should be the first argument, optionally followed by additional related expressions. */ type t = - | Aresource of res_action /** resource acquire/release */ + | Aresource res_action /** resource acquire/release */ | Aautorelease - | Adangling of dangling_kind /** dangling pointer */ + | Adangling dangling_kind /** dangling pointer */ /** undefined value obtained by calling the given procedure, plus its return value annots */ - | Aundef of Procname.t Annot.Item.t Location.t path_pos - | Ataint of taint_info - | Auntaint of taint_info + | Aundef Procname.t Annot.Item.t Location.t path_pos + | Ataint taint_info + | Auntaint taint_info | Alocked | Aunlocked /** value appeared in second argument of division at given path position */ - | Adiv0 of path_pos + | Adiv0 path_pos /** attributed exp is null due to a call to a method with given path as null receiver */ | Aobjc_null /** value was returned from a call to the given procedure, plus the annots of the return value */ - | Aretval of Procname.t Annot.Item.t + | Aretval Procname.t Annot.Item.t /** denotes an object registered as an observers to a notification center */ | Aobserver /** denotes an object unsubscribed from observers of a notification center */ diff --git a/infer/src/IR/ProcAttributes.re b/infer/src/IR/ProcAttributes.re index eaaf995f6..6f74a1101 100644 --- a/infer/src/IR/ProcAttributes.re +++ b/infer/src/IR/ProcAttributes.re @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2015 - present Facebook, Inc. * All rights reserved. * @@ -9,7 +6,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -20,7 +16,9 @@ let module F = Format; /** Type for ObjC accessors */ -type objc_accessor_type = | Objc_getter of Ident.fieldname | Objc_setter of Ident.fieldname; +type objc_accessor_type = + | Objc_getter Ident.fieldname + | Objc_setter Ident.fieldname; type t = { access: PredSymb.access, /** visibility access */ diff --git a/infer/src/IR/ProcAttributes.rei b/infer/src/IR/ProcAttributes.rei index 469f3cbc7..9ca71d253 100644 --- a/infer/src/IR/ProcAttributes.rei +++ b/infer/src/IR/ProcAttributes.rei @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2015 - present Facebook, Inc. * All rights reserved. * @@ -9,12 +6,13 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; /** Attributes of a procedure. */ -type objc_accessor_type = | Objc_getter of Ident.fieldname | Objc_setter of Ident.fieldname; +type objc_accessor_type = + | Objc_getter Ident.fieldname + | Objc_setter Ident.fieldname; type t = { access: PredSymb.access, /** visibility access */ diff --git a/infer/src/IR/Procname.re b/infer/src/IR/Procname.re index fe1dbcd2d..606175bed 100644 --- a/infer/src/IR/Procname.re +++ b/infer/src/IR/Procname.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -40,8 +39,8 @@ type java = { type c = (string, option string); type objc_cpp_method_kind = - | CPPMethod of (option string) /** with mangling */ - | CPPConstructor of (option string) /** with mangling */ + | CPPMethod (option string) /** with mangling */ + | CPPConstructor (option string) /** with mangling */ | ObjCInstanceMethod | ObjCInternalMethod | ObjCClassMethod; @@ -56,18 +55,22 @@ type block = string; /** Type of procedure names. */ -type t = | Java of java | C of c | ObjC_Cpp of objc_cpp | Block of block | Linters_dummy_method; +type t = + | Java java + | C c + | ObjC_Cpp objc_cpp + | Block block + | Linters_dummy_method; /** Level of verbosity of some to_string functions. */ -type detail_level = | Verbose | Non_verbose | Simple; +type detail_level = + | Verbose + | Non_verbose + | Simple; let objc_method_kind_of_bool is_instance => - if is_instance { - ObjCInstanceMethod - } else { - ObjCClassMethod - }; + if is_instance {ObjCInstanceMethod} else {ObjCClassMethod}; let empty_block = Block ""; @@ -150,10 +153,10 @@ let java_return_type_compare jr1 jr2 => /** Compare java procedure names. */ let java_compare (j1: java) (j2: java) => string_compare j1.method_name j2.method_name |> - next java_type_list_compare j1.parameters j2.parameters |> - next java_type_compare j1.class_name j2.class_name |> - next java_return_type_compare j1.return_type j2.return_type |> - next method_kind_compare j1.kind j2.kind; + next java_type_list_compare j1.parameters j2.parameters |> + next java_type_compare j1.class_name j2.class_name |> + next java_return_type_compare j1.return_type j2.return_type |> + next method_kind_compare j1.kind j2.kind; let objc_cpp_method_kind_compare k1 k2 => switch (k1, k2) { @@ -176,8 +179,8 @@ let objc_cpp_method_kind_compare k1 k2 => /** Compare c_method signatures. */ let c_meth_sig_compare osig1 osig2 => string_compare osig1.method_name osig2.method_name |> - next string_compare osig1.class_name osig2.class_name |> - next objc_cpp_method_kind_compare osig1.kind osig2.kind; + next string_compare osig1.class_name osig2.class_name |> + next objc_cpp_method_kind_compare osig1.kind osig2.kind; /** Given a package.class_name string, it looks for the latest dot and split the string @@ -513,22 +516,20 @@ let c_method_to_string osig detail_level => switch osig.kind { | CPPMethod m => "(" ^ - ( - switch m { - | None => "" - | Some s => s - } - ) ^ - ")" + ( + switch m { + | None => "" + | Some s => s + } + ) ^ ")" | CPPConstructor m => "{" ^ - ( - switch m { - | None => "" - | Some s => s - } - ) ^ - "}" + ( + switch m { + | None => "" + | Some s => s + } + ) ^ "}" | ObjCClassMethod => "class" | ObjCInstanceMethod => "instance" | ObjCInternalMethod => "internal" diff --git a/infer/src/IR/Procname.rei b/infer/src/IR/Procname.rei index faa119c71..39f3f26f6 100644 --- a/infer/src/IR/Procname.rei +++ b/infer/src/IR/Procname.rei @@ -10,11 +10,11 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; /** Module for Procedure Names. */ + /** Type of java procedure names. */ type java; @@ -32,7 +32,12 @@ type block; /** Type of procedure names. */ -type t = | Java of java | C of c | ObjC_Cpp of objc_cpp | Block of block | Linters_dummy_method; +type t = + | Java java + | C c + | ObjC_Cpp objc_cpp + | Block block + | Linters_dummy_method; type java_type = (option string, string); @@ -41,8 +46,8 @@ type method_kind = | Non_Static /* in Java, procedures called with invokevirtual, invokespecial, and invokeinterface */; type objc_cpp_method_kind = - | CPPMethod of (option string) /** with mangling */ - | CPPConstructor of (option string) /** with mangling */ + | CPPMethod (option string) /** with mangling */ + | CPPConstructor (option string) /** with mangling */ | ObjCInstanceMethod | ObjCInternalMethod | ObjCClassMethod; diff --git a/infer/src/IR/Pvar.re b/infer/src/IR/Pvar.re index 20c469cba..f2a50af04 100644 --- a/infer/src/IR/Pvar.re +++ b/infer/src/IR/Pvar.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -22,10 +21,10 @@ let module F = Format; /** Kind of global variables */ type pvar_kind = - | Local_var of Procname.t /** local variable belonging to a function */ - | Callee_var of Procname.t /** local variable belonging to a callee */ - | Abduced_retvar of Procname.t Location.t /** synthetic variable to represent return value */ - | Abduced_ref_param of Procname.t t Location.t + | Local_var Procname.t /** local variable belonging to a function */ + | Callee_var Procname.t /** local variable belonging to a callee */ + | Abduced_retvar Procname.t Location.t /** synthetic variable to represent return value */ + | Abduced_ref_param Procname.t t Location.t /** synthetic variable to represent param passed by reference */ | Global_var /** gloval variable */ | Seed_var /** variable used to store the initial value of formal parameters */ @@ -269,7 +268,7 @@ let is_frontend_tmp pvar => { /* Check whether the program variable is a temporary one generated by sawja */ let is_sawja_tmp name => string_is_prefix "$irvar" name || - string_is_prefix "$T" name || string_is_prefix "$bc" name || string_is_prefix "CatchVar" name; + string_is_prefix "$T" name || string_is_prefix "$bc" name || string_is_prefix "CatchVar" name; /* Check whether the program variable is generated by [mk_tmp] */ let is_sil_tmp name => string_is_prefix tmp_prefix name; let name = to_string pvar; diff --git a/infer/src/IR/Pvar.rei b/infer/src/IR/Pvar.rei index ce9655ebd..4534469c6 100644 --- a/infer/src/IR/Pvar.rei +++ b/infer/src/IR/Pvar.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index a7fe4a66d..077f7afc5 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -21,6 +20,7 @@ let module F = Format; /** {2 Programs and Types} */ + /** Kind of prune instruction */ type if_kind = | Ik_bexp /* boolean expressions, and exp ? exp : exp */ @@ -41,23 +41,23 @@ type instr = /* Note for frontend writers: [x] must be used in a subsequent instruction, otherwise the entire `Load` instruction may be eliminated by copy-propagation. */ - | Load of Ident.t Exp.t Typ.t Location.t + | Load Ident.t Exp.t Typ.t Location.t /** Store the value of an expression into the heap. [*lexp1:typ = exp2] where [lexp1] is an expression denoting a heap address [typ] is the root type of [lexp1] [exp2] is the expression whose value is store. */ - | Store of Exp.t Typ.t Exp.t Location.t + | Store Exp.t Typ.t Exp.t Location.t /** prune the state based on [exp=1], the boolean indicates whether true branch */ - | Prune of Exp.t Location.t bool if_kind + | Prune Exp.t Location.t bool if_kind /** [Call (ret_id, e_fun, arg_ts, loc, call_flags)] represents an instruction [ret_id = e_fun(arg_ts);]. The return value is ignored when [ret_id = None]. */ - | Call of (option (Ident.t, Typ.t)) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t + | Call (option (Ident.t, Typ.t)) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t /** nullify stack variable */ - | Nullify of Pvar.t Location.t - | Abstract of Location.t /** apply abstraction */ - | Remove_temps of (list Ident.t) Location.t /** remove temporaries */ - | Declare_locals of (list (Pvar.t, Typ.t)) Location.t /** declare local variables */; + | Nullify Pvar.t Location.t + | Abstract Location.t /** apply abstraction */ + | Remove_temps (list Ident.t) Location.t /** remove temporaries */ + | Declare_locals (list (Pvar.t, Typ.t)) Location.t /** declare local variables */; let skip_instr = Remove_temps [] Location.dummy; @@ -76,16 +76,19 @@ let instr_is_auxiliary = /** offset for an lvalue */ -type offset = | Off_fld of Ident.fieldname Typ.t | Off_index of Exp.t; +type offset = + | Off_fld Ident.fieldname Typ.t + | Off_index Exp.t; /** {2 Components of Propositions} */ + /** an atom is a pure atomic formula */ type atom = - | Aeq of Exp.t Exp.t /** equality */ - | Aneq of Exp.t Exp.t /** disequality */ - | Apred of PredSymb.t (list Exp.t) /** predicate symbol applied to exps */ - | Anpred of PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */; + | Aeq Exp.t Exp.t /** equality */ + | Aneq Exp.t Exp.t /** disequality */ + | Apred PredSymb.t (list Exp.t) /** predicate symbol applied to exps */ + | Anpred PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */; /** kind of lseg or dllseg predicates */ @@ -107,21 +110,21 @@ type inst = | Iabstraction | Iactual_precondition | Ialloc - | Iformal of zero_flag null_case_flag + | Iformal zero_flag null_case_flag | Iinitial | Ilookup | Inone | Inullify - | Irearrange of zero_flag null_case_flag int PredSymb.path_pos + | Irearrange zero_flag null_case_flag int PredSymb.path_pos | Itaint - | Iupdate of zero_flag null_case_flag int PredSymb.path_pos - | Ireturn_from_call of int; + | Iupdate zero_flag null_case_flag int PredSymb.path_pos + | Ireturn_from_call int; /** structured expressions represent a value of structured type, such as an array or a struct. */ type strexp = - | Eexp of Exp.t inst /** Base case: expression with instrumentation */ - | Estruct of (list (Ident.fieldname, strexp)) inst /** C structure */ + | Eexp Exp.t inst /** Base case: expression with instrumentation */ + | Estruct (list (Ident.fieldname, strexp)) inst /** C structure */ /** Array of given length There are two conditions imposed / used in the array case. First, if some index and value pair appears inside an array @@ -129,20 +132,20 @@ type strexp = For instance, x |->[10 | e1: v1] implies that e1 <= 9. Second, if two indices appear in an array, they should be different. For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. */ - | Earray of Exp.t (list (Exp.t, strexp)) inst; + | Earray Exp.t (list (Exp.t, strexp)) inst; /** an atomic heap predicate */ type hpred = - | Hpointsto of Exp.t strexp Exp.t + | Hpointsto Exp.t strexp Exp.t /** represents [exp|->strexp:typexp] where [typexp] is an expression representing a type, e.h. [sizeof(t)]. */ - | Hlseg of lseg_kind hpara Exp.t Exp.t (list Exp.t) + | Hlseg lseg_kind hpara Exp.t Exp.t (list Exp.t) /** higher - order predicate for singly - linked lists. Should ensure that exp1!= exp2 implies that exp1 is allocated. This assumption is used in the rearrangement. The last [exp list] parameter is used to denote the shared links by all the nodes in the list. */ - | Hdllseg of lseg_kind hpara_dll Exp.t Exp.t Exp.t Exp.t (list Exp.t) + | Hdllseg lseg_kind hpara_dll Exp.t Exp.t Exp.t Exp.t (list Exp.t) /** higher-order predicate for doubly-linked lists. */ /** parameter for the higher-order singly-linked list predicate. Means "lambda (root,next,svars). Exists evars. body". @@ -210,15 +213,14 @@ let mk_static_local_name pname vname => pname ^ "_" ^ vname; /** Check if a pvar is a local static in objc */ -let is_static_local_name pname pvar => +let is_static_local_name pname pvar => { /* local static name is of the form procname_varname */ - { - let var_name = Mangled.to_string (Pvar.get_name pvar); - switch (Str.split_delim (Str.regexp_string pname) var_name) { - | [_, _] => true - | _ => false - } - }; + let var_name = Mangled.to_string (Pvar.get_name pvar); + switch (Str.split_delim (Str.regexp_string pname) var_name) { + | [_, _] => true + | _ => false + } +}; let ident_exp_compare = pair_compare Ident.compare Exp.compare; @@ -467,6 +469,7 @@ let module HpredSet = Set.Make { /** {2 Pretty Printing} */ + /** Begin change color if using diff printing, return updated printenv and change status */ let color_pre_wrapper pe f x => if (Config.print_using_diff && pe.pe_kind !== PP_TEXT) { @@ -776,10 +779,12 @@ let rec pp_star_seq pp f => /********* START OF MODULE Predicates **********/ + /** Module Predicates records the occurrences of predicates as parameters of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator. */ let module Predicates: { + /** predicate environment */ type env; @@ -802,6 +807,7 @@ let module Predicates: { /** Process one hpred, updating the predicate environment */ let process_hpred: env => hpred => unit; } = { + /** hash tables for hpara */ let module HparaHash = Hashtbl.Make { type t = hpara; @@ -962,12 +968,7 @@ let inst_to_string inst => { fun | Some true => "(z)" | _ => ""; - let null_case_flag_to_string ncf => - if ncf { - "(ncf)" - } else { - "" - }; + let null_case_flag_to_string ncf => if ncf {"(ncf)"} else {""}; switch inst { | Iabstraction => "abstraction" | Iactual_precondition => "actual_precondition" @@ -1464,17 +1465,13 @@ let rec hpred_fpv = | Hpointsto base se te => exp_fpv base @ strexp_fpv se @ exp_fpv te | Hlseg _ para e1 e2 elist => { let fpvars_in_elist = exp_list_fpv elist; - hpara_fpv para @ /* This set has to be empty. */ exp_fpv e1 @ exp_fpv e2 @ fpvars_in_elist + hpara_fpv para @ /* This set has to be empty. */ exp_fpv e1 @ exp_fpv e2 @ fpvars_in_elist } | Hdllseg _ para e1 e2 e3 e4 elist => { let fpvars_in_elist = exp_list_fpv elist; hpara_dll_fpv para @ - /* This set has to be empty. */ - exp_fpv e1 @ - exp_fpv e2 @ - exp_fpv e3 @ - exp_fpv e4 @ - fpvars_in_elist + /* This set has to be empty. */ + exp_fpv e1 @ exp_fpv e2 @ exp_fpv e3 @ exp_fpv e4 @ fpvars_in_elist } /** hpara should not contain any program variables. This is because it might cause problems when we do interprocedural @@ -1501,6 +1498,7 @@ and hpara_dll_fpv para => { /** {2 Functions for computing free non-program variables} */ + /** Type of free variables. These include primed, normal and footprint variables. We keep a count of how many types the variables appear. */ type fav = ref (list Ident.t); @@ -1715,7 +1713,7 @@ let array_clean_new_index footprint_part new_idx => { if (footprint_part && fav_exists fav (fun id => not (Ident.is_footprint id))) { L.d_warning ( "Array index " ^ - exp_to_string new_idx ^ " has non-footprint vars: replaced by fresh footprint var" + exp_to_string new_idx ^ " has non-footprint vars: replaced by fresh footprint var" ); L.d_ln (); let id = Ident.create_fresh Ident.kfootprint; @@ -2688,6 +2686,7 @@ let hpred_compact sh hpred => /** {2 Functions for constructing or destructing entities in this module} */ + /** Compute the offset list of an expression */ let exp_get_offsets exp => { let rec f offlist_past e => diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index 640020fd5..13fb4ff16 100644 --- a/infer/src/IR/Sil.rei +++ b/infer/src/IR/Sil.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -19,6 +18,7 @@ let module F = Format; /** {2 Programs and Types} */ + /** Convert expression lists to expression sets. */ let elist_to_eset: list Exp.t => Exp.Set.t; @@ -43,23 +43,23 @@ type instr = /* Note for frontend writers: [x] must be used in a subsequent instruction, otherwise the entire `Load` instruction may be eliminated by copy-propagation. */ - | Load of Ident.t Exp.t Typ.t Location.t + | Load Ident.t Exp.t Typ.t Location.t /** Store the value of an expression into the heap. [*lexp1:typ = exp2] where [lexp1] is an expression denoting a heap address [typ] is the root type of [lexp1] [exp2] is the expression whose value is store. */ - | Store of Exp.t Typ.t Exp.t Location.t + | Store Exp.t Typ.t Exp.t Location.t /** prune the state based on [exp=1], the boolean indicates whether true branch */ - | Prune of Exp.t Location.t bool if_kind + | Prune Exp.t Location.t bool if_kind /** [Call (ret_id, e_fun, arg_ts, loc, call_flags)] represents an instruction [ret_id = e_fun(arg_ts);]. The return value is ignored when [ret_id = None]. */ - | Call of (option (Ident.t, Typ.t)) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t + | Call (option (Ident.t, Typ.t)) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t /** nullify stack variable */ - | Nullify of Pvar.t Location.t - | Abstract of Location.t /** apply abstraction */ - | Remove_temps of (list Ident.t) Location.t /** remove temporaries */ - | Declare_locals of (list (Pvar.t, Typ.t)) Location.t /** declare local variables */; + | Nullify Pvar.t Location.t + | Abstract Location.t /** apply abstraction */ + | Remove_temps (list Ident.t) Location.t /** remove temporaries */ + | Declare_locals (list (Pvar.t, Typ.t)) Location.t /** declare local variables */; let skip_instr: instr; @@ -69,16 +69,19 @@ let instr_is_auxiliary: instr => bool; /** Offset for an lvalue. */ -type offset = | Off_fld of Ident.fieldname Typ.t | Off_index of Exp.t; +type offset = + | Off_fld Ident.fieldname Typ.t + | Off_index Exp.t; /** {2 Components of Propositions} */ + /** an atom is a pure atomic formula */ type atom = - | Aeq of Exp.t Exp.t /** equality */ - | Aneq of Exp.t Exp.t /** disequality */ - | Apred of PredSymb.t (list Exp.t) /** predicate symbol applied to exps */ - | Anpred of PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */; + | Aeq Exp.t Exp.t /** equality */ + | Aneq Exp.t Exp.t /** disequality */ + | Apred PredSymb.t (list Exp.t) /** predicate symbol applied to exps */ + | Anpred PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */; /** kind of lseg or dllseg predicates */ @@ -100,15 +103,15 @@ type inst = | Iabstraction | Iactual_precondition | Ialloc - | Iformal of zero_flag null_case_flag + | Iformal zero_flag null_case_flag | Iinitial | Ilookup | Inone | Inullify - | Irearrange of zero_flag null_case_flag int PredSymb.path_pos + | Irearrange zero_flag null_case_flag int PredSymb.path_pos | Itaint - | Iupdate of zero_flag null_case_flag int PredSymb.path_pos - | Ireturn_from_call of int; + | Iupdate zero_flag null_case_flag int PredSymb.path_pos + | Ireturn_from_call int; let inst_abstraction: inst; @@ -161,8 +164,8 @@ let inst_partial_meet: inst => inst => inst; /** structured expressions represent a value of structured type, such as an array or a struct. */ type strexp = - | Eexp of Exp.t inst /** Base case: expression with instrumentation */ - | Estruct of (list (Ident.fieldname, strexp)) inst /** C structure */ + | Eexp Exp.t inst /** Base case: expression with instrumentation */ + | Estruct (list (Ident.fieldname, strexp)) inst /** C structure */ /** Array of given length There are two conditions imposed / used in the array case. First, if some index and value pair appears inside an array @@ -170,20 +173,20 @@ type strexp = For instance, x |->[10 | e1: v1] implies that e1 <= 9. Second, if two indices appear in an array, they should be different. For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. */ - | Earray of Exp.t (list (Exp.t, strexp)) inst; + | Earray Exp.t (list (Exp.t, strexp)) inst; /** an atomic heap predicate */ type hpred = - | Hpointsto of Exp.t strexp Exp.t + | Hpointsto Exp.t strexp Exp.t /** represents [exp|->strexp:typexp] where [typexp] is an expression representing a type, e.g. [sizeof(t)]. */ - | Hlseg of lseg_kind hpara Exp.t Exp.t (list Exp.t) + | Hlseg lseg_kind hpara Exp.t Exp.t (list Exp.t) /** higher - order predicate for singly - linked lists. Should ensure that exp1!= exp2 implies that exp1 is allocated. This assumption is used in the rearrangement. The last [exp list] parameter is used to denote the shared links by all the nodes in the list.*/ - | Hdllseg of lseg_kind hpara_dll Exp.t Exp.t Exp.t Exp.t (list Exp.t) + | Hdllseg lseg_kind hpara_dll Exp.t Exp.t Exp.t Exp.t (list Exp.t) /** higher-order predicate for doubly-linked lists. */ /** parameter for the higher-order singly-linked list predicate. Means "lambda (root,next,svars). Exists evars. body". @@ -304,6 +307,7 @@ let hpred_get_lhs: hpred => Exp.t; /** {2 Pretty Printing} */ + /** Begin change color if using diff printing, return updated printenv and change status */ let color_pre_wrapper: printenv => F.formatter => 'a => (printenv, bool); @@ -448,6 +452,7 @@ let pp_hpara_dll_list: printenv => F.formatter => list hpara_dll => unit; of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator. */ let module Predicates: { + /** predicate environment */ type env; @@ -477,6 +482,7 @@ let pp_hpred_env: printenv => option Predicates.env => F.formatter => hpred => u /** {2 Functions for traversing SIL data types} */ + /** This function should be used before adding a new index to Earray. The [exp] is the newly created index. This function "cleans" [exp] according to whether it is the @@ -486,11 +492,13 @@ let array_clean_new_index: bool => Exp.t => Exp.t; /** Change exps in strexp using [f]. */ + /** WARNING: the result might not be normalized. */ let strexp_expmap: ((Exp.t, option inst) => (Exp.t, option inst)) => strexp => strexp; /** Change exps in hpred by [f]. */ + /** WARNING: the result might not be normalized. */ let hpred_expmap: ((Exp.t, option inst) => (Exp.t, option inst)) => hpred => hpred; @@ -500,16 +508,19 @@ let hpred_instmap: (inst => inst) => hpred => hpred; /** Change exps in hpred list by [f]. */ + /** WARNING: the result might not be normalized. */ let hpred_list_expmap: ((Exp.t, option inst) => (Exp.t, option inst)) => list hpred => list hpred; /** Change exps in atom by [f]. */ + /** WARNING: the result might not be normalized. */ let atom_expmap: (Exp.t => Exp.t) => atom => atom; /** Change exps in atom list by [f]. */ + /** WARNING: the result might not be normalized. */ let atom_list_expmap: (Exp.t => Exp.t) => list atom => list atom; @@ -531,6 +542,7 @@ let hpara_fpv: hpara => list Pvar.t; /** {2 Functions for computing free non-program variables} */ + /** Type of free variables. These include primed, normal and footprint variables. We remember the order in which variables are added. */ type fav; @@ -628,6 +640,7 @@ let hpara_dll_shallow_av: hpara_dll => fav; /** {2 Functions for computing all free or bound non-program variables} */ + /** Non-program variables include all of primed, normal and footprint variables. Thus, the functions essentially compute all the identifiers occuring in a parameter. Some variables can appear more @@ -753,6 +766,7 @@ let sub_fpv: subst => list Pvar.t; /** substitution functions */ + /** WARNING: these functions do not ensure that the results are normalized. */ let exp_sub: subst => Exp.t => Exp.t; @@ -772,6 +786,7 @@ let instr_sub_ids: sub_id_binders::bool => (Ident.t => Exp.t) => instr => instr; /** {2 Functions for replacing occurrences of expressions.} */ + /** The first parameter should define a partial function. No parts of hpara are replaced by these functions. */ let exp_replace_exp: list (Exp.t, Exp.t) => Exp.t => Exp.t; @@ -784,6 +799,7 @@ let hpred_replace_exp: list (Exp.t, Exp.t) => hpred => hpred; /** {2 Functions for constructing or destructing entities in this module} */ + /** Compute the offset list of an expression */ let exp_get_offsets: Exp.t => list offset; diff --git a/infer/src/IR/StructTyp.re b/infer/src/IR/StructTyp.re index 528bce3ac..9a205208b 100644 --- a/infer/src/IR/StructTyp.re +++ b/infer/src/IR/StructTyp.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -123,7 +122,8 @@ let get_field_type_and_annotation lookup::lookup fn (typ: Typ.t) => switch (lookup name) { | Some {fields, statics} => try { - let (_, t, a) = IList.find (fun (f, _, _) => Ident.fieldname_equal f fn) (fields @ statics); + let (_, t, a) = + IList.find (fun (f, _, _) => Ident.fieldname_equal f fn) (fields @ statics); Some (t, a) } { | Not_found => None diff --git a/infer/src/IR/StructTyp.rei b/infer/src/IR/StructTyp.rei index 996e2be70..ef5878664 100644 --- a/infer/src/IR/StructTyp.rei +++ b/infer/src/IR/StructTyp.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/IR/Subtype.re b/infer/src/IR/Subtype.re index 66f4837b5..d08a8bca3 100644 --- a/infer/src/IR/Subtype.re +++ b/infer/src/IR/Subtype.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -40,11 +39,14 @@ let list_to_string list => { type t' = | Exact /** denotes the current type only */ - | Subtypes of (list Typename.t); + | Subtypes (list Typename.t); /** denotes the current type and a list of types that are not their subtypes */ -type kind = | CAST | INSTOF | NORMAL; +type kind = + | CAST + | INSTOF + | NORMAL; type t = (t', kind); diff --git a/infer/src/IR/Subtype.rei b/infer/src/IR/Subtype.rei index b3a6e2a9f..1c1c8adf3 100644 --- a/infer/src/IR/Subtype.rei +++ b/infer/src/IR/Subtype.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/IR/Tenv.re b/infer/src/IR/Tenv.re index f30f2deff..b3dd20a9e 100644 --- a/infer/src/IR/Tenv.re +++ b/infer/src/IR/Tenv.re @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2016 - present Facebook, Inc. * All rights reserved. * @@ -9,11 +6,11 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; /** Module for Type Environments. */ + /** Hash tables on strings. */ let module TypenameHash = Hashtbl.Make { type t = Typename.t; diff --git a/infer/src/IR/Tenv.rei b/infer/src/IR/Tenv.rei index fe8b9e077..a3eceb29c 100644 --- a/infer/src/IR/Tenv.rei +++ b/infer/src/IR/Tenv.rei @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2016 - present Facebook, Inc. * All rights reserved. * @@ -9,7 +6,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/IR/Typ.re b/infer/src/IR/Typ.re index 6710bb0e6..3dd65da34 100644 --- a/infer/src/IR/Typ.re +++ b/infer/src/IR/Typ.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -185,13 +184,13 @@ type static_length = option IntLit.t; /** types for sil (structured) expressions */ type t = - | Tint of ikind /** integer type */ - | Tfloat of fkind /** float type */ + | Tint ikind /** integer type */ + | Tfloat fkind /** float type */ | Tvoid /** void type */ - | Tfun of bool /** function type with noreturn attribute */ - | Tptr of t ptr_kind /** pointer type */ - | Tstruct of Typename.t /** structured value type name */ - | Tarray of t static_length /** array type with statically fixed length */; + | Tfun bool /** function type with noreturn attribute */ + | Tptr t ptr_kind /** pointer type */ + | Tstruct Typename.t /** structured value type name */ + | Tarray t static_length /** array type with statically fixed length */; /** Comparision for types. */ diff --git a/infer/src/IR/Typ.rei b/infer/src/IR/Typ.rei index 8d55ea223..aea9475d8 100644 --- a/infer/src/IR/Typ.rei +++ b/infer/src/IR/Typ.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -75,13 +74,13 @@ type static_length = option IntLit.t; /** types for sil (structured) expressions */ type t = - | Tint of ikind /** integer type */ - | Tfloat of fkind /** float type */ + | Tint ikind /** integer type */ + | Tfloat fkind /** float type */ | Tvoid /** void type */ - | Tfun of bool /** function type with noreturn attribute */ - | Tptr of t ptr_kind /** pointer type */ - | Tstruct of Typename.t /** structured value type name */ - | Tarray of t static_length /** array type with statically fixed length */; + | Tfun bool /** function type with noreturn attribute */ + | Tptr t ptr_kind /** pointer type */ + | Tstruct Typename.t /** structured value type name */ + | Tarray t static_length /** array type with statically fixed length */; /** Comparision for types. */ diff --git a/infer/src/IR/Typename.re b/infer/src/IR/Typename.re index 4b00c1ebf..cf47386ff 100644 --- a/infer/src/IR/Typename.re +++ b/infer/src/IR/Typename.re @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2015 - present Facebook, Inc. * All rights reserved. * @@ -9,14 +6,14 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; let module F = Format; /** Named types. */ -type t = | TN_csu of Csu.t Mangled.t; +type t = + | TN_csu Csu.t Mangled.t; let to_string = fun diff --git a/infer/src/IR/Typename.rei b/infer/src/IR/Typename.rei index 0962f5683..42c367ded 100644 --- a/infer/src/IR/Typename.rei +++ b/infer/src/IR/Typename.rei @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2015 - present Facebook, Inc. * All rights reserved. * @@ -9,12 +6,12 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; /** Named types. */ -type t = | TN_csu of Csu.t Mangled.t; +type t = + | TN_csu Csu.t Mangled.t; /** convert the typename to a string */ @@ -35,6 +32,7 @@ let compare: t => t => int; let equal: t => t => bool; let module Java: { + /** Create a typename from a Java classname in the form "package.class" */ let from_string: string => t; diff --git a/infer/src/IR/Unop.re b/infer/src/IR/Unop.re index 65855b81e..4890810fd 100644 --- a/infer/src/IR/Unop.re +++ b/infer/src/IR/Unop.re @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/IR/Unop.rei b/infer/src/IR/Unop.rei index 2f45bb1dd..a0620bf02 100644 --- a/infer/src/IR/Unop.rei +++ b/infer/src/IR/Unop.rei @@ -10,7 +10,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/backend/InferAnalyze.re b/infer/src/backend/InferAnalyze.re index 22b04daf9..298e92241 100644 --- a/infer/src/backend/InferAnalyze.re +++ b/infer/src/backend/InferAnalyze.re @@ -7,7 +7,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/backend/InferAnalyze.rei b/infer/src/backend/InferAnalyze.rei index be851399e..54ce5e966 100644 --- a/infer/src/backend/InferAnalyze.rei +++ b/infer/src/backend/InferAnalyze.rei @@ -7,7 +7,5 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; - /** Main module for the analysis after the capture phase */ diff --git a/infer/src/backend/InferPrint.re b/infer/src/backend/InferPrint.re index 90a1a677b..013823a7b 100644 --- a/infer/src/backend/InferPrint.re +++ b/infer/src/backend/InferPrint.re @@ -7,7 +7,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; let module L = Logging; @@ -209,12 +208,7 @@ let summary_values top_proc_set summary => { vfile: DB.source_file_to_string attributes.ProcAttributes.loc.Location.file, vline: attributes.ProcAttributes.loc.Location.line, vloc: attributes.ProcAttributes.loc.Location.nLOC, - vtop: - if is_top { - "Y" - } else { - "N" - }, + vtop: if is_top {"Y"} else {"N"}, vsignature: signature, vweight: nodes_nr, vproof_coverage: Printf.sprintf "%2.2f" node_coverage, @@ -226,6 +220,7 @@ let summary_values top_proc_set summary => { }; let module ProcsCsv = { + /** Print the header of the procedures csv file, with column names */ let pp_header fmt () => Format.fprintf @@ -491,6 +486,7 @@ let module IssuesJson = { }; let module IssuesTests = { + /** Write bug report in a format suitable for tests on analysis results. */ let pp_issues_of_error_log fmt error_filter _ proc_loc_opt proc_name err_log => { let pp_row _ loc _ ekind in_footprint error_name error_desc _ _ _ _ => { @@ -503,22 +499,22 @@ let module IssuesTests = { }; let should_report = ekind == Exceptions.Kerror || - IList.exists - (Localise.equal error_name) - [ - Localise.assign_pointer_warning, - Localise.bad_pointer_comparison, - Localise.component_factory_function, - Localise.cxx_reference_captured_in_objc_block, - Localise.direct_atomic_property_access, - Localise.field_not_null_checked, - Localise.global_variable_initialized_with_function_or_method_call, - Localise.mutable_local_variable_in_component_file, - Localise.parameter_not_null_checked, - Localise.registered_observer_being_deallocated, - Localise.return_value_ignored, - Localise.strong_delegate_warning - ]; + IList.exists + (Localise.equal error_name) + [ + Localise.assign_pointer_warning, + Localise.bad_pointer_comparison, + Localise.component_factory_function, + Localise.cxx_reference_captured_in_objc_block, + Localise.direct_atomic_property_access, + Localise.field_not_null_checked, + Localise.global_variable_initialized_with_function_or_method_call, + Localise.mutable_local_variable_in_component_file, + Localise.parameter_not_null_checked, + Localise.registered_observer_being_deallocated, + Localise.return_value_ignored, + Localise.strong_delegate_warning + ]; if (in_footprint && should_report && error_filter source_file error_desc error_name) { F.fprintf fmt @@ -536,6 +532,7 @@ let module IssuesTests = { }; let module IssuesTxt = { + /** Write bug report in text format */ let pp_issues_of_error_log fmt error_filter _ proc_loc_opt _ err_log => { let pp_row (node_id, node_key) loc _ ekind in_footprint error_name error_desc _ _ _ _ => { @@ -644,6 +641,7 @@ let module IssuesXml = { }; let module CallsCsv = { + /** Print the header of the calls csv file, with column names */ let pp_header fmt () => Format.fprintf @@ -667,7 +665,8 @@ let module CallsCsv = { pp "\"%s\"," (Escape.escape_csv (Procname.to_filename caller_name)); pp "\"%s\"," (Escape.escape_csv (Procname.to_string callee_name)); pp "\"%s\"," (Escape.escape_csv (Procname.to_filename callee_name)); - pp "%s," (DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file); + pp + "%s," (DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file); pp "%d," loc.Location.line; pp "%a@\n" Specs.CallStats.pp_trace trace }; @@ -801,7 +800,8 @@ let module Stats = { let process_summary error_filter summary linereader stats => { let specs = Specs.get_specs_from_payload summary; let found_errors = - process_err_log error_filter linereader summary.Specs.attributes.ProcAttributes.err_log stats; + process_err_log + error_filter linereader summary.Specs.attributes.ProcAttributes.err_log stats; let is_defective = found_errors; let is_verified = specs != [] && not is_defective; let is_checked = not (is_defective || is_verified); @@ -884,7 +884,7 @@ let module Summary = { let specs = Specs.get_specs_from_payload summary; if ( not (DB.file_exists xml_file) || - DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time xml_file + DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time xml_file ) { let xml_out = create_outfile (DB.filename_to_string xml_file); do_outf @@ -909,18 +909,18 @@ let module Summary = { let svg_file = DB.filename_add_suffix base ".svg"; if ( not (DB.file_exists dot_file) || - DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time dot_file + DB.file_modified_time (DB.filename_from_string fname) > DB.file_modified_time dot_file ) { Dotty.pp_speclist_dotty_file base specs }; if ( not (DB.file_exists svg_file) || - DB.file_modified_time dot_file > DB.file_modified_time svg_file + DB.file_modified_time dot_file > DB.file_modified_time svg_file ) { ignore ( Sys.command ( "dot -Tsvg \"" ^ - DB.filename_to_string dot_file ^ "\" >\"" ^ DB.filename_to_string svg_file ^ "\"" + DB.filename_to_string dot_file ^ "\" >\"" ^ DB.filename_to_string svg_file ^ "\"" ) ) } @@ -962,16 +962,27 @@ let module PreconditionStats = { }; let error_filter filters proc_name file error_desc error_name => { - let always_report () => Localise.error_desc_extract_tag_value error_desc "always_report" == "true"; + let always_report () => + Localise.error_desc_extract_tag_value error_desc "always_report" == "true"; (Config.write_html || not (Localise.equal error_name Localise.skip_function)) && - (filters.Inferconfig.path_filter file || always_report ()) && - filters.Inferconfig.error_filter error_name && - filters.Inferconfig.proc_filter proc_name + (filters.Inferconfig.path_filter file || always_report ()) && + filters.Inferconfig.error_filter error_name && filters.Inferconfig.proc_filter proc_name }; -type report_kind = | Issues | Procs | Stats | Calls | Summary; +type report_kind = + | Issues + | Procs + | Stats + | Calls + | Summary; -type bug_format_kind = | Json | Csv | Tests | Text | Xml | Latex; +type bug_format_kind = + | Json + | Csv + | Tests + | Text + | Xml + | Latex; type bug_format = (bug_format_kind, outfile); @@ -1129,38 +1140,37 @@ let process_summary filters formats_by_report_kind linereader stats top_proc_set let module AnalysisResults = { type t = list (string, Specs.summary); - let spec_files_from_cmdline = + let spec_files_from_cmdline = { /* find spec files specified by command-line arguments */ - { - IList.iter - ( - fun arg => - if (not (Filename.check_suffix arg Config.specs_files_suffix) && arg != ".") { - print_usage_exit ("file " ^ arg ^ ": arguments must be .specs files") - } - ) - Config.anon_args; - switch Config.source_file_copy { - | Some s => source_file_copy := Some (DB.abs_source_file_from_path s) - | None => () - }; - if Config.test_filtering { - Inferconfig.test (); - exit 0 - }; - IList.append - ( - if (Config.anon_args == ["."]) { - let arr = Sys.readdir "."; - let all_files = Array.to_list arr; - IList.filter - (fun fname => Filename.check_suffix fname Config.specs_files_suffix) all_files - } else { - Config.anon_args + IList.iter + ( + fun arg => + if (not (Filename.check_suffix arg Config.specs_files_suffix) && arg != ".") { + print_usage_exit ("file " ^ arg ^ ": arguments must be .specs files") } - ) - (load_specfiles ()) + ) + Config.anon_args; + switch Config.source_file_copy { + | Some s => source_file_copy := Some (DB.abs_source_file_from_path s) + | None => () + }; + if Config.test_filtering { + Inferconfig.test (); + exit 0 }; + IList.append + ( + if (Config.anon_args == ["."]) { + let arr = Sys.readdir "."; + let all_files = Array.to_list arr; + IList.filter + (fun fname => Filename.check_suffix fname Config.specs_files_suffix) all_files + } else { + Config.anon_args + } + ) + (load_specfiles ()) + }; /** apply [f] to [arg] with the gc compaction disabled during the execution */ let apply_without_gc f arg => { diff --git a/infer/src/backend/PropUtil.re b/infer/src/backend/PropUtil.re index fc523f189..2c400728b 100644 --- a/infer/src/backend/PropUtil.re +++ b/infer/src/backend/PropUtil.re @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2016 - present Facebook, Inc. * All rights reserved. * @@ -9,7 +6,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; let get_name_of_local (curr_f: Cfg.Procdesc.t) (x, _) => @@ -49,104 +45,103 @@ let get_name_of_objc_block_locals p => { IList.flatten (IList.flatten vars_sigma) }; -let remove_abduced_retvars tenv p => +let remove_abduced_retvars tenv p => { /* compute the hpreds and pure atoms reachable from the set of seed expressions in [exps] */ - { - let compute_reachable p seed_exps => { - let (sigma, pi) = (p.Prop.sigma, p.Prop.pi); - let rec collect_exps exps => + let compute_reachable p seed_exps => { + let (sigma, pi) = (p.Prop.sigma, p.Prop.pi); + let rec collect_exps exps => + fun + | Sil.Eexp (Exp.Exn e) _ => Exp.Set.add e exps + | Sil.Eexp e _ => Exp.Set.add e exps + | Sil.Estruct flds _ => + IList.fold_left (fun exps (_, strexp) => collect_exps exps strexp) exps flds + | Sil.Earray _ elems _ => + IList.fold_left (fun exps (_, strexp) => collect_exps exps strexp) exps elems; + let rec compute_reachable_hpreds_rec sigma (reach, exps) => { + let add_hpred_if_reachable (reach, exps) => fun - | Sil.Eexp (Exp.Exn e) _ => Exp.Set.add e exps - | Sil.Eexp e _ => Exp.Set.add e exps - | Sil.Estruct flds _ => - IList.fold_left (fun exps (_, strexp) => collect_exps exps strexp) exps flds - | Sil.Earray _ elems _ => - IList.fold_left (fun exps (_, strexp) => collect_exps exps strexp) exps elems; - let rec compute_reachable_hpreds_rec sigma (reach, exps) => { - let add_hpred_if_reachable (reach, exps) => - fun - | Sil.Hpointsto lhs rhs _ as hpred when Exp.Set.mem lhs exps => { - let reach' = Sil.HpredSet.add hpred reach; - let exps' = collect_exps exps rhs; - (reach', exps') - } - | Sil.Hlseg _ _ exp1 exp2 exp_l as hpred => { - let reach' = Sil.HpredSet.add hpred reach; - let exps' = - IList.fold_left - (fun exps_acc exp => Exp.Set.add exp exps_acc) exps [exp1, exp2, ...exp_l]; - (reach', exps') - } - | Sil.Hdllseg _ _ exp1 exp2 exp3 exp4 exp_l as hpred => { - let reach' = Sil.HpredSet.add hpred reach; - let exps' = - IList.fold_left - (fun exps_acc exp => Exp.Set.add exp exps_acc) - exps - [exp1, exp2, exp3, exp4, ...exp_l]; - (reach', exps') - } - | _ => (reach, exps); - let (reach', exps') = IList.fold_left add_hpred_if_reachable (reach, exps) sigma; - if (Sil.HpredSet.cardinal reach == Sil.HpredSet.cardinal reach') { - (reach, exps) - } else { - compute_reachable_hpreds_rec sigma (reach', exps') - } - }; - let (reach_hpreds, reach_exps) = - compute_reachable_hpreds_rec sigma (Sil.HpredSet.empty, seed_exps); - /* filter away the pure atoms without reachable exps */ - let reach_pi = { - let rec exp_contains = - fun - | exp when Exp.Set.mem exp reach_exps => true - | Exp.UnOp _ e _ - | Exp.Cast _ e - | Exp.Lfield e _ _ => exp_contains e - | Exp.BinOp _ e0 e1 - | Exp.Lindex e0 e1 => exp_contains e0 || exp_contains e1 - | _ => false; - IList.filter - ( - fun - | Sil.Aeq lhs rhs - | Sil.Aneq lhs rhs => exp_contains lhs || exp_contains rhs - | Sil.Apred _ es - | Sil.Anpred _ es => IList.exists exp_contains es - ) - pi - }; - (Sil.HpredSet.elements reach_hpreds, reach_pi) + | Sil.Hpointsto lhs rhs _ as hpred when Exp.Set.mem lhs exps => { + let reach' = Sil.HpredSet.add hpred reach; + let exps' = collect_exps exps rhs; + (reach', exps') + } + | Sil.Hlseg _ _ exp1 exp2 exp_l as hpred => { + let reach' = Sil.HpredSet.add hpred reach; + let exps' = + IList.fold_left + (fun exps_acc exp => Exp.Set.add exp exps_acc) exps [exp1, exp2, ...exp_l]; + (reach', exps') + } + | Sil.Hdllseg _ _ exp1 exp2 exp3 exp4 exp_l as hpred => { + let reach' = Sil.HpredSet.add hpred reach; + let exps' = + IList.fold_left + (fun exps_acc exp => Exp.Set.add exp exps_acc) + exps + [exp1, exp2, exp3, exp4, ...exp_l]; + (reach', exps') + } + | _ => (reach, exps); + let (reach', exps') = IList.fold_left add_hpred_if_reachable (reach, exps) sigma; + if (Sil.HpredSet.cardinal reach == Sil.HpredSet.cardinal reach') { + (reach, exps) + } else { + compute_reachable_hpreds_rec sigma (reach', exps') + } }; - /* separate the abduced pvars from the normal ones, deallocate the abduced ones*/ - let (abduceds, normal_pvars) = - IList.fold_left + let (reach_hpreds, reach_exps) = + compute_reachable_hpreds_rec sigma (Sil.HpredSet.empty, seed_exps); + /* filter away the pure atoms without reachable exps */ + let reach_pi = { + let rec exp_contains = + fun + | exp when Exp.Set.mem exp reach_exps => true + | Exp.UnOp _ e _ + | Exp.Cast _ e + | Exp.Lfield e _ _ => exp_contains e + | Exp.BinOp _ e0 e1 + | Exp.Lindex e0 e1 => exp_contains e0 || exp_contains e1 + | _ => false; + IList.filter ( - fun pvars hpred => - switch hpred { - | Sil.Hpointsto (Exp.Lvar pvar) _ _ => - let (abduceds, normal_pvars) = pvars; - if (Pvar.is_abduced pvar) { - ([pvar, ...abduceds], normal_pvars) - } else { - (abduceds, [pvar, ...normal_pvars]) - } - | _ => pvars - } + fun + | Sil.Aeq lhs rhs + | Sil.Aneq lhs rhs => exp_contains lhs || exp_contains rhs + | Sil.Apred _ es + | Sil.Anpred _ es => IList.exists exp_contains es ) - ([], []) - p.Prop.sigma; - let (_, p') = Attribute.deallocate_stack_vars tenv p abduceds; - let normal_pvar_set = - IList.fold_left - (fun normal_pvar_set pvar => Exp.Set.add (Exp.Lvar pvar) normal_pvar_set) - Exp.Set.empty - normal_pvars; - /* walk forward from non-abduced pvars, keep everything reachable. remove everything else */ - let (sigma_reach, pi_reach) = compute_reachable p' normal_pvar_set; - Prop.normalize tenv (Prop.set p' pi::pi_reach sigma::sigma_reach) + pi + }; + (Sil.HpredSet.elements reach_hpreds, reach_pi) }; + /* separate the abduced pvars from the normal ones, deallocate the abduced ones*/ + let (abduceds, normal_pvars) = + IList.fold_left + ( + fun pvars hpred => + switch hpred { + | Sil.Hpointsto (Exp.Lvar pvar) _ _ => + let (abduceds, normal_pvars) = pvars; + if (Pvar.is_abduced pvar) { + ([pvar, ...abduceds], normal_pvars) + } else { + (abduceds, [pvar, ...normal_pvars]) + } + | _ => pvars + } + ) + ([], []) + p.Prop.sigma; + let (_, p') = Attribute.deallocate_stack_vars tenv p abduceds; + let normal_pvar_set = + IList.fold_left + (fun normal_pvar_set pvar => Exp.Set.add (Exp.Lvar pvar) normal_pvar_set) + Exp.Set.empty + normal_pvars; + /* walk forward from non-abduced pvars, keep everything reachable. remove everything else */ + let (sigma_reach, pi_reach) = compute_reachable p' normal_pvar_set; + Prop.normalize tenv (Prop.set p' pi::pi_reach sigma::sigma_reach) +}; let remove_locals tenv (curr_f: Cfg.Procdesc.t) p => { let names_of_locals = IList.map (get_name_of_local curr_f) (Cfg.Procdesc.get_locals curr_f); diff --git a/infer/src/backend/PropUtil.rei b/infer/src/backend/PropUtil.rei index 24aeeb9b9..305538b93 100644 --- a/infer/src/backend/PropUtil.rei +++ b/infer/src/backend/PropUtil.rei @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2016 - present Facebook, Inc. * All rights reserved. * @@ -9,7 +6,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/base/StatisticsToolbox.re b/infer/src/base/StatisticsToolbox.re index 404b705fa..68d78774b 100644 --- a/infer/src/base/StatisticsToolbox.re +++ b/infer/src/base/StatisticsToolbox.re @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2016 - present Facebook, Inc. * All rights reserved. * @@ -9,7 +6,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; type t = { @@ -36,7 +32,7 @@ let to_json s => ]; let from_json json => { - let open! Yojson.Basic.Util; + open! Yojson.Basic.Util; { sum: json |> member "sum" |> to_float, avg: json |> member "avg" |> to_float, diff --git a/infer/src/base/StatisticsToolbox.rei b/infer/src/base/StatisticsToolbox.rei index e2812b95c..ffb089d63 100644 --- a/infer/src/base/StatisticsToolbox.rei +++ b/infer/src/base/StatisticsToolbox.rei @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2016 - present Facebook, Inc. * All rights reserved. * @@ -9,7 +6,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; type t; diff --git a/infer/src/clang/Capture.re b/infer/src/clang/Capture.re index b9724cc1e..23231a386 100644 --- a/infer/src/clang/Capture.re +++ b/infer/src/clang/Capture.re @@ -6,7 +6,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; @@ -29,7 +28,8 @@ let catch_biniou_buffer_errors f x => /* This function reads the json file in fname, validates it, and encoded in the AST data structure defined in Clang_ast_t. */ let validate_decl_from_file fname => - catch_biniou_buffer_errors (Ag_util.Biniou.from_file len::buffer_len Clang_ast_b.read_decl) fname; + catch_biniou_buffer_errors + (Ag_util.Biniou.from_file len::buffer_len Clang_ast_b.read_decl) fname; let validate_decl_from_channel chan => catch_biniou_buffer_errors @@ -45,7 +45,9 @@ let register_perf_stats_report source_file => { }; let init_global_state_for_capture_and_linters source_file => { - Logging.set_log_file_identifier (Some (Filename.basename (DB.source_file_to_string source_file))); + Logging.set_log_file_identifier ( + Some (Filename.basename (DB.source_file_to_string source_file)) + ); register_perf_stats_report source_file; Config.curr_language := Config.Clang; DB.Results_dir.init source_file; @@ -114,8 +116,7 @@ let run_plugin_and_frontend frontend clang_args => { try [Unix.getenv "INFER_ARGS"] { | Not_found => [] } - ) - @ [ + ) @ [ "--clang-biniou-file", biniou_fname ] @@ -152,7 +153,12 @@ let capture clang_args => { init_global_state_for_capture_and_linters source_file; let trans_unit_ctx = { let clang_langs = - CFrontend_config.[("c", C), ("objective-c", ObjC), ("c++", CPP), ("objective-c++", ObjCPP)]; + CFrontend_config.[ + ("c", C), + ("objective-c", ObjC), + ("c++", CPP), + ("objective-c++", ObjCPP) + ]; let lang = switch (ClangCommand.value_of_option clang_args "-x") { | Some lang_opt when IList.mem_assoc string_equal lang_opt clang_langs => diff --git a/infer/src/clang/Capture.rei b/infer/src/clang/Capture.rei index 1a6565667..2e1c165f2 100644 --- a/infer/src/clang/Capture.rei +++ b/infer/src/clang/Capture.rei @@ -6,5 +6,4 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - let capture: ClangCommand.args => unit; diff --git a/infer/src/clang/ClangCommand.re b/infer/src/clang/ClangCommand.re index 268472364..614d140e8 100644 --- a/infer/src/clang/ClangCommand.re +++ b/infer/src/clang/ClangCommand.re @@ -6,25 +6,24 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; -type quoting_style = | DoubleQuotes | SingleQuotes; +type quoting_style = + | DoubleQuotes + | SingleQuotes; type args = {exec: string, argv: list string, quoting_style: quoting_style}; -type t = | Assembly of args | CC1 of args | ClangError of string | NonCCCommand of args; +type t = + | Assembly args + | CC1 args + | ClangError string + | NonCCCommand args; /** path of the plugin to load in clang */ let plugin_path = - Config.bin_dir /\/ - Filename.parent_dir_name /\/ - Filename.parent_dir_name /\/ - "facebook-clang-plugins" /\/ - "libtooling" /\/ - "build" /\/ - "FacebookClangPlugin.dylib"; + Config.bin_dir /\/ Filename.parent_dir_name /\/ Filename.parent_dir_name /\/ "facebook-clang-plugins" /\/ "libtooling" /\/ "build" /\/ "FacebookClangPlugin.dylib"; let test_env_var var => switch (Sys.getenv var) { @@ -73,18 +72,17 @@ let has_flag {argv} flag => IList.exists (string_equal flag) argv; let mk quoting_style argv => { let argv_list = Array.to_list argv; - let is_assembly = + let is_assembly = { /* whether language is set to "assembler" or "assembler-with-cpp" */ - { - let assembly_language = - switch (value_of_argv_option argv_list "-x") { - | Some lang => string_is_prefix "assembler" lang - | _ => false - }; - /* Detect -cc1as or assembly language commands. -cc1as is always the first argument if - present. */ - string_equal argv.(1) "-cc1as" || assembly_language - }; + let assembly_language = + switch (value_of_argv_option argv_list "-x") { + | Some lang => string_is_prefix "assembler" lang + | _ => false + }; + /* Detect -cc1as or assembly language commands. -cc1as is always the first argument if + present. */ + string_equal argv.(1) "-cc1as" || assembly_language + }; let args = {exec: argv.(0), argv: IList.tl argv_list, quoting_style}; if is_assembly { Assembly args @@ -118,28 +116,24 @@ let with_plugin_args args => { }; let rev_args_before = [] |> - /* -cc1 has to be the first argument or clang will think it runs in driver mode */ - cons "-cc1" |> - /* It's important to place this option before other -isystem options. */ - do_if infer_cxx_models (IList.rev_append ["-isystem", Config.cpp_models_dir]) |> - IList.rev_append [ - "-load", - plugin_path, - /* (t7400979) this is a workaround to avoid that clang crashes when the -fmodules flag and the - YojsonASTExporter plugin are used. Since the -plugin argument disables the generation of .o - files, we invoke apple clang again to generate the expected artifacts. This will keep - xcodebuild plus all the sub-steps happy. */ - if apple_clang { - "-plugin" - } else { - "-add-plugin" - }, - plugin_name, - "-plugin-arg-" ^ plugin_name, - "-", - "-plugin-arg-" ^ plugin_name, - "PREPEND_CURRENT_DIR=1" - ]; + /* -cc1 has to be the first argument or clang will think it runs in driver mode */ + cons "-cc1" |> + /* It's important to place this option before other -isystem options. */ + do_if infer_cxx_models (IList.rev_append ["-isystem", Config.cpp_models_dir]) |> + IList.rev_append [ + "-load", + plugin_path, + /* (t7400979) this is a workaround to avoid that clang crashes when the -fmodules flag and the + YojsonASTExporter plugin are used. Since the -plugin argument disables the generation of .o + files, we invoke apple clang again to generate the expected artifacts. This will keep + xcodebuild plus all the sub-steps happy. */ + if apple_clang {"-plugin"} else {"-add-plugin"}, + plugin_name, + "-plugin-arg-" ^ plugin_name, + "-", + "-plugin-arg-" ^ plugin_name, + "PREPEND_CURRENT_DIR=1" + ]; let args_after = [] |> do_if syntax_only (cons "-fsyntax-only"); {...args, argv: IList.rev_append rev_args_before (args.argv @ args_after)} }; diff --git a/infer/src/clang/ClangCommand.rei b/infer/src/clang/ClangCommand.rei index 3915cbc4d..050c605e0 100644 --- a/infer/src/clang/ClangCommand.rei +++ b/infer/src/clang/ClangCommand.rei @@ -6,16 +6,15 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - type args; type t = - | Assembly of args + | Assembly args /** a normalized clang command that runs the assembler */ - | CC1 of args + | CC1 args /** a -cc1 clang command */ - | ClangError of string - | NonCCCommand of args /** other commands (as, ld, ...) */; + | ClangError string + | NonCCCommand args /** other commands (as, ld, ...) */; type quoting_style = | DoubleQuotes /** the arguments are ready to be enclosed in "double quotes" */ diff --git a/infer/src/clang/InferClang.re b/infer/src/clang/InferClang.re index 39e88fde3..2ddd3a7e0 100644 --- a/infer/src/clang/InferClang.re +++ b/infer/src/clang/InferClang.re @@ -5,10 +5,10 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ + /** Given a clang command, normalize it via `clang -###` if needed to get a clear view of what work is being done and which source files are being compiled, if any, then replace compilation commands by our own clang with our plugin attached for each source file. */ - open! Utils; @@ -28,10 +28,9 @@ let normalize (args: array string) :list ClangCommand.t => if (string_is_prefix " \"" line) { /* massage line to remove edge-cases for splitting */ "\"" ^ line ^ " \"" |> - /* split by whitespace */ - Str.split (Str.regexp_string "\" \"") |> - Array.of_list |> - ClangCommand.mk ClangCommand.DoubleQuotes + /* split by whitespace */ + Str.split (Str.regexp_string "\" \"") |> Array.of_list |> + ClangCommand.mk ClangCommand.DoubleQuotes } else { ClangCommand.ClangError line }; @@ -91,13 +90,7 @@ let execute_clang_command (clang_cmd: ClangCommand.t) => exit 1 | Assembly args => /* We shouldn't get any assembly command at this point */ - ( - if Config.debug_mode { - failwithf - } else { - Logging.err - } - ) + (if Config.debug_mode {failwithf} else {Logging.err}) "WARNING: unexpected assembly command: %s@\n" (ClangCommand.command_to_run args) | NonCCCommand args => /* Non-compilation (eg, linking) command. Run the command as-is. It will not get captured diff --git a/infer/src/scripts/StatsAggregator.re b/infer/src/scripts/StatsAggregator.re index 3b8b9e886..b1a3b228a 100644 --- a/infer/src/scripts/StatsAggregator.re +++ b/infer/src/scripts/StatsAggregator.re @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2016 - present Facebook, Inc. * All rights reserved. * @@ -9,7 +6,6 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; let aggregated_stats_filename = "aggregated_stats.json"; @@ -18,10 +14,8 @@ let aggregated_stats_by_target_filename = "aggregated_stats_by_target.json"; let json_files_to_ignore_regex = Str.regexp ( ".*\\(" ^ - Str.quote aggregated_stats_filename ^ - "\\|" ^ - Str.quote aggregated_stats_by_target_filename ^ - "\\)$" + Str.quote aggregated_stats_filename ^ + "\\|" ^ Str.quote aggregated_stats_by_target_filename ^ "\\)$" ); let dir_exists dir => @@ -34,7 +28,7 @@ let find_json_files_in_dir dir => { let s = Unix.lstat path; let json_regex = Str.regexp_case_fold ".*\\.json$"; not (Str.string_match json_files_to_ignore_regex path 0) && - Str.string_match json_regex path 0 && s.st_kind == Unix.S_REG + Str.string_match json_regex path 0 && s.st_kind == Unix.S_REG }; dir_exists dir ? { @@ -51,7 +45,9 @@ type stats_paths = { reporting_paths: list string }; -type origin = | Buck_out of (list (string, stats_paths)) | Infer_out of stats_paths; +type origin = + | Buck_out (list (string, stats_paths)) + | Infer_out stats_paths; let find_stats_files_in_dir dir => { let frontend_paths = find_json_files_in_dir (Filename.concat dir Config.frontend_stats_dir_name); diff --git a/infer/src/scripts/StatsAggregator.rei b/infer/src/scripts/StatsAggregator.rei index 08600ca96..e92b0aede 100644 --- a/infer/src/scripts/StatsAggregator.rei +++ b/infer/src/scripts/StatsAggregator.rei @@ -1,7 +1,4 @@ /* - * vim: set ft=rust: - * vim: set ft=reason: - * * Copyright (c) 2016 - present Facebook, Inc. * All rights reserved. * @@ -9,5 +6,4 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ - open! Utils; diff --git a/infer/src/scripts/checkCopyright.ml b/infer/src/scripts/checkCopyright.ml index d153c1e89..6437ceafc 100644 --- a/infer/src/scripts/checkCopyright.ml +++ b/infer/src/scripts/checkCopyright.ml @@ -95,7 +95,7 @@ let find_comment_end lines_arr n com_style = done; match com_style with | Line _ -> !found - | Block _ -> !found + 1 + | Block _ -> !found (** Heuristic to check if this looks like a copyright message. *) let looks_like_copyright_message cstart cend lines_arr = @@ -143,7 +143,7 @@ let pp_copyright mono fb_year com_style fmt _prefix = | Block (start, _, _) -> F.fprintf fmt "%s@\n" start in let pp_end () = match com_style with | Line _ -> F.fprintf fmt "@\n"; - | Block (_, _, finish) -> F.fprintf fmt "%s%s@\n@\n" _prefix finish in + | Block (_, _, finish) -> F.fprintf fmt "%s%s@\n" _prefix finish in pp_start (); if mono then pp_line " Copyright (c) 2009 - 2013 Monoidics ltd."; diff --git a/scripts/reup.sh b/scripts/reup.sh new file mode 100755 index 000000000..b698ed146 --- /dev/null +++ b/scripts/reup.sh @@ -0,0 +1,16 @@ +#/bin/bash + +# Copyright (c) 2016 - present Facebook, Inc. +# All rights reserved. +# +# This source code is licensed under the BSD style license found in the +# LICENSE file in the root directory of this source tree. An additional grant +# of patent rights can be found in the PATENTS file in the same directory. + + +# re-format reason code + +base=`basename $0` +TMPFILE=`mktemp -t ${base}` || exit 1 +refmt -print-width 100 -heuristics-file unary.txt -parse re -print re $1 > $TMPFILE +mv $TMPFILE $1