Added animation of the CompCert C semantics (ccomp -interp)

test/regression: int main() so that interpretation works
Revised once more implementation of __builtin_memcpy (to check for PPC & ARM)


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

19 files changed, 2741 insertions, 455 deletions

diff --git a/.depend b/.depend
index dff1aea..fe8c4a7 100644
--- a/.depend
+++ b/.depend
@@ -90,9 +90,10 @@ $(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqli
 cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo
 cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo
 cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
+cfrontend/Cexec.vo cfrontend/Cexec.glob: cfrontend/Cexec.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo
 cfrontend/Initializers.vo cfrontend/Initializers.glob: cfrontend/Initializers.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
 cfrontend/Initializersproof.vo cfrontend/Initializersproof.glob: cfrontend/Initializersproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Globalenvs.vo common/Events.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Initializers.vo
-cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo
+cfrontend/SimplExpr.vo cfrontend/SimplExpr.glob: cfrontend/SimplExpr.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Clight.vo
 cfrontend/SimplExprspec.vo cfrontend/SimplExprspec.glob: cfrontend/SimplExprspec.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/AST.vo cfrontend/Csyntax.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo
 cfrontend/SimplExprproof.vo cfrontend/SimplExprproof.glob: cfrontend/SimplExprproof.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Smallstep.vo common/Globalenvs.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/SimplExpr.vo cfrontend/SimplExprspec.vo
 cfrontend/Clight.vo cfrontend/Clight.glob: cfrontend/Clight.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
@@ -101,5 +102,5 @@ cfrontend/Cshmgenproof.vo cfrontend/Cshmgenproof.glob: cfrontend/Cshmgenproof.v
 cfrontend/Csharpminor.vo cfrontend/Csharpminor.glob: cfrontend/Csharpminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo backend/Cminor.vo common/Smallstep.vo
 cfrontend/Cminorgen.vo cfrontend/Cminorgen.glob: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Memdata.vo cfrontend/Csharpminor.vo backend/Cminor.vo
 cfrontend/Cminorgenproof.vo cfrontend/Cminorgenproof.glob: cfrontend/Cminorgenproof.v lib/Coqlib.vo lib/Intv.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memdata.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Switch.vo cfrontend/Csharpminor.vo backend/Cminor.vo cfrontend/Cminorgen.vo
-driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo
+driver/Compiler.vo driver/Compiler.glob: driver/Compiler.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo common/Values.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Cexec.vo cfrontend/Clight.vo cfrontend/Csharpminor.vo backend/Cminor.vo backend/CminorSel.vo backend/RTL.vo backend/LTL.vo backend/LTLin.vo backend/Linear.vo backend/Mach.vo backend/Machsem.vo $(ARCH)/Asm.vo cfrontend/Initializers.vo cfrontend/SimplExpr.vo cfrontend/Cshmgen.vo cfrontend/Cminorgen.vo backend/Selection.vo backend/RTLgen.vo backend/Tailcall.vo backend/CastOptim.vo backend/Constprop.vo backend/CSE.vo backend/Allocation.vo backend/Tunneling.vo backend/Linearize.vo backend/CleanupLabels.vo backend/Reload.vo backend/Stacking.vo $(ARCH)/Asmgen.vo backend/RTLtyping.vo backend/LTLtyping.vo backend/LTLintyping.vo backend/Lineartyping.vo backend/Machtyping.vo cfrontend/SimplExprproof.vo cfrontend/Cshmgenproof.vo cfrontend/Cminorgenproof.vo backend/Selectionproof.vo backend/RTLgenproof.vo backend/Tailcallproof.vo backend/CastOptimproof.vo backend/Constpropproof.vo backend/CSEproof.vo backend/Allocproof.vo backend/Alloctyping.vo backend/Tunnelingproof.vo backend/Tunnelingtyping.vo backend/Linearizeproof.vo backend/Linearizetyping.vo backend/CleanupLabelsproof.vo backend/CleanupLabelstyping.vo backend/Reloadproof.vo backend/Reloadtyping.vo backend/Stackingproof.vo backend/Stackingtyping.vo $(ARCH)/Asmgenproof.vo
 driver/Complements.vo driver/Complements.glob: driver/Complements.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Behaviors.vo cfrontend/Csyntax.vo cfrontend/Csem.vo cfrontend/Cstrategy.vo cfrontend/Clight.vo backend/Cminor.vo backend/RTL.vo $(ARCH)/Asm.vo driver/Compiler.vo common/Errors.vo
diff --git a/Makefile b/Makefile
index c90b9d6..81d339f 100644
--- a/Makefile
+++ b/Makefile
@@ -71,7 +71,7 @@ BACKEND=\
 
 # C front-end modules (in cfrontend/)
 
-CFRONTEND=Csyntax.v Csem.v Cstrategy.v \
+CFRONTEND=Csyntax.v Csem.v Cstrategy.v Cexec.v \
   Initializers.v Initializersproof.v \
   SimplExpr.v SimplExprspec.v SimplExprproof.v \
   Clight.v Cshmgen.v Cshmgenproof.v \
@@ -114,7 +114,7 @@ ccomp.byte: driver/Configuration.ml
 runtime:
 	$(MAKE) -C runtime
 
-.PHONY: proof extraction cil ccomp ccomp.prof ccomp.byte runtime
+.PHONY: proof extraction cil ccomp ccomp.prof ccomp.byte cinterp cinterp.byte runtime
 
 all:
 	$(MAKE) proof
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index cc42f3c..44a7571 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -269,9 +269,7 @@ let print_annot_val oc txt args res =
 
 (* The ARM has strict alignment constraints. *)
 
-let print_builtin_memcpy oc sz al args =
-  let (dst, src) =
-    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
+let print_builtin_memcpy_small oc sz al src dst =
   let rec copy ofs sz ninstr =
     if sz >= 4 && al >= 4 then begin
       fprintf oc "	ldr	%a, [%a, #%d]\n" ireg IR14 ireg src ofs;
@@ -287,10 +285,50 @@ let print_builtin_memcpy oc sz al args =
       copy (ofs + 1) (sz - 1) (ninstr + 2)
     end else
       ninstr in
-  fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n"
+  copy 0 sz 0
+
+let print_builtin_memcpy_big oc sz al src dst =
+  assert (sz >= al);
+  assert (sz mod al = 0);
+  let (load, store, chunksize) =
+    if al >= 4 then ("ldr", "str", 4)
+    else if al = 2 then ("ldrh", "strh", 2)
+    else ("ldrb", "strb", 1) in
+  let tmp =
+    if src <> IR0 && dst <> IR0 then IR0
+    else if src <> IR1 && dst <> IR1 then IR1
+    else IR2 in
+  fprintf oc "	stmfd	sp!, {%a,%a,%a}\n" ireg tmp ireg src ireg dst;
+  begin match Asmgen.decompose_int
+                 (coqint_of_camlint (Int32.of_int (sz / chunksize))) with
+  | [] -> assert false
+  | hd::tl ->
+      fprintf oc "	mov	%a, #%a\n" ireg IR14 coqint hd;
+      List.iter
+        (fun n ->
+           fprintf oc "	orr	%a, %a, #%a\n" ireg IR14 ireg IR14 coqint n)
+        tl
+  end;
+  let lbl = new_label() in
+  fprintf oc ".L%d:	%s	%a, [%a], #%d\n" lbl load ireg tmp ireg src chunksize;
+  fprintf oc "	subs	%a, %a, #1\n" ireg IR14 ireg IR14;
+  fprintf oc "	%s	%a, [%a], #%d\n" store ireg tmp ireg dst chunksize;
+  fprintf oc "	bne	.L%d\n" lbl;
+  fprintf oc "	ldmfd	sp!, {%a,%a,%a}\n" ireg tmp ireg src ireg dst;
+  9
+
+let print_builtin_memcpy oc sz al args =
+  let (dst, src) =
+    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
+  fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n"
           comment sz al;
-  let n = copy 0 sz 0 in
-  fprintf oc "%s end builtin __builtin_memcpy\n" comment; n
+  let n =
+    if sz <= 64
+    then print_builtin_memcpy_small oc sz al src dst
+    else print_builtin_memcpy_big oc sz al src dst in
+  fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment; n
+
+(* Handling of volatile reads and writes *)
 
 let print_builtin_vload oc chunk args res =
   fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
@@ -351,46 +389,6 @@ let print_builtin_inline oc name args res =
   fprintf oc "%s end %s\n" comment name;
   n
 
-(* Handling of other builtins *)
-
-let re_builtin_function = Str.regexp "__builtin_"
-
-let is_builtin_function s =
-  Str.string_match re_builtin_function (extern_atom s) 0
-
-let print_memcpy oc load store sz log2sz =
-  let lbl1 = new_label() in
-  let lbl2 = new_label() in
-  if sz = 1
-  then fprintf oc "	cmp	%a, #0\n" ireg IR2
-  else fprintf oc "	movs	%a, %a, lsr #%d\n" ireg IR2 ireg IR2 log2sz;
-  fprintf oc "	beq	.L%d\n" lbl1;
-  fprintf oc ".L%d:	%s	%a, [%a], #%d\n" lbl2 load ireg IR3 ireg IR1 sz;
-  fprintf oc "	subs	%a, %a, #1\n" ireg IR2 ireg IR2;
-  fprintf oc "	%s	%a, [%a], #%d\n" store ireg IR3 ireg IR0 sz;
-  fprintf oc "	bne	.L%d\n" lbl2;
-  fprintf oc ".L%d:\n" lbl1;
-  7
-
-let print_builtin_function oc s =
-  fprintf oc "%s begin %s\n" comment (extern_atom s);
-  (* int args: IR0-IR3     float args: FR0, FR1
-     int res:  IR0        float res:  FR0 *)
-  let n = match extern_atom s with
-  (* Block copy *)
-  | "__builtin_memcpy" ->
-      print_memcpy oc "ldrb" "strb" 1 0
-  | "__builtin_memcpy_al2" ->
-      print_memcpy oc "ldrh" "strh" 2 1
-  | "__builtin_memcpy_al4" | "__builtin_memcpy_al8" ->
-      print_memcpy oc "ldr" "str" 4 2
-  (* Catch-all *)
-  | s ->
-      invalid_arg ("unrecognized builtin function " ^ s)
-  in
-  fprintf oc "%s end %s\n" comment (extern_atom s);
-  n
-
 (* Printing of instructions *)
 
 let shift_op oc = function
@@ -424,21 +422,11 @@ let print_instruction oc = function
   | Pbc(bit, lbl) ->
       fprintf oc "	b%s	%a\n" (condition_name bit) print_label lbl; 1
   | Pbsymb id ->
-      if not (is_builtin_function id) then begin
-        fprintf oc "	b	%a\n" print_symb id; 1
-      end else begin
-        let n = print_builtin_function oc id in
-        fprintf oc "	mov	pc, r14\n";
-        n + 1
-      end
+      fprintf oc "	b	%a\n" print_symb id; 1
   | Pbreg r ->
       fprintf oc "	mov	pc, %a\n" ireg r; 1
   | Pblsymb id ->
-      if not (is_builtin_function id) then begin
-        fprintf oc "	bl	%a\n" print_symb id; 1
-      end else begin
-        print_builtin_function oc id
-      end
+      fprintf oc "	bl	%a\n" print_symb id; 1
   | Pblreg r ->
       fprintf oc "	mov	lr, pc\n";
       fprintf oc "	mov	pc, %a\n" ireg r; 2
@@ -658,9 +646,8 @@ let print_fundef oc (Coq_pair(name, defn)) =
   match defn with
   | Internal code ->
       print_function oc name code
-  | External ef ->
-      if need_stub ef && not(is_builtin_function name)
-      then print_external_function oc name (ef_sig ef)
+  | External ef
+      if need_stub ef then print_external_function oc name (ef_sig ef)
 
 (* Data *)
 
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 225905a..f8905a6 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -72,28 +72,11 @@ let builtins_generic = {
     "__builtin_fabs",
       (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
     (* Block copy *)
-    "__builtin_memcpy",
-         (TVoid [],
-           [TPtr(TVoid [], []); 
-            TPtr(TVoid [AConst], []); 
-            TInt(Cutil.size_t_ikind, [])],
-          false);
-    "__builtin_memcpy_al2",
-         (TVoid [],
-           [TPtr(TVoid [], []); 
-            TPtr(TVoid [AConst], []); 
-            TInt(Cutil.size_t_ikind, [])],
-          false);
-    "__builtin_memcpy_al4",
-         (TVoid [],
-           [TPtr(TVoid [], []); 
-            TPtr(TVoid [AConst], []); 
-            TInt(Cutil.size_t_ikind, [])],
-          false);
-    "__builtin_memcpy_al8",
+    "__builtin_memcpy_aligned",
          (TVoid [],
            [TPtr(TVoid [], []); 
             TPtr(TVoid [AConst], []); 
+            TInt(Cutil.size_t_ikind, []);
             TInt(Cutil.size_t_ikind, [])],
           false);
     (* Annotations *)
@@ -216,14 +199,10 @@ let register_annotation_val txt targ =
 
 (** ** Handling of inlined memcpy functions *)
 
-let register_inlined_memcpy basename sz =
+let register_inlined_memcpy sz al =
   let al =
-    match basename with
-    | "__builtin_memcpy_al2" -> 2l
-    | "__builtin_memcpy_al4" -> 4l
-    | "__builtin_memcpy_al8" -> 8l
-    | _ -> 1l in
-  let name = Printf.sprintf "%s_sz%ld" basename sz in
+    if al <= 4l then al else 4l in (* max alignment supported by CompCert *)
+  let name = Printf.sprintf "__builtin_memcpy_sz%ld_al%ld" sz al in
   let targs = Tcons(Tpointer Tvoid, Tcons(Tpointer Tvoid, Tnil))
   and tres = Tvoid
   and ef = EF_memcpy(coqint_of_camlint sz, coqint_of_camlint al) in
@@ -231,24 +210,21 @@ let register_inlined_memcpy basename sz =
   Evalof(Evar(intern_string name, Tfunction(targs, tres)),
          Tfunction(targs, tres))
 
-let memcpy_inline_threshold = ref 64l
-
-let make_builtin_memcpy name fn args =
+let make_builtin_memcpy args =
   match args with
-  | Econs(dst, Econs(src, Econs(sz, Enil))) ->
+  | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) ->
       let sz1 =
         match Initializers.constval sz with
-        | CompcertErrors.OK(Vint n) -> Some (camlint_of_coqint n)
-        | _ -> None in
-      begin match sz1 with
-      | Some sz2 when sz2 <= !memcpy_inline_threshold ->
-          let fn = register_inlined_memcpy name sz2 in
-          Ecall(fn, Econs(dst, Econs(src, Enil)), Tvoid)
-      | _ ->
-          Ecall(fn, args, Tvoid)
-      end
+        | CompcertErrors.OK(Vint n) -> camlint_of_coqint n
+        | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be a constant)"; 0l in
+      let al1 =
+        match Initializers.constval al with
+        | CompcertErrors.OK(Vint n) -> camlint_of_coqint n
+        | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; 0l in
+      let fn = register_inlined_memcpy sz1 al1 in
+      Ecall(fn, Econs(dst, Econs(src, Enil)), Tvoid)
   | _ ->
-    Ecall(fn, args, Tvoid)
+    assert false
 
 (** ** Translation functions *)
 
@@ -570,12 +546,8 @@ let rec convertExpr env e =
           ezero
       end          
 
- | C.ECall({edesc = C.EVar {name = ("__builtin_memcpy"
-                                    |"__builtin_memcpy_al2"
-                                    |"__builtin_memcpy_al4"
-                                    |"__builtin_memcpy_al8" as name)}} as fn,
-            args) ->
-      make_builtin_memcpy name (convertExpr env fn) (convertExprList env args)
+ | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) ->
+      make_builtin_memcpy (convertExprList env args)
 
   | C.ECall(fn, args) ->
       match projFunType env fn.etyp with
@@ -764,11 +736,6 @@ let convertFundef env fd =
 
 (** External function declaration *)
 
-let noninlined_builtin_functions = [
-    "__builtin_memcpy"; "__builtin_memcpy_al2";
-    "__builtin_memcpy_al4"; "__builtin_memcpy_al8"
-]
-
 let convertFundecl env (sto, id, ty, optinit) =
   let (args, res) =
     match convertTyp env ty with
@@ -777,8 +744,9 @@ let convertFundecl env (sto, id, ty, optinit) =
   let id' = intern_string id.name in
   let sg = signature_of_type args res in
   let ef =
+    if id.name = "malloc" then EF_malloc else
+    if id.name = "free" then EF_free else
     if List.mem_assoc id.name builtins.functions
