[eradicate][ondemand] Skeleton of on-demand analysis for Eradicate.

master
Cristiano Calcagno 9 years ago
parent 28f5025862
commit 0f8c3e7974

@ -0,0 +1,110 @@
(*
* Copyright (c) 2015 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
(** Module for on-demand analysis. *)
module L = Logging
module F = Format
open Utils
let trace = false
let enabled () = false
type analyze_proc = Procname.t -> unit
type get_proc_desc = Procname.t -> Cfg.Procdesc.t option
let analyze_proc_fun = ref None
let set_analyze_proc (analyze_proc : analyze_proc) =
analyze_proc_fun := Some analyze_proc
let unset_analyze_prop () =
analyze_proc_fun := None
let do_analysis (get_proc_desc : get_proc_desc) curr_pname proc_name =
if trace then L.stderr "do_analysis %a -> %a@." Procname.pp curr_pname Procname.pp proc_name;
let really_do_analysis analyze_proc proc_desc =
L.stderr "really_do_analysis@.";
let preprocess () =
let attributes_opt =
Some (Cfg.Procdesc.get_attributes proc_desc) in
let call_graph =
let cg = Cg.create () in
Cg.add_node cg proc_name;
cg in
Specs.reset_summary call_graph proc_name attributes_opt;
Specs.set_status proc_name Specs.ACTIVE in
let postprocess () =
let summary = Specs.get_summary_unsafe proc_name in
let summary' =
{ summary with
Specs.status = Specs.INACTIVE;
timestamp = summary.Specs.timestamp + 1 } in
Specs.add_summary proc_name summary';
Checkers.ST.store_summary proc_name in
try
preprocess ();
analyze_proc proc_name;
postprocess ()
with e ->
L.stderr "ONDEMAND EXCEPTION %a %s %s@."
Procname.pp proc_name
(Printexc.to_string e)
(Printexc.get_backtrace ());
raise e in
let currently_analyzed =
Specs.summary_exists proc_name &&
Specs.is_active proc_name in
let already_analyzed = match Specs.get_summary proc_name with
| Some summary ->
Specs.get_timestamp summary > 0
| None ->
false in
(* The procedure to be analyzed is in the same file as the current one. *)
let same_file proc_desc =
match get_proc_desc curr_pname with
| Some curr_pdesc ->
(Cfg.Procdesc.get_loc curr_pdesc).Location.file
=
(Cfg.Procdesc.get_loc proc_desc).Location.file
| None -> false in
match !analyze_proc_fun, get_proc_desc proc_name with
| Some analyze_proc, Some proc_desc
when enabled () &&
Cfg.Procdesc.is_defined proc_desc && (* we have the implementation *)
not currently_analyzed && (* avoid infinite loops *)
not already_analyzed && (* avoid re-analysis of the same procedure *)
same_file proc_desc (* clusters don't have enough info for other files *) ->
really_do_analysis analyze_proc proc_desc
| _ ->
if trace then L.stderr "skipping@."
(** Mark the return type @Nullable by modifying the spec. *)
let proc_add_return_nullable curr_pname =
let summary = Specs.get_summary_unsafe curr_pname in
let proc_attributes = Specs.get_attributes summary in
let method_annotation = proc_attributes.ProcAttributes.method_annotation in
let method_annotation' = Annotations.method_annotation_mark_return
Annotations.Nullable method_annotation in
let proc_attributes' =
{ proc_attributes with
ProcAttributes.method_annotation = method_annotation' } in
let summary' =
{ summary with
Specs.attributes = proc_attributes' } in
Specs.add_summary curr_pname summary'

@ -0,0 +1,31 @@
(*
* Copyright (c) 2015 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
(** Module for on-demand analysis. *)
type analyze_proc = Procname.t -> unit
type get_proc_desc = Procname.t -> Cfg.Procdesc.t option
(** do_analysis get_proc_desc curr_pname proc_name
performs an on-demand analysis of proc_name
triggered during the analysis of curr_pname. *)
val do_analysis : get_proc_desc -> Procname.t -> Procname.t -> unit
(** Check if on-demand is currently active. *)
val enabled : unit -> bool
(** Mark the return type @Nullable by modifying the spec. *)
val proc_add_return_nullable : Procname.t -> unit
(** Set the function to be used to perform on-demand analysis. *)
val set_analyze_proc : analyze_proc -> unit
(** Unset the function to be used to perform on-demand analysis. *)
val unset_analyze_prop : unit -> unit

@ -32,6 +32,19 @@ let generate_keys () =
gen (), gen (), gen (), gen (), gen (), gen ()
(** Retry the function while an exception filtered is thrown,
or until the timeout in seconds expires. *)
let retry_exception timeout catch_exn f x =
let init_time = Unix.gettimeofday () in
let expired () =
Unix.gettimeofday () -. init_time >= timeout in
let rec retry () =
try f x with
| e when catch_exn e && not (expired ()) ->
retry () in
retry ()
let create_serializer (key : key) : 'a serializer =
let match_data ((key': key), (version': int), (value: 'a)) source_msg =
if key <> key' then
@ -50,13 +63,22 @@ let create_serializer (key : key) : 'a serializer =
match_data (Marshal.from_string str 0) "string"
with Sys_error s -> None in
let from_file (_fname : DB.filename) : 'a option =
try
let fname = DB.filename_to_string _fname in
let inc = open_in_bin fname in
let value_option = match_data (Marshal.from_channel inc) fname in
close_in inc;
value_option
with Sys_error s -> None in
let read () =
try
let fname = DB.filename_to_string _fname in
let inc = open_in_bin fname in
let value_option = match_data (Marshal.from_channel inc) fname in
close_in inc;
value_option
with
| Sys_error s -> None in
let timeout = 1.0 in
let catch_exn = function
| End_of_file -> true
| _ -> false in
(* Retry to read for 1 second in case of end of file, *)
(* which indicates that another process is writing the same file. *)
retry_exception timeout catch_exn read () in
let to_file (fname : DB.filename) (value : 'a) =
let outc = open_out_bin (DB.filename_to_string fname) in
Marshal.to_channel outc (key, version, value) [];

@ -640,18 +640,19 @@ let proc_resolve_attributes get_proc_desc proc_name =
| Some summary ->
Some summary.attributes
| None -> None in
match from_proc_desc () with
match from_specs () with
| Some attributes ->
if attributes.ProcAttributes.is_defined
then Some attributes
else begin
match from_specs () with
match from_proc_desc () with
| Some attributes' ->
Some attributes'
| None -> Some attributes
| None ->
Some attributes
end
| None ->
from_specs ()
from_proc_desc ()
(** Like proc_resolve_attributes but start from a proc_desc. *)
let pdesc_resolve_attributes proc_desc =

@ -155,8 +155,6 @@ let ia_is ann ia = match ann with
| Nullable -> ia_is_nullable ia
| Present -> ia_is_present ia
type get_method_annotation = Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation
(** Get a method signature with annotations from a proc_attributes. *)
let get_annotated_signature proc_attributes : annotated_signature =
@ -270,13 +268,19 @@ let annotated_signature_mark proc_name ann asig (b, bs) =
{ ret = ret'; params = params'}
(** Mark the return of the annotated signature with the given annotation. *)
let annotated_signature_mark_return proc_name ann asig =
let annotated_signature_mark_return ann asig =
let ia, t = asig.ret in
let ret' = mark_ia ann ia true, t in
{ asig with ret = ret'}
(** Mark the return of the annotated signature @Strict. *)
let annotated_signature_mark_return_strict proc_name asig =
let annotated_signature_mark_return_strict asig =
let ia, t = asig.ret in
let ret' = mark_ia_strict ia true, t in
{ asig with ret = ret'}
(** Mark the return of the method_annotation with the given annotation. *)
let method_annotation_mark_return ann method_annotation =
let ia_ret, params = method_annotation in
let ia_ret' = mark_ia ann ia_ret true in
ia_ret', params

@ -34,16 +34,14 @@ val annotated_signature_mark :
(** Mark the return of the annotated signature with the given annotation. *)
val annotated_signature_mark_return :
Procname.t -> annotation -> annotated_signature -> annotated_signature
annotation -> annotated_signature -> annotated_signature
(** Mark the return of the annotated signature @Strict. *)
val annotated_signature_mark_return_strict :
Procname.t -> annotated_signature -> annotated_signature
annotated_signature -> annotated_signature
val equal : annotated_signature -> annotated_signature -> bool
type get_method_annotation = Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation
(** Get a method signature with annotations from a proc_attributes. *)
val get_annotated_signature : ProcAttributes.t -> annotated_signature
@ -76,6 +74,10 @@ val ma_has_annotation_with : Sil.method_annotation -> (Sil.annotation -> bool) -
val ma_iter : (Sil.annotation -> unit) -> Sil.method_annotation -> unit
(** Mark the return of the method_annotation with the given annotation. *)
val method_annotation_mark_return :
annotation -> Sil.method_annotation -> Sil.method_annotation
(** Add the annotation to the item_annotation. *)
val mk_ia : annotation -> Sil.item_annotation -> Sil.item_annotation

@ -71,7 +71,8 @@ struct
let callback1
find_canonical_duplicate calls_this checks get_proc_desc idenv tenv curr_pname
curr_pdesc annotated_signature linereader proc_loc : bool * 'a TypeState.t option =
curr_pdesc annotated_signature linereader proc_loc
: bool * Extension.extension TypeState.t option =
let mk_pvar s = Sil.mk_pvar (Mangled.from_string s) curr_pname in
let add_formal typestate (s, ia, typ) =
let pvar = mk_pvar s in
@ -154,7 +155,16 @@ struct
try Cfg.NodeSet.min_elt duplicate_nodes with
| Not_found -> node in
let typecheck_proc do_checks idenv_pn pname pdesc ann_sig loc =
let typecheck_proc do_checks pname pdesc proc_details_opt =
let ann_sig, loc, idenv_pn = match proc_details_opt with
| Some (ann_sig, loc, idenv_pn) ->
(ann_sig, loc, idenv_pn)
| None ->
let ann_sig =
Models.get_modelled_annotated_signature (Cfg.Procdesc.get_attributes pdesc) in
let loc = Cfg.Procdesc.get_loc pdesc in
let idenv_pn = Idenv.create_from_idenv idenv pdesc in
(ann_sig, loc, idenv_pn) in
let checks', calls_this' =
if do_checks then checks, calls_this
else
@ -215,11 +225,7 @@ struct
(** Get the final typestates of all the initializers. *)
let final_typestates = ref [] in
let get_final_typestate (pname, pdesc) =
let ann_sig =
Models.get_modelled_annotated_signature (Cfg.Procdesc.get_attributes pdesc) in
let loc = Cfg.Procdesc.get_loc pdesc in
let idenv_pn = Idenv.create_from_idenv idenv pdesc in
match typecheck_proc false idenv_pn pname pdesc ann_sig loc with
match typecheck_proc false pname pdesc None with
| _, Some final_typestate ->
final_typestates := (pname, final_typestate) :: !final_typestates
| _, None -> () in
@ -277,7 +283,6 @@ struct
curr_pname
curr_pdesc
start_node
typestate
Initializers.final_initializer_typestates_lazy
Initializers.final_constructor_typestates_lazy
proc_loc
@ -292,7 +297,7 @@ struct
TypeErr.reset ();
let calls_this, final_typestate_opt =
typecheck_proc true idenv curr_pname curr_pdesc annotated_signature proc_loc in
typecheck_proc true curr_pname curr_pdesc (Some (annotated_signature, proc_loc, idenv)) in
do_final_typestate final_typestate_opt calls_this;
if checks.TypeCheck.eradicate then
EradicateChecks.check_overridden_annotations
@ -315,19 +320,7 @@ struct
begin
let annotated_signature =
Models.get_modelled_annotated_signature (Specs.pdesc_resolve_attributes proc_desc) in
if (Specs.pdesc_resolve_attributes proc_desc).ProcAttributes.is_abstract then
begin
if Models.infer_library_return &&
EradicateChecks.classify_procedure (Cfg.Procdesc.get_attributes proc_desc) = "L"
then
(let ret_is_nullable = (* get the existing annotation *)
let ia, _ = annotated_signature.Annotations.ret in
Annotations.ia_is_nullable ia in
EradicateChecks.pp_inferred_return_annotation ret_is_nullable proc_name);
Some annotated_signature
end
else
Some annotated_signature
Some annotated_signature
end in
match filter_special_cases () with
| None -> ()
@ -375,26 +368,30 @@ module Main =
Build(EmptyExtension)
(** Eradicate checker for Java @Nullable annotations. *)
let callback_eradicate all_procs get_proc_desc idenv tenv proc_name1 proc_desc1 =
let callback_eradicate all_procs get_proc_desc idenv tenv proc_name proc_desc =
let checks =
{
TypeCheck.eradicate = true;
check_extension = false;
check_ret_type = [];
} in
Main.callback checks all_procs get_proc_desc idenv tenv proc_name1 proc_desc1
let _ondemand pname =
match get_proc_desc pname with
| None -> ()
| Some pdesc ->
let idenv_pname = Idenv.create_from_idenv idenv pdesc in
Main.callback checks all_procs get_proc_desc idenv_pname tenv pname pdesc in
Ondemand.set_analyze_proc _ondemand;
Main.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc;
Ondemand.unset_analyze_prop ()
(** Call the given check_return_type at the end of every procedure. *)
let callback_check_return_type check_return_type all_procs
get_proc_desc idenv tenv proc_name1 proc_desc1 =
get_proc_desc idenv tenv proc_name proc_desc =
let checks =
{
TypeCheck.eradicate = false;
check_extension = false;
check_ret_type = [check_return_type];
} in
Main.callback checks all_procs get_proc_desc idenv tenv proc_name1 proc_desc1
(** Export the ability to add nullable annotations. *)
let field_add_nullable_annotation fieldname =
Models.Inference.field_add_nullable_annotation fieldname
Main.callback checks all_procs get_proc_desc idenv tenv proc_name proc_desc

@ -60,18 +60,12 @@ let classify_procedure proc_attributes =
let unique_id = Procname.to_unique_id pn in
let classification =
if Models.is_modelled_nullable pn then "M" (* modelled *)
else if Models.is_ret_library pn then "R" (* return library *)
else if Specs.proc_is_library proc_attributes then "L" (* library *)
else if not proc_attributes.ProcAttributes.is_defined then "S" (* skip *)
else if string_is_prefix "com.facebook" unique_id then "F" (* FB *)
else "?" in
classification
let pp_inferred_return_annotation is_nullable proc_name =
L.stdout "(*InferredLibraryReturnAnnotation*) %5b, \"%s\";@."
is_nullable
(Procname.to_unique_id proc_name)
let is_virtual = function
| ("this", _, _):: _ -> true
@ -248,7 +242,6 @@ let check_constructor_initialization
curr_pname
curr_pdesc
start_node
final_typestate
final_initializer_typestates
final_constructor_typestates
loc: unit =
@ -339,52 +332,56 @@ let check_return_annotation
let ret_annotated_nullable = Annotations.ia_is_nullable ret_ia in
let ret_annotated_present = Annotations.ia_is_present ret_ia in
let ret_annotated_nonnull = Annotations.ia_is_nonnull ret_ia in
let return_not_nullable =
match ret_range with
| Some (_, final_ta, _) ->
let final_nullable = TypeAnnotation.get_value Annotations.Nullable final_ta in
let final_present = TypeAnnotation.get_value Annotations.Present final_ta in
let origin_descr = TypeAnnotation.descr_origin final_ta in
let return_not_nullable =
final_nullable &&
not ret_annotated_nullable &&
not ret_implicitly_nullable &&
not (return_nonnull_silent && ret_annotated_nonnull) in
let return_value_not_present =
activate_optional_present &&
not final_present &&
ret_annotated_present in
let return_over_annotated =
not final_nullable &&
ret_annotated_nullable &&
activate_return_over_annotated in
if return_not_nullable || return_value_not_present then
begin
let ann =
if return_not_nullable then Annotations.Nullable else Annotations.Present in
if Models.Inference.enabled then Models.Inference.proc_add_return_nullable curr_pname;
report_error
find_canonical_duplicate
exit_node
(TypeErr.Return_annotation_inconsistent (ann, curr_pname, origin_descr))
None
loc curr_pname
end;
if return_over_annotated then
begin
report_error
find_canonical_duplicate
exit_node
(TypeErr.Return_over_annotated curr_pname)
None
loc curr_pname
end;
return_not_nullable
| _ ->
false in
if Models.infer_library_return &&
classify_procedure (Cfg.Procdesc.get_attributes curr_pdesc) = "L"
then pp_inferred_return_annotation return_not_nullable curr_pname
match ret_range with
| Some (_, final_ta, _) ->
let final_nullable = TypeAnnotation.get_value Annotations.Nullable final_ta in
let final_present = TypeAnnotation.get_value Annotations.Present final_ta in
let origin_descr = TypeAnnotation.descr_origin final_ta in
let return_not_nullable =
final_nullable &&
not ret_annotated_nullable &&
not ret_implicitly_nullable &&
not (return_nonnull_silent && ret_annotated_nonnull) in
let return_value_not_present =
activate_optional_present &&
not final_present &&
ret_annotated_present in
let return_over_annotated =
not final_nullable &&
ret_annotated_nullable &&
activate_return_over_annotated in
if return_not_nullable && Models.Inference.enabled then
Models.Inference.proc_add_return_nullable curr_pname;
if return_not_nullable && Ondemand.enabled () then
Ondemand.proc_add_return_nullable curr_pname;
if return_not_nullable || return_value_not_present then
begin
let ann =
if return_not_nullable then Annotations.Nullable else Annotations.Present in
report_error
find_canonical_duplicate
exit_node
(TypeErr.Return_annotation_inconsistent (ann, curr_pname, origin_descr))
None
loc curr_pname
end;
if return_over_annotated then
begin
report_error
find_canonical_duplicate
exit_node
(TypeErr.Return_over_annotated curr_pname)
None
loc curr_pname
end
| None ->
()
(** Check the receiver of a virtual call. *)
let check_call_receiver

@ -13,16 +13,9 @@ module L = Logging
(** Module for standard library models. *)
(* use library of inferred return annotations *)
let use_library = false
(* use model annotations for library functions *)
let use_models = true
(* libary functions: infer nullable annotation of return type *)
let infer_library_return = Config.from_env_variable "ERADICATE_LIBRARY"
(** Module for inference of parameter and return annotations. *)
module Inference = struct
let enabled = false
@ -105,16 +98,6 @@ let table_has_procedure table proc_name =
try ignore (Hashtbl.find table proc_id); true
with Not_found -> false
type table_t = (string, bool) Hashtbl.t
(* precomputed marshalled table of inferred return annotations. *)
let ret_library_table : table_t Lazy.t =
lazy (Hashtbl.create 1)
(*
lazy (Marshal.from_string Eradicate_library.marshalled_library_table 0)
*)
(** Return the annotated signature of the procedure, taking into account models. *)
let get_modelled_annotated_signature proc_attributes =
let proc_name = proc_attributes.ProcAttributes.proc_name in
@ -131,17 +114,10 @@ let get_modelled_annotated_signature proc_attributes =
Annotations.annotated_signature_mark proc_name Annotations.Nullable ann_sig mark in
let infer_return ann_sig =
let mark_r =
let from_library =
if use_library then
try
Hashtbl.find (Lazy.force ret_library_table) proc_id
with Not_found -> false
else false in
let from_inference = Inference.enabled &&
Inference.proc_return_is_marked proc_name in
from_library || from_inference in
Inference.enabled &&
Inference.proc_return_is_marked proc_name in
if mark_r
then Annotations.annotated_signature_mark_return proc_name Annotations.Nullable ann_sig
then Annotations.annotated_signature_mark_return Annotations.Nullable ann_sig
else ann_sig in
let lookup_models_nullable ann_sig =
if use_models then
@ -163,7 +139,7 @@ let get_modelled_annotated_signature proc_attributes =
if use_models
&& Hashtbl.mem annotated_table_strict proc_id
then
Annotations.annotated_signature_mark_return_strict proc_name ann_sig
Annotations.annotated_signature_mark_return_strict ann_sig
else
ann_sig in
@ -183,14 +159,6 @@ let is_modelled_nullable proc_name =
with Not_found -> false
else false
(** Return true when the procedure belongs to the library of inferred return annotations. *)
let is_ret_library proc_name =
if use_library && not infer_library_return then
let proc_id = Procname.to_unique_id proc_name in
try ignore (Hashtbl.find (Lazy.force ret_library_table) proc_id); true
with Not_found -> false
else false
(** Check if the procedure is one of the known Preconditions.checkNotNull. *)
let is_check_not_null proc_name =
table_has_procedure check_not_null_table proc_name

@ -561,6 +561,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
typestate (* skip othe builtins *)
| Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags)
when get_proc_desc callee_pname <> None ->
Ondemand.do_analysis get_proc_desc curr_pname callee_pname;
let callee_attributes =
match get_proc_desc callee_pname with
| Some pdesc ->

Loading…
Cancel
Save