Some abstract interpretation does something now.

11 files changed, 205 insertions, 30 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 403e3e8..1838591 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -1,4 +1,5 @@
 open Ast
+open Ast_util
 open Formula
 
 open Util
@@ -6,9 +7,133 @@ open Environment_domain
 
 module I (E : ENVIRONMENT_DOMAIN) : sig
 
-  val init_state  : prog -> id -> E.t
-  val do_step     : prog -> id -> E.t -> E.t
+    type st
+
+    val do_prog     : prog -> id -> unit
 
 end = struct
 
+    type st = {
+        p           : prog;
+        root_scope  : scope;
+        all_vars    : var_def list;
+        env         : E.t;
+        f           : bool_expr;
+        cl          : conslist;
+    }
+
+
+    let node_vars p f nid =
+      let (n, _) = find_node_decl p f in
+      List.map (fun (p, id, t) -> p, nid^"/"^id, t)
+        (n.args @ n.ret @ n.var)
+
+    (*
+        extract_all_vars : prog -> scope -> var_decl list
+
+        Extracts all variables with names given according to
+        naming convention used here and in transform.ml :
+        - pre variables are not prefixed by scope
+        - next values for variables are prefixed by capital N
+    *)
+    let rec extract_all_vars p (node, prefix, eqs) =
+        let vars_of_expr e =
+          List.flatten
+            (List.map
+              (fun (f, id, eqs, args) ->
+                node_vars p f (node^"/"^id) @
+                extract_all_vars p (node^"/"^id, "", eqs))
+              (extract_instances p e))
+          @
+          List.flatten
+            (List.map
+              (fun (id, _) -> [false, id, AST_TINT; false, "N"^id, AST_TINT])
+                  (* TODO : type of pre value ? *)
+              (extract_pre e))
+        in
+        let vars_of_eq e = match fst e with
+          | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> vars_of_expr e
+          | AST_activate (b, _) ->
+            let rec do_branch = function
+              | AST_activate_body b ->
+                List.map (fun (p, id, t) -> p, node^"/"^b.act_id^"."^id, t) b.act_locals
+                @
+                extract_all_vars p (node, b.act_id^".", b.body)
+              | AST_activate_if(c, a, b) ->
+                vars_of_expr c @ do_branch a @ do_branch b
+            in do_branch b
+          | AST_automaton _ -> not_implemented "extract_all vars automaton"
+        in
+        (false, node^"/"^prefix^"time", AST_TINT)::
+        (false, "N"^node^"/"^prefix^"time", AST_TINT)::
+        (List.flatten (List.map vars_of_eq eqs))
+
+    (* init state *)
+    let init_state p root =
+      let root_scope = get_root_scope p root in
+
+      let f = Formula.eliminate_not (Transform.f_of_prog p root) in
+      let cl = Formula.conslist_of_f f in
+      let all_vars = node_vars p root "" @ extract_all_vars p root_scope in
+      let env = List.fold_left
+        (fun env (_, id, ty) ->
+          E.addvar env id (ty = AST_TREAL))
+        E.init
+        all_vars
+      in
+
+    
+
+      let init_f = Transform.init_f_of_prog p root in
+      let env = E.apply_f env init_f in
+
+      Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
+      Format.printf "Cycle formula: %a@.@." Formula_printer.print_conslist cl;
+
+      { p; root_scope; f; cl; all_vars; env }
+
+    (*
+      pass_cycle : var_def list -> E.t -> E.t
+
+      Does :
+        - x <- Nx, for all x
+        - ignore x for all x such that Nx does not exist
+    *)
+    let pass_cycle vars e =
+      let tr_assigns = List.fold_left
+        (fun q (_, id, _) ->
+            if id.[0] = 'N' then
+              (String.sub id 1 (String.length id - 1), NIdent id)::q
+            else
+              q)
+        [] vars
+      in
+      let e = E.assign e tr_assigns in
+
+      let forget_vars = List.map (fun (_, id, _) -> id)
+          (List.filter
+              (fun (_, id, _) ->
+                 not (List.exists (fun (_, id2, _) -> id2 = "N"^id) vars))
+              vars) in
+      let e = List.fold_left E.forgetvar e forget_vars in
+      Format.printf "Pass cycle: %a@.@." E.print_all e;
+      e
+
+
+    (*
+      do_prog : prog -> id -> st
+    *)
+    let do_prog p root =
+      let st = init_state p root in
+
+      let rec step acc i n =
+        Format.printf "Step %d: %a@." n E.print_all acc;
+        if n < 10 then begin
+          let i' = E.apply_cl (E.join i acc) st.cl in
+          let j = pass_cycle st.all_vars i' in
+          let acc' = (if n > 6 then E.widen else E.join) acc j in
+          step acc' i (n+1)
+        end
+      in
+      step (E.vbottom st.env) st.env 0
 end
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index 1cc418e..ad483ec 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -68,6 +68,9 @@ module D : ENVIRONMENT_DOMAIN = struct
             Environment.add env [| Var.of_string id |] [||]
         in
         Abstract1.change_environment manager x env2 false
