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

Refactor Sil.dexp into separate DecompExp module

Browse Source 
Summary: Move Sil.dexp type and operations into separate DecompExp module.

Reviewed By: dulmarod

Differential Revision: D3548095

fbshipit-source-id: 5ab4360
master
Josh Berdine 9 years ago committed by Facebook Github Bot 7
parent ccd32690d7
commit e739b0e6ea
14 changed files with 360 additions and 315 deletions
Show Stats Download Patch File Download Diff File

179
infer/src/IR/DecompiledExp.re
Unescape View File

@ -0,0 +1,179 @@
/*
* vim: set ft=rust:
* vim: set ft=reason:
*
* 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.
*/
open! Utils;
/** The Smallfoot Intermediate Language: Decompiled Expressions */
let module L = Logging;
let module F = Format;
/** expression representing the result of decompilation */
type t =
| Darray of t t
| Dbinop of Binop.t t t
| Dconst of Const.t
| Dsizeof of Typ.t (option t) Subtype.t
| Dderef of t
| Dfcall of t (list t) Location.t CallFlags.t
| Darrow of t Ident.fieldname
| Ddot of t Ident.fieldname
| Dpvar of Pvar.t
| Dpvaraddr of Pvar.t
| Dunop of Unop.t t
| Dunknown
| Dretcall of t (list t) Location.t CallFlags.t;
/** Value paths: identify an occurrence of a value in a symbolic heap
each expression represents a path, with Dpvar being the simplest one */
type vpath = option t;
let java () => !Config.curr_language == Config.Java;
let eradicate_java () => Config.eradicate && java ();
/** convert a dexp to a string */
let rec to_string =
fun
| Darray de1 de2 => to_string de1 ^ "[" ^ to_string de2 ^ "]"
| Dbinop op de1 de2 => "(" ^ to_string de1 ^ Binop.str pe_text op ^ to_string de2 ^ ")"
| Dconst (Cfun pn) => Procname.to_simplified_string pn
| Dconst c => Const.to_string c
| Dderef de => "*" ^ to_string de
| Dfcall fun_dexp args _ {cf_virtual: isvirtual} => {
let pp_arg fmt de => F.fprintf fmt "%s" (to_string de);
let pp_args fmt des =>
if (eradicate_java ()) {
if (des != []) {
F.fprintf fmt "..."
}
} else {
pp_comma_seq pp_arg fmt des
};
let pp_fun fmt => (
fun
| Dconst (Cfun pname) => {
let s =
switch pname {
| Procname.Java pname_java => Procname.java_get_method pname_java
| _ => Procname.to_string pname
};
F.fprintf fmt "%s" s
}
| de => F.fprintf fmt "%s" (to_string de)
);
let (receiver, args') =
switch args {
| [Dpvar pv, ...args'] when isvirtual && Pvar.is_this pv => (None, args')
| [a, ...args'] when isvirtual => (Some a, args')
| _ => (None, args)
};
let pp fmt () => {
let pp_receiver fmt => (
fun
| None => ()
| Some arg => F.fprintf fmt "%a." pp_arg arg
);
F.fprintf fmt "%a%a(%a)" pp_receiver receiver pp_fun fun_dexp pp_args args'
};
pp_to_string pp ()
}
| 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) {
to_string de
} else if (java ()) {
to_string de ^ "." ^ Ident.fieldname_to_flat_string f
} else {
to_string de ^ "->" ^ Ident.fieldname_to_string f
}
| Ddot (Dpvar _) fe when eradicate_java () =>
/* static field access */
Ident.fieldname_to_simplified_string fe
| Ddot de f =>
if (Ident.fieldname_is_hidden f) {
"&" ^ to_string de
} else if (java ()) {
to_string de ^ "." ^ Ident.fieldname_to_flat_string f
} else {
to_string de ^ "." ^ Ident.fieldname_to_string f
}
| Dpvar pv => Mangled.to_string (Pvar.get_name pv)
| Dpvaraddr pv => {
let s =
if (eradicate_java ()) {
Pvar.get_simplified_name pv
} else {
Mangled.to_string (Pvar.get_name pv)
};
let ampersand =
if (eradicate_java ()) {
""
} else {
"&"
};
ampersand ^ s
}
| Dunop op de => Unop.str op ^ to_string de
| Dsizeof typ _ _ => pp_to_string (Typ.pp_full pe_text) typ
| Dunknown => "unknown"
| Dretcall de _ _ _ => "returned by " ^ to_string de;
/** Pretty print a dexp. */
let pp fmt de => F.fprintf fmt "%s" (to_string de);
/** Pretty print a value path */
let pp_vpath pe fmt vpath => {
let pp fmt =>
fun
| Some de => pp fmt de
| None => ();
if (pe.pe_kind === PP_HTML) {
F.fprintf
fmt
" %a{vpath: %a}%a"
Io_infer.Html.pp_start_color
Orange
pp
vpath
Io_infer.Html.pp_end_color
()
} else {
F.fprintf fmt "%a" pp vpath
}
};
let rec has_tmp_var =
fun
| Dpvar pvar
| Dpvaraddr pvar => Pvar.is_frontend_tmp pvar
| Dderef dexp
| Ddot dexp _
| Darrow dexp _
| Dunop _ dexp
| Dsizeof _ (Some dexp) _ => has_tmp_var dexp
| Darray dexp1 dexp2
| Dbinop _ dexp1 dexp2 => has_tmp_var dexp1 || has_tmp_var dexp2
| Dretcall dexp dexp_list _ _
| Dfcall dexp dexp_list _ _ => has_tmp_var dexp || IList.exists has_tmp_var dexp_list
| Dconst _
| Dunknown
| Dsizeof _ None _ => false;

58
infer/src/IR/DecompiledExp.rei
Unescape View File

@ -0,0 +1,58 @@
/*
* vim: set ft=rust:
* vim: set ft=reason:
*
* 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.
*/
open! Utils;
/** The Smallfoot Intermediate Language: Decompiled Expressions */
let module L = Logging;
let module F = Format;
/** expression representing the result of decompilation */
type t =
| Darray of t t
| Dbinop of Binop.t t t
| Dconst of Const.t
| Dsizeof of Typ.t (option t) Subtype.t
| Dderef of t
| Dfcall of t (list t) Location.t CallFlags.t
| Darrow of t Ident.fieldname
| Ddot of t Ident.fieldname
| Dpvar of Pvar.t
| Dpvaraddr of Pvar.t
| Dunop of Unop.t t
| Dunknown
| Dretcall of t (list t) Location.t CallFlags.t;
/** Value paths: identify an occurrence of a value in a symbolic heap
each expression represents a path, with Dpvar being the simplest one */
type vpath = option t;
/** convert to a string */
let to_string: t => string;
/** pretty print */
let pp: F.formatter => t => unit;
/** Pretty print a value path */
let pp_vpath: printenv => F.formatter => vpath => unit;
/** return true if [dexp] contains a temporary pvar */
let has_tmp_var: t => bool;

163
infer/src/IR/Sil.re
Unescape View File

