diff options
| -rw-r--r-- | abstract/abs_domain.ml | 49 | ||||
| -rw-r--r-- | abstract/abs_interp.ml | 4 | ||||
| -rw-r--r-- | abstract/formula.ml | 10 | ||||
| -rw-r--r-- | abstract/formula_printer.ml | 2 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 6 | ||||
| -rw-r--r-- | abstract/transform.ml | 44 | ||||
| -rw-r--r-- | frontend/ast_printer.ml | 2 | ||||
| -rw-r--r-- | frontend/typing.ml | 19 | ||||
| -rw-r--r-- | main.ml | 25 | ||||
| -rw-r--r-- | tests/source/updown.scade | 2 | ||||
| -rw-r--r-- | tests/source/uturn.scade | 76 |
11 files changed, 160 insertions, 79 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml index 64eefc7..d6ff489 100644 --- a/abstract/abs_domain.ml +++ b/abstract/abs_domain.ml @@ -131,7 +131,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct if i > 0 then Format.fprintf fmt ",@ "; Format.fprintf fmt "%a" Formula_printer.print_id id) ids; - Format.fprintf fmt " = %s@]" v) + Format.fprintf fmt " ≡ %s@]" v) sbl; Format.fprintf fmt " }@]" @@ -171,16 +171,23 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct let strict value = VMap.filter (fun _ v -> not (ND.is_bot v)) value - let add_case x (enum, num) = + let add_case_w widen x (enum, num) = let value = x.value in let enum = VarMap.filter (fun k v -> not (List.mem k x.nodisj_v)) enum in let v = - if VMap.exists (fun e0 n0 -> Valuation.subset enum e0 && ND.subset num n0) value || ND.is_bot num then + if VMap.exists + (fun e0 n0 -> Valuation.subset enum e0 && ND.subset num n0) + value + || ND.is_bot num + then value else - try VMap.add enum (ND.join num (VMap.find enum value)) value + try VMap.add enum + ((if widen then ND.widen else ND.join) (VMap.find enum value) num) + value with Not_found -> VMap.add enum num value in { x with value = v } + let add_case = add_case_w false let addvar x id ty = match ty with | TInt | TReal -> @@ -252,18 +259,18 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct let join x y = VMap.fold (fun enum num value -> add_case value (enum, num)) - x.value - y + y.value + x let meet x y = not_implemented "meet for enum+num domain" let widen x y = - { x with - value = VMap.merge - (fun _ a b -> match a, b with - | None, Some a -> Some a - | Some a, None -> Some a - | Some a, Some b -> Some (ND.widen a b) - | _ -> assert false) - x.value y.value } + let value = VMap.merge + (fun _ a b -> match a, b with + | Some x, None -> Some x + | None, Some y -> Some y + | Some x, Some y -> Some (ND.widen x y) + | _ -> None) + x.value y.value + in { x with value = value } (* Some cases of subset/equality not detected *) let subset a b = @@ -281,13 +288,9 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct VMap.fold (fun enum num value -> match a, b with - | EItem x, EItem y -> - if (x = y && op = E_EQ) || (x <> y && op = E_NE) - then add_case value (enum, num) - else value - | EItem u, EIdent i | EIdent i, EItem u -> - begin try let y = VarMap.find i enum in - if (u = y && op = E_EQ) || (u <> y && op = E_NE) + | i, EItem u -> + begin try let v = VarMap.find i enum in + if (if op = E_EQ then u = v else u <> v) then add_case value (enum, num) else value with Not_found -> @@ -300,11 +303,11 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct value (List.filter ((<>) u) (List.assoc i x.evars)) end - | EIdent i, EIdent j -> + | i, EIdent j -> begin try let x = VarMap.find i enum in try let y = VarMap.find j enum in - if (x = y && op = E_EQ) || (x <> y && op = E_NE) + if (if op = E_EQ then x = y else x <> y) then add_case value (enum, num) else value with Not_found (* J not found *) -> diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 383a69c..a610843 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -111,14 +111,14 @@ end = struct let rec iter n i = let i' = if n < st.widen_delay - then E.join i (fsharp st.cl_g i) + then E.join i (fsharp st.cl 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 - let y = fix E.eq (fsharp st.cl_g) x in (* decreasing iteration *) + let y = fix E.eq (fsharp st.cl) x in (* decreasing iteration *) let z = E.apply_cl y st.cl in (* no more guarantee *) y, z diff --git a/abstract/formula.ml b/abstract/formula.ml index 62acb28..cb7a4c4 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -34,7 +34,7 @@ type enum_expr = type enum_op = | E_EQ | E_NE -type enum_cons = enum_op * enum_expr * enum_expr +type enum_cons = enum_op * id * enum_expr type bool_expr = (* constants *) @@ -62,10 +62,10 @@ let f_or a b = match a, b with | a, BConst false -> a | a, b -> BOr(a, b) -let f_e_eq a b = match a, b with - | EItem u, EItem v -> BConst (u = v) - | _ -> BEnumCons(E_EQ, a, b) - +let f_e_op op a b = match a, b with + | EItem i, EItem j -> BConst (if op = E_EQ then i = j else i <> j) + | EIdent x, v | v, EIdent x -> BEnumCons(op, x, v) +let f_e_eq = f_e_op E_EQ (* Write all formula without using the NOT operator *) diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml index 0c7d65e..383500c 100644 --- a/abstract/formula_printer.ml +++ b/abstract/formula_printer.ml @@ -68,7 +68,7 @@ let str_of_enum_op = function let print_econs fmt (op, a, b) = Format.fprintf fmt "%a %s %a" - print_enum_expr a (str_of_enum_op op) print_enum_expr b + print_id a (str_of_enum_op op) print_enum_expr b (* Print boolean form of formula *) diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index bbdc875..6497760 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -104,11 +104,7 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct let eq a b = match a, b with | Bot, Bot -> true | Env m, Env n -> - VarMap.for_all2o - (fun _ _ -> false) - (fun _ _ -> false) - (fun _ a b -> a = b) - m n + VarMap.equal (=) m n | _ -> false (* Apply some formula to the environment *) diff --git a/abstract/transform.ml b/abstract/transform.ml index 6fa1277..b6781a8 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -136,7 +136,7 @@ and f_of_bexpr td (node, prefix) where expr = | AST_EQ -> E_EQ | AST_NE -> E_NE | _ -> type_error "Invalid operator on enumerated values." - in BEnumCons(eop, x, y) + in f_e_op eop x y | _ -> invalid_arity "Binary operator") (AST_tuple [a; b], snd expr)) (* Temporal *) @@ -233,12 +233,18 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = BConst true in f_and (expr_eq e) assume_eq - | AST_guarantee (_, e) -> + | AST_guarantee ((id, _), e) -> + let gn = node^"/g_"^id in let guarantee_eq = if active && assume_guarantees then - f_of_expr td (node, prefix) e + f_and (f_of_expr td (node, prefix) e) + (BEnumCons(E_EQ, gn, EItem bool_true)) else - BConst true + f_or + (f_and (f_of_expr td (node, prefix) e) + (BEnumCons(E_EQ, gn, EItem bool_true))) + (f_and (BNot (f_of_expr td (node, prefix) e)) + (BEnumCons(E_EQ, gn, EItem bool_false))) in f_and (expr_eq e) guarantee_eq | AST_activate (b, _) -> @@ -265,8 +271,8 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = in f_and (cond_eq b) (if active then do_tree_act b else do_tree_inact b) | AST_automaton (aid, states, _) -> - let stv = EIdent (node^"/"^aid^".state") in - let nstv = EIdent ("N"^node^"/"^aid^".state") in + let stv = node^"/"^aid^".state" in + let nstv = "N"^node^"/"^aid^".state" in let st_eq_inact (st, _) = f_and (f_of_scope false td @@ -304,13 +310,9 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = then BRel(AST_EQ, NIdent("N"^node^"/"^prefix^"time"), NBinary(AST_PLUS, NIntConst 1, NIdent(node^"/"^prefix^"time"))) else BConst true) - (f_and - (if List.mem (node^"/") td.rp.act_scope - then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_true) - else BConst true) - (if List.mem (node^"/") td.rp.init_scope - then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false) - else BConst true)) + (if List.mem (node^"/") td.rp.init_scope + then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) (EItem bool_false) + else BConst true) else f_and (if not (List.mem (node^"/") td.rp.no_time_scope) @@ -318,14 +320,10 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = NIdent("N"^node^"/"^prefix^"time"), NIdent(node^"/"^prefix^"time")) else BConst true) - (f_and - (if List.mem (node^"/") td.rp.act_scope - then f_e_eq (EIdent(node^"/"^prefix^"act")) (EItem bool_false) - else BConst true) - (if List.mem (node^"/") td.rp.init_scope - then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) - (EIdent (node^"/"^prefix^"init")) - else BConst true)) + (if List.mem (node^"/") td.rp.init_scope + then f_e_eq (EIdent("N"^node^"/"^prefix^"init")) + (EIdent (node^"/"^prefix^"init")) + else BConst true) in List.fold_left f_and time_incr_eq @@ -364,7 +362,7 @@ let rec init_f_of_scope rp (node, prefix, eqs) = cond_eq b | AST_automaton (aid, states, _) -> let (st, _) = List.find (fun (st, _) -> st.initial) states in - let init_eq = BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name) in + let init_eq = BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name) in let state_eq (st, _) = let sc_f = init_f_of_scope rp (node, aid^"."^st.st_name^".", st.body) @@ -421,7 +419,7 @@ let rec g_of_scope td (node, prefix, eqs) cond = | AST_automaton (aid, states, _) -> let st_g (st, _) = g_of_scope td (node, aid^"."^st.st_name^".", st.body) - (f_and cond (BEnumCons(E_EQ, EIdent(node^"/"^aid^".state"), EItem st.st_name))) + (f_and cond (BEnumCons(E_EQ, node^"/"^aid^".state", EItem st.st_name))) in List.flatten (List.map st_g states) in diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index ac30fe9..b6c06fb 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -264,7 +264,7 @@ let print_prog fmt p = let print_type fmt = function | TInt -> Format.fprintf fmt "int" | TReal -> Format.fprintf fmt "real" - | TEnum e -> Format.fprintf fmt "enum { %a }" (print_list print_id ", ") e + | TEnum e -> Format.fprintf fmt "enum @[<h>{ %a }@]" (print_list print_id ", ") e let print_typed_var fmt (p, id, t) = Format.fprintf fmt "%s%s: %a" (if p then "probe " else "") id print_type t diff --git a/frontend/typing.ml b/frontend/typing.ml index 564d91e..0417d27 100644 --- a/frontend/typing.ml +++ b/frontend/typing.ml @@ -33,7 +33,6 @@ type rooted_prog = { p : prog; no_time_scope : id list; (* scopes in which not to introduce time variable *) - act_scope : id list; (* scopes in which to introduce act variable *) init_scope : id list; (* scopes in which to introduce init variable *) root_node : node_decl; @@ -146,7 +145,10 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = (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_assign(_, e) | AST_assume(_, e) -> vars_of_expr e + | AST_guarantee((id, _), e) -> + let gn = node^"/g_"^id in + (false, gn, bool_type)::vars_of_expr e | AST_activate (b, _) -> let rec do_branch = function | AST_activate_body b -> @@ -183,10 +185,6 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = (false, "N"^node^"/"^prefix^"time", TInt)::v else v in let v = - if List.mem (node^"/") rp.act_scope - then (false, node^"/"^prefix^"act", bool_type)::v - else v in - let v = if List.mem (node^"/") rp.init_scope then (false, node^"/"^prefix^"init", bool_type):: @@ -196,9 +194,9 @@ let rec extract_all_vars rp (node, prefix, eqs) n_vars = (* - root_prog : prog -> id -> rooted_prog + root_prog : prog -> id -> string list -> string list -> rooted_prog *) -let root_prog p root = +let root_prog p root no_time_scope init_scope = let (root_node, _) = find_node_decl p root in let root_scope = ("", "", root_node.body) in @@ -212,9 +210,8 @@ let root_prog p root = let rp = { p; root_scope; root_node; - no_time_scope = ["/"]; - act_scope = []; - init_scope = ["/"]; + no_time_scope; + init_scope; const_vars; all_vars = [] } in @@ -19,6 +19,8 @@ let ai_itv = ref false let ai_rel = ref false let ai_root = ref "test" let ai_widen_delay = ref 3 +let ai_no_time_scopes = ref "" +let ai_init_scopes = ref "" let ifile = ref "" let usage = "usage: analyzer [options] file.scade" @@ -26,16 +28,18 @@ let usage = "usage: analyzer [options] file.scade" let options = [ "--dump", Arg.Set dump, "Dump program source."; "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming."; - "--vtest", Arg.Set vtest, "Verbose testing."; - "--test", Arg.Set test, "Simple testing."; + "--vtest", Arg.Set vtest, "Verbose testing (direct interpret)."; + "--test", Arg.Set test, "Simple testing (direct interpret)."; "--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)."; + "--wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3)."; + "--root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test)."; + "--no-time", Arg.Set_string ai_no_time_scopes, "Scopes for which not to introduce a 'time' variable in analysis."; + "--init", Arg.Set_string ai_init_scopes, "Scopes for which to introduce a 'init' variable in analysis."; ] let do_test_interpret prog verbose = - let s0 = Interpret.init_state (Typing.root_prog prog "test") in + let s0 = Interpret.init_state (Typing.root_prog prog "test" [] []) in if verbose then begin Format.printf "Init state:@."; Interpret.print_state Format.std_formatter s0; @@ -79,8 +83,15 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - if !ai_itv then AI_Itv.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root); - if !ai_rel then AI_Rel.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root); + if !ai_itv || !ai_rel then begin + let comma_split = Str.split (Str.regexp ",") in + let rp = Typing.root_prog prog !ai_root + (comma_split !ai_no_time_scopes) + (comma_split !ai_init_scopes) in + + if !ai_itv then AI_Itv.do_prog !ai_widen_delay rp; + if !ai_rel then AI_Rel.do_prog !ai_widen_delay rp; + end; if !vtest then do_test_interpret prog true else if !test then do_test_interpret prog false; diff --git a/tests/source/updown.scade b/tests/source/updown.scade index 089293a..c736dd8 100644 --- a/tests/source/updown.scade +++ b/tests/source/updown.scade @@ -4,7 +4,6 @@ node updown() returns(probe x: int) var last_x: int; let last_x = 0 -> pre x; - guarantee x_bounded: x >= -bound and x <= bound; automaton initial state UP let x = last_x + 1; tel @@ -15,6 +14,7 @@ let until if x <= -bound resume UP; returns x; + guarantee x_bounded: x >= -bound and x <= bound; tel node test(i: int) returns(a, b, c: int; exit: bool) diff --git a/tests/source/uturn.scade b/tests/source/uturn.scade new file mode 100644 index 0000000..84c9b51 --- /dev/null +++ b/tests/source/uturn.scade @@ -0,0 +1,76 @@ +-- U turn system for a subway +-- See paper HLR-lustre.tse.ps + + +node edge(X: bool) returns (EDGE: bool) +let + EDGE = X -> (X and not pre X); +tel + +node UMS(on_A, on_B, on_C, ack_AB, ack_BC: bool) + returns (grant_access, grant_exit, do_AB, do_BC: bool) +var empty_section, only_on_B: bool; +let + grant_access = empty_section and ack_AB; + grant_exit = only_on_B and ack_BC; + do_AB = (not ack_AB) and empty_section; + do_BC = (not ack_BC) and only_on_B; + empty_section = not (on_A or on_B or on_C); + only_on_B = on_B and not (on_C or on_A); +tel + +node always_from_to(B, A, C: bool) returns (X: bool) +let + X = implies(after(A), always_since(B, A) or once_since(C, A)); +tel + +node implies(A, B: bool) returns (AimpliesB: bool) +let + AimpliesB = (not A) or B; +tel + +node after(A: bool) returns (afterA: bool) +let + afterA = false -> pre(A or afterA); +tel + +node always_since(B, A: bool) returns (alwaysBsinceA: bool) +let + alwaysBsinceA = if A then B + else if after(A) then B and pre alwaysBsinceA + else true; +tel + +node once_since(C, A: bool) returns (onceCsinceA: bool) +let + onceCsinceA = if A then C + else if after(A) then C or pre onceCsinceA + else true; +tel + +node UMS_verif(on_A, on_B, on_C, ack_AB, ack_BC: bool) + returns() +var + grant_access, grant_exit: bool; + do_AB, do_BC: bool; + empty_section, only_on_B: bool; +let + empty_section = not (on_A or on_B or on_C); + only_on_B = on_B and not(on_A or on_C); + + assume h1: not(ack_AB and ack_BC); + assume h2: always_from_to(ack_AB, ack_AB, do_BC) + and always_from_to(ack_BC, ack_BC, do_AB); + assume h3: empty_section -> true; + assume h4: true -> implies(edge(not empty_section), pre grant_access); + assume h5: true -> implies(edge(on_C), pre grant_exit); + assume h6: implies(edge(not on_A), on_B); + assume h7: implies(edge(not on_B), on_A or on_C); + + grant_access, grant_exit, do_AB, do_BC = UMS(on_A, on_B, on_C, ack_AB, ack_BC); + + guarantee no_collision: implies(grant_access, empty_section); + guarantee exclusive_req: not(do_AB and do_BC); + guarantee no_derail_AB: always_from_to(ack_AB, grant_access, only_on_B); + guarantee no_derail_BC: always_from_to(ack_BC, grant_exit, empty_section); +tel |