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

[infer] Add type field in Sil.Store

Browse Source 
Summary:
It adds typ field in Sil.Store.  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 store statement, the type of RHS is better to be given.

Reviewed By: dulmarod

Differential Revision: D17185346

fbshipit-source-id: f0945c40f
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 41aa20e2b6
commit 3916d1b3bc
12 changed files with 119 additions and 52 deletions
Show Stats Download Patch File Download Diff File

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

@ -85,15 +85,15 @@ let inline_synthetic_method ((ret_id, _) as ret) etl pdesc loc_call : Sil.instr
{id= ret_id; e= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt; typ; loc= loc_call}
in
found instr instr'
| ( Sil.Store {e1= Exp.Lfield (_, fn, ft); root_typ= bt}
| ( Sil.Store {e1= Exp.Lfield (_, fn, ft); root_typ; typ}
, [(* setter for fields *) (e1, _); (e2, _)] ) ->
let instr' = Sil.Store {e1= Exp.Lfield (e1, fn, ft); root_typ= bt; e2; loc= loc_call} in
let instr' = Sil.Store {e1= Exp.Lfield (e1, fn, ft); root_typ; typ; e2; loc= loc_call} in
found instr instr'
| Sil.Store {e1= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt}, [(e1, _)]
| Sil.Store {e1= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ; typ}, [(e1, _)]
when Pvar.is_global pvar ->
(* setter for static fields *)
let instr' =
Sil.Store {e1= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt; e2= e1; loc= loc_call}
Sil.Store {e1= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ; typ; e2= e1; loc= loc_call}
in
found instr instr'
| Sil.Call (_, Exp.Const (Const.Cfun pn), etl', _, cf), _

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

@ -50,12 +50,17 @@ type instr =
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; typ: Typ.t; e2: Exp.t; loc: Location.t}
(** Store the value of an expression into the heap.
[*exp1:root_typ = exp2] where
[*exp1:typ(root_typ) = exp2] where
[exp1] is an expression denoting a heap address
[typ] is typ of [*exp1] and [exp2]
[root_typ] is the root type of [exp1]
[exp2] is the expression whose value is stored. *)
[exp2] is the expression whose value is stored.
The [root_typ] is deprecated: it is broken in C/C++. We are removing [root_typ] in the
future, so please use [typ] instead. *)
| Prune of Exp.t * Location.t * bool * if_kind
(** prune the state based on [exp=1], the boolean indicates whether true branch *)
| Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t
@ -415,17 +420,17 @@ let pp_instr_metadata pe f = function
let pp_instr ~print_types pe0 f instr =
let pp_typ = if print_types then Typ.pp_full else Typ.pp in
let pp_root ~typ ~root_typ f =
if not (Typ.equal typ root_typ) then F.fprintf f "(root %a)" (pp_typ pe0) root_typ
in
color_wrapper pe0 f instr ~f:(fun pe f instr ->
match instr with
| Load {id; e; root_typ; typ; loc} ->
let pp_root f =
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} ->
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_typ pe0) typ (pp_root ~typ ~root_typ) Location.pp loc
| Store {e1; root_typ; typ; e2; loc} ->
F.fprintf f "*%a:%a%t=%a [%a]" (pp_exp_printenv ~print_types pe) e1 (pp_typ pe0) root_typ
(pp_root ~typ ~root_typ) (pp_exp_printenv ~print_types pe) e2 Location.pp loc
| Prune (cond, loc, true_branch, _) ->
F.fprintf f "PRUNE(%a, %b); [%a]" (pp_exp_printenv ~print_types pe) cond true_branch
Location.pp loc
@ -1280,11 +1285,11 @@ let instr_sub_ids ~sub_id_binders f instr =
let rhs_exp' = exp_sub_ids f rhs_exp in
if phys_equal id' id && phys_equal rhs_exp' rhs_exp then instr
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; typ; e2= rhs_exp; loc} ->
let lhs_exp' = exp_sub_ids f lhs_exp in
let rhs_exp' = exp_sub_ids f rhs_exp in
if phys_equal lhs_exp' lhs_exp && phys_equal rhs_exp' rhs_exp then instr
else Store {e1= lhs_exp'; root_typ; e2= rhs_exp'; loc}
else Store {e1= lhs_exp'; root_typ; typ; e2= rhs_exp'; loc}
| Call (((id, typ) as ret_id_typ), fun_exp, actuals, call_flags, loc) ->
let ret_id' =
if sub_id_binders then

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

