Biabduction state: option for last_node

Summary:
Using a dummy node here made the whole reporting wrong because it didn't fail getting a `node_key` when reporting issues from checkers not using the biabduction state.
Now that it's fixed, let's fail hard if someone ever tries again.

Reviewed By: jeremydubreil

Differential Revision: D9654137

fbshipit-source-id: c00273e53

infer/src/backend/errdesc.ml

@@ -462,8 +462,8 @@ let find_typ_without_ptr prop pvar =
     If there is an alloc attribute, print the function call and line number. *)
 let explain_leak tenv hpred prop alloc_att_opt bucket =
   let instro = State.get_instr () in
-  let loc = State.get_loc () in
-  let node = State.get_node () in
+  let loc = State.get_loc_exn () in
+  let node = State.get_node_exn () in
   let node_instrs = Procdesc.Node.get_instrs node in
   let hpred_typ_opt = find_hpred_typ hpred in
   let value_str_from_pvars_vpath pvars vpath =
@@ -513,7 +513,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
           L.d_str "explain_leak: current instruction is Nullify for pvar " ;
           Pvar.d pvar ;
           L.d_ln () ) ;
-        match exp_lv_dexp tenv (State.get_node ()) (Exp.Lvar pvar) with
+        match exp_lv_dexp tenv (State.get_node_exn ()) (Exp.Lvar pvar) with
         | Some de when not (DExp.has_tmp_var de) ->
             Some (DExp.to_string de)
         | _ ->
@@ -989,7 +989,7 @@ let explain_access_ proc_name tenv ?(use_buckets = false) ?(outermost_array = fa
     | _ ->
         None
   in
-  let node = State.get_node () in
+  let node = State.get_node_exn () in
   match find_exp_dereferenced () with
   | None ->
       if verbose then L.d_strln "_explain_access: find_exp_dereferenced returned None" ;
@@ -1041,8 +1041,8 @@ let dexp_apply_pvar_off dexp pvar_off =
 (** Produce a description of the nth parameter of the function call, if the current instruction
     is a function call with that parameter *)
 let explain_nth_function_parameter proc_name tenv use_buckets deref_str prop n pvar_off =
-  let node = State.get_node () in
-  let loc = State.get_loc () in
+  let node = State.get_node_exn () in
+  let loc = State.get_loc_exn () in
   match State.get_instr () with
   | Some (Sil.Call (_, _, args, _, _)) -> (
     try

infer/src/backend/exe_env.ml

@@ -91,12 +91,12 @@ let get_tenv exe_env proc_name =
       | Some tenv ->
           tenv
       | None ->
-          let loc = State.get_loc () in
+          let loc = State.get_loc_exn () in
           L.(die InternalError)
             "get_tenv: tenv not found for %a in file '%a' at %a" Typ.Procname.pp proc_name
             SourceFile.pp loc.Location.file Location.pp loc )
     | None ->
-        let loc = State.get_loc () in
+        let loc = State.get_loc_exn () in
         L.(die InternalError)
           "get_tenv: file_data not found for %a in file '%a' at %a" Typ.Procname.pp proc_name
           SourceFile.pp loc.Location.file Location.pp loc )

infer/src/backend/reporting.ml

@@ -53,11 +53,11 @@ let log_issue_deprecated_using_state severity proc_name ?node ?loc ?ltr exn =
   match Summary.get proc_name with
   | Some summary ->
       let node =
-        let node = match node with None -> State.get_node () | Some node -> node in
+        let node = match node with None -> State.get_node_exn () | Some node -> node in
         Errlog.BackendNode {node}
       in
       let session = State.get_session () in
-      let loc = match loc with None -> State.get_loc () | Some loc -> loc in
+      let loc = match loc with None -> State.get_loc_exn () | Some loc -> loc in
       let ltr = match ltr with None -> State.get_loc_trace () | Some ltr -> ltr in
       log_issue_from_summary severity summary ~node ~session ~loc ~ltr exn
   | None ->
@@ -85,9 +85,9 @@ let log_issue_external procname severity ~loc ~ltr ?access issue_type error_mess
 
 
 let log_error_using_state summary exn =
-  let node = Errlog.BackendNode {node= State.get_node ()} in
+  let node = Errlog.BackendNode {node= State.get_node_exn ()} in
   let session = State.get_session () in
-  let loc = State.get_loc () in
+  let loc = State.get_loc_exn () in
   let ltr = State.get_loc_trace () in
   log_issue_from_summary Exceptions.Error summary ~node ~session ~loc ~ltr ?access:None exn
 

