Instruction selection for operators
The instruction selection pass recognizes opportunities for using
combined arithmetic and logical operations and addressing modes
offered by the target processor. For instance, the expression x + 1
can take advantage of the "immediate add" instruction of the processor,
and on the PowerPC, the expression (x >> 6) & 0xFF can be turned
into a "rotate and mask" instruction.
This file defines functions for building CminorSel expressions and
statements, especially expressions consisting of operator
applications. These functions examine their arguments to choose
cheaper forms of operators whenever possible.
For instance, add e1 e2 will return a CminorSel expression semantically
equivalent to Eop Oadd (e1 ::: e2 ::: Enil), but will use a
Oaddimm operator if one of the arguments is an integer constant,
or suppress the addition altogether if one of the arguments is the
null integer. In passing, we perform operator reassociation
((e + c1) * c2 becomes (e * c2) + (c1 * c2)) and a small amount
of constant propagation.
On top of the "smart constructor" functions defined below,
module Selection implements the actual instruction selection pass.
Require Import Coqlib.
Require Import Compopts.
Require Import AST Integers Floats Builtins.
Require Import Op OpHelpers CminorSel.
Require Import DecBoolOps ExtValues.
Local Open Scope cminorsel_scope.
Constants *
Definition addrsymbol (
id:
qualident) (
ofs:
ptrofs) :=
Eop (
Oaddrsymbol id ofs)
Enil.
Definition addrstack (
ofs:
ptrofs) :=
Eop (
Oaddrstack ofs)
Enil.
Integer logical negation
Original definition:
Nondetfunction notint (e: expr) :=
match e with
| Eop (Ointconst n) Enil => Eop (Ointconst (Int.not n)) Enil
| Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil)
| Eop Onot (t1:::Enil) => t1
| Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil)
| Eop (Oxorimm n) (t1:::Enil) => Eop (Oxorimm (Int.not n)) (t1:::Enil)
| _ => Eop Onot (e:::Enil)
end.
:
forall (
e:
expr),
Type :=
|
notint_case1:
forall n,
notint_cases (
Eop (
Ointconst n)
Enil)
|
notint_case2:
forall s t1,
notint_cases (
Eop (
Oshift s) (
t1:::
Enil))
|
notint_case3:
forall t1,
notint_cases (
Eop Onot (
t1:::
Enil))
|
notint_case4:
forall s t1,
notint_cases (
Eop (
Onotshift s) (
t1:::
Enil))
|
notint_case5:
forall n t1,
notint_cases (
Eop (
Oxorimm n) (
t1:::
Enil))
|
notint_default:
forall (
e:
expr),
notint_cases e.
Definition notint_match (
e:
expr) :=
match e as zz1 return notint_cases zz1 with
|
Eop (
Ointconst n)
Enil =>
notint_case1 n
|
Eop (
Oshift s) (
t1:::
Enil) =>
notint_case2 s t1
|
Eop Onot (
t1:::
Enil) =>
notint_case3 t1
|
Eop (
Onotshift s) (
t1:::
Enil) =>
notint_case4 s t1
|
Eop (
Oxorimm n) (
t1:::
Enil) =>
notint_case5 n t1
|
e =>
notint_default e
end.
Definition notint (
e:
expr) :=
match notint_match e with
|
notint_case1 n =>
Eop (
Ointconst (
Int.not n))
Enil
|
notint_case2 s t1 =>
Eop (
Onotshift s) (
t1:::
Enil)
|
notint_case3 t1 =>
t1
|
notint_case4 s t1 =>
Eop (
Oshift s) (
t1:::
Enil)
|
notint_case5 n t1 =>
Eop (
Oxorimm (
Int.not n)) (
t1:::
Enil)
|
notint_default e =>
Eop Onot (
e:::
Enil)
end.
Integer addition and pointer addition
Original definition:
Nondetfunction addimm (n: int) (e: expr) :=
if Int.eq n Int.zero then e else
match e with
| Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil
| Eop (Oaddrsymbol s m) Enil =>
if Compopts.optim_globaladdroffset tt
then Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil
else Eop (Oaddimm n) (e ::: Enil)
| Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil
| Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil)
| _ => Eop (Oaddimm n) (e ::: Enil)
end.
:
forall (
e:
expr),
Type :=
|
addimm_case1:
forall m,
addimm_cases (
Eop (
Ointconst m)
Enil)
|
addimm_case2:
forall s m,
addimm_cases (
Eop (
Oaddrsymbol s m)
Enil)
|
addimm_case3:
forall m,
addimm_cases (
Eop (
Oaddrstack m)
Enil)
|
addimm_case4:
forall m t,
addimm_cases (
Eop (
Oaddimm m) (
t :::
Enil))
|
addimm_default:
forall (
e:
expr),
addimm_cases e.
Definition addimm_match (
e:
expr) :=
match e as zz1 return addimm_cases zz1 with
|
Eop (
Ointconst m)
Enil =>
addimm_case1 m
|
Eop (
Oaddrsymbol s m)
Enil =>
addimm_case2 s m
|
Eop (
Oaddrstack m)
Enil =>
addimm_case3 m
|
Eop (
Oaddimm m) (
t :::
Enil) =>
addimm_case4 m t
|
e =>
addimm_default e
end.
Definition addimm (
n:
int) (
e:
expr) :=
if Int.eq n Int.zero then e else match addimm_match e with
|
addimm_case1 m =>
Eop (
Ointconst(
Int.add n m))
Enil
|
addimm_case2 s m =>
if Compopts.optim_globaladdroffset tt then Eop (
Oaddrsymbol s (
Ptrofs.add (
Ptrofs.of_int n)
m))
Enil else Eop (
Oaddimm n) (
e :::
Enil)
|
addimm_case3 m =>
Eop (
Oaddrstack (
Ptrofs.add (
Ptrofs.of_int n)
m))
Enil
|
addimm_case4 m t =>
Eop (
Oaddimm(
Int.add n m)) (
t :::
Enil)
|
addimm_default e =>
Eop (
Oaddimm n) (
e :::
Enil)
end.
Helper for add that recognises (-r1) * r2 + r3 and emits
a single Omls (multiply-subtract) when Thumb-2 is supported.
Factored out because Nondetfunction cannot have nested matches
deeply enough to peek inside the Omul arguments.
Definition match_neg (
e:
expr) :
option expr :=
match e with
|
Eop (
Orsubimm n) (
t:::
Enil) =>
if Int.eq n Int.zero then Some t else None
| _ =>
None
end.
Definition mls_or_mla (
e1 e2 e3:
expr) :
expr :=
if Archi.thumb2_support then
match match_neg e1 with
|
Some t1 =>
Eop Omls (
t1:::
e2:::
e3:::
Enil)
|
None =>
match match_neg e2 with
|
Some t2 =>
Eop Omls (
t2:::
e1:::
e3:::
Enil)
|
None =>
Eop Omla (
e1:::
e2:::
e3:::
Enil)
end
end
else Eop Omla (
e1:::
e2:::
e3:::
Enil).
Original definition:
Nondetfunction add (e1: expr) (e2: expr) :=
match e1, e2 with
| Eop (Ointconst n1) Enil, t2 => addimm n1 t2
| t1, Eop (Ointconst n2) Enil => addimm n2 t1
| Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
| Eop(Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil))
| t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil))
| Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil)
| t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil)
| Eop Omul (t1:::t2:::Enil), t3 => mls_or_mla t1 t2 t3
| t1, Eop Omul (t2:::t3:::Enil) => mls_or_mla t2 t3 t1
| _, _ => Eop Oadd (e1:::e2:::Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
add_case1:
forall n1 t2,
add_cases (
Eop (
Ointconst n1)
Enil) (
t2)
|
add_case2:
forall t1 n2,
add_cases (
t1) (
Eop (
Ointconst n2)
Enil)
|
add_case3:
forall n1 t1 n2 t2,
add_cases (
Eop (
Oaddimm n1) (
t1:::
Enil)) (
Eop (
Oaddimm n2) (
t2:::
Enil))
|
add_case4:
forall n1 t1 t2,
add_cases (
Eop(
Oaddimm n1) (
t1:::
Enil)) (
t2)
|
add_case5:
forall t1 n2 t2,
add_cases (
t1) (
Eop (
Oaddimm n2) (
t2:::
Enil))
|
add_case6:
forall s t1 t2,
add_cases (
Eop (
Oshift s) (
t1:::
Enil)) (
t2)
|
add_case7:
forall t1 s t2,
add_cases (
t1) (
Eop (
Oshift s) (
t2:::
Enil))
|
add_case8:
forall t1 t2 t3,
add_cases (
Eop Omul (
t1:::
t2:::
Enil)) (
t3)
|
add_case9:
forall t1 t2 t3,
add_cases (
t1) (
Eop Omul (
t2:::
t3:::
Enil))
|
add_default:
forall (
e1:
expr) (
e2:
expr),
add_cases e1 e2.
Definition add_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return add_cases zz1 zz2 with
|
Eop (
Ointconst n1)
Enil,
t2 =>
add_case1 n1 t2
|
t1,
Eop (
Ointconst n2)
Enil =>
add_case2 t1 n2
|
Eop (
Oaddimm n1) (
t1:::
Enil),
Eop (
Oaddimm n2) (
t2:::
Enil) =>
add_case3 n1 t1 n2 t2
|
Eop(
Oaddimm n1) (
t1:::
Enil),
t2 =>
add_case4 n1 t1 t2
|
t1,
Eop (
Oaddimm n2) (
t2:::
Enil) =>
add_case5 t1 n2 t2
|
Eop (
Oshift s) (
t1:::
Enil),
t2 =>
add_case6 s t1 t2
|
t1,
Eop (
Oshift s) (
t2:::
Enil) =>
add_case7 t1 s t2
|
Eop Omul (
t1:::
t2:::
Enil),
t3 =>
add_case8 t1 t2 t3
|
t1,
Eop Omul (
t2:::
t3:::
Enil) =>
add_case9 t1 t2 t3
|
e1,
e2 =>
add_default e1 e2
end.
Definition add (
e1:
expr) (
e2:
expr) :=
match add_match e1 e2 with
|
add_case1 n1 t2 =>
addimm n1 t2
|
add_case2 t1 n2 =>
addimm n2 t1
|
add_case3 n1 t1 n2 t2 =>
addimm (
Int.add n1 n2) (
Eop Oadd (
t1:::
t2:::
Enil))
|
add_case4 n1 t1 t2 =>
addimm n1 (
Eop Oadd (
t1:::
t2:::
Enil))
|
add_case5 t1 n2 t2 =>
addimm n2 (
Eop Oadd (
t1:::
t2:::
Enil))
|
add_case6 s t1 t2 =>
Eop (
Oaddshift s) (
t2:::
t1:::
Enil)
|
add_case7 t1 s t2 =>
Eop (
Oaddshift s) (
t1:::
t2:::
Enil)
|
add_case8 t1 t2 t3 =>
mls_or_mla t1 t2 t3
|
add_case9 t1 t2 t3 =>
mls_or_mla t2 t3 t1
|
add_default e1 e2 =>
Eop Oadd (
e1:::
e2:::
Enil)
end.
Integer and pointer subtraction
Original definition:
Nondetfunction rsubimm (n: int) (e: expr) :=
match e with
| Eop (Ointconst m) Enil => Eop (Ointconst (Int.sub n m)) Enil
| Eop (Oaddimm m) (t:::Enil) => Eop (Orsubimm (Int.sub n m)) (t:::Enil)
| Eop (Orsubimm m) (t:::Enil) => Eop (Oaddimm (Int.sub n m)) (t:::Enil)
| _ => Eop (Orsubimm n) (e:::Enil)
end.
:
forall (
e:
expr),
Type :=
|
rsubimm_case1:
forall m,
rsubimm_cases (
Eop (
Ointconst m)
Enil)
|
rsubimm_case2:
forall m t,
rsubimm_cases (
Eop (
Oaddimm m) (
t:::
Enil))
|
rsubimm_case3:
forall m t,
rsubimm_cases (
Eop (
Orsubimm m) (
t:::
Enil))
|
rsubimm_default:
forall (
e:
expr),
rsubimm_cases e.
Definition rsubimm_match (
e:
expr) :=
match e as zz1 return rsubimm_cases zz1 with
|
Eop (
Ointconst m)
Enil =>
rsubimm_case1 m
|
Eop (
Oaddimm m) (
t:::
Enil) =>
rsubimm_case2 m t
|
Eop (
Orsubimm m) (
t:::
Enil) =>
rsubimm_case3 m t
|
e =>
rsubimm_default e
end.
Definition rsubimm (
n:
int) (
e:
expr) :=
match rsubimm_match e with
|
rsubimm_case1 m =>
Eop (
Ointconst (
Int.sub n m))
Enil
|
rsubimm_case2 m t =>
Eop (
Orsubimm (
Int.sub n m)) (
t:::
Enil)
|
rsubimm_case3 m t =>
Eop (
Oaddimm (
Int.sub n m)) (
t:::
Enil)
|
rsubimm_default e =>
Eop (
Orsubimm n) (
e:::
Enil)
end.
Original definition:
Nondetfunction sub (e1: expr) (e2: expr) :=
match e1, e2 with
| t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1
| Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
| Eop (Oaddimm n1) (t1:::Enil), t2 =>
addimm n1 (Eop Osub (t1:::t2:::Enil))
| t1, Eop (Oaddimm n2) (t2:::Enil) =>
addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
| Eop (Ointconst n1) Enil, t2 => rsubimm n1 t2
| Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil)
| t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil)
| t1, Eop Omul (t2:::t3:::Enil) =>
if Archi.thumb2_support
then Eop Omls (t2:::t3:::t1:::Enil)
else Eop Osub (e1:::e2:::Enil)
| _, _ => Eop Osub (e1:::e2:::Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
sub_case1:
forall t1 n2,
sub_cases (
t1) (
Eop (
Ointconst n2)
Enil)
|
sub_case2:
forall n1 t1 n2 t2,
sub_cases (
Eop (
Oaddimm n1) (
t1:::
Enil)) (
Eop (
Oaddimm n2) (
t2:::
Enil))
|
sub_case3:
forall n1 t1 t2,
sub_cases (
Eop (
Oaddimm n1) (
t1:::
Enil)) (
t2)
|
sub_case4:
forall t1 n2 t2,
sub_cases (
t1) (
Eop (
Oaddimm n2) (
t2:::
Enil))
|
sub_case5:
forall n1 t2,
sub_cases (
Eop (
Ointconst n1)
Enil) (
t2)
|
sub_case6:
forall s t1 t2,
sub_cases (
Eop (
Oshift s) (
t1:::
Enil)) (
t2)
|
sub_case7:
forall t1 s t2,
sub_cases (
t1) (
Eop (
Oshift s) (
t2:::
Enil))
|
sub_case8:
forall t1 t2 t3,
sub_cases (
t1) (
Eop Omul (
t2:::
t3:::
Enil))
|
sub_default:
forall (
e1:
expr) (
e2:
expr),
sub_cases e1 e2.
Definition sub_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return sub_cases zz1 zz2 with
|
t1,
Eop (
Ointconst n2)
Enil =>
sub_case1 t1 n2
|
Eop (
Oaddimm n1) (
t1:::
Enil),
Eop (
Oaddimm n2) (
t2:::
Enil) =>
sub_case2 n1 t1 n2 t2
|
Eop (
Oaddimm n1) (
t1:::
Enil),
t2 =>
sub_case3 n1 t1 t2
|
t1,
Eop (
Oaddimm n2) (
t2:::
Enil) =>
sub_case4 t1 n2 t2
|
Eop (
Ointconst n1)
Enil,
t2 =>
sub_case5 n1 t2
|
Eop (
Oshift s) (
t1:::
Enil),
t2 =>
sub_case6 s t1 t2
|
t1,
Eop (
Oshift s) (
t2:::
Enil) =>
sub_case7 t1 s t2
|
t1,
Eop Omul (
t2:::
t3:::
Enil) =>
sub_case8 t1 t2 t3
|
e1,
e2 =>
sub_default e1 e2
end.
Definition sub (
e1:
expr) (
e2:
expr) :=
match sub_match e1 e2 with
|
sub_case1 t1 n2 =>
addimm (
Int.neg n2)
t1
|
sub_case2 n1 t1 n2 t2 =>
addimm (
Int.sub n1 n2) (
Eop Osub (
t1:::
t2:::
Enil))
|
sub_case3 n1 t1 t2 =>
addimm n1 (
Eop Osub (
t1:::
t2:::
Enil))
|
sub_case4 t1 n2 t2 =>
addimm (
Int.neg n2) (
Eop Osub (
t1:::
t2:::
Enil))
|
sub_case5 n1 t2 =>
rsubimm n1 t2
|
sub_case6 s t1 t2 =>
Eop (
Orsubshift s) (
t2:::
t1:::
Enil)
|
sub_case7 t1 s t2 =>
Eop (
Osubshift s) (
t1:::
t2:::
Enil)
|
sub_case8 t1 t2 t3 =>
if Archi.thumb2_support then Eop Omls (
t2:::
t3:::
t1:::
Enil)
else Eop Osub (
e1:::
e2:::
Enil)
|
sub_default e1 e2 =>
Eop Osub (
e1:::
e2:::
Enil)
end.
Definition negint (
e:
expr) :=
rsubimm Int.zero e.
Immediate shifts
Original definition:
Nondetfunction shlimm (e1: expr) (n: int) :=
if Int.eq n Int.zero then
e1
else if negb (Int.ltu n Int.iwordsize) then
Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil)
else match e1 with
| Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shl n1 n)) Enil
| Eop (Oshift (Slsl n1)) (t1:::Enil) =>
if Int.ltu (Int.add n n1) Int.iwordsize
then Eop (Oshift (Slsl (mk_shift_amount(Int.add n n1)))) (t1:::Enil)
else Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil)
| _ => Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil)
end.
:
forall (
e1:
expr) ,
Type :=
|
shlimm_case1:
forall n1,
shlimm_cases (
Eop (
Ointconst n1)
Enil)
|
shlimm_case2:
forall n1 t1,
shlimm_cases (
Eop (
Oshift (
Slsl n1)) (
t1:::
Enil))
|
shlimm_default:
forall (
e1:
expr) ,
shlimm_cases e1.
Definition shlimm_match (
e1:
expr) :=
match e1 as zz1 return shlimm_cases zz1 with
|
Eop (
Ointconst n1)
Enil =>
shlimm_case1 n1
|
Eop (
Oshift (
Slsl n1)) (
t1:::
Enil) =>
shlimm_case2 n1 t1
|
e1 =>
shlimm_default e1
end.
Definition shlimm (
e1:
expr) (
n:
int) :=
if Int.eq n Int.zero then e1 else if negb (
Int.ltu n Int.iwordsize)
then Eop Oshl (
e1 :::
Eop (
Ointconst n)
Enil :::
Enil)
else match shlimm_match e1 with
|
shlimm_case1 n1 =>
Eop (
Ointconst(
Int.shl n1 n))
Enil
|
shlimm_case2 n1 t1 =>
if Int.ltu (
Int.add n n1)
Int.iwordsize then Eop (
Oshift (
Slsl (
mk_shift_amount(
Int.add n n1)))) (
t1:::
Enil)
else Eop (
Oshift (
Slsl (
mk_shift_amount n))) (
e1:::
Enil)
|
shlimm_default e1 =>
Eop (
Oshift (
Slsl (
mk_shift_amount n))) (
e1:::
Enil)
end.
Original definition:
Nondetfunction shruimm (e1: expr) (n: int) :=
if Int.eq n Int.zero then
e1
else if negb (Int.ltu n Int.iwordsize) then
Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil)
else match e1 with
| Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shru n1 n)) Enil
| Eop (Oshift (Slsr n1)) (t1:::Enil) =>
if Int.ltu (Int.add n n1) Int.iwordsize
then Eop (Oshift (Slsr (mk_shift_amount (Int.add n n1)))) (t1:::Enil)
else Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil)
| Eop (Oshift (Slsl n1)) (t1:::Enil) =>
if Archi.thumb2_support && Compopts.bitfield_ops tt &&
(Int.ltu n1 Int.iwordsize) &&
(negb (Int.ltu n n1))
then Eop (Oubfx (Int.sub n n1) (Int.sub Int.iwordsize n))
(t1 ::: Enil)
else
Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil)
| _ => Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil)
end.
:
forall (
e1:
expr) ,
Type :=
|
shruimm_case1:
forall n1,
shruimm_cases (
Eop (
Ointconst n1)
Enil)
|
shruimm_case2:
forall n1 t1,
shruimm_cases (
Eop (
Oshift (
Slsr n1)) (
t1:::
Enil))
|
shruimm_case3:
forall n1 t1,
shruimm_cases (
Eop (
Oshift (
Slsl n1)) (
t1:::
Enil))
|
shruimm_default:
forall (
e1:
expr) ,
shruimm_cases e1.
Definition shruimm_match (
e1:
expr) :=
match e1 as zz1 return shruimm_cases zz1 with
|
Eop (
Ointconst n1)
Enil =>
shruimm_case1 n1
|
Eop (
Oshift (
Slsr n1)) (
t1:::
Enil) =>
shruimm_case2 n1 t1
|
Eop (
Oshift (
Slsl n1)) (
t1:::
Enil) =>
shruimm_case3 n1 t1
|
e1 =>
shruimm_default e1
end.
Definition shruimm (
e1:
expr) (
n:
int) :=
if Int.eq n Int.zero then e1 else if negb (
Int.ltu n Int.iwordsize)
then Eop Oshru (
e1 :::
Eop (
Ointconst n)
Enil :::
Enil)
else match shruimm_match e1 with
|
shruimm_case1 n1 =>
Eop (
Ointconst(
Int.shru n1 n))
Enil
|
shruimm_case2 n1 t1 =>
if Int.ltu (
Int.add n n1)
Int.iwordsize then Eop (
Oshift (
Slsr (
mk_shift_amount (
Int.add n n1)))) (
t1:::
Enil)
else Eop (
Oshift (
Slsr (
mk_shift_amount n))) (
e1:::
Enil)
|
shruimm_case3 n1 t1 =>
if Archi.thumb2_support &&
Compopts.bitfield_ops tt && (
Int.ltu n1 Int.iwordsize) && (
negb (
Int.ltu n n1))
then Eop (
Oubfx (
Int.sub n n1) (
Int.sub Int.iwordsize n)) (
t1 :::
Enil)
else Eop (
Oshift (
Slsr (
mk_shift_amount n))) (
e1:::
Enil)
|
shruimm_default e1 =>
Eop (
Oshift (
Slsr (
mk_shift_amount n))) (
e1:::
Enil)
end.
Original definition:
Nondetfunction shrimm (e1: expr) (n: int) :=
if Int.eq n Int.zero then
e1
else if negb (Int.ltu n Int.iwordsize) then
Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil)
else
match e1 with
| Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shr n1 n)) Enil
| Eop (Oshift (Sasr n1)) (t1:::Enil) =>
if Int.ltu (Int.add n n1) Int.iwordsize
then Eop (Oshift (Sasr (mk_shift_amount (Int.add n n1)))) (t1:::Enil)
else Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil)
| Eop (Oshift (Slsl n1)) (t1:::Enil) =>
if Archi.thumb2_support && Compopts.bitfield_ops tt &&
(Int.ltu n1 Int.iwordsize) &&
(negb (Int.ltu n n1))
then Eop (Osbfx (Int.sub n n1) (Int.sub Int.iwordsize n))
(t1 ::: Enil)
else
Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil)
| _ => Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil)
end.
:
forall (
e1:
expr) ,
Type :=
|
shrimm_case1:
forall n1,
shrimm_cases (
Eop (
Ointconst n1)
Enil)
|
shrimm_case2:
forall n1 t1,
shrimm_cases (
Eop (
Oshift (
Sasr n1)) (
t1:::
Enil))
|
shrimm_case3:
forall n1 t1,
shrimm_cases (
Eop (
Oshift (
Slsl n1)) (
t1:::
Enil))
|
shrimm_default:
forall (
e1:
expr) ,
shrimm_cases e1.
Definition shrimm_match (
e1:
expr) :=
match e1 as zz1 return shrimm_cases zz1 with
|
Eop (
Ointconst n1)
Enil =>
shrimm_case1 n1
|
Eop (
Oshift (
Sasr n1)) (
t1:::
Enil) =>
shrimm_case2 n1 t1
|
Eop (
Oshift (
Slsl n1)) (
t1:::
Enil) =>
shrimm_case3 n1 t1
|
e1 =>
shrimm_default e1
end.
Definition shrimm (
e1:
expr) (
n:
int) :=
if Int.eq n Int.zero then e1 else if negb (
Int.ltu n Int.iwordsize)
then Eop Oshr (
e1 :::
Eop (
Ointconst n)
Enil :::
Enil)
else match shrimm_match e1 with
|
shrimm_case1 n1 =>
Eop (
Ointconst(
Int.shr n1 n))
Enil
|
shrimm_case2 n1 t1 =>
if Int.ltu (
Int.add n n1)
Int.iwordsize then Eop (
Oshift (
Sasr (
mk_shift_amount (
Int.add n n1)))) (
t1:::
Enil)
else Eop (
Oshift (
Sasr (
mk_shift_amount n))) (
e1:::
Enil)
|
shrimm_case3 n1 t1 =>
if Archi.thumb2_support &&
Compopts.bitfield_ops tt && (
Int.ltu n1 Int.iwordsize) && (
negb (
Int.ltu n n1))
then Eop (
Osbfx (
Int.sub n n1) (
Int.sub Int.iwordsize n)) (
t1 :::
Enil)
else Eop (
Oshift (
Sasr (
mk_shift_amount n))) (
e1:::
Enil)
|
shrimm_default e1 =>
Eop (
Oshift (
Sasr (
mk_shift_amount n))) (
e1:::
Enil)
end.
Integer multiply
Definition mulimm_base (
n1:
int) (
e2:
expr) :=
match Int.one_bits n1 with
|
i ::
nil =>
shlimm e2 i
|
i ::
j ::
nil =>
Elet e2
(
add (
shlimm (
Eletvar 0)
i) (
shlimm (
Eletvar 0)
j))
| _ =>
match Int.one_bits (
Int.add n1 Int.one)
with
|
k ::
nil =>
if Int.ltu k Int.iwordsize then
Elet e2
(
Eop (
Orsubshift (
Slsl (
mk_shift_amount k)))
(
Eletvar 0 :::
Eletvar 0 :::
Enil))
else
Eop Omul (
Eop (
Ointconst n1)
Enil :::
e2 :::
Enil)
| _ =>
match Int.one_bits (
Int.add (
Int.neg n1)
Int.one)
with
|
k ::
nil =>
if Int.ltu k Int.iwordsize then
Elet e2
(
Eop (
Osubshift (
Slsl (
mk_shift_amount k)))
(
Eletvar 0 :::
Eletvar 0 :::
Enil))
else
Eop Omul (
Eop (
Ointconst n1)
Enil :::
e2 :::
Enil)
| _ =>
Eop Omul (
Eop (
Ointconst n1)
Enil :::
e2 :::
Enil)
end
end
end.
Original definition:
Nondetfunction mulimm (n1: int) (e2: expr) :=
if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil
else if Int.eq n1 Int.one then e2
else match e2 with
| Eop (Ointconst n2) Enil => Eop (Ointconst(Int.mul n1 n2)) Enil
| Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.mul n1 n2) (mulimm_base n1 t2)
| _ => mulimm_base n1 e2
end.
:
forall (
e2:
expr),
Type :=
|
mulimm_case1:
forall n2,
mulimm_cases (
Eop (
Ointconst n2)
Enil)
|
mulimm_case2:
forall n2 t2,
mulimm_cases (
Eop (
Oaddimm n2) (
t2:::
Enil))
|
mulimm_default:
forall (
e2:
expr),
mulimm_cases e2.
Definition mulimm_match (
e2:
expr) :=
match e2 as zz1 return mulimm_cases zz1 with
|
Eop (
Ointconst n2)
Enil =>
mulimm_case1 n2
|
Eop (
Oaddimm n2) (
t2:::
Enil) =>
mulimm_case2 n2 t2
|
e2 =>
mulimm_default e2
end.
Definition mulimm (
n1:
int) (
e2:
expr) :=
if Int.eq n1 Int.zero then Eop (
Ointconst Int.zero)
Enil else if Int.eq n1 Int.one then e2 else match mulimm_match e2 with
|
mulimm_case1 n2 =>
Eop (
Ointconst(
Int.mul n1 n2))
Enil
|
mulimm_case2 n2 t2 =>
addimm (
Int.mul n1 n2) (
mulimm_base n1 t2)
|
mulimm_default e2 =>
mulimm_base n1 e2
end.
Original definition:
Nondetfunction mul (e1: expr) (e2: expr) :=
match e1, e2 with
| Eop (Ointconst n1) Enil, t2 => mulimm n1 t2
| t1, Eop (Ointconst n2) Enil => mulimm n2 t1
| _, _ => Eop Omul (e1:::e2:::Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
mul_case1:
forall n1 t2,
mul_cases (
Eop (
Ointconst n1)
Enil) (
t2)
|
mul_case2:
forall t1 n2,
mul_cases (
t1) (
Eop (
Ointconst n2)
Enil)
|
mul_default:
forall (
e1:
expr) (
e2:
expr),
mul_cases e1 e2.
Definition mul_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return mul_cases zz1 zz2 with
|
Eop (
Ointconst n1)
Enil,
t2 =>
mul_case1 n1 t2
|
t1,
Eop (
Ointconst n2)
Enil =>
mul_case2 t1 n2
|
e1,
e2 =>
mul_default e1 e2
end.
Definition mul (
e1:
expr) (
e2:
expr) :=
match mul_match e1 e2 with
|
mul_case1 n1 t2 =>
mulimm n1 t2
|
mul_case2 t1 n2 =>
mulimm n2 t1
|
mul_default e1 e2 =>
Eop Omul (
e1:::
e2:::
Enil)
end.
Definition mulhs (
e1:
expr) (
e2:
expr) :=
Eop Omulhs (
e1 :::
e2 :::
Enil).
Definition mulhu (
e1:
expr) (
e2:
expr) :=
Eop Omulhu (
e1 :::
e2 :::
Enil).
Bitwise and, or, xor
Definition bfc n e :=
let zstart :=
int_lowest_bit (
Int.not n)
in
let zstop :=
int_highest_bit (
Int.not n)
in
Eop (
Obfc (
Int.repr zstart) (
Int.repr (
Z.succ (
zstop -
zstart)))) (
e:::
Enil).
Original definition:
Nondetfunction ubfx (n: int) (e : expr) :=
match e with
| Eop (Oshift (Slsr lsb)) (e2 ::: Enil) =>
let nbits := Z.min (Z.succ (int_highest_bit n)) (32 - Int.unsigned lsb.(s_amount)) in
Eop (Oubfx lsb (Int.repr nbits)) (e2:::Enil)
| _ =>
let nbits := Z.succ (int_highest_bit n) in
if zlt nbits 32
then Eop (Obfc (Int.repr nbits) (Int.repr (32 - nbits))) (e:::Enil)
else e
end.
:
forall (
e :
expr),
Type :=
|
ubfx_case1:
forall lsb e2,
ubfx_cases (
Eop (
Oshift (
Slsr lsb)) (
e2 :::
Enil))
|
ubfx_default:
forall (
e :
expr),
ubfx_cases e.
Definition ubfx_match (
e :
expr) :=
match e as zz1 return ubfx_cases zz1 with
|
Eop (
Oshift (
Slsr lsb)) (
e2 :::
Enil) =>
ubfx_case1 lsb e2
|
e =>
ubfx_default e
end.
Definition ubfx (
n:
int) (
e :
expr) :=
match ubfx_match e with
|
ubfx_case1 lsb e2 =>
let nbits :=
Z.min (
Z.succ (
int_highest_bit n)) (32 -
Int.unsigned lsb.(
s_amount))
in Eop (
Oubfx lsb (
Int.repr nbits)) (
e2:::
Enil)
|
ubfx_default e =>
let nbits :=
Z.succ (
int_highest_bit n)
in if zlt nbits 32
then Eop (
Obfc (
Int.repr nbits) (
Int.repr (32 -
nbits))) (
e:::
Enil)
else e
end.
(e3 >> lsb) & n1 with n1 = 2^sz - 1 and lsb + sz <= 32 is the
bitfield bits lsb..lsb+sz) of e3, i.e. Oubfx lsb sz e3. Helper
used by andimm to lower the (x >> N) & MASK idiom — extracted
into its own definition because Nondetfunction doesn't accept
nested matches inside its arms. Gated on
Archi.thumb2_support && Compopts.bitfield_ops tt since Oubfx
requires Thumb-2 (ARMv6T2 / ARMv7+).
Definition andimm_lsr_to_ubfx (
n1:
int) (
lsb:
shift_amount) (
e3 e2:
expr) :
expr :=
if Archi.thumb2_support &&
Compopts.bitfield_ops tt then
match Int.is_power2 (
Int.add n1 Int.one)
with
|
Some sz =>
if negb (
Int.ltu Int.iwordsize (
Int.add lsb sz))
then Eop (
Oubfx lsb sz) (
e3:::
Enil)
else Eop (
Oandimm n1) (
e2:::
Enil)
|
None =>
Eop (
Oandimm n1) (
e2:::
Enil)
end
else Eop (
Oandimm n1) (
e2:::
Enil).
Original definition:
Nondetfunction andimm (n1: int) (e2: expr) :=
if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else
if Int.eq n1 Int.mone then e2 else
(* Try constant-folding first: if [e2] is a constant or already an
[Oandimm] chain, fold the masks before deciding between [Oandimm],
[ubfx], and [bfc]. The combined mask is often a Thumb-2-encodable
immediate even when [n1] alone wasn't, in which case a single
[Oandimm] is strictly better than [ubfx]/[bfc] of an inner
[Oandimm]. *)
match e2 with
| Eop (Ointconst n2) Enil =>
Eop (Ointconst (Int.and n1 n2)) Enil
| Eop (Oandimm n2) (t2:::Enil) =>
Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
| Eload Mint8unsigned addr args =>
(* Loaded byte is already in [0, 255]; if the mask covers the whole
byte, the [Oandimm] is identity. *)
if Int.eq n1 (Int.repr 255) then e2
else Eop (Oandimm n1) (e2:::Enil)
| Eload Mint16unsigned addr args =>
if Int.eq n1 (Int.repr 65535) then e2
else Eop (Oandimm n1) (e2:::Enil)
| Eop (Oshift (Slsr lsb)) (e3:::Enil) =>
andimm_lsr_to_ubfx n1 lsb e3 e2
| _ =>
(* Prefer the 3-operand [Oandimm] when [n1] is encodable as a single
Thumb-2 modified immediate. The 2-operand [bfc]/[ubfx]-fallback
paths below would force a [mov rd, rs] copy whenever [rs] is still
live afterwards, costing an extra instruction. *)
if Archi.thumb2_support &&
Compopts.bitfield_ops tt &&
negb (is_immed_arith OTHER n1) &&
(Int.eq n1 (Int.repr (zbitfield_mask (int_highest_bit n1) 0)))
then ubfx n1 e2
else if Archi.thumb2_support &&
Compopts.bitfield_ops tt &&
negb (is_immed_arith OTHER n1) &&
(Int.eq n1 (Int.not (Int.repr (zbitfield_mask (int_highest_bit (Int.not n1)) (int_lowest_bit (Int.not n1))))))
then bfc n1 e2
else Eop (Oandimm n1) (e2:::Enil)
end.
:
forall (
e2:
expr),
Type :=
|
andimm_case1:
forall n2,
andimm_cases (
Eop (
Ointconst n2)
Enil)
|
andimm_case2:
forall n2 t2,
andimm_cases (
Eop (
Oandimm n2) (
t2:::
Enil))
|
andimm_case3:
forall addr args,
andimm_cases (
Eload Mint8unsigned addr args)
|
andimm_case4:
forall addr args,
andimm_cases (
Eload Mint16unsigned addr args)
|
andimm_case5:
forall lsb e3,
andimm_cases (
Eop (
Oshift (
Slsr lsb)) (
e3:::
Enil))
|
andimm_default:
forall (
e2:
expr),
andimm_cases e2.
Definition andimm_match (
e2:
expr) :=
match e2 as zz1 return andimm_cases zz1 with
|
Eop (
Ointconst n2)
Enil =>
andimm_case1 n2
|
Eop (
Oandimm n2) (
t2:::
Enil) =>
andimm_case2 n2 t2
|
Eload Mint8unsigned addr args =>
andimm_case3 addr args
|
Eload Mint16unsigned addr args =>
andimm_case4 addr args
|
Eop (
Oshift (
Slsr lsb)) (
e3:::
Enil) =>
andimm_case5 lsb e3
|
e2 =>
andimm_default e2
end.
Definition andimm (
n1:
int) (
e2:
expr) :=
if Int.eq n1 Int.zero then Eop (
Ointconst Int.zero)
Enil else if Int.eq n1 Int.mone then e2 else match andimm_match e2 with
|
andimm_case1 n2 =>
Eop (
Ointconst (
Int.and n1 n2))
Enil
|
andimm_case2 n2 t2 =>
Eop (
Oandimm (
Int.and n1 n2)) (
t2:::
Enil)
|
andimm_case3 addr args =>
if Int.eq n1 (
Int.repr 255)
then e2 else Eop (
Oandimm n1) (
e2:::
Enil)
|
andimm_case4 addr args =>
if Int.eq n1 (
Int.repr 65535)
then e2 else Eop (
Oandimm n1) (
e2:::
Enil)
|
andimm_case5 lsb e3 =>
andimm_lsr_to_ubfx n1 lsb e3 e2
|
andimm_default e2 =>
if Archi.thumb2_support &&
Compopts.bitfield_ops tt &&
negb (
is_immed_arith OTHER n1) && (
Int.eq n1 (
Int.repr (
zbitfield_mask (
int_highest_bit n1) 0)))
then ubfx n1 e2 else if Archi.thumb2_support &&
Compopts.bitfield_ops tt &&
negb (
is_immed_arith OTHER n1) && (
Int.eq n1 (
Int.not (
Int.repr (
zbitfield_mask (
int_highest_bit (
Int.not n1)) (
int_lowest_bit (
Int.not n1))))))
then bfc n1 e2 else Eop (
Oandimm n1) (
e2:::
Enil)
end.
Original definition:
Nondetfunction and (e1: expr) (e2: expr) :=
match e1, e2 with
| Eop (Ointconst n1) Enil, Eop (Ointconst n2) Enil =>
Eop (Ointconst (Int.and n1 n2)) Enil
| Eop (Ointconst n1) Enil, t2 => andimm n1 t2
| t1, Eop (Ointconst n2) Enil => andimm n2 t1
| Eop (Oshift s) (t1:::Enil), t2 => Eop (Oandshift s) (t2:::t1:::Enil)
| t1, Eop (Oshift s) (t2:::Enil) => Eop (Oandshift s) (t1:::t2:::Enil)
| Eop (Onotshift s) (t1:::Enil), t2 => Eop (Obicshift s) (t2:::t1:::Enil)
| t1, Eop (Onotshift s) (t2:::Enil) => Eop (Obicshift s) (t1:::t2:::Enil)
| Eop Onot (t1:::Enil), t2 => Eop Obic (t2:::t1:::Enil)
| t1, Eop Onot (t2:::Enil) => Eop Obic (t1:::t2:::Enil)
| _, _ => Eop Oand (e1:::e2:::Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
and_case1:
forall n1 n2,
and_cases (
Eop (
Ointconst n1)
Enil) (
Eop (
Ointconst n2)
Enil)
|
and_case2:
forall n1 t2,
and_cases (
Eop (
Ointconst n1)
Enil) (
t2)
|
and_case3:
forall t1 n2,
and_cases (
t1) (
Eop (
Ointconst n2)
Enil)
|
and_case4:
forall s t1 t2,
and_cases (
Eop (
Oshift s) (
t1:::
Enil)) (
t2)
|
and_case5:
forall t1 s t2,
and_cases (
t1) (
Eop (
Oshift s) (
t2:::
Enil))
|
and_case6:
forall s t1 t2,
and_cases (
Eop (
Onotshift s) (
t1:::
Enil)) (
t2)
|
and_case7:
forall t1 s t2,
and_cases (
t1) (
Eop (
Onotshift s) (
t2:::
Enil))
|
and_case8:
forall t1 t2,
and_cases (
Eop Onot (
t1:::
Enil)) (
t2)
|
and_case9:
forall t1 t2,
and_cases (
t1) (
Eop Onot (
t2:::
Enil))
|
and_default:
forall (
e1:
expr) (
e2:
expr),
and_cases e1 e2.
Definition and_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return and_cases zz1 zz2 with
|
Eop (
Ointconst n1)
Enil,
Eop (
Ointconst n2)
Enil =>
and_case1 n1 n2
|
Eop (
Ointconst n1)
Enil,
t2 =>
and_case2 n1 t2
|
t1,
Eop (
Ointconst n2)
Enil =>
and_case3 t1 n2
|
Eop (
Oshift s) (
t1:::
Enil),
t2 =>
and_case4 s t1 t2
|
t1,
Eop (
Oshift s) (
t2:::
Enil) =>
and_case5 t1 s t2
|
Eop (
Onotshift s) (
t1:::
Enil),
t2 =>
and_case6 s t1 t2
|
t1,
Eop (
Onotshift s) (
t2:::
Enil) =>
and_case7 t1 s t2
|
Eop Onot (
t1:::
Enil),
t2 =>
and_case8 t1 t2
|
t1,
Eop Onot (
t2:::
Enil) =>
and_case9 t1 t2
|
e1,
e2 =>
and_default e1 e2
end.
Definition and (
e1:
expr) (
e2:
expr) :=
match and_match e1 e2 with
|
and_case1 n1 n2 =>
Eop (
Ointconst (
Int.and n1 n2))
Enil
|
and_case2 n1 t2 =>
andimm n1 t2
|
and_case3 t1 n2 =>
andimm n2 t1
|
and_case4 s t1 t2 =>
Eop (
Oandshift s) (
t2:::
t1:::
Enil)
|
and_case5 t1 s t2 =>
Eop (
Oandshift s) (
t1:::
t2:::
Enil)
|
and_case6 s t1 t2 =>
Eop (
Obicshift s) (
t2:::
t1:::
Enil)
|
and_case7 t1 s t2 =>
Eop (
Obicshift s) (
t1:::
t2:::
Enil)
|
and_case8 t1 t2 =>
Eop Obic (
t2:::
t1:::
Enil)
|
and_case9 t1 t2 =>
Eop Obic (
t1:::
t2:::
Enil)
|
and_default e1 e2 =>
Eop Oand (
e1:::
e2:::
Enil)
end.
Conservative syntactic equality on CminorSel expressions, used by
rotation/byteswap recognition. Returns true only on PURE
expressions whose evaluation is deterministic given a fixed
environment and memory state. Originally limited to Evar;
extended to recurse through Eop and Eload so that rotation
idioms (x << n) | (x >> (32-n)) with x = Eload … (e.g.
BearSSL's state[d]) are recognised. Ebuiltin/Eexternal are
rejected (potentially side-effecting).
Fixpoint same_expr_pure (
e1 e2:
expr) :
bool :=
match e1,
e2 with
|
Evar v1,
Evar v2 =>
if ident_eq v1 v2 then true else false
|
Eop op1 args1,
Eop op2 args2 =>
if eq_operation op1 op2 then same_exprlist_pure args1 args2 else false
|
Eload chk1 addr1 args1,
Eload chk2 addr2 args2 =>
if chunk_eq chk1 chk2
then if eq_addressing addr1 addr2
then same_exprlist_pure args1 args2
else false
else false
| _, _ =>
false
end
with same_exprlist_pure (
es1 es2:
exprlist) :
bool :=
match es1,
es2 with
|
Enil,
Enil =>
true
|
Econs e1 r1,
Econs e2 r2 =>
if same_expr_pure e1 e2 then same_exprlist_pure r1 r2 else false
| _, _ =>
false
end.
Original definition:
Nondetfunction orimm (n1: int) (e2: expr) :=
if Int.eq n1 Int.zero then e2 else
if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else
match e2 with
| Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil
| Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
| _ => Eop (Oorimm n1) (e2:::Enil)
end.
:
forall (
e2:
expr),
Type :=
|
orimm_case1:
forall n2,
orimm_cases (
Eop (
Ointconst n2)
Enil)
|
orimm_case2:
forall n2 t2,
orimm_cases (
Eop (
Oorimm n2) (
t2:::
Enil))
|
orimm_default:
forall (
e2:
expr),
orimm_cases e2.
Definition orimm_match (
e2:
expr) :=
match e2 as zz1 return orimm_cases zz1 with
|
Eop (
Ointconst n2)
Enil =>
orimm_case1 n2
|
Eop (
Oorimm n2) (
t2:::
Enil) =>
orimm_case2 n2 t2
|
e2 =>
orimm_default e2
end.
Definition orimm (
n1:
int) (
e2:
expr) :=
if Int.eq n1 Int.zero then e2 else if Int.eq n1 Int.mone then Eop (
Ointconst Int.mone)
Enil else match orimm_match e2 with
|
orimm_case1 n2 =>
Eop (
Ointconst (
Int.or n1 n2))
Enil
|
orimm_case2 n2 t2 =>
Eop (
Oorimm (
Int.or n1 n2)) (
t2:::
Enil)
|
orimm_default e2 =>
Eop (
Oorimm n1) (
e2:::
Enil)
end.
Original definition:
Nondetfunction or (e1: expr) (e2: expr) :=
match e1, e2 with
| Eop (Ointconst n1) Enil, Eop (Ointconst n2) Enil =>
Eop (Ointconst (Int.or n1 n2)) Enil
| Eop (Ointconst n1) Enil, t2 => orimm n1 t2
| t1, Eop (Ointconst n2) Enil => orimm n2 t1
| (Eop (Oorshift (Slsr s8))
((Eop (Oorshift (Slsl s24a))
((Eop (Oshift (Slsl s8a))
((Eop (Oandimm c1) (x1:::Enil)):::Enil))
::: (Eop (Oandimm cFF) (x2:::Enil)) ::: Enil))
::: (Eop (Oandimm c2) (x3:::Enil)) ::: Enil)),
(Eop (Oshift (Slsr s24b))
((Eop (Oandimm cFF000000) (x4:::Enil)):::Enil)) =>
if Int.eq (s_amount s8) (Int.repr 8)
&& Int.eq (s_amount s24a) (Int.repr 24)
&& Int.eq (s_amount s8a) (Int.repr 8)
&& Int.eq (s_amount s24b) (Int.repr 24)
&& Int.eq c1 (Int.repr 65280)
&& Int.eq c2 (Int.repr 16711680)
&& Int.eq cFF (Int.repr 255)
&& Int.eq cFF000000 (Int.repr 4278190080)
&& same_expr_pure x1 x2
&& same_expr_pure x2 x3
&& same_expr_pure x3 x4
then Eop Obswap32 (x1:::Enil)
else Eop (Oorshift (Slsr s24b)) (e1 ::: (Eop (Oandimm cFF000000) (x4:::Enil)) ::: Enil)
| Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) =>
if Int.eq (Int.add n1 n2) Int.iwordsize
&& same_expr_pure t1 t2
then Eop (Oshift (Sror n2)) (t1:::Enil)
else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil)
| Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) =>
if Int.eq (Int.add n2 n1) Int.iwordsize
&& same_expr_pure t1 t2
then Eop (Oshift (Sror n1)) (t1:::Enil)
else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil)
| Eop Oshru (t1:::n1:::Enil),
Eop Oshl (t2:::(Eop (Orsubimm c32) (n2:::Enil)):::Enil) =>
if Int.eq c32 Int.iwordsize
&& same_expr_pure t1 t2
&& same_expr_pure n1 n2
then Eop Oror (t1:::n1:::Enil)
else Eop Oor (e1:::e2:::Enil)
| Eop Oshl (t1:::n1:::Enil),
Eop Oshru (t2:::(Eop (Orsubimm c32) (n2:::Enil)):::Enil) =>
if Int.eq c32 Int.iwordsize
&& same_expr_pure t1 t2
&& same_expr_pure n1 n2
then Eop Oror (t1:::(Eop (Orsubimm c32) (n1:::Enil)):::Enil)
else Eop Oor (e1:::e2:::Enil)
| (Eop (Oshift (Slsl lsb2))
((Eop (Oubfx ulsb usz) (fld:::Enil)):::Enil)),
(Eop (Obfc lsb sz) (prev:::Enil)) =>
if and_dec
(and_dec (Int.eq_dec ulsb Int.zero) (Int.eq_dec lsb lsb2))
(Int.eq_dec sz usz)
then Eop (Obfi lsb sz) (prev:::fld:::Enil)
else Eop Oor (e1:::e2:::Enil)
| (Eop (Obfc lsb sz) (prev:::Enil)),
(Eop (Oshift (Slsl lsb2))
((Eop (Oubfx ulsb usz) (fld:::Enil)):::Enil)) =>
if and_dec
(and_dec (Int.eq_dec ulsb Int.zero) (Int.eq_dec lsb lsb2))
(Int.eq_dec sz usz)
then Eop (Obfi lsb sz) (prev:::fld:::Enil)
else Eop Oor (e1:::e2:::Enil)
| (Eop (Oshift (Slsl lsb2))
((Eop (Obfc cl_lsb cl_sz) (fld:::Enil)):::Enil)),
(Eop (Obfc lsb sz) (prev:::Enil)) =>
if and_dec
(and_dec (Int.eq_dec lsb lsb2) (Int.eq_dec cl_lsb sz))
(and_dec
(Int.eq_dec (Int.add cl_lsb cl_sz) (Int.repr 32))
(zle (Int.unsigned cl_lsb + Int.unsigned cl_sz) 32))
then Eop (Obfi lsb sz) (prev:::fld:::Enil)
else Eop Oor (e1:::e2:::Enil)
| (Eop (Obfc lsb sz) (prev:::Enil)),
(Eop (Oshift (Slsl lsb2))
((Eop (Obfc cl_lsb cl_sz) (fld:::Enil)):::Enil)) =>
if and_dec
(and_dec (Int.eq_dec lsb lsb2) (Int.eq_dec cl_lsb sz))
(and_dec
(Int.eq_dec (Int.add cl_lsb cl_sz) (Int.repr 32))
(zle (Int.unsigned cl_lsb + Int.unsigned cl_sz) 32))
then Eop (Obfi lsb sz) (prev:::fld:::Enil)
else Eop Oor (e1:::e2:::Enil)
| (Eop (Oshift (Slsl lsb2))
((Eop (Oandimm m) (fld:::Enil)):::Enil)),
(Eop (Obfc lsb sz) (prev:::Enil)) =>
if and_dec
(Int.eq_dec lsb lsb2)
(Int.eq_dec m (Int.repr (Z.ones (Int.unsigned sz))))
then Eop (Obfi lsb sz) (prev:::fld:::Enil)
else Eop Oor (e1:::e2:::Enil)
| (Eop (Obfc lsb sz) (prev:::Enil)),
(Eop (Oshift (Slsl lsb2))
((Eop (Oandimm m) (fld:::Enil)):::Enil)) =>
if and_dec
(Int.eq_dec lsb lsb2)
(Int.eq_dec m (Int.repr (Z.ones (Int.unsigned sz))))
then Eop (Obfi lsb sz) (prev:::fld:::Enil)
else Eop Oor (e1:::e2:::Enil)
| Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil)
| t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::Enil)
| (Eop (Oandimm mask)
((Eop (Oshift (Slsl lsb2)) (fld:::Enil)):::Enil)),
(Eop (Obfc lsb sz) (prev:::Enil)) =>
let mask' := Int.shl (Int.repr (Z.ones (Int.unsigned sz))) lsb in
if and_dec (Int.eq_dec lsb lsb2) (Int.eq_dec mask' mask)
then Eop (Obfi lsb sz) (prev:::fld:::Enil)
else Eop Oor (e1:::e2:::Enil)
| (Eop (Obfc lsb sz) (prev:::Enil)),
(Eop (Oandimm mask)
((Eop (Oshift (Slsl lsb2)) (fld:::Enil)):::Enil)) =>
let mask' := Int.shl (Int.repr (Z.ones (Int.unsigned sz))) lsb in
if and_dec (Int.eq_dec lsb lsb2) (Int.eq_dec mask' mask)
then Eop (Obfi lsb sz) (prev:::fld:::Enil)
else Eop Oor (e1:::e2:::Enil)
| (Eop (Obfc rest_lsb rest_sz) (fld:::Enil)),
(Eop (Obfc lsb sz) (prev:::Enil)) =>
if and_dec
(and_dec (Int.eq_dec lsb Int.zero)
(Int.eq_dec rest_lsb sz))
(Int.eq_dec (Int.add rest_lsb rest_sz) (Int.repr 32))
then Eop (Obfi Int.zero sz) (prev:::fld:::Enil)
else Eop Oor (e1:::e2:::Enil)
| _, _ => Eop Oor (e1:::e2:::Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
or_case1:
forall n1 n2,
or_cases (
Eop (
Ointconst n1)
Enil) (
Eop (
Ointconst n2)
Enil)
|
or_case2:
forall n1 t2,
or_cases (
Eop (
Ointconst n1)
Enil) (
t2)
|
or_case3:
forall t1 n2,
or_cases (
t1) (
Eop (
Ointconst n2)
Enil)
|
or_case4:
forall s8 s24a s8a c1 x1 cFF x2 c2 x3 s24b cFF000000 x4,
or_cases ((
Eop (
Oorshift (
Slsr s8)) ((
Eop (
Oorshift (
Slsl s24a)) ((
Eop (
Oshift (
Slsl s8a)) ((
Eop (
Oandimm c1) (
x1:::
Enil)):::
Enil)) ::: (
Eop (
Oandimm cFF) (
x2:::
Enil)) :::
Enil)) ::: (
Eop (
Oandimm c2) (
x3:::
Enil)) :::
Enil))) ((
Eop (
Oshift (
Slsr s24b)) ((
Eop (
Oandimm cFF000000) (
x4:::
Enil)):::
Enil)))
|
or_case5:
forall n1 t1 n2 t2,
or_cases (
Eop (
Oshift (
Slsl n1)) (
t1:::
Enil)) (
Eop (
Oshift (
Slsr n2)) (
t2:::
Enil))
|
or_case6:
forall n1 t1 n2 t2,
or_cases (
Eop (
Oshift (
Slsr n1)) (
t1:::
Enil)) (
Eop (
Oshift (
Slsl n2)) (
t2:::
Enil))
|
or_case7:
forall t1 n1 t2 c32 n2,
or_cases (
Eop Oshru (
t1:::
n1:::
Enil)) (
Eop Oshl (
t2:::(
Eop (
Orsubimm c32) (
n2:::
Enil)):::
Enil))
|
or_case8:
forall t1 n1 t2 c32 n2,
or_cases (
Eop Oshl (
t1:::
n1:::
Enil)) (
Eop Oshru (
t2:::(
Eop (
Orsubimm c32) (
n2:::
Enil)):::
Enil))
|
or_case9:
forall lsb2 ulsb usz fld lsb sz prev,
or_cases ((
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Oubfx ulsb usz) (
fld:::
Enil)):::
Enil))) ((
Eop (
Obfc lsb sz) (
prev:::
Enil)))
|
or_case10:
forall lsb sz prev lsb2 ulsb usz fld,
or_cases ((
Eop (
Obfc lsb sz) (
prev:::
Enil))) ((
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Oubfx ulsb usz) (
fld:::
Enil)):::
Enil)))
|
or_case11:
forall lsb2 cl_lsb cl_sz fld lsb sz prev,
or_cases ((
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Obfc cl_lsb cl_sz) (
fld:::
Enil)):::
Enil))) ((
Eop (
Obfc lsb sz) (
prev:::
Enil)))
|
or_case12:
forall lsb sz prev lsb2 cl_lsb cl_sz fld,
or_cases ((
Eop (
Obfc lsb sz) (
prev:::
Enil))) ((
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Obfc cl_lsb cl_sz) (
fld:::
Enil)):::
Enil)))
|
or_case13:
forall lsb2 m fld lsb sz prev,
or_cases ((
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Oandimm m) (
fld:::
Enil)):::
Enil))) ((
Eop (
Obfc lsb sz) (
prev:::
Enil)))
|
or_case14:
forall lsb sz prev lsb2 m fld,
or_cases ((
Eop (
Obfc lsb sz) (
prev:::
Enil))) ((
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Oandimm m) (
fld:::
Enil)):::
Enil)))
|
or_case15:
forall s t1 t2,
or_cases (
Eop (
Oshift s) (
t1:::
Enil)) (
t2)
|
or_case16:
forall t1 s t2,
or_cases (
t1) (
Eop (
Oshift s) (
t2:::
Enil))
|
or_case17:
forall mask lsb2 fld lsb sz prev,
or_cases ((
Eop (
Oandimm mask) ((
Eop (
Oshift (
Slsl lsb2)) (
fld:::
Enil)):::
Enil))) ((
Eop (
Obfc lsb sz) (
prev:::
Enil)))
|
or_case18:
forall lsb sz prev mask lsb2 fld,
or_cases ((
Eop (
Obfc lsb sz) (
prev:::
Enil))) ((
Eop (
Oandimm mask) ((
Eop (
Oshift (
Slsl lsb2)) (
fld:::
Enil)):::
Enil)))
|
or_case19:
forall rest_lsb rest_sz fld lsb sz prev,
or_cases ((
Eop (
Obfc rest_lsb rest_sz) (
fld:::
Enil))) ((
Eop (
Obfc lsb sz) (
prev:::
Enil)))
|
or_default:
forall (
e1:
expr) (
e2:
expr),
or_cases e1 e2.
Definition or_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return or_cases zz1 zz2 with
|
Eop (
Ointconst n1)
Enil,
Eop (
Ointconst n2)
Enil =>
or_case1 n1 n2
|
Eop (
Ointconst n1)
Enil,
t2 =>
or_case2 n1 t2
|
t1,
Eop (
Ointconst n2)
Enil =>
or_case3 t1 n2
| (
Eop (
Oorshift (
Slsr s8)) ((
Eop (
Oorshift (
Slsl s24a)) ((
Eop (
Oshift (
Slsl s8a)) ((
Eop (
Oandimm c1) (
x1:::
Enil)):::
Enil)) ::: (
Eop (
Oandimm cFF) (
x2:::
Enil)) :::
Enil)) ::: (
Eop (
Oandimm c2) (
x3:::
Enil)) :::
Enil)), (
Eop (
Oshift (
Slsr s24b)) ((
Eop (
Oandimm cFF000000) (
x4:::
Enil)):::
Enil)) =>
or_case4 s8 s24a s8a c1 x1 cFF x2 c2 x3 s24b cFF000000 x4
|
Eop (
Oshift (
Slsl n1)) (
t1:::
Enil),
Eop (
Oshift (
Slsr n2)) (
t2:::
Enil) =>
or_case5 n1 t1 n2 t2
|
Eop (
Oshift (
Slsr n1)) (
t1:::
Enil),
Eop (
Oshift (
Slsl n2)) (
t2:::
Enil) =>
or_case6 n1 t1 n2 t2
|
Eop Oshru (
t1:::
n1:::
Enil),
Eop Oshl (
t2:::(
Eop (
Orsubimm c32) (
n2:::
Enil)):::
Enil) =>
or_case7 t1 n1 t2 c32 n2
|
Eop Oshl (
t1:::
n1:::
Enil),
Eop Oshru (
t2:::(
Eop (
Orsubimm c32) (
n2:::
Enil)):::
Enil) =>
or_case8 t1 n1 t2 c32 n2
| (
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Oubfx ulsb usz) (
fld:::
Enil)):::
Enil)), (
Eop (
Obfc lsb sz) (
prev:::
Enil)) =>
or_case9 lsb2 ulsb usz fld lsb sz prev
| (
Eop (
Obfc lsb sz) (
prev:::
Enil)), (
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Oubfx ulsb usz) (
fld:::
Enil)):::
Enil)) =>
or_case10 lsb sz prev lsb2 ulsb usz fld
| (
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Obfc cl_lsb cl_sz) (
fld:::
Enil)):::
Enil)), (
Eop (
Obfc lsb sz) (
prev:::
Enil)) =>
or_case11 lsb2 cl_lsb cl_sz fld lsb sz prev
| (
Eop (
Obfc lsb sz) (
prev:::
Enil)), (
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Obfc cl_lsb cl_sz) (
fld:::
Enil)):::
Enil)) =>
or_case12 lsb sz prev lsb2 cl_lsb cl_sz fld
| (
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Oandimm m) (
fld:::
Enil)):::
Enil)), (
Eop (
Obfc lsb sz) (
prev:::
Enil)) =>
or_case13 lsb2 m fld lsb sz prev
| (
Eop (
Obfc lsb sz) (
prev:::
Enil)), (
Eop (
Oshift (
Slsl lsb2)) ((
Eop (
Oandimm m) (
fld:::
Enil)):::
Enil)) =>
or_case14 lsb sz prev lsb2 m fld
|
Eop (
Oshift s) (
t1:::
Enil),
t2 =>
or_case15 s t1 t2
|
t1,
Eop (
Oshift s) (
t2:::
Enil) =>
or_case16 t1 s t2
| (
Eop (
Oandimm mask) ((
Eop (
Oshift (
Slsl lsb2)) (
fld:::
Enil)):::
Enil)), (
Eop (
Obfc lsb sz) (
prev:::
Enil)) =>
or_case17 mask lsb2 fld lsb sz prev
| (
Eop (
Obfc lsb sz) (
prev:::
Enil)), (
Eop (
Oandimm mask) ((
Eop (
Oshift (
Slsl lsb2)) (
fld:::
Enil)):::
Enil)) =>
or_case18 lsb sz prev mask lsb2 fld
| (
Eop (
Obfc rest_lsb rest_sz) (
fld:::
Enil)), (
Eop (
Obfc lsb sz) (
prev:::
Enil)) =>
or_case19 rest_lsb rest_sz fld lsb sz prev
|
e1,
e2 =>
or_default e1 e2
end.
Definition or (
e1:
expr) (
e2:
expr) :=
match or_match e1 e2 with
|
or_case1 n1 n2 =>
Eop (
Ointconst (
Int.or n1 n2))
Enil
|
or_case2 n1 t2 =>
orimm n1 t2
|
or_case3 t1 n2 =>
orimm n2 t1
|
or_case4 s8 s24a s8a c1 x1 cFF x2 c2 x3 s24b cFF000000 x4 =>
if Int.eq (
s_amount s8) (
Int.repr 8) &&
Int.eq (
s_amount s24a) (
Int.repr 24) &&
Int.eq (
s_amount s8a) (
Int.repr 8) &&
Int.eq (
s_amount s24b) (
Int.repr 24) &&
Int.eq c1 (
Int.repr 65280) &&
Int.eq c2 (
Int.repr 16711680) &&
Int.eq cFF (
Int.repr 255) &&
Int.eq cFF000000 (
Int.repr 4278190080) &&
same_expr_pure x1 x2 &&
same_expr_pure x2 x3 &&
same_expr_pure x3 x4 then Eop Obswap32 (
x1:::
Enil)
else Eop (
Oorshift (
Slsr s24b)) (
e1 ::: (
Eop (
Oandimm cFF000000) (
x4:::
Enil)) :::
Enil)
|
or_case5 n1 t1 n2 t2 =>
if Int.eq (
Int.add n1 n2)
Int.iwordsize &&
same_expr_pure t1 t2 then Eop (
Oshift (
Sror n2)) (
t1:::
Enil)
else Eop (
Oorshift (
Slsr n2)) (
e1:::
t2:::
Enil)
|
or_case6 n1 t1 n2 t2 =>
if Int.eq (
Int.add n2 n1)
Int.iwordsize &&
same_expr_pure t1 t2 then Eop (
Oshift (
Sror n1)) (
t1:::
Enil)
else Eop (
Oorshift (
Slsl n2)) (
e1:::
t2:::
Enil)
|
or_case7 t1 n1 t2 c32 n2 =>
if Int.eq c32 Int.iwordsize &&
same_expr_pure t1 t2 &&
same_expr_pure n1 n2 then Eop Oror (
t1:::
n1:::
Enil)
else Eop Oor (
e1:::
e2:::
Enil)
|
or_case8 t1 n1 t2 c32 n2 =>
if Int.eq c32 Int.iwordsize &&
same_expr_pure t1 t2 &&
same_expr_pure n1 n2 then Eop Oror (
t1:::(
Eop (
Orsubimm c32) (
n1:::
Enil)):::
Enil)
else Eop Oor (
e1:::
e2:::
Enil)
|
or_case9 lsb2 ulsb usz fld lsb sz prev =>
if and_dec (
and_dec (
Int.eq_dec ulsb Int.zero) (
Int.eq_dec lsb lsb2)) (
Int.eq_dec sz usz)
then Eop (
Obfi lsb sz) (
prev:::
fld:::
Enil)
else Eop Oor (
e1:::
e2:::
Enil)
|
or_case10 lsb sz prev lsb2 ulsb usz fld =>
if and_dec (
and_dec (
Int.eq_dec ulsb Int.zero) (
Int.eq_dec lsb lsb2)) (
Int.eq_dec sz usz)
then Eop (
Obfi lsb sz) (
prev:::
fld:::
Enil)
else Eop Oor (
e1:::
e2:::
Enil)
|
or_case11 lsb2 cl_lsb cl_sz fld lsb sz prev =>
if and_dec (
and_dec (
Int.eq_dec lsb lsb2) (
Int.eq_dec cl_lsb sz)) (
and_dec (
Int.eq_dec (
Int.add cl_lsb cl_sz) (
Int.repr 32)) (
zle (
Int.unsigned cl_lsb +
Int.unsigned cl_sz) 32))
then Eop (
Obfi lsb sz) (
prev:::
fld:::
Enil)
else Eop Oor (
e1:::
e2:::
Enil)
|
or_case12 lsb sz prev lsb2 cl_lsb cl_sz fld =>
if and_dec (
and_dec (
Int.eq_dec lsb lsb2) (
Int.eq_dec cl_lsb sz)) (
and_dec (
Int.eq_dec (
Int.add cl_lsb cl_sz) (
Int.repr 32)) (
zle (
Int.unsigned cl_lsb +
Int.unsigned cl_sz) 32))
then Eop (
Obfi lsb sz) (
prev:::
fld:::
Enil)
else Eop Oor (
e1:::
e2:::
Enil)
|
or_case13 lsb2 m fld lsb sz prev =>
if and_dec (
Int.eq_dec lsb lsb2) (
Int.eq_dec m (
Int.repr (
Z.ones (
Int.unsigned sz))))
then Eop (
Obfi lsb sz) (
prev:::
fld:::
Enil)
else Eop Oor (
e1:::
e2:::
Enil)
|
or_case14 lsb sz prev lsb2 m fld =>
if and_dec (
Int.eq_dec lsb lsb2) (
Int.eq_dec m (
Int.repr (
Z.ones (
Int.unsigned sz))))
then Eop (
Obfi lsb sz) (
prev:::
fld:::
Enil)
else Eop Oor (
e1:::
e2:::
Enil)
|
or_case15 s t1 t2 =>
Eop (
Oorshift s) (
t2:::
t1:::
Enil)
|
or_case16 t1 s t2 =>
Eop (
Oorshift s) (
t1:::
t2:::
Enil)
|
or_case17 mask lsb2 fld lsb sz prev =>
let mask' :=
Int.shl (
Int.repr (
Z.ones (
Int.unsigned sz)))
lsb in if and_dec (
Int.eq_dec lsb lsb2) (
Int.eq_dec mask' mask)
then Eop (
Obfi lsb sz) (
prev:::
fld:::
Enil)
else Eop Oor (
e1:::
e2:::
Enil)
|
or_case18 lsb sz prev mask lsb2 fld =>
let mask' :=
Int.shl (
Int.repr (
Z.ones (
Int.unsigned sz)))
lsb in if and_dec (
Int.eq_dec lsb lsb2) (
Int.eq_dec mask' mask)
then Eop (
Obfi lsb sz) (
prev:::
fld:::
Enil)
else Eop Oor (
e1:::
e2:::
Enil)
|
or_case19 rest_lsb rest_sz fld lsb sz prev =>
if and_dec (
and_dec (
Int.eq_dec lsb Int.zero) (
Int.eq_dec rest_lsb sz)) (
Int.eq_dec (
Int.add rest_lsb rest_sz) (
Int.repr 32))
then Eop (
Obfi Int.zero sz) (
prev:::
fld:::
Enil)
else Eop Oor (
e1:::
e2:::
Enil)
|
or_default e1 e2 =>
Eop Oor (
e1:::
e2:::
Enil)
end.
Original definition:
Nondetfunction xorimm (n1: int) (e2: expr) :=
if Int.eq n1 Int.zero then e2 else
if Int.eq n1 Int.mone then notint e2 else
match e2 with
| Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil
| Eop (Oxorimm n2) (t2:::Enil) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
| Eop Onot (t2:::Enil) => Eop (Oxorimm (Int.not n1)) (t2:::Enil)
| _ => Eop (Oxorimm n1) (e2:::Enil)
end.
:
forall (
e2:
expr),
Type :=
|
xorimm_case1:
forall n2,
xorimm_cases (
Eop (
Ointconst n2)
Enil)
|
xorimm_case2:
forall n2 t2,
xorimm_cases (
Eop (
Oxorimm n2) (
t2:::
Enil))
|
xorimm_case3:
forall t2,
xorimm_cases (
Eop Onot (
t2:::
Enil))
|
xorimm_default:
forall (
e2:
expr),
xorimm_cases e2.
Definition xorimm_match (
e2:
expr) :=
match e2 as zz1 return xorimm_cases zz1 with
|
Eop (
Ointconst n2)
Enil =>
xorimm_case1 n2
|
Eop (
Oxorimm n2) (
t2:::
Enil) =>
xorimm_case2 n2 t2
|
Eop Onot (
t2:::
Enil) =>
xorimm_case3 t2
|
e2 =>
xorimm_default e2
end.
Definition xorimm (
n1:
int) (
e2:
expr) :=
if Int.eq n1 Int.zero then e2 else if Int.eq n1 Int.mone then notint e2 else match xorimm_match e2 with
|
xorimm_case1 n2 =>
Eop (
Ointconst (
Int.xor n1 n2))
Enil
|
xorimm_case2 n2 t2 =>
Eop (
Oxorimm (
Int.xor n1 n2)) (
t2:::
Enil)
|
xorimm_case3 t2 =>
Eop (
Oxorimm (
Int.not n1)) (
t2:::
Enil)
|
xorimm_default e2 =>
Eop (
Oxorimm n1) (
e2:::
Enil)
end.
Original definition:
Nondetfunction xor (e1: expr) (e2: expr) :=
match e1, e2 with
| Eop (Ointconst n1) Enil, Eop (Ointconst n2) Enil =>
Eop (Ointconst (Int.xor n1 n2)) Enil
| Eop (Ointconst n1) Enil, t2 => xorimm n1 t2
| t1, Eop (Ointconst n2) Enil => xorimm n2 t1
| Eop (Oshift s) (t1:::Enil), t2 => Eop (Oxorshift s) (t2:::t1:::Enil)
| t1, Eop (Oshift s) (t2:::Enil) => Eop (Oxorshift s) (t1:::t2:::Enil)
| _, _ => Eop Oxor (e1:::e2:::Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
xor_case1:
forall n1 n2,
xor_cases (
Eop (
Ointconst n1)
Enil) (
Eop (
Ointconst n2)
Enil)
|
xor_case2:
forall n1 t2,
xor_cases (
Eop (
Ointconst n1)
Enil) (
t2)
|
xor_case3:
forall t1 n2,
xor_cases (
t1) (
Eop (
Ointconst n2)
Enil)
|
xor_case4:
forall s t1 t2,
xor_cases (
Eop (
Oshift s) (
t1:::
Enil)) (
t2)
|
xor_case5:
forall t1 s t2,
xor_cases (
t1) (
Eop (
Oshift s) (
t2:::
Enil))
|
xor_default:
forall (
e1:
expr) (
e2:
expr),
xor_cases e1 e2.
Definition xor_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return xor_cases zz1 zz2 with
|
Eop (
Ointconst n1)
Enil,
Eop (
Ointconst n2)
Enil =>
xor_case1 n1 n2
|
Eop (
Ointconst n1)
Enil,
t2 =>
xor_case2 n1 t2
|
t1,
Eop (
Ointconst n2)
Enil =>
xor_case3 t1 n2
|
Eop (
Oshift s) (
t1:::
Enil),
t2 =>
xor_case4 s t1 t2
|
t1,
Eop (
Oshift s) (
t2:::
Enil) =>
xor_case5 t1 s t2
|
e1,
e2 =>
xor_default e1 e2
end.
Definition xor (
e1:
expr) (
e2:
expr) :=
match xor_match e1 e2 with
|
xor_case1 n1 n2 =>
Eop (
Ointconst (
Int.xor n1 n2))
Enil
|
xor_case2 n1 t2 =>
xorimm n1 t2
|
xor_case3 t1 n2 =>
xorimm n2 t1
|
xor_case4 s t1 t2 =>
Eop (
Oxorshift s) (
t2:::
t1:::
Enil)
|
xor_case5 t1 s t2 =>
Eop (
Oxorshift s) (
t1:::
t2:::
Enil)
|
xor_default e1 e2 =>
Eop Oxor (
e1:::
e2:::
Enil)
end.
Integer division and modulus
Definition mod_aux (
divop:
operation) (
e1 e2:
expr) :=
Elet e1
(
Elet (
lift e2)
(
sub (
Eletvar 1)
(
Eop Omul (
Eop divop (
Eletvar 1 :::
Eletvar 0 :::
Enil) :::
Eletvar 0 :::
Enil)))).
Definition divs_base (
e1:
expr) (
e2:
expr) :=
Eop Odiv (
e1:::
e2:::
Enil).
Definition mods_base :=
mod_aux Odiv.
Definition divu_base (
e1:
expr) (
e2:
expr) :=
Eop Odivu (
e1:::
e2:::
Enil).
Definition modu_base :=
mod_aux Odivu.
Definition shrximm (
e1:
expr) (
n2:
int) :=
if Int.eq n2 Int.zero then e1 else Eop (
Oshrximm n2) (
e1:::
Enil).
General shifts
Original definition:
Nondetfunction shl (e1: expr) (e2: expr) :=
match e2 with
| Eop (Ointconst n2) Enil => shlimm e1 n2
| _ => Eop Oshl (e1:::e2:::Enil)
end.
:
forall (
e2:
expr),
Type :=
|
shl_case1:
forall n2,
shl_cases (
Eop (
Ointconst n2)
Enil)
|
shl_default:
forall (
e2:
expr),
shl_cases e2.
Definition shl_match (
e2:
expr) :=
match e2 as zz1 return shl_cases zz1 with
|
Eop (
Ointconst n2)
Enil =>
shl_case1 n2
|
e2 =>
shl_default e2
end.
Definition shl (
e1:
expr) (
e2:
expr) :=
match shl_match e2 with
|
shl_case1 n2 =>
shlimm e1 n2
|
shl_default e2 =>
Eop Oshl (
e1:::
e2:::
Enil)
end.
Original definition:
Nondetfunction shr (e1: expr) (e2: expr) :=
match e2 with
| Eop (Ointconst n2) Enil => shrimm e1 n2
| _ => Eop Oshr (e1:::e2:::Enil)
end.
:
forall (
e2:
expr),
Type :=
|
shr_case1:
forall n2,
shr_cases (
Eop (
Ointconst n2)
Enil)
|
shr_default:
forall (
e2:
expr),
shr_cases e2.
Definition shr_match (
e2:
expr) :=
match e2 as zz1 return shr_cases zz1 with
|
Eop (
Ointconst n2)
Enil =>
shr_case1 n2
|
e2 =>
shr_default e2
end.
Definition shr (
e1:
expr) (
e2:
expr) :=
match shr_match e2 with
|
shr_case1 n2 =>
shrimm e1 n2
|
shr_default e2 =>
Eop Oshr (
e1:::
e2:::
Enil)
end.
Original definition:
Nondetfunction shru (e1: expr) (e2: expr) :=
match e2 with
| Eop (Ointconst n2) Enil => shruimm e1 n2
| _ => Eop Oshru (e1:::e2:::Enil)
end.
:
forall (
e2:
expr),
Type :=
|
shru_case1:
forall n2,
shru_cases (
Eop (
Ointconst n2)
Enil)
|
shru_default:
forall (
e2:
expr),
shru_cases e2.
Definition shru_match (
e2:
expr) :=
match e2 as zz1 return shru_cases zz1 with
|
Eop (
Ointconst n2)
Enil =>
shru_case1 n2
|
e2 =>
shru_default e2
end.
Definition shru (
e1:
expr) (
e2:
expr) :=
match shru_match e2 with
|
shru_case1 n2 =>
shruimm e1 n2
|
shru_default e2 =>
Eop Oshru (
e1:::
e2:::
Enil)
end.
Floating-point arithmetic
Definition negf (
e:
expr) :=
Eop Onegf (
e :::
Enil).
Definition absf (
e:
expr) :=
Eop Oabsf (
e :::
Enil).
Original definition:
Nondetfunction addf (e1: expr) (e2: expr) :=
match e1, e2 with
| e1z, Eop Omulf (e2z ::: e3z ::: Enil) =>
Eop Omlaf (e1z ::: e2z ::: e3z ::: Enil)
| _, _ => Eop Oaddf (e1 ::: e2 ::: Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
addf_case1:
forall e1z e2z e3z,
addf_cases (
e1z) (
Eop Omulf (
e2z :::
e3z :::
Enil))
|
addf_default:
forall (
e1:
expr) (
e2:
expr),
addf_cases e1 e2.
Definition addf_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return addf_cases zz1 zz2 with
|
e1z,
Eop Omulf (
e2z :::
e3z :::
Enil) =>
addf_case1 e1z e2z e3z
|
e1,
e2 =>
addf_default e1 e2
end.
Definition addf (
e1:
expr) (
e2:
expr) :=
match addf_match e1 e2 with
|
addf_case1 e1z e2z e3z =>
Eop Omlaf (
e1z :::
e2z :::
e3z :::
Enil)
|
addf_default e1 e2 =>
Eop Oaddf (
e1 :::
e2 :::
Enil)
end.
Original definition:
Nondetfunction subf (e1: expr) (e2: expr) :=
match e1, e2 with
| e1z, Eop Omulf (e2z ::: e3z ::: Enil) =>
Eop Omlsf (e1z ::: e2z ::: e3z ::: Enil)
| _, _ => Eop Osubf (e1 ::: e2 ::: Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
subf_case1:
forall e1z e2z e3z,
subf_cases (
e1z) (
Eop Omulf (
e2z :::
e3z :::
Enil))
|
subf_default:
forall (
e1:
expr) (
e2:
expr),
subf_cases e1 e2.
Definition subf_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return subf_cases zz1 zz2 with
|
e1z,
Eop Omulf (
e2z :::
e3z :::
Enil) =>
subf_case1 e1z e2z e3z
|
e1,
e2 =>
subf_default e1 e2
end.
Definition subf (
e1:
expr) (
e2:
expr) :=
match subf_match e1 e2 with
|
subf_case1 e1z e2z e3z =>
Eop Omlsf (
e1z :::
e2z :::
e3z :::
Enil)
|
subf_default e1 e2 =>
Eop Osubf (
e1 :::
e2 :::
Enil)
end.
Definition mulf (
e1 e2:
expr) :=
Eop Omulf (
e1 :::
e2 :::
Enil).
Definition sqrtf (
e :
expr) :
option expr :=
Some (
Eop Osqrtf (
e :::
Enil)).
Definition bswap32 (
e :
expr) :
option expr :=
Some (
Eop Obswap32 (
e :::
Enil)).
Definition negfs (
e:
expr) :=
Eop Onegfs (
e :::
Enil).
Definition absfs (
e:
expr) :=
Eop Oabsfs (
e :::
Enil).
Definition sqrtfs (
e :
expr) :
option expr :=
Some (
Eop Osqrtfs (
e :::
Enil)).
Original definition:
Nondetfunction addfs (e1: expr) (e2: expr) :=
match e1, e2 with
| e1z, Eop Omulfs (e2z ::: e3z ::: Enil) =>
Eop Omlafs (e1z ::: e2z ::: e3z ::: Enil)
| _, _ => Eop Oaddfs (e1 ::: e2 ::: Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
addfs_case1:
forall e1z e2z e3z,
addfs_cases (
e1z) (
Eop Omulfs (
e2z :::
e3z :::
Enil))
|
addfs_default:
forall (
e1:
expr) (
e2:
expr),
addfs_cases e1 e2.
Definition addfs_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return addfs_cases zz1 zz2 with
|
e1z,
Eop Omulfs (
e2z :::
e3z :::
Enil) =>
addfs_case1 e1z e2z e3z
|
e1,
e2 =>
addfs_default e1 e2
end.
Definition addfs (
e1:
expr) (
e2:
expr) :=
match addfs_match e1 e2 with
|
addfs_case1 e1z e2z e3z =>
Eop Omlafs (
e1z :::
e2z :::
e3z :::
Enil)
|
addfs_default e1 e2 =>
Eop Oaddfs (
e1 :::
e2 :::
Enil)
end.
Original definition:
Nondetfunction subfs (e1: expr) (e2: expr) :=
match e1, e2 with
| e1z, Eop Omulfs (e2z ::: e3z ::: Enil) =>
Eop Omlsfs (e1z ::: e2z ::: e3z ::: Enil)
| _, _ => Eop Osubfs (e1 ::: e2 ::: Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
subfs_case1:
forall e1z e2z e3z,
subfs_cases (
e1z) (
Eop Omulfs (
e2z :::
e3z :::
Enil))
|
subfs_default:
forall (
e1:
expr) (
e2:
expr),
subfs_cases e1 e2.
Definition subfs_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return subfs_cases zz1 zz2 with
|
e1z,
Eop Omulfs (
e2z :::
e3z :::
Enil) =>
subfs_case1 e1z e2z e3z
|
e1,
e2 =>
subfs_default e1 e2
end.
Definition subfs (
e1:
expr) (
e2:
expr) :=
match subfs_match e1 e2 with
|
subfs_case1 e1z e2z e3z =>
Eop Omlsfs (
e1z :::
e2z :::
e3z :::
Enil)
|
subfs_default e1 e2 =>
Eop Osubfs (
e1 :::
e2 :::
Enil)
end.
Definition mulfs (
e1 e2:
expr) :=
Eop Omulfs (
e1 :::
e2 :::
Enil).
Comparisons
(t1 & m) != 0 with m a single bit at position k is just the
k-th bit of t1 zero-extended to a 0/1 value, i.e. Oubfx k 1.
Oubfx requires Thumb-2 (ARMv6T2 or ARMv7+); on earlier ARM models
we fall back to the Cmasknotzero m form (which lowers to
tst + Pmovite in the backend), as we also do when m is not a
single bit.
Definition andimm_ne_zero_to_bool (
m:
int) (
t1:
expr) :
expr :=
match Int.is_power2 m with
|
Some k =>
if Archi.thumb2_support &&
Compopts.bitfield_ops tt
then Eop (
Oubfx k Int.one) (
t1:::
Enil)
else Eop (
Ocmp (
Cmasknotzero m)) (
t1:::
Enil)
|
None =>
Eop (
Ocmp (
Cmasknotzero m)) (
t1:::
Enil)
end.
Original definition:
Nondetfunction compimm (default: comparison -> int -> condition)
(sem: comparison -> int -> int -> bool)
(c: comparison) (e1: expr) (n2: int) :=
match c, e1 with
| c, Eop (Ointconst n1) Enil =>
Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil
| Ceq, Eop (Ocmp c) el =>
if Int.eq_dec n2 Int.zero then
Eop (Ocmp (negate_condition c)) el
else if Int.eq_dec n2 Int.one then
Eop (Ocmp c) el
else
Eop (Ointconst Int.zero) Enil
| Cne, Eop (Ocmp c) el =>
if Int.eq_dec n2 Int.zero then
Eop (Ocmp c) el
else if Int.eq_dec n2 Int.one then
Eop (Ocmp (negate_condition c)) el
else
Eop (Ointconst Int.one) Enil
| Ceq, Eop (Oandimm m) (t1:::Enil) =>
if Int.eq n2 Int.zero
then Eop (Ocmp (Cmaskzero m)) (t1:::Enil)
else Eop (Ocmp (default c n2)) (e1 ::: Enil)
| Cne, Eop (Oandimm m) (t1:::Enil) =>
if Int.eq n2 Int.zero
then andimm_ne_zero_to_bool m t1
else Eop (Ocmp (default c n2)) (e1 ::: Enil)
| Ceq, Eop (Obfc lsb sz) (t1:::Enil) =>
if Int.eq n2 Int.zero
then Eop (Ocmp (Cmaskzero (Int.not (bitfield_mask lsb sz)))) (t1:::Enil)
else Eop (Ocmp (default c n2)) (e1 ::: Enil)
| Cne, Eop (Obfc lsb sz) (t1:::Enil) =>
if Int.eq n2 Int.zero
then Eop (Ocmp (Cmasknotzero (Int.not (bitfield_mask lsb sz)))) (t1:::Enil)
else Eop (Ocmp (default c n2)) (e1 ::: Enil)
| Ceq, Eop (Oubfx lsb sz) (t1:::Enil) =>
if Int.eq n2 Int.zero
then Eop (Ocmp (Cmaskzero (bitfield_mask lsb sz))) (t1:::Enil)
else Eop (Ocmp (default c n2)) (e1 ::: Enil)
| Cne, Eop (Oubfx lsb sz) (t1:::Enil) =>
if Int.eq n2 Int.zero
then Eop (Ocmp (Cmasknotzero (bitfield_mask lsb sz))) (t1:::Enil)
else Eop (Ocmp (default c n2)) (e1 ::: Enil)
| Ceq, Eop (Osbfx lsb sz) (t1:::Enil) =>
if Int.eq n2 Int.zero
then Eop (Ocmp (Cmaskzero (bitfield_mask lsb sz))) (t1:::Enil)
else Eop (Ocmp (default c n2)) (e1 ::: Enil)
| Cne, Eop (Osbfx lsb sz) (t1:::Enil) =>
if Int.eq n2 Int.zero
then Eop (Ocmp (Cmasknotzero (bitfield_mask lsb sz))) (t1:::Enil)
else Eop (Ocmp (default c n2)) (e1 ::: Enil)
| _, _ =>
Eop (Ocmp (default c n2)) (e1 ::: Enil)
end.
:
forall (
c:
comparison) (
e1:
expr) ,
Type :=
|
compimm_case1:
forall c n1,
compimm_cases (
c) (
Eop (
Ointconst n1)
Enil)
|
compimm_case2:
forall c el,
compimm_cases (
Ceq) (
Eop (
Ocmp c)
el)
|
compimm_case3:
forall c el,
compimm_cases (
Cne) (
Eop (
Ocmp c)
el)
|
compimm_case4:
forall m t1,
compimm_cases (
Ceq) (
Eop (
Oandimm m) (
t1:::
Enil))
|
compimm_case5:
forall m t1,
compimm_cases (
Cne) (
Eop (
Oandimm m) (
t1:::
Enil))
|
compimm_case6:
forall lsb sz t1,
compimm_cases (
Ceq) (
Eop (
Obfc lsb sz) (
t1:::
Enil))
|
compimm_case7:
forall lsb sz t1,
compimm_cases (
Cne) (
Eop (
Obfc lsb sz) (
t1:::
Enil))
|
compimm_case8:
forall lsb sz t1,
compimm_cases (
Ceq) (
Eop (
Oubfx lsb sz) (
t1:::
Enil))
|
compimm_case9:
forall lsb sz t1,
compimm_cases (
Cne) (
Eop (
Oubfx lsb sz) (
t1:::
Enil))
|
compimm_case10:
forall lsb sz t1,
compimm_cases (
Ceq) (
Eop (
Osbfx lsb sz) (
t1:::
Enil))
|
compimm_case11:
forall lsb sz t1,
compimm_cases (
Cne) (
Eop (
Osbfx lsb sz) (
t1:::
Enil))
|
compimm_default:
forall (
c:
comparison) (
e1:
expr) ,
compimm_cases c e1.
Definition compimm_match (
c:
comparison) (
e1:
expr) :=
match c as zz1,
e1 as zz2 return compimm_cases zz1 zz2 with
|
c,
Eop (
Ointconst n1)
Enil =>
compimm_case1 c n1
|
Ceq,
Eop (
Ocmp c)
el =>
compimm_case2 c el
|
Cne,
Eop (
Ocmp c)
el =>
compimm_case3 c el
|
Ceq,
Eop (
Oandimm m) (
t1:::
Enil) =>
compimm_case4 m t1
|
Cne,
Eop (
Oandimm m) (
t1:::
Enil) =>
compimm_case5 m t1
|
Ceq,
Eop (
Obfc lsb sz) (
t1:::
Enil) =>
compimm_case6 lsb sz t1
|
Cne,
Eop (
Obfc lsb sz) (
t1:::
Enil) =>
compimm_case7 lsb sz t1
|
Ceq,
Eop (
Oubfx lsb sz) (
t1:::
Enil) =>
compimm_case8 lsb sz t1
|
Cne,
Eop (
Oubfx lsb sz) (
t1:::
Enil) =>
compimm_case9 lsb sz t1
|
Ceq,
Eop (
Osbfx lsb sz) (
t1:::
Enil) =>
compimm_case10 lsb sz t1
|
Cne,
Eop (
Osbfx lsb sz) (
t1:::
Enil) =>
compimm_case11 lsb sz t1
|
c,
e1 =>
compimm_default c e1
end.
Definition compimm (
default:
comparison ->
int ->
condition) (
sem:
comparison ->
int ->
int ->
bool) (
c:
comparison) (
e1:
expr) (
n2:
int) :=
match compimm_match c e1 with
|
compimm_case1 c n1 =>
Eop (
Ointconst (
if sem c n1 n2 then Int.one else Int.zero))
Enil
|
compimm_case2 c el =>
if Int.eq_dec n2 Int.zero then Eop (
Ocmp (
negate_condition c))
el else if Int.eq_dec n2 Int.one then Eop (
Ocmp c)
el else Eop (
Ointconst Int.zero)
Enil
|
compimm_case3 c el =>
if Int.eq_dec n2 Int.zero then Eop (
Ocmp c)
el else if Int.eq_dec n2 Int.one then Eop (
Ocmp (
negate_condition c))
el else Eop (
Ointconst Int.one)
Enil
|
compimm_case4 m t1 =>
if Int.eq n2 Int.zero then Eop (
Ocmp (
Cmaskzero m)) (
t1:::
Enil)
else Eop (
Ocmp (
default c n2)) (
e1 :::
Enil)
|
compimm_case5 m t1 =>
if Int.eq n2 Int.zero then andimm_ne_zero_to_bool m t1 else Eop (
Ocmp (
default c n2)) (
e1 :::
Enil)
|
compimm_case6 lsb sz t1 =>
if Int.eq n2 Int.zero then Eop (
Ocmp (
Cmaskzero (
Int.not (
bitfield_mask lsb sz)))) (
t1:::
Enil)
else Eop (
Ocmp (
default c n2)) (
e1 :::
Enil)
|
compimm_case7 lsb sz t1 =>
if Int.eq n2 Int.zero then Eop (
Ocmp (
Cmasknotzero (
Int.not (
bitfield_mask lsb sz)))) (
t1:::
Enil)
else Eop (
Ocmp (
default c n2)) (
e1 :::
Enil)
|
compimm_case8 lsb sz t1 =>
if Int.eq n2 Int.zero then Eop (
Ocmp (
Cmaskzero (
bitfield_mask lsb sz))) (
t1:::
Enil)
else Eop (
Ocmp (
default c n2)) (
e1 :::
Enil)
|
compimm_case9 lsb sz t1 =>
if Int.eq n2 Int.zero then Eop (
Ocmp (
Cmasknotzero (
bitfield_mask lsb sz))) (
t1:::
Enil)
else Eop (
Ocmp (
default c n2)) (
e1 :::
Enil)
|
compimm_case10 lsb sz t1 =>
if Int.eq n2 Int.zero then Eop (
Ocmp (
Cmaskzero (
bitfield_mask lsb sz))) (
t1:::
Enil)
else Eop (
Ocmp (
default c n2)) (
e1 :::
Enil)
|
compimm_case11 lsb sz t1 =>
if Int.eq n2 Int.zero then Eop (
Ocmp (
Cmasknotzero (
bitfield_mask lsb sz))) (
t1:::
Enil)
else Eop (
Ocmp (
default c n2)) (
e1 :::
Enil)
|
compimm_default c e1 =>
Eop (
Ocmp (
default c n2)) (
e1 :::
Enil)
end.
Original definition:
Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
match e1, e2 with
| Eop (Ointconst n1) Enil, t2 =>
compimm Ccompimm Int.cmp (swap_comparison c) t2 n1
| t1, Eop (Ointconst n2) Enil =>
compimm Ccompimm Int.cmp c t1 n2
| t1, Eop (Oshift s) (t2:::Enil) =>
Eop (Ocmp (Ccompshift c s)) (t1 ::: t2 ::: Enil)
| Eop (Oshift s) (t1:::Enil), t2 =>
Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2 ::: t1 ::: Enil)
| _, _ =>
Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
comp_case1:
forall n1 t2,
comp_cases (
Eop (
Ointconst n1)
Enil) (
t2)
|
comp_case2:
forall t1 n2,
comp_cases (
t1) (
Eop (
Ointconst n2)
Enil)
|
comp_case3:
forall t1 s t2,
comp_cases (
t1) (
Eop (
Oshift s) (
t2:::
Enil))
|
comp_case4:
forall s t1 t2,
comp_cases (
Eop (
Oshift s) (
t1:::
Enil)) (
t2)
|
comp_default:
forall (
e1:
expr) (
e2:
expr),
comp_cases e1 e2.
Definition comp_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return comp_cases zz1 zz2 with
|
Eop (
Ointconst n1)
Enil,
t2 =>
comp_case1 n1 t2
|
t1,
Eop (
Ointconst n2)
Enil =>
comp_case2 t1 n2
|
t1,
Eop (
Oshift s) (
t2:::
Enil) =>
comp_case3 t1 s t2
|
Eop (
Oshift s) (
t1:::
Enil),
t2 =>
comp_case4 s t1 t2
|
e1,
e2 =>
comp_default e1 e2
end.
Definition comp (
c:
comparison) (
e1:
expr) (
e2:
expr) :=
match comp_match e1 e2 with
|
comp_case1 n1 t2 =>
compimm Ccompimm Int.cmp (
swap_comparison c)
t2 n1
|
comp_case2 t1 n2 =>
compimm Ccompimm Int.cmp c t1 n2
|
comp_case3 t1 s t2 =>
Eop (
Ocmp (
Ccompshift c s)) (
t1 :::
t2 :::
Enil)
|
comp_case4 s t1 t2 =>
Eop (
Ocmp (
Ccompshift (
swap_comparison c)
s)) (
t2 :::
t1 :::
Enil)
|
comp_default e1 e2 =>
Eop (
Ocmp (
Ccomp c)) (
e1 :::
e2 :::
Enil)
end.
Original definition:
Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) :=
match e1, e2 with
| Eop (Ointconst n1) Enil, t2 =>
compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1
| t1, Eop (Ointconst n2) Enil =>
compimm Ccompuimm Int.cmpu c t1 n2
| t1, Eop (Oshift s) (t2:::Enil) =>
Eop (Ocmp (Ccompushift c s)) (t1 ::: t2 ::: Enil)
| Eop (Oshift s) (t1:::Enil), t2 =>
Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2 ::: t1 ::: Enil)
| _, _ =>
Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil)
end.
:
forall (
e1:
expr) (
e2:
expr),
Type :=
|
compu_case1:
forall n1 t2,
compu_cases (
Eop (
Ointconst n1)
Enil) (
t2)
|
compu_case2:
forall t1 n2,
compu_cases (
t1) (
Eop (
Ointconst n2)
Enil)
|
compu_case3:
forall t1 s t2,
compu_cases (
t1) (
Eop (
Oshift s) (
t2:::
Enil))
|
compu_case4:
forall s t1 t2,
compu_cases (
Eop (
Oshift s) (
t1:::
Enil)) (
t2)
|
compu_default:
forall (
e1:
expr) (
e2:
expr),
compu_cases e1 e2.
Definition compu_match (
e1:
expr) (
e2:
expr) :=
match e1 as zz1,
e2 as zz2 return compu_cases zz1 zz2 with
|
Eop (
Ointconst n1)
Enil,
t2 =>
compu_case1 n1 t2
|
t1,
Eop (
Ointconst n2)
Enil =>
compu_case2 t1 n2
|
t1,
Eop (
Oshift s) (
t2:::
Enil) =>
compu_case3 t1 s t2
|
Eop (
Oshift s) (
t1:::
Enil),
t2 =>
compu_case4 s t1 t2
|
e1,
e2 =>
compu_default e1 e2
end.
Definition compu (
c:
comparison) (
e1:
expr) (
e2:
expr) :=
match compu_match e1 e2 with
|
compu_case1 n1 t2 =>
compimm Ccompuimm Int.cmpu (
swap_comparison c)
t2 n1
|
compu_case2 t1 n2 =>
compimm Ccompuimm Int.cmpu c t1 n2
|
compu_case3 t1 s t2 =>
Eop (
Ocmp (
Ccompushift c s)) (
t1 :::
t2 :::
Enil)
|
compu_case4 s t1 t2 =>
Eop (
Ocmp (
Ccompushift (
swap_comparison c)
s)) (
t2 :::
t1 :::
Enil)
|
compu_default e1 e2 =>
Eop (
Ocmp (
Ccompu c)) (
e1 :::
e2 :::
Enil)
end.
Definition compf (
c:
comparison) (
e1:
expr) (
e2:
expr) :=
Eop (
Ocmp (
Ccompf c)) (
e1:::
e2:::
Enil).
Definition compfs (
c:
comparison) (
e1:
expr) (
e2:
expr) :=
Eop (
Ocmp (
Ccompfs c)) (
e1 :::
e2 :::
Enil).
Selection
Definition select_supported (
ty:
typ) :=
match ty with
|
Tint |
Tfloat |
Tsingle =>
true
| _ =>
false
end.
Definition selectimm (
cond:
condition) (
args:
exprlist) (
e1:
expr) (
imm:
int) :=
if is_immed_arith CONST imm then Eop (
Oselimm cond imm) (
e1 :::
args)
else Eop (
Osel cond) (
e1 :::
Eop (
Ointconst imm)
Enil :::
args).
Definition selimmn (
cond:
condition) (
args:
exprlist) (
imm:
int) (
e2:
expr) :=
if is_immed_arith CONST imm
then Eop (
Oselimm (
negate_condition cond)
imm) (
e2 :::
args)
else Eop (
Osel cond) (
Eop (
Ointconst imm)
Enil :::
e2 :::
args).
Definition selectimm2 (
cond:
condition) (
args:
exprlist) (
imm1 imm2:
int) :=
if Int.eq imm1 Int.one &&
Int.eq imm2 Int.zero then
Eop (
Ocmp cond)
args
else if Int.eq imm1 Int.zero &&
Int.eq imm2 Int.one then
Eop (
Ocmp (
negate_condition cond))
args
else if is_immed_arith CONST imm1 &&
is_immed_arith CONST imm2
then Eop (
Oselimm2 cond imm1 imm2)
args
else if is_immed_arith CONST imm2
then selectimm cond args (
Eop (
Ointconst imm1)
Enil)
imm2
else selimmn cond args imm1 (
Eop (
Ointconst imm2)
Enil).
Definition select (
ty:
typ) (
cond:
condition) (
args:
exprlist) (
e1 e2:
expr) :=
match ty,
e1,
e2 with
|
Tint,
Eop (
Ointconst imm1)
Enil,
Eop (
Ointconst imm2)
Enil =>
selectimm2 cond args imm1 imm2
|
Tint, _,
Eop (
Ointconst imm)
Enil =>
selectimm cond args e1 imm
|
Tint,
Eop (
Ointconst imm)
Enil, _ =>
selimmn cond args imm e2
| _, _, _ =>
Eop (
Osel cond) (
e1 :::
e2 :::
args)
end.
Integer conversions
Original definition:
Nondetfunction cast8unsigned (e: expr) :=
match e with
| Eop (Ocmp c) el => e
| Eload Mint8unsigned addr args => e
| _ => andimm (Int.repr 255) e
end.
:
forall (
e:
expr),
Type :=
|
cast8unsigned_case1:
forall c el,
cast8unsigned_cases (
Eop (
Ocmp c)
el)
|
cast8unsigned_case2:
forall addr args,
cast8unsigned_cases (
Eload Mint8unsigned addr args)
|
cast8unsigned_default:
forall (
e:
expr),
cast8unsigned_cases e.
Definition cast8unsigned_match (
e:
expr) :=
match e as zz1 return cast8unsigned_cases zz1 with
|
Eop (
Ocmp c)
el =>
cast8unsigned_case1 c el
|
Eload Mint8unsigned addr args =>
cast8unsigned_case2 addr args
|
e =>
cast8unsigned_default e
end.
Definition cast8unsigned (
e:
expr) :=
match cast8unsigned_match e with
|
cast8unsigned_case1 c el =>
e
|
cast8unsigned_case2 addr args =>
e
|
cast8unsigned_default e =>
andimm (
Int.repr 255)
e
end.
Original definition:
Nondetfunction cast8signed (e: expr) :=
match e with
| Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 8 n)) Enil
| _ => Eop Ocast8signed (e ::: Enil)
end.
:
forall (
e:
expr),
Type :=
|
cast8signed_case1:
forall n,
cast8signed_cases (
Eop (
Ointconst n)
Enil)
|
cast8signed_default:
forall (
e:
expr),
cast8signed_cases e.
Definition cast8signed_match (
e:
expr) :=
match e as zz1 return cast8signed_cases zz1 with
|
Eop (
Ointconst n)
Enil =>
cast8signed_case1 n
|
e =>
cast8signed_default e
end.
Definition cast8signed (
e:
expr) :=
match cast8signed_match e with
|
cast8signed_case1 n =>
Eop (
Ointconst (
Int.sign_ext 8
n))
Enil
|
cast8signed_default e =>
Eop Ocast8signed (
e :::
Enil)
end.
Original definition:
Nondetfunction cast16unsigned (e: expr) :=
match e with
| Eop (Ocmp c) el => e
| Eload Mint16unsigned addr args => e
| _ => andimm (Int.repr 65535) e
end.
:
forall (
e:
expr),
Type :=
|
cast16unsigned_case1:
forall c el,
cast16unsigned_cases (
Eop (
Ocmp c)
el)
|
cast16unsigned_case2:
forall addr args,
cast16unsigned_cases (
Eload Mint16unsigned addr args)
|
cast16unsigned_default:
forall (
e:
expr),
cast16unsigned_cases e.
Definition cast16unsigned_match (
e:
expr) :=
match e as zz1 return cast16unsigned_cases zz1 with
|
Eop (
Ocmp c)
el =>
cast16unsigned_case1 c el
|
Eload Mint16unsigned addr args =>
cast16unsigned_case2 addr args
|
e =>
cast16unsigned_default e
end.
Definition cast16unsigned (
e:
expr) :=
match cast16unsigned_match e with
|
cast16unsigned_case1 c el =>
e
|
cast16unsigned_case2 addr args =>
e
|
cast16unsigned_default e =>
andimm (
Int.repr 65535)
e
end.
Original definition:
Nondetfunction cast16signed (e: expr) :=
match e with
| Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 16 n)) Enil
| _ => Eop Ocast16signed (e ::: Enil)
end.
:
forall (
e:
expr),
Type :=
|
cast16signed_case1:
forall n,
cast16signed_cases (
Eop (
Ointconst n)
Enil)
|
cast16signed_default:
forall (
e:
expr),
cast16signed_cases e.
Definition cast16signed_match (
e:
expr) :=
match e as zz1 return cast16signed_cases zz1 with
|
Eop (
Ointconst n)
Enil =>
cast16signed_case1 n
|
e =>
cast16signed_default e
end.
Definition cast16signed (
e:
expr) :=
match cast16signed_match e with
|
cast16signed_case1 n =>
Eop (
Ointconst (
Int.sign_ext 16
n))
Enil
|
cast16signed_default e =>
Eop Ocast16signed (
e :::
Enil)
end.
Floating-point conversions
Definition singleoffloat (
e:
expr) :=
Eop Osingleoffloat (
e :::
Enil).
Definition floatofsingle (
e:
expr) :=
Eop Ofloatofsingle (
e :::
Enil).
Definition intoffloat (
e:
expr) :=
Eop Ointoffloat (
e :::
Enil).
Definition intuoffloat (
e:
expr) :=
Eop Ointuoffloat (
e :::
Enil).
Original definition:
Nondetfunction floatofint (e: expr) :=
match e with
| Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil
| _ => Eop Ofloatofint (e ::: Enil)
end.
:
forall (
e:
expr),
Type :=
|
floatofint_case1:
forall n,
floatofint_cases (
Eop (
Ointconst n)
Enil)
|
floatofint_default:
forall (
e:
expr),
floatofint_cases e.
Definition floatofint_match (
e:
expr) :=
match e as zz1 return floatofint_cases zz1 with
|
Eop (
Ointconst n)
Enil =>
floatofint_case1 n
|
e =>
floatofint_default e
end.
Definition floatofint (
e:
expr) :=
match floatofint_match e with
|
floatofint_case1 n =>
Eop (
Ofloatconst (
Float.of_int n))
Enil
|
floatofint_default e =>
Eop Ofloatofint (
e :::
Enil)
end.
Original definition:
Nondetfunction floatofintu (e: expr) :=
match e with
| Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil
| _ => Eop Ofloatofintu (e ::: Enil)
end.
:
forall (
e:
expr),
Type :=
|
floatofintu_case1:
forall n,
floatofintu_cases (
Eop (
Ointconst n)
Enil)
|
floatofintu_default:
forall (
e:
expr),
floatofintu_cases e.
Definition floatofintu_match (
e:
expr) :=
match e as zz1 return floatofintu_cases zz1 with
|
Eop (
Ointconst n)
Enil =>
floatofintu_case1 n
|
e =>
floatofintu_default e
end.
Definition floatofintu (
e:
expr) :=
match floatofintu_match e with
|
floatofintu_case1 n =>
Eop (
Ofloatconst (
Float.of_intu n))
Enil
|
floatofintu_default e =>
Eop Ofloatofintu (
e :::
Enil)
end.
Definition intofsingle (
e:
expr) :=
Eop Ointofsingle (
e :::
Enil).
Definition intuofsingle (
e:
expr) :=
Eop Ointuofsingle (
e :::
Enil).
Original definition:
Nondetfunction singleofint (e: expr) :=
match e with
| Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_int n)) Enil
| _ => Eop Osingleofint (e ::: Enil)
end.
:
forall (
e:
expr),
Type :=
|
singleofint_case1:
forall n,
singleofint_cases (
Eop (
Ointconst n)
Enil)
|
singleofint_default:
forall (
e:
expr),
singleofint_cases e.
Definition singleofint_match (
e:
expr) :=
match e as zz1 return singleofint_cases zz1 with
|
Eop (
Ointconst n)
Enil =>
singleofint_case1 n
|
e =>
singleofint_default e
end.
Definition singleofint (
e:
expr) :=
match singleofint_match e with
|
singleofint_case1 n =>
Eop (
Osingleconst (
Float32.of_int n))
Enil
|
singleofint_default e =>
Eop Osingleofint (
e :::
Enil)
end.
Original definition:
Nondetfunction singleofintu (e: expr) :=
match e with
| Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_intu n)) Enil
| _ => Eop Osingleofintu (e ::: Enil)
end.
:
forall (
e:
expr),
Type :=
|
singleofintu_case1:
forall n,
singleofintu_cases (
Eop (
Ointconst n)
Enil)
|
singleofintu_default:
forall (
e:
expr),
singleofintu_cases e.
Definition singleofintu_match (
e:
expr) :=
match e as zz1 return singleofintu_cases zz1 with
|
Eop (
Ointconst n)
Enil =>
singleofintu_case1 n
|
e =>
singleofintu_default e
end.
Definition singleofintu (
e:
expr) :=
match singleofintu_match e with
|
singleofintu_case1 n =>
Eop (
Osingleconst (
Float32.of_intu n))
Enil
|
singleofintu_default e =>
Eop Osingleofintu (
e :::
Enil)
end.
Recognition of addressing modes for load and store operations
We do not recognize the Aindexed2 and Aindexed2shift modes
for floating-point accesses, since these are not supported
by the hardware and emulated inefficiently in Asmgen.
For Aindexed2shift, in classic ARM (A32) only LDR(B)/STR(B)
accept a shifted register operand; halfword and signed-byte loads
do not. In Thumb2 (T2 encoding), LDRB/LDRSB/LDRH/LDRSH/STRB/STRH
(register) all accept an LSL #0..3 index.
Definition can_use_Aindexed2 (
chunk:
memory_chunk):
bool :=
match chunk with
|
Mbool =>
true
|
Mint8signed =>
true
|
Mint8unsigned =>
true
|
Mint16signed =>
true
|
Mint16unsigned =>
true
|
Mint32 |
Mint32al1 =>
true
|
Mint64 |
Mint64al1 =>
false
|
Mfloat32 =>
false
|
Mfloat64 =>
false
|
Many32 =>
true
|
Many64 =>
false
end.
Definition can_use_Aindexed2shift (
chunk:
memory_chunk) (
s:
shift):
bool :=
match chunk with
|
Mbool =>
false
|
Mint8signed =>
thumb tt
|
Mint8unsigned =>
true
|
Mint16signed =>
thumb tt
|
Mint16unsigned =>
thumb tt
|
Mint32 |
Mint32al1 =>
true
|
Mint64 |
Mint64al1 =>
false
|
Mfloat32 =>
false
|
Mfloat64 =>
false
|
Many32 =>
true
|
Many64 =>
false
end &&
(
if thumb tt then
match s with
|
Slsl s =>
Int.ltu s (
Int.repr 4)
| _ =>
false
end
else true).
Original definition:
Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
match e with
| Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
| Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil)
| Eop (Oaddshift s) (e1:::e2:::Enil) =>
if can_use_Aindexed2shift chunk s
then (Aindexed2shift s, e1:::e2:::Enil)
else (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil)
| Eop Oadd (e1:::e2:::Enil) =>
if can_use_Aindexed2 chunk
then (Aindexed2, e1:::e2:::Enil)
else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil)
| _ => (Aindexed Int.zero, e:::Enil)
end.
:
forall (
e:
expr),
Type :=
|
addressing_case1:
forall n,
addressing_cases (
Eop (
Oaddrstack n)
Enil)
|
addressing_case2:
forall n e1,
addressing_cases (
Eop (
Oaddimm n) (
e1:::
Enil))
|
addressing_case3:
forall s e1 e2,
addressing_cases (
Eop (
Oaddshift s) (
e1:::
e2:::
Enil))
|
addressing_case4:
forall e1 e2,
addressing_cases (
Eop Oadd (
e1:::
e2:::
Enil))
|
addressing_default:
forall (
e:
expr),
addressing_cases e.
Definition addressing_match (
e:
expr) :=
match e as zz1 return addressing_cases zz1 with
|
Eop (
Oaddrstack n)
Enil =>
addressing_case1 n
|
Eop (
Oaddimm n) (
e1:::
Enil) =>
addressing_case2 n e1
|
Eop (
Oaddshift s) (
e1:::
e2:::
Enil) =>
addressing_case3 s e1 e2
|
Eop Oadd (
e1:::
e2:::
Enil) =>
addressing_case4 e1 e2
|
e =>
addressing_default e
end.
Definition addressing (
chunk:
memory_chunk) (
e:
expr) :=
match addressing_match e with
|
addressing_case1 n =>
(
Ainstack n,
Enil)
|
addressing_case2 n e1 =>
(
Aindexed n,
e1:::
Enil)
|
addressing_case3 s e1 e2 =>
if can_use_Aindexed2shift chunk s then (
Aindexed2shift s,
e1:::
e2:::
Enil)
else (
Aindexed Int.zero,
Eop (
Oaddshift s) (
e1:::
e2:::
Enil) :::
Enil)
|
addressing_case4 e1 e2 =>
if can_use_Aindexed2 chunk then (
Aindexed2,
e1:::
e2:::
Enil)
else (
Aindexed Int.zero,
Eop Oadd (
e1:::
e2:::
Enil) :::
Enil)
|
addressing_default e =>
(
Aindexed Int.zero,
e:::
Enil)
end.
Arguments of builtins
Original definition:
Nondetfunction builtin_arg (e: expr) :=
match e with
| Eop (Ointconst n) Enil => BA_int n
| Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs
| Eop (Oaddrstack ofs) Enil => BA_addrstack ofs
| Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
BA_long (Int64.ofwords h l)
| Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
| Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
| Eload chunk (Aindexed ofs1) (Eop (Oaddrsymbol id ofs) Enil ::: Enil) =>
BA_loadglobal chunk id (Ptrofs.add ofs (Ptrofs.of_int ofs1))
| Eop (Oaddimm n) (e1:::Enil) => BA_addptr (BA e1) (BA_int n)
| _ => BA e
end.
:
forall (
e:
expr),
Type :=
|
builtin_arg_case1:
forall n,
builtin_arg_cases (
Eop (
Ointconst n)
Enil)
|
builtin_arg_case2:
forall id ofs,
builtin_arg_cases (
Eop (
Oaddrsymbol id ofs)
Enil)
|
builtin_arg_case3:
forall ofs,
builtin_arg_cases (
Eop (
Oaddrstack ofs)
Enil)
|
builtin_arg_case4:
forall h l,
builtin_arg_cases (
Eop Omakelong (
Eop (
Ointconst h)
Enil :::
Eop (
Ointconst l)
Enil :::
Enil))
|
builtin_arg_case5:
forall h l,
builtin_arg_cases (
Eop Omakelong (
h :::
l :::
Enil))
|
builtin_arg_case6:
forall chunk ofs,
builtin_arg_cases (
Eload chunk (
Ainstack ofs)
Enil)
|
builtin_arg_case7:
forall chunk ofs1 id ofs,
builtin_arg_cases (
Eload chunk (
Aindexed ofs1) (
Eop (
Oaddrsymbol id ofs)
Enil :::
Enil))
|
builtin_arg_case8:
forall n e1,
builtin_arg_cases (
Eop (
Oaddimm n) (
e1:::
Enil))
|
builtin_arg_default:
forall (
e:
expr),
builtin_arg_cases e.
Definition builtin_arg_match (
e:
expr) :=
match e as zz1 return builtin_arg_cases zz1 with
|
Eop (
Ointconst n)
Enil =>
builtin_arg_case1 n
|
Eop (
Oaddrsymbol id ofs)
Enil =>
builtin_arg_case2 id ofs
|
Eop (
Oaddrstack ofs)
Enil =>
builtin_arg_case3 ofs
|
Eop Omakelong (
Eop (
Ointconst h)
Enil :::
Eop (
Ointconst l)
Enil :::
Enil) =>
builtin_arg_case4 h l
|
Eop Omakelong (
h :::
l :::
Enil) =>
builtin_arg_case5 h l
|
Eload chunk (
Ainstack ofs)
Enil =>
builtin_arg_case6 chunk ofs
|
Eload chunk (
Aindexed ofs1) (
Eop (
Oaddrsymbol id ofs)
Enil :::
Enil) =>
builtin_arg_case7 chunk ofs1 id ofs
|
Eop (
Oaddimm n) (
e1:::
Enil) =>
builtin_arg_case8 n e1
|
e =>
builtin_arg_default e
end.
Definition builtin_arg (
e:
expr) :=
match builtin_arg_match e with
|
builtin_arg_case1 n =>
BA_int n
|
builtin_arg_case2 id ofs =>
BA_addrglobal id ofs
|
builtin_arg_case3 ofs =>
BA_addrstack ofs
|
builtin_arg_case4 h l =>
BA_long (
Int64.ofwords h l)
|
builtin_arg_case5 h l =>
BA_splitlong (
BA h) (
BA l)
|
builtin_arg_case6 chunk ofs =>
BA_loadstack chunk ofs
|
builtin_arg_case7 chunk ofs1 id ofs =>
BA_loadglobal chunk id (
Ptrofs.add ofs (
Ptrofs.of_int ofs1))
|
builtin_arg_case8 n e1 =>
BA_addptr (
BA e1) (
BA_int n)
|
builtin_arg_default e =>
BA e
end.
Definition divf_base (
e1:
expr) (
e2:
expr) :=
Eop Odivf (
e1 :::
e2 :::
Enil).
Definition divfs_base (
e1:
expr) (
e2:
expr) :=
Eop Odivfs (
e1 :::
e2 :::
Enil).
Definition fast_isfinitef (
e:
expr) :=
let mask :=
Int.repr ExtFloats.isfinitef2_mask in
if Archi.thumb2_support &&
Compopts.optim_fast_isfinite_int tt
then
Some (
Eop (
Ocmp (
Ccompimm Cne mask))
((
Eop (
Oubfx (
Int.repr 23) (
Int.repr 8))
((
Eop Obits_of_single (
e :::
Enil)) :::
Enil)) :::
Enil))
else None.
Definition fast_isfinite (
e:
expr) :=
let mask :=
Int.repr ExtFloats.isfinite_mask in
if Archi.thumb2_support &&
Compopts.optim_fast_isfinite_int tt
then Some (
Eop (
Ocmp (
Ccompimm Cne mask))
((
Eop (
Oubfx (
Int.repr 20) (
Int.repr 11))
((
Eop Ohibits_of_float (
e :::
Enil)) :::
Enil)) :::
Enil))
else None.
Platform-specific known builtins
Definition platform_builtin (
b:
platform_builtin) (
args:
exprlist) :
option expr :=
match b with
|
BI_bits_of_float =>
Some (
Eop Obits_of_single args)
|
BI_float_of_bits =>
Some (
Eop Osingle_of_bits args)
|
BI_clz =>
Some (
Eop Oclz args)
|
BI_ctz =>
Some (
Eop Oclz (
Eop Oreverse_bits args :::
Enil))
|
BI_reverse_bits =>
Some (
Eop Oreverse_bits args)
end.