diff --git a/infer/src/Makefile.in b/infer/src/Makefile.in index 78c8daca9..775bf7f8f 100644 --- a/infer/src/Makefile.in +++ b/infer/src/Makefile.in @@ -92,13 +92,14 @@ OCAMLBUILD_OPTIONS = \ -cflags -w,@20 \ -cflags -w,@26 \ -cflags -w,@29 \ + -cflags -w,+32 \ -cflags -w,@33 \ -cflags -w,@34 \ -cflags -w,@35 \ -cflags -w,@37 \ -cflags -w,@38 \ -cflags -w,@39 \ - -tag-line "<*clang/clang_ast_*>: warn(-35-39)" \ + -tag-line "<*{clang/clang_ast_*,backend/jsonbug_*}>: warn(-32-35-39)" \ -tag-line "not <**/{config,iList,utils}.*>: open(Utils)" \ -lflags $(OCAML_INCLUDES) \ -cflags $(OCAML_INCLUDES) \ diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index eb333150c..b06193dce 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1103,24 +1103,6 @@ let get_cycle root prop = []) | _ -> L.d_strln "Root exp is not an allocated object. No cycle found"; [] -(** return a reachability function based on whether an id appears in several hpreds *) -let reachable_when_in_several_hpreds sigma : Ident.t -> bool = - let (id_hpred_map : HpredSet.t IdMap.t ref) = ref IdMap.empty (* map id to hpreds in which it occurs *) in - let add_id_hpred id hpred = - try - let hpred_set = IdMap.find id !id_hpred_map in - id_hpred_map := IdMap.add id (HpredSet.add hpred hpred_set) !id_hpred_map - with - | Not_found -> id_hpred_map := IdMap.add id (HpredSet.singleton hpred) !id_hpred_map in - let add_hpred hpred = - let fav = Sil.fav_new () in - Sil.hpred_fav_add fav hpred; - IList.iter (fun id -> add_id_hpred id hpred) (Sil.fav_to_list fav) in - let id_in_several_hpreds id = - HpredSet.cardinal (IdMap.find id !id_hpred_map) > 1 in - IList.iter add_hpred sigma; - id_in_several_hpreds - (* Check whether the hidden counter field of a struct representing an *) (* objective-c object is positive, and whether the leak is part of the *) @@ -1463,3 +1445,24 @@ let lifted_abstract pname tenv pset = abstracted_pset (***************** End of Main Abstraction Functions *****************) + +(* +(** return a reachability function based on whether an id appears in several hpreds *) +let reachable_when_in_several_hpreds sigma : Ident.t -> bool = + (* map id to hpreds in which it occurs *) + let (id_hpred_map : HpredSet.t IdMap.t ref) = ref IdMap.empty in + let add_id_hpred id hpred = + try + let hpred_set = IdMap.find id !id_hpred_map in + id_hpred_map := IdMap.add id (HpredSet.add hpred hpred_set) !id_hpred_map + with + | Not_found -> id_hpred_map := IdMap.add id (HpredSet.singleton hpred) !id_hpred_map in + let add_hpred hpred = + let fav = Sil.fav_new () in + Sil.hpred_fav_add fav hpred; + IList.iter (fun id -> add_id_hpred id hpred) (Sil.fav_to_list fav) in + let id_in_several_hpreds id = + HpredSet.cardinal (IdMap.find id !id_hpred_map) > 1 in + IList.iter add_hpred sigma; + id_in_several_hpreds +*) diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml index 2e36de2c0..a360a65da 100644 --- a/infer/src/backend/absarray.ml +++ b/infer/src/backend/absarray.ml @@ -41,18 +41,18 @@ module StrexpMatch : sig (** Get the array *) val get_data : t -> strexp_data - (** Get the partition of the sigma: the unmatched part of the sigma and the matched hpred *) - val get_sigma_partition : t -> sigma * Sil.hpred - (** Replace the strexp at a given position by a new strexp *) val replace_strexp : bool -> t -> Sil.strexp -> sigma - (** Replace the strexp and the unmatched part of the sigma by the givn inputs *) - val replace_strexp_sigma : bool -> t -> Sil.strexp -> sigma -> sigma - (** Replace the index in the array at a given position with the new index *) val replace_index : bool -> t -> Sil.exp -> Sil.exp -> sigma +(* + (** Get the partition of the sigma: the unmatched part of the sigma and the matched hpred *) + val get_sigma_partition : t -> sigma * Sil.hpred + (** Replace the strexp and the unmatched part of the sigma by the givn inputs *) + val replace_strexp_sigma : bool -> t -> Sil.strexp -> sigma -> sigma +*) end = struct (** syntactic offset *) @@ -194,11 +194,6 @@ end = struct (path', se', t') | _ -> assert false - (** Get the partition of the sigma: the unmatched part of the sigma and the matched hpred *) - let get_sigma_partition (sigma, hpred, _) = - let sigma_unmatched = IList.filter (fun hpred' -> not (hpred' == hpred)) sigma in - (sigma_unmatched, hpred) - (** Replace the current hpred *) let replace_hpred ((sigma, hpred, syn_offs) : t) hpred' = IList.map (fun hpred'' -> if hpred''== hpred then hpred' else hpred'') sigma @@ -231,12 +226,6 @@ end = struct let hpred' = hpred_replace_strexp footprint_part hpred syn_offs update in replace_hpred (sigma, hpred, syn_offs) hpred' - (** Replace the strexp and the unmatched part of the sigma by the given inputs *) - let replace_strexp_sigma footprint_part ((_, hpred, syn_offs) : t) se_in sigma_in = - let new_sigma = hpred :: sigma_in in - let sigma' = replace_strexp footprint_part (new_sigma, hpred, syn_offs) se_in in - IList.sort Sil.hpred_compare sigma' - (** Replace the index in the array at a given position with the new index *) let replace_index footprint_part ((sigma, hpred, syn_offs) : t) (index: Sil.exp) (index': Sil.exp) = let update se' t' = @@ -247,6 +236,18 @@ end = struct | _ -> assert false in let hpred' = hpred_replace_strexp footprint_part hpred syn_offs update in replace_hpred (sigma, hpred, syn_offs) hpred' +(* + (** Get the partition of the sigma: the unmatched part of the sigma and the matched hpred *) + let get_sigma_partition (sigma, hpred, _) = + let sigma_unmatched = IList.filter (fun hpred' -> not (hpred' == hpred)) sigma in + (sigma_unmatched, hpred) + + (** Replace the strexp and the unmatched part of the sigma by the given inputs *) + let replace_strexp_sigma footprint_part ((_, hpred, syn_offs) : t) se_in sigma_in = + let new_sigma = hpred :: sigma_in in + let sigma' = replace_strexp footprint_part (new_sigma, hpred, syn_offs) se_in in + IList.sort Sil.hpred_compare sigma' +*) end (** This function renames expressions in [p]. The renaming is, roughly @@ -287,29 +288,6 @@ let prop_update_sigma_and_fp_sigma else (ep1, false) in (Prop.normalize ep2, changed || changed2) -(** This function uses [update] and transforms the sigma of the - current SH of [p] or that of the footprint of [p], depending on - [footprint_part]. *) -let prop_update_sigma_or_fp_sigma - (footprint_part : bool) - (p : Prop.normal Prop.t) - (update : bool -> sigma -> sigma * bool) : Prop.normal Prop.t * bool - = - let ep1, changed1 = - if footprint_part then (Prop.expose p, false) - else - let sigma', changed = update false (Prop.get_sigma p) in - (Prop.replace_sigma sigma' p, changed) in - let ep2, changed2 = - if not footprint_part then (ep1, false) - else - begin - (if not !Config.footprint then assert false); (* always run in the footprint mode *) - let sigma_fp', changed = update true (Prop.get_sigma_footprint ep1) in - (Prop.replace_sigma_footprint sigma_fp' ep1, changed) - end in - (Prop.normalize ep2, changed1 || changed2) - (** Remember whether array abstraction was performed (to be reset before calling Abs.abstract) *) let array_abstraction_performed = ref false @@ -535,16 +513,6 @@ let report_error prop = Prop.d_prop prop; L.d_ln (); assert false -let check_footprint_pure prop = - let fav_pure = Sil.fav_new () in - Prop.pi_fav_add fav_pure (Prop.get_pure prop @ Prop.get_pi_footprint prop); - let fav_sigma = Sil.fav_new () in - Prop.sigma_fav_add fav_sigma (Prop.get_sigma prop @ Prop.get_sigma_footprint prop); - Sil.fav_filter_ident fav_pure Ident.is_footprint; - Sil.fav_filter_ident fav_sigma Ident.is_footprint; - if not (Sil.fav_subset_ident fav_pure fav_sigma) - then (L.d_strln "footprint vars in pure and not in sigma"; report_error prop) - (** Check performed after the array abstraction to see whether it was successful. Raise assert false in case of failure *) let check_after_array_abstraction prop = let check_index root offs (ind, _) = @@ -632,3 +600,35 @@ let remove_redundant_elements prop = Prop.normalize prop' else prop +(* +(** This function uses [update] and transforms the sigma of the + current SH of [p] or that of the footprint of [p], depending on + [footprint_part]. *) +let prop_update_sigma_or_fp_sigma + (footprint_part : bool) (p : Prop.normal Prop.t) (update : bool -> sigma -> sigma * bool) + : Prop.normal Prop.t * bool = + let ep1, changed1 = + if footprint_part then (Prop.expose p, false) + else + let sigma', changed = update false (Prop.get_sigma p) in + (Prop.replace_sigma sigma' p, changed) in + let ep2, changed2 = + if not footprint_part then (ep1, false) + else + begin + (if not !Config.footprint then assert false); (* always run in the footprint mode *) + let sigma_fp', changed = update true (Prop.get_sigma_footprint ep1) in + (Prop.replace_sigma_footprint sigma_fp' ep1, changed) + end in + (Prop.normalize ep2, changed1 || changed2) + +let check_footprint_pure prop = + let fav_pure = Sil.fav_new () in + Prop.pi_fav_add fav_pure (Prop.get_pure prop @ Prop.get_pi_footprint prop); + let fav_sigma = Sil.fav_new () in + Prop.sigma_fav_add fav_sigma (Prop.get_sigma prop @ Prop.get_sigma_footprint prop); + Sil.fav_filter_ident fav_pure Ident.is_footprint; + Sil.fav_filter_ident fav_sigma Ident.is_footprint; + if not (Sil.fav_subset_ident fav_pure fav_sigma) + then (L.d_strln "footprint vars in pure and not in sigma"; report_error prop) +*) diff --git a/infer/src/backend/autounit.ml b/infer/src/backend/autounit.ml index e8c81afec..4a45e9b3d 100644 --- a/infer/src/backend/autounit.ml +++ b/infer/src/backend/autounit.ml @@ -350,7 +350,7 @@ module Code : sig val empty : unit -> t val pp : F.formatter -> t -> unit val set_indent : string -> unit - val to_list : t -> string list + (* val to_list : t -> string list *) end = struct type t = string list ref let indent = ref "" diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml index 06096443b..2b2f21b0e 100644 --- a/infer/src/backend/cfg.ml +++ b/infer/src/backend/cfg.ml @@ -316,10 +316,6 @@ module Node = struct try Some (pdesc_tbl_find cfg proc_name) with Not_found -> None - (** Set the proc desc of the node *) - let node_set_proc_desc pdesc node = - node.nd_proc <- Some pdesc - let set_temps node temps = node.nd_temps <- temps @@ -390,10 +386,6 @@ module Node = struct IList.filter filter_out_fun nodes in cfg.node_list := remove_node_in_cfg !(cfg.node_list) - let remove_node cfg node = - remove_node' (fun node' -> not (equal node node')) - cfg node - let remove_node_set cfg nodes = remove_node' (fun node' -> not (NodeSet.mem node' nodes)) cfg nodes @@ -606,7 +598,15 @@ module Node = struct let fold_node acc node = IList.fold_left (fun acc instr -> f acc node instr) acc (get_instrs node) in proc_desc_fold_nodes fold_node acc proc_desc +(* + (** Set the proc desc of the node *) + let node_set_proc_desc pdesc node = + node.nd_proc <- Some pdesc + let remove_node cfg node = + remove_node' (fun node' -> not (equal node node')) + cfg node +*) end (* =============== END of module Node =============== *) diff --git a/infer/src/backend/cfg.mli b/infer/src/backend/cfg.mli index 24d7437d5..5532732ff 100644 --- a/infer/src/backend/cfg.mli +++ b/infer/src/backend/cfg.mli @@ -147,9 +147,6 @@ module Node : sig (** Add the instructions and temporaries at the beginning of the list of instructions to execute *) val prepend_instrs_temps : t -> Sil.instr list -> Ident.t list -> unit - (** Replace the instructions to be executed. *) - val replace_instrs : t -> Sil.instr list -> unit - (** Add declarations for local variables and return variable to the node *) val add_locals_ret_declaration : t -> (Mangled.t * Sil.typ) list -> unit @@ -259,6 +256,10 @@ module Node : sig (** Set the temporary variables *) val set_temps : t -> Ident.t list -> unit +(* + (** Replace the instructions to be executed. *) + val replace_instrs : t -> Sil.instr list -> unit +*) end (** Hash table with nodes as keys. *) diff --git a/infer/src/backend/cg.ml b/infer/src/backend/cg.ml index a33dd374f..50d21d74b 100644 --- a/infer/src/backend/cg.ml +++ b/infer/src/backend/cg.ml @@ -13,10 +13,6 @@ module L = Logging module F = Format -let pp_nodeset fmt set = - let f node = F.fprintf fmt "%a@ " Procname.pp node in - Procname.Set.iter f set - type node = Procname.t type in_out_calls = @@ -189,10 +185,6 @@ let get_nodes (g: t) = node_map_iter f g; !nodes -let map_option f l = - let lo = IList.filter (function | Some _ -> true | None -> false) (IList.map f l) in - IList.map (function Some p -> p | None -> assert false) lo - let compute_calls g node = { in_calls = Procname.Set.cardinal (get_ancestors g node); out_calls = Procname.Set.cardinal (get_heirs g node) } @@ -236,10 +228,6 @@ let get_defined_children (g: t) n = let get_parents (g: t) n = (Procname.Hash.find g.node_map n).parents -(** Return true if [n] is recursive *) -let is_recursive (g: t) n = - Procname.Set.mem n (get_ancestors g n) - (** [call_recursively source dest] returns [true] if function [source] recursively calls function [dest] *) let calls_recursively (g: t) source dest = Procname.Set.mem source (get_ancestors g dest) @@ -379,3 +367,17 @@ let save_call_graph_dotty fname_opt get_specs (g: t) = let fmt = F.formatter_of_out_channel outc in pp_graph_dotty get_specs g fmt; close_out outc + +(* +let pp_nodeset fmt set = + let f node = F.fprintf fmt "%a@ " Procname.pp node in + Procname.Set.iter f set + +let map_option f l = + let lo = IList.filter (function | Some _ -> true | None -> false) (IList.map f l) in + IList.map (function Some p -> p | None -> assert false) lo + +(** Return true if [n] is recursive *) +let is_recursive (g: t) n = + Procname.Set.mem n (get_ancestors g n) +*) diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index c7d64fe6f..82c2d54ff 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -89,11 +89,6 @@ module EPset = Set.Make | _ -> Sil.exp_compare e1' e2' end) -let epset_add e e' set = - match (Sil.exp_compare e e') with - | i when i <= 0 -> EPset.add (e, e') set - | _ -> EPset.add (e', e) set - (** {2 Module for maintaining information about noninjectivity during join} *) module NonInj : sig @@ -456,9 +451,11 @@ module FreshVarExp : sig val init : unit -> unit val get_fresh_exp : Sil.exp -> Sil.exp -> Sil.exp val get_induced_pi : unit -> Prop.pi - val lookup : side -> Sil.exp -> (Sil.exp * Sil.exp) option val final : unit -> unit +(* + val lookup : side -> Sil.exp -> (Sil.exp * Sil.exp) option +*) end = struct let t = ref [] @@ -479,13 +476,6 @@ end = struct t := (e1, e2, e)::!t; e - let lookup side e = - try - let (e1, e2, e) = IList.find (fun (e1', e2', _) -> Sil.exp_equal e (select side e1' e2')) !t in - Some (e, select (opposite side) e1 e2) - with Not_found -> - None - let get_induced_atom acc strict_lower upper e = let ineq_lower = Prop.mk_inequality (Sil.BinOp(Sil.Lt, strict_lower, e)) in let ineq_upper = Prop.mk_inequality (Sil.BinOp(Sil.Le, e, upper)) in @@ -532,6 +522,15 @@ end = struct | _ -> acc in IList.fold_left f_ineqs eqs t_minimal +(* + let lookup side e = + try + let (e1, e2, e) = + IList.find (fun (e1', e2', _) -> Sil.exp_equal e (select side e1' e2')) !t in + Some (e, select (opposite side) e1 e2) + with Not_found -> + None +*) end (** {2 Modules for renaming} *) @@ -547,7 +546,6 @@ module Rename : sig val extend : Sil.exp -> Sil.exp -> data_opt -> Sil.exp val check : (side -> Sil.exp -> Sil.exp list -> bool) -> bool - val get : Sil.exp -> Sil.exp -> Sil.exp option val get_others : side -> Sil.exp -> (Sil.exp * Sil.exp) option val get_other_atoms : side -> Sil.atom -> (Sil.atom * Sil.atom) option @@ -557,14 +555,15 @@ module Rename : sig val to_subst_proj : side -> Sil.fav -> Sil.subst val to_subst_emb : side -> Sil.subst +(* + val get : Sil.exp -> Sil.exp -> Sil.exp option val pp : printenv -> Format.formatter -> (Sil.exp * Sil.exp * Sil.exp) list -> unit - +*) end = struct type t = (Sil.exp * Sil.exp * Sil.exp) list let tbl : t ref = ref [] - let empty = [] let init () = tbl := [] let final () = tbl := [] @@ -678,12 +677,6 @@ end = struct if find_duplicates sub_list_sorted then (L.d_strln "failure reason 12"; raise IList.Fail) else Sil.sub_of_list sub_list_sorted - let get e1 e2 = - let f (e1', e2', _) = Sil.exp_equal e1 e1' && Sil.exp_equal e2 e2' in - match (IList.filter f !tbl) with - | [] -> None - | (_, _, e):: _ -> Some e - let get_others' f_lookup side e = let side_op = opposite side in let r = f_lookup side e in @@ -786,12 +779,18 @@ end = struct push entry; Todo.push entry; e +(* + let get e1 e2 = + let f (e1', e2', _) = Sil.exp_equal e1 e1' && Sil.exp_equal e2 e2' in + match (IList.filter f !tbl) with + | [] -> None + | (_, _, e):: _ -> Some e let pp pe f renaming = let pp_triple f (e1, e2, e3) = F.fprintf f "(%a,%a,%a)" (Sil.pp_exp pe) e3 (Sil.pp_exp pe) e1 (Sil.pp_exp pe) e2 in (pp_seq pp_triple) f renaming - +*) end (** {2 Functions for constructing fresh sil data types} *) @@ -1045,28 +1044,6 @@ let exp_list_partial_join = IList.map2 exp_partial_join let exp_list_partial_meet = IList.map2 exp_partial_meet -let run_without_absval f e1 e2 = - let old_abs_val = !Config.abs_val in - let new_abs_val = if old_abs_val = 0 then 0 else 1 in - try - begin - Config.abs_val := new_abs_val; - let e = f e1 e2 in - Config.abs_val := old_abs_val; - e - end - with exn -> - begin - Config.abs_val := old_abs_val; - raise exn - end - -let exp_partial_join_without_absval e1 e2 = - run_without_absval exp_partial_join e1 e2 - -let exp_partial_meet_without_absval e1 e2 = - run_without_absval exp_partial_meet e1 e2 - (** {2 Join and Meet for Strexp} *) @@ -2046,3 +2023,32 @@ let propset_meet_generate_pre pset = let plist_old = Propset.to_proplist pset in let plist_new = Propset.to_proplist pset_new in plist_new @ plist_old + +(* +let epset_add e e' set = + match (Sil.exp_compare e e') with + | i when i <= 0 -> EPset.add (e, e') set + | _ -> EPset.add (e', e) set + +let run_without_absval f e1 e2 = + let old_abs_val = !Config.abs_val in + let new_abs_val = if old_abs_val = 0 then 0 else 1 in + try + begin + Config.abs_val := new_abs_val; + let e = f e1 e2 in + Config.abs_val := old_abs_val; + e + end + with exn -> + begin + Config.abs_val := old_abs_val; + raise exn + end + +let exp_partial_join_without_absval e1 e2 = + run_without_absval exp_partial_join e1 e2 + +let exp_partial_meet_without_absval e1 e2 = + run_without_absval exp_partial_meet e1 e2 +*) diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index fd44913bb..77a8b0045 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -101,9 +101,6 @@ let invisible_arrows = ref false let print_stack_info = ref false -let exp_is_neq_zero e = - IList.exists (fun e' -> Sil.exp_equal e e') !exps_neq_zero - (* replace a dollar sign in a name with a D. We need this because dotty get confused if there is*) (* a dollar sign i a label*) let strip_special_chars s = @@ -170,19 +167,6 @@ and get_contents pe coo f = function | idx_se:: l -> F.fprintf f "%a | %a" (get_contents_single pe coo) idx_se (get_contents pe coo) l -and get_contents_range_single pe coo f range_se = - let (e1, e2), se = range_se in - let e1_no_special_char = strip_special_chars (Sil.exp_to_string e1) in - F.fprintf f "{ <%s> [%a,%a] : %a }" - e1_no_special_char (Sil.pp_exp pe) e1 (Sil.pp_exp pe) e2 (get_contents_sexp pe coo) se - -and get_contents_range pe coo f = function - | [] -> () - | [range_se] -> - F.fprintf f "%a" (get_contents_range_single pe coo) range_se - | range_se:: l -> - F.fprintf f "%a | %a" (get_contents_range_single pe coo) range_se (get_contents_range pe coo) l - (* true if node is the sorce node of the expression e*) let is_source_node_of_exp e node = match node with @@ -236,30 +220,10 @@ let look_up dotnodes e lambda = let r'= IList.map get_coordinate_id r in r' @ look_up_for_back_pointer e dotnodes lambda -let pp_nesting fmt nesting = - if nesting > 1 then F.fprintf fmt "%d" nesting - let reset_proposition_counter () = proposition_counter:= 0 let reset_dotty_spec_counter () = spec_counter:= 0 -let max_map f l = - let curr_max = ref 0 in - IList.iter (fun x -> curr_max := max !curr_max (f x)) l; - ! curr_max - -let rec sigma_nesting_level sigma = - max_map (function - | Sil.Hpointsto _ -> 0 - | Sil.Hlseg (_, hpara, _, _, _) -> hpara_nesting_level hpara - | Sil.Hdllseg (_, hpara_dll, _, _, _, _, _) -> hpara_dll_nesting_level hpara_dll) sigma - -and hpara_nesting_level hpara = - 1 + sigma_nesting_level hpara.Sil.body - -and hpara_dll_nesting_level hpara_dll = - 1 + sigma_nesting_level hpara_dll.Sil.body_dll - let color_to_str c = match c with | Black -> "black" @@ -374,17 +338,6 @@ let box_dangling e = | Dotdangling(coo, _, _):: _ -> Some coo.id | _ -> None (* NOTE: this cannot be possible since entry_e can be composed only by Dotdangling, see def of entry_e*) -let rec get_color_exp dot_nodes e = - match dot_nodes with - | [] ->"" - | Dotnil(_):: l' -> get_color_exp l' e - | Dotpointsto(_, e', c):: l' - | Dotdangling(_, e', c):: l' - | Dotarray(_, _, e', _, _, c):: l' - | Dotlseg(_, e', _, _, _, c):: l' - | Dotstruct(_, e', _, c, _):: l' - | Dotdllseg(_, e', _, _, _, _, _, c):: l' -> if (Sil.exp_equal e e') then c else get_color_exp l' e - (* construct a Dotnil and returns it's id *) let make_nil_node lambda = let n = !dotty_state_count in @@ -1427,3 +1380,54 @@ let print_specs_xml signature specs loc fmt = ("line", string_of_int loc.Location.line)] [xml_signature; xml_specifications] in Io_infer.Xml.pp_document true fmt proc_summary + +(* +let exp_is_neq_zero e = + IList.exists (fun e' -> Sil.exp_equal e e') !exps_neq_zero + +let rec get_contents_range_single pe coo f range_se = + let (e1, e2), se = range_se in + let e1_no_special_char = strip_special_chars (Sil.exp_to_string e1) in + F.fprintf f "{ <%s> [%a,%a] : %a }" + e1_no_special_char (Sil.pp_exp pe) e1 (Sil.pp_exp pe) e2 (get_contents_sexp pe coo) se + +and get_contents_range pe coo f = function + | [] -> () + | [range_se] -> + F.fprintf f "%a" (get_contents_range_single pe coo) range_se + | range_se:: l -> + F.fprintf f "%a | %a" + (get_contents_range_single pe coo) range_se (get_contents_range pe coo) l + +let pp_nesting fmt nesting = + if nesting > 1 then F.fprintf fmt "%d" nesting + +let max_map f l = + let curr_max = ref 0 in + IList.iter (fun x -> curr_max := max !curr_max (f x)) l; + ! curr_max + +let rec sigma_nesting_level sigma = + max_map (function + | Sil.Hpointsto _ -> 0 + | Sil.Hlseg (_, hpara, _, _, _) -> hpara_nesting_level hpara + | Sil.Hdllseg (_, hpara_dll, _, _, _, _, _) -> hpara_dll_nesting_level hpara_dll) sigma + +and hpara_nesting_level hpara = + 1 + sigma_nesting_level hpara.Sil.body + +and hpara_dll_nesting_level hpara_dll = + 1 + sigma_nesting_level hpara_dll.Sil.body_dll + +let rec get_color_exp dot_nodes e = + match dot_nodes with + | [] ->"" + | Dotnil(_):: l' -> get_color_exp l' e + | Dotpointsto(_, e', c):: l' + | Dotdangling(_, e', c):: l' + | Dotarray(_, _, e', _, _, c):: l' + | Dotlseg(_, e', _, _, _, c):: l' + | Dotstruct(_, e', _, c, _):: l' + | Dotdllseg(_, e', _, _, _, _, _, c):: l' -> + if (Sil.exp_equal e e') then c else get_color_exp l' e +*) diff --git a/infer/src/backend/exceptions.ml b/infer/src/backend/exceptions.ml index 20300c5ce..67c9251e0 100644 --- a/infer/src/backend/exceptions.ml +++ b/infer/src/backend/exceptions.ml @@ -82,9 +82,6 @@ exception Use_after_free of Localise.error_desc * ml_loc exception Wrong_argument_number of ml_loc -let file_line_column_string (file, line, column) = - Printf.sprintf "file %s line %d column %d" file line column - (** Turn an exception into a descriptive string, error description, location in ml source, and category *) let recognize_exception exn = let filter_out_bucket desc = diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml index 7d0b18fb2..461ff3bc8 100644 --- a/infer/src/backend/exe_env.ml +++ b/infer/src/backend/exe_env.ml @@ -155,22 +155,6 @@ let file_data_to_tenv file_data = assert false | Some tenv -> tenv -(** return the procs enabled: active and not shadowed, plus the procs they call directly *) -let procs_enabled exe_env source = - let is_not_shadowed proc_name = (* not shadowed by a definition in another file *) - DB.source_file_equal (get_source exe_env proc_name) source in - match exe_env.active_opt with - | Some pset -> - let res = ref Procname.Set.empty in - let do_pname proc_name = (* add any proc which is not shadowed, and all the procs it calls *) - if is_not_shadowed proc_name then - let pset' = Cg.get_all_children exe_env.cg proc_name in - let pset'' = Procname.Set.add proc_name pset' in - res := Procname.Set.union pset'' !res in - Procname.Set.iter do_pname pset; - Some !res - | None -> None - let file_data_to_cfg exe_env file_data = match file_data.cfg with | None -> @@ -209,3 +193,22 @@ let iter_files f exe_env = DB.SourceFileSet.add fname seen_files_acc end in ignore (Procname.Hash.fold do_file exe_env.proc_map DB.SourceFileSet.empty) + +(* +(** return the procs enabled: active and not shadowed, plus the procs they call directly *) +let procs_enabled exe_env source = + let is_not_shadowed proc_name = (* not shadowed by a definition in another file *) + DB.source_file_equal (get_source exe_env proc_name) source in + match exe_env.active_opt with + | Some pset -> + let res = ref Procname.Set.empty in + (* add any proc which is not shadowed, and all the procs it calls *) + let do_pname proc_name = + if is_not_shadowed proc_name then + let pset' = Cg.get_all_children exe_env.cg proc_name in + let pset'' = Procname.Set.add proc_name pset' in + res := Procname.Set.union pset'' !res in + Procname.Set.iter do_pname pset; + Some !res + | None -> None +*) diff --git a/infer/src/backend/ident.ml b/infer/src/backend/ident.ml index fe7c6bd00..bbd9f24f3 100644 --- a/infer/src/backend/ident.ml +++ b/infer/src/backend/ident.ml @@ -294,10 +294,6 @@ let path_ident_stamp = - 3 let is_path (id: t) = id.kind == knormal && id.stamp = path_ident_stamp -let make_ident_primed id = - if id.kind == kprimed then assert false - else { id with kind = kprimed } - let make_unprimed id = if id.kind <> kprimed then assert false else { id with kind = knormal } @@ -359,3 +355,9 @@ let pp_list pe = pp_comma_seq (pp pe) (** pretty printer for lists of names *) let pp_name_list = pp_comma_seq pp_name + +(* +let make_ident_primed id = + if id.kind == kprimed then assert false + else { id with kind = kprimed } +*) diff --git a/infer/src/backend/inferconfig.ml b/infer/src/backend/inferconfig.ml index 4bcc8691b..f39074d97 100644 --- a/infer/src/backend/inferconfig.ml +++ b/infer/src/backend/inferconfig.ml @@ -128,32 +128,6 @@ struct | "Java" -> Config.Java | l -> failwith ("Inferconfig JSON key " ^ M.json_key ^ " not supported for language " ^ l) - let pp_pattern fmt pattern = - let pp_string fmt s = - Format.fprintf fmt "%s" s in - let pp_option pp_value fmt = function - | None -> pp_string fmt "None" - | Some value -> Format.fprintf fmt "%a" pp_value value in - let pp_key_value pp_value fmt (key, value) = - Format.fprintf fmt " %s: %a,\n" key (pp_option pp_value) value in - let pp_method_pattern fmt mp = - let pp_params fmt l = - Format.fprintf fmt "[%a]" - (pp_semicolon_seq_oneline pe_text pp_string) l in - Format.fprintf fmt "%a%a%a" - (pp_key_value pp_string) ("class", Some mp.class_name) - (pp_key_value pp_string) ("method", mp.method_name) - (pp_key_value pp_params) ("parameters", mp.parameters) - and pp_source_contains fmt sc = - Format.fprintf fmt " pattern: %s\n" sc in - match pattern with - | Method_pattern (language, mp) -> - Format.fprintf fmt "Method pattern (%s) {\n%a}\n" - (Config.string_of_language language) pp_method_pattern mp - | Source_contains (language, sc) -> - Format.fprintf fmt "Source contains (%s) {\n%a}\n" - (Config.string_of_language language) pp_source_contains sc - let detect_language assoc = let rec loop = function | [] -> @@ -267,6 +241,33 @@ struct default_matcher else default_matcher +(* + let pp_pattern fmt pattern = + let pp_string fmt s = + Format.fprintf fmt "%s" s in + let pp_option pp_value fmt = function + | None -> pp_string fmt "None" + | Some value -> Format.fprintf fmt "%a" pp_value value in + let pp_key_value pp_value fmt (key, value) = + Format.fprintf fmt " %s: %a,\n" key (pp_option pp_value) value in + let pp_method_pattern fmt mp = + let pp_params fmt l = + Format.fprintf fmt "[%a]" + (pp_semicolon_seq_oneline pe_text pp_string) l in + Format.fprintf fmt "%a%a%a" + (pp_key_value pp_string) ("class", Some mp.class_name) + (pp_key_value pp_string) ("method", mp.method_name) + (pp_key_value pp_params) ("parameters", mp.parameters) + and pp_source_contains fmt sc = + Format.fprintf fmt " pattern: %s\n" sc in + match pattern with + | Method_pattern (language, mp) -> + Format.fprintf fmt "Method pattern (%s) {\n%a}\n" + (Config.string_of_language language) pp_method_pattern mp + | Source_contains (language, sc) -> + Format.fprintf fmt "Source contains (%s) {\n%a}\n" + (Config.string_of_language language) pp_source_contains sc +*) end (* of module FileOrProcMatcher *) diff --git a/infer/src/backend/mleak_buckets.ml b/infer/src/backend/mleak_buckets.ml index 633fe4b12..2a6f7ed16 100644 --- a/infer/src/backend/mleak_buckets.ml +++ b/infer/src/backend/mleak_buckets.ml @@ -32,14 +32,6 @@ let bucket_from_string bucket_s = | "unknown_origin" -> MLeak_unknown | _ -> assert false -let bucket_to_string bucket = - match bucket with - | MLeak_cf -> "Core Foundation" - | MLeak_arc -> "Arc" - | MLeak_no_arc -> "No arc" - | MLeak_cpp -> "Cpp" - | MLeak_unknown -> "Unknown origin" - let bucket_to_message bucket = match bucket with | MLeak_cf -> "[CF]" @@ -130,3 +122,13 @@ let should_raise_objc_leak typ = else if should_raise_leak_arc () then Some (bucket_to_message MLeak_arc) else if should_raise_leak_no_arc () then Some (bucket_to_message MLeak_no_arc) else None + +(* +let bucket_to_string bucket = + match bucket with + | MLeak_cf -> "Core Foundation" + | MLeak_arc -> "Arc" + | MLeak_no_arc -> "No arc" + | MLeak_cpp -> "Cpp" + | MLeak_unknown -> "Unknown origin" +*) diff --git a/infer/src/backend/objc_models.ml b/infer/src/backend/objc_models.ml index 68dda6191..d8fbf0987 100644 --- a/infer/src/backend/objc_models.ml +++ b/infer/src/backend/objc_models.ml @@ -230,10 +230,6 @@ struct let function_arg_is_cftype typ = (string_contains cf_type typ) - let function_arg_is_core_pgraphics typ = - let res = (string_contains cf_type typ) in - res - let is_core_lib_retain typ funct = function_arg_is_cftype typ && funct = cf_retain @@ -247,6 +243,11 @@ struct (string_contains (cg_typ^ref) typ) with Not_found -> false +(* + let function_arg_is_core_pgraphics typ = + let res = (string_contains cf_type typ) in + res +*) end let is_core_lib_type typ = diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index ba24f445f..56d1de991 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -42,17 +42,12 @@ module Path : sig (** dump statistics of the path *) val d_stats : t -> unit - (** equality for paths *) - val equal : t -> t -> bool - (** extend a path with a new node reached from the given session, with an optional string for exceptions *) val extend : Cfg.node -> Typename.t option -> session -> t -> t (** extend a path with a new node reached from the given session, with an optional string for exceptions *) val add_description : t -> string -> t - val get_description : t -> string option - (** iterate over each node in the path, excluding calls, once *) val iter_all_nodes_nocalls : (Cfg.node -> unit) -> t -> unit @@ -73,6 +68,13 @@ module Path : sig (** create a new path with given start node *) val start : Cfg.node -> t + +(* + (** equality for paths *) + val equal : t -> t -> bool + + val get_description : t -> string option +*) end = struct type session = int type stats = @@ -151,9 +153,6 @@ end = struct let n = compare p1 p2 in if n <> 0 then n else compare sub1 sub2 - let equal p1 p2 = - compare p1 p2 = 0 - let start node = Pstart (node, get_dummy_stats ()) let extend (node: Cfg.node) exn_opt session path = @@ -508,6 +507,10 @@ end = struct IList.remove_irrelevant_duplicates compare relevant (IList.rev !trace) (* IList.remove_duplicates compare (IList.sort compare !trace) *) +(* + let equal p1 p2 = + compare p1 p2 = 0 +*) end (* =============== END of the Path module ===============*) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index e24ccdeb6..80aad67c9 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -90,9 +90,6 @@ let rec use_exp cfg pdesc (exp: Sil.exp) acc = and use_etl cfg pdesc (etl: (Sil.exp * Sil.typ) list) acc = IList.fold_left (fun acc (e, _) -> use_exp cfg pdesc e acc) acc etl -and use_instrl cfg tenv (pdesc: Cfg.Procdesc.t) (il : Sil.instr list) acc = - IList.fold_left (fun acc instr -> use_instr cfg tenv pdesc instr acc) acc il - and use_instr cfg tenv (pdesc: Cfg.Procdesc.t) (instr: Sil.instr) acc = match instr with | Sil.Set (_, _, e, _) @@ -124,7 +121,7 @@ and def_instrl cfg instrs acc = (* computes the addresses that are assigned to something or passed as parameters to*) (* a functions. These will be considered becoming possibly aliased *) -let rec aliasing_instr cfg pdesc (instr: Sil.instr) acc = +let aliasing_instr cfg pdesc (instr: Sil.instr) acc = match instr with | Sil.Set (_, _, e, _) -> use_exp cfg pdesc e acc | Sil.Call (_, _, argl, _, _) -> @@ -135,9 +132,6 @@ let rec aliasing_instr cfg pdesc (instr: Sil.instr) acc = | Sil.Abstract _ | Sil.Remove_temps _ | Sil.Stackop _ | Sil.Declare_locals _ -> acc | Sil.Goto_node _ -> acc -and aliasing_instrl cfg pdesc (il : Sil.instr list) acc = - IList.fold_left (fun acc instr -> aliasing_instr cfg pdesc instr acc) acc il - (* computes possible alisased var *) let def_aliased_var cfg pdesc instrs acc = IList.fold_left (fun acc' i -> aliasing_instr cfg pdesc i acc') acc instrs @@ -163,7 +157,6 @@ module Worklist = struct let reset _ = worklist := S.empty let add node = worklist := S.add node !worklist - let add_list = IList.iter add let pick () = let min = S.min_elt !worklist in worklist := S.remove min !worklist; @@ -174,9 +167,9 @@ end module Table: sig val reset: unit -> unit val get_live: Cfg.node -> Vset.t (** variables live after the last instruction in the current node *) - val replace: Cfg.node -> Vset.t -> unit val propagate_to_preds: Vset.t -> Cfg.node list -> unit (** propagate live variables to predecessor nodes *) val iter: Vset.t -> (Cfg.node -> Vset.t -> Vset.t -> unit) -> unit + (* val replace: Cfg.node -> Vset.t -> unit *) end = struct module H = Cfg.NodeHash let table = H.create 1024 @@ -254,18 +247,6 @@ let analyze_proc cfg tenv pdesc cand = done with Not_found -> () -(* Printing function useful for debugging *) -let print_aliased_var s al_var = - L.out s; - Vset.iter (fun v -> L.out " %a, " (Sil.pp_pvar pe_text) v) al_var; - L.out "@." - -(* Printing function useful for debugging *) -let print_aliased_var_l s al_var = - L.out s; - IList.iter (fun v -> L.out " %a, " (Sil.pp_pvar pe_text) v) al_var; - L.out "@." - (* Instruction i is nullifying a block variable *) let is_block_nullify i = match i with @@ -444,3 +425,16 @@ let doit ?(f_translate_typ=None) cfg cg tenv = if !Config.curr_language = Config.Java then add_dispatch_calls cfg cg tenv f_translate_typ; +(* +Printing function useful for debugging +let print_aliased_var s al_var = + L.out s; + Vset.iter (fun v -> L.out " %a, " (Sil.pp_pvar pe_text) v) al_var; + L.out "@." + +Printing function useful for debugging +let print_aliased_var_l s al_var = + L.out s; + IList.iter (fun v -> L.out " %a, " (Sil.pp_pvar pe_text) v) al_var; + L.out "@." +*) diff --git a/infer/src/backend/procname.ml b/infer/src/backend/procname.ml index 06e7092cc..00cca66a5 100644 --- a/infer/src/backend/procname.ml +++ b/infer/src/backend/procname.ml @@ -216,10 +216,6 @@ let java_get_class = function | Java_method j -> java_type_to_string j.class_name | _ -> assert false -(** Return path components of a java class name *) -let java_get_class_components proc_name = - Str.split (Str.regexp (Str.quote ".")) (java_get_class proc_name) - (** Return the class name of a java procedure name. *) let java_get_simple_class = function | Java_method j -> snd j.class_name @@ -495,3 +491,9 @@ module Set = Set.Make(struct (** Pretty print a set of proc names *) let pp_set fmt set = Set.iter (fun pname -> F.fprintf fmt "%a " pp pname) set + +(* +(** Return path components of a java class name *) +let java_get_class_components proc_name = + Str.split (Str.regexp (Str.quote ".")) (java_get_class proc_name) +*) diff --git a/infer/src/backend/procname.mli b/infer/src/backend/procname.mli index b37b40895..8c5f2c176 100644 --- a/infer/src/backend/procname.mli +++ b/infer/src/backend/procname.mli @@ -61,9 +61,6 @@ val is_c_method : t -> bool (** Replace package and classname of a java procname. *) val java_replace_class : t -> string -> t -(** Replace the method of a java procname. *) -val java_replace_method : t -> string -> t - (** Replace the parameters of a java procname. *) val java_replace_parameters : t -> java_type list -> t @@ -176,3 +173,8 @@ module Set : Set.S with type elt = t (** Pretty print a set of proc names *) val pp_set : Format.formatter -> Set.t -> unit + +(* +(** Replace the method of a java procname. *) +val java_replace_method : t -> string -> t +*) diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 992540ed0..9c0bd8f26 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -20,8 +20,6 @@ type struct_init_mode = | No_init | Fld_init -let cil_exp_compare (e1: Sil.exp) (e2: Sil.exp) = Pervasives.compare e1 e2 - let unSome = function | Some x -> x | _ -> assert false @@ -107,10 +105,6 @@ let pp_footprint _pe f fp = if fp.foot_pi != [] || fp.foot_sigma != [] then F.fprintf f "@\n[footprint@\n @[%a%a@] ]" pp_pi () (pp_semicolon_seq pe (Sil.pp_hpred pe)) fp.foot_sigma -let pp_lseg_kind f = function - | Sil.Lseg_NE -> F.fprintf f "ne" - | Sil.Lseg_PE -> F.fprintf f "" - let pp_texp_simple pe = match pe.pe_opt with | PP_SIM_DEFAULT -> Sil.pp_texp pe | PP_SIM_WITH_TYP -> Sil.pp_texp_full pe @@ -398,24 +392,6 @@ let prop_fpv prop = (sigma_fpv prop.foot_sigma) @ (sigma_fpv prop.sigma) -(** {1 Functions for computing free or bound non-program variables} *) - -let pi_av_add fav pi = - IList.iter (Sil.atom_av_add fav) pi - -let sigma_av_add fav sigma = - IList.iter (Sil.hpred_av_add fav) sigma - -let prop_av_add fav prop = - Sil.sub_av_add fav prop.sub; - pi_av_add fav prop.pi; - sigma_av_add fav prop.sigma; - pi_av_add fav prop.foot_pi; - sigma_av_add fav prop.foot_sigma - -let prop_av = - Sil.fav_imperative_to_functional prop_av_add - (** {2 Functions for Subsitition} *) let pi_sub (subst: Sil.subst) pi = @@ -1070,14 +1046,6 @@ let atom_negate = function | Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2) | Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2) -let rec remove_duplicates_from_sorted special_equal = function - | [] -> [] - | [x] -> [x] - | x:: y:: l -> - if (special_equal x y) - then remove_duplicates_from_sorted special_equal (y:: l) - else x:: (remove_duplicates_from_sorted special_equal (y:: l)) - let rec strexp_normalize sub se = match se with | Sil.Eexp (e, inst) -> @@ -1443,12 +1411,6 @@ let replace_pi pi eprop = let replace_sigma sigma eprop = { eprop with sigma = sigma } -exception No_Footprint - -let unSome_footprint = function - | None -> raise No_Footprint - | Some fp -> fp - let replace_sigma_footprint sigma (prop : 'a t) : exposed t = { prop with foot_sigma = sigma } @@ -1472,11 +1434,6 @@ let prop_is_emp p = match p.sigma with (** {2 Functions for changing and generating propositions} *) -(** Replace the sub part of [prop]. *) -let prop_replace_sub sub p = - let nsub = sub_normalize sub in - { p with sub = nsub } - (** Sil.Construct a disequality. *) let mk_neq e1 e2 = run_with_abs_val_eq_zero @@ -1493,10 +1450,6 @@ let mk_eq e1 e2 = let ne2 = exp_normalize Sil.sub_empty e2 in atom_normalize Sil.sub_empty (Sil.Aeq (ne1, ne2))) -let unstructured_type = function - | Sil.Tstruct _ | Sil.Tarray _ -> false - | _ -> true - (** Construct a points-to predicate for a single program variable. If [expand_structs] is true, initialize the fields of structs with fresh variables. *) let mk_ptsto_lvar tenv expand_structs inst ((pvar: Sil.pvar), texp, expo) : Sil.hpred = @@ -2226,11 +2179,6 @@ let prop_rename_array_indices prop = apply_reindexing subst prop end -let rec pp_ren pe f = function - | [] -> () - | [(i, x)] -> F.fprintf f "%a->%a" (Ident.pp pe) i (Ident.pp pe) x - | (i, x):: ren -> F.fprintf f "%a->%a, %a" (Ident.pp pe) i (Ident.pp pe) x (pp_ren pe) ren - let compute_renaming fav = let ids = Sil.fav_to_list fav in let ids_primed, ids_nonprimed = IList.partition Ident.is_primed ids in @@ -2406,11 +2354,6 @@ let prop_rename_primed_footprint_vars p = let mem_idlist i l = IList.exists (fun id -> Ident.equal i id) l -let id_exp_compare (id1, e1) (id2, e2) = - let n = Sil.exp_compare e1 e2 in - if n <> 0 then n - else Ident.compare id1 id2 - let expose (p : normal t) : exposed t = Obj.magic p (** normalize a prop *) @@ -2771,11 +2714,6 @@ let prop_case_split prop = (IList.fold_left prop_atom_and prop' pi):: props_acc in IList.fold_left f [] pi_sigma_list -(** Raise an exception if the prop is not normalized *) -let check_prop_normalized prop = - let sigma' = sigma_normalize_prop prop prop.sigma in - if sigma_equal prop.sigma sigma' == false then assert false - let prop_expand prop = (* let _ = check_prop_normalized prop in @@ -2885,7 +2823,21 @@ end = struct let pi_size pi = pi_weight * IList.length pi + (** Compute a size value for the prop, which indicates its + complexity *) + let prop_size p = + let size_current = sigma_size p.sigma in + let size_footprint = sigma_size p.foot_sigma in + max size_current size_footprint + (** Approximate the size of the longest chain by counting the max + number of |-> with the same type and whose lhs is primed or + footprint *) + let prop_chain_size p = + let fp_size = pi_size p.foot_pi + sigma_size p.foot_sigma in + pi_size p.pi + sigma_size p.sigma + fp_size + +(* (** Approximate the size of the longest chain by counting the max number of |-> with the same type and whose lhs is primed or footprint *) @@ -2908,20 +2860,7 @@ end = struct let size = ref 0 in Sil.ExpMap.iter (fun t n -> size := max n !size) !tbl; !size - - (** Compute a size value for the prop, which indicates its - complexity *) - let prop_size p = - let size_current = sigma_size p.sigma in - let size_footprint = sigma_size p.foot_sigma in - max size_current size_footprint - - (** Approximate the size of the longest chain by counting the max - number of |-> with the same type and whose lhs is primed or - footprint *) - let prop_chain_size p = - let fp_size = pi_size p.foot_pi + sigma_size p.foot_sigma in - pi_size p.pi + sigma_size p.sigma + fp_size +*) end (*** END of module Metrics ***) @@ -2976,3 +2915,57 @@ module CategorizePreconditions = struct | _:: _, [], [] -> DataConstraints end + +(* +let pp_lseg_kind f = function + | Sil.Lseg_NE -> F.fprintf f "ne" + | Sil.Lseg_PE -> F.fprintf f "" + +let pi_av_add fav pi = + IList.iter (Sil.atom_av_add fav) pi + +let sigma_av_add fav sigma = + IList.iter (Sil.hpred_av_add fav) sigma + +let prop_av_add fav prop = + Sil.sub_av_add fav prop.sub; + pi_av_add fav prop.pi; + sigma_av_add fav prop.sigma; + pi_av_add fav prop.foot_pi; + sigma_av_add fav prop.foot_sigma + +let prop_av = + Sil.fav_imperative_to_functional prop_av_add + +let rec remove_duplicates_from_sorted special_equal = function + | [] -> [] + | [x] -> [x] + | x:: y:: l -> + if (special_equal x y) + then remove_duplicates_from_sorted special_equal (y:: l) + else x:: (remove_duplicates_from_sorted special_equal (y:: l)) + +(** Replace the sub part of [prop]. *) +let prop_replace_sub sub p = + let nsub = sub_normalize sub in + { p with sub = nsub } + +let unstructured_type = function + | Sil.Tstruct _ | Sil.Tarray _ -> false + | _ -> true + +let rec pp_ren pe f = function + | [] -> () + | [(i, x)] -> F.fprintf f "%a->%a" (Ident.pp pe) i (Ident.pp pe) x + | (i, x):: ren -> F.fprintf f "%a->%a, %a" (Ident.pp pe) i (Ident.pp pe) x (pp_ren pe) ren + +let id_exp_compare (id1, e1) (id2, e2) = + let n = Sil.exp_compare e1 e2 in + if n <> 0 then n + else Ident.compare id1 id2 + +(** Raise an exception if the prop is not normalized *) +let check_prop_normalized prop = + let sigma' = sigma_normalize_prop prop prop.sigma in + if sigma_equal prop.sigma sigma' == false then assert false +*) diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index a52e57f56..807b28024 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -193,21 +193,9 @@ module Inequalities : sig (** type for inequalities (and implied disequalities) *) type t - (** Extract inequalities and disequalities from [pi] *) - val from_pi : Sil.atom list -> t - - (** Extract inequalities and disequalities from [sigma] *) - val from_sigma : Sil.hpred list -> t - (** Extract inequalities and disequalities from [prop] *) val from_prop : Prop.normal Prop.t -> t - (** Join two sets of inequalities *) - val join : t -> t -> t - - (** Pretty print inequalities and disequalities *) - val pp : printenv -> Format.formatter -> t -> unit - (** Check [t |- e1!=e2]. Result [false] means "don't know". *) val check_ne : t -> Sil.exp -> Sil.exp -> bool @@ -226,6 +214,19 @@ module Inequalities : sig (** Return [true] if a simple inconsistency is detected *) val inconsistent : t -> bool +(* + (** Extract inequalities and disequalities from [pi] *) + val from_pi : Sil.atom list -> t + + (** Extract inequalities and disequalities from [sigma] *) + val from_sigma : Sil.hpred list -> t + + (** Join two sets of inequalities *) + val join : t -> t -> t + + (** Pretty print inequalities and disequalities *) + val pp : printenv -> Format.formatter -> t -> unit + (** Pretty print <= *) val d_leqs : t -> unit @@ -234,6 +235,7 @@ module Inequalities : sig (** Pretty print <> *) val d_neqs : t -> unit +*) end = struct type t = { @@ -482,6 +484,7 @@ end = struct IList.exists inconsistent_leq leqs || IList.exists inconsistent_lt lts +(* (** Pretty print inequalities and disequalities *) let pp pe fmt { leqs = leqs; lts = lts; neqs = neqs } = let pp_leq fmt (e1, e2) = F.fprintf fmt "%a<=%a" (Sil.pp_exp pe) e1 (Sil.pp_exp pe) e2 in @@ -500,6 +503,7 @@ end = struct let d_neqs { leqs = leqs; lts = lts; neqs = neqs } = let elist = IList.map (fun (e1, e2) -> Sil.BinOp(Sil.Ne, e1, e2)) lts in Sil.d_exp_list elist +*) end (* End of module Inequalities *) @@ -727,11 +731,6 @@ let check_le prop e1 e2 = let e1_le_e2 = Sil.BinOp (Sil.Le, e1, e2) in check_atom prop (Prop.mk_inequality e1_le_e2) -(** Check [prop |- e1 0 then n1 else compare2 x2 y2 - (** Check if two hpreds have the same allocated lhs *) let check_inconsistency_two_hpreds prop = let sigma = Prop.get_sigma prop in @@ -1352,10 +1347,6 @@ let rec exp_list_imply calc_missing subs l1 l2 = match l1, l2 with exp_list_imply calc_missing (exp_imply calc_missing subs e1 e2) l1 l2 | _ -> assert false -let filter_ptsto_lhs sub e0 = function - | Sil.Hpointsto (e, _, _) -> if Sil.exp_equal e0 (Sil.exp_sub sub e) then Some () else None - | _ -> None - let filter_ne_lhs sub e0 = function | Sil.Hpointsto (e, _, _) -> if Sil.exp_equal e0 (Sil.exp_sub sub e) then Some () else None | Sil.Hlseg (Sil.Lseg_NE, _, e, _, _) -> if Sil.exp_equal e0 (Sil.exp_sub sub e) then Some () else None @@ -1403,8 +1394,6 @@ let move_primed_lhs_from_front subs sigma = match sigma with | _:: _ -> sigma_unprimed @ sigma_primed else sigma -let name_n = Ident.string_to_name "n" - (** [expand_hpred_pointer calc_index_frame hpred] expands [hpred] if it is a |-> whose lhs is a Lfield or Lindex or ptr+off. Return [(changed, calc_index_frame', hpred')] where [changed] indicates whether the predicate has changed. *) let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred = @@ -2213,4 +2202,13 @@ let find_minimum_pure_cover cases = in try Some (shrink (grow [] cases)) with NO_COVER -> None +(* +(** Check [prop |- e1 if Sil.exp_equal e0 (Sil.exp_sub sub e) then Some () else None + | _ -> None +*) diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 33fcac50f..60531b4c8 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -13,8 +13,6 @@ module L = Logging module F = Format -let (++) = Sil.Int.add - let list_product l1 l2 = let l1' = IList.rev l1 in let l2' = IList.rev l2 in @@ -27,11 +25,6 @@ let rec list_rev_and_concat l1 l2 = | [] -> l2 | x1:: l1' -> list_rev_and_concat l1' (x1:: l2) -let pp_off fmt off = - IList.iter (fun n -> match n with - | Sil.Off_fld (f, t) -> F.fprintf fmt "%a " Ident.pp_fieldname f - | Sil.Off_index e -> F.fprintf fmt "%a " (Sil.pp_exp pe_text) e) off - (** Check whether the index is out of bounds. If the size is - 1, no check is performed. If the index is provably out of bound, a bound error is given. @@ -619,10 +612,6 @@ let prop_iter_add_hpred_footprint pname tenv orig_prop iter (lexp, typ) inst = let offsets_default = Sil.exp_get_offsets lexp in Prop.prop_iter_set_state iter' offsets_default -let sort_ftl ftl = - let compare (f1, _) (f2, _) = Sil.fld_compare f1 f2 in - IList.sort compare ftl - exception ARRAY_ACCESS let rearrange_arith lexp prop = @@ -644,8 +633,6 @@ let pp_rearrangement_error message prop lexp = L.d_str "Exp:"; Sil.d_exp lexp; L.d_ln (); L.d_str "Prop:"; L.d_ln (); Prop.d_prop prop; L.d_ln (); L.d_ln () -let name_n = Ident.string_to_name "n" - (** do re-arrangment for an iter whose current element is a pointsto *) let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst = if !Config.trace_rearrange then begin @@ -1130,3 +1117,14 @@ let rearrange ?(report_deref_errors=true) pdesc tenv lexp typ prop loc raise (Exceptions.Symexec_memory_error __POS__) end | Some iter -> iter_rearrange pname tenv nlexp typ prop iter inst + +(* +let pp_off fmt off = + IList.iter (fun n -> match n with + | Sil.Off_fld (f, t) -> F.fprintf fmt "%a " Ident.pp_fieldname f + | Sil.Off_index e -> F.fprintf fmt "%a " (Sil.pp_exp pe_text) e) off + +let sort_ftl ftl = + let compare (f1, _) (f2, _) = Sil.fld_compare f1 f2 in + IList.sort compare ftl +*) diff --git a/infer/src/backend/serialization.ml b/infer/src/backend/serialization.ml index 153b51184..8edd6809c 100644 --- a/infer/src/backend/serialization.ml +++ b/infer/src/backend/serialization.ml @@ -26,13 +26,6 @@ let tenv_key, summary_key, cfg_key, trace_key, cg_key, (** version of the binary files, to be incremented for each change *) let version = 24 -(** Generate random keys, to be used in an ocaml toplevel *) -let generate_keys () = - Random.self_init (); - let max_rand_int = 0x3FFFFFFF (* determined by Rand library *) in - let gen () = Random.int max_rand_int in - gen (), gen (), gen (), gen (), gen (), gen () - (** Retry the function while an exception filtered is thrown, or until the timeout in seconds expires. *) @@ -103,3 +96,12 @@ let from_file (serializer : 'a serializer) = let to_file (serializer : 'a serializer) = let (_, _, s) = serializer in s + +(* +(** Generate random keys, to be used in an ocaml toplevel *) +let generate_keys () = + Random.self_init (); + let max_rand_int = 0x3FFFFFFF (* determined by Rand library *) in + let gen () = Random.int max_rand_int in + gen (), gen (), gen (), gen (), gen (), gen () +*) diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index 1fcba7f43..1a8199cd6 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -55,10 +55,6 @@ let item_annotation_empty = [] (** Empty method annotation. *) let method_annotation_empty = [], [] -(** Check if the item annotation is empty. *) -let item_annotation_is_empty avl = - avl = [] - (** Check if the item annodation is empty. *) let item_annotation_is_empty ia = ia = [] @@ -1502,9 +1498,6 @@ let atom_compare a b = let atom_equal x y = atom_compare x y = 0 -let atom_list_compare l1 l2 = - IList.compare atom_compare l1 l2 - let lseg_kind_compare k1 k2 = match k1, k2 with | Lseg_NE, Lseg_NE -> 0 | Lseg_NE, Lseg_PE -> - 1 @@ -1620,12 +1613,6 @@ and hpara_dll_compare hp1 hp2 = let strexp_equal se1 se2 = (strexp_compare se1 se2 = 0) -let fld_strexp_equal fld_sexp1 fld_sexp2 = - (fld_strexp_compare fld_sexp1 fld_sexp2 = 0) - -let exp_strexp_equal ese1 ese2 = - (exp_strexp_compare ese1 ese2 = 0) - let hpred_equal hpred1 hpred2 = (hpred_compare hpred1 hpred2 = 0) @@ -2097,9 +2084,6 @@ let d_typ_full (t: typ) = L.add_print_action (L.PTtyp_full, Obj.repr t) (** dump a list of types. *) let d_typ_list (tl: typ list) = L.add_print_action (L.PTtyp_list, Obj.repr tl) -let pp_pair pe f ((fld: Ident.fieldname), (t: typ)) = - F.fprintf f "%a %a" (pp_typ pe) t Ident.pp_fieldname fld - (** dump an expression. *) let d_exp (e: exp) = L.add_print_action (L.PTexp, Obj.repr e) @@ -3271,13 +3255,6 @@ let sub_check_duplicated_ids sub = let f (id1, _) (id2, _) = Ident.equal id1 id2 in sorted_list_check_consecutives f sub -let sub_check_sortedness sub = - let sub' = IList.sort ident_exp_compare sub in - sub_equal sub sub' - -let sub_check_inv sub = - (sub_check_sortedness sub) && not (sub_check_duplicated_ids sub) - (** Create a substitution from a list of pairs. For all (id1, e1), (id2, e2) in the input list, if id1 = id2, then e1 = e2. *) @@ -3337,8 +3314,6 @@ let sub_symmetric_difference sub1_in sub2_in = module Typtbl = Hashtbl.Make (struct type t = typ let equal = typ_equal let hash = Hashtbl.hash end) -let typ_update_memo = Typtbl.create 17 - (** [sub_find filter sub] returns the expression associated to the first identifier that satisfies [filter]. Raise [Not_found] if there isn't one. *) let sub_find filter (sub: subst) = snd (IList.find (fun (i, _) -> filter i) sub) @@ -3687,20 +3662,12 @@ let instr_compare_structural instr1 instr2 exp_map = let atom_sub subst = atom_expmap (exp_sub subst) -let range_sub subst range = - let lower, upper = range in - let lower' = exp_sub subst lower in - let upper' = exp_sub subst upper in - (lower', upper') - let hpred_sub subst = let f (e, inst_opt) = (exp_sub subst e, inst_opt) in hpred_expmap f let hpara_sub subst para = para -let hpara_dll_sub subst para = para - (** {2 Functions for replacing occurrences of expressions.} *) let exp_replace_exp epairs e = @@ -3709,9 +3676,6 @@ let exp_replace_exp epairs e = e' with Not_found -> e -let exp_list_replace_exp epairs l = - IList.map (exp_replace_exp epairs) l - let atom_replace_exp epairs = function | Aeq (e1, e2) -> let e1' = exp_replace_exp epairs e1 in @@ -3991,17 +3955,52 @@ let hpara_dll_instantiate (para: hpara_dll) cell blink flink elist = let subst = sub_of_list ((para.cell, cell):: (para.blink, blink):: (para.flink, flink):: subst_for_svars@subst_for_evars) in (ids_evars, IList.map (hpred_sub subst) para.body_dll) -(** Return the list of expressions that could be understood as outgoing arrows from the strexp *) -let rec strexp_get_target_exps = function - | Eexp (e, inst) -> [e] - | Estruct (fsel, inst) -> IList.flatten (IList.map (fun (_, se) -> strexp_get_target_exps se) fsel) - | Earray (_, esel, _) -> - (* We ignore size and indices since they are not quite outgoing arrows. *) - IList.flatten (IList.map (fun (_, se) -> strexp_get_target_exps se) esel) - let custom_error = mk_pvar_global (Mangled.from_string "INFER_CUSTOM_ERROR") (* A block pvar used to explain retain cycles *) let block_pvar = mk_pvar (Mangled.from_string "block") (Procname.from_string_c_fun "") + +(* +(** Check if the item annotation is empty. *) +let item_annotation_is_empty avl = + avl = [] + +let atom_list_compare l1 l2 = + IList.compare atom_compare l1 l2 + +let fld_strexp_equal fld_sexp1 fld_sexp2 = + (fld_strexp_compare fld_sexp1 fld_sexp2 = 0) + +let exp_strexp_equal ese1 ese2 = + (exp_strexp_compare ese1 ese2 = 0) + +let pp_pair pe f ((fld: Ident.fieldname), (t: typ)) = + F.fprintf f "%a %a" (pp_typ pe) t Ident.pp_fieldname fld + +let sub_check_sortedness sub = + let sub' = IList.sort ident_exp_compare sub in + sub_equal sub sub' + +let sub_check_inv sub = + (sub_check_sortedness sub) && not (sub_check_duplicated_ids sub) + +let range_sub subst range = + let lower, upper = range in + let lower' = exp_sub subst lower in + let upper' = exp_sub subst upper in + (lower', upper') + +let exp_list_replace_exp epairs l = + IList.map (exp_replace_exp epairs) l + +(** Return the list of expressions that could be understood as outgoing arrows from the strexp *) +let rec strexp_get_target_exps = function + | Eexp (e, inst) -> [e] + | Estruct (fsel, inst) -> + IList.flatten (IList.map (fun (_, se) -> strexp_get_target_exps se) fsel) + | Earray (_, esel, _) -> + (* We ignore size and indices since they are not quite outgoing arrows. *) + IList.flatten (IList.map (fun (_, se) -> strexp_get_target_exps se) esel) +*) diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index fbdaddaad..07a900b19 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -649,9 +649,6 @@ val int_of_int64_kind : int64 -> ikind -> Int.t (** Comparision for ptr_kind *) val ptr_kind_compare : ptr_kind -> ptr_kind -> int -(** Equality for consts. *) -val const_equal : const -> const -> bool - (** Comparision for types. *) val typ_compare : typ -> typ -> int @@ -1340,3 +1337,8 @@ val exp_iter_types : (typ -> unit) -> exp -> unit val instr_iter_types : (typ -> unit) -> instr -> unit val custom_error : pvar + +(* +(** Equality for consts. *) +val const_equal : const -> const -> bool +*) diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index b90c0060f..781ad02d1 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -38,10 +38,6 @@ module Jprop = struct fav_add_dfs fav jp1; fav_add_dfs fav jp2 - let rec jprop_sub sub = function - | Prop (n, p) -> Prop (n, Prop.prop_sub sub p) - | Joined (n, p, jp1, jp2) -> Joined (n, Prop.prop_sub sub p, jprop_sub sub jp1, jprop_sub sub jp2) - let rec normalize = function | Prop (n, p) -> Prop (n, Prop.normalize p) | Joined (n, p, jp1, jp2) -> Joined (n, Prop.normalize p, normalize jp1, normalize jp2) @@ -133,6 +129,13 @@ module Jprop = struct let rec map (f : 'a Prop.t -> 'b Prop.t) = function | Prop (n, p) -> Prop (n, f p) | Joined (n, p, jp1, jp2) -> Joined (n, f p, map f jp1, map f jp2) + +(* + let rec jprop_sub sub = function + | Prop (n, p) -> Prop (n, Prop.prop_sub sub p) + | Joined (n, p, jp1, jp2) -> + Joined (n, Prop.prop_sub sub p, jprop_sub sub jp1, jprop_sub sub jp2) +*) end (***** End of module Jprop *****) @@ -166,15 +169,12 @@ type 'a spec = { pre: 'a Jprop.t; posts: ('a Prop.t * Paths.Path.t) list; visite module NormSpec : sig (* encapsulate type for normalized specs *) type t val normalize : Prop.normal spec -> t - val tospec : t -> Prop.normal spec val tospecs : t list -> Prop.normal spec list val compact : Sil.sharing_env -> t -> t (** Return a compact representation of the spec *) val erase_join_info_pre : t -> t (** Erase join info from pre of spec *) end = struct type t = Prop.normal spec - let tospec spec = spec - let tospecs specs = specs let spec_fav (spec: Prop.normal spec) : Sil.fav = @@ -273,10 +273,12 @@ module CallStats = struct (** module for tracing stats of function calls *) IList.sort compare !elems in IList.iter (fun (x, tr) -> f x tr) sorted_elems +(* let pp fmt t = let do_call (pname, loc) tr = F.fprintf fmt "%a %a: %a@\n" Procname.pp pname Location.pp loc pp_trace tr in iter do_call t +*) end (** stats of the calls performed during the analysis *) @@ -479,14 +481,6 @@ let empty_stats calls in_out_calls_opt = call_stats = CallStats.init calls; } -let rec post_equal pl1 pl2 = match pl1, pl2 with - | [],[] -> true - | [], _:: _ -> false - | _:: _,[] -> false - | p1:: pl1', p2:: pl2' -> - if Prop.prop_equal p1 p2 then post_equal pl1' pl2' - else false - let payload_compact sh payload = match payload.preposts with | Some specs -> @@ -519,9 +513,6 @@ let specs_filename pname = let res_dir_specs_filename pname = DB.Results_dir.path_to_filename DB.Results_dir.Abs_root [Config.specs_dir_name; specs_filename pname] -let summary_exists pname = - Sys.file_exists (DB.filename_to_string (res_dir_specs_filename pname)) - (** paths to the .specs file for the given procedure in the current spec libraries *) let specs_library_filenames pname = IList.map @@ -840,3 +831,13 @@ let reset_summary call_graph proc_name attributes_opt = ) (* =============== END of support for spec tables =============== *) + +(* +let rec post_equal pl1 pl2 = match pl1, pl2 with + | [],[] -> true + | [], _:: _ -> false + | _:: _,[] -> false + | p1:: pl1', p2:: pl2' -> + if Prop.prop_equal p1 p2 then post_equal pl1' pl2' + else false +*) diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index d50a62313..bc734c65b 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -153,9 +153,6 @@ type origin = (** Add the summary to the table for the given function *) val add_summary : Procname.t -> summary -> unit -(** Check if a summary for a given procedure exists in the results directory *) -val summary_exists : Procname.t -> bool - (** Check if a summary for a given procedure exists in the models directory *) val summary_exists_in_models : Procname.t -> bool diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 196758e8a..9ac123e04 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -13,29 +13,10 @@ module L = Logging module F = Format -let rec idlist_assoc id = function - | [] -> raise Not_found - | (i, x):: l -> if Ident.equal i id then x else idlist_assoc id l - let rec fldlist_assoc fld = function | [] -> raise Not_found | (fld', x, a):: l -> if Sil.fld_equal fld fld' then x else fldlist_assoc fld l -let rec explist_assoc e = function - | [] -> raise Not_found - | (e', x):: l -> if Sil.exp_equal e e' then x else explist_assoc e l - -let append_list_op list_op1 list_op2 = - match list_op1, list_op2 with - | None, _ -> list_op2 - | _, None -> list_op1 - | Some list1, Some list2 -> Some (list1@list2) - -let reverse_list_op list_op = - match list_op with - | None -> None - | Some list -> Some (IList.rev list) - let rec unroll_type tenv typ off = match (typ, off) with | Sil.Tvar _, _ -> @@ -294,20 +275,10 @@ module Builtin = struct Procname.Hash.replace builtin_functions proc_name sym_exe_fun; proc_name - (* register a builtin plain function name and symbolic execution handler *) - let register_plain proc_name_str (sym_exe_fun: sym_exe_builtin) = - let proc_name = Procname.from_string_c_fun proc_name_str in - Hashtbl.replace builtin_plain_functions proc_name_str sym_exe_fun; - proc_name - (* register a builtin [Procname.t] and symbolic execution handler *) let register_procname proc_name (sym_exe_fun: sym_exe_builtin) = Procname.Hash.replace builtin_functions proc_name sym_exe_fun - (* register a builtin plain [Procname.t] and symbolic execution handler *) - let register_plain_procname proc_name (sym_exe_fun: sym_exe_builtin) = - Hashtbl.replace builtin_plain_functions (Procname.to_string proc_name) sym_exe_fun - (** print the functions registered *) let pp_registered fmt () = let builtin_names = ref [] in @@ -317,6 +288,18 @@ module Builtin = struct Format.fprintf fmt "Registered builtins:@\n @["; IList.iter pp !builtin_names; Format.fprintf fmt "@]@." + +(* + (** register a builtin plain function name and symbolic execution handler *) + let register_plain proc_name_str (sym_exe_fun: sym_exe_builtin) = + let proc_name = Procname.from_string_c_fun proc_name_str in + Hashtbl.replace builtin_plain_functions proc_name_str sym_exe_fun; + proc_name + + (** register a builtin plain [Procname.t] and symbolic execution handler *) + let register_plain_procname proc_name (sym_exe_fun: sym_exe_builtin) = + Hashtbl.replace builtin_plain_functions (Procname.to_string proc_name) sym_exe_fun +*) end (** print the builtin functions and exit *) @@ -464,25 +447,6 @@ let call_should_be_skipped callee_pname summary = (* treat calls with no specs as skip functions in angelic mode *) || (!Config.angelic_execution && Specs.get_specs_from_payload summary == []) -let report_raise_memory_leak tenv msg hpred prop = - L.d_strln msg; - L.d_increase_indent 1; - L.d_strln "PROP:"; - Prop.d_prop prop; L.d_ln (); - L.d_strln "PREDICATE:"; - Prop.d_sigma [hpred]; - L.d_decrease_indent 1; - L.d_ln (); - let footprint_part = false in - let resource = match Errdesc.hpred_is_open_resource prop hpred with - | Some res -> res - | None -> Sil.Rmemory Sil.Mmalloc in - raise - (Exceptions.Leak - (footprint_part, prop, hpred, - Errdesc.explain_leak tenv hpred prop None None, false, - resource, __POS__)) - (** In case of constant string dereference, return the result immediately *) let check_constant_string_dereference lexp = let string_lookup s n = @@ -2654,3 +2618,43 @@ module ModelBuiltins = struct end (* ============== END of ModelBuiltins ============== *) + +(* +let rec idlist_assoc id = function + | [] -> raise Not_found + | (i, x):: l -> if Ident.equal i id then x else idlist_assoc id l + +let rec explist_assoc e = function + | [] -> raise Not_found + | (e', x):: l -> if Sil.exp_equal e e' then x else explist_assoc e l + +let append_list_op list_op1 list_op2 = + match list_op1, list_op2 with + | None, _ -> list_op2 + | _, None -> list_op1 + | Some list1, Some list2 -> Some (list1@list2) + +let reverse_list_op list_op = + match list_op with + | None -> None + | Some list -> Some (IList.rev list) + +let report_raise_memory_leak tenv msg hpred prop = + L.d_strln msg; + L.d_increase_indent 1; + L.d_strln "PROP:"; + Prop.d_prop prop; L.d_ln (); + L.d_strln "PREDICATE:"; + Prop.d_sigma [hpred]; + L.d_decrease_indent 1; + L.d_ln (); + let footprint_part = false in + let resource = match Errdesc.hpred_is_open_resource prop hpred with + | Some res -> res + | None -> Sil.Rmemory Sil.Mmalloc in + raise + (Exceptions.Leak + (footprint_part, prop, hpred, + Errdesc.explain_leak tenv hpred prop None None, false, + resource, __POS__)) +*) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 49ed7a74b..1f69fb589 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -120,20 +120,6 @@ let spec_find_rename trace_call (proc_name : Procname.t) : (int * Prop.exposed S (Localise.verbatim_desc (Procname.to_string proc_name), __POS__)) end -let check_splitting_precondition sub1 sub2 = - let dom1 = Sil.sub_domain sub1 in - let rng1 = Sil.sub_range sub1 in - let dom2 = Sil.sub_domain sub2 in - let rng2 = Sil.sub_range sub2 in - let overlap = IList.exists (fun id -> IList.exists (Ident.equal id) dom1) dom2 in - if overlap then begin - L.d_str "Dom(Sub1): "; Sil.d_exp_list (IList.map (fun id -> Sil.Var id) dom1); L.d_ln (); - L.d_str "Ran(Sub1): "; Sil.d_exp_list rng1; L.d_ln (); - L.d_str "Dom(Sub2): "; Sil.d_exp_list (IList.map (fun id -> Sil.Var id) dom2); L.d_ln (); - L.d_str "Ran(Sub2): "; Sil.d_exp_list rng2; L.d_ln (); - assert false - end - (** Process a splitting coming straight from a call to the prover: change the instantiating substitution so that it returns primed vars, except for vars occurring in the missing part, where it returns @@ -1046,14 +1032,6 @@ let prop_pure_to_footprint (p: 'a Prop.t) : Prop.normal Prop.t = else (** add pure fact to footprint *) Prop.normalize (Prop.replace_pi_footprint (Prop.get_pi_footprint p @ new_footprint_atoms) p) -(** check whether 0|->- occurs in sigma *) -let sigma_has_null_pointer sigma = - let hpred_null_pointer = function - | Sil.Hpointsto (e, _, _) -> - Sil.exp_equal e Sil.exp_zero - | _ -> false in - IList.exists hpred_null_pointer sigma - (** post-process the raw result of a function call *) let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop results = let filter_valid_res = function @@ -1194,3 +1172,27 @@ let exe_function_call tenv cfg ret_ids caller_pdesc callee_pname loc actual_para let exe_one_spec (n, spec) = exe_spec tenv cfg ret_ids (n, nspecs) caller_pdesc callee_pname loc prop path spec actual_params formal_params in let results = IList.map exe_one_spec spec_list in exe_call_postprocess tenv ret_ids trace_call callee_pname loc prop results + +(* +let check_splitting_precondition sub1 sub2 = + let dom1 = Sil.sub_domain sub1 in + let rng1 = Sil.sub_range sub1 in + let dom2 = Sil.sub_domain sub2 in + let rng2 = Sil.sub_range sub2 in + let overlap = IList.exists (fun id -> IList.exists (Ident.equal id) dom1) dom2 in + if overlap then begin + L.d_str "Dom(Sub1): "; Sil.d_exp_list (IList.map (fun id -> Sil.Var id) dom1); L.d_ln (); + L.d_str "Ran(Sub1): "; Sil.d_exp_list rng1; L.d_ln (); + L.d_str "Dom(Sub2): "; Sil.d_exp_list (IList.map (fun id -> Sil.Var id) dom2); L.d_ln (); + L.d_str "Ran(Sub2): "; Sil.d_exp_list rng2; L.d_ln (); + assert false + end + +(** check whether 0|->- occurs in sigma *) +let sigma_has_null_pointer sigma = + let hpred_null_pointer = function + | Sil.Hpointsto (e, _, _) -> + Sil.exp_equal e Sil.exp_zero + | _ -> false in + IList.exists hpred_null_pointer sigma +*) diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index d1d811c76..56fefacbf 100644 --- a/infer/src/checkers/annotations.ml +++ b/infer/src/checkers/annotations.ml @@ -30,8 +30,6 @@ let equal as1 as2 = IList.for_all2 param_equal as1.params as2.params let visibleForTesting = "com.google.common.annotations.VisibleForTesting" -let javaxNullable = "javax.annotation.Nullable" -let javaxNonnull = "javax.annotation.Nonnull" let suppressLint = "android.annotation.SuppressLint" diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index 75c00f1bc..b2b58abea 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/infer/src/checkers/patternMatch.ml @@ -181,9 +181,6 @@ let get_vararg_type_names IList.rev (type_names call_node) -let has_type_name typ type_name = - get_type_name typ = type_name - let has_formal_proc_argument_type_names proc_desc proc_name argument_type_names = let formals = Cfg.Procdesc.get_formals proc_desc in let equal_formal_arg (_, typ) arg_type_name = get_type_name typ = arg_type_name in diff --git a/infer/src/checkers/performanceCritical.ml b/infer/src/checkers/performanceCritical.ml index 2feb29d46..1c42376e3 100644 --- a/infer/src/checkers/performanceCritical.ml +++ b/infer/src/checkers/performanceCritical.ml @@ -35,10 +35,6 @@ let check_attributes check attributes = check ret_annotation -let is_performance_critical attributes = - check_attributes Annotations.ia_is_performance_critical attributes - - let is_expensive attributes = check_attributes Annotations.ia_is_expensive attributes @@ -318,3 +314,8 @@ let callback_performance_checker { Callbacks.proc_desc; proc_name; get_proc_desc check_one_procedure tenv proc_name proc_desc; Ondemand.unset_callbacks () end + +(* +let is_performance_critical attributes = + check_attributes Annotations.ia_is_performance_critical attributes +*) diff --git a/infer/src/checkers/printfArgs.ml b/infer/src/checkers/printfArgs.ml index 22656a473..8b916fb70 100644 --- a/infer/src/checkers/printfArgs.ml +++ b/infer/src/checkers/printfArgs.ml @@ -17,15 +17,6 @@ type printf_signature = { vararg_pos: int option } -let printf_signature_to_string - (printf: printf_signature): string = - Printf.sprintf - "{%s; %d [%s] %s}" - printf.unique_id - printf.format_pos - (String.concat "," (IList.map string_of_int printf.fixed_pos)) - (match printf.vararg_pos with | Some i -> string_of_int i | _ -> "-") - let printf_like_functions = ref [ @@ -221,3 +212,13 @@ let check_printf_args_ok let callback_printf_args { Callbacks.proc_desc; proc_name } : unit = Cfg.Procdesc.iter_instrs (fun n i -> check_printf_args_ok n i proc_name proc_desc) proc_desc +(* +let printf_signature_to_string + (printf: printf_signature): string = + Printf.sprintf + "{%s; %d [%s] %s}" + printf.unique_id + printf.format_pos + (String.concat "," (IList.map string_of_int printf.fixed_pos)) + (match printf.vararg_pos with | Some i -> string_of_int i | _ -> "-") +*) diff --git a/infer/src/clang/cFrontend_utils.ml b/infer/src/clang/cFrontend_utils.ml index 36fa33b23..755f2fef6 100644 --- a/infer/src/clang/cFrontend_utils.ml +++ b/infer/src/clang/cFrontend_utils.ml @@ -255,22 +255,6 @@ struct | Some name_info -> Some (get_qualified_name name_info) | None -> None - let rec getter_attribute_opt attributes = - match attributes with - | [] -> None - | attr:: rest -> - match attr with - | `Getter getter -> getter.Clang_ast_t.dr_name - | _ -> (getter_attribute_opt rest) - - let rec setter_attribute_opt attributes = - match attributes with - | [] -> None - | attr:: rest -> - match attr with - | `Setter setter -> setter.Clang_ast_t.dr_name - | _ -> (setter_attribute_opt rest) - let pointer_counter = ref 0 let get_fresh_pointer () = @@ -382,6 +366,23 @@ struct ignore (type_ptr_to_sil_type tenv (`DeclPtr dr.Clang_ast_t.dr_decl_pointer)) in IList.iter add_elem decl_ref_list +(* + let rec getter_attribute_opt attributes = + match attributes with + | [] -> None + | attr:: rest -> + match attr with + | `Getter getter -> getter.Clang_ast_t.dr_name + | _ -> (getter_attribute_opt rest) + + let rec setter_attribute_opt attributes = + match attributes with + | [] -> None + | attr:: rest -> + match attr with + | `Setter setter -> setter.Clang_ast_t.dr_name + | _ -> (setter_attribute_opt rest) +*) end (* Global counter for anonymous block*) @@ -417,8 +418,6 @@ struct | [item] -> item | item:: l' -> item^" "^(string_from_list l') - let get_fun_body fdecl_info = fdecl_info.Clang_ast_t.fdi_body - let rec append_no_duplicates eq list1 list2 = match list2 with | el:: rest2 -> diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index a1667facc..a2413219d 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -431,10 +431,6 @@ let create_procdesc_with_pointer context pointer class_name_opt name tp = create_external_procdesc context.cfg callee_name false None; callee_name -let instance_to_method_call_type instance = - if instance then MCVirtual - else MCStatic - let get_method_for_frontend_checks cfg cg tenv class_name decl_info = let stmt_info = Ast_expressions.make_stmt_info decl_info in let source_range = decl_info.Clang_ast_t.di_source_range in @@ -454,3 +450,9 @@ let get_method_for_frontend_checks cfg cg tenv class_name decl_info = Cfg.Node.set_succs_exn start_node [end_node] []; Cg.add_defined_node cg proc_name; pdesc + +(* +let instance_to_method_call_type instance = + if instance then MCVirtual + else MCStatic +*) diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index f040fc4f7..4a5b89c06 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -2320,8 +2320,6 @@ struct and get_clang_stmt_trans stmt = fun trans_state -> instruction trans_state stmt - and empty_trans_fun trans_state = empty_res_trans - (* TODO write translate function for cxx constructor exprs *) and get_custom_stmt_trans stmt = match stmt with | `ClangStmt stmt -> get_clang_stmt_trans stmt diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 870e5c662..b4b92d68b 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -464,12 +464,6 @@ let is_superinstance mei = let get_selector_receiver obj_c_message_expr_info = obj_c_message_expr_info.Clang_ast_t.omei_selector, obj_c_message_expr_info.Clang_ast_t.omei_receiver_kind -(* Similar to extract_item_from_singleton but for option type *) -let extract_item_from_option op warning_string = - match op with - | Some item -> item - | _ -> Printing.log_err warning_string; assert false - let is_member_exp stmt = match stmt with | Clang_ast_t.MemberExpr _ -> true @@ -490,15 +484,9 @@ let is_null_stmt s = | Clang_ast_t.NullStmt _ -> true | _ -> false -let dummy_id () = - Ident.create_normal (Ident.string_to_name "DUMMY_ID_INFER") 0 - let extract_stmt_from_singleton stmt_list warning_string = extract_item_from_singleton stmt_list warning_string (Ast_expressions.dummy_stmt ()) -let extract_id_from_singleton id_list warning_string = - extract_item_from_singleton id_list warning_string (dummy_id ()) - let rec get_type_from_exp_stmt stmt = let do_decl_ref_exp i = match i.Clang_ast_t.drti_decl_ref with @@ -646,10 +634,21 @@ let is_dispatch_function stmt_list = | _ -> None)) | _ -> None +let is_block_enumerate_function mei = + mei.Clang_ast_t.omei_selector = CFrontend_config.enumerateObjectsUsingBlock + +(* +(** Similar to extract_item_from_singleton but for option type *) +let extract_item_from_option op warning_string = + match op with + | Some item -> item + | _ -> Printing.log_err warning_string; assert false + +let extract_id_from_singleton id_list warning_string = + extract_item_from_singleton id_list warning_string (dummy_id ()) + let get_decl_pointer decl_ref_expr_info = match decl_ref_expr_info.Clang_ast_t.drti_decl_ref with | Some decl_ref -> decl_ref.Clang_ast_t.dr_decl_pointer | None -> assert false - -let is_block_enumerate_function mei = - mei.Clang_ast_t.omei_selector = CFrontend_config.enumerateObjectsUsingBlock +*) diff --git a/infer/src/clang/cTypes.ml b/infer/src/clang/cTypes.ml index dd7e815e5..1b407b8c0 100644 --- a/infer/src/clang/cTypes.ml +++ b/infer/src/clang/cTypes.ml @@ -12,23 +12,11 @@ open CFrontend_utils module L = Logging -let get_type_from_expr_info ei = - ei.Clang_ast_t.ei_type_ptr - let get_name_from_struct s = match s with | Sil.Tstruct { Sil.struct_name = Some n } -> n | _ -> assert false -let rec get_type_list nn ll = - match ll with - | [] -> [] - | (n, t):: ll' -> (* Printing.log_out ">>>>>Searching for type '%s'. Seen '%s'.@." nn n; *) - if n = nn then ( - Printing.log_out ">>>>>>>>>>>>>>>>>>>>>>>NOW Found, Its type is: '%s'@." (Sil.typ_to_string t); - [t] - ) else get_type_list nn ll' - let add_pointer_to_typ typ = Sil.Tptr(typ, Sil.Pk_pointer) @@ -128,3 +116,15 @@ let get_name_from_type_pointer custom_type_pointer = match Str.split (Str.regexp "*") custom_type_pointer with | [pointer_type_info; class_name] -> pointer_type_info, class_name | _ -> assert false + +(* +let rec get_type_list nn ll = + match ll with + | [] -> [] + | (n, t):: ll' -> (* Printing.log_out ">>>>>Searching for type '%s'. Seen '%s'.@." nn n; *) + if n = nn then ( + Printing.log_out ">>>>>>>>>>>>>>>>>>>>>>>NOW Found, Its type is: '%s'@." + (Sil.typ_to_string t); + [t] + ) else get_type_list nn ll' +*) diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index ffc555306..506191399 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -115,7 +115,6 @@ struct let module DFTypeCheck = MakeDF(struct type t = Extension.extension TypeState.t - let initial = TypeState.empty Extension.ext let equal = TypeState.equal let join = TypeState.join Extension.ext let do_node node typestate = diff --git a/infer/src/harness/androidFramework.ml b/infer/src/harness/androidFramework.ml index c5b8e4847..ae19146ea 100644 --- a/infer/src/harness/androidFramework.ml +++ b/infer/src/harness/androidFramework.ml @@ -349,12 +349,6 @@ let get_callbacks_registered_by_proc procdesc tenv = | _ -> callback_typs in Cfg.Procdesc.fold_instrs collect_callback_typs [] procdesc -(** returns true if [procname] is a method that registers a callback *) -let is_callback_register_method procname args tenv = - match get_callback_registered_by procname args tenv with - | Some _ -> true - | None -> false - (** given an Android framework type mangled string [lifecycle_typ] (e.g., android.app.Activity) and a list of method names [lifecycle_procs_strs], get the appropriate typ and procnames *) let get_lifecycle_for_framework_typ_opt lifecycle_typ lifecycle_proc_strs tenv = @@ -393,3 +387,11 @@ let is_runtime_exception tenv exn = let non_stub_android_jar () = let root_dir = Filename.dirname (Filename.dirname Sys.executable_name) in IList.fold_left Filename.concat root_dir ["lib"; "java"; "android"; "android-19.jar"] + +(* +(** returns true if [procname] is a method that registers a callback *) +let is_callback_register_method procname args tenv = + match get_callback_registered_by procname args tenv with + | Some _ -> true + | None -> false +*) diff --git a/infer/src/harness/harness.ml b/infer/src/harness/harness.ml index 0913f55e8..7535efe8e 100644 --- a/infer/src/harness/harness.ml +++ b/infer/src/harness/harness.ml @@ -192,7 +192,5 @@ let create_android_harness proc_file_map tenv = | None -> () ) AndroidFramework.get_lifecycles -let parse_trace trace = Stacktrace.parse_stack_trace trace - (** Generate a harness method for exe_env and add it to the execution environment *) let create_harness proc_file_map tenv = create_android_harness proc_file_map tenv diff --git a/infer/src/harness/stacktrace.ml b/infer/src/harness/stacktrace.ml index 08911cfc6..30b638be5 100644 --- a/infer/src/harness/stacktrace.ml +++ b/infer/src/harness/stacktrace.ml @@ -88,6 +88,8 @@ let pp_str_frame fmt = function | Unresolved f -> F.fprintf fmt "UNRESOLVED: %s %s %s %d" f.class_str f.method_str f.file_str f.line_num +(* let rec pp_str_stack_trace fmt = function | [] -> () | frame :: rest -> F.fprintf fmt "%a;@\n%a" pp_str_frame frame pp_str_stack_trace rest +*) diff --git a/infer/src/java/jClasspath.ml b/infer/src/java/jClasspath.ml index 894352507..081f484e5 100644 --- a/infer/src/java/jClasspath.ml +++ b/infer/src/java/jClasspath.ml @@ -14,13 +14,6 @@ module L = Logging let models_specs_filenames = ref StringSet.empty -let arg_classpath = ref "" - -let arg_jarfile = ref "" - -let set_jarfile file = - arg_jarfile := file - let javac_verbose_out = ref "" let set_verbose_out path = @@ -267,12 +260,6 @@ let collect_classes classmap jar_filename = classes -let classmap_of_classpath classpath = - let jar_filenames = - IList.filter (fun p -> not (Sys.is_directory p)) (split_classpath classpath) in - IList.fold_left collect_classes JBasics.ClassMap.empty jar_filenames - - let load_program classpath classes = JUtils.log "loading program ... %!"; let models = @@ -288,3 +275,10 @@ let load_program classpath classes = classes; JUtils.log "done@."; program + +(* +let classmap_of_classpath classpath = + let jar_filenames = + IList.filter (fun p -> not (Sys.is_directory p)) (split_classpath classpath) in + IList.fold_left collect_classes JBasics.ClassMap.empty jar_filenames +*) diff --git a/infer/src/java/jContext.ml b/infer/src/java/jContext.ml index 2a6df071e..b1c047afc 100644 --- a/infer/src/java/jContext.ml +++ b/infer/src/java/jContext.ml @@ -88,8 +88,6 @@ let get_or_set_pvar_type context var typ = set_var_map context (JBir.VarMap.add var (pvar, typ, typ) var_map); (pvar, typ) -let lookup_pvar_type context var typ = (get_or_set_pvar_type context var typ) - let set_pvar context var typ = fst (get_or_set_pvar_type context var typ) let reset_pvar_type context = diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 29dd0e9ac..1833f48e0 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -174,11 +174,6 @@ let get_constant (c : JBir.const) = | `Long i64 -> Sil.Cint (Sil.Int.of_int64 i64) | `String jstr -> Sil.Cstr (JBasics.jstr_pp jstr) -let static_field_name cn fs = - let classname = JBasics.cn_name cn in - let fieldname = JBasics.fs_name fs in - Mangled.from_string (classname^"."^fieldname) - let get_binop binop = match binop with | JBir.Add _ -> Sil.PlusA @@ -1133,3 +1128,10 @@ let rec instruction context pc instr : translation = with Frontend_error s -> JUtils.log "Skipping because of: %s@." s; Skip + +(* +let static_field_name cn fs = + let classname = JBasics.cn_name cn in + let fieldname = JBasics.fs_name fs in + Mangled.from_string (classname^"."^fieldname) +*) diff --git a/infer/src/java/jTransStaticField.ml b/infer/src/java/jTransStaticField.ml index 432094e26..1b500bfdc 100644 --- a/infer/src/java/jTransStaticField.ml +++ b/infer/src/java/jTransStaticField.ml @@ -26,12 +26,6 @@ let sort_pcs () = field_final_pcs := (IList.sort Pervasives.compare !field_final_pcs); field_nonfinal_pcs := (IList.sort Pervasives.compare !field_nonfinal_pcs) -let is_basic_type fs = - let vt = (JBasics.fs_type fs) in - match vt with - | JBasics.TBasic bt -> true - | JBasics.TObject ot -> false - (** Returns whether the node contains static final fields that are not of a primitive type or String. *) let has_static_final_fields node = @@ -206,3 +200,11 @@ let is_static_final_field context cn fs = let is_final = Javalib.is_final_field f in (is_static && is_final) with Not_found -> false + +(* +let is_basic_type fs = + let vt = (JBasics.fs_type fs) in + match vt with + | JBasics.TBasic bt -> true + | JBasics.TObject ot -> false +*) diff --git a/infer/src/java/jUtils.ml b/infer/src/java/jUtils.ml index c2d943cb4..2f998d560 100644 --- a/infer/src/java/jUtils.ml +++ b/infer/src/java/jUtils.ml @@ -8,24 +8,25 @@ * of patent rights can be found in the PATENTS file in the same directory. *) -open Javalib_pack +let rec log fmt = + if !JConfig.debug_mode then + Logging.stdout fmt + else + Obj.magic log + +(* +open Javalib_pack let get_native_methods program = let select_native m l = let is_native cm = (cm.Javalib.cm_implementation = Javalib.Native) in match m with | Javalib.ConcreteMethod cm when is_native cm -> - let (cn, ms) = JBasics.cms_split - cm.Javalib.cm_class_method_signature in ((JBasics.cn_name cn)^"."^(JBasics.ms_name ms)):: l + let (cn, ms) = JBasics.cms_split cm.Javalib.cm_class_method_signature in + ((JBasics.cn_name cn)^"."^(JBasics.ms_name ms)):: l | _ -> l in let collect _ node l = (Javalib.m_fold select_native node l) in JBasics.ClassMap.fold collect program [] - - -let rec log fmt = - if !JConfig.debug_mode then - Logging.stdout fmt - else - Obj.magic log +*)