diff options
Diffstat (limited to '')
-rw-r--r-- | compiler/AssociatedTypes.ml | 12 | ||||
-rw-r--r-- | compiler/InterpreterExpressions.ml | 7 | ||||
-rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.ml | 4 | ||||
-rw-r--r-- | compiler/InterpreterProjectors.ml | 2 | ||||
-rw-r--r-- | compiler/PrintPure.ml | 6 | ||||
-rw-r--r-- | compiler/PureMicroPasses.ml | 8 | ||||
-rw-r--r-- | compiler/Substitute.ml | 2 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 13 |
8 files changed, 29 insertions, 25 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 083a38d1..27425a51 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -428,12 +428,12 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx) | TraitRef trait_ref -> (* The trait instance id necessarily refers to a local sub-clause. We can't project over it and can only peel off the [TraitRef] wrapper *) - cassert_opt_meta __FILE__ __LINE__ + sanity_check_opt_meta __FILE__ __LINE__ (trait_instance_id_is_local_clause trait_ref.trait_id) - ctx.meta "Trait instance id is not a local sub-clause"; - cassert_opt_meta __FILE__ __LINE__ + ctx.meta; + sanity_check_opt_meta __FILE__ __LINE__ (trait_ref.generics = empty_generic_args) - ctx.meta "TODO: error message"; + ctx.meta; (trait_ref.trait_id, None) | FnPointer ty -> let ty = norm_ctx_normalize_ty ctx ty in @@ -482,9 +482,9 @@ and norm_ctx_normalize_trait_ref (ctx : norm_ctx) (trait_ref : trait_ref) : (lazy ("norm_ctx_normalize_trait_ref: normalized to: " ^ trait_ref_to_string ctx trait_ref)); - cassert_opt_meta __FILE__ __LINE__ + sanity_check_opt_meta __FILE__ __LINE__ (generics = empty_generic_args) - ctx.meta "TODO: error message"; + ctx.meta; trait_ref (* Not sure this one is really necessary *) diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index d61ba410..48a1cce6 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -340,7 +340,9 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta) value_as_symbolic meta cv.value, SymbolicAst.VaCgValue vid, e ))) - | CFnPtr _ -> craise __FILE__ __LINE__ meta "TODO: error message") + | CFnPtr _ -> + craise __FILE__ __LINE__ meta + "Function pointers are not supported yet") | Copy p -> (* Access the value *) let access = Read in @@ -523,7 +525,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop) * The remaining binops only operate on scalars. *) if binop = Eq || binop = Ne then ( (* Equality operations *) - exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta "TODO: error message"; + exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta + "The arguments given to the binop don't have the same type"; (* Equality/inequality check is primitive only for a subset of types *) exec_assert __FILE__ __LINE__ (ty_is_primitively_copyable v1.ty) diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml index 6d814c5c..bd271ff4 100644 --- a/compiler/InterpreterLoopsMatchCtxs.ml +++ b/compiler/InterpreterLoopsMatchCtxs.ml @@ -243,7 +243,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct (not (ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos bv.value)) - M.meta "TODO: error message"; + M.meta "The join of nested borrows is not supported yet"; let bid, bv = M.match_mut_borrows ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv in @@ -268,7 +268,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct let sv = match_rec sv0 sv1 in cassert __FILE__ __LINE__ (not (value_has_borrows sv.value)) - M.meta "TODO: error message"; + M.meta "The join of nested borrows is not supported yet"; let ids, sv = M.match_shared_loans ctx0 ctx1 ty ids0 ids1 sv in VSharedLoan (ids, sv) | VMutLoan id0, VMutLoan id1 -> diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml index d7c20ae0..8b6eeb6c 100644 --- a/compiler/InterpreterProjectors.ml +++ b/compiler/InterpreterProjectors.ml @@ -502,7 +502,7 @@ let apply_proj_borrows_on_input_value (config : config) (meta : Meta.meta) (ctx : eval_ctx) (regions : RegionId.Set.t) (ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) : eval_ctx * typed_avalue = - cassert __FILE__ __LINE__ (ty_is_rty ty) meta "TODO: error message"; + sanity_check __FILE__ __LINE__ (ty_is_rty ty) meta; let check_symbolic_no_ended = true in let allow_reborrows = true in (* Prepare the reborrows *) diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 518d8bdd..d0c243bb 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -411,7 +411,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) "Unreachable: improper variant id for result type" | TError -> cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta - "TODO: error message"; + "Ill-formed error value"; 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" @@ -422,7 +422,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) let variant_id = Option.get variant_id in if variant_id = fuel_zero_id then ( cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta - "TODO: error message"; + "Ill-formed full value"; "@Fuel::Zero") else if variant_id = fuel_succ_id then match field_values with @@ -435,7 +435,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env) "Unreachable: improper variant id for fuel type" | TArray | TSlice | TStr -> cassert_opt_meta __FILE__ __LINE__ (variant_id = None) meta - "TODO: error message"; + "Ill-formed value"; let field_values = List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values in diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 91ee16dc..12b3387a 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -1402,9 +1402,9 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) : { fwd_info; effect_info = loop_fwd_effect_info; ignore_output } in - cassert __FILE__ __LINE__ + sanity_check __FILE__ __LINE__ (fun_sig_info_is_wf loop_fwd_sig_info) - def.meta "TODO: error message"; + def.meta; let inputs_tys = let fuel = if !Config.use_fuel then [ mk_fuel_ty ] else [] in @@ -1444,10 +1444,10 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) : (* Introduce the forward input state *) let fwd_state_var, fwd_state_lvs = - cassert __FILE__ __LINE__ + sanity_check __FILE__ __LINE__ (loop_fwd_effect_info.stateful = Option.is_some loop.input_state) - def.meta "TODO: error message"; + def.meta; match loop.input_state with | None -> ([], []) | Some input_state -> diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index b9eebc25..177d8c24 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -77,7 +77,7 @@ let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta) ctx_adt_get_instantiated_field_types ctx id adt.variant_id generics | TTuple -> cassert __FILE__ __LINE__ (generics.regions = []) meta - "Regions should be empty TODO: error message"; + "Tuples don't have region parameters"; generics.types | TAssumed aty -> ( match aty with diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index ccb4f585..4830f65a 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -458,9 +458,7 @@ let rec translate_sty (meta : Meta.meta) (ty : T.ty) : ty = match type_id with | T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics) | T.TTuple -> - cassert __FILE__ __LINE__ - (generics.const_generics = []) - meta "TODO: error message"; + sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; mk_simpl_tuple_ty generics.types | T.TAssumed aty -> ( match aty with @@ -486,7 +484,8 @@ 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 __FILE__ __LINE__ meta "TODO: error message" + | TArrow _ -> + craise __FILE__ __LINE__ meta "Arrow types are not supported yet" and translate_sgeneric_args (meta : Meta.meta) (generics : T.generic_args) : generic_args = @@ -659,7 +658,8 @@ let rec translate_fwd_ty (meta : Meta.meta) (type_infos : type_infos) | 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 __FILE__ __LINE__ meta "TODO: error message" + | TArrow _ -> + craise __FILE__ __LINE__ meta "Arrow types are not supported yet" and translate_fwd_generic_args (meta : Meta.meta) (type_infos : type_infos) (generics : T.generic_args) : generic_args = @@ -768,7 +768,8 @@ 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 __FILE__ __LINE__ meta "TODO: error message" + | TArrow _ -> + craise __FILE__ __LINE__ meta "Arrow types are not supported yet" (** Simply calls [translate_back_ty] *) let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool) |