summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_domain.ml88
-rw-r--r--abstract/abs_interp.ml6
-rw-r--r--abstract/apron_domain.ml25
-rw-r--r--abstract/domain.ml3
-rw-r--r--abstract/formula.ml20
-rw-r--r--abstract/nonrelational.ml21
-rw-r--r--abstract/num_domain.ml (renamed from abstract/environment_domain.ml)12
7 files changed, 124 insertions, 51 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
new file mode 100644
index 0000000..ddc34ab
--- /dev/null
+++ b/abstract/abs_domain.ml
@@ -0,0 +1,88 @@
+open Ast
+open Formula
+open Num_domain
+open Typing
+
+module type ENVIRONMENT_DOMAIN = sig
+ type t
+ type itv
+
+ (* construction *)
+ val init : t
+ val bottom : t
+ val vbottom : t -> t (* bottom value with same environment *)
+ val is_bot : t -> bool
+
+ (* variable management *)
+ val addvar : t -> id -> Typing.typ -> t
+ val rmvar : t -> id -> t
+ val vars : t -> (id * Typing.typ) list
+
+ val forgetvar : t -> id -> t
+ val var_itv : t -> id -> itv
+
+ (* set_theoretic operations *)
+ val join : t -> t -> t (* union *)
+ val meet : t -> t -> t (* intersection *)
+ val widen : t -> t -> t
+
+ val subset : t -> t -> bool
+ val eq : t -> t -> bool
+
+ (* abstract operations *)
+ val apply_f : t -> bool_expr -> t
+ val apply_cl : t -> conslist -> t
+ val assign : t -> (id * num_expr) list -> t
+
+ (* pretty-printing *)
+ val print_vars : Format.formatter -> t -> id list -> unit
+ val print_all : Format.formatter -> t -> unit
+ val print_itv : Format.formatter -> itv -> unit
+
+end
+
+module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
+
+ type t = ND.t
+ type itv = ND.itv
+
+ let init = ND.init
+ let bottom = ND.bottom
+ let vbottom = ND.vbottom
+ let is_bot = ND.is_bot
+
+ let addvar x id ty = ND.addvar x id (ty = TReal)
+ let rmvar = ND.rmvar
+ let vars x = List.map (fun (id, r) -> id, if r then TReal else TInt) (ND.vars x)
+
+ let forgetvar = ND.forgetvar
+ let var_itv = ND.var_itv
+
+ let join = ND.join
+ let meet = ND.meet
+ let widen = ND.widen
+
+ let subset = ND.subset
+ let eq = ND.eq
+
+ let rec apply_cl x (cons, rest) = match rest with
+ | CLTrue ->
+ ND.apply_ncl x cons
+ | CLFalse -> vbottom x
+ | CLAnd(a, b) ->
+ let y = apply_cl x (cons, a) in
+ apply_cl y (cons, b)
+ | CLOr((ca, ra), (cb, rb)) ->
+ let y = apply_cl x (cons@ca, ra) in
+ let z = apply_cl x (cons@cb, rb) in
+ join y z
+
+ let apply_f x f = apply_cl x (conslist_of_f f)
+
+ let assign = ND.assign
+
+ let print_vars = ND.print_vars
+ let print_all = ND.print_all
+ let print_itv = ND.print_itv
+
+end
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index c621734..1d3e20a 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -4,7 +4,8 @@ open Formula
open Typing
open Util
-open Environment_domain
+open Abs_domain
+open Num_domain
module I (E : ENVIRONMENT_DOMAIN) : sig
@@ -36,8 +37,7 @@ end = struct
let cl_g = Formula.conslist_of_f f_g in
let env = List.fold_left
- (fun env (_, id, ty) ->
- E.addvar env id (ty = TReal))
+ (fun env (_, id, ty) -> E.addvar env id ty)
E.init
rp.all_vars
in
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index cef6b66..369f4b7 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -2,11 +2,11 @@ open Formula
open Ast
open Util
-open Environment_domain
+open Num_domain
open Apron
-module D : ENVIRONMENT_DOMAIN = struct
+module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
(* manager *)
type man = Polka.loose Polka.t
@@ -93,27 +93,14 @@ module D : ENVIRONMENT_DOMAIN = struct
Abstract1.bound_variable manager x (Var.of_string id)
(* Apply some formula to the environment *)
- let rec apply_cl x (cons, rest) =
+ let rec apply_ncl 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;
- let y = Abstract1.meet_tcons_array manager x ar in
- apply_cl_r y rest
-
- and apply_cl_r x = function
- | CLTrue -> x
- | CLFalse -> vbottom x
- | CLAnd(a, b) ->
- let y = apply_cl_r x a in
- apply_cl_r y b
- | CLOr(a, b) ->
- let y = apply_cl x a in
- let z = apply_cl x b in
- Abstract1.join manager y z
-
- let apply_f x f = apply_cl x (conslist_of_f f)
-
+ Abstract1.meet_tcons_array manager x ar
+
+
let assign x eqs =
let env = Abstract1.env x in
let vars = Array.of_list
diff --git a/abstract/domain.ml b/abstract/domain.ml
new file mode 100644
index 0000000..76635d1
--- /dev/null
+++ b/abstract/domain.ml
@@ -0,0 +1,3 @@
+open Ast
+open Formula
+
diff --git a/abstract/formula.ml b/abstract/formula.ml
index f3c1df1..a598750 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -2,6 +2,9 @@ open Ast
(* AST for logical formulas *)
+
+(* Numerical part *)
+
type num_expr =
(* constants *)
| NIntConst of int
@@ -12,6 +15,13 @@ type num_expr =
(* identifier *)
| NIdent of id
+type num_cons_op =
+ | CONS_EQ | CONS_NE
+ | CONS_GT | CONS_GE
+type num_cons = num_expr * num_cons_op (* always imply right member = 0 *)
+
+
+(* Logical part *)
type bool_expr =
(* constants *)
@@ -24,7 +34,6 @@ type bool_expr =
| BOr of bool_expr * bool_expr
| BNot of bool_expr
-
let f_and a b = match a, b with
| BConst false, _ | _, BConst false -> BConst false
| BConst true, b -> b
@@ -67,17 +76,14 @@ and eliminate_not_negate = function
| BOr(a, b) ->
BAnd(eliminate_not_negate a, eliminate_not_negate b)
+
+
(*
In big ANDs, try to separate levels of /\ and levels of \/
We also use this step to simplify trues and falses that may be present.
*)
-type cons_op =
- | CONS_EQ | CONS_NE
- | CONS_GT | CONS_GE
-type cons = num_expr * cons_op (* always imply right member = 0 *)
-
-type conslist = cons list * conslist_bool_expr
+type conslist = num_cons list * conslist_bool_expr
and conslist_bool_expr =
| CLTrue
| CLFalse
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 855f970..492b547 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -3,13 +3,13 @@ open Util
open Ast
open Value_domain
-open Environment_domain
+open Num_domain
let debug = false
(* Restricted domain, only support integers *)
-module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
+module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
type env = V.t VarMap.t
type t = Env of env | Bot
@@ -167,20 +167,9 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
List.fold_left restrict_var env
(extract_var (expr, zop, NIntConst 0))
- let rec apply_cl x (cons, rest) = match rest with
- | CLTrue ->
- let apply_cl_l x = List.fold_left apply_cons x cons in
- fix eq apply_cl_l x
- | CLFalse -> vbottom x
- | CLAnd(a, b) ->
- let y = apply_cl x (cons, a) in
- apply_cl y (cons, b)
- | CLOr((ca, ra), (cb, rb)) ->
- let y = apply_cl x (cons@ca, ra) in
- let z = apply_cl x (cons@cb, rb) in
- join y z
-
- let apply_f x f = apply_cl x (conslist_of_f f)
+ let apply_ncl x cl =
+ let f x = List.fold_left apply_cons x cl in
+ fix eq f x
(* Assignment *)
let assign x exprs =
diff --git a/abstract/environment_domain.ml b/abstract/num_domain.ml
index 6e84c75..59ed1a0 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/num_domain.ml
@@ -1,21 +1,22 @@
open Ast
open Formula
-module type ENVIRONMENT_DOMAIN = sig
+module type NUMERICAL_ENVIRONMENT_DOMAIN = sig
type t
type itv
(* construction *)
val init : t
val bottom : t
+ val vbottom : t -> t (* bottom value with same environment *)
val is_bot : t -> bool
(* variable management *)
- val addvar : t -> id -> bool -> t (* integer or float variable ? *)
- val forgetvar : t -> id -> t (* remove var from constraints *)
+ val addvar : t -> id -> bool -> t (* integer or real variable ? *)
val rmvar : t -> id -> t
val vars : t -> (id * bool) list
- val vbottom : t -> t (* bottom value with same environment *)
+
+ val forgetvar : t -> id -> t (* remove var from constraints *)
val var_itv : t -> id -> itv
(* set-theoretic operations *)
@@ -28,8 +29,7 @@ module type ENVIRONMENT_DOMAIN = sig
val eq : t -> t -> bool
(* abstract operation *)
- val apply_f : t -> bool_expr -> t
- val apply_cl : t -> conslist -> t
+ val apply_ncl : t -> num_cons list -> t
val assign : t -> (id * num_expr) list -> t
(* pretty-printing *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-24 15:20:45 +0000