Merge remote-tracking branch 'origin/mppa-work' into mppa-thread

5 files changed, 329 insertions, 207 deletions

diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index d36b6230..7e36abf8 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -63,44 +63,44 @@ let expand_storeind_ptr src base ofs =
 let int_param_regs   = [| X10; X11; X12; X13; X14; X15; X16; X17 |]
 let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |]
 
-let rec fixup_variadic_call pos tyl =
-  if pos < 8 then
+let rec fixup_variadic_call ri rf tyl =
+  if ri < 8 then
     match tyl with
     | [] ->
         ()
     | (Tint | Tany32) :: tyl ->
-        fixup_variadic_call (pos + 1) tyl
+        fixup_variadic_call (ri + 1) rf tyl
     | Tsingle :: tyl ->
-        let rs =float_param_regs.(pos)
-        and rd = int_param_regs.(pos) in
+        let rs = float_param_regs.(rf)
+        and rd = int_param_regs.(ri) in
         emit (Pfmvxs(rd, rs));
-        fixup_variadic_call (pos + 1) tyl
+        fixup_variadic_call (ri + 1) (rf + 1) tyl
     | Tlong :: tyl ->
-        let pos' = if Archi.ptr64 then pos + 1 else align pos 2 + 2 in
-        fixup_variadic_call pos' tyl
+        let ri' = if Archi.ptr64 then ri + 1 else align ri 2 + 2 in
+        fixup_variadic_call ri' rf tyl
     | (Tfloat | Tany64) :: tyl ->
         if Archi.ptr64 then begin
-          let rs = float_param_regs.(pos)
-          and rd = int_param_regs.(pos) in
+          let rs = float_param_regs.(rf)
+          and rd = int_param_regs.(ri) in
           emit (Pfmvxd(rd, rs));
-          fixup_variadic_call (pos + 1) tyl
+          fixup_variadic_call (ri + 1) (rf + 1) tyl
         end else begin
-          let pos = align pos 2 in
-          if pos < 8 then begin
-            let rs = float_param_regs.(pos)
-            and rd1 = int_param_regs.(pos)
-            and rd2 = int_param_regs.(pos + 1) in
+          let ri = align ri 2 in
+          if ri < 8 then begin
+            let rs = float_param_regs.(rf)
+            and rd1 = int_param_regs.(ri)
+            and rd2 = int_param_regs.(ri + 1) in
             emit (Paddiw(X2, X X2, Integers.Int.neg _16));
             emit (Pfsd(rs, X2, Ofsimm _0));
             emit (Plw(rd1, X2, Ofsimm _0));
             emit (Plw(rd2, X2, Ofsimm _4));
             emit (Paddiw(X2, X X2, _16));
-            fixup_variadic_call (pos + 2) tyl
+            fixup_variadic_call (ri + 2) (rf + 1) tyl
           end
         end
         
 let fixup_call sg =
-  if sg.sig_cc.cc_vararg then fixup_variadic_call 0 sg.sig_args
+  if sg.sig_cc.cc_vararg then fixup_variadic_call 0 0 sg.sig_args
 
 (* Handling of annotations *)
 
