Share code for memory access for PowerPC

Instead of duplicating the memory access code in `Asmexpand.ml` we move
the code for each of the different addressings in `Asmgen.v` into
separate functions that then can be reused in `Asmexpand.ml`.

4 files changed, 159 insertions, 166 deletions

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index e663226f..7efa80a6 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -58,6 +58,20 @@ let emit_loadimm r n =
 let emit_addimm rd rs n =
   List.iter emit (Asmgen.addimm rd rs n [])
 
+let emit_aindexed mk1 mk2 unaligned r1 temp ofs =
+  List.iter emit (Asmgen.aindexed mk1 mk2 unaligned r1 temp ofs [])
+
+let emit_aindexed2 mk r1 r2 =
+  List.iter emit (Asmgen.aindexed2 mk r1 r2 [])
+
+let emit_aglobal mk1 mk2 unaligned temp symb ofs =
+  List.iter emit (Asmgen.aglobal mk1 mk2 unaligned temp symb ofs [])
+
+let emit_abased mk1 mk2 unaligned r1 temp symb ofs =
+  List.iter emit (Asmgen.abased mk1 mk2 unaligned r1 temp symb ofs [])
+
+let emit_ainstack mk1 mk2 unaligned temp ofs =
+  List.iter emit (Asmgen.ainstack mk1 mk2 unaligned temp ofs [])
 (* Numbering of bits in the CR register *)
 
 let num_crbit = function
@@ -175,79 +189,23 @@ let expand_builtin_memcpy sz al args =
 (* Handling of volatile reads and writes *)
 
 let expand_volatile_access
-       (mk1: ireg -> constant -> unit)
-       (mk2: ireg -> ireg -> unit)
+       (mk1: constant -> ireg -> instruction list -> instruction list)
+       (mk2: ireg -> ireg -> instruction list -> instruction list)
        ?(ofs_unaligned = true)
        addr temp =
   match addr with
   | BA(IR r) ->
-      mk1 r (Cint _0)
+    List.iter emit (mk1 (Cint _0) r [])
   | BA_addrstack ofs ->
-      if ofs_unaligned || Int.eq (Int.mods ofs _4) _0 then
-        if offset_in_range ofs then
-          mk1 GPR1 (Cint ofs)
-        else begin
-          emit (Paddis(temp, GPR1, Cint (Asmgen.high_s ofs)));
-          mk1 temp (Cint (Asmgen.low_s ofs))
-        end
-      else begin
-        emit (Paddis (temp, GPR1, Cint (Asmgen.high_s ofs)));
-        emit (Paddi (temp, temp, Cint (Asmgen.low_s ofs)));
-        mk1 temp (Cint _0)
-      end
+    emit_ainstack mk1 mk2 ofs_unaligned temp ofs
   | BA_addrglobal(id, ofs) ->
-      if symbol_is_small_data id ofs then
-        if ofs_unaligned || Asmgen.symbol_ofs_word_aligned id ofs then
-          mk1 GPR0 (Csymbol_sda(id, ofs))
-        else begin
-          emit (Paddi (temp, GPR0, (Csymbol_sda (id,ofs))));
-          mk1 temp (Cint _0)
-        end
-      else if symbol_is_rel_data id ofs then begin
-        emit (Paddis(temp, GPR0, Csymbol_rel_high(id, ofs)));
-        emit (Paddi(temp, temp, Csymbol_rel_low(id, ofs)));
-        mk1 temp (Cint _0)
-      end else if ofs_unaligned || Asmgen.symbol_ofs_word_aligned id ofs then begin
-        emit (Paddis(temp, GPR0, Csymbol_high(id, ofs)));
-        mk1 temp (Csymbol_low(id, ofs))
-      end else begin
-        emit (Paddis (temp, GPR0, (Csymbol_high (id, ofs))));
-        emit (Paddi (temp, temp, (Csymbol_low (id, ofs))));
-        mk1 temp (Cint _0)
-      end
+    emit_aglobal mk1 mk2 ofs_unaligned temp id ofs
   | BA_addptr(BA(IR r), BA_int n) ->
