Implemented first existential analysis using underapproximation for

assignment and filter

Makefile

@@ -14,9 +14,8 @@ MENHIR =    menhir
 # external libs
 
 APRONDIR = `$(OCAMLFIND) query apron`
-# APRONDIR = /users/absint/urban/lib/ocaml/site-lib/apron
+ZARITHDIR = `$(OCAMLFIND) query zarith`
 GMPDIR = `$(OCAMLFIND) query gmp`
-# GMPDIR = /users/absint/urban/lib/ocaml/site-lib/gmp
 OUNITDIR = `$(OCAMLFIND) query oUnit`
 
 # flags & paths
@@ -25,9 +24,9 @@ OUNITDIR = `$(OCAMLFIND) query oUnit`
 OCAMLDIR = `$(OCAMLC) -where`
 OCAMLFLAGS = -thread -g
 OCAMLOPTFLAGS = -thread
-OCAMLINC = -I $(APRONDIR) -I frontend -I utils -I domains -I main -I web -I $(OUNITDIR) -I tests -I $(GMPDIR)
-#OCAMLLIBS = bigarray.cma gmp.cma apron.cma boxMPQ.cma octD.cma polkaMPQ.cma str.cma unix.cma threads.cma
-OCAMLOPTLIBS = bigarray.cmxa gmp.cmxa apron.cmxa boxMPQ.cmxa octD.cmxa polkaMPQ.cmxa str.cmxa threads.cmxa
+OCAMLINC = -I $(APRONDIR) -I $(ZARITHDIR) -I frontend -I utils -I banal -I domains -I main -I web -I $(OUNITDIR) -I tests -I $(GMPDIR)
+#OCAMLLIBS = bigarray.cma gmp.cma apron.cma boxMPQ.cma octD.cma zarith.cma polkaMPQ.cma str.cma unix.cma threads.cma
+OCAMLOPTLIBS = bigarray.cmxa gmp.cmxa apron.cmxa boxMPQ.cmxa octD.cmxa zarith.cmxa polkaMPQ.cmxa str.cmxa threads.cmxa
 MENHIRFLAGS = --explain
 CFLAGS = -I $(OCAMLDIR) -O3 -Wall
 CLIBS = -lgmp
@@ -70,6 +69,25 @@ MLFILES = \
   frontend/AbstractSyntax.ml \
   frontend/ItoA.ml \
   utils/Constraints.ml \
+  utils/setext.ml \
+  utils/mapext.ml \
+  banal/banal_int.ml \
+  banal/banal_float.ml \
+  banal/banal_intinf.ml \
+  banal/banal_datatypes.ml \
+  banal/banal_rat.ml \
+  banal/banal_itv_int.ml \
+  banal/banal_itv_rat.ml \
+  banal/banal_itv_float.ml \
+  banal/banal_mathtypes.ml \
+  banal/banal_affine.ml \
+  banal/banal_abstract_syntax.ml \
+  banal/banal_typed_syntax.ml \
+  banal/banal_semantics.ml \
+  banal/banal_domain.ml \
+  banal/banal_linearization.ml \
+  banal/banal_apron_domain.ml \
+  banal/function_banal_converter.ml \
   domains/Partition.ml \
   domains/Numerical.ml \
   domains/Functions.ml \
@@ -94,6 +112,11 @@ TSTMLFILES = \
   tests/TerminationPolyhedraTest.ml \
   tests/Test.ml \
 
+
+CFILES = \
+  banal/ml_float.c \
+
+
 CMOFILES = $(MLFILES:%.ml=%.cmo)
 CMXFILES = $(MLFILES:%.ml=%.cmx)
 CMIFILES = $(MLIFILES:%.ml=%.cmi)

banal/banal_apron_domain.ml

@@ -40,9 +40,7 @@ module ApronDomain(Param: APRON_PARAM) = struct
 
 
   (* apron name of a variable *)
