maketotal mod & div

6 files changed, 593 insertions, 165 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/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..e953bd71 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)
@@ -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...
@@ -669,9 +677,6 @@ Qed.
 
 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
@@ -1033,19 +1038,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 +1080,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 +1102,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 +1145,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.
diff --git a/riscV/SelectLongproof.v b/riscV/SelectLongproof.v
index d47b6d64..f5e8edf8 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:
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index 7f2014dc..436cd4f3 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.
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 5670b5fe..5d1797ae 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -13,6 +13,300 @@
 Require Import Coqlib Compopts.
 Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op RTL ValueDomain.
+Require Import Zbits.
+
+Definition divs_total (v w: aval) := 
+  match w, v with
+  | I i2, I i1 =>
+      if Int.eq i2 Int.zero
+      || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
+      then ntop
+      else I (Int.divs i1 i2)
+  | _, _ => ntop2 v w
+  end.
+
+Lemma divs_total_sound1:
+  forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.divs v w = Some u -> vmatch bc u (divs_total x y).
+Proof.
+  intros until y.
+  intros HX HY VAL.
+  inv HX; inv HY; cbn in *.
+  { destruct (_ || _) eqn:E.
+    discriminate.
+    inv VAL.
+    auto with va.
+  }
+  all: try discriminate.
+  all: destruct (_ || _) eqn:E; inv VAL; unfold ntop2; auto with va.
+Qed.
+
+Lemma divs_total_sound:
+  forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divs v w)) (divs_total x y).
+Proof.
+  intros until y.
+  intros HX HY.
+  inv HX; inv HY; cbn in *.
+  { destruct (_ || _) eqn:E; cbn; unfold ntop; auto with va.
+  }
+  all: unfold ntop2; auto with va.
+  all: destruct (_ || _) eqn:E; unfold ntop2; cbn; auto with va.
+Qed.
+
+Definition divu_total (v w: aval) :=
+  match w, v with
+  | I i2, I i1 =>
+      if Int.eq i2 Int.zero
+       then ntop
+      else I (Int.divu i1 i2)
+  | _, _ => ntop2 v w
+  end.
+
+Lemma divu_total_sound1:
+  forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.divu v w = Some u -> vmatch bc u (divu_total x y).
+Proof.
+  intros until y.
+  intros HX HY VAL.
+  inv HX; inv HY; cbn in *.
+  { destruct Int.eq eqn:E.
+    discriminate.
+    inv VAL.
+    auto with va.
+  }
+  all: try discriminate.
+  all: destruct Int.eq eqn:E; inv VAL; unfold ntop2; auto with va.
+Qed.
+
+Lemma divu_total_sound:
+  forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divu v w)) (divu_total x y).
+Proof.
+  intros until y.
+  intros HX HY.
+  inv HX; inv HY; cbn in *.
+  { destruct Int.eq eqn:E; cbn; unfold ntop; auto with va.
+  }
+  all: unfold ntop2; auto with va.
+  all: destruct Int.eq eqn:E; unfold ntop2; cbn; auto with va.
+Qed.
+
+Definition mods_total (v w: aval) :=
+  match w, v with
+  | I i2, I i1 =>
+      if Int.eq i2 Int.zero
+      || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
+      then ntop
+      else I (Int.mods i1 i2)
+  | _, _ => ntop2 v w
+  end.
+
+Lemma mods_total_sound1:
+  forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.mods v w = Some u -> vmatch bc u (mods x y).
+Proof.
+  intros until y.
+  intros HX HY VAL.
+  inv HX; inv HY; cbn in *.
+  { destruct (_ || _) eqn:E.
+    discriminate.
+    inv VAL.
+    auto with va.
+  }
+  all: try discriminate.
+  all: destruct (_ || _) eqn:E; inv VAL; unfold ntop2; auto with va.
+Qed.
+
+Lemma mods_total_sound:
+  forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.mods v w)) (mods_total x y).
+Proof.
+  intros until y.
+  intros HX HY.
+  inv HX; inv HY; cbn in *.
+  { destruct (_ || _) eqn:E; cbn; unfold ntop; auto with va.
+  }
+  all: unfold ntop2; auto with va.
+  all: destruct (_ || _) eqn:E; unfold ntop2; cbn; auto with va.
+Qed.
+
+Definition modu_total (v w: aval) :=
+  match w, v with
+  | I i2, I i1 =>
+      if Int.eq i2 Int.zero
+      then ntop
+      else I (Int.modu i1 i2)
+  | I i2, _ => uns (provenance v) (usize i2)
+  | _, _ => ntop2 v w
+  end.
+
+Lemma modu_total_sound1:
+  forall bc v w u x y, vmatch bc v x -> vmatch bc w y -> Val.modu v w = Some u -> vmatch bc u (modu x y).
+Proof.
+  assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)).
+  {
+    intros. apply is_uns_mon with (usize (Int.modu i j)).
+    { apply is_uns_usize.
+    }
+    unfold usize, Int.size.
+    apply Zsize_monotone.
+    generalize (Int.unsigned_range_2 j); intros RANGE.
+    assert (Int.unsigned j <> 0).
+    { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
+    exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD.
+    unfold Int.modu. rewrite Int.unsigned_repr. omega. omega.
+  }
+  
+  intros until y.
+  intros HX HY VAL.
+  inv HX; inv HY; cbn in *.
+  { destruct Int.eq eqn:E.
+    discriminate.
+    inv VAL.
+    auto with va.
+  }
+  all: try discriminate.
+  all: destruct Int.eq eqn:E; inv VAL; unfold ntop2; auto with va.
+
+  all:
+    apply vmatch_uns;
+    apply UNS;
+    generalize (Int.eq_spec i0 Int.zero);
+    rewrite E;
+    auto.
+Qed.
+
+Lemma modu_total_sound:
+  forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.modu v w)) (modu_total x y).
+Proof.
+  assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)).
+  {
+    intros. apply is_uns_mon with (usize (Int.modu i j)).
+    { apply is_uns_usize.
+    }
+    unfold usize, Int.size.
+    apply Zsize_monotone.
+    generalize (Int.unsigned_range_2 j); intros RANGE.
+    assert (Int.unsigned j <> 0).
+    { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
+    exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD.
+    unfold Int.modu. rewrite Int.unsigned_repr. omega. omega.
+  }
+  intros until y.
+  intros HX HY.
+  inv HX; inv HY; cbn in *.
+  { destruct Int.eq eqn:E; unfold ntop; cbn; auto with va.
+  }
+  all: try discriminate.
+  all: unfold ntop2; auto with va.
+  all: try (destruct Int.eq eqn:E; cbn; unfold ntop2; auto with va; fail).
+  all: try apply vmatch_uns_undef.
+  
+  all:
+    generalize (Int.eq_spec i0 Int.zero);
+    destruct (Int.eq i0 Int.zero);
+    cbn;
+    intro.
+  all: try apply vmatch_uns_undef.
+  all: apply vmatch_uns; auto.
+Qed.
+
+
+Lemma shrx_total_sound:
+  forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.shrx v w)) (shrx x y).
+Proof.
+  intros until y. intros HX HY.
+  inv HX; inv HY; cbn.
+  all: unfold ntop1; auto with va.
+  all: destruct Int.ltu eqn:LTU; cbn; unfold ntop; auto with va.
+Qed.
+
+
+Definition divls_total (v w: aval) :=
+  match w, v with
+  | L i2, L i1 =>
+      if Int64.eq i2 Int64.zero
+      || Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone
+      then ntop
+      else L (Int64.divs i1 i2)
+  | _, _ => ntop2 v w
+  end.
+
+Lemma divls_total_sound:
+  forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divls v w)) (divls_total x y).
+Proof.
+  intros until y.
+  intros HX HY.
+  inv HX; inv HY; cbn in *.
+  all: unfold ntop2; auto with va.
+  all: destruct (_ || _) eqn:E; unfold ntop2, ntop; cbn; auto with va.
+Qed.
+
+Definition divlu_total (v w: aval) :=
+  match w, v with
+  | L i2, L i1 =>
+      if Int64.eq i2 Int64.zero
+       then ntop
+      else L (Int64.divu i1 i2)
+  | _, _ => ntop2 v w
+  end.
+
+Lemma divlu_total_sound:
+  forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.divlu v w)) (divlu_total x y).
+Proof.
+  intros until y.
+  intros HX HY.
+  inv HX; inv HY; cbn in *.
+  all: unfold ntop2; auto with va.
+  all: destruct Int64.eq eqn:E; unfold ntop2, ntop; cbn; auto with va.
+Qed.
+
+
+Definition modls_total (v w: aval) :=
+  match w, v with
+  | L i2, L i1 =>
+      if Int64.eq i2 Int64.zero
+      || Int64.eq i1 (Int64.repr Int64.min_signed) && Int64.eq i2 Int64.mone
+      then ntop
+      else L (Int64.mods i1 i2)
+  | _, _ => ntop2 v w
+  end.
+
+Lemma modls_total_sound:
+  forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.modls v w)) (modls_total x y).
+Proof.
+  intros until y.
+  intros HX HY.
+  inv HX; inv HY; cbn in *.
+  all: unfold ntop2; auto with va.
+  all: destruct (_ || _) eqn:E; unfold ntop2, ntop; cbn; auto with va.
+Qed.
+
+
+Definition modlu_total (v w: aval) :=
+  match w, v with
+  | L i2, L i1 =>
+      if Int64.eq i2 Int64.zero
+      then ntop
+      else L (Int64.modu i1 i2)
+  | _, _ => ntop2 v w
+  end.
+
+Lemma modlu_total_sound:
+  forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.modlu v w)) (modlu_total x y).
+Proof.
+  intros until y.
+  intros HX HY.
+  inv HX; inv HY; cbn in *.
+  all: unfold ntop2; auto with va.
+  all: destruct Int64.eq eqn:E; cbn; unfold ntop2, ntop; auto with va.
+Qed.
+
+Lemma shrxl_total_sound:
+  forall bc v w x y, vmatch bc v x -> vmatch bc w y -> vmatch bc (Val.maketotal (Val.shrxl v w)) (shrxl x y).
+Proof.
+  intros until y. intros HX HY.
+  inv HX; inv HY; cbn.
+  all: unfold ntop1; auto with va.
+  all: destruct Int.ltu eqn:LTU; cbn; unfold ntop; auto with va.
+Qed.
+
+Hint Resolve divu_total_sound divs_total_sound modu_total_sound mods_total_sound shrx_total_sound divlu_total_sound divls_total_sound modlu_total_sound modls_total_sound shrxl_total_sound : va.
 
 (** Value analysis for RISC V operators *)
 
@@ -59,10 +353,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 +382,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