1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
open Cil_types
open Cil_datatype
open Pdg_types
open PdgIndex
type data_info = ((PdgTypes.Node.t * Locations.Zone.t option) list
* Locations.Zone.t option) option
type ctrl_info = PdgTypes.Node.t list
type decl_info = PdgTypes.Node.t list
let zone_info_nodes pdg data_info =
let add_info_nodes pdg (nodes_acc, undef_acc) info =
let stmt = info.Logic_deps.ki in
let before = info.Logic_deps.before in
let zone = info.Logic_deps.zone in
Pdg_parameters.debug ~level:2 "[pdg:annotation] need %a %s stmt %d@."
Locations.Zone.pretty zone
(if before then "before" else "after") stmt.sid;
let nodes, undef_loc =
Sets.find_location_nodes_at_stmt pdg stmt ~before zone
in
let undef_acc = match undef_acc, undef_loc with
| None, _ -> undef_loc
| _, None -> undef_acc
| Some z1, Some z2 -> Some (Locations.Zone.join z1 z2)
in
(nodes @ nodes_acc, undef_acc)
in match data_info with
| None -> None
| Some data_info ->
let data_dpds = ([], None) in
let data_dpds =
List.fold_left (add_info_nodes pdg) data_dpds data_info
in Some data_dpds
let get_decl_nodes pdg decl_info =
let add_decl_nodes decl_var nodes_acc =
let node = Sets.find_decl_var_node pdg decl_var in
node::nodes_acc
in
Varinfo.Set.fold add_decl_nodes decl_info []
let find_nodes_for_function_contract pdg f_interpret =
let kf = PdgTypes.Pdg.get_kf pdg in
let (data_info, decl_label_info) = f_interpret kf in
let data_dpds = zone_info_nodes pdg data_info in
let decl_nodes =
get_decl_nodes pdg decl_label_info.Logic_deps.var
in
decl_nodes, data_dpds
let find_fun_precond_nodes (pdg:PdgTypes.Pdg.t) p =
let f_interpret kf =
let f_ctx = Logic_deps.mk_ctx_func_contract ~before:true kf in
Logic_deps.from_pred p f_ctx
in find_nodes_for_function_contract pdg f_interpret
let find_fun_postcond_nodes pdg p =
let f_interpret kf =
let f_ctx = Logic_deps.mk_ctx_func_contract ~before:false kf in
Logic_deps.from_pred p f_ctx
in let nodes,deps = find_nodes_for_function_contract pdg f_interpret
in let nodes =
if Logic_deps.to_result_from_pred p then
(Sets.find_output_node pdg)::nodes
else nodes
in nodes,deps
let find_fun_variant_nodes pdg t =
let f_interpret kf =
let f_ctx = Logic_deps.mk_ctx_func_contract ~before:true kf in
Logic_deps.from_term t f_ctx
in find_nodes_for_function_contract pdg f_interpret
let find_code_annot_nodes pdg stmt annot =
Pdg_parameters.debug "[pdg:annotation] CodeAnnot-%d stmt %d : %a @."
annot.annot_id stmt.sid
Printer.pp_code_annotation annot;
if Eva.Results.is_reachable stmt then
begin
let kf = PdgTypes.Pdg.get_kf pdg in
let (data_info, decl_label_info), slices =
Logic_deps.from_stmt_annot annot (stmt, kf)
in
let data_dpds = zone_info_nodes pdg data_info in
let decl_nodes = get_decl_nodes pdg decl_label_info.Logic_deps.var in
let labels = decl_label_info.Logic_deps.lbl in
let stmt_key = Key.stmt_key stmt in
let stmt_node = match stmt_key with
| Key.Stmt _ -> Sets.find_stmt_node pdg stmt
| Key.CallStmt _ -> Sets.find_call_ctrl_node pdg stmt
| _ -> assert false
in
let ctrl_dpds = Sets.direct_ctrl_dpds pdg stmt_node in
let add_stmt_nodes s acc =
try Sets.find_stmt_and_blocks_nodes pdg s @ acc
with Not_found -> acc
in
let stmt_slices = slices.Logic_deps.stmt in
let ctrl_dpds = Stmt.Set.fold add_stmt_nodes stmt_slices ctrl_dpds in
let add_label_nodes l acc = match l with
| StmtLabel stmt ->
let add acc l =
try (Sets.find_label_node pdg !stmt l)::acc
with Not_found -> acc
in List.fold_left add acc (!stmt).labels
| FormalLabel _ | BuiltinLabel _ -> acc
in
let ctrl_dpds = Logic_label.Set.fold add_label_nodes labels ctrl_dpds in
if Pdg_parameters.debug_atleast 2 then begin
let p fmt (n,z) = match z with
| None -> PdgTypes.Node.pretty fmt n
| Some z -> Format.fprintf fmt "%a(%a)"
PdgTypes.Node.pretty n Locations.Zone.pretty z
in
let pl fmt l = List.iter (fun n -> Format.fprintf fmt " %a" p n) l in
Pdg_parameters.debug " ctrl nodes = %a"
PdgTypes.Node.pretty_list ctrl_dpds;
Pdg_parameters.debug " decl nodes = %a"
PdgTypes.Node.pretty_list decl_nodes;
match data_dpds with
| None ->
Pdg_parameters.debug " data nodes = None (failed to compute)"
| Some (data_nodes, data_undef) ->
begin
Pdg_parameters.debug " data nodes = %a" pl data_nodes;
match data_undef with
| None -> ()
| Some data_undef ->
Pdg_parameters.debug " data undef = %a"
Locations.Zone.pretty data_undef;
end
end;
ctrl_dpds, decl_nodes, data_dpds
end
else begin
Pdg_parameters.debug ~level:2
"[pdg:annotation] CodeAnnot-%d : unreachable stmt ! @."
annot.annot_id;
raise Not_found
end