pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo] Renamed a few Itv values

Browse Source 
Reviewed By: jvillard

Differential Revision: D5137445

fbshipit-source-id: f16b68e
master
Mehdi Bouaziz 8 years ago committed by Facebook Github Bot
parent 43d7428e8f
commit 1486b92084
4 changed files with 217 additions and 217 deletions
Show Stats Download Patch File Download Diff File

8
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -36,7 +36,7 @@ struct
type extras = Typ.Procname.t -> Procdesc.t option type extras = Typ.Procname.t -> Procdesc.t option
let set_uninitialized (typ : Typ.t) loc mem = match typ.desc with let set_uninitialized (typ : Typ.t) loc mem = match typ.desc with
| Tint _ | Tfloat _ -> Dom.Mem.weak_update_heap loc Dom.Val.top_itv mem | Tint _ | Tfloat _ -> Dom.Mem.weak_update_heap loc Dom.Val.Itv.top mem
| _ -> mem | _ -> mem
(* NOTE: heuristic *) (* NOTE: heuristic *)
@ -78,13 +78,13 @@ struct
let model_natual_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate let model_natual_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate
= fun ret mem -> = fun ret mem ->
match ret with match ret with
| Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.nat_itv mem | Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.Itv.nat mem
| _ -> mem | _ -> mem
let model_unknown_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate let model_unknown_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate
= fun ret mem -> = fun ret mem ->
match ret with match ret with
Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.top_itv mem Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.Itv.top mem
| None -> mem | None -> mem
let model_infer_print let model_infer_print
@ -236,7 +236,7 @@ struct
let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in let ret_val = Dom.Mem.find_heap ret_loc callee_exit_mem in
Dom.Val.subst ret_val subst_map Dom.Val.subst ret_val subst_map
|> Dom.Val.normalize (* normalize bottom *) |> Dom.Val.normalize (* normalize bottom *)
| _ -> Dom.Val.top_itv | _ -> Dom.Val.Itv.top
let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.Mem.astate -> unit let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.Mem.astate -> unit
= fun instr pre post -> = fun instr pre post ->

25
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -265,17 +265,9 @@ struct
let get_all_locs : t -> PowLoc.t let get_all_locs : t -> PowLoc.t
= fun x -> PowLoc.join x.powloc (get_array_locs x) = fun x -> PowLoc.join x.powloc (get_array_locs x)
let top_itv : t let of_itv itv = { bot with itv }
= { bot with itv = Itv.top }
let pos_itv : t let of_int n = of_itv (Itv.of_int n)
= { bot with itv = Itv.pos }
let nat_itv : t
= { bot with itv = Itv.nat }
let of_int : int -> t
= fun n -> { bot with itv = Itv.of_int n }
let of_itv : Itv.t -> t let of_itv : Itv.t -> t
= fun itv -> { bot with itv } = fun itv -> { bot with itv }
@ -286,9 +278,6 @@ struct
let of_array_blk : ArrayBlk.astate -> t let of_array_blk : ArrayBlk.astate -> t
= fun a -> { bot with arrayblk = a } = fun a -> { bot with arrayblk = a }
let zero : t
= of_int 0
let modify_itv : Itv.t -> t -> t let modify_itv : Itv.t -> t -> t
= fun i x -> { x with itv = i } = fun i x -> { x with itv = i }
@ -414,6 +403,14 @@ struct
let pp_summary : F.formatter -> t -> unit let pp_summary : F.formatter -> t -> unit
= fun fmt x -> F.fprintf fmt "(%a, %a)" Itv.pp x.itv ArrayBlk.pp x.arrayblk = fun fmt x -> F.fprintf fmt "(%a, %a)" Itv.pp x.itv ArrayBlk.pp x.arrayblk
module Itv =
struct
let nat = of_itv Itv.nat
let m1_255 = of_itv Itv.m1_255
let pos = of_itv Itv.pos
let top = of_itv Itv.top
end
end end
module Stack = module Stack =
@ -478,7 +475,7 @@ struct
let find : Loc.t -> astate -> Val.t let find : Loc.t -> astate -> Val.t
= fun l m -> = fun l m ->
try find l m with try find l m with
| Not_found -> Val.top_itv | Not_found -> Val.Itv.top
let find_set : PowLoc.t -> astate -> Val.t let find_set : PowLoc.t -> astate -> Val.t
= fun locs mem -> = fun locs mem ->

