summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-21 18:07:37 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-21 18:07:37 +0200
commit77df0b0f119fc70624e4b830320a2b3e1034f7b5 (patch)
treeebac7e6c6bd653359181af16cc71192138161f47
parent4204d25a2d277af1c16f55ee488e42c7b79bba1f (diff)
downloadSemVerif-Projet-77df0b0f119fc70624e4b830320a2b3e1034f7b5.tar.gz
SemVerif-Projet-77df0b0f119fc70624e4b830320a2b3e1034f7b5.zip
Just retab (many lines changed for nothing)
-rw-r--r--abstract/constant_domain.ml128
-rw-r--r--abstract/environment_domain.ml42
-rw-r--r--abstract/interpret.ml228
-rw-r--r--abstract/intervals_domain.ml230
-rw-r--r--abstract/nonrelational.ml226
-rw-r--r--abstract/value_domain.ml46
-rw-r--r--main.ml37
7 files changed, 469 insertions, 468 deletions
diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml
index 44a13fc..abc3aa0 100644
--- a/abstract/constant_domain.ml
+++ b/abstract/constant_domain.ml
@@ -1,71 +1,71 @@
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 Bot else if i <> j then Top else Int i
+ 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 Bot else 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 = join (* pas besoin d'accélerer la convergence au-delà *)
+ 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 = join (* 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 a b = match a, b with
- | Int x, Int y -> Int (Z.mul x y)
- | Bot, _ | _, Bot -> Bot
- | Int x, _ when x = Z.zero -> Int Z.zero
- | _, Int x when x = Z.zero -> Int (Z.zero)
- | _ -> Top
- let div a b = match a, b with
- | Int x, Int y -> Int (Z.div x y)
- | Bot, _ | _, Bot -> Bot
- | Int x, _ when x = Z.zero -> Int Z.zero
- | _ -> Top
- let rem a b = match a, b with
- | Int x, Int y -> Int (Z.rem x y)
- | Bot, _ | _, Bot -> Bot
- | Int x, _ when x = Z.zero -> Int Z.zero
- | _ -> Top
+ 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 a b = match a, b with
+ | Int x, Int y -> Int (Z.mul x y)
+ | Bot, _ | _, Bot -> Bot
+ | Int x, _ when x = Z.zero -> Int Z.zero
+ | _, Int x when x = Z.zero -> Int (Z.zero)
+ | _ -> Top
+ let div a b = match a, b with
+ | Int x, Int y -> Int (Z.div x y)
+ | Bot, _ | _, Bot -> Bot
+ | Int x, _ when x = Z.zero -> Int Z.zero
+ | _ -> Top
+ let rem a b = match a, b with
+ | Int x, Int y -> Int (Z.rem x y)
+ | Bot, _ | _, Bot -> Bot
+ | Int x, _ when x = Z.zero -> Int Z.zero
+ | _ -> Top
- let leq a b =
- match a, b with
- | Int a, Int b ->
- if Z.leq a b
- 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) ^ "}"
+ let leq a b =
+ match a, b with
+ | Int a, Int b ->
+ if Z.leq a b
+ 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 5c00fbd..404548c 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -1,33 +1,33 @@
open Abstract_syntax_tree
module type ENVIRONMENT_DOMAIN = sig
- type t
+ type t
- (* construction *)
- val init : t
- val bottom : t
- val is_bot : t -> bool
+ (* construction *)
+ val init : t
+ val bottom : t
+ val is_bot : t -> bool
- (* variable management *)
- val addvar : t -> id -> t
- val rmvar : t -> id -> t
- val vars : t -> id list
+ (* variable management *)
+ val addvar : t -> id -> t
+ val rmvar : t -> id -> t
+ val vars : t -> id list
- (* abstract operation *)
- val assign : t -> id -> expr ext -> t (* S[id <- expr] *)
- val compare_leq : t -> expr ext -> expr ext -> t (* S[expr <= expr ?] *)
- val compare_eq : t -> expr ext -> expr ext -> t (* S[expr = expr ?] *)
+ (* abstract operation *)
+ val assign : t -> id -> expr ext -> t (* S[id <- expr] *)
+ val compare_leq : t -> expr ext -> expr ext -> t (* S[expr <= expr ?] *)
+ val compare_eq : 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
+ (* 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
+ (* order *)
+ val subset : t -> t -> bool
- (* pretty-printing *)
- val var_str : t -> id list -> string
+ (* pretty-printing *)
+ val var_str : t -> id list -> string
end
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index 5f03775..c599a76 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -4,94 +4,94 @@ open Util
module Make (E : ENVIRONMENT_DOMAIN) = struct
- let neg (e, l) =
- (AST_unary(AST_NOT, (e, l))), l
+ let neg (e, l) =
+ (AST_unary(AST_NOT, (e, l))), l
- let binop op (e, l) e2 =
- (AST_binary (op, (e,l), e2)), l
- let m1 (e, l) =
- binop AST_MINUS (e, l) (AST_int_const("1", l), l)
- let p1 (e, l) =
- binop AST_PLUS (e, l) (AST_int_const("1", l), l)
+ let binop op (e, l) e2 =
+ (AST_binary (op, (e,l), e2)), l
+ let m1 (e, l) =
+ binop AST_MINUS (e, l) (AST_int_const("1", l), l)
+ let p1 (e, l) =
+ binop AST_PLUS (e, l) (AST_int_const("1", l), l)
let bottom_with_vars =
List.fold_left E.addvar E.bottom
- let rec condition cond env =
- begin match fst cond with
- | AST_binary (AST_LESS_EQUAL, e1, e2) ->
- E.compare_leq env e1 e2
- | AST_binary (AST_EQUAL, e1, e2) ->
+ let rec condition cond env =
+ begin match fst cond with
+ | AST_binary (AST_LESS_EQUAL, e1, e2) ->
+ E.compare_leq env e1 e2
+ | AST_binary (AST_EQUAL, e1, e2) ->
E.compare_eq env e1 e2
- | 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)
+ | 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)
- (* transformations : remove not *)
- | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) ->
- condition cond env
- | 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
+ (* transformations : remove not *)
+ | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) ->
+ condition cond env
+ | 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
- | AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) ->
- let op2 = match op with
- | AST_LESS_EQUAL -> AST_GREATER
- | AST_LESS -> AST_GREATER_EQUAL
- | AST_GREATER_EQUAL -> AST_LESS
- | AST_GREATER -> AST_LESS_EQUAL
- | AST_EQUAL -> AST_NOT_EQUAL
- | AST_NOT_EQUAL -> AST_EQUAL
- | _ -> assert false
- in
- condition (binop op2 e1 e2) env
-
- (* transformations : encode everything with leq *)
- | AST_binary(AST_LESS, e1, e2) ->
- condition
- (binop AST_AND (binop AST_LESS_EQUAL e1 (m1 e2))
- (binop AST_LESS_EQUAL (p1 e1) e2))
- env
- | AST_binary (AST_GREATER_EQUAL, e1, e2) ->
- condition
- (binop AST_LESS_EQUAL e2 e1)
- env
- | AST_binary (AST_GREATER, e1, e2) ->
- condition
- (binop AST_LESS e2 e1)
- env
- | AST_binary (AST_NOT_EQUAL, e1, e2) ->
- condition
- (binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1))
- env
+ | AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) ->
+ let op2 = match op with
+ | AST_LESS_EQUAL -> AST_GREATER
+ | AST_LESS -> AST_GREATER_EQUAL
+ | AST_GREATER_EQUAL -> AST_LESS
+ | AST_GREATER -> AST_LESS_EQUAL
+ | AST_EQUAL -> AST_NOT_EQUAL
+ | AST_NOT_EQUAL -> AST_EQUAL
+ | _ -> assert false
+ in
+ condition (binop op2 e1 e2) env
+
+ (* transformations : encode everything with leq *)
+ | AST_binary(AST_LESS, e1, e2) ->
+ condition
+ (binop AST_AND (binop AST_LESS_EQUAL e1 (m1 e2))
+ (binop AST_LESS_EQUAL (p1 e1) e2))
+ env
+ | AST_binary (AST_GREATER_EQUAL, e1, e2) ->
+ condition
+ (binop AST_LESS_EQUAL e2 e1)
+ env
+ | AST_binary (AST_GREATER, e1, e2) ->
+ condition
+ (binop AST_LESS e2 e1)
+ env
+ | AST_binary (AST_NOT_EQUAL, e1, e2) ->
+ condition
+ (binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1))
+ env
- | _ -> env
- end
+ | _ -> env
+ end
- let rec interp_stmt env stat =
- begin match fst stat with
- | AST_block b ->
- (* remember to remove vars that have gone out of scope at the end *)
- let prevars = E.vars env in
- let env2 = List.fold_left interp_stmt env b in
- let postvars = E.vars env2 in
- let rmvars = List.filter (fun x -> not (List.mem x prevars)) postvars in
- List.fold_left E.rmvar env2 rmvars
- | 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) ->
- let e1 = (interp_stmt (condition cond env) tb) in
- let e2 = (interp_stmt (condition (neg cond) env) eb) in
- E.join e1 e2
- | AST_while (cond, body) ->
+ let rec interp_stmt env stat =
+ begin match fst stat with
+ | AST_block b ->
+ (* remember to remove vars that have gone out of scope at the end *)
+ let prevars = E.vars env in
+ let env2 = List.fold_left interp_stmt env b in
+ let postvars = E.vars env2 in
+ let rmvars = List.filter (fun x -> not (List.mem x prevars)) postvars in
+ List.fold_left E.rmvar env2 rmvars
+ | 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) ->
+ let e1 = (interp_stmt (condition cond env) tb) in
+ let e2 = (interp_stmt (condition (neg cond) env) eb) in
+ E.join e1 e2
+ | AST_while (cond, body) ->
(* loop unrolling *)
let rec unroll u = function
| 0 -> u, bottom_with_vars (E.vars env)
@@ -118,40 +118,40 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
let x = iter 0 env in
let y = fix fsharp x in (* decreasing iteration *)
E.join (condition (neg cond) y) u_u
- | AST_HALT -> bottom_with_vars (E.vars env)
- | AST_assert cond ->
- if not
- (E.is_bot (condition (neg cond) env))
- then begin
- Format.printf "%s: ERROR: assertion failure@."
- (Abstract_syntax_printer.string_of_extent (snd stat));
- end;
- condition cond env
- | AST_print items ->
- Format.printf "%s: %s@."
- (Abstract_syntax_printer.string_of_extent (snd stat))
- (E.var_str env (List.map fst items));
- env
- | AST_local ((ty, _), vars) ->
- List.fold_left
- (fun env ((id, _), init) ->
- let env2 = E.addvar env id in
- match init with
- | Some e -> E.assign env2 id e
- | None -> env2)
- env
- vars
- | _ -> assert false (* not implemented *)
- end
-
- let interpret prog =
- let result = List.fold_left
- (fun env x -> match x with
- | AST_stat st -> interp_stmt env st
- | _ -> env)
- E.init
- (fst prog)
- in
- Format.printf "Output: %s@."
- (E.var_str result (E.vars result))
+ | AST_HALT -> bottom_with_vars (E.vars env)
+ | AST_assert cond ->
+ if not
+ (E.is_bot (condition (neg cond) env))
+ then begin
+ Format.printf "%s: ERROR: assertion failure@."
+ (Abstract_syntax_printer.string_of_extent (snd stat));
+ end;
+ condition cond env
+ | AST_print items ->
+ Format.printf "%s: %s@."
+ (Abstract_syntax_printer.string_of_extent (snd stat))
+ (E.var_str env (List.map fst items));
+ env
+ | AST_local ((ty, _), vars) ->
+ List.fold_left
+ (fun env ((id, _), init) ->
+ let env2 = E.addvar env id in
+ match init with
+ | Some e -> E.assign env2 id e
+ | None -> env2)
+ env
+ vars
+ | _ -> assert false (* not implemented *)
+ end
+
+ let interpret prog =
+ let result = List.fold_left
+ (fun env x -> match x with
+ | AST_stat st -> interp_stmt env st
+ | _ -> env)
+ E.init
+ (fst prog)
+ in
+ Format.printf "Output: %s@."
+ (E.var_str result (E.vars result))
end
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
index 98f4daf..b63f8a9 100644
--- a/abstract/intervals_domain.ml
+++ b/abstract/intervals_domain.ml
@@ -1,122 +1,122 @@
open Value_domain
module Intervals : VALUE_DOMAIN = struct
- type bound = Int of Z.t | PInf | MInf
-
- type t = Itv of bound * bound | Bot
-
- (* utilities *)
- let bound_leq a b = (* a <= b ? *)
- match a, b with
- | MInf, _ | _, PInf -> true
- | Int a, Int b -> Z.leq a b
- | x, y -> x = y
-
- let bound_add a b =
- match a, b with
- | MInf, Int a | Int a, MInf -> MInf
- | PInf, Int a | Int a, PInf -> PInf
- | MInf, MInf -> MInf
- | PInf, PInf -> PInf
- | Int a, Int b -> Int (Z.add a b)
- | _ -> assert false
- let bound_mul a b =
- match a, b with
- | PInf, Int(x) | Int(x), PInf ->
- if x > Z.zero then PInf
- else if x < Z.zero then MInf
- else Int Z.zero
- | MInf, Int(x) | Int(x), MInf ->
- if x < Z.zero then PInf
- else if x > Z.zero then MInf
- else Int Z.zero
- | Int(x), Int(y) -> Int(Z.mul x y)
- | MInf, PInf | PInf, MInf -> MInf
- | MInf, MInf | PInf, PInf -> PInf
-
- let bound_min a b = match a, b with
- | MInf, _ | _, MInf -> MInf
- | Int a, Int b -> Int (min a b)
- | Int a, PInf -> Int a
- | PInf, Int a -> Int a
- | PInf, PInf -> PInf
- let bound_max a b = match a, b with
- | PInf, _ | _, PInf -> PInf
- | Int a, Int b -> Int (max a b)
- | Int a, MInf | MInf, Int a -> Int a
- | MInf, MInf -> MInf
-
- let bound_neg = function
- | PInf -> MInf
- | MInf -> PInf
- | Int i -> Int (Z.neg i)
-
- (* implementation *)
- let top = Itv(MInf, PInf)
- let bottom = Bot
- let const i = Itv(Int i, Int i)
- let rand i j =
+ type bound = Int of Z.t | PInf | MInf
+
+ type t = Itv of bound * bound | Bot
+
+ (* utilities *)
+ let bound_leq a b = (* a <= b ? *)
+ match a, b with
+ | MInf, _ | _, PInf -> true
+ | Int a, Int b -> Z.leq a b
+ | x, y -> x = y
+
+ let bound_add a b =
+ match a, b with
+ | MInf, Int a | Int a, MInf -> MInf
+ | PInf, Int a | Int a, PInf -> PInf
+ | MInf, MInf -> MInf
+ | PInf, PInf -> PInf
+ | Int a, Int b -> Int (Z.add a b)
+ | _ -> assert false
+ let bound_mul a b =
+ match a, b with
+ | PInf, Int(x) | Int(x), PInf ->
+ if x > Z.zero then PInf
+ else if x < Z.zero then MInf
+ else Int Z.zero
+ | MInf, Int(x) | Int(x), MInf ->
+ if x < Z.zero then PInf
+ else if x > Z.zero then MInf
+ else Int Z.zero
+ | Int(x), Int(y) -> Int(Z.mul x y)
+ | MInf, PInf | PInf, MInf -> MInf
+ | MInf, MInf | PInf, PInf -> PInf
+
+ let bound_min a b = match a, b with
+ | MInf, _ | _, MInf -> MInf
+ | Int a, Int b -> Int (min a b)
+ | Int a, PInf -> Int a
+ | PInf, Int a -> Int a
+ | PInf, PInf -> PInf
+ let bound_max a b = match a, b with
+ | PInf, _ | _, PInf -> PInf
+ | Int a, Int b -> Int (max a b)
+ | Int a, MInf | MInf, Int a -> Int a
+ | MInf, MInf -> MInf
+
+ let bound_neg = function
+ | PInf -> MInf
+ | MInf -> PInf
+ | Int i -> Int (Z.neg i)
+
+ (* implementation *)
+ let top = Itv(MInf, PInf)
+ let bottom = Bot
+ let const i = Itv(Int i, Int i)
+ let rand i j =
if Z.leq i j then Itv(Int i, Int j) else Bot
- let subset a b = match a, b with
- | Bot, _ -> true
- | _, Bot -> false
- | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b
-
- let join a b = match a, b with
- | Bot, x | x, Bot -> x
- | Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d)
-
- let meet a b = match a, b with
- | Bot, x | x, Bot -> Bot
- | Itv(a, b), Itv(c, d) ->
- let u, v = bound_max a c, bound_min b d in
- if bound_leq u v
- then Itv(u, v)
- else Bot
-
- let widen a b = match a, b with
- | x, Bot | Bot, x -> x
- | Itv(a, b), Itv(c, d) ->
- Itv(
- (if not (bound_leq a c) then MInf else a),
- (if not (bound_leq d b) then PInf else b))
-
- let neg = function
- | Bot -> Bot
- | Itv(a, b) -> Itv(bound_neg b, bound_neg a)
- let add a b = match a, b with
- | Bot, _ | _, Bot -> Bot
- | Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d)
- let sub a b = match a, b with
- | Bot, _ | _, Bot -> Bot
- | Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
- let mul a b = match a, b with
- | Bot, _ | _, Bot -> Bot
- | Itv(a, b), Itv(c, d) ->
- Itv(
- (bound_min (bound_min (bound_mul a c) (bound_mul a d))
- (bound_min (bound_mul b c) (bound_mul b d))),
- (bound_max (bound_max (bound_mul a c) (bound_mul a d))
- (bound_max (bound_mul b c) (bound_mul b d))))
-
-
- let div a b = top (* TODO *)
- let rem a b = top (* TODO *)
-
- let leq a b = match a, b with
- | Bot, _ | _, Bot -> Bot, Bot
- | Itv(a, b), Itv(c, d) ->
- if not (bound_leq a d)
- then Bot, Bot
- else Itv(a, bound_min b d), Itv(bound_max a c, d)
-
- let bound_str = function
- | MInf -> "-oo"
- | PInf -> "+oo"
- | Int i -> Z.to_string i
- let to_string = function
- | Bot -> "bot"
- | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"
+ let subset a b = match a, b with
+ | Bot, _ -> true
+ | _, Bot -> false
+ | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b
+
+ let join a b = match a, b with
+ | Bot, x | x, Bot -> x
+ | Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d)
+
+ let meet a b = match a, b with
+ | Bot, x | x, Bot -> Bot
+ | Itv(a, b), Itv(c, d) ->
+ let u, v = bound_max a c, bound_min b d in
+ if bound_leq u v
+ then Itv(u, v)
+ else Bot
+
+ let widen a b = match a, b with
+ | x, Bot | Bot, x -> x
+ | Itv(a, b), Itv(c, d) ->
+ Itv(
+ (if not (bound_leq a c) then MInf else a),
+ (if not (bound_leq d b) then PInf else b))
+
+ let neg = function
+ | Bot -> Bot
+ | Itv(a, b) -> Itv(bound_neg b, bound_neg a)
+ let add a b = match a, b with
+ | Bot, _ | _, Bot -> Bot
+ | Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d)
+ let sub a b = match a, b with
+ | Bot, _ | _, Bot -> Bot
+ | Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
+ let mul a b = match a, b with
+ | Bot, _ | _, Bot -> Bot
+ | Itv(a, b), Itv(c, d) ->
+ Itv(
+ (bound_min (bound_min (bound_mul a c) (bound_mul a d))
+ (bound_min (bound_mul b c) (bound_mul b d))),
+ (bound_max (bound_max (bound_mul a c) (bound_mul a d))
+ (bound_max (bound_mul b c) (bound_mul b d))))
+
+
+ let div a b = top (* TODO *)
+ let rem a b = top (* TODO *)
+
+ let leq a b = match a, b with
+ | Bot, _ | _, Bot -> Bot, Bot
+ | Itv(a, b), Itv(c, d) ->
+ if not (bound_leq a d)
+ then Bot, Bot
+ else Itv(a, bound_min b d), Itv(bound_max a c, d)
+
+ let bound_str = function
+ | MInf -> "-oo"
+ | PInf -> "+oo"
+ | Int i -> Z.to_string i
+ let to_string = function
+ | Bot -> "bot"
+ | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"
end
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 8ac6a2a..39095b0 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -6,130 +6,130 @@ open Environment_domain
module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
- type env = V.t VarMap.t
+ type env = V.t VarMap.t
- type t = Env of env | Bot
+ type t = Env of env | Bot
- let init = Env VarMap.empty
- let bottom = 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 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 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
+ 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 *)
+ (* implementation *)
- let is_bot env = match env with
- | Bot -> true
- | Env env -> strict env = Bot
+ 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
+ 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 f 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' = f v1 v2 in
- Env (VarMap.add a v1' (VarMap.add b v2' env))
- | AST_identifier(a, _), _ ->
- let v1, v2 = get_var env a, eval env e2 in
- let v1', v2' = f v1 v2 in
- if V.bottom = v2'
- then Bot
- else Env (VarMap.add a v1' env)
- | _, AST_identifier(b, _) ->
- let v1, v2 = eval env e1, get_var env b in
- let v1', v2' = f v1 v2 in
- if V.bottom = v1'
- then Bot
- else Env (VarMap.add b v2' env)
- | _ ->
- let v1, v2 = eval env e1, eval env e2 in
- let v1', v2' = f v1 v2 in
- if V.bottom = v1' ||V.bottom = v2'
- then Bot
- else Env env)
- x
+ let assign x id expr = strict_apply
+ (fun env -> Env (VarMap.add id (eval env expr) env))
+ x
+ let compare f 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' = f v1 v2 in
+ Env (VarMap.add a v1' (VarMap.add b v2' env))
+ | AST_identifier(a, _), _ ->
+ let v1, v2 = get_var env a, eval env e2 in
+ let v1', v2' = f v1 v2 in
+ if V.bottom = v2'
+ then Bot
+ else Env (VarMap.add a v1' env)
+ | _, AST_identifier(b, _) ->
+ let v1, v2 = eval env e1, get_var env b in
+ let v1', v2' = f v1 v2 in
+ if V.bottom = v1'
+ then Bot
+ else Env (VarMap.add b v2' env)
+ | _ ->
+ let v1, v2 = eval env e1, eval env e2 in
+ let v1', v2' = f v1 v2 in
+ if V.bottom = v1' ||V.bottom = v2'
+ then Bot
+ else Env env)
+ x
let compare_leq = compare V.leq
let compare_eq = compare (fun x y -> let r = V.meet x y in r, r)
- 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 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
-
- (* pretty-printing *)
- let var_str env vars =
- match env with
- | Bot -> "bottom"
- | 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 vars env = match env with
- | Bot -> []
- | Env env -> List.map fst (VarMap.bindings env)
+ 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
+
+ (* pretty-printing *)
+ let var_str env vars =
+ match env with
+ | Bot -> "bottom"
+ | 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 vars env = match env with
+ | Bot -> []
+ | Env env -> List.map fst (VarMap.bindings env)
end
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml
index 9cf6d76..da4f481 100644
--- a/abstract/value_domain.ml
+++ b/abstract/value_domain.ml
@@ -1,31 +1,31 @@
module type VALUE_DOMAIN = sig
- type t
+ type t
- (* constructors *)
- val top : t
- val bottom : t
- val const : Z.t -> t
- val rand : Z.t -> Z.t -> 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
+ (* 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
+ (* 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
+ (* 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]) *)
+ (* 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
+ (* pretty-printing *)
+ val to_string : t -> string
end
diff --git a/main.ml b/main.ml
index 937180e..7e6279c 100644
--- a/main.ml
+++ b/main.ml
@@ -27,11 +27,12 @@ let const_interp = ref false
let interv_interp = ref false
let rel_interp = ref false
let get_interp () =
- if !interv_interp
- then Interp_interv.interpret
- else if !rel_interp
- then Interp_rel.interpret
- else Interp_const.interpret
+ if !interv_interp then
+ Interp_interv.interpret
+ else if !rel_interp then
+ Interp_rel.interpret
+ else
+ Interp_const.interpret
let ifile = ref ""
let set_var v s = v := s
@@ -39,27 +40,27 @@ let set_var v s = v := s
let usage = "usage: analyzer [options] file.c"
let options = [
- "--dump", Arg.Set dump, "Dump program source.";
- "--const-interp", Arg.Set const_interp, "Use constant lattice interpreter.";
- "--interv-interp", Arg.Set interv_interp, "Use interval lattice interpreter.";
- "--rel-interp", Arg.Set rel_interp, "Use relationnal (Apron) lattice.";
+ "--dump", Arg.Set dump, "Dump program source.";
+ "--const-interp", Arg.Set const_interp, "Use constant lattice interpreter.";
+ "--interv-interp", Arg.Set interv_interp, "Use interval lattice interpreter.";
+ "--rel-interp", Arg.Set rel_interp, "Use relationnal (Apron) lattice.";
]
(* parse and print filename *)
let doit filename =
- let prog = File_parser.parse_file filename in
- if !dump then Abstract_syntax_printer.print_prog Format.std_formatter prog;
- (get_interp ()) prog
+ let prog = File_parser.parse_file filename in
+ if !dump then Abstract_syntax_printer.print_prog Format.std_formatter prog;
+ (get_interp ()) prog
(* parses arguments to get filename *)
let main () =
- Arg.parse options (set_var ifile) usage;
+ Arg.parse options (set_var ifile) usage;
- if !ifile = "" then begin
- Format.eprintf "No input file...@.";
- exit 1
- end;
+ if !ifile = "" then begin
+ Format.eprintf "No input file...@.";
+ exit 1
+ end;
- doit !ifile
+ doit !ifile
let _ = main ()