From 993491f7e482f5c7ce87ffb59a5e4ce074950dd4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gerg=C3=B6=20Barany?= <gergo.barany@inria.fr>
Date: Tue, 25 Jul 2017 11:26:54 +0200
Subject: [PATCH 1/5] Add LTLtyping and enforce well-typed LTL in Allocation

---
 Makefile             |   3 +-
 backend/Allocation.v |   8 +-
 backend/Allocproof.v |   1 +
 backend/LTLtyping.v  | 389 +++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 398 insertions(+), 3 deletions(-)
 create mode 100644 backend/LTLtyping.v

diff --git a/Makefile b/Makefile
index e96cb5e3ce..769840062b 100644
--- a/Makefile
+++ b/Makefile
@@ -86,7 +86,8 @@ BACKEND=\
   CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \
   NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \
   Unusedglob.v Unusedglobproof.v \
-  Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \
+  Machregs.v Locations.v Conventions1.v Conventions.v \
+  LTL.v LTLtyping.v \
   Allocation.v Allocproof.v \
   Tunneling.v Tunnelingproof.v \
   Linear.v Lineartyping.v \
diff --git a/backend/Allocation.v b/backend/Allocation.v
index cf62295dde..e60634cef1 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -16,7 +16,7 @@ Require Import FSets FSetAVLplus.
 Require Import Coqlib Ordered Maps Errors Integers Floats.
 Require Import AST Lattice Kildall Memdata.
 Require Archi.
-Require Import Op Registers RTL Locations Conventions RTLtyping LTL.
+Require Import Op Registers RTL Locations Conventions RTLtyping LTL LTLtyping.
 
 (** The validation algorithm used here is described in
   "Validating register allocation and spilling",
@@ -1359,7 +1359,11 @@ Definition transf_function (f: RTL.function) : res LTL.function :=
   | OK env =>
       match regalloc f with
       | Error m => Error m
-      | OK tf => do x <- check_function f tf env; OK tf
+      | OK tf =>
+          if wt_function tf then
+            do x <- check_function f tf env; OK tf
+          else
+            Error (msg "Ill-typed LTL code")
       end
   end.
 
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 4b75e34d4e..4996682bae 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1754,6 +1754,7 @@ Proof.
   unfold transf_function; intros.
   destruct (type_function f) as [env|] eqn:TY; try discriminate.
   destruct (regalloc f); try discriminate.
+  destruct (LTLtyping.wt_function f0); try discriminate.
   destruct (check_function f f0 env) as [] eqn:?; inv H.
   unfold check_function in Heqr.
   destruct (analyze f env (pair_codes f tf)) as [an|] eqn:?; try discriminate.
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
new file mode 100644
index 0000000000..62aa09e259
--- /dev/null
+++ b/backend/LTLtyping.v
@@ -0,0 +1,389 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Type-checking LTL code, adapted with tiny changes from [Lineartyping]. *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Values.
+Require Import Globalenvs.
+Require Import Memory.
+Require Import Events.
+Require Import Op.
+Require Import Machregs.
+Require Import Locations.
+Require Import Conventions.
+Require Import LTL.
+
+(** The rules are presented as boolean-valued functions so that we
+  get an executable type-checker for free. *)
+
+Section WT_INSTR.
+
+Variable funct: function.
+
+Definition slot_valid (sl: slot) (ofs: Z) (ty: typ): bool :=
+  match sl with
+  | Local => zle 0 ofs
+  | Outgoing => zle 0 ofs
+  | Incoming => In_dec Loc.eq (S Incoming ofs ty) (regs_of_rpairs (loc_parameters funct.(fn_sig)))
+  end
+  && Zdivide_dec (typealign ty) ofs (typealign_pos ty).
+
+Definition slot_writable (sl: slot) : bool :=
+  match sl with
+  | Local => true
+  | Outgoing => true
+  | Incoming => false
+  end.
+
+Definition loc_valid (l: loc) : bool :=
+  match l with
+  | R r => true
+  | S Local ofs ty => slot_valid Local ofs ty
+  | S _ _ _ => false
+  end.
+
+Fixpoint wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool :=
+  match res with
+  | BR r => subtype ty (mreg_type r)
+  | BR_none => true
+  | BR_splitlong hi lo => wt_builtin_res Tint hi && wt_builtin_res Tint lo
+  end.
+
+Definition wt_instr (i: instruction) : bool :=
+  match i with
+  | Lgetstack sl ofs ty r =>
+      subtype ty (mreg_type r) && slot_valid sl ofs ty
+  | Lsetstack r sl ofs ty =>
+      slot_valid sl ofs ty && slot_writable sl
+  | Lop op args res =>
+      match is_move_operation op args with
+      | Some arg =>
+          subtype (mreg_type arg) (mreg_type res)
+      | None =>
+          let (targs, tres) := type_of_operation op in
+          subtype tres (mreg_type res)
+      end
+  | Lload chunk addr args dst =>
+      subtype (type_of_chunk chunk) (mreg_type dst)
+  | Ltailcall sg ros =>
+      zeq (size_arguments sg) 0
+  | Lbuiltin ef args res =>
+      wt_builtin_res (proj_sig_res (ef_sig ef)) res
+      && forallb loc_valid (params_of_builtin_args args)
+  | _ =>
+      true
+  end.
+
+End WT_INSTR.
+
+Definition wt_bblock (f: function) (b: bblock) : bool :=
+  forallb (wt_instr f) b.
+
+Definition wt_function (f: function) : bool :=
+  let bs := map snd (Maps.PTree.elements f.(fn_code)) in
+  forallb (wt_bblock f) bs.
+
+(** Typing the run-time state. *)
+
+Definition wt_locset (ls: locset) : Prop :=
+  forall l, Val.has_type (ls l) (Loc.type l).
+
+Lemma wt_setreg:
+  forall ls r v,
+  Val.has_type v (mreg_type r) -> wt_locset ls -> wt_locset (Locmap.set (R r) v ls).
+Proof.
+  intros; red; intros.
+  unfold Locmap.set.
+  destruct (Loc.eq (R r) l).
+  subst l; auto.
+  destruct (Loc.diff_dec (R r) l). auto. red. auto.
+Qed.
+
+Lemma wt_setstack:
+  forall ls sl ofs ty v,
+  wt_locset ls -> wt_locset (Locmap.set (S sl ofs ty) v ls).
+Proof.
+  intros; red; intros.
+  unfold Locmap.set.
+  destruct (Loc.eq (S sl ofs ty) l).
+  subst l. simpl.
+  generalize (Val.load_result_type (chunk_of_type ty) v).
+  replace (type_of_chunk (chunk_of_type ty)) with ty. auto.
+  destruct ty; reflexivity.
+  destruct (Loc.diff_dec (S sl ofs ty) l). auto. red. auto.
+Qed.
+
+Lemma wt_undef_regs:
+  forall rs ls, wt_locset ls -> wt_locset (undef_regs rs ls).
+Proof.
+  induction rs; simpl; intros. auto. apply wt_setreg; auto. red; auto.
+Qed.
+
+Lemma wt_call_regs:
+  forall ls, wt_locset ls -> wt_locset (call_regs ls).
+Proof.
+  intros; red; intros. unfold call_regs. destruct l. auto.
+  destruct sl.
+  red; auto.
+  change (Loc.type (S Incoming pos ty)) with (Loc.type (S Outgoing pos ty)). auto.
+  red; auto.
+Qed.
+
+Lemma wt_return_regs:
+  forall caller callee,
+  wt_locset caller -> wt_locset callee -> wt_locset (return_regs caller callee).
+Proof.
+  intros; red; intros.
+  unfold return_regs. destruct l; auto. destruct (is_callee_save r); auto.
+Qed.
+
+Lemma wt_init:
+  wt_locset (Locmap.init Vundef).
+Proof.
+  red; intros. unfold Locmap.init. red; auto.
+Qed.
+
+Lemma wt_setpair:
+  forall sg v rs,
+  Val.has_type v (proj_sig_res sg) ->
+  wt_locset rs ->
+  wt_locset (Locmap.setpair (loc_result sg) v rs).
+Proof.
+  intros. generalize (loc_result_pair sg) (loc_result_type sg).
+  destruct (loc_result sg); simpl Locmap.setpair.
+- intros. apply wt_setreg; auto. eapply Val.has_subtype; eauto.
+- intros A B. decompose [and] A.
+  apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I.
+  apply wt_setreg. eapply Val.has_subtype; eauto. destruct v; exact I.
+  auto.
+Qed.
+
+Lemma wt_setres:
+  forall res ty v rs,
+  wt_builtin_res ty res = true ->
+  Val.has_type v ty ->
+  wt_locset rs ->
+  wt_locset (Locmap.setres res v rs).
+Proof.
+  induction res; simpl; intros.
+- apply wt_setreg; auto. eapply Val.has_subtype; eauto.
+- auto.
+- InvBooleans. eapply IHres2; eauto. destruct v; exact I.
+  eapply IHres1; eauto. destruct v; exact I.
+Qed.
+
+(** Soundness of the type system *)
+
+Definition wt_fundef (fd: fundef) :=
+  match fd with
+  | Internal f => wt_function f = true
+  | External ef => True
+  end.
+
+Inductive wt_callstack: list stackframe -> Prop :=
+  | wt_callstack_nil:
+      wt_callstack nil
+  | wt_callstack_cons: forall f sp rs b s
+        (WTSTK: wt_callstack s)
+        (WTF: wt_function f = true)
+        (WTB: wt_bblock f b = true)
+        (WTRS: wt_locset rs),
+      wt_callstack (Stackframe f sp rs b :: s).
+
+Lemma wt_parent_locset:
+  forall s, wt_callstack s -> wt_locset (parent_locset s).
+Proof.
+  induction 1; simpl.
+- apply wt_init.
+- auto.
+Qed.
+
+Inductive wt_state: state -> Prop :=
+  | wt_branch_state: forall s f sp n rs m
+        (WTSTK: wt_callstack s )
+        (WTF: wt_function f = true)
+        (WTRS: wt_locset rs),
+      wt_state (State s f sp n rs m)
+  | wt_regular_state: forall s f sp b rs m
+        (WTSTK: wt_callstack s )
+        (WTF: wt_function f = true)
+        (WTB: wt_bblock f b = true)
+        (WTRS: wt_locset rs),
+      wt_state (Block s f sp b rs m)
+  | wt_call_state: forall s fd rs m
+        (WTSTK: wt_callstack s)
+        (WTFD: wt_fundef fd)
+        (WTRS: wt_locset rs),
+      wt_state (Callstate s fd rs m)
+  | wt_return_state: forall s rs m
+        (WTSTK: wt_callstack s)
+        (WTRS: wt_locset rs),
+      wt_state (Returnstate s rs m).
+
+(** Preservation of state typing by transitions *)
+
+Section SOUNDNESS.
+
+Variable prog: program.
+Let ge := Genv.globalenv prog.
+
+Hypothesis wt_prog:
+  forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd.
+
+Lemma wt_find_function:
+  forall ros rs f, find_function ge ros rs = Some f -> wt_fundef f.
+Proof.
+  intros.
+  assert (X: exists i, In (i, Gfun f) prog.(prog_defs)).
+  {
+    destruct ros as [r | s]; simpl in H.
+    eapply Genv.find_funct_inversion; eauto.
+    destruct (Genv.find_symbol ge s) as [b|]; try discriminate.
+    eapply Genv.find_funct_ptr_inversion; eauto.
+  }
+  destruct X as [i IN]. eapply wt_prog; eauto.
+Qed.
+
+Theorem step_type_preservation:
+  forall S1 t S2, step ge S1 t S2 -> wt_state S1 -> wt_state S2.
+Proof.
+Local Opaque mreg_type.
+  induction 1; intros WTS; inv WTS.
+- (* startblock *)
+  econstructor; eauto.
+  apply Maps.PTree.elements_correct in H.
+  unfold wt_function in WTF. eapply forallb_forall in WTF; eauto.
+  change bb with (snd (pc, bb)). apply in_map; auto.
+- (* op *)
+  simpl in *. destruct (is_move_operation op args) as [src | ] eqn:ISMOVE.
+  + (* move *)
+    InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst.
+    simpl in H. inv H.
+    econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. apply WTRS.
+    apply wt_undef_regs; auto.
+  + (* other ops *)
+    destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans.
+    econstructor; eauto.
+    apply wt_setreg; auto. eapply Val.has_subtype; eauto.
+    change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto.
+    red; intros; subst op. simpl in ISMOVE.
+    destruct args; try discriminate. destruct args; discriminate.
+    apply wt_undef_regs; auto.
+- (* load *)
+  simpl in *; InvBooleans.
+  econstructor; eauto.
+  apply wt_setreg. eapply Val.has_subtype; eauto.
+  destruct a; simpl in H0; try discriminate. eapply Mem.load_type; eauto.
+  apply wt_undef_regs; auto.
+- (* getstack *)
+  simpl in *; InvBooleans.
+  econstructor; eauto.
+  eapply wt_setreg; eauto. eapply Val.has_subtype; eauto. apply WTRS.
+  apply wt_undef_regs; auto.
+- (* setstack *)
+  simpl in *; InvBooleans.
+  econstructor; eauto.
+  apply wt_setstack. apply wt_undef_regs; auto.
+- (* store *)
+  simpl in *; InvBooleans.
+  econstructor. eauto. eauto. eauto.
+  apply wt_undef_regs; auto.
+- (* call *)
+  simpl in *; InvBooleans.
+  econstructor; eauto. econstructor; eauto.
+  eapply wt_find_function; eauto.
+- (* tailcall *)
+  simpl in *; InvBooleans.
+  econstructor; eauto.
+  eapply wt_find_function; eauto.
+  apply wt_return_regs; auto. apply wt_parent_locset; auto.
+- (* builtin *)
+  simpl in *; InvBooleans.
+  econstructor; eauto.
+  eapply wt_setres; eauto. eapply external_call_well_typed; eauto.
+  apply wt_undef_regs; auto.
+- (* branch *)
+  simpl in *. econstructor; eauto.
+- (* cond branch *)
+  simpl in *. econstructor; auto.
+- (* jumptable *)
+  simpl in *. econstructor; auto.
+- (* return *)
+  simpl in *. InvBooleans.
+  econstructor; eauto.
+  apply wt_return_regs; auto. apply wt_parent_locset; auto.
+- (* internal function *)
+  simpl in WTFD.
+  econstructor. eauto. eauto. eauto.
+  apply wt_undef_regs. apply wt_call_regs. auto.
+- (* external function *)
+  econstructor. auto. apply wt_setpair; auto.
+  eapply external_call_well_typed; eauto.
+- (* return *)
+  inv WTSTK. econstructor; eauto.
+Qed.
+
+Theorem wt_initial_state:
+  forall S, initial_state prog S -> wt_state S.
+Proof.
+  induction 1. econstructor. constructor.
+  unfold ge0 in H1. exploit Genv.find_funct_ptr_inversion; eauto.
+  intros [id IN]. eapply wt_prog; eauto.
+  apply wt_init.
+Qed.
+
+End SOUNDNESS.
+
+(** Properties of well-typed states that are used in [Allocproof]. *)
+
+Lemma wt_state_getstack:
+  forall s f sp sl ofs ty rd c rs m,
+  wt_state (Block s f sp (Lgetstack sl ofs ty rd :: c) rs m) ->
+  slot_valid f sl ofs ty = true.
+Proof.
+  intros. inv H. simpl in WTB; InvBooleans. auto.
+Qed.
+
+Lemma wt_state_setstack:
+  forall s f sp sl ofs ty r c rs m,
+  wt_state (Block s f sp (Lsetstack r sl ofs ty :: c) rs m) ->
+  slot_valid f sl ofs ty = true /\ slot_writable sl = true.
+Proof.
+  intros. inv H. simpl in WTB; InvBooleans. intuition.
+Qed.
+
+Lemma wt_state_tailcall:
+  forall s f sp sg ros c rs m,
+  wt_state (Block s f sp (Ltailcall sg ros :: c) rs m) ->
+  size_arguments sg = 0.
+Proof.
+  intros. inv H. simpl in WTB; InvBooleans. auto.
+Qed.
+
+Lemma wt_state_builtin:
+  forall s f sp ef args res c rs m,
+  wt_state (Block s f sp (Lbuiltin ef args res :: c) rs m) ->
+  forallb (loc_valid f) (params_of_builtin_args args) = true.
+Proof.
+  intros. inv H. simpl in WTB; InvBooleans. auto.
+Qed.
+
+Lemma wt_callstate_wt_regs:
+  forall s f rs m,
+  wt_state (Callstate s f rs m) ->
+  forall r, Val.has_type (rs (R r)) (mreg_type r).
+Proof.
+  intros. inv H. apply WTRS.
+Qed.

From bb9c9881999b674dc0b03a8d67082f3a0feda2bf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gerg=C3=B6=20Barany?= <gergo.barany@inria.fr>
Date: Mon, 21 Aug 2017 11:45:11 +0200
Subject: [PATCH 2/5] Make builtin_res type nonrecursive

The BR_splitlong constructor used to be recursive, meaning that a long
result could in theory be split into an arbitrary tree of atomic parts. But
we only ever split longs into exactly two ints, so this generality was not
needed. This simplification will help with the LTL typing proof.
---
 arm/Asm.v               |  4 ++--
 arm/Asmexpand.ml        | 10 +++++-----
 backend/Allocation.v    |  2 +-
 backend/Allocproof.v    | 17 ++++++++++-------
 backend/Asmgenproof0.v  | 13 +++++++++----
 backend/Debugvar.v      |  4 ++--
 backend/LTLtyping.v     | 11 +++++++----
 backend/Lineartyping.v  | 11 +++++++----
 backend/Locations.v     |  4 ++--
 backend/Mach.v          |  4 ++--
 backend/PrintAsmaux.ml  |  2 +-
 backend/Regalloc.ml     | 35 ++++++++++++++++++++---------------
 backend/Stackingproof.v |  4 ++--
 backend/XTL.ml          |  4 ++--
 common/AST.v            | 11 +++++------
 common/PrintAST.ml      |  6 ++----
 powerpc/Asm.v           |  4 ++--
 powerpc/Asmexpand.ml    | 10 +++++-----
 riscV/Asm.v             |  4 ++--
 riscV/Asmexpand.ml      | 12 ++++++------
 x86/Asm.v               |  4 ++--
 x86/Asmexpand.ml        | 12 ++++++------
 22 files changed, 102 insertions(+), 86 deletions(-)

diff --git a/arm/Asm.v b/arm/Asm.v
index 85eb94c18e..1b32bd1a3e 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -323,11 +323,11 @@ Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
 
 (** Assigning the result of a builtin *)
 
-Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
+Definition set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   match res with
   | BR r => rs#r <- v
   | BR_none => rs
-  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+  | BR_splitlong hi lo => rs #hi <- (Val.hiword v) #lo <- (Val.loword v)
   end.
 
 Section RELSEM.
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 04b4152d04..3054b2d0be 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -188,7 +188,7 @@ let expand_builtin_vload_common chunk base ofs res =
      emit (Pldrsh (res, base, SOimm ofs))
   | Mint32, BR(IR res) ->
      emit (Pldr (res, base, SOimm ofs))
-  | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) ->
+  | Mint64, BR_splitlong(IR res1, IR res2) ->
      let ofs_hi = if Archi.big_endian then ofs else Int.add ofs _4 in
      let ofs_lo = if Archi.big_endian then Int.add ofs _4 else ofs in
      if base <> res2 then begin
