Tentative first fix for offsets of ld/std.

The offsets immediates used in the ld and std instructions must be a
multiple of the word size. This commit changes the two functions which
are used when generating load/stores in Asmgen, accessind and
transl_memory_access.

For accessind one only needs an additional check that the offset is a
multiple of the word size for the case that the high part of the offset
is zero, since otherwise the immediate is loaded into a register anyway.

The transl_memory_access function needs some slightly more complex
adoption. For all variants that do not construct the address in a
register before hand we must check that the offsets are multiples of the
word size and additionally if a symbol is used that the alignment of the
symbol is also a multiple of the word size. Therefore a new parameter is
introduced that allows checking the alignment.

In order to reduce the code duplication for the proofs these two
functions get an additional parameter in order to indicate wether the
offset needs to be a multiple of the word size or not.
Bug 30983

1 files changed, 169 insertions, 102 deletions

diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 89514d62..7268b407 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -805,6 +805,7 @@ Lemma accessind_load_correct:
   forall (A: Type) (inj: A -> preg)
        (instr1: A -> constant -> ireg -> instruction)
        (instr2: A -> ireg -> ireg -> instruction)
+       (unaligned: bool)
        (base: ireg) ofs rx chunk v (rs: regset) m k,
   (forall rs m r1 cst r2,
    exec_instr ge fn (instr1 r1 cst r2) rs m = load1 ge chunk (inj r1) cst r2 rs m) ->
@@ -813,14 +814,15 @@ Lemma accessind_load_correct:
   Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
   base <> GPR0 -> inj rx <> PC ->
   exists rs',