-      if ofs_unaligned || Int.eq (Int.mods n _4) _0 then
-        if offset_in_range n then
-          mk1 r (Cint n)
-        else begin
-          emit (Paddis(temp, r, Cint (Asmgen.high_s n)));
-          mk1 temp (Cint (Asmgen.low_s n))
-        end
-      else begin
-        emit (Paddis (temp, r, Cint (Asmgen.high_s n)));
-        emit (Paddi (temp, temp, Cint (Asmgen.low_s n)));
-        mk1 temp (Cint _0)
-      end
+    emit_aindexed mk1 mk2 ofs_unaligned r temp n
   | BA_addptr(BA_addrglobal(id, ofs), BA(IR r)) ->
-      if symbol_is_small_data id ofs then begin
-        emit (Paddi(GPR0, GPR0, Csymbol_sda(id, ofs)));
-        mk2 r GPR0
-      end else if symbol_is_rel_data id ofs then begin
-        emit (Pmr(GPR0, r));
-        emit (Paddis(temp, GPR0, Csymbol_rel_high(id, ofs)));
-        emit (Paddi(temp, temp, Csymbol_rel_low(id, ofs)));
-        mk2 temp GPR0
-      end else if ofs_unaligned || Asmgen.symbol_ofs_word_aligned id ofs then begin
-        emit (Paddis(temp, r, Csymbol_high(id, ofs)));
-        mk1 temp (Csymbol_low(id, ofs))
-      end else begin
-        emit (Pmr (GPR0, r));
-        emit (Paddis(temp, GPR0, Csymbol_high(id, ofs)));
-        emit (Paddi(temp, temp, Csymbol_low(id, ofs)));
-        mk2 temp GPR0
-      end
+    emit_abased mk1 mk2 ofs_unaligned r temp id ofs
   | BA_addptr(BA(IR r1), BA(IR r2)) ->
-      mk2 r1 r2
+    emit_aindexed2 mk2 r1 r2
   | _ ->
       assert false
 
@@ -260,69 +218,69 @@ let offset_constant cst delta =
       Some (Csymbol_sda(id, Int.add ofs delta))
   | _ -> None
 
-let expand_load_int64 hi lo base ofs_hi ofs_lo =
+let expand_load_int64 hi lo base ofs_hi ofs_lo k =
   if hi <> base then begin
-    emit (Plwz(hi, ofs_hi, base));
-    emit (Plwz(lo, ofs_lo, base))
+    Plwz(hi, ofs_hi, base) ::
+    Plwz(lo, ofs_lo, base) :: k
   end else begin
-    emit (Plwz(lo, ofs_lo, base));
-    emit (Plwz(hi, ofs_hi, base))
+    Plwz(lo, ofs_lo, base) ::
+    Plwz(hi, ofs_hi, base) :: k
   end
 
 let expand_builtin_vload_1 chunk addr res =
   match chunk, res with
   | Mint8unsigned, BR(IR res) ->
       expand_volatile_access
-        (fun r c -> emit (Plbz(res, c, r)))
-        (fun r1 r2 -> emit (Plbzx(res, r1, r2)))
+        (fun c r k -> Plbz(res, c, r) :: k)
+        (fun r1 r2 k -> Plbzx(res, r1, r2) :: k)
         addr GPR11
   | Mint8signed, BR(IR res) ->
       expand_volatile_access
-        (fun r c -> emit (Plbz(res, c, r)); emit (Pextsb(res, res)))
-        (fun r1 r2 -> emit (Plbzx(res, r1, r2)); emit (Pextsb(res, res)))
+        (fun c r k-> Plbz(res, c, r) :: Pextsb(res, res) :: k)
+        (fun r1 r2 k -> Plbzx(res, r1, r2) :: Pextsb(res, res) :: k)
         addr GPR11
   | Mint16unsigned, BR(IR res) ->
       expand_volatile_access
-        (fun r c -> emit (Plhz(res, c, r)))
-        (fun r1 r2 -> emit (Plhzx(res, r1, r2)))
+        (fun c r k ->  Plhz(res, c, r) :: k)
+        (fun r1 r2 k -> Plhzx(res, r1, r2) :: k)
         addr GPR11
   | Mint16signed, BR(IR res) ->
       expand_volatile_access
-        (fun r c -> emit (Plha(res, c, r)))
-        (fun r1 r2 -> emit (Plhax(res, r1, r2)))
+        (fun c r k-> Plha(res, c, r) :: k)
+        (fun r1 r2 k -> Plhax(res, r1, r2) :: k)
         addr GPR11
   | (Mint32 | Many32), BR(IR res) ->
       expand_volatile_access
