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

[inferbo] Extend alias domain to have multiple aliases on a variable

Browse Source 
Summary:
This diff extends the alias domain, so each variable can have multiple aliases.

It changed `KeyLhs` can be mapped to multiple alias targets in the `AliasMap` domain:

```
before : KeyLhs.t -> KeyRhs.t * AliasTarget.t
after  : KeyLhs.t -> KeyRhs.t -> AliasTarget.t
```

Reviewed By: ezgicicek

Differential Revision: D18062178

fbshipit-source-id: b325a6055
master
Sungkeun Cho 5 years ago committed by Facebook Github Bot
parent 0653284f75
commit fa571100df
8 changed files with 280 additions and 274 deletions
Show Stats Download Patch File Download Diff File

2
infer/src/absint/AbstractDomain.mli
Unescape View File

@ -79,8 +79,6 @@ module TopLifted (Domain : S) : WithTop with type t = Domain.t top_lifted
module TopLiftedUtils : sig module TopLiftedUtils : sig
val pp_top : Format.formatter -> unit val pp_top : Format.formatter -> unit
val pp : pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a top_lifted -> unit
end end
(** Cartesian product of two domains. *) (** Cartesian product of two domains. *)

9
infer/src/bufferoverrun/bufferOverrunAnalysis.ml
Unescape View File

@ -113,9 +113,12 @@ module TransferFunctions = struct
None None
with Caml.Not_found -> None ) with Caml.Not_found -> None )
in in
Option.value_map (Dom.Mem.find_ret_alias callee_exit_mem) ~default:mem ~f:(fun tgt -> match Dom.Mem.find_ret_alias callee_exit_mem with
Option.value_map (Dom.RhsAliasTarget.subst tgt ~subst_loc) ~default:mem | Bottom ->
~f:(fun (rhs, ret_alias) -> Dom.Mem.load_alias ret_id rhs ret_alias mem) ) mem
| NonBottom tgts ->
let ret_alias = Dom.AliasTargets.subst tgts ~subst_loc in
Dom.AliasTargets.fold (Dom.Mem.load_alias ret_id) ret_alias mem
in in
let ret_var = Loc.of_var (Var.of_id ret_id) in let ret_var = Loc.of_var (Var.of_id ret_id) in
let ret_val = let ret_val =

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

