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

[inferbo] On-demand heap symbol using path

Browse Source 
Summary:
It materializes symbolic values of function parameters on-demand. The on-demand materialization is triggered when finding a value from an abstract memory and joining/widening abstract memories.

Depends on D13294630

Main idea:

* Symbolic values are on-demand-ly generated by a symbol path and its type
* In order to avoid infinite generation of symbolic values, symbol paths are canonicalized by structure types and field names (which means they are abstracted to the same value). For example, in a linked list, a symbolic value `x->next->next` is canonicalized to `x->next` when the structures (`*x` and `*x->next`) have the same structure type and the same field name (`next`).

Changes from the previous code:

* `Symbol.t` does not include `id` and `pname` for distinguishing symbols. Now, all symbols are compared by `path:SymbolPath.partial` and `bound_end`.
* `SymbolTable` is no longer used, which was used for generating symbolic values with new `id`s.

Reviewed By: mbouaziz

Differential Revision: D13294635

fbshipit-source-id: fa422f084
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 49e832ed7f
commit f9161b164f
22 changed files with 539 additions and 538 deletions
Show Stats Download Patch File Download Diff File

38
infer/src/bufferoverrun/absLoc.ml
Unescape View File

@ -73,6 +73,12 @@ module Allocsite = struct
let unknown = Unknown
let get_path = function Unknown -> None | Symbol path -> Some path | Known {path} -> path
let get_param_path = function
| Symbol path ->
Option.some_if (not (Symb.SymbolPath.represents_callsite_sound_partial path)) path
| Unknown | Known _ ->
None
end
module Loc = struct
@ -128,6 +134,16 @@ module Loc = struct
let of_id id = Var (Var.of_id id)
let rec of_path path =
match path with
| Symb.SymbolPath.Pvar pvar ->
of_pvar pvar
| Symb.SymbolPath.Deref _ | Symb.SymbolPath.Callsite _ ->
Allocsite (Allocsite.make_symbol path)
| Symb.SymbolPath.Field (fn, path) ->
Field (of_path path, fn)
let append_field l ~fn = Field (l, fn)
let is_return = function
@ -148,6 +164,21 @@ module Loc = struct
Allocsite.get_path allocsite
| Field (l, fn) ->
Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
let rec get_param_path = function
| Var _ ->
None
| Allocsite allocsite ->
Allocsite.get_param_path allocsite
| Field (l, fn) ->
Option.map (get_param_path l) ~f:(fun p -> Symb.SymbolPath.field p fn)
let has_param_path formals x =
Option.value_map (get_path x) ~default:false ~f:(fun x ->
Option.value_map (Symb.SymbolPath.get_pvar x) ~default:false ~f:(fun x ->
List.exists formals ~f:(fun (formal, _) -> Pvar.equal x formal) ) )
end
module PowLoc = struct
@ -173,6 +204,13 @@ module PowLoc = struct
type eval_locpath = Symb.SymbolPath.partial -> t
let subst_loc l (eval_locpath : eval_locpath) =
match Loc.get_param_path l with None -> singleton l | Some path -> eval_locpath path
let subst x (eval_locpath : eval_locpath) =
fold (fun l acc -> join acc (subst_loc l eval_locpath)) x empty
end
(** unsound but ok for bug catching *)

15
infer/src/bufferoverrun/arrayBlk.ml
Unescape View File

@ -153,8 +153,19 @@ let get_pow_loc : t -> PowLoc.t =
fold pow_loc_of_allocsite array PowLoc.bot
let subst : t -> Bound.eval_sym -> t =
fun a eval_sym -> map (fun info -> ArrInfo.subst info eval_sym) a
let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> t =
fun a eval_sym eval_locpath ->
let subst1 l info acc =
let info' = ArrInfo.subst info eval_sym in
match Allocsite.get_param_path l with
| None ->
add l info' acc
| Some path ->
let locs = eval_locpath path in
let add_allocsite l acc = match l with Loc.Allocsite a -> add a info' acc | _ -> acc in
PowLoc.fold add_allocsite locs acc
in
fold subst1 a empty
let get_symbols : t -> Itv.SymbolSet.t =

23
infer/src/bufferoverrun/bounds.ml
Unescape View File

@ -49,18 +49,6 @@ module SymLinear = struct
M.for_all2 ~f:le_one_pair x y
let make :
unsigned:bool
-> Typ.Procname.t
-> Symb.SymbolTable.t
-> Symb.SymbolPath.t
-> Counter.t
-> t * t =
fun ~unsigned pname symbol_table path new_sym_num ->
let lb, ub = Symb.SymbolTable.lookup ~unsigned pname path symbol_table new_sym_num in
(singleton_one lb, singleton_one ub)
let pp1 :
markup:bool -> is_beginning:bool -> F.formatter -> Symb.Symbol.t -> NonZeroInt.t -> unit =
fun ~markup ~is_beginning f s c ->
@ -269,6 +257,17 @@ module Bound = struct
let of_sym : SymLinear.t -> t = fun s -> Linear (Z.zero, s)
let of_path path_of_partial bound_end ~unsigned partial =
let s = Symb.Symbol.make ~unsigned (path_of_partial partial) bound_end in
of_sym (SymLinear.singleton_one s)
let of_normal_path = of_path Symb.SymbolPath.normal
let of_offset_path = of_path Symb.SymbolPath.offset ~unsigned:false
let of_length_path = of_path Symb.SymbolPath.length ~unsigned:true
let is_symbolic : t -> bool = function
| MInf | PInf ->
false

14
infer/src/bufferoverrun/bounds.mli
Unescape View File

@ -14,14 +14,6 @@ module SymLinear : sig
module M = Symb.SymbolMap
type t = Ints.NonZeroInt.t M.t
val make :
unsigned:bool
-> Typ.Procname.t
-> Symb.SymbolTable.t
-> Symb.SymbolPath.t
-> Counter.t
-> t * t
end
module Bound : sig
@ -51,7 +43,11 @@ module Bound : sig
val _255 : t
val of_sym : SymLinear.t -> t
val of_normal_path : Symb.BoundEnd.t -> unsigned:bool -> Symb.SymbolPath.partial -> t
val of_offset_path : Symb.BoundEnd.t -> Symb.SymbolPath.partial -> t
val of_length_path : Symb.BoundEnd.t -> Symb.SymbolPath.partial -> t
val is_symbolic : t -> bool

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

