tallyingTest.ml 11.4 KB
Newer Older
1
open OUnit
2
open Types
3

Pietro Abate's avatar
Pietro Abate committed
4
let parse_typ ?(variance=`Covariant) s =
5
6
  let st = Stream.of_string s in
  let astpat = Parser.pat st in 
Pietro Abate's avatar
Pietro Abate committed
7
  let nodepat = Typer.typ ~variance Builtin.env astpat in
8
9
10
  Types.descr nodepat
;;

11
12
13
14
15
16
17
18
19
20
21
22
23
let to_string pp t =
  Format.fprintf Format.str_formatter "%a@." pp t;
  Format.flush_str_formatter ()
;;

(* the abstract field is ignored in the comparison *)
module ESet = OUnitDiff.SetMake (struct 
  type t = (Var.var * Types.t)
  let compare (v1,t1) (v2,t2) = 
    let a = Types.abstract Abstract.any in
    if (v1,t1) == (v2,t2) then 0
    else let c = Var.compare v1 v2 in if c <> 0 then c
    else Types.compare (diff t1 a) (diff t2 a)
Pietro Abate's avatar
Pietro Abate committed
24
  let pp_printer ppf (v,t) = Format.fprintf ppf "(%a = %s)" Var.print v (to_string Print.print t)
25
26
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)
27

28
29
30
31
32
33
34
35
36
37
38
39
40
41
module SubStSet = OUnitDiff.SetMake (struct 
  type t = ESet.t
  let compare a b = ESet.compare a b
  let pp_printer ppf l = ESet.pp_printer ppf l
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

module MSet = OUnitDiff.SetMake (struct 
  type t = Tallying.CS.m
  let compare = 
    (* the abstract field is ignored in the comparison *)
    let a = Types.abstract Abstract.any in
    let cmp t1 t2 = Types.compare (diff t1 a) (diff t2 a) in
    Tallying.CS.M.compare cmp
Pietro Abate's avatar
Pietro Abate committed
42
  let pp_printer = Tallying.CS.pp_m
43
44
45
  let pp_print_sep = OUnitDiff.pp_comma_separator
end)

Pietro Abate's avatar
Pietro Abate committed
46
47
48
49
type pp = P of vv * string | N of string * vv
and vv = V of string

let mk_s ll =
Pietro Abate's avatar
WIP    
Pietro Abate committed
50
51
52
53
54
55
  let aux l =
    List.fold_left (fun acc -> function
      |P(V alpha,t) -> Tallying.CS.M.add (true,Var.mk alpha) (parse_typ t) acc
      |N(t,V alpha) -> Tallying.CS.M.add (false,Var.mk alpha) (parse_typ t) acc
    ) Tallying.CS.M.empty l
  in
56
  List.fold_left (fun acc l ->
Pietro Abate's avatar
WIP    
Pietro Abate committed
57
    Tallying.CS.S.add (aux l) acc
Pietro Abate's avatar
Pietro Abate committed
58
59
  ) Tallying.CS.S.empty ll

60
61
62
63
64
let mk_union_res l1 l2 =
  let aux_merge k v1 v2 = match (k,v1,v2) with
    |(k,None,None) -> assert false
    |(k,Some v,None) -> Some v
    |(k,None,Some v) -> Some v
65
    |((_,v),Some x,Some y) when Types.equiv x y -> Some x
66
67
68
69
70
    |((true,v),Some x,Some y) -> assert false
    |((false,v),Some x,Some y) -> assert false
  in
  let aux l = 
    List.fold_left (fun acc -> function
71
72
      |P(V v,s) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (true,Var.mk v) (parse_typ s))
      |N(s,V v) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (false,Var.mk v) (parse_typ s))
73
74
75
76
77
78
79
80
    ) Tallying.CS.M.empty l
  in 
  match l1,l2 with
  |[],[] -> Tallying.CS.sat
  |l1,[] -> (Tallying.CS.S.singleton (aux l1))
  |[],l2 -> (Tallying.CS.S.singleton (aux l2))
  |l1,l2 -> Tallying.CS.S.union (Tallying.CS.S.singleton (aux l1)) (Tallying.CS.S.singleton (aux l2))

Pietro Abate's avatar
Pietro Abate committed
81
(* check invariants on the constraints sets *)
Pietro Abate's avatar
WIP    
Pietro Abate committed
82
83
84
85
86
87
88
89
90
91
92
93
let mk_pp = function
  |P(V alpha,t) -> Tallying.CS.singleton (Tallying.Pos (Var.mk alpha,parse_typ t))
  |N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,Var.mk alpha))

let mk_prod l =
    List.fold_left (fun acc c ->
      Tallying.CS.prod (mk_pp c) acc
    ) Tallying.CS.sat l

let mk_union l1 l2 =
  Tallying.CS.union (mk_prod l1) (mk_prod l2)

Pietro Abate's avatar
Pietro Abate committed
94
let test_constraint_ops () = [
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

  "prod pos",mk_prod [P(V "A","Int");P(V "A","Bool")], mk_pp (P(V "A","Int & Bool"));

  "prod neg",mk_prod [N("Int",V "B");N("Bool",V "B")], mk_pp (N("Int | Bool",V "B"));

  "prod var",mk_prod [N("`$B",V "A");P(V "B","Bool | Int")],
      mk_union_res 
        [N("`$B",V "A");P(V "B","Bool | Int")] 
        [];

  "empty", mk_union [P(V "A","Empty")] [P(V "A","Empty")], mk_pp (P(V "A","Empty"));

  "empty <= int 1", mk_union [P(V "A","Int")] [P(V "A","Empty")], mk_pp (P(V "A","Int"));
  "empty <= int 2", mk_union [P(V "A","Empty")] [P(V "A","Int")], mk_pp (P(V "A","Int"));

  "int v bool <= int", mk_union [P(V "A","Int | Bool")] [P(V "A","Int")], mk_pp (P(V "A","Int | Bool"));

  "0 -> 1 <= a -> b", mk_union [P(V "A","Empty -> Any")] [P(V "A","Int -> Bool")], mk_pp (P(V "A","Empty -> Any"));

  "union 1",mk_union [P(V "A","Empty")] [P(V "A","Empty");N("Int",V "B")], mk_pp (P(V "A","Empty"));

  "union 2",mk_union [P(V "A","Empty")] [P(V "A","Int");P(V "A","Bool")],
      mk_union_res 
      [P(V "A","Int & Bool")]
      [P(V "A","Empty")];

  "union 2 comm",mk_union [P(V "A","Int");P(V "A","Bool")] [P(V "A","Empty")],
      mk_union_res
        [P(V "A","Int & Bool")]
        [(P(V "A","Empty"))];

  "union 3",mk_union [P(V "A","Empty")] [P(V "A","Empty");P(V "B","Empty")], mk_pp (P(V "A","Empty"));

  "union 4",mk_union [P(V "A","Empty")] [P(V "A","Empty");P(V "B","Int")], mk_pp (P(V "A","Empty"));

  "union 5",mk_union [P(V "A","Int | Bool");N("Int",V "B");P(V "B","Empty")] [P(V "A","Empty");P(V "B","Empty")],
      mk_union_res 
        [P(V "A","Int | Bool");N("Int",V "B");P(V "B","Empty")]
        [P(V "A","Empty");P(V "B","Empty")];

]
136