340
infer/src/bufferoverrun/bufferOverrunSemantics.ml
Unescape View File

@ -24,23 +24,23 @@ struct
let eval_const : Const.t -> Val.t let eval_const : Const.t -> Val.t
= function = function
| Const.Cint intlit -> (try Val.of_int (IntLit.to_int intlit) with _ -> Val.top_itv) | Const.Cint intlit -> (try Val.of_int (IntLit.to_int intlit) with _ -> Val.Itv.top)
| Const.Cfloat f -> f |> int_of_float |> Val.of_int | Const.Cfloat f -> f |> int_of_float |> Val.of_int
| _ -> Val.top_itv (* TODO *) | _ -> Val.Itv.top (* TODO *)
let sizeof_ikind : Typ.ikind -> int let sizeof_ikind : Typ.ikind -> int
= function = function
| Typ.IChar | Typ.ISChar | Typ.IUChar | Typ.IBool -> 1 | Typ.IChar | Typ.ISChar | Typ.IUChar | Typ.IBool -> 1
| Typ.IInt | Typ.IUInt -> 4 | Typ.IInt | Typ.IUInt -> 4
| Typ.IShort | Typ.IUShort -> 2 | Typ.IShort | Typ.IUShort -> 2
| Typ.ILong | Typ.IULong -> 4 | Typ.ILong | Typ.IULong -> 4
| Typ.ILongLong | Typ.IULongLong -> 8 | Typ.ILongLong | Typ.IULongLong -> 8
| Typ.I128 | Typ.IU128 -> 16 | Typ.I128 | Typ.IU128 -> 16
let sizeof_fkind : Typ.fkind -> int let sizeof_fkind : Typ.fkind -> int
= function = function
| Typ.FFloat -> 4 | Typ.FFloat -> 4
| Typ.FDouble | Typ.FLongDouble -> 8 | Typ.FDouble | Typ.FLongDouble -> 8
(* NOTE: assume 32bit machine *) (* NOTE: assume 32bit machine *)
let rec sizeof (typ : Typ.t) : int = let rec sizeof (typ : Typ.t) : int =
@ -58,60 +58,60 @@ struct
= fun e1 e2 m -> = fun e1 e2 m ->
match e1, e2 with match e1, e2 with
| Exp.Var x1, Exp.Var x2 -> | Exp.Var x1, Exp.Var x2 ->
(match Mem.find_alias x1 m, Mem.find_alias x2 m with (match Mem.find_alias x1 m, Mem.find_alias x2 m with
| Some x1', Some x2' -> Pvar.equal x1' x2' | Some x1', Some x2' -> Pvar.equal x1' x2'
| _, _ -> false) | _, _ -> false)
| Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) -> | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) ->
Unop.equal uop1 uop2 && must_alias e1' e2' m Unop.equal uop1 uop2 && must_alias e1' e2' m
| Exp.BinOp (bop1, e11, e12), Exp.BinOp (bop2, e21, e22) -> | Exp.BinOp (bop1, e11, e12), Exp.BinOp (bop2, e21, e22) ->
Binop.equal bop1 bop2 Binop.equal bop1 bop2
&& must_alias e11 e21 m && must_alias e11 e21 m
&& must_alias e12 e22 m && must_alias e12 e22 m
| Exp.Exn t1, Exp.Exn t2 -> must_alias t1 t2 m | Exp.Exn t1, Exp.Exn t2 -> must_alias t1 t2 m
| Exp.Const c1, Exp.Const c2 -> Const.equal c1 c2 | Exp.Const c1, Exp.Const c2 -> Const.equal c1 c2
| Exp.Cast (t1, e1'), Exp.Cast (t2, e2') -> | Exp.Cast (t1, e1'), Exp.Cast (t2, e2') ->
Typ.equal t1 t2 && must_alias e1' e2' m Typ.equal t1 t2 && must_alias e1' e2' m
| Exp.Lvar x1, Exp.Lvar x2 -> | Exp.Lvar x1, Exp.Lvar x2 ->
Pvar.equal x1 x2 Pvar.equal x1 x2
| Exp.Lfield (e1, fld1, _), Exp.Lfield (e2, fld2, _) -> | Exp.Lfield (e1, fld1, _), Exp.Lfield (e2, fld2, _) ->
must_alias e1 e2 m && Fieldname.equal fld1 fld2 must_alias e1 e2 m && Fieldname.equal fld1 fld2
| Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) -> | Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) ->
must_alias e11 e21 m && must_alias e12 e22 m must_alias e11 e21 m && must_alias e12 e22 m
| Exp.Sizeof {nbytes=Some nbytes1}, Exp.Sizeof {nbytes=Some nbytes2} -> | Exp.Sizeof {nbytes=Some nbytes1}, Exp.Sizeof {nbytes=Some nbytes2} ->
Int.equal nbytes1 nbytes2 Int.equal nbytes1 nbytes2
| Exp.Sizeof {typ=t1; dynamic_length=dynlen1; subtype=subt1}, | Exp.Sizeof {typ=t1; dynamic_length=dynlen1; subtype=subt1},
Exp.Sizeof {typ=t2; dynamic_length=dynlen2; subtype=subt2} -> Exp.Sizeof {typ=t2; dynamic_length=dynlen2; subtype=subt2} ->
Typ.equal t1 t2 Typ.equal t1 t2
&& must_alias_opt dynlen1 dynlen2 m && must_alias_opt dynlen1 dynlen2 m
&& Int.equal (Subtype.compare subt1 subt2) 0 && Int.equal (Subtype.compare subt1 subt2) 0
| _, _ -> false | _, _ -> false
and must_alias_opt : Exp.t option -> Exp.t option -> Mem.astate -> bool and must_alias_opt : Exp.t option -> Exp.t option -> Mem.astate -> bool
= fun e1_opt e2_opt m -> = fun e1_opt e2_opt m ->
match e1_opt, e2_opt with match e1_opt, e2_opt with
| Some e1, Some e2 -> must_alias e1 e2 m | Some e1, Some e2 -> must_alias e1 e2 m
| None, None -> true | None, None -> true
| _, _ -> false | _, _ -> false
let comp_rev : Binop.t -> Binop.t let comp_rev : Binop.t -> Binop.t
= function = function
| Binop.Lt -> Binop.Gt | Binop.Lt -> Binop.Gt
| Binop.Gt -> Binop.Lt | Binop.Gt -> Binop.Lt
| Binop.Le -> Binop.Ge | Binop.Le -> Binop.Ge
| Binop.Ge -> Binop.Le | Binop.Ge -> Binop.Le
| Binop.Eq -> Binop.Eq | Binop.Eq -> Binop.Eq
| Binop.Ne -> Binop.Ne | Binop.Ne -> Binop.Ne
| _ -> assert (false) | _ -> assert (false)
let comp_not : Binop.t -> Binop.t let comp_not : Binop.t -> Binop.t
= function = function
| Binop.Lt -> Binop.Ge | Binop.Lt -> Binop.Ge
| Binop.Gt -> Binop.Le | Binop.Gt -> Binop.Le
| Binop.Le -> Binop.Gt | Binop.Le -> Binop.Gt
| Binop.Ge -> Binop.Lt | Binop.Ge -> Binop.Lt
| Binop.Eq -> Binop.Ne | Binop.Eq -> Binop.Ne
| Binop.Ne -> Binop.Eq | Binop.Ne -> Binop.Eq
| _ -> assert (false) | _ -> assert (false)
let rec must_alias_cmp : Exp.t -> Mem.astate -> bool let rec must_alias_cmp : Exp.t -> Mem.astate -> bool
= fun e m -> = fun e m ->
@ -120,26 +120,26 @@ struct
| Exp.BinOp (Binop.Gt, e1, e2) | Exp.BinOp (Binop.Gt, e1, e2)
| Exp.BinOp (Binop.Ne, e1, e2) -> must_alias e1 e2 m | Exp.BinOp (Binop.Ne, e1, e2) -> must_alias e1 e2 m
| Exp.BinOp (Binop.LAnd, e1, e2) -> | Exp.BinOp (Binop.LAnd, e1, e2) ->
must_alias_cmp e1 m || must_alias_cmp e2 m must_alias_cmp e1 m || must_alias_cmp e2 m
| Exp.BinOp (Binop.LOr, e1, e2) -> | Exp.BinOp (Binop.LOr, e1, e2) ->
must_alias_cmp e1 m && must_alias_cmp e2 m must_alias_cmp e1 m && must_alias_cmp e2 m
| Exp.UnOp (Unop.LNot, Exp.UnOp (Unop.LNot, e1, _), _) -> | Exp.UnOp (Unop.LNot, Exp.UnOp (Unop.LNot, e1, _), _) ->
must_alias_cmp e1 m must_alias_cmp e1 m
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Lt as c, e1, e2), _) | 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.Gt as c, e1, e2), _)
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Le 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.Ge as c, e1, e2), _)
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq 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), _) -> | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne as c, e1, e2), _) ->
must_alias_cmp (Exp.BinOp (comp_not c, e1, e2)) m must_alias_cmp (Exp.BinOp (comp_not c, e1, e2)) m
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) ->
let e1' = Exp.UnOp (Unop.LNot, e1, t) in let e1' = Exp.UnOp (Unop.LNot, e1, t) in
let e2' = Exp.UnOp (Unop.LNot, e2, t) in let e2' = Exp.UnOp (Unop.LNot, e2, t) in
must_alias_cmp (Exp.BinOp (Binop.LAnd, e1', e2')) m must_alias_cmp (Exp.BinOp (Binop.LAnd, e1', e2')) m
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LAnd, e1, e2), t) -> | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LAnd, e1, e2), t) ->
let e1' = Exp.UnOp (Unop.LNot, e1, t) in let e1' = Exp.UnOp (Unop.LNot, e1, t) in
let e2' = Exp.UnOp (Unop.LNot, e2, t) in let e2' = Exp.UnOp (Unop.LNot, e2, t) in
must_alias_cmp (Exp.BinOp (Binop.LOr, e1', e2')) m must_alias_cmp (Exp.BinOp (Binop.LOr, e1', e2')) m
| _ -> false | _ -> false
let rec eval : Exp.t -> Mem.astate -> Location.t -> Val.t let rec eval : Exp.t -> Mem.astate -> Location.t -> Val.t
@ -148,71 +148,71 @@ struct
match exp with match exp with
| Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem | Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem
| Exp.Lvar pvar -> | Exp.Lvar pvar ->
let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in
let arr = Mem.find_stack_set ploc mem in let arr = Mem.find_stack_set ploc mem in
ploc |> Val.of_pow_loc |> Val.join arr ploc |> Val.of_pow_loc |> Val.join arr
| Exp.UnOp (uop, e, _) -> eval_unop uop e mem loc | Exp.UnOp (uop, e, _) -> eval_unop uop e mem loc
| Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem loc
| Exp.Const c -> eval_const c | Exp.Const c -> eval_const c
| Exp.Cast (_, e) -> eval e mem loc | Exp.Cast (_, e) -> eval e mem loc
| Exp.Lfield (e, fn, _) -> | Exp.Lfield (e, fn, _) ->
eval e mem loc eval e mem loc
|> Val.get_array_locs |> Val.get_array_locs
|> Fn.flip PowLoc.append_field fn |> Fn.flip PowLoc.append_field fn
|> Val.of_pow_loc |> Val.of_pow_loc
| Exp.Lindex (e1, _) -> | Exp.Lindex (e1, _) ->
let arr = eval e1 mem loc |> Val.get_array_blk in (* must have array blk *) let arr = eval e1 mem loc |> Val.get_array_blk in (* must have array blk *)
(* let idx = eval e2 mem loc in *) (* let idx = eval e2 mem loc in *)
let ploc = if ArrayBlk.is_bot arr then PowLoc.unknown else ArrayBlk.get_pow_loc arr in let ploc = if ArrayBlk.is_bot arr then PowLoc.unknown else ArrayBlk.get_pow_loc arr in
(* if nested array, add the array blk *) (* if nested array, add the array blk *)
let arr = Mem.find_heap_set ploc mem in let arr = Mem.find_heap_set ploc mem in
Val.join (Val.of_pow_loc ploc) arr Val.join (Val.of_pow_loc ploc) arr
| Exp.Sizeof {nbytes=Some size} -> Val.of_int size | Exp.Sizeof {nbytes=Some size} -> Val.of_int size
| Exp.Sizeof {typ; nbytes=None} -> Val.of_int (sizeof typ) | Exp.Sizeof {typ; nbytes=None} -> Val.of_int (sizeof typ)
| Exp.Exn _ | Exp.Exn _
| Exp.Closure _ -> Val.top_itv | Exp.Closure _ -> Val.Itv.top
and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Location.t -> Val.t and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Location.t -> Val.t
= fun unop e mem loc -> = fun unop e mem loc ->
let v = eval e mem loc in let v = eval e mem loc in
match unop with match unop with
| Unop.Neg -> Val.neg v | Unop.Neg -> Val.neg v
| Unop.BNot -> Val.unknown_bit v | Unop.BNot -> Val.unknown_bit v
| Unop.LNot -> Val.lnot v | Unop.LNot -> Val.lnot v
and eval_binop and eval_binop
: Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Location.t -> Val.t : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Location.t -> Val.t
= fun binop e1 e2 mem loc -> = fun binop e1 e2 mem loc ->
let v1 = eval e1 mem loc in let v1 = eval e1 mem loc in
let v2 = eval e2 mem loc in let v2 = eval e2 mem loc in
match binop with match binop with
| Binop.PlusA -> | Binop.PlusA ->
Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2) Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2)
| Binop.PlusPI -> Val.plus_pi v1 v2 | Binop.PlusPI -> Val.plus_pi v1 v2
| Binop.MinusA -> | Binop.MinusA ->
Val.joins Val.joins
[ Val.minus v1 v2 [ Val.minus v1 v2
; Val.minus_pi v1 v2 ; Val.minus_pi v1 v2
; Val.minus_pp v1 v2 ] ; Val.minus_pp v1 v2 ]
| Binop.MinusPI -> Val.minus_pi v1 v2 | Binop.MinusPI -> Val.minus_pi v1 v2
| Binop.MinusPP -> Val.minus_pp v1 v2 | Binop.MinusPP -> Val.minus_pp v1 v2
| Binop.Mult -> Val.mult v1 v2 | Binop.Mult -> Val.mult v1 v2
| Binop.Div -> Val.div v1 v2 | Binop.Div -> Val.div v1 v2
| Binop.Mod -> Val.mod_sem v1 v2 | Binop.Mod -> Val.mod_sem v1 v2
| Binop.Shiftlt -> Val.shiftlt v1 v2 | Binop.Shiftlt -> Val.shiftlt v1 v2
| Binop.Shiftrt -> Val.shiftrt v1 v2 | Binop.Shiftrt -> Val.shiftrt v1 v2
| Binop.Lt -> Val.lt_sem v1 v2 | Binop.Lt -> Val.lt_sem v1 v2
| Binop.Gt -> Val.gt_sem v1 v2 | Binop.Gt -> Val.gt_sem v1 v2
| Binop.Le -> Val.le_sem v1 v2 | Binop.Le -> Val.le_sem v1 v2
| Binop.Ge -> Val.ge_sem v1 v2 | Binop.Ge -> Val.ge_sem v1 v2
| Binop.Eq -> Val.eq_sem v1 v2 | Binop.Eq -> Val.eq_sem v1 v2
| Binop.Ne -> Val.ne_sem v1 v2 | Binop.Ne -> Val.ne_sem v1 v2
| Binop.BAnd | Binop.BAnd
| Binop.BXor | Binop.BXor
| Binop.BOr -> Val.unknown_bit v1 | Binop.BOr -> Val.unknown_bit v1
| Binop.LAnd -> Val.land_sem v1 v2 | Binop.LAnd -> Val.land_sem v1 v2
| Binop.LOr -> Val.lor_sem v1 v2 | Binop.LOr -> Val.lor_sem v1 v2
| Binop.PtrFld -> raise Not_implemented | Binop.PtrFld -> raise Not_implemented
let get_allocsite : Typ.Procname.t -> CFG.node -> int -> int -> string let get_allocsite : Typ.Procname.t -> CFG.node -> int -> int -> string
= fun proc_name node inst_num dimension -> = fun proc_name node inst_num dimension ->
@ -238,25 +238,25 @@ struct
= fun e mem -> = fun e mem ->
match e with match e with
| Exp.Var x -> | Exp.Var x ->
(match Mem.find_alias x mem with (match Mem.find_alias x mem with
| Some x' -> | Some x' ->
let lv = Loc.of_pvar x' in let lv = Loc.of_pvar x' in
let v = Mem.find_heap lv mem in let v = Mem.find_heap lv mem in
let v' = Val.prune_zero v in let v' = Val.prune_zero v in
Mem.update_mem (PowLoc.singleton lv) v' mem Mem.update_mem (PowLoc.singleton lv) v' mem
| None -> mem) | None -> mem)
| Exp.UnOp (Unop.LNot, Exp.Var x, _) -> | Exp.UnOp (Unop.LNot, Exp.Var x, _) ->
(match Mem.find_alias x mem with (match Mem.find_alias x mem with
| Some x' -> | Some x' ->
let lv = Loc.of_pvar x' in let lv = Loc.of_pvar x' in
let v = Mem.find_heap lv mem in let v = Mem.find_heap lv mem in
let itv_v = let itv_v =
if Itv.is_bot (Val.get_itv v) then Itv.bot else if Itv.is_bot (Val.get_itv v) then Itv.bot else
Val.get_itv Val.zero Itv.false_sem
in in
let v' = Val.modify_itv itv_v v in let v' = Val.modify_itv itv_v v in
Mem.update_mem (PowLoc.singleton lv) v' mem Mem.update_mem (PowLoc.singleton lv) v' mem
| None -> mem) | None -> mem)
| _ -> mem | _ -> mem
let prune_binop_left : Exp.t -> Location.t -> Mem.astate -> Mem.astate let prune_binop_left : Exp.t -> Location.t -> Mem.astate -> Mem.astate
@ -266,29 +266,29 @@ struct
| Exp.BinOp (Binop.Gt as comp, Exp.Var x, e') | Exp.BinOp (Binop.Gt as comp, Exp.Var x, e')
| Exp.BinOp (Binop.Le as comp, Exp.Var x, e') | Exp.BinOp (Binop.Le as comp, Exp.Var x, e')
| Exp.BinOp (Binop.Ge as comp, Exp.Var x, e') -> | Exp.BinOp (Binop.Ge as comp, Exp.Var x, e') ->
(match Mem.find_alias x mem with (match Mem.find_alias x mem with
| Some x' -> | Some x' ->
let lv = Loc.of_pvar x' in let lv = Loc.of_pvar x' in
let v = Mem.find_heap lv mem in let v = Mem.find_heap lv mem in
let v' = Val.prune_comp comp v (eval e' mem loc) in let v' = Val.prune_comp comp v (eval e' mem loc) in
Mem.update_mem (PowLoc.singleton lv) v' mem Mem.update_mem (PowLoc.singleton lv) v' mem
| None -> mem) | None -> mem)
| Exp.BinOp (Binop.Eq, Exp.Var x, e') -> | Exp.BinOp (Binop.Eq, Exp.Var x, e') ->
(match Mem.find_alias x mem with (match Mem.find_alias x mem with
| Some x' -> | Some x' ->
let lv = Loc.of_pvar x' in let lv = Loc.of_pvar x' in
let v = Mem.find_heap lv mem in let v = Mem.find_heap lv mem in
let v' = Val.prune_eq v (eval e' mem loc) in let v' = Val.prune_eq v (eval e' mem loc) in
Mem.update_mem (PowLoc.singleton lv) v' mem Mem.update_mem (PowLoc.singleton lv) v' mem
| None -> mem) | None -> mem)
| Exp.BinOp (Binop.Ne, Exp.Var x, e') -> | Exp.BinOp (Binop.Ne, Exp.Var x, e') ->
(match Mem.find_alias x mem with (match Mem.find_alias x mem with
| Some x' -> | Some x' ->
let lv = Loc.of_pvar x' in let lv = Loc.of_pvar x' in
let v = Mem.find_heap lv mem in let v = Mem.find_heap lv mem in
let v' = Val.prune_ne v (eval e' mem loc) in let v' = Val.prune_ne v (eval e' mem loc) in
Mem.update_mem (PowLoc.singleton lv) v' mem Mem.update_mem (PowLoc.singleton lv) v' mem
| None -> mem) | None -> mem)
| _ -> mem | _ -> mem
let prune_binop_right : Exp.t -> Location.t -> Mem.astate -> Mem.astate let prune_binop_right : Exp.t -> Location.t -> Mem.astate -> Mem.astate
@ -300,7 +300,7 @@ struct
| Exp.BinOp (Binop.Ge as c, e', Exp.Var x) | Exp.BinOp (Binop.Ge as c, e', Exp.Var x)
| Exp.BinOp (Binop.Eq 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) -> | Exp.BinOp (Binop.Ne as c, e', Exp.Var x) ->
prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) loc mem prune_binop_left (Exp.BinOp (comp_rev c, Exp.Var x, e')) loc mem
| _ -> mem | _ -> mem
let is_unreachable_constant : Exp.t -> Location.t -> Mem.astate -> bool let is_unreachable_constant : Exp.t -> Location.t -> Mem.astate -> bool
@ -322,23 +322,23 @@ struct
in in
match e with match e with
| Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
prune e loc mem prune e loc mem
| Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
prune (Exp.UnOp (Unop.LNot, e, None)) loc mem prune (Exp.UnOp (Unop.LNot, e, None)) loc mem
| Exp.UnOp (Unop.Neg, Exp.Var x, _) -> prune (Exp.Var x) loc mem | Exp.UnOp (Unop.Neg, Exp.Var x, _) -> prune (Exp.Var x) loc mem
| Exp.BinOp (Binop.LAnd, e1, e2) -> | Exp.BinOp (Binop.LAnd, e1, e2) ->
mem |> prune e1 loc |> prune e2 loc mem |> prune e1 loc |> prune e2 loc
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) ->
mem mem
|> prune (Exp.UnOp (Unop.LNot, e1, t)) loc |> prune (Exp.UnOp (Unop.LNot, e1, t)) loc
|> prune (Exp.UnOp (Unop.LNot, e2, t)) loc |> prune (Exp.UnOp (Unop.LNot, e2, t)) loc
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Lt as c, e1, e2), _) | 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.Gt as c, e1, e2), _)
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Le 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.Ge as c, e1, e2), _)
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq 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), _) -> | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Ne as c, e1, e2), _) ->
prune (Exp.BinOp (comp_not c, e1, e2)) loc mem prune (Exp.BinOp (comp_not c, e1, e2)) loc mem
| _ -> mem | _ -> mem
let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list
@ -382,15 +382,15 @@ struct
let add_pair_ptr typ v1 v2 pairs = let add_pair_ptr typ v1 v2 pairs =
match typ.Typ.desc with match typ.Typ.desc with
| Typ.Tptr ({desc=Tstruct typename}, _) -> | Typ.Tptr ({desc=Tstruct typename}, _) ->
(match Tenv.lookup tenv typename with (match Tenv.lookup tenv typename with
| Some str -> | Some str ->
let fns = List.map ~f:get_field_name str.Typ.Struct.fields in let fns = List.map ~f:get_field_name str.Typ.Struct.fields in
List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns
| _ -> pairs) | _ -> pairs)
| Typ.Tptr (_ ,_) -> | Typ.Tptr (_ ,_) ->
let v1' = deref_ptr v1 callee_mem in let v1' = deref_ptr v1 callee_mem in
let v2' = deref_ptr v2 caller_mem in let v2' = deref_ptr v2 caller_mem in
add_pair_val v1' v2' pairs add_pair_val v1' v2' pairs
| _ -> pairs | _ -> pairs
in in
[] |> add_pair_val formal actual |> add_pair_ptr typ formal actual [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual
@ -401,10 +401,10 @@ struct
let add_pair map (formal, actual) = let add_pair map (formal, actual) =
match formal with match formal with
| Itv.Bound.Linear (0, se1) when Itv.SymLinear.cardinal se1 > 0 -> | Itv.Bound.Linear (0, se1) when Itv.SymLinear.cardinal se1 > 0 ->
let (symbol, coeff) = Itv.SymLinear.choose se1 in let (symbol, coeff) = Itv.SymLinear.choose se1 in
if Int.equal coeff 1 if Int.equal coeff 1
then Itv.SubstMap.add symbol actual map then Itv.SubstMap.add symbol actual map
else assert false else assert false
| _ -> assert false | _ -> assert false
in in
List.fold ~f:add_pair ~init:Itv.SubstMap.empty pairs List.fold ~f:add_pair ~init:Itv.SubstMap.empty pairs
@ -431,6 +431,6 @@ struct
in in
let formals = get_formals callee_pdesc in let formals = get_formals callee_pdesc in
let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem loc) params in let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem loc) params in
list_fold2_def ~default:Val.top_itv ~f:add_pair formals actuals ~init:[] list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:[]
|> subst_map_of_pairs |> subst_map_of_pairs
end end

