From 1bcdc6e7615d0185a34876da0e91e9b4ed22266f Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 23 Jan 2019 06:34:03 -0800 Subject: [PATCH] [inferbo] Extend conditional proof obligation for inequalities Summary: This diff extends the abstract domain to keep binary conditions on prunings, so Inferbo can suppress more proof obligations (i.e., false positives) that are known to be unreachable according to the binary conditions. Depends on D13729600 Reviewed By: mbouaziz Differential Revision: D13749914 fbshipit-source-id: 314f048f1 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 178 +++++++++++++++--- .../bufferoverrun/bufferOverrunSemantics.ml | 28 +-- .../codetoanalyze/c/bufferoverrun/arith.c | 2 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 3 - .../c/bufferoverrun/prune_alias.c | 2 +- .../codetoanalyze/c/bufferoverrun/relation.c | 2 +- .../conditional_proof_obligation.cpp | 75 +++++++- .../cpp/bufferoverrun/issues.exp | 10 +- .../cpp/bufferoverrun/relation.cpp | 6 +- 9 files changed, 252 insertions(+), 54 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b4f15db5a..ae7c843b8 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -724,11 +724,145 @@ module Alias = struct let remove_temp : Ident.t -> t -> t = fun temp -> lift_map (AliasMap.remove temp) end +module CoreVal = struct + type t = Val.t + + let compare x y = + let r = Itv.compare (Val.get_itv x) (Val.get_itv y) in + if r <> 0 then r else ArrayBlk.compare (Val.get_array_blk x) (Val.get_array_blk y) + + + let pp fmt x = F.fprintf fmt "(%a, %a)" Itv.pp (Val.get_itv x) ArrayBlk.pp (Val.get_array_blk x) + + let is_symbolic v = Itv.is_symbolic (Val.get_itv v) || ArrayBlk.is_symbolic (Val.get_array_blk v) + + let is_empty v = Itv.is_empty (Val.get_itv v) && ArrayBlk.is_empty (Val.get_array_blk v) +end + +module PruningExp = struct + type t = Unknown | Binop of {bop: Binop.t; lhs: CoreVal.t; rhs: CoreVal.t} [@@deriving compare] + + let ( <= ) ~lhs ~rhs = + match (lhs, rhs) with + | _, Unknown -> + true + | Unknown, _ -> + false + | Binop {bop= bop1; lhs= lhs1; rhs= rhs1}, Binop {bop= bop2; lhs= lhs2; rhs= rhs2} -> + Binop.equal bop1 bop2 && Val.( <= ) ~lhs:lhs1 ~rhs:lhs2 && Val.( <= ) ~lhs:rhs1 ~rhs:rhs2 + + + let join x y = + match (x, y) with + | Binop {bop= bop1; lhs= lhs1; rhs= rhs1}, Binop {bop= bop2; lhs= lhs2; rhs= rhs2} + when Binop.equal bop1 bop2 -> + Binop {bop= bop1; lhs= Val.join lhs1 lhs2; rhs= Val.join rhs1 rhs2} + | _, _ -> + Unknown + + + let widen ~prev ~next ~num_iters = + match (prev, next) with + | Binop {bop= bop1; lhs= lhs1; rhs= rhs1}, Binop {bop= bop2; lhs= lhs2; rhs= rhs2} + when Binop.equal bop1 bop2 -> + Binop + { bop= bop1 + ; lhs= Val.widen ~prev:lhs1 ~next:lhs2 ~num_iters + ; rhs= Val.widen ~prev:rhs1 ~next:rhs2 ~num_iters } + | _, _ -> + Unknown + + + let pp fmt x = + match x with + | Unknown -> + F.pp_print_string fmt "Unknown" + | Binop {bop; lhs; rhs} -> + F.fprintf fmt "(%a %s %a)" CoreVal.pp lhs (Binop.str Pp.text bop) CoreVal.pp rhs + + + let make bop ~lhs ~rhs = Binop {bop; lhs; rhs} + + let is_unknown = function Unknown -> true | Binop _ -> false + + let is_symbolic = function + | Unknown -> + false + | Binop {lhs; rhs} -> + CoreVal.is_symbolic lhs || CoreVal.is_symbolic rhs + + + let is_empty = + let le_false v = Itv.( <= ) ~lhs:(Val.get_itv v) ~rhs:Itv.zero in + function + | Unknown -> + false + | Binop {bop= Lt; lhs; rhs} -> + le_false (Val.lt_sem lhs rhs) + | Binop {bop= Gt; lhs; rhs} -> + le_false (Val.gt_sem lhs rhs) + | Binop {bop= Le; lhs; rhs} -> + le_false (Val.le_sem lhs rhs) + | Binop {bop= Ge; lhs; rhs} -> + le_false (Val.ge_sem lhs rhs) + | Binop {bop= Eq; lhs; rhs} -> + le_false (Val.eq_sem lhs rhs) + | Binop {bop= Ne; lhs; rhs} -> + le_false (Val.ne_sem lhs rhs) + | Binop _ -> + assert false + + + let subst x eval_sym_trace location = + match x with + | Unknown -> + Unknown + | Binop {bop; lhs; rhs} -> + Binop + { bop + ; lhs= Val.subst lhs eval_sym_trace location + ; rhs= Val.subst rhs eval_sym_trace location } +end + +module PrunedVal = struct + type t = {v: CoreVal.t; pruning_exp: PruningExp.t} [@@deriving compare] + + let ( <= ) ~lhs ~rhs = + Val.( <= ) ~lhs:lhs.v ~rhs:rhs.v && PruningExp.( <= ) ~lhs:lhs.pruning_exp ~rhs:rhs.pruning_exp + + + let join x y = {v= Val.join x.v y.v; pruning_exp= PruningExp.join x.pruning_exp y.pruning_exp} + + let widen ~prev ~next ~num_iters = + { v= Val.widen ~prev:prev.v ~next:next.v ~num_iters + ; pruning_exp= PruningExp.widen ~prev:prev.pruning_exp ~next:next.pruning_exp ~num_iters } + + + let pp fmt x = + CoreVal.pp fmt x.v ; + if not (PruningExp.is_unknown x.pruning_exp) then + F.fprintf fmt " by %a" PruningExp.pp x.pruning_exp + + + let make v pruning_exp = {v; pruning_exp} + + let get_val x = x.v + + let subst {v; pruning_exp} eval_sym_trace location = + { v= Val.subst v eval_sym_trace location + ; pruning_exp= PruningExp.subst pruning_exp eval_sym_trace location } + + + let is_symbolic {v; pruning_exp} = CoreVal.is_symbolic v || PruningExp.is_symbolic pruning_exp + + let is_empty {v; pruning_exp} = CoreVal.is_empty v || PruningExp.is_empty pruning_exp +end + (* [PrunePairs] is a map from abstract locations to abstract values that represents pruned results in the latest pruning. It uses [InvertedMap] because more pruning means smaller abstract states. *) module PrunePairs = struct - include AbstractDomain.InvertedMap (Loc) (Val) + include AbstractDomain.InvertedMap (Loc) (PrunedVal) let forget locs x = filter (fun l _ -> not (PowLoc.mem l locs)) x end @@ -846,21 +980,6 @@ module LatestPrune = struct end module Reachability = struct - module PrunedVal = struct - type t = Val.t - - let compare x y = - let r = Itv.compare (Val.get_itv x) (Val.get_itv y) in - if r <> 0 then r else ArrayBlk.compare (Val.get_array_blk x) (Val.get_array_blk y) - - - let pp = Val.pp - - let is_symbolic : t -> bool = fun x -> Itv.is_symbolic x.itv || ArrayBlk.is_symbolic x.arrayblk - - let is_empty v = Itv.is_empty (Val.get_itv v) && ArrayBlk.is_empty (Val.get_array_blk v) - end - module M = PrettyPrintable.MakePPSet (PrunedVal) type t = M.t @@ -871,9 +990,9 @@ module Reachability = struct reachability. *) let add v x = if PrunedVal.is_symbolic v then M.add v x else x - let make = + let make latest_prune = let of_prune_pairs p = PrunePairs.fold (fun _ v acc -> add v acc) p M.empty in - function + match latest_prune with | LatestPrune.Latest p | LatestPrune.TrueBranch (_, p) | LatestPrune.FalseBranch (_, p) -> of_prune_pairs p | LatestPrune.V (_, ptrue, pfalse) -> @@ -885,7 +1004,7 @@ module Reachability = struct let subst x eval_sym_trace location = let exception Unreachable in let subst1 x acc = - let v = Val.subst x eval_sym_trace location in + let v = PrunedVal.subst x eval_sym_trace location in if PrunedVal.is_empty v then raise Unreachable else add v acc in match M.fold subst1 x M.empty with x -> `Reachable x | exception Unreachable -> `Unreachable @@ -1089,17 +1208,18 @@ module MemReach = struct 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 -> - PrunePairs.fold (fun l v acc -> update_mem (PowLoc.singleton l) v acc) prunes m + 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 + | 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 -> + PrunePairs.fold apply1 prunes m + | _ -> + m ) | _ -> - m ) - | _ -> - m + m let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t = diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 21f9e6577..0d354fc6e 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -446,8 +446,8 @@ let get_size_sym_f integer_type_widths mem e = Val.get_size_sym (eval integer_ty module Prune = struct type t = {prune_pairs: PrunePairs.t; mem: Mem.t} - let update_mem_in_prune lv v {prune_pairs; mem} = - let prune_pairs = PrunePairs.add lv v prune_pairs in + let update_mem_in_prune lv v ?(pruning_exp = PruningExp.Unknown) {prune_pairs; mem} = + let prune_pairs = PrunePairs.add lv (PrunedVal.make v pruning_exp) prune_pairs in let mem = Mem.update_mem (PowLoc.singleton lv) v mem in {prune_pairs; mem} @@ -503,25 +503,31 @@ module Prune = struct | Exp.BinOp ((Binop.Ge as comp), Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with | Some lv -> - let v = Mem.find lv mem in - let v' = Val.prune_comp comp v (eval integer_type_widths e' mem) in - update_mem_in_prune lv v' astate + let lhs = Mem.find lv mem in + let rhs = eval integer_type_widths e' mem in + let v = Val.prune_comp comp lhs rhs in + let pruning_exp = PruningExp.make comp ~lhs ~rhs in + update_mem_in_prune lv v ~pruning_exp astate | None -> astate ) | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with | Some lv -> - let v = Mem.find lv mem in - let v' = Val.prune_eq v (eval integer_type_widths e' mem) in - update_mem_in_prune lv v' astate + let lhs = Mem.find lv mem in + let rhs = eval integer_type_widths e' mem in + let v = Val.prune_eq lhs rhs in + let pruning_exp = PruningExp.make Binop.Eq ~lhs ~rhs in + update_mem_in_prune lv v ~pruning_exp astate | None -> astate ) | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> ( match Mem.find_simple_alias x mem with | Some lv -> - let v = Mem.find lv mem in - let v' = Val.prune_ne v (eval integer_type_widths e' mem) in - update_mem_in_prune lv v' astate + let lhs = Mem.find lv mem in + let rhs = eval integer_type_widths e' mem in + let v = Val.prune_ne lhs rhs in + let pruning_exp = PruningExp.make Binop.Ne ~lhs ~rhs in + update_mem_in_prune lv v ~pruning_exp astate | None -> astate ) | Exp.BinOp diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c index d4a393603..6be3b9b6e 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/arith.c @@ -263,7 +263,7 @@ void unsigned_prune_ge1_Good(unsigned int x, unsigned int y) { } } -void call_unsigned_prune_ge1_Good_FP() { unsigned_prune_ge1_Good(0, 1); } +void call_unsigned_prune_ge1_Good() { unsigned_prune_ge1_Good(0, 1); } void unsigned_prune_ge2_Good(unsigned int x, unsigned int y) { if (y > 0) { diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 5d6acc2d3..695fff658 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -10,7 +10,6 @@ codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex2_Good_FP, 2, INTEGER_OVERFL codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,,Parameter `*cp`,Array access: Offset: [0, +oo] Size: 2 by call to `scan_hex_Good` ] codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `*cp`,Assignment,Binary operation: (0 - 48):unsigned64 by call to `scan_hex_Good` ] codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,,Call,Assignment,Assignment,,Parameter `s`,Binary operation: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ] -codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Parameter `y`,Binary operation: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ] codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Parameter `n`,Assignment,,Array declaration,Array access: Offset: [-oo, +oo] Size: 1] codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 2 Size: 2] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: (2000000000 + 2000000000):signed32] @@ -220,7 +219,6 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 2, BUFFE codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `x`,,Array declaration,Array access: Offset: 10 (⇐ x + -x + 10) Size: 5] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith5_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,Assignment,,Array declaration,Array access: Offset: [4, 2044] (⇐ [0, 1020] + [4, 1024]) Size: 1024] 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_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_eq_CAF` ] 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] @@ -263,7 +261,6 @@ codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, COND codetoanalyze/c/bufferoverrun/relation.c, FP_array_access2_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 1] codetoanalyze/c/bufferoverrun/relation.c, FP_array_access3_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 1] codetoanalyze/c/bufferoverrun/relation.c, FP_array_access4_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 3 Size: 1] -codetoanalyze/c/bufferoverrun/relation.c, FP_call_array_access_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: -1 Size: 1 by call to `array_access_Ok` ] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 0] codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 5, CONDITION_ALWAYS_TRUE, 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 6ca0a46bf..cb2b3635c 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -142,7 +142,7 @@ void prune_arrblk_eq_CAF(int* x) { } } -void FP_call_prune_arrblk_eq_Ok() { +void call_prune_arrblk_eq_Ok() { int* x = (int*)malloc(sizeof(int) * 5); prune_arrblk_eq_CAF(x); } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/relation.c b/infer/tests/codetoanalyze/c/bufferoverrun/relation.c index 0b3d5af36..2eafffbd2 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/relation.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/relation.c @@ -11,7 +11,7 @@ void array_access_Ok(int x, int y) { } } -void FP_call_array_access_Ok() { array_access_Ok(0, 0); } +void call_array_access_Ok() { array_access_Ok(0, 0); } void FP_array_access2_Ok(int x, int y) { int a[1]; diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp index 07ab1c7ca..7054f19e9 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp @@ -126,6 +126,79 @@ void conditional_inequality(int idx) { } } -void call_conditional_inequality_Good_FP() { conditional_inequality(5); } +void call_conditional_inequality_Good() { conditional_inequality(5); } void call_conditional_inequality_Bad() { conditional_inequality(6); } + +void conditional_inequality_join1(int idx) { + int a[5]; + if (idx == 5) { + } else { + // pruning exp is "idx != 5" + L: + // joined pruning exp is "Unknown" + a[idx] = 0; + } + + if (idx == 6) { + // pruning exp is "idx == 6" + goto L; + } +} + +void call_conditional_inequality_join1_Good_FP() { + conditional_inequality_join1(5); +} + +void call_conditional_inequality_join1_Bad() { + conditional_inequality_join1(6); +} + +void conditional_inequality_join2(int idx) { + int a[5]; + if (idx == 5) { + } else { + // pruning exp is "idx != 5" + L: + // joined pruning exp is "idx != [5, 6]" + a[idx] = 0; + } + + if (idx != 6) { + // pruning exp is "idx != 6" + goto L; + } +} + +void call_conditional_inequality_join2_1_Bad() { + conditional_inequality_join2(5); +} + +void call_conditional_inequality_join2_2_Bad() { + conditional_inequality_join2(6); +} + +void conditional_inequality_depth2(int i) { + int a[5]; + if (i != 1) { + a[i] = 0; + } +} + +void conditional_inequality_depth1(int i) { + if (i != 5) { + conditional_inequality_depth2(i); + } +} + +void call_conditional_inequality_depth1_1_Good_FP() { + conditional_inequality_depth1(5); +} + +void call_conditional_inequality_depth1_2_Good() { + conditional_inequality_depth1(1); +} + +void call_conditional_inequality_depth1_3_Bad() { + conditional_inequality_depth1(6); +} diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 57f34b2be..cbec7b353 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -36,7 +36,12 @@ codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `size`,,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `*ptr`,Assignment,Assignment,Array access: Offset: 2 Size: 1 by call to `conditional_buffer_access` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality` ] -codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_Good_FP, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_depth1_1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `i`,Call,,Parameter `i`,,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality_depth1` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_depth1_3_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Parameter `i`,Call,,Parameter `i`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_depth1` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join1_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_join1` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join1_Good_FP, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality_join1` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join2_1_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 5 Size: 5 by call to `conditional_inequality_join2` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join2_2_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_join2` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ] codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]] @@ -53,9 +58,6 @@ codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFF codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call1_loop_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,,Parameter `*arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ] -codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call2_minus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: 8 Size: 5 by call to `minus_params_Ok` ] -codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params2_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: -1 Size: 5 by call to `plus_params2` ] -codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `x`,,Array declaration,Array access: Offset: -1 Size: 5 by call to `plus_params` ] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_id_Ok, 4, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Assignment,,Assignment,Call,Assignment,Assignment,Array declaration,Assignment,Array access: Offset: 5 Size: [0, 6]] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*data`,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*data`,Assignment,Array access: Offset: [0, +oo] Size: 1 by call to `loop_with_type_casting` ] diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp index 6a51f4eec..97b7d8e3b 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/relation.cpp @@ -15,7 +15,7 @@ void minus_params_Ok(int x, int y) { void call1_minus_params_Ok() { minus_params_Ok(5, 2); } -void FP_call2_minus_params_Ok() { minus_params_Ok(10, 2); } +void call2_minus_params_Ok() { minus_params_Ok(10, 2); } void plus_params(int x, int y) { int a[5]; @@ -28,7 +28,7 @@ void call1_plus_params_Ok() { plus_params(1, 2); } void call2_plus_params_Bad() { plus_params(10, 2); } -void FP_call3_plus_params_Ok() { plus_params(0, 0); } +void call3_plus_params_Ok() { plus_params(0, 0); } void plus_params2(int x, int y) { int a[5]; @@ -41,7 +41,7 @@ void call1_plus_params2_Ok() { plus_params2(1, 2); } void call2_plus_params2_Bad() { plus_params2(10, 2); } -void FP_call3_plus_params2_Ok() { plus_params2(0, 0); } +void call3_plus_params2_Ok() { plus_params2(0, 0); } void loop(char* arr, int len) { while (len > 0) {