From ab1ac822f67aa91754841db49e437c3749506193 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 16 Mar 2016 17:26:32 -0700 Subject: [PATCH] Replacing Ctuple with Cclosure Reviewed By: cristianoc Differential Revision: D3039653 fb-gh-sync-id: a3e9c2e shipit-source-id: a3e9c2e --- infer/src/backend/preanal.ml | 16 +++--------- infer/src/backend/prop.ml | 2 -- infer/src/backend/sil.ml | 42 +++++++++++++++++++++---------- infer/src/backend/sil.mli | 8 +++++- infer/src/backend/symExec.ml | 36 ++++---------------------- infer/src/clang/cTrans.ml | 49 ++++++++++++++++++++---------------- 6 files changed, 73 insertions(+), 80 deletions(-) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index e80ea74b5..980921ff7 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -67,18 +67,10 @@ let is_captured_pvar pdesc x = let rec use_exp cfg pdesc (exp: Sil.exp) acc = match exp with | Sil.Var _ | Sil.Sizeof _ -> acc - | Sil.Const (Sil.Ctuple((Sil.Const (Sil.Cfun pname)):: _)) -> - (* for tuples representing the assignment of a block we take the block name *) - (* look for its procdesc and add its captured vars to the set of captured vars. *) - let found_pd = ref None in - Cfg.iter_proc_desc cfg (fun pn pd -> if Procname.equal pn pname then found_pd:= Some pd); - let defining_proc = Cfg.Procdesc.get_proc_name pdesc in - (match !found_pd with - | Some pd -> - IList.iter (fun (x, _) -> - captured_var:= Vset.add (Sil.mk_pvar x defining_proc) !captured_var - ) (Cfg.Procdesc.get_captured pd) - | _ -> ()); + | Sil.Const (Cclosure { captured_vars }) -> + IList.iter + (fun (_, captured_pvar, _) -> captured_var:= Vset.add captured_pvar !captured_var) + captured_vars; acc | Sil.Const _ -> acc | Sil.Lvar x -> diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index f381e9022..2958443a9 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -434,8 +434,6 @@ let sym_eval abs e = match e with | Sil.Var _ -> e - | Sil.Const (Sil.Ctuple el) -> - Sil.Const (Sil.Ctuple (IList.map eval el)) | Sil.Const _ -> e | Sil.Sizeof (Sil.Tarray (Sil.Tint ik, e), _) diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index a32898602..f7e6b8b22 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -645,6 +645,11 @@ and attribute_category = | ACretval | ACobserver +and closure = { + name : Procname.t; + captured_vars : (Ident.t * pvar * typ) list; +} + (** Constants *) and const = | Cint of Int.t (** integer constants *) @@ -656,7 +661,7 @@ and const = | Cclass of Ident.name (** class constant *) | Cptr_to_fld of Ident.fieldname * typ (** pointer to field constant, and type of the surrounding Csu.t type *) - | Ctuple of exp list (** tuple of values *) + | Cclosure of closure (** anonymous function *) and struct_fields = (Ident.fieldname * typ * item_annotation) list @@ -1297,7 +1302,7 @@ let const_kind_equal c1 c2 = | Cexn _ -> 6 | Cclass _ -> 7 | Cptr_to_fld _ -> 8 - | Ctuple _ -> 9 in + | Cclosure _ -> 9 in const_kind_number c1 = const_kind_number c2 let rec const_compare (c1 : const) (c2 : const) : int = @@ -1328,7 +1333,18 @@ let rec const_compare (c1 : const) (c2 : const) : int = if n <> 0 then n else typ_compare t1 t2 | Cptr_to_fld _, _ -> -1 | _, Cptr_to_fld _ -> 1 - | Ctuple el1, Ctuple el2 -> IList.compare exp_compare el1 el2 + | Cclosure { name=n1; captured_vars=c1; }, Cclosure { name=n2; captured_vars=c2; } -> + let captured_var_compare acc (id1, pvar1, typ1) (id2, pvar2, typ2) = + if acc <> 0 then acc + else + let n = Ident.compare id1 id2 in + if n <> 0 then n + else + let n = pvar_compare pvar1 pvar2 in + if n <> 0 then n + else typ_compare typ1 typ2 in + let n = Procname.compare n1 n2 in + if n <> 0 then n else IList.fold_left2 captured_var_compare 0 c1 c2 and struct_typ_compare struct_typ1 struct_typ2 = if struct_typ1.csu = Csu.Class Csu.Java && struct_typ2.csu = Csu.Class Csu.Java then @@ -1999,7 +2015,9 @@ and pp_const pe f = function | Cexn e -> F.fprintf f "EXN %a" (pp_exp pe) e | Cclass c -> F.fprintf f "%a" Ident.pp_name c | Cptr_to_fld (fn, _) -> F.fprintf f "__fld_%a" Ident.pp_fieldname fn - | Ctuple el -> F.fprintf f "(%a)" (pp_comma_seq (pp_exp pe)) el + | Cclosure { name; captured_vars; } -> + let id_exps = IList.map (fun (id, _, _) -> Var id) captured_vars in + F.fprintf f "(%a)" (pp_comma_seq (pp_exp pe)) ((Const (Cfun name)) :: id_exps) (** Pretty print a type. Do nothing by default. *) and pp_typ pe f te = @@ -2276,8 +2294,8 @@ and exp_iter_types f e = | Var _ -> () | Const (Cexn e1) -> exp_iter_types f e1 - | Const (Ctuple el) -> - IList.iter (exp_iter_types f) el + | Const (Cclosure { captured_vars }) -> + IList.iter (fun (_, _, typ) -> f typ) captured_vars | Const _ -> () | Cast (t, e1) -> @@ -2951,7 +2969,7 @@ let exp_lt e1 e2 = let rec exp_fpv = function | Var _ -> [] | Const (Cexn e) -> exp_fpv e - | Const (Ctuple el) -> exp_list_fpv el + | Const (Cclosure _) -> [] | Const _ -> [] | Cast (_, e) | UnOp (_, e, _) -> exp_fpv e | BinOp (_, e1, e2) -> exp_fpv e1 @ exp_fpv e2 @@ -3113,8 +3131,8 @@ let fav_mem fav id = let rec exp_fav_add fav = function | Var id -> fav ++ id | Const (Cexn e) -> exp_fav_add fav e - | Const (Ctuple el) -> IList.iter (exp_fav_add fav) el - | Const _ -> () + | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _ + | Cclosure _) -> () | Cast (_, e) | UnOp (_, e, _) -> exp_fav_add fav e | BinOp (_, e1, e2) -> exp_fav_add fav e1; exp_fav_add fav e2 | Lvar _ -> () (* do nothing since we only count non-program variables *) @@ -3414,10 +3432,8 @@ and exp_sub (subst: subst) e = | Const (Cexn e1) -> let e1' = exp_sub subst e1 in Const (Cexn e1') - | Const (Ctuple el) -> - let el' = IList.map (exp_sub subst) el in - Const (Ctuple el') - | Const _ -> + | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _ + | Cclosure _) -> e | Cast (t, e1) -> let e1' = exp_sub subst e1 in diff --git a/infer/src/backend/sil.mli b/infer/src/backend/sil.mli index 59e35cca6..e875c8505 100644 --- a/infer/src/backend/sil.mli +++ b/infer/src/backend/sil.mli @@ -281,6 +281,12 @@ and attribute_category = | ACretval | ACobserver + +and closure = { + name : Procname.t; + captured_vars : (Ident.t * pvar * typ) list; +} + (** Constants *) and const = | Cint of Int.t (** integer constants *) @@ -292,7 +298,7 @@ and const = | Cclass of Ident.name (** class constant *) | Cptr_to_fld of Ident.fieldname * typ (** pointer to field constant, and type of the surrounding Csu.t type *) - | Ctuple of exp list (** tuple of values *) + | Cclosure of closure (** anonymous function *) and struct_fields = (Ident.fieldname * typ * item_annotation) list diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 1b2ff89e4..effdffd49 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1006,10 +1006,11 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path | Sil.Call (ret, exp, par, loc, call_flags) -> let exp' = Prop.exp_normalize_prop prop_ exp in let instr' = match exp' with - | Sil.Const (Sil.Ctuple (e1 :: el)) -> (* closure: combine arguments to call *) - let e1' = Prop.exp_normalize_prop prop_ e1 in - let par' = IList.map (fun e -> (e, Sil.Tvoid)) el in - Sil.Call (ret, e1', par' @ par, loc, call_flags) + | Sil.Const (Sil.Cclosure c) -> + let proc_exp = Sil.Const (Sil.Cfun c.name) in + let proc_exp' = Prop.exp_normalize_prop prop_ proc_exp in + let par' = IList.map (fun (id, _, typ) -> (Sil.Var id, typ)) c.captured_vars in + Sil.Call (ret, proc_exp', par' @ par, loc, call_flags) | _ -> Sil.Call (ret, exp', par, loc, call_flags) in instr' @@ -2565,27 +2566,6 @@ module ModelBuiltins = struct | _ -> [(prop, path)]) | _ -> raise (Exceptions.Wrong_argument_number __POS__) - let execute___create_tuple { Builtin.prop_; path; ret_ids; args; } - : Builtin.ret_typ = - let el = IList.map fst args in - let res = Sil.Const (Sil.Ctuple el) in - [(return_result res prop_ ret_ids, path)] - - let execute___tuple_get_nth { Builtin.pdesc; prop_; path; ret_ids; args; } - : Builtin.ret_typ = - match args with - | [(lexp1, _); (lexp2, _)] -> - let pname = Cfg.Procdesc.get_proc_name pdesc in - let n_lexp1, prop__ = exp_norm_check_arith pname prop_ lexp1 in - let n_lexp2, prop = exp_norm_check_arith pname prop__ lexp2 in - (match n_lexp1, n_lexp2 with - | Sil.Const (Sil.Ctuple el), Sil.Const (Sil.Cint i) -> - let n = Sil.Int.to_int i in - let en = IList.nth el n in - [(return_result en prop ret_ids, path)] - | _ -> [(prop, path)]) - | _ -> raise (Exceptions.Wrong_argument_number __POS__) - (* forces the expression passed as parameter to be assumed true at the point where this builtin is called, diverges if this causes an inconsistency *) let execute___infer_assume { Builtin.prop_; path; args; } @@ -2646,9 +2626,6 @@ module ModelBuiltins = struct let _ = Builtin.register (* report a taint error if the parameter is tainted, and assume it is untainted afterward *) "__check_untainted" execute___check_untainted - let __create_tuple = Builtin.register - (* create a tuple value from the arguments *) - "__create_tuple" execute___create_tuple let __delete = Builtin.register (* like free *) "__delete" (execute_free Sil.Mnew) @@ -2764,9 +2741,6 @@ module ModelBuiltins = struct "__set_unlocked_attribute" execute___set_unlocked_attribute let _ = Builtin.register "__throw" execute_skip - let __tuple_get_nth = Builtin.register - (* return the nth element of a tuple *) - "__tuple_get_nth" execute___tuple_get_nth let __unwrap_exception = Builtin.register (* unwrap an exception *) "__unwrap_exception" execute__unwrap_exception diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index b3f678982..74bc6ff72 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -160,23 +160,25 @@ struct let extract_block_from_tuple procname exps loc = let insts = ref [] in let ids = ref [] in - let is_function_name t e = - match e with - | Sil.Const (Sil.Cfun bn) -> - let bn'= Procname.to_string bn in - let bn''= Mangled.from_string bn' in - let block = Sil.Lvar (Sil.mk_pvar bn'' procname) in - let id = Ident.create_fresh Ident.knormal in - ids := id :: !ids; - insts := Sil.Letderef (id, block, t, loc) :: !insts; - [(Sil.Var id, t)] - | _ -> [(e, t)] in - let get_function_name t el = IList.flatten(IList.map (is_function_name t) el) 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 (Sil.mk_pvar 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, _, _) = (Sil.Var id, typ) in let rec f es = match es with | [] -> [] - | (Sil.Const(Sil.Ctuple el), (Sil.Tptr((Sil.Tfun _), _ ) as t)) :: es' -> - get_function_name t el @ (f es') + | (Sil.Const (Sil.Cclosure { name; captured_vars}), + (Sil.Tptr((Sil.Tfun _), _ ) as t)) :: es' -> + let app = + let function_name = make_function_name t name in + let args = IList.map (make_arg t) captured_vars in + function_name :: args in + app @ (f es') | e :: es' -> e :: f es' in (f exps, !insts, !ids) @@ -1898,20 +1900,25 @@ struct (* defining procedure. We add an edge in the call graph.*) Cg.add_edge context.cg procname block_pname; let captured_block_vars = block_decl_info.Clang_ast_t.bdi_captured_variables in - let captured_vars = CVar_decl.captured_vars_from_block_info context captured_block_vars in - let ids_instrs = IList.map assign_captured_var captured_vars in + let captured_pvars = CVar_decl.captured_vars_from_block_info context captured_block_vars in + let ids_instrs = IList.map assign_captured_var captured_pvars in let ids, instrs = IList.split ids_instrs in - let block_data = (context, type_ptr, block_pname, captured_vars) in + let block_data = (context, type_ptr, block_pname, captured_pvars) in F.function_decl context.tenv context.cfg context.cg decl (Some block_data); Cfg.set_procname_priority context.cfg block_pname; - let captured_exps = IList.map (fun id -> Sil.Var id) ids in - let tu = Sil.Ctuple ((Sil.Const (Sil.Cfun block_pname)) :: captured_exps) in + let captured_vars = + IList.map2 (fun id (pvar, typ) -> (id, pvar, typ)) ids captured_pvars in + let closure = Sil.Cclosure { name=block_pname; captured_vars } in 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 = captured_vars @ static_vars in + let captured_static_vars = captured_pvars @ static_vars in let alloc_block_instr, ids_block = 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 tu, typ)]} + { empty_res_trans with + ids = ids_block @ ids; + instrs = alloc_block_instr @ instrs; + exps = [(Sil.Const closure, typ)]; + } | _ -> assert false and cxxNewExpr_trans trans_state stmt_info expr_info =