137
let test_constraints =
138
  "constraints" >:::
139
140
141
142
143
    List.map (fun (test,result,expected) ->
      test >:: (fun _ ->
        let elem s = (MSet.of_list (Tallying.CS.S.elements s)) in
        MSet.assert_equal (elem expected) (elem result)
      )
Pietro Abate's avatar
Pietro Abate committed
144
    ) (test_constraint_ops ())
145
146
147
;;

(* ^ => & -- v => | *)
Pietro Abate's avatar
Pietro Abate committed
148

Pietro Abate's avatar
Pietro Abate committed
149
let norm_tests () = [
Pietro Abate's avatar
Pietro Abate committed
150
151
152
153
154
155
156
157
158
159
160
161
  "Int", "Empty", Tallying.CS.unsat;
  "(Int,Int)", "Empty", Tallying.CS.unsat;
  "Int -> Int", "Empty" , Tallying.CS.unsat;

  "Bool -> Bool","Int -> `$A", Tallying.CS.unsat;
  "Int", "Bool", Tallying.CS.unsat;
  "Int", "Empty", Tallying.CS.unsat;
  "[] -> []","Int -> `$A", Tallying.CS.unsat;

  "Any", "Empty",  Tallying.CS.unsat;
  "Empty", "Empty",  Tallying.CS.sat;

Pietro Abate's avatar
Pietro Abate committed
162
163
164
165
  "(`$A -> Bool)", "(`$B -> `$B)", mk_s [
    [P(V "B","Empty")];
    [N("`$B",V "A");N("Bool",V "B")]
  ];
166

Pietro Abate's avatar
Pietro Abate committed
167
168
169
170
  "`$B", "`$A", mk_s [[N("`$B",V "A")]];
  "`$B", "Empty", mk_s [[P(V "B","Empty")]];
  "Int", "`$B", mk_s [[N("Int",V "B")]];
  "Int", "(`$A | `$B)", mk_s [[N("Int \\ `$B",V "A")]];
171

Pietro Abate's avatar
Pietro Abate committed
172
173
174
175
  "(Int -> Bool)", "(`$A -> `$B)", mk_s [
    [P(V "A","Empty")];
    [P(V "A","Int");N("Bool",V "B")]
  ];
176

Pietro Abate's avatar
Pietro Abate committed
177
  "(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)", mk_s [
178
179
     [P(V "A","Empty")];
    (* All these are subsumed as less general then (A <= 0) *)
Pietro Abate's avatar
Pietro Abate committed
180
181
182
183
    [P(V "A","Empty");N("Int",V "B")];
    [P(V "A","Empty");N("Bool",V "B")];
    [P(V "A","Empty");N("Int | Bool",V "B")]
  ];
184
185
186
187
188
189

  "(`$A -> `$B)", "(Int -> Int) | (Bool -> Bool)", mk_s [
    [P(V "B","Int");N("Int",V "A")];
    [P(V "B","Bool");N("Bool",V "A")];
  ];

Pietro Abate's avatar
Pietro Abate committed
190
  (*
191
192
  "([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
  *)
193

Pietro Abate's avatar
Pietro Abate committed
194
  "(`$A , `$B)","(Int , Bool)", mk_s [
195
196
    [P(V "A","Empty")];
    [P(V "B","Empty")];
Pietro Abate's avatar
Pietro Abate committed
197
198
    [P(V "A","Int");P(V "B","Bool")]
  ];
199
200
201
202
203
204
205
206
207

  "(Int , Bool)","(`$A , `$B)", mk_s [ [N("Int", V "A");N("Bool", V "B")] ];
  "(Bool , Bool)","(`$A , `$B)", mk_s [ [N("Bool", V "A");N("Bool", V "B")] ];

  "(`$A | (`$B , `$C))","(Int , Int)", mk_s [
    [P(V "A","(Int , Int)"); P(V "B","Empty")];
    [P(V "A","(Int , Int)"); P(V "C","Empty")];
    [P(V "A","(Int , Int)"); P(V "B","Int"); P(V "C","Int")];

Pietro Abate's avatar
Pietro Abate committed
208
  ];
209
210

  "(`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
Pietro Abate's avatar
Pietro Abate committed
211
212
    [P(V "A","Int");P(V "B","Int")]
  ];
