Revised handling of annotation statements, and more generally built-in functions, and more generally external functions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 34 insertions, 11 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index d698524..fc29db0 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -130,7 +130,7 @@ Inductive instruction : Type :=
   | Paddi: ireg -> ireg -> constant -> instruction            (**r add immediate *)
   | Paddis: ireg -> ireg -> constant -> instruction           (**r add immediate high *)
   | Paddze: ireg -> ireg -> instruction                       (**r add Carry bit *)
-  | Pallocframe: Z -> int -> instruction                 (**r allocate new stack frame *)
+  | Pallocframe: Z -> int -> instruction                      (**r allocate new stack frame *)
   | Pand_: ireg -> ireg -> ireg -> instruction                (**r bitwise and *)
   | Pandc: ireg -> ireg -> ireg -> instruction                (**r bitwise and-complement *)
   | Pandi_: ireg -> ireg -> constant -> instruction           (**r and immediate and set conditions *)
@@ -154,7 +154,7 @@ Inductive instruction : Type :=
   | Peqv: ireg -> ireg -> ireg -> instruction                 (**r bitwise not-xor *)
   | Pextsb: ireg -> ireg -> instruction                       (**r 8-bit sign extension *)
   | Pextsh: ireg -> ireg -> instruction                       (**r 16-bit sign extension *)
-  | Pfreeframe: Z -> int -> instruction                  (**r deallocate stack frame and restore previous frame *)
+  | Pfreeframe: Z -> int -> instruction                       (**r deallocate stack frame and restore previous frame *)
   | Pfabs: freg -> freg -> instruction                        (**r float absolute value *)
   | Pfadd: freg -> freg -> freg -> instruction                (**r float addition *)
   | Pfcmpu: freg -> freg -> instruction                       (**r float comparison *)
@@ -215,7 +215,12 @@ Inductive instruction : Type :=
   | Pxori: ireg -> ireg -> constant -> instruction            (**r bitwise xor with immediate *)
   | Pxoris: ireg -> ireg -> constant -> instruction           (**r bitwise xor with immediate high *)
   | Plabel: label -> instruction                              (**r define a code label *)
-  | Pbuiltin: external_function -> list preg -> preg -> instruction. (**r built-in *)
+  | Pbuiltin: external_function -> list preg -> preg -> instruction (**r built-in function *)
+  | Pannot: external_function -> list annot_param -> instruction (**r annotation statement *)
+
+with annot_param : Type :=
+  | APreg: preg -> annot_param
+  | APstack: memory_chunk -> Z -> annot_param.
 
 (** The pseudo-instructions are the following:
 
@@ -740,6 +745,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr rs) m
   | Pbuiltin ef args res =>
       Error    (**r treated specially below *)
+  | Pannot ef args =>
+      Error    (**r treated specially below *)
   end.
 
 (** Translation of the LTL/Linear/Mach view of machine registers
@@ -803,20 +810,27 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
       Mem.loadv Mfloat64 m (Val.add (rs (IR GPR1)) (Vint (Int.repr bofs))) = Some v ->
       extcall_arg rs m (S (Outgoing ofs Tfloat)) v.
 
-Inductive extcall_args (rs: regset) (m: mem): list loc -> list val -> Prop :=
-  | extcall_args_nil:
-      extcall_args rs m nil nil
-  | extcall_args_cons: forall l1 ll v1 vl,
-      extcall_arg rs m l1 v1 -> extcall_args rs m ll vl ->
-      extcall_args rs m (l1 :: ll) (v1 :: vl).
-
 Definition extcall_arguments
     (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
-  extcall_args rs m (loc_arguments sg) args.
+  list_forall2 (extcall_arg rs m) (loc_arguments sg) args.
 
 Definition loc_external_result (sg: signature) : preg :=
   preg_of (loc_result sg).
 
+(** Extract the values of the arguments of an annotation. *)
+
+Inductive annot_arg (rs: regset) (m: mem): annot_param -> val -> Prop :=
+  | annot_arg_reg: forall r,
+      annot_arg rs m (APreg r) (rs r)
+  | annot_arg_stack: forall chunk ofs stk base v,
+      rs (IR GPR1) = Vptr stk base ->
+      Mem.load chunk m stk (Int.unsigned base + ofs) = Some v ->
+      annot_arg rs m (APstack chunk ofs) v.
+
+Definition annot_arguments
+    (rs: regset) (m: mem) (params: list annot_param) (args: list val) : Prop :=
+  list_forall2 (annot_arg rs m) params args.
+
 (** Execution of the instruction at [rs#PC]. *)
 
 Inductive state: Type :=
@@ -841,6 +855,15 @@ Inductive step: state -> trace -> state -> Prop :=
                                 #FPR12 <- Vundef #FPR13 <- Vundef
                                 #FPR0 <- Vundef #CTR <- Vundef
                                 #res <- v)) m')
+  | exec_step_annot:
+      forall b ofs c ef args rs m vargs t v m',
+      rs PC = Vptr b ofs ->
+      Genv.find_funct_ptr ge b = Some (Internal c) ->
+      find_instr (Int.unsigned ofs) c = Some (Pannot ef args) ->
+      annot_arguments rs m args vargs ->
+      external_call ef ge vargs m t v m' ->
+      step (State rs m) t
+           (State (nextinstr rs) m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
       rs PC = Vptr b Int.zero ->