diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-25 14:38:30 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-25 14:38:30 +0100 |
| commit | c55522c71d7ed2542bfd50d466dbeb520bde21f4 (patch) | |
| tree | 755c47c96a3dccc601bd085855ff54519fc83f0a /aarch64/Op.v | |
| parent | b8647d11c1af9bfe19fd8be33f8e88f92de77888 (diff) | |
| download | compcert-kvx-c55522c71d7ed2542bfd50d466dbeb520bde21f4.tar.gz compcert-kvx-c55522c71d7ed2542bfd50d466dbeb520bde21f4.zip | |
cond_valid_pointer_eq
Diffstat (limited to 'aarch64/Op.v')
| -rw-r--r-- | aarch64/Op.v | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/aarch64/Op.v b/aarch64/Op.v index f720e545..8d8f654d 100644 --- a/aarch64/Op.v +++ b/aarch64/Op.v @@ -1209,18 +1209,26 @@ Proof. rewrite (cond_depends_on_memory_correct cond args m1 m2 H). auto. Qed. +Lemma cond_valid_pointer_eq: + forall cond args m1 m2, + (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> + eval_condition cond args m1 = eval_condition cond args m2. +Proof. + intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence. + all: repeat (destruct args; simpl; try congruence); + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. +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 eqn:OP; simpl; try congruence. - - intros MEM; destruct cond; simpl; try congruence; + intros until m2. intro MEM. destruct op eqn:OP; simpl; try congruence. + - f_equal; f_equal; auto using cond_valid_pointer_eq. + - destruct cond; simpl; try congruence; repeat (destruct args; simpl; try congruence); erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. - - intro MEM; destruct cond; simpl; try congruence; - 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 *) |