Fix pesky problem with UnitTests for Tallying.norm

- add tests for basic data structures of the Tallying algorithm
- Fix all tests for norm (finally converging)

tests/libtest/tallyingTest.ml

@@ -8,80 +8,199 @@ let parse_typ s =
   Types.descr nodepat
 ;;
 
-let union = Tallying.CS.union
-let prod = Tallying.CS.prod
-let singleton = Tallying.CS.singleton
+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)
+  let pp_printer ppf (`Var v,t) = Format.fprintf ppf "(%s = %s)" v (to_string Print.print t)
+  let pp_print_sep = OUnitDiff.pp_comma_separator
+end)
 
-let mk_pos (alpha,t) = singleton (Tallying.Pos (`Var alpha,parse_typ t))
-let mk_neg (t,alpha) = singleton (Tallying.Neg (parse_typ t,`Var alpha))
+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
+  let pp_printer = Tallying.CS.print_m
+  let pp_print_sep = OUnitDiff.pp_comma_separator
+end)
+
+let mk_pos (alpha,t) = Tallying.CS.singleton (Tallying.Pos (`Var alpha,parse_typ t))
+let mk_neg (t,alpha) = Tallying.CS.singleton (Tallying.Neg (parse_typ t,`Var alpha))
 
 type pp = P of vv * string | N of string * vv
 and vv = V of string
 
+let mk_pp = function
+  |P(V alpha,t) -> Tallying.CS.singleton (Tallying.Pos (`Var alpha,parse_typ t))
+  |N(t,V alpha) -> Tallying.CS.singleton (Tallying.Neg (parse_typ t,`Var alpha))
+
+let mk_prod l =
+    List.fold_left (fun acc2 c ->
+      Tallying.CS.prod (mk_pp c) acc2
+    ) Tallying.CS.sat l
+
+let mk_union l1 l2 =
+  Tallying.CS.union (mk_prod l1) (mk_prod l2)
+
 let mk_s ll =
   List.fold_left (fun acc1 l ->
-    let x = 
-      List.fold_left (fun acc2 -> function
-        |P(V a,b) -> Tallying.CS.prod (mk_pos (a,b)) acc2
-        |N(a,V b) -> Tallying.CS.prod (mk_neg (a,b)) acc2
-      ) Tallying.CS.S.empty l
-    in Tallying.CS.union x acc1
+    Tallying.CS.union (mk_prod l) acc1
   ) Tallying.CS.S.empty ll
 
+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
+    |((_,v),Some x,Some y) when Types.equal x y -> Some x
+    |((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
+      |P(V v,s) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (true,`Var v) (parse_typ s))
+      |N(s,V v) -> Tallying.CS.M.merge aux_merge acc (Tallying.CS.M.singleton (false,`Var v) (parse_typ s))
+    ) 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))
+
+
 (* check invariants on the constraints sets *)
-let constraints_test = [];;
+let test_constraint_ops = [
+
+  "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")];
+
+]
 
-(* ^ => | -- v => & *)
+let test_constraints =
+  "test tallying data structures" >:::
+    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)
+      )
+    ) test_constraint_ops
+;;
+
+(* ^ => & -- v => | *)
 
 let norm_tests = [
   "(`$A -> Bool)", "(`$B -> `$B)", mk_s [
     [P(V "B","Empty")];
     [N("`$B",V "A");N("Bool",V "B")]
   ];
+
   "`$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")]];
+
   "(Int -> Bool)", "(`$A -> `$B)", mk_s [
     [P(V "A","Empty")];
     [P(V "A","Int");N("Bool",V "B")]
   ];
+
   "(Int -> Int) | (Bool -> Bool)", "(`$A -> `$B)", mk_s [
     [P(V "A","Empty")];
     [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")]
   ];
+
+  "(`$A -> `$B)", "(Int -> Int) | (Bool -> Bool)", mk_s [
+    [P(V "B","Int");N("Int",V "A")];
+    [P(V "B","Bool");N("Bool",V "A")];
+  ];
+
   (*
   "([0--*] & `true)", "(`$A | Int) & ((Any \\ `$A) | Bool)",
   *)
+
   "(`$A , `$B)","(Int , Bool)", mk_s [
+    [P(V "A","Empty")];
+    [P(V "B","Empty")];
     [P(V "A","Int");P(V "B","Bool")]
   ];
-  "(`$A & (`$B , `$C))","(Int , Int)", mk_s [
-    [P(V "A","(Int , Int) | (Any \\ (`$B , `$C))")]
+
+  "(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")];
+
   ];