diff --git a/riscV/CSE2deps.v b/riscV/CSE2deps.v
new file mode 100644
index 00000000..8ab9242a
--- /dev/null
+++ b/riscV/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+     (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+  && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+  && ((ofsw + size_chunk chunkw <=? ofsr) ||
+      (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+  match addr, addr', args, args' with
+  | (Aindexed ofs), (Aindexed ofs'),
+    (base :: nil), (base' :: nil) =>
+    if peq base base'
+    then negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
+    else true  | _, _, _, _ => true
+  end.
diff --git a/riscV/CSE2depsproof.v b/riscV/CSE2depsproof.v
new file mode 100644
index 00000000..a3811e78
--- /dev/null
+++ b/riscV/CSE2depsproof.v
@@ -0,0 +1,127 @@
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Memory Registers Op RTL Maps.
+
+Require Import Globalenvs Values.
+Require Import Linking Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import CSE2 CSE2deps.
+Require Import Lia.
+
+Lemma ptrofs_size :
+  Ptrofs.wordsize = (if Archi.ptr64 then 64 else 32)%nat.
+Proof.
+  unfold Ptrofs.wordsize.
+  unfold Wordsize_Ptrofs.wordsize.
+  trivial.
+Qed.
+
+Lemma ptrofs_modulus :
+  Ptrofs.modulus = if Archi.ptr64 then 18446744073709551616 else 4294967296.
+Proof.
+  unfold Ptrofs.modulus.
+  rewrite ptrofs_size.
+  destruct Archi.ptr64; reflexivity.
+Qed.
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Section MEMORY_WRITE.
+  Variable m m2 : mem.
+  Variable chunkw chunkr : memory_chunk.
+  Variable base : val.
+  
+  Variable addrw addrr valw : val.
+  Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
+
+  Section INDEXED_AWAY.
+  Variable ofsw ofsr : ptrofs.
+  Hypothesis ADDRW : eval_addressing genv sp
+                       (Aindexed ofsw) (base :: nil) = Some addrw. 
+  Hypothesis ADDRR : eval_addressing genv sp
+                       (Aindexed ofsr) (base :: nil) = Some addrr.
+
+  Lemma load_store_away1 :
+    forall RANGEW : 0 <= Ptrofs.unsigned ofsw <= Ptrofs.modulus - largest_size_chunk,
+    forall RANGER : 0 <= Ptrofs.unsigned ofsr <= Ptrofs.modulus - largest_size_chunk,
+    forall SWAPPABLE :    Ptrofs.unsigned ofsw + size_chunk chunkw <= Ptrofs.unsigned ofsr
+                          \/ Ptrofs.unsigned ofsr + size_chunk chunkr <= Ptrofs.unsigned ofsw,
+    Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+
+  Proof.
+    intros.
+    
+    pose proof (max_size_chunk chunkr) as size_chunkr_bounded.
+    pose proof (max_size_chunk chunkw) as size_chunkw_bounded.
+    unfold largest_size_chunk in *.
+
+    rewrite ptrofs_modulus in *.
+    simpl in *.
+    inv ADDRR.
+    inv ADDRW.
+    destruct base; try discriminate.
+    eapply Mem.load_store_other with (chunk := chunkw) (v := valw) (b := b).
+    exact STORE.
+    right.
+
+    all: try (destruct (Ptrofs.unsigned_add_either i ofsr) as [OFSR | OFSR];
+              rewrite OFSR).
+    all: try (destruct (Ptrofs.unsigned_add_either i ofsw) as [OFSW | OFSW];
+              rewrite OFSW).
+    all: try rewrite ptrofs_modulus in *.
+    all: destruct Archi.ptr64.
+
+    all: intuition lia.
+  Qed.
+  
+  Theorem load_store_away :
+    can_swap_accesses_ofs (Ptrofs.unsigned ofsr) chunkr (Ptrofs.unsigned ofsw) chunkw = true ->
+    Mem.loadv chunkr m2 addrr = Mem.loadv chunkr m addrr.
+  Proof.
+    intro SWAP.
+    unfold can_swap_accesses_ofs in SWAP.
+    repeat rewrite andb_true_iff in SWAP.
+    repeat rewrite orb_true_iff in SWAP.
+    repeat rewrite Z.leb_le in SWAP.
+    apply load_store_away1.
+    all: tauto.
+  Qed.
+  End INDEXED_AWAY.
+End MEMORY_WRITE.
+End SOUNDNESS.
+
+
+Section SOUNDNESS.
+  Variable F V : Type.
+  Variable genv: Genv.t F V.
+  Variable sp : val.
+
+Lemma may_overlap_sound:
+  forall m m' : mem,
+  forall chunk addr args chunk' addr' args' v a a' rs,
+    (eval_addressing genv sp addr (rs ## args)) = Some a ->
+    (eval_addressing genv sp addr' (rs ## args')) = Some a' ->
+    (may_overlap chunk addr args chunk' addr' args') = false ->
+    (Mem.storev chunk m a v) = Some m' ->
+    (Mem.loadv chunk' m' a') = (Mem.loadv chunk' m  a').
+Proof.
+  intros until rs.
+  intros ADDR ADDR' OVERLAP STORE.
+  destruct addr; destruct addr'; try discriminate.
+  { (* Aindexed / Aindexed *)
+  destruct args as [ | base [ | ]]. 1,3: discriminate.
+  destruct args' as [ | base' [ | ]]. 1,3: discriminate.
+  simpl in OVERLAP.
+  destruct (peq base base'). 2: discriminate.
+  subst base'.
+  destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP.
+  2: discriminate.
+  simpl in *.
+  eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
+  }
+Qed.
+
+End SOUNDNESS.
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index 27d09d94..17326139 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -105,7 +105,9 @@ Definition is_float_reg (r: mreg) :=
   of function arguments), but this leaves much liberty in choosing actual
   locations.  To ensure binary interoperability of code generated by our
   compiler with libraries compiled by another compiler, we
-  implement the standard RISC-V conventions.  *)
+  implement the standard RISC-V conventions as found here:
+  https://github.com/riscv/riscv-elf-psabi-doc/blob/master/riscv-elf.md
+*)
 
 (** ** Location of function result *)
 
@@ -169,38 +171,32 @@ Qed.
 
 (** ** Location of function arguments *)
 
-(** The RISC-V ABI states the following convention for passing arguments
+(** The RISC-V ABI states the following conventions for passing arguments
   to a function:
 
-- Arguments are passed in registers when possible.
-
-- Up to eight integer registers (ai: int_param_regs) and up to eight
-  floating-point registers (fai: float_param_regs) are used for this
-  purpose.
-
-- If the arguments to a function are conceptualized as fields of a C
-  struct, each with pointer alignment, the argument registers are a
-  shadow of the first eight pointer-words of that struct. If argument
-  i < 8 is a floating-point type, it is passed in floating-point
-  register fa_i; otherwise, it is passed in integer register a_i.
-
-- When primitive arguments twice the size of a pointer-word are passed
-  on the stack, they are naturally aligned. When they are passed in the
-  integer registers, they reside in an aligned even-odd register pair,
-  with the even register holding the least-significant bits.
-
-- Floating-point arguments to variadic functions (except those that
-  are explicitly named in the parameter list) are passed in integer
-  registers.
-
-- The portion of the conceptual struct that is not passed in argument
-  registers is passed on the stack. The stack pointer sp points to the
-  first argument not passed in a register.
-
-The bit about variadic functions doesn't quite fit CompCert's model.
-We do our best by passing the FP arguments in registers, as usual,
-and reserving the corresponding integer registers, so that fixup
-code can be introduced in the Asmexpand pass.
+- RV64, not variadic: pass the first 8 integer arguments in
+  integer registers (a1...a8: int_param_regs), the first 8 FP arguments
+  in FP registers (fa1...fa8: float_param_regs), and the remaining
+  arguments on the stack, in 8-byte slots.
+
+- RV32, not variadic: same, but arguments of 64-bit integer type
+  are passed in two consecutive integer registers (a(i), a(i+1))
+  or in a(8) and on a 32-bit word on the stack.  Stack-allocated
+  arguments are aligned to their natural alignment.
+
+- RV64, variadic: pass the first 8 arguments in integer registers
+  (a1...a8), including FP arguments; pass the remaining arguments on
+  the stack, in 8-byte slots.
+
+- RV32, variadic: same, but arguments of 64-bit types (integers as well
+  as floats) are passed in two consecutive aligned integer registers
+  (a(2i), a(2i+1)).  
+
+The passing of FP arguments to variadic functions in integer registers
+doesn't quite fit CompCert's model.  We do our best by passing the FP
+arguments in registers, as usual, and reserving the corresponding
+integer registers, so that fixup code can be introduced in the
+Asmexpand pass.
 *)
 
 Definition int_param_regs :=
@@ -208,80 +204,84 @@ Definition int_param_regs :=
 Definition float_param_regs :=
   F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: F16 :: F17 :: nil.
 
-Definition one_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ)
-                           (rec: Z -> Z -> list (rpair loc)) :=
-  match list_nth_z regs rn with
+Definition int_arg (ri rf ofs: Z) (ty: typ)
+                   (rec: Z -> Z -> Z -> list (rpair loc)) :=
+  match list_nth_z int_param_regs ri with
   | Some r =>
-      One(R r) :: rec (rn + 1) ofs
+      One(R r) :: rec (ri + 1) rf ofs
   | None   =>
-      let ofs := align ofs (typealign ty) in
-      One(S Outgoing ofs ty) :: rec rn (ofs + (if Archi.ptr64 then 2 else typesize ty))
+      let ofs := align ofs (typesize ty) in
+      One(S Outgoing ofs ty)
+      :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
   end.
 
-Definition two_args (regs: list mreg) (rn: Z) (ofs: Z)
-                    (rec: Z -> Z -> list (rpair loc)) :=
-  let rn := align rn 2 in
-  match list_nth_z regs rn, list_nth_z regs (rn + 1) with
-  | Some r1, Some r2 =>
-      Twolong (R r2) (R r1) :: rec (rn + 2) ofs
-  | _, _ =>
-      let ofs := align ofs 2 in
-      Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) ::
-      rec rn (ofs + 2)
+Definition float_arg (va: bool) (ri rf ofs: Z) (ty: typ)
+                     (rec: Z -> Z -> Z -> list (rpair loc)) :=
+  match list_nth_z float_param_regs rf with
+  | Some r =>
+      if va then
+       (let ri' :=  (* reserve 1 or 2 aligned integer registers *)
+          if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2 in
+        if zle ri' 8 then
+            (* we have enough integer registers, put argument in FP reg
+               and fixup code will put it in one or two integer regs *)
+            One (R r) :: rec ri' (rf + 1) ofs
+        else
+            (* we are out of integer registers, pass argument on stack *)
+            let ofs := align ofs (typesize ty) in
+            One(S Outgoing ofs ty)
+            :: rec ri' rf (ofs + (if Archi.ptr64 then 2 else typesize ty)))
+      else
+        One (R r) :: rec ri (rf + 1) ofs
+  | None   =>
+      let ofs := align ofs (typesize ty) in
+      One(S Outgoing ofs ty)
+      :: rec ri rf (ofs + (if Archi.ptr64 then 2 else typesize ty))
   end.
 
-Definition hybrid_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ)
-                      (rec: Z -> Z -> list (rpair loc)) :=
-  let rn := align rn 2 in
-  match list_nth_z regs rn with
-  | Some r =>
-      One (R r) :: rec (rn + 2) ofs
-  | None =>
+Definition split_long_arg (va: bool) (ri rf ofs: Z)
+                          (rec: Z -> Z -> Z -> list (rpair loc)) :=
+  let ri := if va then align ri 2 else ri in
+  match list_nth_z int_param_regs ri, list_nth_z int_param_regs (ri + 1) with
+  | Some r1, Some r2 =>
+      Twolong (R r2) (R r1) :: rec (ri + 2) rf ofs
+  | Some r1, None =>
+      Twolong (S Outgoing ofs Tint) (R r1) :: rec (ri + 1) rf (ofs + 1)
+  | None, _ =>
       let ofs := align ofs 2 in
-      One (S Outgoing ofs ty) :: rec rn (ofs + 2)
+      Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) ::
+      rec ri rf (ofs + 2)
   end.
 
 Fixpoint loc_arguments_rec (va: bool)
-    (tyl: list typ) (r ofs: Z) {struct tyl} : list (rpair loc) :=
+    (tyl: list typ) (ri rf ofs: Z) {struct tyl} : list (rpair loc) :=
   match tyl with
   | nil => nil
   | (Tint | Tany32) as ty :: tys =>
-      one_arg int_param_regs r ofs ty (loc_arguments_rec va tys)
+      (* pass in one integer register or on stack *)
+      int_arg ri rf ofs ty (loc_arguments_rec va tys)
   | Tsingle as ty :: tys =>
-      one_arg float_param_regs r ofs ty (loc_arguments_rec va tys)
+      (* pass in one FP register or on stack.
+         If vararg, reserve 1 integer register. *)
+      float_arg va ri rf ofs ty (loc_arguments_rec va tys)
   | Tlong as ty :: tys =>
-      if Archi.ptr64
-      then one_arg int_param_regs r ofs ty (loc_arguments_rec va tys)
-      else two_args int_param_regs r ofs  (loc_arguments_rec va tys)
+      if Archi.ptr64 then
+        (* pass in one integer register or on stack *)
+        int_arg ri rf ofs ty (loc_arguments_rec va tys)
+      else
+        (* pass in register pair or on stack; align register pair if vararg *)
+        split_long_arg va ri rf ofs(loc_arguments_rec va tys)
   | (Tfloat | Tany64) as ty :: tys =>
-      if va && negb Archi.ptr64
-      then hybrid_arg float_param_regs r ofs ty (loc_arguments_rec va tys)
-      else one_arg float_param_regs r ofs ty (loc_arguments_rec va tys)
+      (* pass in one FP register or on stack.
+         If vararg, reserve 1 or 2 integer registers. *)
+      float_arg va ri rf ofs ty (loc_arguments_rec va tys)
   end.
 
 (** [loc_arguments s] returns the list of locations where to store arguments
   when calling a function with signature [s].  *)
 
 Definition loc_arguments (s: signature) : list (rpair loc) :=
-  loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0.
-
-(** [size_arguments s] returns the number of [Outgoing] slots used
-  to call a function with signature [s]. *)
-
-Definition max_outgoing_1 (accu: Z) (l: loc) : Z :=
-  match l with
-  | S Outgoing ofs ty => Z.max accu (ofs + typesize ty)
-  | _ => accu
-  end.
-
-Definition max_outgoing_2 (accu: Z) (rl: rpair loc) : Z :=
-  match rl with
-  | One l => max_outgoing_1 accu l
-  | Twolong l1 l2 => max_outgoing_1 (max_outgoing_1 accu l1) l2
-  end.
-
-Definition size_arguments (s: signature) : Z :=
-  List.fold_left max_outgoing_2 (loc_arguments s) 0.
+  loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0 0.
 
 (** Argument locations are either non-temporary registers or [Outgoing]
   stack slots at nonnegative offsets. *)
@@ -294,90 +294,87 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
   end.
 
 Lemma loc_arguments_rec_charact:
-  forall va tyl rn ofs p,
+  forall va tyl ri rf ofs p,
   ofs >= 0 ->
-  In p (loc_arguments_rec va tyl rn ofs) -> forall_rpair loc_argument_acceptable p.
+  In p (loc_arguments_rec va tyl ri rf ofs) -> forall_rpair loc_argument_acceptable p.
 Proof.
   set (OK := fun (l: list (rpair loc)) =>
              forall p, In p l -> forall_rpair loc_argument_acceptable p).
-  set (OKF := fun (f: Z -> Z -> list (rpair loc)) =>
-              forall rn ofs, ofs >= 0 -> OK (f rn ofs)).
-  set (OKREGS := fun (l: list mreg) => forall r, In r l -> is_callee_save r = false).
-  assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typealign ty) >= 0).
+  set (OKF := fun (f: Z -> Z -> Z -> list (rpair loc)) =>
+              forall ri rf ofs, ofs >= 0 -> OK (f ri rf ofs)).
+  assert (CSI: forall r, In r int_param_regs -> is_callee_save r = false).
+  { decide_goal. }
+  assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false).
+  { decide_goal. }
+  assert (AL: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0).
   { intros. 
-    assert (ofs <= align ofs (typealign ty)) by (apply align_le; apply typealign_pos).
+    assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos).
     omega. }
