DP locations defined by abstract values and not by formula.

4 files changed, 121 insertions, 92 deletions

diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 1adc430..32ed890 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -21,9 +21,9 @@ end = struct
 
     type location = {
         id              : int;
+        depth           : int;
 
-        mutable def     : bool_expr list;   (* conjunction of formula *)
-        mutable def_cl  : conslist;
+        mutable def     : abs_v;
         is_init         : bool;
 
         mutable f       : bool_expr;
@@ -108,22 +108,45 @@ end = struct
       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)
-          | CLFalse ->
-            (ED.vtop enum, ND.vbottom num)
-          | CLAnd(a, b) ->
-            let enum, num = apply_cl (enum, num) (ec, nc, a) in
-            let enum, num = apply_cl (enum, num) ([], nc, b) in
-            enum, num
-          | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
-            let a = apply_cl (enum, num) (ec@eca, nc@nca, ra) in 
-            let b = apply_cl (enum, num) (ec@ecb, nc@ncb, rb) in 
-            join a b
+        begin match r with
+        | CLTrue ->
+          begin
+            try (ED.apply_cl enum ec, ND.apply_cl num nc)
+            with Bot -> ED.vtop enum, ND.vbottom num
           end
-        with Bot -> ED.vtop enum, ND.vbottom num
+        | CLFalse ->
+          (ED.vtop enum, ND.vbottom num)
+        | CLAnd(a, b) ->
+          let enum, num = apply_cl (enum, num) (ec, nc, a) in
+          let enum, num = apply_cl (enum, num) ([], nc, b) in
+          enum, num
+        | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+          let a = apply_cl (enum, num) (ec@eca, nc@nca, ra) in 
+          let b = apply_cl (enum, num) (ec@ecb, nc@ncb, rb) in 
+          join a b
+        end
+
+    (*
+      apply_cl_all_cases : abs_v -> conslist -> abs_v list
+    *)
+    let rec apply_cl_all_cases v (ec, nc, r) =
+        match r with
+        | CLTrue ->
+          let v =
+            try ED.apply_cl (fst v) ec, ND.apply_cl (snd v) nc
+            with Bot -> ED.vtop (fst v), ND.vbottom (snd v)
+          in
+          if is_bot v then [] else [v]
+        | CLFalse ->
+          []
+        | CLAnd(a, b) ->
+          let q1 = apply_cl_all_cases v (ec, nc, a) in
+          List.flatten
+            (List.map (fun c -> apply_cl_all_cases c ([], [], b)) q1)
+        | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+          let la = apply_cl_all_cases v (ec@eca, nc@nca, ra) in 
+          let lb = apply_cl_all_cases v (ec@ecb, nc@ncb, rb) in 
+          lb@(List.filter (fun a -> not (List.exists (fun b -> eq_v a b) lb)) la)
 
 
     (* ***************************
@@ -190,17 +213,17 @@ end = struct
           loc = Hashtbl.create 2; counter = ref 2; } in
 
         (* add initial disjunction : L/must_reset = tt, L/must_reset ≠ tt *)
-        let rstc = [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] in
-        let rstf = simplify_k rstc f in
+        let rstc = BEnumCons(E_EQ, "L/must_reset", EItem bool_true) in
+        let rstf = simplify_k [rstc] f in
         let rstf = simplify_k (get_root_true rstf) rstf in
