diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-26 20:37:16 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-26 20:37:16 +0100 |
| commit | 45cab18f8f9fc1db4f9877333c09d5a5cb2dc64d (patch) | |
| tree | de0352098747757395dc25e14e524a57b93ebb88 /mppa_k1c/SelectOp.vp | |
| parent | 3ff674c7c3ad5237fa4223596563c2b6e09cd8cf (diff) | |
| download | compcert-kvx-45cab18f8f9fc1db4f9877333c09d5a5cb2dc64d.tar.gz compcert-kvx-45cab18f8f9fc1db4f9877333c09d5a5cb2dc64d.zip | |
rm cruft
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 2ad264c9..d01b7616 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -61,30 +61,6 @@ Section SELECT. Context {hf: helper_functions}. -(** Stuff for select *) -Definition is_zero (vt : expr) : expr := - Eop (Ocmp (Ccomp Ceq)) - (vt:::(Eop (Ointconst Int.zero) Enil):::Enil). - -Definition is_nonzero (vt : expr) : expr := - Eop (Ocmp (Ccomp Cne)) - (vt:::(Eop (Ointconst Int.zero) Enil):::Enil). - -Definition bool_to_bitmask (et : expr) : expr := - Eop Oneg (et:::Enil). - -Definition not_bool_to_bitmask (et : expr) : expr := - Eop Osub (et:::(Eop (Ointconst Int.one) Enil):::Enil). - -Definition ternary_expand (e0 e1 et : expr) : expr := - Eop Oor - ((Eop Oand ((not_bool_to_bitmask et):::e1:::Enil))::: - (Eop Oand ((bool_to_bitmask et):::e0:::Enil))::: - Enil). - -Definition select_or_expand (e0 e1 et: expr) : expr := - ternary_expand e0 e1 (is_zero et). - (** ** Constants **) Definition addrsymbol (id: ident) (ofs: ptrofs) := |