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

[inferbo] Refactoring 4/8: pass node_hash instead of node

Browse Source 
Reviewed By: jvillard

Differential Revision: D7397127

fbshipit-source-id: 9add195
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent 672fd3a9a5
commit 6838fed3e6
4 changed files with 75 additions and 68 deletions
Show Stats Download Patch File Download Diff File

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

@ -38,12 +38,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
type extras = Typ.Procname.t -> Procdesc.t option type extras = Typ.Procname.t -> Procdesc.t option
let declare_symbolic_val let declare_symbolic_val
: Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> Loc.t -> Typ.typ -> inst_num:int : Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> Loc.t -> Typ.typ -> inst_num:int
-> new_sym_num:Itv.Counter.t -> Domain.t -> Domain.t = -> new_sym_num:Itv.Counter.t -> Domain.t -> Domain.t =
fun pname tenv node location loc typ ~inst_num ~new_sym_num mem -> fun pname 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 tenv node location ~depth ~may_last_field loc typ mem = let rec decl_sym_val pname tenv ~node_hash location ~depth ~may_last_field loc typ mem =
if depth > max_depth then mem if depth > max_depth then mem
else else
let depth = depth + 1 in let depth = depth + 1 in
@ -62,8 +62,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in in
Dom.Mem.add_heap loc v mem Dom.Mem.add_heap loc v mem
| Typ.Tptr (typ, _) -> | Typ.Tptr (typ, _) ->
BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname tenv node BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname tenv
location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem ~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
@ -75,18 +75,18 @@ 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 tenv node location ~depth loc elt ~offset ?size ~inst_num ~new_sym_num pname tenv ~node_hash location ~depth loc elt ~offset ?size ~inst_num ~new_sym_num
~new_alloc_num mem ~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 location tenv in let model_env = Models.mk_model_env pname node_hash location tenv in
declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) model_env ~depth loc declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) model_env ~depth loc
~inst_num ~new_sym_num ~new_alloc_num mem ~inst_num ~new_sym_num ~new_alloc_num mem
| None -> | None ->
let decl_fld ~may_last_field mem (fn, typ, _) = let decl_fld ~may_last_field mem (fn, typ, _) =
let loc_fld = Loc.append_field loc ~fn in let loc_fld = Loc.append_field loc ~fn in
decl_sym_val pname tenv node location ~depth loc_fld typ ~may_last_field mem decl_sym_val pname tenv ~node_hash location ~depth loc_fld typ ~may_last_field mem
in in
let decl_flds str = let decl_flds str =
IList.fold_last ~f:(decl_fld ~may_last_field:false) IList.fold_last ~f:(decl_fld ~may_last_field:false)
@ -98,20 +98,22 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
if Config.bo_debug >= 3 then if Config.bo_debug >= 3 then
L.(debug BufferOverrun Verbose) L.(debug BufferOverrun Verbose)
"/!\\ decl_fld of unhandled type: %a at %a@." (Typ.pp Pp.text) typ Location.pp "/!\\ decl_fld of unhandled type: %a at %a@." (Typ.pp Pp.text) typ Location.pp
(CFG.loc node) ; location ;
mem mem
in in
decl_sym_val pname tenv node location ~depth:0 ~may_last_field:true loc typ mem decl_sym_val pname tenv ~node_hash location ~depth:0 ~may_last_field:true loc typ mem
let declare_symbolic_parameters let declare_symbolic_parameters
: Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> inst_num:int -> (Pvar.t * Typ.t) list : Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> inst_num:int
-> Dom.Mem.astate -> Dom.Mem.astate = -> (Pvar.t * Typ.t) list -> Dom.Mem.astate -> Dom.Mem.astate =
fun pname tenv node location ~inst_num formals mem -> fun pname tenv ~node_hash location ~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 mem = declare_symbolic_val pname tenv node location loc typ ~inst_num ~new_sym_num mem in let mem =
declare_symbolic_val pname tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem
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
@ -249,7 +251,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Call (ret, Const Cfun callee_pname, params, location, _) -> ( | Call (ret, Const Cfun callee_pname, params, location, _) -> (
match Models.Call.dispatch callee_pname params with match Models.Call.dispatch callee_pname params with
| Some {Models.exec} -> | Some {Models.exec} ->
let model_env = Models.mk_model_env callee_pname node location tenv ?ret in let node_hash = CFG.hash node in
let model_env = Models.mk_model_env callee_pname node_hash location tenv ?ret in
exec model_env mem exec model_env mem
| None -> | None ->
match Summary.read_summary pdesc callee_pname with match Summary.read_summary pdesc callee_pname with
@ -265,16 +268,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
) )
| Declare_locals (locals, location) -> | Declare_locals (locals, location) ->
(* array allocation in stack e.g., int arr[10] *) (* array allocation in stack e.g., int arr[10] *)
let rec decl_local pname node location loc typ ~inst_num ~dimension mem = let node_hash = CFG.hash node in
let rec decl_local pname ~node_hash location loc typ ~inst_num ~dimension mem =
match typ.Typ.desc with match typ.Typ.desc with
| Typ.Tarray {elt= typ; length; stride} -> | Typ.Tarray {elt= typ; length; stride} ->
let stride = Option.map ~f:IntLit.to_int stride in let stride = Option.map ~f:IntLit.to_int stride in
BoUtils.Exec.decl_local_array ~decl_local pname node location loc typ ~length BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length
?stride ~inst_num ~dimension mem ?stride ~inst_num ~dimension mem
| 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 location tenv in let model_env = Models.mk_model_env pname node_hash location tenv 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) )
@ -283,11 +287,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in in
let try_decl_local (mem, inst_num) (pvar, typ) = let try_decl_local (mem, inst_num) (pvar, typ) =
let loc = Loc.of_pvar pvar in let loc = Loc.of_pvar pvar in
decl_local pname node location loc typ ~inst_num ~dimension:1 mem decl_local pname ~node_hash location loc typ ~inst_num ~dimension:1 mem
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 location ~inst_num formals mem declare_symbolic_parameters pname tenv ~node_hash location ~inst_num formals mem
| Call (_, fun_exp, _, location, _) -> | Call (_, fun_exp, _, location, _) ->
let () = let () =
L.(debug BufferOverrun Verbose) L.(debug BufferOverrun Verbose)
@ -455,7 +459,8 @@ module Report = struct
| Sil.Call (_, Const Cfun callee_pname, params, location, _) -> ( | Sil.Call (_, Const Cfun callee_pname, params, location, _) -> (
match Models.Call.dispatch callee_pname params with match Models.Call.dispatch callee_pname params with
| Some {Models.check} -> | Some {Models.check} ->
check (Models.mk_model_env pname node location tenv) mem cond_set let node_hash = CFG.hash node in
check (Models.mk_model_env pname node_hash location tenv) mem cond_set
| None -> | None ->
match Summary.read_summary pdesc callee_pname with match Summary.read_summary pdesc callee_pname with
| Some callee_summary -> | Some callee_summary ->

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

@ -22,12 +22,12 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
type model_env = type model_env =
{ pname: Typ.Procname.t { pname: Typ.Procname.t
; node: CFG.node ; node_hash: int
; location: Location.t ; location: Location.t
; tenv: Tenv.t ; tenv: Tenv.t
; ret: (Ident.t * Typ.t) option } ; ret: (Ident.t * Typ.t) option }
let mk_model_env pname node location ?ret tenv = {pname; node; location; tenv; ret} let mk_model_env pname node_hash location ?ret tenv = {pname; node_hash; location; tenv; ret}
type exec_fun = model_env -> Dom.Mem.astate -> Dom.Mem.astate type exec_fun = model_env -> Dom.Mem.astate -> Dom.Mem.astate
@ -73,19 +73,19 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
PO.ConditionSet.add_alloc_size pname location ~length traces cond_set PO.ConditionSet.add_alloc_size pname location ~length traces cond_set
let set_uninitialized node (typ: Typ.t) ploc mem = let set_uninitialized location (typ: Typ.t) ploc mem =
match typ.desc with match typ.desc with
| Tint _ | Tfloat _ -> | Tint _ | Tfloat _ ->
Dom.Mem.weak_update_heap ploc Dom.Val.Itv.top mem Dom.Mem.weak_update_heap ploc Dom.Val.Itv.top mem
| _ -> | _ ->
L.(debug BufferOverrun Verbose) L.(debug BufferOverrun Verbose)
"/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp "/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp
(CFG.loc node) ; location ;
mem mem
let malloc size_exp = let malloc size_exp =
let exec {pname; ret; node; location; tenv} mem = let exec {pname; ret; node_hash; location; tenv} mem =
match ret with match ret with
| Some (id, _) -> | Some (id, _) ->
let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in
@ -93,16 +93,16 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
let length = Sem.eval length0 mem in let length = Sem.eval length0 mem in
let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in
let v = let v =
Sem.eval_array_alloc pname node typ ?stride Itv.zero (Dom.Val.get_itv length) 0 1 Sem.eval_array_alloc pname ~node_hash typ ?stride Itv.zero (Dom.Val.get_itv length) 0 1
|> Dom.Val.set_traces traces |> Dom.Val.set_traces traces
in in
mem |> Dom.Mem.add_stack (Loc.of_id id) v mem |> Dom.Mem.add_stack (Loc.of_id id) v
|> set_uninitialized node typ (Dom.Val.get_array_locs v) |> set_uninitialized location typ (Dom.Val.get_array_locs v)
|> BoUtils.Exec.init_array_fields tenv pname node typ (Dom.Val.get_array_locs v) |> BoUtils.Exec.init_array_fields tenv pname ~node_hash typ (Dom.Val.get_array_locs v)
?dyn_length ?dyn_length
| _ -> | _ ->
L.(debug BufferOverrun Verbose) L.(debug BufferOverrun Verbose)
"/!\\ Do not know where to model malloc at %a@\n" Location.pp (CFG.loc node) ; "/!\\ Do not know where to model malloc at %a@\n" Location.pp location ;
mem mem
and check = check_alloc_size size_exp in and check = check_alloc_size size_exp in
{exec; check} {exec; check}
@ -197,14 +197,14 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
let set_array_length array length_exp = let set_array_length array length_exp =
let exec {pname; node} mem = let exec {pname; node_hash; location} mem =
match array with match array with
| Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} -> | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} ->
let length = Sem.eval length_exp mem |> Dom.Val.get_itv in let length = Sem.eval length_exp mem |> Dom.Val.get_itv in
let stride = Option.map ~f:IntLit.to_int stride in let stride = Option.map ~f:IntLit.to_int stride in
let v = Sem.eval_array_alloc pname node elt ?stride Itv.zero length 0 1 in let v = Sem.eval_array_alloc pname ~node_hash elt ?stride Itv.zero length 0 1 in
mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v
|> set_uninitialized node elt (Dom.Val.get_array_locs v) |> set_uninitialized location elt (Dom.Val.get_array_locs v)
| _ -> | _ ->
L.(die InternalError) "Unexpected type of first argument for __set_array_length()" L.(die InternalError) "Unexpected type of first argument for __set_array_length()"
and check = check_alloc_size length_exp in and check = check_alloc_size length_exp in
@ -254,18 +254,18 @@ module Make (BoUtils : BufferOverrunUtils.S) = struct
module StdArray = struct module StdArray = struct
let typ typ length = let typ typ length =
let declare_local ~decl_local {pname; node; location} loc ~inst_num ~dimension mem = let declare_local ~decl_local {pname; node_hash; location} loc ~inst_num ~dimension mem =
(* should this be deferred to the constructor? *) (* should this be deferred to the constructor? *)
let length = Some (IntLit.of_int64 length) in let length = Some (IntLit.of_int64 length) in
BoUtils.Exec.decl_local_array ~decl_local pname node location loc typ ~length ~inst_num BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length
~dimension mem ~inst_num ~dimension mem
in in
let declare_symbolic ~decl_sym_val {pname; tenv; node; location} ~depth loc ~inst_num let declare_symbolic ~decl_sym_val {pname; tenv; node_hash; location} ~depth loc ~inst_num
~new_sym_num ~new_alloc_num mem = ~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 tenv node location ~depth loc typ ~offset BoUtils.Exec.decl_sym_arr ~decl_sym_val pname tenv ~node_hash location ~depth loc typ
~size ~inst_num ~new_sym_num ~new_alloc_num mem ~offset ~size ~inst_num ~new_sym_num ~new_alloc_num mem
in in
{declare_local; declare_symbolic} {declare_local; declare_symbolic}

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

