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; +}