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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
open Abstract_syntax_tree
open Environment_domain
open Util
module Make (E : ENVIRONMENT_DOMAIN) = struct
let neg e =
(AST_unary(AST_NOT, e)), snd e
let binop op e e2 =
(AST_binary (op, e, e2)), snd e
let m1 e =
binop AST_MINUS e (AST_int_const("1", snd e), snd e)
let p1 e =
binop AST_PLUS e (AST_int_const("1", snd e), snd e)
let bottom_with_vars vlist =
List.fold_left E.addvar E.bottom vlist
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_bool_const true -> env
| AST_bool_const false -> E.bottom
(* transformations : remove not *)
| AST_unary(AST_NOT, (AST_bool_const x, _)) ->
condition (AST_bool_const (not x), snd cond) env
| AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), _)) ->
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), _)) ->
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
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)
| 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))
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
|
