tallyingTest.ml 11.5 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
  let st = Stream.of_string s in
6
  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
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 *)
17
module ESet = OUnitDiff.SetMake (struct
18
  type t = (Var.var * Types.t)
19
  let compare (v1,t1) (v2,t2) =
20 21 22 23
    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
module SubStSet = OUnitDiff.SetMake (struct
29 30 31 32 33 34
  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)

35
module MSet = OUnitDiff.SetMake (struct
36
  type t = Tallying.CS.m
37
  let compare =
38 39 40
    (* 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
41
    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
  let aux l =
    List.fold_left (fun acc -> function
52 53
      |P(V alpha,t) -> Tallying.CS.M.add ((*true,*)Var.mk alpha) (Types.empty,parse_typ t) acc
      |N(t,V alpha) -> Tallying.CS.M.add ((*false,*)Var.mk alpha) (parse_typ t,Types.any) acc
Pietro Abate's avatar
WIP  
Pietro Abate committed
54 55
    ) 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
    |((true,v),Some x,Some y) -> assert false
    |((false,v),Some x,Some y) -> assert false
  in
69
  let aux l =
70
    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) (Types.empty, 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, Types.any))
73
    ) Tallying.CS.M.empty l
74
  in
75 76 77 78 79 80
  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

  "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")],
101 102
      mk_union_res
        [N("`$B",V "A");P(V "B","Bool | Int")]
103 104 105 106 107 108 109 110 111 112 113 114 115 116
        [];

  "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")],
117
      mk_union_res
118 119 120 121 122 123 124 125 126 127 128 129 130
      [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")],
131
      mk_union_res
132 133 134 135
        [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
  "Int -> Bool", "`$A", mk_s [[N("Int -> Bool",V "A")]];
219 220

  "((`$A , Int) & (`$B , Bool))","(Int , (*Int & Bool*) Empty)",Tallying.CS.sat;
Pietro Abate's avatar
Pietro Abate committed
221 222 223 224 225

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

226 227 228
]

let test_norm =
229
  "norm" >:::
230 231 232 233 234
    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
235 236
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
237
      )
Pietro Abate's avatar
Pietro Abate committed
238
    ) (norm_tests ())
239 240
;;

Pietro Abate's avatar
Pietro Abate committed
241
let merge_tests () = [
242
  "empty  empty", mk_s [[P(V "A", "Empty");P(V "B", "Empty")]],
243 244 245 246 247 248 249 250
    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;

251
  "quad", mk_s [[N("Bool",V "B");N("Int",V "B");N("`$B",V "A"); P(V "A", "Int | Bool")]],
252 253 254 255
    mk_s [
      [N("`$B", V "A");P(V "A","Int | Bool");N("Int | Bool", V "B"); P(V "B","Int | Bool")]
    ];

256
  "add one", mk_s [[N("`$B", V "A");P(V "A","Int | Bool")]],
257 258 259 260 261 262 263 264 265 266 267
    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")]
    ]
];;
268 269

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

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

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

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

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

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

311 312 313 314 315 316
  [("((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")]
  ];
317 318
  [("[] -> []","Int -> `$A")], [];
  [("Bool -> Bool","Int -> `$A")], [];
Pietro Abate's avatar
Pietro Abate committed
319 320

  [("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [[]];
321

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

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

357 358
let suite =
  "tests" >::: [
359
    test_constraints;
360
    test_norm;
361
    test_merge;
362
    test_tallying;
363
  ]
364

365
let main () =
366
  OUnit.run_test_tt_main suite
367 368
;;

369
main ()