aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-04-04 12:34:11 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-04-04 12:34:11 +0200
commitb7ded97f34c5f0c670f43f2b15e77eb8874a764e (patch)
treedf8cda7c77a4ee98ba9178be184a9e82ca5bbe84
parent3b70f4b0eb0d8efde0946ed883072e0f94d5766d (diff)
downloadcompcert-kvx-b7ded97f34c5f0c670f43f2b15e77eb8874a764e.tar.gz
compcert-kvx-b7ded97f34c5f0c670f43f2b15e77eb8874a764e.zip
progressing on select
-rw-r--r--mppa_k1c/Machregs.v2
-rw-r--r--mppa_k1c/Op.v26
2 files changed, 11 insertions, 17 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index f89f952f..daf724ea 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -209,7 +209,7 @@ Global Opaque
Definition two_address_op (op: operation) : bool :=
match op with
- | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect | Oselectl | Oselectf | Oselectfs => true
+ | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl | Oselectf | Oselectfs => true
| _ => false
end.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 96df5e1f..c3ea4baf 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -1471,22 +1471,16 @@ Proof.
- unfold eval_select.
inv H4; trivial.
inv H2; trivial.
- inv H3; trivial.
- + destruct (eval_condition0 cond _ m1) eqn:Hcond; trivial.
- assert (Hcond' : ((eval_condition0 cond (Vint i1) m2) = Some b)).
- * eapply eval_condition0_inj.
- constructor.
- assumption.
- * rewrite Hcond'. constructor.
- + destruct (eval_condition0 cond _ m1) eqn:Hcond; trivial.
- assert (Hcond' : ((eval_condition0 cond (Vlong i1) m2) = Some b)).
-
- trivial.
- exploit eval_condition0_inj; eauto.
- exploit eval_condition0_inj; eauto.
- destruct v; trivial.
- destruct v0; trivial.
- destruct v'; trivial.
+ inv H3; trivial;
+ try (destruct cond; simpl; trivial; fail).
+ destruct (eval_condition0 cond (Vptr _ _) m1) eqn:Hcond; trivial.
+ eassert (Hcond' : ((eval_condition0 cond (Vptr b2 (Ptrofs.add ofs1 (Ptrofs.repr delta)))) m2) = Some b).
+ * eapply eval_condition0_inj.
+ eapply Val.inject_ptr.
+ eassumption.
+ reflexivity.
+ assumption.
+ * rewrite Hcond'. constructor.
(* selectl *)
- inv H3; simpl; try constructor.
inv H4; simpl; try constructor.