Add a pragma for unrolling recursive functions

For example in RISC-V for the translation table walk:

$optimize unroll 2
val walk32 ...
function walk32 ...

would create two extra copies of the walk_32 function,
walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2
being recursive. Currently we only support the case where we have
$optimize unroll, directly followed by a valspec, then a function, but
this should be generalised in future.

This optimization nearly doubles the performance of RISC-V

It is implemented using a new Optimize.recheck rewrite that replaces
the ordinary recheck_defs pass. It uses a new typechecker
check_with_envs function that allows re-writes to utilise intermediate
typechecking environments to minimize the amount of AST checking that
occurs, for performance reasons.

Note that older Sail versions including the current OPAM release will
complain about the optimize pragma, so this cannot be used until they
become up to date with this change.

1 files changed, 100 insertions, 0 deletions

diff --git a/src/optimize.ml b/src/optimize.ml
new file mode 100644
index 00000000..a372abf4
--- /dev/null
+++ b/src/optimize.ml
@@ -0,0 +1,100 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open Rewriter
+
+let recheck (Defs defs) =
+  let defs = Type_check.check_with_envs Type_check.initial_env defs in
+
+  let rec find_optimizations = function
+    | ([DEF_pragma ("optimize", pragma, p_l)], env)
+      :: ([DEF_spec vs as def1], _)
+      :: ([DEF_fundef fdef as def2], _)
+      :: defs ->
+       let id = id_of_val_spec vs in
+       let args = Str.split (Str.regexp " +") (String.trim pragma) in
+       begin match args with
+       | ["unroll"; n]->
+          let n = int_of_string n in
+
+          let rw_app subst (fn, args) =
+            if Id.compare id fn = 0 then E_app (subst, args) else E_app (fn, args)
+          in
+          let rw_exp subst = { id_exp_alg with e_app = rw_app subst } in
+          let rw_defs subst = { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rw_exp subst)) } in
+
+          let specs = ref [def1] in
+          let bodies = ref [rewrite_def (rw_defs (append_id id "_unroll_1")) def2] in
+
+          for i = 1 to n do
+            let current_id = append_id id ("_unroll_" ^ string_of_int i) in
+            let next_id = if i = n then current_id else append_id id ("_unroll_" ^ string_of_int (i + 1)) in
+            (* Create a valspec for the new unrolled function *)
+            specs := !specs @ [DEF_spec (rename_valspec current_id vs)];
+            (* Then duplicate it's function body and make it call the next unrolled function *)
+            bodies := !bodies @ [rewrite_def (rw_defs next_id) (DEF_fundef (rename_fundef current_id fdef))]
+          done;
+
+          !specs @ !bodies @ find_optimizations defs
+
+       | _ ->
+          Util.warn ("Unrecognised optimize pragma in this context: " ^ pragma);
+          def1 :: def2 :: find_optimizations defs
+       end
+
+    | (defs, _) :: defs' ->
+       defs @ find_optimizations defs'
+
+    | [] -> []
+  in
+
+  Defs (find_optimizations defs)