From ebddb142068d085997524494b8fa0cdb5a2626fc Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 14 Feb 2018 02:50:03 -0800 Subject: [PATCH] [inferbo] Prune by assert Summary: It prunes abstract memories on `assert` commands. Problem: Since the assert command is sometimes translated to two sequential `if` statments, it was not able to prune the memory precisely at `assert` commands in Inferbo---the pruned memory at the first branch was joined before the second branch. Solution: To avoid losing the pruning information at the first branch, now, it records which locations are pruned at the first branch and applies the same pruning at the next branch if they have semantically the same condition. Reviewed By: mbouaziz Differential Revision: D6895919 fbshipit-source-id: 15ac1cb --- .../src/bufferoverrun/bufferOverrunChecker.ml | 28 ++-- .../src/bufferoverrun/bufferOverrunDomain.ml | 144 +++++++++++++++++- .../bufferoverrun/bufferOverrunSemantics.ml | 82 +++++----- .../cpp/bufferoverrun/issues.exp | 2 + .../cpp/bufferoverrun/vector.cpp | 28 ++++ 5 files changed, 230 insertions(+), 54 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index c86a81378..e0f8559ce 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -204,19 +204,23 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let locs = Sem.eval exp1 mem |> Dom.Val.get_all_locs in let v = Sem.eval exp2 mem |> Dom.Val.add_trace_elem (Trace.Assign location) in let mem = Dom.Mem.update_mem locs v mem in - if PowLoc.is_singleton locs then - let loc_v = PowLoc.min_elt locs in - match Typ.Procname.get_method pname with - | "__inferbo_empty" when Loc.is_return loc_v -> ( - match Sem.get_formals pdesc with - | [(formal, _)] -> - let formal_v = Dom.Mem.find_heap (Loc.of_pvar formal) mem in - Dom.Mem.store_empty_alias formal_v loc_v exp2 mem + let mem = + if PowLoc.is_singleton locs then + let loc_v = PowLoc.min_elt locs in + match Typ.Procname.get_method pname with + | "__inferbo_empty" when Loc.is_return loc_v -> ( + match Sem.get_formals pdesc with + | [(formal, _)] -> + let formal_v = Dom.Mem.find_heap (Loc.of_pvar formal) mem in + Dom.Mem.store_empty_alias formal_v loc_v exp2 mem + | _ -> + assert false ) | _ -> - assert false ) - | _ -> - Dom.Mem.store_simple_alias loc_v exp2 mem - else mem + Dom.Mem.store_simple_alias loc_v exp2 mem + else mem + in + let mem = Dom.Mem.update_latest_prune exp1 exp2 mem in + mem | Prune (exp, _, _, _) -> Sem.prune exp mem | Call (ret, Const Cfun callee_pname, params, location, _) -> ( diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index df3664ffa..09c5538e0 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -49,6 +49,8 @@ module Val = struct && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk + let equal x y = phys_equal x y || ( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x + let widen ~prev ~next ~num_iters = if phys_equal prev next then prev else @@ -494,18 +496,102 @@ module Alias = struct fun temps a -> (AliasMap.remove_temps temps (fst a), snd a) end +module PrunePairs = struct + module PrunePair = struct + (* PrunePair.t is a pair of an abstract location and an abstract + value where the abstract location was updated with the abstract + value in the latest pruning. *) + type t = Loc.t * Val.t + + let equal ((l1, v1) as x) ((l2, v2) as y) = + phys_equal x y || Loc.equal l1 l2 && Val.equal v1 v2 + end + + type t = PrunePair.t list + + let empty = [] + + let equal x y = List.equal x y ~equal:PrunePair.equal +end + +module LatestPrune = struct + (* Latest p: The pruned pairs 'p' has pruning information (which + abstract locations are updated by which abstract values) in the + latest pruning. + + TrueBranch (x, p): After a pruning, the variable 'x' is assigned + by 1. There is no other memory updates after the latest pruning. + + FalseBranch (x, p): After a pruning, the variable 'x' is assigned + by 0. There is no other memory updates after the latest pruning. + + V (x, ptrue, pfalse): After two non-sequential prunings ('ptrue' + and 'pfalse'), the variable 'x' is assigned by 1 and 0, + respectively. There is no other memory updates after the latest + prunings. + + Top: No information about the latest pruning. *) + type astate = + | Latest of PrunePairs.t + | TrueBranch of Pvar.t * PrunePairs.t + | FalseBranch of Pvar.t * PrunePairs.t + | V of Pvar.t * PrunePairs.t * PrunePairs.t + | Top + + let ( <= ) ~lhs ~rhs = + if phys_equal lhs rhs then true + else + match (lhs, rhs) with + | _, Top -> + true + | Top, _ -> + false + | Latest p1, Latest p2 -> + PrunePairs.equal p1 p2 + | TrueBranch (x1, p1), TrueBranch (x2, p2) + | FalseBranch (x1, p1), FalseBranch (x2, p2) + | TrueBranch (x1, p1), V (x2, p2, _) + | FalseBranch (x1, p1), V (x2, _, p2) -> + Pvar.equal x1 x2 && PrunePairs.equal p1 p2 + | V (x1, ptrue1, pfalse1), V (x2, ptrue2, pfalse2) -> + Pvar.equal x1 x2 && PrunePairs.equal ptrue1 ptrue2 && PrunePairs.equal pfalse1 pfalse2 + | _, _ -> + false + + + let join x y = + match (x, y) with + | _, _ when ( <= ) ~lhs:x ~rhs:y -> + y + | _, _ when ( <= ) ~lhs:y ~rhs:x -> + x + | FalseBranch (x', pfalse), TrueBranch (y', ptrue) + | TrueBranch (x', ptrue), FalseBranch (y', pfalse) + when Pvar.equal x' y' -> + V (x', ptrue, pfalse) + | _, _ -> + Top + + + let widen ~prev ~next ~num_iters:_ = join prev next + + let top = Top +end + module MemReach = struct - type astate = {stack: Stack.astate; heap: Heap.astate; alias: Alias.astate} + type astate = + {stack: Stack.astate; heap: Heap.astate; alias: Alias.astate; latest_prune: LatestPrune.astate} type t = astate - let bot : t = {stack= Stack.bot; heap= Heap.bot; alias= Alias.bot} + let init : t = {stack= Stack.bot; heap= Heap.bot; alias= Alias.bot; latest_prune= LatestPrune.top} let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else Stack.( <= ) ~lhs:lhs.stack ~rhs:rhs.stack && Heap.( <= ) ~lhs:lhs.heap ~rhs:rhs.heap && Alias.( <= ) ~lhs:lhs.alias ~rhs:rhs.alias + && LatestPrune.( <= ) ~lhs:lhs.latest_prune ~rhs:rhs.latest_prune let widen ~prev ~next ~num_iters = @@ -513,14 +599,17 @@ module MemReach = struct else { stack= Stack.widen ~prev:prev.stack ~next:next.stack ~num_iters ; heap= Heap.widen ~prev:prev.heap ~next:next.heap ~num_iters - ; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters } + ; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters + ; latest_prune= LatestPrune.widen ~prev:prev.latest_prune ~next:next.latest_prune ~num_iters + } let join : t -> t -> t = fun x y -> { stack= Stack.join x.stack y.stack ; heap= Heap.join x.heap y.heap - ; alias= Alias.join x.alias y.alias } + ; alias= Alias.join x.alias y.alias + ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune } let pp : F.formatter -> t -> unit = @@ -617,6 +706,36 @@ module MemReach = struct let remove_temps : Ident.t list -> t -> t = fun temps m -> {m with stack= Stack.remove_temps temps m.stack; alias= Alias.remove_temps temps m.alias} + + + let set_prune_pairs : PrunePairs.t -> t -> t = + fun prune_pairs m -> {m with latest_prune= LatestPrune.Latest prune_pairs} + + + let apply_latest_prune : Exp.t -> t -> t = + fun e m -> + match (m.latest_prune, e) with + | LatestPrune.V (x, prunes, _), Exp.Var r + | LatestPrune.V (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) -> ( + match find_simple_alias r m with + | Some Loc.Var Var.ProgramVar y when Pvar.equal x y -> + List.fold_left prunes ~init:m ~f:(fun acc (l, v) -> + update_mem (PowLoc.singleton l) v acc ) + | _ -> + m ) + | _ -> + m + + + let update_latest_prune : Exp.t -> Exp.t -> t -> t = + fun e1 e2 m -> + match (e1, e2, m.latest_prune) with + | Lvar x, Const Const.Cint i, LatestPrune.Latest p -> + if IntLit.isone i then {m with latest_prune= LatestPrune.TrueBranch (x, p)} + else if IntLit.iszero i then {m with latest_prune= LatestPrune.FalseBranch (x, p)} + else {m with latest_prune= LatestPrune.Top} + | _, _, _ -> + {m with latest_prune= LatestPrune.Top} end module Mem = struct @@ -626,7 +745,7 @@ module Mem = struct let bot : t = Bottom - let init : t = NonBottom MemReach.bot + let init : t = NonBottom MemReach.init let f_lift_default : 'a -> (MemReach.t -> 'a) -> t -> 'a = fun default f m -> match m with Bottom -> default | NonBottom m' -> f m' @@ -706,6 +825,21 @@ module Mem = struct let remove_temps : Ident.t list -> t -> t = fun temps -> f_lift (MemReach.remove_temps temps) + + let set_prune_pairs : PrunePairs.t -> t -> t = + fun prune_pairs -> f_lift (MemReach.set_prune_pairs prune_pairs) + + + let apply_latest_prune : Exp.t -> t -> t = fun e -> f_lift (MemReach.apply_latest_prune e) + + let update_latest_prune : Exp.t -> Exp.t -> t -> t = + fun e1 e2 -> f_lift (MemReach.update_latest_prune e1 e2) + + + let update_mem_in_prune : PrunePairs.t ref -> Loc.t -> Val.t -> t -> t = + fun prune_pairs lv v m -> + prune_pairs := (lv, v) :: !prune_pairs ; + update_mem (PowLoc.singleton lv) v m end module Summary = struct diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index d2aadf762..577f96a86 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -326,20 +326,20 @@ module Make (CFG : ProcCfg.S) = struct ArrayBlk.make allocsite offset size stride |> Val.of_array_blk - let prune_unop : Exp.t -> Mem.astate -> Mem.astate = - fun e mem -> + let prune_unop : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate = + fun prune_pairs e mem -> match e with | Exp.Var x -> ( match Mem.find_alias x mem with | Some AliasTarget.Simple lv -> let v = Mem.find_heap lv mem in let v' = Val.prune_zero v in - Mem.update_mem (PowLoc.singleton lv) v' mem + Mem.update_mem_in_prune prune_pairs lv v' mem | Some AliasTarget.Empty lv -> let v = Mem.find_heap lv mem in let itv_v = Itv.prune_eq (Val.get_itv v) Itv.zero in let v' = Val.modify_itv itv_v v in - Mem.update_mem (PowLoc.singleton lv) v' mem + Mem.update_mem_in_prune prune_pairs lv v' mem | None -> mem ) | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> ( @@ -348,20 +348,20 @@ module Make (CFG : ProcCfg.S) = struct let v = Mem.find_heap lv mem in let itv_v = Itv.prune_eq (Val.get_itv v) Itv.false_sem in let v' = Val.modify_itv itv_v v in - Mem.update_mem (PowLoc.singleton lv) v' mem + Mem.update_mem_in_prune prune_pairs lv v' mem | Some AliasTarget.Empty lv -> let v = Mem.find_heap lv mem in let itv_v = Itv.prune_comp Binop.Ge (Val.get_itv v) Itv.one in let v' = Val.modify_itv itv_v v in - Mem.update_mem (PowLoc.singleton lv) v' mem + Mem.update_mem_in_prune prune_pairs lv v' mem | None -> mem ) | _ -> mem - let prune_binop_left : Exp.t -> Mem.astate -> Mem.astate = - fun e mem -> + let prune_binop_left : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate = + fun prune_pairs e mem -> match e with | Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e') | Exp.BinOp ((Binop.Gt as comp), Exp.Var x, e') @@ -371,7 +371,7 @@ module Make (CFG : ProcCfg.S) = struct | Some lv -> let v = Mem.find_heap lv mem in let v' = Val.prune_comp comp v (eval e' mem) in - Mem.update_mem (PowLoc.singleton lv) v' mem + Mem.update_mem_in_prune prune_pairs lv v' mem | None -> mem ) | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> ( @@ -379,7 +379,7 @@ module Make (CFG : ProcCfg.S) = struct | Some lv -> let v = Mem.find_heap lv mem in let v' = Val.prune_eq v (eval e' mem) in - Mem.update_mem (PowLoc.singleton lv) v' mem + Mem.update_mem_in_prune prune_pairs lv v' mem | None -> mem ) | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> ( @@ -387,15 +387,15 @@ module Make (CFG : ProcCfg.S) = struct | Some lv -> let v = Mem.find_heap lv mem in let v' = Val.prune_ne v (eval e' mem) in - Mem.update_mem (PowLoc.singleton lv) v' mem + Mem.update_mem_in_prune prune_pairs lv v' mem | None -> mem ) | _ -> mem - let prune_binop_right : Exp.t -> Mem.astate -> Mem.astate = - fun e mem -> + let prune_binop_right : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate = + fun prune_pairs e mem -> match e with | Exp.BinOp ((Binop.Lt as c), e', Exp.Var x) | Exp.BinOp ((Binop.Gt as c), e', Exp.Var x) @@ -403,7 +403,7 @@ module Make (CFG : ProcCfg.S) = struct | Exp.BinOp ((Binop.Ge as c), e', Exp.Var x) | Exp.BinOp ((Binop.Eq as c), e', Exp.Var x) | Exp.BinOp ((Binop.Ne as c), e', Exp.Var x) -> - prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) mem + prune_binop_left prune_pairs (Exp.BinOp (comp_rev c, Exp.Var x, e')) mem | _ -> mem @@ -416,31 +416,39 @@ module Make (CFG : ProcCfg.S) = struct fun e mem -> if is_unreachable_constant e mem then Mem.bot else mem - let rec prune : Exp.t -> Mem.astate -> Mem.astate = + let prune : Exp.t -> Mem.astate -> Mem.astate = fun e mem -> - let mem = - mem |> prune_unreachable e |> prune_unop e |> prune_binop_left e |> prune_binop_right e + let prune_pairs = ref PrunePairs.empty in + let rec prune_helper e mem = + let mem = + mem |> prune_unreachable e |> prune_unop prune_pairs e |> prune_binop_left prune_pairs e + |> prune_binop_right prune_pairs e + in + match e with + | Exp.BinOp (Binop.Ne, e, Exp.Const Const.Cint i) when IntLit.iszero i -> + prune_helper e mem + | Exp.BinOp (Binop.Eq, e, Exp.Const Const.Cint i) when IntLit.iszero i -> + prune_helper (Exp.UnOp (Unop.LNot, e, None)) mem + | Exp.UnOp (Unop.Neg, Exp.Var x, _) -> + prune_helper (Exp.Var x) mem + | Exp.BinOp (Binop.LAnd, e1, e2) -> + mem |> prune_helper e1 |> prune_helper e2 + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> + mem |> prune_helper (Exp.UnOp (Unop.LNot, e1, t)) + |> prune_helper (Exp.UnOp (Unop.LNot, e2, t)) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Lt as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Gt as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Le as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ge as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Eq as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ne as c), e1, e2), _) -> + prune_helper (Exp.BinOp (comp_not c, e1, e2)) mem + | _ -> + mem in - match e with - | Exp.BinOp (Binop.Ne, e, Exp.Const Const.Cint i) when IntLit.iszero i -> - prune e mem - | Exp.BinOp (Binop.Eq, e, Exp.Const Const.Cint i) when IntLit.iszero i -> - prune (Exp.UnOp (Unop.LNot, e, None)) mem - | Exp.UnOp (Unop.Neg, Exp.Var x, _) -> - prune (Exp.Var x) mem - | Exp.BinOp (Binop.LAnd, e1, e2) -> - mem |> prune e1 |> prune e2 - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> - mem |> prune (Exp.UnOp (Unop.LNot, e1, t)) |> prune (Exp.UnOp (Unop.LNot, e2, t)) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Lt as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Gt as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Le as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ge as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Eq as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ne as c), e1, e2), _) -> - prune (Exp.BinOp (comp_not c, e1, e2)) mem - | _ -> - mem + let mem = Mem.apply_latest_prune e mem in + let mem = prune_helper e mem in + Mem.set_prune_pairs !prune_pairs mem let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list = diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index e19f30405..c9fe4ea75 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -17,6 +17,8 @@ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_ codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]] codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [42, 42] Size: [42, 42]] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [6, 6] Size: [5, 5]] +codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, [Call,Call,Assignment,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [4, 4] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L1, [Call,Call,Assignment,Call,Call,ArrayDeclaration,Assignment,Assignment,Return,Assignment,Assignment,Return,Assignment,Assignment,ArrayAccess: Offset: [10, 10] Size: [5, 5]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_L5, [Call,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_L3, [Call,Call,Call,Assignment,Call,Call,Call,Call,Call,ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, +oo]] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp index b77a43d0c..b19b13156 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/vector.cpp @@ -8,6 +8,7 @@ */ #include #include +#include void out_of_bound_Bad(std::vector v) { unsigned int n = v.size(); @@ -156,3 +157,30 @@ void data_Bad() { p[4] = 10; p[v[4]] = 1; } + +void assert_Good() { + std::vector v; + for (int i = 0; i < 5; i++) { + v.push_back(1); + } + assert(v.size() == 5); + v[4] = 1; +} + +void assert_Good_FP(int x) { + std::vector v; + for (int i = 0; i < 5; i++) { + v.push_back(1); + } + assert(((v.size() == 5) ? 1 : 0) ? 1 : 0); + v[4] = 1; +} + +void assert_Bad() { + std::vector v; + for (int i = 0; i < 5; i++) { + v.push_back(1); + } + assert(v.size() == 5); + v[6] = 1; +}