@@ -351,7 +351,7 @@ let expand_builtin_inline name args res =
      emit (Pfsqrt (res,a1))
   (* 64-bit integer arithmetic *)
   | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
       expand_int64_arith (rl = ah ) rl (fun rl ->
         emit (Prsbs (rl,al,SOimm _0));
         (* No "rsc" instruction in Thumb2.  Emulate based on
@@ -365,20 +365,20 @@ let expand_builtin_inline name args res =
         end)
   | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al));
                        BA_splitlong(BA(IR bh), BA(IR bl))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      expand_int64_arith (rl = ah || rl = bh) rl
 			(fun rl ->
 			 emit (Padds (rl,al,SOreg bl));
 			 emit (Padc (rh,ah,SOreg bh)))
   | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al));
                        BA_splitlong(BA(IR bh), BA(IR bl))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      expand_int64_arith (rl = ah || rl = bh) rl
 		       (fun rl ->
 			emit (Psubs (rl,al,SOreg bl));
 			emit (Psbc (rh,ah,SOreg bh)))
   | "__builtin_mull", [BA(IR a); BA(IR b)],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      emit (Pumull (rl,rh,a,b))
   (* Memory accesses *)
   | "__builtin_read16_reversed", [BA(IR a1)], BR(IR res) ->
diff --git a/backend/Allocation.v b/backend/Allocation.v
index e60634cef1..d8775f643e 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -847,7 +847,7 @@ Definition remove_equations_builtin_res
     (env: regenv) (res: builtin_res reg) (res': builtin_res mreg) (e: eqs) : option eqs :=
   match res, res' with
   | BR r, BR r' => Some (remove_equation (Eq Full r (R r')) e)
-  | BR r, BR_splitlong (BR rhi) (BR rlo) =>
+  | BR r, BR_splitlong rhi rlo =>
       assertion (typ_eq (env r) Tlong);
       if mreg_eq rhi rlo then None else
         Some (remove_equation (Eq Low r (R rlo))
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 4996682bae..6901f9cd0d 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1681,22 +1681,25 @@ Proof.
   destruct res, res'; simpl in *; inv H.
 - apply parallel_assignment_satisf with (k := Full); auto.
   unfold reg_loc_unconstrained. rewrite H0 by auto. rewrite H1 by auto. auto.
-- destruct res'1; try discriminate. destruct res'2; try discriminate.
-  rename x0 into hi; rename x1 into lo. MonadInv. destruct (mreg_eq hi lo); inv H5.
-  set (e' := remove_equation {| ekind := High; ereg := x; eloc := R hi |} e0) in *.
+- set (e' := remove_equation {| ekind := High; ereg := x; eloc := R hi |} e0) in *.
   set (e'' := remove_equation {| ekind := Low; ereg := x; eloc := R lo |} e') in *.
   simpl in *. red; intros.
+  assert (lo <> hi /\ e'' = e1).
+  { destruct (typ_eq (env x) Tlong), (mreg_eq hi lo); try inversion H5. auto. }
+  destruct H4; subst.
   destruct (OrderedEquation.eq_dec q (Eq Low x (R lo))).
   subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss. apply Val.loword_lessdef; auto.
   destruct (OrderedEquation.eq_dec q (Eq High x (R hi))).
-  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by (red; auto).
+  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by (red; tauto).
   rewrite Locmap.gss. apply Val.hiword_lessdef; auto.
-  assert (EqSet.In q e'').
-  { unfold e'', e', remove_equation; simpl; ESD.fsetdec. }
-  rewrite Regmap.gso. rewrite ! Locmap.gso. auto.
+  rewrite Regmap.gso. rewrite ! Locmap.gso. auto. apply H2.
+  repeat apply ESF.remove_neq_iff; auto.
   eapply loc_unconstrained_sound; eauto.
+  repeat apply ESF.remove_neq_iff; auto.
   eapply loc_unconstrained_sound; eauto.
+  repeat apply ESF.remove_neq_iff; auto.
   eapply reg_unconstrained_sound; eauto.
+  repeat apply ESF.remove_neq_iff; auto.
 - auto.
 Qed.
 
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index f6f03868ce..12839f8c4b 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -416,9 +416,12 @@ Proof.
 - eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto.
   intros. apply Pregmap.gso; auto.
 - auto.
-- apply IHres2. apply IHres1. auto.
-  apply Val.hiword_lessdef; auto.
-  apply Val.loword_lessdef; auto.
+- apply agree_set_mreg with (rs := rs # (preg_of hi) <- (Val.hiword v')).
+  apply agree_set_mreg with (rs := rs).
+  auto. rewrite Pregmap.gss; auto using Val.hiword_lessdef.
+  intros. apply Pregmap.gso; auto.
+  rewrite Pregmap.gss. auto using Val.loword_lessdef.
+  intros. apply Pregmap.gso; auto.
 Qed.
 
 Lemma set_res_other:
@@ -429,7 +432,9 @@ Proof.
   induction res; simpl; intros.
 - apply Pregmap.gso. red; intros; subst r. rewrite preg_of_data in H; discriminate.
 - auto.
-- rewrite IHres2, IHres1; auto.
+- rewrite !Pregmap.gso; auto.
+  red; intros; subst r. rewrite preg_of_data in H; discriminate.
+  red; intros; subst r. rewrite preg_of_data in H; discriminate.
 Qed.
 
 (** * Correspondence between Mach code and Asm code *)
diff --git a/backend/Debugvar.v b/backend/Debugvar.v
index 1f36103017..0cb33a8860 100644
--- a/backend/Debugvar.v
+++ b/backend/Debugvar.v
@@ -111,11 +111,11 @@ Fixpoint arg_no_overlap (a: builtin_arg loc) (l: loc) : bool :=
 Definition kill (l: loc) (s: avail) : avail :=
   List.filter (fun vi => arg_no_overlap (proj1_sig (snd vi)) l) s.
 
-Fixpoint kill_res (r: builtin_res mreg) (s: avail) : avail :=
+Definition kill_res (r: builtin_res mreg) (s: avail) : avail :=
   match r with
   | BR r => kill (R r) s
   | BR_none => s
-  | BR_splitlong hi lo => kill_res hi (kill_res lo s)
+  | BR_splitlong hi lo => kill (R hi) (kill (R lo) s)
   end.
 
 (** Likewise when a function call takes place. *)
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 62aa09e259..bee0ded470 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -54,11 +54,11 @@ Definition loc_valid (l: loc) : bool :=
   | S _ _ _ => false
   end.
 
-Fixpoint wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool :=
+Definition wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool :=
   match res with
   | BR r => subtype ty (mreg_type r)
   | BR_none => true
-  | BR_splitlong hi lo => wt_builtin_res Tint hi && wt_builtin_res Tint lo
+  | BR_splitlong hi lo => subtype Tint (mreg_type hi) && subtype Tint (mreg_type lo)
   end.
 
 Definition wt_instr (i: instruction) : bool :=
@@ -180,8 +180,11 @@ Proof.
   induction res; simpl; intros.
 - apply wt_setreg; auto. eapply Val.has_subtype; eauto.
 - auto.
-- InvBooleans. eapply IHres2; eauto. destruct v; exact I.
-  eapply IHres1; eauto. destruct v; exact I.
+- InvBooleans.
+  apply wt_setreg; auto. apply Val.has_subtype with (ty1 := Tint); auto.
+  destruct v; exact I.
+  apply wt_setreg; auto. apply Val.has_subtype with (ty1 := Tint); auto.
+  destruct v; exact I.
 Qed.
 
 (** Soundness of the type system *)
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 30cc0d9194..bd232be31f 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -55,11 +55,11 @@ Definition loc_valid (l: loc) : bool :=
   | S _ _ _ => false
   end.
 
-Fixpoint wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool :=
+Definition wt_builtin_res (ty: typ) (res: builtin_res mreg) : bool :=
   match res with
   | BR r => subtype ty (mreg_type r)
   | BR_none => true
-  | BR_splitlong hi lo => wt_builtin_res Tint hi && wt_builtin_res Tint lo
+  | BR_splitlong hi lo => subtype Tint (mreg_type hi) && subtype Tint (mreg_type lo)
   end.
 
 Definition wt_instr (i: instruction) : bool :=
@@ -180,8 +180,11 @@ Proof.
   induction res; simpl; intros.
 - apply wt_setreg; auto. eapply Val.has_subtype; eauto.
 - auto.
-- InvBooleans. eapply IHres2; eauto. destruct v; exact I.
-  eapply IHres1; eauto. destruct v; exact I.
+- InvBooleans.
+  apply wt_setreg; auto. apply Val.has_subtype with (ty1 := Tint); auto.
+  destruct v; exact I.
+  apply wt_setreg; auto. apply Val.has_subtype with (ty1 := Tint); auto.
+  destruct v; exact I.
 Qed.
 
 Lemma wt_find_label:
diff --git a/backend/Locations.v b/backend/Locations.v
index c437df5dd6..c2cb66d98b 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -417,12 +417,12 @@ Module Locmap.
   - destruct H. rewrite ! gso by (apply Loc.diff_sym; auto). auto.
   Qed.
 
-  Fixpoint setres (res: builtin_res mreg) (v: val) (m: t) : t :=
+  Definition setres (res: builtin_res mreg) (v: val) (m: t) : t :=
     match res with
     | BR r => set (R r) v m
     | BR_none => m
     | BR_splitlong hi lo =>
-        setres lo (Val.loword v) (setres hi (Val.hiword v) m)
+        set (R lo) (Val.loword v) (set (R hi) (Val.hiword v) m)
     end.
 
 End Locmap.
diff --git a/backend/Mach.v b/backend/Mach.v
index 839a25bd45..e11a5a4f50 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -162,11 +162,11 @@ Definition set_pair (p: rpair mreg) (v: val) (rs: regset) : regset :=
   | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
   end.
 
-Fixpoint set_res (res: builtin_res mreg) (v: val) (rs: regset) : regset :=
+Definition set_res (res: builtin_res mreg) (v: val) (rs: regset) : regset :=
   match res with
   | BR r => Regmap.set r v rs
   | BR_none => rs
-  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+  | BR_splitlong hi lo => Regmap.set lo (Val.loword v) (Regmap.set hi (Val.hiword v) rs)
   end.
 
 Definition is_label (lbl: label) (instr: instruction) : bool :=
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index df3445ea6a..8c18fc9a6b 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -243,7 +243,7 @@ let print_asm_argument print_preg oc modifier = function
 
 let builtin_arg_of_res = function
   | BR r -> BA r
-  | BR_splitlong(BR hi, BR lo) -> BA_splitlong(BA hi, BA lo)
+  | BR_splitlong(hi, lo) -> BA_splitlong(BA hi, BA lo)
   | _ -> assert false
 
 let re_asm_param_1 = Str.regexp "%%\\|%[QR]?[0-9]+"
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index d4d7362d81..05cea84999 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -174,7 +174,7 @@ let convert_builtin_res tyenv = function
   | BR r ->
       let ty = tyenv r in
       if Archi.splitlong && ty = Tlong
-      then BR_splitlong(BR(V(r, Tint)), BR(V(twin_reg r, Tint)))
+      then BR_splitlong(V(r, Tint), V(twin_reg r, Tint))
       else BR(V(r, ty))
   | BR_none -> BR_none
   | BR_splitlong _ -> assert false
@@ -201,15 +201,20 @@ let rec constrain_builtin_args al cl =
       let (al', cl2) = constrain_builtin_args al cl1 in
       (a' :: al', cl2)
 
-let rec constrain_builtin_res a cl =
-  match a, cl with
-  | BR x, None :: cl' -> (a, cl')
-  | BR x, Some mr :: cl' -> (BR (L(R mr)), cl')
-  | BR_splitlong(hi, lo), _ ->
-      let (hi', cl1) = constrain_builtin_res hi cl in
-      let (lo', cl2) = constrain_builtin_res lo cl1 in
-      (BR_splitlong(hi', lo'), cl2)
-  | _, _ -> (a, cl)
+let constrain_builtin_res_var x cl =
+  match cl with
+  | None :: cl' -> (BR x, cl')
+  | Some mr :: cl' -> (BR (L(R mr)), cl')
+  | _ -> (BR x, cl)
+
+let constrain_builtin_res a cl =
+  match a with
+  | BR x -> constrain_builtin_res_var x cl
+  | BR_splitlong(hi, lo) ->
+      let (hi', cl1) = constrain_builtin_res_var hi cl in
+      let (lo', cl2) = constrain_builtin_res_var lo cl1 in
+      (BR_splitlong(hi, lo), cl2)
+  | _ -> (a, cl)
 
 (* Return the XTL basic block corresponding to the given RTL instruction.
    Move and parallel move instructions are introduced to honor calling
@@ -346,11 +351,11 @@ let rec vset_addarg a after =
 
 let vset_addargs al after = List.fold_right vset_addarg al after
 
-let rec vset_removeres r after =
+let vset_removeres r after =
   match r with
   | BR v -> VSet.remove v after
   | BR_none -> after
-  | BR_splitlong(hi, lo) -> vset_removeres hi (vset_removeres lo after)
+  | BR_splitlong(hi, lo) -> VSet.remove hi (VSet.remove lo after)
 
 let live_before instr after =
   match instr with
@@ -883,15 +888,15 @@ let save_var tospill eqs v =
     (t, [Xspill(t, v)], add v t (kill v eqs))
   end
 
-let rec save_res tospill eqs = function
+let save_res tospill eqs = function
   | BR v ->
       let (t, c1, eqs1) = save_var tospill eqs v in
       (BR t, c1, eqs1)
   | BR_none ->
       (BR_none, [], eqs)
   | BR_splitlong(hi, lo) ->
-      let (hi', c1, eqs1) = save_res tospill eqs hi in
-      let (lo', c2, eqs2) = save_res tospill eqs1 lo in
+      let (hi', c1, eqs1) = save_var tospill eqs hi in
+      let (lo', c2, eqs2) = save_var tospill eqs1 lo in
       (BR_splitlong(hi', lo'), c1 @ c2, eqs2)
 
 (* Trimming equations when we have too many or when they are too old.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index f7570f571f..dd4a4e1d3e 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -639,7 +639,7 @@ Proof.
   induction res; simpl; intros.
 - apply agree_regs_set_reg; auto.
 - auto.
-- apply IHres2. apply IHres1. auto.
+- repeat apply agree_regs_set_reg; auto.
   apply Val.hiword_inject; auto.
   apply Val.loword_inject; auto.
 Qed.
@@ -740,7 +740,7 @@ Proof.
   induction res; simpl; intros.
 - eapply agree_locs_set_reg; eauto.
 - auto.
-- apply IHres2; auto using in_or_app.
+- repeat eapply agree_locs_set_reg; eauto.
 Qed.
 
 Lemma agree_locs_undef_regs:
diff --git a/backend/XTL.ml b/backend/XTL.ml
index f10efeedbc..d39b38b8fd 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -142,10 +142,10 @@ let rec type_builtin_args al tyl =
   | a :: al, ty :: tyl -> type_builtin_arg a ty; type_builtin_args al tyl
   | _, _ -> raise Type_error
 
-let rec type_builtin_res a ty =
+let type_builtin_res a ty =
   match a with
   | BR v -> set_var_type v ty
-  | BR_splitlong(a1, a2) -> type_builtin_res a1 Tint; type_builtin_res a2 Tint
+  | BR_splitlong(a1, a2) -> set_var_type a1 Tint; set_var_type a2 Tint
   | _ -> ()
 
 let type_instr = function
diff --git a/common/AST.v b/common/AST.v
index a072ef2934..d4ea7e4f31 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -633,7 +633,7 @@ Inductive builtin_arg (A: Type) : Type :=
 Inductive builtin_res (A: Type) : Type :=
   | BR (x: A)
   | BR_none
-  | BR_splitlong (hi lo: builtin_res A).
+  | BR_splitlong (hi lo: A).
 
 Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident :=
   match a with
@@ -658,11 +658,11 @@ Fixpoint params_of_builtin_arg (A: Type) (a: builtin_arg A) : list A :=
 Definition params_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list A :=
   List.fold_right (fun a l => params_of_builtin_arg a ++ l) nil al.
 
-Fixpoint params_of_builtin_res (A: Type) (a: builtin_res A) : list A :=
+Definition params_of_builtin_res (A: Type) (a: builtin_res A) : list A :=
   match a with
   | BR x => x :: nil
   | BR_none => nil
-  | BR_splitlong hi lo => params_of_builtin_res hi ++ params_of_builtin_res lo
+  | BR_splitlong hi lo => hi :: lo :: nil
   end.
 
 Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_arg B :=
@@ -682,12 +682,11 @@ Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_ar
       BA_addptr (map_builtin_arg f a1) (map_builtin_arg f a2)
   end.
 
-Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B :=
+Definition map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B :=
   match a with
   | BR x => BR (f x)
   | BR_none => BR_none
-  | BR_splitlong hi lo =>
-      BR_splitlong (map_builtin_res f hi) (map_builtin_res f lo)
+  | BR_splitlong hi lo => BR_splitlong (f hi) (f lo)
   end.
 
 (** Which kinds of builtin arguments are supported by which external function. *)
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index ac7d22766f..8cd0f2a080 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -80,10 +80,8 @@ let rec print_builtin_args px oc = function
   | a1 :: al ->
       fprintf oc "%a, %a" (print_builtin_arg px) a1 (print_builtin_args px) al
 
-let rec print_builtin_res px oc = function
+let print_builtin_res px oc = function
   | BR x -> px oc x
   | BR_none -> fprintf oc "_"
-  | BR_splitlong(hi, lo) ->
-      fprintf oc "splitlong(%a, %a)"
-                 (print_builtin_res px) hi (print_builtin_res px) lo
+  | BR_splitlong(hi, lo) -> fprintf oc "splitlong(%a, %a)" px hi px lo
 
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 746a610b7b..c2277b8af3 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -454,11 +454,11 @@ Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
 
 (** Assigning the result of a builtin *)
 
-Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
+Definition set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   match res with
   | BR r => rs#r <- v
   | BR_none => rs
-  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+  | BR_splitlong hi lo => rs #hi <- (Val.hiword v) #lo <- (Val.loword v)
   end.
 
 Section RELSEM.
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index deab77033e..80a535e916 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -275,7 +275,7 @@ let expand_builtin_vload_1 chunk addr res =
         (fun r c -> emit (Pld(res, c, r)))
         (fun r1 r2 -> emit (Pldx(res, r1, r2)))
         addr GPR11
-  | Mint64, BR_splitlong(BR(IR hi), BR(IR lo)) ->
+  | Mint64, BR_splitlong(IR hi, IR lo) ->
       expand_volatile_access
         (fun r c ->
            match offset_constant c _4 with
@@ -517,24 +517,24 @@ let expand_builtin_inline name args res =
       emit (Pcfi_adjust _m8)
   (* 64-bit integer arithmetic *)
   | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
       expand_int64_arith (rl = ah) rl (fun rl ->
         emit (Psubfic(rl, al, Cint _0));
         emit (Psubfze(rh, ah)))
   | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al));
                        BA_splitlong(BA(IR bh), BA(IR bl))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
       expand_int64_arith (rl = ah || rl = bh) rl (fun rl ->
         emit (Paddc(rl, al, bl));
         emit (Padde(rh, ah, bh)))
   | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al));
                        BA_splitlong(BA(IR bh), BA(IR bl))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
       expand_int64_arith (rl = ah || rl = bh) rl (fun rl ->
         emit (Psubfc(rl, bl, al));
         emit (Psubfe(rh, bh, ah)))
   | "__builtin_mull", [BA(IR a); BA(IR b)],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
       expand_int64_arith (rl = a || rl = b) rl (fun rl ->
         emit (Pmullw(rl, a, b));
         emit (Pmulhwu(rh, a, b)))
diff --git a/riscV/Asm.v b/riscV/Asm.v
index 4cd3b1fd0f..db7bddadf5 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -483,11 +483,11 @@ Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset :=
 
 (** Assigning the result of a builtin *)
 
-Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
+Definition set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   match res with
   | BR r => rs#r <- v
   | BR_none => rs
-  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+  | BR_splitlong hi lo => rs #hi <- (Val.hiword v) #lo <- (Val.loword v)
   end.
 
 Section RELSEM.
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index d42f4d134c..164f11e7b8 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -224,7 +224,7 @@ let expand_builtin_vload_common chunk base ofs res =
      emit (Plw  (res, base, Ofsimm ofs))
   | Mint64, BR(IR res) ->
      emit (Pld  (res, base, Ofsimm ofs))
-  | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) ->
+  | Mint64, BR_splitlong(IR res1, IR res2) ->
      let ofs' = Ptrofs.add ofs _4 in
      if base <> res2 then begin
          emit (Plw (res2, base, Ofsimm ofs));
@@ -414,7 +414,7 @@ let expand_builtin_inline name args res =
   | "__builtin_bswap64", [BA(IR a1)], BR(IR res) ->
      expand_bswap64 res a1
   | "__builtin_bswap64", [BA_splitlong(BA(IR ah), BA(IR al))],
-                         BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                         BR_splitlong(IR rh, IR rl) ->
      assert (ah = X6 && al = X5 && rh = X5 && rl = X6);
      expand_bswap32 X5 X5;
      expand_bswap32 X6 X6
@@ -437,7 +437,7 @@ let expand_builtin_inline name args res =
       emit (Pfmaxd(res, a1, a2))
   (* 64-bit integer arithmetic for a 32-bit platform *)
   | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      expand_int64_arith (rl = ah) rl
 			(fun rl ->
                          emit (Psltuw (X1, X0, X al));
@@ -446,7 +446,7 @@ let expand_builtin_inline name args res =
 			 emit (Psubw (rh, X rh, X X1)))
   | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al));
                        BA_splitlong(BA(IR bh), BA(IR bl))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      expand_int64_arith (rl = bl || rl = ah || rl = bh) rl
 			(fun rl ->
 			 emit (Paddw (rl, X al, X bl));
@@ -455,7 +455,7 @@ let expand_builtin_inline name args res =
 			 emit (Paddw (rh, X rh, X X1)))
   | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al));
                        BA_splitlong(BA(IR bh), BA(IR bl))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      expand_int64_arith (rl = ah || rl = bh) rl
 			(fun rl ->
                          emit (Psltuw (X1, X al, X bl));
@@ -463,7 +463,7 @@ let expand_builtin_inline name args res =
 			 emit (Psubw (rh, X ah, X bh));
 			 emit (Psubw (rh, X rh, X X1)))
   | "__builtin_mull", [BA(IR a); BA(IR b)],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      expand_int64_arith (rl = a || rl = b) rl
                         (fun rl ->
                           emit (Pmulw (rl, X a, X b));
diff --git a/x86/Asm.v b/x86/Asm.v
index 8b873e48ac..c0a7076c2d 100644
--- a/x86/Asm.v
+++ b/x86/Asm.v
@@ -333,11 +333,11 @@ Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
 
 (** Assigning the result of a builtin *)
 
-Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
+Definition set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   match res with
   | BR r => rs#r <- v
   | BR_none => rs
-  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+  | BR_splitlong hi lo => rs #hi <- (Val.hiword v) #lo <- (Val.loword v)
   end.
 
 Section RELSEM.
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index 1b71616549..4097f59afe 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -173,7 +173,7 @@ let expand_builtin_vload_common chunk addr res =
      emit (Pmovl_rm (res,addr))
   | Mint64, BR(IR res) ->
      emit (Pmovq_rm (res,addr))
-  | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) ->
+  | Mint64, BR_splitlong(IR res1, IR res2) ->
      let addr' = offset_addressing addr _4z in
      if not (Asmgen.addressing_mentions addr res2) then begin
 	 emit (Pmovl_rm (res2,addr));
@@ -323,7 +323,7 @@ let expand_builtin_inline name args res =
        emit (Pmov_rr (res,a1));
      emit (Pbswap64 res)
   | "__builtin_bswap64", [BA_splitlong(BA(IR ah), BA(IR al))],
-                         BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                         BR_splitlong(IR rh, IR rl) ->
      assert (ah = RAX && al = RDX && rh = RDX && rl = RAX);
      emit (Pbswap32 RAX);
      emit (Pbswap32 RDX)
@@ -411,25 +411,25 @@ let expand_builtin_inline name args res =
         (fun r1 r2 r3 -> Pfnmsub231(r1, r2, r3))
   (* 64-bit integer arithmetic *)
   | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      assert (ah = RDX && al = RAX && rh = RDX && rl = RAX);
      emit (Pnegl RAX);
      emit (Padcl_ri (RDX,_0));
      emit (Pnegl RDX)
   | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al));
                        BA_splitlong(BA(IR bh), BA(IR bl))],
-                       BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                       BR_splitlong(IR rh, IR rl) ->
      assert (ah = RDX && al = RAX && bh = RCX && bl = RBX && rh = RDX && rl = RAX);
      emit (Paddl_rr (RAX,RBX));
      emit (Padcl_rr (RDX,RCX))
   | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al));
                        BA_splitlong(BA(IR bh), BA(IR bl))],
