|
|
|
@ -409,7 +409,7 @@ let rec expression context pc expr =
|
|
|
|
|
let trans_var pvar =
|
|
|
|
|
let id = Ident.create_fresh Ident.knormal in
|
|
|
|
|
let sil_instr = Sil.Letderef (id, Sil.Lvar pvar, type_of_expr, loc) in
|
|
|
|
|
([id], [sil_instr], Sil.Var id) in
|
|
|
|
|
([id], [sil_instr], Sil.Var id, type_of_expr) in
|
|
|
|
|
match expr with
|
|
|
|
|
| JBir.Var (_, var) ->
|
|
|
|
|
let pvar = (JContext.set_pvar context var type_of_expr) in
|
|
|
|
@ -422,14 +422,14 @@ let rec expression context pc expr =
|
|
|
|
|
let procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
|
|
|
|
|
let pvar = Sil.mk_pvar varname procname in
|
|
|
|
|
trans_var pvar
|
|
|
|
|
| _ -> ([], [], Sil.Const (get_constant c))
|
|
|
|
|
| _ -> ([], [], Sil.Const (get_constant c), type_of_expr)
|
|
|
|
|
end
|
|
|
|
|
| JBir.Unop (unop, ex) ->
|
|
|
|
|
let type_of_ex = JTransType.expr_type context ex in
|
|
|
|
|
let (ids, instrs, sil_ex) = expression context pc ex in
|
|
|
|
|
let (ids, instrs, sil_ex, _) = expression context pc ex in
|
|
|
|
|
begin
|
|
|
|
|
match unop with
|
|
|
|
|
| JBir.Neg _ -> (ids, instrs, Sil.UnOp (Sil.Neg, sil_ex, Some type_of_expr))
|
|
|
|
|
| JBir.Neg _ -> (ids, instrs, Sil.UnOp (Sil.Neg, sil_ex, Some type_of_expr), type_of_expr)
|
|
|
|
|
| JBir.ArrayLength ->
|
|
|
|
|
let array_typ_no_ptr =
|
|
|
|
|
match type_of_ex with
|
|
|
|
@ -439,10 +439,10 @@ let rec expression context pc expr =
|
|
|
|
|
let args = [(sil_ex, type_of_ex)] 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
|
|
|
|
|
(ids @ [fresh_id; ret_id], instrs @ [deref; call_instr], Sil.Var ret_id)
|
|
|
|
|
(ids @ [fresh_id; ret_id], instrs @ [deref; call_instr], Sil.Var ret_id, type_of_expr)
|
|
|
|
|
| JBir.Conv conv ->
|
|
|
|
|
let cast_ex = Sil.Cast (JTransType.cast_type conv, sil_ex) in
|
|
|
|
|
(ids, instrs, cast_ex)
|
|
|
|
|
(ids, instrs, cast_ex, type_of_expr)
|
|
|
|
|
| JBir.InstanceOf ot | JBir.Cast ot ->
|
|
|
|
|
let subtypes =
|
|
|
|
|
(match unop with
|
|
|
|
@ -460,11 +460,11 @@ let rec expression context pc expr =
|
|
|
|
|
let ret_id = Ident.create_fresh Ident.knormal in
|
|
|
|
|
let call = Sil.Call([ret_id], builtin, args, loc, Sil.cf_default) in
|
|
|
|
|
let res_ex = Sil.Var ret_id in
|
|
|
|
|
(ids @ [ret_id], instrs @ [call], res_ex)
|
|
|
|
|
(ids @ [ret_id], instrs @ [call], res_ex, type_of_expr)
|
|
|
|
|
end
|
|
|
|
|
| JBir.Binop (binop, ex1, ex2) ->
|
|
|
|
|
let (idl1, instrs1, sil_ex1) = expression context pc ex1
|
|
|
|
|
and (idl2, instrs2, sil_ex2) = expression context pc ex2 in
|
|
|
|
|
let (idl1, instrs1, sil_ex1, _) = expression context pc ex1
|
|
|
|
|
and (idl2, instrs2, sil_ex2, _) = expression context pc ex2 in
|
|
|
|
|
begin
|
|
|
|
|
match binop with
|
|
|
|
|
| JBir.ArrayLoad _ ->
|
|
|
|
@ -476,20 +476,20 @@ let rec expression context pc expr =
|
|
|
|
|
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
|
|
|
|
|
ids, instrs, Sil.Var id
|
|
|
|
|
ids, instrs, Sil.Var id, type_of_expr
|
|
|
|
|
| other_binop ->
|
|
|
|
|
let sil_binop = get_binop other_binop in
|
|
|
|
|
let sil_expr = Sil.BinOp (sil_binop, sil_ex1, sil_ex2) in
|
|
|
|
|
(idl1 @ idl2, (instrs1 @ instrs2), sil_expr)
|
|
|
|
|
(idl1 @ idl2, (instrs1 @ instrs2), sil_expr, type_of_expr)
|
|
|
|
|
end
|
|
|
|
|
| JBir.Field (ex, cn, fs) ->
|
|
|
|
|
let (idl, instrs, sil_expr) = expression context pc ex in
|
|
|
|
|
let (idl, instrs, sil_expr, _) = expression context pc ex 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_expr = Sil.Lfield (sil_expr, field_name, sil_type) in
|
|
|
|
|
let tmp_id = Ident.create_fresh Ident.knormal in
|
|
|
|
|
let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in
|
|
|
|
|
(idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id)
|
|
|
|
|
(idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id, type_of_expr)
|
|
|
|
|
| JBir.StaticField (cn, fs) ->
|
|
|
|
|
let class_exp =
|
|
|
|
|
let classname = Mangled.from_string (JBasics.cn_name cn) in
|
|
|
|
@ -507,18 +507,21 @@ let rec expression context pc expr =
|
|
|
|
|
| Called p | Defined p -> p in
|
|
|
|
|
let field_type =
|
|
|
|
|
JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl) in
|
|
|
|
|
JTransStaticField.translate_instr_static_field context callee_procdesc fs field_type loc
|
|
|
|
|
let idl', instrs', expr' =
|
|
|
|
|
JTransStaticField.translate_instr_static_field
|
|
|
|
|
context callee_procdesc fs field_type loc in
|
|
|
|
|
idl', instrs', expr', type_of_expr
|
|
|
|
|
else
|
|
|
|
|
if JTransType.is_autogenerated_assert_field field_name
|
|
|
|
|
then
|
|
|
|
|
(* assume that reading from C.$assertionsDisabled always yields "false". this allows *)
|
|
|
|
|
(* Infer to understand the assert keyword in the expected way *)
|
|
|
|
|
(idl, instrs, Sil.exp_zero)
|
|
|
|
|
(idl, instrs, Sil.exp_zero, type_of_expr)
|
|
|
|
|
else
|
|
|
|
|
let sil_expr = Sil.Lfield (sil_expr, field_name, sil_type) in
|
|
|
|
|
let tmp_id = Ident.create_fresh Ident.knormal in
|
|
|
|
|
let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in
|
|
|
|
|
(idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id)
|
|
|
|
|
(idl @ [tmp_id], 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 =
|
|
|
|
|
(* This function tries to recursively search for the classname of the class *)
|
|
|
|
@ -575,8 +578,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
|
|
|
|
|
let (idl, instrs, call_args) =
|
|
|
|
|
IList.fold_left
|
|
|
|
|
(fun (idl_accu, instrs_accu, args_accu) expr ->
|
|
|
|
|
let (idl, instrs, sil_expr) = expression context pc expr in
|
|
|
|
|
let sil_expr_type = JTransType.expr_type context expr in
|
|
|
|
|
let (idl, instrs, sil_expr, sil_expr_type) = expression context pc expr in
|
|
|
|
|
(idl_accu @ idl, instrs_accu @ instrs, args_accu @ [(sil_expr, sil_expr_type)]))
|
|
|
|
|
init
|
|
|
|
|
expr_list in
|
|
|
|
@ -632,7 +634,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
|
|
|
|
|
|
|
|
|
|
let get_array_size context pc expr_list content_type =
|
|
|
|
|
let get_expr_instr expr other_instrs =
|
|
|
|
|
let (idl, instrs, sil_size_expr) = expression context pc expr in
|
|
|
|
|
let (idl, instrs, sil_size_expr, _) = expression context pc expr in
|
|
|
|
|
match other_instrs with
|
|
|
|
|
| (other_idl, other_instrs, other_exprs) ->
|
|
|
|
|
(idl@other_idl, instrs@other_instrs, sil_size_expr:: other_exprs) in
|
|
|
|
@ -784,8 +786,7 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
(match_never_null loc.Location.file proc_name
|
|
|
|
|
|| IList.exists (fun p -> Procname.equal p proc_name) JTransType.never_returning_null) in
|
|
|
|
|
let trans_monitor_enter_exit context expr pc loc builtin node_desc =
|
|
|
|
|
let sil_type = JTransType.expr_type context expr
|
|
|
|
|
and ids, instrs, sil_expr = expression context pc expr in
|
|
|
|
|
let ids, instrs, sil_expr, sil_type = expression context pc expr 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 node_kind = Cfg.Node.Stmt_node node_desc in
|
|
|
|
@ -793,8 +794,7 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
try
|
|
|
|
|
match instr with
|
|
|
|
|
| JBir.AffectVar (var, expr) ->
|
|
|
|
|
let (idl, stml, sil_expr) = expression context pc expr in
|
|
|
|
|
let sil_type = JTransType.expr_type context expr in
|
|
|
|
|
let (idl, stml, sil_expr, sil_type) = expression context pc expr 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 node_kind = Cfg.Node.Stmt_node "method_body" in
|
|
|
|
@ -807,7 +807,7 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
| None ->
|
|
|
|
|
create_node node_kind [] []
|
|
|
|
|
| Some expr ->
|
|
|
|
|
let (idl, stml, sil_expr) = expression context pc expr in
|
|
|
|
|
let (idl, stml, sil_expr, _) = expression context pc expr in
|
|
|
|
|
let sil_instrs =
|
|
|
|
|
let return_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_expr, loc) in
|
|
|
|
|
if return_not_null () then
|
|
|
|
@ -818,10 +818,9 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
JContext.add_goto_jump context pc JContext.Exit;
|
|
|
|
|
Instr node
|
|
|
|
|
| JBir.AffectArray (array_ex, index_ex, value_ex) ->
|
|
|
|
|
let (idl_array, instrs_array, sil_expr_array) = expression context pc array_ex
|
|
|
|
|
and (idl_index, instrs_index, sil_expr_index) = expression context pc index_ex
|
|
|
|
|
and (idl_value, instrs_value, sil_expr_value) = expression context pc value_ex
|
|
|
|
|
and arr_type = JTransType.expr_type context array_ex in
|
|
|
|
|
let (idl_array, 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 (idl_value, instrs_value, sil_expr_value, _) = expression context pc value_ex 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 final_idl = idl_array @ idl_index @ idl_value
|
|
|
|
@ -830,8 +829,8 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
let node = create_node node_kind final_idl final_instrs in
|
|
|
|
|
Instr node
|
|
|
|
|
| JBir.AffectField (e_lhs, cn, fs, e_rhs) ->
|
|
|
|
|
let (idl1, stml1, sil_expr_lhs) = expression context pc e_lhs in
|
|
|
|
|
let (idl2, stml2, sil_expr_rhs) = expression context pc e_rhs in
|
|
|
|
|
let (idl1, stml1, sil_expr_lhs, _) = expression context pc e_lhs in
|
|
|
|
|
let (idl2, stml2, sil_expr_rhs, _) = 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
|
|
|
|
@ -846,7 +845,7 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
let var_name = Sil.mk_pvar_global classname in
|
|
|
|
|
Sil.Lvar var_name in
|
|
|
|
|
let (idl1, stml1, sil_expr_lhs) = [], [], class_exp in
|
|
|
|
|
let (idl2, stml2, sil_expr_rhs) = expression context pc e_rhs in
|
|
|
|
|
let (idl2, stml2, sil_expr_rhs, _) = 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
|
|
|
|
@ -861,8 +860,8 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
Skip
|
|
|
|
|
| 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;
|
|
|
|
|
let (idl1, instrs1, sil_ex1) = expression context pc e1
|
|
|
|
|
and (idl2, instrs2, sil_ex2) = expression context pc e2 in
|
|
|
|
|
let (idl1, instrs1, sil_ex1, _) = expression context pc e1
|
|
|
|
|
and (idl2, instrs2, sil_ex2, _) = expression context pc e2 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_true = Sil.UnOp(Sil.LNot, sil_test_false, None) in
|
|
|
|
@ -880,7 +879,7 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
else
|
|
|
|
|
Prune (prune_node_true, prune_node_false)
|
|
|
|
|
| JBir.Throw expr ->
|
|
|
|
|
let (ids, instrs, sil_expr) = expression context pc expr in
|
|
|
|
|
let (ids, instrs, sil_expr, _) = expression context pc 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 node = create_node Cfg.Node.throw_kind ids (instrs @ [sil_instr]) in
|
|
|
|
@ -927,8 +926,7 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
| [arg] when is_clone ms ->
|
|
|
|
|
(* 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 *)
|
|
|
|
|
let (ids, instrs, sil_arg_expr) = expression context pc arg in
|
|
|
|
|
let arg_typ = JTransType.expr_type context arg in
|
|
|
|
|
let (ids, instrs, sil_arg_expr, arg_typ) = expression context pc arg in
|
|
|
|
|
Some (sil_arg_expr, arg_typ), [], ids, instrs
|
|
|
|
|
| _ -> None, args, [], [] in
|
|
|
|
|
let callee_procname, call_idl, call_instrs =
|
|
|
|
@ -940,9 +938,8 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
Instr call_node
|
|
|
|
|
| JBir.InvokeVirtual (var_opt, obj, call_kind, ms, args) ->
|
|
|
|
|
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
|
|
|
|
|
let sil_obj_type = JTransType.expr_type context obj in
|
|
|
|
|
let (ids, instrs, sil_obj_expr, sil_obj_type) = expression context pc obj in
|
|
|
|
|
let create_call_node cn invoke_kind =
|
|
|
|
|
let (ids, instrs, sil_obj_expr) = expression context pc obj in
|
|
|
|
|
let callee_procname, call_ids, call_instrs =
|
|
|
|
|
let ret_opt = Some (sil_obj_expr, sil_obj_type) in
|
|
|
|
|
method_invocation
|
|
|
|
@ -974,8 +971,7 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
trans_virtual_call cn I_Interface
|
|
|
|
|
end
|
|
|
|
|
| JBir.InvokeNonVirtual (var_opt, obj, cn, ms, args) ->
|
|
|
|
|
let (ids, instrs, sil_obj_expr) = expression context pc obj in
|
|
|
|
|
let sil_obj_type = JTransType.expr_type context obj in
|
|
|
|
|
let (ids, instrs, sil_obj_expr, sil_obj_type) = expression context pc obj in
|
|
|
|
|
let callee_procname, call_ids, 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
|
|
|
|
|
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
|
|
|
|
@ -987,14 +983,14 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
|
|
|
|
|
| JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks && is_this expr ->
|
|
|
|
|
(* TODO #6509339: refactor the boilterplate code in the translattion of JVM checks *)
|
|
|
|
|
let (ids, instrs, sil_expr) = expression context pc expr in
|
|
|
|
|
let (ids, instrs, sil_expr, _) = expression context pc expr in
|
|
|
|
|
let this_not_null_node =
|
|
|
|
|
create_node
|
|
|
|
|
(Cfg.Node.Stmt_node "this not null") ids (instrs @ [assume_not_null loc sil_expr]) in
|
|
|
|
|
Instr this_not_null_node
|
|
|
|
|
|
|
|
|
|
| JBir.Check (JBir.CheckNullPointer expr) when !JConfig.translate_checks ->
|
|
|
|
|
let (ids, instrs, sil_expr) = expression context pc expr in
|
|
|
|
|
let (ids, instrs, sil_expr, _) = expression context pc expr in
|
|
|
|
|
let not_null_node =
|
|
|
|
|
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)
|
|
|
|
@ -1024,11 +1020,11 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
| JBir.Check (JBir.CheckArrayBound (array_expr, index_expr)) when !JConfig.translate_checks ->
|
|
|
|
|
|
|
|
|
|
let ids, instrs, _, sil_length_expr, sil_index_expr =
|
|
|
|
|
let array_ids, array_instrs, sil_array_expr =
|
|
|
|
|
let array_ids, array_instrs, sil_array_expr, _ =
|
|
|
|
|
expression context pc array_expr
|
|
|
|
|
and length_ids, length_instrs, sil_length_expr =
|
|
|
|
|
and length_ids, length_instrs, sil_length_expr, _ =
|
|
|
|
|
expression context pc (JBir.Unop (JBir.ArrayLength, array_expr))
|
|
|
|
|
and index_ids, index_instrs, sil_index_expr =
|
|
|
|
|
and index_ids, index_instrs, sil_index_expr, _ =
|
|
|
|
|
expression context pc index_expr in
|
|
|
|
|
let ids = array_ids @ index_ids @ length_ids
|
|
|
|
|
and instrs = array_instrs @ index_instrs @ length_instrs in
|
|
|
|
@ -1080,7 +1076,7 @@ let rec instruction context pc instr : translation =
|
|
|
|
|
|
|
|
|
|
| JBir.Check (JBir.CheckCast (expr, object_type)) when !JConfig.translate_checks ->
|
|
|
|
|
let sil_type = JTransType.expr_type context expr
|
|
|
|
|
and ids, instrs, sil_expr = expression context pc expr
|
|
|
|
|
and ids, instrs, sil_expr, _ = expression context pc expr
|
|
|
|
|
and ret_id = Ident.create_fresh Ident.knormal
|
|
|
|
|
and sizeof_expr =
|
|
|
|
|
JTransType.sizeof_of_object_type program tenv object_type Sil.Subtype.subtypes_instof in
|
|
|
|
|