op_depends_on_memory_correct

1 files changed, 24 insertions, 6 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index 9e98d517..d819ee32 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -853,23 +853,41 @@ Definition is_trivial_op (op: operation) : bool :=
 
 (** Operations that depend on the memory state. *)
 
+Definition cond_depends_on_memory (cond : condition) : bool :=
+  match cond with
+  | Ccompu _ => negb Archi.ptr64
+  | Ccompuimm _ _ => negb Archi.ptr64
+  | Ccomplu _ => Archi.ptr64
+  | Ccompluimm _ _ => Archi.ptr64
+  | _ => false
+  end.
+
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp (Ccompu _) => negb Archi.ptr64
-  | Ocmp (Ccompuimm _ _) => negb Archi.ptr64
-  | Ocmp (Ccomplu _) => Archi.ptr64
-  | Ocmp (Ccompluimm _ _) => Archi.ptr64
+  | Ocmp cmp => cond_depends_on_memory cmp
   | _ => false
   end.
 
+Lemma cond_depends_on_memory_correct:
+  forall cond args m1 m2,
+  cond_depends_on_memory cond = false ->
+  eval_condition cond args m1 = eval_condition cond args m2.
+Proof.
+  intros until m2.
+  destruct cond; cbn; try congruence.
+  all: unfold Val.cmpu_bool, Val.cmplu_bool.
+  all: destruct Archi.ptr64; cbn; intro SF; try discriminate.
+  all: reflexivity.
+Qed.
+
 Lemma op_depends_on_memory_correct:
   forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
   op_depends_on_memory op = false ->
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence.
-  destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF;
-  unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
+  intro DEPEND.
+  f_equal. f_equal. apply cond_depends_on_memory_correct; trivial.
 Qed.
 
 Lemma cond_valid_pointer_eq: