From 7212890846a8c1b4ea826cac934dd8e80f15bba8 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 25 Apr 2017 22:38:01 -0700 Subject: [PATCH] [Bufferoverrun] More prune to make some nodes unreachable Summary: - Bottom-lift abstract memory domain to express unreachable node - Two cases to make a node unreachable + constant: when an evaluation result of condition expression is bottom or false, e.g., "prune(0)". + alias: when the same structure e is compared to itself with "<", ">", and "!=", e.g., "prune(e < e)". - Add test for the new prune (prune_constant.c, prune_alias.c) - Debug the semantics of comparison Reviewed By: mbouaziz Differential Revision: D4938055 fbshipit-source-id: d0fadf0 --- infer/src/bufferoverrun/absLoc.ml | 1 + infer/src/bufferoverrun/arrayBlk.ml | 3 + .../src/bufferoverrun/bufferOverrunChecker.ml | 2 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 115 +++++++++++- .../bufferoverrun/bufferOverrunSemantics.ml | 170 +++++++++++++----- infer/src/bufferoverrun/itv.ml | 3 + .../codetoanalyze/c/bufferoverrun/Makefile | 4 +- .../codetoanalyze/c/bufferoverrun/issues.exp | 1 + .../c/bufferoverrun/prune_alias.c | 109 +++++++++++ .../c/bufferoverrun/prune_constant.c | 38 ++++ 10 files changed, 391 insertions(+), 55 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c create mode 100644 infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 710b3548e..10265eef2 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -69,6 +69,7 @@ struct end) let bot = empty + let is_bot = is_empty let of_pvar pvar = singleton (Loc.of_pvar pvar) let of_id id = singleton (Loc.of_id id) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 66cc9ea6f..aa6d4ea02 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -133,6 +133,9 @@ include AbstractDomain.Map (PPMap) (ArrInfo) let bot : astate = empty +let is_bot : astate -> bool + = is_empty + let make : Allocsite.t -> Itv.t -> Itv.t -> Itv.t -> astate = fun a o sz st -> add a (ArrInfo.make (o, sz, st)) bot diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 86e1b22ab..07d6d3806 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -428,7 +428,7 @@ let compute_post = fun { pdesc; tenv; extras = get_pdesc } -> let cfg = CFG.from_pdesc pdesc in let pdata = ProcData.make pdesc tenv get_pdesc in - let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.bot pdata in + let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in let entry_mem = let entry_id = CFG.id (CFG.start_node cfg) in Analyzer.extract_post entry_id inv_map diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 276f74c99..0783acc8e 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -288,6 +288,16 @@ struct let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t = fun f x y -> { bot with itv = f x.itv y.itv } + let has_pointer : t -> bool + = fun x -> + not (PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk) + + let lift_cmp_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t + = fun f x y -> + if has_pointer x || has_pointer y then + {bot with itv = Itv.unknown_bool} + else lift_itv f x y + let plus : t -> t -> t = fun x y -> { x with itv = Itv.plus x.itv y.itv; arrayblk = ArrayBlk.plus_offset x.arrayblk y.itv } @@ -314,22 +324,22 @@ struct = lift_itv Itv.shiftrt let lt_sem : t -> t -> t - = lift_itv Itv.lt_sem + = lift_cmp_itv Itv.lt_sem let gt_sem : t -> t -> t - = lift_itv Itv.gt_sem + = lift_cmp_itv Itv.gt_sem let le_sem : t -> t -> t - = lift_itv Itv.le_sem + = lift_cmp_itv Itv.le_sem let ge_sem : t -> t -> t - = lift_itv Itv.ge_sem + = lift_cmp_itv Itv.ge_sem let eq_sem : t -> t -> t - = lift_itv Itv.eq_sem + = lift_cmp_itv Itv.eq_sem let ne_sem : t -> t -> t - = lift_itv Itv.ne_sem + = lift_cmp_itv Itv.ne_sem let land_sem : t -> t -> t = lift_itv Itv.land_sem @@ -564,7 +574,7 @@ struct = fun k m -> try Some (M.find k m) with Not_found -> None end -module Mem = +module MemReach = struct type astate = { stack : Stack.astate; heap : Heap.astate; alias : Alias.astate } type t = astate @@ -661,6 +671,97 @@ struct else weak_update_heap ploc v s end +module Mem = struct + include AbstractDomain.BottomLifted (MemReach) + + type t = astate + + let bot : t = Bottom + + let init : t = NonBottom (MemReach.bot) + + let f_lift_default : 'a -> (MemReach.t -> 'a) -> t -> 'a = + fun default f m -> + match m with + | Bottom -> default + | NonBottom m' -> f m' + + let f_lift : (MemReach.t -> MemReach.t) -> t -> t = + fun f -> + f_lift_default Bottom (fun m' -> NonBottom (f m')) + + let pp_summary : F.formatter -> t -> unit + = fun fmt m -> + match m with + | Bottom -> F.fprintf fmt "unreachable" + | NonBottom m' -> MemReach.pp_summary fmt m' + + let find_stack : Loc.t -> t -> Val.t + = fun k -> + f_lift_default Val.bot (MemReach.find_stack k) + + let find_stack_set : PowLoc.t -> t -> Val.t + = fun k -> + f_lift_default Val.bot (MemReach.find_stack_set k) + + let find_heap : Loc.t -> t -> Val.t + = fun k -> + f_lift_default Val.bot (MemReach.find_heap k) + + let find_heap_set : PowLoc.t -> t -> Val.t + = fun k -> + f_lift_default Val.bot (MemReach.find_heap_set k) + + let find_alias : Ident.t -> t -> Pvar.t option + = fun k -> + f_lift_default None (MemReach.find_alias k) + + let load_alias : Ident.t -> Exp.t -> t -> t + = fun id e -> + f_lift (MemReach.load_alias id e) + + let store_alias : Exp.t -> Exp.t -> t -> t + = fun e1 e2 -> + f_lift (MemReach.store_alias e1 e2) + + let add_stack : Loc.t -> Val.t -> t -> t + = fun k v -> + f_lift (MemReach.add_stack k v) + + let add_heap : Loc.t -> Val.t -> t -> t + = fun k v -> + f_lift (MemReach.add_heap k v) + + let strong_update_stack : PowLoc.t -> Val.t -> t -> t + = fun p v -> + f_lift (MemReach.strong_update_stack p v) + + let strong_update_heap : PowLoc.t -> Val.t -> t -> t + = fun p v -> + f_lift (MemReach.strong_update_heap p v) + + let weak_update_stack : PowLoc.t -> Val.t -> t -> t + = fun p v -> + f_lift (MemReach.weak_update_stack p v) + + let weak_update_heap : PowLoc.t -> Val.t -> t -> t + = fun p v -> + f_lift (MemReach.weak_update_heap p v) + + let get_heap_symbols : t -> Itv.Symbol.t list + = f_lift_default [] MemReach.get_heap_symbols + + let get_return : t -> Val.t + = f_lift_default Val.bot MemReach.get_return + + let can_strong_update : PowLoc.t -> bool + = MemReach.can_strong_update + + let update_mem : PowLoc.t -> Val.t -> t -> t + = fun ploc v -> + f_lift (MemReach.update_mem ploc v) +end + module Summary = struct type t = Mem.t * Mem.t * ConditionSet.t diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index ecbb350db..7c4fe2b7b 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -53,33 +53,119 @@ struct | Typ.Tarray (typ, Some ilit) -> sizeof typ * IntLit.to_int ilit | _ -> 4 + let rec must_alias : Exp.t -> Exp.t -> Mem.astate -> bool + = fun e1 e2 m -> + match e1, e2 with + | Exp.Var x1, Exp.Var x2 -> + (match Mem.find_alias x1 m, Mem.find_alias x2 m with + | Some x1', Some x2' -> Pvar.equal x1' x2' + | _, _ -> false) + | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) -> + Unop.equal uop1 uop2 && must_alias e1' e2' m + | Exp.BinOp (bop1, e11, e12), Exp.BinOp (bop2, e21, e22) -> + Binop.equal bop1 bop2 + && must_alias e11 e21 m + && must_alias e12 e22 m + | Exp.Exn t1, Exp.Exn t2 -> must_alias t1 t2 m + | Exp.Const c1, Exp.Const c2 -> Const.equal c1 c2 + | Exp.Cast (t1, e1'), Exp.Cast (t2, e2') -> + Typ.equal t1 t2 && must_alias e1' e2' m + | Exp.Lvar x1, Exp.Lvar x2 -> + Pvar.equal x1 x2 + | Exp.Lfield (e1, fld1, _), Exp.Lfield (e2, fld2, _) -> + must_alias e1 e2 m && Fieldname.equal fld1 fld2 + | Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) -> + must_alias e11 e21 m && must_alias e12 e22 m + | Exp.Sizeof (t1, dynlen1, subt1), Exp.Sizeof (t2, dynlen2, subt2) -> + Typ.equal t1 t2 + && must_alias_opt dynlen1 dynlen2 m + && Int.equal (Subtype.compare subt1 subt2) 0 + | _, _ -> false + + and must_alias_opt : Exp.dynamic_length -> Exp.dynamic_length -> Mem.astate -> bool + = fun dynlen1 dynlen2 m -> + match dynlen1, dynlen2 with + | Some e1, Some e2 -> must_alias e1 e2 m + | None, None -> true + | _, _ -> false + + let comp_rev : Binop.t -> Binop.t + = function + | Binop.Lt -> Binop.Gt + | Binop.Gt -> Binop.Lt + | Binop.Le -> Binop.Ge + | Binop.Ge -> Binop.Le + | Binop.Eq -> Binop.Eq + | Binop.Ne -> Binop.Ne + | _ -> assert (false) + + let comp_not : Binop.t -> Binop.t + = function + | Binop.Lt -> Binop.Ge + | Binop.Gt -> Binop.Le + | Binop.Le -> Binop.Gt + | Binop.Ge -> Binop.Lt + | Binop.Eq -> Binop.Ne + | Binop.Ne -> Binop.Eq + | _ -> assert (false) + + let rec must_alias_cmp : Exp.t -> Mem.astate -> bool + = fun e m -> + match e with + | Exp.BinOp (Binop.Lt, e1, e2) + | Exp.BinOp (Binop.Gt, e1, e2) + | Exp.BinOp (Binop.Ne, e1, e2) -> must_alias e1 e2 m + | Exp.BinOp (Binop.LAnd, e1, e2) -> + must_alias_cmp e1 m || must_alias_cmp e2 m + | Exp.BinOp (Binop.LOr, e1, e2) -> + must_alias_cmp e1 m && must_alias_cmp e2 m + | Exp.UnOp (Unop.LNot, Exp.UnOp (Unop.LNot, e1, _), _) -> + must_alias_cmp e1 m + | 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), _) -> + must_alias_cmp (Exp.BinOp (comp_not c, e1, e2)) m + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> + let e1' = Exp.UnOp (Unop.LNot, e1, t) in + let e2' = Exp.UnOp (Unop.LNot, e2, t) in + must_alias_cmp (Exp.BinOp (Binop.LAnd, e1', e2')) m + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LAnd, e1, e2), t) -> + let e1' = Exp.UnOp (Unop.LNot, e1, t) in + let e2' = Exp.UnOp (Unop.LNot, e2, t) in + must_alias_cmp (Exp.BinOp (Binop.LOr, e1', e2')) m + | _ -> false + let rec eval : Exp.t -> Mem.astate -> Location.t -> Val.t = fun exp mem loc -> - match exp with - | Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem - | Exp.Lvar pvar -> - let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in - let arr = Mem.find_stack_set ploc mem in - ploc |> Val.of_pow_loc |> Val.join arr - | Exp.UnOp (uop, e, _) -> eval_unop uop e mem loc - | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc - | Exp.Const c -> eval_const c - | Exp.Cast (_, e) -> eval e mem loc - | Exp.Lfield (e, fn, _) -> - eval e mem loc - |> Val.get_all_locs - |> Fn.flip PowLoc.append_field fn - |> Val.of_pow_loc - | Exp.Lindex (e1, _) -> - let arr = eval e1 mem loc in (* must have array blk *) - (* let idx = eval e2 mem loc in *) - let ploc = arr |> Val.get_array_blk |> ArrayBlk.get_pow_loc in - (* if nested array, add the array blk *) - let arr = Mem.find_heap_set ploc mem in - Val.join (Val.of_pow_loc ploc) arr - | Exp.Sizeof (typ, _, _) -> Val.of_int (sizeof typ) - | Exp.Exn _ - | Exp.Closure _ -> Val.bot + if must_alias_cmp exp mem then Val.of_int 0 else + match exp with + | Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem + | Exp.Lvar pvar -> + let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in + let arr = Mem.find_stack_set ploc mem in + ploc |> Val.of_pow_loc |> Val.join arr + | Exp.UnOp (uop, e, _) -> eval_unop uop e mem loc + | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc + | Exp.Const c -> eval_const c + | Exp.Cast (_, e) -> eval e mem loc + | Exp.Lfield (e, fn, _) -> + eval e mem loc + |> Val.get_all_locs + |> Fn.flip PowLoc.append_field fn + |> Val.of_pow_loc + | Exp.Lindex (e1, _) -> + let arr = eval e1 mem loc in (* must have array blk *) + (* let idx = eval e2 mem loc in *) + let ploc = arr |> Val.get_array_blk |> ArrayBlk.get_pow_loc in + (* if nested array, add the array blk *) + let arr = Mem.find_heap_set ploc mem in + Val.join (Val.of_pow_loc ploc) arr + | Exp.Sizeof (typ, _, _) -> Val.of_int (sizeof typ) + | Exp.Exn _ + | Exp.Closure _ -> Val.bot and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Location.t -> Val.t = fun unop e mem loc -> @@ -197,26 +283,6 @@ struct | None -> mem) | _ -> mem - let comp_rev : Binop.t -> Binop.t - = function - | Binop.Lt -> Binop.Gt - | Binop.Gt -> Binop.Lt - | Binop.Le -> Binop.Ge - | Binop.Ge -> Binop.Le - | Binop.Eq -> Binop.Eq - | Binop.Ne -> Binop.Ne - | _ -> assert (false) - - let comp_not : Binop.t -> Binop.t - = function - | Binop.Lt -> Binop.Ge - | Binop.Gt -> Binop.Le - | Binop.Le -> Binop.Gt - | Binop.Ge -> Binop.Lt - | Binop.Eq -> Binop.Ne - | Binop.Ne -> Binop.Eq - | _ -> assert (false) - let prune_binop_right : Exp.t -> Location.t -> Mem.astate -> Mem.astate = fun e loc mem -> match e with @@ -229,10 +295,22 @@ struct prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) loc mem | _ -> mem + let is_unreachable_constant : Exp.t -> Location.t -> Mem.astate -> bool + = fun e loc m -> + Val.(<=) ~lhs:(eval e m loc) ~rhs:(Val.of_int 0) + + let prune_unreachable : Exp.t -> Location.t -> Mem.astate -> Mem.astate + = fun e loc mem -> + if is_unreachable_constant e loc mem then Mem.bot else mem + let rec prune : Exp.t -> Location.t -> Mem.astate -> Mem.astate = fun e loc mem -> let mem = - mem |> prune_unop e |> prune_binop_left e loc |> prune_binop_right e loc + mem + |> prune_unreachable e loc + |> prune_unop e + |> prune_binop_left e loc + |> prune_binop_right e loc in match e with | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 60592f525..cd1a6d65e 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -876,6 +876,9 @@ let pos : t let nat : t = NonBottom ItvPure.nat +let unknown_bool : t + = NonBottom ItvPure.unknown_bool + let make : Bound.t -> Bound.t -> t = fun l u -> if Bound.lt u l then Bottom else NonBottom (ItvPure.make l u) diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/Makefile b/infer/tests/codetoanalyze/c/bufferoverrun/Makefile index 0e1a95d5b..32ecb7f90 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/Makefile +++ b/infer/tests/codetoanalyze/c/bufferoverrun/Makefile @@ -25,6 +25,8 @@ SOURCES = \ nested_loop_with_label.c \ break_continue_return.c \ goto_loop.c \ - inf_loop.c + inf_loop.c \ + prune_constant.c \ + prune_alias.c \ include $(TESTS_DIR)/clang.make diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 269d8a953..9813a2918 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -7,5 +7,6 @@ codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN, codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offset : [10, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/goto_loop.c:24:3] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset : [0, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5] +codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset : [1, 1] Size : [1, 1] @ codetoanalyze/c/bufferoverrun/prune_alias.c:107:5] codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset : [10, 10] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3] codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset : [0, +oo] Size : [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:16:10] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c new file mode 100644 index 000000000..26c0012fb --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -0,0 +1,109 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +void prune_alias_le_Ok(int x) { + int a[1]; + + if (x <= x) { + a[0] = 0; + } else { + a[1] = 0; + } +} + +void prune_alias_ge_Ok(int x) { + int a[1]; + + if (x >= x) { + a[0] = 0; + } else { + a[1] = 0; + } +} + +void prune_alias_eq_Ok(int x) { + int a[1]; + + if (x == x) { + a[0] = 0; + } else { + a[1] = 0; + } +} + +void prune_alias_lt_Ok(int x) { + int a[1]; + + if (x < x) { + a[1] = 0; + } +} + +void prune_alias_gt_Ok(int x) { + int a[1]; + + if (x > x) { + a[1] = 0; + } +} + +void prune_alias_ne_Ok(int x) { + int a[1]; + + if (x != x) { + a[1] = 0; + } +} + +void prune_alias_not_Ok(int x) { + int a[1]; + + if (!(x == x)) { + a[1] = 0; + } + + if (!(x <= x)) { + a[1] = 0; + } + + if (!(x >= x)) { + a[1] = 0; + } +} + +void prune_alias_and_Ok(int x) { + int a[1]; + + if (x == x && x != x) { + a[1] = 0; + } +} + +void prune_alias_or_Ok(int x, int y) { + int a[1]; + + if (x != x || y != y) { + a[1] = 0; + } +} + +void prune_alias_exp_Ok(int x) { + int a[1]; + + if (x + 1 != x + 1) { + a[1] = 0; + } +} + +void FP_prune_alias_exp_Ok(int x) { + int a[1]; + + if (x + 1 != 1 + x) { + a[1] = 0; + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c new file mode 100644 index 000000000..40bf96cbc --- /dev/null +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c @@ -0,0 +1,38 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +void prune_constant_true_Ok() { + int a[1]; + + if (1) { + a[0] = 0; + } else { + a[1] = 0; + } +} + +void prune_constant_false_Ok() { + int a[1]; + + if (0) { + a[1] = 0; + } else { + a[0] = 0; + } +} + +void prune_constant_value_Ok(int x) { + int a[1]; + if (-1 < x && x < 1) { + if (x) { + a[1] = 0; + } else { + a[0] = 0; + } + } +}