From 5a4165f55002876033c718303f86e9e1b7417745 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 18 Jun 2014 17:53:11 +0200 Subject: Nice view of guarantees ; add half test, proved. --- abstract/abs_interp.ml | 66 ++++++++++++++++++++++++++++++++------------- abstract/apron_domain.ml | 1 + abstract/formula.ml | 21 ++++++++------- abstract/transform.ml | 69 +++++++++++++++++++++++++++++++++++++++++------- 4 files changed, 120 insertions(+), 37 deletions(-) (limited to 'abstract') 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: @[%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 @[%a@]@.New @[%a@]@.Stay @[%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 @[%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 "@[Final %a@]@." + Format.printf "@[Final %a@]@.@." E.print_all final; - Format.printf "Probes:@["; + let check_guarantee (id, f) = + Format.printf "@[%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: @["; + List.iter check_guarantee st.guarantees; + Format.printf "@]@."; + + Format.printf "Probes:@["; 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) -- cgit v1.2.3