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

[inferbo] Use SymbolPath map in summary instead of entry memory

Browse Source 
Summary: It uses a SymbolPath map to Symbol in Inferbo's summary instead of an entry memory of callee, which is used for instantiations of the abstract memories on function calls.

Reviewed By: mbouaziz

Differential Revision: D9081631

fbshipit-source-id: 478cda0de
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent ba4f33089e
commit df80ccda08
9 changed files with 227 additions and 203 deletions
Show Stats Download Patch File Download Diff File

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

@ -32,12 +32,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
module CFG = CFG module CFG = CFG
module Domain = Dom.Mem module Domain = Dom.Mem
type extras = ProcData.no_extras type extras = Itv.SymbolTable.t
let declare_symbolic_val let declare_symbolic_val
: Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t -> node_hash:int -> Location.t -> Loc.t : Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial -> Tenv.t -> node_hash:int
-> Typ.typ -> inst_num:int -> new_sym_num:Itv.Counter.t -> Domain.t -> Domain.t = -> Location.t -> Loc.t -> Typ.typ -> inst_num:int -> new_sym_num:Itv.Counter.t -> Domain.t
fun pname path tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem -> -> Domain.t =
fun pname symbol_table path tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem ->
let max_depth = 2 in let max_depth = 2 in
let new_alloc_num = Itv.Counter.make 1 in let new_alloc_num = Itv.Counter.make 1 in
let rec decl_sym_val pname path tenv ~node_hash location ~depth ~may_last_field loc typ mem = let rec decl_sym_val pname path tenv ~node_hash location ~depth ~may_last_field loc typ mem =
@ -48,13 +49,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Typ.Tint ikind -> | Typ.Tint ikind ->
let unsigned = Typ.ikind_is_unsigned ikind in let unsigned = Typ.ikind_is_unsigned ikind in
let v = let v =
Dom.Val.make_sym ~unsigned loc pname path new_sym_num Dom.Val.make_sym ~unsigned loc pname symbol_table path new_sym_num
|> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
in in
mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
| Typ.Tfloat _ -> | Typ.Tfloat _ ->
let v = let v =
Dom.Val.make_sym loc pname path new_sym_num Dom.Val.make_sym loc pname symbol_table path new_sym_num
|> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
in in
mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
@ -63,8 +64,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
~decl_sym_val:(decl_sym_val ~may_last_field:false) ~decl_sym_val:(decl_sym_val ~may_last_field:false)
pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num mem pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num mem
| Typ.Tptr (typ, _) -> | Typ.Tptr (typ, _) ->
BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname path tenv BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname
~node_hash location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem symbol_table path tenv ~node_hash location ~depth loc typ ~inst_num ~new_sym_num
~new_alloc_num mem
| Typ.Tarray {elt; length} -> | Typ.Tarray {elt; length} ->
let size = let size =
match length with match length with
@ -76,12 +78,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let offset = Itv.zero in let offset = Itv.zero in
BoUtils.Exec.decl_sym_arr BoUtils.Exec.decl_sym_arr
~decl_sym_val:(decl_sym_val ~may_last_field:false) ~decl_sym_val:(decl_sym_val ~may_last_field:false)
pname path tenv ~node_hash location ~depth loc elt ~offset ?size ~inst_num pname symbol_table path tenv ~node_hash location ~depth loc elt ~offset ?size
~new_sym_num ~new_alloc_num mem ~inst_num ~new_sym_num ~new_alloc_num mem
| Typ.Tstruct typename -> ( | Typ.Tstruct typename -> (
match Models.TypName.dispatch typename with match Models.TypName.dispatch typename with
| Some {Models.declare_symbolic} -> | Some {Models.declare_symbolic} ->
let model_env = Models.mk_model_env pname node_hash location tenv in let model_env = Models.mk_model_env pname node_hash location tenv symbol_table in
declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env ~depth declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env ~depth
loc ~inst_num ~new_sym_num ~new_alloc_num mem loc ~inst_num ~new_sym_num ~new_alloc_num mem
| None -> | None ->
@ -108,34 +110,33 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let declare_symbolic_parameters let declare_symbolic_parameters
: Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> inst_num:int : Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> Itv.SymbolTable.t
-> (Pvar.t * Typ.t) list -> Dom.Mem.astate -> Dom.Mem.astate = -> inst_num:int -> (Pvar.t * Typ.t) list -> Dom.Mem.astate -> Dom.Mem.astate =
fun pname tenv ~node_hash location ~inst_num formals mem -> fun pname tenv ~node_hash location symbol_table ~inst_num formals mem ->
let new_sym_num = Itv.Counter.make 0 in let new_sym_num = Itv.Counter.make 0 in
let add_formal (mem, inst_num) (pvar, typ) = let add_formal (mem, inst_num) (pvar, typ) =
let loc = Loc.of_pvar pvar in let loc = Loc.of_pvar pvar in
let path = Itv.SymbolPath.of_pvar pvar in let path = Itv.SymbolPath.of_pvar pvar in
let mem = let mem =
declare_symbolic_val pname path tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem declare_symbolic_val pname symbol_table path tenv ~node_hash location loc typ ~inst_num
~new_sym_num mem
in in
(mem, inst_num + 1) (mem, inst_num + 1)
in in
List.fold ~f:add_formal ~init:(mem, inst_num) formals |> fst List.fold ~f:add_formal ~init:(mem, inst_num) formals |> fst
let instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem subst_map mem ret_alias let instantiate_ret ret callee_pname ~callee_exit_mem subst_map mem ret_alias location =
location =
let copy_reachable_new_locs_from locs mem = let copy_reachable_new_locs_from locs mem =
let copy loc acc = let copy loc acc =
let v = Option.value_map (Dom.Mem.find_heap_opt loc callee_exit_mem) ~default:acc ~f:(fun v ->
Dom.Mem.find_heap loc callee_exit_mem |> (fun v -> Dom.Val.subst v subst_map location) let v =
|> Dom.Val.add_trace_elem (Trace.Return location) Dom.Val.subst v subst_map location |> Dom.Val.add_trace_elem (Trace.Return location)
in in
Dom.Mem.add_heap loc v acc Dom.Mem.add_heap loc v acc )
in in
let new_locs = Dom.Mem.get_new_heap_locs ~prev:callee_entry_mem ~next:callee_exit_mem in
let reachable_locs = Dom.Mem.get_reachable_locs_from locs callee_exit_mem in let reachable_locs = Dom.Mem.get_reachable_locs_from locs callee_exit_mem in
PowLoc.fold copy (PowLoc.inter new_locs reachable_locs) mem PowLoc.fold copy reachable_locs mem
in in
let id = fst ret in let id = fst ret in
let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in
@ -148,7 +149,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val) |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val)
let instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem subst_map location mem = let instantiate_param tenv pdesc params callee_exit_mem subst_map location mem =
let formals = Sem.get_formals pdesc in let formals = Sem.get_formals pdesc in
let actuals = List.map ~f:(fun (a, _) -> Sem.eval a mem) params in let actuals = List.map ~f:(fun (a, _) -> Sem.eval a mem) params in
let f mem formal actual = let f mem formal actual =
@ -159,7 +160,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
match Tenv.lookup tenv typename with match Tenv.lookup tenv typename with
| Some str -> | Some str ->
let formal_locs = let formal_locs =
Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_entry_mem Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_exit_mem
|> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc |> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc
in in
let instantiate_fld mem (fn, _, _) = let instantiate_fld mem (fn, _, _) =
@ -174,8 +175,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
mem ) mem )
| _ -> | _ ->
let formal_locs = let formal_locs =
Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_entry_mem Dom.Mem.find_heap (Loc.of_pvar (fst formal)) callee_exit_mem |> Dom.Val.get_array_blk
|> Dom.Val.get_array_blk |> ArrayBlk.get_pow_loc |> ArrayBlk.get_pow_loc
in in
let v = Dom.Mem.find_heap_set formal_locs callee_exit_mem in let v = Dom.Mem.find_heap_set formal_locs callee_exit_mem in
let actual_locs = Dom.Val.get_all_locs actual in let actual_locs = Dom.Val.get_all_locs actual in
@ -197,19 +198,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
: Tenv.t -> Ident.t * Typ.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list : Tenv.t -> Ident.t * Typ.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list
-> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate = -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Mem.astate =
fun tenv ret callee_pdesc callee_pname params caller_mem summary location -> fun tenv ret callee_pdesc callee_pname params caller_mem summary location ->
let callee_entry_mem = Dom.Summary.get_input summary in let callee_symbol_table = Dom.Summary.get_symbol_table summary in
let callee_exit_mem = Dom.Summary.get_output summary in let callee_exit_mem = Dom.Summary.get_output summary in
let callee_ret_alias = Dom.Mem.find_ret_alias callee_exit_mem in
match callee_pdesc with match callee_pdesc with
| Some pdesc -> | Some pdesc ->
let bound_subst_map, ret_alias, rel_subst_map = let bound_subst_map, ret_alias, rel_subst_map =
Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias Sem.get_subst_map tenv pdesc params caller_mem callee_symbol_table callee_exit_mem
in in
let caller_mem = let caller_mem =
instantiate_ret ret callee_pname ~callee_entry_mem ~callee_exit_mem bound_subst_map instantiate_ret ret callee_pname ~callee_exit_mem bound_subst_map caller_mem ret_alias
caller_mem ret_alias location location
|> instantiate_param tenv pdesc params callee_entry_mem callee_exit_mem bound_subst_map |> instantiate_param tenv pdesc params callee_exit_mem bound_subst_map location
location
|> forget_ret_relation ret callee_pname |> forget_ret_relation ret callee_pname
in in
Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem
@ -229,7 +228,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let exec_instr : Dom.Mem.astate -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate = let exec_instr : Dom.Mem.astate -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate =
fun mem {pdesc; tenv} node instr -> fun mem {pdesc; tenv; extras= symbol_table} node instr ->
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
let output_mem = let output_mem =
match instr with match instr with
@ -272,7 +271,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
match Models.Call.dispatch callee_pname params with match Models.Call.dispatch callee_pname params with
| Some {Models.exec} -> | Some {Models.exec} ->
let node_hash = CFG.Node.hash node in let node_hash = CFG.Node.hash node in
let model_env = Models.mk_model_env callee_pname node_hash location tenv in let model_env =
Models.mk_model_env callee_pname node_hash location tenv symbol_table
in
exec model_env ~ret mem exec model_env ~ret mem
| None -> | None ->
match Payload.read pdesc callee_pname with match Payload.read pdesc callee_pname with
@ -299,7 +300,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Typ.Tstruct typname -> ( | Typ.Tstruct typname -> (
match Models.TypName.dispatch typname with match Models.TypName.dispatch typname with
| Some {Models.declare_local} -> | Some {Models.declare_local} ->
let model_env = Models.mk_model_env pname node_hash location tenv in let model_env = Models.mk_model_env pname node_hash location tenv symbol_table in
declare_local ~decl_local model_env loc ~inst_num ~dimension mem declare_local ~decl_local model_env loc ~inst_num ~dimension mem
| None -> | None ->
(mem, inst_num) ) (mem, inst_num) )
@ -312,7 +313,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in in
let mem, inst_num = List.fold ~f:try_decl_local ~init:(mem, 1) locals in let mem, inst_num = List.fold ~f:try_decl_local ~init:(mem, 1) locals in
let formals = Sem.get_formals pdesc in let formals = Sem.get_formals pdesc in
declare_symbolic_parameters pname tenv ~node_hash location ~inst_num formals mem declare_symbolic_parameters pname tenv ~node_hash location symbol_table ~inst_num formals
mem
| Call (_, fun_exp, _, location, _) -> | Call (_, fun_exp, _, location, _) ->
let () = let () =
L.(debug BufferOverrun Verbose) L.(debug BufferOverrun Verbose)
@ -443,12 +445,13 @@ module Report = struct
: Tenv.t -> Typ.Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list -> Dom.Mem.astate : Tenv.t -> Typ.Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list -> Dom.Mem.astate
-> Payload.t -> Location.t -> PO.ConditionSet.t = -> Payload.t -> Location.t -> PO.ConditionSet.t =
fun tenv caller_pname callee_pdesc params caller_mem summary location -> fun tenv caller_pname callee_pdesc params caller_mem summary location ->
let callee_entry_mem = Dom.Summary.get_input summary in let callee_symbol_table = Dom.Summary.get_symbol_table summary in
let callee_exit_mem = Dom.Summary.get_output summary in
let callee_cond = Dom.Summary.get_cond_set summary in let callee_cond = Dom.Summary.get_cond_set summary in
match callee_pdesc with match callee_pdesc with
| Some pdesc -> | Some pdesc ->
let bound_subst_map, _, rel_subst_map = let bound_subst_map, _, rel_subst_map =
Sem.get_subst_map tenv pdesc params caller_mem callee_entry_mem ~callee_ret_alias:None Sem.get_subst_map tenv pdesc params caller_mem callee_symbol_table callee_exit_mem
in in
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
let caller_rel = Dom.Mem.get_relation caller_mem in let caller_rel = Dom.Mem.get_relation caller_mem in
@ -459,9 +462,9 @@ module Report = struct
let check_instr let check_instr
: Procdesc.t -> Tenv.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate -> PO.ConditionSet.t : Procdesc.t -> Tenv.t -> Itv.SymbolTable.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.astate
-> PO.ConditionSet.t = -> PO.ConditionSet.t -> PO.ConditionSet.t =
fun pdesc tenv node instr mem cond_set -> fun pdesc tenv symbol_table node instr mem cond_set ->
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
match instr with match instr with
| Sil.Load (_, exp, _, location) | Sil.Store (exp, _, _, location) -> | Sil.Load (_, exp, _, location) | Sil.Store (exp, _, _, location) ->
@ -470,7 +473,7 @@ module Report = struct
match Models.Call.dispatch callee_pname params with match Models.Call.dispatch callee_pname params with
| Some {Models.check} -> | Some {Models.check} ->
let node_hash = CFG.Node.hash node in let node_hash = CFG.Node.hash node in
check (Models.mk_model_env pname node_hash location tenv) mem cond_set check (Models.mk_model_env pname node_hash location tenv symbol_table) mem cond_set
| None -> | None ->
match Payload.read pdesc callee_pname with match Payload.read pdesc callee_pname with
| Some callee_summary -> | Some callee_summary ->
@ -494,9 +497,10 @@ module Report = struct
let check_instrs let check_instrs
: Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> CFG.Node.t -> Instrs.not_reversed_t : Summary.t -> Procdesc.t -> Tenv.t -> Itv.SymbolTable.t -> CFG.t -> CFG.Node.t
-> Dom.Mem.astate AbstractInterpreter.state -> PO.ConditionSet.t -> PO.ConditionSet.t = -> Instrs.not_reversed_t -> Dom.Mem.astate AbstractInterpreter.state -> PO.ConditionSet.t
fun summary pdesc tenv cfg node instrs state cond_set -> -> PO.ConditionSet.t =
fun summary pdesc tenv symbol_table cfg node instrs state cond_set ->
match state with match state with
| _ when Instrs.is_empty instrs -> | _ when Instrs.is_empty instrs ->
cond_set cond_set
@ -513,27 +517,30 @@ module Report = struct
| NonBottom _ -> | NonBottom _ ->
() ()
in in
let cond_set = check_instr pdesc tenv node instr pre cond_set in let cond_set = check_instr pdesc tenv symbol_table node instr pre cond_set in
print_debug_info instr pre cond_set ; print_debug_info instr pre cond_set ;
cond_set cond_set
let check_node let check_node
: Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t : Summary.t -> Procdesc.t -> Tenv.t -> Itv.SymbolTable.t -> CFG.t -> Analyzer.invariant_map
-> CFG.Node.t -> PO.ConditionSet.t = -> PO.ConditionSet.t -> CFG.Node.t -> PO.ConditionSet.t =
fun summary pdesc tenv cfg inv_map cond_set node -> fun summary pdesc tenv symbol_table cfg inv_map cond_set node ->
match Analyzer.extract_state (CFG.Node.id node) inv_map with match Analyzer.extract_state (CFG.Node.id node) inv_map with
| Some state -> | Some state ->
let instrs = CFG.instrs node in let instrs = CFG.instrs node in
check_instrs summary pdesc tenv cfg node instrs state cond_set check_instrs summary pdesc tenv symbol_table cfg node instrs state cond_set
| _ -> | _ ->
cond_set cond_set
let check_proc let check_proc
: Summary.t -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t = : Summary.t -> Procdesc.t -> Tenv.t -> Itv.SymbolTable.t -> CFG.t -> Analyzer.invariant_map
fun summary pdesc tenv cfg inv_map -> -> PO.ConditionSet.t =
CFG.fold_nodes cfg ~f:(check_node summary pdesc tenv cfg inv_map) ~init:PO.ConditionSet.empty fun summary pdesc tenv symbol_table cfg inv_map ->
CFG.fold_nodes cfg
~f:(check_node summary pdesc tenv symbol_table cfg inv_map)
~init:PO.ConditionSet.empty
let make_err_trace : Trace.t -> string -> Errlog.loc_trace = let make_err_trace : Trace.t -> string -> Errlog.loc_trace =
@ -622,21 +629,23 @@ let get_local_decls cfg =
let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t = let compute_invariant_map_and_check : Callbacks.proc_callback_args -> invariant_map * Summary.t =
fun {proc_desc; tenv; summary} -> fun {proc_desc; tenv; summary} ->
Preanal.do_preanalysis proc_desc tenv ; Preanal.do_preanalysis proc_desc tenv ;
let pdata = ProcData.make_default proc_desc tenv in let symbol_table = Itv.SymbolTable.empty () in
let pdata = ProcData.make proc_desc tenv symbol_table in
let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in
let cfg = CFG.from_pdesc proc_desc in let cfg = CFG.from_pdesc proc_desc in
let locals = get_local_decls cfg in let locals = get_local_decls cfg in
let forget_locals mem = Option.map ~f:(Dom.Mem.forget_locs locals) mem in let exit_mem =
let entry_mem = extract_post (CFG.start_node cfg |> CFG.Node.id) inv_map |> forget_locals in extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map
let exit_mem = extract_post (CFG.exit_node cfg |> CFG.Node.id) inv_map |> forget_locals in |> Option.map ~f:(Dom.Mem.forget_locs locals)
in
let cond_set = let cond_set =
Report.check_proc summary proc_desc tenv cfg inv_map |> Report.report_errors summary proc_desc Report.check_proc summary proc_desc tenv symbol_table cfg inv_map
|> Report.forget_locs locals |> Report.report_errors summary proc_desc |> Report.forget_locs locals
in in
let summary = let summary =
match (entry_mem, exit_mem) with match exit_mem with
| Some entry_mem, Some exit_mem -> | Some exit_mem ->
let post = (entry_mem, exit_mem, cond_set) in let post = (Itv.SymbolTable.summary_of symbol_table, exit_mem, cond_set) in
( if Config.bo_debug >= 1 then ( if Config.bo_debug >= 1 then
let proc_name = Procdesc.get_proc_name proc_desc in let proc_name = Procdesc.get_proc_name proc_desc in
print_summary proc_name post ) ; print_summary proc_name post ) ;

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

