1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
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 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 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
(* pretty-printing *)
let var_str env vars =
match env with
| Bot -> "bot"
| 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 all_vars_str env =
match env with
| Bot -> "bot"
| Env map -> var_str env (List.map fst (VarMap.bindings map))
end
|
