From 8124c487b576661dfa7a0833415d07d0978bc43e Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 1 Sep 2017 15:33:24 +0100 Subject: Testing typedef generation for ocaml --- src/rewriter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/rewriter.ml b/src/rewriter.ml index 3dc66b04..b180b0a1 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -2510,7 +2510,7 @@ let rewrite_undefined = let rewrite_e_aux (E_aux (e_aux, _) as exp) = match e_aux with | E_lit (L_aux (L_undef, l)) -> - check_exp (env_of exp) (undefined_of_typ (typ_of exp)) (typ_of exp) + check_exp (env_of exp) (undefined_of_typ (Env.expand_synonyms (env_of exp) (typ_of exp))) (typ_of exp) | _ -> exp in let rewrite_exp_undefined = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in -- cgit v1.2.3 From 2625f48417d25ab0493884b2f934887b86d568ab Mon Sep 17 00:00:00 2001 From: Alastair Reid Date: Tue, 5 Sep 2017 15:41:07 +0100 Subject: Fix printing of negative numbers --- src/pretty_print_common.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml index 70f5b749..02cc3574 100644 --- a/src/pretty_print_common.ml +++ b/src/pretty_print_common.ml @@ -212,7 +212,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint = and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_var v -> doc_var v | Nexp_id i -> braces (doc_id i) - | Nexp_constant i -> doc_int i + | Nexp_constant i -> if i < 0 then parens(doc_int i) else doc_int i | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _-> group (parens (nexp ne)) -- cgit v1.2.3 From 842165c1171fde332bd42e7520338c59a797f76b Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 7 Sep 2017 16:54:20 +0100 Subject: Add ocaml run-time and updates to sail for ocaml backend --- src/initial_check.ml | 6 ++++++ src/ocaml_backend.ml | 35 +++++++++++++++++++++++------------ src/type_check.ml | 2 ++ src/type_check.mli | 1 + 4 files changed, 32 insertions(+), 12 deletions(-) (limited to 'src') diff --git a/src/initial_check.ml b/src/initial_check.ml index 74faba25..e9695dd4 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -1079,6 +1079,12 @@ let generate_undefineds vs_ids (Defs defs) = mk_fundef [mk_funcl (prepend_id "undefined_" id) pat (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]] + | TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) -> + [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id)); + mk_fundef [mk_funcl (prepend_id "undefined_" id) + (mk_pat (P_lit (mk_lit L_unit))) + (mk_exp (E_app (mk_id "internal_pick", + [])))]] | _ -> [] in let rec undefined_defs = function diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 8b88a07e..2509f8ef 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -88,7 +88,13 @@ let ocaml_lit (L_aux (lit_aux, _)) = let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) = match pat_aux with - | P_id id -> zencode ctx id + | P_id id -> + begin + match Env.lookup_id id (pat_env_of pat) with + | Local (Immutable, _) | Unbound -> zencode ctx id + | Enum _ -> zencode_upper ctx id + | _ -> failwith "Ocaml: Cannot pattern match on mutable variable or register" + end | P_lit lit -> ocaml_lit lit | P_typ (_, pat) -> ocaml_pat ctx pat | P_tup pats -> parens (separate_map (comma ^^ space) (ocaml_pat ctx) pats) @@ -110,7 +116,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) = | E_block [] -> string "()" | E_block exps -> begin_end (ocaml_block ctx exps) | E_field (exp, id) -> ocaml_atomic_exp ctx exp ^^ dot ^^ zencode ctx id - | E_exit exp -> string "failwith" ^^ space ^^ dquotes (string (String.escaped (string_of_exp exp))) + | E_exit exp -> string "exit 0" | E_case (exp, pexps) -> begin_end (separate space [string "match"; ocaml_atomic_exp ctx exp; string "with"] ^/^ ocaml_pexps ctx pexps) @@ -218,12 +224,12 @@ let rec ocaml_funcl_matches ctx = function let ocaml_funcls ctx = function | [] -> failwith "Ocaml: empty function" | [FCL_aux (FCL_Funcl (id, pat, exp),_)] -> - separate space [string "let"; zencode ctx id; ocaml_pat ctx pat; equals; string "with_return (fun r ->"] + separate space [string "let rec"; zencode ctx id; ocaml_pat ctx pat; equals; string "with_return (fun r ->"] ^//^ ocaml_exp ctx exp ^^ rparen | funcls -> let id = funcls_id funcls in - separate space [string "let"; zencode ctx id; equals; string "function"] + separate space [string "let rec"; zencode ctx id; equals; string "function"] ^//^ ocaml_funcl_matches ctx funcls let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) = @@ -311,8 +317,10 @@ let ocaml_defs (Defs defs) = let ocaml_main spec = concat [separate space [string "open"; string (String.capitalize spec)] ^^ ocaml_def_end; + separate space [string "open"; string "Elf_loader"] ^^ ocaml_def_end; separate space [string "let"; string "()"; equals] ^//^ (string "Random.self_init ();" + ^/^ string "load_elf ();" ^/^ string "initialize_registers ();" ^/^ string "zmain ()") ] @@ -328,20 +336,23 @@ let ocaml_compile spec defs = if Sys.file_exists "_sbuild" then () else Unix.mkdir "_sbuild" 0o775; let cwd = Unix.getcwd () in Unix.chdir "_sbuild"; - let _ = Unix.system ("cp " ^ sail_lib_dir ^ "/sail_lib.ml .") in + let _ = Unix.system ("cp -r " ^ sail_lib_dir ^ "/ocaml_rts/. .") in let out_chan = open_out (spec ^ ".ml") in ocaml_pp_defs out_chan defs; close_out out_chan; if IdSet.mem (mk_id "main") (Initial_check.val_spec_ids defs) then - let out_chan = open_out "main.ml" in - ToChannel.pretty 1. 80 out_chan (ocaml_main spec); - close_out out_chan; - let _ = Unix.system "ocamlbuild -lib nums main.native" in - let _ = Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec) in - () + begin + print_endline "Generating main"; + let out_chan = open_out "main.ml" in + ToChannel.pretty 1. 80 out_chan (ocaml_main spec); + close_out out_chan; + let _ = Unix.system "ocamlbuild -pkg zarith -pkg uint main.native" in + let _ = Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec) in + () + end else - let _ = Unix.system ("ocamlbuild -lib nums " ^ spec ^ ".cmo") in + let _ = Unix.system ("ocamlbuild -pkg zarith -pkg uint " ^ spec ^ ".cmo") in (); Unix.chdir cwd diff --git a/src/type_check.ml b/src/type_check.ml index 4eb0688b..636d4049 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1573,6 +1573,8 @@ let env_of (E_aux (_, (l, tannot))) = env_of_annot (l, tannot) let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot) +let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot) + (* Flow typing *) let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with diff --git a/src/type_check.mli b/src/type_check.mli index 857e0019..fa75b156 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -201,6 +201,7 @@ val typ_of : tannot exp -> typ val typ_of_annot : Ast.l * tannot -> typ val pat_typ_of : tannot pat -> typ +val pat_env_of : tannot pat -> Env.t val effect_of : tannot exp -> effect val effect_of_annot : tannot -> effect -- cgit v1.2.3 From af478ccda9894883427447cb954fc883efbd2217 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 8 Sep 2017 15:54:57 +0100 Subject: Fixed bug when printing Typ_args in Lem AST output --- src/pretty_print_lem_ast.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 5edf9d12..68745bf9 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -208,9 +208,9 @@ and pp_format_effects_lem (Effect_aux(e,l)) = and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) = "(Typ_arg_aux " ^ (match t with - | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")" - | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")" - | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")"); + | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")" + | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")" + | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")") ^ (pp_format_l_lem l) ^ ")" and pp_format_nexp_constraint_lem (NC_aux(nc,l)) = "(NC_aux " ^ -- cgit v1.2.3 From aa1f89abb2f42d085bd123147144c9c5c7ceb22f Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 13 Sep 2017 16:27:34 +0100 Subject: Work on improving Sail error messages - Modified how sail type error messages are displayed. The typechecker, rather than immediately outputing a string has a datatype for error types, which are the pretty-printed using a PPrint pretty-printer. Needs more work for all the error messages. - Error messages now attempt to highlight the part of the file where the error occurred, by printing the line the error is on and highlighting where the error message is in red. Again, this needs to be made more robust, especially when the error messages span multiple lines. Other things - Improved new parser and lexer. Made the lexer & parser handling of colons simpler and more intuitive. - Added some more typechecking test cases --- src/ast_util.mli | 2 ++ src/initial_check.ml | 6 ++-- src/lexer2.mll | 2 -- src/parser2.mly | 57 +++++++++++------------------------ src/reporting_basic.ml | 59 +++++++++++++++++++++++++++---------- src/type_check.ml | 80 ++++++++++++++++++++++++++++++++++++-------------- src/type_check.mli | 4 ++- 7 files changed, 127 insertions(+), 83 deletions(-) (limited to 'src') diff --git a/src/ast_util.mli b/src/ast_util.mli index e6823ee9..6164fc17 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -44,6 +44,8 @@ open Ast +val no_annot : unit annot + val mk_id : string -> id val mk_kid : string -> kid val mk_ord : order_aux -> order diff --git a/src/initial_check.ml b/src/initial_check.ml index 4c0a0db4..1f7840d0 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -1010,7 +1010,7 @@ let initial_kind_env = ] let typschm_of_string order str = - let typschm = Parser2.typschm Lexer2.token (Lexing.from_string str) in + let typschm = Parser2.typschm_eof Lexer2.token (Lexing.from_string str) in let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in typschm @@ -1057,14 +1057,14 @@ let generate_undefineds vs_ids (Defs defs) = if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str] in let undefined_builtins = List.concat - [gen_vs (mk_id "internal_pick") "forall 'a:Type. list('a) -> 'a effect {undef}"; + [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}"; gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}"; gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}"; gen_vs (mk_id "undefined_int") "unit -> int effect {undef}"; gen_vs (mk_id "undefined_string") "unit -> string effect {undef}"; gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}"; (* FIXME: How to handle inc/dec order correctly? *) - gen_vs (mk_id "undefined_vector") "forall 'n 'm 'a:Type. (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}"; + gen_vs (mk_id "undefined_vector") "forall 'n 'm ('a:Type). (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}"; gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"] in let undefined_td = function diff --git a/src/lexer2.mll b/src/lexer2.mll index f5350ea8..a1717d62 100644 --- a/src/lexer2.mll +++ b/src/lexer2.mll @@ -235,8 +235,6 @@ rule token = parse with Not_found -> raise (LexError ("Operator fixity undeclared", Lexing.lexeme_start_p lexbuf)) } | "(*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf } | "*)" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) } - | (tyvar_start startident ident* as i) ":" { TyDecl(r i) } - | (startident ident* as i) ":" { Decl(r i) } | tyvar_start startident ident* as i { TyVar(r i) } | startident ident* as i { if M.mem i kw_table then (M.find i kw_table) () diff --git a/src/parser2.mly b/src/parser2.mly index 42e13721..02a8f09c 100644 --- a/src/parser2.mly +++ b/src/parser2.mly @@ -139,7 +139,7 @@ let rec desugar_rchain chain s e = /*Terminals with content*/ -%token Id TyVar Decl TyDecl +%token Id TyVar %token Num %token String Bin Hex Real @@ -153,9 +153,8 @@ let rec desugar_rchain chain s e = %token Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r %start file -%start typschm -%type typschm -%type defs +%start typschm_eof +%type typschm_eof %type file %% @@ -233,10 +232,6 @@ op7r: Op7r { mk_id (Id $1) $startpos $endpos } op8r: Op8r { mk_id (Id $1) $startpos $endpos } op9r: Op9r { mk_id (Id $1) $startpos $endpos } -decl: - | Decl - { mk_id (Id $1) $startpos $endpos } - id_list: | id { [$1] } @@ -247,10 +242,6 @@ kid: | TyVar { mk_kid $1 $startpos $endpos } -tydecl: - | TyDecl - { mk_kid $1 $startpos $endpos } - kid_list: | kid { [$1] } @@ -515,8 +506,6 @@ kind: { K_aux (K_kind [$1], loc $startpos $endpos) } kopt: - | tydecl kind - { KOpt_aux (KOpt_kind ($2, $1), loc $startpos $endpos) } | Lparen kid Colon kind Rparen { KOpt_aux (KOpt_kind ($4, $2), loc $startpos $endpos) } | kid @@ -589,6 +578,10 @@ typschm: | Forall typquant Dot typ MinusGt typ Effect effect_set { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, $8)) s e) s e) $startpos $endpos } +typschm_eof: + | typschm Eof + { $1 } + pat: | atomic_pat { $1 } @@ -612,14 +605,10 @@ atomic_pat: { mk_pat (P_id $1) $startpos $endpos } | kid { mk_pat (P_var $1) $startpos $endpos } - | tydecl typ - { mk_pat (P_typ ($2, mk_pat (P_var $1) $startpos $endpos($1))) $startpos $endpos } | id Lparen pat_list Rparen { mk_pat (P_app ($1, $3)) $startpos $endpos } | pat Colon typ { mk_pat (P_typ ($3, $1)) $startpos $endpos } - | decl typ - { mk_pat (P_typ ($2, mk_pat (P_id $1) $startpos $endpos($1))) $startpos $endpos } | Lparen pat Rparen { $2 } @@ -646,27 +635,21 @@ lit: { mk_lit (L_string $1) $startpos $endpos } exp: - | cast_exp Colon typ - { mk_exp (E_cast ($3, $1)) $startpos $endpos } - | cast_exp - { $1 } - -cast_exp: | exp0 { $1 } - | atomic_exp Eq cast_exp + | atomic_exp Eq exp { mk_exp (E_assign ($1, $3)) $startpos $endpos } - | Let_ letbind In cast_exp + | Let_ letbind In exp { mk_exp (E_let ($2, $4)) $startpos $endpos } | Lcurly block Rcurly { mk_exp (E_block $2) $startpos $endpos } - | Return cast_exp + | Return exp { mk_exp (E_return $2) $startpos $endpos } - | Throw cast_exp + | Throw exp { mk_exp (E_throw $2) $startpos $endpos } - | If_ exp Then cast_exp Else cast_exp + | If_ exp Then exp Else exp { mk_exp (E_if ($2, $4, $6)) $startpos $endpos } - | If_ exp Then cast_exp + | If_ exp Then exp { mk_exp (E_if ($2, $4, mk_lit_exp L_unit $endpos($4) $endpos($4))) $startpos $endpos } | Match exp Lcurly case_list Rcurly { mk_exp (E_case ($2, $4)) $startpos $endpos } @@ -856,12 +839,14 @@ block: { LB_aux (LB_val_implicit ($1, $3), loc $startpos $endpos) } atomic_exp: + | atomic_exp Colon atomic_typ + { mk_exp (E_cast ($3, $1)) $startpos $endpos } | lit { mk_exp (E_lit $1) $startpos $endpos } - | decl atomic_typ - { mk_exp (E_cast ($2, mk_exp (E_id $1) $startpos $endpos($1))) $startpos $endpos } | id { mk_exp (E_id $1) $startpos $endpos } + | kid + { mk_exp (E_sizeof (mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos } | id Unit { mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos } | id Lparen exp_list Rparen @@ -922,8 +907,6 @@ enum: { $1 :: $3 } struct_field: - | decl typ - { ($2, $1) } | id Colon typ { ($3, $1) } @@ -936,8 +919,6 @@ struct_fields: { $1 :: $3 } type_union: - | decl typ - { Tu_aux (Tu_ty_id ($2, $1), loc $startpos $endpos) } | id Colon typ { Tu_aux (Tu_ty_id ($3, $1), loc $startpos $endpos) } | id @@ -960,14 +941,10 @@ let_def: { $2 } val_spec_def: - | Val decl typschm - { mk_vs (VS_val_spec ($3, $2)) $startpos $endpos } | Val id Colon typschm { mk_vs (VS_val_spec ($4, $2)) $startpos $endpos } register_def: - | Register decl typ - { mk_reg_dec (DEC_reg ($3, $2)) $startpos $endpos } | Register id Colon typ { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos } diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml index 69c5c084..2bd5d5bc 100644 --- a/src/reporting_basic.ml +++ b/src/reporting_basic.ml @@ -87,19 +87,48 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) -let format_pos ff p = ( - Format.fprintf ff "File \"%s\", line %d, character %d:\n" - p.Lexing.pos_fname p.Lexing.pos_lnum (p.Lexing.pos_cnum - p.Lexing.pos_bol); - Format.pp_print_flush ff ()) - - -let format_pos2 ff p1 p2 = ( - Format.fprintf ff "File \"%s\", line %d, character %d to line %d, character %d" - p1.Lexing.pos_fname - p1.Lexing.pos_lnum (p1.Lexing.pos_cnum - p1.Lexing.pos_bol + 1) - p2.Lexing.pos_lnum (p2.Lexing.pos_cnum - p2.Lexing.pos_bol); - Format.pp_print_flush ff () -) +let format_pos ff p = + let open Lexing in + begin + Format.fprintf ff "file \"%s\", line %d, character %d:\n" + p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol); + Format.pp_print_flush ff () + end + +let rec skip_lines in_chan = function + | n when n <= 0 -> () + | n -> input_line in_chan; skip_lines in_chan (n - 1) + +let termcode n = "\x1B[" ^ string_of_int n ^ "m" + +let print_code ff fname lnum1 cnum1 cnum2 = + try + let in_chan = open_in fname in + begin + try + skip_lines in_chan (lnum1 - 1); + let line = input_line in_chan in + Format.fprintf ff "%s%s%s%s%s" + (Str.string_before line cnum1) + (termcode 41) + (Str.string_before (Str.string_after line cnum1) (cnum2 - cnum1)) + (termcode 49) + (Str.string_after line cnum2); + close_in in_chan + with e -> (close_in_noerr in_chan; print_endline (Printexc.to_string e)) + end + with _ -> () + +let format_pos2 ff p1 p2 = + let open Lexing in + begin + Format.fprintf ff "file \"%s\", line %d, character %d to line %d, character %d\n\n" + p1.pos_fname + p1.pos_lnum (p1.pos_cnum - p1.pos_bol + 1) + p2.pos_lnum (p2.pos_cnum - p2.pos_bol); + print_code ff p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) (p2.pos_cnum - p2.pos_bol); + Format.pp_print_flush ff () + end (* reads the part between p1 and p2 from the file *) @@ -171,12 +200,12 @@ let loc_to_string l = type pos_or_loc = Loc of Parse_ast.l | LocD of Parse_ast.l * Parse_ast.l | Pos of Lexing.position let print_err_internal fatal verb_loc p_l m1 m2 = + Format.eprintf "%s at " m1; let _ = (match p_l with Pos p -> print_err_pos p | Loc l -> print_err_loc l | LocD (l1,l2) -> print_err_loc l1; Format.fprintf Format.err_formatter " and "; print_err_loc l2) in - let m12 = if String.length m2 = 0 then "" else ": " in - Format.eprintf " %s%s%s\n" m1 m12 m2; + Format.eprintf "%s\n" m2; if verb_loc then (match p_l with Loc l -> format_loc_source Format.err_formatter l; Format.pp_print_newline Format.err_formatter (); | _ -> ()); diff --git a/src/type_check.ml b/src/type_check.ml index 636d4049..f952d0d6 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -65,9 +65,47 @@ let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ m) el let typ_warning m = prerr_endline ("Warning: " ^ m) -exception Type_error of l * string;; +type type_error = + (* First parameter is the error that caused us to start doing type + coercions, the second is the errors encountered by all possible + coerctions *) + | Err_no_casts of type_error * type_error list + | Err_subtype of typ * typ * n_constraint list + | Err_other of string + +let pp_type_error err = + let open PPrint in + let rec pp_err = function + | Err_no_casts (trigger, []) -> + (string "Tried performing type coercion because" ^//^ pp_err trigger) + ^/^ string "No possible coercions" + | Err_no_casts (trigger, errs) -> + (string "Tried performing type coerction because" ^//^ pp_err trigger) + | Err_subtype (typ1, typ2, []) -> + separate space [ string (string_of_typ typ1); + string "is not a subtype of"; + string (string_of_typ typ2) ] + | Err_subtype (typ1, typ2, constrs) -> + separate space [ string (string_of_typ typ1); + string "is not a subtype of"; + string (string_of_typ typ2) ] + ^/^ string "in context" + ^//^ string (string_of_list ", " string_of_n_constraint constrs) + | Err_other str -> string str + in + pp_err err + +let rec string_of_type_error err = + let open PPrint in + let b = Buffer.create 20 in + ToBuffer.pretty 1. 120 b (pp_type_error err); + "\n" ^ Buffer.contents b + +exception Type_error of l * type_error;; + +let typ_error l m = raise (Type_error (l, Err_other m)) -let typ_error l m = raise (Type_error (l, m)) +let typ_raise l err = raise (Type_error (l, err)) let deinfix = function | Id_aux (Id v, l) -> Id_aux (DeIid v, l) @@ -1447,9 +1485,7 @@ let rec subtyp l env typ1 typ2 = | _, None -> if subtyp_tnf env (normalize_typ env typ1) (normalize_typ env typ2) then () - else typ_error l (string_of_typ typ1 - ^ " is not a subtype of " ^ string_of_typ typ2 - ^ " in context " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)) + else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env)) let typ_equality l env typ1 typ2 = subtyp l env typ1 typ2; subtyp l env typ2 typ1 @@ -1782,7 +1818,7 @@ let crule r env exp typ = let checked_exp = r env exp typ in decr depth; checked_exp with - | Type_error (l, m) -> decr depth; typ_error l m + | Type_error (l, err) -> decr depth; typ_raise l err let irule r env exp = incr depth; @@ -1792,7 +1828,7 @@ let irule r env exp = decr depth; inferred_exp with - | Type_error (l, m) -> decr depth; typ_error l m + | Type_error (l, err) -> decr depth; typ_raise l err let strip_exp : 'a exp -> unit exp = function exp -> map_exp_annot (fun (l, _) -> (l, ())) exp let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) -> (l, ())) pat @@ -1928,7 +1964,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | (f :: fs) -> begin typ_print ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"); try crule check_exp env (E_aux (E_app (f, xs), (l, ()))) typ with - | Type_error (_, m) -> typ_print ("Error : " ^ m); try_overload fs + | Type_error (_, err) -> typ_print ("Error : " ^ string_of_type_error err); try_overload fs end in try_overload (Env.get_overloads f env) @@ -1991,15 +2027,15 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ = let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in - let rec try_casts m = function - | [] -> typ_error l ("No valid casts:\n" ^ m) + let rec try_casts trigger errs = function + | [] -> typ_raise l (Err_no_casts (trigger, errs)) | (cast :: casts) -> begin typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " to " ^ string_of_typ typ); try let checked_cast = crule check_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) typ in annot_exp (E_cast (typ, checked_cast)) typ with - | Type_error (_, m) -> try_casts m casts + | Type_error (_, err) -> try_casts trigger (err :: errs) casts end in begin @@ -2007,10 +2043,10 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ = typ_debug ("PERFORMING TYPE COERCION: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ); subtyp l env (typ_of annotated_exp) typ; annotated_exp with - | Type_error (_, m) when Env.allow_casts env -> + | Type_error (_, trigger) when Env.allow_casts env -> let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in - try_casts "" casts - | Type_error (l, m) -> typ_error l ("Subtype error " ^ m) + try_casts trigger [] casts + | Type_error (l, err) -> typ_error l "Subtype error" end (* type_coercion_unify env exp typ attempts to coerce exp to a type @@ -2021,8 +2057,8 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ = and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ = let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in - let rec try_casts m = function - | [] -> unify_error l ("No valid casts resulted in unification:\n" ^ m) + let rec try_casts = function + | [] -> unify_error l "No valid casts resulted in unification" | (cast :: casts) -> begin typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " for unification"); try @@ -2030,8 +2066,8 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ = let ityp = typ_of inferred_cast in annot_exp (E_cast (ityp, inferred_cast)) ityp, unify l env typ ityp with - | Type_error (_, m) -> try_casts m casts - | Unification_error (_, m) -> try_casts m casts + | Type_error (_, err) -> try_casts casts + | Unification_error (_, err) -> try_casts casts end in begin @@ -2041,7 +2077,7 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ = with | Unification_error (_, m) when Env.allow_casts env -> let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in - try_casts "" casts + try_casts casts end and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) = @@ -2497,7 +2533,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | (f :: fs) -> begin typ_print ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")"); try irule infer_exp env (E_aux (E_app (f, xs), (l, ()))) with - | Type_error (_, m) -> typ_print ("Error: " ^ m); try_overload fs + | Type_error (_, err) -> typ_print ("Overload error"); try_overload fs end in try_overload (Env.get_overloads f env) @@ -3125,7 +3161,7 @@ let mk_synonym typq typ = typ_subst_typ (kopt_kid kopt) (unaux_typ arg) typ, ncs | kopt :: kopts, Typ_arg_aux (Typ_arg_order arg, _) :: args when is_order_kopt kopt -> let typ, ncs = subst_args kopts args in - typ_subst_order (kopt_kid kopt) (unaux_order arg) typ, ncs + typ_subst_order (kopt_kid kopt) (unaux_order arg) typ, ncs | [], [] -> typ, ncs | _, Typ_arg_aux (_, l) :: _ -> typ_error l "Synonym applied to bad arguments" | _, _ -> typ_error Parse_ast.Unknown "Synonym applied to bad arguments" @@ -3193,4 +3229,4 @@ let rec check' env (Defs defs) = let check env defs = try check' env defs with - | Type_error (l, m) -> raise (Reporting_basic.err_typ l m) + | Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err)) diff --git a/src/type_check.mli b/src/type_check.mli index fa75b156..ca2fb90c 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -47,7 +47,9 @@ open Ast_util val opt_tc_debug : int ref val opt_no_effects : bool ref -exception Type_error of l * string;; +type type_error + +exception Type_error of l * type_error;; type mut = Immutable | Mutable -- cgit v1.2.3 From 3914be09d200eb92ed1e317123f56667d597b5a7 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 13 Sep 2017 17:19:13 +0100 Subject: Fix a regression when writing to a register via a reference in a vector such as GPR This was wrongly translated as an update of the vector of references. --- src/Makefile | 2 +- src/ast_util.ml | 20 +++++++++++++++ src/ast_util.mli | 3 +++ src/pretty_print_lem.ml | 19 +++++++++++--- src/pretty_print_lem_ast.ml | 2 +- src/rewriter.ml | 62 +++++++++++++++++++-------------------------- 6 files changed, 66 insertions(+), 42 deletions(-) (limited to 'src') diff --git a/src/Makefile b/src/Makefile index 6cfcf874..1bac0b71 100644 --- a/src/Makefile +++ b/src/Makefile @@ -177,7 +177,7 @@ _build/cheri_embed_types_sequential.lem: $(CHERI_SAILS) ./sail.native _build/Cheri_embed_sequential.thy: _build/cheri_embed_types_sequential.lem cd _build ;\ - lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem $(MIPS_SAIL_DIR)/mips_extras_embed_sequential.lem cheri_embed_types_sequential.lem cheri_embed_sequential.lem + lem -isa -outdir . -lib ../lem_interp -lib ../gen_lib $(MIPS_SAIL_DIR)/mips_extras_embed_sequential.lem cheri_embed_types_sequential.lem cheri_embed_sequential.lem _build/mips_all.sail: $(MIPS_SAILS) cat $(MIPS_SAILS) > $@ diff --git a/src/ast_util.ml b/src/ast_util.ml index aef1a05d..2f630021 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -618,6 +618,22 @@ let rec simplify_nexp (Nexp_aux (nexp, l)) = | Nexp_exp of nexp (* exponential *) | Nexp_neg of nexp (* For internal use *) *) +let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) = + let rewrap e_aux = E_aux (e_aux, annot) in + match lexp_aux with + | LEXP_id id | LEXP_cast (_, id) -> rewrap (E_id id) + | LEXP_tup les -> + let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with + | LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot) + | _ -> + raise (Reporting_basic.err_unreachable l + ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in + rewrap (E_tuple (List.map get_id les)) + | LEXP_vector (lexp, e) -> rewrap (E_vector_access (lexp_to_exp lexp, e)) + | LEXP_vector_range (lexp, e1, e2) -> rewrap (E_vector_subrange (lexp_to_exp lexp, e1, e2)) + | LEXP_field (lexp, id) -> rewrap (E_field (lexp_to_exp lexp, id)) + | LEXP_memory (id, exps) -> rewrap (E_app (id, exps)) + let rec is_number (Typ_aux (t,_)) = match t with | Typ_app (Id_aux (Id "range", _),_) @@ -625,6 +641,10 @@ let rec is_number (Typ_aux (t,_)) = | Typ_app (Id_aux (Id "atom", _),_) -> true | _ -> false +let is_reftyp (Typ_aux (typ_aux, _)) = match typ_aux with + | Typ_app (id, _) -> string_of_id id = "register" || string_of_id id = "reg" + | _ -> false + let rec is_vector_typ = function | Typ_aux (Typ_app (Id_aux (Id "vector",_), [_;_;_;_]), _) -> true | Typ_aux (Typ_app (Id_aux (Id "register",_), [Typ_arg_aux (Typ_arg_typ rtyp,_)]), _) -> diff --git a/src/ast_util.mli b/src/ast_util.mli index 6164fc17..246e0ebd 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -203,7 +203,10 @@ val nexp_identical : nexp -> nexp -> bool val is_nexp_constant : nexp -> bool val simplify_nexp : nexp -> nexp +val lexp_to_exp : 'a lexp -> 'a exp + val is_number : typ -> bool +val is_reftyp : typ -> bool val is_vector_typ : typ -> bool val is_bit_typ : typ -> bool val is_bitvector_typ : typ -> bool diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 5e0d39a0..e2c8c0ac 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -418,10 +418,21 @@ let doc_exp_lem, doc_let_lem = (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ parens (string "update_reg_field_bit" ^/^ field_ref ^/^ expY e2) ^/^ expY e))) | _ -> - liftR ((prefix 2 1) - (string "update_reg") - (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ - parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e)) + (match le with + | LEXP_aux (_, (_, Some (_, Typ_aux (Typ_app (vector, [_; _; _; Typ_arg_aux (Typ_arg_typ etyp, _)]), _), _))) + when is_reftyp etyp && string_of_id vector = "vector" -> + (* Special case vectors of register references *) + let deref = + parens (separate space [ + string "access"; + expY (lexp_to_exp le); + expY e2 + ]) in + liftR ((prefix 2 1) (string "write_reg") (deref ^/^ expY e)) + | _ -> + liftR ((prefix 2 1) (string "update_reg") + (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ + parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e))) ) (* | LEXP_field (le,id) when is_bit_typ t -> liftR ((prefix 2 1) diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml index 68745bf9..73f06d1a 100644 --- a/src/pretty_print_lem_ast.ml +++ b/src/pretty_print_lem_ast.ml @@ -210,7 +210,7 @@ and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) = (match t with | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")" | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")" - | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")") ^ + | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")") ^ " " ^ (pp_format_l_lem l) ^ ")" and pp_format_nexp_constraint_lem (NC_aux(nc,l)) = "(NC_aux " ^ diff --git a/src/rewriter.ml b/src/rewriter.ml index 78b29200..d6a6aa2f 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -2209,29 +2209,19 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with | Some (_, _, eff) -> effectful_effs eff | _ -> false -let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = match lexp with - | LEXP_id id | LEXP_cast (_, id) -> - (le, E_aux (E_id id, annot), (fun exp -> exp)) - | LEXP_tup les -> - let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with - | LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot) - | _ -> - raise (Reporting_basic.err_unreachable l - ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in - (le, E_aux (E_tuple (List.map get_id les), annot), (fun exp -> exp)) +let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = + match lexp with + | LEXP_id _ | LEXP_cast (_, _) | LEXP_tup _ -> (le, (fun exp -> exp)) | LEXP_vector (lexp, e) -> - let (lexp, access, rexp) = rewrite_local_lexp lexp in - (lexp, E_aux (E_vector_access (access, e), annot), - (fun exp -> rexp (E_aux (E_vector_update (access, e, exp), annot)))) + let (lhs, rhs) = rewrite_local_lexp lexp in + (lhs, (fun exp -> rhs (E_aux (E_vector_update (lexp_to_exp lexp, e, exp), annot)))) | LEXP_vector_range (lexp, e1, e2) -> - let (lexp, access, rexp) = rewrite_local_lexp lexp in - (lexp, E_aux (E_vector_subrange (access, e1, e2), annot), - (fun exp -> rexp (E_aux (E_vector_update_subrange (access, e1, e2, exp), annot)))) + let (lhs, rhs) = rewrite_local_lexp lexp in + (lhs, (fun exp -> rhs (E_aux (E_vector_update_subrange (lexp_to_exp lexp, e1, e2, exp), annot)))) | LEXP_field (lexp, id) -> - let (lexp, access, rexp) = rewrite_local_lexp lexp in + let (lhs, rhs) = rewrite_local_lexp lexp in let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in - (lexp, E_aux (E_field (access, id), annot), - (fun exp -> rexp (E_aux (E_record_update (access, field_update exp), annot)))) + (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), annot)))) | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le)) (*Expects to be called after rewrite_defs; thus the following should not appear: @@ -2250,7 +2240,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f | [] -> [] | (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps when lexp_is_local_intro le env && not (lexp_is_effectful le) -> - let (le', _, re') = rewrite_local_lexp le in + let (le', re') = rewrite_local_lexp le in let e' = re' (rewrite_base e) in let exps' = walker exps in let effects = union_eff_exps exps' in @@ -2303,7 +2293,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f rewrap (E_block (walker exps)) | E_assign(le,e) when lexp_is_local_intro le (env_of full_exp) && not (lexp_is_effectful le) -> - let (le', _, re') = rewrite_local_lexp le in + let (le', re') = rewrite_local_lexp le in let e' = re' (rewrite_base e) in let block = E_aux (E_block [], simple_annot l unit_typ) in fix_eff_exp (E_aux (E_internal_let(le', e', block), annot)) @@ -2635,7 +2625,7 @@ let rewrite_simple_assignments defs = let env = env_of_annot annot in match e_aux with | E_assign (lexp, exp) -> - let (lexp, _, rhs) = rewrite_local_lexp lexp in + let (lexp, rhs) = rewrite_local_lexp lexp in let assign = mk_exp (E_assign (strip_lexp lexp, strip_exp (rhs exp))) in check_exp env assign unit_typ | _ -> E_aux (e_aux, annot) @@ -2977,9 +2967,9 @@ let rewrite_defs_effectful_let_expressions = let e_let (lb,body) = match lb with | LB_aux (LB_val_implicit (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _) - when lexp_is_local le (env_of_annot annot) -> + when lexp_is_local le (env_of_annot annot) && not (lexp_is_effectful le) -> (* Rewrite assignments to local variables into let bindings *) - let (lhs, _, rhs) = rewrite_local_lexp le in + let (lhs, rhs) = rewrite_local_lexp le in E_let (LB_aux (LB_val_implicit (pat_of_local_lexp lhs, rhs exp), annot), body) | LB_aux (LB_val_explicit (_,pat,exp'),annot') | LB_aux (LB_val_implicit (pat,exp'),annot') -> @@ -3023,28 +3013,28 @@ let eqidtyp (id1,_) (id2,_) = name1 = name2 let find_introduced_vars exp = - let lEXP_aux ((ids,lexp),annot) = - let ids = match lexp, annot with - | LEXP_id id, (_, Some (env, _, _)) - | LEXP_cast (_, id), (_, Some (env, _, _)) + let e_aux ((ids,e_aux),annot) = + let ids = match e_aux, annot with + | E_internal_let (LEXP_aux (LEXP_id id, _), _, _), (_, Some (env, _, _)) + | E_internal_let (LEXP_aux (LEXP_cast (_, id), _), _, _), (_, Some (env, _, _)) when id_is_unbound id env -> IdSet.add id ids | _ -> ids in - (ids, LEXP_aux (lexp, annot)) in + (ids, E_aux (e_aux, annot)) in fst (fold_exp - { (compute_exp_alg IdSet.empty IdSet.union) with lEXP_aux = lEXP_aux } exp) + { (compute_exp_alg IdSet.empty IdSet.union) with e_aux = e_aux } exp) let find_updated_vars exp = let intros = find_introduced_vars exp in - let lEXP_aux ((ids,lexp),annot) = - let ids = match lexp, annot with - | LEXP_id id, (_, Some (env, _, _)) - | LEXP_cast (_, id), (_, Some (env, _, _)) + let e_aux ((ids,e_aux),annot) = + let ids = match e_aux, annot with + | E_assign (LEXP_aux (LEXP_id id, _), _), (_, Some (env, _, _)) + | E_assign (LEXP_aux (LEXP_cast (_, id), _), _), (_, Some (env, _, _)) when id_is_local_var id env && not (IdSet.mem id intros) -> (id, annot) :: ids | _ -> ids in - (ids, LEXP_aux (lexp, annot)) in + (ids, E_aux (e_aux, annot)) in dedup eqidtyp (fst (fold_exp - { (compute_exp_alg [] (@)) with lEXP_aux = lEXP_aux } exp)) + { (compute_exp_alg [] (@)) with e_aux = e_aux } exp)) let swaptyp typ (l,tannot) = match tannot with | Some (env, typ', eff) -> (l, Some (env, typ, eff)) -- cgit v1.2.3 From cb90735550541fa6752aaad82ff809d84e6c5f88 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Wed, 13 Sep 2017 19:03:31 +0100 Subject: Fix some more test cases --- src/pretty_print_lem.ml | 23 ++++++++++++++++------- src/rewriter.ml | 15 ++++++++++++++- 2 files changed, 30 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index e2c8c0ac..1bfb19aa 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -530,14 +530,19 @@ let doc_exp_lem, doc_let_lem = if contains_bitvector_typ 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 + if aexp_needed then parens (align taepp) else taepp*) | Id_aux (Id "length",_) -> + (* Another temporary hack: The sizeof rewriting introduces calls to + "length", and the disambiguation between the length function on + bitvectors and vectors of other element types should be done by + the type checker, but type checking after rewriting steps is + currently broken. *) let [arg] = args in let targ = typ_of arg in - let call = if is_bitvector_typ targ then "bvlength" else "length" in + let call = if mwords && is_bitvector_typ targ then "bvlength" else "length" in let epp = separate space [string call;expY arg] in if aexp_needed then parens (align epp) else epp - | Id_aux (Id "bool_not", _) -> + (*)| Id_aux (Id "bool_not", _) -> let [a] = args in let epp = align (string "~" ^^ expY a) in if aexp_needed then parens (align epp) else epp *) @@ -709,7 +714,9 @@ let doc_exp_lem, doc_let_lem = | _ -> parens (separate_map comma expN exps)) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> let recordtyp = match annot with - | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env -> + | Some (env, Typ_aux (Typ_id tid,_), _) + | Some (env, Typ_aux (Typ_app (tid, _), _), _) + when Env.is_record tid env -> tid | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in let epp = anglebars (space ^^ (align (separate_map @@ -717,9 +724,11 @@ let doc_exp_lem, doc_let_lem = (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in if aexp_needed then parens epp else epp | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> - let (E_aux (_, (_, eannot))) = e in - let recordtyp = match eannot with - | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env -> + (* let (E_aux (_, (_, eannot))) = e in *) + let recordtyp = match annot with + | Some (env, Typ_aux (Typ_id tid,_), _) + | Some (env, Typ_aux (Typ_app (tid, _), _), _) + when Env.is_record tid env -> tid | _ -> raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps)) diff --git a/src/rewriter.ml b/src/rewriter.ml index d6a6aa2f..62ea6be7 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -2220,8 +2220,9 @@ let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = (lhs, (fun exp -> rhs (E_aux (E_vector_update_subrange (lexp_to_exp lexp, e1, e2, exp), annot)))) | LEXP_field (lexp, id) -> let (lhs, rhs) = rewrite_local_lexp lexp in + let (LEXP_aux (_, recannot)) = lexp in let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in - (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), annot)))) + (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), recannot)))) | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le)) (*Expects to be called after rewrite_defs; thus the following should not appear: @@ -2946,6 +2947,18 @@ let rewrite_defs_letbind_effects = let _ = reset_fresh_name_counter () in FCL_aux (FCL_Funcl (id,pat,n_exp_term newreturn exp),annot) in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),fdannot) in + let rewrite_def rewriters = function + | DEF_val (LB_aux (lb, annot)) -> + let rewrap lb = DEF_val (LB_aux (lb, annot)) in + begin + match lb with + | LB_val_implicit (pat, exp) -> + rewrap (LB_val_implicit (pat, n_exp_term (effectful exp) exp)) + | LB_val_explicit (ts, pat, exp) -> + rewrap (LB_val_explicit (ts, pat, n_exp_term (effectful exp) exp)) + end + | DEF_fundef fdef -> DEF_fundef (rewrite_fun rewriters fdef) + | d -> d in rewrite_defs_base {rewrite_exp = rewrite_exp ; rewrite_pat = rewrite_pat -- cgit v1.2.3 From 4e7a568bb57337d41dda893044ed84b66e62752f Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Thu, 14 Sep 2017 13:55:17 +0100 Subject: Fix bug in topological sorting --- src/rewriter.ml | 2 +- src/spec_analysis.ml | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/rewriter.ml b/src/rewriter.ml index 62ea6be7..fed8408d 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -3429,7 +3429,7 @@ let rewrite_defs_remove_e_assign = let recheck_defs defs = fst (check initial_env defs) let rewrite_defs_lem =[ - (* top_sort_defs; *) + top_sort_defs; rewrite_trivial_sizeof; rewrite_sizeof; rewrite_defs_remove_vector_concat; diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 5281ef27..d349037e 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -350,6 +350,7 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset. b,used,set | E_exit e -> fv_of_exp consider_var bound used set e | E_assert(c,m) -> list_fv bound used set [c;m] + | E_return e -> fv_of_exp consider_var bound used set e | _ -> bound,used,set and fv_of_pes consider_var bound used set pes = -- cgit v1.2.3