summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp.ml66
-rw-r--r--abstract/apron_domain.ml1
-rw-r--r--abstract/formula.ml21
-rw-r--r--abstract/transform.ml69
4 files changed, 120 insertions, 37 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index feaf037..d706f35 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -21,6 +21,9 @@ end = struct
env : E.t;
f : bool_expr;
cl : conslist;
+ f_g : bool_expr;
+ cl_g : conslist;
+ guarantees : (id * bool_expr) list;
}
@@ -73,8 +76,11 @@ end = struct
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) in
+ let f = Formula.eliminate_not (Transform.f_of_prog p root 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 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) ->
@@ -83,15 +89,25 @@ end = struct
all_vars
in
let init_f = Transform.init_f_of_prog p root in
+ let guarantees = Transform.guarantees_of_prog p root 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:@.%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 "Guarantees:@.";
+ List.iter (fun (id, f) ->
+ Format.printf " %s: %a@." id Formula_printer.print_expr f)
+ guarantees;
+ Format.printf "@.";
+
let env = E.apply_f env init_f in
- { p; root_scope; widen_delay; f; cl; all_vars; env }
+ { p; root_scope; widen_delay;
+ f; cl; f_g; cl_g;
+ guarantees; all_vars; env }
(*
pass_cycle : var_def list -> E.t -> E.t
@@ -125,35 +141,36 @@ end = struct
(pass_cycle st.all_vars (E.apply_cl i cl))
(*
- loop : st -> cl -> env -> env -> env
+ loop : st -> env -> env -> env
*)
- let loop st cycle_cl pnew stay =
+ let loop st pnew stay =
Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@."
- Formula_printer.print_conslist cycle_cl
+ Formula_printer.print_conslist st.cl
E.print_all pnew E.print_all stay;
- let add_stay = cycle st cycle_cl pnew in
+ let add_stay = cycle st st.cl pnew in
let acc0 = E.join stay add_stay in
- let fsharp i =
+ let fsharp cl i =
Format.printf "Acc @[<hv>%a@]@." E.print_all i;
- let j = cycle st cycle_cl i in
+ let j = cycle st cl i in
E.join acc0 j
in
let rec iter n i =
let i' =
if n < st.widen_delay
- then E.join i (fsharp i)
- else E.widen i (fsharp i)
+ then E.join i (fsharp st.cl_g i)
+ else E.widen i (fsharp st.cl_g i)
in
if E.eq i i' then i else iter (n+1) i'
in
let x = iter 0 acc0 in
- fix E.eq fsharp x (* decreasing iteration *)
-
+ let y = fix E.eq (fsharp st.cl_g) x in (* decreasing iteration *)
+ let z = E.apply_cl y st.cl in
+ y, z
(*
do_prog : prog -> id -> unit
@@ -163,16 +180,29 @@ end = struct
let pnew = st.env in
- let stay = loop st st.cl pnew (E.vbottom pnew) in
+ let stay, stay_c = loop st pnew (E.vbottom pnew) in
- let final = E.join (E.apply_cl pnew st.cl) (E.apply_cl stay st.cl) in
+ let final = E.join (E.apply_cl pnew st.cl) stay_c in
- Format.printf "@[<hov>Final %a@]@."
+ Format.printf "@[<hov>Final %a@]@.@."
E.print_all final;
- Format.printf "Probes:@[<hov>";
+ let check_guarantee (id, f) =
+ Format.printf "@[<hv>%s:@ %a@ "
+ id Formula_printer.print_expr f;
+ let z = E.apply_f final (BAnd(f, st.f)) in
+ if E.is_bot z then
+ Format.printf "OK@]@ "
+ else
+ Format.printf "FAIL@]@ "
+ in
+ Format.printf "Guarantees: @[<v 0>";
+ List.iter check_guarantee st.guarantees;
+ Format.printf "@]@.";
+
+ Format.printf "Probes:@[<v>";
List.iter (fun (p, id, _) ->
- if p then Format.printf "@ %a ∊ %a,"
+ if p then Format.printf " %a ∊ %a@ "
Formula_printer.print_id id
E.print_itv (E.var_itv final id))
st.all_vars;
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index d13afd7..cef6b66 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -133,6 +133,7 @@ module D : ENVIRONMENT_DOMAIN = struct
(* Pretty-printing *)
let print_all fmt x =
+ Abstract1.minimize manager x;
Abstract1.print fmt x;
Format.fprintf fmt "@?"
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 44495c4..f3c1df1 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -50,15 +50,18 @@ and eliminate_not_negate = function
| BBoolEq(id, v) -> BBoolEq(id, not v)
| BNot e -> eliminate_not e
| BRel(r, a, b) ->
- let r' = match r with
- | AST_EQ -> AST_NE
- | AST_NE -> AST_EQ
- | AST_LT -> AST_GE
- | AST_LE -> AST_GT
- | AST_GT -> AST_LE
- | AST_GE -> AST_LT
- in
- BRel(r', a, b)
+ if r = AST_EQ then
+ BOr(BRel(AST_LT, a, b), BRel(AST_GT, a, b))
+ else
+ let r' = match r with
+ | AST_EQ -> AST_NE
+ | AST_NE -> AST_EQ
+ | AST_LT -> AST_GE
+ | AST_LE -> AST_GT
+ | AST_GT -> AST_LE
+ | AST_GE -> AST_LT
+ in
+ BRel(r', a, b)
| BAnd(a, b) ->
BOr(eliminate_not_negate a, eliminate_not_negate b)
| BOr(a, b) ->
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 87da1bd..25e4b43 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -18,7 +18,6 @@ type transform_data = {
(* future : the automata state *)
}
-
(* f_of_nexpr :
transform_data -> (string, string) -> (num_expr list -> 'a) -> expr -> 'a
*)
@@ -122,10 +121,13 @@ and f_of_expr td (node, prefix) expr =
f_of_bexpr td (node, prefix) (fun x -> x) expr
-and f_of_scope active td (node, prefix, eqs) =
+(*
+ Translate program into one big formula
+*)
+let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
let expr_eq e eq =
let instance_eq (_, id, eqs, args) =
- let eq = f_of_scope active td (node^"/"^id, "", eqs) in
+ let eq = f_of_scope active td (node^"/"^id, "", eqs) assume_guarantees in
if active then
List.fold_left (fun eq ((_,argname,_), expr) ->
let eq_arg = f_of_nexpr td (node, prefix) (function
@@ -177,7 +179,13 @@ and f_of_scope active td (node, prefix, eqs) =
in
expr_eq e assume_eq
| AST_guarantee (_, e) ->
- expr_eq e (BConst true)
+ let guarantee_eq =
+ if active && assume_guarantees then
+ f_of_expr td (node, prefix) e
+ else
+ BConst true
+ in
+ expr_eq e guarantee_eq
| AST_activate (b, _) ->
let rec cond_eq = function
| AST_activate_body b -> BConst true
@@ -187,7 +195,7 @@ and f_of_scope active td (node, prefix, eqs) =
in
let rec do_tree_act = function
| AST_activate_body b ->
- f_of_scope true td (node, b.act_id^".", b.body)
+ f_of_scope true td (node, b.act_id^".", b.body) assume_guarantees
| AST_activate_if(c, a, b) ->
f_or
(f_and (f_of_expr td (node, prefix) c)
@@ -196,7 +204,7 @@ and f_of_scope active td (node, prefix, eqs) =
(f_and (do_tree_act b) (do_tree_inact a)))
and do_tree_inact = function
| AST_activate_body b ->
- f_of_scope false td (node, b.act_id^".", b.body)
+ f_of_scope false td (node, b.act_id^".", b.body) assume_guarantees
| AST_activate_if(_, a, b) ->
f_and (do_tree_inact a) (do_tree_inact b)
in
@@ -216,17 +224,18 @@ and f_of_scope active td (node, prefix, eqs) =
time_incr_eq
(List.map do_eq eqs)
-and f_of_prog p root =
+and f_of_prog p root assume_guarantees =
let td = {
root_scope = get_root_scope p root;
p = p;
consts = I.consts p root;
} in
- f_of_scope true td td.root_scope
-
-
+ f_of_scope true td td.root_scope assume_guarantees
+(*
+ Translate init state into a formula
+*)
let rec init_f_of_scope p (node, prefix, eqs) =
let expr_eq e =
let instance_eq (_, id, eqs, args) =
@@ -258,3 +267,43 @@ let rec init_f_of_scope p (node, prefix, eqs) =
and init_f_of_prog p root =
init_f_of_scope p (get_root_scope p root)
+
+(*
+ Get expressions for guarantee violation
+*)
+let rec g_of_scope td (node, prefix, eqs) cond =
+ let expr_g e =
+ let instance_g (_, id, eqs, args) =
+ g_of_scope td (node^"/"^id, "", eqs) cond
+ in
+ List.fold_left (fun x i -> (instance_g i) @ x)
+ [] (extract_instances td.p e)
+ in
+ let do_eq eq = match fst eq with
+ | AST_assign(_, e) | AST_assume(_, e) ->
+ expr_g e
+ | AST_guarantee((id, _), e) ->
+ (id, f_and cond (f_of_expr td (node, prefix) (AST_not(e), snd e)))
+ :: (expr_g e)
+ | AST_activate (b, _) ->
+ let rec cond_g cond = function
+ | AST_activate_body b ->
+ g_of_scope td (node, b.act_id^".", b.body) cond
+ | AST_activate_if(c, a, b) ->
+ (cond_g (f_and cond (f_of_expr td (node, prefix) c)) a) @
+ (cond_g (f_and cond (f_of_expr td (node, prefix) (AST_not(c), snd c))) b) @
+ (expr_g c)
+ in
+ cond_g cond b
+ | AST_automaton _ -> not_implemented "g_of_scope automaton"
+ in
+ List.fold_left (@) [] (List.map do_eq eqs)
+
+and guarantees_of_prog p root =
+ let td = {
+ root_scope = get_root_scope p root;
+ p = p;
+ consts = I.consts p root;
+ } in
+
+ g_of_scope td (get_root_scope p root) (BConst true)
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-24 16:15:55 +0000