-        let nrstc = [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] in
-        let nrstf = simplify_k nrstc f in
+        let nrstc = BEnumCons(E_NE, "L/must_reset", EItem bool_true) in
+        let nrstf = simplify_k [nrstc] f in
         let nrstf = simplify_k (get_root_true nrstf) nrstf in
         Hashtbl.add env.loc 0
           {
             id = 0;
-            def = rstc;
-            def_cl = conslist_of_f (f_and_list rstc);
+            depth = 0;
+            def = apply_cl (top env) (conslist_of_f rstc);
             is_init = true;
 
             f = rstf;
@@ -215,8 +238,8 @@ end = struct
         Hashtbl.add env.loc 1
           {
             id = 1;
-            def = nrstc;
-            def_cl = conslist_of_f (f_and_list nrstc);
+            depth = 0;
+            def = apply_cl (top env) (conslist_of_f nrstc);
             is_init = false;
 
             f = nrstf;
@@ -282,23 +305,24 @@ end = struct
 
         (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
 
-    let set_target_case e v cl =
-        let tgt = (unpass_cycle e (apply_cl (top e) cl)) in
-        (*Format.printf "Target %a = %a@." Formula_printer.print_conslist cl print_v tgt;*)
-        meet v tgt
-
     (*
       print_locs : env -> unit
     *)
 
+    let print_locs_defs e =
+        Hashtbl.iter
+          (fun id loc ->
+            Format.printf "q%d: @[<v 2>%a@]@." id print_v loc.def;
+            )
+          e.loc
+
     let print_locs e =
         Hashtbl.iter
           (fun id loc ->
             Format.printf "@.";
-            Format.printf "q%d: @[<v 2>[ %a ]@]@." id
-              (print_list Formula_printer.print_expr " ∧ ") loc.def;
+            Format.printf "q%d (depth = %d):@.  D: @[<v 2>%a@]@." id loc.depth print_v loc.def;
             (*Format.printf "  F: (%a)@." Formula_printer.print_expr loc.f;*)
-            Format.printf "    %a@." print_v loc.v;
+            Format.printf "  V: %a@." print_v loc.v;
             Format.printf " -> @[<hov>[%a]@]@."
               (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
             )
@@ -325,7 +349,7 @@ end = struct
               loc.v <- bottom e)
           e.loc;
 
-        print_locs e;
+        print_locs_defs e;
 
         (* Iterate *)
         let it_counter = ref 0 in
@@ -339,11 +363,11 @@ end = struct
           let start = loc.v in
           let f i =
             (*Format.printf "I: %a@." print_v i;*)
-            let i' = set_target_case e i loc.def_cl in
+            let i' = meet i (unpass_cycle e loc.def) in
             (*Format.printf "I': %a@." print_v i';*)
             let j = join start
               (apply_cl
-                (apply_cl (pass_cycle e.ve i') loc.def_cl)
+                (meet (pass_cycle e.ve i') loc.def)
                 loc.cl) in
             (*Format.printf "J: %a@." print_v j;*)
             j
@@ -372,7 +396,7 @@ end = struct
 
           Hashtbl.iter
             (fun t loc2 ->
-                let v = apply_cl u loc2.def_cl in
+                let v = meet u loc2.def in
                 let w = apply_cl v loc2.cl in
                 (*Format.printf "u: %a@.v: %a@. w: %a@." print_v u print_v v print_v w;*)
                 if not (is_bot w) then begin
@@ -384,9 +408,9 @@ end = struct
                     then loc.out_t <- t::loc.out_t;
                   if not (subset_v w loc2.v) then begin
                     if loc2.in_c < e.opt.widen_delay then
-                      loc2.v <- join w loc2.v
+                      loc2.v <- join loc2.v w
                     else
-                      loc2.v <- widen w loc2.v;
+                      loc2.v <- widen loc2.v w;
                     loc2.in_c <- loc2.in_c + 1;
                     if not (List.mem t !delta)
                       then delta := t::!delta
@@ -438,10 +462,7 @@ end = struct
                     then BNot cond
                     else cond
                   in
-                  if not (List.mem tr loc.def) then begin
-                    loc.def <- tr::loc.def;
-                    loc.def_cl <- conslist_of_f (f_and_list loc.def);
-                  end;
+                  loc.def <- apply_cl loc.def (conslist_of_f tr);
                   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;
@@ -453,31 +474,17 @@ end = struct
           (* find splitting condition *)
           Hashtbl.iter
             (fun q (loc:location) ->
-              if !qc = None then
+              if !qc = None && loc.depth < e.opt.max_dp_depth then
               let cs = ternary_conds loc.f in
               List.iter
                 (fun c ->
-                  let split_e_case_fold_aux cases c =
-                        match c with
-                        | BEnumCons(op, x, EItem _) ->
-                          let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
-                          (List.map (fun v -> BEnumCons(E_EQ, x, EItem v))
-                            (List.filter (op x) (List.assoc x e.ve.evars)))
-                          @cases
-                        | _ -> c::cases
-                  in
-                  let cases_t =
-                    List.fold_left split_e_case_fold_aux []
-                     [c] in
-                  let cases_f =
-                    List.fold_left split_e_case_fold_aux []
-                     [eliminate_not_negate c] in
+                  let cases_t = apply_cl_all_cases (top e) (conslist_of_f c) in
+                  let cases_f = apply_cl_all_cases (top e) (conslist_of_f (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))))
+                        (fun case -> not (is_bot (meet loc.v case)))
                         cases)
                       >= 2
                   &&
@@ -485,20 +492,20 @@ end = struct
                         (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)
+                            (meet (pass_cycle e.ve loci.v) loc.def)
                             loc.cl in
                           List.exists
-                            (fun case -> is_bot (apply_cl v (conslist_of_f case)))
+                            (fun case -> is_bot (meet v case))
                             cases)
                         loc.in_t
                     || List.exists
                         (fun case ->
-                          let v = apply_cl loc.v (conslist_of_f case) in
+                          let v = meet loc.v 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)
+                                (meet (pass_cycle e.ve v) loco.def)
                                 loco.cl in
                               is_bot w)
                             loc.out_t)
@@ -510,27 +517,27 @@ end = struct
             )
             e.loc;
 
-          (*if n < 7 then*)
+          if Hashtbl.length e.loc < e.opt.max_dp_width then
             match !qc with
             | None ->
-              Format.printf "@.Found no more possible refinement."
+              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);
+                (print_list print_v ", ") (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
+                  if not (is_bot (meet loc.v 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));
+                        depth = loc.depth + 1;
+                        def = meet loc.def case;
                         f = ff;
                         cl = conslist_of_f ff } in
                     Hashtbl.add e.loc loc2.id loc2
@@ -539,6 +546,34 @@ end = struct
                 List.iter (handle_case (BNot c)) cases_f;
                           
               iter (n+1)
-        in iter 0
+        in iter 0;
+
+        (* Check guarantees *)
+        let check_guarantee (id, f) =
+          Format.printf "@[<v 4>";
+          let cl = Formula.conslist_of_f f in
+          Format.printf "%s:@ %a ⇒ ⊥  @ "
+            id Formula_printer.print_conslist cl;
+          let violate = ref [] in
+          Hashtbl.iter
+            (fun id loc ->
+              if not (is_bot (apply_cl loc.v cl)) then
+                violate := id::!violate)
+            e.loc;
+          if !violate = [] then
+            Format.printf "OK"
+          else
+            Format.printf "VIOLATED in @[<hov 2>[ %a ]@]"
+              (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") !violate;
+          Format.printf "@]@ ";
+        in
+        if e.guarantees <> [] then begin
+          Format.printf "Guarantee @[<v 0>";
+          List.iter check_guarantee e.guarantees;
+          Format.printf "@]@."
+        end
+
+
+
 
 end
diff --git a/abstract/formula.ml b/abstract/formula.ml
index a124a84..f2a3bd1 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -263,23 +263,3 @@ 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
-      | BTernary(c, a, b) ->
-        true, (BAnd(c, a))::(BAnd(BNot c, b))::l
-      | x -> u, x::l)
-    (false, []) c
-  in
-    if u then split_cases l else l
diff --git a/cmdline.ml b/cmdline.ml
index b8f8ea8..c82b35b 100644
--- a/cmdline.ml
+++ b/cmdline.ml
@@ -2,7 +2,12 @@ open Ast
 
 type cmdline_opt = {
     widen_delay       : int;
+
     disjunct          : (id -> bool);
+
     verbose_ci        : bool;
     vverbose_ci       : bool;
+
+    max_dp_width      : int;
+    max_dp_depth      : int;
 }
diff --git a/main.ml b/main.ml
index 303723d..f85f6fb 100644
--- a/main.ml
+++ b/main.ml
@@ -47,6 +47,8 @@ let ai_widen_delay = ref 5
 let ai_no_time_scopes = ref "all"
 let ai_init_scopes = ref "all"
 let ai_disj_v = ref ""
+let ai_max_dp_depth = ref 10
+let ai_max_dp_width = ref 100
 let ai_vci = ref false
 let ai_vvci = ref false
 let ifile = ref ""
@@ -91,6 +93,11 @@ let options = [
     "--ai-wd", Arg.Set_int ai_widen_delay,
         "Widening delay in abstract analysis of loops (default: 3).";
 
+    "--ai-max-dp-depth", Arg.Set_int ai_max_dp_depth,
+        "Maximum depth in the dynamic partitionning tree.";
+    "--ai-max-dp-width", Arg.Set_int ai_max_dp_width,
+        "Maximum number of dynamically partitionned locations.";
+
     "--root", Arg.Set_string ai_root,
         "Root node for abstract analysis (default: test).";
     "--no-time", Arg.Set_string ai_no_time_scopes,
@@ -178,6 +185,8 @@ let () =
               disjunct = disj;
               verbose_ci = !ai_vci;
               vverbose_ci = !ai_vvci;
+              max_dp_width = !ai_max_dp_width;
+              max_dp_depth = !ai_max_dp_depth;
           } in
           
           if !ai_itv then AI_Itv.do_prog opt rp;