+    let forgetvar x id =
+        let v = [| Var.of_string id |] in
+        Abstract1.forget_array manager x v false
     let rmvar x id =
         let v = [| Var.of_string id |] in
         let env = Abstract1.env x in
@@ -105,6 +108,14 @@ module D : ENVIRONMENT_DOMAIN = struct
           Abstract1.join manager y z
 
     let apply_f x f = apply_cl x (conslist_of_f f)
+    
+    let assign x eqs =
+      let env = Abstract1.env x in
+      let vars = Array.of_list
+        (List.map (fun (id, _) -> Var.of_string id) eqs) in
+      let vals = Array.of_list
+        (List.map (fun (_, v) -> Texpr1.of_expr env (texpr_of_nexpr v)) eqs) in
+      Abstract1.assign_texpr_array manager x vars vals None
 
     
     (* Ensemblistic operations *)
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index 5664474..5dbd08f 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -11,6 +11,7 @@ module type ENVIRONMENT_DOMAIN = sig
 
     (* variable management *)
     val addvar      : t -> id -> bool -> t     (* integer or float variable ? *)
+    val forgetvar   : t -> id -> t             (* remove var from constraints *)
     val rmvar       : t -> id -> t
     val vars        : t -> (id * bool) list
     val vbottom     : t -> t       (* bottom value with same environment *)
@@ -18,6 +19,7 @@ module type ENVIRONMENT_DOMAIN = sig
     (* abstract operation *)
     val apply_f     : t -> bool_expr -> t
     val apply_cl    : t -> conslist -> t
+    val assign      : t -> (id * num_expr) list -> t
 
     (* set-theoretic operations *)
     val join        : t -> t -> t       (* union *)
diff --git a/abstract/transform.ml b/abstract/transform.ml
index e6886b8..40390dd 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -67,7 +67,7 @@ let rec f_of_nexpr td (node, prefix) where expr =
       BAnd(BNot(f_of_bexpr td (node, prefix) c), sub where b))
   | AST_instance ((f, _), args, nid) ->
     let (n, _) = find_node_decl td.p f in
-    where (List.map (fun (_, (id, _), _) -> NIdent (node^"/"^nid^"/"^id)) n.ret)
+    where (List.map (fun (_, id, _) -> NIdent (node^"/"^nid^"/"^id)) n.ret)
     
   (* boolean values treated as integers *)
   | _ ->
@@ -101,10 +101,10 @@ and f_of_bexpr td (node, prefix) expr =
 
 and f_of_scope active td (node, prefix, eqs) =
   let expr_eq e eq =
-    let instance_eq (id, eqs, args) =
+    let instance_eq (_, id, eqs, args) =
       let eq = f_of_scope active td (node^"/"^id, "", eqs) in
       if active then
