From f97a886970bef9e1d6e8a1e217732d6ef8be087e Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Tue, 1 Jul 2014 15:42:57 +0200 Subject: Adapt for real type with Apron ; not very efficient ATM. --- abstract/abs_interp.ml | 3 +- abstract/apron_domain.ml | 20 +++++++----- abstract/formula.ml | 20 ++++++------ abstract/formula_printer.ml | 21 +++++++------ abstract/nonrelational.ml | 38 +++++++++++------------ abstract/transform.ml | 76 ++++++++++++++++++++++++++++----------------- 6 files changed, 104 insertions(+), 74 deletions(-) (limited to 'abstract') diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index a612976..a401f60 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -262,6 +262,7 @@ end = struct let cl = Formula.conslist_of_f f in let cl_g = Formula.conslist_of_f f_g in + Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; (* calculate cycle variables and forget variables *) let cycle = List.fold_left @@ -353,7 +354,7 @@ end = struct *) let cycle st cl env = let env_f = apply_cl env cl in - (* Format.printf "{{ %a ->@.%a }}@." print_dd env print_dd env_f; *) + (*Format.printf "{{ %a ->@.%a }}@." print_dd env print_dd env_f;*) dd_pass_cycle st env_f diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml index 45803fc..288f961 100644 --- a/abstract/apron_domain.ml +++ b/abstract/apron_domain.ml @@ -23,17 +23,21 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct | NIdent id -> Texpr1.Var (Var.of_string id) | NIntConst i -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_int i)) | NRealConst r -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_float r)) - | NUnary(AST_UPLUS, e) -> - texpr_of_nexpr e - | NUnary(AST_UMINUS, e) -> + | NUnary(AST_UPLUS, e, is_real) -> + Texpr1.Unop( + Texpr1.Cast, + texpr_of_nexpr e, + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) + | NUnary(AST_UMINUS, e, is_real) -> (* APRON bug ? Unary negate seems to not work correctly... *) Texpr1.Binop( Texpr1.Sub, Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")), (texpr_of_nexpr e), - Texpr1.Int, - Texpr1.Zero) - | NBinary(op, e1, e2) -> + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) + | NBinary(op, e1, e2, is_real) -> let f = match op with | AST_PLUS -> Texpr1.Add | AST_MINUS -> Texpr1.Sub @@ -45,8 +49,8 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct f, (texpr_of_nexpr e1), (texpr_of_nexpr e2), - Texpr1.Int, - Texpr1.Zero) + (if is_real then Texpr1.Real else Texpr1.Int), + Texpr1.Rnd) (* direct translation of constraints into Apron constraints *) let tcons_of_cons env (eq, op) = diff --git a/abstract/formula.ml b/abstract/formula.ml index cb7a4c4..01f6655 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -7,13 +7,15 @@ open Ast_util (* Numerical part *) +(* bool on numerical operators : is it float ? *) + type num_expr = (* constants *) | NIntConst of int | NRealConst of float (* operators *) - | NBinary of binary_op * num_expr * num_expr - | NUnary of unary_op * num_expr + | NBinary of binary_op * num_expr * num_expr * bool + | NUnary of unary_op * num_expr * bool (* identifier *) | NIdent of id @@ -40,7 +42,7 @@ type bool_expr = (* constants *) | BConst of bool (* operators from numeric values to boolean values *) - | BRel of binary_rel_op * num_expr * num_expr + | BRel of binary_rel_op * num_expr * num_expr * bool (* operators on enumerated types *) | BEnumCons of enum_cons (* boolean operators *) @@ -78,9 +80,9 @@ and eliminate_not_negate = function | BConst x -> BConst(not x) | 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) -> + | BRel(r, a, b, is_real) -> if r = AST_EQ then - BOr(BRel(AST_LT, a, b), BRel(AST_GT, a, b)) + BOr(BRel(AST_LT, a, b, is_real), BRel(AST_GT, a, b, is_real)) else let r' = match r with | AST_EQ -> AST_NE @@ -90,7 +92,7 @@ and eliminate_not_negate = function | AST_GT -> AST_LE | AST_GE -> AST_LT in - BRel(r', a, b) + BRel(r', a, b, is_real) | BAnd(a, b) -> BOr(eliminate_not_negate a, eliminate_not_negate b) | BOr(a, b) -> @@ -112,7 +114,7 @@ and conslist_bool_expr = let rec conslist_of_f = function | BNot e -> conslist_of_f (eliminate_not_negate e) - | BRel (op, a, b) -> + | BRel (op, a, b, is_real) -> let x, y, op = match op with | AST_EQ -> a, b, CONS_EQ | AST_NE -> a, b, CONS_NE @@ -121,9 +123,9 @@ let rec conslist_of_f = function | AST_LT -> b, a, CONS_GT | AST_LE -> b, a, CONS_GE in - let cons = if y = NIntConst 0 + let cons = if y = NIntConst 0 || y = NRealConst 0. then (x, op) - else (NBinary(AST_MINUS, x, y), op) + else (NBinary(AST_MINUS, x, y, is_real), op) in [], [cons], CLTrue | BConst x -> [], [], if x then CLTrue else CLFalse diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml index 383500c..9c6c403 100644 --- a/abstract/formula_printer.ml +++ b/abstract/formula_printer.ml @@ -12,12 +12,12 @@ let string_of_binary_rel = function | AST_GE -> "≥" let ne_prec = function - | NUnary(op, _) -> unary_precedence - | NBinary(op, _, _) -> binary_op_precedence op + | NUnary _ -> unary_precedence + | NBinary(op, _, _, _) -> binary_op_precedence op | _ -> 100 let be_prec = function - | BRel(op, _, _) -> binary_rel_precedence op + | BRel(op, _, _, _) -> binary_rel_precedence op | BAnd _ -> binary_bool_precedence AST_AND | BOr _ -> binary_bool_precedence AST_OR | BNot _ -> unary_precedence @@ -49,12 +49,14 @@ let rec print_num_expr fmt e = match e with | NRealConst f -> Format.fprintf fmt "%f" f | NIdent id -> print_id fmt id - | NBinary(op, a, b) -> + | NBinary(op, a, b, is_real) -> print_ch fmt print_num_expr ne_prec a ne_prec e; - Format.fprintf fmt "@ %s " (string_of_binary_op op); + Format.fprintf fmt "@ %s%s " (string_of_binary_op op) + (if is_real then "." else ""); print_ah fmt print_num_expr ne_prec b ne_prec e - | NUnary(op, a) -> - Format.fprintf fmt "%s " (string_of_unary_op op); + | NUnary(op, a, is_real) -> + Format.fprintf fmt "%s%s " (string_of_unary_op op) + (if is_real then "." else ""); print_ah fmt print_num_expr ne_prec a ne_prec e (* Enumeated expressions *) @@ -75,9 +77,10 @@ let print_econs fmt (op, a, b) = let rec print_bool_expr fmt e = match e with | BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false") | BEnumCons c -> print_econs fmt c - | BRel(op, a, b) -> + | BRel(op, a, b, is_real) -> print_ch fmt print_num_expr ne_prec a be_prec e; - Format.fprintf fmt "@ %s " (string_of_binary_rel op); + Format.fprintf fmt "@ %s%s " (string_of_binary_rel op) + (if is_real then "." else ""); print_ch fmt print_num_expr ne_prec b be_prec e | BAnd (a, b) -> diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 7a83303..efa30dd 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -31,9 +31,9 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | NIdent id -> get_var env id | NIntConst i -> V.const i | NRealConst f -> V.const (int_of_float f) (* TODO floats *) - | NUnary (AST_UPLUS, e) -> eval env e - | NUnary (AST_UMINUS, e) -> V.neg (eval env e) - | NBinary (op, e1, e2) -> + | NUnary (AST_UPLUS, e, _) -> eval env e + | NUnary (AST_UMINUS, e, _) -> V.neg (eval env e) + | NBinary (op, e1, e2, _) -> let f = match op with | AST_PLUS -> V.add | AST_MINUS -> V.sub @@ -128,22 +128,22 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct match lhs with | NIdent i -> [i, op, rhs] | NIntConst _ | NRealConst _ -> [] - | NUnary(AST_UPLUS, x) -> extract_var (x, op, rhs) - | NUnary(AST_UMINUS, x) -> - extract_var (x, inv_op op, NUnary(AST_UMINUS, x)) - | NBinary(AST_PLUS, a, b) -> - extract_var (a, op, NBinary(AST_MINUS, rhs, b)) @ - extract_var (b, op, NBinary(AST_MINUS, rhs, a)) - | NBinary(AST_MINUS, a, b) -> - extract_var (a, op, NBinary(AST_PLUS, rhs, b)) @ - extract_var (b, inv_op op, NBinary(AST_MINUS, a, rhs)) - | NBinary(AST_MUL, a, b) -> - extract_var (a, op, NBinary(AST_DIV, rhs, b)) @ - extract_var (b, op, NBinary(AST_DIV, rhs, a)) - | NBinary(AST_DIV, a, b) -> - extract_var (a, op, NBinary(AST_MUL, rhs, b)) @ - extract_var (b, inv_op op, NBinary(AST_DIV, a, rhs)) - | NBinary(AST_MOD, _, _) -> [] + | NUnary(AST_UPLUS, x, r) -> extract_var (x, op, rhs) + | NUnary(AST_UMINUS, x, r) -> + extract_var (x, inv_op op, NUnary(AST_UMINUS, x, r)) + | NBinary(AST_PLUS, a, b, r) -> + extract_var (a, op, NBinary(AST_MINUS, rhs, b, r)) @ + extract_var (b, op, NBinary(AST_MINUS, rhs, a, r)) + | NBinary(AST_MINUS, a, b, r) -> + extract_var (a, op, NBinary(AST_PLUS, rhs, b, r)) @ + extract_var (b, inv_op op, NBinary(AST_MINUS, a, rhs, r)) + | NBinary(AST_MUL, a, b, r) when r -> + extract_var (a, op, NBinary(AST_DIV, rhs, b, r)) @ + extract_var (b, op, NBinary(AST_DIV, rhs, a, r)) + | NBinary(AST_DIV, a, b, r) when r -> + extract_var (a, op, NBinary(AST_MUL, rhs, b, r)) @ + extract_var (b, inv_op op, NBinary(AST_DIV, a, rhs, r)) + | NBinary _ -> [] in let zop = match sign with | CONS_EQ -> AST_EQ | CONS_NE -> AST_NE diff --git a/abstract/transform.ml b/abstract/transform.ml index d9b20d8..ff2374e 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -21,7 +21,7 @@ type transform_data = { (* Numerical types / Enumerated types *) type ne_expr = | EE of enum_expr - | NE of num_expr + | NE of num_expr * bool (* bool: true -> real, false -> int *) (* f_of_neexpr : transform_data -> (string, string) -> (ne_expr list -> bool_expr) -> expr -> bool_expr @@ -34,31 +34,38 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = | AST_identifier(id, _) -> let qid = node^"/"^id in begin match type_var td.rp node id with - | TInt | TReal -> where [NE (NIdent qid)] + | TInt -> where [NE (NIdent qid, false)] + | TReal -> where [NE (NIdent qid, true)] | TEnum _ -> where [EE (EIdent qid)] end | AST_idconst(id, _) -> begin let x = VarMap.find ("cst/"^id) td.consts in - try where [NE (NIntConst (I.as_int x))] - with _ -> try where [NE (NRealConst (I.as_real x))] + try where [NE (NIntConst (I.as_int x), false)] + with _ -> try where [NE (NRealConst (I.as_real x), true)] 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 [NE(NIntConst(int_of_string i))] - | AST_real_const(r, _) -> where [NE(NRealConst(float_of_string r))] + | AST_int_const(i, _) -> where [NE(NIntConst(int_of_string i), false)] + | AST_real_const(r, _) -> where [NE(NRealConst(float_of_string r), true)] | AST_bool_const b -> where [EE(EItem (if b then bool_true else bool_false))] | AST_unary(op, e) -> sub (function - | [NE x] -> where [NE(NUnary(op, x))] + | [NE (x, r)] -> where [NE(NUnary(op, x, r), r)] | _ -> le invalid_arity "Unary operator") e | AST_binary(op, a, b) -> sub (function - | [NE x] -> - sub (function - | [NE y] -> where [NE(NBinary(op, x, y))] - | _ -> le invalid_arity "binary operator") b - | _ -> le invalid_arity "binary operator") a + | [NE (x, r1); NE (y, r2)] -> + let r = r1 || r2 in + where [NE(NBinary(op, x, y, r), r)] + | _ -> le invalid_arity "binary operator") + (AST_tuple([a; b]), snd expr) + | AST_cast(e, ty) -> + let is_real = (ty = AST_TREAL) in + sub (function + | [NE (x, _)] -> where [NE(NUnary(AST_UPLUS, x, is_real), is_real)] + | _ -> le invalid_arity "Cast.") + e (* temporal *) | AST_pre(expr, id) -> let id = node^"/"^id in @@ -67,7 +74,8 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = (List.mapi (fun i t -> let x = id^"."^(string_of_int i) in match t with - | TInt | TReal -> NE(NIdent x) + | TInt -> NE(NIdent x, false) + | TReal -> NE(NIdent x, true) | TEnum _ -> EE(EIdent x)) typ) | AST_arrow(a, b) -> @@ -81,9 +89,9 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = else if not (td.rp.no_time_scope clock_scope) then f_or - (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0)) + (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false)) (sub where a)) - (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1)) + (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false)) (sub where b)) else f_or (sub where a) (sub where b) @@ -98,7 +106,8 @@ let rec f_of_neexpr td (node, prefix, clock_scope) where expr = (List.map (fun (_, id, t) -> let x = node^"/"^nid^"/"^id in match t with - | AST_TINT | AST_TREAL -> NE(NIdent x) + | AST_TINT -> NE(NIdent x, false) + | AST_TREAL -> NE(NIdent x, true) | _ -> EE(EIdent x)) n.ret) | AST_tuple l -> @@ -135,7 +144,7 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr = where (f_of_neexpr td (node, prefix, clock_scope) (function - | [NE x; NE y] -> BRel(rel, x, y) + | [NE (x, r1); NE (y, r2)] -> BRel(rel, x, y, r1 || r2) | [EE x; EE y] -> let eop = match rel with | AST_EQ -> E_EQ @@ -156,9 +165,9 @@ and f_of_bexpr td (node, prefix, clock_scope) where expr = else if not (td.rp.no_time_scope clock_scope) then f_or - (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0)) + (f_and (BRel(AST_EQ, NIdent(clock_scope^"time"), NIntConst 0, false)) (sub where a)) - (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1)) + (f_and (BRel(AST_GE, NIdent(clock_scope^"time"), NIntConst 1, false)) (sub where b)) else f_or (sub where a) (sub where b) @@ -192,7 +201,8 @@ let gen_clock td (node, prefix, _) active = f_and (if not (td.rp.no_time_scope clock_scope) then BRel(AST_EQ, NIdent("N"^clock_scope^"time"), - NBinary(AST_PLUS, NIntConst 1, NIdent(clock_scope^"time"))) + NBinary(AST_PLUS, NIntConst 1, NIdent(clock_scope^"time"), false), + false) else BConst true) (if td.rp.init_scope clock_scope then f_e_eq (EIdent("N"^clock_scope^"init")) (EItem bool_false) @@ -202,7 +212,7 @@ let gen_clock td (node, prefix, _) active = (if not (td.rp.no_time_scope clock_scope) then BRel(AST_EQ, NIdent("N"^clock_scope^"time"), - NIdent(clock_scope^"time")) + NIdent(clock_scope^"time"), false) else BConst true) (if td.rp.init_scope clock_scope then f_e_eq (EIdent("N"^clock_scope^"init")) @@ -216,9 +226,13 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees = let instance_eq (_, id, eqs, args) = let eq = f_of_scope active td (node^"/"^id, "", eqs) clock_scope assume_guarantees in if active then - let arg_eq ((_,argname,_), expr) = + let arg_eq ((_,argname,ty), expr) = f_of_neexpr td (node, prefix, clock_scope) (function - | [NE v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v) + | [NE (v, r)] -> + let need_r = (ty = AST_TREAL) in + if r <> need_r then error "Invalid type for numerical argument."; + BRel(AST_EQ, + NIdent(node^"/"^id^"/"^argname), v, r) | [EE v] -> f_e_eq (EIdent(node^"/"^id^"/"^argname)) v | _ -> invalid_arity "in argument") expr @@ -236,7 +250,7 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees = (List.mapi (fun i v -> let x = ("N"^id^"."^(string_of_int i)) in match v with - | NE v -> BRel(AST_EQ, NIdent x, v) + | NE (v, r) -> BRel(AST_EQ, NIdent x, v, r) | EE v -> f_e_eq (EIdent x) v) elist)) expr @@ -246,7 +260,8 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees = (List.mapi (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)) + | TInt -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), false) + | TReal -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x), true) | TEnum _ -> f_e_eq (EIdent("N"^id^"."^x)) (EIdent (id^"."^x))) typ) in @@ -260,8 +275,13 @@ let rec f_of_scope active td (node, prefix, eqs) clock_scope assume_guarantees = if active then let apply_f vs = let rels = - List.map2 (fun (id, _) -> function - | NE v -> BRel(AST_EQ, NIdent (node^"/"^id), v) + List.map2 (fun (id, _) -> + let need_r = (type_var td.rp node id = TReal) in + function + | NE (v, r) -> + if r <> need_r then error "Invalid type in numerical assign"; + BRel(AST_EQ, NIdent (node^"/"^id), + v, r) | EE v -> f_e_eq (EIdent (node^"/"^id)) v) ids vs in @@ -380,7 +400,7 @@ let gen_clock_init rp (node, prefix, _) = then BRel(AST_EQ, NIdent(clock_scope^"time"), - NIntConst 0) + NIntConst 0, false) else BConst true) (if rp.init_scope clock_scope then -- cgit v1.2.3