@ -75,35 +75,13 @@ type taint_kind =
type taint_info = {taint_source: Procname.t, taint_kind: taint_kind}; type taint_info = {taint_source: Procname.t, taint_kind: taint_kind};
/** expression representing the result of decompilation */
type dexp =
| Darray of dexp dexp
| Dbinop of Binop.t dexp dexp
| Dconst of Const.t
| Dsizeof of Typ.t (option dexp) Subtype.t
| Dderef of dexp
| Dfcall of dexp (list dexp) Location.t CallFlags.t
| Darrow of dexp Ident.fieldname
| Ddot of dexp Ident.fieldname
| Dpvar of Pvar.t
| Dpvaraddr of Pvar.t
| Dunop of Unop.t dexp
| Dunknown
| Dretcall of dexp (list dexp) Location.t CallFlags.t;
/** Value paths: identify an occurrence of a value in a symbolic heap
each expression represents a path, with Dpvar being the simplest one */
type vpath = option dexp;
/** acquire/release action on a resource */ /** acquire/release action on a resource */
type res_action = { type res_action = {
ra_kind: res_act_kind, /** kind of action */ ra_kind: res_act_kind, /** kind of action */
ra_res: resource, /** kind of resource */ ra_res: resource, /** kind of resource */
ra_pname: Procname.t, /** name of the procedure used to acquire/release the resource */ ra_pname: Procname.t, /** name of the procedure used to acquire/release the resource */
ra_loc: Location.t, /** location of the acquire/release */ ra_loc: Location.t, /** location of the acquire/release */
ra_vpath: vpath /** vpath of the resource value */ ra_vpath: DecompiledExp.vpath /** vpath of the resource value */
}; };
@ -508,23 +486,6 @@ let attr_is_undef =
| Aundef _ => true | Aundef _ => true
| _ => false; | _ => false;
let rec dexp_has_tmp_var =
fun
| Dpvar pvar
| Dpvaraddr pvar => Pvar.is_frontend_tmp pvar
| Dderef dexp
| Ddot dexp _
| Darrow dexp _
| Dunop _ dexp
| Dsizeof _ (Some dexp) _ => dexp_has_tmp_var dexp
| Darray dexp1 dexp2
| Dbinop _ dexp1 dexp2 => dexp_has_tmp_var dexp1 || dexp_has_tmp_var dexp2
| Dretcall dexp dexp_list _ _
| Dfcall dexp dexp_list _ _ => dexp_has_tmp_var dexp || IList.exists dexp_has_tmp_var dexp_list
| Dconst _
| Dunknown
| Dsizeof _ None _ => false;
let attribute_compare (att1: attribute) (att2: attribute) :int => let attribute_compare (att1: attribute) (att2: attribute) :int =>
switch (att1, att2) { switch (att1, att2) {
| (Aresource ra1, Aresource ra2) => | (Aresource ra1, Aresource ra2) =>
@ -1015,126 +976,6 @@ let pp_seq_diff pp pe0 f =>
doit doit
}; };
let java () => !Config.curr_language == Config.Java;
let eradicate_java () => Config.eradicate && java ();
/** convert a dexp to a string */
let rec dexp_to_string =
fun
| Darray de1 de2 => dexp_to_string de1 ^ "[" ^ dexp_to_string de2 ^ "]"
| Dbinop op de1 de2 => "(" ^ dexp_to_string de1 ^ Binop.str pe_text op ^ dexp_to_string de2 ^ ")"
| Dconst (Cfun pn) => Procname.to_simplified_string pn
| Dconst c => Const.to_string c
| Dderef de => "*" ^ dexp_to_string de
| Dfcall fun_dexp args _ {cf_virtual: isvirtual} => {
let pp_arg fmt de => F.fprintf fmt "%s" (dexp_to_string de);
let pp_args fmt des =>
if (eradicate_java ()) {
if (des != []) {
F.fprintf fmt "..."
}
} else {
pp_comma_seq pp_arg fmt des
};
let pp_fun fmt => (
fun
| Dconst (Cfun pname) => {
let s =
switch pname {
| Procname.Java pname_java => Procname.java_get_method pname_java
| _ => Procname.to_string pname
};
F.fprintf fmt "%s" s
}
| de => F.fprintf fmt "%s" (dexp_to_string de)
);
let (receiver, args') =
switch args {
| [Dpvar pv, ...args'] when isvirtual && Pvar.is_this pv => (None, args')
| [a, ...args'] when isvirtual => (Some a, args')
| _ => (None, args)
};
let pp fmt () => {
let pp_receiver fmt => (
fun
| None => ()
| Some arg => F.fprintf fmt "%a." pp_arg arg
);
F.fprintf fmt "%a%a(%a)" pp_receiver receiver pp_fun fun_dexp pp_args args'
};
pp_to_string pp ()
}
| 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) {
dexp_to_string de
} else if (java ()) {
dexp_to_string de ^ "." ^ Ident.fieldname_to_flat_string f
} else {
dexp_to_string de ^ "->" ^ Ident.fieldname_to_string f
}
| Ddot (Dpvar _) fe when eradicate_java () =>
/* static field access */
Ident.fieldname_to_simplified_string fe
| Ddot de f =>
if (Ident.fieldname_is_hidden f) {
"&" ^ dexp_to_string de
} else if (java ()) {
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)
| Dpvaraddr pv => {
let s =
if (eradicate_java ()) {
Pvar.get_simplified_name pv
} else {
Mangled.to_string (Pvar.get_name pv)
};
let ampersand =
if (eradicate_java ()) {
""
} else {
"&"
};
ampersand ^ s
}
| Dunop op de => Unop.str op ^ dexp_to_string de
| Dsizeof typ _ _ => pp_to_string (Typ.pp_full pe_text) typ
| Dunknown => "unknown"
| Dretcall de _ _ _ => "returned by " ^ dexp_to_string de;
/** Pretty print a dexp. */
let pp_dexp fmt de => F.fprintf fmt "%s" (dexp_to_string de);
/** Pretty print a value path */
let pp_vpath pe fmt vpath => {
let pp fmt =>
fun
| Some de => pp_dexp fmt de
| None => ();
if (pe.pe_kind === PP_HTML) {
F.fprintf
fmt
" %a{vpath: %a}%a"
Io_infer.Html.pp_start_color
Orange
pp
vpath
Io_infer.Html.pp_end_color
()
} else {
F.fprintf fmt "%a" pp vpath
}
};
/** convert the attribute to a string */ /** convert the attribute to a string */
let attribute_to_string pe => let attribute_to_string pe =>
@ -1159,7 +1000,7 @@ let attribute_to_string pe =>
}; };
let str_vpath = let str_vpath =
if Config.trace_error { if Config.trace_error {
pp_to_string (pp_vpath pe) ra.ra_vpath pp_to_string (DecompiledExp.pp_vpath pe) ra.ra_vpath
} else { } else {
"" ""
}; };

40
infer/src/IR/Sil.rei
Unescape View File

@ -63,35 +63,13 @@ type taint_kind =
type taint_info = {taint_source: Procname.t, taint_kind: taint_kind}; type taint_info = {taint_source: Procname.t, taint_kind: taint_kind};
/** expression representing the result of decompilation */
type dexp =
| Darray of dexp dexp
| Dbinop of Binop.t dexp dexp
| Dconst of Const.t
| Dsizeof of Typ.t (option dexp) Subtype.t
| Dderef of dexp
| Dfcall of dexp (list dexp) Location.t CallFlags.t
| Darrow of dexp Ident.fieldname
| Ddot of dexp Ident.fieldname
| Dpvar of Pvar.t
| Dpvaraddr of Pvar.t
| Dunop of Unop.t dexp
| Dunknown
| Dretcall of dexp (list dexp) Location.t CallFlags.t;
/** Value paths: identify an occurrence of a value in a symbolic heap
each expression represents a path, with Dpvar being the simplest one */
type vpath = option dexp;
/** acquire/release action on a resource */ /** acquire/release action on a resource */
type res_action = { type res_action = {
ra_kind: res_act_kind, /** kind of action */ ra_kind: res_act_kind, /** kind of action */
ra_res: resource, /** kind of resource */ ra_res: resource, /** kind of resource */
ra_pname: Procname.t, /** name of the procedure used to acquire/release the resource */ ra_pname: Procname.t, /** name of the procedure used to acquire/release the resource */
ra_loc: Location.t, /** location of the acquire/release */ ra_loc: Location.t, /** location of the acquire/release */
ra_vpath: vpath /** vpath of the resource value */ ra_vpath: DecompiledExp.vpath /** vpath of the resource value */
}; };
@ -417,10 +395,6 @@ let is_block_pvar: Pvar.t => bool;
the function raises an exception by calling "assert false". */ the function raises an exception by calling "assert false". */
let binop_invert: Binop.t => exp => exp => exp; let binop_invert: Binop.t => exp => exp => exp;
/** return true if [dexp] contains a temporary pvar */
let dexp_has_tmp_var: dexp => bool;
let mem_kind_compare: mem_kind => mem_kind => int; let mem_kind_compare: mem_kind => mem_kind => int;
let attribute_compare: attribute => attribute => int; let attribute_compare: attribute => attribute => int;
@ -533,14 +507,6 @@ let mem_dealloc_pname: mem_kind => Procname.t;
let attribute_to_string: printenv => attribute => string; let attribute_to_string: printenv => attribute => string;
/** convert a dexp to a string */
let dexp_to_string: dexp => string;
/** Pretty print a dexp. */
let pp_dexp: F.formatter => dexp => unit;
/** Pretty print an expression. */ /** Pretty print an expression. */
let pp_exp: printenv => F.formatter => exp => unit; let pp_exp: printenv => F.formatter => exp => unit;
@ -617,10 +583,6 @@ let pp_instr_list: printenv => F.formatter => list instr => unit;
let d_instr_list: list instr => unit; let d_instr_list: list instr => unit;
/** Pretty print a value path */
let pp_vpath: printenv => F.formatter => vpath => unit;
/** Pretty print an atom. */ /** Pretty print an atom. */
let pp_atom: printenv => F.formatter => atom => unit; let pp_atom: printenv => F.formatter => atom => unit;

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