-     exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m
+     exec_straight ge fn (accessind instr1 instr2 unaligned base ofs rx k) rs m k rs' m
   /\ rs'#(inj rx) = v
   /\ forall r, r <> PC -> r <> inj rx -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
   intros. unfold accessind. set (ofs' := Ptrofs.to_int ofs) in *.
+  set (ofs_mod := unaligned || Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *.
   assert (LD: Mem.loadv chunk m (Val.add (rs base) (Vint ofs')) = Some v)
   by (apply loadv_offset_ptr; auto).
-  destruct (Int.eq (high_s ofs') Int.zero).
+  destruct (Int.eq (high_s ofs') Int.zero && ofs_mod).
 - econstructor; split. apply exec_straight_one.
   rewrite H. unfold load1. rewrite gpr_or_zero_not_zero by auto. simpl.
   rewrite LD. eauto. unfold nextinstr. repeat Simplif.
@@ -862,6 +864,7 @@ Lemma accessind_store_correct:
   forall (A: Type) (inj: A -> preg)
        (instr1: A -> constant -> ireg -> instruction)
        (instr2: A -> ireg -> ireg -> instruction)
+       (unaligned: bool)
        (base: ireg) ofs rx chunk (rs: regset) m m' k,
   (forall rs m r1 cst r2,
    exec_instr ge fn (instr1 r1 cst r2) rs m = store1 ge chunk (inj r1) cst r2 rs m) ->
@@ -870,13 +873,14 @@ Lemma accessind_store_correct:
   Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs (inj rx)) = Some m' ->
   base <> GPR0 -> inj rx <> PC -> inj rx <> GPR0 ->
   exists rs',
-     exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m'
+     exec_straight ge fn (accessind instr1 instr2 unaligned base ofs rx k) rs m k rs' m'
   /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r.
 Proof.
   intros. unfold accessind. set (ofs' := Ptrofs.to_int ofs) in *.
+  set (ofs_mod := unaligned || Int.eq (Int.mods ofs' (Int.repr 4)) Int.zero) in *.
   assert (ST: Mem.storev chunk m (Val.add (rs base) (Vint ofs')) (rs (inj rx)) = Some m')
   by (apply storev_offset_ptr; auto).
-  destruct (Int.eq (high_s ofs') Int.zero).
+  destruct (Int.eq (high_s ofs') Int.zero && ofs_mod).
 - econstructor; split. apply exec_straight_one.
   rewrite H. unfold store1. rewrite gpr_or_zero_not_zero by auto. simpl.
   rewrite ST. eauto. unfold nextinstr. repeat Simplif.
@@ -1540,8 +1544,8 @@ Qed.
 (** Translation of memory accesses *)
 
 Lemma transl_memory_access_correct:
-  forall (P: regset -> Prop) mk1 mk2 addr args temp k c (rs: regset) a m m',
-  transl_memory_access mk1 mk2 addr args temp k = OK c ->
+  forall (P: regset -> Prop) mk1 mk2 unaligned addr args temp k c (rs: regset) a m m',
+  transl_memory_access mk1 mk2 unaligned addr args temp k = OK c ->
   eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a ->
   temp <> GPR0 ->
   (forall cst (r1: ireg) (rs1: regset) k,
@@ -1559,111 +1563,174 @@ Lemma transl_memory_access_correct:
 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 *)
-  case (Int.eq (high_s i) Int.zero).
-  (* Aindexed short *)
-  apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  (* Aindexed long *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
-  exploit (MK1 (Cint (low_s i)) temp rs1 k).
-    simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
-    unfold rs1; Simpl. rewrite Val.add_assoc.
-Transparent Val.add.
-    simpl. rewrite low_high_s. auto.
-    intros; unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'. split. apply exec_straight_step with rs1 m.
-  simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  auto. auto.
-  (* Aindexed2 *)
-  apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  (* Aglobal *)
-  destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR.
-  (* Aglobal from small data *)
-  apply MK1. unfold const_low. rewrite small_data_area_addressing by auto.
-  rewrite add_zero_symbol_address. auto.
-  auto.
-  (* Aglobal from relative data *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
-  set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))).
-  exploit (MK1 (Cint Int.zero) temp rs2).
-    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
-    unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address. auto.
-    intros; unfold rs2, rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m; auto.
-  apply exec_straight_step with rs2 m; auto. simpl. unfold rs2.
-  rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal.
-  unfold rs1; Simpl. apply low_high_half_zero.
-  eexact EX'. auto.
-  (* Aglobal from absolute data *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
-  exploit (MK1 (Csymbol_low i i0) temp rs1).
-    simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
-    unfold rs1. Simpl. rewrite low_high_half_zero. auto.
-    intros; unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m; auto.
-  eexact EX'. auto.
-  (* Abased *)
+  - (* 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.
+    (* Aindexed 4 aligned long *)
+    + set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (Vint (Int.shl (high_s i) (Int.repr 16)))))).
+      exploit (MK1 (Cint (low_s i)) temp rs1 k).
+      simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
+      unfold rs1; Simpl. rewrite Val.add_assoc.
+      Transparent Val.add.
+      simpl. rewrite low_high_s. auto.
+      intros; unfold rs1; Simpl.
+      intros [rs' [EX' AG']].
+      exists rs'. split. apply exec_straight_step with rs1 m.
+      simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+      auto. auto.
+    + (* Aindexed non 4 aligned *)
+      exploit (loadimm_correct GPR0 i (mk2 x GPR0 :: k) rs).
+      intros (rs' & A & B & C).
+      exploit (MK2 x GPR0 rs').
+      rewrite gpr_or_zero_not_zero; eauto with asmgen.
+      rewrite B. rewrite C; eauto with asmgen. auto.
+      intros.  destruct H as [rs'' [A1 B1]]. exists rs''.
+      split. eapply exec_straight_trans. exact A. exact A1. auto.
+  - (* Aindexed2 *)
+    apply MK2. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+  - (* Aglobal *)
+    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).
+      apply MK1. unfold const_low. rewrite small_data_area_addressing by auto.
+      rewrite add_zero_symbol_address. auto. auto.
+      (* Aglobal from small data not aligned *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add (gpr_or_zero rs GPR0) (const_low ge (Csymbol_sda i i0))))).
+      exploit (MK1 (Cint Int.zero) temp rs1). rewrite gpr_or_zero_not_zero; auto.
+      unfold const_low. unfold rs1. Simpl.
+      rewrite gpr_or_zero_zero. unfold const_low.
+      rewrite small_data_area_addressing by auto.
+      rewrite add_zero_symbol_address. rewrite Val.add_commut.
+      rewrite add_zero_symbol_address. auto.
+      intros. unfold rs1. Simpl.
+      intros. destruct H as [rs2 [A B]].
+      exists rs2. split. eapply exec_straight_step. reflexivity.
+      reflexivity. eexact A. apply B.
+    + (* relative data *)
+        set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
+        set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))).
+        exploit (MK1 (Cint Int.zero) temp rs2).
+        simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
+        unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address. auto.
+        intros; unfold rs2, rs1; Simpl.
+        intros [rs' [EX' AG']].
+        exists rs'; split. apply exec_straight_step with rs1 m; auto.
+        apply exec_straight_step with rs2 m; auto. simpl. unfold rs2.
+        rewrite gpr_or_zero_not_zero by eauto with asmgen. f_equal. f_equal. f_equal.
+        unfold rs1; Simpl. apply low_high_half_zero.
+        eexact EX'. auto.
+    + (* Aglobal from absolute data *)
+      destruct (unaligned || symbol_ofs_word_aligned i i0).
+      (* Aglobal 4 aligned *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
+      exploit (MK1 (Csymbol_low i i0) temp rs1).
+      simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
+      unfold rs1. Simpl. rewrite low_high_half_zero. auto.
+      intros; unfold rs1; Simpl.
+      intros [rs' [EX' AG']].
+      exists rs'; split. apply exec_straight_step with rs1 m; auto.
+      eexact EX'. auto.
+      (* Aglobal non aligned *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))).
+      set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))).
+      exploit (MK1 (Cint Int.zero) temp rs2).
+      simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
+      unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address.
+      auto. intros; unfold rs2, rs1; Simpl.
+      intros [rs' [EX' AG']].
+      exists rs'; split. apply exec_straight_step with rs1 m; auto.
+      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 *)
   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))).
-  exploit (MK2 x GPR0 rs1 k).
+  + (* Abased from small data *)
+    set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))).
+    exploit (MK2 x GPR0 rs1 k).
     simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen.
     unfold rs1; Simpl. rewrite Val.add_commut. auto.
     intros. unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'; split. apply exec_straight_step with rs1 m.
-  unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal.
-  unfold const_low. rewrite small_data_area_addressing; auto.
-  apply add_zero_symbol_address.
-  reflexivity.
-  assumption. assumption.
-  (* Abased from relative data *)
-  set (rs1 := nextinstr (rs#GPR0 <- (rs#x))).
-  set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))).
-  set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))).
-  exploit (MK2 temp GPR0 rs3).
+    intros [rs' [EX' AG']].
+    exists rs'; split. apply exec_straight_step with rs1 m.
+    unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal.
+    unfold const_low. rewrite small_data_area_addressing; auto.
+    apply add_zero_symbol_address.
+    reflexivity.
+    assumption. assumption.
+  + (* Abased from relative data *)
+    set (rs1 := nextinstr (rs#GPR0 <- (rs#x))).
+    set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))).
+    set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))).
+    exploit (MK2 temp GPR0 rs3).
     rewrite gpr_or_zero_not_zero by eauto with asmgen.
     f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl.
     intros. unfold rs3, rs2, rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m).