-                       BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                       BR_splitlong(IR rh, IR rl) ->
      assert (ah = RDX && al = RAX && bh = RCX && bl = RBX && rh = RDX && rl = RAX);
      emit (Psubl_rr (RAX,RBX));
      emit (Psbbl_rr (RDX,RCX))
   | "__builtin_mull", [BA(IR a); BA(IR b)],
-                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
+                      BR_splitlong(IR rh, IR rl) ->
      assert (a = RAX && b = RDX && rh = RDX && rl = RAX);
      emit (Pmull_r RDX)
   (* Memory accesses *)

From bdafe18e517d315634744b5d39d8711250793320 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gerg=C3=B6=20Barany?= <gergo.barany@inria.fr>
Date: Mon, 21 Aug 2017 15:21:04 +0200
Subject: [PATCH 3/5] Proof of type preservation on LTL.

If LTLtyping finds that the program after register allocation is well-typed,
then execution preserves well-typedness of the state. In particular, this
typing property ensures that Locmap accesses are well-typed: All register
writes are of values with a type compatible with the register's type.
---
 arm/Op.v                 |  11 +
 backend/Allocation.v     |  10 +-
 backend/Allocproof.v     | 609 ++++++++++++++++++++++++++++++---------
 backend/LTLtyping.v      |  35 ++-
 backend/Lineartyping.v   |   2 +-
 backend/Locations.v      |  17 +-
 backend/Stackingproof.v  |  56 +++-
 backend/Tunnelingproof.v |   4 +-
 common/Values.v          |  42 +++
 powerpc/Op.v             |  11 +
 riscV/Op.v               |  11 +
 x86/Op.v                 |  11 +
 12 files changed, 645 insertions(+), 174 deletions(-)

diff --git a/arm/Op.v b/arm/Op.v
index 60c214d082..b22dc688a0 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -557,6 +557,17 @@ Proof.
   intros; discriminate.
 Qed.
 
+Lemma is_not_move_operation:
+  forall (F V A: Type) (genv: Genv.t F V) (sp: val)
+         (op: operation) (f: A -> val) (args: list A) (m: mem) (v: val),
+  eval_operation genv sp op (map f args) m = Some v ->
+  is_move_operation op args = None ->
+  op <> Omove.
+Proof.
+  intros. destruct (eq_operation op Omove); auto.
+  subst. destruct args; try destruct args; simpl in *; congruence.
+Qed.
+
 (** [negate_condition cond] returns a condition that is logically
   equivalent to the negation of [cond]. *)
 
diff --git a/backend/Allocation.v b/backend/Allocation.v
index d8775f643e..c8cbc87d65 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -849,6 +849,8 @@ Definition remove_equations_builtin_res
   | BR r, BR r' => Some (remove_equation (Eq Full r (R r')) e)
   | BR r, BR_splitlong rhi rlo =>
       assertion (typ_eq (env r) Tlong);
+      assertion (subtype Tint (mreg_type rhi));
+      assertion (subtype Tint (mreg_type rlo));
       if mreg_eq rhi rlo then None else
         Some (remove_equation (Eq Low r (R rlo))
                 (remove_equation (Eq High r (R rhi)) e))
@@ -932,12 +934,6 @@ Definition destroyed_by_move (src dst: loc) :=
   | _, _ => destroyed_by_op Omove
   end.
 