@ -26,121 +26,13 @@ module Payload = SummaryPayload.Make (struct
let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun
end)
type extras = {symbol_table: Itv.SymbolTable.t; integer_type_widths: Typ.IntegerWidths.t}
type extras = Dom.OndemandEnv.t
module CFG = ProcCfg.NormalOneInstrPerNode
module Init = struct
let declare_symbolic_val :
Typ.Procname.t
-> Itv.SymbolTable.t
-> Itv.SymbolPath.partial
-> Tenv.t
-> Typ.IntegerWidths.t
-> node_hash:int
-> Location.t
-> Loc.t
-> Typ.typ
-> new_sym_num:Counter.t
-> Dom.Mem.t
-> Dom.Mem.t =
fun pname symbol_table path tenv integer_type_widths ~node_hash location loc typ ~new_sym_num
mem ->
let max_depth = 2 in
let rec decl_sym_val pname path tenv location ~depth ~may_last_field loc typ mem =
if depth > max_depth then mem
else
let depth = depth + 1 in
match typ.Typ.desc with
| Typ.Tint ikind ->
let unsigned = Typ.ikind_is_unsigned ikind in
let v = Dom.Val.make_sym ~unsigned loc pname symbol_table path new_sym_num location in
mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
| Typ.Tfloat _ ->
let v = Dom.Val.make_sym loc pname symbol_table path new_sym_num location in
mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
| Typ.Tptr (typ, _) when Language.curr_language_is Java -> (
match typ with
| {desc= Typ.Tarray {elt}} ->
BoUtils.Exec.decl_sym_arr
~decl_sym_val:(decl_sym_val ~may_last_field:false)
Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc
elt ~new_sym_num mem
| _ ->
BoUtils.Exec.decl_sym_java_ptr
~decl_sym_val:(decl_sym_val ~may_last_field:false)
pname path tenv location ~depth loc typ mem )
| Typ.Tptr (typ, _) ->
BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field)
Symb.SymbolPath.Deref_CPointer pname symbol_table path tenv location ~depth loc typ
~new_sym_num mem
| Typ.Tarray {elt; length; stride} ->
let size =
match length with
| Some length when may_last_field && (IntLit.iszero length || IntLit.isone length) ->
None (* Will be made symbolic by [decl_sym_arr] *)
| _ ->
Option.map ~f:Itv.of_int_lit length
in
let offset = Itv.zero in
let stride = Option.map ~f:IntLit.to_int_exn stride in
BoUtils.Exec.decl_sym_arr
~decl_sym_val:(decl_sym_val ~may_last_field:false)
Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv location ~depth loc elt
~offset ?size ?stride ~new_sym_num mem
| Typ.Tstruct typename -> (
match Models.TypName.dispatch tenv typename with
| Some {Models.declare_symbolic} ->
let model_env =
Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table
in
declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env ~depth
loc ~new_sym_num mem
| None ->
let decl_fld ~may_last_field mem (fn, typ, _) =
let loc_fld = Loc.append_field loc ~fn in
let path = Itv.SymbolPath.field path fn in
decl_sym_val pname path tenv location ~depth loc_fld typ ~may_last_field mem
in
let decl_flds str =
IList.fold_last ~f:(decl_fld ~may_last_field:false)
~f_last:(decl_fld ~may_last_field) ~init:mem str.Typ.Struct.fields
in
let opt_struct = Tenv.lookup tenv typename in
Option.value_map opt_struct ~default:mem ~f:decl_flds )
| _ ->
if Config.bo_debug >= 3 then
L.(debug BufferOverrun Verbose)
"/!\\ decl_fld of unhandled type: %a at %a@." (Typ.pp Pp.text) typ Location.pp
location ;
mem
in
decl_sym_val pname path tenv location ~depth:0 ~may_last_field:true loc typ mem
let declare_symbolic_parameters :
Typ.Procname.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> node_hash:int
-> Location.t
-> Itv.SymbolTable.t
-> (Pvar.t * Typ.t) list
-> Dom.Mem.t
-> Dom.Mem.t =
fun pname tenv integer_type_widths ~node_hash location symbol_table formals mem ->
let new_sym_num = Counter.make 0 in
let add_formal mem (pvar, typ) =
let loc = Loc.of_pvar pvar in
let path = Itv.SymbolPath.of_pvar pvar in
declare_symbolic_val pname symbol_table path tenv integer_type_widths ~node_hash location loc
typ ~new_sym_num mem
in
List.fold ~f:add_formal ~init:mem formals
let initial_state {ProcData.pdesc; tenv; extras= {symbol_table; integer_type_widths}} start_node
=
let initial_state {ProcData.pdesc; tenv; extras= {Dom.OndemandEnv.integer_type_widths} as oenv}
start_node =
let node_hash = CFG.Node.hash start_node in
let location = CFG.Node.loc start_node in
let pname = Procdesc.get_proc_name pdesc in
@ -155,7 +47,7 @@ module Init = struct
match Models.TypName.dispatch tenv typname with
| Some {Models.declare_local} ->
let model_env =
Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table
Models.mk_model_env pname node_hash location tenv integer_type_widths
in
declare_local ~decl_local model_env loc ~inst_num ~represents_multiple_values
~dimension mem
@ -170,11 +62,9 @@ module Init = struct
decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values:false
~dimension:1 mem
in
let mem = Dom.Mem.init in
let mem = Dom.Mem.init oenv in
let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in
let formals = Dom.get_formals pdesc in
declare_symbolic_parameters pname tenv integer_type_widths ~node_hash location symbol_table
formals mem
mem
end
module TransferFunctions = struct
@ -183,21 +73,24 @@ module TransferFunctions = struct
type nonrec extras = extras
let instantiate_ret (id, _) callee_pname ~callee_exit_mem eval_sym_trace mem location =
let copy_reachable_new_locs_from locs mem =
let instantiate_mem_reachable (ret_id, _) callee_pdesc callee_pname ~callee_exit_mem
({Dom.eval_locpath} as eval_sym_trace) mem location =
let formals = Dom.get_formals callee_pdesc in
let copy_reachable_locs_from locs mem =
let copy loc acc =
Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v ->
let locs = PowLoc.subst_loc loc eval_locpath in
let v = Dom.Val.subst v eval_sym_trace location in
Dom.Mem.add_heap loc v acc )
PowLoc.fold (fun loc acc -> Dom.Mem.add_heap loc v acc) locs acc )
in
let reachable_locs = Dom.Mem.get_reachable_locs_from locs callee_exit_mem in
let reachable_locs = Dom.Mem.get_reachable_locs_from formals locs callee_exit_mem in
PowLoc.fold copy reachable_locs mem
in
let instantiate_ret_alias mem =
let subst_loc l =
Option.find_map (Loc.get_path l) ~f:(fun partial ->
try
let locs = eval_sym_trace.Dom.eval_locpath partial in
let locs = eval_locpath partial in
match PowLoc.is_singleton_or_more locs with
| IContainer.Singleton loc ->
Some loc
@ -209,52 +102,18 @@ module TransferFunctions = struct
Option.find_map (Dom.Mem.find_ret_alias callee_exit_mem) ~f:(fun alias_target ->
Dom.AliasTarget.loc_map alias_target ~f:subst_loc )
in
Option.value_map ret_alias ~default:mem ~f:(fun l -> Dom.Mem.load_alias id l mem)
Option.value_map ret_alias ~default:mem ~f:(fun l -> Dom.Mem.load_alias ret_id l mem)
in
let ret_var = Loc.of_var (Var.of_id id) in
let ret_var = Loc.of_var (Var.of_id ret_id) in
let ret_val = Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in
Dom.Val.subst ret_val eval_sym_trace location
|> Fn.flip (Dom.Mem.add_stack ret_var) mem
|> instantiate_ret_alias
|> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val)
let instantiate_param tenv pdesc params callee_exit_mem eval_sym_trace location mem =
let formals = Dom.get_formals pdesc in
let actuals_locs = List.map ~f:(fun (a, _) -> Sem.eval_locs a mem) params in
let f mem formal actual_locs =
match (snd formal).Typ.desc with
| Typ.Tptr (typ, _) -> (
match typ.Typ.desc with
| Typ.Tstruct typename -> (
match Tenv.lookup tenv typename with
| Some str ->
let formal_locs =
Dom.Mem.find (Loc.of_pvar (fst formal)) callee_exit_mem
|> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc
in
let instantiate_fld mem (fn, _, _) =
let formal_fields = PowLoc.append_field formal_locs ~fn in
let v = Dom.Mem.find_set formal_fields callee_exit_mem in
let actual_fields = PowLoc.append_field actual_locs ~fn in
Dom.Val.subst v eval_sym_trace location
|> Fn.flip (Dom.Mem.strong_update actual_fields) mem
in
List.fold ~f:instantiate_fld ~init:mem str.Typ.Struct.fields
| _ ->
mem )
| _ ->
let formal_locs =
Dom.Mem.find (Loc.of_pvar (fst formal)) callee_exit_mem
|> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc
in
let v = Dom.Mem.find_set formal_locs callee_exit_mem in
Dom.Val.subst v eval_sym_trace location
|> Fn.flip (Dom.Mem.strong_update actual_locs) mem )
| _ ->
mem
let formal_locs =
List.fold formals ~init:PowLoc.bot ~f:(fun acc (formal, _) ->
let v = Dom.Mem.find (Loc.of_pvar formal) callee_exit_mem in
PowLoc.join acc (Dom.Val.get_all_locs v) )
in
try List.fold2_exn formals actuals_locs ~init:mem ~f with Invalid_argument _ -> mem
Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem
|> instantiate_ret_alias
|> copy_reachable_locs_from (PowLoc.join formal_locs (Dom.Val.get_all_locs ret_val))
let forget_ret_relation ret callee_pname mem =
@ -291,15 +150,15 @@ module TransferFunctions = struct
Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem
in
let caller_mem =
instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace caller_mem location
|> instantiate_param tenv callee_pdesc params callee_exit_mem eval_sym_trace location
instantiate_mem_reachable ret callee_pdesc callee_pname ~callee_exit_mem eval_sym_trace
caller_mem location
|> forget_ret_relation ret callee_pname
in
Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem
let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t =
fun mem {pdesc; tenv; extras= {symbol_table; integer_type_widths}} node instr ->
fun mem {pdesc; tenv; extras= {integer_type_widths}} node instr ->
match instr with
| Load (id, _, _, _) when Ident.is_none id ->
mem
@ -371,7 +230,6 @@ module TransferFunctions = struct
let node_hash = CFG.Node.hash node in
let model_env =
Models.mk_model_env callee_pname node_hash location tenv integer_type_widths
symbol_table
in
exec model_env ~ret mem
| None -> (
@ -389,13 +247,13 @@ module TransferFunctions = struct
| None ->
L.d_printfln "/!\\ Unknown call to %a" Typ.Procname.pp callee_pname ;
if is_external callee_pname then (
let node_hash = CFG.Node.hash node in
let path = Itv.SymbolPath.of_callsite (CallSite.make callee_pname location) in
L.(debug BufferOverrun Verbose)
"/!\\ External call to unknown %a \n\n" Typ.Procname.pp callee_pname ;
Init.declare_symbolic_val callee_pname symbol_table path tenv integer_type_widths
~node_hash location (Loc.of_id id) ret_typ ~new_sym_num:(Counter.make node_hash)
mem )
let callsite = CallSite.make callee_pname location in
let path = Symb.SymbolPath.of_callsite ~ret_typ callsite in
let loc = Loc.of_allocsite (Allocsite.make_symbol path) in
let v = Dom.Mem.find loc mem in
Dom.Mem.add_stack (Loc.of_id id) v mem )
else Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) )
| Call ((id, _), fun_exp, _, location, _) ->
let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
@ -619,13 +477,12 @@ module Report = struct
Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> Itv.SymbolTable.t
-> CFG.Node.t
-> Sil.instr
-> Dom.Mem.t
-> PO.ConditionSet.checked_t
-> PO.ConditionSet.checked_t =
fun pdesc tenv integer_type_widths symbol_table node instr mem cond_set ->
fun pdesc tenv integer_type_widths node instr mem cond_set ->
match instr with
| Sil.Load (_, exp, _, location) ->
cond_set
@ -646,7 +503,7 @@ module Report = struct
let node_hash = CFG.Node.hash node in
let pname = Procdesc.get_proc_name pdesc in
check
(Models.mk_model_env pname node_hash location tenv integer_type_widths symbol_table)
(Models.mk_model_env pname node_hash location tenv integer_type_widths)
mem cond_set
| None -> (
match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with
@ -682,14 +539,13 @@ module Report = struct
-> Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> Itv.SymbolTable.t
-> CFG.t
-> CFG.Node.t
-> Instrs.not_reversed_t
-> Dom.Mem.t AbstractInterpreter.State.t
-> PO.ConditionSet.checked_t
-> PO.ConditionSet.checked_t =
fun summary pdesc tenv integer_type_widths symbol_table cfg node instrs state cond_set ->
fun summary pdesc tenv integer_type_widths cfg node instrs state cond_set ->
match state with
| _ when Instrs.is_empty instrs ->
cond_set
@ -706,9 +562,7 @@ module Report = struct
| NonBottom _ ->
()
in
let cond_set =
check_instr pdesc tenv integer_type_widths symbol_table node instr pre cond_set
in
let cond_set = check_instr pdesc tenv integer_type_widths node instr pre cond_set in
print_debug_info instr pre cond_set ;
cond_set
@ -718,18 +572,16 @@ module Report = struct
-> Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> Itv.SymbolTable.t
-> CFG.t
-> Analyzer.invariant_map
-> PO.ConditionSet.checked_t
-> CFG.Node.t
-> PO.ConditionSet.checked_t =
fun summary pdesc tenv integer_type_widths symbol_table cfg inv_map cond_set node ->
fun summary pdesc tenv integer_type_widths cfg inv_map cond_set node ->
match Analyzer.extract_state (CFG.Node.id node) inv_map with
| Some state ->
let instrs = CFG.instrs node in
check_instrs summary pdesc tenv integer_type_widths symbol_table cfg node instrs state
cond_set
check_instrs summary pdesc tenv integer_type_widths cfg node instrs state cond_set
| _ ->
cond_set
@ -739,13 +591,12 @@ module Report = struct
-> Procdesc.t
-> Tenv.t
-> Typ.IntegerWidths.t
-> Itv.SymbolTable.t
-> CFG.t
-> Analyzer.invariant_map
-> PO.ConditionSet.checked_t =
fun summary pdesc tenv integer_type_widths symbol_table cfg inv_map ->
fun summary pdesc tenv integer_type_widths cfg inv_map ->
CFG.fold_nodes cfg
~f:(check_node summary pdesc tenv integer_type_widths symbol_table cfg inv_map)
~f:(check_node summary pdesc tenv integer_type_widths cfg inv_map)
~init:PO.ConditionSet.empty
@ -786,8 +637,8 @@ let get_local_decls proc_desc =
let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t =
fun {proc_desc; tenv; integer_type_widths; summary} ->
Preanal.do_preanalysis proc_desc tenv ;
let symbol_table = Itv.SymbolTable.empty () in
let pdata = ProcData.make proc_desc tenv {symbol_table; integer_type_widths} in
let oenv = Dom.OndemandEnv.mk proc_desc tenv integer_type_widths in
let pdata = ProcData.make proc_desc tenv oenv in
let cfg = CFG.from_pdesc proc_desc in
let initial = Init.initial_state pdata (CFG.start_node cfg) in
let inv_map = Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata in
@ -797,13 +648,13 @@ let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_
|> Option.map ~f:(Dom.Mem.forget_locs locals)
in
let cond_set =
Report.check_proc summary proc_desc tenv integer_type_widths symbol_table cfg inv_map
Report.check_proc summary proc_desc tenv integer_type_widths cfg inv_map
|> Report.report_errors summary |> Report.forget_locs locals |> Report.for_summary
in
let summary =
match exit_mem with
| Some exit_mem ->
let post = (exit_mem, cond_set) in
let post = (Dom.Mem.unset_oenv exit_mem, cond_set) in
Payload.update_summary post summary
| _ ->
summary

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

@ -13,6 +13,7 @@ open! AbstractDomain.Types
module F = Format
module L = Logging
module Relation = BufferOverrunDomainRelation
module SPath = Symb.SymbolPath
module Trace = BufferOverrunTrace
module TraceSet = Trace.Set
@ -27,6 +28,89 @@ let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ))
module OndemandEnv = struct
type t =
{ typ_of_param_path: SPath.partial -> Typ.t option
; may_last_field: SPath.partial -> bool
; entry_location: Location.t
; integer_type_widths: Typ.IntegerWidths.t }
let mk pdesc =
let module FormalTyps = Caml.Map.Make (Pvar) in
let formal_typs =
List.fold (get_formals pdesc) ~init:FormalTyps.empty ~f:(fun acc (formal, typ) ->
FormalTyps.add formal typ acc )
in
fun tenv integer_type_widths ->
let rec typ_of_param_path = function
| SPath.Pvar x ->
FormalTyps.find_opt x formal_typs
| SPath.Deref (_, x) ->
Option.map (typ_of_param_path x) ~f:(fun typ ->
match typ.Typ.desc with
| Tptr (typ, _) ->
typ
| Tarray {elt} ->
elt
| Tvoid ->
Typ.void
| _ ->
L.(die InternalError) "Untyped expression is given." )
| SPath.Field (fn, x) ->
let lookup = Tenv.lookup tenv in
Option.map (typ_of_param_path x) ~f:(Typ.Struct.fld_typ ~lookup ~default:Typ.void fn)
| SPath.Callsite {ret_typ} ->
Some ret_typ
in
let is_last_field fn (fields : Typ.Struct.field list) =
Option.value_map (List.last fields) ~default:false ~f:(fun (last_fn, _, _) ->
Typ.Fieldname.equal fn last_fn )
in
let rec may_last_field = function
| SPath.Pvar _ | SPath.Deref _ | SPath.Callsite _ ->
true
| SPath.Field (fn, x) ->
may_last_field x
&& Option.value_map ~default:true (typ_of_param_path x) ~f:(fun parent_typ ->
match parent_typ.Typ.desc with
| Tstruct typename ->
let opt_struct = Tenv.lookup tenv typename in
Option.value_map opt_struct ~default:false ~f:(fun str ->
is_last_field fn str.Typ.Struct.fields )
| _ ->
true )
in
let entry_location = Procdesc.Node.get_loc (Procdesc.get_start_node pdesc) in
{typ_of_param_path; may_last_field; entry_location; integer_type_widths}
let canonical_path typ_of_param_path path =
let module KnownFields = Caml.Map.Make (struct
type t = Typ.t option * Typ.Fieldname.t [@@deriving compare]
end) in
let rec helper path =
match path with
| SPath.Pvar _ | SPath.Callsite _ ->
(None, KnownFields.empty)
| SPath.Deref (deref_kind, ptr) ->
let ptr_opt, known_fields = helper ptr in
(Option.map ptr_opt ~f:(fun ptr -> SPath.deref ~deref_kind ptr), known_fields)
| SPath.Field (fn, struct_path) -> (
let struct_path_opt, known_fields = helper struct_path in
let key = (typ_of_param_path (Option.value ~default:struct_path struct_path_opt), fn) in
match KnownFields.find_opt key known_fields with
| Some _ as canonicalized ->
(canonicalized, known_fields)
| None ->
let field_path =
Option.value_map struct_path_opt ~default:path ~f:(fun struct_path ->
SPath.field struct_path fn )
in
(None, KnownFields.add key field_path known_fields) )
in
Option.value (helper path |> fst) ~default:path
end
module Val = struct
type t =
{ itv: Itv.t
@ -145,7 +229,7 @@ module Val = struct
let of_big_int n = of_itv (Itv.of_big_int n)
let of_loc : Loc.t -> t = fun x -> {bot with powloc= PowLoc.singleton x}
let of_loc ?(traces = TraceSet.empty) x = {bot with powloc= PowLoc.singleton x; traces}
let of_pow_loc ~traces powloc = {bot with powloc; traces}
@ -162,24 +246,6 @@ module Val = struct
let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i}
let make_sym :
?unsigned:bool
-> Loc.t
-> Typ.Procname.t
-> Itv.SymbolTable.t
-> Itv.SymbolPath.partial
-> Counter.t
-> Location.t
-> t =
fun ?(unsigned = false) loc pname symbol_table path new_sym_num location ->
let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in
{ bot with
itv= Itv.make_sym ~unsigned pname symbol_table (Itv.SymbolPath.normal path) new_sym_num
; sym= Relation.Sym.of_loc loc
; traces= Trace.(Set.singleton location (Parameter loc))
; represents_multiple_values }
let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top}
let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv; sym= Relation.Sym.top}
@ -323,7 +389,7 @@ module Val = struct
let subst : t -> eval_sym_trace -> Location.t -> t =
fun x {eval_sym; trace_of_sym} location ->
fun x {eval_sym; trace_of_sym; eval_locpath} location ->
let symbols = get_symbols x in
let traces_caller =
Itv.SymbolSet.fold
@ -331,7 +397,11 @@ module Val = struct
symbols TraceSet.empty
in
let traces = TraceSet.call location ~traces_caller ~traces_callee:x.traces in
{x with itv= Itv.subst x.itv eval_sym; arrayblk= ArrayBlk.subst x.arrayblk eval_sym; traces}
{ x with
itv= Itv.subst x.itv eval_sym
; powloc= PowLoc.subst x.powloc eval_locpath
; arrayblk= ArrayBlk.subst x.arrayblk eval_sym eval_locpath
; traces }
(* normalize bottom *)
|> normalize
@ -359,6 +429,67 @@ module Val = struct
let is_mone x = Itv.is_mone (get_itv x)
let of_path ~may_last_field integer_type_widths location typ path =
let is_java = Language.curr_language_is Java in
match typ.Typ.desc with
| Tint _ | Tfloat _ | Tvoid | Tfun _ | TVar _ ->
let l = Loc.of_path path in
let traces = TraceSet.singleton location (Trace.Parameter l) in
let unsigned = Typ.is_unsigned_int typ in
of_itv ~traces (Itv.of_normal_path ~unsigned path)
| Tptr (elt, _) ->
if is_java then
let l = Loc.of_path path in
let traces = TraceSet.singleton location (Trace.Parameter l) in
{bot with itv= Itv.of_length_path path; powloc= PowLoc.singleton l; traces}
else
let deref_kind = SPath.Deref_CPointer in
let deref_path = SPath.deref ~deref_kind path in
let l = Loc.of_path deref_path in
let traces = TraceSet.singleton location (Trace.Parameter l) in
let arrayblk =
let allocsite = Allocsite.make_symbol deref_path in
let stride =
match elt.Typ.desc with
| Typ.Tint ikind ->
Itv.of_int (Typ.width_of_ikind integer_type_widths ikind)
| _ ->
Itv.nat
in
let offset = Itv.of_offset_path path in
let size = Itv.of_length_path path in
ArrayBlk.make allocsite ~stride ~offset ~size
in
{bot with arrayblk; traces}
| Tstruct _ ->
let l = Loc.of_path path in
let traces = TraceSet.singleton location (Trace.Parameter l) in
of_loc ~traces l
| Tarray {length; stride} ->
let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in
let l = Loc.of_path deref_path in
let traces = TraceSet.singleton location (Trace.Parameter l) in
let allocsite = Allocsite.make_symbol deref_path in
let stride = Option.map stride ~f:(fun n -> IntLit.to_int_exn n) in
let offset = Itv.zero in
let size =
Option.value_map length ~default:Itv.top ~f:(fun length ->
if may_last_field && (IntLit.iszero length || IntLit.isone length) then
Itv.of_length_path path
else Itv.of_big_int (IntLit.to_big_int length) )
in
of_array_alloc allocsite ~stride ~offset ~size ~traces
let on_demand : default:t -> OndemandEnv.t -> Loc.t -> t =
fun ~default {typ_of_param_path; may_last_field; entry_location; integer_type_widths} l ->
Option.value_map (Loc.get_path l) ~default ~f:(fun path ->
Option.value_map (typ_of_param_path path) ~default ~f:(fun typ ->
let may_last_field = may_last_field path in
let path = OndemandEnv.canonical_path typ_of_param_path path in
of_path ~may_last_field integer_type_widths entry_location typ path ) )
module Itv = struct
let m1_255 = of_itv Itv.m1_255
@ -394,6 +525,41 @@ module MemPure = struct
|> Polynomials.NonNegativePolynomial.mult acc
else acc )
mem Polynomials.NonNegativePolynomial.one
let join oenv astate1 astate2 =
if phys_equal astate1 astate2 then astate1
else
merge
(fun l v1_opt v2_opt ->
match (v1_opt, v2_opt) with
| Some v1, Some v2 ->
Some (Val.join v1 v2)
| Some v1, None | None, Some v1 ->
let v2 = Val.on_demand ~default:Val.bot oenv l in
Some (Val.join v1 v2)
| None, None ->
None )
astate1 astate2
let widen oenv ~prev ~next ~num_iters =
if phys_equal prev next then prev
else
merge
(fun l v1_opt v2_opt ->
match (v1_opt, v2_opt) with
| Some v1, Some v2 ->
Some (Val.widen ~prev:v1 ~next:v2 ~num_iters)
| Some v1, None ->
let v2 = Val.on_demand ~default:Val.bot oenv l in
Some (Val.widen ~prev:v1 ~next:v2 ~num_iters)
| None, Some v2 ->
let v1 = Val.on_demand ~default:Val.bot oenv l in
Some (Val.widen ~prev:v1 ~next:v2 ~num_iters)
| None, None ->
None )
prev next
end
module AliasTarget = struct
@ -625,14 +791,17 @@ module MemReach = struct
; mem_pure: MemPure.t
; alias: Alias.t
; latest_prune: LatestPrune.t
; relation: Relation.t }
; relation: Relation.t
; oenv: OndemandEnv.t option }
let init : t =
let init : OndemandEnv.t -> t =
fun oenv ->
{ stack_locs= StackLocs.bot
; mem_pure= MemPure.bot
; alias= Alias.bot
; latest_prune= LatestPrune.top
; relation= Relation.empty }
; relation= Relation.empty
; oenv= Some oenv }
let ( <= ) ~lhs ~rhs =
@ -647,21 +816,27 @@ module MemReach = struct
let widen ~prev ~next ~num_iters =
if phys_equal prev next then prev
else
else (
assert (phys_equal prev.oenv next.oenv) ;
let oenv = Option.value_exn prev.oenv in
{ stack_locs= StackLocs.widen ~prev:prev.stack_locs ~next:next.stack_locs ~num_iters
; mem_pure= MemPure.widen ~prev:prev.mem_pure ~next:next.mem_pure ~num_iters
; mem_pure= MemPure.widen oenv ~prev:prev.mem_pure ~next:next.mem_pure ~num_iters
; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters
; latest_prune= LatestPrune.widen ~prev:prev.latest_prune ~next:next.latest_prune ~num_iters
; relation= Relation.widen ~prev:prev.relation ~next:next.relation ~num_iters }
; relation= Relation.widen ~prev:prev.relation ~next:next.relation ~num_iters
; oenv= prev.oenv } )
let join : t -> t -> t =
fun x y ->
assert (phys_equal x.oenv y.oenv) ;
let oenv = Option.value_exn x.oenv in
{ stack_locs= StackLocs.join x.stack_locs y.stack_locs
; mem_pure= MemPure.join x.mem_pure y.mem_pure
; mem_pure= MemPure.join oenv x.mem_pure y.mem_pure
; alias= Alias.join x.alias y.alias
; latest_prune= LatestPrune.join x.latest_prune y.latest_prune
; relation= Relation.join x.relation y.relation }
; relation= Relation.join x.relation y.relation
; oenv= x.oenv }
let pp : F.formatter -> t -> unit =
@ -672,16 +847,22 @@ module MemReach = struct
F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation
let unset_oenv x = {x with oenv= None}
let is_stack_loc : Loc.t -> t -> bool = fun l m -> StackLocs.mem l m.stack_locs
let find_opt : Loc.t -> t -> Val.t option = fun l m -> MemPure.find_opt l m.mem_pure
let find_stack : Loc.t -> t -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.bot
let find_heap : Loc.t -> t -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.Itv.top
let find_heap : default:Val.t -> Loc.t -> t -> Val.t =
fun ~default l m ->
IOption.value_default_f (find_opt l m) ~f:(fun () ->
Option.value_map m.oenv ~default ~f:(fun oenv -> Val.on_demand ~default oenv l) )
let find : Loc.t -> t -> Val.t =
fun l m -> if is_stack_loc l m then find_stack l m else find_heap l m
fun l m -> if is_stack_loc l m then find_stack l m else find_heap ~default:Val.Itv.top l m
let find_set : PowLoc.t -> t -> Val.t =
@ -756,7 +937,8 @@ module MemReach = struct
fun ~f locs m ->
let transform_mem1 l m =
let add, find =
if is_stack_loc l m then (replace_stack, find_stack) else (add_heap, find_heap)
if is_stack_loc l m then (replace_stack, find_stack)
else (add_heap, find_heap ~default:Val.bot)
in
add l (f (find l m)) m
in
@ -815,7 +997,7 @@ module MemReach = struct
{m with latest_prune= LatestPrune.Top}
let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t =
let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> t -> PowLoc.t =
let add_reachable1 ~root loc v acc =
if Loc.equal root loc then PowLoc.union acc (Val.get_all_locs v)
else if Loc.is_field_of ~loc:root ~field_loc:loc then PowLoc.add loc acc
@ -828,7 +1010,13 @@ module MemReach = struct
let reachable_locs = MemPure.fold (add_reachable1 ~root:loc) heap PowLoc.empty in
add_from_locs heap reachable_locs (PowLoc.add loc acc)
in
fun locs m -> add_from_locs m.mem_pure locs PowLoc.empty
let add_param_locs formals mem acc =
let add_loc loc _ acc = if Loc.has_param_path formals loc then PowLoc.add loc acc else acc in
MemPure.fold add_loc mem acc
in
fun formals locs m ->
let locs = add_param_locs formals m.mem_pure locs in
add_from_locs m.mem_pure locs PowLoc.empty
let range : filter_loc:(Loc.t -> bool) -> t -> Polynomials.NonNegativePolynomial.t =
@ -877,7 +1065,7 @@ module Mem = struct
let bot : t = Bottom
let init : t = NonBottom MemReach.init
let init : OndemandEnv.t -> t = fun oenv -> NonBottom (MemReach.init oenv)
let f_lift_default : default:'a -> (MemReach.t -> 'a) -> t -> 'a =
fun ~default f m -> match m with Bottom -> default | NonBottom m' -> f m'
@ -952,8 +1140,9 @@ module Mem = struct
let weak_update : PowLoc.t -> Val.t -> t -> t = fun p v -> f_lift (MemReach.weak_update p v)
let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t =
fun locs -> f_lift_default ~default:PowLoc.empty (MemReach.get_reachable_locs_from locs)
let get_reachable_locs_from : (Pvar.t * Typ.t) list -> PowLoc.t -> t -> PowLoc.t =
fun formals locs ->
f_lift_default ~default:PowLoc.empty (MemReach.get_reachable_locs_from formals locs)
let update_mem : PowLoc.t -> Val.t -> t -> t = fun ploc v -> f_lift (MemReach.update_mem ploc v)
@ -1010,4 +1199,7 @@ module Mem = struct
caller
| NonBottom callee ->
f_lift (fun caller -> MemReach.instantiate_relation subst_map ~caller ~callee) caller
let unset_oenv = f_lift MemReach.unset_oenv
end

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

