Do some typing ; support multiple pre in abstract interpretation.

4 files changed, 367 insertions, 0 deletions

diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 3ac881e..7ddcb67 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -1,5 +1,6 @@
 open Ast
 open Lexing
+open Typing
 
 
 (* Locations *)
@@ -252,3 +253,14 @@ let print_toplevel fmt = function
 
 let print_prog fmt p =
     List.iter (print_toplevel fmt) p
+
+
+(* Typed variable *)
+
+let print_type fmt = function
+    | TInt -> Format.fprintf fmt "int"
+    | TReal -> Format.fprintf fmt "real"
+    | TEnum e -> Format.fprintf fmt "enum { %a }" (print_list print_id ", ") e
+
+let print_typed_var fmt (p, id, t) =
+    Format.fprintf fmt "%s%s: %a" (if p then "probe " else "") id print_type t
diff --git a/frontend/ast_util.ml b/frontend/ast_util.ml
new file mode 100644
index 0000000..a7953ad
--- /dev/null
+++ b/frontend/ast_util.ml
@@ -0,0 +1,75 @@
+open Ast
+open Util
+
+(* Some errors *)
+
+let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v)
+let no_variable e = error ("No such variable: " ^ e)
+let type_error e = error ("Type error: " ^ e)
+let not_implemented e = error ("Not implemented: " ^ e)
+let invalid_arity e = error ("Invalid arity (" ^ e ^ ")")
+
+(* Utility : find declaration of a const / a node *)
+
+let find_const_decl p id =
+  match List.find (function
+                   | AST_const_decl (c, _) when c.c_name = id -> true
+                   | _ -> false) 
+                  p with
+  | AST_const_decl d -> d
+  | _ -> assert false
+
+let find_node_decl p id =
+  match List.find (function
+                   | AST_node_decl (c, _) when c.n_name = id -> true
+                   | _ -> false) 
+                  p with
+  | AST_node_decl d -> d
+  | _ -> assert false
+
+let extract_const_decls =
+  List.fold_left
+    (fun l d -> match d with
+      | AST_const_decl d -> d::l
+      | _ -> l)
+    []
+
+
+
+(* Utility : find instances declared in an expression *)
+
+(* extract_instances :
+      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 _
+  | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
+  | AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> extract_instances p e'
+  | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
+  | AST_arrow(e1, e2) ->
+    extract_instances p e1 @ extract_instances p e2
+  | AST_if(e1, e2, e3) ->
+    extract_instances p e1 @ extract_instances p e2 @ extract_instances p e3
+  | AST_instance((f, _), args, id) ->
+    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
+    (f, id, node.body, args_x)::more
+
+(* Utility : find pre declarations in an expression *)
+
+(* extract_pre : expr ext -> (id * expr ext) list *)
+let rec extract_pre e = match fst e with
+  | AST_identifier _ | AST_idconst _
+  | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
+  | AST_unary (_, e') | AST_not e' -> extract_pre e'
+  | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
+  | AST_arrow(e1, e2) ->
+    extract_pre e1 @ extract_pre e2
+  | AST_if(e1, e2, e3) ->
+    extract_pre e1 @ extract_pre e2 @ extract_pre e3
+  | AST_instance((f, _), args, id) ->
+    List.flatten (List.map extract_pre args)
+  | AST_pre(e', n) ->
+    (n, e')::(extract_pre e')
+
diff --git a/frontend/rename.ml b/frontend/rename.ml
new file mode 100644
index 0000000..9c4cc31
--- /dev/null
+++ b/frontend/rename.ml
@@ -0,0 +1,102 @@
+(* Scope analyzer *)
+
+open Ast
+open Util
+open Ast_util
+open Typing
+
+type renaming = (id * bool) VarMap.t    (* bool: is const ? *)
+
+(* consts_renaming : prog -> renaming *)
+let consts_renaming p =
+  let cdecl = extract_const_decls p in
+  List.fold_left
+    (fun rn (d,_) -> VarMap.add d.c_name (d.c_name, true) rn)
+    VarMap.empty
+    cdecl
+
+(* 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)
+
+(* rename_expr : expr ext -> renaming -> expr ext *)
+let rec rename_expr exp rn =
+  let sub e = rename_expr e rn in
+  let a = match fst exp with
+    | AST_identifier(id, l) ->
+      begin try let (nn, const) = VarMap.find id rn in
+          if const then AST_idconst(nn, l) else AST_identifier(nn, l)
+      with Not_found -> loc_error l no_variable id
+      end
+    | AST_idconst(id, l) -> assert false (* expression not already renamed *)
+    | AST_unary(op, e) -> AST_unary(op, sub e)
+    | AST_binary(op, a, b) -> AST_binary(op, sub a, sub b)
+    | AST_binary_rel(op, a, b) -> AST_binary_rel(op, sub a, sub b)
+    | AST_binary_bool(op, a, b) -> AST_binary_bool(op, sub a, sub b)
+    | AST_not(e) -> AST_not(sub e)
+    | AST_pre (e, x) -> AST_pre(sub e, x)
+    | AST_arrow(a, b) -> AST_arrow(sub a, sub b)
+    | AST_if(a, b, c) -> AST_if(sub a, sub b, sub c)
+    | AST_instance(i, l, s) -> AST_instance(i, List.map sub l, s)
+    | x -> x  (* other cases : constant literals *)
+  in a, snd exp
+
+(* rename_var : renaming -> id -> id *)
+let rename_var rn id =
+  try let (nn, const)= VarMap.find id rn in
+      if const then error ("Constant "^id^" cannot be defined in node.");
+      nn
+  with Not_found -> no_variable id
+
+let rename_var_ext rn (id, loc) = (rename_var rn id, loc)
+
+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 =
+  let a = match fst e with
+    | AST_assign(s, e) -> AST_assign (List.map (rename_var_ext rn) s, rename_expr e rn)
+    | AST_guarantee(g, e) -> AST_guarantee(g, rename_expr e rn)
+    | AST_assume(a, e) -> AST_assume(a, rename_expr e rn)
+    | AST_automaton(aid, states, ret) ->
+      let rename_state ((st:Ast.state),l) =
+        let rn = add_var_defs (aid^"."^st.st_name^".") rn st.st_locals in
+        { st with
+          st_locals = List.map (rename_var_def rn) st.st_locals;
+          body = List.map (rename_eqn rn) st.body;
+          until = List.map (fun (c, n, r) -> (rename_expr c rn, n, r)) st.until;
+        }, l
+      in 
+      AST_automaton(aid, List.map rename_state states, List.map (rename_var rn) ret)
+    | AST_activate (c, ret) ->
+      let rec rename_activate_if = function
+        | AST_activate_if(c, a, b) ->
+          AST_activate_if(rename_expr c rn, rename_activate_if a, rename_activate_if b)
+        | AST_activate_body b ->
+          let rn = add_var_defs (b.act_id^".") rn b.act_locals in
+          AST_activate_body{ b with
+            act_locals = List.map (rename_var_def rn) b.act_locals;
+            body = List.map (rename_eqn rn) b.body;
+          }
+      in
+      AST_activate(rename_activate_if c, List.map (rename_var rn) ret)
+  in a, snd e
+
+(* rename_node : renaming -> node_decl -> node_decl *)
+let rename_node const_rn node =
+  let rn = add_var_defs "" const_rn node.args in
+  let rn = add_var_defs "" rn node.ret in
+  let rn = add_var_defs "" rn node.var in
+  { node with
+    body = List.map (rename_eqn rn) node.body }
+
+(* rename_prog : prog -> prog *)
+let rename_prog p =
+  let const_rn = consts_renaming p in
+  let rn_toplevel = function
+  | AST_node_decl (n, l) -> AST_node_decl (rename_node const_rn n, l)
+  | x -> x
+  in
+  List.map rn_toplevel p
+
diff --git a/frontend/typing.ml b/frontend/typing.ml
new file mode 100644
index 0000000..07b3bcd
--- /dev/null
+++ b/frontend/typing.ml
@@ -0,0 +1,178 @@
+(* 
+    - Instanciate a program with a root node
+    - Enumerate all the variables, give them a type
+    - Give a type to expressions
+*)
+
+open Ast
+open Ast_util
+open Util
+
+type typ =
+    | TInt
+    | TReal
+    | TEnum of string list
+
+let bool_true = "T"
+let bool_false = "F"
+let bool_type = TEnum [bool_true; bool_false]
+
+let t_of_ast_t = function
+    | AST_TINT -> TInt
+    | AST_TREAL -> TReal
+    | AST_TBOOL -> bool_type
+
+
+(* probe? * variable full name * variable type *)
+type var = bool * id * typ
+
+(* path to node * subscope prefix in node * equations in scope *)
+type scope = id * id * eqn ext list
+
+type rooted_prog = {
+    p           : prog;
+    root_node   : node_decl;
+    root_scope  : scope;
+    all_vars    : var list;
+    const_vars  : var list;
+}
+
+(* Typing *)
+
+(*
+    type_expr_vl : prog -> var list -> string -> typ list
+*)
+let rec type_expr_vl p vl cvl node expr =
+    let sub = type_expr_vl p vl cvl node in
+    let err = loc_error (snd expr) type_error in
+    match fst expr with
+    (* Identifiers *)
+    | AST_identifier(id, _) ->
+        let _, _, t = List.find (fun (_, x, _) -> x = (node^"/"^id)) vl in [t]
+    | AST_idconst(id, _) ->
+        let _, _, t = List.find (fun (_, x, _) -> x = id) cvl in [t]
+    (* On numerical values *)
+    | AST_int_const _ -> [TInt]
+    | AST_real_const _ -> [TReal]
+    | AST_unary (_, se) ->
+        begin match sub se with
+        | [TInt] -> [TInt]
+        | [TReal] -> [TReal]
+        | _ -> err "Invalid argument for unary."
+        end
+    | AST_binary(_, a, b) ->
+        begin match sub a, sub b with
+        | [TInt], [TInt] -> [TInt]
+        | [TReal], [TReal] -> [TReal]
+        | [TInt], [TReal] | [TReal], [TInt] -> [TReal]
+        | _ -> err "Invalid argument for binary."
+        end
+    (* On boolean values *)
+    | AST_bool_const _ -> [bool_type]
+    | AST_binary_rel _ -> [bool_type] (* do not check subtypes... TODO? *)
+    | AST_binary_bool _ -> [bool_type] (* the same *)
+    | AST_not _ -> [bool_type] (* the same *)
+    (* Temporal primitives *) 
+    | AST_pre(e, _) -> sub e
+    | AST_arrow(a, b) ->
+      let ta, tb = sub a, sub b in
+      if ta = tb then ta
+        else err "Arrow does not have same type on both sides."
+    (* other *)
+    | AST_if(c, a, b) ->
+      let ta, tb = sub a, sub b in
+      if ta = tb then ta
+        else err "If does not have same type on both branches."
+    | AST_instance((f, _), _, _) ->
+      (* do not check types of arguments... TODO? *)
+      let (n, _) = find_node_decl p f in
+      List.map (fun (_, _, t) -> t_of_ast_t t) n.ret
+
+
+(* type_expr : tp -> string -> typ list *)
+let type_expr tp = type_expr_vl tp.p tp.all_vars tp.const_vars
+
+
+(* Program rooting *)
+
+
+(*  decls_of_node : node_decl -> var_decl list       *)
+let decls_of_node n = n.args @ n.ret @ n.var
+
+(*  vars_in_node string -> var_decl list -> var list *)
+let vars_in_node nid =
+  List.map (fun (p, id, t) -> p, nid^"/"^id, t_of_ast_t t)
+
+(* node_vars : prog -> id -> string -> var list      *)
+let node_vars p f nid =
+    let (n, _) = find_node_decl p f in
+    vars_in_node nid (decls_of_node n)
+
+(*
+    extract_all_vars : prog -> scope -> var 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) n_vars const_vars =
+    let vars_of_expr e =
+      List.flatten
+        (List.map
+          (fun (f, id, eqs, args) ->
+            let nv = node_vars p f (node^"/"^id) in
+            nv @ extract_all_vars p (node^"/"^id, "", eqs) nv const_vars)
+          (extract_instances p e))
+      @
+      List.flatten
+        (List.map
+          (fun (id, expr) ->
+              let vd =
+                List.mapi
+                  (fun i t -> false, id^"."^(string_of_int i), t)
+                  (type_expr_vl p n_vars const_vars node expr)
+              in
+              vd @ (List.map (fun (a, x, c) -> (a, "N"^x, c)) vd))
+          (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 ->
+            let bvars = vars_in_node node b.act_locals in
+            bvars @
+              extract_all_vars p
+                (node, b.act_id^".", b.body)
+                (bvars@n_vars)
+                const_vars
+          | 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", TInt)::
+      (false, "N"^node^"/"^prefix^"time", TInt)::
+      (List.flatten (List.map vars_of_eq eqs))
+
+
+(*
+    root_prog : prog -> id -> rooted_prog
+*)
+let root_prog p root =
+    let (n, _) = find_node_decl p root in
+    let root_scope = ("", "", n.body) in
+
+    let const_vars = List.map
+        (fun (cd, _) -> (false, cd.c_name, t_of_ast_t cd.typ))
+        (extract_const_decls p)
+    in
+
+    let root_vars = vars_in_node "" (decls_of_node n) in
+    
+    { p; root_scope; root_node = n;
+      const_vars = const_vars;
+      all_vars = root_vars @ extract_all_vars p root_scope root_vars const_vars }
+
+