-        (fun r c -> emit (Plwz(res, c, r)))
-        (fun r1 r2 -> emit (Plwzx(res, r1, r2)))
+        (fun c r k-> Plwz(res, c, r) :: k)
+        (fun r1 r2 k -> Plwzx(res, r1, r2) :: k)
         addr GPR11
   | Mfloat32, BR(FR res) ->
       expand_volatile_access
-        (fun r c -> emit (Plfs(res, c, r)))
-        (fun r1 r2 -> emit (Plfsx(res, r1, r2)))
+        (fun c r k-> Plfs(res, c, r) :: k)
+        (fun r1 r2 k -> Plfsx(res, r1, r2) :: k)
         addr GPR11
   | (Mfloat64 | Many64), BR(FR res) ->
       expand_volatile_access
-        (fun r c -> emit (Plfd(res, c, r)))
-        (fun r1 r2 -> emit (Plfdx(res, r1, r2)))
+        (fun c r k-> Plfd(res, c, r) :: k)
+        (fun r1 r2 k -> Plfdx(res, r1, r2) :: k)
         addr GPR11
   | (Mint64 | Many64), BR(IR res) ->
       expand_volatile_access
-        (fun r c -> emit (Pld(res, c, r)))
-        (fun r1 r2 -> emit (Pldx(res, r1, r2)))
+        (fun c r k-> Pld(res, c, r) :: k)
+        (fun r1 r2 k -> Pldx(res, r1, r2) :: k)
         ~ofs_unaligned:false
         addr GPR11
   | Mint64, BR_splitlong(BR(IR hi), BR(IR lo)) ->
       expand_volatile_access
-        (fun r c ->
+        (fun c r k->
            match offset_constant c _4 with
-           | Some c' -> expand_load_int64 hi lo r c c'
+           | Some c' -> expand_load_int64 hi lo r c c' k
            | None ->
-               emit (Paddi(GPR11, r, c));
-               expand_load_int64 hi lo GPR11 (Cint _0) (Cint _4))
-        (fun r1 r2 ->
-           emit (Padd(GPR11, r1, r2));
-           expand_load_int64 hi lo GPR11 (Cint _0) (Cint _4))
+               Paddi(GPR11, r, c) ::
+               expand_load_int64 hi lo GPR11 (Cint _0) (Cint _4) k)
+        (fun r1 r2 k ->
+           Padd(GPR11, r1, r2) ::
+           expand_load_int64 hi lo GPR11 (Cint _0) (Cint _4) k)
         addr GPR11
   | _, _ ->
       assert false
@@ -338,55 +296,55 @@ let temp_for_vstore src =
   else if not (List.mem (IR GPR12) rl) then GPR12
   else GPR10
 
-let expand_store_int64 hi lo base ofs_hi ofs_lo =
-  emit (Pstw(hi, ofs_hi, base));
-  emit (Pstw(lo, ofs_lo, base))
+let expand_store_int64 hi lo base ofs_hi ofs_lo k =
+  Pstw(hi, ofs_hi, base) ::
+  Pstw(lo, ofs_lo, base) :: k
 
 let expand_builtin_vstore_1 chunk addr src =
   let temp = temp_for_vstore src in
   match chunk, src with
   | (Mint8signed | Mint8unsigned), BA(IR src) ->
       expand_volatile_access
-        (fun r c -> emit (Pstb(src, c, r)))
-        (fun r1 r2 -> emit (Pstbx(src, r1, r2)))
+        (fun c r k-> Pstb(src, c, r) :: k)
+        (fun r1 r2 k -> Pstbx(src, r1, r2) :: k)
         addr temp
   | (Mint16signed | Mint16unsigned), BA(IR src) ->
       expand_volatile_access
-        (fun r c -> emit (Psth(src, c, r)))
-        (fun r1 r2 -> emit (Psthx(src, r1, r2)))
+        (fun c r k-> Psth(src, c, r) :: k)
+        (fun r1 r2 k -> Psthx(src, r1, r2) :: k)
         addr temp
   | (Mint32 | Many32), BA(IR src) ->
       expand_volatile_access
-        (fun r c -> emit (Pstw(src, c, r)))
-        (fun r1 r2 -> emit (Pstwx(src, r1, r2)))
+        (fun c r k-> Pstw(src, c, r) :: k)
+        (fun r1 r2 k -> Pstwx(src, r1, r2) :: k)
         addr temp
   | Mfloat32, BA(FR src) ->
       expand_volatile_access
