On 2013-04-03 16:33, Steven Schveighoffer wrote:

> I wish there was a way to say "this data is unchecked" or "this data is
> checked and certified to be correct" when you call a function.  That way
> you could run the in contracts on user-specified data, even with asserts
> turned off, and avoid the checks in release code when the data has
> already proven valid.

Scott Meyers had a good talk about this:

http://www.youtube.com/watch?v=Jfu9Kc1D-gQ

-- 
/Jacob Carlborg

On Wednesday, 3 April 2013 at 18:37:09 UTC, Jonathan M Davis wrote:
> ... you could do something like
>
> Verify!T verifyFoo(T param)
> {
>  //do checks...
>  return Verify!T(param);
> }
>
> void foo(T param)
> {
>  foo(verifyFoo(param));
> }
>
> void foo(Verified!T param)
> {
>  ...
>
> }
>
> That would be rather intrusive, but you _could_ do it if you wanted to.

What problems do you see with this (or similar) approach? I find it very straightforward and no overhead is really necessary. Isn't it exactly what type system is for - enforcing static guarantees in between different parts of application?

On Wednesday, April 03, 2013 21:05:19 Dicebot wrote:
> On Wednesday, 3 April 2013 at 18:37:09 UTC, Jonathan M Davis
> 
> wrote:
> > ... you could do something like
> > 
> > Verify!T verifyFoo(T param)
> > {
> > 
> > //do checks...
> > return Verify!T(param);
> > 
> > }
> > 
> > void foo(T param)
> > {
> > 
> > foo(verifyFoo(param));
> > 
> > }
> > 
> > void foo(Verified!T param)
> > {
> > 
> > ...
> > 
> > }
> > 
> > That would be rather intrusive, but you _could_ do it if you wanted to.
> 
> What problems do you see with this (or similar) approach? I find it very straightforward and no overhead is really necessary. Isn't it exactly what type system is for - enforcing static guarantees in between different parts of application?

It's verbose. You're adding a fair bit of boilerplate just to statically determine whether verification has been done or not. It may very well be worth it in many cases, but it's enough extra code that I don't think that I'd advise it as a general solution.

- Jonathan M Davis

On Wednesday, 3 April 2013 at 19:21:53 UTC, Jonathan M Davis wrote:
> It's verbose. You're adding a fair bit of boilerplate just to statically
> determine whether verification has been done or not. It may very well be worth
> it in many cases, but it's enough extra code that I don't think that I'd
> advise it as a general solution.
>
> - Jonathan M Davis

Erm, really? In most cases only wrapper type is needed. Almost all functions should accepts either verified or raw type version so no real boilerplate here (otherwise something is most likely wrong with your module responsibility organization). Wrapper types themselves are trivial and can be created automagically with some template/mixin. What else?

On 04/03/2013 07:42 AM, Lars T. Kyllingstad wrote:
> ...
>
> I personally think that, as a general rule, Errors should stay in
> production code.  I thought we had already separated -noboundscheck from
> -release, but I just tested now and that doesn't seem to be the case:
> -release still implies -noboundscheck.
> ...

It is more subtle than that. -release disables bounds checks in @system code. -noboundscheck disables bounds checks in @safe code.

On Wednesday, April 03, 2013 22:00:17 Dicebot wrote:
> On Wednesday, 3 April 2013 at 19:21:53 UTC, Jonathan M Davis
> 
> wrote:
> > It's verbose. You're adding a fair bit of boilerplate just to
> > statically
> > determine whether verification has been done or not. It may
> > very well be worth
> > it in many cases, but it's enough extra code that I don't think
> > that I'd
> > advise it as a general solution.
> > 
> > - Jonathan M Davis
> 
> Erm, really? In most cases only wrapper type is needed. Almost all functions should accepts either verified or raw type version so no real boilerplate here (otherwise something is most likely wrong with your module responsibility organization). Wrapper types themselves are trivial and can be created automagically with some template/mixin. What else?

The main issue I have with the wrapper is the fact that you're then forced to overload your function if you want it to test the argument for validity if it's not wrapped and not test if it's wrapped. So, you're creating an extra overload with every function that's using the wrapper to determine whether it should test or not. And if you're not creating those overloads, then there was no point in creating the wrapper in the first place.

- Jonathan M Davis

On 04/03/2013 10:01 AM, H. S. Teoh wrote:
> On Wed, Apr 03, 2013 at 09:19:24AM -0700, Ali Çehreli wrote:

>> Because the above is not the case today, if I write a function, I
>> cannot put the function pre-conditions in 'in' blocks because I don't
>> know whether my function is being called as an implementation of my
>> module or as an API function. The API function foo() may also be used
>> as part of the implementation of the same module. (Maybe the same
>> pre-condition checks should be repeated in the 'in' block and in the
>> body; as asserts and corresponding enforces.)
>
> This is very bad. It makes greatly diminishes the value of DbC in D.
> What are the obstacles preventing us from fixing DMD so that contracts
> are compiled with user code instead of library code?

