From 62063b60892dea2e52b32c426bdd481816f24b7f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 18 Sep 2020 18:27:33 +0200
Subject: bogus OpWeights for Risc-V

---
 riscV/OpWeights.ml | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 riscV/OpWeights.ml

(limited to 'riscV')

diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml
new file mode 100644
index 00000000..3662ef1c
--- /dev/null
+++ b/riscV/OpWeights.ml
@@ -0,0 +1,19 @@
+open Op;;
+let resource_bounds = [| 1 |];;
+
+
+let latency_of_op (op : operation) (nargs : int) = 1;;
+
+let resources_of_op (op : operation) (nargs : int) = [| 1 |];;
+
+let resources_of_cond (cond : condition) (nargs : int) = [| 1 |];;
+
+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 |];;
+
+let resources_of_store chunk addressing nargs = [| 1 |];;
+
+let resources_of_call _ _ = resource_bounds;;
+let resources_of_builtin _ = resource_bounds;;
-- 
cgit 


From d87dc1bde1d962fd1192f9176396c4bc7d151041 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 18 Sep 2020 18:38:26 +0200
Subject: EH1 scheduling

---
 riscV/OpWeights.ml | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

(limited to 'riscV')

diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml
index 3662ef1c..02187067 100644
--- a/riscV/OpWeights.ml
+++ b/riscV/OpWeights.ml
@@ -1,19 +1,32 @@
 open Op;;
-let resource_bounds = [| 1 |];;
 
+(* Attempt at modeling SweRV EH1
+[| issues ; LSU ; multiplier ; divider |] *)
+let resource_bounds = [| 2 ; 1; 1; 2 |];;
 
-let latency_of_op (op : operation) (nargs : int) = 1;;
 
-let resources_of_op (op : operation) (nargs : int) = [| 1 |];;
+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; 0 |]
+    | Odiv | Odivu | Odivl | Odivlu -> [| 0 ; 0; 0; 1 |]                        
+    | _ -> [| 1; 0; 0; 0 |];;
 
 let resources_of_cond (cond : condition) (nargs : int) = [| 1 |];;
 
 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 |];;
+let resources_of_load trap chunk addressing nargs = [| 1; 1; 0; 0 |];;
 
-let resources_of_store chunk addressing nargs = [| 1 |];;
+let resources_of_store chunk addressing nargs = [| 1; 1; 0; 0 |];;
 
 let resources_of_call _ _ = resource_bounds;;
 let resources_of_builtin _ = resource_bounds;;
-- 
cgit 


From 1f42a62b6f7694206f805b3317e76341f2da066b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 18 Sep 2020 21:01:04 +0200
Subject: wrong resources

---
 riscV/OpWeights.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'riscV')

diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml
index 02187067..88ef5216 100644
--- a/riscV/OpWeights.ml
+++ b/riscV/OpWeights.ml
@@ -19,7 +19,7 @@ let resources_of_op (op : operation) (nargs : int) =
     | Odiv | Odivu | Odivl | Odivlu -> [| 0 ; 0; 0; 1 |]                        
     | _ -> [| 1; 0; 0; 0 |];;
 
-let resources_of_cond (cond : condition) (nargs : int) = [| 1 |];;
+let resources_of_cond (cond : condition) (nargs : int) = [| 1; 0; 0; 0 |];;
 
 let latency_of_load trap chunk (addr : addressing) (nargs : int) = 3;;
 let latency_of_call _ _ = 6;;
-- 
cgit 


From cae21e8816db863bf99f87469c9680e150d28960 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 21 Sep 2020 09:17:05 +0200
Subject: maketotal mod & div

---
 riscV/Asmgenproof1.v     |  45 ++++++-
 riscV/ConstpropOpproof.v | 152 +++++++++++++++++------
 riscV/Op.v               | 143 +++++++++++++---------
 riscV/SelectLongproof.v  |  46 +++----
 riscV/SelectOpproof.v    |  62 +++++-----
 riscV/ValueAOp.v         | 310 +++++++++++++++++++++++++++++++++++++++++++++--
 6 files changed, 593 insertions(+), 165 deletions(-)

(limited to 'riscV')

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
-- 
cgit 


From 9c2c662a2a70545858d95b2f9f0a3625c506bc24 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 21 Sep 2020 21:37:16 +0200
Subject: moved Risc-V div ValueAOp to central location

---
 riscV/ValueAOp.v | 293 -------------------------------------------------------
 1 file changed, 293 deletions(-)

(limited to 'riscV')

diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 5d1797ae..14b53db9 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -15,299 +15,6 @@ 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 *)
 
 Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
-- 
cgit 


From cdb48111d4baff50d8708b979f8b31ef21505247 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 21 Sep 2020 22:48:45 +0200
Subject: risc-V now without trapping instructions

---
 riscV/Op.v              | 132 ++++++++++++++++++++++++------------------------
 riscV/SelectLongproof.v |   8 +++
 riscV/SelectOpproof.v   |   8 +++
 riscV/ValueAOp.v        |  16 +++---
 4 files changed, 90 insertions(+), 74 deletions(-)

