diff options
| -rw-r--r-- | abstract/abs_interp.ml | 66 | ||||
| -rw-r--r-- | abstract/apron_domain.ml | 1 | ||||
| -rw-r--r-- | abstract/formula.ml | 21 | ||||
| -rw-r--r-- | abstract/transform.ml | 69 | ||||
| -rw-r--r-- | main.ml | 10 | ||||
| -rw-r--r-- | tests/Makefile | 2 | ||||
| -rw-r--r-- | tests/result/half.out | 21 | ||||
| -rw-r--r-- | tests/source/gilbreath.scade | 2 | ||||
| -rw-r--r-- | tests/source/half.scade | 29 | ||||
| -rw-r--r-- | tests/source/limiter.scade | 2 | ||||
| -rw-r--r-- | tests/source/limitera.scade | 1 |
11 files changed, 180 insertions, 44 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) @@ -2,8 +2,8 @@ open Ast module Interpret = Interpret.I -module IntD = Nonrelational.D(Intervals_domain.VD) -module AI_Int = Abs_interp.I(IntD) +module ItvD = Nonrelational.D(Intervals_domain.VD) +module AI_Itv = Abs_interp.I(ItvD) module AI_Rel = Abs_interp.I(Apron_domain.D) (* command line options *) @@ -11,7 +11,7 @@ let dump = ref false let dumprn = ref false let test = ref false let vtest = ref false -let ai_int = ref false +let ai_itv = ref false let ai_rel = ref false let ai_root = ref "test" let ai_widen_delay = ref 3 @@ -24,7 +24,7 @@ let options = [ "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming."; "--vtest", Arg.Set vtest, "Verbose testing."; "--test", Arg.Set test, "Simple testing."; - "--ai-int", Arg.Set ai_int, "Do abstract analysis using intervals."; + "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals."; "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron."; "--ai-root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test)."; "--ai-wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3)."; @@ -75,7 +75,7 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - if !ai_int then AI_Int.do_prog !ai_widen_delay prog !ai_root; + if !ai_itv then AI_Itv.do_prog !ai_widen_delay prog !ai_root; if !ai_rel then AI_Rel.do_prog !ai_widen_delay prog !ai_root; if !vtest then do_test_interpret prog true diff --git a/tests/Makefile b/tests/Makefile index 7d5aac0..165f4ec 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -3,7 +3,7 @@ ALL_OUT=result/limiter.out result/limitera.out result/locals.out \ result/train.out result/updown.out result/updown_fail.out \ result/test0.out result/test1.out result/test2.out result/test3.out \ result/test6.out result/testc.out \ - result/gilbreath.out + result/gilbreath.out result/half.out bin/%.test: source/%.scade test.c rm kcg/* diff --git a/tests/result/half.out b/tests/result/half.out new file mode 100644 index 0000000..c2085c5 --- /dev/null +++ b/tests/result/half.out @@ -0,0 +1,21 @@ +0. 1 0 1 +1. 1 1 0 +2. 2 1 1 +3. 2 2 0 +4. 3 2 1 +5. 3 3 0 +6. 4 3 1 +7. 4 4 0 +8. 5 4 1 +9. 5 5 0 +10. 6 5 1 +11. 6 6 0 +12. 7 6 1 +13. 7 7 0 +14. 8 7 1 +15. 8 8 0 +16. 9 8 1 +17. 9 9 0 +18. 10 9 1 +19. 10 10 0 +20. 11 10 1 diff --git a/tests/source/gilbreath.scade b/tests/source/gilbreath.scade index 2723f9f..e0b7245 100644 --- a/tests/source/gilbreath.scade +++ b/tests/source/gilbreath.scade @@ -16,6 +16,8 @@ let half = false -> not pre half; property = true -> not (half and (o = pre o)); + + guarantee p_true : property; tel node test(i: int) returns (a, b, c: int; exit: bool) diff --git a/tests/source/half.scade b/tests/source/half.scade new file mode 100644 index 0000000..da90586 --- /dev/null +++ b/tests/source/half.scade @@ -0,0 +1,29 @@ +node test(i: int) returns (a, b, probe c: int; exit: bool) +var + la, lb: int; + half: bool; +let + exit = i >= 20; + + half = true -> not pre half; + + la = 0 -> pre a; + lb = 0 -> pre b; + activate + if half then + let + a = la + 1; + b = lb; + tel + else + let + a = la; + b = lb + 1; + tel + returns a, b; + + c = a - b; + + guarantee c_bounded: c >= 0 and c <= 1; + guarantee link_c_half: (half and c = 1) or ((not half) and c = 0); +tel diff --git a/tests/source/limiter.scade b/tests/source/limiter.scade index fc9fb30..05cb2b7 100644 --- a/tests/source/limiter.scade +++ b/tests/source/limiter.scade @@ -4,7 +4,7 @@ node limiter(x: int; d: int) returns (probe y: int) var s, r: int; let assume in_bounded: x >= -bound and x <= bound; - assume d_bounded: d >= 0 and d >= 16; + assume d_bounded: d >= 0 and d <= 16; guarantee out_bounded: y >= -bound and y <= bound; s = 0 -> pre y; r = x - s; diff --git a/tests/source/limitera.scade b/tests/source/limitera.scade index e6db4e2..2b87278 100644 --- a/tests/source/limitera.scade +++ b/tests/source/limitera.scade @@ -4,6 +4,7 @@ node limiter(x: int; d: int) returns (probe y: int) var s, r: int; let assume in_bounded: x >= -bound and x <= bound; + assume d_bounded: d = 16; guarantee out_bounded: y >= -bound and y <= bound; s = 0 -> pre y; r = x - s; |