diff options
Diffstat (limited to 'abstract')
| -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 |
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) |