-  apply exec_straight_three with rs1 m rs2 m; auto.
-  simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto.
-  unfold rs2; Simpl. apply low_high_half_zero.
-  eexact EX'. auto.
-  (* Abased absolute *)
-  set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge i i0)))).
-  exploit (MK1 (Csymbol_low i i0) temp rs1 k).
+    intros [rs' [EX' AG']].
+    exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m).
+    apply exec_straight_three with rs1 m rs2 m; auto.
+    simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto.
+    unfold rs2; Simpl. apply low_high_half_zero.
+    eexact EX'. auto.
+  + (* Abased absolute *)
+    destruct (unaligned || symbol_ofs_word_aligned i i0).
+    (* Abased absolute 4 aligned *)
+    set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (high_half ge i i0)))).
+    exploit (MK1 (Csymbol_low i i0) temp rs1 k).
     simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen.
     unfold rs1. Simpl.
     rewrite Val.add_assoc. rewrite low_high_half. rewrite Val.add_commut. auto.
     intros; unfold rs1; Simpl.
-  intros [rs' [EX' AG']].
-  exists rs'. split. apply exec_straight_step with rs1 m.
-  unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  assumption. assumption.
-  (* Ainstack *)
-  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. }
-  destruct (Int.eq (high_s ofs) Int.zero); inv TR.
-  apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
-  exploit (MK1 (Cint (low_s ofs)) temp rs1 k).
-    simpl. rewrite gpr_or_zero_not_zero; auto.
-    unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
-    rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
-    congruence.
-    intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
-  intros [rs' [EX' AG']].
-  exists rs'. split. apply exec_straight_step with rs1 m.
-  unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
-  assumption. assumption.
+    intros [rs' [EX' AG']].
+    exists rs'. split. apply exec_straight_step with rs1 m.
+    unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+    assumption. assumption.
+    (* Abased absolute non aligned *)
+    set (rs1 := nextinstr (rs#GPR0 <- (rs#x))).
+    set (rs2 := nextinstr (rs1#temp <- (Val.add Vzero (high_half ge i i0)))).
+    set (rs3 := nextinstr (rs2#temp <- (Genv.symbol_address ge i i0))).
+    exploit (MK2 temp GPR0 rs3).
+    rewrite gpr_or_zero_not_zero by eauto with asmgen.
+    f_equal. unfold rs3; Simpl. unfold rs3, rs2, rs1; Simpl.
+    intros. unfold rs3, rs2, rs1; Simpl.
+    intros [rs' [EX' AG']].
+    exists rs'. split. eapply exec_straight_trans with (rs2 := rs3) (m2 := m).
+    apply exec_straight_three with rs1 m rs2 m; auto.
+    simpl. unfold rs3. f_equal. f_equal. f_equal. rewrite gpr_or_zero_not_zero by auto.
+    unfold rs2; Simpl. apply low_high_half_zero.
+    eexact EX'. auto.
+  - (* Ainstack *)
+    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. }
+    destruct (unaligned || Int.eq (Int.mods ofs (Int.repr 4)) Int.zero); [destruct (Int.eq (high_s ofs) Int.zero)|]; inv TR.
+    + (* Ainstack short *)
+      apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+    + (* Ainstack non short *)
+      set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s ofs) (Int.repr 16)))))).
+      exploit (MK1 (Cint (low_s ofs)) temp rs1 k).
+      simpl. rewrite gpr_or_zero_not_zero; auto.
+      unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
+      rewrite Val.add_assoc. simpl. rewrite low_high_s. auto.
+      congruence.
+      intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto.
+      intros [rs' [EX' AG']].
+      exists rs'. split. apply exec_straight_step with rs1 m.
+      unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto.
+      assumption. assumption.
+    + (* Ainstack non aligned *)
+      exploit (addimm_correct temp GPR1 ofs  (mk1 (Cint Int.zero) temp :: k) rs); eauto with asmgen.
+      intros [rs1 [A [B C]]].
+      exploit (MK1 (Cint Int.zero) temp rs1 k).
+      rewrite gpr_or_zero_not_zero; auto. rewrite B. simpl.
+      destruct (rs GPR1); auto.  simpl. rewrite Ptrofs.add_zero.
+      unfold ofs. rewrite Ptrofs.of_int_to_int. auto. auto.
+      intros. rewrite C; auto. intros [rs2 [EX' AG']].
+      exists rs2. split; auto.
+      eapply exec_straight_trans. eexact A. assumption.
 Qed.
 
+
 (** Translation of loads *)
 
 Lemma transl_load_correct:
@@ -1679,8 +1746,8 @@ Proof.
   intros.
   assert (LD: forall v, Val.lessdef a v -> v = a).
   { intros. inv H2; auto. discriminate H1. }
-  assert (BASE: forall mk1 mk2 k' chunk' v',
-  transl_memory_access mk1 mk2 addr args GPR12 k' = OK c ->
+  assert (BASE: forall mk1 mk2 unaligned k' chunk' v',
+  transl_memory_access mk1 mk2 unaligned addr args GPR12 k' = OK c ->
   Mem.loadv chunk' m a = Some v' ->
   (forall cst (r1: ireg) (rs1: regset),
     exec_instr ge fn (mk1 cst r1) rs1 m =
@@ -1758,8 +1825,8 @@ Local Transparent destroyed_by_store.
     subst src; simpl; congruence.
     change (IR GPR12) with (preg_of R12). red; intros; elim n.
     eapply preg_of_injective; eauto.
-  assert (BASE: forall mk1 mk2 chunk',
-  transl_memory_access mk1 mk2 addr args (int_temp_for src) k = OK c ->
+  assert (BASE: forall mk1 mk2 unaligned chunk',
+  transl_memory_access mk1 mk2 unaligned addr args (int_temp_for src) k = OK c ->
   Mem.storev chunk' m a (rs (preg_of src)) = Some m' ->
   (forall cst (r1: ireg) (rs1: regset),
     exec_instr ge fn (mk1 cst r1) rs1 m =