[inferbo] Uncouple numerical analysis and numerical checks

Summary:
This will allow to get the numerical results for Cost, Hoisting, Purity without the Inferbo issues.

For now, I still forced Inferbo issues for Cost and Purity to avoid lots of changes in tests, that will go away soon.

Reviewed By: ezgicicek, skcho

Differential Revision: D13826741

fbshipit-source-id: 796d1a50d

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -273,18 +273,6 @@ module Analyzer = AbstractInterpreter.MakeWTO (TransferFunctions)
 
 type invariant_map = Analyzer.invariant_map
 
-(* Use a weak Hashtbl to prevent memory leaks (GC unnecessarily
-   keeping invariant maps around) *)
-module WeakInvMapHashTbl = Caml.Weak.Make (struct
-  type t = Typ.Procname.t * invariant_map option
-
-  let equal (pname1, _) (pname2, _) = Typ.Procname.equal pname1 pname2
-
-  let hash (pname, _) = Hashtbl.hash pname
-end)
-
-let inv_map_cache = WeakInvMapHashTbl.create 100
-
 module Report = struct
   module UnusedBranch = struct
     type t = {node: CFG.Node.t; location: Location.t; condition: Exp.t; true_branch: bool}
@@ -667,11 +655,20 @@ module Report = struct
     PO.ConditionSet.for_summary ~forget_locs cond_set
 end
 
+type checks = Report.Checks.t
+
+type checks_summary = Report.PO.ConditionSet.summary_t
+
+type local_decls = PowLoc.t
+
+type memory_summary = BufferOverrunSummary.memory
+
 let extract_pre = Analyzer.extract_pre
 
 let extract_post = Analyzer.extract_post
 
-let get_local_decls proc_desc =
+let get_local_decls : Procdesc.t -> local_decls =
+ fun proc_desc ->
   let proc_name = Procdesc.get_proc_name proc_desc in
   let accum_local_decls acc {ProcAttributes.name} =
     let pvar = Pvar.mk name proc_name in
@@ -681,55 +678,75 @@ let get_local_decls proc_desc =
   Procdesc.get_locals proc_desc |> List.fold ~init:PowLoc.empty ~f:accum_local_decls
 
 
-let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t =
+let cached_compute_invariant_map =
- fun {proc_desc; tenv; integer_type_widths; summary} ->
+  let compute_invariant_map : Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map =
-  Preanal.do_preanalysis proc_desc tenv ;
+   fun pdesc tenv integer_type_widths ->
-  let pdata =
+    Preanal.do_preanalysis pdesc tenv ;
-    let oenv = Dom.OndemandEnv.mk proc_desc tenv integer_type_widths in
+    let cfg = CFG.from_pdesc pdesc in
-    ProcData.make proc_desc tenv oenv
+    let pdata =
+      let oenv = Dom.OndemandEnv.mk pdesc tenv integer_type_widths in
+      ProcData.make pdesc tenv oenv
+    in
+    let initial = Init.initial_state pdata (CFG.start_node cfg) in
+    Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata
   in
-  let cfg = CFG.from_pdesc proc_desc in
+  (* Use a weak Hashtbl to prevent memory leaks (GC unnecessarily keeps invariant maps around) *)
-  let initial = Init.initial_state pdata (CFG.start_node cfg) in
+  let module WeakInvMapHashTbl = Caml.Weak.Make (struct
-  let inv_map = Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata in
+    type t = Typ.Procname.t * invariant_map option
-  let exit_node = CFG.exit_node cfg in
+
-  let underlying_exit_node = CFG.Node.underlying_node exit_node in
+    let equal (pname1, _) (pname2, _) = Typ.Procname.equal pname1 pname2
+
+    let hash (pname, _) = Hashtbl.hash pname
+  end) in
+  let inv_map_cache = WeakInvMapHashTbl.create 100 in
+  fun pdesc tenv integer_type_widths ->
+    let pname = Procdesc.get_proc_name pdesc in
+    match WeakInvMapHashTbl.find_opt inv_map_cache (pname, None) with
+    | Some (_, Some inv_map) ->
+        inv_map
+    | Some (_, None) ->
+        (* this should never happen *)
+        assert false
+    | None ->
+        let inv_map = compute_invariant_map pdesc tenv integer_type_widths in
+        WeakInvMapHashTbl.add inv_map_cache (pname, Some inv_map) ;
+        inv_map
+
+
+let memory_summary : local_decls -> CFG.t -> invariant_map -> memory_summary =
+ fun locals cfg inv_map ->
+  let exit_node_id = CFG.exit_node cfg |> CFG.Node.id in
+  match extract_post exit_node_id inv_map with
+  | Some exit_mem ->
+      exit_mem |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv
+  | None ->
+      Bottom
+
+
+let compute_checks :
+    Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t -> invariant_map -> checks =
+  Report.check_proc
+
+
+let checks_summary : local_decls -> checks -> checks_summary =
+ fun locals checks -> Report.for_summary ~forget_locs:locals checks
+
+
+let checker : Callbacks.proc_callback_args -> Summary.t =
+ fun {proc_desc; tenv; integer_type_widths; summary} ->
+  let inv_map = cached_compute_invariant_map proc_desc tenv integer_type_widths in
+  let underlying_exit_node = Procdesc.get_exit_node proc_desc in
   let pp_name f = F.pp_print_string f "bufferoverrun check" in
   NodePrinter.start_session ~pp_name underlying_exit_node ;
   let summary =