@ -874,6 +874,10 @@ module AliasTarget = struct
| Top | Top
[@@deriving compare] [@@deriving compare]
let top = Top
let is_top = function Top -> true | _ -> false
let equal = [%compare.equal: t] let equal = [%compare.equal: t]
let pp_with_key ~pp_lhs ~pp_rhs = let pp_with_key ~pp_lhs ~pp_rhs =
@ -902,6 +906,11 @@ module AliasTarget = struct
F.fprintf fmt "%t=?%t" pp_lhs pp_rhs F.fprintf fmt "%t=?%t" pp_lhs pp_rhs
let pp =
let pp_underscore fmt = F.pp_print_string fmt "_" in
pp_with_key ~pp_lhs:pp_underscore ~pp_rhs:pp_underscore
let get_locs = function let get_locs = function
| Simple {java_tmp= Some tmp} | Simple {java_tmp= Some tmp}
| Size {java_tmp= Some tmp} | Size {java_tmp= Some tmp}
@ -1041,95 +1050,58 @@ end
module KeyRhs = Loc module KeyRhs = Loc
module RhsAliasTarget = struct module AliasTargets = struct
type non_top = KeyRhs.t * AliasTarget.t include AbstractDomain.SafeInvertedMap (KeyRhs) (AliasTarget)
type t = non_top top_lifted
let top = Top
let is_top = function AbstractDomain.Types.Top -> true | AbstractDomain.Types.NonTop _ -> false
let leq ~lhs ~rhs =
match (lhs, rhs) with
| _, Top ->
true
| Top, _ ->
false
| NonTop (k1, v1), NonTop (k2, v2) ->
KeyRhs.equal k1 k2 && AliasTarget.leq ~lhs:v1 ~rhs:v2
let equal x y = leq ~lhs:x ~rhs:y && leq ~lhs:y ~rhs:x
let join x y =
match (x, y) with
| _, Top | Top, _ ->
Top
| NonTop (k1, v1), NonTop (k2, v2) ->
if KeyRhs.equal k1 k2 then NonTop (k1, AliasTarget.join v1 v2) else Top
let widen ~prev ~next ~num_iters =
match (prev, next) with
| _, Top | Top, _ ->
Top
| NonTop (k1, v1), NonTop (k2, v2) ->
if KeyRhs.equal k1 k2 then NonTop (k1, AliasTarget.widen ~prev:v1 ~next:v2 ~num_iters)
else Top
let pp_with_lhs ~pp_lhs fmt x = let pp_with_lhs ~pp_lhs fmt x =
AbstractDomain.TopLiftedUtils.pp fmt x ~pp:(fun fmt (rhs, v) -> let pp_sep fmt () = F.fprintf fmt ", @," in
AliasTarget.pp_with_key ~pp_lhs ~pp_rhs:(fun fmt -> KeyRhs.pp fmt rhs) fmt v ) let pp1 fmt (rhs, v) =
AliasTarget.pp_with_key ~pp_lhs ~pp_rhs:(fun fmt -> KeyRhs.pp fmt rhs) fmt v
in
F.pp_print_list ~pp_sep pp1 fmt (bindings x)
let pp = pp_with_lhs ~pp_lhs:(fun fmt -> F.pp_print_string fmt "_") let pp = pp_with_lhs ~pp_lhs:(fun fmt -> F.pp_print_string fmt "_")
let lift_map ~f = function Top -> Top | NonTop x -> NonTop (f x) let forget l x =
let not_use_l k v = not (KeyRhs.equal l k || AliasTarget.use_loc l v) in
let lift_map2 ~f = function Top -> Top | NonTop x -> f x filter not_use_l x
let forget l =
lift_map2 ~f:(fun ((rhs, v) as x) ->
if not (KeyRhs.equal l rhs || AliasTarget.use_loc l v) then NonTop x else Top )
let forget_size_alias arr_locs = let forget_size_alias arr_locs x =
lift_map2 ~f:(fun ((rhs, v) as x) -> let not_in_arr_locs k v = not (PowLoc.mem k arr_locs && AliasTarget.is_size v) in
if not (PowLoc.mem rhs arr_locs && AliasTarget.is_size v) then NonTop x else Top ) filter not_in_arr_locs x
let incr_size_alias loc = let incr_size_alias loc x = update loc (Option.map ~f:AliasTarget.incr_size_alias) x
lift_map ~f:(fun ((rhs, v) as x) ->
if Loc.equal loc rhs then (rhs, AliasTarget.incr_size_alias v) else x )
let incr_or_not_size_alias loc x =
update loc (Option.map ~f:AliasTarget.incr_or_not_size_alias) x
let incr_or_not_size_alias loc =
lift_map ~f:(fun ((rhs, v) as x) ->
if Loc.equal loc rhs then (rhs, AliasTarget.incr_or_not_size_alias v) else x )
let subst ~subst_loc x =
let subst ~subst_loc (rhs, tgt) = let accum_substed rhs tgt acc =
Option.map (subst_loc rhs) ~f:(fun rhs -> (rhs, AliasTarget.loc_map tgt ~f:subst_loc)) Option.value_map (subst_loc rhs) ~default:acc ~f:(fun rhs ->
add rhs (AliasTarget.loc_map tgt ~f:subst_loc) acc )
in
fold accum_substed x empty
let exists2 f (rhs1, v1) (rhs2, v2) = f rhs1 v1 rhs2 v2 let exists2 f x y = exists (fun k v -> exists (f k v) y) x
let is_simple_zero_alias = function let find_first_simple_zero_alias x =
| rhs, AliasTarget.Simple {i} when IntLit.iszero i -> let exception Found of KeyRhs.t in
Some rhs let is_simple_zero rhs = function
| AliasTarget.Simple {i} when IntLit.iszero i ->
raise (Found rhs)
| _ -> | _ ->
None ()
in
match iter is_simple_zero x with () -> None | exception Found rhs -> Some rhs
let set_java_tmp loc = lift_map ~f:(fun (k, v) -> (k, AliasTarget.set_java_tmp loc v))
let get_non_top = function Some (NonTop x) -> Some x | _ -> None
end end
module AliasMap = struct module AliasMap = struct
module M = AbstractDomain.SafeInvertedMap (KeyLhs) (RhsAliasTarget) module M = AbstractDomain.SafeInvertedMap (KeyLhs) (AliasTargets)
type t = M.t type t = M.t
@ -1142,9 +1114,7 @@ module AliasMap = struct
let pp : F.formatter -> t -> unit = let pp : F.formatter -> t -> unit =
fun fmt x -> fun fmt x ->
let pp_sep fmt () = F.fprintf fmt ", @," in let pp_sep fmt () = F.fprintf fmt ", @," in
let pp1 fmt (lhs, v) = let pp1 fmt (lhs, v) = AliasTargets.pp_with_lhs ~pp_lhs:(fun fmt -> KeyLhs.pp fmt lhs) fmt v in
RhsAliasTarget.pp_with_lhs ~pp_lhs:(fun fmt -> KeyLhs.pp fmt lhs) fmt v
in
F.pp_print_list ~pp_sep pp1 fmt (M.bindings x) F.pp_print_list ~pp_sep pp1 fmt (M.bindings x)
@ -1152,114 +1122,142 @@ module AliasMap = struct
let is_empty = M.is_empty let is_empty = M.is_empty
let add_alias ~lhs tgt m = M.add lhs (NonTop tgt) m let add_alias ~lhs ~rhs v m =
let add_to_tgts = function
| None ->
Some (AliasTargets.singleton rhs v)
| Some tgts ->
Some (AliasTargets.add rhs v tgts)
in
M.update lhs add_to_tgts m
let add_aliases ~lhs tgts m =
AliasTargets.fold (fun rhs v acc -> add_alias ~lhs ~rhs v acc) tgts m
let remove = M.remove let remove = M.remove
let find_id : Ident.t -> t -> RhsAliasTarget.non_top option = let find k m = M.find_opt k m |> Option.value ~default:AliasTargets.empty
fun id x -> M.find_opt (KeyLhs.of_id id) x |> RhsAliasTarget.get_non_top
let find_id : Ident.t -> t -> AliasTargets.t = fun id x -> find (KeyLhs.of_id id) x
let find_loc : Loc.t -> t -> RhsAliasTarget.non_top option = let find_loc : Loc.t -> t -> AliasTargets.t =
fun loc x -> fun loc x -> find (KeyLhs.LocKey loc) x |> AliasTargets.map (AliasTarget.set_java_tmp loc)
M.find_opt (KeyLhs.LocKey loc) x
|> Option.map ~f:(RhsAliasTarget.set_java_tmp loc)
|> RhsAliasTarget.get_non_top
let load : Ident.t -> Loc.t -> AliasTarget.t -> t -> t = let load : Ident.t -> Loc.t -> AliasTarget.t -> t -> t =
fun id loc tgt x -> fun id loc tgt x ->
if Loc.is_unknown loc || AliasTarget.is_unknown tgt then x if Loc.is_unknown loc || AliasTarget.is_unknown tgt then x
else else
let tgt = let tgts =
match tgt with match tgt with
| AliasTarget.Simple {i} when IntLit.iszero i && Language.curr_language_is Java -> | AliasTarget.Simple {i} when IntLit.iszero i && Language.curr_language_is Java ->
Option.value (find_loc loc x) ~default:(loc, tgt) find_loc loc x |> AliasTargets.add loc tgt
| _ -> | _ ->
(loc, tgt) AliasTargets.singleton loc tgt
in in
add_alias ~lhs:(KeyLhs.of_id id) tgt x add_aliases ~lhs:(KeyLhs.of_id id) tgts x
let forget : Loc.t -> t -> t = let forget : Loc.t -> t -> t =
fun l x -> fun l x ->
let forget1 k v = let forget1 k v = if KeyLhs.use_loc l k then AliasTargets.top else AliasTargets.forget l v in
if KeyLhs.use_loc l k then RhsAliasTarget.top else RhsAliasTarget.forget l v
in
M.mapi forget1 x M.mapi forget1 x
let store : Loc.t -> Ident.t -> t -> t = let store : Loc.t -> Ident.t -> t -> t =
fun l id x -> fun l id x ->
if Language.curr_language_is Java then if Language.curr_language_is Java then
if Loc.is_frontend_tmp l then let tgts = find_id id x in
Option.value_map (find_id id x) ~default:x ~f:(fun tgt -> if Loc.is_frontend_tmp l then add_aliases ~lhs:(KeyLhs.of_loc l) tgts x
add_alias ~lhs:(KeyLhs.of_loc l) tgt x )
else else
match find_id id x with let accum_java_tmp_alias rhs tgt acc =
| Some (rhs, AliasTarget.Simple {i}) when IntLit.iszero i && Loc.is_frontend_tmp rhs -> match tgt with
add_alias ~lhs:(KeyLhs.of_id id) (l, AliasTarget.Simple {i; java_tmp= Some rhs}) x | AliasTarget.Simple {i} when IntLit.iszero i && Loc.is_frontend_tmp rhs ->
|> add_alias ~lhs:(KeyLhs.of_loc rhs) (l, AliasTarget.Simple {i; java_tmp= None}) add_alias ~lhs:(KeyLhs.of_id id) ~rhs:l
(AliasTarget.Simple {i; java_tmp= Some rhs})
acc
|> add_alias ~lhs:(KeyLhs.of_loc rhs) ~rhs:l (AliasTarget.Simple {i; java_tmp= None})
| _ -> | _ ->
x acc
in
AliasTargets.fold accum_java_tmp_alias tgts x
else x else x
let add_zero_size_alias ~size ~arr x = let add_zero_size_alias ~size ~arr x =
add_alias ~lhs:(KeyLhs.of_loc size) add_alias ~lhs:(KeyLhs.of_loc size) ~rhs:arr
(arr, AliasTarget.Size {alias_typ= Eq; i= IntLit.zero; java_tmp= None}) (AliasTarget.Size {alias_typ= Eq; i= IntLit.zero; java_tmp= None})
x x
let incr_size_alias loc x = M.map (RhsAliasTarget.incr_size_alias loc) x let incr_size_alias loc x = M.map (AliasTargets.incr_size_alias loc) x
let incr_or_not_size_alias loc x = M.map (RhsAliasTarget.incr_or_not_size_alias loc) x let incr_or_not_size_alias loc x = M.map (AliasTargets.incr_or_not_size_alias loc) x
let forget_size_alias arr_locs x = M.map (RhsAliasTarget.forget_size_alias arr_locs) x let forget_size_alias arr_locs x = M.map (AliasTargets.forget_size_alias arr_locs) x
let store_n ~prev loc id n x = let store_n ~prev loc id n x =
match find_id id prev with let accum_size_alias rhs tgt acc =
| Some (rhs, AliasTarget.Size {alias_typ; i}) -> match tgt with
add_alias ~lhs:(KeyLhs.of_loc loc) | AliasTarget.Size {alias_typ; i} ->
(rhs, AliasTarget.Size {alias_typ; i= IntLit.add i n; java_tmp= None}) add_alias ~lhs:(KeyLhs.of_loc loc) ~rhs
x (AliasTarget.Size {alias_typ; i= IntLit.add i n; java_tmp= None})
acc
| _ -> | _ ->
x acc
in
AliasTargets.fold accum_size_alias (find_id id prev) x
let add_iterator_offset_alias id arr x = let add_iterator_offset_alias id arr x =
add_alias ~lhs:(KeyLhs.of_id id) add_alias ~lhs:(KeyLhs.of_id id) ~rhs:arr
(arr, AliasTarget.IteratorOffset {alias_typ= Eq; i= IntLit.zero; java_tmp= None}) (AliasTarget.IteratorOffset {alias_typ= Eq; i= IntLit.zero; java_tmp= None})
x x
let incr_iterator_offset_alias id x = let incr_iterator_offset_alias id x =
match M.find_opt (KeyLhs.of_id id) x with let accum_incr_iterator_offset_alias rhs tgt acc =
| Some (NonTop (rhs, AliasTarget.IteratorOffset ({i; java_tmp} as tgt))) -> match tgt with
| AliasTarget.IteratorOffset ({i; java_tmp} as tgt) ->
let i = IntLit.(add i one) in let i = IntLit.(add i one) in
let x = let acc =
add_alias ~lhs:(KeyLhs.of_id id) (rhs, AliasTarget.IteratorOffset {tgt with i}) x add_alias ~lhs:(KeyLhs.of_id id) ~rhs (AliasTarget.IteratorOffset {tgt with i}) acc
in in
Option.value_map java_tmp ~default:x ~f:(fun java_tmp -> Option.value_map java_tmp ~default:x ~f:(fun java_tmp ->
add_alias ~lhs:(KeyLhs.of_loc java_tmp) add_alias ~lhs:(KeyLhs.of_loc java_tmp) ~rhs
(rhs, AliasTarget.IteratorOffset {tgt with i; java_tmp= None}) (AliasTarget.IteratorOffset {tgt with i; java_tmp= None})
x ) acc )
| _ ->
acc
in
match M.find_opt (KeyLhs.of_id id) x with
| Some tgts ->
AliasTargets.fold accum_incr_iterator_offset_alias tgts x
| _ -> | _ ->
x x
let add_iterator_has_next_alias ~ret_id ~iterator x = let add_iterator_has_next_alias ~ret_id ~iterator x =
let accum_has_next_alias _rhs tgt acc =
match tgt with
| AliasTarget.IteratorOffset {java_tmp= Some java_tmp} ->
add_alias ~lhs:(KeyLhs.of_id ret_id) ~rhs:java_tmp
(AliasTarget.IteratorHasNext {java_tmp= None})
acc
| _ ->
acc
in
match M.find_opt (KeyLhs.of_id iterator) x with match M.find_opt (KeyLhs.of_id iterator) x with
| Some (NonTop (_rhs, AliasTarget.IteratorOffset {java_tmp= Some java_tmp})) -> | Some tgts ->
add_alias ~lhs:(KeyLhs.of_id ret_id) AliasTargets.fold accum_has_next_alias tgts x
(java_tmp, AliasTarget.IteratorHasNext {java_tmp= None})
x
| _ -> | _ ->
x x
end end
module AliasRet = struct module AliasRet = struct
include AbstractDomain.Flat (RhsAliasTarget) include AliasTargets
let pp : F.formatter -> t -> unit = fun fmt x -> F.pp_print_string fmt "ret=" ; pp fmt x let pp : F.formatter -> t -> unit = fun fmt x -> F.pp_print_string fmt "ret=" ; pp fmt x
end end
@ -1289,23 +1287,17 @@ module Alias = struct
AliasRet.pp x.ret AliasRet.pp x.ret
let bot : t = {map= AliasMap.empty; ret= AliasRet.bottom} let init : t = {map= AliasMap.empty; ret= AliasRet.empty}
let lift_map : (AliasMap.t -> AliasMap.t) -> t -> t = fun f a -> {a with map= f a.map} let lift_map : (AliasMap.t -> AliasMap.t) -> t -> t = fun f a -> {a with map= f a.map}
let bind_map : (AliasMap.t -> 'a) -> t -> 'a = fun f a -> f a.map let bind_map : (AliasMap.t -> 'a) -> t -> 'a = fun f a -> f a.map
let find_id : Ident.t -> t -> RhsAliasTarget.non_top option = let find_id : Ident.t -> t -> AliasTargets.t = fun x -> bind_map (AliasMap.find_id x)
fun x -> bind_map (AliasMap.find_id x)
let find_loc : Loc.t -> t -> AliasTargets.t = fun x -> bind_map (AliasMap.find_loc x)
let find_loc : Loc.t -> t -> RhsAliasTarget.non_top option = let find_ret : t -> AliasTargets.t = fun x -> x.ret
fun x -> bind_map (AliasMap.find_loc x)
let find_ret : t -> RhsAliasTarget.non_top option =
fun x -> AliasRet.get x.ret |> RhsAliasTarget.get_non_top
let load : Ident.t -> Loc.t -> AliasTarget.t -> t -> t = let load : Ident.t -> Loc.t -> AliasTarget.t -> t -> t =
fun id loc tgt -> lift_map (AliasMap.load id loc tgt) fun id loc tgt -> lift_map (AliasMap.load id loc tgt)
@ -1317,10 +1309,7 @@ module Alias = struct
match e with match e with
| Exp.Var l -> | Exp.Var l ->
let a = lift_map (AliasMap.store loc l) a in let a = lift_map (AliasMap.store loc l) a in
if Loc.is_return loc then if Loc.is_return loc then {a with ret= find_id l a} else a
let update_ret retl = {a with ret= AliasRet.v (NonTop retl)} in
Option.value_map (find_id l a) ~default:a ~f:update_ret
else a
| Exp.BinOp (Binop.PlusA _, Exp.Var id, Exp.Const (Const.Cint i)) | Exp.BinOp (Binop.PlusA _, Exp.Var id, Exp.Const (Const.Cint i))
| Exp.BinOp (Binop.PlusA _, Exp.Const (Const.Cint i), Exp.Var id) -> | Exp.BinOp (Binop.PlusA _, Exp.Const (Const.Cint i), Exp.Var id) ->
lift_map (AliasMap.load id loc (AliasTarget.Simple {i= IntLit.neg i; java_tmp= None})) a lift_map (AliasMap.load id loc (AliasTarget.Simple {i= IntLit.neg i; java_tmp= None})) a
@ -1356,31 +1345,18 @@ module Alias = struct
let add_empty_size_alias : Loc.t -> PowLoc.t -> t -> t = let add_empty_size_alias : Loc.t -> PowLoc.t -> t -> t =
fun loc arr_locs prev -> fun loc arr_locs prev ->
let a = lift_map (AliasMap.forget loc) prev in let accum_empty_size_alias arr_loc acc =
match PowLoc.is_singleton_or_more arr_locs with lift_map (AliasMap.add_zero_size_alias ~size:loc ~arr:arr_loc) acc
| IContainer.Singleton arr_loc -> in
lift_map (AliasMap.add_zero_size_alias ~size:loc ~arr:arr_loc) a PowLoc.fold accum_empty_size_alias arr_locs (lift_map (AliasMap.forget loc) prev)
| More ->
(* NOTE: Keeping only one alias here is suboptimal, but current alias domain can keep one
alias for each ident, which will be extended later. *)
let arr_loc = PowLoc.min_elt arr_locs in
lift_map (AliasMap.add_zero_size_alias ~size:loc ~arr:arr_loc) a
| Empty ->
a
let add_iterator_offset_alias : Ident.t -> PowLoc.t -> t -> t = let add_iterator_offset_alias : Ident.t -> PowLoc.t -> t -> t =
fun id arr_locs a -> fun id arr_locs a ->
match PowLoc.is_singleton_or_more arr_locs with let accum_iterator_offset_alias arr_loc acc =
| IContainer.Singleton arr_loc -> lift_map (AliasMap.add_iterator_offset_alias id arr_loc) acc
lift_map (AliasMap.add_iterator_offset_alias id arr_loc) a in
| More -> PowLoc.fold accum_iterator_offset_alias arr_locs a
(* NOTE: Keeping only one alias here is suboptimal, but current alias domain can keep one
alias for each ident, which will be extended later. *)
let arr_loc = PowLoc.min_elt arr_locs in
lift_map (AliasMap.add_iterator_offset_alias id arr_loc) a
| Empty ->
a
let incr_iterator_offset_alias : Ident.t -> t -> t = let incr_iterator_offset_alias : Ident.t -> t -> t =
@ -1798,7 +1774,7 @@ module MemReach = struct
fun oenv -> fun oenv ->
{ stack_locs= StackLocs.bot { stack_locs= StackLocs.bot
; mem_pure= MemPure.bot ; mem_pure= MemPure.bot
; alias= Alias.bot ; alias= Alias.init
; latest_prune= LatestPrune.top ; latest_prune= LatestPrune.top
; relation= Relation.empty ; relation= Relation.empty
; oenv= GOption.GSome oenv } ; oenv= GOption.GSome oenv }
@ -1877,33 +1853,29 @@ module MemReach = struct
PowLoc.fold find_join locs Val.bot PowLoc.fold find_join locs Val.bot
let find_alias_id : Ident.t -> _ t0 -> RhsAliasTarget.non_top option = let find_alias_id : Ident.t -> _ t0 -> AliasTargets.t = fun k m -> Alias.find_id k m.alias
fun k m -> Alias.find_id k m.alias
let find_alias_loc : Loc.t -> _ t0 -> AliasTargets.t = fun k m -> Alias.find_loc k m.alias
let find_alias_loc : Loc.t -> _ t0 -> RhsAliasTarget.non_top option = let find_simple_alias : Ident.t -> _ t0 -> (Loc.t * IntLit.t) list =
fun k m -> Alias.find_loc k m.alias let accum_simple_alias l tgt acc =
match tgt with AliasTarget.Simple {i} -> (l, i) :: acc | _ -> acc
in
let find_simple_alias : Ident.t -> _ t0 -> (Loc.t * IntLit.t) option = fun k m -> AliasTargets.fold accum_simple_alias (Alias.find_id k m.alias) []
fun k m ->
match Alias.find_id k m.alias with
| Some (l, AliasTarget.Simple {i}) ->
Some (l, i)
| _ ->
None
let find_size_alias : Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * Loc.t option) option = let find_size_alias : Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * Loc.t option) list =
fun k m -> let accum_size_alias l tgt acc =
match Alias.find_id k m.alias with match tgt with
| Some (l, AliasTarget.Size {alias_typ; java_tmp}) -> | AliasTarget.Size {alias_typ; java_tmp} ->
Some (alias_typ, l, java_tmp) (alias_typ, l, java_tmp) :: acc
| _ -> | _ ->
None acc
in
fun k m -> AliasTargets.fold accum_size_alias (Alias.find_id k m.alias) []
let find_ret_alias : _ t0 -> RhsAliasTarget.non_top option = fun m -> Alias.find_ret m.alias let find_ret_alias : _ t0 -> AliasTargets.t = fun m -> Alias.find_ret m.alias
let load_alias : Ident.t -> Loc.t -> AliasTarget.t -> t -> t = let load_alias : Ident.t -> Loc.t -> AliasTarget.t -> t -> t =
fun id loc tgt m -> {m with alias= Alias.load id loc tgt m.alias} fun id loc tgt m -> {m with alias= Alias.load id loc tgt m.alias}
@ -2060,8 +2032,7 @@ module MemReach = struct
| _ -> | _ ->
acc acc
in in
let default = (m, PrunePairs.empty) in List.fold (find_simple_alias r m) ~init:(m, PrunePairs.empty) ~f:apply_simple_alias1
Option.value_map ~default (find_simple_alias r m) ~f:(apply_simple_alias1 default)
| LatestPrune.VRet (x, prunes, _), Exp.Var r | LatestPrune.VRet (x, prunes, _), Exp.Var r
| LatestPrune.VRet (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) -> | LatestPrune.VRet (x, _, prunes), Exp.UnOp (Unop.LNot, Exp.Var r, _) ->
if Ident.equal x r then (apply_prunes prunes m, prunes) else (m, PrunePairs.empty) if Ident.equal x r then (apply_prunes prunes m, prunes) else (m, PrunePairs.empty)
@ -2076,12 +2047,16 @@ module MemReach = struct
if IntLit.isone i then {m with latest_prune= LatestPrune.TrueBranch (x, p)} if IntLit.isone i then {m with latest_prune= LatestPrune.TrueBranch (x, p)}
else if IntLit.iszero i then {m with latest_prune= LatestPrune.FalseBranch (x, p)} else if IntLit.iszero i then {m with latest_prune= LatestPrune.FalseBranch (x, p)}
else {m with latest_prune= LatestPrune.forget updated_locs m.latest_prune} else {m with latest_prune= LatestPrune.forget updated_locs m.latest_prune}
| Lvar return, _, _ when Pvar.is_return return -> ( | Lvar return, _, _ when Pvar.is_return return ->
match Alias.find_ret m.alias with let tgts = Alias.find_ret m.alias in
| Some (Loc.Var (ProgramVar pvar), AliasTarget.Simple {i}) when IntLit.iszero i -> let replace_latest_prune l tgt acc =
{m with latest_prune= LatestPrune.replace ~from:pvar ~to_:return m.latest_prune} match (l, tgt) with
| Loc.Var (ProgramVar pvar), AliasTarget.Simple {i} when IntLit.iszero i ->
{acc with latest_prune= LatestPrune.replace ~from:pvar ~to_:return m.latest_prune}
| _ -> | _ ->
m ) acc
in
AliasTargets.fold replace_latest_prune tgts m
| _, _, _ -> | _, _, _ ->
{m with latest_prune= LatestPrune.forget updated_locs m.latest_prune} {m with latest_prune= LatestPrune.forget updated_locs m.latest_prune}
@ -2294,24 +2269,29 @@ module Mem = struct
fun k -> f_lift_default ~default:None (MemReach.find_opt k) fun k -> f_lift_default ~default:None (MemReach.find_opt k)
let find_alias_id : Ident.t -> _ t0 -> RhsAliasTarget.non_top option = let find_alias_id : Ident.t -> _ t0 -> AliasTargets.t =
fun k -> f_lift_default ~default:None (MemReach.find_alias_id k) fun k -> f_lift_default ~default:AliasTargets.empty (MemReach.find_alias_id k)
let find_alias_loc : Loc.t -> _ t0 -> RhsAliasTarget.non_top option = let find_alias_loc : Loc.t -> _ t0 -> AliasTargets.t =
fun k -> f_lift_default ~default:None (MemReach.find_alias_loc k) fun k -> f_lift_default ~default:AliasTargets.empty (MemReach.find_alias_loc k)
let find_simple_alias : Ident.t -> _ t0 -> (Loc.t * IntLit.t) option = let find_simple_alias : Ident.t -> _ t0 -> (Loc.t * IntLit.t) list =
fun k -> f_lift_default ~default:None (MemReach.find_simple_alias k) fun k -> f_lift_default ~default:[] (MemReach.find_simple_alias k)
let find_size_alias : Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * Loc.t option) option = let find_size_alias : Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * Loc.t option) list =
fun k -> f_lift_default ~default:None (MemReach.find_size_alias k) fun k -> f_lift_default ~default:[] (MemReach.find_size_alias k)
let find_ret_alias : _ t0 -> RhsAliasTarget.non_top option = let find_ret_alias : _ t0 -> AliasTargets.t bottom_lifted =
fun m -> match m with Bottom | ExcRaised -> None | NonBottom m' -> MemReach.find_ret_alias m' fun m ->
match m with
| Bottom | ExcRaised ->
Bottom
| NonBottom m' ->
NonBottom (MemReach.find_ret_alias m')
let load_alias : Ident.t -> Loc.t -> AliasTarget.t -> t -> t = let load_alias : Ident.t -> Loc.t -> AliasTarget.t -> t -> t =

3
infer/src/bufferoverrun/bufferOverrunModels.ml
Unescape View File

@ -113,8 +113,7 @@ let malloc ~can_be_zero size_exp =
let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in
let path = let path =
Dom.Mem.find_simple_alias id mem Dom.Mem.find_simple_alias id mem
|> Option.value_map ~default:None ~f:(fun (rhs, i) -> |> List.find_map ~f:(fun (rhs, i) -> if IntLit.iszero i then Loc.get_path rhs else None)
if IntLit.iszero i then Loc.get_path rhs else None )
in in
let offset, size = (Itv.zero, Dom.Val.get_itv length) in let offset, size = (Itv.zero, Dom.Val.get_itv length) in
let represents_multiple_values = not (Itv.is_one size) in let represents_multiple_values = not (Itv.is_one size) in

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

@ -27,15 +27,11 @@ let eval_const : Typ.IntegerWidths.t -> Const.t -> Val.t =
let rec must_alias : Exp.t -> Exp.t -> Mem.t -> bool = let rec must_alias : Exp.t -> Exp.t -> Mem.t -> bool =
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 ->
let same_alias rhs1 tgt1 rhs2 tgt2 = let same_alias rhs1 tgt1 rhs2 tgt2 =
KeyRhs.equal rhs1 rhs2 && AliasTarget.equal tgt1 tgt2 && not (Mem.is_rep_multi_loc rhs1 m) KeyRhs.equal rhs1 rhs2 && AliasTarget.equal tgt1 tgt2 && not (Mem.is_rep_multi_loc rhs1 m)
in in
match (Mem.find_alias_id x1 m, Mem.find_alias_id x2 m) with AliasTargets.exists2 same_alias (Mem.find_alias_id x1 m) (Mem.find_alias_id x2 m)
| Some x1', Some x2' ->
RhsAliasTarget.exists2 same_alias x1' x2'
| _, _ ->
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) ->
@ -314,13 +310,9 @@ let rec eval_locs : Exp.t -> Mem.t -> PowLoc.t =
let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t = let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
fun integer_type_widths exp mem -> fun integer_type_widths exp mem ->
match exp with match exp with
| Exp.Var id -> ( | Exp.Var id ->
match Mem.find_alias_id id mem with let alias_loc = AliasTargets.find_first_simple_zero_alias (Mem.find_alias_id id mem) in
| Some tgt ->
let alias_loc = RhsAliasTarget.is_simple_zero_alias tgt in
Option.value_map alias_loc ~default:Val.bot ~f:(fun loc -> Mem.find loc mem) Option.value_map alias_loc ~default:Val.bot ~f:(fun loc -> Mem.find loc mem)
| None ->
Val.bot )
| Exp.Lvar pvar -> | Exp.Lvar pvar ->
Mem.find (Loc.of_pvar pvar) mem Mem.find (Loc.of_pvar pvar) mem
| Exp.BinOp (bop, e1, e2) -> | Exp.BinOp (bop, e1, e2) ->
@ -540,8 +532,9 @@ module Prune = struct
let prune_has_next ~true_branch iterator ({mem} as astate) = let prune_has_next ~true_branch iterator ({mem} as astate) =
match Mem.find_alias_loc iterator mem with let accum_pruned arr_loc tgt acc =
| Some (arr_loc, AliasTarget.IteratorOffset {alias_typ; i}) when IntLit.(eq i zero) -> match tgt with
| AliasTarget.IteratorOffset {alias_typ; i} when IntLit.(eq i zero) ->
let length = collection_length_of_iterator iterator mem |> Val.get_itv in let length = collection_length_of_iterator iterator mem |> Val.get_itv in
let v = Mem.find arr_loc mem in let v = Mem.find arr_loc mem in
let v = let v =
@ -551,46 +544,54 @@ module Prune = struct
in in
prune_f v length prune_f v length
in in
update_mem_in_prune arr_loc v astate update_mem_in_prune arr_loc v acc
| _ -> | _ ->
astate acc
in
AliasTargets.fold accum_pruned (Mem.find_alias_loc iterator mem) astate
let prune_unop : Exp.t -> t -> t = let prune_unop : Exp.t -> t -> t =
fun e ({mem} as astate) -> fun e ({mem} as astate) ->
match e with match e with
| Exp.Var x -> ( | Exp.Var x ->
match Mem.find_alias_id x mem with let accum_prune_var rhs tgt acc =
| Some (rhs, AliasTarget.Simple {i}) when IntLit.iszero i -> match tgt with
| AliasTarget.Simple {i} when IntLit.iszero i ->
let v = Mem.find rhs mem in let v = Mem.find rhs mem in
let v' = Val.prune_ne_zero v in let v' = Val.prune_ne_zero v in
update_mem_in_prune rhs v' astate update_mem_in_prune rhs v' acc
| Some (rhs, AliasTarget.Empty) -> | AliasTarget.Empty ->
let v = Mem.find rhs mem in let v = Mem.find rhs mem in
let v' = Val.prune_length_eq_zero v in let v' = Val.prune_length_eq_zero v in
update_mem_in_prune rhs v' astate update_mem_in_prune rhs v' acc
| Some (rhs, AliasTarget.Fgets) -> | AliasTarget.Fgets ->
let strlen_loc = Loc.of_c_strlen rhs in let strlen_loc = Loc.of_c_strlen rhs in
let v' = Val.prune_ge_one (Mem.find strlen_loc mem) in let v' = Val.prune_ge_one (Mem.find strlen_loc mem) in
update_mem_in_prune strlen_loc v' astate update_mem_in_prune strlen_loc v' acc
| Some (rhs, AliasTarget.IteratorHasNext _) -> | AliasTarget.IteratorHasNext _ ->
prune_has_next ~true_branch:true rhs astate prune_has_next ~true_branch:true rhs acc
| _ -> | _ ->
astate ) acc
| Exp.UnOp (Unop.LNot, Exp.Var x, _) -> ( in
match Mem.find_alias_id x mem with AliasTargets.fold accum_prune_var (Mem.find_alias_id x mem) astate
| Some (rhs, AliasTarget.Simple {i}) when IntLit.iszero i -> | Exp.UnOp (Unop.LNot, Exp.Var x, _) ->
let accum_prune_not_var rhs tgt acc =
match tgt with
| AliasTarget.Simple {i} when IntLit.iszero i ->
let v = Mem.find rhs mem in let v = Mem.find rhs mem in
let v' = Val.prune_eq_zero v in let v' = Val.prune_eq_zero v in
update_mem_in_prune rhs v' astate update_mem_in_prune rhs v' acc
| Some (rhs, AliasTarget.Empty) -> | AliasTarget.Empty ->
let v = Mem.find rhs mem in let v = Mem.find rhs mem in
let v' = Val.prune_length_ge_one v in let v' = Val.prune_length_ge_one v in
update_mem_in_prune rhs v' astate update_mem_in_prune rhs v' acc
| Some (rhs, AliasTarget.IteratorHasNext _) -> | AliasTarget.IteratorHasNext _ ->
prune_has_next ~true_branch:false rhs astate prune_has_next ~true_branch:false rhs acc
| _ -> | _ ->
astate ) acc
in
AliasTargets.fold accum_prune_not_var (Mem.find_alias_id x mem) astate
| _ -> | _ ->
astate astate
@ -632,7 +633,7 @@ module Prune = struct
let prune_simple_alias = let prune_simple_alias =
let prune_alias_core ~val_prune_eq ~val_prune_le:_ ~make_pruning_exp integer_type_widths x e let prune_alias_core ~val_prune_eq ~val_prune_le:_ ~make_pruning_exp integer_type_widths x e
({mem} as astate) = ({mem} as astate) =
Option.value_map (Mem.find_simple_alias x mem) ~default:astate ~f:(fun (lv, i) -> List.fold (Mem.find_simple_alias x mem) ~init:astate ~f:(fun acc (lv, i) ->
let lhs = Mem.find lv mem in let lhs = Mem.find lv mem in
let rhs = let rhs =
let v' = eval integer_type_widths e mem in let v' = eval integer_type_widths e mem in
@ -640,7 +641,7 @@ module Prune = struct
in in
let v = val_prune_eq lhs rhs in let v = val_prune_eq lhs rhs in
let pruning_exp = make_pruning_exp ~lhs ~rhs in let pruning_exp = make_pruning_exp ~lhs ~rhs in
update_mem_in_prune lv v ~pruning_exp astate ) update_mem_in_prune lv v ~pruning_exp acc )
in in
gen_prune_alias_functions ~prune_alias_core gen_prune_alias_functions ~prune_alias_core
@ -648,8 +649,8 @@ module Prune = struct
let prune_size_alias = let prune_size_alias =
let prune_alias_core ~val_prune_eq ~val_prune_le ~make_pruning_exp integer_type_widths x e let prune_alias_core ~val_prune_eq ~val_prune_le ~make_pruning_exp integer_type_widths x e
({mem} as astate) = ({mem} as astate) =
Option.value_map (Mem.find_size_alias x mem) ~default:astate List.fold (Mem.find_size_alias x mem) ~init:astate
~f:(fun (alias_typ, lv, java_tmp) -> ~f:(fun astate (alias_typ, lv, java_tmp) ->
let array_v = Mem.find lv mem in let array_v = Mem.find lv mem in
let size = let size =
Val.get_array_blk array_v |> ArrayBlk.sizeof |> Val.of_itv Val.get_array_blk array_v |> ArrayBlk.sizeof |> Val.of_itv

24
infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java
Unescape View File

@ -159,4 +159,28 @@ class ArrayListTest {
} // b.size is zero here } // b.size is zero here
int j = b.get(0); int j = b.get(0);
} }
void multi_adds_in_loop_iterator_ok(ArrayList<Integer> b) {
ArrayList<Integer> a1 = new ArrayList<>();
ArrayList<Integer> a2 = new ArrayList<>();
for (Integer i : b) {
a1.add(i);
a2.add(i);
}
int j;
j = a1.get(b.size() - 1);
j = a2.get(b.size() - 1);
}
void multi_adds_in_loop_iterator_bad(ArrayList<Integer> b) {
ArrayList<Integer> a1 = new ArrayList<>();
ArrayList<Integer> a2 = new ArrayList<>();
for (Integer i : b) {
a1.add(i);
a2.add(i);
}
int j;
j = a1.get(b.size() + 1);
j = a2.get(b.size() + 1);
}
} }

