From 68d109416999f31bf0674516e69d56ea9995be0d Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 26 Oct 2017 14:58:49 +0100 Subject: Updated ocaml backend so tracing instrumentation is optional. Cleaned up the option list in sail.ml --- src/ocaml_backend.ml | 45 ++++++++++++++++++++++++++++---------- src/sail.ml | 61 ++++++++++++++++++++++++++-------------------------- 2 files changed, 64 insertions(+), 42 deletions(-) (limited to 'src') diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 384d8109..f103f818 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -3,6 +3,9 @@ open Ast_util open PPrint open Type_check +(* Option to turn tracing features on or off *) +let opt_trace_ocaml = ref false + type ctx = { register_inits : tannot exp list; externs : id Bindings.t; @@ -240,7 +243,10 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) = match Env.lookup_id id (env_of exp) with | Local (Immutable, _) | Unbound -> zencode ctx id | Enum _ | Union _ -> zencode_upper ctx id - | Register _ -> parens (string ("trace \"Read: " ^ string_of_id id ^ "\";") ^^ space ^^ bang ^^ zencode ctx id) + | Register _ -> + if !opt_trace_ocaml + then parens (string ("trace \"Read: " ^ string_of_id id ^ "\";") ^^ space ^^ bang ^^ zencode ctx id) + else bang ^^ zencode ctx id | Local (Mutable, _) -> bang ^^ zencode ctx id end | E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps) @@ -254,8 +260,12 @@ and ocaml_assignment ctx (LEXP_aux (lexp_aux, _) as lexp) exp = | Register typ -> let var = gensym () in let traced_exp = - parens (separate space [string "let"; var; equals; ocaml_atomic_exp ctx exp; string "in"; - string "trace_write" ^^ space ^^ string_lit (string_of_id id) ^^ space ^^ parens (ocaml_string_typ (Rewriter.simple_typ typ) var) ^^ semi; var]) + if !opt_trace_ocaml then + let var = gensym () in + let str_typ = parens (ocaml_string_typ (Rewriter.simple_typ typ) var) in + parens (separate space [string "let"; var; equals; ocaml_atomic_exp ctx exp; string "in"; + string "trace_write" ^^ space ^^ string_lit (string_of_id id) ^^ space ^^ str_typ ^^ semi; var]) + else ocaml_atomic_exp ctx exp in separate space [zencode ctx id; string ":="; traced_exp] | _ -> separate space [zencode ctx id; string ":="; ocaml_exp ctx exp] @@ -331,22 +341,36 @@ let ocaml_funcls ctx = in (arg_sym, string_of_arg, ret_sym, string_of_ret) in + let sail_call id arg_sym pat_sym ret_sym = + if !opt_trace_ocaml + then separate space [string "sail_trace_call"; string_lit (string_of_id id); parens (arg_sym ^^ space ^^ pat_sym); ret_sym] + else separate space [string "sail_call"] + in + let ocaml_funcl call string_of_arg string_of_ret = + if !opt_trace_ocaml + then (call ^^ twice hardline ^^ string_of_arg ^^ twice hardline ^^ string_of_ret) + else call + in function | [] -> failwith "Ocaml: empty function" | [FCL_aux (FCL_Funcl (id, pat, exp),_)] -> let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in let pat_sym = gensym () in - let annot_pat = parens (separate space [parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1); string "as"; pat_sym]) in + let annot_pat = + let pat = parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1) in + if !opt_trace_ocaml + then parens (separate space [pat; string "as"; pat_sym]) + else pat + in let call_header = function_header () in let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in let call = separate space [call_header; zencode ctx id; annot_pat; colon; ocaml_typ ctx typ2; equals; - string "sail_trace_call"; string_lit (string_of_id id); parens (arg_sym ^^ space ^^ pat_sym); ret_sym; - string "(fun r ->"] + sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] ^//^ ocaml_exp ctx exp ^^ rparen in - call ^^ twice hardline ^^ string_of_arg ^^ twice hardline ^^ string_of_ret + ocaml_funcl call string_of_arg string_of_ret | funcls -> let id = funcls_id funcls in let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in @@ -355,12 +379,11 @@ let ocaml_funcls ctx = let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in let call = separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1); equals; - string "sail_trace_call"; string_lit (string_of_id id); parens (arg_sym ^^ space ^^ pat_sym); ret_sym; - string "(fun r ->"] + sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"] ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls) ^^ rparen in - call ^^ twice hardline ^^ string_of_arg ^^ twice hardline ^^ string_of_ret + ocaml_funcl call string_of_arg string_of_ret let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) = ocaml_funcls ctx funcls @@ -391,7 +414,6 @@ let rec ocaml_enum ctx = function (* We generate a string_of_X ocaml function for each type X, to be used for debugging purposes *) - let ocaml_def_end = string ";;" ^^ twice hardline let ocaml_string_of_enum ctx id ids = @@ -491,6 +513,7 @@ let ocaml_main spec = separate space [string "let"; string "()"; equals] ^//^ (string "Random.self_init ();" ^/^ string "load_elf ();" + ^/^ string (if !opt_trace_ocaml then "Sail_lib.opt_trace := true;" else "Sail_lib.opt_trace := false;") ^/^ string "initialize_registers ();" ^/^ string "Printexc.record_backtrace true;" ^/^ string "zmain ()") diff --git a/src/sail.ml b/src/sail.ml index 9c447f36..8a70cb70 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -56,39 +56,35 @@ let opt_libs_lem = ref ([]:string list) let opt_libs_ocaml = ref ([]:string list) let opt_file_arguments = ref ([]:string list) let opt_mono_split = ref ([]:((string * int) * string) list) + let options = Arg.align ([ ( "-o", Arg.String (fun f -> opt_file_out := Some f), " select output filename prefix"); + ( "-ocaml", + Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen], + " output an OCaml translated version of the input"); + ( "-ocaml_trace", + Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml], + " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml"); + ( "-ocaml_lib", + Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml), + " provide additional library to open in OCaml output"); ( "-lem_ast", Arg.Set opt_print_lem_ast, " output a Lem AST representation of the input"); ( "-lem", Arg.Set opt_print_lem, " output a Lem translated version of the input"); - ( "-ocaml", - Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen], - " output an OCaml translated version of the input"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), " provide additional library to open in Lem output"); - ( "-ocaml_lib", - Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml), - " provide additional library to open in OCaml output"); ( "-lem_sequential", Arg.Set Process_file.opt_lem_sequential, " use sequential state monad for Lem output"); ( "-lem_mwords", Arg.Set Process_file.opt_lem_mwords, " use native machine word library for Lem output"); -(* - ( "-i", - Arg.String (fun l -> lib := l::!lib), - " treat this file as input only and generate no output for it"); -*) - ( "-verbose", - Arg.Set opt_print_verbose, - " (debug) pretty-print the input to standard output"); ( "-mono-split", Arg.String (fun s -> let l = Util.split_on_char ':' s in @@ -96,39 +92,42 @@ let options = Arg.align ([ | [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split | _ -> raise (Arg.Bad (s ^ " not of form ::"))), ":: to case split for monomorphisation"); - ( "-ddump_raw_mono_ast", - Arg.Set opt_ddump_raw_mono_ast, - " (debug) dump the monomorphised ast before type-checking"); + ( "-memo_z3", + Arg.Set opt_memo_z3, + " memoize calls to z3, improving performance when typechecking repeatedly"); + ( "-undefined_gen", + Arg.Set Initial_check.opt_undefined_gen, + " generate undefined_type functions for types in the specification"); + ( "-no_effects", + Arg.Set Type_check.opt_no_effects, + " (experimental) turn off effect checking"); ( "-new_parser", Arg.Set Process_file.opt_new_parser, " (experimental) use new parser"); + ( "-convert", + Arg.Set opt_convert, + " (experimental) convert sail to new syntax for use with -new_parser"); ( "-just_check", Arg.Set opt_just_check, " (experimental) terminate immediately after typechecking"); - ( "-convert", - Arg.Set opt_convert, - " Convert sail to new syntax"); - ( "-memo_z3", - Arg.Set opt_memo_z3, - " Memoize calls to z3"); + ( "-ddump_raw_mono_ast", + Arg.Set opt_ddump_raw_mono_ast, + " (debug) dump the monomorphised ast before type-checking"); + ( "-verbose", + Arg.Set opt_print_verbose, + " (debug) pretty-print the input to standard output"); ( "-ddump_tc_ast", Arg.Set opt_ddump_tc_ast, " (debug) dump the typechecked ast to stdout"); ( "-ddump_rewrite_ast", Arg.String (fun l -> opt_ddump_rewrite_ast := Some (l, 0)), - " (debug) dump the ast after each rewriting step to _.lem"); + " (debug) dump the ast after each rewriting step to _.lem"); ( "-dtc_verbose", Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity), - " (debug) verbose typechecker output: 0 is silent"); + " (debug) verbose typechecker output: 0 is silent"); ( "-dno_cast", Arg.Set opt_dno_cast, " (debug) typecheck without any implicit casting"); - ( "-no_effects", - Arg.Set Type_check.opt_no_effects, - " turn off effect checking"); - ( "-undefined_gen", - Arg.Set Initial_check.opt_undefined_gen, - " generate undefined_type functions for types in the specification"); ( "-v", Arg.Set opt_print_version, " print version"); -- cgit v1.2.3 From 9767dedc63482b77eec644c6e68d06310cbbd521 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 27 Oct 2017 20:39:49 +0100 Subject: Fixed some ocaml backend related bugs --- src/ocaml_backend.ml | 17 +++++++++++++---- src/type_check.ml | 10 ++++++---- 2 files changed, 19 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index f103f818..feadb2d5 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -122,7 +122,7 @@ let ocaml_lit (L_aux (lit_aux, _)) = | L_num n -> parens (string "big_int_of_int" ^^ space ^^ string (string_of_int n)) | L_undef -> failwith "undefined should have been re-written prior to ocaml backend" | L_string str -> string_lit str - | L_real str -> parens (string "Num.num_of_string" ^^ space ^^ dquotes (string (String.escaped str))) + | L_real str -> parens (string "real_of_string" ^^ space ^^ dquotes (string (String.escaped str))) | _ -> string "LIT" let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) = @@ -202,11 +202,20 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = ^/^ string "in" ^/^ string "loop ()" | E_lit _ | E_list _ | E_id _ | E_tuple _ -> ocaml_atomic_exp ctx exp - | E_for (id, exp_from, exp_to, exp_step, _, exp_body) -> + | E_for (id, exp_from, exp_to, exp_step, ord, exp_body) -> let loop_var = separate space [string "let"; zencode ctx id; equals; string "ref"; ocaml_atomic_exp ctx exp_from; string "in"] in - let loop_mod = string "add_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step in + let loop_mod = + match ord with + | Ord_aux (Ord_inc, _) -> string "add_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step + | Ord_aux (Ord_dec, _) -> string "sub_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step + in + let loop_compare = + match ord with + | Ord_aux (Ord_inc, _) -> string "le_big_int" + | Ord_aux (Ord_dec, _) -> string "gt_big_int" + in let loop_body = - separate space [string "if"; zencode ctx id; string "<="; ocaml_atomic_exp ctx exp_to] + separate space [string "if"; loop_compare; zencode ctx id; ocaml_atomic_exp ctx exp_to] ^/^ separate space [string "then"; parens (ocaml_atomic_exp ctx exp_body ^^ semi ^^ space ^^ string "loop" ^^ space ^^ parens loop_mod)] ^/^ string "else ()" diff --git a/src/type_check.ml b/src/type_check.ml index 751e70e5..6c5205fe 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2644,9 +2644,9 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = annot_exp (E_loop (loop_type, checked_cond, checked_body)) unit_typ | E_for (v, f, t, step, ord, body) -> begin - let f, t = match ord with - | Ord_aux (Ord_inc, _) -> f, t - | Ord_aux (Ord_dec, _) -> t, f (* reverse direction for downto loop *) + let f, t, is_dec = match ord with + | Ord_aux (Ord_inc, _) -> f, t, false + | Ord_aux (Ord_dec, _) -> t, f, true (* reverse direction to typechecking downto as upto loop *) in let inferred_f = irule infer_exp env f in let inferred_t = irule infer_exp env t in @@ -2668,7 +2668,9 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let env = Env.add_constraint (nc_and (nc_lteq l1 (nvar kid)) (nc_lteq (nvar kid) u2)) env in let loop_vtyp = atom_typ (nvar kid) in let checked_body = crule check_exp (Env.add_local v (Immutable, loop_vtyp) env) body unit_typ in - annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ + if not is_dec (* undo reverse direction in annoteded ast for downto loop *) + then annot_exp (E_for (v, inferred_f, inferred_t, checked_step, ord, checked_body)) unit_typ + else annot_exp (E_for (v, inferred_t, inferred_f, checked_step, ord, checked_body)) unit_typ end | _, _ -> typ_error l "Ranges in foreach overlap" end -- cgit v1.2.3 From a82fcc52ee1145f61698ea7e71141ebd76ff04d2 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 31 Oct 2017 17:16:47 +0000 Subject: Improvements to register read tracing in ocaml backend --- src/ocaml_backend.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index feadb2d5..5a378fa6 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -64,7 +64,10 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, _)) arg = match typ_aux with | Typ_id id -> ocaml_string_of id ^^ space ^^ arg | Typ_app (id, []) -> ocaml_string_of id ^^ space ^^ arg - | Typ_app (id, typs) -> string ("\"APP" ^ string_of_id id ^ "\"") + | Typ_app (id, [Typ_arg_aux (Typ_arg_typ typ, _)]) -> + let farg = gensym () in + separate space [string "string_of_list \", \""; parens (separate space [string "fun"; farg; string "->"; ocaml_string_typ typ farg]); arg] + | Typ_app (_, _) -> assert false | Typ_tup typs -> let args = List.map (fun _ -> gensym ()) typs in let body = @@ -75,6 +78,7 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, _)) arg = | Typ_fn (typ1, typ2, _) -> string "\"FN\"" | Typ_var kid -> string "\"VAR\"" | Typ_exist _ | Typ_wild -> assert false + let ocaml_typ_id ctx = function | id when Id.compare id (mk_id "string") = 0 -> string "string" | id when Id.compare id (mk_id "list") = 0 -> string "list" @@ -252,9 +256,12 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) = match Env.lookup_id id (env_of exp) with | Local (Immutable, _) | Unbound -> zencode ctx id | Enum _ | Union _ -> zencode_upper ctx id - | Register _ -> - if !opt_trace_ocaml - then parens (string ("trace \"Read: " ^ string_of_id id ^ "\";") ^^ space ^^ bang ^^ zencode ctx id) + | Register typ -> + if !opt_trace_ocaml then + let var = gensym () in + let str_typ = parens (ocaml_string_typ (Rewriter.simple_typ typ) var) in + parens (separate space [string "let"; var; equals; bang ^^ zencode ctx id; string "in"; + string "trace_read" ^^ space ^^ string_lit (string_of_id id) ^^ space ^^ str_typ ^^ semi; var]) else bang ^^ zencode ctx id | Local (Mutable, _) -> bang ^^ zencode ctx id end -- cgit v1.2.3 From e8de662b4d8d5e4bcc7368277d8607f9a8bc3405 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 31 Oct 2017 17:32:33 +0000 Subject: Added trace viewer application for traces produced by sail -ocaml_trace See README file for how to set up and use --- src/trace_viewer/.gitignore | 6 + src/trace_viewer/List-add.svg | 56 ++++++++ src/trace_viewer/List-remove.svg | 56 ++++++++ src/trace_viewer/README | 11 ++ src/trace_viewer/index.css | 86 ++++++++++++ src/trace_viewer/index.html | 19 +++ src/trace_viewer/index.ts | 287 +++++++++++++++++++++++++++++++++++++++ src/trace_viewer/main.ts | 12 ++ src/trace_viewer/package.json | 15 ++ src/trace_viewer/tsconfig.json | 18 +++ 10 files changed, 566 insertions(+) create mode 100644 src/trace_viewer/.gitignore create mode 100644 src/trace_viewer/List-add.svg create mode 100644 src/trace_viewer/List-remove.svg create mode 100644 src/trace_viewer/README create mode 100644 src/trace_viewer/index.css create mode 100644 src/trace_viewer/index.html create mode 100644 src/trace_viewer/index.ts create mode 100644 src/trace_viewer/main.ts create mode 100644 src/trace_viewer/package.json create mode 100644 src/trace_viewer/tsconfig.json (limited to 'src') diff --git a/src/trace_viewer/.gitignore b/src/trace_viewer/.gitignore new file mode 100644 index 00000000..c1f9aea6 --- /dev/null +++ b/src/trace_viewer/.gitignore @@ -0,0 +1,6 @@ +*~ +*.js +*.js.map + +# Dependencies +node_modules/ diff --git a/src/trace_viewer/List-add.svg b/src/trace_viewer/List-add.svg new file mode 100644 index 00000000..f8031599 --- /dev/null +++ b/src/trace_viewer/List-add.svg @@ -0,0 +1,56 @@ + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + Add + 2006-01-04 + + + Andreas Nilsson + + + http://tango-project.org + + + add + plus + + + + + + + + + + + + + + + + + + + + + diff --git a/src/trace_viewer/List-remove.svg b/src/trace_viewer/List-remove.svg new file mode 100644 index 00000000..f8031599 --- /dev/null +++ b/src/trace_viewer/List-remove.svg @@ -0,0 +1,56 @@ + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + Add + 2006-01-04 + + + Andreas Nilsson + + + http://tango-project.org + + + add + plus + + + + + + + + + + + + + + + + + + + + + diff --git a/src/trace_viewer/README b/src/trace_viewer/README new file mode 100644 index 00000000..547a1435 --- /dev/null +++ b/src/trace_viewer/README @@ -0,0 +1,11 @@ + +To use, first make sure node.js and npm are installed (e.g. via the +Ubuntu package manager), then run the following in this directory: + +> npm install + +> npm run tsc + +> ./node_modules/.bin/electron . + +and point the file selector at a trace produced by sail -ocaml_trace \ No newline at end of file diff --git a/src/trace_viewer/index.css b/src/trace_viewer/index.css new file mode 100644 index 00000000..35ebcb23 --- /dev/null +++ b/src/trace_viewer/index.css @@ -0,0 +1,86 @@ + +body { + background-color: #202020; + color: #DCDCCC; + font-family: monospace; + font-size: 14pt; + font-weight: bold; +} + +img { + height: 30px; +} + +#control { + position: fixed; + bottom: 0px; + left:10%; + right:10%; + width:80%; +} + +#command { + font-size: 16pt; + width: 100%; +} + +.call { + background-color: #313131; + border: 1px; + border-left: 5px; + border-color: rgb(118, 173, 160); + border-style: solid; + padding-top: 2px; + padding-bottom: 2px; + margin: 0px; + min-height: 32px; + display: flex; + align-items: center; +} + +.write { + background-color: #313131; + border: 1px; + border-left: 5px; + border-color: rgb(255, 40, 40); + border-style: solid; + padding-top: 2px; + padding-bottom: 2px; + margin: 0px; + min-height: 32px; + display: flex; + align-items: center; +} + +.load { + background-color: #313131; + color: white; + border: 1px; + border-left: 5px; + border-color: #ff9100; + border-style: solid; + padding-top: 2px; + padding-bottom: 2px; + margin: 0px; + min-height: 32px; + display: flex; + align-items: center; +} + +.read { + background-color: #313131; + border: 1px; + border-left: 5px; + border-color: rgb(107, 199, 47); + border-style: solid; + padding-top: 2px; + padding-bottom: 2px; + margin: 0px; + min-height: 32px; + display: flex; + align-items: center; +} + +.tree { + padding-left: 20px; +} \ No newline at end of file diff --git a/src/trace_viewer/index.html b/src/trace_viewer/index.html new file mode 100644 index 00000000..75c5e035 --- /dev/null +++ b/src/trace_viewer/index.html @@ -0,0 +1,19 @@ + + + + + Sail Log Viewer + + + + + +
+
+
+ +
+ + \ No newline at end of file diff --git a/src/trace_viewer/index.ts b/src/trace_viewer/index.ts new file mode 100644 index 00000000..f9b5041b --- /dev/null +++ b/src/trace_viewer/index.ts @@ -0,0 +1,287 @@ +import {remote} from "electron" +import fs = require("fs") +const dialog = remote.dialog +const app = remote.app + +let topCallDiv = document.createElement("div") + +const max_arg_length = 5000 + +abstract class Event { + caller: Call + + protected div: HTMLDivElement | null = null + + public hide(): void { + if (this.div != null) { + this.div.remove() + this.div = null + } + } + + protected abstract showText(text: HTMLParagraphElement): void + + public show(): HTMLDivElement { + let callerDiv: HTMLDivElement = (this.caller != null) ? this.caller.show() : topCallDiv + + if (this.div != null) { + return this.div + } else { + this.div = document.createElement("div") + this.div.className = "tree" + callerDiv.appendChild(this.div) + let text = document.createElement("p") + this.showText(text) + this.div.appendChild(text) + return this.div + } + } +} + +class Load extends Event { + loc: string + val: string + + constructor(loc: string, val: string) { + super() + this.loc = loc + this.val = val + } + + protected showText(text: HTMLParagraphElement): void { + text.className = "load" + text.insertAdjacentText('beforeend', this.loc + " " + this.val) + } +} + +class Read extends Event { + reg: string + value: string + + constructor(reg: string, value: string) { + super() + this.reg = reg + this.value = value + } + + public showText(text: HTMLParagraphElement): void { + text.className = "read" + text.insertAdjacentText('beforeend', this.reg + " " + this.value) + } +} + +class Write extends Event { + reg: string + value: string + + constructor(reg: string, value: string) { + super() + this.reg = reg + this.value = value + } + + public showText(text: HTMLParagraphElement): void { + text.className = "write" + text.insertAdjacentText('beforeend', this.reg + " " + this.value) + } +} + +class Call { + fn: string + arg: string + ret: string + callees: (Call | Event)[] = [] + caller: Call + + private div: HTMLDivElement | null = null + + private toggle: boolean = false + private toggleImg: HTMLImageElement | null = null + + constructor(fn: string, arg: string, ret: string) { + this.fn = fn + this.arg = arg + this.ret = ret + } + + public expand() { + if (this.caller != undefined) { + this.caller.expand() + } + this.showChildren() + } + + public iter(f: (call: Call) => void): void { + f(this) + this.callees.forEach((callee) => { + if (callee instanceof Call) { callee.iter(f) } + }) + + } + + public show(): HTMLDivElement { + let callerDiv: HTMLDivElement = (this.caller != null) ? this.caller.show() : topCallDiv + + if (this.div != null) { + return this.div + } else { + this.div = document.createElement("div") + this.div.className = "tree" + callerDiv.appendChild(this.div) + let text = document.createElement("p") + text.className = "call" + if (this.callees.length > 0) { + this.toggleImg = document.createElement("img") + this.toggleImg.src = "List-add.svg" + this.toggleImg.addEventListener('click', () => { + if (this.toggle) { + this.hideChildren() + } else { + this.showChildren() + } + }) + text.appendChild(this.toggleImg) + } + this.toggle = false + let display_arg = this.arg + if (this.arg.length > max_arg_length) { + display_arg = this.arg.slice(0, max_arg_length) + } + let display_ret = this.ret + if (this.ret.length > max_arg_length) { + display_ret = this.ret.slice(0, max_arg_length) + } + + text.insertAdjacentText('beforeend', this.fn + " " + display_arg + " -> " + display_ret) + this.div.appendChild(text) + return this.div + } + } + + public hide(): void { + if (this.toggle == true) { + this.hideChildren() + } + + if (this.div != null) { + this.div.remove() + this.div = null + } + if (this.toggleImg != null) { + this.toggleImg.remove() + this.toggleImg = null + } + } + + public hideChildren(): void { + this.callees.forEach(call => { + call.hide() + }) + + if (this.toggleImg != null) { + this.toggleImg.src = "List-add.svg" + this.toggle = false + } else { + alert("this.toggleImg was null!") + } + } + + public showChildren(): void { + this.callees.forEach(call => { + call.show() + }); + + if (this.toggleImg != null) { + this.toggleImg.src = "List-remove.svg" + this.toggle = true + } else { + alert("this.toggleImg was null!") + } + } + + public appendChild(child: Call | Write | Read | Load): void { + child.caller = this + + this.callees.push(child) + } +} + +document.addEventListener('DOMContentLoaded', () => { + let rootCall = new Call("ROOT", "", "") + topCallDiv.id = "root" + document.getElementById("container")!.appendChild(topCallDiv) + + let commandInput = document.getElementById("command") as HTMLInputElement + + commandInput.addEventListener("keydown", (event) => { + if(event.keyCode == 13) { + let cmd = commandInput.value.split(" ") + commandInput.value = "" + + if (cmd[0] == "function") { + rootCall.iter((call) => { + if (call.fn == cmd[1]) { call.caller.expand() } + }) + } + } + }) + + let files = dialog.showOpenDialog(remote.getCurrentWindow(), {title: "Select log file", defaultPath: app.getAppPath()}) + + if (files == [] || files == undefined) { + dialog.showErrorBox("Error", "No file selected") + app.exit(1) + } + + fs.readFile(files[0], 'utf-8', (err, data) => { + if (err) { + dialog.showErrorBox("Error", "An error occurred when reading the log: " + err.message) + app.exit(1) + } + + let lines = data.split("\n") + // let indents = lines.map(line => line.search(/[^\s]/) / 2) + lines = lines.map(line => line.trim()) + + let stack : Call[] = [rootCall] + + lines.forEach(line => { + if (line.match(/^Call:/)) { + let words = line.slice(6).split(" ") + let call = new Call(words[0], words.slice(1).join(" "), "") + if (stack.length > 0) { + stack[stack.length - 1].appendChild(call) + } + stack.push(call) + } else if (line.match(/^Return:/)) { + let call = stack.pop() + if (call == undefined) { + alert("Unbalanced return") + app.exit(1) + } else { + call.ret = line.slice(8) + } + } else if (line.match(/^Write:/)) { + let words = line.slice(7).split(" ") + let write = new Write(words[0], words.slice(1).join(" ")) + if (stack.length > 0) { + stack[stack.length - 1].appendChild(write) + } + } else if (line.match(/^Read:/)) { + let words = line.slice(6).split(" ") + let read = new Read(words[0], words.slice(1).join(" ")) + if (stack.length > 0) { + stack[stack.length - 1].appendChild(read) + } + } else if (line.match(/^Load:/)) { + let words = line.slice(6).split(" ") + let load = new Load(words[0], words[1]) + if (stack.length > 0) { + stack[stack.length - 1].appendChild(load) + } + } + }) + + rootCall.show() + }) +}) \ No newline at end of file diff --git a/src/trace_viewer/main.ts b/src/trace_viewer/main.ts new file mode 100644 index 00000000..5cc33452 --- /dev/null +++ b/src/trace_viewer/main.ts @@ -0,0 +1,12 @@ +import {app, BrowserWindow} from 'electron' + +let win : BrowserWindow | null = null + +app.on('ready', () => { + win = new BrowserWindow({width: 1920, height: 1200}) + win.loadURL('file://' + __dirname + '/index.html') + //win.webContents.openDevTools() + win.on('close', () => { + win = null + }) +}) \ No newline at end of file diff --git a/src/trace_viewer/package.json b/src/trace_viewer/package.json new file mode 100644 index 00000000..e3a88d30 --- /dev/null +++ b/src/trace_viewer/package.json @@ -0,0 +1,15 @@ +{ + "name": "trace_viewer", + "version": "1.0.0", + "description": "", + "main": "main.js", + "scripts": { + "test": "echo \"Error: no test specified\" && exit 1", + "tsc": "./node_modules/typescript/bin/tsc" + }, + "devDependencies": { + "@types/node": "^8.0.46", + "electron": "1.7.9", + "typescript": "^2.5.3" + } +} diff --git a/src/trace_viewer/tsconfig.json b/src/trace_viewer/tsconfig.json new file mode 100644 index 00000000..e66156b3 --- /dev/null +++ b/src/trace_viewer/tsconfig.json @@ -0,0 +1,18 @@ +{ + "compileOnSave": true, + "compilerOptions": { + "target": "es5", + "moduleResolution": "node", + "pretty": true, + "newLine": "LF", + "allowSyntheticDefaultImports": true, + "strict": true, + "noUnusedLocals": true, + "noUnusedParameters": true, + "sourceMap": true, + "strictNullChecks": true, + "skipLibCheck": true, + "allowJs": true, + "jsx": "preserve" + } +} \ No newline at end of file -- cgit v1.2.3 From d610decb92eea6c0e55456f62d5c73cd03d1997b Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 31 Oct 2017 17:36:00 +0000 Subject: Fixed wrong image for List-remove.svg --- src/trace_viewer/List-remove.svg | 169 ++++++++++++++++++++++++++------------- 1 file changed, 115 insertions(+), 54 deletions(-) (limited to 'src') diff --git a/src/trace_viewer/List-remove.svg b/src/trace_viewer/List-remove.svg index f8031599..18c9a135 100644 --- a/src/trace_viewer/List-remove.svg +++ b/src/trace_viewer/List-remove.svg @@ -1,56 +1,117 @@ - - - - - - - - - - - - - - - - - - - - image/svg+xml - - Add - 2006-01-04 - - - Andreas Nilsson - - - http://tango-project.org - - - add - plus - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + Remove + 2006-01-04 + + + Andreas Nilsson + + + http://tango-project.org + + + remove + delete + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file -- cgit v1.2.3 From bc9ed991891718f8b2b9a7ae5398a8ba30333a0a Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 31 Oct 2017 12:25:58 +0000 Subject: Fix some missing nexp simplification in Lem output --- src/pretty_print_lem.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index a0a4878b..f4ff3a40 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -150,7 +150,9 @@ let is_regtyp (Typ_aux (typ, _)) env = match typ with | Typ_id(id) when Env.is_regtyp id env -> true | _ -> false -let doc_nexp_lem (Nexp_aux (nexp, l) as full_nexp) = match nexp with +let doc_nexp_lem nexp = + let (Nexp_aux (nexp, l) as full_nexp) = simplify_nexp nexp in + match nexp with | Nexp_constant i -> string ("ty" ^ string_of_int i) | Nexp_var v -> string (string_of_kid (orig_kid v)) | _ -> @@ -256,7 +258,7 @@ let doc_typ_lem, doc_atomic_typ_lem = Typ_arg_aux (Typ_arg_typ elem_typ, _)]) -> let tpp = match elem_typ with | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) when mwords -> - string "bitvector " ^^ doc_nexp_lem (simplify_nexp m) + string "bitvector " ^^ doc_nexp_lem m (* (match simplify_nexp m with | (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i | (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m] @@ -308,7 +310,7 @@ let doc_typ_lem, doc_atomic_typ_lem = end and doc_typ_arg_lem sequential mwords (Typ_arg_aux(t,_)) = match t with | Typ_arg_typ t -> app_typ sequential mwords true t - | Typ_arg_nexp n -> doc_nexp_lem (simplify_nexp n) + | Typ_arg_nexp n -> doc_nexp_lem n | Typ_arg_order o -> empty in typ', atomic_typ @@ -426,7 +428,8 @@ let rec typeclass_nexps (Typ_aux(t,_)) = match t with | Typ_app (Id_aux (Id "vector",_), [_;Typ_arg_aux (Typ_arg_nexp size_nexp,_); _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> - if is_nexp_constant (simplify_nexp size_nexp) then NexpSet.empty else + let size_nexp = simplify_nexp size_nexp in + if is_nexp_constant size_nexp then NexpSet.empty else NexpSet.singleton (orig_nexp size_nexp) | Typ_app _ -> NexpSet.empty | Typ_exist (kids,_,t) -> NexpSet.empty (* todo *) -- cgit v1.2.3 From 255b77f23a79a08c1d0f5569e613620aae2b4d0e Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 1 Nov 2017 10:38:44 +0000 Subject: Support bitvector-size-parametric functions in Lem output Translates atom('n) types into itself('n) types that won't be erased Also exports more rewriting functions --- src/gen_lib/sail_operators_mwords.lem | 10 ++ src/initial_check.ml | 1 + src/monomorphise.ml | 283 ++++++++++++++++++++++++++++++++-- src/pretty_print_lem.ml | 35 +++-- src/process_file.ml | 2 +- src/rewriter.mli | 12 ++ src/type_check.ml | 16 ++ 7 files changed, 327 insertions(+), 32 deletions(-) (limited to 'src') diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index d4dca80c..8fb55137 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -3,6 +3,16 @@ open import Machine_word open import Sail_impl_base open import Sail_values +(* Translating between a type level number (itself 'n) and an integer *) + +let size_itself_int x = integerFromNat (size_itself x) + +(* NB: the corresponding sail type is forall 'n. atom('n) -> itself('n), + the actual integer is ignored. *) + +val make_the_value : forall 'n. integer -> itself 'n +let inline make_the_value x = the_value + (*** Bit vector operations *) let bitvector_length bs = integerFromNat (word_length bs) diff --git a/src/initial_check.ml b/src/initial_check.ml index 61e352f5..b33d90f5 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -913,6 +913,7 @@ let initial_kind_env = ("atom", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); ("option", { k = K_Lam( [{k=K_Typ}], {k=K_Typ}) }); ("implicit", {k = K_Lam( [{k = K_Nat}], {k=K_Typ})} ); + ("itself", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})}); ] let typschm_of_string order str = diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 2c3dda0e..53200b16 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -264,24 +264,24 @@ and contains_exist_arg (Typ_arg_aux (arg,_)) = -> false | Typ_arg_typ typ -> contains_exist typ +let rec size_nvars_nexp (Nexp_aux (ne,_)) = + match ne with + | Nexp_var v -> [v] + | Nexp_id _ + | Nexp_constant _ + -> [] + | Nexp_times (n1,n2) + | Nexp_sum (n1,n2) + | Nexp_minus (n1,n2) + -> size_nvars_nexp n1 @ size_nvars_nexp n2 + | Nexp_exp n + | Nexp_neg n + -> size_nvars_nexp n + (* Given a type for a constructor, work out which refinements we ought to produce *) (* TODO collision avoidance *) let split_src_type id ty (TypQ_aux (q,ql)) = let i = string_of_id id in - let rec size_nvars_nexp (Nexp_aux (ne,_)) = - match ne with - | Nexp_var v -> [v] - | Nexp_id _ - | Nexp_constant _ - -> [] - | Nexp_times (n1,n2) - | Nexp_sum (n1,n2) - | Nexp_minus (n1,n2) - -> size_nvars_nexp n1 @ size_nvars_nexp n2 - | Nexp_exp n - | Nexp_neg n - -> size_nvars_nexp n - in (* This was originally written for the general case, but I cut it down to the more manageable prenex-form below *) let rec size_nvars_ty (Typ_aux (ty,l) as typ) = @@ -1438,13 +1438,266 @@ let split_defs splits defs = | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ + | DEF_fixity _ -> [d] | DEF_fundef fd -> [DEF_fundef (map_fundef fd)] | DEF_val lb -> [DEF_val (map_letbind lb)] | DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd) - in Defs (List.concat (List.map map_def defs)) in map_locs splits defs' + + +(* The next section of code turns atom('n) types into itself('n) types, which + survive into the Lem output, so can be used to parametrise functions over + internal bitvector lengths (such as datasize and regsize in ARM specs *) + +module AtomToItself = +struct + +let findi f = + let rec aux n = function + | [] -> None + | h::t -> match f h with Some x -> Some (n,x) | _ -> aux (n+1) t + in aux 0 + +let mapat f is xs = + let rec aux n = function + | _, [] -> [] + | (i,_)::is, h::t when i = n -> + let h' = f h in + let t' = aux (n+1) (is, t) in + h'::t' + | is, h::t -> + let t' = aux (n+1) (is, t) in + h::t' + in aux 0 (is, xs) + +let mapat_extra f is xs = + let rec aux n = function + | _, [] -> [], [] + | (i,v)::is, h::t when i = n -> + let h',x = f v h in + let t',xs = aux (n+1) (is, t) in + h'::t',x::xs + | is, h::t -> + let t',xs = aux (n+1) (is, t) in + h::t',xs + in aux 0 (is, xs) + +let tyvars_bound_in_pat pat = + let open Rewriter in + fst (fold_pat + { (compute_pat_alg KidSet.empty KidSet.union) with + p_var = (fun ((s,pat),kid) -> KidSet.add kid s, P_var (pat,kid)) } + pat) +let tyvars_bound_in_lb (LB_aux (LB_val (pat,_),_)) = tyvars_bound_in_pat pat + +let rec sizes_of_typ (Typ_aux (t,l)) = + match t with + Typ_wild + | Typ_id _ + | Typ_var _ + -> KidSet.empty + | Typ_fn _ -> raise (Reporting_basic.err_general l + "Function type on expressinon") + | Typ_tup typs -> kidset_bigunion (List.map sizes_of_typ typs) + | Typ_exist (kids,_,typ) -> + List.fold_left (fun s k -> KidSet.remove k s) (sizes_of_typ typ) kids + | Typ_app (Id_aux (Id "vector",_), + [_;Typ_arg_aux (Typ_arg_nexp size,_); + _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> + KidSet.of_list (size_nvars_nexp size) + | Typ_app (_,tas) -> + kidset_bigunion (List.map sizes_of_typarg tas) +and sizes_of_typarg (Typ_arg_aux (ta,_)) = + match ta with + Typ_arg_nexp _ + | Typ_arg_order _ + -> KidSet.empty + | Typ_arg_typ typ -> sizes_of_typ typ + +let sizes_of_annot = function + | _,None -> KidSet.empty + | _,Some (_,typ,_) -> sizes_of_typ typ + +let change_parameter_pat kid = function + | P_aux (P_id var, (l,_)) + | P_aux (P_typ (_,P_aux (P_id var, (l,_))),_) + -> P_aux (P_id var, (l,None)), (var,kid) + | P_aux (_,(l,_)) -> raise (Reporting_basic.err_unreachable l + "Expected variable pattern") + +(* We add code to change the itself('n) parameter into the corresponding + integer. *) +let add_var_rebind exp (var,kid) = + let l = Generated Unknown in + let annot = (l,None) in + E_aux (E_let (LB_aux (LB_val (P_aux (P_id var,annot), + E_aux (E_app (mk_id "size_itself_int",[E_aux (E_id var,annot)]),annot)),annot),exp),annot) + +(* atom('n) arguments to function calls need to be rewritten *) +let replace_with_the_value (E_aux (_,(l,_)) as exp) = + let typ = Env.expand_synonyms (env_of exp) (typ_of exp) in + let typ, wrap = match typ with + | Typ_aux (Typ_exist (kids,nc,typ),l) -> typ, fun t -> Typ_aux (Typ_exist (kids,nc,t),l) + | _ -> typ, fun x -> x + in + let mk_exp nexp l l' = + E_aux (E_cast (wrap (Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown), + [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated Unknown)), + E_aux (E_app (Id_aux (Id "make_the_value",Generated Unknown),[exp]),(Generated l,None))), + (Generated l,None)) + in + match typ with + | Typ_aux (Typ_app (Id_aux (Id "range",_), + [Typ_arg_aux (Typ_arg_nexp nexp,l');Typ_arg_aux (Typ_arg_nexp nexp',_)]),_) + when nexp = nexp' -> + mk_exp nexp l l' + | _ -> raise (Reporting_basic.err_unreachable l + "atom stopped being an atom?") + +let replace_type env typ = + let Typ_aux (t,l) = Env.expand_synonyms env typ in + match t with + | Typ_app (Id_aux (Id "range",_), + [Typ_arg_aux (Typ_arg_nexp nexp,l');Typ_arg_aux (Typ_arg_nexp _,_)]) -> + Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown), + [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated l) + | _ -> raise (Reporting_basic.err_unreachable l + "atom stopped being an atom?") + + +let rewrite_size_parameters env (Defs defs) = + let open Rewriter in + let size_vars exp = + fst (fold_exp + { (compute_exp_alg KidSet.empty KidSet.union) with + e_aux = (fun ((s,e),annot) -> KidSet.union s (sizes_of_annot annot), E_aux (e,annot)); + e_let = (fun ((sl,lb),(s2,e2)) -> KidSet.union sl (KidSet.diff s2 (tyvars_bound_in_lb lb)), E_let (lb,e2)); + pat_exp = (fun ((sp,pat),(s,e)) -> KidSet.diff s (tyvars_bound_in_pat pat), Pat_exp (pat,e))} + exp) + in + let sizes_funcl fsizes (FCL_aux (FCL_Funcl (id,pat,exp),(l,_))) = + let sizes = size_vars exp in + (* TODO: what, if anything, should sequential be? *) + let visible_tyvars = + KidSet.union (Pretty_print_lem.lem_tyvars_of_typ false true (pat_typ_of pat)) + (Pretty_print_lem.lem_tyvars_of_typ false true (typ_of exp)) + in + let expose_tyvars = KidSet.diff sizes visible_tyvars in + let parameters = match pat with + | P_aux (P_tup ps,_) -> ps + | _ -> [pat] + in + let to_change = List.map + (fun kid -> + let check (P_aux (_,(_,Some (env,typ,_)))) = + match Env.expand_synonyms env typ with + Typ_aux (Typ_app(Id_aux (Id "range",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_); + Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_)]),_) -> + if Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 then Some kid else None + | _ -> None + in match findi check parameters with + | None -> raise (Reporting_basic.err_general l + ("Unable to find an argument for " ^ string_of_kid kid)) + | Some i -> i) + (KidSet.elements expose_tyvars) + in + let to_change = List.sort compare to_change in + match Bindings.find id fsizes with + | old -> if old = to_change then fsizes else + raise (Reporting_basic.err_general l + ("Different size type variables in different clauses of " ^ string_of_id id)) + | exception Not_found -> Bindings.add id to_change fsizes + in + let sizes_def fsizes = function + | DEF_fundef (FD_aux (FD_function (_,_,_,funcls),_)) -> + List.fold_left sizes_funcl fsizes funcls + | _ -> fsizes + in + let fn_sizes = List.fold_left sizes_def Bindings.empty defs in + + let rewrite_e_app (id,args) = + match Bindings.find id fn_sizes with + | [] -> E_app (id,args) + | to_change -> + let args' = mapat replace_with_the_value to_change args in + E_app (id,args') + | exception Not_found -> E_app (id,args) + in + let rewrite_funcl (FCL_aux (FCL_Funcl (id,pat,body),(l,annot))) = + let pat,body = + (* Update pattern and add itself -> nat wrapper to body *) + match Bindings.find id fn_sizes with + | [] -> pat,body + | to_change -> + let pat, vars = + match pat with + P_aux (P_tup pats,(l,_)) -> + let pats, vars = mapat_extra change_parameter_pat to_change pats in + P_aux (P_tup pats,(l,None)), vars + | P_aux (_,(l,_)) -> + begin + match to_change with + | [0,kid] -> + let pat, var = change_parameter_pat kid pat in + pat, [var] + | _ -> + raise (Reporting_basic.err_unreachable l + "Expected multiple parameters at single parameter") + end + in + let body = List.fold_left add_var_rebind body vars in + pat,body + | exception Not_found -> pat,body + in + (* Update function applications *) + let body = fold_exp { id_exp_alg with e_app = rewrite_e_app } body in + FCL_aux (FCL_Funcl (id,pat,body),(l,None)) + in + let rewrite_def = function + | DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,funcls),(l,_))) -> + (* TODO rewrite tannopt? *) + DEF_fundef (FD_aux (FD_function (recopt,tannopt,effopt,List.map rewrite_funcl funcls),(l,None))) + | DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,annot))) as spec -> + begin + match Bindings.find id fn_sizes with + | [] -> spec + | to_change -> + let typschm = match typschm with + | TypSchm_aux (TypSchm_ts (tq,typ),l) -> + let typ = match typ with + | Typ_aux (Typ_fn (Typ_aux (Typ_tup ts,l),t2,eff),l2) -> + Typ_aux (Typ_fn (Typ_aux (Typ_tup (mapat (replace_type env) to_change ts),l),t2,eff),l2) + | _ -> replace_type env typ + in TypSchm_aux (TypSchm_ts (tq,typ),l) + in + DEF_spec (VS_aux (VS_val_spec (typschm,id,extern,cast),(l,None))) + | exception Not_found -> spec + end + | def -> def + in +(* + Bindings.iter (fun id args -> + print_endline (string_of_id id ^ " needs " ^ + String.concat ", " (List.map string_of_int args))) fn_sizes +*) + Defs (List.map rewrite_def defs) + +end + +let monomorphise mwords splits defs = + let defs = split_defs splits defs in + (* TODO: currently doing this because constant propagation leaves numeric literals as + int, try to avoid this later; also use final env for DEF_spec case above, because the + type checker doesn't store the env at that point :( *) + if mwords then + let (defs,env) = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in + let defs = AtomToItself.rewrite_size_parameters env defs in + defs + else + defs diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index f4ff3a40..6efebbc7 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -427,7 +427,9 @@ let rec typeclass_nexps (Typ_aux(t,_)) = match t with | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts) | Typ_app (Id_aux (Id "vector",_), [_;Typ_arg_aux (Typ_arg_nexp size_nexp,_); - _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) -> + _;Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id (Id_aux (Id "bit",_)),_)),_)]) +| Typ_app (Id_aux (Id "itself",_), + [Typ_arg_aux (Typ_arg_nexp size_nexp,_)]) -> let size_nexp = simplify_nexp size_nexp in if is_nexp_constant size_nexp then NexpSet.empty else NexpSet.singleton (orig_nexp size_nexp) @@ -494,13 +496,14 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) = | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem sequential mwords true p) (doc_pat_lem sequential mwords true p') | P_record (_,_) -> empty (* TODO *) -let rec contains_bitvector_typ (Typ_aux (t,_) as typ) = match t with - | Typ_tup ts -> List.exists contains_bitvector_typ ts - | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists contains_bitvector_typ_arg targs - | Typ_fn (t1,t2,_) -> contains_bitvector_typ t1 || contains_bitvector_typ t2 +let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with + | Typ_tup ts -> List.exists typ_needs_printed ts + | Typ_app (Id_aux (Id "itself",_),_) -> true + | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists typ_needs_printed_arg targs + | Typ_fn (t1,t2,_) -> typ_needs_printed t1 || typ_needs_printed t2 | _ -> false -and contains_bitvector_typ_arg (Typ_arg_aux (targ, _)) = match targ with - | Typ_arg_typ t -> contains_bitvector_typ t +and typ_needs_printed_arg (Typ_arg_aux (targ, _)) = match targ with + | Typ_arg_typ t -> typ_needs_printed t | _ -> false let contains_early_return exp = @@ -697,7 +700,7 @@ let doc_exp_lem, doc_let_lem = let (taepp,aexp_needed) = let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in let eff = effect_of full_exp in - if contains_bitvector_typ t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var t) then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true) else (epp, aexp_needed) in if aexp_needed then parens (align taepp) else taepp*) @@ -739,7 +742,7 @@ let doc_exp_lem, doc_let_lem = let (taepp,aexp_needed) = let t = (*Env.base_typ_of (env_of full_exp)*) (typ_of full_exp) in let eff = effect_of full_exp in - if contains_bitvector_typ (Env.base_typ_of (env_of full_exp) t) + if typ_needs_printed (Env.base_typ_of (env_of full_exp) t) then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true) else (epp, aexp_needed) in liftR (if aexp_needed then parens (align taepp) else taepp) @@ -797,7 +800,7 @@ let doc_exp_lem, doc_let_lem = let (epp,aexp_needed) = if has_effect eff BE_rreg then let epp = align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in - if contains_bitvector_typ t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var t) then (epp ^^ doc_tannot_lem sequential mwords true t, true) else (epp, aexp_needed) else @@ -818,7 +821,7 @@ let doc_exp_lem, doc_let_lem = let eff = effect_of full_exp in let field_f = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in let (ta,aexp_needed) = - if contains_bitvector_typ t + if typ_needs_printed t then (doc_tannot_lem sequential mwords (effectful eff) t, true) else (empty, aexp_needed) in let epp = field_f ^^ space ^^ (expY fexp) in @@ -853,7 +856,7 @@ let doc_exp_lem, doc_let_lem = | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> "read_reg_bitfield" | _ -> "read_reg_field" in let ta = - if contains_bitvector_typ t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var t) then doc_tannot_lem sequential mwords true t else empty in let epp = separate space [string call;string reg;string_lit(string field)] ^^ ta in if aexp_needed then parens (align epp) else epp @@ -861,7 +864,7 @@ let doc_exp_lem, doc_let_lem = let (call,ta) = if has_effect eff BE_rreg then let ta = - if contains_bitvector_typ t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var t) then doc_tannot_lem sequential mwords true t else empty in ("read_two_regs", ta) else @@ -874,7 +877,7 @@ let doc_exp_lem, doc_let_lem = separate space [string "read_reg_bit";string reg;doc_int start] else let ta = - if contains_bitvector_typ t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var t) then doc_tannot_lem sequential mwords true t else empty in separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in if aexp_needed then parens (align epp) else epp @@ -886,7 +889,7 @@ let doc_exp_lem, doc_let_lem = | Base((_,t),External _,_,_,_,_) -> (* TODO: Does this case still exist with the new type checker? *) let epp = string "read_reg" ^^ space ^^ expY e in - if contains_bitvector_typ t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var t) then parens (epp ^^ doc_tannot_lem sequential mwords true t) else epp | Base((_,t),_,_,_,_,_) -> (match typ with @@ -1118,7 +1121,7 @@ let doc_exp_lem, doc_let_lem = | _ -> string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in let (epp,aexp_needed) = - if contains_bitvector_typ t && not (contains_t_pp_var t) + if typ_needs_printed t && not (contains_t_pp_var t) then (parens epp ^^ doc_tannot_lem sequential mwords false t, true) else (epp, aexp_needed) in if aexp_needed then parens (align epp) else epp diff --git a/src/process_file.ml b/src/process_file.ml index 59518075..aea53ca7 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -121,7 +121,7 @@ let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.E let opt_ddump_raw_mono_ast = ref false let monomorphise_ast locs ast = - let ast = Monomorphise.split_defs locs ast in + let ast = Monomorphise.monomorphise (!opt_lem_mwords) locs ast in let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in let ienv = Type_check.Env.no_casts Type_check.initial_env in Type_check.check ienv ast diff --git a/src/rewriter.mli b/src/rewriter.mli index 3125c410..3f375e25 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -151,12 +151,24 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg } +(* fold over patterns *) +val fold_pat : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg -> 'a pat -> 'pat + (* fold over expressions *) val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, 'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind, 'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg +val id_exp_alg : + ('a,'a exp,'a exp_aux,'a lexp,'a lexp_aux,'a fexp, + 'a fexp_aux,'a fexps,'a fexps_aux, + 'a opt_default_aux,'a opt_default,'a pexp,'a pexp_aux, + 'a letbind_aux,'a letbind, + 'a pat,'a pat_aux,'a fpat,'a fpat_aux) exp_alg + +val compute_pat_alg : 'b -> ('b -> 'b -> 'b) -> + ('a,('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) pat_alg val compute_exp_alg : 'b -> ('b -> 'b -> 'b) -> ('a,('b * 'a exp),('b * 'a exp_aux),('b * 'a lexp),('b * 'a lexp_aux),('b * 'a fexp), diff --git a/src/type_check.ml b/src/type_check.ml index 6c5205fe..6b7495c2 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -507,6 +507,7 @@ end = struct || Id.compare id (mk_id "real") = 0 || Id.compare id (mk_id "list") = 0 || Id.compare id (mk_id "string") = 0 + || Id.compare id (mk_id "itself") = 0 (* Check if a type, order, or n-expression is well-formed. Throws a type error if the type is badly formed. FIXME: Add arity to type @@ -922,6 +923,21 @@ let initial_env = Env.empty |> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args))) + (* Internal functions for Monomorphise.AtomToItself *) + + |> Env.add_extern (mk_id "size_itself_int") "size_itself_int" + |> Env.add_val_spec (mk_id "size_itself_int") + (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)), + Parse_ast.Unknown)],Parse_ast.Unknown), + function_typ (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]) + (atom_typ (nvar (mk_kid "n"))) no_effect) + |> Env.add_extern (mk_id "make_the_value") "make_the_value" + |> Env.add_val_spec (mk_id "make_the_value") + (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)), + Parse_ast.Unknown)],Parse_ast.Unknown), + function_typ (atom_typ (nvar (mk_kid "n"))) + (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]) no_effect) + let ex_counter = ref 0 let fresh_existential ?name:(n="") () = -- cgit v1.2.3 From f8107b6b4dc4738d57a1a0c367de72a6d811f4cb Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 2 Nov 2017 11:50:53 +0000 Subject: Handle "undefined" type-level sizes in monomorphisation --- src/monomorphise.ml | 45 ++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 40 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 53200b16..584d94a7 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -575,6 +575,32 @@ let lit_match = function | (L_one | L_true ), (L_one | L_true ) -> true | l1,l2 -> l1 = l2 +(* There's no undefined nexp, so replace undefined sizes with a plausible size. + 32 is used as a sensible default. *) +let fabricate_nexp l = function + | None -> Nexp_aux (Nexp_constant 32,Unknown) + | Some (env,typ,_) -> + match Type_check.destruct_exist env typ with + | None -> Nexp_aux (Nexp_constant 32,Unknown) + | Some (kids,nc,typ') -> + match kids,nc,Env.expand_synonyms env typ' with + | ([kid],NC_aux (NC_set (kid',i::_),_), + Typ_aux (Typ_app (Id_aux (Id "range",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_); + Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_)) + when Kid.compare kid kid' = 0 && Kid.compare kid kid'' = 0 && + Kid.compare kid kid''' = 0 -> + Nexp_aux (Nexp_constant i,Unknown) + | ([kid],NC_aux (NC_true,_), + Typ_aux (Typ_app (Id_aux (Id "range",_), + [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid'',_)),_); + Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid''',_)),_)]),_)) + when Kid.compare kid kid'' = 0 && + Kid.compare kid kid''' = 0 -> + Nexp_aux (Nexp_constant 32,Unknown) + | _ -> raise (Reporting_basic.err_general l + ("Undefined value at unsupported type " ^ string_of_typ typ)) + type 'a matchresult = | DoesMatch of 'a | DoesNotMatch @@ -614,12 +640,20 @@ let can_match_with_env env (E_aux (e,(l,annot)) as exp0) cases = let checkpat = function | P_aux (P_lit (L_aux (lit_p, _)),_) -> if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch - | P_aux (P_var (P_aux (P_id id,_), kid),_) -> + | P_aux (P_var (P_aux (P_id id,p_id_annot), kid),_) -> begin match lit_e with | L_num i -> DoesMatch ([id, E_aux (e,(l,annot))], [kid,Nexp_aux (Nexp_constant i,Unknown)]) + (* For undefined we fix the type-level size (because there's no good + way to construct an undefined size), but leave the term as undefined + to make the meaning clear. *) + | L_undef -> + let nexp = fabricate_nexp l annot in + let typ = subst_src_typ (KBindings.singleton kid nexp) (typ_of_annot p_id_annot) in + DoesMatch ([id, E_aux (E_cast (typ,E_aux (e,(l,None))),(l,None))], + [kid,nexp]) | _ -> (Reporting_basic.print_err false true lit_l "Monomorphisation" "Unexpected kind of literal for var match"; GiveUp) @@ -692,7 +726,7 @@ let try_app (l,ann) (Id_aux (id,_),args) = | _ -> None else if id = Id "ex_int" then match args with - | [E_aux (E_lit (L_aux (L_num _,_)),_) as exp] -> Some exp + | [E_aux (E_lit lit,(l,_))] -> Some (E_aux (E_lit lit,(l,ann))) | _ -> None else if id = Id "vector_access" || id = Id "bitvector_access" then match args with @@ -1540,11 +1574,12 @@ let add_var_rebind exp (var,kid) = (* atom('n) arguments to function calls need to be rewritten *) let replace_with_the_value (E_aux (_,(l,_)) as exp) = - let typ = Env.expand_synonyms (env_of exp) (typ_of exp) in - let typ, wrap = match typ with + let env = env_of exp in + let typ, wrap = match typ_of exp with | Typ_aux (Typ_exist (kids,nc,typ),l) -> typ, fun t -> Typ_aux (Typ_exist (kids,nc,t),l) - | _ -> typ, fun x -> x + | typ -> typ, fun x -> x in + let typ = Env.expand_synonyms env typ in let mk_exp nexp l l' = E_aux (E_cast (wrap (Typ_aux (Typ_app (Id_aux (Id "itself",Generated Unknown), [Typ_arg_aux (Typ_arg_nexp nexp,l')]),Generated Unknown)), -- cgit v1.2.3