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

[dispatcher] + Capture function argument

Browse Source 
Summary:
Allow capturing function arguments.
Model functions don't have to match on a list any more.

Depends on D6347829

Reviewed By: jvillard

Differential Revision: D6350628

fbshipit-source-id: e88b758
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent 7f3467b01d
commit a73162d8e4
4 changed files with 101 additions and 99 deletions
Show Stats Download Patch File Download Diff File

77
infer/src/IR/ProcnameDispatcher.ml
Unescape View File

@ -100,15 +100,16 @@ type ('f_in, 'f_out, 'captured_types) proc_matcher =
{ on_objc_cpp: 'f_in -> objc_cpp -> ('f_out * 'captured_types) option { on_objc_cpp: 'f_in -> objc_cpp -> ('f_out * 'captured_types) option
; on_c: 'f_in -> c -> ('f_out * 'captured_types) option } ; on_c: 'f_in -> c -> ('f_out * 'captured_types) option }
type 'captured_types on_args = 'captured_types -> FuncArg.t list -> FuncArg.t list option type ('f_in, 'f_out, 'captured_types) on_args =
'captured_types -> 'f_in * FuncArg.t list -> ('f_out * FuncArg.t list) option
type ('f_in, 'f_out, 'captured_types, 'markers) args_matcher = type ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher =
{ on_proc: ('f_in, 'f_out, 'captured_types) proc_matcher { on_proc: ('f_in, 'f_proc_out, 'captured_types) proc_matcher
; on_args: 'captured_types on_args ; on_args: ('f_proc_out, 'f_out, 'captured_types) on_args
; markers: 'markers } ; markers: 'markers }
type ('captured_types, 'markers) func_arg = type ('f_in, 'f_out, 'captured_types, 'markers) func_arg =
{eat_func_arg: 'captured_types on_args; marker_static_checker: 'markers -> bool} {eat_func_arg: ('f_in, 'f_out, 'captured_types) on_args; marker_static_checker: 'markers -> bool}
type 'f matcher = Typ.Procname.t -> FuncArg.t list -> 'f option type 'f matcher = Typ.Procname.t -> FuncArg.t list -> 'f option
@ -127,8 +128,9 @@ let pre_to_opt procname args = function
f procname args f procname args
type ('f, 'captured_types) func_args_end = type ('f_in, 'f_out, 'captured_types) func_args_end =
on_args:'captured_types on_args -> FuncArg.t list -> 'f * 'captured_types -> 'f pre_result on_args:('f_in, 'f_out, 'captured_types) on_args -> FuncArg.t list -> 'f_in * 'captured_types
-> 'f_out pre_result
type ('f_in, 'f_out) all_args_matcher = type ('f_in, 'f_out) all_args_matcher =
{ on_objc_cpp: 'f_in -> objc_cpp -> FuncArg.t list -> 'f_out pre_result { on_objc_cpp: 'f_in -> objc_cpp -> FuncArg.t list -> 'f_out pre_result
@ -244,8 +246,8 @@ let templ_end
let args_begin let args_begin
: ('f_in, 'f_out, 'captured_types, unit, 'markers, non_empty) path_matcher : ('f_in, 'f_out, 'captured_types, unit, 'markers, non_empty) path_matcher
-> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher = -> ('f_in, 'f_out, 'f_out, 'captured_types, 'markers) args_matcher =
let on_args _capt args = Some args in let on_args _capt f_args = Some f_args in
fun m -> fun m ->
let {on_templated_name; path_extra= PathNonEmpty {on_objc_cpp}; get_markers} = m in let {on_templated_name; path_extra= PathNonEmpty {on_objc_cpp}; get_markers} = m in
let markers = get_markers () in let markers = get_markers () in
@ -260,20 +262,20 @@ let args_begin
let args_cons let args_cons
: ('f_in, 'f_out, 'captured_types, 'markers) args_matcher : ('f_in, 'f_proc_out, 'f_interm, 'captured_types, 'markers) args_matcher
-> ('captured_types, 'markers) func_arg -> ('f_interm, 'f_out, 'captured_types, 'markers) func_arg
-> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher = -> ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher =
fun m func_arg -> fun m func_arg ->
let {on_proc; on_args; markers} = m in let {on_proc; on_args; markers} = m in
let {marker_static_checker; eat_func_arg} = func_arg in let {marker_static_checker; eat_func_arg} = func_arg in
assert (marker_static_checker markers) ; assert (marker_static_checker markers) ;
let on_args capt args = on_args capt args |> Option.bind ~f:(eat_func_arg capt) in let on_args capt f_args = on_args capt f_args |> Option.bind ~f:(eat_func_arg capt) in
{on_proc; on_args; markers} {on_proc; on_args; markers}
let args_end let args_end
: ('f_in, 'f_out, 'captured_types, 'markers) args_matcher : ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher
-> ('f_out, 'captured_types) func_args_end -> ('f_in, 'f_out) all_args_matcher = -> ('f_proc_out, 'f_out, 'captured_types) func_args_end -> ('f_in, 'f_out) all_args_matcher =
fun m func_args_end -> fun m func_args_end ->
let {on_proc= {on_c; on_objc_cpp}; on_args} = m in let {on_proc= {on_c; on_objc_cpp}; on_args} = m in
let on_c f c args = on_c f c |> pre_bind_opt ~f:(func_args_end ~on_args args) in let on_c f c args = on_c f c |> pre_bind_opt ~f:(func_args_end ~on_args args) in
@ -381,22 +383,19 @@ let capt_all
let no_checker _ = true let no_checker _ = true
let eat_one_func_arg ~match_if capt = function let eat_one_func_arg ~match_if capt (f, args) =
| arg :: rest when match_if capt arg -> match args with arg :: rest when match_if capt arg -> Some (f, rest) | _ -> None
Some rest
| _ ->
None
(** Eats one arg *) (** Eats one arg *)
let any_arg : (_, _) func_arg = let any_arg : ('f, 'f, _, _) func_arg =
let eat_func_arg capt = eat_one_func_arg ~match_if:(fun _ _ -> true) capt in let eat_func_arg capt = eat_one_func_arg ~match_if:(fun _ _ -> true) capt in
{eat_func_arg; marker_static_checker= no_checker} {eat_func_arg; marker_static_checker= no_checker}
let mk_typ_nth let mk_typ_nth
: ('markers -> 'marker) -> ('captured_types -> 'marker mtyp) -> 'marker : ('markers -> 'marker) -> ('captured_types -> 'marker mtyp) -> 'marker
-> ('captured_types, 'markers) func_arg = -> ('f, 'f, 'captured_types, 'markers) func_arg =
fun get_m get_c marker -> fun get_m get_c marker ->
let marker_static_checker markers = Polymorphic_compare.( = ) marker (get_m markers) in let marker_static_checker markers = Polymorphic_compare.( = ) marker (get_m markers) in
let eat_func_arg = let eat_func_arg =
@ -407,40 +406,48 @@ let mk_typ_nth
(** Matches first captured type *) (** Matches first captured type *)
let typ1 : 'marker -> ('marker mtyp * _, 'marker * _) func_arg = let typ1 : 'marker -> ('f, 'f, 'marker mtyp * _, 'marker * _) func_arg =
let pos1 (x, _) = x in let pos1 (x, _) = x in
fun marker -> mk_typ_nth pos1 pos1 marker fun marker -> mk_typ_nth pos1 pos1 marker
(** Matches second captured type *) (** Matches second captured type *)
let typ2 : 'marker -> (_ * ('marker mtyp * _), _ * ('marker * _)) func_arg = let typ2 : 'marker -> ('f, 'f, _ * ('marker mtyp * _), _ * ('marker * _)) func_arg =
let pos2 (_, (x, _)) = x in let pos2 (_, (x, _)) = x in
fun marker -> mk_typ_nth pos2 pos2 marker fun marker -> mk_typ_nth pos2 pos2 marker
(** Matches third captured type *) (** Matches third captured type *)
let typ3 : 'marker -> (_ * (_ * ('marker mtyp * _)), _ * (_ * ('marker * _))) func_arg = let typ3 : 'marker -> ('f, 'f, _ * (_ * ('marker mtyp * _)), _ * (_ * ('marker * _))) func_arg =
let pos3 (_, (_, (x, _))) = x in let pos3 (_, (_, (x, _))) = x in
fun marker -> mk_typ_nth pos3 pos3 marker fun marker -> mk_typ_nth pos3 pos3 marker
let capt_arg : (FuncArg.t -> 'f, 'f, _, _) func_arg =
let eat_func_arg _capt (f, args) =
match args with arg :: rest -> Some (f arg, rest) | _ -> None
in
{eat_func_arg; marker_static_checker= no_checker}
(* Function args end *) (* Function args end *)
(** Matches if there is no function arguments left *) (** Matches if there is no function arguments left *)
let no_args_left : (_, _) func_args_end = let no_args_left : (_, _, _) func_args_end =
let match_empty_args f = function Some [] -> Matches f | _ -> DoesNotMatch in let match_empty_args = function Some (f, []) -> Matches f | _ -> DoesNotMatch in
fun ~on_args args (f, capt) -> on_args capt args |> match_empty_args f fun ~on_args args (f, capt) -> on_args capt (f, args) |> match_empty_args
(** Matches any function arguments *) (** Matches any function arguments *)
let any_func_args : (_, _) func_args_end = let any_func_args : (_, _, _) func_args_end =
fun ~on_args args (f, capt) -> on_args capt args |> pre_map_opt ~f:(fun _ -> f) fun ~on_args args (f, capt) -> on_args capt (f, args) |> pre_map_opt ~f:fst
(** If [func_args_end1] does not match, use [func_args_end2] *) (** If [func_args_end1] does not match, use [func_args_end2] *)
let alternative_args_end let alternative_args_end
: ('f, 'captured_types) func_args_end -> ('f, 'captured_types) func_args_end : ('f_in, 'f_out, 'captured_types) func_args_end
-> ('f, 'captured_types) func_args_end = -> ('f_in, 'f_out, 'captured_types) func_args_end
-> ('f_in, 'f_out, 'captured_types) func_args_end =
fun func_args_end1 func_args_end2 ~on_args args f_capt -> fun func_args_end1 func_args_end2 ~on_args args f_capt ->
match func_args_end1 ~on_args args f_capt with match func_args_end1 ~on_args args f_capt with
| DoesNotMatch -> | DoesNotMatch ->
@ -450,11 +457,11 @@ let alternative_args_end
(** Retries matching with another matcher *) (** Retries matching with another matcher *)
let args_end_retry : _ -> (_, _) func_args_end = fun f ~on_args:_ _args _f_capt -> RetryWith f let args_end_retry : _ -> (_, _, _) func_args_end = fun f ~on_args:_ _args _f_capt -> RetryWith f
(** Retries matching with another matcher if the function does not have the (** Retries matching with another matcher if the function does not have the
exact number/types of args *) exact number/types of args *)
let exact_args_or_retry : 'f -> (_, _) func_args_end = let exact_args_or_retry : 'f -> (_, _, _) func_args_end =
fun f -> alternative_args_end no_args_left (args_end_retry f) fun f -> alternative_args_end no_args_left (args_end_retry f)

45
infer/src/IR/ProcnameDispatcher.mli
Unescape View File

@ -46,9 +46,9 @@ type ( 'f_in
type ('f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, 'list_constraint) templ_matcher type ('f_in, 'f_out, 'captured_types, 'markers_in, 'markers_out, 'list_constraint) templ_matcher
type ('f_in, 'f_out, 'captured_types, 'markers) args_matcher type ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher
type ('captured_types, 'markers) func_arg type ('f_in, 'f_out, 'captured_types, 'markers) func_arg
type 'f matcher = Typ.Procname.t -> FuncArg.t list -> 'f option type 'f matcher = Typ.Procname.t -> FuncArg.t list -> 'f option
@ -99,16 +99,19 @@ val capt_all :
(* Function args *) (* Function args *)
val any_arg : (_, _) func_arg val any_arg : ('f, 'f, _, _) func_arg
(** Eats one arg *) (** Eats one arg *)
val typ1 : 'marker -> ('marker mtyp * _, 'marker * _) func_arg val capt_arg : (FuncArg.t -> 'f, 'f, _, _) func_arg
(** Captures one arg *)
val typ1 : 'marker -> ('f, 'f, 'marker mtyp * _, 'marker * _) func_arg
(** Matches first captured type *) (** Matches first captured type *)
val typ2 : 'marker -> (_ * ('marker mtyp * _), _ * ('marker * _)) func_arg val typ2 : 'marker -> ('f, 'f, _ * ('marker mtyp * _), _ * ('marker * _)) func_arg
(** Matches second captured type *) (** Matches second captured type *)
val typ3 : 'marker -> (_ * (_ * ('marker mtyp * _)), _ * (_ * ('marker * _))) func_arg val typ3 : 'marker -> ('f, 'f, _ * (_ * ('marker mtyp * _)), _ * (_ * ('marker * _))) func_arg
(** Matches third captured type *) (** Matches third captured type *)
(* A matcher is a rule associating a function [f] to a [C/C++ function/method]: (* A matcher is a rule associating a function [f] to a [C/C++ function/method]:
@ -161,17 +164,18 @@ val ( >:: ) :
(** Ends template arguments and starts a name *) (** Ends template arguments and starts a name *)
val ( $+ ) : val ( $+ ) :
('f_in, 'f_out, 'captured_types, 'markers) args_matcher -> ('captured_types, 'markers) func_arg ('f_in, 'f_proc_out, 'f_interm, 'captured_types, 'markers) args_matcher
-> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher -> ('f_interm, 'f_out, 'captured_types, 'markers) func_arg
-> ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher
(** Separate function arguments *) (** Separate function arguments *)
val ( >$ ) : val ( >$ ) :
('f_in, 'f_out, 'captured_types, unit, 'markers, _) templ_matcher ('f_in, 'f_proc_out, 'ct, unit, 'cm, _) templ_matcher -> ('f_proc_out, 'f_out, 'ct, 'cm) func_arg
-> ('captured_types, 'markers) func_arg -> ('f_in, 'f_proc_out, 'f_out, 'ct, 'cm) args_matcher
-> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher
(** Ends template arguments and starts function arguments *) (** Ends template arguments and starts function arguments *)
val ( $--> ) : ('f_in, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in -> 'f_out matcher val ( $--> ) :
('f_in, _, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in -> 'f_out matcher
(** Ends function arguments, binds the function *) (** Ends function arguments, binds the function *)
val ( &+...>:: ) : val ( &+...>:: ) :
@ -190,15 +194,15 @@ val ( <>:: ) :
(** Separates names (accepts NO template arguments on the left one) *) (** Separates names (accepts NO template arguments on the left one) *)
val ( $ ) : val ( $ ) :
('f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher ('f_in, 'f_proc_out, 'captured_types, unit, 'markers) name_matcher
-> ('captured_types, 'markers) func_arg -> ('f_proc_out, 'f_out, 'captured_types, 'markers) func_arg
-> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher -> ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher
(** Ends a name with accept-ALL template arguments and starts function arguments *) (** Ends a name with accept-ALL template arguments and starts function arguments *)
val ( <>$ ) : val ( <>$ ) :
('f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher ('f_in, 'f_proc_out, 'captured_types, unit, 'markers) name_matcher
-> ('captured_types, 'markers) func_arg -> ('f_proc_out, 'f_out, 'captured_types, 'markers) func_arg
-> ('f_in, 'f_out, 'captured_types, 'markers) args_matcher -> ('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher
(** Ends a name with accept-NO template arguments and starts function arguments *) (** Ends a name with accept-NO template arguments and starts function arguments *)
val ( >--> ) : val ( >--> ) :
@ -206,7 +210,7 @@ val ( >--> ) :
(** Ends template arguments, accepts ALL function arguments, binds the function *) (** Ends template arguments, accepts ALL function arguments, binds the function *)
val ( $+...$--> ) : val ( $+...$--> ) :
('f_in, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in -> 'f_out matcher ('f_in, _, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in -> 'f_out matcher
(** Ends function arguments with eats-ALL and binds the function *) (** Ends function arguments with eats-ALL and binds the function *)
val ( >$$--> ) : val ( >$$--> ) :
@ -229,7 +233,8 @@ val ( <>--> ) :
('f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in -> 'f_out matcher ('f_in, 'f_out, 'captured_types, unit, 'markers) name_matcher -> 'f_in -> 'f_out matcher
(** After a name, accepts NO template arguments, accepts ALL function arguments, binds the function *) (** After a name, accepts NO template arguments, accepts ALL function arguments, binds the function *)
val ( $!--> ) : ('f_in, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in -> 'f_out matcher val ( $!--> ) :
('f_in, 'f_proc_out, 'f_out, 'captured_types, 'markers) args_matcher -> 'f_in -> 'f_out matcher
(** Ends function arguments, accepts NO more function arguments. (** Ends function arguments, accepts NO more function arguments.
If the args do not match, raise an internal error. If the args do not match, raise an internal error.
*) *)

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

@ -266,7 +266,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Call (ret, Const Cfun callee_pname, params, location, _) -> ( | Call (ret, Const Cfun callee_pname, params, location, _) -> (
match Models.dispatcher callee_pname params with match Models.dispatcher callee_pname params with
| Some model -> | Some model ->
model callee_pname ret params node location mem model callee_pname ret node location mem
| None -> | None ->
match Summary.read_summary pdesc callee_pname with match Summary.read_summary pdesc callee_pname with
| Some summary -> | Some summary ->
@ -276,7 +276,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
L.(debug BufferOverrun Verbose) L.(debug BufferOverrun Verbose)
"/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp
location ; location ;
Models.model_by_value Dom.Val.unknown callee_pname ret params node location mem Models.model_by_value Dom.Val.unknown callee_pname ret node location mem
|> Dom.Mem.add_heap Loc.unknown Dom.Val.unknown ) |> Dom.Mem.add_heap Loc.unknown Dom.Val.unknown )
| 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] *)

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

@ -19,8 +19,8 @@ module Make (CFG : ProcCfg.S) = struct
module Sem = BufferOverrunSemantics.Make (CFG) module Sem = BufferOverrunSemantics.Make (CFG)
type model_fun = type model_fun =
Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node -> Location.t Typ.Procname.t -> (Ident.t * Typ.t) option -> CFG.node -> Location.t -> Dom.Mem.astate
-> Dom.Mem.astate -> Dom.Mem.astate -> Dom.Mem.astate
let set_uninitialized node (typ: Typ.t) ploc mem = let set_uninitialized node (typ: Typ.t) ploc mem =
match typ.desc with match typ.desc with
@ -44,10 +44,10 @@ module Make (CFG : ProcCfg.S) = struct
(Typ.mk (Typ.Tint Typ.IChar), Some 1, x) (Typ.mk (Typ.Tint Typ.IChar), Some 1, x)
let model_malloc pname ret params node location mem = let model_malloc (size_exp, _) pname ret node location mem =
match ret with match ret with
| Some (id, _) -> | Some (id, _) ->
let typ, stride, length0 = get_malloc_info (List.hd_exn params |> fst) in let typ, stride, length0 = get_malloc_info size_exp in
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 =
@ -62,13 +62,13 @@ module Make (CFG : ProcCfg.S) = struct
mem mem
let model_realloc pname ret params node location mem = let model_realloc size_arg pname ret node location mem =
model_malloc pname ret (List.tl_exn params) node location mem model_malloc size_arg pname ret node location mem
let model_min _pname ret params _node _location mem = let model_min (e1, _) (e2, _) _pname ret _node _location mem =
match (ret, params) with match ret with
| Some (id, _), [(e1, _); (e2, _)] -> | Some (id, _) ->
let i1 = Sem.eval e1 mem |> Dom.Val.get_itv in let i1 = Sem.eval e1 mem |> Dom.Val.get_itv in
let i2 = Sem.eval e2 mem |> Dom.Val.get_itv in let i2 = Sem.eval e2 mem |> Dom.Val.get_itv in
let v = Itv.min_sem i1 i2 |> Dom.Val.of_itv in let v = Itv.min_sem i1 i2 |> Dom.Val.of_itv in
@ -77,19 +77,15 @@ module Make (CFG : ProcCfg.S) = struct
mem mem
let model_set_size _pname _ret params _node _location mem = let model_set_size (e1, _) (e2, _) _pname _ret _node _location mem =
match params with let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in
| [(e1, _); (e2, _)] -> let size = Sem.eval e2 mem |> Dom.Val.get_itv in
let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in let arr = Dom.Mem.find_heap_set locs mem in
let size = Sem.eval e2 mem |> Dom.Val.get_itv in let arr = Dom.Val.set_array_size size arr in
let arr = Dom.Mem.find_heap_set locs mem in Dom.Mem.strong_update_heap locs arr mem
let arr = Dom.Val.set_array_size size arr in
Dom.Mem.strong_update_heap locs arr mem
| _ ->
mem
let model_by_value value _pname ret _params _node _location mem = let model_by_value value _pname ret _node _location mem =
match ret with match ret with
| Some (id, _) -> | Some (id, _) ->
Dom.Mem.add_stack (Loc.of_id id) value mem Dom.Mem.add_stack (Loc.of_id id) value mem
@ -99,45 +95,39 @@ module Make (CFG : ProcCfg.S) = struct
mem mem
let model_bottom _pname _ret _params _node _location _mem = Bottom let model_bottom _pname _ret _node _location _mem = Bottom
let model_infer_print _pname _ret params _node location mem = let model_infer_print (e, _) _pname _ret _node location mem =
match params with L.(debug BufferOverrun Medium)
| (e, _) :: _ -> "@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ;
L.(debug BufferOverrun Medium) mem
"@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ;
mem
| _ ->
mem
let model_infer_set_array_length pname _ret params node _location mem = let model_infer_set_array_length array (length_exp, _) pname _ret node _location mem =
match params with match array with
| [(Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray (typ, _, stride0)}); (length_exp, _)] -> | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray (typ, _, stride0)} ->
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 stride0 in let stride = Option.map ~f:IntLit.to_int stride0 in
let v = Sem.eval_array_alloc pname node typ ?stride Itv.zero length 0 1 in let v = Sem.eval_array_alloc pname node typ ?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 typ (Dom.Val.get_array_locs v) |> set_uninitialized node typ (Dom.Val.get_array_locs v)
| [_; _] ->
L.(die InternalError) "Unexpected type of arguments for __set_array_length()"
| _ -> | _ ->
L.(die InternalError) "Unexpected number of arguments for __set_array_length()" L.(die InternalError) "Unexpected type of first argument for __set_array_length()"
let dispatcher : model_fun ProcnameDispatcher.dispatcher = let dispatcher : model_fun ProcnameDispatcher.dispatcher =
let open ProcnameDispatcher in let open ProcnameDispatcher in
make_dispatcher make_dispatcher
[ -"__inferbo_min" <>$ any_arg $+ any_arg $!--> model_min [ -"__inferbo_min" <>$ capt_arg $+ capt_arg $!--> model_min
; -"__inferbo_set_size" <>$ any_arg $+ any_arg $!--> model_set_size ; -"__inferbo_set_size" <>$ capt_arg $+ capt_arg $!--> model_set_size
; -"__exit" <>--> model_bottom ; -"__exit" <>--> model_bottom
; -"exit" <>--> model_bottom ; -"exit" <>--> model_bottom
; -"fgetc" <>--> model_by_value Dom.Val.Itv.m1_255 ; -"fgetc" <>--> model_by_value Dom.Val.Itv.m1_255
; -"infer_print" <>--> model_infer_print ; -"infer_print" <>$ capt_arg $!--> model_infer_print
; -"malloc" <>--> model_malloc ; -"malloc" <>$ capt_arg $+...$--> model_malloc
; -"__new_array" <>--> model_malloc ; -"__new_array" <>$ capt_arg $+...$--> model_malloc
; -"realloc" <>--> model_realloc ; -"realloc" <>$ any_arg $+ capt_arg $+...$--> model_realloc
; -"__set_array_length" <>$ any_arg $+ any_arg $!--> model_infer_set_array_length ; -"__set_array_length" <>$ capt_arg $+ capt_arg $!--> model_infer_set_array_length
; -"strlen" <>--> model_by_value Dom.Val.Itv.nat ] ; -"strlen" <>--> model_by_value Dom.Val.Itv.nat ]
end end

Write Preview
Loading…
Cancel
Save