[Bucketing] Improve error bucketing by using constant propagation whe…

…n detecting direct null assignments.

infer/src/backend/buckets.ml

@@ -61,9 +61,17 @@ let check_access access_opt de_opt =
       !formal_ids in
     let formal_param_used_in_call = ref false in
     let has_call_or_sets_null node =
-      let rec exp_is_null = function
+      let rec exp_is_null exp = match exp with
         | Sil.Const (Sil.Cint n) -> Sil.Int.iszero n
         | Sil.Cast (_, e) -> exp_is_null e
+        | Sil.Var _
+        | Sil.Lvar _ ->
+            begin
+              match State.get_const_map () node exp with
+              | Some (Sil.Cint n) ->
+                  Sil.Int.iszero n
+              | _ -> false
+            end
         | _ -> false in
       let filter = function
         | Sil.Call (_, _, etl, _, _) ->
@@ -73,7 +81,8 @@ let check_access access_opt de_opt =
               | _ -> false in
             if list_exists arg_is_formal_param etl then formal_param_used_in_call := true;
             true
-        | Sil.Set (_, _, e, _) -> exp_is_null e
+        | Sil.Set (_, _, e, _) ->
+            exp_is_null e
         | _ -> false in
       list_exists filter (Cfg.Node.get_instrs node) in
     let local_access_found = ref false in

infer/src/backend/interproc.ml

@@ -467,11 +467,12 @@ let check_assignement_guard node =
 (** Perform symbolic execution for a node starting from an initial prop *)
 let do_symbolic_execution handle_exn cfg tenv
     (node : Cfg.node) (prop: Prop.normal Prop.t) (path : Paths.Path.t) =
+  let pdesc = Cfg.Node.get_proc_desc node in
   State.mark_execution_start node;
+  State.set_const_map (ConstantPropagation.build_const_map pdesc); (* build the const map lazily *)
   check_assignement_guard node;
   let instrs = Cfg.Node.get_instrs node in
   Ident.update_name_generator (instrs_get_normal_vars instrs); (* fresh normal vars must be fresh w.r.t. instructions *)
-  let pdesc = Cfg.Node.get_proc_desc node in
   let pset =
     SymExec.lifted_sym_exec handle_exn cfg tenv pdesc
       (Paths.PathSet.from_renamed_list [(prop, path)]) node instrs in
@@ -698,7 +699,7 @@ let collect_postconditions tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t =
 let create_seed_vars sigma =
   let hpred_add_seed sigma = function
     | Sil.Hpointsto (Sil.Lvar pv, se, typ) when not (Sil.pvar_is_abducted pv) ->
-      Sil.Hpointsto(Sil.Lvar (Sil.pvar_to_seed pv), se, typ) :: sigma
+        Sil.Hpointsto(Sil.Lvar (Sil.pvar_to_seed pv), se, typ) :: sigma
     | _ -> sigma in
   list_fold_left hpred_add_seed [] sigma
 

infer/src/backend/prop.ml

@@ -2772,23 +2772,19 @@ end = struct
 
   let pi_size pi = pi_weight * list_length pi
 
-  module ExpMap =
-    Map.Make (struct
-      type t = Sil.exp
-      let compare = Sil.exp_compare end)
 
   (** Approximate the size of the longest chain by counting the max
   number of |-> with the same type and whose lhs is primed or
   footprint *)
   let sigma_chain_size sigma =
-    let tbl = ref ExpMap.empty in
+    let tbl = ref Sil.ExpMap.empty in
     let add t =
       try
-        let count = ExpMap.find t !tbl in
-        tbl := ExpMap.add t (count + 1) !tbl
+        let count = Sil.ExpMap.find t !tbl in
+        tbl := Sil.ExpMap.add t (count + 1) !tbl
       with
       | Not_found ->