-    let checks = Report.check_proc proc_desc tenv integer_type_widths cfg inv_map in
+    let cfg = CFG.from_pdesc proc_desc in
+    let checks = compute_checks proc_desc tenv integer_type_widths cfg inv_map in
     Report.report_errors tenv summary checks ;
     let locals = get_local_decls proc_desc in
-    let cond_set = Report.for_summary ~forget_locs:locals checks in
+    let cond_set = checks_summary locals checks in
-    let exit_mem =
+    let exit_mem = memory_summary locals cfg inv_map in
-      extract_post (CFG.Node.id exit_node) inv_map
-      |> Option.value ~default:Bottom |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv
-    in
     let payload = (exit_mem, cond_set) in
     Payload.update_summary payload summary
   in
   NodePrinter.finish_session underlying_exit_node ;
-  if Config.hoisting_report_only_expensive then
+  summary
-    let pname = Procdesc.get_proc_name proc_desc in
-    WeakInvMapHashTbl.add inv_map_cache (pname, Some inv_map)
-  else () ;
-  (inv_map, summary)
-
-
-let lookup_inv_map_cache (callback_args : Callbacks.proc_callback_args) (pname : Typ.Procname.t) :
-    invariant_map =
-  (* Since we are using a weak Hashtbl, represented as a set of
-     (Procname) hashed values, we have to lookup with a dummy element
-     *)
-  match WeakInvMapHashTbl.find_opt inv_map_cache (pname, None) with
-  | Some (_, Some inv_map) ->
-      inv_map
-  | Some (_, None) ->
-      (* this should never happen *)
-      assert false
-  | None ->
-      (* if bufferoverrun has not been run yet, run it *)
-      compute_invariant_map_and_check callback_args |> fst
-
-
-let checker : Callbacks.proc_callback_args -> Summary.t =
- fun args -> compute_invariant_map_and_check args |> snd

infer/src/bufferoverrun/bufferOverrunChecker.mli

@@ -13,9 +13,7 @@ module CFG = ProcCfg.NormalOneInstrPerNode
 
 type invariant_map
 
-val lookup_inv_map_cache : Callbacks.proc_callback_args -> Typ.Procname.t -> invariant_map
+val cached_compute_invariant_map : Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map
-
-val compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t
 
 val extract_pre : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option
 

infer/src/bufferoverrun/bufferOverrunSummary.ml

@@ -10,9 +10,11 @@ module F = Format
 module Dom = BufferOverrunDomain
 module PO = BufferOverrunProofObligations
 
-type t = Dom.Mem.no_oenv_t * PO.ConditionSet.summary_t
+type memory = Dom.Mem.no_oenv_t
 
-let get_output : t -> Dom.Mem.no_oenv_t = fst
+type t = memory * PO.ConditionSet.summary_t
+
+let get_output : t -> memory = fst
 
 let get_cond_set : t -> PO.ConditionSet.summary_t = snd
 

infer/src/checkers/cost.ml

@@ -738,9 +738,9 @@ let check_and_report_top_and_bottom cost proc_desc summary =
   else if BasicCost.is_zero cost then report IssueType.zero_execution_time_call "is zero"
 
 
-let checker ({Callbacks.tenv; proc_desc; integer_type_widths} as callback_args) : Summary.t =
+let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.t =
-  let inferbo_invariant_map, summary =
+  let inferbo_invariant_map =
-    BufferOverrunChecker.compute_invariant_map_and_check callback_args
+    BufferOverrunChecker.cached_compute_invariant_map proc_desc tenv integer_type_widths
   in
   let node_cfg = NodeCFG.from_pdesc proc_desc in
   let proc_data = ProcData.make_default proc_desc tenv in

