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 ()