summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp.ml3
-rw-r--r--abstract/apron_domain.ml20
-rw-r--r--abstract/formula.ml20
-rw-r--r--abstract/formula_printer.ml21
-rw-r--r--abstract/nonrelational.ml38
-rw-r--r--abstract/transform.ml76
6 files changed, 104 insertions, 74 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-09 16:11:09 +0000