make Tabulation.prop_get_exn_name return an option type

Summary: So that we no longer have to run `Tabulation.prop_is_exn` before running `Tabulation.prop_get_exn_name`.

Reviewed By: jberdine

Differential Revision: D3222545

fb-gh-sync-id: a7faa06
fbshipit-source-id: a7faa06

infer/src/backend/interproc.ml

@@ -256,7 +256,7 @@ let propagate
     let f prop path edgeset_curr =
       let exn_opt =
         if is_exception
-        then Some (Tabulation.prop_get_exn_name pname prop)
+        then Tabulation.prop_get_exn_name pname prop
         else None in
       Paths.PathSet.add_renamed_prop
         prop
@@ -1066,12 +1066,10 @@ let reset_global_values proc_desc =
 (* Collect all pairs of the kind (precondition, runtime exception) from a summary *)
 let exception_preconditions tenv pname summary =
   let collect_exceptions pre exns (prop, _) =
-    if Tabulation.prop_is_exn pname prop then
+    match Tabulation.prop_get_exn_name pname prop with
-      let exn_name = Tabulation.prop_get_exn_name pname prop in
+    | Some exn_name when PatternMatch.is_runtime_exception tenv exn_name ->
-      if PatternMatch.is_runtime_exception tenv exn_name then
+        (pre, exn_name) :: exns
-        (pre, exn_name):: exns
+    | _ -> exns in
-      else exns
-    else exns in
   let collect_spec errors spec =
     IList.fold_left (collect_exceptions spec.Specs.pre) errors spec.Specs.posts in
   IList.fold_left collect_spec [] (Specs.get_specs_from_payload summary)

infer/src/backend/tabulation.ml

@@ -627,24 +627,21 @@ let prop_is_exn pname prop =
 (** when prop is an exception, return the exception name *)
 let prop_get_exn_name pname prop =
   let ret_pvar = Sil.Lvar (Pvar.get_ret_pvar pname) in
-  let exn_name = ref (Typename.Java.from_string "") in
+  let rec search_exn e = function
-  let find_exn_name e =
+    | [] -> None
-    let do_hpred = function
+    | Sil.Hpointsto (e1, _, Sil.Sizeof (Sil.Tstruct  { Sil.struct_name = Some name }, _)) :: _
-      | Sil.Hpointsto (e1, _, Sil.Sizeof (Sil.Tstruct  { Sil.struct_name = Some name }, _))
+      when Sil.exp_equal e1 e ->
-        when Sil.exp_equal e1 e ->
+        Some (Typename.TN_csu (Csu.Class Csu.Java, name))
-          let found_exn_name = Typename.TN_csu (Csu.Class Csu.Java, name) in
+    | _ :: tl -> search_exn e tl in
-          exn_name := found_exn_name
+  let rec find_exn_name hpreds = function
-      | _ -> () in
+    | [] -> None
-    IList.iter do_hpred (Prop.get_sigma prop) in
+    | Sil.Hpointsto (e1, Sil.Eexp(Sil.Const (Sil.Cexn e2), _), _) :: _
-  let find_ret () =
+      when Sil.exp_equal e1 ret_pvar ->
-    let do_hpred = function
+        search_exn e2 hpreds
-      | Sil.Hpointsto (e1, Sil.Eexp(Sil.Const (Sil.Cexn e2), _), _)
+    | _ :: tl -> find_exn_name hpreds tl in
-        when Sil.exp_equal e1 ret_pvar ->
+  let hpreds = Prop.get_sigma prop in
-          find_exn_name e2
+  find_exn_name hpreds hpreds
-      | _ -> () in
+
-    IList.iter do_hpred (Prop.get_sigma prop) in
-  find_ret ();
-  !exn_name
 
 (** search in prop for some assignment of global errors *)
 let lookup_custom_errors prop =

infer/src/backend/tabulation.mli

@@ -34,7 +34,7 @@ val raise_cast_exception :
 val prop_is_exn : Procname.t -> 'a Prop.t -> bool
 
 (** when prop is an exception, return the exception name *)
-val prop_get_exn_name : Procname.t -> 'a Prop.t -> Typename.t
+val prop_get_exn_name : Procname.t -> 'a Prop.t -> Typename.t option
 
 (** search in prop contains an error state *)
 val lookup_custom_errors : 'a Prop.t -> string option