diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 12:58:39 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 12:58:39 +0100 |
| commit | 8b03b197c24e32974be1ca254039bc728d48d615 (patch) | |
| tree | 226bf0e361b44a2632d60f7ea944f4613ae94a13 /kvx/Op.v | |
| parent | 73a83b969dbb6f4c419ebdcc663f463509b6d6e3 (diff) | |
| download | compcert-kvx-8b03b197c24e32974be1ca254039bc728d48d615.tar.gz compcert-kvx-8b03b197c24e32974be1ca254039bc728d48d615.zip | |
cond_depends_on_memory for KVX
Diffstat (limited to 'kvx/Op.v')
| -rw-r--r-- | kvx/Op.v | 21 |
1 files changed, 17 insertions, 4 deletions
@@ -1205,12 +1205,25 @@ Definition is_trivial_op (op: operation) : bool := (** Operations that depend on the memory state. *) +Definition cond_depends_on_memory (c: condition) : bool := + match c with + | Ccompu _ | Ccompuimm _ _ => negb Archi.ptr64 + | Ccomplu _ | Ccompluimm _ _ => Archi.ptr64 + | _ => false + end. + +Lemma cond_depends_on_memory_correct: + forall c args m1 m2, + cond_depends_on_memory c = false -> + eval_condition c args m1 = eval_condition c args m2. +Proof. + intros; destruct c; cbn; discriminate || reflexivity. +Qed. + 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 (Ccompu _ | Ccompuimm _ _) => negb Archi.ptr64 + | Ocmp (Ccomplu _ | Ccompluimm _ _) => Archi.ptr64 | Osel (Ccompu0 _) _ | Oselimm (Ccompu0 _) _ | Osellimm (Ccompu0 _) _ => negb Archi.ptr64 | Osel (Ccomplu0 _) _ | Oselimm (Ccomplu0 _) _ | Osellimm (Ccomplu0 _) _ => Archi.ptr64 |