Add bindings to apron. Next : work on abstract interpret.

9 files changed, 242 insertions, 59 deletions

diff --git a/Makefile b/Makefile
index 69bf0ce..2b6f7c6 100644
--- a/Makefile
+++ b/Makefile
@@ -11,9 +11,11 @@ SRC= 	main.ml \
 		abstract/formula.ml \
 		abstract/formula_printer.ml \
 		abstract/transform.ml \
-		interpret/bad_interpret.ml \
-		interpret/interface.ml \
+		abstract/environment_domain.ml \
+		abstract/apron_domain.ml \
+		abstract/abs_interp.ml \
 		interpret/interpret.ml \
+		interpret/ast_util.ml \
 		interpret/rename.ml
 
 all: $(BIN)
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
new file mode 100644
index 0000000..403e3e8
--- /dev/null
+++ b/abstract/abs_interp.ml
@@ -0,0 +1,14 @@
+open Ast
+open Formula
+
+open Util
+open Environment_domain
+
+module I (E : ENVIRONMENT_DOMAIN) : sig
+
+  val init_state  : prog -> id -> E.t
+  val do_step     : prog -> id -> E.t -> E.t
+
+end = struct
+
+end
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
new file mode 100644
index 0000000..1cc418e
--- /dev/null
+++ b/abstract/apron_domain.ml
@@ -0,0 +1,132 @@
+open Formula
+open Ast
+
+open Util
+open Environment_domain
+
+open Apron
+
+module D : ENVIRONMENT_DOMAIN = struct
+
+    (* manager *)
+    type man = Polka.loose Polka.t
+    let manager = Polka.manager_alloc_loose ()
+
+    (* abstract elements *)
+    type t = man Abstract1.t
+
+    (* direct translation of numerical expressions into Apron tree expressions *)
+    (* TODO : some variables have type real and not int... *)
+    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) ->
+            texpr_of_nexpr e
+        | NUnary(AST_UMINUS, e) ->
+            (* 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) ->
+            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),
+                  Texpr1.Int,
+                  Texpr1.Zero)
+    
+    (* 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 init = Abstract1.top manager (Environment.make  [||] [||])
+    let bottom = Abstract1.bottom manager (Environment.make [||] [||])
+    let is_bot = Abstract1.is_bottom manager
+
+    let addvar x id isfloat =
+        let env = Abstract1.env x in
+        let env2 = if isfloat then
+            Environment.add env [||] [| Var.of_string id |]
+          else
+            Environment.add env [| Var.of_string id |] [||]
+        in
+        Abstract1.change_environment manager x env2 false
+    let rmvar x id =
+        let v = [| Var.of_string id |] in
+        let env = Abstract1.env x in
+        let env2 = Environment.remove env v in
+        let y = Abstract1.forget_array manager x v false in
+        Abstract1.change_environment manager y env2 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)
+
+    (* Apply some formula to the environment *)
+    let rec apply_cl x (cons, rest) =
+        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;
+        let y = Abstract1.meet_tcons_array manager x ar in
+        apply_cl_r y rest
+
+    and apply_cl_r x = function
+        | CLTrue -> x
+        | CLFalse -> vbottom x
+        | CLAnd(a, b) ->
+          let y = apply_cl_r x a in
+          apply_cl_r y b
+        | CLOr(a, b) ->
+          let y = apply_cl x a in
+          let z = apply_cl x b in
+          Abstract1.join manager y z
+
+    let apply_f x f = apply_cl x (conslist_of_f f)
+
+    
+    (* 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_all fmt x =
+        Abstract1.print fmt x;
+        Format.fprintf fmt "@?"
+
+    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_all fmt xx
+
+end
+
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
new file mode 100644
index 0000000..5664474
--- /dev/null
+++ b/abstract/environment_domain.ml
@@ -0,0 +1,36 @@
+open Ast
+open Formula
+
+module type ENVIRONMENT_DOMAIN = sig
+    type t
+
+    (* construction *)
+    val init        : t
+    val bottom      : t
+    val is_bot      : t -> bool
+
+    (* variable management *)
+    val addvar      : t -> id -> bool -> t     (* integer or float variable ? *)
+    val rmvar       : t -> id -> t
+    val vars        : t -> (id * bool) list
+    val vbottom     : t -> t       (* bottom value with same environment *)
+
+    (* abstract operation *)
+    val apply_f     : t -> bool_expr -> t
+    val apply_cl    : t -> conslist -> t
+
+    (* set-theoretic operations *)
+    val join        : t -> t -> t       (* union *)
+    val meet        : t -> t -> t       (* intersection *)
+    val widen       : t -> t -> t
+
+    (* order *)
+    val subset      : t -> t -> bool
+    val eq          : t -> t -> bool
+
+    (* pretty-printing *)
+    val print_vars  : Format.formatter -> t -> id list -> unit
+    val print_all   : Format.formatter -> t -> unit
+end
+
+
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 56d54ce..e6886b8 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -191,10 +191,8 @@ and f_of_scope active td (node, prefix, eqs) =
     (List.map do_eq eqs)
 
 and f_of_prog p root =
-    let (n, _) = find_node_decl p root in
-    let root_scope = ("", "", n.body) in
     let td = {
-      root_scope = root_scope;
+      root_scope = get_root_scope p root;
       p = p;
       consts = I.consts p root;
     } in
diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml
index 80411d8..f5a1978 100644
--- a/interpret/ast_util.ml
+++ b/interpret/ast_util.ml
@@ -27,6 +27,17 @@ let extract_const_decls =
     []
 
 
+(* Utility : scopes *)
+
+
+(* path to node * subscope prefix in node * equations in scope *)
+type scope = id * id * eqn ext list
+
+let get_root_scope p root =
+    let (n, _) = find_node_decl p root in
+    ("", "", n.body)
+
+
 (* Utility : find instances declared in an expression *)
 
 (* extract_instances :
diff --git a/interpret/interface.ml b/interpret/interface.ml
deleted file mode 100644
index 621bfa2..0000000
--- a/interpret/interface.ml
+++ /dev/null
@@ -1,46 +0,0 @@
-open Ast
-open Util
-
-
-module type INTERPRET = sig
-
-
-  exception Bad_datatype
-  type value
-
-  val int_value : int -> value
-  val bool_value : bool -> value
-  val real_value : float -> value
-
-  val as_int : value -> int
-  val as_bool : value -> bool
-  val as_real : value -> float
-
-  val str_repr_of_val : value -> string
-
-  type state
-
-  val print_state : Format.formatter -> state -> unit
-
-  type io = (id * value) list
-
-  (*
-    Get the constants only
-  *)
-  val consts : prog -> id -> value VarMap.t
-
-  (*
-    Construct initial state for a program.
-    The id is the root node of the program evaluation.
-  *)
-  val init_state : prog -> id -> state
-
-  (*
-    Run a step of the program (not necessary to specify the program,
-      it should be encoded in the state).
-    State -> Inputs -> Next state, Outputs
-  *)
-  val step : state -> io -> (state * io)
-
-end
-
diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index 24903f1..f28bce0 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -1,9 +1,47 @@
 open Ast
 open Util
 open Ast_util
-open Interface
 
-module I : INTERPRET = struct
+module I : sig
+
+  exception Bad_datatype
+  type value
+
+  val int_value : int -> value
+  val bool_value : bool -> value
+  val real_value : float -> value
+
+  val as_int : value -> int
+  val as_bool : value -> bool
+  val as_real : value -> float
+
+  val str_repr_of_val : value -> string
+
+  type state
+
+  val print_state : Format.formatter -> state -> unit
+
+  type io = (id * value) list
+
+  (*
+    Get the constants only
+  *)
+  val consts : prog -> id -> value VarMap.t
+
+  (*
+    Construct initial state for a program.
+    The id is the root node of the program evaluation.
+  *)
+  val init_state : prog -> id -> state
+
+  (*
+    Run a step of the program (not necessary to specify the program,
+      it should be encoded in the state).
+    State -> Inputs -> Next state, Outputs
+  *)
+  val step : state -> io -> (state * io)
+
+end = struct
 
   (* Values for variables *)
 
@@ -48,8 +86,6 @@ module I : INTERPRET = struct
 
   (* States of the interpret *)
 
-  (* path to node * subscope prefix in node * equations in scope *)
-  type scope = id * id * eqn ext list
 
   type state = {
     p          : prog;
@@ -407,11 +443,9 @@ module I : INTERPRET = struct
   *)
   let init_state p root =
     let (n, _) = find_node_decl p root in
-    let root_scope = ("", "", n.body) in
-
     let st = {
         p = p;
-        root_scope = root_scope;
+        root_scope = get_root_scope p root;
         save = VarMap.empty;
         outputs = (List.map (fun (_,(n,_),_) -> n) n.ret);
     } in
@@ -433,7 +467,7 @@ module I : INTERPRET = struct
         | _ -> ())
       p;
 
-    reset_scope env root_scope;
+    reset_scope env st.root_scope;
     { st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty }
 
   (*
diff --git a/main.ml b/main.ml
index 08bfe91..ccc0e0d 100644
--- a/main.ml
+++ b/main.ml
@@ -2,6 +2,8 @@ open Ast
 
 module Interpret = Interpret.I
 
+module Abstract = Apron_domain.D
+
 (* command line options *)
 let dump = ref false
 let dumprn = ref false