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

Replacing Ctuple with Cclosure

Browse Source 
Reviewed By: cristianoc

Differential Revision: D3039653

fb-gh-sync-id: a3e9c2e
shipit-source-id: a3e9c2e
master
Sam Blackshear 9 years ago committed by Facebook Github Bot 1
parent 0b56374b11
commit ab1ac822f6
6 changed files with 73 additions and 80 deletions
Show Stats Download Patch File Download Diff File

16
infer/src/backend/preanal.ml
Unescape View File

@ -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 ->

2
infer/src/backend/prop.ml
Unescape View File

@ -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), _)

42
infer/src/backend/sil.ml
Unescape View File

@ -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

8
infer/src/backend/sil.mli
Unescape View File

@ -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

36
infer/src/backend/symExec.ml
Unescape View File

@ -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

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

@ -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 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, 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
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 =

Write Preview
Loading…
Cancel
Save