@ -1022,7 +1022,7 @@ let cycle_has_weak_or_unretained_or_assign_field cycle =
let check_observer_is_unsubscribed_deallocation prop e = let check_observer_is_unsubscribed_deallocation prop e =
let pvar_opt = match Prop.get_resource_attribute prop e with let pvar_opt = match Prop.get_resource_attribute prop e with
| Some (Sil.Aresource ({Sil.ra_vpath = Some (Sil.Dpvar pvar) })) -> Some pvar | Some (Sil.Aresource ({Sil.ra_vpath = Some (DecompiledExp.Dpvar pvar) })) -> Some pvar
| _ -> None in | _ -> None in
let loc = State.get_loc () in let loc = State.get_loc () in
match Prop.get_observer_attribute prop e with match Prop.get_observer_attribute prop e with

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

@ -124,7 +124,7 @@ let check_access access_opt de_opt =
| _ -> | _ ->
begin begin
match de_opt with match de_opt with
| Some (Sil.Dconst _) -> | Some (DecompiledExp.Dconst _) ->
Some Localise.BucketLevel.b1 Some Localise.BucketLevel.b1
| _ -> None | _ -> None
end end

3
infer/src/backend/buckets.mli
Unescape View File

@ -14,4 +14,5 @@ open! Utils
(** Classify the bucket of an error desc using Location.access and nullable information *) (** Classify the bucket of an error desc using Location.access and nullable information *)
val classify_access : val classify_access :
Localise.error_desc -> Localise.access option -> Sil.dexp option -> bool -> Localise.error_desc Localise.error_desc -> Localise.access option -> DecompiledExp.t option -> bool ->
Localise.error_desc

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

