|
|
@ -24,7 +24,12 @@ module Payload = SummaryPayload.Make (struct
|
|
|
|
let of_payloads (payloads : Payloads.t) = payloads.uninit
|
|
|
|
let of_payloads (payloads : Payloads.t) = payloads.uninit
|
|
|
|
end)
|
|
|
|
end)
|
|
|
|
|
|
|
|
|
|
|
|
let blacklisted_functions = [BuiltinDecl.__set_array_length]
|
|
|
|
module Models = struct
|
|
|
|
|
|
|
|
let initializing_all_args = [BuiltinDecl.__set_array_length]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let is_initializing_all_args pname =
|
|
|
|
|
|
|
|
List.exists initializing_all_args ~f:(fun fname -> Typ.Procname.equal pname fname)
|
|
|
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
let should_report_on_type t =
|
|
|
|
let should_report_on_type t =
|
|
|
|
match t.Typ.desc with
|
|
|
|
match t.Typ.desc with
|
|
|
@ -36,10 +41,6 @@ let should_report_on_type t =
|
|
|
|
false
|
|
|
|
false
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let is_blacklisted_function pname =
|
|
|
|
|
|
|
|
List.exists ~f:(fun fname -> Typ.Procname.equal pname fname) blacklisted_functions
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
module TransferFunctions (CFG : ProcCfg.S) = struct
|
|
|
|
module TransferFunctions (CFG : ProcCfg.S) = struct
|
|
|
|
module CFG = CFG
|
|
|
|
module CFG = CFG
|
|
|
|
module Domain = RecordDomain
|
|
|
|
module Domain = RecordDomain
|
|
|
@ -307,7 +308,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|
|
|
|
in
|
|
|
|
in
|
|
|
|
match AccessExpression.get_base access_expr with
|
|
|
|
match AccessExpression.get_base access_expr with
|
|
|
|
| _, {Typ.desc= Tarray _}
|
|
|
|
| _, {Typ.desc= Tarray _}
|
|
|
|
when Option.value_map ~default:false ~f:is_blacklisted_function pname_opt ->
|
|
|
|
when Option.exists pname_opt ~f:Models.is_initializing_all_args ->
|
|
|
|
D.remove access_expr acc
|
|
|
|
D.remove access_expr acc
|
|
|
|
| _, t
|
|
|
|
| _, t
|
|
|
|
(* Access to a field of a struct or an element of an array by reference *)
|
|
|
|
(* Access to a field of a struct or an element of an array by reference *)
|
|
|
@ -361,41 +362,41 @@ end
|
|
|
|
module CFG = ProcCfg.Normal
|
|
|
|
module CFG = ProcCfg.Normal
|
|
|
|
module Analyzer = LowerHil.MakeAbstractInterpreter (CFG) (TransferFunctions)
|
|
|
|
module Analyzer = LowerHil.MakeAbstractInterpreter (CFG) (TransferFunctions)
|
|
|
|
|
|
|
|
|
|
|
|
let get_locals tenv pdesc =
|
|
|
|
module Initial = struct
|
|
|
|
List.fold
|
|
|
|
let get_locals tenv pdesc =
|
|
|
|
~f:(fun acc (var_data : ProcAttributes.var_data) ->
|
|
|
|
List.fold (Procdesc.get_locals pdesc) ~init:[]
|
|
|
|
let pvar = Pvar.mk var_data.name (Procdesc.get_proc_name pdesc) in
|
|
|
|
~f:(fun acc (var_data : ProcAttributes.var_data) ->
|
|
|
|
let base_access_expr = AccessExpression.Base (Var.of_pvar pvar, var_data.typ) in
|
|
|
|
let pvar = Pvar.mk var_data.name (Procdesc.get_proc_name pdesc) in
|
|
|
|
match var_data.typ.Typ.desc with
|
|
|
|
let base_access_expr = AccessExpression.Base (Var.of_pvar pvar, var_data.typ) in
|
|
|
|
| Typ.Tstruct qual_name
|
|
|
|
match var_data.typ.Typ.desc with
|
|
|
|
(* T30105165 remove filtering after we improve union translation *)
|
|
|
|
| Typ.Tstruct qual_name
|
|
|
|
when not (Typ.Name.is_union qual_name) -> (
|
|
|
|
(* T30105165 remove filtering after we improve union translation *)
|
|
|
|
match Tenv.lookup tenv qual_name with
|
|
|
|
when not (Typ.Name.is_union qual_name) -> (
|
|
|
|
| Some {fields} ->
|
|
|
|
match Tenv.lookup tenv qual_name with
|
|
|
|
let flist =
|
|
|
|
| Some {fields} ->
|
|
|
|
List.fold
|
|
|
|
let flist =
|
|
|
|
~f:(fun acc' (fn, _, _) ->
|
|
|
|
List.fold
|
|
|
|
AccessExpression.FieldOffset (base_access_expr, fn) :: acc' )
|
|
|
|
~f:(fun acc' (fn, _, _) ->
|
|
|
|
~init:acc fields
|
|
|
|
AccessExpression.FieldOffset (base_access_expr, fn) :: acc' )
|
|
|
|
in
|
|
|
|
~init:acc fields
|
|
|
|
base_access_expr :: flist
|
|
|
|
in
|
|
|
|
(* for struct we take the struct address, and the access_path
|
|
|
|
base_access_expr :: flist
|
|
|
|
|
|
|
|
(* for struct we take the struct address, and the access_path
|
|
|
|
to the fields one level down *)
|
|
|
|
to the fields one level down *)
|
|
|
|
|
|
|
|
| _ ->
|
|
|
|
|
|
|
|
acc )
|
|
|
|
|
|
|
|
| Typ.Tarray {elt} ->
|
|
|
|
|
|
|
|
AccessExpression.ArrayOffset (base_access_expr, elt, []) :: acc
|
|
|
|
|
|
|
|
| Typ.Tptr _ ->
|
|
|
|
|
|
|
|
base_access_expr :: AccessExpression.Dereference base_access_expr :: acc
|
|
|
|
| _ ->
|
|
|
|
| _ ->
|
|
|
|
acc )
|
|
|
|
base_access_expr :: acc )
|
|
|
|
| Typ.Tarray {elt} ->
|
|
|
|
end
|
|
|
|
AccessExpression.ArrayOffset (base_access_expr, elt, []) :: acc
|
|
|
|
|
|
|
|
| Typ.Tptr _ ->
|
|
|
|
|
|
|
|
base_access_expr :: AccessExpression.Dereference base_access_expr :: acc
|
|
|
|
|
|
|
|
| _ ->
|
|
|
|
|
|
|
|
base_access_expr :: acc )
|
|
|
|
|
|
|
|
~init:[] (Procdesc.get_locals pdesc)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
|
|
|
|
let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
|
|
|
|
(* start with empty set of uninit local vars and empty set of init formal params *)
|
|
|
|
(* start with empty set of uninit local vars and empty set of init formal params *)
|
|
|
|
let formal_map = FormalMap.make proc_desc in
|
|
|
|
let formal_map = FormalMap.make proc_desc in
|
|
|
|
let uninit_vars = get_locals tenv proc_desc in
|
|
|
|
let uninit_vars = Initial.get_locals tenv proc_desc in
|
|
|
|
let initial =
|
|
|
|
let initial =
|
|
|
|
{ RecordDomain.uninit_vars= UninitVars.of_list uninit_vars
|
|
|
|
{ RecordDomain.uninit_vars= UninitVars.of_list uninit_vars
|
|
|
|
; aliased_vars= AliasedVars.empty
|
|
|
|
; aliased_vars= AliasedVars.empty
|
|
|
|