All tests pass except one !

1 files changed, 85 insertions, 6 deletions

diff --git a/abstract/relational_apron.ml b/abstract/relational_apron.ml
index bd078cf..926d2a9 100644
--- a/abstract/relational_apron.ml
+++ b/abstract/relational_apron.ml
@@ -1,3 +1,4 @@
+open Abstract_syntax_tree
 open Apron
 open Util
 open Environment_domain
@@ -11,19 +12,86 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
     (* abstract elements *)
     type t = man Abstract1.t
 
+    (* translation in trees *)
+    let rec texpr_of_expr e =
+        match fst e with
+        | AST_identifier (id, _) -> Texpr1.Var (Var.of_string id)
+        | AST_int_const (s, _) -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_string s))
+        | AST_int_rand ((s, _), (t, _)) ->
+            Texpr1.Cst (Coeff.i_of_mpqf (Mpqf.of_string s) (Mpqf.of_string t))
+        | AST_unary(AST_UNARY_PLUS, e) ->
+            texpr_of_expr e
+        | AST_unary(AST_UNARY_MINUS, e) ->
+            (*
+            (* APRON bug ? Unary negate seems to not work correctly... *)
+            Texpr1.Unop(
+                Texpr1.Neg,
+                (texpr_of_expr e),
+                Texpr1.Int,
+                Texpr1.Zero)
+            *)
+            Texpr1.Binop(
+                Texpr1.Sub,
+                Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")),
+                (texpr_of_expr e),
+                Texpr1.Int,
+                Texpr1.Zero)
+        | AST_binary( op, e1, e2) ->
+            let f = match op with
+            | AST_PLUS -> Texpr1.Add
+            | AST_MINUS -> Texpr1.Sub
+            | AST_MULTIPLY -> Texpr1.Mul
+            | AST_DIVIDE -> Texpr1.Div
+            | AST_MODULO -> Texpr1.Mod
+            | _ -> assert false
+            in
+            Texpr1.Binop
+                (f, (texpr_of_expr e1), (texpr_of_expr e2), Texpr1.Int, Texpr1.Zero)
+        | _ -> assert false
+
     (* implementation *)
     let init = Abstract1.top manager (Environment.make  [||] [||])
     let bottom = Abstract1.bottom manager (Environment.make [||] [||])
     let is_bot = Abstract1.is_bottom manager
 
-    let addvar x id = x (* TODO *)
-    let rmvar x id = x (* TODO *)
+    let addvar x id =
+        let env = Abstract1.env x in
+        let env2 = Environment.add env [| Var.of_string id |] [||] in
+        Abstract1.change_environment manager x env2 false
+    let rmvar x id =
+        let env = Abstract1.env x in
+        let env2 = Environment.remove env [| Var.of_string id |] in
+        Abstract1.change_environment manager x env2 false
     let vars x =
         List.map Var.to_string @@
-        Array.to_list @@ snd @@ Environment.vars @@ Abstract1.env x
+        Array.to_list @@ fst @@ Environment.vars @@ Abstract1.env x
 
-    let assign x id e = x (* TODO *)
-    let compare x e1 e2 = x (* TODO *)
+    let assign x id e =
+        let expr = Texpr1.of_expr (Abstract1.env x) (texpr_of_expr e) in
+        let x' =
+            Abstract1.assign_texpr manager x
+                (Var.of_string id) expr None
+        in
+        if false then begin
+            Format.eprintf "Assign : ";
+            Abstract1.print Format.err_formatter x;
+            Format.eprintf " ; %s <- " id;
+            Texpr1.print Format.err_formatter expr;
+            Format.eprintf " ; ";
+            Abstract1.print Format.err_formatter x';
+            Format.eprintf "@.";
+        end;
+        x'
+    let compare op x e1 e2 =
+        let env = Abstract1.env x in
+        let expr = Texpr1.Binop
+            (Texpr1.Sub, texpr_of_expr e2, texpr_of_expr e1, Texpr1.Int, Texpr1.Zero) in
+        let cons = Tcons1.make (Texpr1.of_expr env expr) op in
+        let ar = Tcons1.array_make env 1 in
+        Tcons1.array_set ar 0 cons;
+        Abstract1.meet_tcons_array manager x ar
+    let compare_leq = compare Tcons1.SUPEQ
+    let compare_eq = compare Tcons1.EQ
 
     let join = Abstract1.join manager
     let meet = Abstract1.meet manager
@@ -31,7 +99,18 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
 
     let subset = Abstract1.is_leq manager
 
-    let var_str x idl = "" (* TODO *)
+    let var_str x idl = 
+        let prevars = vars x in
+        let rm_vars_l = List.filter (fun id -> not (List.mem id idl)) prevars in
+        (* print_list "prevars" prevars;
+        print_list "idl" idl;
+        print_list "rm_vars_l" rm_vars_l; *)
+        let rm_vars = Array.of_list (List.map Var.of_string rm_vars_l) in
+        let xx = Abstract1.forget_array manager x rm_vars false in
+        let b = Buffer.create 80 in
+        let s = Format.formatter_of_buffer b in
+        Abstract1.print s xx; Format.fprintf s "@?";
+        (Buffer.contents b)
 
 end