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

[infer] Add typ field in Sil.Load

Browse Source 
Summary:
It adds `typ` field in Sil.Load.  The field will be used by the analyzer in the following diffs.

Motivation: Interbo generates a symbolic value when evaluating  expressions including parameter symbols. At that time, it is done with depending on their types, e.g., an integer, a pointer to struct or a pointer to array. Without the type, it is hard to generate a correct symbolic value that will be instantiated later in call sites. Thus, evaluating RHS of the load statement, the type of RHS is better to be given.

Reviewed By: jvillard

Differential Revision: D17163350

fbshipit-source-id: f7f0f1429
master
Sungkeun Cho 5 years ago committed by Facebook Github Bot
parent a50fcaf2dd
commit 3250ff35d2
12 changed files with 95 additions and 56 deletions
Show Stats Download Patch File Download Diff File

13
infer/src/IR/Cfg.ml
Unescape View File

@ -71,17 +71,18 @@ let inline_synthetic_method ((ret_id, _) as ret) etl pdesc loc_call : Sil.instr
in in
let do_instr instr = let do_instr instr =
match (instr, etl) with match (instr, etl) with
| Sil.Load {e= Exp.Lfield (Exp.Var _, fn, ft); root_typ= bt}, [(* getter for fields *) (e1, _)] | ( Sil.Load {e= Exp.Lfield (Exp.Var _, fn, ft); root_typ= bt; typ}
-> , [(* getter for fields *) (e1, _)] ) ->
let instr' = let instr' =
Sil.Load {id= ret_id; e= Exp.Lfield (e1, fn, ft); root_typ= bt; loc= loc_call} Sil.Load {id= ret_id; e= Exp.Lfield (e1, fn, ft); root_typ= bt; typ; loc= loc_call}
in in
found instr instr' found instr instr'
| Sil.Load {e= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt}, [] when Pvar.is_global pvar | Sil.Load {e= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt; typ}, []
-> when Pvar.is_global pvar ->
(* getter for static fields *) (* getter for static fields *)
let instr' = let instr' =
Sil.Load {id= ret_id; e= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt; loc= loc_call} Sil.Load
{id= ret_id; e= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt; typ; loc= loc_call}
in in
found instr instr' found instr instr'
| ( Sil.Store {e1= Exp.Lfield (_, fn, ft); root_typ= bt} | ( Sil.Store {e1= Exp.Lfield (_, fn, ft); root_typ= bt}

24
infer/src/IR/Sil.ml
Unescape View File

@ -40,11 +40,16 @@ type instr =
(* Note for frontend writers: (* Note for frontend writers:
[x] must be used in a subsequent instruction, otherwise the entire [x] must be used in a subsequent instruction, otherwise the entire
`Load` instruction may be eliminated by copy-propagation. *) `Load` instruction may be eliminated by copy-propagation. *)
| Load of {id: Ident.t; e: Exp.t; root_typ: Typ.t; loc: Location.t} | Load of {id: Ident.t; e: Exp.t; root_typ: Typ.t; typ: Typ.t; loc: Location.t}
(** Load a value from the heap into an identifier. (** Load a value from the heap into an identifier.
[x = *exp:root_typ] where
[id = *exp:typ(root_typ)] where
[exp] is an expression denoting a heap address [exp] is an expression denoting a heap address
[root_typ] is the root type of [exp]. *) [typ] is typ of [exp] and [id]
[root_typ] is the root type of [exp]
The [root_typ] is deprecated: it is broken in C/C++. We are removing [root_typ] in the
future, so please use [typ] instead. *)
| Store of {e1: Exp.t; root_typ: Typ.t; e2: Exp.t; loc: Location.t} | Store of {e1: Exp.t; root_typ: Typ.t; e2: Exp.t; loc: Location.t}
(** Store the value of an expression into the heap. (** Store the value of an expression into the heap.
[*exp1:root_typ = exp2] where [*exp1:root_typ = exp2] where
@ -412,9 +417,12 @@ let pp_instr ~print_types pe0 f instr =
let pp_typ = if print_types then Typ.pp_full else Typ.pp in let pp_typ = if print_types then Typ.pp_full else Typ.pp in
color_wrapper pe0 f instr ~f:(fun pe f instr -> color_wrapper pe0 f instr ~f:(fun pe f instr ->
match instr with match instr with
| Load {id; e; root_typ; loc} -> | Load {id; e; root_typ; typ; loc} ->
F.fprintf f "%a=*%a:%a [%a]" Ident.pp id (pp_exp_printenv ~print_types pe) e (pp_typ pe0) let pp_root f =
root_typ Location.pp loc if not (Typ.equal typ root_typ) then F.fprintf f "(root %a)" (pp_typ pe0) root_typ
in
F.fprintf f "%a=*%a:%a%t [%a]" Ident.pp id (pp_exp_printenv ~print_types pe) e
(pp_typ pe0) typ pp_root Location.pp loc
| Store {e1; root_typ; e2; loc} -> | Store {e1; root_typ; e2; loc} ->
F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv ~print_types pe) e1 (pp_typ pe0) root_typ F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv ~print_types pe) e1 (pp_typ pe0) root_typ
(pp_exp_printenv ~print_types pe) e2 Location.pp loc (pp_exp_printenv ~print_types pe) e2 Location.pp loc
@ -1267,11 +1275,11 @@ let instr_sub_ids ~sub_id_binders f instr =
match exp_sub_ids f (Var id) with Var id' when not (Ident.equal id id') -> id' | _ -> id match exp_sub_ids f (Var id) with Var id' when not (Ident.equal id id') -> id' | _ -> id
in in
match instr with match instr with
| Load {id; e= rhs_exp; root_typ; loc} -> | Load {id; e= rhs_exp; root_typ; typ; loc} ->
let id' = if sub_id_binders then sub_id id else id in let id' = if sub_id_binders then sub_id id else id in
let rhs_exp' = exp_sub_ids f rhs_exp in let rhs_exp' = exp_sub_ids f rhs_exp in
if phys_equal id' id && phys_equal rhs_exp' rhs_exp then instr if phys_equal id' id && phys_equal rhs_exp' rhs_exp then instr
else Load {id= id'; e= rhs_exp'; root_typ; loc} else Load {id= id'; e= rhs_exp'; root_typ; typ; loc}
| Store {e1= lhs_exp; root_typ; e2= rhs_exp; loc} -> | Store {e1= lhs_exp; root_typ; e2= rhs_exp; loc} ->
let lhs_exp' = exp_sub_ids f lhs_exp in let lhs_exp' = exp_sub_ids f lhs_exp in
let rhs_exp' = exp_sub_ids f rhs_exp in let rhs_exp' = exp_sub_ids f rhs_exp in

11
infer/src/IR/Sil.mli
Unescape View File

@ -38,11 +38,16 @@ type instr =
(* Note for frontend writers: (* Note for frontend writers:
[x] must be used in a subsequent instruction, otherwise the entire [x] must be used in a subsequent instruction, otherwise the entire
`Load` instruction may be eliminated by copy-propagation. *) `Load` instruction may be eliminated by copy-propagation. *)
| Load of {id: Ident.t; e: Exp.t; root_typ: Typ.t; loc: Location.t} | Load of {id: Ident.t; e: Exp.t; root_typ: Typ.t; typ: Typ.t; loc: Location.t}
(** Load a value from the heap into an identifier. (** Load a value from the heap into an identifier.
[x = *exp:root_typ] where
[id = *exp:typ(root_typ)] where
[exp] is an expression denoting a heap address [exp] is an expression denoting a heap address
[root_typ] is the root type of [exp]. *) [typ] is typ of [exp] and [id]
[root_typ] is the root type of [exp]
The [root_typ] is deprecated: it is broken in C/C++. We are removing [root_typ] in the
future, so please use [typ] instead. *)
| Store of {e1: Exp.t; root_typ: Typ.t; e2: Exp.t; loc: Location.t} | Store of {e1: Exp.t; root_typ: Typ.t; e2: Exp.t; loc: Location.t}
(** Store the value of an expression into the heap. (** Store the value of an expression into the heap.
[*exp1:root_typ = exp2] where [*exp1:root_typ = exp2] where

17
infer/src/IR/SpecializeProcdesc.ml
Unescape View File

@ -72,8 +72,8 @@ let with_formals_types_proc callee_pdesc resolved_pdesc substitutions =
with Caml.Not_found -> origin_typename with Caml.Not_found -> origin_typename
in in
subst_map := Ident.Map.add id specialized_typname !subst_map ; subst_map := Ident.Map.add id specialized_typname !subst_map ;
Some let root_typ = mk_ptr_typ specialized_typname in
(Sil.Load {id; e= convert_exp origin_exp; root_typ= mk_ptr_typ specialized_typname; loc}) Some (Sil.Load {id; e= convert_exp origin_exp; root_typ; typ= root_typ; loc})
| Sil.Load | Sil.Load
{id; e= Exp.Var origin_id as origin_exp; root_typ= {Typ.desc= Tstruct _} as origin_typ; loc} {id; e= Exp.Var origin_id as origin_exp; root_typ= {Typ.desc= Tstruct _} as origin_typ; loc}
-> ->
@ -81,9 +81,10 @@ let with_formals_types_proc callee_pdesc resolved_pdesc substitutions =
try Typ.mk ~default:origin_typ (Tstruct (Ident.Map.find origin_id !subst_map)) try Typ.mk ~default:origin_typ (Tstruct (Ident.Map.find origin_id !subst_map))
with Caml.Not_found -> origin_typ with Caml.Not_found -> origin_typ
in in
Some (Sil.Load {id; e= convert_exp origin_exp; root_typ= updated_typ; loc}) Some
| Sil.Load {id; e= origin_exp; root_typ= origin_typ; loc} -> (Sil.Load {id; e= convert_exp origin_exp; root_typ= updated_typ; typ= updated_typ; loc})
Some (Sil.Load {id; e= convert_exp origin_exp; root_typ= origin_typ; loc}) | Sil.Load {id; e= origin_exp; root_typ= origin_typ; typ; loc} ->
Some (Sil.Load {id; e= convert_exp origin_exp; root_typ= origin_typ; typ; loc})
| Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= origin_exp; loc} -> | Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= origin_exp; loc} ->
let set_instr = let set_instr =
Sil.Store Sil.Store
@ -208,7 +209,7 @@ let with_block_args_instrs resolved_pdesc substitutions =
let pvar = Pvar.mk var resolved_pname in let pvar = Pvar.mk var resolved_pname in
( Var.of_id id ( Var.of_id id
, (Exp.Var id, pvar, typ) , (Exp.Var id, pvar, typ)
, Sil.Load {id; e= Exp.Lvar pvar; root_typ= typ; loc} ) ) , Sil.Load {id; e= Exp.Lvar pvar; root_typ= typ; typ; loc} ) )
|> List.unzip3 |> List.unzip3
in in
let remove_temps_instr = Sil.Metadata (ExitScope (dead_vars, loc)) in let remove_temps_instr = Sil.Metadata (ExitScope (dead_vars, loc)) in
@ -225,8 +226,8 @@ let with_block_args_instrs resolved_pdesc substitutions =
let id_map = Ident.Map.add id (Pvar.get_name block_param) id_map in let id_map = Ident.Map.add id (Pvar.get_name block_param) id_map in
(* we don't need the load the block param instruction anymore *) (* we don't need the load the block param instruction anymore *)
(instrs, id_map) (instrs, id_map)
| Sil.Load {id; e= origin_exp; root_typ= origin_typ; loc} -> | Sil.Load {id; e= origin_exp; root_typ= origin_typ; typ; loc} ->
(Sil.Load {id; e= convert_exp origin_exp; root_typ= origin_typ; loc} :: instrs, id_map) (Sil.Load {id; e= convert_exp origin_exp; root_typ= origin_typ; typ; loc} :: instrs, id_map)
| Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= Exp.Var id; loc} | Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= Exp.Var id; loc}
when Ident.Map.mem id id_map -> when Ident.Map.mem id id_map ->
let block_param = Ident.Map.find id id_map in let block_param = Ident.Map.find id id_map in