1
infer/tests/codetoanalyze/java/bufferoverrun/issues.exp
Unescape View File

@ -14,6 +14,7 @@ codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_b
codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator2_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Array declaration,Assignment,<Length trace>,Parameter `b.elements[*]`,Array access: Offset: [0, b.length] Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator2_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Array declaration,Assignment,<Length trace>,Parameter `b.elements[*]`,Array access: Offset: [0, b.length] Size: b.length]
codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator_bad(java.util.ArrayList):void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `b.elements[*]`,Assignment,<Length trace>,Array declaration,Array access: Offset: b.length + 1 Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator_bad(java.util.ArrayList):void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `b.elements[*]`,Assignment,<Length trace>,Array declaration,Array access: Offset: b.length + 1 Size: b.length]
codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_negative_bad():void, 2, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_negative_bad():void, 2, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1]
codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.multi_adds_in_loop_iterator_bad(java.util.ArrayList):void, 8, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `b.elements[*]`,Assignment,<Length trace>,Array declaration,Array access: Offset: b.length + 1 Size: b.length]
codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.remove_in_loop_iterator_good_FP(java.util.ArrayList):void, 14, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `b.elements[*]`,Assignment,<Length trace>,Parameter `b.elements[*]`,Array access: Offset: b.length Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.remove_in_loop_iterator_good_FP(java.util.ArrayList):void, 14, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `b.elements[*]`,Assignment,<Length trace>,Parameter `b.elements[*]`,Array access: Offset: b.length Size: b.length]
codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10] codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10]
codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `this.yy`,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32] codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `this.yy`,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]

