Now it's starting to work...

3 files changed, 221 insertions, 43 deletions

diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 28f9238..c47fdc7 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -20,22 +20,21 @@ end = struct
     type abs_v = ED.t * ND.t
 
     type location = {
-        id            : int;
+        id              : int;
 
-        def           : bool_expr list;   (* conjunction of formula *)
-        def_cl        : conslist;
-        is_init       : bool;
+        mutable def     : bool_expr list;   (* conjunction of formula *)
+        mutable def_cl  : conslist;
+        is_init         : bool;
 
-        f             : bool_expr;
-        cl            : conslist;
+        mutable f       : bool_expr;
+        mutable cl      : conslist;
 
         (* For chaotic iteration fixpoint *)
-        mutable star  : bool;
-        mutable in_c  : int;
-        mutable v     : abs_v;
+        mutable in_c    : int;
+        mutable v       : abs_v;
 
-        mutable out_t : int list;
-        mutable in_t  : int list;
+        mutable out_t   : int list;
+        mutable in_t    : int list;
     }
 
     type env = {
@@ -69,16 +68,23 @@ end = struct
       if is_bot (enum, num) then
         Format.fprintf fmt "⊥"
       else
-        Format.fprintf fmt "@[<hov 4>(%a,@ %a)@]" ED.print enum ND.print num
+        Format.fprintf fmt "@[<hov 1>(%a,@ %a)@]" ED.print enum ND.print num
 
     (*
       join : abs_v -> abs_v -> abs_v
+      widen : abs_v -> abs_v -> abs_v
       meet : abs_v -> abs_v -> abs_v
     *)
     let join (e1, n1) (e2, n2) =
       if is_bot (e1, n1) then (e2, n2)
       else if is_bot (e2, n2) then (e1, n1)
       else (ED.join e1 e2, ND.join n1 n2)
+
+    let widen (e1, n1) (e2, n2) =
+      if is_bot (e1, n1) then (e2, n2)
+      else if is_bot (e2, n2) then (e1, n1)
+      else (ED.join e1 e2, ND.widen n1 n2)
+
     let meet (e1, n1) (e2, n2) =
       if is_bot (e1, n1) then ED.vtop e1, ND.vbottom n1
       else if is_bot (e2, n2) then ED.vtop e2, ND.vbottom n2
@@ -87,13 +93,26 @@ end = struct
         with Bot -> e1, ND.vbottom n1
 
     (*
+      eq_v : abs_v -> abs_v -> bool
+      subset_v : abs_v -> abs_v -> bool
+    *)
+    let eq_v (a, b) (c, d) = (ND.is_bot b && ND.is_bot d) || (ED.eq a c && ND.eq b d)
+
+    let subset_v (a, b) (c, d) =
+      ND.is_bot b ||
+        (not (ND.is_bot d) && ED.subset a c && ND.subset b d)
+
+    (*
       apply_cl : abs_v -> conslist -> abs_v
     *)
     let rec apply_cl (enum, num) (ec, nc, r) =
         try
           begin match r with
           | CLTrue ->
-            (ED.apply_cl enum ec, ND.apply_cl num nc)
+            let enum =
+              fix ED.eq (fun v -> ED.apply_cl v ec) enum
+            in
+            (enum, ND.apply_cl num nc)
           | CLFalse ->
             (enum, ND.vbottom num)
           | CLAnd(a, b) ->
@@ -188,7 +207,6 @@ end = struct
             f = rstf;
             cl = conslist_of_f rstf;
 
-            star = false;
             in_c = 0;
             v = (ED.top ve.evars, ND.bottom ve.nvars);
 
@@ -205,7 +223,6 @@ end = struct
             f = nrstf;
             cl = conslist_of_f nrstf;
 
-            star = false;
             in_c = 0;
             v = (ED.top ve.evars, ND.bottom ve.nvars);
 
@@ -216,6 +233,14 @@ end = struct
 
 
     (*
+      ternary_conds : bool_expr -> bool_expr list
+    *)
+    let rec ternary_conds = function
+        | BAnd(a, b) -> ternary_conds a @ ternary_conds b
+        | BTernary(c, a, b) -> [c]
+        | _ -> []
+
+    (*
       pass_cycle : env -> edd_v -> edd_v
       unpass_cycle : env -> edd_v -> edd_v
 
@@ -276,6 +301,7 @@ end = struct
           (fun q loc ->
             loc.out_t <- [];
             loc.in_t <- [];
+            loc.in_c <- 0;
             if loc.is_init then begin
               loc.v <- apply_cl (top e) loc.cl;
               delta := q::!delta
@@ -302,24 +328,21 @@ end = struct
             j
           in
 
-          let rec iter n (i_enum, i_num) =
-            let fi_enum, fi_num = f (i_enum, i_num) in
-            let j_enum, j_num =
-              if ND.is_bot fi_num then
-                i_enum, i_num
-              else
+          let rec iter n i =
+            let fi = f i in
+            let j = 
                 if n < e.opt.widen_delay then
-                  ED.join i_enum fi_enum, ND.join i_num fi_num
+                  join i fi
                 else
-                  ED.join i_enum fi_enum, ND.widen i_num fi_num
+                  widen i fi
             in
-            if ED.eq j_enum i_enum && ND.eq j_num i_num
-              then (i_enum, i_num)
-              else iter (n+1) (j_enum, j_num)
+            if eq_v i j
+              then i
+              else iter (n+1) j
           in
           let y = iter 0 start in
-          let z = fix (fun (a, b) (c, d) -> ED.eq a c && ND.eq b d) f y in
-          Format.printf "Fixpoint: %a@." print_v z;
+          let z = fix eq_v f y in
+          (*Format.printf "Fixpoint: %a@." print_v z;*)
 
           loc.v <- z;
 
@@ -331,16 +354,17 @@ end = struct
                 (*Format.printf "u: %a@.v: %a@. w: %a@." print_v u print_v v print_v w;*)
                 let r_enum, r_num = w in
                 if not (is_bot (r_enum, r_num)) then begin
-                  Format.printf "%d -> %d with:@.  %a@." s t print_v (r_enum, r_num);
+                  (*Format.printf "%d -> %d with:@.  %a@." s t print_v (r_enum, r_num);*)
                   if not (List.mem s loc2.in_t)
                     then loc2.in_t <- s::loc2.in_t;
                   if not (List.mem t loc.out_t)
                     then loc.out_t <- t::loc.out_t;
-                  let enum, num = loc2.v in
-                  let enum2, num2 = join (enum, num) (r_enum, r_num) in
-                  if not (ED.subset enum2 enum) || not (ND.subset num2 num) then
-                  begin
-                    loc2.v <- (enum2, num2);
+                  if not (subset_v (r_enum, r_num) loc2.v) then begin
+                    if loc2.in_c < e.opt.widen_delay then
+                      loc2.v <- join (r_enum, r_num) loc2.v
+                    else
+                      loc2.v <- widen (r_enum, r_num) loc2.v;
+                    loc2.in_c <- loc2.in_c + 1;
                     if not (List.mem t !delta)
                       then delta := t::!delta
                   end
@@ -348,18 +372,28 @@ end = struct
             e.loc;
 
           delta := List.filter ((<>) s) !delta;
-        done
+        done;
+
+        (* remove useless locations *)
+        let useless = ref [] in
+        Hashtbl.iter
+          (fun i loc ->
+            if is_bot loc.v then begin
+              Format.printf "Useless location detected: q%d@." i;
+              useless := i::!useless
+            end)
+          e.loc;
+        List.iter (Hashtbl.remove e.loc) !useless
 
 
     let print_locs e =
         Hashtbl.iter
           (fun id loc ->
             Format.printf "@.";
-            Format.printf "q%d: @[<hov 4>[ %a ]@]@." id
+            Format.printf "q%d: @[<v 2>[ %a ]@]@." id
               (print_list Formula_printer.print_expr " ∧ ") loc.def;
-            (*Format.printf "F: %a@." Formula_printer.print_conslist loc.cl;*)
-            Format.printf "    @[<hv 0>%a ∧@ %a@]@."
-              ED.print (fst loc.v) ND.print (snd loc.v);
+            (*Format.printf "  F: (%a)@." Formula_printer.print_expr loc.f;*)
+            Format.printf "    %a@." print_v loc.v;
             Format.printf " -> @[<hov>[%a]@]@."
               (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
             )
@@ -368,8 +402,127 @@ end = struct
     let do_prog opt rp =
         let e = init_env opt rp in
 
-        Format.printf "@.Initializing.@.";
-        chaotic_iter e;
-        print_locs e
+        let rec iter n =
+          Format.printf "@.--------------@.Refinement #%d@." n;
+
+          chaotic_iter e;
+          print_locs e;
+
+          let qc = ref None in
+
+          (* put true or false conditions into location definition *)
+          Hashtbl.iter
+            (fun q (loc : location) ->
+              let rec iter () =
+                try
+                  let cond = List.find
+                    (fun c ->
+                      is_bot (apply_cl loc.v (conslist_of_f c))
+                      || is_bot (apply_cl loc.v (conslist_of_f (BNot c))))
+                    (ternary_conds loc.f)
+                  in
+                  let tr =
+                    if is_bot (apply_cl loc.v (conslist_of_f cond))
+                    then BNot cond
+                    else cond
+                  in
+                  loc.def <- tr::loc.def;
+                  loc.def_cl <- conslist_of_f (f_and_list loc.def);
+                  loc.f <- simplify_k [tr] loc.f;
+                  loc.f <- simplify_k (get_root_true loc.f) loc.f;
+                  loc.cl <- conslist_of_f loc.f;
+                  iter()
+                with Not_found -> ()
+              in iter ())
+            e.loc;
+
+          (* find splitting condition *)
+          Hashtbl.iter
+            (fun q (loc:location) ->
+              if !qc = None then
+              let cs = ternary_conds loc.f in
+              List.iter
+                (fun c ->
+                  let split_e_case_fold_aux cases c =
+                        match c with
+                        | BEnumCons(_, x, EItem _) ->
+                          (List.map (fun v -> BEnumCons(E_EQ, x, EItem v))
+                            (List.assoc x e.ve.evars))@cases
+                        | _ -> c::cases
+                  in
+                  let cases_t =
+                    List.fold_left split_e_case_fold_aux []
+                      (split_cases [c]) in
+                  let cases_f =
+                    List.fold_left split_e_case_fold_aux []
+                      (split_cases [BNot c]) in
+                  let cases = cases_t @ cases_f in
+                  if
+                    List.length 
+                      (List.filter
+                        (fun case ->
+                          not (is_bot (apply_cl loc.v (conslist_of_f case))))
+                        cases)
+                      >= 2
+                  &&
+                    (List.exists
+                        (fun qi ->
+                          let loci = Hashtbl.find e.loc qi in
+                          let v = apply_cl
+                            (apply_cl (pass_cycle e.ve loci.v) loc.def_cl)
+                            loc.cl in
+                          List.exists
+                            (fun case -> is_bot (apply_cl v (conslist_of_f case)))
+                            cases)
+                        loc.in_t
+                    || List.exists
+                        (fun case ->
+                          let v = apply_cl loc.v (conslist_of_f case) in
+                          List.exists
+                            (fun qo ->
+                              let loco = Hashtbl.find e.loc qo in
+                              let w = apply_cl
+                                (apply_cl (pass_cycle e.ve v) loco.def_cl)
+                                loco.cl in
+                              is_bot w)
+                            loc.out_t)
+                        cases)
+                  then
+                    qc := Some(q, c, cases_t, cases_f)
+                  )
+                cs
+            )
+            e.loc;
+
+          (*if n < 7 then*)
+            match !qc with
+            | None ->
+              Format.printf "@.Found no more possible refinement."
+            | Some (q, c, cases_t, cases_f) ->
+              Format.printf "@.Refine q%d : @[<v 2>[ %a ]@]@." q
+                (print_list Formula_printer.print_expr ", ") (cases_t@cases_f);
+
+              let loc = Hashtbl.find e.loc q in
+              Hashtbl.remove e.loc loc.id;
+
+              let handle_case cc case =
+                  if not (is_bot (apply_cl loc.v (conslist_of_f case))) then
+                    let ff = simplify_k [cc] loc.f in
+                    let ff = simplify_k (get_root_true ff) ff in
+                  
+                    let loc2 =
+                      { loc with
+                        id = (incr e.counter; !(e.counter));
+                        def = case::loc.def;
+                        def_cl = conslist_of_f (f_and_list (case::loc.def));
+                        f = ff;
+                        cl = conslist_of_f ff } in
+                    Hashtbl.add e.loc loc2.id loc2
+              in
+                List.iter (handle_case c) cases_t;
+                List.iter (handle_case (BNot c)) cases_f;
+                          
+              iter (n+1)
+        in iter 0
 
 end
diff --git a/abstract/formula.ml b/abstract/formula.ml
index f2a3bd1..5cbe0c9 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -263,3 +263,21 @@ let rec formula_replace_evars repls e =
   | x -> x
 
 
+
+(*
+  Extract all cases that make a formula true, to a limited degree
+
+  [A || B; not (A || B)] -> A; (B && (not A)); not A && not B]
+*)
+
+let rec split_cases c =
+  let c = List.map eliminate_not c in
+  let u, l = List.fold_left
+    (fun (u, l) c ->
+      match c with
+      | BOr(a, b) ->
+        true, a::(BAnd(BNot a, b))::l
+      | x -> u, x::l)
+    (false, []) c
+  in
+    if u then split_cases l else l
diff --git a/main.ml b/main.ml
index 339a433..96fb95e 100644
--- a/main.ml
+++ b/main.ml
@@ -21,6 +21,8 @@ module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND)
 
 module AI_S_Itv_DP = Abs_interp_dynpart.I
       (Enum_domain.MultiValuation)(ItvND)
+module AI_S_Rel_DP = Abs_interp_dynpart.I
+      (Enum_domain.MultiValuation)(Apron_domain.ND)
 
 (* command line options *)
 let times = ref false
@@ -33,6 +35,7 @@ let ai_rel = ref false
 let ai_itv_edd = ref false
 let ai_rel_edd = ref false
 let ai_s_itv_dp = ref false
+let ai_s_rel_dp = ref false
 let ai_root = ref "test"
 let ai_widen_delay = ref 5
 let ai_no_time_scopes = ref "all"
@@ -60,6 +63,9 @@ let options = [
     "--ai-s-itv-dp", Arg.Set ai_s_itv_dp,
         "Do abstract analysis using dynamic partitionning method, "^
         "with intervals and valuation domain for enums.";
+    "--ai-s-rel-dp", Arg.Set ai_s_rel_dp,
+        "Do abstract analysis using dynamic partitionning method, "^
+        "with Apron and valuation domain for enums.";
     "--ai-vci", Arg.Set ai_vci,
         "Verbose chaotic iterations (show state at each iteration)";
     "--ai-vvci", Arg.Set ai_vvci,
@@ -126,7 +132,7 @@ let () =
 
       if !ai_itv || !ai_rel
           || !ai_itv_edd || !ai_rel_edd
-          || !ai_s_itv_dp then
+          || !ai_s_itv_dp || !ai_s_rel_dp then
       begin
           let comma_split = Str.split (Str.regexp ",") in
           let select_f x =
@@ -161,6 +167,7 @@ let () =
           if !ai_rel_edd then AI_Rel_EDD.do_prog opt rp;
 
           if !ai_s_itv_dp then AI_S_Itv_DP.do_prog opt rp;
+          if !ai_s_rel_dp then AI_S_Rel_DP.do_prog opt rp;
       end;
 
       if !vtest then do_test_interpret prog true