diff options
| -rw-r--r-- | aarch64/Makefile | 3 | ||||
| -rw-r--r-- | aarch64/no_vector/spec.sail | 2 | ||||
| -rw-r--r-- | src/constant_fold.ml | 160 | ||||
| -rw-r--r-- | src/interpreter.ml | 30 | ||||
| -rw-r--r-- | src/isail.ml | 8 | ||||
| -rw-r--r-- | src/process_file.ml | 6 | ||||
| -rw-r--r-- | src/sail.ml | 5 |
7 files changed, 196 insertions, 18 deletions
diff --git a/aarch64/Makefile b/aarch64/Makefile index e307f604..58281dc7 100644 --- a/aarch64/Makefile +++ b/aarch64/Makefile @@ -7,6 +7,9 @@ SAIL:=$(SAIL_DIR)/sail aarch64.c: no_vector.sail $(SAIL) $^ -c -O -undefined_gen -no_lexp_bounds_check -memo_z3 1> aarch64.c +aarch64_c: aarch64.c + gcc -O2 $^ -o aarch64_c -lgmp -L $(SAIL_DIR)/lib + aarch64: no_vector.sail $(SAIL) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3 diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail index 4da6fa33..8710e66b 100644 --- a/aarch64/no_vector/spec.sail +++ b/aarch64/no_vector/spec.sail @@ -2608,7 +2608,7 @@ function ComputePAC (data, modifier, key0, key1) = { val Align__0 : (int, int) -> int -val Align__1 = {c: "arm_align"} : forall ('N : Int), 'N >= 0 & 'N >= 0. (bits('N), int) -> bits('N) +val Align__1 : forall ('N : Int), 'N >= 0 & 'N >= 0. (bits('N), int) -> bits('N) overload Align = {Align__0, Align__1} diff --git a/src/constant_fold.ml b/src/constant_fold.ml new file mode 100644 index 00000000..cf593b04 --- /dev/null +++ b/src/constant_fold.ml @@ -0,0 +1,160 @@ +(**************************************************************************) +(* 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 Type_check +open Rewriter + +module StringMap = Map.Make(String);; + +(* Flag controls whether any constant folding will occur. + false = no folding, true = perform constant folding. *) +let optimize_constant_fold = ref false + +let exp_of_value = + let open Value in + function + | V_int n -> mk_lit_exp (L_num n) + | _ -> failwith "No expression for value" + +(* We want to avoid evaluating things like print statements at compile + time, so we remove them from this list of primops we can use when + constant folding. *) +let safe_primops = + List.fold_left + (fun m k -> StringMap.remove k m) + Value.primops + [ "print_endline"; + "prerr_endline"; + "putchar"; + "print_bits"; + "print_int"; + "print_string"; + "prerr_bits"; + "prerr_int"; + "prerr_string"; + "Elf_loader.elf_entry"; + "Elf_loader.elf_tohost" + ] + +let is_literal = function + | E_aux (E_lit _, _) -> true + | _ -> false + +(* Wrapper around interpreter that repeatedly steps until done. *) +let rec run ast frame = + match frame with + | Interpreter.Done (state, v) -> v + | Interpreter.Step _ -> + run ast (Interpreter.eval_frame ast frame) + | Interpreter.Break frame -> + run ast (Interpreter.eval_frame ast frame) + +(** This rewriting pass looks for function applications (E_app) + expressions where every argument is a literal. It passes these + expressions to the OCaml interpreter in interpreter.ml, and + reconstructs the values returned back into expressions which are + then re-typechecked and re-inserted back into the AST. + + We don't use the effect system to decide if expressions are safe to + evaluate, because this ignores I/O, and would force us to ignore + functions that maybe throw exceptions internally but as called are + totally safe. Instead any exceptions during evaluation are caught, + and the original expression is kept. Some causes of this could be: + + - Function tries to read/write register. + - Calls an unsafe primop. + - Throws an exception that isn't caught. + *) + +let rewrite_constant_function_calls' ast = + let lstate, gstate = + Interpreter.initial_state ast safe_primops + in + let gstate = { gstate with Interpreter.allow_registers = false } in + + let rw_funcall e_aux annot = + match e_aux with + | E_app (id, args) when List.for_all is_literal args -> + begin + let initial_monad = Interpreter.return (E_aux (e_aux, annot)) in + try + begin + let v = run ast (Interpreter.Step (lazy "", (lstate, gstate), initial_monad, [])) in + let exp = exp_of_value v in + try Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot) with + | Type_error (l, err) -> + (* A type error here would be unexpected, so don't ignore it! *) + Util.warn ("Type error when folding constants in " + ^ string_of_exp (E_aux (e_aux, annot)) + ^ "\n" ^ Type_error.string_of_type_error err); + E_aux (e_aux, annot) + end + with + (* Otherwise if anything goes wrong when trying to constant + fold, just continue without optimising. *) + | _ -> E_aux (e_aux, annot) + end + + | _ -> E_aux (e_aux, annot) + in + let rw_exp = { + id_exp_alg with + e_aux = (fun (e_aux, annot) -> rw_funcall e_aux annot) + } in + let rw_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp rw_exp) } in + rewrite_defs_base rw_defs ast + +let rewrite_constant_function_calls ast = + if !optimize_constant_fold then + rewrite_constant_function calls' ast + else + ast diff --git a/src/interpreter.ml b/src/interpreter.ml index 781e4e41..00846d73 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -54,7 +54,9 @@ open Value type gstate = { registers : value Bindings.t; + allow_registers : bool; (* For some uses we want to forbid touching any registers. *) boxes : value StringMap.t; + primops : (value list -> value) StringMap.t; letbinds : (Type_check.tannot letbind) list; } @@ -80,16 +82,18 @@ let rec ast_letbinds (Defs defs) = | DEF_val lb :: defs -> lb :: ast_letbinds (Defs defs) | _ :: defs -> ast_letbinds (Defs defs) -let initial_gstate ast = +let initial_gstate ast primops = { registers = Bindings.empty; + allow_registers = true; boxes = StringMap.empty; + primops = primops; letbinds = ast_letbinds ast; } let initial_lstate = { locals = Bindings.empty } -let initial_state ast = initial_lstate, initial_gstate ast +let initial_state ast primops = initial_lstate, initial_gstate ast primops let value_of_lit (L_aux (l_aux, _)) = match l_aux with @@ -335,10 +339,15 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = if extern = "reg_deref" then let regname = List.hd evaluated |> value_of_exp |> coerce_ref in gets >>= fun (_, gstate) -> - try return (exp_of_value (Bindings.find (mk_id regname) gstate.registers)) with + try + if gstate.allow_registers + then return (exp_of_value (Bindings.find (mk_id regname) gstate.registers)) + else raise Not_found + with | Not_found -> return (exp_of_value (StringMap.find regname gstate.boxes)) else - let primop = try StringMap.find extern primops with Not_found -> failwith ("No primop " ^ extern) in + gets >>= fun (_, gstate) -> + let primop = try StringMap.find extern gstate.primops with Not_found -> failwith ("No primop " ^ extern) in return (exp_of_value (primop (List.map value_of_exp evaluated))) end | [] -> liftM exp_of_value (call id (List.map value_of_exp evaluated)) @@ -392,7 +401,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_ref id -> gets >>= fun (lstate, gstate) -> - if Bindings.mem id gstate.registers then + if Bindings.mem id gstate.registers && gstate.allow_registers then return (exp_of_value (V_ref (string_of_id id))) else if Bindings.mem id lstate.locals then let b = box_name id in @@ -413,7 +422,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = let open Type_check in gets >>= fun (lstate, gstate) -> match Env.lookup_id id (env_of_annot annot) with - | Register _ -> + | Register _ when gstate.allow_registers -> let exp = try exp_of_value (Bindings.find id gstate.registers) with | Not_found -> @@ -428,7 +437,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = return chain | Enum _ -> return (exp_of_value (V_ctor (string_of_id id, []))) - | _ -> failwith ("id " ^ string_of_id id) + | _ -> failwith ("Coudln't find id " ^ string_of_id id) end | E_record (FES_aux (FES_Fexps (fexps, flag), fes_annot)) -> @@ -492,7 +501,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = let open Type_check in gets >>= fun (lstate, gstate) -> match Env.lookup_id id (env_of_annot annot) with - | Register _ -> + | Register _ when gstate.allow_registers -> puts (lstate, { gstate with registers = Bindings.add id (value_of_exp exp) gstate.registers }) >> wrap unit_exp | Local (Mutable, _) | Unbound -> begin @@ -508,7 +517,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | E_assign (LEXP_aux (LEXP_deref reference, annot), exp) -> let name = coerce_ref (value_of_exp reference) in gets >>= fun (lstate, gstate) -> - if Bindings.mem (mk_id name) gstate.registers then + if Bindings.mem (mk_id name) gstate.registers && gstate.allow_registers then puts (lstate, { gstate with registers = Bindings.add (mk_id name) (value_of_exp exp) gstate.registers }) >> wrap unit_exp else puts (lstate, { gstate with boxes = StringMap.add name (value_of_exp exp) gstate.boxes }) >> wrap unit_exp @@ -670,8 +679,7 @@ let rec eval_frame' ast = function | Yield (Assertion_failed msg), _ -> failwith msg | Yield (Exception v), _ -> - print_endline ("Uncaught Exception" |> Util.cyan |> Util.clear); - Done (state, v) + failwith ("Uncaught Exception" |> Util.cyan |> Util.clear) let eval_frame ast frame = try eval_frame' ast frame with diff --git a/src/isail.ml b/src/isail.ml index 514b8763..593167f9 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -103,7 +103,7 @@ let sail_logo = let vs_ids = ref (Initial_check.val_spec_ids !interactive_ast) -let interactive_state = ref (initial_state !interactive_ast) +let interactive_state = ref (initial_state !interactive_ast Value.primops) let print_program () = match !current_mode with @@ -263,7 +263,7 @@ let handle_input' input = let ast, env = Specialize.specialize !interactive_ast !interactive_env in interactive_ast := ast; interactive_env := env; - interactive_state := initial_state !interactive_ast + interactive_state := initial_state !interactive_ast Value.primops | ":pretty" -> print_endline (Pretty_print_sail.to_string (Latex.latex_defs "sail_latex" !interactive_ast)) | ":bytecode" -> @@ -305,13 +305,13 @@ let handle_input' input = let (_, ast, env) = load_files !interactive_env files in let ast = Process_file.rewrite_ast_interpreter ast in interactive_ast := append_ast !interactive_ast ast; - interactive_state := initial_state !interactive_ast; + interactive_state := initial_state !interactive_ast Value.primops; interactive_env := env; vs_ids := Initial_check.val_spec_ids !interactive_ast | ":u" | ":unload" -> interactive_ast := Ast.Defs []; interactive_env := Type_check.initial_env; - interactive_state := initial_state !interactive_ast; + interactive_state := initial_state !interactive_ast Value.primops; vs_ids := Initial_check.val_spec_ids !interactive_ast; (* See initial_check.mli for an explanation of why we need this. *) Initial_check.have_undefined_builtins := false diff --git a/src/process_file.ml b/src/process_file.ml index 2e69f59b..78e7fa48 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -363,6 +363,10 @@ let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefin let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_lem let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml -let rewrite_ast_c = rewrite Rewrites.rewrite_defs_c +let rewrite_ast_c ast = + ast + |> rewrite Rewrites.rewrite_defs_c + |> Constant_fold.rewrite_constant_function_calls + let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check diff --git a/src/sail.ml b/src/sail.ml index 2e150ff4..36b4efd8 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -115,7 +115,10 @@ let options = Arg.align ([ " turn on optimizations for C compilation"); ( "-Oz3", Arg.Set C_backend.optimize_z3, - " use z3 analysis for optimization (slow)"); + " use z3 analysis for optimization (experimental)"); + ( "-Oconstant_fold", + Arg.Set Constant_fold.optimize_constant_fold, + " Apply constant folding optimizations"); ( "-lem_ast", Arg.Set opt_print_lem_ast, " output a Lem AST representation of the input"); |