Source file cond_explore.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
module Diagnostic = Wax_utils.Diagnostic

module Bdd_tbl = Hashtbl.Make (struct
  type t = Cond_solver.t

  let equal = Cond_solver.equal
  let hash = Cond_solver.hash
end)

let max_configurations = 4096

let check_all diagnostics ?truncation_location
    ?(explain = fun env c -> Cond_solver.explain env c) ~specialize ~check () =
  (* A fresh solver state per call, so interning/diagnostics never leak between
     modules processed in the same process. *)
  let env = Cond_solver.create () in
  let queue = Queue.create () in
  Queue.push Cond_solver.true_ queue;
  let processed = Bdd_tbl.create 16 in
  (* error key -> (captured diagnostic, accumulated reachability) *)
  let errors : (string, Diagnostic.entry * Cond_solver.t) Hashtbl.t =
    Hashtbl.create 16
  in
  let count = ref 0 in
  let truncated = ref false in
  (* The union of every reachable configuration's assumption: the whole feasible
     space. A [universal] diagnostic (e.g. an unused local) is only reported if
     it arises across all of it — being unused in some branches but used in
     others is not "unused". *)
  let feasible = ref Cond_solver.false_ in
  while (not (Queue.is_empty queue)) && not !truncated do
    let asm = Queue.pop queue in
    if Bdd_tbl.mem processed asm || not (Cond_solver.is_satisfiable asm) then ()
    else if !count >= max_configurations then truncated := true
    else begin
      Bdd_tbl.add processed asm ();
      incr count;
      let a_full = ref Cond_solver.true_ in
      let record lit = a_full := Cond_solver.and_ !a_full lit in
      let enqueue b = Queue.push b queue in
      let cfg = specialize env asm ~enqueue ~record in
      (* Each configuration is checked in its own collector, derived from the
         parent so it inherits its error-recovery mode: the [unbound_name]
         cascade suppression (see lib-wax/typing.ml) then applies when
         type-checking a module recovered past syntax errors, just as it does on
         the conditional-free path. *)
      let cctx = Diagnostic.collector ~parent:diagnostics () in
      check cctx cfg;
      (* Backstop: [specialize] prunes unreachable branches up front, so a
         configuration's full assumption is normally satisfiable. This guards
         against any residual incompleteness by discarding errors should an
         infeasible configuration slip through. *)
      if Cond_solver.is_satisfiable !a_full then begin
        feasible := Cond_solver.or_ !feasible !a_full;
        List.iter
          (fun e ->
            let loc = Diagnostic.entry_location e in
            let key =
              Printf.sprintf "%d:%d:%s" loc.loc_start.pos_cnum
                loc.loc_end.pos_cnum
                (Wax_utils.Message.to_plain_string (Diagnostic.entry_message e))
            in
            let reach =
              match Hashtbl.find_opt errors key with
              | Some (_, r) -> Cond_solver.or_ r !a_full
              | None -> !a_full
            in
            Hashtbl.replace errors key (e, reach))
          (Diagnostic.collected cctx)
      end
    end
  done;
  let entries = Hashtbl.fold (fun _ v acc -> v :: acc) errors [] in
  (* Drop a [universal] diagnostic unless it arose in every reachable
     configuration, i.e. its accumulated reachability covers the whole feasible
     space. *)
  let entries =
    List.filter
      (fun (e, reach) ->
        (not (Diagnostic.entry_universal e))
        || Cond_solver.logical_implies !feasible reach)
      entries
  in
  let entries =
    List.sort
      (fun (e1, _) (e2, _) ->
        let l1 = Diagnostic.entry_location e1
        and l2 = Diagnostic.entry_location e2 in
        compare
          (l1.loc_start.pos_cnum, l1.loc_end.pos_cnum)
          (l2.loc_start.pos_cnum, l2.loc_end.pos_cnum))
      entries
  in
  List.iter
    (fun (e, reach) ->
      let base_hint = Diagnostic.entry_hint e in
      let hint =
        (* A [universal] diagnostic holds across the whole feasible space, so it
           carries no "reachable when" qualifier. *)
        match
          if Diagnostic.entry_universal e then None else explain env reach
        with
        | None -> base_hint
        | Some s ->
            let reach =
              Wax_utils.Message.text (Printf.sprintf "reachable when %s" s)
            in
            Some
              (match base_hint with
              | Some h -> Wax_utils.Message.(h ++ reach)
              | None -> reach)
      in
      Diagnostic.report diagnostics
        ~location:(Diagnostic.entry_location e)
        ~severity:(Diagnostic.entry_severity e)
        ?warning:(Diagnostic.entry_warning e)
        ?hint
        ~related:(Diagnostic.entry_related e)
        ~message:(Diagnostic.entry_message e)
        ())
    entries;
  if !truncated then
    match truncation_location with
    | Some location ->
        Diagnostic.report diagnostics ~location ~severity:Warning
          ~warning:Wax_utils.Warning.Truncated_coverage
          ~message:
            Wax_utils.Message.(
              text "Too many conditional configurations (over"
              ++ int max_configurations
              ^^ text "); coverage was truncated.")
          ()
    | None -> ()