From 11cd0ace897752ef7ca33609aa1250ca1597185b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 29 May 2019 11:14:46 +0200 Subject: arranging for selection of divisor as option --- mppa_k1c/TargetPrinter.ml | 48 +++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 44 insertions(+), 4 deletions(-) (limited to 'mppa_k1c/TargetPrinter.ml') diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 96779517..4dc4b7c2 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -34,11 +34,51 @@ module Target (*: TARGET*) = let comment = "#" + type idiv_function_kind = + | Idiv_system + | Idiv_stsud + | Idiv_fp;; + + let idiv_function_kind_32bit () = Idiv_fp;; + let idiv_function_kind_64bit () = Idiv_stsud;; + let subst_symbol = function - "__compcert_i64_udiv" -> "__udivdi3" - | "__compcert_i64_sdiv" -> "__divdi3" - | "__compcert_i64_umod" -> "__umoddi3" - | "__compcert_i64_smod" -> "__moddi3" + "__compcert_i64_udiv" -> + (match idiv_function_kind_64bit () with + | Idiv_system | Idiv_fp -> "__udivdi3" + | Idiv_stsud -> "__compcert_i64_udiv_stsud") + | "__compcert_i64_sdiv" -> + (match idiv_function_kind_64bit() with + | Idiv_system | Idiv_fp -> "__divdi3" + | Idiv_stsud -> "__compcert_i64_sdiv_stsud") + | "__compcert_i64_umod" -> + (match idiv_function_kind_64bit() with + | Idiv_system | Idiv_fp -> "__umoddi3" + | Idiv_stsud -> "__compcert_i64_umod_stsud") + | "__compcert_i64_smod" -> + (match idiv_function_kind_64bit() with + | Idiv_system | Idiv_fp -> "__moddi3" + | Idiv_stsud -> "__compcert_i64_stsud") + | "__compcert_i32_sdiv" as s -> + (match idiv_function_kind_32bit() with + | Idiv_system -> s + | Idiv_fp -> "__compcert_i32_sdiv_fp" + | Idiv_stsud -> "__compcert_i32_sdiv_stsud") + | "__compcert_i32_udiv" as s -> + (match idiv_function_kind_32bit() with + | Idiv_system -> s + | Idiv_fp -> "__compcert_i32_udiv_fp" + | Idiv_stsud -> "__compcert_i32_udiv_stsud") + | "__compcert_i32_smod" as s -> + (match idiv_function_kind_32bit() with + | Idiv_system -> s + | Idiv_fp -> "__compcert_i32_smod_fp" + | Idiv_stsud -> "__compcert_i32_smod_stsud") + | "__compcert_i32_umod" as s -> + (match idiv_function_kind_32bit() with + | Idiv_system -> s + | Idiv_fp -> "__compcert_i32_umod_fp" + | Idiv_stsud -> "__compcert_i32_umod_stsud") | "__compcert_f64_div" -> "__divdf3" | "__compcert_f32_div" -> "__divsf3" | x -> x;; -- cgit From d075968e1e516ab80460afce57c9bcc15d206c19 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 29 May 2019 11:43:29 +0200 Subject: added -fdiv-i32 and -fdiv-i64 options --- mppa_k1c/TargetPrinter.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'mppa_k1c/TargetPrinter.ml') diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 4dc4b7c2..2bdd0978 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -39,8 +39,14 @@ module Target (*: TARGET*) = | Idiv_stsud | Idiv_fp;; - let idiv_function_kind_32bit () = Idiv_fp;; - let idiv_function_kind_64bit () = Idiv_stsud;; + let idiv_function_kind = function + "stsud" -> Idiv_stsud + | "system" -> Idiv_system + | "fp" -> Idiv_fp + | _ -> failwith "unknown integer division kind";; + + let idiv_function_kind_32bit () = idiv_function_kind !Clflags.option_div_i32;; + let idiv_function_kind_64bit () = idiv_function_kind !Clflags.option_div_i64;; let subst_symbol = function "__compcert_i64_udiv" -> -- cgit