blob: dda3c86726c7c3f7b0a758f73cf4d63a7448e347 (
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 M = Modules
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 ...;
```
*)
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, st2) with
| Drop p1, Assign (p2, _) ->
if p1 = p2 then self#visit_statement env st2
else super#visit_Sequence env st1 st2
| Drop p1, Sequence (Assign (p2, _), _) ->
if p1 = p2 then self#visit_statement env st2
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 : M.llbc_module) : M.llbc_module =
let functions = List.map filter_drop_assigns m.functions in
{ m with functions }
|