-        (fun r c -> emit (Pstfs(src, c, r)))
-        (fun r1 r2 -> emit (Pstfsx(src, r1, r2)))
+        (fun c r k-> Pstfs(src, c, r) :: k)
+        (fun r1 r2 k -> Pstfsx(src, r1, r2) :: k)
         addr temp
   | (Mfloat64 | Many64), BA(FR src) ->
       expand_volatile_access
-        (fun r c -> emit (Pstfd(src, c, r)))
-        (fun r1 r2 -> emit (Pstfdx(src, r1, r2)))
+        (fun c r k-> Pstfd(src, c, r) :: k)
+        (fun r1 r2 k -> Pstfdx(src, r1, r2) :: k)
         addr temp
   | (Mint64 | Many64), BA(IR src) ->
       expand_volatile_access
-        (fun r c -> emit (Pstd(src, c, r)))
-        (fun r1 r2 -> emit (Pstdx(src, r1, r2)))
+        (fun c r k-> Pstd(src, c, r) :: k)
+        (fun r1 r2 k -> Pstdx(src, r1, r2) :: k)
         ~ofs_unaligned:false
         addr temp
   | Mint64, BA_splitlong(BA(IR hi), BA(IR lo)) ->
       expand_volatile_access
-        (fun r c ->
+        (fun c r k ->
            match offset_constant c _4 with
-           | Some c' -> expand_store_int64 hi lo r c c'
+           | Some c' -> expand_store_int64 hi lo r c c' k
            | None ->
-               emit (Paddi(temp, r, c));
-               expand_store_int64 hi lo temp (Cint _0) (Cint _4))
-        (fun r1 r2 ->
-           emit (Padd(temp, r1, r2));
-           expand_store_int64 hi lo temp (Cint _0) (Cint _4))
+               Paddi(temp, r, c) ::
+               expand_store_int64 hi lo temp (Cint _0) (Cint _4) k)
+        (fun r1 r2 k ->
+           Padd(temp, r1, r2) ::
+           expand_store_int64 hi lo temp (Cint _0) (Cint _4) k)
         addr temp
   | _, _ ->
       assert false
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 0a75ad58..7b6ac9af 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -730,6 +730,82 @@ Definition symbol_ofs_word_aligned symb ofs :=
   let ofs := Ptrofs.to_int ofs in
   symbol_is_aligned symb 4 && (Int.eq (Int.mods ofs (Int.repr 4)) Int.zero).
 
