diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 887f25a97..b269cc981 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -1137,9 +1137,11 @@ let print_retain_cycle _prop = | None -> () | Some (Some _prop) -> let loc = State.get_loc () in - let source_file = DB.source_file_to_string loc.Sil.file in + let source_file = DB.source_file_to_string loc.Location.file in let source_file'= Str.global_replace (Str.regexp_string "/") "_" source_file in - let dest_file_str = (DB.filename_to_string (DB.Results_dir.specs_dir ()))^"/"^source_file'^"_RETAIN_CYCLE_"^(Sil.loc_to_string loc)^".dot" in + let dest_file_str = + (DB.filename_to_string (DB.Results_dir.specs_dir ())) ^ "/" ^ + source_file' ^ "_RETAIN_CYCLE_" ^ (Location.to_string loc) ^ ".dot" in L.d_strln ("Printing dotty proposition for retain cycle in :"^dest_file_str); Prop.d_prop _prop; L.d_strln ""; Dotty.dotty_prop_to_dotty_file dest_file_str _prop @@ -1263,78 +1265,87 @@ let check_junk ?original_prop pname tenv prop = let entries = hpred_entries hpred in if should_remove_hpred entries then begin - let part = if fp_part then "footprint" else "normal" in - L.d_strln (".... Prop with garbage in " ^ part ^ " part ...."); - L.d_increase_indent 1; - L.d_strln "PROP:"; - Prop.d_prop prop; L.d_ln (); - L.d_strln "PREDICATE:"; - Prop.d_sigma [hpred]; + let part = if fp_part then "footprint" else "normal" in + L.d_strln (".... Prop with garbage in " ^ part ^ " part ...."); + 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_ln (); let alloc_attribute = (* find the alloc attribute of one of the roots of hpred, if it exists *) - let res = ref None in - let do_entry e = - match Prop.get_resource_undef_attribute prop e with - | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Racquire }) as a) -> - L.d_str "ATTRIBUTE: "; Sil.d_exp (Sil.Const (Sil.Cattribute a)); L.d_ln (); - res := Some a - | Some (Sil.Aundef _ as a) -> - res := Some a - | _ -> () in - list_iter do_entry entries; - !res in - L.d_decrease_indent 1; - let is_undefined = match alloc_attribute with - | Some (Sil.Aundef _) -> true - | _ -> false in - let resource = match Errdesc.hpred_is_open_resource prop hpred with - | Some res -> res - | None -> Sil.Rmemory Sil.Mmalloc in - let objc_ml_bucket_opt = - match resource with - | Sil.Rmemory Sil.Mobjc -> should_raise_objc_leak prop hpred - | _ -> None in - let exn_retain_cycle cycle = - print_retain_cycle original_prop; - let desc = Errdesc.explain_retain_cycle (remove_opt original_prop) cycle (State.get_loc ()) in - Exceptions.Retain_cycle(remove_opt original_prop, hpred, desc, try assert false with Assert_failure x -> x) in - let exn_leak = - Exceptions.Leak (fp_part, prop, hpred, Errdesc.explain_leak tenv hpred prop alloc_attribute objc_ml_bucket_opt, !Absarray.array_abstraction_performed, resource, try assert false with Assert_failure x -> x) in - let ignore_resource, exn = - (match alloc_attribute, resource with - | Some _, Sil.Rmemory Sil.Mobjc when (hpred_in_cycle hpred) -> - (* When there is a cycle in objc we ignore it only if it has weak or unsafe_unretained fields *) - (* Otherwise we report a retain cycle*) - let cycle = get_var_retain_cycle (remove_opt original_prop) in - if cycle_has_weak_or_unretained_or_assign_field cycle then - true, exn_retain_cycle cycle - else false, exn_retain_cycle cycle - | Some _, Sil.Rmemory Sil.Mobjc -> - objc_ml_bucket_opt = None, exn_leak - | Some _, Sil.Rmemory _ -> !Sil.curr_language = Sil.Java, exn_leak - | Some _, Sil.Rignore -> true, exn_leak - | Some _, Sil.Rfile -> false, exn_leak - | Some _, Sil.Rlock -> false, exn_leak - | _ when hpred_in_cycle hpred && Sil.has_objc_ref_counter hpred -> - (* When its a cycle and the object has a ref counter then *) - (* we have a retain cycle. Objc object may not have the *) - (* Sil.Mobjc qualifier when added in footprint doing abduction *) - let cycle = get_var_retain_cycle (remove_opt original_prop) in - false, exn_retain_cycle cycle - | _ -> !Sil.curr_language = Sil.Java, exn_leak) in - let already_reported () = - let attr_opt_equal ao1 ao2 = match ao1, ao2 with - | None, None -> true - | Some a1, Some a2 -> Sil.attribute_equal a1 a2 - | Some _, None - | None, Some _ -> false in - (alloc_attribute = None && !leaks_reported <> []) || (* None attribute only reported if it's the first one *) + let res = ref None in + let do_entry e = + match Prop.get_resource_undef_attribute prop e with + | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Racquire }) as a) -> + L.d_str "ATTRIBUTE: "; Sil.d_exp (Sil.Const (Sil.Cattribute a)); L.d_ln (); + res := Some a + | Some (Sil.Aundef _ as a) -> + res := Some a + | _ -> () in + list_iter do_entry entries; + !res in + L.d_decrease_indent 1; + let is_undefined = match alloc_attribute with + | Some (Sil.Aundef _) -> true + | _ -> false in + let resource = match Errdesc.hpred_is_open_resource prop hpred with + | Some res -> res + | None -> Sil.Rmemory Sil.Mmalloc in + let objc_ml_bucket_opt = + match resource with + | Sil.Rmemory Sil.Mobjc -> should_raise_objc_leak prop hpred + | _ -> None in + let exn_retain_cycle cycle = + print_retain_cycle original_prop; + let desc = Errdesc.explain_retain_cycle + (remove_opt original_prop) cycle (State.get_loc ()) in + Exceptions.Retain_cycle + (remove_opt original_prop, hpred, desc, + try assert false with Assert_failure x -> x) in + let exn_leak = Exceptions.Leak + (fp_part, prop, hpred, + Errdesc.explain_leak tenv hpred prop alloc_attribute objc_ml_bucket_opt, + !Absarray.array_abstraction_performed, + resource, + try assert false with Assert_failure x -> x) in + let ignore_resource, exn = + (match alloc_attribute, resource with + | Some _, Sil.Rmemory Sil.Mobjc when (hpred_in_cycle hpred) -> + (* When there is a cycle in objc we ignore it *) + (* only if it has weak or unsafe_unretained fields. *) + (* Otherwise we report a retain cycle. *) + let cycle = get_var_retain_cycle (remove_opt original_prop) in + if cycle_has_weak_or_unretained_or_assign_field cycle then + true, exn_retain_cycle cycle + else false, exn_retain_cycle cycle + | Some _, Sil.Rmemory Sil.Mobjc -> + objc_ml_bucket_opt = None, exn_leak + | Some _, Sil.Rmemory _ -> !Config.curr_language = Config.Java, exn_leak + | Some _, Sil.Rignore -> true, exn_leak + | Some _, Sil.Rfile -> false, exn_leak + | Some _, Sil.Rlock -> false, exn_leak + | _ when hpred_in_cycle hpred && Sil.has_objc_ref_counter hpred -> + (* When its a cycle and the object has a ref counter then *) + (* we have a retain cycle. Objc object may not have the *) + (* Sil.Mobjc qualifier when added in footprint doing abduction *) + let cycle = get_var_retain_cycle (remove_opt original_prop) in + false, exn_retain_cycle cycle + | _ -> !Config.curr_language = Config.Java, exn_leak) in + let already_reported () = + let attr_opt_equal ao1 ao2 = match ao1, ao2 with + | None, None -> true + | Some a1, Some a2 -> Sil.attribute_equal a1 a2 + | Some _, None + | None, Some _ -> false in + (alloc_attribute = None && !leaks_reported <> []) || + (* None attribute only reported if it's the first one *) list_mem attr_opt_equal alloc_attribute !leaks_reported in let ignore_leak = !Config.allowleak || ignore_resource || is_undefined || already_reported () in let report_and_continue = - !Sil.curr_language = Sil.Java || !Config.footprint in + !Config.curr_language = Config.Java || !Config.footprint in let report_leak () = if not report_and_continue then raise exn else diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml index e59465e60..98f5e34f2 100644 --- a/infer/src/backend/buckets.ml +++ b/infer/src/backend/buckets.ml @@ -58,7 +58,7 @@ let check_access access_opt de_opt = let process_formal_letref = function | Sil.Letderef (id, Sil.Lvar pvar, _, _) -> let is_java_this = - !Sil.curr_language = Sil.Java && Sil.pvar_is_this pvar in + !Config.curr_language = Config.Java && Sil.pvar_is_this pvar in if not is_java_this && is_formal pvar then formal_ids := id :: !formal_ids | _ -> () in list_iter process_formal_letref node_instrs; @@ -91,7 +91,7 @@ let check_access access_opt de_opt = list_exists filter (Cfg.Node.get_instrs node) in let local_access_found = ref false in let do_node node = - if (Cfg.Node.get_loc node).Sil.line = line_number && has_call_or_sets_null node then + if (Cfg.Node.get_loc node).Location.line = line_number && has_call_or_sets_null node then begin local_access_found := true end in diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 571318537..903e303c7 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -125,12 +125,12 @@ let get_procedure_definition exe_env proc_name = (idenv, tenv, proc_name, proc_desc, language)) (Cfg.Procdesc.find_from_name cfg proc_name) -let get_language proc_name = if Procname.is_java proc_name then Sil.Java else Sil.C_CPP +let get_language proc_name = if Procname.is_java proc_name then Config.Java else Config.C_CPP (** Invoke all registered procedure callbacks on a set of procedures. *) let iterate_procedure_callbacks all_procs exe_env proc_name = let procedure_language = get_language proc_name in - Sil.curr_language := procedure_language; + Config.curr_language := procedure_language; let cfg = Exe_env.get_cfg exe_env proc_name in let get_procdesc proc_name = @@ -195,11 +195,11 @@ let iterate_cluster_callbacks all_procs exe_env proc_names = (** Invoke all procedure and cluster callbacks on a given environment. *) let iterate_callbacks store_summary call_graph exe_env = let proc_names = Cg.get_defined_nodes call_graph in - let saved_language = !Sil.curr_language in + let saved_language = !Config.curr_language in let cluster_id proc_name = match get_language proc_name with - | Sil.Java -> Procname.java_get_class proc_name + | Config.Java -> Procname.java_get_class proc_name | _ -> "unknown" in let cluster proc_names = let cluster_map = @@ -224,7 +224,7 @@ let iterate_callbacks store_summary call_graph exe_env = let loc = match procdesc_opt with | Some proc_desc -> Cfg.Procdesc.get_loc proc_desc - | None -> Sil.loc_none in + | None -> Location.loc_none in Specs.reset_summary call_graph proc_name loc in @@ -243,4 +243,4 @@ let iterate_callbacks store_summary call_graph exe_env = list_iter store_summary proc_names; - Sil.curr_language := saved_language + Config.curr_language := saved_language diff --git a/infer/src/backend/callbacks.mli b/infer/src/backend/callbacks.mli index f3ffc4f8d..f603bb4d5 100644 --- a/infer/src/backend/callbacks.mli +++ b/infer/src/backend/callbacks.mli @@ -32,10 +32,10 @@ type cluster_callback_t = unit (** register a procedure callback *) -val register_procedure_callback : Sil.language option -> proc_callback_t -> unit +val register_procedure_callback : Config.language option -> proc_callback_t -> unit (** register a cluster callback *) -val register_cluster_callback : Sil.language option -> cluster_callback_t -> unit +val register_cluster_callback : Config.language option -> cluster_callback_t -> unit (** un-register all the procedure callbacks currently registered *) val unregister_all_callbacks : unit -> unit diff --git a/infer/src/backend/cfg.ml b/infer/src/backend/cfg.ml index 9318be2d0..be29e9b0e 100644 --- a/infer/src/backend/cfg.ml +++ b/infer/src/backend/cfg.ml @@ -34,7 +34,7 @@ module Node = struct mutable nd_exn : t list; (** exception nodes in the cfg *) mutable nd_instrs : Sil.instr list; (** instructions for symbolic execution *) mutable nd_kind : nodekind; (** kind of node *) - mutable nd_loc : Sil.location; (** location in the source code *) + mutable nd_loc : Location.t; (** location in the source code *) mutable nd_preds : t list; (** predecessor nodes in the cfg *) mutable nd_proc : proc_desc option; (** proc desc from cil *) mutable nd_succs : t list; (** successor nodes in the cfg *) @@ -42,17 +42,9 @@ module Node = struct and proc_desc = { (** procedure description *) pd_attributes : Sil.proc_attributes; (** attributes of the procedure *) pd_id : int; (** unique proc_desc identifier *) - pd_name : Procname.t; (** name of the procedure *) - pd_is_defined : bool; (** true iff the procedure is defined, and not just declared *) - pd_ret_type : Sil.typ; (** return type *) - pd_formals : (string * Sil.typ) list; (** name and type of formal parameters *) - mutable pd_locals : (Mangled.t * Sil.typ) list; (** name and type of local variables *) - pd_captured : (Mangled.t * Sil.typ) list; (** name and type of blocks' captured variables *) mutable pd_nodes : t list; (** list of nodes of this procedure *) mutable pd_start_node : t; (** start node of this procedure *) mutable pd_exit_node : t; (** exit node of ths procedure *) - mutable pd_loc : Sil.location; (** location of this procedure in the source code *) - mutable pd_flags : proc_flags; (** flags for the procedure *) pd_err_log: Errlog.t; (** error log at translation time *) mutable pd_changed : bool; (** true if proc has changed since last analysis *) } @@ -112,9 +104,9 @@ module Node = struct try list_for_all2 node_eq n1s n2s with Invalid_argument _ -> false in - pd1.pd_is_defined = pd2.pd_is_defined && - Sil.typ_equal pd1.pd_ret_type pd2.pd_ret_type && - formals_eq pd1.pd_formals pd2.pd_formals && + pd1.pd_attributes.Sil.is_defined = pd2.pd_attributes.Sil.is_defined && + Sil.typ_equal pd1.pd_attributes.Sil.ret_type pd2.pd_attributes.Sil.ret_type && + formals_eq pd1.pd_attributes.Sil.formals pd2.pd_attributes.Sil.formals && nodes_eq pd1.pd_nodes pd2.pd_nodes in let old_procs = cfg_old.name_pdesc_tbl in let new_procs = cfg_new.name_pdesc_tbl in @@ -139,12 +131,15 @@ module Node = struct let node_list' = let filter_node node = match node.nd_proc with | None -> true - | Some pdesc -> is_enabled pdesc.pd_name in + | Some pdesc -> is_enabled pdesc.pd_attributes.Sil.proc_name in list_filter filter_node !(cfg.node_list) in let procs_to_remove = let psetr = ref Procname.Set.empty in let do_proc pname pdesc = - if pdesc.pd_is_defined && not (is_enabled pname) && not (in_address_set pname) then psetr := Procname.Set.add pname !psetr in + if pdesc.pd_attributes.Sil.is_defined && + not (is_enabled pname) && + not (in_address_set pname) then + psetr := Procname.Set.add pname !psetr in Procname.Hash.iter do_proc cfg.name_pdesc_tbl; !psetr in let remove_proc pname = @@ -176,16 +171,6 @@ module Node = struct let iter_proc_desc cfg f = Procname.Hash.iter f cfg.name_pdesc_tbl - let iter_types cfg f = - let node_iter_types node = - list_iter (Sil.instr_iter_types f) node.nd_instrs in - let pdesc_iter_types pname pdesc = - Sil.typ_iter_types f pdesc.pd_ret_type; - list_iter (fun (_, t) -> Sil.typ_iter_types f t) pdesc.pd_formals; - list_iter (fun (_, t) -> Sil.typ_iter_types f t) pdesc.pd_locals; - list_iter node_iter_types pdesc.pd_nodes in - iter_proc_desc cfg pdesc_iter_types - let dummy () = { nd_id = 0; nd_dist_exit = None; @@ -194,7 +179,7 @@ module Node = struct nd_dead_pvars_before = []; nd_instrs = []; nd_kind = Skip_node "dummy"; - nd_loc = Sil.loc_none; + nd_loc = Location.loc_none; nd_proc = None; nd_succs = []; nd_preds = []; nd_exn = []; } @@ -399,15 +384,15 @@ module Node = struct node.nd_instrs <- instrs let proc_desc_get_ret_var pdesc = - Sil.get_ret_pvar pdesc.pd_name + Sil.get_ret_pvar pdesc.pd_attributes.Sil.proc_name (** Add declarations for local variables and return variable to the node *) let add_locals_ret_declaration node locals = let loc = get_loc node in let pdesc = get_proc_desc node in - let proc_name = pdesc.pd_name in + let proc_name = pdesc.pd_attributes.Sil.proc_name in let ret_var = - let ret_type = pdesc.pd_ret_type in + let ret_type = pdesc.pd_attributes.Sil.ret_type in (proc_desc_get_ret_var pdesc, ret_type) in let construct_decl (x, typ) = (Sil.mk_pvar x proc_name, typ) in @@ -477,33 +462,33 @@ module Node = struct (** Set a flag for the proc desc *) let proc_desc_set_flag pdesc key value = - proc_flags_add pdesc.pd_flags key value + proc_flags_add pdesc.pd_attributes.Sil.proc_flags key value (** Return the return type of the procedure *) let proc_desc_get_ret_type proc_desc = - proc_desc.pd_ret_type + proc_desc.pd_attributes.Sil.ret_type let proc_desc_get_proc_name proc_desc = - proc_desc.pd_name + proc_desc.pd_attributes.Sil.proc_name (** Return [true] iff the procedure is defined, and not just declared *) let proc_desc_is_defined proc_desc = - proc_desc.pd_is_defined + proc_desc.pd_attributes.Sil.is_defined let proc_desc_get_loc proc_desc = - proc_desc.pd_loc + proc_desc.pd_attributes.Sil.loc (** Return name and type of formal parameters *) let proc_desc_get_formals proc_desc = - proc_desc.pd_formals + proc_desc.pd_attributes.Sil.formals (** Return name and type of local variables *) let proc_desc_get_locals proc_desc = - proc_desc.pd_locals + proc_desc.pd_attributes.Sil.locals (** Return name and type of captured variables *) let proc_desc_get_captured proc_desc = - proc_desc.pd_captured + proc_desc.pd_attributes.Sil.captured let proc_desc_get_nodes proc_desc = proc_desc.pd_nodes @@ -518,11 +503,11 @@ module Node = struct (** Get flags for the proc desc *) let proc_desc_get_flags proc_desc = - proc_desc.pd_flags + proc_desc.pd_attributes.Sil.proc_flags (** Append the locals to the list of local variables *) let proc_desc_append_locals proc_desc new_locals = - proc_desc.pd_locals <- proc_desc.pd_locals @ new_locals + proc_desc.pd_attributes.Sil.locals <- proc_desc.pd_attributes.Sil.locals @ new_locals (** Get the cyclomatic complexity for the procedure *) let proc_desc_get_cyclomatic proc_desc = @@ -543,7 +528,7 @@ module Node = struct | None -> pe0 | Some instr -> pe_extend_colormap pe0 (Obj.repr instr) Red in let instrs = get_instrs node in - let pp_loc fmt () = F.fprintf fmt " %a " Sil.pp_loc (get_loc node) in + let pp_loc fmt () = F.fprintf fmt " %a " Location.pp (get_loc node) in let print_sub_instrs () = F.fprintf fmt "%a" (Sil.pp_instr_list pe) instrs in match get_kind node with | Stmt_node s -> @@ -663,7 +648,7 @@ let load_cfg_from_file (filename : DB.filename) : cfg option = let save_source_files cfg = let process_proc pname pdesc = let loc = Node.proc_desc_get_loc pdesc in - let source_file = loc.Sil.file in + let source_file = loc.Location.file in let source_file_str = DB.source_file_to_abs_path source_file in let dest_file = DB.source_file_in_resdir source_file in let dest_file_str = DB.filename_to_string dest_file in @@ -696,14 +681,7 @@ module Procdesc = struct type proc_desc_builder = { cfg : cfg; - name: Procname.t; - is_defined : bool; (** is defined and not just declared *) proc_attributes : Sil.proc_attributes; - ret_type : Sil.typ; (** return type *) - formals : (string * Sil.typ) list; - locals : (Mangled.t * Sil.typ) list; - captured : (Mangled.t * Sil.typ) list; (** variables captured in an ObjC block *) - loc : Sil.location; } let create (b : proc_desc_builder) = @@ -713,21 +691,13 @@ module Procdesc = struct { pd_attributes = b.proc_attributes; pd_id = !proc_desc_id_counter; - pd_name = b.name; - pd_is_defined = b.is_defined; - pd_ret_type = b.ret_type; - pd_formals = b.formals; - pd_locals = b.locals; - pd_captured = b.captured; - pd_nodes =[]; + pd_nodes = []; pd_start_node = dummy (); pd_exit_node = dummy (); - pd_loc = b.loc; - pd_flags = proc_flags_empty (); pd_err_log = Errlog.empty (); pd_changed = true } in - pdesc_tbl_add b.cfg b.name pdesc; + pdesc_tbl_add b.cfg b.proc_attributes.Sil.proc_name pdesc; pdesc let remove = Node.proc_desc_remove @@ -772,9 +742,6 @@ module NodeSet = Node.NodeSet let iter_proc_desc = Node.iter_proc_desc -(** Iterate over all the types (and subtypes) in the CFG *) -let iter_types = Node.iter_types - let rec pp_node_list f = function | [] -> () | [node] -> Node.pp f node @@ -936,8 +903,8 @@ let remove_abducted_retvars p = let remove_locals (curr_f : Procdesc.t) p = let names_of_locals = list_map (get_name_of_local curr_f) (Procdesc.get_locals curr_f) in - let names_of_locals' = match !Sil.curr_language with - | Sil.C_CPP -> (* in ObjC to deal with block we need to remove static locals *) + let names_of_locals' = match !Config.curr_language with + | Config.C_CPP -> (* in ObjC to deal with block we need to remove static locals *) let names_of_static_locals = get_name_of_objc_static_locals curr_f p in let names_of_block_locals = get_name_of_objc_block_locals p in names_of_block_locals @ names_of_locals @ names_of_static_locals diff --git a/infer/src/backend/cfg.mli b/infer/src/backend/cfg.mli index b4c52b72d..3123b784e 100644 --- a/infer/src/backend/cfg.mli +++ b/infer/src/backend/cfg.mli @@ -33,14 +33,7 @@ module Procdesc : sig type proc_desc_builder = { cfg : cfg; - name: Procname.t; - is_defined : bool; (** is defined and not just declared *) proc_attributes : Sil.proc_attributes; - ret_type : Sil.typ; (** return type *) - formals : (string * Sil.typ) list; - locals : (Mangled.t * Sil.typ) list; - captured : (Mangled.t * Sil.typ) list; (** variables captured in an ObjC block *) - loc : Sil.location; } (** Create a procdesc *) @@ -70,7 +63,7 @@ module Procdesc : sig val get_formals : t -> (string * Sil.typ) list (** Return loc information for the procedure *) - val get_loc : t -> Sil.location + val get_loc : t -> Location.t (** Return name and type of local variables *) val get_locals : t -> (Mangled.t * Sil.typ) list @@ -102,7 +95,7 @@ module Procdesc : sig val iter_nodes : (node -> unit) -> t -> unit (** iterate over the calls from the procedure: (callee,location) pairs *) - val iter_calls : ((Procname.t * Sil.location) -> unit) -> t -> unit + val iter_calls : ((Procname.t * Location.t) -> unit) -> t -> unit (** iterate over all nodes and their instructions *) val iter_instrs : (node -> Sil.instr -> unit) -> t -> unit @@ -173,7 +166,7 @@ module Node : sig (** [create cfg loc kind instrs proc_desc temps] create a new cfg node with the given location, kind, list of instructions, procdesc and list of temporary variables *) - val create : cfg -> Sil.location -> nodekind -> Sil.instr list -> Procdesc.t -> Ident.t list -> t + val create : cfg -> Location.t -> nodekind -> Sil.instr list -> Procdesc.t -> Ident.t list -> t (** create a new empty cfg *) val create_cfg : unit -> cfg @@ -206,10 +199,10 @@ module Node : sig val get_id : t -> int (** Get the source location of the node *) - val get_loc : t -> Sil.location + val get_loc : t -> Location.t (** Get the source location of the last instruction in the node *) - val get_last_loc : t -> Sil.location + val get_last_loc : t -> Location.t (** Get the kind of the current node *) val get_kind : t -> nodekind @@ -263,7 +256,7 @@ module Node : sig val set_kind : t -> nodekind -> unit (** Set the source location of the node *) - val set_loc : t -> Sil.location -> unit + val set_loc : t -> Location.t -> unit (** Set the proc desc associated to the node *) val set_proc_desc : t -> Procdesc.t -> unit @@ -288,9 +281,6 @@ val pp_node_list : Format.formatter -> Node.t list -> unit (** Iterate over all the procdesc's *) val iter_proc_desc : cfg -> (Procname.t -> Procdesc.t -> unit) -> unit -(** Iterate over all the types (and subtypes) in the CFG *) -val iter_types : cfg -> (Sil.typ -> unit) -> unit - (** Get all the procedures (defined and declared) *) val get_all_procs : cfg -> Procdesc.t list diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml index 52c2766bd..64d6c1436 100644 --- a/infer/src/backend/config.ml +++ b/infer/src/backend/config.ml @@ -385,3 +385,13 @@ let unsafe_unret = "<\"Unsafe_unretained\">" let weak = "<\"Weak\">" let assign = "<\"Assign\">" + +(** Programming language. *) +type language = C_CPP | Java + +(** current language *) +let curr_language = ref C_CPP + +let string_of_language = function + | Java -> "Java" + | C_CPP -> "C_CPP" diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 522bdff8d..aab726857 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -970,7 +970,7 @@ let pp_cfgnode fmt (n: Cfg.Node.t) = let print_icfg fmt cfg = let print_node node = let loc = Cfg.Node.get_loc node in - if (!Config.dotty_cfg_libs || DB.source_file_equal loc.Sil.file !DB.current_source) then + if (!Config.dotty_cfg_libs || DB.source_file_equal loc.Location.file !DB.current_source) then F.fprintf fmt "%a\n" pp_cfgnode node in list_iter print_node (Cfg.Node.get_all_nodes cfg) @@ -1353,5 +1353,8 @@ let print_specs_xml signature specs loc fmt = specs in let xml_specifications = Io_infer.Xml.create_tree "specifications" [] list_of_specs_xml in let xml_signature = Io_infer.Xml.create_tree "signature" [("name", signature)] [] in - let proc_summary = Io_infer.Xml.create_tree "procedure" [("file", DB.source_file_to_string loc.Sil.file); ("line", string_of_int loc.Sil.line)] [xml_signature; xml_specifications] in + let proc_summary = Io_infer.Xml.create_tree "procedure" + [("file", DB.source_file_to_string loc.Location.file); + ("line", string_of_int loc.Location.line)] + [xml_signature; xml_specifications] in Io_infer.Xml.pp_document true fmt proc_summary diff --git a/infer/src/backend/dotty.mli b/infer/src/backend/dotty.mli index db61da2ab..f6f46f7c9 100644 --- a/infer/src/backend/dotty.mli +++ b/infer/src/backend/dotty.mli @@ -55,4 +55,5 @@ val reset_node_counter : unit -> unit val prop_to_xml : Prop.normal Prop.t -> string -> int -> Io_infer.Xml.node (** Print a list of specs in XML format *) -val print_specs_xml : string -> Prop.normal Specs.spec list -> Sil.location -> Format.formatter -> unit +val print_specs_xml : + string -> Prop.normal Specs.spec list -> Location.t -> Format.formatter -> unit diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 97ea48559..b9a2c57aa 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -99,7 +99,7 @@ let id_is_assigned_then_dead node id = and return the function name and arguments *) let find_normal_variable_funcall (node: Cfg.Node.t) - (id: Ident.t): (Sil.exp * (Sil.exp list) * Sil.location * Sil.call_flags) option = + (id: Ident.t): (Sil.exp * (Sil.exp list) * Location.t * Sil.call_flags) option = let res = ref None in let node_instrs = Cfg.Node.get_instrs node in let find_declaration = function @@ -213,7 +213,7 @@ let pvar_is_edg_tmp pvar = (** Check whether the program variable is a temporary generated by the front-end *) let pvar_is_frontend_tmp pvar = - if !Sil.curr_language = Sil.Java then pvar_is_sawja_tmp pvar + if !Config.curr_language = Config.Java then pvar_is_sawja_tmp pvar else pvar_is_cil_tmp pvar || pvar_is_edg_tmp pvar (** Find the Letderef instruction used to declare normal variable [id], @@ -685,7 +685,7 @@ let explain_dexp_access prop dexp is_nullable = if !verbose then (L.d_strln "lookup: found Dfcall "); (match c with | Sil.Cfun pn -> (* Treat function as an update *) - Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_call loc.Sil.line)) + Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_call loc.Location.line)) | _ -> None) | de -> if !verbose then (L.d_strln ("lookup: unknown case not matched " ^ Sil.dexp_to_string de)); @@ -700,7 +700,7 @@ let explain_dexp_access prop dexp is_nullable = Some (Localise.Last_accessed (n, is_nullable)) | Some (Sil.Ireturn_from_call n) -> Some (Localise.Returned_from_call n) - | Some Sil.Ialloc when !Sil.curr_language = Sil.Java -> + | Some Sil.Ialloc when !Config.curr_language = Config.Java -> Some Localise.Initialized_automatically | Some inst -> if !verbose then (L.d_strln ("explain_dexp_access: inst is not an update " ^ Sil.inst_to_string inst)); @@ -748,7 +748,7 @@ let create_dereference_desc | _ -> access_opt in let desc = Localise.dereference_string deref_str value_str access_opt' loc in let desc = - if !Sil.curr_language = Sil.C_CPP && not is_premature_nil then + if !Config.curr_language = Config.C_CPP && not is_premature_nil then match de_opt with | Some (Sil.Dpvar pvar) | Some (Sil.Dpvaraddr pvar) -> @@ -1020,7 +1020,7 @@ let explain_null_test_after_dereference exp node line loc = | None -> Localise.no_desc let _warning loc fmt fmt_string = - F.fprintf fmt "%s:%d: Warning: " (DB.source_file_to_string !DB.current_source) loc.Sil.line; + F.fprintf fmt "%s:%d: Warning: " (DB.source_file_to_string !DB.current_source) loc.Location.line; F.fprintf fmt fmt_string (** Print a warning to the out stream, at the given location *) diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index ba57f6291..e142e3390 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -25,7 +25,7 @@ val hpred_is_open_resource : 'a Prop.t -> Sil.hpred -> Sil.resource option (** Find the function call instruction used to initialize normal variable [id], and return the function name and arguments *) val find_normal_variable_funcall : - Cfg.Node.t -> Ident.t -> (Sil.exp * (Sil.exp list) * Sil.location * Sil.call_flags) option + Cfg.Node.t -> Ident.t -> (Sil.exp * (Sil.exp list) * Location.t * Sil.call_flags) option (** Find a program variable assignment in the current node or straightline predecessor. *) val find_program_variable_assignment : Cfg.Node.t -> Sil.pvar -> (Cfg.Node.t * Ident.t) option @@ -47,10 +47,12 @@ val explain_activity_leak : Procname.t -> Sil.typ -> Ident.fieldname -> Localise val explain_allocation_mismatch : Sil.res_action -> Sil.res_action -> Localise.error_desc (** Produce a description of the array access performed in the current instruction, if any. *) -val explain_array_access : Localise.deref_str -> 'a Prop.t -> Sil.location -> Localise.error_desc +val explain_array_access : Localise.deref_str -> 'a Prop.t -> Location.t -> Localise.error_desc (** explain a class cast exception *) -val explain_class_cast_exception : Procname.t option -> Sil.exp -> Sil.exp -> Sil.exp -> Cfg.Node.t -> Sil.location -> Localise.error_desc +val explain_class_cast_exception : + Procname.t option -> Sil.exp -> Sil.exp -> Sil.exp -> + Cfg.Node.t -> Location.t -> Localise.error_desc (** Explain a deallocate stack variable error *) val explain_deallocate_stack_var : Sil.pvar -> Sil.res_action -> Localise.error_desc @@ -61,44 +63,49 @@ val explain_deallocate_constant_string : string -> Sil.res_action -> Localise.er (** Produce a description of which expression is dereferenced in the current instruction, if any. *) val explain_dereference : ?use_buckets:bool -> ?is_nullable:bool -> ?is_premature_nil:bool -> - Localise.deref_str -> 'a Prop.t -> Sil.location -> Localise.error_desc + Localise.deref_str -> 'a Prop.t -> Location.t -> Localise.error_desc (** return a description explaining value [exp] in [prop] in terms of a source expression using the formal parameters of the call *) val explain_dereference_as_caller_expression : ?use_buckets:bool -> Localise.deref_str -> 'a Prop.t -> 'b Prop.t -> Sil.exp -> - Cfg.Node.t -> Sil.location -> Sil.pvar list -> Localise.error_desc + Cfg.Node.t -> Location.t -> Sil.pvar list -> Localise.error_desc (** explain a division by zero *) -val explain_divide_by_zero : Sil.exp -> Cfg.Node.t -> Sil.location -> Localise.error_desc +val explain_divide_by_zero : Sil.exp -> Cfg.Node.t -> Location.t -> Localise.error_desc (** explain a return expression required *) -val explain_return_expression_required : Sil.location -> Sil.typ -> Localise.error_desc +val explain_return_expression_required : Location.t -> Sil.typ -> Localise.error_desc (** explain a comparing floats for equality *) -val explain_comparing_floats_for_equality : Sil.location -> Localise.error_desc +val explain_comparing_floats_for_equality : Location.t -> Localise.error_desc (** explain a condition is an assignment *) -val explain_condition_is_assignment : Sil.location -> Localise.error_desc +val explain_condition_is_assignment : Location.t -> Localise.error_desc (** explain a condition which is always true or false *) -val explain_condition_always_true_false : Sil.Int.t -> Sil.exp -> Cfg.Node.t -> Sil.location -> Localise.error_desc +val explain_condition_always_true_false : + Sil.Int.t -> Sil.exp -> Cfg.Node.t -> Location.t -> Localise.error_desc (** explain the escape of a stack variable address from its scope *) -val explain_stack_variable_address_escape : Sil.location -> Sil.pvar -> Sil.dexp option -> Localise.error_desc +val explain_stack_variable_address_escape : + Location.t -> Sil.pvar -> Sil.dexp option -> Localise.error_desc (** explain a return statement missing *) -val explain_return_statement_missing : Sil.location -> Localise.error_desc +val explain_return_statement_missing : Location.t -> Localise.error_desc (** explain a retain cycle *) -val explain_retain_cycle : Prop.normal Prop.t -> ((Sil.strexp * Sil.typ) * Ident.fieldname * Sil.strexp) list -> Sil.location -> Localise.error_desc +val explain_retain_cycle : + Prop.normal Prop.t -> ((Sil.strexp * Sil.typ) * Ident.fieldname * Sil.strexp) list -> + Location.t -> Localise.error_desc (** explain unary minus applied to unsigned expression *) -val explain_unary_minus_applied_to_unsigned_expression : Sil.exp -> Sil.typ -> Cfg.Node.t -> Sil.location -> Localise.error_desc +val explain_unary_minus_applied_to_unsigned_expression : + Sil.exp -> Sil.typ -> Cfg.Node.t -> Location.t -> Localise.error_desc (** Explain a tainted value error *) -val explain_tainted_value_reaching_sensitive_function : Sil.exp -> Sil.location -> Localise.error_desc +val explain_tainted_value_reaching_sensitive_function : Sil.exp -> Location.t -> Localise.error_desc (** Produce a description of a leak by looking at the current state. If the current instruction is a variable nullify, blame the variable. @@ -107,10 +114,11 @@ val explain_tainted_value_reaching_sensitive_function : Sil.exp -> Sil.location val explain_leak : Sil.tenv -> Sil.hpred -> 'a Prop.t -> Sil.attribute option -> string option -> Exceptions.exception_visibility * Localise.error_desc (** Produce a description of the memory access performed in the current instruction, if any. *) -val explain_memory_access : Localise.deref_str -> 'a Prop.t -> Sil.location -> Localise.error_desc +val explain_memory_access : Localise.deref_str -> 'a Prop.t -> Location.t -> Localise.error_desc (** explain a test for NULL of a dereferenced pointer *) -val explain_null_test_after_dereference : Sil.exp -> Cfg.Node.t -> int -> Sil.location -> Localise.error_desc +val explain_null_test_after_dereference : + Sil.exp -> Cfg.Node.t -> int -> Location.t -> Localise.error_desc (** temporary variable name which is used to create edg native temp variables (see Trans_edg) *) val edg_native_tmp_var_name_prefix : string @@ -125,10 +133,10 @@ val pvar_is_edg_tmp : Sil.pvar -> bool val pvar_is_frontend_tmp : Sil.pvar -> bool (** Print a warning to the out stream, at the given location *) -val warning_out : Sil.location -> ('a, Format.formatter, unit) format -> 'a +val warning_out : Location.t -> ('a, Format.formatter, unit) format -> 'a (** Print a warning to the err stream, at the given location *) -val warning_err : Sil.location -> ('a, Format.formatter, unit) format -> 'a +val warning_err : Location.t -> ('a, Format.formatter, unit) format -> 'a (* offset of an expression found following a program variable *) type pvar_off = diff --git a/infer/src/backend/errlog.ml b/infer/src/backend/errlog.ml index 23a3beee0..24131b822 100644 --- a/infer/src/backend/errlog.ml +++ b/infer/src/backend/errlog.ml @@ -14,7 +14,7 @@ module F = Format (** Element of a loc trace *) type loc_trace_elem = { lt_level : int; (** nesting level of procedure calls *) - lt_loc : Sil.location; (** source location at the current step in the trace *) + lt_loc : Location.t; (** source location at the current step in the trace *) lt_description : string; (** description of the current step in the trace *) lt_node_tags : (string * string) list (** tags describing the node at the current location *) } @@ -24,13 +24,13 @@ type loc_trace = loc_trace_elem list (** Data associated to a specific error *) type err_data = - (int * int) * int * Sil.location * ml_location option * loc_trace * + (int * int) * int * Location.t * ml_location option * loc_trace * Prop.normal Prop.t option * Exceptions.err_class let err_data_compare ((nodeid1, key1), session1, loc1, mloco1, ltr1, po1, ec1) ((nodeid2, key2), session2, loc2, mloco2, ltr2, po2, ec2) = - Sil.loc_compare loc1 loc2 + Location.compare loc1 loc2 module ErrDataSet = (* set err_data with no repeated loc *) Set.Make(struct @@ -64,7 +64,7 @@ let empty () = ErrLogHash.create 13 (** type of the function to be passed to iter *) type iter_fun = - (int * int) -> Sil.location -> Exceptions.err_kind -> bool -> Localise.t -> Localise.error_desc -> + (int * int) -> Location.t -> Exceptions.err_kind -> bool -> Localise.t -> Localise.error_desc -> string -> loc_trace -> Prop.normal Prop.t option -> Exceptions.err_class -> unit (** Apply f to nodes and error names *) @@ -95,7 +95,7 @@ let pp fmt (errlog : t) = let pp_html path_to_root fmt (errlog: t) = let pp_eds fmt eds = let pp_nodeid_session_loc fmt ((nodeid, nodekey), session, loc, mloco, ltr, pre_opt, eclass) = - Io_infer.Html.pp_session_link path_to_root fmt (nodeid, session, loc.Sil.line) in + Io_infer.Html.pp_session_link path_to_root fmt (nodeid, session, loc.Location.line) in ErrDataSet.iter (pp_nodeid_session_loc fmt) eds in let f do_fp ek (ekind, infp, err_name, desc, severity) eds = if ekind == ek && do_fp == infp @@ -157,7 +157,9 @@ let log_issue _ekind err_log loc node_id_key session ltr pre_opt exn = | Some ekind -> ekind | _ -> _ekind in let hide_java_loc_zero = (* hide java errors at location zero unless in -developer_mode *) - !Config.developer_mode = false && !Sil.curr_language = Sil.Java && loc.Sil.line = 0 in + !Config.developer_mode = false && + !Config.curr_language = Config.Java && + loc.Location.line = 0 in let log_it = visibility == Exceptions.Exn_user || (!Config.developer_mode && visibility == Exceptions.Exn_developer) in diff --git a/infer/src/backend/errlog.mli b/infer/src/backend/errlog.mli index caf6543ab..ba9a3ae11 100644 --- a/infer/src/backend/errlog.mli +++ b/infer/src/backend/errlog.mli @@ -12,7 +12,7 @@ (** Element of a loc trace *) type loc_trace_elem = { lt_level : int; (** nesting level of procedure calls *) - lt_loc : Sil.location; (** source location at the current step in the trace *) + lt_loc : Location.t; (** source location at the current step in the trace *) lt_description : string; (** description of the current step in the trace *) lt_node_tags : (string * string) list (** tags describing the node at the current location *) } @@ -28,7 +28,7 @@ val empty : unit -> t (** type of the function to be passed to iter *) type iter_fun = - (int * int) -> Sil.location -> Exceptions.err_kind -> bool -> Localise.t -> Localise.error_desc -> + (int * int) -> Location.t -> Exceptions.err_kind -> bool -> Localise.t -> Localise.error_desc -> string -> loc_trace -> Prop.normal Prop.t option -> Exceptions.err_class -> unit (** Apply f to nodes and error names *) @@ -48,7 +48,7 @@ val update : t -> t -> unit val log_issue : Exceptions.err_kind -> - t -> Sil.location -> (int * int) -> int -> loc_trace -> + t -> Location.t -> (int * int) -> int -> loc_trace -> (Prop.normal Prop.t) option -> exn -> unit (** {2 Functions for manipulating per-file error tables} *) diff --git a/infer/src/backend/exceptions.ml b/infer/src/backend/exceptions.ml index 96c4c51f8..11c5abe6d 100644 --- a/infer/src/backend/exceptions.ml +++ b/infer/src/backend/exceptions.ml @@ -256,8 +256,8 @@ let pp_err (node_id, node_key) loc ekind ex_name desc mloco fmt () = let kind = err_kind_string (if ekind = Kinfo then Kwarning else ekind) (* eclipse does not know about infos: treat as warning *) in let pp_key fmt k = if print_key then F.fprintf fmt " key: %d " k else () in F.fprintf fmt "%s:%d: %s: %a %a%a%a@\n" - (DB.source_file_to_string loc.Sil.file) - loc.Sil.line + (DB.source_file_to_string loc.Location.file) + loc.Location.line kind Localise.pp ex_name Localise.pp_error_desc desc diff --git a/infer/src/backend/exceptions.mli b/infer/src/backend/exceptions.mli index 2e40ca0fc..3617159e7 100644 --- a/infer/src/backend/exceptions.mli +++ b/infer/src/backend/exceptions.mli @@ -91,7 +91,7 @@ val handle_exception : exn -> bool val print_exception_html : string -> exn -> unit (** pretty print an error given its (id,key), location, kind, name, description, and optional ml location *) -val pp_err : int * int -> Sil.location -> err_kind -> Localise.t -> Localise.error_desc -> +val pp_err : int * int -> Location.t -> err_kind -> Localise.t -> Localise.error_desc -> Utils.ml_location option -> Format.formatter -> unit -> unit (** Turn an exception into an error name, error description, diff --git a/infer/src/backend/fork.ml b/infer/src/backend/fork.ml index fa81e55b6..c17b53594 100644 --- a/infer/src/backend/fork.ml +++ b/infer/src/backend/fork.ml @@ -437,7 +437,8 @@ let post_process_procs exe_env procs_done = let check_no_specs pn = if Specs.get_specs pn = [] then begin Errdesc.warning_err - (Specs.get_summary_unsafe pn).Specs.loc "No specs found for %a@." Procname.pp pn + (Specs.get_summary_unsafe pn).Specs.attributes.Sil.loc + "No specs found for %a@." Procname.pp pn end in let cg = Exe_env.get_cg exe_env in list_iter (fun pn -> @@ -581,7 +582,8 @@ let parallel_execution exe_env num_processes analyze_proc filter_out process_res (Specs.get_timestamp (Specs.get_summary_unsafe pname) = 0 || not (proc_is_up_to_date call_graph pname)) in let process_one_proc pname (calls: Cg.in_out_calls) = - DB.current_source := (Specs.get_summary_unsafe pname).Specs.loc.Sil.file; + DB.current_source := + (Specs.get_summary_unsafe pname).Specs.attributes.Sil.loc.Location.file; if !trace then begin let whole_seconds = false in @@ -634,7 +636,8 @@ let parallel_execution exe_env num_processes analyze_proc filter_out process_res | Some (p_str, summ) -> let (pname, weight) = Process.get_last_input p_str in (try - DB.current_source := (Specs.get_summary_unsafe pname).Specs.loc.Sil.file; + DB.current_source := + (Specs.get_summary_unsafe pname).Specs.attributes.Sil.loc.Location.file; process_result exe_env (pname, weight) summ with exn -> assert false); Timing_log.event_finish (Procname.to_string pname); diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml index 622b1000a..1270bde17 100644 --- a/infer/src/backend/inferanalyze.ml +++ b/infer/src/backend/inferanalyze.ml @@ -144,7 +144,7 @@ let arg_desc = "-print_builtins", Arg.Unit SymExec.print_builtins, None, "print the builtin functions and exit"; "-source_path", Arg.String source_path, Some "path", "specify the absolute path to the root of the source files. Used to interpret relative paths when using option -exclude."; (* TODO: merge with the -project_root option *) - "-java", Arg.Unit (fun () -> Sil.curr_language := Sil.Java), None, "Set language to Java"; + "-java", Arg.Unit (fun () -> Config.curr_language := Config.Java), None, "Set language to Java"; "-version", Arg.Unit print_version, None, "print version information and exit"; "-version_json", Arg.Unit print_version_json, None, "print version json formatted"; "-objcm", Arg.Set Config.objc_memory_model_on, None, "Use ObjC memory model"; @@ -207,7 +207,7 @@ let () = (* parse command-line arguments *) module Simulator = struct (** Simulate the analysis only *) let reset_summaries cg = list_iter - (fun (pname, in_out_calls) -> Specs.reset_summary cg pname Sil.loc_none) + (fun (pname, in_out_calls) -> Specs.reset_summary cg pname Location.loc_none) (Cg.get_nodes_and_calls cg) (** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for @@ -838,7 +838,7 @@ let () = let () = match !cluster_cmdline with | None -> - if !Sil.curr_language = Sil.C_CPP then + if !Config.curr_language = Config.C_CPP then Objc_preanal.do_objc_preanalysis (); L.stdout "Starting analysis (Infer version %s)@." Version.versionString; | Some clname -> L.stdout "Cluster %s@." clname in @@ -858,7 +858,7 @@ let () = else !err_file_cmdline in let analyzer_out_of = open_output_file Logging.set_out_formatter analyzer_out_file in let analyzer_err_of = open_output_file Logging.set_err_formatter analyzer_err_file in - if (!Sil.curr_language = Sil.C_CPP) then Mleak_buckets.init_buckets !objc_ml_buckets_arg; + if (!Config.curr_language = Config.C_CPP) then Mleak_buckets.init_buckets !objc_ml_buckets_arg; process_cluster_cmdline_exit (); let source_dirs = diff --git a/infer/src/backend/inferconfig.ml b/infer/src/backend/inferconfig.ml index 22cbaf4e5..9383714d7 100644 --- a/infer/src/backend/inferconfig.ml +++ b/infer/src/backend/inferconfig.ml @@ -168,12 +168,12 @@ module NeverReturnNull = struct let default_source_contains = "" type pattern = - | Method_pattern of Sil.language * method_pattern - | Source_contains of Sil.language * string + | Method_pattern of Config.language * method_pattern + | Source_contains of Config.language * string let language_of_string = function - | "Java" -> Sil.Java - | "C_CPP" -> Sil.C_CPP + | "Java" -> Config.Java + | "C_CPP" -> Config.C_CPP | _ -> failwith ("Unknown language found in " ^ inferconfig_file) let pp_pattern fmt pattern = @@ -197,10 +197,10 @@ module NeverReturnNull = struct match pattern with | Method_pattern (language, mp) -> Format.fprintf fmt "Method pattern (%s) {\n%a}\n" - (Sil.string_of_language language) pp_method_pattern mp + (Config.string_of_language language) pp_method_pattern mp | Source_contains (language, sc) -> Format.fprintf fmt "Source contains (%s) {\n%a}\n" - (Sil.string_of_language language) pp_source_contains sc + (Config.string_of_language language) pp_source_contains sc let detect_language assoc = let rec loop = function @@ -262,7 +262,7 @@ module NeverReturnNull = struct | _ -> assert false let create_method_matcher language m_patterns = - if language <> Sil.Java then assert false + if language <> Config.Java then assert false else if m_patterns = [] then default_matcher diff --git a/infer/src/backend/inferconfig.mli b/infer/src/backend/inferconfig.mli index d127478fc..5e440b128 100644 --- a/infer/src/backend/inferconfig.mli +++ b/infer/src/backend/inferconfig.mli @@ -31,7 +31,7 @@ val create_filters : Utils.analyzer -> filters module NeverReturnNull : sig type matcher = DB.source_file -> Procname.t -> bool - val load_matcher : Sil.language -> matcher + val load_matcher : Config.language -> matcher end (** Load the config file and list the files to report on *) diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index 712043f45..d8cf14799 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -166,7 +166,7 @@ let begin_latex_file fmt = (** Write proc summary to latex file *) let write_summary_latex fname fmt summary = - let proc_name = summary.Specs.proc_name in + let proc_name = Specs.get_proc_name summary in Latex.pp_section fmt ("Analysis of function " ^ (Latex.convert_string (Procname.to_string proc_name))); F.fprintf fmt "@[%a@]" (Specs.pp_summary (pe_latex Black) !whole_seconds) summary @@ -206,8 +206,8 @@ let loc_trace_to_jsonbug_record trace_list ekind = list_map (fun tag -> { tag = fst tag; value = snd tag }) tags_list in let trace_item_to_record trace_item = { level = trace_item.Errlog.lt_level; - filename = DB.source_file_to_string trace_item.Errlog.lt_loc.Sil.file; - line_number = trace_item.Errlog.lt_loc.Sil.line; + filename = DB.source_file_to_string trace_item.Errlog.lt_loc.Location.file; + line_number = trace_item.Errlog.lt_loc.Location.line; description = trace_item.Errlog.lt_description; node_tags = node_tags_to_records trace_item.Errlog.lt_node_tags; } in @@ -245,7 +245,7 @@ type summary_val = (** compute values from summary data to export to csv and xml format *) let summary_values top_proc_set summary = let stats = summary.Specs.stats in - let proc_name = summary.Specs.proc_name in + let proc_name = Specs.get_proc_name summary in let is_top = Procname.Set.mem proc_name top_proc_set in let signature = Specs.get_signature summary in let nodes_nr = list_length summary.Specs.nodes in @@ -284,10 +284,10 @@ let summary_values top_proc_set summary = verr = Errlog.size (fun ekind in_footprint -> ekind = Exceptions.Kerror && in_footprint) stats.Specs.err_log; - vflags = summary.Specs.proc_flags; - vfile = DB.source_file_to_string summary.Specs.loc.Sil.file; - vline = summary.Specs.loc.Sil.line; - vloc = summary.Specs.loc.Sil.nLOC; + vflags = summary.Specs.attributes.Sil.proc_flags; + vfile = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file; + vline = summary.Specs.attributes.Sil.loc.Location.line; + vloc = summary.Specs.attributes.Sil.loc.Location.nLOC; vtop = if is_top then "Y" else "N"; vsignature = signature; vweight = nodes_nr; @@ -414,8 +414,8 @@ module BugsCsv = struct Escape.escape_csv s in let kind = Exceptions.err_kind_string ekind in let type_str = Localise.to_string error_name in - let procedure_id = Procname.to_filename summary.Specs.proc_name in - let filename = DB.source_file_to_string summary.Specs.loc.Sil.file in + let procedure_id = Procname.to_filename (Specs.get_proc_name summary) in + let filename = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file in let always_report = match Localise.error_desc_extract_tag_value error_desc "always_report" with | "" -> "false" @@ -428,8 +428,8 @@ module BugsCsv = struct pp "%s," type_str; pp "\"%s\"," err_desc_string; pp "%s," severity; - pp "%d," loc.Sil.line; - pp "\"%s\"," (Escape.escape_csv (Procname.to_string summary.Specs.proc_name)); + pp "%d," loc.Location.line; + pp "\"%s\"," (Escape.escape_csv (Procname.to_string (Specs.get_proc_name summary))); pp "\"%s\"," (Escape.escape_csv procedure_id); pp "%s," filename; pp "\"%s\"," (Escape.escape_csv trace); @@ -455,16 +455,16 @@ module BugsJson = struct if in_footprint && error_filter error_desc error_name then let kind = Exceptions.err_kind_string ekind in let bug_type = Localise.to_string error_name in - let procedure_id = Procname.to_filename summary.Specs.proc_name in - let file = DB.source_file_to_string summary.Specs.loc.Sil.file in + let procedure_id = Procname.to_filename (Specs.get_proc_name summary) in + let file = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file in let bug = { bug_class = Exceptions.err_class_string eclass; kind = kind; bug_type = bug_type; qualifier = error_desc_to_plain_string error_desc; severity = severity; - line = loc.Sil.line; - procedure = Procname.to_string summary.Specs.proc_name; + line = loc.Location.line; + procedure = Procname.to_string (Specs.get_proc_name summary); procedure_id = procedure_id; file = file; bug_trace = loc_trace_to_jsonbug_record ltr ekind; @@ -511,8 +511,8 @@ module BugsXml = struct | None -> "" in Io_infer.Xml.create_tree Io_infer.Xml.tag_loc [("num", string_of_int !num)] [(level_to_xml lt.Errlog.lt_level); - (file_to_xml (DB.source_file_to_string loc.Sil.file)); - (line_to_xml loc.Sil.line); + (file_to_xml (DB.source_file_to_string loc.Location.file)); + (line_to_xml loc.Location.line); (code_to_xml code); (description_to_xml lt.Errlog.lt_description); (node_tags_to_xml lt.Errlog.lt_node_tags)] in @@ -537,10 +537,11 @@ module BugsXml = struct incr xml_bugs_id; let attributes = [("id", string_of_int !xml_bugs_id) ] in let error_class = Exceptions.err_class_string eclass in - let error_line = string_of_int loc.Sil.line in - let procedure_name = Procname.to_string summary.Specs.proc_name in - let procedure_id = Procname.to_filename summary.Specs.proc_name in - let filename = DB.source_file_to_string summary.Specs.loc.Sil.file in + let error_line = string_of_int loc.Location.line in + let proc_name = Specs.get_proc_name summary in + let procedure_name = Procname.to_string proc_name in + let procedure_id = Procname.to_filename proc_name in + let filename = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file in let bug_hash = get_bug_hash kind type_str procedure_id filename node_key error_desc in let forest = [ @@ -582,14 +583,14 @@ module CallsCsv = struct let pp_calls fname fmt summary = let pp x = F.fprintf fmt x in let stats = summary.Specs.stats in - let caller_name = summary.Specs.proc_name in + let caller_name = Specs.get_proc_name summary in let do_call (callee_name, loc) trace = pp "\"%s\"," (Escape.escape_csv (Procname.to_string caller_name)); pp "\"%s\"," (Escape.escape_csv (Procname.to_filename caller_name)); pp "\"%s\"," (Escape.escape_csv (Procname.to_string callee_name)); pp "\"%s\"," (Escape.escape_csv (Procname.to_filename callee_name)); - pp "%s," (DB.source_file_to_string summary.Specs.loc.Sil.file); - pp "%d," loc.Sil.line; + pp "%s," (DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file); + pp "%d," loc.Location.line; pp "%a@\n" Specs.CallStats.pp_trace trace in Specs.CallStats.iter do_call stats.Specs.call_stats end @@ -604,8 +605,10 @@ module UnitTest = struct let fmt = F.std_formatter in let do_spec spec = incr cnt; - let c_file = Filename.basename (DB.source_file_to_string summary.Specs.loc.Sil.file) in - let code = Autounit.genunit c_file proc_name !cnt summary.Specs.formals spec in + let c_file = Filename.basename + (DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file) in + let code = + Autounit.genunit c_file proc_name !cnt (Specs.get_formals summary) spec in F.fprintf fmt "%a@." Autounit.pp_code code in let specs = Specs.get_specs_from_payload summary in list_iter do_spec specs; @@ -639,7 +642,7 @@ end = struct let top_set x = Procname.Set.diff x.possible x.impossible let process_summary x (_, summary) = - let proc_name = summary.Specs.proc_name in + let proc_name = Specs.get_proc_name summary in let nspecs = list_length (Specs.get_specs_from_payload summary) in if nspecs > 0 then begin @@ -678,10 +681,10 @@ module Stats = struct } let process_loc loc stats = - try Hashtbl.find stats.files loc.Sil.file + try Hashtbl.find stats.files loc.Location.file with Not_found -> - stats.nLOC <- stats.nLOC + loc.Sil.nLOC; - Hashtbl.add stats.files loc.Sil.file () + stats.nLOC <- stats.nLOC + loc.Location.nLOC; + Hashtbl.add stats.files loc.Location.file () let loc_trace_to_string_list linereader indent_num ltr = let res = ref [] in @@ -701,7 +704,7 @@ module Stats = struct let line = let pp fmt () = if description <> "" then F.fprintf fmt "%s%04s // %s@\n" (indent_string (level + indent_num)) " " description; - F.fprintf fmt "%s%04d: %s" (indent_string (level + indent_num)) loc.Sil.line code in + F.fprintf fmt "%s%04d: %s" (indent_string (level + indent_num)) loc.Location.line code in pp_to_string pp () in res := line :: "" :: !res in list_iter loc_to_string ltr; @@ -718,7 +721,8 @@ module Stats = struct stats.nerrors <- stats.nerrors + 1; let error_strs = let pp1 fmt () = F.fprintf fmt "%d: %s" stats.nerrors type_str in - let pp2 fmt () = F.fprintf fmt " %s:%d" (DB.source_file_to_string loc.Sil.file) loc.Sil.line in + let pp2 fmt () = F.fprintf fmt " %s:%d" + (DB.source_file_to_string loc.Location.file) loc.Location.line in let pp3 fmt () = F.fprintf fmt " (%a)" Localise.pp_error_desc error_desc in [pp_to_string pp1 (); pp_to_string pp2 (); pp_to_string pp3 ()] in let trace = loc_trace_to_string_list linereader 1 ltr in @@ -740,7 +744,7 @@ module Stats = struct if is_verified then stats.nverified <- stats.nverified + 1; if is_checked then stats.nchecked <- stats.nchecked + 1; if is_defective then stats.ndefective <- stats.ndefective + 1; - process_loc summary.Specs.loc stats + process_loc summary.Specs.attributes.Sil.loc stats let num_files stats = Hashtbl.length stats.files @@ -805,7 +809,7 @@ end (** Process a summary *) let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fname, summary) = - let proc_name = summary.Specs.proc_name in + let proc_name = Specs.get_proc_name summary in let base = DB.chop_extension (DB.filename_from_string fname) in let pp_simple_saved = !Config.pp_simple in Config.pp_simple := true; @@ -814,7 +818,7 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna let error_filter error_desc error_name = let always_report () = Localise.error_desc_extract_tag_value error_desc "always_report" = "true" in - (filters.Inferconfig.path_filter summary.Specs.loc.Sil.file + (filters.Inferconfig.path_filter summary.Specs.attributes.Sil.loc.Location.file || always_report ()) && filters.Inferconfig.error_filter error_name in do_outf procs_csv (fun outf -> F.fprintf outf.fmt "%a" (ProcsCsv.pp_summary fname top_proc_set) summary); @@ -851,7 +855,9 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna begin let xml_out = ref (create_outfile (DB.filename_to_string xml_file)) in do_outf xml_out (fun outf -> - Dotty.print_specs_xml (Specs.get_signature summary) specs summary.Specs.loc outf.fmt; + Dotty.print_specs_xml + (Specs.get_signature summary) + specs summary.Specs.attributes.Sil.loc outf.fmt; close_outf outf) end end @@ -900,8 +906,14 @@ module AnalysisResults = struct summaries := (fname, summary) :: !summaries in apply_without_gc (list_iter load_file) spec_files_from_cmdline; let summ_cmp (fname1, summ1) (fname2, summ2) = - let n = DB.source_file_compare summ1.Specs.loc.Sil.file summ2.Specs.loc.Sil.file in - if n <> 0 then n else int_compare summ1.Specs.loc.Sil.line summ2.Specs.loc.Sil.line in + let n = + DB.source_file_compare + summ1.Specs.attributes.Sil.loc.Location.file + summ2.Specs.attributes.Sil.loc.Location.file in + if n <> 0 then n + else int_compare + summ1.Specs.attributes.Sil.loc.Location.line + summ2.Specs.attributes.Sil.loc.Location.line in list_sort summ_cmp !summaries (** Create an iterator which loads spec files one at a time *) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 41ed204b3..40ddf8d70 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -438,10 +438,16 @@ let check_assignement_guard node = | Cfg.Node.Prune_node(_) -> true | _ -> false) succs in let succs_same_loc_as_node () = - if verbose then (L.d_str ("LOCATION NODE: line: "^(string_of_int l_node.Sil.line)^" nLOC: "^(string_of_int l_node.Sil.nLOC)); L.d_strln " "); + if verbose then + (L.d_str ("LOCATION NODE: line: " ^ (string_of_int l_node.Location.line) ^ + " nLOC: " ^ (string_of_int l_node.Location.nLOC)); + L.d_strln " "); list_for_all (fun l -> - if verbose then (L.d_str ("LOCATION l: line: "^(string_of_int l.Sil.line)^" nLOC: "^(string_of_int l.Sil.nLOC)); L.d_strln " "); - Sil.loc_equal l l_node) succs_loc in + if verbose then + (L.d_str ("LOCATION l: line: " ^ (string_of_int l.Location.line) ^ + " nLOC: " ^ (string_of_int l.Location.nLOC)); + L.d_strln " "); + Location.equal l l_node) succs_loc in let succs_have_simple_guards () = (* check that the guards of the succs are a var or its negation *) let check_instr = function | Sil.Prune (Sil.Var _, _, _, _) -> true @@ -451,11 +457,17 @@ let check_assignement_guard node = let check_guard n = list_for_all check_instr (Cfg.Node.get_instrs n) in list_for_all check_guard succs in - if !Sil.curr_language = Sil.C_CPP && succs_are_all_prune_nodes () && succs_same_loc_as_node () && succs_have_simple_guards () then + if !Config.curr_language = Config.C_CPP && + succs_are_all_prune_nodes () && + succs_same_loc_as_node () && + succs_have_simple_guards () then (let instr = Cfg.Node.get_instrs node in match succs_loc with | loc_succ:: _ -> (* at this point all successors are at the same location, so we can take the first*) - let set_instr_at_succs_loc = list_filter (fun i -> (Sil.loc_equal (Sil.instr_get_loc i) loc_succ) && is_set_instr i) instr in + let set_instr_at_succs_loc = + list_filter + (fun i -> (Location.equal (Sil.instr_get_loc i) loc_succ) && is_set_instr i) + instr in (match set_instr_at_succs_loc with | [Sil.Set(e, _, _, _)] -> (* we now check if e is the same expression used to prune*) if (is_prune_exp e) && not ((node_contains_call node) && (is_cil_tmp e)) && not (is_edg_tmp e) then ( @@ -657,7 +669,7 @@ let compute_visited vset = let node_get_all_lines n = let node_loc = Cfg.Node.get_loc n in let instrs_loc = list_map Sil.instr_get_loc (Cfg.Node.get_instrs n) in - let lines = list_map (fun loc -> loc.Sil.line) (node_loc :: instrs_loc) in + let lines = list_map (fun loc -> loc.Location.line) (node_loc :: instrs_loc) in list_remove_duplicates int_compare (list_sort int_compare lines) in let do_node n = res := Specs.Visitedset.add (Cfg.Node.get_id n, node_get_all_lines n) !res in Cfg.NodeSet.iter do_node vset; @@ -680,7 +692,8 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list = (* let () = L.out "@.AFTER abs:@.$%a@." (Prop.pp_prop Utils.pe_text) prop'' in *) let pre, post = Prop.extract_spec prop'' in let pre' = Prop.normalize (Prop.prop_sub sub pre) in - if !Sil.curr_language = Sil.Java then report_activity_leaks pname (Prop.get_sigma post) tenv; + if !Config.curr_language = Config.Java then + report_activity_leaks pname (Prop.get_sigma post) tenv; let post' = if Prover.check_inconsistency_base prop then None else Some (Prop.normalize (Prop.prop_sub sub post), path) in @@ -750,9 +763,9 @@ let create_seed_vars sigma = let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Prop.t = let sigma_new_formals = let do_formal (pv, typ) = - let texp = match !Sil.curr_language with - | Sil.C_CPP -> Sil.Sizeof (typ, Sil.Subtype.exact) - | Sil.Java -> Sil.Sizeof (typ, Sil.Subtype.subtypes) in + let texp = match !Config.curr_language with + | Config.C_CPP -> Sil.Sizeof (typ, Sil.Subtype.exact) + | Config.Java -> Sil.Sizeof (typ, Sil.Subtype.subtypes) in Prop.mk_ptsto_lvar (Some tenv) Prop.Fld_init Sil.inst_formal (pv, texp, None) in list_map do_formal new_formals in let sigma_seed = @@ -970,7 +983,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t let set_current_language cfg proc_desc = let language = (Cfg.Procdesc.get_attributes proc_desc).Sil.language in - Sil.curr_language := language + Config.curr_language := language (** reset counters before analysing a procedure *) let reset_global_counters cfg proc_name proc_desc = @@ -994,10 +1007,10 @@ let exception_preconditions tenv pname summary = | None -> errors | Some e -> (pre, e) :: errors in let collect_spec errors spec = - match !Sil.curr_language with - | Sil.Java -> + match !Config.curr_language with + | Config.Java -> list_fold_left (collect_exceptions spec.Specs.pre) errors spec.Specs.posts - | Sil.C_CPP -> + | Config.C_CPP -> list_fold_left (collect_errors spec.Specs.pre) errors spec.Specs.posts in list_fold_left collect_spec [] (Specs.get_specs_from_payload summary) @@ -1096,7 +1109,7 @@ let analyze_proc exe_env (proc_name: Procname.t) : Specs.summary = let prev_summary = Specs.get_summary_unsafe proc_name in let updated_summary = update_summary prev_summary specs proc_name elapsed res in - if (!Sil.curr_language <> Sil.Java && Config.report_assertion_failure) + if (!Config.curr_language <> Config.Java && Config.report_assertion_failure) || !Config.report_runtime_exceptions then report_runtime_exceptions tenv cfg proc_desc updated_summary; updated_summary @@ -1214,9 +1227,6 @@ let do_analysis exe_env = let pdesc = match Cfg.Procdesc.find_from_name cfg pname with | Some pdesc -> pdesc | None -> assert false in - let ret_type = Cfg.Procdesc.get_ret_type pdesc in - let formals = Cfg.Procdesc.get_formals pdesc in - let loc = Cfg.Procdesc.get_loc pdesc in let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes pdesc) in let proc_flags = Cfg.Procdesc.get_flags pdesc in let static_err_log = Cfg.Procdesc.get_err_log pdesc in (** err log from translation *) @@ -1226,7 +1236,7 @@ let do_analysis exe_env = Callbacks.proc_inline_synthetic_methods cfg pdesc; Specs.init_summary - (pname, ret_type, formals, dep, loc, nodes, proc_flags, + (dep, nodes, proc_flags, static_err_log, calls, cyclomatic, None, attributes) in let filter = if !Config.only_skips then (filter_skipped_procs cg procs_and_defined_children) diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml index 8b541fbc8..a7d80e109 100644 --- a/infer/src/backend/localise.ml +++ b/infer/src/backend/localise.ml @@ -196,11 +196,11 @@ let error_desc_hash desc = let error_desc_equal desc1 desc2 = (desc_get_comparable desc1) = (desc_get_comparable desc2) let _line_tag tags tag loc = - let line_str = string_of_int loc.Sil.line in + let line_str = string_of_int loc.Location.line in Tags.add tags tag line_str; let s = "line " ^ line_str in - if (loc.Sil.col != -1) then - let col_str = string_of_int loc.Sil.col in + if (loc.Location.col != -1) then + let col_str = string_of_int loc.Location.col in s ^ ", column " ^ col_str else s @@ -241,7 +241,7 @@ type deref_str = problem_str: string; (** description of the problem *) } let pointer_or_object () = - if !Sil.curr_language = Sil.Java then "object" else "pointer" + if !Config.curr_language = Config.Java then "object" else "pointer" let _deref_str_null proc_name_opt _problem_str tags = let problem_str = match proc_name_opt with @@ -466,7 +466,7 @@ let desc_allocation_mismatch alloc dealloc = else Tags.dealloc_function, Tags.dealloc_call, Tags.dealloc_line in Tags.add tags tag_fun (Procname.to_simplified_string primitive_pname); Tags.add tags tag_call (Procname.to_simplified_string called_pname); - Tags.add tags tag_line (string_of_int loc.Sil.line); + Tags.add tags tag_line (string_of_int loc.Location.line); let by_call = if Procname.equal primitive_pname called_pname then "" else " by call to " ^ Procname.to_simplified_string called_pname in diff --git a/infer/src/backend/localise.mli b/infer/src/backend/localise.mli index 412e1e3c7..0ad86de6b 100644 --- a/infer/src/backend/localise.mli +++ b/infer/src/backend/localise.mli @@ -131,7 +131,7 @@ val deref_str_null : Procname.t option -> deref_str val deref_str_nullable : Procname.t option -> string -> deref_str (** dereference strings for an undefined value coming from the given procedure *) -val deref_str_undef : Procname.t * Sil.location -> deref_str +val deref_str_undef : Procname.t * Location.t -> deref_str (** dereference strings for a freed pointer dereference *) val deref_str_freed : Sil.res_action -> deref_str @@ -158,7 +158,7 @@ type access = | Initialized_automatically | Returned_from_call of int -val dereference_string : deref_str -> string -> access option -> Sil.location -> error_desc +val dereference_string : deref_str -> string -> access option -> Location.t -> error_desc val parameter_field_not_null_checked_desc : error_desc -> Sil.exp -> error_desc @@ -168,56 +168,63 @@ val is_field_not_null_checked_desc : error_desc -> bool val is_parameter_field_not_null_checked_desc : error_desc -> bool -val desc_allocation_mismatch : Procname.t * Procname.t * Sil.location -> Procname.t * Procname.t * Sil.location -> error_desc +val desc_allocation_mismatch : + Procname.t * Procname.t * Location.t -> Procname.t * Procname.t * Location.t -> error_desc -val desc_class_cast_exception : Procname.t option -> string -> string -> string option -> Sil.location -> error_desc +val desc_class_cast_exception : + Procname.t option -> string -> string -> string option -> Location.t -> error_desc -val desc_comparing_floats_for_equality : Sil.location -> error_desc +val desc_comparing_floats_for_equality : Location.t -> error_desc -val desc_condition_is_assignment : Sil.location -> error_desc +val desc_condition_is_assignment : Location.t -> error_desc -val desc_condition_always_true_false : Sil.Int.t -> string option -> Sil.location -> error_desc +val desc_condition_always_true_false : Sil.Int.t -> string option -> Location.t -> error_desc -val desc_deallocate_stack_variable : string -> Procname.t -> Sil.location -> error_desc +val desc_deallocate_stack_variable : string -> Procname.t -> Location.t -> error_desc -val desc_deallocate_static_memory : string -> Procname.t -> Sil.location -> error_desc +val desc_deallocate_static_memory : string -> Procname.t -> Location.t -> error_desc -val desc_divide_by_zero : string -> Sil.location -> error_desc +val desc_divide_by_zero : string -> Location.t -> error_desc -val desc_leak : string option -> Sil.resource option -> Sil.res_action option -> Sil.location -> string option -> error_desc +val desc_leak : + string option -> Sil.resource option -> Sil.res_action option -> + Location.t -> string option -> error_desc -val desc_null_test_after_dereference : string -> int -> Sil.location -> error_desc +val desc_null_test_after_dereference : string -> int -> Location.t -> error_desc val java_unchecked_exn_desc : Procname.t -> Mangled.t -> string -> error_desc val desc_activity_leak : Procname.t -> Sil.typ -> Ident.fieldname -> error_desc (* Create human-readable error description for assertion failures *) -val desc_assertion_failure : Sil.location -> error_desc +val desc_assertion_failure : Location.t -> error_desc (** kind of precondition not met *) type pnm_kind = | Pnm_bounds | Pnm_dangling -val desc_precondition_not_met : pnm_kind option -> Procname.t -> Sil.location -> error_desc +val desc_precondition_not_met : pnm_kind option -> Procname.t -> Location.t -> error_desc -val desc_return_expression_required : string -> Sil.location -> error_desc +val desc_return_expression_required : string -> Location.t -> error_desc -val desc_retain_cycle : Prop.normal Prop.t -> ((Sil.strexp * Sil.typ) * Ident.fieldname * Sil.strexp) list -> Sil.location -> error_desc +val desc_retain_cycle : + Prop.normal Prop.t -> ((Sil.strexp * Sil.typ) * Ident.fieldname * Sil.strexp) list -> + Location.t -> error_desc -val desc_return_statement_missing : Sil.location -> error_desc +val desc_return_statement_missing : Location.t -> error_desc -val desc_return_value_ignored : Procname.t -> Sil.location -> error_desc +val desc_return_value_ignored : Procname.t -> Location.t -> error_desc -val desc_stack_variable_address_escape : string -> string option -> Sil.location -> error_desc +val desc_stack_variable_address_escape : string -> string option -> Location.t -> error_desc val desc_skip_function : Procname.t -> error_desc val desc_inherently_dangerous_function : Procname.t -> error_desc -val desc_unary_minus_applied_to_unsigned_expression : string option -> string -> Sil.location -> error_desc +val desc_unary_minus_applied_to_unsigned_expression : + string option -> string -> Location.t -> error_desc -val desc_tainted_value_reaching_sensitive_function : string -> Sil.location -> error_desc +val desc_tainted_value_reaching_sensitive_function : string -> Location.t -> error_desc -val desc_uninitialized_dangling_pointer_deref : deref_str -> string -> Sil.location -> error_desc +val desc_uninitialized_dangling_pointer_deref : deref_str -> string -> Location.t -> error_desc diff --git a/infer/src/backend/location.ml b/infer/src/backend/location.ml new file mode 100644 index 000000000..1cca459fa --- /dev/null +++ b/infer/src/backend/location.ml @@ -0,0 +1,55 @@ +(* + * Copyright (c) 2015 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open Utils +module F = Format +module L = Logging + +(** Location in the original source file *) +type t = { + line: int; (** The line number. -1 means "do not know" *) + col: int; (** The column number. -1 means "do not know" *) + file: DB.source_file; (** The name of the source file *) + nLOC : int; (** Lines of code in the source file *) +} + +let compare loc1 loc2 = + let n = int_compare loc1.line loc2.line in + if n <> 0 then n else DB.source_file_compare loc1.file loc2.file + +(** Dump a location *) +let d (loc: t) = L.add_print_action (L.PTloc, Obj.repr loc) + +let dummy = { + line = -1; + col = -1; + file = DB.source_file_empty; + nLOC = -1; +} + +let equal loc1 loc2 = + compare loc1 loc2 = 0 + +(** Unknown location *) +let loc_none = { + line = - 1; + col = - 1; + file = DB.source_file_empty; + nLOC = 0; +} + +(** Pretty print a location *) +let pp f (loc: t) = + F.fprintf f "[line %d]" loc.line + +let to_string loc = + let s = (string_of_int loc.line) in + if (loc.col != -1) then + s ^":"^(string_of_int loc.col) + else s diff --git a/infer/src/backend/location.mli b/infer/src/backend/location.mli new file mode 100644 index 000000000..f6922f246 --- /dev/null +++ b/infer/src/backend/location.mli @@ -0,0 +1,34 @@ +(* + * Copyright (c) 2015 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +(** Location in the original source file *) +type t = { + line: int; (** The line number. -1 means "do not know" *) + col: int; (** The column number. -1 means "do not know" *) + file: DB.source_file; (** The name of the source file *) + nLOC : int; (** Lines of code in the source file *) +} + +val compare : t -> t -> int + +(** Dump a location. *) +val d : t -> unit + +val dummy : t + +val equal : t -> t -> bool + +(** Unknown location *) +val loc_none : t + +(** Pretty print a location. *) +val pp : Format.formatter -> t -> unit + +(** String representation of a location. *) +val to_string : t -> string diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml index 97f0e76c1..ffcd2bf0d 100644 --- a/infer/src/backend/paths.ml +++ b/infer/src/backend/paths.ml @@ -471,7 +471,7 @@ end = struct iter_longest_sequence g pos_opt path; let compare lt1 lt2 = let n = int_compare lt1.Errlog.lt_level lt2.Errlog.lt_level in - if n <> 0 then n else Sil.loc_compare lt1.Errlog.lt_loc lt2.Errlog.lt_loc in + if n <> 0 then n else Location.compare lt1.Errlog.lt_loc lt2.Errlog.lt_loc in let relevant lt = lt.Errlog.lt_node_tags <> [] in list_remove_irrelevant_duplicates compare relevant (list_rev !trace) (* list_remove_duplicates compare (list_sort compare !trace) *) diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index f008aa12e..7d60d5bf9 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -38,7 +38,8 @@ let html_formatter = ref F.std_formatter (** Print information when starting and finishing the processing of a node *) module Log_nodes : sig - val start_node : int -> Sil.location -> Procname.t -> Cfg.node list -> Cfg.node list -> Cfg.node list -> bool + val start_node : + int -> Location.t -> Procname.t -> Cfg.node list -> Cfg.node list -> Cfg.node list -> bool val finish_node : int -> unit end = struct let log_files = Hashtbl.create 11 @@ -56,14 +57,32 @@ end = struct html_formatter := fmt; Hashtbl.replace log_files (node_fname, !DB.current_source) fd; if needs_initialization then - (F.fprintf fmt "

