Clean up & comment a bit.

23 files changed, 305 insertions, 474 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index b5fc684..319f105 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -3,6 +3,7 @@ open Ast_util
 open Formula
 open Typing
 open Cmdline
+open Varenv
 
 open Util
 open Num_domain
@@ -12,8 +13,6 @@ open Enum_domain
 
 module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
 
-    type st
-
     val do_prog : cmdline_opt -> rooted_prog -> unit
 
 end = struct
@@ -22,6 +21,14 @@ end = struct
             Disjunction domain 
         **************************  *)
 
+    (*
+      This domain uses a fix set of enumerate-type variables to make disjunctions between
+      different cases that are analyzed. A case is a list of values for each of these
+      disjunction variables. The value for that case is the product of a value in a domain
+      specific for enumerated variables and a domain for numeric variables. See README for
+      more details.
+    *)
+
     type case_v = ED.t * ND.t
     type case = ED.item list
 
@@ -291,7 +298,7 @@ end = struct
 
       (* add variables from LASTs *)
       let last_vars = uniq_sorted
-        (List.sort compare (Transform.extract_last_vars f)) in
+        (List.sort compare (extract_last_vars f)) in
       let last_vars = List.map
         (fun id ->
           let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 5beffda..23df612 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -19,6 +19,15 @@ end = struct
 
     type abs_v = ED.t * ND.t
 
+    (*
+      Abstract analysis based on dynamic partitionning of the state space.
+      Idea : use somme conditions appearing in the text of the program as
+      disjunctions. We don't want to consider them all at once  in the first
+      place because it would be way too costly ; instead we try to dynamically
+      partition tye system. But we haven't got a very good heuristic for that,
+      so it doesn't work very well.
+    *)
+
     type location = {
         id              : int;
         depth           : int;
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...@.";
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index 288f961..a929c0b 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -6,6 +6,11 @@ open Num_domain
 
 open Apron
 
+(*
+  Link between our NUMERICAL_ENVIRONMENT_DOMAIN interface and Apron.
+  Mostly direct translation between the two.
+*)
+
 module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
     (* manager *)
@@ -18,7 +23,6 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
     type t = man Abstract1.t
 
     (* direct translation of numerical expressions into Apron tree expressions *)
-    (* TODO : some variables have type real and not int... *)
     let rec texpr_of_nexpr = function
         | NIdent id -> Texpr1.Var (Var.of_string id)
         | NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i))
diff --git a/abstract/domain.ml b/abstract/domain.ml
deleted file mode 100644
index 76635d1..0000000
--- a/abstract/domain.ml
+++ /dev/null
@@ -1,3 +0,0 @@
-open Ast
-open Formula
-
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index 77d7e3f..68b04f5 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -4,6 +4,18 @@ open Util
 
 exception Bot
 
+(*
+  Interface and implementation of an abstract domain meant to handle
+  constraints on enumerated variables.
+
+  Constraints are basically of two types :
+  - var OP value
+  - var OP var'
+  with OP either == or !=
+
+  (see formula.ml for a definition of the enum_cons type)
+*)
+
 module type ENUM_ENVIRONMENT_DOMAIN = sig
     type t
 
diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
index ae71b09..3e03d59 100644
--- a/abstract/enum_domain_edd.ml
+++ b/abstract/enum_domain_edd.ml
@@ -3,6 +3,10 @@ open Formula
 open Util
 open Enum_domain
 
+(*
+  Implementation of a more powerfull domain for enumerate constraints,
+  based on decision graphs (BDD).
+*)
 
 module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
     exception Top
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 650f8f4..4102891 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -4,6 +4,21 @@ open Ast_util
 
 (* AST for logical formulas *)
 
+(*
+  Two representations are used for the formulas :
+  - Formula tree, representing the boolean formula directly
+    as would be expected
+  - "conslist", where all the numerical and enumerate constraints
+    considered in a tree of ANDs are regrouped in a big list.
+  The second form is used when applying a formula to an abstract value,
+  whereas the first form is the one generated by the program transformation
+  procedure and is the one we prefer to show the user because it is more
+  easily understandable.
+*)
+
+(* ------------------------------------ *)
+(*         First representation         *)
+(* ------------------------------------ *)
 
 (* Numerical part *)
 
@@ -27,7 +42,6 @@ type num_cons = num_expr * num_cons_op  (* always imply right member = 0 *)
 
 (* Logical part *)
 
-
 (* Enumerated types *)
 type enum_expr =
   | EIdent of id
@@ -52,6 +66,11 @@ type bool_expr =
       (* (A and B) or ((not A) and C) *)
   | BNot of bool_expr
 