-Definition well_typed_move (env: regenv) (dst: loc) (e: eqs) : bool :=
-  match dst with
-  | R r => true
-  | S sl ofs ty => loc_type_compat env dst e
-  end.
-
 (** Simulate the effect of a sequence of moves [mv] on a set of
   equations [e].  The set [e] is the equations that must hold
   after the sequence of moves.  Return the set of equations that
@@ -950,7 +946,7 @@ Fixpoint track_moves (env: regenv) (mv: moves) (e: eqs) : option eqs :=
   | MV src dst :: mv =>
       do e1 <- track_moves env mv e;
       assertion (can_undef_except dst (destroyed_by_move src dst)) e1;
-      assertion (well_typed_move env dst e1);
+      assertion (loc_type_compat env dst e1);
       subst_loc dst src e1
   | MVmakelong src1 src2 dst :: mv =>
       assertion (negb Archi.ptr64);
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 6901f9cd0d..d3ac289529 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -18,6 +18,7 @@ Require Import Coqlib Ordered Maps Errors Integers Floats.
 Require Import AST Linking Lattice Kildall.
 Require Import Values Memory Globalenvs Events Smallstep.
 Require Archi.
+Require Import LTLtyping.
 Require Import Op Registers RTL Locations Conventions RTLtyping LTL.
 Require Import Allocation.
 
@@ -214,7 +215,8 @@ Proof.
 Qed.
 
 Lemma extract_moves_sound:
-  forall b mv b',
+  forall f b mv b',
+  wt_bblock f b = true ->
   extract_moves nil b = (mv, b') ->
   wf_moves mv /\ b = expand_moves mv b'.
 Proof.
@@ -225,18 +227,19 @@ Proof.
    { intros; split; auto. unfold wf_moves in *; rewrite Forall_forall in *.
      intros. apply H. rewrite <- in_rev in H0; auto. }
 
-  assert (IND: forall b accu mv b',
+  assert (IND: forall f b accu mv b',
+          wt_bblock f b = true ->
           extract_moves accu b = (mv, b') ->
           wf_moves accu ->
           wf_moves mv /\ expand_moves (List.rev accu) b = expand_moves mv b').
   { induction b; simpl; intros.
-  - inv H. auto.
-  - destruct a; try (inv H; apply BASE; auto; fail).
+  - inv H0. auto.
+  - destruct a; try (inv H0; apply BASE; auto; fail); simpl in H; InvBooleans.
   + destruct (is_move_operation op args) as [arg|] eqn:E.
     exploit is_move_operation_correct; eauto. intros [A B]; subst.
     (* reg-reg move *)
     exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto.
-    inv H; apply BASE; auto.
+    inv H0; apply BASE; auto.
   + (* stack-reg move *)
     exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto.
   + (* reg-stack move *)
@@ -246,7 +249,8 @@ Proof.
 Qed.
 
 Lemma extract_moves_ext_sound:
-  forall b mv b',
+  forall f b mv b',
+  wt_bblock f b = true ->
   extract_moves_ext nil b = (mv, b') ->
   wf_moves mv /\ b = expand_moves mv b'.
 Proof.
@@ -257,13 +261,14 @@ Proof.
    { intros; split; auto. unfold wf_moves in *; rewrite Forall_forall in *.
      intros. apply H. rewrite <- in_rev in H0; auto. }
 
-  assert (IND: forall b accu mv b',
+  assert (IND: forall f b accu mv b',
+          wt_bblock f b = true ->
           extract_moves_ext accu b = (mv, b') ->
           wf_moves accu ->
           wf_moves mv /\ expand_moves (List.rev accu) b = expand_moves mv b').
   { induction b; simpl; intros.
-  - inv H. auto.
-  - destruct a; try (inv H; apply BASE; auto; fail).
+  - inv H0. auto.
+  - destruct a; try (inv H0; apply BASE; auto; fail); simpl in H; InvBooleans.
   + destruct (classify_operation op args).
   * (* reg-reg move *)
     exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto.
@@ -274,7 +279,7 @@ Proof.
   * (* highlong *)
     exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto.
   * (* default *)
-    inv H; apply BASE; auto.
+    inv H0; apply BASE; auto.
   + (* stack-reg move *)
     exploit IHb; eauto. constructor; auto. exact I. rewrite expand_moves_cons; auto.
   + (* reg-stack move *)
@@ -291,12 +296,36 @@ Proof.
   destruct (peq s s0); simpl in H; inv H. exists b; auto.
 Qed.
 
+Lemma wt_bblock_expand_moves_head:
+  forall f m i b,
+  wt_bblock f (expand_moves m (i :: b)) = true -> LTLtyping.wt_instr f i = true.
+Proof.
+  intros. unfold expand_moves, wt_bblock in H.
+  rewrite forallb_app in H; InvBooleans.
+  simpl in H1; InvBooleans. auto.
+Qed.
+
+Lemma wt_bblock_expand_moves_cons:
+  forall f m i b,
+  wt_bblock f (expand_moves m (i :: b)) = true -> wt_bblock f b = true.
+Proof.
+  induction b; intros; auto.
+  simpl. unfold expand_moves, wt_bblock in H.
+  rewrite forallb_app in H; InvBooleans.
+  simpl in H1; InvBooleans. unfold wt_bblock.
+  rewrite H1, H3; auto.
+Qed.
+
 Ltac UseParsingLemmas :=
   match goal with
-  | [ H: extract_moves nil _ = (_, _) |- _ ] =>
-      destruct (extract_moves_sound _ _ _ H); clear H; subst; UseParsingLemmas
-  | [ H: extract_moves_ext nil _ = (_, _) |- _ ] =>
-      destruct (extract_moves_ext_sound _ _ _ H); clear H; subst; UseParsingLemmas
+  | [ H: extract_moves nil ?b = (_, _), WT: wt_bblock _ ?b = true |- _ ] =>
+      destruct (extract_moves_sound _ _ _ _ WT H); clear H; subst; UseParsingLemmas
+  | [ H: extract_moves nil ?b = (_, _), WT: wt_bblock _ (expand_moves _ (_ :: ?b)) = true |- _ ] =>
+      apply wt_bblock_expand_moves_cons in WT; UseParsingLemmas
+  | [ H: extract_moves_ext nil ?b = (_, _), WT: wt_bblock _ ?b = true |- _ ] =>
+      destruct (extract_moves_ext_sound _ _ _ _ WT H); clear H; subst; UseParsingLemmas
+  | [ H: extract_moves_ext nil ?b = (_, _), WT: wt_bblock _ (expand_moves _ (_ :: ?b)) = true |- _ ] =>
+      apply wt_bblock_expand_moves_cons in WT; UseParsingLemmas
   | [ H: check_succ _ _ = true |- _ ] =>
       try (discriminate H);
       destruct (check_succ_sound _ _ H); clear H; subst; UseParsingLemmas
@@ -304,19 +333,21 @@ Ltac UseParsingLemmas :=
   end.
 
 Lemma pair_instr_block_sound:
-  forall i b bsh,
+  forall i f b bsh,
+  wt_bblock f b = true ->
   pair_instr_block i b = Some bsh -> expand_block_shape bsh i b.
 Proof.
-  assert (OP: forall op args res s b bsh,
+  assert (OP: forall op args res s f b bsh,
+    wt_bblock f b = true ->
     pair_Iop_block op args res s b = Some bsh -> expand_block_shape bsh (Iop op args res s) b).
   {
     unfold pair_Iop_block; intros. MonadInv. destruct b0.
     MonadInv; UseParsingLemmas.
     destruct i; MonadInv; UseParsingLemmas.
     eapply ebs_op; eauto.
-    inv H0. eapply ebs_op_dead; eauto. }
+    inv H1. eapply ebs_op_dead; eauto. }
 
-  intros; destruct i; simpl in H; MonadInv; UseParsingLemmas.
+  intros i f b bsh WT; intros; destruct i; simpl in H; MonadInv; UseParsingLemmas.
 - (* nop *)
   econstructor; eauto.
 - (* op *)
@@ -371,11 +402,14 @@ Lemma matching_instr_block:
   forall f1 f2 pc bsh i,
   (pair_codes f1 f2)!pc = Some bsh ->
   (RTL.fn_code f1)!pc = Some i ->
+  LTLtyping.wt_function f2 = true ->
   exists b, (LTL.fn_code f2)!pc = Some b /\ expand_block_shape bsh i b.
 Proof.
   intros. unfold pair_codes in H. rewrite PTree.gcombine in H; auto. rewrite H0 in H.
-  destruct (LTL.fn_code f2)!pc as [b|].
-  exists b; split; auto. apply pair_instr_block_sound; auto.
+  destruct (LTL.fn_code f2)!pc as [b|] eqn:B.
+  exists b; split; auto.
+  eapply wt_function_wt_bblock in H1; eauto.
+  eapply pair_instr_block_sound; eauto.
   discriminate.
 Qed.
 
@@ -685,11 +719,12 @@ Lemma loc_unconstrained_satisf:
   satisf rs ls (remove_equation (Eq k r l) e) ->
   loc_unconstrained (R mr) (remove_equation (Eq k r l) e) = true ->
   Val.lessdef (sel_val k rs#r) v ->
+  Val.has_type v (mreg_type mr) ->
   satisf rs (Locmap.set l v ls) e.
 Proof.
   intros; red; intros.
   destruct (OrderedEquation.eq_dec q (Eq k r l)).
-  subst q; simpl. unfold l; rewrite Locmap.gss. auto.
+  subst q; simpl. unfold l; rewrite Locmap.gss. rewrite pred_dec_true; auto.
   assert (EqSet.In q (remove_equation (Eq k r l) e)).
     simpl. ESD.fsetdec.
   rewrite Locmap.gso. apply H; auto. eapply loc_unconstrained_sound; eauto.
@@ -709,13 +744,14 @@ Lemma parallel_assignment_satisf:
   forall k r mr e rs ls v v',
   let l := R mr in
   Val.lessdef (sel_val k v) v' ->
+  Val.has_type v' (mreg_type mr) ->
   reg_loc_unconstrained r (R mr) (remove_equation (Eq k r l) e) = true ->
   satisf rs ls (remove_equation (Eq k r l) e) ->
   satisf (rs#r <- v) (Locmap.set l v' ls) e.
 Proof.
   intros; red; intros.
   destruct (OrderedEquation.eq_dec q (Eq k r l)).
-  subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss; auto.
+  subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss, pred_dec_true; auto.
   assert (EqSet.In q (remove_equation {| ekind := k; ereg := r; eloc := l |} e)).
     simpl. ESD.fsetdec.
   exploit reg_loc_unconstrained_sound; eauto. intros [A B].
@@ -729,24 +765,25 @@ Lemma parallel_assignment_satisf_2:
   reg_unconstrained res e' = true ->
   forallb (fun l => loc_unconstrained l e') (map R (regs_of_rpair res')) = true ->
   Val.lessdef v v' ->
+  Val.has_type_rpair v' res' Val.loword Val.hiword mreg_type ->
   satisf (rs#res <- v) (Locmap.setpair res' v' ls) e.
 Proof.
   intros. functional inversion H.
 - (* One location *)
   subst. simpl in H2. InvBooleans. simpl.
   apply parallel_assignment_satisf with Full; auto.
-  unfold reg_loc_unconstrained. rewrite H1, H4. auto.
+  unfold reg_loc_unconstrained. rewrite H1, H5. auto.
 - (* Two 32-bit halves *)
-  subst.
+  subst. destruct H4.
   set (e' := remove_equation {| ekind := Low; ereg := res; eloc := R mr2 |}
           (remove_equation {| ekind := High; ereg := res; eloc := R mr1 |} e)) in *.
   simpl in H2. InvBooleans. simpl.
   red; intros.
   destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))).
-  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss.
+  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss, pred_dec_true by auto.
   apply Val.loword_lessdef; auto.
   destruct (OrderedEquation.eq_dec q (Eq High res (R mr1))).
-  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by auto. rewrite Locmap.gss.
+  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso, Locmap.gss, pred_dec_true by auto.
   apply Val.hiword_lessdef; auto.
   assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec.
   rewrite Regmap.gso. rewrite ! Locmap.gso. auto.
@@ -1007,19 +1044,14 @@ Proof.
   exact (select_loc_h_monotone l).
 Qed.
 
-Lemma well_typed_move_charact:
+Lemma loc_type_compat_well_typed:
   forall env l e k r rs,
-  well_typed_move env l e = true ->
+  loc_type_compat env l e = true ->
   EqSet.In (Eq k r l) e ->
   wt_regset env rs ->
-  match l with
-  | R mr => True
-  | S sl ofs ty => Val.has_type (sel_val k rs#r) ty
-  end.
+  Val.has_type (sel_val k rs#r) (Loc.type l).
 Proof.
-  unfold well_typed_move; intros.
-  destruct l as [mr | sl ofs ty].
-  auto.
+  intros.
   exploit loc_type_compat_charact; eauto. intros [A | A].
   simpl in A. eapply Val.has_subtype; eauto.
   generalize (H1 r). destruct k; simpl; intros.
@@ -1040,8 +1072,9 @@ Qed.
 Lemma subst_loc_satisf:
   forall env src dst rs ls e e',
   subst_loc dst src e = Some e' ->
-  well_typed_move env dst e = true ->
+  loc_type_compat env dst e = true ->
   wt_regset env rs ->
+  Val.has_type (ls src) (Loc.type dst) ->
   satisf rs ls e' ->
   satisf rs (Locmap.set dst (ls src) ls) e.
 Proof.
@@ -1049,10 +1082,10 @@ Proof.
   exploit in_subst_loc; eauto. intros [[A B] | [A B]].
   subst dst. rewrite Locmap.gss.
   destruct q as [k r l]; simpl in *.
-  exploit well_typed_move_charact; eauto.
+  exploit loc_type_compat_well_typed; eauto.
   destruct l as [mr | sl ofs ty]; intros.
-  apply (H2 _ B).
-  apply val_lessdef_normalize; auto. apply (H2 _ B).
+  rewrite pred_dec_true by auto. apply (H3 _ B).
+  apply val_lessdef_normalize; auto. apply (H3 _ B).
   rewrite Locmap.gso; auto.
 Qed.
 
@@ -1107,24 +1140,28 @@ Qed.
 Lemma subst_loc_part_satisf_lowlong:
   forall src dst rs ls e e',
   subst_loc_part (R dst) (R src) Low e = Some e' ->
+  Val.has_type (Val.loword (ls (R src))) (mreg_type dst) ->
   satisf rs ls e' ->
   satisf rs (Locmap.set (R dst) (Val.loword (ls (R src))) ls) e.
 Proof.
   intros; red; intros.
   exploit in_subst_loc_part; eauto. intros [[A [B C]] | [A B]].
-  rewrite A, B. apply H0 in C. rewrite Locmap.gss. apply Val.loword_lessdef. exact C.
+  rewrite A, B. apply H1 in C. rewrite Locmap.gss, pred_dec_true by auto.
+  apply Val.loword_lessdef. exact C.
   rewrite Locmap.gso; auto.
 Qed.
 
 Lemma subst_loc_part_satisf_highlong:
   forall src dst rs ls e e',
   subst_loc_part (R dst) (R src) High e = Some e' ->
+  Val.has_type (Val.hiword (ls (R src))) (mreg_type dst) ->
   satisf rs ls e' ->
   satisf rs (Locmap.set (R dst) (Val.hiword (ls (R src))) ls) e.
 Proof.
   intros; red; intros.
   exploit in_subst_loc_part; eauto. intros [[A [B C]] | [A B]].
-  rewrite A, B. apply H0 in C. rewrite Locmap.gss. apply Val.hiword_lessdef. exact C.
+  rewrite A, B. apply H1 in C. rewrite Locmap.gss, pred_dec_true by auto.
+  apply Val.hiword_lessdef. exact C.
   rewrite Locmap.gso; auto.
 Qed.
 
@@ -1206,6 +1243,7 @@ Lemma subst_loc_pair_satisf_makelong:
   wt_regset env rs ->
   satisf rs ls e' ->
   Archi.ptr64 = false ->
+  Val.has_type (Val.longofwords (ls (R src1)) (ls (R src2))) (mreg_type dst) ->
   satisf rs (Locmap.set (R dst) (Val.longofwords (ls (R src1)) (ls (R src2))) ls) e.
 Proof.
   intros; red; intros.
@@ -1214,7 +1252,7 @@ Proof.
   assert (subtype (env (ereg q)) Tlong = true).
   { exploit long_type_compat_charact; eauto. intros [P|P]; auto.
     eelim Loc.diff_not_eq; eauto. }
-  rewrite Locmap.gss. simpl. rewrite <- (val_longofwords_eq_1 rs#(ereg q)).
+  rewrite Locmap.gss, pred_dec_true by auto. simpl. rewrite <- (val_longofwords_eq_1 rs#(ereg q)).
   apply Val.longofwords_lessdef. exact C. exact D.
   eapply Val.has_subtype; eauto.
   assumption.
@@ -1266,7 +1304,7 @@ Qed.
 Lemma subst_loc_undef_satisf:
   forall env src dst rs ls ml e e',
   subst_loc dst src e = Some e' ->
-  well_typed_move env dst e = true ->
+  loc_type_compat env dst e = true ->
   can_undef_except dst ml e = true ->
   wt_regset env rs ->
   satisf rs ls e' ->
@@ -1276,9 +1314,19 @@ Proof.
   exploit in_subst_loc; eauto. intros [[A B] | [A B]].
   subst dst. rewrite Locmap.gss.
   destruct q as [k r l]; simpl in *.
-  exploit well_typed_move_charact; eauto.
+  exploit loc_type_compat_well_typed; eauto.
   destruct l as [mr | sl ofs ty]; intros.
-  apply (H3 _ B).
+  destruct (Val.eq (sel_val k rs#r) Vundef).
+  rewrite e0 in *; auto.
+  rewrite pred_dec_true. apply (H3 _ B).
+  exploit loc_type_compat_charact; eauto; intros [SUBTYP | DIFF].
+  simpl in SUBTYP.
+  set (qR := {| ekind := k; ereg := r; eloc := R mr |}).
+  generalize (in_subst_loc (R mr) src qR _ _ H4 H); intros [[EQ IN] | [DIFF' IN']].
+  generalize (H3 _ IN); intro LESSDEF. simpl in LESSDEF.
+  destruct k; simpl in *; inversion LESSDEF; congruence.
+  simpl in DIFF'; congruence.
+  simpl in DIFF; congruence.
   apply val_lessdef_normalize; auto. apply (H3 _ B).
   rewrite Locmap.gso; auto. rewrite undef_regs_outside. eauto.
   eapply can_undef_except_sound; eauto. apply Loc.diff_sym; auto.
@@ -1289,7 +1337,7 @@ Lemma transfer_use_def_satisf:
   transfer_use_def args res args' res' und e = Some e' ->
   satisf rs ls e' ->
   Val.lessdef_list rs##args (reglist ls args') /\
-  (forall v v', Val.lessdef v v' ->
+  (forall v v', Val.lessdef v v' -> Val.has_type v' (mreg_type res') ->
     satisf (rs#res <- v) (Locmap.set (R res') v' (undef_regs und ls)) e).
 Proof.
   unfold transfer_use_def; intros. MonadInv.
@@ -1675,6 +1723,7 @@ Lemma parallel_set_builtin_res_satisf:
   forallb (fun mr => loc_unconstrained (R mr) e1) (params_of_builtin_res res') = true ->
   satisf rs ls e1 ->
   Val.lessdef v v' ->
+  Val.has_type_builtin_res v' res' Val.loword Val.hiword mreg_type ->
   satisf (regmap_setres res v rs) (Locmap.setres res' v' ls) e0.
 Proof.
   intros. rewrite forallb_forall in *.
@@ -1683,23 +1732,25 @@ Proof.
   unfold reg_loc_unconstrained. rewrite H0 by auto. rewrite H1 by auto. auto.
 - set (e' := remove_equation {| ekind := High; ereg := x; eloc := R hi |} e0) in *.
   set (e'' := remove_equation {| ekind := Low; ereg := x; eloc := R lo |} e') in *.
-  simpl in *. red; intros.
-  assert (lo <> hi /\ e'' = e1).
-  { destruct (typ_eq (env x) Tlong), (mreg_eq hi lo); try inversion H5. auto. }
-  destruct H4; subst.
+  red; intros.
+  assert (subtype Tint (mreg_type hi) = true /\
+          subtype Tint (mreg_type lo) = true /\
+          lo <> hi /\ e'' = e1).
+  { destruct (typ_eq (env x) Tlong), (mreg_eq hi lo), (mreg_type hi), (mreg_type lo);
+      try inversion H6; auto. }
+  decompose [and] H4. decompose [and] H5; subst.
   destruct (OrderedEquation.eq_dec q (Eq Low x (R lo))).
-  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss. apply Val.loword_lessdef; auto.
+  subst q; simpl. rewrite Regmap.gss.
+  rewrite Locmap.gss, pred_dec_true; auto. apply Val.loword_lessdef; auto.
   destruct (OrderedEquation.eq_dec q (Eq High x (R hi))).
-  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by (red; tauto).
-  rewrite Locmap.gss. apply Val.hiword_lessdef; auto.
-  rewrite Regmap.gso. rewrite ! Locmap.gso. auto. apply H2.
-  repeat apply ESF.remove_neq_iff; auto.
+  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by (red; auto).
+  rewrite Locmap.gss, pred_dec_true; auto. apply Val.hiword_lessdef; auto.
+  assert (EqSet.In q e'').
+  { unfold e'', e', remove_equation; simpl; ESD.fsetdec. }
+  rewrite Regmap.gso. rewrite ! Locmap.gso. auto.
   eapply loc_unconstrained_sound; eauto.
-  repeat apply ESF.remove_neq_iff; auto.
   eapply loc_unconstrained_sound; eauto.
-  repeat apply ESF.remove_neq_iff; auto.
   eapply reg_unconstrained_sound; eauto.
-  repeat apply ESF.remove_neq_iff; auto.
 - auto.
 Qed.
 
@@ -1757,13 +1808,14 @@ Proof.
   unfold transf_function; intros.
   destruct (type_function f) as [env|] eqn:TY; try discriminate.
   destruct (regalloc f); try discriminate.
-  destruct (LTLtyping.wt_function f0); try discriminate.
+  destruct (LTLtyping.wt_function f0) eqn:WT; try discriminate.
   destruct (check_function f f0 env) as [] eqn:?; inv H.
   unfold check_function in Heqr.
   destruct (analyze f env (pair_codes f tf)) as [an|] eqn:?; try discriminate.
   monadInv Heqr.
   destruct (check_entrypoints_aux f tf env x) as [y|] eqn:?; try discriminate.
   unfold check_entrypoints_aux, pair_entrypoints in Heqo0. MonadInv.
+  eapply wt_function_wt_bblock in WT; eauto.
   exploit extract_moves_ext_sound; eauto. intros [A B]. subst b.
   exploit check_succ_sound; eauto. intros [k EQ1]. subst b0.
   econstructor; eauto. eapply type_function_correct; eauto. congruence.
@@ -1772,6 +1824,7 @@ Qed.
 Lemma invert_code:
   forall f env tf pc i opte e,
   wt_function f env ->
+  LTLtyping.wt_function tf = true ->
   (RTL.fn_code f)!pc = Some i ->
   transfer f env (pair_codes f tf) pc opte = OK e ->
   exists eafter, exists bsh, exists bb,
@@ -1782,10 +1835,10 @@ Lemma invert_code:
   transfer_aux f env bsh eafter = Some e /\
   wt_instr f env i.
 Proof.
-  intros. destruct opte as [eafter|]; simpl in H1; try discriminate. exists eafter.
+  intros. destruct opte as [eafter|]; simpl in H2; try discriminate. exists eafter.
   destruct (pair_codes f tf)!pc as [bsh|] eqn:?; try discriminate. exists bsh.
   exploit matching_instr_block; eauto. intros [bb [A B]].
-  destruct (transfer_aux f env bsh eafter) as [e1|] eqn:?; inv H1.
+  destruct (transfer_aux f env bsh eafter) as [e1|] eqn:?; inv H2.
   exists bb. exploit wt_instr_at; eauto.
   tauto.
 Qed.
@@ -1858,44 +1911,75 @@ Lemma exec_moves:
   wf_moves mv ->
   satisf rs ls e' ->
   wt_regset env rs ->
+  LTLtyping.wt_locset ls /\ LTLtyping.wt_bblock f (expand_moves mv bb) = true ->
   exists ls',
-    star step tge (Block s f sp (expand_moves mv bb) ls m)
-               E0 (Block s f sp bb ls' m)
+  star step tge (Block s f sp (expand_moves mv bb) ls m)
+             E0 (Block s f sp bb ls' m)
+  /\ LTLtyping.wt_locset ls'
   /\ satisf rs ls' e.
 Proof.
 Opaque destroyed_by_op.
   induction mv; simpl; intros.
   (* base *)
-- unfold expand_moves; simpl. inv H. exists ls; split. apply star_refl. auto.
+- unfold expand_moves; simpl. inv H. exists ls; split. apply star_refl. tauto.
   (* step *)
 - assert (wf_moves mv) by (inv H0; auto).
   destruct a; unfold expand_moves; simpl; MonadInv.
 + (* loc-loc move *)
-  destruct src as [rsrc | ssrc]; destruct dst as [rdst | sdst].
+  destruct H3. destruct src as [rsrc | ssrc]; destruct dst as [rdst | sdst].
 * (* reg-reg *)
   exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto.
+  InvBooleans. split; eauto. apply wt_setreg.
+  apply Val.has_subtype with (ty1 := mreg_type rsrc); auto. apply H3.
+  apply wt_undef_regs. auto.
   intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto.
   econstructor. simpl. eauto. auto. auto.
 * (* reg->stack *)
   exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto.
+  InvBooleans. split; eauto. apply wt_setstack, wt_undef_regs. auto.
   intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto.
   econstructor. simpl. eauto. auto.
 * (* stack->reg *)
   simpl in Heqb. exploit IHmv; eauto. eapply subst_loc_undef_satisf; eauto.
+  InvBooleans. split; eauto. apply wt_setreg, wt_undef_regs. auto.
+  apply Val.has_subtype with (ty1 := ty); auto. simpl in H6. InvBooleans; auto.
+  apply H3. auto.
   intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto.
   econstructor. auto. auto.
 * (* stack->stack *)
-  inv H0. simpl in H6. contradiction.
+  inv H0. simpl in H8. contradiction.
 + (* makelong *)
+  assert (HT: Val.has_type (Val.longofwords (ls (R src1)) (ls (R src2))) (mreg_type dst)).
+  {
+    destruct H3; InvBooleans. simpl in H6.
+    destruct (mreg_type dst) eqn:T; simpl; auto; inversion H6.
+    destruct (ls (R src1)), (ls (R src2)); simpl; auto.
+    destruct (ls (R src1)), (ls (R src2)); simpl; auto.
+  }
   exploit IHmv; eauto. eapply subst_loc_pair_satisf_makelong; eauto.
+  destruct H3; InvBooleans. split; eauto using wt_setreg.
   intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto.
   econstructor. simpl; eauto. reflexivity. traceEq.
 + (* lowlong *)
+  assert (HT: Val.has_type (Val.loword (ls (R src))) (mreg_type dst)).
+  {
+    destruct H3. simpl in H5. InvBooleans.
+    destruct (mreg_type dst) eqn:T; simpl; auto; inversion H6;
+      destruct (ls (R src)); simpl; auto.
+  }
   exploit IHmv; eauto. eapply subst_loc_part_satisf_lowlong; eauto.
+  destruct H3; InvBooleans. split; eauto using wt_setreg.
   intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto.
   econstructor. simpl; eauto. reflexivity. traceEq.
 + (* highlong *)
+  assert (HT: Val.has_type (Val.hiword (ls (R src))) (mreg_type dst)).
+  {
+    destruct H3. simpl in H5. InvBooleans.
+    destruct (mreg_type dst) eqn:T; simpl; auto; inversion H6;
+      destruct (ls (R src)); simpl; auto.
+  }
   exploit IHmv; eauto. eapply subst_loc_part_satisf_highlong; eauto.
+  destruct H3; InvBooleans. split; eauto using wt_setreg.
   intros [ls' [A B]]. exists ls'; split; auto. eapply star_left; eauto.
   econstructor. simpl; eauto. reflexivity. traceEq.
 Qed.
@@ -1919,6 +2003,7 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa
            Val.lessdef v (Locmap.getpair (map_rpair R (loc_result sg)) ls1) ->
            Val.has_type v (env res) ->
            agree_callee_save ls ls1 ->
+           wt_locset ls1 ->
            exists ls2,
            star LTL.step tge (Block ts tf sp bb ls1 m)
                           E0 (State ts tf sp pc ls2 m)
@@ -1976,11 +2061,25 @@ Qed.
 
 Ltac UseShape :=
   match goal with
-  | [ WT: wt_function _ _, CODE: (RTL.fn_code _)!_ = Some _, EQ: transfer _ _ _ _ _ = OK _ |- _ ] =>
-      destruct (invert_code _ _ _ _ _ _ _ WT CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR & WTI);
+  | [ WT: wt_function _ _,
+      WTTF: LTLtyping.wt_function _ = true,
+      CODE: (RTL.fn_code _)!_ = Some _,
+      EQ: transfer _ _ _ _ _ = OK _ |- _ ] =>
+      destruct (invert_code _ _ _ _ _ _ _ WT WTTF CODE EQ) as (eafter & bsh & bb & AFTER & BSH & TCODE & EBS & TR & WTI);
       inv EBS; unfold transfer_aux in TR; MonadInv
   end.
 
+Ltac WellTypedBlock :=
+  match goal with
+  | [ T: (fn_code ?tf) ! _ = Some _ |- wt_bblock _ _ = true ] =>
+    apply wt_function_wt_bblock in T; auto;
+    unfold wt_bblock, expand_moves in *; WellTypedBlock
+  | [ T: forallb (LTLtyping.wt_instr _) (_ ++ _) = true |- forallb _ _ = true ] =>
+    rewrite forallb_app in T; simpl in T;
+    InvBooleans; eauto; WellTypedBlock
+  | _ => idtac
+  end.
+
 Remark addressing_not_long:
   forall env f addr args dst s r,
   wt_instr f env (Iload Mint64 addr args dst s) -> Archi.splitlong = true ->
@@ -1996,41 +2095,107 @@ Proof.
   red; intros; subst r. rewrite C in H8; discriminate.
 Qed.
 
+Lemma wt_transf_function:
+  forall (f: RTL.function) (tf: LTL.function),
+  transf_function f = OK tf ->
+  LTLtyping.wt_function tf = true.
+Proof.
+  intros. unfold transf_function in H.
+  destruct (type_function f); try congruence.
+  destruct (regalloc f); try congruence.
+  destruct (LTLtyping.wt_function f0) eqn:WT; try congruence.
+  monadInv H; auto.
+Qed.
+
+Lemma wt_transf_fundef:
+  forall (fd: RTL.fundef) (tfd: LTL.fundef),
+  transf_fundef fd = OK tfd ->
+  LTLtyping.wt_fundef tfd.
+Proof.
+  intros.
+  destruct fd, tfd; simpl in *; auto; try congruence.
+  monadInv H. simpl; eauto using wt_transf_function.
+Qed.
+
+Lemma wt_prog: wt_program prog.
+Proof.
+  red; intros.
+  exploit list_forall2_in_left. eexact (proj1 TRANSF). eauto.
+  intros ([i' gd] & A & B & C). simpl in *; subst i'.
+  inv C. destruct f; simpl in *.
+- monadInv H2.
+  unfold transf_function in EQ.
+  destruct (type_function f) as [env|] eqn:TF; try discriminate.
+  econstructor. eapply type_function_correct; eauto.
+- constructor.
+Qed.
+
+Corollary wt_tprog: LTLtyping.wt_program tprog.
+Proof.
+  generalize wt_prog; unfold wt_program; intros.
+  unfold LTLtyping.wt_program; intros.
+  unfold match_prog, match_program, match_program_gen in TRANSF.
+  decompose [and] TRANSF.
+  exploit list_forall2_in_right; eauto.
+  intros ([i' gd] & A & B & C).
+  inversion C. eapply wt_transf_fundef. eauto.
+Qed.
+
+Lemma star_step_type_preservation:
+  forall S1 t S2,
+  LTLtyping.wt_state S1 ->
+  star LTL.step tge S1 t S2 ->
+  LTLtyping.wt_state S2.
+Proof.
+  intros. induction H0; auto.
+  apply IHstar. eapply LTLtyping.step_type_preservation; eauto.
+  eapply wt_tprog.
+Qed.
+
 (** The proof of semantic preservation is a simulation argument of the
     "plus" kind. *)
 
 Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 -> wt_state S1 ->
-  forall S1', match_states S1 S1' ->
-  exists S2', plus LTL.step tge S1' t S2' /\ match_states S2 S2'.
+  forall S1', match_states S1 S1' -> LTLtyping.wt_state S1' ->
+  exists S2', plus LTL.step tge S1' t S2' /\ LTLtyping.wt_state S2' /\ match_states S2 S2'.
 Proof.
-  induction 1; intros WT S1' MS; inv MS; try UseShape.
+  induction 1; intros WT S1' MS WT'; inv MS;
+    try assert (WTTF: LTLtyping.wt_function tf = true) by (inversion WT'; auto);
+    inversion WT'; subst;
+    try UseShape.
 
 (* nop *)
-- exploit exec_moves; eauto. intros [ls1 [X Y]].
+- exploit exec_moves; eauto.
+  split; eauto using LTLtyping.wt_function_wt_bblock.
+  intros [ls1 [X [Y Z]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_right. eexact X. econstructor; eauto.
   eauto. traceEq.
   exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* op move *)
 - generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
   simpl in H0. inv H0.
-  exploit (exec_moves mv); eauto. intros [ls1 [X Y]].
+  exploit (exec_moves mv); eauto.
+  split; eauto using LTLtyping.wt_function_wt_bblock.
+  intros [ls1 [X [Y Z]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_right. eexact X. econstructor; eauto.
   eauto. traceEq.
   exploit satisf_successors; eauto. simpl; eauto. eapply subst_reg_satisf; eauto.
   intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* op makelong *)
 - generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
   simpl in H0. inv H0.
-  exploit (exec_moves mv); eauto. intros [ls1 [X Y]].
+  exploit (exec_moves mv); eauto.
+  split; eauto using LTLtyping.wt_function_wt_bblock.
+  intros [ls1 [X [Y Z]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_right. eexact X. econstructor; eauto.
@@ -2038,12 +2203,14 @@ Proof.
   exploit satisf_successors; eauto. simpl; eauto.
   eapply subst_reg_kind_satisf_makelong. eauto. eauto.
   intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* op lowlong *)
 - generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
   simpl in H0. inv H0.
-  exploit (exec_moves mv); eauto. intros [ls1 [X Y]].
+  exploit (exec_moves mv); eauto.
+  split; eauto using LTLtyping.wt_function_wt_bblock.
+  intros [ls1 [X [Y Z]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_right. eexact X. econstructor; eauto.
@@ -2051,12 +2218,14 @@ Proof.
   exploit satisf_successors; eauto. simpl; eauto.
   eapply subst_reg_kind_satisf_lowlong. eauto. eauto.
   intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* op highlong *)
 - generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
   simpl in H0. inv H0.
-  exploit (exec_moves mv); eauto. intros [ls1 [X Y]].
+  exploit (exec_moves mv); eauto.
+  split; eauto using LTLtyping.wt_function_wt_bblock.
+  intros [ls1 [X [Y Z]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_right. eexact X. econstructor; eauto.
@@ -2064,14 +2233,31 @@ Proof.
   exploit satisf_successors; eauto. simpl; eauto.
   eapply subst_reg_kind_satisf_highlong. eauto. eauto.
   intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* op regular *)
 - generalize (wt_exec_Iop _ _ _ _ _ _ _ _ _ _ _ WTI H0 WTRS). intros WTRS'.
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+  exploit (exec_moves mv1); eauto.
+  split; eauto using LTLtyping.wt_function_wt_bblock.
+  intros [ls1 [A1 [B1 C1]]].
   exploit transfer_use_def_satisf; eauto. intros [X Y].
   exploit eval_operation_lessdef; eauto. intros [v' [F G]].
-  exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]].
+  assert (RES_TYPE: Val.has_type v' (mreg_type res')).
+  {
+    generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB.
+    apply wt_bblock_expand_moves_head in WTBB.
+    simpl in WTBB.
+    destruct (is_move_operation op args') eqn:MOVE.
+    - apply is_move_operation_correct in MOVE. destruct MOVE; subst. simpl in *.
+      inversion F. eapply Val.has_subtype; eauto. apply B1.
+    - apply Val.has_subtype with (ty1 := snd (type_of_operation op)).
+      destruct (type_of_operation op); simpl; auto.
+      generalize (is_not_move_operation _ _ _ _ _ F MOVE); intros.
+      eapply type_of_operation_sound; eauto.
+  }
+  exploit (exec_moves mv2); eauto.
+  split. apply wt_setreg; auto. apply wt_undef_regs; auto. WellTypedBlock.
+  intros [ls2 [A2 [B2 C2]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_trans. eexact A1.
@@ -2079,11 +2265,14 @@ Proof.
   apply eval_operation_preserved. exact symbols_preserved.
   eauto. eapply star_right. eexact A2. constructor.
   eauto. eauto. eauto. traceEq.
-  exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
-  econstructor; eauto.
+  exploit satisf_successors; eauto. simpl; eauto.
+  intros [enext [U V]].
+  split; econstructor; eauto.
 
 (* op dead *)
-- exploit exec_moves; eauto. intros [ls1 [X Y]].
+- exploit exec_moves; eauto.
+  split; eauto using LTLtyping.wt_function_wt_bblock.
+  intros [ls1 [X [Y Z]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_right. eexact X. econstructor; eauto.
@@ -2091,16 +2280,29 @@ Proof.
   exploit satisf_successors. eauto. eauto. simpl; eauto. eauto.
   eapply reg_unconstrained_satisf; eauto.
   intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
   eapply wt_exec_Iop; eauto.
 
 (* load regular *)
 - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+  exploit (exec_moves mv1); eauto.
+  split; eauto using LTLtyping.wt_function_wt_bblock.
+  intros [ls1 [A1 [B1 C1]]].
   exploit transfer_use_def_satisf; eauto. intros [X Y].
   exploit eval_addressing_lessdef; eauto. intros [a' [F G]].
   exploit Mem.loadv_extends; eauto. intros [v' [P Q]].
-  exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]].
+  assert (DST_TYPE: Val.has_type v' (mreg_type dst')).
+  {
+    generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB.
+    apply wt_bblock_expand_moves_head in WTBB.
+    simpl in WTBB.
+    eapply Val.has_subtype; eauto.
+    unfold Mem.loadv in P; destruct a'; try inversion P.
+    eapply Mem.load_type; eauto.
+  }
+  exploit (exec_moves mv2); eauto.
+  split. apply wt_setreg; auto. WellTypedBlock.
+  intros [ls2 [A2 [B2 C2]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_trans. eexact A1.
@@ -2109,18 +2311,28 @@ Proof.
   eapply star_right. eexact A2. constructor.
   eauto. eauto. eauto. traceEq.
   exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* load pair *)
 - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
   exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+  exploit (exec_moves mv1); eauto.
+  split; eauto using LTLtyping.wt_function_wt_bblock.
+  intros [ls1 [A1 [B1 C1]]].
   assert (LD1: Val.lessdef_list rs##args (reglist ls1 args1')).
   { eapply add_equations_lessdef; eauto. }
   exploit eval_addressing_lessdef. eexact LD1. eauto. intros [a1' [F1 G1]].
   exploit Mem.loadv_extends. eauto. eexact LOAD1. eexact G1. intros (v1'' & LOAD1' & LD2).
+  assert (DST_TYPE1: Val.has_type v1'' (mreg_type dst1')).
+  {
+    generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB.
+    apply wt_bblock_expand_moves_head in WTBB.
+    unfold Mem.loadv in LOAD1'; destruct a1'; inversion LOAD1'.
+    eapply Val.has_subtype; eauto.
+    eapply Mem.load_type; eauto.
+  }
   set (ls2 := Locmap.set (R dst1') v1'' (undef_regs (destroyed_by_load Mint32 addr) ls1)).
   assert (SAT2: satisf (rs#dst <- v) ls2 e2).
   { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto.
@@ -2128,8 +2340,11 @@ Proof.
     eapply add_equations_satisf; eauto. assumption.
     rewrite Regmap.gss.
     apply Val.lessdef_trans with v1'; unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto.
+    auto.
   }
-  exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]].
+  exploit (exec_moves mv2); eauto.
+  split. apply wt_setreg; auto. WellTypedBlock.
+  intros [ls3 [A3 [B3 C3]]].
   assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')).
   { replace (rs##args) with ((rs#dst<-v)##args).
     eapply add_equations_lessdef; eauto.
@@ -2142,21 +2357,37 @@ Proof.
   assert (LOADX: exists v2'', Mem.loadv Mint32 m' a2' = Some v2'' /\ Val.lessdef v2' v2'').
   { discriminate || (eapply Mem.loadv_extends; [eauto|eexact LOAD2|eexact G2]). }
   destruct LOADX as (v2'' & LOAD2' & LD4).
+  assert (DST_TYPE2: Val.has_type v2'' (mreg_type dst2')).
+  {
+    generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB.
+    apply wt_bblock_expand_moves_cons in WTBB.
+    apply wt_bblock_expand_moves_head in WTBB.
+    unfold Mem.loadv in LOAD2'; destruct a2'; inversion LOAD2'.
+    eapply Val.has_subtype; eauto.
+    eapply Mem.load_type; eauto.
+  }
   set (ls4 := Locmap.set (R dst2') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls3)).
   assert (SAT4: satisf (rs#dst <- v) ls4 e0).
   { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto.
     eapply add_equations_satisf; eauto. assumption.
     rewrite Regmap.gss.
     apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto.
+    auto.
   }
-  exploit (exec_moves mv3); eauto. intros [ls5 [A5 B5]].
+  exploit (exec_moves mv3); eauto.
+  split. apply wt_setreg; auto.
+  apply wt_function_wt_bblock in TCODE; auto.
+  unfold wt_bblock, expand_moves in *. rewrite forallb_app in TCODE.
+  simpl in TCODE. InvBooleans. rewrite forallb_app in H5. simpl in H5. InvBooleans. eauto.
+  intros [ls5 [A5 [B5 C5]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_trans. eexact A1.
   eapply star_left. econstructor.
   instantiate (1 := a1'). rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved.
   eexact LOAD1'. instantiate (1 := ls2); auto.
-  eapply star_trans. eexact A3.
+  eapply star_trans.
+  eexact A3.
   eapply star_left. econstructor.
   instantiate (1 := a2'). rewrite <- F2. apply eval_addressing_preserved. exact symbols_preserved.
   eexact LOAD2'. instantiate (1 := ls4); auto.
@@ -2164,18 +2395,30 @@ Proof.
   constructor.
   eauto. eauto. eauto. eauto. eauto. traceEq.
   exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* load first word of a pair *)
 - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
   exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+  exploit (exec_moves mv1); eauto.
+  split. auto. apply wt_function_wt_bblock in TCODE; eauto.
+  intros [ls1 [A1 [B1 C1]]].
   assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')).
   { eapply add_equations_lessdef; eauto. }
   exploit eval_addressing_lessdef. eexact LD1. eauto. intros [a1' [F1 G1]].
   exploit Mem.loadv_extends. eauto. eexact LOAD1. eexact G1. intros (v1'' & LOAD1' & LD2).
+  assert (DST_TYPE: Val.has_type v1'' (mreg_type dst')).
+  {
+    generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB.
+    apply wt_bblock_expand_moves_head in WTBB. simpl in WTBB.
+    unfold Mem.loadv in LOAD1'; destruct a1'; try inversion LOAD1'.
+    apply Mem.load_type in LOAD1'.
+    destruct (mreg_type dst'); auto; try congruence.
+    apply Val.has_subtype with (ty1 := Tint); auto.
+    apply Val.has_subtype with (ty1 := Tint); auto.
+  }
   set (ls2 := Locmap.set (R dst') v1'' (undef_regs (destroyed_by_load Mint32 addr) ls1)).
   assert (SAT2: satisf (rs#dst <- v) ls2 e0).
   { eapply parallel_assignment_satisf; eauto.
@@ -2183,7 +2426,9 @@ Proof.
     unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto.
     eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto.
   }
-  exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]].
+  exploit (exec_moves mv2); eauto.
+  split. apply wt_setreg, wt_undef_regs; auto. WellTypedBlock.
+  intros [ls3 [A3 [B3 C3]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_trans. eexact A1.
@@ -2194,14 +2439,16 @@ Proof.
   constructor.
   eauto. eauto. eauto. traceEq.
   exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* load second word of a pair *)
 - generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
   exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+  exploit (exec_moves mv1); eauto.
+  split. auto. apply wt_function_wt_bblock in TCODE; eauto.
+  intros [ls1 [A1 [B1 C1]]].
   assert (LD1: Val.lessdef_list rs##args (reglist ls1 args')).
   { eapply add_equations_lessdef; eauto. }
   exploit eval_addressing_lessdef. eexact LD1.
@@ -2210,13 +2457,25 @@ Proof.
   assert (LOADX: exists v2'', Mem.loadv Mint32 m' a1' = Some v2'' /\ Val.lessdef v2' v2'').
   { discriminate || (eapply Mem.loadv_extends; [eauto|eexact LOAD2|eexact G1]). }
   destruct LOADX as (v2'' & LOAD2' & LD2).
+  assert (DST_TYPE: Val.has_type v2'' (mreg_type dst')).
+  {
+    generalize (LTLtyping.wt_function_wt_bblock tf pc _ WTTF TCODE); intro WTBB.
+    apply wt_bblock_expand_moves_head in WTBB. simpl in WTBB.
+    unfold Mem.loadv in LOAD2'; destruct a1'; try inversion LOAD2'.
+    apply Mem.load_type in LOAD2'.
+    destruct (mreg_type dst'); auto; try congruence.
+    apply Val.has_subtype with (ty1 := Tint); auto.
+    apply Val.has_subtype with (ty1 := Tint); auto.
+  }
   set (ls2 := Locmap.set (R dst') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls1)).
   assert (SAT2: satisf (rs#dst <- v) ls2 e0).
   { eapply parallel_assignment_satisf; eauto.
     apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto.
     eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto.
   }
-  exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]].
+  exploit (exec_moves mv2); eauto.
+  split. apply wt_setreg, wt_undef_regs; auto. WellTypedBlock.
+  intros [ls3 [A3 [B3 C3]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_trans. eexact A1.
@@ -2227,10 +2486,12 @@ Proof.
   constructor.
   eauto. eauto. eauto. traceEq.
   exploit satisf_successors; eauto. simpl; eauto. intros [enext [W Z]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* load dead *)
-- exploit exec_moves; eauto. intros [ls1 [X Y]].
+- exploit exec_moves; eauto.
+  split; auto. apply wt_function_wt_bblock in TCODE; eauto.
+  intros [ls1 [X [Y Z]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_right. eexact X. econstructor; eauto.
@@ -2238,11 +2499,14 @@ Proof.
   exploit satisf_successors. eauto. eauto. simpl; eauto. eauto.
   eapply reg_unconstrained_satisf; eauto.
   intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
   eapply wt_exec_Iload; eauto.
 
 (* store *)
-- exploit exec_moves; eauto. intros [ls1 [X Y]].
+- exploit exec_moves; eauto.
+  split; auto.
+  eapply wt_function_wt_bblock; eauto.
+  intros [ls1 [X [Y Z]]].
   exploit add_equations_lessdef; eauto. intros LD. simpl in LD. inv LD.
   exploit eval_addressing_lessdef; eauto. intros [a' [F G]].
   exploit Mem.storev_extends; eauto. intros [m'' [P Q]].
@@ -2254,7 +2518,7 @@ Proof.
   constructor. eauto. eauto. traceEq.
   exploit satisf_successors; eauto. simpl; eauto.
   eapply can_undef_satisf; eauto. eapply add_equations_satisf; eauto. intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* store 2 *)
 - assert (SF: Archi.ptr64 = false) by (apply Archi.splitlong_ptr32; auto).
@@ -2266,7 +2530,10 @@ Proof.
      with (sel_val kind_second_word rs#src)
        by (unfold kind_second_word; destruct Archi.big_endian; reflexivity).
   intros [m1 [STORE1 STORE2]].
-  exploit (exec_moves mv1); eauto. intros [ls1 [X Y]].
+  exploit (exec_moves mv1); eauto.
+  split; auto.
+  eapply wt_function_wt_bblock; eauto.
+  intros [ls1 [X [Z Y]]].
   exploit add_equations_lessdef. eexact Heqo1. eexact Y. intros LD1.
   exploit add_equation_lessdef. eapply add_equations_satisf. eexact Heqo1. eexact Y.
   simpl. intros LD2.
@@ -2279,7 +2546,9 @@ Proof.
     rewrite <- F1. apply eval_addressing_preserved. exact symbols_preserved.
   exploit Mem.storev_extends. eauto. eexact STORE1. eexact G1. eauto.
   intros [m1' [STORE1' EXT1]].
-  exploit (exec_moves mv2); eauto. intros [ls3 [U V]].
+  exploit (exec_moves mv2); eauto.
+  split; auto. WellTypedBlock.
+  intros [ls3 [U [W V]]].
   exploit add_equations_lessdef. eexact Heqo. eexact V. intros LD3.
   exploit add_equation_lessdef. eapply add_equations_satisf. eexact Heqo. eexact V.
   simpl. intros LD4.
@@ -2305,13 +2574,16 @@ Proof.
   eapply can_undef_satisf. eauto.
   eapply add_equation_satisf. eapply add_equations_satisf; eauto.
   intros [enext [P Q]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* call *)
 - set (sg := RTL.funsig fd) in *.
   set (args' := loc_arguments sg) in *.
   set (res' := loc_result sg) in *.
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+  exploit (exec_moves mv1); eauto.
+  split; auto.
+  eapply wt_function_wt_bblock; eauto.
+  intros [ls1 [A1 [B1 C1]]].
   exploit find_function_translated. eauto. eauto. eapply add_equations_args_satisf; eauto.
   intros [tfd [E F]].
   assert (SIG: funsig tfd = sg). eapply sig_function_translated; eauto.
@@ -2320,6 +2592,8 @@ Proof.
   eapply star_right. eexact A1. econstructor; eauto.
   eauto. traceEq.
   exploit analyze_successors; eauto. simpl. left; eauto. intros [enext [U V]].
+  split. apply wt_call_state; auto. constructor; auto. WellTypedBlock.
+  eauto using wt_transf_fundef.
   econstructor; eauto.
   econstructor; eauto.
   inv WTI. congruence.
@@ -2329,7 +2603,8 @@ Proof.
   eapply add_equations_args_satisf; eauto.
   congruence.
   apply wt_regset_assign; auto.
-  intros [ls2 [A2 B2]].
+  split; auto. WellTypedBlock.
+  intros [ls2 [A2 [B2 C2]]].
   exists ls2; split.
   eapply star_right. eexact A2. constructor. traceEq.
   apply satisf_incr with eafter; auto.
@@ -2342,7 +2617,10 @@ Proof.
 - set (sg := RTL.funsig fd) in *.
   set (args' := loc_arguments sg) in *.
   exploit Mem.free_parallel_extends; eauto. intros [m'' [P Q]].
-  exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
+  exploit (exec_moves mv); eauto.
+  split; auto.
+  eapply wt_function_wt_bblock; eauto.
+  intros [ls1 [A1 [B1 C1]]].
   exploit find_function_translated. eauto. eauto. eapply add_equations_args_satisf; eauto.
   intros [tfd [E F]].
   assert (SIG: funsig tfd = sg). eapply sig_function_translated; eauto.
@@ -2353,6 +2631,9 @@ Proof.
   replace (fn_stacksize tf) with (RTL.fn_stacksize f); eauto.
   destruct (transf_function_inv _ _ FUN); auto.
   eauto. traceEq.
+  split.
+  constructor. auto. eapply wt_transf_fundef; eauto.
+  auto using wt_return_regs, wt_parent_locset.
   econstructor; eauto.
   eapply match_stackframes_change_sig; eauto. rewrite SIG. rewrite e0. decEq.
   destruct (transf_function_inv _ _ FUN); auto.
@@ -2362,15 +2643,35 @@ Proof.
   rewrite SIG. inv WTI. rewrite <- H6. apply wt_regset_list; auto.
 
 (* builtin *)
-- exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+- exploit (exec_moves mv1); eauto.
+  split; auto.
+  eapply wt_function_wt_bblock; eauto.
+  intros [ls1 [A1 [B1 C1]]].
   exploit add_equations_builtin_eval; eauto.
   intros (C & vargs' & vres' & m'' & D & E & F & G).
   assert (WTRS': wt_regset env (regmap_setres res vres rs)) by (eapply wt_exec_Ibuiltin; eauto).
+  assert (WTBR: wt_builtin_res (proj_sig_res (ef_sig ef)) res' = true).
+  {
+    apply wt_function_wt_bblock in TCODE; auto.
+    unfold wt_bblock, expand_moves in *. rewrite forallb_app in TCODE.
+    simpl in TCODE. InvBooleans. auto.
+  }
+  exploit external_call_well_typed; eauto; intros.
   set (ls2 := Locmap.setres res' vres' (undef_regs (destroyed_by_builtin ef) ls1)).
   assert (satisf (regmap_setres res vres rs) ls2 e0).
   { eapply parallel_set_builtin_res_satisf; eauto.
-    eapply can_undef_satisf; eauto. }
-  exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]].
+    eapply can_undef_satisf; eauto.
+    unfold Val.has_type_builtin_res; unfold wt_builtin_res in WTBR.
+    destruct res'; try eapply Val.has_subtype; eauto.
+    InvBooleans. split.
+    eapply Val.has_subtype; eauto. destruct vres'; simpl; eauto.
+    eapply Val.has_subtype; eauto. destruct vres'; simpl; eauto.
+  }
+  exploit (exec_moves mv2); eauto.
+  split; auto.
+  apply wt_setres with (ty := proj_sig_res (ef_sig ef)); auto.
+  apply wt_undef_regs; auto. WellTypedBlock.
+  intros [ls3 [A3 [B3 C3]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_trans. eexact A1.
@@ -2383,10 +2684,13 @@ Proof.
   reflexivity. reflexivity. reflexivity. traceEq.
   exploit satisf_successors; eauto. simpl; eauto.
   intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* cond *)
-- exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
+- exploit (exec_moves mv); eauto.
+  split; auto.
+  eapply wt_function_wt_bblock; eauto.
+  intros [ls1 [A1 [B1 C1]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_right. eexact A1.
@@ -2396,10 +2700,13 @@ Proof.
   instantiate (1 := if b then ifso else ifnot). simpl. destruct b; auto.
   eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto.
   intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* jumptable *)
-- exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
+- exploit (exec_moves mv); eauto.
+  split; auto.
+  eapply wt_function_wt_bblock; eauto.
+  intros [ls1 [A1 [B1 C1]]].
   assert (Val.lessdef (Vint n) (ls1 (R arg'))).
     rewrite <- H0. eapply add_equation_lessdef with (q := Eq Full arg (R arg')); eauto.
   inv H2.
@@ -2411,28 +2718,38 @@ Proof.
   instantiate (1 := pc'). simpl. eapply list_nth_z_in; eauto.
   eapply can_undef_satisf. eauto. eapply add_equation_satisf; eauto.
   intros [enext [U V]].
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* return *)
 - destruct (transf_function_inv _ _ FUN).
   exploit Mem.free_parallel_extends; eauto. rewrite H10. intros [m'' [P Q]].
   inv WTI; MonadInv.
 + (* without an argument *)
-  exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
+  exploit (exec_moves mv); eauto.
+  split; auto.
+  eapply wt_function_wt_bblock; eauto.
+  intros [ls1 [A1 [B1 C1]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_right. eexact A1.
   econstructor. eauto. eauto. traceEq.
-  simpl. econstructor; eauto.
+  simpl. split. econstructor; eauto.
+  auto using wt_return_regs, wt_parent_locset.
+  econstructor; eauto.
   apply return_regs_agree_callee_save.
   constructor.
 + (* with an argument *)
-  exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
+  exploit (exec_moves mv); eauto.
+  split; auto.
+  eapply wt_function_wt_bblock; eauto.
+  intros [ls1 [A1 [B1 C1]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_right. eexact A1.
   econstructor. eauto. eauto. traceEq.
-  simpl. econstructor; eauto. rewrite <- H11.
+  simpl. split. econstructor; eauto.
+  auto using wt_return_regs, wt_parent_locset.
+  econstructor; eauto. rewrite <- H11.
   replace (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f)))
                           (return_regs (parent_locset ts) ls1))
   with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1).
@@ -2456,14 +2773,16 @@ Proof.
     eapply can_undef_satisf; eauto. eapply compat_entry_satisf; eauto.
     rewrite call_regs_param_values. eexact ARGS.
     exact WTRS.
-  intros [ls1 [A B]].
+  split. apply wt_undef_regs, wt_call_regs. auto.
+  eapply wt_function_wt_bblock; eauto.
+  intros [ls1 [A [B C]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
   eapply star_left. econstructor; eauto.
   eapply star_right. eexact A.
   econstructor; eauto.
   eauto. eauto. traceEq.
-  econstructor; eauto.
+  split; econstructor; eauto.
 
 (* external function *)
 - exploit external_call_mem_extends; eauto. intros [v' [m'' [F [G [J K]]]]].
@@ -2471,13 +2790,29 @@ Proof.
   econstructor; split.
   apply plus_one. econstructor; eauto.
   eapply external_call_symbols_preserved with (ge1 := ge); eauto. apply senv_preserved.
+  exploit external_call_well_typed; eauto; intro WTRES.
+  split. econstructor; eauto.
+  apply wt_setpair; auto.
+
   econstructor; eauto.
   simpl. destruct (loc_result (ef_sig ef)) eqn:RES; simpl.
   rewrite Locmap.gss; auto.
+  generalize (loc_result_type (ef_sig ef)); intro SUBTYP.
+  rewrite RES in SUBTYP; simpl in SUBTYP.
+  exploit Val.has_subtype; eauto; intros.
+  rewrite pred_dec_true; auto.
+
   generalize (loc_result_pair (ef_sig ef)); rewrite RES; intros (A & B & C & D & E).
   exploit external_call_well_typed; eauto. unfold proj_sig_res; rewrite B. intros WTRES'.
   rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss.
+
+  generalize (loc_result_type (ef_sig ef)); intro SUBTYP.
+  rewrite RES in SUBTYP; simpl in SUBTYP.
+  rewrite !pred_dec_true.
   rewrite val_longofwords_eq_1 by auto. auto.
+  eapply Val.has_subtype; eauto. destruct v'; simpl; auto.
+  eapply Val.has_subtype; eauto. destruct v'; simpl; auto.
+
   red; intros. rewrite (AG l H0).
   symmetry; apply Locmap.gpo.
   assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)).
@@ -2490,6 +2825,9 @@ Proof.
   exploit STEPS; eauto. rewrite WTRES0; auto. intros [ls2 [A B]].
   econstructor; split.
   eapply plus_left. constructor. eexact A. traceEq.
+  split.
+  apply star_step_type_preservation in A; eauto.
+  inversion WTSTK. econstructor; eauto.
   econstructor; eauto.
   apply wt_regset_assign; auto. rewrite WTRES0; auto.
 Qed.
@@ -2524,30 +2862,19 @@ Proof.
   rewrite H; auto.
 Qed.
 
-Lemma wt_prog: wt_program prog.
-Proof.
-  red; intros.
-  exploit list_forall2_in_left. eexact (proj1 TRANSF). eauto.
-  intros ([i' gd] & A & B & C). simpl in *; subst i'.
-  inv C. destruct f; simpl in *.
-- monadInv H2.
-  unfold transf_function in EQ.
-  destruct (type_function f) as [env|] eqn:TF; try discriminate.
-  econstructor. eapply type_function_correct; eauto.
-- constructor.
-Qed.
-
 Theorem transf_program_correct:
   forward_simulation (RTL.semantics prog) (LTL.semantics tprog).
 Proof.
-  set (ms := fun s s' => wt_state s /\ match_states s s').
+  set (ms := fun s s' => wt_state s /\ LTLtyping.wt_state s' /\ match_states s s').
   eapply forward_simulation_plus with (match_states := ms).
 - apply senv_preserved.
 - intros. exploit initial_states_simulation; eauto. intros [st2 [A B]].
   exists st2; split; auto. split; auto.
   apply wt_initial_state with (p := prog); auto. exact wt_prog.
-- intros. destruct H. eapply final_states_simulation; eauto.
-- intros. destruct H0.
+  split; auto.
+  apply LTLtyping.wt_initial_state with (prog := tprog); auto. exact wt_tprog.
+- intros. destruct H as [H1 [H2 H3]]. eapply final_states_simulation; eauto.
+- intros. destruct H0 as [H1 [H2 H3]].
   exploit step_simulation; eauto. intros [s2' [A B]].
   exists s2'; split. exact A. split.
   eapply subject_reduction; eauto. eexact wt_prog. eexact H.
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index bee0ded470..bd4010dbcb 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -95,6 +95,17 @@ Definition wt_function (f: function) : bool :=
   let bs := map snd (Maps.PTree.elements f.(fn_code)) in
   forallb (wt_bblock f) bs.
 
+Lemma wt_function_wt_bblock:
+  forall f pc b,
+  wt_function f = true ->
+  Maps.PTree.get pc (fn_code f) = Some b ->
+  wt_bblock f b = true.
+Proof.
+  intros. apply Maps.PTree.elements_correct in H0.
+  unfold wt_function, wt_bblock in *. eapply forallb_forall in H; eauto.
+  change b with (snd (pc, b)). apply in_map; auto.
+Qed.
+
 (** Typing the run-time state. *)
 
 Definition wt_locset (ls: locset) : Prop :=
@@ -107,7 +118,7 @@ Proof.
   intros; red; intros.
   unfold Locmap.set.
   destruct (Loc.eq (R r) l).
-  subst l; auto.
+  subst l; rewrite pred_dec_true; auto.
   destruct (Loc.diff_dec (R r) l). auto. red. auto.
 Qed.
 
@@ -195,6 +206,9 @@ Definition wt_fundef (fd: fundef) :=
   | External ef => True
   end.
 
+Definition wt_program (prog: program): Prop :=
+  forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd.
+
 Inductive wt_callstack: list stackframe -> Prop :=
   | wt_callstack_nil:
       wt_callstack nil
@@ -202,7 +216,7 @@ Inductive wt_callstack: list stackframe -> Prop :=
         (WTSTK: wt_callstack s)
         (WTF: wt_function f = true)
         (WTB: wt_bblock f b = true)
-        (WTRS: wt_locset rs),
+        (WTLS: wt_locset rs),
       wt_callstack (Stackframe f sp rs b :: s).
 
 Lemma wt_parent_locset:
@@ -217,22 +231,22 @@ Inductive wt_state: state -> Prop :=
   | wt_branch_state: forall s f sp n rs m
         (WTSTK: wt_callstack s )
         (WTF: wt_function f = true)
-        (WTRS: wt_locset rs),
+        (WTLS: wt_locset rs),
       wt_state (State s f sp n rs m)
   | wt_regular_state: forall s f sp b rs m
         (WTSTK: wt_callstack s )
         (WTF: wt_function f = true)
         (WTB: wt_bblock f b = true)
-        (WTRS: wt_locset rs),
+        (WTLS: wt_locset rs),
       wt_state (Block s f sp b rs m)
   | wt_call_state: forall s fd rs m
         (WTSTK: wt_callstack s)
         (WTFD: wt_fundef fd)
-        (WTRS: wt_locset rs),
+        (WTLS: wt_locset rs),
       wt_state (Callstate s fd rs m)
   | wt_return_state: forall s rs m
         (WTSTK: wt_callstack s)
-        (WTRS: wt_locset rs),
+        (WTLS: wt_locset rs),
       wt_state (Returnstate s rs m).
 
 (** Preservation of state typing by transitions *)
@@ -242,8 +256,7 @@ Section SOUNDNESS.
 Variable prog: program.
 Let ge := Genv.globalenv prog.
 
-Hypothesis wt_prog:
-  forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd.
+Hypothesis wt_prog: wt_program prog.
 
 Lemma wt_find_function:
   forall ros rs f, find_function ge ros rs = Some f -> wt_fundef f.
@@ -274,7 +287,7 @@ Local Opaque mreg_type.
   + (* move *)
     InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst.
     simpl in H. inv H.
-    econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. apply WTRS.
+    econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. apply WTLS.
     apply wt_undef_regs; auto.
   + (* other ops *)
     destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans.
@@ -293,7 +306,7 @@ Local Opaque mreg_type.
 - (* getstack *)
   simpl in *; InvBooleans.
   econstructor; eauto.
-  eapply wt_setreg; eauto. eapply Val.has_subtype; eauto. apply WTRS.
+  eapply wt_setreg; eauto. eapply Val.has_subtype; eauto. apply WTLS.
   apply wt_undef_regs; auto.
 - (* setstack *)
   simpl in *; InvBooleans.
@@ -388,5 +401,5 @@ Lemma wt_callstate_wt_regs:
   wt_state (Callstate s f rs m) ->
   forall r, Val.has_type (rs (R r)) (mreg_type r).
 Proof.
-  intros. inv H. apply WTRS.
+  intros. inv H. apply WTLS.
 Qed.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index bd232be31f..1d2bffe38e 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -107,7 +107,7 @@ Proof.
   intros; red; intros.
   unfold Locmap.set.
   destruct (Loc.eq (R r) l).
-  subst l; auto.
+  subst l; rewrite pred_dec_true; auto.
   destruct (Loc.diff_dec (R r) l). auto. red. auto.
 Qed.
 
diff --git a/backend/Locations.v b/backend/Locations.v
index c2cb66d98b..b271fed1a1 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -331,26 +331,33 @@ Module Locmap.
   Definition set (l: loc) (v: val) (m: t) : t :=
     fun (p: loc) =>
       if Loc.eq l p then
-        match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end
+        match l with
+        | R r => if Val.has_type_dec v (mreg_type r) then v else Vundef
+        | S sl ofs ty => Val.load_result (chunk_of_type ty) v
+        end
       else if Loc.diff_dec l p then
         m p
       else Vundef.
 
   Lemma gss: forall l v m,
     (set l v m) l =
-    match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end.
+    match l with
+    | R r => if Val.has_type_dec v (mreg_type r) then v else Vundef
+    | S sl ofs ty => Val.load_result (chunk_of_type ty) v
+    end.
   Proof.
     intros. unfold set. apply dec_eq_true.
   Qed.
 
-  Lemma gss_reg: forall r v m, (set (R r) v m) (R r) = v.
+  Lemma gss_reg: forall r v m, Val.has_type v (mreg_type r) -> (set (R r) v m) (R r) = v.
   Proof.
-    intros. unfold set. rewrite dec_eq_true. auto.
+    intros. unfold set. rewrite dec_eq_true, pred_dec_true; auto.
   Qed.
 
   Lemma gss_typed: forall l v m, Val.has_type v (Loc.type l) -> (set l v m) l = v.
   Proof.
-    intros. rewrite gss. destruct l. auto. apply Val.load_result_same; auto.
+    intros. rewrite gss. destruct l.
+    rewrite pred_dec_true; auto. apply Val.load_result_same; auto.
   Qed.
 
   Lemma gso: forall l v m p, Loc.diff l p -> (set l v m) p = m p.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index dd4a4e1d3e..e09eff5fe6 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -610,11 +610,12 @@ Lemma agree_regs_set_reg:
   forall j ls rs r v v',
   agree_regs j ls rs ->
   Val.inject j v v' ->
+  Val.has_type v (mreg_type r) ->
   agree_regs j (Locmap.set (R r) v ls) (Regmap.set r v' rs).
 Proof.
   intros; red; intros.
   unfold Regmap.set. destruct (RegEq.eq r0 r). subst r0.
-  rewrite Locmap.gss; auto.
+  rewrite Locmap.gss, pred_dec_true; auto.
   rewrite Locmap.gso; auto. red. auto.
 Qed.
 
@@ -622,11 +623,12 @@ Lemma agree_regs_set_pair:
   forall j p v v' ls rs,
   agree_regs j ls rs ->
   Val.inject j v v' ->
+  Val.has_type_rpair v p Val.loword Val.hiword mreg_type ->
   agree_regs j (Locmap.setpair p v ls) (set_pair p v' rs).
 Proof.
-  intros. destruct p; simpl.
+  intros. destruct p; try destruct H1; simpl.
 - apply agree_regs_set_reg; auto.
-- apply agree_regs_set_reg. apply agree_regs_set_reg; auto.
+- apply agree_regs_set_reg; auto. apply agree_regs_set_reg; auto.
   apply Val.hiword_inject; auto. apply Val.loword_inject; auto.
 Qed.
 
@@ -634,12 +636,13 @@ Lemma agree_regs_set_res:
   forall j res v v' ls rs,
   agree_regs j ls rs ->
   Val.inject j v v' ->
+  Val.has_type_builtin_res v res Val.loword Val.hiword mreg_type ->
   agree_regs j (Locmap.setres res v ls) (set_res res v' rs).
 Proof.
-  induction res; simpl; intros.
+  destruct res eqn:RES; simpl; intros.
 - apply agree_regs_set_reg; auto.
 - auto.
-- repeat apply agree_regs_set_reg; auto.
+- repeat apply agree_regs_set_reg; try tauto.
   apply Val.hiword_inject; auto.
   apply Val.loword_inject; auto.
 Qed.
@@ -664,6 +667,7 @@ Proof.
   induction rl; simpl; intros.
   auto.
   apply agree_regs_set_reg; auto.
+  simpl; auto.
 Qed.
 
 (** Preservation under assignment of stack slot *)
@@ -1019,7 +1023,7 @@ Remark undef_regs_type:
 Proof.
   induction rl; simpl; intros.
 - auto.
-- unfold Locmap.set. destruct (Loc.eq (R a) l). red; auto.
+- unfold Locmap.set. destruct (Loc.eq (R a) l). simpl; auto.
   destruct (Loc.diff_dec (R a) l); auto. red; auto.
 Qed.
 
@@ -1855,6 +1859,8 @@ Proof.
   apply plus_one. apply exec_Mgetstack. exact A.
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg; auto.
+  inversion WTS; subst. simpl in WTC; InvBooleans.
+  apply Val.has_subtype with (ty1 := ty); auto. apply WTRS.
   apply agree_locs_set_reg; auto.
 + (* Lgetstack, incoming *)
   unfold slot_valid in SV. InvBooleans.
@@ -1872,8 +1878,10 @@ Proof.
   rewrite (unfold_transf_function _ _ TRANSL). unfold fn_link_ofs.
   eapply frame_get_parent. eexact SEP.
   econstructor; eauto with coqlib. econstructor; eauto.
-  apply agree_regs_set_reg. apply agree_regs_set_reg. auto. auto.
+  apply agree_regs_set_reg. apply agree_regs_set_reg. auto. auto. simpl; auto.
   erewrite agree_incoming by eauto. exact B.
+  inversion WTS; subst. simpl in WTC; InvBooleans.
+  apply Val.has_subtype with (ty1 := ty); auto. apply WTRS.
   apply agree_locs_set_reg; auto. apply agree_locs_undef_locs; auto.
 + (* Lgetstack, outgoing *)
   exploit frame_get_outgoing; eauto. intros (v & A & B).
@@ -1881,6 +1889,8 @@ Proof.
   apply plus_one. apply exec_Mgetstack. exact A.
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg; auto.
+  inversion WTS; subst. simpl in WTC; InvBooleans.
+  apply Val.has_subtype with (ty1 := ty); auto. apply WTRS.
   apply agree_locs_set_reg; auto.
 
 - (* Lsetstack *)
@@ -1926,6 +1936,16 @@ Proof.
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg; auto.
   rewrite transl_destroyed_by_op.  apply agree_regs_undef_regs; auto.
+  inversion WTS; subst. simpl in WTC; InvBooleans.
+  destruct (is_move_operation op args) eqn:MOVE.
+    apply is_move_operation_correct in MOVE; destruct MOVE. subst.
+    simpl in H; inv H.
+    apply Val.has_subtype with (ty1 := mreg_type m0); auto. apply WTRS.
+    generalize (is_not_move_operation ge _ _ args m H MOVE); intros.
+    assert (subtype (snd (type_of_operation op)) (mreg_type res) = true).
+    { rewrite <- H0. destruct (type_of_operation op); reflexivity. }
+    assert (Val.has_type v (snd (type_of_operation op))) by eauto using type_of_operation_sound.
+    apply Val.has_subtype with (ty1 := snd (type_of_operation op)); auto.
   apply agree_locs_set_reg; auto. apply agree_locs_undef_locs. auto. apply destroyed_by_op_caller_save.
   apply frame_set_reg. apply frame_undef_regs. exact SEP.
 
@@ -1947,6 +1967,10 @@ Proof.
   eexact C. eauto.
   econstructor; eauto with coqlib.
   apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto.
+  inversion WTS; subst. simpl in WTC; InvBooleans.
+  destruct a'; try inversion C. apply Mem.load_type in H4.
+  apply Val.has_subtype with (ty1 := type_of_chunk chunk); auto.
+  destruct D; auto. simpl; auto.
   apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto.
 
 - (* Lstore *)
@@ -2020,7 +2044,16 @@ Proof.
   eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   eapply match_states_intro with (j := j'); eauto with coqlib.
   eapply match_stacks_change_meminj; eauto.
-  apply agree_regs_set_res; auto. apply agree_regs_undef_regs; auto. eapply agree_regs_inject_incr; eauto.
+  eapply agree_regs_set_res; eauto. apply agree_regs_undef_regs; auto. eapply agree_regs_inject_incr; eauto.
+  inversion WTS; subst. simpl in WTC; InvBooleans.
+  unfold wt_builtin_res in H3.
+  unfold Val.has_type_builtin_res.
+  apply external_call_well_typed in H0.
+  destruct res; auto.
+    eapply Val.has_subtype; eauto.
+    InvBooleans; split.
+    eapply Val.has_subtype; eauto. destruct vres; auto; constructor.
+    eapply Val.has_subtype; eauto. destruct vres; auto; constructor.
   apply agree_locs_set_res; auto. apply agree_locs_undef_regs; auto.
   apply frame_set_res. apply frame_undef_regs. apply frame_contents_incr with j; auto.
   rewrite sep_swap2. apply stack_contents_change_meminj with j; auto. rewrite sep_swap2.
@@ -2114,6 +2147,13 @@ Proof.
   eapply match_states_return with (j := j').
   eapply match_stacks_change_meminj; eauto.
   apply agree_regs_set_pair. apply agree_regs_inject_incr with j; auto. auto.
+  inversion WTS; subst.
+  apply external_call_well_typed in H0.
+  unfold Val.has_type_rpair, loc_result, proj_sig_res in *.
+  destruct (ef_sig ef) eqn:RES; simpl.
+  destruct sig_res; simpl in *.
+  destruct t0, res, Archi.big_endian; auto.
+  destruct res; auto.
   apply agree_callee_save_set_result; auto.
   apply stack_contents_change_meminj with j; auto.
   rewrite sep_comm, sep_assoc; auto.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index c6644cebb1..8595539ff5 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -262,7 +262,9 @@ Lemma locmap_set_lessdef:
   locmap_lessdef ls1 ls2 -> Val.lessdef v1 v2 -> locmap_lessdef (Locmap.set l v1 ls1) (Locmap.set l v2 ls2).
 Proof.
   intros; red; intros l'. unfold Locmap.set. destruct (Loc.eq l l').
-- destruct l; auto using Val.load_result_lessdef.
+- destruct l.
+  + destruct H0. destruct (Val.has_type_dec v (mreg_type r)); auto. auto.
+  + auto using Val.load_result_lessdef.
 - destruct (Loc.diff_dec l l'); auto.
 Qed.
 
diff --git a/common/Values.v b/common/Values.v
index 802d827b44..ef643389cb 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -89,6 +89,19 @@ Definition has_type (v: val) (t: typ) : Prop :=
   | _, _ => False
   end.
 
+Definition has_type_rpair {A} (v: val) (p: rpair A) (lof hif: val -> val) (tf: A -> typ) : Prop :=
+  match p with
+  | One r => has_type v (tf r)
+  | Twolong hi lo => has_type (lof v) (tf lo) /\ has_type (hif v) (tf hi)
+  end.
+
+Definition has_type_builtin_res {A} (v: val) (r: builtin_res A) (lof hif: val -> val) (tf: A -> typ) : Prop :=
+  match r with
+  | BR_none => True
+  | BR r => has_type v (tf r)
+  | BR_splitlong hi lo => has_type (lof v) (tf lo) /\ has_type (hif v) (tf hi)
+  end.
+
 Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop :=
   match vl, tl with
   | nil, nil => True
@@ -132,6 +145,35 @@ Proof.
   simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto.
 Qed.
 
+Definition has_type_b (v: val) (t: typ) : bool :=
+  match v, t with
+  | Vundef, _ => true
+  | Vint _, Tint => true
+  | Vlong _, Tlong => true
+  | Vfloat _, Tfloat => true
+  | Vsingle _, Tsingle => true
+  | Vptr _ _, Tint => negb Archi.ptr64
+  | Vptr _ _, Tlong => Archi.ptr64
+  | (Vint _ | Vsingle _), Tany32 => true
+  | Vptr _ _, Tany32 => negb Archi.ptr64
+  | _, Tany64 => true
+  | _, _ => false
+  end.
+
+Program Definition has_type_dec (v: val) (t: typ) : {has_type v t} + {~ has_type v t} :=
+  match has_type_b v t with
+  | true => left _
+  | false => right _
+  end.
+Next Obligation.
+  destruct v, t; simpl in *; auto; congruence.
+Qed.
+Next Obligation.
+  destruct v, t; simpl in *; auto; try congruence.
+  apply eq_sym, negb_false_iff in Heq_anonymous. congruence.
+  apply eq_sym, negb_false_iff in Heq_anonymous. congruence.
+Qed.
+
 (** Truth values.  Non-zero integers are treated as [True].
   The integer 0 (also used to represent the null pointer) is [False].
   Other values are neither true nor false. *)
diff --git a/powerpc/Op.v b/powerpc/Op.v
index e6f942c1fd..d3bd30ac9e 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -602,6 +602,17 @@ Proof.
   intros; discriminate.
 Qed.
 
+Lemma is_not_move_operation:
+  forall (F V A: Type) (genv: Genv.t F V) (sp: val)
+         (op: operation) (f: A -> val) (args: list A) (m: mem) (v: val),
+  eval_operation genv sp op (map f args) m = Some v ->
+  is_move_operation op args = None ->
+  op <> Omove.
+Proof.
+  intros. destruct (eq_operation op Omove); auto.
+  subst. destruct args; try destruct args; simpl in *; congruence.
+Qed.
+
 (** [negate_condition cond] returns a condition that is logically
   equivalent to the negation of [cond]. *)
 
diff --git a/riscV/Op.v b/riscV/Op.v
index bb04f78641..7c401cec01 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -691,6 +691,17 @@ Proof.
   intros; discriminate.
 Qed.
 
+Lemma is_not_move_operation:
+  forall (F V A: Type) (genv: Genv.t F V) (sp: val)
+         (op: operation) (f: A -> val) (args: list A) (m: mem) (v: val),
+  eval_operation genv sp op (map f args) m = Some v ->
+  is_move_operation op args = None ->
+  op <> Omove.
+Proof.
+  intros. destruct (eq_operation op Omove); auto.
+  subst. destruct args; try destruct args; simpl in *; congruence.
+Qed.
+
 (** [negate_condition cond] returns a condition that is logically
   equivalent to the negation of [cond]. *)
 
diff --git a/x86/Op.v b/x86/Op.v
index 02b0457493..b37e37d739 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -746,6 +746,17 @@ Proof.
   intros; discriminate.
 Qed.
 
+Lemma is_not_move_operation:
+  forall (F V A: Type) (genv: Genv.t F V) (sp: val)
+         (op: operation) (f: A -> val) (args: list A) (m: mem) (v: val),
+  eval_operation genv sp op (map f args) m = Some v ->
+  is_move_operation op args = None ->
+  op <> Omove.
+Proof.
+  intros. destruct (eq_operation op Omove); auto.
+  subst. destruct args; try destruct args; simpl in *; congruence.
+Qed.
+
 (** [negate_condition cond] returns a condition that is logically
   equivalent to the negation of [cond]. *)
 

From bfddee5c2211a0cd2fe879ef42e6c5346b086b93 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gerg=C3=B6=20Barany?= <gergo.barany@inria.fr>
Date: Wed, 30 Aug 2017 17:51:54 +0200
Subject: [PATCH 4/5] Adapt LTL typing proof for all architectures

---
 arm/Conventions1.v      | 12 ++++++++++++
 backend/Allocproof.v    | 25 +++++++++++--------------
 backend/LTLtyping.v     |  4 ++--
 backend/Stackingproof.v |  9 ++-------
 common/Values.v         |  2 +-
 powerpc/Conventions1.v  | 17 +++++++++++++++++
 riscV/Conventions1.v    | 13 ++++++++++++-
 x86/Conventions1.v      | 13 ++++++++++++-
 8 files changed, 69 insertions(+), 26 deletions(-)

diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index c5277e8dca..71ece2d6d5 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -16,6 +16,7 @@
 Require Import Coqlib.
 Require Import Decidableplus.
 Require Import AST.
+Require Import Values.
 Require Import Events.
 Require Import Locations.
 Require Archi.
@@ -122,6 +123,17 @@ Proof.
   intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; destruct Archi.big_endian; auto.
 Qed.
 
+Lemma loc_result_has_type:
+  forall res sig,
+  Val.has_type res (proj_sig_res sig) ->
+  Val.has_type_rpair res (loc_result sig) Val.loword Val.hiword mreg_type.
+Proof.
+  intros. unfold Val.has_type_rpair, loc_result, proj_sig_res in *.
+  destruct sig; simpl. destruct sig_res; simpl in H.
+  destruct t, res, Archi.big_endian; simpl; auto.
+  destruct res; simpl; auto.
+Qed.
+
 (** The result locations are caller-save registers *)
 
 Lemma loc_result_caller_save:
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index d3ac289529..df08196840 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -2072,11 +2072,11 @@ Ltac UseShape :=
 Ltac WellTypedBlock :=
   match goal with
   | [ T: (fn_code ?tf) ! _ = Some _ |- wt_bblock _ _ = true ] =>
-    apply wt_function_wt_bblock in T; auto;
-    unfold wt_bblock, expand_moves in *; WellTypedBlock
+    apply wt_function_wt_bblock in T; try eassumption;
+    unfold wt_bblock, expand_moves in *; try eassumption; WellTypedBlock
   | [ T: forallb (LTLtyping.wt_instr _) (_ ++ _) = true |- forallb _ _ = true ] =>
     rewrite forallb_app in T; simpl in T;
-    InvBooleans; eauto; WellTypedBlock
+    InvBooleans; try eassumption; WellTypedBlock
   | _ => idtac
   end.
 
@@ -2301,7 +2301,7 @@ Proof.
     eapply Mem.load_type; eauto.
   }
   exploit (exec_moves mv2); eauto.
-  split. apply wt_setreg; auto. WellTypedBlock.
+  split. apply wt_setreg; auto using wt_undef_regs. WellTypedBlock.
   intros [ls2 [A2 [B2 C2]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
@@ -2343,7 +2343,7 @@ Proof.
     auto.
   }
   exploit (exec_moves mv2); eauto.
-  split. apply wt_setreg; auto. WellTypedBlock.
+  split. apply wt_setreg; auto using wt_undef_regs. WellTypedBlock.
   intros [ls3 [A3 [B3 C3]]].
   assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')).
   { replace (rs##args) with ((rs#dst<-v)##args).
@@ -2375,10 +2375,7 @@ Proof.
     auto.
   }
   exploit (exec_moves mv3); eauto.
-  split. apply wt_setreg; auto.
-  apply wt_function_wt_bblock in TCODE; auto.
-  unfold wt_bblock, expand_moves in *. rewrite forallb_app in TCODE.
-  simpl in TCODE. InvBooleans. rewrite forallb_app in H5. simpl in H5. InvBooleans. eauto.
+  split. apply wt_setreg; auto using wt_undef_regs. WellTypedBlock.
   intros [ls5 [A5 [B5 C5]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto.
@@ -2518,7 +2515,7 @@ Proof.
   constructor. eauto. eauto. traceEq.
   exploit satisf_successors; eauto. simpl; eauto.
   eapply can_undef_satisf; eauto. eapply add_equations_satisf; eauto. intros [enext [U V]].
-  split; econstructor; eauto.
+  split; econstructor; eauto using wt_undef_regs.
 
 (* store 2 *)
 - assert (SF: Archi.ptr64 = false) by (apply Archi.splitlong_ptr32; auto).
@@ -2547,7 +2544,7 @@ Proof.
   exploit Mem.storev_extends. eauto. eexact STORE1. eexact G1. eauto.
   intros [m1' [STORE1' EXT1]].
   exploit (exec_moves mv2); eauto.
-  split; auto. WellTypedBlock.
+  split; try apply wt_undef_regs; auto. WellTypedBlock.
   intros [ls3 [U [W V]]].
   exploit add_equations_lessdef. eexact Heqo. eexact V. intros LD3.
   exploit add_equation_lessdef. eapply add_equations_satisf. eexact Heqo. eexact V.
@@ -2574,7 +2571,7 @@ Proof.
   eapply can_undef_satisf. eauto.
   eapply add_equation_satisf. eapply add_equations_satisf; eauto.
   intros [enext [P Q]].
-  split; econstructor; eauto.
+  split; econstructor; eauto using wt_undef_regs.
 
 (* call *)
 - set (sg := RTL.funsig fd) in *.
@@ -2700,7 +2697,7 @@ Proof.
   instantiate (1 := if b then ifso else ifnot). simpl. destruct b; auto.
   eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto.
   intros [enext [U V]].
-  split; econstructor; eauto.
+  split; econstructor; eauto using wt_undef_regs.
 
 (* jumptable *)
 - exploit (exec_moves mv); eauto.
@@ -2718,7 +2715,7 @@ Proof.
   instantiate (1 := pc'). simpl. eapply list_nth_z_in; eauto.
   eapply can_undef_satisf. eauto. eapply add_equation_satisf; eauto.
   intros [enext [U V]].
-  split; econstructor; eauto.
+  split; econstructor; eauto using wt_undef_regs.
 
 (* return *)
 - destruct (transf_function_inv _ _ FUN).
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index bd4010dbcb..9fb8d62320 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -333,9 +333,9 @@ Local Opaque mreg_type.
 - (* branch *)
   simpl in *. econstructor; eauto.
 - (* cond branch *)
-  simpl in *. econstructor; auto.
+  simpl in *. econstructor; auto; apply wt_undef_regs; auto.
 - (* jumptable *)
-  simpl in *. econstructor; auto.
+  simpl in *. econstructor; auto; apply wt_undef_regs; auto.
 - (* return *)
   simpl in *. InvBooleans.
   econstructor; eauto.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index e09eff5fe6..92877a003a 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -18,7 +18,7 @@ Require Import Coqlib Errors.
 Require Import Integers AST Linking.
 Require Import Values Memory Separation Events Globalenvs Smallstep.
 Require Import LTL Op Locations Linear Mach.
-Require Import Bounds Conventions Stacklayout Lineartyping.
+Require Import Bounds Conventions Conventions1 Stacklayout Lineartyping.
 Require Import Stacking.
 
 Local Open Scope sep_scope.
@@ -2147,13 +2147,8 @@ Proof.
   eapply match_states_return with (j := j').
   eapply match_stacks_change_meminj; eauto.
   apply agree_regs_set_pair. apply agree_regs_inject_incr with j; auto. auto.
-  inversion WTS; subst.
   apply external_call_well_typed in H0.
-  unfold Val.has_type_rpair, loc_result, proj_sig_res in *.
-  destruct (ef_sig ef) eqn:RES; simpl.
-  destruct sig_res; simpl in *.
-  destruct t0, res, Archi.big_endian; auto.
-  destruct res; auto.
+  apply loc_result_has_type; auto.
   apply agree_callee_save_set_result; auto.
   apply stack_contents_change_meminj with j; auto.
   rewrite sep_comm, sep_assoc; auto.
diff --git a/common/Values.v b/common/Values.v
index ef643389cb..58a43885da 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -166,7 +166,7 @@ Program Definition has_type_dec (v: val) (t: typ) : {has_type v t} + {~ has_type
   | false => right _
   end.
 Next Obligation.
-  destruct v, t; simpl in *; auto; congruence.
+  destruct v, t; simpl in *; auto; try congruence; destruct Archi.ptr64; auto.
 Qed.
 Next Obligation.
   destruct v, t; simpl in *; auto; try congruence.
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 1de55c1af8..bf2f541bbd 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -16,6 +16,7 @@
 Require Import Coqlib.
 Require Import Decidableplus.
 Require Import AST.
+Require Import Values.
 Require Import Events.
 Require Import Locations.
 Require Archi.
@@ -144,6 +145,22 @@ Proof.
   destruct Archi.ptr64 eqn:?; destruct (sig_res sig) as [[]|]; destruct Archi.ppc64; simpl; auto.
 Qed.
 
+Lemma loc_result_has_type:
+  forall res sig,
+  Val.has_type res (proj_sig_res sig) ->
+  Val.has_type_rpair res (loc_result sig) Val.loword Val.hiword mreg_type.
+Proof.
+  intros. unfold Val.has_type_rpair, loc_result, proj_sig_res in *.
+Local Transparent Archi.ptr64.
+  assert (P: Archi.ptr64 = false) by (unfold Archi.ptr64; auto).
+  destruct sig; simpl. destruct sig_res; simpl in H.
+  destruct t, res; simpl; auto;
+    simpl; try rewrite P; auto;
+    destruct Archi.ppc64 eqn:Q; simpl; try rewrite Q; auto.
+  destruct res; simpl; auto; destruct Archi.ppc64; auto.
+Qed.
+Local Opaque Archi.ptr64.
+
 (** The result locations are caller-save registers *)
 
 Lemma loc_result_caller_save:
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index df7ddfd20d..8f5d8f6ca6 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -19,7 +19,7 @@
     machine registers and stack slots. *)
 
 Require Import Coqlib Decidableplus.
-Require Import AST Machregs Locations.
+Require Import AST Values Machregs Locations.
 
 (** * Classification of machine registers *)
 
@@ -132,6 +132,17 @@ Proof.
   destruct (sig_res sig) as [[]|]; auto; destruct Archi.ptr64; auto.
 Qed.
 
+Lemma loc_result_has_type:
+  forall res sig,
+  Val.has_type res (proj_sig_res sig) ->
+  Val.has_type_rpair res (loc_result sig) Val.loword Val.hiword mreg_type.
+Proof.
+  intros. unfold Val.has_type_rpair, loc_result, proj_sig_res in *.
+  destruct sig; simpl. destruct sig_res; simpl in H.
+  destruct t, res; simpl; auto; destruct Archi.ptr64 eqn:P; simpl; try rewrite P; auto.
+  destruct res; simpl; auto; destruct Archi.ptr64; auto.
+Qed.
+
 (** The result locations are caller-save registers *)
 
 Lemma loc_result_caller_save:
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index 646c4afb31..2f4b4da5fc 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -14,7 +14,7 @@
     machine registers and stack slots. *)
 
 Require Import Coqlib Decidableplus.
-Require Import AST Machregs Locations.
+Require Import AST Values Machregs Locations.
 
 (** * Classification of machine registers *)
 
@@ -130,6 +130,17 @@ Proof.
   destruct Archi.ptr64; destruct (sig_res sig) as [[]|]; auto.
 Qed.
 
+Lemma loc_result_has_type:
+  forall res sig,
+  Val.has_type res (proj_sig_res sig) ->
+  Val.has_type_rpair res (loc_result sig) Val.loword Val.hiword mreg_type.
+Proof.
+  intros. unfold Val.has_type_rpair, loc_result, proj_sig_res in *.
+  destruct sig; simpl. destruct sig_res; simpl in H.
+  destruct t, res; simpl; auto; destruct Archi.ptr64 eqn:P; simpl; try rewrite P; auto.
+  destruct res; simpl; auto; destruct Archi.ptr64 eqn:P; simpl; try rewrite P; auto.
+Qed.
+
 (** The result locations are caller-save registers *)
 
 Lemma loc_result_caller_save:

From 2bef5ed4aa1e78abff92839aa126e46b35f542a4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gerg=C3=B6=20Barany?= <gergo.barany@inria.fr>
Date: Thu, 31 Aug 2017 11:06:33 +0200
Subject: [PATCH 5/5] Unify register and stack cases in Locmap.set

Locmap.set now uniformly uses `Val.load_result` to model stores to registers
and to stack slots equivalently.
---
 backend/Allocproof.v     | 41 ++++++++++++++--------------------------
 backend/LTLtyping.v      |  2 +-
 backend/Lineartyping.v   |  2 +-
 backend/Locations.v      | 22 +++++++--------------
 backend/Stackingproof.v  |  8 +++++---
 backend/Tunnelingproof.v |  6 ++----
 6 files changed, 30 insertions(+), 51 deletions(-)

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index df08196840..de48a33e11 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -724,7 +724,7 @@ Lemma loc_unconstrained_satisf:
 Proof.
   intros; red; intros.
   destruct (OrderedEquation.eq_dec q (Eq k r l)).
-  subst q; simpl. unfold l; rewrite Locmap.gss. rewrite pred_dec_true; auto.
+  subst q; simpl. unfold l; rewrite Locmap.gss. rewrite Val.load_result_same; auto.
   assert (EqSet.In q (remove_equation (Eq k r l) e)).
     simpl. ESD.fsetdec.
   rewrite Locmap.gso. apply H; auto. eapply loc_unconstrained_sound; eauto.
@@ -751,7 +751,7 @@ Lemma parallel_assignment_satisf:
 Proof.
   intros; red; intros.
   destruct (OrderedEquation.eq_dec q (Eq k r l)).
-  subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss, pred_dec_true; auto.
+  subst q; simpl. unfold l; rewrite Regmap.gss; rewrite Locmap.gss, Val.load_result_same; auto.
   assert (EqSet.In q (remove_equation {| ekind := k; ereg := r; eloc := l |} e)).
     simpl. ESD.fsetdec.
   exploit reg_loc_unconstrained_sound; eauto. intros [A B].
@@ -780,10 +780,10 @@ Proof.
   simpl in H2. InvBooleans. simpl.
   red; intros.
   destruct (OrderedEquation.eq_dec q (Eq Low res (R mr2))).
-  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss, pred_dec_true by auto.
+  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gss, Val.load_result_same by auto.
   apply Val.loword_lessdef; auto.
   destruct (OrderedEquation.eq_dec q (Eq High res (R mr1))).
-  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso, Locmap.gss, pred_dec_true by auto.
+  subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso, Locmap.gss, Val.load_result_same by auto.
   apply Val.hiword_lessdef; auto.
   assert (EqSet.In q e'). unfold e', remove_equation; simpl; ESD.fsetdec.
   rewrite Regmap.gso. rewrite ! Locmap.gso. auto.
@@ -1083,9 +1083,7 @@ Proof.
   subst dst. rewrite Locmap.gss.
   destruct q as [k r l]; simpl in *.
   exploit loc_type_compat_well_typed; eauto.
-  destruct l as [mr | sl ofs ty]; intros.
-  rewrite pred_dec_true by auto. apply (H3 _ B).
-  apply val_lessdef_normalize; auto. apply (H3 _ B).
+  intro. rewrite Val.load_result_same by auto. apply (H3 _ B).
   rewrite Locmap.gso; auto.
 Qed.
 
@@ -1146,7 +1144,7 @@ Lemma subst_loc_part_satisf_lowlong:
 Proof.
   intros; red; intros.
   exploit in_subst_loc_part; eauto. intros [[A [B C]] | [A B]].
-  rewrite A, B. apply H1 in C. rewrite Locmap.gss, pred_dec_true by auto.
+  rewrite A, B. apply H1 in C. rewrite Locmap.gss, Val.load_result_same by auto.
   apply Val.loword_lessdef. exact C.
   rewrite Locmap.gso; auto.
 Qed.
@@ -1160,7 +1158,7 @@ Lemma subst_loc_part_satisf_highlong:
 Proof.
   intros; red; intros.
   exploit in_subst_loc_part; eauto. intros [[A [B C]] | [A B]].
-  rewrite A, B. apply H1 in C. rewrite Locmap.gss, pred_dec_true by auto.
+  rewrite A, B. apply H1 in C. rewrite Locmap.gss, Val.load_result_same by auto.
   apply Val.hiword_lessdef. exact C.
   rewrite Locmap.gso; auto.
 Qed.
@@ -1252,7 +1250,8 @@ Proof.
   assert (subtype (env (ereg q)) Tlong = true).
   { exploit long_type_compat_charact; eauto. intros [P|P]; auto.
     eelim Loc.diff_not_eq; eauto. }
-  rewrite Locmap.gss, pred_dec_true by auto. simpl. rewrite <- (val_longofwords_eq_1 rs#(ereg q)).
+  rewrite Locmap.gss, Val.load_result_same by auto.
+  simpl. rewrite <- (val_longofwords_eq_1 rs#(ereg q)).
   apply Val.longofwords_lessdef. exact C. exact D.
   eapply Val.has_subtype; eauto.
   assumption.
@@ -1314,19 +1313,7 @@ Proof.
   exploit in_subst_loc; eauto. intros [[A B] | [A B]].
   subst dst. rewrite Locmap.gss.
   destruct q as [k r l]; simpl in *.
-  exploit loc_type_compat_well_typed; eauto.
-  destruct l as [mr | sl ofs ty]; intros.
-  destruct (Val.eq (sel_val k rs#r) Vundef).
-  rewrite e0 in *; auto.
-  rewrite pred_dec_true. apply (H3 _ B).
-  exploit loc_type_compat_charact; eauto; intros [SUBTYP | DIFF].
-  simpl in SUBTYP.
-  set (qR := {| ekind := k; ereg := r; eloc := R mr |}).
-  generalize (in_subst_loc (R mr) src qR _ _ H4 H); intros [[EQ IN] | [DIFF' IN']].
-  generalize (H3 _ IN); intro LESSDEF. simpl in LESSDEF.
-  destruct k; simpl in *; inversion LESSDEF; congruence.
-  simpl in DIFF'; congruence.
-  simpl in DIFF; congruence.
+  exploit loc_type_compat_well_typed; eauto. intros.
   apply val_lessdef_normalize; auto. apply (H3 _ B).
   rewrite Locmap.gso; auto. rewrite undef_regs_outside. eauto.
   eapply can_undef_except_sound; eauto. apply Loc.diff_sym; auto.
@@ -1741,10 +1728,10 @@ Proof.
   decompose [and] H4. decompose [and] H5; subst.
   destruct (OrderedEquation.eq_dec q (Eq Low x (R lo))).
   subst q; simpl. rewrite Regmap.gss.
-  rewrite Locmap.gss, pred_dec_true; auto. apply Val.loword_lessdef; auto.
+  rewrite Locmap.gss, Val.load_result_same; auto. apply Val.loword_lessdef; auto.
   destruct (OrderedEquation.eq_dec q (Eq High x (R hi))).
   subst q; simpl. rewrite Regmap.gss. rewrite Locmap.gso by (red; auto).
-  rewrite Locmap.gss, pred_dec_true; auto. apply Val.hiword_lessdef; auto.
+  rewrite Locmap.gss, Val.load_result_same; auto. apply Val.hiword_lessdef; auto.
   assert (EqSet.In q e'').
   { unfold e'', e', remove_equation; simpl; ESD.fsetdec. }
   rewrite Regmap.gso. rewrite ! Locmap.gso. auto.
@@ -2797,7 +2784,7 @@ Proof.
   generalize (loc_result_type (ef_sig ef)); intro SUBTYP.
   rewrite RES in SUBTYP; simpl in SUBTYP.
   exploit Val.has_subtype; eauto; intros.
-  rewrite pred_dec_true; auto.
+  rewrite Val.load_result_same; auto.
 
   generalize (loc_result_pair (ef_sig ef)); rewrite RES; intros (A & B & C & D & E).
   exploit external_call_well_typed; eauto. unfold proj_sig_res; rewrite B. intros WTRES'.
@@ -2805,7 +2792,7 @@ Proof.
 
   generalize (loc_result_type (ef_sig ef)); intro SUBTYP.
   rewrite RES in SUBTYP; simpl in SUBTYP.
-  rewrite !pred_dec_true.
+  rewrite !Val.load_result_same.
   rewrite val_longofwords_eq_1 by auto. auto.
   eapply Val.has_subtype; eauto. destruct v'; simpl; auto.
   eapply Val.has_subtype; eauto. destruct v'; simpl; auto.
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 9fb8d62320..501c7dbb7a 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -118,7 +118,7 @@ Proof.
   intros; red; intros.
   unfold Locmap.set.
   destruct (Loc.eq (R r) l).
-  subst l; rewrite pred_dec_true; auto.
+  subst l. rewrite Val.load_result_same; auto.
   destruct (Loc.diff_dec (R r) l). auto. red. auto.
 Qed.
 
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 1d2bffe38e..1a31a6efb0 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -107,7 +107,7 @@ Proof.
   intros; red; intros.
   unfold Locmap.set.
   destruct (Loc.eq (R r) l).
-  subst l; rewrite pred_dec_true; auto.
+  subst l; rewrite Val.load_result_same; auto.
   destruct (Loc.diff_dec (R r) l). auto. red. auto.
 Qed.
 
diff --git a/backend/Locations.v b/backend/Locations.v
index b271fed1a1..8e0b3349a4 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -331,33 +331,25 @@ Module Locmap.
   Definition set (l: loc) (v: val) (m: t) : t :=
     fun (p: loc) =>
       if Loc.eq l p then
-        match l with
-        | R r => if Val.has_type_dec v (mreg_type r) then v else Vundef
-        | S sl ofs ty => Val.load_result (chunk_of_type ty) v
-        end
+        Val.load_result (chunk_of_type (Loc.type l)) v
       else if Loc.diff_dec l p then
         m p
       else Vundef.
 
   Lemma gss: forall l v m,
-    (set l v m) l =
-    match l with
-    | R r => if Val.has_type_dec v (mreg_type r) then v else Vundef
-    | S sl ofs ty => Val.load_result (chunk_of_type ty) v
-    end.
+    (set l v m) l = Val.load_result (chunk_of_type (Loc.type l)) v.
   Proof.
     intros. unfold set. apply dec_eq_true.
   Qed.
 
   Lemma gss_reg: forall r v m, Val.has_type v (mreg_type r) -> (set (R r) v m) (R r) = v.
   Proof.
-    intros. unfold set. rewrite dec_eq_true, pred_dec_true; auto.
+    intros. unfold set. rewrite dec_eq_true, Val.load_result_same; auto.
   Qed.
 
   Lemma gss_typed: forall l v m, Val.has_type v (Loc.type l) -> (set l v m) l = v.
   Proof.
-    intros. rewrite gss. destruct l.
-    rewrite pred_dec_true; auto. apply Val.load_result_same; auto.
+    intros. rewrite gss. apply Val.load_result_same; auto.
   Qed.
 
   Lemma gso: forall l v m p, Loc.diff l p -> (set l v m) p = m p.
@@ -384,10 +376,10 @@ Module Locmap.
   Lemma gus: forall ll l m, In l ll -> (undef ll m) l = Vundef.
   Proof.
     assert (P: forall ll l m, m l = Vundef -> (undef ll m) l = Vundef).
-      induction ll; simpl; intros. auto. apply IHll.
+    { induction ll; simpl; intros. auto. apply IHll.
       unfold set. destruct (Loc.eq a l).
-      destruct a. auto. destruct ty; reflexivity.
-      destruct (Loc.diff_dec a l); auto.
+      apply Val.load_result_same; auto. simpl; auto.
+      destruct (Loc.diff_dec a l); auto. }
     induction ll; simpl; intros. contradiction.
     destruct H. apply P. subst a. apply gss_typed. exact I.
     auto.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 92877a003a..66721046ee 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -615,7 +615,7 @@ Lemma agree_regs_set_reg:
 Proof.
   intros; red; intros.
   unfold Regmap.set. destruct (RegEq.eq r0 r). subst r0.
-  rewrite Locmap.gss, pred_dec_true; auto.
+  rewrite Locmap.gss, Val.load_result_same; auto.
   rewrite Locmap.gso; auto. red. auto.
 Qed.
 
@@ -998,7 +998,8 @@ Remark LTL_undef_regs_same:
   forall r rl ls, In r rl -> LTL.undef_regs rl ls (R r) = Vundef.
 Proof.
   induction rl; simpl; intros. contradiction.
-  unfold Locmap.set. destruct (Loc.eq (R a) (R r)). auto.
+  unfold Locmap.set. destruct (Loc.eq (R a) (R r)).
+  rewrite Val.load_result_same; simpl; auto.
   destruct (Loc.diff_dec (R a) (R r)); auto.
   apply IHrl. intuition congruence.
 Qed.
@@ -1023,7 +1024,8 @@ Remark undef_regs_type:
 Proof.
   induction rl; simpl; intros.
 - auto.
-- unfold Locmap.set. destruct (Loc.eq (R a) l). simpl; auto.
+- unfold Locmap.set. destruct (Loc.eq (R a) l).
+  rewrite Val.load_result_same; simpl; auto.
   destruct (Loc.diff_dec (R a) l); auto. red; auto.
 Qed.
 
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 8595539ff5..2dc1d78c93 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -262,9 +262,7 @@ Lemma locmap_set_lessdef:
   locmap_lessdef ls1 ls2 -> Val.lessdef v1 v2 -> locmap_lessdef (Locmap.set l v1 ls1) (Locmap.set l v2 ls2).
 Proof.
   intros; red; intros l'. unfold Locmap.set. destruct (Loc.eq l l').
-- destruct l.
-  + destruct H0. destruct (Val.has_type_dec v (mreg_type r)); auto. auto.
-  + auto using Val.load_result_lessdef.
+- destruct l; auto using Val.load_result_lessdef.
 - destruct (Loc.diff_dec l l'); auto.
 Qed.
 
@@ -273,7 +271,7 @@ Lemma locmap_set_undef_lessdef:
   locmap_lessdef ls1 ls2 -> locmap_lessdef (Locmap.set l Vundef ls1) ls2.
 Proof.
   intros; red; intros l'. unfold Locmap.set. destruct (Loc.eq l l').
-- destruct l; auto. destruct ty; auto. 
+- subst. destruct (Loc.type l'); auto.
 - destruct (Loc.diff_dec l l'); auto.
 Qed.