diff options
| -rw-r--r-- | abstract/abs_interp.ml | 129 | ||||
| -rw-r--r-- | abstract/apron_domain.ml | 11 | ||||
| -rw-r--r-- | abstract/environment_domain.ml | 2 | ||||
| -rw-r--r-- | abstract/transform.ml | 57 | ||||
| -rw-r--r-- | frontend/ast.ml | 2 | ||||
| -rw-r--r-- | frontend/ast_printer.ml | 2 | ||||
| -rw-r--r-- | frontend/parser.mly | 2 | ||||
| -rw-r--r-- | interpret/ast_util.ml | 4 | ||||
| -rw-r--r-- | interpret/interpret.ml | 14 | ||||
| -rw-r--r-- | interpret/rename.ml | 4 | ||||
| -rw-r--r-- | main.ml | 8 |
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 = @@ -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; |