@ -318,19 +318,20 @@ module Make (CFG : ProcCfg.S) = struct
Val.bot Val.bot
let get_allocsite : Typ.Procname.t -> CFG.node -> int -> int -> string = let get_allocsite : Typ.Procname.t -> node_hash:int -> int -> int -> string =
fun proc_name node inst_num dimension -> fun proc_name ~node_hash inst_num dimension ->
let proc_name = Typ.Procname.to_string proc_name in let proc_name = Typ.Procname.to_string proc_name in
let node_num = CFG.hash node |> string_of_int in let node_num = string_of_int node_hash in
let inst_num = string_of_int inst_num in let inst_num = string_of_int inst_num in
let dimension = string_of_int dimension in let dimension = string_of_int dimension in
proc_name ^ "-" ^ node_num ^ "-" ^ inst_num ^ "-" ^ dimension |> Allocsite.make proc_name ^ "-" ^ node_num ^ "-" ^ inst_num ^ "-" ^ dimension |> Allocsite.make
let eval_array_alloc let eval_array_alloc
: Typ.Procname.t -> CFG.node -> Typ.t -> ?stride:int -> Itv.t -> Itv.t -> int -> int -> Val.t = : Typ.Procname.t -> node_hash:int -> Typ.t -> ?stride:int -> Itv.t -> Itv.t -> int -> int
fun pdesc node typ ?stride:stride0 offset size inst_num dimension -> -> Val.t =
let allocsite = get_allocsite pdesc node inst_num dimension in fun pdesc ~node_hash typ ?stride:stride0 offset size inst_num dimension ->
let allocsite = get_allocsite pdesc ~node_hash inst_num dimension in
let int_stride = match stride0 with None -> sizeof typ | Some stride -> stride in let int_stride = match stride0 with None -> sizeof typ | Some stride -> stride in
let stride = Itv.of_int int_stride in let stride = Itv.of_int int_stride in
ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk

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