@ -21,11 +21,10 @@ type model_env =
; node_hash: int
; location: Location.t
; tenv: Tenv.t
; integer_type_widths: Typ.IntegerWidths.t
; symbol_table: Itv.SymbolTable.t }
; integer_type_widths: Typ.IntegerWidths.t }
let mk_model_env pname node_hash location tenv integer_type_widths symbol_table =
{pname; node_hash; location; tenv; integer_type_widths; symbol_table}
let mk_model_env pname node_hash location tenv integer_type_widths =
{pname; node_hash; location; tenv; integer_type_widths}
type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.t -> Dom.Mem.t
@ -50,7 +49,6 @@ type declare_symbolic_fun =
-> model_env
-> depth:int
-> Loc.t
-> new_sym_num:Counter.t
-> Dom.Mem.t
-> Dom.Mem.t
@ -238,9 +236,12 @@ let infer_print e =
let get_array_length array_exp =
let exec {integer_type_widths} ~ret mem =
let arr = Sem.eval_arr integer_type_widths array_exp mem in
let arr = Sem.eval integer_type_widths array_exp mem in
let traces = Dom.Val.get_traces arr in
let length = arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof in
let length =
if Language.curr_language_is Java then arr |> Dom.Val.get_itv
else arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof
in
let result = Dom.Val.of_itv ~traces length in
model_by_value result ret mem
in
@ -314,12 +315,11 @@ module StdArray = struct
BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num
~represents_multiple_values ~dimension mem
in
let declare_symbolic ~decl_sym_val path {pname; tenv; location; symbol_table} ~depth loc
~new_sym_num mem =
let declare_symbolic ~decl_sym_val path {pname; tenv; location} ~depth loc mem =
let offset = Itv.zero in
let size = Itv.of_int64 length in
BoUtils.Exec.decl_sym_arr ~decl_sym_val Symb.SymbolPath.Deref_ArrayIndex pname symbol_table
path tenv location ~depth loc typ ~offset ~size ~new_sym_num mem
BoUtils.Exec.decl_sym_arr ~decl_sym_val Symb.SymbolPath.Deref_ArrayIndex pname path tenv
location ~depth loc typ ~offset ~size mem
in
{declare_local; declare_symbolic}
@ -359,7 +359,7 @@ module StdArray = struct
~dimension:_ mem =
(no_model "local" pname location mem, inst_num)
in
let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~depth:_ _loc ~new_sym_num:_ mem =
let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~depth:_ _loc mem =
no_model "symbolic" pname location mem
in
{declare_local; declare_symbolic}
@ -376,9 +376,8 @@ module Collection = struct
BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num
~represents_multiple_values ~dimension mem
in
let declare_symbolic ~decl_sym_val:_ path {pname; location; symbol_table} ~depth:_ loc
~new_sym_num mem =
BoUtils.Exec.decl_sym_collection pname symbol_table path location loc ~new_sym_num mem
let declare_symbolic ~decl_sym_val:_ path {location} ~depth:_ loc mem =
BoUtils.Exec.decl_sym_collection path location loc mem
in
{declare_local; declare_symbolic}

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

