From a4eac6c2d630e6406ad808605a0616b389a9472c Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 26 Mar 2018 05:51:37 -0700 Subject: [PATCH] [Inferbo] Refactoring 7/8: remove dependency on CFG Reviewed By: jvillard Differential Revision: D7397133 fbshipit-source-id: e036c04 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 13 +- .../src/bufferoverrun/bufferOverrunModels.ml | 575 +++++---- .../bufferoverrun/bufferOverrunSemantics.ml | 1088 ++++++++--------- infer/src/bufferoverrun/bufferOverrunUtils.ml | 320 +++-- .../src/bufferoverrun/bufferOverrunUtils.mli | 51 + 5 files changed, 1018 insertions(+), 1029 deletions(-) create mode 100644 infer/src/bufferoverrun/bufferOverrunUtils.mli diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 9c698cc67..d675c172c 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -13,8 +13,11 @@ open! IStd open AbsLoc open! AbstractDomain.Types -module L = Logging +module BoUtils = BufferOverrunUtils module Dom = BufferOverrunDomain +module L = Logging +module Models = BufferOverrunModels +module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace module TraceSet = Trace.Set @@ -31,9 +34,6 @@ end) module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG module Domain = Dom.Mem - module BoUtils = BufferOverrunUtils.Make (CFG) - module Sem = BoUtils.Sem - module Models = BufferOverrunModels.Make (BoUtils) type extras = Typ.Procname.t -> Procdesc.t option @@ -313,11 +313,6 @@ module CFG = Analyzer.TransferFunctions.CFG type invariant_map = Analyzer.invariant_map module Report = struct - (* I'd like to avoid rebuilding this :( - Everything depend on CFG only because of `get_allocsite` *) - module BoUtils = BufferOverrunUtils.Make (CFG) - module Sem = BoUtils.Sem - module Models = BufferOverrunModels.Make (BoUtils) module PO = BufferOverrunProofObligations type extras = Typ.Procname.t -> Procdesc.t option diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 5a7920236..4515a1d95 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -11,349 +11,344 @@ open! IStd open AbsLoc open! AbstractDomain.Types module L = Logging +module BoUtils = BufferOverrunUtils module Dom = BufferOverrunDomain module PO = BufferOverrunProofObligations +module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace module TraceSet = Trace.Set -module Make (BoUtils : BufferOverrunUtils.S) = struct - module CFG = BoUtils.CFG - module Sem = BoUtils.Sem +type model_env = + { pname: Typ.Procname.t + ; node_hash: int + ; location: Location.t + ; tenv: Tenv.t + ; ret: (Ident.t * Typ.t) option } - type model_env = - { pname: Typ.Procname.t - ; node_hash: int - ; location: Location.t - ; tenv: Tenv.t - ; ret: (Ident.t * Typ.t) option } +let mk_model_env pname node_hash location ?ret tenv = {pname; node_hash; 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 +type check_fun = model_env -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t - type check_fun = model_env -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t +type model = {exec: exec_fun; check: check_fun} - type model = {exec: exec_fun; check: check_fun} +type declare_local_fun = + decl_local:BoUtils.Exec.decl_local -> model_env -> Loc.t -> inst_num:int -> dimension:int + -> Dom.Mem.astate -> Dom.Mem.astate * int - type declare_local_fun = - decl_local:BoUtils.Exec.decl_local -> model_env -> Loc.t -> inst_num:int -> dimension:int - -> Dom.Mem.astate -> Dom.Mem.astate * int +type declare_symbolic_fun = + decl_sym_val:BoUtils.Exec.decl_sym_val -> model_env -> depth:int -> Loc.t -> inst_num:int + -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate - type declare_symbolic_fun = - decl_sym_val:BoUtils.Exec.decl_sym_val -> model_env -> depth:int -> Loc.t -> inst_num:int - -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate +type typ_model = {declare_local: declare_local_fun; declare_symbolic: declare_symbolic_fun} - type typ_model = {declare_local: declare_local_fun; declare_symbolic: declare_symbolic_fun} +let no_check _model_env _mem cond_set = cond_set - let no_check _model_env _mem cond_set = cond_set - - (* It returns a tuple of: +(* It returns a tuple of: - type of array element - stride of the type - array size - flexible array size *) - let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = function - | Exp.BinOp (Binop.Mult, Exp.Sizeof {typ; nbytes}, length) - | Exp.BinOp (Binop.Mult, length, Exp.Sizeof {typ; nbytes}) -> - (typ, nbytes, length, None) - | Exp.Sizeof {typ; nbytes; dynamic_length} -> - (typ, nbytes, Exp.one, dynamic_length) - | x -> - (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None) - - - let check_alloc_size size_exp {pname; location} mem cond_set = - let _, _, length0, _ = get_malloc_info size_exp in - let v_length = Sem.eval length0 mem in - match Dom.Val.get_itv v_length with - | Bottom -> - cond_set - | NonBottom length -> - let traces = Dom.Val.get_traces v_length in - PO.ConditionSet.add_alloc_size pname location ~length traces cond_set - - - let set_uninitialized location (typ: Typ.t) ploc mem = - match typ.desc with - | Tint _ | Tfloat _ -> - Dom.Mem.weak_update_heap ploc Dom.Val.Itv.top mem +let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = function + | Exp.BinOp (Binop.Mult, Exp.Sizeof {typ; nbytes}, length) + | Exp.BinOp (Binop.Mult, length, Exp.Sizeof {typ; nbytes}) -> + (typ, nbytes, length, None) + | Exp.Sizeof {typ; nbytes; dynamic_length} -> + (typ, nbytes, Exp.one, dynamic_length) + | x -> + (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None) + + +let check_alloc_size size_exp {pname; location} mem cond_set = + let _, _, length0, _ = get_malloc_info size_exp in + let v_length = Sem.eval length0 mem in + match Dom.Val.get_itv v_length with + | Bottom -> + cond_set + | NonBottom length -> + let traces = Dom.Val.get_traces v_length in + PO.ConditionSet.add_alloc_size pname location ~length traces cond_set + + +let set_uninitialized location (typ: Typ.t) ploc mem = + match typ.desc with + | Tint _ | Tfloat _ -> + Dom.Mem.weak_update_heap ploc Dom.Val.Itv.top mem + | _ -> + L.(debug BufferOverrun Verbose) + "/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp + location ; + mem + + +let malloc size_exp = + let exec {pname; ret; node_hash; location; tenv} mem = + match ret with + | Some (id, _) -> + let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in + let typ, stride, length0, dyn_length = get_malloc_info size_exp in + let length = Sem.eval length0 mem in + let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in + let v = + Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero + ~size:(Dom.Val.get_itv length) ~inst_num:0 ~dimension:1 + |> Dom.Val.set_traces traces + in + mem |> Dom.Mem.add_stack (Loc.of_id id) v + |> set_uninitialized location 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 | _ -> L.(debug BufferOverrun Verbose) - "/!\\ Do not know how to uninitialize type %a at %a@\n" (Typ.pp Pp.text) typ Location.pp - location ; + "/!\\ Do not know where to model malloc at %a@\n" Location.pp location ; mem + and check = check_alloc_size size_exp in + {exec; check} - let malloc size_exp = - let exec {pname; ret; node_hash; location; tenv} mem = - match ret with - | Some (id, _) -> - let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in - let typ, stride, length0, dyn_length = get_malloc_info size_exp in - let length = Sem.eval length0 mem in - let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in - let v = - Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero - ~size:(Dom.Val.get_itv length) ~inst_num:0 ~dimension:1 - |> Dom.Val.set_traces traces - in - mem |> Dom.Mem.add_stack (Loc.of_id id) v - |> set_uninitialized location 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 - | _ -> - L.(debug BufferOverrun Verbose) - "/!\\ Do not know where to model malloc at %a@\n" Location.pp location ; - mem - and check = check_alloc_size size_exp in - {exec; check} - - - let realloc src_exp size_exp = - let exec {ret; location; tenv} mem = - match ret with - | Some (id, _) -> - let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in - let typ, _, length0, dyn_length = get_malloc_info size_exp in - let length = Sem.eval length0 mem in - let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in - let v = - Sem.eval src_exp mem |> Dom.Val.set_array_size (Dom.Val.get_itv length) - |> Dom.Val.set_traces traces - in - let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in - Option.value_map dyn_length ~default:mem ~f:(fun dyn_length -> - let dyn_length = Dom.Val.get_itv (Sem.eval dyn_length mem) in - BoUtils.Exec.set_dyn_length tenv typ (Dom.Val.get_array_locs v) dyn_length mem ) - | _ -> - mem - and check = check_alloc_size size_exp in - {exec; check} - - - let placement_new allocated_mem_exp = - let exec {ret} mem = - match ret with - | Some (id, _) -> - let v = Sem.eval allocated_mem_exp mem in - Dom.Mem.add_stack (Loc.of_id id) v mem - | None -> - mem - in - {exec; check= no_check} - - - let inferbo_min e1 e2 = - let exec {ret} mem = - match ret with - | Some (id, _) -> - let i1 = Sem.eval e1 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 - mem |> Dom.Mem.add_stack (Loc.of_id id) v - | _ -> - mem - in - {exec; check= no_check} - - - let inferbo_set_size e1 e2 = - let exec _model_env mem = - let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in - let size = Sem.eval e2 mem |> Dom.Val.get_itv in - let arr = Dom.Mem.find_heap_set locs mem in - let arr = Dom.Val.set_array_size size arr in - Dom.Mem.strong_update_heap locs arr mem - and check = check_alloc_size e2 in - {exec; check} +let realloc src_exp size_exp = + let exec {ret; location; tenv} mem = + match ret with + | Some (id, _) -> + let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in + let typ, _, length0, dyn_length = get_malloc_info size_exp in + let length = Sem.eval length0 mem in + let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in + let v = + Sem.eval src_exp mem |> Dom.Val.set_array_size (Dom.Val.get_itv length) + |> Dom.Val.set_traces traces + in + let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in + Option.value_map dyn_length ~default:mem ~f:(fun dyn_length -> + let dyn_length = Dom.Val.get_itv (Sem.eval dyn_length mem) in + BoUtils.Exec.set_dyn_length tenv typ (Dom.Val.get_array_locs v) dyn_length mem ) + | _ -> + mem + and check = check_alloc_size size_exp in + {exec; check} - let model_by_value value ret mem = +let placement_new allocated_mem_exp = + let exec {ret} mem = match ret with | Some (id, _) -> - Dom.Mem.add_stack (Loc.of_id id) value mem + let v = Sem.eval allocated_mem_exp mem in + Dom.Mem.add_stack (Loc.of_id id) v mem | None -> - L.(debug BufferOverrun Verbose) - "/!\\ Do not know where to model value %a@\n" Dom.Val.pp value ; mem + in + {exec; check= no_check} - let by_value value = - let exec {ret} mem = model_by_value value ret mem in - {exec; check= no_check} - +let inferbo_min e1 e2 = + let exec {ret} mem = + match ret with + | Some (id, _) -> + let i1 = Sem.eval e1 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 + mem |> Dom.Mem.add_stack (Loc.of_id id) v + | _ -> + mem + in + {exec; check= no_check} + + +let inferbo_set_size e1 e2 = + let exec _model_env mem = + let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in + let size = Sem.eval e2 mem |> Dom.Val.get_itv in + let arr = Dom.Mem.find_heap_set locs mem in + let arr = Dom.Val.set_array_size size arr in + Dom.Mem.strong_update_heap locs arr mem + and check = check_alloc_size e2 in + {exec; check} + + +let model_by_value value ret mem = + match ret with + | Some (id, _) -> + Dom.Mem.add_stack (Loc.of_id id) value mem + | None -> + L.(debug BufferOverrun Verbose) + "/!\\ Do not know where to model value %a@\n" Dom.Val.pp value ; + mem - let bottom = - let exec _model_env _mem = Bottom in - {exec; check= no_check} +let by_value = + let exec ~value {ret} mem = model_by_value value ret mem in + fun value -> {exec= exec ~value; check= no_check} - let infer_print e = - let exec {location} mem = - L.(debug BufferOverrun Medium) - "@[=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ; - mem - in - {exec; check= no_check} +let bottom = + let exec _model_env _mem = Bottom in + {exec; check= no_check} - let set_array_length array length_exp = - let exec {pname; node_hash; location} mem = - match array with - | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} -> - let length = Sem.eval length_exp mem |> Dom.Val.get_itv in - let stride = Option.map ~f:IntLit.to_int stride in - let v = - Sem.eval_array_alloc pname ~node_hash elt ~stride ~offset:Itv.zero ~size:length - ~inst_num:0 ~dimension:1 - in - mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v - |> set_uninitialized location elt (Dom.Val.get_array_locs v) - | _ -> - L.(die InternalError) "Unexpected type of first argument for __set_array_length()" - and check = check_alloc_size length_exp in - {exec; check} +let infer_print e = + let exec {location} mem = + L.(debug BufferOverrun Medium) + "@[=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp (Sem.eval e mem) ; + mem + in + {exec; check= no_check} - module Split = struct - let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem = - let traces = BufferOverrunTrace.(Call location |> singleton |> Set.singleton) in - let increment_itv = if adds_at_least_one then Itv.pos else Itv.nat in - let increment = Dom.Val.of_itv ~traces increment_itv in - let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in - let size_field = Typ.Fieldname.Clang.from_class_name vector_type_name "infer_size" in - let vector_size_locs = - Sem.eval vector_exp mem |> Dom.Val.get_all_locs |> PowLoc.append_field ~fn:size_field - in - Dom.Mem.transform_mem ~f:(Dom.Val.plus increment) vector_size_locs mem - end - module Boost = struct - module Split = struct - let std_vector vector_arg = - let exec {location} mem = - Split.std_vector ~adds_at_least_one:true vector_arg location mem +let set_array_length array length_exp = + let exec {pname; node_hash; location} mem = + match array with + | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} -> + let length = Sem.eval length_exp mem |> Dom.Val.get_itv in + let stride = Option.map ~f:IntLit.to_int stride in + let v = + Sem.eval_array_alloc pname ~node_hash elt ~stride ~offset:Itv.zero ~size:length + ~inst_num:0 ~dimension:1 in - {exec; check= no_check} - end + mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v + |> set_uninitialized location elt (Dom.Val.get_array_locs v) + | _ -> + L.(die InternalError) "Unexpected type of first argument for __set_array_length()" + and check = check_alloc_size length_exp in + {exec; check} + + +module Split = struct + let std_vector ~adds_at_least_one (vector_exp, vector_typ) location mem = + let traces = BufferOverrunTrace.(Call location |> singleton |> Set.singleton) in + let increment_itv = if adds_at_least_one then Itv.pos else Itv.nat in + let increment = Dom.Val.of_itv ~traces increment_itv in + let vector_type_name = Option.value_exn (vector_typ |> Typ.strip_ptr |> Typ.name) in + let size_field = Typ.Fieldname.Clang.from_class_name vector_type_name "infer_size" in + let vector_size_locs = + Sem.eval vector_exp mem |> Dom.Val.get_all_locs |> PowLoc.append_field ~fn:size_field + in + Dom.Mem.transform_mem ~f:(Dom.Val.plus increment) vector_size_locs mem +end + +module Boost = struct + module Split = struct + let std_vector vector_arg = + let exec {location} mem = Split.std_vector ~adds_at_least_one:true vector_arg location mem in + {exec; check= no_check} end +end - module Folly = struct - module Split = struct - let std_vector vector_arg ignore_empty_opt = - let exec {location} mem = - let adds_at_least_one = - match ignore_empty_opt with - | Some ignore_empty_exp -> - Sem.eval ignore_empty_exp mem |> Dom.Val.get_itv |> Itv.is_false - | None -> - (* default: ignore_empty is false *) - true - in - Split.std_vector ~adds_at_least_one vector_arg location mem +module Folly = struct + module Split = struct + let std_vector vector_arg ignore_empty_opt = + let exec {location} mem = + let adds_at_least_one = + match ignore_empty_opt with + | Some ignore_empty_exp -> + Sem.eval ignore_empty_exp mem |> Dom.Val.get_itv |> Itv.is_false + | None -> + (* default: ignore_empty is false *) + true in - {exec; check= no_check} - end + Split.std_vector ~adds_at_least_one vector_arg location mem + in + {exec; check= no_check} end +end - module StdArray = struct - let typ typ length = - let declare_local ~decl_local {pname; node_hash; location} loc ~inst_num ~dimension mem = - (* should this be deferred to the constructor? *) - let length = Some (IntLit.of_int64 length) in - BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length - ~inst_num ~dimension mem - in - let declare_symbolic ~decl_sym_val {pname; tenv; node_hash; location} ~depth loc ~inst_num - ~new_sym_num ~new_alloc_num mem = - let offset = Itv.zero in - let size = Itv.of_int64 length in - BoUtils.Exec.decl_sym_arr ~decl_sym_val pname tenv ~node_hash location ~depth loc typ - ~offset ~size ~inst_num ~new_sym_num ~new_alloc_num mem - in - {declare_local; declare_symbolic} +module StdArray = struct + let typ typ length = + let declare_local ~decl_local {pname; node_hash; location} loc ~inst_num ~dimension mem = + (* should this be deferred to the constructor? *) + let length = Some (IntLit.of_int64 length) in + BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num + ~dimension mem + in + let declare_symbolic ~decl_sym_val {pname; tenv; node_hash; location} ~depth loc ~inst_num + ~new_sym_num ~new_alloc_num mem = + let offset = Itv.zero in + let size = Itv.of_int64 length in + BoUtils.Exec.decl_sym_arr ~decl_sym_val pname tenv ~node_hash location ~depth loc typ ~offset + ~size ~inst_num ~new_sym_num ~new_alloc_num mem + in + {declare_local; declare_symbolic} - let constructor _size = - let exec _model_env mem = mem (* initialize? *) in - {exec; check= no_check} + let constructor _size = + let exec _model_env mem = mem (* initialize? *) in + {exec; check= no_check} - let at _size (array_exp, _) (index_exp, _) = - (* TODO? use size *) - let exec {ret} mem = - L.(debug BufferOverrun Verbose) "Using model std::array<_, %Ld>::at" _size ; - match ret with - | Some (id, _) -> - BoUtils.Exec.load_val id (Sem.eval_lindex array_exp index_exp mem) mem - | None -> - mem - and check {pname; location} mem cond_set = - BoUtils.Check.lindex ~array_exp ~index_exp mem pname location cond_set - in - {exec; check} + let at _size (array_exp, _) (index_exp, _) = + (* TODO? use size *) + let exec {ret} mem = + L.(debug BufferOverrun Verbose) "Using model std::array<_, %Ld>::at" _size ; + match ret with + | Some (id, _) -> + BoUtils.Exec.load_val id (Sem.eval_lindex array_exp index_exp mem) mem + | None -> + mem + and check {pname; location} mem cond_set = + BoUtils.Check.lindex ~array_exp ~index_exp mem pname location cond_set + in + {exec; check} - let no_model = - let exec {pname; location} mem = - L.(debug BufferOverrun Verbose) - "No model for %a at %a" Typ.Procname.pp pname Location.pp location ; - mem - in - {exec; check= no_check} + let no_model = + let exec {pname; location} mem = + L.(debug BufferOverrun Verbose) + "No model for %a at %a" Typ.Procname.pp pname Location.pp location ; + mem + in + {exec; check= no_check} - let no_typ_model = - let no_model kind pname location mem = - L.(debug BufferOverrun Verbose) - "No %s type model in %a at %a" kind Typ.Procname.pp pname Location.pp location ; - mem - in - let declare_local ~decl_local:_ {pname; location} _loc ~inst_num ~dimension:_ mem = - (no_model "local" pname location mem, inst_num) - in - let declare_symbolic ~decl_sym_val:_ {pname; location} ~depth:_ _loc ~inst_num:_ - ~new_sym_num:_ ~new_alloc_num:_ mem = - no_model "symbolic" pname location mem - in - {declare_local; declare_symbolic} - end + let no_typ_model = + let no_model kind pname location mem = + L.(debug BufferOverrun Verbose) + "No %s type model in %a at %a" kind Typ.Procname.pp pname Location.pp location ; + mem + in + let declare_local ~decl_local:_ {pname; location} _loc ~inst_num ~dimension:_ mem = + (no_model "local" pname location mem, inst_num) + in + let declare_symbolic ~decl_sym_val:_ {pname; location} ~depth:_ _loc ~inst_num:_ ~new_sym_num:_ + ~new_alloc_num:_ mem = + no_model "symbolic" pname location mem + in + {declare_local; declare_symbolic} +end - module Call = struct - let dispatch : model ProcnameDispatcher.Call.dispatcher = - let open ProcnameDispatcher.Call in - let mk_std_array () = -"std" &:: "array" < any_typ &+ capt_int in - let std_array0 = mk_std_array () in - let std_array2 = mk_std_array () in - make_dispatcher - [ -"__inferbo_min" <>$ capt_exp $+ capt_exp $!--> inferbo_min - ; -"__inferbo_set_size" <>$ capt_exp $+ capt_exp $!--> inferbo_set_size - ; -"__exit" <>--> bottom - ; -"exit" <>--> bottom - ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255 - ; -"infer_print" <>$ capt_exp $!--> infer_print - ; -"malloc" <>$ capt_exp $+...$--> malloc - ; -"__new" <>$ capt_exp $+...$--> malloc - ; -"__new_array" <>$ capt_exp $+...$--> malloc - ; -"__placement_new" <>$ any_arg $+ capt_exp $!--> placement_new - ; -"realloc" <>$ capt_exp $+ capt_exp $+...$--> realloc - ; -"__set_array_length" <>$ capt_arg $+ capt_exp $!--> set_array_length - ; -"strlen" <>--> by_value Dom.Val.Itv.nat - ; -"boost" &:: "split" $ capt_arg_of_typ (-"std" &:: "vector") $+ any_arg $+ any_arg - $+? any_arg $--> Boost.Split.std_vector - ; -"folly" &:: "split" $ any_arg $+ any_arg $+ capt_arg_of_typ (-"std" &:: "vector") - $+? capt_exp $--> Folly.Split.std_vector - ; std_array0 >:: "array" &--> StdArray.constructor - ; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at - ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at - ; -"std" &:: "array" &::.*--> StdArray.no_model ] - end +module Call = struct + let dispatch : model ProcnameDispatcher.Call.dispatcher = + let open ProcnameDispatcher.Call in + let mk_std_array () = -"std" &:: "array" < any_typ &+ capt_int in + let std_array0 = mk_std_array () in + let std_array2 = mk_std_array () in + make_dispatcher + [ -"__inferbo_min" <>$ capt_exp $+ capt_exp $!--> inferbo_min + ; -"__inferbo_set_size" <>$ capt_exp $+ capt_exp $!--> inferbo_set_size + ; -"__exit" <>--> bottom + ; -"exit" <>--> bottom + ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255 + ; -"infer_print" <>$ capt_exp $!--> infer_print + ; -"malloc" <>$ capt_exp $+...$--> malloc + ; -"__new" <>$ capt_exp $+...$--> malloc + ; -"__new_array" <>$ capt_exp $+...$--> malloc + ; -"__placement_new" <>$ any_arg $+ capt_exp $!--> placement_new + ; -"realloc" <>$ capt_exp $+ capt_exp $+...$--> realloc + ; -"__set_array_length" <>$ capt_arg $+ capt_exp $!--> set_array_length + ; -"strlen" <>--> by_value Dom.Val.Itv.nat + ; -"boost" &:: "split" $ capt_arg_of_typ (-"std" &:: "vector") $+ any_arg $+ any_arg + $+? any_arg $--> Boost.Split.std_vector + ; -"folly" &:: "split" $ any_arg $+ any_arg $+ capt_arg_of_typ (-"std" &:: "vector") + $+? capt_exp $--> Folly.Split.std_vector + ; std_array0 >:: "array" &--> StdArray.constructor + ; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at + ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at + ; -"std" &:: "array" &::.*--> StdArray.no_model ] +end - module TypName = struct - let dispatch : typ_model ProcnameDispatcher.TypName.dispatcher = - let open ProcnameDispatcher.TypName in - make_dispatcher - [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> StdArray.typ - ; -"std" &:: "array" &::.*--> StdArray.no_typ_model ] - end +module TypName = struct + let dispatch : typ_model ProcnameDispatcher.TypName.dispatcher = + let open ProcnameDispatcher.TypName in + make_dispatcher + [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> StdArray.typ + ; -"std" &:: "array" &::.*--> StdArray.no_typ_model ] end diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index cba14f6f0..8b224ac83 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -19,566 +19,562 @@ module Trace = BufferOverrunTrace module TraceSet = Trace.Set open BufferOverrunDomain -module Make (CFG : ProcCfg.S) = struct - exception Not_implemented - - let eval_const : Const.t -> Val.t = function - | Const.Cint intlit -> ( - try Val.of_int (IntLit.to_int intlit) with _ -> Val.Itv.top ) - | Const.Cfloat f -> - f |> int_of_float |> Val.of_int - | _ -> - Val.Itv.top - - - (* TODO *) - - let sizeof_ikind : Typ.ikind -> int = function - | Typ.IChar | Typ.ISChar | Typ.IUChar | Typ.IBool -> - 1 - | Typ.IInt | Typ.IUInt -> - 4 - | Typ.IShort | Typ.IUShort -> - 2 - | Typ.ILong | Typ.IULong -> - 4 - | Typ.ILongLong | Typ.IULongLong -> - 8 - | Typ.I128 | Typ.IU128 -> - 16 - - - let sizeof_fkind : Typ.fkind -> int = function - | Typ.FFloat -> - 4 - | Typ.FDouble | Typ.FLongDouble -> - 8 - - - (* NOTE: assume 32bit machine *) - let rec sizeof (typ: Typ.t) : int = - match typ.desc with - | Typ.Tint ikind -> - sizeof_ikind ikind - | Typ.Tfloat fkind -> - sizeof_fkind fkind - | Typ.Tvoid -> - 1 - | Typ.Tptr (_, _) -> - 4 - | Typ.Tstruct _ | Typ.TVar _ -> - 4 (* TODO *) - | Typ.Tarray {length= Some length; stride= Some stride} -> - IntLit.to_int stride * IntLit.to_int length - | Typ.Tarray {elt; length= Some length; stride= None} -> - sizeof elt * IntLit.to_int length - | _ -> - 4 - - - let rec must_alias : Exp.t -> Exp.t -> Mem.astate -> bool = - fun e1 e2 m -> - match (e1, e2) with - | Exp.Var x1, Exp.Var x2 -> ( - match (Mem.find_alias x1 m, Mem.find_alias x2 m) with - | Some x1', Some x2' -> - AliasTarget.equal x1' x2' - | _, _ -> - false ) - | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) -> - Unop.equal uop1 uop2 && must_alias e1' e2' m - | Exp.BinOp (bop1, e11, e12), Exp.BinOp (bop2, e21, e22) -> - Binop.equal bop1 bop2 && must_alias e11 e21 m && must_alias e12 e22 m - | Exp.Exn t1, Exp.Exn t2 -> - must_alias t1 t2 m - | Exp.Const c1, Exp.Const c2 -> - Const.equal c1 c2 - | Exp.Cast (t1, e1'), Exp.Cast (t2, e2') -> - Typ.equal t1 t2 && must_alias e1' e2' m - | Exp.Lvar x1, Exp.Lvar x2 -> - Pvar.equal x1 x2 - | Exp.Lfield (e1, fld1, _), Exp.Lfield (e2, fld2, _) -> - must_alias e1 e2 m && Typ.Fieldname.equal fld1 fld2 - | Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) -> - must_alias e11 e21 m && must_alias e12 e22 m - | Exp.Sizeof {nbytes= Some nbytes1}, Exp.Sizeof {nbytes= Some nbytes2} -> - Int.equal nbytes1 nbytes2 - | ( Exp.Sizeof {typ= t1; dynamic_length= dynlen1; subtype= subt1} - , Exp.Sizeof {typ= t2; dynamic_length= dynlen2; subtype= subt2} ) -> - Typ.equal t1 t2 && must_alias_opt dynlen1 dynlen2 m - && Int.equal (Subtype.compare subt1 subt2) 0 - | _, _ -> - false - - - and must_alias_opt : Exp.t option -> Exp.t option -> Mem.astate -> bool = - fun e1_opt e2_opt m -> - match (e1_opt, e2_opt) with - | Some e1, Some e2 -> - must_alias e1 e2 m - | None, None -> - true +let eval_const : Const.t -> Val.t = function + | Const.Cint intlit -> ( + try Val.of_int (IntLit.to_int intlit) with _ -> Val.Itv.top ) + | Const.Cfloat f -> + f |> int_of_float |> Val.of_int + | _ -> + Val.Itv.top + + +(* TODO *) + +let sizeof_ikind : Typ.ikind -> int = function + | Typ.IChar | Typ.ISChar | Typ.IUChar | Typ.IBool -> + 1 + | Typ.IInt | Typ.IUInt -> + 4 + | Typ.IShort | Typ.IUShort -> + 2 + | Typ.ILong | Typ.IULong -> + 4 + | Typ.ILongLong | Typ.IULongLong -> + 8 + | Typ.I128 | Typ.IU128 -> + 16 + + +let sizeof_fkind : Typ.fkind -> int = function + | Typ.FFloat -> + 4 + | Typ.FDouble | Typ.FLongDouble -> + 8 + + +(* NOTE: assume 32bit machine *) +let rec sizeof (typ: Typ.t) : int = + match typ.desc with + | Typ.Tint ikind -> + sizeof_ikind ikind + | Typ.Tfloat fkind -> + sizeof_fkind fkind + | Typ.Tvoid -> + 1 + | Typ.Tptr (_, _) -> + 4 + | Typ.Tstruct _ | Typ.TVar _ -> + 4 (* TODO *) + | Typ.Tarray {length= Some length; stride= Some stride} -> + IntLit.to_int stride * IntLit.to_int length + | Typ.Tarray {elt; length= Some length; stride= None} -> + sizeof elt * IntLit.to_int length + | _ -> + 4 + + +let rec must_alias : Exp.t -> Exp.t -> Mem.astate -> bool = + fun e1 e2 m -> + match (e1, e2) with + | Exp.Var x1, Exp.Var x2 -> ( + match (Mem.find_alias x1 m, Mem.find_alias x2 m) with + | Some x1', Some x2' -> + AliasTarget.equal x1' x2' | _, _ -> - false - - - let comp_rev : Binop.t -> Binop.t = function - | Binop.Lt -> - Binop.Gt - | Binop.Gt -> - Binop.Lt - | Binop.Le -> - Binop.Ge - | Binop.Ge -> - Binop.Le - | Binop.Eq -> - Binop.Eq - | Binop.Ne -> - Binop.Ne - | _ -> - assert false - - - let comp_not : Binop.t -> Binop.t = function - | Binop.Lt -> - Binop.Ge - | Binop.Gt -> - Binop.Le - | Binop.Le -> - Binop.Gt - | Binop.Ge -> - Binop.Lt - | Binop.Eq -> - Binop.Ne - | Binop.Ne -> - Binop.Eq - | _ -> - assert false - - - let rec must_alias_cmp : Exp.t -> Mem.astate -> bool = - fun e m -> - match e with - | Exp.BinOp (Binop.Lt, e1, e2) | Exp.BinOp (Binop.Gt, e1, e2) | Exp.BinOp (Binop.Ne, e1, e2) -> - must_alias e1 e2 m - | Exp.BinOp (Binop.LAnd, e1, e2) -> - must_alias_cmp e1 m || must_alias_cmp e2 m - | Exp.BinOp (Binop.LOr, e1, e2) -> - must_alias_cmp e1 m && must_alias_cmp e2 m - | Exp.UnOp (Unop.LNot, Exp.UnOp (Unop.LNot, e1, _), _) -> - must_alias_cmp e1 m - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Lt as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Gt as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Le as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ge as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Eq as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ne as c), e1, e2), _) -> - must_alias_cmp (Exp.BinOp (comp_not c, e1, e2)) m - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> - let e1' = Exp.UnOp (Unop.LNot, e1, t) in - let e2' = Exp.UnOp (Unop.LNot, e2, t) in - must_alias_cmp (Exp.BinOp (Binop.LAnd, e1', e2')) m - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LAnd, e1, e2), t) -> - let e1' = Exp.UnOp (Unop.LNot, e1, t) in - let e2' = Exp.UnOp (Unop.LNot, e2, t) in - must_alias_cmp (Exp.BinOp (Binop.LOr, e1', e2')) m - | _ -> - false - - - let rec eval : Exp.t -> Mem.astate -> Val.t = - fun exp mem -> - if must_alias_cmp exp mem then Val.of_int 0 - else - match exp with - | Exp.Var id -> - Mem.find_stack (Var.of_id id |> Loc.of_var) mem - | Exp.Lvar pvar -> - let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in - let arr = Mem.find_stack_set ploc mem in - ploc |> Val.of_pow_loc |> Val.join arr - | Exp.UnOp (uop, e, _) -> - eval_unop uop e mem - | Exp.BinOp (bop, e1, e2) -> - eval_binop bop e1 e2 mem - | Exp.Const c -> - eval_const c - | Exp.Cast (_, e) -> - eval e mem - | Exp.Lfield (e, fn, _) -> - eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc - | Exp.Lindex (e1, e2) -> - eval_lindex e1 e2 mem - | Exp.Sizeof {nbytes= Some size} -> - Val.of_int size - | Exp.Sizeof {typ; nbytes= None} -> - Val.of_int (sizeof typ) - | Exp.Exn _ | Exp.Closure _ -> - Val.Itv.top - - - (* NOTE: multidimensional array is not supported yet *) - and eval_lindex array_exp index_exp mem = - let array_v, index_v = (eval array_exp mem, eval index_exp mem) in - let arr = Val.plus_pi array_v index_v in - if ArrayBlk.is_bot (Val.get_array_blk arr) then - match array_exp with - | Exp.Lfield _ when not (PowLoc.is_bot (Val.get_pow_loc array_v)) -> - (* It handles the case accessing an array field of struct, - e.g., x.f[n] . Since our abstract domain distinguishes - memory sections for each array fields in struct, it finds - the memory section using the abstract memory, though the - memory lookup is not required to evaluate the address of - x.f[n] in the concrete semantics. *) - Val.plus_pi (Mem.find_set (Val.get_pow_loc array_v) mem) index_v - | _ -> - Val.of_pow_loc PowLoc.unknown - else arr - - - and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t = - fun unop e mem -> - let v = eval e mem in - match unop with - | Unop.Neg -> - Val.neg v - | Unop.BNot -> - Val.unknown_bit v - | Unop.LNot -> - Val.lnot v - - - and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t = - fun binop e1 e2 mem -> - let v1 = eval e1 mem in - let v2 = eval e2 mem in - match binop with - | Binop.PlusA -> - Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2) - | Binop.PlusPI -> - Val.plus_pi v1 v2 - | Binop.MinusA -> - Val.joins [Val.minus v1 v2; Val.minus_pi v1 v2; Val.minus_pp v1 v2] - | Binop.MinusPI -> - Val.minus_pi v1 v2 - | Binop.MinusPP -> - Val.minus_pp v1 v2 - | Binop.Mult -> - Val.mult v1 v2 - | Binop.Div -> - Val.div v1 v2 - | Binop.Mod -> - Val.mod_sem v1 v2 - | Binop.Shiftlt -> - Val.shiftlt v1 v2 - | Binop.Shiftrt -> - Val.shiftrt v1 v2 - | Binop.Lt -> - Val.lt_sem v1 v2 - | Binop.Gt -> - Val.gt_sem v1 v2 - | Binop.Le -> - Val.le_sem v1 v2 - | Binop.Ge -> - Val.ge_sem v1 v2 - | Binop.Eq -> - Val.eq_sem v1 v2 - | Binop.Ne -> - Val.ne_sem v1 v2 - | Binop.BAnd | Binop.BXor | Binop.BOr -> - Val.unknown_bit v1 - | Binop.LAnd -> - Val.land_sem v1 v2 - | Binop.LOr -> - Val.lor_sem v1 v2 - - - let rec eval_locs : Exp.t -> Mem.astate -> Val.t = - fun exp mem -> + false ) + | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) -> + Unop.equal uop1 uop2 && must_alias e1' e2' m + | Exp.BinOp (bop1, e11, e12), Exp.BinOp (bop2, e21, e22) -> + Binop.equal bop1 bop2 && must_alias e11 e21 m && must_alias e12 e22 m + | Exp.Exn t1, Exp.Exn t2 -> + must_alias t1 t2 m + | Exp.Const c1, Exp.Const c2 -> + Const.equal c1 c2 + | Exp.Cast (t1, e1'), Exp.Cast (t2, e2') -> + Typ.equal t1 t2 && must_alias e1' e2' m + | Exp.Lvar x1, Exp.Lvar x2 -> + Pvar.equal x1 x2 + | Exp.Lfield (e1, fld1, _), Exp.Lfield (e2, fld2, _) -> + must_alias e1 e2 m && Typ.Fieldname.equal fld1 fld2 + | Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) -> + must_alias e11 e21 m && must_alias e12 e22 m + | Exp.Sizeof {nbytes= Some nbytes1}, Exp.Sizeof {nbytes= Some nbytes2} -> + Int.equal nbytes1 nbytes2 + | ( Exp.Sizeof {typ= t1; dynamic_length= dynlen1; subtype= subt1} + , Exp.Sizeof {typ= t2; dynamic_length= dynlen2; subtype= subt2} ) -> + Typ.equal t1 t2 && must_alias_opt dynlen1 dynlen2 m + && Int.equal (Subtype.compare subt1 subt2) 0 + | _, _ -> + false + + +and must_alias_opt : Exp.t option -> Exp.t option -> Mem.astate -> bool = + fun e1_opt e2_opt m -> + match (e1_opt, e2_opt) with + | Some e1, Some e2 -> + must_alias e1 e2 m + | None, None -> + true + | _, _ -> + false + + +let comp_rev : Binop.t -> Binop.t = function + | Binop.Lt -> + Binop.Gt + | Binop.Gt -> + Binop.Lt + | Binop.Le -> + Binop.Ge + | Binop.Ge -> + Binop.Le + | Binop.Eq -> + Binop.Eq + | Binop.Ne -> + Binop.Ne + | _ -> + assert false + + +let comp_not : Binop.t -> Binop.t = function + | Binop.Lt -> + Binop.Ge + | Binop.Gt -> + Binop.Le + | Binop.Le -> + Binop.Gt + | Binop.Ge -> + Binop.Lt + | Binop.Eq -> + Binop.Ne + | Binop.Ne -> + Binop.Eq + | _ -> + assert false + + +let rec must_alias_cmp : Exp.t -> Mem.astate -> bool = + fun e m -> + match e with + | Exp.BinOp (Binop.Lt, e1, e2) | Exp.BinOp (Binop.Gt, e1, e2) | Exp.BinOp (Binop.Ne, e1, e2) -> + must_alias e1 e2 m + | Exp.BinOp (Binop.LAnd, e1, e2) -> + must_alias_cmp e1 m || must_alias_cmp e2 m + | Exp.BinOp (Binop.LOr, e1, e2) -> + must_alias_cmp e1 m && must_alias_cmp e2 m + | Exp.UnOp (Unop.LNot, Exp.UnOp (Unop.LNot, e1, _), _) -> + must_alias_cmp e1 m + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Lt as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Gt as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Le as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ge as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Eq as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ne as c), e1, e2), _) -> + must_alias_cmp (Exp.BinOp (comp_not c, e1, e2)) m + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> + let e1' = Exp.UnOp (Unop.LNot, e1, t) in + let e2' = Exp.UnOp (Unop.LNot, e2, t) in + must_alias_cmp (Exp.BinOp (Binop.LAnd, e1', e2')) m + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LAnd, e1, e2), t) -> + let e1' = Exp.UnOp (Unop.LNot, e1, t) in + let e2' = Exp.UnOp (Unop.LNot, e2, t) in + must_alias_cmp (Exp.BinOp (Binop.LOr, e1', e2')) m + | _ -> + false + + +let rec eval : Exp.t -> Mem.astate -> Val.t = + fun exp mem -> + if must_alias_cmp exp mem then Val.of_int 0 + else match exp with - | Exp.Var id -> ( - match Mem.find_alias id mem with - | Some AliasTarget.Simple loc -> - PowLoc.singleton loc |> Val.of_pow_loc - | Some AliasTarget.Empty _ | None -> - Val.bot ) + | Exp.Var id -> + Mem.find_stack (Var.of_id id |> Loc.of_var) mem | Exp.Lvar pvar -> - pvar |> Loc.of_pvar |> PowLoc.singleton |> Val.of_pow_loc + let ploc = pvar |> Loc.of_pvar |> PowLoc.singleton in + let arr = Mem.find_stack_set ploc mem in + ploc |> Val.of_pow_loc |> Val.join arr + | Exp.UnOp (uop, e, _) -> + eval_unop uop e mem | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem + | Exp.Const c -> + eval_const c | Exp.Cast (_, e) -> - eval_locs e mem + eval e mem | Exp.Lfield (e, fn, _) -> eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc | Exp.Lindex (e1, e2) -> - let arr = eval e1 mem in - let idx = eval e2 mem in - Val.plus_pi arr idx - | Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ -> - Val.bot - - - let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> string = - fun proc_name ~node_hash ~inst_num ~dimension -> - let proc_name = Typ.Procname.to_string proc_name in - let node_num = string_of_int node_hash in - let inst_num = string_of_int inst_num in - let dimension = string_of_int dimension in - proc_name ^ "-" ^ node_num ^ "-" ^ inst_num ^ "-" ^ dimension |> Allocsite.make - - - let eval_array_alloc - : Typ.Procname.t -> node_hash:int -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t - -> inst_num:int -> dimension:int -> Val.t = - fun pdesc ~node_hash typ ~stride ~offset ~size ~inst_num ~dimension -> - let allocsite = get_allocsite pdesc ~node_hash ~inst_num ~dimension in - let int_stride = match stride with None -> sizeof typ | Some stride -> stride in - let stride = Itv.of_int int_stride in - ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk - - - let prune_unop : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate = - fun prune_pairs e mem -> - match e with - | Exp.Var x -> ( - match Mem.find_alias x mem with - | Some AliasTarget.Simple lv -> - let v = Mem.find_heap lv mem in - let v' = Val.prune_zero v in - Mem.update_mem_in_prune prune_pairs lv v' mem - | Some AliasTarget.Empty lv -> - let v = Mem.find_heap lv mem in - let itv_v = Itv.prune_eq (Val.get_itv v) Itv.zero in - let v' = Val.modify_itv itv_v v in - Mem.update_mem_in_prune prune_pairs lv v' mem - | None -> - mem ) - | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> ( - match Mem.find_alias x mem with - | Some AliasTarget.Simple lv -> - let v = Mem.find_heap lv mem in - let itv_v = Itv.prune_eq (Val.get_itv v) Itv.false_sem in - let v' = Val.modify_itv itv_v v in - Mem.update_mem_in_prune prune_pairs lv v' mem - | Some AliasTarget.Empty lv -> - let v = Mem.find_heap lv mem in - let itv_v = Itv.prune_comp Binop.Ge (Val.get_itv v) Itv.one in - let v' = Val.modify_itv itv_v v in - Mem.update_mem_in_prune prune_pairs lv v' mem - | None -> - mem ) - | _ -> - mem + eval_lindex e1 e2 mem + | Exp.Sizeof {nbytes= Some size} -> + Val.of_int size + | Exp.Sizeof {typ; nbytes= None} -> + Val.of_int (sizeof typ) + | Exp.Exn _ | Exp.Closure _ -> + Val.Itv.top - let prune_binop_left : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate = - fun prune_pairs e mem -> - match e with - | Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e') - | Exp.BinOp ((Binop.Gt as comp), Exp.Var x, e') - | Exp.BinOp ((Binop.Le as comp), Exp.Var x, e') - | Exp.BinOp ((Binop.Ge as comp), Exp.Var x, e') -> ( - match Mem.find_simple_alias x mem with - | Some lv -> - let v = Mem.find_heap lv mem in - let v' = Val.prune_comp comp v (eval e' mem) in - Mem.update_mem_in_prune prune_pairs lv v' mem - | None -> - mem ) - | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> ( - match Mem.find_simple_alias x mem with - | Some lv -> - let v = Mem.find_heap lv mem in - let v' = Val.prune_eq v (eval e' mem) in - Mem.update_mem_in_prune prune_pairs lv v' mem - | None -> - mem ) - | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> ( - match Mem.find_simple_alias x mem with - | Some lv -> - let v = Mem.find_heap lv mem in - let v' = Val.prune_ne v (eval e' mem) in - Mem.update_mem_in_prune prune_pairs lv v' mem - | None -> - mem ) +(* NOTE: multidimensional array is not supported yet *) +and eval_lindex array_exp index_exp mem = + let array_v, index_v = (eval array_exp mem, eval index_exp mem) in + let arr = Val.plus_pi array_v index_v in + if ArrayBlk.is_bot (Val.get_array_blk arr) then + match array_exp with + | Exp.Lfield _ when not (PowLoc.is_bot (Val.get_pow_loc array_v)) -> + (* It handles the case accessing an array field of struct, + e.g., x.f[n] . Since our abstract domain distinguishes + memory sections for each array fields in struct, it finds + the memory section using the abstract memory, though the + memory lookup is not required to evaluate the address of + x.f[n] in the concrete semantics. *) + Val.plus_pi (Mem.find_set (Val.get_pow_loc array_v) mem) index_v | _ -> - mem - - - let prune_binop_right : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate = - fun prune_pairs e mem -> + Val.of_pow_loc PowLoc.unknown + else arr + + +and eval_unop : Unop.t -> Exp.t -> Mem.astate -> Val.t = + fun unop e mem -> + let v = eval e mem in + match unop with + | Unop.Neg -> + Val.neg v + | Unop.BNot -> + Val.unknown_bit v + | Unop.LNot -> + Val.lnot v + + +and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t = + fun binop e1 e2 mem -> + let v1 = eval e1 mem in + let v2 = eval e2 mem in + match binop with + | Binop.PlusA -> + Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2) + | Binop.PlusPI -> + Val.plus_pi v1 v2 + | Binop.MinusA -> + Val.joins [Val.minus v1 v2; Val.minus_pi v1 v2; Val.minus_pp v1 v2] + | Binop.MinusPI -> + Val.minus_pi v1 v2 + | Binop.MinusPP -> + Val.minus_pp v1 v2 + | Binop.Mult -> + Val.mult v1 v2 + | Binop.Div -> + Val.div v1 v2 + | Binop.Mod -> + Val.mod_sem v1 v2 + | Binop.Shiftlt -> + Val.shiftlt v1 v2 + | Binop.Shiftrt -> + Val.shiftrt v1 v2 + | Binop.Lt -> + Val.lt_sem v1 v2 + | Binop.Gt -> + Val.gt_sem v1 v2 + | Binop.Le -> + Val.le_sem v1 v2 + | Binop.Ge -> + Val.ge_sem v1 v2 + | Binop.Eq -> + Val.eq_sem v1 v2 + | Binop.Ne -> + Val.ne_sem v1 v2 + | Binop.BAnd | Binop.BXor | Binop.BOr -> + Val.unknown_bit v1 + | Binop.LAnd -> + Val.land_sem v1 v2 + | Binop.LOr -> + Val.lor_sem v1 v2 + + +let rec eval_locs : Exp.t -> Mem.astate -> Val.t = + fun exp mem -> + match exp with + | Exp.Var id -> ( + match Mem.find_alias id mem with + | Some AliasTarget.Simple loc -> + PowLoc.singleton loc |> Val.of_pow_loc + | Some AliasTarget.Empty _ | None -> + Val.bot ) + | Exp.Lvar pvar -> + pvar |> Loc.of_pvar |> PowLoc.singleton |> Val.of_pow_loc + | Exp.BinOp (bop, e1, e2) -> + eval_binop bop e1 e2 mem + | Exp.Cast (_, e) -> + eval_locs e mem + | Exp.Lfield (e, fn, _) -> + eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc + | Exp.Lindex (e1, e2) -> + let arr = eval e1 mem in + let idx = eval e2 mem in + Val.plus_pi arr idx + | Exp.Const _ | Exp.UnOp _ | Exp.Sizeof _ | Exp.Exn _ | Exp.Closure _ -> + Val.bot + + +let get_allocsite : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> string = + fun proc_name ~node_hash ~inst_num ~dimension -> + let proc_name = Typ.Procname.to_string proc_name in + let node_num = string_of_int node_hash in + let inst_num = string_of_int inst_num in + let dimension = string_of_int dimension in + proc_name ^ "-" ^ node_num ^ "-" ^ inst_num ^ "-" ^ dimension |> Allocsite.make + + +let eval_array_alloc + : Typ.Procname.t -> node_hash:int -> Typ.t -> stride:int option -> offset:Itv.t -> size:Itv.t + -> inst_num:int -> dimension:int -> Val.t = + fun pdesc ~node_hash typ ~stride ~offset ~size ~inst_num ~dimension -> + let allocsite = get_allocsite pdesc ~node_hash ~inst_num ~dimension in + let int_stride = match stride with None -> sizeof typ | Some stride -> stride in + let stride = Itv.of_int int_stride in + ArrayBlk.make allocsite ~offset ~size ~stride |> Val.of_array_blk + + +let prune_unop : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate = + fun prune_pairs e mem -> + match e with + | Exp.Var x -> ( + match Mem.find_alias x mem with + | Some AliasTarget.Simple lv -> + let v = Mem.find_heap lv mem in + let v' = Val.prune_zero v in + Mem.update_mem_in_prune prune_pairs lv v' mem + | Some AliasTarget.Empty lv -> + let v = Mem.find_heap lv mem in + let itv_v = Itv.prune_eq (Val.get_itv v) Itv.zero in + let v' = Val.modify_itv itv_v v in + Mem.update_mem_in_prune prune_pairs lv v' mem + | None -> + mem ) + | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> ( + match Mem.find_alias x mem with + | Some AliasTarget.Simple lv -> + let v = Mem.find_heap lv mem in + let itv_v = Itv.prune_eq (Val.get_itv v) Itv.false_sem in + let v' = Val.modify_itv itv_v v in + Mem.update_mem_in_prune prune_pairs lv v' mem + | Some AliasTarget.Empty lv -> + let v = Mem.find_heap lv mem in + let itv_v = Itv.prune_comp Binop.Ge (Val.get_itv v) Itv.one in + let v' = Val.modify_itv itv_v v in + Mem.update_mem_in_prune prune_pairs lv v' mem + | None -> + mem ) + | _ -> + mem + + +let prune_binop_left : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate = + fun prune_pairs e mem -> + match e with + | Exp.BinOp ((Binop.Lt as comp), Exp.Var x, e') + | Exp.BinOp ((Binop.Gt as comp), Exp.Var x, e') + | Exp.BinOp ((Binop.Le as comp), Exp.Var x, e') + | Exp.BinOp ((Binop.Ge as comp), Exp.Var x, e') -> ( + match Mem.find_simple_alias x mem with + | Some lv -> + let v = Mem.find_heap lv mem in + let v' = Val.prune_comp comp v (eval e' mem) in + Mem.update_mem_in_prune prune_pairs lv v' mem + | None -> + mem ) + | Exp.BinOp (Binop.Eq, Exp.Var x, e') -> ( + match Mem.find_simple_alias x mem with + | Some lv -> + let v = Mem.find_heap lv mem in + let v' = Val.prune_eq v (eval e' mem) in + Mem.update_mem_in_prune prune_pairs lv v' mem + | None -> + mem ) + | Exp.BinOp (Binop.Ne, Exp.Var x, e') -> ( + match Mem.find_simple_alias x mem with + | Some lv -> + let v = Mem.find_heap lv mem in + let v' = Val.prune_ne v (eval e' mem) in + Mem.update_mem_in_prune prune_pairs lv v' mem + | None -> + mem ) + | _ -> + mem + + +let prune_binop_right : PrunePairs.t ref -> Exp.t -> Mem.astate -> Mem.astate = + fun prune_pairs e mem -> + match e with + | Exp.BinOp ((Binop.Lt as c), e', Exp.Var x) + | Exp.BinOp ((Binop.Gt as c), e', Exp.Var x) + | Exp.BinOp ((Binop.Le as c), e', Exp.Var x) + | Exp.BinOp ((Binop.Ge as c), e', Exp.Var x) + | Exp.BinOp ((Binop.Eq as c), e', Exp.Var x) + | Exp.BinOp ((Binop.Ne as c), e', Exp.Var x) -> + prune_binop_left prune_pairs (Exp.BinOp (comp_rev c, Exp.Var x, e')) mem + | _ -> + mem + + +let is_unreachable_constant : Exp.t -> Mem.astate -> bool = + fun e m -> Val.( <= ) ~lhs:(eval e m) ~rhs:(Val.of_int 0) + + +let prune_unreachable : Exp.t -> Mem.astate -> Mem.astate = + fun e mem -> if is_unreachable_constant e mem then Mem.bot else mem + + +let prune : Exp.t -> Mem.astate -> Mem.astate = + fun e mem -> + let prune_pairs = ref PrunePairs.empty in + let rec prune_helper e mem = + let mem = + mem |> prune_unreachable e |> prune_unop prune_pairs e |> prune_binop_left prune_pairs e + |> prune_binop_right prune_pairs e + in match e with - | Exp.BinOp ((Binop.Lt as c), e', Exp.Var x) - | Exp.BinOp ((Binop.Gt as c), e', Exp.Var x) - | Exp.BinOp ((Binop.Le as c), e', Exp.Var x) - | Exp.BinOp ((Binop.Ge as c), e', Exp.Var x) - | Exp.BinOp ((Binop.Eq as c), e', Exp.Var x) - | Exp.BinOp ((Binop.Ne as c), e', Exp.Var x) -> - prune_binop_left prune_pairs (Exp.BinOp (comp_rev c, Exp.Var x, e')) mem + | Exp.BinOp (Binop.Ne, e, Exp.Const Const.Cint i) when IntLit.iszero i -> + prune_helper e mem + | Exp.BinOp (Binop.Eq, e, Exp.Const Const.Cint i) when IntLit.iszero i -> + prune_helper (Exp.UnOp (Unop.LNot, e, None)) mem + | Exp.UnOp (Unop.Neg, Exp.Var x, _) -> + prune_helper (Exp.Var x) mem + | Exp.BinOp (Binop.LAnd, e1, e2) -> + mem |> prune_helper e1 |> prune_helper e2 + | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> + mem |> prune_helper (Exp.UnOp (Unop.LNot, e1, t)) + |> prune_helper (Exp.UnOp (Unop.LNot, e2, t)) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Lt as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Gt as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Le as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ge as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Eq as c), e1, e2), _) + | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ne as c), e1, e2), _) -> + prune_helper (Exp.BinOp (comp_not c, e1, e2)) mem | _ -> mem - - - let is_unreachable_constant : Exp.t -> Mem.astate -> bool = - fun e m -> Val.( <= ) ~lhs:(eval e m) ~rhs:(Val.of_int 0) - - - let prune_unreachable : Exp.t -> Mem.astate -> Mem.astate = - fun e mem -> if is_unreachable_constant e mem then Mem.bot else mem - - - let prune : Exp.t -> Mem.astate -> Mem.astate = - fun e mem -> - let prune_pairs = ref PrunePairs.empty in - let rec prune_helper e mem = - let mem = - mem |> prune_unreachable e |> prune_unop prune_pairs e |> prune_binop_left prune_pairs e - |> prune_binop_right prune_pairs e - in - match e with - | Exp.BinOp (Binop.Ne, e, Exp.Const Const.Cint i) when IntLit.iszero i -> - prune_helper e mem - | Exp.BinOp (Binop.Eq, e, Exp.Const Const.Cint i) when IntLit.iszero i -> - prune_helper (Exp.UnOp (Unop.LNot, e, None)) mem - | Exp.UnOp (Unop.Neg, Exp.Var x, _) -> - prune_helper (Exp.Var x) mem - | Exp.BinOp (Binop.LAnd, e1, e2) -> - mem |> prune_helper e1 |> prune_helper e2 - | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> - mem |> prune_helper (Exp.UnOp (Unop.LNot, e1, t)) - |> prune_helper (Exp.UnOp (Unop.LNot, e2, t)) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Lt as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Gt as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Le as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ge as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Eq as c), e1, e2), _) - | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ne as c), e1, e2), _) -> - prune_helper (Exp.BinOp (comp_not c, e1, e2)) mem + in + let mem = Mem.apply_latest_prune e mem in + let mem = prune_helper e mem in + Mem.set_prune_pairs !prune_pairs mem + + +let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list = + fun pdesc -> + let proc_name = Procdesc.get_proc_name pdesc in + Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ)) + + +let get_matching_pairs + : Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate + -> callee_ret_alias:AliasTarget.t option + -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list * AliasTarget.t option = + fun tenv formal actual typ caller_mem callee_mem ~callee_ret_alias -> + let get_itv v = Val.get_itv v 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_field_name (fn, _, _) = fn in + let append_field v fn = PowLoc.append_field (Val.get_all_locs v) ~fn in + let deref_field v fn mem = Mem.find_heap_set (append_field v fn) mem in + let deref_ptr v mem = + let array_locs = Val.get_array_locs v in + let locs = if PowLoc.is_empty array_locs then Val.get_pow_loc v else array_locs in + Mem.find_heap_set locs mem + in + let ret_alias = ref None in + let add_ret_alias v1 v2 = + match callee_ret_alias with + | Some ret_loc -> + if PowLoc.is_singleton v1 && PowLoc.is_singleton v2 + && AliasTarget.use (PowLoc.min_elt v1) ret_loc + then ret_alias := Some (AliasTarget.replace (PowLoc.min_elt v2) ret_loc) + | None -> + () + in + let add_pair_itv itv1 itv2 traces l = + let open Itv in + if itv1 <> bot && itv1 <> top then + if Itv.eq itv2 bot then + (lb itv1, Bottom, TraceSet.empty) :: (ub itv1, Bottom, TraceSet.empty) :: l + else (lb itv1, NonBottom (lb itv2), traces) :: (ub itv1, NonBottom (ub itv2), traces) :: l + else l + in + let add_pair_val v1 v2 pairs = + add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; + pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2) + |> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2) + |> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2) + in + let add_pair_field v1 v2 pairs fn = + add_ret_alias (append_field v1 fn) (append_field v2 fn) ; + let v1' = deref_field v1 fn callee_mem in + let v2' = deref_field v2 fn caller_mem in + add_pair_val v1' v2' pairs + in + let add_pair_ptr typ v1 v2 pairs = + add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; + match typ.Typ.desc with + | Typ.Tptr ({desc= Tstruct typename}, _) -> ( + match Tenv.lookup tenv typename with + | Some str -> + let fns = List.map ~f:get_field_name str.Typ.Struct.fields in + List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns | _ -> - mem - in - let mem = Mem.apply_latest_prune e mem in - let mem = prune_helper e mem in - Mem.set_prune_pairs !prune_pairs mem - - - let get_formals : Procdesc.t -> (Pvar.t * Typ.t) list = - fun pdesc -> - let proc_name = Procdesc.get_proc_name pdesc in - Procdesc.get_formals pdesc |> List.map ~f:(fun (name, typ) -> (Pvar.mk name proc_name, typ)) - - - let get_matching_pairs - : Tenv.t -> Val.t -> Val.t -> Typ.t -> Mem.astate -> Mem.astate - -> callee_ret_alias:AliasTarget.t option - -> (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list * AliasTarget.t option = - fun tenv formal actual typ caller_mem callee_mem ~callee_ret_alias -> - let get_itv v = Val.get_itv v 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_field_name (fn, _, _) = fn in - let append_field v fn = PowLoc.append_field (Val.get_all_locs v) ~fn in - let deref_field v fn mem = Mem.find_heap_set (append_field v fn) mem in - let deref_ptr v mem = - let array_locs = Val.get_array_locs v in - let locs = if PowLoc.is_empty array_locs then Val.get_pow_loc v else array_locs in - Mem.find_heap_set locs mem - in - let ret_alias = ref None in - let add_ret_alias v1 v2 = - match callee_ret_alias with - | Some ret_loc -> - if PowLoc.is_singleton v1 && PowLoc.is_singleton v2 - && AliasTarget.use (PowLoc.min_elt v1) ret_loc - then ret_alias := Some (AliasTarget.replace (PowLoc.min_elt v2) ret_loc) - | None -> - () - in - let add_pair_itv itv1 itv2 traces l = - let open Itv in - if itv1 <> bot && itv1 <> top then - if Itv.eq itv2 bot then - (lb itv1, Bottom, TraceSet.empty) :: (ub itv1, Bottom, TraceSet.empty) :: l - else (lb itv1, NonBottom (lb itv2), traces) :: (ub itv1, NonBottom (ub itv2), traces) :: l - else l - in - let add_pair_val v1 v2 pairs = - add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; - pairs |> add_pair_itv (get_itv v1) (get_itv v2) (Val.get_traces v2) - |> add_pair_itv (get_offset v1) (get_offset v2) (Val.get_traces v2) - |> add_pair_itv (get_size v1) (get_size v2) (Val.get_traces v2) - in - let add_pair_field v1 v2 pairs fn = - add_ret_alias (append_field v1 fn) (append_field v2 fn) ; - let v1' = deref_field v1 fn callee_mem in - let v2' = deref_field v2 fn caller_mem in - add_pair_val v1' v2' pairs - in - let add_pair_ptr typ v1 v2 pairs = - add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; - match typ.Typ.desc with - | Typ.Tptr ({desc= Tstruct typename}, _) -> ( - match Tenv.lookup tenv typename with - | Some str -> - let fns = List.map ~f:get_field_name str.Typ.Struct.fields in - List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns - | _ -> - pairs ) - | Typ.Tptr (_, _) -> - let v1' = deref_ptr v1 callee_mem in - let v2' = deref_ptr v2 caller_mem in - add_pair_val v1' v2' pairs - | _ -> - pairs - in - let pairs = [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual in - (pairs, !ret_alias) - - - let subst_map_of_pairs - : (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list - -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t = - fun pairs -> - let add_pair (bound_map, trace_map) (formal, actual, traces) = - if Itv.Bound.is_const formal |> Option.is_some then (bound_map, trace_map) - else - let symbol = Itv.Bound.get_one_symbol formal in - (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map) - in - List.fold ~f:add_pair ~init:(Itv.SubstMap.empty, Itv.SubstMap.empty) pairs - - - let rec list_fold2_def - : default:Val.t -> f:('a -> Val.t -> 'b -> 'b) -> 'a list -> Val.t list -> init:'b -> 'b = - fun ~default ~f xs ys ~init:acc -> - match (xs, ys) with - | [], _ -> - acc - | x :: xs', [] -> - list_fold2_def ~default ~f xs' ys ~init:(f x default acc) - | [x], _ :: _ -> - f x (List.fold ~f:Val.join ~init:Val.bot ys) acc - | x :: xs', y :: ys' -> - list_fold2_def ~default ~f xs' ys' ~init:(f x y acc) - - - let get_subst_map - : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate - -> callee_ret_alias:AliasTarget.t option - -> (Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t) - * AliasTarget.t option = - fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias -> - let add_pair (formal, typ) actual (l, ret_alias) = - let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in - let new_matching, ret_alias' = - get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem ~callee_ret_alias - in - (List.rev_append new_matching l, Option.first_some ret_alias ret_alias') - in - let formals = get_formals callee_pdesc in - let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) params in - let pairs, ret_alias = - list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:([], None) + pairs ) + | Typ.Tptr (_, _) -> + let v1' = deref_ptr v1 callee_mem in + let v2' = deref_ptr v2 caller_mem in + add_pair_val v1' v2' pairs + | _ -> + pairs + in + let pairs = [] |> add_pair_val formal actual |> add_pair_ptr typ formal actual in + (pairs, !ret_alias) + + +let subst_map_of_pairs + : (Itv.Bound.t * Itv.Bound.t bottom_lifted * TraceSet.t) list + -> Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t = + fun pairs -> + let add_pair (bound_map, trace_map) (formal, actual, traces) = + if Itv.Bound.is_const formal |> Option.is_some then (bound_map, trace_map) + else + let symbol = Itv.Bound.get_one_symbol formal in + (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map) + in + List.fold ~f:add_pair ~init:(Itv.SubstMap.empty, Itv.SubstMap.empty) pairs + + +let rec list_fold2_def + : default:Val.t -> f:('a -> Val.t -> 'b -> 'b) -> 'a list -> Val.t list -> init:'b -> 'b = + fun ~default ~f xs ys ~init:acc -> + match (xs, ys) with + | [], _ -> + acc + | x :: xs', [] -> + list_fold2_def ~default ~f xs' ys ~init:(f x default acc) + | [x], _ :: _ -> + f x (List.fold ~f:Val.join ~init:Val.bot ys) acc + | x :: xs', y :: ys' -> + list_fold2_def ~default ~f xs' ys' ~init:(f x y acc) + + +let get_subst_map + : Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate + -> callee_ret_alias:AliasTarget.t option + -> (Itv.Bound.t bottom_lifted Itv.SubstMap.t * TraceSet.t Itv.SubstMap.t) + * AliasTarget.t option = + fun tenv callee_pdesc params caller_mem callee_entry_mem ~callee_ret_alias -> + let add_pair (formal, typ) actual (l, ret_alias) = + let formal = Mem.find_heap (Loc.of_pvar formal) callee_entry_mem in + let new_matching, ret_alias' = + get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem ~callee_ret_alias in - (subst_map_of_pairs pairs, ret_alias) -end + (List.rev_append new_matching l, Option.first_some ret_alias ret_alias') + in + let formals = get_formals callee_pdesc in + let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem) params in + let pairs, ret_alias = + list_fold2_def ~default:Val.Itv.top ~f:add_pair formals actuals ~init:([], None) + in + (subst_map_of_pairs pairs, ret_alias) diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index ef731f1ed..f50a83387 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -13,202 +13,154 @@ open! AbstractDomain.Types module L = Logging module Dom = BufferOverrunDomain module PO = BufferOverrunProofObligations +module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace module TraceSet = Trace.Set -module type S = sig - module CFG : ProcCfg.S - - module Sem : module type of BufferOverrunSemantics.Make (CFG) - - module Exec : sig - val load_val : Ident.t -> Dom.Val.astate -> Dom.Mem.astate -> Dom.Mem.astate - - type decl_local = - Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t -> inst_num:int - -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int - - val decl_local_array : - 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 - -> Dom.Mem.astate * int - - type decl_sym_val = - Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t - -> Dom.Mem.astate -> Dom.Mem.astate - - val decl_sym_arr : - 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 - -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate - -> Dom.Mem.astate - - val init_array_fields : - Tenv.t -> Typ.Procname.t -> node_hash:int -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.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 - end - - module Check : sig - val lindex : - array_exp:Exp.t -> index_exp:Exp.t -> Dom.Mem.astate -> Typ.Procname.t -> Location.t - -> PO.ConditionSet.t -> PO.ConditionSet.t - end -end - -module Make (CFG : ProcCfg.S) = struct - module CFG = CFG - module Sem = BufferOverrunSemantics.Make (CFG) - - module Exec = struct - let load_val id val_ mem = - let locs = val_ |> Dom.Val.get_all_locs in - let v = Dom.Mem.find_heap_set locs mem in - let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in - if PowLoc.is_singleton locs then Dom.Mem.load_simple_alias id (PowLoc.min_elt locs) mem - else mem - - - type decl_local = - Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t -> inst_num:int - -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int - - let decl_local_array - : 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 -> Dom.Mem.astate * int = - 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 arr = - Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size ~inst_num - ~dimension - |> Dom.Val.add_trace_elem (Trace.ArrDecl location) - in +module Exec = struct + let load_val id val_ mem = + let locs = val_ |> Dom.Val.get_all_locs in + let v = Dom.Mem.find_heap_set locs mem in + let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in + if PowLoc.is_singleton locs then Dom.Mem.load_simple_alias id (PowLoc.min_elt locs) mem + else mem + + + type decl_local = + Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t -> inst_num:int + -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int + + let decl_local_array + : 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 + -> Dom.Mem.astate * int = + 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 arr = + Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size ~inst_num ~dimension + |> Dom.Val.add_trace_elem (Trace.ArrDecl location) + in + let mem = + if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem else Dom.Mem.add_heap loc arr mem + in + let loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension) in + let mem, _ = + decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem + in + (mem, inst_num + 1) + + + type decl_sym_val = + Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t + -> Dom.Mem.astate -> Dom.Mem.astate + + let decl_sym_arr + : 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 + -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate + -> Dom.Mem.astate = + fun ~decl_sym_val pname tenv ~node_hash location ~depth loc typ ?offset ?size ~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 itv_make_sym () = Itv.make_sym pname new_sym_num in + let offset = option_value offset itv_make_sym in + let size = option_value size itv_make_sym in + let alloc_num = Itv.Counter.next new_alloc_num in + let elem = Trace.SymAssign (loc, location) in + let arr = + Sem.eval_array_alloc pname ~node_hash typ ~stride:None ~offset ~size ~inst_num + ~dimension:alloc_num + |> Dom.Val.add_trace_elem elem + in + let mem = Dom.Mem.add_heap loc arr mem in + let deref_loc = + Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num) + in + decl_sym_val pname tenv ~node_hash location ~depth deref_loc typ 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 field_loc = PowLoc.append_field locs ~fn:field_name in let mem = - if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem - else Dom.Mem.add_heap loc arr mem - in - let loc = Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension) in - let mem, _ = - decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem - in - (mem, inst_num + 1) - - - type decl_sym_val = - Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t - -> Dom.Mem.astate -> Dom.Mem.astate - - let decl_sym_arr - : 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 - -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate - -> Dom.Mem.astate = - fun ~decl_sym_val pname tenv ~node_hash location ~depth loc typ ?offset ?size ~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 itv_make_sym () = Itv.make_sym pname new_sym_num in - let offset = option_value offset itv_make_sym in - let size = option_value size itv_make_sym in - let alloc_num = Itv.Counter.next new_alloc_num in - let elem = Trace.SymAssign (loc, location) in - let arr = - Sem.eval_array_alloc pname ~node_hash typ ~stride:None ~offset ~size ~inst_num - ~dimension:alloc_num - |> Dom.Val.add_trace_elem elem - in - let mem = Dom.Mem.add_heap loc arr mem in - let deref_loc = - Loc.of_allocsite (Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num) - in - decl_sym_val pname tenv ~node_hash location ~depth deref_loc typ 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 field_loc = PowLoc.append_field locs ~fn:field_name in - let mem = - match field_typ.Typ.desc with - | Tarray {elt= typ; length= Some length; stride} -> - let length = Itv.of_int_lit length in - let length = - Option.value_map dyn_length ~default:length ~f:(fun dyn_length -> - let i = Dom.Val.get_itv (Sem.eval dyn_length mem) in - Itv.plus i length ) - in - let stride = Option.map stride ~f:IntLit.to_int in - let v = - Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size:length - ~inst_num ~dimension - in - Dom.Mem.strong_update_heap field_loc v mem - | _ -> - init_fields field_typ field_loc dimension ?dyn_length mem - in - (mem, inst_num + 1) - and init_fields typ locs dimension ?dyn_length mem = - match typ.Typ.desc with - | Tstruct typename -> ( - match Tenv.lookup tenv typename with - | Some str -> - let f = init_field locs (dimension + 1) in - IList.fold_last ~f ~f_last:(f ?dyn_length) ~init:(mem, 1) str.Typ.Struct.fields - |> fst - | None -> - mem ) + match field_typ.Typ.desc with + | Tarray {elt= typ; length= Some length; stride} -> + let length = Itv.of_int_lit length in + let length = + Option.value_map dyn_length ~default:length ~f:(fun dyn_length -> + let i = Dom.Val.get_itv (Sem.eval dyn_length mem) in + Itv.plus i length ) + in + let stride = Option.map stride ~f:IntLit.to_int in + let v = + Sem.eval_array_alloc pname ~node_hash typ ~stride ~offset:Itv.zero ~size:length + ~inst_num ~dimension + in + Dom.Mem.strong_update_heap field_loc v mem | _ -> - mem + init_fields field_typ field_loc dimension ?dyn_length mem in - init_fields typ locs 1 ?dyn_length mem - - - let rec set_dyn_length tenv typ locs dyn_length mem = + (mem, inst_num + 1) + and init_fields typ locs dimension ?dyn_length mem = match typ.Typ.desc with | Tstruct typename -> ( match Tenv.lookup tenv typename with - | Some {fields} when not (List.is_empty fields) - -> ( - let field_name, field_typ, _ = List.last_exn fields in - let field_loc = PowLoc.append_field locs ~fn:field_name in - match field_typ.Typ.desc with - | Tarray {length= Some length} -> - let length = Itv.plus (Itv.of_int_lit length) dyn_length in - let v = Dom.Mem.find_set field_loc mem |> Dom.Val.set_array_size length in - Dom.Mem.strong_update_heap field_loc v mem - | _ -> - set_dyn_length tenv field_typ field_loc dyn_length mem ) - | _ -> + | Some str -> + let f = init_field locs (dimension + 1) in + IList.fold_last ~f ~f_last:(f ?dyn_length) ~init:(mem, 1) str.Typ.Struct.fields |> fst + | None -> mem ) | _ -> mem - end - - module Check = struct - let array_access ~arr ~idx ~is_plus pname location cond_set = - let arr_blk = Dom.Val.get_array_blk arr in - let arr_traces = Dom.Val.get_traces arr in - let size = ArrayBlk.sizeof arr_blk in - let offset = ArrayBlk.offsetof arr_blk in - let idx_itv = Dom.Val.get_itv idx in - let idx_traces = Dom.Val.get_traces idx in - let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in - L.(debug BufferOverrun Verbose) "@[Add condition :@," ; - L.(debug BufferOverrun Verbose) "array: %a@," ArrayBlk.pp arr_blk ; - L.(debug BufferOverrun Verbose) " idx: %a@," Itv.pp idx_in_blk ; - L.(debug BufferOverrun Verbose) "@]@." ; - match (size, idx_in_blk) with - | NonBottom size, NonBottom idx -> - let traces = TraceSet.merge ~arr_traces ~idx_traces location in - PO.ConditionSet.add_array_access pname location ~size ~idx traces cond_set + in + init_fields typ locs 1 ?dyn_length mem + + + let rec set_dyn_length tenv typ locs dyn_length mem = + match typ.Typ.desc with + | Tstruct typename -> ( + match Tenv.lookup tenv typename with + | Some {fields} when not (List.is_empty fields) + -> ( + let field_name, field_typ, _ = List.last_exn fields in + let field_loc = PowLoc.append_field locs ~fn:field_name in + match field_typ.Typ.desc with + | Tarray {length= Some length} -> + let length = Itv.plus (Itv.of_int_lit length) dyn_length in + let v = Dom.Mem.find_set field_loc mem |> Dom.Val.set_array_size length in + Dom.Mem.strong_update_heap field_loc v mem + | _ -> + set_dyn_length tenv field_typ field_loc dyn_length mem ) | _ -> - cond_set - + mem ) + | _ -> + mem +end - let lindex ~array_exp ~index_exp mem pname location cond_set = - let locs = Sem.eval_locs array_exp mem |> Dom.Val.get_all_locs in - let arr = Dom.Mem.find_set locs mem in - let idx = Sem.eval index_exp mem in - array_access ~arr ~idx ~is_plus:true pname location cond_set - end +module Check = struct + let array_access ~arr ~idx ~is_plus pname location cond_set = + let arr_blk = Dom.Val.get_array_blk arr in + let arr_traces = Dom.Val.get_traces arr in + let size = ArrayBlk.sizeof arr_blk in + let offset = ArrayBlk.offsetof arr_blk in + let idx_itv = Dom.Val.get_itv idx in + let idx_traces = Dom.Val.get_traces idx in + let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in + L.(debug BufferOverrun Verbose) "@[Add condition :@," ; + L.(debug BufferOverrun Verbose) "array: %a@," ArrayBlk.pp arr_blk ; + L.(debug BufferOverrun Verbose) " idx: %a@," Itv.pp idx_in_blk ; + L.(debug BufferOverrun Verbose) "@]@." ; + match (size, idx_in_blk) with + | NonBottom size, NonBottom idx -> + let traces = TraceSet.merge ~arr_traces ~idx_traces location in + PO.ConditionSet.add_array_access pname location ~size ~idx traces cond_set + | _ -> + cond_set + + + let lindex ~array_exp ~index_exp mem pname location cond_set = + let locs = Sem.eval_locs array_exp mem |> Dom.Val.get_all_locs in + let arr = Dom.Mem.find_set locs mem in + let idx = Sem.eval index_exp mem in + array_access ~arr ~idx ~is_plus:true pname location cond_set end diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli new file mode 100644 index 000000000..f72f7e7be --- /dev/null +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -0,0 +1,51 @@ +(* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +open! IStd +open AbsLoc +module Dom = BufferOverrunDomain +module PO = BufferOverrunProofObligations + +module Exec : sig + val load_val : Ident.t -> Dom.Val.astate -> Dom.Mem.astate -> Dom.Mem.astate + + type decl_local = + Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> Typ.t -> inst_num:int + -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int + + val decl_local_array : + 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 + -> Dom.Mem.astate * int + + type decl_sym_val = + Typ.Procname.t -> Tenv.t -> node_hash:int -> Location.t -> depth:int -> Loc.t -> Typ.t + -> Dom.Mem.astate -> Dom.Mem.astate + + val decl_sym_arr : + 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 + -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate -> Dom.Mem.astate + + val init_array_fields : + Tenv.t -> Typ.Procname.t -> node_hash:int -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.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 +end + +module Check : sig + val array_access : + arr:Dom.Val.t -> idx:Dom.Val.t -> is_plus:bool -> Typ.Procname.t -> Location.t + -> PO.ConditionSet.t -> PO.ConditionSet.t + + val lindex : + array_exp:Exp.t -> index_exp:Exp.t -> Dom.Mem.astate -> Typ.Procname.t -> Location.t + -> PO.ConditionSet.t -> PO.ConditionSet.t +end