open Formula
open Util
open Ast
open Value_domain
open Num_domain
(*
Implementation of a nonrelationnal domain for numerical values.
Restricted implementation, only support integers.
*)
module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
type env = V.t VarMap.t
type t = Env of env | Bot
type itv = Value_domain.itv
let top vars = Env
(List.fold_left
(fun e (v, _) -> VarMap.add v V.top e)
VarMap.empty vars)
let bottom _ = Bot
let get_var env id =
try VarMap.find id env
with Not_found -> V.top
(* utilities *)
let rec eval env = function
| NIdent id -> get_var env id
| NIntConst i -> V.const i
| NRealConst f -> V.const (int_of_float f) (* TODO floats *)
| NUnary (AST_UPLUS, e, _) -> eval env e
| NUnary (AST_UMINUS, e, _) -> V.neg (eval env e)
| NBinary (op, e1, e2, _) ->
let f = match op with
| AST_PLUS -> V.add
| AST_MINUS -> V.sub
| AST_MUL -> V.mul
| AST_DIV -> V.div
| AST_MOD -> V.rem
in f (eval env e1) (eval env e2)
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 is_bot env = match env with
| Bot -> true
| Env env -> strict env = Bot
let is_top env = match env with
| Bot -> false
| Env e -> VarMap.for_all (fun _ v -> v = V.top) e
let forgetvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x
let vars env = match env with
| Bot -> []
| Env env -> List.map (fun (k, _) -> (k, false)) (VarMap.bindings env)
let vbottom _ = Bot
let project x id = match x with
| Bot -> Value_domain.Bot
| Env env -> V.to_itv (get_var env id)
(* Set-theoretic operations *)
let f_in_merge f _ a b = match a, b with
| Some a, None -> Some a
| None, Some b -> Some b
| Some a, Some b -> Some (f a b)
| _ -> assert false
let join a b = match a, b with
| Bot, x | x, Bot -> x
| Env m, Env n ->
strict (VarMap.merge (f_in_merge V.join) m n)
let meet a b = match a, b with
| Bot, _ | _, Bot -> Bot
| Env m, Env n ->
strict (VarMap.merge (f_in_merge V.meet) m n)
let widen a b = match a, b with
| Bot, x | x, Bot -> x
| Env m, Env n ->
strict (VarMap.merge (f_in_merge V.widen) m n)
(* Inclusion and equality *)
let subset a b = match a, b with
| Bot, x -> true
| Env _, Bot -> false
| Env m, Env n ->
VarMap.for_all
(fun id vn ->
try let vm = VarMap.find id m in V.subset vm vn
with Not_found -> vn = V.top)
n
let eq a b = match a, b with
| Bot, Bot -> true
| Env m, Env n ->
VarMap.for_all2o
(fun _ v -> v = V.top)
(fun _ v -> v = V.top)
(fun _ a b -> a = b)
m n
| _ -> false
(* Apply some formula to the environment *)
let apply_cons env (expr, sign) =
let inv_op = function
| AST_LT -> AST_GT
| AST_GT -> AST_LT
| AST_LE -> AST_GE
| AST_GE -> AST_LE
| x -> x
in
let rec extract_var (lhs, op, rhs) =
match lhs with
| NIdent i -> [i, op, rhs]
| NIntConst _ | NRealConst _ -> []
| NUnary(AST_UPLUS, x, r) -> extract_var (x, op, rhs)
| NUnary(AST_UMINUS, x, r) ->
extract_var (x, inv_op op, NUnary(AST_UMINUS, x, r))
| NBinary(AST_PLUS, a, b, r) ->
extract_var (a, op, NBinary(AST_MINUS, rhs, b, r)) @
extract_var (b, op, NBinary(AST_MINUS, rhs, a, r))
| NBinary(AST_MINUS, a, b, r) ->
extract_var (a, op, NBinary(AST_PLUS, rhs, b, r)) @
extract_var (b, inv_op op, NBinary(AST_MINUS, a, rhs, r))
| NBinary(AST_MUL, a, b, r) when r ->
extract_var (a, op, NBinary(AST_DIV, rhs, b, r)) @
extract_var (b, op, NBinary(AST_DIV, rhs, a, r))
| NBinary(AST_DIV, a, b, r) when r ->
extract_var (a, op, NBinary(AST_MUL, rhs, b, r)) @
extract_var (b, inv_op op, NBinary(AST_DIV, a, rhs, r))
| NBinary _ -> []
in
let zop = match sign with
| CONS_EQ -> AST_EQ | CONS_NE -> AST_NE
| CONS_GT -> AST_GT | CONS_GE -> AST_GE
in
let restrict_var env (i, op, expr) =
strict_apply (fun env ->
let v1, v2 = get_var env i, eval env expr in
let v1' = match op with
| AST_EQ -> V.meet v1 v2
| AST_NE -> v1
| AST_LE -> let u, _ = V.leq v1 v2 in u
| AST_GE -> let _, v = V.leq v2 v1 in v
| AST_LT -> let u, _ = V.leq v1 (V.sub v2 (V.const 1)) in u
| AST_GT -> let _, v = V.leq (V.add v2 (V.const 1)) v1 in v
in
Env (VarMap.add i v1' env))
env
in
List.fold_left restrict_var env
(extract_var (expr, zop, NIntConst 0))
let apply_cl x cl =
let f x = List.fold_left apply_cons x cl in
fix eq f x
(* Assignment *)
let assign x exprs =
let aux env =
let vars = List.map (fun (id, v) -> (id, eval env v)) exprs in
let env2 =
List.fold_left (fun e (id, v) -> VarMap.add id v e)
env vars
in Env env2
in
strict_apply aux x
(* pretty-printing *)
let print_vars fmt env ids =
match env with
| Bot -> Format.fprintf fmt "⊥"
| Env env ->
let l = List.map (fun id -> (get_var env id, id)) ids in
let s = List.sort Pervasives.compare l in
let rec bl = function
| [] -> []
| (v, id)::q when v <> V.top ->
begin match bl q with
| (vv, ids)::q when vv = v -> (v, id::ids)::q
| r -> (v, [id])::r
end
| _::q -> bl q
in
let sbl = bl s in
if sbl = [] then
Format.fprintf fmt "⊤"
else begin
Format.fprintf fmt "@[<v 2>{ ";
List.iteri
(fun j (v, ids) ->
if j > 0 then Format.fprintf fmt "@ ";
Format.fprintf fmt "@[<hov 4>";
List.iteri
(fun i id ->
if i > 0 then Format.fprintf fmt ",@ ";
Format.fprintf fmt "%a" Formula_printer.print_id id)
ids;
match V.as_const v with
| Some i -> Format.fprintf fmt " = %d@]" i
| _ -> Format.fprintf fmt " ∊ %s@]" (V.to_string v))
sbl;
Format.fprintf fmt " }@]"
end
let print fmt x =
print_vars fmt x (List.map fst (vars x))
let print_itv fmt x =
Format.fprintf fmt "%s" (string_of_itv x)
end
