summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml9
-rw-r--r--src/ast_util.mli2
-rw-r--r--src/c_backend.ml3
-rw-r--r--src/optimize.ml100
-rw-r--r--src/rewrites.ml2
-rw-r--r--src/type_check.ml8
-rw-r--r--src/type_check.mli4
7 files changed, 124 insertions, 4 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index a771291e..6fce9a2a 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -128,7 +128,7 @@ let mk_val_spec vs_aux =
let kopt_kid (KOpt_aux (KOpt_kind (_, kid), _)) = kid
let kopt_kind (KOpt_aux (KOpt_kind (k, _), _)) = k
-
+
let is_nat_kopt = function
| KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> true
| _ -> false
@@ -165,7 +165,7 @@ module Kind = struct
| K_type, _ -> 1 | _, K_type -> -1
| K_order, _ -> 1 | _, K_order -> -1
end
-
+
module KOpt = struct
type t = kinded_id
let compare kopt1 kopt2 =
@@ -1289,6 +1289,9 @@ let is_fundef id = function
| DEF_fundef (FD_aux (FD_function (_, _, _, FCL_aux (FCL_Funcl (id', _), _) :: _), _)) when Id.compare id' id = 0 -> true
| _ -> false
+let rename_valspec id (VS_aux (VS_val_spec (typschm, _, externs, is_cast), annot)) =
+ VS_aux (VS_val_spec (typschm, id, externs, is_cast), annot)
+
let rename_funcl id (FCL_aux (FCL_Funcl (_, pexp), annot)) = FCL_aux (FCL_Funcl (id, pexp), annot)
let rename_fundef id (FD_aux (FD_function (ropt, topt, eopt, funcls), annot)) =
@@ -1425,7 +1428,7 @@ let locate_id f (Id_aux (name, l)) = Id_aux (name, f l)
let locate_kid f (Kid_aux (name, l)) = Kid_aux (name, f l)
let locate_kind f (K_aux (kind, l)) = K_aux (kind, f l)
-
+
let locate_kinded_id f (KOpt_aux (KOpt_kind (k, kid), l)) =
KOpt_aux (KOpt_kind (locate_kind f k, locate_kid f kid), f l)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index ca3a9598..f741704a 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -372,6 +372,8 @@ val is_valspec : id -> 'a def -> bool
val is_fundef : id -> 'a def -> bool
+val rename_valspec : id -> 'a val_spec -> 'a val_spec
+
val rename_fundef : id -> 'a fundef -> 'a fundef
val split_defs : ('a def -> bool) -> 'a defs -> ('a defs * 'a def * 'a defs) option
diff --git a/src/c_backend.ml b/src/c_backend.ml
index f02cdb9c..7cda4668 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -1763,6 +1763,9 @@ let rec compile_def ctx = function
(* Only the parser and sail pretty printer care about this. *)
| DEF_fixity _ -> [], ctx
+ (* We just ignore any pragmas we don't want to deal with. *)
+ | DEF_pragma _ -> [], ctx
+
| DEF_internal_mutrec fundefs ->
let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in
List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs
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)
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 8894f2c8..382f9c8f 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5129,7 +5129,7 @@ let rewrite_defs_c = [
("trivial_sizeof", rewrite_trivial_sizeof);
("sizeof", rewrite_sizeof);
("merge_function_clauses", merge_funcls);
- ("recheck_defs", recheck_defs)
+ ("recheck_defs", Optimize.recheck)
]
let rewrite_defs_interpreter = [
diff --git a/src/type_check.ml b/src/type_check.ml
index 1b6efa46..712b9944 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -4470,6 +4470,14 @@ and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
let (Defs defs, env) = check env (Defs defs) in
(Defs (def @ defs)), env
+and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list =
+ fun env defs ->
+ match defs with
+ | [] -> []
+ | def :: defs ->
+ let def, env = check_def env def in
+ (def, env) :: check_with_envs env defs
+
let initial_env =
Env.empty
|> Env.add_prover prove
diff --git a/src/type_check.mli b/src/type_check.mli
index 81682606..6a0f0410 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -411,5 +411,9 @@ Some invariants that will hold of a fully checked AST are:
Type_error.check *)
val check : Env.t -> 'a defs -> tannot defs * Env.t
+(** The same as [check], but exposes the intermediate type-checking
+ environments so we don't have to always re-check the entire AST *)
+val check_with_envs : Env.t -> 'a def list -> (tannot def list * Env.t) list
+
(** The initial type checking environment *)
val initial_env : Env.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 08:30:31 +0000