-  let apron_of_var (v:var) : Var.t =
-    Var.of_string (string_of_id (v.var_name^"#") v.var_id)
-
+  let apron_of_var (v:var) : Var.t = Var.of_string v.var_id
 
   let add_var_to_env env v =
     let i,r = match v.var_typ with

banal/banal_linearization.ml

@@ -16,7 +16,7 @@ module Affine = Banal_affine
 
 module Var = struct
   type t = var
-  let compare x y = compare_id x.var_id y.var_id
+  let compare x y = compare x.var_id y.var_id
   let to_string v = v.var_name
 end
 

banal/banal_typed_syntax.ml

@@ -43,7 +43,8 @@ and var = {
     var_name: string;
     var_extent: extent;
     var_typ: typ;
-    var_id: id;
+    (* var_id: id; *)
+    var_id: string;
     var_synthetic: bool; (* added by translation? *)
     var_scope: var_scope;
   }

banal/function_banal_converter.ml

@@ -14,13 +14,13 @@ let int_type = A_int (A_INTEGER, A_SIGNED)
 
 let var_to_banal (v:FAS.var) : var = 
   let name = v.FAS.varName in 
-  let id = Z.of_string v.FAS.varId in 
+  let id = v.FAS.varId in 
   {
     var_name = name;
     var_extent = dummy_extent;
     var_typ = int_type;
     var_id = id;
-    var_synthetic =false; (* added by translation? *)
+    var_synthetic = false; 
     var_scope = T_LOCAL;
   }
 
@@ -48,10 +48,9 @@ let rec of_aExp_aux (aExp:FAS.aExp) : expr =
       | FAS.A_MULTIPLY -> A_MULTIPLY
       | FAS.A_DIVIDE -> A_DIVIDE
     in T_binary (binOp, expr1, expr2) 
-  | FAS.A_RANDOM -> raise (Invalid_argument "TODO") 
-
+  | FAS.A_RANDOM -> T_int_const (Banal_intinf.minus_inf, Banal_intinf.inf) 
+    
 let of_aExp (aExp:FAS.aExp) : expr typed = (of_aExp_aux aExp, int_type, dummy_extent)
-
 
 let rec of_bExp_aux (bExp:FAS.bExp) : expr = 
   match bExp with 

domains/DecisionTree.ml

@@ -1013,7 +1013,7 @@ struct
     in aux t.tree []
 
 
-  let bwdAssign ?domain t e = 
+  let bwdAssign ?domain ?(underapprox = false) t e = 
     let cache = ref CMap.empty in
     let pre = domain in
     let post = t.domain in
@@ -1041,14 +1041,14 @@ struct
         then (* x is normalized *) Node((x,nx),build t xs,Bot)
         else (* x is not normalized *) Node((nx,x),Bot,build t xs)
     in
+    let b_bwdAssign = if underapprox then B.bwdAssign_underapprox else B.bwdAssign in
     let rec aux t cs =
       match t with
       | Bot -> Bot
       | Leaf f -> Leaf (F.bwdAssign f e)
       | Node((c,nc),l,r) -> match (fst e) with
         | A_var variable ->
-          if (C.var variable c)
-          then
+          if (C.var variable c) then
             let filter_constraints cs dom =
               List.fold_left (fun cs c ->
                   let b = B.inner env vars [c] in
@@ -1064,18 +1064,16 @@ struct
                 (match pre, post with
                  | Some pre, Some post ->
                    let key = c in
-                   let c = B.constraints (B.bwdAssign (B.meet
-                                                         (B.inner env vars [c]) post) e) in
+                   let c = B.constraints (b_bwdAssign (B.meet (B.inner env vars [c]) post) e) in
                    let c = filter_constraints c pre in
-                   let nc = B.constraints (B.bwdAssign (B.meet
-                                                          (B.inner env vars [nc]) post) e) in
+                   let nc = B.constraints (b_bwdAssign (B.meet (B.inner env vars [nc]) post) e)in
                    let nc = filter_constraints nc pre in
                    cache := CMap.add key (c,nc) !cache;
                    (c, nc)
                  | _ ->
                    let key = c in
-                   let c = B.constraints (B.bwdAssign (B.inner env vars [c]) e) in
-                   let nc = B.constraints (B.bwdAssign (B.inner env vars [nc]) e) in
+                   let c = B.constraints (b_bwdAssign (B.inner env vars [c]) e) in
+                   let nc = B.constraints (b_bwdAssign (B.inner env vars [nc]) e) in
                    cache := CMap.add key (c,nc) !cache;
                    (c, nc)
                 ) in
@@ -1110,11 +1108,12 @@ struct
       env = env;
       vars = vars }
 