+Definition aindexed
+     (mk1: constant -> ireg -> code -> code)
+     (mk2: ireg -> ireg -> code -> code)
+     (unaligned : bool) (r1 temp: ireg) (ofs: int) (k: code) :=
+  if unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero then
+    if Int.eq (high_s ofs) Int.zero then
+      mk1 (Cint ofs) r1 k
+    else
+      Paddis temp r1 (Cint (high_s ofs)) ::
+             mk1 (Cint (low_s ofs)) temp k
+  else
+    (loadimm GPR0 ofs (mk2 r1 GPR0 k)).
+
+Definition aindexed2
+     (mk: ireg -> ireg -> code -> code)
+     (r1 r2: ireg) (k: code) :=
+  mk r1 r2 k.
+
+Definition aglobal
+     (mk1: constant -> ireg -> code -> code)
+     (mk2: ireg -> ireg -> code -> code)
+     (unaligned : bool) (temp: ireg)
+     symb ofs k :=
+  if symbol_is_small_data symb ofs then
+    if unaligned || symbol_ofs_word_aligned symb ofs then
+      mk1 (Csymbol_sda symb ofs) GPR0 k
+    else
+      Paddi temp GPR0 (Csymbol_sda symb ofs) ::
+      mk1 (Cint Int.zero) temp k
+  else if symbol_is_rel_data symb ofs then
+    Paddis temp GPR0 (Csymbol_rel_high symb ofs) ::
+    Paddi temp temp (Csymbol_rel_low symb ofs) ::
+    mk1 (Cint Int.zero) temp k
+  else if  unaligned || symbol_ofs_word_aligned symb ofs then
+    Paddis temp GPR0 (Csymbol_high symb ofs) ::
+    mk1 (Csymbol_low symb ofs) temp k
+  else
+    Paddis temp GPR0 (Csymbol_high symb ofs) ::
+    Paddi temp temp (Csymbol_low symb ofs) ::
+    mk1 (Cint Int.zero) temp k.
+
+Definition abased
+     (mk1: constant -> ireg -> code -> code)
+     (mk2: ireg -> ireg -> code -> code)
+     (unaligned : bool) (r1 temp: ireg)
+     symb ofs k :=
+  if symbol_is_small_data symb ofs then
+    Paddi GPR0 GPR0 (Csymbol_sda symb ofs) ::
+    mk2 r1 GPR0 k
+  else if symbol_is_rel_data symb ofs then
+    Pmr GPR0 r1 ::
+    Paddis temp GPR0 (Csymbol_rel_high symb ofs) ::
+    Paddi temp temp (Csymbol_rel_low symb ofs) ::
+    mk2 temp GPR0 k
+  else if  unaligned || symbol_ofs_word_aligned symb ofs then
+    Paddis temp r1 (Csymbol_high symb ofs) ::
+    mk1 (Csymbol_low symb ofs) temp k
+  else
+    Pmr GPR0 r1 ::
+    Paddis temp GPR0 (Csymbol_high symb ofs) ::
+    Paddi temp temp (Csymbol_low symb ofs) ::
+    mk2 temp GPR0 k.
+
+Definition ainstack
+     (mk1 : constant -> ireg -> code -> code)
+     (mk2 : ireg -> ireg -> code -> code)
+     (unaligned : bool) (temp: ireg) ofs k :=
+  if  unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero then
+    if Int.eq (high_s ofs) Int.zero then
+      mk1 (Cint ofs) GPR1 k
+    else
+      Paddis temp GPR1 (Cint (high_s ofs)) ::
+      mk1 (Cint (low_s ofs)) temp k
+  else
+    addimm temp GPR1 ofs (mk1 (Cint Int.zero) temp k).
+
 Definition transl_memory_access
      (mk1: constant -> ireg -> instruction)
      (mk2: ireg -> ireg -> instruction)
@@ -739,63 +815,18 @@ Definition transl_memory_access
   match addr, args with
   | Aindexed ofs, a1 :: nil =>
       do r1 <- ireg_of a1;
-      OK (if unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero then
-            if Int.eq (high_s ofs) Int.zero then
-               mk1 (Cint ofs) r1 :: k
-             else
-               Paddis temp r1 (Cint (high_s ofs)) ::
-               mk1 (Cint (low_s ofs)) temp :: k
-          else
-            (loadimm GPR0 ofs (mk2 r1 GPR0 :: k)))
+      OK (aindexed (fun c r k => mk1 c r :: k) (fun r1 r2 k => mk2 r1 r2 :: k) unaligned r1 temp ofs k)
   | Aindexed2, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
-      OK (mk2 r1 r2 :: k)
+      OK (aindexed2 (fun r1 r2 k => mk2 r1 r2 :: k) r1 r2 k)
   | Aglobal symb ofs, nil =>
-       OK (if symbol_is_small_data symb ofs then
-             if unaligned || symbol_ofs_word_aligned symb ofs then
-               mk1 (Csymbol_sda symb ofs) GPR0 :: k
-             else
-               Paddi temp GPR0 (Csymbol_sda symb ofs) ::
-               mk1 (Cint Int.zero) temp :: k
-         else if symbol_is_rel_data symb ofs then
-           Paddis temp GPR0 (Csymbol_rel_high symb ofs) ::
-           Paddi temp temp (Csymbol_rel_low symb ofs) ::
-           mk1 (Cint Int.zero) temp :: k
-         else if  unaligned || symbol_ofs_word_aligned symb ofs then
-           Paddis temp GPR0 (Csymbol_high symb ofs) ::
-           mk1 (Csymbol_low symb ofs) temp :: k
-         else
-           Paddis temp GPR0 (Csymbol_high symb ofs) ::
-           Paddi temp temp (Csymbol_low symb ofs) ::
-           mk1 (Cint Int.zero) temp :: k)
+      OK (aglobal (fun c r k => mk1 c r :: k) (fun r1 r2 k => mk2 r1 r2 :: k) unaligned temp symb ofs k)
   | Abased symb ofs, a1 :: nil =>
       do r1 <- ireg_of a1;