@ -142,7 +142,7 @@ let set_array_stride integer_type_widths typ v =
let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
fun integer_type_widths exp mem ->
if must_alias_cmp exp mem then Val.Itv.zero
if (not (Language.curr_language_is Java)) && must_alias_cmp exp mem then Val.Itv.zero
else
match exp with
| Exp.Var id ->
@ -346,29 +346,33 @@ let rec eval_sympath_partial params p mem =
L.(debug BufferOverrun Verbose)
"Symbol %a is not found in parameters.@\n" (Pvar.pp Pp.text) x ;
Val.Itv.top )
| Symb.SymbolPath.Callsite cs ->
| Symb.SymbolPath.Callsite {cs} ->
L.(debug BufferOverrun Verbose)
"Symbol for %a is not expected to be in parameters.@\n" Typ.Procname.pp (CallSite.pname cs) ;
Val.Itv.top
Mem.find (Loc.of_allocsite (Allocsite.make_symbol p)) mem
| Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ ->
let locs = eval_locpath params p mem in
Mem.find_set locs mem
and eval_locpath params p mem =
match p with
| Symb.SymbolPath.Pvar _ ->
let v = eval_sympath_partial params p mem in
Val.get_all_locs v
| Symb.SymbolPath.Deref (_, p) ->
let v = eval_sympath_partial params p mem in
Val.get_all_locs v
| Symb.SymbolPath.Callsite _ ->
let v = eval_sympath_partial params p mem in
Val.get_all_locs v
| Symb.SymbolPath.Field (fn, p) ->
let locs = eval_locpath params p mem in
PowLoc.append_field ~fn locs
let res =
match p with
| Symb.SymbolPath.Pvar _ | Symb.SymbolPath.Callsite _ ->
let v = eval_sympath_partial params p mem in
Val.get_all_locs v
| Symb.SymbolPath.Deref (_, p) ->
let v = eval_sympath_partial params p mem in
Val.get_all_locs v
| Symb.SymbolPath.Field (fn, p) ->
let locs = eval_locpath params p mem in
PowLoc.append_field ~fn locs
in
if PowLoc.is_empty res then (
L.(debug BufferOverrun Verbose)
"Location value for %a is not found.@\n" Symb.SymbolPath.pp_partial p ;
PowLoc.unknown )
else res
let eval_sympath params sympath mem =
@ -381,7 +385,10 @@ let eval_sympath params sympath mem =
(ArrayBlk.offsetof (Val.get_array_blk v), Val.get_traces v)
| Symb.SymbolPath.Length p ->
let v = eval_sympath_partial params p mem in
(ArrayBlk.sizeof (Val.get_array_blk v), Val.get_traces v)
let traces = Val.get_traces v in
let itv = ArrayBlk.sizeof (Val.get_array_blk v) in
let itv = if Language.curr_language_is Java then Itv.join itv (Val.get_itv v) else itv in
(itv, traces)
let mk_eval_sym_trace integer_type_widths callee_pdesc actual_exps caller_mem =

