From e505fd2dba4d45899f48eb180ae0865d8a94b7b1 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Sun, 25 Nov 2018 12:19:28 -0800 Subject: [PATCH] [inferbo] Pointer comparison Reviewed By: skcho Differential Revision: D13066771 fbshipit-source-id: 134b27db8 --- infer/src/bufferoverrun/absLoc.ml | 24 +++++++++++ infer/src/bufferoverrun/arrayBlk.ml | 16 ++++++++ infer/src/bufferoverrun/boolean.ml | 30 ++++++++++++++ infer/src/bufferoverrun/boolean.mli | 26 ++++++++++++ .../src/bufferoverrun/bufferOverrunDomain.ml | 41 +++++++++++++------ .../codetoanalyze/c/bufferoverrun/global.c | 8 +++- .../codetoanalyze/c/bufferoverrun/issues.exp | 6 ++- .../c/bufferoverrun/prune_alias.c | 34 +++++++++++++++ .../codetoanalyze/java/performance/Loops.java | 2 +- .../codetoanalyze/java/performance/issues.exp | 6 ++- 10 files changed, 174 insertions(+), 19 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 858a1b65f..0d0aee49a 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -21,6 +21,18 @@ module Allocsite = struct ; path: Symb.SymbolPath.partial option } [@@deriving compare] + let eq as1 as2 = + match (as1, as2) with + | Unknown, _ | _, Unknown -> + Boolean.Top + | Known {path= Some _}, Known {path= Some _} -> + (* Known with a path are parameters, parameters may alias *) Boolean.Top + | Known {path= Some _}, Known {path= None} | Known {path= None}, Known {path= Some _} -> + Boolean.False + | Known {path= None}, Known {path= None} -> + Boolean.of_bool ([%compare.equal: t] as1 as2) + + let pp fmt = function | Unknown -> F.fprintf fmt "Unknown" @@ -57,6 +69,10 @@ module Loc = struct let equal = [%compare.equal: t] + let eq l1 l2 = + match (l1, l2) with Allocsite as1, Allocsite as2 -> Allocsite.eq as1 as2 | _ -> Boolean.Top + + let unknown = Allocsite Allocsite.unknown let rec pp fmt = function @@ -127,6 +143,14 @@ module PowLoc = struct let append_field ploc ~fn = if is_bot ploc then singleton Loc.unknown else fold (fun l -> add (Loc.append_field l ~fn)) ploc empty + + + let lift_cmp cmp_loc ploc1 ploc2 = + match (is_singleton_or_more ploc1, is_singleton_or_more ploc2) with + | IContainer.Singleton loc1, IContainer.Singleton loc2 -> + Boolean.EqualOrder.of_equal cmp_loc (Loc.eq loc1 loc2) + | _ -> + Boolean.Top end (** unsound but ok for bug catching *) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index f7370bf65..37b8e18f7 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -103,6 +103,12 @@ module ArrInfo = struct else let set itv = Itv.div_const (Itv.mult_const itv stride) new_stride in {offset= set offset; size= set size; stride= Itv.of_big_int new_stride} ) + + + let lift_cmp_itv cmp_itv arr1 arr2 = + if Itv.eq arr1.stride arr2.stride && Itv.eq arr1.size arr2.size then + cmp_itv arr1.offset arr2.offset + else Boolean.Top end include AbstractDomain.Map (Allocsite) (ArrInfo) @@ -184,3 +190,13 @@ let prune_ne : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_ let set_length : Itv.t -> astate -> astate = fun length a -> map (ArrInfo.set_length length) a let set_stride : Z.t -> astate -> astate = fun stride a -> map (ArrInfo.set_stride stride) a + +let lift_cmp_itv cmp_itv cmp_loc arr1 arr2 = + match (is_singleton_or_more arr1, is_singleton_or_more arr2) with + | IContainer.Singleton (as1, ai1), IContainer.Singleton (as2, ai2) -> + Boolean.EqualOrder.( + of_equal + {on_equal= ArrInfo.lift_cmp_itv cmp_itv ai1 ai2; on_not_equal= cmp_loc.on_not_equal} + (Allocsite.eq as1 as2)) + | _ -> + Boolean.Top diff --git a/infer/src/bufferoverrun/boolean.ml b/infer/src/bufferoverrun/boolean.ml index 1806a866f..d0ec8d2f6 100644 --- a/infer/src/bufferoverrun/boolean.ml +++ b/infer/src/bufferoverrun/boolean.ml @@ -11,6 +11,8 @@ type t = Bottom | False | True | Top [@@deriving compare] let equal = [%compare.equal: t] +let of_bool = function false -> False | true -> True + let is_false = function False -> true | _ -> false let is_true = function True -> true | _ -> false @@ -39,3 +41,31 @@ let or_ x y = True | Top, Top -> Top + + +module EqualOrder = struct + type b = t + + type t = {on_equal: b; on_not_equal: b} + + let eq = {on_equal= True; on_not_equal= False} + + let ne = {on_equal= False; on_not_equal= True} + + let strict_cmp = {on_equal= False; on_not_equal= Top} + + let loose_cmp = {on_equal= True; on_not_equal= Top} + + let top = {on_equal= Top; on_not_equal= Top} + + let of_equal t equal = + match equal with + | Bottom -> + Bottom + | True -> + t.on_equal + | False -> + t.on_not_equal + | Top -> + (* join t.on_equal t.on_not_equal is always Top *) Top +end diff --git a/infer/src/bufferoverrun/boolean.mli b/infer/src/bufferoverrun/boolean.mli index 7a3351189..cead4ebbd 100644 --- a/infer/src/bufferoverrun/boolean.mli +++ b/infer/src/bufferoverrun/boolean.mli @@ -9,6 +9,8 @@ open! IStd type t = Bottom | False | True | Top +val of_bool : bool -> t + val equal : t -> t -> bool val is_false : t -> bool @@ -20,3 +22,27 @@ val not_ : t -> t val and_ : t -> t -> t val or_ : t -> t -> t + +module EqualOrder : sig + (** + This module provides abstract transfer functions for comparisons on unordered values, only based on equality, like abstract locations. +*) + + type b = t + + type t = {on_equal: b; on_not_equal: b} + + val eq : t + + val ne : t + + val strict_cmp : t + (** > or < *) + + val loose_cmp : t + (** >= or <= *) + + val top : t + + val of_equal : t -> b -> b +end diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 97cf98c6d..89ace8ffe 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -182,11 +182,26 @@ module Val = struct {bot with itv= f x.itv y.itv; traces= f_trace 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 -> Boolean.t) -> t -> t -> t = - fun f x y -> - let b = if has_pointer x || has_pointer y then Boolean.Top else f x.itv y.itv in + let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> t = + fun cmp_itv cmp_loc x y -> + let b = + match + ( x.itv + , PowLoc.is_bot x.powloc + , ArrayBlk.is_bot x.arrayblk + , y.itv + , PowLoc.is_bot y.powloc + , ArrayBlk.is_bot y.arrayblk ) + with + | NonBottom _, true, true, NonBottom _, true, true -> + cmp_itv x.itv y.itv + | Bottom, false, true, Bottom, false, true -> + PowLoc.lift_cmp cmp_loc x.powloc y.powloc + | Bottom, true, false, Bottom, true, false -> + ArrayBlk.lift_cmp_itv cmp_itv cmp_loc x.arrayblk y.arrayblk + | _ -> + Boolean.Top + in let itv = Itv.of_bool b in {bot with itv; traces= TraceSet.join x.traces y.traces} @@ -209,21 +224,21 @@ module Val = struct let band_sem = lift_itv Itv.band_sem - let lt_sem : t -> t -> t = lift_cmp_itv Itv.lt_sem + let lt_sem : t -> t -> t = lift_cmp_itv Itv.lt_sem Boolean.EqualOrder.strict_cmp - let gt_sem : t -> t -> t = lift_cmp_itv Itv.gt_sem + let gt_sem : t -> t -> t = lift_cmp_itv Itv.gt_sem Boolean.EqualOrder.strict_cmp - let le_sem : t -> t -> t = lift_cmp_itv Itv.le_sem + let le_sem : t -> t -> t = lift_cmp_itv Itv.le_sem Boolean.EqualOrder.loose_cmp - let ge_sem : t -> t -> t = lift_cmp_itv Itv.ge_sem + let ge_sem : t -> t -> t = lift_cmp_itv Itv.ge_sem Boolean.EqualOrder.loose_cmp - let eq_sem : t -> t -> t = lift_cmp_itv Itv.eq_sem + let eq_sem : t -> t -> t = lift_cmp_itv Itv.eq_sem Boolean.EqualOrder.eq - let ne_sem : t -> t -> t = lift_cmp_itv Itv.ne_sem + let ne_sem : t -> t -> t = lift_cmp_itv Itv.ne_sem Boolean.EqualOrder.ne - let land_sem : t -> t -> t = lift_cmp_itv Itv.land_sem + let land_sem : t -> t -> t = lift_cmp_itv Itv.land_sem Boolean.EqualOrder.top - let lor_sem : t -> t -> t = lift_cmp_itv Itv.lor_sem + let lor_sem : t -> t -> t = lift_cmp_itv Itv.lor_sem Boolean.EqualOrder.top (* TODO: get rid of those cases *) let warn_against_pruning_multiple_values : t -> t = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/global.c b/infer/tests/codetoanalyze/c/bufferoverrun/global.c index 7eb7b97ba..b0317757c 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/global.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/global.c @@ -16,12 +16,18 @@ const int global_const_zero = 0; enum { global_const = global_const_zero }; -void compare_global_const_enum_bad_FN() { +void compare_global_const_enum_Bad() { char arr[10]; if (global_const < 10) arr[10] = 1; } +void compare_global_const_enum_Good_FP() { + char arr[10]; + if (global_const > 10) + arr[10] = 1; +} + const int global_const_ten = 10; void use_global_const_ten_Good() { diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index a2b70337b..ec2d6794f 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -72,8 +72,8 @@ codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_ codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Call,Call,Parameter `x[*].field`,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Call,Call,Parameter `x[*].field`,Assignment,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 5] codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] -codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/global.c, use_global_const_ten_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] @@ -158,6 +158,8 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFE codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `FN_pointer_arith4_Bad` ] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ] codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Parameter `length`,,Parameter `length`,Array declaration,Array access: Offset: [-length + length + 1, length] Size: length] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c index b212b00a4..d735b5867 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -193,3 +193,37 @@ void nested_loop_prune_Good(int length) { } } } + +void bad_if_alias(int* x, int* y) { + char a[1]; + if (x == y) { + a[1] = 'A'; + } +} + +void call_bad_if_alias_Bad_AlreadyReported() { + int x; + bad_if_alias(x, x); +} + +void call_bad_if_alias_Good() { + int x, y; + bad_if_alias(x, y); +} + +void bad_if_not_alias(int* x, int* y) { + char a[1]; + if (x != y) { + a[1] = 'B'; + } +} + +void call_bad_if_not_alias_Good() { + int x; + bad_if_not_alias(x, x); +} + +void call_bad_if_not_alias_Bad_AlreadyReported() { + int x, y; + bad_if_not_alias(x, y); +} diff --git a/infer/tests/codetoanalyze/java/performance/Loops.java b/infer/tests/codetoanalyze/java/performance/Loops.java index c8e317c08..29d16e7f8 100644 --- a/infer/tests/codetoanalyze/java/performance/Loops.java +++ b/infer/tests/codetoanalyze/java/performance/Loops.java @@ -66,7 +66,7 @@ public class Loops { public float[] f; } - static boolean similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(C[] x, C[] y) { + static boolean similar(C[] x, C[] y) { if (x == null || y == null || x.length != y.length) { return false; } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 262d91968..c12605152 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -150,8 +150,10 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops. codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_SHOULD_NOT_REPORT_CONDITION_ALWAYS_TRUE_OR_FALSE(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + 33 ⋅ x.length.ub, degree = 1] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 33 ⋅ x.length.ub, degree = 1] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 14 + 33 ⋅ x.length.ub, degree = 1] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 13 + 33 ⋅ x.length.ub, degree = 1] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0] codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]