Begin implementation of EDD ; SCA implemented.

6 files changed, 536 insertions, 26 deletions

diff --git a/Makefile b/Makefile
index 93ae422..e3e5391 100644
--- a/Makefile
+++ b/Makefile
@@ -24,6 +24,7 @@ SRC= 	main.ml \
 		abstract/transform.ml \
 		\
 		abstract/abs_interp.ml \
+		abstract/abs_interp_edd.ml \
 		interpret/interpret.ml \
 
 all: $(BIN)
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index f526095..bed2f2c 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -233,7 +233,7 @@ end = struct
     *)
     let init_state opt rp =
       Format.printf "Vars: @[<hov>%a@]@.@."
-          (Ast_printer.print_list Ast_printer.print_typed_var ", ")
+          (print_list Ast_printer.print_typed_var ", ")
           rp.all_vars;
 
       let enum_vars = List.fold_left
@@ -390,7 +390,7 @@ end = struct
         incr n_ch_iter;
         Format.printf "Chaotic iteration %d: @[<hov>[%a]@]@."
             !n_ch_iter
-            (Ast_printer.print_list Formula_printer.print_id ", ") case;
+            (print_list Formula_printer.print_id ", ") case;
         
         let start = try Hashtbl.find st.env case with Not_found -> assert false in
         let start_dd = dd_singleton st.d_vars start in
@@ -465,11 +465,11 @@ end = struct
                 Format.printf "%a" ND.print_itv (ND.project num id)
               | TEnum _ ->
                 Format.printf "@[<hov>{ %a }@]"
-                  (Ast_printer.print_list Formula_printer.print_id ", ")
+                  (print_list Formula_printer.print_id ", ")
                   (ED.project enum id)
               end;
               Format.printf " when @[<hov>[%a]@]@ "
