[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
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 3fc4ccbc14
commit 1bcdc6e761

@ -724,11 +724,145 @@ module Alias = struct
let remove_temp : Ident.t -> t -> t = fun temp -> lift_map (AliasMap.remove temp) let remove_temp : Ident.t -> t -> t = fun temp -> lift_map (AliasMap.remove temp)
end 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 (* [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 in the latest pruning. It uses [InvertedMap] because more pruning means smaller abstract
states. *) states. *)
module PrunePairs = struct 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 let forget locs x = filter (fun l _ -> not (PowLoc.mem l locs)) x
end end
@ -846,21 +980,6 @@ module LatestPrune = struct
end end
module Reachability = struct 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) module M = PrettyPrintable.MakePPSet (PrunedVal)
type t = M.t type t = M.t
@ -871,9 +990,9 @@ module Reachability = struct
reachability. *) reachability. *)
let add v x = if PrunedVal.is_symbolic v then M.add v x else x 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 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) -> | LatestPrune.Latest p | LatestPrune.TrueBranch (_, p) | LatestPrune.FalseBranch (_, p) ->
of_prune_pairs p of_prune_pairs p
| LatestPrune.V (_, ptrue, pfalse) -> | LatestPrune.V (_, ptrue, pfalse) ->
@ -885,7 +1004,7 @@ module Reachability = struct
let subst x eval_sym_trace location = let subst x eval_sym_trace location =
let exception Unreachable in let exception Unreachable in
let subst1 x acc = 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 if PrunedVal.is_empty v then raise Unreachable else add v acc
in in
match M.fold subst1 x M.empty with x -> `Reachable x | exception Unreachable -> `Unreachable match M.fold subst1 x M.empty with x -> `Reachable x | exception Unreachable -> `Unreachable
@ -1089,13 +1208,14 @@ module MemReach = struct
let apply_latest_prune : Exp.t -> t -> t = let apply_latest_prune : Exp.t -> t -> t =
let apply1 l v acc = update_mem (PowLoc.singleton l) (PrunedVal.get_val v) acc in
fun e m -> fun e m ->
match (m.latest_prune, e) with match (m.latest_prune, e) with
| LatestPrune.V (x, prunes, _), Exp.Var r | LatestPrune.V (x, prunes, _), Exp.Var r
| LatestPrune.V (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) -> ( | LatestPrune.V (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) -> (
match find_simple_alias r m with match find_simple_alias r m with
| Some (Loc.Var (Var.ProgramVar y)) when Pvar.equal x y -> | 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 PrunePairs.fold apply1 prunes m
| _ -> | _ ->
m ) m )
| _ -> | _ ->

@ -446,8 +446,8 @@ let get_size_sym_f integer_type_widths mem e = Val.get_size_sym (eval integer_ty
module Prune = struct module Prune = struct
type t = {prune_pairs: PrunePairs.t; mem: Mem.t} type t = {prune_pairs: PrunePairs.t; mem: Mem.t}
let update_mem_in_prune lv v {prune_pairs; mem} = let update_mem_in_prune lv v ?(pruning_exp = PruningExp.Unknown) {prune_pairs; mem} =
let prune_pairs = PrunePairs.add lv v prune_pairs in 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 let mem = Mem.update_mem (PowLoc.singleton lv) v mem in
{prune_pairs; mem} {prune_pairs; mem}
@ -503,25 +503,31 @@ module Prune = struct
| Exp.BinOp ((Binop.Ge as comp), Exp.Var x, e') -> ( | Exp.BinOp ((Binop.Ge as comp), Exp.Var x, e') -> (
match Mem.find_simple_alias x mem with match Mem.find_simple_alias x mem with
| Some lv -> | Some lv ->
let v = Mem.find lv mem in let lhs = Mem.find lv mem in
let v' = Val.prune_comp comp v (eval integer_type_widths e' mem) in let rhs = eval integer_type_widths e' mem in
update_mem_in_prune lv v' astate 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 -> | None ->
astate ) astate )
| Exp.BinOp (Binop.Eq, Exp.Var x, e') -> ( | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> (
match Mem.find_simple_alias x mem with match Mem.find_simple_alias x mem with
| Some lv -> | Some lv ->
let v = Mem.find lv mem in let lhs = Mem.find lv mem in
let v' = Val.prune_eq v (eval integer_type_widths e' mem) in let rhs = eval integer_type_widths e' mem in
update_mem_in_prune lv v' astate 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 -> | None ->
astate ) astate )
| Exp.BinOp (Binop.Ne, Exp.Var x, e') -> ( | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> (
match Mem.find_simple_alias x mem with match Mem.find_simple_alias x mem with
| Some lv -> | Some lv ->
let v = Mem.find lv mem in let lhs = Mem.find lv mem in
let v' = Val.prune_ne v (eval integer_type_widths e' mem) in let rhs = eval integer_type_widths e' mem in
update_mem_in_prune lv v' astate 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 -> | None ->
astate ) astate )
| Exp.BinOp | Exp.BinOp

