Skip to main content

Exceptions

Gitlab

In this report we show exceptions that are used in the Tezos Protocol. The exceptions listed here are raised by failwith raise raise_notrace or invalid_arg. Still, other exceptions may still occurr in the procotol code.

Exceptions are hard to formally verify, it is better if the code uses the error monad instead of exceptions. But this change reflects on the signature of functions which is not always desirable. We present suggestions for each file, what can be done to improve the code verifiability without sacrificing performance or idiomacity.

To easily distinguish these kinds of exceptions we use some emojis:

  • 👮 invalid_arg
  • 🚀 raise
  • 🚫 failwith

_Note that this report is based on the b9b6f296c32a3364b64992fe41f4454d14936dfd commit. It is done in this way so that the links in the report do not break.

Summary​

  • Number of occurrences
    • 👮 invalid_arg: 24
    • 🚀 raise: 6
    • 🚫 failwith: 20

apply_results.ml​

  • 🚫 Pervasives.failwith 🔗
    • Used in operation_data_and_metadata_encoding
    • It can be replaced by conv_with_guard which will use error monad instead of exceptions.

cache_repr.ml​

  • 👮 invalid_arg 🔗
    • Used in sanitize to create validate a new namespace, this is called by create_namespace too.
    • We can replace this by error monad to avoid the exception. It's hard to prove that this is impossible because it depends on the caller.
  • 👮 invalid_arg 🔗
    • Used in make_key to avoid duplicate namespaces. Note that this function returns a closure over a ref, which would be hard to verify. It's used on the register_exn.
    • Same as above, we can send it to the error monad
  • 🚫 failwith 🔗
    • Used in value_of_key when no handler for a key is found. This code involves a ref (!value_of_key_handlers) which holds state, it would be hard to verify it. We can sent it to error monad too, to avoid the exception, but this will not help with the reference.
  • 👮 then invalid_arg "Cache index is invalid" ; 🔗
    • Used in register_exn to avoid invalid cache index.
    • This is quoted in alpha_context.mli and cache_repr.mli, changing its return value would impact other code. It's better to keep it as it is.

contract_manager_storage.ml​

  • 🚫 | None -> failwith "get_manager_key" 🔗
    • Used in get_mananger_key when no ?error value is provided, otherwise this function uses the error monad
    • This already returns an result so we can send the error to the error monad instead of raising it

contract_services.ml​

  • 🚀 | None -> raise Not_found 🔗
    • Used in do_big_map_get_all when Big_map.exists ctxt id returns Ok (_, None)
    • Can be sent to the error monad.

contract_storage.ml​

⁉ This file 🔗 overrides failwith, the errors are not raised but sent to the error monad, the same solution can be done for other files. For functions that are already in the error monad this is trivial for other functions some work need to be done. I left this here for completeness 

let failwith msg = fail (Failure msg)
  • ⁉ failwith "Non implicit contracts cannot be removed" 🔗
    • Do not raise exception, uses the error monad instead.
  • ⁉ | (None, Some _) | (Some _, None) -> failwith "get_script" 🔗
    • Do not raise exception, uses the error monad instead.
  • ⁉ | None -> failwith "get_counter") 🔗
    • Do not raise exception, uses the error monad instead.
  • ⁉ | None -> failwith "get_balance") 🔗
    • Do not raise exception, uses the error monad instead.

cycle_repr.ml​

_exn functions are expected to raise exceptions, the problem is when other functions (like _opt for example) are implemented in terms of them but this is not the case. It's always possible to remove this and refactor code to use the error monad instead.

  • 👮 if Compare.Int32.(l >= 0l) then l else invalid_arg "Cycle_repr.of_int32_exn" 🔗
    • Used in of_int32_exn to filter out negative values
  • 👮 | None -> invalid_arg "Cycle_repr.of_string_exn" 🔗
    • Used in of_string_exn to filter non numeric values

entrypoint_repr.ml​