10
infer/tests/codetoanalyze/java/performance/issues.exp
Unescape View File

@ -30,17 +30,17 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remov
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 1 Size: 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 1 Size: 1]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.boolean_control_var_linear():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 19 ⋅ this.arr.length + 4 ⋅ (this.arr.length + 1), O(this.arr.length), degree = 1,{this.arr.length + 1},Loop at line 290,{this.arr.length},Loop at line 290] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.boolean_control_var_linear():void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 19 ⋅ this.arr.length + 4 ⋅ (this.arr.length + 1), O(this.arr.length), degree = 1,{this.arr.length + 1},Loop at line 290,{this.arr.length},Loop at line 290]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_init_with_put_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 16 ⋅ (a.length + 1), O(a.length), degree = 1,{a.length + 1},call to HashMap ArrayListTest.init_with_put_linear(ArrayList),Loop at line 299] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_init_with_put_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 13 ⋅ a.length + 3 ⋅ (a.length + 1), O(a.length), degree = 1,{a.length + 1},call to HashMap ArrayListTest.init_with_put_linear(ArrayList),Loop at line 299,{a.length},call to HashMap ArrayListTest.init_with_put_linear(ArrayList),Loop at line 299]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + list.length × log(list.length), O(list.length × log(list.length)), degree = 1 + 1⋅log,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + list.length × log(list.length), O(list.length × log(list.length)), degree = 1 + 1⋅log,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 240,{l.length + list.length},Loop at line 240] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 240,{l.length + list.length},Loop at line 240]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 247,{l.length + list.length},Loop at line 247] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), O((l.length + list.length)), degree = 1,{l.length + list.length + 1},Loop at line 247,{l.length + list.length},Loop at line 247]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 222,{list.length},Loop at line 222] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 222,{list.length},Loop at line 222]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 5 ⋅ (list.length + 4) + 3 ⋅ (list.length + 5), O(list.length), degree = 1,{list.length + 5},Loop at line 233,{list.length + 4},Loop at line 233] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 5 ⋅ (list.length + 4) + 3 ⋅ (list.length + 5), O(list.length), degree = 1,{list.length + 5},Loop at line 233,{list.length + 4},Loop at line 233]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.empty_list_constant(int):void, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.empty_list_constant(int):void, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.init_with_put_linear(java.util.ArrayList):java.util.HashMap, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 16 ⋅ (a.length + 1), O(a.length), degree = 1,{a.length + 1},Loop at line 299] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.init_with_put_linear(java.util.ArrayList):java.util.HashMap, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 13 ⋅ a.length + 3 ⋅ (a.length + 1), O(a.length), degree = 1,{a.length + 1},Loop at line 299,{a.length},Loop at line 299]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ list.length, O(list.length), degree = 1,{list.length},Loop at line 15] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ list.length, O(list.length), degree = 1,{list.length},Loop at line 15]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ list.length + 2 ⋅ list.length × (11-max(10, list.elements)) + 3 ⋅ (list.length + 1) × (11-max(10, list.elements)), O(list.length × (-list.elements + 11)), degree = 2,{11-max(10, list.elements)},Loop at line 188,{list.length + 1},Loop at line 188,{11-max(10, list.elements)},Loop at line 188,{list.length},Loop at line 188] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ list.length + 2 ⋅ list.length × (11-max(10, list.elements)) + 3 ⋅ (list.length + 1) × (11-max(10, list.elements)), O(list.length × (-list.elements + 11)), degree = 2,{11-max(10, list.elements)},Loop at line 188,{list.length + 1},Loop at line 188,{11-max(10, list.elements)},Loop at line 188,{list.length},Loop at line 188]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 14 ⋅ (list1.length + 1), O(list1.length), degree = 1,{list1.length + 1},Loop at line 179] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 11 ⋅ list1.length + 3 ⋅ (list1.length + 1), O(list1.length), degree = 1,{list1.length + 1},Loop at line 179,{list1.length},Loop at line 179]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length, O(list.length), degree = 1,{list.length},Loop at line 20] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length, O(list.length), degree = 1,{list.length},Loop at line 20]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 10 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 171,{list.length},Loop at line 171] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 10 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 171,{list.length},Loop at line 171]
codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 8 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 165,{list.length},Loop at line 165] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 8 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 165,{list.length},Loop at line 165]
@ -89,7 +89,7 @@ codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performanc
codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7963049, O(1), degree = 0] codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7963049, O(1), degree = 0]
codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ k, O(k), degree = 1,{k},Loop at line 92] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.FN_loop2(int):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ k, O(k), degree = 1,{k},Loop at line 92]
codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.call_inputstream_read_linear(java.io.InputStream):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 28604, O(1), degree = 0] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.call_inputstream_read_linear(java.io.InputStream):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 27304, O(1), degree = 0]
codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.ignore_boolean_symbols_linear(boolean,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), O(n), degree = 1,{1+max(0, n)},Loop at line 135,{n},Loop at line 135] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.ignore_boolean_symbols_linear(boolean,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ n + 2 ⋅ (1+max(0, n)), O(n), degree = 1,{1+max(0, n)},Loop at line 135,{n},Loop at line 135]
codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1202, O(1), degree = 0] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop0_bad():int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1202, O(1), degree = 0]
codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop1_bad():int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1303, O(1), degree = 0] codetoanalyze/java/performance/Cost_test.java, codetoanalyze.java.performance.Cost_test.loop1_bad():int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1303, O(1), degree = 0]
@ -151,7 +151,7 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util
codetoanalyze/java/performance/ListTest.java, ListTest.asList_linear(java.lang.String[]):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 8 ⋅ array.length + 3 ⋅ (array.length + 1), O(array.length), degree = 1,{array.length + 1},Loop at line 42,{array.length},Loop at line 42] codetoanalyze/java/performance/ListTest.java, ListTest.asList_linear(java.lang.String[]):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 8 ⋅ array.length + 3 ⋅ (array.length + 1), O(array.length), degree = 1,{array.length + 1},Loop at line 42,{array.length},Loop at line 42]
codetoanalyze/java/performance/ListTest.java, ListTest.call_iterate_elements_linear(java.util.List,java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 26 + 5 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1), O((l2.length + l1.length)), degree = 1,{l2.length + l1.length + 1},call to void ListTest.iterate_elements_linear(List),Loop at line 59,{l2.length + l1.length},call to void ListTest.iterate_elements_linear(List),Loop at line 59] codetoanalyze/java/performance/ListTest.java, ListTest.call_iterate_elements_linear(java.util.List,java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 26 + 5 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1), O((l2.length + l1.length)), degree = 1,{l2.length + l1.length + 1},call to void ListTest.iterate_elements_linear(List),Loop at line 59,{l2.length + l1.length},call to void ListTest.iterate_elements_linear(List),Loop at line 59]
codetoanalyze/java/performance/ListTest.java, ListTest.indexOfImpl_linear(java.util.List,java.lang.Object):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 18,{list.length},Loop at line 18] codetoanalyze/java/performance/ListTest.java, ListTest.indexOfImpl_linear(java.util.List,java.lang.Object):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 18,{list.length},Loop at line 18]
codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list1_linear(java.util.List,java.util.List):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 17 + 15 ⋅ (l2.length + l1.length + 1), O((l2.length + l1.length)), degree = 1,{l2.length + l1.length + 1},Loop at line 76] codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list1_linear(java.util.List,java.util.List):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 17 + 12 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1), O((l2.length + l1.length)), degree = 1,{l2.length + l1.length + 1},Loop at line 76,{l2.length + l1.length},Loop at line 76]
codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list2_linear(java.util.List,java.util.List):void, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14 + 8 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1), O((l2.length + l1.length)), degree = 1,{l2.length + l1.length + 1},Loop at line 88,{l2.length + l1.length},Loop at line 88] codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list2_linear(java.util.List,java.util.List):void, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14 + 8 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1), O((l2.length + l1.length)), degree = 1,{l2.length + l1.length + 1},Loop at line 88,{l2.length + l1.length},Loop at line 88]
codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list3_linear(java.util.List,java.util.List,java.util.List):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 8 ⋅ (l2.length + l1.length + a.length) + 3 ⋅ (l2.length + l1.length + a.length + 1), O((l2.length + l1.length + a.length)), degree = 1,{l2.length + l1.length + a.length + 1},Loop at line 99,{l2.length + l1.length + a.length},Loop at line 99] codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list3_linear(java.util.List,java.util.List,java.util.List):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 8 ⋅ (l2.length + l1.length + a.length) + 3 ⋅ (l2.length + l1.length + a.length + 1), O((l2.length + l1.length + a.length)), degree = 1,{l2.length + l1.length + a.length + 1},Loop at line 99,{l2.length + l1.length + a.length},Loop at line 99]
codetoanalyze/java/performance/ListTest.java, ListTest.iterate_elements_linear(java.util.List):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 5 ⋅ l.length + 3 ⋅ (l.length + 1), O(l.length), degree = 1,{l.length + 1},Loop at line 59,{l.length},Loop at line 59] codetoanalyze/java/performance/ListTest.java, ListTest.iterate_elements_linear(java.util.List):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 5 ⋅ l.length + 3 ⋅ (l.length + 1), O(l.length), degree = 1,{l.length + 1},Loop at line 59,{l.length},Loop at line 59]

Write Preview
Loading…
Cancel
Save