@ -8,100 +8,9 @@
open ! IStd
module Hashtbl = Caml . Hashtbl
open ModelTables
module L = Logging
(* * Module for standard library models. *)
(* * Module for inference of parameter and return annotations. *)
module Inference = struct
let enabled = false
let get_dir () = Filename . concat Config . results_dir " eradicate "
let field_get_dir_fname fn =
let fname = Typ . Fieldname . to_string fn in
( get_dir () , fname )
let field_is_marked fn =
let dir , fname = field_get_dir_fname fn in
DB . read_file_with_lock dir fname < > None
let proc_get_ret_dir_fname pname =
let fname = Typ . Procname . to_filename pname ^ " _ret " in
( get_dir () , fname )
let proc_get_param_dir_fname pname =
let fname = Typ . Procname . to_filename pname ^ " _params " in
( get_dir () , fname )
let update_count_str s_old =
let n =
if String . is_empty s_old then 0
else try int_of_string s_old with Failure _ -> L . die InternalError " int_of_string %s " s_old
in
string_of_int ( n + 1 )
let update_boolvec_str s_ size index bval =
let s = if String . is_empty s_ then Bytes . make size '0' else Bytes . of_string s_ in
Bytes . set s index ( if bval then '1' else '0' ) ;
Bytes . to_string s
let mark_file update_str dir fname =
DB . update_file_with_lock dir fname update_str ;
match DB . read_file_with_lock dir fname with
| Some buf ->
L . internal_error " Read %s: %s@. " fname buf
| None ->
L . internal_error " Read %s: None@. " fname
let mark_file_count = mark_file update_count_str
(* * Mark the field @Nullable indirectly by writing to a global file. *)
let field_add_nullable_annotation fn =
let dir , fname = field_get_dir_fname fn in
mark_file_count dir fname
(* * Mark the return type @Nullable indirectly by writing to a global file. *)
let proc_mark_return_nullable pn =
let dir , fname = proc_get_ret_dir_fname pn in
mark_file_count dir fname
(* * Return true if the return type is marked @Nullable in the global file *)
let proc_return_is_marked pname =
let dir , fname = proc_get_ret_dir_fname pname in
DB . read_file_with_lock dir fname < > None
(* * Mark the n-th parameter @Nullable indirectly by writing to a global file. *)
let proc_add_parameter_nullable pn n tot =
let dir , fname = proc_get_param_dir_fname pn in
let update_str s = update_boolvec_str s tot n true in
mark_file update_str dir fname
(* * Return None if the parameters are not marked, or a vector of marked parameters *)
let proc_parameters_marked pn =
let dir , fname = proc_get_param_dir_fname pn in
match DB . read_file_with_lock dir fname with
| None ->
None
| Some buf ->
let boolvec = ref [] in
String . iter ~ f : ( fun c -> boolvec := Char . equal c '1' :: ! boolvec ) buf ;
Some ( List . rev ! boolvec )
end
(* Inference *)
let match_method_name pn name =
match pn with
| Typ . Procname . Java pn_java ->
@ -123,21 +32,6 @@ let get_modelled_annotated_signature proc_attributes =
let proc_name = proc_attributes . ProcAttributes . proc_name in
let annotated_signature = AnnotatedSignature . get proc_attributes in
let proc_id = Typ . Procname . to_unique_id proc_name in
let infer_parameters ann_sig =
let mark_par =
if Inference . enabled then Inference . proc_parameters_marked proc_name else None
in
match mark_par with
| None ->
ann_sig
| Some bs ->
let mark = ( false , bs ) in
AnnotatedSignature . mark proc_name AnnotatedSignature . Nullable ann_sig mark
in
let infer_return ann_sig =
let mark_r = Inference . enabled && Inference . proc_return_is_marked proc_name in
if mark_r then AnnotatedSignature . mark_return AnnotatedSignature . Nullable ann_sig else ann_sig
in
let lookup_models_nullable ann_sig =
try
let mark = Hashtbl . find annotated_table_nullable proc_id in
@ -150,8 +44,7 @@ let get_modelled_annotated_signature proc_attributes =
AnnotatedSignature . mark proc_name AnnotatedSignature . Present ann_sig mark
with Caml . Not_found -> ann_sig
in
annotated_signature | > lookup_models_nullable | > lookup_models_present | > infer_return
| > infer_parameters
annotated_signature | > lookup_models_nullable | > lookup_models_present
(* * Return true when the procedure has been modelled for nullable. *)
Jeremy Dubreil
6 years ago
committed by
Facebook Github Bot