summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-07 17:41:06 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-07 17:41:06 +0200
commit9ccef2c0850b73bf3d92f26bfa0aeacf933e1d17 (patch)
tree0c8b4157db1cb8851d75dae6f8706103ba081091
parent73fa920959d22c084265fe847f4788564bf49700 (diff)
downloadSemVerif-Projet-9ccef2c0850b73bf3d92f26bfa0aeacf933e1d17.tar.gz
SemVerif-Projet-9ccef2c0850b73bf3d92f26bfa0aeacf933e1d17.zip
Restart anew ; done nonrelational stuff, interpret remains, intervals domain remains
-rw-r--r--Makefile9
-rw-r--r--abstract/_constant_domain.ml153
-rw-r--r--abstract/_domain.ml (renamed from abstract/domain.ml)0
-rw-r--r--abstract/constant_domain.ml206
-rw-r--r--abstract/environment_domain.ml27
-rw-r--r--abstract/interpret.ml57
-rw-r--r--abstract/nonrelational.ml103
-rw-r--r--abstract/value_domain.ml28
-rw-r--r--libs/util.ml1
-rw-r--r--main.ml11
10 files changed, 434 insertions, 161 deletions
diff --git a/Makefile b/Makefile
index 0f09d87..51d9995 100644
--- a/Makefile
+++ b/Makefile
@@ -3,9 +3,16 @@
BIN=analyze
SRCDIRS=libs,frontend,abstract
+SRC= main.ml \
+ abstract/constant_domain.ml \
+ abstract/environment_domain.ml \
+ abstract/interpret.ml \
+ abstract/nonrelational.ml \
+ abstract/value_domain.ml \
+
all: $(BIN)
-$(BIN): main.ml abstract/domain.ml abstract/constant_domain.ml
+$(BIN): $(SRC)
ocamlbuild -Is $(SRCDIRS) -cflags '-I /usr/lib/ocaml/zarith' -lflags '-I /usr/lib/ocaml/zarith zarith.cmxa' main.native
mv main.native $(BIN)
diff --git a/abstract/_constant_domain.ml b/abstract/_constant_domain.ml
new file mode 100644
index 0000000..544d2e9
--- /dev/null
+++ b/abstract/_constant_domain.ml
@@ -0,0 +1,153 @@
+open Util
+open Abstract_syntax_tree
+
+module CD : Domain.S =
+ struct
+
+ exception DivideByZero
+ exception TypeError
+ exception Bot
+ exception NotImplemented
+
+ type tv = (* type for a variable *)
+ | Top
+ | I of Z.t
+
+ type ts = (* type for an environment *)
+ | Bot
+ | Nb of tv VarMap.t
+
+ let top_ts = Nb VarMap.empty
+
+ let ts_union a b =
+ begin match a, b with
+ | Bot, Bot -> Bot
+ | Nb a, Bot -> Nb a
+ | Bot, Nb b -> Nb b
+ | Nb a, Nb b ->
+ Nb
+ (VarMap.fold
+ (fun var value a ->
+ try match VarMap.find var a with
+ | Top -> a
+ | I x ->
+ match value with
+ | I y when y = x -> a
+ | _ -> VarMap.add var Top a
+ with
+ | Not_found -> VarMap.add var value a)
+ b a)
+ end
+
+ (* must not raise exception *)
+ let ts_add_bool_constraint expr (s : ts) =
+ s (* TODO, not necessary... *)
+
+
+ (* only evaluates numerical statements, raises
+ TypeError when result is bool *)
+ let rec eval_abs expr (s : tv VarMap.t) =
+ match expr with
+ | AST_unary(op, (i, _)) ->
+ begin match eval_abs i s with
+ | Top -> Top
+ | I x ->
+ match op with
+ | AST_UNARY_PLUS -> I x
+ | AST_UNARY_MINUS -> I (Z.neg x)
+ | _ -> raise TypeError
+ end
+ | AST_binary(op, (a, _), (b, _)) ->
+ begin match eval_abs a s, eval_abs b s with
+ | I x, I y ->
+ begin match op with
+ | AST_PLUS -> I (Z.add x y)
+ | AST_MINUS -> I (Z.sub x y)
+ | AST_MULTIPLY -> I (Z.mul x y)
+ | AST_DIVIDE ->
+ if y = Z.zero then raise DivideByZero;
+ I (Z.div x y)
+ | AST_MODULO ->
+ if y = Z.zero then raise DivideByZero;
+ I (Z.rem x y)
+ | _ -> raise TypeError
+ end
+ | _ -> Top
+ end
+ | AST_identifier(id, _) ->
+ begin
+ try VarMap.find id s
+ with _ -> Top
+ end
+ | AST_int_const(s, _) ->
+ I (Z.of_string s)
+ | AST_bool_const(_) -> raise TypeError
+ | AST_int_rand _ -> Top
+ | _ -> raise NotImplemented (* extensions *)
+
+ (* returns true if the expression can evaluate to true
+ returns false if the expression always evaluates to false *)
+ let rec eval_bool_abs expr (s : tv VarMap.t) =
+ true (* TODO *)
+
+ (* must not raise exception *)
+ let rec interp_abs stat s =
+ begin match s with
+ | Bot -> Bot
+ | Nb vars ->
+ begin match stat with
+ | AST_block b ->
+ List.fold_left
+ (fun ss (st, _) -> interp_abs st ss)
+ s b
+ | AST_assign ((id, _), (exp, _)) ->
+ begin
+ try
+ let value = eval_abs exp vars in
+ Nb (VarMap.add id value vars)
+ with _ -> Bot
+ end
+ | AST_if ((cond, _), (tb, _), None) ->
+ ts_union (Nb vars)
+ (interp_abs tb
+ (ts_add_bool_constraint cond (Nb vars)))
+ | AST_if ((cond, l), (tb, _), Some (eb, _)) ->
+ ts_union
+ (interp_abs tb
+ (ts_add_bool_constraint cond (Nb vars)))
+ (interp_abs eb
+ (ts_add_bool_constraint
+ (AST_unary (AST_NOT, (cond, l)))
+ (Nb vars)))
+ | AST_while ((cond, _), (body, _)) ->
+ let f s =
+ ts_union
+ s
+ (ts_add_bool_constraint cond s)
+ in
+ fix f (Nb vars)
+ | AST_HALT -> Bot
+ | AST_assert (cond, _) ->
+ if eval_bool_abs cond vars
+ then Nb vars
+ else begin
+ print_string "Assert fail\n";
+ Bot
+ end
+ | AST_print items ->
+ List.iter
+ (fun (var, _) ->
+ print_string (var ^ " = ");
+ try
+ match VarMap.find var vars with
+ | Top -> print_string "T\n"
+ | I x -> print_string (Z.to_string x ^ "\n")
+ with _ -> print_string "T\n")
+ items;
+ Nb vars
+ | _ -> raise NotImplemented (* extensions *)
+ end
+ end
+
+ end
+
diff --git a/abstract/domain.ml b/abstract/_domain.ml
index 643a6ec..643a6ec 100644
--- a/abstract/domain.ml
+++ b/abstract/_domain.ml
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml
index 544d2e9..4bd5cf2 100644
--- a/abstract/constant_domain.ml
+++ b/abstract/constant_domain.ml
@@ -1,153 +1,53 @@
-open Util
-open Abstract_syntax_tree
-
-module CD : Domain.S =
- struct
-
- exception DivideByZero
- exception TypeError
- exception Bot
- exception NotImplemented
-
- type tv = (* type for a variable *)
- | Top
- | I of Z.t
-
- type ts = (* type for an environment *)
- | Bot
- | Nb of tv VarMap.t
-
- let top_ts = Nb VarMap.empty
-
- let ts_union a b =
- begin match a, b with
- | Bot, Bot -> Bot
- | Nb a, Bot -> Nb a
- | Bot, Nb b -> Nb b
- | Nb a, Nb b ->
- Nb
- (VarMap.fold
- (fun var value a ->
- try match VarMap.find var a with
- | Top -> a
- | I x ->
- match value with
- | I y when y = x -> a
- | _ -> VarMap.add var Top a
- with
- | Not_found -> VarMap.add var value a)
- b a)
- end
-
- (* must not raise exception *)
- let ts_add_bool_constraint expr (s : ts) =
- s (* TODO, not necessary... *)
-
-
- (* only evaluates numerical statements, raises
- TypeError when result is bool *)
- let rec eval_abs expr (s : tv VarMap.t) =
- match expr with
- | AST_unary(op, (i, _)) ->
- begin match eval_abs i s with
- | Top -> Top
- | I x ->
- match op with
- | AST_UNARY_PLUS -> I x
- | AST_UNARY_MINUS -> I (Z.neg x)
- | _ -> raise TypeError
- end
- | AST_binary(op, (a, _), (b, _)) ->
- begin match eval_abs a s, eval_abs b s with
- | I x, I y ->
- begin match op with
- | AST_PLUS -> I (Z.add x y)
- | AST_MINUS -> I (Z.sub x y)
- | AST_MULTIPLY -> I (Z.mul x y)
- | AST_DIVIDE ->
- if y = Z.zero then raise DivideByZero;
- I (Z.div x y)
- | AST_MODULO ->
- if y = Z.zero then raise DivideByZero;
- I (Z.rem x y)
- | _ -> raise TypeError
- end
- | _ -> Top
- end
- | AST_identifier(id, _) ->
- begin
- try VarMap.find id s
- with _ -> Top
- end
- | AST_int_const(s, _) ->
- I (Z.of_string s)
- | AST_bool_const(_) -> raise TypeError
- | AST_int_rand _ -> Top
- | _ -> raise NotImplemented (* extensions *)
-
- (* returns true if the expression can evaluate to true
- returns false if the expression always evaluates to false *)
- let rec eval_bool_abs expr (s : tv VarMap.t) =
- true (* TODO *)
-
- (* must not raise exception *)
- let rec interp_abs stat s =
- begin match s with
- | Bot -> Bot
- | Nb vars ->
- begin match stat with
- | AST_block b ->
- List.fold_left
- (fun ss (st, _) -> interp_abs st ss)
- s b
- | AST_assign ((id, _), (exp, _)) ->
- begin
- try
- let value = eval_abs exp vars in
- Nb (VarMap.add id value vars)
- with _ -> Bot
- end
- | AST_if ((cond, _), (tb, _), None) ->
- ts_union (Nb vars)
- (interp_abs tb
- (ts_add_bool_constraint cond (Nb vars)))
- | AST_if ((cond, l), (tb, _), Some (eb, _)) ->
- ts_union
- (interp_abs tb
- (ts_add_bool_constraint cond (Nb vars)))
- (interp_abs eb
- (ts_add_bool_constraint
- (AST_unary (AST_NOT, (cond, l)))
- (Nb vars)))
- | AST_while ((cond, _), (body, _)) ->
- let f s =
- ts_union
- s
- (ts_add_bool_constraint cond s)
- in
- fix f (Nb vars)
- | AST_HALT -> Bot
- | AST_assert (cond, _) ->
- if eval_bool_abs cond vars
- then Nb vars
- else begin
- print_string "Assert fail\n";
- Bot
- end
- | AST_print items ->
- List.iter
- (fun (var, _) ->
- print_string (var ^ " = ");
- try
- match VarMap.find var vars with
- | Top -> print_string "T\n"
- | I x -> print_string (Z.to_string x ^ "\n")
- with _ -> print_string "T\n")
- items;
- Nb vars
- | _ -> raise NotImplemented (* extensions *)
- end
- end
-
- end
-
+open Value_domain
+
+module Constants : VALUE_DOMAIN = struct
+ type t =
+ | Top
+ | Int of Z.t
+ | Bot
+
+ let top = Top
+ let bottom = Bot
+ let const i = Int i
+ let rand i j = if i <> j then Top else Int i
+
+ let subset a b = match a, b with
+ | _, Top -> true
+ | Bot, _ -> true
+ | Int a, Int b -> a = b
+ | _, _ -> false
+
+ let join a b = match a, b with
+ | Bot, x | x, Bot -> x
+ | Int a, Int b when a = b -> Int a
+ | _ -> Top
+
+ let meet a b = match a, b with
+ | Top, x | x, Top -> x
+ | Int a, Int b when a = b -> Int a
+ | _ -> Bot
+
+ let widen = meet (* pas besoin d'accélerer la convergence au-delà *)
+
+ let neg = function
+ | Int a -> Int (Z.neg a)
+ | x -> x
+
+ let b_aux op a b = match a, b with
+ | Int x, Int y -> Int (op x y)
+ | Bot, _ | _, Bot -> Bot
+ | _ -> Top
+ let add = b_aux Z.add
+ let sub = b_aux Z.sub
+ let mul = b_aux Z.mul
+ let div = b_aux Z.div
+ let rem = b_aux Z.rem
+
+ let leq a b =
+ match a, b with
+ | Int a, Int b when Z.leq a b ->
+ if Z.leq a b
+ then Int a, Int b
+ else Bot, Bot
+ | x, y -> x, y
+end
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
new file mode 100644
index 0000000..f5614fe
--- /dev/null
+++ b/abstract/environment_domain.ml
@@ -0,0 +1,27 @@
+open Abstract_syntax_tree
+
+module type ENVIRONMENT_DOMAIN = sig
+ type t
+
+ (* construction *)
+ val init : t
+ val bottom : t
+
+ (* variable management *)
+ val addvar : t -> id -> t
+ val rmvar : t -> id -> t
+
+ (* abstract operation *)
+ val assign : t -> id -> expr ext -> t (* S[id <- expr] *)
+ val compare : t -> expr ext -> expr ext -> t (* S[expr <= expr ?] *)
+
+ (* 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
+end
+
+
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
new file mode 100644
index 0000000..51c7cd6
--- /dev/null
+++ b/abstract/interpret.ml
@@ -0,0 +1,57 @@
+open Abstract_syntax_tree
+open Environment_domain
+open Util
+
+module Make (E : ENVIRONMENT_DOMAIN) = struct
+
+ let neg (e, l) =
+ (AST_unary(AST_NOT, (e, l))), l
+
+ let rec condition cond env =
+ begin match fst cond with
+ | AST_binary (AST_LESS_EQUAL, e1, e2) ->
+ E.compare env e1 e2
+ | AST_binary (AST_GREATER_EQUAL, e1, e2) ->
+ E.compare env e2 e1
+ | AST_binary (AST_AND, e1, e2) ->
+ 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 *)
+ end
+
+ let rec interp_stmt env stat =
+ begin match fst stat with
+ | AST_block b ->
+ List.fold_left interp_stmt env b
+ | AST_assign ((id, _), exp) ->
+ E.assign env id exp
+ | AST_if (cond, tb, None) ->
+ E.join
+ (interp_stmt (condition cond env) tb)
+ (condition (neg cond) env)
+ | AST_if (cond, tb, Some eb) ->
+ E.join
+ (interp_stmt (condition cond env) tb)
+ (interp_stmt (condition (neg cond) env) eb)
+ | AST_while (cond, (body, _)) ->
+ (* TODO *)
+ env
+ | AST_HALT -> E.bottom
+ | AST_assert (cond, l) ->
+ (* TODO *)
+ env
+ | AST_print items ->
+ (* TODO *)
+ env
+ | _ -> assert false (* not implemented *)
+ end
+
+ let interpret prog =
+ List.fold_left
+ (fun env x -> match x with
+ | AST_stat st -> interp_stmt env st
+ | _ -> env)
+ E.init
+ (fst prog)
+end
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
new file mode 100644
index 0000000..6e2ff2b
--- /dev/null
+++ b/abstract/nonrelational.ml
@@ -0,0 +1,103 @@
+open Abstract_syntax_tree
+open Util
+
+open Value_domain
+open Environment_domain
+
+
+module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
+ type env = V.t VarMap.t
+
+ type t = Env of env | Bot
+
+ let init = Env VarMap.empty
+ let bottom = Bot
+
+ let get_var env id =
+ try VarMap.find id env
+ with Not_found -> V.top
+
+
+ (* utilities *)
+
+ let rec eval env expr =
+ begin match fst expr with
+ | AST_identifier (id, _) -> get_var env id
+ | AST_int_const (s, _) -> V.const (Z.of_string s)
+ | AST_int_rand ((s, _), (t, _)) -> V.rand (Z.of_string s) (Z.of_string t)
+ | AST_unary (AST_UNARY_PLUS, e) -> eval env e
+ | AST_unary (AST_UNARY_MINUS, e) -> V.neg (eval env e)
+ | AST_unary (_, e) -> V.bottom
+ | AST_binary (op, e1, e2) ->
+ let f = match op with
+ | AST_PLUS -> V.add
+ | AST_MINUS -> V.sub
+ | AST_MULTIPLY -> V.mul
+ | AST_DIVIDE -> V.div
+ | AST_MODULO -> V.rem
+ | _ -> fun _ _ -> V.bottom
+ in f (eval env e1) (eval env e2)
+ | _ -> assert false (* unimplemented extension *)
+ end
+
+ let strict env = (* env -> t *)
+ if VarMap.exists (fun _ x -> x = V.bottom) env
+ then Bot
+ else Env env
+ let strict_apply f = function (* (env -> t) -> t -> t *)
+ | Bot -> Bot
+ | Env e -> match f e with
+ | Bot -> Bot
+ | Env e -> strict e
+
+ (* implementation *)
+
+ 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
+
+ let assign x id expr = strict_apply
+ (fun env -> Env (VarMap.add id (eval env expr) env))
+ x
+ let compare x e1 e2 =
+ strict_apply (fun env -> match fst e1, fst e2 with
+ | AST_identifier(a, _), AST_identifier(b, _) ->
+ let v1, v2 = get_var env a, get_var env b in
+ let v1', v2' = V.leq v1 v2 in
+ Env (VarMap.add a v1' (VarMap.add b v1' env))
+ | AST_identifier(a, _), AST_int_const(s, _) ->
+ let v1, v2 = get_var env a, V.const (Z.of_string s) in
+ let v1', _ = V.leq v1 v2 in
+ Env (VarMap.add a v1' env)
+ | AST_int_const(s, _), AST_identifier(b, _) ->
+ let v1, v2 = V.const (Z.of_string s), get_var env b in
+ let _, v2' = V.leq v1 v2 in
+ Env (VarMap.add b v2' env)
+ | _ -> Env env)
+ x
+
+ let join a b = match a, b with
+ | Bot, x | x, Bot -> x
+ | Env m, Env n ->
+ strict (VarMap.map2z (fun _ a b -> V.join a b) m n)
+
+ let meet a b = match a, b with
+ | Bot, _ | _, Bot -> Bot
+ | Env m, Env n ->
+ strict (VarMap.map2z (fun _ a b -> V.meet a b) m n)
+
+ let widen a b = match a, b with
+ | Bot, x | x, Bot -> x
+ | Env m, Env n ->
+ strict (VarMap.map2z (fun _ a b -> V.widen a b) m n)
+
+ let subset a b = match a, b with
+ | Bot, x -> true
+ | Env _, Bot -> false
+ | Env m, Env n ->
+ VarMap.for_all2o
+ (fun _ _ -> true)
+ (fun _ _ -> true)
+ (fun _ a b -> V.subset a b)
+ m n
+
+end
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
new file mode 100644
index 0000000..a0f082f
--- /dev/null
+++ b/abstract/value_domain.ml
@@ -0,0 +1,28 @@
+module type VALUE_DOMAIN = sig
+ type t
+
+ (* constructors *)
+ val top : t
+ val bottom : t
+ val const : Z.t -> t
+ val rand : Z.t -> Z.t -> t
+
+ (* order *)
+ val subset : t -> t -> bool
+
+ (* set-theoretic operations *)
+ val join : t -> t -> t (* union *)
+ val meet : t -> t -> t (* intersection *)
+ val widen : t -> t -> t
+
+ (* arithmetic operations *)
+ val neg : t -> t
+ val add : t -> t -> t
+ val sub : t -> t -> t
+ val mul : t -> t -> t
+ val div : t -> t -> t
+ val rem : t -> t -> t
+
+ (* boolean test *)
+ val leq : t -> t -> t * t (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *)
+end
diff --git a/libs/util.ml b/libs/util.ml
index b2838b6..17c1ad4 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -1,3 +1,4 @@
+exception TypeError
module VarMap = Mapext.Make(String)
diff --git a/main.ml b/main.ml
index 91ac4b1..e09ac0e 100644
--- a/main.ml
+++ b/main.ml
@@ -12,18 +12,15 @@
*)
open Abstract_syntax_tree
-open Constant_domain
+
+module Env_dom = Nonrelational.NonRelational(Constant_domain.Constants)
+module Interp = Interpret.Make(Env_dom)
(* parse and print filename *)
let doit filename =
let prog = File_parser.parse_file filename in
Abstract_syntax_printer.print_prog Format.std_formatter prog;
- List.fold_left
- (fun s x -> match x with
- | AST_stat(stat, _) -> CD.interp_abs(stat) s
- | _ -> s)
- CD.top_ts
- (fst prog)
+ Interp.interpret prog
(* parses arguments to get filename *)
let main () =