diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-01 16:44:29 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-01 16:44:29 +0200 |
| commit | 75d50c12ee220fecf955b1626c78b78636cbca92 (patch) | |
| tree | d1d3926a9df12113d36350ed6c8d6f55e373c748 /powerpc/Asm.v | |
| parent | 951963b380f1ff1e0b55f8303e4ae098cedb3cb5 (diff) | |
| download | compcert-kvx-75d50c12ee220fecf955b1626c78b78636cbca92.tar.gz compcert-kvx-75d50c12ee220fecf955b1626c78b78636cbca92.zip | |
Added the gcc builtin prefetch.
This commit implements the gcc __builtin_prefetch in a form with all
arguments for the powerpc architecture. The resulting instructions are
the dcbt and dcbtst instructions in Server Category.
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 589d66fe..dbb819d1 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -167,6 +167,8 @@ Inductive instruction : Type := | Pcrxor: crbit -> crbit -> crbit -> instruction (**r xor between condition bits *) | Pdcbf: ireg -> ireg -> instruction (**r data cache flush *) | Pdcbi: ireg -> ireg -> instruction (**r data cache invalidate *) + | Pdcbt: int -> ireg -> instruction (**r data cache block touch *) + | Pdcbtst: int -> ireg -> instruction (**r data cache block touch *) | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) | Peieio: instruction (**r EIEIO barrier *) @@ -870,6 +872,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pcrxor _ _ _ | Pdcbf _ _ | Pdcbi _ _ + | Pdcbt _ _ + | Pdcbtst _ _ | Peieio | Pfctiw _ _ | Pfctiwz _ _ |