trapping ops

1 files changed, 30 insertions, 0 deletions

diff --git a/aarch64/Op.v b/aarch64/Op.v
index bf33ab0d..c0b9d435 100644
--- a/aarch64/Op.v
+++ b/aarch64/Op.v
@@ -921,6 +921,36 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - unfold Val.select. destruct (eval_condition cond vl m). apply Val.normalize_type. exact I.
 Qed.
 
+
+Definition is_trapping_op (op : operation) :=
+  match op with
+  | Odiv | Odivu | Odivl | Odivlu
+  | Oshrximm _  | Oshrlximm _
+  | Ointoffloat | Ointuoffloat
+  | Ointofsingle | Ointuofsingle
+  | Ofloatofint | Ofloatofintu
+  | Osingleofint | Osingleofintu
+  | Olongoffloat | Olonguoffloat
+  | Olongofsingle | Olonguofsingle
+  | Ofloatoflong | Ofloatoflongu
+  | Osingleoflong | Osingleoflongu => 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 *)