@ -48,12 +48,17 @@ type instr =
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; typ: Typ.t; e2: Exp.t; loc: Location.t}
(** Store the value of an expression into the heap.
[*exp1:root_typ = exp2] where
[*exp1:typ(root_typ) = exp2] where
[exp1] is an expression denoting a heap address
[typ] is typ of [*exp1] and [exp2]
[root_typ] is the root type of [exp1]
[exp2] is the expression whose value is stored. *)
[exp2] is the expression whose value is stored.
The [root_typ] is deprecated: it is broken in C/C++. We are removing [root_typ] in the
future, so please use [typ] instead. *)
| Prune of Exp.t * Location.t * bool * if_kind
(** prune the state based on [exp=1], the boolean indicates whether true branch *)
| Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t

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

@ -88,7 +88,11 @@ let with_formals_types_proc callee_pdesc resolved_pdesc substitutions =
| Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= origin_exp; loc} ->
let set_instr =
Sil.Store
{e1= convert_exp assignee_exp; root_typ= origin_typ; e2= convert_exp origin_exp; loc}
{ e1= convert_exp assignee_exp
; root_typ= origin_typ
; typ= origin_typ
; e2= convert_exp origin_exp
; loc }
in
Some set_instr
| Sil.Call
@ -235,12 +239,18 @@ let with_block_args_instrs resolved_pdesc substitutions =
get_block_name_and_load_captured_vars_instrs block_param loc
in
let closure = Exp.Closure {name= block_name; captured_vars= id_exp_typs} in
let instr = Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= closure; loc} in
let instr =
Sil.Store {e1= assignee_exp; root_typ= origin_typ; typ= origin_typ; e2= closure; loc}
in
((remove_temps_instr :: instr :: load_instrs) @ instrs, id_map)
| Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= origin_exp; loc} ->
let set_instr =
Sil.Store
{e1= convert_exp assignee_exp; root_typ= origin_typ; e2= convert_exp origin_exp; loc}
{ e1= convert_exp assignee_exp
; root_typ= origin_typ
; typ= origin_typ
; e2= convert_exp origin_exp
; loc }
in
(set_instr :: instrs, id_map)
| Sil.Call (return_ids, Exp.Var id, origin_args, loc, call_flags) -> (

10
infer/src/biabduction/BuiltinDefn.ml
Unescape View File

@ -19,7 +19,7 @@ let execute___builtin_va_arg {Builtin.summary; tenv; prop_; path; args; loc; exe
Builtin.ret_typ =
match args with
| [(lexp3, typ3)] ->
let instr' = Sil.Store {e1= lexp3; root_typ= typ3; e2= Exp.zero; loc} in
let instr' = Sil.Store {e1= lexp3; root_typ= typ3; typ= typ3; e2= Exp.zero; loc} in
SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton instr')
[(prop_, path)]
| _ ->
@ -627,7 +627,11 @@ let execute___cxx_typeid ({Builtin.summary; tenv; prop_; args; loc; exe_env} as
let typ_string = Typ.to_string typ in
let set_instr =
Sil.Store
{e1= field_exp; root_typ= Typ.mk Tvoid; e2= Exp.Const (Const.Cstr typ_string); loc}
{ e1= field_exp
; root_typ= Typ.mk Tvoid
; typ= Typ.mk Tvoid
; e2= Exp.Const (Const.Cstr typ_string)
; loc }
in
SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton set_instr) res
| _ ->
@ -767,6 +771,7 @@ let execute___infer_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_env
Sil.Store
{ e1= Exp.Lvar Sil.custom_error
; root_typ= Typ.mk Tvoid
; typ= Typ.mk Tvoid
; e2= Exp.Const (Const.Cstr error_str)
; loc }
in
@ -787,6 +792,7 @@ let execute___assert_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_en
Sil.Store
{ e1= Exp.Lvar Sil.custom_error
; root_typ= Typ.mk Tvoid
; typ= Typ.mk Tvoid
; e2= Exp.Const (Const.Cstr error_str)
; loc }
in

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

@ -41,7 +41,7 @@ let compound_assignment_binary_operation_instruction boi_kind (e1, t1) typ e2 lo
in
let id = Ident.create_fresh Ident.knormal in
[ 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; typ; e2= Exp.BinOp (bop, Exp.Var id, e2); loc} ]
in
(e1, instrs)
@ -105,7 +105,7 @@ let binary_operation_instruction source_range boi ((e1, t1) as e1_with_typ) typ
| `LOr ->
(binop_exp Binop.LOr, [])
| `Assign ->
(e1, [Sil.Store {e1; root_typ= typ; e2; loc}])
(e1, [Sil.Store {e1; root_typ= typ; typ; e2; loc}])
| `Cmp ->
CFrontend_errors.unimplemented __POS__ source_range "C++20 spaceship operator <=>"
(* C++20 spaceship operator <=>, TODO *)
@ -132,7 +132,7 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
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 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; typ; e2= e_plus_1; loc}])
| `PreInc ->
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Load {id; e; root_typ= typ; typ; loc} in
@ -141,7 +141,7 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
let exp =
if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_plus_1
in
(exp, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_plus_1; loc}])
(exp, [instr1; Sil.Store {e1= e; root_typ= typ; typ; e2= e_plus_1; loc}])
| `PostDec ->
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Load {id; e; root_typ= typ; typ; loc} in
@ -149,7 +149,7 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ)
in
let e_minus_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_minus_1; loc}])
(Exp.Var id, [instr1; Sil.Store {e1= e; root_typ= typ; typ; e2= e_minus_1; loc}])
| `PreDec ->
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Load {id; e; root_typ= typ; typ; loc} in
@ -160,7 +160,7 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
let exp =
if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_minus_1
in
(exp, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_minus_1; loc}])
(exp, [instr1; Sil.Store {e1= e; root_typ= typ; typ; e2= e_minus_1; loc}])
| `Not ->
(un_exp Unop.BNot, [])
| `Minus ->

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

