diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-10-22 16:54:24 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-10-22 16:54:24 +0000 |
| commit | 210352d90e5972aabfb253f7c8a38349f53917b3 (patch) | |
| tree | 93ccbf36e6840118abe84ee940252a7a1fbc7720 /backend/Machabstr.v | |
| parent | ee41c6eae5af0703605780e0b3d8f5c3937f3276 (diff) | |
| download | compcert-210352d90e5972aabfb253f7c8a38349f53917b3.tar.gz compcert-210352d90e5972aabfb253f7c8a38349f53917b3.zip | |
Lever la restriction sur les fonctions externes, restriction qui exigeait que tous les arguments resident en registres
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Machabstr.v')
| -rw-r--r-- | backend/Machabstr.v | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/backend/Machabstr.v b/backend/Machabstr.v index 33ed93ca..d83ffa51 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -88,6 +88,26 @@ Inductive set_slot: frame -> typ -> Z -> val -> frame -> Prop := Definition init_frame (f: function) := empty_block (- f.(fn_framesize)) 0. +(** Extract the values of the arguments of an external call. *) + +Inductive extcall_arg: regset -> frame -> loc -> val -> Prop := + | extcall_arg_reg: forall rs fr r, + extcall_arg rs fr (R r) (rs r) + | extcall_arg_stack: forall rs fr ofs ty v, + get_slot fr ty (Int.signed (Int.repr (4 * ofs))) v -> + extcall_arg rs fr (S (Outgoing ofs ty)) v. + +Inductive extcall_args: regset -> frame -> list loc -> list val -> Prop := + | extcall_args_nil: forall rs fr, + extcall_args rs fr nil nil + | extcall_args_cons: forall rs fr l1 ll v1 vl, + extcall_arg rs fr l1 v1 -> extcall_args rs fr ll vl -> + extcall_args rs fr (l1 :: ll) (v1 :: vl). + +Definition extcall_arguments + (rs: regset) (fr: frame) (sg: signature) (args: list val) : Prop := + extcall_args rs fr (Conventions.loc_arguments sg) args. + Section RELSEM. Variable ge: genv. @@ -223,7 +243,7 @@ with exec_function: | exec_funct_external: forall ef parent args res rs1 rs2 m t, event_match ef args t res -> - args = rs1##(Conventions.loc_external_arguments ef.(ef_sig)) -> + extcall_arguments rs1 parent ef.(ef_sig) args -> rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) -> exec_function (External ef) parent rs1 m t rs2 m. @@ -367,7 +387,7 @@ Lemma exec_mutual_induction: (res : val) (rs1 : mreg -> val) (rs2 : RegEq.t -> val) (m : mem) (t0 : trace), event_match ef args t0 res -> - args = rs1 ## (Conventions.loc_external_arguments (ef_sig ef)) -> + extcall_arguments rs1 parent ef.(ef_sig) args -> rs2 = rs1 # (Conventions.loc_result (ef_sig ef)) <- res -> P2 (External ef) parent rs1 m t0 rs2 m) -> (forall (f16 : function) (v : val) (f17 : frame) (c : code) |