diff options
| -rw-r--r-- | lib/ocaml_rts/elf_loader.ml | 13 | ||||
| -rw-r--r-- | lib/ocaml_rts/sail_lib.ml | 2 | ||||
| -rw-r--r-- | src/ast_util.ml | 15 | ||||
| -rw-r--r-- | src/ast_util.mli | 6 | ||||
| -rw-r--r-- | src/type_check.ml | 5 | ||||
| -rw-r--r-- | src/type_check.mli | 13 | ||||
| -rwxr-xr-x | test/ocaml/run_tests.sh | 2 |
7 files changed, 45 insertions, 11 deletions
diff --git a/lib/ocaml_rts/elf_loader.ml b/lib/ocaml_rts/elf_loader.ml index 4e35a192..ab49c57b 100644 --- a/lib/ocaml_rts/elf_loader.ml +++ b/lib/ocaml_rts/elf_loader.ml @@ -122,11 +122,8 @@ let load_segment seg = List.iteri (fun i byte -> Sail_lib.wram (add_big_int paddr (big_int_of_int i)) byte) (List.map int_of_char bs) let load_elf () = - let name = - match !opt_file_arguments with - | (name :: _) -> name - | [] -> failwith "Must provide an elf file" - in - let segments, e_entry = read name in - List.iter load_segment segments; - () + match !opt_file_arguments with + | (name :: _) -> + let segments, e_entry = read name in + List.iter load_segment segments + | [] -> () diff --git a/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml index 0602a3d0..6c0a0f64 100644 --- a/lib/ocaml_rts/sail_lib.ml +++ b/lib/ocaml_rts/sail_lib.ml @@ -315,3 +315,5 @@ let shl_int (n, m) = shift_left_big_int n (int_of_big_int m) let shr_int (n, m) = shift_right_big_int n (int_of_big_int m) let debug (str1, n, str2, v) = prerr_endline (str1 ^ string_of_big_int n ^ str2 ^ string_of_bits v) + +let eq_string (str1, str2) = String.compare str1 str2 == 0 diff --git a/src/ast_util.ml b/src/ast_util.ml index 2f630021..46c79764 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -70,6 +70,14 @@ let mk_lit_exp lit_aux = mk_exp (E_lit (mk_lit lit_aux)) let mk_funcl id pat body = FCL_aux (FCL_Funcl (id, pat, body), no_annot) +let mk_qi_nc nc = QI_aux (QI_const nc, Parse_ast.Unknown) + +let mk_qi_id bk kid = + let kopt = + KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (bk, Parse_ast.Unknown)], Parse_ast.Unknown), kid), Parse_ast.Unknown) + in + QI_aux (QI_id kopt, Parse_ast.Unknown) + let mk_fundef funcls = let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in let effect_opt = Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown) in @@ -155,6 +163,8 @@ let range_typ nexp1 nexp2 = let bool_typ = mk_id_typ (mk_id "bool") let string_typ = mk_id_typ (mk_id "string") let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)])) +let tuple_typ typs = mk_typ (Typ_tup typs) +let function_typ typ1 typ2 eff = mk_typ (Typ_fn (typ1, typ2, eff)) let vector_typ n m ord typ = mk_typ (Typ_app (mk_id "vector", @@ -173,6 +183,7 @@ let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown) let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown) let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown) +let nc_set kid ints = mk_nc (NC_nat_set_bounded (kid, ints)) let nc_eq n1 n2 = mk_nc (NC_fixed (n1, n2)) let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2)) let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown) @@ -297,6 +308,10 @@ let string_of_id = function let id_of_kid = function | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l) +let kid_of_id = function + | Id_aux (Id v, l) -> Kid_aux (Var ("'" ^ v), l) + | Id_aux (DeIid v, _) -> assert false + let string_of_kid = function | Kid_aux (Var v, _) -> v diff --git a/src/ast_util.mli b/src/ast_util.mli index 246e0ebd..33d65ede 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -60,6 +60,8 @@ val mk_funcl : id -> unit pat -> unit exp -> unit funcl val mk_fundef : (unit funcl) list -> unit def val mk_val_spec : val_spec_aux -> unit def val mk_typschm : typquant -> typ -> typschm +val mk_qi_id : base_kind_aux -> kid -> quant_item +val mk_qi_nc : n_constraint -> quant_item val mk_fexp : id -> unit exp -> unit fexp val mk_fexps : (unit fexp) list -> unit fexps val mk_letbind : unit pat -> unit exp -> unit letbind @@ -94,6 +96,8 @@ val real_typ : typ val vector_typ : nexp -> nexp -> order -> typ -> typ val list_typ : typ -> typ val exc_typ : typ +val tuple_typ : typ list -> typ +val function_typ : typ -> typ -> effect -> typ val no_effect : effect val mk_effect : base_effect_aux list -> effect @@ -120,6 +124,7 @@ val nc_and : n_constraint -> n_constraint -> n_constraint val nc_or : n_constraint -> n_constraint -> n_constraint val nc_true : n_constraint val nc_false : n_constraint +val nc_set : kid -> int list -> n_constraint val quant_items : typquant -> quant_item list @@ -164,6 +169,7 @@ val string_of_index_range : index_range -> string val id_of_fundef : 'a fundef -> id val id_of_kid : kid -> id +val kid_of_id : id -> kid val prepend_id : string -> id -> id diff --git a/src/type_check.ml b/src/type_check.ml index 0e1928dd..f89ff0d3 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -72,6 +72,7 @@ type type_error = | Err_no_casts of type_error * type_error list | Err_unresolved_quants of id * quant_item list | Err_subtype of typ * typ * n_constraint list + | Err_no_num_ident of id | Err_other of string let pp_type_error err = @@ -92,6 +93,8 @@ let pp_type_error err = string (string_of_typ typ2) ] ^/^ string "in context" ^//^ string (string_of_list ", " string_of_n_constraint constrs) + | Err_no_num_ident id -> + string "No num identifier" ^^ space ^^ string (string_of_id id) | Err_other str -> string str in pp_err err @@ -770,7 +773,7 @@ end = struct let get_num_def id env = try Bindings.find id env.num_defs with - | Not_found -> typ_error (id_loc id) ("No Num identifier " ^ string_of_id id) + | Not_found -> typ_raise (id_loc id) (Err_no_num_ident id) let rec wf_constraint env (NC_aux (nc, _)) = match nc with diff --git a/src/type_check.mli b/src/type_check.mli index ca2fb90c..6073913b 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -47,10 +47,17 @@ open Ast_util val opt_tc_debug : int ref val opt_no_effects : bool ref -type type_error +type type_error = + | Err_no_casts of type_error * type_error list + | Err_unresolved_quants of id * quant_item list + | Err_subtype of typ * typ * n_constraint list + | Err_no_num_ident of id + | Err_other of string exception Type_error of l * type_error;; +val string_of_type_error : type_error -> string + type mut = Immutable | Mutable type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound @@ -249,4 +256,8 @@ Some invariants that will hold of a fully checked AST are: for them to have type annotations. *) val check : Env.t -> 'a defs -> tannot defs * Env.t +(* Like check but throws type_errors rather than Sail generic errors + from Reporting_basic. *) +val check' : Env.t -> 'a defs -> tannot defs * Env.t + val initial_env : Env.t diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh index 4454aa48..481ff80f 100755 --- a/test/ocaml/run_tests.sh +++ b/test/ocaml/run_tests.sh @@ -43,7 +43,7 @@ function finish_suite { fail=0 } -SAILLIBDIR="$DIR" +SAILLIBDIR="$DIR/../../lib/" printf "<testsuites>\n" >> $DIR/tests.xml |