infer/src/biabduction/Abs.ml

@@ -975,7 +975,7 @@ let check_observer_is_unsubscribed_deallocation tenv prop e =
     | _ ->
         None
   in
-  let loc = State.get_loc () in
+  let loc = State.get_loc_exn () in
   match Attribute.get_observer tenv prop e with
   | Some (Apred (Aobserver, _)) -> (
     match pvar_opt with

infer/src/biabduction/BuiltinDefn.ml

@@ -31,7 +31,7 @@ let mk_empty_array len = Sil.Earray (len, [], Sil.inst_none)
    it requires that the function is called with the array allocated. If not infer
    return a null pointer deref *)
 let mk_empty_array_rearranged len =
-  Sil.Earray (len, [], Sil.inst_rearrange true (State.get_loc ()) (State.get_path_pos ()))
+  Sil.Earray (len, [], Sil.inst_rearrange true (State.get_loc_exn ()) (State.get_path_pos ()))
 
 
 let extract_array_type typ =

infer/src/biabduction/Prover.ml

@@ -883,7 +883,7 @@ let check_atom tenv prop a0 =
   if Config.smt_output then (
     let key = get_smt_key a prop_no_fp in
     let key_filename =
-      let source = (State.get_loc ()).file in
+      let source = (State.get_loc_exn ()).file in
       DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source) [key ^ ".cns"]
     in
     let outc = Out_channel.create (DB.filename_to_string key_filename) in

infer/src/biabduction/Rearrange.ml

@@ -140,7 +140,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
         | [] ->
             ([], Sil.Earray (len, [], inst), t)
         | Sil.Off_index e :: off' ->
-            bounds_check tenv pname orig_prop len e (State.get_loc ()) ;
+            bounds_check tenv pname orig_prop len e (State.get_loc_exn ()) ;
             let atoms', se', res_t' =
               create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst
             in
@@ -269,7 +269,7 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp
   | ( Off_index e :: off'
     , Sil.Earray (len, esel, inst_arr)
     , Tarray {elt= typ'; length= len_for_typ'; stride} ) -> (
-      bounds_check tenv pname orig_prop len e (State.get_loc ()) ;
+      bounds_check tenv pname orig_prop len e (State.get_loc_exn ()) ;
       match List.find ~f:(fun (e', _) -> Exp.equal e e') esel with
       | Some (_, se') ->
           let atoms_se_typ_list' =
@@ -452,7 +452,7 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst :
       L.internal_error "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp ;
       let deref_str = Localise.deref_str_dangling None in
       let err_desc =
-        Errdesc.explain_dereference pname tenv deref_str orig_prop (State.get_loc ())
+        Errdesc.explain_dereference pname tenv deref_str orig_prop (State.get_loc_exn ())
       in
       raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__)) ) ;
   let off_foot, eqs = laundry_offset_for_footprint max_stamp off in
@@ -892,7 +892,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
           false
     in
     let warn accessed_fld guarded_by_str =
-      let loc = State.get_loc () in
+      let loc = State.get_loc_exn () in
       let err_desc = Localise.desc_unsafe_guarded_by_access accessed_fld guarded_by_str loc in
       let exn = Exceptions.Unsafe_guarded_by_access (err_desc, __POS__) in
       Reporting.log_issue_deprecated_using_state Exceptions.Error pname exn
@@ -1336,7 +1336,7 @@ let check_type_size tenv pname prop texp off typ_from_instr =
         && not (Prover.check_type_size_leq typ_from_instr typ_of_object)
       then
         let deref_str = Localise.deref_str_pointer_size_mismatch typ_from_instr typ_of_object in
-        let loc = State.get_loc () in
+        let loc = State.get_loc_exn () in
         let exn =
           Exceptions.Pointer_size_mismatch
             (Errdesc.explain_dereference pname tenv deref_str prop loc, __POS__)
@@ -1630,7 +1630,9 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc =
   match attribute_opt with
   | Some (Apred (Adangling dk, _)) ->
       let deref_str = Localise.deref_str_dangling (Some dk) in
-      let err_desc = Errdesc.explain_dereference pname tenv deref_str prop (State.get_loc ()) in
+      let err_desc =
+        Errdesc.explain_dereference pname tenv deref_str prop (State.get_loc_exn ())
+      in
       raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__))
   | Some (Apred (Aundef _, _)) ->
       ()