-      OK (if symbol_is_small_data symb ofs then
-            Paddi GPR0 GPR0 (Csymbol_sda symb ofs) ::
-            mk2 r1 GPR0 :: k
-          else if symbol_is_rel_data symb ofs then
-            Pmr GPR0 r1 ::
-            Paddis temp GPR0 (Csymbol_rel_high symb ofs) ::
-            Paddi temp temp (Csymbol_rel_low symb ofs) ::
-            mk2 temp GPR0 :: k
-          else if  unaligned || symbol_ofs_word_aligned symb ofs then
-            Paddis temp r1 (Csymbol_high symb ofs) ::
-            mk1 (Csymbol_low symb ofs) temp :: k
-          else
-            Pmr GPR0 r1 ::
-            Paddis temp GPR0 (Csymbol_high symb ofs) ::
-            Paddi temp temp (Csymbol_low symb ofs) ::
-            mk2 temp GPR0 :: k)
+      OK (abased (fun c r k => mk1 c r :: k) (fun r1 r2 k => mk2 r1 r2 :: k) unaligned r1 temp symb ofs k)
   | Ainstack ofs, nil =>
       let ofs := Ptrofs.to_int ofs in
-      OK (if  unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero then
-            if Int.eq (high_s ofs) Int.zero then
-              mk1 (Cint ofs) GPR1 :: k
-            else
-              Paddis temp GPR1 (Cint (high_s ofs)) ::
-              mk1 (Cint (low_s ofs)) temp :: k
-          else
-             addimm temp GPR1 ofs (mk1 (Cint Int.zero) temp :: k))
+      OK (ainstack (fun c r k => mk1 c r :: k) (fun r1 r2 k => mk2 r1 r2 :: k) unaligned temp ofs k)
   | _, _ =>
       Error(msg "Asmgen.transl_memory_access")
   end.
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 2730e3d6..85541118 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -310,7 +310,7 @@ Remark transl_memory_access_label:
   (forall r1 r2, nolabel (mk2 r1 r2)) ->
   tail_nolabel k c.
 Proof.
-  unfold transl_memory_access; intros; destruct addr; TailNoLabel.
+  unfold transl_memory_access, aindexed, aindexed2, aglobal, abased, ainstack; intros; destruct addr; TailNoLabel.
   destruct (unaligned || Int.eq (Int.mods i (Int.repr 4)) Int.zero). destruct (Int.eq (high_s i) Int.zero); TailNoLabel.
   eapply tail_nolabel_trans. apply loadimm_label. TailNoLabel.
   destruct (symbol_is_small_data i i0). destruct (unaligned || symbol_ofs_word_aligned i i0); TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 7268b407..6ae520ef 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1564,6 +1564,7 @@ Proof.
   intros until m'; intros TR ADDR TEMP MK1 MK2.
   unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in ADDR; inv ADDR.
   - (* Aindexed *)
+    unfold aindexed.
     destruct (unaligned || Int.eq (Int.mods i (Int.repr 4)) Int.zero); [destruct (Int.eq (high_s i) Int.zero) |].
     + (* Aindexed 4 aligned short *)
       apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
@@ -1590,6 +1591,7 @@ Proof.
   - (* Aindexed2 *)
     apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
   - (* Aglobal *)
+    unfold aglobal in *.
     destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR.
     + (* Aglobal from small data 4 aligned *)
       case (unaligned || symbol_ofs_word_aligned i i0).
@@ -1643,7 +1645,8 @@ Proof.
       apply exec_straight_step with rs2 m; auto. simpl. unfold rs2.
       rewrite gpr_or_zero_not_zero; auto. f_equal. f_equal. f_equal.
       unfold rs1; Simpl. apply low_high_half_zero. eexact EX'. auto.
-  -(* Abased *)
+  - (* Abased *)
+  unfold abased in *.
   destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ].
   + (* Abased from small data *)
     set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))).
@@ -1700,6 +1703,7 @@ Proof.
     unfold rs2; Simpl. apply low_high_half_zero.
     eexact EX'. auto.
   - (* Ainstack *)
+    unfold ainstack in *.
     set (ofs := Ptrofs.to_int i) in *.
     assert (L: Val.lessdef (Val.offset_ptr (rs GPR1) i) (Val.add (rs GPR1) (Vint ofs))).
     { destruct (rs GPR1); simpl; auto. unfold ofs; rewrite Ptrofs.of_int_to_int; auto. }