Add support for octagons.

2 files changed, 147 insertions, 7 deletions

diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index a929c0b..58cd544 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -11,7 +11,9 @@ open Apron
   Mostly direct translation between the two.
 *)
 
-module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
+(* Polyhedra *)
+
+module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
     (* manager *)
     type man = Polka.loose Polka.t
@@ -127,9 +129,142 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
     (* Pretty-printing *)
     let print fmt x =
-        Abstract1.minimize manager x;
-        Abstract1.print fmt x;
-        Format.fprintf fmt "@?"
+        if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x;
+        Format.fprintf fmt "%a@?" Abstract1.print x
+
+    let print_vars fmt x idl = 
+        let prevars = vars x in
+        let rm_vars_l = List.filter (fun (id, _) -> not (List.mem id idl)) prevars in
+        let rm_vars = Array.of_list
+          (List.map (fun (id, _) -> Var.of_string id) rm_vars_l) in
+        let xx = Abstract1.forget_array manager x rm_vars false in
+        print fmt xx
+
+    let print_itv = Interval.print
+
+end
+
+
+(* Octagons *)
+
+module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct
+
+    (* manager *)
+    type man = Oct.t
+    let manager = Oct.manager_alloc()
+
+    type itv = Interval.t
+
+    (* abstract elements *)
+    type t = man Abstract1.t
+
+    (* direct translation of numerical expressions into Apron tree expressions *)
+    let rec texpr_of_nexpr = function
+        | 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, 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),
+                (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
+            | AST_MUL -> Texpr1.Mul
+            | AST_DIV -> Texpr1.Div
+            | AST_MOD -> Texpr1.Mod
+            in
+            Texpr1.Binop(
+                  f,
+                  (texpr_of_nexpr e1),
+                  (texpr_of_nexpr e2),
+                  (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) =
+        let op = match op with
+          | CONS_EQ -> Tcons1.EQ
+          | CONS_NE -> Tcons1.DISEQ
+          | CONS_GT -> Tcons1.SUP
+          | CONS_GE -> Tcons1.SUPEQ
+        in Tcons1.make (Texpr1.of_expr env (texpr_of_nexpr eq)) op
+
+    (* implementation *)
+    let v_env vars = 
+        let intv = List.map
+              (fun (s, _) -> Var.of_string s)
+              (List.filter (fun (_, n) -> not n) vars) in
+        let realv = List.map
+              (fun (s, _) -> Var.of_string s)
+              (List.filter (fun (_, n) -> n) vars) in
+        (Environment.make (Array.of_list intv) (Array.of_list realv))
+
+    let top vars =
+      Abstract1.top manager (v_env vars)
+    let bottom vars = Abstract1.bottom manager (v_env vars)
+    let is_bot = Abstract1.is_bottom manager
+    let is_top = Abstract1.is_top manager
+
+    let forgetvar x id =
+        let v = [| Var.of_string id |] in
+        Abstract1.forget_array manager x v false
+
+    let vars x =
+        let (ivt, fvt) = Environment.vars (Abstract1.env x) in
+        let ivl = List.map Var.to_string (Array.to_list ivt) in
+        let fvl = List.map Var.to_string (Array.to_list fvt) in
+        (List.map (fun x -> x, false) ivl) @ (List.map (fun x -> x, true) fvl)
+
+    let vbottom x =
+        Abstract1.bottom manager (Abstract1.env x)
+
+    let project x id =
+        Abstract1.bound_variable manager x (Var.of_string id)
+
+    (* Apply some formula to the environment *)
+    let apply_cl x cons =
+        let env = Abstract1.env x in
+        let tca = Array.of_list (List.map (tcons_of_cons env) cons) in
+        let ar = Tcons1.array_make env (Array.length tca) in
+        Array.iteri (Tcons1.array_set ar) tca;
+        Abstract1.meet_tcons_array manager x ar
+
+    let apply_cons x cons = apply_cl x [cons]
+
+
+    let assign x eqs =
+      let env = Abstract1.env x in
+      let vars = Array.of_list
+        (List.map (fun (id, _) -> Var.of_string id) eqs) in
+      let vals = Array.of_list
+        (List.map (fun (_, v) -> Texpr1.of_expr env (texpr_of_nexpr v)) eqs) in
+      Abstract1.assign_texpr_array manager x vars vals None
+
+    
+    (* Ensemblistic operations *)
+    let join = Abstract1.join manager
+    let meet = Abstract1.meet manager
+    let widen = Abstract1.widening manager
+
+    let subset = Abstract1.is_leq manager
+    let eq = Abstract1.is_eq manager
+
+    (* Pretty-printing *)
+    let print fmt x =
+        if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x;
+        Format.fprintf fmt "%a@?" Abstract1.print x
 
     let print_vars fmt x idl = 
         let prevars = vars x in
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index ed029da..dbc17c9 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -33,9 +33,14 @@ 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, isreal) ->
+          if isreal then not_implemented "real type for nonrelationnal domain";
+          eval env e
+        | NUnary (AST_UMINUS, e, isreal) ->
+          if isreal then not_implemented "real type for nonrelationnal domain";
+          V.neg (eval env e)
+        | NBinary (op, e1, e2, isreal) ->
+            if isreal then not_implemented "real type for nonrelationnal domain";
             let f = match op with
             | AST_PLUS -> V.add
             | AST_MINUS -> V.sub