diff options
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | abstract/abs_interp.ml | 85 | ||||
| -rw-r--r-- | abstract/transform.ml | 58 | ||||
| -rw-r--r-- | frontend/ast_printer.ml | 12 | ||||
| -rw-r--r-- | frontend/ast_util.ml (renamed from interpret/ast_util.ml) | 25 | ||||
| -rw-r--r-- | frontend/rename.ml (renamed from interpret/rename.ml) | 3 | ||||
| -rw-r--r-- | frontend/typing.ml | 178 | ||||
| -rw-r--r-- | interpret/interpret.ml | 24 | ||||
| -rw-r--r-- | main.ml | 6 |
9 files changed, 270 insertions, 126 deletions
@@ -8,6 +8,9 @@ SRC= main.ml \ frontend/parser.mly \ frontend/lexer.mll \ frontend/ast_printer.ml \ + frontend/typing.ml \ + frontend/ast_util.ml \ + frontend/rename.ml \ abstract/formula.ml \ abstract/formula_printer.ml \ abstract/transform.ml \ @@ -17,8 +20,6 @@ SRC= main.ml \ abstract/nonrelational.ml \ abstract/intervals_domain.ml \ interpret/interpret.ml \ - interpret/ast_util.ml \ - interpret/rename.ml all: $(BIN) 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) 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/interpret/ast_util.ml b/frontend/ast_util.ml index 9cfe995..a7953ad 100644 --- a/interpret/ast_util.ml +++ b/frontend/ast_util.ml @@ -1,6 +1,14 @@ 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 = @@ -27,16 +35,6 @@ let extract_const_decls = [] -(* Utility : scopes *) - - -(* path to node * subscope prefix in node * equations in scope *) -type scope = id * id * eqn ext list - -let get_root_scope p root = - let (n, _) = find_node_decl p root in - ("", "", n.body) - (* Utility : find instances declared in an expression *) @@ -75,10 +73,3 @@ let rec extract_pre e = match fst e with | AST_pre(e', n) -> (n, e')::(extract_pre e') -(* 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 ^ ")") diff --git a/interpret/rename.ml b/frontend/rename.ml index 654b101..9c4cc31 100644 --- a/interpret/rename.ml +++ b/frontend/rename.ml @@ -3,8 +3,9 @@ open Ast open Util open Ast_util +open Typing -type renaming = (id * bool) VarMap.t +type renaming = (id * bool) VarMap.t (* bool: is const ? *) (* consts_renaming : prog -> renaming *) let consts_renaming 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 } + + diff --git a/interpret/interpret.ml b/interpret/interpret.ml index 6f7c90e..b9a5576 100644 --- a/interpret/interpret.ml +++ b/interpret/interpret.ml @@ -1,6 +1,7 @@ open Ast open Util open Ast_util +open Typing module I : sig @@ -26,13 +27,13 @@ module I : sig (* Get the constants only *) - val consts : prog -> id -> value VarMap.t + val consts : rooted_prog -> value VarMap.t (* Construct initial state for a program. The id is the root node of the program evaluation. *) - val init_state : prog -> id -> state + val init_state : rooted_prog -> state (* Run a step of the program (not necessary to specify the program, @@ -88,6 +89,7 @@ end = struct type state = { + rp : rooted_prog; p : prog; root_scope : scope; outputs : id list; @@ -441,13 +443,13 @@ end = struct (* init_state : prog -> id -> state *) - let init_state p root = - let (n, _) = find_node_decl p root in + let init_state rp = let st = { - p = p; - root_scope = get_root_scope p root; + rp = rp; + p = rp.p; + root_scope = rp.root_scope; save = VarMap.empty; - outputs = (List.map (fun (_,n,_) -> n) n.ret); + outputs = (List.map (fun (_,n,_) -> n) rp.root_node.ret); } in let env = { st = st; vars = Hashtbl.create 42 } in @@ -461,11 +463,11 @@ end = struct | [v] -> Hashtbl.replace env.vars cpath v | _ -> loc_error l error "Arity error in constant expression.")) | _ -> ()) - p; + rp.p; List.iter (function | AST_const_decl(d, l) -> ignore (get_var env "cst" d.c_name) | _ -> ()) - p; + rp.p; reset_scope env st.root_scope; { st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty } @@ -485,7 +487,7 @@ end = struct do_weak_transitions env st.root_scope; extract_st env, out - let consts p root = - (init_state p root).save + let consts rp = + (init_state rp).save end @@ -31,7 +31,7 @@ let options = [ ] let do_test_interpret prog verbose = - let s0 = Interpret.init_state prog "test" in + let s0 = Interpret.init_state (Typing.root_prog prog "test") in if verbose then begin Format.printf "Init state:@."; Interpret.print_state Format.std_formatter s0; @@ -75,8 +75,8 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - if !ai_itv then AI_Itv.do_prog !ai_widen_delay prog !ai_root; - if !ai_rel then AI_Rel.do_prog !ai_widen_delay prog !ai_root; + if !ai_itv then AI_Itv.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root); + if !ai_rel then AI_Rel.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root); if !vtest then do_test_interpret prog true else if !test then do_test_interpret prog false; |