From c5ce74f3d301ca70eba78e1c79c506b080d477fe Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 13 Jul 2016 15:50:56 -0700 Subject: [PATCH] Exception values are not constants Summary: Move exception values from const to exp. They are not constants, and this reduces interdependence between Sil types. Reviewed By: sblackshear Differential Revision: D3541355 fbshipit-source-id: f22e0ba --- infer/src/IR/Cfg.re | 2 +- infer/src/IR/Sil.re | 26 ++++++++++++++------------ infer/src/IR/Sil.rei | 3 ++- infer/src/backend/dom.ml | 1 + infer/src/backend/match.ml | 2 ++ infer/src/backend/modelBuiltins.ml | 4 ++-- infer/src/backend/prop.ml | 7 +++++-- infer/src/backend/propgraph.ml | 2 +- infer/src/backend/prover.ml | 2 +- infer/src/backend/symExec.ml | 6 ++++-- infer/src/backend/tabulation.ml | 4 ++-- infer/src/checkers/addressTaken.ml | 3 ++- infer/src/checkers/checkers.ml | 1 + infer/src/checkers/dataflow.ml | 2 +- infer/src/eradicate/typeCheck.ml | 4 ++-- infer/src/java/jTrans.ml | 8 ++++---- infer/src/java/jTransExn.ml | 3 ++- 17 files changed, 47 insertions(+), 33 deletions(-) diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index 1d1effacf..b8ee2202b 100644 --- a/infer/src/IR/Cfg.re +++ b/infer/src/IR/Cfg.re @@ -906,7 +906,7 @@ let remove_abducted_retvars p => let (sigma, pi) = (Prop.get_sigma p, Prop.get_pi p); let rec collect_exps exps => fun - | Sil.Eexp (Sil.Const (Sil.Cexn e)) _ => Sil.ExpSet.add e exps + | Sil.Eexp (Sil.Exn e) _ => Sil.ExpSet.add e exps | Sil.Eexp e _ => Sil.ExpSet.add e exps | Sil.Estruct flds _ => IList.fold_left (fun exps (_, strexp) => collect_exps exps strexp) exps flds diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 5f1f2cdad..78dd24e1a 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -470,7 +470,6 @@ and const = | Cstr of string /** string constants */ | Cfloat of float /** float constants */ | Cattribute of attribute /** attribute used in disequalities to annotate a value */ - | Cexn of exp /** exception */ | 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 */ @@ -485,6 +484,8 @@ and exp = | UnOp of unop exp (option Typ.t) /** Binary operator */ | BinOp of binop exp exp + /** Exception */ + | Exn of exp /** Constants */ | Const of const /** Type cast */ @@ -980,7 +981,6 @@ let const_kind_equal c1 c2 => { | Cstr _ => 3 | Cfloat _ => 4 | Cattribute _ => 5 - | Cexn _ => 6 | Cclass _ => 7 | Cptr_to_fld _ => 8 | Cclosure _ => 9; @@ -1075,9 +1075,6 @@ and const_compare (c1: const) (c2: const) :int => | (Cattribute att1, Cattribute att2) => attribute_compare att1 att2 | (Cattribute _, _) => (-1) | (_, Cattribute _) => 1 - | (Cexn e1, Cexn e2) => exp_compare e1 e2 - | (Cexn _, _) => (-1) - | (_, Cexn _) => 1 | (Cclass c1, Cclass c2) => Ident.name_compare c1 c2 | (Cclass _, _) => (-1) | (_, Cclass _) => 1 @@ -1148,6 +1145,9 @@ and exp_compare (e1: exp) (e2: exp) :int => } | (BinOp _, _) => (-1) | (_, BinOp _) => 1 + | (Exn e1, Exn e2) => exp_compare e1 e2 + | (Exn _, _) => (-1) + | (_, Exn _) => 1 | (Const c1, Const c2) => const_compare c1 c2 | (Const _, _) => (-1) | (_, Const _) => 1 @@ -1762,7 +1762,6 @@ and pp_const pe f => | Cstr s => F.fprintf f "\"%s\"" (String.escaped s) | Cfloat v => F.fprintf f "%f" v | Cattribute att => F.fprintf f "%s" (attribute_to_string pe att) - | 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 | Cclosure {name, captured_vars} => { @@ -1803,6 +1802,7 @@ and _pp_exp pe0 pp_t f e0 => { | UnOp op e _ => F.fprintf f "%s%a" (str_unop op) pp_exp e | 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 | 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 @@ -2684,7 +2684,8 @@ let rec root_of_lexp lexp => | Const _ => lexp | Cast _ e => root_of_lexp e | UnOp _ - | BinOp _ => lexp + | BinOp _ + | Exn _ => lexp | Lvar _ => lexp | Lfield e _ _ => root_of_lexp e | Lindex e _ => root_of_lexp e @@ -2765,7 +2766,7 @@ let exp_lt e1 e2 => BinOp Lt e1 e2; let rec exp_fpv = fun | Var _ => [] - | Const (Cexn e) => exp_fpv e + | Exn e => exp_fpv e | Const (Cclosure {captured_vars}) => IList.map (fun (_, pvar, _) => pvar) captured_vars | Const _ => [] | Cast _ e @@ -2956,7 +2957,7 @@ let fav_mem fav id => IList.exists (Ident.equal id) !fav; let rec exp_fav_add fav => fun | Var id => fav ++ id - | Const (Cexn e) => exp_fav_add fav e + | Exn e => exp_fav_add fav e | Const (Cclosure {captured_vars}) => IList.iter (fun (e, _, _) => exp_fav_add fav e) captured_vars | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _) => () @@ -3356,12 +3357,12 @@ let rec exp_sub_ids (f: Ident.t => exp) exp => switch exp { | Var id => f id | Lvar _ => exp - | Const (Cexn e) => + | Exn e => let e' = exp_sub_ids f e; if (e' === e) { exp } else { - Const (Cexn e') + Exn e' } | Const (Cclosure c) => let captured_vars = @@ -4046,7 +4047,7 @@ let exp_get_vars exp => { | Cast _ e | UnOp _ e _ | Lfield e _ _ - | Const (Cexn e) => exp_get_vars_ e vars + | 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}) => @@ -4072,6 +4073,7 @@ let exp_get_offsets exp => { | Const _ | UnOp _ | BinOp _ + | Exn _ | Lvar _ | Sizeof _ None _ => offlist_past | Sizeof _ (Some l) _ => f offlist_past l diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index 8e4491594..adc004b35 100644 --- a/infer/src/IR/Sil.rei +++ b/infer/src/IR/Sil.rei @@ -197,7 +197,6 @@ and const = | Cstr of string /** string constants */ | Cfloat of float /** float constants */ | Cattribute of attribute /** attribute used in disequalities to annotate a value */ - | Cexn of exp /** exception */ | 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 */ @@ -212,6 +211,8 @@ and exp = | UnOp of unop exp (option Typ.t) /** Binary operator */ | BinOp of binop exp exp + /** Exception */ + | Exn of exp /** Constants */ | Const of const /** Type cast */ diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index d15bf22c8..b4d408811 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -813,6 +813,7 @@ let rec exp_construct_fresh side e = let e1' = exp_construct_fresh side e1 in let e2' = exp_construct_fresh side e2 in Sil.BinOp(binop, e1', e2') + | Sil.Exn _ -> e | Sil.Lvar _ -> e | Sil.Lfield(e1, fld, typ) -> diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml index 3e4a93912..123475a24 100644 --- a/infer/src/backend/match.ml +++ b/infer/src/backend/match.ml @@ -68,6 +68,8 @@ let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option = | Some (sub', vars') -> exp_match e1'' sub' vars' e2'') | Sil.BinOp _, _ | _, Sil.BinOp _ -> None (* Naive *) + | Sil.Exn _, _ | _, Sil.Exn _ -> + 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) -> diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index 52cf89673..c06003ea8 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/modelBuiltins.ml @@ -757,7 +757,7 @@ 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.Const _ | Sil.Cast _ | Sil.Lvar _ | Sil.Lfield _ | Sil.Lindex _ -> e + | Sil.Exn _ | 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 -> @@ -879,7 +879,7 @@ let execute__unwrap_exception { Builtin.pdesc; prop_; path; ret_ids; args; } let pname = Cfg.Procdesc.get_proc_name pdesc in let n_ret_exn, prop = check_arith_norm_exp pname ret_exn prop_ in match n_ret_exn with - | Sil.Const (Sil.Cexn exp) -> + | Sil.Exn exp -> let prop_with_exn = return_result exp prop ret_ids in [(prop_with_exn, path)] | _ -> assert false diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 5e001523a..92c616110 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -810,6 +810,8 @@ let sym_eval abs e = Sil.exp_zero (* cause a NULL dereference *) | _ -> Sil.BinOp (Sil.PtrFld, e1', e2') end + | Sil.Exn _ -> + e | Sil.Lvar _ -> e | Sil.Lfield (e1, fld, typ) -> @@ -1524,7 +1526,7 @@ let prop_sigma_star (p : 'a t) (sigma : sigma) : exposed t = (** return the set of subexpressions of [strexp] *) let strexp_get_exps strexp = let rec strexp_get_exps_rec exps = function - | Sil.Eexp (Sil.Const (Sil.Cexn e), _) -> Sil.ExpSet.add e exps + | Sil.Eexp (Sil.Exn e, _) -> Sil.ExpSet.add e exps | Sil.Eexp (e, _) -> Sil.ExpSet.add e exps | Sil.Estruct (flds, _) -> IList.fold_left (fun exps (_, strexp) -> strexp_get_exps_rec exps strexp) exps flds @@ -1975,6 +1977,7 @@ let find_arithmetic_problem proc_node_session prop exp = | Sil.BinOp(op, e1, e2) -> if op = Sil.Div || op = Sil.Mod then exps_divided := e2 :: !exps_divided; walk e1; walk e2 + | Sil.Exn _ -> () | Sil.Const _ -> () | Sil.Cast (_, e) -> walk e | Sil.Lvar _ -> () @@ -2260,7 +2263,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.Const (Sil.Cexn e) -> Sil.Const (Sil.Cexn (exp_captured_ren ren e)) + | Sil.Exn e -> Sil.Exn (exp_captured_ren ren e) | 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) diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml index 9a6810f50..91636dd02 100644 --- a/infer/src/backend/propgraph.ml +++ b/infer/src/backend/propgraph.ml @@ -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.Lvar _ -> true + | Sil.Const _ | Sil.Exn _ | Sil.Lvar _ -> true | Sil.Cast (_, e) -> is_root e | Sil.UnOp _ | Sil.BinOp _ | Sil.Lfield _ | Sil.Lindex _ | Sil.Sizeof _ -> false diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index bf297f71d..75bdb3a3c 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -551,7 +551,7 @@ 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.Lvar _ | Sil.Sizeof _ -> + | Sil.Var _ | Sil.Const _ | Sil.UnOp _ | Sil.BinOp _ | Sil.Exn _ | Sil.Lvar _ | Sil.Sizeof _ -> if check_equal prop base_exp e then Some offlist_past else None diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 61e6e605b..30869821e 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -350,6 +350,8 @@ let rec prune ~positive condition prop = pruner ~positive condition1 condition2 prop | Sil.BinOp _ | Sil.Lfield _ | Sil.Lindex _ -> prune_ne ~positive condition Sil.exp_zero prop + | Sil.Exn _ -> + assert false and prune_inter ~positive condition1 condition2 prop = let res = ref Propset.empty in @@ -1204,8 +1206,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path match attrs_opt with | Some attrs -> attrs.ProcAttributes.is_objc_instance_method | None -> false in - skip_call ~is_objc_instance_method prop path resolved_pname ret_annots loc ret_ids - ret_typ_opt n_actual_params + skip_call ~is_objc_instance_method prop path resolved_pname ret_annots loc ret_ids + ret_typ_opt n_actual_params else proc_call (Option.get summary) (call_args prop resolved_pname n_actual_params ret_ids loc) in diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index f1bdbe0df..49272302b 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -612,7 +612,7 @@ let prop_copy_footprint_pure p1 p2 = (** check if an expression is an exception *) let exp_is_exn = function - | Sil.Const Sil.Cexn _ -> true + | Sil.Exn _ -> true | _ -> false (** check if a prop is an exception *) @@ -635,7 +635,7 @@ let prop_get_exn_name pname prop = | _ :: tl -> search_exn e tl in let rec find_exn_name hpreds = function | [] -> None - | Sil.Hpointsto (e1, Sil.Eexp(Sil.Const (Sil.Cexn e2), _), _) :: _ + | Sil.Hpointsto (e1, Sil.Eexp (Sil.Exn e2, _), _) :: _ when Sil.exp_equal e1 ret_pvar -> search_exn e2 hpreds | _ :: tl -> find_exn_name hpreds tl in diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index ddd9cee78..10401a252 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -30,7 +30,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Sil.BinOp (_, e1, e2) | Lindex (e1, e2) -> add_address_taken_pvars e1 astate |> add_address_taken_pvars e2 - | Sil.Const (Cclosure _ | Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cexn _ | Cclass _ + | Sil.Exn _ + | Sil.Const (Cclosure _ | Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cattribute _ | Cclass _ | Cptr_to_fld _) | Var _ | Sizeof _ -> astate diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index f7b4f6c63..0d2b5cd71 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -505,6 +505,7 @@ let callback_check_field_access { Callbacks.proc_desc } = | Sil.BinOp (_, e1, e2) -> do_exp is_read e1; do_exp is_read e2 + | Sil.Exn _ -> () | Sil.Const _ -> () | Sil.Cast (_, e) -> do_exp is_read e diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml index 3ced387a9..3fa2c31d4 100644 --- a/infer/src/checkers/dataflow.ml +++ b/infer/src/checkers/dataflow.ml @@ -48,7 +48,7 @@ let node_throws node (proc_throws : Procname.t -> throws) : throws = let ret_pvar = Cfg.Procdesc.get_ret_var pdesc in Pvar.equal pvar ret_pvar in match instr with - | Sil.Set (Sil.Lvar pvar, _, Sil.Const (Sil.Cexn _), _) when is_return pvar -> + | Sil.Set (Sil.Lvar pvar, _, Sil.Exn _, _) when is_return pvar -> (* assignment to return variable is an artifact of a throw instruction *) Throws | Sil.Call (_, Sil.Const (Sil.Cfun callee_pn), _, _, _) diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index ed3e59429..a38900173 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -176,7 +176,7 @@ let rec typecheck_expr else let t, ta, ll = tr_default in (t, TypeAnnotation.with_origin ta (TypeOrigin.Const loc), ll) - | Sil.Const (Sil.Cexn e1) -> + | Sil.Exn e1 -> typecheck_expr find_canonical_duplicate visited checks node instr_ref curr_pname @@ -481,7 +481,7 @@ let typecheck_instr TypeState.add_id id (typecheck_expr_simple typestate' e' typ TypeOrigin.Undef loc) typestate' - | Sil.Set (Sil.Lvar pvar, _, Sil.Const (Sil.Cexn _), _) when is_return pvar -> + | Sil.Set (Sil.Lvar pvar, _, Sil.Exn _, _) when is_return pvar -> (* skip assignment to return variable where it is an artifact of a throw instruction *) typestate | Sil.Set (e1, typ, e2, loc) -> diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index ba789aa88..8158fdef9 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -891,7 +891,7 @@ let rec instruction context pc instr : translation = Prune (prune_node_true, prune_node_false) | JBir.Throw expr -> let (instrs, sil_expr, _) = expression context pc expr in - let sil_exn = Sil.Const (Sil.Cexn sil_expr) in + let sil_exn = Sil.Exn 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 (instrs @ [sil_instr]) in JContext.add_goto_jump context pc JContext.Exit; @@ -1022,7 +1022,7 @@ let rec instruction context pc instr : translation = 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 sil_exn = Sil.Exn (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 npe_instrs in @@ -1076,7 +1076,7 @@ let rec instruction context pc instr : translation = method_invocation context loc pc None out_of_bound_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 sil_exn = Sil.Exn (Sil.Var ret_id) in 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 @@ -1114,7 +1114,7 @@ let rec instruction context pc instr : translation = 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 sil_exn = Sil.Exn (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 diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index 3dd4fd987..1e77f327b 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -77,7 +77,8 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table = let instr_set_catch_var = let catch_var = JContext.set_pvar context handler.JBir.e_catch_var ret_type in Sil.Set (Sil.Lvar catch_var, ret_type, Sil.Var id_exn_val, loc) in - let instr_rethrow_exn = Sil.Set (Sil.Lvar ret_var, ret_type, Sil.Const (Sil.Cexn (Sil.Var id_exn_val)), loc) in + let instr_rethrow_exn = + Sil.Set (Sil.Lvar ret_var, ret_type, Sil.Exn (Sil.Var id_exn_val), loc) in let node_kind_true = Cfg.Node.Prune_node (true, if_kind, exn_message) in let node_kind_false = Cfg.Node.Prune_node (false, if_kind, exn_message) in let node_true =