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, 38 insertions, 23 deletions

diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index a1ed8b33..88eb3c7b 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -68,6 +68,7 @@ Inductive stmt : Type :=
   | Sset : ident -> expr -> stmt
   | Sstore : memory_chunk -> expr -> expr -> stmt
   | Scall : option ident -> 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
@@ -84,32 +85,36 @@ with lbl_stmt : Type :=
 
 (** The variables can be either scalar variables
   (whose type, size and signedness are given by a [memory_chunk]
-  or array variables (of the indicated sizes).  The only operation
-  permitted on an array variable is taking its address. *)
+  or array variables (of the indicated sizes and alignment).
+  The only operation permitted on an array variable is taking its address. *)
 
 Inductive var_kind : Type :=
-  | Vscalar: memory_chunk -> var_kind
-  | Varray: Z -> var_kind.
+  | Vscalar(chunk: memory_chunk)
+  | Varray(sz al: Z).
 
 Definition sizeof (lv: var_kind) : Z :=
   match lv with
   | Vscalar chunk => size_chunk chunk
-  | Varray sz => Zmax 0 sz
+  | Varray sz al => Zmax 0 sz
+  end.
+
+Definition type_of_kind (lv: var_kind) : typ :=
+  match lv with
+  | Vscalar chunk => type_of_chunk chunk
+  | Varray _ _ => Tint
   end.
 
 (** Functions are composed of a return type, a list of parameter names
-  with associated memory chunks (parameters must be scalar), a list of
-  local variables with associated [var_kind] description, and a
+  with associated [var_kind] descriptions, a list of
+  local variables with associated [var_kind] descriptions, and a
   statement representing the function body.  *)
 
-Definition param_name (p: ident * memory_chunk) := fst p.
-Definition param_chunk (p: ident * memory_chunk) := snd p.
 Definition variable_name (v: ident * var_kind) := fst v.
 Definition variable_kind (v: ident * var_kind) := snd v.
 
 Record function : Type := mkfunction {
   fn_return: option typ;
-  fn_params: list (ident * memory_chunk);
+  fn_params: list (ident * var_kind);
   fn_vars: list (ident * var_kind);
   fn_temps: list ident;
   fn_body: stmt
@@ -120,7 +125,7 @@ Definition fundef := AST.fundef function.
 Definition program : Type := AST.program fundef var_kind.
 
 Definition fn_sig (f: function) :=
-  mksignature (List.map type_of_chunk (List.map param_chunk f.(fn_params)))
+  mksignature (List.map type_of_kind (List.map variable_kind f.(fn_params)))
               f.(fn_return).
 
 Definition funsig (fd: fundef) :=
@@ -129,13 +134,9 @@ Definition funsig (fd: fundef) :=
   | External ef => ef_sig ef
   end.
 
-Definition var_of_param (p: ident * memory_chunk) : ident * var_kind :=
-  (fst p, Vscalar (snd p)).
-
-Definition fn_variables (f: function) :=
-  List.map var_of_param f.(fn_params) ++ f.(fn_vars).
+Definition fn_variables (f: function) := f.(fn_params) ++ f.(fn_vars).
 
-Definition fn_params_names (f: function) := List.map param_name f.(fn_params).
+Definition fn_params_names (f: function) := List.map variable_name f.(fn_params).
 Definition fn_vars_names (f: function) := List.map variable_name f.(fn_vars).
 
 (** * Operational semantics *)
@@ -292,6 +293,10 @@ Definition block_of_binding (id_b_lv: ident * (block * var_kind)) :=
 Definition blocks_of_env (e: env) : list (block * Z * Z) :=
   List.map block_of_binding (PTree.elements e).
 
+Section RELSEM.
+
+Variable ge: genv.
+
 (** Initialization of local variables that are parameters.  The value
   of the corresponding argument is stored into the memory block
   bound to the parameter. *)
@@ -300,22 +305,26 @@ Definition val_normalized (v: val) (chunk: memory_chunk) : Prop :=
   Val.load_result chunk v = v.
 
 Inductive bind_parameters: env ->
-                           mem -> list (ident * memory_chunk) -> list val ->
+                           mem -> list (ident * var_kind) -> list val ->
                            mem -> Prop :=
   | bind_parameters_nil:
       forall e m,
       bind_parameters e m nil nil m
-  | bind_parameters_cons:
+  | bind_parameters_scalar:
       forall e m id chunk params v1 vl b m1 m2,
       PTree.get id e = Some (b, Vscalar chunk) ->
       val_normalized v1 chunk ->
       Mem.store chunk m b 0 v1 = Some m1 ->
       bind_parameters e m1 params vl m2 ->
-      bind_parameters e m ((id, chunk) :: params) (v1 :: vl) m2.
-
-Section RELSEM.
+      bind_parameters e m ((id, Vscalar chunk) :: params) (v1 :: vl) m2
+  | bind_parameters_array:
+      forall e m id sz al params v1 vl b m1 m2,
+      PTree.get id e = Some (b, Varray sz al) ->
+      extcall_memcpy_sem sz (Zmin al 4) 
+                   ge (Vptr b Int.zero :: v1 :: nil) m E0 Vundef m1 ->
+      bind_parameters e m1 params vl m2 ->
+      bind_parameters e m ((id, Varray sz al) :: params) (v1 :: vl) m2.
 
-Variable ge: genv.
 
 (* Evaluation of the address of a variable: 
    [eval_var_addr prg ge e id b] states that variable [id] 
@@ -459,6 +468,12 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Scall optid sig a bl) k e le m)
         E0 (Callstate fd vargs (Kcall optid f e le k) m)
 
+  | step_builtin: forall f optid ef bl k e le m vargs t vres m',
+      eval_exprlist e le m bl vargs ->
+      external_call ef ge vargs m t vres m' ->
+      step (State f (Sbuiltin optid ef bl) k e le m)
+         t (State f Sskip k e (Cminor.set_optvar optid vres le) m')
+
   | step_seq: forall f s1 s2 k e le m,
       step (State f (Sseq s1 s2) k e le m)
         E0 (State f s1 (Kseq s2 k) e le m)