From a8e2039a772da0fcfd484b7445de8cc093be5d2b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 23 Sep 2019 14:17:12 +0200
Subject: is_trapping_op_sound

---
 mppa_k1c/Op.v | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 7aea2929..92061d04 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -1030,6 +1030,34 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
     + constructor.
 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
+  | 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