diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 174 |
1 files changed, 102 insertions, 72 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index e7bf8d30..d2a86595 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -54,6 +54,10 @@ open Pretty_print_common let opt_lem_output_dir = ref None let opt_isa_output_dir = ref None let opt_coq_output_dir = ref None +let opt_alt_modules_coq = ref ([]:string list) +let opt_alt_modules2_coq = ref ([]:string list) +let opt_memo_z3 = ref false +let opt_file_out : string option ref = ref None type out_type = | Lem_out of string list @@ -69,7 +73,6 @@ let get_lexbuf f = lexbuf, in_chan let parse_file ?loc:(l=Parse_ast.Unknown) (f : string) : Parse_ast.defs = - let open Reporting in try let lexbuf, in_chan = get_lexbuf f in begin @@ -80,22 +83,29 @@ let parse_file ?loc:(l=Parse_ast.Unknown) (f : string) : Parse_ast.defs = | Parser.Error -> let pos = Lexing.lexeme_start_p lexbuf in let tok = Lexing.lexeme lexbuf in - raise (Fatal_error (Err_syntax (pos, "current token: " ^ tok))) - | Lexer.LexError(s,p) -> - raise (Fatal_error (Err_lex (p, s))) + raise (Reporting.err_syntax pos ("current token: " ^ tok)) + | Lexer.LexError (s, p) -> + raise (Reporting.err_lex p s) end with - | Sys_error err -> raise (err_general l err) + | Sys_error err -> raise (Reporting.err_general l err) (* Simple preprocessor features for conditional file loading *) module StringSet = Set.Make(String) let default_symbols = List.fold_left (fun set str -> StringSet.add str set) StringSet.empty - [ "FEATURE_IMPLICITS" ] + [ "FEATURE_IMPLICITS"; + "FEATURE_CONSTANT_TYPES"; + "FEATURE_BITVECTOR_TYPE"; + "FEATURE_UNION_BARRIER"; + ] let symbols = ref default_symbols +let have_symbol symbol = + StringSet.mem symbol !symbols + let clear_symbols () = symbols := default_symbols let cond_pragma l defs = @@ -126,32 +136,24 @@ let cond_pragma l defs = in scan defs -let astid_to_string (Ast.Id_aux (id, _)) = - match id with - | Ast.Id x | Ast.DeIid x -> x - -let parseid_to_string (Parse_ast.Id_aux (id, _)) = - match id with - | Parse_ast.Id x | Parse_ast.DeIid x -> x - -let rec realise_union_anon_rec_types orig_union arms = - match orig_union with - | Parse_ast.TD_variant (union_id, typq, _, flag) -> - begin match arms with - | [] -> [] - | arm :: arms -> - match arm with - | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_id _), _)) -> (None, arm) :: realise_union_anon_rec_types orig_union arms - | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_anon_rec (fields, id)), l)) -> - let open Parse_ast in - let record_str = "_" ^ parseid_to_string union_id ^ "_" ^ parseid_to_string id ^ "_record" in - let record_id = Id_aux (Id record_str, Generated l) in - let new_arm = Tu_aux ((Tu_ty_id ((ATyp_aux (ATyp_id record_id, Generated l)), id)), Generated l) in - let new_rec_def = DEF_type (TD_aux (TD_record (record_id, typq, fields, flag), Generated l)) in - (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms) - end - | _ -> - raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Non union type-definition passed to realise_union_anon_rec_typs") +(* We want to provide warnings for e.g. a mispelled pragma rather than + just silently ignoring them, so we have a list here of all + recognised pragmas. *) +let all_pragmas = + List.fold_left (fun set str -> StringSet.add str set) StringSet.empty + [ "define"; + "include"; + "ifdef"; + "ifndef"; + "else"; + "endif"; + "option"; + "optimize"; + "latex"; + "property"; + "counterexample"; + "suppress_warnings"; + ] let rec preprocess opts = function | [] -> [] @@ -186,7 +188,7 @@ let rec preprocess opts = function | 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 opts defs) + (Reporting.warn "" l "Skipping bad $include. No file argument."; preprocess opts defs) else if file.[0] = '"' && file.[len - 1] = '"' then let relative = match l with | Parse_ast.Range (pos, _) -> Filename.dirname (Lexing.(pos.pos_fname)) @@ -213,25 +215,20 @@ let rec preprocess opts = function include_defs @ preprocess opts defs else let help = "Make sure the filename is surrounded by quotes or angle brackets" in - (Util.warn ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess opts defs) + (Reporting.warn "" l ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess opts defs) + + | Parse_ast.DEF_pragma ("suppress_warnings", _, l) :: defs -> + begin match Reporting.simp_loc l with + | None -> () (* This shouldn't happen, but if it does just continue *) + | Some (p, _) -> Reporting.suppress_warnings_for_file p.pos_fname + end; + preprocess opts defs | Parse_ast.DEF_pragma (p, arg, l) :: defs -> + if not (StringSet.mem p all_pragmas) then + Reporting.warn "" l ("Unrecognised directive: " ^ p); Parse_ast.DEF_pragma (p, arg, l) :: preprocess opts defs - (* realise any anonymous record arms of variants *) - | Parse_ast.DEF_type (Parse_ast.TD_aux - (Parse_ast.TD_variant (id, typq, arms, flag) as union, l) - ) :: defs -> - let records_and_arms = realise_union_anon_rec_types union arms in - let rec filter_records = function [] -> [] - | Some x :: xs -> x :: filter_records xs - | None :: xs -> filter_records xs - in - let generated_records = filter_records (List.map fst records_and_arms) in - let rewritten_arms = List.map snd records_and_arms in - let rewritten_union = Parse_ast.TD_variant (id, typq, rewritten_arms, flag) in - generated_records @ (Parse_ast.DEF_type (Parse_ast.TD_aux (rewritten_union, l))) :: preprocess opts defs - | (Parse_ast.DEF_default (Parse_ast.DT_aux (Parse_ast.DT_order (_, Parse_ast.ATyp_aux (atyp, _)), _)) as def) :: defs -> begin match atyp with | Parse_ast.ATyp_inc -> symbols := StringSet.add "_DEFAULT_INC" !symbols; def :: preprocess opts defs @@ -243,12 +240,6 @@ let rec preprocess opts = function let preprocess_ast opts (Parse_ast.Defs defs) = Parse_ast.Defs (preprocess opts defs) -let load_file_no_check opts order f = Initial_check.process_ast (preprocess_ast opts (parse_file f)) - -let load_file opts order env f = - let ast = Initial_check.process_ast (preprocess_ast opts (parse_file f)) in - Type_error.check env ast - let opt_just_check = ref false let opt_ddump_tc_ast = ref false let opt_ddump_rewrite_ast = ref None @@ -261,6 +252,33 @@ let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tanno let () = if !opt_just_check then exit 0 else () in (ast, env) +let load_files ?check:(check=false) options type_envs files = + if !opt_memo_z3 then Constraint.load_digests () else (); + + let t = Profile.start () in + let parsed = List.map (fun f -> (f, parse_file f)) files in + 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 = preprocess_ast options ast in + let ast = Initial_check.process_ast ~generate:(not check) ast in + (* The separate loop measures declarations would be awkward to type check, so + move them into the definitions beforehand. *) + let ast = Rewrites.move_loop_measures ast in + Profile.finish "parsing" t; + + let t = Profile.start () in + let (ast, type_envs) = check_ast type_envs ast in + Profile.finish "type checking" t; + + if !opt_memo_z3 then Constraint.save_digests () else (); + + let out_name = match !opt_file_out with + | None when parsed = [] -> "out.sail" + | None -> fst (List.hd parsed) + | Some f -> f ^ ".sail" in + + (out_name, ast, type_envs) let open_output_with_check opt_dir file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in @@ -336,12 +354,12 @@ let output_lem filename libs type_env defs = print ol isa_lemmas; close_output_with_check ext_ol -let output_coq opt_dir filename libs defs = +let output_coq opt_dir filename alt_modules alt_modules2 libs defs = let generated_line = generated_line filename in let types_module = (filename ^ "_types") in let monad_modules = ["Sail2_prompt_monad"; "Sail2_prompt"; "Sail2_state"] in let operators_module = "Sail2_operators_mwords" in - let base_imports = [ + let base_imports_default = [ "Sail2_instr_kinds"; "Sail2_values"; "Sail2_string"; @@ -349,14 +367,25 @@ let output_coq opt_dir filename libs defs = operators_module ] @ monad_modules in + let base_imports = + (match alt_modules with + | [] -> base_imports_default + | _ -> Str.split (Str.regexp "[ \t]+") (String.concat " " alt_modules) + ) in + let alt_modules2_imports = + (match alt_modules2 with + | [] -> [] + | _ -> Str.split (Str.regexp "[ \t]+") (String.concat " " alt_modules2) + ) in let ((ot,_,_,_) as ext_ot) = open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".v") in let ((o,_,_,_) as ext_o) = open_output_with_check_unformatted opt_dir (filename ^ ".v") in (Pretty_print_coq.pp_defs_coq (ot, base_imports) - (o, base_imports @ (types_module :: libs)) - defs generated_line); + (o, base_imports @ (types_module :: libs) @ alt_modules2) + defs generated_line) + (alt_modules2 <> []); (* suppress MR and M defns if alt_modules2 present*) close_output_with_check ext_ot; close_output_with_check ext_o @@ -370,7 +399,7 @@ let output1 libpath out_arg filename type_env defs = | Lem_out libs -> output_lem f' libs type_env defs | Coq_out libs -> - output_coq !opt_coq_output_dir f' libs defs + output_coq !opt_coq_output_dir f' !opt_alt_modules_coq !opt_alt_modules2_coq libs defs let output libpath out_arg files = List.iter @@ -378,9 +407,9 @@ let output libpath out_arg files = output1 libpath out_arg f type_env defs) files -let rewrite_step n total env defs (name, rewriter) = +let rewrite_step n total (defs, env) (name, rewriter) = let t = Profile.start () in - let defs = rewriter env defs in + let defs, env = rewriter env defs in Profile.finish ("rewrite " ^ name) t; let _ = match !(opt_ddump_rewrite_ast) with | Some (f, i) -> @@ -394,22 +423,23 @@ let rewrite_step n total env defs (name, rewriter) = end | _ -> () in Util.progress "Rewrite " name n total; - defs + defs, env let rewrite env rewriters defs = let total = List.length rewriters in - try snd (List.fold_left (fun (n, defs) rw -> n + 1, rewrite_step n total env defs rw) (1, defs) rewriters) with + try snd (List.fold_left (fun (n, defsenv) rw -> n + 1, rewrite_step n total defsenv rw) (1, (defs, env)) rewriters) with | Type_check.Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) -let rewrite_ast env = rewrite env [("initial", fun _ -> Rewriter.rewrite_defs)] -let rewrite_ast_lem env = rewrite env Rewrites.rewrite_defs_lem -let rewrite_ast_coq env = rewrite env Rewrites.rewrite_defs_coq -let rewrite_ast_ocaml env = rewrite env Rewrites.rewrite_defs_ocaml -let rewrite_ast_c env ast = - ast - |> rewrite env Rewrites.rewrite_defs_c - |> rewrite env [("constant_fold", fun _ -> Constant_fold.rewrite_constant_function_calls)] +let rewrite_ast_initial env = rewrite env [("initial", fun env defs -> Rewriter.rewrite_defs defs, env)] + +let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_defs_target tgt) -let rewrite_ast_interpreter env = rewrite env Rewrites.rewrite_defs_interpreter let rewrite_ast_check env = rewrite env Rewrites.rewrite_defs_check + +let descatter type_envs ast = + let ast = Scattered.descatter ast in + let ast, type_envs = rewrite_ast_initial type_envs ast in + (* Recheck after descattering so that the internal type environments + always have complete variant types *) + Type_error.check Type_check.initial_env ast |