The following thread is relevant but I don't remember whether it touches issues with dmd:

  http://forum.dlang.org/thread/kf19eh$14tv$1@digitalmars.com

Ali

On Wed, Apr 03, 2013 at 03:28:10PM -0700, Ali Çehreli wrote:
> On 04/03/2013 10:01 AM, H. S. Teoh wrote:
> > On Wed, Apr 03, 2013 at 09:19:24AM -0700, Ali Çehreli wrote:
> 
> >> Because the above is not the case today, if I write a function, I cannot put the function pre-conditions in 'in' blocks because I don't know whether my function is being called as an implementation of my module or as an API function. The API function foo() may also be used as part of the implementation of the same module. (Maybe the same pre-condition checks should be repeated in the 'in' block and in the body; as asserts and corresponding enforces.)
> >
> > This is very bad. It makes greatly diminishes the value of DbC in D. What are the obstacles preventing us from fixing DMD so that contracts are compiled with user code instead of library code?
> 
> The following thread is relevant but I don't remember whether it touches issues with dmd:
> 
>   http://forum.dlang.org/thread/kf19eh$14tv$1@digitalmars.com
[...]

Alright. Apparently Jonathan touched on some of the issues in the above
thread (quoted below):


[...]
> Unfortunately, while that's how it really _should_ work, AFAIK, there's no way with D's linking model to make things work that way. You can link against functions without any access to their bodies.
>
> Function pointers make it trivial to use a function without the compiler knowing what function your using (meaning that it couldn't insert the contracts at the call point).  Etc.  Etc. The contracts would have to be passed around with the functions in a manner which made it so that the caller could always insert them if it's being compiled with assertions enabled, and that just won't work.
[...]

This is not impossible to overcome.

One approach is to define contracts as separate (sub)functions that wrap around the real function according to some well-known scheme; say the contract is mangled as mangle(funcname)~"__contract" or something like that. The contract wrapper has exactly the same arguments/return value as the real function, and simply forwards them to the real function, and passes the real function's return value back.  Then when compiling in non-release mode, DMD will link all calls/references to the function to the contract wrapper instead, and when compiling for release, these calls/references go directly to the "real" function.

In essence, this code:

	RetType myFunc(Args...)(Args args)
	in { assert(inContract(args)); }
	out(RetType ret) { assert(outContract(ret)); }
	body {
		return dotDotDotMagic(args);
	}

	void main() {
		auto x = myFunc(1,2,3);
		auto fp = &myFunc;
	}

gets lowered to:

	RetType myFunc__contract(Args...)(Args args)
	{
		assert(inContract(args));
		auto retVal = myFunc(args);
		assert(outContract(retVal));
		return retVal;
	}

	RetType myFunc(Args...)(Args args)
	{
		return dotDotDotMagic(args);
	}

	void main() {
		version(release)
		{
			auto x = myFunc(1,2,3);
			auto fp = &myFunc;
		}
		else
		{
			auto x = myFunc__contract(1,2,3);
			auto fp = &myFunc__contract;
		}
	}

The *__in_contract wrappers are always shipped with the library, so library users can always choose to link to the contracted version or not. (Even if the library is compiled in release mode, the contract wrappers are still there, they are just bypassed by internal library calls. They can still be enforced when compiling user code in non-release mode, since the compiler will then route all calls through the wrappers.)


T

-- 
Real Programmers use "cat > a.out".

On Wednesday, 3 April 2013 at 21:44:36 UTC, Jonathan M Davis wrote:
> The main issue I have with the wrapper is the fact that you're then forced to
> overload your function if you want it to test the argument for validity if
> it's not wrapped and not test if it's wrapped. So, you're creating an extra
> overload with every function that's using the wrapper to determine whether it
> should test or not. And if you're not creating those overloads, then there was
> no point in creating the wrapper in the first place.
>
> - Jonathan M Davis

Imagine typical web app. It does want all string data used with db backend escaped to prevent any SQL injections. It does not want to add checks if data is escaped in every single db-related function because they aren't free and data is supposed to come in already escaped by user input validator.

Consider using wrapper types here. db backend functions don't need to accept raw data because they are supposed to get them already escaped. User input validation works with raw strings and can never receive wrapped ones from anyone.

It is like contract, but works in release and is verified by type system instead of custom code. You may just omit wrapper, of course, but you lose compile-time errors on attempt to send raw string to db then. That is huge difference.

On 2013-04-03 23:44, Jonathan M Davis wrote:

> The main issue I have with the wrapper is the fact that you're then forced to
> overload your function if you want it to test the argument for validity if
> it's not wrapped and not test if it's wrapped. So, you're creating an extra
> overload with every function that's using the wrapper to determine whether it
> should test or not. And if you're not creating those overloads, then there was
> no point in creating the wrapper in the first place.

Then you're doing it wrong. The point is that you should validate the data in one place. Then pass the validated data around. You can also turn it around. Instead of having Verified!(T) you could have Raw!(T). Where ever you get the input data from should return Raw!(T). You have one function accepting Raw!(T), validate. The rest of the functions accepts T.

-- 
/Jacob Carlborg