diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 11:57:17 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 11:57:17 +0100 |
| commit | 19e9d0ca5d4ba59db9c1bc40842ac08b5ca4ac41 (patch) | |
| tree | 16c28f9cb84e99b7ef9e171092b041df6c7fcbe8 /mppa_k1c/SelectOpproof.v | |
| parent | cfc949a5fce43f2d4e094b52ea42d619f64692c1 (diff) | |
| download | compcert-kvx-19e9d0ca5d4ba59db9c1bc40842ac08b5ca4ac41.tar.gz compcert-kvx-19e9d0ca5d4ba59db9c1bc40842ac08b5ca4ac41.zip | |
andn/orn start being generated
Diffstat (limited to 'mppa_k1c/SelectOpproof.v')
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 26df4fc7..c81f6fb5 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -430,6 +430,7 @@ Proof. red; intros until y; unfold and; case (and_match a b); intros; InvEval. - rewrite Val.and_commut. apply eval_andimm; auto. - apply eval_andimm; auto. + - (*andn*) TrivialExists; simpl; congruence. - TrivialExists. Qed. @@ -493,6 +494,7 @@ Proof. destruct (same_expr_pure t1 t2) eqn:?; auto. InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. exists (Val.ror v1 (Vint n2)); split. EvalOp. rewrite Val.or_commut. apply ROR; auto. + - (*orn*) TrivialExists; simpl; congruence. - apply DEFAULT. Qed. @@ -526,14 +528,14 @@ Theorem eval_notint: unary_constructor_sound notint Val.notint. Proof. assert (forall v, Val.lessdef (Val.notint (Val.notint v)) v). destruct v; simpl; auto. rewrite Int.not_involutive; auto. - unfold notint; red; intros until x; case (notint_match a); intros; InvEval. - - TrivialExists; simpl; congruence. - - TrivialExists; simpl; congruence. - - TrivialExists; simpl; congruence. - - TrivialExists; simpl; congruence. - - TrivialExists; simpl; congruence. - - TrivialExists; simpl; congruence. - - TrivialExists. + unfold notint; red; intros until x; case (notint_match a); intros; InvEval. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists. Qed. Theorem eval_divs_base: |