summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-21 17:57:06 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-21 17:57:06 +0200
commit4204d25a2d277af1c16f55ee488e42c7b79bba1f (patch)
tree81f62443a6466ca35719588836038c62f7ac3485
parent4d59f3a805d0cca882caab353ac8ec0dd4c04f73 (diff)
downloadSemVerif-Projet-4204d25a2d277af1c16f55ee488e42c7b79bba1f.tar.gz
SemVerif-Projet-4204d25a2d277af1c16f55ee488e42c7b79bba1f.zip
All tests pass except one !
-rw-r--r--abstract/environment_domain.ml3
-rw-r--r--abstract/interpret.ml63
-rw-r--r--abstract/nonrelational.ml12
-rw-r--r--abstract/relational_apron.ml91
-rw-r--r--libs/util.ml9
-rwxr-xr-xtests/test.sh45
6 files changed, 165 insertions, 58 deletions
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml
index 05473aa..5c00fbd 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/environment_domain.ml
@@ -15,7 +15,8 @@ module type ENVIRONMENT_DOMAIN = sig
(* abstract operation *)
val assign : t -> id -> expr ext -> t (* S[id <- expr] *)
- val compare : t -> expr ext -> expr ext -> t (* S[expr <= 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 *)
diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index 79d4d2c..5f03775 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -14,10 +14,15 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
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 env 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) ->
@@ -59,10 +64,6 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
condition
(binop AST_LESS e2 e1)
env
- | AST_binary (AST_EQUAL, e1, e2) ->
- condition
- (binop AST_AND (binop AST_LESS_EQUAL e1 e2) (binop AST_LESS_EQUAL e2 e1))
- env
| AST_binary (AST_NOT_EQUAL, e1, e2) ->
condition
(binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1))
@@ -91,31 +92,33 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
let e2 = (interp_stmt (condition (neg cond) env) eb) in
E.join e1 e2
| AST_while (cond, body) ->
- let unroll_count = 3 in
- let rec iter n i x =
- (* Format.printf "(iter %d) i:%s x:%s @." n (E.var_str i (E.vars i))
- (E.var_str x (E.vars x)); *)
- let out_state = condition (neg cond) i in
- let next_step = interp_stmt (condition cond i) body in
- (* Format.printf ". next step: %s@." (E.var_str next_step (E.vars next_step)); *)
- if n < unroll_count then
- E.join
- out_state
- (iter (n+1) next_step x)
- else
- let env2 =
- E.widen
- i
- next_step
- in
- if env2 = i
- then env2
- else E.join
- out_state
- (iter (n+1) env2 x)
- in
- condition (neg cond) (iter 0 env env)
- | AST_HALT -> E.bottom
+ (* loop unrolling *)
+ let rec unroll u = function
+ | 0 -> u, bottom_with_vars (E.vars env)
+ | n ->
+ let prev_u, u_prev_u = unroll u (n-1) in
+ interp_stmt (condition cond prev_u) body,
+ E.join u_prev_u (condition (neg cond) prev_u)
+ in
+ 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
+ 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)
+ in
+ if 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
+ | AST_HALT -> bottom_with_vars (E.vars env)
| AST_assert cond ->
if not
(E.is_bot (condition (neg cond) env))
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 7221df1..8ac6a2a 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -61,31 +61,33 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
let assign x id expr = strict_apply
(fun env -> Env (VarMap.add id (eval env expr) env))
x
- let compare x e1 e2 =
+ 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' = V.leq v1 v2 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' = V.leq v1 v2 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' = V.leq v1 v2 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' = V.leq v1 v2 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
diff --git a/abstract/relational_apron.ml b/abstract/relational_apron.ml
index bd078cf..926d2a9 100644
--- a/abstract/relational_apron.ml
+++ b/abstract/relational_apron.ml
@@ -1,3 +1,4 @@
+open Abstract_syntax_tree
open Apron
open Util
open Environment_domain
@@ -11,19 +12,86 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
(* abstract elements *)
type t = man Abstract1.t
+ (* translation in trees *)
+ let rec texpr_of_expr e =
+ match fst e with
+ | AST_identifier (id, _) -> Texpr1.Var (Var.of_string id)
+ | AST_int_const (s, _) -> Texpr1.Cst (Coeff.s_of_mpqf (Mpqf.of_string s))
+ | AST_int_rand ((s, _), (t, _)) ->
+ Texpr1.Cst (Coeff.i_of_mpqf (Mpqf.of_string s) (Mpqf.of_string t))
+ | AST_unary(AST_UNARY_PLUS, e) ->
+ texpr_of_expr e
+ | AST_unary(AST_UNARY_MINUS, e) ->
+ (*
+ (* APRON bug ? Unary negate seems to not work correctly... *)
+ Texpr1.Unop(
+ Texpr1.Neg,
+ (texpr_of_expr e),
+ Texpr1.Int,
+ Texpr1.Zero)
+ *)
+ Texpr1.Binop(
+ Texpr1.Sub,
+ Texpr1.Cst(Coeff.s_of_mpqf (Mpqf.of_string "0")),
+ (texpr_of_expr e),
+ Texpr1.Int,
+ Texpr1.Zero)
+ | AST_binary( op, e1, e2) ->
+ let f = match op with
+ | AST_PLUS -> Texpr1.Add
+ | AST_MINUS -> Texpr1.Sub
+ | AST_MULTIPLY -> Texpr1.Mul
+ | AST_DIVIDE -> Texpr1.Div
+ | AST_MODULO -> Texpr1.Mod
+ | _ -> assert false
+ in
+ Texpr1.Binop
+ (f, (texpr_of_expr e1), (texpr_of_expr e2), Texpr1.Int, Texpr1.Zero)
+ | _ -> assert false
+
(* implementation *)
let init = Abstract1.top manager (Environment.make [||] [||])
let bottom = Abstract1.bottom manager (Environment.make [||] [||])
let is_bot = Abstract1.is_bottom manager
- let addvar x id = x (* TODO *)
- let rmvar x id = x (* TODO *)
+ let addvar x id =
+ let env = Abstract1.env x in
+ let env2 = Environment.add env [| Var.of_string id |] [||] in
+ Abstract1.change_environment manager x env2 false
+ let rmvar x id =
+ let env = Abstract1.env x in
+ let env2 = Environment.remove env [| Var.of_string id |] in
+ Abstract1.change_environment manager x env2 false
let vars x =
List.map Var.to_string @@
- Array.to_list @@ snd @@ Environment.vars @@ Abstract1.env x
+ Array.to_list @@ fst @@ Environment.vars @@ Abstract1.env x
- let assign x id e = x (* TODO *)
- let compare x e1 e2 = x (* TODO *)
+ let assign x id e =
+ let expr = Texpr1.of_expr (Abstract1.env x) (texpr_of_expr e) in
+ let x' =
+ Abstract1.assign_texpr manager x
+ (Var.of_string id) expr None
+ in
+ if false then begin
+ Format.eprintf "Assign : ";
+ Abstract1.print Format.err_formatter x;
+ Format.eprintf " ; %s <- " id;
+ Texpr1.print Format.err_formatter expr;
+ Format.eprintf " ; ";
+ Abstract1.print Format.err_formatter x';
+ Format.eprintf "@.";
+ end;
+ x'
+ let compare op x e1 e2 =
+ let env = Abstract1.env x in
+ let expr = Texpr1.Binop
+ (Texpr1.Sub, texpr_of_expr e2, texpr_of_expr e1, Texpr1.Int, Texpr1.Zero) in
+ let cons = Tcons1.make (Texpr1.of_expr env expr) op in
+ let ar = Tcons1.array_make env 1 in
+ Tcons1.array_set ar 0 cons;
+ Abstract1.meet_tcons_array manager x ar
+ let compare_leq = compare Tcons1.SUPEQ
+ let compare_eq = compare Tcons1.EQ
let join = Abstract1.join manager
let meet = Abstract1.meet manager
@@ -31,7 +99,18 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct
let subset = Abstract1.is_leq manager
- let var_str x idl = "" (* TODO *)
+ 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
+ let s = Format.formatter_of_buffer b in
+ Abstract1.print s xx; Format.fprintf s "@?";
+ (Buffer.contents b)
end
diff --git a/libs/util.ml b/libs/util.ml
index 68332b6..b1fcdc4 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -9,3 +9,12 @@ let rec fix f s =
else fix f fs
let (@@) f x = f x
+
+let print_list x l =
+ Format.printf "%s: " x;
+ let rec aux = function
+ | [] -> ()
+ | [a] -> Format.printf "%s" a
+ | p::q -> Format.printf "%s, " p; aux q
+ in
+ Format.printf "["; aux l; Format.printf "]@.";
diff --git a/tests/test.sh b/tests/test.sh
index 443868a..b736fb2 100755
--- a/tests/test.sh
+++ b/tests/test.sh
@@ -1,26 +1,39 @@
#!/bin/bash
+function test_it {
+ if ../analyze $1 $2 > /tmp/analyze_out.txt;
+ then
+ cat /tmp/analyze_out.txt | uniq | tr -d " \\n" > /tmp/analyze_out_2.txt;
+ cat results/$3 | uniq | tr -d " \\n" > /tmp/expected_out_2.txt;
+ if diff -B /tmp/analyze_out_2.txt /tmp/expected_out_2.txt >/dev/null; then
+ echo "OK $2"
+ else
+ cat /tmp/analyze_out.txt | grep Output > /tmp/analyze_out_3.txt;
+ cat results/$3 | grep Output > /tmp/expected_out_3.txt;
+ if diff -B /tmp/analyze_out_3.txt /tmp/expected_out_3.txt >/dev/null; then
+ echo "(TR) $2"
+ else
+ echo "FAIL $2"
+ fi;
+ fi;
+ else
+ echo "TODO $2"
+ fi;
+}
+
echo "== CONSTANT ABSTRACT DOMAIN"
for a in sources/*.c; do
- if ../analyze --const-interp $a > /tmp/analyze_out.txt;
- then
- if diff -B /tmp/analyze_out.txt results/`basename -s .c $a`.constants.txt > /dev/null
- then echo "OK $a"
- else echo "FAIL $a"
- fi
- else echo "TODO $a";
- fi;
+ test_it --const-interp $a `basename $a .c`.constants.txt;
done;
echo "== INTERVALS ABSTRACT DOMAIN"
for a in sources/*.c; do
- if ../analyze --interv-interp $a > /tmp/analyze_out.txt;
- then
- if diff -B /tmp/analyze_out.txt results/`basename -s .c $a`.intervals.txt > /dev/null
- then echo "OK $a"
- else echo "FAIL $a"
- fi
- else echo "TODO $a";
- fi;
+ test_it --interv-interp $a `basename $a .c`.intervals.txt;
+done;
+
+
+echo "== RELATIONNAL ABSTRACT DOMAIN"
+for a in sources/*.c; do
+ test_it --rel-interp $a `basename $a .c`.polyhedra.txt;
done;