Begin work on interface with Apron

6 files changed, 52 insertions, 6 deletions

diff --git a/.gitignore b/.gitignore
index 17ef805..ca7415d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
 *.swp
 _build
-analyzer
+analyze
+*~
diff --git a/Makefile b/Makefile
index 00cda6d..2907754 100644
--- a/Makefile
+++ b/Makefile
@@ -10,11 +10,14 @@ SRC= 	main.ml \
 		abstract/interpret.ml \
 		abstract/nonrelational.ml \
 		abstract/value_domain.ml \
+		abstract/relational_apron.ml
 
 all: $(BIN)
 
 $(BIN): $(SRC)
-	ocamlbuild -Is $(SRCDIRS) -cflags '-I /usr/lib/ocaml/zarith' -lflags '-I /usr/lib/ocaml/zarith zarith.cmxa' main.native
+	ocamlbuild -Is $(SRCDIRS) -cflags '-I +zarith -I +apron -I +gmp' \
+			-lflags '-I +zarith -I +apron -I +gmp zarith.cmxa bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa' \
+		    main.native
 	mv main.native $(BIN)
 
 clean:
diff --git a/abstract/relational_apron.ml b/abstract/relational_apron.ml
new file mode 100644
index 0000000..bd078cf
--- /dev/null
+++ b/abstract/relational_apron.ml
@@ -0,0 +1,37 @@
+open Apron
+open Util
+open Environment_domain
+
+module RelationalDomain : ENVIRONMENT_DOMAIN = struct
+
+    (* manager *)
+    type man = Polka.loose Polka.t
+    let manager = Polka.manager_alloc_loose ()
+
+    (* abstract elements *)
+    type t = man Abstract1.t
+
+    (* 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 vars x =
+        List.map Var.to_string @@
+        Array.to_list @@ snd @@ Environment.vars @@ Abstract1.env x
+
+    let assign x id e = x (* TODO *)
+    let compare x e1 e2 = x (* TODO *)
+
+    let join = Abstract1.join manager
+    let meet = Abstract1.meet manager
+    let widen = Abstract1.widening manager
+
+    let subset = Abstract1.is_leq manager
+
+    let var_str x idl = "" (* TODO *)
+
+end
+
diff --git a/analyze b/analyze
deleted file mode 120000
index 660214f..0000000
--- a/analyze
+++ /dev/null
@@ -1 +0,0 @@
-/home/katchup/Core/ENS/Info/psv-SemVerif-Projet/_build/main.native
\ No newline at end of file
diff --git a/libs/util.ml b/libs/util.ml
index 17c1ad4..68332b6 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -7,3 +7,5 @@ let rec fix f s =
   if fs = s
     then fs
     else fix f fs
+
+let (@@) f x = f x
diff --git a/main.ml b/main.ml
index 8f33d2d..937180e 100644
--- a/main.ml
+++ b/main.ml
@@ -19,15 +19,19 @@ module Interp_const = Interpret.Make(Env_dom_const)
 module Env_dom_interv = Nonrelational.NonRelational(Intervals_domain.Intervals)
 module Interp_interv = Interpret.Make(Env_dom_interv)
 
+module Interp_rel = Interpret.Make(Relational_apron.RelationalDomain)
+
 (* option parsing *)
 let dump = ref false
 let const_interp = ref false
 let interv_interp = ref false
-let poly_interp = ref false
+let rel_interp = ref false
 let get_interp () =
   if !interv_interp
       then Interp_interv.interpret
-      else Interp_const.interpret
+      else if !rel_interp
+        then Interp_rel.interpret
+        else Interp_const.interpret
 
 let ifile = ref ""
 let set_var v s = v := s
@@ -38,7 +42,7 @@ let options = [
   "--dump", Arg.Set dump, "Dump program source.";
   "--const-interp",  Arg.Set const_interp, "Use constant lattice interpreter.";
   "--interv-interp", Arg.Set interv_interp, "Use interval lattice interpreter.";
-  "--poly-interp", Arg.Set poly_interp, "Use polyhedra lattice interpreter.";
+  "--rel-interp", Arg.Set rel_interp, "Use relationnal (Apron) lattice.";
 ]
 
 (* parse and print filename *)