summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-09 15:32:28 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-09 15:32:28 +0200
commitbc9ad2280839677bb46acfd846ff05bb37719b6e (patch)
tree238de281268baef8399d52c7315eb618b7e120d9
parent52a7d356a1c1c1bf0d1881d0cf6e13bb94dbc1a4 (diff)
downloadscade-analyzer-bc9ad2280839677bb46acfd846ff05bb37719b6e.tar.gz
scade-analyzer-bc9ad2280839677bb46acfd846ff05bb37719b6e.zip
Begin dynamic partitionning ; CORRECT BUG IN unpass_cycle !!
-rw-r--r--Makefile1
-rw-r--r--abstract/abs_interp_dynpart.ml375
-rw-r--r--abstract/abs_interp_edd.ml28
-rw-r--r--abstract/enum_domain.ml29
-rw-r--r--abstract/enum_domain_edd.ml40
-rw-r--r--abstract/varenv.ml8
-rw-r--r--main.ml45
-rw-r--r--tests/source/two_counters.scade12
8 files changed, 475 insertions, 63 deletions
diff --git a/Makefile b/Makefile
index ffa531c..4a76187 100644
--- a/Makefile
+++ b/Makefile
@@ -27,6 +27,7 @@ SRC= main.ml \
abstract/varenv.ml \
abstract/abs_interp.ml \
abstract/abs_interp_edd.ml \
+ abstract/abs_interp_dynpart.ml \
interpret/interpret.ml \
all: $(BIN)
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
new file mode 100644
index 0000000..28f9238
--- /dev/null
+++ b/abstract/abs_interp_dynpart.ml
@@ -0,0 +1,375 @@
+open Ast
+open Ast_util
+open Formula
+open Typing
+open Cmdline
+
+open Util
+open Num_domain
+open Enum_domain
+
+open Varenv
+
+module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN)
+: sig
+
+ val do_prog : cmdline_opt -> rooted_prog -> unit
+
+end = struct
+
+ type abs_v = ED.t * ND.t
+
+ type location = {
+ id : int;
+
+ def : bool_expr list; (* conjunction of formula *)
+ def_cl : conslist;
+ is_init : bool;
+
+ f : bool_expr;
+ cl : conslist;
+
+ (* For chaotic iteration fixpoint *)
+ mutable star : bool;
+ mutable in_c : int;
+ mutable v : abs_v;
+
+ mutable out_t : int list;
+ mutable in_t : int list;
+ }
+
+ type env = {
+ rp : rooted_prog;
+ opt : cmdline_opt;
+
+ ve : varenv;
+
+ (* program expressions *)
+ f : bool_expr;
+ guarantees : (id * bool_expr) list;
+
+ (* data *)
+ loc : (int, location) Hashtbl.t;
+ counter : int ref;
+ }
+
+ (* **************************
+ ABSTRACT VALUES
+ ************************** *)
+
+ (*
+ top : env -> abs_v
+ bottom : env -> abs_v
+ *)
+ let top e = (ED.top e.ve.evars, ND.top e.ve.nvars)
+ let bottom e = (ED.top e.ve.evars, ND.bottom e.ve.nvars)
+ let is_bot (e, n) = ND.is_bot n
+
+ let print_v fmt (enum, num) =
+ if is_bot (enum, num) then
+ Format.fprintf fmt "⊥"
+ else
+ Format.fprintf fmt "@[<hov 4>(%a,@ %a)@]" ED.print enum ND.print num
+
+ (*
+ join : abs_v -> abs_v -> abs_v
+ meet : abs_v -> abs_v -> abs_v
+ *)
+ let join (e1, n1) (e2, n2) =
+ if is_bot (e1, n1) then (e2, n2)
+ else if is_bot (e2, n2) then (e1, n1)
+ else (ED.join e1 e2, ND.join n1 n2)
+ let meet (e1, n1) (e2, n2) =
+ if is_bot (e1, n1) then ED.vtop e1, ND.vbottom n1
+ else if is_bot (e2, n2) then ED.vtop e2, ND.vbottom n2
+ else
+ try (ED.meet e1 e2 , ND.meet n1 n2)
+ with Bot -> e1, ND.vbottom n1
+
+ (*
+ apply_cl : abs_v -> conslist -> abs_v
+ *)
+ let rec apply_cl (enum, num) (ec, nc, r) =
+ try
+ begin match r with
+ | CLTrue ->
+ (ED.apply_cl enum ec, ND.apply_cl num nc)
+ | CLFalse ->
+ (enum, ND.vbottom num)
+ | CLAnd(a, b) ->
+ let enum, num = apply_cl (enum, num) (ec, nc, a) in
+ let enum, num = apply_cl (enum, num) ([], nc, b) in
+ enum, num
+ | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+ let a = apply_cl (enum, num) (ec@eca, nc@nca, ra) in
+ let b = apply_cl (enum, num) (ec@ecb, nc@ncb, rb) in
+ join a b
+ end
+ with Bot -> ED.vtop enum, ND.vbottom num
+
+
+ (* ***************************
+ INTERPRET
+ *************************** *)
+
+
+
+ (*
+ init_env : cmdline_opt -> rooted_prog -> env
+ *)
+ let init_env opt rp =
+ let f = Transform.f_of_prog_incl_init rp false in
+
+ let f = simplify_k (get_root_true f) f in
+ Format.printf "Complete formula:@.%a@.@." Formula_printer.print_expr f;
+
+ let facts = get_root_true f in
+ let f, rp, _ = List.fold_left
+ (fun (f, (rp : rooted_prog), repls) eq ->
+ match eq with
+ | BEnumCons(E_EQ, a, EIdent b)
+ when a.[0] <> 'L' && b.[0] <> 'L' ->
+
+ let a = try List.assoc a repls with Not_found -> a in
+ let b = try List.assoc b repls with Not_found -> b in
+
+ if a = b then
+ f, rp, repls
+ else begin
+ let keep, repl =
+ if String.length a <= String.length b
+ then a, b
+ else b, a
+ in
+ Format.printf "Replacing %s with %s@." repl keep;
+ let f = formula_replace_evars [repl, keep; "L"^repl, "L"^keep] f in
+ let rp =
+ { rp with all_vars =
+ List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in
+ let repls = (repl, keep)::
+ (List.map (fun (r, k) -> r, if k = repl then keep else k) repls) in
+ f, rp, repls
+ end
+ | _ -> f, rp, repls)
+ (f, rp, []) facts in
+
+ let f = simplify_k (get_root_true f) f in
+
+ Format.printf "Complete formula after simpl:@.%a@.@."
+ Formula_printer.print_expr f;
+
+ let guarantees = Transform.guarantees_of_prog rp in
+ Format.printf "Guarantees:@.";
+ List.iter (fun (id, f) ->
+ Format.printf " %s: %a@." id Formula_printer.print_expr f)
+ guarantees;
+ Format.printf "@.";
+
+ let ve = mk_varenv rp f (conslist_of_f f) in
+
+ let env = {
+ rp; opt; ve; f; guarantees;
+ loc = Hashtbl.create 2; counter = ref 2; } in
+
+ (* add initial disjunction : L/must_reset = tt, L/must_reset ≠ tt *)
+ let rstc = [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] in
+ let rstf = simplify_k rstc f in
+ let rstf = simplify_k (get_root_true rstf) rstf in
+ let nrstc = [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] in
+ let nrstf = simplify_k nrstc f in
+ let nrstf = simplify_k (get_root_true nrstf) nrstf in
+ Hashtbl.add env.loc 0
+ {
+ id = 0;
+ def = rstc;
+ def_cl = conslist_of_f (f_and_list rstc);
+ is_init = true;
+
+ f = rstf;
+ cl = conslist_of_f rstf;
+
+ star = false;
+ in_c = 0;
+ v = (ED.top ve.evars, ND.bottom ve.nvars);
+
+ out_t = [];
+ in_t = [];
+ };
+ Hashtbl.add env.loc 1
+ {
+ id = 1;
+ def = nrstc;
+ def_cl = conslist_of_f (f_and_list nrstc);
+ is_init = false;
+
+ f = nrstf;
+ cl = conslist_of_f nrstf;
+
+ star = false;
+ in_c = 0;
+ v = (ED.top ve.evars, ND.bottom ve.nvars);
+
+ out_t = [];
+ in_t = [];
+ };
+ env
+
+
+ (*
+ pass_cycle : env -> edd_v -> edd_v
+ unpass_cycle : env -> edd_v -> edd_v
+
+ set_target_case : env -> edd_v -> bool_expr -> edd_v
+ cycle : env -> edd_v -> conslist -> edd_v
+ *)
+ let pass_cycle env (enum, num) =
+ let assign_e, assign_n = List.fold_left
+ (fun (ae, an) (a, b, t) -> match t with
+ | TEnum _ -> (a, b)::ae, an
+ | TInt | TReal -> ae, (a, NIdent b)::an)
+ ([], []) env.cycle in
+
+ let enum = ED.assign enum assign_e in
+ let num = ND.assign num assign_n in
+
+ let ef, nf = List.fold_left
+ (fun (ef, nf) (var, t) -> match t with
+ | TEnum _ -> var::ef, nf
+ | TReal | TInt -> ef, var::nf)
+ ([], []) env.forget in
+
+ (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
+
+ let unpass_cycle env (enum, num) =
+ let assign_e, assign_n = List.fold_left
+ (fun (ae, an) (a, b, t) -> match t with
+ | TEnum _ -> (b, a)::ae, an
+ | TInt | TReal -> ae, (b, NIdent a)::an)
+ ([], []) env.ve.cycle in
+
+ let enum = ED.assign enum assign_e in
+ let num = ND.assign num assign_n in
+
+ let ef, nf = List.fold_left
+ (fun (ef, nf) (var, t) -> match t with
+ | TEnum _ -> var::ef, nf
+ | TReal | TInt -> ef, var::nf)
+ ([], []) env.ve.forget_inv in
+
+ (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
+
+ let set_target_case e v cl =
+ let tgt = (unpass_cycle e (apply_cl (top e) cl)) in
+ (*Format.printf "Target %a = %a@." Formula_printer.print_conslist cl print_v tgt;*)
+ meet v tgt
+
+ (*
+ chaotic_iter : env -> unit
+
+ Fills the values of loc[*].v, and updates out_t and in_t
+ *)
+ let chaotic_iter e =
+ let delta = ref [] in
+
+ (* Fill up initial states *)
+ Hashtbl.iter
+ (fun q loc ->
+ loc.out_t <- [];
+ loc.in_t <- [];
+ if loc.is_init then begin
+ loc.v <- apply_cl (top e) loc.cl;
+ delta := q::!delta
+ end else
+ loc.v <- bottom e)
+ e.loc;
+
+ (* Iterate *)
+ let it_counter = ref 0 in
+ while !delta <> [] do
+ let s = List.hd !delta in
+ let loc = Hashtbl.find e.loc s in
+
+ incr it_counter;
+ Format.printf "@.Iteration %d: q%d@." !it_counter s;
+
+ let start = loc.v in
+ let f i =
+ (*Format.printf "I: %a@." print_v i;*)
+ let i' = set_target_case e i loc.def_cl in
+ (*Format.printf "I': %a@." print_v i';*)
+ let j = join start (apply_cl (apply_cl (pass_cycle e.ve i') loc.def_cl) loc.cl) in
+ (*Format.printf "J: %a@." print_v j;*)
+ j
+ in
+
+ let rec iter n (i_enum, i_num) =
+ let fi_enum, fi_num = f (i_enum, i_num) in
+ let j_enum, j_num =
+ if ND.is_bot fi_num then
+ i_enum, i_num
+ else
+ if n < e.opt.widen_delay then
+ ED.join i_enum fi_enum, ND.join i_num fi_num
+ else
+ ED.join i_enum fi_enum, ND.widen i_num fi_num
+ in
+ if ED.eq j_enum i_enum && ND.eq j_num i_num
+ then (i_enum, i_num)
+ else iter (n+1) (j_enum, j_num)
+ in
+ let y = iter 0 start in
+ let z = fix (fun (a, b) (c, d) -> ED.eq a c && ND.eq b d) f y in
+ Format.printf "Fixpoint: %a@." print_v z;
+
+ loc.v <- z;
+
+ Hashtbl.iter
+ (fun t loc2 ->
+ let u = pass_cycle e.ve z in
+ let v = apply_cl u loc2.def_cl in
+ let w = apply_cl v loc2.cl in
+ (*Format.printf "u: %a@.v: %a@. w: %a@." print_v u print_v v print_v w;*)
+ let r_enum, r_num = w in
+ if not (is_bot (r_enum, r_num)) then begin
+ Format.printf "%d -> %d with:@. %a@." s t print_v (r_enum, r_num);
+ if not (List.mem s loc2.in_t)
+ then loc2.in_t <- s::loc2.in_t;
+ if not (List.mem t loc.out_t)
+ then loc.out_t <- t::loc.out_t;
+ let enum, num = loc2.v in
+ let enum2, num2 = join (enum, num) (r_enum, r_num) in
+ if not (ED.subset enum2 enum) || not (ND.subset num2 num) then
+ begin
+ loc2.v <- (enum2, num2);
+ if not (List.mem t !delta)
+ then delta := t::!delta
+ end
+ end)
+ e.loc;
+
+ delta := List.filter ((<>) s) !delta;
+ done
+
+
+ let print_locs e =
+ Hashtbl.iter
+ (fun id loc ->
+ Format.printf "@.";
+ Format.printf "q%d: @[<hov 4>[ %a ]@]@." id
+ (print_list Formula_printer.print_expr " ∧ ") loc.def;
+ (*Format.printf "F: %a@." Formula_printer.print_conslist loc.cl;*)
+ Format.printf " @[<hv 0>%a ∧@ %a@]@."
+ ED.print (fst loc.v) ND.print (snd loc.v);
+ Format.printf " -> @[<hov>[%a]@]@."
+ (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
+ )
+ e.loc
+
+ let do_prog opt rp =
+ let e = init_env opt rp in
+
+ Format.printf "@.Initializing.@.";
+ chaotic_iter e;
+ print_locs e
+
+end
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index a439995..23d4734 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -557,7 +557,8 @@ end = struct
last_vars = [];
all_vars = [];
cycle = [];
- forget = []; } in
+ forget = [];
+ forget_inv = []; } in
Hashtbl.add ve.ev_order "x" 0;
Hashtbl.add ve.ev_order "y" 1;
Hashtbl.add ve.ev_order "z" 2;
@@ -755,13 +756,10 @@ end = struct
let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in
let ef, nf = List.fold_left
- (fun (ef, nf) (_, var, t) ->
- if var.[0] <> 'N' then
- match t with
- | TEnum _ -> var::ef, nf
- | TReal | TInt -> ef, var::nf
- else ef, nf)
- ([], []) env.rp.all_vars in
+ (fun (ef, nf) (var, t) -> match t with
+ | TEnum _ -> var::ef, nf
+ | TReal | TInt -> ef, var::nf)
+ ([], []) env.ve.forget_inv in
let v = edd_forget_vars v ef in
edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
@@ -779,8 +777,9 @@ end = struct
(* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *)
(* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *)
+ (* WHY THE **** AM I SHOUTING LIKE THAT ? *)
let facts = get_root_true f in
- let f, rp, _ = List.fold_left
+ let f, rp, repls = List.fold_left
(fun (f, (rp : rooted_prog), repls) eq ->
match eq with
| BEnumCons(E_EQ, a, EIdent b)
@@ -802,8 +801,12 @@ end = struct
let rp =
{ rp with all_vars =
List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in
- let repls = (repl, keep)::
- (List.map (fun (r, k) -> r, if k = repl then keep else k) repls) in
+ let repls = (repl, keep; "L"^repl, "L"^keep)::
+ (List.map
+ (fun (r, k) -> r,
+ if k = repl then keep else
+ if k = "L"^repl then "L"^keep else k)
+ repls) in
f, rp, repls
end
| _ -> f, rp, repls)
@@ -825,6 +828,9 @@ end = struct
Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
let guarantees = Transform.guarantees_of_prog rp in
+ let guarantees = List.map
+ (fun (id, f) -> id, formula_replace_evars repls f)
+ guarantees in
Format.printf "Guarantees:@.";
List.iter (fun (id, f) ->
Format.printf " %s: %a@." id Formula_printer.print_expr f)
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index ea2b053..4f6aacd 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -11,11 +11,15 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig
(* construction *)
val top : (id * item list) list -> t
+ val bottom : (id * item list) list -> t
+ val vtop : t -> t (* top with same vars *)
+ 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 *)
@@ -27,6 +31,7 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig
(* abstract operations *)
val apply_cons : t -> enum_cons -> t list (* may disjunct *)
+ val apply_cl : t -> enum_cons list -> t (* join any disjunction ; may raise Bot *)
val assign : t -> (id * id) list -> t
(* pretty-printing *)
@@ -47,11 +52,15 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
}
let top vars = { vars; value = VarMap.empty }
+ let vtop x = { x with value = VarMap.empty }
+ let bottom vars = raise Bot (* we don't represent Bot *)
+ let is_bot x = false
let vars x = x.vars
let forgetvar x id =
{ x with value = VarMap.remove id x.value }
+ let forgetvars = List.fold_left forgetvar
let project x id =
try [VarMap.find id x.value]
with Not_found -> List.assoc id x.vars
@@ -108,7 +117,14 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
(List.filter (cc op s) (List.assoc id2 x.vars))
| Some s, Some t ->
if cc op s t then [x] else []
-
+
+ let apply_cl x l =
+ List.fold_left
+ (fun k c -> match apply_cons k c with
+ | [] -> raise Bot
+ | p::q -> List.fold_left join p q )
+ x l
+
let assign x idl =
let v = List.fold_left
(fun v (id, id2) ->
@@ -163,11 +179,15 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
let uniq x = uniq_sorted (sort x)
let top vars = { vars; value = VarMap.empty }
+ let vtop x = { x with value = VarMap.empty }
+ let bottom vars = raise Bot (* we don't represent Bot *)
+ let is_bot x = false
let vars x = x.vars
let forgetvar x id =
{ x with value = VarMap.remove id x.value }
+ let forgetvars = List.fold_left forgetvar
let project x id =
try VarMap.find id x.value
with Not_found -> List.assoc id x.vars
@@ -220,6 +240,13 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
| [] -> l
| _ -> { x with value = VarMap.add id2 v2 x.value }::l)
[] v1
+
+ let apply_cl x l =
+ List.fold_left
+ (fun k c -> match apply_cons k c with
+ | [] -> raise Bot
+ | p::q -> List.fold_left join p q )
+ x l
let assign x idl =
let v = List.fold_left
diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
index 47515eb..ae71b09 100644
--- a/abstract/enum_domain_edd.ml
+++ b/abstract/enum_domain_edd.ml
@@ -1,41 +1,10 @@
open Ast
open Formula
open Util
+open Enum_domain
-module type ENUM_ENVIRONMENT_DOMAIN2 = sig
- type t
- type item = string
-
- (* construction *)
- val top : (id * item list) list -> t
- val bottom : (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
+module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
exception Top
type item = string
@@ -173,6 +142,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct
let bottom vars = let t = top vars in { t with root = DBot }
+ let vtop x = { x with root = DTop }
+
(*
is_bot : t -> bool
*)
@@ -284,7 +255,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct
apply_cl : t -> enum_cons list -> t
*)
let apply_cons v x =
- meet v (of_cons v x)
+ let v = meet v (of_cons v x) in
+ if v.root = DBot then [] else [v]
let apply_cl v ec =
let rec cl_k = function
diff --git a/abstract/varenv.ml b/abstract/varenv.ml
index 8bd3971..450bef3 100644
--- a/abstract/varenv.ml
+++ b/abstract/varenv.ml
@@ -20,6 +20,7 @@ type varenv = {
cycle : (id * id * typ) list; (* s'(x) = s(y) *)
forget : (id * typ) list; (* s'(x) not specified *)
+ forget_inv : (id * typ) list;
}
@@ -267,7 +268,12 @@ let mk_varenv (rp : rooted_prog) f cl =
[] last_vars
in
let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
+ let forget_inv = List.map (fun (_, id, ty) -> (id, ty))
+ (List.filter
+ (fun (_, id, _) ->
+ not (List.exists (fun (_, b, _) -> b = id) cycle))
+ all_vars) in
{ evars = enum_vars; nvars = num_vars; ev_order;
- last_vars; all_vars; cycle; forget }
+ last_vars; all_vars; cycle; forget; forget_inv }
diff --git a/main.ml b/main.ml
index e114554..339a433 100644
--- a/main.ml
+++ b/main.ml
@@ -7,6 +7,7 @@ open Nonrelational
open Apron_domain
open Enum_domain_edd
+open Abs_interp_dynpart
module Interpret = Interpret.I
@@ -18,6 +19,9 @@ module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND)
module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND)
+module AI_S_Itv_DP = Abs_interp_dynpart.I
+ (Enum_domain.MultiValuation)(ItvND)
+
(* command line options *)
let times = ref false
let dump = ref false
@@ -28,6 +32,7 @@ let ai_itv = ref false
let ai_rel = ref false
let ai_itv_edd = ref false
let ai_rel_edd = ref false
+let ai_s_itv_dp = ref false
let ai_root = ref "test"
let ai_widen_delay = ref 5
let ai_no_time_scopes = ref "all"
@@ -40,22 +45,35 @@ let ifile = ref ""
let usage = "usage: analyzer [options] file.scade"
let options = [
- "--exec-times", Arg.Set times, "Show time spent in each function of the analyzer, for some functions";
+ "--exec-times", Arg.Set times,
+ "Show time spent in each function of the analyzer, for some functions";
"--dump", Arg.Set dump, "Dump program source.";
"--dump-rn", Arg.Set dumprn, "Dump program source, after renaming.";
"--vtest", Arg.Set vtest, "Verbose testing (direct interpret).";
"--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-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-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)";
- "--ai-vvci", Arg.Set ai_vvci, "Very verbose chaotic iterations (show everything all the time)";
- "--wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3).";
- "--root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test).";
- "--no-time", Arg.Set_string ai_no_time_scopes, "Scopes for which not to introduce a 'time' variable in analysis.";
- "--disj", Arg.Set_string ai_disj_v, "Variables for which to introduce a disjunction.";
- "--init", Arg.Set_string ai_init_scopes, "Scopes for which to introduce a 'init' variable in analysis.";
+ "--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-s-itv-dp", Arg.Set ai_s_itv_dp,
+ "Do abstract analysis using dynamic partitionning method, "^
+ "with intervals and valuation domain for enums.";
+ "--ai-vci", Arg.Set ai_vci,
+ "Verbose chaotic iterations (show state at each iteration)";
+ "--ai-vvci", Arg.Set ai_vvci,
+ "Very verbose chaotic iterations (show everything all the time)";
+ "--wd", Arg.Set_int ai_widen_delay,
+ "Widening delay in abstract analysis of loops (default: 3).";
+ "--root", Arg.Set_string ai_root,
+ "Root node for abstract analysis (default: test).";
+ "--no-time", Arg.Set_string ai_no_time_scopes,
+ "Scopes for which not to introduce a 'time' variable in analysis.";
+ "--disj", Arg.Set_string ai_disj_v,
+ "Variables for which to introduce a disjunction.";
+ "--init", Arg.Set_string ai_init_scopes,
+ "Scopes for which to introduce a 'init' variable in analysis.";
]
let do_test_interpret prog verbose =
@@ -106,7 +124,10 @@ 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 then begin
+ if !ai_itv || !ai_rel
+ || !ai_itv_edd || !ai_rel_edd
+ || !ai_s_itv_dp then
+ begin
let comma_split = Str.split (Str.regexp ",") in
let select_f x =
if x = "all" then
@@ -138,6 +159,8 @@ let () =
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_s_itv_dp then AI_S_Itv_DP.do_prog opt rp;
end;
if !vtest then do_test_interpret prog true
diff --git a/tests/source/two_counters.scade b/tests/source/two_counters.scade
index 7970aab..6468523 100644
--- a/tests/source/two_counters.scade
+++ b/tests/source/two_counters.scade
@@ -1,5 +1,5 @@
-const n1: int = 10;
-const n2: int = 6;
+const n1: int = 100;
+const n2: int = 60;
node top(a,b,c : bool) returns (ok, r1, r2 : bool)
@@ -7,12 +7,12 @@ var
x, y, pre_x, pre_y: int;
o1, o2: bool;
- m: bool;
+ m, n, lb: bool;
let
x = if (b or c) then 0 else (if (a and pre_x < n1) then pre_x + 1 else pre_x);
y = if (c) then 0 else (if (a and pre_y < n2) then pre_y + 1 else pre_y);
- o1= x = n1;
- o2= y = n2;
+ o1= x >= n1;
+ o2= y >= n2;
ok= if o1 then o2 else true;
r1 = 0<=x and x<=n1;
r2 = 0<=y and y<=n2;
@@ -20,6 +20,8 @@ let
pre_y = 0 -> pre(y);
m = true -> pre o2;
+ n = true -> pre o1;
+ lb = true -> pre b;
guarantee g1: ok;
guarantee g2: r1;