add: non trapping ops

1 files changed, 26 insertions, 0 deletions

diff --git a/arm/Op.v b/arm/Op.v
index 9de365e9..671bdbe4 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -518,6 +518,32 @@ Proof with (try exact I; try reflexivity).
   unfold Val.select. destruct (eval_condition c vl m). apply Val.normalize_type. exact I.
 Qed.
 
+
+Definition is_trapping_op (op : operation) :=
+  match op with
+  | Odiv | Odivu
+  | Oshrximm _
+  | Ointoffloat | Ointuoffloat
+  | Ointofsingle | Ointuofsingle
+  | Ofloatofint | Ofloatofintu
+  | Osingleofint | Osingleofintu => 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 *)