summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-07 19:04:38 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-07 19:04:38 +0200
commitd4ab85a1a6503cdbcb98c183c3357926d78da8a7 (patch)
treeb28ac764dd21ca7225ee46c6f4a4686648511fa3
parent9ccef2c0850b73bf3d92f26bfa0aeacf933e1d17 (diff)
downloadSemVerif-Projet-d4ab85a1a6503cdbcb98c183c3357926d78da8a7.tar.gz
SemVerif-Projet-d4ab85a1a6503cdbcb98c183c3357926d78da8a7.zip
implement assert, print
-rw-r--r--abstract/constant_domain.ml5
-rw-r--r--abstract/environment_domain.ml5
-rw-r--r--abstract/interpret.ml29
-rw-r--r--abstract/nonrelational.ml26
-rw-r--r--abstract/value_domain.ml3
5 files changed, 61 insertions, 7 deletions
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml
index 4bd5cf2..d142228 100644
--- a/abstract/constant_domain.ml
+++ b/abstract/constant_domain.ml
@@ -50,4 +50,9 @@ module Constants : VALUE_DOMAIN = struct
then Int a, Int b
else Bot, Bot
| x, y -> x, y
+
+ let to_string = function
+ | Bot -> "bot"
+ | Top -> "top"
+ | Int i -> "{" ^ (Z.to_string i) ^ "}"
end
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index f5614fe..254f755 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -6,6 +6,7 @@ module type ENVIRONMENT_DOMAIN = sig
(* construction *)
val init : t
val bottom : t
+ val is_bot : t -> bool
(* variable management *)
val addvar : t -> id -> t
@@ -22,6 +23,10 @@ module type ENVIRONMENT_DOMAIN = sig
(* order *)
val subset : t -> t -> bool
+
+ (* pretty-printing *)
+ val var_str : t -> id list -> string
+ val all_vars_str : t -> string
end
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index 51c7cd6..fe998a6 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -17,7 +17,14 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
E.meet (condition e1 env) (condition e2 env)
| AST_binary (AST_OR, e1, e2) ->
E.join (condition e1 env) (condition e2 env)
- | _ -> env (* TODO : encode some transformations *)
+ (* transformations *)
+ | AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) ->
+ condition
+ (AST_binary(AST_OR, neg e1, neg e2), x) env
+ | AST_unary (AST_NOT, (AST_binary(AST_OR, e1, e2), x)) ->
+ condition
+ (AST_binary(AST_AND, neg e1, neg e2), x) env
+ | _ -> env (* TODO : encode some more transformations *)
end
let rec interp_stmt env stat =
@@ -39,19 +46,31 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
env
| AST_HALT -> E.bottom
| AST_assert (cond, l) ->
- (* TODO *)
- env
+ if not
+ (E.is_bot (condition (neg (cond, l)) env))
+ then begin
+ print_string (Abstract_syntax_printer.string_of_extent l);
+ print_string ": ERROR: assertion failure\n"
+ end;
+ condition (cond, l) env
| AST_print items ->
- (* TODO *)
+ print_string (Abstract_syntax_printer.string_of_extent (snd stat));
+ print_string ": ";
+ print_string (E.var_str env (List.map fst items));
+ print_string "\n";
env
| _ -> assert false (* not implemented *)
end
let interpret prog =
- List.fold_left
+ let result = List.fold_left
(fun env x -> match x with
| AST_stat st -> interp_stmt env st
| _ -> env)
E.init
(fst prog)
+ in
+ print_string "Output: ";
+ print_string (E.all_vars_str result);
+ print_string "\n"
end
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 6e2ff2b..d4118da 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -16,8 +16,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
let get_var env id =
try VarMap.find id env
with Not_found -> V.top
-
-
+
(* utilities *)
let rec eval env expr =
@@ -52,6 +51,10 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
(* implementation *)
+ let is_bot env = match env with
+ | Bot -> true
+ | Env env -> strict env = Bot
+
let addvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x
let rmvar x id = strict_apply (fun y -> Env (VarMap.remove id y)) x
@@ -100,4 +103,23 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
(fun _ a b -> V.subset a b)
m n
+ (* pretty-printing *)
+ let var_str env vars =
+ match env with
+ | Bot -> "bot"
+ | Env env ->
+ let v = List.fold_left
+ (fun s id ->
+ (if s = "" then s else s ^ ", ") ^
+ id ^ " in " ^ (V.to_string (get_var env id))
+ )
+ ""
+ vars
+ in
+ "[ " ^ v ^ " ]"
+
+ let all_vars_str env =
+ match env with
+ | Bot -> "bot"
+ | Env map -> var_str env (List.map fst (VarMap.bindings map))
end
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
index a0f082f..9cf6d76 100644
--- a/abstract/value_domain.ml
+++ b/abstract/value_domain.ml
@@ -25,4 +25,7 @@ module type VALUE_DOMAIN = sig
(* boolean test *)
val leq : t -> t -> t * t (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *)
+
+ (* pretty-printing *)
+ val to_string : t -> string
end