diff options
| -rw-r--r-- | .gitignore | 3 | ||||
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | abstract/relational_apron.ml | 37 | ||||
| l--------- | analyze | 1 | ||||
| -rw-r--r-- | libs/util.ml | 2 | ||||
| -rw-r--r-- | main.ml | 10 |
6 files changed, 52 insertions, 6 deletions
@@ -1,3 +1,4 @@ *.swp _build -analyzer +analyze +*~ @@ -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 @@ -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 *) |