diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-25 07:18:39 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-25 07:18:39 +0100 |
| commit | f9b5ef305997c22b505865f2a2334b56115426b6 (patch) | |
| tree | cc5889db8af36d44f7015d21de1fbfaae5bcf55a /mppa_k1c/Op.v | |
| parent | 61e7b02ec6b25f4cf5ef7053b92c6eab3bcf616b (diff) | |
| download | compcert-kvx-f9b5ef305997c22b505865f2a2334b56115426b6.tar.gz compcert-kvx-f9b5ef305997c22b505865f2a2334b56115426b6.zip | |
going forward with select/selectl
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 38 |
1 files changed, 26 insertions, 12 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index edb42d2f..8332621b 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -253,12 +253,12 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool end. Definition select (v0 : val) (v1 : val) (vselect : val) : option val := - match v0 with - | Vint i0 => - match v1 with - | Vint i1 => - match vselect with - | Vint iselect => + match vselect with + | Vint iselect => + match v0 with + | Vint i0 => + match v1 with + | Vint i1 => Some (Vint (if Int.cmp Ceq Int.zero iselect then i0 else i1)) @@ -270,12 +270,12 @@ Definition select (v0 : val) (v1 : val) (vselect : val) : option val := end. Definition selectl (v0 : val) (v1 : val) (vselect : val) : option val := - match v0 with - | Vlong i0 => - match v1 with - | Vlong i1 => - match vselect with - | Vint iselect => + match vselect with + | Vint iselect => + match v0 with + | Vlong i0 => + match v1 with + | Vlong i1 => Some (Vlong (if Int.cmp Ceq Int.zero iselect then i0 else i1)) @@ -1371,6 +1371,20 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. + (* select *) + - inv H5; simpl in H1; try discriminate. + inv H4; simpl in H1; try discriminate. + inv H3; simpl in H1; try discriminate. + simpl. + injection H1; clear H1; intro H1. + destruct (Int.eq _ _); rewrite <- H1; simpl; TrivialExists. + (* selectl *) + - inv H5; simpl in H1; try discriminate. + inv H4; simpl in H1; try discriminate. + inv H3; simpl in H1; try discriminate. + simpl. + injection H1; clear H1; intro H1. + destruct (Int.eq _ _); rewrite <- H1; simpl; TrivialExists. Qed. Lemma eval_addressing_inj: |