@ -25,11 +25,12 @@ module Payload = SummaryPayload.Make (struct
let field = Payloads . Fields . buffer_overrun_analysis
let field = Payloads . Fields . buffer_overrun_analysis
end )
end )
type summary_and_formals = BufferOverrunAnalysisSummary . t * ( Pvar . t * Typ . t ) list
type get_formals = Procname . t -> ( Pvar . t * Typ . t ) list option
type get_proc_summary_and_formals = Procname . t -> summary_and_formals option
type extras =
{ get_summary : BufferOverrunAnalysisSummary . get_summary
type extras = { get_proc_summary_and_formals : get_proc_summary_and_formals ; oenv : OndemandEnv . t }
; get_formals : get_formals
; oenv : OndemandEnv . t }
module CFG = ProcCfg . NormalOneInstrPerNode
module CFG = ProcCfg . NormalOneInstrPerNode
@ -223,7 +224,7 @@ module TransferFunctions = struct
let reachable_locs = Dom . Mem . get_reachable_locs_from [] ( PowLoc . singleton loc ) from_mem in
let reachable_locs = Dom . Mem . get_reachable_locs_from [] ( PowLoc . singleton loc ) from_mem in
PowLoc . fold copy reachable_locs to_mem
PowLoc . fold copy reachable_locs to_mem
in
in
fun tenv get_ proc_ summary_and_formals exp mem ->
fun tenv get_ summary exp mem ->
Option . value_map ( Exp . get_java_class_initializer tenv exp ) ~ default : mem
Option . value_map ( Exp . get_java_class_initializer tenv exp ) ~ default : mem
~ f : ( fun ( clinit_pname , pvar , fn , field_typ ) ->
~ f : ( fun ( clinit_pname , pvar , fn , field_typ ) ->
match field_typ . Typ . desc with
match field_typ . Typ . desc with
@ -231,8 +232,7 @@ module TransferFunctions = struct
(* It copies all of the reachable values when the contents of the field are commonly
(* It copies all of the reachable values when the contents of the field are commonly
used as immutable , e . g . , values of enum . Otherwise , it copies only the size of
used as immutable , e . g . , values of enum . Otherwise , it copies only the size of
static final array . * )
static final array . * )
Option . value_map ( get_proc_summary_and_formals clinit_pname ) ~ default : mem
Option . value_map ( get_summary clinit_pname ) ~ default : mem ~ f : ( fun clinit_mem ->
~ f : ( fun ( clinit_mem , _ ) ->
let field_loc = Loc . append_field ~ typ : field_typ ( Loc . of_pvar pvar ) ~ fn in
let field_loc = Loc . append_field ~ typ : field_typ ( Loc . of_pvar pvar ) ~ fn in
if is_known_java_static_field fn then
if is_known_java_static_field fn then
copy_reachable_locs_from field_loc ~ from_mem : clinit_mem ~ to_mem : mem
copy_reachable_locs_from field_loc ~ from_mem : clinit_mem ~ to_mem : mem
@ -266,7 +266,7 @@ module TransferFunctions = struct
let exec_instr : Dom . Mem . t -> extras ProcData . t -> CFG . Node . t -> Sil . instr -> Dom . Mem . t =
let exec_instr : Dom . Mem . t -> extras ProcData . t -> CFG . Node . t -> Sil . instr -> Dom . Mem . t =
fun mem { summary ; tenv ; extras = { get_ proc_summary_and _formals; oenv = { integer_type_widths } } } node
fun mem { summary ; tenv ; extras = { get_ summary; get _formals; oenv = { integer_type_widths } } } node
instr ->
instr ->
match instr with
match instr with
| Load { id } when Ident . is_none id ->
| Load { id } when Ident . is_none id ->
@ -275,8 +275,8 @@ module TransferFunctions = struct
when Pvar . is_compile_constant pvar | | Pvar . is_ice pvar -> (
when Pvar . is_compile_constant pvar | | Pvar . is_ice pvar -> (
match Pvar . get_initializer_pname pvar with
match Pvar . get_initializer_pname pvar with
| Some callee_pname -> (
| Some callee_pname -> (
match get_ proc_ summary_and_formals callee_pname with
match get_ summary callee_pname with
| Some ( callee_mem , _ ) ->
| Some callee_mem ->
let v = Dom . Mem . find ( Loc . of_pvar pvar ) callee_mem in
let v = Dom . Mem . find ( Loc . of_pvar pvar ) callee_mem in
Dom . Mem . add_stack ( Loc . of_id id ) v mem
Dom . Mem . add_stack ( Loc . of_id id ) v mem
| None ->
| None ->
@ -298,8 +298,7 @@ module TransferFunctions = struct
mem'
mem'
| None ->
| None ->
let mem =
let mem =
if Language . curr_language_is Java then
if Language . curr_language_is Java then join_java_static_final tenv get_summary exp mem
join_java_static_final tenv get_proc_summary_and_formals exp mem
else mem
else mem
in
in
let represents_multiple_values = is_array_access_exp exp in
let represents_multiple_values = is_array_access_exp exp in
@ -374,11 +373,11 @@ module TransferFunctions = struct
in
in
exec model_env ~ ret mem
exec model_env ~ ret mem
| None -> (
| None -> (
match get_proc_summary_and_formals callee_pname with
match ( get_summary callee_pname , get_formals callee_pname ) with
| Some ( callee_exit_mem , callee_formals ) ->
| Some callee_exit_mem , Some callee_formals ->
instantiate_mem integer_type_widths ret callee_formals callee_pname params mem
instantiate_mem integer_type_widths ret callee_formals callee_pname params mem
callee_exit_mem location
callee_exit_mem location
| None ->
| _ , _ ->
(* This may happen for procedures with a biabduction model too. *)
(* This may happen for procedures with a biabduction model too. *)
L . d_printfln_escaped " /! \\ Unknown call to %a " Procname . pp callee_pname ;
L . d_printfln_escaped " /! \\ Unknown call to %a " Procname . pp callee_pname ;
if is_external callee_pname then (
if is_external callee_pname then (
@ -424,13 +423,18 @@ let extract_post = Analyzer.extract_post
let extract_state = Analyzer . extract_state
let extract_state = Analyzer . extract_state
let compute_invariant_map :
let compute_invariant_map :
Summary . t -> Tenv . t -> Typ . IntegerWidths . t -> get_proc_summary_and_formals -> invariant_map =
Summary . t
fun summary tenv integer_type_widths get_proc_summary_and_formals ->
-> Tenv . t
-> Typ . IntegerWidths . t
-> BufferOverrunAnalysisSummary . get_summary
-> get_formals
-> invariant_map =
fun summary tenv integer_type_widths get_summary get_formals ->
let pdesc = Summary . get_proc_desc summary in
let pdesc = Summary . get_proc_desc summary in
let cfg = CFG . from_pdesc pdesc in
let cfg = CFG . from_pdesc pdesc in
let pdata =
let pdata =
let oenv = OndemandEnv . mk pdesc tenv integer_type_widths in
let oenv = OndemandEnv . mk pdesc tenv integer_type_widths in
ProcData . make summary tenv { get_proc_summary_and_formals ; oenv }
ProcData . make summary tenv { get_ summary; get _formals; oenv }
in
in
let initial = Init . initial_state pdata ( CFG . start_node cfg ) in
let initial = Init . initial_state pdata ( CFG . start_node cfg ) in
Analyzer . exec_pdesc ~ do_narrowing : true ~ initial pdata
Analyzer . exec_pdesc ~ do_narrowing : true ~ initial pdata
@ -455,15 +459,17 @@ let cached_compute_invariant_map =
(* this should never happen *)
(* this should never happen *)
assert false
assert false
| None ->
| None ->
let get_proc_summary_and_formals callee_pname =
let get_summary callee_pname =
Ondemand . analyze_proc_name ~ caller_summary : summary callee_pname
| > Option . bind ~ f : Payload . of_summary
in
let get_formals callee_pname =
Ondemand . analyze_proc_name ~ caller_summary : summary callee_pname
Ondemand . analyze_proc_name ~ caller_summary : summary callee_pname
| > Option . bind ~ f : ( fun summary ->
| > Option . map ~ f : Summary . get_proc_desc
Payload . of_summary summary
| > Option . map ~ f : Procdesc . get_pvar_formals
| > Option . map ~ f : ( fun payload ->
( payload , Summary . get_proc_desc summary | > Procdesc . get_pvar_formals ) ) )
in
in
let inv_map =
let inv_map =
compute_invariant_map summary tenv integer_type_widths get_ proc_summary_and _formals
compute_invariant_map summary tenv integer_type_widths get_ summary get _formals
in
in
WeakInvMapHashTbl . add inv_map_cache ( pname , Some inv_map ) ;
WeakInvMapHashTbl . add inv_map_cache ( pname , Some inv_map ) ;
inv_map
inv_map