Clean up & comment a bit.

1 files changed, 40 insertions, 21 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 31fe5aa..722dc1a 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -26,6 +26,27 @@ end = struct
     (*  **********************
               EDD Domain  
         **********************  *)
+
+    (*
+      This abstract domain is capable of representing values of a program using enumerated
+      variables and numerical variables. The representation is a decision graph on
+      enumerated variables, whose leaves are values for the numerical variables in a given
+      numerical domain (relationnal or non-relationnal). This domain necessarily does the
+      disjunction between all the cases that appear for the enumerated variables, and is
+      not able to do a disjunction with respect to a condition on numerical variables if
+      that condition is not bound to a boolean variable appearing in the program.
+
+      Possible extensions :
+      - use groups of variables, so that an EDD does not have to consider all the
+        numerical and enumerated variables at once
+      - add the possibility for numeric condition decision nodes (something like ghost
+        boolean variables that would be bound to a numeric condition)
+      - ...
+
+      This domain is currently the most promising lead in our research on abstract
+      interpretation of Scade programs.
+    *)
+
     type edd =
         | DBot
         | DTop
@@ -479,10 +500,10 @@ end = struct
         let ve = v.ve in
 
         let leaves, get_leaf = get_leaf_fun () in
+        let dq = new_node_fun () in
 
-        let nc = ref 0 in
         let memo = Hashtbl.create 12 in
-        let node_memo = Hashtbl.create 12 in
+
         let rec f l =
             let kl = List.sort Pervasives.compare (List.map key l) in
             try Hashtbl.find memo kl
@@ -522,16 +543,7 @@ end = struct
                         let ch3 = List.map (fun (_, _, cl) -> List.assoc c cl) d in
                         c, f (ch1@ch2@ch3))
                       cl in
-                    let _, x0 = List.hd cc in
-                    if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) cc
-                    then begin
-                      let k = (dv, List.map (fun (a, b) -> a, key b) cc) in
-                      let n =
-                        try Hashtbl.find node_memo k
-                        with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc)
-                      in
-                      DChoice(n, dv, cc)
-                    end else x0
+                    dq dv cc
               with | Top -> DTop
             in Hashtbl.add memo kl r; r
         in
@@ -616,7 +628,7 @@ end = struct
 
 
     (*
-      edd_join_widen : edd_v -> edd_v -> edd_v
+      edd_widen : edd_v -> edd_v -> edd_v
     *)
     let edd_widen (a:edd_v) (b:edd_v) =
         let ve = a.ve in
@@ -658,7 +670,7 @@ end = struct
 
           | _ -> assert false
         in
-        { leaves; ve; root = time "join/W" (fun () -> memo2 f a.root b.root) }
+        { leaves; ve; root = time "widen" (fun () -> memo2 f a.root b.root) }
 
     (*
       edd_accumulate : edd_v -> edd_v -> edd_v
@@ -703,7 +715,7 @@ end = struct
 
           | _ -> assert false
         in
-        { leaves; ve; root = time "join/*" (fun () -> memo2 f a.root b.root) }
+        { leaves; ve; root = time "accumulate" (fun () -> memo2 f a.root b.root) }
 
     (*
       edd_star_new : edd_v -> edd_v -> edd_v
@@ -775,9 +787,11 @@ end = struct
         let f = simplify_k (get_root_true f) f in
         Format.printf "Complete formula:@.%a@.@." Formula_printer.print_expr f;
 
-        (* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *)
-        (* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *)
-        (* WHY THE **** AM I SHOUTING LIKE THAT ? *)
+        (*
+          Here we simplify the program formula so that uselessly redundant variables don't
+          appear anymore. If an enumerated equation x = y appears at the root of the
+          program, then we chose to remove either x or y.
+        *)
         let facts = get_root_true f in
         let f, rp, repls = List.fold_left
           (fun (f, (rp : rooted_prog), repls) eq ->
@@ -814,6 +828,11 @@ end = struct
         Format.printf "Complete formula after simpl:@.%a@.@."
             Formula_printer.print_expr f;
 
+        (*
+          Here we specialize the program formula for the two following cases :
+          - L/must_reset = tt, this is the first instant of the program (global reset)
+          - L/must_reset = ff, this is for all the rest of the time
+        *)
         let init_f = simplify_k [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] f in
         let f = simplify_k [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] f in
 
@@ -839,10 +858,8 @@ end = struct
         
         let ve = mk_varenv rp f cl in
 
-
         { rp; opt; ve; init_cl; cl; guarantees; }
 
-          
 
 
     let do_prog opt rp =
@@ -925,8 +942,10 @@ end = struct
         let init_acc = edd_star_new (edd_bot e.ve)
             (pass_cycle e.ve (edd_apply_cl (edd_top e.ve) e.init_cl)) in
         
-        (* Dump final state *)
+        (* Iterate *)
         let acc = ch_it 0 init_acc in
+
+        (* Dump final state *)
         edd_dump_graphviz acc "/tmp/graph-final0.dot";
 
         Format.printf "Finishing up...@.";