56
infer/src/bufferoverrun/bufferOverrunUtils.ml
Unescape View File

@ -128,7 +128,6 @@ module Exec = struct
decl_sym_val:decl_sym_val
-> Symb.SymbolPath.deref_kind
-> Typ.Procname.t
-> Itv.SymbolTable.t
-> Itv.SymbolPath.partial
-> Tenv.t
-> Location.t
@ -138,20 +137,11 @@ module Exec = struct
-> ?offset:Itv.t
-> ?size:Itv.t
-> ?stride:int
-> new_sym_num:Counter.t
-> Dom.Mem.t
-> Dom.Mem.t =
fun ~decl_sym_val deref_kind pname symbol_table path tenv location ~depth loc typ ?offset ?size
?stride ~new_sym_num mem ->
let offset =
IOption.value_default_f offset ~f:(fun () ->
Itv.make_sym pname symbol_table (Itv.SymbolPath.offset path) new_sym_num )
in
let size =
IOption.value_default_f size ~f:(fun () ->
Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num
)
in
fun ~decl_sym_val deref_kind pname path tenv location ~depth loc typ ?offset ?size ?stride mem ->
let offset = IOption.value_default_f offset ~f:(fun () -> Itv.of_offset_path path) in
let size = IOption.value_default_f size ~f:(fun () -> Itv.of_length_path path) in
let deref_path = Itv.SymbolPath.deref ~deref_kind path in
let allocsite = Allocsite.make_symbol deref_path in
let mem =
@ -168,45 +158,13 @@ module Exec = struct
decl_sym_val pname deref_path tenv location ~depth deref_loc typ mem
let decl_sym_java_ptr :
decl_sym_val:decl_sym_val
-> Typ.Procname.t
-> Itv.SymbolPath.partial
-> Tenv.t
-> Location.t
-> depth:int
-> Loc.t
-> Typ.t
-> Dom.Mem.t
-> Dom.Mem.t =
fun ~decl_sym_val pname path tenv location ~depth loc typ mem ->
let allocsite = Allocsite.make_symbol path in
let alloc_loc = Loc.of_allocsite allocsite in
let v =
let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in
let traces = Trace.(Set.singleton location (Trace.Parameter loc)) in
Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces
|> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
in
let mem = Dom.Mem.add_heap loc v mem in
decl_sym_val pname path tenv location ~depth alloc_loc typ mem
let decl_sym_collection :
Typ.Procname.t
-> Itv.SymbolTable.t
-> Itv.SymbolPath.partial
-> Location.t
-> Loc.t
-> new_sym_num:Counter.t
-> Dom.Mem.t
-> Dom.Mem.t =
fun pname symbol_table path location loc ~new_sym_num mem ->
let decl_sym_collection : Itv.SymbolPath.partial -> Location.t -> Loc.t -> Dom.Mem.t -> Dom.Mem.t
=
fun path location loc mem ->
let size =
let represents_multiple_values = Itv.SymbolPath.represents_multiple_values path in
let traces = Trace.(Set.singleton location (Parameter loc)) in
Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num
|> Dom.Val.of_itv ~traces
Itv.of_length_path path |> Dom.Val.of_itv ~traces
|> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
in
Dom.Mem.add_heap loc size mem

24
infer/src/bufferoverrun/bufferOverrunUtils.mli
Unescape View File

@ -71,7 +71,6 @@ module Exec : sig
decl_sym_val:decl_sym_val
-> Symb.SymbolPath.deref_kind
-> Typ.Procname.t
-> Itv.SymbolTable.t
-> Itv.SymbolPath.partial
-> Tenv.t
-> Location.t
@ -81,31 +80,10 @@ module Exec : sig
-> ?offset:Itv.t
-> ?size:Itv.t
-> ?stride:int
-> new_sym_num:Counter.t
-> Dom.Mem.t
-> Dom.Mem.t
val decl_sym_java_ptr :
decl_sym_val:decl_sym_val
-> Typ.Procname.t
-> Itv.SymbolPath.partial
-> Tenv.t
-> Location.t
-> depth:int
-> Loc.t
-> Typ.t
-> Dom.Mem.t
-> Dom.Mem.t
val decl_sym_collection :
Typ.Procname.t
-> Itv.SymbolTable.t
-> Itv.SymbolPath.partial
-> Location.t
-> Loc.t
-> new_sym_num:Counter.t
-> Dom.Mem.t
-> Dom.Mem.t
val decl_sym_collection : Itv.SymbolPath.partial -> Location.t -> Loc.t -> Dom.Mem.t -> Dom.Mem.t
val init_array_fields :
Tenv.t

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

@ -14,7 +14,6 @@ module L = Logging
module Bound = Bounds.Bound
open Ints
module SymbolPath = Symb.SymbolPath
module SymbolTable = Symb.SymbolTable
module SymbolSet = Symb.SymbolSet
module ItvRange = struct
@ -113,13 +112,6 @@ module ItvPure = struct
let of_big_int n = of_bound (Bound.of_big_int n)
let make_sym : unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t
=
fun ~unsigned pname symbol_table path new_sym_num ->
let lb, ub = Bounds.SymLinear.make ~unsigned pname symbol_table path new_sym_num in
(Bound.of_sym lb, Bound.of_sym ub)
let mone = of_bound Bound.mone
let m1_255 = (Bound.minus_one, Bound._255)
@ -417,6 +409,19 @@ module ItvPure = struct
let max_of_ikind integer_type_widths ikind =
let _, max = Typ.range_of_ikind integer_type_widths ikind in
of_big_int max
let of_path bound_of_path path =
let lb = bound_of_path Symb.BoundEnd.LowerBound path in
let ub = bound_of_path Symb.BoundEnd.UpperBound path in
(lb, ub)
let of_normal_path ~unsigned = of_path (Bound.of_normal_path ~unsigned)
let of_offset_path = of_path Bound.of_offset_path
let of_length_path = of_path Bound.of_length_path
end
include AbstractDomain.BottomLifted (ItvPure)
@ -552,12 +557,6 @@ let minus : t -> t -> t = lift2 ItvPure.minus
let get_iterator_itv : t -> t = lift1 ItvPure.get_iterator_itv
let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t
=
fun ?(unsigned = false) pname symbol_table path new_sym_num ->
NonBottom (ItvPure.make_sym ~unsigned pname symbol_table path new_sym_num)
let is_const : t -> Z.t option = bind1zo ItvPure.is_const
let is_mone = bind1bool ItvPure.is_mone
@ -627,3 +626,10 @@ let normalize : t -> t = bind1 ItvPure.normalize
let max_of_ikind integer_type_widths ikind =
NonBottom (ItvPure.max_of_ikind integer_type_widths ikind)
let of_normal_path ~unsigned path = NonBottom (ItvPure.of_normal_path ~unsigned path)
let of_offset_path path = NonBottom (ItvPure.of_offset_path path)
let of_length_path path = NonBottom (ItvPure.of_length_path path)

