summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-08 10:47:49 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-08 10:47:49 +0200
commitbbdb36bfad796b26b16233e1693bb9dc8a909130 (patch)
treeae546daa64c5419b558af23a672422f0663f7c70
parent3b647cab0d3ac143b97524e6b0a406c349898db5 (diff)
downloadscade-analyzer-bbdb36bfad796b26b16233e1693bb9dc8a909130.tar.gz
scade-analyzer-bbdb36bfad796b26b16233e1693bb9dc8a909130.zip
Adapt abs_interp to use ENUM_DOMAIN2 (this is a test...)
-rw-r--r--abstract/abs_interp.ml132
-rw-r--r--abstract/enum_domain_edd.ml48
-rw-r--r--main.ml6
3 files changed, 113 insertions, 73 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index cb5ae9c..10bd33f 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -7,10 +7,11 @@ open Cmdline
open Util
open Num_domain
open Enum_domain
+open Enum_domain_edd
-module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
+module I (ED : ENUM_ENVIRONMENT_DOMAIN2) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
type st
@@ -56,21 +57,22 @@ end = struct
dd_add_case : dd_v -> case_v -> unit
*)
let dd_add_case env (enum, num) =
- let rec aux enum vals = function
- | [] ->
- let case = List.rev vals in
- begin try let e0, n0 = Hashtbl.find env.data case in
- Hashtbl.replace env.data case (ED.join enum e0, ND.join num n0);
- with Not_found ->
- Hashtbl.add env.data case (enum, num);
- end
- | p::q ->
- List.iter
- (fun v -> match ED.apply_cons enum (E_EQ, p, EItem v) with
- | [en] -> aux en (v::vals) q
- | _ -> assert false)
- (ED.project enum p)
- in aux enum [] env.d_vars
+ if not (ED.is_bot enum || ND.is_bot num) then
+ let rec aux enum vals = function
+ | [] ->
+ let case = List.rev vals in
+ begin try let e0, n0 = Hashtbl.find env.data case in
+ Hashtbl.replace env.data case (ED.join enum e0, ND.join num n0);
+ with Not_found ->
+ Hashtbl.add env.data case (enum, num);
+ end
+ | p::q ->
+ List.iter
+ (fun v -> let en = ED.apply_cons enum (E_EQ, p, EItem v) in
+ assert (not (ED.is_bot en));
+ aux en (v::vals) q)
+ (ED.project enum p)
+ in aux enum [] env.d_vars
(*
dd_singleton : id list -> case_v -> dd_v
@@ -101,14 +103,12 @@ end = struct
vv
(*
- dd_apply_econs : dd_v -> enum_cons -> dd_v
+ dd_apply_ecl : dd_v -> enum_cons list -> dd_v
*)
- let dd_apply_econs v cons =
+ let dd_apply_ecl v cons =
let vv = dd_bot v.d_vars in
Hashtbl.iter (fun case (enum, num) ->
- List.iter
- (fun enum -> dd_add_case vv (enum, num))
- (ED.apply_cons enum cons))
+ dd_add_case vv (ED.apply_cl enum cons, num))
v.data;
vv
@@ -133,7 +133,7 @@ end = struct
try let e2, n2 = Hashtbl.find b.data case in
let en, nn = ED.meet enum e2, ND.meet n2 num in
if not (ND.is_bot nn) then Hashtbl.add vv.data case (en, nn)
- with _ -> ())
+ with Not_found -> ())
a.data;
vv
@@ -143,10 +143,8 @@ end = struct
let rec apply_cl env (ec, nc, r) =
match r with
| CLTrue ->
- let env_ec = List.fold_left dd_apply_econs env ec in
+ let env_ec = dd_apply_ecl env ec in
let env_nc = dd_apply_ncl env_ec nc in
- (* Format.printf "[[ %a -> %a ]]@."
- print_dd env print_dd env_nc; *)
env_nc
| CLFalse -> dd_bot env.d_vars
| CLAnd(a, b) ->
@@ -194,33 +192,34 @@ end = struct
add_case : st -> case_v -> unit
*)
let add_case st (enum, num) =
- let rec aux enum vals = function
- | [] ->
- let case = List.rev vals in
- begin try let e0, n0 = Hashtbl.find st.env case in
- if (not (ED.subset enum e0)) || (not (ND.subset num n0)) then begin
- begin try
- let n = Hashtbl.find st.widen case in
- let jw = if n < st.opt.widen_delay then ND.join else ND.widen in
- Hashtbl.replace st.env case (ED.join e0 enum, jw n0 num);
- Hashtbl.replace st.widen case (n+1);
- with Not_found ->
- Hashtbl.replace st.env case (ED.join enum e0, ND.join num n0);
- Hashtbl.add st.widen case 0;
- end;
+ if not (ED.is_bot enum || ND.is_bot num) then
+ let rec aux enum vals = function
+ | [] ->
+ let case = List.rev vals in
+ begin try let e0, n0 = Hashtbl.find st.env case in
+ if (not (ED.subset enum e0)) || (not (ND.subset num n0)) then begin
+ begin try
+ let n = Hashtbl.find st.widen case in
+ let jw = if n < st.opt.widen_delay then ND.join else ND.widen in
+ Hashtbl.replace st.env case (ED.join e0 enum, jw n0 num);
+ Hashtbl.replace st.widen case (n+1);
+ with Not_found ->
+ Hashtbl.replace st.env case (ED.join enum e0, ND.join num n0);
+ Hashtbl.add st.widen case 0;
+ end;
+ if not (List.mem case st.delta) then st.delta <- case::st.delta
+ end
+ with Not_found ->
+ Hashtbl.add st.env case (enum, num);
if not (List.mem case st.delta) then st.delta <- case::st.delta
end
- with Not_found ->
- Hashtbl.add st.env case (enum, num);
- if not (List.mem case st.delta) then st.delta <- case::st.delta
- end
- | p::q ->
- List.iter
- (fun v -> match ED.apply_cons enum (E_EQ, p, EItem v) with
- | [en] -> aux en (v::vals) q
- | _ -> assert false)
- (ED.project enum p)
- in aux enum [] st.acc_d_vars
+ | p::q ->
+ List.iter
+ (fun v -> let en = ED.apply_cons enum (E_EQ, p, EItem v) in
+ assert (not (ED.is_bot en));
+ aux en (v::vals) q)
+ (ED.project enum p)
+ in aux enum [] st.acc_d_vars
(*
@@ -229,10 +228,8 @@ end = struct
let rec apply_cl_get_all_cases (enum, num) (ec, nc, r) =
match r with
| CLTrue ->
- let enums = List.fold_left
- (fun enums ec -> List.flatten
- (List.map (fun e -> ED.apply_cons e ec) enums))
- [enum] ec in
+ let enum = ED.apply_cl enum ec in
+ let enums = if ED.is_bot enum then [] else [enum] in
let num = ND.apply_cl num nc in
List.map (fun ec -> ec, num) enums
| CLFalse -> []
@@ -257,13 +254,12 @@ end = struct
let enum = ED.assign enum assign_e in
let num = ND.assign num assign_n in
- List.fold_left
- (fun (enum, num) (var, t) ->
- let e, n = match t with
- | TEnum _ -> ED.forgetvar enum var, num
- | TReal | TInt -> enum, ND.forgetvar num var
- in e, n)
- (enum, num) st.forget
+ let ef, nf = List.fold_left
+ (fun (ef, nf) (var, t) -> match t with
+ | TEnum _ -> var::ef, nf
+ | TReal | TInt -> ef, var::nf)
+ ([], []) st.forget in
+ ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf
let dd_pass_cycle st (v : dd_v) =
let vv = dd_bot st.acc_d_vars in
@@ -363,12 +359,14 @@ end = struct
set_target_case : st -> dd_v -> case -> dd_v
*)
let set_target_case st env case =
- List.fold_left2
- (fun env id v ->
- if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then
- dd_apply_econs env (E_EQ, id, EItem v)
- else env)
- env st.acc_d_vars case
+ let cl =
+ List.fold_left2
+ (fun cl id v ->
+ if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then
+ (E_EQ, id, EItem v)::cl
+ else cl)
+ [] st.acc_d_vars case
+ in dd_apply_ecl env cl
(*
do_prog : rooted_prog -> unit
diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
index 60f2d3b..a372772 100644
--- a/abstract/enum_domain_edd.ml
+++ b/abstract/enum_domain_edd.ml
@@ -1,9 +1,41 @@
open Ast
open Formula
open Util
-open Enum_domain
-module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
+module type ENUM_ENVIRONMENT_DOMAIN2 = sig
+ type t
+
+ type item = string
+
+ (* construction *)
+ val top : (id * item list) list -> t
+ val bot : (id * item list) list -> t
+ val is_bot : t -> bool
+
+ (* variable management *)
+ val vars : t -> (id * item list) list
+
+ val forgetvar : t -> id -> t
+ val forgetvars : t -> id list -> t
+ val project : t -> id -> item list
+
+ (* set-theoretic operations *)
+ val join : t -> t -> t (* union *)
+ val meet : t -> t -> t (* intersection *)
+
+ val subset : t -> t -> bool
+ val eq : t -> t -> bool
+
+ (* abstract operations *)
+ val apply_cons : t -> enum_cons -> t
+ val apply_cl : t -> enum_cons list -> t
+ val assign : t -> (id * id) list -> t
+
+ (* pretty-printing *)
+ val print : Format.formatter -> t -> unit
+end
+
+module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct
exception Top
type item = string
@@ -132,11 +164,19 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
(*
top : (id * item list) list -> t
+ bot : (id * item list) list -> t
*)
let top vars =
let order = Hashtbl.create 12 in
List.iteri (fun i (id, _) -> Hashtbl.add order id i) vars;
{ vars; order; root = DTop }
+ let bot vars = let t = top vars in { t with root = DBot }
+
+ (*
+ is_bot : t -> bool
+ *)
+ let is_bot x = (x.root = DBot)
+
(*
vars : t -> (id * item list) list
*)
@@ -243,8 +283,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
apply_cl : t -> enum_cons list -> t
*)
let apply_cons v x =
- let v = meet v (of_cons v x) in
- if v.root = DBot then [] else [v]
+ meet v (of_cons v x)
+
let apply_cl v ec =
let rec cl_k = function
| [] -> { v with root = DTop }
diff --git a/main.ml b/main.ml
index 2995e24..e5d162e 100644
--- a/main.ml
+++ b/main.ml
@@ -6,12 +6,14 @@ open Num_domain
open Nonrelational
open Apron_domain
+open Enum_domain_edd
+
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_Itv = Abs_interp.I(Enum_domain_edd.EDD)(ItvND)
+module AI_Rel = Abs_interp.I(Enum_domain_edd.EDD)(Apron_domain.ND)
module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND)