From 4204d25a2d277af1c16f55ee488e42c7b79bba1f Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 21 May 2014 17:57:06 +0200 Subject: All tests pass except one ! --- abstract/environment_domain.ml | 3 +- abstract/interpret.ml | 63 +++++++++++++++-------------- abstract/nonrelational.ml | 12 +++--- abstract/relational_apron.ml | 91 +++++++++++++++++++++++++++++++++++++++--- 4 files changed, 127 insertions(+), 42 deletions(-) (limited to 'abstract') 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 -- cgit v1.2.3