[inferbo] Add traces in lift functions

Reviewed By: mbouaziz

Differential Revision: D7484003

fbshipit-source-id: 4411337

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -116,31 +116,25 @@ module Val = struct
   let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv}
 
   let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t =
-   fun f x y -> {bot with itv= f x.itv y.itv}
+   fun f x y -> {bot with itv= f x.itv y.itv; traces= TraceSet.join x.traces y.traces}
 
 
   let has_pointer : t -> bool = fun x -> not (PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk)
 
   let lift_cmp_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t =
    fun f x y ->
-    if has_pointer x || has_pointer y then {bot with itv= Itv.unknown_bool} else lift_itv f x y
+    if has_pointer x || has_pointer y then
+      {bot with itv= Itv.unknown_bool; traces= TraceSet.join x.traces y.traces}
+    else lift_itv f x y
 
 
-  let plus_a : t -> t -> t =
-   fun x y -> {(lift_itv Itv.plus x y) with traces= TraceSet.join x.traces y.traces}
+  let plus_a : t -> t -> t = lift_itv Itv.plus
 
+  let minus_a : t -> t -> t = lift_itv Itv.minus
 
-  let minus_a : t -> t -> t =
-   fun x y -> {(lift_itv Itv.minus x y) with traces= TraceSet.join x.traces y.traces}
-
-
-  let mult : t -> t -> t =
-   fun x y -> {(lift_itv Itv.mult x y) with traces= TraceSet.join x.traces y.traces}
-
-
-  let div : t -> t -> t =
-   fun x y -> {(lift_itv Itv.div x y) with traces= TraceSet.join x.traces y.traces}
+  let mult : t -> t -> t = lift_itv Itv.mult
 
+  let div : t -> t -> t = lift_itv Itv.div
 
   let mod_sem : t -> t -> t = lift_itv Itv.mod_sem
 

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -1,5 +1,5 @@
-codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]]
-codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]]
+codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: [5, 5]]
+codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, ERROR, [ArrayDeclaration,Parameter: i,ArrayAccess: Offset: [-4, 4] Size: [5, 5]]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: [10, 10]]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: [20, 20]]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: [19, 19]]

infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp

@@ -31,7 +31,7 @@ codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_O
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, WARNING, []
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [5, 5]]
 codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, WARNING, []
-codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN_L5, ERROR, [Call,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
+codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN_L5, ERROR, [Call,Call,Assignment,Return,Assignment,Return,Assignment,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [0, +oo] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, BUFFER_OVERRUN_S2, ERROR, [Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_u_FP, 5, BUFFER_OVERRUN_S2, ERROR, [Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$8), -1+max(1, s$9)] Size: [0, +oo]]
 codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, ERROR, [Call,Call,Parameter: bi,Call,Call,ArrayDeclaration,Assignment,Parameter: index,ArrayAccess: Offset: [-1+max(1, s$4), -1+max(1, s$5)] Size: [0, +oo]]