From fb9578680d1cd88650e7e6aa9bf1e1ffd8b32f49 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 15 Sep 2015 12:32:09 +0200 Subject: Removed usage of bne and removed duplicated code for return values of atomics. Instead of introducing a new bne instruction in Asm.v and the TargetPrinter.ml I use the equivalent bf instruction. The duplicated code is due to unused return values of builtins. Now we only emit the additional code for the return value if the return value is used instead of duplicating the whole emiting sequence. --- powerpc/Asm.v | 4 ---- 1 file changed, 4 deletions(-) (limited to 'powerpc/Asm.v') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 5fd40a27..3c7bdd15 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -153,8 +153,6 @@ Inductive instruction : Type := | Pbdnz: label -> instruction (**r decrement CTR and branch if not zero *) | Pbf: crbit -> label -> instruction (**r branch if false *) | Pbl: ident -> signature -> instruction (**r branch and link *) - | Pbne: label -> instruction (**r branch not equal *) - | Pbne_rel: int -> instruction (**r branch not equal with relative offset *) | Pbs: ident -> signature -> instruction (**r branch to symbol *) | Pblr: instruction (**r branch to contents of register LR *) | Pbt: crbit -> label -> instruction (**r branch if true *) @@ -875,8 +873,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** The following instructions and directives are not generated directly by [Asmgen], so we do not model them. *) | Pbdnz _ - | Pbne _ - | Pbne_rel _ | Pcmpb _ _ _ | Pcntlzw _ _ | Pcreqv _ _ _ -- cgit