@ -423,7 +423,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
|> mk_trans_result exp_typ
| Tint _ | Tfloat _ | Tptr _ ->
let zero_exp = Exp.zero_of_type_exn typ in
let instrs = [Sil.Store {e1= exp; root_typ= typ; e2= zero_exp; loc= sil_loc}] in
let instrs = [Sil.Store {e1= exp; root_typ= typ; typ; e2= zero_exp; loc= sil_loc}] in
mk_trans_result (exp, typ) {empty_control with instrs}
| Tfun _ | Tvoid | Tarray _ | TVar _ ->
CFrontend_errors.unimplemented __POS__ stmt_info.Clang_ast_t.si_source_range
@ -1506,7 +1506,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
e'
in
let temp_var = Exp.Lvar pvar in
let set_temp_var = [Sil.Store {e1= temp_var; root_typ= var_typ; e2= e'; loc= sil_loc}] in
let set_temp_var =
[Sil.Store {e1= temp_var; root_typ= var_typ; typ= var_typ; e2= e'; loc= sil_loc}]
in
let temp_return = (temp_var, var_typ) in
let tmp_var_res_trans =
mk_trans_result temp_return {empty_control with instrs= set_temp_var}
@ -2327,7 +2329,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
let sil_e1', ie_typ = res_trans_ie.return in
Some
{ empty_control with
instrs= [Sil.Store {e1= var_exp; root_typ= ie_typ; e2= sil_e1'; loc= sil_loc}] }
instrs=
[ Sil.Store
{e1= var_exp; root_typ= ie_typ; typ= ie_typ; e2= sil_e1'; loc= sil_loc} ] }
in
let pre_init_opt =
match var_exp with
@ -2642,7 +2646,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
if List.exists ~f:(Exp.equal ret_exp) res_trans_stmt.control.initd_exps then []
else
let sil_expr, _ = res_trans_stmt.return in
[Sil.Store {e1= ret_exp; root_typ= ret_type; e2= sil_expr; loc= sil_loc}]
[ Sil.Store
{e1= ret_exp; root_typ= ret_type; typ= ret_typ; e2= sil_expr; loc= sil_loc} ]
in
let instrs = var_instrs @ res_trans_stmt.control.instrs @ ret_instrs in
let ret_node = mk_ret_node instrs in

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

@ -679,7 +679,8 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex
let ret_id = Ident.create_fresh Ident.knormal in
let call_instr = Sil.Call ((ret_id, return_type), callee_fun, call_args, loc, call_flags) in
let set_instr =
Sil.Store {e1= Exp.Lvar sil_var; root_typ= return_type; e2= Exp.Var ret_id; loc}
Sil.Store
{e1= Exp.Lvar sil_var; root_typ= return_type; typ= return_type; e2= Exp.Var ret_id; loc}
in
instrs @ [call_instr; set_instr]
in
@ -869,7 +870,9 @@ let instruction (context : JContext.t) pc instr : translation =
| AffectVar (var, expr) ->
let stml, sil_expr, sil_type = expression context pc expr in
let pvar = JContext.set_pvar context var sil_type in
let sil_instr = Sil.Store {e1= Exp.Lvar pvar; root_typ= sil_type; e2= sil_expr; loc} in
let sil_instr =
Sil.Store {e1= Exp.Lvar pvar; root_typ= sil_type; typ= sil_type; e2= sil_expr; loc}
in
let node_kind = Procdesc.Node.Stmt_node MethodBody in
let node = create_node node_kind (stml @ [sil_instr]) in
Instr node
@ -883,7 +886,8 @@ let instruction (context : JContext.t) pc instr : translation =
let stml, sil_expr, _ = expression context pc expr in
let sil_instrs =
let return_instr =
Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_expr; loc}
Sil.Store
{e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_expr; loc}
in
if return_not_null () then [assume_not_null loc sil_expr; return_instr]
else [return_instr]
@ -900,6 +904,7 @@ let instruction (context : JContext.t) pc instr : translation =
Sil.Store
{ e1= Exp.Lindex (sil_expr_array, sil_expr_index)
; root_typ= value_typ
; typ= value_typ
; e2= sil_expr_value
; loc }
in
@ -909,13 +914,14 @@ let instruction (context : JContext.t) pc instr : translation =
Instr node
| AffectField (e_lhs, cn, fs, e_rhs) ->
let stml1, sil_expr_lhs, _ = expression context pc e_lhs in
let stml2, sil_expr_rhs, _ = expression context pc e_rhs in
let stml2, sil_expr_rhs, rhs_typ = expression context pc e_rhs in
let field_name = get_field_name program false tenv cn fs in
let type_of_the_surrounding_class = JTransType.get_class_type_no_pointer program tenv cn in
let type_of_the_root_of_e_lhs = type_of_the_surrounding_class in
let expr_off = Exp.Lfield (sil_expr_lhs, field_name, type_of_the_surrounding_class) in
let sil_instr =
Sil.Store {e1= expr_off; root_typ= type_of_the_root_of_e_lhs; e2= sil_expr_rhs; loc}
Sil.Store
{e1= expr_off; root_typ= type_of_the_root_of_e_lhs; typ= rhs_typ; e2= sil_expr_rhs; loc}
in
let node_kind = Procdesc.Node.Stmt_node MethodBody in
let node = create_node node_kind (stml1 @ stml2 @ [sil_instr]) in
@ -927,13 +933,14 @@ let instruction (context : JContext.t) pc instr : translation =
Exp.Lvar var_name
in
let stml1, sil_expr_lhs = ([], class_exp) in
let stml2, sil_expr_rhs, _ = expression context pc e_rhs in
let stml2, sil_expr_rhs, rhs_typ = expression context pc e_rhs in
let field_name = get_field_name program true tenv cn fs in
let type_of_the_surrounding_class = JTransType.get_class_type_no_pointer program tenv cn in
let type_of_the_root_of_e_lhs = type_of_the_surrounding_class in
let expr_off = Exp.Lfield (sil_expr_lhs, field_name, type_of_the_surrounding_class) in
let sil_instr =
Sil.Store {e1= expr_off; root_typ= type_of_the_root_of_e_lhs; e2= sil_expr_rhs; loc}
Sil.Store
{e1= expr_off; root_typ= type_of_the_root_of_e_lhs; typ= rhs_typ; e2= sil_expr_rhs; loc}
in
let node_kind = Procdesc.Node.Stmt_node MethodBody in
let node = create_node node_kind (stml1 @ stml2 @ [sil_instr]) in
@ -971,7 +978,9 @@ let instruction (context : JContext.t) pc instr : translation =
| Throw expr ->
let instrs, sil_expr, _ = expression context pc expr in
let sil_exn = Exp.Exn sil_expr in
let sil_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in
let sil_instr =
Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_exn; loc}
in
let node = create_node Procdesc.Node.throw_kind (instrs @ [sil_instr]) in
JContext.add_goto_jump context pc JContext.Exit ;
Instr node
@ -996,7 +1005,8 @@ let instruction (context : JContext.t) pc instr : translation =
in
let pvar = JContext.set_pvar context var class_type in
let set_instr =
Sil.Store {e1= Exp.Lvar pvar; root_typ= class_type; e2= Exp.Var ret_id; loc}
Sil.Store
{e1= Exp.Lvar pvar; root_typ= class_type; typ= class_type; e2= Exp.Var ret_id; loc}
in
let instrs = (new_instr :: call_instrs) @ [set_instr] in
let node_kind = create_node_kind constr_procname in
@ -1014,7 +1024,12 @@ let instruction (context : JContext.t) pc instr : translation =
Sil.Call ((ret_id, array_type), builtin_new_array, call_args, loc, CallFlags.default)
in
let set_instr =
Sil.Store {e1= Exp.Lvar array_name; root_typ= array_type; e2= Exp.Var ret_id; loc}
Sil.Store
{ e1= Exp.Lvar array_name
; root_typ= array_type
; typ= array_type
; e2= Exp.Var ret_id
; loc }
in
let node_kind = Procdesc.Node.Stmt_node MethodBody in
let node = create_node node_kind (instrs @ [call_instr; set_instr]) in
@ -1121,7 +1136,9 @@ let instruction (context : JContext.t) pc instr : translation =
Typ.Procname.Java.Static
in
let sil_exn = Exp.Exn (Exp.Var ret_id) in
let set_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in
let set_instr =
Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_exn; loc}
in
let npe_instrs = instrs @ [sil_prune_null] @ (new_instr :: call_instrs) @ [set_instr] in
create_node npe_kind npe_instrs
in
@ -1181,7 +1198,9 @@ let instruction (context : JContext.t) pc instr : translation =
[] I_Special Typ.Procname.Java.Static
in
let sil_exn = Exp.Exn (Exp.Var ret_id) in
let set_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in
let set_instr =
Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_exn; loc}
in
let out_of_bound_instrs =
instrs @ [sil_assume_out_of_bound] @ (new_instr :: call_instrs) @ [set_instr]
in
@ -1229,7 +1248,9 @@ let instruction (context : JContext.t) pc instr : translation =
[] I_Special Typ.Procname.Java.Static
in
let sil_exn = Exp.Exn (Exp.Var ret_id) in
let set_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in
let set_instr =
Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_exn; loc}
in
let cce_instrs =
instrs @ [call; asssume_not_instance_of] @ (new_instr :: call_instrs) @ [set_instr]
in

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

@ -36,7 +36,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
Sil.Load {id= id_ret_val; e= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; loc}
in
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; typ= ret_type; e2= Exp.null; loc}
in
let instr_unwrap_ret_val =
let unwrap_builtin = Exp.Const (Const.Cfun BuiltinDecl.__unwrap_exception) in
@ -101,11 +101,20 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
in
let instr_set_catch_var =
let catch_var = JContext.set_pvar context handler.JBir.e_catch_var ret_type in
Sil.Store {e1= Exp.Lvar catch_var; root_typ= ret_type; e2= Exp.Var id_exn_val; loc}
Sil.Store
{ e1= Exp.Lvar catch_var
; root_typ= ret_type
; typ= ret_type
; e2= Exp.Var id_exn_val
; loc }
in
let instr_rethrow_exn =
Sil.Store
{e1= Exp.Lvar ret_var; root_typ= ret_type; e2= Exp.Exn (Exp.Var id_exn_val); loc}
{ e1= Exp.Lvar ret_var
; root_typ= ret_type
; typ= ret_type
; e2= Exp.Exn (Exp.Var id_exn_val)
; loc }
in
let node_kind_true =
Procdesc.Node.Prune_node (true, if_kind, PruneNodeKind_ExceptionHandler)

1
infer/src/topl/Topl.ml
Unescape View File

@ -85,6 +85,7 @@ let set_transitions loc active_transitions =
Sil.Store
{ e1= ToplUtils.static_var (ToplName.transition i)
; root_typ= ToplUtils.topl_class_typ
; typ= ToplUtils.topl_class_typ
; e2= value
; loc }
in

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

@ -176,7 +176,11 @@ let sil_assign lhs rhs =
; typ= ToplUtils.any_type
; loc= sourcefile_location () }
; Sil.Store
{e1= lhs; root_typ= ToplUtils.any_type; e2= Exp.Var tempvar; loc= sourcefile_location ()} ]
{ e1= lhs
; root_typ= ToplUtils.any_type
; typ= ToplUtils.any_type
; e2= Exp.Var tempvar
; loc= sourcefile_location () } ]
let assign lhs rhs : node_generator = stmt_node (sil_assign lhs rhs)
@ -258,6 +262,7 @@ let generate_execute_state automaton proc_name =
[ Sil.Store
{ e1= ToplUtils.static_var ToplName.state
; root_typ= Typ.mk (Tint IInt)
; typ= Typ.mk (Tint IInt)
; e2= Exp.int (IntLit.of_int transition.target)
; loc= sourcefile_location () } ]
:: step (ToplUtils.static_var ToplName.retval) transition.label.ToplAst.return

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

@ -73,7 +73,7 @@ module StructuredSil = struct
let make_set ~rhs_typ ~lhs_exp ~rhs_exp =
Cmd (Sil.Store {e1= lhs_exp; root_typ= rhs_typ; e2= rhs_exp; loc= dummy_loc})
Cmd (Sil.Store {e1= lhs_exp; root_typ= rhs_typ; typ= rhs_typ; e2= rhs_exp; loc= dummy_loc})
let make_call ?(procname = dummy_procname) ?return:return_opt args =

Write Preview
Loading…
Cancel
Save