@ -147,10 +147,11 @@ module Val = struct
let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i} let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i}
let make_sym let make_sym
: ?unsigned:bool -> Loc.t -> Typ.Procname.t -> Itv.SymbolPath.partial -> Itv.Counter.t -> t = : ?unsigned:bool -> Loc.t -> Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial
fun ?(unsigned= false) loc pname path new_sym_num -> -> Itv.Counter.t -> t =
fun ?(unsigned= false) loc pname symbol_table path new_sym_num ->
{ bot with { bot with
itv= Itv.make_sym ~unsigned pname (Itv.SymbolPath.normal path) new_sym_num itv= Itv.make_sym ~unsigned pname symbol_table (Itv.SymbolPath.normal path) new_sym_num
; sym= Relation.Sym.of_loc loc } ; sym= Relation.Sym.of_loc loc }
@ -363,14 +364,6 @@ module Heap = struct
fun locs v mem -> PowLoc.fold (fun x -> add x (Val.join v (find x mem))) locs mem fun locs v mem -> PowLoc.fold (fun x -> add x (Val.join v (find x mem))) locs mem
let pp_summary : F.formatter -> astate -> unit =
fun fmt mem ->
let pp_map fmt (k, v) = F.fprintf fmt "%a -> %a" Loc.pp k Val.pp_summary v in
F.fprintf fmt "@[<v 2>{ " ;
F.pp_print_list pp_map fmt (bindings mem) ;
F.fprintf fmt " }@]"
let get_return : astate -> Val.t = let get_return : astate -> Val.t =
fun mem -> fun mem ->
let mem = filter (fun l _ -> Loc.is_return l) mem in let mem = filter (fun l _ -> Loc.is_return l) mem in
@ -703,16 +696,14 @@ module MemReach = struct
F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation F.fprintf fmt "@;Relation:@;%a" Relation.pp x.relation
let pp_summary : F.formatter -> t -> unit =
fun fmt x -> F.fprintf fmt "@[<v 0>Parameters:@,%a@]" Heap.pp_summary x.heap
let find_stack : Loc.t -> t -> Val.t = fun k m -> Stack.find k m.stack let find_stack : Loc.t -> t -> Val.t = fun k m -> Stack.find k m.stack
let find_stack_set : PowLoc.t -> t -> Val.t = fun k m -> Stack.find_set k m.stack let find_stack_set : PowLoc.t -> t -> Val.t = fun k m -> Stack.find_set k m.stack
let find_heap : Loc.t -> t -> Val.t = fun k m -> Heap.find k m.heap let find_heap : Loc.t -> t -> Val.t = fun k m -> Heap.find k m.heap
let find_heap_opt : Loc.t -> t -> Val.t option = fun k m -> Heap.find_opt k m.heap
let find_heap_set : PowLoc.t -> t -> Val.t = fun k m -> Heap.find_set k m.heap let find_heap_set : PowLoc.t -> t -> Val.t = fun k m -> Heap.find_set k m.heap
let find_set : PowLoc.t -> t -> Val.t = let find_set : PowLoc.t -> t -> Val.t =
@ -810,12 +801,6 @@ module MemReach = struct
{m with latest_prune= LatestPrune.Top} {m with latest_prune= LatestPrune.Top}
let get_new_heap_locs : prev:t -> next:t -> PowLoc.t =
fun ~prev ~next ->
let add_loc loc _val acc = if Heap.mem loc prev.heap then acc else PowLoc.add loc acc in
Heap.fold add_loc next.heap PowLoc.empty
let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t = let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t =
let add_reachable1 ~root loc v acc = let add_reachable1 ~root loc v acc =
if Loc.equal root loc then PowLoc.union acc (Val.get_all_locs v) if Loc.equal root loc then PowLoc.union acc (Val.get_all_locs v)
@ -884,28 +869,10 @@ module Mem = struct
fun ~default f m -> match m with Bottom -> default | NonBottom m' -> f m' fun ~default f m -> match m with Bottom -> default | NonBottom m' -> f m'
let f_lift_default2 : default:'a -> (MemReach.t -> MemReach.t -> 'a) -> t -> t -> 'a =
fun ~default f m1 m2 ->
match (m1, m2) with
| Bottom, _ | _, Bottom ->
default
| NonBottom m1', NonBottom m2' ->
f m1' m2'
let f_lift : (MemReach.t -> MemReach.t) -> t -> t = let f_lift : (MemReach.t -> MemReach.t) -> t -> t =
fun f -> f_lift_default ~default:Bottom (fun m' -> NonBottom (f m')) fun f -> f_lift_default ~default:Bottom (fun m' -> NonBottom (f m'))
let pp_summary : F.formatter -> t -> unit =
fun fmt m ->
match m with
| Bottom ->
F.pp_print_string fmt "unreachable"
| NonBottom m' ->
MemReach.pp_summary fmt m'
let find_stack : Loc.t -> t -> Val.t = let find_stack : Loc.t -> t -> Val.t =
fun k -> f_lift_default ~default:Val.bot (MemReach.find_stack k) fun k -> f_lift_default ~default:Val.bot (MemReach.find_stack k)
@ -918,6 +885,10 @@ module Mem = struct
fun k -> f_lift_default ~default:Val.bot (MemReach.find_heap k) fun k -> f_lift_default ~default:Val.bot (MemReach.find_heap k)
let find_heap_opt : Loc.t -> t -> Val.t option =
fun k -> f_lift_default ~default:None (MemReach.find_heap_opt k)
let find_heap_set : PowLoc.t -> t -> Val.t = let find_heap_set : PowLoc.t -> t -> Val.t =
fun k -> f_lift_default ~default:Val.bot (MemReach.find_heap_set k) fun k -> f_lift_default ~default:Val.bot (MemReach.find_heap_set k)
@ -968,13 +939,6 @@ module Mem = struct
let get_return : t -> Val.t = f_lift_default ~default:Val.bot MemReach.get_return let get_return : t -> Val.t = f_lift_default ~default:Val.bot MemReach.get_return
let get_new_heap_locs : prev:t -> next:t -> PowLoc.t =
fun ~prev ~next ->
f_lift_default2 ~default:PowLoc.empty
(fun m1 m2 -> MemReach.get_new_heap_locs ~prev:m1 ~next:m2)
prev next
let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t = let get_reachable_locs_from : PowLoc.t -> t -> PowLoc.t =
fun locs -> f_lift_default ~default:PowLoc.empty (MemReach.get_reachable_locs_from locs) fun locs -> f_lift_default ~default:PowLoc.empty (MemReach.get_reachable_locs_from locs)
@ -1034,9 +998,9 @@ module Mem = struct
end end
module Summary = struct module Summary = struct
type t = Mem.t * Mem.t * PO.ConditionSet.t type t = Itv.SymbolTable.summary_t * Mem.t * PO.ConditionSet.t
let get_input : t -> Mem.t = fst3 let get_symbol_table : t -> Itv.SymbolTable.summary_t = fst3
let get_output : t -> Mem.t = snd3 let get_output : t -> Mem.t = snd3
@ -1044,7 +1008,9 @@ module Summary = struct
let get_return : t -> Val.t = fun s -> Mem.get_return (get_output s) let get_return : t -> Val.t = fun s -> Mem.get_return (get_output s)
let pp_symbol_map : F.formatter -> t -> unit = fun fmt s -> Mem.pp_summary fmt (get_input s) let pp_symbol_map : F.formatter -> t -> unit =
fun fmt s -> Itv.SymbolTable.pp fmt (get_symbol_table s)
let pp_return : F.formatter -> t -> unit = let pp_return : F.formatter -> t -> unit =
fun fmt s -> F.fprintf fmt "Return value: %a" Val.pp_summary (get_return s) fun fmt s -> F.fprintf fmt "Return value: %a" Val.pp_summary (get_return s)
@ -1057,6 +1023,7 @@ module Summary = struct
let pp : F.formatter -> t -> unit = let pp : F.formatter -> t -> unit =
fun fmt (entry_mem, exit_mem, condition_set) -> fun fmt (symbol_table, exit_mem, condition_set) ->
F.fprintf fmt "%a@;%a@;%a" Mem.pp entry_mem Mem.pp exit_mem PO.ConditionSet.pp condition_set F.fprintf fmt "%a@;%a@;%a" Itv.SymbolTable.pp symbol_table Mem.pp exit_mem PO.ConditionSet.pp
condition_set
end end

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