Pietro Abate's avatar
WIP    
Pietro Abate committed
213
214

  "(`$A -> `$B) -> [ `$A ] -> [ `$B ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$Gamma", mk_s [
Pietro Abate's avatar
Pietro Abate committed
215
216
    [P(V "A","Empty")]
  ];
217

218
219
  "Int -> Bool", "`$A", mk_s [[N("Int -> Bool",V "A")]];
  "((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))",Tallying.CS.sat;
Pietro Abate's avatar
Pietro Abate committed
220
221
222
223
224

  "((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
    [P(V "A","Int");P(V "B","Int")]
  ];

225
226
227
]

let test_norm =
228
  "norm" >:::
229
230
231
232
233
    List.map (fun (s,t,expected) ->
      (Printf.sprintf " %s \\ %s" s t) >:: (fun _ ->
        let s = parse_typ s in
        let t = parse_typ t in
        let result = Tallying.norm (diff s t) in
234
235
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
236
      )
Pietro Abate's avatar
Pietro Abate committed
237
    ) (norm_tests ())
238
239
;;

Pietro Abate's avatar
Pietro Abate committed
240
let merge_tests () = [
241
242
243
244
245
246
247
248
249
  "empty  empty", mk_s [[P(V "A", "Empty");P(V "B", "Empty")]], 
    mk_s [
      [P(V "A","Empty");P(V "B","Empty")]
    ];

  "unsat 1", mk_s [[P(V "A", "Int | Bool");N("Int",V "B");P(V "B", "Empty")]], Tallying.CS.unsat;

  "unsat 2", mk_s [[N("Bool",V "B"); N("`$B", V "A"); P(V "A", "Empty")]], Tallying.CS.unsat;

250
  "quad", mk_s [[N("Bool",V "B");N("Int",V "B");N("`$B",V "A"); P(V "A", "Int | Bool")]],
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
    mk_s [
      [N("`$B", V "A");P(V "A","Int | Bool");N("Int | Bool", V "B"); P(V "B","Int | Bool")]
    ];

  "add one", mk_s [[N("`$B", V "A");P(V "A","Int | Bool")]], 
    mk_s [[N("`$B", V "A");P(V "A","Int | Bool");P(V "B","Int | Bool")]];

  "A B", mk_s [[P(V "A", "`$B")]], mk_pp (P(V "A","`$B"));

  "", mk_s [[P(V "B", "Empty")]], mk_pp (P(V "B","Empty"));

  "", mk_s [[P(V "A", "Int");P(V "B", "Bool"); P(V "A", "Empty")]],
    mk_s [
      [P(V "A","Empty");P(V "B","Bool")]
    ]
];;
267
268

