Merge branch 'kvx-work' into kvx-work-merge3.8

Conflicts:
	Makefile
	configure

11 files changed, 577 insertions, 242 deletions

diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 8678a5dc..d2255e66 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -1035,7 +1035,9 @@ Opaque Int.eq.
   intros (rs' & A & B & C).
   exists rs'; split; eauto. rewrite B; auto with asmgen.
 - (* shrximm *)
-  clear H. exploit Val.shrx_shr_3; eauto. intros E; subst v; clear EV.
+  destruct (Val.shrx (rs x0) (Vint n)) eqn:TOTAL; cbn.
+  {
+  exploit Val.shrx_shr_3; eauto. intros E; subst v.
   destruct (Int.eq n Int.zero).
 + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
   split; intros; Simpl. 
@@ -1052,6 +1054,24 @@ Opaque Int.eq.
     eapply exec_straight_step. simpl; reflexivity. auto. 
     apply exec_straight_one. simpl; reflexivity. auto. 
     split; intros; Simpl.
+  }
+  destruct (Int.eq n Int.zero).
++ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros; Simpl. 
++ destruct (Int.eq n Int.one).
+  * econstructor; split.
+    eapply exec_straight_step. simpl; reflexivity. auto.
+    eapply exec_straight_step. simpl; reflexivity. auto.
+    apply exec_straight_one. simpl; reflexivity. auto.
+    split; intros; Simpl.
+  * change (Int.repr 32) with Int.iwordsize. set (n' := Int.sub Int.iwordsize n).
+    econstructor; split.
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    apply exec_straight_one. simpl; reflexivity. auto. 
+    split; intros; Simpl.
+  
 - (* longofintu *)
   econstructor; split.
   eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. auto. auto. auto.
@@ -1076,7 +1096,27 @@ Opaque Int.eq.
   intros (rs' & A & B & C).
   exists rs'; split; eauto. rewrite B; auto with asmgen.
 - (* shrxlimm *)
-  clear H. exploit Val.shrxl_shrl_3; eauto. intros E; subst v; clear EV.
+  destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL.
+  {
+   exploit Val.shrxl_shrl_3; eauto. intros E; subst v.
+  destruct (Int.eq n Int.zero).
++ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
+  split; intros; Simpl. 
++ destruct (Int.eq n Int.one).
+  * econstructor; split.
+    eapply exec_straight_step. simpl; reflexivity. auto.
+    eapply exec_straight_step. simpl; reflexivity. auto.
+    apply exec_straight_one. simpl; reflexivity. auto.
+    split; intros; Simpl.
+
+  * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n).
+    econstructor; split.
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    eapply exec_straight_step. simpl; reflexivity. auto. 
+    apply exec_straight_one. simpl; reflexivity. auto. 
+    split; intros; Simpl.
+  }
   destruct (Int.eq n Int.zero).
 + econstructor; split. apply exec_straight_one. simpl; eauto. auto.
   split; intros; Simpl. 
@@ -1094,6 +1134,7 @@ Opaque Int.eq.
     eapply exec_straight_step. simpl; reflexivity. auto. 
     apply exec_straight_one. simpl; reflexivity. auto. 
     split; intros; Simpl.
+  
 - (* cond *)
   exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
   exists rs'; split. eexact A. eauto with asmgen.
diff --git a/riscV/CSE2deps.v b/riscV/CSE2deps.v
index b4b80e2f..c0deacf0 100644
--- a/riscV/CSE2deps.v
+++ b/riscV/CSE2deps.v
@@ -28,5 +28,8 @@ Definition may_overlap chunk addr args chunk' addr' args' :=
     (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
+    else true
+  | (Ainstack ofs), (Ainstack ofs'), _, _ =>
+    negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
+  | _, _, _, _ => true
   end.
diff --git a/riscV/CSE2depsproof.v b/riscV/CSE2depsproof.v
index f283c8ac..cf9e62b1 100644
--- a/riscV/CSE2depsproof.v
+++ b/riscV/CSE2depsproof.v
@@ -123,7 +123,7 @@ Proof.
   intros until rs.
   intros ADDR ADDR' OVERLAP STORE.
   destruct addr; destruct addr'; try discriminate.
-  { (* Aindexed / Aindexed *)
+- (* Aindexed / Aindexed *)
   destruct args as [ | base [ | ]]. 1,3: discriminate.
   destruct args' as [ | base' [ | ]]. 1,3: discriminate.
   simpl in OVERLAP.
@@ -133,7 +133,15 @@ Proof.
   2: discriminate.
   simpl in *.
   eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
-  }
+
+- (* Ainstack / Ainstack *)
+  destruct args. 2: discriminate.
+  destruct args'. 2: discriminate.
+  cbn in OVERLAP.
+  destruct (can_swap_accesses_ofs (Ptrofs.unsigned i0) chunk' (Ptrofs.unsigned i) chunk) eqn:SWAP.
+  2: discriminate.
+  cbn in *.
+  eapply load_store_away with (F:=F) (V:=V) (genv:=genv) (sp:=sp); eassumption.
 Qed.
 
 End SOUNDNESS.
diff --git a/riscV/ConstpropOpproof.v b/riscV/ConstpropOpproof.v
index 765aa035..26a50317 100644
--- a/riscV/ConstpropOpproof.v
+++ b/riscV/ConstpropOpproof.v
@@ -265,52 +265,84 @@ Qed.
 
 Lemma make_divimm_correct:
   forall n r1 r2 v,
-  Val.divs e#r1 e#r2 = Some v ->
+  Val.maketotal (Val.divs e#r1 e#r2) = v ->
   e#r2 = Vint n ->
   let (op, args) := make_divimm n r1 r2 in
   exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divimm.
-  predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H.
-  destruct (e#r1) eqn:?;
-    try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto);
-    inv H; auto.
-  destruct (Int.is_power2 n) eqn:?.
-  destruct (Int.ltu i (Int.repr 31)) eqn:?.
-  exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence.
-  exists v; auto.
-  exists v; auto.
+  predSpec Int.eq Int.eq_spec n Int.one; intros; subst; rewrite H0.
+  { destruct (e # r1) eqn:Er1.
+    all: try (cbn; exists (e # r1); split; auto; fail).
+    rewrite Val.divs_one.
+    cbn.
+    rewrite Er1.
+    exists (Vint i); split; auto.
+ }
+ destruct (Int.is_power2 n) eqn:Power2.
+ {
+    destruct (Int.ltu i (Int.repr 31)) eqn:iLT31.
+    {
+      cbn.
+      exists (Val.maketotal (Val.shrx e # r1 (Vint i))); split; auto.
+      destruct (Val.divs e # r1 (Vint n)) eqn:DIVS; cbn; auto.
+      rewrite Val.divs_pow2 with (y:=v) (n:=n).
+      cbn.
+      all: auto.
+    }
+    exists (Val.maketotal (Val.divs e # r1 (Vint n))); split; cbn; auto; congruence.
+ }
+ exists (Val.maketotal (Val.divs e # r1 (Vint n))); split; cbn; auto; congruence.
 Qed.
 
 Lemma make_divuimm_correct:
   forall n r1 r2 v,
-  Val.divu e#r1 e#r2 = Some v ->
+  Val.maketotal (Val.divu e#r1 e#r2) = v ->
   e#r2 = Vint n ->
   let (op, args) := make_divuimm n r1 r2 in
   exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divuimm.
-  predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H.
-  destruct (e#r1) eqn:?;
-    try (rewrite Val.divu_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto);
-    inv H; auto.
-  destruct (Int.is_power2 n) eqn:?.
-  econstructor; split. simpl; eauto.
-  rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto.
-  exists v; auto.
+  predSpec Int.eq Int.eq_spec n Int.one; intros; subst; rewrite H0.
+  { destruct (e # r1) eqn:Er1.
+    all: try (cbn; exists (e # r1); split; auto; fail).
+    rewrite Val.divu_one.
+    cbn.
+    rewrite Er1.
+    exists (Vint i); split; auto.
+ }
+ destruct (Int.is_power2 n) eqn:Power2.
+ {
+   cbn.
+   exists (Val.shru e # r1 (Vint i)); split; auto.
+   destruct (Val.divu e # r1 (Vint n)) eqn:DIVU; cbn; auto.
+   rewrite Val.divu_pow2 with (y:=v) (n:=n).
+   all: auto.
+ }
+ exists (Val.maketotal (Val.divu e # r1 (Vint n))); split; cbn; auto; congruence.
 Qed.
 
 Lemma make_moduimm_correct:
   forall n r1 r2 v,
-  Val.modu e#r1 e#r2 = Some v ->
+  Val.maketotal (Val.modu e#r1 e#r2) = v ->
   e#r2 = Vint n ->
   let (op, args) := make_moduimm n r1 r2 in
   exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_moduimm.
   destruct (Int.is_power2 n) eqn:?.
-  exists v; split; auto. simpl. decEq. eapply Val.modu_pow2; eauto. congruence.
-  exists v; auto.
+  { destruct (Val.modu e # r1 e # r2) eqn:MODU; cbn in H.
+    { subst v0.
+      exists v; split; auto.
+      cbn. decEq. eapply Val.modu_pow2; eauto. congruence.
+    }
+    subst v.
+    eexists; split; auto.
+    cbn. reflexivity.
+  }
+  exists v; split; auto.
+  cbn.
+  congruence.
 Qed.
 
 Lemma make_andimm_correct:
@@ -444,48 +476,82 @@ Qed.
 
 Lemma make_divlimm_correct:
   forall n r1 r2 v,
-  Val.divls e#r1 e#r2 = Some v ->
+  Val.maketotal (Val.divls e#r1 e#r2) = v ->
   e#r2 = Vlong n ->
   let (op, args) := make_divlimm n r1 r2 in
   exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divlimm.
-  destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?.
-  rewrite H0 in H. econstructor; split. simpl; eauto. eapply Val.divls_pow2; eauto. auto.
-  exists v; auto.
-  exists v; auto.
+ destruct (Int64.is_power2' n) eqn:Power2.
+ {
+    destruct (Int.ltu i (Int.repr 63)) eqn:iLT63.
+    {
+      cbn.
+      exists (Val.maketotal (Val.shrxl e # r1 (Vint i))); split; auto.
+      rewrite H0 in H.
+      destruct (Val.divls e # r1 (Vlong n)) eqn:DIVS; cbn in H; auto.
+      {
+        subst v0.
+        rewrite Val.divls_pow2 with (y:=v) (n:=n).
+        cbn.
+        all: auto.
+      }
+      subst. auto.
+    }
+    cbn. subst. rewrite H0.
+    exists (Val.maketotal (Val.divls e # r1 (Vlong n))); split; auto.
+ }
+ cbn. subst. rewrite H0.
+ exists (Val.maketotal (Val.divls e # r1 (Vlong n))); split; auto.
 Qed.
 
 Lemma make_divluimm_correct:
   forall n r1 r2 v,
-  Val.divlu e#r1 e#r2 = Some v ->
+  Val.maketotal (Val.divlu e#r1 e#r2) = v ->
   e#r2 = Vlong n ->
   let (op, args) := make_divluimm n r1 r2 in
   exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divluimm.
   destruct (Int64.is_power2' n) eqn:?.
+  {
   econstructor; split. simpl; eauto.
-  rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2.
-  simpl.
-  erewrite Int64.is_power2'_range by eauto.    
-  erewrite Int64.divu_pow2' by eauto.  auto. 
-  exists v; auto.
+  rewrite H0 in H. destruct (e#r1); inv H.
+  all: cbn; auto.
+  { 
+    destruct (Int64.eq n Int64.zero); cbn; auto.
+    erewrite Int64.is_power2'_range by eauto.    
+    erewrite Int64.divu_pow2' by eauto.  auto.
+  }
+  }
+  exists v; split; auto.
+  cbn.
+  rewrite H.
+  reflexivity.
 Qed.
 
 Lemma make_modluimm_correct:
   forall n r1 r2 v,
-  Val.modlu e#r1 e#r2 = Some v ->
+  Val.maketotal (Val.modlu e#r1 e#r2) = v ->
   e#r2 = Vlong n ->
   let (op, args) := make_modluimm n r1 r2 in
   exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_modluimm.
   destruct (Int64.is_power2 n) eqn:?.
-  exists v; split; auto. simpl. decEq.
-  rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. 
-  simpl. erewrite Int64.modu_and by eauto. auto.
-  exists v; auto.
+  {
+  econstructor; split. simpl; eauto.
+  rewrite H0 in H. destruct (e#r1); inv H.
+  all: cbn; auto.
+  { 
+    destruct (Int64.eq n Int64.zero); cbn; auto.
+    erewrite Int64.modu_and by eauto.  auto.
+  }
+  }
+  exists v; split; auto.
+  cbn.
+  rewrite H.
+  reflexivity.
 Qed.
 
 Lemma make_andlimm_correct:
@@ -633,14 +699,17 @@ Proof.
 - (* mul 2*)
   InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto.
 - (* divs *)
-  assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
-  apply make_divimm_correct; auto.
+  assert (e#r2 = Vint n2). { clear H0. InvApproxRegs; SimplVM; auto. }
+                           apply make_divimm_correct; auto.
+  congruence.
 - (* divu *)
   assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_divuimm_correct; auto.
+  congruence.
 - (* modu *)
   assert (e#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_moduimm_correct; auto.
+  congruence.
 - (* and 1 *)
   rewrite Val.and_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_andimm_correct; auto.
 - (* and 2 *)
@@ -680,12 +749,15 @@ Proof.
 - (* divl *)
   assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_divlimm_correct; auto.
+  congruence.
 - (* divlu *)
   assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_divluimm_correct; auto.
+  congruence.
 - (* modlu *)
   assert (e#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto.
   apply make_modluimm_correct; auto.
+  congruence.
 - (* andl 1 *)
   rewrite Val.andl_commut in H0. InvApproxRegs; SimplVM; inv H0. apply make_andlimm_correct; auto.
 - (* andl 2 *)
diff --git a/riscV/Op.v b/riscV/Op.v
index 14d07e0b..62999a2f 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -241,10 +241,10 @@ Definition eval_operation
   | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2)
   | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2)
   | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2)
-  | Odiv, v1 :: v2 :: nil => Val.divs v1 v2
-  | Odivu, v1 :: v2 :: nil => Val.divu v1 v2
-  | Omod, v1 :: v2 :: nil => Val.mods v1 v2
-  | Omodu, v1 :: v2 :: nil => Val.modu v1 v2
+  | Odiv, v1 :: v2 :: nil => Some (Val.maketotal (Val.divs v1 v2))
+  | Odivu, v1 :: v2 :: nil => Some (Val.maketotal (Val.divu v1 v2))
+  | Omod, v1 :: v2 :: nil => Some (Val.maketotal (Val.mods v1 v2))
+  | Omodu, v1 :: v2 :: nil => Some (Val.maketotal (Val.modu v1 v2))
   | Oand, v1 :: v2 :: nil => Some (Val.and v1 v2)
   | Oandimm n, v1 :: nil => Some (Val.and v1 (Vint n))
   | Oor, v1 :: v2 :: nil => Some (Val.or v1 v2)
@@ -257,7 +257,7 @@ Definition eval_operation
   | Oshrimm n, v1 :: nil => Some (Val.shr v1 (Vint n))
   | Oshru, v1 :: v2 :: nil => Some (Val.shru v1 v2)
   | Oshruimm n, v1 :: nil => Some (Val.shru v1 (Vint n))
-  | Oshrximm n, v1::nil => Val.shrx v1 (Vint n)
+  | Oshrximm n, v1::nil => Some (Val.maketotal (Val.shrx v1 (Vint n)))
   | Omakelong, v1::v2::nil => Some (Val.longofwords v1 v2)
   | Olowlong, v1::nil => Some (Val.loword v1)
   | Ohighlong, v1::nil => Some (Val.hiword v1)
@@ -270,10 +270,10 @@ Definition eval_operation
   | Omull, v1::v2::nil => Some (Val.mull v1 v2)
   | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2)
   | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2)
-  | Odivl, v1::v2::nil => Val.divls v1 v2
-  | Odivlu, v1::v2::nil => Val.divlu v1 v2
-  | Omodl, v1::v2::nil => Val.modls v1 v2
-  | Omodlu, v1::v2::nil => Val.modlu v1 v2
+  | Odivl, v1::v2::nil => Some (Val.maketotal (Val.divls v1 v2))
+  | Odivlu, v1::v2::nil => Some (Val.maketotal (Val.divlu v1 v2))
+  | Omodl, v1::v2::nil => Some (Val.maketotal (Val.modls v1 v2))
+  | Omodlu, v1::v2::nil => Some (Val.maketotal (Val.modlu v1 v2))
   | Oandl, v1::v2::nil => Some(Val.andl v1 v2)
   | Oandlimm n, v1::nil => Some (Val.andl v1 (Vlong n))
   | Oorl, v1::v2::nil => Some(Val.orl v1 v2)
@@ -286,7 +286,7 @@ Definition eval_operation
   | Oshrlimm n, v1::nil => Some (Val.shrl v1 (Vint n))
   | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2)
   | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n))
-  | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n)
+  | Oshrxlimm n, v1::nil => Some (Val.maketotal (Val.shrxl v1 (Vint n)))
   | Onegf, v1::nil => Some (Val.negf v1)
   | Oabsf, v1::nil => Some (Val.absf v1)
   | Oaddf, v1::v2::nil => Some (Val.addf v1 v2)
@@ -301,22 +301,22 @@ Definition eval_operation
   | Odivfs, v1::v2::nil => Some (Val.divfs v1 v2)
   | Osingleoffloat, v1::nil => Some (Val.singleoffloat v1)
   | Ofloatofsingle, v1::nil => Some (Val.floatofsingle v1)
-  | Ointoffloat, v1::nil => Val.intoffloat v1
-  | Ointuoffloat, v1::nil => Val.intuoffloat v1
-  | Ofloatofint, v1::nil => Val.floatofint v1
-  | Ofloatofintu, v1::nil => Val.floatofintu v1
-  | Ointofsingle, v1::nil => Val.intofsingle v1
-  | Ointuofsingle, v1::nil => Val.intuofsingle v1
-  | Osingleofint, v1::nil => Val.singleofint v1
-  | Osingleofintu, v1::nil => Val.singleofintu v1
-  | Olongoffloat, v1::nil => Val.longoffloat v1
-  | Olonguoffloat, v1::nil => Val.longuoffloat v1
-  | Ofloatoflong, v1::nil => Val.floatoflong v1
-  | Ofloatoflongu, v1::nil => Val.floatoflongu v1
-  | Olongofsingle, v1::nil => Val.longofsingle v1
-  | Olonguofsingle, v1::nil => Val.longuofsingle v1
-  | Osingleoflong, v1::nil => Val.singleoflong v1
-  | Osingleoflongu, v1::nil => Val.singleoflongu v1
+  | Ointoffloat, v1::nil => Some (Val.maketotal (Val.intoffloat v1))
+  | Ointuoffloat, v1::nil => Some (Val.maketotal (Val.intuoffloat v1))
+  | Ofloatofint, v1::nil => Some (Val.maketotal (Val.floatofint v1))
+  | Ofloatofintu, v1::nil => Some (Val.maketotal (Val.floatofintu v1))
+  | Ointofsingle, v1::nil => Some (Val.maketotal (Val.intofsingle v1))
+  | Ointuofsingle, v1::nil => Some (Val.maketotal (Val.intuofsingle v1))
+  | Osingleofint, v1::nil => Some (Val.maketotal (Val.singleofint v1))
+  | Osingleofintu, v1::nil => Some (Val.maketotal (Val.singleofintu v1))
+  | Olongoffloat, v1::nil => Some (Val.maketotal (Val.longoffloat v1))
+  | Olonguoffloat, v1::nil => Some (Val.maketotal (Val.longuoffloat v1))
+  | Ofloatoflong, v1::nil => Some (Val.maketotal (Val.floatoflong v1))
+  | Ofloatoflongu, v1::nil => Some (Val.maketotal (Val.floatoflongu v1))
+  | Olongofsingle, v1::nil => Some (Val.maketotal (Val.longofsingle v1))
+  | Olonguofsingle, v1::nil => Some (Val.maketotal (Val.longuofsingle v1))
+  | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1))
+  | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
   | _, _ => None
   end.
@@ -539,15 +539,17 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
   (* div, divu *)
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int.eq i0 Int.zero); inv H2...
+  - destruct v0; destruct v1; cbn; trivial.
+    destruct (Int.eq i0 Int.zero
+         || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn; trivial.
+  - destruct v0; destruct v1; cbn; trivial.
+    destruct (Int.eq i0 Int.zero); cbn; trivial.
   (* mod, modu *)
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int.eq i0 Int.zero); inv H2...
+  - destruct v0; destruct v1; cbn; trivial.
+    destruct (Int.eq i0 Int.zero
+         || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn; trivial.
+  - destruct v0; destruct v1; cbn; trivial.
+    destruct (Int.eq i0 Int.zero); cbn; trivial.
   (* and, andimm *)
   - destruct v0; destruct v1...
   - destruct v0...
@@ -567,7 +569,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
   - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
   (* shrx *)
-  - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 31)); inv H0...
+  - destruct v0; cbn; trivial.
+    destruct (Int.ltu n (Int.repr 31)); cbn; trivial.
   (* makelong, lowlong, highlong *)
   - destruct v0; destruct v1...
   - destruct v0...
@@ -588,15 +591,19 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
   (* divl, divlu *)
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2...
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int64.eq i0 Int64.zero); inv H2...
+  - destruct v0; destruct v1; cbn; trivial.
+    destruct (Int64.eq i0 Int64.zero
+         || Int64.eq i (Int64.repr (-9223372036854775808)) &&
+            Int64.eq i0 Int64.mone); cbn; trivial.
+  - destruct v0; destruct v1; cbn; trivial.
+    destruct (Int64.eq i0 Int64.zero); cbn; trivial.
   (* modl, modlu *)
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2...
-  - destruct v0; destruct v1; simpl in *; inv H0.
-    destruct (Int64.eq i0 Int64.zero); inv H2...
+  - destruct v0; destruct v1; cbn; trivial.
+    destruct (Int64.eq i0 Int64.zero
+         || Int64.eq i (Int64.repr (-9223372036854775808)) &&
+            Int64.eq i0 Int64.mone); cbn; trivial.
+  - destruct v0; destruct v1; cbn; trivial.
+    destruct (Int64.eq i0 Int64.zero); cbn; trivial.
   (* andl, andlimm *)
   - destruct v0; destruct v1...
   - destruct v0...
@@ -616,7 +623,8 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
   - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
   (* shrxl *)
-  - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0...
+  - destruct v0; cbn; trivial.
+    destruct (Int.ltu n (Int.repr 63)); cbn; trivial.
   (* negf, absf *)
   - destruct v0...
   - destruct v0...
@@ -639,50 +647,47 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0...
   - destruct v0...
   (* intoffloat, intuoffloat *)
-  - destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2...
-  - destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); inv H2...
+  - destruct v0; cbn; trivial.
+    destruct (Float.to_int f); cbn; trivial.
+  - destruct v0; cbn; trivial.
+    destruct (Float.to_intu f); cbn; trivial.
   (* floatofint, floatofintu *)
-  - destruct v0; simpl in H0; inv H0...
-  - destruct v0; simpl in H0; inv H0...
+  - destruct v0; cbn; trivial.
+  - destruct v0; cbn; trivial.
   (* intofsingle, intuofsingle *)
-  - destruct v0; simpl in H0; inv H0. destruct (Float32.to_int f); inv H2...
-  - destruct v0; simpl in H0; inv H0. destruct (Float32.to_intu f); inv H2...
+  - destruct v0; cbn; trivial.
+    destruct (Float32.to_int f); cbn; trivial.
+  - destruct v0; cbn; trivial.
+    destruct (Float32.to_intu f); cbn; trivial.
   (* singleofint, singleofintu *)
-  - destruct v0; simpl in H0; inv H0...
-  - destruct v0; simpl in H0; inv H0...
+  - destruct v0; cbn; trivial.
+  - destruct v0; cbn; trivial.
   (* longoffloat, longuoffloat *)
-  - destruct v0; simpl in H0; inv H0. destruct (Float.to_long f); inv H2...
-  - destruct v0; simpl in H0; inv H0. destruct (Float.to_longu f); inv H2...
+  - destruct v0; cbn; trivial.
+    destruct (Float.to_long f); cbn; trivial.
+  - destruct v0; cbn; trivial.
+    destruct (Float.to_longu f); cbn; trivial.
   (* floatoflong, floatoflongu *)
-  - destruct v0; simpl in H0; inv H0...
-  - destruct v0; simpl in H0; inv H0...
+  - destruct v0; cbn; trivial.
+  - destruct v0; cbn; trivial.
   (* longofsingle, longuofsingle *)
-  - destruct v0; simpl in H0; inv H0. destruct (Float32.to_long f); inv H2...
-  - destruct v0; simpl in H0; inv H0. destruct (Float32.to_longu f); inv H2...
+  - destruct v0; cbn; trivial.
+    destruct (Float32.to_long f); cbn; trivial.
+  - destruct v0; cbn; trivial.
+    destruct (Float32.to_longu f); cbn; trivial.
   (* singleoflong, singleoflongu *)
-  - destruct v0; simpl in H0; inv H0...
-  - destruct v0; simpl in H0; inv H0...
+  - destruct v0; cbn; trivial.
+  - destruct v0; cbn; trivial.
   (* cmp *)
   - destruct (eval_condition cond vl m)... destruct b...
 Qed.
 
-
+(* This should not be simplified to "false" because it breaks proofs elsewhere. *)
 Definition is_trapping_op (op : operation) :=
   match op with
-  | Odiv | Odivl | Odivu | Odivlu
-  | Omod | Omodl | Omodu | Omodlu
-  | Oshrximm _ | Oshrxlimm _
-  | Ointoffloat | Ointuoffloat
-  | Ointofsingle | Ointuofsingle
-  | Olongoffloat | Olonguoffloat
-  | Olongofsingle | Olonguofsingle
-  | Osingleofint | Osingleofintu
-  | Osingleoflong | Osingleoflongu
-  | Ofloatofint | Ofloatofintu
-  | Ofloatoflong | Ofloatoflongu => true
+  | Omove => false
   | _ => false
   end.
-                
 
 Definition args_of_operation op :=
   if eq_operation op Omove
@@ -872,6 +877,16 @@ Proof.
   unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
+Lemma op_valid_pointer_eq:
+  forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
+Proof.
+  intros until m2. destruct op; simpl; try congruence.
+  intros MEM; destruct cond; repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+
 (** Global variables mentioned in an operation or addressing mode *)
 
 Definition globals_addressing (addr: addressing) : list ident :=
@@ -1033,19 +1048,29 @@ Proof.
   - inv H4; inv H2; simpl; auto.
   - inv H4; inv H2; simpl; auto.
   (* div, divu *)
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
+  - inv H4; inv H2; cbn.
+    all: try apply Val.val_inject_undef.
     destruct (Int.eq i0 Int.zero
-              || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2.
-    TrivialExists.
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
-    destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
+              || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn.
+    apply Val.val_inject_undef.
+    apply Val.inject_int.
+  - inv H4; inv H2; cbn.
+    all: try apply Val.val_inject_undef.
+    destruct (Int.eq i0 Int.zero); cbn.
+    apply Val.val_inject_undef.
+    apply Val.inject_int.
   (* mod, modu *)
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
+  - inv H4; inv H2; cbn.
+    all: try apply Val.val_inject_undef.
     destruct (Int.eq i0 Int.zero
-                     || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2.
-    TrivialExists.
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
-    destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
+              || Int.eq i (Int.repr (-2147483648)) && Int.eq i0 Int.mone); cbn.
+    apply Val.val_inject_undef.
+    apply Val.inject_int.
+  - inv H4; inv H2; cbn.
+    all: try apply Val.val_inject_undef.
+    destruct (Int.eq i0 Int.zero); cbn.
+    apply Val.val_inject_undef.
+    apply Val.inject_int.
   (* and, andimm *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
@@ -1065,8 +1090,10 @@ Proof.
   - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
   - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
   (* shrx *)
-  - inv H4; simpl in H1; try discriminate. simpl.
-    destruct (Int.ltu n (Int.repr 31)); inv H1. TrivialExists.
+  - inv H4; cbn; try apply Val.val_inject_undef.
+    destruct (Int.ltu n (Int.repr 31)); cbn.
+    apply Val.inject_int.
+    apply Val.val_inject_undef.
   (* makelong, highlong, lowlong *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
@@ -1085,19 +1112,31 @@ Proof.
   - inv H4; inv H2; simpl; auto.
   - inv H4; inv H2; simpl; auto.
   (* divl, divlu *)
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
+  - inv H4; inv H2; cbn.
+    all: try apply Val.val_inject_undef.
     destruct (Int64.eq i0 Int64.zero
-              || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2.
-    TrivialExists.
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
-    destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists.
+         || Int64.eq i (Int64.repr (-9223372036854775808)) &&
+            Int64.eq i0 Int64.mone); cbn.
+    apply Val.val_inject_undef.
+    apply Val.inject_long.
+  - inv H4; inv H2; cbn.
+    all: try apply Val.val_inject_undef.
+    destruct (Int64.eq i0 Int64.zero); cbn.
+    apply Val.val_inject_undef.
+    apply Val.inject_long.
   (* modl, modlu *)
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
+  - inv H4; inv H2; cbn.
+    all: try apply Val.val_inject_undef.
     destruct (Int64.eq i0 Int64.zero
-                     || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2.
-    TrivialExists.
-  - inv H4; inv H3; simpl in H1; inv H1. simpl.
-    destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists.
+         || Int64.eq i (Int64.repr (-9223372036854775808)) &&
+            Int64.eq i0 Int64.mone); cbn.
+    apply Val.val_inject_undef.
+    apply Val.inject_long.
+  - inv H4; inv H2; cbn.
+    all: try apply Val.val_inject_undef.
+    destruct (Int64.eq i0 Int64.zero); cbn.
+    apply Val.val_inject_undef.
+    apply Val.inject_long.
   (* andl, andlimm *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
@@ -1116,9 +1155,11 @@ Proof.
   (* shru, shruimm *)
   - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
   - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
-  (* shrx *)
-  - inv H4; simpl in H1; try discriminate. simpl.
-    destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists.
+    (* shrx *)
+  - inv H4; cbn; try apply Val.val_inject_undef.
+    destruct (Int.ltu n (Int.repr 63)); cbn.
+    apply Val.inject_long.
+    apply Val.val_inject_undef.
   (* negf, absf *)
   - inv H4; simpl; auto.
   - inv H4; simpl; auto.
@@ -1141,37 +1182,37 @@ Proof.
   - inv H4; simpl; auto.
   - inv H4; simpl; auto.
   (* intoffloat, intuoffloat *)
-  - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2.
-    exists (Vint i); auto.
-  - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2.
-    exists (Vint i); auto.
+  - inv H4; cbn; auto.
+    destruct (Float.to_int f0); cbn; auto.
+  - inv H4; cbn; auto.
+    destruct (Float.to_intu f0); cbn; auto.
   (* floatofint, floatofintu *)
-  - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
-  - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* intofsingle, intuofsingle *)
-  - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_int f0); simpl in H2; inv H2.
-    exists (Vint i); auto.
-  - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_intu f0); simpl in H2; inv H2.
-    exists (Vint i); auto.
+  - inv H4; cbn; auto.
+    destruct (Float32.to_int f0); cbn; auto.
+  - inv H4; cbn; auto.
+    destruct (Float32.to_intu f0); cbn; auto.
   (* singleofint, singleofintu *)
-  - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
-  - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* longoffloat, longuoffloat *)
-  - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_long f0); simpl in H2; inv H2.
-    exists (Vlong i); auto.
-  - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_longu f0); simpl in H2; inv H2.
-    exists (Vlong i); auto.
+  - inv H4; cbn; auto.
+    destruct (Float.to_long f0); cbn; auto.
+  - inv H4; cbn; auto.
+    destruct (Float.to_longu f0); cbn; auto.
   (* floatoflong, floatoflongu *)
-  - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
-  - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* longofsingle, longuofsingle *)
-  - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_long f0); simpl in H2; inv H2.
-    exists (Vlong i); auto.
-  - inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_longu f0); simpl in H2; inv H2.
-    exists (Vlong i); auto.
+  - inv H4; cbn; auto.
+    destruct (Float32.to_long f0); cbn; auto.
+  - inv H4; cbn; auto.
+    destruct (Float32.to_longu f0); cbn; auto.
   (* singleoflong, singleoflongu *)
-  - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
-  - inv H4; simpl in H1; inv H1. simpl. TrivialExists.
+  - inv H4; cbn; auto.
+  - inv H4; cbn; auto.
   (* cmp *)
   - subst v1. destruct (eval_condition cond vl1 m1) eqn:?.
     exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml
new file mode 100644
index 00000000..75a913c6
--- /dev/null
+++ b/riscV/OpWeights.ml
@@ -0,0 +1,161 @@
+open Op;;
+open PrepassSchedulingOracleDeps;;
+
+module Rocket =
+  struct
+    (* Attempt at modeling the Rocket core *)
+    
+    let resource_bounds = [| 1 |];;
+    let nr_non_pipelined_units = 1;; (* divider *)
+    
+    let latency_of_op (op : operation) (nargs : int) =
+      match op with
+      | Omul  | Omulhs  | Omulhu
+        | Omull | Omullhs | Omullhu -> 4
+                                     
+      | Onegf -> 1               (*r [rd = - r1] *)
+      | Oabsf                    (*r [rd = abs(r1)] *)
+        | Oaddf                    (*r [rd = r1 + r2] *)
+        | Osubf                    (*r [rd = r1 - r2] *)
+        | Omulf -> 6               (*r [rd = r1 * r2] *)
+      | Onegfs -> 1              (*r [rd = - r1] *)
+      | Oabsfs                   (*r [rd = abs(r1)] *)
+        | Oaddfs                   (*r [rd = r1 + r2] *)
+        | Osubfs                   (*r [rd = r1 - r2] *)
+        | Omulfs -> 4              (*r [rd = r1 * r2] *)
+      | Osingleoffloat           (*r [rd] is [r1] truncated to single-precision float *)
+        | Ofloatofsingle -> 4      (*r [rd] is [r1] extended to double-precision float *)
+      (*c Conversions between int and float: *)
+      | Ointoffloat              (*r [rd = signed_int_of_float64(r1)] *)
+        | Ointuoffloat             (*r [rd = unsigned_int_of_float64(r1)] *)
+        | Ofloatofint              (*r [rd = float64_of_signed_int(r1)] *)
+        | Ofloatofintu -> 6        (*r [rd = float64_of_unsigned_int(r1)] *)
+      | Ointofsingle             (*r [rd = signed_int_of_float32(r1)] *)
+        | Ointuofsingle            (*r [rd = unsigned_int_of_float32(r1)] *)
+        | Osingleofint             (*r [rd = float32_of_signed_int(r1)] *)
+        | Osingleofintu -> 4       (*r [rd = float32_of_unsigned_int(r1)] *)
+      | Olongoffloat             (*r [rd = signed_long_of_float64(r1)] *)
+        | Olonguoffloat            (*r [rd = unsigned_long_of_float64(r1)] *)
+        | Ofloatoflong             (*r [rd = float64_of_signed_long(r1)] *)
+        | Ofloatoflongu -> 6       (*r [rd = float64_of_unsigned_long(r1)] *)
+      | Olongofsingle            (*r [rd = signed_long_of_float32(r1)] *)
+        | Olonguofsingle           (*r [rd = unsigned_long_of_float32(r1)] *)
+        | Osingleoflong            (*r [rd = float32_of_signed_long(r1)] *)
+        | Osingleoflongu -> 4      (*r [rd = float32_of_unsigned_int(r1)] *)
+                          
+      | Odiv | Odivu | Odivl | Odivlu -> 16  
+      | Odivfs -> 35
+      | Odivf -> 50
+
+      | Ocmp cond ->
+         (match cond with
+          | Ccomp _
+            | Ccompu _
+            | Ccompimm _
+            | Ccompuimm _
+            | Ccompl _
+            | Ccomplu _
+            | Ccomplimm _
+            | Ccompluimm _ -> 1
+          | Ccompf _
+            | Cnotcompf _ -> 6
+          | Ccompfs _
+            | Cnotcompfs _ -> 4)
+      | _ -> 1;;
+    
+    let resources_of_op (op : operation) (nargs : int) = resource_bounds;;
+  
+    let non_pipelined_resources_of_op (op : operation) (nargs : int) =
+      match op with
+      | Odiv | Odivu -> [| 29 |]
+      | Odivfs -> [| 20 |]
+      | Odivl | Odivlu | Odivf -> [| 50 |]
+      | _ -> [| -1 |];;
+    
+    let resources_of_cond (cond : condition) (nargs : int) = resource_bounds;;
+
+    let latency_of_load trap chunk (addr : addressing) (nargs : int) = 3;;
+    let latency_of_call _ _ = 6;;
+    
+    let resources_of_load trap chunk addressing nargs = resource_bounds;;
+    
+    let resources_of_store chunk addressing nargs = resource_bounds;;
+    
+    let resources_of_call _ _ = resource_bounds;;
+    let resources_of_builtin _ = resource_bounds;;
+  end;;
+
+module SweRV_EH1 =
+  struct
+    (* Attempt at modeling SweRV EH1
+       [| issues ; LSU ; multiplier |] *)
+    let resource_bounds = [| 2 ; 1; 1 |];;
+    let nr_non_pipelined_units = 1;; (* divider *)
+    
+    let latency_of_op (op : operation) (nargs : int) =
+      match op with
+      | Omul  | Omulhs  | Omulhu
+        | Omull | Omullhs | Omullhu -> 3
+      | Odiv | Odivu | Odivl | Odivlu -> 16  
+      | _ -> 1;;
+    
+    let resources_of_op (op : operation) (nargs : int) = 
+      match op with
+      | Omul  | Omulhs  | Omulhu
+        | Omull | Omullhs | Omullhu -> [| 1 ; 0 ; 1 |]
+      | Odiv | Odivu | Odivl | Odivlu -> [| 0 ; 0; 0 |]                        
+      | _ -> [| 1; 0; 0; 0 |];;
+    
+    let non_pipelined_resources_of_op (op : operation) (nargs : int) =
+      match op with
+      | Odiv | Odivu -> [| 29 |]
+      | Odivfs -> [| 20 |]
+      | Odivl | Odivlu | Odivf -> [| 50 |]
+      | _ -> [| -1 |];;
+    
+    let resources_of_cond (cond : condition) (nargs : int) = [| 1; 0; 0 |];;
+    
+    let latency_of_load trap chunk (addr : addressing) (nargs : int) = 3;;
+    let latency_of_call _ _ = 6;;
+    
+    let resources_of_load trap chunk addressing nargs = [| 1; 1; 0 |];;
+    
+    let resources_of_store chunk addressing nargs = [| 1; 1; 0 |];;
+    
+    let resources_of_call _ _ = resource_bounds;;
+    let resources_of_builtin _ = resource_bounds;;
+  end;;
+
+let get_opweights () : opweights =
+  match !Clflags.option_mtune with
+  | "rocket" | "" ->
+     {
+       pipelined_resource_bounds = Rocket.resource_bounds;
+       nr_non_pipelined_units = Rocket.nr_non_pipelined_units;
+       latency_of_op = Rocket.latency_of_op;
+       resources_of_op = Rocket.resources_of_op;
+       non_pipelined_resources_of_op = Rocket.non_pipelined_resources_of_op;
+       latency_of_load = Rocket.latency_of_load;
+       resources_of_load = Rocket.resources_of_load;
+       resources_of_store = Rocket.resources_of_store;
+       resources_of_cond = Rocket.resources_of_cond;
+       latency_of_call = Rocket.latency_of_call;
+       resources_of_call = Rocket.resources_of_call;
+       resources_of_builtin = Rocket.resources_of_builtin
+     }
+  | "SweRV_EH1" | "EH1" ->
+     {
+       pipelined_resource_bounds = SweRV_EH1.resource_bounds;
+       nr_non_pipelined_units = SweRV_EH1.nr_non_pipelined_units;
+       latency_of_op = SweRV_EH1.latency_of_op;
+       resources_of_op = SweRV_EH1.resources_of_op;
+       non_pipelined_resources_of_op = SweRV_EH1.non_pipelined_resources_of_op;
+       latency_of_load = SweRV_EH1.latency_of_load;
+       resources_of_load = SweRV_EH1.resources_of_load;
+       resources_of_store = SweRV_EH1.resources_of_store;
+       resources_of_cond = SweRV_EH1.resources_of_cond;
+       latency_of_call = SweRV_EH1.latency_of_call;
+       resources_of_call = SweRV_EH1.resources_of_call;
+       resources_of_builtin = SweRV_EH1.resources_of_builtin
+     }
+  | xxx -> failwith (Printf.sprintf "unknown -mtune: %s" xxx);;
diff --git a/riscV/PrepassSchedulingOracle.ml b/riscV/PrepassSchedulingOracle.ml
new file mode 120000
index 00000000..912e9ffa
--- /dev/null
+++ b/riscV/PrepassSchedulingOracle.ml
@@ -0,0 +1 @@
+../aarch64/PrepassSchedulingOracle.ml
\ No newline at end of file
diff --git a/riscV/PrepassSchedulingOracleDeps.ml b/riscV/PrepassSchedulingOracleDeps.ml
new file mode 120000
index 00000000..1e955b85
--- /dev/null
+++ b/riscV/PrepassSchedulingOracleDeps.ml
@@ -0,0 +1 @@
+../aarch64/PrepassSchedulingOracleDeps.ml
\ No newline at end of file
diff --git a/riscV/SelectLongproof.v b/riscV/SelectLongproof.v
index d47b6d64..0fc578bf 100644
--- a/riscV/SelectLongproof.v
+++ b/riscV/SelectLongproof.v
@@ -455,6 +455,10 @@ Proof.
   unfold divls_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_divls_base; eauto.
   TrivialExists.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
 Qed.
 
 Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls.
@@ -462,6 +466,10 @@ Proof.
   unfold modls_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_modls_base; eauto.
   TrivialExists.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
 Qed.
 
 Theorem eval_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu.
@@ -469,6 +477,10 @@ Proof.
   unfold divlu_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_divlu_base; eauto.
   TrivialExists.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
 Qed.
 
 Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu.
@@ -476,6 +488,10 @@ Proof.
   unfold modlu_base; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_modlu_base; eauto.
   TrivialExists.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
 Qed.
 
 Theorem eval_shrxlimm:
@@ -490,33 +506,9 @@ Proof.
 - subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto.
   change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto.
 - TrivialExists.
-(*
-  intros. unfold shrxlimm. destruct Archi.splitlong eqn:SL.
-+ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32.
-+ destruct x; simpl in H0; try discriminate. 
-  destruct (Int.ltu n (Int.repr 63)) eqn:LTU; inv H0.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-  - subst n. exists (Vlong i); split; auto. rewrite Int64.shrx'_zero. auto.
-  - assert (NZ: Int.unsigned n <> 0).
-    { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
-    assert (LT: 0 <= Int.unsigned n < 63) by (apply Int.ltu_inv in LTU; assumption).
-    assert (LTU2: Int.ltu (Int.sub Int64.iwordsize' n) Int64.iwordsize' = true).
-    { unfold Int.ltu; apply zlt_true.
-      unfold Int.sub. change (Int.unsigned Int64.iwordsize') with 64. 
-      rewrite Int.unsigned_repr. omega. 
-      assert (64 < Int.max_unsigned) by reflexivity. omega. }
-    assert (X: eval_expr ge sp e m le
-               (Eop (Oshrlimm (Int.repr (Int64.zwordsize - 1))) (a ::: Enil))
-               (Vlong (Int64.shr' i (Int.repr (Int64.zwordsize - 1))))).
-    { EvalOp. }
-    assert (Y: eval_expr ge sp e m le (shrxlimm_inner a n)
-               (Vlong (Int64.shru' (Int64.shr' i (Int.repr (Int64.zwordsize - 1))) (Int.sub Int64.iwordsize' n)))).
-    { EvalOp. simpl. rewrite LTU2. auto. }
-    TrivialExists. 
-    constructor. EvalOp. simpl; eauto. constructor. 
-    simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int64.shrx'_shr_2 by auto. reflexivity. 
-    change (Int.unsigned Int64.iwordsize') with 64; omega.
-*)
+  cbn.
+  rewrite H0.
+  reflexivity.
 Qed.
 
 Theorem eval_cmplu:
@@ -566,6 +558,7 @@ Proof.
   unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_longoffloat; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 Theorem eval_longuoffloat: partial_unary_constructor_sound longuoffloat Val.longuoffloat.
@@ -573,6 +566,7 @@ Proof.
   unfold longuoffloat; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_longuoffloat; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong.
@@ -580,6 +574,7 @@ Proof.
   unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_floatoflong; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 Theorem eval_floatoflongu: partial_unary_constructor_sound floatoflongu Val.floatoflongu.
@@ -587,6 +582,7 @@ Proof.
   unfold floatoflongu; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_floatoflongu; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle.
@@ -594,6 +590,7 @@ Proof.
   unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_longofsingle; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle.
@@ -601,6 +598,7 @@ Proof.
   unfold longuofsingle; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_longuofsingle; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
@@ -608,6 +606,7 @@ Proof.
   unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_singleoflong; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu.
@@ -615,6 +614,7 @@ Proof.
   unfold singleoflongu; red; intros. destruct Archi.splitlong eqn:SL.
   eapply SplitLongproof.eval_singleoflongu; eauto.
   TrivialExists.
+  cbn; rewrite H0; reflexivity.
 Qed.
 
 End CMCONSTR.
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 7f2014dc..1d13702a 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -506,7 +506,12 @@ Theorem eval_divs_base:
     Val.divs x y = Some z ->
     exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold divs_base. exists z; split. EvalOp. auto.
+  intros. unfold divs_base. exists z; split. EvalOp.
+  2: apply Val.lessdef_refl.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
 Qed.
 
 Theorem eval_mods_base:
@@ -516,7 +521,12 @@ Theorem eval_mods_base:
     Val.mods x y = Some z ->
     exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold mods_base. exists z; split. EvalOp. auto.
+  intros. unfold mods_base. exists z; split. EvalOp.
+  2: apply Val.lessdef_refl.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
 Qed.
 
 Theorem eval_divu_base:
@@ -526,7 +536,12 @@ Theorem eval_divu_base:
     Val.divu x y = Some z ->
     exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold divu_base. exists z; split. EvalOp. auto.
+  intros. unfold divu_base. exists z; split. EvalOp.
+  2: apply Val.lessdef_refl.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
 Qed.
 
 Theorem eval_modu_base:
@@ -536,7 +551,12 @@ Theorem eval_modu_base:
     Val.modu x y = Some z ->
     exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold modu_base. exists z; split. EvalOp. auto.
+  intros. unfold modu_base. exists z; split. EvalOp.
+  2: apply Val.lessdef_refl.
+  cbn.
+  rewrite H1.
+  cbn.
+  trivial.
 Qed.
 
 Theorem eval_shrximm:
@@ -553,34 +573,12 @@ Proof.
   replace (Int.shrx i Int.zero) with i. auto.
   unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
   change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
-  econstructor; split. EvalOp. auto.
-(*
-  intros. destruct x; simpl in H0; try discriminate. 
-  destruct (Int.ltu n (Int.repr 31)) eqn:LTU; inv H0.
-  unfold shrximm.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-  - subst n. exists (Vint i); split; auto.
-    unfold Int.shrx, Int.divs. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto.
-  - assert (NZ: Int.unsigned n <> 0).
-    { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
-    assert (LT: 0 <= Int.unsigned n < 31) by (apply Int.ltu_inv in LTU; assumption).
-    assert (LTU2: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true).
-    { unfold Int.ltu; apply zlt_true.
-      unfold Int.sub. change (Int.unsigned Int.iwordsize) with 32. 
-      rewrite Int.unsigned_repr. omega. 
-      assert (32 < Int.max_unsigned) by reflexivity. omega. }
-    assert (X: eval_expr ge sp e m le
-               (Eop (Oshrimm (Int.repr (Int.zwordsize - 1))) (a ::: Enil))
-               (Vint (Int.shr i (Int.repr (Int.zwordsize - 1))))).
-    { EvalOp. }
-    assert (Y: eval_expr ge sp e m le (shrximm_inner a n)
-               (Vint (Int.shru (Int.shr i (Int.repr (Int.zwordsize - 1))) (Int.sub Int.iwordsize n)))).
-    { EvalOp. simpl. rewrite LTU2. auto. }
-    TrivialExists. 
-    constructor. EvalOp. simpl; eauto. constructor. 
-    simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int.shrx_shr_2 by auto. reflexivity. 
-    change (Int.unsigned Int.iwordsize) with 32; omega.
-*)
+  econstructor; split. EvalOp.
+  cbn.
+  rewrite H0.
+  cbn.
+  reflexivity.
+  apply Val.lessdef_refl.
 Qed.
 
 Theorem eval_shl: binary_constructor_sound shl Val.shl.
@@ -790,6 +788,7 @@ Theorem eval_intoffloat:
   exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold intoffloat. TrivialExists.
+  cbn. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_intuoffloat:
@@ -799,6 +798,7 @@ Theorem eval_intuoffloat:
   exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold intuoffloat. TrivialExists.
+  cbn. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_floatofintu:
@@ -810,6 +810,7 @@ Proof.
   intros until y; unfold floatofintu. case (floatofintu_match a); intros.
   InvEval. simpl in H0. TrivialExists.
   TrivialExists.
+  cbn. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_floatofint:
@@ -821,6 +822,7 @@ Proof.
   intros until y; unfold floatofint. case (floatofint_match a); intros.
   InvEval. simpl in H0. TrivialExists.
   TrivialExists.
+  cbn. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_intofsingle:
@@ -830,6 +832,7 @@ Theorem eval_intofsingle:
   exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold intofsingle. TrivialExists.
+  cbn. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_singleofint:
@@ -839,6 +842,7 @@ Theorem eval_singleofint:
   exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold singleofint; TrivialExists.
+  cbn. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_intuofsingle:
@@ -848,6 +852,7 @@ Theorem eval_intuofsingle:
   exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold intuofsingle. TrivialExists.
+  cbn. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_singleofintu:
@@ -857,6 +862,7 @@ Theorem eval_singleofintu:
   exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold intuofsingle. TrivialExists.
+  cbn. rewrite H0. reflexivity.
 Qed.
 
 Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 5670b5fe..f4b7b4d6 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -13,6 +13,7 @@
 Require Import Coqlib Compopts.
 Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op RTL ValueDomain.
+Require Import Zbits.
 
 (** Value analysis for RISC V operators *)
 
@@ -59,10 +60,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Omul, v1::v2::nil => mul v1 v2
   | Omulhs, v1::v2::nil => mulhs v1 v2
   | Omulhu, v1::v2::nil => mulhu v1 v2
-  | Odiv, v1::v2::nil => divs v1 v2
-  | Odivu, v1::v2::nil => divu v1 v2
-  | Omod, v1::v2::nil => mods v1 v2
-  | Omodu, v1::v2::nil => modu v1 v2
+  | Odiv, v1::v2::nil => divs_total v1 v2
+  | Odivu, v1::v2::nil => divu_total v1 v2
+  | Omod, v1::v2::nil => mods_total v1 v2
+  | Omodu, v1::v2::nil => modu_total v1 v2
   | Oand, v1::v2::nil => and v1 v2
   | Oandimm n, v1::nil => and v1 (I n)
   | Oor, v1::v2::nil => or v1 v2
@@ -88,10 +89,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Omull, v1::v2::nil => mull v1 v2
   | Omullhs, v1::v2::nil => mullhs v1 v2
   | Omullhu, v1::v2::nil => mullhu v1 v2
-  | Odivl, v1::v2::nil => divls v1 v2
-  | Odivlu, v1::v2::nil => divlu v1 v2
-  | Omodl, v1::v2::nil => modls v1 v2
-  | Omodlu, v1::v2::nil => modlu v1 v2
+  | Odivl, v1::v2::nil => divls_total v1 v2
+  | Odivlu, v1::v2::nil => divlu_total v1 v2
+  | Omodl, v1::v2::nil => modls_total v1 v2
+  | Omodlu, v1::v2::nil => modlu_total v1 v2
   | Oandl, v1::v2::nil => andl v1 v2
   | Oandlimm n, v1::nil => andl v1 (L n)
   | Oorl, v1::v2::nil => orl v1 v2
@@ -119,20 +120,20 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Odivfs, v1::v2::nil => divfs v1 v2
   | Osingleoffloat, v1::nil => singleoffloat v1
   | Ofloatofsingle, v1::nil => floatofsingle v1
-  | Ointoffloat, v1::nil => intoffloat v1
-  | Ointuoffloat, v1::nil => intuoffloat v1
+  | Ointoffloat, v1::nil => intoffloat_total v1
+  | Ointuoffloat, v1::nil => intuoffloat_total v1
   | Ofloatofint, v1::nil => floatofint v1
   | Ofloatofintu, v1::nil => floatofintu v1
-  | Ointofsingle, v1::nil => intofsingle v1
-  | Ointuofsingle, v1::nil => intuofsingle v1
+  | Ointofsingle, v1::nil => intofsingle_total v1
+  | Ointuofsingle, v1::nil => intuofsingle_total v1
   | Osingleofint, v1::nil => singleofint v1
   | Osingleofintu, v1::nil => singleofintu v1
-  | Olongoffloat, v1::nil => longoffloat v1
-  | Olonguoffloat, v1::nil => longuoffloat v1
+  | Olongoffloat, v1::nil => longoffloat_total v1
+  | Olonguoffloat, v1::nil => longuoffloat_total v1
   | Ofloatoflong, v1::nil => floatoflong v1
   | Ofloatoflongu, v1::nil => floatoflongu v1
-  | Olongofsingle, v1::nil => longofsingle v1
-  | Olonguofsingle, v1::nil => longuofsingle v1
+  | Olongofsingle, v1::nil => longofsingle_total v1
+  | Olonguofsingle, v1::nil => longuofsingle_total v1
   | Osingleoflong, v1::nil => singleoflong v1
   | Osingleoflongu, v1::nil => singleoflongu v1
   | Ocmp c, _ => of_optbool (eval_static_condition c vl)