infer/src/checkers/hoisting.ml

@@ -110,8 +110,7 @@ let get_issue_to_report tenv Call.({pname; node; params}) integer_type_widths in
   else None
 
 
-let checker ({Callbacks.tenv; summary; proc_desc; integer_type_widths} as callback_args) :
+let checker Callbacks.({tenv; summary; proc_desc; integer_type_widths}) : Summary.t =
-    Summary.t =
   let cfg = InstrCFG.from_pdesc proc_desc in
   let proc_data = ProcData.make_default proc_desc tenv in
   (* computes reaching defs: node -> (var -> node set) *)
@@ -119,9 +118,8 @@ let checker ({Callbacks.tenv; summary; proc_desc; integer_type_widths} as callba
     ReachingDefs.Analyzer.exec_cfg cfg proc_data
       ~initial:(ReachingDefs.init_reaching_defs_with_formals proc_desc)
   in
-  let pname = Procdesc.get_proc_name proc_desc in
   let inferbo_invariant_map =
-    lazy (BufferOverrunChecker.lookup_inv_map_cache callback_args pname)
+    lazy (BufferOverrunChecker.cached_compute_invariant_map proc_desc tenv integer_type_widths)
   in
   (* get dominators *)
   let idom = Dominators.get_idoms proc_desc in

infer/src/checkers/purity.ml

@@ -182,10 +182,10 @@ let should_report pdesc =
       L.(die InternalError "Not supposed to run on non-Java code.")
 
 
-let checker ({Callbacks.tenv; summary; proc_desc} as callback_args) : Summary.t =
+let checker {Callbacks.tenv; summary; proc_desc; integer_type_widths} : Summary.t =
   let proc_name = Procdesc.get_proc_name proc_desc in
-  let inferbo_invariant_map, _ =
+  let inferbo_invariant_map =
-    BufferOverrunChecker.compute_invariant_map_and_check callback_args
+    BufferOverrunChecker.cached_compute_invariant_map proc_desc tenv integer_type_widths
   in
   let formals =
     Procdesc.get_formals proc_desc

infer/src/checkers/registerCheckers.ml

@@ -44,9 +44,7 @@ let all_checkers =
         [ (DynamicDispatch Interproc.analyze_procedure, Language.Clang)
         ; (DynamicDispatch Interproc.analyze_procedure, Language.Java) ] }
   ; { name= "buffer overrun"
-    ; active=
+    ; active= Config.bufferoverrun || Config.cost || Config.purity || Config.quandaryBO
-        (Config.bufferoverrun || Config.quandaryBO) && not Config.cost
-        (* Cost analysis already triggers Inferbo *)
     ; callbacks=
         [ (Procedure BufferOverrunChecker.checker, Language.Clang)
         ; (Procedure BufferOverrunChecker.checker, Language.Java) ] }

infer/tests/codetoanalyze/java/hoisting/issues.exp

@@ -1,7 +1,6 @@
 codetoanalyze/java/hoisting/Hoist.java, Hoist.array_store_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 117 is loop-invariant]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.clash_function_calls_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 26 is loop-invariant]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.legit_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 73 is loop-invariant]
-codetoanalyze/java/hoisting/Hoist.java, Hoist.loop_guard_hoist(int,int[]):void, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.loop_guard_hoist(int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 65 is loop-invariant]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_hoist(int,int,int):void, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_hoist(int,int,int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 127 is loop-invariant]
@@ -10,23 +9,24 @@ codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void,
 codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.bar(int) at line 35 is loop-invariant]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.used_in_loop_body_before_def_temp_hoist(int,int[]):void, 6, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 57 is loop-invariant]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.void_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void Hoist.dumb_foo() at line 183 is loop-invariant]
