From 3f98eba95b1d0bcb64a07f3188e3623954dc7db3 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 24 Sep 2019 21:05:42 +0200
Subject: trapping ops on rv

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

(limited to 'riscV/Op.v')

diff --git a/riscV/Op.v b/riscV/Op.v
index 97bc301a..a71696c7 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -666,6 +666,36 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct (eval_condition cond vl m)... destruct b...
 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
+  | Olongofsingle | Olonguofsingle
+  | Osingleofint | Osingleofintu
+  | Osingleoflong | Osingleoflongu
+  | Ofloatofint | Ofloatofintu
+  | Ofloatoflong | Ofloatoflongu => true
+  | _ => false
+  end.
+
+Lemma is_trapping_op_sound:
+  forall op vl sp m,
+    op <> Omove ->
+    is_trapping_op op = false ->
+    (List.length vl) = (List.length (fst (type_of_operation op))) ->
+    eval_operation genv sp op vl m <> None.
+Proof.
+  destruct op; intros; simpl in *; try congruence.
+  all: try (destruct vl as [ | vh1 vl1]; try discriminate).
+  all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
+  all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
+  all: try (destruct vl3 as [ | vh4 vl4]; try discriminate).
+Qed.
 End SOUNDNESS.
 
 (** * Manipulating and transforming operations *)
-- 
cgit