diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 355 |
1 files changed, 211 insertions, 144 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 57a14028..80cfdccb 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -48,68 +48,160 @@ (* SUCH DAMAGE. *) (**************************************************************************) -open Type_internal +let opt_lem_sequential = ref false +let opt_lem_mwords = ref false type out_type = | Lem_ast_out - | Lem_out of string option - | Ocaml_out of string option + | Lem_out of string list -let get_lexbuf fn = - let lexbuf = Lexing.from_channel (open_in fn) in - lexbuf.Lexing.lex_curr_p <- { Lexing.pos_fname = fn; - Lexing.pos_lnum = 1; - Lexing.pos_bol = 0; - Lexing.pos_cnum = 0; }; - lexbuf +let get_lexbuf f = + let in_chan = open_in f in + let lexbuf = Lexing.from_channel in_chan in + lexbuf.Lexing.lex_curr_p <- { Lexing.pos_fname = f; + Lexing.pos_lnum = 1; + Lexing.pos_bol = 0; + Lexing.pos_cnum = 0; }; + lexbuf, in_chan let parse_file (f : string) : Parse_ast.defs = - let scanbuf = get_lexbuf f in - let type_names = + let lexbuf, in_chan = get_lexbuf f in try - Pre_parser.file Pre_lexer.token scanbuf + let ast = Parser.file Lexer.token lexbuf in + close_in in_chan; ast with - | Parsing.Parse_error -> - let pos = Lexing.lexeme_start_p scanbuf in - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "pre"))) - | Parse_ast.Parse_error_locn(l,m) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))) - | Lexer.LexError(s,p) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) in - let () = Lexer.custom_type_names := !Lexer.custom_type_names @ type_names in - let lexbuf = get_lexbuf f in - try - Parser.file Lexer.token lexbuf - with - | Parsing.Parse_error -> - let pos = Lexing.lexeme_start_p lexbuf in - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main"))) - | Parse_ast.Parse_error_locn(l,m) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))) - | Lexer.LexError(s,p) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) - -(*Should add a flag to say whether we want to consider Oinc or Odec the default order *) -let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)= - Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs - -let initi_check_ast (defs : Type_internal.tannot Ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t * Ast.order)= - Initial_check_full_ast.to_checked_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs - -let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs * Type_check.envs = - let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env; - Type_internal.nabbrevs = Envmap.empty; - Type_internal.namesch = Envmap.empty; Type_internal.enum_env = Envmap.empty; - Type_internal.rec_env = []; Type_internal.alias_env = Envmap.empty; - Type_internal.default_o = - {Type_internal.order = (match o with | (Ast.Ord_aux(Ast.Ord_inc,_)) -> Type_internal.Oinc - | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec - | _ -> Type_internal.Oinc)};} in - Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob,Envmap.empty)) defs - -let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs -let rewrite_ast_lem (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs_lem defs -let rewrite_ast_ocaml (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs_ocaml defs + | Parser.Error -> + let pos = Lexing.lexeme_start_p lexbuf in + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "no information"))) + | Lexer.LexError(s,p) -> + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) + +(* Simple preprocessor features for conditional file loading *) +module StringSet = Set.Make(String) + +let symbols = ref StringSet.empty + +let cond_pragma defs = + let depth = ref 0 in + let in_then = ref true in + let then_defs = ref [] in + let else_defs = ref [] in + + let push_def def = + if !in_then then + then_defs := (def :: !then_defs) + else + else_defs := (def :: !else_defs) + in + + let rec scan = function + | Parse_ast.DEF_pragma ("endif", _, _) :: defs when !depth = 0 -> + (List.rev !then_defs, List.rev !else_defs, defs) + | Parse_ast.DEF_pragma ("else", _, _) :: defs when !depth = 0 -> + in_then := false; scan defs + | (Parse_ast.DEF_pragma (p, _, _) as def) :: defs when p = "ifdef" || p = "ifndef" -> + incr depth; push_def def; scan defs + | (Parse_ast.DEF_pragma ("endif", _, _) as def) :: defs-> + decr depth; push_def def; scan defs + | def :: defs -> + push_def def; scan defs + | [] -> failwith "$ifdef or $ifndef never ended" + in + scan defs + +let rec preprocess = function + | [] -> [] + | Parse_ast.DEF_pragma ("define", symbol, _) :: defs -> + symbols := StringSet.add symbol !symbols; + preprocess defs + + | Parse_ast.DEF_pragma ("ifndef", symbol, _) :: defs -> + let then_defs, else_defs, defs = cond_pragma defs in + if not (StringSet.mem symbol !symbols) then + preprocess (then_defs @ defs) + else + preprocess (else_defs @ defs) + + | Parse_ast.DEF_pragma ("ifdef", symbol, _) :: defs -> + let then_defs, else_defs, defs = cond_pragma defs in + if StringSet.mem symbol !symbols then + preprocess (then_defs @ defs) + else + preprocess (else_defs @ defs) + + | Parse_ast.DEF_pragma ("include", file, l) :: defs -> + let len = String.length file in + if len = 0 then + (Util.warn "Skipping bad $include. No file argument."; preprocess defs) + else if file.[0] = '"' && file.[len - 1] = '"' then + let relative = match l with + | Parse_ast.Range (pos, _) -> Filename.dirname (Lexing.(pos.pos_fname)) + | _ -> failwith "Couldn't figure out relative path for $include. This really shouldn't ever happen." + in + let file = String.sub file 1 (len - 2) in + let (Parse_ast.Defs include_defs) = parse_file (Filename.concat relative file) in + let include_defs = preprocess include_defs in + include_defs @ preprocess defs + else if file.[0] = '<' && file.[len - 1] = '>' then + let file = String.sub file 1 (len - 2) in + let sail_dir = + try Sys.getenv "SAIL_DIR" with + | Not_found -> (failwith ("Environment variable SAIL_DIR unset. Cannot $include " ^ file)) + in + let file = Filename.concat sail_dir ("lib/" ^ file) in + let (Parse_ast.Defs include_defs) = parse_file file in + let include_defs = preprocess include_defs in + include_defs @ preprocess defs + else + let help = "Make sure the filename is surrounded by quotes or angle brackets" in + (Util.warn ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess defs) + + | Parse_ast.DEF_pragma (p, arg, _) :: defs -> + (Util.warn ("Bad pragma $" ^ p ^ " " ^ arg); preprocess defs) + + | def :: defs -> def :: preprocess defs + +let preprocess_ast (Parse_ast.Defs defs) = Parse_ast.Defs (preprocess defs) + +let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs + +let load_file_no_check order f = convert_ast order (preprocess_ast (parse_file f)) + +let load_file order env f = + let ast = convert_ast order (preprocess_ast (parse_file f)) in + Type_check.check env ast + +let opt_just_check = ref false +let opt_ddump_tc_ast = ref false +let opt_ddump_rewrite_ast = ref None +let opt_dno_cast = ref false + +let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t = + let env = if !opt_dno_cast then Type_check.Env.no_casts env else env in + let ast, env = Type_check.check env defs in + let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in + let () = if !opt_just_check then exit 0 else () in + (ast, env) + +let opt_ddump_raw_mono_ast = ref false +let opt_dmono_analysis = ref 0 +let opt_auto_mono = ref false +let opt_mono_rewrites = ref false +let opt_dall_split_errors = ref false +let opt_dmono_continue = ref false + +let monomorphise_ast locs type_env ast = + let open Monomorphise in + let opts = { + auto = !opt_auto_mono; + debug_analysis = !opt_dmono_analysis; + rewrites = !opt_mono_rewrites; + rewrite_size_parameters = !Pretty_print_lem.opt_mwords; + all_split_errors = !opt_dall_split_errors; + continue_anyway = !opt_dmono_continue; + dump_raw = !opt_ddump_raw_mono_ast + } in + monomorphise opts locs type_env ast let open_output_with_check file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in @@ -132,6 +224,41 @@ let close_output_with_check (o, temp_file_name, file_name) = let generated_line f = Printf.sprintf "Generated by Sail from %s." f +let output_lem filename libs defs = + let generated_line = generated_line filename in + (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *) + let types_module = (filename ^ "_types") in + let monad_modules = ["Prompt_monad"; "Prompt"; "State"] in + (* if !Pretty_print_lem.opt_sequential + then ["State_monad"; "State"] + else ["Prompt_monad"; "Prompt"] in *) + let operators_module = + if !Pretty_print_lem.opt_mwords + then "Sail_operators_mwords" + else "Sail_operators_bitlists" in + (* let libs = List.map (fun lib -> lib ^ seq_suffix) libs in *) + let base_imports = [ + "Pervasives_extra"; + "Sail_instr_kinds"; + "Sail_values"; + operators_module + ] @ monad_modules + in + let ((ot,_, _) as ext_ot) = + open_output_with_check_unformatted (filename ^ "_types" ^ ".lem") in + let ((o,_, _) as ext_o) = + open_output_with_check_unformatted (filename ^ ".lem") in + (Pretty_print.pp_defs_lem + (ot, base_imports) + (o, base_imports @ (String.capitalize types_module :: libs)) + defs generated_line); + close_output_with_check ext_ot; + close_output_with_check ext_o + +let rec iterate (f : int -> unit) (n : int) : unit = + if n = 0 then () + else (f n; iterate f (n - 1)) + let output1 libpath out_arg filename defs = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with @@ -142,100 +269,13 @@ let output1 libpath out_arg filename defs = Format.fprintf o "open import Interp_ast@\n"; Format.fprintf o "open import Pervasives@\n"; Format.fprintf o "(*Supply common numeric constants at the right type to alleviate repeated calls to typeclass macro*)\n"; - Format.fprintf o "let zero : integer = integerFromNat 0\n"; - Format.fprintf o "let one : integer = integerFromNat 1\n"; - Format.fprintf o "let two : integer = integerFromNat 2\n"; - Format.fprintf o "let three : integer = integerFromNat 3\n"; - Format.fprintf o "let four : integer = integerFromNat 4\n"; - Format.fprintf o "let five : integer = integerFromNat 5\n"; - Format.fprintf o "let six : integer = integerFromNat 6\n"; - Format.fprintf o "let seven : integer = integerFromNat 7\n"; - Format.fprintf o "let eight : integer = integerFromNat 8\n"; - Format.fprintf o "let fifteen : integer = integerFromNat 15\n"; - Format.fprintf o "let sixteen : integer = integerFromNat 16\n"; - Format.fprintf o "let twenty : integer = integerFromNat 20\n"; - Format.fprintf o "let twentythree : integer = integerFromNat 23\n"; - Format.fprintf o "let twentyfour : integer = integerFromNat 24\n"; - Format.fprintf o "let thirty : integer = integerFromNat 30\n"; - Format.fprintf o "let thirtyone : integer = integerFromNat 31\n"; - Format.fprintf o "let thirtytwo : integer = integerFromNat 32\n"; - Format.fprintf o "let thirtyfive : integer = integerFromNat 35\n"; - Format.fprintf o "let thirtynine : integer = integerFromNat 39\n"; - Format.fprintf o "let forty : integer = integerFromNat 40\n"; - Format.fprintf o "let fortyseven : integer = integerFromNat 47\n"; - Format.fprintf o "let fortyeight : integer = integerFromNat 48\n"; - Format.fprintf o "let fiftyfive : integer = integerFromNat 55\n"; - Format.fprintf o "let fiftysix : integer = integerFromNat 56\n"; - Format.fprintf o "let fiftyseven : integer = integerFromNat 57\n"; - Format.fprintf o "let sixtyone : integer = integerFromNat 61\n"; - Format.fprintf o "let sixtythree : integer = integerFromNat 63\n"; - Format.fprintf o "let sixtyfour : integer = integerFromNat 64\n"; - Format.fprintf o "let onetwentyseven : integer = integerFromNat 127\n"; - Format.fprintf o "let onetwentyeight : integer = integerFromNat 128\n"; - + iterate (fun n -> Format.fprintf o "let int%i : integer = integerFromNat %i\n" (n - 1) (n - 1)) 129; Format.fprintf o "let defs = "; Pretty_print.pp_lem_defs o defs; close_output_with_check ext_o end - | Lem_out None -> - let generated_line = generated_line filename in - let types_module = (f' ^ "_embed_types") in - let tofrom_module = (f' ^ "_toFromInterp") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (f' ^ "_embed_types.lem") in - let ((o',_, _) as ext_o') = - open_output_with_check_unformatted (f' ^ "_embed.lem") in - let ((o'',_, _) as ext_o'') = - open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in - let ((o''',_, _) as ext_o''') = - open_output_with_check_unformatted (f' ^ "_toFromInterp.lem") in - (Pretty_print.pp_defs_lem - (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"]) - (o',["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values"; - String.capitalize types_module]) - (o'',["Pervasives_extra";"Sail_impl_base";"State";"Sail_values"; - String.capitalize types_module]) - (o''',["Pervasives_extra";"Sail_impl_base";"Sail_values"; - String.capitalize types_module]) - defs generated_line); - close_output_with_check ext_o; - close_output_with_check ext_o'; - close_output_with_check ext_o''; - | Lem_out (Some lib) -> - let generated_line = generated_line filename in - let types_module = (f' ^ "_embed_types") in - let tofrom_module = (f' ^ "_toFromInterp") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (f' ^ "_embed_types.lem") in - let ((o',_, _) as ext_o') = - open_output_with_check_unformatted (f' ^ "_embed.lem") in - let ((o'',_, _) as ext_o'') = - open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in - let ((o''',_, _) as ext_o''') = - open_output_with_check_unformatted (f' ^ "_toFromInterp.lem") in - (Pretty_print.pp_defs_lem - (o,["Pervasives_extra";"Sail_impl_base";"Sail_values"]) - (o',["Pervasives_extra";"Sail_impl_base";"Prompt"; - "Sail_values";String.capitalize types_module;lib]) - (o'',["Pervasives_extra";"Sail_impl_base";"State"; - "Sail_values";String.capitalize types_module;lib ^ "_sequential"]) - (o''',["Pervasives_extra";"Sail_impl_base"; - "Sail_values";String.capitalize types_module;lib]) - defs generated_line); - close_output_with_check ext_o; - close_output_with_check ext_o'; - close_output_with_check ext_o''; - close_output_with_check ext_o''' - | Ocaml_out None -> - let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in - begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"]; - close_output_with_check ext_o - end - | Ocaml_out (Some lib) -> - let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in - Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z"; "Sail_values"; lib]; - close_output_with_check ext_o - + | Lem_out libs -> + output_lem f' libs defs let output libpath out_arg files = List.iter @@ -243,3 +283,30 @@ let output libpath out_arg files = output1 libpath out_arg f defs) files +let rewrite_step defs (name,rewriter) = + let defs = rewriter defs in + let _ = match !(opt_ddump_rewrite_ast) with + | Some (f, i) -> + begin + let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in + (* output "" Lem_ast_out [filename, defs]; *) + let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in + Pretty_print_sail.pp_defs ot defs; + close_output_with_check ext_ot; + opt_ddump_rewrite_ast := Some (f, i + 1) + end + | _ -> () in + defs + +let rewrite rewriters defs = + try List.fold_left rewrite_step defs rewriters with + | Type_check.Type_error (l, err) -> + raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err)) + +let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)] +let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !Pretty_print_lem.opt_mwords x)] +let rewrite_ast_lem = 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_interpreter = rewrite Rewrites.rewrite_defs_interpreter +let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check |