Cfg Node %a

" (Io_infer.Html.pp_line_link ~text: (Some (string_of_int nodeid)) [".."]) loc.Sil.line; - F.fprintf fmt "PROC: %a LINE:%a\n" (Io_infer.Html.pp_proc_link [".."] proc_name) (Escape.escape_xml (Procname.to_string proc_name)) (Io_infer.Html.pp_line_link [".."]) loc.Sil.line; + (F.fprintf fmt "

Cfg Node %a

" + (Io_infer.Html.pp_line_link ~text: (Some (string_of_int nodeid)) [".."]) + loc.Location.line; + F.fprintf fmt "PROC: %a LINE:%a\n" + (Io_infer.Html.pp_proc_link [".."] proc_name) + (Escape.escape_xml (Procname.to_string proc_name)) + (Io_infer.Html.pp_line_link [".."]) loc.Location.line; F.fprintf fmt "
PREDS:@\n"; - list_iter (fun node -> Io_infer.Html.pp_node_link [".."] "" (list_map Cfg.Node.get_id (Cfg.Node.get_preds node)) (list_map Cfg.Node.get_id (Cfg.Node.get_succs node)) (list_map Cfg.Node.get_id (Cfg.Node.get_exn node)) (is_visited node) false fmt (Cfg.Node.get_id node)) preds; + list_iter (fun node -> + Io_infer.Html.pp_node_link [".."] "" + (list_map Cfg.Node.get_id (Cfg.Node.get_preds node)) + (list_map Cfg.Node.get_id (Cfg.Node.get_succs node)) + (list_map Cfg.Node.get_id (Cfg.Node.get_exn node)) + (is_visited node) false fmt (Cfg.Node.get_id node)) preds; F.fprintf fmt "
SUCCS: @\n"; - list_iter (fun node -> Io_infer.Html.pp_node_link [".."] "" (list_map Cfg.Node.get_id (Cfg.Node.get_preds node)) (list_map Cfg.Node.get_id (Cfg.Node.get_succs node)) (list_map Cfg.Node.get_id (Cfg.Node.get_exn node)) (is_visited node) false fmt (Cfg.Node.get_id node)) succs; + list_iter (fun node -> Io_infer.Html.pp_node_link [".."] "" + (list_map Cfg.Node.get_id (Cfg.Node.get_preds node)) + (list_map Cfg.Node.get_id (Cfg.Node.get_succs node)) + (list_map Cfg.Node.get_id (Cfg.Node.get_exn node)) + (is_visited node) false fmt (Cfg.Node.get_id node)) succs; F.fprintf fmt "
EXN: @\n"; - list_iter (fun node -> Io_infer.Html.pp_node_link [".."] "" (list_map Cfg.Node.get_id (Cfg.Node.get_preds node)) (list_map Cfg.Node.get_id (Cfg.Node.get_succs node)) (list_map Cfg.Node.get_id (Cfg.Node.get_exn node)) (is_visited node) false fmt (Cfg.Node.get_id node)) exn; + list_iter (fun node -> Io_infer.Html.pp_node_link [".."] "" + (list_map Cfg.Node.get_id (Cfg.Node.get_preds node)) + (list_map Cfg.Node.get_id (Cfg.Node.get_succs node)) + (list_map Cfg.Node.get_id (Cfg.Node.get_exn node)) + (is_visited node) false fmt (Cfg.Node.get_id node)) exn; F.fprintf fmt "
@\n"; F.pp_print_flush fmt (); true @@ -117,8 +136,8 @@ let force_delayed_print fmt = let (jp: Prop.normal Specs.Jprop.t) = Obj.obj jp in Specs.Jprop.pp_short pe_default fmt jp | (L.PTloc, loc) -> - let (loc: Sil.location) = Obj.obj loc in - Sil.pp_loc fmt loc + let (loc: Location.t) = Obj.obj loc in + Location.pp fmt loc | (L.PTnode_instrs, b_n) -> let (b: bool), (io: Sil.instr option), (n: Cfg.node) = Obj.obj b_n in if !Config.write_html then F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Green (Cfg.Node.pp_instr (pe_html Green) io ~sub_instrs: b) n Io_infer.Html.pp_end_color () @@ -217,11 +236,14 @@ let force_delayed_prints () = Config.forcing_delayed_prints := false (** Start a session, and create a new html fine for the node if it does not exist yet *) -let _start_session node (loc: Sil.location) proc_name session = +let _start_session node (loc: Location.t) proc_name session = let node_id = Cfg.Node.get_id node in (if Log_nodes.start_node node_id loc proc_name (Cfg.Node.get_preds node) (Cfg.Node.get_succs node) (Cfg.Node.get_exn node) then F.fprintf !html_formatter "%a@[%a@]%a" Io_infer.Html.pp_start_color Green (Cfg.Node.pp_instr (pe_html Green) None ~sub_instrs: true) node Io_infer.Html.pp_end_color ()); - F.fprintf !html_formatter "%a%a" Io_infer.Html.pp_hline () (Io_infer.Html.pp_session_link ~with_name: true [".."]) (node_id, session, loc.Sil.line); + F.fprintf !html_formatter "%a%a" + Io_infer.Html.pp_hline () + (Io_infer.Html.pp_session_link ~with_name: true [".."]) + (node_id, session, loc.Location.line); F.fprintf !html_formatter "%a" Io_infer.Html.pp_start_color Black let start_session node loc proc_name session = @@ -241,7 +263,7 @@ let _proc_write_log whole_seconds cfg pname = match Cfg.Procdesc.find_from_name cfg pname with | Some pdesc -> let nodes = list_sort Cfg.Node.compare (Cfg.Procdesc.get_nodes pdesc) in - let linenum = (Cfg.Node.get_loc (list_hd nodes)).Sil.line in + let linenum = (Cfg.Node.get_loc (list_hd nodes)).Location.line in let fd, fmt = Io_infer.Html.create DB.Results_dir.Abs_source_dir [Procname.to_filename pname] in F.fprintf fmt "