2
infer/src/biabduction/SymExec.ml
Unescape View File

@ -1763,7 +1763,7 @@ and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_po
let check_allocated result ((lexp, typ), i) = let check_allocated result ((lexp, typ), i) =
(* simulate a Load for [lexp] *) (* simulate a Load for [lexp] *)
let tmp_id_deref = Ident.create_fresh Ident.kprimed in let tmp_id_deref = Ident.create_fresh Ident.kprimed in
let load_instr = Sil.Load {id= tmp_id_deref; e= lexp; root_typ= typ; loc} in let load_instr = Sil.Load {id= tmp_id_deref; e= lexp; root_typ= typ; typ; loc} in
try instrs exe_env tenv summary (Instrs.singleton load_instr) result try instrs exe_env tenv summary (Instrs.singleton load_instr) result
with e when SymOp.exn_not_failure e -> with e when SymOp.exn_not_failure e ->
IExn.reraise_if e ~f:(fun () -> fails_on_nil) ; IExn.reraise_if e ~f:(fun () -> fails_on_nil) ;

10
infer/src/clang/cArithmetic_trans.ml
Unescape View File

@ -40,7 +40,7 @@ let compound_assignment_binary_operation_instruction boi_kind (e1, t1) typ e2 lo
Binop.BXor Binop.BXor
in in
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
[ Sil.Load {id; e= e1; root_typ= typ; loc} [ Sil.Load {id; e= e1; root_typ= typ; typ; loc}
; Sil.Store {e1; root_typ= typ; e2= Exp.BinOp (bop, Exp.Var id, e2); loc} ] ; Sil.Store {e1; root_typ= typ; e2= Exp.BinOp (bop, Exp.Var id, e2); loc} ]
in in
(e1, instrs) (e1, instrs)
@ -129,13 +129,13 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
match uoi.Clang_ast_t.uoi_kind with match uoi.Clang_ast_t.uoi_kind with
| `PostInc -> | `PostInc ->
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Load {id; e; root_typ= typ; loc} in let instr1 = Sil.Load {id; e; root_typ= typ; typ; loc} in
let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ) in let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ) in
let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
(Exp.Var id, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_plus_1; loc}]) (Exp.Var id, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_plus_1; loc}])
| `PreInc -> | `PreInc ->
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Load {id; e; root_typ= typ; loc} in let instr1 = Sil.Load {id; e; root_typ= typ; typ; loc} in
let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ) in let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ) in
let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
let exp = let exp =
@ -144,7 +144,7 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
(exp, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_plus_1; loc}]) (exp, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_plus_1; loc}])
| `PostDec -> | `PostDec ->
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Load {id; e; root_typ= typ; loc} in let instr1 = Sil.Load {id; e; root_typ= typ; typ; loc} in
let bop = let bop =
if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ) if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ)
in in
@ -152,7 +152,7 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
(Exp.Var id, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_minus_1; loc}]) (Exp.Var id, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_minus_1; loc}])
| `PreDec -> | `PreDec ->
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Load {id; e; root_typ= typ; loc} in let instr1 = Sil.Load {id; e; root_typ= typ; typ; loc} in
let bop = let bop =
if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ) if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ)
in in

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

