diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-08-21 11:05:36 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-08-21 11:05:36 +0200 |
commit | 54f97d1988f623ba7422e13a504caeb5701ba93c (patch) | |
tree | d8dea46837352979490f4ed4516f9649fef41b98 /backend/Bounds.v | |
parent | b4846ffadfa3fbb73ffa7d9c43e5218adeece8da (diff) | |
download | compcert-kvx-54f97d1988f623ba7422e13a504caeb5701ba93c.tar.gz compcert-kvx-54f97d1988f623ba7422e13a504caeb5701ba93c.zip |
Refactoring of builtins and annotations in the back-end.
Before, the back-end languages had distinct instructions
- Iannot for annotations, taking structured expressions (annot_arg)
as arguments, and producing no results'
- Ibuiltin for other builtins, using simple pseudoregs/locations/registers
as arguments and results.
This branch enriches Ibuiltin instructions so that they take structured
expressions (builtin_arg and builtin_res) as arguments and results.
This way,
- Annotations fit the general pattern of builtin functions,
so Iannot instructions are removed.
- EF_vload_global and EF_vstore_global become useless, as the
same optimization can be achieved by EF_vload/vstore taking
a structured argument of the "address of global" kind.
- Better code can be generated for builtin_memcpy between stack locations,
or volatile accesses to stack locations.
Finally, this commit also introduces a new kind of external function,
EF_debug, which is like EF_annot but produces no observable events.
It will be used later to transport debug info through the back-end,
without preventing optimizations.
Diffstat (limited to 'backend/Bounds.v')
-rw-r--r-- | backend/Bounds.v | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v index 04c1328d..beb29965 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -67,9 +67,8 @@ Definition instr_within_bounds (i: instruction) := | Lload chunk addr args dst => mreg_within_bounds dst | Lcall sig ros => size_arguments sig <= bound_outgoing b | Lbuiltin ef args res => - forall r, In r res \/ In r (destroyed_by_builtin ef) -> mreg_within_bounds r - | Lannot ef args => - forall sl ofs ty, In (S sl ofs ty) (params_of_annot_args args) -> slot_within_bounds sl ofs ty + (forall r, In r (params_of_builtin_res res) \/ In r (destroyed_by_builtin ef) -> mreg_within_bounds r) + /\ (forall sl ofs ty, In (S sl ofs ty) (params_of_builtin_args args) -> slot_within_bounds sl ofs ty) | _ => True end. @@ -101,8 +100,7 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => nil | Lcall sig ros => nil | Ltailcall sig ros => nil - | Lbuiltin ef args res => res ++ destroyed_by_builtin ef - | Lannot ef args => nil + | Lbuiltin ef args res => params_of_builtin_res res ++ destroyed_by_builtin ef | Llabel lbl => nil | Lgoto lbl => nil | Lcond cond args lbl => nil @@ -121,7 +119,7 @@ Definition slots_of_instr (i: instruction) : list (slot * Z * typ) := match i with | Lgetstack sl ofs ty r => (sl, ofs, ty) :: nil | Lsetstack r sl ofs ty => (sl, ofs, ty) :: nil - | Lannot ef args => slots_of_locs (params_of_annot_args args) + | Lbuiltin ef args res => slots_of_locs (params_of_builtin_args args) | _ => nil end. @@ -351,8 +349,8 @@ Proof. (* call *) eapply size_arguments_bound; eauto. (* builtin *) + split; intros. apply H1. apply in_or_app; auto. -(* annot *) apply H0. rewrite slots_of_locs_charact; auto. Qed. |