From 094ac30cfbc757dd633191513c05b0738993651d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 25 Jul 2020 17:11:44 +0200 Subject: RISC-V implementation of __builtin_clz* and __builtin_ctz* Using binary search loops expanded at point of use. --- riscV/Machregs.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) (limited to 'riscV/Machregs.v') diff --git a/riscV/Machregs.v b/riscV/Machregs.v index d8bb4a4b..d469e594 100644 --- a/riscV/Machregs.v +++ b/riscV/Machregs.v @@ -194,6 +194,17 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_inline_asm txt sg clob => destroyed_by_clobber clob | EF_memcpy sz al => R5 :: R6 :: R7 :: F0 :: nil + | EF_builtin name sg => + if string_dec name "__builtin_clz" + || string_dec name "__builtin_clzl" + || string_dec name "__builtin_clzll" then + R5 :: R8 :: R9 :: nil + else if string_dec name "__builtin_ctz" + || string_dec name "__builtin_ctzl" + || string_dec name "__builtin_ctzll" then + R6 :: R8 :: R9 :: nil + else + nil | _ => nil end. @@ -213,6 +224,20 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list( | EF_builtin name sg => if (negb Archi.ptr64) && string_dec name "__builtin_bswap64" then (Some R6 :: Some R5 :: nil, Some R5 :: Some R6 :: nil) + else if string_dec name "__builtin_clz" + || string_dec name "__builtin_clzl" then + (Some R5 :: nil, Some R7 :: nil) + else if string_dec name "__builtin_clzll" then + if Archi.ptr64 + then (Some R5 :: nil, Some R7 :: nil) + else (Some R6 :: Some R5 :: nil, Some R7 :: nil) + else if string_dec name "__builtin_ctz" + || string_dec name "__builtin_ctzl" then + (Some R6 :: nil, Some R7 :: nil) + else if string_dec name "__builtin_ctzll" then + if Archi.ptr64 + then (Some R6 :: nil, Some R7 :: nil) + else (Some R6 :: Some R5 :: nil, Some R7 :: nil) else (nil, nil) | _ => -- cgit