@ -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) { void unsigned_prune_ge2_Good(unsigned int x, unsigned int y) {
if (y > 0) { if (y > 0) {

@ -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,<Length trace>,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, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,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,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: (0 - 48):unsigned64 by call to `scan_hex_Good` ] codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,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,<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Parameter `s`,Binary operation: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ] codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Call,Assignment,Assignment,<RHS trace>,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,<LHS trace>,Parameter `x`,<RHS trace>,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, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1] codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1]
codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2] codetoanalyze/c/bufferoverrun/arith.c, div_const_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,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, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: (2000000000 + 2000000000):signed32] codetoanalyze/c/bufferoverrun/arith.c, integer_overflow_by_addition_Bad, 4, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,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, [<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 (⇐ x + -x + 10) Size: 5] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `x`,<Length trace>,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, [<Offset trace>,Array declaration,Assignment,<Length trace>,Array declaration,Array access: Offset: [4, 2044] (⇐ [0, 1020] + [4, 1024]) Size: 1024] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith5_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Array declaration,Assignment,<Length trace>,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, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,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,<Length trace>,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, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,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, [<Length trace>,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, [<Length trace>,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, [<Length trace>,Array declaration,Array access: Offset: 3 Size: 1] codetoanalyze/c/bufferoverrun/relation.c, FP_array_access2_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 3 Size: 1]
codetoanalyze/c/bufferoverrun/relation.c, FP_array_access3_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 3 Size: 1] codetoanalyze/c/bufferoverrun/relation.c, FP_array_access3_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 3 Size: 1]
codetoanalyze/c/bufferoverrun/relation.c, FP_array_access4_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 3 Size: 1] codetoanalyze/c/bufferoverrun/relation.c, FP_array_access4_Ok, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,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,<Offset trace>,Parameter `x`,<Length trace>,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, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 0] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 0]
codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/sizeof.c, static_stride_bad, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]

@ -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); int* x = (int*)malloc(sizeof(int) * 5);
prune_arrblk_eq_CAF(x); prune_arrblk_eq_CAF(x);
} }

@ -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) { void FP_array_access2_Ok(int x, int y) {
int a[1]; int a[1];

@ -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 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);
}

@ -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,<Offset trace>,Parameter `size`,<Length trace>,Parameter `*ptr`,Array access: Offset: -1 Size: 1 by call to `conditional_buffer_access3` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_buffer_access3_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `size`,<Length trace>,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,<Length trace>,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_buffer_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,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,<Offset trace>,Parameter `idx`,<Length trace>,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `idx`,<Length trace>,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,<Offset trace>,Parameter `idx`,<Length trace>,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,<Offset trace>,Parameter `i`,<Length trace>,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,<Offset trace>,Parameter `i`,<Length trace>,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,<Offset trace>,Parameter `idx`,<Length trace>,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,<Offset trace>,Parameter `idx`,<Length trace>,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,<Offset trace>,Parameter `idx`,<Length trace>,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,<Offset trace>,Parameter `idx`,<Length trace>,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,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,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,<LHS trace>,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,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,<Length trace>,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]] 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,<Length trace>,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, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,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,<Length trace>,Parameter `*arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call1_loop_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,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,<Offset trace>,Parameter `x`,<Length trace>,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,<Offset trace>,Parameter `x`,<Length trace>,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,<Offset trace>,Parameter `x`,<Length trace>,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, [<Offset trace>,Assignment,<Length trace>,Assignment,Call,Assignment,Assignment,Array declaration,Assignment,Array access: Offset: 5 Size: [0, 6]] codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_id_Ok, 4, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,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,<Length trace>,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_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,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,<Length trace>,Parameter `*data`,Assignment,Array access: Offset: [0, +oo] 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,<Length trace>,Parameter `*data`,Assignment,Array access: Offset: [0, +oo] Size: 1 by call to `loop_with_type_casting` ]

@ -15,7 +15,7 @@ void minus_params_Ok(int x, int y) {
void call1_minus_params_Ok() { minus_params_Ok(5, 2); } 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) { void plus_params(int x, int y) {
int a[5]; 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 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) { void plus_params2(int x, int y) {
int a[5]; 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 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) { void loop(char* arr, int len) {
while (len > 0) { while (len > 0) {

Loading…
Cancel
Save