-  let rec filter ?domain t e =
+  let rec filter ?domain ?(underapprox = false) t e =
     let pre = domain in
     let post = t.domain in
     let env = t.env in
     let vars = t.vars in
+    let b_filter = if underapprox then B.filter_underapprox else B.filter in
     let rec aux t bs cs =
       let bcs = match pre with
         | None -> B.inner env vars cs
@@ -1217,7 +1216,7 @@ struct
         | None -> B.inner env vars []
         | Some post -> B.meet (B.inner env vars []) post
       in
-      let bs = List.map (fun c -> let nc = C.negate c in (c,nc)) (B.constraints (B.filter bp e)) in
+      let bs = List.map (fun c -> let nc = C.negate c in (c,nc)) (B.constraints (b_filter bp e)) in
       let bs = List.sort L.compare bs in
       { domain = pre; tree = aux t.tree bs []; env = env; vars = vars }
 

domains/Domain.ml

@@ -33,8 +33,8 @@ sig
   val dual_widen : t -> t -> t
 
   val terminating : t -> bool
-  val bwdAssign : ?domain:B.t -> t -> aExp * aExp -> t
-  val filter : ?domain:B.t -> t -> bExp -> t
+  val bwdAssign : ?domain:B.t -> ?underapprox:bool -> t -> aExp * aExp -> t
+  val filter : ?domain:B.t -> ?underapprox:bool -> t -> bExp -> t
   val reset : ?mask:t -> t -> bExp -> t
   val refine : t -> B.t -> t
 

domains/Numerical.ml

@@ -17,6 +17,7 @@ open Constraints
 module type APRON_PARAM = sig 
   type lib
   val manager: lib Manager.t 
