diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-02 13:50:24 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-02 13:50:24 +0200 |
| commit | db8e35c6abf58c82853b94f416aa76b33efc1f65 (patch) | |
| tree | dcd1a758de6234817c9947e9898c1bc87937e597 /powerpc/Asm.v | |
| parent | 75d50c12ee220fecf955b1626c78b78636cbca92 (diff) | |
| download | compcert-db8e35c6abf58c82853b94f416aa76b33efc1f65.tar.gz compcert-db8e35c6abf58c82853b94f416aa76b33efc1f65.zip | |
Added builtin for dcbtls
THis commit adds a builtin function for the dcbtls instruction.
Additionaly it changes the printing of the dcbt and dcbtst instruction to
embedded mode and adds support for different address variants.
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index dbb819d1..43ddc1ed 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -168,7 +168,8 @@ Inductive instruction : Type := | 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 *) + | Pdcbtst: int -> ireg -> instruction (**r data cache block touch *) + | Pdcbtls: int -> ireg -> instruction (**r data cache block touch and lock set *) | Pdivw: ireg -> ireg -> ireg -> instruction (**r signed division *) | Pdivwu: ireg -> ireg -> ireg -> instruction (**r unsigned division *) | Peieio: instruction (**r EIEIO barrier *) @@ -874,6 +875,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pdcbi _ _ | Pdcbt _ _ | Pdcbtst _ _ + | Pdcbtls _ _ | Peieio | Pfctiw _ _ | Pfctiwz _ _ |