-          tbl := ExpMap.add t 1 !tbl in
+          tbl := Sil.ExpMap.add t 1 !tbl in
     let process_hpred = function
       | Sil.Hpointsto (e, _, te) ->
           (match e with
@@ -2797,7 +2793,7 @@ end = struct
       | Sil.Hlseg _ | Sil.Hdllseg _ -> () in
     list_iter process_hpred sigma;
     let size = ref 0 in
-    ExpMap.iter (fun t n -> size := max n !size) !tbl;
+    Sil.ExpMap.iter (fun t n -> size := max n !size) !tbl;
     !size
 
   (** Compute a size value for the prop, which indicates its

infer/src/backend/prover.ml

@@ -233,11 +233,6 @@ module Inequalities : sig
   val d_neqs : t -> unit
 end = struct
 
-  module ExpMap =
-    Map.Make (struct
-      type t = Sil.exp
-      let compare = Sil.exp_compare end)
-
   type t = {
     mutable leqs: (Sil.exp * Sil.exp) list; (** le fasts [e1 <= e2] *)
     mutable lts: (Sil.exp * Sil.exp) list; (** lt facts [e1 < e2] *)
@@ -281,14 +276,14 @@ end = struct
     else begin
       let umap_add umap e new_upper =
         try
-          let old_upper = ExpMap.find e umap in
-          if Sil.Int.leq old_upper new_upper then umap else ExpMap.add e new_upper umap
-        with Not_found -> ExpMap.add e new_upper umap in
+          let old_upper = Sil.ExpMap.find e umap in
+          if Sil.Int.leq old_upper new_upper then umap else Sil.ExpMap.add e new_upper umap
+        with Not_found -> Sil.ExpMap.add e new_upper umap in
       let lmap_add lmap e new_lower =
         try
-          let old_lower = ExpMap.find e lmap in
-          if Sil.Int.geq old_lower new_lower then lmap else ExpMap.add e new_lower lmap
-        with Not_found -> ExpMap.add e new_lower lmap in
+          let old_lower = Sil.ExpMap.find e lmap in
+          if Sil.Int.geq old_lower new_lower then lmap else Sil.ExpMap.add e new_lower lmap
+        with Not_found -> Sil.ExpMap.add e new_lower lmap in
       let rec umap_create_from_leqs umap = function
         | [] -> umap
         | (e1, Sil.Const (Sil.Cint upper1)):: leqs_rest ->
@@ -306,7 +301,7 @@ end = struct
         | constr:: constrs_rest ->
             try
               let e1, e2, n = DiffConstr.to_triple constr (* e1 - e2 <= n *) in
-              let upper2 = ExpMap.find e2 umap in
+              let upper2 = Sil.ExpMap.find e2 umap in
               let new_upper1 = upper2 ++ n in
               let new_umap = umap_add umap e1 new_upper1 in
               umap_improve_by_difference_constraints new_umap constrs_rest
@@ -317,22 +312,26 @@ end = struct
         | constr:: constrs_rest -> (* e2 - e1 > -n-1 *)
             try
               let e1, e2, n = DiffConstr.to_triple constr (* e2 - e1 > -n-1 *) in
-              let lower1 = ExpMap.find e1 lmap in
+              let lower1 = Sil.ExpMap.find e1 lmap in
               let new_lower2 = lower1 -- n -- Sil.Int.one in
               let new_lmap = lmap_add lmap e2 new_lower2 in
               lmap_improve_by_difference_constraints new_lmap constrs_rest
             with Not_found ->
                 lmap_improve_by_difference_constraints lmap constrs_rest in
       let leqs_res =
-        let umap = umap_create_from_leqs ExpMap.empty leqs in
+        let umap = umap_create_from_leqs Sil.ExpMap.empty leqs in
         let umap' = umap_improve_by_difference_constraints umap diff_constraints2 in
-        let leqs' = ExpMap.fold (fun e upper acc_leqs -> (e, Sil.exp_int upper):: acc_leqs) umap' [] in
+        let leqs' = Sil.ExpMap.fold
+            (fun e upper acc_leqs -> (e, Sil.exp_int upper):: acc_leqs)
+            umap' [] in
         let leqs'' = (list_map DiffConstr.to_leq diff_constraints2) @ leqs' in
         leqs_sort_then_remove_redundancy leqs'' in
       let lts_res =
-        let lmap = lmap_create_from_lts ExpMap.empty lts in
+        let lmap = lmap_create_from_lts Sil.ExpMap.empty lts in
         let lmap' = lmap_improve_by_difference_constraints lmap diff_constraints2 in
-        let lts' = ExpMap.fold (fun e lower acc_lts -> (Sil.exp_int lower, e):: acc_lts) lmap' [] in
+        let lts' = Sil.ExpMap.fold
+            (fun e lower acc_lts -> (Sil.exp_int lower, e):: acc_lts)
+            lmap' [] in
         let lts'' = (list_map DiffConstr.to_lt diff_constraints2) @ lts' in
         lts_sort_then_remove_redundancy lts'' in
       { leqs = leqs_res; lts = lts_res; neqs = neqs }

infer/src/backend/sil.ml

@@ -1658,6 +1658,12 @@ module ExpSet = Set.Make
     let compare = exp_compare
   end)
 
+module ExpMap = Map.Make(struct
+    type t = exp
+    let compare = exp_compare
+  end)
+
+
 let elist_to_eset es =
   list_fold_left (fun set e -> ExpSet.add e set) ExpSet.empty es
 

infer/src/backend/sil.mli

@@ -349,6 +349,9 @@ module TypMap : Map.S with type key = typ
 (** Sets of expressions. *)
 module ExpSet : Set.S with type elt = exp
 
+(** Maps with expression keys. *)
+module ExpMap : Map.S with type key = exp
+
 (** Hashtable with expressions as keys. *)
 module ExpHash : Hashtbl.S with type key = exp
 

infer/src/backend/state.ml

@@ -10,6 +10,12 @@ module L = Logging
 module F = Format
 open Utils
 
+type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option
+
+(** Constant map for the procedure *)
+let const_map : const_map ref =
+  ref (fun node exp -> None)
+
 (** Diverging states since the last reset for the node *)
 let diverging_states_node = ref Paths.PathSet.empty
 
@@ -318,3 +324,9 @@ let set_node (node: Cfg.node) =
 
 let set_session (session: int) =
   last_session := session
+
+let get_const_map () =
+  !const_map
+
+let set_const_map const_map' =
+  const_map := const_map'

infer/src/backend/state.mli

@@ -11,6 +11,11 @@ open Utils
 (** Add diverging states *)
 val add_diverging_states : Paths.PathSet.t -> unit
 
+type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option
+
+(** Get the constant map for the current procedure. *)
+val get_const_map : unit -> const_map
+
 (** Get the diverging states for the node *)
 val get_diverging_states_node : unit -> Paths.PathSet.t
 
@@ -93,6 +98,9 @@ val reset : unit -> unit
 (** Reset the diverging states and goto information for the node *)
 val reset_diverging_states_goto_node : unit -> unit
 
+(** Set the constant map for the current procedure. *)
+val set_const_map : const_map -> unit
+
 (** Set the node target of a Sil.Goto_node instruction *)
 val set_goto_node : int -> unit
 

infer/src/backend/symExec.ml

@@ -939,7 +939,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
       let sym_exe_builtin = Builtin.get_sym_exe_builtin fn in
       sym_exe_builtin cfg pdesc instr tenv _prop path ret_ids args fn loc
   | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_param, loc, call_flags) ->
-     (** Generic fun call with known name *)
+  (** Generic fun call with known name *)
       let (prop_r, _n_actual_params) = normalize_params pdesc _prop actual_param in
       let fn, n_actual_params = handle_special_cases_call tenv cfg callee_pname _n_actual_params in
       let resolved_pname =
@@ -955,24 +955,24 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
         Reporting.log_info pname exn;
         L.d_strln
           ("Undefined function " ^ Procname.to_string callee_pname
-           ^ ", returning undefined value.");
+            ^ ", returning undefined value.");
         (match Specs.get_summary pname with
-         | None -> ()
-         | Some summary ->
-            Specs.CallStats.trace
-              summary.Specs.stats.Specs.call_stats callee_pname loc
-              (Specs.CallStats.CR_skip) !Config.footprint);
+          | None -> ()
+          | Some summary ->
+              Specs.CallStats.trace
+                summary.Specs.stats.Specs.call_stats callee_pname loc
+                (Specs.CallStats.CR_skip) !Config.footprint);
         call_unknown_or_scan
           false cfg pdesc tenv prop_r path
           ret_ids ret_typ_opt n_actual_params resolved_pname loc in
       begin
         match Specs.get_summary resolved_pname with
         | None -> skip_call ()
         | Some summary when call_should_be_skipped resolved_pname summary ->
