autoremove unviolated precondition checks at compile time

[Toon Knapen]

I like to check the preconditions of a function explicitly by means of code (instead of only documenting them). Of course this incurs a time-penalty. 

When being extremely cautious every function in a call-chain will always check its preconditions. But for a function down in the call-chain, the precondition checks of all its callers might already guarantee that its own pre-condition checks will never be violated. And thus these checks down the chain are unnecessary cpu cycles. 

Do there exist tools/methods to detect this and auto-remove these precondition checks? 

For example:
the function Muladd below verifies that all arrays have the same length. Muladd relies on two functions to perform the `mul` and the `add` and each of these will also verify their respective preconditions explicitly. Given these functions are not exported and given these functions are only called by `muladd`, the compiler might be able to determine that the precondition checks are guaranteed to be valid and can thus be removed. 

https://go.dev/play/p/92isKKx-vYx

package main

import "fmt"

func main() {
    x := []float64{1.0, 2.0, 3.0}
    y := []float64{1.0, 2.0, 3.0}
    z := []float64{1.0, 2.0, 3.0}
    Muladd(x, y, z)
    fmt.Printf("%+v", x)
}

func Muladd(x []float64, y []float64, z []float64) error {
    // check precondition (but unnecessary if only called by Muladd)
    if len(x) != len(y) || len(x) != len(z) {
        return fmt.Errorf("slices have different lengths %d vs %d vs %d", len(x), len(y), len(z))
    }
    mul(x, y)
    add(x, z)
    return nil
}

func mul(x []float64, y []float64) error {
    // check precondition
    if len(x) != len(y) {
        return fmt.Errorf("slices have different lengths %d vs %d", len(x), len(y))
    }
   
    for i := range x {
        x[i] *= y[i]
    }
    return nil
}

func add(x []float64, y []float64) error {
    // check precondition
    if len(x) != len(y) {
        return fmt.Errorf("slices have different lengths %d vs %d", len(x), len(y))
    }
   
    for i := range x {
        x[i] += y[i]
    }
    return nil
}

[Henry]

You will need a build tag for that.

For example: 

In a separate file, define the build tag

```

// +build debug

package mypkg

func init() {

   Debug = true

}

```

Then, in other files, use the tag

```

package mypkg

var Debug bool

func DoWork() {

   if Debug {

      // perform validation

   }

}

```

When building with validation, call "go build -tags debug"

[Jan Mercl]

On Thu, Mar 31, 2022 at 5:27 AM Henry <henry.ad...@gmail.com> wrote:

> // +build debug
>
> package mypkg
>
> func init() {
> Debug = true
> }

Doing here instead

const Debug = true

removes (DCE) the runtime checks in other files.

[Toon Knapen]

but that would enable or disable _all_ precondition checks.

What I am looking for is soth. smart enough that deduces that the precondition checks in `mul` and `add` can be removed because of the precondition check in `Muladd`.

[Jan Mercl]

On Thu, Mar 31, 2022 at 10:01 AM Toon Knapen <toon....@gmail.com> wrote:

> but that would enable or disable _all_ precondition checks.

Sure, that's the point. Henry used the +build debug mechanism, so the
checks would be disabled in production. If one wants the checks to be
always present there's no need to use a debug build tag nor to wrap
the checks in a condition.

> What I am looking for is soth. smart enough that deduces that the precondition checks in `mul` and `add` can be removed because of the precondition check in `Muladd`.

What you need is a prover that understands the facts holding up the
callers' stack and can statically detect tautologies in the calees
checks. Not trivial, but I believe it would be a ton of fun to write
;-)

[Toon Knapen]

What you need is a prover that understands the facts holding up the
callers' stack and can statically detect tautologies in the calees
checks. Not trivial, but I believe it would be a ton of fun to write
;-)

Indeed, that is what I want to achieve. 

Are there any of these tools already? Maybe for other languages (that I can draw inspiration from) ?

 

[Axel Wagner]

There is a concept called "dependent types", which is more or less this. Wikipedia has a good overview of languages with dependent types:

https://en.wikipedia.org/wiki/Dependent_type#Comparison_of_languages_with_dependent_types

That being said, it's pretty complex stuff.

--
You received this message because you are subscribed to the Google Groups "golang-nuts" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/b9e2e539-f99e-4d44-9157-723cd11a0c2cn%40googlegroups.com.

[Henry]

You only need to validate in Mul and Add. They are the ones that work directly with the slices and know the reason behind such requirements. Muladd only needs to check for any error returned by either Mul or Add. In the future, if the requirement changes in either Mul or Add, you don't need to modify Muladd.

Anyway, I would not worry about such micro-optimization. I don't think such checks consume many CPU cycles. Your performance bottleneck is likely to come from something else. Just write clear codes, and profile your app later.  

PS: Thanks for the insight, Jan. I didn't know you could do that.