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

4 files changed, 71 insertions, 26 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 7174f79..2d71ca9 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -508,12 +508,6 @@ Definition compare_float (rs: regset) (v1 v2: val) :=
     #CR0_2 <- (Val.cmpf Ceq v1 v2)
     #CR0_3 <- Vundef.
 
-Definition val_cond_reg (rs: regset) :=
-  Val.or (Val.shl rs#CR0_0 (Vint (Int.repr 31)))
-  (Val.or (Val.shl rs#CR0_1 (Vint (Int.repr 30)))
-   (Val.or (Val.shl rs#CR0_2 (Vint (Int.repr 29)))
-            (Val.shl rs#CR0_3 (Vint (Int.repr 28))))).
-
 (** Execution of a single instruction [i] in initial state
     [rs] and [m].  Return updated state.  For instructions
     that correspond to actual PowerPC instructions, the cases are
@@ -968,7 +962,7 @@ Ltac Equalities :=
   exploit external_call_determ. eexact H3. eexact H8. intros [A B].
   split. auto. intros. destruct B; auto. subst. auto.
 (* trace length *)
-  inv H; simpl.
+  red; intros. inv H; simpl.
   omega.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index e566e3c..f6c1c49 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -202,8 +202,8 @@ let name_of_section_MacOS = function
 
 let name_of_section_Linux = function
   | Section_text -> ".text"
-  | Section_data i -> ".data" (*if i then ".data" else ".bss"*)
-  | Section_small_data i -> ".sdata" (*if i then ".sdata" else ".sbss"*)
+  | Section_data i -> if i then ".data" else "COMM"
+  | Section_small_data i -> if i then ".sdata" else "COMM"
   | Section_const -> ".rodata"
   | Section_small_const -> ".sdata2"
   | Section_string -> ".rodata"
@@ -238,7 +238,9 @@ let name_of_section =
   | Diab  -> name_of_section_Diab
 
 let section oc sec =
-  fprintf oc "	%s\n" (name_of_section sec)
+  let name = name_of_section sec in
+  assert (name <> "COMM");
+  fprintf oc "	%s\n" name
 
 (* Encoding masks for rlwinm instructions *)
 
@@ -663,8 +665,8 @@ let print_instruction oc = function
   | Plwzx(r1, r2, r3) ->
       fprintf oc "	lwzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pmfcrbit(r1, bit) ->
-      fprintf oc "	mfcr	%a\n" ireg GPR12;
-      fprintf oc "	rlwinm	%a, %a, %d, 31, 31\n" ireg r1  ireg GPR12  (1 + num_crbit bit)
+      fprintf oc "	mfcr	%a\n" ireg r1;
+      fprintf oc "	rlwinm	%a, %a, %d, 31, 31\n" ireg r1  ireg r1 (1 + num_crbit bit)
   | Pmflr(r1) ->
       fprintf oc "	mflr	%a\n" ireg r1
   | Pmr(r1, r2) ->
@@ -1012,21 +1014,32 @@ let print_var oc (name, v) =
       let init =
         match v.gvar_init with [Init_space _] -> false | _ -> true in
       let sec =
-        Sections.section_for_variable name init
-      and align =
+        Sections.section_for_variable name init in
+      let align =
         match C2C.atom_alignof name with
         | Some a -> log2 a
-        | None -> 3 (* 8-alignment is a safe default *)
-      in
-      section oc sec;
-      fprintf oc "	.align	%d\n" align;
-      if not (C2C.atom_is_static name) then
-        fprintf oc "	.globl	%a\n" symbol name;
-      fprintf oc "%a:\n" symbol name;
-      print_init_data oc name v.gvar_init;
-      if target <> MacOS then begin
-        fprintf oc "	.type	%a, @object\n" symbol name;
-        fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
+        | None -> 3 in (* 8-alignment is a safe default *)
+      let name_sec =
+        name_of_section sec in
+      if name_sec <> "COMM" then begin
+        fprintf oc "	%s\n" name_sec;
+        fprintf oc "	.align	%d\n" align;
+        if not (C2C.atom_is_static name) then
+          fprintf oc "	.globl	%a\n" symbol name;
+        fprintf oc "%a:\n" symbol name;
+        print_init_data oc name v.gvar_init;
+        if target <> MacOS then begin
+          fprintf oc "	.type	%a, @object\n" symbol name;
+          fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
+        end
+      end else begin
+        let sz =
+          match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
+        fprintf oc "	%s	%a, %ld, %d\n"
+          (if C2C.atom_is_static name then ".lcomm" else ".comm")
+          symbol name
+          (camlint_of_coqint sz)
+          (1 lsl align)
       end
 
 let print_program oc p =
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 3bb5544..08968f7 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -69,7 +69,20 @@ Nondetfunction notint (e: expr) :=
   | _ => Elet e (Eop Onor (Eletvar O ::: Eletvar O ::: Enil))
   end.
 
-(** ** Boolean negation *)
+(** ** Boolean value and boolean negation *)
+
+Fixpoint boolval (e: expr) {struct e} : expr :=
+  let default := Eop (Ocmp (Ccompuimm Cne Int.zero)) (e ::: Enil) in
+  match e with 
+  | Eop (Ointconst n) Enil =>
+      Eop (Ointconst (if Int.eq n Int.zero then Int.zero else Int.one)) Enil
+  | Eop (Ocmp cond) args =>
+      Eop (Ocmp cond) args
+  | Econdition e1 e2 e3 =>
+      Econdition e1 (boolval e2) (boolval e3)
+  | _ =>
+      default
+  end.
 
 Fixpoint notbool (e: expr) {struct e} : expr :=
   let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index cc14d33..59f2a41 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -148,6 +148,31 @@ Proof.
   simpl. destruct x; simpl; auto. rewrite Int.or_idem. auto.
 Qed.
 
+Theorem eval_boolval: unary_constructor_sound boolval Val.boolval.
+Proof.
+  assert (DFL: 
+    forall le a x,
+    eval_expr ge sp e m le a x ->
+     exists v, eval_expr ge sp e m le (Eop (Ocmp (Ccompuimm Cne Int.zero)) (a ::: Enil)) v
+           /\ Val.lessdef (Val.boolval x) v).
+  intros. TrivialExists. simpl. destruct x; simpl; auto.
+
+  red. induction a; simpl; intros; eauto. destruct o; eauto.
+(* intconst *)
+  destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto.
+(* cmp *)
+  inv H. simpl in H5.
+  destruct (eval_condition c vl m) as []_eqn. 
+  TrivialExists. simpl. inv H5. rewrite Heqo. destruct b; auto.
+  simpl in H5. inv H5. 
+  exists Vundef; split; auto. EvalOp; simpl. rewrite Heqo; auto.
+
+(* condition *)
+  inv H. destruct v1.
+  exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
+  exploit IHa2; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. 
+Qed.
+
 Theorem eval_notbool: unary_constructor_sound notbool Val.notbool.
 Proof.
   assert (DFL: