From c92bbf362ba2083459c9d58cc2a0cbd16bd6ec5b Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 10 May 2016 18:06:29 -0700 Subject: [PATCH] removing need to pass around lists of temporary id's in the frontend Reviewed By: jberdine Differential Revision: D3245746 fbshipit-source-id: 3594a46 --- infer/src/IR/cfg.ml | 34 ++-- infer/src/IR/cfg.mli | 25 +-- infer/src/backend/preanal.ml | 21 +-- infer/src/clang/cArithmetic_trans.ml | 76 ++++----- infer/src/clang/cArithmetic_trans.mli | 8 +- infer/src/clang/cMethod_trans.ml | 8 +- infer/src/clang/cTrans.ml | 157 ++++++++---------- infer/src/clang/cTrans_utils.ml | 66 ++++---- infer/src/clang/cTrans_utils.mli | 14 +- infer/src/harness/inhabit.ml | 20 ++- infer/src/java/jTrans.ml | 225 +++++++++++++------------- infer/src/java/jTransExn.ml | 19 ++- infer/src/java/jTransStaticField.ml | 2 +- infer/src/java/jTransStaticField.mli | 2 +- infer/src/llvm/lTrans.ml | 6 +- infer/src/unit/analyzerTester.ml | 3 +- infer/src/unit/procCfgTests.ml | 2 +- 17 files changed, 302 insertions(+), 386 deletions(-) diff --git a/infer/src/IR/cfg.ml b/infer/src/IR/cfg.ml index 038bb7136..5af42b370 100644 --- a/infer/src/IR/cfg.ml +++ b/infer/src/IR/cfg.ml @@ -34,9 +34,6 @@ module Node = struct (** distance to the exit node *) mutable nd_dist_exit : int option; - (** temporary variables *) - mutable nd_temps : Ident.t list; - (** dead program variables after executing the instructions *) mutable nd_dead_pvars_after : Pvar.t list; @@ -164,7 +161,6 @@ module Node = struct let dummy () = { nd_id = 0; nd_dist_exit = None; - nd_temps = []; nd_dead_pvars_after = []; nd_deads_before = []; nd_instrs = []; @@ -185,12 +181,11 @@ module Node = struct let get_all_nodes cfg = !(cfg.node_list) - let create cfg loc kind instrs pdesc temps = + let create cfg loc kind instrs pdesc = let node_id = node_id_gen cfg in let node = { nd_id = node_id; nd_dist_exit = None; - nd_temps = temps; nd_dead_pvars_after = []; nd_deads_before = []; nd_instrs = instrs; @@ -280,7 +275,7 @@ module Node = struct | Join_node, [({nd_kind = (Exit_node _)} as exit_node)] -> let kind = Stmt_node "between_join_and_exit" in let pdesc = get_proc_desc node in - let node' = create cfg node.nd_loc kind node.nd_instrs pdesc node.nd_temps in + let node' = create cfg node.nd_loc kind node.nd_instrs pdesc in set_succs_exn_base node [node'] exn; set_succs_exn_base node' [exit_node] exn | _ -> @@ -373,12 +368,6 @@ module Node = struct try Some (pdesc_tbl_find cfg proc_name) with Not_found -> None - let set_temps node temps = - node.nd_temps <- temps - - let get_temps node = - node.nd_temps - let set_dead_pvars node after dead = if after then node.nd_dead_pvars_after <- dead else node.nd_deads_before <- dead @@ -390,16 +379,13 @@ module Node = struct let get_distance_to_exit node = node.nd_dist_exit - (** Append the instructions and temporaries to the list of instructions to execute *) - let append_instrs_temps node instrs temps = - node.nd_instrs <- node.nd_instrs @ instrs; - node.nd_temps <- node.nd_temps @ temps + (** Append the instructions to the list of instructions to execute *) + let append_instrs node instrs = + node.nd_instrs <- node.nd_instrs @ instrs - (** Add the instructions and temporaties at the beginning - of the list of instructions to execute *) - let prepend_instrs_temps node instrs temps = - node.nd_instrs <- instrs @ node.nd_instrs; - node.nd_temps <- temps @ node.nd_temps + (** Add the instructions at the beginning of the list of instructions to execute *) + let prepend_instrs node instrs = + node.nd_instrs <- instrs @ node.nd_instrs (** Replace the instructions to be executed. *) let replace_instrs node instrs = @@ -420,7 +406,7 @@ module Node = struct (Pvar.mk x proc_name, typ) in let ptl = ret_var :: IList.map construct_decl locals in let instr = Sil.Declare_locals (ptl, loc) in - prepend_instrs_temps node [instr] [] + prepend_instrs node [instr] (** Counter for identifiers of procdescs *) let proc_desc_id_counter = ref 0 @@ -751,7 +737,7 @@ module Node = struct and kind = convert_node_kind (get_kind node) and instrs = IList.fold_left convert_instr [] (get_instrs node) |> IList.rev in - create cfg loc kind instrs resolved_proc_desc (get_temps node) + create cfg loc kind instrs resolved_proc_desc and loop callee_nodes = match callee_nodes with | [] -> [] diff --git a/infer/src/IR/cfg.mli b/infer/src/IR/cfg.mli index acbf63837..9d34d83ea 100644 --- a/infer/src/IR/cfg.mli +++ b/infer/src/IR/cfg.mli @@ -147,12 +147,11 @@ module Node : sig (** kind of Stmt_node for a throw instruction. *) val throw_kind : nodekind - (** Append the instructions and temporaries to the list of instructions to execute *) - val append_instrs_temps : t -> Sil.instr list -> Ident.t list -> unit + (** Append the instructions to the list of instructions to execute *) + val append_instrs : t -> Sil.instr list -> unit - (** Add the instructions and temporaries at the beginning - of the list of instructions to execute *) - val prepend_instrs_temps : t -> Sil.instr list -> Ident.t list -> unit + (** Add the instructions at the beginning of the list of instructions to execute *) + val prepend_instrs : t -> Sil.instr list -> unit (** Add declarations for local variables and return variable to the node *) val add_locals_ret_declaration : t -> (Mangled.t * Sil.typ) list -> unit @@ -160,10 +159,10 @@ module Node : sig (** Compare two nodes *) val compare : t -> t -> int - (** [create cfg loc kind instrs proc_desc temps] create a new cfg node + (** [create cfg loc kind instrs proc_desc] create a new cfg node with the given location, kind, list of instructions, - procdesc and list of temporary variables *) - val create : cfg -> Location.t -> nodekind -> Sil.instr list -> Procdesc.t -> Ident.t list -> t + procdesc *) + val create : cfg -> Location.t -> nodekind -> Sil.instr list -> Procdesc.t -> t (** create a new empty cfg *) val create_cfg : unit -> cfg @@ -233,9 +232,6 @@ module Node : sig (** Get the predecessor nodes of a node where the given predicate evaluates to true *) val get_sliced_preds : t -> (t -> bool) -> t list - (** Get the temporary variables introduced for the instructions stored in the node *) - val get_temps: t -> Ident.t list - (** Hash function for nodes *) val hash : t -> int @@ -270,13 +266,6 @@ module Node : sig (** Set the successor nodes and exception nodes, and build predecessor links *) val set_succs_exn : cfg -> t -> t list -> t list -> unit - - (** Set the temporary variables *) - val set_temps : t -> Ident.t list -> unit -(* - (** Replace the instructions to be executed. *) - val replace_instrs : t -> Sil.instr list -> unit -*) end (** Hash table with nodes as keys. *) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 9096899c6..7beb23532 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -236,8 +236,8 @@ let node_add_nullify_instrs n dead_vars_after dead_vars_before = (* nullification of blocks at the end of existing instructions. *) let block_nullify, no_block_nullify = IList.partition is_block_nullify (Cfg.Node.get_instrs n) in Cfg.Node.replace_instrs n (no_block_nullify @ block_nullify); - Cfg.Node.append_instrs_temps n instrs_after []; - Cfg.Node.prepend_instrs_temps n instrs_before [] + Cfg.Node.append_instrs n instrs_after; + Cfg.Node.prepend_instrs n instrs_before (** return true if the node does not assign any variables *) let node_assigns_no_variables cfg node = @@ -435,17 +435,7 @@ let add_abstraction_instructions cfg = let all_nodes = Node.get_all_nodes cfg in let do_node node = let loc = Node.get_last_loc node in - if node_requires_abstraction node then Node.append_instrs_temps node [Sil.Abstract loc] [] in - IList.iter do_node all_nodes - -(** add instructions to remove temporaries *) -let add_removetemps_instructions cfg = - let open Cfg in - let all_nodes = Node.get_all_nodes cfg in - let do_node node = - let loc = Node.get_last_loc node in - let temps = Node.get_temps node in - if temps != [] then Node.append_instrs_temps node [Sil.Remove_temps (temps, loc)] [] in + if node_requires_abstraction node then Node.append_instrs node [Sil.Abstract loc] in IList.iter do_node all_nodes module BackwardCfg = ProcCfg.Backward(ProcCfg.Exceptional) @@ -538,12 +528,12 @@ let add_nullify_instrs tenv _ pdesc = IList.filter is_local pvars |> IList.map (fun pvar -> Sil.Nullify (pvar, loc)) in if nullify_instrs <> [] - then Cfg.Node.append_instrs_temps node (IList.rev nullify_instrs) [] in + then Cfg.Node.append_instrs node (IList.rev nullify_instrs) in let node_add_removetmps_instructions node ids = if ids <> [] then let loc = Cfg.Node.get_last_loc node in - Cfg.Node.append_instrs_temps node [Sil.Remove_temps (IList.rev ids, loc)] [] in + Cfg.Node.append_instrs node [Sil.Remove_temps (IList.rev ids, loc)] in IList.iter (fun node -> @@ -576,7 +566,6 @@ let doit ?(f_translate_typ=None) cfg cg tenv = if old_nullify_analysis then begin - add_removetemps_instructions cfg; AllPreds.mk_table cfg; Cfg.iter_proc_desc cfg (analyze_and_annotate_proc cfg tenv); AllPreds.clear_table () diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index 2bb912b52..84012d4f7 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/infer/src/clang/cArithmetic_trans.ml @@ -36,22 +36,22 @@ let assignment_arc_mode e1 typ e2 loc rhs_owning_method is_e1_decl = let id = Ident.create_fresh Ident.knormal in let tmp_assign = Sil.Letderef(id, e1, typ, loc) in let release = mk_call release_pname (Sil.Var id) typ in - (e1,[retain; tmp_assign; assign; release ], [id]) + (e1,[retain; tmp_assign; assign; release]) | Sil.Tptr (_, Sil.Pk_pointer) when not rhs_owning_method && is_e1_decl -> (* for A __strong *e1 = e2 the semantics is*) (* retain(e2); e1=e2; *) let retain = mk_call retain_pname e2 typ in - (e1,[retain; assign ], []) + (e1,[retain; assign]) | Sil.Tptr (_, Sil.Pk_objc_weak) | Sil.Tptr (_, Sil.Pk_objc_unsafe_unretained) -> - (e1, [assign],[]) + (e1, [assign]) | Sil.Tptr (_, Sil.Pk_objc_autoreleasing) -> (* for __autoreleasing e1 = e2 the semantics is*) (* retain(e2); autorelease(e2); e1=e2; *) let retain = mk_call retain_pname e2 typ in let autorelease = mk_call autorelease_pname e2 typ in - (e1, [retain; autorelease; assign], []) - | _ -> (e1, [assign], []) + (e1, [retain; autorelease; assign]) + | _ -> (e1, [assign]) (* Returns a pair ([binary_expression], instructions) for binary operator representing a *) (* CompoundAssignment. "binary_expression" is returned when we are calculating an expression*) @@ -92,7 +92,7 @@ let compound_assignment_binary_operation_instruction boi e1 typ e2 loc = let e1_xor_e2 = Sil.BinOp(Sil.BXor, Sil.Var id, e2) in (e1, [Sil.Set (e1, typ, e1_xor_e2, loc)]) | _ -> assert false in - (e_res, instr1:: instr_op, [id]) + (e_res, instr1:: instr_op) (* Returns a pair ([binary_expression], instructions). "binary_expression" *) (* is returned when we are calculating an expression "instructions" is not *) @@ -101,30 +101,30 @@ let compound_assignment_binary_operation_instruction boi e1 typ e2 loc = let binary_operation_instruction context boi e1 typ e2 loc rhs_owning_method = let binop_exp op = Sil.BinOp(op, e1, e2) in match boi.Clang_ast_t.boi_kind with - | `Add -> (binop_exp (Sil.PlusA), [], []) - | `Mul -> (binop_exp (Sil.Mult), [], []) - | `Div -> (binop_exp (Sil.Div), [], []) - | `Rem -> (binop_exp (Sil.Mod), [], []) - | `Sub -> (binop_exp (Sil.MinusA), [], []) - | `Shl -> (binop_exp (Sil.Shiftlt), [], []) - | `Shr -> (binop_exp(Sil.Shiftrt), [], []) - | `Or -> (binop_exp (Sil.BOr), [], []) - | `And -> (binop_exp (Sil.BAnd), [], []) - | `Xor -> (binop_exp (Sil.BXor), [], []) - | `LT -> (binop_exp (Sil.Lt), [], []) - | `GT -> (binop_exp (Sil.Gt), [], []) - | `LE -> (binop_exp (Sil.Le), [], []) - | `GE -> (binop_exp (Sil.Ge), [], []) - | `NE -> (binop_exp (Sil.Ne), [], []) - | `EQ -> (binop_exp (Sil.Eq), [], []) - | `LAnd -> (binop_exp (Sil.LAnd), [], []) - | `LOr -> (binop_exp (Sil.LOr), [], []) + | `Add -> (binop_exp (Sil.PlusA), []) + | `Mul -> (binop_exp (Sil.Mult), []) + | `Div -> (binop_exp (Sil.Div), []) + | `Rem -> (binop_exp (Sil.Mod), []) + | `Sub -> (binop_exp (Sil.MinusA), []) + | `Shl -> (binop_exp (Sil.Shiftlt), []) + | `Shr -> (binop_exp(Sil.Shiftrt), []) + | `Or -> (binop_exp (Sil.BOr), []) + | `And -> (binop_exp (Sil.BAnd), []) + | `Xor -> (binop_exp (Sil.BXor), []) + | `LT -> (binop_exp (Sil.Lt), []) + | `GT -> (binop_exp (Sil.Gt), []) + | `LE -> (binop_exp (Sil.Le), []) + | `GE -> (binop_exp (Sil.Ge), []) + | `NE -> (binop_exp (Sil.Ne), []) + | `EQ -> (binop_exp (Sil.Eq), []) + | `LAnd -> (binop_exp (Sil.LAnd), []) + | `LOr -> (binop_exp (Sil.LOr), []) | `Assign -> if !Config.arc_mode && ObjcInterface_decl.is_pointer_to_objc_class context.CContext.tenv typ then assignment_arc_mode e1 typ e2 loc rhs_owning_method false else - (e1, [Sil.Set (e1, typ, e2, loc)], []) - | `Comma -> (e2, [], []) (* C99 6.5.17-2 *) + (e1, [Sil.Set (e1, typ, e2, loc)]) + | `Comma -> (e2, []) (* C99 6.5.17-2 *) | `MulAssign | `DivAssign | `RemAssign | `AddAssign | `SubAssign | `ShlAssign | `ShrAssign | `AndAssign | `XorAssign | `OrAssign -> compound_assignment_binary_operation_instruction boi e1 typ e2 loc @@ -134,7 +134,7 @@ let binary_operation_instruction context boi e1 typ e2 loc rhs_owning_method = Printing.log_stats "\nWARNING: Missing translation for Binary Operator Kind %s. Construct ignored...\n" (Clang_ast_j.string_of_binary_operator_kind bok); - (Sil.exp_minus_one, [], []) + (Sil.exp_minus_one, []) let unary_operation_instruction uoi e typ loc = let uok = Clang_ast_j.string_of_unary_operator_kind (uoi.Clang_ast_t.uoi_kind) in @@ -145,7 +145,7 @@ let unary_operation_instruction uoi e typ loc = let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Letderef (id, e, typ, loc) in let e_plus_1 = Sil.BinOp(Sil.PlusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in - ([id], Sil.Var id, instr1::[Sil.Set (e, typ, e_plus_1, loc)]) + (Sil.Var id, instr1::[Sil.Set (e, typ, e_plus_1, loc)]) | `PreInc -> let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Letderef (id, e, typ, loc) in @@ -154,12 +154,12 @@ let unary_operation_instruction uoi e typ loc = e else e_plus_1 in - ([id], exp, instr1::[Sil.Set (e, typ, e_plus_1, loc)]) + (exp, instr1::[Sil.Set (e, typ, e_plus_1, loc)]) | `PostDec -> let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Letderef (id, e, typ, loc) in let e_minus_1 = Sil.BinOp(Sil.MinusA, Sil.Var id, Sil.Const(Sil.Cint (Sil.Int.one))) in - ([id], Sil.Var id, instr1::[Sil.Set (e, typ, e_minus_1, loc)]) + (Sil.Var id, instr1::[Sil.Set (e, typ, e_minus_1, loc)]) | `PreDec -> let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Letderef (id, e, typ, loc) in @@ -168,19 +168,19 @@ let unary_operation_instruction uoi e typ loc = e else e_minus_1 in - ([id], exp, instr1::[Sil.Set (e, typ, e_minus_1, loc)]) - | `Not -> ([], un_exp (Sil.BNot), []) - | `Minus -> ([], un_exp (Sil.Neg), []) - | `Plus -> ([], e, []) - | `LNot -> ([], un_exp (Sil.LNot), []) + (exp, instr1::[Sil.Set (e, typ, e_minus_1, loc)]) + | `Not -> (un_exp (Sil.BNot), []) + | `Minus -> (un_exp (Sil.Neg), []) + | `Plus -> (e, []) + | `LNot -> (un_exp (Sil.LNot), []) | `Deref -> (* Actual dereferencing is handled by implicit cast from rvalue to lvalue *) - ([], e, []) - | `AddrOf -> ([], e, []) + (e, []) + | `AddrOf -> (e, []) | `Real | `Imag | `Extension | `Coawait -> Printing.log_stats "\nWARNING: Missing translation for Unary Operator Kind %s. The construct has been ignored...\n" uok; - ([], e, []) + (e, []) let bin_op_to_string boi = match boi.Clang_ast_t.boi_kind with diff --git a/infer/src/clang/cArithmetic_trans.mli b/infer/src/clang/cArithmetic_trans.mli index b3afb93f1..0f24f1d5a 100644 --- a/infer/src/clang/cArithmetic_trans.mli +++ b/infer/src/clang/cArithmetic_trans.mli @@ -15,14 +15,12 @@ val bin_op_to_string : Clang_ast_t.binary_operator_info -> string val binary_operation_instruction : CContext.t -> Clang_ast_t.binary_operator_info -> Sil.exp -> Sil.typ -> Sil.exp -> - Location.t -> bool -> Sil.exp * Sil.instr list * Ident.t list + Location.t -> bool -> Sil.exp * Sil.instr list val unary_operation_instruction : - Clang_ast_t.unary_operator_info -> Sil.exp -> Sil.typ -> Location.t -> - Ident.t list * Sil.exp * Sil.instr list + Clang_ast_t.unary_operator_info -> Sil.exp -> Sil.typ -> Location.t -> Sil.exp * Sil.instr list val assignment_arc_mode : - Sil.exp -> Sil.typ -> Sil.exp -> Location.t -> bool -> bool -> - Sil.exp * Sil.instr list * Ident.t list + Sil.exp -> Sil.typ -> Sil.exp -> Location.t -> bool -> bool -> Sil.exp * Sil.instr list val sil_const_plus_one : Sil.exp -> Sil.exp diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index f3dd7903b..9b3f5c1f2 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -398,9 +398,9 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method = (if !Config.arc_mode then Cfg.Procdesc.set_flag procdesc Mleak_buckets.objc_arc_flag "true"; 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_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc [] in + let exit_node = Cfg.Node.create cfg loc_exit exit_kind [] procdesc in Cfg.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_exit_node procdesc exit_node) in if should_create_procdesc cfg proc_name defined then @@ -454,8 +454,8 @@ let get_method_for_frontend_checks cfg cg loc = loc = loc; } in let pdesc = Cfg.Procdesc.create cfg attrs in - let start_node = Cfg.Node.create cfg loc (Cfg.Node.Start_node pdesc) [] pdesc [] in - let exit_node = Cfg.Node.create cfg loc (Cfg.Node.Exit_node pdesc) [] pdesc [] in + let start_node = Cfg.Node.create cfg loc (Cfg.Node.Start_node pdesc) [] pdesc in + let exit_node = Cfg.Node.create cfg loc (Cfg.Node.Exit_node pdesc) [] pdesc in Cfg.Procdesc.set_start_node pdesc start_node; Cfg.Procdesc.set_exit_node pdesc exit_node; Cfg.Node.set_succs_exn cfg start_node [exit_node] []; diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index da33f9fd8..e2c018ddf 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -85,8 +85,8 @@ struct let ret_id = Ident.create_fresh Ident.knormal in let stmt_call = Sil.Call ([ret_id], (Sil.Const (Sil.Cfun fname)), [(exp, typ)], sil_loc, Sil.cf_default) in - ([ret_id], [stmt_call]) - else ([], []) + [stmt_call] + else [] let rec is_block_expr s = let open Clang_ast_t in @@ -157,20 +157,17 @@ struct (declare_block_local :: trans_res.instrs) @ [set_instr] @ captured_instrs @ - set_fields, - id_block :: ids + set_fields (* From a list of expression extract blocks from tuples and *) (* returns block names and assignment to temp vars *) let extract_block_from_tuple procname exps loc = let insts = ref [] in - let ids = ref [] in let make_function_name typ bn = let bn'= Procname.to_string bn in let bn''= Mangled.from_string bn' in let block = Sil.Lvar (Pvar.mk bn'' procname) in let id = Ident.create_fresh Ident.knormal in - ids := id :: !ids; insts := Sil.Letderef (id, block, typ, loc) :: !insts; (Sil.Var id, typ) in let make_arg typ (id, _, _) = (id, typ) in @@ -185,7 +182,7 @@ struct function_name :: args in app @ (f es') | e :: es' -> e :: f es' in - (f exps, !insts, !ids) + (f exps, !insts) let collect_exprs res_trans_list = IList.flatten (IList.map (fun res_trans -> res_trans.exps) res_trans_list) @@ -319,7 +316,6 @@ struct else ret_id, params_sil, [], match ret_id with [x] -> [(Sil.Var x, return_type)] | _ -> [] in let call_instr = Sil.Call (ret_id', function_sil, params, sil_loc, call_flags) in { empty_res_trans with - ids = ret_id'; instrs = [call_instr]; exps = ret_exps; initd_exps = initd_exps;} @@ -382,20 +378,19 @@ struct (* type like long, unsigned long, etc *) and integerLiteral_trans trans_state expr_info integer_literal_info = let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in - let exp, ids = + let exp = try let i = Int64.of_string integer_literal_info.Clang_ast_t.ili_value in let exp = Sil.exp_int (Sil.Int.of_int64 i) in - exp, [] + exp with | Failure _ -> (* Parse error: return a nondeterministic value *) let id = Ident.create_fresh Ident.knormal in - let exp = Sil.Var id in - exp, [id] in + Sil.Var id in { empty_res_trans with exps = [(exp, typ)]; - ids = ids; } + } let cxxScalarValueInitExpr_trans trans_state expr_info = let typ = CTypes_decl.get_type_from_expr_info expr_info trans_state.context.CContext.tenv in @@ -530,15 +525,14 @@ struct (* constructor's initializer list (when reference itself is initialized) *) let should_add_deref = (not is_pointer_typ) || (not is_constructor_init && CTypes.is_reference_type type_ptr) in - let exp, deref_ids, deref_instrs = if should_add_deref then + let exp, deref_instrs = if should_add_deref then let id = Ident.create_fresh Ident.knormal in let deref_instr = Sil.Letderef (id, field_exp, field_typ, sil_loc) in - Sil.Var id, [id], [deref_instr] + Sil.Var id, [deref_instr] else - field_exp, [], [] in + field_exp, [] in let instrs = pre_trans_result.instrs @ deref_instrs in - let ids = pre_trans_result.ids @ deref_ids in - { pre_trans_result with ids; instrs; exps = [(exp, field_typ)] } + { pre_trans_result with instrs; exps = [(exp, field_typ)] } let method_deref_trans trans_state pre_trans_result decl_ref stmt_info decl_kind = let open CContext in @@ -558,27 +552,27 @@ struct let is_cpp_virtual = match ms_opt with | Some ms -> CMethod_signature.ms_is_cpp_virtual ms | _ -> false in - let extra_exps, extra_ids, extra_instrs = if is_instance_method then ( + let extra_exps, extra_instrs = if is_instance_method then ( (* pre_trans_result.exps may contain expr for 'this' parameter:*) (* if it comes from CXXMemberCallExpr it will be there *) (* if it comes from CXXOperatorCallExpr it won't be there and will be added later *) (* In case of CXXMemberCallExpr it's possible that type of 'this' parameter *) (* won't have a pointer - if that happens add a pointer to type of the object *) match pre_trans_result.exps with - | [] -> [], [], [] + | [] -> [], [] (* We need to add a dereference before a method call to find null dereferences when *) (* calling a method with null *) | [(exp, Sil.Tptr (typ, _) )] when decl_kind <> `CXXConstructor -> let typ = CTypes.expand_structured_type context.tenv typ in - let extra_ids, extra_instrs, _ = CTrans_utils.dereference_var_sil (exp, typ) sil_loc in - pre_trans_result.exps, extra_ids, extra_instrs - | [(_, Sil.Tptr _ )] -> pre_trans_result.exps, [], [] - | [(sil, typ)] -> [(sil, Sil.Tptr (typ, Sil.Pk_reference))], [], [] + let extra_instrs, _ = CTrans_utils.dereference_var_sil (exp, typ) sil_loc in + pre_trans_result.exps, extra_instrs + | [(_, Sil.Tptr _ )] -> pre_trans_result.exps, [] + | [(sil, typ)] -> [(sil, Sil.Tptr (typ, Sil.Pk_reference))], [] | _ -> assert false ) else (* don't add 'this' expression for static methods *) - [], [], [] in + [], [] in (* consider using context.CContext.is_callee_expression to deal with pointers to methods? *) (* unlike field access, for method calls there is no need to expand class type *) let pname = CMethod_trans.create_procdesc_with_pointer context decl_ptr (Some class_name) @@ -589,7 +583,7 @@ struct is_cpp_call_virtual = is_cpp_virtual; exps = [method_exp] @ extra_exps; instrs = pre_trans_result.instrs @ extra_instrs; - ids = pre_trans_result.ids @ extra_ids } + } let destructor_deref_trans trans_state pvar_trans_result class_type_ptr si = let open Clang_ast_t in @@ -729,7 +723,6 @@ struct { empty_res_trans with root_nodes; leaf_nodes; - ids = res_trans_idx.ids @ res_trans_a.ids; instrs = res_trans_a.instrs @ res_trans_idx.instrs; exps = [(array_exp, typ)]; initd_exps = res_trans_idx.initd_exps @ res_trans_a.initd_exps; } @@ -766,14 +759,15 @@ struct let binop_res_trans, exp_to_parent = if IList.exists (Sil.exp_equal var_exp) res_trans_e2.initd_exps then [], [] else - let exp_op, instr_bin, ids_bin = CArithmetic_trans.binary_operation_instruction + let exp_op, instr_bin = + CArithmetic_trans.binary_operation_instruction context binary_operator_info var_exp typ sil_e2 sil_loc rhs_owning_method in (* Create a node if the priority if free and there are instructions *) let creating_node = (PriorityNode.own_priority_node trans_state_pri.priority stmt_info) && (IList.length instr_bin >0) in - let extra_instrs, extra_ids, exp_to_parent = + let extra_instrs, exp_to_parent = if (is_binary_assign_op binary_operator_info) (* assignment operator result is lvalue in CPP, rvalue in C, *) (* hence the difference *) @@ -785,11 +779,10 @@ struct (* As no node is created here ids are passed to the parent *) let id = Ident.create_fresh Ident.knormal in let res_instr = Sil.Letderef (id, var_exp, var_exp_typ, sil_loc) in - [res_instr], [id], Sil.Var id + [res_instr], Sil.Var id ) else ( - [], [], exp_op) in + [], exp_op) in let binop_res_trans = { empty_res_trans with - ids = ids_bin @ extra_ids; instrs = instr_bin @ extra_instrs } in [binop_res_trans], [(exp_to_parent, var_exp_typ)] in @@ -862,11 +855,10 @@ struct | None -> let res_trans_call = match cast_trans context act_params sil_loc callee_pname_opt function_type with - | Some (id, instr, _) -> + | Some (instr, cast_exp) -> { empty_res_trans with - ids = [id]; instrs = [instr]; - exps = [(Sil.Var id, function_type)]; } + exps = [(cast_exp, function_type)]; } | None -> let call_flags = { Sil.cf_default with Sil.cf_is_objc_block = is_call_to_block; } in create_call_instr trans_state function_type sil_fe act_params sil_loc call_flags @@ -1054,10 +1046,9 @@ struct let is_virtual = method_call_type = CMethod_trans.MCVirtual in Cg.add_edge context.CContext.cg procname callee_name; - let param_exps, instr_block_param, ids_block_param = + let param_exps, instr_block_param = extract_block_from_tuple procname subexpr_exprs sil_loc in let res_trans_block = { empty_res_trans with - ids = ids_block_param; instrs = instr_block_param; } in let call_flags = { Sil.cf_default with Sil.cf_virtual = is_virtual; } in @@ -1121,7 +1112,7 @@ struct CTypes_decl.type_ptr_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in let var_typ = add_reference_if_glvalue typ expr_info in - let join_node = create_node (Cfg.Node.Join_node) [] [] sil_loc context in + let join_node = create_node (Cfg.Node.Join_node) [] sil_loc context in Cfg.Node.set_succs_exn cfg join_node succ_nodes []; let pvar = mk_temp_sil_var procdesc "SIL_temp_conditional___" in Cfg.Procdesc.append_locals procdesc [(Pvar.get_name pvar, var_typ)]; @@ -1136,7 +1127,6 @@ struct { empty_res_trans with root_nodes = res_trans_cond.root_nodes; leaf_nodes = [join_node]; - ids = [id]; instrs = instrs; exps = [(Sil.Var id, typ)]; initd_exps = []; (* TODO we should get exps from branches+cond *) @@ -1164,8 +1154,7 @@ struct "BinaryConditinalStmt Init" stmt_info [init_res_trans] in let root_nodes = init_res_trans'.root_nodes in let root_nodes' = if root_nodes <> [] then root_nodes else op_res_trans.root_nodes in - let ids = op_res_trans.ids @ init_res_trans'.ids in - { op_res_trans with root_nodes = root_nodes'; ids = ids } + { op_res_trans with root_nodes = root_nodes'; } | _ -> Printing.log_stats "BinaryConditionalOperator not translated@."; assert false @@ -1176,8 +1165,8 @@ struct let context = trans_state.context in let si, _ = Clang_ast_proj.get_stmt_tuple cond in let sil_loc = CLocation.get_sil_location si context in - let mk_prune_node b e ids ins = - create_prune_node b e ids ins sil_loc (Sil.Ik_if) context in + let mk_prune_node b e ins = + create_prune_node b e ins sil_loc (Sil.Ik_if) context in let extract_exp el = extract_exp_from_list el "\nWARNING: Missing expression for Conditional operator. Need to be fixed" in @@ -1193,8 +1182,8 @@ struct instruction trans_state cond in let e', instrs' = define_condition_side_effects res_trans_cond.exps res_trans_cond.instrs sil_loc in - let prune_t = mk_prune_node true e' res_trans_cond.ids instrs' in - let prune_f = mk_prune_node false e' res_trans_cond.ids instrs' in + let prune_t = mk_prune_node true e' instrs' in + let prune_f = mk_prune_node false e' instrs' in IList.iter (fun n' -> Cfg.Node.set_succs_exn context.cfg n' [prune_t; prune_f] []) res_trans_cond.leaf_nodes; @@ -1204,7 +1193,6 @@ struct { empty_res_trans with root_nodes = rnodes; leaf_nodes = [prune_t; prune_f]; - ids = res_trans_cond.ids; instrs = instrs'; exps = e'; } in @@ -1242,7 +1230,6 @@ struct { empty_res_trans with root_nodes = root_nodes_to_parent; leaf_nodes = prune_to_short_c@res_trans_s2.leaf_nodes; - ids = res_trans_s1.ids@res_trans_s2.ids; instrs = res_trans_s1.instrs@res_trans_s2.instrs; exps = [(e_cond, typ1)]; } in @@ -1271,7 +1258,7 @@ struct let context = trans_state.context in let succ_nodes = trans_state.succ_nodes in let sil_loc = CLocation.get_sil_location stmt_info context in - let join_node = create_node (Cfg.Node.Join_node) [] [] sil_loc context in + let join_node = create_node (Cfg.Node.Join_node) [] sil_loc context in Cfg.Node.set_succs_exn context.cfg join_node succ_nodes []; let trans_state' = { trans_state with succ_nodes = [join_node] } in let do_branch branch stmt_branch prune_nodes = @@ -1280,14 +1267,12 @@ struct let nodes_branch = (match res_trans_b.root_nodes with | [] -> - [create_node (Cfg.Node.Stmt_node "IfStmt Branch" ) - res_trans_b.ids res_trans_b.instrs sil_loc context] + [create_node (Cfg.Node.Stmt_node "IfStmt Branch") res_trans_b.instrs sil_loc context] | _ -> res_trans_b.root_nodes) in let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes in let prune_nodes' = if branch then prune_nodes_t else prune_nodes_f in - IList.iter (fun n -> Cfg.Node.set_succs_exn context.cfg n nodes_branch []) prune_nodes'; - res_trans_b.ids in + IList.iter (fun n -> Cfg.Node.set_succs_exn context.cfg n nodes_branch []) prune_nodes' in (match stmt_list with | [decl_stmt; cond; stmt1; stmt2] -> (* set the flat to inform that we are translating a condition of a if *) @@ -1299,12 +1284,11 @@ struct let res_trans_cond = cond_trans trans_state'' cond in let res_trans_decl = declStmt_in_condition_trans trans_state decl_stmt res_trans_cond in (* Note: by contruction prune nodes are leafs_nodes_cond *) - let ids_t = do_branch true stmt1 res_trans_cond.leaf_nodes in - let ids_f = do_branch false stmt2 res_trans_cond.leaf_nodes in + do_branch true stmt1 res_trans_cond.leaf_nodes; + do_branch false stmt2 res_trans_cond.leaf_nodes; { empty_res_trans with root_nodes = res_trans_decl.root_nodes; leaf_nodes = [join_node]; - ids = res_trans_decl.ids @ res_trans_cond.ids @ ids_t @ ids_f; } | _ -> assert false) @@ -1322,7 +1306,7 @@ struct let res_trans_cond_tmp = instruction trans_state' cond in let switch_special_cond_node = let node_kind = Cfg.Node.Stmt_node "Switch_stmt" in - create_node node_kind [] res_trans_cond_tmp.instrs sil_loc context in + create_node node_kind res_trans_cond_tmp.instrs sil_loc context in IList.iter (fun n' -> Cfg.Node.set_succs_exn context.cfg n' [switch_special_cond_node] []) res_trans_cond_tmp.leaf_nodes; @@ -1408,12 +1392,10 @@ struct let sil_loc = CLocation.get_sil_location stmt_info context in let true_prune_node = create_prune_node true [(sil_eq_cond, switch_e_cond'_typ)] - res_trans_case_const.ids res_trans_case_const.instrs - sil_loc Sil.Ik_switch context in + res_trans_case_const.instrs sil_loc Sil.Ik_switch context in let false_prune_node = create_prune_node false [(sil_eq_cond, switch_e_cond'_typ)] - res_trans_case_const.ids res_trans_case_const.instrs - sil_loc Sil.Ik_switch context in + res_trans_case_const.instrs sil_loc Sil.Ik_switch context in (true_prune_node, false_prune_node) | _ -> assert false in match cases with (* top-down to handle default cases *) @@ -1430,7 +1412,7 @@ struct | DefaultStmt(stmt_info, default_content) :: rest -> let sil_loc = CLocation.get_sil_location stmt_info context in let placeholder_entry_point = - create_node (Cfg.Node.Stmt_node "DefaultStmt_placeholder") [] [] sil_loc context in + create_node (Cfg.Node.Stmt_node "DefaultStmt_placeholder") [] sil_loc context in let last_nodes, last_prune_nodes = translate_and_connect_cases rest next_nodes [placeholder_entry_point] in let default_entry_point = @@ -1444,7 +1426,7 @@ struct Cfg.Node.set_succs_exn context.cfg switch_special_cond_node top_prune_nodes []; let top_nodes = res_trans_decl.root_nodes in IList.iter - (fun n' -> Cfg.Node.append_instrs_temps n' [] res_trans_cond.ids) succ_nodes; + (fun n' -> Cfg.Node.append_instrs n' []) succ_nodes; (* succ_nodes will remove the temps *) { empty_res_trans with root_nodes = top_nodes; leaf_nodes = succ_nodes } | _ -> assert false @@ -1455,7 +1437,6 @@ struct extract_stmt_from_singleton stmt_list "ERROR: StmtExpr should have only one statement.\n" in let res_trans_stmt = instruction trans_state stmt in - let idl = res_trans_stmt.ids in let exps' = IList.rev res_trans_stmt.exps in match exps' with | (last, typ) :: _ -> @@ -1467,7 +1448,6 @@ struct let loc = CLocation.get_sil_location stmt_info context in let instr' = Sil.Letderef (id, last, typ, loc) in { res_trans_stmt with - ids = id :: idl; instrs = res_trans_stmt.instrs @ [instr']; exps = [(Sil.Var id, typ)]; } @@ -1478,7 +1458,7 @@ struct let context = trans_state.context in let succ_nodes = trans_state.succ_nodes in let sil_loc = CLocation.get_sil_location stmt_info context in - let join_node = create_node Cfg.Node.Join_node [] [] sil_loc context in + let join_node = create_node Cfg.Node.Join_node [] sil_loc context in let continuation = Some { break = succ_nodes; continue = [join_node]; return_temp = false } in (* set the flat to inform that we are translating a condition of a if *) let continuation_cond = mk_cond_continuation outer_continuation in @@ -1682,9 +1662,9 @@ struct let (sil_e1', ie_typ) = extract_exp_from_list res_trans_ie.exps "WARNING: In DeclStmt we expect only one expression returned in recursive call\n" in let rhs_owning_method = CTrans_utils.is_owning_method ie in - let _, instrs_assign, ids_assign = + let _, instrs_assign = (* variable might be initialized already - do nothing in that case*) - if IList.exists (Sil.exp_equal var_exp) res_trans_ie.initd_exps then ([], [], []) + if IList.exists (Sil.exp_equal var_exp) res_trans_ie.initd_exps then ([], []) else if !Config.arc_mode && (CTrans_utils.is_method_call ie || ObjcInterface_decl.is_pointer_to_objc_class context.CContext.tenv ie_typ) @@ -1692,14 +1672,13 @@ struct (* In arc mode, if it's a method call or we are initializing with a pointer to objc class *) (* we need to add retain/release *) - let (e, instrs, ids) = + let (e, instrs) = CArithmetic_trans.assignment_arc_mode var_exp ie_typ sil_e1' sil_loc rhs_owning_method true in - ([(e, ie_typ)], instrs, ids) + ([(e, ie_typ)], instrs) else - ([], [Sil.Set (var_exp, ie_typ, sil_e1', sil_loc)], []) in + ([], [Sil.Set (var_exp, ie_typ, sil_e1', sil_loc)]) in let res_trans_assign = { empty_res_trans with - ids = ids_assign; instrs = instrs_assign } in let all_res_trans = [res_trans_ie; res_trans_assign] in let res_trans = PriorityNode.compute_results_to_parent trans_state_pri sil_loc "DeclStmt" @@ -1727,7 +1706,6 @@ struct let res_trans_tmp = do_var_dec (di, n, tp, vdi) res_trans_vd.root_nodes in { empty_res_trans with root_nodes = res_trans_tmp.root_nodes; leaf_nodes = []; - ids = res_trans_tmp.ids @ res_trans_vd.ids; instrs = res_trans_tmp.instrs @ res_trans_vd.instrs; exps = res_trans_tmp.exps @ res_trans_vd.exps; initd_exps = res_trans_tmp.initd_exps @ res_trans_vd.initd_exps; @@ -1821,10 +1799,9 @@ struct let is_objc_bridged_cast_expr _ stmt = match stmt with | Clang_ast_t.ObjCBridgedCastExpr _ -> true | _ -> false in let is_objc_bridged = Ast_utils.exists_eventually_st is_objc_bridged_cast_expr () stmt in - let cast_ids, cast_inst, cast_exp = + let cast_inst, cast_exp = cast_operation trans_state cast_kind res_trans_stmt.exps typ sil_loc is_objc_bridged in { res_trans_stmt with - ids = res_trans_stmt.ids @ cast_ids; instrs = res_trans_stmt.instrs @ cast_inst; exps = [cast_exp]; } @@ -1866,9 +1843,9 @@ struct let ret_typ = CTypes_decl.type_ptr_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in - let ids_op, exp_op, instr_op = + let exp_op, instr_op = CArithmetic_trans.unary_operation_instruction unary_operator_info sil_e' ret_typ sil_loc in - let unary_op_res_trans = { empty_res_trans with ids = ids_op; instrs = instr_op } in + let unary_op_res_trans = { empty_res_trans with instrs = instr_op } in let all_res_trans = [ res_trans_stmt; unary_op_res_trans ] in let nname = "UnaryOperator" in let res_trans_to_parent = PriorityNode.compute_results_to_parent trans_state_pri sil_loc nname @@ -1880,8 +1857,8 @@ struct let succ_nodes = trans_state.succ_nodes in let sil_loc = CLocation.get_sil_location stmt_info context in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in - let mk_ret_node ids instrs = - let ret_node = create_node (Cfg.Node.Stmt_node "Return Stmt") ids instrs sil_loc context in + let mk_ret_node instrs = + let ret_node = create_node (Cfg.Node.Stmt_node "Return Stmt") instrs sil_loc context in Cfg.Node.set_succs_exn context.cfg ret_node [(Cfg.Procdesc.get_exit_node context.CContext.procdesc)] []; ret_node in @@ -1889,7 +1866,7 @@ struct | [stmt] -> (* return exp; *) let procdesc = context.CContext.procdesc in let ret_type = Cfg.Procdesc.get_ret_type procdesc in - let ret_exp, ret_typ, var_instrs, var_ids = match context.CContext.return_param_typ with + let ret_exp, ret_typ, var_instrs = match context.CContext.return_param_typ with | Some ret_param_typ -> let name = CFrontend_config.return_param in let procname = Cfg.Procdesc.get_proc_name procdesc in @@ -1897,9 +1874,9 @@ struct let id = Ident.create_fresh Ident.knormal in let instr = Sil.Letderef (id, Sil.Lvar pvar, ret_param_typ, sil_loc) in let ret_typ = match ret_param_typ with Sil.Tptr (t, _) -> t | _ -> assert false in - Sil.Var id, ret_typ, [instr], [id] + Sil.Var id, ret_typ, [instr] | None -> - Sil.Lvar (Cfg.Procdesc.get_ret_var procdesc), ret_type, [], [] in + Sil.Lvar (Cfg.Procdesc.get_ret_var procdesc), ret_type, [] in let trans_state' = { trans_state_pri with succ_nodes = []; var_exp_typ = Some (ret_exp, ret_typ) } in @@ -1910,11 +1887,10 @@ struct let ret_instrs = if IList.exists (Sil.exp_equal ret_exp) res_trans_stmt.initd_exps then [] else [Sil.Set (ret_exp, ret_type, sil_expr, sil_loc)] in - let autorelease_ids, autorelease_instrs = + let autorelease_instrs = add_autorelease_call context sil_expr ret_type sil_loc in let instrs = var_instrs @ res_trans_stmt.instrs @ ret_instrs @ autorelease_instrs in - let ids = var_ids @ res_trans_stmt.ids @ autorelease_ids in - let ret_node = mk_ret_node ids instrs in + let ret_node = mk_ret_node instrs in IList.iter (fun n -> Cfg.Node.set_succs_exn context.cfg n [ret_node] []) res_trans_stmt.leaf_nodes; @@ -1924,7 +1900,7 @@ struct else [ret_node] in { empty_res_trans with root_nodes = root_nodes_to_parent; leaf_nodes = [ret_node]} | [] -> (* return; *) - let ret_node = mk_ret_node [] [] in + let ret_node = mk_ret_node [] in { empty_res_trans with root_nodes = [ret_node]; leaf_nodes = [ret_node]} | _ -> Printing.log_out "\nWARNING: Missing translation of Return Expression. \ @@ -2000,7 +1976,7 @@ struct Sil.Call([ret_id], (Sil.Const (Sil.Cfun fname)), autorelease_pool_vars, sil_loc, Sil.cf_default) in let node_kind = Cfg.Node.Stmt_node ("Release the autorelease pool") in - let call_node = create_node node_kind ([ret_id]) ([stmt_call]) sil_loc context in + let call_node = create_node node_kind [stmt_call] sil_loc context in Cfg.Node.set_succs_exn context.cfg call_node trans_state.succ_nodes []; let trans_state'={ trans_state with continuation = None; succ_nodes =[call_node] } in instructions trans_state' stmts @@ -2048,10 +2024,9 @@ struct let block_name = Procname.to_string block_pname in let static_vars = CContext.static_vars_for_block context block_pname in let captured_static_vars = captureds @ static_vars in - let alloc_block_instr, ids_block = + let alloc_block_instr = allocate_block trans_state block_name captured_static_vars loc in { empty_res_trans with - ids = ids_block @ ids; instrs = alloc_block_instr @ instrs; exps = [(Sil.Const closure, typ)]; } @@ -2211,7 +2186,7 @@ struct let ret_id = Ident.create_fresh Ident.knormal in let call = Sil.Call ([ret_id], builtin, args, sil_loc, Sil.cf_default) in let res_ex = Sil.Var ret_id in - let res_trans_dynamic_cast = { empty_res_trans with instrs = [call]; ids = [ret_id] } in + let res_trans_dynamic_cast = { empty_res_trans with instrs = [call]; } in let all_res_trans = [ res_trans_stmt; res_trans_dynamic_cast ] in let nname = "CxxDynamicCast" in let res_trans_to_parent = PriorityNode.compute_results_to_parent trans_state_pri sil_loc nname @@ -2234,7 +2209,6 @@ struct let sil_fun = Sil.Const (Sil.Cfun fun_name) in let call_instr = Sil.Call ([], sil_fun, params, sil_loc, Sil.cf_default) in let res_trans_call = { empty_res_trans with - ids = []; instrs = [call_instr]; exps = []; } in let all_res_trans = res_trans_subexpr_list @ [res_trans_call] in @@ -2268,7 +2242,6 @@ struct let args = [type_info_objc; (field_exp, Sil.Tvoid)] @ res_trans_subexpr.exps in let call_instr = Sil.Call ([ret_id], sil_fun, args, sil_loc, Sil.cf_default) in let res_trans_call = { empty_res_trans with - ids = [ret_id]; instrs = [call_instr]; exps = [(ret_exp, typ)]; } in let all_res_trans = [res_trans_subexpr; res_trans_call] in @@ -2292,7 +2265,6 @@ struct let ret_exp = Sil.Var ret_id in let call_instr = Sil.Call ([ret_id], sil_fun, params, sil_loc, Sil.cf_default) in let res_trans_call = { empty_res_trans with - ids = [ret_id]; instrs = [call_instr]; exps = [(ret_exp, typ)]; } in let all_res_trans = res_trans_subexpr_list @ [res_trans_call] in @@ -2638,7 +2610,6 @@ struct { empty_res_trans with root_nodes = res_trans_tail.root_nodes; leaf_nodes = []; - ids = res_trans_s.ids @ res_trans_tail.ids; instrs = res_trans_tail.instrs @ res_trans_s.instrs; exps = res_trans_tail.exps @ res_trans_s.exps; initd_exps = res_trans_tail.initd_exps @ res_trans_s.initd_exps; diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 964043d63..351a6d23f 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -52,11 +52,11 @@ struct | Cfg.Node.Prune_node(true, _, _) -> true | _ -> false - let create_node node_kind temps instrs loc context = + let create_node node_kind instrs loc context = let procdesc = CContext.get_procdesc context in - Cfg.Node.create (CContext.get_cfg context) loc node_kind instrs procdesc temps + Cfg.Node.create (CContext.get_cfg context) loc node_kind instrs procdesc - let create_prune_node branch e_cond ids_cond instrs_cond loc ik context = + let create_prune_node branch e_cond instrs_cond loc ik context = let (e_cond', _) = extract_exp_from_list e_cond "\nWARNING: Missing expression for Conditional operator. Need to be fixed" in let e_cond'' = @@ -65,7 +65,7 @@ struct else Sil.BinOp(Sil.Eq, e_cond', Sil.exp_zero) in let instrs_cond'= instrs_cond @ [Sil.Prune(e_cond'', loc, branch, ik)] in - create_node (prune_kind branch) ids_cond instrs_cond' loc context + create_node (prune_kind branch) instrs_cond' loc context (** Check if this binary opertor requires the creation of a node in the cfg. *) let is_binary_assign_op boi = @@ -92,7 +92,7 @@ struct Hashtbl.find context.CContext.label_map label with Not_found -> let node_name = Format.sprintf "GotoLabel_%s" label in - let new_node = Nodes.create_node (Cfg.Node.Skip_node node_name) [] [] sil_loc context in + let new_node = Nodes.create_node (Cfg.Node.Skip_node node_name) [] sil_loc context in Hashtbl.add context.CContext.label_map label new_node; new_node end @@ -139,7 +139,6 @@ type trans_state = { type trans_result = { root_nodes: Cfg.Node.t list; (* Top cfg nodes (root) created by the translation *) leaf_nodes: Cfg.Node.t list; (* Bottom cfg nodes (leaf) created by the translate *) - ids: Ident.t list; (* list of temp identifiers created that need to be removed by the caller *) instrs: Sil.instr list; (* list of SIL instruction that need to be placed in cfg nodes of the parent*) exps: (Sil.exp * Sil.typ) list; (* SIL expressions resulting from the translation of the clang stmt *) initd_exps: Sil.exp list; @@ -150,7 +149,6 @@ type trans_result = { let empty_res_trans = { root_nodes = []; leaf_nodes = []; - ids = []; instrs = []; exps = []; initd_exps = []; @@ -174,7 +172,6 @@ let collect_res_trans cfg l = collect l' { root_nodes = root_nodes; leaf_nodes = leaf_nodes; - ids = IList.rev_append rt'.ids rt.ids; instrs = IList.rev_append rt'.instrs rt.instrs; exps = IList.rev_append rt'.exps rt.exps; initd_exps = IList.rev_append rt'.initd_exps rt.initd_exps; @@ -182,7 +179,6 @@ let collect_res_trans cfg l = let rt = collect l empty_res_trans in { rt with - ids = IList.rev rt.ids; instrs = IList.rev rt.instrs; exps = IList.rev rt.exps; initd_exps = IList.rev rt.initd_exps; @@ -245,10 +241,8 @@ struct let create_node = own_priority_node trans_state.priority stmt_info && res_state.instrs <> [] in if create_node then (* We need to create a node *) - let ids_node = ids_to_node trans_state.continuation res_state.ids in - let ids_parent = ids_to_parent trans_state.continuation res_state.ids in let node_kind = Cfg.Node.Stmt_node (nd_name) in - let node = Nodes.create_node node_kind ids_node res_state.instrs loc trans_state.context in + let node = Nodes.create_node node_kind res_state.instrs loc trans_state.context in Cfg.Node.set_succs_exn cfg node trans_state.succ_nodes []; IList.iter (fun leaf -> Cfg.Node.set_succs_exn cfg leaf [node] []) res_state.leaf_nodes; (* Invariant: if root_nodes is empty then the params have not created a node.*) @@ -257,7 +251,6 @@ struct { res_state with root_nodes = root_nodes; leaf_nodes = [node]; - ids = ids_parent; instrs = []; exps = []; } @@ -314,16 +307,16 @@ let create_alloc_instrs context sil_loc function_type fname size_exp_opt procnam let args = exp :: procname_arg in let ret_id = Ident.create_fresh Ident.knormal in let stmt_call = Sil.Call([ret_id], (Sil.Const (Sil.Cfun fname)), args, sil_loc, Sil.cf_default) in - (function_type, ret_id, stmt_call, Sil.Var ret_id) + (function_type, stmt_call, Sil.Var ret_id) let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc procname_opt = let fname = if is_cf_non_null_alloc then ModelBuiltins.__objc_alloc_no_fail else ModelBuiltins.__objc_alloc in - let (function_type, ret_id, stmt_call, exp) = + let (function_type, stmt_call, exp) = create_alloc_instrs trans_state.context loc function_type fname None procname_opt in - let res_trans_tmp = { empty_res_trans with ids =[ret_id]; instrs =[stmt_call]} in + let res_trans_tmp = { empty_res_trans with instrs =[stmt_call]} in let res_trans = let nname = "Call alloc" in PriorityNode.compute_results_to_parent trans_state loc nname stmt_info [res_trans_tmp] in @@ -331,18 +324,17 @@ let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc pro let objc_new_trans trans_state loc stmt_info cls_name function_type = let fname = ModelBuiltins.__objc_alloc_no_fail in - let (alloc_ret_type, alloc_ret_id, alloc_stmt_call, _) = + let (alloc_ret_type, alloc_stmt_call, alloc_ret_exp) = create_alloc_instrs trans_state.context loc function_type fname None None in let init_ret_id = Ident.create_fresh Ident.knormal in let is_instance = true in let call_flags = { Sil.cf_default with Sil.cf_virtual = is_instance; } in let pname = General_utils.mk_procname_from_objc_method cls_name CFrontend_config.init Procname.Instance_objc_method in CMethod_trans.create_external_procdesc trans_state.context.CContext.cfg pname is_instance None; - let args = [(Sil.Var alloc_ret_id, alloc_ret_type)] in + let args = [(alloc_ret_exp, alloc_ret_type)] in let init_stmt_call = Sil.Call([init_ret_id], (Sil.Const (Sil.Cfun pname)), args, loc, call_flags) in let instrs = [alloc_stmt_call; init_stmt_call] in - let ids = [alloc_ret_id; init_ret_id] in - let res_trans_tmp = { empty_res_trans with ids = ids; instrs = instrs } in + let res_trans_tmp = { empty_res_trans with instrs = instrs } in let res_trans = let nname = "Call objC new" in PriorityNode.compute_results_to_parent trans_state loc nname stmt_info [res_trans_tmp] in @@ -366,9 +358,9 @@ let cpp_new_trans trans_state sil_loc function_type size_exp_opt = match size_exp_opt with | Some _ -> ModelBuiltins.__new_array | None -> ModelBuiltins.__new in - let (function_type, ret_id, stmt_call, exp) = + let (function_type, stmt_call, exp) = create_alloc_instrs trans_state.context sil_loc function_type fname size_exp_opt None in - { empty_res_trans with ids = [ret_id]; instrs = [stmt_call]; exps = [(exp, function_type)] } + { empty_res_trans with instrs = [stmt_call]; exps = [(exp, function_type)] } let create_cast_instrs context exp cast_from_typ cast_to_typ sil_loc = let ret_id = Ident.create_fresh Ident.knormal in @@ -378,7 +370,7 @@ let create_cast_instrs context exp cast_from_typ cast_to_typ sil_loc = let pname = ModelBuiltins.__objc_cast in let args = [(exp, cast_from_typ); (sizeof_exp, Sil.Tint Sil.IULong)] in let stmt_call = Sil.Call([ret_id], (Sil.Const (Sil.Cfun pname)), args, sil_loc, Sil.cf_default) in - (ret_id, stmt_call, Sil.Var ret_id) + (stmt_call, Sil.Var ret_id) let cast_trans context exps sil_loc callee_pname_opt function_type = if CTrans_models.is_toll_free_bridging callee_pname_opt then @@ -399,17 +391,16 @@ let builtin_trans trans_state loc stmt_info function_type callee_pname_opt = let dereference_var_sil (exp, typ) sil_loc = let id = Ident.create_fresh Ident.knormal in let sil_instr = Sil.Letderef (id, exp, typ, sil_loc) in - ([id], [sil_instr], Sil.Var id) + ([sil_instr], Sil.Var id) (** Given trans_result with ONE expression, create temporary variable with *) (** value of an expression assigned to it *) let dereference_value_from_result sil_loc trans_result ~strip_pointer = let (obj_sil, class_typ) = extract_exp_from_list trans_result.exps "" in - let cast_ids, cast_inst, cast_exp = dereference_var_sil (obj_sil, class_typ) sil_loc in + let cast_inst, cast_exp = dereference_var_sil (obj_sil, class_typ) sil_loc in let typ_no_ptr = match class_typ with | Sil.Tptr (typ, _) -> typ | _ -> assert false in let cast_typ = if strip_pointer then typ_no_ptr else class_typ in { trans_result with - ids = trans_result.ids @ cast_ids; instrs = trans_result.instrs @ cast_inst; exps = [(cast_exp, cast_typ)] } @@ -421,12 +412,12 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged = match cast_kind with | `DerivedToBase | `UncheckedDerivedToBase -> (* These casts ignore change of type *) - ([], [], (exp, typ)) + ([], (exp, typ)) | `NoOp | `BitCast | `IntegralCast | `IntegralToBoolean -> (* This is treated as a nop by returning the same expressions exps*) - ([], [], (exp, cast_typ)) + ([], (exp, cast_typ)) | `CPointerToObjCPointerCast | `ARCProduceObject | `ARCConsumeObject when is_objc_bridged -> @@ -435,18 +426,18 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged = match trans_state.obj_bridged_cast_typ with | Some typ -> typ | None -> cast_typ in - let id, instr, exp = create_cast_instrs trans_state.context exp typ objc_cast_typ sil_loc in - [id], [instr], (exp, cast_typ) + let instr, exp = create_cast_instrs trans_state.context exp typ objc_cast_typ sil_loc in + [instr], (exp, cast_typ) | `LValueToRValue -> (* Takes an LValue and allow it to use it as RValue. *) (* So we assign the LValue to a temp and we pass it to the parent.*) - let ids, instrs, deref_exp = dereference_var_sil (exp, typ) sil_loc in - ids, instrs, (deref_exp, cast_typ) + let instrs, deref_exp = dereference_var_sil (exp, typ) sil_loc in + instrs, (deref_exp, cast_typ) | _ -> Printing.log_err "\nWARNING: Missing translation for Cast Kind %s. The construct has been ignored...\n" (Clang_ast_j.string_of_cast_kind cast_kind); - ([],[], (exp, cast_typ)) + ([], (exp, cast_typ)) let trans_assertion_failure sil_loc context = let assert_fail_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__infer_fail) in @@ -454,13 +445,13 @@ let trans_assertion_failure sil_loc context = let call_instr = Sil.Call ([], assert_fail_builtin, args, sil_loc, Sil.cf_default) in let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context) and failure_node = - Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [] [call_instr] sil_loc context in + Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [call_instr] sil_loc context in Cfg.Node.set_succs_exn context.CContext.cfg failure_node [exit_node] []; { empty_res_trans with root_nodes = [failure_node]; } let trans_assume_false sil_loc context succ_nodes = let instrs_cond = [Sil.Prune (Sil.exp_zero, sil_loc, true, Sil.Ik_land_lor)] in - let prune_node = Nodes.create_node (Nodes.prune_kind true) [] instrs_cond sil_loc context in + let prune_node = Nodes.create_node (Nodes.prune_kind true) instrs_cond sil_loc context in Cfg.Node.set_succs_exn context.CContext.cfg prune_node succ_nodes []; { empty_res_trans with root_nodes = [prune_node]; leaf_nodes = [prune_node] } @@ -549,16 +540,15 @@ struct let add_self_parameter_for_super_instance context procname loc mei = if is_superinstance mei then - let typ, self_expr, id, ins = + let typ, self_expr, ins = let t' = CTypes.add_pointer_to_typ (CTypes_decl.get_type_curr_class_objc context.CContext.tenv context.CContext.curr_class) in let e = Sil.Lvar (Pvar.mk (Mangled.from_string CFrontend_config.self) procname) in let id = Ident.create_fresh Ident.knormal in - t', Sil.Var id, [id], [Sil.Letderef (id, e, t', loc)] in + t', Sil.Var id, [Sil.Letderef (id, e, t', loc)] in { empty_res_trans with exps = [(self_expr, typ)]; - ids = id; instrs = ins } else empty_res_trans diff --git a/infer/src/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli index f5349a74f..91574c16d 100644 --- a/infer/src/clang/cTrans_utils.mli +++ b/infer/src/clang/cTrans_utils.mli @@ -34,7 +34,6 @@ type trans_state = { type trans_result = { root_nodes: Cfg.Node.t list; leaf_nodes: Cfg.Node.t list; - ids: Ident.t list; instrs: Sil.instr list; exps: (Sil.exp * Sil.typ) list; initd_exps: Sil.exp list; @@ -83,7 +82,7 @@ val dereference_value_from_result : Location.t -> trans_result -> strip_pointer: val cast_operation : trans_state -> Clang_ast_t.cast_kind -> (Sil.exp * Sil.typ) list -> Sil.typ -> Location.t -> - bool -> Ident.t list * Sil.instr list * (Sil.exp * Sil.typ) + bool -> Sil.instr list * (Sil.exp * Sil.typ) val trans_assertion: Location.t -> CContext.t -> Cfg.Node.t list -> trans_result @@ -111,9 +110,9 @@ val cpp_new_trans : trans_state -> Location.t -> Sil.typ -> Sil.exp option -> tr val cast_trans : CContext.t -> (Sil.exp * Sil.typ) list -> Location.t -> Procname.t option -> Sil.typ -> - (Ident.t * Sil.instr * Sil.exp) option + (Sil.instr * Sil.exp) option -val dereference_var_sil : Sil.exp * Sil.typ -> Location.t -> Ident.t list * Sil.instr list * Sil.exp +val dereference_var_sil : Sil.exp * Sil.typ -> Location.t -> Sil.instr list * Sil.exp (** Module for creating cfg nodes and other utility functions related to them. *) module Nodes : @@ -122,14 +121,13 @@ sig val need_unary_op_node : Clang_ast_t.unary_operator_info -> bool - val create_node : Cfg.Node.nodekind -> Ident.t list -> Sil.instr list -> - Location.t -> CContext.t -> Cfg.Node.t + val create_node : Cfg.Node.nodekind -> Sil.instr list -> Location.t -> CContext.t -> Cfg.Node.t val is_join_node : Cfg.Node.t -> bool val create_prune_node : - bool -> (Sil.exp * Sil.typ) list -> Ident.t list -> Sil.instr list -> Location.t -> - Sil.if_kind -> CContext.t -> Cfg.Node.t + bool -> (Sil.exp * Sil.typ) list -> Sil.instr list -> Location.t -> Sil.if_kind -> + CContext.t -> Cfg.Node.t val is_prune_node : Cfg.Node.t -> bool diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 24de032d6..1e2bba5b2 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -24,7 +24,6 @@ type lifecycle_trace = (Procname.t * Sil.typ option) list (** list of instrs and temporary variables created during inhabitation and a cache of types that * have already been inhabited *) type env = { instrs : Sil.instr list; - tmp_vars : Ident.t list; cache : Sil.exp TypMap.t; (* set of types currently being inhabited. consult to prevent infinite recursion *) cur_inhabiting : TypSet.t; @@ -46,9 +45,9 @@ let formals_from_name cfg pname = | None -> [] (** add an instruction to the env, update tmp_vars, and bump the pc *) -let env_add_instr instr tmp_vars env = +let env_add_instr instr env = let incr_pc pc = { pc with Location.line = pc.Location.line + 1 } in - { env with instrs = instr :: env.instrs; tmp_vars = tmp_vars @ env.tmp_vars; pc = incr_pc env.pc } + { env with instrs = instr :: env.instrs; pc = incr_pc env.pc } (** call flags for an allocation or call to a constructor *) let cf_alloc = Sil.cf_default @@ -77,7 +76,7 @@ let inhabit_alloc sizeof_typ ret_typ alloc_kind env = let sizeof_exp = Sil.Sizeof (sizeof_typ, Sil.Subtype.exact) in let args = [(sizeof_exp, Sil.Tptr (ret_typ, Sil.Pk_pointer))] in Sil.Call ([retval], fun_new, args, env.pc, cf_alloc) in - (inhabited_exp, env_add_instr call_instr [retval] env) + (inhabited_exp, env_add_instr call_instr env) (** find or create a Sil expression with type typ *) (* TODO: this should be done in a differnt way: just make typ a param of the harness procedure *) @@ -127,10 +126,10 @@ let rec inhabit_typ typ cfg env = Sil.Lvar (Pvar.mk typ_class_name (Procname.Java env.harness_name)) in let write_to_local_instr = Sil.Set (fresh_local_exp, ptr_to_typ, allocated_obj_exp, env.pc) in - let env' = env_add_instr write_to_local_instr [] env in + let env' = env_add_instr write_to_local_instr env in let fresh_id = Ident.create_fresh Ident.knormal in let read_from_local_instr = Sil.Letderef (fresh_id, fresh_local_exp, ptr_to_typ, env'.pc) in - (Sil.Var fresh_id, env_add_instr read_from_local_instr [fresh_id] env') + (Sil.Var fresh_id, env_add_instr read_from_local_instr env') | Sil.Tint (_) -> (Sil.Const (Sil.Cint (Sil.Int.zero)), env) | Sil.Tfloat (_) -> (Sil.Const (Sil.Cfloat 0.0), env) | typ -> @@ -160,7 +159,7 @@ and inhabit_constructor constr_name (allocated_obj, obj_type) cfg env = let constr_instr = let fun_exp = fun_exp_from_name constr_name in Sil.Call ([], fun_exp, (allocated_obj, obj_type) :: args, env.pc, Sil.cf_default) in - env_add_instr constr_instr [] env + env_add_instr constr_instr env with Not_found -> env let inhabit_call_with_args procname procdesc args env = @@ -171,7 +170,7 @@ let inhabit_call_with_args procname procdesc args env = let fun_exp = fun_exp_from_name procname in let flags = { Sil.cf_default with Sil.cf_virtual = not (Procname.java_is_static procname); } in Sil.Call (retval, fun_exp, args, env.pc, flags) in - env_add_instr call_instr retval env + env_add_instr call_instr env (** create Sil that inhabits args to and calls proc_name *) let inhabit_call (procname, receiver) cfg env = @@ -240,9 +239,9 @@ let setup_harness_cfg harness_name env cg cfg = (* important to reverse the list or there will be scoping issues! *) let instrs = (IList.rev env.instrs) in let nodekind = Cfg.Node.Stmt_node "method_body" in - Cfg.Node.create cfg env.pc nodekind instrs procdesc env.tmp_vars in + Cfg.Node.create cfg env.pc nodekind instrs procdesc in let (start_node, exit_node) = - let create_node kind = Cfg.Node.create cfg env.pc kind [] procdesc [] in + let create_node kind = Cfg.Node.create cfg env.pc kind [] procdesc in let start_kind = Cfg.Node.Start_node procdesc in let exit_kind = Cfg.Node.Exit_node procdesc in (create_node start_kind, create_node exit_kind) in @@ -263,7 +262,6 @@ let inhabit_trace trace harness_name cg cfg = let empty_env = let pc = { Location.line = start_line; col = 1; file = source_file; nLOC = 0; } in { instrs = []; - tmp_vars = []; cache = TypMap.empty; pc = pc; cur_inhabiting = TypSet.empty; diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 852d1d5b5..88c1550af 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -298,9 +298,9 @@ let create_local_procdesc program linereader cfg tenv node m = } in Cfg.Procdesc.create cfg proc_attributes 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_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.Procdesc.set_start_node procdesc start_node; Cfg.Procdesc.set_exit_node procdesc exit_node @@ -346,11 +346,11 @@ let create_local_procdesc program linereader cfg tenv node m = } in Cfg.Procdesc.create cfg proc_attributes 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_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_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; Cfg.Procdesc.set_start_node procdesc start_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 fresh_id = Ident.create_fresh Ident.knormal in - let deref = Sil.Letderef (fresh_id, exp, typ, loc) in - fresh_id, deref + Sil.Letderef (fresh_id, exp, typ, loc) (** translate an expression used as an r-value *) let rec expression context pc expr = @@ -418,7 +417,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, type_of_expr) in + ([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 @@ -431,27 +430,27 @@ let rec expression context pc expr = let procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in let pvar = Pvar.mk varname procname in trans_var pvar - | _ -> ([], [], Sil.Const (get_constant c), type_of_expr) + | _ -> ([], 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 (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), type_of_expr) + | JBir.Neg _ -> (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 | Sil.Tptr (typ, _) -> typ | _ -> 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 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, type_of_expr) + (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, type_of_expr) + (instrs, cast_ex, type_of_expr) | JBir.InstanceOf ot | JBir.Cast ot -> let subtypes = (match unop with @@ -469,42 +468,41 @@ 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, type_of_expr) + (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 (instrs1, sil_ex1, _) = expression context pc ex1 + and (instrs2, sil_ex2, _) = expression context pc ex2 in begin match binop with | JBir.ArrayLoad _ -> (* add an instruction that dereferences the array *) 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 letderef_instr = 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, type_of_expr + 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, type_of_expr) + ((instrs1 @ instrs2), sil_expr, type_of_expr) end | 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 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, type_of_expr) + (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 let var_name = Pvar.mk_global classname 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 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 @@ -516,21 +514,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 - let idl', instrs', expr' = + let instrs', expr' = JTransStaticField.translate_instr_static_field context callee_procdesc fs field_type loc in - idl', instrs', expr', type_of_expr + 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, type_of_expr) + (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, 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 = (* 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 let init = match sil_obj_opt with - | None -> ([], [], []) + | None -> [], [] | Some (sil_obj_expr, sil_obj_type) -> (* for non-constructors, add an instruction that dereferences the receiver *) - let ids, instrs = + let instrs = let is_non_constructor_call = match invoke_code with | 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 | Sil.Tptr (typ, _) -> typ | _ -> sil_obj_type in - let fresh_id, deref = create_sil_deref sil_obj_expr obj_typ_no_ptr loc in - [fresh_id], [deref] - | _ -> [], [] in - (ids, instrs, [(sil_obj_expr, sil_obj_type)]) in - let (idl, instrs, call_args) = + [create_sil_deref sil_obj_expr obj_typ_no_ptr loc] + | _ -> [] in + (instrs, [(sil_obj_expr, sil_obj_type)]) in + let (instrs, call_args) = IList.fold_left - (fun (idl_accu, instrs_accu, args_accu) expr -> - 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)])) + (fun (instrs_accu, args_accu) expr -> + let (instrs, sil_expr, sil_expr_type) = expression context pc expr in + (instrs_accu @ instrs, args_accu @ [(sil_expr, sil_expr_type)])) init expr_list in 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 then proc 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 return_type = 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 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 - (idl @ [ret_id], instrs @ [call_instr; set_instr]) in + (instrs @ [call_instr; set_instr]) in match var_opt with | None -> let call_instr = Sil.Call ([], callee_fun, call_args, loc, call_flags) in - (idl, instrs @ [call_instr]) + instrs @ [call_instr] | Some var -> 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 = match call_args with (* 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 - (callee_procname, call_idl, instrs) + (callee_procname, instrs) 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 (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 - let (idl, instrs, sil_size_exprs) = (IList.fold_right get_expr_instr expr_list ([],[],[])) in + | (other_instrs, other_exprs) -> + (instrs@other_instrs, sil_size_expr:: other_exprs) in + let (instrs, sil_size_exprs) = (IList.fold_right get_expr_instr expr_list ([],[])) in let get_array_type sil_size_expr content_type = 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_size = Sil.Sizeof (array_type, Sil.Subtype.exact) in - (idl, instrs, array_size) + (instrs, array_size) module Int = 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 loc = get_location (JContext.get_impl context) pc meth_kind cn 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 (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 () = 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) JTransType.never_returning_null in 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 instr = Sil.Call ([], builtin_const, [(sil_expr, sil_type)], loc, Sil.cf_default) 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 match instr with | 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 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 = create_node node_kind idl (stml @ [sil_instr]) in + let node = create_node node_kind (stml @ [sil_instr]) in Instr node | JBir.Return expr_option -> let node_kind = Cfg.Node.Stmt_node "method_body" in let node = match expr_option with | None -> - create_node node_kind [] [] + create_node node_kind [] | 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 return_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_expr, loc) in if return_not_null () then [assume_not_null loc sil_expr; return_instr] else [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; Instr node | JBir.AffectArray (array_ex, index_ex, value_ex) -> - 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 (instrs_array, sil_expr_array, arr_type) = expression context pc array_ex + and (instrs_index, sil_expr_index, _) = expression context pc index_ex + 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 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 - and final_instrs = instrs_array @ instrs_index @ instrs_value @ [sil_instr] in + let final_instrs = instrs_array @ instrs_index @ instrs_value @ [sil_instr] 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 | 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 (stml1, sil_expr_lhs, _) = expression context pc e_lhs 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 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 = 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 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 | JBir.AffectStaticField (cn, fs, e_rhs) -> let class_exp = let classname = Mangled.from_string (JBasics.cn_name cn) in let var_name = Pvar.mk_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 (stml1, sil_expr_lhs) = [], class_exp 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 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 = 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 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 | JBir.Goto goto_pc -> JContext.reset_pvar_type context; @@ -871,8 +871,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 (instrs1, sil_ex1, _) = expression context pc e1 + and (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,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 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 prune_node_true = create_node node_kind_true (idl1 @ idl2) (instrs1 @ instrs2 @ [sil_instrs_true]) - and prune_node_false = create_node node_kind_false (idl1 @ idl2) (instrs1 @ instrs2 @ [sil_instrs_false]) in + let prune_node_true = create_node node_kind_true (instrs1 @ instrs2 @ [sil_instrs_true]) + 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; if detect_loop pc (JContext.get_impl context) then 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) else Prune (prune_node_true, prune_node_false) | 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_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; Instr node | 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 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_procname, call_ids, call_instrs = + let constr_procname, call_instrs = let ret_opt = Some (Sil.Var ret_id, class_type) in method_invocation 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 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 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 Cg.add_edge cg caller_procname constr_procname; Instr node @@ -923,40 +923,40 @@ let rec instruction context pc instr : translation = 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_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 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 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 = 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 | JBir.InvokeStatic (var_opt, cn, ms, args) -> - let sil_obj_opt, args, ids, instrs = + let sil_obj_opt, args, instrs = match args with | [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, 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 = + let (instrs, sil_arg_expr, arg_typ) = expression context pc arg in + Some (sil_arg_expr, arg_typ), [], instrs + | _ -> None, args, [] in + let callee_procname, call_instrs = 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 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 Cg.add_edge cg caller_procname callee_procname; 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 (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 callee_procname, call_ids, call_instrs = + let callee_procname, call_instrs = let ret_opt = Some (sil_obj_expr, sil_obj_type) in method_invocation 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 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; call_node in 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 end | JBir.InvokeNonVirtual (var_opt, obj, cn, ms, args) -> - let (ids, instrs, sil_obj_expr, sil_obj_type) = expression context pc obj in - let callee_procname, call_ids, call_instrs = + let (instrs, sil_obj_expr, sil_obj_type) = expression context pc obj in + 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 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 caller_procname = (Cfg.Procdesc.get_proc_name procdesc) in 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 -> (* 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 = 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 | 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 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) 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 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) @@ -1019,27 +1019,26 @@ let rec instruction context pc instr : translation = 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 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 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 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 - create_node npe_kind (ids @ call_ids) npe_instrs in + create_node npe_kind npe_instrs in Prune (not_null_node, throw_npe_node) | 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 instrs, _, sil_length_expr, sil_index_expr = + let array_instrs, sil_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)) - and index_ids, index_instrs, sil_index_expr, _ = + and 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 - (ids, instrs, sil_array_expr, sil_length_expr, sil_index_expr) in + let instrs = array_instrs @ index_instrs @ length_instrs in + (instrs, sil_array_expr, sil_length_expr, sil_index_expr) in let in_bound_node = 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.LAnd, sil_positive_index, sil_less_than_length) 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 = 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 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 _, call_ids, call_instrs = + let _, call_instrs = method_invocation context loc pc None out_of_bound_cn constr_ms (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 out_of_bound_instrs = 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) | 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 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 @@ -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 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 - 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 = 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) @@ -1112,14 +1111,14 @@ let rec instruction context pc instr : translation = 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 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 (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 set_instr = Sil.Set (Sil.Lvar ret_var, ret_type, sil_exn, loc) in let cce_instrs = 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) | JBir.MonitorEnter expr -> diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index 6c5aef3bf..356535377 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -31,7 +31,7 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table = let exn_message = "exception handler" in let procdesc = JContext.get_procdesc context in let cfg = JContext.get_cfg context in - let create_node loc node_kind instrs temps = Cfg.Node.create cfg loc node_kind instrs procdesc temps in + let create_node loc node_kind instrs = Cfg.Node.create cfg loc node_kind instrs procdesc in let ret_var = Cfg.Procdesc.get_ret_var procdesc in let ret_type = Cfg.Procdesc.get_ret_type procdesc in let id_ret_val = Ident.create_fresh Ident.knormal in @@ -43,12 +43,15 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table = let instr_unwrap_ret_val = let unwrap_builtin = Sil.Const (Sil.Cfun ModelBuiltins.__unwrap_exception) in Sil.Call([id_exn_val], unwrap_builtin, [(Sil.Var id_ret_val, ret_type)], loc, Sil.cf_default) in - create_node loc Cfg.Node.exn_handler_kind [instr_get_ret_val; instr_deactivate_exn; instr_unwrap_ret_val] [id_ret_val; id_deactivate] in + create_node + loc + Cfg.Node.exn_handler_kind + [instr_get_ret_val; instr_deactivate_exn; instr_unwrap_ret_val] in let create_entry_block handler_list = try ignore (Hashtbl.find catch_block_table handler_list) with Not_found -> - let collect succ_nodes last_handler rethrow_exception handler = + let collect succ_nodes rethrow_exception handler = let catch_nodes = get_body_nodes handler.JBir.e_handler in let loc = match catch_nodes with | n:: _ -> Cfg.Node.get_loc n @@ -77,12 +80,10 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table = let node_kind_false = Cfg.Node.Prune_node (false, if_kind, exn_message) in let node_true = let instrs_true = [instr_call_instanceof; instr_prune_true; instr_set_catch_var] in - let ids_true = [id_exn_val; id_instanceof] in - create_node loc node_kind_true instrs_true ids_true in + create_node loc node_kind_true instrs_true in let node_false = let instrs_false = [instr_call_instanceof; instr_prune_false] @ (if rethrow_exception then [instr_rethrow_exn] else []) in - let ids_false = (if last_handler then [id_exn_val] else []) @ [id_instanceof] in - create_node loc node_kind_false instrs_false ids_false in + create_node loc node_kind_false instrs_false in Cfg.Node.set_succs_exn cfg node_true catch_nodes exit_nodes; Cfg.Node.set_succs_exn cfg node_false succ_nodes exit_nodes; let is_finally = handler.JBir.e_catch_type = None in @@ -91,11 +92,9 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table = else [node_true; node_false] in let is_last_handler = ref true in let process_handler succ_nodes handler = (* process handlers starting from the last one *) - let is_finally_handler = handler.JBir.e_catch_type = None in let remove_temps = !is_last_handler in (* remove temporary variables on last handler *) - let rethrow_exception = !is_last_handler && not is_finally_handler in (* rethrow exception if there is no finally *) is_last_handler := false; - collect succ_nodes remove_temps rethrow_exception handler in + collect succ_nodes remove_temps handler in let nodes_first_handler = IList.fold_left process_handler exit_nodes (IList.rev handler_list) in diff --git a/infer/src/java/jTransStaticField.ml b/infer/src/java/jTransStaticField.ml index ee161770b..5810f85cd 100644 --- a/infer/src/java/jTransStaticField.ml +++ b/infer/src/java/jTransStaticField.ml @@ -189,7 +189,7 @@ let translate_instr_static_field context callee_procdesc fs field_type loc = let field_arg = Sil.Const (Sil.Cstr (JBasics.fs_name fs)) in let call_instr = Sil.Call([ret_id], callee_fun, [field_arg, field_type], loc, Sil.cf_default) in Cg.add_edge cg caller_procname callee_procname; - ([ret_id], [call_instr], Sil.Var ret_id) + ([call_instr], Sil.Var ret_id) let is_static_final_field context cn fs = diff --git a/infer/src/java/jTransStaticField.mli b/infer/src/java/jTransStaticField.mli index 7f31d663d..c577237aa 100644 --- a/infer/src/java/jTransStaticField.mli +++ b/infer/src/java/jTransStaticField.mli @@ -19,7 +19,7 @@ val is_static_final_field : JContext.t -> JBasics.class_name -> JBasics.field_si val has_static_final_fields : JCode.jcode Javalib.interface_or_class -> bool val translate_instr_static_field : JContext.t -> Cfg.Procdesc.t -> JBasics.field_signature -> Sil.typ -> - Location.t -> Ident.t list * Sil.instr list * Sil.exp + Location.t -> Sil.instr list * Sil.exp val static_field_init : JCode.jcode Javalib.interface_or_class -> JBasics.class_name -> JBir.instr array -> JBir.instr array diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index 62ed62b71..f457561c4 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -140,12 +140,12 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map) } in let procdesc = Cfg.Procdesc.create cfg proc_attrs in let start_kind = Cfg.Node.Start_node procdesc in - let start_node = Cfg.Node.create cfg (source_only_location ()) start_kind [] procdesc [] in + let start_node = Cfg.Node.create cfg (source_only_location ()) start_kind [] procdesc in let exit_kind = Cfg.Node.Exit_node procdesc in - let exit_node = Cfg.Node.create cfg (source_only_location ()) exit_kind [] procdesc [] in + let exit_node = Cfg.Node.create cfg (source_only_location ()) exit_kind [] procdesc in let node_of_sil_instr cfg procdesc sil_instr = Cfg.Node.create cfg (Sil.instr_get_loc sil_instr) (Cfg.Node.Stmt_node "method_body") - [sil_instr] procdesc [] in + [sil_instr] procdesc in let rec link_nodes (start_node : Cfg.Node.t) : Cfg.Node.t list -> unit = function (* link all nodes in a chain for now *) | [] -> diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 65ce0b46f..cbae176aa 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -158,8 +158,7 @@ module Make Cfg.Procdesc.create cfg (ProcAttributes.default dummy_procname !Config.curr_language) in let create_node kind cmds = - let no_tmp_idents = [] in - Cfg.Node.create cfg dummy_loc kind cmds pdesc no_tmp_idents in + Cfg.Node.create cfg dummy_loc kind cmds pdesc in let set_succs cur_node succs ~exn_handlers= Cfg.Node.set_succs_exn cfg cur_node succs exn_handlers in let mk_prune_nodes_for_cond cond_exp if_kind = diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml index 2de89c123..0e5b016ee 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/infer/src/unit/procCfgTests.ml @@ -25,7 +25,7 @@ let tests = let instrs3 = [] in let instrs4 = [] in let create_node cfg instrs = - Cfg.Node.create cfg Location.dummy (Cfg.Node.Stmt_node "") instrs test_pdesc [] in + Cfg.Node.create cfg Location.dummy (Cfg.Node.Stmt_node "") instrs test_pdesc in let n1 = create_node cfg instrs1 in let n2 = create_node cfg instrs2 in let n3 = create_node cfg instrs3 in