From e12a4a1071d8d065396ab33c95396371459f0975 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 4 Apr 2018 18:49:26 -0700 Subject: [PATCH] [inferbo] Add traces in lift functions Reviewed By: mbouaziz Differential Revision: D7484003 fbshipit-source-id: 4411337 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 22 +++++++------------ .../codetoanalyze/c/bufferoverrun/issues.exp | 4 ++-- .../cpp/bufferoverrun/issues.exp | 2 +- 3 files changed, 11 insertions(+), 17 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index ac316edf1..913e2b9e6 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 6c39c97eb..eb4b6302f 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/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]] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index bd8fe96d8..d8a6e692f 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/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_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_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_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_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]]