proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass scheduler)

1 files changed, 10 insertions, 0 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index 25214ddc..62999a2f 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -877,6 +877,16 @@ Proof.
   unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
+Lemma op_valid_pointer_eq:
+  forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2,
+  (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
+  eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
+Proof.
+  intros until m2. destruct op; simpl; try congruence.
+  intros MEM; destruct cond; repeat (destruct args; simpl; try congruence);
+    erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+Qed.
+
 (** Global variables mentioned in an operation or addressing mode *)
 
 Definition globals_addressing (addr: addressing) : list ident :=