From db8e35c6abf58c82853b94f416aa76b33efc1f65 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 2 Sep 2015 13:50:24 +0200 Subject: 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. --- powerpc/Asm.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'powerpc/Asm.v') 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 _ _ -- cgit