@@ -1670,7 +1672,7 @@ let check_call_to_objc_block_error tenv pdesc prop fun_exp loc =
     (* when e is a temp var, try to find the pvar defining e*)
     match e with
     | Exp.Var id -> (
-      match Errdesc.find_ident_assignment (State.get_node ()) id with
+      match Errdesc.find_ident_assignment (State.get_node_exn ()) id with
       | Some (_, e') ->
           e'
       | None ->
@@ -1682,7 +1684,7 @@ let check_call_to_objc_block_error tenv pdesc prop fun_exp loc =
     (* Exp called in the block's function call*)
     match State.get_instr () with
     | Some (Sil.Call (_, Exp.Var id, _, _, _)) ->
-        Errdesc.find_ident_assignment (State.get_node ()) id
+        Errdesc.find_ident_assignment (State.get_node_exn ()) id
     | _ ->
         None
   in
@@ -1761,7 +1763,7 @@ let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc :
   Prop.d_prop prop ;
   L.d_ln () ;
   L.d_ln () ;
-  if report_deref_errors then check_dereference_error tenv pdesc prop nlexp (State.get_loc ()) ;
+  if report_deref_errors then check_dereference_error tenv pdesc prop nlexp (State.get_loc_exn ()) ;
   let pname = Procdesc.get_proc_name pdesc in
   let prop' =
     match pname with

infer/src/biabduction/RetainCycles.ml

@@ -12,7 +12,7 @@ let desc_retain_cycle tenv (cycle : RetainCyclesType.t) =
   Logging.d_strln "Proposition with retain cycle:" ;
   let do_edge index_ edge =
     let index = index_ + 1 in
-    let node = State.get_node () in
+    let node = State.get_node_exn () in
     let from_exp_str edge_obj =
       let type_str =
         let typ_str = Typ.to_string edge_obj.rc_from.rc_node_typ in
@@ -229,7 +229,7 @@ let exn_retain_cycle tenv cycle =
     Utils.create_dir rc_dotty_dir ;
     let rc_dotty_file = Filename.temp_file ~in_dir:rc_dotty_dir "rc" ".dot" in
     RetainCyclesType.write_dotty_to_file rc_dotty_file cycle ) ;
-  let desc = Localise.desc_retain_cycle retain_cycle (State.get_loc ()) (Some cycle_dotty) in
+  let desc = Localise.desc_retain_cycle retain_cycle (State.get_loc_exn ()) (Some cycle_dotty) in
   Exceptions.Retain_cycle (desc, __POS__)
 
 

infer/src/biabduction/State.ml

@@ -31,7 +31,7 @@ type t =
   ; mutable diverging_states_proc: Paths.PathSet.t
         (** Diverging states since the last reset for the procedure *)
   ; mutable last_instr: Sil.instr option  (** Last instruction seen *)
-  ; mutable last_node: Procdesc.Node.t  (** Last node seen *)
+  ; mutable last_node: Procdesc.Node.t option  (** Last node seen *)
   ; mutable last_path: (Paths.Path.t * PredSymb.path_pos option) option  (** Last path seen *)
   ; mutable last_prop_tenv_pdesc: (Prop.normal Prop.t * Tenv.t * Procdesc.t) option
         (** Last prop,tenv,pdesc seen *)
@@ -42,7 +42,7 @@ let initial () =
   { diverging_states_node= Paths.PathSet.empty
   ; diverging_states_proc= Paths.PathSet.empty
   ; last_instr= None
-  ; last_node= Procdesc.Node.dummy None
+  ; last_node= None
   ; last_path= None
   ; last_prop_tenv_pdesc= None
   ; last_session= 0
@@ -84,15 +84,15 @@ let get_diverging_states_proc () = !gs.diverging_states_proc
 
 let get_instr () = !gs.last_instr
 
-let get_loc () =
+let get_node_exn () = Option.value_exn !gs.last_node
+
+let get_loc_exn () =
   match !gs.last_instr with
   | Some instr ->
       Sil.instr_get_loc instr
   | None ->
-      Procdesc.Node.get_loc !gs.last_node
-
+      get_node_exn () |> Procdesc.Node.get_loc
 
-let get_node () = !gs.last_node
 
 (** normalize the list of instructions by renaming let-bound ids *)
 let instrs_normalize instrs =
@@ -159,17 +159,15 @@ let mk_find_duplicate_nodes : Procdesc.t -> Procdesc.Node.t -> Procdesc.NodeSet.
     find_duplicate_nodes
 
 
-let get_node_id () = Procdesc.Node.get_id !gs.last_node
-
 let get_inst_update pos =
-  let loc = get_loc () in
+  let loc = get_loc_exn () in
   Sil.inst_update loc pos
 
 
 let get_path () =
   match !gs.last_path with
   | None ->
-      (Paths.Path.start !gs.last_node, None)
+      (Paths.Path.start (get_node_exn ()), None)
   | Some (path, pos_opt) ->
       (path, pos_opt)
 
@@ -220,7 +218,7 @@ let get_path_pos () =
     | None ->
         Typ.Procname.from_string_c_fun "unknown_procedure"
   in
-  let nid = get_node_id () in
+  let nid = Procdesc.Node.get_id (get_node_exn ()) in
   (pname, (nid :> int))
 
 
@@ -239,13 +237,13 @@ let mark_execution_end node =
 
 
 let mark_instr_ok () =
-  let fs = get_failure_stats (get_node ()) in
+  let fs = get_failure_stats (get_node_exn ()) in
   fs.instr_ok <- fs.instr_ok + 1
 
 
 let mark_instr_fail exn =
-  let loc = get_loc () in
-  let node = get_node () in
+  let loc = get_loc_exn () in
+  let node = get_node_exn () in
   let session = get_session () in
   let loc_trace = get_loc_trace () in
   let fs = get_failure_stats node in
@@ -285,7 +283,7 @@ let set_prop_tenv_pdesc prop tenv pdesc = !gs.last_prop_tenv_pdesc <- Some (prop
 
 let set_node (node : Procdesc.Node.t) =
   !gs.last_instr <- None ;
-  !gs.last_node <- node
+  !gs.last_node <- Some node
 
 
 let set_session (session : int) = !gs.last_session <- session

infer/src/biabduction/State.mli

@@ -28,13 +28,13 @@ val get_inst_update : PredSymb.path_pos -> Sil.inst
 val get_instr : unit -> Sil.instr option
 (** Get last instruction seen in symbolic execution *)
 
-val get_loc : unit -> Location.t
+val get_loc_exn : unit -> Location.t
 (** Get last location seen in symbolic execution *)
 
 val get_loc_trace : unit -> Errlog.loc_trace
 (** Get the location trace of the last path seen in symbolic execution *)
 
-val get_node : unit -> Procdesc.Node.t
+val get_node_exn : unit -> Procdesc.Node.t
 (** Get last node seen in symbolic execution *)
 
 val get_normalized_pre :

infer/src/biabduction/SymExec.ml

@@ -416,14 +416,16 @@ let check_constant_string_dereference lexp =
 let check_arith_norm_exp tenv pname exp prop =
   match Attribute.find_arithmetic_problem tenv (State.get_path_pos ()) prop exp with
   | Some (Attribute.Div0 div), prop' ->
-      let desc = Errdesc.explain_divide_by_zero tenv div (State.get_node ()) (State.get_loc ()) in
+      let desc =
+        Errdesc.explain_divide_by_zero tenv div (State.get_node_exn ()) (State.get_loc_exn ())
+      in
       let exn = Exceptions.Divide_by_zero (desc, __POS__) in
       Reporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ;
       (Prop.exp_normalize_prop tenv prop exp, prop')
   | Some (Attribute.UminusUnsigned (e, typ)), prop' ->
       let desc =
-        Errdesc.explain_unary_minus_applied_to_unsigned_expression tenv e typ (State.get_node ())
-          (State.get_loc ())
+        Errdesc.explain_unary_minus_applied_to_unsigned_expression tenv e typ
+          (State.get_node_exn ()) (State.get_loc_exn ())
       in
       let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, __POS__) in
       Reporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ;
@@ -480,8 +482,8 @@ let check_already_dereferenced tenv pname cond prop =
   match dereferenced_line with
   | Some (id, (n, _)) ->
       let desc =
-        Errdesc.explain_null_test_after_dereference tenv (Exp.Var id) (State.get_node ()) n
-          (State.get_loc ())
+        Errdesc.explain_null_test_after_dereference tenv (Exp.Var id) (State.get_node_exn ()) n
+          (State.get_loc_exn ())
       in
       let exn = Exceptions.Null_test_after_dereference (desc, __POS__) in
       Reporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
@@ -1299,7 +1301,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t)
           in
           match Prop.exp_normalize_prop tenv Prop.prop_emp cond with
           | Exp.Const (Const.Cint i) when report_condition_always_true_false i ->
-              let node = State.get_node () in
+              let node = State.get_node_exn () in
               let desc = Errdesc.explain_condition_always_true_false tenv i cond node loc in
               let exn =
                 Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__)
@@ -1870,7 +1872,7 @@ and proc_call ?dynamic_dispatch exe_env callee_summary
     | (e, t_e) :: etl', _ :: tl' ->
         (e, t_e) :: comb etl' tl'
     | _, [] ->
-        Errdesc.warning_err (State.get_loc ())
+        Errdesc.warning_err (State.get_loc_exn ())
           "likely use of variable-arguments function, or function prototype missing@." ;
         L.d_warning "likely use of variable-arguments function, or function prototype missing" ;
         L.d_ln () ;
@@ -1961,7 +1963,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr
         let instr_is_abstraction = function Sil.Abstract _ -> true | _ -> false in
         Instrs.exists ~f:instr_is_abstraction (ProcCfg.Exceptional.instrs node)
       in
-      let curr_node = State.get_node () in
+      let curr_node = State.get_node_exn () in
       match ProcCfg.Exceptional.Node.kind curr_node with
       | Procdesc.Node.Prune_node _ when not (node_has_abstraction curr_node) ->
           (* don't check for leaks in prune nodes, unless there is abstraction anyway,*)

infer/src/biabduction/Tabulation.ml

@@ -367,7 +367,7 @@ let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre fo
     let desc use_buckets deref_str =
       let error_desc =
         Errdesc.explain_dereference_as_caller_expression caller_pname tenv ~use_buckets deref_str
-          actual_pre spec_pre e (State.get_node ()) (State.get_loc ()) formal_params
+          actual_pre spec_pre e (State.get_node_exn ()) (State.get_loc_exn ()) formal_params
       in
       L.d_strln_color Red "found error in dereference" ;
       L.d_strln "spec_pre:" ;
@@ -459,7 +459,7 @@ let check_path_errors_in_post tenv caller_pname post post_path =
     | Sil.Apred (Adiv0 path_pos, [e]) ->
         if Prover.check_zero tenv e then (
           let desc =
-            Errdesc.explain_divide_by_zero tenv e (State.get_node ()) (State.get_loc ())
+            Errdesc.explain_divide_by_zero tenv e (State.get_node_exn ()) (State.get_loc_exn ())
           in
           let new_path, path_pos_opt =
             let current_path, _ = State.get_path () in
@@ -1057,8 +1057,8 @@ let inconsistent_actualpre_missing tenv actual_pre split_opt =
 
 let class_cast_exn tenv pname_opt texp1 texp2 exp ml_loc =
   let desc =
-    Errdesc.explain_class_cast_exception tenv pname_opt texp1 texp2 exp (State.get_node ())
-      (State.get_loc ())
+    Errdesc.explain_class_cast_exception tenv pname_opt texp1 texp2 exp (State.get_node_exn ())
+      (State.get_loc_exn ())
   in
   Exceptions.Class_cast_exception (desc, ml_loc)
 

infer/src/biabduction/Timeout.ml

@@ -117,5 +117,5 @@ let exe_timeout f x =
         None )
       ~finally:resume_previous_timeout
   with SymOp.Analysis_failure_exe kind ->
-    Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." SymOp.pp_failure_kind kind ;
+    Errdesc.warning_err (State.get_loc_exn ()) "TIMEOUT: %a@." SymOp.pp_failure_kind kind ;
     Some kind

infer/src/biabduction/interproc.ml

@@ -283,7 +283,7 @@ let propagate_nodes_divergence tenv (proc_cfg : ProcCfg.Exceptional.t) (pset : P
   let pname = Procdesc.get_proc_name (ProcCfg.Exceptional.proc_desc proc_cfg) in
   let pset_exn, pset_ok = Paths.PathSet.partition (Tabulation.prop_is_exn pname) pset in
   if !Config.footprint && not (Paths.PathSet.is_empty (State.get_diverging_states_node ())) then (
-    Errdesc.warning_err (State.get_loc ()) "Propagating Divergence@." ;
+    Errdesc.warning_err (State.get_loc_exn ()) "Propagating Divergence@." ;
     let exit_node = ProcCfg.Exceptional.exit_node proc_cfg in
     let diverging_states = State.get_diverging_states_node () in
     let prop_incons =