summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-18 18:21:18 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-18 18:21:18 +0200
commit4d59f3a805d0cca882caab353ac8ec0dd4c04f73 (patch)
treeada69c3799c7fbb0d0cb6100bff2f4c649907edb
parent9714afeb275360110161c870b50627128fda75a0 (diff)
downloadSemVerif-Projet-4d59f3a805d0cca882caab353ac8ec0dd4c04f73.tar.gz
SemVerif-Projet-4d59f3a805d0cca882caab353ac8ec0dd4c04f73.zip
Begin work on interface with Apron
-rw-r--r--.gitignore3
-rw-r--r--Makefile5
-rw-r--r--abstract/relational_apron.ml37
l---------analyze1
-rw-r--r--libs/util.ml2
-rw-r--r--main.ml10
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 *)