aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Inject.v
blob: 6da10019212c120429ba28e5262fec1ba0fa8dea (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
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
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL.

Local Open Scope positive.

Inductive inj_instr : Type :=
  | INJop: operation -> list reg -> reg -> inj_instr
  | INJload: memory_chunk -> addressing -> list reg -> reg -> inj_instr.

Definition inject_instr (i : inj_instr) (pc' : node) : instruction :=
  match i with
  | INJop op args dst => Iop op args dst pc'
  | INJload chunk addr args dst => Iload NOTRAP chunk addr args dst pc'
  end.

Fixpoint inject_list (prog : code) (pc : node) (dst : node)
         (l : list inj_instr) : node * code :=
  let pc' := Pos.succ pc in
  match l with
  | nil => (pc', PTree.set pc (Inop dst) prog)
  | h::t =>
    inject_list (PTree.set pc (inject_instr h pc') prog)
                pc' dst t
  end.

Definition successor (i : instruction) : node :=
  match i with
  | Inop pc' => pc'
  | Iop _ _ _ pc' => pc'
  | Iload _ _ _ _ _ pc' => pc'
  | Istore _ _ _ _ pc' => pc'
  | Icall _ _ _ _ pc' => pc'
  | Ibuiltin _ _ _ pc' => pc'
  | Icond _ _ pc' _ => pc'
  | Itailcall _ _ _
  | Ijumptable _ _
  | Ireturn _ => 1
  end.

Definition alter_successor (i : instruction) (pc' : node) : instruction :=
  match i with
  | Inop _ => Inop pc'
  | Iop op args dst _ => Iop op args dst pc'
  | Iload trap chunk addr args dst _ => Iload trap chunk addr args dst pc'
  | Istore chunk addr args src _ => Istore chunk addr args src pc'
  | Icall sig ri args dst _ => Icall sig ri args dst pc'
  | Ibuiltin ef args res _ => Ibuiltin ef args res pc'
  | Icond cond args _ pc2 => Icond cond args pc' pc2
  | Itailcall _ _ _
  | Ijumptable _ _
  | Ireturn _ => i
  end.

Definition inject_at (prog : code) (pc extra_pc : node)
           (l : list inj_instr) : node * code :=
  match PTree.get pc prog with
  | Some i =>
    inject_list (PTree.set pc (alter_successor i extra_pc) prog)
                extra_pc (successor i) l
  | None => inject_list prog extra_pc 1 l (* does not happen *)
  end.

Definition inject_at' (already : node * code) pc l :=
  let (extra_pc, prog) := already in
  inject_at prog pc extra_pc l.

Definition inject_l (prog : code) extra_pc injections :=
  List.fold_left (fun already (injection : node * (list inj_instr)) =>
                    inject_at' already (fst injection) (snd injection))
    injections
    (extra_pc, prog).
(*
Definition inject' (prog : code) (extra_pc : node) (injections : PTree.t (list inj_instr)) :=
  PTree.fold inject_at' injections (extra_pc, prog).

Definition inject prog extra_pc injections : code :=
  snd (inject' prog extra_pc injections).
*)

Section INJECTOR.
  Variable gen_injections : function -> PTree.t (list inj_instr).

  Definition transf_function (f : function) : res function :=
    let injections := PTree.elements (gen_injections f) in
    let max_pc := max_pc_function f in
    let max_reg := max_reg_function f in
    if List.forallb
         (fun injection =>
            ((fst injection) <=? max_pc) &&
            (List.forallb
               (fun (i : inj_instr) =>
                  (match i with
                   | INJop _ _ res => res
                   | INJload _ _ _ res => res
                   end) <=? max_reg) (snd injection))
         ) injections
    then
      OK {| fn_sig := f.(fn_sig);
            fn_params := f.(fn_params);
            fn_stacksize := f.(fn_stacksize);
            fn_code := snd (inject_l (fn_code f) (Pos.succ max_pc) injections);
            fn_entrypoint := f.(fn_entrypoint) |}
    else Error (msg "Inject.transf_function: injections at bad locations").

Definition transf_fundef (fd: fundef) : res fundef :=
  AST.transf_partial_fundef transf_function fd.

Definition transf_program (p: program) : res program :=
  transform_partial_program transf_fundef p.
End INJECTOR.