The same as previous file.

  • 👮 match of_string_strict' str with Ok v -> v | Error err -> invalid_arg err 🔗
    • Used in of_string_strict_exn to filter out invalid endpoints (too long or literally "default"
  • 👮 match of_string_lax' str with Ok name -> name | Error err -> invalid_arg err 🔗
    • Used in of_string_strict_exn to filter out invalid endpoints (too long)

gas_limit_repr.ml​

The same as cycle_repr

  • 🚫 failwith (string_of_int i ^ " should not be saturated.") 🔗
    • Used in integral_of_int_exn to filter out saturated values
  • 🚫 failwith (Z.to_string z ^ " should not be saturated.") 🔗
    • Same as above

indexable.ml​

The same as cycle_repr

  • 🚀 | Error _ -> raise (Invalid_argument "Indexable.index_exn") 🔗
    • Used in index_exn to filter out negative values
  • 🚀 | Error _ -> raise (Invalid_argument "Indexable.from_index_exn") 🔗
    • Used in from_index_exn to filter out negative values

legacy_script_patches_for_J.ml​

  • 🚀 | None -> raise (Failure "Decoding script failed.") 🔗
    • Used in bin_expr_exn because of decoding error
    • bin_expr_exn is then used in the decoding of various literal strings, it should be possible to show that these decodings do not fail.

non_empty_string.ml​

  • 👮 | "" -> invalid_arg "Unexpected empty string" 🔗
    • Used in of_string_exn to filter out empty strings.
    • There is a val of_string : string -> option version of this function, also this function is used in two places only and with literals "@" so we can show that this exception do not happen for this cases.

period_repr.ml​

  • 👮 | None -> invalid_arg "Period.of_seconds_exn" 🔗
    • Used in of_seconds_exn to filter negative values.
    • This is used in a lot of places, there is an of_seconds which is in the error monad so it's a matter of refactoring the code to remove the uses of _exn version.

raw_context.ml​

  • 🚫 | None -> failwith "Missing protocol parameters." 🔗
    • Used in get_proto_param when Context.find ctxt "protocol_parameters" fails. This is expected to never happen. The function is in the error monad anyway so it is just a matter of refactoring return the error instead of raising this.
  • 🚫 failwith 🔗
    • Also used in get_proto_param, but this time raised when Data_encoding.Json.destruct fails.
  • 🚫 | None -> failwith "Internal error: cannot read constants in context." 🔗
    • Used in get_constants, raises when Context.find ctxt constants_key fails.
  • 🚫 | None -> failwith "Internal error: cannot parse constants in context." 🔗
    • Used in get_constants too, raises on decoding error
  • 🚫 | None -> failwith "Internal error: un-initialized context." 🔗
    • Used in check_inited, raises when Context.find ctxt version_key fails
  • 🚫 failwith "Internal error: un-initialized context in check_first_block." 🔗
    • Used in check_and_update_protocol_version, raises when Context.find ctxt version_key fails.
  • 🚫 failwith "Internal error: previously initialized context." 🔗
    • Also used in check_and_update_protocol_version, raises when the value read from the context differs from the version_value literal.
  • 🚫 failwith 🔗
    • Used in get_previous_protocol_constants, raises when Context.find ctxt constants_key fails
    • This is annoted with [@warning "-32"], and it has a comment (* only for the migrations *)
    • This do not return a result so it's not trivial to replace the exception by the error monad
  • 🚫 failwith 🔗
    • Also used in get_previous_protocl_constants, raises when decoding fails
    • Same as above

raw_level_repr.ml​

  • 👮 | Error _ -> invalid_arg "Level_repr.of_int32" 🔗
    • Used in of_int32_exn to filter out negative values
    • There is an of_int32 version that send errors to the error monad.
    • It's used in Level_repr for example, there may be other places, it's heavily used in the tests too.

round_repr.ml​

  • 👮 invalid_arg "round_repr.succ: cannot apply succ to maximum round value" 🔗
    • Used in succ to filter out max_int value.
    • There are other succ/pred functions that use option, it's better than sending and error here. Of course that the caller can check if the value is max_int before calling succ too but this is not sound.
  • 👮 invalid_arg "round must be a non-negative integer" 🔗
    • Used in round_duration to filter negative values.
    • The same as the succ function above.

sampler.ml​

  • The invalid_arg function is used in check_and_cleanup to filter out negatives values which is then called by create. Which is then called in Delegate_storage.select_distribuition_for_cycle. I couldn't convince my self that this will never happen, the better would be to return a result so that select_distribution_for_cycle can propagate the error if needed.

  • 👮 else if Mass.(p < zero) then invalid_arg "create" 🔗

  • 👮 | [] -> invalid_arg "create" 🔗

sapling_storage.ml​

  • 🚫 then failwith "Invalid argument." 🔗
    • Used in get_diff, it uses Samplig.Commitment.valid_position to avoid invalid arguments.
    • This function should be using invalid_arg instead of failwith as the most of the rest of the code. Anyway this function already return a result Lwt.t so it would be easier to return the errors in the error monad.
  • 🚫 | Error () -> failwith "Invalid argument." 🔗
    • Also in get_diff, raised when List.combine fails, the same case as above.

saturation_repr.ml​

  • 🚫 else failwith (Format.sprintf "mul_safe_exn: %d must be below 2147483648" x) 🔗
    • Used in mul_safe_exn to avoid overflow. There is a option version of this so it is a matter of refactoring to not use the _exn version and then remove it.
  • 🚫 failwith 🔗
    • Same as above but in mul_safe_of_int_exn

sc_rollups.ml​

  • 🚫 failwith 🔗
    • Used in kind_of to avoid invalid module name. It excludes modules M where M.name is not "arith"
    • This is implemented on top of kind_of_string which is in option it's just can return an option and be handled by the caller.

script_cache.ml​

  • 🚫 failwith "Script_cache: Inconsistent script cache." 🔗
    • Used in value_of_identifier, this seems to mark unreachable code
    • From comment in the code

      ( [value_of_identifier ctxt k] is applied to identifiers stored in the cache. Only script-based contracts that have been executed are in the cache. Hence, [get_script] always succeeds for these identifiers if [ctxt] and the [cache] are properly synchronized by the shell. )

    • We can formulate the above comment as a predicate and try to verify it.

script_ir_annot.ml​

  • 🚀 | _ -> raise Exit) 🔗
    • Used in classify_annot to do short circuit a loop, it a not an error

