Some abstract interpretation does something now.

4 files changed, 189 insertions, 10 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)