tallyingTest.ml 10.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
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
  "(`$A -> Bool)", "(`$B -> `$B)", mk_s [
    [P(V "B","Empty")];
    [N("`$B",V "A");N("Bool",V "B")]
  ];
149

Pietro Abate's avatar
Pietro Abate committed
150 151 152 153
  "`$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")]];
154

Pietro Abate's avatar
Pietro Abate committed
155 156 157 158
  "(Int -> Bool)", "(`$A -> `$B)", mk_s [
    [P(V "A","Empty")];
    [P(V "A","Int");N("Bool",V "B")]
  ];
159

Pietro Abate's avatar
Pietro Abate committed
160
  "(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)", mk_s [
161 162
     [P(V "A","Empty")];
    (* All these are subsumed as less general then (A <= 0) *)
Pietro Abate's avatar
Pietro Abate committed
163 164 165 166
    [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")]
  ];
167 168 169 170 171 172

  "(`$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
173
  (*
174 175
  "([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
  *)
176

Pietro Abate's avatar
Pietro Abate committed
177
  "(`$A , `$B)","(Int , Bool)", mk_s [
178 179
    [P(V "A","Empty")];
    [P(V "B","Empty")];
Pietro Abate's avatar
Pietro Abate committed
180 181
    [P(V "A","Int");P(V "B","Bool")]
  ];
182 183 184 185 186 187 188 189 190

  "(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
191
  ];
192 193

  "(`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
Pietro Abate's avatar
Pietro Abate committed
194 195
    [P(V "A","Int");P(V "B","Int")]
  ];
196
(*
Pietro Abate's avatar
Pietro Abate committed
197 198 199
  "(`$A1 -> `$B1) -> [ `$A1 ] -> [ `$B1 ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$G", mk_s [
    [P(V "A","Empty")]
  ];
200
  *)
201

202 203
  "Int -> Bool", "`$A", mk_s [[N("Int -> Bool",V "A")]];
  "((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))",Tallying.CS.sat;
204 205
  "Bool -> Bool","Int -> `$A", Tallying.CS.unsat;
  "Int", "Bool", Tallying.CS.unsat;
206
  "Int", "Empty", Tallying.CS.unsat;
207
  "[] -> []","Int -> `$A",Tallying.CS.unsat;
Pietro Abate's avatar
Pietro Abate committed
208 209 210 211 212

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

213 214 215
]

let test_norm =
216
  "norm" >:::
217 218 219 220 221
    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
222 223
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
224
      )
Pietro Abate's avatar
Pietro Abate committed
225
    ) (norm_tests ())
226 227
;;

Pietro Abate's avatar
Pietro Abate committed
228
let merge_tests () = [
229 230 231 232 233 234 235 236 237
  "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;

238
  "quad", mk_s [[N("Bool",V "B");N("Int",V "B");N("`$B",V "A"); P(V "A", "Int | Bool")]],
239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
    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")]
    ]
];;
255 256

let test_merge =
257
  "merge" >:::
258 259 260
    List.map (fun (test,s,expected) ->
      test >:: (fun _ ->
        let result = 
261
          try
262 263 264 265
            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
266
        in
267 268
        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
        MSet.assert_equal (elem expected) (elem result)
269
      )
Pietro Abate's avatar
Pietro Abate committed
270
    ) (merge_tests ())
271 272
;;

273 274
let mk_e ll =
  List.map (fun l ->
275
    List.map (fun (V v,t) -> (Var.mk v),(parse_typ t)) l
276 277 278
  ) ll

let tallying_tests = [
Pietro Abate's avatar
Pietro Abate committed
279 280 281 282 283
  [("((Int | Bool) -> Int)", "(`$A -> `$B)")], mk_e [
    [(V "A","Empty")];
    [(V "A","Int | Bool");(V "B","Int")]
  ];

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

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

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

298 299 300 301 302 303
  [("((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")]
  ];
304 305
  [("[] -> []","Int -> `$A")], [];
  [("Bool -> Bool","Int -> `$A")], [];
Pietro Abate's avatar
Pietro Abate committed
306 307

  [("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [[]];
Pietro Abate's avatar
Pietro Abate committed
308 309 310
  
  (* map even *)
  [("(`$A -> `$B) -> [`$A] -> [`$B]","(Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int))")], [[]];
311 312 313 314 315 316
]

let test_tallying =
  let print_test l =
    String.concat ";" (List.map (fun (s,t) -> Printf.sprintf " %s \\ %s" s t) l)
  in
317
  "tallying" >:::
318 319
    List.map (fun (l,expected) ->
      (print_test l) >:: (fun _ ->
320 321 322 323 324 325
        try
          let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
          let result = Tallying.tallying l in
          let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
          SubStSet.assert_equal (elem expected) (elem result)
        with Tallying.Step1Fail -> assert_equal expected []
326 327 328 329
      )
    ) tallying_tests
;;

330 331
let suite =
  "tests" >::: [
332
    test_constraints;
333
    test_norm;
334
    test_merge;
335
    test_tallying;
336 337 338
  ]
 
let main () =
339
  OUnit.run_test_tt_main suite
340 341 342 343
;;
 
main ()