pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Refactor Sil.pvar into a separate module.

Browse Source 
Reviewed By: sblackshear

Differential Revision: D3103575

fb-gh-sync-id: 8e3a786
fbshipit-source-id: 8e3a786
master
Cristiano Calcagno 9 years ago committed by Facebook Github Bot 6
parent 53702e43e8
commit 509a666ee0
59 changed files with 1361 additions and 935 deletions
Show Stats Download Patch File Download Diff File

68
infer/src/IR/cfg.ml
Unescape View File

@ -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), _, _

8
infer/src/IR/cfg.mli
Unescape View File

@ -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

213
infer/src/IR/pvar.ml
Unescape View File

@ -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 -> "&amp;"
| 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) }

97
infer/src/IR/pvar.mli
Unescape View File

@ -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

308
infer/src/IR/sil.ml
Unescape View File

@ -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 -> "&amp;"
| 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")

116
infer/src/IR/sil.mli
Unescape View File

@ -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

18
infer/src/backend/abs.ml
Unescape View File

@ -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

6
infer/src/backend/autounit.ml
Unescape View File

@ -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 () =

4
infer/src/backend/buckets.ml
Unescape View File

@ -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;

4
infer/src/backend/dom.ml
Unescape View File

@ -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)

8
infer/src/backend/dotty.ml
Unescape View File

@ -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"

216
infer/src/backend/errdesc.ml
Unescape View File

@ -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 =

16
infer/src/backend/errdesc.mli
Unescape View File

@ -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

10
infer/src/backend/interproc.ml
Unescape View File

@ -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

10
infer/src/backend/localise.ml
Unescape View File

@ -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 "

5
infer/src/backend/localise.mli
Unescape View File

@ -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

119
infer/src/backend/preanal.ml
Unescape View File

@ -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 "@."
*)

4
infer/src/backend/printer.ml
Unescape View File

@ -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

222
infer/src/backend/prop.ml
Unescape View File

@ -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 "@,@[<h>%a@]" (pp_hpara_simple pe env n) hpara in
let iter_f_dll n hpara_dll = F.fprintf f "@,@[<h>%a@]" (pp_hpara_dll_simple pe env n) hpara_dll in
let iter_f_dll n hpara_dll =
F.fprintf f "@,@[<h>%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<e] return [n,e] *)
let atom_const_lt_exp = function
| Sil.Aeq(Sil.BinOp (Sil.Lt, Sil.Const (Sil.Cint n), e1), Sil.Const (Sil.Cint i)) when Sil.Int.isone i ->
| 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 =

34
infer/src/backend/prop.mli
Unescape View File

@ -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

14
infer/src/backend/prover.ml
Unescape View File

@ -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

10
infer/src/backend/rearrange.ml
Unescape View File

@ -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 *)

24
infer/src/backend/symExec.ml
Unescape View File

@ -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

235
infer/src/backend/tabulation.ml
Unescape View File

@ -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) =

6
infer/src/checkers/addressTaken.ml
Unescape View File

@ -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)

2
infer/src/checkers/annotations.ml
Unescape View File

@ -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. *)

2
infer/src/checkers/annotations.mli
Unescape View File

@ -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 :

4
infer/src/checkers/checkTraceCallSequence.ml
Unescape View File

@ -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

4
infer/src/checkers/checkers.ml
Unescape View File

@ -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

16
infer/src/checkers/copyPropagation.ml
Unescape View File

@ -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 *)

6
infer/src/checkers/dataflow.ml
Unescape View File

@ -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), _, _, _)

6
infer/src/checkers/patternMatch.ml
Unescape View File

@ -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

4
infer/src/checkers/patternMatch.mli
Unescape View File

@ -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

6
infer/src/clang/cContext.ml
Unescape View File

@ -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

6
infer/src/clang/cContext.mli
Unescape View File

@ -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

2
infer/src/clang/cFrontend_checkers.ml
Unescape View File

@ -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

2
infer/src/clang/cFrontend_checkers.mli
Unescape View File

@ -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

12
infer/src/clang/cFrontend_utils.ml
Unescape View File

@ -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

32
infer/src/clang/cFrontend_utils.mli
Unescape View File

@ -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

4
infer/src/clang/cMethod_trans.ml
Unescape View File

@ -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

2
infer/src/clang/cMethod_trans.mli
Unescape View File

@ -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

2
infer/src/clang/cModule_type.ml
Unescape View File

@ -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

287
infer/src/clang/cTrans.ml
Unescape View File

@ -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,8 +149,11 @@ 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;
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) =
@ -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(<type pf a>) *)
(* 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(<type pf a>) *)
(* 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
@ -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
@ -1506,7 +1567,8 @@ struct
| [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
@ -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
@ -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)

4
infer/src/clang/cTrans_utils.ml
Unescape View File

@ -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

2
infer/src/clang/cTrans_utils.mli
Unescape View File

@ -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 :

8
infer/src/clang/cVar_decl.ml
Unescape View File

@ -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)

8
infer/src/clang/cVar_decl.mli
Unescape View File

@ -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

6
infer/src/eradicate/eradicate.ml
Unescape View File

@ -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

2
infer/src/eradicate/eradicateChecks.ml
Unescape View File

@ -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))

46
infer/src/eradicate/typeCheck.ml
Unescape View File

@ -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

2
infer/src/eradicate/typeState.ml
Unescape View File

@ -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' }

4
infer/src/eradicate/typeState.mli
Unescape View File

@ -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

2
infer/src/harness/inhabit.ml
Unescape View File

@ -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

4
infer/src/java/jContext.ml
Unescape View File

@ -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)

2
infer/src/java/jContext.mli
Unescape View File

@ -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

8
infer/src/java/jTrans.ml
Unescape View File

@ -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

2
infer/src/llvm/lTrans.ml
Unescape View File

@ -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)

4
infer/src/unit/addressTakenTests.ml
Unescape View File

@ -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 = [

2
infer/src/unit/analyzerTester.ml
Unescape View File

@ -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)

Write Preview
Loading…
Cancel
Save