-  "(`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))", mk_s [
+
+  "(`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
     [P(V "A","Int");P(V "B","Int")]
   ];
+
   "(`$A1 -> `$B1) -> [ `$A1 ] -> [ `$B1 ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$G", mk_s [
     [P(V "A","Empty")]
   ];
 ]
 
-(* the abstract field is ignored in the comparison *)
-let m_compare = 
-  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
-
-module MList = OUnitDiff.ListSimpleMake (struct 
-  type t = Tallying.CS.m
-  let compare = m_compare
-  let pp_printer = Tallying.CS.print_m
-  let pp_print_sep = OUnitDiff.pp_comma_separator
-end)
-
 let test_norm =
   "test tallying norm" >:::
     List.map (fun (s,t,expected) ->
@@ -89,14 +208,14 @@ let test_norm =
         let s = parse_typ s in
         let t = parse_typ t in
         let result = Tallying.norm (diff s t) in
-        let elem s = List.sort m_compare (Tallying.CS.S.elements s) in
-        MList.assert_equal (elem expected) (elem result)
+        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
+        MSet.assert_equal (elem expected) (elem result)
       )
     ) norm_tests
 ;;
 
 let merge_tests = [
-  [("`$A", "Empty");("`$B", "Empty")], prod (mk_pos ("A", "Empty")) (mk_pos ("B", "Empty"));
+  [("`$A", "Empty");("`$B", "Empty")], Tallying.CS.prod (mk_pos ("A", "Empty")) (mk_pos ("B", "Empty"));
   [("`$A", "Int | Bool");("Int","`$B");("`$B", "Empty")], Tallying.CS.unsat;
   [("Bool","`$B"); ("`$B", "`$A"); ("`$A", "Empty")], Tallying.CS.unsat;
   [("Bool","`$B"); ("Int","`$B"); ("`$B","`$A"); ("`$A", "Int | Bool")],
@@ -130,38 +249,12 @@ let test_merge =
           try Tallying.CS.union (Tallying.merge c) acc with Tallying.UnSatConstr -> acc
           ) n Tallying.CS.S.empty
         in
-        let elem s = List.sort m_compare (Tallying.CS.S.elements s) in
-        MList.assert_equal (elem expected) (elem result)
+        let elem s = MSet.of_list (Tallying.CS.S.elements s) in
+        MSet.assert_equal (elem expected) (elem result)
       )
     ) merge_tests
 ;;
 
-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 *)
-let compare_constr (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)
-
-module EList = OUnitDiff.ListSimpleMake (struct 
-  type t = (Var.var * Types.t)
-  let compare = compare_constr
-  let pp_printer ppf (`Var v,t) = Format.fprintf ppf "(%s = %s)" v (to_string Print.print t)
-  let pp_print_sep = OUnitDiff.pp_comma_separator
-end)
-
-module SubSet = OUnitDiff.SetMake (struct 
-  type t = EList.t
-  let compare a b = EList.compare a b
-  let pp_printer ppf l = EList.pp_printer ppf l
-  let pp_print_sep = OUnitDiff.pp_comma_separator
-end)
-
 let mk_e ll =
   List.map (fun l ->
     List.map (fun (v,t) -> (`Var v),(parse_typ t)) l
