aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/SelectOp.vp2
-rw-r--r--arm/SelectOpproof.v15
-rw-r--r--backend/Selection.v5
-rw-r--r--backend/Selectionproof.v20
-rw-r--r--ia32/SelectOp.vp7
-rw-r--r--ia32/SelectOpproof.v23
-rw-r--r--powerpc/SelectOp.vp7
-rw-r--r--powerpc/SelectOpproof.v23
8 files changed, 90 insertions, 12 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 7b8851c9..27b5f536 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -454,4 +454,4 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
| _ => (Aindexed Int.zero, e:::Enil)
end.
-
+Definition cond_of_expr (e: expr) := (Ccompuimm Cne Int.zero, e:::Enil).
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 0a5ee645..1a2f5606 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -769,4 +769,19 @@ Proof.
exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Int.add_zero; auto.
Qed.
+Theorem eval_cond_of_expr:
+ forall le a v b,
+ eval_expr ge sp e m le a v ->
+ Val.bool_of_val v b ->
+ match cond_of_expr a with (cond, args) =>
+ exists vl,
+ eval_exprlist ge sp e m le args vl /\
+ eval_condition cond vl m = Some b
+ end.
+Proof.
+ intros. unfold cond_of_expr; simpl.
+ exists (v :: nil); split; auto with evalexpr.
+ simpl. inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto.
+Qed.
+
End CMCONSTR.
diff --git a/backend/Selection.v b/backend/Selection.v
index 2d6c9017..ef627d79 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -62,6 +62,9 @@ Definition is_compare_eq_zero (c: condition) : bool :=
| _ => false
end.
+Definition condexpr_of_expr_base (e: expr) : condexpr :=
+ let (c, args) := cond_of_expr e in CEcond c args.
+
Fixpoint condexpr_of_expr (e: expr) : condexpr :=
match e with
| Eop (Ointconst n) Enil =>
@@ -78,7 +81,7 @@ Fixpoint condexpr_of_expr (e: expr) : condexpr :=
| Econdition ce e1 e2 =>
CEcondition ce (condexpr_of_expr e1) (condexpr_of_expr e2)
| _ =>
- CEcond (Ccompuimm Cne Int.zero) (e:::Enil)
+ condexpr_of_expr_base e
end.
(** Conversion of loads and stores *)
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 9681c66b..b5bc216b 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -81,17 +81,17 @@ Proof.
intros. simpl. auto.
Qed.
-Lemma eval_base_condition_of_expr:
+Lemma eval_condition_of_expr_base:
forall le a v b,
eval_expr ge sp e m le a v ->
Val.bool_of_val v b ->
- eval_condexpr ge sp e m le
- (CEcond (Ccompuimm Cne Int.zero) (a ::: Enil))
- b.
+ eval_condexpr ge sp e m le (condexpr_of_expr_base a) b.
Proof.
- intros.
- eapply eval_CEcond. eauto with evalexpr.
- inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto.
+ intros. unfold condexpr_of_expr_base.
+ exploit eval_cond_of_expr; eauto.
+ destruct (cond_of_expr a) as [cond args].
+ intros [vl [A B]].
+ econstructor; eauto.
Qed.
Lemma is_compare_neq_zero_correct:
@@ -135,15 +135,15 @@ Lemma eval_condition_of_expr:
Proof.
intro a0; pattern a0.
apply expr_induction_principle; simpl; intros;
- try (eapply eval_base_condition_of_expr; eauto; fail).
+ try (eapply eval_condition_of_expr_base; eauto; fail).
- destruct o; try (eapply eval_base_condition_of_expr; eauto; fail).
+ destruct o; try (eapply eval_condition_of_expr_base; eauto; fail).
destruct e0. inv H0. inv H5. simpl in H7. inv H7.
inversion H1.
rewrite Int.eq_false; auto. constructor.
subst i; rewrite Int.eq_true. constructor.
- eapply eval_base_condition_of_expr; eauto.
+ eapply eval_condition_of_expr_base; eauto.
inv H0. simpl in H7.
assert (eval_condition c vl m = Some b).
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 98db3885..62de4ce1 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -429,3 +429,10 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
| _ => (Aindexed Int.zero, e:::Enil)
end.
+(** ** Turning an expression into a condition *)
+
+Nondetfunction cond_of_expr (e: expr) :=
+ match e with
+ | Eop (Oandimm n) (t1:::Enil) => (Cmasknotzero n, t1:::Enil)
+ | _ => (Ccompuimm Cne Int.zero, e:::Enil)
+ end.
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index e6fd8098..658a7550 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -753,4 +753,27 @@ Proof.
exists (v :: nil); split. constructor; auto. constructor. subst; simpl. rewrite Int.add_zero; auto.
Qed.
+Theorem eval_cond_of_expr:
+ forall le a v b,
+ eval_expr ge sp e m le a v ->
+ Val.bool_of_val v b ->
+ match cond_of_expr a with (cond, args) =>
+ exists vl,
+ eval_exprlist ge sp e m le args vl /\
+ eval_condition cond vl m = Some b
+ end.
+Proof.
+ intros until v. unfold cond_of_expr; case (cond_of_expr_match a); intros; InvEval.
+ subst v. exists (v1 :: nil); split; auto with evalexpr.
+ simpl. destruct b.
+ generalize (Val.bool_of_true_val2 _ H0); clear H0; intro ISTRUE.
+ destruct v1; simpl in ISTRUE; try contradiction.
+ rewrite Int.eq_false; auto.
+ generalize (Val.bool_of_false_val2 _ H0); clear H0; intro ISFALSE.
+ destruct v1; simpl in ISFALSE; try contradiction.
+ rewrite ISFALSE. rewrite Int.eq_true; auto.
+ exists (v :: nil); split; auto with evalexpr.
+ simpl. inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto.
+Qed.
+
End CMCONSTR.
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 290704bc..943c4006 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -460,3 +460,10 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
| _ => (Aindexed Int.zero, e:::Enil)
end.
+(** ** Turning an expression into a condition *)
+
+Nondetfunction cond_of_expr (e: expr) :=
+ match e with
+ | Eop (Oandimm n) (t1:::Enil) => (Cmasknotzero n, t1:::Enil)
+ | _ => (Ccompuimm Cne Int.zero, e:::Enil)
+ end.
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 39205dbd..1d35d9f8 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -817,5 +817,28 @@ Proof.
rewrite Int.add_zero. auto.
Qed.
+Theorem eval_cond_of_expr:
+ forall le a v b,
+ eval_expr ge sp e m le a v ->
+ Val.bool_of_val v b ->
+ match cond_of_expr a with (cond, args) =>
+ exists vl,
+ eval_exprlist ge sp e m le args vl /\
+ eval_condition cond vl m = Some b
+ end.
+Proof.
+ intros until v. unfold cond_of_expr; case (cond_of_expr_match a); intros; InvEval.
+ subst v. exists (v1 :: nil); split; auto with evalexpr.
+ simpl. destruct b.
+ generalize (Val.bool_of_true_val2 _ H0); clear H0; intro ISTRUE.
+ destruct v1; simpl in ISTRUE; try contradiction.
+ rewrite Int.eq_false; auto.
+ generalize (Val.bool_of_false_val2 _ H0); clear H0; intro ISFALSE.
+ destruct v1; simpl in ISFALSE; try contradiction.
+ rewrite ISFALSE. rewrite Int.eq_true; auto.
+ exists (v :: nil); split; auto with evalexpr.
+ simpl. inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto.
+Qed.
+
End CMCONSTR.
generated by cgit (git 2.34.1) at 2024-06-02 18:39:17 +0000