@ -1071,25 +1071,6 @@ let pp_dotty_one_spec f pre posts =
F . fprintf f " @ \n } @ \n "
F . fprintf f " @ \n } @ \n "
(* this is used to print a list of proposition when considered in a path of nodes *)
let pp_dotty_prop_list_in_path f plist prev_n curr_n =
try
incr proposition_counter ;
incr dotty_state_count ;
F . fprintf f " @ \n subgraph cluster_%i { color=blue @ \n " ! dotty_state_count ;
incr dotty_state_count ;
F . fprintf f " @ \n state%iN [label= \" NODE %i \" , style=filled, color= lightblue]@ \n " curr_n
curr_n ;
List . iter
~ f : ( fun po ->
incr proposition_counter ;
pp_dotty f Generic_proposition po None )
plist ;
if prev_n < > - 1 then F . fprintf f " @ \n state%iN ->state%iN@ \n " prev_n curr_n ;
F . fprintf f " @ \n } @ \n "
with exn when SymOp . exn_not_failure exn -> ()
let pp_dotty_prop fmt ( prop , cycle ) = let pp_dotty_prop fmt ( prop , cycle ) =
reset_proposition_counter () ;
reset_proposition_counter () ;
Format . fprintf fmt " @ \n @ \n @ \n digraph main { @ \n node [shape=box]; @ \n " ;
Format . fprintf fmt " @ \n @ \n @ \n digraph main { @ \n node [shape=box]; @ \n " ;
@ -1119,38 +1100,9 @@ let dotty_retain_cycle_to_str prop (cycle: RetainCyclesType.t) =
with exn when SymOp . exn_not_failure exn -> None
with exn when SymOp . exn_not_failure exn -> None
(* create a dotty file with a single proposition *)
let dotty_prop_to_dotty_file fname prop cycle =
try
let out_dot = Out_channel . create fname in
let fmt_dot = Format . formatter_of_out_channel out_dot in
pp_dotty_prop fmt_dot ( prop , cycle ) ;
Out_channel . close out_dot
with exn when SymOp . exn_not_failure exn -> ()
(* This is used only to print a list of prop parsed with the external parser. Basically
deprecated . * )
let pp_proplist_parsed2dotty_file filename plist =
try
let pp_list f plist =
reset_proposition_counter () ;
F . fprintf f " @ \n @ \n @ \n digraph main { @ \n node [shape=box];@ \n " ;
F . fprintf f " @ \n compound = true; @ \n " ;
F . fprintf f " @ \n /* size= \" 12,7 \" ; ratio=fill;*/ @ \n " ;
ignore ( List . map ~ f : ( pp_dotty f Generic_proposition ) plist ) ;
F . fprintf f " @ \n } "
in
let outc = Out_channel . create filename in
let fmt = F . formatter_of_out_channel outc in
F . fprintf fmt " #### Dotty version: ####@.%a@.@. " pp_list plist ;
Out_channel . close outc
with exn when SymOp . exn_not_failure exn -> ()
(* * * * * * * * * * START of Print interprocedural cfgs in dotty format *) (* * * * * * * * * * START of Print interprocedural cfgs in dotty format *)
(* * * * * * * * * * Print control flow graph ( in dot form ) for fundec to *) (* * * * * * * * * * Print control flow graph ( in dot form ) for fundec to channel. You have to compute an
(* channel. You have to compute an interprocedural cfg first * interprocedural cfg first . * )
let pp_cfgnodename pname fmt ( n : Procdesc . Node . t ) = let pp_cfgnodename pname fmt ( n : Procdesc . Node . t ) =
F . fprintf fmt " \" %s_%d \" "
F . fprintf fmt " \" %s_%d \" "
@ -1318,418 +1270,3 @@ let pp_speclist_to_file (filename: DB.filename) spec_list =
let pp_speclist_dotty_file ( filename : DB . filename ) spec_list = let pp_speclist_dotty_file ( filename : DB . filename ) spec_list =
try pp_speclist_to_file filename spec_list with exn when SymOp . exn_not_failure exn -> ()
try pp_speclist_to_file filename spec_list with exn when SymOp . exn_not_failure exn -> ()
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
(* Code prodicing a xml version of a graph *)
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
(* each node has an unique integer identifier *)
type visual_heap_node =
| VH_dangling of int * Exp . t
| VH_pointsto of int * Exp . t * Sil . strexp * Exp . t
(* VH_pointsto ( id,address,content,type ) *)
| VH_lseg of int * Exp . t * Exp . t * Sil . lseg_kind
(* VH_lseg ( id,address,content last cell, kind ) *)
(* VH_dllseg ( id, address, content first cell, content last cell, address last cell, kind ) *)
| VH_dllseg of int * Exp . t * Exp . t * Exp . t * Exp . t * Sil . lseg_kind
(* an edge is a pair of node identifiers *)
type visual_heap_edge = { src : int ; trg : int ; lab : string }
let mk_visual_heap_edge s t l = { src = s ; trg = t ; lab = l }
(* used to generate unique identifier for all the nodes in the set of visual graphs used to *)
(* represent a proposition *)
let global_node_counter = ref 0
let working_list = ref []
let set_dangling_nodes = ref []
(* convert an exp into a string which is xml friendly, ie. special character are replaced by *)
(* the proper xml way to visualize them *)
let exp_to_xml_string e = F . asprintf " %a " ( Sil . pp_exp_printenv ( Pp . html Black ) ) e
(* convert an atom into an xml-friendly string without special characters *)
let atom_to_xml_string a = F . asprintf " %a " ( Sil . pp_atom ( Pp . html Black ) ) a
(* return the dangling node corresponding to an expression it exists or None *)
let exp_dangling_node e =
let entry_e =
List . filter
~ f : ( fun b -> match b with VH_dangling ( _ , e' ) -> Exp . equal e e' | _ -> false )
! set_dangling_nodes
in
match entry_e with
| [] ->
None
| ( VH_dangling ( n , e' ) ) :: _ ->
Some ( VH_dangling ( n , e' ) )
| _ ->
None
(* NOTE: this cannot be possible since entry_e can be composed only by VH_dangling, see def of entry_e *)
(* make nodes and when it finds a list records in the working list *)
(* to do ( n, prop ) where n is the integer identifier of the list node. *)
(* This allow to keep the connection between the list node and the graph *)
(* that displays its contents. *)
let rec make_visual_heap_nodes sigma =
let n = ! global_node_counter in
incr global_node_counter ;
match sigma with
| [] ->
[]
| ( Sil . Hpointsto ( e , se , t ) ) :: sigma' ->
VH_pointsto ( n , e , se , t ) :: make_visual_heap_nodes sigma'
| ( Sil . Hlseg ( k , hpara , e1 , e2 , _ ) ) :: sigma' ->
working_list := ( n , hpara . Sil . body ) :: ! working_list ;
VH_lseg ( n , e1 , e2 , k ) :: make_visual_heap_nodes sigma'
| ( Sil . Hdllseg ( k , hpara_dll , e1 , e2 , e3 , e4 , _ ) ) :: sigma' ->
working_list := ( n , hpara_dll . Sil . body_dll ) :: ! working_list ;
VH_dllseg ( n , e1 , e2 , e3 , e4 , k ) :: make_visual_heap_nodes sigma'
(* given a node returns its id and address *)
let get_node_id_and_addr node =
match node with
| VH_dangling ( n , e )
| VH_pointsto ( n , e , _ , _ )
| VH_lseg ( n , e , _ , _ )
| VH_dllseg ( n , e , _ , _ , _ , _ ) ->
( n , e )
(* return node's id *)
let get_node_id node = fst ( get_node_id_and_addr node )
(* return node's address *)
let get_node_addr node = snd ( get_node_id_and_addr node )
(* return the nodes corresponding to an address given by an expression *)
let rec select_node_at_address nodes e =
match nodes with
| [] ->
None
| n :: l' ->
let e' = get_node_addr n in
if Exp . equal e e' then Some n else select_node_at_address l' e
(* look-up the ids in the list of nodes corresponding to expression e *)
(* let look_up_nodes_ids nodes e =
List . map ~ f : get_node_id ( select_nodes_exp nodes e ) * )
(* create a list of dangling nodes *)
let make_set_dangling_nodes allocated_nodes ( sigma : Sil . hpred list ) =
let make_new_dangling e =
let n = ! global_node_counter in
incr global_node_counter ; VH_dangling ( n , e )
in
let get_rhs_predicate hpred =
match hpred with
| Sil . Hpointsto ( _ , Sil . Eexp ( e , _ ) , _ ) when not ( Exp . equal e Exp . zero ) ->
[ e ]
| Sil . Hlseg ( _ , _ , _ , e2 , _ ) when not ( Exp . equal e2 Exp . zero ) ->
[ e2 ]
| Sil . Hdllseg ( _ , _ , _ , e2 , e3 , _ , _ ) ->
if Exp . equal e2 Exp . zero then if Exp . equal e3 Exp . zero then [] else [ e3 ] else [ e2 ; e3 ]
| Sil . Hpointsto ( _ , _ , _ ) | _ ->
[]
(* arrays and struct do not give danglings. CHECK THIS! *)
in
let is_not_allocated e =
let allocated =
List . exists
~ f : ( fun a ->
match a with
| VH_pointsto ( _ , e' , _ , _ ) | VH_lseg ( _ , e' , _ , _ ) | VH_dllseg ( _ , e' , _ , _ , _ , _ ) ->
Exp . equal e e'
| _ ->
false )
allocated_nodes
in
not allocated
in
let rec filter_duplicate l seen_exp =
match l with
| [] ->
[]
| e :: l' ->
if List . exists ~ f : ( Exp . equal e ) seen_exp then filter_duplicate l' seen_exp
else e :: filter_duplicate l' ( e :: seen_exp )
in
let rhs_exp_list = List . concat_map ~ f : get_rhs_predicate sigma in
let candidate_dangling_exps = filter_duplicate rhs_exp_list [] in
(* get rid of allocated ones *)
let dangling_exps = List . filter ~ f : is_not_allocated candidate_dangling_exps in
List . map ~ f : make_new_dangling dangling_exps
(* return a list of pairs ( n,field_lab ) where n is a target node *)
(* corresponding to se and is going to be used a target for and edge *)
(* field_lab is the name of the field which points to n ( if any ) *)
let rec compute_target_nodes_from_sexp nodes se prop field_lab =
match se with
| Sil . Eexp ( e , _ ) when is_nil e prop ->
(* Nil is not represented by a node, it's just a value which should be printed *)
[]
| Sil . Eexp ( e , _ )
-> (
let e_node = select_node_at_address nodes e in
match e_node with
| None -> (
match exp_dangling_node e with None -> [] | Some dang_node -> [ ( dang_node , field_lab ) ] )
| Some n ->
[ ( n , field_lab ) ] )
| Sil . Estruct ( lfld , inst ) -> (
match lfld with
| [] ->
[]
| ( fn , se2 ) :: l' ->
compute_target_nodes_from_sexp nodes se2 prop ( Typ . Fieldname . to_string fn )
@ compute_target_nodes_from_sexp nodes ( Sil . Estruct ( l' , inst ) ) prop " " )
| Sil . Earray ( len , lie , inst ) ->
match lie with
| [] ->
[]
| ( idx , se2 ) :: l' ->
let lab = " [ " ^ exp_to_xml_string idx ^ " ] " in
compute_target_nodes_from_sexp nodes se2 prop lab
@ compute_target_nodes_from_sexp nodes ( Sil . Earray ( len , l' , inst ) ) prop " "
(* build the set of edges between nodes *)
let rec make_visual_heap_edges nodes sigma prop =
let combine_source_target_label n ( m , lab ) =
mk_visual_heap_edge ( get_node_id n ) ( get_node_id m ) lab
in
match sigma with
| [] ->
[]
| ( Sil . Hpointsto ( e , se , _ ) ) :: sigma'
-> (
let e_node = select_node_at_address nodes e in
match e_node with
| None ->
assert false
| Some n ->
let target_nodes = compute_target_nodes_from_sexp nodes se prop " " in
let ll = List . map ~ f : ( combine_source_target_label n ) target_nodes in
ll @ make_visual_heap_edges nodes sigma' prop )
| ( Sil . Hlseg ( _ , _ , e1 , e2 , _ ) ) :: sigma'
-> (
let e1_node = select_node_at_address nodes e1 in
match e1_node with
| None ->
assert false
| Some n ->
let target_nodes =
compute_target_nodes_from_sexp nodes ( Sil . Eexp ( e2 , Sil . inst_none ) ) prop " "
in
let ll = List . map ~ f : ( combine_source_target_label n ) target_nodes in
ll @ make_visual_heap_edges nodes sigma' prop )
| ( Sil . Hdllseg ( _ , _ , e1 , e2 , e3 , _ , _ ) ) :: sigma' ->
let e1_node = select_node_at_address nodes e1 in
match e1_node with
| None ->
assert false
| Some n ->
let target_nodesF =
compute_target_nodes_from_sexp nodes ( Sil . Eexp ( e3 , Sil . inst_none ) ) prop " "
in
let target_nodesB =
compute_target_nodes_from_sexp nodes ( Sil . Eexp ( e2 , Sil . inst_none ) ) prop " "
in
let llF = List . map ~ f : ( combine_source_target_label n ) target_nodesF in
let llB = List . map ~ f : ( combine_source_target_label n ) target_nodesB in
llF @ llB @ make_visual_heap_edges nodes sigma' prop
(* from a prop generate and return visual proposition *)
let prop_to_set_of_visual_heaps prop =
let result = ref [] in
working_list := [ ( ! global_node_counter , prop . Prop . sigma ) ] ;
incr global_node_counter ;
while ! working_list < > [] do
set_dangling_nodes := [] ;
let n , h = List . hd_exn ! working_list in
working_list := List . tl_exn ! working_list ;
let nodes = make_visual_heap_nodes h in
set_dangling_nodes := make_set_dangling_nodes nodes h ;
let edges = make_visual_heap_edges nodes h prop in
result := ! result @ [ ( n , nodes @ ! set_dangling_nodes , edges ) ]
done ;
! result
let rec pointsto_contents_to_xml ( co : Sil . strexp ) : Io_infer . Xml . node =
match co with
| Sil . Eexp ( e , _ ) ->
Io_infer . Xml . create_tree " cell " [ ( " content-value " , exp_to_xml_string e ) ] []
| Sil . Estruct ( fel , _ ) ->
let f ( fld , exp ) =
Io_infer . Xml . create_tree " struct-field " [ ( " id " , Typ . Fieldname . to_string fld ) ]
[ pointsto_contents_to_xml exp ]
in
Io_infer . Xml . create_tree " struct " [] ( List . map ~ f fel )
| Sil . Earray ( len , nel , _ ) ->
let f ( e , se ) =
Io_infer . Xml . create_tree " array-element " [ ( " index " , exp_to_xml_string e ) ]
[ pointsto_contents_to_xml se ]
in
Io_infer . Xml . create_tree " array " [ ( " size " , exp_to_xml_string len ) ] ( List . map ~ f nel )
(* Convert an atom to xml in a light version. Namely, the expressions are not fully blown-up into *)
(* xml tree but visualized as strings *)
let atom_to_xml_light ( a : Sil . atom ) : Io_infer . Xml . node =
let kind_info =
match a with
| Sil . Aeq _ when Prop . atom_is_inequality a ->
" inequality "
| Sil . Aeq _ ->
" equality "
| Sil . Aneq _ ->
" disequality "
| Sil . Apred _ ->
" pred "
| Sil . Anpred _ ->
" npred "
in
Io_infer . Xml . create_tree " stack-variable "
[ ( " type " , kind_info ) ; ( " instance " , atom_to_xml_string a ) ] []
let xml_pure_info prop =
let pure = Prop . get_pure prop in
let xml_atom_list = List . map ~ f : atom_to_xml_light pure in
Io_infer . Xml . create_tree " stack " [] xml_atom_list
(* * Return a string describing the kind of a pointsto address *)
let pointsto_addr_kind = function
| Exp . Lvar pv ->
if Pvar . is_global pv then " global "
else if Pvar . is_local pv && Mangled . equal ( Pvar . get_name pv ) Ident . name_return then " return "
else if Pvar . is_local pv then " parameter "
else " other "
| _ ->
" other "
let heap_node_to_xml node =
match node with
| VH_dangling ( id , addr ) ->
let atts =
[ ( " id " , string_of_int id )
; ( " address " , exp_to_xml_string addr )
; ( " node-type " , " dangling " )
; ( " memory-type " , pointsto_addr_kind addr ) ]
in
Io_infer . Xml . create_tree " node " atts []
| VH_pointsto ( id , addr , cont , _ ) ->
let atts =
[ ( " id " , string_of_int id )
; ( " address " , exp_to_xml_string addr )
; ( " node-type " , " allocated " )
; ( " memory-type " , pointsto_addr_kind addr ) ]
in
let contents = pointsto_contents_to_xml cont in
Io_infer . Xml . create_tree " node " atts [ contents ]
| VH_lseg ( id , addr , _ , Sil . Lseg_NE ) ->
let atts =
[ ( " id " , string_of_int id )
; ( " address " , exp_to_xml_string addr )
; ( " node-type " , " single linked list " )
; ( " list-type " , " non-empty " )
; ( " memory-type " , " other " ) ]
in
Io_infer . Xml . create_tree " node " atts []
| VH_lseg ( id , addr , _ , Sil . Lseg_PE ) ->
let atts =
[ ( " id " , string_of_int id )
; ( " address " , exp_to_xml_string addr )
; ( " node-type " , " single linked list " )
; ( " list-type " , " possibly empty " )
; ( " memory-type " , " other " ) ]
in
Io_infer . Xml . create_tree " node " atts []
| VH_dllseg ( id , addr1 , cont1 , cont2 , addr2 , _ ) ->
let contents1 = pointsto_contents_to_xml ( Sil . Eexp ( cont1 , Sil . inst_none ) ) in
let contents2 = pointsto_contents_to_xml ( Sil . Eexp ( cont2 , Sil . inst_none ) ) in
let atts =
[ ( " id " , string_of_int id )
; ( " addr-first " , exp_to_xml_string addr1 )
; ( " addr-last " , exp_to_xml_string addr2 )
; ( " node-type " , " double linked list " )
; ( " memory-type " , " other " ) ]
in
Io_infer . Xml . create_tree " node " atts [ contents1 ; contents2 ]
let heap_edge_to_xml edge =
let atts =
[ ( " source " , string_of_int edge . src ) ; ( " target " , string_of_int edge . trg ) ; ( " label " , edge . lab ) ]
in
Io_infer . Xml . create_tree " edge " atts []
let visual_heap_to_xml heap =
let n , nodes , edges = heap in
let xml_heap_nodes = List . map ~ f : heap_node_to_xml nodes in
let xml_heap_edges = List . map ~ f : heap_edge_to_xml edges in
Io_infer . Xml . create_tree " heap " [ ( " id " , string_of_int n ) ] ( xml_heap_nodes @ xml_heap_edges )
(* * convert a proposition to xml with the given tag and id *)
let prop_to_xml prop tag_name id =
let visual_heaps = prop_to_set_of_visual_heaps prop in
let xml_visual_heaps = List . map ~ f : visual_heap_to_xml visual_heaps in
let xml_pure_part = xml_pure_info prop in
let xml_graph =
Io_infer . Xml . create_tree tag_name [ ( " id " , string_of_int id ) ]
( xml_visual_heaps @ [ xml_pure_part ] )
in
xml_graph
(* * reset the counter used for node and heap identifiers *)
let reset_node_counter () = global_node_counter := 0
let print_specs_xml signature specs loc fmt =
reset_node_counter () ;
let do_one_spec pre posts n =
let add_stack_to_prop prop_ =
(* add stack vars from pre *)
let pre_stack = fst ( Prop . sigma_get_stack_nonstack true pre . Prop . sigma ) in
let prop'_ = Prop . set prop_ ~ sigma : ( pre_stack @ prop_ . Prop . sigma ) in
Prop . normalize ( Tenv . create () ) prop'_
in
let jj = ref 0 in
let xml_pre = prop_to_xml pre " precondition " ! jj in
let xml_spec =
xml_pre
:: List . map
~ f : ( fun ( po , _ ) ->
jj := ! jj + 1 ;
prop_to_xml ( add_stack_to_prop po ) " postcondition " ! jj )
posts
in
Io_infer . Xml . create_tree " specification " [ ( " id " , string_of_int n ) ] xml_spec
in
let j = ref 0 in
let list_of_specs_xml =
List . map
~ f : ( fun s ->
j := ! j + 1 ;
do_one_spec ( Specs . Jprop . to_prop s . Specs . pre ) s . Specs . posts ! j )
specs
in
let xml_specifications = Io_infer . Xml . create_tree " specifications " [] list_of_specs_xml in
let xml_signature = Io_infer . Xml . create_tree " signature " [ ( " name " , signature ) ] [] in
let proc_summary =
Io_infer . Xml . create_tree " procedure "
[ ( " file " , SourceFile . to_string loc . Location . file ) ; ( " line " , string_of_int loc . Location . line ) ]
[ xml_signature ; xml_specifications ]
in
Io_infer . Xml . pp_document true fmt proc_summary
Jules Villard
7 years ago
committed by
Facebook Github Bot