summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-06-01 11:40:43 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-06-01 11:40:43 +0200
commitc4a24372b70180f23b7a56a81533e86ebb8509e7 (patch)
treed7a97ab4aa99d3d27331edb83f672398d030e41d
parent727354805f3c33d17bff18b74fc688b631e85f41 (diff)
downloadSemVerif-Projet-c4a24372b70180f23b7a56a81533e86ebb8509e7.tar.gz
SemVerif-Projet-c4a24372b70180f23b7a56a81533e86ebb8509e7.zip
Fix assertions ; fix environment equality test ; fix varialbe removal.HEADmaster
-rw-r--r--abstract/environment_domain.ml1
-rw-r--r--abstract/interpret.ml30
-rw-r--r--abstract/nonrelational.ml10
-rw-r--r--abstract/relational_apron.ml10
-rw-r--r--libs/util.ml6
5 files changed, 38 insertions, 19 deletions
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index 404548c..b2d18c4 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -25,6 +25,7 @@ module type ENVIRONMENT_DOMAIN = sig
(* order *)
val subset : t -> t -> bool
+ val eq : t -> t -> bool
(* pretty-printing *)
val var_str : t -> id list -> string
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index f6a6cb4..e28bf84 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -76,7 +76,8 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
| _ -> env
end
- let rec interp_stmt env stat =
+ let rec interp_stmt_a show_asserts env stat =
+ let interp_stmt = interp_stmt_a show_asserts in
begin match fst stat with
| AST_block b ->
(* remember to remove vars that have gone out of scope at the end *)
@@ -107,25 +108,30 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
let env, u_u = unroll env 3 in
(* widening *)
let widen_delay = 3 in
- let fsharp i =
- let next_step = interp_stmt (condition cond i) body in
+ let fsharp a i =
+ let next_step = interp_stmt_a a (condition cond i) body in
E.join env next_step
in
let rec iter n i =
let i' =
- (if n < widen_delay then E.join else E.widen)
- i
- (fsharp i)
+ if n < widen_delay
+ then E.join i (fsharp show_asserts i)
+ else E.widen i (fsharp false i)
in
- if i = i' then i else iter (n+1) i'
+ if E.eq i i' then i else iter (n+1) i'
in
let x = iter 0 env in
- let y = fix fsharp x in (* decreasing iteration *)
- E.join (condition (neg cond) y) u_u
+ let y = fix E.eq (fsharp false) x in (* decreasing iteration *)
+ let z =
+ if show_asserts then
+ (* last iteration : show real assert failures *)
+ fsharp true y
+ else y in
+ E.join (condition (neg cond) z) u_u
| AST_HALT -> bottom_with_vars (E.vars env)
| AST_assert cond ->
- if not
- (E.is_bot (condition (neg cond) env))
+ if show_asserts &&
+ not (E.is_bot (condition (neg cond) env))
then begin
Format.printf "%s: ERROR: assertion failure@."
(Abstract_syntax_printer.string_of_extent (snd stat));
@@ -147,6 +153,8 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
vars
| _ -> assert false (* not implemented *)
end
+
+ let interp_stmt = interp_stmt_a true
let interpret prog =
let result = List.fold_left
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 188c8bc..530b373 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -113,6 +113,16 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
(fun _ v -> v = V.top)
(fun _ a b -> V.subset a b)
m n
+
+ let eq a b = match a, b with
+ | Bot, Bot -> true
+ | Env m, Env n ->
+ VarMap.for_all2o
+ (fun _ _ -> false)
+ (fun _ _ -> false)
+ (fun _ a b -> a = b)
+ m n
+ | _ -> false
(* pretty-printing *)
let var_str env vars =
diff --git a/abstract/relational_apron.ml b/abstract/relational_apron.ml
index 926d2a9..4541b0e 100644
--- a/abstract/relational_apron.ml
+++ b/abstract/relational_apron.ml
@@ -59,9 +59,11 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
let env2 = 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 [| Var.of_string id |] in
- Abstract1.change_environment manager x env2 false
+ 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 =
List.map Var.to_string @@
Array.to_list @@ fst @@ Environment.vars @@ Abstract1.env x
@@ -98,13 +100,11 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
let widen = Abstract1.widening manager
let subset = Abstract1.is_leq manager
+ let eq = Abstract1.is_eq manager
let var_str x idl =
let prevars = vars x in
let rm_vars_l = List.filter (fun id -> not (List.mem id idl)) prevars in
- (* print_list "prevars" prevars;
- print_list "idl" idl;
- print_list "rm_vars_l" rm_vars_l; *)
let rm_vars = Array.of_list (List.map Var.of_string rm_vars_l) in
let xx = Abstract1.forget_array manager x rm_vars false in
let b = Buffer.create 80 in
diff --git a/libs/util.ml b/libs/util.ml
index b1fcdc4..30cf5bf 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -2,11 +2,11 @@ exception TypeError
module VarMap = Mapext.Make(String)
-let rec fix f s =
+let rec fix equal f s =
let fs = f s in
- if fs = s
+ if equal fs s
then fs
- else fix f fs
+ else fix equal f fs
let (@@) f x = f x