-        List.fold_left (fun eq ((_,(argname,_),_), expr) ->
+        List.fold_left (fun eq ((_,argname,_), expr) ->
             let eq_arg = f_of_nexpr td (node, prefix) (function
                   | [v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v)
                   | _ -> invalid_arity "in argument")
@@ -146,11 +146,15 @@ and f_of_scope active td (node, prefix, eqs) =
       in
         expr_eq e assign_eq
     | AST_assume (_, e) ->
-      if active then
-        f_of_bexpr td (node, prefix) e
-      else
-        BConst true
-    | AST_guarantee _ -> BConst true
+      let assume_eq = 
+        if active then
+          f_of_bexpr td (node, prefix) e
+        else
+          BConst true
+      in
+        expr_eq e assume_eq
+    | AST_guarantee (_, e) ->
+      expr_eq e (BConst true)
     | AST_activate (b, _) ->
       let rec cond_eq = function
         | AST_activate_body b -> BConst true
@@ -199,3 +203,40 @@ and f_of_prog p root =
 
     f_of_scope true td td.root_scope
   
+
+
+
+
+
+
+let rec init_f_of_scope p (node, prefix, eqs) =
+  let expr_eq e =
+    let instance_eq (_, id, eqs, args) =
+     init_f_of_scope p (node^"/"^id, "", eqs)
+    in
+    List.fold_left (fun x i -> f_and (instance_eq i) x)
+      (BConst true) (extract_instances p e)
+  in
+  let do_eq eq = match fst eq with
+    | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
+        expr_eq e
+    | AST_activate (b, _) ->
+      let rec cond_eq = function
+        | AST_activate_body b ->
+          init_f_of_scope p (node, b.act_id^"_", b.body)
+        | AST_activate_if(c, a, b) ->
+          f_and (expr_eq c)
+            (f_and (cond_eq a) (cond_eq b))
+      in
+      cond_eq b
+    | AST_automaton _ -> not_implemented "f_of_scope do_eq automaton"
+  in
+  let time_eq =
+    BRel(AST_EQ,
+        NIdent(node^"/"^prefix^"time"),
+        NIntConst 0)
+  in
+  List.fold_left f_and time_eq (List.map do_eq eqs)
+
+and init_f_of_prog p root =
+    init_f_of_scope p (get_root_scope p root)
diff --git a/frontend/ast.ml b/frontend/ast.ml
index fbf099c..4f8c860 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -58,7 +58,7 @@ type expr =
     | AST_if          of (expr ext) * (expr ext) * (expr ext)
     | AST_instance    of (id ext) * (expr ext list) * id
 
-type var_def = bool * (id ext) * typ
+type var_def = bool * id * typ
 
 type automaton = id * state ext list * id list
 and  state = {
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 641e4fd..c14d0d1 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -171,7 +171,7 @@ let rec print_vars ind fmt = function
     List.iter (fun d -> Format.fprintf fmt " %a;" print_var_decl d) v;
     Format.fprintf fmt "@\n";
 
-and print_var_decl fmt (pr, (i, _), ty) =
+and print_var_decl fmt (pr, i, ty) =
     Format.fprintf fmt "%s%s: %s"
       (if pr then "probe " else "")
       i
diff --git a/frontend/parser.mly b/frontend/parser.mly
index 0d257dd..4301a05 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -166,7 +166,7 @@ body:
   { l }
 
 var:
-|   p=boption(PROBE) i=ext(IDENT)   { (p, i) }
+|   p=boption(PROBE) i=IDENT                    { (p, i) }
 
 vari:
 |   vn=separated_list(COMMA, var) COLON t=typ
diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml
index f5a1978..9cfe995 100644
--- a/interpret/ast_util.ml
+++ b/interpret/ast_util.ml
@@ -41,7 +41,7 @@ let get_root_scope p root =
 (* Utility : find instances declared in an expression *)
 
 (* extract_instances :
-      prog -> expr ext -> (id * eqs * (var_def * expr ext) list) list
+      prog -> expr ext -> (id * id * eqs * (var_def * expr ext) list) list
 *)
 let rec extract_instances p e = match fst e with
   | AST_idconst _ | AST_identifier _
@@ -56,7 +56,7 @@ let rec extract_instances p e = match fst e with
     let more = List.flatten (List.map (extract_instances p) args) in
     let (node, _) = find_node_decl p f in
     let args_x = List.map2 (fun id arg -> id, arg) node.args args in
-    (id, node.body, args_x)::more
+    (f, id, node.body, args_x)::more
 
 (* Utility : find pre declarations in an expression *)
 
diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index f28bce0..6f7c90e 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -211,7 +211,7 @@ end = struct
     | AST_instance((f, _), args, nid) ->
       let (n, _) = find_node_decl env.st.p f in
       List.map
-        (fun (_, (id, _), _) -> get_var env (node^"/"^nid) id)
+        (fun (_, id, _) -> get_var env (node^"/"^nid) id)
         n.ret
 
   (*
@@ -226,7 +226,7 @@ end = struct
     Hashtbl.replace env.vars (node^"/"^prefix^"init") (VBool true);
     let do_exp e =
       List.iter
-        (fun (id, eqs, _) -> reset_scope env (node^"/"^id, "", eqs))
+        (fun (_, id, eqs, _) -> reset_scope env (node^"/"^id, "", eqs))
         (extract_instances env.st.p e)
     in
     let do_eq (e, _) = match e with
@@ -259,9 +259,9 @@ end = struct
     Hashtbl.replace env.vars (node^"/"^prefix^"act") (VBool true);
     let do_expr e =
       List.iter
-        (fun (id, eqs, args) ->
+        (fun (_, id, eqs, args) ->
           activate_scope env (node^"/"^id, "", eqs);
-          let do_arg ((_,(name,_),_), expr) =
+          let do_arg ((_,name,_), expr) =
             let apath = node^"/"^id^"/"^name in
             let calc () =
               match eval_expr env (node, prefix) expr with
@@ -329,7 +329,7 @@ end = struct
   let rec do_weak_transitions env (node, prefix, eqs) =
     let do_expr e =
       List.iter
-        (fun (id, eqs, args) ->
+        (fun (_, id, eqs, args) ->
           do_weak_transitions env (node^"/"^id, "", eqs))
         (extract_instances env.st.p e)
     in
@@ -404,7 +404,7 @@ end = struct
           save (extract_pre e) in
         (* Save recursively in sub instances of nodes *)
         let save = List.fold_left
-          (fun save (n, eqs, _) ->
+          (fun save (_, n, eqs, _) ->
             aux (node^"/"^n, "", eqs) save)
           save (extract_instances env.st.p e)
         in save
@@ -447,7 +447,7 @@ end = struct
         p = p;
         root_scope = get_root_scope p root;
         save = VarMap.empty;
-        outputs = (List.map (fun (_,(n,_),_) -> n) n.ret);
+        outputs = (List.map (fun (_,n,_) -> n) n.ret);
     } in
 
     let env = { st = st; vars = Hashtbl.create 42 } in
diff --git a/interpret/rename.ml b/interpret/rename.ml
index 46c6f04..654b101 100644
--- a/interpret/rename.ml
+++ b/interpret/rename.ml
@@ -17,7 +17,7 @@ let consts_renaming p =
 (* add_var_defs : string -> renaming -> var_def list -> renaming *)
 let add_var_defs prefix =
   List.fold_left
-    (fun rn (_,(n,_),_) -> VarMap.add n (prefix^n, false) rn)
+    (fun rn (_,n,_) -> VarMap.add n (prefix^n, false) rn)
 
 (* rename_expr : expr ext -> renaming -> expr ext *)
 let rec rename_expr exp rn =
@@ -50,7 +50,7 @@ let rename_var rn id =
 
 let rename_var_ext rn (id, loc) = (rename_var rn id, loc)
 
-let rename_var_def rn (p, id, t) = (p, rename_var_ext rn id, t)
+let rename_var_def rn (p, id, t) = (p, rename_var rn id, t)
 
 (* rename_eqn : renaming -> eqn ext -> eqn ext *)
 let rec rename_eqn rn e =
diff --git a/main.ml b/main.ml
index ccc0e0d..be98cf7 100644
--- a/main.ml
+++ b/main.ml
@@ -2,7 +2,7 @@ open Ast
 
 module Interpret = Interpret.I
 
-module Abstract = Apron_domain.D
+module AI = Abs_interp.I(Apron_domain.D)
 
 (* command line options *)
 let dump = ref false
@@ -65,11 +65,7 @@ let () =
       let prog = Rename.rename_prog prog in
       if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
 
-      let prog_f = Formula.eliminate_not (Transform.f_of_prog prog "test") in
-      Formula_printer.print_expr Format.std_formatter prog_f;
-      Format.printf "@.";
-      let prog_f_cl = Formula.conslist_of_f prog_f in
-      Formula_printer.print_conslist Format.std_formatter prog_f_cl;
+      let () = AI.do_prog prog "test" in
 
       if !vtest then do_test_interpret prog true
       else if !test then do_test_interpret prog false;