@ -17,9 +17,16 @@ module Relation = BufferOverrunDomainRelation
module Trace = BufferOverrunTrace module Trace = BufferOverrunTrace
module TraceSet = Trace.Set module TraceSet = Trace.Set
type model_env = {pname: Typ.Procname.t; node_hash: int; location: Location.t; tenv: Tenv.t} type model_env =
{ pname: Typ.Procname.t
; node_hash: int
; location: Location.t
; tenv: Tenv.t
; symbol_table: Itv.SymbolTable.t }
let mk_model_env pname node_hash location tenv symbol_table =
{pname; node_hash; location; tenv; symbol_table}
let mk_model_env pname node_hash location tenv = {pname; node_hash; location; tenv}
type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.astate -> Dom.Mem.astate type exec_fun = model_env -> ret:Ident.t * Typ.t -> Dom.Mem.astate -> Dom.Mem.astate
@ -247,12 +254,12 @@ module StdArray = struct
BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num
~dimension mem ~dimension mem
in in
let declare_symbolic ~decl_sym_val path {pname; tenv; node_hash; location} ~depth loc ~inst_num let declare_symbolic ~decl_sym_val path {pname; tenv; node_hash; location; symbol_table} ~depth
~new_sym_num ~new_alloc_num mem = loc ~inst_num ~new_sym_num ~new_alloc_num mem =
let offset = Itv.zero in let offset = Itv.zero in
let size = Itv.of_int64 length in let size = Itv.of_int64 length in
BoUtils.Exec.decl_sym_arr ~decl_sym_val pname path tenv ~node_hash location ~depth loc typ BoUtils.Exec.decl_sym_arr ~decl_sym_val pname symbol_table path tenv ~node_hash location
~offset ~size ~inst_num ~new_sym_num ~new_alloc_num mem ~depth loc typ ~offset ~size ~inst_num ~new_sym_num ~new_alloc_num mem
in in
{declare_local; declare_symbolic} {declare_local; declare_symbolic}
@ -307,9 +314,9 @@ module ArrayList = struct
let declare_local ~decl_local:_ {pname; node_hash; location} loc ~inst_num ~dimension mem = let declare_local ~decl_local:_ {pname; node_hash; location} loc ~inst_num ~dimension mem =
BoUtils.Exec.decl_local_arraylist pname ~node_hash location loc ~inst_num ~dimension mem BoUtils.Exec.decl_local_arraylist pname ~node_hash location loc ~inst_num ~dimension mem
in in
let declare_symbolic ~decl_sym_val:_ path {pname; location} ~depth:_ loc ~inst_num:_ let declare_symbolic ~decl_sym_val:_ path {pname; location; symbol_table} ~depth:_ loc
~new_sym_num ~new_alloc_num:_ mem = ~inst_num:_ ~new_sym_num ~new_alloc_num:_ mem =
BoUtils.Exec.decl_sym_arraylist pname path location loc ~new_sym_num mem BoUtils.Exec.decl_sym_arraylist pname symbol_table path location loc ~new_sym_num mem
in in
{declare_local; declare_symbolic} {declare_local; declare_symbolic}

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

