New function colour: unsafe

I've been thinking about this for some time and may now found a solution.

Here I'll be talking now about "unsafe" v "safe" (and potentially v "utmostSafe") colouring only, but it could be applied to other function colouring as well.

Consider an unsafe call example:

var inited = false

unsafe func foo_unsafe(...) {
    if !inited {
        inited = true
        malloc(...)
        some_unsafe_call()
    }
    while condition1 {
        ...
        if condition2 {
            some_unsafe_call()
        }
        ...
        // some other safe code
    }
}

or anything similar and as complex as possible. As you've said we may have some knowledge about this code that compiler doesn't have, for example we know that at the time we want to use this call – unsafe paths will never be taken, so we put this call in the "unsafe" / "safeUnchecked" / "trusted" block (the name is under discussion):

/*safe*/ func bar() {
    safeUnchecked {
        // Note to the auditor:
        // I swear this call is safe under the current conditions:
        foo_unsafe(...)
    }
}

Now imagine that compiler is autogenerating an extra functions (as a result of some explicit opt-in, so it doesn't do this unnecessary):

var inited = false

/*safe*/ func foo_safe(...) {
    if !inited {
        inited = true
        fatalError() // unsafe code substituted
        fatalError() // unsafe code substituted
    }
    while condition1 {
        ...
        if condition2 {
            fatalError() // unsafe code substituted
        }
        ...
        // some other safe code
    }
}

with some method of name disambiguation which here is shown as bikesheded "_safe" suffix attached.

Now we can change our original bar to be safe without the need of "trust me" block:

/*safe*/ func bar() {
    foo_safe(...)
}

and if we do so we won't have the ability of lying or be mistaken!

Equally, if we do have a further distinction between "safe" and "utmostSafe" functions, then given a "safe" function:

/*safe*/ func baz_safe() {
    some_utmostSafe_code()
    if condition {
        safeUnchecked {
            // but we know it will never trigger unsafe parts
            some_unsafe_code()
        }
    }
    some_other_utmostSafe_code()
}

compiler could autogenerate the "utmostSafe" version:

utmostSafe func baz_utmostSafe() {
    some_utmostSafe_code() // utmost safe - so ok
    if condition {
        fatalError() // "just" safe so substituted
    }
    some_other_utmostSafe_code() // utmost safe - so ok
}

and now we'd be able calling the "utmost safe" version of baz() from "utmost safe" contexts.

This feels a bullet proof solution to me.


Edit: a more complete example that turns unsafe code into safe.

The transformation algorithm goes as follows:

  • if you have unsafe function you can make it safe by enclosing all internal callouts to unsafe functions in the "trust me" brackets.
  • if you hit a callout to some compiled / C / C++ / etc code which you can't change any further - replace those callouts with calls to fatalError
  • if all callouts in the "trust me" brackets are safe (or became safe after the previous transformation step) - those brackets could be removed.
Original unsafe code
/*safe*/ func main_safe() {
    some_code_safe()
    TRUST_ME_THIS_WONT_TRIGGER_UNSAFE_PATHS_I_SWEAR {
        op1_unsafe()
    }
}

unsafe func op1_unsafe() {
    some_code_safe()
    if condition {
        op2_unsafe()
    }
}

unsafe func op2_unsafe() {
    some_code_safe()
    if condition {
        malloc(...) // "leaf" unsafe code
    }
}
Safe code after the transformation
/*safe*/ func main_safe() {
    some_code_safe()
    op1_safe()
}

/*safe*/ func op1_safe() {
    some_code_safe()
    if condition {
        op2_safe()
    }
}

/*safe*/ func op2_safe() {
    some_code_safe()
    if condition {
        fatalError()
        // "leaf" / C / C++ / compiled / etc function was here, 
        // so we'd just replace it with "fatalError" without drilling any deeper.
        // if this path is triggered the assumption that "unsafe paths won't be
        // triggered" was false, but with "fatalError" here we know for sure
        // that unsafe code will not be triggered.
    }
}

We started with unsafe code (or the code that's claimed to be safe but safety of which was unchecked), and after this simple transformation we've got a safe version of this code, safety of which is now checked by the compiler. It's obvious how to do this transformation manually, and hopefully its equivalent could be performed by the compiler.