Adapt for real type with Apron ; not very efficient ATM.

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