add: non trapping ops

1 files changed, 31 insertions, 0 deletions

diff --git a/x86/Op.v b/x86/Op.v
index a7176ce4..15672bbe 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -742,6 +742,37 @@ 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 | Odivl | Odivu | Odivlu
+  | Omod | Omodl | Omodu | Omodlu
+  | Oshrximm _ | Oshrxlimm _
+  | Ointoffloat
+  | Ointofsingle
+  | Olongoffloat
+  | Olongofsingle 
+  | Osingleofint
+  | Osingleoflong
+  | Ofloatofint
+  | Ofloatoflong
+  | Olea _ | Oleal _ (* TODO this is suboptimal *) => 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 *)