10
infer/src/bufferoverrun/itv.mli
Unescape View File

@ -10,7 +10,6 @@ open! AbstractDomain.Types
module F = Format
module Bound = Bounds.Bound
module SymbolPath = Symb.SymbolPath
module SymbolTable = Symb.SymbolTable
module SymbolSet = Symb.SymbolSet
module ItvRange : sig
@ -142,9 +141,6 @@ val is_mone : t -> bool
val eq_const : Z.t -> t -> bool
val make_sym :
?unsigned:bool -> Typ.Procname.t -> Symb.SymbolTable.t -> Symb.SymbolPath.t -> Counter.t -> t
val lb : t -> Bound.t
val ub : t -> Bound.t
@ -218,3 +214,9 @@ val prune_ne : t -> t -> t
val subst : t -> Bound.eval_sym -> t
val max_of_ikind : Typ.IntegerWidths.t -> Typ.ikind -> t
val of_normal_path : unsigned:bool -> Symb.SymbolPath.partial -> t
val of_offset_path : Symb.SymbolPath.partial -> t
val of_length_path : Symb.SymbolPath.partial -> t

114
infer/src/bufferoverrun/symb.ml
Unescape View File

@ -8,7 +8,7 @@ open! IStd
module F = Format
module BoundEnd = struct
type t = LowerBound | UpperBound
type t = LowerBound | UpperBound [@@deriving compare]
let neg = function LowerBound -> UpperBound | UpperBound -> LowerBound
@ -22,7 +22,7 @@ module SymbolPath = struct
| Pvar of Pvar.t
| Deref of deref_kind * partial
| Field of Typ.Fieldname.t * partial
| Callsite of CallSite.t
| Callsite of {ret_typ: Typ.t; cs: CallSite.t}
[@@deriving compare]
type t = Normal of partial | Offset of partial | Length of partial [@@deriving compare]
@ -33,7 +33,7 @@ module SymbolPath = struct
let of_pvar pvar = Pvar pvar
let of_callsite cs = Callsite cs
let of_callsite ~ret_typ cs = Callsite {ret_typ; cs}
let field p fn = Field (fn, p)
@ -45,6 +45,15 @@ module SymbolPath = struct
let length p = Length p
let rec get_pvar = function
| Pvar pvar ->
Some pvar
| Deref (_, partial) | Field (_, partial) ->
get_pvar partial
| Callsite _ ->
None
let rec pp_partial_paren ~paren fmt = function
| Pvar pvar ->
Pvar.pp_value fmt pvar
@ -58,7 +67,7 @@ module SymbolPath = struct
F.fprintf fmt "%a->%s" (pp_partial_paren ~paren:true) p (Typ.Fieldname.to_flat_string fn)
| Field (fn, p) ->
F.fprintf fmt "%a.%s" (pp_partial_paren ~paren:true) p (Typ.Fieldname.to_flat_string fn)
| Callsite cs ->
| Callsite {cs} ->
F.fprintf fmt "%a" Typ.Procname.pp (CallSite.pname cs)
@ -94,107 +103,46 @@ module SymbolPath = struct
represents_callsite_sound_partial p
let represents_partial_sound ~f = function Normal p | Offset p | Length p -> f p
let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
end
module Symbol = struct
type t =
| IntraProc of
{ id: int
; pname: Typ.Procname.t
; unsigned: bool
; path: SymbolPath.t
; bound_end: BoundEnd.t }
(* symbols for unknown calls *)
| Call of
{ id: int
; pname: Typ.Procname.t
; unsigned: bool
; path: SymbolPath.t
; bound_end: BoundEnd.t }
type extra_bool = bool
type 'res eval = t -> 'res AbstractDomain.Types.bottom_lifted
let compare_extra_bool _ _ = 0
let compare s1 s2 =
match (s1, s2) with
| IntraProc s1, IntraProc s2 ->
(* Parameter symbols only make sense within a given function, so shouldn't be compared across function boundaries. *)
assert (phys_equal s1.pname s2.pname) ;
Int.compare s1.id s2.id
| Call s1, Call s2 ->
Int.compare s1.id s2.id
| Call _, IntraProc _ ->
-1
| IntraProc _, Call _ ->
1
type t = {unsigned: extra_bool; path: SymbolPath.t; bound_end: BoundEnd.t} [@@deriving compare]
let compare x y =
let r = compare x y in
if Int.equal r 0 then assert (Bool.equal x.unsigned y.unsigned) ;
r
let equal = [%compare.equal: t]
let paths_equal s1 s2 =
match (s1, s2) with
| IntraProc _, Call _ | Call _, IntraProc _ ->
false
| IntraProc {path= path1}, IntraProc {path= path2} | Call {path= path1}, Call {path= path2} ->
SymbolPath.equal path1 path2
type 'res eval = t -> 'res AbstractDomain.Types.bottom_lifted
let make_intraproc : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t =
fun ~unsigned pname path bound_end id -> IntraProc {id; pname; unsigned; path; bound_end}
let equal = [%compare.equal: t]
let paths_equal s1 s2 = SymbolPath.equal s1.path s2.path
let make_call : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t =
fun ~unsigned pname path bound_end id -> Call {id; pname; unsigned; path; bound_end}
let make : unsigned:bool -> SymbolPath.t -> BoundEnd.t -> t =
fun ~unsigned path bound_end -> {unsigned; path; bound_end}
let pp : F.formatter -> t -> unit =
fun fmt s ->
match s with
| Call {id; pname; unsigned; path; bound_end} | IntraProc {id; pname; unsigned; path; bound_end}
->
SymbolPath.pp fmt path ;
if Config.developer_mode then Format.fprintf fmt ".%s" (BoundEnd.to_string bound_end) ;
if Config.bo_debug > 1 then
let symbol_name = if unsigned then 'u' else 's' in
F.fprintf fmt "(%s-%c$%d)" (Typ.Procname.to_string pname) symbol_name id
SymbolPath.pp fmt s.path ;
if Config.developer_mode then Format.fprintf fmt ".%s" (BoundEnd.to_string s.bound_end) ;
if Config.bo_debug > 1 then F.fprintf fmt "(%c)" (if s.unsigned then 'u' else 's')
let pp_mark ~markup = if markup then MarkupFormatter.wrap_monospaced pp else pp
let is_unsigned : t -> bool = function IntraProc {unsigned} | Call {unsigned} -> unsigned
let path = function IntraProc {path} | Call {path} -> path
let is_unsigned {unsigned} = unsigned
let bound_end = function IntraProc {bound_end} | Call {bound_end} -> bound_end
end
let path {path} = path
module SymbolTable = struct
module M = PrettyPrintable.MakePPMap (SymbolPath)
type t = (Symbol.t * Symbol.t) M.t ref
let empty () = ref M.empty
let lookup ~unsigned pname path symbol_table new_sym_num =
match M.find_opt path !symbol_table with
| Some s ->
s
| None ->
let s =
if
SymbolPath.represents_partial_sound ~f:SymbolPath.represents_callsite_sound_partial
path
then
( Symbol.make_call ~unsigned pname path LowerBound (Counter.next new_sym_num)
, Symbol.make_call ~unsigned pname path UpperBound (Counter.next new_sym_num) )
else
( Symbol.make_intraproc ~unsigned pname path LowerBound (Counter.next new_sym_num)
, Symbol.make_intraproc ~unsigned pname path UpperBound (Counter.next new_sym_num) )
in
symbol_table := M.add path s !symbol_table ;
s
let bound_end {bound_end} = bound_end
end
module SymbolSet = struct

21
infer/src/bufferoverrun/symb.mli
Unescape View File

@ -21,7 +21,7 @@ module SymbolPath : sig
| Pvar of Pvar.t
| Deref of deref_kind * partial
| Field of Typ.Fieldname.t * partial
| Callsite of CallSite.t
| Callsite of {ret_typ: Typ.t; cs: CallSite.t}
[@@deriving compare]
type t = private Normal of partial | Offset of partial | Length of partial
@ -30,11 +30,15 @@ module SymbolPath : sig
val pp_mark : markup:bool -> F.formatter -> t -> unit
val pp_partial : F.formatter -> partial -> unit
val pp_partial_paren : paren:bool -> F.formatter -> partial -> unit
val of_pvar : Pvar.t -> partial
val of_callsite : CallSite.t -> partial
val of_callsite : ret_typ:Typ.t -> CallSite.t -> partial
val get_pvar : partial -> Pvar.t option
val deref : deref_kind:deref_kind -> partial -> partial
@ -47,6 +51,8 @@ module SymbolPath : sig
val length : partial -> t
val represents_multiple_values : partial -> bool
val represents_callsite_sound_partial : partial -> bool
end
module Symbol : sig
@ -67,6 +73,8 @@ module Symbol : sig
val path : t -> SymbolPath.t
val bound_end : t -> BoundEnd.t
val make : unsigned:bool -> SymbolPath.t -> BoundEnd.t -> t
end
module SymbolSet : sig
@ -80,12 +88,3 @@ module SymbolMap : sig
val for_all2 : f:(key -> 'a option -> 'b option -> bool) -> 'a t -> 'b t -> bool
end
module SymbolTable : sig
type t
val empty : unit -> t
val lookup :
unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> t -> Counter.t -> Symbol.t * Symbol.t
end

2
infer/tests/codetoanalyze/c/bufferoverrun/get_field.c
Unescape View File

@ -23,7 +23,7 @@ void call_get_field_cond_Bad() {
}
}
void FP_call_get_field_Good() {
void call_get_field_Good() {
int a[5];
t x = {0};
a[get_field_wrapper(&x)] = 0;

26
infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
Unescape View File

@ -3,7 +3,9 @@ codetoanalyze/c/bufferoverrun/arith.c, band_negative_Bad, 8, BUFFER_OVERRUN_L2,
codetoanalyze/c/bufferoverrun/arith.c, band_negative_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/c/bufferoverrun/arith.c, band_positive_Bad, 6, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 8] Size: 5]
codetoanalyze/c/bufferoverrun/arith.c, band_positive_constant_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, +oo] - 97):unsigned64 by call to `scan_hex_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L2, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([58, 102] - 87):unsigned64 by call to `scan_hex_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_scan_hex_Good_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Parameter `*cp`,Assignment,Binary operation: ([-oo, +oo] - 48):unsigned64 by call to `scan_hex_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, call_two_safety_conditions2_Bad, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Call,Assignment,Assignment,<RHS trace>,Parameter `s`,Binary operation: ([0, +oo] + 15):unsigned32 by call to `two_safety_conditions2_Bad` ]
codetoanalyze/c/bufferoverrun/arith.c, call_unsigned_prune_ge1_Good_FP, 0, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,<LHS trace>,Parameter `x`,<RHS trace>,Parameter `y`,Binary operation: (0 - 1):unsigned32 by call to `unsigned_prune_ge1_Good` ]
codetoanalyze/c/bufferoverrun/arith.c, div_const2_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Parameter `n`,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 1]
@ -46,7 +48,7 @@ codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, COND
codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `len`,<Length trace>,Parameter `len`,Array declaration,Array access: Offset: [3⋅len + 1, 3⋅len + 1] Size: [3⋅len + 1, 3⋅len + 1]]
codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 20 Size: 10]
codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `x->f`,Assignment,Assignment,Assignment,Array access: Offset: -1 Size: 2]
codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `x->f[*]`,Assignment,Assignment,Assignment,Array access: Offset: -1 Size: 2]
codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 3 Size: 3]
codetoanalyze/c/bufferoverrun/array_multidim.c, multidim_arr4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 6 Size: 6]
@ -66,14 +68,14 @@ codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Bad, 5, BUFFER_OVE
codetoanalyze/c/bufferoverrun/cast.c, cast_signed_to_unsigned_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Bad_FN, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/cast.c, cast_unsigned_to_signed_Good, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/do_while.c, do_while_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Assignment,Call,<Offset trace>,Assignment,<Length trace>,Parameter `a`,Array access: Offset: [0, 10] Size: 10 by call to `do_while_sub` ]
codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `arr`,Array access: Offset: 1 Size: 1 by call to `two_accesses` ]
codetoanalyze/c/bufferoverrun/do_while.c, do_while_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Assignment,Call,<Offset trace>,Assignment,<Length trace>,Parameter `*a`,Array access: Offset: [0, 10] Size: 10 by call to `do_while_sub` ]
codetoanalyze/c/bufferoverrun/duplicates.c, one_alarm_is_enough, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*arr`,Array access: Offset: 1 Size: 1 by call to `two_accesses` ]
codetoanalyze/c/bufferoverrun/duplicates.c, tsa_one_alarm_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 3 Size: 1 by call to `two_symbolic_accesses` ]
codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: -1 Size: 1 by call to `two_symbolic_accesses` ]
codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1 by call to `two_symbolic_accesses` ]
codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 30 Size: 10]
codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Assignment,<Length trace>,Parameter `arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ]
codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Assignment,<Length trace>,Parameter `*arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ]
codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `m`,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: [5, 10]]
codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]
@ -82,10 +84,10 @@ codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER
codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad1, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Call,<Offset trace>,Parameter `*arr`,Assignment,<Length trace>,Parameter `arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ]
codetoanalyze/c/bufferoverrun/get_field.c, FP_call_get_field_Good, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,Parameter `x->field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,Parameter `x->field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `*arr`,Assignment,<Length trace>,Parameter `*arr`,Array access: Offset: 100 Size: 10 by call to `arr_access` ]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `x->field`,Call,Parameter `x->field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
@ -125,7 +127,7 @@ codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_overrun_Good_FP, 2,
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_no_underrun_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, 9] Size: 9]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [0, 10] Size: 10]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-1, 9] Size: 9]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow2_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [-length + length + 1, length] Size: length]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow2_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [length - length + 1, length] Size: length]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_loop_overflow_Bad, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,Assignment,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [1, length] Size: length]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l2_symbolic_overrun_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `n`,<Length trace>,Parameter `n`,Array declaration,Array access: Offset: n Size: n]
codetoanalyze/c/bufferoverrun/issue_kinds.c, l3_concrete_no_overrun_Good_FP, 2, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Call,Assignment,Array declaration,Array access: Offset: [0, 10] Size: [5, 15]]
@ -177,14 +179,14 @@ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label,
codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 7, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: [3, 2043] (⇐ [0, 1020] + [3, 1023]) Size: 1024]
codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 10 (⇐ 5 + 5) Size: 10]
codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `x`,<Length trace>,Parameter `p`,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `pointer_arith3` ]
codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,<Offset trace>,Parameter `x`,<Length trace>,Parameter `*p`,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `pointer_arith3` ]
codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 10 (⇐ 100 + -90) Size: 5 by call to `FN_pointer_arith4_Bad` ]
codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ]
codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [-length + length + 1, length] Size: length]
codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ]
codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Parameter `length`,<Length trace>,Parameter `length`,Array declaration,Array access: Offset: [length - length + 1, length] Size: length]
codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_eq_Ok, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]

