@ -8,7 +8,6 @@
open ! IStd
module F = Format
open PolyVariantEqual
module Stats = struct
type t =
@ -96,14 +95,6 @@ let get_err_log summary = summary.err_log
let get_loc summary = ( get_attributes summary ) . ProcAttributes . loc
type cache = t Typ . Procname . Hash . t
let cache : cache = Typ . Procname . Hash . create 128
let clear_cache () = Typ . Procname . Hash . clear cache
let remove_from_cache pname = Typ . Procname . Hash . remove cache pname
let pp_errlog fmt err_log =
F . fprintf fmt " ERRORS: @[<h>%a@]@ \n %! " Errlog . pp_errors err_log ;
F . fprintf fmt " WARNINGS: @[<h>%a@] " Errlog . pp_warnings err_log
@ -139,142 +130,155 @@ let pp_html source fmt summary =
F . fprintf fmt " </LISTING>@ \n "
(* * Add the summary to the table for the given function *)
let add ( proc_name : Typ . Procname . t ) ( summary : t ) : unit =
Typ . Procname . Hash . replace cache proc_name summary
module OnDisk = struct
open PolyVariantEqual
type cache = t Typ . Procname . Hash . t
let specs_filename pname =
let pname_file = Typ . Procname . to_filename pname in
pname_file ^ Config . specs_files_suffix
let cache : cache = Typ . Procname . Hash . create 128
let clear_cache () = Typ . Procname . Hash . clear cache
(* * Return the path to the .specs file for the given procedure in the current results directory *)
let specs_filename_of_procname pname =
DB . Results_dir . path_to_filename DB . Results_dir . Abs_root
[ Config . specs_dir_name ; specs_filename pname ]
let remove_from_cache pname = Typ . Procname . Hash . remove cache pname
(* * Add the summary to the table for the given function *)
let add ( proc_name : Typ . Procname . t ) ( summary : t ) : unit =
Typ . Procname . Hash . replace cache proc_name summary
(* * paths to the .specs file for the given procedure in the current spec libraries *)
let specs_library_filename specs_dir pname =
DB . filename_from_string ( Filename . concat specs_dir ( specs_filename pname ) )
let specs_filename pname =
let pname_file = Typ . Procname . to_filename pname in
pname_file ^ Config . specs_files_suffix
(* * paths to the .specs file for the given procedure in the models folder *)
let specs_models_filename pname =
DB . filename_from_string ( Filename . concat Config . models_dir ( specs_filename pname ) )
(* * Return the path to the .specs file for the given procedure in the current results directory *)
let specs_filename_of_procname pname =
DB . Results_dir . path_to_filename DB . Results_dir . Abs_root
[ Config . specs_dir_name ; specs_filename pname ]
let has_model pname = Sys . file_exists ( DB . filename_to_string ( specs_models_filename pname ) ) = ` Yes
let summary_serializer : t Serialization . serializer =
Serialization . create_serializer Serialization . Key . summary
(* * paths to the .specs file for the given procedure in the current spec libraries *)
let specs_library_filename specs_dir pname =
DB . filename_from_string ( Filename . concat specs_dir ( specs_filename pname ) )
(* * Load procedure summary from the given file *)
let load_from_file specs_file = Serialization . read_from_file summary_serializer specs_file
(* * paths to the .specs file for the given procedure in the models folder *)
let specs_models_filename pname =
DB . filename_from_string ( Filename . concat Config . models_dir ( specs_filename pname ) )
(* * Load procedure summary for the given procedure name and update spec table *)
let load_summary_to_spec_table =
let rec or_load_summary_libs specs_dirs proc_name summ_opt =
match ( summ_opt , specs_dirs ) with
| Some _ , _ | _ , [] ->
summ_opt
| None , specs_dir :: specs_dirs ->
load_from_file ( specs_library_filename specs_dir proc_name )
| > or_load_summary_libs specs_dirs proc_name
in
let load_summary_ziplibs zip_specs_filename =
let zip_specs_path = Filename . concat Config . specs_dir_name zip_specs_filename in
ZipLib . load summary_serializer zip_specs_path
in
let or_from f_load f_filenames proc_name summ_opt =
match summ_opt with Some _ -> summ_opt | None -> f_load ( f_filenames proc_name )
in
fun proc_name ->
let summ_opt =
load_from_file ( specs_filename_of_procname proc_name )
| > or_from load_from_file specs_models_filename proc_name
| > or_from load_summary_ziplibs specs_filename proc_name
| > or_load_summary_libs Config . specs_library proc_name
in
Option . iter ~ f : ( add proc_name ) summ_opt ;
summ_opt
let has_model pname =
Sys . file_exists ( DB . filename_to_string ( specs_models_filename pname ) ) = ` Yes
let get proc_name =
try Some ( Typ . Procname . Hash . find cache proc_name )
with Caml . Not_found -> load_summary_to_spec_table proc_name
let summary_serializer : t Serialization . serializer =
Serialization . create_serializer Serialization . Key . summary
(* * Check if the procedure is from a library:
(* * Load procedure summary from the given file *)
let load_from_file specs_file = Serialization . read_from_file summary_serializer specs_file
(* * Load procedure summary for the given procedure name and update spec table *)
let load_summary_to_spec_table =
let rec or_load_summary_libs specs_dirs proc_name summ_opt =
match ( summ_opt , specs_dirs ) with
| Some _ , _ | _ , [] ->
summ_opt
| None , specs_dir :: specs_dirs ->
load_from_file ( specs_library_filename specs_dir proc_name )
| > or_load_summary_libs specs_dirs proc_name
in
let load_summary_ziplibs zip_specs_filename =
let zip_specs_path = Filename . concat Config . specs_dir_name zip_specs_filename in
ZipLib . load summary_serializer zip_specs_path
in
let or_from f_load f_filenames proc_name summ_opt =
match summ_opt with Some _ -> summ_opt | None -> f_load ( f_filenames proc_name )
in
fun proc_name ->
let summ_opt =
load_from_file ( specs_filename_of_procname proc_name )
| > or_from load_from_file specs_models_filename proc_name
| > or_from load_summary_ziplibs specs_filename proc_name
| > or_load_summary_libs Config . specs_library proc_name
in
Option . iter ~ f : ( add proc_name ) summ_opt ;
summ_opt
let get proc_name =
match Typ . Procname . Hash . find cache proc_name with
| summary ->
Some summary
| exception Caml . Not_found ->
load_summary_to_spec_table proc_name
(* * Check if the procedure is from a library:
It's not defined , and there is no spec file for it . * )
let proc_is_library proc_attributes =
if not proc_attributes . ProcAttributes . is_defined then
match get proc_attributes . ProcAttributes . proc_name with None -> true | Some _ -> false
else false
let proc_is_library proc_attributes =
if not proc_attributes . ProcAttributes . is_defined then
match get proc_attributes . ProcAttributes . proc_name with None -> true | Some _ -> false
else false
(* * Try to find the attributes for a defined proc.
(* * Try to find the attributes for a defined proc.
First look at specs ( to get attributes computed by analysis )
then look at the attributes table .
If no attributes can be found , return None .
* )
let proc_resolve_attributes proc_name =
match get proc_name with
| Some summary ->
Some ( get_attributes summary )
| None ->
Attributes . load proc_name
(* * Save summary for the procedure into the spec database *)
let store ( summ : t ) =
let final_summary = { summ with status = Status . Analyzed } in
let proc_name = get_proc_name final_summary in
(* Make sure the summary in memory is identical to the saved one *)
add proc_name final_summary ;
Serialization . write_to_file summary_serializer
( specs_filename_of_procname proc_name )
~ data : final_summary
let init_summary proc_desc =
let summary =
{ sessions = ref 0
; payloads = Payloads . empty
; stats = Stats . empty
; status = Status . Pending
; proc_desc
; err_log = Errlog . empty ()
; callee_pnames = Typ . Procname . Set . empty }
in
Typ . Procname . Hash . replace cache ( Procdesc . get_proc_name proc_desc ) summary ;
summary
let dummy =
let dummy_attributes =
ProcAttributes . default ( SourceFile . invalid _ _ FILE__ ) Typ . Procname . empty_block
in
let dummy_proc_desc = Procdesc . from_proc_attributes dummy_attributes in
init_summary dummy_proc_desc
(* * Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
let reset proc_desc = init_summary proc_desc
let reset_all ~ filter () =
let reset proc_name =
let filename = specs_filename_of_procname proc_name in
Serialization . read_from_file summary_serializer filename
| > Option . iter ~ f : ( fun summary ->
let blank_summary = reset summary . proc_desc in
Serialization . write_to_file summary_serializer filename ~ data : blank_summary )
in
Procedures . get_all ~ filter () | > List . iter ~ f : reset
let proc_resolve_attributes proc_name =
match get proc_name with
| Some summary ->
Some ( get_attributes summary )
| None ->
Attributes . load proc_name
(* * Save summary for the procedure into the spec database *)
let store ( summ : t ) =
let final_summary = { summ with status = Status . Analyzed } in
let proc_name = get_proc_name final_summary in
(* Make sure the summary in memory is identical to the saved one *)
add proc_name final_summary ;
Serialization . write_to_file summary_serializer
( specs_filename_of_procname proc_name )
~ data : final_summary
let reset proc_desc =
let summary =
{ sessions = ref 0
; payloads = Payloads . empty
; stats = Stats . empty
; status = Status . Pending
; proc_desc
; err_log = Errlog . empty ()
; callee_pnames = Typ . Procname . Set . empty }
in
Typ . Procname . Hash . replace cache ( Procdesc . get_proc_name proc_desc ) summary ;
summary
let dummy =
let dummy_attributes =
ProcAttributes . default ( SourceFile . invalid _ _ FILE__ ) Typ . Procname . empty_block
in
let dummy_proc_desc = Procdesc . from_proc_attributes dummy_attributes in
reset dummy_proc_desc
let reset_all ~ filter () =
let reset proc_name =
let filename = specs_filename_of_procname proc_name in
Serialization . read_from_file summary_serializer filename
| > Option . iter ~ f : ( fun summary ->
let blank_summary = reset summary . proc_desc in
Serialization . write_to_file summary_serializer filename ~ data : blank_summary )
in
Procedures . get_all ~ filter () | > List . iter ~ f : reset
end
module SummaryValue = struct
type nonrec t = t option