Introduce safety modes

[FedericoCeratto]

For some classes of applications safety, security and the ability to recover from exceptions and bugs are important. Nim could implement a safety option that:

• enables --checks:on
• enables --assertions:on
• enables --lineTrace:on (and therefore stackTrace)
• guarantees that any checked runtime error results in a catchable exception (see https://forum.nim-lang.org/t/5784)
• depending on the option e.g. safety:3, refuse to compile procs that use unsafe operations and inline asm (unless specifically tagged as safe?)
• pass extra sanitization flags to compilers and linkers as needed
• refuses to compile with any risky experimental features enabled
• enables any safety check that might be added to stdlib in future (e.g. when defined(safety): ...)

Related:

• https://nim-lang.org/docs/manual.html#definitions
• "Nim is unsafe" Nim is unsafe #4
• @Araq mentioned introducing -d:safety in Enabling some runtime checks in release mode Nim#2809 (comment)

[Araq]

Big -1 from me, we don't need more compiler and runtime modes, we need fewer. And let's also not conflate everything together, most experimental language features are about syntactic sugar and have no security impact.

[mratsim]

I'm not sure what kind of safety concerns you want to address but where safety is critical (aerospace, train scheduling systems, ...) what is required is completely different:

• A formally verified C compiler
• Provably correct software

See the guarantees levels Spark Pro offer: https://www.adacore.com/sparkpro

For me the biggest safety feature that we could bring is a spec extension (maybe similar to Crystal's) and have that compile to a formal verification language like Spin or TLA+ (tuto) and being able to check Nim code against the spec. Or we forge the spec extension and directly compile a restricted subset of Nim/stdlib to those languages.

This goes way beyond runtime checks or a borrow checker. This is similar to having a blueprint in civil or mechanical engineering, plan and verify the soundness of the design and then starting to build. This is not a replacement to runtime checks or Memory/Thread/AddressSanitizer by the way.

As an example, for Weave I was hunting several deadlocks and livelocks on my backoff mechanism (to put idle threads to sleep) and after spending a weekend dabbling into TLA+ I implemented my protocol, solved the logical and concurrency bugs (one did not exist with 2 threads, and was too rare with 8+ threads). Furthermore it allowed me to unravel a bug in glibc and musl condition variables where signaling them could be ignored, deadlocking the application. See mratsim/weave#56.

While I don't expect Nim to be run on planes or space shuttles anytime soon:

• Formal verification is big in the blockchain space and many DSL tout formal verification as a killer advantage.
• In particular formally verifying a program and then producing portable WASM code would probably be a very appealing.
• Concurrency, Distributed Computing and also commit schemes in databases often have design bugs that are very hard to hunt hence the use of TLA+ at Microsoft and Amazon for distributed design
• Beyond correctness it's also used to prove properties of protocols:
  • for blockchain, how many honest people needs there to be for the protocol to work: https://blog.trailofbits.com/2019/10/25/formal-analysis-of-the-cbc-casper-consensus-algorithm-with-tla/
  • for P2P messaging, can we guarantee that a sent message will be received: https://github.com/vacp2p/formalities/blob/master/MVDS/MVDS.tla
• Less known, cache-coherency protocols in chip design needs to be provably bug free

Side-notes

• I'd like a RFC on the potential Z3 backend for Nim btw.
• And also for the Nim language to not produce spurious ThreadSanitizer and AddressSanitizer warnings so that debugging low-level code is made easier.

Other references:

• Discussions spawned in AeroRust announcement: https://www.reddit.com/r/rust/comments/ejdv7w/announcing_aerorust_the_unofficial_working_group/

[Araq]

And also for the Nim language to not produce spurious ThreadSanitizer and AddressSanitizer warnings so that debugging low-level code is made easier.

At least that's addressed by --gc:arc.

[Araq]

I'm working on --panics:on/off (default is "off") that finally settles this cause. If panics are turned on you get the speed benefits of an optimizer that can assume that not everything can raise. If they are turned off, you can catch Defects just like today. For backwards compatibility --panics:off is the default.

[timotheecour]

when defined(safety):

s/safety/nimSafety/, new defined symbols need to be prefixed by package name (related: #181)

[arnetheduck]

Does this mean we'll get an effect to track panics as well? I mean, so that we can statically prove that no panics happen in a piece of code?

[timotheecour]

Seems needed to implement araqs's sfalwaysreturn in his PR...

[Araq]

Does this mean we'll get an effect to track panics as well? I mean, so that we can statically prove that no panics happen in a piece of code?

Probably yes, but I have no final design for it.

[timotheecour]

proposal

these already have a meaning and should keep their meaning:

raises: []. # cannot raise a CatchableError (but could raise a Defect)
raises: [OsError]. # can only raise a OsError amongst the Catchable ones (but could raise a Defect)

so we introduce a new pragma:

exceptions: []. # cannot raise any Exception (so can't raise any Defect either)
exceptions: [OsError]. # can only raise a OsError (and no Defect)
exceptions: [AssertionError]. # can only raise a AssertionError (and no other Defect, unless subclass of AssertionError of course)
exceptions: [AssertionError, IndexError]. # obvious meaning
exceptions: [Defect]. # obvious meaning
exceptions: [Exception]. # obvious meaning

[arnetheduck]

@timotheecour: raises: [] means "no Defect exceptions" presently - only some defects are actually tracked though, so it's a bit random: nim-lang/Nim#12862

after the PR by @Araq , there now seem to be 4 categories of errors to consider: Exception ("unknown, could be anything but you shouldn't really use this"), CatchableError ("you should catch these"), Defect ("you did something wrong with the API, you should maybe catch these") and panic/fatal ("you did something wrong with the API, and that API was part of the system library") - it would mean that some, but not all, of the things that are currently tracked by raises Defect will no longer cause that effect, so to detect them, we'd need something else.

Since the new proposed implementation depends on a compiler flag it means that if you're using a library that was written for one setting of the flag, and you're using raises, you can't mix that library with a library that was written for the other setting of the flag - on small projects that don't use raises this doesn't matter of course (which is most existing code, I guess - the low penetration of that particular feature is a signal perhaps?)

[Araq]

Why not simply .defects: [], .defects: [IndexError]?

[timotheecour]

there now seem to be 4 categories of errors to consider

no, it's simpler than what you describe;

• everything is derived by the exception hierarchy:

Exception < Defect,
Exception < CatchableError

• if an exception is subclass of CatchableError, it's catchable, else it depends on --panics:on/off

Why not simply .defects: [], .defects: [IndexError]?

i thought about that too, but exceptions unifies it under 1 base class, exactly matching the Exception hierarchy
This results in simpler (or equal) declarations in all cases:

exceptions: [] # same as your defects: [] raises:[]
exceptions: [IndexError] # same as your defects: [IndexError] raises:[]
exceptions: [OsError] # same as your defects: [] raises:[OsError]
raises: [OsError] # same as your raises:[OsError] # this could raise any defect, as well as OsError
raises: [] # same as your raises:[] # this could raise any defect, but no Catchable

note

everything is (obviously) expressible in terms of exceptions only, eg:

exceptions: [Foo], raises: [Bar] can be expressible as: exceptions: [Foo, Bar]
raises: [Bar] can be expressible as: exceptions: [Defect, Bar]

so raises is only for convenience of not having to specify Defect

[Araq]

everything is derived by the exception hierarchy

That's not true. (We could make it true though.) There is sysFatal (about to be renamed and exposed as panic) and --panics:on/off deals with panic whereas .raises is only concerned about the raise statement. But maybe keeping it tied to the exception hierarchy is the better idea. At least then there is only raise IndexError and not also raise IndexError vs panic IndexError.

[timotheecour]

ya, having a separate panic IndexError doesn't serve any useful purpose; tying to hierarchy makes sense

[arnetheduck]

But maybe keeping it tied to the exception hierarchy

this is very confusing in practice - the same constructs (try/catch and raises) being used for both "severities" of errors is difficult to educate around - it's "kind of" the same thing at that point - just another error, and deciding between the two when designing a library becomes very subjective - there's no clear boundary.

the consequence of having a global compiler flag for it is that you get completely different effects propagated through the code base making it impossible to mix panic:on and panic:off code - for example, it would be very hard to annotate the standard library itself with correct "raises" for both modes - this is a very real problem: almost everywhere where resources are managed in the standard library, there are leaks and errors because the code is not exception safe - these annotations should really be an explicit part of the standard library, because if you raise a new exception suddenly, that's a breaking API change.

[timotheecour]

but effect system tracks this so it only affects fwd decls

[Araq]

the consequence of having a global compiler flag for it is that you get completely different effects propagated through the code base making it impossible to mix panic:on and panic:off code

Why would you do that though... Just leave it turned off, isn't that what happened already? I introduced turning them on via --exceptions:goto (--gc:arc implies --exceptions:goto) and got so much backslash that I had to revert it.

[timotheecour]

IMO:

• the main (or only) use case for --panic:on is in getting extra performance (or smaller binary), just like -d:danger; it really is/should be orthogonal to --gc:arc or --exceptions:goto.
• some use case for catching a Defect (with --panic:off, the default) is for things like:
  • testing framework so that this works: doAssertRaises(AssertionError): badFunctionCall()
  • production servers that can't crash (or need to gracefully crash with cleanup code right after catching a Defect; eg honoring defer)
  • things like REPL's where user input could violate some API spec; eg: nim secret should NOT crash if user enters a command that raises a Defect

But other than that your application should usually not rely on Defect's being catchable as it should indicate a bug.

[Araq]

this is very confusing in practice - the same constructs (try/catch and raises) being used for both "severities" of errors is difficult to educate around - it's "kind of" the same thing at that point - just another error, and deciding between the two when designing a library becomes very subjective - there's no clear boundary.

Here is the problem: Let's assume that a panic Error is not the same as a raise Error. For raise you can use try except to catch it. For panic you need do use a recover errorHandler. Let's further assume that you really want to handle the panic and it must bubble up the call stack. What are you gonna do? So you write a raise statement in your errorHandler, you turn a panic into an exception. The optimizer must assume that every function call can fail. The programmer is also better off assuming this and to code appropriately, so nothing really was gained by Nim's exception tracking. IMHO.

[zah]

If we want to be able to have guarantees for panic-free (defect-free) code, then the current tracking of Defect already solves this. There are just issues that need to be resolved.

It's true that there are "educational" problems when it comes to the distinction between errors and defects, but I believe these problems will be present with any of the alternative proposals. Nim has few inappropriate defaults that exacerbate the problem:

1. Uneducated people tend to inherit from Exception. Nobody should do this, because it creates a third category of Errors. It's no longer possible to use the following pattern in the code:

prof foo() {.raises: [Defect, MyRecoverableError, OtherRecoverableError]`.}

Instead, you end up with procs that must be annotated with raises: [Exception] (see point 3 for more of this).

2. Uneducated people tend to write try: ..., except: .... This is currently bad, because it handles all defects. The default here should be CatchableError.

3. Uneducated people don't annotate their proc types and the default effect is set to raises: [Exception]. This is bad because it leads to libraries where the computed effect on all functions is raises: [Exception]. Such libraries are unusable in code that wants to use exception tracking. The language could be brave and set the default to raises: [Defect].

The two compilation modes (panics:on/off) are less of an issue in my opinion, because non-testing code should not discriminate between different types of defects by definition (defects are failures that are not anticipated in the normal operation of the program). Adding or removing defects to an API is a breaking change only when you are going from "no defects" to "some defects" and vice versa.

[Araq]

There is now a warning for (1) in Nim devel. Will do (2)-(3) for the upcoming release.

Edit: 2-3 are still to be done after 1.2.

[alehander92]

Whenever one says Uneducated people tend to do x bad simple pattern, he should try to think of a way to make that simple pattern a compiler warning/error (or a linter one): there is no other good way to educate people (focus on simple to detect/explain)

[Araq]

Uneducated people don't annotate their proc types and the default effect is set to raises: [Exception]. This is bad because it leads to libraries where the computed effect on all functions is raises: [Exception]. Such libraries are unusable in code that wants to use exception tracking. The language could be brave and set the default to raises: [Defect].

That's what Java did, the most important problem is that when your library uses callbacks (in Java's case: interfaces), you as the library author do not know if the callback can raise something or not.

[alehander92]

why not "generic" effects? function a raises exactly when arg callback b raises =>
proc a(b: proc: void {.raises: R.}): {.raises: R.} .. ? i guess too non-obvious api

[Araq]

The callback handler can also be inside an object, have fun with the complexities in the type system. ;-)

[mratsim]

This is bad because it leads to libraries where the computed effect on all functions is raises: [Exception]. Such libraries are unusable in code that wants to use exception tracking. The language could be brave and set the default to raises: [Defect]

There are seldom cases where it makes sense for a library to use exceptions instead of using errors or result/either.
In my experience that's for libraries where consumers are not software engineers but domain experts like in:

• scientific computing: matrix addition is easier to use when it returns a matrix
• mathematics: BigInteger addition is easier to use when it returns a BigInt

For most other cases (IO, streams, networking, serialization, ...), it makes more sense to use errors at the low-level and let/force consumer applications (not libraries) deal with the error.

This makes the error model part of the API (the raises: [MyNewException] is an alternative but in practice no one pushed it far enough to show it worked), this makes it easier to provide libraries to consume from other language, this avoids the mistake of Python of using exceptions for all control flow and only coding/testing for the happy path (i.e. all files are found, network connection is never lost, and there is always disk space).

[alehander92]

@Araq well .. you can annotate that if you really want :P :)

[Araq]

why not "generic" effects? function a raises exactly when arg callback b raises =>
proc a(b: proc: void {.raises: R.}): {.raises: R.} .. ? i guess too non-obvious api

Actually we have a variation of this rule in the effect tracking. It helps a little but also was complex to implement and I doubt many people understand it. ;-)

[zah]

Judging from the responses, I'm not sure my point about proc types was understood well, so I'll clarify.

Consider a library that uses a function pointer internally. For example, it may provide a user-hook or a callback for a certain operation. The library authors are likely to write their code like this:

type
  ClickHandler = proc (e: MouseEvent): bool

proc onClick(node: GuiElement, handler: ClickHandler) =
  node.clickHandler = handler

What happens next is that clickHandler is going to be called internally somewhere in the library. Since its effect is raises: [Exception] this infects every function that may end up calling it. For a sufficiently complicated library, all functions might be infected (for example, asyncdispatch fits that description).

If the language states that unannotated procs can raise only defects, a whole lot of usages of callbacks will stop compiling and the users will have to think about either handling the exceptions or providing a correct annotation for the callback.

[arnetheduck]

why not "generic" effects?

... or just make exceptions a strict requirement of the function signature - this is already kind of possible (but there are a few language features missing to make this truly convenient): func f[X, E: ref Exception](): Result[X, E] - in fact, I'd love to have this capability not just for callbacks but also for templates:

https://github.com/status-im/nim-stew/blob/76beeb769e30adc912d648c014fd95bf748fef24/stew/result.nim#L238

like that, Result works as a transport to capture the current exception and pass it to a different stack frame (because it will rethrow the same exception), but I'd like the Exception type to be forwarded perfectly as well - think that's not common? think async/await where the Future does this (in fact, after a future has been completed, it is semantically the same thing as a Result.

Being able to reason about the deduced exceptions is pretty useful in generic code, as evidenced by nothrow(bool) support in C++ - it's very commonly used to differentiate code paths so that code that can be shown to be exception-free (and thus amenable to reasoning / optimization) can be more efficient and elegant thanks to stronger guarantees.

the callback problem happens when type erasure is involved, which is when the callback registration is dynamic - but there are plenty of cases where that's not the case.

[arnetheduck]

...though one has to wonder why no modern language tries to follow java's footsteps and actually put specific exceptions in signatures through raises - C++ removed them, rust and go didn't add them and neither did swift (except raises or not).. clearly, they're not very convenient all things considered ;)

[Araq]

There are seldom cases where it makes sense for a library to use exceptions instead of using errors or result/either.
In my experience that's for libraries where consumers are not software engineers but domain experts like in ...
This makes the error model part of the API (the raises: [MyNewException] is an alternative but in practice no one pushed it far enough to show it worked), this makes it easier to provide libraries to consume from other language, this avoids the mistake of Python of using exceptions for all control flow and only coding/testing for the happy path (i.e. all files are found, network connection is never lost, and there is always disk space).

That's a programming language design fashion, ymmv. In my opinion garbage collection and exception handling are what enabled Python to grow its impressive set of libraries in the first place. And are responsible for Python's success. And yes, also its dynamic typing helped as you can emulate in your custom class what is required by the function f which comes from a thirdparty dependency.

For most other cases (IO, streams, networking, serialization, ...), it makes more sense to use errors at the low-level and let/force consumer applications (not libraries) deal with the error.

That doesn't match my experience at all. Exceptions are useful when errors, including IO errors, are pervasive.

[FedericoCeratto]

the mistake of Python of using exceptions for all control flow and only coding/testing for the happy path (i.e. all files are found, network connection is never lost, and there is always disk space).

A lot of of mission critical software is written in Python and injecting faults during functional testing is common practice.

One of the main benefit of exception is constraining failure modes: turning both known and unexpected failures from a system failure (e.g. a process crashing out) into loss of functionality of a subsystem.

[Araq]

This RFC has been implemented, closing. For defect tracking or other new features / warnings /etc we can create new RFCs.