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

6 files changed, 66 insertions, 2 deletions

diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index e3a6f704..244a73f0 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -90,6 +90,7 @@ let type_unary_operation = function
   | Ocast8unsigned -> tint, tint
   | Ocast16unsigned -> tint, tint
   | Onegint -> tint, tint
+  | Oboolval -> tint, tint
   | Onotbool -> tint, tint
   | Onotint -> tint, tint
   | Onegf -> tfloat, tfloat
@@ -134,6 +135,7 @@ let name_of_unary_operation = function
   | Ocast8unsigned -> "cast8unsigned"
   | Ocast16unsigned -> "cast16unsigned"
   | Onegint -> "negint"
+  | Oboolval -> "notbool"
   | Onotbool -> "notbool"
   | Onotint -> "notint"
   | Onegf -> "negf"
@@ -293,6 +295,22 @@ let rec type_stmt env blk ret s =
       with Error s ->
         raise (Error (sprintf "In call:\n%s" s))
       end
+  | Sbuiltin(optid, ef, el) ->
+      let sg = ef_sig ef in
+      let tel = type_exprlist env [] el in
+      begin try
+        unify_list (ty_of_sig_args sg.sig_args) tel;
+        let ty_res =
+          match sg.sig_res with
+          | None -> tint (*???*)
+          | Some t -> ty_of_typ t in
+        begin match optid with
+        | None -> ()
+        | Some id -> unify (type_var env id) ty_res
+        end
+      with Error s ->
+        raise (Error (sprintf "In builtin call:\n%s" s))
+      end
   | Sseq(s1, s2) ->
       type_stmt env blk ret s1;
       type_stmt env blk ret s2
diff --git a/backend/Cminor.v b/backend/Cminor.v
index c9ee5b5c..6d288a9e 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.
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 30884b18..110e735e 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -21,6 +21,7 @@ open Datatypes
 open BinPos
 open Integers
 open AST
+open PrintAST
 open Cminor
 
 (* Precedences and associativity -- like those of C *)
@@ -57,6 +58,7 @@ let name_of_unop = function
   | Ocast16unsigned -> "int16u"
   | Ocast16signed -> "int16s"
   | Onegint -> "-"
+  | Oboolval -> "(_Bool)"
   | Onotbool -> "!"
   | Onotint -> "~"
   | Onegf -> "-f"
@@ -193,6 +195,15 @@ let rec print_stmt p s =
                 print_expr e1
                 print_expr_list (true, el)
                 print_sig sg
+  | Sbuiltin(None, ef, el) ->
+      fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@])@;@]"
+                (name_of_external ef)
+                print_expr_list (true, el)
+  | Sbuiltin(Some id, ef, el) ->
+      fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]);@]@]"
+                (ident_name id)
+                (name_of_external ef)
+                print_expr_list (true, el)
   | Sseq(Sskip, s2) ->
       print_stmt p s2
   | Sseq(s1, Sskip) ->
diff --git a/backend/RTL.v b/backend/RTL.v
index 6a209412..9b27a172 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -360,7 +360,7 @@ Proof.
   exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. 
   exists (Returnstate s0 vres2 m2). econstructor; eauto.
 (* trace length *)
-  inv H; simpl; try omega.
+  red; intros; inv H; simpl; try omega.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 Qed.
diff --git a/backend/Selection.v b/backend/Selection.v
index 9c037b82..2d6c9017 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -112,6 +112,7 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
   | Cminor.Ocast16unsigned => cast16unsigned arg 
   | Cminor.Ocast16signed => cast16signed arg 
   | Cminor.Onegint => negint arg
+  | Cminor.Oboolval => boolval arg
   | Cminor.Onotbool => notbool arg
   | Cminor.Onotint => notint arg
   | Cminor.Onegf => negf arg
@@ -202,6 +203,8 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : stmt :=
       | None => Scall optid sg (sel_expr fn) (sel_exprlist args)
       | Some ef => Sbuiltin optid ef (sel_exprlist args)
       end
+  | Cminor.Sbuiltin optid ef args =>
+      Sbuiltin optid ef (sel_exprlist args)
   | Cminor.Stailcall sg fn args => 
       Stailcall sg (sel_expr fn) (sel_exprlist args)
   | Cminor.Sseq s1 s2 => Sseq (sel_stmt ge s1) (sel_stmt ge s2)
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 54d59b1c..9681c66b 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -212,6 +212,7 @@ Proof.
   apply eval_cast8signed; auto.
   apply eval_cast16unsigned; auto.
   apply eval_cast16signed; auto.
+  apply eval_boolval; auto.
   apply eval_negint; auto.
   apply eval_notbool; auto.
   apply eval_notint; auto.
@@ -619,6 +620,15 @@ Proof.
   eapply functions_translated; eauto. 
   apply sig_function_translated.
   constructor; auto. apply call_cont_commut; auto.
+  (* Sbuiltin *)
+  exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]].
+  exploit external_call_mem_extends; eauto. 
+  intros [vres' [m2 [A [B [C D]]]]].
+  left; econstructor; split.
+  econstructor. eauto. eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  constructor; auto.
+  destruct optid; simpl; auto. apply set_var_lessdef; auto.
   (* Seq *)
   left; econstructor; split. constructor. constructor; auto. constructor; auto.
   (* Sifthenelse *)