summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml2
-rw-r--r--src/jib/jib_compile.mli7
-rw-r--r--src/jib/jib_optimize.ml12
-rw-r--r--src/monomorphise.ml31
-rw-r--r--src/process_file.ml9
-rw-r--r--src/reporting.ml16
-rw-r--r--src/reporting.mli18
-rw-r--r--src/slice.ml16
8 files changed, 58 insertions, 53 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 065b443c..6544d3b4 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -60,7 +60,7 @@ let lvar_typ = function
| Local (_, typ) -> typ
| Register (_, _, typ) -> typ
| Enum typ -> typ
- | Unbound -> failwith "No type for unbound variable"
+ | Unbound -> Reporting.unreachable Parse_ast.Unknown __POS__ "No type for unbound variable"
let no_annot = (Parse_ast.Unknown, ())
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 6269b40d..c863b6ba 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -83,10 +83,9 @@ val initial_ctx : Env.t -> ctx
(** {2 Compilation functions} *)
(** The Config module specifies static configuration for compiling
- Sail into Jib. We have to provide a conversion
- function from Sail types into Jib types, as well as a function that
- optimizes ANF expressions (which can just be the identity function)
- *)
+ Sail into Jib. We have to provide a conversion function from Sail
+ types into Jib types, as well as a function that optimizes ANF
+ expressions (which can just be the identity function) *)
module type Config = sig
val convert_typ : ctx -> typ -> ctyp
val optimize_anf : ctx -> typ aexp -> typ aexp
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index 82906cb6..f4d9c9c2 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -345,6 +345,15 @@ let rec remove_pointless_goto = function
instr :: remove_pointless_goto instrs
| [] -> []
+let rec remove_pointless_exit = function
+ | I_aux (I_end id, aux) :: I_aux (I_end _, _) :: instrs ->
+ I_aux (I_end id, aux) :: remove_pointless_exit instrs
+ | I_aux (I_end id, aux) :: I_aux (I_undefined _, _) :: instrs ->
+ I_aux (I_end id, aux) :: remove_pointless_exit instrs
+ | instr :: instrs ->
+ instr :: remove_pointless_exit instrs
+ | [] -> []
+
module StringSet = Set.Make(String)
let rec get_used_labels set = function
@@ -362,7 +371,6 @@ let remove_unused_labels instrs =
in
go [] instrs
-
let remove_dead_after_goto instrs =
let rec go acc = function
| (I_aux (I_goto _, _) as instr) :: instrs -> go_dead (instr :: acc) instrs
@@ -377,7 +385,7 @@ let remove_dead_after_goto instrs =
let rec remove_dead_code instrs =
let instrs' =
- instrs |> remove_unused_labels |> remove_pointless_goto |> remove_dead_after_goto
+ instrs |> remove_unused_labels |> remove_pointless_goto |> remove_dead_after_goto |> remove_pointless_exit
in
if List.length instrs' < List.length instrs then
remove_dead_code instrs'
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 5168d16a..0785c3cd 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -252,12 +252,11 @@ let rec size_nvars_nexp (Nexp_aux (ne,_)) =
let split_src_type all_errors env id ty (TypQ_aux (q,ql)) =
let cannot l msg default =
let open Reporting in
- let error = Err_general (l, msg) in
match all_errors with
- | None -> raise (Fatal_error error)
+ | None -> raise (err_general l msg)
| Some flag -> begin
flag := false;
- print_error error;
+ print_err l "Error" msg;
default
end
in
@@ -659,14 +658,12 @@ let split_defs target all_errors splits env defs =
let renew_id (Id_aux (id,l)) = Id_aux (id,new_l) in
let cannot msg =
let open Reporting in
- let error =
- Err_general (pat_l,
- ("Cannot split type " ^ string_of_typ typ ^ " for variable " ^ v ^ ": " ^ msg))
- in if all_errors
+ let error_msg = "Cannot split type " ^ string_of_typ typ ^ " for variable " ^ v ^ ": " ^ msg in
+ if all_errors
then (no_errors_happened := false;
- print_error error;
+ print_err pat_l "" error_msg;
[P_aux (P_id var,(pat_l,annot)),[],[],KBindings.empty])
- else raise (Fatal_error error)
+ else raise (err_general pat_l error_msg)
in
match ty with
| Typ_id (Id_aux (Id "bool",_)) | Typ_app (Id_aux (Id "atom_bool", _), [_]) ->
@@ -951,13 +948,11 @@ let split_defs target all_errors splits env defs =
let size = List.length lst in
if size > size_set_limit then
let open Reporting in
- let error =
- Err_general (l, "Case split is too large (" ^ string_of_int size ^
- " > limit " ^ string_of_int size_set_limit ^ ")")
- in if all_errors
- then (no_errors_happened := false;
- print_error error; false)
- else raise (Fatal_error error)
+ let error_msg = "Case split is too large (" ^ string_of_int size ^ " > limit " ^ string_of_int size_set_limit ^ ")" in
+ if all_errors
+ then (no_errors_happened := false;
+ print_err l "" error_msg; false)
+ else raise (err_general l error_msg)
else true
in
@@ -1927,9 +1922,7 @@ let refine_dependency env (E_aux (e,(l,annot)) as exp) pexps =
with
| Some pats ->
if l = Parse_ast.Unknown then
- (Reporting.print_error
- (Reporting.Err_general
- (l, "No location for pattern match: " ^ string_of_exp exp));
+ (Reporting.print_err l "" ("No location for pattern match: " ^ string_of_exp exp);
None)
else
Some (Have (ArgSplits.singleton (id,loc) (Partial (pats,l)),
diff --git a/src/process_file.ml b/src/process_file.ml
index eeb7c0d7..72e25777 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -71,7 +71,6 @@ let get_lexbuf f =
lexbuf, in_chan
let parse_file ?loc:(l=Parse_ast.Unknown) (f : string) : Parse_ast.defs =
- let open Reporting in
try
let lexbuf, in_chan = get_lexbuf f in
begin
@@ -82,12 +81,12 @@ let parse_file ?loc:(l=Parse_ast.Unknown) (f : string) : Parse_ast.defs =
| Parser.Error ->
let pos = Lexing.lexeme_start_p lexbuf in
let tok = Lexing.lexeme lexbuf in
- raise (Fatal_error (Err_syntax (pos, "current token: " ^ tok)))
- | Lexer.LexError(s,p) ->
- raise (Fatal_error (Err_lex (p, s)))
+ raise (Reporting.err_syntax pos ("current token: " ^ tok))
+ | Lexer.LexError (s, p) ->
+ raise (Reporting.err_lex p s)
end
with
- | Sys_error err -> raise (err_general l err)
+ | Sys_error err -> raise (Reporting.err_general l err)
(* Simple preprocessor features for conditional file loading *)
module StringSet = Set.Make(String)
diff --git a/src/reporting.ml b/src/reporting.ml
index e89ce396..d5e3003c 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -132,19 +132,19 @@ let print_err l m1 m2 =
type error =
| Err_general of Parse_ast.l * string
- | Err_unreachable of Parse_ast.l * (string * int * int * int) * string
+ | Err_unreachable of Parse_ast.l * (string * int * int * int) * Printexc.raw_backtrace * string
| Err_todo of Parse_ast.l * string
| Err_syntax of Lexing.position * string
| Err_syntax_loc of Parse_ast.l * string
| Err_lex of Lexing.position * string
| Err_type of Parse_ast.l * string
-let issues = "\n\nPlease report this as an issue on GitHub at https://github.com/rems-project/sail/issues"
+let issues = "\nPlease report this as an issue on GitHub at https://github.com/rems-project/sail/issues"
let dest_err = function
| Err_general (l, m) -> ("Error", Loc l, m)
- | Err_unreachable (l, (file, line, _, _), m) ->
- (Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line, Loc l, m ^ issues)
+ | Err_unreachable (l, (file, line, _, _), backtrace, m) ->
+ (Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line, Loc l, m ^ "\n\n" ^ Printexc.raw_backtrace_to_string backtrace ^ issues)
| Err_todo (l, m) -> ("Todo", Loc l, m)
| Err_syntax (p, m) -> ("Syntax error", Pos p, m)
| Err_syntax_loc (l, m) -> ("Syntax error", Loc l, m)
@@ -155,10 +155,14 @@ exception Fatal_error of error
(* Abbreviations for the very common cases *)
let err_todo l m = Fatal_error (Err_todo (l, m))
-let err_unreachable l ocaml_pos m = Fatal_error (Err_unreachable (l, ocaml_pos, m))
+let err_unreachable l ocaml_pos m =
+ let backtrace = Printexc.get_callstack 10 in
+ Fatal_error (Err_unreachable (l, ocaml_pos, backtrace, m))
let err_general l m = Fatal_error (Err_general (l, m))
-let err_typ l m = Fatal_error (Err_type (l,m))
+let err_typ l m = Fatal_error (Err_type (l, m))
+let err_syntax p m = Fatal_error (Err_syntax (p, m))
let err_syntax_loc l m = Fatal_error (Err_syntax_loc (l, m))
+let err_lex p m = Fatal_error (Err_lex (p, m))
let unreachable l pos msg =
raise (err_unreachable l pos msg)
diff --git a/src/reporting.mli b/src/reporting.mli
index 0bdff5ca..e0744c66 100644
--- a/src/reporting.mli
+++ b/src/reporting.mli
@@ -74,8 +74,7 @@ val simp_loc : Ast.l -> (Lexing.position * Lexing.position) option
val short_loc_to_string : Parse_ast.l -> string
(** [print_err fatal print_loc_source l head mes] prints an error / warning message to
- std-err. It starts with printing location information stored in [l]
- It then prints "head: mes". If [fatal] is set, the program exists with error-code 1 afterwards.
+ std-err.
*)
val print_err : Parse_ast.l -> string -> string -> unit
@@ -83,13 +82,13 @@ val print_err : Parse_ast.l -> string -> string -> unit
(** Errors stop execution and print a message; they typically have a location and message.
*)
-type error =
+type error = private
(** General errors, used for multi purpose. If you are unsure, use this one. *)
| Err_general of Parse_ast.l * string
(** Unreachable errors should never be thrown. It means that some
code was excuted that the programmer thought of as unreachable *)
- | Err_unreachable of Parse_ast.l * (string * int * int * int) * string
+ | Err_unreachable of Parse_ast.l * (string * int * int * int) * Printexc.raw_backtrace * string
(** [Err_todo] indicates that some feature is unimplemented; it should be built using [err_todo]. *)
| Err_todo of Parse_ast.l * string
@@ -101,20 +100,13 @@ type error =
exception Fatal_error of error
-(** [err_todo l m] is an abreviatiation for [Fatal_error (Err_todo (l, m))] *)
val err_todo : Parse_ast.l -> string -> exn
-
-(** [err_general l m] is an abreviatiation for [Fatal_error (Err_general (b, l, m))] *)
val err_general : Parse_ast.l -> string -> exn
-
-(** [err_unreachable l __POS__ m] is an abreviatiation for [Fatal_error (Err_unreachable (l, __POS__, m))] *)
val err_unreachable : Parse_ast.l -> (string * int * int * int) -> string -> exn
-
-(** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
val err_typ : Parse_ast.l -> string -> exn
-
-(** [err_syntax_loc] is an abbreviation for [Fatal_error (Err_syntax_loc (l, m))] *)
+val err_syntax : Lexing.position -> string -> exn
val err_syntax_loc : Parse_ast.l -> string -> exn
+val err_lex : Lexing.position -> string -> exn
val unreachable : Parse_ast.l -> (string * int * int * int) -> string -> 'a
diff --git a/src/slice.ml b/src/slice.ml
index 83010733..a38a207c 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -169,13 +169,23 @@ let add_def_to_graph graph def =
let scan_lexp self lexp_aux annot =
let env = env_of_annot annot in
begin match lexp_aux with
- | LEXP_cast (typ, _) ->
- IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ)
+ | LEXP_cast (typ, id) ->
+ IdSet.iter (fun id -> graph := G.add_edge self (Type id) !graph) (typ_ids typ);
+ begin match Env.lookup_id id env with
+ | Register _ ->
+ graph := G.add_edge self (Register id) !graph
+ | Enum _ -> graph := G.add_edge self (Constructor id) !graph
+ | _ ->
+ if IdSet.mem id (Env.get_toplevel_lets env) then
+ graph := G.add_edge self (Letbind id) !graph
+ else ()
+ end
| LEXP_memory (id, _) ->
graph := G.add_edge self (Function id) !graph
| LEXP_id id ->
begin match Env.lookup_id id env with
- | Register _ -> graph := G.add_edge self (Register id) !graph
+ | Register _ ->
+ graph := G.add_edge self (Register id) !graph
| Enum _ -> graph := G.add_edge self (Constructor id) !graph
| _ ->
if IdSet.mem id (Env.get_toplevel_lets env) then
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 18:42:19 +0000