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

Closure values are not constants

Browse Source 
Summary:
Move closure values from const to exp.  They are not constants, and
this reduces interdependence between Sil types.

Reviewed By: sblackshear

Differential Revision: D3541364

fbshipit-source-id: 1a2f998
master
Josh Berdine 8 years ago committed by Facebook Github Bot 7
parent c5ce74f3d3
commit 32d09545e2
14 changed files with 66 additions and 55 deletions
Show Stats Download Patch File Download Diff File

78
infer/src/IR/Sil.re
Unescape View File

@ -473,7 +473,6 @@ and const =
| Cclass of Ident.name /** class constant */
| Cptr_to_fld of Ident.fieldname Typ.t /** pointer to field constant,
and type of the surrounding Csu.t type */
| Cclosure of closure /** anonymous function */
/** dynamically determined length of an array value, if any */
and dynamic_length = option exp
/** Program expressions. */
@ -486,6 +485,8 @@ and exp =
| BinOp of binop exp exp
/** Exception */
| Exn of exp
/** Anonymous function */
| Closure of closure
/** Constants */
| Const of const
/** Type cast */
@ -982,8 +983,7 @@ let const_kind_equal c1 c2 => {
| Cfloat _ => 4
| Cattribute _ => 5
| Cclass _ => 7
| Cptr_to_fld _ => 8
| Cclosure _ => 9;
| Cptr_to_fld _ => 8;
const_kind_number c1 == const_kind_number c2
};
@ -1085,31 +1085,6 @@ and const_compare (c1: const) (c2: const) :int =>
} else {
Typ.compare t1 t2
}
| (Cptr_to_fld _, _) => (-1)
| (_, Cptr_to_fld _) => 1
| (Cclosure {name: n1, captured_vars: c1}, Cclosure {name: n2, captured_vars: c2}) =>
let captured_var_compare acc (e1, pvar1, typ1) (e2, pvar2, typ2) =>
if (acc != 0) {
acc
} else {
let n = exp_compare e1 e2;
if (n != 0) {
n
} else {
let n = Pvar.compare pvar1 pvar2;
if (n != 0) {
n
} else {
Typ.compare typ1 typ2
}
}
};
let n = Procname.compare n1 n2;
if (n != 0) {
n
} else {
IList.fold_left2 captured_var_compare 0 c1 c2
}
}
/** Compare epressions. Variables come before other expressions. */
and exp_compare (e1: exp) (e2: exp) :int =>
@ -1148,6 +1123,31 @@ and exp_compare (e1: exp) (e2: exp) :int =>
| (Exn e1, Exn e2) => exp_compare e1 e2
| (Exn _, _) => (-1)
| (_, Exn _) => 1
| (Closure {name: n1, captured_vars: c1}, Closure {name: n2, captured_vars: c2}) =>
let captured_var_compare acc (e1, pvar1, typ1) (e2, pvar2, typ2) =>
if (acc != 0) {
acc
} else {
let n = exp_compare e1 e2;
if (n != 0) {
n
} else {
let n = Pvar.compare pvar1 pvar2;
if (n != 0) {
n
} else {
Typ.compare typ1 typ2
}
}
};
let n = Procname.compare n1 n2;
if (n != 0) {
n
} else {
IList.fold_left2 captured_var_compare 0 c1 c2
}
| (Closure _, _) => (-1)
| (_, Closure _) => 1
| (Const c1, Const c2) => const_compare c1 c2
| (Const _, _) => (-1)
| (_, Const _) => 1
@ -1764,10 +1764,6 @@ and pp_const pe f =>
| Cattribute att => F.fprintf f "%s" (attribute_to_string pe att)
| Cclass c => F.fprintf f "%a" Ident.pp_name c
| Cptr_to_fld fn _ => F.fprintf f "__fld_%a" Ident.pp_fieldname fn
| Cclosure {name, captured_vars} => {
let id_exps = IList.map (fun (id_exp, _, _) => id_exp) captured_vars;
F.fprintf f "(%a)" (pp_comma_seq (pp_exp pe)) [Const (Cfun name), ...id_exps]
}
/** Pretty print an expression. */
and _pp_exp pe0 pp_t f e0 => {
let (pe, changed) = color_pre_wrapper pe0 f e0;
@ -1803,6 +1799,9 @@ and _pp_exp pe0 pp_t f e0 => {
| BinOp op (Const c) e2 when Config.smt_output => print_binop_stm_output (Const c) op e2
| BinOp op e1 e2 => F.fprintf f "(%a %s %a)" pp_exp e1 (str_binop pe op) pp_exp e2
| Exn e => F.fprintf f "EXN %a" pp_exp e
| Closure {name, captured_vars} =>
let id_exps = IList.map (fun (id_exp, _, _) => id_exp) captured_vars;
F.fprintf f "(%a)" (pp_comma_seq pp_exp) [Const (Cfun name), ...id_exps]
| Lvar pv => Pvar.pp pe f pv
| Lfield e fld _ => F.fprintf f "%a.%a" pp_exp e Ident.pp_fieldname fld
| Lindex e1 e2 => F.fprintf f "%a[%a]" pp_exp e1 pp_exp e2
@ -2685,7 +2684,8 @@ let rec root_of_lexp lexp =>
| Cast _ e => root_of_lexp e
| UnOp _
| BinOp _
| Exn _ => lexp
| Exn _
| Closure _ => lexp
| Lvar _ => lexp
| Lfield e _ _ => root_of_lexp e
| Lindex e _ => root_of_lexp e
@ -2767,7 +2767,7 @@ let rec exp_fpv =
fun
| Var _ => []
| Exn e => exp_fpv e
| Const (Cclosure {captured_vars}) => IList.map (fun (_, pvar, _) => pvar) captured_vars
| Closure {captured_vars} => IList.map (fun (_, pvar, _) => pvar) captured_vars
| Const _ => []
| Cast _ e
| UnOp _ e _ => exp_fpv e
@ -2958,8 +2958,7 @@ let rec exp_fav_add fav =>
fun
| Var id => fav ++ id
| Exn e => exp_fav_add fav e
| Const (Cclosure {captured_vars}) =>
IList.iter (fun (e, _, _) => exp_fav_add fav e) captured_vars
| Closure {captured_vars} => IList.iter (fun (e, _, _) => exp_fav_add fav e) captured_vars
| Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _) => ()
| Cast _ e
| UnOp _ e _ => exp_fav_add fav e
@ -3364,7 +3363,7 @@ let rec exp_sub_ids (f: Ident.t => exp) exp =>
} else {
Exn e'
}
| Const (Cclosure c) =>
| Closure c =>
let captured_vars =
IList.map_changed
(
@ -3381,7 +3380,7 @@ let rec exp_sub_ids (f: Ident.t => exp) exp =>
if (captured_vars === c.captured_vars) {
exp
} else {
Const (Cclosure {...c, captured_vars})
Closure {...c, captured_vars}
}
| Const (Cattribute (Aobjc_null e)) =>
let e' = exp_sub_ids f e;
@ -4050,7 +4049,7 @@ let exp_get_vars exp => {
| Exn e => exp_get_vars_ e vars
| BinOp _ e1 e2
| Lindex e1 e2 => exp_get_vars_ e1 vars |> exp_get_vars_ e2
| Const (Cclosure {captured_vars}) =>
| Closure {captured_vars} =>
IList.fold_left
(fun vars_acc (captured_exp, _, _) => exp_get_vars_ captured_exp vars_acc)
vars
@ -4074,6 +4073,7 @@ let exp_get_offsets exp => {
| UnOp _
| BinOp _
| Exn _
| Closure _
| Lvar _
| Sizeof _ None _ => offlist_past
| Sizeof _ (Some l) _ => f offlist_past l

3
infer/src/IR/Sil.rei
Unescape View File

@ -200,7 +200,6 @@ and const =
| Cclass of Ident.name /** class constant */
| Cptr_to_fld of Ident.fieldname Typ.t /** pointer to field constant,
and type of the surrounding Csu.t type */
| Cclosure of closure /** anonymous function */
/** dynamically determined length of an array value, if any */
and dynamic_length = option exp
/** Program expressions. */
@ -213,6 +212,8 @@ and exp =
| BinOp of binop exp exp
/** Exception */
| Exn of exp
/** Anonymous function */
| Closure of closure
/** Constants */
| Const of const
/** Type cast */

1
infer/src/backend/dom.ml
Unescape View File

@ -814,6 +814,7 @@ let rec exp_construct_fresh side e =
let e2' = exp_construct_fresh side e2 in
Sil.BinOp(binop, e1', e2')
| Sil.Exn _ -> e
| Sil.Closure _ -> e
| Sil.Lvar _ ->
e
| Sil.Lfield(e1, fld, typ) ->

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

@ -70,6 +70,8 @@ let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option =
None (* Naive *)
| Sil.Exn _, _ | _, Sil.Exn _ ->
check_equal sub vars e1 e2
| Sil.Closure _, _ | _, Sil.Closure _ ->
check_equal sub vars e1 e2
| Sil.Lvar _, _ | _, Sil.Lvar _ ->
check_equal sub vars e1 e2
| Sil.Lfield(e1', fld1, _), Sil.Lfield(e2', fld2, _) when (Ident.fieldname_equal fld1 fld2) ->

3
infer/src/backend/modelBuiltins.ml
Unescape View File

@ -757,7 +757,8 @@ let execute_alloc mk can_return_null
Sil.UnOp (uop, evaluate_char_sizeof e', typ)
| Sil.BinOp (bop, e1', e2') ->
Sil.BinOp (bop, evaluate_char_sizeof e1', evaluate_char_sizeof e2')
| Sil.Exn _ | Sil.Const _ | Sil.Cast _ | Sil.Lvar _ | Sil.Lfield _ | Sil.Lindex _ -> e
| Sil.Exn _ | Sil.Closure _ | Sil.Const _ | Sil.Cast _ | Sil.Lvar _ | Sil.Lfield _
| Sil.Lindex _ -> e
| Sil.Sizeof (Typ.Tarray (Typ.Tint ik, _), Some len, _) when Typ.ikind_is_char ik ->
evaluate_char_sizeof len
| Sil.Sizeof (Typ.Tarray (Typ.Tint ik, Some len), None, _) when Typ.ikind_is_char ik ->

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

@ -450,10 +450,10 @@ let sym_eval abs e =
match e with
| Sil.Var _ ->
e
| Sil.Const (Sil.Cclosure c) ->
| Sil.Closure c ->
let captured_vars =
IList.map (fun (exp, pvar, typ) -> (eval exp, pvar, typ)) c.captured_vars in
Sil.Const (Sil.Cclosure { c with captured_vars; })
Sil.Closure { c with captured_vars; }
| Sil.Const _ ->
e
| Sil.Sizeof (Typ.Tarray (Typ.Tint ik, _), Some l, _)
@ -1978,6 +1978,7 @@ let find_arithmetic_problem proc_node_session prop exp =
if op = Sil.Div || op = Sil.Mod then exps_divided := e2 :: !exps_divided;
walk e1; walk e2
| Sil.Exn _ -> ()
| Sil.Closure _ -> ()
| Sil.Const _ -> ()
| Sil.Cast (_, e) -> walk e
| Sil.Lvar _ -> ()
@ -2264,6 +2265,7 @@ let ident_captured_ren ren id =
let rec exp_captured_ren ren = function
| Sil.Var id -> Sil.Var (ident_captured_ren ren id)
| Sil.Exn e -> Sil.Exn (exp_captured_ren ren e)
| Sil.Closure _ as e -> e (* TODO: why captured vars not renamed? *)
| Sil.Const _ as e -> e
| Sil.Sizeof (t, len, st) -> Sil.Sizeof (t, Option.map (exp_captured_ren ren) len, st)
| Sil.Cast (t, e) -> Sil.Cast (t, exp_captured_ren ren e)

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

@ -28,7 +28,7 @@ let from_prop p = p
(** Return [true] if root node *)
let rec is_root = function
| Sil.Var id -> Ident.is_normal id
| Sil.Const _ | Sil.Exn _ | Sil.Lvar _ -> true
| Sil.Exn _ | Sil.Closure _ | Sil.Const _ | Sil.Lvar _ -> true
| Sil.Cast (_, e) -> is_root e
| Sil.UnOp _ | Sil.BinOp _ | Sil.Lfield _ | Sil.Lindex _ | Sil.Sizeof _ -> false

3
infer/src/backend/prover.ml
Unescape View File

@ -551,7 +551,8 @@ let check_zero e =
*)
let is_root prop base_exp exp =
let rec f offlist_past e = match e with
| Sil.Var _ | Sil.Const _ | Sil.UnOp _ | Sil.BinOp _ | Sil.Exn _ | Sil.Lvar _ | Sil.Sizeof _ ->
| Sil.Var _ | Sil.Const _ | Sil.UnOp _ | Sil.BinOp _ | Sil.Exn _ | Sil.Closure _ | Sil.Lvar _
| Sil.Sizeof _ ->
if check_equal prop base_exp e
then Some offlist_past
else None

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

@ -352,6 +352,8 @@ let rec prune ~positive condition prop =
prune_ne ~positive condition Sil.exp_zero prop
| Sil.Exn _ ->
assert false
| Sil.Closure _ ->
assert false
and prune_inter ~positive condition1 condition2 prop =
let res = ref Propset.empty in
@ -999,7 +1001,7 @@ 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.Cclosure c) ->
| Sil.Closure 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_exp, _, typ) -> (id_exp, typ)) c.captured_vars in