-codetoanalyze/java/hoisting/Hoist.java, Hoist.x_not_invariant_dont_hoist(int,int,int):void, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: int Hoist.foo(int,int),Assignment,<RHS trace>,Parameter `y`,Binary operation: ([-oo, +oo] + y):signed32]
+codetoanalyze/java/hoisting/Hoist.java, Hoist.x_not_invariant_dont_hoist(int,int,int):void, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `y`,Call,Parameter `x`,Assignment,Assignment,<RHS trace>,Parameter `y`,Binary operation: ([-oo, +oo] + y):signed32]
-codetoanalyze/java/hoisting/HoistGlobal.java, HoistGlobal.global_modification_dont_hoist(int):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistGlobal.read_global(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/Hoist.java, Hoist.x_not_invariant_dont_hoist(int,int,int):void, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter `y`,Call,<LHS trace>,Parameter `x`,<RHS trace>,Parameter `y`,Binary operation: ([-oo, +oo] + y):signed32 by call to `int Hoist.foo(int,int)` ]
+codetoanalyze/java/hoisting/HoistGlobal.java, HoistGlobal.global_modification_dont_hoist(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Assignment,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.indirect_modification_hoist(int):int, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect$Test.foo(int) at line 72 is loop-invariant]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.indirect_modification_only_second_call_hoist(int,HoistIndirect$Test,HoistIndirect$Test):int, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect$Test.get_test(HoistIndirect$Test) at line 86 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.arg_modification_hoist(int,HoistIndirect$Test):int, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect.get(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.arg_modification_hoist(int,HoistIndirect$Test):int, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Assignment,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.arg_modification_hoist(int,HoistIndirect$Test):int, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 133 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.direct_this_modification_dont_hoist_FP(int):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect.get(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.direct_this_modification_dont_hoist_FP(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Assignment,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.direct_this_modification_dont_hoist_FP(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 115 is loop-invariant]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.independent_hoist(int,HoistIndirect$Test):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect$Test.foo(int) at line 160 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.independent_hoist(int,HoistIndirect$Test):int, 5, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect.get_ith(int,int[]),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.irvar_change_dont_hoist(int[][],int,int[]):void, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.irvar_independent_hoist(int[][],int,int[]):void, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: int HoistIndirect.regionFirst(int[]),Assignment,<RHS trace>,Unknown value from: int HoistIndirect.double_me(int),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.irvar_independent_hoist(int[][],int,int[]):void, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.irvar_independent_hoist(int[][],int,int[]):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.double_me(int) at line 210 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.modified_array_dont_hoist(int,HoistIndirect$Test):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect.get_ith(int,int[]),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.modified_inner_array_dont_hoist(int,HoistIndirect$Test):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Assignment,Call,Parameter `x`,Assignment,Assignment,Binary operation: ([0, +oo] + 10):signed32]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.modified_inner_array_dont_hoist(int,HoistIndirect$Test):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect$Test.foo(int),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.this_modification_outside_hoist(int):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Assignment,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.this_modification_outside_hoist(int):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect.get(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.this_modification_outside_hoist(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 125 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.unmodified_arg_hoist(int[][],int,int[]):void, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: int HoistIndirect.regionFirst(int[]),Assignment,<RHS trace>,Unknown value from: int HoistIndirect.regionFirst(int[]),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.tmp_irvar_change_dont_hoist(int[][],int,int[]):void, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.unmodified_arg_hoist(int[][],int,int[]):void, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.unmodified_arg_hoist(int[][],int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.regionFirst(int[]) at line 220 is loop-invariant]
 codetoanalyze/java/hoisting/HoistInvalidate.java, HoistInvalidate.loop_indirect_hoist(java.util.ArrayList,int,int[]):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistInvalidate.get_length(int[]) at line 52 is loop-invariant]
 codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.deserialize_hoist(com.fasterxml.jackson.databind.JsonDeserializer,com.fasterxml.jackson.core.JsonParser,com.fasterxml.jackson.databind.DeserializationContext):void, 8, LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to Object JsonDeserializer.deserialize(JsonParser,DeserializationContext) at line 33 is loop-invariant]
@@ -36,6 +36,6 @@ codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.list_contains_hoist(
 codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.avg(java.util.ArrayList):int, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: __cast,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.avg(java.util.ArrayList):int, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int Integer.intValue(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
 codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.increment_dont_hoist_FP(int):int, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.calcNext() at line 28 is loop-invariant]
-codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.modify_and_increment_dont_hoist_FP(int):int, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistNoIndirectMod.calcNext(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.modify_and_increment_dont_hoist_FP(int):int, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Parameter `this.id`,Call,Parameter `this.id`,Assignment,Assignment,Binary operation: ([-oo, +oo] + [1+min(0, this.id), +oo]):signed32]
 codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.modify_and_increment_dont_hoist_FP(int):int, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.calcNext() at line 36 is loop-invariant]
 codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.no_mod_hoist(java.lang.Integer[],java.util.ArrayList):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.avg(ArrayList) at line 77 is loop-invariant]