@ -221,8 +221,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
let pvar = Pvar.mk formal procname in let pvar = Pvar.mk formal procname in
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
( (Exp.Var id, typ) :: forwarded_params ( (Exp.Var id, typ) :: forwarded_params
, Sil.Load {id; e= Exp.Lvar pvar; root_typ= typ; loc= sil_loc} :: forwarded_init_exps ) , Sil.Load {id; e= Exp.Lvar pvar; root_typ= typ; typ; loc= sil_loc}
) :: forwarded_init_exps ) )
let create_call_instr trans_state (return_type : Typ.t) function_sil params_sil sil_loc let create_call_instr trans_state (return_type : Typ.t) function_sil params_sil sil_loc
@ -291,7 +291,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
(** Given a captured var, return the instruction to assign it to a temp *) (** Given a captured var, return the instruction to assign it to a temp *)
let assign_captured_var loc (cvar, typ) = let assign_captured_var loc (cvar, typ) =
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let instr = Sil.Load {id; e= Exp.Lvar cvar; root_typ= typ; loc} in let instr = Sil.Load {id; e= Exp.Lvar cvar; root_typ= typ; typ; loc} in
((Exp.Var id, cvar, typ), instr) ((Exp.Var id, cvar, typ), instr)
@ -555,7 +555,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
let exp, deref_instrs = let exp, deref_instrs =
if should_add_deref then if should_add_deref then
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let deref_instr = Sil.Load {id; e= field_exp; root_typ= field_typ; loc= sil_loc} in let deref_instr =
Sil.Load {id; e= field_exp; root_typ= field_typ; typ= field_typ; loc= sil_loc}
in
(Exp.Var id, [deref_instr]) (Exp.Var id, [deref_instr])
else (field_exp, []) else (field_exp, [])
in in
@ -605,7 +607,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
calling a method with null *) calling a method with null *)
when decl_kind <> `CXXConstructor -> when decl_kind <> `CXXConstructor ->
let no_id = Ident.create_none () in let no_id = Ident.create_none () in
let extra_instrs = [Sil.Load {id= no_id; e= exp; root_typ= typ; loc= sil_loc}] in let extra_instrs = [Sil.Load {id= no_id; e= exp; root_typ= typ; typ; loc= sil_loc}] in
(return, extra_instrs) (return, extra_instrs)
| MemberOrIvar {return= (_, {Typ.desc= Tptr _}) as return} -> | MemberOrIvar {return= (_, {Typ.desc= Tptr _}) as return} ->
(return, []) (return, [])
@ -973,7 +975,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
(* assignment. *) (* assignment. *)
(* As no node is created here ids are passed to the parent *) (* As no node is created here ids are passed to the parent *)
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let res_instr = Sil.Load {id; e= exp1; root_typ= typ1; loc= sil_loc} in let res_instr = Sil.Load {id; e= exp1; root_typ= typ1; typ= typ1; loc= sil_loc} in
([res_instr], Exp.Var id) ([res_instr], Exp.Var id)
else ([], exp_op) else ([], exp_op)
in in
@ -1553,7 +1555,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
do_branch false exp2 var_typ res_trans_cond.control.leaf_nodes join_node pvar do_branch false exp2 var_typ res_trans_cond.control.leaf_nodes join_node pvar
in in
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let instrs = [Sil.Load {id; e= Exp.Lvar pvar; root_typ= var_typ; loc= sil_loc}] in let instrs =
[Sil.Load {id; e= Exp.Lvar pvar; root_typ= var_typ; typ= var_typ; loc= sil_loc}]
in
mk_trans_result (Exp.Var id, typ) mk_trans_result (Exp.Var id, typ)
{ root_nodes= res_trans_cond.control.root_nodes { root_nodes= res_trans_cond.control.root_nodes
; leaf_nodes= [join_node] ; leaf_nodes= [join_node]
@ -2616,7 +2620,12 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
let pvar = Pvar.mk (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 id = Ident.create_fresh Ident.knormal in
let instr = let instr =
Sil.Load {id; e= Exp.Lvar pvar; root_typ= ret_param_typ; loc= sil_loc} Sil.Load
{ id
; e= Exp.Lvar pvar
; root_typ= ret_param_typ
; typ= ret_param_typ
; loc= sil_loc }
in in
let ret_typ = let ret_typ =
match ret_param_typ.desc with Typ.Tptr (t, _) -> t | _ -> assert false match ret_param_typ.desc with Typ.Tptr (t, _) -> t | _ -> assert false

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

@ -401,7 +401,7 @@ let create_call_to_free_cf sil_loc exp typ =
let dereference_var_sil (exp, typ) sil_loc = let dereference_var_sil (exp, typ) sil_loc =
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let sil_instr = Sil.Load {id; e= exp; root_typ= typ; loc= sil_loc} in let sil_instr = Sil.Load {id; e= exp; root_typ= typ; typ; loc= sil_loc} in
([sil_instr], Exp.Var id) ([sil_instr], Exp.Var id)
@ -548,7 +548,7 @@ let define_condition_side_effects ((e_cond_exp, e_cond_typ) as e_cond) instrs_co
| Exp.Lvar pvar -> | Exp.Lvar pvar ->
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
( (Exp.Var id, e_cond_typ) ( (Exp.Var id, e_cond_typ)
, [Sil.Load {id; e= Exp.Lvar pvar; root_typ= e_cond_typ; loc= sil_loc}] ) , [Sil.Load {id; e= Exp.Lvar pvar; root_typ= e_cond_typ; typ= e_cond_typ; loc= sil_loc}] )
| _ -> | _ ->
(e_cond, instrs_cond) (e_cond, instrs_cond)
@ -581,7 +581,7 @@ module Self = struct
in in
let e = Exp.Lvar (Pvar.mk (Mangled.from_string CFrontend_config.self) procname) in let e = Exp.Lvar (Pvar.mk (Mangled.from_string CFrontend_config.self) procname) in
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
(t', Exp.Var id, [Sil.Load {id; e; root_typ= t'; loc}]) (t', Exp.Var id, [Sil.Load {id; e; root_typ= t'; typ= t'; loc}])
in in
Some (mk_trans_result (self_expr, typ) {empty_control with instrs}) Some (mk_trans_result (self_expr, typ) {empty_control with instrs})
else None else None

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

@ -461,9 +461,9 @@ let builtin_new = Exp.Const (Const.Cfun BuiltinDecl.__new)
let builtin_get_array_length = Exp.Const (Const.Cfun BuiltinDecl.__get_array_length) let builtin_get_array_length = Exp.Const (Const.Cfun BuiltinDecl.__get_array_length)
let create_sil_deref exp typ loc = let create_sil_deref exp ~root_typ ~typ loc =
let no_id = Ident.create_none () in let no_id = Ident.create_none () in
Sil.Load {id= no_id; e= exp; root_typ= typ; loc} Sil.Load {id= no_id; e= exp; root_typ; typ; loc}
(** translate an expression used as an r-value *) (** translate an expression used as an r-value *)
@ -474,7 +474,9 @@ let rec expression (context : JContext.t) pc expr =
let type_of_expr = JTransType.expr_type context expr in let type_of_expr = JTransType.expr_type context expr in
let trans_var pvar = let trans_var pvar =
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let sil_instr = Sil.Load {id; e= Exp.Lvar pvar; root_typ= type_of_expr; loc} in let sil_instr =
Sil.Load {id; e= Exp.Lvar pvar; root_typ= type_of_expr; typ= type_of_expr; loc}
in
([sil_instr], Exp.Var id, type_of_expr) ([sil_instr], Exp.Var id, type_of_expr)
in in
match expr with match expr with
@ -501,7 +503,7 @@ let rec expression (context : JContext.t) pc expr =
let array_typ_no_ptr = let array_typ_no_ptr =
match type_of_ex.Typ.desc with Typ.Tptr (typ, _) -> typ | _ -> type_of_ex match type_of_ex.Typ.desc with Typ.Tptr (typ, _) -> typ | _ -> type_of_ex
in in
let deref = create_sil_deref sil_ex array_typ_no_ptr loc in let deref = create_sil_deref sil_ex ~root_typ:array_typ_no_ptr ~typ:type_of_expr loc in
let args = [(sil_ex, type_of_ex)] in let args = [(sil_ex, type_of_ex)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let ret_typ = Typ.mk (Tint IInt) in let ret_typ = Typ.mk (Tint IInt) in
@ -546,10 +548,13 @@ let rec expression (context : JContext.t) pc expr =
| JBir.ArrayLoad _ -> | JBir.ArrayLoad _ ->
(* add an instruction that dereferences the array *) (* add an instruction that dereferences the array *)
let array_typ = Typ.mk_array type_of_expr in let array_typ = Typ.mk_array type_of_expr in
let deref_array_instr = create_sil_deref sil_ex1 array_typ loc in let deref_array_instr =
create_sil_deref sil_ex1 ~root_typ:array_typ ~typ:type_of_expr loc
in
let id = Ident.create_fresh Ident.knormal in let id = Ident.create_fresh Ident.knormal in
let load_instr = let load_instr =
Sil.Load {id; e= Exp.Lindex (sil_ex1, sil_ex2); root_typ= type_of_expr; loc} Sil.Load
{id; e= Exp.Lindex (sil_ex1, sil_ex2); root_typ= type_of_expr; typ= type_of_expr; loc}
in in
let instrs = (instrs1 @ (deref_array_instr :: instrs2)) @ [load_instr] in let instrs = (instrs1 @ (deref_array_instr :: instrs2)) @ [load_instr] in
(instrs, Exp.Var id, type_of_expr) (instrs, Exp.Var id, type_of_expr)
@ -563,7 +568,9 @@ let rec expression (context : JContext.t) pc expr =
let sil_type = JTransType.get_class_type_no_pointer program tenv cn in let sil_type = JTransType.get_class_type_no_pointer program tenv cn in
let sil_expr = Exp.Lfield (sil_expr, field_name, sil_type) in let sil_expr = Exp.Lfield (sil_expr, field_name, sil_type) in
let tmp_id = Ident.create_fresh Ident.knormal in let tmp_id = Ident.create_fresh Ident.knormal in
let lderef_instr = Sil.Load {id= tmp_id; e= sil_expr; root_typ= sil_type; loc} in let lderef_instr =
Sil.Load {id= tmp_id; e= sil_expr; root_typ= sil_type; typ= type_of_expr; loc}
in
(instrs @ [lderef_instr], Exp.Var tmp_id, type_of_expr) (instrs @ [lderef_instr], Exp.Var tmp_id, type_of_expr)
| JBir.StaticField (cn, fs) -> | JBir.StaticField (cn, fs) ->
let class_exp = let class_exp =
@ -581,7 +588,9 @@ let rec expression (context : JContext.t) pc expr =
else else
let sil_expr = Exp.Lfield (sil_expr, field_name, sil_type) in let sil_expr = Exp.Lfield (sil_expr, field_name, sil_type) in
let tmp_id = Ident.create_fresh Ident.knormal in let tmp_id = Ident.create_fresh Ident.knormal in
let lderef_instr = Sil.Load {id= tmp_id; e= sil_expr; root_typ= sil_type; loc} in let lderef_instr =
Sil.Load {id= tmp_id; e= sil_expr; root_typ= sil_type; typ= type_of_expr; loc}
in
(instrs @ [lderef_instr], Exp.Var tmp_id, type_of_expr) (instrs @ [lderef_instr], Exp.Var tmp_id, type_of_expr)
@ -636,7 +645,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex
let obj_typ_no_ptr = let obj_typ_no_ptr =
match sil_obj_type.Typ.desc with Typ.Tptr (typ, _) -> typ | _ -> sil_obj_type match sil_obj_type.Typ.desc with Typ.Tptr (typ, _) -> typ | _ -> sil_obj_type
in in
[create_sil_deref sil_obj_expr obj_typ_no_ptr loc] [create_sil_deref sil_obj_expr ~root_typ:obj_typ_no_ptr ~typ:sil_obj_type loc]
| _ -> | _ ->
[] []
in in
@ -847,7 +856,7 @@ let instruction (context : JContext.t) pc instr : translation =
, CallFlags.default ) , CallFlags.default )
in in
let typ_no_ptr = match sil_type.Typ.desc with Typ.Tptr (typ, _) -> typ | _ -> sil_type in let typ_no_ptr = match sil_type.Typ.desc with Typ.Tptr (typ, _) -> typ | _ -> sil_type in
let deref_instr = create_sil_deref sil_expr typ_no_ptr loc in let deref_instr = create_sil_deref sil_expr ~root_typ:typ_no_ptr ~typ:sil_type loc in
let node_kind = Procdesc.Node.Stmt_node node_desc in let node_kind = Procdesc.Node.Stmt_node node_desc in
Instr (create_node node_kind (instrs @ [deref_instr; instr])) Instr (create_node node_kind (instrs @ [deref_instr; instr]))
in in

2
infer/src/java/jTransExn.ml
Unescape View File

@ -33,7 +33,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
let id_exn_val = Ident.create_fresh Ident.knormal in let id_exn_val = Ident.create_fresh Ident.knormal in
let create_entry_node loc = let create_entry_node loc =
let instr_get_ret_val = let instr_get_ret_val =
Sil.Load {id= id_ret_val; e= Exp.Lvar ret_var; root_typ= ret_type; loc} Sil.Load {id= id_ret_val; e= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; loc}
in in
let instr_deactivate_exn = let instr_deactivate_exn =
Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= Exp.null; loc} Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= Exp.null; loc}