+(*
+  Helper functions to construct formula trees and automatically
+  simplifying some tautologies/contradictions
+*)
+
 let is_false = function
   | BConst false | BNot(BConst true) -> true
   | _ -> false
@@ -85,7 +104,10 @@ let f_e_op op a b = match a, b with
   | EIdent x, v | v, EIdent x -> BEnumCons(op, x, v)
 let f_e_eq = f_e_op E_EQ
 
-(* Write all formula without using the NOT operator *)
+(*
+  Transformation functions so that all the logical formula are written
+  without using the NOT operator
+*)
 
 let rec eliminate_not = function
   | BNot e -> eliminate_not_negate e
@@ -117,68 +139,19 @@ and eliminate_not_negate = function
     BOr(eliminate_not_negate a, eliminate_not_negate b)
   | BOr(a, b) ->
     BAnd(eliminate_not_negate a, eliminate_not_negate b)
+ 
 
 
+(* ------------------------------------ *)
+(*    Simplification functions on the   *)
+(*         first representation         *)
+(* ------------------------------------ *)
 
 (*
-  In big ANDs, try to separate levels of /\ and levels of \/
-  We also use this step to simplify trues and falses that may be present.
-*)
-
-type conslist = enum_cons list * num_cons list * conslist_bool_expr
-and conslist_bool_expr =
-  | CLTrue
-  | CLFalse
-  | CLAnd of conslist_bool_expr * conslist_bool_expr
-  | CLOr of conslist * conslist
-
-let rec conslist_of_f = function
-  | BNot e -> conslist_of_f (eliminate_not_negate e)
-  | BRel (op, a, b, is_real) ->
-    let x, y, op = match op with
-      | AST_EQ -> a, b, CONS_EQ
-      | AST_NE -> a, b, CONS_NE
-      | AST_GT -> a, b, CONS_GT
-      | AST_GE -> a, b, CONS_GE
-      | AST_LT -> b, a, CONS_GT
-      | AST_LE -> b, a, CONS_GE
-    in
-    let cons = if y = NIntConst 0 || y = NRealConst 0.
-      then (x, op)
-      else (NBinary(AST_MINUS, x, y, is_real), op)
-    in [], [cons], CLTrue
-  | BConst x ->
-    [], [], if x then CLTrue else CLFalse
-  | BEnumCons e ->
-    [e], [], CLTrue
-  | BOr(a, b) ->
-    let eca, ca, ra = conslist_of_f a in
-    let ecb, cb, rb = conslist_of_f b in
-    begin match eca, ca, ra, ecb, cb, rb with
-      | _, _, CLFalse, _, _, _ -> ecb, cb, rb
-      | _, _, _, _, _, CLFalse -> eca, ca, ra
-      | [], [], CLTrue, _, _, _ -> [], [], CLTrue
-      | _, _, _, [], [], CLTrue -> [], [], CLTrue
-      | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb))
-    end
-  | BAnd(a, b) ->
-    let eca, ca, ra = conslist_of_f a in
-    let ecb, cb, rb = conslist_of_f b in
-    let cons = ca @ cb in
-    let econs = eca @ ecb in
-    begin match ra, rb with
-      | CLFalse, _ | _, CLFalse -> [], [], CLFalse
-      | CLTrue, _ -> econs, cons, rb
-      | _, CLTrue -> econs, cons, ra
-      | _, _ -> econs, cons, CLAnd(ra, rb)
-    end
-  | BTernary(c, a, b) ->
-    conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b)))
-
-
-
-(*
-  Simplify formula considering something is true
+  Extract enumerated and numeric constants that
+  are always true in the formula (ie do not appear
+  under an OR or a ternary).
+  (not mathematically exact : only a subset is returned)
 *)
 
 let rec get_root_true = function
@@ -188,6 +161,13 @@ let rec get_root_true = function
   | BRel (a, b, c, d) -> [BRel (a, b, c, d)]
   | _ -> []
 