@ -25,26 +25,26 @@ module type S = sig
val load_val : Ident.t -> Dom.Val.astate -> Dom.Mem.astate -> Dom.Mem.astate val load_val : Ident.t -> Dom.Val.astate -> Dom.Mem.astate -> Dom.Mem.astate
type decl_local = type decl_local =
Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t -> inst_num:int -> dimension:int Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t -> inst_num:int
-> Dom.Mem.astate -> Dom.Mem.astate * int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int
val decl_local_array : val decl_local_array :
decl_local:decl_local -> Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t decl_local:decl_local -> Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t
-> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate
-> Dom.Mem.astate * int -> Dom.Mem.astate * int
type decl_sym_val = type decl_sym_val =
Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> depth:int -> Loc.t -> Typ.t Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t
-> Dom.Mem.astate -> Dom.Mem.astate -> Dom.Mem.astate -> Dom.Mem.astate
val decl_sym_arr : val decl_sym_arr :
decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> depth:int decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t
-> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int -> 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 -> Dom.Mem.astate -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate
-> Dom.Mem.astate -> Dom.Mem.astate
val init_array_fields : val init_array_fields :
Tenv.t -> Typ.Procname.t -> CFG.node -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t Tenv.t -> Typ.Procname.t -> node_hash:int -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t
-> Dom.Mem.astate -> Dom.Mem.astate -> Dom.Mem.astate -> Dom.Mem.astate
val set_dyn_length : Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.astate -> Dom.Mem.astate val set_dyn_length : Tenv.t -> Typ.t -> PowLoc.t -> Itv.t -> Dom.Mem.astate -> Dom.Mem.astate
@ -71,41 +71,41 @@ module Make (CFG : ProcCfg.S) = struct
type decl_local = type decl_local =
Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t -> inst_num:int -> dimension:int Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t -> inst_num:int
-> Dom.Mem.astate -> Dom.Mem.astate * int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int
let decl_local_array let decl_local_array
: decl_local:decl_local -> Typ.Procname.t -> CFG.node -> Location.t -> Loc.t -> Typ.t : decl_local:decl_local -> Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t
-> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int
-> Dom.Mem.astate -> Dom.Mem.astate * int = -> Dom.Mem.astate -> Dom.Mem.astate * int =
fun ~decl_local pname node location loc typ ~length ?stride ~inst_num ~dimension mem -> fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num ~dimension mem ->
let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in
let arr = let arr =
Sem.eval_array_alloc pname node typ Itv.zero size ?stride inst_num dimension Sem.eval_array_alloc pname ~node_hash typ Itv.zero size ?stride inst_num dimension
|> Dom.Val.add_trace_elem (Trace.ArrDecl location) |> Dom.Val.add_trace_elem (Trace.ArrDecl location)
in in
let mem = let mem =
if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem
else Dom.Mem.add_heap loc arr mem else Dom.Mem.add_heap loc arr mem
in in
let loc = Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension) in let loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash inst_num dimension) in
let mem, _ = let mem, _ =
decl_local pname node location loc typ ~inst_num ~dimension:(dimension + 1) mem decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem
in in
(mem, inst_num + 1) (mem, inst_num + 1)
type decl_sym_val = type decl_sym_val =
Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t -> depth:int -> Loc.t -> Typ.t Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t
-> Dom.Mem.astate -> Dom.Mem.astate -> Dom.Mem.astate -> Dom.Mem.astate
let decl_sym_arr let decl_sym_arr
: decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> CFG.node -> Location.t : decl_sym_val:decl_sym_val -> Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t
-> depth:int -> Loc.t -> Typ.t -> ?offset:Itv.t -> ?size:Itv.t -> inst_num:int -> 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 -> Dom.Mem.astate -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate
-> Dom.Mem.astate = -> Dom.Mem.astate =
fun ~decl_sym_val pname tenv node location ~depth loc typ ?offset ?size ~inst_num ~new_sym_num fun ~decl_sym_val pname tenv ~node_hash location ~depth loc typ ?offset ?size ~inst_num
~new_alloc_num mem -> ~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 itv_make_sym () = Itv.make_sym pname new_sym_num in let itv_make_sym () = Itv.make_sym pname new_sym_num in
let offset = option_value offset itv_make_sym in let offset = option_value offset itv_make_sym in
@ -113,15 +113,15 @@ module Make (CFG : ProcCfg.S) = struct
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
let arr = let arr =
Sem.eval_array_alloc pname node typ offset size inst_num alloc_num Sem.eval_array_alloc pname ~node_hash typ offset size inst_num alloc_num
|> Dom.Val.add_trace_elem elem |> Dom.Val.add_trace_elem elem
in in
let mem = Dom.Mem.add_heap loc arr mem in let mem = Dom.Mem.add_heap loc arr mem in
let deref_loc = Loc.of_allocsite (Sem.get_allocsite pname node inst_num alloc_num) in let deref_loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash inst_num alloc_num) in
decl_sym_val pname tenv node location ~depth deref_loc typ mem decl_sym_val pname tenv ~node_hash location ~depth deref_loc typ mem
let init_array_fields tenv pname node typ locs ?dyn_length mem = let init_array_fields tenv pname ~node_hash typ locs ?dyn_length mem =
let rec init_field locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) = let rec init_field locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) =
let field_loc = PowLoc.append_field locs ~fn:field_name in let field_loc = PowLoc.append_field locs ~fn:field_name in
let mem = let mem =
@ -135,7 +135,8 @@ module Make (CFG : ProcCfg.S) = struct
in in
let stride = Option.map stride ~f:IntLit.to_int in let stride = Option.map stride ~f:IntLit.to_int in
let v = let v =
Sem.eval_array_alloc pname node typ ?stride Itv.zero length inst_num dimension Sem.eval_array_alloc pname ~node_hash typ ?stride Itv.zero length inst_num
dimension
in in
Dom.Mem.strong_update_heap field_loc v mem Dom.Mem.strong_update_heap field_loc v mem
| _ -> | _ ->

Write Preview
Loading…
Cancel
Save