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

5 files changed, 43 insertions, 37 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index cb26b72..95f4209 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -17,12 +17,10 @@ let linker_options = ref ([]: string list)
 let exe_name = ref "a.out"
 let option_flonglong = ref true
 let option_flongdouble = ref false
-let option_fstruct_passing = ref false
-let option_fstruct_assign = ref false
+let option_fstruct_return = ref false
 let option_fbitfields = ref false
 let option_fvararg_calls = ref true
 let option_fpacked_structs = ref false
-let option_fvolatile_rmw = ref true
 let option_fmadd = ref false
 let option_fsse = ref true
 let option_dparse = ref false
diff --git a/driver/Compiler.v b/driver/Compiler.v
index ce9db20..6779aaf 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -400,7 +400,7 @@ Theorem transf_cstrategy_program_correct:
   forall p tp,
   transf_c_program p = OK tp ->
   forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)
-  * backward_simulation (Cstrategy.semantics p) (Asm.semantics tp).
+  * backward_simulation (atomic (Cstrategy.semantics p)) (Asm.semantics tp).
 Proof.
   intros.
   assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)).
@@ -411,8 +411,9 @@ Proof.
   exact (fst (transf_clight_program_correct _ _ EQ1)). 
 
   split. auto. 
-  apply forward_to_backward_simulation. auto. 
-  apply Cstrategy.semantics_receptive.
+  apply forward_to_backward_simulation.
+  apply factor_forward_simulation. auto. eapply sd_traces. eapply Asm.semantics_determinate.
+  apply atomic_receptive. apply Cstrategy.semantics_strongly_receptive.
   apply Asm.semantics_determinate.
 Qed.
 
@@ -422,7 +423,11 @@ Theorem transf_c_program_correct:
   backward_simulation (Csem.semantics p) (Asm.semantics tp).
 Proof.
   intros. 
-  eapply compose_backward_simulation.
+  apply compose_backward_simulation with (atomic (Cstrategy.semantics p)).
+  eapply sd_traces; eapply Asm.semantics_determinate.
+  apply factor_backward_simulation. 
   apply Cstrategy.strategy_simulation.
+  apply Csem.semantics_single_events.
+  eapply ssr_well_behaved; eapply Cstrategy.semantics_strongly_receptive.
   exact (snd (transf_cstrategy_program_correct _ _ H)).
 Qed.
diff --git a/driver/Complements.v b/driver/Complements.v
index 1b7e974..57351a2 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -78,15 +78,21 @@ Theorem transf_cstrategy_program_preservation:
      program_behaves (Asm.semantics tp) beh ->
      program_behaves (Cstrategy.semantics p) beh).
 Proof.
+  assert (WBT: forall p, well_behaved_traces (Cstrategy.semantics p)).
+    intros. eapply ssr_well_behaved. apply Cstrategy.semantics_strongly_receptive.
   intros. intuition.
   eapply forward_simulation_behavior_improves; eauto. 
     apply (fst (transf_cstrategy_program_correct _ _ H)).
-  eapply backward_simulation_behavior_improves; eauto. 
+  exploit backward_simulation_behavior_improves.
     apply (snd (transf_cstrategy_program_correct _ _ H)).
+    eauto.
+  intros [beh1 [A B]]. exists beh1; split; auto. rewrite atomic_behaviors; auto.
   eapply forward_simulation_same_safe_behavior; eauto.
     apply (fst (transf_cstrategy_program_correct _ _ H)).
-  eapply backward_simulation_same_safe_behavior; eauto.
+  exploit backward_simulation_same_safe_behavior.
     apply (snd (transf_cstrategy_program_correct _ _ H)).
+    intros. rewrite <- atomic_behaviors in H2; eauto. eauto.
+    intros. rewrite atomic_behaviors; auto. 
 Qed.
 
 (** We can also use the alternate big-step semantics for [Cstrategy]
diff --git a/driver/Driver.ml b/driver/Driver.ml
index cee6250..9813939 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -69,11 +69,9 @@ let parse_c_file sourcename ifile =
   (* Simplification options *)
   let simplifs =
     "b" (* blocks: mandatory *)
-  ^ (if !option_fstruct_passing then "s" else "")
-  ^ (if !option_fstruct_assign then "S" else "")
+  ^ (if !option_fstruct_return then "s" else "")
   ^ (if !option_fbitfields then "f" else "")
   ^ (if !option_fpacked_structs then "p" else "")
-  ^ (if !option_fvolatile_rmw then "v" else "")
   in
   (* Parsing and production of a simplified C AST *)
   let ast =
@@ -333,10 +331,8 @@ Language support options (use -fno-<opt> to turn off -f<opt>) :
   -fbitfields    Emulate bit fields in structs [off]
   -flonglong     Partial emulation of 'long long' types [on]
   -flongdouble   Treat 'long double' as 'double' [off]
-  -fstruct-passing  Emulate passing structs and unions by value [off]
-  -fstruct-assign   Emulate assignment between structs or unions [off]
+  -fstruct-return  Emulate returning structs and unions by value [off]
   -fvararg-calls Emulate calls to variable-argument functions [on]
-  -fvolatile-rmw Emulate ++, -- and op= on volatile l-values [on]
   -fpacked-structs  Emulate packed structs [off]
   -fall          Activate all language support options above
   -fnone         Turn off all language support options above
@@ -374,9 +370,8 @@ Interpreter mode:
 "
 
 let language_support_options = [
-  option_fbitfields; option_flonglong; option_flongdouble; option_fstruct_passing;
-  option_fstruct_assign; option_fvararg_calls; option_fpacked_structs;
-  option_fvolatile_rmw
+  option_fbitfields; option_flonglong; option_flongdouble;
+  option_fstruct_return; option_fvararg_calls; option_fpacked_structs
 ]
 
 let cmdline_actions =
@@ -434,14 +429,12 @@ let cmdline_actions =
   ]
   @ f_opt "longlong" option_flonglong
   @ f_opt "longdouble" option_flongdouble