+(*
+  Simplify formula considering something is true
+  (only does some clearly visible simplifications ;
+  later simplifications are implicitly done when
+  abstract-interpreting the formula)
+*)
+
 let rec simplify true_eqs e =
   if List.exists
       (fun f ->
@@ -228,7 +208,6 @@ let rec simplify_k true_eqs e =
   List.fold_left f_and (simplify true_eqs e) true_eqs
   
 
-
 (*
   Simplify a formula replacing a variable with another
 *)
@@ -266,7 +245,7 @@ let rec formula_replace_evars repls e =
 
 
 (*
-  extract names of variables referenced in formula
+  Extract names of enumerated variables referenced in formula
 *)
 
 let rec refd_evars_of_f = function
@@ -276,3 +255,65 @@ let rec refd_evars_of_f = function
   | BEnumCons(_, e, EItem _) -> [e]
   | BEnumCons(_, e, EIdent f) -> [e; f]
   | _ -> []
+
+
+
+(* ------------------------------------ *)
+(*         Second representation        *)
+(* ------------------------------------ *)
+
+(*
+  In big ANDs, try to separate levels of /\ and levels of \/
+  We also use this step to simplify trues and falses that may be present.
+*)
+
+type conslist = enum_cons list * num_cons list * conslist_bool_expr
+and conslist_bool_expr =
+  | CLTrue
+  | CLFalse
+  | CLAnd of conslist_bool_expr * conslist_bool_expr
+  | CLOr of conslist * conslist
+
+let rec conslist_of_f = function
+  | BNot e -> conslist_of_f (eliminate_not_negate e)
+  | BRel (op, a, b, is_real) ->
+    let x, y, op = match op with
+      | AST_EQ -> a, b, CONS_EQ
+      | AST_NE -> a, b, CONS_NE
+      | AST_GT -> a, b, CONS_GT
+      | AST_GE -> a, b, CONS_GE
+      | AST_LT -> b, a, CONS_GT
+      | AST_LE -> b, a, CONS_GE
+    in
+    let cons = if y = NIntConst 0 || y = NRealConst 0.
+      then (x, op)
+      else (NBinary(AST_MINUS, x, y, is_real), op)
+    in [], [cons], CLTrue
+  | BConst x ->
+    [], [], if x then CLTrue else CLFalse
+  | BEnumCons e ->
+    [e], [], CLTrue
+  | BOr(a, b) ->
+    let eca, ca, ra = conslist_of_f a in
+    let ecb, cb, rb = conslist_of_f b in
+    begin match eca, ca, ra, ecb, cb, rb with
+      | _, _, CLFalse, _, _, _ -> ecb, cb, rb
+      | _, _, _, _, _, CLFalse -> eca, ca, ra
+      | [], [], CLTrue, _, _, _ -> [], [], CLTrue
+      | _, _, _, [], [], CLTrue -> [], [], CLTrue
+      | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb))
+    end
+  | BAnd(a, b) ->
+    let eca, ca, ra = conslist_of_f a in
+    let ecb, cb, rb = conslist_of_f b in
+    let cons = ca @ cb in
+    let econs = eca @ ecb in
+    begin match ra, rb with
+      | CLFalse, _ | _, CLFalse -> [], [], CLFalse
+      | CLTrue, _ -> econs, cons, rb
+      | _, CLTrue -> econs, cons, ra
+      | _, _ -> econs, cons, CLAnd(ra, rb)
+    end
+  | BTernary(c, a, b) ->
+    conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b)))
+
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index a5359a8..dd902ad 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -3,6 +3,8 @@ open Ast
 open Formula
 open Ast_printer
 
+(* Just a pretty-printer, nothing to see here *)
+
 let string_of_binary_rel = function
   | AST_EQ -> "="
   | AST_NE -> "≠"
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
index 084e397..22ea60b 100644
--- a/abstract/intervals_domain.ml
+++ b/abstract/intervals_domain.ml
@@ -1,5 +1,12 @@
 open Value_domain
 
+(*
+  Value domain for representing one interval, doing operations on
+  such representations, etc.
+
+  Restricted implementation, only support integers.
+*)
+
 module VD : VALUE_DOMAIN = struct
     type t = itv
 
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index efa30dd..ed029da 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -5,9 +5,11 @@ open Ast
 open Value_domain
 open Num_domain
 
-let debug = false
+(*
+  Implementation of a nonrelationnal domain for numerical values.
 
-(* Restricted domain, only support integers *)
+  Restricted implementation, only support integers.
+*)
 
 module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
     type env = V.t VarMap.t
@@ -160,11 +162,6 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
             | AST_LT -> let u, _ = V.leq v1 (V.sub v2 (V.const 1)) in u
             | AST_GT -> let _, v = V.leq (V.add v2 (V.const 1)) v1 in v
             in
