diff --git a/infer/src/IR/Const.re b/infer/src/IR/Const.re index 8fde16d39..2c5866463 100644 --- a/infer/src/IR/Const.re +++ b/infer/src/IR/Const.re @@ -40,11 +40,11 @@ let compare (c1: t) (c2: t) :int => | (Cfloat f1, Cfloat f2) => float_compare f1 f2 | (Cfloat _, _) => (-1) | (_, Cfloat _) => 1 - | (Cclass c1, Cclass c2) => Ident.name_compare c1 c2 + | (Cclass c1, Cclass c2) => Ident.compare_name c1 c2 | (Cclass _, _) => (-1) | (_, Cclass _) => 1 | (Cptr_to_fld fn1 t1, Cptr_to_fld fn2 t2) => - let n = Ident.fieldname_compare fn1 fn2; + let n = Ident.compare_fieldname fn1 fn2; if (n != 0) { n } else { diff --git a/infer/src/IR/Exp.re b/infer/src/IR/Exp.re index ef5f42748..284053ff8 100644 --- a/infer/src/IR/Exp.re +++ b/infer/src/IR/Exp.re @@ -133,7 +133,7 @@ let rec compare e1 e2 => if (n != 0) { n } else { - let n = Ident.fieldname_compare f1 f2; + let n = Ident.compare_fieldname f1 f2; if (n != 0) { n } else { diff --git a/infer/src/IR/Ident.re b/infer/src/IR/Ident.re index c87826fed..f11bbee36 100644 --- a/infer/src/IR/Ident.re +++ b/infer/src/IR/Ident.re @@ -18,119 +18,72 @@ let module L = Logging; let module F = Format; -type name = string; +type name = string [@@deriving compare]; -type fieldname = {fpos: int, fname: Mangled.t}; +let equal_name x y => 0 == compare_name x y; -type kind = int; +type fieldname = {fpos: int, fname: Mangled.t} [@@deriving compare]; -let kprimed = (-1); +let equal_fieldname x y => 0 == compare_fieldname x y; -let knormal = 0; +type kind = + | KNone + /** special kind of "null ident" (basically, a more compact way of implementing an ident option). + useful for situations when an instruction requires an id, but no one should read the result. */ + | KFootprint + | KNormal + | KPrimed +[@@deriving compare]; -let kfootprint = 1; +let kfootprint = KFootprint; +let knormal = KNormal; -/** special kind of "null ident" (basically, a more compact way of implementing an ident option). - useful for situations when an instruction requires an id, but no one should read the result. */ -let knone = 2; +let kprimed = KPrimed; + +let equal_kind x y => 0 == compare_kind x y; /* timestamp for a path identifier */ let path_ident_stamp = (-3); -type t = {kind: int, name: name, stamp: int}; - -type _ident = t; - - -/** {2 Comparison Functions} */ -let name_compare = string_compare; - -let fieldname_compare fn1 fn2 => { - let n = int_compare fn1.fpos fn2.fpos; - if (n != 0) { - n - } else { - Mangled.compare fn1.fname fn2.fname - } -}; +type t = {kind: kind, name: name, stamp: int} [@@deriving compare]; -let name_equal = string_equal; - -let kind_equal k1 k2 => k1 === k2; - -let compare i1 i2 => { - let n = i2.kind - i1.kind; - if (n != 0) { - n - } else { - let n = name_compare i1.name i2.name; - if (n != 0) { - n - } else { - int_compare i1.stamp i2.stamp - } - } -}; - -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; - -let rec ident_list_compare il1 il2 => - switch (il1, il2) { - | ([], []) => 0 - | ([], _) => (-1) - | (_, []) => 1 - | ([i1, ...l1], [i2, ...l2]) => - let n = compare i1 i2; - if (n != 0) { - n - } else { - ident_list_compare l1 l2 - } - }; - -let ident_list_equal ids1 ids2 => ident_list_compare ids1 ids2 == 0; +/* most unlikely first */ +let equal i1 i2 => i1.stamp === i2.stamp && i1.kind === i2.kind && equal_name i1.name i2.name; /** {2 Set for identifiers} */ let module IdentSet = Set.Make { - type t = _ident; + type nonrec t = t; let compare = compare; }; let module IdentMap = Map.Make { - type t = _ident; + type nonrec t = t; let compare = compare; }; let module IdentHash = Hashtbl.Make { - type t = _ident; + type nonrec t = t; let equal = equal; let hash (id: t) => Hashtbl.hash id; }; let module FieldSet = Set.Make { - type t = fieldname; - let compare = fieldname_compare; + type t = fieldname [@@deriving compare]; }; let module FieldMap = Map.Make { - type t = fieldname; - let compare = fieldname_compare; + type t = fieldname [@@deriving compare]; }; let idlist_to_idset ids => IList.fold_left (fun set id => IdentSet.add id set) IdentSet.empty ids; /** {2 Conversion between Names and Strings} */ - let module NameHash = Hashtbl.Make { type t = name; - let equal = name_equal; + let equal = equal_name; let hash = Hashtbl.hash; }; @@ -215,7 +168,7 @@ let fieldname_hidden = create_fieldname (Mangled.from_string ".hidden") 0; /** hidded fieldname constant */ -let fieldname_is_hidden fn => fieldname_equal fn fieldname_hidden; +let fieldname_is_hidden fn => equal_fieldname fn fieldname_hidden; /** {2 Functions and Hash Tables for Managing Stamps} */ @@ -288,9 +241,9 @@ let name_return = Mangled.from_string "return"; /** Return the standard name for the given kind */ let standard_name kind => - if (kind === knormal || kind === knone) { + if (kind === KNormal || kind === KNone) { name_normal - } else if (kind === kfootprint) { + } else if (kind === KFootprint) { name_footprint } else { name_primed @@ -309,21 +262,21 @@ let create kind stamp => create_with_stamp kind (standard_name kind) stamp; /** Generate a normal identifier with the given name and stamp */ -let create_normal name stamp => create_with_stamp knormal name stamp; +let create_normal name stamp => create_with_stamp KNormal name stamp; /** Create a fresh identifier with default name for the given kind. */ let create_fresh kind => NameGenerator.create_fresh_ident kind (standard_name kind); -let create_none () => create_fresh knone; +let create_none () => create_fresh KNone; /** Generate a primed identifier with the given name and stamp */ -let create_primed name stamp => create_with_stamp kprimed name stamp; +let create_primed name stamp => create_with_stamp KPrimed name stamp; /** Generate a footprint identifier with the given name and stamp */ -let create_footprint name stamp => create_with_stamp kfootprint name stamp; +let create_footprint name stamp => create_with_stamp KFootprint name stamp; /** {2 Functions for Identifiers} */ @@ -331,23 +284,23 @@ let create_footprint name stamp => create_with_stamp kfootprint name stamp; /** Get a name of an identifier */ let get_name id => id.name; -let is_primed (id: t) => id.kind === kprimed; +let is_primed (id: t) => id.kind === KPrimed; -let is_normal (id: t) => id.kind === knormal || id.kind === knone; +let is_normal (id: t) => id.kind === KNormal || id.kind === KNone; -let is_footprint (id: t) => id.kind === kfootprint; +let is_footprint (id: t) => id.kind === KFootprint; -let is_none (id: t) => id.kind == knone; +let is_none (id: t) => id.kind == KNone; -let is_path (id: t) => id.kind === knormal && id.stamp == path_ident_stamp; +let is_path (id: t) => id.kind === KNormal && id.stamp == path_ident_stamp; let make_unprimed id => - if (id.kind != kprimed) { + if (id.kind != KPrimed) { assert false - } else if (id.kind === knone) { - {...id, kind: knone} + } else if (id.kind === KNone) { + {...id, kind: KNone} } else { - {...id, kind: knormal} + {...id, kind: KNormal} }; @@ -367,14 +320,14 @@ let create_path pathstring => /** Convert an identifier to a string. */ let to_string id => - if (id.kind === knone) { + if (id.kind === KNone) { "_" } else { let base_name = name_to_string id.name; let prefix = - if (id.kind === kfootprint) { + if (id.kind === KFootprint) { "@" - } else if (id.kind === knormal) { + } else if (id.kind === KNormal) { "" } else { "_" @@ -406,9 +359,9 @@ let pp pe f id => | PP_LATEX => let base_name = name_to_string id.name; let style = - if (id.kind == kfootprint) { + if (id.kind == KFootprint) { Latex.Boldface - } else if (id.kind == knormal) { + } else if (id.kind == KNormal) { Latex.Roman } else { Latex.Roman diff --git a/infer/src/IR/Ident.rei b/infer/src/IR/Ident.rei index 4e2ebfa70..522b2ef95 100644 --- a/infer/src/IR/Ident.rei +++ b/infer/src/IR/Ident.rei @@ -16,19 +16,35 @@ open! Utils; /** Identifiers: program variables and logical variables */ /** Program and logical variables. */ -type t; +type t [@@deriving compare]; + + +/** Equality for identifiers. */ +let equal: t => t => bool; /** Names used to replace strings. */ -type name; +type name [@@deriving compare]; + + +/** Equality for names. */ +let equal_name: name => name => bool; /** Names for fields of class/struct/union */ -type fieldname; +type fieldname [@@deriving compare]; + + +/** Equality for field names. */ +let equal_fieldname: fieldname => fieldname => bool; /** Kind of identifiers. */ -type kind; +type kind [@@deriving compare]; + + +/** Equality for kind. */ +let equal_kind: kind => kind => bool; /** Set for identifiers. */ @@ -210,44 +226,6 @@ let get_stamp: t => int; let set_stamp: t => int => t; -/** {2 Comparision Functions} */ - -/** Comparison for names. */ -let name_compare: name => name => int; - - -/** Comparison for field names. */ -let fieldname_compare: fieldname => fieldname => int; - - -/** Equality for names. */ -let name_equal: name => name => bool; - - -/** Equality for field names. */ -let fieldname_equal: fieldname => fieldname => bool; - - -/** Equality for kind. */ -let kind_equal: kind => kind => bool; - - -/** Comparison for identifiers. */ -let compare: t => t => int; - - -/** Equality for identifiers. */ -let equal: t => t => bool; - - -/** Comparison for lists of identities */ -let ident_list_compare: list t => list t => int; - - -/** Equality for lists of identities */ -let ident_list_equal: list t => list t => bool; - - /** {2 Pretty Printing} */ /** Pretty print a name. */ diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 6fcc062c0..91df934cb 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -408,7 +408,7 @@ let rec strexp_compare inst::inst=false se1 se2 => } } } -and fld_strexp_compare fse1 fse2 => pair_compare Ident.fieldname_compare strexp_compare fse1 fse2 +and fld_strexp_compare fse1 fse2 => pair_compare Ident.compare_fieldname strexp_compare fse1 fse2 and fld_strexp_list_compare fsel1 fsel2 => IList.compare fld_strexp_compare fsel1 fsel2 and exp_strexp_compare ese1 ese2 => pair_compare Exp.compare strexp_compare ese1 ese2 and exp_strexp_list_compare esel1 esel2 => IList.compare exp_strexp_compare esel1 esel2; @@ -508,11 +508,11 @@ and hpara_compare hp1 hp2 => { if (n != 0) { n } else { - let n = Ident.ident_list_compare hp1.svars hp2.svars; + let n = IList.compare Ident.compare hp1.svars hp2.svars; if (n != 0) { n } else { - let n = Ident.ident_list_compare hp1.evars hp2.evars; + let n = IList.compare Ident.compare hp1.evars hp2.evars; if (n != 0) { n } else { @@ -535,11 +535,11 @@ and hpara_dll_compare hp1 hp2 => { if (n != 0) { n } else { - let n = Ident.ident_list_compare hp1.svars_dll hp2.svars_dll; + let n = IList.compare Ident.compare hp1.svars_dll hp2.svars_dll; if (n != 0) { n } else { - let n = Ident.ident_list_compare hp1.evars_dll hp2.evars_dll; + let n = IList.compare Ident.compare hp1.evars_dll hp2.evars_dll; if (n != 0) { n } else { @@ -2479,7 +2479,7 @@ let rec exp_compare_structural e1 e2 exp_map => { if (n != 0) { n } else { - let n = Ident.fieldname_compare f1 f2; + let n = Ident.compare_fieldname f1 f2; if (n != 0) { n } else { diff --git a/infer/src/IR/StructTyp.re b/infer/src/IR/StructTyp.re index 9a205208b..d06580857 100644 --- a/infer/src/IR/StructTyp.re +++ b/infer/src/IR/StructTyp.re @@ -33,7 +33,7 @@ type t = { type lookup = Typename.t => option t; let fld_typ_ann_compare fta1 fta2 => - triple_compare Ident.fieldname_compare Typ.compare Annot.Item.compare fta1 fta2; + triple_compare Ident.compare_fieldname Typ.compare Annot.Item.compare fta1 fta2; let pp pe pp_base name f {fields} => if false { @@ -107,7 +107,7 @@ let fld_typ lookup::lookup default::default fn (typ: Typ.t) => | Tstruct name => switch (lookup name) { | Some {fields} => - try (snd3 (IList.find (fun (f, _, _) => Ident.fieldname_equal f fn) fields)) { + try (snd3 (IList.find (fun (f, _, _) => Ident.equal_fieldname f fn) fields)) { | Not_found => default } | None => default @@ -123,7 +123,7 @@ let get_field_type_and_annotation lookup::lookup fn (typ: Typ.t) => | Some {fields, statics} => try { let (_, t, a) = - IList.find (fun (f, _, _) => Ident.fieldname_equal f fn) (fields @ statics); + IList.find (fun (f, _, _) => Ident.equal_fieldname f fn) (fields @ statics); Some (t, a) } { | Not_found => None diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index e2d23aceb..982e8f7bf 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -469,7 +469,7 @@ let discover_para_candidates tenv p = let edges = ref [] in let add_edge edg = edges := edg :: !edges in let get_edges_strexp rec_flds root se = - let is_rec_fld fld = IList.exists (Ident.fieldname_equal fld) rec_flds in + let is_rec_fld fld = IList.exists (Ident.equal_fieldname fld) rec_flds in match se with | Sil.Eexp _ | Sil.Earray _ -> () | Sil.Estruct (fsel, _) -> @@ -505,7 +505,7 @@ let discover_para_dll_candidates tenv p = let edges = ref [] in let add_edge edg = (edges := edg :: !edges) in let get_edges_strexp rec_flds root se = - let is_rec_fld fld = IList.exists (Ident.fieldname_equal fld) rec_flds in + let is_rec_fld fld = IList.exists (Ident.equal_fieldname fld) rec_flds in match se with | Sil.Eexp _ | Sil.Earray _ -> () | Sil.Estruct (fsel, _) -> @@ -1004,7 +1004,7 @@ let cycle_has_weak_or_unretained_or_assign_field tenv cycle = let get_item_annotation (t: Typ.t) fn = match t with | Tstruct name -> ( - let equal_fn (fn', _, _) = Ident.fieldname_equal fn fn' in + let equal_fn (fn', _, _) = Ident.equal_fieldname fn fn' in match Tenv.lookup tenv name with | Some { fields; statics } -> ( try trd3 (IList.find equal_fn (fields @ statics)) diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml index bf335957e..a22afd4c8 100644 --- a/infer/src/backend/absarray.ml +++ b/infer/src/backend/absarray.ml @@ -76,8 +76,8 @@ end = struct | Sil.Estruct (fsel, _), Tstruct name, Field (fld, _) :: syn_offs' -> ( match Tenv.lookup tenv name with | Some { fields } -> - let se' = snd (IList.find (fun (f', _) -> Ident.fieldname_equal f' fld) fsel) in - let t' = snd3 (IList.find (fun (f', _, _) -> Ident.fieldname_equal f' fld) fields) in + let se' = snd (IList.find (fun (f', _) -> Ident.equal_fieldname f' fld) fsel) in + let t' = snd3 (IList.find (fun (f', _, _) -> Ident.equal_fieldname f' fld) fields) in get_strexp_at_syn_offsets tenv se' t' syn_offs' | None -> fail () @@ -96,14 +96,14 @@ end = struct | Sil.Estruct (fsel, inst), Tstruct name, Field (fld, _) :: syn_offs' -> ( match Tenv.lookup tenv name with | Some { fields } -> - let se' = snd (IList.find (fun (f', _) -> Ident.fieldname_equal f' fld) fsel) in + let se' = snd (IList.find (fun (f', _) -> Ident.equal_fieldname f' fld) fsel) in let t' = (fun (_,y,_) -> y) (IList.find (fun (f', _, _) -> - Ident.fieldname_equal f' fld) fields) in + Ident.equal_fieldname f' fld) fields) in let se_mod = replace_strexp_at_syn_offsets tenv se' t' syn_offs' update in let fsel' = IList.map (fun (f'', se'') -> - if Ident.fieldname_equal f'' fld then (fld, se_mod) else (f'', se'') + if Ident.equal_fieldname f'' fld then (fld, se_mod) else (f'', se'') ) fsel in Sil.Estruct (fsel', inst) | None -> @@ -178,7 +178,7 @@ end = struct | (f, se) :: fsel' -> begin try - let t = snd3 (IList.find (fun (f', _, _) -> Ident.fieldname_equal f' f) ftal) in + let t = snd3 (IList.find (fun (f', _, _) -> Ident.equal_fieldname f' f) ftal) in find_offset_sexp sigma_other hpred root ((Field (f, typ)) :: offs) se t with Not_found -> L.d_strln ("Can't find field " ^ (Ident.fieldname_to_string f) ^ " in StrexpMatch.find") diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index f23ca4083..6a6813945 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -961,7 +961,7 @@ let rec exp_partial_join (e1: Exp.t) (e2: Exp.t) : Exp.t = if not (Pvar.equal pvar1 pvar2) then (L.d_strln "failure reason 25"; raise IList.Fail) else e1 | Exp.Lfield(e1, f1, t1), Exp.Lfield(e2, f2, _) -> - if not (Ident.fieldname_equal f1 f2) then (L.d_strln "failure reason 26"; raise IList.Fail) + if not (Ident.equal_fieldname f1 f2) then (L.d_strln "failure reason 26"; raise IList.Fail) else Exp.Lfield(exp_partial_join e1 e2, f1, t1) (* should be t1 = t2 *) | Exp.Lindex(e1, e1'), Exp.Lindex(e2, e2') -> let e1'' = exp_partial_join e1 e2 in @@ -1044,7 +1044,7 @@ let rec exp_partial_meet (e1: Exp.t) (e2: Exp.t) : Exp.t = if not (Pvar.equal pvar1 pvar2) then (L.d_strln "failure reason 35"; raise IList.Fail) else e1 | Exp.Lfield(e1, f1, t1), Exp.Lfield(e2, f2, _) -> - if not (Ident.fieldname_equal f1 f2) then (L.d_strln "failure reason 36"; raise IList.Fail) + if not (Ident.equal_fieldname f1 f2) then (L.d_strln "failure reason 36"; raise IList.Fail) else Exp.Lfield(exp_partial_meet e1 e2, f1, t1) (* should be t1 = t2 *) | Exp.Lindex(e1, e1'), Exp.Lindex(e2, e2') -> let e1'' = exp_partial_meet e1 e2 in @@ -1071,7 +1071,7 @@ let rec strexp_partial_join mode (strexp1: Sil.strexp) (strexp2: Sil.strexp) : S | JoinState.Post -> Sil.Estruct (IList.rev acc, inst) end | (fld1, se1):: fld_se_list1', (fld2, se2):: fld_se_list2' -> - let comparison = Ident.fieldname_compare fld1 fld2 in + let comparison = Ident.compare_fieldname fld1 fld2 in if comparison = 0 then let strexp' = strexp_partial_join mode se1 se2 in let fld_se_list_new = (fld1, strexp') :: acc in @@ -1135,7 +1135,7 @@ let rec strexp_partial_meet (strexp1: Sil.strexp) (strexp2: Sil.strexp) : Sil.st | _, [] -> Sil.Estruct (construct Lhs acc fld_se_list1, inst) | (fld1, se1):: fld_se_list1', (fld2, se2):: fld_se_list2' -> - let comparison = Ident.fieldname_compare fld1 fld2 in + let comparison = Ident.compare_fieldname fld1 fld2 in if comparison < 0 then let se' = strexp_construct_fresh Lhs se1 in let acc_new = (fld1, se'):: acc in diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 20957407c..b241d191a 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -384,7 +384,7 @@ let in_cycle cycle edge = match cycle with | Some cycle' -> IList.mem (fun (fn, se) (_,fn',se') -> - Ident.fieldname_equal fn fn' && Sil.strexp_equal se se') edge cycle' + Ident.equal_fieldname fn fn' && Sil.strexp_equal se se') edge cycle' | _ -> false let node_in_cycle cycle node = @@ -655,7 +655,7 @@ let filter_useless_spec_dollar_box (nodes: dotty_node list) (links: link list) = else boxes_pointing_at n ln' in let is_spec_variable = function | Exp.Var id -> - Ident.is_normal id && Ident.name_equal (Ident.get_name id) Ident.name_spec + Ident.is_normal id && Ident.equal_name (Ident.get_name id) Ident.name_spec | _ -> false in let handle_one_node node = match node with diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index ebb9bfea2..cbf2005f5 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -582,7 +582,7 @@ let vpath_find tenv prop _exp : DExp.t option * Typ.t option = | Exp.Sizeof (Tstruct name, _, _) -> ( match Tenv.lookup tenv name with | Some {fields} -> ( - match IList.find (fun (f', _, _) -> Ident.fieldname_equal f' f) fields with + match IList.find (fun (f', _, _) -> Ident.equal_fieldname f' f) fields with | _, t, _ -> Some t | exception Not_found -> None ) @@ -684,7 +684,7 @@ let explain_dexp_access prop dexp is_nullable = (L.d_strln ("lookup_fld: can't find field " ^ Ident.fieldname_to_string f)); None | (f1, se):: fsel' -> - if Ident.fieldname_equal f1 f then Some se + if Ident.equal_fieldname f1 f then Some se else lookup_fld fsel' f in let rec lookup_esel esel e = match esel with | [] -> diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml index 0f4c09922..f0bca1a23 100644 --- a/infer/src/backend/match.ml +++ b/infer/src/backend/match.ml @@ -74,7 +74,7 @@ let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option = check_equal sub vars e1 e2 | Exp.Lvar _, _ | _, Exp.Lvar _ -> check_equal sub vars e1 e2 - | Exp.Lfield(e1', fld1, _), Exp.Lfield(e2', fld2, _) when (Ident.fieldname_equal fld1 fld2) -> + | Exp.Lfield(e1', fld1, _), Exp.Lfield(e2', fld2, _) when (Ident.equal_fieldname fld1 fld2) -> exp_match e1' sub vars e2' | Exp.Lfield _, _ | _, Exp.Lfield _ -> None @@ -121,7 +121,7 @@ and fsel_match fsel1 sub vars fsel2 = if (Config.abs_struct <= 0) then None else Some (sub, vars) (* This can lead to great information loss *) | (fld1, se1') :: fsel1', (fld2, se2') :: fsel2' -> - let n = Ident.fieldname_compare fld1 fld2 in + let n = Ident.compare_fieldname fld1 fld2 in if (n = 0) then begin match strexp_match se1' sub vars se2' with | None -> None @@ -517,7 +517,7 @@ and generate_todos_from_fel mode todos fel1 fel2 = | _, [] -> if mode == LFieldForget then Some todos else None | (fld1, strexp1) :: fel1', (fld2, strexp2) :: fel2' -> - let n = Ident.fieldname_compare fld1 fld2 in + let n = Ident.compare_fieldname fld1 fld2 in if (n = 0) then begin match generate_todos_from_strexp mode todos strexp1 strexp2 with diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 590b1966e..da214226b 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1270,7 +1270,7 @@ module Normalize = struct (* n1-e1 == n2 -> e1==n1-n2 *) (e1, Exp.int (n1 -- n2)) | Lfield (e1', fld1, _), Lfield (e2', fld2, _) -> - if Ident.fieldname_equal fld1 fld2 + if Ident.equal_fieldname fld1 fld2 then normalize_eq (e1', e2') else eq | Lindex (e1', idx1), Lindex (e2', idx2) -> diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml index 457152a5c..7e83a6e7e 100644 --- a/infer/src/backend/propgraph.ml +++ b/infer/src/backend/propgraph.ml @@ -138,7 +138,7 @@ let rec compute_sexp_diff (se1: Sil.strexp) (se2: Sil.strexp) : Obj.t list = mat and compute_fsel_diff fsel1 fsel2 : Obj.t list = match fsel1, fsel2 with | ((f1, se1):: fsel1'), (((f2, se2) as x):: fsel2') -> - (match Ident.fieldname_compare f1 f2 with + (match Ident.compare_fieldname f1 f2 with | n when n < 0 -> compute_fsel_diff fsel1' fsel2 | 0 -> compute_sexp_diff se1 se2 @ compute_fsel_diff fsel1' fsel2' | _ -> (Obj.repr x) :: compute_fsel_diff fsel1 fsel2') diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 76f9c3b26..1a5809005 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -1335,7 +1335,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Ide | _, [] -> subs, fsel1, [] | (f1, se1) :: fsel1', (f2, se2) :: fsel2' -> begin - match Ident.fieldname_compare f1 f2 with + match Ident.compare_fieldname f1 f2 with | 0 -> let typ' = StructTyp.fld_typ ~lookup ~default:Typ.Tvoid f2 typ2 in let subs', se_frame, se_missing = diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 725e43f92..8dcf76fb2 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -105,14 +105,14 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp | Tstruct name, (Off_fld (f, _)) :: off' -> ( match Tenv.lookup tenv name with | Some ({ fields; statics; } as struct_typ) -> ( - match IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') (fields @ statics) with + match IList.find (fun (f', _, _) -> Ident.equal_fieldname f f') (fields @ statics) with | _, t', _ -> let atoms', se', res_t' = create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst in let se = Sil.Estruct ([(f, se')], inst) in let replace_typ_of_f (f', t', a') = - if Ident.fieldname_equal f f' then (f, res_t', a') else (f', t', a') in + if Ident.equal_fieldname f f' then (f, res_t', a') else (f', t', a') in let fields' = IList.sort StructTyp.fld_typ_ann_compare (IList.map replace_typ_of_f fields) in ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ; @@ -206,10 +206,10 @@ let rec _strexp_extend_values | (Off_fld (f, _)) :: off', Sil.Estruct (fsel, inst'), Tstruct name -> ( match Tenv.lookup tenv name with | Some ({ fields; statics; } as struct_typ) -> ( - let replace_fv new_v fv = if Ident.fieldname_equal (fst fv) f then (f, new_v) else fv in - match IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') (fields @ statics) with + let replace_fv new_v fv = if Ident.equal_fieldname (fst fv) f then (f, new_v) else fv in + match IList.find (fun (f', _, _) -> Ident.equal_fieldname f f') (fields @ statics) with | _, typ', _ -> ( - match IList.find (fun (f', _) -> Ident.fieldname_equal f f') fsel with + match IList.find (fun (f', _) -> Ident.equal_fieldname f f') fsel with | _, se' -> let atoms_se_typ_list' = _strexp_extend_values @@ -232,7 +232,7 @@ let rec _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp typ' off' inst in let res_fsel' = IList.sort Sil.fld_strexp_compare ((f, se'):: fsel) in let replace_fta (f', t', a') = - if Ident.fieldname_equal f' f then (f, res_typ', a') else (f', t', a') in + if Ident.equal_fieldname f' f then (f, res_typ', a') else (f', t', a') in let fields' = IList.sort StructTyp.fld_typ_ann_compare (IList.map replace_fta fields) in ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ; @@ -470,7 +470,7 @@ let prop_iter_check_fields_ptsto_shallow tenv iter lexp = (match se with | Sil.Estruct (fsel, _) -> (try - let _, se' = IList.find (fun (fld', _) -> Ident.fieldname_equal fld fld') fsel in + let _, se' = IList.find (fun (fld', _) -> Ident.equal_fieldname fld fld') fsel in check_offset se' off' with Not_found -> Some fld) | _ -> Some fld) @@ -534,7 +534,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = pname tenv orig_prop false extend_kind max_stamp se te offset inst in IList.map (atoms_se_te_to_iter e) atoms_se_te_list in let res_iter_list = - if Ident.kind_equal extend_kind Ident.kprimed + if Ident.equal_kind extend_kind Ident.kprimed then iter_list (* normal part already extended: nothing to do *) else (* extend footprint part *) let atoms_fp_sigma_list = @@ -842,7 +842,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc = IList.exists (fun (fld, strexp) -> match strexp with | Sil.Eexp (rhs_exp, _) -> - Exp.equal exp rhs_exp && not (Ident.fieldname_equal fld accessed_fld) + Exp.equal exp rhs_exp && not (Ident.equal_fieldname fld accessed_fld) | _ -> false) flds @@ -1119,7 +1119,7 @@ let type_at_offset tenv texp off = | (Off_fld (f, _)) :: off', Tstruct name -> ( match Tenv.lookup tenv name with | Some { fields } -> ( - match IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') fields with + match IList.find (fun (f', _, _) -> Ident.equal_fieldname f f') fields with | _, typ', _ -> strip_offset off' typ' | exception Not_found -> None ) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 068d96308..c944abe85 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -17,7 +17,7 @@ module F = Format let rec fldlist_assoc fld = function | [] -> raise Not_found - | (fld', x, _):: l -> if Ident.fieldname_equal fld fld' then x else fldlist_assoc fld l + | (fld', x, _):: l -> if Ident.equal_fieldname fld fld' then x else fldlist_assoc fld l let unroll_type tenv (typ: Typ.t) (off: Sil.offset) = let fail fld_to_string fld = @@ -141,17 +141,17 @@ let rec apply_offlist match Tenv.lookup tenv name with | Some ({fields} as struct_typ) -> ( let t' = unroll_type tenv typ (Sil.Off_fld (fld, fld_typ)) in - match IList.find (fun fse -> Ident.fieldname_equal fld (fst fse)) fsel with + match IList.find (fun fse -> Ident.equal_fieldname fld (fst fse)) fsel with | _, se' -> let res_e', res_se', res_t', res_pred_insts_op' = apply_offlist pdesc tenv p fp_root nullify_struct (root_lexp, se', t') offlist' f inst lookup_inst in let replace_fse fse = - if Ident.fieldname_equal fld (fst fse) then (fld, res_se') else fse in + if Ident.equal_fieldname fld (fst fse) then (fld, res_se') else fse in let res_se = Sil.Estruct (IList.map replace_fse fsel, inst') in let replace_fta (f, t, a) = - if Ident.fieldname_equal fld f then (fld, res_t', a) else (f, t, a) in + if Ident.equal_fieldname fld f then (fld, res_t', a) else (f, t, a) in let fields' = IList.map replace_fta fields in ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ; (res_e', res_se, typ, res_pred_insts_op') diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 857c20366..2fe5b89c6 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -418,7 +418,7 @@ let rec fsel_star_fld fsel1 fsel2 = match fsel1, fsel2 with | [], fsel2 -> fsel2 | fsel1,[] -> fsel1 | (f1, se1):: fsel1', (f2, se2):: fsel2' -> - (match Ident.fieldname_compare f1 f2 with + (match Ident.compare_fieldname f1 f2 with | 0 -> (f1, sexp_star_fld se1 se2) :: fsel_star_fld fsel1' fsel2' | n when n < 0 -> (f1, se1) :: fsel_star_fld fsel1' fsel2 | _ -> (f2, se2) :: fsel_star_fld fsel1 fsel2') @@ -461,7 +461,7 @@ let texp_star tenv texp1 texp2 = | [], _ -> true | _, [] -> false | (f1, _, _):: ftal1', (f2, _, _):: ftal2' -> - begin match Ident.fieldname_compare f1 f2 with + begin match Ident.compare_fieldname f1 f2 with | n when n < 0 -> false | 0 -> ftal_sub ftal1' ftal2' | _ -> ftal_sub ftal1 ftal2' end in diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml index 73dd123ae..171165b00 100644 --- a/infer/src/backend/taint.ml +++ b/infer/src/backend/taint.ml @@ -353,7 +353,7 @@ let tainted_params callee_pname = let has_taint_annotation fieldname (struct_typ: StructTyp.t) = let fld_has_taint_annot (fname, _, annot) = - Ident.fieldname_equal fieldname fname && + Ident.equal_fieldname fieldname fname && (Annotations.ia_is_privacy_source annot || Annotations.ia_is_integrity_source annot) in IList.exists fld_has_taint_annot struct_typ.fields || IList.exists fld_has_taint_annot struct_typ.statics diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index 5f10a9946..fced84744 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -42,7 +42,7 @@ let access_compare access1 access2 = else match access1, access2 with | FieldAccess (f1, typ1), FieldAccess (f2, typ2) -> - let n = Ident.fieldname_compare f1 f2 in + let n = Ident.compare_fieldname f1 f2 in if n <> 0 then n else Typ.compare typ1 typ2 diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index 76def35e0..6f11d664c 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/infer/src/checkers/patternMatch.ml @@ -123,7 +123,7 @@ let get_field_type_name tenv | Tstruct name | Tptr (Tstruct name, _) -> ( match Tenv.lookup tenv name with | Some { fields } -> ( - match IList.find (function | (fn, _, _) -> Ident.fieldname_equal fn fieldname) fields with + match IList.find (function | (fn, _, _) -> Ident.equal_fieldname fn fieldname) fields with | _, ft, _ -> Some (get_type_name ft) | exception Not_found -> None ) diff --git a/infer/src/clang/cFrontend_utils.ml b/infer/src/clang/cFrontend_utils.ml index c646eee36..4f55e8409 100644 --- a/infer/src/clang/cFrontend_utils.ml +++ b/infer/src/clang/cFrontend_utils.ml @@ -581,7 +581,7 @@ struct match field_tuple, l with | (field, typ, annot), ((old_field, old_typ, old_annot) as old_field_tuple :: rest) -> let ret_list, ret_found = replace_field field_tuple rest found in - if Ident.fieldname_equal field old_field && Typ.equal typ old_typ then + if Ident.equal_fieldname field old_field && Typ.equal typ old_typ then let annotations = append_no_duplicates_annotations annot old_annot in (field, typ, annotations) :: ret_list, true else old_field_tuple :: ret_list, ret_found @@ -599,7 +599,7 @@ struct let sort_fields fields = let compare (name1, _, _) (name2, _, _) = - Ident.fieldname_compare name1 name2 in + Ident.compare_fieldname name1 name2 in IList.sort compare fields diff --git a/infer/src/eradicate/typeErr.ml b/infer/src/eradicate/typeErr.ml index 94dacfd4b..79465bd26 100644 --- a/infer/src/eradicate/typeErr.ml +++ b/infer/src/eradicate/typeErr.ml @@ -86,28 +86,28 @@ module H = Hashtbl.Make(struct | Condition_redundant _, _ | _, Condition_redundant _ -> false | Field_not_initialized (fn1, pn1), Field_not_initialized (fn2, pn2) -> - Ident.fieldname_equal fn1 fn2 && + Ident.equal_fieldname fn1 fn2 && Procname.equal pn1 pn2 | Field_not_initialized (_, _), _ | _, Field_not_initialized (_, _) -> false | Field_not_mutable (fn1, _), Field_not_mutable (fn2, _) -> - Ident.fieldname_equal fn1 fn2 + Ident.equal_fieldname fn1 fn2 | Field_not_mutable _, _ | _, Field_not_mutable _ -> false | Field_annotation_inconsistent (ann1, fn1, _), Field_annotation_inconsistent (ann2, fn2, _) -> ann1 = ann2 && - Ident.fieldname_equal fn1 fn2 + Ident.equal_fieldname fn1 fn2 | Field_annotation_inconsistent _, _ | _, Field_annotation_inconsistent _ -> false | Field_over_annotated (fn1, pn1), Field_over_annotated (fn2, pn2) -> - Ident.fieldname_equal fn1 fn2 && + Ident.equal_fieldname fn1 fn2 && Procname.equal pn1 pn2 | Field_over_annotated (_, _), _ | _, Field_over_annotated (_, _) -> false | Null_field_access (so1, fn1, _, ii1), Null_field_access (so2, fn2, _, ii2) -> (opt_equal string_equal) so1 so2 && - Ident.fieldname_equal fn1 fn2 && + Ident.equal_fieldname fn1 fn2 && bool_equal ii1 ii2 | Null_field_access _, _ | _, Null_field_access _ -> false diff --git a/infer/src/eradicate/typeOrigin.ml b/infer/src/eradicate/typeOrigin.ml index de5d34409..1796d1c1a 100644 --- a/infer/src/eradicate/typeOrigin.ml +++ b/infer/src/eradicate/typeOrigin.ml @@ -45,7 +45,7 @@ let equal o1 o2 = match o1, o2 with | Const _, _ | _, Const _ -> false | Field (fn1, loc1), Field (fn2, loc2) -> - Ident.fieldname_equal fn1 fn2 && + Ident.equal_fieldname fn1 fn2 && Location.equal loc1 loc2 | Field _, _ | _, Field _ -> false