@@ -187,14 +280,15 @@ let test_tallying =
       (print_test l) >:: (fun _ ->
         let l = List.map (fun (s,t) -> (parse_typ s,parse_typ t)) l in
         let result = Tallying.tallying l in
-        let elem s = SubSet.of_list (List.map (fun l -> EList.of_list (List.sort compare_constr l)) s) in
-        SubSet.assert_equal (elem expected) (elem result)
+        let elem s = SubStSet.of_list (List.map (fun l -> ESet.of_list l) s) in
+        SubStSet.assert_equal (elem expected) (elem result)
       )
     ) tallying_tests
 ;;
 
 let all =
   "all tests" >::: [
+    test_constraints;
     test_norm;
     test_merge;
     test_tallying;

types/types.ml

@@ -2344,7 +2344,7 @@ module Tallying = struct
     (* Inv : a map contains only on binding for each variable *)
     let merge m1 m2 =
       let f k v1 v2 = match (k,v1,v2) with
-        |(k,None,None) -> None
+        |(k,None,None) -> assert false
         |(k,Some v,None) -> Some v
         |(k,None,Some v) -> Some v
         |((_,v),Some x,Some y) when Descr.equal x y -> Some x
@@ -2359,23 +2359,14 @@ module Tallying = struct
     (* m1 is less general than m2 if for all elements (alpha,s) of
      * m1 there is a correspoding element (alpha,t) in m2 such that
      * s <= t . In this case m2 is a more restrictive constraint set
-     * then m1 *)
-    let lessgeneral m1 m2 acc =
-      let test m1 m2 = (* m1 is less general them m2 *)
-        M.for_all (fun k1 t1 ->
-          M.exists (fun k2 t2 -> (Var.equal k1 k2) && (subtype t1 t2)) m2
-        ) m1
-      in
-
-      if M.is_empty m1 then S.add m2 acc
-      else if M.is_empty m2 then S.add m1 acc else
-      if (M.compare compare m1 m2) = 0 then S.add m1 acc
-
-      (* m1 is less general them m2 *)
-      else if test m1 m2 then S.add m2 acc
-      (* m2 is less general them m1 *)
-      else if test m2 m1 then S.add m1 acc
-      else S.add m1 (S.add m2 acc)
+     * then m1 . m1 < m2 *)
+    let lessgeneral m1 m2 =
+      M.for_all (fun (b1,v1) s ->
+        M.exists (fun (b2,v2) t -> 
+          (b1 == b2) && (Var.equal v1 v2) &&
+          (if b1 then (subtype t s) else (subtype s t))
+        ) m2
+      ) m1
 
     (* this is O(n^2) filter . Only more restritive constraints sets are kept *)
     let union x y =
@@ -2386,9 +2377,17 @@ module Tallying = struct
       |false,false ->
           S.fold (fun m1 acc ->
             S.fold (fun m2 acc1 ->
-              lessgeneral m1 m2 acc1
+              if (M.compare Descr.compare m1 m2) = 0 then S.add m1 acc1 else
+              if M.is_empty m1 then S.add m2 acc1 else
+              if M.is_empty m2 then S.add m1 acc1 else
+              begin match (lessgeneral m1 m2),(lessgeneral m2 m1) with
+              |true,true -> S.add m1 acc1 (* equivalent *)
+              |true,false -> S.add m1 acc1 (* m1 < m2 ==> discard m2 *)
+              |false,true -> S.add m2 acc1 (* m2 < m1 ==> discard m1 *)
+              |false,false -> S.add m1 (S.add m2 acc1) (* m1 <> m2 ==> we add both *)
+              end
             ) y acc
-          ) x y
+          ) x S.empty
 
     (* cartesian product of two sets of contraints sets where each
      * resulting constraint set is than merged *)
@@ -2399,14 +2398,14 @@ module Tallying = struct
       |true,false -> y
       |false,false ->
         S.fold (fun m1 acc ->
-          S.fold (fun m2 acc1 -> S.add (merge m1 m2) acc1) y acc
+          S.fold (fun m2 acc1 -> union (S.singleton (merge m1 m2)) acc1) y acc
         ) x S.empty
 
   end
 
-  let normatoms (t,_) = if Atoms.is_empty t then CS.sat else raise UnSatConstr
-  let normchars (t,_) = if Chars.is_empty t then CS.sat else raise UnSatConstr
-  let normints (t,_) = if Intervals.is_empty t then CS.sat else raise UnSatConstr
+  let normatoms (t,_) = if Atoms.is_empty t then CS.sat else CS.unsat (* raise UnSatConstr *)
+  let normchars (t,_) = if Chars.is_empty t then CS.sat else CS.unsat (* raise UnSatConstr *)
+  let normints (t,_) = if Intervals.is_empty t then CS.sat else CS.unsat (* raise UnSatConstr *)
 
   let single_aux constr (b,v,p,n) =
     let aux f constr acc l = 
@@ -2457,8 +2456,8 @@ module Tallying = struct
           CS.singleton (Neg (t,`Var y))
 
     |([`Atm a], (`Var x)::neg) -> 
-          let t = single (false,x,p,neg) in
-          CS.singleton (Neg (t,`Var x))
+        let t = single (false,x,p,neg) in
+        CS.singleton (Neg (t,`Var x))
 
     |([`Atm t], []) -> norm_rec (t,mem)
     |([],[`Atm t]) -> failwith "impossible0" (* norm_rec (t,mem) *)
@@ -2469,6 +2468,7 @@ module Tallying = struct
     |_,_ -> failwith "impossible4"
 
   let rec norm ( (t,m) : (s * DescrSet.t)) =
+    Format.printf "Norm of %a\n" Print.print t;
     if DescrSet.mem t m then CS.sat else begin
       let aux_base single norm_aux acc l = 
         List.fold_left (fun acc (pos,neg) ->