Source file translators.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
open Batteries

open ConstrSys
open SolverTypes

(** Translate a [DemandConstrSys] into a [EqConstrSys] *)
module EqConstrSysFromDemandConstrSys (S: DemandEqConstrSys)
  : EqConstrSys   with type v = S.v
                   and type d = S.d
                   and module Var = S.Var
                   and module Dom = S.Dom =
struct
  type v = S.v
  type d = S.d
  module Var = S.Var
  module Dom = S.Dom

  let system (x: v) =
    match S.system x with
    | None -> None
    | Some f ->
      let f' get set = f get set (ignore % get) in
      Some f'

  let sys_change = S.sys_change
  let postmortem = S.postmortem
end

(** Translate a [DemandGlobConstrSys] into a [DemandEqConstrSys] *)
module EqConstrSysFromGlobConstrSys (S:DemandGlobConstrSys)
  : DemandEqConstrSys   with type v = Var2(S.LVar)(S.GVar).t
                         and type d = Lattice.Lift2(S.G)(S.D).t
                         and module Var = Var2(S.LVar)(S.GVar)
                         and module Dom = Lattice.Lift2(S.G)(S.D)
=
struct
  module Var = Var2(S.LVar)(S.GVar)
  module Dom =
  struct
    include Lattice.Lift2 (S.G) (S.D)
    let printXml f = function
      | `Lifted1 a -> S.G.printXml f a
      | `Lifted2 a -> S.D.printXml f a
      | (`Bot | `Top) as x -> printXml f x
  end
  type v = Var.t
  type d = Dom.t

  let getG = function
    | `Lifted1 x -> x
    | `Bot -> S.G.bot ()
    | `Top -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has top value"
    | `Lifted2 _ -> failwith "EqConstrSysFromGlobConstrSys.getG: global variable has local value"

  let getL = function
    | `Lifted2 x -> x
    | `Bot -> S.D.bot ()
    | `Top -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has top value"
    | `Lifted1 _ -> failwith "EqConstrSysFromGlobConstrSys.getL: local variable has global value"

  let l, g = (fun x -> `L x), (fun x -> `G x)
  let lD, gD = (fun x -> `Lifted2 x), (fun x -> `Lifted1 x)

  let conv f get set demand =
    f (getL % get % l) (fun x v -> set (l x) (lD v)) (fun x -> demand @@ l x)
      (getG % get % g) (fun x v -> set (g x) (gD v))
    |> lD

  let system = function
    | `G _ -> None
    | `L x -> Option.map conv (S.system x)

  let sys_change get =
    S.sys_change (getL % get % l) (getG % get % g)

  let postmortem = function
    | `L g -> List.map (fun x -> `L x) @@ S.postmortem g
    | _ -> []
end

(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution with given [Hashtbl.S] for the [EqConstrSys]. *)
module GlobConstrSolFromEqConstrSolBase (S: DemandGlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) (VH: Hashtbl.S with type key = Var2 (S.LVar) (S.GVar).t) =
struct
  let split_solution hm =
    let l' = LH.create 113 in
    let g' = GH.create 113 in
    let split_vars x d = match x with
      | `L x ->
        begin match d with
          | `Lifted2 d -> LH.replace l' x d
          (* | `Bot -> () *)
          (* Since Verify2 is broken and only checks existing keys, add it with local bottom value.
             This works around some cases, where Verify2 would not detect a problem due to completely missing variable. *)
          | `Bot -> LH.replace l' x (S.D.bot ())
          | `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has top value"
          | `Lifted1 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has global value"
        end
      | `G x ->
        begin match d with
          | `Lifted1 d -> GH.replace g' x d
          | `Bot -> ()
          | `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has top value"
          | `Lifted2 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: global variable has local value"
        end
    in
    VH.iter split_vars hm;
    (l', g')
end

(** Splits a [EqConstrSys] solution into a [GlobConstrSys] solution. *)
module GlobConstrSolFromEqConstrSol (S: DemandGlobConstrSys) (LH: Hashtbl.S with type key = S.LVar.t) (GH: Hashtbl.S with type key = S.GVar.t) =
struct
  module S2 = EqConstrSysFromGlobConstrSys (S)
  module VH = Hashtbl.Make (S2.Var)

  include GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH)
end


module DemandEqIncrSolverFromGenericEqIncrSolver (Sol: GenericEqIncrSolver): DemandEqIncrSolver =
  functor (Arg: IncrSolverArg) ->
  functor (S: DemandEqConstrSys) ->
  functor (H: Hashtbl.S with type key = S.v) ->
    Sol (Arg) (EqConstrSysFromDemandConstrSys  (S)) (H)


(** Transforms a [DemandEqIncrSolver] into a [DemandGlobIncrSolver]. *)
module GlobSolverFromEqSolver (Sol:DemandEqIncrSolverBase)
  = functor (S:DemandGlobConstrSys) ->
    functor (LH:Hashtbl.S with type key=S.LVar.t) ->
    functor (GH:Hashtbl.S with type key=S.GVar.t) ->
    struct
      module EqSys = EqConstrSysFromGlobConstrSys (S)

      module VH : Hashtbl.S with type key=EqSys.v = Hashtbl.Make(EqSys.Var)
      module Sol' = Sol (EqSys) (VH)

      module Splitter = GlobConstrSolFromEqConstrSolBase (S) (LH) (GH) (VH) (* reuse EqSys and VH *)

      type marshal = Sol'.marshal

      let copy_marshal = Sol'.copy_marshal
      let relift_marshal = Sol'.relift_marshal

      let solve ls gs l old_data =
        let vs = List.map (fun (x,v) -> `L x, `Lifted2 v) ls
                 @ List.map (fun (x,v) -> `G x, `Lifted1 v) gs in
        let sv = List.map (fun x -> `L x) l in
        let hm, solver_data = Sol'.solve vs sv old_data in
        Splitter.split_solution hm, solver_data
    end