risc-V now without trapping instructions

5 files changed, 114 insertions, 74 deletions

diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 81a52bab..f1a46baa 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -2711,6 +2711,28 @@ Proof.
   all: try constructor.
 Qed.
 
+Lemma floatofint_total_sound:
+  forall v x, vmatch v x ->
+              vmatch (Val.maketotal (Val.floatofint v)) (floatofint x).
+Proof.
+  unfold Val.floatofint, floatofint; intros.
+  inv H; simpl.
+  all: auto with va.
+  all: unfold ntop1, provenance.
+  all: try constructor.
+Qed.
+
+Lemma floatofintu_total_sound:
+  forall v x, vmatch v x ->
+              vmatch (Val.maketotal (Val.floatofintu v)) (floatofintu x).
+Proof.
+  unfold Val.floatofintu, floatofintu; intros.
+  inv H; simpl.
+  all: auto with va.
+  all: unfold ntop1, provenance.
+  all: try constructor.
+Qed.
+
 
 Definition divs_total (v w: aval) := 
   match w, v with
@@ -5187,6 +5209,8 @@ Hint Resolve cnot_sound symbol_address_sound
        singleoflongu_total_sound
        floatoflong_total_sound
        floatoflongu_total_sound
+       floatofint_total_sound
+       floatofintu_total_sound
        divu_total_sound divs_total_sound
        modu_total_sound mods_total_sound shrx_total_sound
        divlu_total_sound divls_total_sound
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)