diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_domain.ml | 21 | ||||
| -rw-r--r-- | abstract/abs_interp.ml | 7 | ||||
| -rw-r--r-- | abstract/formula.ml | 64 | ||||
| -rw-r--r-- | abstract/formula_printer.ml | 39 | ||||
| -rw-r--r-- | abstract/transform.ml | 162 |
5 files changed, 187 insertions, 106 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml index ddc34ab..a7f5455 100644 --- a/abstract/abs_domain.ml +++ b/abstract/abs_domain.ml @@ -2,6 +2,7 @@ open Ast open Formula open Num_domain open Typing +open Util module type ENVIRONMENT_DOMAIN = sig type t @@ -43,6 +44,14 @@ end module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct + type enum_valuation = (string * string) list + + module VMapKey = struct + type t = enum_valuation VarMap.t + let compare = VarMap.compare (fun a b -> Pervasives.compare (List.sort Pervasives.compare a) (List.sort Pervasives.compare b)) + end + module VMap = Mapext.Make(VMapKey) + type t = ND.t type itv = ND.itv @@ -65,16 +74,16 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct let subset = ND.subset let eq = ND.eq - let rec apply_cl x (cons, rest) = match rest with + let rec apply_cl x (econs, cons, rest) = match rest with | CLTrue -> ND.apply_ncl x cons | CLFalse -> vbottom x | CLAnd(a, b) -> - let y = apply_cl x (cons, a) in - apply_cl y (cons, b) - | CLOr((ca, ra), (cb, rb)) -> - let y = apply_cl x (cons@ca, ra) in - let z = apply_cl x (cons@cb, rb) in + let y = apply_cl x (econs, cons, a) in + apply_cl y (econs, cons, b) + | CLOr((eca, ca, ra), (ecb, cb, rb)) -> + let y = apply_cl x (econs@eca, cons@ca, ra) in + let z = apply_cl x (econs@ecb, cons@cb, rb) in join y z let apply_f x f = apply_cl x (conslist_of_f f) diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 1d3e20a..7950144 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -27,14 +27,10 @@ end = struct } - - (* init state *) let init_state widen_delay rp = let f = Formula.eliminate_not (Transform.f_of_prog rp false) in - let cl = Formula.conslist_of_f f in let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in - let cl_g = Formula.conslist_of_f f_g in let env = List.fold_left (fun env (_, id, ty) -> E.addvar env id ty) @@ -58,6 +54,9 @@ end = struct let env = E.apply_f env init_f in + let cl = Formula.conslist_of_f f in + let cl_g = Formula.conslist_of_f f_g in + { rp; widen_delay; f; cl; f_g; cl_g; guarantees; env } diff --git a/abstract/formula.ml b/abstract/formula.ml index a598750..ce83935 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -1,4 +1,6 @@ open Ast +open Util +open Ast_util (* AST for logical formulas *) @@ -23,12 +25,24 @@ type num_cons = num_expr * num_cons_op (* always imply right member = 0 *) (* Logical part *) + +(* Enumerated types *) +type enum_expr = + | EIdent of id + | EItem of string + +type enum_op = + | E_EQ | E_NE + +type enum_cons = enum_op * enum_expr * enum_expr + 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 + (* operators on enumerated types *) + | BEnumCons of enum_cons (* boolean operators *) | BAnd of bool_expr * bool_expr | BOr of bool_expr * bool_expr @@ -46,6 +60,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) + (* Write all formula without using the NOT operator *) @@ -56,7 +74,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) + | BEnumCons(op, a, b) -> BEnumCons((if op = E_EQ then E_NE else E_EQ), a, b) | BNot e -> eliminate_not e | BRel(r, a, b) -> if r = AST_EQ then @@ -83,7 +101,7 @@ and eliminate_not_negate = function We also use this step to simplify trues and falses that may be present. *) -type conslist = num_cons list * conslist_bool_expr +type conslist = enum_cons list * num_cons list * conslist_bool_expr and conslist_bool_expr = | CLTrue | CLFalse @@ -104,32 +122,30 @@ let rec conslist_of_f = function let cons = if y = NIntConst 0 then (x, op) else (NBinary(AST_MINUS, x, y), op) - in [cons], CLTrue + 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 + [], [], if x then CLTrue else CLFalse + | BEnumCons e -> + [e], [], CLTrue | BOr(a, b) -> - let ca, ra = conslist_of_f a in - let cb, rb = conslist_of_f b in - begin match ca, ra, cb, rb with - | _, CLFalse, _, _ -> cb, rb - | _, _, _, CLFalse -> ca, ra - | [], CLTrue, _, _ -> [], CLTrue - | _, _, [], CLTrue -> [], CLTrue - | _ -> [], CLOr((ca, ra), (cb, rb)) + let eca, ca, ra = conslist_of_f a in + let ecb, cb, rb = conslist_of_f b in + begin match eca, ca, ra, ecb, cb, rb with + | _, _, CLFalse, _, _, _ -> ecb, cb, rb + | _, _, _, _, _, CLFalse -> eca, ca, ra + | [], [], CLTrue, _, _, _ -> [], [], CLTrue + | _, _, _, [], [], CLTrue -> [], [], CLTrue + | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb)) end | BAnd(a, b) -> - let ca, ra = conslist_of_f a in - let cb, rb = conslist_of_f b in + let eca, ca, ra = conslist_of_f a in + let ecb, cb, rb = conslist_of_f b in let cons = ca @ cb in + let econs = eca @ ecb in begin match ra, rb with - | CLFalse, _ | _, CLFalse -> [], CLFalse - | CLTrue, _ -> cons, rb - | ra, CLTrue -> cons, ra - | _, _ -> cons, CLAnd(ra, rb) + | CLFalse, _ | _, CLFalse -> [], [], CLFalse + | CLTrue, _ -> econs, cons, rb + | _, CLTrue -> econs, cons, ra + | _, _ -> econs, cons, CLAnd(ra, rb) end diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml index 1b31ba1..44f2d39 100644 --- a/abstract/formula_printer.ml +++ b/abstract/formula_printer.ml @@ -1,3 +1,4 @@ +open Util open Ast open Formula open Ast_printer @@ -56,15 +57,24 @@ let rec print_num_expr fmt e = match e with Format.fprintf fmt "%s " (string_of_unary_op op); print_ah fmt print_num_expr ne_prec a ne_prec e +(* Enumeated expressions *) +let print_enum_expr fmt = function + | EIdent id -> Format.fprintf fmt "%s" id + | EItem x -> Format.fprintf fmt "%s" x + +let str_of_enum_op = function + | E_EQ -> "≡" + | E_NE -> "≢" + +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 boolean form of formula *) 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 + | BEnumCons c -> print_econs fmt c | 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); @@ -112,26 +122,33 @@ let print_cons fmt (eq, sg) = Format.fprintf fmt "@[<hv 2>%a %a 0@]" print_num_expr eq print_cons_sg sg -let rec print_conslist fmt (cons, e) = +let rec print_conslist fmt (econs, cons, e) = + let c = + (List.map (fun x -> Left x) econs) @ (List.map (fun y -> Right y) cons) + in + let f fmt = function + | Left x -> Format.fprintf fmt "@[<hv 2>%a@]" print_econs x + | Right x -> Format.fprintf fmt "@[<hv 2>%a@]" print_cons x + in let rec aux = function | [] -> false | [a] -> - Format.fprintf fmt "@[<hv 2>%a@]" print_cons a; true + f fmt a; true | p::q -> - Format.fprintf fmt "@[<hv 2>%a@]" print_cons p; + f fmt p; Format.fprintf fmt "@ ∧ "; aux q in match e with | CLTrue -> Format.fprintf fmt "@[<hv 2>("; - ignore (aux cons); + ignore (aux c); Format.fprintf fmt ")@]" | CLFalse -> Format.fprintf fmt "false" | _ -> Format.fprintf fmt "@[<hv 2>("; - if aux cons then Format.fprintf fmt "@ ∧ "; + if aux c then Format.fprintf fmt "@ ∧ "; print_conslist_expr fmt e; Format.fprintf fmt ")@]" @@ -140,7 +157,7 @@ and print_conslist_expr fmt = function | CLFalse -> Format.fprintf fmt "false" | CLOr(a, b) -> Format.fprintf fmt "@[<hv 2>(%a@ ∨ %a)@]" - print_conslist a + print_conslist a print_conslist b | CLAnd(a, b) -> Format.fprintf fmt "%a@ ∧ %a" diff --git a/abstract/transform.ml b/abstract/transform.ml index 890f598..708456e 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -18,38 +18,57 @@ type transform_data = { (* future : the automata state *) } -(* f_of_nexpr : - transform_data -> (string, string) -> (num_expr list -> 'a) -> expr -> 'a +(* Numerical types / Enumerated types *) +type ne_expr = + | EE of enum_expr + | NE of num_expr + +(* f_of_neexpr : + transform_data -> (string, string) -> (ne_expr list -> bool_expr) -> expr -> bool_expr *) -let rec f_of_nexpr td (node, prefix) where expr = - let sub = f_of_nexpr td (node, prefix) in +let rec f_of_neexpr td (node, prefix) where expr = + let sub = f_of_neexpr td (node, prefix) in + let le = loc_error (snd expr) in match fst expr with (* ident *) - | AST_identifier(id, _) -> where [NIdent (node^"/"^id)] + | AST_identifier(id, _) -> + let qid = node^"/"^id in + begin match type_var td.rp node id with + | TInt | TReal -> where [NE (NIdent qid)] + | TEnum _ -> where [EE (EIdent qid)] + end | AST_idconst(id, _) -> begin let x = VarMap.find ("cst/"^id) td.consts in - try where [NIntConst (I.as_int x)] - with _ -> try where [NRealConst (I.as_real x)] - with _ -> error "Invalid data for supposedly numerical constant." + try where [NE (NIntConst (I.as_int x))] + with _ -> try where [NE (NRealConst (I.as_real x))] + with _ -> try where [EE (EItem (if I.as_bool x then bool_true else bool_false))] + with _ -> le error "Invalid data for supposedly numerical/boolean constant." end (* numerical *) - | AST_int_const(i, _) -> where [NIntConst(int_of_string i)] - | AST_real_const(r, _) -> where [NRealConst(float_of_string r)] + | AST_int_const(i, _) -> where [NE(NIntConst(int_of_string i))] + | AST_real_const(r, _) -> where [NE(NRealConst(float_of_string r))] + | AST_bool_const b -> where [EE(EItem (if b then bool_true else bool_false))] | AST_unary(op, e) -> sub (function - | [x] -> where [NUnary(op, x)] - | _ -> invalid_arity "Unary operator") e + | [NE x] -> where [NE(NUnary(op, x))] + | _ -> le invalid_arity "Unary operator") e | AST_binary(op, a, b) -> sub (function - | [x] -> + | [NE x] -> sub (function - | [y] -> where [NBinary(op, x, y)] - | _ -> invalid_arity "binary_operator") b - | _ -> invalid_arity "binary operator") a + | [NE y] -> where [NE(NBinary(op, x, y))] + | _ -> le invalid_arity "binary operator") b + | _ -> le invalid_arity "binary operator") a (* temporal *) | AST_pre(expr, id) -> let typ = type_expr td.rp node expr in - where (List.mapi (fun i _ -> NIdent (id^"."^(string_of_int i))) typ) + where + (List.mapi + (fun i t -> let x = id^"."^(string_of_int i) in + match t with + | TInt | TReal -> NE(NIdent x) + | TEnum _ -> EE(EIdent x)) + typ) | AST_arrow(a, b) -> f_or (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0)) @@ -63,20 +82,34 @@ let rec f_of_nexpr td (node, prefix) where expr = (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b)) | AST_instance ((f, _), args, nid) -> let (n, _) = find_node_decl td.rp.p f in - where (List.map (fun (_, id, _) -> NIdent (node^"/"^nid^"/"^id)) n.ret) - - (* boolean values treated as integers *) - | _ -> + where + (List.map + (fun (_, id, t) -> let x = node^"/"^nid^"/"^id in + match t with + | AST_TINT | AST_TREAL -> NE(NIdent x) + | _ -> EE(EIdent x)) + n.ret) + | AST_tuple l -> + let rec rl l x = match l with + | [] -> where x + | p::q -> + sub (fun y -> rl q (x@y)) p + in rl l [] + (* boolean values treated as enumerated types *) + | _ when type_expr td.rp node expr = [bool_type] -> 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_and (f_of_expr td (node, prefix) expr) (where [EE (EItem bool_true)])) + (f_and (f_of_expr td (node, prefix) (AST_not(expr), snd expr)) + (where [EE (EItem bool_false)])) + | _ -> le type_error "Expected numerical/enumerated value" + (* f_of_expr : transform_data -> (string, string) -> expr -> bool_expr f_of_bexpr : - transform_data -> (string, string) -> (bool_expr -> 'a) -> expr -> 'a + transform_data -> (string, string) -> (bool_expr -> bool_expr) -> expr -> bool_expr *) and f_of_bexpr td (node, prefix) where expr = let sub = f_of_bexpr td (node, prefix) in @@ -87,37 +120,35 @@ and f_of_bexpr td (node, prefix) where expr = | AST_not(a) -> BNot(sub where a) | AST_binary_rel(rel, a, b) -> where - (f_of_nexpr td (node, prefix) + (f_of_neexpr 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))) + | [NE x; NE y] -> BRel(rel, x, y) + | [EE x; EE y] -> + let eop = match rel with + | AST_EQ -> E_EQ + | AST_NE -> E_NE + | _ -> type_error "Invalid operator on enumerated values." + in BEnumCons(eop, x, y) + | _ -> invalid_arity "Binary operator") + (AST_tuple [a; b], snd expr)) + (* Temporal *) | 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." + (* Enumerations... *) + | _ when type_expr td.rp node expr = [bool_type] -> + let ff = function + | [EE x] -> + f_or + (f_and (f_e_eq x (EItem bool_true)) (where (BConst true))) + (f_and (f_e_eq x (EItem bool_false)) (where (BConst false))) + | _ -> assert false + in + f_of_neexpr td (node, prefix) ff expr + | _ -> type_error "Expected boolean value." and f_of_expr td (node, prefix) expr = f_of_bexpr td (node, prefix) (fun x -> x) expr @@ -132,8 +163,9 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = 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 - | [v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v) + let eq_arg = f_of_neexpr td (node, prefix) (function + | [NE v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v) + | [EE v] -> f_e_eq (EIdent(node^"/"^id^"/"^argname)) v | _ -> invalid_arity "in argument") expr in f_and eq eq_arg) @@ -146,17 +178,23 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = in let pre_expr (id, expr) = if active then - f_of_nexpr td (node, prefix) (fun elist -> + f_of_neexpr td (node, prefix) (fun elist -> list_fold_op f_and (List.mapi - (fun i v -> BRel(AST_EQ, NIdent("N"^id^"."^(string_of_int i)), v)) + (fun i v -> let x = ("N"^id^"."^(string_of_int i)) in + match v with + | NE v -> BRel(AST_EQ, NIdent x, v) + | EE v -> f_e_eq (EIdent x) v) elist)) expr else let typ = type_expr td.rp node expr in list_fold_op f_and (List.mapi - (fun i _ -> let x = string_of_int i in BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x))) + (fun i t -> let x = string_of_int i in + match t with + | TInt | TReal -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x)) + | TEnum _ -> f_e_eq (EIdent("N"^id^"."^x)) (EIdent (id^"."^x))) typ) in List.fold_left (fun x i -> f_and (pre_expr i) x) @@ -166,14 +204,16 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees = | AST_assign(ids, e) -> let assign_eq = if active then - f_of_nexpr td (node, prefix) - (fun vs -> - let rels = - List.map2 (fun (id, _) v -> BRel(AST_EQ, NIdent (node^"/"^id), v)) - ids vs - in - list_fold_op f_and rels) - e + f_of_neexpr td (node, prefix) + (fun vs -> + let rels = + List.map2 (fun (id, _) -> function + | NE v -> BRel(AST_EQ, NIdent (node^"/"^id), v) + | EE v -> f_e_eq (EIdent (node^"/"^id)) v) + ids vs + in + list_fold_op f_and rels) + e else BConst true in |