From 0f919eb26c68d3882e612a1b3a9df45bee6d3624 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 13 Feb 2019 18:53:17 +0100 Subject: Upgrade embedded version of Flocq to 3.1. Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully). --- extraction/extraction.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index a47a7237..15a64d89 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -153,11 +153,11 @@ Load extractionMachdep. Extraction Blacklist List String Int. (* Cutting the dependency to R. *) -Extract Inlined Constant Fcore_defs.F2R => "fun _ -> assert false". -Extract Inlined Constant Fappli_IEEE.FF2R => "fun _ -> assert false". -Extract Inlined Constant Fappli_IEEE.B2R => "fun _ -> assert false". -Extract Inlined Constant Fappli_IEEE.round_mode => "fun _ -> assert false". -Extract Inlined Constant Fcalc_bracket.inbetween_loc => "fun _ -> assert false". +Extract Inlined Constant Defs.F2R => "fun _ -> assert false". +Extract Inlined Constant Binary.FF2R => "fun _ -> assert false". +Extract Inlined Constant Binary.B2R => "fun _ -> assert false". +Extract Inlined Constant Binary.round_mode => "fun _ -> assert false". +Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. -- cgit From 95938a8732b572d61955b1de8c49362c9e162640 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 31 May 2019 19:15:19 +0200 Subject: If-conversion optimization Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches. --- extraction/extraction.v | 1 + 1 file changed, 1 insertion(+) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 15a64d89..c0286f7b 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -72,6 +72,7 @@ Extract Constant Iteration.GenIter.iterate => (* Selection *) Extract Constant Selection.compile_switch => "Switchaux.compile_switch". +Extract Constant Selection.if_conversion_heuristic => "Selectionaux.if_conversion_heuristic". (* RTLgen *) Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". -- cgit