summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile6
-rw-r--r--abstract/abs_interp.ml14
-rw-r--r--abstract/apron_domain.ml132
-rw-r--r--abstract/environment_domain.ml36
-rw-r--r--abstract/transform.ml4
-rw-r--r--interpret/ast_util.ml11
-rw-r--r--interpret/interface.ml46
-rw-r--r--interpret/interpret.ml50
-rw-r--r--main.ml2
9 files changed, 242 insertions, 59 deletions
diff --git a/Makefile b/Makefile
index 69bf0ce..2b6f7c6 100644
--- a/Makefile
+++ b/Makefile
@@ -11,9 +11,11 @@ SRC= main.ml \
abstract/formula.ml \
abstract/formula_printer.ml \
abstract/transform.ml \
- interpret/bad_interpret.ml \
- interpret/interface.ml \
+ abstract/environment_domain.ml \
+ abstract/apron_domain.ml \
+ abstract/abs_interp.ml \
interpret/interpret.ml \
+ interpret/ast_util.ml \
interpret/rename.ml
all: $(BIN)
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
new file mode 100644
index 0000000..403e3e8
--- /dev/null
+++ b/abstract/abs_interp.ml
@@ -0,0 +1,14 @@
+open Ast
+open Formula
+
+open Util
+open Environment_domain
+
+module I (E : ENVIRONMENT_DOMAIN) : sig
+
+ val init_state : prog -> id -> E.t
+ val do_step : prog -> id -> E.t -> E.t
+
+end = struct
+
+end
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
new file mode 100644
index 0000000..1cc418e
--- /dev/null
+++ b/abstract/apron_domain.ml
@@ -0,0 +1,132 @@
+open Formula
+open Ast
+
+open Util
+open Environment_domain
+
+open Apron
+
+module D : ENVIRONMENT_DOMAIN = struct
+
+ (* manager *)
+ type man = Polka.loose Polka.t
+ let manager = Polka.manager_alloc_loose ()
+
+ (* abstract elements *)
+ type t = man Abstract1.t
+
+ (* direct translation of numerical expressions into Apron tree expressions *)
+ (* TODO : some variables have type real and not int... *)
+ 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) ->
+ texpr_of_nexpr e
+ | NUnary(AST_UMINUS, e) ->
+ (* 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),
+ Texpr1.Int,
+ Texpr1.Zero)
+ | NBinary(op, e1, e2) ->
+ 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),
+ Texpr1.Int,
+ Texpr1.Zero)
+
+ (* 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 init = Abstract1.top manager (Environment.make [||] [||])
+ let bottom = Abstract1.bottom manager (Environment.make [||] [||])
+ let is_bot = Abstract1.is_bottom manager
+
+ let addvar x id isfloat =
+ let env = Abstract1.env x in
+ let env2 = if isfloat then
+ Environment.add env [||] [| Var.of_string id |]
+ else
+ Environment.add env [| Var.of_string id |] [||]
+ in
+ Abstract1.change_environment manager x env2 false
+ let rmvar x id =
+ let v = [| Var.of_string id |] in
+ let env = Abstract1.env x in
+ let env2 = Environment.remove env v in
+ let y = Abstract1.forget_array manager x v false in
+ Abstract1.change_environment manager y env2 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)
+
+ (* Apply some formula to the environment *)
+ let rec apply_cl x (cons, rest) =
+ 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)
+
+
+ (* 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_all fmt x =
+ Abstract1.print fmt x;
+ Format.fprintf fmt "@?"
+
+ 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_all fmt xx
+
+end
+
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
new file mode 100644
index 0000000..5664474
--- /dev/null
+++ b/abstract/environment_domain.ml
@@ -0,0 +1,36 @@
+open Ast
+open Formula
+
+module type ENVIRONMENT_DOMAIN = sig
+ type t
+
+ (* construction *)
+ val init : t
+ val bottom : t
+ val is_bot : t -> bool
+
+ (* variable management *)
+ val addvar : t -> id -> bool -> t (* integer or float variable ? *)
+ val rmvar : t -> id -> t
+ val vars : t -> (id * bool) list
+ val vbottom : t -> t (* bottom value with same environment *)
+
+ (* abstract operation *)
+ val apply_f : t -> bool_expr -> t
+ val apply_cl : t -> conslist -> t
+
+ (* set-theoretic operations *)
+ val join : t -> t -> t (* union *)
+ val meet : t -> t -> t (* intersection *)
+ val widen : t -> t -> t
+
+ (* order *)
+ val subset : t -> t -> bool
+ val eq : t -> t -> bool
+
+ (* pretty-printing *)
+ val print_vars : Format.formatter -> t -> id list -> unit
+ val print_all : Format.formatter -> t -> unit
+end
+
+
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 56d54ce..e6886b8 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -191,10 +191,8 @@ and f_of_scope active td (node, prefix, eqs) =
(List.map do_eq eqs)
and f_of_prog p root =
- let (n, _) = find_node_decl p root in
- let root_scope = ("", "", n.body) in
let td = {
- root_scope = root_scope;
+ root_scope = get_root_scope p root;
p = p;
consts = I.consts p root;
} in
diff --git a/interpret/ast_util.ml b/interpret/ast_util.ml
index 80411d8..f5a1978 100644
--- a/interpret/ast_util.ml
+++ b/interpret/ast_util.ml
@@ -27,6 +27,17 @@ let extract_const_decls =
[]
+(* Utility : scopes *)
+
+
+(* path to node * subscope prefix in node * equations in scope *)
+type scope = id * id * eqn ext list
+
+let get_root_scope p root =
+ let (n, _) = find_node_decl p root in
+ ("", "", n.body)
+
+
(* Utility : find instances declared in an expression *)
(* extract_instances :
diff --git a/interpret/interface.ml b/interpret/interface.ml
deleted file mode 100644
index 621bfa2..0000000
--- a/interpret/interface.ml
+++ /dev/null
@@ -1,46 +0,0 @@
-open Ast
-open Util
-
-
-module type INTERPRET = sig
-
-
- exception Bad_datatype
- type value
-
- val int_value : int -> value
- val bool_value : bool -> value
- val real_value : float -> value
-
- val as_int : value -> int
- val as_bool : value -> bool
- val as_real : value -> float
-
- val str_repr_of_val : value -> string
-
- type state
-
- val print_state : Format.formatter -> state -> unit
-
- type io = (id * value) list
-
- (*
- Get the constants only
- *)
- val consts : prog -> id -> value VarMap.t
-
- (*
- Construct initial state for a program.
- The id is the root node of the program evaluation.
- *)
- val init_state : prog -> id -> state
-
- (*
- Run a step of the program (not necessary to specify the program,
- it should be encoded in the state).
- State -> Inputs -> Next state, Outputs
- *)
- val step : state -> io -> (state * io)
-
-end
-
diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index 24903f1..f28bce0 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -1,9 +1,47 @@
open Ast
open Util
open Ast_util
-open Interface
-module I : INTERPRET = struct
+module I : sig
+
+ exception Bad_datatype
+ type value
+
+ val int_value : int -> value
+ val bool_value : bool -> value
+ val real_value : float -> value
+
+ val as_int : value -> int
+ val as_bool : value -> bool
+ val as_real : value -> float
+
+ val str_repr_of_val : value -> string
+
+ type state
+
+ val print_state : Format.formatter -> state -> unit
+
+ type io = (id * value) list
+
+ (*
+ Get the constants only
+ *)
+ val consts : prog -> id -> value VarMap.t
+
+ (*
+ Construct initial state for a program.
+ The id is the root node of the program evaluation.
+ *)
+ val init_state : prog -> id -> state
+
+ (*
+ Run a step of the program (not necessary to specify the program,
+ it should be encoded in the state).
+ State -> Inputs -> Next state, Outputs
+ *)
+ val step : state -> io -> (state * io)
+
+end = struct
(* Values for variables *)
@@ -48,8 +86,6 @@ module I : INTERPRET = struct
(* States of the interpret *)
- (* path to node * subscope prefix in node * equations in scope *)
- type scope = id * id * eqn ext list
type state = {
p : prog;
@@ -407,11 +443,9 @@ module I : INTERPRET = struct
*)
let init_state p root =
let (n, _) = find_node_decl p root in
- let root_scope = ("", "", n.body) in
-
let st = {
p = p;
- root_scope = root_scope;
+ root_scope = get_root_scope p root;
save = VarMap.empty;
outputs = (List.map (fun (_,(n,_),_) -> n) n.ret);
} in
@@ -433,7 +467,7 @@ module I : INTERPRET = struct
| _ -> ())
p;
- reset_scope env root_scope;
+ reset_scope env st.root_scope;
{ st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty }
(*
diff --git a/main.ml b/main.ml
index 08bfe91..ccc0e0d 100644
--- a/main.ml
+++ b/main.ml
@@ -2,6 +2,8 @@ open Ast
module Interpret = Interpret.I
+module Abstract = Apron_domain.D
+
(* command line options *)
let dump = ref false
let dumprn = ref false
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-09 16:54:25 +0000