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

4 files changed, 183 insertions, 3 deletions

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