|
|
|
@ -298,9 +298,9 @@ let create_local_procdesc program linereader cfg tenv node m =
|
|
|
|
} in
|
|
|
|
} in
|
|
|
|
Cfg.Procdesc.create cfg proc_attributes in
|
|
|
|
Cfg.Procdesc.create cfg proc_attributes in
|
|
|
|
let start_kind = Cfg.Node.Start_node procdesc in
|
|
|
|
let start_kind = Cfg.Node.Start_node procdesc in
|
|
|
|
let start_node = Cfg.Node.create cfg Location.dummy start_kind [] procdesc [] in
|
|
|
|
let start_node = Cfg.Node.create cfg Location.dummy start_kind [] procdesc in
|
|
|
|
let exit_kind = (Cfg.Node.Exit_node procdesc) in
|
|
|
|
let exit_kind = (Cfg.Node.Exit_node procdesc) in
|
|
|
|
let exit_node = Cfg.Node.create cfg Location.dummy exit_kind [] procdesc [] in
|
|
|
|
let exit_node = Cfg.Node.create cfg Location.dummy exit_kind [] procdesc in
|
|
|
|
Cfg.Node.set_succs_exn cfg start_node [exit_node] [exit_node];
|
|
|
|
Cfg.Node.set_succs_exn cfg start_node [exit_node] [exit_node];
|
|
|
|
Cfg.Procdesc.set_start_node procdesc start_node;
|
|
|
|
Cfg.Procdesc.set_start_node procdesc start_node;
|
|
|
|
Cfg.Procdesc.set_exit_node procdesc exit_node
|
|
|
|
Cfg.Procdesc.set_exit_node procdesc exit_node
|
|
|
|
@ -346,11 +346,11 @@ let create_local_procdesc program linereader cfg tenv node m =
|
|
|
|
} in
|
|
|
|
} in
|
|
|
|
Cfg.Procdesc.create cfg proc_attributes in
|
|
|
|
Cfg.Procdesc.create cfg proc_attributes in
|
|
|
|
let start_kind = Cfg.Node.Start_node procdesc in
|
|
|
|
let start_kind = Cfg.Node.Start_node procdesc in
|
|
|
|
let start_node = Cfg.Node.create cfg loc_start start_kind [] procdesc [] in
|
|
|
|
let start_node = Cfg.Node.create cfg loc_start start_kind [] procdesc in
|
|
|
|
let exit_kind = (Cfg.Node.Exit_node procdesc) in
|
|
|
|
let exit_kind = (Cfg.Node.Exit_node procdesc) in
|
|
|
|
let exit_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc [] in
|
|
|
|
let exit_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc in
|
|
|
|
let exn_kind = Cfg.Node.exn_sink_kind in
|
|
|
|
let exn_kind = Cfg.Node.exn_sink_kind in
|
|
|
|
let exn_node = Cfg.Node.create cfg loc_exit exn_kind [] procdesc [] in
|
|
|
|
let exn_node = Cfg.Node.create cfg loc_exit exn_kind [] procdesc in
|
|
|
|
JContext.add_exn_node proc_name exn_node;
|
|
|
|
JContext.add_exn_node proc_name exn_node;
|
|
|
|
Cfg.Procdesc.set_start_node procdesc start_node;
|
|
|
|
Cfg.Procdesc.set_start_node procdesc start_node;
|
|
|
|
Cfg.Procdesc.set_exit_node procdesc exit_node;
|
|
|
|
Cfg.Procdesc.set_exit_node procdesc exit_node;
|
|
|
|
@ -404,8 +404,7 @@ let builtin_get_array_size =
|
|
|
|
|
|
|
|
|
|
|
|
let create_sil_deref exp typ loc =
|
|
|
|
let create_sil_deref exp typ loc =
|
|
|
|
let fresh_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let fresh_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let deref = Sil.Letderef (fresh_id, exp, typ, loc) in
|
|
|
|
Sil.Letderef (fresh_id, exp, typ, loc)
|
|
|
|
fresh_id, deref
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** translate an expression used as an r-value *)
|
|
|
|
(** translate an expression used as an r-value *)
|
|
|
|
let rec expression context pc expr =
|
|
|
|
let rec expression context pc expr =
|
|
|
|
@ -418,7 +417,7 @@ let rec expression context pc expr =
|
|
|
|
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.Letderef (id, Sil.Lvar pvar, type_of_expr, loc) in
|
|
|
|
let sil_instr = Sil.Letderef (id, Sil.Lvar pvar, type_of_expr, loc) in
|
|
|
|
([id], [sil_instr], Sil.Var id, type_of_expr) in
|
|
|
|
([sil_instr], Sil.Var id, type_of_expr) in
|
|
|
|
match expr with
|
|
|
|
match expr with
|
|
|
|
| JBir.Var (_, var) ->
|
|
|
|
| JBir.Var (_, var) ->
|
|
|
|
let pvar = (JContext.set_pvar context var type_of_expr) in
|
|
|
|
let pvar = (JContext.set_pvar context var type_of_expr) in
|
|
|
|
@ -431,27 +430,27 @@ let rec expression context pc expr =
|
|
|
|
let procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
|
|
|
|
let procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
|
|
|
|
let pvar = Pvar.mk varname procname in
|
|
|
|
let pvar = Pvar.mk varname procname in
|
|
|
|
trans_var pvar
|
|
|
|
trans_var pvar
|
|
|
|
| _ -> ([], [], Sil.Const (get_constant c), type_of_expr)
|
|
|
|
| _ -> ([], Sil.Const (get_constant c), type_of_expr)
|
|
|
|
end
|
|
|
|
end
|
|
|
|
| JBir.Unop (unop, ex) ->
|
|
|
|
| JBir.Unop (unop, ex) ->
|
|
|
|
let type_of_ex = JTransType.expr_type context ex in
|
|
|
|
let type_of_ex = JTransType.expr_type context ex in
|
|
|
|
let (ids, instrs, sil_ex, _) = expression context pc ex in
|
|
|
|
let (instrs, sil_ex, _) = expression context pc ex in
|
|
|
|
begin
|
|
|
|
begin
|
|
|
|
match unop with
|
|
|
|
match unop with
|
|
|
|
| JBir.Neg _ -> (ids, instrs, Sil.UnOp (Sil.Neg, sil_ex, Some type_of_expr), type_of_expr)
|
|
|
|
| JBir.Neg _ -> (instrs, Sil.UnOp (Sil.Neg, sil_ex, Some type_of_expr), type_of_expr)
|
|
|
|
| JBir.ArrayLength ->
|
|
|
|
| JBir.ArrayLength ->
|
|
|
|
let array_typ_no_ptr =
|
|
|
|
let array_typ_no_ptr =
|
|
|
|
match type_of_ex with
|
|
|
|
match type_of_ex with
|
|
|
|
| Sil.Tptr (typ, _) -> typ
|
|
|
|
| Sil.Tptr (typ, _) -> typ
|
|
|
|
| _ -> type_of_ex in
|
|
|
|
| _ -> type_of_ex in
|
|
|
|
let fresh_id, deref = create_sil_deref sil_ex array_typ_no_ptr loc in
|
|
|
|
let deref = create_sil_deref sil_ex array_typ_no_ptr 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 call_instr = Sil.Call([ret_id], builtin_get_array_size, args, loc, Sil.cf_default) in
|
|
|
|
let call_instr = Sil.Call([ret_id], builtin_get_array_size, args, loc, Sil.cf_default) in
|
|
|
|
(ids @ [fresh_id; ret_id], instrs @ [deref; call_instr], Sil.Var ret_id, type_of_expr)
|
|
|
|
(instrs @ [deref; call_instr], Sil.Var ret_id, type_of_expr)
|
|
|
|
| JBir.Conv conv ->
|
|
|
|
| JBir.Conv conv ->
|
|
|
|
let cast_ex = Sil.Cast (JTransType.cast_type conv, sil_ex) in
|
|
|
|
let cast_ex = Sil.Cast (JTransType.cast_type conv, sil_ex) in
|
|
|
|
(ids, instrs, cast_ex, type_of_expr)
|
|
|
|
(instrs, cast_ex, type_of_expr)
|
|
|
|
| JBir.InstanceOf ot | JBir.Cast ot ->
|
|
|
|
| JBir.InstanceOf ot | JBir.Cast ot ->
|
|
|
|
let subtypes =
|
|
|
|
let subtypes =
|
|
|
|
(match unop with
|
|
|
|
(match unop with
|
|
|
|
@ -469,42 +468,41 @@ let rec expression context pc expr =
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let call = Sil.Call([ret_id], builtin, args, loc, Sil.cf_default) in
|
|
|
|
let call = Sil.Call([ret_id], builtin, args, loc, Sil.cf_default) in
|
|
|
|
let res_ex = Sil.Var ret_id in
|
|
|
|
let res_ex = Sil.Var ret_id in
|
|
|
|
(ids @ [ret_id], instrs @ [call], res_ex, type_of_expr)
|
|
|
|
(instrs @ [call], res_ex, type_of_expr)
|
|
|
|
end
|
|
|
|
end
|
|
|
|
| JBir.Binop (binop, ex1, ex2) ->
|
|
|
|
| JBir.Binop (binop, ex1, ex2) ->
|
|
|
|
let (idl1, instrs1, sil_ex1, _) = expression context pc ex1
|
|
|
|
let (instrs1, sil_ex1, _) = expression context pc ex1
|
|
|
|
and (idl2, instrs2, sil_ex2, _) = expression context pc ex2 in
|
|
|
|
and (instrs2, sil_ex2, _) = expression context pc ex2 in
|
|
|
|
begin
|
|
|
|
begin
|
|
|
|
match binop with
|
|
|
|
match binop with
|
|
|
|
| JBir.ArrayLoad _ ->
|
|
|
|
| JBir.ArrayLoad _ ->
|
|
|
|
(* add an instruction that dereferences the array *)
|
|
|
|
(* add an instruction that dereferences the array *)
|
|
|
|
let array_typ = Sil.Tarray(type_of_expr, Sil.Var (Ident.create_fresh Ident.kprimed)) in
|
|
|
|
let array_typ = Sil.Tarray(type_of_expr, Sil.Var (Ident.create_fresh Ident.kprimed)) in
|
|
|
|
let fresh_id, deref_array_instr = create_sil_deref sil_ex1 array_typ loc in
|
|
|
|
let deref_array_instr = create_sil_deref sil_ex1 array_typ loc in
|
|
|
|
let id = Ident.create_fresh Ident.knormal in
|
|
|
|
let id = Ident.create_fresh Ident.knormal in
|
|
|
|
let letderef_instr =
|
|
|
|
let letderef_instr =
|
|
|
|
Sil.Letderef (id, Sil.Lindex (sil_ex1, sil_ex2), type_of_expr, loc) in
|
|
|
|
Sil.Letderef (id, Sil.Lindex (sil_ex1, sil_ex2), type_of_expr, loc) in
|
|
|
|
let ids = idl1 @ idl2 @ [fresh_id; id] in
|
|
|
|
|
|
|
|
let instrs = (instrs1 @ (deref_array_instr :: instrs2)) @ [letderef_instr] in
|
|
|
|
let instrs = (instrs1 @ (deref_array_instr :: instrs2)) @ [letderef_instr] in
|
|
|
|
ids, instrs, Sil.Var id, type_of_expr
|
|
|
|
instrs, Sil.Var id, type_of_expr
|
|
|
|
| other_binop ->
|
|
|
|
| other_binop ->
|
|
|
|
let sil_binop = get_binop other_binop in
|
|
|
|
let sil_binop = get_binop other_binop in
|
|
|
|
let sil_expr = Sil.BinOp (sil_binop, sil_ex1, sil_ex2) in
|
|
|
|
let sil_expr = Sil.BinOp (sil_binop, sil_ex1, sil_ex2) in
|
|
|
|
(idl1 @ idl2, (instrs1 @ instrs2), sil_expr, type_of_expr)
|
|
|
|
((instrs1 @ instrs2), sil_expr, type_of_expr)
|
|
|
|
end
|
|
|
|
end
|
|
|
|
| JBir.Field (ex, cn, fs) ->
|
|
|
|
| JBir.Field (ex, cn, fs) ->
|
|
|
|
let (idl, instrs, sil_expr, _) = expression context pc ex in
|
|
|
|
let (instrs, sil_expr, _) = expression context pc ex in
|
|
|
|
let field_name = get_field_name program false tenv cn fs in
|
|
|
|
let field_name = get_field_name program false tenv cn fs in
|
|
|
|
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 = Sil.Lfield (sil_expr, field_name, sil_type) in
|
|
|
|
let sil_expr = Sil.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.Letderef (tmp_id, sil_expr, sil_type, loc) in
|
|
|
|
let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in
|
|
|
|
(idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id, type_of_expr)
|
|
|
|
(instrs @ [lderef_instr], Sil.Var tmp_id, type_of_expr)
|
|
|
|
| JBir.StaticField (cn, fs) ->
|
|
|
|
| JBir.StaticField (cn, fs) ->
|
|
|
|
let class_exp =
|
|
|
|
let class_exp =
|
|
|
|
let classname = Mangled.from_string (JBasics.cn_name cn) in
|
|
|
|
let classname = Mangled.from_string (JBasics.cn_name cn) in
|
|
|
|
let var_name = Pvar.mk_global classname in
|
|
|
|
let var_name = Pvar.mk_global classname in
|
|
|
|
Sil.Lvar var_name in
|
|
|
|
Sil.Lvar var_name in
|
|
|
|
let (idl, instrs, sil_expr) = [], [], class_exp in
|
|
|
|
let (instrs, sil_expr) = [], class_exp in
|
|
|
|
let field_name = get_field_name program true tenv cn fs in
|
|
|
|
let field_name = get_field_name program true tenv cn fs in
|
|
|
|
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
|
|
|
|
if JTransStaticField.is_static_final_field context cn fs && use_static_final_fields context
|
|
|
|
if JTransStaticField.is_static_final_field context cn fs && use_static_final_fields context
|
|
|
|
@ -516,21 +514,21 @@ let rec expression context pc expr =
|
|
|
|
| Called p | Defined p -> p in
|
|
|
|
| Called p | Defined p -> p in
|
|
|
|
let field_type =
|
|
|
|
let field_type =
|
|
|
|
JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl) in
|
|
|
|
JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl) in
|
|
|
|
let idl', instrs', expr' =
|
|
|
|
let instrs', expr' =
|
|
|
|
JTransStaticField.translate_instr_static_field
|
|
|
|
JTransStaticField.translate_instr_static_field
|
|
|
|
context callee_procdesc fs field_type loc in
|
|
|
|
context callee_procdesc fs field_type loc in
|
|
|
|
idl', instrs', expr', type_of_expr
|
|
|
|
instrs', expr', type_of_expr
|
|
|
|
else
|
|
|
|
else
|
|
|
|
if JTransType.is_autogenerated_assert_field field_name
|
|
|
|
if JTransType.is_autogenerated_assert_field field_name
|
|
|
|
then
|
|
|
|
then
|
|
|
|
(* assume that reading from C.$assertionsDisabled always yields "false". this allows *)
|
|
|
|
(* assume that reading from C.$assertionsDisabled always yields "false". this allows *)
|
|
|
|
(* Infer to understand the assert keyword in the expected way *)
|
|
|
|
(* Infer to understand the assert keyword in the expected way *)
|
|
|
|
(idl, instrs, Sil.exp_zero, type_of_expr)
|
|
|
|
(instrs, Sil.exp_zero, type_of_expr)
|
|
|
|
else
|
|
|
|
else
|
|
|
|
let sil_expr = Sil.Lfield (sil_expr, field_name, sil_type) in
|
|
|
|
let sil_expr = Sil.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.Letderef (tmp_id, sil_expr, sil_type, loc) in
|
|
|
|
let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in
|
|
|
|
(idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id, type_of_expr)
|
|
|
|
(instrs @ [lderef_instr], Sil.Var tmp_id, type_of_expr)
|
|
|
|
|
|
|
|
|
|
|
|
let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_code method_kind =
|
|
|
|
let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_code method_kind =
|
|
|
|
(* This function tries to recursively search for the classname of the class *)
|
|
|
|
(* This function tries to recursively search for the classname of the class *)
|
|
|
|
@ -563,10 +561,10 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
|
|
|
|
{ Sil.cf_default with Sil.cf_virtual = cf_virtual; Sil.cf_interface = cf_interface; } in
|
|
|
|
{ Sil.cf_default with Sil.cf_virtual = cf_virtual; Sil.cf_interface = cf_interface; } in
|
|
|
|
let init =
|
|
|
|
let init =
|
|
|
|
match sil_obj_opt with
|
|
|
|
match sil_obj_opt with
|
|
|
|
| None -> ([], [], [])
|
|
|
|
| None -> [], []
|
|
|
|
| Some (sil_obj_expr, sil_obj_type) ->
|
|
|
|
| Some (sil_obj_expr, sil_obj_type) ->
|
|
|
|
(* for non-constructors, add an instruction that dereferences the receiver *)
|
|
|
|
(* for non-constructors, add an instruction that dereferences the receiver *)
|
|
|
|
let ids, instrs =
|
|
|
|
let instrs =
|
|
|
|
let is_non_constructor_call =
|
|
|
|
let is_non_constructor_call =
|
|
|
|
match invoke_code with
|
|
|
|
match invoke_code with
|
|
|
|
| I_Special -> false
|
|
|
|
| I_Special -> false
|
|
|
|
@ -577,15 +575,14 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
|
|
|
|
match sil_obj_type with
|
|
|
|
match sil_obj_type with
|
|
|
|
| Sil.Tptr (typ, _) -> typ
|
|
|
|
| Sil.Tptr (typ, _) -> typ
|
|
|
|
| _ -> sil_obj_type in
|
|
|
|
| _ -> sil_obj_type in
|
|
|
|
let fresh_id, deref = create_sil_deref sil_obj_expr obj_typ_no_ptr loc in
|
|
|
|
[create_sil_deref sil_obj_expr obj_typ_no_ptr loc]
|
|
|
|
[fresh_id], [deref]
|
|
|
|
| _ -> [] in
|
|
|
|
| _ -> [], [] in
|
|
|
|
(instrs, [(sil_obj_expr, sil_obj_type)]) in
|
|
|
|
(ids, instrs, [(sil_obj_expr, sil_obj_type)]) in
|
|
|
|
let (instrs, call_args) =
|
|
|
|
let (idl, instrs, call_args) =
|
|
|
|
|
|
|
|
IList.fold_left
|
|
|
|
IList.fold_left
|
|
|
|
(fun (idl_accu, instrs_accu, args_accu) expr ->
|
|
|
|
(fun (instrs_accu, args_accu) expr ->
|
|
|
|
let (idl, instrs, sil_expr, sil_expr_type) = expression context pc expr in
|
|
|
|
let (instrs, sil_expr, sil_expr_type) = expression context pc expr in
|
|
|
|
(idl_accu @ idl, instrs_accu @ instrs, args_accu @ [(sil_expr, sil_expr_type)]))
|
|
|
|
(instrs_accu @ instrs, args_accu @ [(sil_expr, sil_expr_type)]))
|
|
|
|
init
|
|
|
|
init
|
|
|
|
expr_list in
|
|
|
|
expr_list in
|
|
|
|
let callee_procname =
|
|
|
|
let callee_procname =
|
|
|
|
@ -594,7 +591,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
|
|
|
|
Builtin.is_registered proc
|
|
|
|
Builtin.is_registered proc
|
|
|
|
then proc
|
|
|
|
then proc
|
|
|
|
else Procname.Java (JTransType.get_method_procname cn' ms method_kind) in
|
|
|
|
else Procname.Java (JTransType.get_method_procname cn' ms method_kind) in
|
|
|
|
let call_idl, call_instrs =
|
|
|
|
let call_instrs =
|
|
|
|
let callee_fun = Sil.Const (Sil.Cfun callee_procname) in
|
|
|
|
let callee_fun = Sil.Const (Sil.Cfun callee_procname) in
|
|
|
|
let return_type =
|
|
|
|
let return_type =
|
|
|
|
match JBasics.ms_rtype ms with
|
|
|
|
match JBasics.ms_rtype ms with
|
|
|
|
@ -604,14 +601,14 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let call_instr = Sil.Call ([ret_id], callee_fun, call_args, loc, call_flags) in
|
|
|
|
let call_instr = Sil.Call ([ret_id], callee_fun, call_args, loc, call_flags) in
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar sil_var, return_type, Sil.Var ret_id, loc) in
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar sil_var, return_type, Sil.Var ret_id, loc) in
|
|
|
|
(idl @ [ret_id], instrs @ [call_instr; set_instr]) in
|
|
|
|
(instrs @ [call_instr; set_instr]) in
|
|
|
|
match var_opt with
|
|
|
|
match var_opt with
|
|
|
|
| None ->
|
|
|
|
| None ->
|
|
|
|
let call_instr = Sil.Call ([], callee_fun, call_args, loc, call_flags) in
|
|
|
|
let call_instr = Sil.Call ([], callee_fun, call_args, loc, call_flags) in
|
|
|
|
(idl, instrs @ [call_instr])
|
|
|
|
instrs @ [call_instr]
|
|
|
|
| Some var ->
|
|
|
|
| Some var ->
|
|
|
|
let sil_var = JContext.set_pvar context var return_type in
|
|
|
|
let sil_var = JContext.set_pvar context var return_type in
|
|
|
|
(call_ret_instrs sil_var) in
|
|
|
|
call_ret_instrs sil_var in
|
|
|
|
let instrs =
|
|
|
|
let instrs =
|
|
|
|
match call_args with
|
|
|
|
match call_args with
|
|
|
|
(* modeling a class bypasses the treatment of Closeable *)
|
|
|
|
(* modeling a class bypasses the treatment of Closeable *)
|
|
|
|
@ -638,20 +635,20 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
|
|
|
|
|
|
|
|
|
|
|
|
| _ -> call_instrs in
|
|
|
|
| _ -> call_instrs in
|
|
|
|
|
|
|
|
|
|
|
|
(callee_procname, call_idl, instrs)
|
|
|
|
(callee_procname, instrs)
|
|
|
|
|
|
|
|
|
|
|
|
let get_array_size context pc expr_list content_type =
|
|
|
|
let get_array_size context pc expr_list content_type =
|
|
|
|
let get_expr_instr expr other_instrs =
|
|
|
|
let get_expr_instr expr other_instrs =
|
|
|
|
let (idl, instrs, sil_size_expr, _) = expression context pc expr in
|
|
|
|
let (instrs, sil_size_expr, _) = expression context pc expr in
|
|
|
|
match other_instrs with
|
|
|
|
match other_instrs with
|
|
|
|
| (other_idl, other_instrs, other_exprs) ->
|
|
|
|
| (other_instrs, other_exprs) ->
|
|
|
|
(idl@other_idl, instrs@other_instrs, sil_size_expr:: other_exprs) in
|
|
|
|
(instrs@other_instrs, sil_size_expr:: other_exprs) in
|
|
|
|
let (idl, instrs, sil_size_exprs) = (IList.fold_right get_expr_instr expr_list ([],[],[])) in
|
|
|
|
let (instrs, sil_size_exprs) = (IList.fold_right get_expr_instr expr_list ([],[])) in
|
|
|
|
let get_array_type sil_size_expr content_type =
|
|
|
|
let get_array_type sil_size_expr content_type =
|
|
|
|
Sil.Tarray (content_type, sil_size_expr) in
|
|
|
|
Sil.Tarray (content_type, sil_size_expr) in
|
|
|
|
let array_type = (IList.fold_right get_array_type sil_size_exprs content_type) in
|
|
|
|
let array_type = (IList.fold_right get_array_type sil_size_exprs content_type) in
|
|
|
|
let array_size = Sil.Sizeof (array_type, Sil.Subtype.exact) in
|
|
|
|
let array_size = Sil.Sizeof (array_type, Sil.Subtype.exact) in
|
|
|
|
(idl, instrs, array_size)
|
|
|
|
(instrs, array_size)
|
|
|
|
|
|
|
|
|
|
|
|
module Int =
|
|
|
|
module Int =
|
|
|
|
struct
|
|
|
|
struct
|
|
|
|
@ -787,9 +784,13 @@ let rec instruction context pc instr : translation =
|
|
|
|
let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in
|
|
|
|
let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in
|
|
|
|
let loc = get_location (JContext.get_impl context) pc meth_kind cn in
|
|
|
|
let loc = get_location (JContext.get_impl context) pc meth_kind cn in
|
|
|
|
let match_never_null = JContext.get_never_null_matcher context in
|
|
|
|
let match_never_null = JContext.get_never_null_matcher context in
|
|
|
|
let create_node node_kind temps sil_instrs =
|
|
|
|
let create_node node_kind sil_instrs =
|
|
|
|
Cfg.Node.create
|
|
|
|
Cfg.Node.create
|
|
|
|
cfg (get_location (JContext.get_impl context) pc meth_kind cn) node_kind sil_instrs (JContext.get_procdesc context) temps in
|
|
|
|
cfg
|
|
|
|
|
|
|
|
(get_location (JContext.get_impl context) pc meth_kind cn)
|
|
|
|
|
|
|
|
node_kind
|
|
|
|
|
|
|
|
sil_instrs
|
|
|
|
|
|
|
|
(JContext.get_procdesc context) in
|
|
|
|
let return_not_null () =
|
|
|
|
let return_not_null () =
|
|
|
|
match_never_null loc.Location.file proc_name
|
|
|
|
match_never_null loc.Location.file proc_name
|
|
|
|
||
|
|
|
|
||
|
|
|
|
@ -797,73 +798,72 @@ let rec instruction context pc instr : translation =
|
|
|
|
(fun pnj -> Procname.equal (Procname.Java pnj) proc_name)
|
|
|
|
(fun pnj -> Procname.equal (Procname.Java pnj) proc_name)
|
|
|
|
JTransType.never_returning_null in
|
|
|
|
JTransType.never_returning_null in
|
|
|
|
let trans_monitor_enter_exit context expr pc loc builtin node_desc =
|
|
|
|
let trans_monitor_enter_exit context expr pc loc builtin node_desc =
|
|
|
|
let ids, instrs, sil_expr, sil_type = expression context pc expr in
|
|
|
|
let instrs, sil_expr, sil_type = expression context pc expr in
|
|
|
|
let builtin_const = Sil.Const (Sil.Cfun builtin) in
|
|
|
|
let builtin_const = Sil.Const (Sil.Cfun builtin) in
|
|
|
|
let instr = Sil.Call ([], builtin_const, [(sil_expr, sil_type)], loc, Sil.cf_default) in
|
|
|
|
let instr = Sil.Call ([], builtin_const, [(sil_expr, sil_type)], loc, Sil.cf_default) in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node node_desc in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node node_desc in
|
|
|
|
Instr (create_node node_kind ids (instrs @ [instr])) in
|
|
|
|
Instr (create_node node_kind (instrs @ [instr])) in
|
|
|
|
try
|
|
|
|
try
|
|
|
|
match instr with
|
|
|
|
match instr with
|
|
|
|
| JBir.AffectVar (var, expr) ->
|
|
|
|
| JBir.AffectVar (var, expr) ->
|
|
|
|
let (idl, stml, sil_expr, sil_type) = expression context pc expr in
|
|
|
|
let (stml, sil_expr, sil_type) = expression context pc expr in
|
|
|
|
let pvar = (JContext.set_pvar context var sil_type) in
|
|
|
|
let pvar = (JContext.set_pvar context var sil_type) in
|
|
|
|
let sil_instr = Sil.Set (Sil.Lvar pvar, sil_type, sil_expr, loc) in
|
|
|
|
let sil_instr = Sil.Set (Sil.Lvar pvar, sil_type, sil_expr, loc) in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node = create_node node_kind idl (stml @ [sil_instr]) in
|
|
|
|
let node = create_node node_kind (stml @ [sil_instr]) in
|
|
|
|
Instr node
|
|
|
|
Instr node
|
|
|
|
| JBir.Return expr_option ->
|
|
|
|
| JBir.Return expr_option ->
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node =
|
|
|
|
let node =
|
|
|
|
match expr_option with
|
|
|
|
match expr_option with
|
|
|
|
| None ->
|
|
|
|
| None ->
|
|
|
|
create_node node_kind [] []
|
|
|
|
create_node node_kind []
|
|
|
|
| Some expr ->
|
|
|
|
| Some expr ->
|
|
|
|
let (idl, stml, sil_expr, _) = expression context pc expr in
|
|
|
|
let (stml, sil_expr, _) = expression context pc expr in
|
|
|
|
let sil_instrs =
|
|
|
|
let sil_instrs =
|
|
|
|
let return_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_expr, loc) in
|
|
|
|
let return_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_expr, loc) in
|
|
|
|
if return_not_null () then
|
|
|
|
if return_not_null () then
|
|
|
|
[assume_not_null loc sil_expr; return_instr]
|
|
|
|
[assume_not_null loc sil_expr; return_instr]
|
|
|
|
else
|
|
|
|
else
|
|
|
|
[return_instr] in
|
|
|
|
[return_instr] in
|
|
|
|
create_node node_kind idl (stml @ sil_instrs) in
|
|
|
|
create_node node_kind (stml @ sil_instrs) in
|
|
|
|
JContext.add_goto_jump context pc JContext.Exit;
|
|
|
|
JContext.add_goto_jump context pc JContext.Exit;
|
|
|
|
Instr node
|
|
|
|
Instr node
|
|
|
|
| JBir.AffectArray (array_ex, index_ex, value_ex) ->
|
|
|
|
| JBir.AffectArray (array_ex, index_ex, value_ex) ->
|
|
|
|
let (idl_array, instrs_array, sil_expr_array, arr_type) = expression context pc array_ex
|
|
|
|
let (instrs_array, sil_expr_array, arr_type) = expression context pc array_ex
|
|
|
|
and (idl_index, instrs_index, sil_expr_index, _) = expression context pc index_ex
|
|
|
|
and (instrs_index, sil_expr_index, _) = expression context pc index_ex
|
|
|
|
and (idl_value, instrs_value, sil_expr_value, _) = expression context pc value_ex in
|
|
|
|
and (instrs_value, sil_expr_value, _) = expression context pc value_ex in
|
|
|
|
let arr_type_np = JTransType.extract_cn_type_np arr_type in
|
|
|
|
let arr_type_np = JTransType.extract_cn_type_np arr_type in
|
|
|
|
let sil_instr = Sil.Set (Sil.Lindex (sil_expr_array, sil_expr_index), arr_type_np, sil_expr_value, loc) in
|
|
|
|
let sil_instr = Sil.Set (Sil.Lindex (sil_expr_array, sil_expr_index), arr_type_np, sil_expr_value, loc) in
|
|
|
|
let final_idl = idl_array @ idl_index @ idl_value
|
|
|
|
let final_instrs = instrs_array @ instrs_index @ instrs_value @ [sil_instr] in
|
|
|
|
and final_instrs = instrs_array @ instrs_index @ instrs_value @ [sil_instr] in
|
|
|
|
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node = create_node node_kind final_idl final_instrs in
|
|
|
|
let node = create_node node_kind final_instrs in
|
|
|
|
Instr node
|
|
|
|
Instr node
|
|
|
|
| JBir.AffectField (e_lhs, cn, fs, e_rhs) ->
|
|
|
|
| JBir.AffectField (e_lhs, cn, fs, e_rhs) ->
|
|
|
|
let (idl1, stml1, sil_expr_lhs, _) = expression context pc e_lhs in
|
|
|
|
let (stml1, sil_expr_lhs, _) = expression context pc e_lhs in
|
|
|
|
let (idl2, stml2, sil_expr_rhs, _) = expression context pc e_rhs in
|
|
|
|
let (stml2, sil_expr_rhs, _) = expression context pc e_rhs in
|
|
|
|
let field_name = get_field_name program false tenv cn fs 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_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 type_of_the_root_of_e_lhs = type_of_the_surrounding_class in
|
|
|
|
let expr_off = Sil.Lfield(sil_expr_lhs, field_name, type_of_the_surrounding_class) in
|
|
|
|
let expr_off = Sil.Lfield(sil_expr_lhs, field_name, type_of_the_surrounding_class) in
|
|
|
|
let sil_instr = Sil.Set (expr_off, type_of_the_root_of_e_lhs, sil_expr_rhs, loc) in
|
|
|
|
let sil_instr = Sil.Set (expr_off, type_of_the_root_of_e_lhs, sil_expr_rhs, loc) in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node = create_node node_kind (idl1 @ idl2) (stml1 @ stml2 @ [sil_instr]) in
|
|
|
|
let node = create_node node_kind (stml1 @ stml2 @ [sil_instr]) in
|
|
|
|
Instr node
|
|
|
|
Instr node
|
|
|
|
| JBir.AffectStaticField (cn, fs, e_rhs) ->
|
|
|
|
| JBir.AffectStaticField (cn, fs, e_rhs) ->
|
|
|
|
let class_exp =
|
|
|
|
let class_exp =
|
|
|
|
let classname = Mangled.from_string (JBasics.cn_name cn) in
|
|
|
|
let classname = Mangled.from_string (JBasics.cn_name cn) in
|
|
|
|
let var_name = Pvar.mk_global classname in
|
|
|
|
let var_name = Pvar.mk_global classname in
|
|
|
|
Sil.Lvar var_name in
|
|
|
|
Sil.Lvar var_name in
|
|
|
|
let (idl1, stml1, sil_expr_lhs) = [], [], class_exp in
|
|
|
|
let (stml1, sil_expr_lhs) = [], class_exp in
|
|
|
|
let (idl2, stml2, sil_expr_rhs, _) = expression context pc e_rhs in
|
|
|
|
let (stml2, sil_expr_rhs, _) = expression context pc e_rhs in
|
|
|
|
let field_name = get_field_name program true tenv cn fs 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_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 type_of_the_root_of_e_lhs = type_of_the_surrounding_class in
|
|
|
|
let expr_off = Sil.Lfield(sil_expr_lhs, field_name, type_of_the_surrounding_class) in
|
|
|
|
let expr_off = Sil.Lfield(sil_expr_lhs, field_name, type_of_the_surrounding_class) in
|
|
|
|
let sil_instr = Sil.Set (expr_off, type_of_the_root_of_e_lhs, sil_expr_rhs, loc) in
|
|
|
|
let sil_instr = Sil.Set (expr_off, type_of_the_root_of_e_lhs, sil_expr_rhs, loc) in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node = create_node node_kind (idl1 @ idl2) (stml1 @ stml2 @ [sil_instr]) in
|
|
|
|
let node = create_node node_kind (stml1 @ stml2 @ [sil_instr]) in
|
|
|
|
Instr node
|
|
|
|
Instr node
|
|
|
|
| JBir.Goto goto_pc ->
|
|
|
|
| JBir.Goto goto_pc ->
|
|
|
|
JContext.reset_pvar_type context;
|
|
|
|
JContext.reset_pvar_type context;
|
|
|
|
@ -871,8 +871,8 @@ let rec instruction context pc instr : translation =
|
|
|
|
Skip
|
|
|
|
Skip
|
|
|
|
| JBir.Ifd ((op, e1, e2), if_pc) -> (* Note: JBir provides the condition for the false branch, under which to jump *)
|
|
|
|
| JBir.Ifd ((op, e1, e2), if_pc) -> (* Note: JBir provides the condition for the false branch, under which to jump *)
|
|
|
|
JContext.reset_pvar_type context;
|
|
|
|
JContext.reset_pvar_type context;
|
|
|
|
let (idl1, instrs1, sil_ex1, _) = expression context pc e1
|
|
|
|
let (instrs1, sil_ex1, _) = expression context pc e1
|
|
|
|
and (idl2, instrs2, sil_ex2, _) = expression context pc e2 in
|
|
|
|
and (instrs2, sil_ex2, _) = expression context pc e2 in
|
|
|
|
let sil_op = get_test_operator op in
|
|
|
|
let sil_op = get_test_operator op in
|
|
|
|
let sil_test_false = Sil.BinOp (sil_op, sil_ex1, sil_ex2) in
|
|
|
|
let sil_test_false = Sil.BinOp (sil_op, sil_ex1, sil_ex2) in
|
|
|
|
let sil_test_true = Sil.UnOp(Sil.LNot, sil_test_false, None) in
|
|
|
|
let sil_test_true = Sil.UnOp(Sil.LNot, sil_test_false, None) in
|
|
|
|
@ -880,20 +880,21 @@ let rec instruction context pc instr : translation =
|
|
|
|
let sil_instrs_false = Sil.Prune (sil_test_false, loc, false, Sil.Ik_if) in
|
|
|
|
let sil_instrs_false = Sil.Prune (sil_test_false, loc, false, Sil.Ik_if) in
|
|
|
|
let node_kind_true = Cfg.Node.Prune_node (true, Sil.Ik_if, "method_body") in
|
|
|
|
let node_kind_true = Cfg.Node.Prune_node (true, Sil.Ik_if, "method_body") in
|
|
|
|
let node_kind_false = Cfg.Node.Prune_node (false, Sil.Ik_if, "method_body") in
|
|
|
|
let node_kind_false = Cfg.Node.Prune_node (false, Sil.Ik_if, "method_body") in
|
|
|
|
let prune_node_true = create_node node_kind_true (idl1 @ idl2) (instrs1 @ instrs2 @ [sil_instrs_true])
|
|
|
|
let prune_node_true = create_node node_kind_true (instrs1 @ instrs2 @ [sil_instrs_true])
|
|
|
|
and prune_node_false = create_node node_kind_false (idl1 @ idl2) (instrs1 @ instrs2 @ [sil_instrs_false]) in
|
|
|
|
and prune_node_false =
|
|
|
|
|
|
|
|
create_node node_kind_false (instrs1 @ instrs2 @ [sil_instrs_false]) in
|
|
|
|
JContext.add_if_jump context prune_node_false if_pc;
|
|
|
|
JContext.add_if_jump context prune_node_false if_pc;
|
|
|
|
if detect_loop pc (JContext.get_impl context) then
|
|
|
|
if detect_loop pc (JContext.get_impl context) then
|
|
|
|
let join_node_kind = Cfg.Node.Join_node in
|
|
|
|
let join_node_kind = Cfg.Node.Join_node in
|
|
|
|
let join_node = create_node join_node_kind [] [] in
|
|
|
|
let join_node = create_node join_node_kind [] in
|
|
|
|
Loop (join_node, prune_node_true, prune_node_false)
|
|
|
|
Loop (join_node, prune_node_true, prune_node_false)
|
|
|
|
else
|
|
|
|
else
|
|
|
|
Prune (prune_node_true, prune_node_false)
|
|
|
|
Prune (prune_node_true, prune_node_false)
|
|
|
|
| JBir.Throw expr ->
|
|
|
|
| JBir.Throw expr ->
|
|
|
|
let (ids, instrs, sil_expr, _) = expression context pc expr in
|
|
|
|
let (instrs, sil_expr, _) = expression context pc expr in
|
|
|
|
let sil_exn = Sil.Const (Sil.Cexn sil_expr) in
|
|
|
|
let sil_exn = Sil.Const (Sil.Cexn sil_expr) in
|
|
|
|
let sil_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
|
|
|
|
let sil_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
|
|
|
|
let node = create_node Cfg.Node.throw_kind ids (instrs @ [sil_instr]) in
|
|
|
|
let node = create_node Cfg.Node.throw_kind (instrs @ [sil_instr]) in
|
|
|
|
JContext.add_goto_jump context pc JContext.Exit;
|
|
|
|
JContext.add_goto_jump context pc JContext.Exit;
|
|
|
|
Instr node
|
|
|
|
Instr node
|
|
|
|
| JBir.New (var, cn, constr_type_list, constr_arg_list) ->
|
|
|
|
| JBir.New (var, cn, constr_type_list, constr_arg_list) ->
|
|
|
|
@ -905,16 +906,15 @@ let rec instruction context pc instr : translation =
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
|
|
|
|
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
|
|
|
|
let constr_ms = JBasics.make_ms JConfig.constructor_name constr_type_list None in
|
|
|
|
let constr_ms = JBasics.make_ms JConfig.constructor_name constr_type_list None in
|
|
|
|
let constr_procname, call_ids, call_instrs =
|
|
|
|
let constr_procname, call_instrs =
|
|
|
|
let ret_opt = Some (Sil.Var ret_id, class_type) in
|
|
|
|
let ret_opt = Some (Sil.Var ret_id, class_type) in
|
|
|
|
method_invocation
|
|
|
|
method_invocation
|
|
|
|
context loc pc None cn constr_ms ret_opt constr_arg_list I_Special Procname.Non_Static in
|
|
|
|
context loc pc None cn constr_ms ret_opt constr_arg_list I_Special Procname.Non_Static in
|
|
|
|
let pvar = JContext.set_pvar context var class_type in
|
|
|
|
let pvar = JContext.set_pvar context var class_type in
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar pvar, class_type, Sil.Var ret_id, loc) in
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar pvar, class_type, Sil.Var ret_id, loc) in
|
|
|
|
let ids = ret_id :: call_ids in
|
|
|
|
|
|
|
|
let instrs = (new_instr :: call_instrs) @ [set_instr] in
|
|
|
|
let instrs = (new_instr :: call_instrs) @ [set_instr] in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string constr_procname)) in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string constr_procname)) in
|
|
|
|
let node = create_node node_kind ids instrs in
|
|
|
|
let node = create_node node_kind instrs in
|
|
|
|
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
|
|
|
|
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
|
|
|
|
Cg.add_edge cg caller_procname constr_procname;
|
|
|
|
Cg.add_edge cg caller_procname constr_procname;
|
|
|
|
Instr node
|
|
|
|
Instr node
|
|
|
|
@ -923,40 +923,40 @@ let rec instruction context pc instr : translation =
|
|
|
|
let content_type = JTransType.value_type program tenv vt in
|
|
|
|
let content_type = JTransType.value_type program tenv vt in
|
|
|
|
let array_type = JTransType.create_array_type content_type (IList.length expr_list) in
|
|
|
|
let array_type = JTransType.create_array_type content_type (IList.length expr_list) in
|
|
|
|
let array_name = JContext.set_pvar context var array_type in
|
|
|
|
let array_name = JContext.set_pvar context var array_type in
|
|
|
|
let (idl, instrs, array_size) = get_array_size context pc expr_list content_type in
|
|
|
|
let (instrs, array_size) = get_array_size context pc expr_list content_type in
|
|
|
|
let call_args = [(array_size, array_type)] in
|
|
|
|
let call_args = [(array_size, array_type)] in
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let call_instr = Sil.Call([ret_id], builtin_new_array, call_args, loc, Sil.cf_default) in
|
|
|
|
let call_instr = Sil.Call([ret_id], builtin_new_array, call_args, loc, Sil.cf_default) in
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar array_name, array_type, Sil.Var ret_id, loc) in
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar array_name, array_type, Sil.Var ret_id, loc) in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
let node = create_node node_kind (idl @ [ret_id]) (instrs @ [call_instr; set_instr]) in
|
|
|
|
let node = create_node node_kind (instrs @ [call_instr; set_instr]) in
|
|
|
|
Instr node
|
|
|
|
Instr node
|
|
|
|
| JBir.InvokeStatic (var_opt, cn, ms, args) ->
|
|
|
|
| JBir.InvokeStatic (var_opt, cn, ms, args) ->
|
|
|
|
let sil_obj_opt, args, ids, instrs =
|
|
|
|
let sil_obj_opt, args, instrs =
|
|
|
|
match args with
|
|
|
|
match args with
|
|
|
|
| [arg] when is_clone ms ->
|
|
|
|
| [arg] when is_clone ms ->
|
|
|
|
(* hack to null check the receiver of clone when clone is an array. in the array.clone()
|
|
|
|
(* hack to null check the receiver of clone when clone is an array. in the array.clone()
|
|
|
|
case, clone is a virtual call that we translate as a static call *)
|
|
|
|
case, clone is a virtual call that we translate as a static call *)
|
|
|
|
let (ids, instrs, sil_arg_expr, arg_typ) = expression context pc arg in
|
|
|
|
let (instrs, sil_arg_expr, arg_typ) = expression context pc arg in
|
|
|
|
Some (sil_arg_expr, arg_typ), [], ids, instrs
|
|
|
|
Some (sil_arg_expr, arg_typ), [], instrs
|
|
|
|
| _ -> None, args, [], [] in
|
|
|
|
| _ -> None, args, [] in
|
|
|
|
let callee_procname, call_idl, call_instrs =
|
|
|
|
let callee_procname, call_instrs =
|
|
|
|
method_invocation context loc pc var_opt cn ms sil_obj_opt args I_Static Procname.Static in
|
|
|
|
method_invocation context loc pc var_opt cn ms sil_obj_opt args I_Static Procname.Static in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
|
|
|
|
let call_node = create_node node_kind (ids @ call_idl) (instrs @ call_instrs) in
|
|
|
|
let call_node = create_node node_kind (instrs @ call_instrs) in
|
|
|
|
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
|
|
|
|
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
|
|
|
|
Cg.add_edge cg caller_procname callee_procname;
|
|
|
|
Cg.add_edge cg caller_procname callee_procname;
|
|
|
|
Instr call_node
|
|
|
|
Instr call_node
|
|
|
|
| JBir.InvokeVirtual (var_opt, obj, call_kind, ms, args) ->
|
|
|
|
| JBir.InvokeVirtual (var_opt, obj, call_kind, ms, args) ->
|
|
|
|
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
|
|
|
|
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
|
|
|
|
let (ids, instrs, sil_obj_expr, sil_obj_type) = expression context pc obj in
|
|
|
|
let (instrs, sil_obj_expr, sil_obj_type) = expression context pc obj in
|
|
|
|
let create_call_node cn invoke_kind =
|
|
|
|
let create_call_node cn invoke_kind =
|
|
|
|
let callee_procname, call_ids, call_instrs =
|
|
|
|
let callee_procname, call_instrs =
|
|
|
|
let ret_opt = Some (sil_obj_expr, sil_obj_type) in
|
|
|
|
let ret_opt = Some (sil_obj_expr, sil_obj_type) in
|
|
|
|
method_invocation
|
|
|
|
method_invocation
|
|
|
|
context loc pc var_opt cn ms ret_opt args invoke_kind Procname.Non_Static in
|
|
|
|
context loc pc var_opt cn ms ret_opt args invoke_kind Procname.Non_Static in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
|
|
|
|
let call_node = create_node node_kind (ids @ call_ids) (instrs @ call_instrs) in
|
|
|
|
let call_node = create_node node_kind (instrs @ call_instrs) in
|
|
|
|
Cg.add_edge cg caller_procname callee_procname;
|
|
|
|
Cg.add_edge cg caller_procname callee_procname;
|
|
|
|
call_node in
|
|
|
|
call_node in
|
|
|
|
let trans_virtual_call original_cn invoke_kind =
|
|
|
|
let trans_virtual_call original_cn invoke_kind =
|
|
|
|
@ -982,11 +982,11 @@ let rec instruction context pc instr : translation =
|
|
|
|
trans_virtual_call cn I_Interface
|
|
|
|
trans_virtual_call cn I_Interface
|
|
|
|
end
|
|
|
|
end
|
|
|
|
| JBir.InvokeNonVirtual (var_opt, obj, cn, ms, args) ->
|
|
|
|
| JBir.InvokeNonVirtual (var_opt, obj, cn, ms, args) ->
|
|
|
|
let (ids, instrs, sil_obj_expr, sil_obj_type) = expression context pc obj in
|
|
|
|
let (instrs, sil_obj_expr, sil_obj_type) = expression context pc obj in
|
|
|
|
let callee_procname, call_ids, call_instrs =
|
|
|
|
let callee_procname, call_instrs =
|
|
|
|
method_invocation context loc pc var_opt cn ms (Some (sil_obj_expr, sil_obj_type)) args I_Special Procname.Non_Static in
|
|
|
|
method_invocation context loc pc var_opt cn ms (Some (sil_obj_expr, sil_obj_type)) args I_Special Procname.Non_Static in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
|
|
|
|
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
|
|
|
|
let call_node = create_node node_kind (ids @ call_ids) (instrs @ call_instrs) in
|
|
|
|
let call_node = create_node node_kind (instrs @ call_instrs) in
|
|
|
|
let procdesc = (JContext.get_procdesc context) in
|
|
|
|
let procdesc = (JContext.get_procdesc context) in
|
|
|
|
let caller_procname = (Cfg.Procdesc.get_proc_name procdesc) in
|
|
|
|
let caller_procname = (Cfg.Procdesc.get_proc_name procdesc) in
|
|
|
|
Cg.add_edge cg caller_procname callee_procname;
|
|
|
|
Cg.add_edge cg caller_procname callee_procname;
|
|
|
|
@ -994,19 +994,19 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
|
|
|
|
|
|
|
| JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks && is_this expr ->
|
|
|
|
| JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks && is_this expr ->
|
|
|
|
(* TODO #6509339: refactor the boilterplate code in the translattion of JVM checks *)
|
|
|
|
(* TODO #6509339: refactor the boilterplate code in the translattion of JVM checks *)
|
|
|
|
let (ids, instrs, sil_expr, _) = expression context pc expr in
|
|
|
|
let (instrs, sil_expr, _) = expression context pc expr in
|
|
|
|
let this_not_null_node =
|
|
|
|
let this_not_null_node =
|
|
|
|
create_node
|
|
|
|
create_node
|
|
|
|
(Cfg.Node.Stmt_node "this not null") ids (instrs @ [assume_not_null loc sil_expr]) in
|
|
|
|
(Cfg.Node.Stmt_node "this not null") (instrs @ [assume_not_null loc sil_expr]) in
|
|
|
|
Instr this_not_null_node
|
|
|
|
Instr this_not_null_node
|
|
|
|
|
|
|
|
|
|
|
|
| JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks ->
|
|
|
|
| JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks ->
|
|
|
|
let (ids, instrs, sil_expr, _) = expression context pc expr in
|
|
|
|
let (instrs, sil_expr, _) = expression context pc expr in
|
|
|
|
let not_null_node =
|
|
|
|
let not_null_node =
|
|
|
|
let sil_not_null = Sil.BinOp (Sil.Ne, sil_expr, Sil.exp_null) in
|
|
|
|
let sil_not_null = Sil.BinOp (Sil.Ne, sil_expr, Sil.exp_null) in
|
|
|
|
let sil_prune_not_null = Sil.Prune (sil_not_null, loc, true, Sil.Ik_if)
|
|
|
|
let sil_prune_not_null = Sil.Prune (sil_not_null, loc, true, Sil.Ik_if)
|
|
|
|
and not_null_kind = Cfg.Node.Prune_node (true, Sil.Ik_if, "Not null") in
|
|
|
|
and not_null_kind = Cfg.Node.Prune_node (true, Sil.Ik_if, "Not null") in
|
|
|
|
create_node not_null_kind ids (instrs @ [sil_prune_not_null]) in
|
|
|
|
create_node not_null_kind (instrs @ [sil_prune_not_null]) in
|
|
|
|
let throw_npe_node =
|
|
|
|
let throw_npe_node =
|
|
|
|
let sil_is_null = Sil.BinOp (Sil.Eq, sil_expr, Sil.exp_null) in
|
|
|
|
let sil_is_null = Sil.BinOp (Sil.Eq, sil_expr, Sil.exp_null) in
|
|
|
|
let sil_prune_null = Sil.Prune (sil_is_null, loc, true, Sil.Ik_if)
|
|
|
|
let sil_prune_null = Sil.Prune (sil_is_null, loc, true, Sil.Ik_if)
|
|
|
|
@ -1019,27 +1019,26 @@ let rec instruction context pc instr : translation =
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
|
|
|
|
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
|
|
|
|
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
|
|
|
|
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
|
|
|
|
let _, call_ids, call_instrs =
|
|
|
|
let _, call_instrs =
|
|
|
|
let ret_opt = Some (Sil.Var ret_id, class_type) in
|
|
|
|
let ret_opt = Some (Sil.Var ret_id, class_type) in
|
|
|
|
method_invocation context loc pc None npe_cn constr_ms ret_opt [] I_Special Procname.Static in
|
|
|
|
method_invocation context loc pc None npe_cn constr_ms ret_opt [] I_Special Procname.Static in
|
|
|
|
let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in
|
|
|
|
let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
|
|
|
|
let npe_instrs = instrs @ [sil_prune_null] @ (new_instr :: call_instrs) @ [set_instr] in
|
|
|
|
let npe_instrs = instrs @ [sil_prune_null] @ (new_instr :: call_instrs) @ [set_instr] in
|
|
|
|
create_node npe_kind (ids @ call_ids) npe_instrs in
|
|
|
|
create_node npe_kind npe_instrs in
|
|
|
|
Prune (not_null_node, throw_npe_node)
|
|
|
|
Prune (not_null_node, throw_npe_node)
|
|
|
|
|
|
|
|
|
|
|
|
| JBir.Check (JBir.CheckArrayBound (array_expr, index_expr)) when !JConfig.translate_checks ->
|
|
|
|
| JBir.Check (JBir.CheckArrayBound (array_expr, index_expr)) when !JConfig.translate_checks ->
|
|
|
|
|
|
|
|
|
|
|
|
let ids, instrs, _, sil_length_expr, sil_index_expr =
|
|
|
|
let instrs, _, sil_length_expr, sil_index_expr =
|
|
|
|
let array_ids, array_instrs, sil_array_expr, _ =
|
|
|
|
let array_instrs, sil_array_expr, _ =
|
|
|
|
expression context pc array_expr
|
|
|
|
expression context pc array_expr
|
|
|
|
and length_ids, length_instrs, sil_length_expr, _ =
|
|
|
|
and length_instrs, sil_length_expr, _ =
|
|
|
|
expression context pc (JBir.Unop (JBir.ArrayLength, array_expr))
|
|
|
|
expression context pc (JBir.Unop (JBir.ArrayLength, array_expr))
|
|
|
|
and index_ids, index_instrs, sil_index_expr, _ =
|
|
|
|
and index_instrs, sil_index_expr, _ =
|
|
|
|
expression context pc index_expr in
|
|
|
|
expression context pc index_expr in
|
|
|
|
let ids = array_ids @ index_ids @ length_ids
|
|
|
|
let instrs = array_instrs @ index_instrs @ length_instrs in
|
|
|
|
and instrs = array_instrs @ index_instrs @ length_instrs in
|
|
|
|
(instrs, sil_array_expr, sil_length_expr, sil_index_expr) in
|
|
|
|
(ids, instrs, sil_array_expr, sil_length_expr, sil_index_expr) in
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let in_bound_node =
|
|
|
|
let in_bound_node =
|
|
|
|
let in_bound_node_kind =
|
|
|
|
let in_bound_node_kind =
|
|
|
|
@ -1052,7 +1051,7 @@ let rec instruction context pc instr : translation =
|
|
|
|
Sil.BinOp (Sil.Lt, sil_index_expr, sil_length_expr) in
|
|
|
|
Sil.BinOp (Sil.Lt, sil_index_expr, sil_length_expr) in
|
|
|
|
Sil.BinOp (Sil.LAnd, sil_positive_index, sil_less_than_length) in
|
|
|
|
Sil.BinOp (Sil.LAnd, sil_positive_index, sil_less_than_length) in
|
|
|
|
Sil.Prune (sil_in_bound, loc, true, Sil.Ik_if) in
|
|
|
|
Sil.Prune (sil_in_bound, loc, true, Sil.Ik_if) in
|
|
|
|
create_node in_bound_node_kind ids (instrs @ [sil_assume_in_bound])
|
|
|
|
create_node in_bound_node_kind (instrs @ [sil_assume_in_bound])
|
|
|
|
|
|
|
|
|
|
|
|
and throw_out_of_bound_node =
|
|
|
|
and throw_out_of_bound_node =
|
|
|
|
let out_of_bound_node_kind =
|
|
|
|
let out_of_bound_node_kind =
|
|
|
|
@ -1073,7 +1072,7 @@ let rec instruction context pc instr : translation =
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
|
|
|
|
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
|
|
|
|
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
|
|
|
|
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
|
|
|
|
let _, call_ids, call_instrs =
|
|
|
|
let _, call_instrs =
|
|
|
|
method_invocation
|
|
|
|
method_invocation
|
|
|
|
context loc pc None out_of_bound_cn constr_ms
|
|
|
|
context loc pc None out_of_bound_cn constr_ms
|
|
|
|
(Some (Sil.Var ret_id, class_type)) [] I_Special Procname.Static in
|
|
|
|
(Some (Sil.Var ret_id, class_type)) [] I_Special Procname.Static in
|
|
|
|
@ -1081,13 +1080,13 @@ let rec instruction context pc instr : translation =
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
|
|
|
|
let out_of_bound_instrs =
|
|
|
|
let out_of_bound_instrs =
|
|
|
|
instrs @ [sil_assume_out_of_bound] @ (new_instr :: call_instrs) @ [set_instr] in
|
|
|
|
instrs @ [sil_assume_out_of_bound] @ (new_instr :: call_instrs) @ [set_instr] in
|
|
|
|
create_node out_of_bound_node_kind (ids @ call_ids) out_of_bound_instrs in
|
|
|
|
create_node out_of_bound_node_kind out_of_bound_instrs in
|
|
|
|
|
|
|
|
|
|
|
|
Prune (in_bound_node, throw_out_of_bound_node)
|
|
|
|
Prune (in_bound_node, throw_out_of_bound_node)
|
|
|
|
|
|
|
|
|
|
|
|
| JBir.Check (JBir.CheckCast (expr, object_type)) when !JConfig.translate_checks ->
|
|
|
|
| JBir.Check (JBir.CheckCast (expr, object_type)) when !JConfig.translate_checks ->
|
|
|
|
let sil_type = JTransType.expr_type context expr
|
|
|
|
let sil_type = JTransType.expr_type context expr
|
|
|
|
and ids, instrs, sil_expr, _ = expression context pc expr
|
|
|
|
and instrs, sil_expr, _ = expression context pc expr
|
|
|
|
and ret_id = Ident.create_fresh Ident.knormal
|
|
|
|
and ret_id = Ident.create_fresh Ident.knormal
|
|
|
|
and sizeof_expr =
|
|
|
|
and sizeof_expr =
|
|
|
|
JTransType.sizeof_of_object_type program tenv object_type Sil.Subtype.subtypes_instof in
|
|
|
|
JTransType.sizeof_of_object_type program tenv object_type Sil.Subtype.subtypes_instof in
|
|
|
|
@ -1099,7 +1098,7 @@ let rec instruction context pc instr : translation =
|
|
|
|
let check_is_false = Sil.BinOp (Sil.Ne, res_ex, Sil.exp_zero) in
|
|
|
|
let check_is_false = Sil.BinOp (Sil.Ne, res_ex, Sil.exp_zero) in
|
|
|
|
let asssume_instance_of = Sil.Prune (check_is_false, loc, true, Sil.Ik_if)
|
|
|
|
let asssume_instance_of = Sil.Prune (check_is_false, loc, true, Sil.Ik_if)
|
|
|
|
and instance_of_kind = Cfg.Node.Prune_node (true, Sil.Ik_if, "Is instance") in
|
|
|
|
and instance_of_kind = Cfg.Node.Prune_node (true, Sil.Ik_if, "Is instance") in
|
|
|
|
create_node instance_of_kind ids (instrs @ [call; asssume_instance_of])
|
|
|
|
create_node instance_of_kind (instrs @ [call; asssume_instance_of])
|
|
|
|
and throw_cast_exception_node =
|
|
|
|
and throw_cast_exception_node =
|
|
|
|
let check_is_true = Sil.BinOp (Sil.Ne, res_ex, Sil.exp_one) in
|
|
|
|
let check_is_true = Sil.BinOp (Sil.Ne, res_ex, Sil.exp_one) in
|
|
|
|
let asssume_not_instance_of = Sil.Prune (check_is_true, loc, true, Sil.Ik_if)
|
|
|
|
let asssume_not_instance_of = Sil.Prune (check_is_true, loc, true, Sil.Ik_if)
|
|
|
|
@ -1112,14 +1111,14 @@ let rec instruction context pc instr : translation =
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
|
|
|
|
let new_instr = Sil.Call([ret_id], builtin_new, args, loc, Sil.cf_default) in
|
|
|
|
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
|
|
|
|
let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in
|
|
|
|
let _, call_ids, call_instrs =
|
|
|
|
let _, call_instrs =
|
|
|
|
method_invocation context loc pc None cce_cn constr_ms
|
|
|
|
method_invocation context loc pc None cce_cn constr_ms
|
|
|
|
(Some (Sil.Var ret_id, class_type)) [] I_Special Procname.Static in
|
|
|
|
(Some (Sil.Var ret_id, class_type)) [] I_Special Procname.Static in
|
|
|
|
let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in
|
|
|
|
let sil_exn = Sil.Const (Sil.Cexn (Sil.Var ret_id)) in
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
|
|
|
|
let set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in
|
|
|
|
let cce_instrs =
|
|
|
|
let cce_instrs =
|
|
|
|
instrs @ [call; asssume_not_instance_of] @ (new_instr :: call_instrs) @ [set_instr] in
|
|
|
|
instrs @ [call; asssume_not_instance_of] @ (new_instr :: call_instrs) @ [set_instr] in
|
|
|
|
create_node throw_cast_exception_kind (ids @ call_ids) cce_instrs in
|
|
|
|
create_node throw_cast_exception_kind cce_instrs in
|
|
|
|
|
|
|
|
|
|
|
|
Prune (is_instance_node, throw_cast_exception_node)
|
|
|
|
Prune (is_instance_node, throw_cast_exception_node)
|
|
|
|
| JBir.MonitorEnter expr ->
|
|
|
|
| JBir.MonitorEnter expr ->
|
|
|
|
|
Sam Blackshear
9 years ago
committed by
Facebook Github Bot 2