Add support for octagons.

5 files changed, 223 insertions, 21 deletions

diff --git a/Makefile b/Makefile
index 4a76187..1faacde 100644
--- a/Makefile
+++ b/Makefile
@@ -34,7 +34,7 @@ all: $(BIN)
 
 $(BIN): $(SRC)
 	ocamlbuild -Is $(SRCDIRS) -cflags '-I +zarith -I +apron -I +gmp -I +str' \
-			-lflags '-I +zarith -I +apron -I +gmp -I +str str.cmxa zarith.cmxa bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa unix.cmxa' \
+			-lflags '-I +zarith -I +apron -I +gmp -I +str str.cmxa zarith.cmxa bigarray.cmxa gmp.cmxa apron.cmxa polkaMPQ.cmxa unix.cmxa octMPQ.cmxa' \
 		    main.native \
 			-classic-display
 	mv main.native $(BIN)
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index a929c0b..58cd544 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -11,7 +11,9 @@ open Apron
   Mostly direct translation between the two.
 *)
 
-module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
+(* Polyhedra *)
+
+module ND_Poly : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
     (* manager *)
     type man = Polka.loose Polka.t
@@ -127,9 +129,142 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
     (* Pretty-printing *)
     let print fmt x =
-        Abstract1.minimize manager x;
-        Abstract1.print fmt x;
-        Format.fprintf fmt "@?"
+        if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x;
+        Format.fprintf fmt "%a@?" Abstract1.print x
+
+    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 fmt xx
+
+    let print_itv = Interval.print
+
+end
+
+
+(* Octagons *)
+
+module ND_Oct : NUMERICAL_ENVIRONMENT_DOMAIN = struct
+
+    (* manager *)
+    type man = Oct.t
+    let manager = Oct.manager_alloc()
+
+    type itv = Interval.t
+
+    (* abstract elements *)
+    type t = man Abstract1.t
+
+    (* direct translation of numerical expressions into Apron tree expressions *)
+    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, is_real) ->
+            Texpr1.Unop(
+                Texpr1.Cast,
+                texpr_of_nexpr e,
+                (if is_real then Texpr1.Real else Texpr1.Int),
+                Texpr1.Rnd)
+        | NUnary(AST_UMINUS, e, is_real) ->
+            (* 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),
+                (if is_real then Texpr1.Real else Texpr1.Int),
+                Texpr1.Rnd)
+        | NBinary(op, e1, e2, is_real) ->
+            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),
+                  (if is_real then Texpr1.Real else Texpr1.Int),
+                  Texpr1.Rnd)
+    
+    (* 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 v_env vars = 
+        let intv = List.map
+              (fun (s, _) -> Var.of_string s)
+              (List.filter (fun (_, n) -> not n) vars) in
+        let realv = List.map
+              (fun (s, _) -> Var.of_string s)
+              (List.filter (fun (_, n) -> n) vars) in
+        (Environment.make (Array.of_list intv) (Array.of_list realv))
+
+    let top vars =
+      Abstract1.top manager (v_env vars)
+    let bottom vars = Abstract1.bottom manager (v_env vars)
+    let is_bot = Abstract1.is_bottom manager
+    let is_top = Abstract1.is_top manager
+
+    let forgetvar x id =
+        let v = [| Var.of_string id |] in
+        Abstract1.forget_array manager x v 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)
+
+    let project x id =
+        Abstract1.bound_variable manager x (Var.of_string id)
+
+    (* Apply some formula to the environment *)
+    let apply_cl x cons =
+        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;
+        Abstract1.meet_tcons_array manager x ar
+
+    let apply_cons x cons = apply_cl x [cons]
+
+
+    let assign x eqs =
+      let env = Abstract1.env x in
+      let vars = Array.of_list
+        (List.map (fun (id, _) -> Var.of_string id) eqs) in
+      let vals = Array.of_list
+        (List.map (fun (_, v) -> Texpr1.of_expr env (texpr_of_nexpr v)) eqs) in
+      Abstract1.assign_texpr_array manager x vars vals None
+
+    
+    (* 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 fmt x =
+        if not (Oct.manager_is_oct manager) then Abstract1.minimize manager x;
+        Format.fprintf fmt "%a@?" Abstract1.print x
 
     let print_vars fmt x idl = 
         let prevars = vars x in
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index ed029da..dbc17c9 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -33,9 +33,14 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
         | NIdent id -> get_var env id
         | NIntConst i -> V.const i
         | NRealConst f -> V.const (int_of_float f) (* TODO floats *)
-        | NUnary (AST_UPLUS, e, _) -> eval env e
-        | NUnary (AST_UMINUS, e, _) -> V.neg (eval env e)
-        | NBinary (op, e1, e2, _) ->
+        | NUnary (AST_UPLUS, e, isreal) ->
+          if isreal then not_implemented "real type for nonrelationnal domain";
+          eval env e
+        | NUnary (AST_UMINUS, e, isreal) ->
+          if isreal then not_implemented "real type for nonrelationnal domain";
+          V.neg (eval env e)
+        | NBinary (op, e1, e2, isreal) ->
+            if isreal then not_implemented "real type for nonrelationnal domain";
             let f = match op with
             | AST_PLUS -> V.add
             | AST_MINUS -> V.sub
diff --git a/main.ml b/main.ml
index 55a3837..08ec36a 100644
--- a/main.ml
+++ b/main.ml
@@ -16,19 +16,21 @@ module Interpret = Interpret.I
 module ItvND = Nonrelational.ND(Intervals_domain.VD)
 
 module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
-module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND)
+module AI_Poly = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND_Poly)
+module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND_Oct)
 
 module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
