blob: e82b7cdba4198ad119ee583795473740ac656307 (
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
|
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL Maps CSE2deps.
Require Import CSE3analysis HashedSet.
Require Import RTLtyping.
Local Open Scope error_monad_scope.
Axiom preanalysis : typing_env -> RTL.function -> invariants * analysis_hints.
Section REWRITE.
Context {ctx : eq_context}.
Definition find_op_in_fmap fmap pc op args :=
match PMap.get pc fmap with
| Some rel => rhs_find (ctx:=ctx) pc (SOp op) args rel
| None => None
end.
Definition find_load_in_fmap fmap pc chunk addr args :=
match PMap.get pc fmap with
| Some rel => rhs_find (ctx:=ctx) pc (SLoad chunk addr) args rel
| None => None
end.
Definition forward_move_b (rb : RB.t) (x : reg) :=
match rb with
| None => x
| Some rel => forward_move (ctx := ctx) rel x
end.
Definition subst_arg (fmap : PMap.t RB.t) (pc : node) (x : reg) : reg :=
forward_move_b (PMap.get pc fmap) x.
Definition subst_args fmap pc := List.map (subst_arg fmap pc).
Definition transf_instr (fmap : PMap.t RB.t)
(pc: node) (instr: instruction) :=
match instr with
| Iop op args dst s =>
let args' := subst_args fmap pc args in
match find_op_in_fmap fmap pc op args' with
| None => Iop op args' dst s
| Some src => Iop Omove (src::nil) dst s
end
| Iload trap chunk addr args dst s =>
let args' := subst_args fmap pc args in
match find_load_in_fmap fmap pc chunk addr args' with
| None => Iload trap chunk addr args' dst s
| Some src => Iop Omove (src::nil) dst s
end
| Istore chunk addr args src s =>
Istore chunk addr (subst_args fmap pc args) src s
| Icall sig ros args dst s =>
Icall sig ros (subst_args fmap pc args) dst s
| Itailcall sig ros args =>
Itailcall sig ros (subst_args fmap pc args)
| Icond cond args s1 s2 =>
Icond cond (subst_args fmap pc args) s1 s2
| Ijumptable arg tbl =>
Ijumptable (subst_arg fmap pc arg) tbl
| Ireturn (Some arg) =>
Ireturn (Some (subst_arg fmap pc arg))
| _ => instr
end.
End REWRITE.
Definition transf_function (f: function) : res function :=
do tenv <- type_function f;
let (invariants, hints) := preanalysis tenv f in
let ctx := context_from_hints hints in
OK {| fn_sig := f.(fn_sig);
fn_params := f.(fn_params);
fn_stacksize := f.(fn_stacksize);
fn_code := PTree.map (transf_instr (ctx := ctx) invariants)
f.(fn_code);
fn_entrypoint := f.(fn_entrypoint) |}.
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.
|
