summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Config.ml2
-rw-r--r--compiler/Errors.ml5
-rw-r--r--compiler/Extract.ml24
-rw-r--r--compiler/ExtractBase.ml96
-rw-r--r--compiler/ExtractTypes.ml8
-rw-r--r--compiler/Interpreter.ml15
-rw-r--r--compiler/InterpreterBorrows.ml26
-rw-r--r--compiler/InterpreterBorrowsCore.ml4
-rw-r--r--compiler/InterpreterExpressions.ml19
-rw-r--r--compiler/InterpreterPaths.ml21
-rw-r--r--compiler/InterpreterProjectors.ml4
-rw-r--r--compiler/InterpreterStatements.ml13
-rw-r--r--compiler/Invariants.ml9
-rw-r--r--compiler/Main.ml16
-rw-r--r--compiler/PrePasses.ml19
-rw-r--r--compiler/Print.ml1
-rw-r--r--compiler/PrintPure.ml6
-rw-r--r--compiler/Pure.ml10
-rw-r--r--compiler/PureMicroPasses.ml25
-rw-r--r--compiler/PureTypeCheck.ml12
-rw-r--r--compiler/PureUtils.ml28
-rw-r--r--compiler/SymbolicAst.ml1
-rw-r--r--compiler/SymbolicToPure.ml295
-rw-r--r--compiler/Translate.ml95
-rw-r--r--compiler/TypesUtils.ml20
-rw-r--r--compiler/ValuesUtils.ml2
26 files changed, 517 insertions, 259 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 099cdc8b..0b26e2ef 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -368,4 +368,4 @@ let backend_has_tuple_projectors () =
let use_nested_tuple_projectors = ref false
(** Generate name patterns for the external definitions we encounter *)
-let extract_external_name_patterns = ref false
+let extract_external_name_patterns = ref true
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..6eeef772 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -219,7 +219,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
^ string_of_int (List.length types)
^ " type arguments"
in
- log#serror err;
+ save_error __FILE__ __LINE__ None err;
Result.Error (types, err))
else
let types = List.combine filter types in
@@ -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
@@ -1871,7 +1879,7 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx)
[{start,end}_gloabl_decl_group], contrary to {!extract_type_decl}
and {!extract_fun_decl}.
*)
-let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
(global : global_decl) (body : fun_decl) (interface : bool) : unit =
let meta = body.meta in
sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
@@ -1966,6 +1974,12 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break to insert lines between declarations *)
F.pp_print_break fmt 0 0
+let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
+ (global : global_decl option) (body : fun_decl) (interface : bool) : unit =
+ match global with
+ | Some global -> extract_global_decl_aux ctx fmt global body interface
+ | None -> ()
+
(** Similar to {!extract_trait_decl_register_names} *)
let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
(trait_decl : trait_decl)
@@ -2853,7 +2867,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "=";
F.pp_print_space fmt ();
let success =
- ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx
+ ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx
in
F.pp_print_string fmt (success ^ " ())")
| Coq ->
@@ -2884,11 +2898,11 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "==";
F.pp_print_space fmt ();
let success =
- ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx
+ ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx
in
F.pp_print_string fmt (success ^ " ())")
| HOL4 ->
- F.pp_print_string fmt "val _ = assert_return (";
+ F.pp_print_string fmt "val _ = assert_ok (";
F.pp_print_string fmt "“";
let fun_name =
ctx_get_local_function def.meta def.def_id def.loop_id ctx
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 74ac9e32..656d2f27 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
@@ -1006,7 +1020,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
match !backend with
| FStar ->
[
- (TResult, result_return_id, "Return");
+ (TResult, result_ok_id, "Ok");
(TResult, result_fail_id, "Fail");
(TError, error_failure_id, "Failure");
(TError, error_out_of_fuel_id, "OutOfFuel");
@@ -1015,7 +1029,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
]
| Coq ->
[
- (TResult, result_return_id, "Return");
+ (TResult, result_ok_id, "Ok");
(TResult, result_fail_id, "Fail_");
(TError, error_failure_id, "Failure");
(TError, error_out_of_fuel_id, "OutOfFuel");
@@ -1024,7 +1038,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
]
| Lean ->
[
- (TResult, result_return_id, "Result.ret");
+ (TResult, result_ok_id, "Result.ok");
(TResult, result_fail_id, "Result.fail");
(* For panic: we omit the prefix "Error." because the type is always
clear from the context. Also, "Error" is often used by user-defined
@@ -1035,7 +1049,7 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
]
| HOL4 ->
[
- (TResult, result_return_id, "Return");
+ (TResult, result_ok_id, "Ok");
(TResult, result_fail_id, "Fail");
(TError, error_failure_id, "Failure");
(* No Fuel::Zero on purpose *)
@@ -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
@@ -1662,9 +1679,11 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
in
(* If there is a basename, we use it *)
match basename with
- | Some basename ->
+ | Some basename -> (
(* This should be a no-op *)
- to_snake_case basename
+ match !Config.backend with
+ | Lean -> basename
+ | FStar | Coq | HOL4 -> to_snake_case basename)
| None -> (
(* No basename: we use the first letter of the type *)
match ty with
@@ -1700,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..769e3144 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -191,6 +191,18 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
* do it, and because it gives a bit of sanity.
* *)
let sg = fdef.signature in
+ (* Sanity check: no nested borrows, borrows in ADTs, etc. *)
+ cassert __FILE__ __LINE__
+ (List.for_all
+ (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty))
+ (sg.output :: sg.inputs))
+ fdef.meta "Nested borrows are not supported yet";
+ cassert __FILE__ __LINE__
+ (List.for_all
+ (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty))
+ (sg.output :: sg.inputs))
+ fdef.meta "ADTs containing borrows are not supported yet";
+
(* Create the context *)
let regions_hierarchy =
FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
@@ -612,7 +624,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/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index e593ae75..a158ed9a 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -303,13 +303,11 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id)
if bid' = bid then (
(* Sanity check *)
let expected_ty = ty in
- if nv.ty <> expected_ty then (
- log#serror
- ("give_back_value: improper type:\n- expected: "
- ^ ty_to_string ctx ty ^ "\n- received: "
- ^ ty_to_string ctx nv.ty);
+ if nv.ty <> expected_ty then
craise __FILE__ __LINE__ meta
- "Value given back doesn't have the proper type");
+ ("Value given back doesn't have the proper type:\n\
+ - expected: " ^ ty_to_string ctx ty ^ "\n- received: "
+ ^ ty_to_string ctx nv.ty);
(* Replace *)
set_replaced ();
nv.value)
@@ -540,13 +538,11 @@ let give_back_avalue_to_same_abstraction (_config : config) (meta : Meta.meta)
* see the comment at the level of the definition of
* {!typed_avalue} *)
let _, expected_ty, _ = ty_get_ref ty in
- if nv.ty <> expected_ty then (
- log#serror
- ("give_back_avalue_to_same_abstraction: improper type:\n\
+ if nv.ty <> expected_ty then
+ craise __FILE__ __LINE__ meta
+ ("Value given back doesn't have the proper type:\n\
- expected: " ^ ty_to_string ctx ty ^ "\n- received: "
^ ty_to_string ctx nv.ty);
- craise __FILE__ __LINE__ meta
- "Value given back doesn't have the proper type");
(* This is the loan we are looking for: apply the projection to
* the value we give back and replaced this mutable loan with
* an ended loan *)
@@ -836,26 +832,26 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string)
match lookup_borrow_opt ek_all l ctx with
| None -> () (* Ok *)
| Some _ ->
- log#lerror
+ log#ltrace
(lazy
(fun_name ^ ": " ^ BorrowId.to_string l
^ ": borrow didn't disappear:\n- original context:\n"
^ eval_ctx_to_string ~meta:(Some meta) ctx0
^ "\n\n- new context:\n"
^ eval_ctx_to_string ~meta:(Some meta) ctx));
- craise __FILE__ __LINE__ meta "Borrow not eliminated"
+ internal_error __FILE__ __LINE__ meta
in
match lookup_loan_opt meta ek_all l ctx with
| None -> () (* Ok *)
| Some _ ->
- log#lerror
+ log#ltrace
(lazy
(fun_name ^ ": " ^ BorrowId.to_string l
^ ": loan didn't disappear:\n- original context:\n"
^ eval_ctx_to_string ~meta:(Some meta) ctx0
^ "\n\n- new context:\n"
^ eval_ctx_to_string ~meta:(Some meta) ctx));
- craise __FILE__ __LINE__ meta "Loan not eliminated"
+ internal_error __FILE__ __LINE__ meta
in
unit_to_cm_fun check_disappeared
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 6e65b11d..a01be046 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -162,11 +162,11 @@ let rec compare_rtys (meta : Meta.meta) (default : bool)
sanity_check __FILE__ __LINE__ (ty1 = ty2) meta;
default
| _ ->
- log#lerror
+ log#ltrace
(lazy
("compare_rtys: unexpected inputs:" ^ "\n- ty1: " ^ show_ty ty1
^ "\n- ty2: " ^ show_ty ty2));
- craise __FILE__ __LINE__ meta "Unreachable"
+ internal_error __FILE__ __LINE__ meta
(** Check if two different projections intersect. This is necessary when
giving a symbolic value to an abstraction: we need to check that
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 48a1cce6..5f849230 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -146,7 +146,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
"Can't copy an assumed value other than Option"
| TAdt (TAdtId _, _) as ty ->
sanity_check __FILE__ __LINE__
- (allow_adt_copy || ty_is_primitively_copyable ty)
+ (allow_adt_copy || ty_is_copyable ty)
meta
| TAdt (TTuple, _) -> () (* Ok *)
| TAdt
@@ -157,9 +157,8 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
const_generics = [];
trait_refs = [];
} ) ->
- exec_assert __FILE__ __LINE__
- (ty_is_primitively_copyable ty)
- meta "The type is not primitively copyable"
+ exec_assert __FILE__ __LINE__ (ty_is_copyable ty) meta
+ "The type is not primitively copyable"
| _ -> exec_raise __FILE__ __LINE__ meta "Unreachable");
let ctx, fields =
List.fold_left_map
@@ -195,7 +194,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
* thus requires calling the proper function. Here, we copy values
* for very simple types such as integers, shared borrows, etc. *)
cassert __FILE__ __LINE__
- (ty_is_primitively_copyable (Substitute.erase_regions sp.sv_ty))
+ (ty_is_copyable (Substitute.erase_regions sp.sv_ty))
meta "Not primitively copyable";
(* If the type is copyable, we simply return the current value. Side
* remark: what is important to look at when copying symbolic values
@@ -528,9 +527,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta
"The arguments given to the binop don't have the same type";
(* Equality/inequality check is primitive only for a subset of types *)
- exec_assert __FILE__ __LINE__
- (ty_is_primitively_copyable v1.ty)
- meta "Type is not primitively copyable";
+ exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta
+ "Type is not primitively copyable";
let b = v1 = v2 in
Ok { value = VLiteral (VBool b); ty = TLiteral TBool })
else
@@ -621,9 +619,8 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
(* Equality operations *)
sanity_check __FILE__ __LINE__ (v1.ty = v2.ty) meta;
(* Equality/inequality check is primitive only for a subset of types *)
- exec_assert __FILE__ __LINE__
- (ty_is_primitively_copyable v1.ty)
- meta "The type is not primitively copyable";
+ exec_assert __FILE__ __LINE__ (ty_is_copyable v1.ty) meta
+ "The type is not primitively copyable";
TLiteral TBool)
else
(* Other operations: input types are integers *)
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index f2c0bcb1..ab3daa72 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -83,7 +83,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
let nv = update v in
(* Type checking *)
if nv.ty <> v.ty then (
- log#lerror
+ log#ltrace
(lazy
("Not the same type:\n- nv.ty: " ^ show_ety nv.ty ^ "\n- v.ty: "
^ show_ety v.ty));
@@ -252,8 +252,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access)
let pe = "- pe: " ^ show_projection_elem pe in
let v = "- v:\n" ^ show_value v in
let ty = "- ty:\n" ^ show_ety ty in
- log#serror ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty);
- craise __FILE__ __LINE__ meta "Inconsistent projection")
+ craise __FILE__ __LINE__ meta
+ ("Inconsistent projection:\n" ^ pe ^ "\n" ^ v ^ "\n" ^ ty))
(** Generic function to access (read/write) the value at a given place.
@@ -319,14 +319,13 @@ let try_read_place (meta : Meta.meta) (access : access_kind) (p : place)
(* Note that we ignore the new environment: it should be the same as the
original one.
*)
- if !Config.sanity_checks then
- if ctx1 <> ctx then (
- let msg =
- "Unexpected environment update:\nNew environment:\n"
- ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
- in
- log#serror msg;
- craise __FILE__ __LINE__ meta "Unexpected environment update");
+ (if !Config.sanity_checks then
+ if ctx1 <> ctx then
+ let msg =
+ "Unexpected environment update:\nNew environment:\n"
+ ^ show_env ctx1.env ^ "\n\nOld environment:\n" ^ show_env ctx.env
+ in
+ craise __FILE__ __LINE__ meta msg);
Ok read_value
let read_place (meta : Meta.meta) (access : access_kind) (p : place)
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 6e86e6a4..3993d845 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -217,12 +217,12 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool)
meta);
ASymbolic (AProjBorrows (s, ty))
| _ ->
- log#lerror
+ log#ltrace
(lazy
("apply_proj_borrows: unexpected inputs:\n- input value: "
^ typed_value_to_string ~meta:(Some meta) ctx v
^ "\n- proj rty: " ^ ty_to_string ctx ty));
- craise __FILE__ __LINE__ meta "Unreachable"
+ internal_error __FILE__ __LINE__ meta
in
{ value; ty }
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 1cf1c5ef..de89f316 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1365,10 +1365,21 @@ and eval_transparent_function_call_symbolic (config : config) (meta : Meta.meta)
let func, generics, trait_method_generics, def, regions_hierarchy, inst_sg =
eval_transparent_function_call_symbolic_inst meta call ctx
in
- (* Sanity check *)
+ (* Sanity check: same number of inputs *)
sanity_check __FILE__ __LINE__
(List.length call.args = List.length def.signature.inputs)
def.meta;
+ (* Sanity check: no nested borrows, borrows in ADTs, etc. *)
+ cassert __FILE__ __LINE__
+ (List.for_all
+ (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty))
+ (inst_sg.output :: inst_sg.inputs))
+ meta "Nested borrows are not supported yet";
+ cassert __FILE__ __LINE__
+ (List.for_all
+ (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty))
+ (inst_sg.output :: inst_sg.inputs))
+ meta "ADTs containing borrows are not supported yet";
(* Evaluate the function call *)
eval_function_call_symbolic_from_inst_sig config def.meta func def.signature
regions_hierarchy inst_sg generics trait_method_generics call.args call.dest
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 642d7a37..689db0c4 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -185,7 +185,6 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
"find_info: could not find the representant of borrow "
^ BorrowId.to_string bid ^ ":\nContext:\n" ^ context_to_string ()
in
- log#serror err;
craise __FILE__ __LINE__ meta err
in
@@ -706,13 +705,13 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
| AEndedProjBorrows _ | AIgnoredProjBorrows -> ())
| AIgnored, _ -> ()
| _ ->
- log#lerror
+ log#ltrace
(lazy
("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv
^ "\n- value: "
^ typed_avalue_to_string ~meta:(Some meta) ctx atv
^ "\n- type: " ^ ty_to_string ctx atv.ty));
- craise __FILE__ __LINE__ meta "Erroneous typing");
+ internal_error __FILE__ __LINE__ meta);
(* Continue exploring to inspect the subterms *)
super#visit_typed_avalue info atv
end
@@ -826,9 +825,9 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
* it must be expanded first *)
if ty_has_borrows ctx.type_ctx.type_infos info.ty then
sanity_check __FILE__ __LINE__ (info.env_count <= 1) meta;
- (* A duplicated symbolic value is necessarily primitively copyable *)
+ (* A duplicated symbolic value is necessarily copyable *)
sanity_check __FILE__ __LINE__
- (info.env_count <= 1 || ty_is_primitively_copyable info.ty)
+ (info.env_count <= 1 || ty_is_copyable info.ty)
meta;
sanity_check __FILE__ __LINE__
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 64d8ae2b..6161f2f2 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -120,9 +120,6 @@ let () =
Arg.Set use_nested_tuple_projectors,
" Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \
(0, 1).1)." );
- ( "-ext-name-pats",
- Arg.Set extract_external_name_patterns,
- " Generate name patterns for the external definitions we find." );
]
in
@@ -277,12 +274,19 @@ 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))
+ (* Reverse the list of error messages so that we print them from the
+ earliest to the latest. *)
+ (List.rev !Errors.error_list);
+ exit 1);
(* Print total elapsed time *)
log#linfo
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 0b39f64a..a46ef79c 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -238,9 +238,9 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl =
method! visit_Sequence env st1 st2 =
match st1.content with
| Loop _ ->
- sanity_check __FILE__ __LINE__
+ cassert __FILE__ __LINE__
(statement_has_no_loop_break_continue st2)
- st2.meta;
+ st2.meta "Sequences of loops are not supported yet";
(replace_breaks_with st1 st2).content
| _ -> super#visit_Sequence env st1 st2
end
@@ -437,9 +437,22 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl =
let apply_passes (crate : crate) : crate =
let passes = [ remove_loop_breaks crate; remove_shallow_borrows crate ] in
+ (* Attempt to apply a pass: if it fails we replace the body by [None] *)
+ let apply_pass (pass : fun_decl -> fun_decl) (f : fun_decl) =
+ try pass f
+ with CFailure (_, _) ->
+ (* The error was already registered, we don't need to register it twice.
+ However, we replace the body of the function, and save an error to
+ report to the user the fact that we will ignore the function body *)
+ let fmt = Print.Crate.crate_to_fmt_env crate in
+ let name = Print.name_to_string fmt f.name in
+ save_error __FILE__ __LINE__ (Some f.meta)
+ ("Ignoring the body of '" ^ name ^ "' because of previous error");
+ { f with body = None }
+ in
let fun_decls =
List.fold_left
- (fun fl pass -> FunDeclId.Map.map pass fl)
+ (fun fl pass -> FunDeclId.Map.map (apply_pass pass) fl)
crate.fun_decls passes
in
let crate = { crate with fun_decls } in
diff --git a/compiler/Print.ml b/compiler/Print.ml
index dad1aea3..51286553 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -1,4 +1,5 @@
include Charon.PrintUtils
+include Charon.PrintTypes
include Charon.PrintLlbcAst
open Charon.PrintTypes
open Charon.PrintExpressions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index d0c243bb..db9c583d 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 =
@@ -311,7 +312,7 @@ let adt_variant_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id)
craise_opt_meta __FILE__ __LINE__ meta "Unreachable"
| TResult ->
let variant_id = Option.get variant_id in
- if variant_id = result_return_id then "@Result::Return"
+ if variant_id = result_ok_id then "@Result::Return"
else if variant_id = result_fail_id then "@Result::Fail"
else
craise_opt_meta __FILE__ __LINE__ meta
@@ -394,7 +395,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
craise_opt_meta __FILE__ __LINE__ meta "Unreachable"
| TResult ->
let variant_id = Option.get variant_id in
- if variant_id = result_return_id then
+ if variant_id = result_ok_id then
match field_values with
| [ v ] -> "@Result::Return " ^ v
| _ ->
@@ -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..451767f8 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -92,7 +92,7 @@ type assumed_ty =
(* TODO: we should never directly manipulate [Return] and [Fail], but rather
* the monadic functions [return] and [fail] (makes treatment of error and
* state-error monads more uniform) *)
-let result_return_id = VariantId.of_int 0
+let result_ok_id = VariantId.of_int 0
let result_fail_id = VariantId.of_int 1
let option_some_id = T.option_some_id
let option_none_id = T.option_none_id
@@ -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..004ecfef 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 })
(* *)
@@ -751,7 +752,7 @@ let simplify_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
},
x ) ->
(* return/fail case *)
- if variant_id = result_return_id then
+ if variant_id = result_ok_id then
(* Return case - note that the simplification we just perform
might have unlocked the tuple simplification below *)
self#visit_Let env false lv x next
@@ -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
@@ -1082,19 +1084,19 @@ let filter_useless (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
let body = { body with body = body_exp; inputs_lvs } in
{ def with body = Some body }
-(** Simplify the lets immediately followed by a return.
+(** Simplify the lets immediately followed by an ok.
Ex.:
{[
x <-- f y;
- Return x
+ Ok x
~~>
f y
]}
*)
-let simplify_let_then_return _ctx (def : fun_decl) =
+let simplify_let_then_ok _ctx (def : fun_decl) =
(* Match a pattern and an expression: evaluates to [true] if the expression
is actually exactly the pattern *)
let rec match_pattern_and_expr (pat : typed_pattern) (e : texpression) : bool
@@ -1150,7 +1152,7 @@ let simplify_let_then_return _ctx (def : fun_decl) =
| Some e ->
if match_pattern_and_expr lv e then
(* We need to wrap the right-value in a ret *)
- (mk_result_return_texpression def.meta rv).e
+ (mk_result_ok_texpression def.meta rv).e
else not_simpl_e
| None ->
if match_pattern_and_expr lv next_e then rv.e else not_simpl_e
@@ -1789,7 +1791,7 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
let err_v = mk_texpression_from_var err_var in
let fail_value = mk_result_fail_texpression def.meta err_v e.ty in
let fail_branch = { pat = fail_pat; branch = fail_value } in
- let success_pat = mk_result_return_pattern lv in
+ let success_pat = mk_result_ok_pattern lv in
let success_branch = { pat = success_pat; branch = e } in
let switch_body = Match [ fail_branch; success_branch ] in
let e = Switch (re, switch_body) in
@@ -1852,9 +1854,9 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
f y
]}
*)
- let def = simplify_let_then_return ctx def in
+ let def = simplify_let_then_ok ctx def in
log#ldebug
- (lazy ("simplify_let_then_return:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
+ (lazy ("simplify_let_then_ok:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
(* Simplify the aggregated ADTs.
@@ -1890,11 +1892,10 @@ let apply_end_passes_to_def (ctx : trans_ctx) (def : fun_decl) : fun_decl =
(* Simplify the let-then return again (the lambda simplification may have
unlocked more simplifications here) *)
- let def = simplify_let_then_return ctx def in
+ let def = simplify_let_then_ok ctx def in
log#ldebug
(lazy
- ("simplify_let_then_return (pass 2):\n\n" ^ fun_decl_to_string ctx def
- ^ "\n"));
+ ("simplify_let_then_ok (pass 2):\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
(* Decompose the monadic let-bindings - used by Coq *)
let def =
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 53ff8983..c1da4019 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -32,7 +32,7 @@ let get_adt_field_types (meta : Meta.meta)
| TResult ->
let ty = Collections.List.to_cons_nil generics.types in
let variant_id = Option.get variant_id in
- if variant_id = result_return_id then [ ty ]
+ if variant_id = result_ok_id then [ ty ]
else if variant_id = result_fail_id then [ mk_error_ty ]
else
craise __FILE__ __LINE__ meta
@@ -93,12 +93,11 @@ let rec check_typed_pattern (meta : Meta.meta) (ctx : tc_ctx)
get_adt_field_types meta ctx.type_decls type_id av.variant_id generics
in
let check_value (ctx : tc_ctx) (ty : ty) (v : typed_pattern) : tc_ctx =
- if ty <> v.ty then (
+ if ty <> v.ty then
(* TODO: we need to normalize the types *)
- log#serror
- ("check_typed_pattern: not the same types:" ^ "\n- ty: "
- ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty);
- craise __FILE__ __LINE__ meta "Inconsistent types");
+ craise __FILE__ __LINE__ meta
+ ("Inconsistent types:" ^ "\n- ty: " ^ show_ty ty ^ "\n- v.ty: "
+ ^ show_ty v.ty);
check_typed_pattern meta ctx v
in
(* Check the field types: check that the field patterns have the expected
@@ -238,3 +237,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 4bc90872..fdd14eba 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -75,10 +75,15 @@ let inputs_info_is_wf (info : inputs_info) : bool =
let fun_sig_info_is_wf (info : fun_sig_info) : bool =
inputs_info_is_wf info.fwd_info
+let opt_dest_arrow_ty (ty : ty) : (ty * ty) option =
+ match ty with TArrow (arg_ty, ret_ty) -> Some (arg_ty, ret_ty) | _ -> None
+
+let is_arrow_ty (ty : ty) : bool = Option.is_some (opt_dest_arrow_ty ty)
+
let dest_arrow_ty (meta : Meta.meta) (ty : ty) : ty * ty =
- match ty with
- | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
- | _ -> craise __FILE__ __LINE__ meta "Not an arrow type"
+ match opt_dest_arrow_ty ty with
+ | Some (arg_ty, ret_ty) -> (arg_ty, ret_ty)
+ | None -> craise __FILE__ __LINE__ meta "Not an arrow type"
let compute_literal_type (cv : literal) : literal_type =
match cv with
@@ -228,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
@@ -578,12 +586,12 @@ let mk_result_fail_texpression_with_error_id (meta : Meta.meta)
let error = mk_error error in
mk_result_fail_texpression meta error ty
-let mk_result_return_texpression (meta : Meta.meta) (v : texpression) :
- texpression =
+let mk_result_ok_texpression (meta : Meta.meta) (v : texpression) : texpression
+ =
let type_args = [ v.ty ] in
let ty = TAdt (TAssumed TResult, mk_generic_args_from_types type_args) in
let id =
- AdtCons { adt_id = TAssumed TResult; variant_id = Some result_return_id }
+ AdtCons { adt_id = TAssumed TResult; variant_id = Some result_ok_id }
in
let qualif = { id; generics = mk_generic_args_from_types type_args } in
let cons_e = Qualif qualif in
@@ -605,11 +613,9 @@ let mk_result_fail_pattern_ignore_error (ty : ty) : typed_pattern =
let error_pat : pattern = PatDummy in
mk_result_fail_pattern error_pat ty
-let mk_result_return_pattern (v : typed_pattern) : typed_pattern =
+let mk_result_ok_pattern (v : typed_pattern) : typed_pattern =
let ty = TAdt (TAssumed TResult, mk_generic_args_from_types [ v.ty ]) in
- let value =
- PatAdt { variant_id = Some result_return_id; field_values = [ v ] }
- in
+ let value = PatAdt { variant_id = Some result_ok_id; field_values = [ v ] } in
{ value; ty }
let opt_unmeta_mplace (e : texpression) : mplace option * texpression =
@@ -783,6 +789,6 @@ let opt_destruct_ret (e : texpression) : texpression option =
ty = _;
},
arg )
- when variant_id = Some result_return_id ->
+ when variant_id = Some result_ok_id ->
Some arg
| _ -> None
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 0c30f44c..15b52237 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -268,6 +268,22 @@ type bs_ctx = {
Note that when a function contains a loop, we group the function symbolic AST and the loop symbolic
AST in a single function.
*)
+ mk_return : (bs_ctx -> texpression option -> texpression) option;
+ (** Small helper: translate a [return] expression, given a value to "return".
+ The translation of [return] depends on the context, and in particular depends on
+ whether we are inside a subexpression like a loop or not.
+
+ Note that the function consumes an optional expression, which is:
+ - [Some] for a forward computation
+ - [None] for a backward computation
+
+ We initialize this at [None].
+ *)
+ mk_panic : texpression option;
+ (** Small helper: translate a [fail] expression.
+
+ We initialize this at [None].
+ *)
}
[@@deriving show]
@@ -1499,9 +1515,27 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
let back_vars =
List.map
(fun (name, ty) ->
- match ty with None -> None | Some ty -> Some (name, ty))
+ match ty with
+ | None -> None
+ | Some ty ->
+ (* If the type is not an arrow type, don't use the name "back"
+ (it is a backward function with no inputs, that is to say a
+ value) *)
+ let name = if is_arrow_ty ty then name else None in
+ Some (name, ty))
back_vars
in
+ (* If there is one backward function or less, we use the name "back"
+ (there is no point in using the lifetime name, and it makes the
+ code generation more stable) *)
+ let num_back_vars = List.length (List.filter_map (fun x -> x) back_vars) in
+ let back_vars =
+ if num_back_vars = 1 then
+ List.map
+ (Option.map (fun (name, ty) -> (Option.map (fun _ -> "back") name, ty)))
+ back_vars
+ else back_vars
+ in
fresh_opt_vars back_vars ctx
(** IMPORTANT: do not use this one directly, but rather {!symbolic_value_to_texpression} *)
@@ -1963,6 +1997,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) ->
@@ -1989,55 +2026,9 @@ 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
- * we don't match on panics which happen inside the function body -
- * but it won't be true anymore once we translate individual blocks *)
- (* If we use a state monad, we need to add a lambda for the state variable *)
- (* Note that only forward functions return a state *)
- let effect_info = ctx_get_effect_info ctx in
- (* TODO: we should use a [Fail] function *)
- let mk_output output_ty =
- if effect_info.stateful then
- (* Create the [Fail] value *)
- let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
- let ret_v =
- mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
- ret_ty
- in
- ret_v
- else
- mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
- output_ty
- in
- if ctx.inside_loop && Option.is_some ctx.bid then
- (* We are synthesizing the backward function of a loop body *)
- let bid = Option.get ctx.bid in
- let loop_id = Option.get ctx.loop_id in
- let loop = LoopId.Map.find loop_id ctx.loops in
- let tys = RegionGroupId.Map.find bid loop.back_outputs in
- let output = mk_simpl_tuple_ty tys in
- mk_output output
- else
- (* Regular function, or forward function (the forward translation for
- a loop has the same return type as the parent function)
- *)
- match ctx.bid with
- | None ->
- let back_tys = compute_back_tys ctx.sg None in
- let back_tys = List.filter_map (fun x -> x) back_tys in
- let tys =
- if ctx.sg.fwd_info.ignore_output then back_tys
- else ctx.sg.fwd_output :: back_tys
- in
- let output = mk_simpl_tuple_ty tys in
- mk_output output
- | Some bid ->
- let output =
- mk_simpl_tuple_ty (RegionGroupId.Map.find bid ctx.sg.back_sg).outputs
- in
- mk_output output
+and translate_panic (ctx : bs_ctx) : texpression = Option.get ctx.mk_panic
(** [opt_v]: the value to return, in case we translate a forward body.
@@ -2049,42 +2040,8 @@ and translate_panic (ctx : bs_ctx) : texpression =
*)
and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
(ctx : bs_ctx) : texpression =
- (* There are two cases:
- - either we reach the return of a forward function or a forward loop body,
- in which case the optional value should be [Some] (it is the returned value)
- - or we are translating a backward function, in which case it should be [None]
- *)
- (* Compute the values that we should return *without the state and the result
- wrapper* *)
- let output =
- match ctx.bid with
- | None ->
- (* Forward function *)
- let v = Option.get opt_v in
- typed_value_to_texpression ctx ectx v
- | Some _ ->
- (* Backward function *)
- (* Sanity check *)
- sanity_check __FILE__ __LINE__ (opt_v = None) ctx.meta;
- (* Group the variables in which we stored the values we need to give back.
- See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
- let backward_outputs = Option.get ctx.backward_outputs in
- let field_values = List.map mk_texpression_from_var backward_outputs in
- mk_simpl_tuple_texpression ctx.meta field_values
- in
- (* We may need to return a state
- * - error-monad: Return x
- * - state-error: Return (state, x)
- * *)
- let effect_info = ctx_get_effect_info ctx in
- let output =
- if effect_info.stateful then
- let state_rvalue = mk_state_texpression ctx.state_var in
- mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
- else output
- in
- (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
- mk_result_return_texpression ctx.meta output
+ let opt_v = Option.map (typed_value_to_texpression ctx ectx) opt_v in
+ (Option.get ctx.mk_return) ctx opt_v
and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
(ctx : bs_ctx) : texpression =
@@ -2132,8 +2089,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
else output
in
(* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
- mk_emeta (Tag "return_with_loop")
- (mk_result_return_texpression ctx.meta output)
+ mk_emeta (Tag "return_with_loop") (mk_result_ok_texpression ctx.meta output)
and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
texpression =
@@ -2240,15 +2196,14 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
(fun ty ->
match ty with
| None -> None
- | Some (back_sg, ty) ->
- (* We insert a name for the variable only if the function
- can fail: if it can fail, it means the call returns a backward
- function. Otherwise, it directly returns the value given
- back by the backward function, which means we shouldn't
- give it a name like "back..." (it doesn't make sense) *)
+ | Some (_back_sg, ty) ->
+ (* We insert a name for the variable only if the type
+ is an arrow type. If it is not, it means the backward
+ function is degenerate (it takes no inputs) so it is
+ not a function anymore but a value: it doesn't make
+ sense to use a name like "back...". *)
let name =
- if back_sg.effect_info.can_fail then Some back_fun_name
- else None
+ if is_arrow_ty ty then Some back_fun_name else None
in
Some (name, ty))
back_tys)
@@ -3102,6 +3057,49 @@ and translate_forward_end (ectx : C.eval_ctx)
(ctx, backward_inputs_no_state @ [ var ])
else (ctx, backward_inputs_no_state)
in
+ (* Update the functions mk_return and mk_panic *)
+ let effect_info = back_sg.effect_info in
+ let mk_return ctx v =
+ assert (v = None);
+ let output =
+ (* Group the variables in which we stored the values we need to give back.
+ See the explanations for the [SynthInput] case in [translate_end_abstraction] *)
+ let backward_outputs = Option.get ctx.backward_outputs in
+ let field_values =
+ List.map mk_texpression_from_var backward_outputs
+ in
+ mk_simpl_tuple_texpression ctx.meta field_values
+ in
+ let output =
+ if effect_info.stateful then
+ let state_rvalue = mk_state_texpression ctx.state_var in
+ mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
+ else output
+ in
+ (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
+ mk_result_ok_texpression ctx.meta output
+ in
+ let mk_panic =
+ (* TODO: we should use a [Fail] function *)
+ let mk_output output_ty =
+ if effect_info.stateful then
+ (* Create the [Fail] value *)
+ let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
+ let ret_v =
+ mk_result_fail_texpression_with_error_id ctx.meta
+ error_failure_id ret_ty
+ in
+ ret_v
+ else
+ mk_result_fail_texpression_with_error_id ctx.meta
+ error_failure_id output_ty
+ in
+ let output =
+ mk_simpl_tuple_ty
+ (RegionGroupId.Map.find bid ctx.sg.back_sg).outputs
+ in
+ mk_output output
+ in
{
ctx with
backward_inputs_no_state =
@@ -3110,6 +3108,8 @@ and translate_forward_end (ectx : C.eval_ctx)
backward_inputs_with_state =
RegionGroupId.Map.add bid backward_inputs_with_state
ctx.backward_inputs_with_state;
+ mk_return = Some mk_return;
+ mk_panic = Some mk_panic;
}
in
@@ -3209,7 +3209,7 @@ and translate_forward_end (ectx : C.eval_ctx)
let state_var = List.map mk_texpression_from_var state_var in
let ret = mk_simpl_tuple_texpression ctx.meta (state_var @ [ ret ]) in
- let ret = mk_result_return_texpression ctx.meta ret in
+ let ret = mk_result_ok_texpression ctx.meta ret in
(* Introduce all the let-bindings *)
@@ -3454,7 +3454,6 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
in
(* Compute the backward outputs *)
- let ctx = ref ctx in
let rg_to_given_back_tys =
RegionGroupId.Map.map
(fun tys ->
@@ -3462,13 +3461,12 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
List.map
(fun ty ->
cassert __FILE__ __LINE__
- (not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty))
- !ctx.meta "The types shouldn't contain borrows";
- ctx_translate_fwd_ty !ctx ty)
+ (not (TypesUtils.ty_has_borrows ctx.type_ctx.type_infos ty))
+ ctx.meta "The types shouldn't contain borrows";
+ ctx_translate_fwd_ty ctx ty)
tys)
loop.rg_to_given_back_tys
in
- let ctx = !ctx in
(* The output type of the loop function *)
let fwd_effect_info = { ctx.sg.fwd_info.effect_info with is_rec = true } in
@@ -3573,6 +3571,44 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
{ types; const_generics; trait_refs }
in
+ (* Update the helpers to translate the fail and return expressions *)
+ let mk_panic =
+ (* Note that we reuse the effect information from the parent function *)
+ let effect_info = ctx_get_effect_info ctx in
+ let back_tys = compute_back_tys ctx.sg None in
+ let back_tys = List.filter_map (fun x -> x) back_tys in
+ let tys =
+ if ctx.sg.fwd_info.ignore_output then back_tys
+ else ctx.sg.fwd_output :: back_tys
+ in
+ let output_ty = mk_simpl_tuple_ty tys in
+ if effect_info.stateful then
+ (* Create the [Fail] value *)
+ let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
+ let ret_v =
+ mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
+ ret_ty
+ in
+ ret_v
+ else
+ mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
+ output_ty
+ in
+ let mk_return ctx v =
+ match v with
+ | None -> raise (Failure "Unexpected")
+ | Some output ->
+ let effect_info = ctx_get_effect_info ctx in
+ let output =
+ if effect_info.stateful then
+ let state_rvalue = mk_state_texpression ctx.state_var in
+ mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
+ else output
+ in
+ (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
+ mk_result_ok_texpression ctx.meta output
+ in
+
let loop_info =
{
loop_id;
@@ -3588,7 +3624,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
}
in
let loops = LoopId.Map.add loop_id loop_info ctx.loops in
- { ctx with loops }
+ { ctx with loops; mk_return = Some mk_return; mk_panic = Some mk_panic }
in
(* Update the context to translate the function end *)
@@ -3755,6 +3791,50 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
let effect_info =
get_fun_effect_info ctx (FunId (FRegular def_id)) None None
in
+ let mk_return ctx v =
+ match v with
+ | None ->
+ raise
+ (Failure
+ "Unexpected: reached a return expression without value in a \
+ function forward expression")
+ | Some output ->
+ let output =
+ if effect_info.stateful then
+ let state_rvalue = mk_state_texpression ctx.state_var in
+ mk_simpl_tuple_texpression ctx.meta [ state_rvalue; output ]
+ else output
+ in
+ (* Wrap in a result - TODO: check effect_info.can_fail to not always wrap *)
+ mk_result_ok_texpression ctx.meta output
+ in
+ let mk_panic =
+ (* TODO: we should use a [Fail] function *)
+ let mk_output output_ty =
+ if effect_info.stateful then
+ (* Create the [Fail] value *)
+ let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
+ let ret_v =
+ mk_result_fail_texpression_with_error_id ctx.meta
+ error_failure_id ret_ty
+ in
+ ret_v
+ else
+ mk_result_fail_texpression_with_error_id ctx.meta error_failure_id
+ output_ty
+ in
+ let back_tys = compute_back_tys ctx.sg None in
+ let back_tys = List.filter_map (fun x -> x) back_tys in
+ let tys =
+ if ctx.sg.fwd_info.ignore_output then back_tys
+ else ctx.sg.fwd_output :: back_tys
+ in
+ let output = mk_simpl_tuple_ty tys in
+ mk_output output
+ in
+ let ctx =
+ { ctx with mk_return = Some mk_return; mk_panic = Some mk_panic }
+ in
let body = translate_expression body ctx in
(* Add a match over the fuel, if necessary *)
let body =
@@ -3840,7 +3920,16 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
def
let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
- List.map (translate_type_decl ctx)
+ List.filter_map
+ (fun a ->
+ try Some (translate_type_decl ctx a)
+ with CFailure (meta, _) ->
+ let env = PrintPure.decls_ctx_to_fmt_env ctx in
+ let name = PrintPure.name_to_string env a.name in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate type decl '" ^ name
+ ^ "' because of previous error");
+ None)
(TypeDeclId.Map.values ctx.type_ctx.type_decls)
let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 348183c5..9460c5f4 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -41,7 +41,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
of backward functions, we also provide names for the outputs.
TODO: maybe we should introduce a record for this.
*)
-let translate_function_to_pure (trans_ctx : trans_ctx)
+let translate_function_to_pure_aux (trans_ctx : trans_ctx)
(pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t)
(fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) :
pure_fun_translation_no_loops =
@@ -158,6 +158,8 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
inside_loop = false;
loop_ids_map;
loops = Pure.LoopId.Map.empty;
+ mk_return = None;
+ mk_panic = None;
}
in
@@ -195,6 +197,20 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
| None -> SymbolicToPure.translate_fun_decl ctx None
| Some (_, ast) -> SymbolicToPure.translate_fun_decl ctx (Some ast)
+let translate_function_to_pure (trans_ctx : trans_ctx)
+ (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t)
+ (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) :
+ pure_fun_translation_no_loops option =
+ try
+ Some
+ (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef)
+ with CFailure (meta, _) ->
+ let name = name_to_string trans_ctx fdef.name in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate the function '" ^ name
+ ^ "' because of previous error");
+ None
+
(* TODO: factor out the return type *)
let translate_crate_to_pure (crate : crate) :
trans_ctx
@@ -220,32 +236,54 @@ let translate_crate_to_pure (crate : crate) :
(* Compute the decomposed fun sigs for the whole crate *)
let fun_dsigs =
FunDeclId.Map.of_list
- (List.map
+ (List.filter_map
(fun (fdef : LlbcAst.fun_decl) ->
- ( fdef.def_id,
- SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx
- fdef ))
+ try
+ Some
+ ( fdef.def_id,
+ SymbolicToPure.translate_fun_sig_from_decl_to_decomposed
+ trans_ctx fdef )
+ with CFailure (meta, _) ->
+ let name = name_to_string trans_ctx fdef.name in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate the function signature of '" ^ name
+ ^ "' because of previous error");
+ None)
(FunDeclId.Map.values crate.fun_decls))
in
(* Translate all the *transparent* functions *)
let pure_translations =
- List.map
+ List.filter_map
(translate_function_to_pure trans_ctx type_decls_map fun_dsigs)
(FunDeclId.Map.values crate.fun_decls)
in
(* Translate the trait declarations *)
let trait_decls =
- List.map
- (SymbolicToPure.translate_trait_decl trans_ctx)
+ List.filter_map
+ (fun a ->
+ try Some (SymbolicToPure.translate_trait_decl trans_ctx a)
+ with CFailure (meta, _) ->
+ let name = name_to_string trans_ctx a.name in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate the trait declaration '" ^ name
+ ^ "' because of previous error");
+ None)
(TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
in
(* Translate the trait implementations *)
let trait_impls =
- List.map
- (SymbolicToPure.translate_trait_impl trans_ctx)
+ List.filter_map
+ (fun a ->
+ try Some (SymbolicToPure.translate_trait_impl trans_ctx a)
+ with CFailure (meta, _) ->
+ let name = name_to_string trans_ctx a.name in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate the trait instance '" ^ name
+ ^ "' because of previous error");
+ None)
(TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
in
@@ -471,7 +509,15 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
groups are always singletons, so the [extract_global_decl] function
takes care of generating the delimiters.
*)
- let global = SymbolicToPure.translate_global ctx.trans_ctx global in
+ let global =
+ try Some (SymbolicToPure.translate_global ctx.trans_ctx global)
+ with CFailure (meta, _) ->
+ let name = name_to_string ctx.trans_ctx global.name in
+ save_error __FILE__ __LINE__ meta
+ ("Could not translate the global declaration '" ^ name
+ ^ "' because of previous error");
+ None
+ in
Extract.extract_global_decl ctx fmt global body config.interface
(** Utility.
@@ -726,22 +772,28 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
| TypeGroup (RecGroup ids) ->
if config.extract_types then export_types_group true ids
| FunGroup (NonRecGroup id) -> (
- (* Lookup *)
- let pure_fun = FunDeclId.Map.find id ctx.trans_funs in
+ (* Lookup - the translated function may not be in the map if we had
+ to ignore it because of errors *)
+ let pure_fun = FunDeclId.Map.find_opt id ctx.trans_funs in
(* Special case: we skip trait method *declarations* (we will
extract their type directly in the records we generate for
the trait declarations themselves, there is no point in having
separate type definitions) *)
- match pure_fun.f.Pure.kind with
- | TraitItemDecl _ -> ()
- | _ ->
- (* Translate *)
- export_functions_group [ pure_fun ])
+ match pure_fun with
+ | Some pure_fun -> (
+ match pure_fun.f.Pure.kind with
+ | TraitItemDecl _ -> ()
+ | _ ->
+ (* Translate *)
+ export_functions_group [ pure_fun ])
+ | None -> ())
| FunGroup (RecGroup ids) ->
(* General case of mutually recursive functions *)
(* Lookup *)
let pure_funs =
- List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids
+ List.filter_map
+ (fun id -> FunDeclId.Map.find_opt id ctx.trans_funs)
+ ids
in
(* Translate *)
export_functions_group pure_funs
@@ -899,7 +951,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
| Coq -> Printf.fprintf out "End %s.\n" fi.module_name);
(* Some logging *)
- log#linfo (lazy ("Generated: " ^ fi.filename));
+ if !Errors.error_list <> [] then
+ log#linfo
+ (lazy ("Generated the partial file (because of errors): " ^ fi.filename))
+ else log#linfo (lazy ("Generated: " ^ fi.filename));
(* Flush and close the file *)
close_out out
diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml
index f5dd7df4..b2c60cc6 100644
--- a/compiler/TypesUtils.ml
+++ b/compiler/TypesUtils.ml
@@ -12,6 +12,26 @@ let ty_has_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool =
let info = TypesAnalysis.analyze_ty infos ty in
info.TypesAnalysis.contains_borrow
+let ty_has_adt_with_borrows (infos : TypesAnalysis.type_infos) (ty : ty) : bool
+ =
+ let visitor =
+ object
+ inherit [_] iter_ty as super
+
+ method! visit_ty env ty =
+ match ty with
+ | TAdt (type_id, _) when type_id <> TTuple ->
+ let info = TypesAnalysis.analyze_ty infos ty in
+ if info.TypesAnalysis.contains_borrow then raise Found
+ else super#visit_ty env ty
+ | _ -> super#visit_ty env ty
+ end
+ in
+ try
+ visitor#visit_ty () ty;
+ false
+ with Found -> true
+
(** Retuns true if the type contains nested borrows.
Note that we can't simply explore the type and look for regions: sometimes
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 91010e07..b6ee66f5 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -160,7 +160,7 @@ let find_first_primitively_copyable_sv_with_borrows
method! visit_VSymbolic _ sv =
let ty = sv.sv_ty in
- if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then
+ if ty_is_copyable ty && ty_has_borrows type_infos ty then
raise (FoundSymbolicValue sv)
else ()
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:05:36 +0000