-    && not (List.mem id.name noninlined_builtin_functions)
     then EF_builtin(id', sg)
     else EF_external(id', sg) in
   Datatypes.Coq_pair(id', External(ef, args, res))
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
new file mode 100644
index 0000000..3dd34c1
--- /dev/null
+++ b/cfrontend/Cexec.v
@@ -0,0 +1,1814 @@
+Require Import Axioms.
+Require Import Coqlib.
+Require Import Errors.
+Require Import Maps.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import AST.
+Require Import Memory.
+Require Import Events.
+Require Import Globalenvs.
+Require Import Determinism.
+Require Import Csyntax.
+Require Import Csem.
+Require Cstrategy.
+
+(** Animating the CompCert C semantics *)
+
+Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2}
+with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}
+with fieldlist_eq: forall (fld1 fld2: fieldlist), {fld1=fld2} + {fld1<>fld2}.
+Proof.
+  assert (forall (x y: intsize), {x=y} + {x<>y}). decide equality.
+  assert (forall (x y: signedness), {x=y} + {x<>y}). decide equality.
+  assert (forall (x y: floatsize), {x=y} + {x<>y}). decide equality.
+  generalize ident_eq zeq. intros E1 E2. 
+  decide equality.
+  decide equality.
+  generalize ident_eq. intros E1.
+  decide equality.
+Defined.
+
+Opaque type_eq.
+
+(** Error monad with options or lists *)
+
+Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end)
+  (at level 200, X ident, A at level 100, B at level 200)
+  : option_monad_scope.
+
+Notation " 'check' A ; B" := (if A then B else None)
+  (at level 200, A at level 100, B at level 200)
+  : option_monad_scope.
+
+Notation "'do' X <- A ; B" := (match A with Some X => B | None => nil end)
+  (at level 200, X ident, A at level 100, B at level 200)
+  : list_monad_scope.
+
+Notation " 'check' A ; B" := (if A then B else nil)
+  (at level 200, A at level 100, B at level 200)
+  : list_monad_scope.
+
+Definition is_val (a: expr) : option (val * type) :=
+  match a with
+  | Eval v ty => Some(v, ty)
+  | _ => None
+  end.
+
+Lemma is_val_inv:
+  forall a v ty, is_val a = Some(v, ty) -> a = Eval v ty.
+Proof.
+  intros until ty. destruct a; simpl; congruence.
+Qed.
+
+Definition is_loc (a: expr) : option (block * int * type) :=
+  match a with
+  | Eloc b ofs ty => Some(b, ofs, ty)
+  | _ => None
+  end.
+
+Lemma is_loc_inv:
+  forall a b ofs ty, is_loc a = Some(b, ofs, ty) -> a = Eloc b ofs ty.
+Proof.
+  intros until ty. destruct a; simpl; congruence.
+Qed.
+
+Local Open Scope option_monad_scope. 
+
+Fixpoint is_val_list (al: exprlist) : option (list (val * type)) :=
+  match al with
+  | Enil => Some nil
+  | Econs a1 al => do vt1 <- is_val a1; do vtl <- is_val_list al; Some(vt1::vtl)
+  end.
+
+Definition is_skip (s: statement) : {s = Sskip} + {s <> Sskip}.
+Proof.
+  destruct s; (left; congruence) || (right; congruence).
+Qed.
+
+(** * Reduction of expressions *)
+
+Section EXEC.
+
+Variable ge: genv.
+
+Inductive reduction: Type :=
+  | Lred (l': expr) (m': mem)
+  | Rred (r': expr) (m': mem)
+  | Callred (fd: fundef) (args: list val) (tyres: type) (m': mem).
+
+Section EXPRS.
+
+Variable e: env.
+
+Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) : option (list val) :=
+  match vtl, tl with
+  | nil, Tnil => Some nil
+  | (v1,t1)::vtl, Tcons t1' tl =>
+      do v <- sem_cast v1 t1 t1'; do vl <- sem_cast_arguments vtl tl; Some(v::vl)
+  | _, _ => None
+  end.
+
+(** The result of stepping an expression can be
+- [None] denoting that the expression is stuck;
+- [Some nil] meaning that the expression is fully reduced
+   (it's [Eval] for a r-value and [Eloc] for a l-value);
+- [Some ll] meaning that the expression can reduce to any of
+   the elements of [ll].  Each element is a pair of a context
+   and a reduction inside this context (see type [reduction] above).
+*)
+
+Definition reducts (A: Type): Type := option (list ((expr -> A) * reduction)).
+
+Definition topred (r: reduction) : reducts expr :=
+  Some (((fun (x: expr) => x), r) :: nil).
+
+Definition incontext {A B: Type} (ctx: A -> B) (r: reducts A) : reducts B :=
+  match r with
+  | None => None
+  | Some l => Some (map (fun z => ((fun (x: expr) => ctx(fst z x)), snd z)) l)
+  end.
+
+Definition incontext2 {A1 A2 B: Type}
+                     (ctx1: A1 -> B) (r1: reducts A1)
+                     (ctx2: A2 -> B) (r2: reducts A2) : reducts B :=
+  match r1, r2 with
+  | None, _ => None
+  | _, None => None
+  | Some l1, Some l2 =>
+      Some (map (fun z => ((fun (x: expr) => ctx1(fst z x)), snd z)) l1
+            ++ map (fun z => ((fun (x: expr) => ctx2(fst z x)), snd z)) l2)
+  end.
+
+Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr :=
+  match k, a with
+  | LV, Eloc b ofs ty =>
+      Some nil
+  | LV, Evar x ty =>
+      match e!x with
+      | Some(b, ty') =>
+          check type_eq ty ty';
+          topred (Lred (Eloc b Int.zero ty) m)
+      | None =>
+          do b <- Genv.find_symbol ge x;
+          do ty' <- type_of_global ge b;
+          check type_eq ty ty';
+          topred (Lred (Eloc b Int.zero ty) m)
+      end
+  | LV, Ederef r ty =>
+      match is_val r with
+      | Some(Vptr b ofs, ty') =>
+          topred (Lred (Eloc b ofs ty) m)
+      | Some _ =>
+          None
+      | None =>
+          incontext (fun x => Ederef x ty) (step_expr RV r m)
+      end
+  | LV, Efield l f ty =>
+      match is_loc l with
+      | Some(b, ofs, ty') =>
+          match ty' with
+          | Tstruct id fList =>
+              match field_offset f fList with
+              | Error _ => None
+              | OK delta => topred (Lred (Eloc b (Int.add ofs (Int.repr delta)) ty) m)
+              end
+          | Tunion id fList =>
+              topred (Lred (Eloc b ofs ty) m)
+          | _ => None
+          end
+      | None =>
+          incontext (fun x => Efield x f ty) (step_expr LV l m)
+      end
+  | RV, Eval v ty =>
+      Some nil
+  | RV, Evalof l ty =>
+      match is_loc l with
+      | Some(b, ofs, ty') =>
+          check type_eq ty ty';
+          do v <- load_value_of_type ty m b ofs;
+          topred (Rred (Eval v ty) m)
+      | None =>
+          incontext (fun x => Evalof x ty) (step_expr LV l m)
+      end
+  | RV, Eaddrof l ty =>
+      match is_loc l with
+      | Some(b, ofs, ty') => topred (Rred (Eval (Vptr b ofs) ty) m)
+      | None => incontext (fun x => Eaddrof x ty) (step_expr LV l m)
+      end
+  | RV, Eunop op r1 ty =>
+      match is_val r1 with
+      | Some(v1, ty1) =>
+          do v <- sem_unary_operation op v1 ty1;
+          topred (Rred (Eval v ty) m)
+      | None =>
+          incontext (fun x => Eunop op x ty) (step_expr RV r1 m)
+      end
+  | RV, Ebinop op r1 r2 ty =>
+      match is_val r1, is_val r2 with
+      | Some(v1, ty1), Some(v2, ty2) =>
+          do v <- sem_binary_operation op v1 ty1 v2 ty2 m;
+          topred (Rred (Eval v ty) m)
+      | _, _ =>
+         incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m)
+                    (fun x => Ebinop op r1 x ty) (step_expr RV r2 m)
+      end
+  | RV, Ecast r1 ty =>
+      match is_val r1 with
+      | Some(v1, ty1) =>
+          do v <- sem_cast v1 ty1 ty;
+          topred (Rred (Eval v ty) m)
+      | None =>
+          incontext (fun x => Ecast x ty) (step_expr RV r1 m)
+      end
+  | RV, Econdition r1 r2 r3 ty =>
+      match is_val r1 with
+      | Some(v1, ty1) =>
+          do b <- bool_val v1 ty1;
+          topred (Rred (Eparen (if b then r2 else r3) ty) m)
+      | None =>
+          incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m)
+      end
+  | RV, Esizeof ty' ty =>
+      topred (Rred (Eval (Vint (Int.repr (sizeof ty'))) ty) m)
+  | RV, Eassign l1 r2 ty =>
+      match is_loc l1, is_val r2 with
+      | Some(b, ofs, ty1), Some(v2, ty2) =>
+          check type_eq ty1 ty;
+          do v <- sem_cast v2 ty2 ty1;
+          do m' <- store_value_of_type ty1 m b ofs v;
+          topred (Rred (Eval v ty) m')
+      | _, _ =>
+         incontext2 (fun x => Eassign x r2 ty) (step_expr LV l1 m)
+                    (fun x => Eassign l1 x ty) (step_expr RV r2 m)
+      end
+  | RV, Eassignop op l1 r2 tyres ty =>
+      match is_loc l1, is_val r2 with
+      | Some(b, ofs, ty1), Some(v2, ty2) =>
+          check type_eq ty1 ty;
+          do v1 <- load_value_of_type ty1 m b ofs;
+          do v <- sem_binary_operation op v1 ty1 v2 ty2 m;
+          do v' <- sem_cast v tyres ty1;
+          do m' <- store_value_of_type ty1 m b ofs v';
+          topred (Rred (Eval v' ty) m')
+      | _, _ =>
+         incontext2 (fun x => Eassignop op x r2 tyres ty) (step_expr LV l1 m)
+                    (fun x => Eassignop op l1 x tyres ty) (step_expr RV r2 m)
+      end
+  | RV, Epostincr id l ty =>
+      match is_loc l with
+      | Some(b, ofs, ty1) =>
+          check type_eq ty1 ty;
+          do v1 <- load_value_of_type ty m b ofs;
+          do v2 <- sem_incrdecr id v1 ty;
+          do v3 <- sem_cast v2 (typeconv ty) ty;
+          do m' <- store_value_of_type ty m b ofs v3;
+          topred (Rred (Eval v1 ty) m')
+      | None =>
+          incontext (fun x => Epostincr id x ty) (step_expr LV l m)
+      end
+  | RV, Ecomma r1 r2 ty =>
+      match is_val r1 with
+      | Some _ =>
+          check type_eq (typeof r2) ty;
+          topred (Rred r2 m)
+      | None =>
+          incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m)
+      end
+  | RV, Eparen r1 ty =>
+      match is_val r1 with
+      | Some (v1, ty1) =>
+          do v <- sem_cast v1 ty1 ty;
+          topred (Rred (Eval v ty) m)
+      | None =>
+          incontext (fun x => Eparen x ty) (step_expr RV r1 m)
+      end
+  | RV, Ecall r1 rargs ty =>
+      match is_val r1, is_val_list rargs with
+      | Some(vf, tyf), Some vtl =>
+          match classify_fun tyf with
+          | fun_case_f tyargs tyres =>
+              do fd <- Genv.find_funct ge vf;
+              do vargs <- sem_cast_arguments vtl tyargs;
+              check type_eq (type_of_fundef fd) (Tfunction tyargs tyres);
+              topred (Callred fd vargs ty m)
+          | _ => None
+          end
+      | _, _ =>
+          incontext2 (fun x => Ecall x rargs ty) (step_expr RV r1 m)
+                     (fun x => Ecall r1 x ty) (step_exprlist rargs m)
+      end
+  | _, _ => None
+  end
+
+with step_exprlist (rl: exprlist) (m: mem): reducts exprlist :=
+  match rl with
+  | Enil =>
+      Some nil
+  | Econs r1 rs =>
+      incontext2 (fun x => Econs x rs) (step_expr RV r1 m)
+                 (fun x => Econs r1 x) (step_exprlist rs m)
+  end.
+
+(** Soundness: if [step_expr] returns [Some ll], then every element
+  of [ll] is a reduct. *)
+
+Lemma context_compose:
+  forall k2 k3 C2, context k2 k3 C2 ->
+  forall k1 C1, context k1 k2 C1 ->
+  context k1 k3 (fun x => C2(C1 x))
+with contextlist_compose:
+  forall k2 C2, contextlist k2 C2 ->
+  forall k1 C1, context k1 k2 C1 ->
+  contextlist k1 (fun x => C2(C1 x)).
+Proof.
+  induction 1; intros; try (constructor; eauto).
+  replace (fun x => C1 x) with C1. auto. apply extensionality; auto.
+  induction 1; intros; constructor; eauto.
+Qed.
+
+Hint Constructors context contextlist.
+Hint Resolve context_compose contextlist_compose.
+
+Definition reduction_ok (a: expr) (m: mem) (rd: reduction) : Prop :=
+  match rd with
+  | Lred l' m' => lred ge e a m l' m'
+  | Rred r' m' => rred a m r' m'
+  | Callred fd args tyres m' => callred ge a fd args tyres /\ m' = m
+  end.
+
+Definition reduction_kind (rd: reduction): kind :=
+  match rd with
+  | Lred l' m' => LV
+  | Rred r' m' => RV
+  | Callred fd args tyres m' => RV
+  end.
+
+Ltac monadInv :=
+  match goal with
+  | [ H: match ?x with Some _ => _ | None => None end = Some ?y |- _ ] =>
+      destruct x as []_eqn; [monadInv|discriminate]
+  | [ H: match ?x with left _ => _ | right _ => None end = Some ?y |- _ ] =>
+      destruct x; [monadInv|discriminate]
+  | _ => idtac
+  end.
+
+Lemma sem_cast_arguments_sound:
+  forall rargs vtl tyargs vargs,
+  is_val_list rargs = Some vtl ->
+  sem_cast_arguments vtl tyargs = Some vargs ->
+  cast_arguments rargs tyargs vargs.
+Proof.
+  induction rargs; simpl; intros.
+  inv H. destruct tyargs; simpl in H0; inv H0. constructor.
+  monadInv. inv H. simpl in H0. destruct p as [v1 t1]. destruct tyargs; try congruence. monadInv.
+  inv H0. rewrite (is_val_inv _ _ _ Heqo). constructor. auto. eauto. 
+Qed.
+
+Definition reducts_ok (k: kind) (a: expr) (m: mem) (res: reducts expr) : Prop :=
+  match res with
+  | None => True
+  | Some nil => match k with LV => is_loc a <> None | RV => is_val a <> None end
+  | Some ll =>
+      forall C rd,
+      In (C, rd) ll ->
+      context (reduction_kind rd) k C /\ exists a', a = C a' /\ reduction_ok a' m rd
+  end.
+
+Definition list_reducts_ok (al: exprlist) (m: mem) (res: reducts exprlist) : Prop :=
+  match res with
+  | None => True
+  | Some nil => is_val_list al <> None
+  | Some ll =>
+      forall C rd,
+      In (C, rd) ll ->
+      contextlist (reduction_kind rd) C /\ exists a', al = C a' /\ reduction_ok a' m rd
+  end.
+
+Lemma topred_ok:
+  forall k a m rd,
+  reduction_ok a m rd ->
+  k = reduction_kind rd ->
+  reducts_ok k a m (topred rd).
+Proof.
+  intros. unfold topred; red. simpl; intros. destruct H1; try contradiction.
+  inv H1. split. auto. exists a; auto.
+Qed.
+
+Lemma incontext_ok:
+  forall k a m C res k' a',
+  reducts_ok k' a' m res ->
+  a = C a' ->
+  context k' k C ->
+  match k' with LV => is_loc a' = None | RV => is_val a' = None end ->
+  reducts_ok k a m (incontext C res).
+Proof.
+  unfold reducts_ok; intros. destruct res; simpl. destruct l.
+(* res = Some nil *)
+  destruct k'; congruence.
+(* res = Some nonempty-list *)
+  simpl map at 1. hnf. intros. 
+  exploit list_in_map_inv; eauto. intros [[C1 rd1] [P Q]]. inv P.
+  exploit H; eauto. intros [U [a'' [V W]]].
+  split. eapply context_compose; eauto. exists a''; split; auto. congruence. 
+(* res = None *)
+  auto.
+Qed.
+
+Remark incontext2_inv:
+  forall {A1 A2 B: Type} (C1: A1 -> B) res1 (C2: A2 -> B) res2,
+  match incontext2 C1 res1 C2 res2 with
+  | None => res1 = None \/ res2 = None
+  | Some nil => res1 = Some nil /\ res2 = Some nil
+  | Some ll => 
+      exists ll1, exists ll2,
+      res1 = Some ll1 /\ res2 = Some ll2 /\
+      forall C rd, In (C, rd) ll ->
+      (exists C', C = (fun x => C1(C' x)) /\ In (C', rd) ll1)
+      \/ (exists C', C = (fun x => C2(C' x)) /\ In (C', rd) ll2)
+  end.
+Proof.
+  intros. unfold incontext2. destruct res1 as [ll1|]; auto. destruct res2 as [ll2|]; auto.
+  set (ll := map
+    (fun z : (expr -> A1) * reduction =>
+     (fun x : expr => C1 (fst z x), snd z)) ll1 ++
+  map
+    (fun z : (expr -> A2) * reduction =>
+     (fun x : expr => C2 (fst z x), snd z)) ll2).
+  destruct ll as []_eqn.
+  destruct (app_eq_nil _ _ Heql). 
+  split. destruct ll1; auto || discriminate. destruct ll2; auto || discriminate.
+  rewrite <- Heql. exists ll1; exists ll2. split. auto. split. auto.
+  unfold ll; intros.
+  rewrite in_app in H. destruct H.
+  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
+  left; exists C'; auto. 
+  exploit list_in_map_inv; eauto. intros [[C' rd'] [P Q]]. inv P.
+  right; exists C'; auto.
+Qed.
+
+Lemma incontext2_ok:
+  forall k a m k1 a1 res1 k2 a2 res2 C1 C2,
+  reducts_ok k1 a1 m res1 ->
+  reducts_ok k2 a2 m res2 ->
+  a = C1 a1 -> a = C2 a2 ->
+  context k1 k C1 -> context k2 k C2 ->
+  match k1 with LV => is_loc a1 = None | RV => is_val a1 = None end
+  \/ match k2 with LV => is_loc a2 = None | RV => is_val a2 = None end ->
+  reducts_ok k a m (incontext2 C1 res1 C2 res2).
+Proof.
+  unfold reducts_ok; intros.
+  generalize (incontext2_inv C1 res1 C2 res2). 
+  destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto.
+  destruct ll. 
+  intros [EQ1 EQ2]. subst. destruct H5. destruct k1; congruence. destruct k2; congruence.
+  intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. 
+  exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst.
+  destruct ll1; try contradiction. exploit H; eauto.
+  intros [U [a' [V W]]]. split. eauto. exists a'; split. congruence. auto. 
+  destruct ll2; try contradiction. exploit H0; eauto.
+  intros [U [a' [V W]]]. split. eauto. exists a'; split. congruence. auto.
+Qed.
+
+Lemma incontext2_list_ok:
+  forall a1 a2 ty m res1 res2,
+  reducts_ok RV a1 m res1 ->
+  list_reducts_ok a2 m res2 ->
+  is_val a1 = None \/ is_val_list a2 = None ->
+  reducts_ok RV (Ecall a1 a2 ty) m 
+               (incontext2 (fun x => Ecall x a2 ty) res1
+                           (fun x => Ecall a1 x ty) res2).
+Proof.
+  unfold reducts_ok, list_reducts_ok; intros.
+  set (C1 := fun x => Ecall x a2 ty). set (C2 := fun x => Ecall a1 x ty). 
+  generalize (incontext2_inv C1 res1 C2 res2). 
+  destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto.
+  destruct ll. 
+  intros [EQ1 EQ2]. subst. intuition congruence.
+  intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. 
+  exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst.
+  destruct ll1; try contradiction. exploit H; eauto.
+  intros [U [a' [V W]]]. split. unfold C1. auto. exists a'; split. unfold C1; congruence. auto. 
+  destruct ll2; try contradiction. exploit H0; eauto.
+  intros [U [a' [V W]]]. split. unfold C2. auto. exists a'; split. unfold C2; congruence. auto.
+Qed.
+
+Lemma incontext2_list_ok':
+  forall a1 a2 m res1 res2,
+  reducts_ok RV a1 m res1 ->
+  list_reducts_ok a2 m res2 ->
+  list_reducts_ok (Econs a1 a2) m
+               (incontext2 (fun x => Econs x a2) res1
+                           (fun x => Econs a1 x) res2).
+Proof.
+  unfold reducts_ok, list_reducts_ok; intros.
+  set (C1 := fun x => Econs x a2). set (C2 := fun x => Econs a1 x). 
+  generalize (incontext2_inv C1 res1 C2 res2). 
+  destruct (incontext2 C1 res1 C2 res2) as [ll|]; auto.
+  destruct ll. 
+  intros [EQ1 EQ2]. subst.
+  simpl. destruct (is_val a1); try congruence. destruct (is_val_list a2); congruence.
+  intros [ll1 [ll2 [EQ1 [EQ2 IN]]]]. subst. intros. 
+  exploit IN; eauto. intros [[C' [P Q]] | [C' [P Q]]]; subst.
+  destruct ll1; try contradiction. exploit H; eauto.
+  intros [U [a' [V W]]]. split. unfold C1. auto. exists a'; split. unfold C1; congruence. auto. 
+  destruct ll2; try contradiction. exploit H0; eauto.
+  intros [U [a' [V W]]]. split. unfold C2. auto. exists a'; split. unfold C2; congruence. auto.
+Qed.
+
+Ltac mysimpl :=
+  match goal with
+  | [ |- reducts_ok _ _ _ (match ?x with Some _ => _ | None => None end) ] =>
+      destruct x as []_eqn; [mysimpl|exact I]
+  | [ |- reducts_ok _ _ _ (match ?x with left _ => _ | right _ => None end) ] =>
+      destruct x as []_eqn; [subst;mysimpl|exact I]
+  | _ =>
+      idtac
+  end.
+
+Theorem step_expr_sound:
+  forall a k m, reducts_ok k a m (step_expr k a m)
+with step_exprlist_sound:
+  forall al m, list_reducts_ok al m (step_exprlist al m).
+Proof with try (exact I).
+  induction a; destruct k; intros; simpl...
+(* Eval *)
+  congruence.
+(* Evar *)
+  destruct (e!x) as [[b ty'] | ]_eqn; mysimpl.
+  apply topred_ok; auto. apply red_var_local; auto.
+  apply topred_ok; auto. apply red_var_global; auto.
+(* Efield *)
+  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn.
+  destruct ty'... 
+  (* top struct *)
+  destruct (field_offset f f0) as [delta|]_eqn...
+  rewrite (is_loc_inv _ _ _ _ Heqo). apply topred_ok; auto. apply red_field_struct; auto.
+  (* top union *)
+  rewrite (is_loc_inv _ _ _ _ Heqo). apply topred_ok; auto. apply red_field_union; auto.
+  (* in depth *)
+  eapply incontext_ok; eauto. 
+(* Evalof *)
+  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn.
+  (* top *)
+  mysimpl. apply topred_ok; auto. rewrite (is_loc_inv _ _ _ _ Heqo). apply red_rvalof; auto. 
+  (* depth *)
+  eapply incontext_ok; eauto.
+(* Ederef *)
+  destruct (is_val a) as [[v ty'] | ]_eqn.
+  (* top *)
+  destruct v... mysimpl. apply topred_ok; auto. rewrite (is_val_inv _ _ _ Heqo). apply red_deref; auto. 
+  (* depth *)
+  eapply incontext_ok; eauto.
+(* Eaddrof *)
+  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn.
+  (* top *)
+  apply topred_ok; auto. rewrite (is_loc_inv _ _ _ _ Heqo). apply red_addrof; auto. 
+  (* depth *)
+  eapply incontext_ok; eauto.
+(* unop *)
+  destruct (is_val a) as [[v ty'] | ]_eqn.
+  (* top *)
+  mysimpl. apply topred_ok; auto. rewrite (is_val_inv _ _ _ Heqo). apply red_unop; auto. 
+  (* depth *)
+  eapply incontext_ok; eauto.
+(* binop *)
+  destruct (is_val a1) as [[v1 ty1] | ]_eqn.
+  destruct (is_val a2) as [[v2 ty2] | ]_eqn.
+  (* top *)
+  mysimpl. apply topred_ok; auto. 
+  rewrite (is_val_inv _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). apply red_binop; auto.
+  (* depth *)
+  eapply incontext2_ok; eauto. 
+  eapply incontext2_ok; eauto. 
+(* cast *)
+  destruct (is_val a) as [[v ty'] | ]_eqn.
+  (* top *)
+  mysimpl. apply topred_ok; auto. 
+  rewrite (is_val_inv _ _ _ Heqo). apply red_cast; auto. 
+  (* depth *)
+  eapply incontext_ok; eauto.
+(* condition *)
+  destruct (is_val a1) as [[v ty'] | ]_eqn.
+  (* top *)
+  mysimpl. apply topred_ok; auto.
+  rewrite (is_val_inv _ _ _ Heqo). eapply red_condition; eauto.
+  (* depth *)
+  eapply incontext_ok; eauto.
+(* sizeof *)
+  apply topred_ok; auto. apply red_sizeof.
+(* assign *)
+  destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn.
+  destruct (is_val a2) as [[v2 ty2] | ]_eqn.
+  (* top *)
+  mysimpl. apply topred_ok; auto.
+  rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). apply red_assign; auto.
+  (* depth *)
+  eapply incontext2_ok; eauto.
+  eapply incontext2_ok; eauto.
+(* assignop *)
+  destruct (is_loc a1) as [[[b ofs] ty1] | ]_eqn.
+  destruct (is_val a2) as [[v2 ty2] | ]_eqn.
+  (* top *)
+  mysimpl. apply topred_ok; auto.
+  rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). eapply red_assignop; eauto.
+  (* depth *)
+  eapply incontext2_ok; eauto.
+  eapply incontext2_ok; eauto.
+(* postincr *)
+  destruct (is_loc a) as [[[b ofs] ty'] | ]_eqn.
+  (* top *)
+  mysimpl. apply topred_ok; auto.
+  rewrite (is_loc_inv _ _ _ _ Heqo). eapply red_postincr; eauto. 
+  (* depth *)
+  eapply incontext_ok; eauto.
+(* comma *)
+  destruct (is_val a1) as [[v ty'] | ]_eqn.
+  (* top *)
+  mysimpl. apply topred_ok; auto.
+  rewrite (is_val_inv _ _ _ Heqo). apply red_comma; auto. 
+  (* depth *)
+  eapply incontext_ok; eauto.
+(* call *)
+  destruct (is_val a) as [[vf tyf] | ]_eqn.
+  destruct (is_val_list rargs) as [vtl | ]_eqn.
+  (* top *)
+  destruct (classify_fun tyf) as [tyargs tyres|]_eqn...
+  mysimpl. apply topred_ok; auto.
+  rewrite (is_val_inv _ _ _ Heqo). red. split; auto. eapply red_Ecall; eauto. 
+  eapply sem_cast_arguments_sound; eauto. 
+  (* depth *)
+  eapply incontext2_list_ok; eauto.
+  eapply incontext2_list_ok; eauto. 
+(* loc *)
+  congruence.
+(* paren *)
+  destruct (is_val a) as [[v ty'] | ]_eqn.
+  (* top *)
+  mysimpl. apply topred_ok; auto.
+  rewrite (is_val_inv _ _ _ Heqo). apply red_paren; auto. 
+  (* depth *)
+  eapply incontext_ok; eauto.
+
+  induction al; simpl; intros.
+(* nil *)
+  congruence.
+(* cons *)
+  eapply incontext2_list_ok'; eauto.
+Qed.
+
+
+Lemma step_exprlist_val_list:
+  forall m al, is_val_list al <> None -> step_exprlist al m = Some nil.
+Proof.
+  induction al; simpl; intros. 
+  auto.
+  destruct (is_val r1) as [[v1 ty1]|]_eqn; try congruence.
+  destruct (is_val_list al) as []_eqn; try congruence.
+  rewrite (is_val_inv _ _ _ Heqo).
+  rewrite IHal. auto. congruence.
+Qed.
+
+(** Completeness, part 1: if [step_expr] returns [Some ll],
+  then [ll] contains all possible reducts. *)
+
+Lemma lred_topred:
+  forall l1 m1 l2 m2,
+  lred ge e l1 m1 l2 m2 ->
+  step_expr LV l1 m1 = topred (Lred l2 m2).
+Proof.
+  induction 1; simpl.
+(* var local *)
+  rewrite H. rewrite dec_eq_true; auto.
+(* var global *)
+  rewrite H; rewrite H0; rewrite H1. rewrite dec_eq_true; auto.
+(* deref *) 
+  auto.
+(* field struct *)
+  rewrite H; auto.
+(* field union *)
+  auto.
+Qed.
+
+Lemma rred_topred:
+  forall r1 m1 r2 m2,
+  rred r1 m1 r2 m2 ->
+  step_expr RV r1 m1 = topred (Rred r2 m2).
+Proof.
+  induction 1; simpl.
+(* valof *)
+  rewrite dec_eq_true; auto. rewrite H; auto.
+(* addrof *)
+  auto.
+(* unop *)
+  rewrite H; auto.
+(* binop *)
+  rewrite H; auto.
+(* cast *)
+  rewrite H; auto.
+(* condition *)
+  rewrite H; auto.
+(* sizeof *)
+  auto.
+(* assign *)
+  rewrite dec_eq_true; auto. rewrite H; rewrite H0; auto.
+(* assignop *)
+  rewrite dec_eq_true; auto. rewrite H; rewrite H0; rewrite H1; rewrite H2; auto.
+(* postincr *)
+  rewrite dec_eq_true; auto. rewrite H; rewrite H0; rewrite H1; rewrite H2; auto.
+(* comma *)
+  rewrite H; rewrite dec_eq_true; auto.
+(* paren *)
+  rewrite H; auto.
+Qed.
+
+Lemma sem_cast_arguments_complete:
+  forall al tyl vl,
+  cast_arguments al tyl vl ->
+  exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl = Some vl.
+Proof.
+  induction 1.
+  exists (@nil (val * type)); auto.
+  destruct IHcast_arguments as [vtl [A B]]. 
+  exists ((v, ty) :: vtl); simpl. rewrite A; rewrite B; rewrite H. auto.
+Qed.
+
+Lemma callred_topred:
+  forall a fd args ty m,
+  callred ge a fd args ty ->
+  step_expr RV a m = topred (Callred fd args ty m).
+Proof.
+  induction 1; simpl.
+  rewrite H2. exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]].
+  rewrite A; rewrite H; rewrite B; rewrite H1; rewrite dec_eq_true. auto.
+Qed.
+
+Definition reducts_incl {A B: Type} (C: A -> B) (res1: reducts A) (res2: reducts B) : Prop :=
+  match res1, res2 with
+  | Some ll1, Some ll2 =>
+      forall C1 rd, In (C1, rd) ll1 -> In ((fun x => C(C1 x)), rd) ll2
+  | None, Some ll2 => False
+  | _, None => True
+  end.
+
+Lemma reducts_incl_trans:
+  forall (A1 A2: Type) (C: A1 -> A2) res1 res2, reducts_incl C res1 res2 ->
+  forall (A3: Type) (C': A2 -> A3) res3,
+  reducts_incl C' res2 res3 ->
+  reducts_incl (fun x => C'(C x)) res1 res3.
+Proof.
+  unfold reducts_incl; intros. destruct res1; destruct res2; destruct res3; auto. contradiction.
+Qed.
+
+Lemma reducts_incl_nil:
+  forall (A B: Type) (C: A -> B) res,
+  reducts_incl C (Some nil) res.
+Proof.
+  intros; red. destruct res; auto. intros; contradiction.
+Qed.
+
+Lemma reducts_incl_val:
+  forall (A: Type) a m v ty (C: expr -> A) res,
+  is_val a = Some(v, ty) -> reducts_incl C (step_expr RV a m) res.
+Proof.
+  intros. rewrite (is_val_inv _ _ _ H). apply reducts_incl_nil.
+Qed.
+
+Lemma reducts_incl_loc:
+  forall (A: Type) a m b ofs ty (C: expr -> A) res,
+  is_loc a = Some(b, ofs, ty) -> reducts_incl C (step_expr LV a m) res.
+Proof.
+  intros. rewrite (is_loc_inv _ _ _ _ H). apply reducts_incl_nil.
+Qed.
+
+Lemma reducts_incl_listval:
+  forall (A: Type) a m vtl (C: exprlist -> A) res,
+  is_val_list a = Some vtl -> reducts_incl C (step_exprlist a m) res.
+Proof.
+  intros. rewrite step_exprlist_val_list. apply reducts_incl_nil. congruence.
+Qed.
+
+Lemma reducts_incl_incontext:
+  forall (A B: Type) (C: A -> B) res,
+  reducts_incl C res (incontext C res).
+Proof.
+  intros; unfold reducts_incl. destruct res; simpl; auto.
+  intros. set (f := fun z : (expr -> A) * reduction => (fun x : expr => C (fst z x), snd z)).
+  change (In (f (C1, rd)) (map f l)). apply in_map. auto.
+Qed.
+
+Lemma reducts_incl_incontext2_left:
+  forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2,
+  reducts_incl C1 res1 (incontext2 C1 res1 C2 res2).
+Proof.
+  intros. destruct res1; simpl; auto. destruct res2; auto. 
+  intros. rewrite in_app_iff. left.
+  set (f := fun z : (expr -> A1) * reduction => (fun x : expr => C1 (fst z x), snd z)).
+  change (In (f (C0, rd)) (map f l)). apply in_map; auto.
+Qed.
+
+Lemma reducts_incl_incontext2_right:
+  forall (A1 A2 B: Type) (C1: A1 -> B) res1 (C2: A2 -> B) res2,
+  reducts_incl C2 res2 (incontext2 C1 res1 C2 res2).
+Proof.
+  intros. destruct res1; destruct res2; simpl; auto.
+  intros. rewrite in_app_iff. right.
+  set (f := fun z : (expr -> A2) * reduction => (fun x : expr => C2 (fst z x), snd z)).
+  change (In (f (C0, rd)) (map f l0)). apply in_map; auto.
+Qed.
+
+Hint Resolve reducts_incl_val reducts_incl_loc reducts_incl_listval
+             reducts_incl_incontext reducts_incl_incontext2_left reducts_incl_incontext2_right.
+
+Lemma step_expr_context:
+  forall from to C, context from to C ->
+  forall a m, reducts_incl C (step_expr from a m) (step_expr to (C a) m)
+with step_exprlist_context:
+  forall from C, contextlist from C ->
+  forall a m, reducts_incl C (step_expr from a m) (step_exprlist (C a) m).
+Proof.
+  induction 1; simpl; intros.
+(* top *)
+  red. destruct (step_expr k a m); auto. intros. 
+  replace (fun x => C1 x) with C1; auto. apply extensionality; auto.
+(* deref *)
+  eapply reducts_incl_trans with (C' := fun x => Ederef x ty); eauto.
+  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+(* field *)
+  eapply reducts_incl_trans with (C' := fun x => Efield x f ty); eauto.
+  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+(* valof *)
+  eapply reducts_incl_trans with (C' := fun x => Evalof x ty); eauto.
+  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+(* addrof *)
+  eapply reducts_incl_trans with (C' := fun x => Eaddrof x ty); eauto.
+  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+(* unop *)
+  eapply reducts_incl_trans with (C' := fun x => Eunop op x ty); eauto.
+  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+(* binop left *)
+  eapply reducts_incl_trans with (C' := fun x => Ebinop op x e2 ty); eauto.
+  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+(* binop right *)
+  eapply reducts_incl_trans with (C' := fun x => Ebinop op e1 x ty); eauto.
+  destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto.
+(* cast *)
+  eapply reducts_incl_trans with (C' := fun x => Ecast x ty); eauto.
+  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+(* condition *)
+  eapply reducts_incl_trans with (C' := fun x => Econdition x r2 r3 ty); eauto.
+  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+(* assign left *)
+  eapply reducts_incl_trans with (C' := fun x => Eassign x e2 ty); eauto.
+  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+(* assign right *)
+  eapply reducts_incl_trans with (C' := fun x => Eassign e1 x ty); eauto.
+  destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto.
+(* assignop left *)
+  eapply reducts_incl_trans with (C' := fun x => Eassignop op x e2 tyres ty); eauto.
+  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+(* assignop right *)
+  eapply reducts_incl_trans with (C' := fun x => Eassignop op e1 x tyres ty); eauto.
+  destruct (is_loc e1) as [[[b ofs] ty1]|]_eqn; eauto.
+  destruct (is_val (C a)) as [[v2 ty2]|]_eqn; eauto.
+(* postincr *)
+  eapply reducts_incl_trans with (C' := fun x => Epostincr id x ty); eauto.
+  destruct (is_loc (C a)) as [[[b ofs] ty']|]_eqn; eauto.
+(* call left *)
+  eapply reducts_incl_trans with (C' := fun x => Ecall x el ty); eauto.
+  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+(* call right *)
+  eapply reducts_incl_trans with (C' := fun x => Ecall e1 x ty). apply step_exprlist_context. auto. 
+  destruct (is_val e1) as [[v1 ty1]|]_eqn; eauto.
+  destruct (is_val_list (C a)) as [vl|]_eqn; eauto.
+(* comma *)
+  eapply reducts_incl_trans with (C' := fun x => Ecomma x e2 ty); eauto.
+  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+(* paren *)
+  eapply reducts_incl_trans with (C' := fun x => Eparen x ty); eauto.
+  destruct (is_val (C a)) as [[v ty']|]_eqn; eauto.
+
+  induction 1; simpl; intros.
+(* cons left *)
+  eapply reducts_incl_trans with (C' := fun x => Econs x el).
+  apply step_expr_context; eauto. eauto.
+(* binop right *)
+  eapply reducts_incl_trans with (C' := fun x => Econs e1 x).
+  apply step_exprlist_context; eauto. eauto.
+Qed.
+
+(** Completeness, part 2: given a safe expression, [step_expr] does not return [None]. *)
+
+Lemma topred_none:
+  forall rd, topred rd <> None.
+Proof.
+  intros; unfold topred; congruence.
+Qed.
+
+Lemma incontext_none:
+  forall (A B: Type) (C: A -> B) rds,
+  rds <> None -> incontext C rds <> None.
+Proof.
+  unfold incontext; intros. destruct rds; congruence.
+Qed.
+
+Lemma incontext2_none:
+  forall (A1 A2 B: Type) (C1: A1 -> B) rds1 (C2: A2 -> B) rds2,
+  rds1 <> None -> rds2 <> None -> incontext2 C1 rds1 C2 rds2 <> None.
+Proof.
+  unfold incontext2; intros. destruct rds1; destruct rds2; congruence.
+Qed.
+
+Lemma safe_expr_kind:
+  forall k C a m,
+  context k RV C ->
+  not_stuck ge e (C a) m ->
+  k = Cstrategy.expr_kind a.
+Proof.
+  intros.
+  symmetry. eapply Cstrategy.not_imm_stuck_kind; eauto.
+Qed.
+
+Lemma safe_inversion:
+  forall k C a m,
+  context k RV C ->
+  not_stuck ge e (C a) m ->
+  match a with
+  | Eloc _ _ _ => True
+  | Eval _ _ => True
+  | _ => Cstrategy.invert_expr_prop ge e a m
+  end.
+Proof.
+  intros. eapply Cstrategy.not_imm_stuck_inv; eauto.
+Qed. 
+
+Lemma is_val_list_all_values:
+  forall al vtl, is_val_list al = Some vtl -> Cstrategy.exprlist_all_values al.
+Proof.
+  induction al; simpl; intros. auto. 
+  destruct (is_val r1) as [[v ty]|]_eqn; try discriminate.
+  destruct (is_val_list al) as [vtl'|]_eqn; try discriminate.
+  rewrite (is_val_inv _ _ _ Heqo). eauto.
+Qed.
+
+Theorem step_expr_defined:
+  forall a k m C,
+  context k RV C ->
+  not_stuck ge e (C a) m ->
+  step_expr k a m <> None
+with step_exprlist_defined:
+  forall al m C,
+  Cstrategy.contextlist' C ->
+  not_stuck ge e (C al) m ->
+  step_exprlist al m <> None.
+Proof.
+  induction a; intros k m C CTX NS; 
+  rewrite (safe_expr_kind _ _ _ _ CTX NS);
+  rewrite (safe_expr_kind _ _ _ _ CTX NS) in CTX;
+  simpl in *;
+  generalize (safe_inversion _ _ _ _ CTX NS); intro INV.
+(* val *)
+  congruence.
+(* var *)
+  red in INV. destruct INV as [b [P | [P [Q R]]]].
+  rewrite P; rewrite dec_eq_true. apply topred_none.
+  rewrite P; rewrite Q; rewrite R; rewrite dec_eq_true. apply topred_none.
+(* field *)
+  destruct (is_loc a) as [[[b ofs] ty']|]_eqn. 
+  rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. 
+  destruct ty'; try contradiction. destruct INV as [delta EQ]. rewrite EQ. apply topred_none.
+  apply topred_none.
+  apply incontext_none. apply IHa with (C := fun x => C(Efield x f ty)); eauto.
+(* valof *)
+  destruct (is_loc a) as [[[b ofs] ty']|]_eqn. 
+  rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. destruct INV as [EQ [v LD]]. subst.
+  rewrite dec_eq_true; rewrite LD; apply topred_none.
+  apply incontext_none. apply IHa with (C := fun x => C(Evalof x ty)); eauto.
+(* deref *)
+  destruct (is_val a) as [[v ty']|]_eqn. 
+  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [b [ofs EQ]]. subst. 
+  apply topred_none.
+  apply incontext_none. apply IHa with (C := fun x => C(Ederef x ty)); eauto.
+(* addrof *) 
+  destruct (is_loc a) as [[[b ofs] ty']|]_eqn. 
+  apply topred_none.
+  apply incontext_none. apply IHa with (C := fun x => C(Eaddrof x ty)); eauto.
+(* unop *)
+  destruct (is_val a) as [[v1 ty1]|]_eqn. 
+  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ].
+  rewrite EQ; apply topred_none.
+  apply incontext_none. apply IHa with (C := fun x => C(Eunop op x ty)); eauto.
+(* binop *)
+  destruct (is_val a1) as [[v1 ty1]|]_eqn. 
+  destruct (is_val a2) as [[v2 ty2]|]_eqn. 
+  rewrite (is_val_inv _ _ _ Heqo) in INV.
+  rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. destruct INV as [v EQ].
+  rewrite EQ; apply topred_none.
+  apply incontext2_none. apply IHa1 with (C := fun x => C(Ebinop op x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Ebinop op a1 x ty)); eauto.
+  apply incontext2_none. apply IHa1 with (C := fun x => C(Ebinop op x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Ebinop op a1 x ty)); eauto.
+(* cast *)
+  destruct (is_val a) as [[v1 ty1]|]_eqn. 
+  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ].
+  rewrite EQ; apply topred_none.
+  apply incontext_none. apply IHa with (C := fun x => C(Ecast x ty)); eauto.
+(* condition *)
+  destruct (is_val a1) as [[v1 ty1]|]_eqn. 
+  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ].
+  rewrite EQ; apply topred_none.
+  apply incontext_none. apply IHa1 with (C := fun x => C(Econdition x a2 a3 ty)); eauto.
+(* sizeof *)
+  apply topred_none.
+(* assign *)
+  destruct (is_loc a1) as [[[b ofs] ty1]|]_eqn. 
+  destruct (is_val a2) as [[v2 ty2]|]_eqn. 
+  rewrite (is_loc_inv _ _ _ _ Heqo) in INV.
+  rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. 
+  destruct INV as [v [m' [P [Q R]]]]. 
+  subst. rewrite dec_eq_true; rewrite Q; rewrite R; apply topred_none.
+  apply incontext2_none. apply IHa1 with (C := fun x => C(Eassign x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Eassign a1 x ty)); eauto.
+  apply incontext2_none. apply IHa1 with (C := fun x => C(Eassign x a2 ty)); eauto. apply IHa2 with (C := fun x => C(Eassign a1 x ty)); eauto.
+(* assignop *)
+  destruct (is_loc a1) as [[[b ofs] ty1]|]_eqn. 
+  destruct (is_val a2) as [[v2 ty2]|]_eqn. 
+  rewrite (is_loc_inv _ _ _ _ Heqo) in INV.
+  rewrite (is_val_inv _ _ _ Heqo0) in INV. red in INV. 
+  destruct INV as [v1 [v [v' [m' [P [Q [R [S T]]]]]]]]. 
+  subst. rewrite dec_eq_true; rewrite Q; rewrite R; rewrite S; rewrite T; apply topred_none.
+  apply incontext2_none. apply IHa1 with (C := fun x => C(Eassignop op x a2 tyres ty)); eauto. apply IHa2 with (C := fun x => C(Eassignop op a1 x tyres ty)); eauto.
+  apply incontext2_none. apply IHa1 with (C := fun x => C(Eassignop op x a2 tyres ty)); eauto. apply IHa2 with (C := fun x => C(Eassignop op a1 x tyres ty)); eauto.
+(* postincr *)
+  destruct (is_loc a) as [[[b ofs] ty1]|]_eqn. 
+  rewrite (is_loc_inv _ _ _ _ Heqo) in INV. red in INV. 
+  destruct INV as [v1 [v2 [v3 [m' [P [Q [R [S T]]]]]]]]. 
+  subst. rewrite dec_eq_true; rewrite Q; rewrite R; rewrite S; rewrite T; apply topred_none.
+  apply incontext_none. apply IHa with (C := fun x => C(Epostincr id x ty)); eauto.
+(* comma *)
+  destruct (is_val a1) as [[v1 ty1]|]_eqn. 
+  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. rewrite INV.
+  rewrite dec_eq_true; apply topred_none.
+  apply incontext_none. apply IHa1 with (C := fun x => C(Ecomma x a2 ty)); eauto.
+(* call *)
+  destruct (is_val a) as [[vf tyf]|]_eqn. 
+  destruct (is_val_list rargs) as [vtl|]_eqn. 
+  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. 
+  destruct INV as [tyargs [tyres [fd [vl [P [Q [R S]]]]]]].
+  eapply is_val_list_all_values; eauto.
+  rewrite P; rewrite Q. 
+  exploit sem_cast_arguments_complete; eauto. intros [vtl' [U V]]. 
+  assert (vtl' = vtl) by congruence. subst. rewrite V. rewrite S. rewrite dec_eq_true. 
+  apply topred_none.
+  apply incontext2_none. apply IHa with (C := fun x => C(Ecall x rargs ty)); eauto.
+  apply step_exprlist_defined with (C := fun x => C(Ecall a x ty)); auto.
+  apply Cstrategy.contextlist'_intro with (rl0 := Enil). auto.
+  apply incontext2_none. apply IHa with (C := fun x => C(Ecall x rargs ty)); eauto.
+  apply step_exprlist_defined with (C := fun x => C(Ecall a x ty)); auto.
+  apply Cstrategy.contextlist'_intro with (rl0 := Enil). auto.
+(* loc *)
+  congruence.
+(* paren *)
+  destruct (is_val a) as [[v1 ty1]|]_eqn. 
+  rewrite (is_val_inv _ _ _ Heqo) in INV. red in INV. destruct INV as [v EQ].
+  rewrite EQ; apply topred_none.
+  apply incontext_none. apply IHa with (C := fun x => C(Eparen x ty)); eauto.
+
+  induction al; intros; simpl.
+(* nil *)
+  congruence.
+(* cons *)
+  apply incontext2_none.
+  apply step_expr_defined with (C := fun x => C(Econs x al)); eauto. 
+  apply Cstrategy.contextlist'_head; auto.
+  apply IHal with (C := fun x => C(Econs r1 x)); auto.
+  apply Cstrategy.contextlist'_tail; auto.
+Qed.
+
+(** Connections between [not_stuck] and [step_expr]. *)
+
+Lemma step_expr_not_imm_stuck:
+  forall k a m,
+  step_expr k a m <> None ->
+  not_imm_stuck ge e k a m.
+Proof.
+  intros. generalize (step_expr_sound a k m). unfold reducts_ok. 
+  destruct (step_expr k a m) as [ll|]. destruct ll.
+(* value or location *)
+  destruct k; destruct a; simpl; intros; try congruence. 
+  apply not_stuck_loc.
+  apply Csem.not_stuck_val.
+(* reducible *)
+  intros R. destruct p as [C1 rd1]. destruct (R C1 rd1) as [P [a' [U V]]]; auto with coqlib.
+  subst a. red in V. destruct rd1. 
+  eapply not_stuck_lred; eauto. 
+  eapply not_stuck_rred; eauto.
+  destruct V. subst m'. eapply not_stuck_callred; eauto.
+(* stuck *)
+  congruence.
+Qed.
+
+Lemma step_expr_not_stuck:
+  forall a m,
+  step_expr RV a m <> None ->
+  not_stuck ge e a m.
+Proof.
+  intros; red; intros. subst a. 
+  apply step_expr_not_imm_stuck.
+  generalize (step_expr_context _ _ C H0 e' m). unfold reducts_incl. 
+  destruct (step_expr k e' m). congruence.
+  destruct (step_expr RV (C e') m). tauto. congruence.
+Qed.
+
+Lemma not_stuck_step_expr:
+  forall a m,
+  not_stuck ge e a m ->
+  step_expr RV a m <> None.
+Proof.
+  intros. apply step_expr_defined with (C := fun x => x); auto. 
+Qed.
+
+End EXPRS.
+
+(** * External functions and events. *)
+
+Section EVENTS.
+
+Variable F V: Type.
+Variable genv: Genv.t F V.
+
+Definition eventval_of_val (v: val) (t: typ) : option eventval :=
+  match v, t with
+  | Vint i, AST.Tint => Some (EVint i)
+  | Vfloat f, AST.Tfloat => Some (EVfloat f)
+  | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol genv b; Some (EVptr_global id ofs)
+  | _, _ => None
+  end.
+
+Fixpoint list_eventval_of_val (vl: list val) (tl: list typ) : option (list eventval) :=
+  match vl, tl with
+  | nil, nil => Some nil
+  | v1::vl, t1::tl =>
+      do ev1 <- eventval_of_val v1 t1;
+      do evl <- list_eventval_of_val vl tl;
+      Some (ev1 :: evl)
+  | _, _ => None
+  end.
+
+Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
+  match ev, t with
+  | EVint i, AST.Tint => Some (Vint i)
+  | EVfloat f, AST.Tfloat => Some (Vfloat f)
+  | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol genv id; Some (Vptr b ofs)
+  | _, _ => None
+  end.
+
+Lemma eventval_of_val_sound:
+  forall v t ev, eventval_of_val v t = Some ev -> eventval_match genv ev t v.
+Proof.
+  intros. destruct v; destruct t; simpl in H; inv H.
+  constructor.
+  constructor.
+  destruct (Genv.invert_symbol genv b) as [id|]_eqn; inv H1. 
+  constructor. apply Genv.invert_find_symbol; auto.
+Qed.
+
+Lemma eventval_of_val_complete:
+  forall ev t v, eventval_match genv ev t v -> eventval_of_val v t = Some ev.
+Proof.
+  induction 1; simpl; auto.
+  rewrite (Genv.find_invert_symbol _ _ H). auto. 
+Qed.
+
+Lemma list_eventval_of_val_sound:
+  forall vl tl evl, list_eventval_of_val vl tl = Some evl -> eventval_list_match genv evl tl vl.
+Proof with try discriminate.
+  induction vl; destruct tl; simpl; intros; inv H.
+  constructor.
+  destruct (eventval_of_val a t) as [ev1|]_eqn...
+  destruct (list_eventval_of_val vl tl) as [evl'|]_eqn...
+  inv H1. constructor. apply eventval_of_val_sound; auto. eauto.
+Qed.
+
+Lemma list_eventval_of_val_complete:
+  forall evl tl vl, eventval_list_match genv evl tl vl -> list_eventval_of_val vl tl = Some evl.
+Proof.
+  induction 1; simpl. auto. 
+  rewrite (eventval_of_val_complete _ _ _ H). rewrite IHeventval_list_match. auto.
+Qed.
+
+Lemma val_of_eventval_sound:
+  forall ev t v, val_of_eventval ev t = Some v -> eventval_match genv ev t v.
+Proof.
+  intros. destruct ev; destruct t; simpl in H; inv H.
+  constructor.
+  constructor.
+  destruct (Genv.find_symbol genv i) as [b|]_eqn; inv H1.
+  constructor. auto.
+Qed.
+
+Lemma val_of_eventval_complete:
+  forall ev t v, eventval_match genv ev t v -> val_of_eventval ev t = Some v.
+Proof.
+  induction 1; simpl; auto. rewrite H; auto.
+Qed.
+
+(** System calls and library functions *)
+
+Definition do_ef_external (name: ident) (sg: signature)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  do args <- list_eventval_of_val vargs (sig_args sg);
+  match nextworld_io w name args with
+  | None => None
+  | Some(res, w') =>
+      do vres <- val_of_eventval res (proj_sig_res sg);
+      Some(w', Event_syscall name args res :: E0, vres, m)
+  end.
+
+Definition do_ef_volatile_load (chunk: memory_chunk)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | Vptr b ofs :: nil =>
+      if block_is_volatile genv b then
+        do id <- Genv.invert_symbol genv b;
+        match nextworld_vload w chunk id ofs with
+        | None => None
+        | Some(res, w') =>
+            do vres <- val_of_eventval res (type_of_chunk chunk);
+            Some(w', Event_vload chunk id ofs res :: nil, Val.load_result chunk vres, m)
+        end
+      else
+        do v <- Mem.load chunk m b (Int.unsigned ofs);
+        Some(w, E0, v, m)
+  | _ => None
+  end.
+
+Definition do_ef_volatile_store (chunk: memory_chunk)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | Vptr b ofs :: v :: nil =>
+      if block_is_volatile genv b then
+        do id <- Genv.invert_symbol genv b;
+        do ev <- eventval_of_val v (type_of_chunk chunk);
+        do w' <- nextworld_vstore w chunk id ofs ev;
+        Some(w', Event_vstore chunk id ofs ev :: nil, Vundef, m)
+      else
+        do m' <- Mem.store chunk m b (Int.unsigned ofs) v;
+        Some(w, E0, Vundef, m')
+  | _ => None
+  end.
+
+Definition do_ef_malloc
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | Vint n :: nil =>
+      let (m', b) := Mem.alloc m (-4) (Int.unsigned n) in
+      do m'' <- Mem.store Mint32 m' b (-4) (Vint n);
+      Some(w, E0, Vptr b Int.zero, m'')
+  | _ => None
+  end.
+
+Definition do_ef_free
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | Vptr b lo :: nil =>
+      do vsz <- Mem.load Mint32 m b (Int.unsigned lo - 4);
+      match vsz with
+      | Vint sz =>
+          check (zlt 0 (Int.unsigned sz));
+          do m' <- Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz);
+          Some(w, E0, Vundef, m')
+      | _ => None
+      end
+  | _ => None
+  end.
+
+Definition memcpy_args_ok
+  (sz al: Z) (bdst: block) (odst: Z) (bsrc: block) (osrc: Z) : Prop :=
+      (al = 1 \/ al = 2 \/ al = 4)
+   /\ sz > 0
+   /\ (al | sz) /\ (al | osrc) /\ (al | odst)
+   /\ (bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc).
+
+Remark memcpy_check_args:
+  forall sz al bdst odst bsrc osrc,
+  {memcpy_args_ok sz al bdst odst bsrc osrc} + {~memcpy_args_ok sz al bdst odst bsrc osrc}.
+Proof with try (right; intuition omega).
+  intros. 
+  assert (X: {al = 1 \/ al = 2 \/ al = 4} + {~(al = 1 \/ al = 2 \/ al = 4)}).
+    destruct (zeq al 1); auto. destruct (zeq al 2); auto. destruct (zeq al 4); auto...
+  unfold memcpy_args_ok. destruct X...
+  assert (al > 0) by (intuition omega).
+  destruct (zlt 0 sz)...
+  destruct (Zdivide_dec al sz); auto...
+  destruct (Zdivide_dec al osrc); auto...
+  destruct (Zdivide_dec al odst); auto...
+  assert (Y: {bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc}
+           +{~(bsrc <> bdst \/ osrc = odst \/ osrc + sz <= odst \/ odst + sz <= osrc)}).
+    destruct (eq_block bsrc bdst); auto.
+    destruct (zeq osrc odst); auto.
+    destruct (zle (osrc + sz) odst); auto.
+    destruct (zle (odst + sz) osrc); auto.
+    right; intuition omega.
+  destruct Y... left; intuition omega.
+Qed.
+
+Definition do_ef_memcpy (sz al: Z)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | Vptr bdst odst :: Vptr bsrc osrc :: nil =>
+      if memcpy_check_args sz al bdst (Int.unsigned odst) bsrc (Int.unsigned osrc) then
+        do bytes <- Mem.loadbytes m bsrc (Int.unsigned osrc) sz;
+        do m' <- Mem.storebytes m bdst (Int.unsigned odst) bytes;
+        Some(w, E0, Vundef, m')
+      else None
+  | _ => None
+  end.
+
+Definition do_ef_annot (text: ident) (targs: list typ)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  do args <- list_eventval_of_val vargs targs;
+  Some(w, Event_annot text args :: E0, Vundef, m).
+
+Definition do_ef_annot_val (text: ident) (targ: typ)
+       (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
+  match vargs with
+  | varg :: nil =>
+      do arg <- eventval_of_val varg targ;
+      Some(w, Event_annot text (arg :: nil) :: E0, varg, m)
+  | _ => None
+  end.
+
+Definition do_external (ef: external_function):
+       world -> list val -> mem -> option (world * trace * val * mem) :=
+  match ef with
+  | EF_external name sg => do_ef_external name sg
+  | EF_builtin name sg => do_ef_external name sg
+  | EF_vload chunk => do_ef_volatile_load chunk
+  | EF_vstore chunk => do_ef_volatile_store chunk
+  | EF_malloc => do_ef_malloc
+  | EF_free => do_ef_free
+  | EF_memcpy sz al => do_ef_memcpy sz al
+  | EF_annot text targs => do_ef_annot text targs
+  | EF_annot_val text targ => do_ef_annot_val text targ
+  end.
+
+Ltac mydestr :=
+  match goal with
+  | [ |- None = Some _ -> _ ] => intro X; discriminate
+  | [ |- Some _ = Some _ -> _ ] => intro X; inv X
+  | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr
+  | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x as []_eqn; mydestr
+  | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr
+  | _ => idtac
+  end.
+
+Lemma do_ef_external_sound:
+  forall ef w vargs m w' t vres m',
+  do_external ef w vargs m = Some(w', t, vres, m') ->
+  external_call ef genv vargs m t vres m' /\ possible_trace w t w'.
+Proof with try congruence.
+  intros until m'.
+  assert (IO: forall name sg,
+             do_ef_external name sg w vargs m = Some(w', t, vres, m') ->
+             extcall_io_sem name sg genv vargs m t vres m' /\ possible_trace w t w').
+    intros until sg. unfold do_ef_external. mydestr. destruct p as [res w'']; mydestr.
+    split. econstructor. apply list_eventval_of_val_sound; auto. 
+    apply val_of_eventval_sound; auto. 
+    econstructor. constructor; eauto. constructor.
+
+  destruct ef; simpl.
+(* EF_external *)
+  auto. 
+(* EF_builtin *)
+  auto.
+(* EF_vload *)
+  unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... 
+  mydestr. destruct p as [res w'']; mydestr.
+  split. constructor. apply Genv.invert_find_symbol; auto. auto. 
+  apply val_of_eventval_sound; auto. 
+  econstructor. constructor; eauto. constructor.
+  split. constructor; auto. constructor.
+(* EF_vstore *)
+  unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... 
+  mydestr.
+  split. constructor. apply Genv.invert_find_symbol; auto. auto. 
+  apply eventval_of_val_sound; auto. 
+  econstructor. constructor; eauto. constructor.
+  split. constructor; auto. constructor.
+(* EF_malloc *)
+  unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs...
+  destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b]_eqn. mydestr.
+  split. econstructor; eauto. constructor.
+(* EF_free *)
+  unfold do_ef_free. destruct vargs... destruct v... destruct vargs... 
+  mydestr. destruct v... mydestr. 
+  split. econstructor; eauto. omega. constructor.
+(* EF_memcpy *)
+  unfold do_ef_memcpy. destruct vargs... destruct v... destruct vargs... 
+  destruct v... destruct vargs... mydestr. red in m0. 
+  split. econstructor; eauto; tauto. constructor.
+(* EF_annot *)
+  unfold do_ef_annot. mydestr. 
+  split. constructor. apply list_eventval_of_val_sound; auto.
+  econstructor. constructor; eauto. constructor.
+(* EF_annot_val *)
+  unfold do_ef_annot_val. destruct vargs... destruct vargs... mydestr. 
+  split. constructor. apply eventval_of_val_sound; auto.
+  econstructor. constructor; eauto. constructor.
+Qed.
+
+Lemma do_ef_external_complete:
+  forall ef w vargs m w' t vres m',
+  external_call ef genv vargs m t vres m' -> possible_trace w t w' ->
+  do_external ef w vargs m = Some(w', t, vres, m').
+Proof.
+  intros.
+  assert (IO: forall name sg,
+             extcall_io_sem name sg genv vargs m t vres m' ->
+             do_ef_external name sg w vargs m = Some (w', t, vres, m')).
+    intros. inv H1. inv H0. inv H8. inv H6. 
+    unfold do_ef_external. rewrite (list_eventval_of_val_complete _ _ _ H2). rewrite H8. 
+    rewrite (val_of_eventval_complete _ _ _ H3). auto.
+ 
+  destruct ef; simpl in *.
+(* EF_external *)
+  auto.
+(* EF_builtin *)
+  auto.
+(* EF_vload *)
+  inv H; unfold do_ef_volatile_load.
+  inv H0. inv H8. inv H6. 
+  rewrite H2. rewrite (Genv.find_invert_symbol _ _ H1). rewrite H9. 
+  rewrite (val_of_eventval_complete _ _ _ H3). auto.
+  inv H0. rewrite H1. rewrite H2. auto.
+(* EF_vstore *)
+  inv H; unfold do_ef_volatile_store.
+  inv H0. inv H8. inv H6. 
+  rewrite H2. rewrite (Genv.find_invert_symbol _ _ H1).
+  rewrite (eventval_of_val_complete _ _ _ H3). rewrite H9. auto.
+  inv H0. rewrite H1. rewrite H2. auto.
+(* EF_malloc *)
+  inv H; unfold do_ef_malloc. 
+  inv H0. rewrite H1. rewrite H2. auto.
+(* EF_free *)
+  inv H; unfold do_ef_free.
+  inv H0. rewrite H1. rewrite zlt_true. rewrite H3. auto. omega.
+(* EF_memcpy *)
+  inv H; unfold do_ef_memcpy.
+  inv H0. rewrite pred_dec_true. rewrite H7; rewrite H8; auto.
+  red. tauto. 
+(* EF_annot *)
+  inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. 
+  rewrite (list_eventval_of_val_complete _ _ _ H1). auto.
+(* EF_annot_val *)
+  inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. 
+  rewrite (eventval_of_val_complete _ _ _ H1). auto.
+Qed.
+
+End EVENTS.
+
+(** * Transitions over states. *)
+
+Fixpoint do_alloc_variables (e: env) (m: mem) (l: list (ident * type)) {struct l} : env * mem :=
+  match l with
+  | nil => (e,m)
+  | (id, ty) :: l' =>
+      let (m1,b1) := Mem.alloc m 0 (sizeof ty) in 
+      do_alloc_variables (PTree.set id (b1, ty) e) m1 l'
+end.
+
+Lemma do_alloc_variables_sound:
+  forall l e m, alloc_variables e m l (fst (do_alloc_variables e m l)) (snd (do_alloc_variables e m l)).
+Proof.
+  induction l; intros; simpl. 
+  constructor.
+  destruct a as [id ty]. destruct (Mem.alloc m 0 (sizeof ty)) as [m1 b1]_eqn; simpl.
+  econstructor; eauto.
+Qed.
+
+Lemma do_alloc_variables_complete:
+  forall e1 m1 l e2 m2, alloc_variables e1 m1 l e2 m2 ->
+  do_alloc_variables e1 m1 l = (e2, m2).
+Proof.
+  induction 1; simpl. 
+  auto.
+  rewrite H; rewrite IHalloc_variables; auto. 
+Qed.
+
+Function sem_bind_parameters (e: env) (m: mem) (l: list (ident * type)) (lv: list val) 
+                          {struct l} : option mem :=
+  match l, lv  with
+  | nil, nil => Some m
+  | (id, ty) :: params, v1::lv =>
+      match PTree.get id e with
+         | Some (b, ty') =>
+             check (type_eq ty ty');
+             do m1 <- store_value_of_type ty m b Int.zero v1;
+             sem_bind_parameters e m1 params lv
+        | None => None
+      end
+   | _, _ => None
+end.
+
+Lemma sem_bind_parameters_sound : forall e m l lv m',
+  sem_bind_parameters e m l lv = Some m' -> 
+  bind_parameters e m l lv m'.
+Proof.
+   intros; functional induction (sem_bind_parameters e m l lv); try discriminate.
+   inversion H; constructor; auto.  
+   econstructor; eauto.
+Qed.
+
+Lemma sem_bind_parameters_complete : forall e m l lv m',
+  bind_parameters e m l lv m' ->
+  sem_bind_parameters e m l lv = Some m'.
+Proof.
+   induction 1; simpl; auto.
+   rewrite H. rewrite dec_eq_true. 
+   destruct (store_value_of_type ty m b Int.zero v1); try discriminate.
+   inv H0; auto.
+Qed.
+
+Definition expr_final_state (f: function) (k: cont) (e: env) (C_rd: (expr -> expr) * reduction) :=
+  match snd C_rd with
+  | Lred a m => (E0, ExprState f (fst C_rd a) k e m)
+  | Rred a m => (E0, ExprState f (fst C_rd a) k e m)
+  | Callred fd vargs ty m => (E0, Callstate fd vargs (Kcall f e (fst C_rd) ty k) m)
+  end.
+
+Local Open Scope list_monad_scope.
+
+Definition ret (S: state) : list (trace * state) := (E0, S) :: nil.
+
+Definition do_step (w: world) (s: state) : list (trace * state) :=
+  match s with
+
+  | ExprState f a k e m =>
+      match is_val a with
+      | Some(v, ty) =>
+        match k with
+        | Kdo k => ret (State f Sskip k e m )
+        | Kifthenelse s1 s2 k =>
+            do b <- bool_val v ty; ret (State f (if b then s1 else s2) k e m)
+        | Kwhile1 x s k =>
+            do b <- bool_val v ty; 
+            if b then ret (State f s (Kwhile2 x s k) e m) else ret (State f Sskip k e m)
+        | Kdowhile2 x s k =>
+            do b <- bool_val v ty;
+            if b then ret (State f (Sdowhile x s) k e m) else ret (State f Sskip k e m)
+        | Kfor2 a2 a3 s k =>
+            do b <- bool_val v ty;
+            if b then ret (State f s (Kfor3 a2 a3 s k) e m) else ret (State f Sskip k e m)
+        | Kreturn k =>
+            do v' <- sem_cast v ty f.(fn_return);
+            do m' <- Mem.free_list m (blocks_of_env e);
+            ret (Returnstate v' (call_cont k) m')
+        | Kswitch1 sl k =>
+            match v with
+            | Vint n => ret (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m)
+            | _ => nil
+            end
+        | _ => nil
+        end
+
+      | None =>
+          match step_expr e RV a m with
+          | None => nil
+          | Some ll => map (expr_final_state f k e) ll
+          end
+      end
+
+  | State f (Sdo x) k e m => ret(ExprState f x (Kdo k) e m)
+
+  | State f (Ssequence s1 s2) k e m => ret(State f s1 (Kseq s2 k) e m)
+  | State f Sskip (Kseq s k) e m => ret (State f s k e m)
+  | State f Scontinue (Kseq s k) e m => ret (State f Scontinue k e m)
+  | State f Sbreak (Kseq s k) e m => ret (State f Sbreak k e m)
+
+  | State f (Sifthenelse a s1 s2) k e m => ret (ExprState f a (Kifthenelse s1 s2 k) e m)
+
+  | State f (Swhile x s) k e m => ret (ExprState f x (Kwhile1 x s k) e m)
+  | State f (Sskip|Scontinue) (Kwhile2 x s k) e m => ret (State f (Swhile x s) k e m)
+  | State f Sbreak (Kwhile2 x s k) e m => ret (State f Sskip k e m)
+
+  | State f (Sdowhile a s) k e m => ret (State f s (Kdowhile1 a s k) e m)
+  | State f (Sskip|Scontinue) (Kdowhile1 x s k) e m => ret (ExprState f x (Kdowhile2 x s k) e m)
+  | State f Sbreak (Kdowhile1 x s k) e m => ret (State f Sskip k e m)
+
+  | State f (Sfor a1 a2 a3 s) k e m =>
+      if is_skip a1
+      then ret (ExprState f a2 (Kfor2 a2 a3 s k) e m)
+      else ret (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
+  | State f Sskip (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m)
+  | State f Scontinue (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m)
+  | State f Sbreak (Kfor3 a2 a3 s k) e m => ret (State f Sskip k e m)
+  | State f Sskip (Kfor4 a2 a3 s k) e m => ret (State f (Sfor Sskip a2 a3 s) k e m)
+
+  | State f (Sreturn None) k e m =>
+      do m' <- Mem.free_list m (blocks_of_env e);
+      ret (Returnstate Vundef (call_cont k) m')
+  | State f (Sreturn (Some x)) k e m => ret (ExprState f x (Kreturn k) e m)
+  | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => 
+     check (type_eq f.(fn_return) Tvoid);
+     do m' <- Mem.free_list m (blocks_of_env e);
+     ret (Returnstate Vundef k m')
+
+  | State f (Sswitch x sl) k e m => ret (ExprState f x (Kswitch1 sl k) e m)
+  | State f (Sskip|Sbreak) (Kswitch2 k) e m => ret (State f Sskip k e m)
+  | State f Scontinue (Kswitch2 k) e m => ret (State f Scontinue k e m)
+
+  | State f (Slabel lbl s) k e m => ret (State f s k e m)
+  | State f (Sgoto lbl) k e m =>
+      match find_label lbl f.(fn_body) (call_cont k) with
+      | Some(s', k') => ret (State f s' k' e m)
+      | None => nil
+      end
+
+  | Callstate (Internal f) vargs k m =>
+      check (list_norepet_dec ident_eq (var_names (fn_params f) ++ var_names (fn_vars f)));
+      let (e,m1) := do_alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) in
+      do m2 <- sem_bind_parameters e m1 f.(fn_params) vargs;
+      ret (State f f.(fn_body) k e m2)
+  | Callstate (External ef _ _) vargs k m =>
+      match do_external _ _ ge ef w vargs m with
+      | None => nil
+      | Some(w',t,v,m') => (t, Returnstate v k m') :: nil
+      end
+
+  | Returnstate v (Kcall f e C ty k) m => ret (ExprState f (C (Eval v ty)) k e m)
+
+  | _ => nil
+  end.
+
+(*
+Definition at_external (S: state): option (external_function * list val * mem) :=
+  match S with
+  | Callstate (External ef _ _) vargs k m => Some (ef, vargs, m)
+  | _ => None
+  end.
+
+Definition after_external (S: state) (v: val) (m: mem): option state :=
+  match S with
+  | Callstate _ _ k _ => Some (Returnstate v k m)
+  | _ => None
+  end.
+*)
+
+Ltac myinv :=
+  match goal with
+  | [ |- In _ nil -> _ ] => intro X; elim X
+  | [ |- In _ (ret _) -> _ ] => 
+        intro X; elim X; clear X;
+        [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv]
+  | [ |- In _ (_ :: nil) -> _ ] => 
+        intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv]
+  | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x as []_eqn; myinv
+  | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x as []_eqn; myinv
+  | [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv
+  | _ => idtac
+  end.
+
+Hint Extern 3 => exact I.
+
+Lemma do_step_sound:
+  forall w S t S', In (t, S') (do_step w S) -> Csem.step ge S t S'.
+Proof with try (right; econstructor; eauto; fail).
+  intros until S'. destruct S; simpl.
+(* State *)
+  destruct s; myinv...
+  (* skip *)
+  destruct k; myinv...
+  (* break *)
+  destruct k; myinv...
+  (* continue *)
+  destruct k; myinv...
+  (* goto *)
+  destruct p as [s' k']. myinv...
+(* ExprState *)
+  destruct (is_val r) as [[v ty]|]_eqn.
+  (* expression is a value *)
+  rewrite (is_val_inv _ _ _ Heqo).
+  destruct k; myinv...
+  destruct v; myinv...
+  (* expression reduces *)
+  destruct (step_expr e RV r m) as [ll|]_eqn; try contradiction. intros.
+  exploit list_in_map_inv; eauto. intros [[C rd] [A B]].
+  generalize (step_expr_sound e r RV m). unfold reducts_ok. rewrite Heqr0. 
+  destruct ll; try contradiction. intros SOUND. 
+  exploit SOUND; eauto. intros [CTX [a [EQ RD]]]. subst r. 
+  unfold expr_final_state in A. simpl in A. left.
+  destruct rd; inv A; simpl in RD. 
+  apply step_lred. auto. apply step_expr_not_stuck; congruence. auto. 
+  apply step_rred. auto. apply step_expr_not_stuck; congruence. auto.
+  destruct RD; subst m'. apply Csem.step_call. auto.  apply step_expr_not_stuck; congruence. auto.
+(* callstate *)
+  destruct fd; myinv.
+  (* internal *)
+  destruct (do_alloc_variables empty_env m (fn_params f ++ fn_vars f)) as [e m1]_eqn.
+  myinv. right; apply step_internal_function with m1. auto. 
+  change e with (fst (e,m1)). change m1 with (snd (e,m1)) at 2. rewrite <- Heqp. 
+  apply do_alloc_variables_sound. apply sem_bind_parameters_sound; auto.
+  (* external *)
+  destruct p as [[[w' tr] v] m']. myinv. right; constructor. 
+  eapply do_ef_external_sound; eauto.
+(* returnstate *)
+  destruct k; myinv...
+Qed.
+
+Remark estep_not_val:
+  forall f a k e m t S, estep ge (ExprState f a k e m) t S -> is_val a = None.
+Proof.
+  intros. 
+  assert (forall b from to C, context from to C -> (C = fun x => x) \/ is_val (C b) = None).
+    induction 1; simpl; auto. 
+  inv H. 
+  destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto.
+  destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto.
+  destruct (H0 a0 _ _ _ H10). subst. inv H8; auto. auto.
+Qed.
+
+Lemma do_step_complete:
+  forall w S t S' w', possible_trace w t w' -> Csem.step ge S t S' -> In (t, S') (do_step w S).
+Proof with (unfold ret; auto with coqlib).
+  intros until w'; intro PT; intros. 
+  destruct H. 
+  (* Expression step *)
+  inversion H; subst; exploit estep_not_val; eauto; intro NOTVAL.
+(* lred *)
+  unfold do_step; rewrite NOTVAL.
+  destruct (step_expr e RV (C a) m) as [ll|]_eqn.
+  change (E0, ExprState f (C a') k e m') with (expr_final_state f k e (C, Lred a' m')).
+  apply in_map.
+  generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl.
+  rewrite Heqr. destruct (step_expr e LV a m) as [ll'|]_eqn; try tauto.
+  intro. replace C with (fun x => C x). apply H3. 
+  rewrite (lred_topred _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib.
+  apply extensionality; auto.
+  exploit not_stuck_step_expr; eauto.
+(* rred *)
+  unfold do_step; rewrite NOTVAL.
+  destruct (step_expr e RV (C a) m) as [ll|]_eqn.
+  change (E0, ExprState f (C a') k e m') with (expr_final_state f k e (C, Rred a' m')).
+  apply in_map.
+  generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl.
+  rewrite Heqr. destruct (step_expr e RV a m) as [ll'|]_eqn; try tauto.
+  intro. replace C with (fun x => C x). apply H3. 
+  rewrite (rred_topred _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib.
+  apply extensionality; auto.
+  exploit not_stuck_step_expr; eauto.
+(* callred *)
+  unfold do_step; rewrite NOTVAL.
+  destruct (step_expr e RV (C a) m) as [ll|]_eqn.
+  change (E0, Callstate fd vargs (Kcall f e C ty k) m) with (expr_final_state f k e (C, Callred fd vargs ty m)).
+  apply in_map.
+  generalize (step_expr_context e _ _ _ H2 a m). unfold reducts_incl.
+  rewrite Heqr. destruct (step_expr e RV a m) as [ll'|]_eqn; try tauto.
+  intro. replace C with (fun x => C x). apply H3. 
+  rewrite (callred_topred _ _ _ _ _ _ H0) in Heqr0. inv Heqr0. auto with coqlib.
+  apply extensionality; auto.
+  exploit not_stuck_step_expr; eauto.
+
+  (* Statement step *)
+  inv H; simpl...
+  rewrite H0...
+  rewrite H0...
+  rewrite H0...
+  destruct H0; subst s0...
+  destruct H0; subst s0...
+  rewrite H0...
+  rewrite H0...
+  rewrite pred_dec_false...
+  rewrite pred_dec_true...
+  rewrite H0...
+  rewrite H0...
+  destruct H0; subst x...
+  rewrite H0...
+  rewrite H0; rewrite H1...
+  rewrite pred_dec_true; auto. rewrite H2. red in H0. destruct k; try contradiction...
+  destruct H0; subst x...
+  rewrite H0...
+
+  (* Call step *)
+  rewrite pred_dec_true; auto. rewrite (do_alloc_variables_complete _ _ _ _ _ H1).
+  rewrite (sem_bind_parameters_complete _ _ _ _ _ H2)...
+  exploit do_ef_external_complete; eauto. intro EQ; rewrite EQ. auto with coqlib.
+Qed.
+
+End EXEC.
+
+Local Open Scope option_monad_scope.
+
+Definition do_initial_state (p: program): option (genv * state) :=
+  let ge := Genv.globalenv p in
+  do m0 <- Genv.init_mem p;
+  do b <- Genv.find_symbol ge p.(prog_main);
+  do f <- Genv.find_funct_ptr ge b;
+  check (type_eq (type_of_fundef f) (Tfunction Tnil (Tint I32 Signed)));
+  Some (ge, Callstate f nil Kstop m0).
+
+Definition at_final_state (S: state): option int :=
+  match S with
+  | Returnstate (Vint r) Kstop m => Some r
+  | _ => None
+  end.
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 61599cf..6358786 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -129,7 +129,7 @@ let name_type ty = name_cdecl "" ty
 type associativity = LtoR | RtoL | NA
 
 let rec precedence = function
-  | Eloc _ -> assert false
+  | Eloc _ -> (16, NA)
   | Evar _ -> (16, NA)
   | Ederef _ -> (15, RtoL)
   | Efield _ -> (16, LtoR)
@@ -153,7 +153,7 @@ let rec precedence = function
   | Eassign _ -> (2, RtoL)
   | Eassignop _ -> (2, RtoL)
   | Ecomma _ -> (1, LtoR)
-  | Eparen _ -> assert false
+  | Eparen _ -> (14, RtoL)
 
 (* Expressions *)
 
@@ -168,7 +168,7 @@ let rec expr p (prec, e) =
   else fprintf p "@[<hov 2>";
   begin match e with
   | Eloc _ ->
-      assert false
+      fprintf p "<loc>"
   | Evar(id, _) ->
       fprintf p "%s" (extern_atom id)
   | Ederef(a1, _) ->
@@ -181,8 +181,10 @@ let rec expr p (prec, e) =
       fprintf p "%ld" (camlint_of_coqint n)
   | Eval(Vfloat f, _) ->
       fprintf p "%F" f
-  | Eval(_, _) ->
-      assert false
+  | Eval(Vptr _, _) ->
+      fprintf p "<ptr>"
+  | Eval(Vundef, _) ->
+      fprintf p "<undef>"
   | Esizeof(ty, _) ->
       fprintf p "sizeof(%s)" (name_type ty)
   | Eunop(op, a1, _) ->
@@ -207,8 +209,8 @@ let rec expr p (prec, e) =
       fprintf p "%a,@ %a" expr (prec1, a1) expr (prec2, a2)
   | Ecall(a1, al, _) ->
       fprintf p "%a@[<hov 1>(%a)@]" expr (prec', a1) exprlist (true, al)
-  | Eparen _ ->
-      assert false
+  | Eparen(a1, ty) ->
+      fprintf p "(%s) %a" (name_type ty) expr (prec', a1)
   end;
   if prec' < prec then fprintf p ")@]" else fprintf p "@]"
 
@@ -221,6 +223,7 @@ and exprlist p (first, rl) =
       exprlist p (false, rl)
 
 let print_expr p e = expr p (0, e)
+let print_exprlist p el = exprlist p (true, el)
 
 (* Statements *)
 
diff --git a/common/Determinism.v b/common/Determinism.v
index 16e8890..29cc695 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -222,13 +222,13 @@ Qed.
 
 Record sem_deterministic (L: semantics) := mk_deterministic {
   det_step: forall s0 t1 s1 t2 s2,
-    L (genv L) s0 t1 s1 -> L (genv L) s0 t2 s2 -> s1 = s2 /\ t1 = t2;
+    Step L s0 t1 s1 -> Step L s0 t2 s2 -> s1 = s2 /\ t1 = t2;
   det_initial_state: forall s1 s2,
     initial_state L s1 -> initial_state L s2 -> s1 = s2;
   det_final_state: forall s r1 r2,
     final_state L s r1 -> final_state L s r2 -> r1 = r2;
   det_final_nostep: forall s r,
-    final_state L s r -> nostep L (genv L) s
+    final_state L s r -> Nostep L s
 }.
 
 Section DETERM_SEM.
@@ -238,18 +238,18 @@ Hypothesis DET: sem_deterministic L.
 
 Ltac use_step_deterministic :=
   match goal with
-  | [ S1: step L (genv L) _ ?t1 _, S2: step L (genv L) _ ?t2 _ |- _ ] =>
+  | [ S1: Step L _ ?t1 _, S2: Step L _ ?t2 _ |- _ ] =>
     destruct (det_step L DET _ _ _ _ _ S1 S2) as [EQ1 EQ2]; subst
   end.
 
 (** Determinism for finite transition sequences. *)
 
 Lemma star_step_diamond:
-  forall s0 t1 s1, star L (genv L) s0 t1 s1 -> 
-  forall t2 s2, star L (genv L) s0 t2 s2 -> 
+  forall s0 t1 s1, Star L s0 t1 s1 -> 
+  forall t2 s2, Star L s0 t2 s2 -> 
   exists t,
-     (star L (genv L) s1 t s2 /\ t2 = t1 ** t)
-  \/ (star L (genv L) s2 t s1 /\ t1 = t2 ** t).
+     (Star L s1 t s2 /\ t2 = t1 ** t)
+  \/ (Star L s2 t s1 /\ t1 = t2 ** t).
 Proof.
   induction 1; intros. 
   exists t2; auto. 
@@ -262,7 +262,7 @@ Qed.
 
 Ltac use_star_step_diamond :=
   match goal with
-  | [ S1: star (step L) (genv L) _ ?t1 _, S2: star (step L) (genv L) _ ?t2 _ |- _ ] =>
+  | [ S1: Star L _ ?t1 _, S2: Star L _ ?t2 _ |- _ ] =>
     let t := fresh "t" in let P := fresh "P" in let EQ := fresh "EQ" in
     destruct (star_step_diamond _ _ _ S1 _ _ S2)
     as [t [ [P EQ] | [P EQ] ]]; subst
@@ -270,16 +270,16 @@ Ltac use_star_step_diamond :=
 
 Ltac use_nostep :=
   match goal with
-  | [ S: step L (genv L) ?s _ _, NO: nostep (step L) (genv L) ?s |- _ ] => elim (NO _ _ S)
+  | [ S: Step L ?s _ _, NO: Nostep L ?s |- _ ] => elim (NO _ _ S)
   end.
 
 Lemma star_step_triangle:
   forall s0 t1 s1 t2 s2,
-  star L (genv L) s0 t1 s1 -> 
-  star L (genv L) s0 t2 s2 -> 
-  nostep L (genv L) s2 ->
+  Star L s0 t1 s1 -> 
+  Star L s0 t2 s2 -> 
+  Nostep L s2 ->
   exists t,
-  star L (genv L) s1 t s2 /\ t2 = t1 ** t.
+  Star L s1 t s2 /\ t2 = t1 ** t.
 Proof.
   intros. use_star_step_diamond.
   exists t; auto.
@@ -289,8 +289,7 @@ Qed.
 
 Ltac use_star_step_triangle :=
   match goal with
-  | [ S1: star (step L) (genv L) _ ?t1 _, S2: star (step L) (genv L) _ ?t2 ?s2,
-      NO: nostep (step L) (genv L) ?s2 |- _ ] =>
+  | [ S1: Star L _ ?t1 _, S2: Star L _ ?t2 ?s2, NO: Nostep L ?s2 |- _ ] =>
     let t := fresh "t" in let P := fresh "P" in let EQ := fresh "EQ" in
     destruct (star_step_triangle _ _ _ _ _ S1 S2 NO)
     as [t [P EQ]]; subst
@@ -298,8 +297,8 @@ Ltac use_star_step_triangle :=
 
 Lemma steps_deterministic:
   forall s0 t1 s1 t2 s2,
-  star L (genv L) s0 t1 s1 -> star L (genv L) s0 t2 s2 -> 
-  nostep L (genv L) s1 -> nostep L (genv L) s2 ->
+  Star L s0 t1 s1 -> Star L s0 t2 s2 -> 
+  Nostep L s1 -> Nostep L s2 ->
   t1 = t2 /\ s1 = s2.
 Proof.
   intros. use_star_step_triangle. inv P.
@@ -308,8 +307,8 @@ Qed.
 
 Lemma terminates_not_goes_wrong:
   forall s t1 s1 r t2 s2,
-  star L (genv L) s t1 s1 -> final_state L s1 r ->
-  star L (genv L) s t2 s2 -> nostep L (genv L) s2 ->
+  Star L s t1 s1 -> final_state L s1 r ->
+  Star L s t2 s2 -> Nostep L s2 ->
   (forall r, ~final_state L s2 r) -> False.
 Proof.
   intros.
@@ -321,9 +320,9 @@ Qed.
 (** Determinism for infinite transition sequences. *)
 
 Lemma star_final_not_forever_silent:
-  forall s t s', star L (genv L) s t s' ->
-  nostep L (genv L) s' ->
-  forever_silent L (genv L) s -> False.
+  forall s t s', Star L s t s' ->
+  Nostep L s' ->
+  Forever_silent L s -> False.
 Proof.
   induction 1; intros. 
   inv H0. use_nostep. 
@@ -332,8 +331,8 @@ Qed.
 
 Lemma star2_final_not_forever_silent:
   forall s t1 s1 t2 s2,
-  star L (genv L) s t1 s1 -> nostep L (genv L) s1 ->
-  star L (genv L) s t2 s2 -> forever_silent L (genv L) s2 ->
+  Star L s t1 s1 -> Nostep L s1 ->
+  Star L s t2 s2 -> Forever_silent L s2 ->
   False.
 Proof.
   intros. use_star_step_triangle.
@@ -341,8 +340,8 @@ Proof.
 Qed.
 
 Lemma star_final_not_forever_reactive:
-  forall s t s', star L (genv L) s t s' -> 
-  forall T, nostep L (genv L) s' -> forever_reactive L (genv L) s T -> False.
+  forall s t s', Star L s t s' -> 
+  forall T, Nostep L s' -> Forever_reactive L s T -> False.
 Proof.
   induction 1; intros.
   inv H0. inv H1. congruence. use_nostep. 
@@ -353,9 +352,9 @@ Proof.
 Qed.
 
 Lemma star_forever_silent_inv:
-  forall s t s', star L (genv L) s t s' ->
-  forever_silent L (genv L) s -> 
-  t = E0 /\ forever_silent L (genv L) s'.
+  forall s t s', Star L s t s' ->
+  Forever_silent L s -> 
+  t = E0 /\ Forever_silent L s'.
 Proof.
   induction 1; intros.
   auto.
@@ -364,23 +363,23 @@ Qed.
 
 Lemma forever_silent_reactive_exclusive:
   forall s T,
-  forever_silent L (genv L) s -> forever_reactive L (genv L) s T -> False.
+  Forever_silent L s -> Forever_reactive L s T -> False.
 Proof.
   intros. inv H0. exploit star_forever_silent_inv; eauto. 
   intros [A B]. contradiction.
 Qed.
 
 Lemma forever_reactive_inv2:
-  forall s t1 s1, star L (genv L) s t1 s1 ->
+  forall s t1 s1, Star L s t1 s1 ->
   forall t2 s2 T1 T2,
-  star L (genv L) s t2 s2 ->
+  Star L s t2 s2 ->
   t1 <> E0 -> t2 <> E0 ->
-  forever_reactive L (genv L) s1 T1 ->
-  forever_reactive L (genv L) s2 T2 ->
+  Forever_reactive L s1 T1 ->
+  Forever_reactive L s2 T2 ->
   exists s', exists t, exists T1', exists T2',
   t <> E0 /\
-  forever_reactive L (genv L) s' T1' /\
-  forever_reactive L (genv L) s' T2' /\
+  Forever_reactive L s' T1' /\
+  Forever_reactive L s' T2' /\
   t1 *** T1 = t *** T1' /\
   t2 *** T2 = t *** T2'.
 Proof.
@@ -401,8 +400,8 @@ Qed.
 
 Lemma forever_reactive_determ':
   forall s T1 T2,
-  forever_reactive L (genv L) s T1 ->
-  forever_reactive L (genv L) s T2 ->
+  Forever_reactive L s T1 ->
+  Forever_reactive L s T2 ->
   traceinf_sim' T1 T2.
 Proof.
   cofix COINDHYP; intros.
@@ -415,17 +414,17 @@ Qed.
 
 Lemma forever_reactive_determ:
   forall s T1 T2,
-  forever_reactive L (genv L) s T1 ->
-  forever_reactive L (genv L) s T2 ->
+  Forever_reactive L s T1 ->
+  Forever_reactive L s T2 ->
   traceinf_sim T1 T2.
 Proof.
   intros. apply traceinf_sim'_sim. eapply forever_reactive_determ'; eauto.
 Qed.
 
 Lemma star_forever_reactive_inv:
-  forall s t s', star L (genv L) s t s' ->
-  forall T, forever_reactive L (genv L) s T ->
-  exists T', forever_reactive L (genv L) s' T' /\ T = t *** T'.
+  forall s t s', Star L s t s' ->
+  forall T, Forever_reactive L s T ->
+  exists T', Forever_reactive L s' T' /\ T = t *** T'.
 Proof.
   induction 1; intros. 
   exists T; auto.
@@ -437,8 +436,8 @@ Qed.
 
 Lemma forever_silent_reactive_exclusive2:
   forall s t s' T,
-  star L (genv L) s t s' -> forever_silent L (genv L) s' ->
-  forever_reactive L (genv L) s T ->
+  Star L s t s' -> Forever_silent L s' ->
+  Forever_reactive L s T ->
   False.
 Proof.
   intros. exploit star_forever_reactive_inv; eauto. 
@@ -529,28 +528,28 @@ Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
 Local Open Scope pair_scope.
 
-Definition world_sem : semantics := @mk_semantics
+Definition world_sem : semantics := @Semantics
   (state L * world)%type
   (funtype L)
   (vartype L)
-  (fun ge s t s' => L ge s#1 t s'#1 /\ possible_trace s#2 t s'#2)
+  (fun ge s t s' => step L ge s#1 t s'#1 /\ possible_trace s#2 t s'#2)
   (fun s => initial_state L s#1 /\ s#2 = initial_world)
   (fun s r => final_state L s#1 r)
-  (genv L).
+  (globalenv L).
 
 (** If the original semantics is determinate, the world-aware semantics is deterministic. *)
 
-Hypothesis D: sem_determinate L.
+Hypothesis D: determinate L.
 
 Theorem world_sem_deterministic: sem_deterministic world_sem.
 Proof.
   constructor; simpl; intros.
 (* steps *)
   destruct H; destruct H0.
-  exploit (sd_match D). eexact H. eexact H0. intros MT.
+  exploit (sd_determ D). eexact H. eexact H0. intros [A B].
   exploit match_possible_traces; eauto. intros [EQ1 EQ2]. subst t2.
-  exploit (sd_determ D). eexact H. eexact H0. intros EQ3. 
-  split; auto. rewrite (surjective_pairing s1). rewrite (surjective_pairing s2). congruence.
+  split; auto.
+  rewrite (surjective_pairing s1). rewrite (surjective_pairing s2). intuition congruence.
 (* initial states *)
   destruct H; destruct H0.
   rewrite (surjective_pairing s1). rewrite (surjective_pairing s2). decEq. 
@@ -562,8 +561,8 @@ Proof.
   red; simpl; intros. red; intros [A B]. exploit (sd_final_nostep D); eauto. 
 Qed.
 
-
-
+(*** To be updated. *)
+(***********
 Variable genv: Type.
 Variable state: Type.
 Variable step: genv -> state -> trace -> state -> Prop.
@@ -822,6 +821,8 @@ Qed.
 
 End INTERNAL_DET_TO_DET.
 
+***********)
+
 End WORLD_SEM.
 
 
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 4a57a37..a9db51e 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -33,6 +33,8 @@
   place during program linking and program loading in a real operating
   system. *)
 
+Require Recdef.
+Require Import Zwf.
 Require Import Axioms.
 Require Import Coqlib.
 Require Import Errors.
@@ -99,6 +101,13 @@ Definition find_funct (ge: t) (v: val) : option F :=
   | _ => None
   end.
 
+(** [invert_symbol ge b] returns the name associated with the given block, if any *)
+
+Definition invert_symbol (ge: t) (b: block) : option ident :=
+  PTree.fold
+    (fun res id b' => if eq_block b b' then Some id else res)
+    ge.(genv_symb) None.
+
 (** [find_var_info ge b] returns the information attached to the variable
    at address [b]. *)
 
@@ -468,6 +477,39 @@ Proof.
   intros. red; intros; subst. elim H. destruct ge. eauto. 
 Qed.
 
+Theorem invert_find_symbol:
+  forall ge id b,
+  invert_symbol ge b = Some id -> find_symbol ge id = Some b.
+Proof.
+  intros until b; unfold find_symbol, invert_symbol.
+  apply PTree_Properties.fold_rec.
+  intros. rewrite H in H0; auto. 
+  congruence.
+  intros. destruct (eq_block b v). inv H2. apply PTree.gss. 
+  rewrite PTree.gsspec. destruct (peq id k).
+  subst. assert (m!k = Some b) by auto. congruence.
+  auto.
+Qed.
+
+Theorem find_invert_symbol:
+  forall ge id b,
+  find_symbol ge id = Some b -> invert_symbol ge b = Some id.
+Proof.
+  intros until b.
+  assert (find_symbol ge id = Some b -> exists id', invert_symbol ge b = Some id').
+  unfold find_symbol, invert_symbol.
+  apply PTree_Properties.fold_rec.
+  intros. rewrite H in H0; auto.
+  rewrite PTree.gempty; congruence.
+  intros. destruct (eq_block b v). exists k; auto.
+  rewrite PTree.gsspec in H2. destruct (peq id k).
+  inv H2. congruence. auto. 
+
+  intros; exploit H; eauto. intros [id' A]. 
+  assert (id = id'). eapply genv_vars_inj; eauto. apply invert_find_symbol; auto.
+  congruence.
+Qed.
+
 (** * Construction of the initial memory state *)
 
 Section INITMEM.
@@ -517,6 +559,18 @@ Fixpoint store_init_data_list (m: mem) (b: block) (p: Z) (idl: list init_data)
       end
   end.
 
+Function store_zeros (m: mem) (b: block) (n: Z) {wf (Zwf 0) n}: option mem :=
+  if zle n 0 then Some m else
+    let n' := n - 1 in
+    match Mem.store Mint8unsigned m b n' Vzero with
+    | Some m' => store_zeros m' b n'
+    | None => None
+    end.
+Proof.
+  intros. red. omega.
+  apply Zwf_well_founded.
+Qed.
+
 Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
   match il with
   | nil => 0
@@ -530,10 +584,15 @@ Definition perm_globvar (gv: globvar V) : permission :=
 
 Definition alloc_variable (m: mem) (idv: ident * globvar V) : option mem :=
   let init := idv#2.(gvar_init) in
-  let (m', b) := Mem.alloc m 0 (init_data_list_size init) in
-  match store_init_data_list m' b 0 init with
+  let sz := init_data_list_size init in
+  let (m1, b) := Mem.alloc m 0 sz in
+  match store_zeros m1 b sz with
   | None => None
-  | Some m'' => Mem.drop_perm m'' b 0 (init_data_list_size init) (perm_globvar idv#2)
+  | Some m2 =>
+      match store_init_data_list m2 b 0 init with
+      | None => None
+      | Some m3 => Mem.drop_perm m3 b 0 sz (perm_globvar idv#2)
+      end
   end.
 
 Fixpoint alloc_variables (m: mem) (vl: list (ident * globvar V))
@@ -561,6 +620,15 @@ Proof.
   destruct (find_symbol ge i); try congruence. eapply Mem.nextblock_store; eauto. 
 Qed.
 
+Remark store_zeros_nextblock:
+  forall m b n m', store_zeros m b n = Some m' -> Mem.nextblock m' = Mem.nextblock m.
+Proof.
+  intros until n. functional induction (store_zeros m b n); intros.
+  inv H; auto.
+  rewrite IHo; eauto with mem.
+  congruence.
+Qed.
+
 Remark alloc_variables_nextblock:
   forall vl m m',
   alloc_variables m vl = Some m' ->
@@ -571,17 +639,31 @@ Proof.
   simpl length; rewrite inj_S; simpl. intros m m'. 
   unfold alloc_variable. 
   set (init := gvar_init a#2).
-  caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC.
-  caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE.
-  caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence.
-  intros m3 DROP REC.
+  set (sz := init_data_list_size init).
+  caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
+  caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
+  caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
+  caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC.
   rewrite (IHvl _ _ REC).
   rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
   rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
+  rewrite (store_zeros_nextblock _ _ _ STZ).
   rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC).
   unfold block in *; omega.
 Qed.
 
+
+Remark store_zeros_perm:
+  forall prm b' q m b n m',
+  store_zeros m b n = Some m' ->
+  Mem.perm m b' q prm -> Mem.perm m' b' q prm.
+Proof.
+  intros until n. functional induction (store_zeros m b n); intros.
+  inv H; auto.
+  eauto with mem.
+  congruence.
+Qed.
+
 Remark store_init_data_list_perm:
   forall prm b' q idl b m p m',
   store_init_data_list m b p idl = Some m' ->
@@ -605,17 +687,31 @@ Proof.
   simpl; intros. congruence.
   intros until m'. simpl. unfold alloc_variable. 
   set (init := gvar_init a#2).
-  caseEq (Mem.alloc m 0 (init_data_list_size init)). intros m1 b ALLOC.
-  caseEq (store_init_data_list m1 b 0 init); try congruence. intros m2 STORE.
-  caseEq (Mem.drop_perm m2 b 0 (init_data_list_size init) (perm_globvar a#2)); try congruence.
-  intros m3 DROP REC PERM.
+  set (sz := init_data_list_size init).
+  caseEq (Mem.alloc m 0 sz). intros m1 b ALLOC.
+  caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
+  caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
+  caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC PERM.
   assert (b' <> b). apply Mem.valid_not_valid_diff with m; eauto with mem.
   eapply IHvl; eauto.
   eapply Mem.perm_drop_3; eauto. 
-  eapply store_init_data_list_perm; eauto. 
+  eapply store_init_data_list_perm; eauto.
+  eapply store_zeros_perm; eauto.
   eauto with mem.
 Qed.
 
+Remark store_zeros_outside:
+  forall m b n m',
+  store_zeros m b n = Some m' ->
+  forall chunk b' p,
+  b' <> b -> Mem.load chunk m' b' p = Mem.load chunk m b' p.
+Proof.
+  intros until n. functional induction (store_zeros m b n); intros.
+  inv H; auto.
+  rewrite IHo; auto. eapply Mem.load_store_other; eauto. 
+  inv H.
+Qed.
+
 Remark store_init_data_list_outside:
   forall b il m p m',
   store_init_data_list m b p il = Some m' ->
@@ -699,20 +795,24 @@ Proof.
   congruence.
   unfold alloc_variable. 
   set (init := gvar_init a#2).
-  caseEq (Mem.alloc m 0 (init_data_list_size init)); intros m1 b1 ALLOC.
-  caseEq (store_init_data_list m1 b1 0 init); try congruence. intros m2 STO.
-  caseEq (Mem.drop_perm m2 b1 0 (init_data_list_size init) (perm_globvar a#2)); try congruence.
-  intros m3 DROP RED VALID.
+  set (sz := init_data_list_size init).
+  caseEq (Mem.alloc m 0 sz). intros m1 b1 ALLOC.
+  caseEq (store_zeros m1 b1 sz); try congruence. intros m2 STZ.
+  caseEq (store_init_data_list m2 b1 0 init); try congruence. intros m3 STORE.
+  caseEq (Mem.drop_perm m3 b1 0 sz (perm_globvar a#2)); try congruence. intros m4 DROP REC VALID.
   assert (b <> b1). apply Mem.valid_not_valid_diff with m; eauto with mem.
-  transitivity (Mem.load chunk m3 b p).
+  transitivity (Mem.load chunk m4 b p).
   apply IHvl; auto. red.
   rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
-  rewrite (store_init_data_list_nextblock _ _ _ _ STO).
+  rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
+  rewrite (store_zeros_nextblock _ _ _ STZ).
   change (Mem.valid_block m1 b). eauto with mem.
-  transitivity (Mem.load chunk m2 b p). 
+  transitivity (Mem.load chunk m3 b p). 
   eapply Mem.load_drop; eauto. 
+  transitivity (Mem.load chunk m2 b p).
+  eapply store_init_data_list_outside; eauto.
   transitivity (Mem.load chunk m1 b p).
-  eapply store_init_data_list_outside; eauto. 
+  eapply store_zeros_outside; eauto.
   eapply Mem.load_alloc_unchanged; eauto.
 Qed. 
 
@@ -742,14 +842,15 @@ Proof.
   contradiction.
   intros until m'; intro NEXT.
   unfold alloc_variable. destruct a as [id' gv']. simpl.
-  caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init gv'))); try congruence.
-  intros m1 b ALLOC. 
-  caseEq (store_init_data_list m1 b 0 (gvar_init gv')); try congruence.
-  intros m2 STORE.
-  caseEq (Mem.drop_perm m2 b 0 (init_data_list_size (gvar_init gv')) (perm_globvar gv')); try congruence.
-  intros m3 DROP REC NOREPET IN. inv NOREPET.
+  set (init := gvar_init gv').
+  set (sz := init_data_list_size init).
+  caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC.
+  caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
+  caseEq (store_init_data_list m2 b 0 init); try congruence. intros m3 STORE.
+  caseEq (Mem.drop_perm m3 b 0 sz (perm_globvar gv')); try congruence.
+  intros m4 DROP REC NOREPET IN. inv NOREPET.
   exploit Mem.alloc_result; eauto. intro BEQ. 
-  destruct IN. inv H.
+  destruct IN. inversion H; subst id gv.
   exists (Mem.nextblock m); split. 
   rewrite add_variables_same_symb; auto. unfold find_symbol; simpl. 
   rewrite PTree.gss. congruence. 
@@ -757,23 +858,24 @@ Proof.
   rewrite NEXT. apply ZMap.gss.
   simpl. rewrite <- NEXT; omega.
   split. red; intros.
-  eapply alloc_variables_perm; eauto.
-  eapply Mem.perm_drop_1; eauto. 
+  rewrite <- BEQ. eapply alloc_variables_perm; eauto. eapply Mem.perm_drop_1; eauto. 
   intros NOVOL. 
-  apply load_store_init_data_invariant with m2.
-  intros. transitivity (Mem.load chunk m3 (Mem.nextblock m) ofs).
+  apply load_store_init_data_invariant with m3.
+  intros. transitivity (Mem.load chunk m4 (Mem.nextblock m) ofs).
   eapply load_alloc_variables; eauto. 
   red. rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
   rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
-  change (Mem.valid_block m1 (Mem.nextblock m)). eauto with mem.
+  rewrite (store_zeros_nextblock _ _ _ STZ).
+  change (Mem.valid_block m1 (Mem.nextblock m)). rewrite <- BEQ. eauto with mem.
   eapply Mem.load_drop; eauto. repeat right. 
-  unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv); auto with mem.
-  eapply store_init_data_list_charact; eauto. 
+  unfold perm_globvar. rewrite NOVOL. destruct (gvar_readonly gv'); auto with mem.
+  rewrite <- BEQ. eapply store_init_data_list_charact; eauto. 
 
-  apply IHvl with m3; auto.
+  apply IHvl with m4; auto.
   simpl.
   rewrite (Mem.nextblock_drop _ _ _ _ _ _ DROP). 
   rewrite (store_init_data_list_nextblock _ _ _ _ STORE).
+  rewrite (store_zeros_nextblock _ _ _ STZ).
   rewrite (Mem.nextblock_alloc _ _ _ _ _ ALLOC). unfold block in *; omega.
 Qed.
 
@@ -861,6 +963,19 @@ Proof.
   eapply IHidl. eapply store_init_data_neutral; eauto. auto. eauto. 
 Qed.
 
+Lemma store_zeros_neutral:
+  forall m b n m',
+  Mem.inject_neutral thr m ->
+  b < thr ->
+  store_zeros m b n = Some m' ->
+  Mem.inject_neutral thr m'.
+Proof.
+  intros until n. functional induction (store_zeros m b n); intros.
+  inv H1; auto.
+  apply IHo; auto. eapply Mem.store_inject_neutral; eauto. constructor.  
+  inv H1.
+Qed.
+
 Lemma alloc_variable_neutral:
   forall id m m',
   alloc_variable ge m id = Some m' ->
@@ -868,16 +983,18 @@ Lemma alloc_variable_neutral:
   Mem.nextblock m < thr ->
   Mem.inject_neutral thr m'.
 Proof.
-  intros until m'. unfold alloc_variable. 
-  caseEq (Mem.alloc m 0 (init_data_list_size (gvar_init id#2))); intros m1 b ALLOC.
-  caseEq (store_init_data_list ge m1 b 0 (gvar_init id#2)); try congruence.
-  intros m2 STORE DROP NEUTRAL NEXT.
+  intros until m'. unfold alloc_variable.
+  set (init := gvar_init id#2).
+  set (sz := init_data_list_size init).
+  caseEq (Mem.alloc m 0 sz); try congruence. intros m1 b ALLOC.
+  caseEq (store_zeros m1 b sz); try congruence. intros m2 STZ.
+  caseEq (store_init_data_list ge m2 b 0 init); try congruence.
+  intros m3 STORE DROP NEUTRAL NEXT.
+  assert (b < thr). rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto.
   eapply Mem.drop_inject_neutral; eauto. 
-  eapply store_init_data_list_neutral with (b := b).
+  eapply store_init_data_list_neutral with (m := m2) (b := b); eauto.
+  eapply store_zeros_neutral with (m := m1); eauto. 
   eapply Mem.alloc_inject_neutral; eauto.
-  rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto.
-  eauto.
-  rewrite (Mem.alloc_result _ _ _ _ _ ALLOC). auto.
 Qed.
 
 Lemma alloc_variables_neutral:
@@ -1099,11 +1216,12 @@ Proof.
   inv H. 
   unfold alloc_variable; simpl. 
   destruct (Mem.alloc m 0 (init_data_list_size init)). 
+  destruct (store_zeros m0 b (init_data_list_size init)); auto.
   rewrite store_init_data_list_match. 
-  destruct (store_init_data_list (globalenv p) m0 b 0 init); auto.
+  destruct (store_init_data_list (globalenv p) m1 b 0 init); auto.
   change (perm_globvar (mkglobvar info2 init ro vo))
     with (perm_globvar (mkglobvar info1 init ro vo)).
-  destruct (Mem.drop_perm m1 b 0 (init_data_list_size init)
+  destruct (Mem.drop_perm m2 b 0 (init_data_list_size init)
     (perm_globvar (mkglobvar info1 init ro vo))); auto.
 Qed.
 
diff --git a/cparser/StructAssign.ml b/cparser/StructAssign.ml
index edf8821..6d38b55 100644
--- a/cparser/StructAssign.ml
+++ b/cparser/StructAssign.ml
@@ -50,20 +50,17 @@ let default_memcpy () =
       memcpy_decl := Some id;
       (id, memcpy_type)
 
-let rec find_memcpy env = function
-  | [] ->
-      default_memcpy()
-  | name :: rem ->
-      try lookup_function env name with Env.Error _ -> find_memcpy env rem
-
-let memcpy_1_ident env =
-  find_memcpy env ["__builtin_memcpy"; "memcpy"]
-let memcpy_2_ident env =
-  find_memcpy env ["__builtin_memcpy_al2"; "__builtin_memcpy"; "memcpy"]
-let memcpy_4_ident env =
-  find_memcpy env ["__builtin_memcpy_al4"; "__builtin_memcpy"; "memcpy"]
-let memcpy_8_ident env =
-  find_memcpy env ["__builtin_memcpy_al8"; "__builtin_memcpy"; "memcpy"]
+let find_memcpy env =
+  try
+    (lookup_function env "__builtin_memcpy_aligned", true)
+  with Env.Error _ ->
+  try
+    (lookup_function env "__builtin_memcpy", false)
+  with Env.Error _ ->
+  try
+    (lookup_function env "memcpy", false)
+  with Env.Error _ ->
+    (default_memcpy(), false)
 
 (* Smart constructor for "," expressions *)
 
@@ -84,20 +81,19 @@ let rec addrof e =
    [lhs] and [rhs] must be l-values. *)
 
 let transf_assign env lhs rhs =
-  let (al, sz) =
-     match Cutil.alignof env lhs.etyp, Cutil.sizeof env lhs.etyp with
-     | Some al, Some sz -> (al, sz)
-     | _, _ -> (1, 1) in
-  let (ident, ty) = 
-    if al mod 8 = 0 && sz mod 8 = 0 then memcpy_8_ident env
-    else if al mod 4 = 0 && sz mod 4 = 0 then memcpy_4_ident env
-    else if al mod 2 = 0 && sz mod 2 = 0 then memcpy_2_ident env
-    else memcpy_1_ident env in
+  let al =
+     match Cutil.alignof env lhs.etyp with Some al -> al | None -> 1 in
+  let ((ident, ty), four_args) = find_memcpy env in
   let memcpy = {edesc = EVar(ident); etyp = ty} in
-  let e_lhs = addrof lhs in
-  let e_rhs = addrof rhs in
-  let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])} in
-  {edesc = ECall(memcpy, [e_lhs; e_rhs; e_size]); etyp = TVoid[]}
+  let e_lhs = addrof lhs
+  and e_rhs = addrof rhs
+  and e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])}
+  and e_align = intconst (Int64.of_int al) size_t_ikind in
+  let args =
+    if four_args
+    then [e_lhs; e_rhs; e_size; e_align]
+    else [e_lhs; e_rhs; e_size] in
+  {edesc = ECall(memcpy, args); etyp = TVoid[]}
 
 (* Detect invariant l-values *)
 
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 2a96c38..87de59f 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -22,6 +22,7 @@ let option_fbitfields = ref false
 let option_fvararg_calls = ref true
 let option_fpacked_structs = ref false
 let option_fmadd = ref false
+let option_fsse = ref true
 let option_dparse = ref false
 let option_dcmedium = ref false
 let option_dclight = ref false
diff --git a/driver/Compiler.v b/driver/Compiler.v
index a51cd8f..37a187e 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -24,6 +24,7 @@ Require Import Smallstep.
 Require Csyntax.
 Require Csem.
 Require Cstrategy.
+Require Cexec.
 Require Clight.
 Require Csharpminor.
 Require Cminor.
@@ -82,8 +83,8 @@ Require Reloadtyping.
 Require Stackingproof.
 Require Stackingtyping.
 Require Asmgenproof.
+
 (** Pretty-printers (defined in Caml). *)
-Parameter print_Csyntax: Csyntax.program -> unit.
 Parameter print_Clight: Clight.program -> unit.
 Parameter print_Cminor: Cminor.program -> unit.
 Parameter print_RTL: RTL.fundef -> unit.
@@ -180,13 +181,13 @@ Definition transf_clight_program (p: Clight.program) : res Asm.program :=
 
 Definition transf_c_program (p: Csyntax.program) : res Asm.program :=
   OK p 
-   @@ print print_Csyntax
   @@@ SimplExpr.transl_program
   @@@ transf_clight_program.
 
-(** Force [Initializers] to be extracted as well. *)
+(** Force [Initializers] and [Cexec] to be extracted as well. *)
 
 Definition transl_init := Initializers.transl_init.
+Definition cexec_do_step := Cexec.do_step.
 
 (** The following lemmas help reason over compositions of passes. *)
 
@@ -403,7 +404,7 @@ Theorem transf_cstrategy_program_correct:
 Proof.
   intros.
   assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics tp)).
-  revert H; unfold transf_c_program; simpl. rewrite print_identity.
+  revert H; unfold transf_c_program; simpl.
   caseEq (SimplExpr.transl_program p); simpl; try congruence; intros p0 EQ0.
   intros EQ1.
   eapply compose_forward_simulation. apply SimplExprproof.transl_program_correct. eauto.
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 6aa63e0..d5a659d 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -62,9 +62,9 @@ let preprocess ifile ofile =
     exit 2
   end
 
-(* From preprocessed C to asm *)
+(* From preprocessed C to Csyntax *)
 
-let compile_c_file sourcename ifile ofile =
+let parse_c_file sourcename ifile =
   Sections.initialize();
   (* Simplification options *)
   let simplifs =
@@ -94,11 +94,22 @@ let compile_c_file sourcename ifile ofile =
     | None -> exit 2
     | Some p -> p in
   flush stderr;
-  (* Prepare to dump Csyntax, Clight, RTL, etc, if requested *)
+  (* Save CompCert C AST if requested *)
+  if !option_dcmedium then begin
+    let ofile = Filename.chop_suffix sourcename ".c" ^ ".compcert.c" in
+    let oc = open_out ofile in
+    PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
+    close_out oc
+  end;
+  csyntax
+
+(* From CompCert C AST to asm *)
+
+let compile_c_ast sourcename csyntax ofile =
+  (* Prepare to dump Clight, RTL, etc, if requested *)
   let set_dest dst opt ext =
     dst := if !opt then Some (Filename.chop_suffix sourcename ".c" ^ ext)
                    else None in
-  set_dest PrintCsyntax.destination option_dcmedium ".compcert.c";
   set_dest PrintClight.destination option_dclight ".light.c";
   set_dest PrintCminor.destination option_dcminor ".cm";
   set_dest PrintRTL.destination_rtl option_drtl ".rtl";
@@ -120,6 +131,11 @@ let compile_c_file sourcename ifile ofile =
   PrintAsm.print_program oc asm;
   close_out oc
 
+(* From C source to asm *)
+
+let compile_c_file sourcename ifile ofile =
+  compile_c_ast sourcename (parse_c_file sourcename ifile) ofile
+
 (* From Cminor to asm *)
 
 let compile_cminor_file ifile ofile =
@@ -178,6 +194,8 @@ let linker exe_name files =
 
 (* Processing of a .c file *)
 
+let option_interp = ref false
+
 let process_c_file sourcename =
   let prefixname = Filename.chop_suffix sourcename ".c" in
   if !option_E then begin
@@ -185,7 +203,10 @@ let process_c_file sourcename =
   end else begin
     let preproname = Filename.temp_file "compcert" ".i" in
     preprocess sourcename preproname;
-    if !option_S then begin
+    if !option_interp then begin
+      let csyntax = parse_c_file sourcename preproname in
+      Interp.execute csyntax
+    end else if !option_S then begin
       compile_c_file sourcename preproname (prefixname ^ ".s")
     end else begin
       let asmname =
@@ -235,57 +256,13 @@ let process_S_file sourcename =
   end;
   prefixname ^ ".o"
 
-(* Command-line parsing *)
+(* Interpretation of a .c file *)
 
-let usage_string =
-"ccomp [options] <source files>
-Recognized source files:
-  .c             C source file
-  .cm            Cminor source file
-  .s             Assembly file
-  .S             Assembly file, to be run through the preprocessor
-  .o             Object file
-  .a             Library file
-Processing options:
-  -E             Preprocess only, send result to standard output
-  -S             Compile to assembler only, save result in <file>.s
-  -c             Compile to object file only (no linking), result in <file>.o
-Preprocessing options:
-  -I<dir>        Add <dir> to search path for #include files
-  -D<symb>=<val> Define preprocessor symbol
-  -U<symb>       Undefine preprocessor symbol
-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]
-  -fstruct-passing  Emulate passing structs and unions by value [off]
-  -fstruct-assign   Emulate assignment between structs or unions [off]
-  -fvararg-calls Emulate calls to variable-argument functions [on]
-  -fpacked-structs  Emulate packed structs [off]
-Code generation options:
-  -fmadd         Use fused multiply-add and multiply-sub instructions [off]
-  -fsmall-data <n>  Set maximal size <n> for allocation in small data area
-  -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
-Tracing options:
-  -dparse        Save C file after parsing and elaboration in <file>.parse.c
-  -dc            Save generated Compcert C in <file>.compcert.c
-  -dclight       Save generated Clight in <file>.light.c
-  -dcminor       Save generated Cminor in <file>.cm
-  -drtl          Save unoptimized generated RTL in <file>.rtl
-  -dtailcall     Save RTL after tail call optimization in <file>.tailcall.rtl
-  -dcastopt      Save RTL after cast optimization in <file>.castopt.rtl
-  -dconstprop    Save RTL after constant propagation in <file>.constprop.rtl
-  -dcse          Save RTL after CSE optimization in <file>.cse.rtl
-  -dalloc        Save LTL after register allocation in <file>.alloc.ltl
-  -dmach         Save generated Mach code in <file>.mach
-  -dasm          Save generated assembly in <file>.s
-Linking options:
-  -l<lib>        Link library <lib>
-  -L<dir>        Add <dir> to search path for libraries
-  -o <file>      Generate executable in <file> (default: a.out)
-General options:
-  -stdlib <dir>  Set the path of the Compcert run-time library [MacOS X only]
-  -v             Print external commands before invoking them
-"
+let execute_c_file sourcename =
+  let preproname = Filename.temp_file "compcert" ".i" in
+  preprocess sourcename preproname
+
+(* Command-line parsing *)
 
 type action =
   | Set of bool ref
@@ -340,6 +317,63 @@ let parse_cmdline spec usage =
     end
   in parse 1
 
+let usage_string =
+"ccomp [options] <source files>
+Recognized source files:
+  .c             C source file
+  .cm            Cminor source file
+  .s             Assembly file
+  .S             Assembly file, to be run through the preprocessor
+  .o             Object file
+  .a             Library file
+Processing options:
+  -E             Preprocess only, send result to standard output
+  -S             Compile to assembler only, save result in <file>.s
+  -c             Compile to object file only (no linking), result in <file>.o
+Preprocessing options:
+  -I<dir>        Add <dir> to search path for #include files
+  -D<symb>=<val> Define preprocessor symbol
+  -U<symb>       Undefine preprocessor symbol
+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]
+  -fstruct-passing  Emulate passing structs and unions by value [off]
+  -fstruct-assign   Emulate assignment between structs or unions [off]
+  -fvararg-calls Emulate calls to variable-argument functions [on]
+  -fpacked-structs  Emulate packed structs [off]
+Code generation options: (use -fno-<opt> to turn off -f<opt>) :
+  -fmadd         (PowerPC) Use fused multiply-add and multiply-sub instructions [off]
+  -fsse          (IA32) Use SSE2 instructions for some integer operations [on]
+  -fsmall-data <n>  Set maximal size <n> for allocation in small data area
+  -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
+Tracing options:
+  -dparse        Save C file after parsing and elaboration in <file>.parse.c
+  -dc            Save generated Compcert C in <file>.compcert.c
+  -dclight       Save generated Clight in <file>.light.c
+  -dcminor       Save generated Cminor in <file>.cm
+  -drtl          Save unoptimized generated RTL in <file>.rtl
+  -dtailcall     Save RTL after tail call optimization in <file>.tailcall.rtl
+  -dcastopt      Save RTL after cast optimization in <file>.castopt.rtl
+  -dconstprop    Save RTL after constant propagation in <file>.constprop.rtl
+  -dcse          Save RTL after CSE optimization in <file>.cse.rtl
+  -dalloc        Save LTL after register allocation in <file>.alloc.ltl
+  -dmach         Save generated Mach code in <file>.mach
+  -dasm          Save generated assembly in <file>.s
+Linking options:
+  -l<lib>        Link library <lib>
+  -L<dir>        Add <dir> to search path for libraries
+  -o <file>      Generate executable in <file> (default: a.out)
+General options:
+  -stdlib <dir>  Set the path of the Compcert run-time library [MacOS X only]
+  -v             Print external commands before invoking them
+Interpreter mode:
+  -interp        Execute given .c files using the reference interpreter
+  -quiet         Suppress diagnostic messages for the interpreter
+  -trace         Have the interpreter produce a detailed trace of reductions
+  -random        Randomize execution order
+  -all           Simulate all possible execution orders
+"
+
 let cmdline_actions =
   let f_opt name ref =
     ["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in
@@ -367,6 +401,11 @@ let cmdline_actions =
   "-S$", Set option_S;
   "-c$", Set option_c;
   "-v$", Set option_v;
+  "-interp$", Set option_interp;
+  "-quiet$", Self (fun _ -> Interp.trace := 0);
+  "-trace$", Self (fun _ -> Interp.trace := 2);
+  "-random$", Self (fun _ -> Interp.mode := Interp.Random);
+  "-all$", Self (fun _ -> Interp.mode := Interp.All);
   ".*\\.c$", Self (fun s ->
       let objfile = process_c_file s in
       linker_options := objfile :: !linker_options);
@@ -391,6 +430,7 @@ let cmdline_actions =
   @ f_opt "vararg-calls" option_fvararg_calls
   @ f_opt "madd" option_fmadd
   @ f_opt "packed-structs" option_fpacked_structs
+  @ f_opt "sse" option_fsse
 
 let _ =
   Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 };
@@ -405,7 +445,7 @@ let _ =
   CPragmas.initialize();
   parse_cmdline cmdline_actions usage_string;
   if !linker_options <> [] 
-  && not (!option_c || !option_S || !option_E)
+  && not (!option_c || !option_S || !option_E || !option_interp)
   then begin
     linker !exe_name !linker_options
   end
diff --git a/driver/Interp.ml b/driver/Interp.ml
new file mode 100644
index 0000000..84037ae
--- /dev/null
+++ b/driver/Interp.ml
@@ -0,0 +1,408 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Interpreting CompCert C sources *)
+
+open Format
+open Camlcoq
+open Datatypes
+open BinPos
+open BinInt
+open AST
+open Values
+open Memory
+open Globalenvs
+open Events
+open Csyntax
+open Csem
+open Clflags
+
+(* Configuration *)
+
+let trace = ref 1   (* 0 if quiet, 1 if normally verbose, 2 if full trace *)
+
+type mode = First | Random | All
+
+let mode = ref First
+
+(* Printing events *)
+
+let print_eventval p = function
+  | EVint n -> fprintf p "%ld" (camlint_of_coqint n)
+  | EVfloat f -> fprintf p "%F" f
+  | EVptr_global(id, ofs) -> 
+      fprintf p "&%s%+ld" (extern_atom id) (camlint_of_coqint ofs)
+
+let print_eventval_list p = function
+  | [] -> ()
+  | v1 :: vl ->
+      print_eventval p v1;
+      List.iter (fun v -> fprintf p ",@ %a" print_eventval v) vl
+
+let print_event p = function
+  | Event_syscall(id, args, res) ->
+      fprintf p "extcall %s(%a) -> %a"
+                (extern_atom id)
+                print_eventval_list args
+                print_eventval res
+  | Event_vload(chunk, id, ofs, res) ->
+      fprintf p "volatile load %s[&%s%+ld] -> %a"
+                (PrintCminor.name_of_chunk chunk)
+                (extern_atom id) (camlint_of_coqint ofs)
+                print_eventval res
+  | Event_vstore(chunk, id, ofs, arg) ->
+      fprintf p "volatile store %s[&%s%+ld] <- %a"
+                (PrintCminor.name_of_chunk chunk)
+                (extern_atom id) (camlint_of_coqint ofs)
+                print_eventval arg
+  | Event_annot(text, args) ->
+      fprintf p "annotation \"%s\" %a"
+                (extern_atom text)
+                print_eventval_list args
+
+(* Printing states *)
+
+let name_of_fundef prog fd =
+  let rec find_name = function
+  | [] -> "<unknown function>"
+  | Coq_pair(id, fd') :: rem ->
+      if fd = fd' then extern_atom id else find_name rem
+  in find_name prog.prog_funct
+
+let name_of_function prog fn =
+  name_of_fundef prog (Internal fn)
+
+let print_val p = function
+  | Vint n -> fprintf p "%ld" (camlint_of_coqint n)
+  | Vfloat f -> fprintf p "%F" f
+  | Vptr(b, ofs) -> fprintf p "<ptr>"
+  | Vundef -> fprintf p "<undef>"
+
+let print_val_list p = function
+  | [] -> ()
+  | v1 :: vl ->
+      print_val p v1;
+      List.iter (fun v -> fprintf p ",@ %a" print_val v) vl
+
+let print_state prog p = function
+  | State(f, s, k, e, m) ->
+      fprintf p "in function %s, statement@ @[<hv 0>%a@]"
+              (name_of_function prog f)
+              PrintCsyntax.print_stmt s 
+  | ExprState(f, r, k, e, m) ->
+      fprintf p "in function %s, expression@ @[<hv 0>%a@]"
+              (name_of_function prog f)
+              PrintCsyntax.print_expr r
+  | Callstate(fd, args, k, m) ->
+      fprintf p "calling@ @[<hov 2>%s(%a)@]"
+              (name_of_fundef prog fd)
+              print_val_list args
+  | Returnstate(res, k, m) ->
+      fprintf p "returning@ %a"
+              print_val res
+
+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
+
+(* Comparing memory states *)
+
+let rec compare_Z_range lo hi f =
+  if coq_Zcompare lo hi = Lt then begin
+    let c = f lo in if c <> 0 then c else compare_Z_range (coq_Zsucc lo) hi f
+  end else 0
+
+let compare_mem m1 m2 =
+  if m1 == m2 then 0 else
+  let c = compare m1.Mem.nextblock m2.Mem.nextblock in if c <> 0 then c else
+  compare_Z_range Z0 m1.Mem.nextblock (fun b ->
+    let (Coq_pair(lo, hi) as bnds) = m1.Mem.bounds b in
+    let c = compare bnds (m2.Mem.bounds b) in if c <> 0 then c else
+    let contents1 = m1.Mem.mem_contents b and contents2 = m2.Mem.mem_contents b in
+    if contents1 == contents2 then 0 else
+    let c = compare_Z_range lo hi (fun ofs ->
+               compare (contents1 ofs) (contents2 ofs)) in if c <> 0 then c else
+    let access1 = m1.Mem.mem_access b and access2 = m2.Mem.mem_access b in
+    if access1 == access2 then 0 else
+    compare_Z_range lo hi (fun ofs -> compare (access1 ofs) (access2 ofs)))
+
+(* Comparing continuations *)
+
+let some_expr = Evar(Coq_xH, Tvoid)
+
+let rank_cont = function
+  | Kstop -> 0
+  | Kdo _ -> 1
+  | Kseq _ -> 2
+  | Kifthenelse _ -> 3
+  | Kwhile1 _ -> 4
+  | Kwhile2 _ -> 5
+  | Kdowhile1 _ -> 6
+  | Kdowhile2 _ -> 7
+  | Kfor2 _ -> 8
+  | Kfor3 _ -> 9
+  | Kfor4 _ -> 10
+  | Kswitch1 _ -> 11
+  | Kswitch2 _ -> 12
+  | Kreturn _ -> 13
+  | Kcall _ -> 14
+
+let rec compare_cont k1 k2 =
+  if k1 == k2 then 0 else
+  match k1, k2 with
+  | Kstop, Kstop -> 0
+  | Kdo k1, Kdo k2 -> compare_cont k1 k2
+  | Kseq(s1, k1), Kseq(s2, k2) ->  
+      let c = compare s1 s2 in if c <> 0 then c else compare_cont k1 k2
+  | Kifthenelse(s1, s1', k1), Kifthenelse(s2, s2', k2) ->
+      let c = compare (s1,s1') (s2,s2') in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kwhile1(e1, s1, k1), Kwhile1(e2, s2, k2) ->
+      let c = compare (e1,s1) (e2,s2) in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kwhile2(e1, s1, k1), Kwhile2(e2, s2, k2) ->
+      let c = compare (e1,s1) (e2,s2) in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kdowhile1(e1, s1, k1), Kdowhile1(e2, s2, k2) ->
+      let c = compare (e1,s1) (e2,s2) in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kdowhile2(e1, s1, k1), Kdowhile2(e2, s2, k2) ->
+      let c = compare (e1,s1) (e2,s2) in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kfor2(e1, s1, s1', k1), Kfor2(e2, s2, s2', k2) ->
+      let c = compare (e1,s1,s1') (e2,s2,s2') in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kfor3(e1, s1, s1', k1), Kfor3(e2, s2, s2', k2) ->
+      let c = compare (e1,s1,s1') (e2,s2,s2') in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kfor4(e1, s1, s1', k1), Kfor4(e2, s2, s2', k2) ->
+      let c = compare (e1,s1,s1') (e2,s2,s2') in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kswitch1(sl1, k1), Kswitch1(sl2, k2) ->
+      let c = compare sl1 sl2 in
+      if c <> 0 then c else compare_cont k1 k2
+  | Kreturn k1, Kreturn k2 ->
+      compare_cont k1 k2
+  | Kcall(f1, e1, c1, ty1, k1), Kcall(f2, e2, c2, ty2, k2) ->
+      let c = compare (f1, e1, c1 some_expr, ty1) (f2, e2, c2 some_expr, ty2) in
+      if c <> 0 then c else compare_cont k1 k2
+  | _, _ ->
+      compare (rank_cont k1) (rank_cont k2)
+
+(* Comparing states *)
+
+let rank_state = function
+  | State _ -> 0
+  | ExprState _ -> 1
+  | Callstate _ -> 2
+  | Returnstate _ -> 3
+
+let compare_state s1 s2 =
+  if s1 == s2 then 0 else
+  match s1, s2 with
+  | State(f1,s1,k1,e1,m1), State(f2,s2,k2,e2,m2) ->
+      let c = compare (f1,s1,e1) (f2,s2,e2) in if c <> 0 then c else
+      let c = compare_cont k1 k2 in if c <> 0 then c else
+      compare_mem m1 m2
+  | ExprState(f1,r1,k1,e1,m1), ExprState(f2,r2,k2,e2,m2) ->
+      let c = compare (f1,r1,e1) (f2,r2,e2) in if c <> 0 then c else
+      let c = compare_cont k1 k2 in if c <> 0 then c else
+      compare_mem m1 m2
+  | Callstate(fd1,args1,k1,m1), Callstate(fd2,args2,k2,m2) ->
+      let c = compare (fd1,args1) (fd2,args2) in if c <> 0 then c else
+      let c = compare_cont k1 k2 in if c <> 0 then c else
+      compare_mem m1 m2
+  | Returnstate(res1,k1,m1), Returnstate(res2,k2,m2) ->
+      let c = compare res1 res2 in if c <> 0 then c else
+      let c = compare_cont k1 k2 in if c <> 0 then c else
+      compare_mem m1 m2
+  | _, _ ->
+      compare (rank_state s1) (rank_state s2)
+
+module StateSet =
+  Set.Make(struct type t = state let compare = compare_state end)
+
+(* Extract a string from a global pointer *)
+
+let extract_string ge m id ofs =
+  let b = Buffer.create 80 in
+  let rec extract blk ofs =
+    match Memory.Mem.load Mint8unsigned m blk ofs with
+    | Some(Vint n) ->
+        let c = Char.chr (Int32.to_int (camlint_of_coqint n)) in
+        if c = '\000' then begin
+          Some(Buffer.contents b)
+        end else begin
+          Buffer.add_char b c; 
+          extract blk (coq_Zsucc ofs)
+        end
+    | _ ->
+        None in
+  match Genv.find_symbol ge id with
+  | None -> None
+  | Some blk -> extract blk ofs
+
+(* Emulation of printf *)
+
+(* All ISO C 99 formats except size modifiers [ll] (long long) and [L]
+   (long double) *)
+
+let re_conversion = Str.regexp
+  "%[-+0# ]*[0-9]*\\(\\.[0-9]*\\)?\\([lhjzt]\\|hh\\)?\\([aAcdeEfgGinopsuxX%]\\)"
+
+external format_float: string -> float -> string
+  = "caml_format_float"
+external format_int32: string -> int32 -> string
+  = "caml_int32_format"
+
+let do_printf ge m fmt args =
+
+  let b = Buffer.create 80 in
+  let len = String.length fmt in
+
+  let opt_search_forward pos =
+    try Some(Str.search_forward re_conversion fmt pos)
+    with Not_found -> None in
+
+  let rec scan pos args =
+    if pos < len then begin
+    match opt_search_forward pos with
+    | None ->
+        Buffer.add_substring b fmt pos (len - pos)
+    | Some pos1 ->
+        Buffer.add_substring b fmt pos (pos1 - pos);
+        let pat = Str.matched_string fmt
+        and conv = Str.matched_group 3 fmt
+        and pos' = Str.match_end() in
+        match args, conv.[0] with
+        | _, '%' ->
+            Buffer.add_char b '%';
+            scan pos' args
+        | [], _ ->
+            Buffer.add_string b "<missing argument>";
+            scan pos' []
+        | EVint i :: args', ('d'|'i'|'u'|'o'|'x'|'X'|'c') ->
+            Buffer.add_string b (format_int32 pat (camlint_of_coqint i));
+            scan pos' args'
+        | EVfloat f :: args', ('f'|'e'|'E'|'g'|'G'|'a') ->
+            Buffer.add_string b (format_float pat f);
+            scan pos' args'
+        | EVptr_global(id, ofs) :: args', 's' ->
+            Buffer.add_string b
+              (match extract_string ge m id ofs with
+               | Some s -> s
+               | None -> "<bad string>");
+            scan pos' args'
+        | EVptr_global(id, ofs) :: args', 'p' ->
+            Printf.bprintf b "<&%s%+ld>" (extern_atom id) (camlint_of_coqint ofs);
+            scan pos' args'
+        | _ :: args', _ ->
+            Buffer.add_string b "<formatting error>";
+            scan pos' args'
+    end
+  in scan 0 args; Buffer.contents b
+
+(* Implementing external functions *)
+
+let re_stub = Str.regexp "\\$[if]*$"
+
+let chop_stub name = Str.replace_first re_stub "" name
+
+let rec world = Determinism.World(world_io, world_vload, world_vstore)
+
+and world_io id args =
+  match chop_stub(extern_atom id), args with
+  | "printf", EVptr_global(id, ofs) :: args' ->
+      Some(Coq_pair(EVint Integers.Int.zero, world))
+  | _, _ ->
+      None
+
+and world_vload chunk id ofs =
+  let res = match chunk with
+    | Mint8signed -> EVint(coqint_of_camlint(Int32.sub (Random.int32 0x100l) 0x80l))
+    | Mint8unsigned -> EVint(coqint_of_camlint(Random.int32 0x100l))
+    | Mint16signed -> EVint(coqint_of_camlint(Int32.sub (Random.int32 0x10000l) 0x8000l))
+    | Mint16unsigned -> EVint(coqint_of_camlint(Random.int32 0x10000l))
+    | Mint32 -> EVint(coqint_of_camlint(Random.int32 0x7FFF_FFFFl))
+    | Mfloat32 -> EVfloat(Floats.Float.singleoffloat(Random.float 1.0))
+    | Mfloat64 -> EVfloat(Random.float 1.0)
+  in Some(Coq_pair(res, world))
+
+and world_vstore chunk id ofs arg =
+  Some world
+
+let do_event p ge time s ev =
+  if !trace >= 1 then
+    fprintf p "@[<hov 2>Time %d: observable event: %a@]@."
+              time print_event ev;
+  match ev with
+  | Event_syscall(name, EVptr_global(id, ofs) :: args', res) 
+    when chop_stub (extern_atom name) = "printf" ->
+      flush stderr;
+      let m = mem_of_state s in
+      begin match extract_string ge m id ofs with
+      | Some fmt -> print_string (do_printf ge m fmt args')
+      | None -> print_string "<bad printf>\n"
+      end;
+      flush stdout
+  | _ -> ()
+
+let do_events p ge time s t =
+  List.iter (do_event p ge time s) t
+
+(* Exploration *)
+
+let do_step p prog ge time s =
+  if !trace >= 2 then
+    fprintf p "@[<hov 2>Time %d: %a@]@." time (print_state prog) s;
+  match Cexec.at_final_state s with
+  | Some r ->
+      if !trace >= 1 then begin
+        fprintf p "Time %d: program terminated (exit code = %ld)@."
+                  time (camlint_of_coqint r);
+        []
+      end else begin
+        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 (Coq_pair(t, s')) -> do_events p ge time s t) l;
+          List.map snd l
+
+let rec explore p prog ge time ss =
+  let succs =
+    StateSet.fold (fun s l -> do_step p prog ge time s @ l) ss [] in
+  if succs <> [] then begin
+    let ss' =
+      match !mode with
+      | First -> StateSet.singleton (List.hd succs)
+      | Random -> StateSet.singleton (List.nth succs (Random.int (List.length succs)))
+      | All -> List.fold_right StateSet.add succs StateSet.empty in
+    explore p prog ge (time + 1) ss'
+  end
+
+let execute prog =
+  let p = err_formatter in
+  pp_set_max_boxes p 10;
+  begin match Cexec.do_initial_state prog with
+  | None -> fprintf p "ERROR: Initial state undefined@."
+  | Some(Coq_pair(ge, s)) -> explore p prog ge 0 (StateSet.singleton s)
+  end
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 765bebd..4bfac69 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -82,7 +82,6 @@ Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
 Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2.
 
 (* Compiler *)
-Extract Constant Compiler.print_Csyntax => "PrintCsyntax.print_if".
 Extract Constant Compiler.print_Clight => "PrintClight.print_if".
 Extract Constant Compiler.print_Cminor => "PrintCminor.print_if".
 Extract Constant Compiler.print_RTL => "PrintRTL.print_rtl".
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index c9ee970..842957f 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -268,21 +268,26 @@ let print_annot_val oc txt args res =
 (* Unaligned memory accesses are quite fast on IA32, so use large
    memory accesses regardless of alignment. *)
 
-let print_builtin_memcpy oc sz al args =
-  let (dst, src) =
-    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
+let print_builtin_memcpy_small oc sz al src dst =
   let tmp =
     if src <> ECX && dst <> ECX then ECX
     else if src <> EDX && dst <> EDX then EDX
     else EAX in
+  let need_tmp =
+    sz mod 4 <> 0 || not !Clflags.option_fsse in
   let rec copy ofs sz =
-    if sz >= 8 then begin
+    if sz >= 8 && !Clflags.option_fsse then begin
       fprintf oc "	movq	%d(%a), %a\n" ofs ireg src freg XMM6;
       fprintf oc "	movq	%a, %d(%a)\n" freg XMM6 ofs ireg dst;
       copy (ofs + 8) (sz - 8)
     end else if sz >= 4 then begin
-      fprintf oc "	movd	%d(%a), %a\n" ofs ireg src freg XMM6;
-      fprintf oc "	movd	%a, %d(%a)\n" freg XMM6 ofs ireg dst;
+      if !Clflags.option_fsse then begin
+        fprintf oc "	movd	%d(%a), %a\n" ofs ireg src freg XMM6;
+        fprintf oc "	movd	%a, %d(%a)\n" freg XMM6 ofs ireg dst
+      end else begin
+        fprintf oc "	movl	%d(%a), %a\n" ofs ireg src ireg tmp;
+        fprintf oc "	movl	%a, %d(%a)\n" ireg tmp ofs ireg dst
+      end;
       copy (ofs + 4) (sz - 4)
     end else if sz >= 2 then begin
       fprintf oc "	movw	%d(%a), %a\n" ofs ireg src ireg16 tmp;
@@ -293,14 +298,39 @@ let print_builtin_memcpy oc sz al args =
       fprintf oc "	movb	%a, %d(%a)\n" ireg8 tmp ofs ireg dst;
       copy (ofs + 1) (sz - 1)
     end in
-  fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n"
-          comment sz al;
-  if tmp = EAX && sz mod 4 <> 0 then
-    fprintf oc "	movd	%a, %a\n" ireg EAX freg XMM7;
+  if need_tmp && tmp = EAX then
+    fprintf oc "	pushl	%a\n" ireg EAX;
   copy 0 sz;
-  if tmp = EAX && sz mod 4 <> 0 then
-    fprintf oc "	movd	%a, %a\n" freg XMM7 ireg EAX;
-  fprintf oc "%s end builtin __builtin_memcpy\n" comment
+  if need_tmp && tmp = EAX then
+    fprintf oc "	popl	%a\n" ireg EAX
+
+let print_builtin_memcpy_big oc sz al src dst =
+  fprintf oc "	pushl	%a\n" ireg ESI;
+  fprintf oc "	pushl	%a\n" ireg EDI;
+  begin match src, dst with
+  | ESI, EDI -> ()
+  | EDI, ESI -> fprintf oc "	xchgl	%a, %a\n" ireg ESI ireg EDI
+  | ESI, _   -> fprintf oc "	movl	%a, %a\n" ireg dst ireg EDI
+  | _,   EDI -> fprintf oc "	movl	%a, %a\n" ireg src ireg ESI
+  | _,   _   -> fprintf oc "	movl	%a, %a\n" ireg src ireg ESI;
+                fprintf oc "	movl	%a, %a\n" ireg dst ireg EDI
+  end;
+  fprintf oc "	movl	$%d, %a\n" (sz / 4) ireg ECX;
+  fprintf oc "	rep	movsl\n";
+  if sz mod 4 >= 2 then fprintf oc "	movsw\n";
+  if sz mod 2 >= 1 then fprintf oc "	movsb\n";
+  fprintf oc "	popl	%a\n" ireg EDI;
+  fprintf oc "	popl	%a\n" ireg ESI
+
+let print_builtin_memcpy oc sz al args =
+  let (dst, src) =
+    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
+  fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n"
+          comment sz al;
+  if sz <= 64
+  then print_builtin_memcpy_small oc sz al src dst
+  else print_builtin_memcpy_big oc sz al src dst;
+  fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment
 
 (* Handling of volatile reads and writes *)
 
@@ -414,47 +444,6 @@ let print_builtin_inline oc name args res =
   end;
   fprintf oc "%s end builtin %s\n" comment name
 
-(* Handling of other builtins *)
-
-let re_builtin_function = Str.regexp "__builtin_"
-
-let is_builtin_function s =
-  Str.string_match re_builtin_function (extern_atom s) 0
-
-let print_memcpy oc sz =
-  fprintf oc "	movl	%%esi, %%eax\n";     (* Preserve esi, edi *)
-  fprintf oc "	movl	%%edi, %%edx\n";
-  fprintf oc "	movl	0(%%esp), %%edi\n";  (* Load args *)
-  fprintf oc "	movl	4(%%esp), %%esi\n";
-  fprintf oc "	movl	8(%%esp), %%ecx\n";
-  fprintf oc "	shr	$2, %%ecx\n";
-  fprintf oc "	rep movsl\n";                (* Copy by words *)
-  if sz < 4 then begin
-    fprintf oc "	movl	8(%%esp), %%ecx\n";
-    fprintf oc "	andl	$3, %%ecx\n";
-    fprintf oc "	rep movsb\n"         (* Finish copy by bytes *)
-  end;
-  fprintf oc "	movl	%%eax, %%esi\n";     (* Restore esi, edi *)
-  fprintf oc "	movl	%%edx, %%edi\n"
-
-let print_builtin_function oc s =
-  fprintf oc "%s begin builtin function %s\n" comment (extern_atom s);
-  (* arguments: on stack, starting at offset 0 *)
-  (* result: EAX or ST0 *)
-  begin match extern_atom s with
-  (* Block copy *)
-  | "__builtin_memcpy" ->
-      print_memcpy oc 1
-  | "__builtin_memcpy_al2" ->
-      print_memcpy oc 2
-  | "__builtin_memcpy_al4" | "__builtin_memcpy_al8" ->
-      print_memcpy oc 4
-  (* Catch-all *)
-  | s ->
-      invalid_arg ("unrecognized builtin function " ^ s)
-  end;
-  fprintf oc "%s end builtin function %s\n" comment (extern_atom s)
-
 (* Printing of instructions *)
 
 let float_literals : (int * int64) list ref = ref []
@@ -631,12 +620,7 @@ let print_instruction oc = function
   | Pjmp_l(l) ->
       fprintf oc "	jmp	%a\n" label (transl_label l)
   | Pjmp_s(f) ->
-      if not (is_builtin_function f) then
-        fprintf oc "	jmp	%a\n" symbol f
-      else begin
-        print_builtin_function oc f;
-        fprintf oc "	ret\n"
-      end
+      fprintf oc "	jmp	%a\n" symbol f
   | Pjmp_r(r) ->
       fprintf oc "	jmp	*%a\n" ireg r
   | Pjcc(c, l) ->
@@ -658,10 +642,7 @@ let print_instruction oc = function
       fprintf oc "	jmp	*%a(, %a, 4)\n" label l ireg r;
       jumptables := (l, tbl) :: !jumptables
   | Pcall_s(f) ->
-      if not (is_builtin_function f) then
-        fprintf oc "	call	%a\n" symbol f
-      else
-        print_builtin_function oc f
+      fprintf oc "	call	%a\n" symbol f
   | Pcall_r(r) ->
       fprintf oc "	call	*%a\n" ireg r
   | Pret ->
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index efe5b98..0567f3f 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -316,14 +316,12 @@ let print_annot_val oc txt args res =
 (* On the PowerPC, unaligned accesses to 16- and 32-bit integers are
    fast, but unaligned accesses to 64-bit floats can be slow
    (not so much on G5, but clearly so on Power7).
-   So, use 64-bit accesses only if alignment >= 8.
+   So, use 64-bit accesses only if alignment >= 4.
    Note that lfd and stfd cannot trap on ill-formed floats. *)
 
-let print_builtin_memcpy oc sz al args =
-  let (dst, src) =
-    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
+let print_builtin_memcpy_small oc sz al src dst =
   let rec copy ofs sz =
-    if sz >= 8 && al >= 8 then begin
+    if sz >= 8 && al >= 4 then begin
       fprintf oc "	lfd	%a, %d(%a)\n" freg FPR0 ofs ireg src;
       fprintf oc "	stfd	%a, %d(%a)\n" freg FPR0 ofs ireg dst;
       copy (ofs + 8) (sz - 8)
@@ -340,10 +338,40 @@ let print_builtin_memcpy oc sz al args =
       fprintf oc "	stb	%a, %d(%a)\n" ireg GPR0 ofs ireg dst;
       copy (ofs + 1) (sz - 1)
     end in
-  fprintf oc "%s begin builtin __builtin_memcpy, size = %d, alignment = %d\n"
+  copy 0 sz
+
+let print_builtin_memcpy_big oc sz al src dst =
+  assert (sz >= 4);
+  fprintf oc "	li	%a, %d\n" ireg GPR0 (sz / 4);
+  fprintf oc "	mtctr	%a\n" ireg GPR0;
+  let (s,d) = if dst <> GPR11 then (GPR11, GPR12) else (GPR12, GPR11) in
+  fprintf oc "	addi	%a, %a, -4\n" ireg s ireg src;
+  fprintf oc "	addi	%a, %a, -4\n" ireg d ireg dst;
+  let lbl = new_label() in
+  fprintf oc "%a:	lwzu	%a, 4(%a)\n" ireg GPR0 ireg s;
+  fprintf oc "	stwu	%a, 4(%a)\n" ireg GPR0 ireg d;
+  fprintf oc "	bdnz	%a\n" label lbl;
+  (* s and d lag behind by 4 bytes *)
+  match sz land 3 with
+  | 1 -> fprintf oc "	lbz	%a, 4(%a)\n" ireg GPR0 ireg s;
+         fprintf oc "	stb	%a, 4(%a)\n" ireg GPR0 ireg d
+  | 2 -> fprintf oc "	lhz	%a, 4(%a)\n" ireg GPR0 ireg s;
+         fprintf oc "	sth	%a, 4(%a)\n" ireg GPR0 ireg d
+  | 3 -> fprintf oc "	lhz	%a, 4(%a)\n" ireg GPR0 ireg s;
+         fprintf oc "	sth	%a, 4(%a)\n" ireg GPR0 ireg d;
+         fprintf oc "	lbz	%a, 6(%a)\n" ireg GPR0 ireg s;
+         fprintf oc "	stb	%a, 6(%a)\n" ireg GPR0 ireg d
+  | _ -> ()
+
+let print_builtin_memcpy oc sz al args =
+  let (dst, src) =
+    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
+  fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n"
           comment sz al;
-  copy 0 sz;
-  fprintf oc "%s end builtin __builtin_memcpy\n" comment
+  if sz <= 64
+  then print_builtin_memcpy_small oc sz al src dst
+  else print_builtin_memcpy_big oc sz al src dst;
+  fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment
 
 (* Handling of volatile reads and writes *)
 
@@ -441,61 +469,6 @@ let print_builtin_inline oc name args res =
   end;
   fprintf oc "%s end builtin %s\n" comment name
 
-(* Handling of other builtins *)
-
-let re_builtin_function = Str.regexp "__builtin_"
-
-let is_builtin_function s =
-  Str.string_match re_builtin_function (extern_atom s) 0
-
-let print_memcpy oc sz prepare load store =
-  let lbl1 = new_label() in
-  let lbl2 = new_label() in
-  prepare GPR5;
-  fprintf oc "	beq     %a, %a\n" creg 0 label lbl1;
-  fprintf oc "	mtctr   %a\n" ireg GPR5;
-  fprintf oc "	addi    %a, %a, -%d\n" ireg GPR3 ireg GPR3 sz;
-  fprintf oc "	addi    %a, %a, -%d\n" ireg GPR4 ireg GPR4 sz;
-  fprintf oc "%a:\n" label lbl2;
-  load GPR4;
-  store GPR3;
-  fprintf oc "	bdnz    %a\n" label lbl2;
-  fprintf oc "%a:\n" label lbl1
-
-let print_builtin_function oc s =
-  fprintf oc "%s begin builtin function %s\n" comment (extern_atom s);
-  (* int args: GPR3, GPR4, GPR5     float args: FPR1, FPR2, FPR3
-     int res:  GPR3                 float res:  FPR1
-     Watch out for MacOSX/EABI incompatibility: functions that take
-     some floats then some ints.  There are none here. *)
-  (* Block copy *)
-  begin match extern_atom s with
-  | "__builtin_memcpy" ->
-      print_memcpy oc 1
-        (fun r -> fprintf oc "	cmplwi	%a, %a, 0\n" creg 0 ireg r)
-        (fun r -> fprintf oc "	lbzu    %a, 1(%a)\n" ireg GPR0 ireg r)
-        (fun r -> fprintf oc "	stbu    %a, 1(%a)\n" ireg GPR0 ireg r)
-  | "__builtin_memcpy_al2" ->
-      print_memcpy oc 2
-        (fun r -> fprintf oc "	rlwinm.	%a, %a, 31, 1, 31\n" ireg r ireg r)
-        (fun r -> fprintf oc "	lhzu    %a, 2(%a)\n" ireg GPR0 ireg r)
-        (fun r -> fprintf oc "	sthu    %a, 2(%a)\n" ireg GPR0 ireg r)
-  | "__builtin_memcpy_al4" ->
-      print_memcpy oc 4
-        (fun r -> fprintf oc "	rlwinm.	%a, %a, 30, 2, 31\n" ireg r ireg r)
-        (fun r -> fprintf oc "	lwzu    %a, 4(%a)\n" ireg GPR0 ireg r)
-        (fun r -> fprintf oc "	stwu    %a, 4(%a)\n" ireg GPR0 ireg r)
-  | "__builtin_memcpy_al8" ->
-      print_memcpy oc 8
-        (fun r -> fprintf oc "	rlwinm.	%a, %a, 29, 3, 31\n" ireg r ireg r)
-        (fun r -> fprintf oc "	lfdu    %a, 8(%a)\n" freg FPR0 ireg r)
-        (fun r -> fprintf oc "	stfdu   %a, 8(%a)\n" freg FPR0 ireg r)
-  (* Catch-all *)
-  | s ->
-      invalid_arg ("unrecognized builtin function " ^ s)
-  end;
-  fprintf oc "%s end builtin function %s\n" comment (extern_atom s)
-
 (* Printing of instructions *)
 
 let float_literals : (int * int64) list ref = ref []
@@ -543,17 +516,9 @@ let print_instruction oc = function
   | Pbf(bit, lbl) ->
       fprintf oc "	bf	%a, %a\n" crbit bit label (transl_label lbl)
   | Pbl s ->
-      if not (is_builtin_function s) then
-        fprintf oc "	bl	%a\n" symbol s
-      else
-        print_builtin_function oc s
+      fprintf oc "	bl	%a\n" symbol s
   | Pbs s ->
-      if not (is_builtin_function s) then
-        fprintf oc "	b	%a\n" symbol s
-      else begin
-        print_builtin_function oc s;
-        fprintf oc "	blr\n"
-      end
+      fprintf oc "	b	%a\n" symbol s
   | Pblr ->
       fprintf oc "	blr\n"
   | Pbt(bit, lbl) ->
@@ -955,15 +920,18 @@ let print_fundef oc (Coq_pair(name, defn)) =
   match defn with
   | Internal code ->
       print_function oc name code
-  | External ef ->
-      if not (is_builtin_function name) then stub_function oc name (ef_sig ef)
+  | External (EF_external _ as ef) ->
+      if function_needs_stub name then stub_function oc name (ef_sig ef)
+  | External _ ->
+      ()
 
 let record_extfun (Coq_pair(name, defn)) =
   match defn with
   | Internal _ -> ()
-  | External _ ->
-      if function_needs_stub name && not (is_builtin_function name) then
+  | External (EF_external _) ->
+      if function_needs_stub name then
         stubbed_functions := IdentSet.add name !stubbed_functions
+  | External _ -> ()
 
 let print_init oc = function
   | Init_int8 n ->
diff --git a/test/regression/expr1.c b/test/regression/expr1.c
index 132ce44..10c9ea6 100644
--- a/test/regression/expr1.c
+++ b/test/regression/expr1.c
@@ -7,7 +7,7 @@ struct list * f(struct list ** p)
   return ((*p)->tl = 0);
 }
 
-int main(int argc, char ** argv)
+int main()
 {
   struct list l;
   l.tl = &l;
diff --git a/test/regression/initializers.c b/test/regression/initializers.c
index 7384091..c16a356 100644
--- a/test/regression/initializers.c
+++ b/test/regression/initializers.c
@@ -46,7 +46,7 @@ char * x18 = "Hello!";
 
 char * x19[2] = { "Hello", "world!" };
 
-int main(int argc, char ** argv)
+int main()
 {
   int i;
 
diff --git a/test/regression/volatile2.c b/test/regression/volatile2.c
index d83927b..0608650 100644
--- a/test/regression/volatile2.c
+++ b/test/regression/volatile2.c
@@ -8,7 +8,7 @@
   *((ty *) &x) = v2;                                               \
   printf("%s 2: %s\n", msg, *((volatile ty *) &x) == v2 ? "OK" : "FAILED");
 
-int main(int argc, char ** argv)
+int main()
 {
   signed char sc;
   unsigned char uc;