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
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
(** Utility functions *)
open Ast.Stmt
open Ast.Expr
open Manager
open Cases
open Post
open Ast.Semantic
open Route
open Token
open Flow
open Mopsa_utils
let rec exec_cleaner stmt man flow =
let post = man.exec stmt flow in
if !Cases.opt_clean_cur_only then
post
else
post >>% fun flow ->
Flow.fold (fun acc tk env ->
match tk with
| T_cur -> acc
| _ ->
let annot = Flow.get_ctx flow in
let flow' = Flow.singleton annot T_cur env in
let flow'' = man.exec stmt flow' |> post_to_flow man in
Flow.copy T_cur tk man.lattice flow'' flow |>
Flow.copy_ctx flow''
) flow flow |>
Post.return
and exec_cleaners man post =
let post' =
post >>= fun case flow ->
let cleaners = Cases.get_case_cleaners case in
StmtSet.fold
(fun stmt acc ->
acc >>% exec_cleaner stmt man
) cleaners (Post.return flow)
in
Cases.set_cleaners [] post'
and post_to_flow man post =
let clean = exec_cleaners man post in
Cases.reduce
(fun _ flow -> flow)
~join:(Flow.join man.lattice)
~meet:(Flow.meet man.lattice)
clean
let assume
cond ?(route=toplevel) ?(translate=any_semantic)
~fthen ~felse
?(fboth=(fun then_flow else_flow ->
let ret1 = fthen then_flow in
let ctx1 = Cases.get_ctx ret1 in
let ret2 = Flow.set_ctx ctx1 else_flow |>
felse
in
let ret1 = Cases.copy_ctx ret2 ret1 in
Cases.join ret1 ret2
))
?(fnone=(fun then_flow else_flow ->
Cases.join
(Cases.empty then_flow)
(Cases.empty else_flow)
))
?(eval=true)
man flow
=
let evl = if eval then man.eval cond flow ~route ~translate else Eval.singleton cond flow in
let then_post = ( evl >>$ fun cond flow -> man.exec (mk_assume cond cond.erange) flow ~route ) |>
exec_cleaners man |>
Post.remove_duplicates man.lattice
in
let then_ctx = Cases.get_ctx then_post in
let evl' = Cases.set_ctx then_ctx evl in
let else_post = ( evl' >>$ fun cond flow -> man.exec (mk_assume (mk_not cond cond.erange) cond.erange) flow ~route ) |>
exec_cleaners man |>
Post.remove_duplicates man.lattice
in
let then_post' = Cases.copy_ctx else_post then_post in
then_post' >>% fun then_flow ->
else_post >>% fun else_flow ->
match man.lattice.is_bottom (Flow.get T_cur man.lattice then_flow),
man.lattice.is_bottom (Flow.get T_cur man.lattice else_flow)
with
| false,true -> fthen then_flow
| true,false -> felse else_flow
| true,true -> fnone then_flow else_flow
| false,false -> fboth then_flow else_flow
let switch
(cases : (expr list * ('a Flow.flow -> ('a,'r) cases)) list)
?(route = toplevel)
man flow
: ('a,'r) cases
=
let rec one (cond : expr list) acc f =
match cond with
| [] -> f acc
| x :: tl ->
let s = mk_assume x x.erange in
man.exec ~route s acc >>% fun acc' ->
if Flow.get T_cur man.lattice acc' |> man.lattice.is_bottom then
Cases.empty acc'
else
one tl acc' f
in
let rec aux ctx cases =
match cases with
| [] -> assert false
| [(cond, t)] -> one cond (Flow.set_ctx ctx flow) t
| (cond, t) :: q ->
let r = one cond (Flow.set_ctx ctx flow) t in
let rr = aux (Cases.get_ctx r) q in
Cases.join (Cases.copy_ctx rr r) rr
in
aux (Flow.get_ctx flow) cases
let set_env (tk:token) (env:'t) (man:('a,'t) man) (flow:'a flow) : 'a flow =
Flow.set tk (man.set env (Flow.get tk man.lattice flow)) man.lattice flow
let get_env (tk:token) (man:('a,'t) man) (flow:'a flow) : 't =
man.get (Flow.get tk man.lattice flow)
let map_env (tk:token) (f:'t -> 't) (man:('a,'t) man) (flow:'a flow) : 'a flow =
set_env tk (f (get_env tk man flow)) man flow
let get_pair_fst man = (fun a -> man.get a |> fst)
let set_pair_fst man = (fun a1 a -> let old = man.get a in if a1 == fst old then a else man.set (a1, snd old) a)
let get_pair_snd man = (fun a -> man.get a |> snd)
let set_pair_snd man = (fun a2 a -> let old = man.get a in if a2 == snd old then a else man.set (fst old, a2) a)
let env_exec (f:'a flow -> 'a post) ctx (man:('a,'t) man) (a:'a) : 'a =
let flow = Flow.singleton ctx T_cur a in
let flow' = f flow |> post_to_flow man in
Flow.get T_cur man.lattice flow'
let ask_and_reduce_cases f q ?(bottom = fun () -> assert false) a =
let cases = f q a in
Cases.reduce_result
(fun r flow -> r)
~join:(Query.join_query q)
~meet:(Query.meet_query q)
~bottom
cases
let ask_and_reduce_list f q ?(bottom = fun () -> assert false) a =
let l = f q a in
match l with
| [] -> bottom ()
| (_,r)::tl ->
List.fold_left
(fun acc (_,r) -> Query.join_query q acc r)
r tl
let ask_and_reduce = ask_and_reduce_cases
let find_var_by_name ?(function_scope = None) name man flow =
let vars = ask_and_reduce man.ask (Query.Q_defined_variables function_scope) flow in
List.find
(fun v ->
name = Format.asprintf "%a" Ast.Var.pp_var v
) vars
let dummy_range = Location.mk_fresh_range ()
let pp_vars_info man flow fmt vars =
let printer = Print.empty_printer () in
List.iter
(fun v ->
try man.print_expr flow printer (mk_var v dummy_range)
with Not_found -> ()
) vars;
Format.fprintf fmt "%a" Print.pflush printer
let pp_vars_info_by_name man flow fmt names =
pp_vars_info man flow fmt (ListExt.map_filter (fun name ->
try Some (find_var_by_name name man flow)
with Not_found -> None
) names)
let pp_expr_vars_info man flow fmt e =
let vars = Ast.Visitor.expr_vars e in
pp_vars_info man flow fmt vars
let pp_stmt_vars_info man flow fmt s =
let vars = Ast.Visitor.stmt_vars s in
pp_vars_info man flow fmt vars
let breakpoint name man flow =
let _ = man.exec (mk_breakpoint name dummy_range) flow in
()