From 263d7fe07538c35ea371bc77198803a29e7aaf34 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 8 Mar 2018 10:22:02 +0100 Subject: Removed % prefix from ais annot register names. Registers should not contain the % prefix for ais annotations. Bug 23176 --- x86/TargetPrinter.ml | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) (limited to 'x86/TargetPrinter.ml') diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 12ef6472..97af0cab 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -72,6 +72,23 @@ let preg_annot = function | FR r -> float_reg_name r | _ -> assert false +let ais_int64_reg_name = function + | RAX -> "rax" | RBX -> "rbx" | RCX -> "rcx" | RDX -> "rdx" + | RSI -> "rsi" | RDI -> "rdi" | RBP -> "rbp" | RSP -> "rsp" + | R8 -> "r8" | R9 -> "r9" | R10 -> "r10" | R11 -> "r11" + | R12 -> "r12" | R13 -> "r13" | R14 -> "r14" | R15 -> "r15" + +let ais_int32_reg_name = function + | RAX -> "eax" | RBX -> "ebx" | RCX -> "ecx" | RDX -> "edx" + | RSI -> "esi" | RDI -> "edi" | RBP -> "ebp" | RSP -> "esp" + | R8 -> "r8d" | R9 -> "r9d" | R10 -> "r10d" | R11 -> "r11d" + | R12 -> "r12d" | R13 -> "r13d" | R14 -> "r14d" | R15 -> "r15d" + +let preg_ais_annot = function + | IR r -> if Archi.ptr64 then ais_int64_reg_name r else ais_int32_reg_name r + | FR r -> float_reg_name r + | _ -> assert false + let z oc n = output_string oc (Z.to_string n) (* 32/64 bit dependencies *) @@ -798,7 +815,7 @@ module Target(System: SYSTEM):TARGET = fprintf oc "%s annotation: %S\n" comment annot | 2 -> let lbl = new_label () in fprintf oc "%a: " label lbl; - add_ais_annot lbl preg_annot "r1" (camlstring_of_coqstring txt) args + add_ais_annot lbl preg_ais_annot "r1" (camlstring_of_coqstring txt) args | _ -> assert false end | EF_debug(kind, txt, targs) -> -- cgit