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]?