blob: a24fef504b34f436a97ae6763676f5a2604d855a (
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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* David Monniaux CNRS, VERIMAG *)
(* *)
(* Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
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 :=
| INJnop
| 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
| INJnop => Inop pc'
| 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'
| Ibuiltin ef args res _ => Ibuiltin ef args res pc'
| Icond cond args _ pc2 expected => Icond cond args pc' pc2 expected
| Icall sig ros args res _ => Icall sig ros args res pc'
| 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 -> node -> reg -> PTree.t (list inj_instr).
Definition valid_injection_instr (max_reg : reg) (i : inj_instr) :=
match i with
| INJnop => true
| INJop op args res => (max_reg <? res) && (negb (is_trapping_op op)
&& (Datatypes.length args =? args_of_operation op)%nat)
| INJload _ _ _ res => max_reg <? res
end.
Definition valid_injections1 max_pc max_reg :=
List.forallb
(fun injection =>
((fst injection) <=? max_pc) &&
(List.forallb (valid_injection_instr max_reg) (snd injection))
).
Definition valid_injections f :=
valid_injections1 (max_pc_function f) (max_reg_function f).
Definition transf_function (f : function) : res function :=
let max_pc := max_pc_function f in
let max_reg := max_reg_function f in
let injections := PTree.elements (gen_injections f max_pc max_reg) in
if valid_injections1 max_pc max_reg 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.
|
