From 5762c47ef244b30a14351adeb6342cc905890054 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 27 Mar 2019 19:38:24 -0700 Subject: [PATCH] [inferbo] Accumulate LatestPrune in sequential prunings Summary: This diff accumulates LatestPrune in sequential prunings. It should be sound since Inferbo invalidates some data of LatestPrune if they are updated. Depends on D14321534 Reviewed By: mbouaziz Differential Revision: D14321575 fbshipit-source-id: 233dbae32 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 19 +++++++++++++------ .../bufferoverrun/bufferOverrunSemantics.ml | 6 ++---- .../cpp/bufferoverrun/issues.exp | 4 +--- .../cpp/bufferoverrun/vector.cpp | 2 +- 4 files changed, 17 insertions(+), 14 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index e4c23a532..0846594ea 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -1342,7 +1342,7 @@ module MemReach = struct fun prune_pairs m -> {m with latest_prune= LatestPrune.Latest prune_pairs} - let apply_latest_prune : Exp.t -> t -> t = + let apply_latest_prune : Exp.t -> t -> t * PrunePairs.t = let apply1 l v acc = update_mem (PowLoc.singleton l) (PrunedVal.get_val v) acc in fun e m -> match (m.latest_prune, e) with @@ -1350,11 +1350,11 @@ module MemReach = struct | LatestPrune.V (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) -> ( match find_simple_alias r m with | Some (Loc.Var (Var.ProgramVar y), None) when Pvar.equal x y -> - PrunePairs.fold apply1 prunes m + (PrunePairs.fold apply1 prunes m, prunes) | _ -> - m ) + (m, PrunePairs.empty) ) | _ -> - m + (m, PrunePairs.empty) let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t = @@ -1563,14 +1563,21 @@ module Mem = struct fun prune_pairs -> map ~f:(MemReach.set_prune_pairs prune_pairs) - let apply_latest_prune : Exp.t -> t -> t = fun e -> map ~f:(MemReach.apply_latest_prune e) + let apply_latest_prune : Exp.t -> t -> t * PrunePairs.t = + fun e -> function + | Bottom -> + (Bottom, PrunePairs.empty) + | NonBottom m -> + let m, prune_pairs = MemReach.apply_latest_prune e m in + (NonBottom m, prune_pairs) + let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t = fun ~updated_locs e1 e2 -> map ~f:(MemReach.update_latest_prune ~updated_locs e1 e2) let get_latest_prune : t -> LatestPrune.t = - f_lift_default ~default:LatestPrune.Top MemReach.get_latest_prune + fun m -> f_lift_default ~default:LatestPrune.Top MemReach.get_latest_prune m let get_relation : t -> Relation.t = diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 5976030aa..141342039 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -657,14 +657,12 @@ module Prune = struct let prune : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Mem.t = fun integer_type_widths e mem -> - let mem = Mem.apply_latest_prune e mem in + let mem, prune_pairs = Mem.apply_latest_prune e mem in let mem = let constrs = Relation.Constraints.of_exp e ~get_sym_f:(get_sym_f integer_type_widths mem) in Mem.meet_constraints constrs mem in - let {mem; prune_pairs} = - prune_helper integer_type_widths e {mem; prune_pairs= PrunePairs.empty} - in + let {mem; prune_pairs} = prune_helper integer_type_widths e {mem; prune_pairs} in Mem.set_prune_pairs prune_pairs mem end diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 0f4917ed3..333842e7e 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -118,9 +118,7 @@ codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_b codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5] codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `__n`,Call,,Parameter `index`,,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]] -codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_2, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Unknown value from: std::distance_>,Assignment,Call,,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Unknown value from: std::distance_>,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,,Parameter `this->infer_size`,,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp index 4d8c90853..7613da08b 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp @@ -165,7 +165,7 @@ void assert_Good() { v[4] = 1; } -void assert_Good_FP(int x) { +void assert_Good_2(int x) { std::vector v; for (int i = 0; i < 5; i++) { v.push_back(1);