@ -14,6 +14,7 @@ open! Utils
module L = Logging module L = Logging
module F = Format module F = Format
module DExp = DecompiledExp
let smart_pointers = [ let smart_pointers = [
["std"; "shared_ptr"]; ["std"; "shared_ptr"];
@ -217,7 +218,7 @@ let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option =
(** Find the Letderef instruction used to declare normal variable [id], (** Find the Letderef instruction used to declare normal variable [id],
and return the expression dereferenced to initialize [id] *) and return the expression dereferenced to initialize [id] *)
let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp option = let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : DExp.t option =
let is_infer = not (Config.checkers || Config.eradicate) in let is_infer = not (Config.checkers || Config.eradicate) in
let find_declaration node = function let find_declaration node = function
| Sil.Letderef (id0, e, _, _) when Ident.equal id id0 -> | Sil.Letderef (id0, e, _, _) when Ident.equal id id0 ->
@ -240,7 +241,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
(L.d_str "find_normal_variable_letderef function call "; (L.d_str "find_normal_variable_letderef function call ";
Sil.d_exp fun_exp; L.d_ln ()); Sil.d_exp fun_exp; L.d_ln ());
let fun_dexp = Sil.Dconst (Const.Cfun pname) in let fun_dexp = DExp.Dconst (Const.Cfun pname) in
let args_dexp = let args_dexp =
let args_dexpo = IList.map (fun (e, _) -> _exp_rv_dexp seen node e) args in let args_dexpo = IList.map (fun (e, _) -> _exp_rv_dexp seen node e) args in
if IList.exists (fun x -> x = None) args_dexpo if IList.exists (fun x -> x = None) args_dexpo
@ -248,7 +249,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
else else
let unNone = function Some x -> x | None -> assert false in let unNone = function Some x -> x | None -> assert false in
IList.map unNone args_dexpo in IList.map unNone args_dexpo in
Some (Sil.Dretcall (fun_dexp, args_dexp, loc, call_flags)) Some (DExp.Dretcall (fun_dexp, args_dexp, loc, call_flags))
| Sil.Set (Sil.Lvar pvar, _, Sil.Var id0, _) | Sil.Set (Sil.Lvar pvar, _, Sil.Var id0, _)
when is_infer && Ident.equal id id0 && not (Pvar.is_frontend_tmp pvar) -> when is_infer && Ident.equal id id0 && not (Pvar.is_frontend_tmp pvar) ->
(* this case is a hack to make bucketing continue to work in the presence of copy (* this case is a hack to make bucketing continue to work in the presence of copy
@ -256,7 +257,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
n1 = foo(); x = n1; n2 = x; n2.toString(), but copy-propagation will optimize this to: n1 = foo(); x = n1; n2 = x; n2.toString(), but copy-propagation will optimize this to:
n1 = foo(); x = n1; n1.toString(). This case allows us to recognize the association n1 = foo(); x = n1; n1.toString(). This case allows us to recognize the association
between n1 and x. Eradicate/checkers don't use copy-prop, so they don't need this. *) between n1 and x. Eradicate/checkers don't use copy-prop, so they don't need this. *)
Some (Sil.Dpvar pvar) Some (DExp.Dpvar pvar)
| _ -> None in | _ -> None in
let res = find_in_node_or_preds node find_declaration in let res = find_in_node_or_preds node find_declaration in
if verbose && res == None if verbose && res == None
@ -270,7 +271,7 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : Sil.dexp
res res
(** describe lvalue [e] as a dexp *) (** describe lvalue [e] as a dexp *)
and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : DExp.t option =
if Sil.ExpSet.mem e _seen then if Sil.ExpSet.mem e _seen then
(L.d_str "exp_lv_dexp: cycle detected"; Sil.d_exp e; L.d_ln (); None) (L.d_str "exp_lv_dexp: cycle detected"; Sil.d_exp e; L.d_ln (); None)
else else
@ -278,17 +279,17 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
match Prop.exp_normalize_noabs Sil.sub_empty e with match Prop.exp_normalize_noabs Sil.sub_empty e with
| Sil.Const c -> | Sil.Const c ->
if verbose then (L.d_str "exp_lv_dexp: constant "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_lv_dexp: constant "; Sil.d_exp e; L.d_ln ());
Some (Sil.Dderef (Sil.Dconst c)) Some (DExp.Dderef (DExp.Dconst c))
| Sil.BinOp(Binop.PlusPI, e1, e2) -> | Sil.BinOp(Binop.PlusPI, e1, e2) ->
if verbose then (L.d_str "exp_lv_dexp: (e1 +PI e2) "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_lv_dexp: (e1 +PI e2) "; Sil.d_exp e; L.d_ln ());
(match _exp_lv_dexp seen node e1, _exp_rv_dexp seen node e2 with (match _exp_lv_dexp seen node e1, _exp_rv_dexp seen node e2 with
| Some de1, Some de2 -> Some (Sil.Dbinop(Binop.PlusPI, de1, de2)) | Some de1, Some de2 -> Some (DExp.Dbinop(Binop.PlusPI, de1, de2))
| _ -> None) | _ -> None)
| Sil.Var id when Ident.is_normal id -> | Sil.Var id when Ident.is_normal id ->
if verbose then (L.d_str "exp_lv_dexp: normal var "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_lv_dexp: normal var "; Sil.d_exp e; L.d_ln ());
(match _find_normal_variable_letderef seen node id with (match _find_normal_variable_letderef seen node id with
| None -> None | None -> None
| Some de -> Some (Sil.Dderef de)) | Some de -> Some (DExp.Dderef de))
| Sil.Lvar pvar -> | Sil.Lvar pvar ->
if verbose then (L.d_str "exp_lv_dexp: program var "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_lv_dexp: program var "; Sil.d_exp e; L.d_ln ());
if Pvar.is_frontend_tmp pvar then if Pvar.is_frontend_tmp pvar then
@ -298,7 +299,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
begin begin
match find_struct_by_value_assignment node pvar with match find_struct_by_value_assignment node pvar with
| Some (_, pname, loc, call_flags) -> | Some (_, pname, loc, call_flags) ->
Some (Sil.Dfcall (Sil.Dconst (Cfun pname), [], loc, call_flags)) Some (DExp.Dfcall (DExp.Dconst (Cfun pname), [], loc, call_flags))
| None -> | None ->
None None
end end
@ -312,12 +313,12 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
else else
let unNone = function Some x -> x | None -> assert false in let unNone = function Some x -> x | None -> assert false in
let args = IList.map unNone blame_args in let args = IList.map unNone blame_args in
Some (Sil.Dfcall (unNone fun_dexpo, args, loc, call_flags)) Some (DExp.Dfcall (unNone fun_dexpo, args, loc, call_flags))
| None -> | None ->
_exp_rv_dexp seen node' (Sil.Var id) _exp_rv_dexp seen node' (Sil.Var id)
end end
end end
else Some (Sil.Dpvar pvar) else Some (DExp.Dpvar pvar)
| Sil.Lfield (Sil.Var id, f, _) when Ident.is_normal id -> | Sil.Lfield (Sil.Var id, f, _) when Ident.is_normal id ->
if verbose then if verbose then
begin begin
@ -328,7 +329,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
end; end;
(match _find_normal_variable_letderef seen node id with (match _find_normal_variable_letderef seen node id with
| None -> None | None -> None
| Some de -> Some (Sil.Darrow (de, f))) | Some de -> Some (DExp.Darrow (de, f)))
| Sil.Lfield (e1, f, _) -> | Sil.Lfield (e1, f, _) ->
if verbose then if verbose then
begin begin
@ -339,7 +340,7 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
end; end;
(match _exp_lv_dexp seen node e1 with (match _exp_lv_dexp seen node e1 with
| None -> None | None -> None
| Some de -> Some (Sil.Ddot (de, f))) | Some de -> Some (DExp.Ddot (de, f)))
| Sil.Lindex (e1, e2) -> | Sil.Lindex (e1, e2) ->
if verbose then if verbose then
begin begin
@ -353,14 +354,14 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
| None, _ -> None | None, _ -> None
| Some de1, None -> | Some de1, None ->
(* even if the index is unknown, the array info is useful for bound errors *) (* even if the index is unknown, the array info is useful for bound errors *)
Some (Sil.Darray (de1, Sil.Dunknown)) Some (DExp.Darray (de1, DExp.Dunknown))
| Some de1, Some de2 -> Some (Sil.Darray (de1, de2))) | Some de1, Some de2 -> Some (DExp.Darray (de1, de2)))
| _ -> | _ ->
if verbose then (L.d_str "exp_lv_dexp: no match for "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_lv_dexp: no match for "; Sil.d_exp e; L.d_ln ());
None None
(** describe rvalue [e] as a dexp *) (** describe rvalue [e] as a dexp *)
and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option = and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : DExp.t option =
if Sil.ExpSet.mem e _seen then if Sil.ExpSet.mem e _seen then
(L.d_str "exp_rv_dexp: cycle detected"; Sil.d_exp e; L.d_ln (); None) (L.d_str "exp_rv_dexp: cycle detected"; Sil.d_exp e; L.d_ln (); None)
else else
@ -368,12 +369,12 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
match e with match e with
| Sil.Const c -> | Sil.Const c ->
if verbose then (L.d_str "exp_rv_dexp: constant "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: constant "; Sil.d_exp e; L.d_ln ());
Some (Sil.Dconst c) Some (DExp.Dconst c)
| Sil.Lvar pv -> | Sil.Lvar pv ->
if verbose then (L.d_str "exp_rv_dexp: program var "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: program var "; Sil.d_exp e; L.d_ln ());
if Pvar.is_frontend_tmp pv if Pvar.is_frontend_tmp pv
then _exp_lv_dexp _seen (* avoid spurious cycle detection *) node e then _exp_lv_dexp _seen (* avoid spurious cycle detection *) node e
else Some (Sil.Dpvaraddr pv) else Some (DExp.Dpvaraddr pv)
| Sil.Var id when Ident.is_normal id -> | Sil.Var id when Ident.is_normal id ->
if verbose then (L.d_str "exp_rv_dexp: normal var "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: normal var "; Sil.d_exp e; L.d_ln ());
_find_normal_variable_letderef seen node id _find_normal_variable_letderef seen node id
@ -387,7 +388,7 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
end; end;
(match _exp_rv_dexp seen node e1 with (match _exp_rv_dexp seen node e1 with
| None -> None | None -> None
| Some de -> Some (Sil.Ddot(de, f))) | Some de -> Some (DExp.Ddot(de, f)))
| Sil.Lindex (e1, e2) -> | Sil.Lindex (e1, e2) ->
if verbose then if verbose then
begin begin
@ -399,23 +400,23 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : Sil.dexp option =
end; end;
(match _exp_rv_dexp seen node e1, _exp_rv_dexp seen node e2 with (match _exp_rv_dexp seen node e1, _exp_rv_dexp seen node e2 with
| None, _ | _, None -> None | None, _ | _, None -> None
| Some de1, Some de2 -> Some (Sil.Darray(de1, de2))) | Some de1, Some de2 -> Some (DExp.Darray(de1, de2)))
| Sil.BinOp (op, e1, e2) -> | Sil.BinOp (op, e1, e2) ->
if verbose then (L.d_str "exp_rv_dexp: BinOp "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: BinOp "; Sil.d_exp e; L.d_ln ());
(match _exp_rv_dexp seen node e1, _exp_rv_dexp seen node e2 with (match _exp_rv_dexp seen node e1, _exp_rv_dexp seen node e2 with
| None, _ | _, None -> None | None, _ | _, None -> None
| Some de1, Some de2 -> Some (Sil.Dbinop (op, de1, de2))) | Some de1, Some de2 -> Some (DExp.Dbinop (op, de1, de2)))
| Sil.UnOp (op, e1, _) -> | Sil.UnOp (op, e1, _) ->
if verbose then (L.d_str "exp_rv_dexp: UnOp "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: UnOp "; Sil.d_exp e; L.d_ln ());
(match _exp_rv_dexp seen node e1 with (match _exp_rv_dexp seen node e1 with
| None -> None | None -> None
| Some de1 -> Some (Sil.Dunop (op, de1))) | Some de1 -> Some (DExp.Dunop (op, de1)))
| Sil.Cast (_, e1) -> | Sil.Cast (_, e1) ->
if verbose then (L.d_str "exp_rv_dexp: Cast "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: Cast "; Sil.d_exp e; L.d_ln ());
_exp_rv_dexp seen node e1 _exp_rv_dexp seen node e1
| Sil.Sizeof (typ, len, sub) -> | Sil.Sizeof (typ, len, sub) ->
if verbose then (L.d_str "exp_rv_dexp: type "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: type "; Sil.d_exp e; L.d_ln ());
Some (Sil.Dsizeof (typ, Option.map_default (_exp_rv_dexp seen node) None len, sub)) Some (DExp.Dsizeof (typ, Option.map_default (_exp_rv_dexp seen node) None len, sub))
| _ -> | _ ->
if verbose then (L.d_str "exp_rv_dexp: no match for "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: no match for "; Sil.d_exp e; L.d_ln ());
None None
@ -507,8 +508,8 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
Some desc_string Some desc_string
end end
else match vpath with else match vpath with
| Some de when not (Sil.dexp_has_tmp_var de) -> | Some de when not (DExp.has_tmp_var de) ->
Some (Sil.dexp_to_string de) Some (DExp.to_string de)
| _ -> None in | _ -> None in
let res_action_opt, resource_opt, vpath = match alloc_att_opt with let res_action_opt, resource_opt, vpath = match alloc_att_opt with
| Some (Sil.Aresource ({ Sil.ra_kind = Sil.Racquire } as ra)) -> | Some (Sil.Aresource ({ Sil.ra_kind = Sil.Racquire } as ra)) ->
@ -541,7 +542,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
(L.d_str "explain_leak: current instruction is Nullify for pvar "; (L.d_str "explain_leak: current instruction is Nullify for pvar ";
Pvar.d pvar; L.d_ln ()); Pvar.d pvar; L.d_ln ());
(match exp_lv_dexp (State.get_node ()) (Sil.Lvar pvar) with (match exp_lv_dexp (State.get_node ()) (Sil.Lvar pvar) with
| Some de when not (Sil.dexp_has_tmp_var de)-> Some (Sil.dexp_to_string de) | Some de when not (DExp.has_tmp_var de)-> Some (DExp.to_string de)
| _ -> None) | _ -> None)
| Some (Sil.Abstract _) -> | Some (Sil.Abstract _) ->
if verbose then (L.d_str "explain_leak: current instruction is Abstract"; L.d_ln ()); if verbose then (L.d_str "explain_leak: current instruction is Abstract"; L.d_ln ());
@ -563,7 +564,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
(L.d_str "explain_leak: current instruction Set for "; (L.d_str "explain_leak: current instruction Set for ";
Sil.d_exp lexp; L.d_ln ()); Sil.d_exp lexp; L.d_ln ());
(match exp_lv_dexp node lexp with (match exp_lv_dexp node lexp with
| Some dexp when not (Sil.dexp_has_tmp_var dexp) -> Some (Sil.dexp_to_string dexp) | Some dexp when not (DExp.has_tmp_var dexp) -> Some (DExp.to_string dexp)
| _ -> None) | _ -> None)
| Some instr -> | Some instr ->
if verbose if verbose
@ -586,7 +587,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
(** find the dexp, if any, where the given value is stored (** find the dexp, if any, where the given value is stored
also return the type of the value if found *) also return the type of the value if found *)
let vpath_find prop _exp : Sil.dexp option * Typ.t option = let vpath_find prop _exp : DExp.t option * Typ.t option =
if verbose then (L.d_str "in vpath_find exp:"; Sil.d_exp _exp; L.d_ln ()); if verbose then (L.d_str "in vpath_find exp:"; Sil.d_exp _exp; L.d_ln ());
let rec find sigma_acc sigma_todo exp = let rec find sigma_acc sigma_todo exp =
let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) = match se with let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) = match se with
@ -604,11 +605,11 @@ let vpath_find prop _exp : Sil.dexp option * Typ.t option =
Some t Some t
with Not_found -> None) with Not_found -> None)
| _ -> None in | _ -> None in
res := Some (Sil.Ddot (Sil.Dpvar pv, f)), typo res := Some (DExp.Ddot (DExp.Dpvar pv, f)), typo
| Sil.Var id -> | Sil.Var id ->
(match find [] sigma' (Sil.Var id) with (match find [] sigma' (Sil.Var id) with
| None, _ -> () | None, _ -> ()
| Some de, typo -> res := Some (Sil.Darrow (de, f)), typo) | Some de, typo -> res := Some (DExp.Darrow (de, f)), typo)
| lexp -> | lexp ->
if verbose if verbose
then then
@ -623,11 +624,11 @@ let vpath_find prop _exp : Sil.dexp option * Typ.t option =
let typo = match texp with let typo = match texp with
| Sil.Sizeof (typ, _, _) -> Some typ | Sil.Sizeof (typ, _, _) -> Some typ
| _ -> None in | _ -> None in
Some (Sil.Dpvar pv), typo Some (DExp.Dpvar pv), typo
| Sil.Var id -> | Sil.Var id ->
(match find [] sigma' (Sil.Var id) with (match find [] sigma' (Sil.Var id) with
| None, typo -> None, typo | None, typo -> None, typo
| Some de, typo -> Some (Sil.Dderef de), typo) | Some de, typo -> Some (DExp.Dderef de), typo)
| lexp -> | lexp ->
if verbose if verbose
then then
@ -665,7 +666,8 @@ let vpath_find prop _exp : Sil.dexp option * Typ.t option =
if verbose then begin if verbose then begin
match res with match res with
| None, _ -> L.d_str "vpath_find: cannot find "; Sil.d_exp _exp; L.d_ln () | None, _ -> L.d_str "vpath_find: cannot find "; Sil.d_exp _exp; L.d_ln ()
| Some de, typo -> L.d_str "vpath_find: found "; L.d_str (Sil.dexp_to_string de); L.d_str " : "; | Some de, typo ->
L.d_str "vpath_find: found "; L.d_str (DExp.to_string de); L.d_str " : ";
match typo with match typo with
| None -> L.d_str " No type" | None -> L.d_str " No type"
| Some typ -> Typ.d_full typ; | Some typ -> Typ.d_full typ;
@ -706,10 +708,10 @@ let explain_dexp_access prop dexp is_nullable =
| (e1, se):: esel' -> | (e1, se):: esel' ->
if Sil.exp_equal e1 e then Some se if Sil.exp_equal e1 e then Some se
else lookup_esel esel' e in else lookup_esel esel' e in
let rec lookup : Sil.dexp -> Sil.strexp option = function let rec lookup : DExp.t -> Sil.strexp option = function
| Sil.Dconst c -> | DExp.Dconst c ->
Some (Sil.Eexp (Sil.Const c, Sil.inst_none)) Some (Sil.Eexp (Sil.Const c, Sil.inst_none))
| Sil.Darray (de1, de2) -> | DExp.Darray (de1, de2) ->
(match lookup de1, lookup de2 with (match lookup de1, lookup de2 with
| None, _ | _, None -> None | None, _ | _, None -> None
| Some Sil.Earray (_, esel, _), Some Sil.Eexp (e, _) -> | Some Sil.Earray (_, esel, _), Some Sil.Eexp (e, _) ->
@ -720,23 +722,23 @@ let explain_dexp_access prop dexp is_nullable =
(L.d_str "lookup: case not matched on Darray "; (L.d_str "lookup: case not matched on Darray ";
Sil.d_sexp se1; L.d_str " "; Sil.d_sexp se2; L.d_ln()); Sil.d_sexp se1; L.d_str " "; Sil.d_sexp se2; L.d_ln());
None) None)
| Sil.Darrow ((Sil.Dpvaraddr pvar), f) -> | DExp.Darrow ((DExp.Dpvaraddr pvar), f) ->
(match lookup (Sil.Dpvaraddr pvar) with (match lookup (DExp.Dpvaraddr pvar) with
| None -> None | None -> None
| Some Sil.Estruct (fsel, _) -> | Some Sil.Estruct (fsel, _) ->
lookup_fld fsel f lookup_fld fsel f
| Some _ -> | Some _ ->
if verbose then (L.d_str "lookup: case not matched on Darrow "; L.d_ln ()); if verbose then (L.d_str "lookup: case not matched on Darrow "; L.d_ln ());
None) None)
| Sil.Darrow (de1, f) -> | DExp.Darrow (de1, f) ->
(match lookup (Sil.Dderef de1) with (match lookup (DExp.Dderef de1) with
| None -> None | None -> None
| Some Sil.Estruct (fsel, _) -> | Some Sil.Estruct (fsel, _) ->
lookup_fld fsel f lookup_fld fsel f
| Some _ -> | Some _ ->
if verbose then (L.d_str "lookup: case not matched on Darrow "; L.d_ln ()); if verbose then (L.d_str "lookup: case not matched on Darrow "; L.d_ln ());
None) None)
| Sil.Ddot (de1, f) -> | DExp.Ddot (de1, f) ->
(match lookup de1 with (match lookup de1 with
| None -> None | None -> None
| Some Sil.Estruct (fsel, _) -> | Some Sil.Estruct (fsel, _) ->
@ -746,38 +748,38 @@ let explain_dexp_access prop dexp is_nullable =
| Some _ -> | Some _ ->
if verbose then (L.d_str "lookup: case not matched on Ddot "; L.d_ln ()); if verbose then (L.d_str "lookup: case not matched on Ddot "; L.d_ln ());
None) None)
| Sil.Dpvar pvar -> | DExp.Dpvar pvar ->
if verbose then (L.d_str "lookup: found Dpvar "; L.d_ln ()); if verbose then (L.d_str "lookup: found Dpvar "; L.d_ln ());
(find_ptsto (Sil.Lvar pvar)) (find_ptsto (Sil.Lvar pvar))
| Sil.Dderef de -> | DExp.Dderef de ->
(match lookup de with (match lookup de with
| None -> None | None -> None
| Some (Sil.Eexp (e, _)) -> find_ptsto e | Some (Sil.Eexp (e, _)) -> find_ptsto e
| Some _ -> None) | Some _ -> None)
| (Sil.Dbinop(Binop.PlusPI, Sil.Dpvar _, Sil.Dconst _) as de) -> | (DExp.Dbinop(Binop.PlusPI, DExp.Dpvar _, DExp.Dconst _) as de) ->
if verbose then (L.d_strln ("lookup: case )pvar + constant) " ^ Sil.dexp_to_string de)); if verbose then (L.d_strln ("lookup: case )pvar + constant) " ^ DExp.to_string de));
None None
| Sil.Dfcall (Sil.Dconst c, _, loc, _) -> | DExp.Dfcall (DExp.Dconst c, _, loc, _) ->
if verbose then (L.d_strln "lookup: found Dfcall "); if verbose then (L.d_strln "lookup: found Dfcall ");
(match c with (match c with
| Const.Cfun _ -> (* Treat function as an update *) | Const.Cfun _ -> (* Treat function as an update *)
Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_call loc.Location.line)) Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_call loc.Location.line))
| _ -> None) | _ -> None)
| Sil.Dretcall (Sil.Dconst (Const.Cfun pname as c ) , _, loc, _ ) | DExp.Dretcall (DExp.Dconst (Const.Cfun pname as c ) , _, loc, _ )
when method_of_pointer_wrapper pname -> when method_of_pointer_wrapper pname ->
if verbose then (L.d_strln "lookup: found Dretcall "); if verbose then (L.d_strln "lookup: found Dretcall ");
Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_pointer_wrapper_call loc.Location.line)) Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_pointer_wrapper_call loc.Location.line))
| Sil.Dpvaraddr pvar -> | DExp.Dpvaraddr pvar ->
(L.d_strln ("lookup: found Dvaraddr " ^ Sil.dexp_to_string (Sil.Dpvaraddr pvar))); (L.d_strln ("lookup: found Dvaraddr " ^ DExp.to_string (DExp.Dpvaraddr pvar)));
find_ptsto (Sil.Lvar pvar) find_ptsto (Sil.Lvar pvar)
| de -> | de ->
if verbose then (L.d_strln ("lookup: unknown case not matched " ^ Sil.dexp_to_string de)); if verbose then (L.d_strln ("lookup: unknown case not matched " ^ DExp.to_string de));
None in None in
let access_opt = match sexpo_to_inst (lookup dexp) with let access_opt = match sexpo_to_inst (lookup dexp) with
| None -> | None ->
if verbose if verbose
then then
(L.d_strln ("explain_dexp_access: cannot find inst of " ^ Sil.dexp_to_string dexp)); (L.d_strln ("explain_dexp_access: cannot find inst of " ^ DExp.to_string dexp));
None None
| Some (Sil.Iupdate (_, ncf, n, _)) -> | Some (Sil.Iupdate (_, ncf, n, _)) ->
Some (Localise.Last_assigned (n, ncf)) Some (Localise.Last_assigned (n, ncf))
@ -801,15 +803,17 @@ let explain_dexp_access prop dexp is_nullable =
let explain_dereference_access outermost_array is_nullable _de_opt prop = let explain_dereference_access outermost_array is_nullable _de_opt prop =
let de_opt = let de_opt =
let rec remove_outermost_array_access = function (* remove outermost array access from [de] *) let rec remove_outermost_array_access = function (* remove outermost array access from [de] *)
| Sil.Dbinop(Binop.PlusPI, de1, _) -> (* remove pointer arithmetic before array access *) | DExp.Dbinop(Binop.PlusPI, de1, _) ->
(* remove pointer arithmetic before array access *)
remove_outermost_array_access de1 remove_outermost_array_access de1
| Sil.Darray(Sil.Dderef de1, _) -> (* array access is a deref already: remove both *) | DExp.Darray(DExp.Dderef de1, _) ->
(* array access is a deref already: remove both *)
de1 de1
| Sil.Darray(de1, _) -> (* remove array access *) | DExp.Darray(de1, _) -> (* remove array access *)
de1 de1
| Sil.Dderef de -> (* remove implicit array access *) | DExp.Dderef de -> (* remove implicit array access *)
de de
| Sil.Ddot (de, _) -> (* remove field access before array access *) | DExp.Ddot (de, _) -> (* remove field access before array access *)
remove_outermost_array_access de remove_outermost_array_access de
| de -> de in | de -> de in
match _de_opt with match _de_opt with
@ -817,12 +821,12 @@ let explain_dereference_access outermost_array is_nullable _de_opt prop =
| Some de -> | Some de ->
Some (if outermost_array then remove_outermost_array_access de else de) in Some (if outermost_array then remove_outermost_array_access de else de) in
let value_str = match de_opt with let value_str = match de_opt with
| Some (Sil.Darrow ((Sil.Dpvaraddr pvar), f) as de) -> | Some (DExp.Darrow ((DExp.Dpvaraddr pvar), f) as de) ->
if is_special_field smart_pointers None f then if is_special_field smart_pointers None f then
Sil.dexp_to_string (Sil.Dpvaraddr pvar) DExp.to_string (DExp.Dpvaraddr pvar)
else Sil.dexp_to_string de else DExp.to_string de
| Some de -> | Some de ->
Sil.dexp_to_string de DExp.to_string de
| None -> "" in | None -> "" in
let access_opt = match de_opt with let access_opt = match de_opt with
| Some de -> explain_dexp_access prop de is_nullable | Some de -> explain_dexp_access prop de is_nullable
@ -846,20 +850,20 @@ let create_dereference_desc
let desc = let desc =
if !Config.curr_language = Config.Clang && not is_premature_nil then if !Config.curr_language = Config.Clang && not is_premature_nil then
match de_opt with match de_opt with
| Some (Sil.Dpvar pvar) | Some (DExp.Dpvar pvar)
| Some (Sil.Dpvaraddr pvar) -> | Some (DExp.Dpvaraddr pvar) ->
(match Prop.get_objc_null_attribute prop (Sil.Lvar pvar) with (match Prop.get_objc_null_attribute prop (Sil.Lvar pvar) with
| Some (Sil.Aobjc_null (v,fs)) -> | Some (Sil.Aobjc_null (v,fs)) ->
let e = IList.fold_left (fun e f -> Sil.Lfield (e, f, Typ.Tvoid)) (Sil.Lvar v) fs in let e = IList.fold_left (fun e f -> Sil.Lfield (e, f, Typ.Tvoid)) (Sil.Lvar v) fs in
Localise.parameter_field_not_null_checked_desc desc e Localise.parameter_field_not_null_checked_desc desc e
| _ -> | _ ->
desc) desc)
| Some (Sil.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _ )) | Some (DExp.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _ ))
when is_vector_method pname -> when is_vector_method pname ->
Localise.desc_empty_vector_access (Some pname) (Sil.dexp_to_string this_dexp) loc Localise.desc_empty_vector_access (Some pname) (DExp.to_string this_dexp) loc
| Some (Sil.Darrow (dexp, fieldname)) | Some (DExp.Darrow (dexp, fieldname))
when is_special_field [vector_class] (Some "beginPtr") fieldname -> when is_special_field [vector_class] (Some "beginPtr") fieldname ->
Localise.desc_empty_vector_access None (Sil.dexp_to_string dexp) loc Localise.desc_empty_vector_access None (DExp.to_string dexp) loc
| _ -> desc | _ -> desc
else desc in else desc in
if use_buckets then Buckets.classify_access desc access_opt' de_opt is_nullable if use_buckets then Buckets.classify_access desc access_opt' de_opt is_nullable
@ -974,10 +978,10 @@ let dexp_apply_pvar_off dexp pvar_off =
let rec add_ddot de = function let rec add_ddot de = function
| [] -> de | [] -> de
| f:: fl -> | f:: fl ->
add_ddot (Sil.Ddot (de, f)) fl in add_ddot (DExp.Ddot (de, f)) fl in
match pvar_off with match pvar_off with
| Fpvar -> dexp | Fpvar -> dexp
| Fstruct (f:: fl) -> add_ddot (Sil.Darrow (dexp, f)) fl | Fstruct (f:: fl) -> add_ddot (DExp.Darrow (dexp, f)) fl
| Fstruct [] -> dexp (* case should not happen *) | Fstruct [] -> dexp (* case should not happen *)
(** Produce a description of the nth parameter of the function call, if the current instruction (** Produce a description of the nth parameter of the function call, if the current instruction
@ -1061,12 +1065,12 @@ let explain_dereference_as_caller_expression
(** explain a class cast exception *) (** explain a class cast exception *)
let explain_class_cast_exception pname_opt typ1 typ2 exp node loc = let explain_class_cast_exception pname_opt typ1 typ2 exp node loc =
let exp_str_opt = match exp_rv_dexp node exp with let exp_str_opt = match exp_rv_dexp node exp with
| Some dexp -> Some (Sil.dexp_to_string dexp) | Some dexp -> Some (DExp.to_string dexp)
| None -> None in | None -> None in
match exp_rv_dexp node typ1, exp_rv_dexp node typ2 with match exp_rv_dexp node typ1, exp_rv_dexp node typ2 with
| Some de1, Some de2 -> | Some de1, Some de2 ->
let typ_str1 = Sil.dexp_to_string de1 in let typ_str1 = DExp.to_string de1 in
let typ_str2 = Sil.dexp_to_string de2 in let typ_str2 = DExp.to_string de2 in
Localise.desc_class_cast_exception pname_opt typ_str1 typ_str2 exp_str_opt loc Localise.desc_class_cast_exception pname_opt typ_str1 typ_str2 exp_str_opt loc
| _ -> Localise.no_desc | _ -> Localise.no_desc
@ -1074,7 +1078,7 @@ let explain_class_cast_exception pname_opt typ1 typ2 exp node loc =
let explain_divide_by_zero exp node loc = let explain_divide_by_zero exp node loc =
match exp_rv_dexp node exp with match exp_rv_dexp node exp with
| Some de -> | Some de ->
let exp_str = Sil.dexp_to_string de in let exp_str = DExp.to_string de in
Localise.desc_divide_by_zero exp_str loc Localise.desc_divide_by_zero exp_str loc
| None -> Localise.no_desc | None -> Localise.no_desc
@ -1099,8 +1103,8 @@ let explain_tainted_value_reaching_sensitive_function
begin begin
match find_with_exp prop e with match find_with_exp prop e with
| Some (pvar, pvar_off) -> | Some (pvar, pvar_off) ->
let dexp = dexp_apply_pvar_off (Sil.Dpvar pvar) pvar_off in let dexp = dexp_apply_pvar_off (DExp.Dpvar pvar) pvar_off in
Sil.dexp_to_string dexp DExp.to_string dexp
| None -> Sil.exp_to_string e | None -> Sil.exp_to_string e
end in end in
Localise.desc_tainted_value_reaching_sensitive_function Localise.desc_tainted_value_reaching_sensitive_function
@ -1130,25 +1134,25 @@ let explain_condition_is_assignment loc =
let explain_condition_always_true_false i cond node loc = let explain_condition_always_true_false i cond node loc =
let cond_str_opt = match exp_rv_dexp node cond with let cond_str_opt = match exp_rv_dexp node cond with
| Some de -> | Some de ->
Some (Sil.dexp_to_string de) Some (DExp.to_string de)
| None -> None in | None -> None in
Localise.desc_condition_always_true_false i cond_str_opt loc Localise.desc_condition_always_true_false i cond_str_opt loc
(** explain the escape of a stack variable address from its scope *) (** explain the escape of a stack variable address from its scope *)
let explain_stack_variable_address_escape loc pvar addr_dexp_opt = let explain_stack_variable_address_escape loc pvar addr_dexp_opt =
let addr_dexp_str = match addr_dexp_opt with let addr_dexp_str = match addr_dexp_opt with
| Some (Sil.Dpvar pv) | Some (DExp.Dpvar pv)
when Pvar.is_local pv && when Pvar.is_local pv &&
Mangled.equal (Pvar.get_name pv) Ident.name_return -> Mangled.equal (Pvar.get_name pv) Ident.name_return ->
Some "the caller via a return" Some "the caller via a return"
| Some dexp -> Some (Sil.dexp_to_string dexp) | Some dexp -> Some (DExp.to_string dexp)
| None -> None in | None -> None in
Localise.desc_stack_variable_address_escape (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 *) (** explain unary minus applied to unsigned expression *)
let explain_unary_minus_applied_to_unsigned_expression exp typ node loc = let explain_unary_minus_applied_to_unsigned_expression exp typ node loc =
let exp_str_opt = match exp_rv_dexp node exp with let exp_str_opt = match exp_rv_dexp node exp with
| Some de -> Some (Sil.dexp_to_string de) | Some de -> Some (DExp.to_string de)
| None -> None in | None -> None in
let typ_str = let typ_str =
let pp fmt () = Typ.pp_full pe_text fmt typ in let pp fmt () = Typ.pp_full pe_text fmt typ in
@ -1159,7 +1163,7 @@ let explain_unary_minus_applied_to_unsigned_expression exp typ node loc =
let explain_null_test_after_dereference exp node line loc = let explain_null_test_after_dereference exp node line loc =
match exp_rv_dexp node exp with match exp_rv_dexp node exp with
| Some de -> | Some de ->
let expr_str = Sil.dexp_to_string de in let expr_str = DExp.to_string de in
Localise.desc_null_test_after_dereference expr_str line loc Localise.desc_null_test_after_dereference expr_str line loc
| None -> Localise.no_desc | None -> Localise.no_desc

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

@ -14,7 +14,7 @@ open! Utils
(** find the dexp, if any, where the given value is stored (** find the dexp, if any, where the given value is stored
also return the type of the value if found *) also return the type of the value if found *)
val vpath_find : 'a Prop.t -> Sil.exp -> Sil.vpath * Typ.t option val vpath_find : 'a Prop.t -> Sil.exp -> DecompiledExp.vpath * Typ.t option
(** Return true if [id] is assigned to a program variable which is then nullified *) (** Return true if [id] is assigned to a program variable which is then nullified *)
val id_is_assigned_then_dead : Cfg.Node.t -> Ident.t -> bool val id_is_assigned_then_dead : Cfg.Node.t -> Ident.t -> bool
@ -38,7 +38,7 @@ val find_ident_assignment : Cfg.Node.t -> Ident.t -> (Cfg.Node.t * Sil.exp) opti
val find_boolean_assignment : Cfg.Node.t -> Pvar.t -> 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 *) (** describe rvalue [e] as a dexp *)
val exp_rv_dexp : Cfg.Node.t -> Sil.exp -> Sil.dexp option val exp_rv_dexp : Cfg.Node.t -> Sil.exp -> DecompiledExp.t option
(** Produce a description of a persistent reference to an Android Context *) (** Produce a description of a persistent reference to an Android Context *)
val explain_context_leak : Procname.t -> Typ.t -> Ident.fieldname -> val explain_context_leak : Procname.t -> Typ.t -> Ident.fieldname ->
@ -94,7 +94,7 @@ val explain_condition_always_true_false :
(** explain the escape of a stack variable address from its scope *) (** explain the escape of a stack variable address from its scope *)
val explain_stack_variable_address_escape : val explain_stack_variable_address_escape :
Location.t -> Pvar.t -> Sil.dexp option -> Localise.error_desc Location.t -> Pvar.t -> DecompiledExp.t option -> Localise.error_desc
(** explain frontend warning *) (** explain frontend warning *)
val explain_frontend_warning : string -> string -> Location.t -> Localise.error_desc val explain_frontend_warning : string -> string -> Location.t -> Localise.error_desc

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

@ -469,7 +469,7 @@ let desc_custom_error loc : error_desc =
let desc_bad_pointer_comparison dexp_opt loc : error_desc = let desc_bad_pointer_comparison dexp_opt loc : error_desc =
let dexp_str = match dexp_opt with let dexp_str = match dexp_opt with
| Some dexp -> (Sil.dexp_to_string dexp) ^ " " | Some dexp -> (DecompiledExp.to_string dexp) ^ " "
| None -> "" in | None -> "" in
let line_info = at_line (Tags.create ()) loc in let line_info = at_line (Tags.create ()) loc in
let check_msg = let check_msg =

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

@ -227,7 +227,7 @@ val desc_fragment_retains_view :
(* Create human-readable error description for assertion failures *) (* Create human-readable error description for assertion failures *)
val desc_custom_error : Location.t -> error_desc val desc_custom_error : Location.t -> error_desc
val desc_bad_pointer_comparison : Sil.dexp option -> Location.t -> error_desc val desc_bad_pointer_comparison : DecompiledExp.t option -> Location.t -> error_desc
(** kind of precondition not met *) (** kind of precondition not met *)
type pnm_kind = type pnm_kind =
| Pnm_bounds | Pnm_bounds

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

@ -548,7 +548,7 @@ let callback_print_c_method_calls { Callbacks.proc_desc; proc_name } =
| Sil.Call (_, Sil.Const (Const.Cfun pn), (e, _):: _, loc, _) | Sil.Call (_, Sil.Const (Const.Cfun pn), (e, _):: _, loc, _)
when Procname.is_c_method pn -> when Procname.is_c_method pn ->
let receiver = match Errdesc.exp_rv_dexp node e with let receiver = match Errdesc.exp_rv_dexp node e with
| Some de -> Sil.dexp_to_string de | Some de -> DecompiledExp.to_string de
| None -> "?" in | None -> "?" in
let description = let description =
Printf.sprintf "['%s' %s]" receiver (Procname.to_string pn) in Printf.sprintf "['%s' %s]" receiver (Procname.to_string pn) in

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

@ -57,7 +57,7 @@ let report_error =
let explain_expr node e = let explain_expr node e =
match Errdesc.exp_rv_dexp node e with match Errdesc.exp_rv_dexp node e with
| Some de -> Some (Sil.dexp_to_string de) | Some de -> Some (DecompiledExp.to_string de)
| None -> None | None -> None
(** Classify a procedure. *) (** Classify a procedure. *)

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

@ -11,6 +11,7 @@ open! Utils
module L = Logging module L = Logging
module F = Format module F = Format
module DExp = DecompiledExp
(** Module for type checking. *) (** Module for type checking. *)
@ -91,21 +92,21 @@ module ComplexExpressions = struct
raise Not_handled in raise Not_handled in
match dexp with match dexp with
| Sil.Darray (de1, de2) -> | DExp.Darray (de1, de2) ->
dexp_to_string de1 ^ "[" ^ dexp_to_string de2 ^ "]" dexp_to_string de1 ^ "[" ^ dexp_to_string de2 ^ "]"
| Sil.Darrow (de, f) | DExp.Darrow (de, f)
| Sil.Ddot (de, f) -> | DExp.Ddot (de, f) ->
dexp_to_string de ^ "." ^ Ident.fieldname_to_string f dexp_to_string de ^ "." ^ Ident.fieldname_to_string f
| Sil.Dbinop (op, de1, de2) -> | DExp.Dbinop (op, de1, de2) ->
"(" ^ dexp_to_string de1 ^ (Binop.str pe_text op) ^ dexp_to_string de2 ^ ")" "(" ^ dexp_to_string de1 ^ (Binop.str pe_text op) ^ dexp_to_string de2 ^ ")"
| Sil.Dconst (Const.Cfun pn) -> | DExp.Dconst (Const.Cfun pn) ->
Procname.to_unique_id pn Procname.to_unique_id pn
| Sil.Dconst c -> | DExp.Dconst c ->
pp_to_string (Const.pp pe_text) c pp_to_string (Const.pp pe_text) c
| Sil.Dderef de -> | DExp.Dderef de ->
dexp_to_string de dexp_to_string de
| Sil.Dfcall (fun_dexp, args, _, { CallFlags.cf_virtual = isvirtual }) | DExp.Dfcall (fun_dexp, args, _, { CallFlags.cf_virtual = isvirtual })
| Sil.Dretcall (fun_dexp, args, _, { CallFlags.cf_virtual = isvirtual }) | DExp.Dretcall (fun_dexp, args, _, { CallFlags.cf_virtual = isvirtual })
when functions_idempotent () -> when functions_idempotent () ->
let pp_arg fmt de = F.fprintf fmt "%s" (dexp_to_string de) in let pp_arg fmt de = F.fprintf fmt "%s" (dexp_to_string de) in
let pp_args fmt des = (pp_comma_seq) pp_arg fmt des in let pp_args fmt des = (pp_comma_seq) pp_arg fmt des in
@ -113,20 +114,20 @@ module ComplexExpressions = struct
let virt = if isvirtual then "V" else "" in let virt = if isvirtual then "V" else "" in
F.fprintf fmt "%a(%a)%s" pp_arg fun_dexp pp_args args virt in F.fprintf fmt "%a(%a)%s" pp_arg fun_dexp pp_args args virt in
pp_to_string pp () pp_to_string pp ()
| Sil.Dfcall _ | DExp.Dfcall _
| Sil.Dretcall _ -> | DExp.Dretcall _ ->
case_not_handled () case_not_handled ()
| Sil.Dpvar pv | DExp.Dpvar pv
| Sil.Dpvaraddr pv when not (Pvar.is_frontend_tmp pv) -> | DExp.Dpvaraddr pv when not (Pvar.is_frontend_tmp pv) ->
Pvar.to_string pv Pvar.to_string pv
| Sil.Dpvar _ | DExp.Dpvar _
| Sil.Dpvaraddr _ (* front-end variable -- this should not happen) *) -> | DExp.Dpvaraddr _ (* front-end variable -- this should not happen) *) ->
case_not_handled () case_not_handled ()
| Sil.Dunop (op, de) -> | DExp.Dunop (op, de) ->
Unop.str op ^ dexp_to_string de Unop.str op ^ dexp_to_string de
| Sil.Dsizeof _ -> | DExp.Dsizeof _ ->
case_not_handled () case_not_handled ()
| Sil.Dunknown -> | DExp.Dunknown ->
case_not_handled () in case_not_handled () in
match map_dexp (Errdesc.exp_rv_dexp node' exp) with match map_dexp (Errdesc.exp_rv_dexp node' exp) with
@ -770,11 +771,11 @@ let typecheck_instr
| Some dexp_key, Procname.Java callee_pname_java -> | Some dexp_key, Procname.Java callee_pname_java ->
let pname_get = let pname_get =
Procname.Java (pname_get_from_pname_put callee_pname_java) in Procname.Java (pname_get_from_pname_put callee_pname_java) in
let dexp_get = Sil.Dconst (Const.Cfun pname_get) in let dexp_get = DExp.Dconst (Const.Cfun pname_get) in
let dexp_map = Sil.Dpvar pv_map in let dexp_map = DExp.Dpvar pv_map in
let args = [dexp_map; dexp_key] in let args = [dexp_map; dexp_key] in
let call_flags = { CallFlags.default with CallFlags.cf_virtual = true } in let call_flags = { CallFlags.default with CallFlags.cf_virtual = true } in
Some (Sil.Dretcall (dexp_get, args, loc, call_flags)) Some (DExp.Dretcall (dexp_get, args, loc, call_flags))
| _ -> None in | _ -> None in
begin begin
match ComplexExpressions.exp_to_string_map_dexp match ComplexExpressions.exp_to_string_map_dexp
@ -903,16 +904,15 @@ let typecheck_instr
let handle_containsKey e = let handle_containsKey e =
let map_dexp = function let map_dexp = function
| Some | Some
(Sil.Dretcall (DExp.Dretcall
(Sil.Dconst (DExp.Dconst (Const.Cfun (Procname.Java pname_java)), args, loc, call_flags)) ->
(Const.Cfun (Procname.Java pname_java)), args, loc, call_flags)) ->
let pname_java' = let pname_java' =
let object_t = (Some "java.lang", "Object") in let object_t = (Some "java.lang", "Object") in
Procname.java_replace_return_type Procname.java_replace_return_type
(Procname.java_replace_method pname_java "get") (Procname.java_replace_method pname_java "get")
object_t in object_t in
let fun_dexp = Sil.Dconst (Const.Cfun (Procname.Java pname_java')) in let fun_dexp = DExp.Dconst (Const.Cfun (Procname.Java pname_java')) in
Some (Sil.Dretcall (fun_dexp, args, loc, call_flags)) Some (DExp.Dretcall (fun_dexp, args, loc, call_flags))
| _ -> None in | _ -> None in
begin begin
match ComplexExpressions.exp_to_string_map_dexp map_dexp node' e with match ComplexExpressions.exp_to_string_map_dexp map_dexp node' e with

Write Preview
Loading…
Cancel
Save