@ -484,12 +484,14 @@ let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list =
let get_matching_pairs let get_matching_pairs
: Tenv.t -> Val.t -> Val.t -> Exp.t option -> Typ.t -> Mem.astate -> Mem.astate : Tenv.t -> Itv.SymbolPath.partial -> Val.t -> Val.t -> Exp.t option -> Typ.t -> Mem.astate
-> callee_ret_alias:AliasTarget.t option -> Itv.SymbolTable.summary_t -> Mem.astate
-> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list -> (Itv.Symbol.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
* AliasTarget.t option * AliasTarget.t option
* (Relation.Var.t * Relation.SymExp.t option) list = * (Relation.Var.t * Relation.SymExp.t option) list =
fun tenv formal actual actual_exp_opt typ caller_mem callee_mem ~callee_ret_alias -> fun tenv formal callee_v actual actual_exp_opt typ caller_mem callee_symbol_table callee_exit_mem ->
let open Itv in
let callee_ret_alias = Mem.find_ret_alias callee_exit_mem in
let get_itv v = Val.get_itv v in let get_itv v = Val.get_itv v in
let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in let get_offset v = v |> Val.get_array_blk |> ArrayBlk.offsetof in
let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in let get_size v = v |> Val.get_array_blk |> ArrayBlk.sizeof in
@ -514,13 +516,13 @@ let get_matching_pairs
| None -> | None ->
() ()
in in
let add_pair_itv itv1 itv2 traces l = let add_pair_itv path1 itv2 traces l =
let open Itv in match SymbolTable.find_opt path1 callee_symbol_table with
if itv1 <> bot && itv1 <> top then | Some (lb1, ub1) ->
if Itv.eq itv2 bot then if Itv.eq itv2 bot then (lb1, Bottom, TraceSet.empty) :: (ub1, Bottom, TraceSet.empty) :: l
(lb itv1, Bottom, TraceSet.empty) :: (ub itv1, Bottom, TraceSet.empty) :: l else (lb1, NonBottom (lb itv2), traces) :: (ub1, NonBottom (ub itv2), traces) :: l
else (lb itv1, NonBottom (lb itv2), traces) :: (ub itv1, NonBottom (ub itv2), traces) :: l | _ ->
else l l
in in
let add_pair_sym_main_value v1 v2 ~e2_opt l = let add_pair_sym_main_value v1 v2 ~e2_opt l =
Option.value_map (Val.get_sym_var v1) ~default:l ~f:(fun var -> Option.value_map (Val.get_sym_var v1) ~default:l ~f:(fun var ->
@ -535,12 +537,12 @@ let get_matching_pairs
Option.value_map (Relation.Sym.get_var s1) ~default:l ~f:(fun var -> Option.value_map (Relation.Sym.get_var s1) ~default:l ~f:(fun var ->
(var, Relation.SymExp.of_sym s2) :: l ) (var, Relation.SymExp.of_sym s2) :: l )
in in
let add_pair_val v1 v2 ~e2_opt (bound_pairs, rel_pairs) = let add_pair_val path1 v1 v2 ~e2_opt (bound_pairs, rel_pairs) =
add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
let bound_pairs = let bound_pairs =
bound_pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2) bound_pairs |> add_pair_itv (SymbolPath.normal path1) (get_itv v2) (Val.get_traces v2)
|> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2) |> add_pair_itv (SymbolPath.offset path1) (get_offset v2) (Val.get_traces v2)
|> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2) |> add_pair_itv (SymbolPath.length path1) (get_size v2) (Val.get_traces v2)
in in
let rel_pairs = let rel_pairs =
rel_pairs |> add_pair_sym_main_value v1 v2 ~e2_opt rel_pairs |> add_pair_sym_main_value v1 v2 ~e2_opt
@ -549,44 +551,44 @@ let get_matching_pairs
in in
(bound_pairs, rel_pairs) (bound_pairs, rel_pairs)
in in
let add_pair_field v1 v2 pairs fn = let add_pair_field path1 v1 v2 pairs fn =
add_ret_alias (append_field v1 fn) (append_field v2 fn) ; add_ret_alias (append_field v1 fn) (append_field v2 fn) ;
let v1' = deref_field v1 fn callee_mem in let path1' = SymbolPath.field (SymbolPath.index path1) fn in
let v1' = deref_field v1 fn callee_exit_mem in
let v2' = deref_field v2 fn caller_mem in let v2' = deref_field v2 fn caller_mem in
add_pair_val v1' v2' ~e2_opt:None pairs add_pair_val path1' v1' v2' ~e2_opt:None pairs
in in
let add_pair_ptr typ v1 v2 pairs = let add_pair_ptr typ path1 v1 v2 pairs =
add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ;
match typ.Typ.desc with match typ.Typ.desc with
| Typ.Tptr ({desc= Tstruct typename}, _) -> ( | Typ.Tptr ({desc= Tstruct typename}, _) -> (
match Tenv.lookup tenv typename with match Tenv.lookup tenv typename with
| Some str -> | Some str ->
let fns = List.map ~f:get_field_name str.Typ.Struct.fields in let fns = List.map ~f:get_field_name str.Typ.Struct.fields in
List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns List.fold ~f:(add_pair_field path1 v1 v2) ~init:pairs fns
| _ -> | _ ->
pairs ) pairs )
| Typ.Tptr (_, _) -> | Typ.Tptr (_, _) ->
let v1' = deref_ptr v1 callee_mem in let path1' = SymbolPath.index path1 in
let v1' = deref_ptr v1 callee_exit_mem in
let v2' = deref_ptr v2 caller_mem in let v2' = deref_ptr v2 caller_mem in
add_pair_val v1' v2' ~e2_opt:None pairs add_pair_val path1' v1' v2' ~e2_opt:None pairs
| _ -> | _ ->
pairs pairs
in in
let bound_pairs, rel_pairs = let bound_pairs, rel_pairs =
([], []) |> add_pair_val formal actual ~e2_opt:actual_exp_opt |> add_pair_ptr typ formal actual ([], []) |> add_pair_val formal callee_v actual ~e2_opt:actual_exp_opt
|> add_pair_ptr typ formal callee_v actual
in in
(bound_pairs, !ret_alias, rel_pairs) (bound_pairs, !ret_alias, rel_pairs)
let subst_map_of_bound_pairs let subst_map_of_bound_pairs
: (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list : (Itv.Symbol.t * Itv.Bound.t bottom_lifted * TraceSet.t) list
-> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t = -> Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t =
fun pairs -> fun pairs ->
let add_pair (bound_map, trace_map) (formal, actual, traces) = let add_pair (bound_map, trace_map) (formal, actual, traces) =
if Itv.Bound.is_const formal |> Option.is_some then (bound_map, trace_map) (Itv.SymbolMap.add formal actual bound_map, Itv.SymbolMap.add formal traces trace_map)
else
let symbol = Itv.Bound.get_one_symbol formal in
(Itv.SymbolMap.add symbol actual bound_map, Itv.SymbolMap.add symbol traces trace_map)
in in
List.fold ~f:add_pair ~init:(Itv.SymbolMap.empty, Itv.SymbolMap.empty) pairs List.fold ~f:add_pair ~init:(Itv.SymbolMap.empty, Itv.SymbolMap.empty) pairs
@ -616,17 +618,17 @@ let rec list_fold2_def
let get_subst_map let get_subst_map
: Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Itv.SymbolTable.summary_t
-> callee_ret_alias:AliasTarget.t option -> Mem.astate
-> (Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t) -> (Itv.Bound.t bottom_lifted Itv.SymbolMap.t * TraceSet.t Itv.SymbolMap.t)
* AliasTarget.t option * AliasTarget.t option
* Relation.SubstMap.t = * Relation.SubstMap.t =
fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias -> fun tenv callee_pdesc params caller_mem callee_symbol_table callee_exit_mem ->
let add_pair (formal, typ) (actual, actual_exp) (bound_l, ret_alias, rel_l) = let add_pair (formal, typ) (actual, actual_exp) (bound_l, ret_alias, rel_l) =
let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in let callee_v = Mem.find_heap (Loc.of_pvar formal) callee_exit_mem in
let new_bound_matching, ret_alias', new_rel_matching = let new_bound_matching, ret_alias', new_rel_matching =
get_matching_pairs tenv formal actual actual_exp typ caller_mem callee_entry_mem get_matching_pairs tenv (Itv.SymbolPath.of_pvar formal) callee_v actual actual_exp typ
~callee_ret_alias caller_mem callee_symbol_table callee_exit_mem
in in
( List.rev_append new_bound_matching bound_l ( List.rev_append new_bound_matching bound_l
, Option.first_some ret_alias ret_alias' , Option.first_some ret_alias ret_alias'

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

@ -80,19 +80,21 @@ module Exec = struct
-> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate -> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate
let decl_sym_arr let decl_sym_arr
: decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t : decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial
-> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t
-> ?size:Itv.t -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> ?size:Itv.t -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t
-> Dom.Mem.astate -> Dom.Mem.astate = -> Dom.Mem.astate -> Dom.Mem.astate =
fun ~decl_sym_val pname path tenv ~node_hash location ~depth loc typ ?offset ?size ~inst_num fun ~decl_sym_val pname symbol_table path tenv ~node_hash location ~depth loc typ ?offset ?size
~new_sym_num ~new_alloc_num mem -> ~inst_num ~new_sym_num ~new_alloc_num mem ->
let option_value opt_x default_f = match opt_x with Some x -> x | None -> default_f () in let option_value opt_x default_f = match opt_x with Some x -> x | None -> default_f () in
let offset = let offset =
option_value offset (fun () -> Itv.make_sym pname (Itv.SymbolPath.offset path) new_sym_num) option_value offset (fun () ->
Itv.make_sym pname symbol_table (Itv.SymbolPath.offset path) new_sym_num )
in in
let size = let size =
option_value size (fun () -> option_value size (fun () ->
Itv.make_sym ~unsigned:true pname (Itv.SymbolPath.length path) new_sym_num ) Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num
)
in in
let alloc_num = Itv.Counter.next new_alloc_num in let alloc_num = Itv.Counter.next new_alloc_num in
let elem = Trace.SymAssign (loc, location) in let elem = Trace.SymAssign (loc, location) in
@ -128,12 +130,12 @@ module Exec = struct
let decl_sym_arraylist let decl_sym_arraylist
: Typ.Procname.t -> Itv.SymbolPath.partial -> Location.t -> Loc.t : Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial -> Location.t -> Loc.t
-> new_sym_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate = -> new_sym_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate =
fun pname path location loc ~new_sym_num mem -> fun pname symbol_table path location loc ~new_sym_num mem ->
let size = let size =
Itv.make_sym ~unsigned:true pname (Itv.SymbolPath.length path) new_sym_num |> Dom.Val.of_itv Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num
|> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location)) |> Dom.Val.of_itv |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
in in
Dom.Mem.add_heap loc size mem Dom.Mem.add_heap loc size mem

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

@ -34,10 +34,10 @@ module Exec : sig
-> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate -> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate
val decl_sym_arr : val decl_sym_arr :
decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial
-> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t
-> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> ?size:Itv.t -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t
-> Dom.Mem.astate -> Dom.Mem.astate -> Dom.Mem.astate
val decl_sym_java_ptr : val decl_sym_java_ptr :
decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t decl_sym_val:decl_sym_val -> Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t
@ -45,8 +45,8 @@ module Exec : sig
-> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate
val decl_sym_arraylist : val decl_sym_arraylist :
Typ.Procname.t -> Itv.SymbolPath.partial -> Location.t -> Loc.t -> new_sym_num:Itv.Counter.t Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial -> Location.t -> Loc.t
-> Dom.Mem.astate -> Dom.Mem.astate -> new_sym_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate
val init_array_fields : val init_array_fields :
Tenv.t -> Typ.Procname.t -> node_hash:int -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t Tenv.t -> Typ.Procname.t -> node_hash:int -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t

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

@ -45,7 +45,7 @@ module Boolean = struct
end end
module BoundEnd = struct module BoundEnd = struct
type t = LowerBound | UpperBound type t = LowerBound | UpperBound [@@deriving compare]
let neg = function LowerBound -> UpperBound | UpperBound -> LowerBound let neg = function LowerBound -> UpperBound | UpperBound -> LowerBound
@ -54,8 +54,11 @@ end
module SymbolPath = struct module SymbolPath = struct
type partial = Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial type partial = Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial
[@@deriving compare]
type t = Normal of partial | Offset of partial | Length of partial [@@deriving compare]
type t = Normal of partial | Offset of partial | Length of partial let equal = [%compare.equal : t]
let of_pvar pvar = Pvar pvar let of_pvar pvar = Pvar pvar
@ -99,7 +102,7 @@ module Symbol = struct
let equal = [%compare.equal : t] let equal = [%compare.equal : t]
let paths_equal s1 s2 = phys_equal s1.path s2.path let paths_equal s1 s2 = SymbolPath.equal s1.path s2.path
let make : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t = let make : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t =
fun ~unsigned pname path bound_end id -> {id; pname; unsigned; path; bound_end} fun ~unsigned pname path bound_end id -> {id; pname; unsigned; path; bound_end}
@ -116,6 +119,35 @@ module Symbol = struct
let is_unsigned : t -> bool = fun x -> x.unsigned let is_unsigned : t -> bool = fun x -> x.unsigned
end end
module SymbolTable = struct
module M = PrettyPrintable.MakePPMap (SymbolPath)
type summary_t = (Symbol.t * Symbol.t) M.t
let find_opt = M.find_opt
let pp = M.pp ~pp_value:(fun fmt (lb, ub) -> F.fprintf fmt "[%a, %a]" Symbol.pp lb Symbol.pp ub)
type t = summary_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 =
( Symbol.make ~unsigned pname path LowerBound (Counter.next new_sym_num)
, Symbol.make ~unsigned pname path UpperBound (Counter.next new_sym_num) )
in
symbol_table := M.add path s !symbol_table ;
s
let summary_of x = !x
end
exception Symbol_not_found of Symbol.t exception Symbol_not_found of Symbol.t
module SymbolMap = struct module SymbolMap = struct
@ -178,9 +210,10 @@ module SymLinear = struct
M.for_all2 ~f:le_one_pair x y M.for_all2 ~f:le_one_pair x y
let make : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t = let make : unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t * t =
fun ~unsigned pname path bound_end i -> fun ~unsigned pname symbol_table path new_sym_num ->
singleton_one (Symbol.make ~unsigned pname path bound_end i) let lb, ub = SymbolTable.lookup ~unsigned pname path symbol_table new_sym_num in
(singleton_one lb, singleton_one ub)
let eq : t -> t -> bool = let eq : t -> t -> bool =
@ -1376,17 +1409,10 @@ module ItvPure = struct
let of_int n = of_bound (Bound.of_int n) let of_int n = of_bound (Bound.of_int n)
let make_sym : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> Counter.t -> t = let make_sym : unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t =
fun ~unsigned pname path new_sym_num -> fun ~unsigned pname symbol_table path new_sym_num ->
let lower = let lb, ub = SymLinear.make ~unsigned pname symbol_table path new_sym_num in
Bound.of_sym (Bound.of_sym lb, Bound.of_sym ub)
(SymLinear.make ~unsigned pname path BoundEnd.LowerBound (Counter.next new_sym_num))
in
let upper =
Bound.of_sym
(SymLinear.make ~unsigned pname path BoundEnd.UpperBound (Counter.next new_sym_num))
in
(lower, upper)
let mone = of_bound Bound.mone let mone = of_bound Bound.mone
@ -1820,9 +1846,9 @@ let plus : t -> t -> t = lift2 ItvPure.plus
let minus : t -> t -> t = lift2 ItvPure.minus let minus : t -> t -> t = lift2 ItvPure.minus
let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> Counter.t -> t = let make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t =
fun ?(unsigned= false) pname path new_sym_num -> fun ?(unsigned= false) pname symbol_table path new_sym_num ->
NonBottom (ItvPure.make_sym ~unsigned pname path new_sym_num) NonBottom (ItvPure.make_sym ~unsigned pname symbol_table path new_sym_num)
let neg : t -> t = lift1 ItvPure.neg let neg : t -> t = lift1 ItvPure.neg

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

@ -32,9 +32,9 @@ module Boolean : sig
end end
module SymbolPath : sig module SymbolPath : sig
type partial type partial [@@deriving compare]
type t type t [@@deriving compare]
val of_pvar : Pvar.t -> partial val of_pvar : Pvar.t -> partial
@ -53,6 +53,20 @@ module Symbol : sig
type t type t
end end
module SymbolTable : sig
type summary_t
val pp : F.formatter -> summary_t -> unit
val find_opt : SymbolPath.t -> summary_t -> (Symbol.t * Symbol.t) option
type t
val empty : unit -> t
val summary_of : t -> summary_t
end
module SymbolMap : PrettyPrintable.PPMap with type key = Symbol.t module SymbolMap : PrettyPrintable.PPMap with type key = Symbol.t
module Bound : sig module Bound : sig
@ -66,8 +80,6 @@ module Bound : sig
val is_symbolic : t -> bool val is_symbolic : t -> bool
val get_one_symbol : t -> Symbol.t
val gt : t -> t -> bool val gt : t -> t -> bool
val le : t -> t -> bool val le : t -> t -> bool
@ -197,7 +209,7 @@ val of_int_lit : IntLit.t -> t
val of_int64 : Int64.t -> t val of_int64 : Int64.t -> t
val make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> Counter.t -> t val make_sym : ?unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t
val lb : t -> Bound.t val lb : t -> Bound.t

5
infer/src/checkers/cost.ml
Unescape View File

@ -58,12 +58,11 @@ module TransferFunctionsNodesBasicCost = struct
callee_cost Typ.Procname.pp callee_pname callee_cost Typ.Procname.pp callee_pname
| Some inferbo_summary -> | Some inferbo_summary ->
let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in let inferbo_caller_mem = Option.value_exn inferbo_caller_mem in
let callee_entry_mem = BufferOverrunDomain.Summary.get_input inferbo_summary in let callee_symbol_table = BufferOverrunDomain.Summary.get_symbol_table inferbo_summary in
let callee_exit_mem = BufferOverrunDomain.Summary.get_output inferbo_summary in let callee_exit_mem = BufferOverrunDomain.Summary.get_output inferbo_summary in
let callee_ret_alias = BufferOverrunDomain.Mem.find_ret_alias callee_exit_mem in
let (subst_map, _), _, _ = let (subst_map, _), _, _ =
BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem BufferOverrunSemantics.get_subst_map tenv callee_pdesc params inferbo_caller_mem
callee_entry_mem ~callee_ret_alias callee_symbol_table callee_exit_mem
in in
BasicCost.subst callee_cost subst_map BasicCost.subst callee_cost subst_map

Write Preview
Loading…
Cancel
Save