-module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND)
+module AI_Poly_EDD = Abs_interp_edd.I(Apron_domain.ND_Poly)
+module AI_Oct_EDD = Abs_interp_edd.I(Apron_domain.ND_Oct)
 
 module AI_S_Itv_DP = Abs_interp_dynpart.I
       (Enum_domain.MultiValuation)(ItvND)
 module AI_S_Rel_DP = Abs_interp_dynpart.I
-      (Enum_domain.MultiValuation)(Apron_domain.ND)
+      (Enum_domain.MultiValuation)(Apron_domain.ND_Poly)
 module AI_EDD_Itv_DP = Abs_interp_dynpart.I
       (Enum_domain_edd.EDD)(ItvND)
 module AI_EDD_Rel_DP = Abs_interp_dynpart.I
-      (Enum_domain_edd.EDD)(Apron_domain.ND)
+      (Enum_domain_edd.EDD)(Apron_domain.ND_Poly)
 
 (* command line options *)
 let times = ref false
@@ -37,9 +39,11 @@ let dumprn = ref false
 let test = ref false
 let vtest = ref false
 let ai_itv = ref false
-let ai_rel = ref false
+let ai_poly = ref false
+let ai_oct = ref false
 let ai_itv_edd = ref false
-let ai_rel_edd = ref false
+let ai_poly_edd = ref false
+let ai_oct_edd = ref false
 let ai_s_itv_dp = ref false
 let ai_s_rel_dp = ref false
 let ai_edd_itv_dp = ref false
@@ -68,12 +72,15 @@ let options = [
     "--test", Arg.Set test, "Simple testing (direct interpret).";
 
     "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals.";
-    "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron.";
+    "--ai-poly", Arg.Set ai_poly, "Do abstract analysis using Apron polyhedra domain.";
+    "--ai-oct", Arg.Set ai_oct, "Do abstract analysis using Apron octagon domain.";
 
     "--ai-itv-edd", Arg.Set ai_itv_edd,
         "Do abstract analysis using intervals and EDD disjunction domain.";
-    "--ai-rel-edd", Arg.Set ai_rel_edd,
-        "Do abstract analysis using Apron and EDD disjunction domain.";
+    "--ai-poly-edd", Arg.Set ai_poly_edd,
+        "Do abstract analysis using Apron polyhedra domain and EDD disjunction domain.";
+    "--ai-oct-edd", Arg.Set ai_oct_edd,
+        "Do abstract analysis using Apron octagon domain and EDD disjunction domain.";
 
     "--ai-s-itv-dp", Arg.Set ai_s_itv_dp,
         "Do abstract analysis using dynamic partitionning method, "^
@@ -172,8 +179,8 @@ let () =
       let prog = Rename.rename_prog prog in
       if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
 
-      if !ai_itv || !ai_rel
-          || !ai_itv_edd || !ai_rel_edd
+      if !ai_itv || !ai_poly || !ai_oct
+          || !ai_itv_edd || !ai_poly_edd || !ai_oct_edd
           || !ai_s_itv_dp || !ai_s_rel_dp
           || !ai_edd_itv_dp || !ai_edd_rel_dp then
       begin
@@ -206,10 +213,12 @@ let () =
           } in
           
           if !ai_itv then AI_Itv.do_prog opt rp;
-          if !ai_rel then AI_Rel.do_prog opt rp;
+          if !ai_poly then AI_Poly.do_prog opt rp;
+          if !ai_oct then AI_Oct.do_prog opt rp;
           
           if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
-          if !ai_rel_edd then AI_Rel_EDD.do_prog opt rp;
+          if !ai_poly_edd then AI_Poly_EDD.do_prog opt rp;
+          if !ai_oct_edd then AI_Oct_EDD.do_prog opt rp;
 
           if !ai_s_itv_dp then AI_S_Itv_DP.do_prog opt rp;
           if !ai_s_rel_dp then AI_S_Rel_DP.do_prog opt rp;
diff --git a/tests/source/tst_heater.scade b/tests/source/tst_heater.scade
new file mode 100755
index 0000000..c9212e9
--- /dev/null
+++ b/tests/source/tst_heater.scade
@@ -0,0 +1,53 @@
+const dt : real = 0.001;
+
+node heater(xi,yi : real) returns (xo, yo: real)
+let
+  automaton
+    initial state Off
+    --unless 
+    --  if xi <= 21.0 and yi <= 55.0 restart On;
+    let
+      xo = -xi * dt + xi;
+      yo = -3.0 * yi * dt + yi;
+    tel
+    until 
+      if xi <= 21.0 and yi <= 55.0 restart On;
+
+    state On
+    --unless 
+    --  if xi >= 24.0 or yi >= 75.0 restart Off;
+    let
+      xo = (100.0 - xi) * dt + xi;
+      yo = 2.0 * (150.0 - yi) * dt + yi;
+    tel
+    until 
+      if xi >= 24.0 or yi >= 75.0 restart Off;
+  returns xo, yo;
+tel
+
+node top (ix, iy : real) returns (x,y : real ; safe, stabilized : bool)
+var
+  mem: bool;
+  reached: bool;
+  safe_init : bool;
+  temp: bool;
+let
+  assume init_cond: ix = iy;
+
+  x,y = heater (ix -> pre x, iy -> pre y);
+  safe_init = (ix=iy and iy < 80.0) -> pre safe_init;
+  safe = not safe_init or y < 80.0;
+
+  reached = x >= 21.0 and x <= 24.0 and y >= 55.0 and y <= 75.0;
+  temp = x>=20.0 and x<=25.0;
+  
+  mem = 
+    (ix > 21.0 and ix < 24.0 and iy >= 55.0 and iy <= 75.0) 
+    -> reached or pre mem;
+
+  stabilized = not mem or temp;
+
+  guarantee g1: safe;
+  guarantee g2: stabilized;
+
+tel