10
infer/src/topl/ToplMonitor.ml
Unescape View File

@ -120,7 +120,8 @@ let pure_exp e : Exp.t * Sil.instr list =
let subst = List.map ~f:(function e, id -> (e, Exp.Var id)) pairs in let subst = List.map ~f:(function e, id -> (e, Exp.Var id)) pairs in
let e' = Sil.exp_replace_exp subst e in let e' = Sil.exp_replace_exp subst e in
let mk_load (e, id) = let mk_load (e, id) =
Sil.Load {id; e; root_typ= ToplUtils.any_type; loc= sourcefile_location ()} Sil.Load
{id; e; root_typ= ToplUtils.any_type; typ= ToplUtils.any_type; loc= sourcefile_location ()}
in in
let loads = List.map ~f:mk_load pairs in let loads = List.map ~f:mk_load pairs in
(e', loads) (e', loads)
@ -168,7 +169,12 @@ let stmt_node instrs : node_generator =
let sil_assign lhs rhs = let sil_assign lhs rhs =
let tempvar = Ident.create_fresh Ident.knormal in let tempvar = Ident.create_fresh Ident.knormal in
[ Sil.Load {id= tempvar; e= rhs; root_typ= ToplUtils.any_type; loc= sourcefile_location ()} [ Sil.Load
{ id= tempvar
; e= rhs
; root_typ= ToplUtils.any_type
; typ= ToplUtils.any_type
; loc= sourcefile_location () }
; Sil.Store ; Sil.Store
{e1= lhs; root_typ= ToplUtils.any_type; e2= Exp.Var tempvar; loc= sourcefile_location ()} ] {e1= lhs; root_typ= ToplUtils.any_type; e2= Exp.Var tempvar; loc= sourcefile_location ()} ]

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

@ -69,7 +69,7 @@ module StructuredSil = struct
let unknown_exp = var_of_str "__unknown__" let unknown_exp = var_of_str "__unknown__"
let make_load ~rhs_typ lhs_id rhs_exp = let make_load ~rhs_typ lhs_id rhs_exp =
Cmd (Sil.Load {id= lhs_id; e= rhs_exp; root_typ= rhs_typ; loc= dummy_loc}) Cmd (Sil.Load {id= lhs_id; e= rhs_exp; root_typ= rhs_typ; typ= rhs_typ; loc= dummy_loc})
let make_set ~rhs_typ ~lhs_exp ~rhs_exp = let make_set ~rhs_typ ~lhs_exp ~rhs_exp =

Write Preview
Loading…
Cancel
Save