+  val supports_underapproximation: bool
 end
 
 (** Single partition of the domain of a ranking function 
@@ -61,6 +62,28 @@ module Numerical(Param: APRON_PARAM)(C: CONSTRAINT): PARTITION = struct
 
   (**)
 
+  let print fmt b =
+    let vars = b.vars in
+    let a = Lincons1.array_make b.env (List.length b.constraints) in
+    let i = ref 0 in
+    List.iter (fun c -> Lincons1.array_set a !i c; i := !i + 1) b.constraints;
+    let b = Abstract1.of_lincons_array manager b.env a in
+    let a = Abstract1.to_lincons_array manager b in
+    let cs = ref [] in
+    for i=0 to (Lincons1.array_length a)-1 do
+      cs := (Lincons1.array_get a i)::!cs;
+    done;
+    match !cs with
+    | [] -> Format.fprintf fmt "top"
+    | x::_ ->
+      if (C.isBot x) then Format.fprintf fmt "bottom" else
+        let i = ref 1 and l = List.length !cs in
+        List.iter (fun c ->
+            C.print vars fmt c;
+            if (!i = l) then () else Format.fprintf fmt " && ";
+            i := !i + 1
+          ) !cs
+
   let bot e vs = {
     constraints = [Lincons1.make_unsat e];
     env = e;
@@ -190,6 +213,22 @@ module Numerical(Param: APRON_PARAM)(C: CONSTRAINT): PARTITION = struct
       done; { constraints = !cs; env = env; vars = vars }
     | _ -> raise (Invalid_argument "fwdAssign: unexpected lvalue")
 
+
+  let bwdAssign_underapprox (t:t) ((x,e): aExp * aExp) : t = match x with
+    | A_var x ->
+      if not Param.supports_underapproximation then
+        raise (Invalid_argument "Underapproximation not supported by this abstract domain, use polyhedra instead");
+      let env = t.env in
+      let vars = t.vars in
+      let at = to_apron_t t in
+      let top = Abstract1.top manager (Abstract1.env at) in
+      let pre = top in (* use top as pre environment *)
+      let assignDest = Banal_domain.STRONG (Function_banal_converter.var_to_banal x) in
+      let assignValue = Function_banal_converter.of_aExp e in
+      let assigned = BanalApron.bwd_assign at () assignDest assignValue pre in
+      of_apron_t env vars assigned
+    | _ -> raise (Invalid_argument "bwdAssign_underapprox: unexpected lvalue")
+
   let bwdAssign b (x,e) = match x with
     | A_var x ->
       let env = b.env in
@@ -209,14 +248,18 @@ module Numerical(Param: APRON_PARAM)(C: CONSTRAINT): PARTITION = struct
 
 
   let filter_underapprox (t:t) (e:bExp) : t = 
+    if not Param.supports_underapproximation then
+      raise (Invalid_argument "Underapproximation not supported by this abstract domain, use octagons or polyhedra instead");
     let env = t.env in
     let vars = t.vars in
     let expr = Function_banal_converter.of_bExp e in
     let at = to_apron_t t in
     let top = Abstract1.top manager (Abstract1.env at) in
+    let bot = Abstract1.bottom manager (Abstract1.env at) in
     let pre = top in (* use top as pre environment *)
-    let filtered = BanalApron.bwd_filter at top () expr () pre in
-    of_apron_t env vars filtered
+    let filtered = BanalApron.bwd_filter at bot () expr () pre in
+    let result = of_apron_t env vars filtered in 
+    result
 
 
   let rec filter b e =
@@ -287,27 +330,6 @@ module Numerical(Param: APRON_PARAM)(C: CONSTRAINT): PARTITION = struct
 
   (**)
 
-  let print fmt b =
-    let vars = b.vars in
-    let a = Lincons1.array_make b.env (List.length b.constraints) in
-    let i = ref 0 in
-    List.iter (fun c -> Lincons1.array_set a !i c; i := !i + 1) b.constraints;
-    let b = Abstract1.of_lincons_array manager b.env a in
-    let a = Abstract1.to_lincons_array manager b in
-    let cs = ref [] in
-    for i=0 to (Lincons1.array_length a)-1 do
-      cs := (Lincons1.array_get a i)::!cs;
-    done;
-    match !cs with
-    | [] -> Format.fprintf fmt "top"
-    | x::_ ->
-      if (C.isBot x) then Format.fprintf fmt "bottom" else
-        let i = ref 1 and l = List.length !cs in
-        List.iter (fun c ->
-            C.print vars fmt c;
-            if (!i = l) then () else Format.fprintf fmt " && ";
-            i := !i + 1
-          ) !cs
 
 end
 
@@ -317,6 +339,7 @@ module B = Numerical(
   struct 
     type lib = Box.t
     let manager = Box.manager_alloc ()
+    let supports_underapproximation = false
   end)(C)
 
 (** Single partition of the domain of a ranking function 
@@ -325,6 +348,7 @@ module O = Numerical(
   struct 
     type lib = Oct.t 
     let manager = Oct.manager_alloc () 
+    let supports_underapproximation = false
   end)(C)
 
 (** Single partition of the domain of a ranking function 
@@ -333,4 +357,5 @@ module P = Numerical(
   struct 
     type lib = Polka.loose Polka.t
     let manager = Polka.manager_alloc_loose ()
+    let supports_underapproximation = true
   end)(C)

domains/Partition.ml

@@ -34,6 +34,7 @@ module type PARTITION = sig
 
   val fwdAssign : t -> aExp * aExp -> t
   val bwdAssign : t -> aExp * aExp -> t
+  val bwdAssign_underapprox : t -> aExp * aExp -> t
   val filter : t -> bExp -> t
   val filter_underapprox : t -> bExp -> t