6
infer/tests/codetoanalyze/c/performance/issues.exp
Unescape View File

@ -185,6 +185,6 @@ codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb, 9, EXPENSIVE_E
codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 6 ⋅ m.ub + 2 ⋅ (1+max(0, m.ub)), degree = 1]
codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ m.ub + 6 ⋅ k.ub + 2 ⋅ (1+max(0, m.ub)) + 2 ⋅ (1+max(0, k.ub)), degree = 1]
codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ m.ub + 6 ⋅ k.ub + 2 ⋅ (1+max(0, m.ub)) + 2 ⋅ (1+max(0, k.ub)), degree = 1]
codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 6 ⋅ m.ub + 6 ⋅ k.ub + 2 ⋅ (1+max(0, m.ub)) + 2 ⋅ (1+max(0, k.ub)), degree = 1]
codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ k.ub + 6 ⋅ m.ub + 2 ⋅ (1+max(0, k.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 1]
codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 6 ⋅ k.ub + 6 ⋅ m.ub + 2 ⋅ (1+max(0, k.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 1]
codetoanalyze/c/performance/two_loops_symbolic.c, two_loops_symb_diff, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 6 ⋅ k.ub + 6 ⋅ m.ub + 2 ⋅ (1+max(0, k.ub)) + 2 ⋅ (1+max(0, m.ub)), degree = 1]

4
infer/tests/codetoanalyze/cpp/bufferoverrun/class.cpp
Unescape View File

@ -296,7 +296,7 @@ class my_class6 {
void dummy_function() {}
void set_x_two_Good_FP() {
void set_x_two_Good() {
int arr[5];
*x = 0;
dummy_function();
@ -312,7 +312,7 @@ class my_class6 {
void set_x_three() { *x = 3; }
void call_set_x_three_Good_FP() {
void call_set_x_three_Good() {
int arr[5];
set_x_three();
arr[*x] = 0;

78
infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp
Unescape View File

@ -9,33 +9,31 @@ codetoanalyze/cpp/bufferoverrun/arith.cpp, bool_overflow_Good_FP, 3, BUFFER_OVER
codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/arith.cpp, range_bool_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 2 Size: 2]
codetoanalyze/cpp/bufferoverrun/arith.cpp, sizeof_bool_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Parameter `this->arr`,Array access: Offset: 15 Size: 10 by call to `my_class_access_nth` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, access_after_new_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `n`,<Length trace>,Parameter `this->arr[*]`,Array access: Offset: 15 Size: 10 by call to `my_class_access_nth` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, array_member_malloc_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array4_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Parameter `this->children`,Call,<Offset trace>,Parameter `nth`,<Length trace>,Parameter `this->children`,Array access: Offset: 5 Size: 3 by call to `Tree_set_child` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array5_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,<Offset trace>,Parameter `nth`,<Length trace>,Parameter `this->children[*]`,Array access: Offset: 5 Size: 3 by call to `Tree_set_child` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload1_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_new_overload2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 6]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Length trace>,Parameter `x->b`,Array access: Offset: 3 Size: 3 by call to `flexible_array_param_access` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 3]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Good_FP, 3, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Good_FP, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this->arr`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `n`,Assignment,<Length trace>,Call,Parameter `this->arr`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/class.cpp, flexible_array_param_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Length trace>,Parameter `x->b[*]`,Array access: Offset: 3 Size: 3 by call to `flexible_array_param_access` ]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_call_set_x_three_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: 3 Size: 3]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class6_set_x_two_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access2_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `n`,Assignment,<Length trace>,Parameter `this->arr[*]`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/class.cpp, my_class_access_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `n`,Assignment,<Length trace>,Parameter `this->arr[*]`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/class.cpp, new_nothrow_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload1_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, placement_new_overload2_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, return_class_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Call,Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/class.cpp, use_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 32 Size: 30]
codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/cpp_is_tricky.cpp, CppIsTricky::vector_size_Bad, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `__x->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Assignment,Binary operation: (1 - [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 30 Size: 10]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty2_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [1, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empty_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Through,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [1, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]
@ -44,29 +42,29 @@ codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Good_FP, 6, BUFFER_OVERRUN_
codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 7 Size: 5]
codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct2_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call1_loop_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call1_loop_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call2_minus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 8 Size: 5 by call to `minus_params_Ok` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params2_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: -1 Size: 5 by call to `plus_params2` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call3_plus_params_Ok, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: -1 Size: 5 by call to `plus_params` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_id_Ok, 4, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Assignment,Call,Assignment,Assignment,Array declaration,Assignment,Array access: Offset: 5 Size: [0, 6]]
codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `data`,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `data`,Assignment,Array access: Offset: [0, +oo] Size: 1 by call to `loop_with_type_casting` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*data`,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 1 by call to `loop_with_type_casting` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_call_loop_with_type_casting_Ok, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Assignment,Call,<Length trace>,Parameter `*data`,Assignment,Array access: Offset: [0, +oo] Size: 1 by call to `loop_with_type_casting` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, FP_loop2_Ok, 9, BUFFER_OVERRUN_L4, no_bucket, ERROR, [<Length trace>,Assignment,Array declaration,Assignment,Array access: Offset: [2, +oo] (⇐ [0, +oo] + 2) Size: 12]
codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_loop_Bad, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [Array declaration,Call,<Length trace>,Parameter `*arr`,Array access: Offset: [0, +oo] Size: 5 by call to `loop` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 11 Size: 5 by call to `plus_params2` ]
codetoanalyze/cpp/bufferoverrun/relation.cpp, call2_plus_params_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,<Offset trace>,Parameter `x`,<Length trace>,Array declaration,Array access: Offset: 11 Size: 5 by call to `plus_params` ]
codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_foo_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
codetoanalyze/cpp/bufferoverrun/remove_temps.cpp, C_goo, 1, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_fB_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Parameter `this->infer_size`,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI_FP, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Parameter `this->infer_size`,Assignment,Assignment,Assignment,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Call,Parameter `this->infer_size`,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter `bi`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [-1+max(1, bi.lb), -1+max(1, bi.ub)] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `t->bI`,Call,Parameter `bi`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `t->bI`,Call,<LHS trace>,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral` ]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->_size`,Call,Parameter `this->_size`,Call,<Offset trace>,Parameter `i`,<Length trace>,Parameter `this->_size`,Array declaration,Assignment,Array access: Offset: v->_size Size: v->_size by call to `int_vector_access_at` ]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_fB_FP, 0, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Assignment,Binary operation: ([-oo, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI_FP, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Assignment,Assignment,Assignment,Binary operation: ([-oo, +oo] - 1):signed32]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Call,Assignment,Assignment,Call,Parameter `t->bI`,Call,Parameter `t->bI`,Call,<LHS trace>,Parameter `bi`,Binary operation: ([-oo, +oo] - 1):signed32 by call to `ral_FP` ]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, gal_FP, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [0, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, gal_FP, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, BUFFER_OVERRUN_S2, no_bucket, ERROR, [Parameter `t->bI`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: [-1+max(1, t->bI.lb), -1+max(1, t->bI.ub)] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, ral_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->b.infer_size`,Call,Parameter `this->b.infer_size`,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->_size`,Call,<Offset trace>,Parameter `i`,<Length trace>,Parameter `this->_size`,Array declaration,Assignment,Array access: Offset: v->_size Size: v->_size by call to `int_vector_access_at` ]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int1_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 4611686018427387903]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INFERBO_ALLOC_IS_BIG, no_bucket, ERROR, [Assignment,Allocation: Length: 9223372036854775807]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int2_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 9223372036854775807):unsigned64]
@ -74,25 +72,25 @@ codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INFERBO_ALLOC_IS
codetoanalyze/cpp/bufferoverrun/std_array.cpp, new_int3_Bad, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [<RHS trace>,Assignment,Binary operation: (4 × 18446744073709551615):unsigned64]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, normal_array_bo, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
codetoanalyze/cpp/bufferoverrun/std_array.cpp, std_array_bo_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 42 Size: 42]
codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `this->h`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/symb_arr.cpp, symb_arr_alloc_symb_arr_access_bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Parameter `this->h[*]`,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 6 Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,<Length trace>,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [45, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 4 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, assert_Good_FP, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, data_Bad, 4, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Call,<Length trace>,Call,Parameter `__n`,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Array declaration,Assignment,Assignment,Array access: Offset: [-oo, +oo] Size: 5]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 7, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,Binary operation: ([0, +oo] + 1):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 10, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,<LHS trace>,Parameter `this->infer_size`,<RHS trace>,Parameter `__n`,Binary operation: ([3, +oo] + 42):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [45, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: __infer_skip_function,Call,<Length trace>,Parameter `*__il`,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,<RHS trace>,Parameter `this->infer_size`,Binary operation: (4 × [0, +oo]):unsigned64]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: v->infer_size Size: v->infer_size]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0->a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `this->a`,Assignment,Array access: Offset: -1 Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `init`,Assignment,Call,Parameter `__param_0->a`,Assignment,Call,<Length trace>,Parameter `count`,Call,Parameter `this->a`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `__n`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Allocation: Length: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Call,Unknown value from: std::distance<const_int_*>,Call,Parameter `__n`,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Parameter `v->infer_size`,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: v->infer_size Size: v->infer_size]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,Parameter `*init`,Assignment,Call,Parameter `*__param_0->a`,Assignment,Call,<Length trace>,Parameter `*v->a`,Call,Parameter `*this->a`,Assignment,Array access: Offset: -1 Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, precise_subst_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [Array declaration,Call,Parameter `*init`,Assignment,Call,Parameter `*__param_0->a`,Assignment,Call,<Length trace>,Parameter `*v->a`,Call,Parameter `*this->a`,Assignment,Array access: Offset: [-1, 0] Size: 10 by call to `access_minus_one` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 1 Size: 1]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,<Offset trace>,Parameter `index`,<Length trace>,Parameter `this->infer_size`,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, INFERBO_ALLOC_IS_ZERO, no_bucket, ERROR, [Call,Call,Assignment,Call,Parameter `this->infer_size`,Call,Parameter `this->infer_size`,Allocation: Length: 0]
codetoanalyze/cpp/bufferoverrun/vector.cpp, safe_access3_Good, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]

12
infer/tests/codetoanalyze/cpp/bufferoverrun/repro1.cpp
Unescape View File

@ -78,7 +78,7 @@ struct LM {
if (t.bI == kBN) {
return;
}
uI_FP(t.bI, o);
uI(t.bI, o);
t.bI = kBN;
}
@ -93,7 +93,7 @@ struct LM {
}
t.bI = bi;
}
void uI_FP(BI bi, const lo& o) { b[bi - 1]->u(o); }
void uI(BI bi, const lo& o) { b[bi - 1]->u(o); }
std::vector<std::unique_ptr<B>> b;
};
@ -103,13 +103,13 @@ typedef TFM LMDM;
static LM<LMDM>* al;
static inline void ral(lt* t, ai a) {
static inline void ral_FP(lt* t, ai a) {
ASSERT(t);
lo o = alo(a);
al->u(*t, o);
}
static inline void gal(lt* t, ai a) {
static inline void gal_FP(lt* t, ai a) {
ASSERT(t);
lo o = alo(a);
if (__infer_nondet_int()) {
@ -137,6 +137,6 @@ static void am_Good_FP(im* it) {
const arh* ch = (const arh*)it->gKPC();
const ai a = aft(ch->i1);
lt at;
gal(&at, a);
ral(&at, a);
gal_FP(&at, a);
ral_FP(&at, a);
}

4
infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java
Unescape View File

@ -52,9 +52,7 @@ class UnknownCallsTest {
for (Character c : input.toCharArray()) {}
}
// We can't instantiate loop_over_charArray properly because I don't
// know what to do with the symbol for the call to "toCharArray()"
private static void call_loop_over_charArray_FN(StringBuilder out, String in) {
private static void call_loop_over_charArray(StringBuilder out, String in) {
loop_over_charArray(out, in);
}
}

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

@ -122,12 +122,30 @@ codetoanalyze/java/performance/Invariant.java, Invariant.x_is_invariant_ok(int):
codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 ⋅ (parts.length.ub - 1) + 4 ⋅ parts.length.ub, degree = 1]
codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 ⋅ (parts.length.ub - 1) + 4 ⋅ parts.length.ub, degree = 1]
codetoanalyze/java/performance/IteratorTest.java, IteratorTest.appendTo(java.util.Iterator):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 ⋅ (parts.length.ub - 1) + 4 ⋅ parts.length.ub, degree = 1]
codetoanalyze/java/performance/JsonArray.java, libraries.marauder.analytics.utils.json.JsonArray.addStringEntry(java.lang.String):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 52 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,boolean):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,boolean):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 64 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,double):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,double):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 64 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.Object):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.Object):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 64 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,java.lang.String):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 64 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,libraries.marauder.analytics.utils.json.JsonType):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 87 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,libraries.marauder.analytics.utils.json.JsonType):void, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 91 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,long):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 60 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addEntry(java.lang.String,long):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 64 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonMap.java, libraries.marauder.analytics.utils.json.JsonMap.addKeyToMap(java.lang.String):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 52 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.<init>(java.lang.String), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 50 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonString.java, libraries.marauder.analytics.utils.json.JsonString.<init>(java.lang.String), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 44 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 11 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 38 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 22 + 74 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 251, degree = 0]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0]
@ -138,7 +156,7 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `a[*]`,<RHS trace>,Parameter `b[*]`,Binary operation: (a[*] × b[*]):signed64]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Parameter `a`,<RHS trace>,Parameter `b`,Binary operation: (a.length × b.length):signed64]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 71 ⋅ (length.ub - 1)² + 8 ⋅ length.ub, degree = 2]
@ -153,6 +171,7 @@ codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switc
codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]
codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 13, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]
codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 13 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ (int JSONArray.length().ub), degree = 1]
codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ (int JSONArray.length().ub), degree = 1]
codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_quadratic(org.json.JSONArray):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ (int JSONArray.length().ub)² + 4 ⋅ (1+max(0, int JSONArray.length().ub)), degree = 2]
@ -161,5 +180,5 @@ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over
codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 13 ⋅ (char[] String.toCharArray().length.ub), degree = 1]
codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 6 ⋅ (int InputStream.read(byte[],int,int).ub + int Math.min(int,int).ub), degree = 1]
codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 17 + 6 ⋅ (int InputStream.read(byte[],int,int).ub + int Math.min(int,int).ub), degree = 1]
codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 17 + 6 ⋅ (int Math.min(int,int).ub + int InputStream.read(byte[],int,int).ub), degree = 1]
codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 6 ⋅ (int Math.min(int,int).ub + int InputStream.read(byte[],int,int).ub), degree = 1]

Write Preview
Loading…
Cancel
Save