diff --git a/infer/src/IR/cfg.ml b/infer/src/IR/cfg.ml index 387378df6..e09c0d6c1 100644 --- a/infer/src/IR/cfg.ml +++ b/infer/src/IR/cfg.ml @@ -34,10 +34,10 @@ module Node = struct mutable nd_temps : Ident.t list; (** dead program variables after executing the instructions *) - mutable nd_dead_pvars_after : Sil.pvar list; + mutable nd_dead_pvars_after : Pvar.t list; (** dead program variables before executing the instructions *) - mutable nd_dead_pvars_before : Sil.pvar list; + mutable nd_deads_before : Pvar.t list; (** exception nodes in the cfg *) mutable nd_exn : t list; @@ -160,7 +160,7 @@ module Node = struct nd_dist_exit = None; nd_temps = []; nd_dead_pvars_after = []; - nd_dead_pvars_before = []; + nd_deads_before = []; nd_instrs = []; nd_kind = Skip_node "dummy"; nd_loc = Location.dummy; @@ -186,7 +186,7 @@ module Node = struct nd_dist_exit = None; nd_temps = temps; nd_dead_pvars_after = []; - nd_dead_pvars_before = []; + nd_deads_before = []; nd_instrs = instrs; nd_kind = kind; nd_loc = loc; @@ -222,7 +222,9 @@ module Node = struct let do_node acc n = visited := NodeSet.add n !visited; if f n then NodeSet.singleton n - else NodeSet.union acc (slice_nodes (IList.filter (fun s -> not (NodeSet.mem s !visited)) n.nd_succs)) in + else + NodeSet.union acc + (slice_nodes (IList.filter (fun s -> not (NodeSet.mem s !visited)) n.nd_succs)) in IList.fold_left do_node NodeSet.empty nodes in NodeSet.elements (slice_nodes node.nd_succs) @@ -232,7 +234,9 @@ module Node = struct let do_node acc n = visited := NodeSet.add n !visited; if f n then NodeSet.singleton n - else NodeSet.union acc (slice_nodes (IList.filter (fun s -> not (NodeSet.mem s !visited)) n.nd_preds)) in + else + NodeSet.union acc + (slice_nodes (IList.filter (fun s -> not (NodeSet.mem s !visited)) n.nd_preds)) in IList.fold_left do_node NodeSet.empty nodes in NodeSet.elements (slice_nodes node.nd_preds) @@ -249,7 +253,8 @@ module Node = struct (** Get the predecessors of the node *) let get_preds node = node.nd_preds - (** Generates a list of nodes starting at a given node and recursively adding the results of the generator *) + (** Generates a list of nodes starting at a given node + and recursively adding the results of the generator *) let get_generated_slope start_node generator = let visited = ref NodeSet.empty in let rec nodes n = @@ -346,11 +351,11 @@ module Node = struct let set_dead_pvars node after dead = if after then node.nd_dead_pvars_after <- dead - else node.nd_dead_pvars_before <- dead + else node.nd_deads_before <- dead let get_dead_pvars node after = if after then node.nd_dead_pvars_after - else node.nd_dead_pvars_before + else node.nd_deads_before let get_distance_to_exit node = node.nd_dist_exit @@ -360,7 +365,8 @@ module Node = struct node.nd_instrs <- node.nd_instrs @ instrs; node.nd_temps <- node.nd_temps @ temps - (** Add the instructions and temporaties at the beginning of the list of instructions to execute *) + (** Add the instructions and temporaties at the beginning + of the list of instructions to execute *) let prepend_instrs_temps node instrs temps = node.nd_instrs <- instrs @ node.nd_instrs; node.nd_temps <- temps @ node.nd_temps @@ -370,7 +376,7 @@ module Node = struct node.nd_instrs <- instrs let proc_desc_get_ret_var pdesc = - Sil.get_ret_pvar pdesc.pd_attributes.ProcAttributes.proc_name + Pvar.get_ret_pvar pdesc.pd_attributes.ProcAttributes.proc_name (** Add declarations for local variables and return variable to the node *) let add_locals_ret_declaration node locals = @@ -381,7 +387,7 @@ module Node = struct let ret_type = pdesc.pd_attributes.ProcAttributes.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 + (Pvar.mk x proc_name, typ) in let ptl = ret_var :: IList.map construct_decl locals in let instr = Sil.Declare_locals (ptl, loc) in prepend_instrs_temps node [instr] [] @@ -645,7 +651,7 @@ module Node = struct and callee_start_node = proc_desc_get_start_node callee_proc_desc and callee_exit_node = proc_desc_get_exit_node callee_proc_desc in let convert_pvar pvar = - Sil.mk_pvar (Sil.pvar_get_name pvar) resolved_proc_name in + Pvar.mk (Pvar.get_name pvar) resolved_proc_name in let convert_exp = function | Sil.Lvar origin_pvar -> Sil.Lvar (convert_pvar origin_pvar) @@ -662,7 +668,7 @@ module Node = struct let convert_instr instrs = function | Sil.Letderef (id, (Sil.Lvar origin_pvar as origin_exp), origin_typ, loc) -> let (_, specialized_typ) = - let pvar_name = Sil.pvar_get_name origin_pvar in + let pvar_name = Pvar.get_name origin_pvar in try IList.find (fun (n, _) -> Mangled.equal n pvar_name) @@ -765,7 +771,7 @@ module Procdesc = struct let get_sliced_slope = Node.proc_desc_get_sliced_slope let get_proc_name = Node.proc_desc_get_proc_name let get_ret_type = Node.proc_desc_get_ret_type - let get_ret_var pdesc = Sil.mk_pvar Ident.name_return (get_proc_name pdesc) + let get_ret_var pdesc = Pvar.mk Ident.name_return (get_proc_name pdesc) let get_start_node = Node.proc_desc_get_start_node let is_defined = Node.proc_desc_is_defined let iter_nodes = Node.proc_desc_iter_nodes @@ -818,14 +824,15 @@ let set_procname_priority cfg pname = cfg.Node.priority_set <- Procname.Set.add pname cfg.Node.priority_set let get_name_of_local (curr_f : Procdesc.t) (x, _) = - Sil.mk_pvar x (Procdesc.get_proc_name curr_f) + Pvar.mk x (Procdesc.get_proc_name curr_f) (* returns a list of local static variables (ie local variables defined static) in a proposition *) let get_name_of_objc_static_locals (curr_f : Procdesc.t) p = let pname = Procname.to_string (Procdesc.get_proc_name curr_f) in let local_static e = match e with (* is a local static if it's a global and it has a static local name *) - | Sil.Lvar pvar when (Sil.pvar_is_global pvar) && (Sil.is_static_local_name pname pvar) -> [pvar] + | Sil.Lvar pvar + when (Pvar.is_global pvar) && (Sil.is_static_local_name pname pvar) -> [pvar] | _ -> [] in let hpred_local_static hpred = match hpred with @@ -885,18 +892,18 @@ let remove_abducted_retvars p = pi in Sil.HpredSet.elements reach_hpreds, reach_pi in (* separate the abducted pvars from the normal ones, deallocate the abducted ones*) - let abducted_pvars, normal_pvars = + let abducteds, normal_pvars = IList.fold_left (fun pvars hpred -> match hpred with | Sil.Hpointsto (Sil.Lvar pvar, _, _) -> - let abducted_pvars, normal_pvars = pvars in - if Sil.pvar_is_abducted pvar then pvar :: abducted_pvars, normal_pvars - else abducted_pvars, pvar :: normal_pvars + let abducteds, normal_pvars = pvars in + if Pvar.is_abducted pvar then pvar :: abducteds, normal_pvars + else abducteds, pvar :: normal_pvars | _ -> pvars) ([], []) (Prop.get_sigma p) in - let _, p' = Prop.deallocate_stack_vars p abducted_pvars in + let _, p' = Prop.deallocate_stack_vars p abducteds in let normal_pvar_set = IList.fold_left (fun normal_pvar_set pvar -> Sil.ExpSet.add (Sil.Lvar pvar) normal_pvar_set) @@ -919,14 +926,14 @@ let remove_locals (curr_f : Procdesc.t) p = let remove_formals (curr_f : Procdesc.t) p = let pname = Procdesc.get_proc_name curr_f in - let formal_vars = IList.map (fun (n, _) -> Sil.mk_pvar n pname) (Procdesc.get_formals curr_f) in + let formal_vars = IList.map (fun (n, _) -> Pvar.mk n pname) (Procdesc.get_formals curr_f) in Prop.deallocate_stack_vars p formal_vars (** remove the return variable from the prop *) let remove_ret (curr_f : Procdesc.t) (p: Prop.normal Prop.t) = let pname = Procdesc.get_proc_name curr_f in let name_of_ret = Procdesc.get_ret_var curr_f in - let _, p' = Prop.deallocate_stack_vars p [(Sil.pvar_to_callee pname name_of_ret)] in + let _, p' = Prop.deallocate_stack_vars p [(Pvar.to_callee pname name_of_ret)] in p' (** remove locals and return variable from the prop *) @@ -943,7 +950,7 @@ let remove_locals_formals (curr_f : Procdesc.t) p = (** remove seed vars from a prop *) let remove_seed_vars (prop: 'a Prop.t) : Prop.normal Prop.t = let hpred_not_seed = function - | Sil.Hpointsto(Sil.Lvar pv, _, _) -> not (Sil.pvar_is_seed pv) + | Sil.Hpointsto(Sil.Lvar pv, _, _) -> not (Pvar.is_seed pv) | _ -> true in let sigma = Prop.get_sigma prop in let sigma' = IList.filter hpred_not_seed sigma in @@ -964,7 +971,8 @@ let check_cfg_connectedness cfg = | Node.Stmt_node _ | Node.Prune_node _ | Node.Skip_node _ -> (IList.length succs = 0) || (IList.length preds = 0) | Node.Join_node -> - (* Join node has the exception that it may be without predecessors and pointing to an exit node *) + (* Join node has the exception that it may be without predecessors + and pointing to an exit node *) (* if the if brances end with a return *) (match succs with | [n'] when is_exit_node n' -> false @@ -985,8 +993,8 @@ let remove_seed_captured_vars_block captured_vars prop = let is_captured pname vn = Mangled.equal pname vn in let hpred_seed_captured = function | Sil.Hpointsto(Sil.Lvar pv, _, _) -> - let pname = Sil.pvar_get_name pv in - (Sil.pvar_is_seed pv) && (IList.mem is_captured pname captured_vars) + let pname = Pvar.get_name pv in + (Pvar.is_seed pv) && (IList.mem is_captured pname captured_vars) | _ -> false in let sigma = Prop.get_sigma prop in let sigma' = IList.filter (fun hpred -> not (hpred_seed_captured hpred)) sigma in @@ -1062,7 +1070,7 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call : Sil.instr option = let instr' = Sil.Letderef (ret_id, Sil.Lfield (e1, fn, ft), bt, loc_call) in found instr instr' | Sil.Letderef (_, Sil.Lfield (Sil.Lvar pvar, fn, ft), bt, _), [ret_id], [] - when Sil.pvar_is_global pvar -> (* getter for static fields *) + when Pvar.is_global pvar -> (* getter for static fields *) let instr' = Sil.Letderef (ret_id, Sil.Lfield (Sil.Lvar pvar, fn, ft), bt, loc_call) in found instr instr' | Sil.Set (Sil.Lfield (_, fn, ft), bt , _, _), @@ -1071,7 +1079,7 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call : Sil.instr option = let instr' = Sil.Set (Sil.Lfield (e1, fn, ft), bt , e2, loc_call) in found instr instr' | Sil.Set (Sil.Lfield (Sil.Lvar pvar, fn, ft), bt , _, _), _, [(e1, _)] - when Sil.pvar_is_global pvar -> (* setter for static fields *) + when Pvar.is_global pvar -> (* setter for static fields *) let instr' = Sil.Set (Sil.Lfield (Sil.Lvar pvar, fn, ft), bt , e1, loc_call) in found instr instr' | Sil.Call (ret_ids', Sil.Const (Sil.Cfun pn), etl', _, cf), _, _ diff --git a/infer/src/IR/cfg.mli b/infer/src/IR/cfg.mli index b6461ec94..57f71b0ab 100644 --- a/infer/src/IR/cfg.mli +++ b/infer/src/IR/cfg.mli @@ -78,7 +78,7 @@ module Procdesc : sig (** Return the return type of the procedure and type string *) val get_ret_type : t -> Sil.typ - val get_ret_var : t -> Sil.pvar + val get_ret_var : t -> Pvar.t val get_start_node : t -> node @@ -178,7 +178,7 @@ module Node : sig (** Get the (after/before) dead program variables. After/before indicated with the true/false flag. *) - val get_dead_pvars: t -> bool -> Sil.pvar list + val get_dead_pvars: t -> bool -> Pvar.t list (** Get the distance to the exit node, if it has been computed *) val get_distance_to_exit: t -> int option @@ -248,7 +248,7 @@ module Node : sig (** Set the (after/before) dead program variables. After/before indicated with the true/false flag. *) - val set_dead_pvars : t -> bool -> Sil.pvar list -> unit + val set_dead_pvars : t -> bool -> Pvar.t list -> unit (** Set the node kind *) val set_kind : t -> nodekind -> unit @@ -303,7 +303,7 @@ val remove_locals_ret : Procdesc.t -> Prop.normal Prop.t -> Prop.normal Prop.t (** Deallocate the stack variables in [pvars], and replace them by normal variables. Return the list of stack variables whose address was still present after deallocation. *) -val remove_locals_formals : Procdesc.t -> Prop.normal Prop.t -> Sil.pvar list * Prop.normal Prop.t +val remove_locals_formals : Procdesc.t -> Prop.normal Prop.t -> Pvar.t list * Prop.normal Prop.t (** remove seed vars from a prop *) val remove_seed_vars : 'a Prop.t -> Prop.normal Prop.t diff --git a/infer/src/IR/pvar.ml b/infer/src/IR/pvar.ml new file mode 100644 index 000000000..db73b24bb --- /dev/null +++ b/infer/src/IR/pvar.ml @@ -0,0 +1,213 @@ +(* + * 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. + *) + +(** The Smallfoot Intermediate Language *) + +module L = Logging +module F = Format + +(** Kind of global variables *) +type pvar_kind = + | Local_var of Procname.t (** local variable belonging to a function *) + | Callee_var of Procname.t (** local variable belonging to a callee *) + | Abducted_retvar of Procname.t * Location.t (** synthetic variable to represent return value *) + | Abducted_ref_param of Procname.t * t * Location.t + (** synthetic variable to represent param passed by reference *) + | Global_var (** gloval variable *) + | Seed_var (** variable used to store the initial value of formal parameters *) + +(** Names for program variables. *) +and t = + { pv_name: Mangled.t; + pv_kind: pvar_kind } + +let rec pvar_kind_compare k1 k2 = match k1, k2 with + | Local_var n1, Local_var n2 -> Procname.compare n1 n2 + | Local_var _, _ -> - 1 + | _, Local_var _ -> 1 + | Callee_var n1, Callee_var n2 -> Procname.compare n1 n2 + | Callee_var _, _ -> - 1 + | _, Callee_var _ -> 1 + | Abducted_retvar (p1, l1), Abducted_retvar (p2, l2) -> + let n = Procname.compare p1 p2 in + 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 = compare pv1 pv2 in + if n <> 0 then n else Location.compare l1 l2 + | Abducted_ref_param _, _ -> - 1 + | _, Abducted_ref_param _ -> 1 + | Global_var, Global_var -> 0 + | Global_var, _ -> - 1 + | _, Global_var -> 1 + | Seed_var, Seed_var -> 0 + +and compare pv1 pv2 = + let n = Mangled.compare pv1.pv_name pv2.pv_name in + if n <> 0 then n else pvar_kind_compare pv1.pv_kind pv2.pv_kind + +let equal pvar1 pvar2 = + compare pvar1 pvar2 = 0 + + +let rec _pp f pv = + let name = pv.pv_name in + match pv.pv_kind with + | Local_var n -> + if !Config.pp_simple then F.fprintf f "%a" Mangled.pp name + else F.fprintf f "%a$%a" Procname.pp n Mangled.pp name + | Callee_var n -> + if !Config.pp_simple then F.fprintf f "%a|callee" Mangled.pp name + 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 Location.pp l Mangled.pp name + | Abducted_ref_param (n, pv, l) -> + if !Config.pp_simple then F.fprintf f "%a|%a|abductedRefParam" _pp pv 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 + +(** Pretty print a program variable in latex. *) +let pp_latex f pv = + let name = pv.pv_name in + match pv.pv_kind with + | Local_var _ -> + Latex.pp_string Latex.Roman f (Mangled.to_string name) + | Callee_var _ -> + F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) + (Latex.pp_string Latex.Roman) "callee" + | Abducted_retvar _ -> + F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) + (Latex.pp_string Latex.Roman) "abductedRetvar" + | Abducted_ref_param _ -> + F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) + (Latex.pp_string Latex.Roman) "abductedRefParam" + | Global_var -> + Latex.pp_string Latex.Boldface f (Mangled.to_string name) + | Seed_var -> + F.fprintf f "%a^{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) + (Latex.pp_string Latex.Roman) "old" + +(** Pretty print a pvar which denotes a value, not an address *) +let pp_value pe f pv = + match pe.pe_kind with + | PP_TEXT -> _pp f pv + | PP_HTML -> _pp f pv + | PP_LATEX -> pp_latex f pv + +(** Pretty print a program variable. *) +let pp pe f pv = + let ampersand = match pe.pe_kind with + | PP_TEXT -> "&" + | PP_HTML -> "&" + | PP_LATEX -> "\\&" in + F.fprintf f "%s%a" ampersand (pp_value pe) pv + +(** Dump a program variable. *) +let d (pvar: t) = L.add_print_action (L.PTpvar, Obj.repr pvar) + +(** Pretty print a list of program variables. *) +let pp_list pe f pvl = + F.fprintf f "%a" (pp_seq (fun f e -> F.fprintf f "%a" (pp pe) e)) pvl + +(** Dump a list of program variables. *) +let d_list pvl = + IList.iter (fun pv -> d pv; L.d_str " ") pvl + +let get_name pv = pv.pv_name + +let to_string pv = Mangled.to_string pv.pv_name + +let get_simplified_name pv = + let s = Mangled.to_string pv.pv_name in + match string_split_character s '.' with + | Some s1, s2 -> + (match string_split_character s1 '.' with + | Some _, s4 -> s4 ^ "." ^ s2 + | _ -> s) + | _ -> s + +(** Check if the pvar is an abucted return var or param passed by ref *) +let is_abducted pv = + match pv.pv_kind with + | Abducted_retvar _ | Abducted_ref_param _ -> true + | _ -> false + +(** Turn a pvar into a seed pvar (which stored the initial value) *) +let to_seed pv = { pv with pv_kind = Seed_var } + +(** Check if the pvar is a local var *) +let is_local pv = + match pv.pv_kind with + | Local_var _ -> true + | _ -> false + +(** Check if the pvar is a callee var *) +let is_callee pv = + match pv.pv_kind with + | Callee_var _ -> true + | _ -> false + +(** Check if the pvar is a seed var *) +let is_seed pv = + match pv.pv_kind with + | Seed_var -> true + | _ -> false + +(** Check if the pvar is a global var *) +let is_global pv = + pv.pv_kind = Global_var + +(** Check if a pvar is the special "this" var *) +let is_this pvar = + Mangled.equal (get_name pvar) (Mangled.from_string "this") + +(** Check if the pvar is a return var *) +let is_return pv = + get_name pv = Ident.name_return + +(** Turn an ordinary program variable into a callee program variable *) +let to_callee pname pvar = match pvar.pv_kind with + | Local_var _ -> + { pvar with pv_kind = Callee_var pname } + | Global_var -> + pvar + | Callee_var _ | Abducted_retvar _ | Abducted_ref_param _ | Seed_var -> + L.d_str "Cannot convert pvar to callee: "; + d pvar; L.d_ln (); + assert false +(** [mk name proc_name] creates a program var with the given function name *) +let mk (name: Mangled.t) (proc_name: Procname.t) : t = + { pv_name = name; pv_kind = Local_var proc_name } + +let get_ret_pvar pname = + mk Ident.name_return pname + +(** [mk_callee name proc_name] creates a program var + for a callee function with the given function name *) +let mk_callee (name: Mangled.t) (proc_name: Procname.t) : t = + { pv_name = name; pv_kind = Callee_var proc_name } + +(** create a global variable with the given name *) +let mk_global (name: Mangled.t) : t = + { pv_name = name; pv_kind = Global_var } + +(** create an abducted return variable for a call to [proc_name] at [loc] *) +let mk_abducted_ret (proc_name : Procname.t) (loc : Location.t) : t = + 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_abducted_ref_param (proc_name : Procname.t) (pv : t) (loc : Location.t) : t = + 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/IR/pvar.mli b/infer/src/IR/pvar.mli new file mode 100644 index 000000000..cc656d1ea --- /dev/null +++ b/infer/src/IR/pvar.mli @@ -0,0 +1,97 @@ +(* + * 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. + *) + +(** Program variables. *) + +module F = Format + +(** 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]) + 3) global variables + 4) seed variables, used to store the initial value of formal parameters +*) +type t + +(** Compare two pvar's *) +val compare : t -> t -> int + +(** Dump a program variable. *) +val d : t -> unit + +(** Dump a list of program variables. *) +val d_list : t list -> unit + +(** Equality for pvar's *) +val equal : t -> t -> bool + +(** Get the name component of a program variable. *) +val get_name : t -> Mangled.t + +(** [get_ret_pvar proc_name] retuns the return pvar associated with the procedure name *) +val get_ret_pvar : Procname.t -> t + +(** Get a simplified version of the name component of a program variable. *) +val get_simplified_name : t -> string + +(** Check if the pvar is an abducted return var or param passed by ref *) +val is_abducted : t -> bool + +(** Check if the pvar is a callee var *) +val is_callee : t -> bool + +(** Check if the pvar is a global var *) +val is_global : t -> bool + +(** Check if the pvar is a local var *) +val is_local : t -> bool + +(** Check if the pvar is a seed var *) +val is_seed : t -> bool + +(** Check if the pvar is a return var *) +val is_return : t -> bool + +(** Check if a pvar is the special "this" var *) +val is_this : t -> bool + +(** [mk name proc_name suffix] creates a program var with the given function name and suffix *) +val mk : Mangled.t -> Procname.t -> t + +(** create an abducted variable for a parameter passed by reference *) +val mk_abducted_ref_param : Procname.t -> t -> Location.t -> t + +(** create an abducted return variable for a call to [proc_name] at [loc] *) +val mk_abducted_ret : Procname.t -> Location.t -> t + +(** [mk_callee name proc_name] creates a program var + for a callee function with the given function name *) +val mk_callee : Mangled.t -> Procname.t -> t + +(** create a global variable with the given name *) +val mk_global : Mangled.t -> t + +(** Pretty print a program variable. *) +val pp : printenv -> F.formatter -> t -> unit + +(** Pretty print a list of program variables. *) +val pp_list : printenv -> F.formatter -> t list -> unit + +(** Pretty print a pvar which denotes a value, not an address *) +val pp_value : printenv -> F.formatter -> t -> unit + +(** Turn an ordinary program variable into a callee program variable *) +val to_callee : Procname.t -> t -> t + +(** Turn a pvar into a seed pvar (which stores the initial value of a stack var) *) +val to_seed : t -> t + +(** Convert a pvar to string. *) +val to_string : t -> string diff --git a/infer/src/IR/sil.ml b/infer/src/IR/sil.ml index 488211d52..d775eb1d4 100644 --- a/infer/src/IR/sil.ml +++ b/infer/src/IR/sil.ml @@ -84,19 +84,6 @@ let get_sentinel_func_attribute_value attr_list = | FA_sentinel (sentinel, null_pos) :: _ -> Some (sentinel, null_pos) | [] -> None -(** 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.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 *) - -(** Names for program variables. *) -and pvar = { pv_name: Mangled.t; pv_kind: pvar_kind } - (** Unary operations *) type unop = | Neg (** Unary minus *) @@ -593,8 +580,8 @@ type dexp = | 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 + | Dpvar of Pvar.t + | Dpvaraddr of Pvar.t | Dunop of unop * dexp | Dunknown | Dretcall of dexp * dexp list * Location.t * call_flags @@ -659,7 +646,7 @@ and attribute_category = and closure = { name : Procname.t; - captured_vars : (exp * pvar * typ) list; + captured_vars : (exp * Pvar.t * typ) list; } (** Constants *) @@ -718,7 +705,7 @@ and exp = | Cast of typ * exp (** The address of a program variable *) - | Lvar of pvar + | Lvar of Pvar.t (** A field offset, the type is the surrounding struct type *) | Lfield of exp * Ident.fieldname * typ @@ -758,11 +745,11 @@ type instr = 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 + | Nullify of Pvar.t * 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 *) + | Declare_locals of (Pvar.t * 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 @@ -925,100 +912,17 @@ let zero_value_of_numerical_type typ = | Tptr _ -> Const (Cint Int.null) | _ -> assert false -let pvar_get_name pv = pv.pv_name - -let pvar_to_string pv = Mangled.to_string pv.pv_name - -let pvar_get_simplified_name pv = - let s = Mangled.to_string pv.pv_name in - match string_split_character s '.' with - | Some s1, s2 -> - (match string_split_character s1 '.' with - | Some _, s4 -> s4 ^ "." ^ s2 - | _ -> s) - | _ -> s - -(** Check if the pvar is an abucted return var or param passed by ref *) -let pvar_is_abducted pv = - match pv.pv_kind with - | Abducted_retvar _ | Abducted_ref_param _ -> true - | _ -> false - -(** Turn a pvar into a seed pvar (which stored the initial value) *) -let pvar_to_seed pv = { pv with pv_kind = Seed_var } - -(** Check if the pvar is a local var *) -let pvar_is_local pv = - match pv.pv_kind with - | Local_var _ -> true - | _ -> false - -(** Check if the pvar is a callee var *) -let pvar_is_callee pv = - match pv.pv_kind with - | Callee_var _ -> true - | _ -> false - -(** Check if the pvar is a seed var *) -let pvar_is_seed pv = - match pv.pv_kind with - | Seed_var -> true - | _ -> false - -(** Check if the pvar is a global var *) -let pvar_is_global pv = - pv.pv_kind = Global_var - -(** Check if a pvar is the special "this" var *) -let pvar_is_this pvar = - Mangled.equal (pvar_get_name pvar) (Mangled.from_string "this") - -(** Check if the pvar is a return var *) -let pvar_is_return pv = - pvar_get_name pv = Ident.name_return - (** Make a static local name in objc *) let mk_static_local_name pname vname = pname^"_"^vname (** Check if a pvar is a local static in objc *) let is_static_local_name pname pvar = (* local static name is of the form procname_varname *) - let var_name = Mangled.to_string(pvar_get_name pvar) in + let var_name = Mangled.to_string (Pvar.get_name pvar) in match Str.split_delim (Str.regexp_string pname) var_name with | [_; _] -> true | _ -> false -let rec pv_kind_compare k1 k2 = match k1, k2 with - | Local_var n1, Local_var n2 -> Procname.compare n1 n2 - | Local_var _, _ -> - 1 - | _, Local_var _ -> 1 - | Callee_var n1, Callee_var n2 -> Procname.compare n1 n2 - | Callee_var _, _ -> - 1 - | _, Callee_var _ -> 1 - | Abducted_retvar (p1, l1), Abducted_retvar (p2, l2) -> - let n = Procname.compare p1 p2 in - 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 Location.compare l1 l2 - | Abducted_ref_param _, _ -> - 1 - | _, Abducted_ref_param _ -> 1 - | Global_var, Global_var -> 0 - | Global_var, _ -> - 1 - | _, Global_var -> 1 - | Seed_var, Seed_var -> 0 - -and pvar_compare pv1 pv2 = - let n = Mangled.compare pv1.pv_name pv2.pv_name in - if n <> 0 then n else pv_kind_compare pv1.pv_kind pv2.pv_kind - -let pvar_equal pvar1 pvar2 = - pvar_compare pvar1 pvar2 = 0 - let fld_compare (fld1 : Ident.fieldname) fld2 = Ident.fieldname_compare fld1 fld2 let fld_equal fld1 fld2 = fld_compare fld1 fld2 = 0 @@ -1032,7 +936,7 @@ let exp_is_null_literal = function | _ -> false let exp_is_this = function - | Lvar pvar -> pvar_is_this pvar + | Lvar pvar -> Pvar.is_this pvar | _ -> false let ikind_is_char = function @@ -1370,7 +1274,7 @@ let rec const_compare (c1 : const) (c2 : const) : int = let n = exp_compare e1 e2 in if n <> 0 then n else - let n = pvar_compare pvar1 pvar2 in + let n = Pvar.compare pvar1 pvar2 in if n <> 0 then n else typ_compare typ1 typ2 in let n = Procname.compare n1 n2 in @@ -1506,7 +1410,7 @@ and exp_compare (e1 : exp) (e2 : exp) : int = | Cast _, _ -> - 1 | _, Cast _ -> 1 | Lvar i1, Lvar i2 -> - pvar_compare i1 i2 + Pvar.compare i1 i2 | Lvar _, _ -> - 1 | _, Lvar _ -> 1 | Lfield (e1, f1, t1), Lfield (e2, f2, t2) -> @@ -1818,71 +1722,6 @@ let str_binop pe binop = | _ -> text_binop binop -let rec _pp_pvar f pv = - let name = pv.pv_name in - match pv.pv_kind with - | Local_var n -> - if !Config.pp_simple then F.fprintf f "%a" Mangled.pp name - else F.fprintf f "%a$%a" Procname.pp n Mangled.pp name - | Callee_var n -> - if !Config.pp_simple then F.fprintf f "%a|callee" Mangled.pp name - 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 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 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 - -(** Pretty print a program variable in latex. *) -let pp_pvar_latex f pv = - let name = pv.pv_name in - match pv.pv_kind with - | Local_var _ -> - Latex.pp_string Latex.Roman f (Mangled.to_string name) - | Callee_var _ -> - F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) - (Latex.pp_string Latex.Roman) "callee" - | Abducted_retvar _ -> - F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) - (Latex.pp_string Latex.Roman) "abductedRetvar" - | Abducted_ref_param _ -> - F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) - (Latex.pp_string Latex.Roman) "abductedRefParam" - | Global_var -> - Latex.pp_string Latex.Boldface f (Mangled.to_string name) - | Seed_var -> - F.fprintf f "%a^{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) - (Latex.pp_string Latex.Roman) "old" - -(** Pretty print a pvar which denotes a value, not an address *) -let pp_pvar_value pe f pv = - match pe.pe_kind with - | PP_TEXT -> _pp_pvar f pv - | PP_HTML -> _pp_pvar f pv - | PP_LATEX -> pp_pvar_latex f pv - -(** Pretty print a program variable. *) -let pp_pvar pe f pv = - let ampersand = match pe.pe_kind with - | PP_TEXT -> "&" - | PP_HTML -> "&" - | PP_LATEX -> "\\&" in - F.fprintf f "%s%a" ampersand (pp_pvar_value pe) pv - -(** Dump a program variable. *) -let d_pvar (pvar: pvar) = L.add_print_action (L.PTpvar, Obj.repr pvar) - -(** Pretty print a list of program variables. *) -let pp_pvar_list pe f pvl = - F.fprintf f "%a" (pp_seq (fun f e -> F.fprintf f "%a" (pp_pvar pe) e)) pvl - -(** Dump a list of program variables. *) -let d_pvar_list pvl = - IList.iter (fun pv -> d_pvar pv; L.d_str " ") pvl - let ikind_to_string = function | IChar -> "char" | ISChar -> "signed char" @@ -1940,7 +1779,7 @@ let rec dexp_to_string = function F.fprintf fmt "%s" s | de -> F.fprintf fmt "%s" (dexp_to_string de) in let receiver, args' = match args with - | (Dpvar pv):: args' when isvirtual && pvar_is_this pv -> + | (Dpvar pv):: args' when isvirtual && Pvar.is_this pv -> (None, args') | a:: args' when isvirtual -> (Some a, args') @@ -1952,7 +1791,7 @@ let rec dexp_to_string = function | Some arg -> F.fprintf fmt "%a." pp_arg arg in F.fprintf fmt "%a%a(%a)" pp_receiver receiver pp_fun fun_dexp pp_args args' in pp_to_string pp () - | Darrow ((Dpvar pv), f) when pvar_is_this pv -> (* this->fieldname *) + | Darrow ((Dpvar pv), f) when Pvar.is_this pv -> (* this->fieldname *) Ident.fieldname_to_simplified_string f | Darrow (de, f) -> if Ident.fieldname_is_hidden f then dexp_to_string de @@ -1964,11 +1803,11 @@ let rec dexp_to_string = function if Ident.fieldname_is_hidden f then "&" ^ dexp_to_string de else if java() then dexp_to_string de ^ "." ^ Ident.fieldname_to_flat_string f else dexp_to_string de ^ "." ^ Ident.fieldname_to_string f - | Dpvar pv -> Mangled.to_string (pvar_get_name pv) + | Dpvar pv -> Mangled.to_string (Pvar.get_name pv) | Dpvaraddr pv -> let s = - if eradicate_java () then pvar_get_simplified_name pv - else Mangled.to_string (pvar_get_name pv) in + if eradicate_java () then Pvar.get_simplified_name pv + else Mangled.to_string (Pvar.get_name pv) in let ampersand = if eradicate_java () then "" else "&" in @@ -2033,8 +1872,8 @@ and attribute_to_string pe = function | Aobjc_null exp -> let info_s = match exp with - | Lvar var -> "FORMAL "^(pvar_to_string var) - | Lfield _ -> "FIELD "^(exp_to_string exp) + | Lvar var -> "FORMAL " ^ (Pvar.to_string var) + | Lfield _ -> "FIELD " ^ (exp_to_string exp) | _ -> "" in "OBJC_NULL["^ info_s ^"]" | Aretval pn -> "RET" ^ str_binop pe Lt ^ Procname.to_string pn ^ str_binop pe Gt @@ -2119,7 +1958,7 @@ and _pp_exp pe0 pp_t f e0 = (if not (exp_equal e0 e) then match e with - | Lvar pvar -> pp_pvar_value pe f pvar + | Lvar pvar -> Pvar.pp_value pe f pvar | _ -> assert false else let pp_exp = _pp_exp pe pp_t in @@ -2138,7 +1977,7 @@ and _pp_exp pe0 pp_t f e0 = | UnOp (op, e, _) -> F.fprintf f "%s%a" (str_unop op) pp_exp e | BinOp (op, Const c, e2) when !Config.smt_output -> print_binop_stm_output (Const c) op e2 | BinOp (op, e1, e2) -> F.fprintf f "(%a %s %a)" pp_exp e1 (str_binop pe op) pp_exp e2 - | Lvar pv -> pp_pvar pe f pv + | Lvar pv -> Pvar.pp pe f pv | Lfield (e, fld, _) -> F.fprintf f "%a.%a" pp_exp e Ident.pp_fieldname fld | Lindex (e1, e2) -> F.fprintf f "%a[%a]" pp_exp e1 pp_exp e2 | Sizeof (t, s) -> F.fprintf f "sizeof(%a%a)" pp_t t Subtype.pp s @@ -2275,7 +2114,7 @@ let pp_instr pe0 f instr = pp_call_flags cf Location.pp loc | Nullify (pvar, loc, deallocate) -> - F.fprintf f "NULLIFY(%a,%b); %a" (pp_pvar pe) pvar deallocate Location.pp loc + F.fprintf f "NULLIFY(%a,%b); %a" (Pvar.pp pe) pvar deallocate Location.pp loc | Abstract loc -> F.fprintf f "APPLY_ABSTRACTION; %a" Location.pp loc | Remove_temps (temps, loc) -> @@ -2287,8 +2126,8 @@ let pp_instr pe0 f instr = | Pop -> "Pop" in F.fprintf f "STACKOP.%s; %a" s Location.pp loc | Declare_locals (ptl, loc) -> - let pp_pvar_typ fmt (pvar, _) = F.fprintf fmt "%a" (pp_pvar pe) pvar in - F.fprintf f "DECLARE_LOCALS(%a); %a" (pp_comma_seq pp_pvar_typ) ptl Location.pp loc + let pp_typ fmt (pvar, _) = F.fprintf fmt "%a" (Pvar.pp pe) pvar in + F.fprintf f "DECLARE_LOCALS(%a); %a" (pp_comma_seq pp_typ) ptl Location.pp loc | Goto_node (e, loc) -> F.fprintf f "Goto_node %a %a" (pp_exp pe) e Location.pp loc ); @@ -2299,14 +2138,18 @@ let has_block_prefix s = | _ :: _ :: _ -> true | _ -> false -(** Check if a pvar is a local pointing to a block in objc *) -let is_block_pvar pvar = - has_block_prefix (Mangled.to_string (pvar_get_name pvar)) - (** Check if type is a type for a block in objc *) let is_block_type typ = has_block_prefix (typ_to_string typ) +(** Check if a pvar is a local pointing to a block in objc *) +let is_block_pvar pvar = + has_block_prefix (Mangled.to_string (Pvar.get_name pvar)) + +(* A block pvar used to explain retain cycles *) +let block_pvar = + Pvar.mk (Mangled.from_string "block") (Procname.from_string_c_fun "") + (** Iterate over all the subtypes in the type (including the type itself) *) let rec typ_iter_types (f : typ -> unit) typ = f typ; @@ -2738,7 +2581,7 @@ and pp_hpred_env pe0 envo f hpred = begin match hpred with | Hpointsto (e, se, te) -> let pe' = match (e, se) with - | Lvar pvar, Eexp (Var _, _) when not (pvar_is_global pvar) -> + | Lvar pvar, Eexp (Var _, _) when not (Pvar.is_global pvar) -> { pe with pe_obj_sub = None } (* dont use obj sub on the var defining it *) | _ -> pe in (match pe'.pe_kind with @@ -3612,7 +3455,7 @@ let instr_compare instr1 instr2 = match instr1, instr2 with | Call _, _ -> -1 | _, Call _ -> 1 | Nullify (pvar1, loc1, deallocate1), Nullify (pvar2, loc2, deallocate2) -> - let n = pvar_compare pvar1 pvar2 in + let n = Pvar.compare pvar1 pvar2 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 @@ -3633,7 +3476,7 @@ let instr_compare instr1 instr2 = match instr1, instr2 with | _, Stackop _ -> 1 | Declare_locals (ptl1, loc1), Declare_locals (ptl2, loc2) -> let pt_compare (pv1, t1) (pv2, t2) = - let n = pvar_compare pv1 pv2 in + let n = Pvar.compare pv1 pv2 in if n <> 0 then n else typ_compare t1 t2 in let n = IList.compare pt_compare ptl1 ptl2 in @@ -3881,42 +3724,6 @@ let hpred_compact sh hpred = (** {2 Functions for constructing or destructing entities in this module} *) -(** [mk_pvar name proc_name] creates a program var with the given function name *) -let mk_pvar (name: Mangled.t) (proc_name: Procname.t) : pvar = - { pv_name = name; pv_kind = Local_var proc_name } - - -let get_ret_pvar pname = - mk_pvar Ident.name_return pname - -(** [mk_pvar_callee name proc_name] creates a program var - for a callee function with the given function name *) -let mk_pvar_callee (name: Mangled.t) (proc_name: Procname.t) : pvar = - { pv_name = name; pv_kind = Callee_var proc_name } - -(** create a global variable with the given name *) -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.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.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) } - -(** Turn an ordinary program variable into a callee program variable *) -let pvar_to_callee pname pvar = match pvar.pv_kind with - | Local_var _ -> - { pvar with pv_kind = Callee_var pname } - | Global_var -> pvar - | Callee_var _ | Abducted_retvar _ | Abducted_ref_param _ | Seed_var -> - L.d_str "Cannot convert pvar to callee: "; - d_pvar pvar; L.d_ln (); - assert false - (** Compute the offset list of an expression *) let exp_get_offsets exp = let rec f offlist_past e = match e with @@ -3999,51 +3806,4 @@ let hpara_dll_instantiate (para: hpara_dll) cell blink flink elist = (ids_evars, IList.map (hpred_sub subst) para.body_dll) let custom_error = - mk_pvar_global (Mangled.from_string "INFER_CUSTOM_ERROR") - -(* A block pvar used to explain retain cycles *) -let block_pvar = - mk_pvar (Mangled.from_string "block") (Procname.from_string_c_fun "") - -(* -(** Check if the item annotation is empty. *) -let item_annotation_is_empty avl = - avl = [] - -let atom_list_compare l1 l2 = - IList.compare atom_compare l1 l2 - -let fld_strexp_equal fld_sexp1 fld_sexp2 = - (fld_strexp_compare fld_sexp1 fld_sexp2 = 0) - -let exp_strexp_equal ese1 ese2 = - (exp_strexp_compare ese1 ese2 = 0) - -let pp_pair pe f ((fld: Ident.fieldname), (t: typ)) = - F.fprintf f "%a %a" (pp_typ pe) t Ident.pp_fieldname fld - -let sub_check_sortedness sub = - let sub' = IList.sort ident_exp_compare sub in - sub_equal sub sub' - -let sub_check_inv sub = - (sub_check_sortedness sub) && not (sub_check_duplicated_ids sub) - -let range_sub subst range = - let lower, upper = range in - let lower' = exp_sub subst lower in - let upper' = exp_sub subst upper in - (lower', upper') - -let exp_list_replace_exp epairs l = - IList.map (exp_replace_exp epairs) l - -(** Return the list of expressions that could be understood as outgoing arrows from the strexp *) -let rec strexp_get_target_exps = function - | Eexp (e, inst) -> [e] - | Estruct (fsel, inst) -> - IList.flatten (IList.map (fun (_, se) -> strexp_get_target_exps se) fsel) - | Earray (_, esel, _) -> - (* We ignore size and indices since they are not quite outgoing arrows. *) - IList.flatten (IList.map (fun (_, se) -> strexp_get_target_exps se) esel) -*) + Pvar.mk_global (Mangled.from_string "INFER_CUSTOM_ERROR") diff --git a/infer/src/IR/sil.mli b/infer/src/IR/sil.mli index d8740bf2f..2e75bf291 100644 --- a/infer/src/IR/sil.mli +++ b/infer/src/IR/sil.mli @@ -32,14 +32,6 @@ type func_attribute = (** Visibility modifiers. *) type access = Default | Public | Private | Protected -(** 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]) - 3) global variables - 4) seed variables, used to store the initial value of formal parameters -*) -type pvar - (** Unary operations *) type unop = | Neg (** Unary minus *) @@ -225,8 +217,8 @@ type dexp = | 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 + | Dpvar of Pvar.t + | Dpvaraddr of Pvar.t | Dunop of unop * dexp | Dunknown | Dretcall of dexp * dexp list * Location.t * call_flags @@ -292,7 +284,7 @@ and attribute_category = and closure = { name : Procname.t; - captured_vars : (exp * pvar * typ) list; + captured_vars : (exp * Pvar.t * typ) list; } (** Constants *) @@ -350,7 +342,7 @@ and exp = | Cast of typ * exp (** The address of a program variable *) - | Lvar of pvar + | Lvar of Pvar.t (** A field offset, the type is the surrounding struct type *) | Lfield of exp * Ident.fieldname * typ @@ -408,11 +400,11 @@ type instr = 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 + | Nullify of Pvar.t * 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 *) + | Declare_locals of (Pvar.t * 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 @@ -583,55 +575,21 @@ val typ_strip_ptr : typ -> typ val zero_value_of_numerical_type : typ -> exp -val pvar_get_name : pvar -> Mangled.t - -val pvar_to_string : pvar -> string - -(** Turn a pvar into a seed pvar (which stores the initial value of a stack var) *) -val pvar_to_seed : pvar -> pvar - -(** Check if the pvar is a callee var *) -val pvar_is_callee : pvar -> bool - -(** Check if the pvar is an abducted return var or param passed by ref *) -val pvar_is_abducted : pvar -> bool - -(** Check if the pvar is a local var *) -val pvar_is_local : pvar -> bool - -(** Check if the pvar is a seed var *) -val pvar_is_seed : pvar -> bool - -(** Check if the pvar is a global var *) -val pvar_is_global : pvar -> bool - -(** Check if a pvar is the special "this" var *) -val pvar_is_this : pvar -> bool - -(** Check if the pvar is a return var *) -val pvar_is_return : pvar -> bool - (** Make a static local name in objc *) val mk_static_local_name : string -> string -> string (** Check if a pvar is a local static in objc *) -val is_static_local_name : string -> pvar -> bool +val is_static_local_name : string -> Pvar.t -> bool (* A block pvar used to explain retain cycles *) -val block_pvar : pvar +val block_pvar : Pvar.t (** Check if a pvar is a local pointing to a block in objc *) -val is_block_pvar : pvar -> bool +val is_block_pvar : Pvar.t -> bool (** Check if type is a type for a block in objc *) val is_block_type : typ -> bool -(** Compare two pvar's *) -val pvar_compare : pvar -> pvar -> int - -(** Equality for pvar's *) -val pvar_equal : pvar -> pvar -> bool - (** Comparision for fieldnames. *) val fld_compare : Ident.fieldname -> Ident.fieldname -> int @@ -843,21 +801,6 @@ val d_typ_full : typ -> unit (** Dump a list of types. *) val d_typ_list : typ list -> unit -(** Pretty print a program variable. *) -val pp_pvar : printenv -> F.formatter -> pvar -> unit - -(** Pretty print a pvar which denotes a value, not an address *) -val pp_pvar_value : printenv -> F.formatter -> pvar -> unit - -(** Dump a program variable. *) -val d_pvar : pvar -> unit - -(** Pretty print a list of program variables. *) -val pp_pvar_list : printenv -> F.formatter -> pvar list -> unit - -(** Dump a list of program variables. *) -val d_pvar_list : pvar list -> unit - (** convert the attribute to a string *) val attribute_to_string : printenv -> attribute -> string @@ -1086,15 +1029,15 @@ val exp_lt : exp -> exp -> exp (** {2 Functions for computing program variables} *) -val exp_fpv : exp -> pvar list +val exp_fpv : exp -> Pvar.t list -val strexp_fpv : strexp -> pvar list +val strexp_fpv : strexp -> Pvar.t list -val atom_fpv : atom -> pvar list +val atom_fpv : atom -> Pvar.t list -val hpred_fpv : hpred -> pvar list +val hpred_fpv : hpred -> Pvar.t list -val hpara_fpv : hpara -> pvar list +val hpara_fpv : hpara -> Pvar.t list (** {2 Functions for computing free non-program variables} *) @@ -1277,7 +1220,7 @@ val sub_fav_add : fav -> subst -> unit val sub_av_add : fav -> subst -> unit (** Compute free pvars in a sub *) -val sub_fpv : subst -> pvar list +val sub_fpv : subst -> Pvar.t list (** substitution functions *) (** WARNING: these functions do not ensure that the results are normalized. *) @@ -1304,28 +1247,6 @@ val hpred_replace_exp : (exp * exp) list -> hpred -> hpred (** {2 Functions for constructing or destructing entities in this module} *) - -(** [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 - -(** [get_ret_pvar proc_name] retuns the return pvar associated with the procedure name *) -val get_ret_pvar : Procname.t -> pvar - -(** [mk_pvar_callee name proc_name] creates a program var - for a callee function with the given function name *) -val mk_pvar_callee : Mangled.t -> Procname.t -> pvar - -(** create a global variable with the given name *) -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.t -> 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 - (** Compute the offset list of an expression *) val exp_get_offsets : exp -> offset list @@ -1354,9 +1275,4 @@ val exp_iter_types : (typ -> unit) -> exp -> unit (** Iterate over all the types (and subtypes) in the instruction *) val instr_iter_types : (typ -> unit) -> instr -> unit -val custom_error : pvar - -(* -(** Equality for consts. *) -val const_equal : const -> const -> bool -*) +val custom_error : Pvar.t diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 6ce22c907..bffa1307b 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -950,7 +950,7 @@ let get_var_retain_cycle _prop = | Sil.Hpointsto (e, _, Sil.Sizeof(typ, _)), Sil.Eexp (e', _) when Sil.exp_equal e e' && Sil.is_block_type typ -> true | _, _ -> false in - let find_pvar v = + let find v = try let hp = IList.find (is_pvar v) sigma in Some (Sil.hpred_get_lhs hp) @@ -960,8 +960,8 @@ let get_var_retain_cycle _prop = Some (Sil.Lvar Sil.block_pvar) else None in let sexp e = Sil.Eexp (e, Sil.Inone) in - let find_pvar_or_block ((e, t), f, e') = - match find_pvar e with + let find_or_block ((e, t), f, e') = + match find e with | Some pvar -> [((sexp pvar, t), f, e')] | _ -> (match find_block e with | Some blk -> [((sexp blk, t), f, e')] @@ -976,7 +976,7 @@ let get_var_retain_cycle _prop = | hp:: sigma' -> let cycle = get_cycle hp _prop in L.d_strln "Filtering pvar in cycle "; - let cycle' = IList.flatten (IList.map find_pvar_or_block cycle) in + let cycle' = IList.flatten (IList.map find_or_block cycle) in if cycle' = [] then do_sigma sigma' else cycle' in do_sigma sigma @@ -1025,7 +1025,7 @@ let check_observer_is_unsubscribed_deallocation prop e = | Some Sil.Aobserver -> (match pvar_opt with | Some pvar -> - L.d_strln (" ERROR: Object " ^ (Sil.pvar_to_string pvar) ^ + L.d_strln (" ERROR: Object " ^ (Pvar.to_string pvar) ^ " is being deallocated while still registered in a notification center"); let desc = Localise.desc_registered_observer_being_deallocated pvar loc in raise (Exceptions.Registered_observer_being_deallocated (desc, __POS__)) @@ -1219,8 +1219,8 @@ let get_local_stack cur_sigma init_sigma = let get_stack_var = function | Sil.Hpointsto (Sil.Lvar pvar, _, _) -> pvar | Sil.Hpointsto _ | Sil.Hlseg _ | Sil.Hdllseg _ -> assert false in - let filter_local_stack old_pvars = function - | Sil.Hpointsto (Sil.Lvar pvar, _, _) -> not (IList.exists (Sil.pvar_equal pvar) old_pvars) + let filter_local_stack olds = function + | Sil.Hpointsto (Sil.Lvar pvar, _, _) -> not (IList.exists (Pvar.equal pvar) olds) | Sil.Hpointsto _ | Sil.Hlseg _ | Sil.Hdllseg _ -> false in let init_stack = IList.filter filter_stack init_sigma in let init_stack_pvars = IList.map get_stack_var init_stack in @@ -1229,7 +1229,7 @@ let get_local_stack cur_sigma init_sigma = (cur_local_stack, cur_local_stack_pvars) (** Extract the footprint, add a local stack and return it as a prop *) -let extract_footprint_for_abs (p : 'a Prop.t) : Prop.exposed Prop.t * Sil.pvar list = +let extract_footprint_for_abs (p : 'a Prop.t) : Prop.exposed Prop.t * Pvar.t list = let sigma = Prop.get_sigma p in let foot_pi = Prop.get_pi_footprint p in let foot_sigma = Prop.get_sigma_footprint p in @@ -1240,7 +1240,7 @@ let extract_footprint_for_abs (p : 'a Prop.t) : Prop.exposed Prop.t * Sil.pvar l let remove_local_stack sigma pvars = let filter_non_stack = function - | Sil.Hpointsto (Sil.Lvar pvar, _, _) -> not (IList.exists (Sil.pvar_equal pvar) pvars) + | Sil.Hpointsto (Sil.Lvar pvar, _, _) -> not (IList.exists (Pvar.equal pvar) pvars) | Sil.Hpointsto _ | Sil.Hlseg _ | Sil.Hdllseg _ -> true in IList.filter filter_non_stack sigma diff --git a/infer/src/backend/autounit.ml b/infer/src/backend/autounit.ml index 867ed18a0..df6d6ec42 100644 --- a/infer/src/backend/autounit.ml +++ b/infer/src/backend/autounit.ml @@ -398,8 +398,8 @@ let pp_typ_c pe typ = Sil.pp_type_decl pe pp_nil pp_exp_c typ (** Convert a pvar to a string by just extracting the name *) -let pvar_to_string pvar = - Mangled.to_string (Sil.pvar_get_name pvar) +let to_string pvar = + Mangled.to_string (Pvar.get_name pvar) (** pretty print an expression list in C *) let pp_exp_list_c pe f expl = @@ -449,7 +449,7 @@ let gen_sigma code proc_name spec_num env sigma = let gen_hpred = function | Sil.Hpointsto (Sil.Lvar pvar, se, _) -> - let base = pvar_to_string pvar in + let base = to_string pvar in do_strexp post_code base false se | Sil.Hpointsto (Sil.Var id, se, te) -> let pp1 f () = diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml index 4382b1d2b..85e5791ba 100644 --- a/infer/src/backend/buckets.ml +++ b/infer/src/backend/buckets.ml @@ -54,13 +54,13 @@ let check_access access_opt de_opt = let formals = Cfg.Procdesc.get_formals (Cfg.Node.get_proc_desc node) in let formal_names = IList.map fst formals in let is_formal pvar = - let name = Sil.pvar_get_name pvar in + let name = Pvar.get_name pvar in IList.exists (Mangled.equal name) formal_names in let formal_ids = ref [] in let process_formal_letref = function | Sil.Letderef (id, Sil.Lvar pvar, _, _) -> let is_java_this = - !Config.curr_language = Config.Java && Sil.pvar_is_this pvar in + !Config.curr_language = Config.Java && Pvar.is_this pvar in if not is_java_this && is_formal pvar then formal_ids := id :: !formal_ids | _ -> () in IList.iter process_formal_letref node_instrs; diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index f9df2a00d..abf16f6d8 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -954,7 +954,7 @@ let rec exp_partial_join (e1: Sil.exp) (e2: Sil.exp) : Sil.exp = let e2'' = exp_partial_join e1' e2' in Sil.BinOp(binop1, e1'', e2'') | Sil.Lvar(pvar1), Sil.Lvar(pvar2) -> - if not (Sil.pvar_equal pvar1 pvar2) then (L.d_strln "failure reason 25"; raise IList.Fail) + if not (Pvar.equal pvar1 pvar2) then (L.d_strln "failure reason 25"; raise IList.Fail) else e1 | Sil.Lfield(e1, f1, t1), Sil.Lfield(e2, f2, _) -> if not (Sil.fld_equal f1 f2) then (L.d_strln "failure reason 26"; raise IList.Fail) @@ -1029,7 +1029,7 @@ let rec exp_partial_meet (e1: Sil.exp) (e2: Sil.exp) : Sil.exp = Rename.extend e1 e2 (Rename.ExtDefault(e1)) else (L.d_strln "failure reason 34"; raise IList.Fail) | Sil.Lvar(pvar1), Sil.Lvar(pvar2) -> - if not (Sil.pvar_equal pvar1 pvar2) then (L.d_strln "failure reason 35"; raise IList.Fail) + if not (Pvar.equal pvar1 pvar2) then (L.d_strln "failure reason 35"; raise IList.Fail) else e1 | Sil.Lfield(e1, f1, t1), Sil.Lfield(e2, f2, _) -> if not (Sil.fld_equal f1 f2) then (L.d_strln "failure reason 36"; raise IList.Fail) diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 171e0a99b..9968853ad 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -125,7 +125,7 @@ let strip_special_chars s = let rec strexp_to_string pe coo f se = match se with - | Sil.Eexp (Sil.Lvar pvar, _) -> F.fprintf f "%a" (Sil.pp_pvar pe) pvar + | Sil.Eexp (Sil.Lvar pvar, _) -> F.fprintf f "%a" (Pvar.pp pe) pvar | Sil.Eexp (Sil.Var id, _) -> if !print_full_prop then F.fprintf f "%a" (Ident.pp pe) id @@ -1306,11 +1306,11 @@ let xml_pure_info prop = (** Return a string describing the kind of a pointsto address *) let pointsto_addr_kind = function | Sil.Lvar pv -> - if Sil.pvar_is_global pv + if Pvar.is_global pv then "global" - else if Sil.pvar_is_local pv && Mangled.equal (Sil.pvar_get_name pv) Ident.name_return + else if Pvar.is_local pv && Mangled.equal (Pvar.get_name pv) Ident.name_return then "return" - else if Sil.pvar_is_local pv + else if Pvar.is_local pv then "parameter" else "other" | _ -> "other" diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 5e631cd90..f4256387b 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -28,7 +28,7 @@ let explain_context_leak pname context_typ fieldname error_path = (** Explain a deallocate stack variable error *) let explain_deallocate_stack_var pvar ra = - let pvar_str = Sil.pvar_to_string pvar in + let pvar_str = Pvar.to_string pvar in Localise.desc_deallocate_stack_variable pvar_str ra.Sil.ra_pname ra.Sil.ra_loc (** Explain a deallocate constant string error *) @@ -58,13 +58,14 @@ let find_nullify_after_instr node instr pvar : bool = let node_instrs = Cfg.Node.get_instrs node in let found_instr = ref false in let find_nullify = function - | Sil.Nullify (pv, _, _) when !found_instr -> Sil.pvar_equal pv pvar + | Sil.Nullify (pv, _, _) when !found_instr -> Pvar.equal pv pvar | _instr -> if instr = _instr then found_instr := true; false in IList.exists find_nullify node_instrs -(** Find the other prune node of a conditional (e.g. the false branch given the true branch of a conditional) *) +(** Find the other prune node of a conditional + (e.g. the false branch given the true branch of a conditional) *) let find_other_prune_node node = match Cfg.Node.get_preds node with | [n_pre] -> @@ -77,11 +78,13 @@ let find_other_prune_node node = (** Return true if [id] is assigned to a program variable which is then nullified *) let id_is_assigned_then_dead node id = match find_variable_assigment node id with - | Some (Sil.Set (Sil.Lvar pvar, _, _, _) as instr) when Sil.pvar_is_local pvar || Sil.pvar_is_callee pvar -> + | Some (Sil.Set (Sil.Lvar pvar, _, _, _) as instr) + when Pvar.is_local pvar || Pvar.is_callee pvar -> let is_prune = match Cfg.Node.get_kind node with | Cfg.Node.Prune_node _ -> true | _ -> false in - let prune_check = function (* if prune node, check that it's also nullified in the other branch *) + let prune_check = function + (* if prune node, check that it's also nullified in the other branch *) | Some node' -> (match Cfg.Node.get_instrs node' with | instr':: _ -> find_nullify_after_instr node' instr' pvar @@ -104,8 +107,14 @@ let find_normal_variable_funcall true | _ -> false in ignore (IList.exists find_declaration node_instrs); - if !verbose && !res == None then (L.d_str ("find_normal_variable_funcall could not find " ^ - Ident.to_string id ^ " in node " ^ string_of_int (Cfg.Node.get_id node)); L.d_ln ()); + if !verbose && !res == None + then + (L.d_str + ("find_normal_variable_funcall could not find " ^ + Ident.to_string id ^ + " in node " ^ + string_of_int (Cfg.Node.get_id node)); + L.d_ln ()); !res (** Find a program variable assignment in the current node or predecessors. *) @@ -118,7 +127,8 @@ let find_program_variable_assignment node pvar : (Cfg.Node.t * Ident.t) option = visited := Cfg.NodeSet.add node !visited; let res = ref None in let find_instr = function - | Sil.Set (Sil.Lvar _pvar, _, Sil.Var id, _) when Sil.pvar_equal pvar _pvar && Ident.is_normal id -> + | Sil.Set (Sil.Lvar _pvar, _, Sil.Var id, _) + when Pvar.equal pvar _pvar && Ident.is_normal id -> res := Some (node, id); true | _ -> false in @@ -167,7 +177,7 @@ let find_ident_assignment node id : (Cfg.Node.t * Sil.exp) option = let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option = let find_instr n = let filter = function - | Sil.Set (Sil.Lvar _pvar, _, Sil.Const (Sil.Cint i), _) when Sil.pvar_equal pvar _pvar -> + | Sil.Set (Sil.Lvar _pvar, _, Sil.Const (Sil.Cint i), _) when Pvar.equal pvar _pvar -> Sil.Int.iszero i <> true_branch | _ -> false in IList.exists filter (Cfg.Node.get_instrs n) in @@ -181,14 +191,14 @@ let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option = (** Check whether the program variable is a temporary one generated by CIL *) let pvar_is_cil_tmp pvar = - Sil.pvar_is_local pvar && - let name = Sil.pvar_to_string pvar in + Pvar.is_local pvar && + let name = Pvar.to_string pvar in string_is_prefix "_tmp" name (** Check whether the program variable is a temporary one generated by sawja *) let pvar_is_sawja_tmp pvar = - Sil.pvar_is_local pvar && - let name = Sil.pvar_to_string pvar in + Pvar.is_local pvar && + let name = Pvar.to_string pvar in string_is_prefix "$irvar" name || string_is_prefix "$T" name || string_is_prefix "$bc" name @@ -205,16 +215,26 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp let node_instrs = Cfg.Node.get_instrs node in let find_declaration = function | Sil.Letderef (id0, e, _, _) when Ident.equal id id0 -> - if !verbose then (L.d_str "find_normal_variable_letderef defining "; Sil.d_exp e; L.d_ln ()); + if !verbose + then + (L.d_str "find_normal_variable_letderef defining "; + Sil.d_exp e; L.d_ln ()); res := _exp_lv_dexp seen node e; true - | Sil.Call ([id0], Sil.Const (Sil.Cfun pn), (e, _):: _, _, _) when Ident.equal id id0 && Procname.equal pn (Procname.from_string_c_fun "__cast") -> - if !verbose then (L.d_str "find_normal_variable_letderef cast on "; Sil.d_exp e; L.d_ln ()); + | Sil.Call ([id0], Sil.Const (Sil.Cfun pn), (e, _):: _, _, _) + when Ident.equal id id0 && Procname.equal pn (Procname.from_string_c_fun "__cast") -> + if !verbose + then + (L.d_str "find_normal_variable_letderef cast on "; + Sil.d_exp e; L.d_ln ()); res := _exp_rv_dexp seen node e; true | Sil.Call ([id0], (Sil.Const (Sil.Cfun pname) as fun_exp), args, loc, call_flags) when Ident.equal id id0 -> - if !verbose then (L.d_str "find_normal_variable_letderef function call "; Sil.d_exp fun_exp; L.d_ln ()); + if !verbose + then + (L.d_str "find_normal_variable_letderef function call "; + Sil.d_exp fun_exp; L.d_ln ()); let fun_dexp = Sil.Dconst (Sil.Cfun pname) in let args_dexp = @@ -229,8 +249,14 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp true | _ -> false in ignore (IList.exists find_declaration node_instrs); - if !verbose && !res == None then (L.d_str ("find_normal_variable_letderef could not find " ^ - Ident.to_string id ^ " in node " ^ string_of_int (Cfg.Node.get_id node)); L.d_ln ()); + if !verbose && !res == None + then + (L.d_str + ("find_normal_variable_letderef could not find " ^ + Ident.to_string id ^ + " in node " ^ + string_of_int (Cfg.Node.get_id node)); + L.d_ln ()); !res (** describe lvalue [e] as a dexp *) @@ -381,24 +407,28 @@ let find_normal_variable_letderef = _find_normal_variable_letderef Sil.ExpSet.em let exp_lv_dexp = _exp_lv_dexp Sil.ExpSet.empty let exp_rv_dexp = _exp_rv_dexp Sil.ExpSet.empty -(** Produce a description of a mismatch between an allocation function and a deallocation function *) +(** Produce a description of a mismatch between an allocation function + and a deallocation function *) let explain_allocation_mismatch ra_alloc ra_dealloc = let get_primitive_called is_alloc ra = (* primitive alloc/dealloc function ultimately used, and function actually called *) (* e.g. malloc and my_malloc *) let primitive = match ra.Sil.ra_res with - | Sil.Rmemory mk_alloc -> (if is_alloc then Sil.mem_alloc_pname else Sil.mem_dealloc_pname) mk_alloc + | Sil.Rmemory mk_alloc -> + (if is_alloc then Sil.mem_alloc_pname else Sil.mem_dealloc_pname) mk_alloc | _ -> ra_alloc.Sil.ra_pname in let called = ra.Sil.ra_pname in (primitive, called, ra.Sil.ra_loc) in - Localise.desc_allocation_mismatch (get_primitive_called true ra_alloc) (get_primitive_called false ra_dealloc) + Localise.desc_allocation_mismatch + (get_primitive_called true ra_alloc) (get_primitive_called false ra_dealloc) (** Produce a description of a pointer dangerously coerced to a boolean in a comparison *) let explain_bad_pointer_comparison exp node loc = let dexp_opt = exp_rv_dexp node exp in Localise.desc_bad_pointer_comparison dexp_opt loc -(** check whether the type of leaked [hpred] appears as a predicate in an inductive predicate in [prop] *) +(** check whether the type of leaked [hpred] appears as a predicate + in an inductive predicate in [prop] *) let leak_from_list_abstraction hpred prop = let hpred_type = function | Sil.Hpointsto (_, _, texp) -> @@ -420,7 +450,10 @@ let leak_from_list_abstraction hpred prop = | Some texp -> let env = Prop.prop_pred_env prop in Sil.Predicates.iter env (check_hpara texp) (check_hpara_dll texp); - if !found then (L.d_str "leak_from_list_abstraction of predicate of type "; Sil.d_texp_full texp; L.d_ln()); + if !found + then + (L.d_str "leak_from_list_abstraction of predicate of type "; + Sil.d_texp_full texp; L.d_ln()); !found | None -> false @@ -430,7 +463,7 @@ let find_hpred_typ hpred = match hpred with | _ -> None (** find the type of pvar and remove the pointer, if any *) -let find_pvar_typ_without_ptr prop pvar = +let find_typ_without_ptr prop pvar = let res = ref None in let do_hpred = function | Sil.Hpointsto (e, _, te) when Sil.exp_equal e (Sil.Lvar pvar) -> @@ -452,7 +485,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = let value_str_from_pvars_vpath pvars vpath = if pvars <> [] then begin - let pp = pp_seq (Sil.pp_pvar_value pe_text) in + let pp = pp_seq (Pvar.pp_value pe_text) in let desc_string = pp_to_string pp pvars in Some desc_string end @@ -467,16 +500,18 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = let is_file = match resource_opt with | Some Sil.Rfile -> true | _ -> false in - let check_pvar pvar = (* check that pvar is local or global and has the same type as the leaked hpred *) - (Sil.pvar_is_local pvar || Sil.pvar_is_global pvar) && + let check_pvar pvar = + (* check that pvar is local or global and has the same type as the leaked hpred *) + (Pvar.is_local pvar || Pvar.is_global pvar) && not (pvar_is_frontend_tmp pvar) && - match hpred_typ_opt, find_pvar_typ_without_ptr prop pvar with + match hpred_typ_opt, find_typ_without_ptr prop pvar with | Some (Sil.Sizeof (t1, _)), Some (Sil.Sizeof (Sil.Tptr (_t2, _), _)) -> (try let t2 = Tenv.expand_type tenv _t2 in Sil.typ_equal t1 t2 with exn when exn_not_failure exn -> false) - | Some (Sil.Sizeof (Sil.Tint _, _)), Some (Sil.Sizeof (Sil.Tint _, _)) when is_file -> (* must be a file opened with "open" *) + | Some (Sil.Sizeof (Sil.Tint _, _)), Some (Sil.Sizeof (Sil.Tint _, _)) + when is_file -> (* must be a file opened with "open" *) true | _ -> false in let value_str = match instro with @@ -484,7 +519,10 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = if !verbose then (L.d_str "explain_leak: no current instruction"; L.d_ln ()); value_str_from_pvars_vpath [] vpath | Some (Sil.Nullify (pvar, _, _)) when check_pvar pvar -> - if !verbose then (L.d_str "explain_leak: current instruction is Nullify for pvar "; Sil.d_pvar pvar; L.d_ln ()); + if !verbose + then + (L.d_str "explain_leak: current instruction is Nullify for pvar "; + Pvar.d pvar; L.d_ln ()); (match exp_lv_dexp (State.get_node ()) (Sil.Lvar pvar) with | None -> None | Some de -> Some (Sil.dexp_to_string de)) @@ -492,19 +530,29 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = if !verbose then (L.d_str "explain_leak: current instruction is Abstract"; L.d_ln ()); let get_nullify = function | Sil.Nullify (pvar, _, _) when check_pvar pvar -> - if !verbose then (L.d_str "explain_leak: found nullify before Abstract for pvar "; Sil.d_pvar pvar; L.d_ln ()); + if !verbose + then + (L.d_str "explain_leak: found nullify before Abstract for pvar "; + Pvar.d pvar; L.d_ln ()); [pvar] | _ -> [] in let nullify_pvars = IList.flatten (IList.map get_nullify node_instrs) in - let nullify_pvars_notmp = IList.filter (fun pvar -> not (pvar_is_frontend_tmp pvar)) nullify_pvars in + let nullify_pvars_notmp = + IList.filter (fun pvar -> not (pvar_is_frontend_tmp pvar)) nullify_pvars in value_str_from_pvars_vpath nullify_pvars_notmp vpath | Some (Sil.Set (lexp, _, _, _)) when vpath = None -> - if !verbose then (L.d_str "explain_leak: current instruction Set for "; Sil.d_exp lexp; L.d_ln ()); + if !verbose + then + (L.d_str "explain_leak: current instruction Set for "; + Sil.d_exp lexp; L.d_ln ()); (match exp_lv_dexp node lexp with | Some dexp -> Some (Sil.dexp_to_string dexp) | None -> None) | Some instr -> - if !verbose then (L.d_str "explain_leak: case not matched in instr "; Sil.d_instr instr; L.d_ln()); + if !verbose + then + (L.d_str "explain_leak: case not matched in instr "; + Sil.d_instr instr; L.d_ln()); value_str_from_pvars_vpath [] vpath in let exn_cat, bucket = (* decide whether Exn_user or Exn_developer *) match resource_opt with @@ -512,7 +560,10 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = Exceptions.Exn_user, bucket | None -> if leak_from_list_abstraction hpred prop && value_str != None - then Exceptions.Exn_user, bucket (* we don't know it's been allocated, but it's coming from list abstraction and we have a name *) + then + (* we don't know it's been allocated, + but it's coming from list abstraction and we have a name *) + Exceptions.Exn_user, bucket else Exceptions.Exn_developer, Some (Mleak_buckets.ml_bucket_unknown_origin ()) in exn_cat, Localise.desc_leak hpred_typ_opt value_str resource_opt res_action_opt loc bucket @@ -542,7 +593,10 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option = | None, _ -> () | Some de, typo -> res := Some (Sil.Darrow (de, f)), typo) | lexp -> - if !verbose then (L.d_str "vpath_find do_fse: no match on Eexp "; Sil.d_exp lexp; L.d_ln ())) + if !verbose + then + (L.d_str "vpath_find do_fse: no match on Eexp "; + Sil.d_exp lexp; L.d_ln ())) | _ -> () in let do_sexp sigma_acc' sigma_todo' lexp sexp texp = match sexp with | Sil.Eexp (e, _) when Sil.exp_equal exp e -> @@ -558,7 +612,10 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option = | None, typo -> None, typo | Some de, typo -> Some (Sil.Dderef de), typo) | lexp -> - if !verbose then (L.d_str "vpath_find do_sexp: no match on Eexp "; Sil.d_exp lexp; L.d_ln ()); + if !verbose + then + (L.d_str "vpath_find do_sexp: no match on Eexp "; + Sil.d_exp lexp; L.d_ln ()); None, None) | Sil.Estruct (fsel, _) -> let res = ref (None, None) in @@ -573,12 +630,13 @@ let vpath_find prop _exp : Sil.dexp option * Sil.typ option = | _ -> false in IList.exists filter (Sil.sub_to_list (Prop.get_sub prop)) in function - | Sil.Hpointsto (Sil.Lvar pv, sexp, texp) when (Sil.pvar_is_local pv || Sil.pvar_is_global pv || Sil.pvar_is_seed pv) -> + | Sil.Hpointsto (Sil.Lvar pv, sexp, texp) + when (Pvar.is_local pv || Pvar.is_global pv || Pvar.is_seed pv) -> do_sexp sigma_acc' sigma_todo' (Sil.Lvar pv) sexp texp - | Sil.Hpointsto (Sil.Var id, sexp, texp) when Ident.is_normal id || (Ident.is_footprint id && substituted_from_normal id) -> + | Sil.Hpointsto (Sil.Var id, sexp, texp) + when Ident.is_normal id || (Ident.is_footprint id && substituted_from_normal id) -> do_sexp sigma_acc' sigma_todo' (Sil.Var id) sexp texp | _ -> - (* if !verbose then (L.d_str "vpath_find do_hpred: no match "; Sil.d_hpred hpred; L.d_ln ()); *) None, None in match sigma_todo with | [] -> None, None @@ -617,7 +675,9 @@ let explain_dexp_access prop dexp is_nullable = !res in let rec lookup_fld fsel f = match fsel with | [] -> - if !verbose then (L.d_strln ("lookup_fld: can't find field " ^ Ident.fieldname_to_string f)); + if !verbose + then + (L.d_strln ("lookup_fld: can't find field " ^ Ident.fieldname_to_string f)); None | (f1, se):: fsel' -> if Ident.fieldname_equal f1 f then Some se @@ -638,7 +698,10 @@ let explain_dexp_access prop dexp is_nullable = | Some Sil.Earray (_, esel, _), Some Sil.Eexp (e, _) -> lookup_esel esel e | Some se1, Some se2 -> - if !verbose then (L.d_str "lookup: case not matched on Darray "; Sil.d_sexp se1; L.d_str " "; Sil.d_sexp se2; L.d_ln()); + if !verbose + then + (L.d_str "lookup: case not matched on Darray "; + Sil.d_sexp se1; L.d_str " "; Sil.d_sexp se2; L.d_ln()); None) | Sil.Darrow (de1, f) -> (match lookup (Sil.Dderef de1) with @@ -678,7 +741,9 @@ let explain_dexp_access prop dexp is_nullable = None in let access_opt = match sexpo_to_inst (lookup dexp) with | None -> - if !verbose then (L.d_strln ("explain_dexp_access: cannot find inst of " ^ Sil.dexp_to_string dexp)); + if !verbose + then + (L.d_strln ("explain_dexp_access: cannot find inst of " ^ Sil.dexp_to_string dexp)); None | Some (Sil.Iupdate (_, ncf, n, _)) -> Some (Localise.Last_assigned (n, ncf)) @@ -689,7 +754,11 @@ let explain_dexp_access prop dexp is_nullable = | 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)); + if !verbose + then + (L.d_strln + ("explain_dexp_access: inst is not an update " ^ + Sil.inst_to_string inst)); None in access_opt @@ -730,7 +799,8 @@ let create_dereference_desc let value_str, access_opt = explain_dereference_access outermost_array is_nullable de_opt prop in let access_opt' = match access_opt with - | Some (Localise.Last_accessed _) when outermost_array -> None (* don't report last accessed for arrays *) + | Some (Localise.Last_accessed _) + when outermost_array -> None (* don't report last accessed for arrays *) | _ -> access_opt in let desc = Localise.dereference_string deref_str value_str access_opt' loc in let desc = @@ -762,7 +832,10 @@ let _explain_access if !verbose then (L.d_str "find_outermost_dereference: constant "; Sil.d_exp e; L.d_ln ()); exp_lv_dexp node e | Sil.Var id when Ident.is_normal id -> (* look up the normal variable declaration *) - if !verbose then (L.d_str "find_outermost_dereference: normal var "; Sil.d_exp e; L.d_ln ()); + if !verbose + then + (L.d_str "find_outermost_dereference: normal var "; + Sil.d_exp e; L.d_ln ()); find_normal_variable_letderef node id | Sil.Lfield (e', _, _) -> if !verbose then (L.d_str "find_outermost_dereference: Lfield "; Sil.d_exp e; L.d_ln ()); @@ -774,7 +847,10 @@ let _explain_access if !verbose then (L.d_str "find_outermost_dereference: Lvar "; Sil.d_exp e; L.d_ln ()); exp_lv_dexp node e | Sil.BinOp(Sil.PlusPI, Sil.Lvar _, _) -> - if !verbose then (L.d_str "find_outermost_dereference: Lvar+index "; Sil.d_exp e; L.d_ln ()); + if !verbose + then + (L.d_str "find_outermost_dereference: Lvar+index "; + Sil.d_exp e; L.d_ln ()); exp_lv_dexp node e | Sil.Cast (_, e') -> if !verbose then (L.d_str "find_outermost_dereference: cast "; Sil.d_exp e; L.d_ln ()); @@ -783,7 +859,10 @@ let _explain_access if !verbose then (L.d_str "find_outermost_dereference: PtrFld "; Sil.d_exp e; L.d_ln ()); find_outermost_dereference node e' | _ -> - if !verbose then (L.d_str "find_outermost_dereference: no match for "; Sil.d_exp e; L.d_ln ()); + if !verbose + then + (L.d_str "find_outermost_dereference: no match for "; + Sil.d_exp e; L.d_ln ()); None in let find_exp_dereferenced () = match State.get_instr () with | Some Sil.Set (e, _, _, _) -> @@ -836,8 +915,11 @@ let explain_memory_access deref_str prop loc = (* offset of an expression found following a program variable *) type pvar_off = - | Fpvar (* value of a pvar *) - | Fstruct of Ident.fieldname list (* value obtained by dereferencing the pvar and following a sequence of fields *) + (* value of a pvar *) + | Fpvar + + (* value obtained by dereferencing the pvar and following a sequence of fields *) + | Fstruct of Ident.fieldname list let dexp_apply_pvar_off dexp pvar_off = let rec add_ddot de = function @@ -868,10 +950,10 @@ let explain_nth_function_parameter use_buckets deref_str prop n pvar_off = | _ -> Localise.no_desc (** Find a program variable whose value is [exp] or pointing to a struct containing [exp] *) -let find_pvar_with_exp prop exp = +let find_with_exp prop exp = let res = ref None in let found_in_pvar pv = - if not (Sil.pvar_is_abducted pv) && not (Sil.pvar_is_this pv) then + if not (Pvar.is_abducted pv) && not (Pvar.is_this pv) then res := Some (pv, Fpvar) in let found_in_struct pv fld_lst = (* found_in_pvar has priority *) if !res = None then res := Some (pv, Fstruct (IList.rev fld_lst)) in @@ -902,27 +984,29 @@ let explain_dereference_as_caller_expression let rec find n = function | [] -> 0 | v :: pars -> - if Mangled.equal (Sil.pvar_get_name v) name then n + if Mangled.equal (Pvar.get_name v) name then n else find (n + 1) pars in find 1 formal_params in - match find_pvar_with_exp spec_pre exp with + match find_with_exp spec_pre exp with | Some (pv, pvar_off) -> - if !verbose then L.d_strln ("pvar: " ^ (Sil.pvar_to_string pv)); - let pv_name = Sil.pvar_get_name pv in - if Sil.pvar_is_global pv + if !verbose then L.d_strln ("pvar: " ^ (Pvar.to_string pv)); + let pv_name = Pvar.get_name pv in + if Pvar.is_global pv then let dexp = exp_lv_dexp node (Sil.Lvar pv) in create_dereference_desc ~use_buckets dexp deref_str actual_pre loc - else if Sil.pvar_is_callee pv then + else if Pvar.is_callee pv then let position = find_formal_param_number pv_name in if !verbose then L.d_strln ("parameter number: " ^ string_of_int position); explain_nth_function_parameter use_buckets deref_str actual_pre position pvar_off else if Prop.has_dangling_uninit_attribute spec_pre exp then - Localise.desc_uninitialized_dangling_pointer_deref deref_str (Sil.pvar_to_string pv) loc + Localise.desc_uninitialized_dangling_pointer_deref deref_str (Pvar.to_string pv) loc else Localise.no_desc | None -> - if !verbose then (L.d_str "explain_dereference_as_caller_expression "; Sil.d_exp exp; L.d_str ": cannot explain None "; L.d_ln ()); + if !verbose + then (L.d_str "explain_dereference_as_caller_expression "; + Sil.d_exp exp; L.d_str ": cannot explain None "; L.d_ln ()); Localise.no_desc (** explain a class cast exception *) @@ -961,10 +1045,10 @@ let explain_tainted_value_reaching_sensitive_function prop e { Sil.taint_source; taint_kind } sensitive_fun loc = let var_desc = match e with - | Sil.Lvar pv -> Sil.pvar_to_string pv + | Sil.Lvar pv -> Pvar.to_string pv | _ -> begin - match find_pvar_with_exp prop e with + match find_with_exp prop e with | Some (pvar, pvar_off) -> let dexp = dexp_apply_pvar_off (Sil.Dpvar pvar) pvar_off in Sil.dexp_to_string dexp @@ -1004,11 +1088,13 @@ let explain_condition_always_true_false i cond node loc = (** explain the escape of a stack variable address from its scope *) let explain_stack_variable_address_escape loc pvar addr_dexp_opt = let addr_dexp_str = match addr_dexp_opt with - | Some (Sil.Dpvar pv) when Sil.pvar_is_local pv && Mangled.equal (Sil.pvar_get_name pv) Ident.name_return -> + | Some (Sil.Dpvar pv) + when Pvar.is_local pv && + Mangled.equal (Pvar.get_name pv) Ident.name_return -> Some "the caller via a return" | Some dexp -> Some (Sil.dexp_to_string dexp) | None -> None in - Localise.desc_stack_variable_address_escape (Sil.pvar_to_string pvar) addr_dexp_str loc + Localise.desc_stack_variable_address_escape (Pvar.to_string pvar) addr_dexp_str loc (** explain unary minus applied to unsigned expression *) let explain_unary_minus_applied_to_unsigned_expression exp typ node loc = diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index 3bbaedfb0..40c5aafaf 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -26,14 +26,14 @@ val find_normal_variable_funcall : 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 +val find_program_variable_assignment : Cfg.Node.t -> Pvar.t -> (Cfg.Node.t * Ident.t) option (** Find a program variable assignment to id in the current node or predecessors. *) val find_ident_assignment : Cfg.Node.t -> Ident.t -> (Cfg.Node.t * Sil.exp) option (** Find a boolean assignment to a temporary variable holding a boolean condition. The boolean parameter indicates whether the true or false branch is required. *) -val find_boolean_assignment : Cfg.Node.t -> Sil.pvar -> bool -> Cfg.Node.t option +val find_boolean_assignment : Cfg.Node.t -> Pvar.t -> bool -> Cfg.Node.t option (** describe rvalue [e] as a dexp *) val exp_rv_dexp : Cfg.Node.t -> Sil.exp -> Sil.dexp option @@ -57,7 +57,7 @@ val explain_class_cast_exception : 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 +val explain_deallocate_stack_var : Pvar.t -> Sil.res_action -> Localise.error_desc (** Explain a deallocate constant string error *) val explain_deallocate_constant_string : string -> Sil.res_action -> Localise.error_desc @@ -72,7 +72,7 @@ val explain_dereference : val explain_dereference_as_caller_expression : ?use_buckets:bool -> Localise.deref_str -> 'a Prop.t -> 'b Prop.t -> Sil.exp -> - Cfg.Node.t -> Location.t -> Sil.pvar list -> Localise.error_desc + Cfg.Node.t -> Location.t -> Pvar.t list -> Localise.error_desc (** explain a division by zero *) val explain_divide_by_zero : Sil.exp -> Cfg.Node.t -> Location.t -> Localise.error_desc @@ -92,7 +92,7 @@ val explain_condition_always_true_false : (** explain the escape of a stack variable address from its scope *) val explain_stack_variable_address_escape : - Location.t -> Sil.pvar -> Sil.dexp option -> Localise.error_desc + Location.t -> Pvar.t -> Sil.dexp option -> Localise.error_desc (** explain frontend warning *) val explain_frontend_warning : string -> string -> Location.t -> Localise.error_desc @@ -129,10 +129,10 @@ val explain_null_test_after_dereference : Sil.exp -> Cfg.Node.t -> int -> Location.t -> Localise.error_desc (** Check whether the program variable is a temporary one generated by CIL *) -val pvar_is_cil_tmp : Sil.pvar -> bool +val pvar_is_cil_tmp : Pvar.t -> bool (** Check whether the program variable is a temporary generated by the front-end *) -val pvar_is_frontend_tmp : Sil.pvar -> bool +val pvar_is_frontend_tmp : Pvar.t -> bool (** Print a warning to the err stream at the given location (note: only prints in developer mode) *) val warning_err : Location.t -> ('a, Format.formatter, unit) format -> 'a @@ -143,4 +143,4 @@ type pvar_off = | Fstruct of Ident.fieldname list (* value obtained by dereferencing the pvar and following a sequence of fields *) (** Find a program variable whose value is [exp] or pointing to a struct containing [exp] *) -val find_pvar_with_exp : 'a Prop.t -> Sil.exp -> (Sil.pvar * pvar_off) option +val find_with_exp : 'a Prop.t -> Sil.exp -> (Pvar.t * pvar_off) option diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 77cc7ff32..11ccc36ff 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -644,7 +644,7 @@ let report_context_leaks pname sigma tenv = IList.iter (function | Sil.Hpointsto (Sil.Lvar pv, Sil.Estruct (static_flds, _), _) - when Sil.pvar_is_global pv -> + when Pvar.is_global pv -> IList.iter (fun (f_name, f_strexp) -> check_reachable_context_from_fld (f_name, f_strexp) context_exps) @@ -788,8 +788,8 @@ let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t let create_seed_vars sigma = let hpred_add_seed sigma = function - | Sil.Hpointsto (Sil.Lvar pv, se, typ) when not (Sil.pvar_is_abducted pv) -> - Sil.Hpointsto(Sil.Lvar (Sil.pvar_to_seed pv), se, typ) :: sigma + | Sil.Hpointsto (Sil.Lvar pv, se, typ) when not (Pvar.is_abducted pv) -> + Sil.Hpointsto(Sil.Lvar (Pvar.to_seed pv), se, typ) :: sigma | _ -> sigma in IList.fold_left hpred_add_seed [] sigma @@ -824,7 +824,7 @@ let initial_prop tenv (curr_f: Cfg.Procdesc.t) (prop : 'a Prop.t) add_formals : Prop.normal Prop.t = let construct_decl (x, typ) = - (Sil.mk_pvar x (Cfg.Procdesc.get_proc_name curr_f), typ) in + (Pvar.mk x (Cfg.Procdesc.get_proc_name curr_f), typ) in let new_formals = if add_formals then IList.map construct_decl (Cfg.Procdesc.get_formals curr_f) @@ -1098,7 +1098,7 @@ let custom_error_preconditions summary = let remove_this_not_null prop = let collect_hpred (var_option, hpreds) = function | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (Sil.Var var, _), _) - when !Config.curr_language = Config.Java && Sil.pvar_is_this pvar -> + when !Config.curr_language = Config.Java && Pvar.is_this pvar -> (Some var, hpreds) | hpred -> (var_option, hpred:: hpreds) in let collect_atom var atoms = function diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml index d7809d7ce..6bcfb1d1e 100644 --- a/infer/src/backend/localise.ml +++ b/infer/src/backend/localise.ml @@ -499,7 +499,7 @@ let dereference_string deref_str value_str access_opt loc = let parameter_field_not_null_checked_desc (desc : error_desc) exp = let parameter_not_nullable_desc var = - let var_s = Sil.pvar_to_string var in + let var_s = Pvar.to_string var in let param_not_null_desc = "Parameter "^var_s^" is not checked for null, there could be a null pointer dereference:" in { desc with descriptions = param_not_null_desc :: desc.descriptions; @@ -508,7 +508,7 @@ let parameter_field_not_null_checked_desc (desc : error_desc) exp = let rec exp_to_string exp = match exp with | Sil.Lfield (exp', field, _) -> (exp_to_string exp')^" -> "^(Ident.fieldname_to_string field) - | Sil.Lvar pvar -> Mangled.to_string (Sil.pvar_get_name pvar) + | Sil.Lvar pvar -> Mangled.to_string (Pvar.get_name pvar) | _ -> "" in let var_s = exp_to_string exp in let field_not_null_desc = @@ -724,12 +724,12 @@ let desc_retain_cycle prop cycle loc cycle_dotty = | _ -> s in let do_edge ((se, _), f, _) = match se with - | Sil.Eexp(Sil.Lvar pvar, _) when Sil.pvar_equal pvar Sil.block_pvar -> + | Sil.Eexp(Sil.Lvar pvar, _) when Pvar.equal pvar Sil.block_pvar -> str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") a block capturing "^(Ident.fieldname_to_string f)^"; "; ct:=!ct +1; | Sil.Eexp(Sil.Lvar pvar as e, _) -> let e_str = Sil.exp_to_string e in - let e_str = if Sil.pvar_is_seed pvar then + let e_str = if Pvar.is_seed pvar then remove_old e_str else e_str in str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") object "^e_str^" retaining "^e_str^"."^(Ident.fieldname_to_string f)^", "; @@ -748,7 +748,7 @@ let registered_observer_being_deallocated_str obj_str = let desc_registered_observer_being_deallocated pvar loc = let tags = Tags.create () in - let obj_str = Sil.pvar_to_string pvar in + let obj_str = Pvar.to_string pvar in { no_desc with descriptions = [ registered_observer_being_deallocated_str obj_str ^ at_line tags loc ^ ". Being still registered as observer of the notification " ^ "center, the deallocated object " diff --git a/infer/src/backend/localise.mli b/infer/src/backend/localise.mli index 9b40d2c5f..a295e2c6f 100644 --- a/infer/src/backend/localise.mli +++ b/infer/src/backend/localise.mli @@ -108,7 +108,8 @@ val error_desc_get_tag_call_procedure : error_desc -> string (** get the bucket value of an error_desc, if any *) val error_desc_get_bucket : error_desc -> string option -(** set the bucket value of an error_desc; the boolean indicates where the bucket should be shown in the message *) +(** set the bucket value of an error_desc. + The boolean indicates where the bucket should be shown in the message *) val error_desc_set_bucket : error_desc -> string -> bool -> error_desc (** hash function for error_desc *) @@ -231,7 +232,7 @@ val desc_retain_cycle : val registered_observer_being_deallocated_str : string -> string -val desc_registered_observer_being_deallocated : Sil.pvar -> Location.t -> error_desc +val desc_registered_observer_being_deallocated : Pvar.t -> Location.t -> error_desc val desc_return_statement_missing : Location.t -> error_desc diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index c587ecdf3..741f24b43 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -47,8 +47,8 @@ module AllPreds = struct end module Vset = Set.Make (struct - type t = Sil.pvar - let compare = Sil.pvar_compare + type t = Pvar.t + let compare = Pvar.compare end) let aliased_var = ref Vset.empty @@ -56,12 +56,12 @@ let aliased_var = ref Vset.empty let captured_var = ref Vset.empty let is_not_function cfg x = - let pname = Procname.from_string_c_fun (Mangled.to_string (Sil.pvar_get_name x)) in + let pname = Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name x)) in Cfg.Procdesc.find_from_name cfg pname = None -let is_captured_pvar pdesc x = +let is_captured pdesc x = let captured = Cfg.Procdesc.get_captured pdesc in - IList.exists (fun (m, _) -> (Sil.pvar_to_string x) = (Mangled.to_string m)) captured + IList.exists (fun (m, _) -> (Pvar.to_string x) = (Mangled.to_string m)) captured (** variables read in the expression *) let rec use_exp cfg pdesc (exp: Sil.exp) acc = @@ -69,13 +69,13 @@ let rec use_exp cfg pdesc (exp: Sil.exp) acc = | Sil.Var _ | Sil.Sizeof _ -> acc | Sil.Const (Cclosure { captured_vars }) -> IList.iter - (fun (_, captured_pvar, _) -> captured_var:= Vset.add captured_pvar !captured_var) + (fun (_, captured, _) -> captured_var:= Vset.add captured !captured_var) captured_vars; acc | Sil.Const _ -> acc | Sil.Lvar x -> (* If x is a captured var in the current procdesc don't add it to acc *) - if is_captured_pvar pdesc x then acc else Vset.add x acc + if is_captured pdesc x then acc else Vset.add x acc | Sil.Cast (_, e) | Sil.UnOp (_, e, _) | Sil.Lfield (e, _, _) -> use_exp cfg pdesc e acc | Sil.BinOp (_, e1, e2) | Sil.Lindex (e1, e2) -> use_exp cfg pdesc e1 (use_exp cfg pdesc e2 acc) @@ -161,10 +161,14 @@ end (** table of live variables *) module Table: sig val reset: unit -> unit - val get_live: Cfg.node -> Vset.t (** variables live after the last instruction in the current node *) - val propagate_to_preds: Vset.t -> Cfg.node list -> unit (** propagate live variables to predecessor nodes *) + + (** variables live after the last instruction in the current node *) + val get_live: Cfg.node -> Vset.t + + (** propagate live variables to predecessor nodes *) + val propagate_to_preds: Vset.t -> Cfg.node list -> unit + val iter: Vset.t -> (Cfg.node -> Vset.t -> Vset.t -> unit) -> unit - (* val replace: Cfg.node -> Vset.t -> unit *) end = struct module H = Cfg.NodeHash let table = H.create 1024 @@ -194,7 +198,10 @@ end (** compute the variables which are possibly aliased in node n *) let compute_aliased cfg n aliased_var = match Cfg.Node.get_kind n with - | Cfg.Node.Start_node _ | Cfg.Node.Exit_node _ | Cfg.Node.Join_node | Cfg.Node.Skip_node _ -> aliased_var + | Cfg.Node.Start_node _ + | Cfg.Node.Exit_node _ + | Cfg.Node.Join_node + | Cfg.Node.Skip_node _ -> aliased_var | Cfg.Node.Prune_node _ | Cfg.Node.Stmt_node _ -> def_aliased_var cfg (Cfg.Node.get_proc_desc n) (Cfg.Node.get_instrs n) aliased_var @@ -207,8 +214,9 @@ let compute_candidates procdesc : Vset.t * (Vset.t -> Vset.elt list) = | Sil.Tstruct _ | Sil.Tarray _ -> true | _ -> false in let add_vi (pvar, typ) = - let pv = Sil.mk_pvar pvar (Cfg.Procdesc.get_proc_name procdesc) in - if is_captured_pvar procdesc pv then () (* don't add captured vars of the current pdesc to candidates *) + let pv = Pvar.mk pvar (Cfg.Procdesc.get_proc_name procdesc) in + if is_captured procdesc pv then () + (* don't add captured vars of the current pdesc to candidates *) else ( candidates := Vset.add pv !candidates; if typ_is_struct_array typ then struct_array_cand := Vset.add pv !struct_array_cand @@ -216,7 +224,10 @@ let compute_candidates procdesc : Vset.t * (Vset.t -> Vset.elt list) = IList.iter add_vi (Cfg.Procdesc.get_formals procdesc); IList.iter add_vi (Cfg.Procdesc.get_locals procdesc); let get_sorted_candidates vs = - let priority, no_pri = IList.partition (fun pv -> Vset.mem pv !struct_array_cand) (Vset.elements vs) in + let priority, no_pri = + IList.partition + (fun pv -> Vset.mem pv !struct_array_cand) + (Vset.elements vs) in IList.rev_append (IList.rev priority) no_pri in !candidates, get_sorted_candidates @@ -235,7 +246,10 @@ let analyze_proc cfg pdesc cand = let preds = AllPreds.get_preds node in let live_at_predecessors = match Cfg.Node.get_kind node with - | Cfg.Node.Start_node _ | Cfg.Node.Exit_node _ | Cfg.Node.Join_node | Cfg.Node.Skip_node _ -> curr_live + | Cfg.Node.Start_node _ + | Cfg.Node.Exit_node _ + | Cfg.Node.Join_node + | Cfg.Node.Skip_node _ -> curr_live | Cfg.Node.Prune_node _ | Cfg.Node.Stmt_node _ -> compute_live_instrl cfg pdesc (Cfg.Node.get_instrs node) curr_live in @@ -256,11 +270,17 @@ let node_add_nullify_instrs n dead_vars_after dead_vars_before = let pvars_tmp, pvars_notmp = IList.partition Errdesc.pvar_is_frontend_tmp pvars in pvars_tmp @ pvars_notmp in let instrs_after = - IList.map (fun pvar -> Sil.Nullify (pvar, loc, false)) (move_tmp_pvars_first dead_vars_after) in + IList.map + (fun pvar -> Sil.Nullify (pvar, loc, false)) + (move_tmp_pvars_first dead_vars_after) in let instrs_before = - IList.map (fun pvar -> Sil.Nullify (pvar, loc, false)) (move_tmp_pvars_first dead_vars_before) in - (* Nullify(bloc_var,_,true) can be placed in the middle of the block because when we add this instruction*) - (* we don't have already all the instructions of the node. Here we reorder the instructions to move *) + IList.map + (fun pvar -> Sil.Nullify (pvar, loc, false)) + (move_tmp_pvars_first dead_vars_before) in + (* Nullify(bloc_var,_,true) can be placed in the middle + of the block because when we add this instruction*) + (* we don't have already all the instructions of the node. + Here we reorder the instructions to move *) (* nullification of blocks at the end of existing instructions. *) let block_nullify, no_block_nullify = IList.partition is_block_nullify (Cfg.Node.get_instrs n) in Cfg.Node.replace_instrs n (no_block_nullify @ block_nullify); @@ -275,12 +295,12 @@ let node_assigns_no_variables cfg node = (** Set the dead variables of a node, by default as dead_after. If the node is a prune or a join node, propagate as dead_before in the successors *) -let add_dead_pvars_after_conditionals_join cfg n dead_pvars = - (* L.out " node %d: %a@." (Cfg.Node.get_id n) (Sil.pp_pvar_list pe_text) dead_pvars; *) +let add_deads_after_conditionals_join cfg n deads = + (* L.out " node %d: %a@." (Cfg.Node.get_id n) (Sil.pp_list pe_text) deads; *) let seen = ref Cfg.NodeSet.empty in let rec add_after_prune_join is_after node = if Cfg.NodeSet.mem node !seen (* gone through a loop in the cfg *) - then Cfg.Node.set_dead_pvars n true dead_pvars + then Cfg.Node.set_dead_pvars n true deads else begin seen := Cfg.NodeSet.add node !seen; @@ -291,15 +311,18 @@ let add_dead_pvars_after_conditionals_join cfg n dead_pvars = | [n'] -> node_is_exit n' | _ -> false in match Cfg.Node.get_kind node with - | Cfg.Node.Prune_node _ | Cfg.Node.Join_node when node_assigns_no_variables cfg node && not (next_is_exit node) -> - (* cannot push nullify instructions after an assignment, as they could nullify the same variable *) + | Cfg.Node.Prune_node _ + | Cfg.Node.Join_node + when node_assigns_no_variables cfg node && not (next_is_exit node) -> + (* cannot push nullify instructions after an assignment, + as they could nullify the same variable *) let succs = Cfg.Node.get_succs node in IList.iter (add_after_prune_join false) succs | _ -> let new_dead_pvs = let old_pvs = Cfg.Node.get_dead_pvars node is_after in - let pv_is_new pv = not (IList.exists (Sil.pvar_equal pv) old_pvs) in - (IList.filter pv_is_new dead_pvars) @ old_pvs in + let pv_is_new pv = not (IList.exists (Pvar.equal pv) old_pvs) in + (IList.filter pv_is_new deads) @ old_pvs in Cfg.Node.set_dead_pvars node is_after new_dead_pvs end in add_after_prune_join true n @@ -318,30 +341,34 @@ let analyze_and_annotate_proc cfg pname pdesc = analyze_proc cfg pdesc cand; (* as side effect it coputes the set aliased_var *) (* print_aliased_var "@.@.Aliased variable computed: " !aliased_var; L.out " PROCEDURE %s@." (Procname.to_string pname); *) - let dead_pvars_added = ref 0 in - let dead_pvars_limit = 100000 in - let incr_dead_pvars_added pvars = + let deads_added = ref 0 in + let deads_limit = 100000 in + let incr_deads_added pvars = let num = IList.length pvars in - dead_pvars_added := num + !dead_pvars_added; - if !dead_pvars_added > dead_pvars_limit && !dead_pvars_added - num <= dead_pvars_limit - then L.err "WARNING: liveness: more than %d dead pvars added in procedure %a, stopping@." dead_pvars_limit Procname.pp pname in + deads_added := num + !deads_added; + if !deads_added > deads_limit && !deads_added - num <= deads_limit + then + L.err "WARNING: liveness: more than %d dead pvars added in procedure %a, stopping@." + deads_limit Procname.pp pname in Table.iter cand (fun n live_at_predecessors live_current -> (* set dead variables on nodes *) - let nonnull_pvars = Vset.inter (def_node cfg n live_at_predecessors) cand in (* live before, or assigned to *) - let dead_pvars = Vset.diff nonnull_pvars live_current in (* only nullify when variable become live *) + let nonnull_pvars = + Vset.inter (def_node cfg n live_at_predecessors) cand in (* live before, or assigned to *) + let deads = + Vset.diff nonnull_pvars live_current in (* only nullify when variable become live *) (* L.out " Node %s " (string_of_int (Cfg.Node.get_id n)); *) - let dead_pvars_no_captured = Vset.diff dead_pvars !captured_var in + let deads_no_captured = Vset.diff deads !captured_var in (* print_aliased_var "@.@.Non-nullable variable computed: " nonnull_pvars; - print_aliased_var "@.Dead variable computed: " dead_pvars; + print_aliased_var "@.Dead variable computed: " deads; print_aliased_var "@.Captured variable computed: " !captured_var; - print_aliased_var "@.Dead variable excluding captured computed: " dead_pvars_no_captured; *) - let dead_pvars_no_alias = get_sorted_cand (Vset.diff dead_pvars_no_captured !aliased_var) in - (* print_aliased_var_l "@. Final Dead variable computed: " dead_pvars_no_alias; *) - let dead_pvars_to_add = + print_aliased_var "@.Dead variable excluding captured computed: " deads_no_captured; *) + let deads_no_alias = get_sorted_cand (Vset.diff deads_no_captured !aliased_var) in + (* print_aliased_var_l "@. Final Dead variable computed: " deads_no_alias; *) + let deads_to_add = if exit_node_is_succ n (* add dead aliased vars just before the exit node *) - then dead_pvars_no_alias @ (get_sorted_cand (Vset.inter cand !aliased_var)) - else dead_pvars_no_alias in - incr_dead_pvars_added dead_pvars_to_add; - if !dead_pvars_added < dead_pvars_limit then add_dead_pvars_after_conditionals_join cfg n dead_pvars_to_add); + then deads_no_alias @ (get_sorted_cand (Vset.inter cand !aliased_var)) + else deads_no_alias in + incr_deads_added deads_to_add; + if !deads_added < deads_limit then add_deads_after_conditionals_join cfg n deads_to_add); IList.iter (fun n -> (* generate nullify instructions *) let dead_pvs_after = Cfg.Node.get_dead_pvars n true in let dead_pvs_before = Cfg.Node.get_dead_pvars n false in @@ -474,12 +501,12 @@ let doit ?(f_translate_typ=None) cfg cg tenv = Printing function useful for debugging let print_aliased_var s al_var = L.out s; - Vset.iter (fun v -> L.out " %a, " (Sil.pp_pvar pe_text) v) al_var; + Vset.iter (fun v -> L.out " %a, " (Sil.pp pe_text) v) al_var; L.out "@." Printing function useful for debugging let print_aliased_var_l s al_var = L.out s; - IList.iter (fun v -> L.out " %a, " (Sil.pp_pvar pe_text) v) al_var; + IList.iter (fun v -> L.out " %a, " (Sil.pp pe_text) v) al_var; L.out "@." *) diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 45151eb7d..7de90697b 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -255,8 +255,8 @@ let force_delayed_print fmt = let (p: Prop.normal Prop.t) = Obj.obj p in Prop.pp_prop_with_typ pe_default fmt p | (L.PTpvar, pvar) -> - let (pvar: Sil.pvar) = Obj.obj pvar in - Sil.pp_pvar pe_default fmt pvar + let (pvar: Pvar.t) = Obj.obj pvar in + Pvar.pp pe_default fmt pvar | (L.PTsexp, se) -> let (se: Sil.strexp) = Obj.obj se in Sil.pp_sexp pe_default fmt se diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index b07631bd3..f340206f8 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -103,7 +103,8 @@ let pp_footprint _pe f fp = if fp.foot_pi != [] then F.fprintf f "%a ;@\n" (pp_semicolon_seq_oneline pe (Sil.pp_atom pe)) fp.foot_pi in if fp.foot_pi != [] || fp.foot_sigma != [] then - F.fprintf f "@\n[footprint@\n @[%a%a@] ]" pp_pi () (pp_semicolon_seq pe (Sil.pp_hpred pe)) fp.foot_sigma + F.fprintf f "@\n[footprint@\n @[%a%a@] ]" + pp_pi () (pp_semicolon_seq pe (Sil.pp_hpred pe)) fp.foot_sigma let pp_texp_simple pe = match pe.pe_opt with | PP_SIM_DEFAULT -> Sil.pp_texp pe @@ -115,14 +116,15 @@ let pp_hpred_stackvar pe0 f hpred = begin match hpred with | Sil.Hpointsto (Sil.Lvar pvar, se, te) -> let pe' = match se with - | Sil.Eexp (Sil.Var _, _) when not (Sil.pvar_is_global pvar) -> + | Sil.Eexp (Sil.Var _, _) when not (Pvar.is_global pvar) -> { pe with pe_obj_sub = None } (* dont use obj sub on the var defining it *) | _ -> pe in (match pe'.pe_kind with | PP_TEXT | PP_HTML -> - F.fprintf f "%a = %a:%a" (Sil.pp_pvar_value pe') pvar (Sil.pp_sexp pe') se (pp_texp_simple pe') te + F.fprintf f "%a = %a:%a" + (Pvar.pp_value pe') pvar (Sil.pp_sexp pe') se (pp_texp_simple pe') te | PP_LATEX -> - F.fprintf f "%a{=}%a" (Sil.pp_pvar_value pe') pvar (Sil.pp_sexp pe') se) + F.fprintf f "%a{=}%a" (Pvar.pp_value pe') pvar (Sil.pp_sexp pe') se) | Sil.Hpointsto _ | Sil.Hlseg _ | Sil.Hdllseg _ -> assert false (* should not happen *) end; Sil.color_post_wrapper changed pe0 f @@ -168,7 +170,7 @@ let pp_sigma pe = The boolean indicates whether the stack should only include local variales. *) let sigma_get_stack_nonstack only_local_vars sigma = let hpred_is_stack_var = function - | Sil.Hpointsto (Sil.Lvar pvar, _, _) -> not only_local_vars || Sil.pvar_is_local pvar + | Sil.Hpointsto (Sil.Lvar pvar, _, _) -> not only_local_vars || Pvar.is_local pvar | _ -> false in IList.partition hpred_is_stack_var sigma @@ -184,7 +186,9 @@ let pp_sigma_simple pe env fmt sigma = | PP_LATEX -> Format.fprintf fmt " ; \\\\@\n") in let pp_nonstack fmt = pp_semicolon_seq pe (Sil.pp_hpred_env pe (Some env)) fmt in if sigma_stack != [] || sigma_nonstack != [] then - Format.fprintf fmt "%a%a%a" pp_stack sigma_stack pp_nl (sigma_stack != [] && sigma_nonstack != []) pp_nonstack sigma_nonstack + Format.fprintf fmt "%a%a%a" + pp_stack sigma_stack pp_nl + (sigma_stack != [] && sigma_nonstack != []) pp_nonstack sigma_nonstack (** Dump a sigma. *) let d_sigma (sigma: sigma) = L.add_print_action (L.PTsigma, Obj.repr sigma) @@ -221,25 +225,33 @@ let pp_hpara_simple _pe env n f pred = let pe = pe_reset_obj_sub _pe in (* no free vars: disable object substitution *) match pe.pe_kind with | PP_TEXT | PP_HTML -> - F.fprintf f "P%d = %a%a" n (pp_evars pe) pred.Sil.evars (pp_semicolon_seq pe (Sil.pp_hpred_env pe (Some env))) pred.Sil.body + F.fprintf f "P%d = %a%a" + n (pp_evars pe) pred.Sil.evars + (pp_semicolon_seq pe (Sil.pp_hpred_env pe (Some env))) pred.Sil.body | PP_LATEX -> - F.fprintf f "P_{%d} = %a%a\\\\" n (pp_evars pe) pred.Sil.evars (pp_semicolon_seq pe (Sil.pp_hpred_env pe (Some env))) pred.Sil.body + F.fprintf f "P_{%d} = %a%a\\\\" + n (pp_evars pe) pred.Sil.evars + (pp_semicolon_seq pe (Sil.pp_hpred_env pe (Some env))) pred.Sil.body (** Print an hpara_dll in simple mode *) let pp_hpara_dll_simple _pe env n f pred = let pe = pe_reset_obj_sub _pe in (* no free vars: disable object substitution *) match pe.pe_kind with | PP_TEXT | PP_HTML -> - F.fprintf f "P%d = %a%a" n (pp_evars pe) pred.Sil.evars_dll (pp_semicolon_seq pe (Sil.pp_hpred_env pe (Some env))) pred.Sil.body_dll + F.fprintf f "P%d = %a%a" + n (pp_evars pe) pred.Sil.evars_dll + (pp_semicolon_seq pe (Sil.pp_hpred_env pe (Some env))) pred.Sil.body_dll | PP_LATEX -> - F.fprintf f "P_{%d} = %a%a" n (pp_evars pe) pred.Sil.evars_dll (pp_semicolon_seq pe (Sil.pp_hpred_env pe (Some env))) pred.Sil.body_dll + F.fprintf f "P_{%d} = %a%a" + n (pp_evars pe) pred.Sil.evars_dll + (pp_semicolon_seq pe (Sil.pp_hpred_env pe (Some env))) pred.Sil.body_dll (** Create an environment mapping (ident) expressions to the program variables containing them *) let create_pvar_env (sigma: sigma) : (Sil.exp -> Sil.exp) = let env = ref [] in let filter = function | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (Sil.Var v, _), _) -> - if not (Sil.pvar_is_global pvar) then env := (Sil.Var v, Sil.Lvar pvar) :: !env + if not (Pvar.is_global pvar) then env := (Sil.Var v, Sil.Lvar pvar) :: !env | _ -> () in IList.iter filter sigma; let find e = @@ -277,7 +289,8 @@ let pp_prop pe0 f prop = let pe = prop_update_obj_sub pe0 prop in let latex = pe.pe_kind == PP_LATEX in let do_print f () = - let subl = Sil.sub_to_list (get_sub prop) in (* since prop diff is based on physical equality, we need to extract the sub verbatim *) + let subl = Sil.sub_to_list (get_sub prop) in + (* since prop diff is based on physical equality, we need to extract the sub verbatim *) let pi = get_pi prop in let pp_pure f () = if subl != [] then F.fprintf f "%a ;@\n" (pp_subl pe) subl; @@ -286,7 +299,8 @@ let pp_prop pe0 f prop = begin let env = prop_pred_env prop in let iter_f n hpara = F.fprintf f "@,@[%a@]" (pp_hpara_simple pe env n) hpara in - let iter_f_dll n hpara_dll = F.fprintf f "@,@[%a@]" (pp_hpara_dll_simple pe env n) hpara_dll in + let iter_f_dll n hpara_dll = + F.fprintf f "@,@[%a@]" (pp_hpara_dll_simple pe env n) hpara_dll in let pp_predicates _ () = if Sil.Predicates.is_empty env then () @@ -503,7 +517,8 @@ let sym_eval abs e = | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) -> Sil.exp_bool (v < w) | Sil.Const (Sil.Cint n), Sil.BinOp (Sil.MinusA, f1, f2) -> - Sil.BinOp(Sil.Le, Sil.BinOp (Sil.MinusA, f2, f1), Sil.exp_int (Sil.Int.minus_one -- n)) + Sil.BinOp + (Sil.Le, Sil.BinOp (Sil.MinusA, f2, f1), Sil.exp_int (Sil.Int.minus_one -- n)) | Sil.BinOp(Sil.MinusA, f1 , f2), Sil.Const(Sil.Cint n) -> Sil.exp_le (Sil.BinOp(Sil.MinusA, f1 , f2)) (Sil.exp_int (n -- Sil.Int.one)) | Sil.BinOp (Sil.PlusA, e3, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint m) -> @@ -569,7 +584,8 @@ let sym_eval abs e = | Sil.BinOp(Sil.PlusPI, Sil.Lindex (ep, e1), e2) -> (* array access with pointer arithmetic *) let e' = Sil.BinOp (Sil.PlusA, e1, e2) in eval (Sil.Lindex (ep, e')) - | Sil.BinOp (Sil.PlusPI, (Sil.BinOp (Sil.PlusPI, e11, e12)), e2) -> (* take care of pattern ((ptr + off1) + off2) *) + | Sil.BinOp (Sil.PlusPI, (Sil.BinOp (Sil.PlusPI, e11, e12)), e2) -> + (* take care of pattern ((ptr + off1) + off2) *) (* progress: convert inner +I to +A *) let e2' = Sil.BinOp (Sil.PlusA, e12, e2) in eval (Sil.BinOp (Sil.PlusPI, e11, e2')) @@ -673,7 +689,8 @@ let sym_eval abs e = | Sil.BinOp (Sil.MinusPP, e1, e2) -> if abs then Sil.exp_get_undefined false else Sil.BinOp (Sil.MinusPP, eval e1, eval e2) - | Sil.BinOp (Sil.Mult, esize, Sil.Sizeof (t, st)) | Sil.BinOp(Sil.Mult, Sil.Sizeof (t, st), esize) -> + | Sil.BinOp (Sil.Mult, esize, Sil.Sizeof (t, st)) + | Sil.BinOp(Sil.Mult, Sil.Sizeof (t, st), esize) -> begin match eval esize, eval (Sil.Sizeof (t, st)) with | Sil.Const (Sil.Cint i), e' when Sil.Int.isone i -> e' @@ -720,7 +737,8 @@ let sym_eval abs e = Sil.exp_int (Sil.Int.div n m) | Sil.Const (Sil.Cfloat v), Sil.Const (Sil.Cfloat w) -> Sil.exp_float (v /.w) - | Sil.Sizeof(Sil.Tarray(typ, size), _), Sil.Sizeof(_typ, _) (* pattern: sizeof(arr) / sizeof(arr[0]) = size of arr *) + | Sil.Sizeof(Sil.Tarray(typ, size), _), Sil.Sizeof(_typ, _) + (* pattern: sizeof(arr) / sizeof(arr[0]) = size of arr *) when Sil.typ_equal _typ typ -> size | _ -> @@ -801,7 +819,9 @@ let sym_eval abs e = | Sil.Lfield (e1, fld, typ) -> let e1' = eval e1 in Sil.Lfield (e1', fld, typ) - | Sil.Lindex(Sil.Lvar pv, e2) when false (* removed: it interferes with re-arrangement and error messages *) -> (* &x[n] --> &x + n *) + | Sil.Lindex(Sil.Lvar pv, e2) when false + (* removed: it interferes with re-arrangement and error messages *) + -> (* &x[n] --> &x + n *) eval (Sil.BinOp (Sil.PlusPI, Sil.Lvar pv, e2)) | Sil.Lindex (Sil.BinOp(Sil.PlusPI, ep, e1), e2) -> (* array access with pointer arithmetic *) let e' = Sil.BinOp (Sil.PlusA, e1, e2) in @@ -863,13 +883,15 @@ let atom_is_inequality = function (** If the atom is [e<=n] return [e,n] *) let atom_exp_le_const = function - | Sil.Aeq(Sil.BinOp (Sil.Le, e1, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint i)) when Sil.Int.isone i -> + | Sil.Aeq(Sil.BinOp (Sil.Le, e1, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint i)) + when Sil.Int.isone i -> Some (e1, n) | _ -> None (** If the atom is [n + | Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n), e1), Sil.Const (Sil.Cint i)) + when Sil.Int.isone i -> Some (n, e1) | _ -> None @@ -932,7 +954,8 @@ let mk_inequality e = (** Normalize an inequality *) let inequality_normalize a = - (** turn an expression into a triple (pos,neg,off) of positive and negative occurrences, and integer offset *) + (** turn an expression into a triple (pos,neg,off) of positive and negative occurrences, + and integer offset *) (** representing inequality [sum(pos) - sum(neg) + off <= 0] *) let rec exp_to_posnegoff e = match e with | Sil.Const (Sil.Cint n) -> [],[], n @@ -940,7 +963,9 @@ let inequality_normalize a = let pos1, neg1, n1 = exp_to_posnegoff e1 in let pos2, neg2, n2 = exp_to_posnegoff e2 in (pos1@pos2, neg1@neg2, n1 ++ n2) - | Sil.BinOp(Sil.MinusA, e1, e2) | Sil.BinOp(Sil.MinusPI, e1, e2) | Sil.BinOp(Sil.MinusPP, e1, e2) -> + | Sil.BinOp(Sil.MinusA, e1, e2) + | Sil.BinOp(Sil.MinusPI, e1, e2) + | Sil.BinOp(Sil.MinusPP, e1, e2) -> let pos1, neg1, n1 = exp_to_posnegoff e1 in let pos2, neg2, n2 = exp_to_posnegoff e2 in (pos1@neg2, neg1@pos2, n1 -- n2) @@ -995,13 +1020,16 @@ let exp_reorder e1 e2 = if Sil.exp_compare e1 e2 <= 0 then (e1, e2) else (e2, e1 let atom_normalize sub a0 = let a = Sil.atom_sub sub a0 in let rec normalize_eq eq = match eq with - | Sil.BinOp(Sil.PlusA, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2) (* e1+n1==n2 ---> e1==n2-n1 *) + | Sil.BinOp(Sil.PlusA, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2) + (* e1+n1==n2 ---> e1==n2-n1 *) | Sil.BinOp(Sil.PlusPI, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2) -> (e1, Sil.exp_int (n2 -- n1)) - | Sil.BinOp(Sil.MinusA, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2) (* e1-n1==n2 ---> e1==n1+n2 *) + | Sil.BinOp(Sil.MinusA, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2) + (* e1-n1==n2 ---> e1==n1+n2 *) | Sil.BinOp(Sil.MinusPI, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint n2) -> (e1, Sil.exp_int (n1 ++ n2)) - | Sil.BinOp(Sil.MinusA, Sil.Const (Sil.Cint n1), e1), Sil.Const (Sil.Cint n2) -> (* n1-e1 == n2 -> e1==n1-n2 *) + | Sil.BinOp(Sil.MinusA, Sil.Const (Sil.Cint n1), e1), Sil.Const (Sil.Cint n2) -> + (* n1-e1 == n2 -> e1==n1-n2 *) (e1, Sil.exp_int (n1 -- n2)) | Sil.Lfield (e1', fld1, _), Sil.Lfield (e2', fld2, _) -> if Sil.fld_equal fld1 fld2 @@ -1116,8 +1144,10 @@ let mk_ptsto lexp sexp te = let nsexp = strexp_normalize Sil.sub_empty sexp in Sil.Hpointsto(lexp, nsexp, te) -(** Construct a points-to predicate for an expression using either the provided expression [name] as - base for fresh identifiers. If [expand_structs] is true, initialize the fields of structs with fresh variables. *) +(** Construct a points-to predicate for an expression using + either the provided expression [name] as + base for fresh identifiers. If [expand_structs] is true, + initialize the fields of structs with fresh variables. *) let mk_ptsto_exp tenvo struct_init_mode (exp, te, expo) inst : Sil.hpred = let default_strexp () = match te with | Sil.Sizeof (typ, _) -> @@ -1237,9 +1267,14 @@ let pi_tighten_ineq pi = let nonineq_list' = IList.filter (function - | Sil.Aneq(Sil.Const (Sil.Cint n), e) | Sil.Aneq(e, Sil.Const (Sil.Cint n)) -> - (not (IList.exists (fun (e', n') -> Sil.exp_equal e e' && Sil.Int.lt n' n) le_list_tightened)) && - (not (IList.exists (fun (n', e') -> Sil.exp_equal e e' && Sil.Int.leq n n') lt_list_tightened)) + | Sil.Aneq(Sil.Const (Sil.Cint n), e) + | Sil.Aneq(e, Sil.Const (Sil.Cint n)) -> + (not (IList.exists + (fun (e', n') -> Sil.exp_equal e e' && Sil.Int.lt n' n) + le_list_tightened)) && + (not (IList.exists + (fun (n', e') -> Sil.exp_equal e e' && Sil.Int.leq n n') + lt_list_tightened)) | _ -> true) nonineq_list in (ineq_list', nonineq_list') @@ -1248,11 +1283,14 @@ let pi_tighten_ineq pi = let rec pi_sorted_remove_redundant = function | (Sil.Aeq(Sil.BinOp (Sil.Le, e1, Sil.Const (Sil.Cint n1)), Sil.Const (Sil.Cint i1)) as a1) :: Sil.Aeq(Sil.BinOp (Sil.Le, e2, Sil.Const (Sil.Cint n2)), Sil.Const (Sil.Cint i2)) :: rest - when Sil.Int.isone i1 && Sil.Int.isone i2 && Sil.exp_equal e1 e2 && Sil.Int.lt n1 n2 -> (* second inequality redundant *) + when Sil.Int.isone i1 && Sil.Int.isone i2 && Sil.exp_equal e1 e2 && Sil.Int.lt n1 n2 -> + (* second inequality redundant *) pi_sorted_remove_redundant (a1 :: rest) | Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n1), e1), Sil.Const (Sil.Cint i1)) :: - (Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n2), e2), Sil.Const (Sil.Cint i2)) as a2) :: rest - when Sil.Int.isone i1 && Sil.Int.isone i2 && Sil.exp_equal e1 e2 && Sil.Int.lt n1 n2 -> (* first inequality redundant *) + (Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n2), e2), Sil.Const (Sil.Cint i2)) as a2) :: + rest + when Sil.Int.isone i1 && Sil.Int.isone i2 && Sil.exp_equal e1 e2 && Sil.Int.lt n1 n2 -> + (* first inequality redundant *) pi_sorted_remove_redundant (a2 :: rest) | a1:: a2:: rest -> if Sil.atom_equal a1 a2 then pi_sorted_remove_redundant (a2 :: rest) @@ -1281,10 +1319,14 @@ let pi_normalize sub sigma pi0 = Sil.binop_equal op1 op2 && Sil.binop_injective op1 && not (Sil.const_equal c1 c2) | e1, Sil.BinOp(op2, e2, Sil.Const(c2)) when Sil.exp_equal e1 e2 -> - Sil.binop_injective op2 && Sil.binop_is_zero_runit op2 && not (Sil.const_equal (Sil.Cint Sil.Int.zero) c2) + Sil.binop_injective op2 && + Sil.binop_is_zero_runit op2 && + not (Sil.const_equal (Sil.Cint Sil.Int.zero) c2) | Sil.BinOp(op1, e1, Sil.Const(c1)), e2 when Sil.exp_equal e1 e2 -> - Sil.binop_injective op1 && Sil.binop_is_zero_runit op1 && not (Sil.const_equal (Sil.Cint Sil.Int.zero) c1) + Sil.binop_injective op1 && + Sil.binop_is_zero_runit op1 && + not (Sil.const_equal (Sil.Cint Sil.Int.zero) c1) | _ -> false in let filter_useful_atom = let unsigned_exps = lazy (sigma_get_unsigned_exps sigma) in @@ -1296,7 +1338,10 @@ let pi_normalize sub sigma pi0 = | Sil.Aeq(Sil.Const c1, Sil.Const c2) -> not (Sil.const_equal c1 c2) | _ -> true in - let pi' = IList.stable_sort Sil.atom_compare ((IList.filter filter_useful_atom nonineq_list) @ ineq_list) in + let pi' = + IList.stable_sort + Sil.atom_compare + ((IList.filter filter_useful_atom nonineq_list) @ ineq_list) in let pi'' = pi_sorted_remove_redundant pi' in if pi_equal pi0 pi'' then pi0 else pi'' @@ -1305,7 +1350,8 @@ let sigma_normalize sub sigma = IList.stable_sort Sil.hpred_compare (IList.map (hpred_normalize sub) sigma) in if sigma_equal sigma sigma' then sigma else sigma' -(** normalize the footprint part, and rename any primed vars in the footprint with fresh footprint vars *) +(** normalize the footprint part, and rename any primed vars + in the footprint with fresh footprint vars *) let footprint_normalize prop = let nsigma = sigma_normalize Sil.sub_empty prop.foot_sigma in let npi = pi_normalize Sil.sub_empty nsigma prop.foot_pi in @@ -1328,7 +1374,8 @@ let footprint_normalize prop = let ids_primed = Sil.fav_to_list fp_vars in let ids_footprint = IList.map (fun id -> (id, Ident.create_fresh Ident.kfootprint)) ids_primed in - let ren_sub = Sil.sub_of_list (IList.map (fun (id1, id2) -> (id1, Sil.Var id2)) ids_footprint) in + let ren_sub = + Sil.sub_of_list (IList.map (fun (id1, id2) -> (id1, Sil.Var id2)) ids_footprint) in let nsigma' = sigma_normalize Sil.sub_empty (sigma_sub ren_sub nsigma) in let npi' = pi_normalize Sil.sub_empty nsigma' (pi_sub ren_sub npi) in (npi', nsigma') in @@ -1445,7 +1492,7 @@ let mk_eq e1 e2 = (** Construct a points-to predicate for a single program variable. If [expand_structs] is true, initialize the fields of structs with fresh variables. *) -let mk_ptsto_lvar tenv expand_structs inst ((pvar: Sil.pvar), texp, expo) : Sil.hpred = +let mk_ptsto_lvar tenv expand_structs inst ((pvar: Pvar.t), texp, expo) : Sil.hpred = mk_ptsto_exp tenv expand_structs (Sil.Lvar pvar, texp, expo) inst (** Sil.Construct a lseg predicate *) @@ -1460,12 +1507,23 @@ let mk_dllseg k para exp_iF exp_oB exp_oF exp_iB exps_shared = (** Sil.Construct a hpara *) let mk_hpara root next svars evars body = - let para = { Sil.root = root; Sil.next = next; Sil.svars = svars; Sil.evars = evars; Sil.body = body } in + let para = + { Sil.root = root; + next = next; + svars = svars; + evars = evars; + body = body } in hpara_normalize para (** Sil.Construct a dll_hpara *) let mk_dll_hpara iF oB oF svars evars body = - let para = { Sil.cell = iF; Sil.blink = oB; Sil.flink = oF; Sil.svars_dll = svars; Sil.evars_dll = evars; Sil.body_dll = body } in + let para = + { Sil.cell = iF; + blink = oB; + flink = oF; + svars_dll = svars; + evars_dll = evars; + body_dll = body } in hpara_dll_normalize para (** Proposition [true /\ emp]. *) @@ -1632,12 +1690,14 @@ let sigma_intro_nonemptylseg e1 e2 sigma = let normalize_and_strengthen_atom (p : normal t) (a : Sil.atom) : Sil.atom = let a' = atom_normalize p.sub a in match a' with - | Sil.Aeq (Sil.BinOp (Sil.Le, Sil.Var id, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint i)) when Sil.Int.isone i -> + | Sil.Aeq (Sil.BinOp (Sil.Le, Sil.Var id, Sil.Const (Sil.Cint n)), Sil.Const (Sil.Cint i)) + when Sil.Int.isone i -> let lower = Sil.exp_int (n -- Sil.Int.one) in let a_lower = Sil.Aeq (Sil.BinOp (Sil.Lt, lower, Sil.Var id), Sil.exp_one) in if not (IList.mem Sil.atom_equal a_lower p.pi) then a' else Sil.Aeq (Sil.Var id, Sil.exp_int n) - | Sil.Aeq (Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n), Sil.Var id), Sil.Const (Sil.Cint i)) when Sil.Int.isone i -> + | Sil.Aeq (Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n), Sil.Var id), Sil.Const (Sil.Cint i)) + when Sil.Int.isone i -> let upper = Sil.exp_int (n ++ Sil.Int.one) in let a_upper = Sil.Aeq (Sil.BinOp (Sil.Le, Sil.Var id, upper), Sil.exp_one) in if not (IList.mem Sil.atom_equal a_upper p.pi) then a' @@ -1909,8 +1969,11 @@ let attribute_map_resource prop f = (** type for arithmetic problems *) type arith_problem = - | Div0 of Sil.exp (* division by zero *) - | UminusUnsigned of Sil.exp * Sil.typ (* unary minus of unsigned type applied to the given expression *) + (* division by zero *) + | Div0 of Sil.exp + + (* unary minus of unsigned type applied to the given expression *) + | UminusUnsigned of Sil.exp * Sil.typ (** Look for an arithmetic problem in [exp] *) let find_arithmetic_problem proc_node_session prop exp = @@ -1925,7 +1988,9 @@ let find_arithmetic_problem proc_node_session prop exp = false in let rec walk = function | Sil.Var _ -> () - | Sil.UnOp (Sil.Neg, e, Some ((Sil.Tint (Sil.IUChar | Sil.IUInt | Sil.IUShort | Sil.IULong | Sil.IULongLong) as typ))) -> + | Sil.UnOp (Sil.Neg, e, Some ( + (Sil.Tint + (Sil.IUChar | Sil.IUInt | Sil.IUShort | Sil.IULong | Sil.IULongLong) as typ))) -> uminus_unsigned := (e, typ) :: !uminus_unsigned | Sil.UnOp(_, e, _) -> walk e | Sil.BinOp(op, e1, e2) -> @@ -1949,7 +2014,7 @@ let find_arithmetic_problem proc_node_session prop exp = let deallocate_stack_vars p pvars = let filter = function | Sil.Hpointsto (Sil.Lvar v, _, _) -> - IList.exists (Sil.pvar_equal v) pvars + IList.exists (Pvar.equal v) pvars | _ -> false in let sigma_stack, sigma_other = IList.partition filter p.sigma in let fresh_address_vars = ref [] in (* fresh vars substituted for the address of stack vars *) @@ -1962,7 +2027,11 @@ let deallocate_stack_vars p pvars = | _ -> assert false) sigma_stack in let pi1 = IList.map (fun (id, e) -> Sil.Aeq (Sil.Var id, e)) (Sil.sub_to_list p.sub) in let pi = IList.map (Sil.atom_replace_exp exp_replace) (p.pi @ pi1) in - let p' = { p with sub = Sil.sub_empty; pi = []; sigma = sigma_replace_exp exp_replace sigma_other } in + let p' = + { p with + sub = Sil.sub_empty; + pi = []; + sigma = sigma_replace_exp exp_replace sigma_other } in let p'' = let res = ref p' in let p'_fav = prop_fav p' in @@ -1996,7 +2065,10 @@ let extract_spec p = (** [prop_set_fooprint p p_foot] sets proposition [p_foot] as footprint of [p]. *) let prop_set_footprint p p_foot = - let pi = (IList.map (fun (i, e) -> Sil.Aeq(Sil.Var i, e)) (Sil.sub_to_list p_foot.sub)) @ p_foot.pi in + let pi = + (IList.map + (fun (i, e) -> Sil.Aeq(Sil.Var i, e)) + (Sil.sub_to_list p_foot.sub)) @ p_foot.pi in { p with foot_pi = pi; foot_sigma = p_foot.sigma } (** {2 Functions for renaming primed variables by "canonical names"} *) @@ -2301,7 +2373,12 @@ and hpara_dll_ren para = let svars' = IList.map (ident_captured_ren ren) para.Sil.svars_dll in let evars' = IList.map (ident_captured_ren ren) para.Sil.evars_dll in let body' = IList.map (hpred_captured_ren ren) para.Sil.body_dll in - { Sil.cell = iF; Sil.flink = oF; Sil.blink = oB; Sil.svars_dll = svars'; Sil.evars_dll = evars'; Sil.body_dll = body'} + { Sil.cell = iF; + flink = oF; + blink = oB; + svars_dll = svars'; + evars_dll = evars'; + body_dll = body'} let pi_captured_ren ren pi = IList.map (atom_captured_ren ren) pi @@ -2401,7 +2478,10 @@ let prop_expmap (fe: Sil.exp -> Sil.exp) prop = (** convert identifiers in fav to kind [k] *) let vars_make_unprimed fav prop = let ids = Sil.fav_to_list fav in - let ren_sub = Sil.sub_of_list (IList.map (fun i -> (i, Sil.Var (Ident.create_fresh Ident.knormal))) ids) in + let ren_sub = + Sil.sub_of_list (IList.map + (fun i -> (i, Sil.Var (Ident.create_fresh Ident.knormal))) + ids) in prop_ren_sub ren_sub prop (** convert the normal vars to primed vars. *) @@ -2480,7 +2560,11 @@ let prop_iter_to_prop iter = let sigma = IList.rev_append iter.pit_old (iter.pit_curr:: iter.pit_new) in let prop = normalize - { sub = iter.pit_sub; pi = iter.pit_pi; sigma = sigma; foot_pi = iter.pit_foot_pi; foot_sigma = iter.pit_foot_sigma } in + { sub = iter.pit_sub; + pi = iter.pit_pi; + sigma = sigma; + foot_pi = iter.pit_foot_pi; + foot_sigma = iter.pit_foot_sigma } in IList.fold_left (fun p (footprint, atom) -> prop_atom_and ~footprint: footprint p atom) prop iter.pit_newpi @@ -2737,14 +2821,18 @@ let trans_land_lor op ((idl1, stml1), e1) ((idl2, stml2), e2) loc = | _ -> assert false in let cond_res1 = Sil.BinOp(Sil.Eq, Sil.Var id, e2) in let cond_res2 = Sil.BinOp(Sil.Eq, Sil.Var id, Sil.exp_int res) in - let mk_prune cond = Sil.Prune (cond, loc, true, Sil.Ik_land_lor) (* don't report always true/false *) in + let mk_prune cond = + (* don't report always true/false *) + Sil.Prune (cond, loc, true, Sil.Ik_land_lor) in mk_prune cond1, mk_prune cond_res1, mk_prune cond2, mk_prune cond_res2 in - let instrs2 = mk_nondet (prune_instr1 :: stml2 @ [prune_res1]) ([prune_instr2; prune_res2]) loc in + let instrs2 = + mk_nondet (prune_instr1 :: stml2 @ [prune_res1]) ([prune_instr2; prune_res2]) loc in ((id:: idl1@idl2, stml1@instrs2), Sil.Var id) end (** Input of this mehtod is an exp in a prop. Output is a formal variable or path from a - formal variable that is equal to the expression, or the OBJC_NULL attribute of the expression. *) + formal variable that is equal to the expression, + or the OBJC_NULL attribute of the expression. *) let find_equal_formal_path e prop = let rec find_in_sigma e seen_hpreds = IList.fold_right ( @@ -2757,7 +2845,8 @@ let find_equal_formal_path e prop = | None -> match hpred with | Sil.Hpointsto (Sil.Lvar pvar1, Sil.Eexp (exp2, Sil.Iformal(_, _) ), _) - when Sil.exp_equal exp2 e && (Sil.pvar_is_local pvar1 || Sil.pvar_is_seed pvar1) -> + when Sil.exp_equal exp2 e && + (Pvar.is_local pvar1 || Pvar.is_seed pvar1) -> Some (Sil.Lvar pvar1) | Sil.Hpointsto (exp1, Sil.Estruct (fields, _), _) -> IList.fold_right (fun (field, strexp) res -> @@ -2786,11 +2875,14 @@ let trans_if_then_else ((idl1, stml1), e1) ((idl2, stml2), e2) ((idl3, stml3), e let e1not = Sil.UnOp(Sil.LNot, e1, None) in let id = Ident.create_fresh Ident.knormal in let mk_prune_res e = - let mk_prune cond = Sil.Prune (cond, loc, true, Sil.Ik_land_lor) (* don't report always true/false *) in + let mk_prune cond = Sil.Prune (cond, loc, true, Sil.Ik_land_lor) + (* don't report always true/false *) in mk_prune (Sil.BinOp(Sil.Eq, Sil.Var id, e)) in let prune1 = Sil.Prune (e1, loc, true, Sil.Ik_bexp) in let prune1not = Sil.Prune (e1not, loc, false, Sil.Ik_bexp) in - let stml' = mk_nondet (prune1 :: stml2 @ [mk_prune_res e2]) (prune1not :: stml3 @ [mk_prune_res e3]) loc in + let stml' = + mk_nondet + (prune1 :: stml2 @ [mk_prune_res e2]) (prune1not :: stml3 @ [mk_prune_res e3]) loc in (id:: idl1@idl2@idl3, stml1@stml'), Sil.Var id (*** START of module Metrics ***) @@ -2860,10 +2952,16 @@ end module CategorizePreconditions = struct type pre_category = - | NoPres (* no preconditions *) - | Empty (* the preconditions impose no restrictions *) - | OnlyAllocation (* the preconditions only demand that some pointers are allocated *) - | DataConstraints (* the preconditions impose constraints on the values of variables and/or memory *) + (* no preconditions *) + | NoPres + + (* the preconditions impose no restrictions *) + | Empty + (* the preconditions only demand that some pointers are allocated *) + | OnlyAllocation + + (* the preconditions impose constraints on the values of variables and/or memory *) + | DataConstraints (** categorize a list of preconditions *) let categorize preconditions = diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 672399f0f..7a9a87262 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -119,7 +119,7 @@ val prop_fav_nonpure : normal t -> fav val prop_footprint_fav : 'a t -> fav (** Compute all the free program variables in the prop *) -val prop_fpv: 'a t -> Sil.pvar list +val prop_fpv: 'a t -> Pvar.t list (** Apply substitution for pi *) val pi_sub : subst -> atom list -> atom list @@ -159,8 +159,11 @@ val atom_negate : Sil.atom -> Sil.atom (** type for arithmetic problems *) type arith_problem = - | Div0 of Sil.exp (* division by zero *) - | UminusUnsigned of Sil.exp * Sil.typ (* unary minus of unsigned type applied to the given expression *) + (* division by zero *) + | Div0 of Sil.exp + + (* unary minus of unsigned type applied to the given expression *) + | UminusUnsigned of Sil.exp * Sil.typ (** Look for an arithmetic problem in [exp] *) val find_arithmetic_problem : path_pos -> normal t -> Sil.exp -> arith_problem option * normal t @@ -228,7 +231,7 @@ val mk_ptsto_exp : Tenv.t option -> struct_init_mode -> exp * exp * exp option - (** Construct a points-to predicate for a single program variable. If [expand_structs] is true, initialize the fields of structs with fresh variables. *) val mk_ptsto_lvar : - Tenv.t option -> struct_init_mode -> Sil.inst -> pvar * exp * exp option -> hpred + Tenv.t option -> struct_init_mode -> Sil.inst -> Pvar.t * exp * exp option -> hpred (** Construct a lseg predicate *) val mk_lseg : lseg_kind -> hpara -> exp -> exp -> exp list -> hpred @@ -240,7 +243,8 @@ val mk_dllseg : lseg_kind -> hpara_dll -> exp -> exp -> exp -> exp -> exp list - val mk_hpara : Ident.t -> Ident.t -> Ident.t list -> Ident.t list -> hpred list -> hpara (** Construct a dll_hpara *) -val mk_dll_hpara : Ident.t -> Ident.t -> Ident.t -> Ident.t list -> Ident.t list -> hpred list -> hpara_dll +val mk_dll_hpara : + Ident.t -> Ident.t -> Ident.t -> Ident.t list -> Ident.t list -> hpred list -> hpara_dll (** Proposition [true /\ emp]. *) val prop_emp : normal t @@ -316,7 +320,8 @@ val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Location. (** Remove an attribute from all the atoms in the heap *) val remove_attribute : Sil.attribute -> 'a t -> normal t -(** [replace_objc_null lhs rhs]. If rhs has the objc_null attribute, replace the attribute and set the lhs = 0 *) +(** [replace_objc_null lhs rhs]. + If rhs has the objc_null attribute, replace the attribute and set the lhs = 0 *) val replace_objc_null : normal t -> exp -> exp -> normal t val nullify_exp_with_objc_null : normal t -> exp -> normal t @@ -347,7 +352,7 @@ val get_sigma_footprint : 'a t -> hpred list (** Deallocate the stack variables in [pvars], and replace them by normal variables. Return the list of stack variables whose address was still present after deallocation. *) -val deallocate_stack_vars : normal t -> pvar list -> Sil.pvar list * normal t +val deallocate_stack_vars : normal t -> Pvar.t list -> Pvar.t list * normal t (** Canonicalize the names of primed variables. *) val prop_rename_primed_footprint_vars : normal t -> normal t @@ -512,10 +517,17 @@ end module CategorizePreconditions : sig type pre_category = - | NoPres (* no preconditions *) - | Empty (* the preconditions impose no restrictions *) - | OnlyAllocation (* the preconditions only demand that some pointers are allocated *) - | DataConstraints (* the preconditions impose constraints on the values of variables and/or memory *) + (* no preconditions *) + | NoPres + + (* the preconditions impose no restrictions *) + | Empty + + (* the preconditions only demand that some pointers are allocated *) + | OnlyAllocation + + (* the preconditions impose constraints on the values of variables and/or memory *) + | DataConstraints (** categorize a list of preconditions *) val categorize : 'a t list -> pre_category diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index f67fee77a..bc5ddba04 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -819,18 +819,18 @@ let check_inconsistency_base prop = let procedure_attr = Cfg.Procdesc.get_attributes procdesc in let is_java_this pvar = - !Config.curr_language = Config.Java && Sil.pvar_is_this pvar in + !Config.curr_language = Config.Java && Pvar.is_this pvar in let is_objc_instance_self pvar = !Config.curr_language = Config.C_CPP && - Sil.pvar_get_name pvar = Mangled.from_string "self" && + Pvar.get_name pvar = Mangled.from_string "self" && procedure_attr.ProcAttributes.is_objc_instance_method in let is_cpp_this pvar = - !Config.curr_language = Config.C_CPP && Sil.pvar_is_this pvar && + !Config.curr_language = Config.C_CPP && Pvar.is_this pvar && procedure_attr.ProcAttributes.is_cpp_instance_method in let do_hpred = function | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) -> Sil.exp_equal e Sil.exp_zero && - Sil.pvar_is_seed pv && + Pvar.is_seed pv && (is_java_this pv || is_cpp_this pv || is_objc_instance_self pv) | _ -> false in IList.exists do_hpred sigma in @@ -1139,13 +1139,13 @@ let exp_imply calc_missing subs e1_in e2_in : subst2 = let () = ProverState.add_missing_pi (Sil.Aeq (e1_in, e2_in)) in subs else raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2)))) - | Sil.Lvar pv1, Sil.Const _ when Sil.pvar_is_global pv1 -> + | Sil.Lvar pv1, Sil.Const _ when Pvar.is_global pv1 -> if calc_missing then let () = ProverState.add_missing_pi (Sil.Aeq (e1_in, e2_in)) in subs else raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2)))) | Sil.Lvar v1, Sil.Lvar v2 -> - if Sil.pvar_equal v1 v2 then subs + if Pvar.equal v1 v2 then subs else raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2)))) | Sil.Const c1, Sil.Const c2 -> if (Sil.const_equal c1 c2) then subs @@ -1682,7 +1682,7 @@ let sexp_imply_preprocess se1 texp1 se2 = match se1, texp1, se2 with of the one in the callee, add a type frame and type missing *) let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2) = let is_callee = match e1 with - | Sil.Lvar pv -> Sil.pvar_is_callee pv + | Sil.Lvar pv -> Pvar.is_callee pv | _ -> false in let is_allocated_lhs e = let filter = function diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index a5f201336..7b505d053 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -424,7 +424,7 @@ let mk_ptsto_exp_footprint | 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 + let fun_name = Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in let fun_exp = Sil.Const (Sil.Cfun fun_name) in ([], Prop.mk_ptsto root (Sil.Eexp (fun_exp, inst)) (Sil.Sizeof (typ, st))) | _, [], Sil.Tfun _ -> @@ -512,7 +512,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst = end; let extend_kind = match e with (* Determine whether to extend the footprint part or just the normal part *) | Sil.Var id when not (Ident.is_footprint id) -> Ident.kprimed - | Sil.Lvar pvar when Sil.pvar_is_local pvar -> Ident.kprimed + | Sil.Lvar pvar when Pvar.is_local pvar -> Ident.kprimed | _ -> Ident.kfootprint in let iter_list = let atoms_se_te_list = @@ -945,9 +945,9 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc = when Sil.exp_equal exp deref_exp -> let is_nullable = Annotations.param_is_nullable pvar ann_sig in if is_nullable then - nullable_obj_str := Some (Sil.pvar_to_string pvar); + nullable_obj_str := Some (Pvar.to_string pvar); (* it's ok for a non-nullable local to point to deref_exp *) - is_nullable || Sil.pvar_is_local pvar + is_nullable || Pvar.is_local pvar | Sil.Hpointsto (_, Sil.Estruct (flds, _), Sil.Sizeof (typ, _)) -> let fld_is_nullable fld = match Annotations.get_field_type_and_annotation fld typ with @@ -1047,7 +1047,7 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc = let is_fun_exp_captured_var () = (* Called expression is a captured variable of the block *) match get_exp_called () with | Some (_, Sil.Lvar pvar) -> (* pvar is the block *) - let name = Sil.pvar_get_name pvar in + let name = Pvar.get_name pvar in IList.exists (fun (cn, _) -> (Mangled.to_string name) = (Mangled.to_string cn)) (Cfg.Procdesc.get_captured pdesc) | _ -> false in let is_field_deref () = (*Called expression is a field *) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 6d488d0ed..a61491f77 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -51,7 +51,7 @@ let get_blocks_nullified node = (** Given a proposition and an objc block checks whether by existentially quantifying captured variables in the block we obtain a leak. *) let check_block_retain_cycle tenv caller_pname prop block_nullified = - let mblock = Sil.pvar_get_name block_nullified in + let mblock = Pvar.get_name block_nullified in let block_pname = Procname.mangled_objc_block (Mangled.to_string mblock) in let block_captured = match AttributesTable.load_attributes block_pname with @@ -473,7 +473,7 @@ let check_already_dereferenced pname cond prop = let check_deallocate_static_memory prop_after = let check_deallocated_attribute = function | Sil.Lvar pv, Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra) - when Sil.pvar_is_local pv || Sil.pvar_is_global pv -> + when Pvar.is_local pv || Pvar.is_global pv -> let freed_desc = Errdesc.explain_deallocate_stack_var pv ra in raise (Exceptions.Deallocate_stack_variable freed_desc) | Sil.Const (Sil.Cstr s), Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra) -> @@ -834,14 +834,14 @@ let add_constraints_on_retval pdesc prop ret_exp typ callee_pname callee_loc = let already_has_abducted_retval p abducted_ret_pv = IList.exists (fun hpred -> match hpred with - | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ret_pv + | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Pvar.equal pv abducted_ret_pv | _ -> false) (Prop.get_sigma_footprint p) in - (* find an hpred [abducted_pvar] |-> A in [prop] and add [exp] = A to prop *) - let bind_exp_to_abducted_val exp_to_bind abducted_pvar prop = + (* find an hpred [abducted] |-> A in [prop] and add [exp] = A to prop *) + let bind_exp_to_abducted_val exp_to_bind abducted prop = let bind_exp prop = function | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (rhs, _), _) - when Sil.pvar_equal pv abducted_pvar -> + when Pvar.equal pv abducted -> Prop.conjoin_eq exp_to_bind rhs prop | _ -> prop in IList.fold_left bind_exp prop (Prop.get_sigma prop) in @@ -855,7 +855,7 @@ let add_constraints_on_retval pdesc prop ret_exp typ callee_pname callee_loc = if !Config.angelic_execution && not (is_rec_call callee_pname) then (* introduce a fresh program variable to allow abduction on the return value *) - let abducted_ret_pv = Sil.mk_pvar_abducted_ret callee_pname callee_loc in + let abducted_ret_pv = Pvar.mk_abducted_ret callee_pname callee_loc in (* prevent introducing multiple abducted retvals for a single call site in a loop *) if already_has_abducted_retval prop abducted_ret_pv then prop else @@ -1200,7 +1200,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path let eprop = Prop.expose prop_ in match IList.partition (function - | Sil.Hpointsto (Sil.Lvar pvar', _, _) -> Sil.pvar_equal pvar pvar' + | Sil.Hpointsto (Sil.Lvar pvar', _, _) -> Pvar.equal pvar pvar' | _ -> false) (Prop.get_sigma eprop) with | [Sil.Hpointsto(e, se, typ)], sigma' -> let sigma'' = match deallocate with @@ -1289,11 +1289,11 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call | Sil.Lvar actual_pv -> (* introduce a fresh program variable to allow abduction on the return value *) let abducted_ref_pv = - Sil.mk_pvar_abducted_ref_param callee_pname actual_pv callee_loc in + Pvar.mk_abducted_ref_param callee_pname actual_pv callee_loc in let already_has_abducted_retval p = IList.exists (fun hpred -> match hpred with - | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ref_pv + | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Pvar.equal pv abducted_ref_pv | _ -> false) (Prop.get_sigma_footprint p) in (* prevent introducing multiple abducted retvals for a single call site in a loop *) @@ -1337,7 +1337,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call IList.fold_left (fun p hpred -> match hpred with - | Sil.Hpointsto (Sil.Lvar pv, rhs, texp) when Sil.pvar_equal pv abducted_ref_pv -> + | Sil.Hpointsto (Sil.Lvar pv, rhs, texp) when Pvar.equal pv abducted_ref_pv -> let new_hpred = Sil.Hpointsto (actual, rhs, texp) in Prop.normalize (Prop.replace_sigma (new_hpred :: (Prop.get_sigma prop')) p) | _ -> p) @@ -2519,7 +2519,7 @@ module ModelBuiltins = struct let routine_arg = Prop.exp_normalize_prop prop_ (fst arg) in (match routine_name, (snd start_routine) with | Sil.Lvar pvar, _ -> - let fun_name = Sil.pvar_get_name pvar in + let fun_name = Pvar.get_name pvar in let fun_string = Mangled.to_string fun_name in L.d_strln ("pthread_create: calling function " ^ fun_string); begin diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 085538c9d..4a1d5f58b 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -33,11 +33,20 @@ type deref_error = | Deref_undef_exp (** dereference an undefined expression *) type invalid_res = - | Dereference_error of deref_error * Localise.error_desc * Paths.Path.t option (** dereference error and description *) - | Prover_checks of Prover.check list (** the abduction prover failed some checks *) - | Cannot_combine (** cannot combine actual pre with splitting and post *) - | Missing_fld_not_empty (** missing_fld not empty in re-execution mode *) - | Missing_sigma_not_empty (** missing sigma not empty in re-execution mode *) + (** dereference error and description *) + | Dereference_error of deref_error * Localise.error_desc * Paths.Path.t option + + (** the abduction prover failed some checks *) + | Prover_checks of Prover.check list + + (** cannot combine actual pre with splitting and post *) + | Cannot_combine + + (** missing_fld not empty in re-execution mode *) + | Missing_fld_not_empty + + (** missing sigma not empty in re-execution mode *) + | Missing_sigma_not_empty type valid_res = { incons_pre_missing : bool; (** whether the actual pre is consistent with the missing part *) @@ -47,7 +56,8 @@ type valid_res = vr_incons_res : (Prop.normal Prop.t * Paths.Path.t) list; (** inconsistent result props *) } (** Result of (bi)-abduction on a single spec. - A result is invalid if no splitting was found, or if combine failed, or if we are in re - execution mode and the sigma + A result is invalid if no splitting was found, + or if combine failed, or if we are in re - execution mode and the sigma part of the splitting is not empty. A valid result contains the missing pi ans sigma, as well as the resulting props. *) type abduction_res = @@ -64,8 +74,10 @@ let d_splitting split = L.d_strln "MISSING ="; Prop.d_pi_sigma split.missing_pi split.missing_sigma; L.d_ln (); L.d_strln "FRAME FLD = "; Prop.d_sigma split.frame_fld; L.d_ln (); L.d_strln "MISSING FLD = "; Prop.d_sigma split.missing_fld; L.d_ln (); - if split.frame_typ <> [] then L.d_strln "FRAME TYP = "; Prover.d_typings split.frame_typ; L.d_ln (); - if split.missing_typ <> [] then L.d_strln "MISSING TYP = "; Prover.d_typings split.missing_typ; L.d_ln (); + if split.frame_typ <> [] + then L.d_strln "FRAME TYP = "; Prover.d_typings split.frame_typ; L.d_ln (); + if split.missing_typ <> [] + then L.d_strln "MISSING TYP = "; Prover.d_typings split.missing_typ; L.d_ln (); L.d_strln "------------------------------------------------------------"; L.d_decrease_indent 1 @@ -80,12 +92,14 @@ let spec_rename_vars pname spec = let prop_add_callee_suffix p = let f = function | Sil.Lvar pv -> - Sil.Lvar (Sil.pvar_to_callee pname pv) + Sil.Lvar (Pvar.to_callee pname pv) | e -> e in Prop.prop_expmap f p in let jprop_add_callee_suffix = function - | Specs.Jprop.Prop (n, p) -> Specs.Jprop.Prop (n, prop_add_callee_suffix p) - | Specs.Jprop.Joined (n, p, jp1, jp2) -> Specs.Jprop.Joined (n, prop_add_callee_suffix p, jp1, jp2) in + | Specs.Jprop.Prop (n, p) -> + Specs.Jprop.Prop (n, prop_add_callee_suffix p) + | Specs.Jprop.Joined (n, p, jp1, jp2) -> + Specs.Jprop.Joined (n, prop_add_callee_suffix p, jp1, jp2) in let fav = Sil.fav_new () in Specs.Jprop.fav_add fav spec.Specs.pre; IList.iter (fun (p, _) -> Prop.prop_fav_add fav p) spec.Specs.posts; @@ -98,8 +112,10 @@ let spec_rename_vars pname spec = let posts'' = IList.map (fun (p, path) -> (prop_add_callee_suffix p, path)) posts' in { Specs.pre = pre''; Specs.posts = posts''; Specs.visited = spec.Specs.visited } -(** Find and number the specs for [proc_name], after renaming their vars, and also return the parameters *) -let spec_find_rename trace_call (proc_name : Procname.t) : (int * Prop.exposed Specs.spec) list * Sil.pvar list = +(** Find and number the specs for [proc_name], + after renaming their vars, and also return the parameters *) +let spec_find_rename trace_call (proc_name : Procname.t) + : (int * Prop.exposed Specs.spec) list * Pvar.t list = try let count = ref 0 in let f spec = @@ -112,10 +128,13 @@ let spec_find_rename trace_call (proc_name : Procname.t) : (int * Prop.exposed S (Localise.verbatim_desc (Procname.to_string proc_name), __POS__)) end; let formal_parameters = - IList.map (fun (x, _) -> Sil.mk_pvar_callee x proc_name) formals in + IList.map (fun (x, _) -> Pvar.mk_callee x proc_name) formals in IList.map f specs, formal_parameters with Not_found -> begin - L.d_strln ("ERROR: found no entry for procedure " ^ Procname.to_string proc_name ^ ". Give up..."); + L.d_strln + ("ERROR: found no entry for procedure " ^ + Procname.to_string proc_name ^ + ". Give up..."); raise (Exceptions.Precondition_not_found (Localise.verbatim_desc (Procname.to_string proc_name), __POS__)) end @@ -124,7 +143,9 @@ let spec_find_rename trace_call (proc_name : Procname.t) : (int * Prop.exposed S change the instantiating substitution so that it returns primed vars, except for vars occurring in the missing part, where it returns footprint vars. *) -let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_fld missing_fld frame_typ missing_typ = +let process_splitting + actual_pre sub1 sub2 frame missing_pi missing_sigma + frame_fld missing_fld frame_typ missing_typ = let hpred_has_only_footprint_vars hpred = let fav = Sil.fav_new () in @@ -134,7 +155,10 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_ let sub1_inverse = let sub1_list = Sil.sub_to_list sub1 in let sub1_list' = IList.filter (function (_, Sil.Var _) -> true | _ -> false) sub1_list in - let sub1_inverse_list = IList.map (function (id, Sil.Var id') -> (id', Sil.Var id) | _ -> assert false) sub1_list' + let sub1_inverse_list = + IList.map + (function (id, Sil.Var id') -> (id', Sil.Var id) | _ -> assert false) + sub1_list' in Sil.sub_of_list_duplicates sub1_inverse_list in let fav_actual_pre = let fav_sub2 = (* vars which represent expansions of fields *) @@ -157,7 +181,8 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_ let map_var_to_pre_var_or_fresh id = match Sil.exp_sub sub1_inverse (Sil.Var id) with | Sil.Var id' -> - if Sil.fav_mem fav_actual_pre id' || Ident.is_path id' (** a path id represents a position in the pre *) + if Sil.fav_mem fav_actual_pre id' || Ident.is_path id' + (** a path id represents a position in the pre *) then Sil.Var id' else Sil.Var (Ident.create_fresh Ident.kprimed) | _ -> assert false in @@ -212,7 +237,7 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_ end else match hpred with | Sil.Hpointsto(Sil.Var _, _, _) -> true - | Sil.Hpointsto(Sil.Lvar pvar, _, _) -> Sil.pvar_is_global pvar + | Sil.Hpointsto(Sil.Lvar pvar, _, _) -> Pvar.is_global pvar | _ -> L.d_warning "Missing fields in complex pred: "; Sil.d_hpred hpred; L.d_ln (); false in @@ -227,13 +252,15 @@ let process_splitting actual_pre sub1 sub2 frame missing_pi missing_sigma frame_ frame_typ = norm_frame_typ; missing_typ = norm_missing_typ; } -(** Check whether an inst represents a dereference without null check, and return the line number and path position *) +(** Check whether an inst represents a dereference without null check, + and return the line number and path position *) let find_dereference_without_null_check_in_inst = function | Sil.Iupdate (Some true, _, n, pos) | Sil.Irearrange (Some true, _, n, pos) -> Some (n, pos) | _ -> None -(** Check whether a sexp contains a dereference without null check, and return the line number and path position *) +(** Check whether a sexp contains a dereference without null check, + and return the line number and path position *) let rec find_dereference_without_null_check_in_sexp = function | Sil.Eexp (_, inst) -> find_dereference_without_null_check_in_inst inst | Sil.Estruct (fsel, inst) -> @@ -265,7 +292,8 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = deref_str actual_pre spec_pre e (State.get_node ()) (State.get_loc ()) formal_params in (L.d_strln_color Red) "found error in dereference"; L.d_strln "spec_pre:"; Prop.d_prop spec_pre; L.d_ln(); - L.d_str "exp "; Sil.d_exp e; L.d_strln (" desc: " ^ (pp_to_string Localise.pp_error_desc error_desc)); + L.d_str "exp "; Sil.d_exp e; + L.d_strln (" desc: " ^ (pp_to_string Localise.pp_error_desc error_desc)); error_desc in let deref_no_null_check_pos = if Sil.exp_equal e_sub Sil.exp_zero then @@ -274,7 +302,9 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = | None -> None else None in if deref_no_null_check_pos != None - then (* only report a dereference null error if we know there was a dereference without null check *) + then + (* only report a dereference null error if we know + there was a dereference without null check *) match deref_no_null_check_pos with | Some pos -> Some (Deref_null pos, desc true (Localise.deref_str_null (Some callee_pname))) | None -> assert false @@ -283,7 +313,8 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = (* In that case it raise a dangling pointer dereferece *) if Prop.has_dangling_uninit_attribute spec_pre e then Some (Deref_undef_exp, desc false (Localise.deref_str_dangling (Some Sil.DAuninit)) ) - else if Sil.exp_equal e_sub Sil.exp_minus_one then Some (Deref_minusone, desc true (Localise.deref_str_dangling None)) + else if Sil.exp_equal e_sub Sil.exp_minus_one + then Some (Deref_minusone, desc true (Localise.deref_str_dangling None)) else match Prop.get_resource_attribute actual_pre e_sub with | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra)) -> Some (Deref_freed ra, desc true (Localise.deref_str_freed ra)) @@ -305,7 +336,8 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = | deref_err :: _ -> if !Config.angelic_execution then (* In angelic mode, prefer to report Deref_null over other kinds of deref errors. this - * makes sure we report a NULL_DEREFERENCE instead of a less interesting PRECONDITION_NOT_MET + * makes sure we report a NULL_DEREFERENCE instead of + a less interesting PRECONDITION_NOT_MET * whenever possible *) (* TOOD (t4893533): use this trick outside of angelic mode and in other parts of the code *) Some @@ -320,7 +352,8 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = let post_process_sigma (sigma: Sil.hpred list) loc : Sil.hpred list = let map_inst inst = Sil.inst_new_loc loc inst in - let do_hpred (_, _, hpred) = Sil.hpred_instmap map_inst hpred in (** update the location of instrumentations *) + let do_hpred (_, _, hpred) = Sil.hpred_instmap map_inst hpred in + (** update the location of instrumentations *) IList.map (fun hpred -> do_hpred (Prover.expand_hpred_pointer false hpred)) sigma (** check for interprocedural path errors in the post *) @@ -352,14 +385,16 @@ let post_process_post let atom_update_alloc_attribute = function | Sil.Aneq (e , Sil.Const (Sil.Cattribute (Sil.Aresource ra))) | Sil.Aneq (Sil.Const (Sil.Cattribute (Sil.Aresource ra)), e) - when not (ra.Sil.ra_kind = Sil.Rrelease && actual_pre_has_freed_attribute e) -> (* unless it was already freed before the call *) + when not (ra.Sil.ra_kind = Sil.Rrelease && actual_pre_has_freed_attribute e) -> + (* unless it was already freed before the call *) let vpath, _ = Errdesc.vpath_find post e in let ra' = { ra with Sil.ra_pname = callee_pname; Sil.ra_loc = loc; Sil.ra_vpath = vpath } in let c = Sil.Const (Sil.Cattribute (Sil.Aresource ra')) in Sil.Aneq (e, c) | a -> a in let prop' = Prop.replace_sigma (post_process_sigma (Prop.get_sigma post) loc) post in - let pi' = IList.map atom_update_alloc_attribute (Prop.get_pi prop') in (* update alloc attributes to refer to the caller *) + let pi' = IList.map atom_update_alloc_attribute (Prop.get_pi prop') in + (* update alloc attributes to refer to the caller *) let post' = Prop.replace_pi pi' prop' in check_path_errors_in_post caller_pname post' post_path; post', post_path @@ -401,7 +436,8 @@ and esel_star_fld esel1 esel2 = match esel1, esel2 with | 0 -> (e1, array_content_star se1 se2) :: esel_star_fld esel1' esel2' | n when n < 0 -> (e1, se1) :: esel_star_fld esel1' esel2 | _ -> - let se2' = sexp_set_inst Sil.Inone se2 in (* don't know whether element is read or written in fun call with array *) + let se2' = sexp_set_inst Sil.Inone se2 in + (* don't know whether element is read or written in fun call with array *) (e2, se2') :: esel_star_fld esel1 esel2') and sexp_star_fld se1 se2 : Sil.strexp = @@ -435,8 +471,10 @@ let texp_star texp1 texp2 = if ftal_sub instance_fields1 instance_fields2 then t2 else t1 | _ -> t1 in match texp1, texp2 with - | Sil.Sizeof (t1, st1), Sil.Sizeof (t2, st2) -> Sil.Sizeof (typ_star t1 t2, Sil.Subtype.join st1 st2) - | _ -> texp1 + | Sil.Sizeof (t1, st1), Sil.Sizeof (t2, st2) -> + Sil.Sizeof (typ_star t1 t2, Sil.Subtype.join st1 st2) + | _ -> + texp1 let hpred_star_fld (hpred1 : Sil.hpred) (hpred2 : Sil.hpred) : Sil.hpred = match hpred1, hpred2 with @@ -480,7 +518,8 @@ let hpred_star_typing (hpred1 : Sil.hpred) (_, te2) : Sil.hpred = | _ -> assert false (** Implementation of [*] between predicates and typings *) -let sigma_star_typ (sigma1 : Sil.hpred list) (typings2 : (Sil.exp * Sil.exp) list) : Sil.hpred list = +let sigma_star_typ + (sigma1 : Sil.hpred list) (typings2 : (Sil.exp * Sil.exp) list) : Sil.hpred list = let typing_lhs_compare (e1, _) (e2, _) = Sil.exp_compare e1 e2 in let sigma1 = IList.stable_sort hpred_lhs_compare sigma1 in let typings2 = IList.stable_sort typing_lhs_compare typings2 in @@ -502,8 +541,11 @@ let sigma_star_typ (sigma1 : Sil.hpred list) (typings2 : (Sil.exp * Sil.exp) lis L.d_ln (); raise (Prop.Cannot_star __POS__) -(** [prop_footprint_add_pi_sigma_starfld_sigma prop pi sigma missing_fld] extends the footprint of [prop] with [pi,sigma] and extends the fields of |-> with [missing_fld] *) -let prop_footprint_add_pi_sigma_starfld_sigma (prop : 'a Prop.t) pi_new sigma_new missing_fld missing_typ : Prop.normal Prop.t option = +(** [prop_footprint_add_pi_sigma_starfld_sigma prop pi sigma missing_fld] + extends the footprint of [prop] with [pi,sigma] + and extends the fields of |-> with [missing_fld] *) +let prop_footprint_add_pi_sigma_starfld_sigma + (prop : 'a Prop.t) pi_new sigma_new missing_fld missing_typ : Prop.normal Prop.t option = let rec extend_sigma current_sigma new_sigma = match new_sigma with | [] -> Some current_sigma | hpred :: new_sigma' -> @@ -512,7 +554,8 @@ let prop_footprint_add_pi_sigma_starfld_sigma (prop : 'a Prop.t) pi_new sigma_ne if Sil.fav_exists fav (fun id -> not (Ident.is_footprint id) && not !Config.angelic_execution) then begin - L.d_warning "found hpred with non-footprint variable, dropping the spec"; L.d_ln (); Sil.d_hpred hpred; L.d_ln (); + L.d_warning "found hpred with non-footprint variable, dropping the spec"; + L.d_ln (); Sil.d_hpred hpred; L.d_ln (); None end else extend_sigma (hpred :: current_sigma) new_sigma' in @@ -522,7 +565,8 @@ let prop_footprint_add_pi_sigma_starfld_sigma (prop : 'a Prop.t) pi_new sigma_ne let fav = Prop.pi_fav [a] in if Sil.fav_exists fav (fun id -> not (Ident.is_footprint id)) then begin - L.d_warning "dropping atom with non-footprint variable"; L.d_ln (); Sil.d_atom a; L.d_ln (); + L.d_warning "dropping atom with non-footprint variable"; + L.d_ln (); Sil.d_atom a; L.d_ln (); extend_pi current_pi new_pi' end else extend_pi (a :: current_pi) new_pi' in @@ -533,11 +577,13 @@ let prop_footprint_add_pi_sigma_starfld_sigma (prop : 'a Prop.t) pi_new sigma_ne let foot_sigma' = sigma_star_fld sigma' missing_fld in let foot_sigma'' = sigma_star_typ foot_sigma' missing_typ in let pi' = pi_new @ Prop.get_pi prop in - let prop' = Prop.replace_sigma_footprint foot_sigma'' (Prop.replace_pi_footprint foot_pi' prop) in + let prop' = + Prop.replace_sigma_footprint foot_sigma'' (Prop.replace_pi_footprint foot_pi' prop) in let prop'' = Prop.replace_pi pi' prop' in Some (Prop.normalize prop'') -(** Check if the attribute change is a mismatch between a kind of allocation and a different kind of deallocation *) +(** Check if the attribute change is a mismatch between a kind + of allocation and a different kind of deallocation *) let check_attr_dealloc_mismatch att_old att_new = match att_old, att_new with | Sil.Aresource ({ Sil.ra_kind = Sil.Racquire; Sil.ra_res = Sil.Rmemory mk_old } as ra_old), Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease; Sil.ra_res = Sil.Rmemory mk_new } as ra_new) @@ -548,7 +594,9 @@ let check_attr_dealloc_mismatch att_old att_new = match att_old, att_new with (** [prop_copy_footprint p1 p2] copies the footprint and pure part of [p1] into [p2] *) let prop_copy_footprint_pure p1 p2 = - let p2' = Prop.replace_sigma_footprint (Prop.get_sigma_footprint p1) (Prop.replace_pi_footprint (Prop.get_pi_footprint p1) p2) in + let p2' = + Prop.replace_sigma_footprint + (Prop.get_sigma_footprint p1) (Prop.replace_pi_footprint (Prop.get_pi_footprint p1) p2) in let pi2 = Prop.get_pi p2' in let pi2_attr, pi2_noattr = IList.partition Prop.atom_is_attribute pi2 in let res_noattr = Prop.replace_pi (Prop.get_pure p1 @ pi2_noattr) p2' in @@ -567,7 +615,7 @@ let exp_is_exn = function (** check if a prop is an exception *) let prop_is_exn pname prop = - let ret_pvar = Sil.Lvar (Sil.get_ret_pvar pname) in + let ret_pvar = Sil.Lvar (Pvar.get_ret_pvar pname) in let is_exn = function | Sil.Hpointsto (e1, Sil.Eexp(e2, _), _) when Sil.exp_equal e1 ret_pvar -> exp_is_exn e2 @@ -576,7 +624,7 @@ let prop_is_exn pname prop = (** when prop is an exception, return the exception name *) let prop_get_exn_name pname prop = - let ret_pvar = Sil.Lvar (Sil.get_ret_pvar pname) in + let ret_pvar = Sil.Lvar (Pvar.get_ret_pvar pname) in let exn_name = ref (Typename.Java.from_string "") in let find_exn_name e = let do_hpred = function @@ -588,7 +636,8 @@ let prop_get_exn_name pname prop = IList.iter do_hpred (Prop.get_sigma prop) in let find_ret () = let do_hpred = function - | Sil.Hpointsto (e1, Sil.Eexp(Sil.Const (Sil.Cexn e2), _), _) when Sil.exp_equal e1 ret_pvar -> + | Sil.Hpointsto (e1, Sil.Eexp(Sil.Const (Sil.Cexn e2), _), _) + when Sil.exp_equal e1 ret_pvar -> find_exn_name e2 | _ -> () in IList.iter do_hpred (Prop.get_sigma prop) in @@ -600,13 +649,13 @@ let lookup_custom_errors prop = let rec search_error = function | [] -> None | Sil.Hpointsto (Sil.Lvar var, Sil.Eexp (Sil.Const (Sil.Cstr error_str), _), _) :: _ - when Sil.pvar_equal var Sil.custom_error -> Some error_str + when Pvar.equal var Sil.custom_error -> Some error_str | _ :: tl -> search_error tl in search_error (Prop.get_sigma prop) (** set a prop to an exception sexp *) let prop_set_exn pname prop se_exn = - let ret_pvar = Sil.Lvar (Sil.get_ret_pvar pname) in + let ret_pvar = Sil.Lvar (Pvar.get_ret_pvar pname) in let map_hpred = function | Sil.Hpointsto (e, _, t) when Sil.exp_equal e ret_pvar -> Sil.Hpointsto(e, se_exn, t) @@ -648,11 +697,18 @@ let combine L.d_increase_indent 1; L.d_strln "New footprint:"; Prop.d_pi_sigma split.missing_pi split.missing_sigma; L.d_ln (); L.d_strln "Frame fld:"; Prop.d_sigma split.frame_fld; L.d_ln (); - if split.frame_typ <> [] then begin L.d_strln "Frame typ:"; Prover.d_typings split.frame_typ; L.d_ln () end; + if split.frame_typ <> [] + then + begin L.d_strln "Frame typ:"; + Prover.d_typings split.frame_typ; L.d_ln () end; L.d_strln "Missing fld:"; Prop.d_sigma split.missing_fld; L.d_ln (); - if split.missing_typ <> [] then begin L.d_strln "Missing typ:"; Prover.d_typings split.missing_typ; L.d_ln (); end; + if split.missing_typ <> [] + then + begin L.d_strln "Missing typ:"; + Prover.d_typings split.missing_typ; L.d_ln (); end; L.d_strln "Instantiated frame:"; Prop.d_sigma split.frame; L.d_ln (); - L.d_strln "Instantiated post:"; Propgraph.d_proplist Prop.prop_emp (IList.map fst instantiated_post); + L.d_strln "Instantiated post:"; + Propgraph.d_proplist Prop.prop_emp (IList.map fst instantiated_post); L.d_decrease_indent 1; L.d_ln (); let compute_result post_p = let post_p' = @@ -683,7 +739,7 @@ let combine let post_p3 = (** replace [result|callee] with an aux variable dedicated to this proc *) let callee_ret_pvar = - Sil.Lvar (Sil.pvar_to_callee callee_pname (Sil.get_ret_pvar callee_pname)) in + Sil.Lvar (Pvar.to_callee callee_pname (Pvar.get_ret_pvar callee_pname)) in match Prop.prop_iter_create post_p2 with | None -> post_p2 | Some iter -> @@ -729,7 +785,9 @@ let combine if IList.exists (fun (x, _) -> x = None) _results then (* at least one combine failed *) None else - let results = IList.map (function (Some x, path) -> (x, path) | (None, _) -> assert false) _results in + let results = + IList.map (function (Some x, path) -> (x, path) | (None, _) -> assert false) + _results in print_results actual_pre (IList.map fst results); Some results @@ -739,9 +797,9 @@ let add_tainting_attribute att pvar_param prop = (fun prop_acc hpred -> match hpred with | Sil.Hpointsto (Sil.Lvar pvar, (Sil.Eexp (rhs, _)), _) - when Sil.pvar_equal pvar pvar_param -> + when Pvar.equal pvar pvar_param -> L.d_strln ("TAINT ANALYSIS: setting taint/untaint attribute of parameter " ^ - (Sil.pvar_to_string pvar)); + (Pvar.to_string pvar)); Prop.add_or_replace_exp_attribute prop_acc rhs att | _ -> prop_acc) prop (Prop.get_sigma prop) @@ -760,7 +818,7 @@ let add_tainting_att_param_list prop param_nums formal_params att = (* Set Ataint attribute to list of parameters in a prop *) let add_param_taint proc_name formal_params prop param_nums = let formal_params' = IList.map - (fun (p, _) -> Sil.mk_pvar p proc_name) formal_params in + (fun (p, _) -> Pvar.mk p proc_name) formal_params in (* TODO: add taint_kind as part of specification format in taint.ml *) let taint_info = { Sil.taint_source = proc_name; taint_kind = Unknown; } in add_tainting_att_param_list prop param_nums formal_params' (Sil.Ataint taint_info) @@ -783,13 +841,23 @@ let mk_actual_precondition prop actual_params formal_params = | f:: fpars', a:: apars' -> (f, a) :: comb fpars' apars' | [], _ -> if apars != [] then - (let str = "more actual pars than formal pars in fun call (" ^ string_of_int (IList.length actual_params) ^ " vs " ^ string_of_int (IList.length formal_params) ^ ")" in - L.d_warning str; L.d_ln ()); + begin + let str = + "more actual pars than formal pars in fun call (" ^ + string_of_int (IList.length actual_params) ^ + " vs " ^ + string_of_int (IList.length formal_params) ^ + ")" in + L.d_warning str; L.d_ln () + end; [] | _:: _,[] -> raise (Exceptions.Wrong_argument_number __POS__) in comb formal_params actual_params in let mk_instantiation (formal_var, (actual_e, actual_t)) = - Prop.mk_ptsto (Sil.Lvar formal_var) (Sil.Eexp (actual_e, Sil.inst_actual_precondition)) (Sil.Sizeof (actual_t, Sil.Subtype.exact)) in + Prop.mk_ptsto + (Sil.Lvar formal_var) + (Sil.Eexp (actual_e, Sil.inst_actual_precondition)) + (Sil.Sizeof (actual_t, Sil.Subtype.exact)) in let instantiated_formals = IList.map mk_instantiation formals_actuals in let actual_pre = Prop.prop_sigma_star prop instantiated_formals in Prop.normalize actual_pre @@ -814,7 +882,7 @@ let mk_posts ret_ids prop callee_pname posts = let returns_null prop = IList.exists (function - | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (e, _), _) when Sil.pvar_is_return pvar -> + | Sil.Hpointsto (Sil.Lvar pvar, Sil.Eexp (e, _), _) when Pvar.is_return pvar -> Prover.check_equal (Prop.normalize prop) e Sil.exp_zero | _ -> false) (Prop.get_sigma prop) in @@ -909,7 +977,9 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub = IList.filter not_untaint_atom missing_pi_sub let class_cast_exn pname_opt texp1 texp2 exp ml_loc = - let desc = Errdesc.explain_class_cast_exception pname_opt texp1 texp2 exp (State.get_node ()) (State.get_loc ()) in + let desc = + Errdesc.explain_class_cast_exception + pname_opt texp1 texp2 exp (State.get_node ()) (State.get_loc ()) in Exceptions.Class_cast_exception (desc, ml_loc) let raise_cast_exception ml_loc pname_opt texp1 texp2 exp = @@ -946,7 +1016,9 @@ let exe_spec SymOp.pay(); (* pay one symop *) match Prover.check_implication_for_footprint caller_pname tenv actual_pre spec_pre with | Prover.ImplFail checks -> Invalid_res (Prover_checks checks) - | Prover.ImplOK (checks, sub1, sub2, frame, missing_pi, missing_sigma, frame_fld, missing_fld, frame_typ, missing_typ) -> + | Prover.ImplOK + (checks, sub1, sub2, frame, missing_pi, missing_sigma, + frame_fld, missing_fld, frame_typ, missing_typ) -> let log_check_exn check = let exn = get_check_exn check callee_pname loc __POS__ in Reporting.log_warning caller_pname exn in @@ -955,7 +1027,9 @@ let exe_spec if !Config.taint_analysis then do_taint_check caller_pname callee_pname actual_pre missing_pi sub2 else missing_pi in - process_splitting actual_pre sub1 sub2 frame missing_pi' missing_sigma frame_fld missing_fld frame_typ missing_typ in + process_splitting + actual_pre sub1 sub2 frame missing_pi' missing_sigma + frame_fld missing_fld frame_typ missing_typ in let report_valid_res split = match combine ret_ids posts @@ -963,8 +1037,10 @@ let exe_spec caller_pdesc callee_pname loc with | None -> Invalid_res Cannot_combine | Some results -> - (* After combining we check that we have not added a points-to of initialized variables.*) - check_uninitialize_dangling_deref callee_pname actual_pre split.sub formal_params results; + (* After combining we check that we have not added + a points-to of initialized variables.*) + check_uninitialize_dangling_deref + callee_pname actual_pre split.sub formal_params results; let inconsistent_results, consistent_results = IList.partition (fun (p, _) -> Prover.check_inconsistency p) results in let incons_pre_missing = inconsistent_actualpre_missing actual_pre (Some split) in @@ -1020,7 +1096,8 @@ let remove_constant_string_class prop = let prop' = Prop.replace_sigma_footprint sigmafp (Prop.replace_sigma sigma prop) in Prop.normalize prop' -(** existentially quantify the path identifier generated by the prover to keep track of expansions of lhs paths +(** existentially quantify the path identifier generated + by the prover to keep track of expansions of lhs paths and remove pointsto's whose lhs is a constant string *) let quantify_path_idents_remove_constant_strings (prop: Prop.normal Prop.t) : Prop.normal Prop.t = let fav = Prop.prop_fav prop in @@ -1063,14 +1140,17 @@ let exe_call_postprocess ret_ids trace_call callee_pname loc results = let res_with_path_idents = if !Config.footprint then begin - if valid_res_cons_pre_missing == [] then (* no valid results where actual pre and missing are consistent *) + if valid_res_cons_pre_missing == [] then + (* no valid results where actual pre and missing are consistent *) begin if deref_errors <> [] then (* dereference error detected *) let extend_path path_opt path_pos_opt = match path_opt with | None -> () | Some path_post -> let old_path, _ = State.get_path () in - let new_path = Paths.Path.add_call (include_subtrace callee_pname) old_path callee_pname path_post in + let new_path = + Paths.Path.add_call + (include_subtrace callee_pname) old_path callee_pname path_post in State.set_path new_path path_pos_opt in match IList.hd deref_errors with | Dereference_error (Deref_minusone, desc, path_opt) -> @@ -1099,7 +1179,10 @@ let exe_call_postprocess ret_ids trace_call callee_pname loc results = trace_call Specs.CallStats.CR_not_met; extend_path path_opt (Some pos); raise (Exceptions.Skip_pointer_dereference (desc, __POS__)) - | Prover_checks _ | Cannot_combine | Missing_sigma_not_empty | Missing_fld_not_empty -> + | Prover_checks _ + | Cannot_combine + | Missing_sigma_not_empty + | Missing_fld_not_empty -> trace_call Specs.CallStats.CR_not_met; assert false else (* no dereference error detected *) @@ -1120,12 +1203,18 @@ let exe_call_postprocess ret_ids trace_call callee_pname loc results = else (* combine the valid results, and store diverging states *) let process_valid_res vr = let save_diverging_states () = - if not vr.incons_pre_missing && vr.vr_cons_res = [] then (* no consistent results on one spec: divergence *) - let incons_res = IList.map (fun (p, path) -> (prop_pure_to_footprint p, path)) vr.vr_incons_res in + if not vr.incons_pre_missing && vr.vr_cons_res = [] + then (* no consistent results on one spec: divergence *) + let incons_res = + IList.map + (fun (p, path) -> (prop_pure_to_footprint p, path)) + vr.vr_incons_res in State.add_diverging_states (Paths.PathSet.from_renamed_list incons_res) in save_diverging_states (); vr.vr_cons_res in - IList.map (fun (p, path) -> (prop_pure_to_footprint p, path)) (IList.flatten (IList.map process_valid_res valid_res)) + IList.map + (fun (p, path) -> (prop_pure_to_footprint p, path)) + (IList.flatten (IList.map process_valid_res valid_res)) end else if valid_res_no_miss_pi != [] then IList.flatten (IList.map (fun vr -> vr.vr_cons_res) valid_res_no_miss_pi) @@ -1135,7 +1224,9 @@ let exe_call_postprocess ret_ids trace_call callee_pname loc results = begin L.d_strln "Missing pure facts for the function call:"; IList.iter print_pi (IList.map (fun vr -> vr.vr_pi) valid_res_miss_pi); - match Prover.find_minimum_pure_cover (IList.map (fun vr -> (vr.vr_pi, vr.vr_cons_res)) valid_res_miss_pi) with + match + Prover.find_minimum_pure_cover + (IList.map (fun vr -> (vr.vr_pi, vr.vr_cons_res)) valid_res_miss_pi) with | None -> trace_call Specs.CallStats.CR_not_met; raise (Exceptions.Precondition_not_met (call_desc None, __POS__)) @@ -1179,7 +1270,11 @@ let exe_function_call tenv ret_ids caller_pdesc callee_pname loc actual_params p summary.Specs.stats.Specs.call_stats callee_pname loc res !Config.footprint in let spec_list, formal_params = spec_find_rename trace_call callee_pname in let nspecs = IList.length spec_list in - L.d_strln ("Found " ^ string_of_int nspecs ^ " specs for function " ^ Procname.to_string callee_pname); + L.d_strln + ("Found " ^ + string_of_int nspecs ^ + " specs for function " ^ + Procname.to_string callee_pname); L.d_strln ("START EXECUTING SPECS FOR " ^ Procname.to_string callee_pname ^ " from state"); Prop.d_prop prop; L.d_ln (); let exe_one_spec (n, spec) = diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 25a655cbc..9265fc0a4 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -8,9 +8,9 @@ *) module PvarSet = PrettyPrintable.MakePPSet(struct - type t = Sil.pvar - let compare = Sil.pvar_compare - let pp_element = (Sil.pp_pvar pe_text) + type t = Pvar.t + let compare = Pvar.compare + let pp_element = (Pvar.pp pe_text) end) module Domain = AbstractDomain.FiniteSetDomain(PvarSet) diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index de9cc6c31..f0d4bcdac 100644 --- a/infer/src/checkers/annotations.ml +++ b/infer/src/checkers/annotations.ml @@ -258,7 +258,7 @@ let annotated_signature_is_anonymous_inner_class_wrapper ann_sig proc_name = let param_is_nullable pvar ann_sig = IList.exists (fun (param, annot, _) -> - Mangled.equal param (Sil.pvar_get_name pvar) && ia_is_nullable annot) + Mangled.equal param (Pvar.get_name pvar) && ia_is_nullable annot) ann_sig.params (** Pretty print a method signature with annotations. *) diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index 353057f1b..291f52897 100644 --- a/infer/src/checkers/annotations.mli +++ b/infer/src/checkers/annotations.mli @@ -31,7 +31,7 @@ type annotated_signature = val annotated_signature_is_anonymous_inner_class_wrapper : annotated_signature -> Procname.t -> bool (** Check if the given parameter has a Nullable annotation in the given signature *) -val param_is_nullable : Sil.pvar -> annotated_signature -> bool +val param_is_nullable : Pvar.t -> annotated_signature -> bool (** Mark the annotated signature with the given annotation map. *) val annotated_signature_mark : diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml index e89691e3d..97839c931 100644 --- a/infer/src/checkers/checkTraceCallSequence.ml +++ b/infer/src/checkers/checkTraceCallSequence.ml @@ -230,8 +230,8 @@ module BooleanVars = struct (** Check if the expression exp is one of the listed boolean variables. *) let exp_boolean_var exp = match exp with - | Sil.Lvar pvar when Sil.pvar_is_local pvar -> - let name = Mangled.to_string (Sil.pvar_get_name pvar) in + | Sil.Lvar pvar when Pvar.is_local pvar -> + let name = Mangled.to_string (Pvar.get_name pvar) in if IList.mem string_equal name boolean_variables then Some name else None diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index 782fde38d..d8d137e83 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -323,7 +323,7 @@ let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } = IList.map fst class_formals) in let equal_formal_param exp formal_name = match exp with | Sil.Lvar pvar -> - let name = Sil.pvar_get_name pvar in + let name = Pvar.get_name pvar in Mangled.equal name formal_name | _ -> false in @@ -424,7 +424,7 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p Some proc_desc' -> let is_return_instr = function | Sil.Set (Sil.Lvar p, _, _, _) - when Sil.pvar_equal p (Cfg.Procdesc.get_ret_var proc_desc') -> true + when Pvar.equal p (Cfg.Procdesc.get_ret_var proc_desc') -> true | _ -> false in (match reverse_find_instr is_return_instr (Cfg.Procdesc.get_exit_node proc_desc') with | Some (Sil.Set (_, _, Sil.Const (Sil.Cclass n), _)) -> Ident.name_to_string n diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index 06168a18c..7758391f3 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/infer/src/checkers/copyPropagation.ml @@ -11,11 +11,11 @@ module F = Format module L = Logging type var = - | ProgramVar of Sil.pvar + | ProgramVar of Pvar.t | LogicalVar of Ident.t let var_compare v1 v2 = match v1, v2 with - | ProgramVar pv1, ProgramVar pv2 -> Sil.pvar_compare pv1 pv2 + | ProgramVar pv1, ProgramVar pv2 -> Pvar.compare pv1 pv2 | LogicalVar sv1, LogicalVar sv2 -> Ident.compare sv1 sv2 | ProgramVar _, _ -> 1 | LogicalVar _, _ -> -1 @@ -24,8 +24,10 @@ let var_equal v1 v2 = var_compare v1 v2 = 0 let pp_var fmt = function - | ProgramVar pv -> (Sil.pp_pvar pe_text) fmt pv - | LogicalVar id -> (Ident.pp pe_text) fmt id + | ProgramVar pv -> + (Pvar.pp pe_text) fmt pv + | LogicalVar id -> + (Ident.pp pe_text) fmt id module Domain = struct module VarMap = PrettyPrintable.MakePPMap(struct @@ -102,12 +104,12 @@ module TransferFunctions = struct | Sil.Letderef (lhs_id, Sil.Var rhs_id, _, _) -> (* note: logical vars are SSA, don't need to worry about overwriting existing bindings *) Domain.gen (LogicalVar lhs_id) (LogicalVar rhs_id) astate - | Sil.Letderef (lhs_id, Sil.Lvar rhs_pvar, _, _) when not (Sil.pvar_is_global rhs_pvar) -> + | Sil.Letderef (lhs_id, Sil.Lvar rhs_pvar, _, _) when not (Pvar.is_global rhs_pvar) -> Domain.gen (LogicalVar lhs_id) (ProgramVar rhs_pvar) astate - | Sil.Set (Sil.Lvar lhs_pvar, _, Sil.Var rhs_id, _) when not (Sil.pvar_is_global lhs_pvar) -> + | Sil.Set (Sil.Lvar lhs_pvar, _, Sil.Var rhs_id, _) when not (Pvar.is_global lhs_pvar) -> Domain.kill_then_gen (ProgramVar lhs_pvar) (LogicalVar rhs_id) astate | Sil.Set (Sil.Lvar lhs_pvar, _, Sil.Lvar rhs_pvar, _) - when not (Sil.pvar_is_global lhs_pvar || Sil.pvar_is_global rhs_pvar) -> + when not (Pvar.is_global lhs_pvar || Pvar.is_global rhs_pvar) -> Domain.kill_then_gen (ProgramVar lhs_pvar) (ProgramVar rhs_pvar) astate | Sil.Letderef (lhs_id, _, _, _) -> (* non-copy assignment (or assignment to global); can only kill *) diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml index 1c40cf4d6..aeb6c174e 100644 --- a/infer/src/checkers/dataflow.ml +++ b/infer/src/checkers/dataflow.ml @@ -41,12 +41,12 @@ end (** Determine if the node can throw an exception. *) let node_throws node (proc_throws : Procname.t -> throws) : throws = let instr_throws instr = - let pvar_is_return pvar = + let is_return pvar = let pdesc = Cfg.Node.get_proc_desc node in let ret_pvar = Cfg.Procdesc.get_ret_var pdesc in - Sil.pvar_equal pvar ret_pvar in + Pvar.equal pvar ret_pvar in match instr with - | Sil.Set (Sil.Lvar pvar, _, Sil.Const (Sil.Cexn _), _) when pvar_is_return pvar -> + | Sil.Set (Sil.Lvar pvar, _, Sil.Const (Sil.Cexn _), _) when is_return pvar -> (* assignment to return variable is an artifact of a throw instruction *) Throws | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, _, _) diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index dc39d2538..6550da50d 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/infer/src/checkers/patternMatch.ml @@ -138,13 +138,13 @@ let java_get_const_type_name let get_vararg_type_names (call_node: Cfg.Node.t) - (ivar: Sil.pvar): string list = + (ivar: Pvar.t): string list = (* Is this the node creating ivar? *) let rec initializes_array instrs = match instrs with | Sil.Call ([t1], Sil.Const (Sil.Cfun pn), _, _, _):: Sil.Set (Sil.Lvar iv, _, Sil.Var t2, _):: is -> - (Sil.pvar_equal ivar iv && Ident.equal t1 t2 && + (Pvar.equal ivar iv && Ident.equal t1 t2 && Procname.equal pn (Procname.from_string_c_fun "__new_array")) || initializes_array is | _:: is -> initializes_array is @@ -172,7 +172,7 @@ let get_vararg_type_names let rec array_nvar instrs = match instrs with | Sil.Letderef (nv, Sil.Lvar iv, _, _):: _ - when Sil.pvar_equal iv ivar -> + when Pvar.equal iv ivar -> added_nvar nv instrs | _:: is -> array_nvar is | _ -> None in diff --git a/infer/src/checkers/patternMatch.mli b/infer/src/checkers/patternMatch.mli index b1138f9e2..ddc343ebe 100644 --- a/infer/src/checkers/patternMatch.mli +++ b/infer/src/checkers/patternMatch.mli @@ -33,7 +33,7 @@ val get_this_type : ProcAttributes.t -> Sil.typ option val get_type_name : Sil.typ -> string (** Get the type names of a variable argument *) -val get_vararg_type_names : Cfg.Node.t -> Sil.pvar -> string list +val get_vararg_type_names : Cfg.Node.t -> Pvar.t -> string list val has_formal_method_argument_type_names : Cfg.Procdesc.t -> Procname.java -> string list -> bool @@ -54,7 +54,7 @@ val is_direct_subtype_of : Sil.typ -> Typename.t -> bool val java_get_const_type_name : Sil.const -> string (** Get the values of a vararg parameter given the pvar used to assign the elements. *) -val java_get_vararg_values : Cfg.Node.t -> Sil.pvar -> Idenv.t -> Sil.exp list +val java_get_vararg_values : Cfg.Node.t -> Pvar.t -> Idenv.t -> Sil.exp list val java_proc_name_with_class_method : Procname.java -> string -> string -> bool diff --git a/infer/src/clang/cContext.ml b/infer/src/clang/cContext.ml index 72d5905cd..e8ec78010 100644 --- a/infer/src/clang/cContext.ml +++ b/infer/src/clang/cContext.ml @@ -30,7 +30,7 @@ type t = return_param_typ : Sil.typ option; is_callee_expression : bool; outer_context : t option; (* in case of objc blocks, the context of the method containing the block *) - mutable blocks_static_vars : ((Sil.pvar * Sil.typ) list) Procname.Map.t; + mutable blocks_static_vars : ((Pvar.t * Sil.typ) list) Procname.Map.t; } let create_context tenv cg cfg procdesc curr_class return_param_typ is_objc_method context_opt = @@ -127,12 +127,12 @@ let create_curr_class tenv class_name ck = let add_block_static_var context block_name static_var_typ = match context.outer_context, static_var_typ with - | Some outer_context, (static_var, _) when Sil.pvar_is_global static_var -> + | Some outer_context, (static_var, _) when Pvar.is_global static_var -> (let new_static_vars, duplicate = try let static_vars = Procname.Map.find block_name outer_context.blocks_static_vars in if IList.mem ( - fun (var1, _) (var2, _) -> Sil.pvar_equal var1 var2 + fun (var1, _) (var2, _) -> Pvar.equal var1 var2 ) static_var_typ static_vars then static_vars, true else diff --git a/infer/src/clang/cContext.mli b/infer/src/clang/cContext.mli index b7674082c..e10a37149 100644 --- a/infer/src/clang/cContext.mli +++ b/infer/src/clang/cContext.mli @@ -28,7 +28,7 @@ type t = return_param_typ : Sil.typ option; is_callee_expression : bool; outer_context : t option; (* in case of objc blocks, the context of the method containing the block *) - mutable blocks_static_vars : ((Sil.pvar * Sil.typ) list) Procname.Map.t; + mutable blocks_static_vars : ((Pvar.t * Sil.typ) list) Procname.Map.t; } val get_procdesc : t -> Cfg.Procdesc.t @@ -58,9 +58,9 @@ val create_context : Tenv.t -> Cg.t -> Cfg.cfg -> Cfg.Procdesc.t -> val create_curr_class : Tenv.t -> string -> Csu.class_kind -> curr_class -val add_block_static_var : t -> Procname.t -> (Sil.pvar * Sil.typ) -> unit +val add_block_static_var : t -> Procname.t -> (Pvar.t * Sil.typ) -> unit -val static_vars_for_block : t -> Procname.t -> (Sil.pvar * Sil.typ) list +val static_vars_for_block : t -> Procname.t -> (Pvar.t * Sil.typ) list val is_objc_instance : t -> bool diff --git a/infer/src/clang/cFrontend_checkers.ml b/infer/src/clang/cFrontend_checkers.ml index b4e5586aa..9093f941d 100644 --- a/infer/src/clang/cFrontend_checkers.ml +++ b/infer/src/clang/cFrontend_checkers.ml @@ -140,7 +140,7 @@ let captured_cxx_ref_in_objc_block_warning stmt_info captured_vars = | _ -> false in let capt_refs = IList.filter is_cxx_ref captured_vars in let pvar_descs = - IList.fold_left (fun s (v, _) -> s ^ " '" ^ (Sil.pvar_to_string v) ^ "' ") "" capt_refs in + IList.fold_left (fun s (v, _) -> s ^ " '" ^ (Pvar.to_string v) ^ "' ") "" capt_refs in (* Fire if the list of captured references is not empty *) let condition = IList.length capt_refs > 0 in if condition then diff --git a/infer/src/clang/cFrontend_checkers.mli b/infer/src/clang/cFrontend_checkers.mli index 424896ea3..1b52d1685 100644 --- a/infer/src/clang/cFrontend_checkers.mli +++ b/infer/src/clang/cFrontend_checkers.mli @@ -28,7 +28,7 @@ val direct_atomic_property_access_warning : (* CXX_REFERENCE_CAPTURED_IN_OBJC_BLOCK: C++ references should not be captured in blocks. *) -val captured_cxx_ref_in_objc_block_warning : Clang_ast_t.stmt_info -> (Sil.pvar * Sil.typ) list -> +val captured_cxx_ref_in_objc_block_warning : Clang_ast_t.stmt_info -> (Pvar.t * Sil.typ) list -> warning_desc option (* REGISTERED_OBSERVER_BEING_DEALLOCATED: an object is registered in a notification center diff --git a/infer/src/clang/cFrontend_utils.ml b/infer/src/clang/cFrontend_utils.ml index 12814e7d7..f3c60641f 100644 --- a/infer/src/clang/cFrontend_utils.ml +++ b/infer/src/clang/cFrontend_utils.ml @@ -433,7 +433,7 @@ struct let eq (m1, t1) (m2, t2) = (Mangled.equal m1 m2) && (Sil.typ_equal t1 t2) in append_no_duplicates eq list1 list2 - let append_no_duplicated_pvars list1 list2 = + let append_no_duplicateds list1 list2 = let eq (e1, t1) (e2, t2) = (Sil.exp_equal e1 e2) && (Sil.typ_equal t1 t2) in append_no_duplicates eq list1 list2 @@ -498,7 +498,7 @@ struct (* It does not update the global block_counter *) let get_next_block_pvar defining_proc = let name = block_procname_with_index defining_proc (!block_counter +1) in - Sil.mk_pvar (Mangled.from_string (CFrontend_config.temp_var^"_"^name)) defining_proc + Pvar.mk (Mangled.from_string (CFrontend_config.temp_var^"_"^name)) defining_proc (* Reset block counter *) let reset_block_counter () = @@ -599,8 +599,8 @@ struct if var_decl_info.Clang_ast_t.vdi_is_static_local then Mangled.from_string ((Procname.to_string outer_procname) ^ "_" ^ name_string) else simple_name in - Sil.mk_pvar_global global_mangled_name - else if not should_be_mangled then Sil.mk_pvar simple_name procname + Pvar.mk_global global_mangled_name + else if not should_be_mangled then Pvar.mk simple_name procname else let type_name = Ast_utils.string_of_type_ptr type_ptr in let start_location = fst decl_info.Clang_ast_t.di_source_range in @@ -608,8 +608,8 @@ struct let line_str = match line_opt with | Some line -> string_of_int line | None -> "" in let mangled = string_crc_hex32 (type_name ^ line_str) in let mangled_name = Mangled.mangled name_string mangled in - Sil.mk_pvar mangled_name procname - | None -> Sil.mk_pvar (Mangled.from_string name_string) procname + Pvar.mk mangled_name procname + | None -> Pvar.mk (Mangled.from_string name_string) procname let is_cpp_translation language = language = CFrontend_config.CPP || language = CFrontend_config.OBJCPP diff --git a/infer/src/clang/cFrontend_utils.mli b/infer/src/clang/cFrontend_utils.mli index 7f3e44b00..7aa3cc1ea 100644 --- a/infer/src/clang/cFrontend_utils.mli +++ b/infer/src/clang/cFrontend_utils.mli @@ -48,11 +48,14 @@ sig val property_name : Clang_ast_t.obj_c_property_impl_decl_info -> Clang_ast_t.named_decl_info - val property_attribute_compare : Clang_ast_t.property_attribute -> Clang_ast_t.property_attribute -> int + val property_attribute_compare : + Clang_ast_t.property_attribute -> Clang_ast_t.property_attribute -> int - val generated_ivar_name : Clang_ast_t.named_decl_info -> Clang_ast_t.named_decl_info + val generated_ivar_name : + Clang_ast_t.named_decl_info -> Clang_ast_t.named_decl_info - val property_attribute_eq : Clang_ast_t.property_attribute -> Clang_ast_t.property_attribute -> bool + val property_attribute_eq : + Clang_ast_t.property_attribute -> Clang_ast_t.property_attribute -> bool val get_memory_management_attributes : unit -> Clang_ast_t.property_attribute list @@ -133,23 +136,29 @@ sig val string_from_list : string list -> string val append_no_duplicates_fields : (Ident.fieldname * Sil.typ * Sil.item_annotation) list -> - (Ident.fieldname * Sil.typ * Sil.item_annotation) list -> (Ident.fieldname * Sil.typ * Sil.item_annotation) list + (Ident.fieldname * Sil.typ * Sil.item_annotation) list -> + (Ident.fieldname * Sil.typ * Sil.item_annotation) list val append_no_duplicates_csu : Typename.t list -> Typename.t list -> Typename.t list val append_no_duplicates_methods : Procname.t list -> Procname.t list -> Procname.t list - val append_no_duplicated_vars : (Mangled.t * Sil.typ) list -> (Mangled.t * Sil.typ) list -> (Mangled.t * Sil.typ) list + val append_no_duplicated_vars : + (Mangled.t * Sil.typ) list -> (Mangled.t * Sil.typ) list -> (Mangled.t * Sil.typ) list - val append_no_duplicated_pvars : (Sil.exp * Sil.typ) list -> (Sil.exp * Sil.typ) list -> (Sil.exp * Sil.typ) list + val append_no_duplicateds : + (Sil.exp * Sil.typ) list -> (Sil.exp * Sil.typ) list -> (Sil.exp * Sil.typ) list - val sort_fields : (Ident.fieldname * Sil.typ * Sil.item_annotation) list -> (Ident.fieldname * Sil.typ * Sil.item_annotation) list + val sort_fields : + (Ident.fieldname * Sil.typ * Sil.item_annotation) list -> + (Ident.fieldname * Sil.typ * Sil.item_annotation) list val sort_fields_tenv : Tenv.t -> unit val collect_list_tuples : ('a list * 'b list * 'c list * 'd list * 'e list) list -> - 'a list * 'b list * 'c list * 'd list * 'e list -> 'a list * 'b list * 'c list * 'd list * 'e list + 'a list * 'b list * 'c list * 'd list * 'e list -> + 'a list * 'b list * 'c list * 'd list * 'e list val swap_elements_list : 'a list -> 'a list @@ -157,11 +166,12 @@ sig val mk_fresh_block_procname : Procname.t -> Procname.t - val get_next_block_pvar : Procname.t -> Sil.pvar + val get_next_block_pvar : Procname.t -> Pvar.t val reset_block_counter : unit -> unit - val mk_function_decl_info_from_block : Clang_ast_t.block_decl_info -> Clang_ast_t.function_decl_info + val mk_function_decl_info_from_block : + Clang_ast_t.block_decl_info -> Clang_ast_t.function_decl_info val zip: 'a list -> 'b list -> ('a * 'b) list @@ -181,7 +191,7 @@ sig val get_var_name_string : Clang_ast_t.named_decl_info -> Clang_ast_t.var_decl_info -> string val mk_sil_var : Clang_ast_t.named_decl_info -> var_info option -> Procname.t -> Procname.t -> - Sil.pvar + Pvar.t val is_cpp_translation : CFrontend_config.lang -> bool end diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 60c799c46..6135abd78 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -368,7 +368,7 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = let create_new_procdesc () = let formals = get_formal_parameters tenv ms in let captured_str = - IList.map (fun (var, t) -> (Mangled.from_string (Sil.pvar_to_string var), t)) captured in + IList.map (fun (var, t) -> (Mangled.from_string (Pvar.to_string var), t)) captured in (* Captured variables for blocks are treated as parameters *) let formals = captured_str @ formals in let source_range = CMethod_signature.ms_get_loc ms in @@ -376,7 +376,7 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = let loc_start = CLocation.get_sil_location_from_range source_range true in let loc_exit = CLocation.get_sil_location_from_range source_range false in let ret_type = get_return_type tenv ms in - let captured' = IList.map (fun (var, t) -> (Sil.pvar_get_name var, t)) captured in + let captured' = IList.map (fun (var, t) -> (Pvar.get_name var, t)) captured in let procdesc = let proc_attributes = { (ProcAttributes.default proc_name Config.C_CPP) with diff --git a/infer/src/clang/cMethod_trans.mli b/infer/src/clang/cMethod_trans.mli index cce66e997..7ca08901f 100644 --- a/infer/src/clang/cMethod_trans.mli +++ b/infer/src/clang/cMethod_trans.mli @@ -23,7 +23,7 @@ type method_call_type = val should_add_return_param : Sil.typ -> is_objc_method:bool -> bool val create_local_procdesc : Cfg.cfg -> Tenv.t -> CMethod_signature.method_signature -> - Clang_ast_t.stmt list -> (Sil.pvar * Sil.typ) list -> bool -> bool + Clang_ast_t.stmt list -> (Pvar.t * Sil.typ) list -> bool -> bool val create_external_procdesc : Cfg.cfg -> Procname.t -> bool -> (Sil.typ * Sil.typ list) option -> unit diff --git a/infer/src/clang/cModule_type.ml b/infer/src/clang/cModule_type.ml index 6f08402ef..c30c6423e 100644 --- a/infer/src/clang/cModule_type.ml +++ b/infer/src/clang/cModule_type.ml @@ -7,7 +7,7 @@ * of patent rights can be found in the PATENTS file in the same directory. *) -type block_data = CContext.t * Clang_ast_t.type_ptr * Procname.t * (Sil.pvar * Sil.typ) list +type block_data = CContext.t * Clang_ast_t.type_ptr * Procname.t * (Pvar.t * Sil.typ) list type instr_type = [ | `ClangStmt of Clang_ast_t.stmt diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 7f395c840..63cf61ab2 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -105,13 +105,14 @@ struct (* An object of this class has type:*) (* name_of_block |-> {capture_var1:typ_of_capture_var1,... capture_varn:typ_of_capture_varn} *) (* It allocates one element and sets its fields with the current values of the *) - (* captured variables. This allocated instance is used to detect retain cycles involving the block.*) + (* captured variables. This allocated instance + is used to detect retain cycles involving the block.*) let allocate_block trans_state block_name captured_vars loc = let tenv = trans_state.context.CContext.tenv in let procdesc = trans_state.context.CContext.procdesc in let procname = Cfg.Procdesc.get_proc_name procdesc in let mk_field_from_captured_var (var, typ) = - let vname = Sil.pvar_get_name var in + let vname = Pvar.get_name var in let qual_name = Ast_utils.make_qual_name_decl [block_name] (Mangled.to_string vname) in let fname = General_utils.mk_class_field_name qual_name in let item_annot = Sil.item_annotation_empty in @@ -134,11 +135,13 @@ struct let block_type = Sil.Tstruct block_struct_typ in let block_name = Typename.TN_csu (Csu.Class Csu.Objc, mblock) in Tenv.add tenv block_name block_struct_typ; - let trans_res = CTrans_utils.alloc_trans trans_state loc (Ast_expressions.dummy_stmt_info ()) block_type true in + let trans_res = + CTrans_utils.alloc_trans + trans_state loc (Ast_expressions.dummy_stmt_info ()) block_type true in let id_block = match trans_res.exps with | [(Sil.Var id, _)] -> id | _ -> assert false in - let block_var = Sil.mk_pvar mblock procname in + let block_var = Pvar.mk mblock procname in let declare_block_local = Sil.Declare_locals ([(block_var, Sil.Tptr (block_type, Sil.Pk_pointer))], loc) in (* Adds Nullify of the temp block variable in the predecessors of the exit node. *) @@ -146,9 +149,12 @@ struct let block_nullify_instr = if pred_exit = [] then [Sil.Nullify (block_var, loc, true)] - else (IList.iter (fun n -> let loc = Cfg.Node.get_loc n in - Cfg.Node.append_instrs_temps n [Sil.Nullify(block_var, loc, true)] []) pred_exit; - []) in + else + (IList.iter + (fun n -> let loc = Cfg.Node.get_loc n in + Cfg.Node.append_instrs_temps n [Sil.Nullify(block_var, loc, true)] []) + pred_exit; + []) in let set_instr = Sil.Set (Sil.Lvar block_var, block_type, Sil.Var id_block, loc) in let create_field_exp (var, typ) = let id = Ident.create_fresh Ident.knormal in @@ -157,7 +163,11 @@ struct let fields_ids = IList.combine fields ids in let set_fields = IList.map (fun ((f, t, _), id) -> Sil.Set (Sil.Lfield (Sil.Var id_block, f, block_type), t, Sil.Var id, loc)) fields_ids in - (declare_block_local :: trans_res.instrs) @ [set_instr] @ captured_instrs @ set_fields @ block_nullify_instr, + (declare_block_local :: trans_res.instrs) @ + [set_instr] @ + captured_instrs @ + set_fields @ + block_nullify_instr, id_block :: ids (* From a list of expression extract blocks from tuples and *) @@ -168,7 +178,7 @@ struct let make_function_name typ bn = let bn'= Procname.to_string bn in let bn''= Mangled.from_string bn' in - let block = Sil.Lvar (Sil.mk_pvar bn'' procname) in + let block = Sil.Lvar (Pvar.mk bn'' procname) in let id = Ident.create_fresh Ident.knormal in ids := id :: !ids; insts := Sil.Letderef (id, block, typ, loc) :: !insts; @@ -201,15 +211,19 @@ struct f { trans_state with priority = Free } e) else f trans_state e - (* This is the standard way of dealing with self:Class or a call [a class]. We translate it as sizeof() *) - (* The only time when we want to translate those expressions differently is when they are the first argument of *) - (* method calls. In that case they are not translated as expressions, but we take the type and create a static *) + (* This is the standard way of dealing with self:Class or a call [a class]. + We translate it as sizeof() *) + (* The only time when we want to translate those expressions differently + is when they are the first argument of *) + (* method calls. In that case they are not translated as expressions, + but we take the type and create a static *) (* method call from it. This is done in objcMessageExpr_trans. *) let exec_with_self_exception f trans_state stmt = try f trans_state stmt with Self.SelfClassException class_name -> - let typ = CTypes_decl.objc_class_name_to_sil_type trans_state.context.CContext.tenv class_name in + let typ = + CTypes_decl.objc_class_name_to_sil_type trans_state.context.CContext.tenv class_name in let expanded_type = CTypes.expand_structured_type trans_state.context.CContext.tenv typ in { empty_res_trans with exps = [(Sil.Sizeof(expanded_type, Sil.Subtype.exact), Sil.Tint Sil.IULong)] } @@ -241,8 +255,10 @@ struct "[Warning] Need exactly one expression to add reference type\n" in { res_trans with exps = [(exp, add_reference_if_glvalue typ expr_info)] } - (* Execute translation of e forcing to release priority (if it's not free) and then setting it back.*) - (* This is used in conditional operators where we need to force the priority to be free for the *) + (* Execute translation of e forcing to release priority + (if it's not free) and then setting it back.*) + (* This is used in conditional operators where we need to force + the priority to be free for the *) (* computation of the expressions*) let exec_with_priority_exception trans_state e f = if PriorityNode.is_priority_free trans_state then @@ -253,7 +269,7 @@ struct let procname = Cfg.Procdesc.get_proc_name procdesc in let id = Ident.create_fresh Ident.knormal in let pvar_mangled = Mangled.from_string (var_name_prefix ^ Ident.to_string id) in - Sil.mk_pvar pvar_mangled procname + Pvar.mk pvar_mangled procname let mk_temp_sil_var_for_expr tenv procdesc var_name_prefix expr_info = let type_ptr = expr_info.Clang_ast_t.ei_type_ptr in @@ -265,7 +281,7 @@ struct let procdesc = context.CContext.procdesc in let (pvar, typ) = mk_temp_sil_var_for_expr context.CContext.tenv procdesc var_name expr_info in - Cfg.Procdesc.append_locals procdesc [(Sil.pvar_get_name pvar, typ)]; + Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, typ)]; Sil.Lvar pvar, typ let create_call_instr trans_state return_type function_sil params_sil sil_loc @@ -281,7 +297,7 @@ struct | _ -> let procdesc = trans_state.context.CContext.procdesc in let pvar = mk_temp_sil_var procdesc "__temp_return_" in - Cfg.Procdesc.append_locals procdesc [(Sil.pvar_get_name pvar, return_type)]; + Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, return_type)]; Sil.Lvar pvar in (* It is very confusing - same expression has two different types in two contexts:*) (* 1. if passed as parameter it's RETURN_TYPE* since we are passing it as rvalue *) @@ -323,10 +339,14 @@ struct let exp = Sil.Const (Sil.Cstr (str)) in { empty_res_trans with exps = [(exp, typ)]} - (* FROM CLANG DOCS: "Implements the GNU __null extension, which is a name for a null pointer constant *) - (* that has integral type (e.g., int or long) and is the same size and alignment as a pointer. The __null *) - (* extension is typically only used by system headers, which define NULL as __null in C++ rather than using 0 *) - (* (which is an integer that may not match the size of a pointer)". So we implement it as the constant zero *) + (* FROM CLANG DOCS: "Implements the GNU __null extension, + which is a name for a null pointer constant *) + (* that has integral type (e.g., int or long) and is the same + size and alignment as a pointer. The __null *) + (* extension is typically only used by system headers, + which define NULL as __null in C++ rather than using 0 *) + (* (which is an integer that may not match the size of a pointer)". + So we implement it as the constant zero *) let gNUNullExpr_trans trans_state expr_info = let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in let exp = Sil.Const (Sil.Cint (Sil.Int.zero)) in @@ -404,14 +424,17 @@ struct let typ = CTypes_decl.type_ptr_to_sil_type tenv expr_info.Clang_ast_t.ei_type_ptr in match unary_expr_or_type_trait_expr_info.Clang_ast_t.uttei_kind with | `SizeOf -> - let tp = Ast_utils.type_from_unary_expr_or_type_trait_expr_info unary_expr_or_type_trait_expr_info in + let tp = + Ast_utils.type_from_unary_expr_or_type_trait_expr_info + unary_expr_or_type_trait_expr_info in let sizeof_typ = match tp with | Some tp -> CTypes_decl.type_ptr_to_sil_type tenv tp | None -> typ in (* Some default type since the type is missing *) { empty_res_trans with exps = [(Sil.Sizeof(sizeof_typ, Sil.Subtype.exact), sizeof_typ)]} | k -> Printing.log_stats - "\nWARNING: Missing translation of Uniry_Expression_Or_Trait of kind: %s . Expression ignored, returned -1... \n" + "\nWARNING: Missing translation of Uniry_Expression_Or_Trait of kind: \ + %s . Expression ignored, returned -1... \n" (Clang_ast_j.string_of_unary_expr_or_type_trait_kind k); { empty_res_trans with exps =[(Sil.exp_minus_one, typ)]} @@ -470,7 +493,7 @@ struct (CTypes_decl.get_type_curr_class_objc context.tenv curr_class) in [(e, typ)] else [(e, typ)] in - Printing.log_out "\n\n PVAR ='%s'\n\n" (Sil.pvar_to_string pvar); + Printing.log_out "\n\n PVAR ='%s'\n\n" (Pvar.to_string pvar); let res_trans = { empty_res_trans with exps = exps } in if CTypes.is_reference_type type_ptr then (* dereference pvar due to the behavior of reference types in clang's AST *) @@ -579,7 +602,7 @@ struct let context = trans_state.context in let procname = Cfg.Procdesc.get_proc_name context.CContext.procdesc in let name = CFrontend_config.this in - let pvar = Sil.mk_pvar (Mangled.from_string name) procname in + let pvar = Pvar.mk (Mangled.from_string name) procname in let exp = Sil.Lvar pvar in let typ = CTypes_decl.type_ptr_to_sil_type context.CContext.tenv class_type_ptr in let exps = [(exp, typ)] in @@ -697,7 +720,7 @@ struct res_trans_a.leaf_nodes; (* Note the order of res_trans_idx.ids @ res_trans_a.ids is important. *) - (* We expect to use only res_trans_idx.ids in construction of other operation. *) + (* We expect to use only res_trans_idx.ids in construction of other operation. *) (* res_trans_a.ids is passed to be Removed.*) { empty_res_trans with root_nodes; @@ -708,7 +731,8 @@ struct initd_exps = res_trans_idx.initd_exps @ res_trans_a.initd_exps; } and binaryOperator_trans trans_state binary_operator_info stmt_info expr_info stmt_list = - let bok = (Clang_ast_j.string_of_binary_operator_kind binary_operator_info.Clang_ast_t.boi_kind) in + let bok = + Clang_ast_j.string_of_binary_operator_kind binary_operator_info.Clang_ast_t.boi_kind in Printing.log_out " BinaryOperator '%s' " bok; Printing.log_out " priority node free = '%s'\n@." (string_of_bool (PriorityNode.is_priority_free trans_state)); @@ -717,7 +741,8 @@ struct let nname = "BinaryOperatorStmt: "^ (CArithmetic_trans.bin_op_to_string binary_operator_info) in let trans_state' = { trans_state_pri with succ_nodes = [] } in let sil_loc = CLocation.get_sil_location stmt_info context in - let typ = CTypes_decl.type_ptr_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in + let typ = + CTypes_decl.type_ptr_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in (match stmt_list with | [s1; s2] -> (* Assumption: We expect precisely 2 stmt corresponding to the 2 operands*) let rhs_owning_method = CTrans_utils.is_owning_method s2 in @@ -792,7 +817,8 @@ struct let trans_state_param = { trans_state_pri with succ_nodes = []; var_exp_typ = None } in let (sil_fe, _) = extract_exp_from_list res_trans_callee.exps - "WARNING: The translation of fun_exp did not return an expression. Returning -1. NEED TO BE FIXED" in + "WARNING: The translation of fun_exp did not return an expression.\ + Returning -1. NEED TO BE FIXED" in let callee_pname_opt = match sil_fe with | Sil.Const (Sil.Cfun pn) -> @@ -823,12 +849,14 @@ struct if IList.length params = IList.length params_stmt then params else (Printing.log_err - "WARNING: stmt_list and res_trans_par.exps must have same size. NEED TO BE FIXED\n\n"; + "WARNING: stmt_list and res_trans_par.exps must have same size. \ + NEED TO BE FIXED\n\n"; fix_param_exps_mismatch params_stmt params) in let act_params = if is_cf_retain_release then (Sil.Const (Sil.Cint Sil.Int.one), Sil.Tint Sil.IBool) :: act_params else act_params in - match CTrans_utils.builtin_trans trans_state_pri sil_loc si function_type callee_pname_opt with + match + CTrans_utils.builtin_trans trans_state_pri sil_loc si function_type callee_pname_opt with | Some builtin -> builtin | None -> let res_trans_call = @@ -925,7 +953,7 @@ struct let procdesc = trans_state.context.CContext.procdesc in let pvar = mk_temp_sil_var procdesc "__temp_construct_" in let class_type = CTypes_decl.get_type_from_expr_info ei context.CContext.tenv in - Cfg.Procdesc.append_locals procdesc [(Sil.pvar_get_name pvar, class_type)]; + Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, class_type)]; Sil.Lvar pvar, class_type in let this_type = match class_type with @@ -1047,21 +1075,24 @@ struct let procname = Cfg.Procdesc.get_proc_name trans_state.context.CContext.procdesc in let pvar = CFrontend_utils.General_utils.get_next_block_pvar procname in let transformed_stmt, _ = - Ast_expressions.translate_dispatch_function (Sil.pvar_to_string pvar) stmt_info stmt_list n in + Ast_expressions.translate_dispatch_function + (Pvar.to_string pvar) stmt_info stmt_list n in instruction trans_state transformed_stmt and block_enumeration_trans trans_state stmt_info stmt_list ei = let declare_nullify_vars loc preds pvar = (* Add nullify of the temp block var to the last node (predecessor or the successor nodes)*) - IList.iter (fun n -> Cfg.Node.append_instrs_temps n [Sil.Nullify(pvar, loc, true)] []) preds in + IList.iter + (fun n -> Cfg.Node.append_instrs_temps n [Sil.Nullify(pvar, loc, true)] []) + preds in Printing.log_out "\n Call to a block enumeration function treated as special case...\n@."; let procname = Cfg.Procdesc.get_proc_name trans_state.context.CContext.procdesc in let pvar = CFrontend_utils.General_utils.get_next_block_pvar procname in let transformed_stmt, vars_to_register = - Ast_expressions.translate_block_enumerate (Sil.pvar_to_string pvar) stmt_info stmt_list ei in + Ast_expressions.translate_block_enumerate (Pvar.to_string pvar) stmt_info stmt_list ei in let pvars = IList.map (fun (v, _, _) -> - Sil.mk_pvar (Mangled.from_string v) procname + Pvar.mk (Mangled.from_string v) procname ) vars_to_register in let loc = CLocation.get_sil_location stmt_info trans_state.context in let res_state = instruction trans_state transformed_stmt in @@ -1077,7 +1108,7 @@ struct let succ_nodes = trans_state.succ_nodes in let procname = Cfg.Procdesc.get_proc_name context.CContext.procdesc in let mk_temp_var id = - Sil.mk_pvar (Mangled.from_string ("SIL_temp_conditional___"^(string_of_int id))) procname in + Pvar.mk (Mangled.from_string ("SIL_temp_conditional___"^(string_of_int id))) procname in let sil_loc = CLocation.get_sil_location stmt_info context in let do_branch branch stmt var_typ prune_nodes join_node pvar = let trans_state_pri = PriorityNode.force_claim_priority_node trans_state stmt_info in @@ -1100,7 +1131,8 @@ struct (match stmt_list with | [cond; exp1; exp2] -> let typ = - CTypes_decl.type_ptr_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in + CTypes_decl.type_ptr_to_sil_type + context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in let var_typ = add_reference_if_glvalue typ expr_info in let join_node = create_node (Cfg.Node.Join_node) [] [] sil_loc context in Cfg.Node.set_succs_exn join_node succ_nodes []; @@ -1152,7 +1184,9 @@ struct define_condition_side_effects res_trans_cond.exps res_trans_cond.instrs sil_loc in let prune_t = mk_prune_node true e' res_trans_cond.ids instrs' in let prune_f = mk_prune_node false e' res_trans_cond.ids instrs' in - IList.iter (fun n' -> Cfg.Node.set_succs_exn n' [prune_t; prune_f] []) res_trans_cond.leaf_nodes; + IList.iter + (fun n' -> Cfg.Node.set_succs_exn n' [prune_t; prune_f] []) + res_trans_cond.leaf_nodes; let rnodes = if (IList.length res_trans_cond.root_nodes) = 0 then [prune_t; prune_f] else res_trans_cond.root_nodes in @@ -1173,7 +1207,8 @@ struct (* the condition to decide its truth value). *) let short_circuit binop s1 s2 = let res_trans_s1 = cond_trans trans_state s1 in - let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node res_trans_s1.leaf_nodes in + let prune_nodes_t, prune_nodes_f = + IList.partition is_true_prune_node res_trans_s1.leaf_nodes in let res_trans_s2 = cond_trans trans_state s2 in (* prune_to_s2 is the prune node that is connected with the root node of the *) (* translation of s2.*) @@ -1185,7 +1220,9 @@ struct | _ -> assert false) in IList.iter (fun n -> Cfg.Node.set_succs_exn n res_trans_s2.root_nodes []) prune_to_s2; let root_nodes_to_parent = - if (IList.length res_trans_s1.root_nodes) = 0 then res_trans_s1.leaf_nodes else res_trans_s1.root_nodes in + if (IList.length res_trans_s1.root_nodes) = 0 + then res_trans_s1.leaf_nodes + else res_trans_s1.root_nodes in let (exp1, typ1) = extract_exp res_trans_s1.exps in let (exp2, _) = extract_exp res_trans_s2.exps in let e_cond = Sil.BinOp (binop, exp1, exp2) in @@ -1227,9 +1264,13 @@ struct let do_branch branch stmt_branch prune_nodes = (* leaf nodes are ignored here as they will be already attached to join_node *) let res_trans_b = instruction trans_state' stmt_branch in - let nodes_branch = (match res_trans_b.root_nodes with - | [] -> [create_node (Cfg.Node.Stmt_node "IfStmt Branch" ) res_trans_b.ids res_trans_b.instrs sil_loc context] - | _ -> res_trans_b.root_nodes) in + let nodes_branch = + (match res_trans_b.root_nodes with + | [] -> + [create_node (Cfg.Node.Stmt_node "IfStmt Branch" ) + res_trans_b.ids res_trans_b.instrs sil_loc context] + | _ -> + res_trans_b.root_nodes) in let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes in let prune_nodes' = if branch then prune_nodes_t else prune_nodes_f in IList.iter (fun n -> Cfg.Node.set_succs_exn n nodes_branch []) prune_nodes'; @@ -1269,7 +1310,9 @@ struct let switch_special_cond_node = let node_kind = Cfg.Node.Stmt_node "Switch_stmt" in create_node node_kind [] res_trans_cond_tmp.instrs sil_loc context in - IList.iter (fun n' -> Cfg.Node.set_succs_exn n' [switch_special_cond_node] []) res_trans_cond_tmp.leaf_nodes; + IList.iter + (fun n' -> Cfg.Node.set_succs_exn n' [switch_special_cond_node] []) + res_trans_cond_tmp.leaf_nodes; let root_nodes = if res_trans_cond_tmp.root_nodes <> [] then res_trans_cond_tmp.root_nodes else [switch_special_cond_node] in @@ -1281,7 +1324,9 @@ struct leaf_nodes = [switch_special_cond_node] } in let res_trans_decl = declStmt_in_condition_trans trans_state decl_stmt res_trans_cond in - let trans_state_no_pri = if PriorityNode.own_priority_node trans_state_pri.priority stmt_info then + let trans_state_no_pri = + if PriorityNode.own_priority_node trans_state_pri.priority stmt_info + then { trans_state_pri with priority = Free } else trans_state_pri in let switch_exit_point = succ_nodes in @@ -1294,18 +1339,24 @@ struct let rec aux rev_stmt_list acc cases = (match rev_stmt_list with | CaseStmt (info, a :: b :: (CaseStmt x) :: c) :: rest -> (* case x: case y: ... *) - if c <> [] then assert false; (* empty case with nested case, then followed by some instructions *) + if c <> [] + (* empty case with nested case, then followed by some instructions *) + then assert false; let rest' = [CaseStmt(info, a :: b :: [])] @ rest in let rev_stmt_list' = (CaseStmt x) :: rest' in aux rev_stmt_list' acc cases | CaseStmt (info, a :: b :: (DefaultStmt x) :: c) :: rest -> (* case x: default: ... *) - if c <> [] then assert false; (* empty case with nested case, then followed by some instructions *) + if c <> [] + (* empty case with nested case, then followed by some instructions *) + then assert false; let rest' = [CaseStmt(info, a :: b :: [])] @ rest in let rev_stmt_list' = (DefaultStmt x) :: rest' in aux rev_stmt_list' acc cases | DefaultStmt (info, (CaseStmt x) :: c) :: rest -> (* default: case x: ... *) - if c <> [] then assert false; (* empty case with nested case, then followed by some instructions *) + if c <> [] + (* empty case with nested case, then followed by some instructions *) + then assert false; let rest' = [DefaultStmt(info, [])] @ rest in let rev_stmt_list' = (CaseStmt x) :: rest' in aux rev_stmt_list' acc cases @@ -1355,7 +1406,8 @@ struct match cases with (* top-down to handle default cases *) | [] -> next_nodes, next_prune_nodes | CaseStmt(_, _ :: _ :: case_content) as case :: rest -> - let last_nodes, last_prune_nodes = translate_and_connect_cases rest next_nodes next_prune_nodes in + let last_nodes, last_prune_nodes = + translate_and_connect_cases rest next_nodes next_prune_nodes in let case_entry_point = connected_instruction (IList.rev case_content) last_nodes in (* connects between cases, then continuation has priority about breaks *) let prune_node_t, prune_node_f = create_prune_nodes_for_case case in @@ -1366,30 +1418,38 @@ struct let sil_loc = CLocation.get_sil_location stmt_info context in let placeholder_entry_point = create_node (Cfg.Node.Stmt_node "DefaultStmt_placeholder") [] [] sil_loc context in - let last_nodes, last_prune_nodes = translate_and_connect_cases rest next_nodes [placeholder_entry_point] in - let default_entry_point = connected_instruction (IList.rev default_content) last_nodes in + let last_nodes, last_prune_nodes = + translate_and_connect_cases rest next_nodes [placeholder_entry_point] in + let default_entry_point = + connected_instruction (IList.rev default_content) last_nodes in Cfg.Node.set_succs_exn placeholder_entry_point default_entry_point []; default_entry_point, last_prune_nodes | _ -> assert false in - let top_entry_point, top_prune_nodes = translate_and_connect_cases list_of_cases succ_nodes succ_nodes in + let top_entry_point, top_prune_nodes = + translate_and_connect_cases list_of_cases succ_nodes succ_nodes in let _ = connected_instruction (IList.rev pre_case_stmts) top_entry_point in Cfg.Node.set_succs_exn switch_special_cond_node top_prune_nodes []; let top_nodes = res_trans_decl.root_nodes in - IList.iter (fun n' -> Cfg.Node.append_instrs_temps n' [] res_trans_cond.ids) succ_nodes; (* succ_nodes will remove the temps *) + IList.iter + (fun n' -> Cfg.Node.append_instrs_temps n' [] res_trans_cond.ids) succ_nodes; + (* succ_nodes will remove the temps *) { empty_res_trans with root_nodes = top_nodes; leaf_nodes = succ_nodes } | _ -> assert false and stmtExpr_trans trans_state stmt_info stmt_list = let context = trans_state.context in - let stmt = extract_stmt_from_singleton stmt_list "ERROR: StmtExpr should have only one statement.\n" in + let stmt = + extract_stmt_from_singleton stmt_list + "ERROR: StmtExpr should have only one statement.\n" in let res_trans_stmt = instruction trans_state stmt in let idl = res_trans_stmt.ids in let exps' = IList.rev res_trans_stmt.exps in match exps' with | (last, typ) :: _ -> (* The StmtExpr contains a single CompoundStmt node, which it evaluates and *) - (* takes the value of the last subexpression.*) - (* Exp returned by StmtExpr is always a RValue. So we need to assign to a temp and return the temp.*) + (* takes the value of the last subexpression. *) + (* Exp returned by StmtExpr is always a RValue. + So we need to assign to a temp and return the temp. *) let id = Ident.create_fresh Ident.knormal in let loc = CLocation.get_sil_location stmt_info context in let instr' = Sil.Letderef (id, last, typ, loc) in @@ -1457,7 +1517,8 @@ struct | Loops.For _ | Loops.While _ -> res_trans_decl.root_nodes | Loops.DoWhile _ -> res_trans_body.root_nodes in (* Note: prune nodes are by contruction the res_trans_cond.leaf_nodes *) - let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node res_trans_cond.leaf_nodes in + let prune_nodes_t, prune_nodes_f = + IList.partition is_true_prune_node res_trans_cond.leaf_nodes in let prune_t_succ_nodes = match loop_kind with | Loops.For _ | Loops.While _ -> res_trans_body.root_nodes @@ -1485,7 +1546,7 @@ struct loop_instruction trans_state dowhile_kind stmt_info - (* Iteration over colection + (* Iteration over colection for (v : C) { body; } @@ -1494,21 +1555,22 @@ struct TypeC __range = C; for (__begin = __range.begin(), __end = __range.end(); __begin != __end; - ++__begin) + ++__begin) { v = *__begin; loop_body; - } + } *) and cxxForRangeStmt_trans trans_state stmt_info stmt_list = let open Clang_ast_t in match stmt_list with - | [iterator_decl; initial_cond; exit_cond; increment; assign_current_index; loop_body] -> + | [iterator_decl; initial_cond; exit_cond; increment; assign_current_index; loop_body] -> let loop_body' = CompoundStmt (stmt_info, [assign_current_index; loop_body]) in let null_stmt = NullStmt (stmt_info, []) in - let for_loop = ForStmt (stmt_info, [initial_cond; null_stmt; exit_cond; increment; loop_body']) in + let for_loop = + ForStmt (stmt_info, [initial_cond; null_stmt; exit_cond; increment; loop_body']) in instruction trans_state (CompoundStmt (stmt_info, [iterator_decl; for_loop])) - | _ -> assert false + | _ -> assert false (* Fast iteration for colection for (type_it i in collection) { body } @@ -1580,14 +1642,17 @@ struct and init_expr_trans trans_state var_exp_typ var_stmt_info init_expr_opt = match init_expr_opt with - | None -> { empty_res_trans with root_nodes = trans_state.succ_nodes } (* Nothing to do if no init expression *) + | None -> + (* Nothing to do if no init expression *) + { empty_res_trans with root_nodes = trans_state.succ_nodes } | Some ie -> (*For init expr, translate how to compute it and assign to the var*) let stmt_info, _ = Clang_ast_proj.get_stmt_tuple ie in let var_exp, _ = var_exp_typ in let context = trans_state.context in let sil_loc = CLocation.get_sil_location stmt_info context in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state var_stmt_info in - (* if ie is a block the translation need to be done with the block special cases by exec_with_block_priority*) + (* if ie is a block the translation need to be done + with the block special cases by exec_with_block_priority *) let res_trans_ie = let trans_state' = { trans_state_pri with succ_nodes = []; @@ -1605,7 +1670,8 @@ struct (CTrans_utils.is_method_call ie || ObjcInterface_decl.is_pointer_to_objc_class context.CContext.tenv ie_typ) then - (* In arc mode, if it's a method call or we are initializing with a pointer to objc class *) + (* In arc mode, if it's a method call or we are initializing + with a pointer to objc class *) (* we need to add retain/release *) let (e, instrs, ids) = CArithmetic_trans.assignment_arc_mode @@ -1667,7 +1733,8 @@ struct collect_all_decl trans_state decl_list succ_nodes stmt_info | _ -> Printing.log_stats - "WARNING: In DeclStmt found an unknown declaration type. RETURNING empty list of declaration. NEED TO BE FIXED"; + "WARNING: In DeclStmt found an unknown declaration type. \ + RETURNING empty list of declaration. NEED TO BE FIXED"; empty_res_trans in { res_trans with leaf_nodes = [] } @@ -1693,11 +1760,15 @@ struct (* defines how that expression is going to be implemented at runtime. *) (* 2. the semantic description is composed by a list of OpaqueValueExpr that define the *) (* various expressions involved and one finale expression that define how the final value of*) - (* the PseudoObjectExpr is obtained. All the OpaqueValueExpr will be part of the last expression.*) + (* the PseudoObjectExpr is obtained. + All the OpaqueValueExpr will be part of the last expression.*) (* So they can be skipped. *) - (* For example: 'x.f = a' when 'f' is a property will be translated with a call to f's setter [x f:a]*) - (* the stmt_list will be [x.f = a; x; a; CallToSetter] Among all element of the list we only need*) - (* to translate the CallToSetter which is how x.f = a is actually implemented by the runtime.*) + (* For example: 'x.f = a' when 'f' is a property will be + translated with a call to f's setter [x f:a]*) + (* the stmt_list will be [x.f = a; x; a; CallToSetter] + Among all element of the list we only need*) + (* to translate the CallToSetter which is + how x.f = a is actually implemented by the runtime.*) and pseudoObjectExpr_trans trans_state stmt_list = Printing.log_out " priority node free = '%s'\n@." (string_of_bool (PriorityNode.is_priority_free trans_state)); @@ -1759,12 +1830,17 @@ struct let sil_loc = CLocation.get_sil_location stmt_info context in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in let stmt = extract_stmt_from_singleton stmt_list - "WARNING: We expect only one element in stmt list defining the operand in UnaryOperator. NEED FIXING\n" in + "WARNING: We expect only one element in stmt list defining \ + the operand in UnaryOperator. NEED FIXING\n" in let trans_state' = { trans_state_pri with succ_nodes = [] } in let res_trans_stmt = instruction trans_state' stmt in (* Assumption: the operand does not create a cfg node*) - let (sil_e', _) = extract_exp_from_list res_trans_stmt.exps "\nWARNING: Missing operand in unary operator. NEED FIXING.\n" in - let ret_typ = CTypes_decl.type_ptr_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in + let (sil_e', _) = + extract_exp_from_list res_trans_stmt.exps + "\nWARNING: Missing operand in unary operator. NEED FIXING.\n" in + let ret_typ = + CTypes_decl.type_ptr_to_sil_type + context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in let ids_op, exp_op, instr_op = CArithmetic_trans.unary_operation_instruction unary_operator_info sil_e' ret_typ sil_loc in let unary_op_res_trans = { empty_res_trans with ids = ids_op; instrs = instr_op } in @@ -1791,7 +1867,7 @@ struct | Some ret_param_typ -> let name = CFrontend_config.return_param in let procname = Cfg.Procdesc.get_proc_name procdesc in - let pvar = Sil.mk_pvar (Mangled.from_string name) procname in + let pvar = Pvar.mk (Mangled.from_string name) procname in let id = Ident.create_fresh Ident.knormal in let instr = Sil.Letderef (id, Sil.Lvar pvar, ret_param_typ, sil_loc) in let ret_typ = match ret_param_typ with Sil.Tptr (t, _) -> t | _ -> assert false in @@ -1808,20 +1884,25 @@ struct let ret_instrs = if IList.exists (Sil.exp_equal ret_exp) res_trans_stmt.initd_exps then [] else [Sil.Set (ret_exp, ret_type, sil_expr, sil_loc)] in - let autorelease_ids, autorelease_instrs = add_autorelease_call context sil_expr ret_type sil_loc in + let autorelease_ids, autorelease_instrs = + add_autorelease_call context sil_expr ret_type sil_loc in let instrs = var_instrs @ res_trans_stmt.instrs @ ret_instrs @ autorelease_instrs in let ids = var_ids @ res_trans_stmt.ids @ autorelease_ids in let ret_node = mk_ret_node ids instrs in IList.iter (fun n -> Cfg.Node.set_succs_exn n [ret_node] []) res_trans_stmt.leaf_nodes; let root_nodes_to_parent = - if IList.length res_trans_stmt.root_nodes >0 then res_trans_stmt.root_nodes else [ret_node] in + if IList.length res_trans_stmt.root_nodes >0 + then res_trans_stmt.root_nodes + else [ret_node] in { empty_res_trans with root_nodes = root_nodes_to_parent; leaf_nodes = [ret_node]} | [] -> (* return; *) let ret_node = mk_ret_node [] [] in { empty_res_trans with root_nodes = [ret_node]; leaf_nodes = [ret_node]} | _ -> Printing.log_out - "\nWARNING: Missing translation of Return Expression. Return Statement ignored. Need fixing!\n"; - { empty_res_trans with root_nodes = succ_nodes }) in (* We expect a return with only one expression *) + "\nWARNING: Missing translation of Return Expression. \ + Return Statement ignored. Need fixing!\n"; + { empty_res_trans with root_nodes = succ_nodes }) in + (* We expect a return with only one expression *) trans_result (* We analyze the content of the expr. We treat ExprWithCleanups as a wrapper. *) @@ -1834,13 +1915,18 @@ struct instruction trans_state stmt and objCBoxedExpr_trans trans_state info sel stmt_info stmts = - let typ = CTypes_decl.class_from_pointer_type trans_state.context.CContext.tenv info.Clang_ast_t.ei_type_ptr in + let typ = + CTypes_decl.class_from_pointer_type + trans_state.context.CContext.tenv info.Clang_ast_t.ei_type_ptr in let obj_c_message_expr_info = Ast_expressions.make_obj_c_message_expr_info_class sel typ None in - let message_stmt = Clang_ast_t.ObjCMessageExpr (stmt_info, stmts, info, obj_c_message_expr_info) in + let message_stmt = + Clang_ast_t.ObjCMessageExpr (stmt_info, stmts, info, obj_c_message_expr_info) in instruction trans_state message_stmt and objCArrayLiteral_trans trans_state info stmt_info stmts = - let typ = CTypes_decl.class_from_pointer_type trans_state.context.CContext.tenv info.Clang_ast_t.ei_type_ptr in + let typ = + CTypes_decl.class_from_pointer_type + trans_state.context.CContext.tenv info.Clang_ast_t.ei_type_ptr in let meth = CFrontend_config.array_with_objects_count_m in let obj_c_mes_expr_info = Ast_expressions.make_obj_c_message_expr_info_class meth typ None in let stmts = stmts @ [Ast_expressions.create_nil stmt_info] in @@ -1848,20 +1934,26 @@ struct instruction trans_state message_stmt and objCDictionaryLiteral_trans trans_state info stmt_info stmts = - let typ = CTypes_decl.class_from_pointer_type trans_state.context.CContext.tenv info.Clang_ast_t.ei_type_ptr in + let typ = + CTypes_decl.class_from_pointer_type + trans_state.context.CContext.tenv info.Clang_ast_t.ei_type_ptr in let dictionary_literal_pname = SymExec.ModelBuiltins.__objc_dictionary_literal in let dictionary_literal_s = Procname.get_method dictionary_literal_pname in let obj_c_message_expr_info = Ast_expressions.make_obj_c_message_expr_info_class dictionary_literal_s typ None in let stmts = General_utils.swap_elements_list stmts in let stmts = stmts @ [Ast_expressions.create_nil stmt_info] in - let message_stmt = Clang_ast_t.ObjCMessageExpr (stmt_info, stmts, info, obj_c_message_expr_info) in + let message_stmt = + Clang_ast_t.ObjCMessageExpr + (stmt_info, stmts, info, obj_c_message_expr_info) in instruction trans_state message_stmt and objCStringLiteral_trans trans_state stmt_info stmts info = let stmts = [Ast_expressions.create_implicit_cast_expr stmt_info stmts Ast_expressions.create_char_star_type `ArrayToPointerDecay] in - let typ = CTypes_decl.class_from_pointer_type trans_state.context.CContext.tenv info.Clang_ast_t.ei_type_ptr in + let typ = + CTypes_decl.class_from_pointer_type + trans_state.context.CContext.tenv info.Clang_ast_t.ei_type_ptr in let meth = CFrontend_config.string_with_utf8_m in let obj_c_mess_expr_info = Ast_expressions.make_obj_c_message_expr_info_class meth typ None in let message_stmt = Clang_ast_t.ObjCMessageExpr (stmt_info, stmts, info, obj_c_mess_expr_info) in @@ -1875,7 +1967,9 @@ struct let fname = SymExec.ModelBuiltins.__objc_release_autorelease_pool in let ret_id = Ident.create_fresh Ident.knormal in let autorelease_pool_vars = CVar_decl.compute_autorelease_pool_vars trans_state.context stmts in - let stmt_call = Sil.Call([ret_id], (Sil.Const (Sil.Cfun fname)), autorelease_pool_vars, sil_loc, Sil.cf_default) in + let stmt_call = + Sil.Call([ret_id], (Sil.Const (Sil.Cfun fname)), + autorelease_pool_vars, sil_loc, Sil.cf_default) in let node_kind = Cfg.Node.Stmt_node ("Release the autorelease pool") in let call_node = create_node node_kind ([ret_id]) ([stmt_call]) sil_loc trans_state.context in Cfg.Node.set_succs_exn call_node trans_state.succ_nodes []; @@ -1884,7 +1978,8 @@ struct (* Assumption: stmt_list contains 2 items, the first can be ObjCMessageExpr or ParenExpr *) (* We ignore this item since we don't deal with the concurrency problem yet *) - (* For the same reason we also ignore the stmt_info that is related with the ObjCAtSynchronizedStmt construct *) + (* For the same reason we also ignore the stmt_info that + is related with the ObjCAtSynchronizedStmt construct *) (* Finally we recursively work on the CompoundStmt, the second item of stmt_list *) and objCAtSynchronizedStmt_trans trans_state stmt_list = (match stmt_list with @@ -1912,18 +2007,18 @@ struct (* defining procedure. We add an edge in the call graph.*) Cg.add_edge context.cg procname block_pname; let captured_block_vars = block_decl_info.Clang_ast_t.bdi_captured_variables in - let captured_pvars = CVar_decl.captured_vars_from_block_info context captured_block_vars in - let ids_instrs = IList.map assign_captured_var captured_pvars in + let captureds = CVar_decl.captured_vars_from_block_info context captured_block_vars in + let ids_instrs = IList.map assign_captured_var captureds in let ids, instrs = IList.split ids_instrs in - let block_data = (context, type_ptr, block_pname, captured_pvars) in + let block_data = (context, type_ptr, block_pname, captureds) in F.function_decl context.tenv context.cfg context.cg decl (Some block_data); Cfg.set_procname_priority context.cfg block_pname; let captured_vars = - IList.map2 (fun id (pvar, typ) -> (Sil.Var id, pvar, typ)) ids captured_pvars in + IList.map2 (fun id (pvar, typ) -> (Sil.Var id, pvar, typ)) ids captureds in let closure = Sil.Cclosure { name=block_pname; captured_vars } in let block_name = Procname.to_string block_pname in let static_vars = CContext.static_vars_for_block context block_pname in - let captured_static_vars = captured_pvars @ static_vars in + let captured_static_vars = captureds @ static_vars in let alloc_block_instr, ids_block = allocate_block trans_state block_name captured_static_vars loc in { empty_res_trans with @@ -2001,7 +2096,7 @@ struct let (pvar, typ) = mk_temp_sil_var_for_expr context.CContext.tenv procdesc "SIL_materialize_temp__" expr_info in let temp_exp = match stmt_list with [p] -> p | _ -> assert false in - Cfg.Procdesc.append_locals procdesc [(Sil.pvar_get_name pvar, typ)]; + Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, typ)]; let var_exp_typ = (Sil.Lvar pvar, typ) in let res_trans = init_expr_trans trans_state var_exp_typ stmt_info (Some temp_exp) in { res_trans with exps = [var_exp_typ] } @@ -2185,7 +2280,9 @@ struct switchStmt_trans trans_state stmt_info switch_stmt_list | CaseStmt _ -> - Printing.log_out "FATAL: Passing from CaseStmt outside of SwitchStmt, terminating.\n"; assert false + Printing.log_out + "FATAL: Passing from CaseStmt outside of SwitchStmt, terminating.\n"; + assert false | StmtExpr(stmt_info, stmt_list, _) -> stmtExpr_trans trans_state stmt_info stmt_list @@ -2199,7 +2296,7 @@ struct | DoStmt(stmt_info, [body; cond]) -> doStmt_trans trans_state stmt_info cond body - | CXXForRangeStmt (stmt_info, stmt_list) -> + | CXXForRangeStmt (stmt_info, stmt_list) -> cxxForRangeStmt_trans trans_state stmt_info stmt_list | ObjCForCollectionStmt(stmt_info, [item; items; body]) -> @@ -2269,8 +2366,10 @@ struct memberExpr_trans trans_state stmt_info stmt_list member_expr_info | UnaryOperator(stmt_info, stmt_list, expr_info, unary_operator_info) -> - if is_logical_negation_of_int trans_state.context.CContext.tenv expr_info unary_operator_info then - let conditional = Ast_expressions.trans_negation_with_conditional stmt_info expr_info stmt_list in + if is_logical_negation_of_int + trans_state.context.CContext.tenv expr_info unary_operator_info then + let conditional = + Ast_expressions.trans_negation_with_conditional stmt_info expr_info stmt_list in instruction trans_state conditional else unaryOperator_trans trans_state stmt_info expr_info stmt_list unary_operator_info @@ -2351,7 +2450,8 @@ struct | BinaryConditionalOperator (stmt_info, stmts, expr_info) -> (match stmts with - | [stmt1; ostmt1; ostmt2; stmt2] when contains_opaque_value_expr ostmt1 && contains_opaque_value_expr ostmt2 -> + | [stmt1; ostmt1; ostmt2; stmt2] + when contains_opaque_value_expr ostmt1 && contains_opaque_value_expr ostmt2 -> conditionalOperator_trans trans_state stmt_info [stmt1; stmt1; stmt2] expr_info | _ -> Printing.log_stats "BinaryConditionalOperator not translated %s @." @@ -2398,7 +2498,8 @@ struct cxxStdInitializerListExpr_trans trans_state stmt_info stmts expr_info | s -> (Printing.log_stats - "\n!!!!WARNING: found statement %s. \nACTION REQUIRED: Translation need to be defined. Statement ignored.... \n" + "\n!!!!WARNING: found statement %s. \nACTION REQUIRED: \ + Translation need to be defined. Statement ignored.... \n" (Ast_utils.string_of_stmt s); assert false) diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index e13700b7b..3cb569870 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -536,7 +536,7 @@ struct let t' = CTypes.add_pointer_to_typ (CTypes_decl.get_type_curr_class_objc context.CContext.tenv context.CContext.curr_class) in - let e = Sil.Lvar (Sil.mk_pvar (Mangled.from_string CFrontend_config.self) procname) in + let e = Sil.Lvar (Pvar.mk (Mangled.from_string CFrontend_config.self) procname) in let id = Ident.create_fresh Ident.knormal in t', Sil.Var id, [id], [Sil.Letderef (id, e, t', loc)] in { empty_res_trans with @@ -546,7 +546,7 @@ struct else empty_res_trans let is_var_self pvar is_objc_method = - let is_self = Mangled.to_string (Sil.pvar_get_name pvar) = CFrontend_config.self in + let is_self = Mangled.to_string (Pvar.get_name pvar) = CFrontend_config.self in is_self && is_objc_method end diff --git a/infer/src/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli index 974da2aca..de6ea0f06 100644 --- a/infer/src/clang/cTrans_utils.mli +++ b/infer/src/clang/cTrans_utils.mli @@ -211,7 +211,7 @@ sig CContext.t -> Procname.t -> Location.t -> Clang_ast_t.obj_c_message_expr_info -> trans_result - val is_var_self : Sil.pvar -> bool -> bool + val is_var_self : Pvar.t -> bool -> bool end val is_logical_negation_of_int : diff --git a/infer/src/clang/cVar_decl.ml b/infer/src/clang/cVar_decl.ml index d994aa260..2619d0ebb 100644 --- a/infer/src/clang/cVar_decl.ml +++ b/infer/src/clang/cVar_decl.ml @@ -50,7 +50,7 @@ let sil_var_of_decl_ref context decl_ref procname = General_utils.mk_sil_var name None procname outer_procname | _ -> if is_custom_var_pointer pointer then - Sil.mk_pvar (Mangled.from_string name.Clang_ast_t.ni_name) procname + Pvar.mk (Mangled.from_string name.Clang_ast_t.ni_name) procname else match Ast_utils.get_decl decl_ref.Clang_ast_t.dr_decl_pointer with | Some var_decl -> sil_var_of_decl context var_decl procname | None -> assert false @@ -60,7 +60,7 @@ let add_var_to_locals procdesc var_decl sil_typ pvar = match var_decl with | VarDecl (_, _, _, vdi) -> if not vdi.Clang_ast_t.vdi_is_global then - Cfg.Procdesc.append_locals procdesc [(Sil.pvar_get_name pvar, sil_typ)] + Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, sil_typ)] | _ -> assert false let rec compute_autorelease_pool_vars context stmts = @@ -75,8 +75,8 @@ let rec compute_autorelease_pool_vars context stmts = | Some type_ptr when decl_ref.Clang_ast_t.dr_kind = `Var -> let typ = CTypes_decl.type_ptr_to_sil_type context.CContext.tenv type_ptr in let pvar = sil_var_of_decl_ref context decl_ref procname in - if Sil.pvar_is_local pvar then - General_utils.append_no_duplicated_pvars [(Sil.Lvar pvar, typ)] res + if Pvar.is_local pvar then + General_utils.append_no_duplicateds [(Sil.Lvar pvar, typ)] res else res | _ -> res) | _ -> res) diff --git a/infer/src/clang/cVar_decl.mli b/infer/src/clang/cVar_decl.mli index c6986644e..662af8018 100644 --- a/infer/src/clang/cVar_decl.mli +++ b/infer/src/clang/cVar_decl.mli @@ -10,13 +10,13 @@ (** Process variable declarations by saving them as local or global variables. *) (** Computes the local variables of a function or method to be added to the procdesc *) -val sil_var_of_decl : CContext.t -> Clang_ast_t.decl -> Procname.t -> Sil.pvar +val sil_var_of_decl : CContext.t -> Clang_ast_t.decl -> Procname.t -> Pvar.t -val sil_var_of_decl_ref : CContext.t -> Clang_ast_t.decl_ref -> Procname.t -> Sil.pvar +val sil_var_of_decl_ref : CContext.t -> Clang_ast_t.decl_ref -> Procname.t -> Pvar.t -val add_var_to_locals : Cfg.Procdesc.t -> Clang_ast_t.decl -> Sil.typ -> Sil.pvar -> unit +val add_var_to_locals : Cfg.Procdesc.t -> Clang_ast_t.decl -> Sil.typ -> Pvar.t -> unit val compute_autorelease_pool_vars : CContext.t -> Clang_ast_t.stmt list -> (Sil.exp * Sil.typ) list val captured_vars_from_block_info : CContext.t -> Clang_ast_t.block_captured_variable list -> - (Sil.pvar * Sil.typ) list + (Pvar.t * Sil.typ) list diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index 6be1cc7b0..5102dbe28 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -73,13 +73,13 @@ struct tenv find_canonical_duplicate calls_this checks get_proc_desc idenv curr_pname curr_pdesc annotated_signature linereader proc_loc : bool * Extension.extension TypeState.t option = - let mk_pvar s = Sil.mk_pvar s curr_pname in + let mk s = Pvar.mk s curr_pname in let add_formal typestate (s, ia, typ) = - let pvar = mk_pvar s in + let pvar = mk s in let ta = let origin = TypeOrigin.Formal s in TypeAnnotation.from_item_annotation ia origin in - TypeState.add_pvar pvar (typ, ta, []) typestate in + TypeState.add pvar (typ, ta, []) typestate in let get_initial_typestate () = let typestate_empty = TypeState.empty Extension.ext in IList.fold_left add_formal typestate_empty annotated_signature.Annotations.params in diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml index b3c61a659..19fc28922 100644 --- a/infer/src/eradicate/eradicateChecks.ml +++ b/infer/src/eradicate/eradicateChecks.ml @@ -271,7 +271,7 @@ let check_constructor_initialization | None -> unknown in IList.exists (function pname, typestate -> - let pvar = Sil.mk_pvar + let pvar = Pvar.mk (Mangled.from_string (Ident.fieldname_to_string fn)) pname in filter_range_opt (TypeState.lookup_pvar pvar typestate)) diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 9fa660c73..01d9396b5 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -116,7 +116,7 @@ module ComplexExpressions = struct case_not_handled () | Sil.Dpvar pv | Sil.Dpvaraddr pv when not (Errdesc.pvar_is_frontend_tmp pv) -> - Sil.pvar_to_string pv + Pvar.to_string pv | Sil.Dpvar _ | Sil.Dpvaraddr _ (* front-end variable -- this should not happen) *) -> case_not_handled () @@ -258,11 +258,11 @@ let typecheck_instr Some (TypeAnnotation.get_origin ta) | None -> None in let handle_temporary e = match Idenv.expand_expr idenv e with - | Sil.Lvar pvar when name_is_temporary (Sil.pvar_to_string pvar) -> + | Sil.Lvar pvar when name_is_temporary (Pvar.to_string pvar) -> begin match pvar_get_origin pvar with | Some (TypeOrigin.Formal s) -> - let pvar' = Sil.mk_pvar s curr_pname in + let pvar' = Pvar.mk s curr_pname in Some (Sil.Lvar pvar') | _ -> None end @@ -295,7 +295,7 @@ let typecheck_instr TypeAnnotation.from_item_annotation ia (TypeOrigin.Field (fn, loc)), [loc] ) in - TypeState.add_pvar pvar range typestate + TypeState.add pvar range typestate | None -> typestate) in (* Convert a function call to a pvar. *) @@ -307,7 +307,7 @@ let typecheck_instr match ComplexExpressions.exp_to_string node' exp with | None -> default | Some exp_str -> - let pvar = Sil.mk_pvar (Mangled.from_string exp_str) curr_pname in + let pvar = Pvar.mk (Mangled.from_string exp_str) curr_pname in let already_defined_in_typestate = match TypeState.lookup_pvar pvar typestate with | Some (_, ta, _) -> @@ -345,27 +345,27 @@ let typecheck_instr let exp' = Idenv.expand_expr_temps idenv node _exp in let is_parameter_field pvar = (* parameter.field *) - let name = Sil.pvar_get_name pvar in + let name = Pvar.get_name pvar in let filter (s, _, _) = Mangled.equal s name in IList.exists filter annotated_signature.Annotations.params in let is_static_field pvar = (* static field *) - Sil.pvar_is_global pvar in + Pvar.is_global pvar in let pvar_to_str pvar = if Sil.exp_is_this (Sil.Lvar pvar) then "" - else Sil.pvar_to_string pvar ^ "_" in + else Pvar.to_string pvar ^ "_" in let res = match exp' with | Sil.Lvar pv when is_parameter_field pv || is_static_field pv -> let fld_name = pvar_to_str pv ^ Ident.fieldname_to_string fn in - let pvar = Sil.mk_pvar (Mangled.from_string fld_name) curr_pname in + let pvar = Pvar.mk (Mangled.from_string fld_name) curr_pname in let typestate' = update_typestate_fld pvar fn typ in (Sil.Lvar pvar, typestate') | Sil.Lfield (_exp', fn', _) when Ident.java_fieldname_is_outer_instance fn' -> (** handle double dereference when accessing a field from an outer class *) let fld_name = Ident.fieldname_to_string fn' ^ "_" ^ Ident.fieldname_to_string fn in - let pvar = Sil.mk_pvar (Mangled.from_string fld_name) curr_pname in + let pvar = Pvar.mk (Mangled.from_string fld_name) curr_pname in let typestate' = update_typestate_fld pvar fn typ in (Sil.Lvar pvar, typestate') | Sil.Lvar _ | Sil.Lfield _ when ComplexExpressions.all_nested_fields () -> @@ -373,7 +373,7 @@ let typecheck_instr begin match ComplexExpressions.exp_to_string node' exp with | Some exp_str -> - let pvar = Sil.mk_pvar (Mangled.from_string exp_str) curr_pname in + let pvar = Pvar.mk (Mangled.from_string exp_str) curr_pname in let typestate' = update_typestate_fld pvar fn typ in (Sil.Lvar pvar, typestate') | None -> @@ -430,10 +430,10 @@ let typecheck_instr else annotated_signature.Annotations.params in - let pvar_is_return pvar = + let is_return pvar = let pdesc = Cfg.Node.get_proc_desc node in let ret_pvar = Cfg.Procdesc.get_ret_var pdesc in - Sil.pvar_equal pvar ret_pvar in + Pvar.equal pvar ret_pvar in (* Apply a function to a pvar and its associated content if front-end generated. *) let pvar_apply loc handle_pvar typestate pvar = @@ -481,7 +481,7 @@ let typecheck_instr TypeState.add_id id (typecheck_expr_simple typestate' e' typ TypeOrigin.Undef loc) typestate' - | Sil.Set (Sil.Lvar pvar, _, Sil.Const (Sil.Cexn _), _) when pvar_is_return pvar -> + | Sil.Set (Sil.Lvar pvar, _, Sil.Const (Sil.Cexn _), _) when is_return pvar -> (* skip assignment to return variable where it is an artifact of a throw instruction *) typestate | Sil.Set (e1, typ, e2, loc) -> @@ -499,7 +499,7 @@ let typecheck_instr let typestate2 = match e1' with | Sil.Lvar pvar -> - TypeState.add_pvar + TypeState.add pvar (typecheck_expr_simple typestate1 e2 typ TypeOrigin.Undef loc) typestate1 @@ -655,7 +655,7 @@ let typecheck_instr (Some instr_ref) loc curr_pname end; - TypeState.add_pvar + TypeState.add pvar (t, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, [loc]) typestate'' @@ -686,7 +686,7 @@ let typecheck_instr let handle_pvar ann b typestate1 pvar = (* handle the annotation flag for pvar *) match TypeState.lookup_pvar pvar typestate1 with | Some (t, _, _) -> - TypeState.add_pvar + TypeState.add pvar (t, TypeAnnotation.const ann b TypeOrigin.ONone, [loc]) typestate1 @@ -776,8 +776,8 @@ let typecheck_instr match ComplexExpressions.exp_to_string_map_dexp convert_dexp_key_to_dexp_get node exp_key with | Some map_get_str -> - let pvar_map_get = Sil.mk_pvar (Mangled.from_string map_get_str) curr_pname in - TypeState.add_pvar + let pvar_map_get = Pvar.mk (Mangled.from_string map_get_str) curr_pname in + TypeState.add pvar_map_get (typecheck_expr_simple typestate' exp_value typ_value TypeOrigin.Undef loc) typestate' @@ -914,12 +914,12 @@ let typecheck_instr match ComplexExpressions.exp_to_string_map_dexp map_dexp node' e with | Some e_str -> let pvar = - Sil.mk_pvar (Mangled.from_string e_str) curr_pname in + Pvar.mk (Mangled.from_string e_str) curr_pname in let e1 = Sil.Lvar pvar in let (typ, ta, _) = typecheck_expr_simple typestate e1 Sil.Tvoid TypeOrigin.ONone loc in let range = (typ, ta, [loc]) in - let typestate1 = TypeState.add_pvar pvar range typestate in + let typestate1 = TypeState.add pvar range typestate in typestate1, e1, EradicateChecks.From_containsKey | None -> typestate, e, EradicateChecks.From_condition @@ -931,7 +931,7 @@ let typecheck_instr | Some (t, ta1, locs) -> if TypeAnnotation.get_value ann ta1 <> b then let ta2 = TypeAnnotation.set_value ann b ta1 in - TypeState.add_pvar pvar (t, ta2, locs) typestate' + TypeState.add pvar (t, ta2, locs) typestate' else typestate' | None -> typestate' in match e' with @@ -1090,7 +1090,7 @@ let typecheck_node if has_exceptions then typestates_exn := typestate :: !typestates_exn | Sil.Set (Sil.Lvar pv, _, _, _) when - Sil.pvar_is_return pv && + Pvar.is_return pv && Cfg.Node.get_kind node = Cfg.Node.throw_kind -> (* throw instruction *) typestates_exn := typestate :: !typestates_exn diff --git a/infer/src/eradicate/typeState.ml b/infer/src/eradicate/typeState.ml index fda950992..8dd0b4ce7 100644 --- a/infer/src/eradicate/typeState.ml +++ b/infer/src/eradicate/typeState.ml @@ -139,7 +139,7 @@ let add_id id range typestate = if map' == typestate.map then typestate else { typestate with map = map' } -let add_pvar pvar range typestate = +let add pvar range typestate = let map' = M.add (Sil.Lvar pvar) range typestate.map in if map' == typestate.map then typestate else { typestate with map = map' } diff --git a/infer/src/eradicate/typeState.mli b/infer/src/eradicate/typeState.mli index 3265d03f2..85323c0a0 100644 --- a/infer/src/eradicate/typeState.mli +++ b/infer/src/eradicate/typeState.mli @@ -31,13 +31,13 @@ type 'a t 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 +val add : Pvar.t -> range -> 'a t -> 'a t val empty : 'a ext -> 'a t val equal : 'a t -> 'a t -> bool val get_extension : 'a t -> 'a 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 lookup_pvar : Pvar.t -> 'a t -> range option val pp : 'a ext -> Format.formatter -> 'a t -> unit val range_add_locs : range -> (Location.t list) -> range val remove_id : Ident.t -> 'a t -> 'a t diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 044657033..a6e63cc48 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -122,7 +122,7 @@ let rec inhabit_typ typ cfg env = * both fresh. the only point of this is to add a descriptive local name that makes error * reports from the harness look nicer -- it's not necessary to make symbolic execution work *) let fresh_local_exp = - Sil.Lvar (Sil.mk_pvar typ_class_name (Procname.Java env.harness_name)) in + Sil.Lvar (Pvar.mk typ_class_name (Procname.Java env.harness_name)) in let write_to_local_instr = Sil.Set (fresh_local_exp, ptr_to_typ, allocated_obj_exp, env.pc) in let env' = env_add_instr write_to_local_instr [] env in diff --git a/infer/src/java/jContext.ml b/infer/src/java/jContext.ml index cfca379c6..97648c932 100644 --- a/infer/src/java/jContext.ml +++ b/infer/src/java/jContext.ml @@ -33,7 +33,7 @@ type t = { icfg : icfg; procdesc : Cfg.Procdesc.t; impl : JBir.t; - mutable var_map : (Sil.pvar * Sil.typ * Sil.typ) JBir.VarMap.t; + mutable var_map : (Pvar.t * Sil.typ * Sil.typ) JBir.VarMap.t; if_jumps : int NodeTbl.t; goto_jumps : (int, jump_kind) Hashtbl.t; cn : JBasics.class_name; @@ -84,7 +84,7 @@ let get_or_set_pvar_type context var typ = with Not_found -> let procname = (Cfg.Procdesc.get_proc_name (get_procdesc context)) in let varname = Mangled.from_string (JBir.var_name_g var) in - let pvar = Sil.mk_pvar varname procname in + let pvar = Pvar.mk varname procname in set_var_map context (JBir.VarMap.add var (pvar, typ, typ) var_map); (pvar, typ) diff --git a/infer/src/java/jContext.mli b/infer/src/java/jContext.mli index f0692be2f..6ea809c4f 100644 --- a/infer/src/java/jContext.mli +++ b/infer/src/java/jContext.mli @@ -106,7 +106,7 @@ val get_node : t -> JCode.jcode Javalib.interface_or_class val get_never_null_matcher : t -> Inferconfig.NeverReturnNull.matcher (** [set_pvar context var type] adds a variable with a type to the context *) -val set_pvar : t -> JBir.var -> Sil.typ -> Sil.pvar +val set_pvar : t -> JBir.var -> Sil.typ -> Pvar.t (** [get_var_type context var] returns the type of the variable, if the variable is in the context *) val get_var_type : t -> JBir.var -> Sil.typ option diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 6028bbf82..266ba7428 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -427,7 +427,7 @@ let rec expression context pc expr = | `String s when (JBasics.jstr_pp s) = JConfig.field_cst -> let varname = JConfig.field_st in let procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in - let pvar = Sil.mk_pvar varname procname in + let pvar = Pvar.mk varname procname in trans_var pvar | _ -> ([], [], Sil.Const (get_constant c), type_of_expr) end @@ -500,7 +500,7 @@ let rec expression context pc expr = | JBir.StaticField (cn, fs) -> let class_exp = let classname = Mangled.from_string (JBasics.cn_name cn) in - let var_name = Sil.mk_pvar_global classname in + let var_name = Pvar.mk_global classname in Sil.Lvar var_name in let (idl, instrs, sil_expr) = [], [], class_exp in let field_name = get_field_name program true tenv cn fs in @@ -781,7 +781,7 @@ let rec instruction context pc instr : translation = let program = JContext.get_program context in let meth_kind = JContext.get_meth_kind context in let proc_name = Cfg.Procdesc.get_proc_name (JContext.get_procdesc context) in - let ret_var = Sil.get_ret_pvar proc_name in + let ret_var = Pvar.get_ret_pvar proc_name in let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in let loc = get_location (JContext.get_impl context) pc meth_kind cn in let match_never_null = JContext.get_never_null_matcher context in @@ -851,7 +851,7 @@ let rec instruction context pc instr : translation = | JBir.AffectStaticField (cn, fs, e_rhs) -> let class_exp = let classname = Mangled.from_string (JBasics.cn_name cn) in - let var_name = Sil.mk_pvar_global classname in + let var_name = Pvar.mk_global classname in Sil.Lvar var_name in let (idl1, stml1, sil_expr_lhs) = [], [], class_exp in let (idl2, stml2, sil_expr_rhs, _) = expression context pc e_rhs in diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index 1270f5047..0413700d8 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -69,7 +69,7 @@ let rec trans_annotated_instructions | Ret None -> (sil_instrs, locals) | Ret (Some (tp, exp)) -> let procname = Cfg.Procdesc.get_proc_name procdesc in - let ret_var = Sil.get_ret_pvar procname in + let ret_var = Pvar.get_ret_pvar procname in let new_sil_instr = Sil.Set (Sil.Lvar ret_var, trans_typ tp, trans_operand exp, location) in (new_sil_instr :: sil_instrs, locals) diff --git a/infer/src/unit/addressTakenTests.ml b/infer/src/unit/addressTakenTests.ml index d6d458ffb..90fda4584 100644 --- a/infer/src/unit/addressTakenTests.ml +++ b/infer/src/unit/addressTakenTests.ml @@ -22,9 +22,9 @@ let tests = let int_typ = Sil.Tint IInt in let int_ptr_typ = Sil.Tptr (int_typ, Pk_pointer) in let fun_ptr_typ = Sil.Tptr (Tfun false, Pk_pointer) in - let closure_exp captured_pvars = + let closure_exp captureds = let mk_captured_var str = (Sil.Var (ident_of_str str), pvar_of_str str, int_ptr_typ) in - let captured_vars = IList.map mk_captured_var captured_pvars in + let captured_vars = IList.map mk_captured_var captureds in let closure = { Sil.name=dummy_procname; captured_vars; } in Sil.Const (Cclosure closure) in let test_list = [ diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index fc9df706b..dabe1850b 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -64,7 +64,7 @@ module StructuredSil = struct Invariant (inv_str, fresh_label ()) let pvar_of_str str = - Sil.mk_pvar (Mangled.from_string str) dummy_procname + Pvar.mk (Mangled.from_string str) dummy_procname let var_of_str str = Sil.Lvar (pvar_of_str str)