tallyingTest.ml 11.2 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
type pp = P of vv * string | N of string * vv
and vv = V of string

49
let mk_pp = function
50
51
  |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))
52
53

let mk_prod l =
54
55
    List.fold_left (fun acc c ->
      Tallying.CS.prod (mk_pp c) acc
56
57
58
59
60
    ) 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
61
let mk_s ll =
62
63
  List.fold_left (fun acc l ->
    Tallying.CS.union (mk_prod l) acc
Pietro Abate's avatar
Pietro Abate committed
64
65
  ) Tallying.CS.S.empty ll

66
67
68
69
70
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
71
    |((_,v),Some x,Some y) when Types.equiv x y -> Some x
72
73
74
75
76
    |((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
77
78
      |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))
79
80
81
82
83
84
85
86
87
    ) 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
88
(* check invariants on the constraints sets *)
Pietro Abate's avatar
Pietro Abate committed
89
let test_constraint_ops () = [
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

  "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")];

]
131

132
let test_constraints =
133
  "constraints" >:::
134
135
136
137
138
    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
139
    ) (test_constraint_ops ())
140
141
142
;;

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

Pietro Abate's avatar
Pietro Abate committed
144
let norm_tests () = [
Pietro Abate's avatar
Pietro Abate committed
145
146
147
148
149
150
151
152
153
154
155
156
  "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
157
158
159
160
  "(`$A -> Bool)", "(`$B -> `$B)", mk_s [
    [P(V "B","Empty")];
    [N("`$B",V "A");N("Bool",V "B")]
  ];
161

Pietro Abate's avatar
Pietro Abate committed
162
163
164
165
  "`$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")]];
166

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

Pietro Abate's avatar
Pietro Abate committed
172
  "(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)", mk_s [
173
174
     [P(V "A","Empty")];
    (* All these are subsumed as less general then (A <= 0) *)
Pietro Abate's avatar
Pietro Abate committed
175
176
177
178
    [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")]
  ];
179
180
181
182
183
184

  "(`$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
185
  (*
186
187
  "([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
  *)
188

Pietro Abate's avatar
Pietro Abate committed
189
  "(`$A , `$B)","(Int , Bool)", mk_s [
190
191
    [P(V "A","Empty")];
    [P(V "B","Empty")];
Pietro Abate's avatar
Pietro Abate committed
192
193
    [P(V "A","Int");P(V "B","Bool")]
  ];
194
195
196
197
198
199
200
201
202

  "(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
203
  ];
204
205

  "(`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
Pietro Abate's avatar
Pietro Abate committed
206
207
    [P(V "A","Int");P(V "B","Int")]
  ];
Pietro Abate's avatar
WIP    
Pietro Abate committed
208
209

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

213
214
  "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
215
216
217
218
219

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

220
221
222
]

let test_norm =
223
  "norm" >:::
224
225
226
227
228
    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
229
230
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
231
      )
Pietro Abate's avatar
Pietro Abate committed
232
    ) (norm_tests ())
233
234
;;

Pietro Abate's avatar
Pietro Abate committed
235
let merge_tests () = [
236
237
238
239
240
241
242
243
244
  "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;

245
  "quad", mk_s [[N("Bool",V "B");N("Int",V "B");N("`$B",V "A"); P(V "A", "Int | Bool")]],
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
    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")]
    ]
];;
262
263

let test_merge =
264
  "merge" >:::
265
266
267
    List.map (fun (test,s,expected) ->
      test >:: (fun _ ->
        let result = 
268
          try
269
270
271
272
            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
273
        in
274
275
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
276
      )
Pietro Abate's avatar
Pietro Abate committed
277
    ) (merge_tests ())
278
279
;;

280
281
let mk_e ll =
  List.map (fun l ->
282
    List.map (fun (V v,t) -> (Var.mk v),(parse_typ t)) l
283
284
285
  ) ll

let tallying_tests = [
Pietro Abate's avatar
Pietro Abate committed
286
287
288
289
290
  [("((Int | Bool) -> Int)", "(`$A -> `$B)")], mk_e [
    [(V "A","Empty")];
    [(V "A","Int | Bool");(V "B","Int")]
  ];

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

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

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

305
306
307
308
309
310
  [("((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")]
  ];
311
312
  [("[] -> []","Int -> `$A")], [];
  [("Bool -> Bool","Int -> `$A")], [];
Pietro Abate's avatar
Pietro Abate committed
313
314

  [("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [[]];
Pietro Abate's avatar
Pietro Abate committed
315
316
  
  (* map even *)
Pietro Abate's avatar
WIP    
Pietro Abate committed
317
318
  [("(`$A -> `$B) -> [`$A* ] -> [`$B* ]","((Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int)))")], [[]];
  [("(`$A -> `$A)", "((Int -> Int) & (Bool -> Bool)) -> `$T")], mk_e []
319
320
]

Pietro Abate's avatar
Pietro Abate committed
321
(* to test tallying { sigma_i } -- > for all i => s sigma_i <= t sigma_i *)
322
323
324
325
let test_tallying =
  let print_test l =
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
  in
326
  "tallying" >:::
327
328
    List.map (fun (l,expected) ->
      (print_test l) >:: (fun _ ->
329
330
331
        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
332
333
334
335
          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
336
337
338
339
              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
340
341
342
            ) result
          ) l
          (*
343
344
          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
345
      *)
346
        with Tallying.Step1Fail -> assert_equal expected []
347
348
349
350
      )
    ) tallying_tests
;;

351
352
let suite =
  "tests" >::: [
353
    test_constraints;
354
    test_norm;
355
    test_merge;
356
    test_tallying;
357
358
359
  ]
 
let main () =
360
  OUnit.run_test_tt_main suite
361
362
363
364
;;
 
main ()