-           skip_call ()
+            skip_call ()
         | Some summary ->
-           sym_exec_call
-             cfg pdesc tenv prop_r path ret_ids n_actual_params summary loc
+            sym_exec_call
+              cfg pdesc tenv prop_r path ret_ids n_actual_params summary loc
       end
   | Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (** Call via function pointer *)
       let (prop_r, n_actual_params) = normalize_params pdesc _prop actual_params in
@@ -1192,7 +1192,7 @@ and call_unknown_or_scan is_scan cfg pdesc tenv pre path
     let do_exp p (e, t) =
       let do_attribute q = function
         | Sil.Aresource res_action as res
-             when res_action.Sil.ra_res = Sil.Rfile ->
+        when res_action.Sil.ra_res = Sil.Rfile ->
             Prop.remove_attribute res q
         | _ -> q in
       list_fold_left do_attribute p (Prop.get_exp_attributes p e) in
@@ -1229,26 +1229,26 @@ and sym_exe_check_variadic_sentinel cfg pdesc tenv prop path actual_params fails
   (* sentinels start counting from the last argument to the function *)
   let n = nargs - sentinel - 1 in
   let build_argsi (acc, i) a =
-    if i = n then (acc, i+1)
-    else ((a,i)::acc, i+1) in
+    if i = n then (acc, i +1)
+    else ((a, i):: acc, i +1) in
   (* list_fold_left reverses the arguments *)
   let non_terminal_actuals_i = fst (list_fold_left build_argsi ([], 0) args) in
   let check_allocated result ((lexp, typ), i) =
