diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-09 09:00:51 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-09 09:00:51 +0200 |
| commit | a6b6bf31121d975c915c01f501618d97df7879fb (patch) | |
| tree | 061cf73e547622695621fc05ce692c029991c9e0 /backend | |
| parent | 56bac3dc3d45c219db5d9c7b6a97794c00f8115e (diff) | |
| download | compcert-kvx-a6b6bf31121d975c915c01f501618d97df7879fb.tar.gz compcert-kvx-a6b6bf31121d975c915c01f501618d97df7879fb.zip | |
Extended inline asm: revised treatment of clobbered registers.
- Treat clobbered registers as being destroyed by EF_inline_asm builtins
(which is the truth, semantically).
- To enable the above, represent clobbers as Coq strings rather than idents
and move register_by_name from Machregsaux.ml to Machregs.v.
- Side benefit: more efficient implementation of Machregsaux.name_of_register.
-# Please enter the commit message for your changes. Lines starting
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Bounds.v | 7 | ||||
| -rw-r--r-- | backend/Regalloc.ml | 6 |
2 files changed, 3 insertions, 10 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v index 7528b66e..04c1328d 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -87,8 +87,6 @@ Section BOUNDS. Variable f: function. -Parameter mregs_of_clobber: list ident -> list mreg. - (** In the proof of the [Stacking] pass, we only need to bound the registers written by an instruction. Therefore, this function returns these registers, ignoring registers used only as @@ -103,7 +101,6 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => nil | Lcall sig ros => nil | Ltailcall sig ros => nil - | Lbuiltin (EF_inline_asm txt typs clob) args res => res ++ mregs_of_clobber clob | Lbuiltin ef args res => res ++ destroyed_by_builtin ef | Lannot ef args => nil | Llabel lbl => nil @@ -354,9 +351,7 @@ Proof. (* call *) eapply size_arguments_bound; eauto. (* builtin *) - apply H1. destruct e; apply in_or_app; auto. - change (destroyed_by_builtin (EF_inline_asm text sg clobbers)) with (@nil mreg) in H2. - simpl in H2; tauto. + apply H1. apply in_or_app; auto. (* annot *) apply H0. rewrite slots_of_locs_charact; auto. Qed. diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index c286e946..aa4efc53 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -585,13 +585,11 @@ let add_interfs_instr g instr live = (* like a move *) IRC.add_pref g arg res | EF_inline_asm(txt, sg, clob), _, _ -> - (* clobbered regs interfere with live set - and also with res and args for GCC compatibility *) + (* clobbered regs interfere with res and args for GCC compatibility *) List.iter (fun c -> - match Machregsaux.register_by_name (extern_atom c) with + match Machregs.register_by_name c with | None -> () | Some mr -> - add_interfs_destroyed g across [mr]; add_interfs_list_mreg g args mr; if sg.sig_res <> None then add_interfs_list_mreg g res mr) clob |