-  @ f_opt "struct-passing" option_fstruct_passing
-  @ f_opt "struct-assign" option_fstruct_assign
+  @ f_opt "struct-return" option_fstruct_return
   @ f_opt "bitfields" option_fbitfields
   @ f_opt "vararg-calls" option_fvararg_calls
   @ f_opt "madd" option_fmadd
   @ f_opt "packed-structs" option_fpacked_structs
   @ f_opt "sse" option_fsse
-  @ f_opt "volatile-rmw" option_fvolatile_rmw
 
 let _ =
   Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 };
diff --git a/driver/Interp.ml b/driver/Interp.ml
index a1e01f0..50e512b 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -113,12 +113,15 @@ let print_state prog p = function
   | Returnstate(res, k, m) ->
       fprintf p "returning@ %a"
               print_val res
+  | Stuckstate ->
+      fprintf p "stuck after an undefined expression"
 
 let mem_of_state = function
   | State(f, s, k, e, m) -> m
   | ExprState(f, r, k, e, m) -> m
   | Callstate(fd, args, k, m) -> m
   | Returnstate(res, k, m) -> m
+  | Stuckstate -> assert false
 
 (* Comparing memory states *)
 
@@ -211,6 +214,7 @@ let rank_state = function
   | ExprState _ -> 1
   | Callstate _ -> 2
   | Returnstate _ -> 3
+  | Stuckstate -> 4
 
 let compare_state s1 s2 =
   if s1 == s2 then 0 else
@@ -382,16 +386,17 @@ let do_step p prog ge time s =
         exit (Int32.to_int (camlint_of_coqint r))
       end
   | None ->
-      match Cexec.do_step ge world s with
-      | [] ->
-          if !trace = 1 then
-            fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s;
-          fprintf p "ERROR: Undefined behavior@.";
-          fprintf p "@].";
-          exit 126
-      | l ->
-          List.iter (fun (t, s') -> do_events p ge time s t) l;
-          List.map snd l
+      let l = Cexec.do_step ge world s in
+      if l = [] || List.exists (fun (t,s) -> s = Stuckstate) l then begin
+        if !trace = 1 then
+          fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s;
+        fprintf p "ERROR: Undefined behavior@.";
+        fprintf p "@].";
+        exit 126
+      end else begin
+        List.iter (fun (t, s') -> do_events p ge time s t) l;
+        List.map snd l
+      end
 
 let rec explore p prog ge time ss =
   let succs =
@@ -415,14 +420,13 @@ let unvolatile prog =
   {prog with prog_vars = List.map unvolatile_globvar prog.prog_vars}
 
 let change_main_function p old_main old_main_ty =
-  let tint = Tint(I32, Signed) in
   let old_main = Evalof(Evar(old_main, old_main_ty), old_main_ty) in
-  let arg1 = Eval(Vint(coqint_of_camlint 0l), tint) in
+  let arg1 = Eval(Vint(coqint_of_camlint 0l), type_int32s) in
   let arg2 = arg1 in
   let body =
-    Sreturn(Some(Ecall(old_main, Econs(arg1, Econs(arg2, Enil)), tint))) in
+    Sreturn(Some(Ecall(old_main, Econs(arg1, Econs(arg2, Enil)), type_int32s))) in
   let new_main_fn =
-    { fn_return = tint; fn_params = []; fn_vars = []; fn_body = body } in
+    { fn_return = type_int32s; fn_params = []; fn_vars = []; fn_body = body } in
   let new_main_id = intern_string "___main" in
   { p with
     prog_main = new_main_id;
@@ -431,9 +435,9 @@ let change_main_function p old_main old_main_ty =
 let fixup_main p =
   try
     match type_of_fundef (List.assoc p.prog_main p.prog_funct) with
-    | Tfunction(Tnil, Tint(I32, Signed)) ->
+    | Tfunction(Tnil, Tint(I32, Signed, _)) ->
         Some p
-    | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_))), Tnil)),
+    | Tfunction(Tcons(Tint _, Tcons(Tpointer(Tpointer(Tint(I8,_,_),_),_), Tnil)),
                 Tint _) as ty ->
         Some (change_main_function p p.prog_main ty)
     | _ ->