summaryrefslogtreecommitdiff
path: root/src/PrePasses.ml
blob: 3159907e5edb5db26c66128336155f283e006dd7 (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, 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 : Crates.llbc_crate) : Crates.llbc_crate =
  let functions = List.map filter_drop_assigns m.functions in
  { m with functions }