Procedure %a

@\n" @@ -272,10 +294,10 @@ let create_errors_per_line err_log = let err_str = Localise.to_string err_name ^ " " ^ (pp_to_string Localise.pp_error_desc desc) in (* if in_footprint then *) try - let set = Hashtbl.find err_per_line loc.Sil.line in - Hashtbl.replace err_per_line loc.Sil.line (StringSet.add err_str set) + let set = Hashtbl.find err_per_line loc.Location.line in + Hashtbl.replace err_per_line loc.Location.line (StringSet.add err_str set) with Not_found -> - Hashtbl.add err_per_line loc.Sil.line (StringSet.singleton err_str) in + Hashtbl.add err_per_line loc.Location.line (StringSet.singleton err_str) in Errlog.iter add_err err_log; err_per_line @@ -298,7 +320,7 @@ module LineReader : sig val from_file_linenum : t -> DB.source_file -> int -> string option (** get the line from a location looking for the copy of the file in the results dir *) - val from_loc : t -> Sil.location -> string option + val from_loc : t -> Location.t -> string option end = struct (* map a file name to an array of string, one for each line in the file *) @@ -349,7 +371,7 @@ end = struct from_file_linenum_original hash sourcefile_in_resdir linenum let from_loc hash loc = - from_file_linenum hash loc.Sil.file loc.Sil.line + from_file_linenum hash loc.Location.file loc.Location.line end (** Create filename.c.html with line numbers and links to nodes *) @@ -357,7 +379,7 @@ let c_file_write_html proc_is_active linereader fname tenv cfg = let proof_cover = ref Specs.Visitedset.empty in let tbl = Hashtbl.create 11 in let process_node n = - let lnum = (Cfg.Node.get_loc n).Sil.line in + let lnum = (Cfg.Node.get_loc n).Location.line in let curr_nodes = try Hashtbl.find tbl lnum with Not_found -> [] in @@ -367,7 +389,9 @@ let c_file_write_html proc_is_active linereader fname tenv cfg = let global_err_log = Errlog.empty () in let do_proc proc_name proc_desc = (* add the err_log of this proc to [global_err_log] *) let proc_loc = (Cfg.Procdesc.get_loc proc_desc) in - if proc_is_active proc_name && Cfg.Procdesc.is_defined proc_desc && (DB.source_file_equal proc_loc.Sil.file !DB.current_source) then + if proc_is_active proc_name && + Cfg.Procdesc.is_defined proc_desc && + (DB.source_file_equal proc_loc.Location.file !DB.current_source) then begin list_iter process_node (Cfg.Procdesc.get_nodes proc_desc); match Specs.get_summary proc_name with diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli index 8137576ca..25b727b2f 100644 --- a/infer/src/backend/printer.mli +++ b/infer/src/backend/printer.mli @@ -20,7 +20,7 @@ val is_visited : Cfg.Node.t -> bool val force_delayed_prints : unit -> unit (** Start a session, and create a new html fine for the node if it does not exist yet *) -val start_session : Cfg.node -> Sil.location -> Procname.t -> int -> unit +val start_session : Cfg.node -> Location.t -> Procname.t -> int -> unit (** Finish a session, and perform delayed print actions if required *) val finish_session : Cfg.node -> unit @@ -43,7 +43,7 @@ module LineReader : sig val from_file_linenum : t -> DB.source_file -> int -> string option (** get the line from a location looking for the copy of the file in the results dir *) - val from_loc : t -> Sil.location -> string option + val from_loc : t -> Location.t -> string option end (** Create filename.c.html with line numbers and links to nodes for each file in the exe_env *) diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 8f3e931dc..49de9629c 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -461,7 +461,8 @@ let sym_eval abs e = Sil.Const (Sil.Ctuple (list_map eval el)) | Sil.Const _ -> e - | Sil.Sizeof (Sil.Tarray (Sil.Tint ik, e), _) when Sil.ikind_is_char ik && !Sil.curr_language <> Sil.Java -> + | Sil.Sizeof (Sil.Tarray (Sil.Tint ik, e), _) + when Sil.ikind_is_char ik && !Config.curr_language <> Config.Java -> eval e | Sil.Sizeof _ -> e @@ -1099,7 +1100,7 @@ let rec create_strexp_of_type tenvo struct_init_mode typ inst = let fresh_id = (Ident.create_fresh (if !Config.footprint then Ident.kfootprint else Ident.kprimed)) in Sil.Var fresh_id in - if !Sil.curr_language = Sil.Java && inst = Sil.Ialloc + if !Config.curr_language = Config.Java && inst = Sil.Ialloc then match typ with | Sil.Tfloat _ -> Sil.Const (Sil.Cfloat 0.0) diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index c77022ded..47bbd25f1 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -295,7 +295,7 @@ val has_dangling_uninit_attribute : 'a t -> exp -> bool val add_or_replace_exp_attribute : (Sil.attribute -> Sil.attribute -> unit) -> normal t -> exp -> attribute -> normal t (** mark Sil.Var's or Sil.Lvar's as undefined *) -val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Sil.location -> +val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Location.t -> Sil.path_pos -> normal t (** Remove an attribute from all the atoms in the heap *) @@ -350,11 +350,18 @@ val prop_set_footprint : 'a t -> 'b t -> exposed t (** Expand PE listsegs if the flag is on. *) val prop_expand : normal t -> normal t list -(** translate a logical and/or operation taking care of the non-strict semantics for side effects *) -val trans_land_lor : Sil.binop -> (Ident.t list * Sil.instr list) * Sil.exp -> (Ident.t list * Sil.instr list) * Sil.exp -> Sil.location -> (Ident.t list * Sil.instr list) * Sil.exp +(** translate a logical and/or operation + taking care of the non-strict semantics for side effects *) +val trans_land_lor : + Sil.binop -> (Ident.t list * Sil.instr list) * Sil.exp -> + (Ident.t list * Sil.instr list) * Sil.exp -> Location.t -> + (Ident.t list * Sil.instr list) * Sil.exp (** translate an if-then-else expression *) -val trans_if_then_else : (Ident.t list * Sil.instr list) * Sil.exp -> (Ident.t list * Sil.instr list) * Sil.exp -> (Ident.t list * Sil.instr list) * Sil.exp -> Sil.location -> (Ident.t list * Sil.instr list) * Sil.exp +val trans_if_then_else : + (Ident.t list * Sil.instr list) * Sil.exp -> (Ident.t list * Sil.instr list) * Sil.exp -> + (Ident.t list * Sil.instr list) * Sil.exp -> Location.t -> + (Ident.t list * Sil.instr list) * Sil.exp (** {2 Functions for existentially quantifying and unquantifying variables} *) diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 1e4d1eb7b..e31f66208 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -818,7 +818,7 @@ let check_inconsistency_base prop = let inconsistent_this () = (* "this" cannot be null in Java *) let do_hpred = function | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) -> - !Sil.curr_language = Sil.Java && + !Config.curr_language = Config.Java && Sil.pvar_is_this pv && Sil.exp_equal e Sil.exp_zero && Sil.pvar_is_seed pv @@ -830,7 +830,7 @@ let check_inconsistency_base prop = let procedure_attr = Cfg.Procdesc.get_attributes procdesc in let do_hpred = function | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) -> - !Sil.curr_language = Sil.C_CPP && + !Config.curr_language = Config.C_CPP && Sil.exp_equal e Sil.exp_zero && Sil.pvar_is_seed pv && Sil.pvar_get_name pv = Mangled.from_string "self" && @@ -1557,7 +1557,7 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing = | Sil.Sizeof (Sil.Tarray _, _), Sil.Sizeof (Sil.Tstruct _, _) | Sil.Sizeof (Sil.Tstruct _, _), Sil.Sizeof (Sil.Tarray _, _) -> true | _ -> false in - if !Sil.curr_language = Sil.Java && types_subject_to_cast then + if !Config.curr_language = Config.Java && types_subject_to_cast then begin let pos_type_opt, neg_type_opt = subtype_case_analysis tenv texp1 texp2 in let has_changed = match pos_type_opt with @@ -1630,7 +1630,10 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2 | None -> () end | _ -> () in - if is_callee && !Config.footprint && (!Config.Experiment.activate_subtyping_in_cpp || !Sil.curr_language = Sil.Java) then add_subtype () + if is_callee && + !Config.footprint && + (!Config.Experiment.activate_subtyping_in_cpp || !Config.curr_language = Config.Java) + then add_subtype () let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 : subst2 * Prop.normal Prop.t = match hpred2 with | Sil.Hpointsto (_e2, se2, texp2) -> @@ -1836,10 +1839,10 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * let root = Sil.Const (Sil.Cstr s) in let sexp = let index = Sil.exp_int (Sil.Int.of_int (String.length s)) in - match !Sil.curr_language with - | Sil.C_CPP -> + match !Config.curr_language with + | Config.C_CPP -> Sil.Earray (size, [(index, Sil.Eexp (Sil.exp_zero, Sil.inst_none))], Sil.inst_none) - | Sil.Java -> + | Config.Java -> let mk_fld_sexp s = let fld = Ident.create_fieldname (Mangled.from_string s) 0 in let se = Sil.Eexp (Sil.Var (Ident.create_fresh Ident.kprimed), Sil.Inone) in @@ -1847,9 +1850,9 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * let fields = ["java.lang.String.count"; "java.lang.String.hash"; "java.lang.String.offset"; "java.lang.String.value"] in Sil.Estruct (list_map mk_fld_sexp fields, Sil.inst_none) in let const_string_texp = - match !Sil.curr_language with - | Sil.C_CPP -> Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, size), Sil.Subtype.exact) - | Sil.Java -> + match !Config.curr_language with + | Config.C_CPP -> Sil.Sizeof (Sil.Tarray (Sil.Tint Sil.IChar, size), Sil.Subtype.exact) + | Config.Java -> let object_type = Sil.TN_csu (Sil.Class, Mangled.from_string "java.lang.String") in let typ = match Sil.tenv_lookup tenv object_type with | Some typ -> typ diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 1c10ef008..0631b50c4 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -411,9 +411,9 @@ let mk_ptsto_exp_footprint end end; let off_foot, eqs = laundry_offset_for_footprint max_stamp off in - let st = match !Sil.curr_language with - | Sil.C_CPP -> Sil.Subtype.exact - | Sil.Java -> Sil.Subtype.subtypes in + let st = match !Config.curr_language with + | Config.C_CPP -> Sil.Subtype.exact + | Config.Java -> Sil.Subtype.subtypes in let create_ptsto footprint_part off0 = match root, off0, typ with | Sil.Lvar pvar, [], Sil.Tfun _ -> let fun_name = Procname.from_string_c_fun (Mangled.to_string (Sil.pvar_get_name pvar)) in @@ -967,7 +967,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = let is_deref_of_nullable = let is_definitely_non_null exp prop = Prover.check_disequal prop exp Sil.exp_zero in - !Config.report_nullable_inconsistency && !Sil.curr_language = Sil.Java && + !Config.report_nullable_inconsistency && !Config.curr_language = Config.Java && not (is_definitely_non_null root prop) && is_only_pt_by_nullable_fld_or_param root in let relevant_attributes_getters = [ Prop.get_resource_undef_attribute; @@ -1054,28 +1054,38 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc = Some (Sil.Lfield(e'', fn, t)), true (* the block dereferences is a field of an object*) | Some (_, e) -> Some e, false | _ -> None, false in - if (!Sil.curr_language = Sil.C_CPP) && fun_exp_may_be_null () && not (is_fun_exp_captured_var ()) then begin - let deref_str = Localise.deref_str_null None in - let err_desc_nobuckets = Errdesc.explain_dereference ~is_nullable: true deref_str prop loc in - match fun_exp with - | Sil.Var id when Ident.is_footprint id -> - let e_opt, is_field_deref = is_field_deref () in - let err_desc_nobuckets' = (match e_opt with - | Some e -> Localise.parameter_field_not_null_checked_desc err_desc_nobuckets e - | _ -> err_desc_nobuckets) in - let err_desc = - Localise.error_desc_set_bucket - err_desc_nobuckets' Localise.BucketLevel.b1 !Config.show_buckets in - if is_field_deref then - raise (Exceptions.Field_not_null_checked (err_desc, try assert false with Assert_failure x -> x)) - else - raise (Exceptions.Parameter_not_null_checked (err_desc, try assert false with Assert_failure x -> x)) - | _ -> (* HP: fun_exp is not a footprint therefore, either is a local or it's a modified param *) - let err_desc = - Localise.error_desc_set_bucket - err_desc_nobuckets Localise.BucketLevel.b1 !Config.show_buckets in - raise (Exceptions.Null_dereference (err_desc, try assert false with Assert_failure x -> x)) - end + if (!Config.curr_language = Config.C_CPP) && + fun_exp_may_be_null () && + not (is_fun_exp_captured_var ()) then + begin + let deref_str = Localise.deref_str_null None in + let err_desc_nobuckets = Errdesc.explain_dereference ~is_nullable: true deref_str prop loc in + match fun_exp with + | Sil.Var id when Ident.is_footprint id -> + let e_opt, is_field_deref = is_field_deref () in + let err_desc_nobuckets' = (match e_opt with + | Some e -> Localise.parameter_field_not_null_checked_desc err_desc_nobuckets e + | _ -> err_desc_nobuckets) in + let err_desc = + Localise.error_desc_set_bucket + err_desc_nobuckets' Localise.BucketLevel.b1 !Config.show_buckets in + if is_field_deref then + raise + (Exceptions.Field_not_null_checked + (err_desc, try assert false with Assert_failure x -> x)) + else + raise + (Exceptions.Parameter_not_null_checked + (err_desc, try assert false with Assert_failure x -> x)) + | _ -> + (* HP: fun_exp is not a footprint therefore, + either is a local or it's a modified param *) + let err_desc = + Localise.error_desc_set_bucket + err_desc_nobuckets Localise.BucketLevel.b1 !Config.show_buckets in + raise (Exceptions.Null_dereference + (err_desc, try assert false with Assert_failure x -> x)) + end (** [rearrange lexp prop] rearranges [prop] into the form [prop' * lexp|->strexp:typ]. It returns an iterator with [lexp |-> strexp: typ] as current predicate diff --git a/infer/src/backend/rearrange.mli b/infer/src/backend/rearrange.mli index f162970ff..e475c52ef 100644 --- a/infer/src/backend/rearrange.mli +++ b/infer/src/backend/rearrange.mli @@ -14,11 +14,13 @@ exception ARRAY_ACCESS (** Check for dereference errors: dereferencing 0, a freed value, or an undefined value *) val check_dereference_error : - Cfg.Procdesc.t -> Prop.normal Prop.t -> Sil.exp -> Sil.location -> unit + Cfg.Procdesc.t -> Prop.normal Prop.t -> Sil.exp -> Location.t -> unit -(** Check that an expression representing an objc block can be null and raise a [B1] null exception.*) +(** Check that an expression representing an objc block + can be null and raise a [B1] null exception. *) (** It's used to check that we don't call possibly null blocks *) -val check_call_to_objc_block_error : Cfg.Procdesc.t -> Prop.normal Prop.t -> Sil.exp -> Sil.location -> unit +val check_call_to_objc_block_error : + Cfg.Procdesc.t -> Prop.normal Prop.t -> Sil.exp -> Location.t -> unit (** [rearrange lexp prop] rearranges [prop] into the form [prop' * lexp|->strexp:typ]. It returns an iterator with [lexp |-> strexp: typ] as current predicate @@ -26,4 +28,4 @@ val check_call_to_objc_block_error : Cfg.Procdesc.t -> Prop.normal Prop.t -> Si val rearrange : Cfg.Procdesc.t -> Sil.tenv -> Sil.exp -> Sil.typ -> Prop.normal Prop.t -> - Sil.location -> (Sil.offset list) Prop.prop_iter list + Location.t -> (Sil.offset list) Prop.prop_iter list diff --git a/infer/src/backend/reporting.ml b/infer/src/backend/reporting.ml index b951cdf04..16c02d2d9 100644 --- a/infer/src/backend/reporting.ml +++ b/infer/src/backend/reporting.ml @@ -12,7 +12,7 @@ module L = Logging type log_issue = Procname.t -> - ?loc: Sil.location option -> + ?loc: Location.t option -> ?node_id: (int * int) option -> ?session: int option -> ?ltr: Errlog.loc_trace option -> diff --git a/infer/src/backend/reporting.mli b/infer/src/backend/reporting.mli index deffcc780..376981b1b 100644 --- a/infer/src/backend/reporting.mli +++ b/infer/src/backend/reporting.mli @@ -10,7 +10,7 @@ (** Type of functions to report issues to the error_log in a spec. *) type log_issue = Procname.t -> - ?loc: Sil.location option -> + ?loc: Location.t option -> ?node_id: (int * int) option -> ?session: int option -> ?ltr: Errlog.loc_trace option -> diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index 6b4f22ade..1749b97f9 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -31,41 +31,9 @@ type method_annotation = type func_attribute = | FA_sentinel of int * int (** __attribute__((sentinel(int, int))) *) -(** Programming language. *) -type language = C_CPP | Java - (** Visibility modifiers. *) type access = Default | Public | Private | Protected -(** Attributes of a procedure. *) -type proc_attributes = - { - access : access; (** visibility access *) - exceptions : string list; (** exceptions thrown by the procedure *) - is_abstract : bool; (** the procedure is abstract *) - mutable is_bridge_method : bool; (** the procedure is a bridge method *) - is_objc_instance_method : bool; (** the procedure is an objective-C instance method *) - mutable is_synthetic_method : bool; (** the procedure is a synthetic method *) - language : language; - func_attributes : func_attribute list; - method_annotation : method_annotation; - is_generated : bool; - } - -let copy_proc_attributes pa = - { - access = pa.access; - exceptions = pa.exceptions; - is_abstract = pa.is_abstract; - is_bridge_method = pa.is_bridge_method; - is_objc_instance_method = pa.is_objc_instance_method; - is_synthetic_method = pa.is_synthetic_method; - language = pa.language; - func_attributes = pa.func_attributes; - method_annotation = pa.method_annotation; - is_generated = pa.is_generated; - } - (** Compare function for annotations. *) let annotation_compare a1 a2 = let n = string_compare a1.class_name a2.class_name in @@ -120,9 +88,6 @@ let get_sentinel_func_attribute_value attr_list = | FA_sentinel (sentinel, null_pos) -> Some (sentinel, null_pos) with Not_found -> None -(** current language *) -let curr_language = ref C_CPP - (** Class, struct, union, (Obj C) protocol *) type csu = | Class @@ -136,27 +101,12 @@ type typename = | TN_enum of Mangled.t | TN_csu of csu * Mangled.t -(** Location in the original source file *) -type location = { - line: int; (** The line number. -1 means "do not know" *) - col: int; (** The column number. -1 means "do not know" *) - file: DB.source_file; (** The name of the source file *) - nLOC : int; (** Lines of code in the source file *) -} - -let dummy_location = { - line = -1; - col = -1; - file = DB.source_file_empty; - nLOC = -1 -} - (** Kind of global variables *) type pvar_kind = | Local_var of Procname.t (** local variable belonging to a function *) | Callee_var of Procname.t (** local variable belonging to a callee *) - | Abducted_retvar of Procname.t * location (** synthetic variable to represent return value *) - | Abducted_ref_param of Procname.t * pvar * location + | Abducted_retvar of Procname.t * Location.t (** synthetic variable to represent return value *) + | Abducted_ref_param of Procname.t * pvar * Location.t (** synthetic variable to represent param passed by reference *) | Global_var (** gloval variable *) | Seed_var (** variable used to store the initial value of formal parameters *) @@ -639,14 +589,14 @@ type dexp = | Dconst of const | Dsizeof of typ * Subtype.t | Dderef of dexp - | Dfcall of dexp * dexp list * location * call_flags + | Dfcall of dexp * dexp list * Location.t * call_flags | Darrow of dexp * Ident.fieldname | Ddot of dexp * Ident.fieldname | Dpvar of pvar | Dpvaraddr of pvar | Dunop of unop * dexp | Dunknown - | Dretcall of dexp * dexp list * location * call_flags + | Dretcall of dexp * dexp list * Location.t * call_flags (** Value paths: identify an occurrence of a value in a symbolic heap each expression represents a path, with Dpvar being the simplest one *) @@ -658,7 +608,7 @@ and res_action = { ra_kind : res_act_kind; (** kind of action *) ra_res : resource; (** kind of resource *) ra_pname : Procname.t; (** name of the procedure used to acquire/release the resource *) - ra_loc : location; (** location of the acquire/release *) + ra_loc : Location.t; (** location of the acquire/release *) ra_vpath: vpath; (** vpath of the resource value *) } @@ -667,12 +617,16 @@ and attribute = | Aresource of res_action (** resource acquire/release *) | Aautorelease | Adangling of dangling_kind (** dangling pointer *) - | Aundef of Procname.t * location * path_pos (** undefined value obtained by calling the given procedure *) + (** undefined value obtained by calling the given procedure *) + | Aundef of Procname.t * Location.t * path_pos | Ataint | Auntaint - | Adiv0 of path_pos (** value appeared in second argument of division in path position *) - | Aobjc_null of exp (** the exp. is null because of a call to a method with exp as a null receiver *) - | Aretval of Procname.t (** value was returned from a call to the given procedure *) + (** value appeared in second argument of division at given path position *) + | Adiv0 of path_pos + (** the exp. is null because of a call to a method with exp as a null receiver *) + | Aobjc_null of exp + (** value was returned from a call to the given procedure *) + | Aretval of Procname.t (** Categories of attributes *) and attribute_category = @@ -724,9 +678,50 @@ and exp = | Lindex of exp * exp (** an array index offset: exp1[exp2] *) | Sizeof of typ * Subtype.t (** a sizeof expression *) -(** Unknown location *) -let loc_none = - { line = - 1; col = - 1; file = DB.source_file_empty; nLOC = 0 } +(** Attributes of a procedure. *) +type proc_attributes = + { + access : access; (** visibility access *) + captured : (Mangled.t * typ) list; (** name and type of variables captured in blocks *) + exceptions : string list; (** exceptions thrown by the procedure *) + formals : (string * typ) list; (** name and type of formal parameters *) + func_attributes : func_attribute list; + is_abstract : bool; (** the procedure is abstract *) + mutable is_bridge_method : bool; (** the procedure is a bridge method *) + is_defined : bool; (** true if the procedure is defined, and not just declared *) + is_generated : bool; (** the procedure has been generated *) + is_objc_instance_method : bool; (** the procedure is an objective-C instance method *) + mutable is_synthetic_method : bool; (** the procedure is a synthetic method *) + language : Config.language; (** language of the procedure *) + loc : Location.t; (** location of this procedure in the source code *) + mutable locals : (Mangled.t * typ) list; (** name and type of local variables *) + method_annotation : method_annotation; (** annotations for java methods *) + proc_flags : proc_flags; (** flags of the procedure *) + proc_name : Procname.t; (** name of the procedure *) + ret_type : typ; (** return type *) + } + +let copy_proc_attributes pa = + { + access = pa.access; + captured = pa.captured; + exceptions = pa.exceptions; + formals = pa.formals; + func_attributes = pa.func_attributes; + is_abstract = pa.is_abstract; + is_bridge_method = pa.is_bridge_method; + is_defined = pa.is_defined; + is_generated = pa.is_generated; + is_objc_instance_method = pa.is_objc_instance_method; + is_synthetic_method = pa.is_synthetic_method; + language = pa.language; + loc = pa.loc; + locals = pa.locals; + method_annotation = pa.method_annotation; + proc_flags = pa.proc_flags; + proc_name = pa.proc_name; + ret_type = pa.ret_type; + } (** Kind of prune instruction *) type if_kind = @@ -746,18 +741,25 @@ type stackop = (** An instruction. *) type instr = - | Letderef of Ident.t * exp * typ * location (** declaration [let x = *lexp:typ] where [typ] is the root type of [lexp] *) - | Set of exp * typ * exp * location (** assignment [*lexp1:typ = exp2] where [typ] is the root type of [lexp1] *) - | Prune of exp * location * bool * if_kind (** prune the state based on [exp=1], the boolean indicates whether true branch *) - | Call of Ident.t list * exp * (exp * typ) list * location * call_flags + (** declaration [let x = *lexp:typ] where [typ] is the root type of [lexp] *) + | Letderef of Ident.t * exp * typ * Location.t + (** assignment [*lexp1:typ = exp2] where [typ] is the root type of [lexp1] *) + | Set of exp * typ * exp * Location.t + (** prune the state based on [exp=1], the boolean indicates whether true branch *) + | Prune of exp * Location.t * bool * if_kind (** [Call (ret_id1..ret_idn, e_fun, arg_ts, loc, call_flags)] represents an instructions - [ret_id1..ret_idn = e_fun(arg_ts);] where n = 0 for void return and n > 1 for struct return *) - | Nullify of pvar * location * bool (** nullify stack variable, the bool parameter indicates whether to deallocate the variable *) - | Abstract of location (** apply abstraction *) - | Remove_temps of Ident.t list * location (** remove temporaries *) - | Stackop of stackop * location (** operation on the stack of propsets *) - | Declare_locals of (pvar * typ) list * location (** declare local variables *) - | Goto_node of exp * location (** jump to a specific cfg node, assuming all the possible target nodes are successors of the current node *) + [ret_id1..ret_idn = e_fun(arg_ts);] + where n = 0 for void return and n > 1 for struct return *) + | Call of Ident.t list * exp * (exp * typ) list * Location.t * call_flags + (** nullify stack variable, the bool parameter indicates whether to deallocate the variable *) + | Nullify of pvar * Location.t * bool + | Abstract of Location.t (** apply abstraction *) + | Remove_temps of Ident.t list * Location.t (** remove temporaries *) + | Stackop of stackop * Location.t (** operation on the stack of propsets *) + | Declare_locals of (pvar * typ) list * Location.t (** declare local variables *) + (** jump to a specific cfg node, + assuming all the possible target nodes are successors of the current node *) + | Goto_node of exp * Location.t (** Check if an instruction is auxiliary, or if it comes from source instructions. *) let instr_is_auxiliary = function @@ -944,13 +946,6 @@ let is_static_local_name pname pvar = (* local static name is of the form procna | [s1; s2] -> true | _ -> false -let loc_compare loc1 loc2 = - let n = int_compare loc1.line loc2.line in - if n <> 0 then n else DB.source_file_compare loc1.file loc2.file - -let loc_equal loc1 loc2 = - loc_compare loc1 loc2 = 0 - let rec pv_kind_compare k1 k2 = match k1, k2 with | Local_var n1, Local_var n2 -> Procname.compare n1 n2 | Local_var _, _ -> - 1 @@ -960,14 +955,14 @@ let rec pv_kind_compare k1 k2 = match k1, k2 with | _, Callee_var _ -> 1 | Abducted_retvar (p1, l1), Abducted_retvar (p2, l2) -> let n = Procname.compare p1 p2 in - if n <> 0 then n else loc_compare l1 l2 + if n <> 0 then n else Location.compare l1 l2 | Abducted_retvar _, _ -> - 1 | _, Abducted_retvar _ -> 1 | Abducted_ref_param (p1, pv1, l1), Abducted_ref_param (p2, pv2, l2) -> let n = Procname.compare p1 p2 in if n <> 0 then n else let n = pvar_compare pv1 pv2 in - if n <> 0 then n else loc_compare l1 l2 + if n <> 0 then n else Location.compare l1 l2 | Abducted_ref_param _, _ -> - 1 | _, Abducted_ref_param _ -> 1 | Global_var, Global_var -> 0 @@ -1770,19 +1765,6 @@ let str_binop pe binop = | _ -> text_binop binop -(** Pretty print a location *) -let pp_loc f (loc: location) = - F.fprintf f "[line %d]" loc.line - -let loc_to_string loc = - let s = (string_of_int loc.line) in - if (loc.col != -1) then - s ^":"^(string_of_int loc.col) - else s - -(** Dump a location *) -let d_loc (loc: location) = L.add_print_action (L.PTloc, Obj.repr loc) - let rec _pp_pvar f pv = let name = pv.pv_name in match pv.pv_kind with @@ -1794,10 +1776,10 @@ let rec _pp_pvar f pv = else F.fprintf f "%a$%a|callee" Procname.pp n Mangled.pp name | Abducted_retvar (n, l) -> if !Config.pp_simple then F.fprintf f "%a|abductedRetvar" Mangled.pp name - else F.fprintf f "%a$%a%a|abductedRetvar" Procname.pp n pp_loc l Mangled.pp name + else F.fprintf f "%a$%a%a|abductedRetvar" Procname.pp n Location.pp l Mangled.pp name | Abducted_ref_param (n, pv, l) -> if !Config.pp_simple then F.fprintf f "%a|%a|abductedRefParam" _pp_pvar pv Mangled.pp name - else F.fprintf f "%a$%a%a|abductedRefParam" Procname.pp n pp_loc l Mangled.pp name + else F.fprintf f "%a$%a%a|abductedRefParam" Procname.pp n Location.pp l Mangled.pp name | Global_var -> F.fprintf f "#GB$%a" Mangled.pp name | Seed_var -> F.fprintf f "old_%a" Mangled.pp name @@ -1892,7 +1874,7 @@ let ptr_kind_string = function | Pk_objc_unsafe_unretained -> "__unsafe_unretained *" | Pk_objc_autoreleasing -> "__autoreleasing *" -let java () = !curr_language = Java +let java () = !Config.curr_language = Config.Java let eradicate_java () = !Config.eradicate && java () (** convert a dexp to a string *) @@ -1988,7 +1970,8 @@ and attribute_to_string pe = function if !Config.trace_error then pp_to_string (pp_vpath pe) ra.ra_vpath else "" in - name ^ (str_binop pe Lt) ^ Procname.to_string ra.ra_pname ^ ":" ^ (string_of_int ra.ra_loc.line) ^ (str_binop pe Gt) ^ str_vpath + name ^ (str_binop pe Lt) ^ Procname.to_string ra.ra_pname ^ ":" ^ + (string_of_int ra.ra_loc.Location.line) ^ (str_binop pe Gt) ^ str_vpath | Aautorelease -> "AUTORELEASE" | Adangling dk -> let dks = match dk with @@ -1996,7 +1979,9 @@ and attribute_to_string pe = function | DAaddr_stack_var -> "ADDR_STACK" | DAminusone -> "MINUS1" in "DANGL" ^ (str_binop pe Lt) ^ dks ^ (str_binop pe Gt) - | Aundef (pn, loc, _) -> "UND" ^ (str_binop pe Lt) ^ Procname.to_string pn ^ (str_binop pe Gt) ^ ":" ^ (string_of_int loc.line) + | Aundef (pn, loc, _) -> + "UND" ^ (str_binop pe Lt) ^ Procname.to_string pn ^ + (str_binop pe Gt) ^ ":" ^ (string_of_int loc.Location.line) | Ataint -> "TAINTED" | Auntaint -> "UNTAINTED" | Adiv0 (pn, nd_id) -> "DIV0" @@ -2207,33 +2192,47 @@ let pp_call_flags f cf = let pp_instr pe0 f instr = let pe, changed = color_pre_wrapper pe0 f instr in (match instr with - | Letderef (id, e, t, loc) -> F.fprintf f "%a=*%a:%a %a" (Ident.pp pe) id (pp_exp pe) e (pp_typ pe) t pp_loc loc - | Set (e1, t, e2, loc) -> F.fprintf f "*%a:%a=%a %a" (pp_exp pe) e1 (pp_typ pe) t (pp_exp pe) e2 pp_loc loc + | Letderef (id, e, t, loc) -> + F.fprintf f "%a=*%a:%a %a" + (Ident.pp pe) id + (pp_exp pe) e + (pp_typ pe) t + Location.pp loc + | Set (e1, t, e2, loc) -> + F.fprintf f "*%a:%a=%a %a" + (pp_exp pe) e1 + (pp_typ pe) t + (pp_exp pe) e2 + Location.pp loc | Prune (cond, loc, true_branch, ik) -> - F.fprintf f "PRUNE(%a, %b); %a" (pp_exp pe) cond true_branch pp_loc loc + F.fprintf f "PRUNE(%a, %b); %a" (pp_exp pe) cond true_branch Location.pp loc | Call (ret_ids, e, arg_ts, loc, cf) -> (match ret_ids with | [] -> () | _ -> F.fprintf f "%a=" (pp_comma_seq (Ident.pp pe)) ret_ids); - F.fprintf f "%a(%a)%a %a" (pp_exp pe) e (pp_comma_seq (pp_exp_typ pe)) (arg_ts) pp_call_flags cf pp_loc loc + F.fprintf f "%a(%a)%a %a" + (pp_exp pe) e + (pp_comma_seq (pp_exp_typ pe)) (arg_ts) + pp_call_flags cf + Location.pp loc | Nullify (pvar, loc, deallocate) -> - F.fprintf f "NULLIFY(%a,%b); %a" (pp_pvar pe) pvar deallocate pp_loc loc + F.fprintf f "NULLIFY(%a,%b); %a" (pp_pvar pe) pvar deallocate Location.pp loc | Abstract loc -> - F.fprintf f "APPLY_ABSTRACTION; %a" pp_loc loc + F.fprintf f "APPLY_ABSTRACTION; %a" Location.pp loc | Remove_temps (temps, loc) -> - F.fprintf f "REMOVE_TEMPS(%a); %a" (Ident.pp_list pe) temps pp_loc loc + F.fprintf f "REMOVE_TEMPS(%a); %a" (Ident.pp_list pe) temps Location.pp loc | Stackop (stackop, loc) -> let s = match stackop with | Push -> "Push" | Swap -> "Swap" | Pop -> "Pop" in - F.fprintf f "STACKOP.%s; %a" s pp_loc loc + F.fprintf f "STACKOP.%s; %a" s Location.pp loc | Declare_locals (ptl, loc) -> (* let pp_pvar_typ fmt (pvar, typ) = F.fprintf fmt "%a:%a" (pp_pvar pe) pvar (pp_typ_full pe) typ in *) let pp_pvar_typ fmt (pvar, typ) = F.fprintf fmt "%a" (pp_pvar pe) pvar in - F.fprintf f "DECLARE_LOCALS(%a); %a" (pp_comma_seq pp_pvar_typ) ptl pp_loc loc + F.fprintf f "DECLARE_LOCALS(%a); %a" (pp_comma_seq pp_pvar_typ) ptl Location.pp loc | Goto_node (e, loc) -> - F.fprintf f "Goto_node %a %a" (pp_exp pe) e pp_loc loc + F.fprintf f "Goto_node %a %a" (pp_exp pe) e Location.pp loc ); color_post_wrapper changed pe0 f @@ -2516,9 +2515,9 @@ let inst_initial = Iinitial (** for initial values *) let inst_lookup = Ilookup let inst_none = Inone let inst_nullify = Inullify -let inst_rearrange b loc pos = Irearrange (Some b, false, loc.line, pos) +let inst_rearrange b loc pos = Irearrange (Some b, false, loc.Location.line, pos) let inst_taint = Itaint -let inst_update loc pos = Iupdate (None, false, loc.line, pos) +let inst_update loc pos = Iupdate (None, false, loc.Location.line, pos) (** update the location of the instrumentation *) let inst_new_loc loc inst = match inst with @@ -2530,10 +2529,10 @@ let inst_new_loc loc inst = match inst with | Ilookup -> inst | Inone -> inst | Inullify -> inst - | Irearrange (zf, ncf, n, pos) -> Irearrange (zf, ncf, loc.line, pos) + | Irearrange (zf, ncf, n, pos) -> Irearrange (zf, ncf, loc.Location.line, pos) | Itaint -> inst - | Iupdate (zf, ncf, n, pos) -> Iupdate (zf, ncf, loc.line, pos) - | Ireturn_from_call n -> Ireturn_from_call loc.line + | Iupdate (zf, ncf, n, pos) -> Iupdate (zf, ncf, loc.Location.line, pos) + | Ireturn_from_call n -> Ireturn_from_call loc.Location.line (** return a string representing the inst *) let inst_to_string inst = @@ -2633,10 +2632,6 @@ let update_inst inst_old inst_new = Iupdate (zf', ncf, n, pos) | Ireturn_from_call _ -> inst_new -let string_of_language = function - | Java -> "Java" - | C_CPP -> "C_CPP" - (** describe an instrumentation with a string *) let pp_inst pe f inst = let str = inst_to_string inst in @@ -3506,19 +3501,19 @@ let instr_compare instr1 instr2 = match instr1, instr2 with let n = Ident.compare id1 id2 in if n <> 0 then n else let n = exp_compare e1 e2 in if n <> 0 then n else let n = typ_compare t1 t2 in - if n <> 0 then n else loc_compare loc1 loc2 + if n <> 0 then n else Location.compare loc1 loc2 | Letderef _, _ -> -1 | _, Letderef _ -> 1 | Set (e11, t1, e21, loc1), Set (e12, t2, e22, loc2) -> let n = exp_compare e11 e12 in if n <> 0 then n else let n = typ_compare t1 t2 in if n <> 0 then n else let n = exp_compare e21 e22 in - if n <> 0 then n else loc_compare loc1 loc2 + if n <> 0 then n else Location.compare loc1 loc2 | Set _, _ -> -1 | _, Set _ -> 1 | Prune (cond1, loc1, true_branch1, ik1), Prune (cond2, loc2, true_branch2, ik2) -> let n = exp_compare cond1 cond2 in - if n <> 0 then n else let n = loc_compare loc1 loc2 in + if n <> 0 then n else let n = Location.compare loc1 loc2 in if n <> 0 then n else let n = bool_compare true_branch1 true_branch2 in if n <> 0 then n else Pervasives.compare ik1 ik2 | Prune _, _ -> -1 @@ -3527,28 +3522,28 @@ let instr_compare instr1 instr2 = match instr1, instr2 with let n = list_compare Ident.compare ret_ids1 ret_ids2 in if n <> 0 then n else let n = exp_compare e1 e2 in if n <> 0 then n else let n = list_compare exp_typ_compare arg_ts1 arg_ts2 in - if n <> 0 then n else let n = loc_compare loc1 loc2 in + if n <> 0 then n else let n = Location.compare loc1 loc2 in if n <> 0 then n else call_flags_compare cf1 cf2 | Call _, _ -> -1 | _, Call _ -> 1 | Nullify (pvar1, loc1, deallocate1), Nullify (pvar2, loc2, deallocate2) -> let n = pvar_compare pvar1 pvar2 in - if n <> 0 then n else let n = loc_compare loc1 loc2 in + if n <> 0 then n else let n = Location.compare loc1 loc2 in if n <> 0 then n else bool_compare deallocate1 deallocate2 | Nullify _, _ -> -1 | _, Nullify _ -> 1 | Abstract loc1, Abstract loc2 -> - loc_compare loc1 loc2 + Location.compare loc1 loc2 | Abstract _, _ -> -1 | _, Abstract _ -> 1 | Remove_temps (temps1, loc1), Remove_temps (temps2, loc2) -> let n = list_compare Ident.compare temps1 temps2 in - if n <> 0 then n else loc_compare loc1 loc2 + if n <> 0 then n else Location.compare loc1 loc2 | Remove_temps _, _ -> -1 | _, Remove_temps _ -> 1 | Stackop (stackop1, loc1), Stackop (stackop2, loc2) -> let n = Pervasives.compare stackop1 stackop2 in - if n <> 0 then n else loc_compare loc1 loc2 + if n <> 0 then n else Location.compare loc1 loc2 | Stackop _, _ -> -1 | _, Stackop _ -> 1 | Declare_locals (ptl1, loc1), Declare_locals (ptl2, loc2) -> @@ -3557,12 +3552,12 @@ let instr_compare instr1 instr2 = match instr1, instr2 with if n <> 0 then n else typ_compare t1 t2 in let n = list_compare pt_compare ptl1 ptl2 in - if n <> 0 then n else loc_compare loc1 loc2 + if n <> 0 then n else Location.compare loc1 loc2 | Declare_locals _, _ -> -1 | _, Declare_locals _ -> 1 | Goto_node (e1, loc1), Goto_node (e2, loc2) -> let n = exp_compare e1 e2 in - if n <> 0 then n else loc_compare loc1 loc2 + if n <> 0 then n else Location.compare loc1 loc2 (** compare expressions from different procedures without considering loc's, ident's, and pvar's. the [exp_map] param gives a mapping of names used in the procedure of [e1] to names used in the @@ -3911,11 +3906,11 @@ let mk_pvar_global (name: Mangled.t) : pvar = { pv_name = name; pv_kind = Global_var } (** create an abducted return variable for a call to [proc_name] at [loc] *) -let mk_pvar_abducted_ret (proc_name : Procname.t) (loc : location) : pvar = +let mk_pvar_abducted_ret (proc_name : Procname.t) (loc : Location.t) : pvar = let name = Mangled.from_string ("$RET_" ^ (Procname.to_unique_id proc_name)) in { pv_name = name; pv_kind = Abducted_retvar (proc_name, loc) } -let mk_pvar_abducted_ref_param (proc_name : Procname.t) (pv : pvar) (loc : location) : pvar = +let mk_pvar_abducted_ref_param (proc_name : Procname.t) (pv : pvar) (loc : Location.t) : pvar = let name = Mangled.from_string ("$REF_PARAM_" ^ (Procname.to_unique_id proc_name)) in { pv_name = name; pv_kind = Abducted_ref_param (proc_name, pv, loc) } diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index 40171fdd6..fd3135815 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -12,14 +12,6 @@ open Utils -(** Programming language. *) -type language = C_CPP | Java - -(** current language *) -val curr_language : language ref (* TODO: move to Config. It is good to have all global variables in the same place *) - -val string_of_language : language -> string - (** Class, struct, union, (Obj C) protocol *) type csu = | Class @@ -53,24 +45,6 @@ type func_attribute = (** Visibility modifiers. *) type access = Default | Public | Private | Protected -(** Attributes of a procedure. *) -type proc_attributes = - { - access : access; (** visibility access *) - exceptions : string list; (** exceptions thrown by the procedure *) - is_abstract : bool; (** the procedure is abstract *) - mutable is_bridge_method : bool; (** the procedure is a bridge method *) - is_objc_instance_method : bool; (** the procedure is an objective-C instance method *) - mutable is_synthetic_method : bool; (** the procedure is a synthetic method *) - language : language; - func_attributes : func_attribute list; - method_annotation : method_annotation; - is_generated : bool; - } - -(** Create a copy of a proc_attributes *) -val copy_proc_attributes : proc_attributes -> proc_attributes - (** Type for program variables. There are 4 kinds of variables: 1) local variables, used for local variables and formal parameters 2) callee program variables, used to handle recursion ([x | callee] is distinguished from [x]) @@ -79,16 +53,6 @@ val copy_proc_attributes : proc_attributes -> proc_attributes *) type pvar -(** Location in the original source file *) -type location = { - line: int; (** The line number. -1 means "do not know" *) - col: int; (** The column number. -1 means "do not know" *) - file: DB.source_file; (** The name of the source file *) - nLOC : int; (** Lines of code in the source file *) -} - -val dummy_location : location - (** Unary operations *) type unop = | Neg (** Unary minus *) @@ -260,14 +224,14 @@ type dexp = | Dconst of const | Dsizeof of typ * Subtype.t | Dderef of dexp - | Dfcall of dexp * dexp list * location * call_flags + | Dfcall of dexp * dexp list * Location.t * call_flags | Darrow of dexp * Ident.fieldname | Ddot of dexp * Ident.fieldname | Dpvar of pvar | Dpvaraddr of pvar | Dunop of unop * dexp | Dunknown - | Dretcall of dexp * dexp list * location * call_flags + | Dretcall of dexp * dexp list * Location.t * call_flags (** Value paths: identify an occurrence of a value in a symbolic heap each expression represents a path, with Dpvar being the simplest one *) @@ -279,7 +243,7 @@ and res_action = { ra_kind : res_act_kind; (** kind of action *) ra_res : resource; (** kind of resource *) ra_pname : Procname.t; (** name of the procedure used to acquire/release the resource *) - ra_loc : location; (** location of the acquire/release *) + ra_loc : Location.t; (** location of the acquire/release *) ra_vpath: vpath; (** vpath of the resource value *) } @@ -288,12 +252,16 @@ and attribute = | Aresource of res_action (** resource acquire/release *) | Aautorelease | Adangling of dangling_kind (** dangling pointer *) - | Aundef of Procname.t * location * path_pos (** undefined value obtained by calling the given procedure *) + (** undefined value obtained by calling the given procedure *) + | Aundef of Procname.t * Location.t * path_pos | Ataint | Auntaint - | Adiv0 of path_pos (** value appeared in second argument of division at given path position *) - | Aobjc_null of exp (** the exp. is null because of a call to a method with exp as a null receiver *) - | Aretval of Procname.t (** value was returned from a call to the given procedure *) + (** value appeared in second argument of division at given path position *) + | Adiv0 of path_pos + (** the exp. is null because of a call to a method with exp as a null receiver *) + | Aobjc_null of exp + (** value was returned from a call to the given procedure *) + | Aretval of Procname.t (** Categories of attributes *) and attribute_category = @@ -345,6 +313,32 @@ and exp = | Lindex of exp * exp (** an array index offset: [exp1\[exp2\]] *) | Sizeof of typ * Subtype.t (** a sizeof expression *) +(** Attributes of a procedure. *) +type proc_attributes = + { + access : access; (** visibility access *) + captured : (Mangled.t * typ) list; (** name and type of variables captured in blocks *) + exceptions : string list; (** exceptions thrown by the procedure *) + formals : (string * typ) list; (** name and type of formal parameters *) + func_attributes : func_attribute list; + is_abstract : bool; (** the procedure is abstract *) + mutable is_bridge_method : bool; (** the procedure is a bridge method *) + is_defined : bool; (** true if the procedure is defined, and not just declared *) + is_generated : bool; (** the procedure has been generated *) + is_objc_instance_method : bool; (** the procedure is an objective-C instance method *) + mutable is_synthetic_method : bool; (** the procedure is a synthetic method *) + language : Config.language; (** language of the procedure *) + loc : Location.t; (** location of this procedure in the source code *) + mutable locals : (Mangled.t * typ) list; (** name and type of local variables *) + method_annotation : method_annotation; (** annotations for java methods *) + proc_flags : proc_flags; (** flags of the procedure *) + proc_name : Procname.t; (** name of the procedure *) + ret_type : typ; (** return type *) + } + +(** Create a copy of a proc_attributes *) +val copy_proc_attributes : proc_attributes -> proc_attributes + (** Sets of types. *) module TypSet : Set.S with type elt = typ @@ -381,18 +375,25 @@ type stackop = (** An instruction. *) type instr = - | Letderef of Ident.t * exp * typ * location (** declaration [let x = *lexp:typ] where [typ] is the root type of [lexp] *) - | Set of exp * typ * exp * location (** assignment [*lexp1:typ = exp2] where [typ] is the root type of [lexp1] *) - | Prune of exp * location * bool * if_kind (** prune the state based on [exp=1], the boolean indicates whether true branch *) - | Call of Ident.t list * exp * (exp * typ) list * location * call_flags + (** declaration [let x = *lexp:typ] where [typ] is the root type of [lexp] *) + | Letderef of Ident.t * exp * typ * Location.t + (** assignment [*lexp1:typ = exp2] where [typ] is the root type of [lexp1] *) + | Set of exp * typ * exp * Location.t + (** prune the state based on [exp=1], the boolean indicates whether true branch *) + | Prune of exp * Location.t * bool * if_kind (** [Call (ret_id1..ret_idn, e_fun, arg_ts, loc, call_flags)] represents an instructions - [ret_id1..ret_idn = e_fun(arg_ts);] where n = 0 for void return and n > 1 for struct return *) - | Nullify of pvar * location * bool (** nullify stack variable, the bool parameter indicates whether to deallocate the variable *) - | Abstract of location (** apply abstraction *) - | Remove_temps of Ident.t list * location (** remove temporaries *) - | Stackop of stackop * location (** operation on the stack of propsets *) - | Declare_locals of (pvar * typ) list * location (** declare local variables *) - | Goto_node of exp * location (** jump to a specific cfg node, assuming all the possible target nodes are successors of the current node *) + [ret_id1..ret_idn = e_fun(arg_ts);] + where n = 0 for void return and n > 1 for struct return *) + | Call of Ident.t list * exp * (exp * typ) list * Location.t * call_flags + (** nullify stack variable, the bool parameter indicates whether to deallocate the variable *) + | Nullify of pvar * Location.t * bool + | Abstract of Location.t (** apply abstraction *) + | Remove_temps of Ident.t list * Location.t (** remove temporaries *) + | Stackop of stackop * Location.t (** operation on the stack of propsets *) + | Declare_locals of (pvar * typ) list * Location.t (** declare local variables *) + (** jump to a specific cfg node, + assuming all the possible target nodes are successors of the current node *) + | Goto_node of exp * Location.t (** Check if an instruction is auxiliary, or if it comes from source instructions. *) val instr_is_auxiliary : instr -> bool @@ -441,9 +442,10 @@ val inst_initial : inst (** for initial values *) val inst_lookup : inst val inst_none : inst val inst_nullify : inst -val inst_rearrange : bool -> location -> path_pos -> inst (** the boolean indicates whether the pointer is known nonzero *) +(** the boolean indicates whether the pointer is known nonzero *) +val inst_rearrange : bool -> Location.t -> path_pos -> inst val inst_taint : inst -val inst_update : location -> path_pos -> inst +val inst_update : Location.t -> path_pos -> inst (** Get the null case flag of the inst. *) val inst_get_null_case_flag : inst -> bool option @@ -452,7 +454,7 @@ val inst_get_null_case_flag : inst -> bool option val inst_set_null_case_flag : inst -> inst (** update the location of the instrumentation *) -val inst_new_loc : location -> inst -> inst +val inst_new_loc : Location.t -> inst -> inst (** Update [inst_old] to [inst_new] preserving the zero flag *) val update_inst : inst -> inst -> inst @@ -590,10 +592,6 @@ val exp_is_null_literal : exp -> bool (** return true if [exp] is the special this/self expression *) val exp_is_this : exp -> bool -val loc_compare : location -> location -> int - -val loc_equal : location -> location -> bool - val path_pos_equal : path_pos -> path_pos -> bool (** turn a *T into a T. fails if [typ] is not a pointer type *) @@ -816,14 +814,6 @@ val str_unop : unop -> string (** String representation of a binary operator. *) val str_binop : printenv -> binop -> string -(** Pretty print a location. *) -val pp_loc : Format.formatter -> location -> unit - -val loc_to_string : location -> string - -(** Dump a location. *) -val d_loc : location -> unit - (** name of the allocation function for the given memory kind *) val mem_alloc_pname : mem_kind -> Procname.t @@ -927,7 +917,7 @@ val pp_offset_list : printenv -> Format.formatter -> offset list -> unit val d_offset_list : offset list -> unit (** Get the location of the instruction *) -val instr_get_loc : instr -> location +val instr_get_loc : instr -> Location.t (** get the expressions occurring in the instruction *) val instr_get_exps : instr -> exp list @@ -1321,8 +1311,6 @@ val hpred_replace_exp : (exp * exp) list -> hpred -> hpred (** {2 Functions for constructing or destructing entities in this module} *) -(** Unknown location *) -val loc_none : location (** [mk_pvar name proc_name suffix] creates a program var with the given function name and suffix *) val mk_pvar : Mangled.t -> Procname.t -> pvar @@ -1337,9 +1325,9 @@ val mk_pvar_callee : Mangled.t -> Procname.t -> pvar val mk_pvar_global : Mangled.t -> pvar (** create an abducted return variable for a call to [proc_name] at [loc] *) -val mk_pvar_abducted_ret : Procname.t -> location -> pvar +val mk_pvar_abducted_ret : Procname.t -> Location.t -> pvar -val mk_pvar_abducted_ref_param : Procname.t -> pvar -> location -> pvar +val mk_pvar_abducted_ref_param : Procname.t -> pvar -> Location.t -> pvar (** Turn an ordinary program variable into a callee program variable *) val pvar_to_callee : Procname.t -> pvar -> pvar diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 3c1b0a782..8f226efbb 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -221,10 +221,10 @@ let normalized_specs_to_specs = module CallStats = struct (** module for tracing stats of function calls *) module PnameLocHash = Hashtbl.Make (struct - type t = Procname.t * Sil.location - let hash (pname, loc) = Hashtbl.hash (Procname.hash_pname pname, loc.Sil.line) + type t = Procname.t * Location.t + let hash (pname, loc) = Hashtbl.hash (Procname.hash_pname pname, loc.Location.line) let equal (pname1, loc1) (pname2, loc2) = - Sil.loc_equal loc1 loc2 && Procname.equal pname1 pname2 + Location.equal loc1 loc2 && Procname.equal pname1 pname2 end) type call_result = (** kind of result of a procedure call *) @@ -272,12 +272,13 @@ module CallStats = struct (** module for tracing stats of function calls *) let sorted_elems = let compare ((pname1, loc1), _) ((pname2, loc2), _) = let n = Procname.compare pname1 pname2 in - if n <> 0 then n else Sil.loc_compare loc1 loc2 in + if n <> 0 then n else Location.compare loc1 loc2 in list_sort compare !elems in list_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 Sil.pp_loc loc pp_trace tr in + 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 @@ -312,13 +313,8 @@ type payload = type summary = { dependency_map: dependency_map_t; (** maps children procs to timestamp as last seen at the start of an analysys phase for this proc *) - loc: Sil.location; (** original file and line number *) nodes: int list; (** ids of cfg nodes of the procedure *) - ret_type : Sil.typ; (** type of the return parameter *) - formals : (string * Sil.typ) list; (** name and type of the formal parameters of the procedure *) phase: phase; (** in FOOTPRINT phase or in RE_EXECUTION PHASE *) - proc_name : Procname.t; (** name of the procedure *) - proc_flags : proc_flags; (** flags of the procedure *) payload: payload; (** payload containing the result of some analysis *) sessions: int ref; (** Session number: how many nodes went trough symbolic execution *) stats: stats; (** statistics: execution time and list of errors *) @@ -410,9 +406,11 @@ let get_signature summary = let pp_name f () = F.fprintf f "%s" p in let pp f () = Sil.pp_type_decl pe_text pp_name Sil.pp_exp f typ in let decl = pp_to_string pp () in - s := if !s = "" then decl else !s ^ ", " ^ decl) summary.formals; - let pp_procname f () = F.fprintf f "%a" Procname.pp summary.proc_name in - let pp f () = Sil.pp_type_decl pe_text pp_procname Sil.pp_exp f summary.ret_type in + s := if !s = "" then decl else !s ^ ", " ^ decl) summary.attributes.Sil.formals; + let pp_procname f () = F.fprintf f "%a" + Procname.pp summary.attributes.Sil.proc_name in + let pp f () = + Sil.pp_type_decl pe_text pp_procname Sil.pp_exp f summary.attributes.Sil.ret_type in let decl = pp_to_string pp () in decl ^ "(" ^ !s ^ ")" @@ -665,13 +663,13 @@ let get_timestamp summary = summary.timestamp let get_proc_name summary = - summary.proc_name + summary.attributes.Sil.proc_name let get_ret_type summary = - summary.ret_type + summary.attributes.Sil.ret_type let get_formals summary = - summary.formals + summary.attributes.Sil.formals let get_attributes summary = summary.attributes @@ -682,7 +680,7 @@ let get_flag proc_name key = match get_summary proc_name with | None -> None | Some summary -> - let proc_flags = summary.proc_flags in + let proc_flags = summary.attributes.Sil.proc_flags in try Some (Hashtbl.find proc_flags key) with Not_found -> None @@ -694,7 +692,7 @@ let get_iterations proc_name = | None -> raise (Failure ("Specs.get_iterations: " ^ (Procname.to_string proc_name) ^ "Not_found")) | Some summary -> - let proc_flags = summary.proc_flags in + let proc_flags = summary.attributes.Sil.proc_flags in try let time_str = Hashtbl.find proc_flags proc_flag_iterations in Pervasives.int_of_string time_str @@ -707,7 +705,7 @@ let get_specs_formals proc_name = raise (Failure ("Specs.get_specs_formals: " ^ (Procname.to_string proc_name) ^ "Not_found")) | Some summary -> let specs = get_specs_from_payload summary in - let formals = summary.formals in + let formals = get_formals summary in (specs, formals) (** Return the specs for the proc in the spec table *) @@ -748,54 +746,54 @@ let update_dependency_map proc_name = summary.dependency_map in set_summary_origin proc_name { summary with dependency_map = current_dependency_map } origin -(** [init_summary loc (proc_name, ret_type, formals, depend_list, loc, nodes, +(** [init_summary (depend_list, nodes, proc_flags, initial_err_log, calls, cyclomatic, in_out_calls_opt, proc_attributes)] initializes the summary for [proc_name] given dependent procs in list [depend_list]. *) let init_summary - (proc_name, ret_type, formals, depend_list, loc, - nodes, proc_flags, initial_err_log, calls, cyclomatic, in_out_calls_opt, + (depend_list, nodes, + proc_flags, initial_err_log, calls, cyclomatic, in_out_calls_opt, proc_attributes) = let dependency_map = mk_initial_dependency_map depend_list in let summary = { dependency_map = dependency_map; - loc = loc; nodes = nodes; - ret_type = ret_type; - formals = formals; phase = FOOTPRINT; - proc_name = proc_name; - proc_flags = proc_flags; sessions = ref 0; payload = PrePosts []; stats = empty_stats initial_err_log calls cyclomatic in_out_calls_opt; status = INACTIVE; timestamp = 0; - attributes = proc_attributes; + attributes = + { proc_attributes with + Sil.proc_flags = proc_flags; }; } in - Procname.Hash.replace spec_tbl proc_name (summary, Res_dir) + Procname.Hash.replace spec_tbl proc_attributes.Sil.proc_name (summary, Res_dir) let reset_summary call_graph proc_name loc = let dependents = Cg.get_defined_children call_graph proc_name in let proc_attributes = { Sil.access = Sil.Default; - Sil.exceptions = []; - Sil.is_abstract = false; - Sil.is_bridge_method = false; - Sil.is_objc_instance_method = false; - Sil.is_synthetic_method = false; - Sil.language = !Sil.curr_language; - Sil.func_attributes = []; - Sil.method_annotation = Sil.method_annotation_empty; - Sil.is_generated = false; + formals = []; + captured = []; + exceptions = []; + func_attributes = []; + is_abstract = false; + is_defined = false; + is_bridge_method = false; + is_generated = false; + is_objc_instance_method = false; + is_synthetic_method = false; + language = !Config.curr_language; + loc; + locals = []; + method_annotation = Sil.method_annotation_empty; + proc_flags = proc_flags_empty (); + proc_name; + ret_type = Sil.Tvoid; } in init_summary ( - proc_name, - Sil.Tvoid, - [], - Procname.Set.elements - dependents, - loc, + Procname.Set.elements dependents, [], proc_flags_empty (), Errlog.empty (), diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index bd33f11d2..332704326 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -90,10 +90,10 @@ sig type trace = (call_result * bool) list (** iterate over results of procedure calls *) - val iter : (Procname.t * Sil.location -> trace -> unit) -> t -> unit + val iter : (Procname.t * Location.t -> trace -> unit) -> t -> unit (** trace a procedure call *) - val trace : t -> Procname.t -> Sil.location -> call_result -> bool -> unit + val trace : t -> Procname.t -> Location.t -> call_result -> bool -> unit (** pretty print a call trace *) val pp_trace : Format.formatter -> trace -> unit @@ -126,13 +126,8 @@ type payload = (** Procedure summary *) type summary = { dependency_map: dependency_map_t; (** maps children procs to timestamp as last seen at the start of an analysys phase for this proc *) - loc: Sil.location; (** original file and line number *) nodes: int list; (** ids of cfg nodes of the procedure *) - ret_type : Sil.typ; (** type of the return parameter *) - formals : (string * Sil.typ) list; (** name and type of the formal parameters of the procedure *) phase: phase; (** in FOOTPRINT phase or in RE_EXECUTION PHASE *) - proc_name : Procname.t; (** name of the procedure *) - proc_flags : proc_flags; (** flags of the procedure *) payload: payload; (** payload containing the result of some analysis *) sessions: int ref; (** Session number: how many nodes went trough symbolic execution *) stats: stats; (** statistics: execution time and list of errors *) @@ -219,21 +214,17 @@ val is_inactive : Procname.t -> bool (** Initialize the summary for [proc_name] given dependent procs in list [depend_list]. Do nothing if a summary exists already. *) val init_summary : - (Procname.t * (** proc_name *) - Sil.typ * (** ret type *) - (string * Sil.typ) list * (** formals *) - Procname.t list * (** depend list *) - Sil.location * (** loc *) + (Procname.t list * (** depend list *) int list * (** nodes *) proc_flags * (** procedure flags *) Errlog.t * (** initial error log *) - (Procname.t * Sil.location) list * (** calls *) + (Procname.t * Location.t) list * (** calls *) int * (** cyclomatic *) (Cg.in_out_calls option) * (** in and out calls *) Sil.proc_attributes) (** attributes of the procedure *) -> unit -val reset_summary : Cg.t -> Procname.t -> Sil.location -> unit +val reset_summary : Cg.t -> Procname.t -> Location.t -> unit (** Load procedure summary from the given file *) val load_summary : DB.filename -> summary option diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index 15ce5ec27..f07039828 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -51,7 +51,7 @@ type failure_stats = { mutable node_fail: int; (* number of node failures (i.e. at least one instruction failure) *) mutable node_ok: int; (* number of node successes (i.e. no instruction failures) *) mutable first_failure : - (Sil.location * (int * int) * int * Errlog.loc_trace * + (Location.t * (int * int) * int * Errlog.loc_trace * (Prop.normal Prop.t) option * exn) option (* exception at the first failure *) } @@ -142,9 +142,9 @@ let instrs_normalize instrs = let mk_find_duplicate_nodes proc_desc : (Cfg.Node.t -> Cfg.NodeSet.t) = let module M = (* map from (loc,kind) *) Map.Make(struct - type t = Sil.location * Cfg.Node.nodekind + type t = Location.t * Cfg.Node.nodekind let compare (loc1, k1) (loc2, k2) = - let n = Sil.loc_compare loc1 loc2 in + let n = Location.compare loc1 loc2 in if n <> 0 then n else Cfg.Node.kind_compare k1 k2 end) in @@ -283,7 +283,7 @@ let mark_instr_fail pre_opt exn = type log_issue = Procname.t -> - ?loc: Sil.location option -> + ?loc: Location.t option -> ?node_id: (int * int) option -> ?session: int option -> ?ltr: Errlog.loc_trace option -> diff --git a/infer/src/backend/state.mli b/infer/src/backend/state.mli index a68cac08f..f57543fb4 100644 --- a/infer/src/backend/state.mli +++ b/infer/src/backend/state.mli @@ -36,7 +36,7 @@ val get_inst_update : Sil.path_pos -> Sil.inst val get_instr : unit -> Sil.instr option (** Get last location seen in symbolic execution *) -val get_loc : unit -> Sil.location +val get_loc : unit -> Location.t (** Get the location trace of the last path seen in symbolic execution *) val get_loc_trace : unit -> Errlog.loc_trace @@ -85,7 +85,7 @@ val mk_find_duplicate_nodes: Cfg.Procdesc.t -> (Cfg.Node.t -> Cfg.NodeSet.t) type log_issue = Procname.t -> - ?loc: Sil.location option -> + ?loc: Location.t option -> ?node_id: (int * int) option -> ?session: int option -> ?ltr: Errlog.loc_trace option -> diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 69f8c3e5e..01c09dd05 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1,12 +1,12 @@ (* -* Copyright (c) 2009 - 2013 Monoidics ltd. -* Copyright (c) 2013 - present Facebook, Inc. -* All rights reserved. -* -* This source code is licensed under the BSD style license found in the -* LICENSE file in the root directory of this source tree. An additional grant -* of patent rights can be found in the PATENTS file in the same directory. -*) + * Copyright (c) 2009 - 2013 Monoidics ltd. + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) (** Symbolic Execution *) @@ -116,7 +116,9 @@ let rec apply_offlist match offlist, strexp with | [], Sil.Eexp (e, inst_curr) -> let inst_is_uninitialized = function - | Sil.Ialloc -> !Sil.curr_language <> Sil.Java (* java allocation initializes with default values *) + | Sil.Ialloc -> + (* java allocation initializes with default values *) + !Config.curr_language <> Config.Java | Sil.Iinitial -> true | _ -> false in let is_hidden_field () = @@ -326,7 +328,7 @@ module Builtin = struct type ret_typ = (Prop.normal Prop.t * Paths.Path.t) list type sym_exe_builtin = Cfg.cfg -> Cfg.Procdesc.t -> Sil.instr -> Sil.tenv -> Prop.normal Prop.t -> Paths.Path.t -> - Ident.t list -> (Sil.exp * Sil.typ) list -> Procname.t -> Sil.location -> ret_typ + Ident.t list -> (Sil.exp * Sil.typ) list -> Procname.t -> Location.t -> ret_typ (* builtin function names for which we do symbolic execution *) let builtin_functions = Procname.Hash.create 4 @@ -644,18 +646,13 @@ let proc_desc_copy cfg pdesc pname pname' = let open Cfg.Procdesc in create { cfg = cfg; - name = pname'; - proc_attributes = Sil.copy_proc_attributes (get_attributes pdesc); - is_defined = is_defined pdesc; - ret_type = get_ret_type pdesc; - formals = get_formals pdesc; - locals = get_locals pdesc; - captured = get_captured pdesc; - loc = get_loc pdesc; + proc_attributes = + { (Sil.copy_proc_attributes (get_attributes pdesc)) with + Sil.proc_name = pname'; }; }) let method_exists right_proc_name methods = - if !Sil.curr_language = Sil.Java then + if !Config.curr_language = Config.Java then list_exists (fun meth_name -> Procname.equal right_proc_name meth_name) methods else (* ObjC case *) Specs.summary_exists right_proc_name @@ -784,9 +781,9 @@ let call_constructor_url_update_args tenv cfg pname actual_params = (** Handles certain method calls in a special way *) let handle_special_cases_call tenv cfg pname actual_params = - if (!Sil.curr_language = Sil.Java) then + if (!Config.curr_language = Config.Java) then pname, (call_constructor_url_update_args tenv cfg pname actual_params) - else if (!Sil.curr_language = Sil.C_CPP) then + else if (!Config.curr_language = Config.C_CPP) then (redirect_shared_ptr tenv cfg pname actual_params), actual_params else pname, actual_params @@ -964,7 +961,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path false cfg pdesc tenv prop path ret_ids ret_typ_opt n_actual_params resolved_pname loc in let sentinel_result = - if !Sil.curr_language = Sil.C_CPP then + if !Config.curr_language = Config.C_CPP then sym_exe_check_variadic_sentinel_if_present cfg pdesc tenv prop_r path actual_params callee_pname loc else [(prop_r, path)] in let do_call (prop, path) = @@ -1206,7 +1203,7 @@ and call_unknown_or_scan is_scan cfg pdesc tenv pre path | _ -> false) actual_pars in (* in Java, assume that skip functions close resources passed as params *) - let pre' = if !Sil.curr_language = Sil.Java then remove_file_attribute pre else pre in + let pre' = if !Config.curr_language = Config.Java then remove_file_attribute pre else pre in let pre'' = add_constraints_on_retval pdesc pre' ret_ids ret_type_option callee_pname in let pre''' = add_constraints_on_actuals_by_ref pre'' actuals_by_ref callee_pname in if is_scan (* if scan function, don't mark anything with undef attributes *) @@ -1294,7 +1291,11 @@ and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc = match actual_pars, formal_types with | [], [] -> actual_pars | (e, t_e):: etl', t:: tl' -> - (e, if (!Config.Experiment.activate_subtyping_in_cpp || !Sil.curr_language = Sil.Java) then t_e else t) :: comb etl' tl' + (e, + if + (!Config.Experiment.activate_subtyping_in_cpp || + !Config.curr_language = Config.Java) + then t_e else t) :: comb etl' tl' | _,[] -> if !Config.developer_mode then Errdesc.warning_err (State.get_loc ()) "likely use of variable-arguments function, or function prototype missing@."; L.d_warning "likely use of variable-arguments function, or function prototype missing"; L.d_ln(); @@ -1315,7 +1316,7 @@ and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc = check_return_value_ignored (); (* In case we call an objc instance method we add and extra spec *) (* were the receiver is null and the semantics of the call is nop*) - if (!Sil.curr_language <> Sil.Java) && !Config.objc_method_call_semantics && + if (!Config.curr_language <> Config.Java) && !Config.objc_method_call_semantics && (Specs.get_attributes summary).Sil.is_objc_instance_method then handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc callee_pname loc path else (* non-objective-c method call. Standard tabulation *) @@ -1447,7 +1448,7 @@ module ModelBuiltins = struct Sil.Earray (size, [], Sil.inst_none) let extract_array_type typ = - if (!Sil.curr_language = Sil.Java) then + if (!Config.curr_language = Config.Java) then match typ with | Sil.Tptr ( Sil.Tarray (typ', _), _) -> Some typ' | _ -> None @@ -2237,7 +2238,6 @@ module ModelBuiltins = struct let __get_array_size = Builtin.register "__get_array_size" execute___get_array_size (* return the size of the array passed as a parameter *) let _ = Builtin.register "__get_hidden_field" execute___get_hidden_field (* return the value of a hidden field in the struct *) let __get_type_of = Builtin.register "__get_type_of" execute___get_type_of (* return the get the type of the allocated object passed as a parameter *) - let _ = Builtin.register "__infer_set_flag" execute_skip (** NOTE: __infer_set_flag should have been handled in the translation already (see frontend.ml) *) let __instanceof = Builtin.register "__instanceof" execute___instanceof (** [__instanceof(val,typ)] implements java's [val instanceof typ] *) let __cast = Builtin.register "__cast" execute___cast (** [__cast(val,typ)] implements java's [typ(val)] *) let __new = Builtin.register "__new" (execute_alloc Sil.Mnew false) (* like malloc, but always succeeds *) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index c2fd7d5b3..5a7466b8c 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -29,7 +29,8 @@ type deref_error = | Deref_freed of Sil.res_action (** dereference a freed pointer *) | Deref_minusone (** dereference -1 *) | Deref_null of Sil.path_pos (** dereference null *) - | Deref_undef of Procname.t * Sil.location * Sil.path_pos (** dereference a value coming from the given undefined function *) + (** dereference a value coming from the given undefined function *) + | Deref_undef of Procname.t * Location.t * Sil.path_pos | Deref_undef_exp (** dereference an undefined expression *) type invalid_res = @@ -462,7 +463,7 @@ let hpred_star_typing (hpred1 : Sil.hpred) (e2, te2) : Sil.hpred = (** Implementation of [*] between predicates and typings *) let sigma_star_typ (sigma1 : Sil.hpred list) (typings2 : (Sil.exp * Sil.exp) list) : Sil.hpred list = - if !Config.Experiment.activate_subtyping_in_cpp || !Sil.curr_language = Sil.Java then + if !Config.Experiment.activate_subtyping_in_cpp || !Config.curr_language = Config.Java then begin let typing_lhs_compare (e1, _) (e2, _) = Sil.exp_compare e1 e2 in let sigma1 = list_stable_sort hpred_lhs_compare sigma1 in @@ -829,7 +830,7 @@ let exe_spec let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in let posts = match ret_ids with - | [ret_id] when !Config.idempotent_getters && !Sil.curr_language = Sil.Java -> + | [ret_id] when !Config.idempotent_getters && !Config.curr_language = Config.Java -> (* if we have seen a previous call to the same function, only use specs whose return value is consistent with constraints on the return value of the previous call w.r.t to nullness. meant to eliminate false NPE warnings from the common "if (get() != null) get().something()" @@ -1076,7 +1077,9 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop r res_with_path_idents in let should_add_ret_attr _ = let is_likely_getter pn = list_length (Procname.java_get_parameters pn) = 0 in - !Config.idempotent_getters && !Sil.curr_language = Sil.Java && is_likely_getter callee_pname in + !Config.idempotent_getters && + !Config.curr_language = Config.Java && + is_likely_getter callee_pname in match ret_ids with | [ret_id] when should_add_ret_attr ()-> (* add attribute to remember what function call a return id came from *) diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index d60005873..2c5da35d5 100644 --- a/infer/src/backend/tabulation.mli +++ b/infer/src/backend/tabulation.mli @@ -39,4 +39,7 @@ val lookup_global_errors : 'a Prop.t -> Mangled.t option val d_splitting : splitting -> unit (** Execute the function call and return the list of results with return value *) -val exe_function_call: Sil.tenv -> Cfg.cfg -> Ident.t list -> Cfg.Procdesc.t -> Procname.t -> Sil.location -> (Sil.exp * Sil.typ) list -> Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list +val exe_function_call: + Sil.tenv -> Cfg.cfg -> Ident.t list -> Cfg.Procdesc.t -> Procname.t -> Location.t -> + (Sil.exp * Sil.typ) list -> Prop.normal Prop.t -> Paths.Path.t -> + (Prop.normal Prop.t * Paths.Path.t) list diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index 98d4e6626..ac4456596 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -1121,7 +1121,7 @@ module Escape = struct end -(** flags for a procedure, these can be set programmatically by __infer_set_flag: see frontend.ml *) +(** flags for a procedure *) type proc_flags = (string, string) Hashtbl.t let proc_flags_empty () : proc_flags = Hashtbl.create 1 diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli index 9ac821a40..b02123ffe 100644 --- a/infer/src/backend/utils.mli +++ b/infer/src/backend/utils.mli @@ -411,7 +411,7 @@ module Escape : sig end -(** flags for a procedure, these can be set programmatically by __infer_set_flag: see frontend.ml *) +(** flags for a procedure *) type proc_flags = (string, string) Hashtbl.t (** keys for proc_flags *) diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index 990c9d21e..8f2af663b 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -20,18 +20,19 @@ module PP = struct (** Print a range of lines of the source file in [loc], including [nbefore] lines before loc and [nafter] lines after [loc] *) let pp_loc_range linereader nbefore nafter fmt loc = - let printline n = match Printer.LineReader.from_loc linereader { loc with Sil.line = n } with - | Some s -> F.fprintf fmt "%s%s@\n" (if n = loc.Sil.line then "-->" else " ") s + let printline n = + match Printer.LineReader.from_loc linereader { loc with Location.line = n } with + | Some s -> F.fprintf fmt "%s%s@\n" (if n = loc.Location.line then "-->" else " ") s | _ -> () in - F.fprintf fmt "%s:%d@\n" (DB.source_file_to_string loc.Sil.file) loc.Sil.line; - for n = loc.Sil.line - nbefore to loc.Sil.line + nafter do printline n done + F.fprintf fmt "%s:%d@\n" (DB.source_file_to_string loc.Location.file) loc.Location.line; + for n = loc.Location.line - nbefore to loc.Location.line + nafter do printline n done end (* PP *) (** State that persists in the .specs files. *) module ST = struct let add summary key value = - proc_flags_add summary.Specs.proc_flags key value + proc_flags_add summary.Specs.attributes.Sil.proc_flags key value let pname_add proc_name key value = let summary = Specs.get_summary_unsafe proc_name in @@ -42,14 +43,14 @@ module ST = struct let pname_find proc_name key = if Procname.Set.mem proc_name !files_open then let summary = Specs.get_summary_unsafe proc_name in - proc_flags_find summary.Specs.proc_flags key + proc_flags_find summary.Specs.attributes.Sil.proc_flags key else begin match Specs.get_summary proc_name with | None -> raise Not_found | Some summary -> begin files_open := Procname.Set.add proc_name !files_open; - proc_flags_find summary.Specs.proc_flags key + proc_flags_find summary.Specs.attributes.Sil.proc_flags key end end @@ -141,7 +142,7 @@ module ST = struct begin if !verbose then begin - let file = DB.source_file_to_string loc.Sil.file in + let file = DB.source_file_to_string loc.Location.file in L.stdout "%s: %s: %s@." kind file @@ -312,8 +313,11 @@ let callback_monitor_nullcheck all_procs get_proc_desc idenv tenv proc_name proc not (Sil.ExpSet.exists (fun exp -> equal_formal_param exp formal_name) !checks_to_formals) in let missing = list_filter was_not_found formal_names in let loc = Cfg.Procdesc.get_loc proc_desc in - let pp_file_loc fmt () = F.fprintf fmt "%s:%d" (DB.source_file_to_string loc.Sil.file) loc.Sil.line in - L.stdout "Null Checks of Formal Parameters: %d out of %d parameters checked (missing checks on: %a)[%a]@." nchecks nformals (pp_seq Mangled.pp) missing pp_file_loc (); + let pp_file_loc fmt () = + F.fprintf fmt "%s:%d" (DB.source_file_to_string loc.Location.file) loc.Location.line in + L.stdout "Null Checks of Formal Parameters: "; + L.stdout "%d out of %d parameters checked (missing checks on: %a)[%a]@." + nchecks nformals (pp_seq Mangled.pp) missing pp_file_loc (); let linereader = Printer.LineReader.create () in L.stdout "%a@." (PP.pp_loc_range linereader 10 10) loc diff --git a/infer/src/checkers/checkers.mli b/infer/src/checkers/checkers.mli index 386aae742..aa3099eb4 100644 --- a/infer/src/checkers/checkers.mli +++ b/infer/src/checkers/checkers.mli @@ -22,10 +22,10 @@ module ST : sig Procname.t -> Cfg.Procdesc.t -> string -> - Sil.location -> + Location.t -> ?advice: string option -> ?field_name: Ident.fieldname option -> - ?origin_loc: Sil.location option -> + ?origin_loc: Location.t option -> ?exception_kind: (string -> Localise.error_desc -> exn) -> ?always_report: bool -> string -> @@ -39,7 +39,7 @@ end (* ST *) module PP : sig (** Print a range of lines of the source file in [loc], including [nbefore] lines before loc and [nafter] lines after [loc] *) - val pp_loc_range : Printer.LineReader.t -> int -> int -> Format.formatter -> Sil.location -> unit + val pp_loc_range : Printer.LineReader.t -> int -> int -> Format.formatter -> Location.t -> unit end (* PP *) val callback_check_access : Callbacks.proc_callback_t diff --git a/infer/src/checkers/codeQuery.ml b/infer/src/checkers/codeQuery.ml index 6dd0e173a..3c2c7e9da 100644 --- a/infer/src/checkers/codeQuery.ml +++ b/infer/src/checkers/codeQuery.ml @@ -47,7 +47,9 @@ module Err = struct } in [(Specs.spec_normalize spec)] in let new_summ = { old_summ with - Specs.loc = Cfg.Procdesc.get_loc proc_desc; + Specs.attributes = + { old_summ.Specs.attributes with + Sil.loc = Cfg.Procdesc.get_loc proc_desc }; Specs.nodes = nodes; Specs.payload = Specs.PrePosts specs } in Specs.add_summary proc_name new_summ diff --git a/infer/src/checkers/eradicate.ml b/infer/src/checkers/eradicate.ml index 422e741df..611fcf1b4 100644 --- a/infer/src/checkers/eradicate.ml +++ b/infer/src/checkers/eradicate.ml @@ -58,13 +58,13 @@ struct let new_summ = { old_summ with - Specs.loc = Cfg.Procdesc.get_loc proc_desc; Specs.nodes = nodes; Specs.payload = Extension.mkpayload final_typestate_opt; Specs.attributes = { old_summ.Specs.attributes with - Sil.method_annotation = method_annotation + Sil.loc = Cfg.Procdesc.get_loc proc_desc; + method_annotation; }; } in Specs.add_summary proc_name new_summ diff --git a/infer/src/checkers/eradicateChecks.ml b/infer/src/checkers/eradicateChecks.ml index ccf668502..dfe0ef264 100644 --- a/infer/src/checkers/eradicateChecks.ml +++ b/infer/src/checkers/eradicateChecks.ml @@ -142,7 +142,7 @@ let check_condition case_zero find_canonical_duplicate get_proc_desc curr_pname throwable_found := true | _ -> () in let do_node n = - if Sil.loc_equal loc (Cfg.Node.get_loc n) + if Location.equal loc (Cfg.Node.get_loc n) then list_iter do_instr (Cfg.Node.get_instrs n) in Cfg.Procdesc.iter_nodes do_node (Cfg.Node.get_proc_desc node); !throwable_found in diff --git a/infer/src/checkers/printfArgs.ml b/infer/src/checkers/printfArgs.ml index a23aeba87..d1d1c2825 100644 --- a/infer/src/checkers/printfArgs.ml +++ b/infer/src/checkers/printfArgs.ml @@ -133,7 +133,7 @@ let callback_printf_args (* Check if format string lines up with arguments *) let rec check_type_names instr_loc n_arg instr_proc_name fmt_type_names arg_type_names = let instr_name = Procname.to_simplified_string instr_proc_name in - let instr_line = Sil.loc_to_string instr_loc in + let instr_line = Location.to_string instr_loc in match (fmt_type_names, arg_type_names) with | ft:: fs, gt:: gs -> if not (format_type_matches_given_type ft gt) then diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index e9160382c..1f1684466 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -36,19 +36,19 @@ let active_procedure_checkers () = RepeatedCallsChecker.callback_check_repeated_calls, checkers_enabled; PrintfArgs.callback_printf_args, checkers_enabled; ] in - list_map (fun (x, y) -> (x, y, Some Sil.Java)) l in + list_map (fun (x, y) -> (x, y, Some Config.Java)) l in let c_cpp_checkers = let l = [ Checkers.callback_print_c_method_calls, false; CheckDeadCode.callback_check_dead_code, checkers_enabled; ] in - list_map (fun (x, y) -> (x, y, Some Sil.C_CPP)) l in + list_map (fun (x, y) -> (x, y, Some Config.C_CPP)) l in java_checkers @ c_cpp_checkers let active_cluster_checkers () = - [(Checkers.callback_check_cluster_access, false, Some Sil.Java)] + [(Checkers.callback_check_cluster_access, false, Some Config.Java)] let register () = let register registry (callback, active, language_opt) = diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml index 960018866..2103aeee4 100644 --- a/infer/src/checkers/repeatedCallsChecker.ml +++ b/infer/src/checkers/repeatedCallsChecker.ml @@ -63,9 +63,9 @@ struct (** Check if the procedure performs an allocation operation. If [paths] is AllPaths, check if an allocation happens on all paths. If [paths] is SomePath, check if a path with an allocation exists. *) - let proc_performs_allocation pdesc paths : Sil.location option = + let proc_performs_allocation pdesc paths : Location.t option = - let node_allocates node : Sil.location option = + let node_allocates node : Location.t option = let found = ref None in let proc_is_new pn = Procname.equal pn SymExec.ModelBuiltins.__new || @@ -79,8 +79,8 @@ struct !found in let module DFAllocCheck = Dataflow.MakeDF(struct - type t = Sil.location option - let equal = opt_equal Sil.loc_equal + type t = Location.t option + let equal = opt_equal Location.equal let _join _paths l1o l2o = (* join with left priority *) match l1o, l2o with | None, None -> @@ -136,9 +136,9 @@ struct let description = Printf.sprintf "call to %s seen before on line %d (may allocate at %s:%n)" (Procname.to_simplified_string callee_pname) - loc_old.Sil.line - (DB.source_file_to_string alloc_loc.Sil.file) - alloc_loc.Sil.line in + loc_old.Location.line + (DB.source_file_to_string alloc_loc.Location.file) + alloc_loc.Location.line in Checkers.ST.report_error curr_pname curr_pdesc checkers_repeated_calls_name loc description | None -> () diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml index 9b0c69915..223f69a05 100644 --- a/infer/src/checkers/typeCheck.ml +++ b/infer/src/checkers/typeCheck.ml @@ -121,7 +121,7 @@ module ComplexExpressions = struct end (* ComplexExpressions *) type check_return_type = - Procname.t -> Cfg.Procdesc.t -> Sil.typ -> Sil.typ option -> Sil.location -> unit + Procname.t -> Cfg.Procdesc.t -> Sil.typ -> Sil.typ option -> Location.t -> unit type find_canonical_duplicate = Cfg.Node.t -> Cfg.Node.t diff --git a/infer/src/checkers/typeCheck.mli b/infer/src/checkers/typeCheck.mli index df25f8522..5c632e5c5 100644 --- a/infer/src/checkers/typeCheck.mli +++ b/infer/src/checkers/typeCheck.mli @@ -11,7 +11,7 @@ (** Module type for the type checking functions. *) type check_return_type = - Procname.t -> Cfg.Procdesc.t -> Sil.typ -> Sil.typ option -> Sil.location -> unit + Procname.t -> Cfg.Procdesc.t -> Sil.typ -> Sil.typ option -> Location.t -> unit type find_canonical_duplicate = Cfg.Node.t -> Cfg.Node.t diff --git a/infer/src/checkers/typeErr.ml b/infer/src/checkers/typeErr.ml index e3b6087aa..4435b8666 100644 --- a/infer/src/checkers/typeErr.ml +++ b/infer/src/checkers/typeErr.ml @@ -48,7 +48,7 @@ end (* InstrRef *) type origin_descr = string * - Sil.location option * + Location.t option * Annotations.annotated_signature option (* callee signature *) type parameter_not_nullable = @@ -56,7 +56,7 @@ type parameter_not_nullable = string * (* description *) int * (* parameter number *) Procname.t * - Sil.location * (* callee location *) + Location.t * (* callee location *) origin_descr (** Instance of an error *) @@ -122,7 +122,7 @@ module H = Hashtbl.Make(struct string_equal s1 s2 && int_equal n1 n2 && Procname.equal pn1 pn2 && - Sil.loc_equal cl1 cl2 + Location.equal cl1 cl2 | Parameter_annotation_inconsistent _, _ | _, Parameter_annotation_inconsistent _ -> false | Return_annotation_inconsistent (ann1, pn1, od1), @@ -190,7 +190,7 @@ module H = Hashtbl.Make(struct end (* H *)) type err_state = { - loc: Sil.location; (** location of the error *) + loc: Location.t; (** location of the error *) mutable always: bool; (** always fires on its associated node *) } @@ -292,10 +292,10 @@ type st_report_error = Procname.t -> Cfg.Procdesc.t -> string -> - Sil.location -> + Location.t -> ?advice: string option -> ?field_name: Ident.fieldname option -> - ?origin_loc: Sil.location option -> + ?origin_loc: Location.t option -> ?exception_kind: (string -> Localise.error_desc -> exn) -> ?always_report: bool -> string -> @@ -309,14 +309,14 @@ let report_error_now let do_print_base ew_string kind_s s = L.stdout "%s %s in %s %s@." ew_string kind_s (Procname.java_get_method proc_name) s in let do_print ew_string kind_s s = - L.stdout "%s:%d " (DB.source_file_to_string loc.Sil.file) loc.Sil.line; + L.stdout "%s:%d " (DB.source_file_to_string loc.Location.file) loc.Location.line; do_print_base ew_string kind_s s in let do_print_demo ew_string kind_s s = (* demo mode print for Eclipse and ocaml plugin *) let process_path s = filename_to_relative (Sys.getcwd ()) s in L.stdout "File %s, line %d, characters 0-10:\n" - (process_path (DB.source_file_to_string loc.Sil.file)) - loc.Sil.line; + (process_path (DB.source_file_to_string loc.Location.file)) + loc.Location.line; do_print_base ew_string kind_s s in let is_err, kind_s, description, advice, field_name, origin_loc = match err_instance with diff --git a/infer/src/checkers/typeErr.mli b/infer/src/checkers/typeErr.mli index 679d7bf7a..228ca10c8 100644 --- a/infer/src/checkers/typeErr.mli +++ b/infer/src/checkers/typeErr.mli @@ -33,7 +33,7 @@ end (* Strict *) type origin_descr = string * - Sil.location option * + Location.t option * Annotations.annotated_signature option (* callee signature *) type parameter_not_nullable = @@ -41,7 +41,7 @@ type parameter_not_nullable = string * (* description *) int * (* parameter number *) Procname.t * - Sil.location * (* callee location *) + Location.t * (* callee location *) origin_descr (** Instance of an error *) @@ -67,10 +67,10 @@ type st_report_error = Procname.t -> Cfg.Procdesc.t -> string -> - Sil.location -> + Location.t -> ?advice: string option -> ?field_name: Ident.fieldname option -> - ?origin_loc: Sil.location option -> + ?origin_loc: Location.t option -> ?exception_kind: (string -> Localise.error_desc -> exn) -> ?always_report: bool -> string -> @@ -79,7 +79,7 @@ type st_report_error = val report_error : st_report_error -> (Cfg.Node.t -> Cfg.Node.t) -> Cfg.Node.t -> - err_instance -> InstrRef.t option -> Sil.location -> + err_instance -> InstrRef.t option -> Location.t -> Procname.t -> unit val report_forall_checks_and_reset : st_report_error -> Procname.t -> unit diff --git a/infer/src/checkers/typeOrigin.ml b/infer/src/checkers/typeOrigin.ml index 50c58ba6c..af60631cf 100644 --- a/infer/src/checkers/typeOrigin.ml +++ b/infer/src/checkers/typeOrigin.ml @@ -16,11 +16,11 @@ open Utils type proc_origin = - Procname.t * Sil.location * Annotations.annotated_signature * bool (* is_library *) + Procname.t * Location.t * Annotations.annotated_signature * bool (* is_library *) type t = - | Const of Sil.location - | Field of Ident.fieldname * Sil.location + | Const of Location.t + | Field of Ident.fieldname * Location.t | Formal of string | Proc of proc_origin | New @@ -29,12 +29,12 @@ type t = let equal o1 o2 = match o1, o2 with | Const loc1, Const loc2 -> - Sil.loc_equal loc1 loc2 + Location.equal loc1 loc2 | Const _, _ | _, Const _ -> false | Field (fn1, loc1), Field (fn2, loc2) -> Ident.fieldname_equal fn1 fn2 && - Sil.loc_equal loc1 loc2 + Location.equal loc1 loc2 | Field _, _ | _, Field _ -> false | Formal s1, Formal s2 -> @@ -43,7 +43,7 @@ let equal o1 o2 = match o1, o2 with | _, Formal _ -> false | Proc (pn1, loc1, as1, b1), Proc (pn2, loc2, as2, b2) -> Procname.equal pn1 pn2 && - Sil.loc_equal loc1 loc2 && + Location.equal loc1 loc2 && Annotations.equal as1 as2 && bool_equal b1 b2 | Proc _, _ @@ -70,7 +70,7 @@ let to_string = function let get_description origin = let atline loc = - " at line " ^ (string_of_int loc.Sil.line) in + " at line " ^ (string_of_int loc.Location.line) in match origin with | Const loc -> Some ("null constant" ^ atline loc, Some loc, None) diff --git a/infer/src/checkers/typeOrigin.mli b/infer/src/checkers/typeOrigin.mli index b15924b9c..68cf2a5cc 100644 --- a/infer/src/checkers/typeOrigin.mli +++ b/infer/src/checkers/typeOrigin.mli @@ -9,11 +9,11 @@ type proc_origin = (** Case Proc *) - Procname.t * Sil.location * Annotations.annotated_signature * bool (* is_library *) + Procname.t * Location.t * Annotations.annotated_signature * bool (* is_library *) type t = - | Const of Sil.location (** A constant in the source *) - | Field of Ident.fieldname * Sil.location (** A field access *) + | Const of Location.t (** A constant in the source *) + | Field of Ident.fieldname * Location.t (** A field access *) | Formal of string (** A formal parameter *) | Proc of proc_origin (** A procedure call *) | New (** A new object creation *) diff --git a/infer/src/checkers/typeState.ml b/infer/src/checkers/typeState.ml index 789b018b1..f50f15c64 100644 --- a/infer/src/checkers/typeState.ml +++ b/infer/src/checkers/typeState.ml @@ -35,7 +35,7 @@ module M = Map.Make (struct type t = Sil.exp let compare = Sil.exp_compare end) -type range = Sil.typ * TypeAnnotation.t * (Sil.location list) +type range = Sil.typ * TypeAnnotation.t * (Location.t list) type 'a t = { @@ -49,7 +49,7 @@ let empty ext = extension = ext.empty; } -let locs_compare = list_compare Sil.loc_compare +let locs_compare = list_compare Location.compare let locs_equal locs1 locs2 = locs_compare locs1 locs2 = 0 let range_equal (typ1, ta1, locs1) (typ2, ta2, locs2) = @@ -60,7 +60,7 @@ let equal t1 t2 = M.equal range_equal t1.map t2.map let pp ext fmt typestate = - let pp_loc fmt loc = F.fprintf fmt "%d" loc.Sil.line in + let pp_loc fmt loc = F.fprintf fmt "%d" loc.Location.line in let pp_locs fmt locs = F.fprintf fmt " [%a]" (pp_seq pp_loc) locs in let pp_one exp (typ, ta, locs) = F.fprintf fmt " %a -> [%s] %s %a%a@\n" @@ -78,7 +78,7 @@ exception JoinFail let type_join typ1 typ2 = if PatternMatch.type_is_object typ1 then typ2 else typ1 let locs_join locs1 locs2 = - list_merge_sorted_nodup Sil.loc_compare [] locs1 locs2 + list_merge_sorted_nodup Location.compare [] locs1 locs2 (** Add a list of locations to a range. *) let range_add_locs (typ, ta, locs1) locs2 = diff --git a/infer/src/checkers/typeState.mli b/infer/src/checkers/typeState.mli index aa6685d76..e7ca81bb3 100644 --- a/infer/src/checkers/typeState.mli +++ b/infer/src/checkers/typeState.mli @@ -28,7 +28,7 @@ type 'a ext = (** Typestate extended with elements of type 'a. *) type 'a t -type range = Sil.typ * TypeAnnotation.t * (Sil.location list) +type range = Sil.typ * TypeAnnotation.t * (Location.t list) val add_id : Ident.t -> range -> 'a t -> 'a t val add_pvar : Sil.pvar -> range -> 'a t -> 'a t @@ -39,6 +39,6 @@ val join : 'a ext -> 'a t -> 'a t -> 'a t val lookup_id : Ident.t -> 'a t -> range option val lookup_pvar : Sil.pvar -> 'a t -> range option val pp : 'a ext -> Format.formatter -> 'a t -> unit -val range_add_locs : range -> (Sil.location list) -> range +val range_add_locs : range -> (Location.t list) -> range val remove_id : Ident.t -> 'a t -> 'a t val set_extension : 'a t -> 'a -> 'a t diff --git a/infer/src/clang/cArithmetic_trans.mli b/infer/src/clang/cArithmetic_trans.mli index 3709b6ba8..13afea2e6 100644 --- a/infer/src/clang/cArithmetic_trans.mli +++ b/infer/src/clang/cArithmetic_trans.mli @@ -11,14 +11,17 @@ val bin_op_to_string : Clang_ast_t.binary_operator_info -> string -val binary_operation_instruction : CContext.t -> Clang_ast_t.binary_operator_info -> Sil.exp -> Sil.typ -> Sil.exp -> - Sil.location -> bool -> Sil.exp * Sil.instr list * Ident.t list +val binary_operation_instruction : + CContext.t -> Clang_ast_t.binary_operator_info -> Sil.exp -> Sil.typ -> Sil.exp -> + Location.t -> bool -> Sil.exp * Sil.instr list * Ident.t list -val unary_operation_instruction : Clang_ast_t.unary_operator_info -> Sil.exp -> Sil.typ -> Sil.location -> +val unary_operation_instruction : + Clang_ast_t.unary_operator_info -> Sil.exp -> Sil.typ -> Location.t -> Ident.t list * Sil.exp * Sil.instr list val compound_assignment_binary_operation_instruction : Clang_ast_t.binary_operator_info -> Sil.exp -> - Sil.typ -> Sil.exp -> Sil.location -> Ident.t list * Sil.exp * Sil.instr list - -val assignment_arc_mode : CContext.t -> Sil.exp -> Sil.typ -> Sil.exp -> Sil.location -> bool -> bool -> Sil.exp * Sil.instr list * Ident.t list + Sil.typ -> Sil.exp -> Location.t -> Ident.t list * Sil.exp * Sil.instr list +val assignment_arc_mode : + CContext.t -> Sil.exp -> Sil.typ -> Sil.exp -> Location.t -> bool -> bool -> + Sil.exp * Sil.instr list * Ident.t list diff --git a/infer/src/clang/cEnum_decl.ml b/infer/src/clang/cEnum_decl.ml index d3b9a2efd..b9c363cf5 100644 --- a/infer/src/clang/cEnum_decl.ml +++ b/infer/src/clang/cEnum_decl.ml @@ -10,33 +10,35 @@ (** Translate an enumeration declaration by adding it to the tenv and *) (** translating the code and adding it to a fake procdesc *) +open Utils open CFrontend_utils let create_empty_procdesc () = - let procname = Procname.from_string_c_fun "__INFER_$GLOBAL_VAR_env" in + let proc_name = Procname.from_string_c_fun "__INFER_$GLOBAL_VAR_env" in let open Cfg.Procdesc in let proc_attributes = { Sil.access = Sil.Default; - Sil.exceptions = []; - Sil.is_abstract = false; - Sil.is_bridge_method = false; - Sil.is_objc_instance_method = false; - Sil.is_synthetic_method = false; - Sil.language = Sil.C_CPP; - Sil.func_attributes = []; - Sil.method_annotation = Sil.method_annotation_empty; - Sil.is_generated = false; + captured = []; + exceptions = []; + formals = []; + func_attributes = []; + is_abstract = false; + is_bridge_method = false; + is_defined = false; + is_generated = false; + is_objc_instance_method = false; + is_synthetic_method = false; + language = Config.C_CPP; + loc = Location.loc_none; + locals = []; + method_annotation = Sil.method_annotation_empty; + proc_flags = proc_flags_empty (); + proc_name; + ret_type = Sil.Tvoid; } in create { cfg = Cfg.Node.create_cfg (); - name = procname; - is_defined = false; - ret_type = Sil.Tvoid; - formals = []; - locals = []; - captured = []; - loc = Sil.loc_none; proc_attributes = proc_attributes; } diff --git a/infer/src/clang/cFrontend.ml b/infer/src/clang/cFrontend.ml index 3e0b475a3..b8594a3cc 100644 --- a/infer/src/clang/cFrontend.ml +++ b/infer/src/clang/cFrontend.ml @@ -120,7 +120,7 @@ let compute_icfg tenv source_file ast = | _ -> assert false (* NOTE: Assumes that an AST alsways starts with a TranslationUnitDecl *) let init_global_state source_file = - Sil.curr_language := Sil.C_CPP; + Config.curr_language := Config.C_CPP; DB.current_source := source_file; DB.Results_dir.init (); Ident.reset_name_generator (); diff --git a/infer/src/clang/cLocation.ml b/infer/src/clang/cLocation.ml index 72ed6d3d6..7f02779c6 100644 --- a/infer/src/clang/cLocation.ml +++ b/infer/src/clang/cLocation.ml @@ -75,9 +75,9 @@ let clang_to_sil_location clang_loc parent_line_number procdesc_opt = match procdesc_opt with | Some procdesc -> let proc_loc = Cfg.Procdesc.get_loc procdesc in - if (DB.source_file_equal proc_loc.Sil.file DB.source_file_empty) then + if (DB.source_file_equal proc_loc.Location.file DB.source_file_empty) then !curr_file, !Config.nLOC - else proc_loc.Sil.file, proc_loc.Sil.nLOC + else proc_loc.Location.file, proc_loc.Location.nLOC | None -> match clang_loc.Clang_ast_t.sl_file with | Some f -> @@ -88,14 +88,14 @@ let clang_to_sil_location clang_loc parent_line_number procdesc_opt = else -1 in file_db, nloc | None -> !curr_file, !Config.nLOC in - { Sil.line = line; Sil.col = col; Sil.file = file; Sil.nLOC = nLOC } + { Location.line = line; Location.col = col; Location.file = file; Location.nLOC = nLOC } let should_translate_lib source_range = if !CFrontend_config.no_translate_libs then match source_range with (loc_start, loc_end) -> let loc_start = choose_sloc_to_update_curr_file loc_start loc_end in let loc = clang_to_sil_location loc_start (-1) None in - DB.source_file_equal loc.Sil.file !DB.current_source + DB.source_file_equal loc.Location.file !DB.current_source else true let should_translate_enum source_range = @@ -103,7 +103,7 @@ let should_translate_enum source_range = match source_range with (loc_start, loc_end) -> let loc_start = choose_sloc_to_update_curr_file loc_start loc_end in let loc = clang_to_sil_location loc_start (-1) None in - DB.source_file_equal loc.Sil.file !DB.current_source + DB.source_file_equal loc.Location.file !DB.current_source else true let get_sil_location_from_range source_range prefer_first = diff --git a/infer/src/clang/cLocation.mli b/infer/src/clang/cLocation.mli index a6f979c66..8fe5d6845 100644 --- a/infer/src/clang/cLocation.mli +++ b/infer/src/clang/cLocation.mli @@ -18,9 +18,9 @@ val current_source_file : DB.source_file ref val curr_file : DB.source_file ref val clang_to_sil_location : Clang_ast_t.source_location -> int -> Cfg.Procdesc.t option -> - Sil.location + Location.t -val get_sil_location : Clang_ast_t.stmt_info -> int -> CContext.t -> Sil.location +val get_sil_location : Clang_ast_t.stmt_info -> int -> CContext.t -> Location.t val get_line : Clang_ast_t.stmt_info -> int -> int @@ -36,4 +36,4 @@ val check_source_file : string -> unit val source_file_from_path : string -> DB.source_file -val get_sil_location_from_range : Clang_ast_t.source_range -> bool -> Sil.location +val get_sil_location_from_range : Clang_ast_t.source_range -> bool -> Location.t diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 03d7f2ffe..85c7c24d9 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -240,8 +240,8 @@ let should_create_procdesc cfg procname defined generated = (** Creates a procedure description. *) let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = let defined = not ((list_length fbody) == 0) in - let procname = CMethod_signature.ms_get_name ms in - let pname = Procname.to_string procname in + let proc_name = CMethod_signature.ms_get_name ms in + let pname = Procname.to_string proc_name in let attributes = sil_func_attributes_of_attributes (CMethod_signature.ms_get_attributes ms) in let is_generated = CMethod_signature.ms_is_generated ms in let create_new_procdesc () = @@ -262,26 +262,27 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = let proc_attributes = { Sil.access = Sil.Default; - Sil.exceptions = []; - Sil.is_abstract = false; - Sil.is_bridge_method = false; - Sil.is_objc_instance_method = is_objc_inst_method; - Sil.is_synthetic_method = false; - Sil.language = Sil.C_CPP; - Sil.func_attributes = attributes; - Sil.method_annotation = Sil.method_annotation_empty; - Sil.is_generated = is_generated; + captured = captured'; + exceptions = []; + formals; + func_attributes = attributes; + is_abstract = false; + is_bridge_method = false; + is_defined = defined; + is_generated; + is_objc_instance_method = is_objc_inst_method; + is_synthetic_method = false; + language = Config.C_CPP; + loc = loc_start; + locals = []; + method_annotation = Sil.method_annotation_empty; + proc_flags = proc_flags_empty (); + proc_name; + ret_type; } in create { - cfg = cfg; - name = procname; - is_defined = defined; - ret_type = ret_type; - formals = formals; - locals = []; - captured = captured'; - loc = loc_start; - proc_attributes = proc_attributes; + cfg; + proc_attributes; } in if defined then (if !Config.arc_mode then @@ -293,13 +294,13 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_exit_node procdesc exit_node) in let generated = CMethod_signature.ms_is_generated ms in - if should_create_procdesc cfg procname defined generated then + if should_create_procdesc cfg proc_name defined generated then (create_new_procdesc (); true) else false (** Create a procdesc for objc methods whose signature cannot be found. *) -let create_external_procdesc cfg procname is_objc_inst_method type_opt = - match Cfg.Procdesc.find_from_name cfg procname with +let create_external_procdesc cfg proc_name is_objc_inst_method type_opt = + match Cfg.Procdesc.find_from_name cfg proc_name with | Some _ -> () | None -> let ret_type, formals = @@ -307,31 +308,32 @@ let create_external_procdesc cfg procname is_objc_inst_method type_opt = | Some (ret_type, arg_types) -> ret_type, list_map (fun typ -> ("x", typ)) arg_types | None -> Sil.Tvoid, []) in - let loc = Sil.loc_none in + let loc = Location.loc_none in let _ = let open Cfg.Procdesc in let proc_attributes = { Sil.access = Sil.Default; - Sil.exceptions = []; - Sil.is_abstract = false; - Sil.is_bridge_method = false; - Sil.is_objc_instance_method = is_objc_inst_method; - Sil.is_synthetic_method = false; - Sil.language = Sil.C_CPP; - Sil.func_attributes = []; - Sil.method_annotation = Sil.method_annotation_empty; - Sil.is_generated = false; + captured = []; + exceptions = []; + formals; + func_attributes = []; + is_abstract = false; + is_bridge_method = false; + is_defined = false; + is_generated = false; + is_objc_instance_method = is_objc_inst_method; + is_synthetic_method = false; + language = Config.C_CPP; + loc; + locals = []; + method_annotation = Sil.method_annotation_empty; + proc_flags = proc_flags_empty (); + proc_name; + ret_type; } in create { cfg = cfg; - name = procname; - is_defined = false; - ret_type = ret_type; - formals = formals; - locals = []; - captured = []; - loc = loc; proc_attributes = proc_attributes; } in () diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 35ef1953d..3613d86a7 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -193,7 +193,8 @@ struct let try_claim_priority_node trans_state stmt_info = match trans_state.priority with | Free -> - Printing.log_out "Priority is free. Locking priority node in %s\n@." stmt_info.Clang_ast_t.si_pointer; + Printing.log_out "Priority is free. Locking priority node in %s\n@." + stmt_info.Clang_ast_t.si_pointer; { trans_state with priority = Busy stmt_info.Clang_ast_t.si_pointer } | _ -> Printing.log_out "Priority busy in %s. No claim possible\n@." stmt_info.Clang_ast_t.si_pointer; @@ -704,11 +705,11 @@ let assign_default_params params_stmt class_name_opt stmt ~is_cxx_method = (let args = CMethod_signature.ms_get_args callee_ms in let args = if is_cxx_method then match args with _::tl -> tl | _ -> assert false else args in - let replace_default_arg param = - match param with - | Clang_ast_t.CXXDefaultArgExpr _, (_, _, Some default_instr) -> - default_instr - | instr, _ -> instr in + let replace_default_arg param = + match param with + | Clang_ast_t.CXXDefaultArgExpr _, (_, _, Some default_instr) -> + default_instr + | instr, _ -> instr in try let params_args = list_combine params_stmt args in list_map replace_default_arg params_args diff --git a/infer/src/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli index 6c62a875e..1329a3240 100644 --- a/infer/src/clang/cTrans_utils.mli +++ b/infer/src/clang/cTrans_utils.mli @@ -56,15 +56,18 @@ val fix_param_exps_mismatch : 'a list -> (Sil.exp * Sil.typ) list -> (Sil.exp * val get_selector_receiver : Clang_ast_t.obj_c_message_expr_info -> string * Clang_ast_t.receiver_kind -val define_condition_side_effects : CContext.t -> (Sil.exp * Sil.typ) list -> Sil.instr list -> Sil.location -> +val define_condition_side_effects : + CContext.t -> (Sil.exp * Sil.typ) list -> Sil.instr list -> Location.t -> (Sil.exp * Sil.typ) list * Sil.instr list val extract_stmt_from_singleton : Clang_ast_t.stmt list -> string -> Clang_ast_t.stmt val is_null_stmt : Clang_ast_t.stmt -> bool -val compute_instr_ids_exp_to_parent : Clang_ast_t.stmt_info -> Sil.instr list -> Ident.t list -> (Sil.exp * Sil.typ) list -> - Sil.exp -> Sil.typ -> Sil.location -> priority_node -> Sil.instr list * Ident.t list * (Sil.exp * Sil.typ) list +val compute_instr_ids_exp_to_parent : + Clang_ast_t.stmt_info -> Sil.instr list -> Ident.t list -> (Sil.exp * Sil.typ) list -> + Sil.exp -> Sil.typ -> Location.t -> priority_node -> + Sil.instr list * Ident.t list * (Sil.exp * Sil.typ) list val get_name_decl_ref_exp_info : Clang_ast_t.decl_ref_expr_info -> Clang_ast_t.stmt_info -> string @@ -78,12 +81,13 @@ val is_member_exp : Clang_ast_t.stmt -> bool val get_type_from_exp_stmt : Clang_ast_t.stmt -> Clang_ast_t.qual_type -val cast_operation : CContext.t -> Clang_ast_t.cast_kind -> (Sil.exp * Sil.typ) list -> Sil.typ -> Sil.location -> +val cast_operation : + CContext.t -> Clang_ast_t.cast_kind -> (Sil.exp * Sil.typ) list -> Sil.typ -> Location.t -> bool -> Ident.t list * Sil.instr list * Sil.exp -val trans_assertion_failure : Sil.location -> CContext.t -> trans_result +val trans_assertion_failure : Location.t -> CContext.t -> trans_result -val trans_assume_false : Sil.location -> CContext.t -> Cfg.Node.t list -> trans_result +val trans_assume_false : Location.t -> CContext.t -> Cfg.Node.t list -> trans_result val is_owning_method : Clang_ast_t.stmt -> bool @@ -95,16 +99,19 @@ val contains_opaque_value_expr : Clang_ast_t.stmt -> bool val get_decl_ref_info : Clang_ast_t.stmt -> int -> string * int -val builtin_trans : trans_state -> Sil.location -> Clang_ast_t.stmt_info -> +val builtin_trans : trans_state -> Location.t -> Clang_ast_t.stmt_info -> Sil.typ -> Procname.t option -> trans_result option -val alloc_trans : trans_state -> Sil.location -> Clang_ast_t.stmt_info -> Sil.typ -> bool -> trans_result +val alloc_trans : + trans_state -> Location.t -> Clang_ast_t.stmt_info -> Sil.typ -> bool -> trans_result -val new_or_alloc_trans : trans_state -> Sil.location -> Clang_ast_t.stmt_info -> string -> string -> trans_result +val new_or_alloc_trans : + trans_state -> Location.t -> Clang_ast_t.stmt_info -> string -> string -> trans_result -val cpp_new_trans : trans_state -> Sil.location -> Clang_ast_t.stmt_info -> Sil.typ -> trans_result +val cpp_new_trans : trans_state -> Location.t -> Clang_ast_t.stmt_info -> Sil.typ -> trans_result -val cast_trans : CContext.t -> (Sil.exp * Sil.typ) list -> Sil.location -> Procname.t option -> Sil.typ -> +val cast_trans : + CContext.t -> (Sil.exp * Sil.typ) list -> Location.t -> Procname.t option -> Sil.typ -> (Ident.t * Sil.instr * Sil.exp) option (** Module for creating cfg nodes and other utility functions related to them. *) @@ -115,12 +122,13 @@ sig val need_unary_op_node : Clang_ast_t.unary_operator_info -> bool val create_node : Cfg.Node.nodekind -> Ident.t list -> Sil.instr list -> - Sil.location -> CContext.t -> Cfg.Node.t + Location.t -> CContext.t -> Cfg.Node.t val is_join_node : Cfg.Node.t -> bool - val create_prune_node : bool -> (Sil.exp * Sil.typ) list -> Ident.t list -> Sil.instr list -> Sil.location -> Sil.if_kind -> - CContext.t -> Cfg.Node.t + val create_prune_node : + bool -> (Sil.exp * Sil.typ) list -> Ident.t list -> Sil.instr list -> Location.t -> + Sil.if_kind -> CContext.t -> Cfg.Node.t val is_prune_node : Cfg.Node.t -> bool @@ -156,14 +164,15 @@ sig (* Used for function call and method call. It deals with creating or not *) (* a cfg node depending of owning the priority_node and the nodes returned *) (* by the parameters of the call *) - val compute_results_to_parent : trans_state -> Sil.location -> string -> Clang_ast_t.stmt_info -> trans_result -> trans_result + val compute_results_to_parent : + trans_state -> Location.t -> string -> Clang_ast_t.stmt_info -> trans_result -> trans_result end (** Module for translating goto instructions by keeping a map of labels. *) module GotoLabel : sig - val find_goto_label : CContext.t -> string -> Sil.location -> Cfg.Node.t + val find_goto_label : CContext.t -> string -> Location.t -> Cfg.Node.t val reset_all_labels : unit -> unit @@ -193,7 +202,8 @@ sig exception SelfClassException of string - val add_self_parameter_for_super_instance : CContext.t -> Procname.t -> Sil.location -> Clang_ast_t.obj_c_message_expr_info -> + val add_self_parameter_for_super_instance : + CContext.t -> Procname.t -> Location.t -> Clang_ast_t.obj_c_message_expr_info -> trans_result -> trans_result val is_var_self : Sil.pvar -> bool -> bool diff --git a/infer/src/harness/harness.ml b/infer/src/harness/harness.ml index f67baa22b..624d26cf2 100644 --- a/infer/src/harness/harness.ml +++ b/infer/src/harness/harness.ml @@ -55,7 +55,7 @@ let extract_callbacks procdesc cfg_file cfg tenv harness_name harness_lvar callb * implements. translation always places interfaces at the end of the supertypes list *) Mangled.get_mangled (list_hd (list_rev l)) else typ_str in - Mangled.from_string (pretty_typ_str ^ "[line " ^ Sil.loc_to_string loc ^ "]") in + Mangled.from_string (pretty_typ_str ^ "[line " ^ Location.to_string loc ^ "]") in let create_instrumentation_fields created_flds node instr = match instr with | Sil.Call([], Sil.Const (Sil.Cfun callee), args, loc, _) -> begin diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 951a919f9..7029ea11a 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -28,12 +28,12 @@ type env = { instrs : Sil.instr list; cache : Sil.exp TypMap.t; (* set of types currently being inhabited. consult to prevent infinite recursion *) cur_inhabiting : TypSet.t; - pc : Sil.location; + pc : Location.t; harness_name : Procname.t } (** add an instruction to the env, update tmp_vars, and bump the pc *) let env_add_instr instr tmp_vars env = - let incr_pc pc = { pc with Sil.line = pc.Sil.line + 1 } in + let incr_pc pc = { pc with Location.line = pc.Location.line + 1 } in { env with instrs = instr :: env.instrs; tmp_vars = tmp_vars @ env.tmp_vars; pc = incr_pc env.pc } (** call flags for an allocation or call to a constructor *) @@ -253,7 +253,7 @@ let write_harness_to_file harness_instrs harness_file = (** add the harness proc to the cg and make sure its callees can be looked up by sym execution *) let add_harness_to_cg harness_name harness_cfg harness_node loc cg tenv = Cg.add_node cg harness_name; - let create_dummy_procdesc procname = + let create_dummy_procdesc proc_name = (* convert a java type string to a type *) let rec lookup_typ typ_str = match typ_str with | "" | "void" -> Sil.Tvoid @@ -274,33 +274,34 @@ let add_harness_to_cg harness_name harness_cfg harness_node loc cg tenv = match Sil.get_typ (Mangled.from_string typ_str) None tenv with | Some typ -> typ | None -> failwith ("Failed to look up typ " ^ typ_str) in - let return_typ = lookup_typ (Procname.java_get_return_type procname) in - let params = - let param_strs = Procname.java_get_parameters procname in + let ret_type = lookup_typ (Procname.java_get_return_type proc_name) in + let formals = + let param_strs = Procname.java_get_parameters proc_name in list_fold_right (fun typ_str params -> ("", lookup_typ typ_str) :: params) param_strs [] in let open Cfg.Procdesc in let proc_attributes = { Sil.access = Sil.Default; - Sil.exceptions = []; - Sil.is_abstract = false; - Sil.is_bridge_method = false; - Sil.is_objc_instance_method = false; - Sil.is_synthetic_method = false; - Sil.language = Sil.Java; - Sil.func_attributes = []; - Sil.method_annotation = Sil.method_annotation_empty; - Sil.is_generated = false; + captured = []; + exceptions = []; + formals; + func_attributes = []; + is_abstract = false; + is_defined = false; + is_bridge_method = false; + is_generated = false; + is_objc_instance_method = false; + is_synthetic_method = false; + language = Config.Java; + loc; + locals = []; + method_annotation = Sil.method_annotation_empty; + proc_flags = proc_flags_empty (); + proc_name; + ret_type; } in create { cfg = harness_cfg; - name = procname; - is_defined = false; - ret_type = return_typ; - formals = params; - locals = []; - captured = []; - loc = loc; proc_attributes = proc_attributes; } in list_iter (fun p -> @@ -334,26 +335,27 @@ let setup_harness_cfg harness_name harness_cfg env proc_file_map tenv = let proc_attributes = { Sil.access = Sil.Default; - Sil.exceptions = []; - Sil.is_abstract = false; - Sil.is_bridge_method = false; - Sil.is_objc_instance_method = false; - Sil.is_synthetic_method = false; - Sil.language = Sil.Java; - Sil.func_attributes = []; - Sil.method_annotation = Sil.method_annotation_empty; - Sil.is_generated = false; + captured = []; + exceptions = []; + formals = []; + func_attributes = []; + is_abstract = false; + is_bridge_method = false; + is_defined = true; + is_generated = false; + is_objc_instance_method = false; + is_synthetic_method = false; + language = Config.Java; + loc = env.pc; + locals = []; + method_annotation = Sil.method_annotation_empty; + proc_flags = proc_flags_empty (); + proc_name = harness_name; + ret_type = Sil.Tvoid; } in create { cfg = harness_cfg; - name = harness_name; - is_defined = true; - ret_type = Sil.Tvoid; - formals = []; - locals = []; - captured = []; - loc = env.pc; - proc_attributes = proc_attributes; + proc_attributes; } in let harness_node = (* important to reverse the list or there will be scoping issues! *) @@ -383,7 +385,7 @@ let inhabit_trace trace cb_flds harness_name proc_file_map tenv = if list_length let harness_cfg = Cfg.Node.create_cfg () in let harness_file = create_dummy_harness_file harness_name harness_cfg tenv in let empty_env = - let pc = { Sil.line = 1; col = 1; file = harness_file; nLOC = 0; } in + let pc = { Location.line = 1; col = 1; file = harness_file; nLOC = 0; } in { instrs = []; tmp_vars = []; cache = TypMap.empty; diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index e7a967ce2..892610a00 100644 --- a/infer/src/java/jMain.ml +++ b/infer/src/java/jMain.ml @@ -45,7 +45,7 @@ let () = let init_global_state source_file = - Sil.curr_language := Sil.Java; + Config.curr_language := Config.Java; DB.current_source := source_file; DB.Results_dir.init (); Ident.reset_name_generator (); @@ -146,7 +146,7 @@ let do_all_files classpath sources classes = let program = JClasspath.load_program classpath classes sources in let tenv = load_tenv program in let linereader = Printer.LineReader.create () in - let never_null_matcher = Inferconfig.NeverReturnNull.load_matcher Sil.Java in + let never_null_matcher = Inferconfig.NeverReturnNull.load_matcher Config.Java in let proc_file_map = StringMap.fold (do_source_file never_null_matcher linereader classes program tenv) diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 250ea4b93..00f271746 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -23,9 +23,9 @@ type invoke_kind = exception Frontend_error of string -let constr_loc_map : Sil.location JBasics.ClassMap.t ref = ref JBasics.ClassMap.empty +let constr_loc_map : Location.t JBasics.ClassMap.t ref = ref JBasics.ClassMap.empty -let init_loc_map : Sil.location JBasics.ClassMap.t ref = ref JBasics.ClassMap.empty +let init_loc_map : Location.t JBasics.ClassMap.t ref = ref JBasics.ClassMap.empty (** Fix the line associated to a method definition. Since Sawja often reports a method off by a few lines, we search @@ -38,25 +38,25 @@ let fix_method_definition_line linereader proc_name loc = else Procname.java_get_method proc_name in let regex = Str.regexp (Str.quote method_name) in let method_is_defined_here linenum = - match Printer.LineReader.from_file_linenum_original linereader loc.Sil.file linenum with + match Printer.LineReader.from_file_linenum_original linereader loc.Location.file linenum with | None -> raise Not_found | Some line -> (try ignore (Str.search_forward regex line 0); true with Not_found -> false) in - let line = ref loc.Sil.line in + let line = ref loc.Location.line in try while not (method_is_defined_here !line) do line := !line -1; if !line < 0 then raise Not_found done; - { loc with Sil.line = !line } + { loc with Location.line = !line } with Not_found -> loc let get_location impl pc meth_kind cn = if meth_kind = JContext.Init then try JBasics.ClassMap.find cn !init_loc_map - with Not_found -> Sil.dummy_location + with Not_found -> Location.dummy else let line_number = let ln = @@ -65,7 +65,10 @@ let get_location impl pc meth_kind cn = match ln with | None -> 0 | Some n -> n in - { Sil.line = line_number; Sil.col = -1; Sil.file = !DB.current_source; Sil.nLOC = !Config.nLOC } + { Location.line = line_number; + col = -1; + file = !DB.current_source; + nLOC = !Config.nLOC } let get_undefined_method_call ovt = let get_undefined_method ovt = @@ -270,7 +273,7 @@ let create_local_procdesc program linereader cfg tenv node m = meth_kind = JContext.Init && not (JTransStaticField.has_static_final_fields node)) then - let procname = JTransType.get_method_procname cn ms (JTransType.get_method_kind m) in + let proc_name = JTransType.get_method_procname cn ms (JTransType.get_method_kind m) in let create_new_procdesc () = let trans_access = function | `Default -> Sil.Default @@ -287,31 +290,32 @@ let create_local_procdesc program linereader cfg tenv node m = let proc_attributes = { Sil.access = trans_access am.Javalib.am_access; - Sil.exceptions = list_map JBasics.cn_name am.Javalib.am_exceptions; - Sil.is_abstract = true; - Sil.is_bridge_method = am.Javalib.am_bridge; - Sil.is_objc_instance_method = false; - Sil.is_synthetic_method = am.Javalib.am_synthetic; - Sil.language = Sil.Java; - Sil.func_attributes = []; - Sil.method_annotation = method_annotation; - Sil.is_generated = false; + captured = []; + exceptions = list_map JBasics.cn_name am.Javalib.am_exceptions; + formals; + func_attributes = []; + is_abstract = true; + is_bridge_method = am.Javalib.am_bridge; + is_defined = true; + is_generated = false; + is_objc_instance_method = false; + is_synthetic_method = am.Javalib.am_synthetic; + language = Config.Java; + loc = Location.dummy; + locals = []; + method_annotation; + proc_flags = proc_flags_empty (); + proc_name; + ret_type = JTransType.return_type program tenv ms meth_kind; } in create { cfg = cfg; - name = procname; - is_defined = true; - ret_type = JTransType.return_type program tenv ms meth_kind; - formals = formals; - locals = []; - captured = []; - loc = Sil.dummy_location; - proc_attributes = proc_attributes + proc_attributes; } in let start_kind = Cfg.Node.Start_node procdesc in - let start_node = Cfg.Node.create cfg Sil.dummy_location start_kind [] procdesc [] in + let start_node = Cfg.Node.create cfg Location.dummy start_kind [] procdesc [] in let exit_kind = (Cfg.Node.Exit_node procdesc) in - let exit_node = Cfg.Node.create cfg Sil.dummy_location exit_kind [] procdesc [] in + let exit_node = Cfg.Node.create cfg Location.dummy exit_kind [] procdesc [] in Cfg.Node.set_succs_exn start_node [exit_node] [exit_node]; Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_exit_node procdesc exit_node @@ -323,25 +327,26 @@ let create_local_procdesc program linereader cfg tenv node m = let proc_attributes = { Sil.access = trans_access cm.Javalib.cm_access; - Sil.exceptions = list_map JBasics.cn_name cm.Javalib.cm_exceptions; - Sil.is_abstract = false; - Sil.is_bridge_method = cm.Javalib.cm_bridge; - Sil.is_objc_instance_method = false; - Sil.is_synthetic_method = cm.Javalib.cm_synthetic; - Sil.language = Sil.Java; - Sil.func_attributes = []; - Sil.method_annotation = method_annotation; - Sil.is_generated = false; + captured = []; + exceptions = list_map JBasics.cn_name cm.Javalib.cm_exceptions; + formals; + func_attributes = []; + is_abstract = false; + is_bridge_method = cm.Javalib.cm_bridge; + is_defined = false; + is_generated = false; + is_objc_instance_method = false; + is_synthetic_method = cm.Javalib.cm_synthetic; + language = Config.Java; + loc = Location.dummy; + locals = []; + method_annotation; + proc_flags = proc_flags_empty (); + proc_name; + ret_type = JTransType.return_type program tenv ms meth_kind; } in create { cfg = cfg; - name = procname; - is_defined = false; - ret_type = JTransType.return_type program tenv ms meth_kind; - formals = formals; - locals = []; - captured = []; - loc = Sil.dummy_location; proc_attributes = proc_attributes; } in () @@ -350,7 +355,7 @@ let create_local_procdesc program linereader cfg tenv node m = let locals, formals = locals_formals program tenv cn impl meth_kind in let loc_start = let loc = (get_location impl 0 JContext.Normal cn) in - fix_method_definition_line linereader procname loc in + fix_method_definition_line linereader proc_name loc in let loc_exit = (get_location impl (Array.length (JBir.code impl) - 1) JContext.Normal cn) in let method_annotation = JAnnotation.translate_method cm.Javalib.cm_annotations in update_constr_loc cn ms loc_start; @@ -360,25 +365,26 @@ let create_local_procdesc program linereader cfg tenv node m = let proc_attributes = { Sil.access = trans_access cm.Javalib.cm_access; - Sil.exceptions = list_map JBasics.cn_name cm.Javalib.cm_exceptions; - Sil.is_abstract = false; - Sil.is_bridge_method = cm.Javalib.cm_bridge; - Sil.is_objc_instance_method = false; - Sil.is_synthetic_method = cm.Javalib.cm_synthetic; - Sil.language = Sil.Java; - Sil.func_attributes = []; - Sil.method_annotation = method_annotation; - Sil.is_generated = false; + captured = []; + exceptions = list_map JBasics.cn_name cm.Javalib.cm_exceptions; + formals; + func_attributes = []; + is_abstract = false; + is_bridge_method = cm.Javalib.cm_bridge; + is_defined = true; + is_generated = false; + is_objc_instance_method = false; + is_synthetic_method = cm.Javalib.cm_synthetic; + language = Config.Java; + loc = loc_start; + locals; + method_annotation; + proc_flags = proc_flags_empty (); + proc_name; + ret_type = JTransType.return_type program tenv ms meth_kind; } in create { cfg = cfg; - name = procname; - is_defined = true; - ret_type = JTransType.return_type program tenv ms meth_kind; - formals = formals; - locals = locals; - captured = []; - loc = loc_start; proc_attributes = proc_attributes; } in let start_kind = Cfg.Node.Start_node procdesc in @@ -387,13 +393,13 @@ let create_local_procdesc program linereader cfg tenv node m = let exit_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc [] in let exn_kind = Cfg.Node.exn_sink_kind in let exn_node = Cfg.Node.create cfg loc_exit exn_kind [] procdesc [] in - JContext.add_exn_node procname exn_node; + JContext.add_exn_node proc_name exn_node; Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_exit_node procdesc exit_node; Cfg.Node.add_locals_ret_declaration start_node locals; with JBir.Subroutine -> - L.err "create_local_procdesc raised JBir.Subroutine on %a@." Procname.pp procname in - match lookup_procdesc cfg procname with + L.err "create_local_procdesc raised JBir.Subroutine on %a@." Procname.pp proc_name in + match lookup_procdesc cfg proc_name with | Unknown -> create_new_procdesc () | Created defined_status -> begin @@ -410,31 +416,32 @@ let create_external_procdesc program cfg tenv cn ms method_annotation kind = | None -> Sil.Tvoid | Some vt -> JTransType.value_type program tenv vt in let formals = formals_from_signature program tenv cn ms kind in - let procname = JTransType.get_method_procname cn ms kind in + let proc_name = JTransType.get_method_procname cn ms kind in ignore ( let open Cfg.Procdesc in let proc_attributes = { Sil.access = Sil.Default; - Sil.exceptions = []; - Sil.is_abstract = false; - Sil.is_bridge_method = false; - Sil.is_objc_instance_method = false; - Sil.is_synthetic_method = false; - Sil.language = Sil.Java; - Sil.func_attributes = []; - Sil.method_annotation = method_annotation; - Sil.is_generated = false; + captured = []; + exceptions = []; + formals; + func_attributes = []; + is_abstract = false; + is_bridge_method = false; + is_defined = false; + is_generated = false; + is_objc_instance_method = false; + is_synthetic_method = false; + language = Config.Java; + loc = Location.dummy; + locals = []; + method_annotation; + proc_flags = proc_flags_empty (); + proc_name; + ret_type = return_type; } in create { cfg = cfg; - name = procname; - is_defined = false; - ret_type = return_type; - formals = formals; - locals = []; - captured = []; - loc = Sil.dummy_location; proc_attributes = proc_attributes; }) @@ -848,7 +855,7 @@ let rec instruction context pc instr : translation = Cfg.Node.create cfg (get_location (JContext.get_impl context) pc meth_kind cn) node_kind sil_instrs (JContext.get_procdesc context) temps in let return_not_null () = - (match_never_null loc.Sil.file proc_name + (match_never_null loc.Location.file proc_name || list_exists (fun p -> Procname.equal p proc_name) JTransType.never_returning_null) in try match instr with diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index 0cca387a9..781c25519 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -50,7 +50,7 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table = let catch_nodes = get_body_nodes handler.JBir.e_handler in let loc = match catch_nodes with | n:: _ -> Cfg.Node.get_loc n - | [] -> Sil.dummy_location in + | [] -> Location.dummy in let exn_type = let class_name = match handler.JBir.e_catch_type with @@ -98,7 +98,7 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table = let nodes_first_handler = List.fold_left process_handler exit_nodes (List.rev handler_list) in let loc = match nodes_first_handler with | n:: _ -> Cfg.Node.get_loc n - | [] -> Sil.dummy_location in + | [] -> Location.dummy in let entry_node = create_entry_node loc in Cfg.Node.set_succs_exn entry_node nodes_first_handler exit_nodes; Hashtbl.add catch_block_table handler_list [entry_node] in diff --git a/infer/src/java/jTransStaticField.mli b/infer/src/java/jTransStaticField.mli index b1d36b667..2fa64c83e 100644 --- a/infer/src/java/jTransStaticField.mli +++ b/infer/src/java/jTransStaticField.mli @@ -17,7 +17,7 @@ val is_static_final_field : JContext.t -> JBasics.class_name -> JBasics.field_si val has_static_final_fields : JCode.jcode Javalib.interface_or_class -> bool val translate_instr_static_field : JContext.t -> Cfg.Procdesc.t -> JBasics.field_signature -> Sil.typ -> - Sil.location -> Ident.t list * Sil.instr list * Sil.exp + Location.t -> Ident.t list * Sil.instr list * Sil.exp val static_field_init : JCode.jcode Javalib.interface_or_class -> JBasics.class_name -> JBir.instr array -> JBir.instr array diff --git a/infer/src/llvm/lMain.ml b/infer/src/llvm/lMain.ml index d9eb0bab0..8a5e1e224 100644 --- a/infer/src/llvm/lMain.ml +++ b/infer/src/llvm/lMain.ml @@ -6,6 +6,7 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. *) + open Utils let arg_desc = @@ -31,7 +32,7 @@ let print_usage_exit () = exit(1) let init_global_state source_filename = - Sil.curr_language := Sil.C_CPP; + Config.curr_language := Config.C_CPP; begin match !Config.project_root with | None -> DB.current_source := DB.abs_source_file_from_path source_filename | Some project_root -> diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index 17258e8b0..a5862841d 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -14,8 +14,8 @@ exception ImproperTypeError of string exception MalformedMetadata of string exception Unimplemented of string -let source_only_location () : Sil.location = - let open Sil in { line = -1; col = -1; file = !DB.current_source; nLOC = !Config.nLOC } +let source_only_location () : Location.t = + let open Location in { line = -1; col = -1; file = !DB.current_source; nLOC = !Config.nLOC } let ident_of_variable (var : LAst.variable) : Ident.t = (* TODO: use unique stamps *) Ident.create_normal (Ident.string_to_name (LAst.string_of_variable var)) 0 @@ -41,15 +41,15 @@ let rec trans_typ : LAst.typ -> Sil.typ = function | Tmetadata -> raise (ImproperTypeError "Tried to generate Sil type from LLVM metadata type.") let location_of_annotation_option (metadata : LAst.metadata_map) - : LAst.annotation option -> Sil.location = function + : LAst.annotation option -> Location.t = function | None -> source_only_location () (* no source line/column numbers *) | Some (Annotation i) -> begin match MetadataMap.find i metadata with | Components (TypOperand (_, Const (Cint line_num)) :: _) -> - let open Sil in + let open Location in { line = line_num; col = -1; file = !DB.current_source; nLOC = !Config.nLOC } | Location loc -> - let open Sil in + let open Location in { line = loc.line; col = loc.col; file = !DB.current_source; nLOC = !Config.nLOC } | _ -> raise (MalformedMetadata ("Instruction annotation refers to metadata node " ^ "without line number as first component.")) @@ -91,7 +91,8 @@ let rec trans_annotated_instructions | _ -> raise (ImproperTypeError "Not expecting alloca instruction to a numbered variable.") end | Call (ret_var, func_var, typed_args) -> - let new_sil_instr = Sil.Call ([ident_of_variable ret_var], + let new_sil_instr = Sil.Call ( + [ident_of_variable ret_var], Sil.Const (Sil.Cfun (procname_of_function_variable func_var)), list_map (fun (tp, arg) -> (trans_operand arg, trans_typ tp)) typed_args, location, Sil.cf_default) in @@ -105,41 +106,45 @@ let callees_of_function_def : LAst.function_def -> Procname.t list = function | Call (_, func_var, _) -> Some (procname_of_function_variable func_var) | _ -> None end in - list_flatten_options (list_map + list_flatten_options ( + list_map (fun annotated_instr -> callee_of_instruction (fst annotated_instr)) annotated_instrs) (* Update CFG and call graph with new function definition *) let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map) - (func_def : LAst.function_def) : unit = match func_def with + (func_def : LAst.function_def) : unit = match func_def with FunctionDef (func_name, ret_tp_opt, params, annotated_instrs) -> - let procname = procname_of_function_variable func_name in + let proc_name = procname_of_function_variable func_name in + let ret_type = + match ret_tp_opt with + | None -> Sil.Tvoid + | Some ret_tp -> trans_typ ret_tp in let (proc_attrs : Sil.proc_attributes) = let open Sil in { access = Sil.Default; + captured = []; exceptions = []; + formals = list_map (fun (tp, name) -> (name, trans_typ tp)) params; + func_attributes = []; is_abstract = false; is_bridge_method = false; + is_defined = true; (** is defined and not just declared *) + is_generated = false; is_objc_instance_method = false; is_synthetic_method = false; - language = Sil.C_CPP; - func_attributes = []; + language = Config.C_CPP; + loc = source_only_location (); + locals = []; (* TODO *) method_annotation = Sil.method_annotation_empty; - is_generated = false + proc_flags = proc_flags_empty (); + proc_name; + ret_type; } in let (procdesc_builder : Cfg.Procdesc.proc_desc_builder) = let open Cfg.Procdesc in { cfg = cfg; - name = procname; - is_defined = true; (** is defined and not just declared *) proc_attributes = proc_attrs; - ret_type = (match ret_tp_opt with - | None -> Sil.Tvoid - | Some ret_tp -> trans_typ ret_tp); - formals = list_map (fun (tp, name) -> (name, trans_typ tp)) params; - locals = []; (* TODO *) - captured = []; - loc = source_only_location () } in let procdesc = Cfg.Procdesc.create procdesc_builder in let start_kind = Cfg.Node.Start_node procdesc in @@ -148,7 +153,7 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map) let exit_node = Cfg.Node.create cfg (source_only_location ()) exit_kind [] procdesc [] in let node_of_sil_instr cfg procdesc sil_instr = Cfg.Node.create cfg (Sil.instr_get_loc sil_instr) (Cfg.Node.Stmt_node "method_body") - [sil_instr] procdesc [] in + [sil_instr] procdesc [] in let rec link_nodes (start_node : Cfg.Node.t) : Cfg.Node.t list -> unit = function (* link all nodes in a chain for now *) | [] -> Cfg.Node.set_succs_exn start_node [exit_node] [exit_node] @@ -159,8 +164,8 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map) Cfg.Procdesc.set_exit_node procdesc exit_node; link_nodes start_node nodes; Cfg.Node.add_locals_ret_declaration start_node locals; - Cg.add_node cg procname; - list_iter (Cg.add_edge cg procname) (callees_of_function_def func_def) + Cg.add_node cg proc_name; + list_iter (Cg.add_edge cg proc_name) (callees_of_function_def func_def) let trans_program : LAst.program -> Cfg.cfg * Cg.t * Sil.tenv = function Program (func_defs, metadata) ->