Issue 13185 - Detect precondition violations at compile time when possible

[yebblies]

Implement compile-time contract checks for preconditions with the following limitations:

• Precondition contains only a single assert
• Parameters are value types or immutable
• Arguments are constant expressions
• Assert condition consists of only integer constants, parameters and comparisons

https://issues.dlang.org/show_bug.cgi?id=13185

[bearophile]

I like compile-time tests, I'm asking for them since years. But I think this makes the D specs more complex, making it harder the creation of alternative D front-end, and it seems far from a principled and general solution. And expanding the number of checks makes the situation worse. So instead of this I'd like a more general solution, (like "enum pre-conditions", as explained in Issue 13185 and in various D newsgroup posts). Adding a language feature allows to keep the front-end more clean and better specified, allows the D users to define more general constraints, allows to use the CTFE of D in an explicit way, it makes the code more self-documenting, and perhaps in the end may even keep the front-end code simpler.

[WalterBright]

Right now, there's a clear line between what's done at compile time and run time. This significantly blurs that distinction, in complex ways I think would be hard to document and explain to people. This kind of change needs a wider discussion.

[bearophile]

@walter:

Right now, there's a clear line between what's done at compile time and run time.

This is unfortunately false: switch cases act in a weird mix of compile time and run time:

#2887

https://d.puremagic.com/issues/show_bug.cgi?id=11613

[walter]

@bearophile I think you meant @WalterBright.

[bearophile]

Yes, sorry.

[WalterBright]

Yes, and people complain about it.

[yebblies]

Right now, there's a clear line between what's done at compile time and run time. This significantly blurs that distinction, in complex ways I think would be hard to document and explain to people.

This is just not true. The const-folder already detects errors such as division by zero, and out of bounds array accesses. The optimizer detects null dereferences. There is precedent for this kind of checking.

To document this we add one line to the spec for contracts - "the compiler may detect contract failures at compile time".

Other D compilers do not even have to implement this, because it's a diagnostic enhancement. Programs are still correct either way because they have the run-time check.

This kind of change needs a wider discussion.

I don't think it does, and I want to make sure you understand it properly before widening the discussion. Your response does not seem to match my understanding of what this pull does.

[tgehr]

@yebblies: One issue is that the extent of the additional diagnostic support can be queried at compile time and different code can be generated accordingly. I think there are no features that do not affect D code during run time.

[dnadlinger]

@yebblies: I think this is a complete no-go if it affects conditional compilation, which it seems to from a cursory glance at the implementation. It might be useful as an "ungaggable" error though.

[yebblies]

It behaves the same as the other constfold-detected errors, like division by zero and out-of-bounds indexing. eg

int divide(int a, int b)
in
{
    assert(b != 0);
}
body
{
    return a / b;
}

void main()
{
    static assert(is(typeof(divide(1, 0))));    // passes
    static assert(is(typeof(1 / 0)));           // passes
    static assert(is(typeof({divide(1, 0);}))); // fails
    static assert(is(typeof({cast(void)(1 / 0);}))); // fails
}

I don't see any way to implement it that would not affect conditional compilation. I'm not sure what the benefit of making it ungaggable would be?

@klickverbot Why would affecting conditional compilation be a deal-breaker?

I wouldn't mind it being a warning, although that would still have the same problems.

[andralex]

This is attractive, though I understand the objections. @WalterBright shall we cast a fresh eye on this?

[bearophile]

@andralex: in the meantime @WalterBright has essentially shot down my suggestion for "enum preconditions". So apparently now this patch (and similar ones) is all we can have...

[dnadlinger]

@yebblies: Seems like I never replied to this. The deal-breaker for me is that

Other D compilers do not even have to implement this, because it's a diagnostic enhancement.

is incompatible with a change in behavior that is observable via is(typeof()).

[yebblies]

Yeah, it's true that is(typeof()) makes everything a behavior change. So it would have to be a required part of the language.

But I still think this is worthwhile, and has precedent in the current behavior of the division by zero check. I think it's worth noting that is(typeof()) checks can be written in a way that would avoid triggering these errors. Also, note that a direct call inside typeof will not generate an error.

eg

static assert(is(typeof(divide(1, 0))));    // passes

[yebblies]

What about if I do this later, right before inlining? This would make it similar to the backend null dereference/div by zero errors, and would not affect is(typeof()). @klickverbot does that satisfy your concerns?

[dlang-bot]

Fix	Bugzilla	Description
✗	13185	Detect precondition violations at compile time when possible

[WalterBright]

The typeof problem can be resolved by disabling this if sc.intypeof is set. That is used in several places already.

The implementation also seems rather underpowered and duplicative. Why not simply ship the contracts off to CTFE to attempt to interpret? Then there are 3 outcomes:

1. interprets and passes
2. interprets and assert trips
3. does not interpret

and if (3) happens, just ignore it. Then, the capability of this is matched with the capability of CTFE.

[yebblies]

If we do that, the interpreter would attempt to call functions and other stuff that we don't necessarily want to speculatively interpret. The big issues here are:
4. Infinitely loops
5. Runs too slow

[dkorpel]

https://issues.dlang.org/show_bug.cgi?id=13185#c7