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

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

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

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 */

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

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

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

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)

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
 

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

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

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

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

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

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

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

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

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 =