seed_repr.ml​

  • The take_int32 and take_int64 could return option so the caller can handle this error, the former is used at Seed_repr.take_int32 seq (Int32.of_int max_snapshot_index), max_snapshot_index comes from let max_snapshot_index = Storage.Stake.Last_snapshot.get in Stake_storage. One example case of stored values invariants.

  • 👮 if Compare.Int32.(bound <= 0l) then invalid_arg "Seed_repr.take_int32" 🔗

    • Used in take_int32 to filter ou t negative values.
    • There is (* FIXME *) just above this

  • 👮 if Compare.Int64.(bound <= 0L) then invalid_arg "Seed_repr.take_int64" 🔗

    • Same as above but for take_int64

services_registration.ml​

  • 🚀 raise (Failure (Format.asprintf "%a" Error_monad.pp_trace t)) 🔗
    • Used in get_rpc_services, raised when rpc_init fails. get_rpc_services is called in mail.ml after Alpha_services.register (). It would be better to verify that rpc_init do not fail but this _init functions are hard to verify.

storage_description.ml​

These are used in the storage registrations during the initialization. The better would be to show that these errors could not happen, for example, that there are no duplicated names, so that the subcontext registration do not fail.

  • 👮 invalid_arg 🔗
    • Used in register_named_subcontext to signal the failure of a subcontext registration, this uses Format.kasprintf
  • 👮 invalid_arg 🔗
    • Used in register_indexed_subcontext to signal the failure of an indexed subcontext registration, this uses Format.kasprintf
  • 👮 invalid_arg 🔗
    • The same as above but to signal that another context is already registered with the same name
  • 👮 invalid_arg 🔗

tez_repr.ml​

There are safe versions of _exn as operators, */ for example. So the code should use those when it's not statically known that the exception will not be raised.

  • 👮 | Error _ -> invalid_arg "mul_exn" 🔗
    • Used in mul_exn to signal overflow
  • 👮 | Error _ -> invalid_arg "div_exn" 🔗
    • Used in div_exn to signal underflow
  • 👮 match of_mutez x with None -> invalid_arg "Tez.of_mutez" | Some v -> v 🔗
    • Used in of_mutez_exn to filter out negative values

tx_rollup_l2_qty.ml​

The same as the previous file

  • 👮 | None -> invalid_arg "Tx_rollup_l2_qty.of_int64_exn" 🔗
    • Used in of_int64_exn to filter out negative values.

Conclusion​

The most of the exceptions are used during the initialization of the blockchain. This has the effect that once the initialization finished there is room for assumptions about the initialized state. This is true during runtime. Some function that did not failed during the initialization have no reason to fail afterwards, but it's not obvious on what initialization effects it relies on. This make it hard to reason about the code.

This becomes obvious during the formal verification because we need to formulate the precondition and while searching it converges to storage state which is not statically derivable from the code.