package catala

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file linting.ml

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
(* This file is part of the Catala compiler, a specification language for tax
   and social benefits computation rules. Copyright (C) 2023 Inria, contributor:
   Denis Merigoux <denis.merigoux@inria.fr>

   Licensed under the Apache License, Version 2.0 (the "License"); you may not
   use this file except in compliance with the License. You may obtain a copy of
   the License at

   http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
   WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
   License for the specific language governing permissions and limitations under
   the License. *)

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

(* To detect rules that have the same justification and conclusion, we create a
   set data structure with an appropriate comparison function *)
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 =
  (* TODO: this analysis should be finer grained: a false negative is if the
     field is used to define itself, for passing data around but that never gets
     really used or defined. *)
  if p.program_module_name <> None then ()
  else
    (* Disabled on modules *)
    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
            (* linting must be performed after disambiguation *)
            | 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
          (* Only check structs from the current module *)
          ()
        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
    (* Disabled on modules *)
    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
          (* Only check enums from the current module *)
          ()
        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

(* Reachability in a graph can be implemented as a simple fixpoint analysis with
   backwards propagation. *)
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 =
  (* Dead code detection for scope variables based on an intra-scope dependency
     analysis. *)
  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
        (* A variable is initially alive if it is an 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
OCaml

Innovation. Community. Security.