@ -28,37 +28,41 @@ module NodeVisitSet = Caml.Set.Make (struct
(* higher id is better *)
Procdesc . Node . compare n2 n1
let compare_distance_to_exit { node = n1 } { node = n2 } =
(* smaller means higher priority *)
let n =
match ( Procdesc . Node . get_distance_to_exit n1 , Procdesc . Node . get_distance_to_exit n2 ) with
| None , None
-> 0
| None , Some _
-> 1
| Some _ , None
-> - 1
| Some d1 , Some d2
-> (* shorter distance to exit is better *)
| None , None ->
0
| None , Some _ ->
1
| Some _ , None ->
- 1
| Some d1 , Some d2 ->
(* shorter distance to exit is better *)
Int . compare d1 d2
in
if n < > 0 then n else compare_ids n1 n2
let compare_number_of_visits x1 x2 =
let n = Int . compare x1 . visits x2 . visits in
(* visited fewer times is better *)
if n < > 0 then n else compare_distance_to_exit x1 x2
let compare x1 x2 =
if ! Config . footprint then
match Config . worklist_mode with
| 0
-> compare_ids x1 . node x2 . node
| 1
-> compare_distance_to_exit x1 x2
| _
-> compare_number_of_visits x1 x2
| 0 ->
compare_ids x1 . node x2 . node
| 1 ->
compare_distance_to_exit x1 x2
| _ ->
compare_number_of_visits x1 x2
else compare_ids x1 . node x2 . node
end )
(* * Table for the results of the join operation on nodes. *)
@ -79,6 +83,7 @@ end = struct
try Hashtbl . find table i
with Not_found -> Paths . PathSet . empty
let add table i dset = Hashtbl . replace table i dset
end
@ -98,6 +103,7 @@ module Worklist = struct
; todo_set = NodeVisitSet . empty
; visit_map = Procdesc . NodeMap . empty }
let is_empty ( wl : t ) : bool = NodeVisitSet . is_empty wl . todo_set
let add ( wl : t ) ( node : Procdesc . Node . t ) : unit =
@ -108,6 +114,7 @@ module Worklist = struct
in
wl . todo_set <- NodeVisitSet . add { node ; visits } wl . todo_set
(* * remove the minimum element from the worklist, and increase its number of visits *)
let remove ( wl : t ) : Procdesc . Node . t =
try
@ -119,6 +126,7 @@ module Worklist = struct
with Not_found ->
L . internal_error " @ \n ...Work list is empty! Impossible to remove edge...@ \n " ;
assert false
end
(* =============== END of module Worklist =============== *)
@ -129,10 +137,14 @@ let path_set_create_worklist proc_cfg =
Procdesc . compute_distance_to_exit_node ( ProcCfg . Exceptional . proc_desc proc_cfg ) ;
Worklist . create ()
let htable_retrieve ( htable : ( Procdesc . Node . id , Paths . PathSet . t ) Hashtbl . t ) ( key : Procdesc . Node . id )
: Paths . PathSet . t =
try Hashtbl . find htable key
with Not_found -> Hashtbl . replace htable key Paths . PathSet . empty ; Paths . PathSet . empty
with Not_found ->
Hashtbl . replace htable key Paths . PathSet . empty ;
Paths . PathSet . empty
(* * Add [d] to the pathset todo at [node] returning true if changed *)
let path_set_put_todo ( wl : Worklist . t ) ( node : Procdesc . Node . t ) ( d : Paths . PathSet . t ) : bool =
@ -150,6 +162,7 @@ let path_set_put_todo (wl: Worklist.t) (node: Procdesc.Node.t) (d: Paths.PathSet
in
changed
let path_set_checkout_todo ( wl : Worklist . t ) ( node : Procdesc . Node . t ) : Paths . PathSet . t =
try
let node_id = Procdesc . Node . get_id node in
@ -157,15 +170,18 @@ let path_set_checkout_todo (wl: Worklist.t) (node: Procdesc.Node.t) : Paths.Path
Hashtbl . replace wl . Worklist . path_set_todo node_id Paths . PathSet . empty ;
let visited = Hashtbl . find wl . Worklist . path_set_visited node_id in
let new_visited = Paths . PathSet . union visited todo in
Hashtbl . replace wl . Worklist . path_set_visited node_id new_visited ; todo
Hashtbl . replace wl . Worklist . path_set_visited node_id new_visited ;
todo
with Not_found -> L . die InternalError " could not find todo for node %a " Procdesc . Node . pp node
(* =============== END of the edge_set object =============== *)
let collect_do_abstract_pre pname tenv ( pset : Propset . t ) : Propset . t =
if ! Config . footprint then Config . run_in_re_execution_mode ( Abs . lifted_abstract pname tenv ) pset
else Abs . lifted_abstract pname tenv pset
let collect_do_abstract_post pname tenv ( pathset : Paths . PathSet . t ) : Paths . PathSet . t =
let abs_option p =
if Prover . check_inconsistency tenv p then None else Some ( Abs . abstract pname tenv p )
@ -174,16 +190,19 @@ let collect_do_abstract_post pname tenv (pathset: Paths.PathSet.t) : Paths.PathS
Config . run_in_re_execution_mode ( Paths . PathSet . map_option abs_option ) pathset
else Paths . PathSet . map_option abs_option pathset
let do_join_pre plist = Dom . proplist_collapse_pre plist
let do_join_post pname tenv ( pset : Paths . PathSet . t ) =
if Config . spec_abs_level < = 0 then Dom . pathset_collapse tenv pset
else Dom . pathset_collapse tenv ( Dom . pathset_collapse_impl pname tenv pset )
let do_meet_pre tenv pset =
if Config . meet_level > 0 then Dom . propset_meet_generate_pre tenv pset
else Propset . to_proplist pset
(* * Find the preconditions in the current spec table,
apply meet then join , and return the joined preconditions * )
let collect_preconditions tenv summary : Prop . normal Specs . Jprop . t list =
@ -247,6 +266,7 @@ let collect_preconditions tenv summary : Prop.normal Specs.Jprop.t list =
L . d_ln () ;
jplist''
(* =============== START of symbolic execution =============== *)
(* * propagate a set of results to the given node *)
@ -265,6 +285,7 @@ let propagate (wl: Worklist.t) pname ~is_exception (pset: Paths.PathSet.t)
let changed = path_set_put_todo wl curr_node edgeset_todo in
if changed then Worklist . add wl curr_node
(* * propagate a set of results, including exceptions and divergence *)
let propagate_nodes_divergence tenv ( proc_cfg : ProcCfg . Exceptional . t ) ( pset : Paths . PathSet . t )
( succ_nodes : Procdesc . Node . t list ) ( exn_nodes : Procdesc . Node . t list ) ( wl : Worklist . t ) =
@ -289,6 +310,7 @@ let propagate_nodes_divergence tenv (proc_cfg: ProcCfg.Exceptional.t) (pset: Pat
List . iter ~ f : ( propagate wl pname ~ is_exception : false pset_ok ) succ_nodes ;
List . iter ~ f : ( propagate wl pname ~ is_exception : true pset_exn ) exn_nodes
(* ===================== END of symbolic execution ===================== *)
(* =============== START of forward_tabulate =============== *)
@ -312,6 +334,7 @@ let do_symexec_join proc_cfg tenv wl curr_node (edgeset_todo: Paths.PathSet.t) =
new_dset' )
succ_nodes
let prop_max_size = ref ( 0 , Prop . prop_emp )
let prop_max_chain_size = ref ( 0 , Prop . prop_emp )
@ -325,14 +348,17 @@ let check_prop_size_ p _ =
Prop . d_prop p ;
L . d_ln () )
(* Check prop size and filter out possible unabstracted lists *)
let check_prop_size edgeset_todo =
if Config . monitor_prop_size then Paths . PathSet . iter check_prop_size_ edgeset_todo
let reset_prop_metrics () =
prop_max_size := ( 0 , Prop . prop_emp ) ;
prop_max_chain_size := ( 0 , Prop . prop_emp )
exception RE_EXE_ERROR
let do_before_node session node =
@ -341,6 +367,7 @@ let do_before_node session node =
L . reset_delayed_prints () ;
Printer . node_start_session node ( session :> int )
let do_after_node node = Printer . node_finish_session node
(* * Return the list of normal ids occurring in the instructions *)
@ -351,7 +378,10 @@ let instrs_get_normal_vars instrs =
let exps = Sil . instr_get_exps instr in
List . iter ~ f : do_e exps
in
List . iter ~ f : do_instr instrs ; Sil . fav_filter_ident fav Ident . is_normal ; Sil . fav_to_list fav
List . iter ~ f : do_instr instrs ;
Sil . fav_filter_ident fav Ident . is_normal ;
Sil . fav_to_list fav
(* * Perform symbolic execution for a node starting from an initial prop *)
let do_symbolic_execution proc_cfg handle_exn tenv ( node : ProcCfg . Exceptional . node )
@ -373,6 +403,7 @@ let do_symbolic_execution proc_cfg handle_exn tenv (node: ProcCfg.Exceptional.no
State . mark_execution_end node ;
pset
let mark_visited summary node =
let node_id = Procdesc . Node . get_id node in
let stats = summary . Specs . stats in
@ -380,6 +411,7 @@ let mark_visited summary node =
stats . Specs . nodes_visited_fp <- IntSet . add ( node_id :> int ) stats . Specs . nodes_visited_fp
else stats . Specs . nodes_visited_re <- IntSet . add ( node_id :> int ) stats . Specs . nodes_visited_re
let forward_tabulate tenv proc_cfg wl =
let pname = Procdesc . get_proc_name ( ProcCfg . Exceptional . proc_desc proc_cfg ) in
let handle_exn_node curr_node exn =
@ -389,10 +421,10 @@ let forward_tabulate tenv proc_cfg wl =
State . get_normalized_pre ( Abs . abstract_no_symop pname )
in
( match pre_opt with
| Some pre
-> L . d_strln " Precondition: " ; Prop . d_prop pre ; L . d_ln ()
| None
-> () ) ;
| Some pre ->
L . d_strln " Precondition: " ; Prop . d_prop pre ; L . d_ln ()
| None ->
() ) ;
L . d_strln " SIL INSTR: " ;
Procdesc . Node . d_instrs ~ sub_instrs : true ( State . get_instr () ) curr_node ;
L . d_ln () ;
@ -452,14 +484,14 @@ let forward_tabulate tenv proc_cfg wl =
check_prop_size pathset_todo ;
print_node_preamble curr_node session pathset_todo ;
match Procdesc . Node . get_kind curr_node with
| Procdesc . Node . Join_node
-> do_symexec_join proc_cfg tenv wl curr_node pathset_todo
| Procdesc . Node . Join_node ->
do_symexec_join proc_cfg tenv wl curr_node pathset_todo
| Procdesc . Node . Stmt_node _
| Procdesc . Node . Prune_node _
| Procdesc . Node . Exit_node _
| Procdesc . Node . Skip_node _
| Procdesc . Node . Start_node _
-> exe_iter ( do_prop curr_node handle_exn ) pathset_todo
| Procdesc . Node . Start_node _ ->
exe_iter ( do_prop curr_node handle_exn ) pathset_todo
in
let do_node_and_handle curr_node session =
let pathset_todo = path_set_checkout_todo wl curr_node in
@ -485,38 +517,40 @@ let forward_tabulate tenv proc_cfg wl =
mark_visited summary curr_node ;
(* mark nodes visited in fp and re phases *)
let session = incr summary . Specs . sessions ; ! ( summary . Specs . sessions ) in
do_before_node session curr_node ; do_node_and_handle curr_node session
do_before_node session curr_node ;
do_node_and_handle curr_node session
done ;
L . d_strln " .... Work list empty. Stop .... " ;
L . d_ln ()
(* * if possible, produce a ( fieldname, typ ) path from one of the [src_exps] to [sink_exp] using
[ reachable_hpreds ] . * )
let get_fld_typ_path_opt src_exps sink_exp_ reachable_hpreds_ =
let strexp_matches target_exp = function
| Sil . Eexp ( e , _ )
-> Exp . equal target_exp e
| _
-> false
| Sil . Eexp ( e , _ ) ->
Exp . equal target_exp e
| _ ->
false
in
let extend_path hpred ( sink_exp , path , reachable_hpreds ) =
match hpred with
| Sil . Hpointsto ( lhs , Sil . Estruct ( flds , _ ) , Exp . Sizeof { typ } )
-> List . find ~ f : ( function _ , se -> strexp_matches sink_exp se ) flds
| Sil . Hpointsto ( lhs , Sil . Estruct ( flds , _ ) , Exp . Sizeof { typ } ) ->
List . find ~ f : ( function _ , se -> strexp_matches sink_exp se ) flds
| > Option . value_map
~ f : ( function
| fld , _
-> let reachable_hpreds' = Sil . HpredSet . remove hpred reachable_hpreds in
| fld , _ ->
let reachable_hpreds' = Sil . HpredSet . remove hpred reachable_hpreds in
( lhs , ( Some fld , typ ) :: path , reachable_hpreds' ) )
~ default : ( sink_exp , path , reachable_hpreds )
| Sil . Hpointsto ( lhs , Sil . Earray ( _ , elems , _ ) , Exp . Sizeof { typ } )
-> if List . exists ~ f : ( function _ , se -> strexp_matches sink_exp se ) elems then
| Sil . Hpointsto ( lhs , Sil . Earray ( _ , elems , _ ) , Exp . Sizeof { typ } ) ->
if List . exists ~ f : ( function _ , se -> strexp_matches sink_exp se ) elems then
let reachable_hpreds' = Sil . HpredSet . remove hpred reachable_hpreds in
(* None means "no field name" ~=~ nameless array index *)
( lhs , ( None , typ ) :: path , reachable_hpreds' )
else ( sink_exp , path , reachable_hpreds )
| _
-> ( sink_exp , path , reachable_hpreds )
| _ ->
( sink_exp , path , reachable_hpreds )
in
(* terminates because [reachable_hpreds] is shrinking on each recursive call *)
let rec get_fld_typ_path sink_exp path reachable_hpreds =
@ -530,6 +564,7 @@ let get_fld_typ_path_opt src_exps sink_exp_ reachable_hpreds_ =
in
get_fld_typ_path sink_exp_ [] reachable_hpreds_
(* * report an error if any Context is reachable from a static field *)
let report_context_leaks pname sigma tenv =
(* report an error if an expression in [context_exps] is reachable from [field_strexp] *)
@ -541,10 +576,10 @@ let report_context_leaks pname sigma tenv =
~ f : ( fun ( context_exp , name ) ->
if Exp . Set . mem context_exp reachable_exps then
match get_fld_typ_path_opt fld_exps context_exp reachable_hpreds with
| None
-> () (* TODO ( T21871205 ) : the underlying issue still need to be fixed *)
| Some leak_path
-> let err_desc =
| None ->
() (* TODO ( T21871205 ) : the underlying issue still need to be fixed *)
| Some leak_path ->
let err_desc =
Errdesc . explain_context_leak pname ( Typ . mk ( Tstruct name ) ) fld_name leak_path
in
let exn = Exceptions . Context_leak ( err_desc , _ _ POS__ ) in
@ -558,23 +593,24 @@ let report_context_leaks pname sigma tenv =
match hpred with
| Sil . Hpointsto ( _ , Eexp ( exp , _ ) , Sizeof { typ = { desc = Tptr ( { desc = Tstruct name } , _ ) } } )
when not ( Exp . is_null_literal exp ) && AndroidFramework . is_context tenv name
&& not ( AndroidFramework . is_application tenv name )
-> ( exp , name ) :: exps
| _
-> exps )
&& not ( AndroidFramework . is_application tenv name ) ->
( exp , name ) :: exps
| _ ->
exps )
~ init : [] sigma
in
List . iter
~ f : ( function
| Sil . Hpointsto ( Exp . Lvar pv , Sil . Estruct ( static_flds , _ ) , _ ) when Pvar . is_global pv
-> List . iter
| Sil . Hpointsto ( Exp . Lvar pv , Sil . Estruct ( static_flds , _ ) , _ ) when Pvar . is_global pv ->
List . iter
~ f : ( fun ( f_name , f_strexp ) ->
check_reachable_context_from_fld ( f_name , f_strexp ) context_exps )
static_flds
| _
-> () )
| _ ->
() )
sigma
(* * Remove locals and formals,
and check if the address of a stack variable is left in the result * )
let remove_locals_formals_and_check tenv proc_cfg p =
@ -590,6 +626,7 @@ let remove_locals_formals_and_check tenv proc_cfg p =
in
List . iter ~ f : check_pvar pvars ; p'
(* * Collect the analysis results for the exit node. *)
let collect_analysis_result tenv wl proc_cfg : Paths . PathSet . t =
let exit_node = ProcCfg . Exceptional . exit_node proc_cfg in
@ -597,6 +634,7 @@ let collect_analysis_result tenv wl proc_cfg : Paths.PathSet.t =
let pathset = htable_retrieve wl . Worklist . path_set_visited exit_node_id in
Paths . PathSet . map ( remove_locals_formals_and_check tenv proc_cfg ) pathset
module Pmap = Caml . Map . Make ( struct
type t = Prop . normal Prop . t
@ -606,9 +644,11 @@ end)
let vset_ref_add_path vset_ref path =
Paths . Path . iter_all_nodes_nocalls ( fun n -> vset_ref := Procdesc . NodeSet . add n ! vset_ref ) path
let vset_ref_add_pathset vset_ref pathset =
Paths . PathSet . iter ( fun _ path -> vset_ref_add_path vset_ref path ) pathset
let compute_visited vset =
let res = ref Specs . Visitedset . empty in
let node_get_all_lines n =
@ -620,7 +660,9 @@ let compute_visited vset =
let do_node n =
res := Specs . Visitedset . add ( Procdesc . Node . get_id n , node_get_all_lines n ) ! res
in
Procdesc . NodeSet . iter do_node vset ; ! res
Procdesc . NodeSet . iter do_node vset ;
! res
(* * Extract specs from a pathset *)
let extract_specs tenv pdesc pathset : Prop . normal Specs . spec list =
@ -665,10 +707,10 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
in
let new_posts =
match post with
| None
-> current_posts
| Some ( post , path )
-> Paths . PathSet . add_renamed_prop post path current_posts
| None ->
current_posts
| Some ( post , path ) ->
Paths . PathSet . add_renamed_prop post path current_posts
in
let new_visited = Specs . Visitedset . union visited current_visited in
Pmap . add pre ( new_posts , new_visited ) map
@ -682,21 +724,20 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
~ f : ( fun ( p , path ) -> ( PropUtil . remove_seed_vars tenv p , path ) )
( Paths . PathSet . elements ( do_join_post pname tenv posts ) )
in
let spec =
{ Specs . pre = Specs . Jprop . Prop ( 1 , pre ) ; Specs . posts = posts' ; Specs . visited = visited }
in
let spec = { Specs . pre = Specs . Jprop . Prop ( 1 , pre ) ; Specs . posts = posts' ; Specs . visited } in
specs := spec :: ! specs
in
Pmap . iter add_spec pre_post_map ; ! specs
let collect_postconditions wl tenv proc_cfg : Paths . PathSet . t * Specs . Visitedset . t =
let pname = Procdesc . get_proc_name ( ProcCfg . Exceptional . proc_desc proc_cfg ) in
let pathset = collect_analysis_result tenv wl proc_cfg in
(* Assuming C++ developers use RAII, remove resources from the constructor posts *)
let pathset =
match pname with
| Typ . Procname . ObjC_Cpp _
-> if Typ . Procname . is_constructor pname then
| Typ . Procname . ObjC_Cpp _ ->
if Typ . Procname . is_constructor pname then
Paths . PathSet . map
( fun prop ->
Attribute . remove_resource tenv Racquire ( Rmemory Mobjc )
@ -704,8 +745,8 @@ let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * Specs.Visitedset
( Attribute . remove_resource tenv Racquire Rfile prop ) ) )
pathset
else pathset
| _
-> pathset
| _ ->
pathset
in
L . d_strln ( " #### [FUNCTION " ^ Typ . Procname . to_string pname ^ " ] Analysis result #### " ) ;
Propset . d Prop . prop_emp ( Paths . PathSet . to_propset tenv pathset ) ;
@ -733,15 +774,17 @@ let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * Specs.Visitedset
L . d_ln () ;
res
let create_seed_vars sigma =
let hpred_add_seed sigma = function
| Sil . Hpointsto ( Exp . Lvar pv , se , typ ) when not ( Pvar . is_abduced pv )
-> Sil . Hpointsto ( Exp . Lvar ( Pvar . to_seed pv ) , se , typ ) :: sigma
| _
-> sigma
| Sil . Hpointsto ( Exp . Lvar pv , se , typ ) when not ( Pvar . is_abduced pv ) ->
Sil . Hpointsto ( Exp . Lvar ( Pvar . to_seed pv ) , se , typ ) :: sigma
| _ ->
sigma
in
List . fold ~ f : hpred_add_seed ~ init : [] sigma
(* * Initialize proposition for execution given formal and global
parameters . The footprint is initialized according to the
execution mode . The prop is not necessarily emp , so it
@ -751,26 +794,27 @@ let prop_init_formals_seed tenv new_formals (prop: 'a Prop.t) : Prop.exposed Pro
let do_formal ( pv , typ ) =
let texp =
match ! Config . curr_language with
| Config . Clang
-> Exp . Sizeof { typ ; nbytes = None ; dynamic_length = None ; subtype = Subtype . exact }
| Config . Java
-> Exp . Sizeof { typ ; nbytes = None ; dynamic_length = None ; subtype = Subtype . subtypes }
| Config . Python
-> L . die InternalError " prop_init_formals_seed not implemented for Python "
| Config . Clang ->
Exp . Sizeof { typ ; nbytes = None ; dynamic_length = None ; subtype = Subtype . exact }
| Config . Java ->
Exp . Sizeof { typ ; nbytes = None ; dynamic_length = None ; subtype = Subtype . subtypes }
| Config . Python ->
L . die InternalError " prop_init_formals_seed not implemented for Python "
in
Prop . mk_ptsto_lvar tenv Prop . Fld_init Sil . inst_formal ( pv , texp , None )
in
List . map ~ f : do_formal new_formals
in
let sigma_seed =
create_seed_vars (* formals already there plus new ones *)
( prop . Prop . sigma @ sigma_new_formals )
create_seed_vars ( (* formals already there plus new ones *)
prop . Prop . sigma @ sigma_new_formals )
in
let sigma = sigma_seed @ sigma_new_formals in
let new_pi = prop . Prop . pi in
let prop' = Prop . set ( Prop . prop_sigma_star prop sigma ) ~ pi : new_pi in
Prop . set prop' ~ sigma_fp : ( prop' . Prop . sigma_fp @ sigma_new_formals )
(* * Construct an initial prop by extending [prop] with locals, and formals if [add_formals] is true
as well as seed variables * )
let initial_prop tenv ( curr_f : Procdesc . t ) ( prop : ' a Prop . t ) add_formals : Prop . normal Prop . t =
@ -785,6 +829,7 @@ let initial_prop tenv (curr_f: Procdesc.t) (prop: 'a Prop.t) add_formals : Prop.
let prop2 = prop_init_formals_seed tenv new_formals prop1 in
Prop . prop_rename_primed_footprint_vars tenv ( Prop . normalize tenv prop2 )
(* * Construct an initial prop from the empty prop *)
let initial_prop_from_emp tenv curr_f = initial_prop tenv curr_f Prop . prop_emp true
@ -801,6 +846,7 @@ let initial_prop_from_pre tenv curr_f pre =
initial_prop tenv curr_f pre3 false
else initial_prop tenv curr_f pre false
(* * Re-execute one precondition and return some spec if there was no re-execution error. *)
let execute_filter_prop wl tenv proc_cfg init_node ( precondition : Prop . normal Specs . Jprop . t )
: Prop . normal Specs . spec option =
@ -841,12 +887,12 @@ let execute_filter_prop wl tenv proc_cfg init_node (precondition: Prop.normal Sp
let pre =
let p = PropUtil . remove_locals_ret tenv pdesc ( Specs . Jprop . to_prop precondition ) in
match precondition with
| Specs . Jprop . Prop ( n , _ )
-> Specs . Jprop . Prop ( n , p )
| Specs . Jprop . Joined ( n , _ , jp1 , jp2 )
-> Specs . Jprop . Joined ( n , p , jp1 , jp2 )
| Specs . Jprop . Prop ( n , _ ) ->
Specs . Jprop . Prop ( n , p )
| Specs . Jprop . Joined ( n , _ , jp1 , jp2 ) ->
Specs . Jprop . Joined ( n , p , jp1 , jp2 )
in
let spec = { Specs . pre = pre ; Specs . posts = posts ; Specs . visited = visited } in
let spec = { Specs . pre ; Specs . posts ; Specs . visited } in
L . d_decrease_indent 1 ; do_after_node init_node ; Some spec
with RE_EXE_ERROR ->
do_before_node 0 init_node ;
@ -860,6 +906,7 @@ let execute_filter_prop wl tenv proc_cfg init_node (precondition: Prop.normal Sp
do_after_node init_node ;
None
let pp_intra_stats wl proc_cfg fmt _ =
let nstates = ref 0 in
let nodes = ProcCfg . Exceptional . nodes proc_cfg in
@ -872,6 +919,7 @@ let pp_intra_stats wl proc_cfg fmt _ =
nodes ;
F . fprintf fmt " (%d nodes containing %d states) " ( List . length nodes ) ! nstates
type exe_phase = ( unit -> unit ) * ( unit -> Prop . normal Specs . spec list * Specs . phase )
(* * Return functions to perform one phase of the analysis for a procedure.
@ -933,7 +981,8 @@ let perform_analysis_phase tenv (summary: Specs.summary) (proc_cfg: ProcCfg.Exce
Exceptions . Internal_error
( Localise . verbatim_desc " Leak_while_collecting_specs_after_footprint " )
in
Reporting . log_error_deprecated pname exn ; (* retuning no specs *) []
Reporting . log_error_deprecated pname exn ;
(* retuning no specs *) []
in
( specs , Specs . FOOTPRINT )
in
@ -952,10 +1001,10 @@ let perform_analysis_phase tenv (summary: Specs.summary) (proc_cfg: ProcCfg.Exce
let speco = execute_filter_prop wl tenv proc_cfg start_node p in
let is_valid =
match speco with
| None
-> false
| Some spec
-> valid_specs := ! valid_specs @ [ spec ] ;
| None ->
false
| Some spec ->
valid_specs := ! valid_specs @ [ spec ] ;
true
in
let outcome = if is_valid then " pass " else " fail " in
@ -982,26 +1031,32 @@ let perform_analysis_phase tenv (summary: Specs.summary) (proc_cfg: ProcCfg.Exce
L . ( debug Analysis Medium ) " @ \n *** CANDIDATE PRECONDITIONS FOR %a: " Typ . Procname . pp pname ;
L . ( debug Analysis Medium ) " @ \n ================================================@ \n " ;
L . ( debug Analysis Medium )
" @ \n %a @ \n @ \n " ( Specs . Jprop . pp_list Pp . text false ) candidate_preconditions ;
" @ \n %a @ \n @ \n "
( Specs . Jprop . pp_list Pp . text false )
candidate_preconditions ;
L . ( debug Analysis Medium ) " @ \n @ \n ================================================ " ;
L . ( debug Analysis Medium ) " @ \n *** VALID PRECONDITIONS FOR %a: " Typ . Procname . pp pname ;
L . ( debug Analysis Medium ) " @ \n ================================================@ \n " ;
L . ( debug Analysis Medium )
" @ \n %a @ \n @. " ( Specs . Jprop . pp_list Pp . text true ) valid_preconditions ;
" @ \n %a @ \n @. "
( Specs . Jprop . pp_list Pp . text true )
valid_preconditions ;
( specs , Specs . RE_EXECUTION )
in
( go , get_results )
in
match Specs . get_phase summary with
| Specs . FOOTPRINT
-> compute_footprint ()
| Specs . RE_EXECUTION
-> re_execution ()
| Specs . FOOTPRINT ->
compute_footprint ()
| Specs . RE_EXECUTION ->
re_execution ()
let set_current_language proc_desc =
let language = ( Procdesc . get_attributes proc_desc ) . ProcAttributes . language in
Config . curr_language := language
(* * reset global values before analysing a procedure *)
let reset_global_values proc_desc =
Config . reset_abs_val () ;
@ -1011,67 +1066,72 @@ let reset_global_values proc_desc =
Abs . reset_current_rules () ;
set_current_language proc_desc
(* Collect all pairs of the kind ( precondition, runtime exception ) from a summary *)
let exception_preconditions tenv pname summary =
let collect_exceptions pre ( exns , all_post_exn ) ( prop , _ ) =
match Tabulation . prop_get_exn_name pname prop with
| Some exn_name when PatternMatch . is_runtime_exception tenv exn_name
-> ( ( pre , exn_name ) :: exns , all_post_exn )
| _
-> ( exns , false )
| Some exn_name when PatternMatch . is_runtime_exception tenv exn_name ->
( ( pre , exn_name ) :: exns , all_post_exn )
| _ ->
( exns , false )
in
let collect_spec errors spec =
List . fold ~ f : ( collect_exceptions spec . Specs . pre ) ~ init : errors spec . Specs . posts
in
List . fold ~ f : collect_spec ~ init : ( [] , true ) ( Specs . get_specs_from_payload summary )
(* Collect all pairs of the kind ( precondition, custom error ) from a summary *)
let custom_error_preconditions summary =
let collect_errors pre ( errors , all_post_error ) ( prop , _ ) =
match Tabulation . lookup_custom_errors prop with
| None
-> ( errors , false )
| Some e
-> ( ( pre , e ) :: errors , all_post_error )
| None ->
( errors , false )
| Some e ->
( ( pre , e ) :: errors , all_post_error )
in
let collect_spec errors spec =
List . fold ~ f : ( collect_errors spec . Specs . pre ) ~ init : errors spec . Specs . posts
in
List . fold ~ f : collect_spec ~ init : ( [] , true ) ( Specs . get_specs_from_payload summary )
(* Remove the constrain of the form this != null which is true for all Java virtual calls *)
let remove_this_not_null tenv prop =
let collect_hpred ( var_option , hpreds ) = function
| Sil . Hpointsto ( Exp . Lvar pvar , Sil . Eexp ( Exp . Var var , _ ) , _ )
when Config . curr_language_is Config . Java && Pvar . is_this pvar
-> ( Some var , hpreds )
| hpred
-> ( var_option , hpred :: hpreds )
when Config . curr_language_is Config . Java && Pvar . is_this pvar ->
( Some var , hpreds )
| hpred ->
( var_option , hpred :: hpreds )
in
let collect_atom var atoms = function
| Sil . Aneq ( Exp . Var v , e ) when Ident . equal v var && Exp . equal e Exp . null
-> atoms
| a
-> a :: atoms
| Sil . Aneq ( Exp . Var v , e ) when Ident . equal v var && Exp . equal e Exp . null ->
atoms
| a ->
a :: atoms
in
match List . fold ~ f : collect_hpred ~ init : ( None , [] ) prop . Prop . sigma with
| None , _
-> prop
| Some var , filtered_hpreds
-> let filtered_atoms = List . fold ~ f : ( collect_atom var ) ~ init : [] prop . Prop . pi in
| None , _ ->
prop
| Some var , filtered_hpreds ->
let filtered_atoms = List . fold ~ f : ( collect_atom var ) ~ init : [] prop . Prop . pi in
let prop' = Prop . set Prop . prop_emp ~ pi : filtered_atoms ~ sigma : filtered_hpreds in
Prop . normalize tenv prop'
(* * Is true when the precondition does not contain constrains that can be false at call site.
This means that the post - conditions associated with this precondition cannot be prevented
by the calling context . * )
let is_unavoidable tenv pre =
let prop = remove_this_not_null tenv ( Specs . Jprop . to_prop pre ) in
match Prop . CategorizePreconditions . categorize [ prop ] with
| Prop . CategorizePreconditions . NoPres | Prop . CategorizePreconditions . Empty
-> true
| _
-> false
| Prop . CategorizePreconditions . NoPres | Prop . CategorizePreconditions . Empty ->
true
| _ ->
false
(* * Detects if there are specs of the form {precondition} proc {runtime exception} and report
an error in that case , generating the trace that lead to the runtime exception if the method is
@ -1085,11 +1145,11 @@ let report_runtime_exceptions tenv pdesc summary =
is_public_method
&&
match pname with
| Typ . Procname . Java pname_java
-> Typ . Procname . java_is_static pname
| Typ . Procname . Java pname_java ->
Typ . Procname . java_is_static pname
&& String . equal ( Typ . Procname . java_get_method pname_java ) " main "
| _
-> false
| _ ->
false
in
let is_annotated pdesc = Annotations . pdesc_has_return_annot pdesc Annotations . ia_is_verify in
let exn_preconditions , all_post_exn = exception_preconditions tenv pname summary in
@ -1105,6 +1165,7 @@ let report_runtime_exceptions tenv pdesc summary =
in
List . iter ~ f : report exn_preconditions
let report_custom_errors tenv summary =
let pname = Specs . get_proc_name summary in
let error_preconditions , all_post_error = custom_error_preconditions summary in
@ -1117,6 +1178,7 @@ let report_custom_errors tenv summary =
in
List . iter ~ f : report error_preconditions
module SpecMap = Caml . Map . Make ( struct
type t = Prop . normal Specs . Jprop . t
@ -1180,7 +1242,7 @@ let update_specs tenv prev_summary phase (new_specs: Specs.NormSpec.t list)
let convert pre ( post_set , visited ) =
res
:= Specs . spec_normalize tenv
{ Specs . pre = pre ; Specs . posts = Paths . PathSet . elements post_set ; Specs . visited = visited }
{ Specs . pre ; Specs . posts = Paths . PathSet . elements post_set ; Specs . visited }
:: ! res
in
List . iter ~ f : re_exe_filter old_specs ;
@ -1190,6 +1252,7 @@ let update_specs tenv prev_summary phase (new_specs: Specs.NormSpec.t list)
SpecMap . iter convert ! current_specs ;
( ! res , ! changed )
(* * update a summary after analysing a procedure *)
let update_summary tenv prev_summary specs phase res =
let normal_specs = List . map ~ f : ( Specs . spec_normalize tenv ) specs in
@ -1201,13 +1264,14 @@ let update_summary tenv prev_summary specs phase res =
let stats = { prev_summary . Specs . stats with symops ; stats_failure } in
let preposts =
match phase with
| Specs . FOOTPRINT
-> Some new_specs
| Specs . RE_EXECUTION
-> Some ( List . map ~ f : ( Specs . NormSpec . erase_join_info_pre tenv ) new_specs )
| Specs . FOOTPRINT ->
Some new_specs
| Specs . RE_EXECUTION ->
Some ( List . map ~ f : ( Specs . NormSpec . erase_join_info_pre tenv ) new_specs )
in
let payload = { prev_summary . Specs . payload with Specs . preposts = preposts } in
{ prev_summary with Specs . phase = phase ; stats ; payload }
let payload = { prev_summary . Specs . payload with Specs . preposts } in
{ prev_summary with Specs . phase ; stats ; payload }
(* * Analyze the procedure and return the resulting summary. *)
let analyze_proc tenv proc_cfg : Specs . summary =
@ -1225,6 +1289,7 @@ let analyze_proc tenv proc_cfg : Specs.summary =
report_runtime_exceptions tenv proc_desc updated_summary ;
updated_summary
(* * Perform the transition from [FOOTPRINT] to [RE_EXECUTION] in spec table *)
let transition_footprint_re_exe tenv proc_name joined_pres =
L . ( debug Analysis Medium ) " Transition %a from footprint to re-exe@. " Typ . Procname . pp proc_name ;
@ -1243,6 +1308,7 @@ let transition_footprint_re_exe tenv proc_name joined_pres =
in
Specs . add_summary proc_name summary'
(* * Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for
the procedures enabled after the analysis of [ proc_name ] * )
let perform_transition proc_cfg tenv proc_name =
@ -1269,15 +1335,17 @@ let perform_transition proc_cfg tenv proc_name =
" Error in collect_preconditions for %a@. " Typ . Procname . pp proc_name ;
let error = Exceptions . recognize_exception exn in
let err_str = " exception raised " ^ error . name . IssueType . unique_id in
L . ( debug Analysis Medium ) " Error: %s %a@. " err_str L . pp_ml_loc_opt error . ml_loc ; []
L . ( debug Analysis Medium ) " Error: %s %a@. " err_str L . pp_ml_loc_opt error . ml_loc ;
[]
in
transition_footprint_re_exe tenv proc_name joined_pres
in
match Specs . get_summary proc_name with
| Some summary when Specs . equal_phase ( Specs . get_phase summary ) Specs . FOOTPRINT
-> transition summary
| _
-> ()
| Some summary when Specs . equal_phase ( Specs . get_phase summary ) Specs . FOOTPRINT ->
transition summary
| _ ->
()
(* Create closures for the interprocedural algorithm *)
let interprocedural_algorithm_closures ~ prepare_proc exe_env : Tasks . closure list =
@ -1289,17 +1357,18 @@ let interprocedural_algorithm_closures ~prepare_proc exe_env : Tasks.closure lis
| Some proc_desc
when Config . reactive_mode
(* in reactive mode, only analyze changed procedures *)
&& ( Procdesc . get_attributes proc_desc ) . ProcAttributes . changed
-> analyze proc_desc
| Some proc_desc
-> analyze proc_desc
| None
-> ()
&& ( Procdesc . get_attributes proc_desc ) . ProcAttributes . changed ->
analyze proc_desc
| Some proc_desc ->
analyze proc_desc
| None ->
()
in
let procs_to_analyze = Cg . get_defined_nodes call_graph in
let create_closure proc_name () = process_one_proc proc_name in
List . map ~ f : create_closure procs_to_analyze
let analyze_procedure_aux cg_opt tenv proc_desc =
let proc_name = Procdesc . get_proc_name proc_desc in
let proc_cfg = ProcCfg . Exceptional . from_pdesc proc_desc in
@ -1311,17 +1380,20 @@ let analyze_procedure_aux cg_opt tenv proc_desc =
Specs . add_summary proc_name summaryfp ;
perform_transition proc_cfg tenv proc_name ;
let summaryre = Config . run_in_re_execution_mode ( analyze_proc tenv ) proc_cfg in
Specs . add_summary proc_name summaryre ; summaryre
Specs . add_summary proc_name summaryre ;
summaryre
let analyze_procedure { Callbacks . summary ; proc_desc ; tenv } : Specs . summary =
let proc_name = Procdesc . get_proc_name proc_desc in
Specs . add_summary proc_name summary ;
( try ignore ( analyze_procedure_aux None tenv proc_desc )
with exn ->
reraise_if exn ~ f : ( fun () -> not ( Exceptions . handle_exception exn ) ) ;
Reporting . log_error_deprecated proc_name exn ) ;
reraise_if exn ~ f : ( fun () -> not ( Exceptions . handle_exception exn ) ) ;
Reporting . log_error_deprecated proc_name exn ) ;
Specs . get_summary_unsafe _ _ FILE__ proc_name
(* * Create closures to perform the analysis of an exe_env *)
let do_analysis_closures exe_env : Tasks . closure list =
let get_calls caller_pdesc =
@ -1350,13 +1422,13 @@ let do_analysis_closures exe_env : Tasks.closure list =
let callbacks =
let get_proc_desc proc_name =
match Exe_env . get_proc_desc exe_env proc_name with
| Some pdesc
-> Some pdesc
| None when Config . ( equal_dynamic_dispatch dynamic_dispatch Lazy )
-> Option . bind ( Specs . get_summary proc_name ) ~ f : ( fun summary ->
| Some pdesc ->
Some pdesc
| None when Config . ( equal_dynamic_dispatch dynamic_dispatch Lazy ) ->
Option . bind ( Specs . get_summary proc_name ) ~ f : ( fun summary ->
summary . Specs . proc_desc_option )
| None
-> None
| None ->
None
in
let analyze_ondemand _ proc_desc =
let proc_name = Procdesc . get_proc_name proc_desc in
@ -1364,7 +1436,7 @@ let do_analysis_closures exe_env : Tasks.closure list =
let cg = Exe_env . get_cg exe_env in
analyze_procedure_aux ( Some cg ) tenv proc_desc
in
{ Ondemand . analyze_ondemand = analyze_ondemand ; get_proc_desc }
{ Ondemand . analyze_ondemand ; get_proc_desc }
in
let prepare_proc pn =
let should_init = Config . models_mode | | is_none ( Specs . get_summary pn ) in
@ -1378,6 +1450,7 @@ let do_analysis_closures exe_env : Tasks.closure list =
in
closures
let visited_and_total_nodes ~ filter cfg =
let filter_node pdesc n =
Procdesc . is_defined pdesc && filter pdesc
@ -1386,10 +1459,10 @@ let visited_and_total_nodes ~filter cfg =
| Procdesc . Node . Stmt_node _
| Procdesc . Node . Prune_node _
| Procdesc . Node . Start_node _
| Procdesc . Node . Exit_node _
-> true
| Procdesc . Node . Skip_node _ | Procdesc . Node . Join_node
-> false
| Procdesc . Node . Exit_node _ ->
true
| Procdesc . Node . Skip_node _ | Procdesc . Node . Join_node ->
false
in
let counted_nodes , visited_nodes_re =
let set = ref Procdesc . NodeSet . empty in
@ -1404,6 +1477,7 @@ let visited_and_total_nodes ~filter cfg =
in
( Procdesc . NodeSet . elements visited_nodes_re , Procdesc . NodeSet . elements counted_nodes )
(* * Print the stats for the given cfg.
Consider every defined proc unless a proc with the same name
was defined in another module , and was the one which was analyzed * )
@ -1411,10 +1485,10 @@ let print_stats_cfg proc_shadowed source cfg =
let err_table = Errlog . create_err_table () in
let filter pdesc =
match Specs . get_summary ( Procdesc . get_proc_name pdesc ) with
| None
-> false
| Some summary
-> Specs . get_specs_from_payload summary < > []
| None ->
false
| Some summary ->
Specs . get_specs_from_payload summary < > []
in
let nodes_visited , nodes_total = visited_and_total_nodes ~ filter cfg in
let num_proc = ref 0 in
@ -1428,14 +1502,14 @@ let print_stats_cfg proc_shadowed source cfg =
let compute_stats_proc proc_desc =
let proc_name = Procdesc . get_proc_name proc_desc in
match Specs . get_summary proc_name with
| None
-> ()
| Some _ when proc_shadowed proc_desc
-> L . ( debug Analysis Medium )
| None ->
()
| Some _ when proc_shadowed proc_desc ->
L . ( debug Analysis Medium )
" print_stats: ignoring function %a which is also defined in another file@. "
Typ . Procname . pp proc_name
| Some summary
-> let stats = summary . Specs . stats in
| Some summary ->
let stats = summary . Specs . stats in
let err_log = summary . Specs . attributes . ProcAttributes . err_log in
incr num_proc ;
let specs = Specs . get_specs_from_payload summary in
@ -1448,14 +1522,14 @@ let print_stats_cfg proc_shadowed source cfg =
Exceptions . equal_err_kind ekind Exceptions . Kerror && in_footprint )
err_log )
with
| [] , 0
-> incr num_nospec_noerror_proc
| _ , 0
-> incr num_spec_noerror_proc
| [] , _
-> incr num_nospec_error_proc
| _ , _
-> incr num_spec_error_proc
| [] , 0 ->
incr num_nospec_noerror_proc
| _ , 0 ->
incr num_spec_noerror_proc
| [] , _ ->
incr num_nospec_error_proc
| _ , _ ->
incr num_spec_error_proc
in
tot_symops := ! tot_symops + stats . Specs . symops ;
if Option . is_some stats . Specs . stats_failure then incr num_timeout ;
@ -1498,6 +1572,7 @@ let print_stats_cfg proc_shadowed source cfg =
L . ( debug Analysis Medium ) " %a " print_file_stats () ;
save_file_stats ()
(* * Print the stats for all the files in the cluster *)
let print_stats cluster =
let exe_env = Exe_env . from_cluster cluster in
@ -1510,3 +1585,4 @@ let print_stats cluster =
in
print_stats_cfg proc_shadowed source cfg )
exe_env