61
infer/src/bufferoverrun/itv.ml
Unescape View File

@ -189,7 +189,6 @@ let pp_min_max : F.formatter -> min_max_t -> unit
| Min -> F.fprintf fmt "min" | Min -> F.fprintf fmt "min"
| Max -> F.fprintf fmt "max" | Max -> F.fprintf fmt "max"
let pp : F.formatter -> t -> unit let pp : F.formatter -> t -> unit
= fun fmt -> function = fun fmt -> function
| MInf -> F.fprintf fmt "-oo" | MInf -> F.fprintf fmt "-oo"
@ -207,6 +206,14 @@ let pp : F.formatter -> t -> unit
let of_int : int -> t let of_int : int -> t
= fun n -> Linear (n, SymLinear.empty) = fun n -> Linear (n, SymLinear.empty)
let zero = of_int 0
let one = of_int 1
let minus_one = of_int ~-1
let _255 = of_int 255
let of_sym : SymLinear.t -> t let of_sym : SymLinear.t -> t
= fun s -> Linear (0, s) = fun s -> Linear (0, s)
@ -536,8 +543,9 @@ struct
let pp : F.formatter -> t -> unit let pp : F.formatter -> t -> unit
= fun fmt (l, u) -> F.fprintf fmt "[%a, %a]" Bound.pp l Bound.pp u = fun fmt (l, u) -> F.fprintf fmt "[%a, %a]" Bound.pp l Bound.pp u
let of_int : int -> t let of_bound bound = (bound, bound)
= fun n -> (Bound.of_int n, Bound.of_int n)
let of_int n = of_bound (Bound.of_int n)
let get_new_sym : Typ.Procname.t -> t let get_new_sym : Typ.Procname.t -> t
= fun pname -> = fun pname ->
@ -551,29 +559,23 @@ struct
let upper = Bound.of_sym (SymLinear.make pname (i+1)) in let upper = Bound.of_sym (SymLinear.make pname (i+1)) in
(lower, upper) (lower, upper)
let top : t let m1_255 = (Bound.minus_one, Bound._255)
= (Bound.MInf, Bound.PInf)
let pos : t let nat = (Bound.zero, Bound.PInf)
= (Bound.of_int 1, Bound.PInf)
let nat : t let one = of_bound Bound.one
= (Bound.of_int 0, Bound.PInf)
let zero : t let pos = (Bound.one, Bound.PInf)
= of_int 0
let one : t let top = (Bound.MInf, Bound.PInf)
= of_int 1
let true_sem : t let zero = of_bound Bound.zero
= one
let false_sem : t let true_sem = one
= zero
let unknown_bool : t let false_sem = zero
= (Bound.of_int 0, Bound.of_int 1)
let unknown_bool = join false_sem true_sem
let is_true : t -> bool let is_true : t -> bool
= fun (l, u) -> Bound.le (Bound.of_int 1) l || Bound.le u (Bound.of_int (-1)) = fun (l, u) -> Bound.le (Bound.of_int 1) l || Bound.le u (Bound.of_int (-1))
@ -869,20 +871,21 @@ let is_finite : t -> bool
| NonBottom x -> ItvPure.is_finite x | NonBottom x -> ItvPure.is_finite x
| Bottom -> false | Bottom -> false
let zero : t let false_sem = NonBottom ItvPure.false_sem
= of_int 0
let one : t let m1_255 = NonBottom ItvPure.m1_255
= of_int 1
let nat = NonBottom ItvPure.nat
let one = NonBottom ItvPure.one
let pos = NonBottom ItvPure.pos
let pos : t let true_sem = NonBottom ItvPure.true_sem
= NonBottom ItvPure.pos
let nat : t let unknown_bool = NonBottom ItvPure.unknown_bool
= NonBottom ItvPure.nat
let unknown_bool : t let zero = NonBottom ItvPure.zero
= NonBottom ItvPure.unknown_bool
let make : Bound.t -> Bound.t -> t let make : Bound.t -> Bound.t -> t
= fun l u -> if Bound.lt u l then Bottom else NonBottom (ItvPure.make l u) = fun l u -> if Bound.lt u l then Bottom else NonBottom (ItvPure.make l u)

Write Preview
Loading…
Cancel
Save