Do some typing ; support multiple pre in abstract interpretation.

2 files changed, 51 insertions, 92 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 00f7fad..c621734 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -1,6 +1,7 @@
 open Ast
 open Ast_util
 open Formula
+open Typing
 
 open Util
 open Environment_domain
@@ -9,15 +10,13 @@ module I (E : ENVIRONMENT_DOMAIN) : sig
 
     type st
 
-    val do_prog     : int -> prog -> id -> unit
+    val do_prog     : int -> rooted_prog -> unit
 
 end = struct
 
     type st = {
-        p           : prog;
+        rp          : rooted_prog;
         widen_delay : int;
-        root_scope  : scope;
-        all_vars    : var_def list;
         env         : E.t;
         f           : bool_expr;
         cl          : conslist;
@@ -27,75 +26,29 @@ end = struct
     }
 
 
-    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^"/"^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 widen_delay p root =
-      let root_scope = get_root_scope p root in
-
-      let f = Formula.eliminate_not (Transform.f_of_prog p root false) in
+    let init_state widen_delay rp =
+      let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
       let cl = Formula.conslist_of_f f in
-      let f_g = Formula.eliminate_not (Transform.f_of_prog p root true) in
+      let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
       let cl_g = Formula.conslist_of_f f_g 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.addvar env id (ty = TReal))
         E.init
-        all_vars
+        rp.all_vars
       in
-      let init_f = Transform.init_f_of_prog p root in
-      let guarantees = Transform.guarantees_of_prog p root in
+      let init_f = Transform.init_f_of_prog rp in
+      let guarantees = Transform.guarantees_of_prog rp in
 
       Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
       Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
       Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g;
 
-      Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
+      Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_typed_var ", ") rp.all_vars;
 
       Format.printf "Guarantees:@.";
       List.iter (fun (id, f) ->
@@ -105,9 +58,9 @@ end = struct
 
       let env = E.apply_f env init_f in
 
-      { p; root_scope; widen_delay;
+      { rp; widen_delay;
         f; cl; f_g; cl_g;
-        guarantees; all_vars; env }
+        guarantees; env }
 
     (*
       pass_cycle : var_def list -> E.t -> E.t
@@ -138,7 +91,7 @@ end = struct
 
     (* cycle : st -> cl -> env -> env *)
     let cycle st cl i =
-      (pass_cycle st.all_vars (E.apply_cl i cl)) 
+      (pass_cycle st.rp.all_vars (E.apply_cl i cl)) 
 
     (*
       loop : st -> env -> env -> env
@@ -173,10 +126,10 @@ end = struct
       y, z
 
     (*
-      do_prog : prog -> id -> unit
+      do_prog : rooted_prog -> unit
     *)
-    let do_prog widen_delay p root =
-      let st = init_state widen_delay p root in
+    let do_prog widen_delay rp =
+      let st = init_state widen_delay rp in
 
       let pnew = st.env in
       let pnew_c = E.apply_cl pnew st.cl in
@@ -209,13 +162,13 @@ end = struct
         Format.printf "@]@."
       end;
 
-      if List.exists (fun (p, _, _) -> p) st.all_vars then begin
+      if List.exists (fun (p, _, _) -> p) st.rp.all_vars then begin
         Format.printf "Probes:@[<v>";
         List.iter (fun (p, id, _) ->
           if p then Format.printf " %a ∊ %a@ "
                 Formula_printer.print_id id
                 E.print_itv (E.var_itv final id))
-          st.all_vars;
+          st.rp.all_vars;
         Format.printf "@]@."
       end
 
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 25e4b43..890f598 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -2,6 +2,7 @@ open Ast
 open Util
 open Ast_util
 open Formula
+open Typing
 
 open Interpret  (* used for constant evaluation ! *)
 
@@ -12,9 +13,8 @@ open Interpret  (* used for constant evaluation ! *)
 type scope = id * id * eqn ext list
 
 type transform_data = {
-    p           : Ast.prog;
+    rp          : rooted_prog;
     consts      : I.value VarMap.t;
-    root_scope  : scope;
     (* future : the automata state *)
 }
 
@@ -47,7 +47,9 @@ let rec f_of_nexpr td (node, prefix) where expr =
           | _ -> invalid_arity "binary_operator") b
       | _ -> invalid_arity "binary operator") a
   (* temporal *)
-  | AST_pre(_, id) -> where [NIdent id]
+  | AST_pre(expr, id) ->
+    let typ = type_expr td.rp node expr in
+      where (List.mapi (fun i _ -> NIdent (id^"."^(string_of_int i))) typ)
   | AST_arrow(a, b) ->
     f_or
       (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
@@ -60,7 +62,7 @@ let rec f_of_nexpr td (node, prefix) where expr =
       (f_and (f_of_expr td (node, prefix) c) (sub where a))
       (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b))
   | AST_instance ((f, _), args, nid) ->
-    let (n, _) = find_node_decl td.p f in
+    let (n, _) = find_node_decl td.rp.p f in
     where (List.map (fun (_, id, _) -> NIdent (node^"/"^nid^"/"^id)) n.ret)
     
   (* boolean values treated as integers *)
@@ -140,16 +142,22 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
         eq
     in
     let eq = List.fold_left (fun x i -> f_and (instance_eq i) x)
-      eq (extract_instances td.p e)
+      eq (extract_instances td.rp.p e)
     in
     let pre_expr (id, expr) =
       if active then
-        f_of_nexpr td (node, prefix) (function
-            | [v] -> BRel(AST_EQ, NIdent("N"^id), v)
-            | _ -> invalid_arity "pre on complex data not supported")
+        f_of_nexpr td (node, prefix) (fun elist ->
+            list_fold_op f_and
+              (List.mapi
+                (fun i v -> BRel(AST_EQ, NIdent("N"^id^"."^(string_of_int i)), v))
+                elist))
           expr
       else
-        BRel(AST_EQ, NIdent("N"^id), NIdent id)
+        let typ = type_expr td.rp node expr in
+        list_fold_op f_and
+          (List.mapi
+            (fun i _ -> let x = string_of_int i in BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x)))
+            typ)
     in
     List.fold_left (fun x i -> f_and (pre_expr i) x)
       eq (extract_pre e)
