diff options
Diffstat (limited to 'aarch64/Peephole.v')
| -rw-r--r-- | aarch64/Peephole.v | 33 |
1 files changed, 0 insertions, 33 deletions
diff --git a/aarch64/Peephole.v b/aarch64/Peephole.v index 2282326a..167def44 100644 --- a/aarch64/Peephole.v +++ b/aarch64/Peephole.v @@ -17,39 +17,6 @@ Require Import Integers. Require Import AST. Require Compopts. -(*Fixpoint gpreg_q_search_rec r0 r1 l := - match l with - | h :: t => - let (s0, s1) := gpreg_q_expand h in - if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) - then Some h - else gpreg_q_search_rec r0 r1 t - | nil => None - end. - -Fixpoint gpreg_o_search_rec r0 r1 r2 r3 l := - match l with - | h :: t => - match gpreg_o_expand h with - | (((s0, s1), s2), s3) => - if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) && - (gpreg_eq r2 s2) && (gpreg_eq r3 s3) - then Some h - else gpreg_o_search_rec r0 r1 r2 r3 t - end - | nil => None - end. - -Definition gpreg_q_search (r0 : gpreg) (r1 : gpreg) : option gpreg_q := - gpreg_q_search_rec r0 r1 gpreg_q_list. - -Definition gpreg_o_search r0 r1 r2 r3 : option gpreg_o := - gpreg_o_search_rec r0 r1 r2 r3 gpreg_o_list. - -Parameter print_found_store: forall A, Z -> A -> A. - - Definition coalesce_octuples := true.*) - Definition is_valid_immofs_32 (z: Z) : bool := if (zle z 252) && (zle (-256) z) && ((Z.modulo z 4) =? 0) then true else false. |