summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorEscherichia2024-03-28 13:56:31 +0100
committerEscherichia2024-03-28 15:45:45 +0100
commit5ad671a0960692af1c00609fa6864c6f44ca299c (patch)
tree2c210b418d8b417ace12a95c1707095c47861c1b /compiler
parent0f0082c81db8852dff23cd4691af19c434c8be78 (diff)
Should answer all comments, there are still some TODO: error message left
Diffstat (limited to 'compiler')
-rw-r--r--compiler/AssociatedTypes.ml20
-rw-r--r--compiler/Contexts.ml4
-rw-r--r--compiler/Errors.ml50
-rw-r--r--compiler/Extract.ml37
-rw-r--r--compiler/ExtractBase.ml88
-rw-r--r--compiler/ExtractName.ml12
-rw-r--r--compiler/ExtractTypes.ml33
-rw-r--r--compiler/FunsAnalysis.ml4
-rw-r--r--compiler/Interpreter.ml16
-rw-r--r--compiler/InterpreterBorrows.ml132
-rw-r--r--compiler/InterpreterBorrowsCore.ml54
-rw-r--r--compiler/InterpreterExpansion.ml36
-rw-r--r--compiler/InterpreterExpressions.ml68
-rw-r--r--compiler/InterpreterLoops.ml24
-rw-r--r--compiler/InterpreterLoopsCore.ml32
-rw-r--r--compiler/InterpreterLoopsFixedPoint.ml44
-rw-r--r--compiler/InterpreterLoopsJoinCtxs.ml42
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml322
-rw-r--r--compiler/InterpreterPaths.ml18
-rw-r--r--compiler/InterpreterProjectors.ml10
-rw-r--r--compiler/InterpreterStatements.ml64
-rw-r--r--compiler/InterpreterStatements.mli2
-rw-r--r--compiler/InterpreterUtils.ml22
-rw-r--r--compiler/Invariants.ml164
-rw-r--r--compiler/Main.ml2
-rw-r--r--compiler/PrePasses.ml7
-rw-r--r--compiler/Print.ml134
-rw-r--r--compiler/PrintPure.ml102
-rw-r--r--compiler/PureMicroPasses.ml13
-rw-r--r--compiler/PureTypeCheck.ml64
-rw-r--r--compiler/PureUtils.ml27
-rw-r--r--compiler/RegionsHierarchy.ml10
-rw-r--r--compiler/Substitute.ml6
-rw-r--r--compiler/SymbolicToPure.ml68
-rw-r--r--compiler/SynthesizeSymbolic.ml4
-rw-r--r--compiler/Translate.ml14
-rw-r--r--compiler/ValuesUtils.ml10
37 files changed, 882 insertions, 877 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index 70739b3c..a4b0e921 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -239,7 +239,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
match trait_ref.trait_id with
| TraitRef { trait_id = TraitImpl impl_id; generics = ref_generics; _ }
->
- cassert_opt_meta (ref_generics = empty_generic_args) ctx.meta "Higher order types are not supported yet TODO: error message";
+ cassert_opt_meta (ref_generics = empty_generic_args) ctx.meta "Higher order trait types are not supported yet";
log#ldebug
(lazy
("norm_ctx_normalize_ty: trait type: trait ref: "
@@ -279,7 +279,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty =
^ trait_ref_to_string ctx trait_ref
^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref));
(* We can't project *)
- cassert_opt_meta (trait_instance_id_is_local_clause trait_ref.trait_id) ctx.meta "TODO: error message";
+ sanity_check_opt_meta (trait_instance_id_is_local_clause trait_ref.trait_id) ctx.meta ;
TTraitType (trait_ref, type_name)
in
let tr : trait_type_ref = { trait_ref; type_name } in
@@ -347,7 +347,7 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
match impl with
| None ->
(* This is actually a local clause *)
- cassert_opt_meta (trait_instance_id_is_local_clause inst_id) ctx.meta "TODO: error message";
+ sanity_check_opt_meta (trait_instance_id_is_local_clause inst_id) ctx.meta ;
(ParentClause (inst_id, decl_id, clause_id), None)
| Some impl ->
(* We figure out the parent clause by doing the following:
@@ -378,7 +378,7 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
match impl with
| None ->
(* This is actually a local clause *)
- cassert_opt_meta (trait_instance_id_is_local_clause inst_id) ctx.meta "Trait instance id is not a local clause";
+ sanity_check_opt_meta (trait_instance_id_is_local_clause inst_id) ctx.meta ;
(ItemClause (inst_id, decl_id, item_name, clause_id), None)
| Some impl ->
(* We figure out the item clause by doing the following:
@@ -511,7 +511,7 @@ let ctx_normalize_trait_type_constraint (meta : Meta.meta) (ctx : eval_ctx)
norm_ctx_normalize_trait_type_constraint (mk_norm_ctx meta ctx) ttc
(** Same as [type_decl_get_instantiated_variants_fields_types] but normalizes the types *)
-let type_decl_get_inst_norm_variants_fields_rtypes (ctx : eval_ctx)
+let type_decl_get_inst_norm_variants_fields_rtypes (meta : Meta.meta) (ctx : eval_ctx)
(def : type_decl) (generics : generic_args) :
(VariantId.id option * ty list) list =
let res =
@@ -519,16 +519,16 @@ let type_decl_get_inst_norm_variants_fields_rtypes (ctx : eval_ctx)
in
List.map
(fun (variant_id, types) ->
- (variant_id, List.map (ctx_normalize_ty def.meta ctx) types))
+ (variant_id, List.map (ctx_normalize_ty meta ctx) types))
res
(** Same as [type_decl_get_instantiated_field_types] but normalizes the types *)
-let type_decl_get_inst_norm_field_rtypes (ctx : eval_ctx) (def : type_decl)
+let type_decl_get_inst_norm_field_rtypes (meta : Meta.meta) (ctx : eval_ctx) (def : type_decl)
(opt_variant_id : VariantId.id option) (generics : generic_args) : ty list =
let types =
Subst.type_decl_get_instantiated_field_types def opt_variant_id generics
in
- List.map (ctx_normalize_ty def.meta ctx) types
+ List.map (ctx_normalize_ty meta ctx) types
(** Same as [ctx_adt_value_get_instantiated_field_rtypes] but normalizes the types *)
let ctx_adt_value_get_inst_norm_field_rtypes (meta : Meta.meta) (ctx : eval_ctx) (adt : adt_value)
@@ -540,12 +540,12 @@ let ctx_adt_value_get_inst_norm_field_rtypes (meta : Meta.meta) (ctx : eval_ctx)
(** Same as [ctx_adt_value_get_instantiated_field_types] but normalizes the types
and erases the regions. *)
-let type_decl_get_inst_norm_field_etypes (ctx : eval_ctx) (def : type_decl)
+let type_decl_get_inst_norm_field_etypes (meta : Meta.meta) (ctx : eval_ctx) (def : type_decl)
(opt_variant_id : VariantId.id option) (generics : generic_args) : ty list =
let types =
Subst.type_decl_get_instantiated_field_types def opt_variant_id generics
in
- let types = List.map (ctx_normalize_ty def.meta ctx) types in
+ let types = List.map (ctx_normalize_ty meta ctx) types in
List.map Subst.erase_regions types
(** Same as [ctx_adt_get_instantiated_field_types] but normalizes the types and
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 558aaa4e..51392edf 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -371,7 +371,7 @@ let ctx_update_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) (n
is important).
*)
let ctx_push_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
- cassert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty) meta "Pushed variables and their values do not have the same type TODO: Error message";
+ cassert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty) meta "The pushed variables and their values do not have the same type";
let bv = var_to_binder var in
{ ctx with env = EBinding (BVar bv, v) :: ctx.env }
@@ -395,7 +395,7 @@ let ctx_push_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : (var * typed_value
List.for_all
(fun (var, (value : typed_value)) ->
TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
- vars) meta "Pushed variables and their values do not have the same type TODO: Error message";
+ vars) meta "The pushed variables and their values do not have the same type TODO: Error message";
let vars =
List.map
(fun (var, value) -> EBinding (BVar (var_to_binder var), value))
diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 4c51720f..aff62022 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -11,38 +11,48 @@ let format_error_message (meta : Meta.meta) msg =
exception CFailure of string
-
let error_list : (Meta.meta option * string) list ref = ref []
-let save_error (meta : Meta.meta option) (msg : string) = error_list := (meta, msg)::(!error_list)
-
-let craise (meta : Meta.meta) (msg : string) =
- if !Config.fail_hard then
- raise (Failure (format_error_message meta msg))
- else
- let () = save_error (Some meta) msg in
- raise (CFailure msg)
+let push_error (meta : Meta.meta option) (msg : string) = error_list := (meta, msg)::(!error_list)
-let cassert (b : bool) (meta : Meta.meta) (msg : string) =
- if b then
- craise meta msg
+let save_error ?(b : bool = true) (meta : Meta.meta option) (msg : string) =
+ push_error meta msg;
+ match meta with
+ | Some m ->
+ if !Config.fail_hard && b then
+ raise (Failure (format_error_message m msg))
+ | None ->
+ if !Config.fail_hard && b then
+ raise (Failure msg)
let craise_opt_meta (meta : Meta.meta option) (msg : string) =
match meta with
- | Some m -> craise m msg
+ | Some m ->
+ if !Config.fail_hard then
+ raise (Failure (format_error_message m msg))
+ else
+ let () = push_error (Some m) msg in
+ raise (CFailure msg)
| None ->
- let () = save_error (None) msg in
+ if !Config.fail_hard then
+ raise (Failure msg)
+ else
+ let () = push_error None msg in
raise (CFailure msg)
+let craise (meta : Meta.meta) (msg : string) =
+ craise_opt_meta (Some meta) msg
+
let cassert_opt_meta (b : bool) (meta : Meta.meta option) (msg : string) =
- match meta with
- | Some m -> cassert b m msg
- | None ->
- if b then
- let () = save_error (None) msg in
- raise (CFailure msg)
+ if b then
+ craise_opt_meta meta msg
+
+let cassert (b : bool) (meta : Meta.meta) (msg : string) =
+ cassert_opt_meta b (Some meta) msg
let sanity_check b meta = cassert b meta "Internal error, please file an issue"
let sanity_check_opt_meta b meta = cassert_opt_meta b meta "Internal error, please file an issue"
+let internal_error meta = craise meta "Internal error, please report an issue"
+
let exec_raise = craise
let exec_assert = cassert \ No newline at end of file
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 82656273..0e86e187 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -128,8 +128,8 @@ let extract_adt_g_value (meta : Meta.meta)
| TAdt (TTuple, generics) ->
(* Tuple *)
(* For now, we only support fully applied tuple constructors *)
- cassert (List.length generics.types = List.length field_values) meta "Only applied tuple constructors are currently supported";
- cassert (generics.const_generics = [] && generics.trait_refs = []) meta "Only applied tuple constructors are currently supported";
+ cassert (List.length generics.types = List.length field_values) meta "Only fully applied tuple constructors are currently supported";
+ cassert (generics.const_generics = [] && generics.trait_refs = []) meta "Only fully applied tuple constructors are currently supported";
extract_as_tuple ()
| TAdt (adt_id, _) ->
(* "Regular" ADT *)
@@ -188,7 +188,6 @@ let extract_adt_g_value (meta : Meta.meta)
(* Extract globals in the same way as variables *)
let extract_global (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(id : A.GlobalDeclId.id) (generics : generic_args) : unit =
- (* let trait_decl = GlobalDeclId.Map.find id ctx.trait_decl_id in there might be a way to extract the meta ? *)
let use_brackets = inside && generics <> empty_generic_args in
F.pp_open_hvbox fmt ctx.indent_incr;
if use_brackets then F.pp_print_string fmt "(";
@@ -449,7 +448,7 @@ and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.for
if not method_id.is_provided then (
(* Required method *)
- cassert (lp_id = None) trait_decl.meta "TODO: Error message";
+ sanity_check (lp_id = None) trait_decl.meta ;
extract_trait_ref trait_decl.meta ctx fmt TypeDeclId.Set.empty true trait_ref;
let fun_name =
ctx_get_trait_method meta trait_ref.trait_decl_ref.trait_decl_id
@@ -498,9 +497,10 @@ and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.for
| Error (types, err) ->
extract_generic_args meta ctx fmt TypeDeclId.Set.empty
{ generics with types };
- if !Config.fail_hard then craise meta err
- else
- F.pp_print_string fmt
+ (* if !Config.fail_hard then craise meta err
+ else *)
+ save_error (Some meta) err;
+ F.pp_print_string fmt
"(\"ERROR: ill-formed builtin: invalid number of filtering \
arguments\")");
(* Print the arguments *)
@@ -645,7 +645,7 @@ and extract_Lambda (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
(* Open parentheses *)
if inside then F.pp_print_string fmt "(";
(* Print the lambda - note that there should always be at least one variable *)
- cassert (xl <> []) meta "TODO: error message";
+ sanity_check (xl <> []) meta ;
F.pp_print_string fmt "fun";
let with_type = !backend = Coq in
let ctx =
@@ -944,7 +944,7 @@ and extract_StructUpdate (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.form
(inside : bool) (e_ty : ty) (supd : struct_update) : unit =
(* We can't update a subset of the fields in Coq (i.e., we can do
[{| x:= 3; y := 4 |}], but there is no syntax for [{| s with x := 3 |}]) *)
- cassert (!backend <> Coq || supd.init = None) meta "TODO: error message";
+ sanity_check (!backend <> Coq || supd.init = None) meta ;
(* In the case of HOL4, records with no fields are not supported and are
thus extracted to unit. We need to check that by looking up the definition *)
let extract_as_unit =
@@ -1188,7 +1188,7 @@ let assert_backend_supports_decreases_clauses (meta : Meta.meta) =
| FStar | Lean -> ()
| _ ->
craise
- meta "decreases clauses only supported for the Lean & F* backends"
+ meta "Decreases clauses are only supported for the Lean and F* backends"
(** Extract a decreases clause function template body.
@@ -1208,7 +1208,7 @@ let assert_backend_supports_decreases_clauses (meta : Meta.meta) =
*)
let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : unit =
- cassert (!backend = FStar) def.meta "TODO: error message";
+ cassert (!backend = FStar) def.meta "The generation of template decrease clauses is only supported for the F* backend";
(* Retrieve the function name *)
let def_name = ctx_get_termination_measure def.meta def.def_id def.loop_id ctx in
@@ -1273,7 +1273,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
*)
let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : unit =
- cassert (!backend = Lean) def.meta "TODO: error message";
+ cassert (!backend = Lean) def.meta "The generation of template termination and decreasing clauses is only supported for the Lean backend" ;
(*
* Extract a template for the termination measure
*)
@@ -1396,7 +1396,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
- cassert (not def.is_global_decl_body) def.meta "TODO: error message";
+ sanity_check (not def.is_global_decl_body) def.meta ;
(* Retrieve the function name *)
let def_name = ctx_get_local_function def.meta def.def_id def.loop_id ctx in
(* Add a break before *)
@@ -1643,7 +1643,7 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
(def : fun_decl) : unit =
(* Retrieve the definition name *)
let def_name = ctx_get_local_function def.meta def.def_id def.loop_id ctx in
- cassert (def.signature.generics.const_generics = []) def.meta "TODO: error message";
+ cassert (def.signature.generics.const_generics = []) def.meta "Constant generics are not supported yet when generating code for HOL4";
(* Add the type/const gen parameters - note that we need those bindings
only for the generation of the type (they are not top-level) *)
let ctx, _, _, _ =
@@ -1689,7 +1689,7 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
- cassert (not def.is_global_decl_body) def.meta "TODO: error message";
+ sanity_check (not def.is_global_decl_body) def.meta ;
(* We treat HOL4 opaque functions in a specific manner *)
if !backend = HOL4 && Option.is_none def.body then
extract_fun_decl_hol4_opaque ctx fmt def
@@ -2252,7 +2252,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
- we only generate trait clauses for the clauses we find in the
pure generics *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params decl.meta f.llbc_name f.signature.llbc_generics generics ctx (* TODO: confirm it's the right meta*)
+ ctx_add_generic_params decl.meta f.llbc_name f.signature.llbc_generics generics ctx
in
let backend_uses_forall =
match !backend with Coq | Lean -> true | FStar | HOL4 -> false
@@ -2263,7 +2263,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
let use_forall_use_sep = false in
extract_generic_params decl.meta ctx fmt TypeDeclId.Set.empty ~use_forall
~use_forall_use_sep ~use_arrows generics type_params cg_params
- trait_clauses; (* TODO: confirm it's the right meta*)
+ trait_clauses;
if use_forall then F.pp_print_string fmt ",";
(* Extract the inputs and output *)
F.pp_print_space fmt ();
@@ -2558,8 +2558,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
in
extract_trait_impl_item ctx fmt fun_name ty
-(** Extract a trait implementation
- * TODO: check if impl.meta everywhere is the right meta
+(** Extract a trait implementation
*)
let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(impl : trait_impl) : unit =
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 1c21e99c..022643f5 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -262,9 +262,8 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
\"" ^ name ^ "\":" ^ id1 ^ id2
^ "\nYou may want to rename some of your definitions, or report an issue."
in
- log#serror err;
(* If we fail hard on errors, raise an exception *)
- craise_opt_meta None err
+ save_error None err
let names_map_get_id_from_name (name : string) (nm : names_map) : id option =
StringMap.find_opt name nm.name_to_id
@@ -296,9 +295,8 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
"Error when registering the name for id: " ^ id_to_string id
^ ":\nThe chosen name is already in the names set: " ^ name
in
- log#serror err;
(* If we fail hard on errors, raise an exception *)
- craise_opt_meta None err);
+ save_error None err);
(* Insert *)
names_map_add_unchecked id name nm
@@ -425,7 +423,7 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
(** The [id_to_string] function to print nice debugging messages if there are
collisions *)
-let names_maps_get ?(meta = None) (id_to_string : id -> string) (id : id) (nm : names_maps) :
+let names_maps_get (meta : Meta.meta option) (id_to_string : id -> string) (id : id) (nm : names_maps) :
string =
(* We do not use the same name map if we allow/disallow collisions *)
let map_to_string (m : string IdMap.t) : string =
@@ -445,9 +443,8 @@ let names_maps_get ?(meta = None) (id_to_string : id -> string) (id : id) (nm :
"Could not find: " ^ id_to_string id ^ "\nNames map:\n"
^ map_to_string m
in
- log#serror err;
- if !Config.fail_hard then craise_opt_meta meta err
- else "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)")
+ save_error meta err;
+ "(%%%ERROR: unknown identifier\": " ^ id_to_string id ^ "\"%%%)")
else
let m = nm.names_map.id_to_name in
match IdMap.find_opt id m with
@@ -457,9 +454,8 @@ let names_maps_get ?(meta = None) (id_to_string : id -> string) (id : id) (nm :
"Could not find: " ^ id_to_string id ^ "\nNames map:\n"
^ map_to_string m
in
- log#serror err;
- if !Config.fail_hard then craise_opt_meta meta err
- else "(ERROR: \"" ^ id_to_string id ^ "\")"
+ save_error meta err;
+ "(ERROR: \"" ^ id_to_string id ^ "\")"
type names_map_init = {
keywords : string list;
@@ -591,17 +587,17 @@ let llbc_fun_id_to_string (ctx : extraction_ctx) =
let fun_id_to_string (ctx : extraction_ctx) =
PrintPure.regular_fun_id_to_string (extraction_ctx_to_fmt_env ctx)
-let adt_variant_to_string ?(meta = None) (ctx : extraction_ctx) =
+let adt_variant_to_string (meta : Meta.meta option) (ctx : extraction_ctx) =
PrintPure.adt_variant_to_string ~meta:meta (extraction_ctx_to_fmt_env ctx)
-let adt_field_to_string ?(meta = None) (ctx : extraction_ctx) =
+let adt_field_to_string (meta : Meta.meta option) (ctx : extraction_ctx) =
PrintPure.adt_field_to_string ~meta:meta (extraction_ctx_to_fmt_env ctx)
(** Debugging function, used when communicating name collisions to the user,
and also to print ids for internal debugging (in case of lookup miss for
instance).
*)
-let id_to_string ?(meta = None) (id : id) (ctx : extraction_ctx) : string =
+let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string =
let trait_decl_id_to_string (id : A.TraitDeclId.id) : string =
let trait_name = trait_decl_id_to_string ctx id in
"trait_decl: " ^ trait_name ^ " (id: " ^ A.TraitDeclId.to_string id ^ ")"
@@ -629,11 +625,11 @@ let id_to_string ?(meta = None) (id : id) (ctx : extraction_ctx) : string =
| StructId id -> "struct constructor of: " ^ type_id_to_string ctx id
| VariantId (id, variant_id) ->
let type_name = type_id_to_string ctx id in
- let variant_name = adt_variant_to_string ~meta:meta ctx id (Some variant_id) in
+ let variant_name = adt_variant_to_string meta ctx id (Some variant_id) in
"type name: " ^ type_name ^ ", variant name: " ^ variant_name
| FieldId (id, field_id) ->
let type_name = type_id_to_string ctx id in
- let field_name = adt_field_to_string ~meta:meta ctx id field_id in
+ let field_name = adt_field_to_string meta ctx id field_id in
"type name: " ^ type_name ^ ", field name: " ^ field_name
| UnknownId -> "keyword"
| TypeVarId id -> "type_var_id: " ^ TypeVarId.to_string id
@@ -660,50 +656,50 @@ let id_to_string ?(meta = None) (id : id) (ctx : extraction_ctx) : string =
| TraitSelfClauseId -> "trait_self_clause"
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 ~meta:(Some meta) id ctx in
+ 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
{ ctx with names_maps }
-let ctx_get ?(meta = None) (id : id) (ctx : extraction_ctx) : string =
- let id_to_string (id : id) : string = id_to_string ~meta:meta id ctx in
- names_maps_get ~meta:meta id_to_string id ctx.names_maps (* TODO check if we can remove the meta arg, same for following functions*)
+let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string =
+ let id_to_string (id : id) : string = id_to_string meta id ctx in
+ names_maps_get meta id_to_string id ctx.names_maps
let ctx_get_global (meta : Meta.meta) (id : A.GlobalDeclId.id) (ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (GlobalId id) ctx
+ ctx_get (Some meta) (GlobalId id) ctx
let ctx_get_function (meta : Meta.meta) (id : fun_id) (ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (FunId id) ctx
+ ctx_get (Some meta) (FunId id) ctx
let ctx_get_local_function (meta : Meta.meta) (id : A.FunDeclId.id) (lp : LoopId.id option)
(ctx : extraction_ctx) : string =
ctx_get_function meta (FromLlbc (FunId (FRegular id), lp)) ctx
-let ctx_get_type ?(meta=None) (id : type_id) (ctx : extraction_ctx) : string =
- cassert_opt_meta (id <> TTuple) meta "TODO: error message";
- ctx_get ~meta:meta (TypeId id) ctx
+let ctx_get_type (meta : Meta.meta option) (id : type_id) (ctx : extraction_ctx) : string =
+ sanity_check_opt_meta (id <> TTuple) meta;
+ ctx_get meta (TypeId id) ctx
let ctx_get_local_type (meta : Meta.meta) (id : TypeDeclId.id) (ctx : extraction_ctx) : string =
- ctx_get_type ~meta:(Some meta) (TAdtId id) ctx
+ ctx_get_type (Some meta) (TAdtId id) ctx
-let ctx_get_assumed_type ?(meta = None) (id : assumed_ty) (ctx : extraction_ctx) : string =
- ctx_get_type ~meta:meta (TAssumed id) ctx
+let ctx_get_assumed_type (meta : Meta.meta option) (id : assumed_ty) (ctx : extraction_ctx) : string =
+ ctx_get_type meta (TAssumed id) ctx
let ctx_get_trait_constructor (meta : Meta.meta) (id : trait_decl_id) (ctx : extraction_ctx) :
string =
- ctx_get ~meta:(Some meta) (TraitDeclConstructorId id) ctx
+ ctx_get (Some meta) (TraitDeclConstructorId id) ctx
let ctx_get_trait_self_clause (meta : Meta.meta) (ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) TraitSelfClauseId ctx
+ ctx_get (Some meta) TraitSelfClauseId ctx
let ctx_get_trait_decl (meta : Meta.meta) (id : trait_decl_id) (ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (TraitDeclId id) ctx
+ ctx_get (Some meta) (TraitDeclId id) ctx
let ctx_get_trait_impl (meta : Meta.meta) (id : trait_impl_id) (ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (TraitImplId id) ctx
+ ctx_get (Some meta) (TraitImplId id) ctx
let ctx_get_trait_item (meta : Meta.meta) (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (TraitItemId (id, item_name)) ctx
+ ctx_get (Some meta) (TraitItemId (id, item_name)) ctx
let ctx_get_trait_const (meta : Meta.meta) (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
@@ -715,48 +711,48 @@ let ctx_get_trait_type (meta : Meta.meta) (id : trait_decl_id) (item_name : stri
let ctx_get_trait_method (meta : Meta.meta) (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (TraitMethodId (id, item_name)) ctx
+ ctx_get (Some meta) (TraitMethodId (id, item_name)) ctx
let ctx_get_trait_parent_clause (meta : Meta.meta) (id : trait_decl_id) (clause : trait_clause_id)
(ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (TraitParentClauseId (id, clause)) ctx
+ ctx_get (Some meta) (TraitParentClauseId (id, clause)) ctx
let ctx_get_trait_item_clause (meta : Meta.meta) (id : trait_decl_id) (item : string)
(clause : trait_clause_id) (ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (TraitItemClauseId (id, item, clause)) ctx
+ ctx_get (Some meta) (TraitItemClauseId (id, item, clause)) ctx
let ctx_get_var (meta : Meta.meta) (id : VarId.id) (ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (VarId id) ctx
+ ctx_get (Some meta) (VarId id) ctx
let ctx_get_type_var (meta : Meta.meta) (id : TypeVarId.id) (ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (TypeVarId id) ctx
+ ctx_get (Some meta) (TypeVarId id) ctx
let ctx_get_const_generic_var (meta : Meta.meta) (id : ConstGenericVarId.id) (ctx : extraction_ctx)
: string =
- ctx_get ~meta:(Some meta) (ConstGenericVarId id) ctx
+ ctx_get (Some meta) (ConstGenericVarId id) ctx
let ctx_get_local_trait_clause (meta : Meta.meta) (id : TraitClauseId.id) (ctx : extraction_ctx) :
string =
- ctx_get ~meta:(Some meta) (LocalTraitClauseId id) ctx
+ ctx_get (Some meta) (LocalTraitClauseId id) ctx
let ctx_get_field (meta : Meta.meta) (type_id : type_id) (field_id : FieldId.id)
(ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (FieldId (type_id, field_id)) ctx
+ ctx_get (Some meta) (FieldId (type_id, field_id)) ctx
let ctx_get_struct (meta : Meta.meta) (def_id : type_id) (ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (StructId def_id) ctx
+ ctx_get (Some meta) (StructId def_id) ctx
let ctx_get_variant (meta : Meta.meta) (def_id : type_id) (variant_id : VariantId.id)
(ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (VariantId (def_id, variant_id)) ctx
+ ctx_get (Some meta) (VariantId (def_id, variant_id)) ctx
let ctx_get_decreases_proof (meta : Meta.meta) (def_id : A.FunDeclId.id)
(loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (DecreasesProofId (FRegular def_id, loop_id)) ctx
+ ctx_get (Some meta) (DecreasesProofId (FRegular def_id, loop_id)) ctx
let ctx_get_termination_measure (meta : Meta.meta) (def_id : A.FunDeclId.id)
(loop_id : LoopId.id option) (ctx : extraction_ctx) : string =
- ctx_get ~meta:(Some meta) (TerminationMeasureId (FRegular def_id, loop_id)) ctx
+ ctx_get (Some meta) (TerminationMeasureId (FRegular def_id, loop_id)) ctx
(** Small helper to compute the name of a unary operation *)
let unop_name (unop : unop) : string =
@@ -1633,7 +1629,7 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx) (basename
let cl = to_snake_case name in
let cl = String.split_on_char '_' cl in
let cl = List.filter (fun s -> String.length s > 0) cl in
- cassert (List.length cl > 0) meta "TODO: error message";
+ sanity_check (List.length cl > 0) meta;
let cl = List.map (fun s -> s.[0]) cl in
StringUtils.string_of_chars cl
in
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 9df5b03e..c4e145a0 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -32,7 +32,7 @@ end
For impl blocks, we simply use the name of the type (without its arguments)
if all the arguments are variables.
*)
-let pattern_to_extract_name ?(meta = None) (name : pattern) : string list =
+let pattern_to_extract_name (meta : Meta.meta option) (name : pattern) : string list =
let c = { tgt = TkName } in
let all_vars =
let check (g : generic_arg) : bool =
@@ -92,9 +92,9 @@ let pattern_to_extract_name ?(meta = None) (name : pattern) : string list =
let name = visitor#visit_pattern () name in
List.map (pattern_elem_to_string c) name
-let pattern_to_type_extract_name = pattern_to_extract_name
-let pattern_to_fun_extract_name = pattern_to_extract_name
-let pattern_to_trait_impl_extract_name = pattern_to_extract_name
+let pattern_to_type_extract_name = pattern_to_extract_name None
+let pattern_to_fun_extract_name = pattern_to_extract_name None
+let pattern_to_trait_impl_extract_name = pattern_to_extract_name None
(* TODO: this is provisional. We just want to make sure that the extraction
names we derive from the patterns (for the builtin definitions) are
@@ -103,7 +103,7 @@ let name_to_simple_name (ctx : ctx) (n : Types.name) : string list =
let c : to_pat_config =
{ tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs }
in
- pattern_to_extract_name (name_to_pattern ctx c n)
+ pattern_to_extract_name None (name_to_pattern ctx c n)
(** If the [prefix] is Some, we attempt to remove the common prefix
between [prefix] and [name] from [name] *)
@@ -125,4 +125,4 @@ let name_with_generics_to_simple_name (ctx : ctx)
let _, _, name = pattern_common_prefix { equiv = true } prefix name in
name
in
- pattern_to_extract_name name
+ pattern_to_extract_name None name
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 02aaec65..a8143876 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -287,7 +287,7 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt
("val [" ^ String.concat ", " names ^ "] = DefineDiv ‘")
else (
- assert (List.length names = 1) (* TODO: Error message, meta todo*);
+ sanity_check_opt_meta (List.length names = 1) None;
let name = List.hd names in
F.pp_print_string fmt ("val " ^ name ^ " = Define ‘"));
F.pp_print_cut fmt ()
@@ -470,7 +470,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
if print_paren then F.pp_print_string fmt "(";
(* TODO: for now, only the opaque *functions* are extracted in the
opaque module. The opaque *types* are assumed. *)
- F.pp_print_string fmt (ctx_get_type ~meta:(Some meta) type_id ctx);
+ F.pp_print_string fmt (ctx_get_type (Some meta) type_id ctx);
(* We might need to filter the type arguments, if the type
is builtin (for instance, we filter the global allocator type
argument for `Vec`). *)
@@ -496,7 +496,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
| HOL4 ->
let { types; const_generics; trait_refs } = generics in
(* Const generics are not supported in HOL4 *)
- cassert (const_generics = []) meta "Const generics are not supported in HOL4";
+ cassert (const_generics = []) meta "Constant generics are not supported yet when generating code for HOL4";
let print_tys =
match type_id with
| TAdtId id -> not (TypeDeclId.Set.mem id no_params_tys)
@@ -513,7 +513,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
(extract_rec true) types;
if print_paren then F.pp_print_string fmt ")";
F.pp_print_space fmt ());
- F.pp_print_string fmt (ctx_get_type ~meta:(Some meta) type_id ctx);
+ F.pp_print_string fmt (ctx_get_type (Some meta) type_id ctx);
if trait_refs <> [] then (
F.pp_print_space fmt ();
Collections.List.iter_link (F.pp_print_space fmt)
@@ -554,7 +554,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt type_name
| _ ->
(* HOL4 doesn't have 1st class types *)
- cassert (!backend <> HOL4) meta "TODO: Error message";
+ cassert (!backend <> HOL4) meta "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))
@@ -606,7 +606,7 @@ and extract_generic_args (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.form
(extract_ty meta ctx fmt no_params_tys true)
types);
if const_generics <> [] then (
- cassert (!backend <> HOL4) meta "TODO: Error message";
+ cassert (!backend <> HOL4) meta "Constant generics are not supported yet when generating code for HOL4";
F.pp_print_space fmt ();
Collections.List.iter_link (F.pp_print_space fmt)
(extract_const_generic meta ctx fmt true)
@@ -661,9 +661,8 @@ and extract_trait_instance_id (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F
| Self ->
(* This has a specific treatment depending on the item we're extracting
(associated type, etc.). We should have caught this elsewhere. *)
- if !Config.fail_hard then
- craise meta "Unexpected occurrence of `Self`"
- else F.pp_print_string fmt "ERROR(\"Unexpected Self\")"
+ save_error (Some meta) "Unexpected occurrence of `Self`";
+ F.pp_print_string fmt "ERROR(\"Unexpected Self\")"
| TraitImpl id ->
let name = ctx_get_trait_impl meta id ctx in
F.pp_print_string fmt name
@@ -1076,7 +1075,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
else (
(* We extract for Coq or Lean, and we have a recursive record, or a record in
a group of mutually recursive types: we extract it as an inductive type *)
- cassert (is_rec && (!backend = Coq || !backend = Lean)) def.meta "TODO: error message";
+ cassert (is_rec && (!backend = Coq || !backend = Lean)) def.meta "Constant generics are not supported yet when generating code for HOL4";
(* Small trick: in Lean we use namespaces, meaning we don't need to prefix
the constructor name with the name of the type at definition site,
i.e., instead of generating `inductive Foo := | MkFoo ...` like in Coq
@@ -1177,7 +1176,7 @@ let extract_generic_params (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.fo
(trait_clauses : string list) : unit =
let all_params = List.concat [ type_params; cg_params; trait_clauses ] in
(* HOL4 doesn't support const generics *)
- cassert (cg_params = [] || !backend <> HOL4) meta "HOL4 doesn't support const generics";
+ cassert (cg_params = [] || !backend <> HOL4) meta "Constant generics are not supported yet when generating code for HOL4";
let left_bracket (implicit : bool) =
if implicit && !backend <> FStar then F.pp_print_string fmt "{"
else F.pp_print_string fmt "("
@@ -1395,7 +1394,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
| None -> F.pp_print_string fmt def_name);
(* HOL4 doesn't support const generics, and type definitions in HOL4 don't
support trait clauses *)
- cassert ((cg_params = [] && trait_clauses = []) || !backend <> HOL4) def.meta "HOL4 doesn't support const generics, and type definitions in HOL4 don't support trait clauses";
+ cassert ((cg_params = [] && trait_clauses = []) || !backend <> HOL4) def.meta "Constant generics and type definitions with trait clauses are not supported yet when generating code for HOL4";
(* Print the generic parameters *)
extract_generic_params def.meta ctx_body fmt type_decl_group ~use_forall def.generics
type_params cg_params trait_clauses;
@@ -1464,9 +1463,9 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
(* Retrieve the definition name *)
let def_name = ctx_get_local_type def.meta def.def_id ctx in
(* Generic parameters are unsupported *)
- cassert (def.generics.const_generics = []) def.meta "Generic parameters are unsupported";
+ cassert (def.generics.const_generics = []) def.meta "Constant generics are not supported yet when generating code for HOL4";
(* Trait clauses on type definitions are unsupported *)
- cassert (def.generics.trait_clauses = []) def.meta "Trait clauses on type definitions are unsupported";
+ cassert (def.generics.trait_clauses = []) def.meta "Types with trait clauses are not supported yet when generating code for HOL4";
(* Types *)
(* Count the number of parameters *)
let num_params = List.length def.generics.types in
@@ -1565,7 +1564,7 @@ let extract_coq_arguments_instruction (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (decl : type_decl) : unit =
- cassert (!backend = Coq) decl.meta "TODO: error message";
+ sanity_check (!backend = Coq) decl.meta;
(* Generating the [Arguments] instructions is useful only if there are parameters *)
let num_params =
List.length decl.generics.types
@@ -1611,7 +1610,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
(fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
- cassert (!backend = Coq) decl.meta "TODO: error message";
+ sanity_check (!backend = Coq) decl.meta;
match decl.kind with
| Opaque | Enum _ -> ()
| Struct fields ->
@@ -1782,7 +1781,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
* one line *)
F.pp_open_hvbox fmt 0;
(* Retrieve the name *)
- let state_name = ctx_get_assumed_type TState ctx in
+ let state_name = ctx_get_assumed_type None TState ctx in
(* The syntax for Lean and Coq is almost identical. *)
let print_axiom () =
let axiom =
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index f3840a8c..9ca35e79 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -167,8 +167,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
(* We need to know if the declaration group contains a global - note that
* groups containing globals contain exactly one declaration *)
let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in
- cassert ((not is_global_decl_body) || List.length d = 1) (List.hd d).meta "The declaration group should containing globals should contain exactly one declaration"; (*TODO recheck how to get meta*)
- cassert ((not !group_has_builtin_info) || List.length d = 1) (List.hd d).meta "The declaration group should containing globals should contain exactly one declaration";
+ cassert ((not is_global_decl_body) || List.length d = 1) (List.hd d).meta "This global definition is in a group of mutually recursive definitions";
+ cassert ((not !group_has_builtin_info) || List.length d = 1) (List.hd d).meta "This builtin function belongs to a group of mutually recursive definitions";
(* We ignore on purpose functions that cannot fail and consider they *can*
* fail: the result of the analysis is not used yet to adjust the translation
* so that the functions which syntactically can't fail don't use an error monad.
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 0bbde79c..034304c7 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -211,7 +211,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
in
(* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
let call_id = fresh_fun_call_id () in
- cassert (call_id = FunCallId.zero) fdef.meta "The abstractions should be empty (i.e., with no avalues) abstractions";
+ sanity_check (call_id = FunCallId.zero) fdef.meta;
let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
eval_ctx * typed_avalue list =
(* Project over the values - we use *loan* projectors, as explained above *)
@@ -272,7 +272,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
^ "\n- inside_loop: "
^ Print.bool_to_string inside_loop
^ "\n- ctx:\n"
- ^ Print.Contexts.eval_ctx_to_string fdef.meta ctx));
+ ^ Print.Contexts.eval_ctx_to_string ~meta:(Some fdef.meta) ctx));
(* We need to instantiate the function signature - to retrieve
* the return type. Note that it is important to re-generate
* an instantiation of the signature, so that we use fresh
@@ -330,7 +330,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
let region_can_end rid =
RegionGroupId.Set.mem rid parent_and_current_rgs
in
- cassert (region_can_end back_id) fdef.meta "The region should be able to end";
+ sanity_check (region_can_end back_id) fdef.meta;
let ctx =
create_push_abstractions_from_abs_region_groups
(fun rg_id -> SynthRet rg_id)
@@ -417,9 +417,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
| Loop (loop_id', rg_id', LoopSynthInput) ->
(* We only allow to end the loop synth input abs for the region
group [rg_id] *)
- cassert (
+ sanity_check (
if Option.is_some loop_id then loop_id = Some loop_id'
- else true) fdef.meta "Only the loop synth input abs for the region group [rg_id] are allowed to end";
+ else true) fdef.meta;
(* Loop abstractions *)
let rg_id' = Option.get rg_id' in
if rg_id' = back_id && inside_loop then
@@ -427,7 +427,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
else abs
| Loop (loop_id', _, LoopCall) ->
(* We can end all the loop call abstractions *)
- cassert (loop_id = Some loop_id') fdef.meta "TODO: error message";
+ sanity_check (loop_id = Some loop_id') fdef.meta;
{ abs with can_end = true }
| SynthInput rg_id' ->
if rg_id' = back_id && end_fun_synth_input then
@@ -603,7 +603,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
(* Evaluate the function *)
let symbolic =
- eval_function_body config fdef.meta (Option.get fdef.body).body cf_finish ctx
+ eval_function_body config (Option.get fdef.body).body cf_finish ctx
in
(* Return *)
@@ -655,7 +655,7 @@ module Test = struct
in
(* Evaluate the function *)
- let _ = eval_function_body config body.meta body.body cf_check ctx in
+ let _ = eval_function_body config body.body cf_check ctx in
()
(** Small helper: return true if the function is a *transparent* unit function
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index ab2639ad..c1cf8441 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -42,7 +42,7 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt
in
let set_replaced_bc (abs_id : AbstractionId.id option) (bc : g_borrow_content)
=
- cassert (Option.is_none !replaced_bc) meta "TODO: error message";
+ sanity_check (Option.is_none !replaced_bc) meta;
replaced_bc := Some (abs_id, bc)
in
(* Raise an exception if:
@@ -224,8 +224,8 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt
method! visit_abs outer abs =
(* Update the outer abs *)
let outer_abs, outer_borrows = outer in
- cassert (Option.is_none outer_abs) meta "TODO: error message";
- cassert (Option.is_none outer_borrows) meta "TODO: error message";
+ sanity_check (Option.is_none outer_abs) meta;
+ sanity_check (Option.is_none outer_borrows) meta;
let outer = (Some abs.abs_id, None) in
super#visit_abs outer abs
end
@@ -248,18 +248,18 @@ let end_borrow_get_borrow (meta : Meta.meta) (allowed_abs : AbstractionId.id opt
let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv : typed_value)
(ctx : eval_ctx) : eval_ctx =
(* Sanity check *)
- sanity_check (not (loans_in_value nv)) meta;
- sanity_check (not (bottom_in_value ctx.ended_regions nv)) meta;
+ exec_assert (not (loans_in_value nv)) meta "Can not end a borrow because the value to give back contains bottom";
+ exec_assert (not (bottom_in_value ctx.ended_regions nv)) meta "Can not end a borrow because the value to give back contains bottom";
(* Debug *)
log#ldebug
(lazy
("give_back_value:\n- bid: " ^ BorrowId.to_string bid ^ "\n- value: "
- ^ typed_value_to_string meta ctx nv
- ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+ ^ typed_value_to_string ~meta:(Some meta) ctx nv
+ ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
(* We use a reference to check that we updated exactly one loan *)
let replaced : bool ref = ref false in
let set_replaced () =
- cassert (not !replaced) meta "Exactly one loan should have been updated";
+ sanity_check (not !replaced) meta;
replaced := true
in
(* Whenever giving back symbolic values, they shouldn't contain already ended regions *)
@@ -427,7 +427,7 @@ let give_back_value (config : config) (meta : Meta.meta) (bid : BorrowId.id) (nv
(* We remember in which abstraction we are before diving -
* this is necessary for projecting values: we need to know
* over which regions to project *)
- cassert (Option.is_none opt_abs) meta "TODO: error message";
+ sanity_check (Option.is_none opt_abs) meta;
super#visit_EAbs (Some abs) abs
end
in
@@ -466,7 +466,7 @@ let give_back_symbolic_value (_config : config) (meta : Meta.meta) (proj_regions
type [T]! We thus *mustn't* introduce a projector here.
*)
(* AProjBorrows (nsv, sv.sv_ty) *)
- craise meta "TODO: error message"
+ internal_error meta
in
AProjLoans (sv, (mv, child_proj) :: local_given_back)
in
@@ -671,7 +671,7 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : B
(* Keep track of changes *)
let r = ref false in
let set_ref () =
- cassert (not !r) meta "TODO: error message";
+ sanity_check (not !r) meta;
r := true
in
@@ -701,7 +701,7 @@ let reborrow_shared (meta : Meta.meta) (original_bid : BorrowId.id) (new_bid : B
let env = obj#visit_env () ctx.env in
(* Check that we reborrowed once *)
- cassert !r meta "Not reborrowed once";
+ sanity_check !r meta;
{ ctx with env }
(** Convert an {!type:avalue} to a {!type:value}.
@@ -746,11 +746,11 @@ let give_back (config : config) (meta : Meta.meta) (l : BorrowId.id) (bc : g_bor
(lazy
(let bc =
match bc with
- | Concrete bc -> borrow_content_to_string meta ctx bc
- | Abstract bc -> aborrow_content_to_string meta ctx bc
+ | Concrete bc -> borrow_content_to_string ~meta:(Some meta) ctx bc
+ | Abstract bc -> aborrow_content_to_string ~meta:(Some meta) ctx bc
in
"give_back:\n- bid: " ^ BorrowId.to_string l ^ "\n- content: " ^ bc
- ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+ ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
(* This is used for sanity checks *)
let sanity_ek =
{ enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true }
@@ -814,8 +814,8 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI
(lazy
(fun_name ^ ": " ^ BorrowId.to_string l
^ ": borrow didn't disappear:\n- original context:\n"
- ^ eval_ctx_to_string meta ctx0 ^ "\n\n- new context:\n"
- ^ eval_ctx_to_string meta ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n- new context:\n"
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx));
craise meta "Borrow not eliminated"
in
match lookup_loan_opt meta ek_all l ctx with
@@ -825,8 +825,8 @@ let check_borrow_disappeared (meta : Meta.meta) (fun_name : string) (l : BorrowI
(lazy
(fun_name ^ ": " ^ BorrowId.to_string l
^ ": loan didn't disappear:\n- original context:\n"
- ^ eval_ctx_to_string meta ctx0 ^ "\n\n- new context:\n"
- ^ eval_ctx_to_string meta ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n- new context:\n"
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx));
craise meta "Loan not eliminated"
in
unit_to_cm_fun check_disappeared
@@ -863,7 +863,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_a
log#ldebug
(lazy
("end borrow: " ^ BorrowId.to_string l ^ ":\n- original context:\n"
- ^ eval_ctx_to_string meta ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx));
(* Utility function for the sanity checks: check that the borrow disappeared
* from the context *)
@@ -922,7 +922,7 @@ let rec end_borrow_aux (config : config) (meta : Meta.meta) (chain : borrow_or_a
log#ldebug (lazy "End borrow: borrow not found");
(* It is possible that we can't find a borrow in symbolic mode (ending
* an abstraction may end several borrows at once *)
- cassert (config.mode = SymbolicMode) meta "Borrow should be in symbolic mode";
+ sanity_check (config.mode = SymbolicMode) meta;
(* Do a sanity check and continue *)
cf_check cf ctx
(* We found a borrow and replaced it with [Bottom]: give it back (i.e., update
@@ -966,7 +966,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
(lazy
("end_abstraction_aux: "
^ AbstractionId.to_string abs_id
- ^ "\n- original context:\n" ^ eval_ctx_to_string meta ctx0));
+ ^ "\n- original context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0));
(* Lookup the abstraction - note that if we end a list of abstractions,
ending one abstraction may lead to the current abstraction having
@@ -999,7 +999,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
("end_abstraction_aux: "
^ AbstractionId.to_string abs_id
^ "\n- context after parent abstractions ended:\n"
- ^ eval_ctx_to_string meta ctx)))
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx)))
in
(* End the loans inside the abstraction *)
@@ -1010,7 +1010,7 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
(lazy
("end_abstraction_aux: "
^ AbstractionId.to_string abs_id
- ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string meta ctx)))
+ ^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)))
in
(* End the abstraction itself by redistributing the borrows it contains *)
@@ -1039,8 +1039,8 @@ and end_abstraction_aux (config : config) (meta : Meta.meta) (chain : borrow_or_
(lazy
("end_abstraction_aux: "
^ AbstractionId.to_string abs_id
- ^ "\n- original context:\n" ^ eval_ctx_to_string meta ctx0
- ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx)))
+ ^ "\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)))
in
(* Sanity check: ending an abstraction must preserve the invariants *)
@@ -1173,7 +1173,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) (chain : borrow
log#ldebug
(lazy
("end_abstraction_borrows: found aborrow content: "
- ^ aborrow_content_to_string meta ctx bc));
+ ^ aborrow_content_to_string ~meta:(Some meta) ctx bc));
let ctx =
match bc with
| AMutBorrow (bid, av) ->
@@ -1243,7 +1243,7 @@ and end_abstraction_borrows (config : config) (meta : Meta.meta) (chain : borrow
log#ldebug
(lazy
("end_abstraction_borrows: found borrow content: "
- ^ borrow_content_to_string meta ctx bc));
+ ^ borrow_content_to_string ~meta:(Some meta) ctx bc));
let ctx =
match bc with
| VSharedBorrow bid -> (
@@ -1466,7 +1466,7 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
log#ldebug
(lazy
("promote_shared_loan_to_mut_loan:\n- loan: " ^ BorrowId.to_string l
- ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+ ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
(* Lookup the shared loan - note that we can't promote a shared loan
* in a shared value, but we can do it in a mutably borrowed value.
* This is important because we can do: [let y = &two-phase ( *x );]
@@ -1485,9 +1485,9 @@ let promote_shared_loan_to_mut_loan (meta : Meta.meta) (l : BorrowId.id)
to do a sanity check. *)
sanity_check (not (loans_in_value sv)) meta;
(* Check there isn't {!Bottom} (this is actually an invariant *)
- cassert (not (bottom_in_value ctx.ended_regions sv)) meta "There shouldn't be a !Bottom";
+ cassert (not (bottom_in_value ctx.ended_regions sv)) meta "There shouldn't be a bottom";
(* Check there aren't reserved borrows *)
- cassert (not (reserved_in_value sv)) meta "There shouldn't have reserved borrows";
+ cassert (not (reserved_in_value sv)) meta "There shouldn't be reserved borrows";
(* Update the loan content *)
let ctx = update_loan meta ek l (VMutLoan l) ctx in
(* Continue *)
@@ -1563,7 +1563,7 @@ let rec promote_reserved_mut_borrow (config : config) (meta : Meta.meta) (l : Bo
log#ldebug
(lazy
("activate_reserved_mut_borrow: resulting value:\n"
- ^ typed_value_to_string meta ctx sv));
+ ^ typed_value_to_string ~meta:(Some meta) ctx sv));
sanity_check (not (loans_in_value sv)) meta;
sanity_check (not (bottom_in_value ctx.ended_regions sv)) meta;
sanity_check (not (reserved_in_value sv)) meta;
@@ -1649,7 +1649,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
| AIgnoredMutLoan (opt_bid, child_av) ->
(* We don't support nested borrows for now *)
cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
- cassert (opt_bid = None) meta "TODO: error message";
+ sanity_check (opt_bid = None) meta;
(* Simply explore the child *)
list_avalues false push_fail child_av
| AEndedMutLoan
@@ -1680,7 +1680,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
| AIgnoredMutBorrow (opt_bid, child_av) ->
(* We don't support nested borrows for now *)
cassert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty)) meta "Nested borrows are not supported yet";
- cassert (opt_bid = None) meta "TODO: error message";
+ sanity_check (opt_bid = None) meta;
(* Just explore the child *)
list_avalues false push_fail child_av
| AEndedIgnoredMutBorrow
@@ -1703,7 +1703,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
| ASymbolic _ ->
(* For now, we fore all symbolic values containing borrows to be eagerly
expanded *)
- cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message"
+ sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta
and list_values (v : typed_value) : typed_avalue list * typed_value =
let ty = v.ty in
match v.value with
@@ -1725,9 +1725,9 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
let avl, sv = list_values sv in
if destructure_shared_values then (
(* Rem.: the shared value can't contain loans nor borrows *)
- cassert (ty_no_regions ty) meta "The shared value can't contain loans nor borrows";
+ cassert (ty_no_regions ty) meta "Nested borrows are not supported yet";
let av : typed_avalue =
- cassert (not (value_has_loans_or_borrows ctx sv.value)) meta "The shared value can't contain loans nor borrows";
+ sanity_check (not (value_has_loans_or_borrows ctx sv.value)) meta;
(* We introduce fresh ids for the symbolic values *)
let mk_value_with_fresh_sids (v : typed_value) : typed_value =
let visitor =
@@ -1752,7 +1752,7 @@ let destructure_abs (meta : Meta.meta) (abs_kind : abs_kind) (can_end : bool)
| VSymbolic _ ->
(* For now, we fore all symbolic values containing borrows to be eagerly
expanded *)
- cassert (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta "TODO: error message";
+ sanity_check (not (ty_has_borrows ctx.type_ctx.type_infos ty)) meta;
([], v)
in
@@ -1808,7 +1808,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
log#ldebug
(lazy
("convert_value_to_abstractions: to_avalues:\n- value: "
- ^ typed_value_to_string meta ctx v));
+ ^ typed_value_to_string ~meta:(Some meta) ctx v));
let ty = v.ty in
match v.value with
@@ -1852,13 +1852,13 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
(avl, { v with value = VAdt adt })
| VBorrow bc -> (
let _, ref_ty, kind = ty_as_ref ty in
- cassert (ty_no_regions ref_ty) meta "TODO: error message";
+ cassert (ty_no_regions ref_ty) meta "Nested borrows are not supported yet";
(* Sanity check *)
sanity_check allow_borrows meta;
(* Convert the borrow content *)
match bc with
| VSharedBorrow bid ->
- cassert (ty_no_regions ref_ty) meta "TODO: error message";
+ cassert (ty_no_regions ref_ty) meta "Nested borrows are not supported yet";
let ty = TRef (RFVar r_id, ref_ty, kind) in
let value = ABorrow (ASharedBorrow bid) in
([ { value; ty } ], v)
@@ -1887,7 +1887,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
cassert (not (value_has_borrows ctx sv.value)) meta "Nested borrows are not supported yet";
(* Push the avalue - note that we use [AIgnore] for the inner avalue *)
(* For avalues, a loan has the borrow type *)
- cassert (ty_no_regions ty) meta "TODO: error message";
+ cassert (ty_no_regions ty) meta "Nested borrows are not supported yet";
let ty = mk_ref_ty (RFVar r_id) ty RShared in
let ignored = mk_aignored meta ty in
(* Rem.: the shared value might contain loans *)
@@ -1905,7 +1905,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
| VMutLoan bid ->
(* Push the avalue - note that we use [AIgnore] for the inner avalue *)
(* For avalues, a loan has the borrow type *)
- cassert (ty_no_regions ty) meta "TODO: error message";
+ cassert (ty_no_regions ty) meta "Nested borrows are not supported yet";
let ty = mk_ref_ty (RFVar r_id) ty RMut in
let ignored = mk_aignored meta ty in
let av = ALoan (AMutLoan (bid, ignored)) in
@@ -1914,7 +1914,7 @@ let convert_value_to_abstractions (meta : Meta.meta) (abs_kind : abs_kind) (can_
| VSymbolic _ ->
(* For now, we force all the symbolic values containing borrows to
be eagerly expanded, and we don't support nested borrows *)
- cassert (not (value_has_borrows ctx v.value)) meta "TODO: error message";
+ cassert (not (value_has_borrows ctx v.value)) meta "Nested borrows are not supported yet";
(* Return nothing *)
([], v)
in
@@ -1968,26 +1968,26 @@ let compute_merge_abstraction_info (meta : Meta.meta) (ctx : eval_ctx) (abs : ab
in
let push_loans ids (lc : g_loan_content_with_ty) : unit =
- cassert (BorrowId.Set.disjoint !loans ids) meta "TODO: error message";
+ sanity_check (BorrowId.Set.disjoint !loans ids) meta;
loans := BorrowId.Set.union !loans ids;
BorrowId.Set.iter
(fun id ->
- cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message";
+ sanity_check (not (BorrowId.Map.mem id !loan_to_content)) meta;
loan_to_content := BorrowId.Map.add id lc !loan_to_content;
borrows_loans := LoanId id :: !borrows_loans)
ids
in
let push_loan id (lc : g_loan_content_with_ty) : unit =
- cassert (not (BorrowId.Set.mem id !loans)) meta "TODO: error message";
+ sanity_check (not (BorrowId.Set.mem id !loans)) meta;
loans := BorrowId.Set.add id !loans;
- cassert (not (BorrowId.Map.mem id !loan_to_content)) meta "TODO: error message";
+ sanity_check (not (BorrowId.Map.mem id !loan_to_content)) meta;
loan_to_content := BorrowId.Map.add id lc !loan_to_content;
borrows_loans := LoanId id :: !borrows_loans
in
let push_borrow id (bc : g_borrow_content_with_ty) : unit =
- cassert (not (BorrowId.Set.mem id !borrows)) meta "TODO: error message";
+ sanity_check (not (BorrowId.Set.mem id !borrows)) meta;
borrows := BorrowId.Set.add id !borrows;
- cassert (not (BorrowId.Map.mem id !borrow_to_content)) meta "TODO: error message";
+ sanity_check (not (BorrowId.Map.mem id !borrow_to_content)) meta;
borrow_to_content := BorrowId.Map.add id bc !borrow_to_content;
borrows_loans := BorrowId id :: !borrows_loans
in
@@ -2146,8 +2146,8 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
(* Check that the abstractions are destructured *)
if !Config.sanity_checks then (
let destructure_shared_values = true in
- cassert (abs_is_destructured meta destructure_shared_values ctx abs0) meta "Abstractions should be destructured";
- cassert (abs_is_destructured meta destructure_shared_values ctx abs1) meta "Abstractions should be destructured");
+ sanity_check (abs_is_destructured meta destructure_shared_values ctx abs0) meta;
+ sanity_check (abs_is_destructured meta destructure_shared_values ctx abs1) meta);
(* Compute the relevant information *)
let {
@@ -2201,7 +2201,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
log#ldebug
(lazy
("merge_into_abstraction_aux: push_avalue: "
- ^ typed_avalue_to_string meta ctx av));
+ ^ typed_avalue_to_string ~meta:(Some meta) ctx av));
avalues := av :: !avalues
in
let push_opt_avalue av =
@@ -2215,7 +2215,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
in
let filter_bids (bids : BorrowId.Set.t) : BorrowId.Set.t =
let bids = BorrowId.Set.diff bids intersect in
- cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message";
+ sanity_check (not (BorrowId.Set.is_empty bids)) meta;
bids
in
let filter_bid (bid : BorrowId.id) : BorrowId.id option =
@@ -2278,7 +2278,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
(* Check that the sets of ids are the same - if it is not the case, it
means we actually need to merge more than 2 avalues: we ignore this
case for now *)
- cassert (BorrowId.Set.equal ids0 ids1) meta "Ids are not the same - Case ignored for now";
+ sanity_check (BorrowId.Set.equal ids0 ids1) meta;
let ids = ids0 in
if BorrowId.Set.is_empty ids then (
(* If the set of ids is empty, we can eliminate this shared loan.
@@ -2290,10 +2290,10 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
to preserve (in practice it works because we destructure the
shared values in the abstractions, and forbid nested borrows).
*)
- cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message";
- cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message";
- cassert (is_aignored child0.value) meta "TODO: error message";
- cassert (is_aignored child1.value) meta "TODO: error message";
+ sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta;
+ sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta;
+ sanity_check (is_aignored child0.value) meta;
+ sanity_check (is_aignored child1.value) meta;
None)
else (
(* Register the loan ids *)
@@ -2365,7 +2365,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
craise meta "Unreachable"
| Abstract (ty, bc) -> { value = ABorrow bc; ty })
| Some bc0, Some bc1 ->
- cassert (merge_funs <> None) meta "TODO: error message";
+ sanity_check (merge_funs <> None) meta;
merge_g_borrow_contents bc0 bc1
| None, None -> craise meta "Unreachable"
in
@@ -2405,10 +2405,10 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
match lc with
| ASharedLoan (bids, sv, child) ->
let bids = filter_bids bids in
- cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message";
- cassert (is_aignored child.value) meta "TODO: error message";
- cassert (
- not (value_has_loans_or_borrows ctx sv.value)) meta "TODO: error message";
+ sanity_check (not (BorrowId.Set.is_empty bids)) meta;
+ sanity_check (is_aignored child.value) meta;
+ sanity_check (
+ not (value_has_loans_or_borrows ctx sv.value)) meta;
let lc = ASharedLoan (bids, sv, child) in
set_loans_as_merged bids;
Some { value = ALoan lc; ty }
@@ -2421,7 +2421,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
(* The abstraction has been destructured, so those shouldn't appear *)
craise meta "Unreachable"))
| Some lc0, Some lc1 ->
- cassert (merge_funs <> None) meta "TODO: error message";
+ sanity_check (merge_funs <> None) meta;
merge_g_loan_contents lc0 lc1
| None, None -> craise meta "Unreachable"
in
@@ -2476,7 +2476,7 @@ let merge_into_abstraction_aux (meta : Meta.meta) (abs_kind : abs_kind) (can_end
in
(* Sanity check *)
- if !Config.sanity_checks then sanity_check (abs_is_destructured meta true ctx abs) meta;
+ sanity_check (abs_is_destructured meta true ctx abs) meta;
(* Return *)
abs
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index d61e0bd1..1948c5a6 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -104,13 +104,13 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) (combine : bool -> bool
(* Normalize the associated types *)
match (ty1, ty2) with
| TLiteral lit1, TLiteral lit2 ->
- cassert (lit1 = lit2) meta "Tlitrals are not equal TODO: Error message";
+ sanity_check (lit1 = lit2) meta;
default
| TAdt (id1, generics1), TAdt (id2, generics2) ->
- cassert (id1 = id2) meta "ids are not equal TODO: Error message";
+ sanity_check (id1 = id2) meta;
(* There are no regions in the const generics, so we ignore them,
but we still check they are the same, for sanity *)
- cassert (generics1.const_generics = generics2.const_generics) meta "const generics are not the same";
+ sanity_check (generics1.const_generics = generics2.const_generics) meta;
(* We also ignore the trait refs *)
@@ -152,12 +152,12 @@ let rec compare_rtys (meta : Meta.meta) (default : bool) (combine : bool -> bool
let tys_b = compare ty1 ty2 in
combine regions_b tys_b
| TVar id1, TVar id2 ->
- cassert (id1 = id2) meta "Ids are not the same TODO: Error message";
+ sanity_check (id1 = id2) meta;
default
| TTraitType _, TTraitType _ ->
(* The types should have been normalized. If after normalization we
get trait types, we can consider them as variables *)
- cassert (ty1 = ty2) meta "The types are not normalized";
+ sanity_check (ty1 = ty2) meta;
default
| _ ->
log#lerror
@@ -269,7 +269,7 @@ let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
super#visit_aloan_content env lc
method! visit_EBinding env bv v =
- cassert (Option.is_none !abs_or_var) meta "TODO : error message ";
+ sanity_check (Option.is_none !abs_or_var) meta;
abs_or_var :=
Some
(match bv with
@@ -279,7 +279,7 @@ let lookup_loan_opt (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
abs_or_var := None
method! visit_EAbs env abs =
- cassert (Option.is_none !abs_or_var) meta "TODO : error message ";
+ sanity_check (Option.is_none !abs_or_var) meta;
if ek.enter_abs then (
abs_or_var := Some (AbsId abs.abs_id);
super#visit_EAbs env abs;
@@ -320,7 +320,7 @@ let update_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) (nl
* returning we check that we updated at least once. *)
let r = ref false in
let update () : loan_content =
- cassert (not !r) meta "TODO : error message ";
+ sanity_check (not !r) meta;
r := true;
nlc
in
@@ -367,7 +367,7 @@ let update_loan (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id) (nl
let ctx = obj#visit_eval_ctx () ctx in
(* Check that we updated at least one loan *)
- cassert !r meta "No loan was updated";
+ sanity_check !r meta;
ctx
(** Update a abstraction loan content.
@@ -383,7 +383,7 @@ let update_aloan (meta : Meta.meta ) (ek : exploration_kind) (l : BorrowId.id) (
* returning we check that we updated at least once. *)
let r = ref false in
let update () : aloan_content =
- cassert (not !r) meta "TODO : error message ";
+ sanity_check (not !r) meta;
r := true;
nlc
in
@@ -416,7 +416,7 @@ let update_aloan (meta : Meta.meta ) (ek : exploration_kind) (l : BorrowId.id) (
let ctx = obj#visit_eval_ctx () ctx in
(* Check that we updated at least one loan *)
- cassert !r meta "No loan was uodated";
+ sanity_check !r meta;
ctx
(** Lookup a borrow content from a borrow id. *)
@@ -501,7 +501,7 @@ let update_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
* returning we check that we updated at least once. *)
let r = ref false in
let update () : borrow_content =
- cassert (not !r) meta "TODO : error message ";
+ sanity_check (not !r) meta;
r := true;
nbc
in
@@ -542,7 +542,7 @@ let update_borrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
let ctx = obj#visit_eval_ctx () ctx in
(* Check that we updated at least one borrow *)
- cassert !r meta "No borrow was updated";
+ sanity_check !r meta;
ctx
(** Update an abstraction borrow content.
@@ -558,7 +558,7 @@ let update_aborrow (meta : Meta.meta) (ek : exploration_kind) (l : BorrowId.id)
* returning we check that we updated at least once. *)
let r = ref false in
let update () : avalue =
- cassert (not !r) meta "TODO: error message";
+ sanity_check (not !r) meta;
r := true;
nv
in
@@ -881,7 +881,7 @@ let update_intersecting_aproj_borrows_non_shared (meta : Meta.meta) (regions : R
update_non_shared regions sv ctx
in
(* Check that we updated at least once *)
- cassert !updated meta "Not updated at least once";
+ sanity_check !updated meta;
(* Return *)
ctx
@@ -936,7 +936,7 @@ let update_intersecting_aproj_loans (meta : Meta.meta) (proj_regions : RegionId.
(subst : abs -> (msymbolic_value * aproj) list -> aproj) (ctx : eval_ctx) :
eval_ctx =
(* *)
- cassert (ty_is_rty proj_ty) meta "proj_ty is not rty TODO: Error message";
+ sanity_check (ty_is_rty proj_ty) meta;
(* Small helpers for sanity checks *)
let updated = ref false in
let update abs local_given_back : aproj =
@@ -958,7 +958,7 @@ let update_intersecting_aproj_loans (meta : Meta.meta) (proj_regions : RegionId.
| AProjLoans (sv', given_back) ->
let abs = Option.get abs in
if same_symbolic_id sv sv' then (
- cassert (sv.sv_ty = sv'.sv_ty) meta "TODO : error message ";
+ sanity_check (sv.sv_ty = sv'.sv_ty) meta;
if
projections_intersect meta proj_ty proj_regions sv'.sv_ty abs.regions
then update abs given_back
@@ -969,7 +969,7 @@ let update_intersecting_aproj_loans (meta : Meta.meta) (proj_regions : RegionId.
(* Apply *)
let ctx = obj#visit_eval_ctx None ctx in
(* Check that we updated the context at least once *)
- cassert !updated meta "Context was not updated at least once";
+ sanity_check !updated meta;
(* Return *)
ctx
@@ -989,7 +989,7 @@ let lookup_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symb
let found = ref None in
let set_found x =
(* There is at most one projector which corresponds to the description *)
- cassert (Option.is_none !found) meta "More than one projecto corresponds to the description";
+ sanity_check (Option.is_none !found) meta;
found := Some x
in
(* The visitor *)
@@ -1007,9 +1007,9 @@ let lookup_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symb
super#visit_aproj abs sproj
| AProjLoans (sv', given_back) ->
let abs = Option.get abs in
- cassert (abs.abs_id = abs_id) meta "TODO : error message ";
+ sanity_check (abs.abs_id = abs_id) meta;
if sv'.sv_id = sv.sv_id then (
- cassert (sv' = sv) meta "TODO : error message ";
+ sanity_check (sv' = sv) meta;
set_found given_back)
else ());
super#visit_aproj abs sproj
@@ -1034,7 +1034,7 @@ let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symb
let found = ref false in
let update () =
(* We update at most once *)
- cassert (not !found) meta "Updated more than once";
+ sanity_check (not !found) meta;
found := true;
nproj
in
@@ -1053,9 +1053,9 @@ let update_aproj_loans (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : symb
super#visit_aproj abs sproj
| AProjLoans (sv', _) ->
let abs = Option.get abs in
- cassert (abs.abs_id = abs_id) meta "TODO : error message ";
+ sanity_check (abs.abs_id = abs_id) meta;
if sv'.sv_id = sv.sv_id then (
- cassert (sv' = sv) meta "TODO : error message ";
+ sanity_check (sv' = sv) meta;
update ())
else super#visit_aproj (Some abs) sproj
end
@@ -1083,7 +1083,7 @@ let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : sy
let found = ref false in
let update () =
(* We update at most once *)
- cassert (not !found) meta "Updated more than once";
+ sanity_check (not !found) meta;
found := true;
nproj
in
@@ -1102,9 +1102,9 @@ let update_aproj_borrows (meta : Meta.meta) (abs_id : AbstractionId.id) (sv : sy
super#visit_aproj abs sproj
| AProjBorrows (sv', _proj_ty) ->
let abs = Option.get abs in
- cassert (abs.abs_id = abs_id) meta "TODO : error message ";
+ sanity_check (abs.abs_id = abs_id) meta;
if sv'.sv_id = sv.sv_id then (
- cassert (sv' = sv) meta "TODO : error message ";
+ sanity_check (sv' = sv) meta;
update ())
else super#visit_aproj (Some abs) sproj
end
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 086c0786..a2550e88 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -66,7 +66,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.me
(** When visiting an abstraction, we remember the regions it owns to be
able to properly reduce projectors when expanding symbolic values *)
method! visit_abs current_abs abs =
- cassert (Option.is_none current_abs) meta "TODO: error message";
+ sanity_check (Option.is_none current_abs) meta;
let current_abs = Some abs in
super#visit_abs current_abs abs
@@ -78,7 +78,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.me
method! visit_aproj current_abs aproj =
(match aproj with
| AProjLoans (sv, _) | AProjBorrows (sv, _) ->
- cassert (not (same_symbolic_id sv original_sv)) meta "TODO: error message"
+ sanity_check (not (same_symbolic_id sv original_sv)) meta
| AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
super#visit_aproj current_abs aproj
@@ -98,7 +98,7 @@ let apply_symbolic_expansion_to_target_avalues (config : config) (meta : Meta.me
(* Check if this is the symbolic value we are looking for *)
if same_symbolic_id sv original_sv then (
(* There mustn't be any given back values *)
- cassert (given_back = []) meta "TODO: error message";
+ sanity_check (given_back = []) meta;
(* Apply the projector *)
let projected_value =
apply_proj_loans_on_symbolic_expansion meta proj_regions
@@ -168,7 +168,7 @@ let replace_symbolic_values (meta : Meta.meta) (at_most_once : bool) (original_s
(* Count *)
let replaced = ref false in
let replace () =
- if at_most_once then cassert (not !replaced) meta "TODO: error message";
+ if at_most_once then sanity_check (not !replaced) meta;
replaced := true;
nv
in
@@ -215,10 +215,10 @@ let compute_expanded_symbolic_non_assumed_adt_value (meta : Meta.meta) (expand_e
(* Lookup the definition and check if it is an enumeration with several
* variants *)
let def = ctx_lookup_type_decl ctx def_id in
- cassert (List.length generics.regions = List.length def.generics.regions) meta "TODO: error message";
+ sanity_check (List.length generics.regions = List.length def.generics.regions) meta;
(* Retrieve, for every variant, the list of its instantiated field types *)
let variants_fields_types =
- AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes ctx def
+ AssociatedTypes.type_decl_get_inst_norm_variants_fields_rtypes meta ctx def
generics
in
(* Check if there is strictly more than one variant *)
@@ -325,7 +325,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
else super#visit_VSymbolic env sv
method! visit_EAbs proj_regions abs =
- cassert (Option.is_none proj_regions) meta "TODO: error message";
+ sanity_check (Option.is_none proj_regions) meta;
let proj_regions = Some abs.regions in
super#visit_EAbs proj_regions abs
@@ -350,7 +350,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
method! visit_aproj proj_regions aproj =
(match aproj with
| AProjLoans (sv, _) | AProjBorrows (sv, _) ->
- cassert (not (same_symbolic_id sv original_sv)) meta "TODO: error message"
+ sanity_check (not (same_symbolic_id sv original_sv)) meta
| AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
super#visit_aproj proj_regions aproj
@@ -376,7 +376,7 @@ let expand_symbolic_value_shared_borrow (config : config) (meta : Meta.meta)
let ctx = obj#visit_eval_ctx None ctx in
(* Finally, replace the projectors on loans *)
let bids = !borrows in
- cassert (not (BorrowId.Set.is_empty bids)) meta "TODO: error message";
+ sanity_check (not (BorrowId.Set.is_empty bids)) meta;
let see = SeSharedRef (bids, shared_sv) in
let allow_reborrows = true in
let ctx =
@@ -394,9 +394,9 @@ let expand_symbolic_value_borrow (config : config) (meta : Meta.meta)
(original_sv : symbolic_value) (original_sv_place : SA.mplace option)
(region : region) (ref_ty : rty) (rkind : ref_kind) : cm_fun =
fun cf ctx ->
- cassert (region <> RErased) meta "TODO: error message";
+ sanity_check (region <> RErased) meta;
(* Check that we are allowed to expand the reference *)
- cassert (not (region_in_set region ctx.ended_regions)) meta "TODO: error message";
+ sanity_check (not (region_in_set region ctx.ended_regions)) meta;
(* Match on the reference kind *)
match rkind with
| RMut ->
@@ -446,7 +446,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met
(see_cf_l : (symbolic_expansion option * st_cm_fun) list)
(cf_after_join : st_m_fun) : m_fun =
fun ctx ->
- cassert (see_cf_l <> []) meta "TODO: error message";
+ sanity_check (see_cf_l <> []) meta;
(* Apply the symbolic expansion in the context and call the continuation *)
let resl =
List.map
@@ -464,8 +464,8 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met
(lazy
("apply_branching_symbolic_expansions_non_borrow: "
^ symbolic_value_to_string ctx0 sv
- ^ "\n\n- original context:\n" ^ eval_ctx_to_string meta ctx0
- ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+ ^ "\n\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 ^ "\n"));
(* Continuation *)
cf_br cf_after_join ctx)
see_cf_l
@@ -476,7 +476,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : config) (meta : Met
match resl with
| Some _ :: _ -> Some (List.map Option.get resl)
| None :: _ ->
- List.iter (fun res -> cassert (res = None) meta "TODO: error message") resl;
+ List.iter (fun res -> sanity_check (res = None) meta) resl;
None
| _ -> craise meta "Unreachable"
in
@@ -492,7 +492,7 @@ let expand_symbolic_bool (config : config) (meta : Meta.meta) (sv : symbolic_val
let original_sv = sv in
let original_sv_place = sv_place in
let rty = original_sv.sv_ty in
- cassert (rty = TLiteral TBool) meta "TODO: error message";
+ sanity_check (rty = TLiteral TBool) meta;
(* Expand the symbolic value to true or false and continue execution *)
let see_true = SeLiteral (VBool true) in
let see_false = SeLiteral (VBool false) in
@@ -554,8 +554,8 @@ let expand_symbolic_value_no_branching (config : config) (meta : Meta.meta) (sv
(lazy
("expand_symbolic_value_no_branching: "
^ symbolic_value_to_string ctx0 sv
- ^ "\n\n- original context:\n" ^ eval_ctx_to_string meta ctx0
- ^ "\n\n- new context:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+ ^ "\n\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 ^ "\n"));
(* Sanity check: the symbolic value has disappeared *)
sanity_check (not (symbolic_value_id_in_ctx original_sv.sv_id ctx)) meta)
in
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 3922a3ab..7045d886 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -101,8 +101,8 @@ let literal_to_typed_value (meta : Meta.meta) (ty : literal_type) (cv : literal)
| TChar, VChar v -> { value = VLiteral (VChar v); ty = TLiteral ty }
| TInteger int_ty, VScalar v ->
(* Check the type and the ranges *)
- cassert (int_ty = v.int_ty) meta "Wrong type TODO: error message";
- cassert (check_scalar_value_in_range v) meta "Wrong range TODO: error message";
+ sanity_check (int_ty = v.int_ty) meta;
+ sanity_check (check_scalar_value_in_range v) meta;
{ value = VLiteral (VScalar v); ty = TLiteral ty }
(* Remaining cases (invalid) *)
| _, _ -> craise meta "Improperly typed constant value"
@@ -123,8 +123,8 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
log#ldebug
(lazy
("copy_value: "
- ^ typed_value_to_string meta ctx v
- ^ "\n- context:\n" ^ eval_ctx_to_string meta ctx));
+ ^ typed_value_to_string ~meta:(Some meta) ctx v
+ ^ "\n- context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
(* Remark: at some point we rewrote this function to use iterators, but then
* we reverted the changes: the result was less clear actually. In particular,
* the fact that we have exhaustive matches below makes very obvious the cases
@@ -135,7 +135,7 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
(* Sanity check *)
(match v.ty with
| TAdt (TAssumed TBox, _) ->
- craise meta "Can't copy an assumed value other than Option"
+ exec_raise meta "Can't copy an assumed value other than Option"
| TAdt (TAdtId _, _) as ty ->
sanity_check (allow_adt_copy || ty_is_primitively_copyable ty) meta
| TAdt (TTuple, _) -> () (* Ok *)
@@ -147,15 +147,15 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
const_generics = [];
trait_refs = [];
} ) ->
- sanity_check (ty_is_primitively_copyable ty) meta
- | _ -> craise meta "Unreachable");
+ exec_assert (ty_is_primitively_copyable ty) meta "The type is not primitively copyable"
+ | _ -> exec_raise meta "Unreachable");
let ctx, fields =
List.fold_left_map
(copy_value meta allow_adt_copy config)
ctx av.field_values
in
(ctx, { v with value = VAdt { av with field_values = fields } })
- | VBottom -> craise meta "Can't copy ⊥"
+ | VBottom -> exec_raise meta "Can't copy ⊥"
| VBorrow bc -> (
(* We can only copy shared borrows *)
match bc with
@@ -165,13 +165,13 @@ let rec copy_value (meta : Meta.meta) (allow_adt_copy : bool) (config : config)
let bid' = fresh_borrow_id () in
let ctx = InterpreterBorrows.reborrow_shared meta bid bid' ctx in
(ctx, { v with value = VBorrow (VSharedBorrow bid') })
- | VMutBorrow (_, _) -> craise meta "Can't copy a mutable borrow"
+ | VMutBorrow (_, _) -> exec_raise meta "Can't copy a mutable borrow"
| VReservedMutBorrow _ ->
- craise meta "Can't copy a reserved mut borrow")
+ exec_raise meta "Can't copy a reserved mut borrow")
| VLoan lc -> (
(* We can only copy shared loans *)
match lc with
- | VMutLoan _ -> craise meta "Can't copy a mutable loan"
+ | VMutLoan _ -> exec_raise meta "Can't copy a mutable loan"
| VSharedLoan (_, sv) ->
(* We don't copy the shared loan: only the shared value inside *)
copy_value meta allow_adt_copy config ctx sv)
@@ -256,7 +256,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
log#ldebug
(lazy
("eval_operand_no_reorganize: op: " ^ operand_to_string ctx op
- ^ "\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n"));
+ ^ "\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
(* Evaluate *)
match op with
| Constant cv -> (
@@ -305,14 +305,14 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
let e = cf cv ctx in
(* If we are synthesizing a symbolic AST, it means that we are in symbolic
mode: the value of the const generic is necessarily symbolic. *)
- cassert (e = None || is_symbolic cv.value) meta "The value of the const generic should be symbolic";
+ sanity_check (e = None || is_symbolic cv.value) meta;
(* We have to wrap the generated expression *)
match e with
| None -> None
| Some e ->
(* If we are synthesizing a symbolic AST, it means that we are in symbolic
mode: the value of the const generic is necessarily symbolic. *)
- cassert (is_symbolic cv.value) meta "The value of the const generic should be symbolic";
+ sanity_check (is_symbolic cv.value) meta;
(* *)
Some
(SymbolicAst.IntroSymbolic
@@ -321,7 +321,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
value_as_symbolic meta cv.value,
SymbolicAst.VaCgValue vid,
e )))
- | CFnPtr _ -> craise meta "TODO")
+ | CFnPtr _ -> craise meta "TODO: error message")
| Copy p ->
(* Access the value *)
let access = Read in
@@ -330,7 +330,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
let copy cf v : m_fun =
fun ctx ->
(* Sanity checks *)
- sanity_check (not (bottom_in_value ctx.ended_regions v)) meta;
+ exec_assert (not (bottom_in_value ctx.ended_regions v)) meta "Can not copy a value containing bottom";
sanity_check (
Option.is_none
(find_first_primitively_copyable_sv_with_borrows
@@ -351,7 +351,7 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) (op : operan
let move cf v : m_fun =
fun ctx ->
(* Check that there are no bottoms in the value we are about to move *)
- cassert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value we are about to move";
+ exec_assert (not (bottom_in_value ctx.ended_regions v)) meta "There should be no bottoms in the value we are about to move";
let bottom : typed_value = { value = VBottom; ty = v.ty } in
let ctx = write_place meta access p bottom ctx in
cf v ctx
@@ -366,7 +366,7 @@ let eval_operand (config : config) (meta : Meta.meta) (op : operand) (cf : typed
log#ldebug
(lazy
("eval_operand: op: " ^ operand_to_string ctx op ^ "\n- ctx:\n"
- ^ eval_ctx_to_string meta ctx ^ "\n"));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n"));
(* We reorganize the context, then evaluate the operand *)
comp
(prepare_eval_operand_reorganize config meta op)
@@ -421,7 +421,7 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) (o
| ( Cast (CastScalar (TInteger src_ty, TInteger tgt_ty)),
VLiteral (VScalar sv) ) -> (
(* Cast between integers *)
- cassert (src_ty = sv.int_ty) meta "TODO: error message";
+ sanity_check (src_ty = sv.int_ty) meta;
let i = sv.value in
match mk_scalar tgt_ty i with
| Error _ -> cf (Error EPanic)
@@ -443,12 +443,12 @@ let eval_unary_op_concrete (config : config) (meta : Meta.meta) (unop : unop) (o
let b =
if Z.of_int 0 = sv.value then false
else if Z.of_int 1 = sv.value then true
- else craise meta "Conversion from int to bool: out of range"
+ else exec_raise meta "Conversion from int to bool: out of range"
in
let value = VLiteral (VBool b) in
let ty = TLiteral TBool in
cf (Ok { ty; value })
- | _ -> craise meta "Invalid input for unop"
+ | _ -> exec_raise meta "Invalid input for unop"
in
comp eval_op apply cf
@@ -466,7 +466,7 @@ let eval_unary_op_symbolic (config : config) (meta : Meta.meta) (unop : unop) (o
| Not, (TLiteral TBool as lty) -> lty
| Neg, (TLiteral (TInteger _) as lty) -> lty
| Cast (CastScalar (_, tgt_ty)), _ -> TLiteral tgt_ty
- | _ -> craise meta "Invalid input for unop"
+ | _ -> exec_raise meta "Invalid input for unop"
in
let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
(* Call the continuation *)
@@ -494,9 +494,9 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ
* The remaining binops only operate on scalars. *)
if binop = Eq || binop = Ne then (
(* Equality operations *)
- cassert (v1.ty = v2.ty) meta "TODO: error message";
+ exec_assert (v1.ty = v2.ty) meta "TODO: error message";
(* Equality/inequality check is primitive only for a subset of types *)
- cassert (ty_is_primitively_copyable v1.ty) meta "Not primitively copyable TODO: error message";
+ exec_assert (ty_is_primitively_copyable v1.ty) meta "Type is not primitively copyable";
let b = v1 = v2 in
Ok { value = VLiteral (VBool b); ty = TLiteral TBool })
else
@@ -511,7 +511,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ
match binop with
| Lt | Le | Ge | Gt ->
(* The two operands must have the same type and the result is a boolean *)
- cassert (sv1.int_ty = sv2.int_ty) meta "The two operands must have the same type and the result is a boolean";
+ sanity_check (sv1.int_ty = sv2.int_ty) meta;
let b =
match binop with
| Lt -> Z.lt sv1.value sv2.value
@@ -527,7 +527,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) (v1 : typ
: typed_value)
| Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> (
(* The two operands must have the same type and the result is an integer *)
- cassert (sv1.int_ty = sv2.int_ty) meta "The two operands must have the same type and the result is an integer";
+ sanity_check (sv1.int_ty = sv2.int_ty) meta;
let res =
match binop with
| Div ->
@@ -583,9 +583,9 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
let res_sv_ty =
if binop = Eq || binop = Ne then (
(* Equality operations *)
- cassert (v1.ty = v2.ty) meta "TODO: error message";
+ sanity_check (v1.ty = v2.ty) meta;
(* Equality/inequality check is primitive only for a subset of types *)
- cassert (ty_is_primitively_copyable v1.ty) meta "Not primitively copyable TODO: error message";
+ exec_assert (ty_is_primitively_copyable v1.ty) meta "The type is not primitively copyable";
TLiteral TBool)
else
(* Other operations: input types are integers *)
@@ -593,10 +593,10 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
| TLiteral (TInteger int_ty1), TLiteral (TInteger int_ty2) -> (
match binop with
| Lt | Le | Ge | Gt ->
- cassert (int_ty1 = int_ty2) meta "TODO: error message";
+ sanity_check (int_ty1 = int_ty2) meta;
TLiteral TBool
| Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr ->
- cassert (int_ty1 = int_ty2) meta "TODO: error message";
+ sanity_check (int_ty1 = int_ty2) meta;
TLiteral (TInteger int_ty1)
| Shl | Shr ->
(* The number of bits can be of a different integer type
@@ -632,7 +632,7 @@ let eval_rvalue_ref (config : config) (meta : Meta.meta) (p : place) (bkind : bo
In practice this restricted the behaviour too much, so for now we
forbid them.
*)
- cassert (bkind <> BShallow) meta "Shallow borrow are currently forbidden";
+ sanity_check (bkind <> BShallow) meta;
(* Access the value *)
let access =
@@ -744,9 +744,9 @@ let eval_rvalue_aggregate (config : config) (meta : Meta.meta) (aggregate_kind :
AssociatedTypes.ctx_adt_get_inst_norm_field_etypes meta ctx def_id
opt_variant_id generics
in
- cassert (
+ sanity_check (
expected_field_types
- = List.map (fun (v : typed_value) -> v.ty) values) meta "TODO: error message";
+ = List.map (fun (v : typed_value) -> v.ty) values) meta;
(* Construct the value *)
let av : adt_value =
{ variant_id = opt_variant_id; field_values = values }
@@ -815,7 +815,7 @@ let eval_fake_read (config : config) (meta : Meta.meta) (p : place) : cm_fun =
in
let cf_continue cf v : m_fun =
fun ctx ->
- cassert (not (bottom_in_value ctx.ended_regions v)) meta "TODO: error message";
+ cassert (not (bottom_in_value ctx.ended_regions v)) meta "Fake read: the value contains bottom";
cf ctx
in
comp cf_prepare cf_continue cf ctx
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 4d4b709e..d2f1b5fb 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -68,7 +68,7 @@ let eval_loop_symbolic (config : config) (meta : meta)
fun cf ctx ->
(* Debug *)
log#ldebug
- (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n"));
+ (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n"));
(* Generate a fresh loop id *)
let loop_id = fresh_loop_id () in
@@ -81,8 +81,8 @@ let eval_loop_symbolic (config : config) (meta : meta)
(* Debug *)
log#ldebug
(lazy
- ("eval_loop_symbolic:\nInitial context:\n" ^ eval_ctx_to_string meta ctx
- ^ "\n\nFixed point:\n" ^ eval_ctx_to_string meta fp_ctx));
+ ("eval_loop_symbolic:\nInitial context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx
+ ^ "\n\nFixed point:\n" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx));
(* Compute the loop input parameters *)
let fresh_sids, input_svalues = compute_fp_ctx_symbolic_values meta ctx fp_ctx in
@@ -122,8 +122,8 @@ let eval_loop_symbolic (config : config) (meta : meta)
(lazy
("eval_loop_symbolic: about to match the fixed-point context with the \
original context:\n\
- - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx
- ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string meta ctx));
+ - src ctx (fixed-point ctx)" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx
+ ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
let end_expr : SymbolicAst.expression option =
match_ctx_with_target config meta loop_id true fp_bl_corresp fp_input_svalues
fixed_ids fp_ctx cf ctx
@@ -155,8 +155,8 @@ let eval_loop_symbolic (config : config) (meta : meta)
(lazy
("eval_loop_symbolic: about to match the fixed-point context \
with the context at a continue:\n\
- - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx
- ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string meta ctx));
+ - src ctx (fixed-point ctx)" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx
+ ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
let cc =
match_ctx_with_target config meta loop_id false fp_bl_corresp
fp_input_svalues fixed_ids fp_ctx
@@ -173,9 +173,9 @@ let eval_loop_symbolic (config : config) (meta : meta)
log#ldebug
(lazy
("eval_loop_symbolic: result:" ^ "\n- src context:\n"
- ^ eval_ctx_to_string_no_filter meta ctx
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx
^ "\n- fixed point:\n"
- ^ eval_ctx_to_string_no_filter meta fp_ctx
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_ctx
^ "\n- fixed_sids: "
^ SymbolicValueId.Set.show fixed_ids.sids
^ "\n- fresh_sids: "
@@ -209,7 +209,7 @@ let eval_loop_symbolic (config : config) (meta : meta)
(fun (av : typed_avalue) ->
match av.value with
| ABorrow (AMutBorrow (bid, child_av)) ->
- cassert (is_aignored child_av.value) meta "TODO: error message";
+ sanity_check (is_aignored child_av.value) meta;
Some (bid, child_av.ty)
| ABorrow (ASharedBorrow _) -> None
| _ -> craise meta "Unreachable")
@@ -222,7 +222,7 @@ let eval_loop_symbolic (config : config) (meta : meta)
(fun (av : typed_avalue) ->
match av.value with
| ALoan (AMutLoan (bid, child_av)) ->
- cassert (is_aignored child_av.value) meta "TODO: error message";
+ sanity_check (is_aignored child_av.value) meta;
Some bid
| ALoan (ASharedLoan _) -> None
| _ -> craise meta "Unreachable")
@@ -241,7 +241,7 @@ let eval_loop_symbolic (config : config) (meta : meta)
ty)
loan_ids
in
- cassert (BorrowId.Map.is_empty !borrows) meta "TODO: error message";
+ sanity_check (BorrowId.Map.is_empty !borrows) meta;
given_back_tys
in
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index 6ef4a13b..2de5aed0 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -53,16 +53,17 @@ type abs_borrows_loans_maps = {
regions.
*)
module type PrimMatcher = sig
- val match_etys : Meta.meta -> eval_ctx -> eval_ctx -> ety -> ety -> ety
- val match_rtys : Meta.meta -> eval_ctx -> eval_ctx -> rty -> rty -> rty
+ val meta : Meta.meta
+ val match_etys : eval_ctx -> eval_ctx -> ety -> ety -> ety
+ val match_rtys : eval_ctx -> eval_ctx -> rty -> rty -> rty
(** The input primitive values are not equal *)
val match_distinct_literals :
- Meta.meta -> eval_ctx -> eval_ctx -> ety -> literal -> literal -> typed_value
+ eval_ctx -> eval_ctx -> ety -> literal -> literal -> typed_value
(** The input ADTs don't have the same variant *)
val match_distinct_adts :
- Meta.meta -> eval_ctx -> eval_ctx -> ety -> adt_value -> adt_value -> typed_value
+ eval_ctx -> eval_ctx -> ety -> adt_value -> adt_value -> typed_value
(** The meta-value is the result of a match.
@@ -75,7 +76,6 @@ module type PrimMatcher = sig
calling the match function.
*)
val match_shared_borrows :
- Meta.meta ->
eval_ctx ->
eval_ctx ->
(typed_value -> typed_value -> typed_value) ->
@@ -93,7 +93,6 @@ module type PrimMatcher = sig
- [bv]: the result of matching [bv0] with [bv1]
*)
val match_mut_borrows :
- Meta.meta ->
eval_ctx ->
eval_ctx ->
ety ->
@@ -111,7 +110,6 @@ module type PrimMatcher = sig
[v]: the result of matching the shared values coming from the two loans
*)
val match_shared_loans :
- Meta.meta ->
eval_ctx ->
eval_ctx ->
ety ->
@@ -125,7 +123,7 @@ module type PrimMatcher = sig
(** There are no constraints on the input symbolic values *)
val match_symbolic_values :
- Meta.meta -> eval_ctx -> eval_ctx -> symbolic_value -> symbolic_value -> symbolic_value
+ eval_ctx -> eval_ctx -> symbolic_value -> symbolic_value -> symbolic_value
(** Match a symbolic value with a value which is not symbolic.
@@ -135,7 +133,7 @@ module type PrimMatcher = sig
end loans in one of the two environments).
*)
val match_symbolic_with_other :
- Meta.meta -> eval_ctx -> eval_ctx -> bool -> symbolic_value -> typed_value -> typed_value
+ eval_ctx -> eval_ctx -> bool -> symbolic_value -> typed_value -> typed_value
(** Match a bottom value with a value which is not bottom.
@@ -145,11 +143,10 @@ module type PrimMatcher = sig
end loans in one of the two environments).
*)
val match_bottom_with_other :
- Meta.meta -> eval_ctx -> eval_ctx -> bool -> typed_value -> typed_value
+ eval_ctx -> eval_ctx -> bool -> typed_value -> typed_value
(** The input ADTs don't have the same variant *)
val match_distinct_aadts :
- Meta.meta ->
eval_ctx ->
eval_ctx ->
rty ->
@@ -167,7 +164,6 @@ module type PrimMatcher = sig
[ty]: result of matching ty0 and ty1
*)
val match_ashared_borrows :
- Meta.meta ->
eval_ctx ->
eval_ctx ->
rty ->
@@ -188,7 +184,6 @@ module type PrimMatcher = sig
[av]: result of matching av0 and av1
*)
val match_amut_borrows :
- Meta.meta ->
eval_ctx ->
eval_ctx ->
rty ->
@@ -215,7 +210,6 @@ module type PrimMatcher = sig
[av]: result of matching av0 and av1
*)
val match_ashared_loans :
- Meta.meta ->
eval_ctx ->
eval_ctx ->
rty ->
@@ -242,7 +236,6 @@ module type PrimMatcher = sig
[av]: result of matching av0 and av1
*)
val match_amut_loans :
- Meta.meta ->
eval_ctx ->
eval_ctx ->
rty ->
@@ -259,7 +252,7 @@ module type PrimMatcher = sig
is typically used to raise the proper exception).
*)
val match_avalues :
- Meta.meta -> eval_ctx -> eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue
+ eval_ctx -> eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue
end
module type Matcher = sig
@@ -267,15 +260,16 @@ module type Matcher = sig
Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}.
*)
+ val meta : Meta.meta
val match_typed_values :
- Meta.meta -> eval_ctx -> eval_ctx -> typed_value -> typed_value -> typed_value
+ eval_ctx -> eval_ctx -> typed_value -> typed_value -> typed_value
(** Match two avalues.
Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}.
*)
val match_typed_avalues :
- Meta.meta -> eval_ctx -> eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue
+ eval_ctx -> eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue
end
(** See {!module:InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and
@@ -304,6 +298,7 @@ module type MatchCheckEquivState = sig
val aid_map : AbstractionId.InjSubst.t ref
val lookup_shared_value_in_ctx0 : BorrowId.id -> typed_value
val lookup_shared_value_in_ctx1 : BorrowId.id -> typed_value
+ val meta : Meta.meta
end
module type CheckEquivMatcher = sig
@@ -353,6 +348,7 @@ module type MatchJoinState = sig
(** The abstractions introduced when performing the matches *)
val nabs : abs list ref
+ val meta : Meta.meta
end
(** Split an environment between the fixed abstractions, values, etc. and
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index 44b9a44e..f6ce9b32 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -272,7 +272,7 @@ let prepare_ashared_loans (meta : Meta.meta) (loop_id : LoopId.id option) : cm_f
sanity_check (RegionId.Set.is_empty abs.ancestors_regions) meta;
(* Introduce the new abstraction for the shared values *)
- cassert (ty_no_regions sv.ty) meta "TODO : error message ";
+ cassert (ty_no_regions sv.ty) meta "Nested borrows are not supported yet";
let rty = sv.ty in
(* Create the shared loan child *)
@@ -461,9 +461,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
(lazy
("compute_loop_entry_fixed_point: after prepare_ashared_loans:"
^ "\n\n- ctx0:\n"
- ^ eval_ctx_to_string_no_filter meta ctx0
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx0
^ "\n\n- ctx1:\n"
- ^ eval_ctx_to_string_no_filter meta ctx
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx
^ "\n\n"));
let cf_exit_loop_body (res : statement_eval_res) : m_fun =
@@ -597,9 +597,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
log#ldebug
(lazy
("compute_fixed_point:" ^ "\n\n- ctx0:\n"
- ^ eval_ctx_to_string_no_filter meta ctx
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx
^ "\n\n- ctx1:\n"
- ^ eval_ctx_to_string_no_filter meta ctx1
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx1
^ "\n\n"));
(* Check if we reached a fixed point: if not, iterate *)
@@ -612,7 +612,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
(lazy
("compute_fixed_point: fixed point computed before matching with input \
region groups:" ^ "\n\n- fp:\n"
- ^ eval_ctx_to_string_no_filter meta fp
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp
^ "\n\n"));
(* Make sure we have exactly one loop abstraction per function region (merge
@@ -634,10 +634,10 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
method! visit_abs _ abs =
match abs.kind with
| Loop (loop_id', _, kind) ->
- cassert (loop_id' = loop_id) meta "TODO : error message ";
- cassert (kind = LoopSynthInput) meta "TODO : error message ";
+ sanity_check (loop_id' = loop_id) meta;
+ sanity_check (kind = LoopSynthInput) meta;
(* The abstractions introduced so far should be endable *)
- cassert (abs.can_end = true) meta "The abstractions introduced so far can not end";
+ sanity_check (abs.can_end = true) meta;
add_aid abs.abs_id;
abs
| _ -> abs
@@ -694,9 +694,9 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
in
(* By default, the [SynthInput] abs can't end *)
let ctx = ctx_set_abs_can_end meta ctx abs_id true in
- cassert (
+ sanity_check (
let abs = ctx_lookup_abs ctx abs_id in
- abs.kind = SynthInput rg_id) meta "TODO : error message ";
+ abs.kind = SynthInput rg_id) meta;
(* End this abstraction *)
let ctx =
InterpreterBorrows.end_abstraction_no_synth config meta abs_id ctx
@@ -725,7 +725,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
(* We also check that all the regions need to end - this is not necessary per
se, but if it doesn't happen it is bizarre and worth investigating... *)
- cassert (AbstractionId.Set.equal !aids_union !fp_aids) meta "Not all regions need to end TODO: Error message";
+ sanity_check (AbstractionId.Set.equal !aids_union !fp_aids) meta;
(* Merge the abstractions which need to be merged, and compute the map from
region id to abstraction id *)
@@ -815,8 +815,8 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
method! visit_abs _ abs =
match abs.kind with
| Loop (loop_id', _, kind) ->
- cassert (loop_id' = loop_id) meta "TODO : error message ";
- cassert (kind = LoopSynthInput) meta "TODO : error message ";
+ sanity_check (loop_id' = loop_id) meta;
+ sanity_check (kind = LoopSynthInput) meta;
let kind : abs_kind =
if remove_rg_id then Loop (loop_id, None, LoopSynthInput)
else abs.kind
@@ -838,7 +838,7 @@ let compute_loop_entry_fixed_point (config : config) (meta : Meta.meta) (loop_id
(lazy
("compute_fixed_point: fixed point after matching with the function \
region groups:\n"
- ^ eval_ctx_to_string_no_filter meta fp_test));
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_test));
compute_fixed_point fp_test 1 1
in
@@ -855,8 +855,8 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se
log#ldebug
(lazy
("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n"
- ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n" ^ eval_ctx_to_string meta src_ctx
- ^ "\n\n- tgt_ctx:\n" ^ eval_ctx_to_string meta tgt_ctx ^ "\n\n"));
+ ^ show_ids_sets fixed_ids ^ "\n\n- src_ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) src_ctx
+ ^ "\n\n- tgt_ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx ^ "\n\n"));
let filt_src_env, _, _ = ctx_split_fixed_new meta fixed_ids src_ctx in
let filt_src_ctx = { src_ctx with env = filt_src_env } in
@@ -867,9 +867,9 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se
(lazy
("compute_fixed_point_id_correspondance:\n\n- fixed_ids:\n"
^ show_ids_sets fixed_ids ^ "\n\n- filt_src_ctx:\n"
- ^ eval_ctx_to_string meta filt_src_ctx
+ ^ eval_ctx_to_string ~meta:(Some meta) filt_src_ctx
^ "\n\n- filt_tgt_ctx:\n"
- ^ eval_ctx_to_string meta filt_tgt_ctx
+ ^ eval_ctx_to_string ~meta:(Some meta) filt_tgt_ctx
^ "\n\n"));
(* Match the source context and the filtered target context *)
@@ -941,7 +941,7 @@ let compute_fixed_point_id_correspondance (meta : Meta.meta) (fixed_ids : ids_se
ids.loan_ids
in
(* Check that the loan and borrows are related *)
- cassert (BorrowId.Set.equal ids.borrow_ids loan_ids) meta "The loan and borrows are not related")
+ sanity_check (BorrowId.Set.equal ids.borrow_ids loan_ids) meta)
new_absl;
(* For every target abstraction (going back to the [list_nth_mut] example,
@@ -1089,9 +1089,9 @@ let compute_fp_ctx_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) (fp_ctx :
log#ldebug
(lazy
("compute_fp_ctx_symbolic_values:" ^ "\n- src context:\n"
- ^ eval_ctx_to_string_no_filter meta ctx
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx
^ "\n- fixed point:\n"
- ^ eval_ctx_to_string_no_filter meta fp_ctx
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_ctx
^ "\n- fresh_sids: "
^ SymbolicValueId.Set.show fresh_sids
^ "\n- input_svalues: "
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 74d31975..8153ef08 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -136,7 +136,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
log#ldebug
(lazy
("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
- ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string meta ctx0 ^ "\n\n"));
+ ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx0 ^ "\n\n"));
let abs_kind : abs_kind = Loop (loop_id, None, LoopSynthInput) in
let can_end = true in
@@ -171,13 +171,13 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
log#ldebug
(lazy
("collapse_ctx: after converting values to abstractions:\n"
- ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n"
+ ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n"
));
log#ldebug
(lazy
("collapse_ctx: after decomposing the shared values in the abstractions:\n"
- ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n"
+ ^ show_ids_sets old_ids ^ "\n\n- ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n"
));
(* Explore all the *new* abstractions, and compute various maps *)
@@ -252,7 +252,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
^ AbstractionId.to_string abs_id1
^ " into "
^ AbstractionId.to_string abs_id0
- ^ ":\n\n" ^ eval_ctx_to_string meta !ctx));
+ ^ ":\n\n" ^ eval_ctx_to_string ~meta:(Some meta) !ctx));
(* Update the environment - pay attention to the order: we
we merge [abs_id1] *into* [abs_id0] *)
@@ -272,7 +272,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
log#ldebug
(lazy
("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
- ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string meta !ctx ^ "\n\n"));
+ ^ "\n\n- after collapse:\n" ^ eval_ctx_to_string ~meta:(Some meta) !ctx ^ "\n\n"));
(* Reorder the loans and borrows in the fresh abstractions *)
let ctx = reorder_loans_borrows_in_fresh_abs meta old_ids.aids !ctx in
@@ -281,7 +281,7 @@ let collapse_ctx (meta : Meta.meta) (loop_id : LoopId.id)
(lazy
("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
^ "\n\n- after collapse and reorder borrows/loans:\n"
- ^ eval_ctx_to_string meta ctx ^ "\n\n"));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n"));
(* Return the new context *)
ctx
@@ -290,6 +290,7 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
: merge_duplicates_funcs =
(* Rem.: the merge functions raise exceptions (that we catch). *)
let module S : MatchJoinState = struct
+ let meta = meta
let loop_id = loop_id
let nabs = ref []
end in
@@ -356,11 +357,11 @@ let mk_collapse_ctx_merge_duplicate_funs (meta : Meta.meta) (loop_id : LoopId.id
This time we need to also merge the shared values. We rely on the
join matcher [JM] to do so.
*)
- cassert (not (value_has_loans_or_borrows ctx sv0.value)) meta "TODO: error message";
- cassert (not (value_has_loans_or_borrows ctx sv1.value)) meta "TODO: error message";
+ sanity_check (not (value_has_loans_or_borrows ctx sv0.value)) meta;
+ sanity_check (not (value_has_loans_or_borrows ctx sv1.value)) meta;
let ty = ty0 in
let child = child0 in
- let sv = M.match_typed_values meta ctx ctx sv0 sv1 in
+ let sv = M.match_typed_values ctx ctx sv0 sv1 in
let value = ALoan (ASharedLoan (ids, sv, child)) in
{ value; ty }
in
@@ -397,9 +398,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
(lazy
("join_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids
^ "\n\n- ctx0:\n"
- ^ eval_ctx_to_string_no_filter meta ctx0
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx0
^ "\n\n- ctx1:\n"
- ^ eval_ctx_to_string_no_filter meta ctx1
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx1
^ "\n\n"));
let env0 = List.rev ctx0.env in
@@ -413,9 +414,9 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
(lazy
("join_suffixes:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids
^ "\n\n- ctx0:\n"
- ^ eval_ctx_to_string_no_filter meta { ctx0 with env = List.rev env0 }
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx0 with env = List.rev env0 }
^ "\n\n- ctx1:\n"
- ^ eval_ctx_to_string_no_filter meta { ctx1 with env = List.rev env1 }
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx1 with env = List.rev env1 }
^ "\n\n"));
(* Sanity check: there are no values/abstractions which should be in the prefix *)
@@ -441,6 +442,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
in
let module S : MatchJoinState = struct
+ let meta = meta
let loop_id = loop_id
let nabs = nabs
end in
@@ -468,7 +470,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
(* Still in the prefix: match the values *)
cassert (b0 = b1) meta "Bindings are not the same. We are not in the prefix anymore";
let b = b0 in
- let v = M.match_typed_values meta ctx0 ctx1 v0 v1 in
+ let v = M.match_typed_values ctx0 ctx1 v0 v1 in
let var = EBinding (BDummy b, v) in
(* Continue *)
var :: join_prefixes env0' env1')
@@ -492,7 +494,7 @@ let join_ctxs (meta : Meta.meta) (loop_id : LoopId.id) (fixed_ids : ids_sets) (c
ids must be the same";
(* Match the values *)
let b = b0 in
- let v = M.match_typed_values meta ctx0 ctx1 v0 v1 in
+ let v = M.match_typed_values ctx0 ctx1 v0 v1 in
let var = EBinding (BVar b, v) in
(* Continue *)
var :: join_prefixes env0' env1'
@@ -669,21 +671,21 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (lo
log#ldebug
(lazy
("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n"
- ^ eval_ctx_to_string meta ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx));
(* Destructure the abstractions introduced in the new context *)
let ctx = destructure_new_abs meta loop_id fixed_ids.aids ctx in
log#ldebug
(lazy
("loop_join_origin_with_continue_ctxs:join_one: after destructure:\n"
- ^ eval_ctx_to_string meta ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx));
(* Collapse the context we want to add to the join *)
let ctx = collapse_ctx meta loop_id None fixed_ids ctx in
log#ldebug
(lazy
("loop_join_origin_with_continue_ctxs:join_one: after collapse:\n"
- ^ eval_ctx_to_string meta ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx));
(* Refresh the fresh abstractions *)
let ctx = refresh_abs fixed_ids.aids ctx in
@@ -693,7 +695,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (lo
log#ldebug
(lazy
("loop_join_origin_with_continue_ctxs:join_one: after join:\n"
- ^ eval_ctx_to_string meta ctx1));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx1));
(* Collapse again - the join might have introduce abstractions we want
to merge with the others (note that those abstractions may actually
@@ -702,7 +704,7 @@ let loop_join_origin_with_continue_ctxs (config : config) (meta : Meta.meta) (lo
log#ldebug
(lazy
("loop_join_origin_with_continue_ctxs:join_one: after join-collapse:\n"
- ^ eval_ctx_to_string meta !joined_ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) !joined_ctx));
(* Sanity check *)
if !Config.sanity_checks then Invariants.check_invariants meta !joined_ctx;
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 435174a7..c02d3117 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -149,9 +149,9 @@ let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty)
let match_rec = match_types meta match_distinct_types match_regions in
match (ty0, ty1) with
| TAdt (id0, generics0), TAdt (id1, generics1) ->
- cassert (id0 = id1) meta "TODO: error message";
- cassert (generics0.const_generics = generics1.const_generics) meta "TODO: error message";
- cassert (generics0.trait_refs = generics1.trait_refs) meta "TODO: error message";
+ sanity_check (id0 = id1) meta;
+ sanity_check (generics0.const_generics = generics1.const_generics) meta;
+ sanity_check (generics0.trait_refs = generics1.trait_refs) meta;
let id = id0 in
let const_generics = generics1.const_generics in
let trait_refs = generics1.trait_refs in
@@ -168,27 +168,28 @@ let rec match_types (meta : Meta.meta) (match_distinct_types : ty -> ty -> ty)
let generics = { regions; types; const_generics; trait_refs } in
TAdt (id, generics)
| TVar vid0, TVar vid1 ->
- cassert (vid0 = vid1) meta "TODO: error message";
+ sanity_check (vid0 = vid1) meta;
let vid = vid0 in
TVar vid
| TLiteral lty0, TLiteral lty1 ->
- cassert (lty0 = lty1) meta "TODO: error message";
+ sanity_check (lty0 = lty1) meta;
ty0
| TNever, TNever -> ty0
| TRef (r0, ty0, k0), TRef (r1, ty1, k1) ->
let r = match_regions r0 r1 in
let ty = match_rec ty0 ty1 in
- cassert (k0 = k1) meta "TODO: error message";
+ sanity_check (k0 = k1) meta;
let k = k0 in
TRef (r, ty, k)
| _ -> match_distinct_types ty0 ty1
module MakeMatcher (M : PrimMatcher) : Matcher = struct
- let rec match_typed_values (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx)
+ let meta = M.meta
+ let rec match_typed_values (ctx0 : eval_ctx) (ctx1 : eval_ctx)
(v0 : typed_value) (v1 : typed_value) : typed_value =
- let match_rec = match_typed_values meta ctx0 ctx1 in
- let ty = M.match_etys meta ctx0 ctx1 v0.ty v1.ty in
- (* Using ValuesUtils.value_has_borrows on purpose here: we want
+ let match_rec = match_typed_values ctx0 ctx1 in
+ let ty = M.match_etys ctx0 ctx1 v0.ty v1.ty in
+ (* Using ValuesUtils.value_ has_borrows on purpose here: we want
to make explicit the fact that, though we have to pick
one of the two contexts (ctx0 here) to call value_has_borrows,
it doesn't matter here. *)
@@ -197,7 +198,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
in
match (v0.value, v1.value) with
| VLiteral lv0, VLiteral lv1 ->
- if lv0 = lv1 then v1 else M.match_distinct_literals meta ctx0 ctx1 ty lv0 lv1
+ if lv0 = lv1 then v1 else M.match_distinct_literals ctx0 ctx1 ty lv0 lv1
| VAdt av0, VAdt av1 ->
if av0.variant_id = av1.variant_id then
let fields = List.combine av0.field_values av1.field_values in
@@ -210,17 +211,17 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
{ value; ty = v1.ty }
else (
(* For now, we don't merge ADTs which contain borrows *)
- cassert (not (value_has_borrows v0.value)) meta "ADTs which contain borrows are not merged yet";
- cassert (not (value_has_borrows v1.value)) meta "ADTs which contain borrows are not merged yet";
+ sanity_check (not (value_has_borrows v0.value)) M.meta;
+ sanity_check (not (value_has_borrows v1.value)) M.meta;
(* Merge *)
- M.match_distinct_adts meta ctx0 ctx1 ty av0 av1)
+ M.match_distinct_adts ctx0 ctx1 ty av0 av1)
| VBottom, VBottom -> v0
| VBorrow bc0, VBorrow bc1 ->
let bc =
match (bc0, bc1) with
| VSharedBorrow bid0, VSharedBorrow bid1 ->
let bid =
- M.match_shared_borrows meta ctx0 ctx1 match_rec ty bid0 bid1
+ M.match_shared_borrows ctx0 ctx1 match_rec ty bid0 bid1
in
VSharedBorrow bid
| VMutBorrow (bid0, bv0), VMutBorrow (bid1, bv1) ->
@@ -229,9 +230,9 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
cassert (
not
(ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos
- bv.value)) meta "TODO: error message";
+ bv.value)) M.meta "TODO: error message";
let bid, bv =
- M.match_mut_borrows meta ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv
+ M.match_mut_borrows ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv
in
VMutBorrow (bid, bv)
| VReservedMutBorrow _, _
@@ -242,7 +243,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
trying to match a reserved borrow, which shouldn't happen because
reserved borrow should be eliminated very quickly - they are introduced
just before function calls which activate them *)
- craise meta "Unexpected"
+ craise M.meta "Unexpected"
in
{ value = VBorrow bc; ty }
| VLoan lc0, VLoan lc1 ->
@@ -252,23 +253,23 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
match (lc0, lc1) with
| VSharedLoan (ids0, sv0), VSharedLoan (ids1, sv1) ->
let sv = match_rec sv0 sv1 in
- cassert (not (value_has_borrows sv.value)) meta "TODO: error message";
- let ids, sv = M.match_shared_loans meta ctx0 ctx1 ty ids0 ids1 sv in
+ cassert (not (value_has_borrows sv.value)) M.meta "TODO: error message";
+ let ids, sv = M.match_shared_loans ctx0 ctx1 ty ids0 ids1 sv in
VSharedLoan (ids, sv)
| VMutLoan id0, VMutLoan id1 ->
let id = M.match_mut_loans ctx0 ctx1 ty id0 id1 in
VMutLoan id
| VSharedLoan _, VMutLoan _ | VMutLoan _, VSharedLoan _ ->
- craise meta "Unreachable"
+ craise M.meta "Unreachable"
in
{ value = VLoan lc; ty = v1.ty }
| VSymbolic sv0, VSymbolic sv1 ->
(* For now, we force all the symbolic values containing borrows to
be eagerly expanded, and we don't support nested borrows *)
- cassert (not (value_has_borrows v0.value)) meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded";
- cassert (not (value_has_borrows v1.value)) meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded";
+ cassert (not (value_has_borrows v0.value)) M.meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded";
+ cassert (not (value_has_borrows v1.value)) M.meta "Nested borrows are not supported yet and all the symbolic values containing borrows are currently forced to be eagerly expanded";
(* Match *)
- let sv = M.match_symbolic_values meta ctx0 ctx1 sv0 sv1 in
+ let sv = M.match_symbolic_values ctx0 ctx1 sv0 sv1 in
{ v1 with value = VSymbolic sv }
| VLoan lc, _ -> (
match lc with
@@ -278,27 +279,27 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
match lc with
| VSharedLoan (ids, _) -> raise (ValueMatchFailure (LoansInRight ids))
| VMutLoan id -> raise (ValueMatchFailure (LoanInRight id)))
- | VSymbolic sv, _ -> M.match_symbolic_with_other meta ctx0 ctx1 true sv v1
- | _, VSymbolic sv -> M.match_symbolic_with_other meta ctx0 ctx1 false sv v0
- | VBottom, _ -> M.match_bottom_with_other meta ctx0 ctx1 true v1
- | _, VBottom -> M.match_bottom_with_other meta ctx0 ctx1 false v0
+ | VSymbolic sv, _ -> M.match_symbolic_with_other ctx0 ctx1 true sv v1
+ | _, VSymbolic sv -> M.match_symbolic_with_other ctx0 ctx1 false sv v0
+ | VBottom, _ -> M.match_bottom_with_other ctx0 ctx1 true v1
+ | _, VBottom -> M.match_bottom_with_other ctx0 ctx1 false v0
| _ ->
log#ldebug
(lazy
("Unexpected match case:\n- value0: "
- ^ typed_value_to_string meta ctx0 v0
+ ^ typed_value_to_string ~meta:(Some M.meta) ctx0 v0
^ "\n- value1: "
- ^ typed_value_to_string meta ctx1 v1));
- craise meta "Unexpected match case"
+ ^ typed_value_to_string ~meta:(Some M.meta) ctx1 v1));
+ craise M.meta "Unexpected match case"
- and match_typed_avalues (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx)
+ and match_typed_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx)
(v0 : typed_avalue) (v1 : typed_avalue) : typed_avalue =
log#ldebug
(lazy
("match_typed_avalues:\n- value0: "
- ^ typed_avalue_to_string meta ctx0 v0
+ ^ typed_avalue_to_string ~meta:(Some M.meta) ctx0 v0
^ "\n- value1: "
- ^ typed_avalue_to_string meta ctx1 v1));
+ ^ typed_avalue_to_string ~meta:(Some M.meta) ctx1 v1));
(* Using ValuesUtils.value_has_borrows on purpose here: we want
to make explicit the fact that, though we have to pick
@@ -308,9 +309,9 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos
in
- let match_rec = match_typed_values meta ctx0 ctx1 in
- let match_arec = match_typed_avalues meta ctx0 ctx1 in
- let ty = M.match_rtys meta ctx0 ctx1 v0.ty v1.ty in
+ let match_rec = match_typed_values ctx0 ctx1 in
+ let match_arec = match_typed_avalues ctx0 ctx1 in
+ let ty = M.match_rtys ctx0 ctx1 v0.ty v1.ty in
match (v0.value, v1.value) with
| AAdt av0, AAdt av1 ->
if av0.variant_id = av1.variant_id then
@@ -323,15 +324,15 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
in
{ value; ty }
else (* Merge *)
- M.match_distinct_aadts meta ctx0 ctx1 v0.ty av0 v1.ty av1 ty
- | ABottom, ABottom -> mk_abottom meta ty
- | AIgnored, AIgnored -> mk_aignored meta ty
+ M.match_distinct_aadts ctx0 ctx1 v0.ty av0 v1.ty av1 ty
+ | ABottom, ABottom -> mk_abottom M.meta ty
+ | AIgnored, AIgnored -> mk_aignored M.meta ty
| ABorrow bc0, ABorrow bc1 -> (
log#ldebug (lazy "match_typed_avalues: borrows");
match (bc0, bc1) with
| ASharedBorrow bid0, ASharedBorrow bid1 ->
log#ldebug (lazy "match_typed_avalues: shared borrows");
- M.match_ashared_borrows meta ctx0 ctx1 v0.ty bid0 v1.ty bid1 ty
+ M.match_ashared_borrows ctx0 ctx1 v0.ty bid0 v1.ty bid1 ty
| AMutBorrow (bid0, av0), AMutBorrow (bid1, av1) ->
log#ldebug (lazy "match_typed_avalues: mut borrows");
log#ldebug
@@ -340,10 +341,10 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
let av = match_arec av0 av1 in
log#ldebug
(lazy "match_typed_avalues: mut borrows: matched children values");
- M.match_amut_borrows meta ctx0 ctx1 v0.ty bid0 av0 v1.ty bid1 av1 ty av
+ M.match_amut_borrows ctx0 ctx1 v0.ty bid0 av0 v1.ty bid1 av1 ty av
| AIgnoredMutBorrow _, AIgnoredMutBorrow _ ->
(* The abstractions are destructured: we shouldn't get there *)
- craise meta "Unexpected"
+ craise M.meta "Unexpected"
| AProjSharedBorrow asb0, AProjSharedBorrow asb1 -> (
match (asb0, asb1) with
| [], [] ->
@@ -352,7 +353,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
v0
| _ ->
(* We should get there only if there are nested borrows *)
- craise meta "Unexpected")
+ craise M.meta "Unexpected")
| _ ->
(* TODO: getting there is not necessarily inconsistent (it may
just be because the environments don't match) so we may want
@@ -363,7 +364,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
we are *currently* ending it, in which case we need
to completely end it before continuing.
*)
- craise meta "Unexpected")
+ craise M.meta "Unexpected")
| ALoan lc0, ALoan lc1 -> (
log#ldebug (lazy "match_typed_avalues: loans");
(* TODO: maybe we should enforce that the ids are always exactly the same -
@@ -373,8 +374,8 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
log#ldebug (lazy "match_typed_avalues: shared loans");
let sv = match_rec sv0 sv1 in
let av = match_arec av0 av1 in
- cassert (not (value_has_borrows sv.value)) meta "TODO: error message";
- M.match_ashared_loans meta ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1
+ sanity_check (not (value_has_borrows sv.value)) M.meta;
+ M.match_ashared_loans ctx0 ctx1 v0.ty ids0 sv0 av0 v1.ty ids1 sv1
av1 ty sv av
| AMutLoan (id0, av0), AMutLoan (id1, av1) ->
log#ldebug (lazy "match_typed_avalues: mut loans");
@@ -383,48 +384,49 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
let av = match_arec av0 av1 in
log#ldebug
(lazy "match_typed_avalues: mut loans: matched children values");
- M.match_amut_loans meta ctx0 ctx1 v0.ty id0 av0 v1.ty id1 av1 ty av
+ M.match_amut_loans ctx0 ctx1 v0.ty id0 av0 v1.ty id1 av1 ty av
| AIgnoredMutLoan _, AIgnoredMutLoan _
| AIgnoredSharedLoan _, AIgnoredSharedLoan _ ->
(* Those should have been filtered when destructuring the abstractions -
they are necessary only when there are nested borrows *)
- craise meta "Unreachable"
- | _ -> craise meta "Unreachable")
+ craise M.meta "Unreachable"
+ | _ -> craise M.meta "Unreachable")
| ASymbolic _, ASymbolic _ ->
(* For now, we force all the symbolic values containing borrows to
be eagerly expanded, and we don't support nested borrows *)
- craise meta "Unreachable"
- | _ -> M.match_avalues meta ctx0 ctx1 v0 v1
+ craise M.meta "Unreachable"
+ | _ -> M.match_avalues ctx0 ctx1 v0 v1
end
module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(** Small utility *)
+ let meta = S.meta
let push_abs (abs : abs) : unit = S.nabs := abs :: !S.nabs
let push_absl (absl : abs list) : unit = List.iter push_abs absl
- let match_etys (meta : Meta.meta) _ _ ty0 ty1 =
- cassert (ty0 = ty1) meta "TODO: error message";
+ let match_etys _ _ ty0 ty1 =
+ sanity_check (ty0 = ty1) meta;
ty0
- let match_rtys (meta : Meta.meta) _ _ ty0 ty1 =
+ let match_rtys _ _ ty0 ty1 =
(* The types must be equal - in effect, this forbids to match symbolic
values containing borrows *)
- cassert (ty0 = ty1) meta "The types must be equal - in effect, this forbids to match symbolic values containing borrows";
+ sanity_check (ty0 = ty1) meta;
ty0
- let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
+ let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
(_ : literal) (_ : literal) : typed_value =
mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty
- let match_distinct_adts (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (ty : ety)
+ let match_distinct_adts (ctx0 : eval_ctx) (ctx1 : eval_ctx) (ty : ety)
(adt0 : adt_value) (adt1 : adt_value) : typed_value =
(* Check that the ADTs don't contain borrows - this is redundant with checks
performed by the caller, but we prefer to be safe with regards to future
updates
*)
let check_no_borrows ctx (v : typed_value) =
- cassert (not (value_has_borrows ctx v.value)) meta "ADTs should not contain borrows"
+ sanity_check (not (value_has_borrows ctx v.value)) meta
in
List.iter (check_no_borrows ctx0) adt0.field_values;
List.iter (check_no_borrows ctx1) adt1.field_values;
@@ -452,7 +454,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* No borrows, no loans, no bottoms: we can introduce a symbolic value *)
mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty
- let match_shared_borrows (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) match_rec
+ let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx) match_rec
(ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id =
(* Lookup the shared values and match them - we do this mostly
to make sure we end loans which might appear on one side
@@ -508,7 +510,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* Return the new borrow *)
bid2
- let match_mut_borrows (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx) (ty : ety)
+ let match_mut_borrows (ctx0 : eval_ctx) (_ : eval_ctx) (ty : ety)
(bid0 : borrow_id) (bv0 : typed_value) (bid1 : borrow_id)
(bv1 : typed_value) (bv : typed_value) : borrow_id * typed_value =
if bid0 = bid1 then (
@@ -560,10 +562,10 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
will update [v], while the backward loop function will return nothing.
*)
cassert (
- not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "TODO: error message";
+ not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) meta "Nested borrows are not supported yet";
if bv0 = bv1 then (
- cassert (bv0 = bv) meta "TODO: error message";
+ sanity_check (bv0 = bv) meta;
(bid0, bv))
else
let rid = fresh_region_id () in
@@ -571,7 +573,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
let kind = RMut in
let bv_ty = bv.ty in
- cassert (ty_no_regions bv_ty) meta "TODO: error message";
+ sanity_check (ty_no_regions bv_ty) meta;
let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
let borrow_av =
@@ -624,7 +626,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* Generate the avalues for the abstraction *)
let mk_aborrow (bid : borrow_id) (bv : typed_value) : typed_avalue =
let bv_ty = bv.ty in
- cassert (ty_no_regions bv_ty) meta "TODO: error message";
+ cassert (ty_no_regions bv_ty) meta "Nested borrows are not supported yet";
let value = ABorrow (AMutBorrow (bid, mk_aignored meta bv_ty)) in
{ value; ty = borrow_ty }
in
@@ -654,7 +656,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* Return the new borrow *)
(bid2, sv)
- let match_shared_loans (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
+ let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
(ids0 : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) :
loan_id_set * typed_value =
(* Check if the ids are the same - Rem.: we forbid the sets of loans
@@ -671,7 +673,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
raise (ValueMatchFailure (LoansInRight extra_ids_right));
(* This should always be true if we get here *)
- cassert (ids0 = ids1) meta "This should always be true if we get here ";
+ sanity_check (ids0 = ids1) meta;
let ids = ids0 in
(* Return *)
@@ -685,7 +687,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
both borrows *)
raise (ValueMatchFailure (LoanInLeft id0))
- let match_symbolic_values (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx)
+ let match_symbolic_values (ctx0 : eval_ctx) (_ : eval_ctx)
(sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value =
let id0 = sv0.sv_id in
let id1 = sv1.sv_id in
@@ -697,11 +699,11 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
else (
(* The caller should have checked that the symbolic values don't contain
borrows *)
- cassert (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta "The caller should have checked that the symbolic values don't contain borrows";
+ sanity_check (not (ty_has_borrows ctx0.type_ctx.type_infos sv0.sv_ty)) meta;
(* We simply introduce a fresh symbolic value *)
mk_fresh_symbolic_value meta sv0.sv_ty)
- let match_symbolic_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool)
+ let match_symbolic_with_other (ctx0 : eval_ctx) (_ : eval_ctx) (left : bool)
(sv : symbolic_value) (v : typed_value) : typed_value =
(* Check that:
- there are no borrows in the symbolic value
@@ -729,7 +731,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* Return a fresh symbolic value *)
mk_fresh_symbolic_typed_value meta sv.sv_ty
- let match_bottom_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool)
+ let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool)
(v : typed_value) : typed_value =
(* If there are outer loans in the non-bottom value, raise an exception.
Otherwise, convert it to an abstraction and return [Bottom].
@@ -770,15 +772,15 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* As explained in comments: we don't use the join matcher to join avalues,
only concrete values *)
- let match_distinct_aadts (meta : Meta.meta) _ _ _ _ _ _ _ = craise meta "Unreachable"
- let match_ashared_borrows (meta : Meta.meta) _ _ _ _ _ _ = craise meta "Unreachable"
- let match_amut_borrows (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable"
+ let match_distinct_aadts _ _ _ _ _ _ _ = craise meta "Unreachable"
+ let match_ashared_borrows _ _ _ _ _ _ = craise meta "Unreachable"
+ let match_amut_borrows _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable"
- let match_ashared_loans (meta: Meta.meta) _ _ _ _ _ _ _ _ _ _ _ _ _ =
+ let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ =
craise meta "Unreachable"
- let match_amut_loans (meta: Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable"
- let match_avalues (meta: Meta.meta) _ _ _ _ = craise meta "Unreachable"
+ let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable"
+ let match_avalues _ _ _ _ = craise meta "Unreachable"
end
(* Very annoying: functors only take modules as inputs... *)
@@ -788,6 +790,7 @@ module type MatchMoveState = sig
(** The moved values *)
val nvalues : typed_value list ref
+ val meta : Meta.meta
end
(* We use this matcher to move values in environment.
@@ -808,40 +811,41 @@ end
*)
module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
(** Small utility *)
+ let meta = S.meta
let push_moved_value (v : typed_value) : unit = S.nvalues := v :: !S.nvalues
- let match_etys (meta : Meta.meta) _ _ ty0 ty1 =
- cassert (ty0 = ty1) meta "TODO: error message";
+ let match_etys _ _ ty0 ty1 =
+ sanity_check (ty0 = ty1) meta;
ty0
- let match_rtys (meta : Meta.meta) _ _ ty0 ty1 =
+ let match_rtys _ _ ty0 ty1 =
(* The types must be equal - in effect, this forbids to match symbolic
values containing borrows *)
- cassert (ty0 = ty1) meta "The types must be equal - in effect, this forbids to match symbolic values containing borrows";
+ sanity_check (ty0 = ty1) meta;
ty0
- let match_distinct_literals (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
+ let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
(_ : literal) (l : literal) : typed_value =
{ value = VLiteral l; ty }
- let match_distinct_adts (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
+ let match_distinct_adts (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
(_ : adt_value) (adt1 : adt_value) : typed_value =
(* Note that if there was a bottom inside the ADT on the left,
the value on the left should have been simplified to bottom. *)
{ ty; value = VAdt adt1 }
- let match_shared_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ (_ : ety)
+ let match_shared_borrows (_ : eval_ctx) (_ : eval_ctx) _ (_ : ety)
(_ : borrow_id) (bid1 : borrow_id) : borrow_id =
(* There can't be bottoms in shared values *)
bid1
- let match_mut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (_ : borrow_id)
+ let match_mut_borrows (_ : eval_ctx) (_ : eval_ctx) (_ : ety) (_ : borrow_id)
(_ : typed_value) (bid1 : borrow_id) (bv1 : typed_value) (_ : typed_value)
: borrow_id * typed_value =
(* There can't be bottoms in borrowed values *)
(bid1, bv1)
- let match_shared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
+ let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
(_ : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) :
loan_id_set * typed_value =
(* There can't be bottoms in shared loans *)
@@ -851,15 +855,15 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
(id1 : loan_id) : loan_id =
id1
- let match_symbolic_values (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : symbolic_value)
+ let match_symbolic_values (_ : eval_ctx) (_ : eval_ctx) (_ : symbolic_value)
(sv1 : symbolic_value) : symbolic_value =
sv1
- let match_symbolic_with_other (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool)
+ let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool)
(sv : symbolic_value) (v : typed_value) : typed_value =
if left then v else mk_typed_value_from_symbolic_value sv
- let match_bottom_with_other (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool)
+ let match_bottom_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool)
(v : typed_value) : typed_value =
let with_borrows = false in
if left then (
@@ -891,22 +895,21 @@ module MakeMoveMatcher (S : MatchMoveState) : PrimMatcher = struct
(* As explained in comments: we don't use the join matcher to join avalues,
only concrete values *)
- let match_distinct_aadts (meta : Meta.meta) _ _ _ _ _ _ _ = craise meta "Unreachable"
- let match_ashared_borrows (meta : Meta.meta) _ _ _ _ _ _ = craise meta "Unreachable"
- let match_amut_borrows (meta : Meta.meta) _ _ _ _ _ _ _ _ _ = craise meta "Unreachable"
+ let match_distinct_aadts _ _ _ _ _ _ _ = craise meta "Unreachable"
+ let match_ashared_borrows _ _ _ _ _ _ = craise meta "Unreachable"
+ let match_amut_borrows _ _ _ _ _ _ _ _ _ = craise meta "Unreachable"
- let match_ashared_loans (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ _ _ _ =
+ let match_ashared_loans _ _ _ _ _ _ _ _ _ _ _ _ _ =
craise meta "Unreachable"
- let match_amut_loans (meta : Meta.meta) _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable"
- let match_avalues (meta : Meta.meta) _ _ _ _ = craise meta "Unreachable"
+ let match_amut_loans _ _ _ _ _ _ _ _ _ _ = craise meta "Unreachable"
+ let match_avalues _ _ _ _ = craise meta "Unreachable"
end
module MakeCheckEquivMatcher (S : MatchCheckEquivState) : CheckEquivMatcher =
struct
module MkGetSetM (Id : Identifiers.Id) = struct
module Inj = Id.InjSubst
-
let add (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) =
(* Check if k0 is already registered as a key *)
match Inj.find_opt k0 !m with
@@ -945,7 +948,7 @@ struct
Id.Set.of_list
(match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1))
end
-
+ let meta = S.meta
module GetSetRid = MkGetSetM (RegionId)
let match_rid = GetSetRid.match_e "match_rid: " S.rid_map
@@ -989,10 +992,10 @@ struct
let match_aids = GetSetAid.match_es "match_aids: " S.aid_map
(** *)
- let match_etys (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 =
+ let match_etys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 =
if ty0 <> ty1 then raise (Distinct "match_etys") else ty0
- let match_rtys (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 =
+ let match_rtys (_ : eval_ctx) (_ : eval_ctx) ty0 ty1 =
let match_distinct_types _ _ = raise (Distinct "match_rtys") in
let match_regions r0 r1 =
match (r0, r1) with
@@ -1004,15 +1007,15 @@ struct
in
match_types meta match_distinct_types match_regions ty0 ty1
- let match_distinct_literals (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
+ let match_distinct_literals (_ : eval_ctx) (_ : eval_ctx) (ty : ety)
(_ : literal) (_ : literal) : typed_value =
mk_fresh_symbolic_typed_value_from_no_regions_ty meta ty
- let match_distinct_adts (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ty : ety)
+ let match_distinct_adts (_ : eval_ctx) (_ : eval_ctx) (_ty : ety)
(_adt0 : adt_value) (_adt1 : adt_value) : typed_value =
raise (Distinct "match_distinct_adts")
- let match_shared_borrows (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx)
+ let match_shared_borrows (ctx0 : eval_ctx) (ctx1 : eval_ctx)
(match_typed_values : typed_value -> typed_value -> typed_value)
(_ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) : borrow_id =
log#ldebug
@@ -1033,22 +1036,22 @@ struct
(lazy
("MakeCheckEquivMatcher: match_shared_borrows: looked up values:"
^ "sv0: "
- ^ typed_value_to_string meta ctx0 v0
+ ^ typed_value_to_string ~meta:(Some meta) ctx0 v0
^ ", sv1: "
- ^ typed_value_to_string meta ctx1 v1));
+ ^ typed_value_to_string ~meta:(Some meta) ctx1 v1));
let _ = match_typed_values v0 v1 in
()
in
bid
- let match_mut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ty : ety)
+ let match_mut_borrows (_ : eval_ctx) (_ : eval_ctx) (_ty : ety)
(bid0 : borrow_id) (_bv0 : typed_value) (bid1 : borrow_id)
(_bv1 : typed_value) (bv : typed_value) : borrow_id * typed_value =
let bid = match_borrow_id bid0 bid1 in
(bid, bv)
- let match_shared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
+ let match_shared_loans (_ : eval_ctx) (_ : eval_ctx) (_ : ety)
(ids0 : loan_id_set) (ids1 : loan_id_set) (sv : typed_value) :
loan_id_set * typed_value =
let ids = match_loan_ids ids0 ids1 in
@@ -1058,7 +1061,7 @@ struct
(bid1 : loan_id) : loan_id =
match_loan_id bid0 bid1
- let match_symbolic_values (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx)
+ let match_symbolic_values (ctx0 : eval_ctx) (ctx1 : eval_ctx)
(sv0 : symbolic_value) (sv1 : symbolic_value) : symbolic_value =
let id0 = sv0.sv_id in
let id1 = sv1.sv_id in
@@ -1077,12 +1080,12 @@ struct
let sv_id =
GetSetSid.match_e "match_symbolic_values: ids: " S.sid_map id0 id1
in
- let sv_ty = match_rtys meta ctx0 ctx1 sv0.sv_ty sv1.sv_ty in
+ let sv_ty = match_rtys ctx0 ctx1 sv0.sv_ty sv1.sv_ty in
let sv = { sv_id; sv_ty } in
sv
else (
(* Check: fixed values are fixed *)
- cassert (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)) meta "Fixed values should be fixed";
+ sanity_check (id0 = id1 || not (SymbolicValueId.InjSubst.mem id0 !S.sid_map)) meta;
(* Update the symbolic value mapping *)
let sv1 = mk_typed_value_from_symbolic_value sv1 in
@@ -1095,21 +1098,21 @@ struct
we want *)
sv0)
- let match_symbolic_with_other (meta : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) (left : bool)
+ let match_symbolic_with_other (_ : eval_ctx) (_ : eval_ctx) (left : bool)
(sv : symbolic_value) (v : typed_value) : typed_value =
if S.check_equiv then raise (Distinct "match_symbolic_with_other")
else (
- cassert left meta "TODO: error message";
+ sanity_check left meta;
let id = sv.sv_id in
(* Check: fixed values are fixed *)
- cassert (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta "Fixed values should be fixed";
+ sanity_check (not (SymbolicValueId.InjSubst.mem id !S.sid_map)) meta;
(* Update the binding for the target symbolic value *)
S.sid_to_value_map :=
SymbolicValueId.Map.add_strict id v !S.sid_to_value_map;
(* Return - the returned value is not used, so we can return whatever we want *)
v)
- let match_bottom_with_other (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool)
+ let match_bottom_with_other (ctx0 : eval_ctx) (ctx1 : eval_ctx) (left : bool)
(v : typed_value) : typed_value =
(* It can happen that some variables get initialized in some branches
and not in some others, which causes problems when matching. *)
@@ -1126,47 +1129,47 @@ struct
^ Print.bool_to_string left ^ "\n- value to match with bottom:\n"
^ show_typed_value v))
- let match_distinct_aadts _ _ _ _ _ _ _ _ =
+ let match_distinct_aadts _ _ _ _ _ _ _ =
raise (Distinct "match_distinct_adts")
- let match_ashared_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _ty1 bid1 ty
+ let match_ashared_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _ty1 bid1 ty
=
let bid = match_borrow_id bid0 bid1 in
let value = ABorrow (ASharedBorrow bid) in
{ value; ty }
- let match_amut_borrows (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _av0 _ty1 bid1
+ let match_amut_borrows (_ : eval_ctx) (_ : eval_ctx) _ty0 bid0 _av0 _ty1 bid1
_av1 ty av =
let bid = match_borrow_id bid0 bid1 in
let value = ABorrow (AMutBorrow (bid, av)) in
{ value; ty }
- let match_ashared_loans (_ : Meta.meta) (_ : eval_ctx) (_ : eval_ctx) _ty0 ids0 _v0 _av0 _ty1
+ let match_ashared_loans (_ : eval_ctx) (_ : eval_ctx) _ty0 ids0 _v0 _av0 _ty1
ids1 _v1 _av1 ty v av =
let bids = match_loan_ids ids0 ids1 in
let value = ALoan (ASharedLoan (bids, v, av)) in
{ value; ty }
- let match_amut_loans (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1
+ let match_amut_loans (ctx0 : eval_ctx) (ctx1 : eval_ctx) _ty0 id0 _av0 _ty1
id1 _av1 ty av =
log#ldebug
(lazy
("MakeCheckEquivMatcher:match_amut_loans:" ^ "\n- id0: "
^ BorrowId.to_string id0 ^ "\n- id1: " ^ BorrowId.to_string id1
^ "\n- ty: " ^ ty_to_string ctx0 ty ^ "\n- av: "
- ^ typed_avalue_to_string meta ctx1 av));
+ ^ typed_avalue_to_string ~meta:(Some meta) ctx1 av));
let id = match_loan_id id0 id1 in
let value = ALoan (AMutLoan (id, av)) in
{ value; ty }
- let match_avalues (meta : Meta.meta) (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 =
+ let match_avalues (ctx0 : eval_ctx) (ctx1 : eval_ctx) v0 v1 =
log#ldebug
(lazy
("avalues don't match:\n- v0: "
- ^ typed_avalue_to_string meta ctx0 v0
+ ^ typed_avalue_to_string ~meta:(Some meta) ctx0 v0
^ "\n- v1: "
- ^ typed_avalue_to_string meta ctx1 v1));
+ ^ typed_avalue_to_string ~meta:(Some meta) ctx1 v1));
raise (Distinct "match_avalues")
end
@@ -1178,9 +1181,9 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
(lazy
("match_ctxs:\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids
^ "\n\n- ctx0:\n"
- ^ eval_ctx_to_string_no_filter meta ctx0
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx0
^ "\n\n- ctx1:\n"
- ^ eval_ctx_to_string_no_filter meta ctx1
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx1
^ "\n\n"));
(* Initialize the maps and instantiate the matcher *)
@@ -1222,6 +1225,7 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
in
let module S : MatchCheckEquivState = struct
+ let meta = meta
let check_equiv = check_equiv
let rid_map = rid_map
let blid_map = blid_map
@@ -1288,7 +1292,7 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
log#ldebug (lazy "match_abstractions: matching values");
let _ =
List.map
- (fun (v0, v1) -> M.match_typed_avalues meta ctx0 ctx1 v0 v1)
+ (fun (v0, v1) -> M.match_typed_avalues ctx0 ctx1 v0 v1)
(List.combine avalues0 avalues1)
in
log#ldebug (lazy "match_abstractions: values matched OK");
@@ -1309,9 +1313,9 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
^ "\n- aid_map: "
^ AbstractionId.InjSubst.show_t !aid_map
^ "\n\n- ctx0:\n"
- ^ eval_ctx_to_string_no_filter meta { ctx0 with env = List.rev env0 }
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx0 with env = List.rev env0 }
^ "\n\n- ctx1:\n"
- ^ eval_ctx_to_string_no_filter meta { ctx1 with env = List.rev env1 }
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) { ctx1 with env = List.rev env1 }
^ "\n\n"));
match (env0, env1) with
@@ -1320,19 +1324,19 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
be the same and their values equal (and the borrows/loans/symbolic *)
if DummyVarId.Set.mem b0 fixed_ids.dids then (
(* Fixed values: the values must be equal *)
- cassert (b0 = b1) meta "The fixed values should be equal";
- cassert (v0 = v1) meta "The fixed values should be equal";
+ sanity_check (b0 = b1) meta;
+ sanity_check (v0 = v1) meta;
(* The ids present in the left value must be fixed *)
let ids, _ = compute_typed_value_ids v0 in
- cassert ((not S.check_equiv) || ids_are_fixed ids)) meta "TODO: error message";
+ sanity_check ((not S.check_equiv) || ids_are_fixed ids)) meta;
(* We still match the values - allows to compute mappings (which
are the identity actually) *)
- let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in
+ let _ = M.match_typed_values ctx0 ctx1 v0 v1 in
match_envs env0' env1'
| EBinding (BVar b0, v0) :: env0', EBinding (BVar b1, v1) :: env1' ->
- cassert (b0 = b1) meta "TODO: error message";
+ sanity_check (b0 = b1) meta;
(* Match the values *)
- let _ = M.match_typed_values meta ctx0 ctx1 v0 v1 in
+ let _ = M.match_typed_values ctx0 ctx1 v0 v1 in
(* Continue *)
match_envs env0' env1'
| EAbs abs0 :: env0', EAbs abs1 :: env1' ->
@@ -1341,10 +1345,10 @@ let match_ctxs (meta : Meta.meta) (check_equiv : bool) (fixed_ids : ids_sets)
if AbstractionId.Set.mem abs0.abs_id fixed_ids.aids then (
log#ldebug (lazy "match_ctxs: match_envs: matching abs: fixed abs");
(* Still in the prefix: the abstractions must be the same *)
- cassert (abs0 = abs1) meta "The abstractions should be the same";
+ sanity_check (abs0 = abs1) meta;
(* Their ids must be fixed *)
let ids, _ = compute_abs_ids abs0 in
- cassert ((not S.check_equiv) || ids_are_fixed ids) meta "The ids should be fixed";
+ sanity_check ((not S.check_equiv) || ids_are_fixed ids) meta;
(* Continue *)
match_envs env0' env1')
else (
@@ -1408,7 +1412,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id
(lazy
("prepare_match_ctx_with_target:\n" ^ "\n- fixed_ids: "
^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: "
- ^ eval_ctx_to_string meta src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string meta tgt_ctx
+ ^ eval_ctx_to_string ~meta:(Some meta) src_ctx ^ "\n- tgt_ctx: " ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx
));
(* End the loans which lead to mismatches when joining *)
let rec cf_reorganize_join_tgt : cm_fun =
@@ -1437,6 +1441,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id
let nabs = ref [] in
let module S : MatchJoinState = struct
+ let meta = meta
let loop_id = loop_id
let nabs = nabs
end in
@@ -1448,12 +1453,12 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id
(fun (var0, var1) ->
match (var0, var1) with
| EBinding (BDummy b0, v0), EBinding (BDummy b1, v1) ->
- cassert (b0 = b1) meta "TODO: error message";
- let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in
+ sanity_check (b0 = b1) meta;
+ let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in
()
| EBinding (BVar b0, v0), EBinding (BVar b1, v1) ->
- cassert (b0 = b1) meta "TODO: error message";
- let _ = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in
+ sanity_check (b0 = b1) meta;
+ let _ = M.match_typed_values src_ctx tgt_ctx v0 v1 in
()
| _ -> craise meta "Unexpected")
(List.combine filt_src_env filt_tgt_env)
@@ -1475,6 +1480,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id
environment *)
let nvalues = ref [] in
let module S : MatchMoveState = struct
+ let meta = meta
let loop_id = loop_id
let nvalues = nvalues
end in
@@ -1485,12 +1491,12 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id
(fun (var0, var1) ->
match (var0, var1) with
| EBinding (BDummy b0, v0), EBinding ((BDummy b1 as var1), v1) ->
- cassert (b0 = b1) meta "TODO: error message";
- let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in
+ sanity_check (b0 = b1) meta;
+ let v = M.match_typed_values src_ctx tgt_ctx v0 v1 in
(var1, v)
| EBinding (BVar b0, v0), EBinding ((BVar b1 as var1), v1) ->
- cassert (b0 = b1) meta "TODO: error message";
- let v = M.match_typed_values meta src_ctx tgt_ctx v0 v1 in
+ sanity_check (b0 = b1) meta;
+ let v = M.match_typed_values src_ctx tgt_ctx v0 v1 in
(var1, v)
| _ -> craise meta "Unexpected")
(List.combine filt_src_env filt_tgt_env)
@@ -1520,8 +1526,8 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id
(lazy
("cf_reorganize_join_tgt: done with borrows/loans and moves:\n"
^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids ^ "\n" ^ "\n- src_ctx: "
- ^ eval_ctx_to_string meta src_ctx ^ "\n- tgt_ctx: "
- ^ eval_ctx_to_string meta tgt_ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) src_ctx ^ "\n- tgt_ctx: "
+ ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx));
cf tgt_ctx
with ValueMatchFailure e ->
@@ -1590,7 +1596,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
let filt_src_env, new_absl, new_dummyl =
ctx_split_fixed_new meta fixed_ids src_ctx
in
- cassert (new_dummyl = []) meta "TODO: error message";
+ sanity_check (new_dummyl = []) meta;
let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in
let filt_src_ctx = { src_ctx with env = filt_src_env } in
@@ -1622,13 +1628,13 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
log#ldebug
(lazy
("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- src_ctx: "
- ^ eval_ctx_to_string meta src_ctx ^ "\n\n- tgt_ctx: "
- ^ eval_ctx_to_string meta tgt_ctx ^ "\n\n- filt_tgt_ctx: "
- ^ eval_ctx_to_string_no_filter meta filt_tgt_ctx
+ ^ eval_ctx_to_string ~meta:(Some meta) src_ctx ^ "\n\n- tgt_ctx: "
+ ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx ^ "\n\n- filt_tgt_ctx: "
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_tgt_ctx
^ "\n\n- filt_src_ctx: "
- ^ eval_ctx_to_string_no_filter meta filt_src_ctx
+ ^ eval_ctx_to_string_no_filter ~meta:(Some meta) filt_src_ctx
^ "\n\n- new_absl:\n"
- ^ eval_ctx_to_string meta
+ ^ eval_ctx_to_string ~meta:(Some meta)
{ src_ctx with env = List.map (fun abs -> EAbs abs) new_absl }
^ "\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- fp_bl_maps:\n"
^ show_borrow_loan_corresp fp_bl_maps
@@ -1726,7 +1732,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
abstractions and in the *variable bindings* once we allow symbolic
values containing borrows to not be eagerly expanded.
*)
- cassert Config.greedy_expand_symbolics_with_borrows meta "TODO: error message";
+ sanity_check Config.greedy_expand_symbolics_with_borrows meta;
(* Update the borrows and loans in the abstractions of the target context.
@@ -1795,8 +1801,8 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
(* No mapping: this means that the borrow was mapped when
we matched values (it doesn't come from a fresh abstraction)
and because of this, it should actually be mapped to itself *)
- cassert (
- BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) meta "The borrow should mapped to itself: no mapping means that the borrow was mapped when we matched values (it doesn't come from a fresh abstraction) ";
+ sanity_check (
+ BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id) meta;
id
| Some id -> id
@@ -1808,8 +1814,8 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
method! visit_abs env abs =
match abs.kind with
| Loop (loop_id', rg_id, kind) ->
- cassert (loop_id' = loop_id) meta "TODO: error message";
- cassert (kind = LoopSynthInput) meta "TODO: error message";
+ sanity_check (loop_id' = loop_id) meta;
+ sanity_check (kind = LoopSynthInput) meta;
let can_end = false in
let kind : abs_kind = Loop (loop_id, rg_id, LoopCall) in
let abs = { abs with kind; can_end } in
@@ -1827,7 +1833,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
log#ldebug
(lazy
("match_ctx_with_target: cf_introduce_loop_fp_abs: done:\n\
- - result ctx:\n" ^ eval_ctx_to_string meta tgt_ctx));
+ - result ctx:\n" ^ eval_ctx_to_string ~meta:(Some meta) tgt_ctx));
(* Sanity check *)
if !Config.sanity_checks then
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 3733c06d..93ce0515 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -100,8 +100,8 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx :
(* Check consistency *)
(match (proj_kind, type_id) with
| ProjAdt (def_id, opt_variant_id), TAdtId def_id' ->
- cassert (def_id = def_id') meta "TODO: Error message";
- cassert (opt_variant_id = adt.variant_id) meta "TODO: Error message"
+ sanity_check (def_id = def_id') meta;
+ sanity_check (opt_variant_id = adt.variant_id) meta
| _ -> craise meta "Unreachable");
(* Actually project *)
let fv = FieldId.nth adt.field_values field_id in
@@ -117,7 +117,7 @@ let rec access_projection (meta : Meta.meta) (access : projection_access) (ctx :
Ok (ctx, { res with updated }))
(* Tuples *)
| Field (ProjTuple arity, field_id), VAdt adt, TAdt (TTuple, _) -> (
- cassert (arity = List.length adt.field_values) meta "TODO: Error message";
+ sanity_check (arity = List.length adt.field_values) meta;
let fv = FieldId.nth adt.field_values field_id in
(* Project *)
match access_projection meta access ctx update p' fv with
@@ -349,16 +349,16 @@ let write_place (meta : Meta.meta) (access : access_kind) (p : place) (nv : type
let compute_expanded_bottom_adt_value (meta : Meta.meta) (ctx : eval_ctx) (def_id : TypeDeclId.id)
(opt_variant_id : VariantId.id option) (generics : generic_args) :
typed_value =
- cassert (TypesUtils.generic_args_only_erased_regions generics) meta "TODO: Error message";
+ sanity_check (TypesUtils.generic_args_only_erased_regions generics) meta;
(* Lookup the definition and check if it is an enumeration - it
should be an enumeration if and only if the projection element
is a field projection with *some* variant id. Retrieve the list
of fields at the same time. *)
let def = ctx_lookup_type_decl ctx def_id in
- cassert (List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message";
+ sanity_check (List.length generics.regions = List.length def.generics.regions) meta;
(* Compute the field types *)
let field_types =
- AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def opt_variant_id
+ AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def opt_variant_id
generics
in
(* Initialize the expanded value *)
@@ -425,14 +425,14 @@ let expand_bottom_value_from_projection (meta : Meta.meta) (access : access_kind
(* "Regular" ADTs *)
| ( Field (ProjAdt (def_id, opt_variant_id), _),
TAdt (TAdtId def_id', generics) ) ->
- cassert (def_id = def_id') meta "TODO: Error message";
+ sanity_check (def_id = def_id') meta;
compute_expanded_bottom_adt_value meta ctx def_id opt_variant_id generics
(* Tuples *)
| ( Field (ProjTuple arity, _),
TAdt
(TTuple, { regions = []; types; const_generics = []; trait_refs = [] })
) ->
- cassert (arity = List.length types) meta "TODO: Error message";
+ sanity_check (arity = List.length types) meta;
(* Generate the field values *)
compute_expanded_bottom_tuple_value meta types
| _ ->
@@ -616,7 +616,7 @@ let prepare_lplace (config : config) (meta : Meta.meta) (p : place) (cf : typed_
log#ldebug
(lazy
("prepare_lplace:" ^ "\n- p: " ^ place_to_string ctx p
- ^ "\n- Initial context:\n" ^ eval_ctx_to_string meta ctx));
+ ^ "\n- Initial context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
(* Access the place *)
let access = Write in
let cc = update_ctx_along_write_place config meta access p in
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 5f83b938..809303ae 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -84,7 +84,7 @@ let rec apply_proj_borrows_on_shared_borrow (meta : Meta.meta) (ctx : eval_ctx)
| VLoan _, _ -> craise meta "Unreachable"
| VSymbolic s, _ ->
(* Check that the projection doesn't contain ended regions *)
- cassert (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions)) meta "TODO: error message";
+ sanity_check (not (projections_intersect meta s.sv_ty ctx.ended_regions ty regions)) meta;
[ AsbProjReborrows (s, ty) ]
| _ -> craise meta "Unreachable"
@@ -212,13 +212,13 @@ let rec apply_proj_borrows (meta : Meta.meta) (check_symbolic_no_ended : bool) (
^ "\n- ty2: " ^ ty_to_string ctx ty2 ^ "\n- rset2: "
^ RegionId.Set.to_string None rset2
^ "\n"));
- cassert (not (projections_intersect meta ty1 rset1 ty2 rset2))) meta "TODO: error message";
+ sanity_check (not (projections_intersect meta ty1 rset1 ty2 rset2))) meta;
ASymbolic (AProjBorrows (s, ty))
| _ ->
log#lerror
(lazy
("apply_proj_borrows: unexpected inputs:\n- input value: "
- ^ typed_value_to_string meta ctx v
+ ^ typed_value_to_string ~meta:(Some meta) ctx v
^ "\n- proj rty: " ^ ty_to_string ctx ty));
craise meta "Unreachable"
in
@@ -464,7 +464,7 @@ let apply_reborrows (meta : Meta.meta) (reborrows : (BorrowId.id * BorrowId.id)
(* Visit *)
let ctx = obj#visit_eval_ctx () ctx in
(* Check that there are no reborrows remaining *)
- cassert (!reborrows = []) meta "TODO: error message";
+ sanity_check (!reborrows = []) meta;
(* Return *)
ctx
@@ -483,7 +483,7 @@ let prepare_reborrows (config : config) (meta : Meta.meta) (allow_reborrows : bo
let apply_registered_reborrows (ctx : eval_ctx) : eval_ctx =
match config.mode with
| ConcreteMode ->
- cassert (!reborrows = []) meta "TODO: error message";
+ sanity_check (!reborrows = []) meta;
ctx
| SymbolicMode ->
(* Apply the reborrows *)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 5e8f7c55..a872f24a 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -24,7 +24,7 @@ let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun =
log#ldebug
(lazy
("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n"
- ^ eval_ctx_to_string meta ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx));
(* Note that we use [Write], not [Move]: we allow to drop values *below* borrows *)
let access = Write in
(* First make sure we can access the place, by ending loans or expanding
@@ -45,7 +45,7 @@ let drop_value (config : config) (meta : Meta.meta) (p : place) : cm_fun =
log#ldebug
(lazy
("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n"
- ^ eval_ctx_to_string meta ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx));
cf ctx
in
(* Compose and apply *)
@@ -99,9 +99,9 @@ let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value) (p :
log#ldebug
(lazy
("assign_to_place:" ^ "\n- rv: "
- ^ typed_value_to_string meta ctx rv
+ ^ typed_value_to_string ~meta:(Some meta) ctx rv
^ "\n- p: " ^ place_to_string ctx p ^ "\n- Initial context:\n"
- ^ eval_ctx_to_string meta ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx));
(* Push the rvalue to a dummy variable, for bookkeeping *)
let rvalue_vid = fresh_dummy_var_id () in
let cc = push_dummy_var rvalue_vid rv in
@@ -119,16 +119,16 @@ let assign_to_place (config : config) (meta : Meta.meta) (rv : typed_value) (p :
let ctx = ctx_push_dummy_var ctx dest_vid mv in
(* Write to the destination *)
(* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *)
- cassert (not (bottom_in_value ctx.ended_regions rv)) meta "TODO: Error message";
+ exec_assert (not (bottom_in_value ctx.ended_regions rv)) meta "The value to move contains bottom";
(* Update the destination *)
let ctx = write_place meta Write p rv ctx in
(* Debug *)
log#ldebug
(lazy
("assign_to_place:" ^ "\n- rv: "
- ^ typed_value_to_string meta ctx rv
+ ^ typed_value_to_string ~meta:(Some meta) ctx rv
^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n"
- ^ eval_ctx_to_string meta ctx));
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx));
(* Continue *)
cf ctx
in
@@ -149,7 +149,7 @@ let eval_assertion_concrete (config : config) (meta : Meta.meta) (assertion : as
if b = assertion.expected then cf Unit ctx else cf Panic ctx
| _ ->
craise
- meta ("Expected a boolean, got: " ^ typed_value_to_string meta ctx v)
+ meta ("Expected a boolean, got: " ^ typed_value_to_string ~meta:(Some meta) ctx v)
in
(* Compose and apply *)
comp eval_op eval_assert cf ctx
@@ -167,7 +167,7 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion)
(* Evaluate the assertion *)
let eval_assert cf (v : typed_value) : m_fun =
fun ctx ->
- cassert (v.ty = TLiteral TBool) meta "TODO: Error message";
+ sanity_check (v.ty = TLiteral TBool) meta;
(* We make a choice here: we could completely decouple the concrete and
* symbolic executions here but choose not to. In the case where we
* know the concrete value of the boolean we test, we use this value
@@ -178,8 +178,8 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion)
(* Delegate to the concrete evaluation function *)
eval_assertion_concrete config meta assertion cf ctx
| VSymbolic sv ->
- cassert (config.mode = SymbolicMode) meta "TODO: Error message";
- cassert (sv.sv_ty = TLiteral TBool) meta "TODO: Error message";
+ sanity_check(config.mode = SymbolicMode) meta;
+ sanity_check (sv.sv_ty = TLiteral TBool) meta;
(* We continue the execution as if the test had succeeded, and thus
* perform the symbolic expansion: sv ~~> true.
* We will of course synthesize an assertion in the generated code
@@ -194,7 +194,7 @@ let eval_assertion (config : config) (meta : Meta.meta) (assertion : assertion)
S.synthesize_assertion ctx v expr
| _ ->
craise
- meta ("Expected a boolean, got: " ^ typed_value_to_string meta ctx v)
+ meta ("Expected a boolean, got: " ^ typed_value_to_string ~meta:(Some meta) ctx v)
in
(* Compose and apply *)
comp eval_op eval_assert cf ctx
@@ -218,7 +218,7 @@ let set_discriminant (config : config) (meta : Meta.meta) (p : place) (variant_i
("set_discriminant:" ^ "\n- p: " ^ place_to_string ctx p
^ "\n- variant id: "
^ VariantId.to_string variant_id
- ^ "\n- initial context:\n" ^ eval_ctx_to_string meta ctx));
+ ^ "\n- initial context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
(* Access the value *)
let access = Write in
let cc = update_ctx_along_read_place config meta access p in
@@ -259,7 +259,7 @@ let set_discriminant (config : config) (meta : Meta.meta) (p : place) (variant_i
in
assign_to_place config meta bottom_v p (cf Unit) ctx
| _, VSymbolic _ ->
- cassert (config.mode = SymbolicMode) meta "The Config mode should be SymbolicMode";
+ sanity_check (config.mode = SymbolicMode) meta;
(* This is a bit annoying: in theory we should expand the symbolic value
* then set the discriminant, because in the case the discriminant is
* exactly the one we set, the fields are left untouched, and in the
@@ -287,13 +287,13 @@ let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx)
*)
let get_assumed_function_return_type (meta : Meta.meta) (ctx : eval_ctx) (fid : assumed_fun_id)
(generics : generic_args) : ety =
- cassert (generics.trait_refs = []) meta "TODO: Error message";
+ sanity_check (generics.trait_refs = []) meta;
(* [Box::free] has a special treatment *)
match fid with
| BoxFree ->
- cassert (generics.regions = []) meta "TODO: Error message";
- cassert (List.length generics.types = 1) meta "TODO: Error message";
- cassert (generics.const_generics = []) meta "TODO: Error message";
+ sanity_check (generics.regions = []) meta;
+ sanity_check (List.length generics.types = 1) meta;
+ sanity_check (generics.const_generics = []) meta;
mk_unit_ty
| _ ->
(* Retrieve the function's signature *)
@@ -324,7 +324,7 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool)
(cf : typed_value option -> m_fun) : m_fun =
fun ctx ->
(* Debug *)
- log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string meta ctx));
+ log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
(* List the local variables, but the return variable *)
let ret_vid = VarId.zero in
@@ -377,7 +377,7 @@ let pop_frame (config : config) (meta : Meta.meta) (pop_return_value : bool)
log#ldebug
(lazy
("pop_frame: after dropping outer loans in local variables:\n"
- ^ eval_ctx_to_string meta ctx)))
+ ^ eval_ctx_to_string ~meta:(Some meta) ctx)))
in
(* Pop the frame - we remove the [Frame] delimiter, and reintroduce all
@@ -479,7 +479,7 @@ let eval_box_free (config : config) (meta : Meta.meta) (generics : generic_args)
(* Required type checking *)
let input_box = InterpreterPaths.read_place meta Write input_box_place ctx in
(let input_ty = ty_get_box input_box.ty in
- cassert (input_ty = boxed_ty)) meta "TODO: Error message";
+ sanity_check (input_ty = boxed_ty)) meta;
(* Drop the value *)
let cc = drop_value config meta input_box_place in
@@ -930,7 +930,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
(lazy
("\n**About to evaluate statement**: [\n"
^ statement_to_string_with_tab ctx st
- ^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string st.meta ctx ^ "\n\n"));
+ ^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string ~meta:(Some st.meta) ctx ^ "\n\n"));
(* Take a snapshot of the current context for the purpose of generating pretty names *)
let cc = S.cf_save_snapshot in
@@ -963,7 +963,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
log#ldebug
(lazy
("about to assign to place: " ^ place_to_string ctx p
- ^ "\n- Context:\n" ^ eval_ctx_to_string st.meta ctx));
+ ^ "\n- Context:\n" ^ eval_ctx_to_string ~meta:(Some st.meta) ctx));
match res with
| Error EPanic -> cf Panic ctx
| Ok rv -> (
@@ -1037,7 +1037,7 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
| SymbolicMode ->
(* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
* defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
- cassert (ty_no_regions global.ty) meta "TODO: Error message";
+ cassert (ty_no_regions global.ty) global.meta "Const globals should not contain regions";
(* Instantiate the type *)
(* There shouldn't be any reference to Self *)
let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in
@@ -1049,7 +1049,7 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
global.ty
in
- let sval = mk_fresh_symbolic_value ty in
+ let sval = mk_fresh_symbolic_value global.meta ty in
let cc =
assign_to_place config global.meta (mk_typed_value_from_symbolic_value sval) dest
in
@@ -1250,7 +1250,7 @@ and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta)
| Some body -> body
in
(* TODO: we need to normalize the types if we want to correctly support traits *)
- cassert (generics.trait_refs = []) body.meta "Traits are not supported yet TODO: error message";
+ cassert (generics.trait_refs = []) body.meta "Traits are not supported yet in concrete mode";
(* There shouldn't be any reference to Self *)
let tr_self = UnknownTrait __FUNCTION__ in
let subst =
@@ -1259,7 +1259,7 @@ and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta)
let locals, body_st = Subst.fun_body_substitute_in_body subst body in
(* Evaluate the input operands *)
- cassert (List.length args = body.arg_count) body.meta "TODO: Error message";
+ sanity_check(List.length args = body.arg_count) body.meta;
let cc = eval_operands config body.meta args in
(* Push a frame delimiter - we use {!comp_transmit} to transmit the result
@@ -1295,7 +1295,7 @@ and eval_transparent_function_call_concrete (config : config) (meta : Meta.meta)
let cc = comp cc (push_uninitialized_vars meta locals) in
(* Execute the function body *)
- let cc = comp cc (eval_function_body config meta body_st) in
+ let cc = comp cc (eval_function_body config body_st) in
(* Pop the stack frame and move the return value to its destination *)
let cf_finish cf res =
@@ -1387,11 +1387,11 @@ and eval_function_call_symbolic_from_inst_sig (config : config) (meta : Meta.met
* be fed to functions (i.e., symbolic values output from function return
* values and which contain borrows of borrows can't be used as function
* inputs *)
- cassert (
+ sanity_check (
List.for_all
(fun arg ->
not (value_has_ret_symbolic_value_with_borrow_under_mut ctx arg))
- args) meta "The input argument should not contain symbolic values that can't be fed to functions TODO: error message";
+ args) meta;
(* Initialize the abstractions and push them in the context.
* First, we define the function which, given an initialized, empty
@@ -1538,7 +1538,7 @@ and eval_assumed_function_call_symbolic (config : config) (meta : Meta.meta) (fi
regions_hierarchy inst_sig generics None args dest cf ctx
(** Evaluate a statement seen as a function body *)
-and eval_function_body (config : config) (meta : Meta.meta) (body : statement) : st_cm_fun =
+and eval_function_body (config : config) (body : statement) : st_cm_fun =
fun cf ctx ->
log#ldebug (lazy "eval_function_body:");
let cc = eval_statement config body in
@@ -1550,7 +1550,7 @@ and eval_function_body (config : config) (meta : Meta.meta) (body : statement) :
* checking the invariants *)
let cc = greedy_expand_symbolic_values config body.meta in
(* Sanity check *)
- let cc = comp_check_ctx cc (Invariants.check_invariants meta) in (* Check if right meta *)
+ let cc = comp_check_ctx cc (Invariants.check_invariants body.meta) in (* Check if right meta *)
(* Continue *)
cc (cf res)
in
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index 519d2c8e..13743cb1 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -48,4 +48,4 @@ val create_push_abstractions_from_abs_region_groups :
val eval_statement : config -> statement -> st_cm_fun
(** Evaluate a statement seen as a function body *)
-val eval_function_body : config -> Meta.meta -> statement -> st_cm_fun
+val eval_function_body : config -> statement -> st_cm_fun
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index be8400f7..a24cd543 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -20,7 +20,7 @@ let log = Logging.interpreter_log
let get_cf_ctx_no_synth (meta : Meta.meta) (f : cm_fun) (ctx : eval_ctx) : eval_ctx =
let nctx = ref None in
let cf ctx =
- cassert (!nctx = None) meta "TODO: error message";
+ sanity_check (!nctx = None) meta;
nctx := Some ctx;
None
in
@@ -62,9 +62,9 @@ let statement_to_string ctx = Print.EvalCtx.statement_to_string ctx "" " "
let statement_to_string_with_tab ctx =
Print.EvalCtx.statement_to_string ctx " " " "
-let env_elem_to_string meta ctx = Print.EvalCtx.env_elem_to_string meta ctx "" " "
-let env_to_string meta ctx env = eval_ctx_to_string meta { ctx with env }
-let abs_to_string meta ctx = Print.EvalCtx.abs_to_string meta ctx "" " "
+let env_elem_to_string meta ctx = Print.EvalCtx.env_elem_to_string ~meta:(Some meta) ctx "" " "
+let env_to_string meta ctx env = eval_ctx_to_string ~meta:(Some meta) { ctx with env }
+let abs_to_string meta ctx = Print.EvalCtx.abs_to_string ~meta:(Some meta) ctx "" " "
let same_symbolic_id (sv0 : symbolic_value) (sv1 : symbolic_value) : bool =
sv0.sv_id = sv1.sv_id
@@ -85,12 +85,12 @@ let mk_fresh_symbolic_value (meta : Meta.meta) (ty : ty) : symbolic_value =
svalue
let mk_fresh_symbolic_value_from_no_regions_ty (meta : Meta.meta) (ty : ty) : symbolic_value =
- cassert (ty_no_regions ty) meta "TODO: error message";
+ sanity_check (ty_no_regions ty) meta;
mk_fresh_symbolic_value meta ty
(** Create a fresh symbolic value *)
let mk_fresh_symbolic_typed_value (meta : Meta.meta) (rty : ty) : typed_value =
- cassert (ty_is_rty rty) meta "TODO: error message";
+ sanity_check (ty_is_rty rty) meta;
let ty = Substitute.erase_regions rty in
(* Generate the fresh a symbolic value *)
let value = mk_fresh_symbolic_value meta rty in
@@ -98,7 +98,7 @@ let mk_fresh_symbolic_typed_value (meta : Meta.meta) (rty : ty) : typed_value =
{ value; ty }
let mk_fresh_symbolic_typed_value_from_no_regions_ty (meta : Meta.meta) (ty : ty) : typed_value =
- cassert (ty_no_regions ty) meta "TODO: error message";
+ sanity_check (ty_no_regions ty) meta;
mk_fresh_symbolic_typed_value meta ty
(** Create a typed value from a symbolic value. *)
@@ -127,7 +127,7 @@ let mk_aproj_loans_value_from_symbolic_value (regions : RegionId.Set.t)
(** Create a borrows projector from a symbolic value *)
let mk_aproj_borrows_from_symbolic_value (meta : Meta.meta) (proj_regions : RegionId.Set.t)
(svalue : symbolic_value) (proj_ty : ty) : aproj =
- cassert (ty_is_rty proj_ty) meta "TODO: error message";
+ sanity_check (ty_is_rty proj_ty) meta;
if ty_has_regions_in_set proj_regions proj_ty then
AProjBorrows (svalue, proj_ty)
else AIgnoredProjBorrows
@@ -153,7 +153,7 @@ let remove_borrow_from_asb (meta : Meta.meta) (bid : BorrowId.id) (asb : abstrac
false))
asb
in
- cassert (!removed = 1) meta "TODO: error message";
+ sanity_check (!removed = 1) meta;
asb
(** We sometimes need to return a value whose type may vary depending on
@@ -499,8 +499,8 @@ let instantiate_fun_sig (meta : Meta.meta) (ctx : eval_ctx) (generics : generic_
(* Generate the type substitution
Note that for now we don't support instantiating the type parameters with
types containing regions. *)
- cassert (List.for_all TypesUtils.ty_no_regions generics.types) meta "TODO: error message";
- cassert (TypesUtils.trait_instance_id_no_regions tr_self) meta "TODO: error message";
+ sanity_check (List.for_all TypesUtils.ty_no_regions generics.types) meta;
+ sanity_check (TypesUtils.trait_instance_id_no_regions tr_self) meta;
let tsubst =
Substitute.make_type_subst_from_vars sg.generics.types generics.types
in
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 50f008b8..9b389ba5 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -55,7 +55,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
(* Link all the id representants to a borrow information *)
let borrows_infos : borrow_info BorrowId.Map.t ref = ref BorrowId.Map.empty in
let context_to_string () : string =
- eval_ctx_to_string meta ctx ^ "- representants:\n"
+ eval_ctx_to_string ~meta:(Some meta) ctx ^ "- representants:\n"
^ ids_reprs_to_string " " !ids_reprs
^ "\n- info:\n"
^ borrows_infos_to_string " " !borrows_infos
@@ -77,12 +77,12 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
let infos = !borrows_infos in
(* Use the first borrow id as representant *)
let repr_bid = BorrowId.Set.min_elt bids in
- cassert (not (BorrowId.Map.mem repr_bid infos)) meta "TODO: Error message";
+ sanity_check (not (BorrowId.Map.mem repr_bid infos)) meta;
(* Insert the mappings to the representant *)
let reprs =
BorrowId.Set.fold
(fun bid reprs ->
- cassert (not (BorrowId.Map.mem bid reprs)) meta "TODO: Error message";
+ sanity_check (not (BorrowId.Map.mem bid reprs)) meta;
BorrowId.Map.add bid repr_bid reprs)
bids reprs
in
@@ -212,10 +212,10 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
| RShared, (BShared | BReserved) | RMut, BMut -> ()
| _ -> craise meta "Invariant not satisfied");
(* A reserved borrow can't point to a value inside an abstraction *)
- cassert (kind <> BReserved || not info.loan_in_abs) meta "A reserved borrow can't point to a value inside an abstraction";
+ sanity_check (kind <> BReserved || not info.loan_in_abs) meta;
(* Insert the borrow id *)
let borrow_ids = info.borrow_ids in
- cassert (not (BorrowId.Set.mem bid borrow_ids)) meta "TODO: Error message";
+ sanity_check (not (BorrowId.Set.mem bid borrow_ids)) meta;
let info = { info with borrow_ids = BorrowId.Set.add bid borrow_ids } in
(* Update the info in the map *)
update_info bid info
@@ -270,7 +270,7 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
List.iter
(fun (rkind, bid) ->
let info = find_info bid in
- cassert (info.loan_kind = rkind) meta "Not all the ignored loans are present at the proper place")
+ sanity_check (info.loan_kind = rkind) meta)
!ignored_loans;
(* Then, check the borrow infos *)
@@ -278,11 +278,11 @@ let check_loans_borrows_relation_invariant (meta : Meta.meta) (ctx : eval_ctx) :
(fun _ info ->
(* Note that we can't directly compare the sets - I guess they are
* different depending on the order in which we add the elements... *)
- cassert (
+ sanity_check (
BorrowId.Set.elements info.loan_ids
- = BorrowId.Set.elements info.borrow_ids) meta "TODO: Error message";
+ = BorrowId.Set.elements info.borrow_ids) meta;
match info.loan_kind with
- | RMut -> cassert (BorrowId.Set.cardinal info.loan_ids = 1) meta "TODO: Error message"
+ | RMut -> sanity_check (BorrowId.Set.cardinal info.loan_ids = 1) meta
| RShared -> ())
!borrows_infos
@@ -297,7 +297,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
method! visit_VBottom info =
(* No ⊥ inside borrowed values *)
- cassert (Config.allow_bottom_below_borrow || not info.outer_borrow) meta "There should be no ⊥ inside borrowed values"
+ sanity_check (Config.allow_bottom_below_borrow || not info.outer_borrow) meta
method! visit_ABottom _info =
(* ⊥ inside an abstraction is not the same as in a regular value *)
@@ -310,7 +310,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
| VSharedLoan (_, _) -> set_outer_shared info
| VMutLoan _ ->
(* No mutable loan inside a shared loan *)
- cassert (not info.outer_shared) meta "There should be no mutable loan inside a shared loan";
+ sanity_check (not info.outer_shared) meta;
set_outer_mut info
in
(* Continue exploring *)
@@ -322,7 +322,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
match bc with
| VSharedBorrow _ -> set_outer_shared info
| VReservedMutBorrow _ ->
- cassert (not info.outer_borrow) meta "TODO: Error message";
+ sanity_check (not info.outer_borrow) meta;
set_outer_shared info
| VMutBorrow (_, _) -> set_outer_mut info
in
@@ -369,7 +369,7 @@ let check_borrowed_values_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
let check_literal_type (meta : Meta.meta) (cv : literal) (ty : literal_type) : unit =
match (cv, ty) with
- | VScalar sv, TInteger int_ty -> cassert (sv.int_ty = int_ty) meta "TODO: Error message"
+ | VScalar sv, TInteger int_ty -> sanity_check (sv.int_ty = int_ty) meta
| VBool _, TBool | VChar _, TChar -> ()
| _ -> craise meta "Erroneous typing"
@@ -393,17 +393,17 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
method! visit_EBinding info binder v =
(* We also check that the regions are erased *)
- cassert (ty_is_ety v.ty) meta "The regions should be erased";
+ sanity_check (ty_is_ety v.ty) meta;
super#visit_EBinding info binder v
method! visit_symbolic_value inside_abs v =
(* Check that the types have regions *)
- cassert (ty_is_rty v.sv_ty) meta "The types should have regions";
+ sanity_check (ty_is_rty v.sv_ty) meta;
super#visit_symbolic_value inside_abs v
method! visit_typed_value info tv =
(* Check that the types have erased regions *)
- cassert (ty_is_ety tv.ty) meta "The types should have erased regions";
+ sanity_check (ty_is_ety tv.ty) meta;
(* Check the current pair (value, type) *)
(match (tv.value, tv.ty) with
| VLiteral cv, TLiteral ty -> check_literal_type meta cv ty
@@ -413,40 +413,40 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
* parameters, etc. *)
let def = ctx_lookup_type_decl ctx def_id in
(* Check the number of parameters *)
- cassert (
- List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message";
- cassert (List.length generics.types = List.length def.generics.types) meta "TODO: Error message";
+ sanity_check (
+ List.length generics.regions = List.length def.generics.regions) meta;
+ sanity_check (List.length generics.types = List.length def.generics.types) meta;
(* Check that the variant id is consistent *)
(match (av.variant_id, def.kind) with
| Some variant_id, Enum variants ->
- cassert (VariantId.to_int variant_id < List.length variants) meta "The variant id should be consistent"
+ sanity_check (VariantId.to_int variant_id < List.length variants) meta
| None, Struct _ -> ()
| _ -> craise meta "Erroneous typing");
(* Check that the field types are correct *)
let field_types =
- AssociatedTypes.type_decl_get_inst_norm_field_etypes ctx def
+ AssociatedTypes.type_decl_get_inst_norm_field_etypes meta ctx def
av.variant_id generics
in
let fields_with_types = List.combine av.field_values field_types in
List.iter
- (fun ((v, ty) : typed_value * ty) -> cassert (v.ty = ty) meta "The field types are not correct")
+ (fun ((v, ty) : typed_value * ty) -> sanity_check (v.ty = ty) meta)
fields_with_types
(* Tuple case *)
| VAdt av, TAdt (TTuple, generics) ->
- cassert (generics.regions = []) meta "TODO: Error message";
- cassert (generics.const_generics = []) meta "TODO: Error message";
- cassert (av.variant_id = None) meta "TODO: Error message";
+ sanity_check (generics.regions = []) meta;
+ sanity_check (generics.const_generics = []) meta;
+ sanity_check (av.variant_id = None) meta;
(* Check that the fields have the proper values - and check that there
* are as many fields as field types at the same time *)
let fields_with_types =
List.combine av.field_values generics.types
in
List.iter
- (fun ((v, ty) : typed_value * ty) -> cassert (v.ty = ty) meta "The fields does not have the proper values or there are not as many fields as field types at the same time TODO: error message")
+ (fun ((v, ty) : typed_value * ty) -> sanity_check (v.ty = ty) meta)
fields_with_types
(* Assumed type case *)
| VAdt av, TAdt (TAssumed aty_id, generics) -> (
- cassert (av.variant_id = None) meta "TODO: Error message";
+ sanity_check (av.variant_id = None) meta;
match
( aty_id,
av.field_values,
@@ -456,20 +456,20 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
with
(* Box *)
| TBox, [ inner_value ], [], [ inner_ty ], [] ->
- cassert (inner_value.ty = inner_ty) meta "TODO: Error message"
+ sanity_check (inner_value.ty = inner_ty) meta
| TArray, inner_values, _, [ inner_ty ], [ cg ] ->
(* *)
- cassert (
+ sanity_check (
List.for_all
(fun (v : typed_value) -> v.ty = inner_ty)
- inner_values) meta "TODO: Error message";
+ inner_values) meta;
(* The length is necessarily concrete *)
let len =
(ValuesUtils.literal_as_scalar
(TypesUtils.const_generic_as_literal cg))
.value
in
- cassert (Z.of_int (List.length inner_values) = len) meta "TODO: Error message"
+ sanity_check (Z.of_int (List.length inner_values) = len) meta
| (TSlice | TStr), _, _, _, _ -> craise meta "Unexpected"
| _ -> craise meta "Erroneous type")
| VBottom, _ -> (* Nothing to check *) ()
@@ -481,27 +481,27 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
match glc with
| Concrete (VSharedLoan (_, sv))
| Abstract (ASharedLoan (_, sv, _)) ->
- cassert (sv.ty = ref_ty) meta "TODO: Error message"
+ sanity_check (sv.ty = ref_ty) meta
| _ -> craise meta "Inconsistent context")
| VMutBorrow (_, bv), RMut ->
- cassert (
+ sanity_check (
(* Check that the borrowed value has the proper type *)
- bv.ty = ref_ty) meta "TODO: Error message"
+ bv.ty = ref_ty) meta
| _ -> craise meta "Erroneous typing")
| VLoan lc, ty -> (
match lc with
- | VSharedLoan (_, sv) -> cassert (sv.ty = ty) meta "TODO: Error message"
+ | VSharedLoan (_, sv) -> sanity_check (sv.ty = ty) meta
| VMutLoan bid -> (
(* Lookup the borrowed value to check it has the proper type *)
let glc = lookup_borrow meta ek_all bid ctx in
match glc with
- | Concrete (VMutBorrow (_, bv)) -> cassert (bv.ty = ty) meta "The borrowed value does not have the proper type"
+ | Concrete (VMutBorrow (_, bv)) -> sanity_check (bv.ty = ty) meta
| Abstract (AMutBorrow (_, sv)) ->
- cassert (Substitute.erase_regions sv.ty = ty) meta "The borrowed value does not have the proper type"
+ sanity_check (Substitute.erase_regions sv.ty = ty) meta
| _ -> craise meta "Inconsistent context"))
| VSymbolic sv, ty ->
let ty' = Substitute.erase_regions sv.sv_ty in
- cassert (ty' = ty) meta "TODO: Error message"
+ sanity_check (ty' = ty) meta
| _ -> craise meta "Erroneous typing");
(* Continue exploring to inspect the subterms *)
super#visit_typed_value info tv
@@ -516,7 +516,7 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
* *)
method! visit_typed_avalue info atv =
(* Check that the types have regions *)
- cassert (ty_is_rty atv.ty) meta "The types should have regions";
+ sanity_check (ty_is_rty atv.ty) meta;
(* Check the current pair (value, type) *)
(match (atv.value, atv.ty) with
(* ADT case *)
@@ -525,43 +525,43 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
* parameters, etc. *)
let def = ctx_lookup_type_decl ctx def_id in
(* Check the number of parameters *)
- cassert (
- List.length generics.regions = List.length def.generics.regions) meta "TODO: Error message";
- cassert (List.length generics.types = List.length def.generics.types) meta "TODO: Error message";
- cassert (
+ sanity_check (
+ List.length generics.regions = List.length def.generics.regions) meta;
+ sanity_check (List.length generics.types = List.length def.generics.types) meta;
+ sanity_check (
List.length generics.const_generics
- = List.length def.generics.const_generics) meta "TODO: Error message";
+ = List.length def.generics.const_generics) meta;
(* Check that the variant id is consistent *)
(match (av.variant_id, def.kind) with
| Some variant_id, Enum variants ->
- cassert (VariantId.to_int variant_id < List.length variants) meta "The variant id should be consistent"
+ sanity_check (VariantId.to_int variant_id < List.length variants) meta
| None, Struct _ -> ()
| _ -> craise meta "Erroneous typing");
(* Check that the field types are correct *)
let field_types =
- AssociatedTypes.type_decl_get_inst_norm_field_rtypes ctx def
+ AssociatedTypes.type_decl_get_inst_norm_field_rtypes meta ctx def
av.variant_id generics
in
let fields_with_types = List.combine av.field_values field_types in
List.iter
- (fun ((v, ty) : typed_avalue * ty) -> cassert (v.ty = ty) meta "TODO: Error message")
+ (fun ((v, ty) : typed_avalue * ty) -> sanity_check (v.ty = ty) meta)
fields_with_types
(* Tuple case *)
| AAdt av, TAdt (TTuple, generics) ->
- cassert (generics.regions = []) meta "TODO: Error message";
- cassert (generics.const_generics = []) meta "TODO: Error message";
- cassert (av.variant_id = None) meta "TODO: Error message";
+ sanity_check (generics.regions = []) meta;
+ sanity_check (generics.const_generics = []) meta;
+ sanity_check (av.variant_id = None) meta;
(* Check that the fields have the proper values - and check that there
* are as many fields as field types at the same time *)
let fields_with_types =
List.combine av.field_values generics.types
in
List.iter
- (fun ((v, ty) : typed_avalue * ty) -> cassert (v.ty = ty) meta "The fields do not have the proper values or there are not as many fields as field types at the same time TODO: Error message")
+ (fun ((v, ty) : typed_avalue * ty) -> sanity_check (v.ty = ty) meta)
fields_with_types
(* Assumed type case *)
| AAdt av, TAdt (TAssumed aty_id, generics) -> (
- cassert (av.variant_id = None) meta "TODO: Error message";
+ sanity_check (av.variant_id = None) meta;
match
( aty_id,
av.field_values,
@@ -571,27 +571,27 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
with
(* Box *)
| TBox, [ boxed_value ], [], [ boxed_ty ], [] ->
- cassert (boxed_value.ty = boxed_ty) meta "TODO: Error message"
+ sanity_check (boxed_value.ty = boxed_ty) meta
| _ -> craise meta "Erroneous type")
| ABottom, _ -> (* Nothing to check *) ()
| ABorrow bc, TRef (_, ref_ty, rkind) -> (
match (bc, rkind) with
| AMutBorrow (_, av), RMut ->
(* Check that the child value has the proper type *)
- cassert (av.ty = ref_ty) meta "TODO: Error message"
+ sanity_check (av.ty = ref_ty) meta
| ASharedBorrow bid, RShared -> (
(* Lookup the borrowed value to check it has the proper type *)
let _, glc = lookup_loan meta ek_all bid ctx in
match glc with
| Concrete (VSharedLoan (_, sv))
| Abstract (ASharedLoan (_, sv, _)) ->
- cassert (sv.ty = Substitute.erase_regions ref_ty) meta "TODO: Error message"
+ sanity_check (sv.ty = Substitute.erase_regions ref_ty) meta
| _ -> craise meta "Inconsistent context")
- | AIgnoredMutBorrow (_opt_bid, av), RMut -> cassert (av.ty = ref_ty) meta "TODO: Error message"
+ | AIgnoredMutBorrow (_opt_bid, av), RMut -> sanity_check (av.ty = ref_ty) meta
| ( AEndedIgnoredMutBorrow { given_back; child; given_back_meta = _ },
RMut ) ->
- cassert (given_back.ty = ref_ty) meta "TODO: Error message";
- cassert (child.ty = ref_ty) meta "TODO: Error message"
+ sanity_check (given_back.ty = ref_ty) meta;
+ sanity_check (child.ty = ref_ty) meta
| AProjSharedBorrow _, RShared -> ()
| _ -> craise meta "Inconsistent context")
| ALoan lc, aty -> (
@@ -599,54 +599,54 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
| AMutLoan (bid, child_av) | AIgnoredMutLoan (Some bid, child_av)
-> (
let borrowed_aty = aloan_get_expected_child_type aty in
- cassert (child_av.ty = borrowed_aty) meta "TODO: Error message";
+ sanity_check (child_av.ty = borrowed_aty) meta;
(* Lookup the borrowed value to check it has the proper type *)
let glc = lookup_borrow meta ek_all bid ctx in
match glc with
| Concrete (VMutBorrow (_, bv)) ->
- cassert (bv.ty = Substitute.erase_regions borrowed_aty) meta "TODO: Error message"
+ sanity_check (bv.ty = Substitute.erase_regions borrowed_aty) meta
| Abstract (AMutBorrow (_, sv)) ->
- cassert (
+ sanity_check (
Substitute.erase_regions sv.ty
- = Substitute.erase_regions borrowed_aty) meta "TODO: Error message"
+ = Substitute.erase_regions borrowed_aty) meta
| _ -> craise meta "Inconsistent context")
| AIgnoredMutLoan (None, child_av) ->
let borrowed_aty = aloan_get_expected_child_type aty in
- cassert (child_av.ty = borrowed_aty) meta "TODO: Error message"
+ sanity_check (child_av.ty = borrowed_aty) meta
| ASharedLoan (_, sv, child_av) | AEndedSharedLoan (sv, child_av) ->
let borrowed_aty = aloan_get_expected_child_type aty in
- cassert (sv.ty = Substitute.erase_regions borrowed_aty) meta "TODO: Error message";
+ sanity_check (sv.ty = Substitute.erase_regions borrowed_aty) meta;
(* TODO: the type of aloans doesn't make sense, see above *)
- cassert (child_av.ty = borrowed_aty) meta "TODO: Error message"
+ sanity_check (child_av.ty = borrowed_aty) meta
| AEndedMutLoan { given_back; child; given_back_meta = _ }
| AEndedIgnoredMutLoan { given_back; child; given_back_meta = _ } ->
let borrowed_aty = aloan_get_expected_child_type aty in
- cassert (given_back.ty = borrowed_aty) meta "TODO: Error message";
- cassert (child.ty = borrowed_aty) meta "TODO: Error message"
+ sanity_check (given_back.ty = borrowed_aty) meta;
+ sanity_check (child.ty = borrowed_aty) meta
| AIgnoredSharedLoan child_av ->
- cassert (child_av.ty = aloan_get_expected_child_type aty) meta "TODO: Error message")
+ sanity_check (child_av.ty = aloan_get_expected_child_type aty) meta)
| ASymbolic aproj, ty -> (
let ty1 = Substitute.erase_regions ty in
match aproj with
| AProjLoans (sv, _) ->
let ty2 = Substitute.erase_regions sv.sv_ty in
- cassert (ty1 = ty2) meta "TODO: Error message";
+ sanity_check (ty1 = ty2) meta;
(* Also check that the symbolic values contain regions of interest -
* otherwise they should have been reduced to [_] *)
let abs = Option.get info in
- cassert (ty_has_regions_in_set abs.regions sv.sv_ty) meta "The symbolic values should contain regions of interest or they should have been reduced to [] TODO: error message"
+ sanity_check (ty_has_regions_in_set abs.regions sv.sv_ty) meta
| AProjBorrows (sv, proj_ty) ->
let ty2 = Substitute.erase_regions sv.sv_ty in
- cassert (ty1 = ty2) meta "TODO: Error message";
+ sanity_check (ty1 = ty2) meta;
(* Also check that the symbolic values contain regions of interest -
* otherwise they should have been reduced to [_] *)
let abs = Option.get info in
- cassert (ty_has_regions_in_set abs.regions proj_ty) meta "The symbolic values should contain regions of interest or they should have been reduced to [] TODO: error message"
+ sanity_check (ty_has_regions_in_set abs.regions proj_ty) meta
| AEndedProjLoans (_msv, given_back_ls) ->
List.iter
(fun (_, proj) ->
match proj with
- | AProjBorrows (_sv, ty') -> cassert (ty' = ty) meta "TODO: Error message"
+ | AProjBorrows (_sv, ty') -> sanity_check (ty' = ty) meta
| AEndedProjBorrows _ | AIgnoredProjBorrows -> ()
| _ -> craise meta "Unexpected")
given_back_ls
@@ -657,7 +657,7 @@ let check_typing_invariant (meta : Meta.meta) (ctx : eval_ctx) : unit =
(lazy
("Erroneous typing:" ^ "\n- raw value: " ^ show_typed_avalue atv
^ "\n- value: "
- ^ typed_avalue_to_string meta ctx atv
+ ^ typed_avalue_to_string ~meta:(Some meta) ctx atv
^ "\n- type: " ^ ty_to_string ctx atv.ty));
craise meta "Erroneous typing");
(* Continue exploring to inspect the subterms *)
@@ -766,15 +766,15 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
*)
(* A symbolic value can't be both in the regular environment and inside
* projectors of borrows in abstractions *)
- cassert (info.env_count = 0 || info.aproj_borrows = []) meta "A symbolic value can't be both in the regular environment and inside projectors of borrows in abstractions";
+ sanity_check (info.env_count = 0 || info.aproj_borrows = []) meta;
(* A symbolic value containing borrows can't be duplicated (i.e., copied):
* it must be expanded first *)
if ty_has_borrows ctx.type_ctx.type_infos info.ty then
- cassert (info.env_count <= 1) meta "A symbolic value containing borrows can't be duplicated (i.e., copied): it must be expanded first";
+ sanity_check (info.env_count <= 1) meta;
(* A duplicated symbolic value is necessarily primitively copyable *)
- cassert (info.env_count <= 1 || ty_is_primitively_copyable info.ty) meta "A duplicated symbolic value should necessarily be primitively copyable";
+ sanity_check (info.env_count <= 1 || ty_is_primitively_copyable info.ty) meta;
- cassert (info.aproj_borrows = [] || info.aproj_loans <> []) meta "TODO: Error message";
+ sanity_check (info.aproj_borrows = [] || info.aproj_loans <> []) meta;
(* At the same time:
* - check that the loans don't intersect
* - compute the set of regions for which we project loans
@@ -786,7 +786,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
let regions =
RegionId.Set.fold
(fun rid regions ->
- cassert (not (RegionId.Set.mem rid regions)) meta "The loan projectors should contain the region projectors";
+ sanity_check (not (RegionId.Set.mem rid regions)) meta;
RegionId.Set.add rid regions)
regions linfo.regions
in
@@ -796,8 +796,8 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
(* Check that the union of the loan projectors contains the borrow projections. *)
List.iter
(fun binfo ->
- cassert (
- projection_contains meta info.ty loan_regions binfo.proj_ty binfo.regions) meta "The union of the loan projectors should contain the borrow projections")
+ sanity_check (
+ projection_contains meta info.ty loan_regions binfo.proj_ty binfo.regions) meta)
info.aproj_borrows;
()
in
@@ -806,7 +806,7 @@ let check_symbolic_values (meta : Meta.meta) (ctx : eval_ctx) : unit =
let check_invariants (meta : Meta.meta) (ctx : eval_ctx) : unit =
if !Config.sanity_checks then (
- log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string meta ctx));
+ log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx));
check_loans_borrows_relation_invariant meta ctx;
check_borrowed_values_invariant meta ctx;
check_typing_invariant meta ctx;
diff --git a/compiler/Main.ml b/compiler/Main.ml
index f860bec8..f8765247 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -113,7 +113,7 @@ let () =
Arg.Clear lean_gen_lakefile,
" Generate a default lakefile.lean (Lean only)" );
("-print-llbc", Arg.Set print_llbc, " Print the imported LLBC");
- ("-abort-on-error", Arg.Set fail_hard, " Fail hard (fail on first error) in case of error");
+ ("-abort-on-error", Arg.Set fail_hard, "Abort on the first encountered error");
( "-tuple-nested-proj",
Arg.Set use_nested_tuple_projectors,
" Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 3ea9c777..c10dbf5d 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -215,11 +215,11 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl =
inherit [_] map_statement as super
method! visit_Loop entered_loop loop =
- cassert (not entered_loop) st.meta "TODO: error message";
+ cassert (not entered_loop) st.meta "Nested loops are not supported yet";
super#visit_Loop true loop
method! visit_Break _ i =
- cassert (i = 0) st.meta "TODO: error message";
+ cassert (i = 0) st.meta "Breaks to outer loops are not supported yet";
nst.content
end
in
@@ -234,7 +234,7 @@ let remove_loop_breaks (crate : crate) (f : fun_decl) : fun_decl =
method! visit_Sequence env st1 st2 =
match st1.content with
| Loop _ ->
- cassert (statement_has_no_loop_break_continue st2) st2.meta "TODO: error message";
+ sanity_check (statement_has_no_loop_break_continue st2) st2.meta;
(replace_breaks_with st1 st2).content
| _ -> super#visit_Sequence env st1 st2
end
@@ -393,7 +393,6 @@ let remove_shallow_borrows (crate : crate) (f : fun_decl) : fun_decl =
let body = filter_visitor#visit_statement () body in
(* Check that the filtered variables completely disappeared from the body *)
- (* let statement = crate in *)
let check_visitor =
object
inherit [_] iter_statement as super
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 85e7eaf6..47ae9b79 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -43,12 +43,12 @@ module Values = struct
* typed_avalue_to_string. At some point we had done it, because [typed_value]
* and [typed_avalue] were instances of the same general type [g_typed_value],
* but then we removed this general type because it proved to be a bad idea. *)
- let rec typed_value_to_string (meta : Meta.meta) (env : fmt_env) (v : typed_value) : string =
+ let rec typed_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (v : typed_value) : string =
match v.value with
| VLiteral cv -> literal_to_string cv
| VAdt av -> (
let field_values =
- List.map (typed_value_to_string meta env) av.field_values
+ List.map (typed_value_to_string~meta:meta env) av.field_values
in
match v.ty with
| TAdt (TTuple, _) ->
@@ -83,28 +83,28 @@ module Values = struct
| TArray, _ ->
(* Happens when we aggregate values *)
"@Array[" ^ String.concat ", " field_values ^ "]"
- | _ -> craise meta ("Inconsistent value: " ^ show_typed_value v)
+ | _ -> craise_opt_meta meta ("Inconsistent value: " ^ show_typed_value v)
)
- | _ -> craise meta "Inconsistent typed value")
+ | _ -> craise_opt_meta meta "Inconsistent typed value")
| VBottom -> "⊥ : " ^ ty_to_string env v.ty
- | VBorrow bc -> borrow_content_to_string meta env bc
- | VLoan lc -> loan_content_to_string meta env lc
+ | VBorrow bc -> borrow_content_to_string ~meta:meta env bc
+ | VLoan lc -> loan_content_to_string ~meta:meta env lc
| VSymbolic s -> symbolic_value_to_string env s
- and borrow_content_to_string (meta : Meta.meta) (env : fmt_env) (bc : borrow_content) : string =
+ and borrow_content_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (bc : borrow_content) : string =
match bc with
| VSharedBorrow bid -> "shared_borrow@" ^ BorrowId.to_string bid
| VMutBorrow (bid, tv) ->
"mut_borrow@" ^ BorrowId.to_string bid ^ " ("
- ^ typed_value_to_string meta env tv
+ ^ typed_value_to_string ~meta:meta env tv
^ ")"
| VReservedMutBorrow bid -> "reserved_borrow@" ^ BorrowId.to_string bid
- and loan_content_to_string (meta : Meta.meta) (env : fmt_env) (lc : loan_content) : string =
+ and loan_content_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (lc : loan_content) : string =
match lc with
| VSharedLoan (loans, v) ->
let loans = BorrowId.Set.to_string None loans in
- "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string meta env v ^ ")"
+ "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string ~meta:meta env v ^ ")"
| VMutLoan bid -> "ml@" ^ BorrowId.to_string bid
let abstract_shared_borrow_to_string (env : fmt_env)
@@ -142,11 +142,11 @@ module Values = struct
| AEndedProjBorrows _mv -> "_"
| AIgnoredProjBorrows -> "_"
- let rec typed_avalue_to_string (meta : Meta.meta) (env : fmt_env) (v : typed_avalue) : string =
+ let rec typed_avalue_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (v : typed_avalue) : string =
match v.value with
| AAdt av -> (
let field_values =
- List.map (typed_avalue_to_string meta env) av.field_values
+ List.map (typed_avalue_to_string ~meta:meta env) av.field_values
in
match v.ty with
| TAdt (TTuple, _) ->
@@ -178,75 +178,75 @@ module Values = struct
(* Assumed type *)
match (aty, field_values) with
| TBox, [ bv ] -> "@Box(" ^ bv ^ ")"
- | _ -> craise meta "Inconsistent value")
- | _ -> craise meta "Inconsistent typed value")
+ | _ -> craise_opt_meta meta "Inconsistent value")
+ | _ -> craise_opt_meta meta "Inconsistent typed value")
| ABottom -> "⊥ : " ^ ty_to_string env v.ty
- | ABorrow bc -> aborrow_content_to_string meta env bc
- | ALoan lc -> aloan_content_to_string meta env lc
+ | ABorrow bc -> aborrow_content_to_string ~meta:meta env bc
+ | ALoan lc -> aloan_content_to_string ~meta:meta env lc
| ASymbolic s -> aproj_to_string env s
| AIgnored -> "_"
- and aloan_content_to_string (meta : Meta.meta) (env : fmt_env) (lc : aloan_content) : string =
+ and aloan_content_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (lc : aloan_content) : string =
match lc with
| AMutLoan (bid, av) ->
"@mut_loan(" ^ BorrowId.to_string bid ^ ", "
- ^ typed_avalue_to_string meta env av
+ ^ typed_avalue_to_string ~meta:meta env av
^ ")"
| ASharedLoan (loans, v, av) ->
let loans = BorrowId.Set.to_string None loans in
"@shared_loan(" ^ loans ^ ", "
- ^ typed_value_to_string meta env v
+ ^ typed_value_to_string ~meta:meta env v
^ ", "
- ^ typed_avalue_to_string meta env av
+ ^ typed_avalue_to_string ~meta:meta env av
^ ")"
| AEndedMutLoan ml ->
"@ended_mut_loan{"
- ^ typed_avalue_to_string meta env ml.child
+ ^ typed_avalue_to_string ~meta:meta env ml.child
^ "; "
- ^ typed_avalue_to_string meta env ml.given_back
+ ^ typed_avalue_to_string ~meta:meta env ml.given_back
^ " }"
| AEndedSharedLoan (v, av) ->
"@ended_shared_loan("
- ^ typed_value_to_string meta env v
+ ^ typed_value_to_string ~meta:meta env v
^ ", "
- ^ typed_avalue_to_string meta env av
+ ^ typed_avalue_to_string ~meta:meta env av
^ ")"
| AIgnoredMutLoan (opt_bid, av) ->
"@ignored_mut_loan("
^ option_to_string BorrowId.to_string opt_bid
^ ", "
- ^ typed_avalue_to_string meta env av
+ ^ typed_avalue_to_string ~meta:meta env av
^ ")"
| AEndedIgnoredMutLoan ml ->
"@ended_ignored_mut_loan{ "
- ^ typed_avalue_to_string meta env ml.child
+ ^ typed_avalue_to_string ~meta:meta env ml.child
^ "; "
- ^ typed_avalue_to_string meta env ml.given_back
+ ^ typed_avalue_to_string ~meta:meta env ml.given_back
^ "}"
| AIgnoredSharedLoan sl ->
- "@ignored_shared_loan(" ^ typed_avalue_to_string meta env sl ^ ")"
+ "@ignored_shared_loan(" ^ typed_avalue_to_string ~meta:meta env sl ^ ")"
- and aborrow_content_to_string (meta : Meta.meta) (env : fmt_env) (bc : aborrow_content) : string
+ and aborrow_content_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (bc : aborrow_content) : string
=
match bc with
| AMutBorrow (bid, av) ->
"mb@" ^ BorrowId.to_string bid ^ " ("
- ^ typed_avalue_to_string meta env av
+ ^ typed_avalue_to_string ~meta:meta env av
^ ")"
| ASharedBorrow bid -> "sb@" ^ BorrowId.to_string bid
| AIgnoredMutBorrow (opt_bid, av) ->
"@ignored_mut_borrow("
^ option_to_string BorrowId.to_string opt_bid
^ ", "
- ^ typed_avalue_to_string meta env av
+ ^ typed_avalue_to_string ~meta:meta env av
^ ")"
| AEndedMutBorrow (_mv, child) ->
- "@ended_mut_borrow(" ^ typed_avalue_to_string meta env child ^ ")"
+ "@ended_mut_borrow(" ^ typed_avalue_to_string ~meta:meta env child ^ ")"
| AEndedIgnoredMutBorrow { child; given_back; given_back_meta = _ } ->
"@ended_ignored_mut_borrow{ "
- ^ typed_avalue_to_string meta env child
+ ^ typed_avalue_to_string ~meta:meta env child
^ "; "
- ^ typed_avalue_to_string meta env given_back
+ ^ typed_avalue_to_string ~meta:meta env given_back
^ ")"
| AEndedSharedBorrow -> "@ended_shared_borrow"
| AProjSharedBorrow sb ->
@@ -276,11 +276,11 @@ module Values = struct
^ ")"
| Identity -> "Identity"
- let abs_to_string (meta : Meta.meta) (env : fmt_env) (verbose : bool) (indent : string)
+ let abs_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (verbose : bool) (indent : string)
(indent_incr : string) (abs : abs) : string =
let indent2 = indent ^ indent_incr in
let avs =
- List.map (fun av -> indent2 ^ typed_avalue_to_string meta env av) abs.avalues
+ List.map (fun av -> indent2 ^ typed_avalue_to_string ~meta:meta env av) abs.avalues
in
let avs = String.concat ",\n" avs in
let kind =
@@ -323,7 +323,7 @@ module Contexts = struct
| BVar b -> var_binder_to_string env b
| BDummy bid -> dummy_var_id_to_string bid
- let env_elem_to_string (meta : Meta.meta) (env : fmt_env) (verbose : bool)
+ let env_elem_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (verbose : bool)
(with_var_types : bool) (indent : string) (indent_incr : string)
(ev : env_elem) : string =
match ev with
@@ -332,17 +332,17 @@ module Contexts = struct
let ty =
if with_var_types then " : " ^ ty_to_string env tv.ty else ""
in
- indent ^ bv ^ ty ^ " -> " ^ typed_value_to_string meta env tv ^ " ;"
- | EAbs abs -> abs_to_string meta env verbose indent indent_incr abs
- | EFrame -> craise meta "Can't print a Frame element"
+ indent ^ bv ^ ty ^ " -> " ^ typed_value_to_string ~meta:meta env tv ^ " ;"
+ | EAbs abs -> abs_to_string ~meta:meta env verbose indent indent_incr abs
+ | EFrame -> craise_opt_meta meta "Can't print a Frame element"
- let opt_env_elem_to_string (meta : Meta.meta) (env : fmt_env) (verbose : bool)
+ let opt_env_elem_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (verbose : bool)
(with_var_types : bool) (indent : string) (indent_incr : string)
(ev : env_elem option) : string =
match ev with
| None -> indent ^ "..."
| Some ev ->
- env_elem_to_string meta env verbose with_var_types indent indent_incr ev
+ env_elem_to_string ~meta:meta env verbose with_var_types indent indent_incr ev
(** Filters "dummy" bindings from an environment, to gain space and clarity/
See [env_to_string]. *)
@@ -379,7 +379,7 @@ module Contexts = struct
"..." to gain space and clarity.
[with_var_types]: if true, print the type of the variables
*)
- let env_to_string (meta : Meta.meta) (filter : bool) (fmt_env : fmt_env) (verbose : bool)
+ let env_to_string ?(meta : Meta.meta option = None) (filter : bool) (fmt_env : fmt_env) (verbose : bool)
(with_var_types : bool) (env : env) : string =
let env =
if filter then filter_env env else List.map (fun ev -> Some ev) env
@@ -388,7 +388,7 @@ module Contexts = struct
^ String.concat "\n"
(List.map
(fun ev ->
- opt_env_elem_to_string meta fmt_env verbose with_var_types " " " " ev)
+ opt_env_elem_to_string ~meta:meta fmt_env verbose with_var_types " " " " ev)
env)
^ "\n}"
@@ -468,7 +468,7 @@ module Contexts = struct
let frames = split_aux [] [] env in
frames
- let eval_ctx_to_string_gen (meta : Meta.meta) (verbose : bool) (filter : bool)
+ let eval_ctx_to_string_gen ?(meta : Meta.meta option = None) (verbose : bool) (filter : bool)
(with_var_types : bool) (ctx : eval_ctx) : string =
let fmt_env = eval_ctx_to_fmt_env ctx in
let ended_regions = RegionId.Set.to_string None ctx.ended_regions in
@@ -486,24 +486,24 @@ module Contexts = struct
| EBinding (BDummy _, _) -> num_dummies := !num_abs + 1
| EBinding (BVar _, _) -> num_bindings := !num_bindings + 1
| EAbs _ -> num_abs := !num_abs + 1
- | _ -> craise meta "Unreachable")
+ | _ -> craise_opt_meta meta "Unreachable")
f;
"\n# Frame " ^ string_of_int i ^ ":" ^ "\n- locals: "
^ string_of_int !num_bindings
^ "\n- dummy bindings: " ^ string_of_int !num_dummies
^ "\n- abstractions: " ^ string_of_int !num_abs ^ "\n"
- ^ env_to_string meta filter fmt_env verbose with_var_types f
+ ^ env_to_string ~meta:meta filter fmt_env verbose with_var_types f
^ "\n")
frames
in
"# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames
^ " frame(s)\n" ^ String.concat "" frames
- let eval_ctx_to_string (meta : Meta.meta) (ctx : eval_ctx) : string =
- eval_ctx_to_string_gen meta false true true ctx
+ let eval_ctx_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) : string =
+ eval_ctx_to_string_gen ~meta:meta false true true ctx
- let eval_ctx_to_string_no_filter (meta : Meta.meta) (ctx : eval_ctx) : string =
- eval_ctx_to_string_gen meta false false true ctx
+ let eval_ctx_to_string_no_filter ?(meta : Meta.meta option = None) (ctx : eval_ctx) : string =
+ eval_ctx_to_string_gen ~meta:meta false false true ctx
end
(** Pretty-printing for LLBC ASTs (functions based on an evaluation context) *)
@@ -541,22 +541,22 @@ module EvalCtx = struct
let env = eval_ctx_to_fmt_env ctx in
trait_instance_id_to_string env x
- let borrow_content_to_string (meta : Meta.meta) (ctx : eval_ctx) (bc : borrow_content) : string =
+ let borrow_content_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (bc : borrow_content) : string =
let env = eval_ctx_to_fmt_env ctx in
- borrow_content_to_string meta env bc
+ borrow_content_to_string ~meta:meta env bc
- let loan_content_to_string (meta : Meta.meta) (ctx : eval_ctx) (lc : loan_content) : string =
+ let loan_content_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (lc : loan_content) : string =
let env = eval_ctx_to_fmt_env ctx in
- loan_content_to_string meta env lc
+ loan_content_to_string ~meta:meta env lc
- let aborrow_content_to_string (meta : Meta.meta) (ctx : eval_ctx) (bc : aborrow_content) : string
+ let aborrow_content_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (bc : aborrow_content) : string
=
let env = eval_ctx_to_fmt_env ctx in
- aborrow_content_to_string meta env bc
+ aborrow_content_to_string ~meta:meta env bc
- let aloan_content_to_string (meta : Meta.meta) (ctx : eval_ctx) (lc : aloan_content) : string =
+ let aloan_content_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (lc : aloan_content) : string =
let env = eval_ctx_to_fmt_env ctx in
- aloan_content_to_string meta env lc
+ aloan_content_to_string ~meta:meta env lc
let aproj_to_string (ctx : eval_ctx) (p : aproj) : string =
let env = eval_ctx_to_fmt_env ctx in
@@ -566,13 +566,13 @@ module EvalCtx = struct
let env = eval_ctx_to_fmt_env ctx in
symbolic_value_to_string env sv
- let typed_value_to_string (meta : Meta.meta) (ctx : eval_ctx) (v : typed_value) : string =
+ let typed_value_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (v : typed_value) : string =
let env = eval_ctx_to_fmt_env ctx in
- typed_value_to_string meta env v
+ typed_value_to_string ~meta:meta env v
- let typed_avalue_to_string (meta : Meta.meta) (ctx : eval_ctx) (v : typed_avalue) : string =
+ let typed_avalue_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (v : typed_avalue) : string =
let env = eval_ctx_to_fmt_env ctx in
- typed_avalue_to_string meta env v
+ typed_avalue_to_string ~meta:meta env v
let place_to_string (ctx : eval_ctx) (op : place) : string =
let env = eval_ctx_to_fmt_env ctx in
@@ -613,13 +613,13 @@ module EvalCtx = struct
let env = eval_ctx_to_fmt_env ctx in
trait_impl_to_string env " " " " timpl
- let env_elem_to_string (meta : Meta.meta) (ctx : eval_ctx) (indent : string)
+ let env_elem_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (indent : string)
(indent_incr : string) (ev : env_elem) : string =
let env = eval_ctx_to_fmt_env ctx in
- env_elem_to_string meta env false true indent indent_incr ev
+ env_elem_to_string ~meta:meta env false true indent indent_incr ev
- let abs_to_string (meta : Meta.meta) (ctx : eval_ctx) (indent : string) (indent_incr : string)
+ let abs_to_string ?(meta : Meta.meta option = None) (ctx : eval_ctx) (indent : string) (indent_incr : string)
(abs : abs) : string =
let env = eval_ctx_to_fmt_env ctx in
- abs_to_string meta env false indent indent_incr abs
+ abs_to_string ~meta:meta env false indent indent_incr abs
end
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 3008e1bd..6ef87194 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -351,7 +351,7 @@ let adt_field_to_string ?(meta = None) (env : fmt_env) (adt_id : type_id)
(** TODO: we don't need a general function anymore (it is now only used for
patterns)
*)
-let adt_g_value_to_string (meta : Meta.meta) (env : fmt_env) (value_to_string : 'v -> string)
+let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (value_to_string : 'v -> string)
(variant_id : VariantId.id option) (field_values : 'v list) (ty : ty) :
string =
let field_values = List.map value_to_string field_values in
@@ -386,50 +386,50 @@ let adt_g_value_to_string (meta : Meta.meta) (env : fmt_env) (value_to_string :
match aty with
| TState | TRawPtr _ ->
(* This type is opaque: we can't get there *)
- craise meta "Unreachable"
+ craise_opt_meta meta "Unreachable"
| TResult ->
let variant_id = Option.get variant_id in
if variant_id = result_return_id then
match field_values with
| [ v ] -> "@Result::Return " ^ v
- | _ -> craise meta "Result::Return takes exactly one value"
+ | _ -> craise_opt_meta meta "Result::Return takes exactly one value"
else if variant_id = result_fail_id then
match field_values with
| [ v ] -> "@Result::Fail " ^ v
- | _ -> craise meta "Result::Fail takes exactly one value"
+ | _ -> craise_opt_meta meta "Result::Fail takes exactly one value"
else
- craise meta "Unreachable: improper variant id for result type"
+ craise_opt_meta meta "Unreachable: improper variant id for result type"
| TError ->
- cassert (field_values = []) meta "TODO: error message";
+ cassert_opt_meta (field_values = []) meta "TODO: error message";
let variant_id = Option.get variant_id in
if variant_id = error_failure_id then "@Error::Failure"
else if variant_id = error_out_of_fuel_id then "@Error::OutOfFuel"
- else craise meta "Unreachable: improper variant id for error type"
+ else craise_opt_meta meta "Unreachable: improper variant id for error type"
| TFuel ->
let variant_id = Option.get variant_id in
if variant_id = fuel_zero_id then (
- cassert (field_values = []) meta "TODO: error message";
+ cassert_opt_meta (field_values = []) meta "TODO: error message";
"@Fuel::Zero")
else if variant_id = fuel_succ_id then
match field_values with
| [ v ] -> "@Fuel::Succ " ^ v
- | _ -> craise meta "@Fuel::Succ takes exactly one value"
- else craise meta "Unreachable: improper variant id for fuel type"
+ | _ -> craise_opt_meta meta "@Fuel::Succ takes exactly one value"
+ else craise_opt_meta meta "Unreachable: improper variant id for fuel type"
| TArray | TSlice | TStr ->
- cassert (variant_id = None) meta "TODO: error message";
+ cassert_opt_meta (variant_id = None) meta "TODO: error message";
let field_values =
List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
in
let id = assumed_ty_to_string aty in
id ^ " [" ^ String.concat "; " field_values ^ "]")
| _ ->
- craise
+ craise_opt_meta
meta
("Inconsistently typed value: expected ADT type but found:"
^ "\n- ty: " ^ ty_to_string env false ty ^ "\n- variant_id: "
^ Print.option_to_string VariantId.to_string variant_id)
-let rec typed_pattern_to_string (meta : Meta.meta) (env : fmt_env) (v : typed_pattern) : string =
+let rec typed_pattern_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (v : typed_pattern) : string =
match v.value with
| PatConstant cv -> literal_to_string cv
| PatVar (v, None) -> var_to_string env v
@@ -440,8 +440,8 @@ let rec typed_pattern_to_string (meta : Meta.meta) (env : fmt_env) (v : typed_pa
^ ")"
| PatDummy -> "_"
| PatAdt av ->
- adt_g_value_to_string meta env
- (typed_pattern_to_string meta env)
+ adt_g_value_to_string ~meta:meta env
+ (typed_pattern_to_string ~meta:meta env)
av.variant_id av.field_values v.ty
let fun_sig_to_string (env : fmt_env) (sg : fun_sig) : string =
@@ -522,7 +522,7 @@ let fun_or_op_id_to_string (env : fmt_env) (fun_id : fun_or_op_id) : string =
binop_to_string binop ^ "<" ^ integer_type_to_string int_ty ^ ">"
(** [inside]: controls the introduction of parentheses *)
-let rec texpression_to_string (metadata : Meta.meta) (env : fmt_env) (inside : bool) (indent : string)
+let rec texpression_to_string ?(metadata : Meta.meta option = None) (env : fmt_env) (inside : bool) (indent : string)
(indent_incr : string) (e : texpression) : string =
match e.e with
| Var var_id -> var_id_to_string env var_id
@@ -532,22 +532,22 @@ let rec texpression_to_string (metadata : Meta.meta) (env : fmt_env) (inside : b
(* Recursively destruct the app, to have a pair (app, arguments list) *)
let app, args = destruct_apps e in
(* Convert to string *)
- app_to_string metadata env inside indent indent_incr app args
+ app_to_string ~meta:metadata env inside indent indent_incr app args
| Lambda _ ->
let xl, e = destruct_lambdas e in
- let e = lambda_to_string metadata env indent indent_incr xl e in
+ let e = lambda_to_string ~meta:metadata env indent indent_incr xl e in
if inside then "(" ^ e ^ ")" else e
| Qualif _ ->
(* Qualifier without arguments *)
- app_to_string metadata env inside indent indent_incr e []
+ app_to_string ~meta:metadata env inside indent indent_incr e []
| Let (monadic, lv, re, e) ->
- let e = let_to_string metadata env indent indent_incr monadic lv re e in
+ let e = let_to_string ~meta:metadata env indent indent_incr monadic lv re e in
if inside then "(" ^ e ^ ")" else e
| Switch (scrutinee, body) ->
- let e = switch_to_string metadata env indent indent_incr scrutinee body in
+ let e = switch_to_string ~meta:metadata env indent indent_incr scrutinee body in
if inside then "(" ^ e ^ ")" else e
| Loop loop ->
- let e = loop_to_string metadata env indent indent_incr loop in
+ let e = loop_to_string ~meta:metadata env indent indent_incr loop in
if inside then "(" ^ e ^ ")" else e
| StructUpdate supd -> (
let s =
@@ -566,7 +566,7 @@ let rec texpression_to_string (metadata : Meta.meta) (env : fmt_env) (inside : b
(fun (fid, fe) ->
let field = FieldId.nth field_names fid in
let fe =
- texpression_to_string metadata env false indent2 indent_incr fe
+ texpression_to_string ~metadata:metadata env false indent2 indent_incr fe
in
"\n" ^ indent1 ^ field ^ " := " ^ fe ^ ";")
supd.updates
@@ -577,21 +577,21 @@ let rec texpression_to_string (metadata : Meta.meta) (env : fmt_env) (inside : b
let fields =
List.map
(fun (_, fe) ->
- texpression_to_string metadata env false indent2 indent_incr fe)
+ texpression_to_string ~metadata:metadata env false indent2 indent_incr fe)
supd.updates
in
"[ " ^ String.concat ", " fields ^ " ]"
- | _ -> craise metadata "Unexpected")
+ | _ -> craise_opt_meta metadata "Unexpected")
| Meta (meta, e) -> (
- let meta_s = emeta_to_string metadata env meta in
- let e = texpression_to_string metadata env inside indent indent_incr e in
+ let meta_s = emeta_to_string ~metadata:metadata env meta in
+ let e = texpression_to_string ~metadata:metadata env inside indent indent_incr e in
match meta with
| Assignment _ | SymbolicAssignments _ | SymbolicPlaces _ | Tag _ ->
let e = meta_s ^ "\n" ^ indent ^ e in
if inside then "(" ^ e ^ ")" else e
| MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
-and app_to_string (meta : Meta.meta) (env : fmt_env) (inside : bool) (indent : string)
+and app_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (inside : bool) (indent : string)
(indent_incr : string) (app : texpression) (args : texpression list) :
string =
(* There are two possibilities: either the [app] is an instantiated,
@@ -611,13 +611,13 @@ and app_to_string (meta : Meta.meta) (env : fmt_env) (inside : bool) (indent : s
(global_decl_id_to_string env global_id, generics)
| AdtCons adt_cons_id ->
let variant_s =
- adt_variant_to_string ~meta:(Some meta) env adt_cons_id.adt_id
+ adt_variant_to_string ~meta:meta env adt_cons_id.adt_id
adt_cons_id.variant_id
in
(ConstStrings.constructor_prefix ^ variant_s, [])
| Proj { adt_id; field_id } ->
- let adt_s = adt_variant_to_string ~meta:(Some meta) env adt_id None in
- let field_s = adt_field_to_string ~meta:(Some meta) env adt_id field_id in
+ let adt_s = adt_variant_to_string ~meta:meta env adt_id None in
+ let field_s = adt_field_to_string ~meta:meta env adt_id field_id in
(* Adopting an F*-like syntax *)
(ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, [])
| TraitConst (trait_ref, const_name) ->
@@ -627,7 +627,7 @@ and app_to_string (meta : Meta.meta) (env : fmt_env) (inside : bool) (indent : s
| _ ->
(* "Regular" expression case *)
let inside = args <> [] || (args = [] && inside) in
- (texpression_to_string meta env inside indent indent_incr app, [])
+ (texpression_to_string ~metadata:meta env inside indent indent_incr app, [])
in
(* Convert the arguments.
* The arguments are expressions, so indentation might get weird... (though
@@ -635,7 +635,7 @@ and app_to_string (meta : Meta.meta) (env : fmt_env) (inside : bool) (indent : s
let arg_to_string =
let inside = true in
let indent1 = indent ^ indent_incr in
- texpression_to_string meta env inside indent1 indent_incr
+ texpression_to_string ~metadata:meta env inside indent1 indent_incr
in
let args = List.map arg_to_string args in
let all_args = List.append generics args in
@@ -646,31 +646,31 @@ and app_to_string (meta : Meta.meta) (env : fmt_env) (inside : bool) (indent : s
(* Add parentheses *)
if all_args <> [] && inside then "(" ^ e ^ ")" else e
-and lambda_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (indent_incr : string)
+and lambda_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (indent : string) (indent_incr : string)
(xl : typed_pattern list) (e : texpression) : string =
- let xl = List.map (typed_pattern_to_string meta env) xl in
- let e = texpression_to_string meta env false indent indent_incr e in
+ let xl = List.map (typed_pattern_to_string ~meta:meta env) xl in
+ let e = texpression_to_string ~metadata:meta env false indent indent_incr e in
"λ " ^ String.concat " " xl ^ ". " ^ e
-and let_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (indent_incr : string)
+and let_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (indent : string) (indent_incr : string)
(monadic : bool) (lv : typed_pattern) (re : texpression) (e : texpression) :
string =
let indent1 = indent ^ indent_incr in
let inside = false in
- let re = texpression_to_string meta env inside indent1 indent_incr re in
- let e = texpression_to_string meta env inside indent indent_incr e in
- let lv = typed_pattern_to_string meta env lv in
+ let re = texpression_to_string ~metadata:meta env inside indent1 indent_incr re in
+ let e = texpression_to_string ~metadata:meta env inside indent indent_incr e in
+ let lv = typed_pattern_to_string ~meta:meta env lv in
if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e
else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e
-and switch_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (indent_incr : string)
+and switch_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (indent : string) (indent_incr : string)
(scrutinee : texpression) (body : switch_body) : string =
let indent1 = indent ^ indent_incr in
(* Printing can mess up on the scrutinee, because it is an expression - but
* in most situations it will be a value or a function call, so it should be
* ok*)
- let scrut = texpression_to_string meta env true indent1 indent_incr scrutinee in
- let e_to_string = texpression_to_string meta env false indent1 indent_incr in
+ let scrut = texpression_to_string ~metadata:meta env true indent1 indent_incr scrutinee in
+ let e_to_string = texpression_to_string ~metadata:meta env false indent1 indent_incr in
match body with
| If (e_true, e_false) ->
let e_true = e_to_string e_true in
@@ -679,13 +679,13 @@ and switch_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (inden
^ indent ^ "else\n" ^ indent1 ^ e_false
| Match branches ->
let branch_to_string (b : match_branch) : string =
- let pat = typed_pattern_to_string meta env b.pat in
+ let pat = typed_pattern_to_string ~meta:meta env b.pat in
indent ^ "| " ^ pat ^ " ->\n" ^ indent1 ^ e_to_string b.branch
in
let branches = List.map branch_to_string branches in
"match " ^ scrut ^ " with\n" ^ String.concat "\n" branches
-and loop_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (indent_incr : string)
+and loop_to_string ?(meta : Meta.meta option = None) (env : fmt_env) (indent : string) (indent_incr : string)
(loop : loop) : string =
let indent1 = indent ^ indent_incr in
let indent2 = indent1 ^ indent_incr in
@@ -696,17 +696,17 @@ and loop_to_string (meta : Meta.meta) (env : fmt_env) (indent : string) (indent_
in
let output_ty = "output_ty: " ^ ty_to_string env false loop.output_ty in
let fun_end =
- texpression_to_string meta env false indent2 indent_incr loop.fun_end
+ texpression_to_string ~metadata:meta env false indent2 indent_incr loop.fun_end
in
let loop_body =
- texpression_to_string meta env false indent2 indent_incr loop.loop_body
+ texpression_to_string ~metadata:meta env false indent2 indent_incr loop.loop_body
in
"loop {\n" ^ indent1 ^ loop_inputs ^ "\n" ^ indent1 ^ output_ty ^ "\n"
^ indent1 ^ "fun_end: {\n" ^ indent2 ^ fun_end ^ "\n" ^ indent1 ^ "}\n"
^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1 ^ "}\n"
^ indent ^ "}"
-and emeta_to_string (metadata : Meta.meta) (env : fmt_env) (meta : emeta) : string =
+and emeta_to_string ?(metadata : Meta.meta option = None) (env : fmt_env) (meta : emeta) : string =
let meta =
match meta with
| Assignment (lp, rv, rp) ->
@@ -716,14 +716,14 @@ and emeta_to_string (metadata : Meta.meta) (env : fmt_env) (meta : emeta) : stri
| Some rp -> " [@src=" ^ mplace_to_string env rp ^ "]"
in
"@assign(" ^ mplace_to_string env lp ^ " := "
- ^ texpression_to_string metadata env false "" "" rv
+ ^ texpression_to_string ~metadata:metadata env false "" "" rv
^ rp ^ ")"
| SymbolicAssignments info ->
let infos =
List.map
(fun (var_id, rv) ->
VarId.to_string var_id ^ " == "
- ^ texpression_to_string metadata env false "" "" rv)
+ ^ texpression_to_string ~metadata:metadata env false "" "" rv)
info
in
let infos = String.concat ", " infos in
@@ -756,5 +756,5 @@ let fun_decl_to_string (env : fmt_env) (def : fun_decl) : string =
if inputs = [] then indent
else " fun " ^ String.concat " " inputs ^ " ->\n" ^ indent
in
- let body = texpression_to_string def.meta env inside indent indent body.body in
+ let body = texpression_to_string ~metadata:(Some def.meta) env inside indent indent body.body in
"let " ^ name ^ " :\n " ^ signature ^ " =\n" ^ inputs ^ body
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index d7423441..1df7176d 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -222,7 +222,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
(* Register a variable for constraints propagation - used when an variable is
* introduced (left-hand side of a left binding) *)
let register_var (ctx : pn_ctx) (v : var) : pn_ctx =
- cassert (not (VarId.Map.mem v.id ctx.pure_vars)) def.meta "TODO: error message";
+ sanity_check (not (VarId.Map.mem v.id ctx.pure_vars)) def.meta;
match v.basename with
| None -> ctx
| Some name ->
@@ -1204,7 +1204,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
let num_fields = List.length fields in
(* In order to simplify, there must be as many arguments as
* there are fields *)
- cassert (num_fields > 0) def.meta "The number of fields is not > 0";
+ sanity_check (num_fields > 0) def.meta;
if num_fields = List.length args then
(* We now need to check that all the arguments are of the form:
* [x.field] for some variable [x], and where the projection
@@ -1572,7 +1572,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
let arg, args = Collections.List.pop args in
mk_apps def.meta arg args
| BoxFree ->
- cassert (args = []) def.meta "TODO: error message";
+ sanity_check (args = []) def.meta;
mk_unit_rvalue
| SliceIndexShared | SliceIndexMut | ArrayIndexShared
| ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
@@ -1767,7 +1767,7 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
(* TODO: this information should be computed in SymbolicToPure and
* store in an enum ("monadic" should be an enum, not a bool). *)
let re_ty = Option.get (opt_destruct_result def.meta re.ty) in
- cassert (lv.ty = re_ty) def.meta "TODO: error message";
+ sanity_check (lv.ty = re_ty) def.meta;
let err_vid = fresh_id () in
let err_var : var =
{
@@ -1981,7 +1981,6 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
(List.concat (List.map (fun { f; loops } -> [ f :: loops ]) transl))
in
let subgroups = ReorderDecls.group_reorder_fun_decls all_decls in
-(* TODO meta or not meta ? *)
log#ldebug
(lazy
("filter_loop_inputs: all_decls:\n\n"
@@ -2021,7 +2020,7 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
^ String.concat ", " (List.map (var_to_string ctx) inputs_prefix)
^ "\n"));
let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in
- cassert (Option.is_some decl.loop_id) decl.meta "TODO: error message";
+ sanity_check (Option.is_some decl.loop_id) decl.meta;
let fun_id = (E.FRegular decl.def_id, decl.loop_id) in
@@ -2173,7 +2172,7 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
in
let fwd_info = { fwd_info; effect_info; ignore_output } in
- cassert (fun_sig_info_is_wf fwd_info) decl.meta "TODO: error message";
+ sanity_check (fun_sig_info_is_wf fwd_info) decl.meta;
let signature =
{
generics;
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index 6bc11a7c..d2fa57ae 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -15,9 +15,9 @@ let get_adt_field_types (meta : Meta.meta) (type_decls : type_decl TypeDeclId.Ma
match type_id with
| TTuple ->
(* Tuple *)
- cassert (generics.const_generics = []) meta "TODO: error message";
- cassert (generics.trait_refs = []) meta "TODO: error message";
- cassert (variant_id = None) meta "TODO: error message";
+ sanity_check (generics.const_generics = []) meta;
+ sanity_check (generics.trait_refs = []) meta;
+ sanity_check (variant_id = None) meta;
generics.types
| TAdtId def_id ->
(* "Regular" ADT *)
@@ -37,10 +37,10 @@ let get_adt_field_types (meta : Meta.meta) (type_decls : type_decl TypeDeclId.Ma
else
craise meta "Unreachable: improper variant id for result type"
| TError ->
- cassert (generics = empty_generic_args) meta "TODO: error message";
+ sanity_check (generics = empty_generic_args) meta;
let variant_id = Option.get variant_id in
- cassert (
- variant_id = error_failure_id || variant_id = error_out_of_fuel_id) meta "TODO: error message";
+ sanity_check (
+ variant_id = error_failure_id || variant_id = error_out_of_fuel_id) meta;
[]
| TFuel ->
let variant_id = Option.get variant_id in
@@ -64,7 +64,7 @@ type tc_ctx = {
let check_literal (meta : Meta.meta) (v : literal) (ty : literal_type) : unit =
match (ty, v) with
- | TInteger int_ty, VScalar sv -> cassert (int_ty = sv.int_ty) meta "TODO: error message"
+ | TInteger int_ty, VScalar sv -> sanity_check (int_ty = sv.int_ty) meta
| TBool, VBool _ | TChar, VChar _ -> ()
| _ -> craise meta "Inconsistent type"
@@ -76,7 +76,7 @@ let rec check_typed_pattern (meta : Meta.meta) (ctx : tc_ctx) (v : typed_pattern
ctx
| PatDummy -> ctx
| PatVar (var, _) ->
- cassert (var.ty = v.ty) meta "TODO: error message";
+ sanity_check (var.ty = v.ty) meta;
let env = VarId.Map.add var.id var.ty ctx.env in
{ ctx with env }
| PatAdt av ->
@@ -110,21 +110,21 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) :
* we use a locally nameless representation *)
match VarId.Map.find_opt var_id ctx.env with
| None -> ()
- | Some ty -> cassert (ty = e.ty) meta "TODO: error message")
+ | Some ty -> sanity_check (ty = e.ty) meta)
| CVar cg_id ->
let ty = T.ConstGenericVarId.Map.find cg_id ctx.const_generics in
- cassert (ty = e.ty) meta "TODO: error message"
+ sanity_check (ty = e.ty) meta
| Const cv -> check_literal meta cv (ty_as_literal meta e.ty)
| App (app, arg) ->
let input_ty, output_ty = destruct_arrow meta app.ty in
- cassert (input_ty = arg.ty) meta "TODO: error message";
- cassert (output_ty = e.ty) meta "TODO: error message";
+ sanity_check (input_ty = arg.ty) meta;
+ sanity_check (output_ty = e.ty) meta;
check_texpression meta ctx app;
check_texpression meta ctx arg
| Lambda (pat, body) ->
let pat_ty, body_ty = destruct_arrow meta e.ty in
- cassert (pat.ty = pat_ty) meta "TODO: error message";
- cassert (body.ty = body_ty) meta "TODO: error message";
+ sanity_check (pat.ty = pat_ty) meta;
+ sanity_check (body.ty = body_ty) meta;
(* Check the pattern and register the introduced variables at the same time *)
let ctx = check_typed_pattern meta ctx pat in
check_texpression meta ctx body
@@ -139,8 +139,8 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) :
let adt_ty, field_ty = destruct_arrow meta e.ty in
let adt_id, adt_generics = ty_as_adt meta adt_ty in
(* Check the ADT type *)
- cassert (adt_id = proj_adt_id) meta "TODO: error message";
- cassert (adt_generics = qualif.generics) meta "TODO: error message";
+ sanity_check (adt_id = proj_adt_id) meta;
+ sanity_check (adt_generics = qualif.generics) meta;
(* Retrieve and check the expected field type *)
let variant_id = None in
let expected_field_tys =
@@ -148,23 +148,23 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) :
qualif.generics
in
let expected_field_ty = FieldId.nth expected_field_tys field_id in
- cassert (expected_field_ty = field_ty) meta "TODO: error message"
+ sanity_check (expected_field_ty = field_ty) meta
| AdtCons id -> (
let expected_field_tys =
get_adt_field_types meta ctx.type_decls id.adt_id id.variant_id
qualif.generics
in
let field_tys, adt_ty = destruct_arrows e.ty in
- cassert (expected_field_tys = field_tys) meta "TODO: error message";
+ sanity_check (expected_field_tys = field_tys) meta;
match adt_ty with
| TAdt (type_id, generics) ->
- cassert (type_id = id.adt_id) meta "TODO: error message";
- cassert (generics = qualif.generics) meta "TODO: error message"
+ sanity_check (type_id = id.adt_id) meta;
+ sanity_check (generics = qualif.generics) meta
| _ -> craise meta "Unreachable"))
| Let (monadic, pat, re, e_next) ->
let expected_pat_ty = if monadic then destruct_result meta re.ty else re.ty in
- cassert (pat.ty = expected_pat_ty) meta "TODO: error message";
- cassert (e.ty = e_next.ty) meta "TODO: error message";
+ sanity_check (pat.ty = expected_pat_ty) meta;
+ sanity_check (e.ty = e_next.ty) meta;
(* Check the right-expression *)
check_texpression meta ctx re;
(* Check the pattern and register the introduced variables at the same time *)
@@ -175,20 +175,20 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) :
check_texpression meta ctx scrut;
match switch_body with
| If (e_then, e_else) ->
- cassert (scrut.ty = TLiteral TBool) meta "TODO: error message";
- cassert (e_then.ty = e.ty) meta "TODO: error message";
- cassert (e_else.ty = e.ty) meta "TODO: error message";
+ sanity_check (scrut.ty = TLiteral TBool) meta;
+ sanity_check (e_then.ty = e.ty) meta;
+ sanity_check (e_else.ty = e.ty) meta;
check_texpression meta ctx e_then;
check_texpression meta ctx e_else
| Match branches ->
let check_branch (br : match_branch) : unit =
- cassert (br.pat.ty = scrut.ty) meta "TODO: error message";
+ sanity_check (br.pat.ty = scrut.ty) meta;
let ctx = check_typed_pattern meta ctx br.pat in
check_texpression meta ctx br.branch
in
List.iter check_branch branches)
| Loop loop ->
- cassert (loop.fun_end.ty = e.ty) meta "TODO: error message";
+ sanity_check (loop.fun_end.ty = e.ty) meta;
check_texpression meta ctx loop.fun_end;
check_texpression meta ctx loop.loop_body
| StructUpdate supd -> (
@@ -196,11 +196,11 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) :
(if Option.is_some supd.init then
match VarId.Map.find_opt (Option.get supd.init) ctx.env with
| None -> ()
- | Some ty -> cassert (ty = e.ty) meta "TODO: error message");
+ | Some ty -> sanity_check (ty = e.ty) meta);
(* Check the fields *)
(* Retrieve and check the expected field type *)
let adt_id, adt_generics = ty_as_adt meta e.ty in
- cassert (adt_id = supd.struct_id) meta "TODO: error message";
+ sanity_check (adt_id = supd.struct_id) meta;
(* The id can only be: a custom type decl or an array *)
match adt_id with
| TAdtId _ ->
@@ -211,7 +211,7 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) :
List.iter
(fun ((fid, fe) : _ * texpression) ->
let expected_field_ty = FieldId.nth expected_field_tys fid in
- cassert (expected_field_ty = fe.ty) meta "TODO: error message";
+ sanity_check (expected_field_ty = fe.ty) meta;
check_texpression meta ctx fe)
supd.updates
| TAssumed TArray ->
@@ -220,10 +220,10 @@ let rec check_texpression (meta : Meta.meta) (ctx : tc_ctx) (e : texpression) :
in
List.iter
(fun ((_, fe) : _ * texpression) ->
- cassert (expected_field_ty = fe.ty) meta "TODO: error message";
+ sanity_check (expected_field_ty = fe.ty) meta;
check_texpression meta ctx fe)
supd.updates
| _ -> craise meta "Unexpected")
| Meta (_, e_next) ->
- cassert (e_next.ty = e.ty) meta "TODO: error message";
+ sanity_check (e_next.ty = e.ty) meta;
check_texpression meta ctx e_next
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 0f9c2dfe..cce70382 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -78,7 +78,7 @@ let fun_sig_info_is_wf (info : fun_sig_info) : bool =
let dest_arrow_ty (meta : Meta.meta) (ty : ty) : ty * ty =
match ty with
| TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
- | _ -> craise meta "Unreachable"
+ | _ -> craise meta "Not an arrow type"
let compute_literal_type (cv : literal) : literal_type =
match cv with
@@ -237,7 +237,7 @@ let is_var (e : texpression) : bool =
match e.e with Var _ -> true | _ -> false
let as_var (meta : Meta.meta) (e : texpression) : VarId.id =
- match e.e with Var v -> v | _ -> craise meta "Unreachable"
+ match e.e with Var v -> v | _ -> craise meta "Not a var"
let is_cvar (e : texpression) : bool =
match e.e with CVar _ -> true | _ -> false
@@ -251,7 +251,7 @@ let is_const (e : texpression) : bool =
let ty_as_adt (meta : Meta.meta) (ty : ty) : type_id * generic_args =
match ty with
| TAdt (id, generics) -> (id, generics)
- | _ -> craise meta "Unreachable"
+ | _ -> craise meta "Not an ADT"
(** Remove the external occurrences of {!Meta} *)
let rec unmeta (e : texpression) : texpression =
@@ -294,7 +294,7 @@ let destruct_lets_no_interleave (meta : Meta.meta) (e : texpression) :
let m =
match e.e with
| Let (monadic, _, _, _) -> monadic
- | _ -> craise meta "Unreachable"
+ | _ -> craise meta "Not a let-binding"
in
(* Destruct the rest *)
let rec destruct_lets (e : texpression) :
@@ -323,12 +323,11 @@ let destruct_apps (e : texpression) : texpression * texpression list =
(** Make an [App (app, arg)] expression *)
let mk_app (meta : Meta.meta) (app : texpression) (arg : texpression) : texpression =
let raise_or_return msg =
- if !Config.fail_hard then craise meta msg
- else
- let e = App (app, arg) in
- (* Dummy type - TODO: introduce an error type *)
- let ty = app.ty in
- { e; ty }
+ save_error (Some meta) msg;
+ let e = App (app, arg) in
+ (* Dummy type - TODO: introduce an error type *)
+ let ty = app.ty in
+ { e; ty }
in
match app.ty with
| TArrow (ty0, ty1) ->
@@ -371,8 +370,8 @@ let opt_destruct_function_call (e : texpression) :
let opt_destruct_result (meta : Meta.meta) (ty : ty) : ty option =
match ty with
| TAdt (TAssumed TResult, generics) ->
- cassert (generics.const_generics = []) meta "TODO: Error message";
- cassert (generics.trait_refs = []) meta "TODO: Error message";
+ sanity_check (generics.const_generics = []) meta;
+ sanity_check (generics.trait_refs = []) meta;
Some (Collections.List.to_cons_nil generics.types)
| _ -> None
@@ -381,8 +380,8 @@ let destruct_result (meta : Meta.meta) (ty : ty) : ty = Option.get (opt_destruct
let opt_destruct_tuple (meta : Meta.meta) (ty : ty) : ty list option =
match ty with
| TAdt (TTuple, generics) ->
- cassert (generics.const_generics = []) meta "TODO: Error message";
- cassert (generics.trait_refs = []) meta "TODO: Error message";
+ sanity_check (generics.const_generics = []) meta;
+ sanity_check (generics.trait_refs = []) meta;
Some generics.types
| _ -> None
diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml
index f4e2ff35..a4d66854 100644
--- a/compiler/RegionsHierarchy.ml
+++ b/compiler/RegionsHierarchy.ml
@@ -44,7 +44,7 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty
(fun_decls : fun_decl FunDeclId.Map.t)
(global_decls : global_decl GlobalDeclId.Map.t)
(trait_decls : trait_decl TraitDeclId.Map.t)
- (trait_impls : trait_impl TraitImplId.Map.t) (* ?meta *) (fun_name : string)
+ (trait_impls : trait_impl TraitImplId.Map.t) (fun_name : string)
(sg : fun_sig) : region_var_groups =
log#ldebug (lazy (__FUNCTION__ ^ ": " ^ fun_name));
(* Initialize a normalization context (we may need to normalize some
@@ -174,13 +174,13 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty
| TTraitType (trait_ref, _) ->
(* The trait should reference a clause, and not an implementation
(otherwise it should have been normalized) *)
- cassert_opt_meta (
- AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id) meta "The trait should reference a clause, and not an implementation (otherwise it should have been normalized)";
+ sanity_check_opt_meta (
+ AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id) meta;
(* We have nothing to do *)
()
| TArrow (regions, inputs, output) ->
(* TODO: *)
- cassert_opt_meta (regions = []) meta "Regions should be empty";
+ cassert_opt_meta (regions = []) meta "We don't support arrow types with locally quantified regions";
(* We can ignore the outer regions *)
List.iter (explore_ty []) (output :: inputs)
and explore_generics (outer : region list) (generics : generic_args) =
@@ -223,7 +223,7 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty
(SccId.Map.bindings sccs.sccs)
in
(* The SCC should only contain the 'static *)
- cassert_opt_meta (static_scc = [ RStatic ]) meta "The SCC should only contain the 'static";
+ sanity_check_opt_meta (static_scc = [ RStatic ]) meta;
(* Remove the group as well as references to this group from the
other SCCs *)
let { sccs; scc_deps } = sccs in
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index a35fdbf3..14cda863 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -80,9 +80,9 @@ let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta) (ctx : eval_ct
| TAssumed aty -> (
match aty with
| TBox ->
- cassert (generics.regions = []) meta "Regions should be empty TODO: error message";
- cassert (List.length generics.types = 1) meta "Too many types TODO: error message";
- cassert (generics.const_generics = []) meta "const_generics should be empty TODO: error message";
+ sanity_check (generics.regions = []) meta;
+ sanity_check (List.length generics.types = 1) meta;
+ sanity_check (generics.const_generics = []) meta;
generics.types
| TArray | TSlice | TStr ->
(* Those types don't have fields *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 46058a9a..e60d6870 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -325,7 +325,7 @@ let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
let typed_value_to_string (ctx : bs_ctx) (v : V.typed_value) : string =
let env = bs_ctx_to_fmt_env ctx in
- Print.Values.typed_value_to_string ctx.fun_decl.meta env v
+ Print.Values.typed_value_to_string ~meta:(Some ctx.fun_decl.meta) env v
let pure_ty_to_string (ctx : bs_ctx) (ty : ty) : string =
let env = bs_ctx_to_pure_fmt_env ctx in
@@ -349,7 +349,7 @@ let pure_type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string =
let texpression_to_string (ctx : bs_ctx) (e : texpression) : string =
let env = bs_ctx_to_pure_fmt_env ctx in
- PrintPure.texpression_to_string ctx.fun_decl.meta env false "" " " e
+ PrintPure.texpression_to_string ~metadata:(Some ctx.fun_decl.meta) env false "" " " e
let fun_id_to_string (ctx : bs_ctx) (id : A.fun_id) : string =
let env = bs_ctx_to_fmt_env ctx in
@@ -363,9 +363,9 @@ let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string =
let env = bs_ctx_to_pure_fmt_env ctx in
PrintPure.fun_decl_to_string env def
-let typed_pattern_to_string (meta : Meta.meta) (ctx : bs_ctx) (p : Pure.typed_pattern) : string =
+let typed_pattern_to_string ?(meta : Meta.meta option = None) (ctx : bs_ctx) (p : Pure.typed_pattern) : string =
let env = bs_ctx_to_pure_fmt_env ctx in
- PrintPure.typed_pattern_to_string meta env p
+ PrintPure.typed_pattern_to_string ~meta:meta env p
let ctx_get_effect_info_for_bid (ctx : bs_ctx) (bid : RegionGroupId.id option) :
fun_effect_info =
@@ -384,7 +384,7 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
let verbose = false in
let indent = "" in
let indent_incr = " " in
- Print.Values.abs_to_string ctx.fun_decl.meta env verbose indent indent_incr abs
+ Print.Values.abs_to_string ~meta:(Some ctx.fun_decl.meta) env verbose indent indent_incr abs
let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
T.type_decl =
@@ -478,7 +478,7 @@ let rec translate_sty (meta : Meta.meta) (ty : T.ty) : ty =
| TTraitType (trait_ref, type_name) ->
let trait_ref = translate_strait_ref meta trait_ref in
TTraitType (trait_ref, type_name)
- | TArrow _ -> craise meta "TODO"
+ | TArrow _ -> craise meta "TODO: error message"
and translate_sgeneric_args (meta : Meta.meta) (generics : T.generic_args) : generic_args =
translate_generic_args meta (translate_sty meta) generics
@@ -555,7 +555,7 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
let name = Print.Types.name_to_string env def.name in
let { T.regions; types; const_generics; trait_clauses } = def.generics in
(* Can't translate types with regions for now *)
- cassert (regions = []) def.meta "Translating types with regions is not supported yet";
+ cassert (regions = []) def.meta "ADTs containing borrows are not supported yet";
let trait_clauses = List.map (translate_trait_clause def.meta) trait_clauses in
let generics = { types; const_generics; trait_clauses } in
let kind = translate_type_decl_kind def.meta def.T.kind in
@@ -620,7 +620,7 @@ let rec translate_fwd_ty (meta : Meta.meta) (type_infos : type_infos) (ty : T.ty
not
(List.exists
(TypesUtils.ty_has_borrows type_infos)
- generics.types)) meta "General parametricity is not supported yet";
+ generics.types)) meta "ADTs containing borrows are not supported yet";
match t_generics.types with
| [ bty ] -> bty
| _ ->
@@ -640,7 +640,7 @@ let rec translate_fwd_ty (meta : Meta.meta) (type_infos : type_infos) (ty : T.ty
| TTraitType (trait_ref, type_name) ->
let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in
TTraitType (trait_ref, type_name)
- | TArrow _ -> craise meta "TODO"
+ | TArrow _ -> craise meta "TODO: error message"
and translate_fwd_generic_args (meta : Meta.meta) (type_infos : type_infos)
(generics : T.generic_args) : generic_args =
@@ -701,7 +701,7 @@ let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos)
else None
| TAssumed TBox -> (
(* Don't accept ADTs (which are not tuples) with borrows for now *)
- cassert (not (TypesUtils.ty_has_borrows type_infos ty)) meta "ADTs with borrows are not supported yet";
+ cassert (not (TypesUtils.ty_has_borrows type_infos ty)) meta "ADTs containing borrows are not supported yet";
(* Eliminate the box *)
match generics.types with
| [ bty ] -> translate bty
@@ -744,7 +744,7 @@ let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos)
let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in
Some (TTraitType (trait_ref, type_name))
else None
- | TArrow _ -> craise meta "TODO"
+ | TArrow _ -> craise meta "TODO: error message"
(** Simply calls [translate_back_ty] *)
let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
@@ -794,7 +794,7 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
(back_funs : texpression option RegionGroupId.Map.t option) (ctx : bs_ctx) :
bs_ctx =
let calls = ctx.calls in
- cassert (not (V.FunCallId.Map.mem call_id calls)) ctx.fun_decl.meta "TODO: error message";
+ sanity_check (not (V.FunCallId.Map.mem call_id calls)) ctx.fun_decl.meta;
let info = { forward; forward_inputs = args; back_funs } in
let calls = V.FunCallId.Map.add call_id info calls in
{ ctx with calls }
@@ -816,7 +816,7 @@ let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id)
let calls = V.FunCallId.Map.add call_id info ctx.calls in
(* Insert the abstraction in the abstractions map *)
let abstractions = ctx.abstractions in
- cassert (not (V.AbstractionId.Map.mem abs.abs_id abstractions)) ctx.fun_decl.meta "This abstraction should not be in the abstractions map";
+ sanity_check (not (V.AbstractionId.Map.mem abs.abs_id abstractions)) ctx.fun_decl.meta;
let abstractions =
V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions
in
@@ -896,7 +896,7 @@ let compute_raw_fun_effect_info (meta : Meta.meta) (fun_infos : fun_info A.FunD
is_rec = info.is_rec || Option.is_some lid;
}
| FunId (FAssumed aid) ->
- cassert (lid = None) meta "TODO: error message";
+ sanity_check (lid = None) meta;
{
can_fail = Assumed.assumed_fun_can_fail aid;
stateful_group = false;
@@ -926,7 +926,7 @@ let get_fun_effect_info (ctx : bs_ctx) (fun_id : A.fun_id_or_trait_method_ref)
(* This is necessarily for the current function *)
match fun_id with
| FunId (FRegular fid) -> (
- cassert (fid = ctx.fun_decl.def_id) ctx.fun_decl.meta "TODO: error message";
+ sanity_check (fid = ctx.fun_decl.def_id) ctx.fun_decl.meta;
(* Lookup the loop *)
let lid = V.LoopId.Map.find lid ctx.loop_ids_map in
let loop_info = LoopId.Map.find lid ctx.loops in
@@ -1188,7 +1188,7 @@ let translate_fun_sig_with_regions_hierarchy_to_decomposed (meta : Meta.meta)
else false
in
let info = { fwd_info; effect_info = fwd_effect_info; ignore_output } in
- cassert (fun_sig_info_is_wf info) meta "TODO: error message";
+ sanity_check (fun_sig_info_is_wf info) meta;
info
in
@@ -1541,7 +1541,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
(* Eliminate the tuple wrapper if it is a tuple with exactly one field *)
match v.ty with
| TAdt (TTuple, _) ->
- cassert (variant_id = None) ctx.fun_decl.meta "TODO: error message";
+ sanity_check (variant_id = None) ctx.fun_decl.meta;
mk_simpl_tuple_texpression ctx.fun_decl.meta field_values
| _ ->
(* Retrieve the type and the translated generics from the translated
@@ -1619,7 +1619,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
| TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
- cassert (field_values = []) ctx.fun_decl.meta "Only tuples can currently contain borrows";
+ cassert (field_values = []) ctx.fun_decl.meta "ADTs containing borrows are not supported yet";
None
| TTuple ->
(* Return *)
@@ -1687,7 +1687,7 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option =
(* The symbolic value was left unchanged *)
Some (symbolic_value_to_texpression ctx msv)
| V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) ->
- cassert (child_aproj = AIgnoredProjBorrows) ctx.fun_decl.meta "TODO: error message";
+ sanity_check (child_aproj = AIgnoredProjBorrows) ctx.fun_decl.meta;
(* The symbolic value was updated *)
Some (symbolic_value_to_texpression ctx mnv)
| V.AEndedProjLoans (_, _) ->
@@ -1762,12 +1762,12 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
let adt_id, _ = TypesUtils.ty_as_adt av.ty in
match adt_id with
| TAdtId _ | TAssumed (TBox | TArray | TSlice | TStr) ->
- cassert (field_values = []) ctx.fun_decl.meta "Only tuples can currently contain borrows";
+ cassert (field_values = []) ctx.fun_decl.meta "ADTs with borrows are not supported yet";
(ctx, None)
| TTuple ->
(* Return *)
let variant_id = adt_v.variant_id in
- cassert (variant_id = None) ctx.fun_decl.meta "TODO: error message";
+ sanity_check (variant_id = None) ctx.fun_decl.meta;
if field_values = [] then (ctx, None)
else
(* Note that if there is exactly one field value, [mk_simpl_tuple_pattern]
@@ -2042,9 +2042,9 @@ and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
(ctx : bs_ctx) : texpression =
- cassert (is_continue = ctx.inside_loop) ctx.fun_decl.meta "TODO: error message";
+ sanity_check (is_continue = ctx.inside_loop) ctx.fun_decl.meta;
let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in
- cassert (loop_id = Option.get ctx.loop_id) ctx.fun_decl.meta "TODO: error message";
+ sanity_check (loop_id = Option.get ctx.loop_id) ctx.fun_decl.meta;
(* Lookup the loop information *)
let loop_id = Option.get ctx.loop_id in
@@ -2313,7 +2313,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
(match binop with
(* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *)
| E.Shl | E.Shr -> ()
- | _ -> cassert (int_ty0 = int_ty1) ctx.fun_decl.meta "TODO: error message");
+ | _ -> sanity_check (int_ty0 = int_ty1) ctx.fun_decl.meta);
let effect_info =
{
can_fail = ExpressionsUtils.binop_can_fail binop;
@@ -2368,7 +2368,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
^ T.RegionGroupId.to_string rg_id
^ "\n- loop_id: "
^ Print.option_to_string Pure.LoopId.to_string ctx.loop_id
- ^ "\n- eval_ctx:\n" ^ eval_ctx_to_string ctx.fun_decl.meta ectx ^ "\n- abs:\n"
+ ^ "\n- eval_ctx:\n" ^ eval_ctx_to_string ~meta:(Some ctx.fun_decl.meta) ectx ^ "\n- abs:\n"
^ abs_to_string ctx abs ^ "\n"));
(* When we end an input abstraction, this input abstraction gets back
@@ -2382,7 +2382,7 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
for a parent backward function.
*)
let bid = Option.get ctx.bid in
- cassert (rg_id = bid) ctx.fun_decl.meta "TODO: error message";
+ sanity_check (rg_id = bid) ctx.fun_decl.meta;
(* First, introduce the given back variables.
@@ -2523,8 +2523,8 @@ and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs)
(* We can do this simply by checking that it consumes and gives back nothing *)
let inputs = abs_to_consumed ctx ectx abs in
let ctx, outputs = abs_to_given_back None abs ctx in
- cassert (inputs = []) ctx.fun_decl.meta "TODO: error message";
- cassert (outputs = []) ctx.fun_decl.meta "TODO: error message";
+ sanity_check (inputs = []) ctx.fun_decl.meta;
+ sanity_check (outputs = []) ctx.fun_decl.meta;
(* Translate the next expression *)
translate_expression e ctx
@@ -2566,7 +2566,7 @@ and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs)
(* Retrieve the values consumed upon ending the loans inside this
* abstraction: as there are no nested borrows, there should be none. *)
let consumed = abs_to_consumed ctx ectx abs in
- cassert (consumed = []) ctx.fun_decl.meta "Nested borrows are not supported yet TODO: error message";
+ cassert (consumed = []) ctx.fun_decl.meta "Nested borrows are not supported yet";
(* Retrieve the values given back upon ending this abstraction - note that
* we don't provide meta-place information, because those assignments will
* be inlined anyway... *)
@@ -2601,7 +2601,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
texpression =
let vloop_id = loop_id in
let loop_id = V.LoopId.Map.find loop_id ctx.loop_ids_map in
- cassert (loop_id = Option.get ctx.loop_id) ctx.fun_decl.meta "TODO: error message";
+ sanity_check (loop_id = Option.get ctx.loop_id) ctx.fun_decl.meta;
let rg_id = Option.get rg_id in
(* There are two cases depending on the [abs_kind] (whether this is a
synth input or a regular loop call) *)
@@ -2819,7 +2819,7 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
^ pure_ty_to_string ctx true_e.ty
^ "\n\nfalse_e.ty: "
^ pure_ty_to_string ctx false_e.ty));
- if !Config.fail_hard then cassert (ty = false_e.ty) ctx.fun_decl.meta "TODO: error message"; (* TODO: remove if ? *)
+ save_error ~b:(ty = false_e.ty) (Some ctx.fun_decl.meta) "Internal error, please file an issue";
{ e; ty }
| ExpandInt (int_ty, branches, otherwise) ->
let translate_branch ((v, branch_e) : V.scalar_value * S.expression) :
@@ -2844,8 +2844,8 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
Match all_branches )
in
let ty = otherwise.branch.ty in
- cassert (
- List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches) ctx.fun_decl.meta "TODO: error message";
+ sanity_check (
+ List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches) ctx.fun_decl.meta;
{ e; ty }
(* Translate and [ExpandAdt] when there is no branching (i.e., one branch).
@@ -3480,7 +3480,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
(* Add the loop information in the context *)
let ctx =
- cassert (not (LoopId.Map.mem loop_id ctx.loops)) ctx.fun_decl.meta "The loop information should not already be in the context TODO: error message";
+ sanity_check (not (LoopId.Map.mem loop_id ctx.loops)) ctx.fun_decl.meta;
(* Note that we will retrieve the input values later in the [ForwardEnd]
(and will introduce the outputs at that moment, together with the actual
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 787bfb4f..bdd27d0f 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -47,7 +47,7 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (plac
let get_scalar (see : symbolic_expansion option) : scalar_value =
match see with
| Some (SeLiteral (VScalar cv)) ->
- cassert (cv.int_ty = int_ty) meta "For all the regular branches, the symbolic value should have been expanded to a constant TODO: Error message";
+ sanity_check (cv.int_ty = int_ty) meta;
cv
| _ -> craise meta "Unreachable"
in
@@ -57,7 +57,7 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (plac
(* For the otherwise branch, the symbolic value should have been left
* unchanged *)
let otherwise_see, otherwise = otherwise in
- cassert (otherwise_see = None) meta "For the otherwise branch, the symbolic value should have been left unchanged";
+ sanity_check (otherwise_see = None) meta;
(* Return *)
ExpandInt (int_ty, branches, otherwise)
| TAdt (_, _) ->
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 11b179db..f97d7ab1 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -354,7 +354,7 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
*)
let export_types_group (fmt : Format.formatter) (config : gen_config)
(ctx : gen_ctx) (is_rec : bool) (ids : Pure.TypeDeclId.id list) : unit =
- assert (ids <> []) (* meta "TODO: Error message" *);
+ assert (ids <> []);
let export_type = export_type fmt config ctx in
let ids_set = Pure.TypeDeclId.Set.of_list ids in
let export_type_decl kind id = export_type ids_set kind id true false in
@@ -396,11 +396,11 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
if List.exists (fun b -> b) builtin then
(* Sanity check *)
- assert (List.for_all (fun b -> b) builtin) (* meta "TODO: Error message" *)
+ assert (List.for_all (fun b -> b) builtin)
else if List.exists dont_extract defs then
(* Check if we have to ignore declarations *)
(* Sanity check *)
- assert (List.for_all dont_extract defs) (* meta "TODO: Error message" *)
+ assert (List.for_all dont_extract defs)
else (
(* Extract the type declarations.
@@ -447,8 +447,8 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
let global_decls = ctx.trans_ctx.global_ctx.global_decls in
let global = GlobalDeclId.Map.find id global_decls in
let trans = FunDeclId.Map.find global.body ctx.trans_funs in
- cassert (trans.fwd.loops = []) global.meta "TODO: Error message";
- cassert (trans.backs = []) global.meta "TODO: Error message";
+ sanity_check (trans.fwd.loops = []) global.meta;
+ sanity_check (trans.backs = []) global.meta;
let body = trans.fwd.f in
let is_opaque = Option.is_none body.Pure.body in
@@ -915,7 +915,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
(* Initialize the names map by registering the keywords used in the
language, as well as some primitive names ("u32", etc.).
We insert the names of the local declarations later. *)
- let names_maps = Extract.initialize_names_maps () in (*TODO*)
+ let names_maps = Extract.initialize_names_maps () in
(* We need to compute which functions are recursive, in order to know
* whether we should generate a decrease clause or not. *)
@@ -1038,7 +1038,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
match Filename.chop_suffix_opt ~suffix:".llbc" filename with
| None ->
(* Note that we already checked the suffix upon opening the file *)
- raise (Failure "Unreachable") (* TODO check *)
+ raise (Failure "Unreachable")
| Some filename ->
(* Retrieve the file basename *)
let basename = Filename.basename filename in
diff --git a/compiler/ValuesUtils.ml b/compiler/ValuesUtils.ml
index 51c9e8cc..9c4b8b45 100644
--- a/compiler/ValuesUtils.ml
+++ b/compiler/ValuesUtils.ml
@@ -12,23 +12,23 @@ let mk_unit_value : typed_value =
{ value = VAdt { variant_id = None; field_values = [] }; ty = mk_unit_ty }
let mk_typed_value (meta : Meta.meta) (ty : ty) (value : value) : typed_value =
- cassert (ty_is_ety ty) meta "TODO: error message";
+ sanity_check (ty_is_ety ty) meta;
{ value; ty }
let mk_typed_avalue (meta : Meta.meta) (ty : ty) (value : avalue) : typed_avalue =
- cassert (ty_is_rty ty) meta "TODO: error message";
+ sanity_check (ty_is_rty ty) meta;
{ value; ty }
let mk_bottom (meta : Meta.meta) (ty : ty) : typed_value =
- cassert (ty_is_ety ty) meta "TODO: error message";
+ sanity_check (ty_is_ety ty) meta;
{ value = VBottom; ty }
let mk_abottom (meta : Meta.meta) (ty : ty) : typed_avalue =
- cassert (ty_is_rty ty) meta "TODO: error message";
+ sanity_check (ty_is_rty ty) meta;
{ value = ABottom; ty }
let mk_aignored (meta : Meta.meta) (ty : ty) : typed_avalue =
- cassert (ty_is_rty ty) meta "TODO: error message";
+ sanity_check (ty_is_rty ty) meta;
{ value = AIgnored; ty }
let value_as_symbolic (meta : Meta.meta) (v : value) : symbolic_value =