Merge of the "volatile" branch:

- native treatment of volatile accesses in CompCert C's semantics
- translation of volatile accesses to built-ins in SimplExpr
- native treatment of struct assignment and passing struct parameter by value
- only passing struct result by value remains emulated
- in cparser, remove emulations that are no longer used
- added C99's type _Bool and used it to express || and && more efficiently.


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

1 files changed, 23 insertions, 1 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index c9ee5b5..6d288a9 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -44,6 +44,7 @@ Inductive unary_operation : Type :=
   | Ocast8signed: unary_operation          (**r 8-bit sign extension  *)
   | Ocast16unsigned: unary_operation       (**r 16-bit zero extension  *)
   | Ocast16signed: unary_operation         (**r 16-bit sign extension *)
+  | Oboolval: unary_operation              (**r 0 if null, 1 if non-null *)
   | Onegint: unary_operation               (**r integer opposite *)
   | Onotbool: unary_operation              (**r boolean negation  *)
   | Onotint: unary_operation               (**r bitwise complement  *)
@@ -103,6 +104,7 @@ Inductive stmt : Type :=
   | Sstore : memory_chunk -> expr -> expr -> stmt
   | Scall : option ident -> signature -> expr -> list expr -> stmt
   | Stailcall: signature -> expr -> list expr -> stmt
+  | Sbuiltin : option ident -> external_function -> list expr -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: expr -> stmt -> stmt -> stmt
   | Sloop: stmt -> stmt
@@ -228,6 +230,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
   | Ocast8signed => Some (Val.sign_ext 8 arg)
   | Ocast16unsigned => Some (Val.zero_ext 16 arg)
   | Ocast16signed => Some (Val.sign_ext 16 arg)
+  | Oboolval => Some(Val.boolval arg)
   | Onegint => Some (Val.negint arg)
   | Onotbool => Some (Val.notbool arg)
   | Onotint => Some (Val.notint arg)
@@ -401,6 +404,12 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m)
         E0 (Callstate fd vargs (call_cont k) m')
 
+  | step_builtin: forall f optid ef bl k sp e m vargs t vres m',
+      eval_exprlist sp e m bl vargs ->
+      external_call ef ge vargs m t vres m' ->
+      step (State f (Sbuiltin optid ef bl) k sp e m)
+         t (State f Sskip k sp (set_optvar optid vres e) m')
+
   | step_seq: forall f s1 s2 k sp e m,
       step (State f (Sseq s1 s2) k sp e m)
         E0 (State f s1 (Kseq s2 k) sp e m)
@@ -505,9 +514,11 @@ Proof.
     intros. subst. inv H0. exists s1; auto.
   inversion H; subst; auto.
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. 
+  exists (State f Sskip k sp (set_optvar optid vres2 e) m2). econstructor; eauto. 
+  exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. 
   exists (Returnstate vres2 k m2). econstructor; eauto.
 (* trace length *)
-  inv H; simpl; try omega. eapply external_call_trace_length; eauto.
+  red; intros; inv H; simpl; try omega; eapply external_call_trace_length; eauto.
 Qed.
 
 (** * Alternate operational semantics (big-step) *)
@@ -608,6 +619,12 @@ with exec_stmt:
       eval_funcall m fd vargs t m' vres ->
       e' = set_optvar optid vres e ->
       exec_stmt f sp e m (Scall optid sig a bl) t e' m' Out_normal
+  | exec_Sbuiltin:
+      forall f sp e m optid ef bl t m' vargs vres e',
+      eval_exprlist ge sp e m bl vargs ->
+      external_call ef ge vargs m t vres m' ->
+      e' = set_optvar optid vres e ->
+      exec_stmt f sp e m (Sbuiltin optid ef bl) t e' m' Out_normal
   | exec_Sifthenelse:
       forall f sp e m a s1 s2 v b t e' m' out,
       eval_expr ge sp e m a v ->
@@ -884,6 +901,11 @@ Proof.
   constructor. reflexivity. traceEq.
   subst e'. constructor.
 
+(* builtin *)
+  econstructor; split.
+  apply star_one. econstructor; eauto. 
+  subst e'. constructor.
+
 (* ifthenelse *)
   destruct (H2 k) as [S [A B]].
   exists S; split.