diff options
| -rw-r--r-- | src/initial_check.ml | 33 | ||||
| -rw-r--r-- | src/initial_check.mli | 1 | ||||
| -rw-r--r-- | src/lexer2.mll | 6 | ||||
| -rw-r--r-- | src/parse_ast.ml | 3 | ||||
| -rw-r--r-- | src/parser2.mly | 28 | ||||
| -rw-r--r-- | src/pretty_print_sail2.ml | 24 | ||||
| -rw-r--r-- | src/process_file.ml | 1 | ||||
| -rw-r--r-- | src/process_file.mli | 1 | ||||
| -rw-r--r-- | src/rewrites.ml | 12 | ||||
| -rw-r--r-- | src/rewrites.mli | 3 | ||||
| -rw-r--r-- | src/sail.ml | 12 |
11 files changed, 102 insertions, 22 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index de5b625b..2764c30b 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -46,6 +46,7 @@ open Ast_util open Big_int let opt_undefined_gen = ref false +let opt_magic_hash = ref false module Envmap = Finite_map.Fmap_map(String) module Nameset' = Set.Make(String) @@ -117,10 +118,21 @@ let typ_error l msg opt_id opt_var opt_kind = | None,None,Some(kind) -> " " ^ (kind_to_string kind) | _ -> ""))) -let to_ast_id (Parse_ast.Id_aux(id,l)) = - Id_aux( (match id with - | Parse_ast.Id(x) -> Id(x) - | Parse_ast.DeIid(x) -> DeIid(x)) , l) +let string_of_parse_id_aux = function + | Parse_ast.Id v -> v + | Parse_ast.DeIid v -> v + +let string_contains str char = + try (String.index str char; true) with + | Not_found -> false + +let to_ast_id (Parse_ast.Id_aux(id, l)) = + if string_contains (string_of_parse_id_aux id) '#' && not (!opt_magic_hash) + then typ_error l "Identifier contains hash character" None None None + else Id_aux ((match id with + | Parse_ast.Id(x) -> Id(x) + | Parse_ast.DeIid(x) -> DeIid(x)), + l) let to_ast_var (Parse_ast.Kid_aux(Parse_ast.Var v,l)) = Kid_aux(Var v,l) @@ -483,7 +495,10 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) | Parse_ast.E_vector_append(e1,e2) -> E_vector_append(to_ast_exp k_env def_ord e1,to_ast_exp k_env def_ord e2) | Parse_ast.E_list(exps) -> E_list(List.map (to_ast_exp k_env def_ord) exps) | Parse_ast.E_cons(e1,e2) -> E_cons(to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2) - | Parse_ast.E_record _ -> raise (Reporting_basic.err_unreachable l "parser generated an E_record") + | Parse_ast.E_record fexps -> + (match to_ast_fexps true k_env def_ord fexps with + | Some fexps -> E_record fexps + | None -> raise (Reporting_basic.err_unreachable l "to_ast_fexps with true returned none")) | Parse_ast.E_record_update(exp,fexps) -> (match to_ast_fexps true k_env def_ord fexps with | Some(fexps) -> E_record_update(to_ast_exp k_env def_ord exp, fexps) @@ -886,7 +901,15 @@ let rec to_ast_defs_helper envs partial_defs = function then (fst !d) :: defs, envs, partial_defs else typ_error l "Scattered type definition never ended" (Some id) None None)) +let rec remove_mutrec = function + | [] -> [] + | Parse_ast.DEF_internal_mutrec fundefs :: defs -> + List.map (fun fdef -> Parse_ast.DEF_fundef fdef) fundefs @ remove_mutrec defs + | def :: defs -> + def :: remove_mutrec defs + let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (def_ord : order) (Parse_ast.Defs(defs)) = + let defs = remove_mutrec defs in let defs,(_,k_env,def_ord),partial_defs = to_ast_defs_helper (default_names,kind_env,def_ord) [] defs in List.iter (fun (id,(d,k)) -> diff --git a/src/initial_check.mli b/src/initial_check.mli index feb9cb83..cfbea3e1 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -44,6 +44,7 @@ open Ast open Ast_util val opt_undefined_gen : bool ref +val opt_magic_hash : bool ref val process_ast : order -> Parse_ast.defs -> unit defs diff --git a/src/lexer2.mll b/src/lexer2.mll index 40e7eec6..a8dbaaf3 100644 --- a/src/lexer2.mll +++ b/src/lexer2.mll @@ -121,6 +121,7 @@ let kw_table = ("in", (fun x -> In)); ("inc", (fun _ -> Inc)); ("let", (fun x -> Let_)); + ("record", (fun _ -> Record)); ("Int", (fun x -> Int)); ("Order", (fun x -> Order)); ("pure", (fun x -> Pure)); @@ -142,6 +143,7 @@ let kw_table = ("until", (fun _ -> Until)); ("while", (fun _ -> While)); ("do", (fun _ -> Do)); + ("mutual", (fun _ -> Mutual)); ("barr", (fun x -> Barr)); ("depend", (fun x -> Depend)); @@ -169,7 +171,7 @@ let binarydigit = ['0'-'1'] let hexdigit = ['0'-'9''A'-'F''a'-'f'] let alphanum = letter|digit let startident = letter|'_' -let ident = alphanum|['_''\''] +let ident = alphanum|['_''\'''#'] let tyvar_start = '\'' let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''@''^''|'] let operator = (oper_char+ ('_' ident)?) @@ -200,6 +202,8 @@ rule token = parse | ";" { Semi } | "*" { (Star(r"*")) } | "_" { Under } + | "[|" { LsquareBar } + | "|]" { RsquareBar } | "{|" { LcurlyBar } | "|}" { RcurlyBar } | "|" { Bar } diff --git a/src/parse_ast.ml b/src/parse_ast.ml index bdf56cc8..aceba3b6 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -275,7 +275,7 @@ exp_aux = (* Expression *) | E_vector_append of exp * exp (* vector concatenation *) | E_list of (exp) list (* list *) | E_cons of exp * exp (* cons *) - | E_record of fexps (* struct *) + | E_record of exp list (* struct *) | E_record_update of exp * (exp) list (* functional update of struct *) | E_field of exp * id (* field projection from struct *) | E_case of exp * (pexp) list (* pattern matching *) @@ -498,6 +498,7 @@ def = (* Top-level definition *) | DEF_default of default_typing_spec (* default kind and type assumptions *) | DEF_scattered of scattered_def (* scattered definition *) | DEF_reg_dec of dec_spec (* register declaration *) + | DEF_internal_mutrec of fundef list type diff --git a/src/parser2.mly b/src/parser2.mly index a752e5c1..1444f6cd 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -142,13 +142,13 @@ let rec desugar_rchain chain s e = %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union With Val Constraint Throw Try Catch Exit %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape -%token Repeat Until While Do +%token Repeat Until While Do Record Mutual %nonassoc Then %nonassoc Else %token Bar Comma Dot Eof Minus Semi Under DotDot -%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar +%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar %token MinusGt /*Terminals with content*/ @@ -957,17 +957,33 @@ atomic_exp: { mk_exp (E_vector_access ($1, $3)) $startpos $endpos } | atomic_exp Lsquare exp DotDot exp Rsquare { mk_exp (E_vector_subrange ($1, $3, $5)) $startpos $endpos } + | Record Lcurly fexp_exp_list Rcurly + { mk_exp (E_record $3) $startpos $endpos } + | Lcurly exp With fexp_exp_list Rcurly + { mk_exp (E_record_update ($2, $4)) $startpos $endpos } | Lsquare exp_list Rsquare { mk_exp (E_vector $2) $startpos $endpos } | Lsquare exp With atomic_exp Eq exp Rsquare { mk_exp (E_vector_update ($2, $4, $6)) $startpos $endpos } | Lsquare exp With atomic_exp DotDot atomic_exp Eq exp Rsquare { mk_exp (E_vector_update_subrange ($2, $4, $6, $8)) $startpos $endpos } + | LsquareBar exp_list RsquareBar + { mk_exp (E_list $2) $startpos $endpos } | Lparen exp Rparen { $2 } | Lparen exp Comma exp_list Rparen { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos } +fexp_exp: + | atomic_exp Eq exp + { mk_exp (E_app_infix ($1, mk_id (Id "=") $startpos($2) $endpos($2), $3)) $startpos $endpos } + +fexp_exp_list: + | fexp_exp + { [$1] } + | fexp_exp Comma fexp_exp_list + { $1 :: $3 } + exp_list: | exp { [$1] } @@ -1042,6 +1058,12 @@ fun_def: | Function_ funcls { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos } +fun_def_list: + | fun_def + { [$1] } + | fun_def fun_def_list + { $1 :: $2 } + let_def: | Let_ letbind { $2 } @@ -1115,6 +1137,8 @@ def: { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) } | default_def { DEF_default $1 } + | Mutual Lcurly fun_def_list Rcurly + { DEF_internal_mutrec $3 } defs_list: | def diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml index 8c8b5661..8ebef0f0 100644 --- a/src/pretty_print_sail2.ml +++ b/src/pretty_print_sail2.ml @@ -183,12 +183,13 @@ let rec doc_exp (E_aux (e_aux, _) as exp) = group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp]) | E_list exps -> string "[|" ^^ separate_map (comma ^^ space) doc_exp exps ^^ string "|]" | E_cons (exp1, exp2) -> string "E_cons" - | E_record fexps -> string "E_record" + | E_record fexps -> separate space [string "record"; string "{"; doc_fexps fexps; string "}"] | E_loop (While, cond, exp) -> separate space [string "while"; doc_exp cond; string "do"; doc_exp exp] | E_loop (Until, cond, exp) -> separate space [string "repeat"; doc_exp exp; string "until"; doc_exp cond] - | E_record_update (exp, fexps) -> string "E_record_update" + | E_record_update (exp, fexps) -> + separate space [string "{"; doc_exp exp; string "with"; doc_fexps fexps; string "}"] | E_vector_append (exp1, exp2) -> separate space [doc_atomic_exp exp1; string "@"; doc_atomic_exp exp2] | E_case (exp, pexps) -> separate space [string "match"; doc_exp exp; doc_pexps pexps] @@ -245,6 +246,10 @@ and doc_atomic_exp (E_aux (e_aux, _) as exp) = | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4]) | _ -> parens (doc_exp exp) +and doc_fexps (FES_aux (FES_Fexps (fexps, _), _)) = + separate_map (comma ^^ space) doc_fexp fexps +and doc_fexp (FE_aux (FE_Fexp (id, exp), _)) = + separate space [doc_id id; equals; doc_exp exp] and doc_block = function | [] -> string "()" | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] -> @@ -336,17 +341,7 @@ let doc_spec (VS_aux(v,_)) = let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^ utf8string ("\"" ^ String.escaped id ^ "\"")) (ext b) in let docs = Util.option_these (List.map doc_backend ["ocaml"; "lem"]) in - if docs = [] then empty else braces (separate (comma ^^ space) docs) - (* function - | Some s -> - let ext_for backend = utf8string ("\"" ^ String.escaped (s backend) ^ "\"") in - let extern = - if s "ocaml" = s "lem" - then ext_for "ocaml" - else separate space [lbrace; string "ocaml:"; ext_for "ocaml"; string "lem:"; ext_for "lem"; rbrace] - in - equals ^^ space ^^ extern ^^ space - | None -> empty *) + if docs = [] then empty else equals ^^ space ^^ braces (separate (comma ^^ space) docs) in match v with | VS_val_spec(ts,id,ext,is_cast) -> @@ -382,6 +377,9 @@ let rec doc_def def = group (match def with | DEF_kind k_def -> doc_kind_def k_def | DEF_fundef f_def -> doc_fundef f_def | DEF_val lbind -> string "let" ^^ space ^^ doc_letbind lbind + | DEF_internal_mutrec fundefs -> + (string "mutual {" ^//^ separate_map (hardline ^^ hardline) doc_fundef fundefs) + ^^ hardline ^^ string "}" | DEF_reg_dec dec -> doc_dec dec | DEF_scattered sdef -> doc_scattered sdef | DEF_fixity (prec, n, id) -> diff --git a/src/process_file.ml b/src/process_file.ml index 92b3f328..75e3092f 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -229,4 +229,5 @@ let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)] let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !opt_lem_mwords x)] let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml +let rewrite_ast_sil = rewrite Rewrites.rewrite_defs_sil let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check diff --git a/src/process_file.mli b/src/process_file.mli index b575bd14..116df06e 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -48,6 +48,7 @@ val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs +val rewrite_ast_sil : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_check : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val load_file_no_check : Ast.order -> string -> unit Ast.defs diff --git a/src/rewrites.ml b/src/rewrites.ml index 13d811e4..80e09e9a 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2757,6 +2757,18 @@ let rewrite_defs_ocaml = [ (* ("separate_numbs", rewrite_defs_separate_numbs) *) ] +let rewrite_defs_sil = [ + ("top_sort_defs", top_sort_defs); + ("tuple_vector_assignments", rewrite_tuple_vector_assignments); + ("tuple_assignments", rewrite_tuple_assignments); + ("simple_assignments", rewrite_simple_assignments); + ("constraint", rewrite_constraint); + ("trivial_sizeof", rewrite_trivial_sizeof); + ("sizeof", rewrite_sizeof); + ("remove_vector_concat", rewrite_defs_remove_vector_concat); + ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); + ] + let rewrite_check_annot = let check_annot exp = try diff --git a/src/rewrites.mli b/src/rewrites.mli index 628296ec..432a2bd8 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -53,6 +53,9 @@ val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list (* Perform rewrites to exclude AST nodes not supported for lem out*) val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list +(* Perform rewrites to sail intermediate language *) +val rewrite_defs_sil : (string * (tannot defs -> tannot defs)) list + (* This is a special rewriter pass that checks AST invariants without actually doing any re-writing *) val rewrite_defs_check : (string * (tannot defs -> tannot defs)) list diff --git a/src/sail.ml b/src/sail.ml index e7e965ba..dbd95f1d 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -49,6 +49,7 @@ let opt_print_initial_env = ref false let opt_print_verbose = ref false let opt_print_lem_ast = ref false let opt_print_lem = ref false +let opt_print_sil = ref false let opt_print_ocaml = ref false let opt_convert = ref false let opt_memo_z3 = ref false @@ -74,6 +75,9 @@ let options = Arg.align ([ ( "-lem_ast", Arg.Set opt_print_lem_ast, " output a Lem AST representation of the input"); + ( "-sil", + Arg.Tuple [Arg.Set opt_print_sil; Arg.Set Initial_check.opt_undefined_gen], + " output a SIL translated version of the input"); ( "-lem", Arg.Set opt_print_lem, " output a Lem translated version of the input"); @@ -138,6 +142,9 @@ let options = Arg.align ([ ( "-dsanity", Arg.Set opt_sanity, " (debug) sanity check the AST (slow)"); + ( "-dmagic_hash", + Arg.Set Initial_check.opt_magic_hash, + " (debug) allow special character # in identifiers"); ( "-v", Arg.Set opt_print_version, " print version"); @@ -204,6 +211,11 @@ let main() = (if !(opt_print_lem_ast) then output "" Lem_ast_out [out_name,ast] else ()); + (if !(opt_print_sil) + then + let ast = rewrite_ast_sil ast in + Pretty_print_sail2.pp_defs stdout ast + else ()); (if !(opt_print_ocaml) then let ast_ocaml = rewrite_ast_ocaml ast in |