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
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
open Shared_ast
open Ast
open Catala_utils
(** If the variable is not an input, then it should be defined somewhere. *)
let detect_empty_definitions (p : program) : unit =
ScopeName.Map.iter
(fun (scope_name : ScopeName.t) scope ->
ScopeDef.Map.iter
(fun scope_def_key scope_def ->
if
(match scope_def_key with _, ScopeDef.Var _ -> true | _ -> false)
&& RuleName.Map.is_empty scope_def.scope_def_rules
&& (not scope_def.scope_def_is_condition)
&& (not
(ScopeVar.Map.mem
(Mark.remove (fst scope_def_key))
scope.scope_sub_scopes))
&&
match Mark.remove scope_def.scope_def_io.io_input with
| NoInput -> true
| _ -> false
then
Message.warning
~pos:(ScopeDef.get_position scope_def_key)
"In scope \"%a\",@ the@ variable@ \"%a\"@ is@ declared@ but@ \
never@ defined;@ did you forget something?"
ScopeName.format scope_name Ast.ScopeDef.format scope_def_key)
scope.scope_defs)
p.program_root.module_scopes
module RuleExpressionsMap = Map.Make (struct
type t = rule
let compare x y =
let xj, xj_mark = x.rule_just in
let yj, yj_mark = y.rule_just in
let just =
Bindlib.unbox
(Bindlib.box_apply2
(fun xj yj -> Expr.compare (xj, xj_mark) (yj, yj_mark))
xj yj)
in
if just = 0 then
let xc, xc_mark = x.rule_cons in
let yc, yc_mark = y.rule_cons in
Bindlib.unbox
(Bindlib.box_apply2
(fun xc yc -> Expr.compare (xc, xc_mark) (yc, yc_mark))
xc yc)
else just
let format ppf r = RuleName.format ppf r.rule_id
end)
let detect_identical_rules (p : program) : unit =
ScopeName.Map.iter
(fun _ scope ->
ScopeDef.Map.iter
(fun _ scope_def ->
let rules_seen =
RuleName.Map.fold
(fun _ rule rules_seen ->
RuleExpressionsMap.update rule
(fun l ->
let x =
( "",
Pos.overwrite_law_info
(snd (RuleName.get_info rule.rule_id))
(Pos.get_law_info (Expr.pos rule.rule_just)) )
in
match l with None -> Some [x] | Some l -> Some (x :: l))
rules_seen)
scope_def.scope_def_rules RuleExpressionsMap.empty
in
RuleExpressionsMap.iter
(fun _ pos ->
if List.length pos > 1 then
Message.warning ~extra_pos:pos
"These %s have identical justifications@ and@ consequences;@ \
is it a mistake?"
(if scope_def.scope_def_is_condition then "rules"
else "definitions"))
rules_seen)
scope.scope_defs)
p.program_root.module_scopes
let detect_unused_struct_fields (p : program) : unit =
if p.program_module_name <> None then ()
else
let struct_fields_used =
Ast.fold_exprs
~f:(fun struct_fields_used e ->
let rec structs_fields_used_expr e struct_fields_used =
match Mark.remove e with
| EDStructAccess _ -> assert false
| EStructAccess { e = e_struct; field; _ } ->
StructField.Set.add field
(structs_fields_used_expr e_struct struct_fields_used)
| EStruct { name = _; fields } ->
StructField.Map.fold
(fun field e_field struct_fields_used ->
StructField.Set.add field
(structs_fields_used_expr e_field struct_fields_used))
fields struct_fields_used
| _ ->
Expr.shallow_fold structs_fields_used_expr e struct_fields_used
in
structs_fields_used_expr e struct_fields_used)
~init:StructField.Set.empty p
in
let scope_out_structs_fields =
ScopeName.Map.fold
(fun _ out_struct acc ->
ScopeVar.Map.fold
(fun _ field acc -> StructField.Set.add field acc)
out_struct.out_struct_fields acc)
p.program_ctx.ctx_scopes StructField.Set.empty
in
StructName.Map.iter
(fun s_name fields ->
if StructName.path s_name <> [] then
()
else if
(not (StructField.Map.is_empty fields))
&& StructField.Map.for_all
(fun field _ ->
(not (StructField.Set.mem field struct_fields_used))
&& not (StructField.Set.mem field scope_out_structs_fields))
fields
then
Message.warning
~pos:(snd (StructName.get_info s_name))
"The structure@ \"%a\"@ is@ never@ used;@ maybe it's unnecessary?"
StructName.format s_name
else
StructField.Map.iter
(fun field _ ->
if
(not (StructField.Set.mem field struct_fields_used))
&& not (StructField.Set.mem field scope_out_structs_fields)
then
Message.warning
~pos:(snd (StructField.get_info field))
"The field@ \"%a\"@ of@ struct@ @{<yellow>\"%a\"@}@ is@ \
never@ used;@ maybe it's unnecessary?"
StructField.format field StructName.format s_name)
fields)
p.program_ctx.ctx_structs
let detect_unused_enum_constructors (p : program) : unit =
if p.program_module_name <> None then ()
else
let enum_constructors_used =
Ast.fold_exprs
~f:(fun enum_constructors_used e ->
let rec enum_constructors_used_expr e enum_constructors_used =
match Mark.remove e with
| EInj { name = _; e = e_enum; cons } ->
EnumConstructor.Set.add cons
(enum_constructors_used_expr e_enum enum_constructors_used)
| EMatch { e = e_match; name = _; cases } ->
let enum_constructors_used =
enum_constructors_used_expr e_match enum_constructors_used
in
EnumConstructor.Map.fold
(fun cons e_cons enum_constructors_used ->
EnumConstructor.Set.add cons
(enum_constructors_used_expr e_cons enum_constructors_used))
cases enum_constructors_used
| _ ->
Expr.shallow_fold enum_constructors_used_expr e
enum_constructors_used
in
enum_constructors_used_expr e enum_constructors_used)
~init:EnumConstructor.Set.empty p
in
EnumName.Map.iter
(fun e_name constructors ->
if EnumName.path e_name <> [] then
()
else if
EnumConstructor.Map.for_all
(fun cons _ ->
not (EnumConstructor.Set.mem cons enum_constructors_used))
constructors
then
Message.warning
~pos:(snd (EnumName.get_info e_name))
"The enumeration@ \"%a\"@ is@ never@ used;@ maybe it's unnecessary?"
EnumName.format e_name
else
EnumConstructor.Map.iter
(fun constructor _ ->
if
not (EnumConstructor.Set.mem constructor enum_constructors_used)
then
Message.warning
~pos:(snd (EnumConstructor.get_info constructor))
"The constructor@ \"%a\"@ of@ enumeration@ \"%a\"@ is@ \
never@ used;@ maybe it's unnecessary?"
EnumConstructor.format constructor EnumName.format e_name)
constructors)
p.program_ctx.ctx_enums
module Reachability =
Graph.Fixpoint.Make
(Dependency.ScopeDependencies)
(struct
type vertex = Dependency.ScopeDependencies.vertex
type edge = Dependency.ScopeDependencies.E.t
type g = Dependency.ScopeDependencies.t
type data = bool
let direction = Graph.Fixpoint.Backward
let equal = ( = )
let join = ( || )
let analyze _ x = x
end)
let detect_dead_code (p : program) : unit =
ScopeName.Map.iter
(fun scope_name scope ->
let scope_dependencies = Dependency.build_scope_dependencies scope in
let is_alive (v : Dependency.ScopeDependencies.vertex) =
match v with
| Assertion _ -> true
| Var (var, state) ->
let scope_def =
ScopeDef.Map.find
((var, Pos.no_pos), ScopeDef.Var state)
scope.scope_defs
in
Mark.remove scope_def.scope_def_io.io_output
in
let is_alive = Reachability.analyze is_alive scope_dependencies in
let emit_unused_warning vx =
Message.warning
~pos:(Mark.get (Dependency.Vertex.info vx))
"Unused varible:@ %a@ does@ not@ contribute@ to@ computing@ any@ of@ \
scope@ %a@ outputs.@ Did you forget something?"
Dependency.Vertex.format vx ScopeName.format scope_name
in
Dependency.ScopeDependencies.iter_vertex
(fun vx ->
if
(not (is_alive vx))
&& Dependency.ScopeDependencies.succ scope_dependencies vx = []
then emit_unused_warning vx)
scope_dependencies)
p.program_root.module_scopes
let lint_program (p : program) : unit =
detect_empty_definitions p;
detect_dead_code p;
detect_unused_struct_fields p;
detect_unused_enum_constructors p;
detect_identical_rules p