summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp.ml85
-rw-r--r--abstract/transform.ml58
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)
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 22:01:22 +0000