diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-23 14:17:12 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-23 14:17:12 +0200 |
| commit | a8e2039a772da0fcfd484b7445de8cc093be5d2b (patch) | |
| tree | 90f890796d291d4e466258785e6948102d4dca5c /mppa_k1c | |
| parent | 5d455f088929be06ce1c61d02e541d44dfefc42f (diff) | |
| download | compcert-kvx-a8e2039a772da0fcfd484b7445de8cc093be5d2b.tar.gz compcert-kvx-a8e2039a772da0fcfd484b7445de8cc093be5d2b.zip | |
is_trapping_op_sound
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Op.v | 28 |
1 files changed, 28 insertions, 0 deletions
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 *) |