-                (Ast_printer.print_list Formula_printer.print_id ", ") case)
+                (print_list Formula_printer.print_id ", ") case)
               final.data;
             Format.printf "@]@ "
           end)
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
new file mode 100644
index 0000000..a9ecc07
--- /dev/null
+++ b/abstract/abs_interp_edd.ml
@@ -0,0 +1,500 @@
+open Ast
+open Ast_util
+open Formula
+open Typing
+
+open Util
+open Num_domain
+open Abs_interp
+
+module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
+
+    val do_prog : cmdline_opt -> rooted_prog -> unit
+
+    val test : unit -> unit
+
+end = struct
+
+
+    (*  **********************
+              EDD Domain  
+        **********************  *)
+
+    type item = string
+
+    type evar = id * item list
+    type nvar = id * bool
+
+    type varenv = {
+        evars         : evar list;
+        nvars         : nvar list;
+        ev_order      : (id, int) Hashtbl.t;
+    }
+
+    type edd =
+        | DBot
+        | DVal of int
+        | DChoice of id * (item * edd) list
+
+    type edd_v = {
+        ve            : varenv;
+        root          : edd;
+        leaves        : (int, ND.t) Hashtbl.t;
+        (* add here eventual annotations *)
+    }
+
+          
+
+    (*
+      edd_print : Format.formatter -> edd_v -> unit
+    *)
+    let edd_print fmt v =
+        let ids = Hashtbl.create 12 in
+        let n = ref 0 in
+        let rec mkid = function
+            | DChoice(_, l) as x ->
+              if not (Hashtbl.mem ids x) then begin
+                incr n; Hashtbl.add ids x !n;
+                List.iter (fun (_, x) -> mkid x) l
+              end
+            | _ -> ()
+        in mkid v.root;
+        let print_n fmt = function
+          | DBot -> Format.fprintf fmt "⊥";
+          | DVal i -> Format.fprintf fmt "v%d" i;
+          | DChoice _ as x -> Format.fprintf fmt "n%d" (Hashtbl.find ids x)
+        in
+        Format.fprintf fmt "Root: %a@." print_n v.root;
+        Hashtbl.iter
+            (fun x id -> match x with
+              | DChoice (var, l) ->
+                let p fmt (c, l) = Format.fprintf fmt "%s → %a" c print_n l in
+                Format.fprintf fmt "n%d: %s ? @[<hov>%a@]@." id var
+                    (print_list p ", ") l
+              | _ -> assert false)
+            ids;
+        Hashtbl.iter
+            (fun id v -> Format.fprintf fmt "v%d: %a@." id ND.print v)
+            v.leaves
+            
+
+
+    (*
+      edd_bot : varenv -> edd_v
+    *)
+    let edd_bot ve = { ve; root = DBot; leaves = Hashtbl.create 1 }
+
+    (*
+      edd_top : evar list -> nvar list -> edd_v
+    *)
+    let edd_top ve =
+        let leaves = Hashtbl.create 1 in
+        Hashtbl.add leaves 0 (ND.top ve.nvars);
+        { ve; root = DVal 0; leaves }
+
+    (*
+      edd_of_cons : varenv -> enum_cons -> edd_v
+    *)
+    let edd_of_cons ve (op, vid, r) =
+        let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
+
+        let leaves = Hashtbl.create 1 in
+        Hashtbl.add leaves 0 (ND.top ve.nvars);
+
+        let root = match r with
+        | EItem x ->
+          DChoice(vid,
+            List.map (fun v -> if op v x then v, DVal 0 else v, DBot)
+              (List.assoc vid ve.evars))      
+        | EIdent vid2 ->
+            let a, b =
+                if Hashtbl.find ve.ev_order vid < Hashtbl.find ve.ev_order vid2
+                  then vid, vid2
+                  else vid2, vid
+            in
+            let nb x =
+              DChoice(b,
+                List.map (fun v -> if op v x then v, DVal 0 else v, DBot)
+                  (List.assoc b ve.evars))
+            in
+            DChoice(a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
+        in
+        { ve; root; leaves }
+
+    (*
+      edd_join : edd_v -> edd_v -> edd_v
+    *)
+    let edd_join a b =
+        let ve = a.ve in
+
+        let leaves = Hashtbl.copy a.leaves in
+        let n = ref 0 in
+        Hashtbl.iter (fun i _ -> if i > !n then n := i) leaves;
+
+        let get_leaf x = 
+          let id = ref None in
+          Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
+          begin match !id with
+          | Some i -> DVal i
+          | None ->
+            incr n;
+            Hashtbl.add leaves !n x;
+            DVal (!n)
+          end
+        in
+
+        let memo_bcopy = Hashtbl.create 12 in
+        let rec bcopy nb =
+          try Hashtbl.find memo_bcopy nb
+          with Not_found -> let r =
+            match nb with
+            | DBot -> DBot
+            | DVal i -> get_leaf (Hashtbl.find b.leaves i)
+            | DChoice (v, x) ->
+              DChoice(v, List.map (fun (c, n) -> c, bcopy n) x)
+          in Hashtbl.add memo_bcopy nb r; r
+        in
+
+        let memo = Hashtbl.create 12 in
+        let rec f (na, nb) =
+          try Hashtbl.find memo (na, nb)
+          with Not_found -> let r =
+            let dq v l =
+              let _, x0 = List.hd l in
+              if List.exists (fun (_, x) -> x <> x0) l
+                then DChoice(v, l)
+                else x0
+            in
+            match na, nb with
+            | DBot, x -> bcopy x
+            | x, DBot -> x
+
+            | DChoice(va, la), DChoice(vb, lb) when va = vb ->
+              let kl = List.map2
+                  (fun (ta, ba) (tb, bb) -> assert (ta = tb);
+                    ta, f (ba, bb))
+                  la lb
+              in
+              dq va kl
+            | DChoice(va, la), DChoice(vb, lb) ->
+              let v, kl =
+                if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
+                  va, List.map (fun (k, ca) -> k, f (ca, nb)) la
+                else
+                  vb, List.map (fun (k, cb) -> k, f (na, cb)) lb
+              in
+              dq v kl
+
+            | DChoice(va, la), _ ->
+              let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in
+              dq va kl
+            | _, DChoice(vb, lb) ->
+              let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in
+              dq vb kl
+
+            | DVal u, DVal v ->
+              let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+              get_leaf x
+          in Hashtbl.add memo (na, nb) r; r
+        in
+        { leaves; ve; root = f (a.root, b.root) }
+
+    (*
+      edd_meet : edd_v -> edd_v -> edd_v
+    *)
+    let edd_meet a b =
+        let ve = a.ve in
+
+        let n = ref 0 in
+        let leaves = Hashtbl.create 12 in
+
+        let get_leaf x = 
+          if ND.is_bot x then DBot else begin
+            let id = ref None in
+            Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
+            match !id with
+            | Some i -> DVal i
+            | None ->
+              incr n;
+              Hashtbl.add leaves !n x;
+              DVal (!n)
+          end
+        in
+
+        let memo = Hashtbl.create 12 in
+        let rec f (na, nb) =
+          try Hashtbl.find memo (na, nb)
+          with Not_found -> let r =
+            let dq v l =
+              let _, x0 = List.hd l in
+              if List.exists (fun (_, x) -> x <> x0) l
+                then DChoice(v, l)
+                else x0
+            in
+            match na, nb with
+            | DBot, _ | _, DBot -> DBot
+            | DChoice(va, la), DChoice(vb, lb) when va = vb ->
+              let kl = List.map2
+                  (fun (ta, ba) (tb, bb) -> assert (ta = tb);
+                    ta, f (ba, bb))
+                  la lb
+              in
+              dq va kl
+            | DChoice(va, la), DChoice(vb, lb) ->
+              let v, kl =
+                if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
+                  va, List.map (fun (k, ca) -> k, f (ca, nb)) la
+                else
+                  vb, List.map (fun (k, cb) -> k, f (na, cb)) lb
+              in
+              dq v kl
+            | DChoice(va, la), _ ->
+              let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in
+              dq va kl
+            | _, DChoice(vb, lb) ->
+              let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in
+              dq vb kl
+            | DVal u, DVal v ->
+              let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+              get_leaf x
+          in Hashtbl.add memo (na, nb) r; r
+        in
+        { leaves; ve; root = f (a.root, b.root) }
+
+    (*
+      edd_of_conslist : varenv -> enum_cons list -> edd_v
+
+      Does this by dichotomy so that the EDD meets are done mostly on
+      small sized EDDs.
+    *)
+    let rec edd_of_conslist ve = function
+      | [] -> edd_top ve
+      | [a] -> edd_of_cons ve a
+      | l ->
+        let rec split = function
+          | [] -> [], []
+          | [a] -> [a], []
+          | a::b::q -> let u, v = split q in a::u, b::v
+        in
+        let u, v = split l in
+        edd_meet (edd_of_conslist ve u) (edd_of_conslist ve v)
+
+
+    let test () =
+        let ve = {
+            evars = ["x", ["tt"; "ff"]; "y", ["tt"; "ff"]; "z", ["tt"; "ff"]];
+            nvars = [];
+            ev_order = Hashtbl.create 2 } in
+        Hashtbl.add ve.ev_order "x" 0;
+        Hashtbl.add ve.ev_order "y" 1;
+        Hashtbl.add ve.ev_order "z" 2;
+        let u = edd_of_cons ve (E_EQ, "x", EIdent "y") in
+        Format.printf "x = y : @[%a@]@." edd_print u;
+        let v = edd_of_cons ve (E_NE, "y", EIdent "z") in
+        Format.printf "y != z : @[%a@]@." edd_print v;
+        let w = edd_meet u v in
+        Format.printf "x = y && y != z : @[%a@]@." edd_print w;
+        let t = edd_join u v in
+        Format.printf "x = y || y != z : @[%a@]@." edd_print t
+
+
+    (* ******************************
+            Abstract interpret
+      ******************************* *)
+    
+    type env = {
+        rp          : rooted_prog;
+        opt         : cmdline_opt;
+
+        ve          : varenv;
+
+        (* program expressions *)
+        f           : bool_expr;
+        cl          : conslist;
+        f_g         : bool_expr;
+        cl_g        : conslist;
+        guarantees  : (id * bool_expr) list;
+
+        (* abstract interpretation *)
+        cycle       : (id * id * typ) list;     (* s'(x) = s(y) *)
+        forget      : (id * typ) list;          (* s'(x) not specified *)
+    }
+
+    (*
+      extract_linked_evars : conslist -> (id * id) list
+
+      Extract all pairs of enum-type variable (x, y) appearing in an
+      equation like x = y or x != y
+
+      A couple may appear several times in the result.
+    *)
+    let rec extract_linked_evars (ecl, _, r) =
+        let v_ecl = List.fold_left
+            (fun c (_, x, v) -> match v with
+                | EIdent y -> (x, y)::c
+                | _ -> c)
+            [] ecl
+        in
+        let v_ecl2 =
+          let q = List.fold_left
+            (fun c (_, x, v) -> match v with
+              | EItem _ -> x::c | _ -> c)
+            [] ecl
+          in
+          match q with
+          | [x; y] -> [x, y]
+          | _ -> []
+        in
+        let rec aux = function
+          | CLTrue | CLFalse -> []
+          | CLAnd(a, b) -> aux a @ aux b
+          | CLOr(a, b) -> extract_linked_evars a @ extract_linked_evars b
+        in
+        v_ecl @ v_ecl2 @ aux r
+
+    (*
+      scope_constrict : id list -> (id * id) list -> id list
+
+      Orders the variable in the first argument such as to minimize the
+      sum of the distance between the position of two variables appearing in
+      a couple of the second list. (minimisation is approximate, this is
+      an heuristic so that the EDD will not explode in size when expressing
+      equations such as x = y && u = v && a != b)
+    *)
+    let scope_constrict vars cp_id =
+        let var_i = Array.of_list vars in
+        let n = Array.length var_i in
+
+        let i_var = Hashtbl.create n in
+        Array.iteri (fun i v -> Hashtbl.add i_var v i) var_i;
+
+        let cp_i = List.map
+          (fun (x, y) -> Hashtbl.find i_var x, Hashtbl.find i_var y)
+          cp_id in
+
+        let eval i =
+          let r = Array.make n (-1) in
+          Array.iteri (fun pos var -> r.(var) <- pos) i;
+          Array.iteri (fun _ x -> assert (x <> (-1))) r;
+          List.fold_left
+            (fun s (x, y) -> s + abs (r.(x) - r.(y)))
+            0 cp_i
+        in
+
+        let best = Array.make n 0 in
+        for i = 0 to n-1 do best.(i) <- i done;
+
+        let usefull = ref true in
+        Format.printf "SCA";
+        while !usefull do
+          Format.printf ".@?";
+
+          usefull := false;
+          let try_s x =
+            if eval x < eval best then begin
+              Array.blit x 0 best 0 n;
+              usefull := true
+            end
+          in
+
+          for i = 0 to n-1 do
+            let tt = Array.copy best in
+            (* move item i at beginning *)
+            let temp = tt.(i) in
+            for j = i downto 1 do tt.(j) <- tt.(j-1) done;
+            tt.(0) <- temp;
+            (* try all positions *)
+            try_s tt;
+            for j = 1 to n-1 do
+              let temp = tt.(j-1) in
+              tt.(j-1) <- tt.(j);
+              tt.(j) <- temp;
+              try_s tt
+            done
+          done
+        done;
+        Format.printf "@.";
+
+        Array.to_list (Array.map (Array.get var_i) best)
+
+    (*
+      init_env : cmdline_opt -> rooted_prog -> env
+    *)
+    let init_env opt rp =
+        Format.printf "Vars: @[<hov>%a@]@.@."
+            (print_list Ast_printer.print_typed_var ", ")
+            rp.all_vars;
+
+        let enum_vars = List.fold_left
+            (fun v (_, id, t) -> match t with
+                | TEnum ch -> (id, ch)::v | _ -> v)
+            [] rp.all_vars in
+        let num_vars = List.fold_left
+            (fun v (_, id, t) -> match t with
+                | TInt -> (id, false)::v | TReal -> (id, true)::v | _ -> v)
+            [] rp.all_vars in
+
+        let init_f = Transform.init_f_of_prog rp in
+        Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
+        let init_cl = conslist_of_f init_f in
+
+        let guarantees = Transform.guarantees_of_prog rp in
+        Format.printf "Guarantees:@.";
+        List.iter (fun (id, f) ->
+            Format.printf "  %s: %a@." id Formula_printer.print_expr f)
+          guarantees;
+        Format.printf "@.";
+
+        let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
+        let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
+        Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
+
+        let cl = Formula.conslist_of_f f in
+        let cl_g = Formula.conslist_of_f f_g in
+
+        (* calculate order for enumerated variables *)
+        let evars = List.map fst enum_vars in
+
+        let lv0 = List.map (fun x -> x, "N"^x)
+            (List.filter (fun x -> List.exists (fun y -> y = "N"^x) evars) evars) in
+        let lv = lv0 @ extract_linked_evars init_cl @ extract_linked_evars cl_g in
+        let lv = uniq_sorted
+             (List.sort Pervasives.compare (List.map ord_couple lv)) in
+        let evars_ord = scope_constrict evars (lv0 @ lv) in
+
+        let ev_order = Hashtbl.create (List.length evars) in
+        List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
+        let ve = { evars = enum_vars; nvars = num_vars; ev_order } in
+
+        Format.printf "Order for variables: @[<hov>[%a]@]@."
+          (print_list Formula_printer.print_id ", ") evars_ord;
+
+        (* calculate cycle variables and forget variables *)
+        let cycle = List.fold_left
+          (fun q (_, id, ty) ->
+              if id.[0] = 'N' then
+                (String.sub id 1 (String.length id - 1), id, ty)::q
+              else q)
+          [] rp.all_vars
+        in
+        let forget = List.map (fun (_, id, ty) -> (id, ty))
+            (List.filter
+              (fun (_, id, _) ->
+                not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars))
+              rp.all_vars)
+        in
+
+        { rp; opt; ve;
+          f; cl; f_g; cl_g; guarantees;
+          cycle; forget }
+
+          
+
+
+    let do_prog opt rp =
+        let e = init_env opt rp in
+        ()
+
+end
+
+
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index b6c06fb..9a4d62d 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -1,6 +1,7 @@
 open Ast
 open Lexing
 open Typing
+open Util
 
 
 (* Locations *)
@@ -69,14 +70,6 @@ let expr_precedence = function
 
 (* utility *)
 
-let print_list f sep fmt l =
-  let rec aux = function
-    | [] -> ()
-    | [a] -> f fmt a
-    | a::b -> f fmt a; Format.fprintf fmt "%s@," sep; aux b
-  in
-  aux l
-
 let print_id_ext fmt (i, _) =
   Format.pp_print_string fmt i
 
diff --git a/libs/util.ml b/libs/util.ml
index 01b0c5c..443fb1e 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -1,3 +1,21 @@
+(* Small things *)
+
+let ord_couple (a, b) = if a < b then a, b else b, a
+
+(* uniq_sorted : 'a list -> 'a list *)
+let rec uniq_sorted = function
+  | [] -> []
+  | [a] -> [a]
+  | a::b::q when a = b -> uniq_sorted (b::q)
+  | a::r -> a::(uniq_sorted r)
+
+(* list_fold_op : ('a -> 'a -> 'a) -> 'a list -> 'a *)
+let rec list_fold_op op = function
+  | [] -> invalid_arg "list_fold_opt on empty list"
+  | [a] -> a
+  | x::q -> op x (list_fold_op op q)
+
+
 (* Either type *)
 
 type ('a, 'b) either =
@@ -47,24 +65,15 @@ let rec fix equal f s =
 
 let (@@) f x = f x
 
-let print_list x l =
-  Format.printf "%s: " x;
+let print_list f sep fmt l =
   let rec aux = function
     | [] -> ()
-    | [a] -> Format.printf "%s" a
-    | p::q -> Format.printf "%s, " p; aux q
+    | [a] -> f fmt a
+    | a::b -> f fmt a; Format.fprintf fmt "%s@," sep; aux b
   in
-  Format.printf "["; aux l; Format.printf "]@."
+  aux l
 
 let uid =
   let c = ref 0 in
   fun () -> c := !c + 1; string_of_int !c
 
-(* On lists *)
-
-(* list_fold_op : ('a -> 'a -> 'a) -> 'a list -> 'a *)
-let rec list_fold_op op = function
-  | [] -> invalid_arg "list_fold_opt on empty list"
-  | [a] -> a
-  | x::q -> op x (list_fold_op op q)
-
diff --git a/main.ml b/main.ml
index 2e4eb49..667ffed 100644
--- a/main.ml
+++ b/main.ml
@@ -12,6 +12,8 @@ module ItvND = Nonrelational.ND(Intervals_domain.VD)
 module AI_Itv = Abs_interp.I(Enum_domain.Valuation)(ItvND)
 module AI_Rel = Abs_interp.I(Enum_domain.Valuation)(Apron_domain.ND)
 
+module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
+
 (* command line options *)
 let dump = ref false
 let dumprn = ref false
@@ -19,6 +21,7 @@ let test = ref false
 let vtest = ref false
 let ai_itv = ref false
 let ai_rel = ref false
+let ai_itv_edd = ref false
 let ai_root = ref "test"
 let ai_widen_delay = ref 3
 let ai_no_time_scopes = ref ""
@@ -36,6 +39,7 @@ let options = [
     "--test", Arg.Set test, "Simple testing (direct interpret).";
     "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals.";
     "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron.";
+    "--ai-itv-edd", Arg.Set ai_itv_edd, "Do abstract analysis using intervals and EDD disjunction domain.";
     "--ai-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)";
     "--wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3).";
     "--root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test).";
@@ -78,6 +82,8 @@ let do_test_interpret prog verbose =
 let () =
     Arg.parse options (fun f -> ifile := f) usage;
 
+    AI_Itv_EDD.test ();
+
     if !ifile = "" then begin
         Format.eprintf "No input file...@.";
         exit 1
@@ -90,7 +96,7 @@ let () =
       let prog = Rename.rename_prog prog in
       if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
 
-      if !ai_itv || !ai_rel then begin
+      if !ai_itv || !ai_rel || !ai_itv_edd then begin
           let comma_split = Str.split (Str.regexp ",") in
           let select_f x =
               if x = "all"
@@ -111,6 +117,7 @@ let () =
           
           if !ai_itv then AI_Itv.do_prog opt rp;
           if !ai_rel then AI_Rel.do_prog opt rp;
+          if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
       end;
 
       if !vtest then do_test_interpret prog true