4
infer/src/checkers/addressTaken.ml
Unescape View File

@ -31,8 +31,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
add_address_taken_pvars e1 astate
|> add_address_taken_pvars e2
| Sil.Exn _
| Sil.Const (Cclosure _ | Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _
| Cptr_to_fld _)
| Sil.Closure _
| Sil.Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _)
| Var _ | Sizeof _ ->
astate

1
infer/src/checkers/checkers.ml
Unescape View File

@ -506,6 +506,7 @@ let callback_check_field_access { Callbacks.proc_desc } =
do_exp is_read e1;
do_exp is_read e2
| Sil.Exn _ -> ()
| Sil.Closure _ -> ()
| Sil.Const _ -> ()
| Sil.Cast (_, e) ->
do_exp is_read e

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

@ -174,7 +174,7 @@ struct
let rec f es =
match es with
| [] -> []
| (Sil.Const (Sil.Cclosure { name; captured_vars}),
| (Sil.Closure {name; captured_vars},
(Typ.Tptr((Typ.Tfun _), _ ) as t)) :: es' ->
let app =
let function_name = make_function_name t name in
@ -2023,7 +2023,7 @@ struct
Cfg.set_procname_priority context.cfg block_pname;
let captured_vars =
IList.map2 (fun id (pvar, typ) -> (Sil.Var id, pvar, typ)) ids captureds in
let closure = Sil.Cclosure { name=block_pname; captured_vars } in
let closure = Sil.Closure { 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 = captureds @ static_vars in
@ -2031,7 +2031,7 @@ struct
allocate_block trans_state block_name captured_static_vars loc in
{ empty_res_trans with
instrs = alloc_block_instr @ instrs;
exps = [(Sil.Const closure, typ)];
exps = [(closure, typ)];
}
| _ -> assert false
@ -2072,8 +2072,8 @@ struct
(* defining procedure. We add an edge in the call graph.*)
Cg.add_edge context.cg procname lambda_pname;
let captured_vars = [] in (* TODO *)
let closure = Sil.Cclosure { name = lambda_pname; captured_vars } in
{ empty_res_trans with exps = [(Sil.Const closure, typ)] }
let closure = Sil.Closure { name = lambda_pname; captured_vars } in
{ empty_res_trans with exps = [(closure, typ)] }
and cxxNewExpr_trans trans_state stmt_info expr_info cxx_new_expr_info =
let context = trans_state.context in

2
infer/src/unit/addressTakenTests.ml
Unescape View File

@ -27,7 +27,7 @@ let tests =
let mk_captured_var str = (Sil.Var (ident_of_str str), pvar_of_str str, int_ptr_typ) in
let captured_vars = IList.map mk_captured_var captureds in
let closure = { Sil.name=dummy_procname; captured_vars; } in
Sil.Const (Cclosure closure) in
Sil.Closure closure in
let test_list = [
"address_taken_set_instr",
[

2
infer/src/unit/livenessTests.ml
Unescape View File

@ -25,7 +25,7 @@ let tests =
let mk_captured_var str = (Sil.Var (ident_of_str str), pvar_of_str str, dummy_typ) in
let captured_vars = IList.map mk_captured_var captured_pvars in
let closure = { Sil.name=dummy_procname; captured_vars; } in
Sil.Const (Cclosure closure) in
Sil.Closure closure in
let unknown_cond =
(* don't want to use AnalyzerTest.unknown_exp because we'll treat it as a live var! *)
Sil.exp_zero in

Write Preview
Loading…
Cancel
Save