Correctness, distinct, mutability, effects, exceptions

!!! warning This auditors' handbook is frozen and obsolete; the Nim language manual alongside other Nim documentation, Status Nim style guide, Chronos guides, and Nim by Example supercede it.

The Nim compiler provides several constraints that can be used to enforce proper usage of variables, types and error handling at compile-time.

One was already mentioned in previous paragraphs:

  • Side-Effect analysis via using func or {.noSideEffect.} (in the routines chapter)

Note that range types currently work at runtime only

Side-Effect

As mentioned in the routines chapter, using a func or a proc tagged with {.noSideEffect.} will prevent reading or writing to global variables (i.e. variables that are neither parameters or locals).

Note that side-effect analysis cannot analyse raw emitted C code

Additionally, allocating a sequence or a string, even if they technically access a global memory allocator, is not considered a side-effect.

The compiler will ignore statements in a {.noSIdeEffect.} block for the purpose of side-effect analysis. At the moment this is only used for trace and some debug logs, as writing to stdout/stderr is considered writing to a global variables and so a side-effect.

not nil

The compiler exposes a "not nil" annotation for reference and pointer types. This enforces that parameters are proven always initialized in tagged:

  • procedures
  • types

This is not used in the codebase as a more powerful prover is required for our application.

Currently, the compiler warns when it cannot prove that a result reference is not nil.

distinct types

A distinct type is a type that has the same representation as a base type at a low-level but cannot be used in its stead.

type Miles = distinct float32
type Meters = distinct float32

Procedures accepting:

  • float32 will not accept Miles or Meters
  • Miles will not accept float32 or Meters
  • Meters will not accept float32 or Miles

distinct type can reuse the base type procedures and fields via the borrow annotation as described in the manual (https://nim-lang.org/docs/manual.html#types-distinct-type)

Enforcing exception handling

The codebase uses a mix of Result and Exceptions for error handling with option types and bool in some cases.

As an effort to sanitize error handling and ensure that all exception paths are handled, we use the effect tracking system the following way:

proc foo() {.raises: [].} =
  discard

The procedure above will refuse to compile if its body can throw an unhandled exception.

proc foo() {.raises: [ValueError].} =
  discard

The procedure above will refuse to compile if its body can throw an exception besides a ValueError.

In particular Nim distinguishes between Defects, which are non-recoverable, and Exceptions, which we should recover from.

For our purposes, we allow all procedures to throw a Defect (for example an assertion broken), this is done by adding {.push raises:[Defect]} at the start of a file

{.push raises:[Defect]}

proc foo1() =
  discard

proc foo2() =
  discard

{.pop.}

Mutability

Only variables declared with var and var parameters are mutable.

Note that mutability analysis is not deep for reference types or pointer types. You can always mutate through a pointer.

Future

Significant improvements are in-progress planned to improve Nim safety:

however it is too early to use them in a production codebase.