blob: 8f1354b7f32998160cfe657a4f5249c5001ea5de (
plain)
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
|
(** This files contains passes we apply on the AST *before* calling the
(concrete/symbolic) interpreter on it
*)
module T = Types
module V = Values
module E = Expressions
module C = Contexts
module A = LlbcAst
module L = Logging
let log = L.pre_passes_log
(** Rustc inserts a lot of drops before the assignments.
We consider those drops are part of the assignment, and splitting the
drop and the assignment is problematic for us because it can introduce
[⊥] under borrows. For instance, we encountered situations like the
following one:
{[
drop( *x ); // Illegal! Inserts a ⊥ under a borrow
*x = move ...;
]}
TODO: this is not necessary anymore
*)
let filter_drop_assigns (f : A.fun_decl) : A.fun_decl =
(* The visitor *)
let obj =
object (self)
inherit [_] A.map_statement as super
method! visit_Sequence env st1 st2 =
match (st1.content, st2.content) with
| Drop p1, Assign (p2, _) ->
if p1 = p2 then (self#visit_statement env st2).content
else super#visit_Sequence env st1 st2
| Drop p1, Sequence ({ content = Assign (p2, _); meta = _ }, _) ->
if p1 = p2 then (self#visit_statement env st2).content
else super#visit_Sequence env st1 st2
| _ -> super#visit_Sequence env st1 st2
end
in
(* Map *)
let body =
match f.body with
| Some body -> Some { body with body = obj#visit_statement () body.body }
| None -> None
in
{ f with body }
let apply_passes (m : A.crate) : A.crate =
let functions = List.map filter_drop_assigns m.functions in
{ m with functions }
|