-            if debug then Format.printf
-              "restrict %s %s @[<hv>%a@] : %s %s -> %s@." i 
-              (Formula_printer.string_of_binary_rel op)
-              Formula_printer.print_num_expr expr
-              (V.to_string v1) (V.to_string v2) (V.to_string v1');
             Env (VarMap.add i v1' env))
           env
         in
diff --git a/abstract/num_domain.ml b/abstract/num_domain.ml
index 285b3c4..a91c69f 100644
--- a/abstract/num_domain.ml
+++ b/abstract/num_domain.ml
@@ -1,6 +1,11 @@
 open Ast
 open Formula
 
+(*
+  Interface specification for a numerical environment domain
+  (relationnal with Apron or nonrelationnal with intervals)
+*)
+
 module type NUMERICAL_ENVIRONMENT_DOMAIN = sig
     type t
     type itv
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 20512aa..eedec3e 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -7,7 +7,8 @@ open Typing
 open Interpret  (* used for constant evaluation ! *)
 
 
-(* Transform SCADE program to logical formula.
+(*  Transform SCADE program to logical formula.
+    See formula.ml for a description of the formula's AST.
 
     Convention : to access the last value of a variable,
     access the variable with the same name prefixed by "L".
@@ -527,8 +528,6 @@ let f_of_prog_incl_init rp assume_guarantees =
         assume_guarantees in
     f_and clock_eq (f_and no_next_init_cond scope_f)
 
-      
-
 
 (*
     Get expressions for guarantee violation
@@ -583,30 +582,3 @@ and guarantees_of_prog rp =
 
 
 
-(*
-    Extract variables accessed by a LAST
-*)
-
-let rec extract_last_vars = function
-  | BRel(_, a, b, _) ->
-      elv_ne a @ elv_ne b
-  | BEnumCons c ->
-      elv_ec c
-  | BAnd(a, b) | BOr (a, b) ->
-    extract_last_vars a @ extract_last_vars b
-  | BNot(e) -> extract_last_vars e
-  | BTernary(c, a, b) -> extract_last_vars c @ 
-      extract_last_vars a @ extract_last_vars b
-  | _ -> []
-
-and elv_ne = function
-  | NIdent i when i.[0] = 'L' -> [i]
-  | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b
-  | NUnary (_, a, _) -> elv_ne a
-  | _ -> []
-
-and elv_ec (_, v, q) =
-  (if v.[0] = 'L' then [v] else []) @
-  (match q with
-    | EIdent i when i.[0] = 'L' -> [i]
-    | _ -> [])
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
index 0a421f7..48d87f9 100644
--- a/abstract/value_domain.ml
+++ b/abstract/value_domain.ml
@@ -1,4 +1,11 @@
 
+(*
+  Interface definition for any single-value abstract domain.
+  Only implementation of interface is intervals.
+*)
+
+
+
 type bound = Int of int | PInf | MInf
 type itv = Itv of bound * bound | Bot
 
diff --git a/abstract/varenv.ml b/abstract/varenv.ml
index 4d6caca..cf29edf 100644
--- a/abstract/varenv.ml
+++ b/abstract/varenv.ml
@@ -25,6 +25,37 @@ type varenv = {
 
 
 
+
+(*
+    Extract variables accessed by a LAST
+*)
+
+let rec extract_last_vars = function
+  | BRel(_, a, b, _) ->
+      elv_ne a @ elv_ne b
+  | BEnumCons c ->
+      elv_ec c
+  | BAnd(a, b) | BOr (a, b) ->
+    extract_last_vars a @ extract_last_vars b
+  | BNot(e) -> extract_last_vars e
+  | BTernary(c, a, b) -> extract_last_vars c @ 
+      extract_last_vars a @ extract_last_vars b
+  | _ -> []
+
+and elv_ne = function
+  | NIdent i when i.[0] = 'L' -> [i]
+  | NBinary(_, a, b, _) -> elv_ne a @ elv_ne b
+  | NUnary (_, a, _) -> elv_ne a
+  | _ -> []
+
+and elv_ec (_, v, q) =
+  (if v.[0] = 'L' then [v] else []) @
+  (match q with
+    | EIdent i when i.[0] = 'L' -> [i]
+    | _ -> [])
+
+
+
 (*
   extract_linked_evars : conslist -> (id * id) list
 
@@ -200,7 +231,7 @@ let force_ordering vars groups =
 let mk_varenv (rp : rooted_prog) f cl =
     (* add variables from LASTs *)
     let last_vars = uniq_sorted 
-      (List.sort compare (Transform.extract_last_vars f)) in
+      (List.sort compare (extract_last_vars f)) in
     let last_vars = List.map
       (fun id ->
         let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars
diff --git a/frontend/ast.ml b/frontend/ast.ml
index d55626d..773efa4 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -2,6 +2,15 @@ open Lexing
 open Util
 
 
+(*
+  Abstract Syntax Tree for a subset of the SCADE language.
+
+  This subset includes :
+  - basic dataflow core (excluding when, merge, and all other clock primitives)
+  - activate blocks
+  - automata with weak transitions only
+*)
+
 type 'a ext = 'a * extent
 
 type id = string
@@ -63,7 +72,7 @@ type expr =
 type var_def = bool * id * typ
 
 type automaton = id * state ext list * id list
-and  state = {
+and state = {
     initial   : bool;
     st_name   : id;
     st_locals : var_def list;
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 8908687..09f4986 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -3,23 +3,9 @@ open Lexing
 open Typing
 open Util
 
-
-(* Locations *)
-
-let string_of_position p =
-  Printf.sprintf "%s:%i:%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol)
-    
-let string_of_extent (p,q) =
-  if p.pos_fname = q.pos_fname then
-    if p.pos_lnum = q.pos_lnum then
-      if p.pos_cnum = q.pos_cnum then
-        Printf.sprintf "%s:%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol)
-      else
-        Printf.sprintf "%s:%i.%i-%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) (q.pos_cnum - q.pos_bol)
-    else
-      Printf.sprintf "%s:%i.%i-%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) q.pos_lnum (q.pos_cnum - q.pos_bol)
-  else
-    Printf.sprintf "%s:%i.%i-%s:%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) q.pos_fname q.pos_lnum (q.pos_cnum - q.pos_bol)
+(*
+  Just a pretty-printer, nothing to see here.
+*)
 
 
 (* Operators *)
diff --git a/frontend/file_parser.ml b/frontend/file_parser.ml
deleted file mode 100644
index 85eb9cd..0000000
--- a/frontend/file_parser.ml
+++ /dev/null
@@ -1,17 +0,0 @@
-open Ast
-open Ast_printer
-open Lexing
-
-let parse_file (filename : string) : prog =
-  let f = open_in filename in
-  let lex = from_channel f in
-  try
-    lex.lex_curr_p <- { lex.lex_curr_p with pos_fname = filename; };
-    Parser.file Lexer.token lex
-  with
-  | Parser.Error ->
-    Util.error (Printf.sprintf "Parse error (invalid syntax) near %s"
-                  (string_of_position lex.lex_start_p))
-  | Failure "lexing: empty token" ->
-    Util.error (Printf.sprintf "Parse error (invalid token) near %s"
-                  (string_of_position lex.lex_start_p))
diff --git a/frontend/rename.ml b/frontend/rename.ml
index 9c4cc31..71ec321 100644
--- a/frontend/rename.ml
+++ b/frontend/rename.ml
@@ -1,4 +1,12 @@
-(* Scope analyzer *)
+(*
+  Scope analyzer
+
+  Does a tiny bit of renaming, so that in a given node, every
+  variable declaration is unique.
+
+  Variable name unicity is not assured program-wide. Node paths are
+  handled only once the program has been "rooted" (see fronted/typing.ml)
+*)
 
 open Ast
 open Util
diff --git a/interpret/bad_interpret.ml b/interpret/bad_interpret.ml
deleted file mode 100644
index 08ccf85..0000000
--- a/interpret/bad_interpret.ml
+++ /dev/null
@@ -1,308 +0,0 @@
-open Ast
-open Data
-open Util
-open Ast_util
-
-(* Data structures for the interpret *)
-
-type scope = string
-
-type svalue =
-  | VInt of int
-  | VBool of bool
-  | VReal of float
-  | VState of id
-  | VPrevious of value
-  | VBusy   (* intermediate value : calculating ! for detection of cycles *)
-and value = svalue list
-
-type state = svalue VarMap.t
-
-(* functions for recursively getting variables *)
-
-type calc_fun = 
-  | F of (state -> calc_map -> state)
-and calc_map = calc_fun VarMap.t
-
-let get_var (st: state) (c: calc_map) (id: id) : (state * svalue) =
-  let st =
-    if VarMap.mem id st then st
-    else match VarMap.find id c with
-    | F f ->
-      (* Format.printf "%s[ " id; *)
-      let r = f (VarMap.add id VBusy st) c in
-      (* Format.printf "]%s " id; *)
-      r
-  in
-    match VarMap.find id st with
-    | VBusy -> combinatorial_cycle id
-    | v -> st, v
-
-(* pretty-printing *)
-
-let rec str_of_value = function
-  | VInt i -> string_of_int i
-  | VReal r -> string_of_float r
-  | VBool b -> if b then "true" else "false"
-  | VState s -> "state " ^ s
-  | VPrevious p ->
-    "[" ^
-      List.fold_left (fun s v -> (if s = "" then "" else s ^ ", ") ^ str_of_value v) "" p
-      ^ "]"
-  | VBusy -> "#"
-let print_state st =
-  VarMap.iter (fun id v -> Format.printf "%s = %s@." id (str_of_value v)) st
-
-
-
-
-(* Expression evaluation *)
-
-type eval_env = {
-  p: prog;
-  c: calc_map;
-  scopes: string list;
-}
-
-(*
-  eval_expr : eval_env -> string -> expr ext -> (state * value)
-*)
-let rec eval_expr env st exp =
-  let sub_eval = eval_expr env in
-  let scope = List.hd env.scopes in
-  match fst exp with
-  | AST_identifier (id, _) ->
-    let rec aux = function
-      | [] ->
-        no_variable id
-      | sc::q ->
-        try let st, v = get_var st env.c (sc^"/"^id) in st, [v]
-        with Not_found -> aux q
-    in loc_error (snd exp) aux env.scopes
-  | AST_idconst (id, _) ->
-    let st, v = get_var st env.c ("cst/"^id) in st, [v]
-  (* on numerical values *)
-  | AST_int_const (i, _) -> st, [VInt (int_of_string i)]
-  | AST_real_const (r, _) -> st, [VReal (float_of_string r)]
-  | AST_unary(AST_UPLUS, e) -> sub_eval st e
-  | AST_unary(AST_UMINUS, e) ->
-    begin match sub_eval st e with
-    | st, [VInt x] -> st, [VInt (-x)]
-    | st, [VReal x] -> st, [VReal(-. x)]
-    | _ -> type_error "Unary on non-numerical."
-    end
-  | AST_binary(op, e1, e2) ->
-    let st, v1 = sub_eval st e1 in
-    let st, v2 = sub_eval st e2 in
-    let iop, fop = match op with
-    | AST_PLUS -> (+), (+.)
-    | AST_MINUS -> (-), (-.)
-    | AST_MUL -> ( * ), ( *. )
-    | AST_DIV -> (/), (/.)
-    | AST_MOD -> (mod), mod_float
-    in
-    begin match v1, v2 with
-    | [VInt a], [VInt b] -> st, [VInt (iop a b)]
-    | [VReal a], [VReal b] -> st, [VReal(fop a b)]
-    | _ -> type_error "Invalid arguments for numerical binary."
-    end
-  (* on boolean values *)
-  | AST_bool_const b -> st, [VBool b]
-  | AST_binary_rel(op, e1, e2) ->
-    let st, v1 = sub_eval st e1 in
-    let st, v2 = sub_eval st e2 in
-    let r = match op with
-    | AST_EQ -> (=)     | AST_NE -> (<>)
-    | AST_LT -> (<)     | AST_LE -> (<=)
-    | AST_GT -> (>)     | AST_GE -> (>=)
-    in
-    begin match v1, v2 with
-    | [VInt a], [VInt b] -> st, [VBool (r a b)]
-    | [VReal a], [VReal b] -> st, [VBool (r a b)]
-    | [VBool a], [VBool b] -> st, [VBool (r a b)]
-    | _ -> type_error "Invalid arguments for binary relation."
-    end
-  | AST_binary_bool(op, e1, e2) ->
-    let st, v1 = sub_eval st e1 in
-    let st, v2 = sub_eval st e2 in
-    let r = match op with
-    | AST_AND -> (&&)   | AST_OR -> (||)
-    in
-    begin match v1, v2 with
-    | [VBool a], [VBool b] -> st, [VBool (r a b)]
-    | _ -> type_error "Invalid arguments for boolean relation."
-    end
-  | AST_not(e) ->
-    begin match sub_eval st e with
-    | st, [VBool b] -> st, [VBool (not b)]
-    | _ -> type_error "Invalid arguments for boolean negation."
-    end
-  (* temporal primitives *)
-  | AST_pre(exp, n) ->
-    begin try match VarMap.find (scope^"/"^n) st with
-      | VPrevious x -> st, x
-      | _ -> st, []
-    with Not_found -> st, []
-    end
-  | AST_arrow(before, after) -> 
-    begin try match VarMap.find (scope^"/init") st with
-    | VBool true -> sub_eval st before
-    | VBool false -> sub_eval st after
-    | _ -> assert false
-    with Not_found -> error ("Internal: could not find init for scope " ^ scope)
-    end
-  (* other *)
-  | AST_if(cond, a, b) ->
-    let st, cv = sub_eval st cond in
-    begin match cv with
-    | [VBool true] -> sub_eval st a
-    | [VBool false] -> sub_eval st b
-    | _ -> type_error "Invalid condition in if."
-    end
-  | AST_instance((f, _), args, nid) ->
-    let (n, _) = find_node_decl env.p f in
-    List.fold_left
-      (fun (st, vs) (_, (id,_), _) ->
-          let st, v = get_var st env.c (scope^"/"^nid^"/"^id) in
-          st, vs @ [v])
-      (st, []) n.ret
-
-(* Constant calculation *)
-
-let rec calc_const p d st c =
-  let env = { p = p; c = c; scopes = ["cst"] } in
-  match eval_expr env st d.value with
-  | st, [v] -> VarMap.add ("cst/"^d.c_name) v st
-  | _ -> type_error ("Cannot assign tuple to constant" ^ d.c_name)
-
-let program_consts p =
-  let cdecl = extract_const_decls p in
-  let ccmap = List.fold_left
-    (fun c (d, _) -> VarMap.add ("cst/"^d.c_name) (F (calc_const p d)) c)
-    VarMap.empty cdecl
-  in
-  List.fold_left
-    (fun st (d, _) -> let st, _ = get_var st ccmap ("cst/"^d.c_name) in st)
-    VarMap.empty
-    cdecl
-
-(* get initial state for program *)
-let program_init_state p root_node =
-  let (n, _) = find_node_decl p root_node in
-  let rec aux st p scope eqs =
-    let st = VarMap.add (scope^"/init") (VBool true) st in
-    let add_subscopes =
-      List.fold_left (fun st (ss_id, ss_eqs, _) -> aux st p (scope^"/"^ss_id) ss_eqs)
-    in
-    let add_eq st eq = match fst eq with
-        | AST_assign(_, e) -> add_subscopes st (extract_instances p e)
-        | AST_assume _ | AST_guarantee _ -> st
-        | AST_automaton (aid, astates, ret) ->
-          let (initial, _) = List.find (fun (s, _) -> s.initial) astates in
-          let st = VarMap.add (scope^":"^aid^".state") (VState initial.name) st in
-          let add_astate st ((astate:Ast.state), _) =
-            aux st p (scope^":"^aid^"."^astate.name) astate.body
-          in
-          List.fold_left add_astate st astates
-        | AST_activate _ -> not_implemented "program_init_state activate"
-    in
-    List.fold_left add_eq st eqs
-  in
-    aux (program_consts p) p "" n.body
-
-
-(* Program execution *)
-
-(* build calc map *)
-let rec build_prog_ccmap p scopes eqs st =
-  let scope = List.hd scopes in
-  let add_eq c eq = match fst eq with
-    | AST_assign(vars, e) ->
-      let calc st c =
-        let env = { p = p; c = c; scopes = scopes } in
-        let st, vals = eval_expr env st e in
-        List.fold_left2
-          (fun st (id,_) v -> VarMap.add (scope^"/"^id) v st)
-          st vars vals
-      in
-      let c = List.fold_left (fun c (id, _) -> VarMap.add (scope^"/"^id) (F calc) c) c vars in
-
-      let add_subscope c (ss_id, ss_eqs, ss_args) =
-        let c = VarMap.merge disjoint_union c
-          (build_prog_ccmap p [scope^"/"^ss_id] ss_eqs st)
-        in
-        let add_v c ((_, (id, _), _), eq) =
-          let calc st c =
-            let env = { p = p; c = c; scopes = scopes } in
-            let st, vals = eval_expr env st eq in
-            match vals with
-            | [v] -> VarMap.add (scope^"/"^ss_id^"/"^id) v st
-            | _ -> type_error "invalid arity"
-          in
-          VarMap.add (scope^"/"^ss_id^"/"^id) (F calc) c
-        in
-        List.fold_left add_v c ss_args
-      in
-      List.fold_left add_subscope c (extract_instances p e)
-    | AST_assume _ | AST_guarantee _ -> c
-    | AST_automaton _ -> not_implemented "build_prog_ccmap for automaton"
-    | AST_activate _ -> not_implemented "build_prog_ccmap for activate"
-  in
-  List.fold_left add_eq VarMap.empty eqs
-
-let extract_next_state active env eqs st =
-  let csts = VarMap.filter
-    (fun k _ -> String.length k > 4 && String.sub k 0 4 = "cst/")
-    st
-  in
-  let rec aux active scopes eqs st nst =
-    let scope = List.hd env.scopes in
-
-    let r = VarMap.add (scope^"/init")
-        (if active then VBool false
-          else try VarMap.find (scope^"/init") st with Not_found -> assert false)
-        nst
-    in
-    let add_subscopes active =
-      List.fold_left (fun (st, nst) (ss_id, ss_eqs, _) ->
-        aux active [scope^"/"^ss_id] ss_eqs st nst)
-    in
-    let add_eq (st, nst) eq = match fst eq with
-      | AST_assign(vars, e) ->
-        let st, nst = add_subscopes active (st, nst) (extract_instances env.p e) in
-        List.fold_left (fun (st, nst) (pn, pe) ->
-            let st, v = if active then eval_expr { env with scopes = scopes } st pe
-              else st,
-                try match VarMap.find (scope^"/"^pn) st with VPrevious x -> x | _ -> []
-                with Not_found -> []
-            in
-            st, VarMap.add (scope^"/"^pn) (VPrevious v) nst)
-          (st, nst) (extract_pre e)
-      | AST_assume _ | AST_guarantee _ -> st, nst
-      | AST_automaton _ -> not_implemented "extract_next_state automaton"
-      | AST_activate _ -> not_implemented "extract_next_state activate"
-    in
-    List.fold_left add_eq (st, r) eqs
-  in aux active env.scopes eqs st csts
-
-
-
-let program_step p st inputs root_node =
-  let (n, _) = find_node_decl p root_node in
-  let st = List.fold_left
-    (fun st (n, v) -> VarMap.add ("/"^n) v st) st inputs in
-
-  let ccmap = build_prog_ccmap p [""] n.body st in
-
-  let st = List.fold_left
-    (fun st (_, (id, _), _) -> let st, _ = get_var st ccmap ("/"^id) in st)
-    st n.ret in
-  let outputs = List.map
-    (fun (_, (id, _), _) -> let _, v = get_var st ccmap ("/"^id) in (id, v))
-    n.ret in
-
-  let st, next_st = extract_next_state true { p = p; scopes = [""]; c = ccmap } n.body st in
-
-  st, outputs, next_st
-  
-
diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index 8bdf650..f14d6e2 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -1,3 +1,10 @@
+(*
+  Interpret for a portion of the concrete semantics of the Scade language.
+  (basically, interpretation is handled for all the subset of the language
+  that we can parse).
+*)
+
+
 open Ast
 open Util
 open Ast_util
diff --git a/libs/util.ml b/libs/util.ml
index 6e8dc59..ffeee82 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -1,4 +1,5 @@
 open Unix
+open Lexing
 
 (* Small things *)
 
@@ -33,6 +34,21 @@ let position_unknown = Lexing.dummy_pos
 type extent = position * position
 let extent_unknown = (position_unknown, position_unknown)
 
+let string_of_position p =
+  Printf.sprintf "%s:%i:%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol)
+    
+let string_of_extent (p,q) =
+  if p.pos_fname = q.pos_fname then
+    if p.pos_lnum = q.pos_lnum then
+      if p.pos_cnum = q.pos_cnum then
+        Printf.sprintf "%s:%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol)
+      else
+        Printf.sprintf "%s:%i.%i-%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) (q.pos_cnum - q.pos_bol)
+    else
+      Printf.sprintf "%s:%i.%i-%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) q.pos_lnum (q.pos_cnum - q.pos_bol)
+  else
+    Printf.sprintf "%s:%i.%i-%s:%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) q.pos_fname q.pos_lnum (q.pos_cnum - q.pos_bol)
+
 
 (* Exceptions *)
 
diff --git a/main.ml b/main.ml
index f85f6fb..55a3837 100644
--- a/main.ml
+++ b/main.ml
@@ -1,3 +1,5 @@
+open Lexing
+
 open Cmdline
 
 open Ast
@@ -108,6 +110,20 @@ let options = [
         "Scopes for which to introduce a 'init' variable in analysis.";
 ]
 
+let parse_file (filename : string) : prog =
+  let f = open_in filename in
+  let lex = from_channel f in
+  try
+    lex.lex_curr_p <- { lex.lex_curr_p with pos_fname = filename; };
+    Parser.file Lexer.token lex
+  with
+  | Parser.Error ->
+    Util.error (Printf.sprintf "Parse error (invalid syntax) near %s"
+                  (Util.string_of_position lex.lex_start_p))
+  | Failure "lexing: empty token" ->
+    Util.error (Printf.sprintf "Parse error (invalid token) near %s"
+                  (Util.string_of_position lex.lex_start_p))
+
 let do_test_interpret prog verbose =
     let f0 _ = false in
     let s0 = Interpret.init_state (Typing.root_prog prog "test" f0 f0) in
@@ -150,7 +166,7 @@ let () =
     end;
 
     try
-      let prog = File_parser.parse_file !ifile in
+      let prog = parse_file !ifile in
       if !dump then Ast_printer.print_prog Format.std_formatter prog;
 
       let prog = Rename.rename_prog prog in
@@ -211,6 +227,6 @@ let () =
     | Util.LocError(l, e) ->
         Format.eprintf "Error: %s@." e;
         List.iter
-          (fun loc -> Format.eprintf "At: %s@." (Ast_printer.string_of_extent loc))
+          (fun loc -> Format.eprintf "At: %s@." (Util.string_of_extent loc))
           l