From a5e2b3b7411f630b6d2337402330e13862b5666a Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Mon, 14 Jan 2019 17:35:43 -0800 Subject: Add options for output directories for the lem and coq backends. --- src/process_file.ml | 48 ++++++++++++++++++++++++++++-------------------- src/process_file.mli | 3 +++ src/sail.ml | 6 ++++++ 3 files changed, 37 insertions(+), 20 deletions(-) (limited to 'src') diff --git a/src/process_file.ml b/src/process_file.ml index ca013077..38e60ff8 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -51,6 +51,9 @@ open PPrint open Pretty_print_common +let opt_lem_output_dir = ref None +let opt_coq_output_dir = ref None + type out_type = | Lem_out of string list | Coq_out of string list @@ -254,19 +257,24 @@ let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tanno (ast, env) -let open_output_with_check file_name = +let open_output_with_check opt_dir file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in let o' = Format.formatter_of_out_channel o in - (o', (o, temp_file_name, file_name)) + (o', (o, temp_file_name, opt_dir, file_name)) -let open_output_with_check_unformatted file_name = +let open_output_with_check_unformatted opt_dir file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in - (o, temp_file_name, file_name) + (o, temp_file_name, opt_dir, file_name) let always_replace_files = ref true -let close_output_with_check (o, temp_file_name, file_name) = +let close_output_with_check (o, temp_file_name, opt_dir, file_name) = let _ = close_out o in + let file_name = match opt_dir with + | None -> file_name + | Some dir -> if Sys.file_exists dir then () + else Unix.mkdir dir 0o775; + Filename.concat dir file_name in let do_replace = !always_replace_files || (not (Util.same_content_files temp_file_name file_name)) in let _ = if (not do_replace) then Sys.remove temp_file_name else Util.move_file temp_file_name file_name in @@ -275,7 +283,7 @@ 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 output_lem opt_dir 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 @@ -308,22 +316,22 @@ let output_lem filename libs defs = string "end" ] ^^ hardline 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 + let ((ot,_,_,_) as ext_ot) = + open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".lem") in + let ((o,_,_,_) as ext_o) = + open_output_with_check_unformatted opt_dir (filename ^ ".lem") in (Pretty_print.pp_defs_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) defs generated_line); close_output_with_check ext_ot; close_output_with_check ext_o; - let ((ol, _, _) as ext_ol) = - open_output_with_check_unformatted (isa_thy_name ^ ".thy") in + let ((ol,_,_,_) as ext_ol) = + open_output_with_check_unformatted opt_dir (isa_thy_name ^ ".thy") in print ol isa_lemmas; close_output_with_check ext_ol -let output_coq filename libs defs = +let output_coq opt_dir filename 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 @@ -336,10 +344,10 @@ let output_coq filename libs defs = operators_module ] @ monad_modules in - let ((ot,_, _) as ext_ot) = - open_output_with_check_unformatted (filename ^ "_types" ^ ".v") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (filename ^ ".v") 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)) @@ -355,9 +363,9 @@ let output1 libpath out_arg filename defs = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with | Lem_out libs -> - output_lem f' libs defs + output_lem !opt_lem_output_dir f' libs defs | Coq_out libs -> - output_coq f' libs defs + output_coq !opt_coq_output_dir f' libs defs let output libpath out_arg files = List.iter @@ -374,7 +382,7 @@ let rewrite_step defs (name, rewriter) = 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 + let ((ot,_,_,_) as ext_ot) = open_output_with_check_unformatted None filename in Pretty_print_sail.pp_defs ot defs; close_output_with_check ext_ot; opt_ddump_rewrite_ast := Some (f, i + 1) diff --git a/src/process_file.mli b/src/process_file.mli index 1d4d629a..2c4973bc 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -71,6 +71,9 @@ val opt_ddump_tc_ast : bool ref val opt_ddump_rewrite_ast : ((string * int) option) ref val opt_dno_cast : bool ref +val opt_lem_output_dir : (string option) ref +val opt_coq_output_dir : (string option) ref + type out_type = | Lem_out of string list (* If present, the strings are files to open in the lem backend*) | Coq_out of string list (* If present, the strings are files to open in the coq backend*) diff --git a/src/sail.ml b/src/sail.ml index 59190d15..3e89f39d 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -150,6 +150,9 @@ let options = Arg.align ([ ( "-lem", Arg.Set opt_print_lem, " output a Lem translated version of the input"); + ( "-lem_output_dir", + Arg.String (fun dir -> Process_file.opt_lem_output_dir := Some dir), + " set a custom directory to output generated Lem"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), " provide additional library to open in Lem output"); @@ -162,6 +165,9 @@ let options = Arg.align ([ ( "-coq", Arg.Set opt_print_coq, " output a Coq translated version of the input"); + ( "-coq_output_dir", + Arg.String (fun dir -> Process_file.opt_coq_output_dir := Some dir), + " set a custom directory to output generated Coq"); ( "-coq_lib", Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq), " provide additional library to open in Coq output"); -- cgit v1.2.3 From bb231219ff3d2d498d6f23f71ec1966dd58a304c Mon Sep 17 00:00:00 2001 From: Prashanth Mundkur Date: Wed, 16 Jan 2019 15:15:40 -0800 Subject: Latex: handle underscores when generating latex names. --- src/latex.ml | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) (limited to 'src') diff --git a/src/latex.ml b/src/latex.ml index 2f578f2c..56ba29ef 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -102,8 +102,7 @@ type id_category = | FunclNum of int | FunclApp of string -let replace_numbers str = - let replacements = +let number_replacements = [ ("0", "Zero"); ("1", "One"); ("2", "Two"); @@ -114,16 +113,27 @@ let replace_numbers str = ("7", "Seven"); ("8", "Eight"); ("9", "Nine") ] - in + +(* add to this as needed *) +let other_replacements = + [ ("_", "Underscore") ] + +let char_replace str replacements = List.fold_left (fun str (from, into) -> Str.global_replace (Str.regexp_string from) into str) str replacements +let replace_numbers str = + char_replace str number_replacements + +let replace_others str = + char_replace str other_replacements + let category_name = function | Function -> "fn" | Val -> "val" | Overload -> "overload" | FunclNum n -> "fcl" ^ unique_postfix n | FunclCtor (id, n) -> - let str = replace_numbers (Util.zencode_string (string_of_id id)) in + let str = replace_others (replace_numbers (Util.zencode_string (string_of_id id))) in "fcl" ^ String.sub str 1 (String.length str - 1) ^ unique_postfix n | FunclApp str -> "fcl" ^ str @@ -162,8 +172,8 @@ let latex_id id = (* If we have any other weird symbols in the id, remove them using Util.zencode_string (removing the z prefix) *) let str = Util.zencode_string str in let str = String.sub str 1 (String.length str - 1) in - (* Latex only allows letters in identifiers, so replace all numbers *) - let str = replace_numbers str in + (* Latex only allows letters in identifiers, so replace all numbers and other characters *) + let str = replace_others (replace_numbers str) in let generated = state.generated_names |> Bindings.bindings |> List.map snd |> StringSet.of_list in -- cgit v1.2.3 From 3797f0a21c142b37c6ce0728f60b231f2230c4f0 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 21 Jan 2019 14:25:56 +0000 Subject: Fix a bug with type-checking and latex generation We should maybe just make the -latex option behavior the default to avoid this kind of thing --- src/type_check.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index ee80296f..b3c691fb 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -4272,14 +4272,18 @@ let check_val_spec env (VS_aux (vs, (l, _))) = typ_print (lazy (Util.("Check val spec " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm)); let env = Env.add_extern id ext_opt env in let env = if is_cast then Env.add_cast id env else env in + let typq', typ' = expand_bind_synonyms ts_l env (typq, typ) in + (* !opt_expand_valspec controls whether the actual valspec in + the AST is expanded, the val_spec type stored in the + environment is always expanded and uses typq' and typ' *) let typq, typ = if !opt_expand_valspec then - expand_bind_synonyms ts_l env (typq, typ) + (typq', typ') else (typq, typ) in let vs = VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), ts_l), id, ext_opt, is_cast) in - (vs, id, typq, typ, env) + (vs, id, typq', typ', env) in let eff = match typ with -- cgit v1.2.3 From d2d7321afb0112142966c44a8dc4719851f20035 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 21 Jan 2019 16:19:20 +0000 Subject: Fix some issues with latex generation so manual builds again since riscv is no longer in this repository, and we use the RISC-V duopod as an example, you need to build as: make RISCV=directory manual.pdf if directory is not equal to ../../sail-riscv (which is where it would be if sail and sail-riscv are checked out in the same respository together) --- src/latex.ml | 55 +++++++++++++++++++++++++++++++++++++++---------------- src/sail.ml | 3 +++ 2 files changed, 42 insertions(+), 16 deletions(-) (limited to 'src') diff --git a/src/latex.ml b/src/latex.ml index 56ba29ef..71e0ba54 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -57,6 +57,7 @@ module StringSet = Set.Make(String);; let opt_prefix = ref "sail" let opt_directory = ref "sail_latex" +let opt_simple_val = ref true let rec unique_postfix n = if n < 0 then @@ -97,10 +98,11 @@ let rec unique_postfix n = type id_category = | Function | Val - | Overload + | Overload of int | FunclCtor of id * int | FunclNum of int | FunclApp of string + | Type let number_replacements = [ ("0", "Zero"); @@ -130,7 +132,8 @@ let replace_others str = let category_name = function | Function -> "fn" | Val -> "val" - | Overload -> "overload" + | Type -> "type" + | Overload n -> "overload" ^ unique_postfix n | FunclNum n -> "fcl" ^ unique_postfix n | FunclCtor (id, n) -> let str = replace_others (replace_numbers (Util.zencode_string (string_of_id id))) in @@ -144,7 +147,8 @@ let category_name_val = function let category_name_simple = function | Function -> "fn" | Val -> "val" - | Overload -> "overload" + | Type -> "type" + | Overload n -> "overload" | FunclNum _ -> "fcl" | FunclCtor (_, _) -> "fcl" | FunclApp _ -> "fcl" @@ -300,10 +304,10 @@ let latex_loc no_loc l = let commands = ref StringSet.empty -let doc_spec_simple (VS_val_spec(ts,id,ext,is_cast)) = - Pretty_print_sail.doc_id id ^^ space - ^^ colon ^^ space - ^^ Pretty_print_sail.doc_typschm ~simple:true ts +let doc_spec_simple (VS_aux (VS_val_spec (ts, id, ext, is_cast), _)) = + Pretty_print_sail.doc_id id ^^ space + ^^ colon ^^ space + ^^ Pretty_print_sail.doc_typschm ~simple:true ts let rec latex_command cat id no_loc ((l, _) as annot) = state.this <- Some id; @@ -319,7 +323,7 @@ let rec latex_command cat id no_loc ((l, _) as annot) = output_string chan (Pretty_print_sail.to_string doc); close_out chan; - ksprintf string "\\newcommand{\\sail%s%s}{\\phantomsection%s\\saildoc%s{" (category_name cat) (latex_id id) labelling (category_name_simple cat) + ksprintf string "\\newcommand{\\%s%s%s}{\\phantomsection%s\\saildoc%s{" !opt_prefix (category_name cat) (latex_id id) labelling (category_name_simple cat) ^^ docstring l ^^ string "}{" ^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}" (Filename.concat !opt_directory code_file) @@ -391,30 +395,47 @@ let process_pragma l command = Util.warn (Printf.sprintf "Bad latex pragma %s" (Reporting.loc_to_string l)); None +let tdef_id = function + | TD_abbrev (id, _, _) -> id + | TD_record (id, _, _, _, _) -> id + | TD_variant (id, _, _, _, _) -> id + | TD_enum (id, _, _, _) -> id + | TD_bitfield (id, _, _) -> id + let defs (Defs defs) = reset_state state; + let overload_counter = ref 0 in + let valspecs = ref IdSet.empty in let fundefs = ref IdSet.empty in + let typedefs = ref IdSet.empty in let latex_def def = match def with - | DEF_overload (id, ids) -> None - (* + | DEF_overload (id, ids) -> let doc = string (Printf.sprintf "overload %s = {%s}" (string_of_id id) (Util.string_of_list ", " string_of_id ids)) in - Some (latex_command Overload id doc (id_loc id, None)) - *) + incr overload_counter; + Some (latex_command (Overload !overload_counter) id doc (id_loc id, None)) - | DEF_spec (VS_aux (VS_val_spec (_, id, _, _) as vs, annot)) as def -> + | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), annot) as vs) as def -> valspecs := IdSet.add id !valspecs; - Some (latex_command Val id (doc_spec_simple vs) annot) + if !opt_simple_val then + Some (latex_command Val id (doc_spec_simple vs) annot) + else + Some (latex_command Val id (Pretty_print_sail.doc_spec ~comment:false vs) annot) | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, _), _)]), annot)) as def -> fundefs := IdSet.add id !fundefs; Some (latex_command Function id (Pretty_print_sail.doc_def def) annot) + | DEF_type (TD_aux (tdef, annot)) as def -> + let id = tdef_id tdef in + typedefs := IdSet.add id !typedefs; + Some (latex_command Type id (Pretty_print_sail.doc_def def) annot) + | DEF_fundef (FD_aux (FD_function (_, _, _, funcls), annot)) as def -> Some (latex_funcls def funcls) @@ -442,7 +463,7 @@ let defs (Defs defs) = identifiers then outputs the correct mangled command. *) let id_command cat ids = sprintf "\\newcommand{\\%s%s}[1]{\n " !opt_prefix (category_name cat) - ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\sail%s%s}{}" (string_of_id id) (category_name cat) (latex_id id)) + ^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s%s%s}{}" (string_of_id id) !opt_prefix (category_name cat) (latex_id id)) (IdSet.elements ids) ^ "}" |> string @@ -459,5 +480,7 @@ let defs (Defs defs) = ^^ separate (twice hardline) [id_command Val !valspecs; ref_command Val !valspecs; id_command Function !fundefs; - ref_command Function !fundefs] + ref_command Function !fundefs; + id_command Type !typedefs; + ref_command Type !typedefs] ^^ hardline diff --git a/src/sail.ml b/src/sail.ml index 3e89f39d..a5cac041 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -112,6 +112,9 @@ let options = Arg.align ([ ( "-latex", Arg.Tuple [Arg.Set opt_print_latex; Arg.Clear Type_check.opt_expand_valspec ], " pretty print the input to latex"); + ( "-latex_full_valspecs", + Arg.Clear Latex.opt_simple_val, + " print full valspecs in latex output latex"); ( "-c", Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input"); -- cgit v1.2.3 From d34329753b1e8faa32a7c95ac085733555c16749 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 21 Jan 2019 18:37:24 +0000 Subject: Add output directory option for generated Isabelle auxiliary theories --- src/process_file.ml | 11 ++++++----- src/process_file.mli | 1 + src/sail.ml | 3 +++ 3 files changed, 10 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/process_file.ml b/src/process_file.ml index 38e60ff8..094b0ecb 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -52,6 +52,7 @@ open PPrint 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 type out_type = @@ -283,7 +284,7 @@ let close_output_with_check (o, temp_file_name, opt_dir, file_name) = let generated_line f = Printf.sprintf "Generated by Sail from %s." f -let output_lem opt_dir filename libs defs = +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 @@ -317,9 +318,9 @@ let output_lem opt_dir filename libs defs = ] ^^ hardline in let ((ot,_,_,_) as ext_ot) = - open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".lem") in + open_output_with_check_unformatted !opt_lem_output_dir (filename ^ "_types" ^ ".lem") in let ((o,_,_,_) as ext_o) = - open_output_with_check_unformatted opt_dir (filename ^ ".lem") in + open_output_with_check_unformatted !opt_lem_output_dir (filename ^ ".lem") in (Pretty_print.pp_defs_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) @@ -327,7 +328,7 @@ let output_lem opt_dir filename libs defs = close_output_with_check ext_ot; close_output_with_check ext_o; let ((ol,_,_,_) as ext_ol) = - open_output_with_check_unformatted opt_dir (isa_thy_name ^ ".thy") in + open_output_with_check_unformatted !opt_isa_output_dir (isa_thy_name ^ ".thy") in print ol isa_lemmas; close_output_with_check ext_ol @@ -363,7 +364,7 @@ let output1 libpath out_arg filename defs = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with | Lem_out libs -> - output_lem !opt_lem_output_dir f' libs defs + output_lem f' libs defs | Coq_out libs -> output_coq !opt_coq_output_dir f' libs defs diff --git a/src/process_file.mli b/src/process_file.mli index 2c4973bc..e209c829 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -72,6 +72,7 @@ val opt_ddump_rewrite_ast : ((string * int) option) ref val opt_dno_cast : bool ref val opt_lem_output_dir : (string option) ref +val opt_isa_output_dir : (string option) ref val opt_coq_output_dir : (string option) ref type out_type = diff --git a/src/sail.ml b/src/sail.ml index a5cac041..920542bc 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -156,6 +156,9 @@ let options = Arg.align ([ ( "-lem_output_dir", Arg.String (fun dir -> Process_file.opt_lem_output_dir := Some dir), " set a custom directory to output generated Lem"); + ( "-isa_output_dir", + Arg.String (fun dir -> Process_file.opt_isa_output_dir := Some dir), + " set a custom directory to output generated Isabelle auxiliary theories"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), " provide additional library to open in Lem output"); -- cgit v1.2.3 From 2c81fff611c458fe04b2de2045247bdc77f8f80a Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 21 Jan 2019 19:02:46 +0000 Subject: Update manual snapshot and add basic sail -latex documentation --- src/type_check.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index b3c691fb..1b6efa46 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1243,7 +1243,7 @@ let prove_z3 env (NC_aux (_, l) as nc) = | Constraint.Sat -> typ_debug (lazy "sat"); false | Constraint.Unknown -> typ_debug (lazy "unknown"); false -let solve env (Nexp_aux (_, l) as nexp) = +let solve env (Nexp_aux (_, l) as nexp) = typ_print (lazy (Util.("Solve " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_nexp nexp ^ " = ?")); match nexp with @@ -1255,6 +1255,8 @@ let solve env (Nexp_aux (_, l) as nexp) = let constr = List.fold_left nc_and (nc_eq (nvar (mk_kid "solve#")) nexp) (Env.get_constraints env) in Constraint.solve_z3 l vars constr (mk_kid "solve#") + + let prove env nc = typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc)); let (NC_aux (nc_aux, _) as nc) = Env.expand_constraint_synonyms env nc in -- cgit v1.2.3 From 63a3cdcd18972cdc2b6fa24d6a2deb5cae7549cc Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 22 Jan 2019 03:08:46 +0000 Subject: Make sure we optimize constrained union constructors --- src/c_backend.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/c_backend.ml b/src/c_backend.ml index 65702764..f02cdb9c 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -1399,9 +1399,11 @@ let compile_type_def ctx (TD_aux (type_def, _)) = CTD_struct (id, Bindings.bindings ctors), { ctx with records = Bindings.add id ctors ctx.records } - | TD_variant (id, _, _, tus, _) -> + | TD_variant (id, _, typq, tus, _) -> let compile_tu = function - | Tu_aux (Tu_ty_id (typ, id), _) -> ctyp_of_typ ctx typ, id + | Tu_aux (Tu_ty_id (typ, id), _) -> + let ctx = { ctx with local_env = add_typquant (id_loc id) typq ctx.local_env } in + ctyp_of_typ ctx typ, id in let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in CTD_variant (id, Bindings.bindings ctus), -- cgit v1.2.3 From 8c457ba46217978c1845ae9d6ebb0970e9b30cb9 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 22 Jan 2019 13:22:30 +0000 Subject: Make sure there is an ocaml representation for optimized memory read for RISC-V --- src/sail_lib.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src') diff --git a/src/sail_lib.ml b/src/sail_lib.ml index c0bf80fa..d1a21b73 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -508,6 +508,13 @@ let read_ram (addr_size, data_size, hex_ram, addr) = Bytes.iter (fun byte -> vector := (byte_of_int (int_of_char byte)) @ !vector) bytes; !vector +let fast_read_ram (data_size, addr) = + let addr = uint addr in + let bytes = read_mem_bytes addr (Big_int.to_int data_size) in + let vector = ref [] in + Bytes.iter (fun byte -> vector := (byte_of_int (int_of_char byte)) @ !vector) bytes; + !vector + let tag_ram = (ref Mem.empty : (bool Mem.t) ref);; let write_tag_bool (addr, tag) = -- cgit v1.2.3 From 8258b81bf1485e3133fb4351413ed1f554717f43 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 22 Jan 2019 18:04:16 +0000 Subject: Add a pragma for unrolling recursive functions For example in RISC-V for the translation table walk: $optimize unroll 2 val walk32 ... function walk32 ... would create two extra copies of the walk_32 function, walk_32_unroll_1 and walk_32_unroll_2, with only walk_32_unroll_2 being recursive. Currently we only support the case where we have $optimize unroll, directly followed by a valspec, then a function, but this should be generalised in future. This optimization nearly doubles the performance of RISC-V It is implemented using a new Optimize.recheck rewrite that replaces the ordinary recheck_defs pass. It uses a new typechecker check_with_envs function that allows re-writes to utilise intermediate typechecking environments to minimize the amount of AST checking that occurs, for performance reasons. Note that older Sail versions including the current OPAM release will complain about the optimize pragma, so this cannot be used until they become up to date with this change. --- src/ast_util.ml | 9 +++-- src/ast_util.mli | 2 ++ src/c_backend.ml | 3 ++ src/optimize.ml | 100 +++++++++++++++++++++++++++++++++++++++++++++++++++++ src/rewrites.ml | 2 +- src/type_check.ml | 8 +++++ src/type_check.mli | 4 +++ 7 files changed, 124 insertions(+), 4 deletions(-) create mode 100644 src/optimize.ml (limited to 'src') 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 -- cgit v1.2.3 From c1e0bc6530bcc18d2c3798894b58855ed1231719 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 25 Jan 2019 15:47:41 +0000 Subject: Fix solution finding using SMT by looking for the right variable --- src/constraint.ml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/constraint.ml b/src/constraint.ml index 7ead0cc8..b7e3cb47 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -131,16 +131,17 @@ let to_smt l vars constr = | _ -> raise (Reporting.err_unreachable l __POS__ "Tried to pass Type or Order kind to SMT function") in - var_decs l vars, smt_constraint constr + var_decs l vars, smt_constraint constr, smt_var -let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string = - let variables, problem = to_smt l vars constr in +let smtlib_of_constraints ?get_model:(get_model=false) l vars constr : string * (kid -> sexpr) = + let variables, problem, var_map = to_smt l vars constr in "(push)\n" ^ variables ^ "\n" ^ pp_sexpr (sfun "define-fun" [Atom "constraint"; List []; Atom "Bool"; problem]) ^ "\n(assert constraint)\n(check-sat)" ^ (if get_model then "\n(get-model)" else "") - ^ "\n(pop)" + ^ "\n(pop)", + var_map type smt_result = Unknown | Sat | Unsat @@ -183,7 +184,7 @@ let save_digests () = let call_z3' l vars constraints : smt_result = let problems = [constraints] in - let z3_file = smtlib_of_constraints l vars constraints in + let z3_file, _ = smtlib_of_constraints l vars constraints in (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *) @@ -230,9 +231,11 @@ let call_z3 l vars constraints = result let rec solve_z3 l vars constraints var = - let z3_file = smtlib_of_constraints ~get_model:true l vars constraints in + let z3_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in + let z3_var = pp_sexpr (smt_var var) in - (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *) + (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); + prerr_endline ("Solving for " ^ z3_var); *) let rec input_all chan = try @@ -250,7 +253,7 @@ let rec solve_z3 l vars constraints var = let z3_output = String.concat " " (input_all z3_chan) in let _ = Unix.close_process_in z3_chan in Sys.remove input_file; - let regexp = {|(define-fun v|} ^ Util.zencode_string (string_of_kid var) ^ {| () Int[ ]+\([0-9]+\))|} in + let regexp = {|(define-fun |} ^ z3_var ^ {| () Int[ ]+\([0-9]+\))|} in try let _ = Str.search_forward (Str.regexp regexp) z3_output 0 in let result = Big_int.of_string (Str.matched_group 1 z3_output) in -- cgit v1.2.3 From e3266e1ce5463d57f3d35c89dc811348f76c9e41 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 25 Jan 2019 15:48:57 +0000 Subject: Monomorphisation: update a built-in name --- src/monomorphise.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 4bb1876c..76a48cd7 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3418,7 +3418,7 @@ let rec sets_from_assert e = match e with | E_app (Id_aux (Id "or_bool",_),[e1;e2]) -> aux e1 @ aux e2 - | E_app (Id_aux (Id "eq_atom",_), + | E_app (Id_aux (Id "eq_int",_), [E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); E_aux (E_lit (L_aux (L_num i,_)),_)]) -> (check_kid kid; [i]) @@ -4034,7 +4034,7 @@ let rec extract_value_from_guard var (E_aux (e,_)) = match e with | E_app (op, ([E_aux (E_id var',_); E_aux (E_lit (L_aux (L_num i,_)),_)] | [E_aux (E_lit (L_aux (L_num i,_)),_); E_aux (E_id var',_)])) - when string_of_id op = "eq_atom" && Id.compare var var' == 0 -> + when string_of_id op = "eq_int" && Id.compare var var' == 0 -> Some i | E_app (op, [e1;e2]) when string_of_id op = "and_bool" -> (match extract_value_from_guard var e1 with @@ -4047,7 +4047,8 @@ let fill_in_type env typ = let subst = KidSet.fold (fun kid subst -> match Env.get_typ_var kid env with | K_type - | K_order -> subst + | K_order + | K_bool -> subst | K_int -> (match solve env (nvar kid) with | None -> subst @@ -4102,7 +4103,7 @@ let add_bitvector_casts (Defs defs) = | E_app (op, ([E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); y] | [y; E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_)])) - when string_of_id op = "eq_atom" -> + when string_of_id op = "eq_int" -> (match destruct_atom_nexp (env_of y) (typ_of y) with | Some (Nexp_aux (Nexp_constant i,_)) -> [(kid,i)] | _ -> []) -- cgit v1.2.3 From b826df25ee3ec624483b8486af211e6d1e965589 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Mon, 28 Jan 2019 21:21:16 +0000 Subject: Lem: Be more careful about nexps occurring in the function signature Don't ask Z3 to simplify them, as flow typing might lead to different results in different if-branches, for example, leading to type errors in Lem. --- src/pretty_print_lem.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 5c67f93a..c0af581a 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -349,14 +349,14 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) = let mk_typ nexp = Some (Typ_aux (Typ_app (id, [A_aux (A_nexp nexp,Parse_ast.Unknown);ord;typ']),a)) in - match Type_check.solve env size with - | Some n -> mk_typ (nconstant n) - | None -> - let is_equal nexp = - prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) - in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with - | nexp -> mk_typ nexp - | exception Not_found -> None + let is_equal nexp = + prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown)) + in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with + | nexp -> mk_typ nexp + | exception Not_found -> + match Type_check.solve env size with + | Some n -> mk_typ (nconstant n) + | None -> None end | _ -> None -- cgit v1.2.3 From 60164a9a221ed6566f1067100dbea2ec828b47d2 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 29 Jan 2019 16:50:05 +0000 Subject: Improve generation of initial register state Define initial values for record types once instead of repeating them in the initial register state. --- src/state.ml | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/state.ml b/src/state.ml index c9a47b06..fe1cebe7 100644 --- a/src/state.ml +++ b/src/state.ml @@ -135,20 +135,20 @@ let generate_initial_regstate defs = let typ_subst_typquant tq args typ = List.fold_left2 typ_subst_quant_item typ (quant_items tq) args in - let add_typ_init_val vals = function + let add_typ_init_val (defs', vals) = function | TD_enum (id, _, id1 :: _, _) -> (* Choose the first value of an enumeration type as default *) - Bindings.add id (fun _ -> string_of_id id1) vals + (defs', Bindings.add id (fun _ -> string_of_id id1) vals) | TD_variant (id, _, tq, (Tu_aux (Tu_ty_id (typ1, id1), _)) :: _, _) -> (* Choose the first variant of a union type as default *) let init_val args = let typ1 = typ_subst_typquant tq args typ1 in string_of_id id1 ^ " (" ^ lookup_init_val vals typ1 ^ ")" in - Bindings.add id init_val vals + (defs', Bindings.add id init_val vals) | TD_abbrev (id, tq, A_aux (A_typ typ, _)) -> let init_val args = lookup_init_val vals (typ_subst_typquant tq args typ) in - Bindings.add id init_val vals + (defs', Bindings.add id init_val vals) | TD_record (id, _, tq, fields, _) -> let init_val args = let init_field (typ, id) = @@ -157,16 +157,21 @@ let generate_initial_regstate defs = in "struct { " ^ (String.concat ", " (List.map init_field fields)) ^ " }" in - Bindings.add id init_val vals + let def_name = "initial_" ^ string_of_id id in + if quant_items tq = [] && not (is_defined defs def_name) then + (defs' @ ["let " ^ def_name ^ " : " ^ string_of_id id ^ " = " ^ init_val []], + Bindings.add id (fun _ -> def_name) vals) + else (defs', Bindings.add id init_val vals) | TD_bitfield (id, typ, _) -> - Bindings.add id (fun _ -> lookup_init_val vals typ) vals - | _ -> vals + (defs', Bindings.add id (fun _ -> lookup_init_val vals typ) vals) + | _ -> (defs', vals) in - let init_vals = List.fold_left (fun vals def -> match def with - | DEF_type (TD_aux (td, _)) -> add_typ_init_val vals td - | _ -> vals) Bindings.empty defs + let (init_defs, init_vals) = List.fold_left (fun inits def -> match def with + | DEF_type (TD_aux (td, _)) -> add_typ_init_val inits td + | _ -> inits) ([], Bindings.empty) defs in let init_reg (typ, id) = string_of_id id ^ " = " ^ lookup_init_val init_vals typ in + init_defs @ ["let initial_regstate : regstate = struct { " ^ (String.concat ", " (List.map init_reg registers)) ^ " }"] with | _ -> [] (* Do not generate an initial register state if anything goes wrong *) -- cgit v1.2.3