From d87d4ad3a6d2ec2804cb7b20128fecb6d9df4e6e Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 25 Jan 2018 00:30:24 +0000 Subject: Add simple conditional processing and file include Can now use C-style include declarations to include files within other sail files. This is done in such a way that all the location information is preserved in error messages. As an example: $include "aarch64/prelude.sail" $define SYM $ifndef SYM $include <../util.sail> $endif would include the file aarch64/prelude.sail relative to the file where the include is contained. It then defines a symbol SYM and includes another file if it is not defined. The <../util.sail> include will be accessed relative to $SAIL_DIR/lib, so $SAIL_DIR/lib/../util.sail in this case. This can be used with the standard C trick of $ifndef ONCE $define ONCE val f : unit -> unit $endif so no matter how many sail files include the above file, the valspec for f will only appear once. Currently we just have $include, $define, $ifdef and $ifndef (with $else and $endif). We're using $ rather than # because # is already used in internal identifiers, although this could be switched. --- editors/sail2-mode.el | 2 +- src/initial_check.ml | 4 ++- src/lexer.mll | 5 ++- src/parse_ast.ml | 1 + src/parser.mly | 4 +++ src/process_file.ml | 91 +++++++++++++++++++++++++++++++++++++++++++++++++-- src/process_file.mli | 1 + src/sail.ml | 1 + src/util.ml | 2 ++ src/util.mli | 2 ++ 10 files changed, 108 insertions(+), 5 deletions(-) diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el index e17b1a4f..eb3e0fe6 100644 --- a/editors/sail2-mode.el +++ b/editors/sail2-mode.el @@ -19,7 +19,7 @@ '("vector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string" "bits")) (defconst sail2-special - '("_prove")) + '("_prove" "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif")) (defconst sail2-font-lock-keywords `((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face) diff --git a/src/initial_check.ml b/src/initial_check.ml index 87adb290..16df4648 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -826,9 +826,11 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out | Parse_ast.DEF_reg_dec(dec) -> let d = to_ast_dec envs dec in ((Finished(DEF_reg_dec(d))),envs),partial_defs + | Parse_ast.DEF_pragma (_, _, l) -> + typ_error l "Encountered preprocessor directive in initial check" None None None | Parse_ast.DEF_internal_mutrec _ -> (* Should never occur because of remove_mutrec *) - typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None + typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,l)) -> (match sd with | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) -> diff --git a/src/lexer.mll b/src/lexer.mll index 21b70c5f..77fba70b 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -186,9 +186,10 @@ let alphanum = letter|digit let startident = letter|'_' let ident = alphanum|['_''\'''#'] let tyvar_start = '\'' -let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''@''^''|'] +let oper_char = ['!''%''&''*''+''-''.''/'':''<''=''>''@''^''|'] let operator = (oper_char+ ('_' ident)?) let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit) +let lchar = [^'\n'] rule token = parse | ws @@ -236,6 +237,8 @@ rule token = parse | "//" { line_comment (Lexing.lexeme_start_p lexbuf) lexbuf; token lexbuf } | "/*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf } | "*/" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) } + | "$" (ident+ as i) (lchar* as f) "\n" + { Lexing.new_line lexbuf; Pragma(i, String.trim f) } | "infix" ws (digit as p) ws (operator as op) { operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators; Fixity (Infix, Big_int.of_string (Char.escaped p), op) } diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 362333f3..5eb8038a 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -507,6 +507,7 @@ def = (* Top-level definition *) | DEF_default of default_typing_spec (* default kind and type assumptions *) | DEF_scattered of scattered_def (* scattered definition *) | DEF_reg_dec of dec_spec (* register declaration *) + | DEF_pragma of string * string * l | DEF_internal_mutrec of fundef list diff --git a/src/parser.mly b/src/parser.mly index b11b4b61..32ee3368 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -182,6 +182,8 @@ let rec desugar_rchain chain s e = %token Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l %token Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r +%token Pragma + %token Fixity %start file @@ -1246,6 +1248,8 @@ def: { DEF_default $1 } | Mutual Lcurly fun_def_list Rcurly { DEF_internal_mutrec $3 } + | Pragma + { DEF_pragma (fst $1, snd $1, loc $startpos $endpos) } defs_list: | def diff --git a/src/process_file.ml b/src/process_file.ml index ec280fbf..cb8c8011 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -76,12 +76,99 @@ let parse_file (f : string) : Parse_ast.defs = | 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 (parse_file f) +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 (parse_file f) in + let ast = convert_ast order (preprocess_ast (parse_file f)) in Type_check.check env ast let opt_just_check = ref false diff --git a/src/process_file.mli b/src/process_file.mli index 82fe1cf7..d8094682 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -50,6 +50,7 @@ val parse_file : string -> Parse_ast.defs val convert_ast : Ast.order -> Parse_ast.defs -> unit Ast.defs +val preprocess_ast : Parse_ast.defs -> Parse_ast.defs val check_ast: Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t val monomorphise_ast : ((string * int) * string) list -> Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs diff --git a/src/sail.ml b/src/sail.ml index b819350b..d5ef684b 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -193,6 +193,7 @@ let load_files type_envs files = let ast = List.fold_right (fun (_, Parse_ast.Defs ast_nodes) (Parse_ast.Defs later_nodes) -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in + let ast = Process_file.preprocess_ast ast in let ast = convert_ast Ast_util.inc_ord ast in let (ast, type_envs) = check_ast type_envs ast in diff --git a/src/util.ml b/src/util.ml index 94bbc6dc..6d4b3726 100644 --- a/src/util.ml +++ b/src/util.ml @@ -413,3 +413,5 @@ let zchar c = let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (string_to_list str)) let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (string_to_list str)) + +let warn str = prerr_endline (("Warning" |> yellow |> clear) ^ ": " ^ str) diff --git a/src/util.mli b/src/util.mli index 8fcf68be..c9eae02f 100644 --- a/src/util.mli +++ b/src/util.mli @@ -240,5 +240,7 @@ val cyan : string -> string val blue : string -> string val clear : string -> string +val warn : string -> unit + val zencode_string : string -> string val zencode_upper_string : string -> string -- cgit v1.2.3