summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/Errors.ml5
-rw-r--r--compiler/Extract.ml8
-rw-r--r--compiler/ExtractBase.ml82
-rw-r--r--compiler/ExtractTypes.ml8
-rw-r--r--compiler/Interpreter.ml3
-rw-r--r--compiler/Main.ml11
-rw-r--r--compiler/PrintPure.ml2
-rw-r--r--compiler/Pure.ml8
-rw-r--r--compiler/PureMicroPasses.ml4
-rw-r--r--compiler/PureTypeCheck.ml1
-rw-r--r--compiler/PureUtils.ml3
-rw-r--r--compiler/SymbolicAst.ml1
-rw-r--r--compiler/SymbolicToPure.ml4
13 files changed, 101 insertions, 39 deletions
diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 53e56c44..30887593 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -1,6 +1,7 @@
let log = Logging.errors_log
-let meta_to_string (span : Meta.span) =
+let meta_to_string (meta : Meta.meta) =
+ let span = meta.span in
let file = match span.file with Virtual s | Local s -> s in
let loc_to_string (l : Meta.loc) : string =
string_of_int l.line ^ ":" ^ string_of_int l.col
@@ -10,7 +11,7 @@ let meta_to_string (span : Meta.span) =
let format_error_message (meta : Meta.meta option) (msg : string) =
let meta =
- match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta.span
+ match meta with None -> "" | Some meta -> "\n" ^ meta_to_string meta
in
msg ^ meta
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1f9c9117..af0bf98d 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -297,6 +297,13 @@ let lets_require_wrap_in_do (meta : Meta.meta)
- application argument: [f (exp)]
- match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
*)
+
+let extract_texpression_errors (fmt : F.formatter) =
+ match !Config.backend with
+ | FStar | Coq -> F.pp_print_string fmt "admit"
+ | Lean -> F.pp_print_string fmt "sorry"
+ | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+
let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
(fmt : F.formatter) (inside : bool) (e : texpression) : unit =
match e.e with
@@ -323,6 +330,7 @@ let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
| Loop _ ->
(* The loop nodes should have been eliminated in {!PureMicroPasses} *)
craise __FILE__ __LINE__ meta "Unreachable"
+ | EError (_, _) -> extract_texpression_errors fmt
(* Extract an application *or* a top-level qualif (function extraction has
* to handle top-level qualifiers, so it seemed more natural to merge the
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 0a7c8df2..47b613c2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -237,7 +237,7 @@ module IdSet = Collections.MakeSet (IdOrderedType)
*)
type names_map = {
id_to_name : string IdMap.t;
- name_to_id : id StringMap.t;
+ name_to_id : (id * Meta.meta option) StringMap.t;
(** The name to id map is used to look for name clashes, and generate nice
debugging messages: if there is a name clash, it is useful to know
precisely which identifiers are mapped to the same name...
@@ -253,42 +253,53 @@ let empty_names_map : names_map =
}
(** Small helper to report name collision *)
-let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
+let report_name_collision (id_to_string : id -> string)
+ ((id1, meta1) : id * Meta.meta option) (id2 : id) (meta2 : Meta.meta option)
(name : string) : unit =
- let id1 = "\n- " ^ id_to_string id1 in
- let id2 = "\n- " ^ id_to_string id2 in
+ let meta_to_string (meta : Meta.meta option) =
+ match meta with
+ | None -> ""
+ | Some meta -> "\n " ^ Errors.meta_to_string meta
+ in
+ let id1 = "\n- " ^ id_to_string id1 ^ meta_to_string meta1 in
+ let id2 = "\n- " ^ id_to_string id2 ^ meta_to_string meta2 in
let err =
"Name clash detected: the following identifiers are bound to the same name \
\"" ^ name ^ "\":" ^ id1 ^ id2
^ "\nYou may want to rename some of your definitions, or report an issue."
in
- (* If we fail hard on errors, raise an exception *)
+ (* Register the error.
+
+ We don't link this error to any meta information because we already put
+ the span information about the two problematic definitions in the error
+ message above. *)
save_error __FILE__ __LINE__ None err
-let names_map_get_id_from_name (name : string) (nm : names_map) : id option =
+let names_map_get_id_from_name (name : string) (nm : names_map) :
+ (id * Meta.meta option) option =
StringMap.find_opt name nm.name_to_id
let names_map_check_collision (id_to_string : id -> string) (id : id)
- (name : string) (nm : names_map) : unit =
+ (meta : Meta.meta option) (name : string) (nm : names_map) : unit =
match names_map_get_id_from_name name nm with
| None -> () (* Ok *)
| Some clash ->
(* There is a clash: print a nice debugging message for the user *)
- report_name_collision id_to_string clash id name
+ report_name_collision id_to_string clash id meta name
(** Insert bindings in a names map without checking for collisions *)
-let names_map_add_unchecked (id : id) (name : string) (nm : names_map) :
- names_map =
+let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
+ (nm : names_map) : names_map =
(* Insert *)
let id_to_name = IdMap.add id name nm.id_to_name in
- let name_to_id = StringMap.add name id nm.name_to_id in
+ let name_to_id = StringMap.add name (id, meta) nm.name_to_id in
let names_set = StringSet.add name nm.names_set in
{ id_to_name; name_to_id; names_set }
-let names_map_add (id_to_string : id -> string) (id : id) (name : string)
- (nm : names_map) : names_map =
+let names_map_add (id_to_string : id -> string) ((id, meta) : id * meta option)
+ (name : string) (nm : names_map) : names_map =
(* Check if there is a clash *)
- names_map_check_collision id_to_string id name nm;
+ names_map_check_collision id_to_string id meta name nm;
(* Sanity check *)
(if StringSet.mem name nm.names_set then
let err =
@@ -296,9 +307,9 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
^ ":\nThe chosen name is already in the names set: " ^ name
in
(* If we fail hard on errors, raise an exception *)
- save_error __FILE__ __LINE__ None err);
+ save_error __FILE__ __LINE__ meta err);
(* Insert *)
- names_map_add_unchecked id name nm
+ names_map_add_unchecked (id, meta) name nm
(** The unsafe names map stores mappings from identifiers to names which might
collide. For some backends and some names, it might be acceptable to have
@@ -384,8 +395,8 @@ let allow_collisions (id : id) : bool =
(** The [id_to_string] function to print nice debugging messages if there are
collisions *)
-let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
- (nm : names_maps) : names_maps =
+let names_maps_add (id_to_string : id -> string) (id : id)
+ (meta : Meta.meta option) (name : string) (nm : names_maps) : names_maps =
(* We do not use the same name map if we allow/disallow collisions.
We notably use it for field names: some backends like Lean can use the
type information to disambiguate field projections.
@@ -400,7 +411,7 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
*)
if allow_collisions id then (
(* Check with the ids which are considered to be strict on collisions *)
- names_map_check_collision id_to_string id name nm.strict_names_map;
+ names_map_check_collision id_to_string id meta name nm.strict_names_map;
{
nm with
unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map;
@@ -415,10 +426,10 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
*)
let strict_names_map =
if strict_collisions id then
- names_map_add id_to_string id name nm.strict_names_map
+ names_map_add id_to_string (id, meta) name nm.strict_names_map
else nm.strict_names_map
in
- let names_map = names_map_add id_to_string id name nm.names_map in
+ let names_map = names_map_add id_to_string (id, meta) name nm.names_map in
{ nm with strict_names_map; names_map }
(** The [id_to_string] function to print nice debugging messages if there are
@@ -468,20 +479,21 @@ type names_map_init = {
let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
(name : string) (nm : names_maps) : names_maps =
- names_maps_add id_to_string (TypeId (TAssumed id)) name nm
+ names_maps_add id_to_string (TypeId (TAssumed id)) None name nm
let names_maps_add_assumed_struct (id_to_string : id -> string)
(id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
- names_maps_add id_to_string (StructId (TAssumed id)) name nm
+ names_maps_add id_to_string (StructId (TAssumed id)) None name nm
let names_maps_add_assumed_variant (id_to_string : id -> string)
(id : assumed_ty) (variant_id : VariantId.id) (name : string)
(nm : names_maps) : names_maps =
- names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) name nm
+ names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) None name nm
-let names_maps_add_function (id_to_string : id -> string) (fid : fun_id)
- (name : string) (nm : names_maps) : names_maps =
- names_maps_add id_to_string (FunId fid) name nm
+let names_maps_add_function (id_to_string : id -> string)
+ ((fid, meta) : fun_id * meta option) (name : string) (nm : names_maps) :
+ names_maps =
+ names_maps_add id_to_string (FunId fid) meta name nm
let bool_name () = if !backend = Lean then "Bool" else "bool"
let char_name () = if !backend = Lean then "Char" else "char"
@@ -659,7 +671,9 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
: extraction_ctx =
let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
- let names_maps = names_maps_add id_to_string id name ctx.names_maps in
+ let names_maps =
+ names_maps_add id_to_string id (Some meta) name ctx.names_maps
+ in
{ ctx with names_maps }
let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string
@@ -1125,7 +1139,7 @@ let initialize_names_maps () : names_maps =
(* There is duplication in the keywords so we don't check the collisions
while registering them (what is important is that there are no collisions
between keywords and user-defined identifiers) *)
- names_map_add_unchecked UnknownId name nm)
+ names_map_add_unchecked (UnknownId, None) name nm)
strict_names_map keywords
in
let nm = { names_map; unsafe_names_map; strict_names_map } in
@@ -1155,9 +1169,12 @@ let initialize_names_maps () : names_maps =
in
let assumed_functions =
List.map
- (fun (fid, name) -> (FromLlbc (Pure.FunId (FAssumed fid), None), name))
+ (fun (fid, name) ->
+ ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
init.assumed_llbc_functions
- @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
+ @ List.map
+ (fun (fid, name) -> ((Pure fid, None), name))
+ init.assumed_pure_functions
in
let nm =
List.fold_left
@@ -1702,7 +1719,8 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
| TLiteral lty -> (
match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i")
| TArrow _ -> "f"
- | TTraitType (_, name) -> name_from_type_ident name)
+ | TTraitType (_, name) -> name_from_type_ident name
+ | Error -> "x")
(** Generates a type variable basename. *)
let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) :
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 1f0abf8a..1c3657a3 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -433,6 +433,13 @@ let extract_literal_type (_ctx : extraction_ctx) (fmt : F.formatter)
End
]}
*)
+
+let extract_ty_errors (fmt : F.formatter) : unit =
+ match !Config.backend with
+ | FStar | Coq -> F.pp_print_string fmt "admit"
+ | Lean -> F.pp_print_string fmt "sorry"
+ | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)"
+
let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (inside : bool) (ty : ty) : unit =
let extract_rec = extract_ty meta ctx fmt no_params_tys in
@@ -566,6 +573,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
"Trait types are not supported yet when generating code for HOL4";
extract_trait_ref meta ctx fmt no_params_tys false trait_ref;
F.pp_print_string fmt ("." ^ add_brackets type_name))
+ | Error -> extract_ty_errors fmt
and extract_trait_ref (meta : Meta.meta) (ctx : extraction_ctx)
(fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index a65e1663..d0a54750 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -612,7 +612,8 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
(* Evaluate the function *)
let symbolic =
- eval_function_body config (Option.get fdef.body).body cf_finish ctx
+ try eval_function_body config (Option.get fdef.body).body cf_finish ctx
+ with CFailure (meta, msg) -> Some (Error (meta, msg))
in
(* Return *)
diff --git a/compiler/Main.ml b/compiler/Main.ml
index db200f37..416f3a07 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -274,12 +274,17 @@ let () =
(* Translate the functions *)
Aeneas.Translate.translate_crate filename dest_dir m
- with Errors.CFailure (meta, msg) ->
+ with Errors.CFailure (_, _) ->
(* In theory it shouldn't happen, but there may be uncaught errors -
note that we let the [Failure] exceptions go through (they are
send if we use the option [-abort-on-error] *)
- log#serror (Errors.format_error_message meta msg);
- exit 1);
+ ());
+
+ if !Errors.error_list <> [] then (
+ List.iter
+ (fun (meta, msg) -> log#serror (Errors.format_error_message meta msg))
+ !Errors.error_list;
+ exit 1);
(* Print total elapsed time *)
log#linfo
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index d0c243bb..97ea6048 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -164,6 +164,7 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string =
let trait_ref = trait_ref_to_string env false trait_ref in
let s = trait_ref ^ "::" ^ type_name in
if inside then "(" ^ s ^ ")" else s
+ | Error -> "@Error"
and generic_args_to_strings (env : fmt_env) (inside : bool)
(generics : generic_args) : string list =
@@ -615,6 +616,7 @@ let rec texpression_to_string ?(metadata : Meta.meta option = None)
let e = meta_s ^ "\n" ^ indent ^ e in
if inside then "(" ^ e ^ ")" else e
| MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
+ | EError (_, _) -> "@Error"
and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
(inside : bool) (indent : string) (indent_incr : string) (app : texpression)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 7de7e0f4..7366783c 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -285,6 +285,7 @@ type ty =
| TArrow of ty * ty
| TTraitType of trait_ref * string
(** The string is for the name of the associated type *)
+ | Error
and trait_ref = {
trait_id : trait_instance_id;
@@ -621,6 +622,7 @@ class ['self] iter_expression_base =
method visit_qualif : 'env -> qualif -> unit = fun _ _ -> ()
method visit_loop_id : 'env -> loop_id -> unit = fun _ _ -> ()
method visit_field_id : 'env -> field_id -> unit = fun _ _ -> ()
+ method visit_meta : 'env -> Meta.meta -> unit = fun _ _ -> ()
end
(** Ancestor for {!map_expression} visitor *)
@@ -632,6 +634,7 @@ class ['self] map_expression_base =
method visit_qualif : 'env -> qualif -> qualif = fun _ x -> x
method visit_loop_id : 'env -> loop_id -> loop_id = fun _ x -> x
method visit_field_id : 'env -> field_id -> field_id = fun _ x -> x
+ method visit_meta : 'env -> Meta.meta -> Meta.meta = fun _ x -> x
end
(** Ancestor for {!reduce_expression} visitor *)
@@ -643,6 +646,7 @@ class virtual ['self] reduce_expression_base =
method visit_qualif : 'env -> qualif -> 'a = fun _ _ -> self#zero
method visit_loop_id : 'env -> loop_id -> 'a = fun _ _ -> self#zero
method visit_field_id : 'env -> field_id -> 'a = fun _ _ -> self#zero
+ method visit_meta : 'env -> Meta.meta -> 'a = fun _ _ -> self#zero
end
(** Ancestor for {!mapreduce_expression} visitor *)
@@ -662,6 +666,9 @@ class virtual ['self] mapreduce_expression_base =
method visit_field_id : 'env -> field_id -> field_id * 'a =
fun _ x -> (x, self#zero)
+
+ method visit_meta : 'env -> Meta.meta -> Meta.meta * 'a =
+ fun _ x -> (x, self#zero)
end
(** **Rk.:** here, {!expression} is not at all equivalent to the expressions
@@ -726,6 +733,7 @@ type expression =
| Loop of loop (** See the comments for {!loop} *)
| StructUpdate of struct_update (** See the comments for {!struct_update} *)
| Meta of (emeta[@opaque]) * texpression (** Meta-information *)
+ | EError of Meta.meta option * string
and switch_body = If of texpression * texpression | Match of match_branch list
and match_branch = { pat : typed_pattern; branch : texpression }
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 9fa07029..ebc5c65f 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -416,6 +416,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
| StructUpdate supd -> update_struct_update supd ctx
| Lambda (lb, e) -> update_lambda lb e ctx
| Meta (meta, e) -> update_emeta meta e ctx
+ | EError (meta, msg) -> (ctx, EError (meta, msg))
in
(ctx, { e; ty })
(* *)
@@ -1006,7 +1007,8 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
match e with
| Var _ | CVar _ | Const _ | App _ | Qualif _
| Meta (_, _)
- | StructUpdate _ | Lambda _ ->
+ | StructUpdate _ | Lambda _
+ | EError (_, _) ->
super#visit_expression env e
| Switch (scrut, switch) -> (
match switch with
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 53ff8983..098e2564 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -238,3 +238,4 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) :
| Meta (_, e_next) ->
sanity_check __FILE__ __LINE__ (e_next.ty = e.ty) meta;
check_texpression meta ctx e_next
+ | EError (meta, msg) -> craise_opt_meta __FILE__ __LINE__ meta msg
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 6f44bb74..1bef43b4 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -233,6 +233,9 @@ let rec let_group_requires_parentheses (meta : Meta.meta) (e : texpression) :
| Loop _ ->
(* Should have been eliminated *)
craise __FILE__ __LINE__ meta "Unreachable"
+ | EError (meta, msg) ->
+ craise_opt_meta __FILE__ __LINE__ meta
+ msg (* TODO : check if true should'nt be returned instead ? *)
let texpression_requires_parentheses meta e =
match !Config.backend with
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index e164fd49..f15a2c23 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -212,6 +212,7 @@ type expression =
TODO: merge this with Return.
*)
| Meta of emeta * expression (** Meta information *)
+ | Error of Meta.meta option * string
and loop = {
loop_id : loop_id;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 5cd13072..f036cc37 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1981,6 +1981,9 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx)
(* Return the computed information *)
!info
+let translate_error (meta : Meta.meta option) (msg : string) : texpression =
+ { e = EError (meta, msg); ty = Error }
+
let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
match e with
| S.Return (ectx, opt_v) ->
@@ -2007,6 +2010,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
*)
translate_forward_end ectx loop_input_values e back_e ctx
| Loop loop -> translate_loop loop ctx
+ | Error (meta, msg) -> translate_error meta msg
and translate_panic (ctx : bs_ctx) : texpression =
(* Here we use the function return type - note that it is ok because
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 11:11:21 +0000