-  (* simulate a Letderef for [lexp] *)
+    (* simulate a Letderef for [lexp] *)
     let tmp_id_deref = Ident.create_fresh Ident.kprimed in
     let letderef = Sil.Letderef (tmp_id_deref, lexp, typ, loc) in
     try
       sym_exec_generated false cfg tenv pdesc [letderef] result
     with e when exn_not_timeout e ->
-      if not fails_on_nil then
-        let deref_str = Localise.deref_str_nil_argument_in_variadic_method pname nargs i in
-        let err_desc =
-          Errdesc.explain_dereference ~use_buckets: true ~is_premature_nil: true
-            deref_str prop loc in
-        raise (Exceptions.Premature_nil_termination
-                 (err_desc, try assert false with Assert_failure x -> x))
-      else
-        raise e in
+        if not fails_on_nil then
+          let deref_str = Localise.deref_str_nil_argument_in_variadic_method pname nargs i in
+          let err_desc =
+            Errdesc.explain_dereference ~use_buckets: true ~is_premature_nil: true
+              deref_str prop loc in
+          raise (Exceptions.Premature_nil_termination
+              (err_desc, try assert false with Assert_failure x -> x))
+        else
+          raise e in
   (* list_fold_left reverses the arguments back so that we report an *)
   (* error on the first premature nil argument *)
   list_fold_left check_allocated [(prop, path)] non_terminal_actuals_i
@@ -1374,7 +1374,7 @@ and sym_exec_wrapper handle_exn cfg tenv pdesc instr ((prop: Prop.normal Prop.t)
 
 let lifted_sym_exec
     handle_exn cfg tenv pdesc (pset : Paths.PathSet.t) node (instrs : Sil.instr list)
-    : Paths.PathSet.t =
+: Paths.PathSet.t =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
   let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) =
     let pset2 =
@@ -2088,8 +2088,8 @@ module ModelBuiltins = struct
                 match Specs.get_summary (Procname.from_string fun_string) with
                 | None -> assert false
                 | Some callee_summary ->
-                   sym_exec_call
-                     cfg pdesc tenv prop path ret_ids [(routine_arg, snd arg)] callee_summary loc
+                    sym_exec_call
+                      cfg pdesc tenv prop path ret_ids [(routine_arg, snd arg)] callee_summary loc
               end
           | _ ->
               L.d_str "pthread_create: unknown function "; Sil.d_exp routine_name; L.d_strln ", skipping call.";