@ -20,6 +20,31 @@ let is_whitelisted (pname : Procname.t) =
Procname . get_qualifiers pname
| > QualifiedCppName . match_qualifiers methods_whitelist
type siof_model = {
qual_name : string ; (* * ( fuzzy ) name of the method, eg "std::ios_base::Init::Init" *)
initialized_globals : string list ; (* * names of variables that are guaranteed to be initialized
once the method is executed , eg [ " std::cerr " ] * )
}
let parse_siof_model ( qual_name , initialized_globals ) = { qual_name ; initialized_globals ; }
let models = List . map ~ f : parse_siof_model [
( " std::ios_base::Init::Init " , [
" std::cerr " ; " std::wcerr " ;
" std::cin " ; " std::wcin " ;
" std::clog " ; " std::wclog " ;
" std::cout " ; " std::wcout " ;
] ) ;
]
let is_modelled =
let models_matcher =
List . map models ~ f : ( fun { qual_name } -> qual_name )
| > QualifiedCppName . quals_matcher_of_fuzzy_qual_names in
fun pname ->
Procname . get_qualifiers pname
| > QualifiedCppName . match_qualifiers models_matcher
module Summary = Summary . Make ( struct
type summary = SiofDomain . astate
@ -38,7 +63,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let is_compile_time_constructed pdesc pv =
let init_pname = Pvar . get_initializer_pname pv in
match Option . bind init_pname ( Summary . read_summary pdesc ) with
| Some Domain . Bottom ->
| Some ( Domain . BottomSiofTrace . Bottom , _ ) ->
(* we analyzed the initializer for this global and found that it doesn't require any runtime
initialization so cannot participate in SIOF * )
true
@ -57,16 +82,30 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| > IList . map ( fun v -> ( v , loc ) ) in
GlobalsAccesses . of_list globals_accesses
let filter_global_accesses initialized globals =
let initialized_matcher =
Domain . VarNames . elements initialized
| > QualifiedCppName . quals_matcher_of_fuzzy_qual_names in
(* gvar \notin initialized, up to some fuzzing *)
let f ( gvar , _ ) =
QualifiedCppName . qualifiers_of_qual_name ( Pvar . to_string gvar )
| > Fn . non ( QualifiedCppName . match_qualifiers initialized_matcher ) in
GlobalsAccesses . filter f globals
let add_globals astate outer_loc globals =
if GlobalsAccesses . is_empty globals then
astate
else
let trace = match astate with
| Domain . Bottom -> SiofTrace . empty
| Domain . NonBottom t -> t in
let trace = match fst astate with
| Domain . BottomSiofTrace . Bottom -> SiofTrace . empty
| Domain . BottomSiofTrace . NonBottom t -> t in
(* filter out variables that are known to be already initialized *)
let non_init_globals =
let initialized = snd astate in
filter_global_accesses initialized globals in
let globals_trace =
SiofTrace . add_sink ( SiofTrace . make_access globals outer_loc ) trace in
Domain . NonBottom globals_trace
SiofTrace . add_sink ( SiofTrace . make_access non_init_ globals outer_loc ) trace in
( Domain . BottomSiofTrace . NonBottom globals_trace , snd astate )
let add_params_globals astate pdesc call_loc params =
IList . map ( fun ( e , _ ) -> get_globals pdesc call_loc e ) params
@ -74,7 +113,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| > add_globals astate ( Procdesc . get_loc pdesc )
let at_least_nonbottom =
Domain . join ( Domain . NonBottom SiofTrace . empty )
Domain . join ( ( Domain . BottomSiofTrace . NonBottom SiofTrace . empty ) , Domain . VarNames . empty )
let exec_instr astate { ProcData . pdesc ; } _ ( instr : Sil . instr ) =
match instr with
@ -85,20 +124,40 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
get_globals pdesc loc exp | > add_globals astate proc_loc
| Call ( _ , Const ( Cfun callee_pname ) , _ , _ , _ ) when is_whitelisted callee_pname ->
at_least_nonbottom astate
| Call ( _ , Const ( Cfun callee_pname ) , _ , _ , _ ) when is_modelled callee_pname ->
let init = List . find_map_exn models
~ f : ( fun { qual_name ; initialized_globals } ->
if QualifiedCppName . quals_matcher_of_fuzzy_qual_names [ qual_name ]
| > Fn . flip QualifiedCppName . match_qualifiers
( Procname . get_qualifiers callee_pname ) then
Some initialized_globals
else
None ) in
Domain . join astate ( Domain . BottomSiofTrace . NonBottom SiofTrace . empty ,
Domain . VarNames . of_list init )
| Call ( _ , Const ( Cfun callee_pname ) , _ :: params_without_self , loc , _ )
when Procname . is_c_method callee_pname && Procname . is_constructor callee_pname
&& Procname . is_constexpr callee_pname ->
add_params_globals astate pdesc loc params_without_self
| Call ( _ , Const ( Cfun callee_pname ) , params , loc , _ ) ->
let callsite = CallSite . make callee_pname loc in
let callee_globals =
match Summary . read_summary pdesc callee_pname with
| Some ( Domain . NonBottom trace ) ->
Domain . NonBottom ( SiofTrace . with_callsite trace callsite )
| None | Some Domain . Bottom ->
Domain . Bottom in
let callee_astate = match Summary . read_summary pdesc callee_pname with
| Some ( Domain . BottomSiofTrace . NonBottom trace , initialized_globals ) ->
let trace_without_initialized_globals =
let sinks_with_non_init_globals =
SiofTrace . Sinks . filter ( fun sink ->
filter_global_accesses ( snd astate ) ( SiofTrace . Sink . kind sink )
| > Fn . non GlobalsAccesses . is_empty ) ( SiofTrace . sinks trace ) in
SiofTrace . update_sinks trace sinks_with_non_init_globals in
( Domain . BottomSiofTrace . NonBottom
( SiofTrace . with_callsite trace_without_initialized_globals callsite ) ,
initialized_globals )
| Some ( ( Domain . BottomSiofTrace . Bottom , _ ) as astate ) ->
astate
| None ->
( Domain . BottomSiofTrace . Bottom , Domain . VarNames . empty ) in
add_params_globals astate pdesc loc params
| > Domain . join callee_globals
| > Domain . join callee_ astate
| >
(* make sure it's not Bottom: we made a function call so this needs initialization *)
at_least_nonbottom
@ -130,7 +189,7 @@ let report_siof trace pdesc gname loc =
attrs . ProcAttributes . translation_unit in
let trace_of_pname pname =
match Summary . read_summary pdesc pname with
| Some ( SiofDomain . NonBottom summary ) -> summary
| Some ( SiofDomain . BottomSiofTrace . NonBottom summary , _ ) -> summary
| _ -> SiofTrace . empty in
let report_one_path ( passthroughs , path ) =
@ -166,7 +225,7 @@ let report_siof trace pdesc gname loc =
| > IList . iter report_one_path
let siof_check pdesc gname = function
| Some ( SiofDomain . NonBottom post ) ->
| Some ( ( SiofDomain . BottomSiofTrace . NonBottom post , _ ) ) ->
let attrs = Procdesc . get_attributes pdesc in
let all_globals = SiofTrace . Sinks . fold
( fun sink -> GlobalsAccesses . union ( SiofTrace . Sink . kind sink ) )
@ -176,11 +235,13 @@ let siof_check pdesc gname = function
attrs . ProcAttributes . translation_unit in
if GlobalsAccesses . exists ( is_foreign tu_opt ) all_globals then
report_siof post pdesc gname attrs . ProcAttributes . loc ;
| Some SiofDomain . Bottom | None ->
| Some ( SiofDomain . BottomSiofTrace . Bottom , _ ) | None ->
()
let compute_post proc_data =
Analyzer . compute_post proc_data ~ initial : SiofDomain . Bottom | > Option . map ~ f : SiofDomain . normalize
Analyzer . compute_post proc_data
~ initial : ( SiofDomain . BottomSiofTrace . Bottom , SiofDomain . VarNames . empty )
| > Option . map ~ f : SiofDomain . normalize
let checker ( { Callbacks . proc_desc ; } as callback ) =
let post =