@@ -224,25 +232,24 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
     time_incr_eq
     (List.map do_eq eqs)
 
-and f_of_prog p root assume_guarantees =
+and f_of_prog rp assume_guarantees =
     let td = {
-      root_scope = get_root_scope p root;
-      p = p;
-      consts = I.consts p root;
+      rp = rp;
+      consts = I.consts rp;
     } in
 
-    f_of_scope true td td.root_scope assume_guarantees
+    f_of_scope true td td.rp.root_scope assume_guarantees
 
 (*
     Translate init state into a formula
 *)
-let rec init_f_of_scope p (node, prefix, eqs) =
+let rec init_f_of_scope rp (node, prefix, eqs) =
   let expr_eq e =
     let instance_eq (_, id, eqs, args) =
-     init_f_of_scope p (node^"/"^id, "", eqs)
+     init_f_of_scope rp (node^"/"^id, "", eqs)
     in
     List.fold_left (fun x i -> f_and (instance_eq i) x)
-      (BConst true) (extract_instances p e)
+      (BConst true) (extract_instances rp.p e)
   in
   let do_eq eq = match fst eq with
     | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
@@ -250,7 +257,7 @@ let rec init_f_of_scope p (node, prefix, eqs) =
     | AST_activate (b, _) ->
       let rec cond_eq = function
         | AST_activate_body b ->
-          init_f_of_scope p (node, b.act_id^".", b.body)
+          init_f_of_scope rp (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))
@@ -265,8 +272,8 @@ let rec init_f_of_scope p (node, prefix, eqs) =
   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)
+and init_f_of_prog rp =
+    init_f_of_scope rp rp.root_scope
 
 (*
     Get expressions for guarantee violation
@@ -277,7 +284,7 @@ let rec g_of_scope td (node, prefix, eqs) cond =
         g_of_scope td (node^"/"^id, "", eqs) cond
     in
     List.fold_left (fun x i -> (instance_g i) @ x)
-      [] (extract_instances td.p e)
+      [] (extract_instances td.rp.p e)
   in
   let do_eq eq = match fst eq with
     | AST_assign(_, e) | AST_assume(_, e) ->
@@ -299,11 +306,10 @@ let rec g_of_scope td (node, prefix, eqs) cond =
   in
   List.fold_left (@) [] (List.map do_eq eqs)
 
-and guarantees_of_prog p root =
+and guarantees_of_prog rp =
     let td = {
-      root_scope = get_root_scope p root;
-      p = p;
-      consts = I.consts p root;
+      rp = rp;
+      consts = I.consts rp;
     } in
 
-    g_of_scope td (get_root_scope p root) (BConst true)
+    g_of_scope td rp.root_scope (BConst true)