(limited to 'riscV')

diff --git a/riscV/Op.v b/riscV/Op.v
index e953bd71..25214ddc 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -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.
@@ -647,47 +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
-  | 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
@@ -1172,37 +1172,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/SelectLongproof.v b/riscV/SelectLongproof.v
index f5e8edf8..0fc578bf 100644
--- a/riscV/SelectLongproof.v
+++ b/riscV/SelectLongproof.v
@@ -558,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.
@@ -565,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.
@@ -572,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.
@@ -579,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.
@@ -586,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.
@@ -593,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.
@@ -600,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.
@@ -607,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 436cd4f3..1d13702a 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -788,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:
@@ -797,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:
@@ -808,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:
@@ -819,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:
@@ -828,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:
@@ -837,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:
@@ -846,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:
@@ -855,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 14b53db9..f4b7b4d6 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -120,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)
-- 
cgit 


From 825b77fe8b4eb0919564e51cfaae69a6dfae24e3 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 2 Oct 2020 21:54:34 +0200
Subject: so that all architectures compile

---
 riscV/OpWeights.ml               | 23 +++++++++++++++--------
 riscV/PrepassSchedulingOracle.ml |  1 +
 2 files changed, 16 insertions(+), 8 deletions(-)
 create mode 120000 riscV/PrepassSchedulingOracle.ml

(limited to 'riscV')

diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml
index 88ef5216..143435c1 100644
--- a/riscV/OpWeights.ml
+++ b/riscV/OpWeights.ml
@@ -1,9 +1,9 @@
 open Op;;
 
 (* Attempt at modeling SweRV EH1
-[| issues ; LSU ; multiplier ; divider |] *)
-let resource_bounds = [| 2 ; 1; 1; 2 |];;
-
+[| 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
@@ -15,18 +15,25 @@ let latency_of_op (op : operation) (nargs : int) =
 let resources_of_op (op : operation) (nargs : int) = 
   match op with
     | Omul  | Omulhs  | Omulhu
-    | Omull | Omullhs | Omullhu -> [| 1 ; 0 ; 1; 0 |]
-    | Odiv | Odivu | Odivl | Odivlu -> [| 0 ; 0; 0; 1 |]                        
+    | 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; 0 |];;
+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; 0 |];;
+let resources_of_load trap chunk addressing nargs = [| 1; 1; 0 |];;
 
-let resources_of_store chunk addressing nargs = [| 1; 1; 0; 0 |];;
+let resources_of_store chunk addressing nargs = [| 1; 1; 0 |];;
 
 let resources_of_call _ _ = resource_bounds;;
 let resources_of_builtin _ = resource_bounds;;
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
-- 
cgit 


From 41a97a2d5eace2a0b113d7da590df69f1cc0d763 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Sat, 17 Oct 2020 17:03:07 +0200
Subject: proves op_valid_pointer_eq lemma for RISC-V (necessary for the
 pre-pass scheduler)

---
 riscV/Op.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'riscV')

diff --git a/riscV/Op.v b/riscV/Op.v
index 25214ddc..62999a2f 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -877,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 :=
-- 
cgit 


From d3c9c0f5659d9c97f09f4aaa4d0e9bede9ce3e2b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 22 Oct 2020 09:55:47 +0200
Subject: attempt at modeling Rocket

---
 riscV/OpWeights.ml | 83 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 83 insertions(+)

(limited to 'riscV')

diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml
index 143435c1..637f2904 100644
--- a/riscV/OpWeights.ml
+++ b/riscV/OpWeights.ml
@@ -1,5 +1,87 @@
 open Op;;
 
+(* 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;;
+
+(*
 (* Attempt at modeling SweRV EH1
 [| issues ; LSU ; multiplier |] *)
 let resource_bounds = [| 2 ; 1; 1 |];;
@@ -37,3 +119,4 @@ let resources_of_store chunk addressing nargs = [| 1; 1; 0 |];;
 
 let resources_of_call _ _ = resource_bounds;;
 let resources_of_builtin _ = resource_bounds;;
+ *)
-- 
cgit 


From a8f9909dda3a6f1f997721b753057030575c3c4e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 22 Oct 2020 13:26:00 +0200
Subject: allow changing the target core

---
 riscV/OpWeights.ml                   | 279 ++++++++++++++++++++---------------
 riscV/PrepassSchedulingOracleDeps.ml |   1 +
 2 files changed, 160 insertions(+), 120 deletions(-)
 create mode 120000 riscV/PrepassSchedulingOracleDeps.ml

(limited to 'riscV')

diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml
index 637f2904..75a913c6 100644
--- a/riscV/OpWeights.ml
+++ b/riscV/OpWeights.ml
@@ -1,122 +1,161 @@
 open Op;;
-
-(* 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;;
-
-(*
-(* 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 |];;
+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) = [| 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;;
- *)
+    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/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
-- 
cgit