let test_merge =
269
  "merge" >:::
270
271
272
    List.map (fun (test,s,expected) ->
      test >:: (fun _ ->
        let result = 
273
          try
274
275
276
277
            Tallying.CS.S.fold (fun c acc ->
              Tallying.CS.union (Tallying.merge c) acc
            ) s Tallying.CS.S.empty
          with Tallying.UnSatConstr -> Tallying.CS.unsat
278
        in
279
280
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
281
      )
Pietro Abate's avatar
Pietro Abate committed
282
    ) (merge_tests ())
283
284
;;

285
286
let mk_e ll =
  List.map (fun l ->
287
    List.map (fun (V v,t) -> (Var.mk v),(parse_typ t)) l
288
289
290
  ) ll

let tallying_tests = [
Pietro Abate's avatar
Pietro Abate committed
291
292
293
294
295
  [("((Int | Bool) -> Int)", "(`$A -> `$B)")], mk_e [
    [(V "A","Empty")];
    [(V "A","Int | Bool");(V "B","Int")]
  ];

296
  [("((Int | Bool) -> Int)", "(`$A -> `$B)"); ("(`$A -> Bool)","(`$B -> `$B)")], mk_e [
297
298
    [(V "A","Int | Bool");(V "B","Int | Bool")];
    [(V "A","Empty");(V "B","Empty")]
299
  ];
Pietro Abate's avatar
Pietro Abate committed
300
301

  [("(Int -> Bool)", "(`$A -> `$B)")], mk_e [
302
303
    [(V "A","Empty")];
    [(V "A","Int");(V "B","Bool")];
Pietro Abate's avatar
Pietro Abate committed
304
305
  ];

306
  [("(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)")], mk_e [
307
    [(V "A","Empty")];
308
  ];
Pietro Abate's avatar
Pietro Abate committed
309

310
311
312
313
314
315
  [("((Int,Int) , (Int | Bool))","(`$A,Int) | ((`$B,Int),Bool)")], mk_e [
    [(V "A", "(Int,Int)"); (V "B","Int")]
  ];
  [("((`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))")], mk_e [
    [(V "A","Int");(V "B","Int")]
  ];
316
317
  [("[] -> []","Int -> `$A")], [];
  [("Bool -> Bool","Int -> `$A")], [];
Pietro Abate's avatar
Pietro Abate committed
318
319

  [("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [[]];
Pietro Abate's avatar
Pietro Abate committed
320
321
  
  (* map even *)
Pietro Abate's avatar
WIP    
Pietro Abate committed
322
323
  [("(`$A -> `$B) -> [`$A* ] -> [`$B* ]","((Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int)))")], [[]];
  [("(`$A -> `$A)", "((Int -> Int) & (Bool -> Bool)) -> `$T")], mk_e []
324
325
]

Pietro Abate's avatar
Pietro Abate committed
326
(* to test tallying { sigma_i } -- > for all i => s sigma_i <= t sigma_i *)
327
328
329
330
let test_tallying =
  let print_test l =
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
  in
331
  "tallying" >:::
332
333
    List.map (fun (l,expected) ->
      (print_test l) >:: (fun _ ->
334
335
336
        try
          let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
          let result = Tallying.tallying l in
Pietro Abate's avatar
Pietro Abate committed
337
338
339
340
          List.iter (fun (s,t) -> 
            List.iter (fun sigma ->
              let s_sigma = Tallying.apply_subst s sigma in
              let t_sigma = Tallying.apply_subst t sigma in
Pietro Abate's avatar
Pietro Abate committed
341
342
343
344
              assert_equal ~pp_diff:(fun fmt _ -> 
                  Format.fprintf fmt "s @ sigma_i = %a\n" Types.Print.print s_sigma;
                  Format.fprintf fmt "t @ sigma_i = %a\n" Types.Print.print t_sigma
              ) (Types.subtype s_sigma t_sigma) true
Pietro Abate's avatar
Pietro Abate committed
345
346
347
            ) result
          ) l
          (*
348
349
          let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
          SubStSet.assert_equal (elem expected) (elem result)
Pietro Abate's avatar
Pietro Abate committed
350
      *)
351
        with Tallying.Step1Fail -> assert_equal expected []
352
353
354
355
      )
    ) tallying_tests
;;

356
357
let suite =
  "tests" >::: [
358
    test_constraints;
359
    test_norm;
360
    test_merge;
361
    test_tallying;
362
363
364
  ]
 
let main () =
365
  OUnit.run_test_tt_main suite
366
367
368
369
;;
 
main ()