From 43487d3baf695875482454ade1bdbc1403bfaaf6 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 18 Jun 2014 15:31:03 +0200 Subject: Add gilbreath suite ; booleans are not represented in a good way. --- abstract/abs_interp.ml | 27 +++++------ abstract/formula.ml | 20 ++++++++ abstract/formula_printer.ml | 5 ++ abstract/nonrelational.ml | 7 +-- abstract/transform.ml | 106 +++++++++++++++++++++++++------------------ frontend/ast_printer.ml | 2 +- main.ml | 14 +++++- tests/Makefile | 3 +- tests/result/gilbreath.out | 21 +++++++++ tests/result/limitera.out | 48 ++++++++++---------- tests/source/gilbreath.scade | 34 ++++++++++++++ tests/source/limiter.scade | 1 + tests/source/limitera.scade | 2 +- 13 files changed, 201 insertions(+), 89 deletions(-) create mode 100644 tests/result/gilbreath.out create mode 100644 tests/source/gilbreath.scade diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 4c3fddb..feaf037 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -9,12 +9,13 @@ module I (E : ENVIRONMENT_DOMAIN) : sig type st - val do_prog : prog -> id -> unit + val do_prog : int -> prog -> id -> unit end = struct type st = { p : prog; + widen_delay : int; root_scope : scope; all_vars : var_def list; env : E.t; @@ -69,7 +70,7 @@ end = struct (List.flatten (List.map vars_of_eq eqs)) (* init state *) - let init_state p root = + 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 @@ -86,11 +87,11 @@ end = struct Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f; - Format.printf "Vars: %a@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars; + Format.printf "Vars: @[%a@]@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars; let env = E.apply_f env init_f in - { p; root_scope; f; cl; all_vars; env } + { p; root_scope; widen_delay; f; cl; all_vars; env } (* pass_cycle : var_def list -> E.t -> E.t @@ -121,13 +122,12 @@ end = struct (* cycle : st -> cl -> env -> env *) let cycle st cl i = - E.apply_cl (pass_cycle st.all_vars i) cl + (pass_cycle st.all_vars (E.apply_cl i cl)) (* loop : st -> cl -> env -> env -> env *) let loop st cycle_cl pnew stay = - let pnew = E.apply_cl pnew cycle_cl in Format.printf "Loop @[%a@]@.New @[%a@]@.Stay @[%a@]@." Formula_printer.print_conslist cycle_cl @@ -142,10 +142,9 @@ end = struct E.join acc0 j in - let widen_delay = 10 in let rec iter n i = let i' = - if n < widen_delay + if n < st.widen_delay then E.join i (fsharp i) else E.widen i (fsharp i) in @@ -159,21 +158,23 @@ end = struct (* do_prog : prog -> id -> unit *) - let do_prog p root = - let st = init_state p root in + let do_prog widen_delay p root = + let st = init_state widen_delay p root in let pnew = st.env in let stay = loop st st.cl pnew (E.vbottom pnew) in - Format.printf "@[Final stay %a@]@." - E.print_all stay; + let final = E.join (E.apply_cl pnew st.cl) (E.apply_cl stay st.cl) in + + Format.printf "@[Final %a@]@." + E.print_all final; Format.printf "Probes:@["; List.iter (fun (p, id, _) -> if p then Format.printf "@ %a ∊ %a," Formula_printer.print_id id - E.print_itv (E.var_itv stay id)) + E.print_itv (E.var_itv final id)) st.all_vars; Format.printf "@]@." diff --git a/abstract/formula.ml b/abstract/formula.ml index 262bccb..44495c4 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -12,17 +12,31 @@ type num_expr = (* identifier *) | NIdent of id + type bool_expr = (* constants *) | BConst of bool (* operators from numeric values to boolean values *) | BRel of binary_rel_op * num_expr * num_expr + | BBoolEq of id * bool (* boolean operators *) | BAnd of bool_expr * bool_expr | BOr of bool_expr * bool_expr | BNot of bool_expr +let f_and a b = match a, b with + | BConst false, _ | _, BConst false -> BConst false + | BConst true, b -> b + | a, BConst true -> a + | a, b -> BAnd(a, b) + +let f_or a b = match a, b with + | BConst true, _ | _, BConst true -> BConst true + | BConst false, b -> b + | a, BConst false -> a + | a, b -> BOr(a, b) + (* Write all formula without using the NOT operator *) @@ -33,6 +47,7 @@ let rec eliminate_not = function | x -> x and eliminate_not_negate = function | BConst x -> BConst(not x) + | BBoolEq(id, v) -> BBoolEq(id, not v) | BNot e -> eliminate_not e | BRel(r, a, b) -> let r' = match r with @@ -83,6 +98,11 @@ let rec conslist_of_f = function in [cons], CLTrue | BConst x -> [], if x then CLTrue else CLFalse + | BBoolEq(id, v) -> + if v then + [NBinary(AST_MINUS, NIdent id, NIntConst 1), CONS_EQ], CLTrue + else + [NIdent id, CONS_EQ], CLTrue | BOr(a, b) -> let ca, ra = conslist_of_f a in let cb, rb = conslist_of_f b in diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml index 53a9b6a..1b31ba1 100644 --- a/abstract/formula_printer.ml +++ b/abstract/formula_printer.ml @@ -60,6 +60,11 @@ let rec print_num_expr fmt e = match e with let rec print_bool_expr fmt e = match e with | BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false") + | BBoolEq(id, v) -> + if v then + Format.fprintf fmt "%a" print_id id + else + Format.fprintf fmt "¬%a" print_id id | BRel(op, a, b) -> print_ch fmt print_num_expr ne_prec a be_prec e; Format.fprintf fmt "@ %s " (string_of_binary_rel op); diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 3cdcc31..855f970 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -215,14 +215,15 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct List.iteri (fun j (v, ids) -> if j > 0 then Format.fprintf fmt "@ "; + Format.fprintf fmt "@["; List.iteri (fun i id -> - if i > 0 then Format.fprintf fmt ", "; + if i > 0 then Format.fprintf fmt ",@ "; Format.fprintf fmt "%a" Formula_printer.print_id id) ids; match V.as_const v with - | Some i -> Format.fprintf fmt " = %d" i - | _ -> Format.fprintf fmt " ∊ %s" (V.to_string v)) + | Some i -> Format.fprintf fmt " = %d@]" i + | _ -> Format.fprintf fmt " ∊ %s@]" (V.to_string v)) sbl; Format.fprintf fmt " }@]" diff --git a/abstract/transform.ml b/abstract/transform.ml index b141cc6..87da1bd 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -18,11 +18,6 @@ type transform_data = { (* future : the automata state *) } -let f_and a b = - if a = BConst true then b - else if b = BConst true then a - else BAnd(a, b) - (* f_of_nexpr : transform_data -> (string, string) -> (num_expr list -> 'a) -> expr -> 'a @@ -55,48 +50,76 @@ let rec f_of_nexpr td (node, prefix) where expr = (* temporal *) | AST_pre(_, id) -> where [NIdent id] | AST_arrow(a, b) -> - BOr( - BAnd(BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0), - sub where a), - BAnd(BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1), - sub where b)) + f_or + (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0)) + (sub where a)) + (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1)) + (sub where b)) (* other *) | AST_if(c, a, b) -> - BOr( - BAnd(f_of_bexpr td (node, prefix) c, sub where a), - BAnd(BNot(f_of_bexpr td (node, prefix) c), sub where b)) + f_or + (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 where (List.map (fun (_, id, _) -> NIdent (node^"/"^nid^"/"^id)) n.ret) (* boolean values treated as integers *) | _ -> - BOr( - BAnd ((f_of_bexpr td (node, prefix) expr), where [NIntConst 1]), - BAnd (BNot(f_of_bexpr td (node, prefix) expr), where [NIntConst 0]) - ) + f_or + (f_and ((f_of_expr td (node, prefix) expr)) (where [NIntConst 1])) + (f_and (BNot(f_of_expr td (node, prefix) expr)) (where [NIntConst 0])) + -(* f_of_expr : +(* + f_of_expr : transform_data -> (string, string) -> expr -> bool_expr + f_of_bexpr : + transform_data -> (string, string) -> (bool_expr -> 'a) -> expr -> 'a *) -and f_of_bexpr td (node, prefix) expr = +and f_of_bexpr td (node, prefix) where expr = let sub = f_of_bexpr td (node, prefix) in match fst expr with - | AST_bool_const b -> BConst b - | AST_binary_bool(AST_AND, a, b) -> BAnd(sub a, sub b) - | AST_binary_bool(AST_OR, a, b) -> BOr(sub a, sub b) - | AST_not(a) -> BNot(sub a) + | AST_bool_const b -> where (BConst b) + | AST_binary_bool(AST_AND, a, b) -> f_and (sub where a) (sub where b) + | AST_binary_bool(AST_OR, a, b) -> f_or (sub where a) (sub where b) + | AST_not(a) -> BNot(sub where a) | AST_binary_rel(rel, a, b) -> - f_of_nexpr td (node, prefix) - (function - | [x] -> f_of_nexpr td (node, prefix) - (function - | [y] -> BRel(rel, x, y) - | _ -> invalid_arity "boolean relation") b - | _ -> invalid_arity "boolean relation") - a - | _ -> loc_error (snd expr) error "Invalid type : expected boolean value" - + where + (f_of_nexpr td (node, prefix) + (function + | [x] -> f_of_nexpr td (node, prefix) + (function + | [y] -> BRel(rel, x, y) + | _ -> invalid_arity "boolean relation") b + | _ -> invalid_arity "boolean relation") + a) + | AST_identifier (id, _) -> + let id = node^"/"^id in + f_or + (f_and (BBoolEq(id, true)) (where (BConst true))) + (f_and (BBoolEq(id, false)) (where (BConst false))) + (* temporal *) + | AST_pre(_, id) -> + f_or + (f_and (BBoolEq(id, true)) (where (BConst true))) + (f_and (BBoolEq(id, false)) (where (BConst false))) + | AST_arrow(a, b) -> + f_or + (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0)) + (sub where a)) + (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1)) + (sub where b)) + (* other *) + | AST_if(c, a, b) -> + f_or + (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)) + + | _ -> loc_error (snd expr) error "Expected boolean value." + +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) = @@ -148,7 +171,7 @@ and f_of_scope active td (node, prefix, eqs) = | AST_assume (_, e) -> let assume_eq = if active then - f_of_bexpr td (node, prefix) e + f_of_expr td (node, prefix) e else BConst true in @@ -166,12 +189,11 @@ and f_of_scope active td (node, prefix, eqs) = | AST_activate_body b -> f_of_scope true td (node, b.act_id^".", b.body) | AST_activate_if(c, a, b) -> - BOr( - f_and (f_of_bexpr td (node, prefix) c) - (f_and (do_tree_act a) (do_tree_inact b)), - f_and (BNot(f_of_bexpr td (node, prefix) c)) - (f_and (do_tree_act b) (do_tree_inact a)) - ) + f_or + (f_and (f_of_expr td (node, prefix) c) + (f_and (do_tree_act a) (do_tree_inact b))) + (f_and (BNot(f_of_expr td (node, prefix) c)) + (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) @@ -202,10 +224,6 @@ and f_of_prog p root = } in f_of_scope true td td.root_scope - - - - diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index c14d0d1..3ac881e 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -72,7 +72,7 @@ let print_list f sep fmt l = let rec aux = function | [] -> () | [a] -> f fmt a - | a::b -> f fmt a; Format.pp_print_string fmt sep; aux b + | a::b -> f fmt a; Format.fprintf fmt "%s@," sep; aux b in aux l diff --git a/main.ml b/main.ml index aa60c57..0ddf91c 100644 --- a/main.ml +++ b/main.ml @@ -3,13 +3,18 @@ open Ast module Interpret = Interpret.I module IntD = Nonrelational.D(Intervals_domain.VD) -module AI = Abs_interp.I(Apron_domain.D) +module AI_Int = Abs_interp.I(IntD) +module AI_Rel = Abs_interp.I(Apron_domain.D) (* command line options *) let dump = ref false let dumprn = ref false let test = ref false let vtest = ref false +let ai_int = ref false +let ai_rel = ref false +let ai_root = ref "test" +let ai_widen_delay = ref 3 let ifile = ref "" let usage = "usage: analyzer [options] file.scade" @@ -19,6 +24,10 @@ 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-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)."; ] let do_test_interpret prog verbose = @@ -66,7 +75,8 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - let () = AI.do_prog prog "test" in + if !ai_int then AI_Int.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 else if !test then do_test_interpret prog false; diff --git a/tests/Makefile b/tests/Makefile index f51eb61..7d5aac0 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -2,7 +2,8 @@ ALL_OUT=result/limiter.out result/limitera.out result/locals.out \ result/test4.out result/test5.out result/test7.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/test6.out result/testc.out \ + result/gilbreath.out bin/%.test: source/%.scade test.c rm kcg/* diff --git a/tests/result/gilbreath.out b/tests/result/gilbreath.out new file mode 100644 index 0000000..d6a0fa4 --- /dev/null +++ b/tests/result/gilbreath.out @@ -0,0 +1,21 @@ +0. 0 1 1 +1. 1 1 0 +2. 0 1 0 +3. 1 1 1 +4. 1 1 0 +5. 0 1 0 +6. 0 1 1 +7. 1 1 0 +8. 0 1 0 +9. 1 1 0 +10. 0 1 0 +11. 1 1 0 +12. 1 1 1 +13. 0 1 0 +14. 1 1 0 +15. 0 1 1 +16. 0 1 0 +17. 1 1 0 +18. 1 1 1 +19. 0 1 0 +20. 1 1 0 diff --git a/tests/result/limitera.out b/tests/result/limitera.out index 1851c7d..f047b8f 100644 --- a/tests/result/limitera.out +++ b/tests/result/limitera.out @@ -5,27 +5,27 @@ 4. 78 16 58 5. 99 16 74 6. 120 16 90 -7. -115 16 74 -8. -94 16 58 -9. -73 16 42 -10. -52 16 26 -11. -31 16 10 -12. -10 16 -6 -13. 11 16 10 -14. 32 16 26 -15. 53 16 42 -16. 74 16 58 -17. 95 16 74 -18. 116 16 90 -19. -119 16 74 -20. -98 16 58 -21. -77 16 42 -22. -56 16 26 -23. -35 16 10 -24. -14 16 -6 -25. 7 16 7 -26. 28 16 23 -27. 49 16 39 -28. 70 16 55 -29. 91 16 71 -30. 112 16 87 +7. -116 16 74 +8. -95 16 58 +9. -74 16 42 +10. -53 16 26 +11. -32 16 10 +12. -11 16 -6 +13. 10 16 10 +14. 31 16 26 +15. 52 16 42 +16. 73 16 58 +17. 94 16 74 +18. 115 16 90 +19. -121 16 74 +20. -100 16 58 +21. -79 16 42 +22. -58 16 26 +23. -37 16 10 +24. -16 16 -6 +25. 5 16 5 +26. 26 16 21 +27. 47 16 37 +28. 68 16 53 +29. 89 16 69 +30. 110 16 85 diff --git a/tests/source/gilbreath.scade b/tests/source/gilbreath.scade new file mode 100644 index 0000000..2723f9f --- /dev/null +++ b/tests/source/gilbreath.scade @@ -0,0 +1,34 @@ +node gilbreath_stream(c: bool) returns (o, probe property: bool) +var + half: bool; +let + activate + if c then + let + o = false -> not pre o; + tel + else + let + o = true -> not pre o; + tel + returns o; + + half = false -> not pre half; + + property = true -> not (half and (o = pre o)); +tel + +node test(i: int) returns (a, b, c: int; exit: bool) +var + cond: bool; + o, prop: bool; +let + exit = i >= 20; + cond = i mod 3 = 0 and not (i mod 7 = 2); + c = if cond then 1 else 0; + o, prop = gilbreath_stream(cond); + a = if o then 1 else 0; + b = if prop then 1 else 0; +tel + + diff --git a/tests/source/limiter.scade b/tests/source/limiter.scade index ff60567..fc9fb30 100644 --- a/tests/source/limiter.scade +++ b/tests/source/limiter.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 >= 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 1e4927e..e6db4e2 100644 --- a/tests/source/limitera.scade +++ b/tests/source/limitera.scade @@ -20,7 +20,7 @@ node limiter(x: int; d: int) returns (probe y: int) node test(i: int) returns(a, b, c: int; exit: bool) let exit = i >= 30; - a = (i * 21 + 122) mod (2 * bound) - bound; -- not really random + a = (i * 21 + 122) mod (2 * bound + 1) - bound; -- not really random b = 16; c = limiter(a, b); tel -- cgit v1.2.3