+  assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))).
+  { intros. eapply Z.divide_trans. apply typealign_typesize.
+    apply align_divides. apply typesize_pos. }
   assert (SK: (if Archi.ptr64 then 2 else 1) > 0).
   { destruct Archi.ptr64; omega. }
   assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0).
   { intros. destruct Archi.ptr64. omega. apply typesize_pos.  }
-  assert (A: forall regs rn ofs ty f,
-             OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)).
-  { intros until f; intros OR OF OO; red; unfold one_arg; intros.
-    destruct (list_nth_z regs rn) as [r|] eqn:NTH; destruct H.
-  - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. 
+  assert (A: forall ri rf ofs ty f,
+             OKF f -> ofs >= 0 -> OK (int_arg ri rf ofs ty f)).
+  { intros until f; intros OF OO; red; unfold int_arg; intros.
+    destruct (list_nth_z int_param_regs ri) as [r|] eqn:NTH; destruct H.
+  - subst p; simpl. apply CSI. eapply list_nth_z_in; eauto. 
   - eapply OF; eauto. 
   - subst p; simpl. auto using align_divides, typealign_pos.
   - eapply OF; [idtac|eauto].
     generalize (AL ofs ty OO) (SKK ty); omega.
   }
-  assert (B: forall regs rn ofs f,
-             OKREGS regs -> OKF f -> ofs >= 0 -> OK (two_args regs rn ofs f)).
-  { intros until f; intros OR OF OO; unfold two_args.
-    set (rn' := align rn 2).
+  assert (B: forall va ri rf ofs ty f,
+             OKF f -> ofs >= 0 -> OK (float_arg va ri rf ofs ty f)).
+  { intros until f; intros OF OO; red; unfold float_arg; intros.
+    destruct (list_nth_z float_param_regs rf) as [r|] eqn:NTH.
+  - set (ri' := if Archi.ptr64 || zeq (typesize ty) 1 then ri + 1 else align ri 2 + 2) in *.
+    destruct va; [destruct (zle ri' 8)|idtac]; destruct H.
+    + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
+    + eapply OF; eauto.
+    + subst p; repeat split; auto.
+    + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
+    + subst p; simpl. apply CSF. eapply list_nth_z_in; eauto.
+    + eapply OF; eauto.
+  - destruct H.
+    + subst p; repeat split; auto.
+    + eapply OF; [idtac|eauto]. generalize (AL ofs ty OO) (SKK ty); omega.
+  }
+  assert (C: forall va ri rf ofs f,
+             OKF f -> ofs >= 0 -> OK (split_long_arg va ri rf ofs f)).
+  { intros until f; intros OF OO; unfold split_long_arg.
+    set (ri' := if va then align ri 2 else ri).
     set (ofs' := align ofs 2).
     assert (OO': ofs' >= 0) by (apply (AL ofs Tlong); auto).
-    assert (DFL: OK (Twolong (S Outgoing (ofs' + 1) Tint) (S Outgoing ofs' Tint)
-                     :: f rn' (ofs' + 2))).
-    { red; simpl; intros. destruct H.
-    - subst p; simpl. 
-      repeat split; auto using Z.divide_1_l. omega.
-    - eapply OF; [idtac|eauto]. omega.
-    }
-    destruct (list_nth_z regs rn') as [r1|] eqn:NTH1;
-    destruct (list_nth_z regs (rn' + 1)) as [r2|] eqn:NTH2;
-    try apply DFL.
-    red; simpl; intros; destruct H.
-  - subst p; simpl. split; apply OR; eauto using list_nth_z_in.  
-  - eapply OF; [idtac|eauto]. auto.
-  }
-  assert (C: forall regs rn ofs ty f,
-             OKREGS regs -> OKF f -> ofs >= 0 -> typealign ty = 1 -> OK (hybrid_arg regs rn ofs ty f)).
-  { intros until f; intros OR OF OO OTY; unfold hybrid_arg; red; intros.
-    set (rn' := align rn 2) in *.
-    destruct (list_nth_z regs rn') as [r|] eqn:NTH; destruct H.
-  - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. 
-  - eapply OF; eauto. 
-  - subst p; simpl. rewrite OTY. split. apply (AL ofs Tlong OO). apply Z.divide_1_l. 
-  - eapply OF; [idtac|eauto]. generalize (AL ofs Tlong OO); simpl; omega.
+    destruct (list_nth_z int_param_regs ri') as [r1|] eqn:NTH1;
+    [destruct (list_nth_z int_param_regs (ri'+1)) as [r2|] eqn:NTH2 | idtac].
+  - red; simpl; intros; destruct H.
+    + subst p; split; apply CSI; eauto using list_nth_z_in.
+    + eapply OF; [idtac|eauto]. omega.
+  - red; simpl; intros; destruct H.
+    + subst p; split. split; auto using Z.divide_1_l. apply CSI; eauto using list_nth_z_in.
+    + eapply OF; [idtac|eauto]. omega.
+  - red; simpl; intros; destruct H.
+    + subst p; repeat split; auto using Z.divide_1_l. omega. 
+    + eapply OF; [idtac|eauto]. omega.
   }
-  assert (D: OKREGS int_param_regs).
-  { red. decide_goal. }
-  assert (E: OKREGS float_param_regs).
-  { red. decide_goal. }
-
-  cut (forall va tyl rn ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl rn ofs)).
+  cut (forall va tyl ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec va tyl ri rf ofs)).
   unfold OK. eauto.
   induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl.
 - red; simpl; tauto.
 - destruct ty1.
 + (* int *) apply A; auto.
-+ (* float *) 
-  destruct (va && negb Archi.ptr64).
-  apply C; auto.
-  apply A; auto.
++ (* float *) apply B; auto.
 + (* long *)
   destruct Archi.ptr64.
   apply A; auto.
-  apply B; auto.
-+ (* single *)
-  apply A; auto.
-+ (* any32 *)
-  apply A; auto.
-+ (* any64 *)
-  destruct (va && negb Archi.ptr64).
   apply C; auto.
-  apply A; auto.
++ (* single *) apply B; auto.
++ (* any32 *) apply A; auto.
++ (* any64 *) apply B; auto.
 Qed.
 
 Lemma loc_arguments_acceptable:
@@ -387,52 +384,6 @@ Proof.
   unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. omega.
 Qed.
 
-(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
-
-Remark fold_max_outgoing_above:
-  forall l n, fold_left max_outgoing_2 l n >= n.
-Proof.
-  assert (A: forall n l, max_outgoing_1 n l >= n).
-  { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
-  induction l; simpl; intros. 
-  - omega.
-  - eapply Zge_trans. eauto.
-    destruct a; simpl. apply A. eapply Zge_trans; eauto.
-Qed.
-
-Lemma size_arguments_above:
-  forall s, size_arguments s >= 0.
-Proof.
-  intros. apply fold_max_outgoing_above.
-Qed.
-
-Lemma loc_arguments_bounded:
-  forall (s: signature) (ofs: Z) (ty: typ),
-  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
-  ofs + typesize ty <= size_arguments s.
-Proof.
-  intros until ty.
-  assert (A: forall n l, n <= max_outgoing_1 n l).
-  { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
-  assert (B: forall p n,
-             In (S Outgoing ofs ty) (regs_of_rpair p) ->
-             ofs + typesize ty <= max_outgoing_2 n p).
-  { intros. destruct p; simpl in H; intuition; subst; simpl.
-  - xomega.
-  - eapply Z.le_trans. 2: apply A. xomega.
-  - xomega. }
-  assert (C: forall l n,
-             In (S Outgoing ofs ty) (regs_of_rpairs l) ->
-             ofs + typesize ty <= fold_left max_outgoing_2 l n).
-  { induction l; simpl; intros.
-  - contradiction.
-  - rewrite in_app_iff in H. destruct H.
-  + eapply Z.le_trans. eapply B; eauto. apply Z.ge_le. apply fold_max_outgoing_above.
-  + apply IHl; auto.
-  }
-  apply C. 
-Qed.
-
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
 Proof.
diff --git a/riscV/DuplicateOpcodeHeuristic.ml b/riscV/DuplicateOpcodeHeuristic.ml
index 85505245..2ec314c1 100644
--- a/riscV/DuplicateOpcodeHeuristic.ml
+++ b/riscV/DuplicateOpcodeHeuristic.ml
@@ -1,3 +1,27 @@
-exception HeuristicSucceeded
-        
-let opcode_heuristic code cond ifso ifnot preferred = ()
+(* open Camlcoq *)
+open Op
+open Integers
+
+let opcode_heuristic code cond ifso ifnot is_loop_header =
+  match cond with
+  | Ccompimm (c, n) | Ccompuimm (c, n) -> if n == Integers.Int.zero then (match c with
+      | Clt | Cle -> Some false
+      | Cgt | Cge -> Some true
+      | _ -> None
+      ) else None
+  | Ccomplimm (c, n) | Ccompluimm (c, n) -> if n == Integers.Int64.zero then (match c with
+      | Clt | Cle -> Some false
+      | Cgt | Cge -> Some true
+      | _ -> None
+      ) else None
+  | Ccompf c | Ccompfs c -> (match c with
+      | Ceq -> Some false
+      | Cne -> Some true
+      | _ -> None
+      )
+  | Cnotcompf c | Cnotcompfs c -> (match c with
+      | Ceq -> Some true
+      | Cne -> Some false
+      | _ -> None
+      )
+  | _ -> None