@require -- like assert but throws ArgumentError

[samoconnor]

@require is the same as @assert but it throws ArgumentError and generates an error message of the form "ArgumentError: $method_signature requires $condition".

function split{T}(c::T, n::Int)
    @require n > 0
    return SplitIterator{T}(c, n)
end

julia> split("xxx", 0)
ERROR: ArgumentError: split(::ASCIIString, ::Int64) requires n > 0

Note: this arrises from a request not to use the @assert macro for precondition assertions: #15409 (comment) .

Update: I prefer to call this @require (vs @precondition) in the tradition of DBC. I originally thought that would clash with Requires.jl, but it turns out that is not the case: #15495 (comment) .

[toivoh]

+1
Add a test as well?

Seems like 32 bit Travis timed out, anyone have an idea why that might happen?

[yuyichao]

This should not be a macro. It's much better to be a function. (and you don't want this to be inlined.)

[samoconnor]

That makes a lot of sense.
Done: samoconnor@258aa74

[nalimilan]

I find this interesting since it would raise the average quality of error messages. Most of the time, people write things like n > 0 || error("n must be strictly positive"), which doesn't say what n was (note this PR currently doesn't either, but it would be trivial to do it). And improving error messages to be more explicit about the actual values which were passed always require some thought about how to phrase it. With such a macro, one would get good error messages for free. Not having to start the debugger just to check what was the incorrect value makes a language much nicer to work with (just like rich BoundsError).

For the name, one could also think of @check, which sounds a bit more natural to me (and shorter).

FWIW, this makes me think of @requires and @ensures from the Midori project (the former identifier is still free, BTW): http://joeduffyblog.com/2016/02/07/the-error-model/#contracts. Using a macro instead of custom if clauses would indeed offer the advantages Joe Duffy talks about:

First, contracts written this way [i.e. as standard function calls] are part of the API’s implementation, whereas we want them to be part of the signature. This might seem like a theoretical concern but it is far from being theoretical. We want the resulting program to contain built-in metadata so tools like IDEs and debuggers can display the contracts at callsites. And we want tools to be in a position to auto-generate documentation from the contracts.

In their model, @ensures is symmetric to @requires, but is run on return from any code path. This is definitely beyond the scope of this PR, but it can be an argument in favor of moving in that direction.

[IainNZ]

Interesting idea, I like the concept at least. Counter-argument is maybe, does Base need yet another error checking condition type thing?

The @assert macro is kind of weird, as IIRC it just punts to assert and has no purpose at this time (although it seems like it'd be a smarter choice than a plain function as it could choose to generate no code at all if it detects a "release mode" type flag, see #8856).

[toivoh]

The @assert macro definitely has a purpose: it uses the assert condition to create the assertion error message. It could also be made to pick apart the assertion condition, just like @test does.

So @assert and @precondition (or @requires or whatever we would like to call it) and maybe @postcondition/@ensures would be very similar macros, even in the implementation, but I think that the semantic distinction is very important. You shouldn't use @assert to check preconditions, but I think that you should be allowed to do it with @precondition.

[mbauman]

Swift uses exactly this verbiage for something similar. Assertions are completely removed in optimized builds, whereas preconditions are only removed in unchecked builds. Interestingly, Swift still manages to propagate the precondition knowledge to LLVM even when the check is removed. So I can see a case here, too, even if we don't have the infrastructure (yet) to exploit it.

https://www.mikeash.com/pyblog/friday-qa-2016-03-04-swift-asserts.html

[samoconnor]

Add a test as well?

Done: samoconnor@9d75e4c

FWIW, this makes me think of @requires and @ensures from the Midori project

@nalimilan 😀
I think the idea of a Parisian attributing DBC and requires to the Midori project would amuse Bertrand Meyer. His ideas have certainly stood the test of time!
Midori definiely has ideas worth borrowing. e.g. #7026 (comment) and anything that Midori borrowed from Eiffel is probably a good thing to borrow again.

I originally used @requrie but that is apparently already in use.

@requires would suit me.

@mbauman The use of precondition in swift is interesting.

[samoconnor]

Disclosure of bias: I spent a couple of years in Santa Barbara working for eiffel.com in the late '90s. And, I later implemented Design by Contract in Tcl. Some might see that as a sign of madness.

[eschnett]

It seems that, to implement an @postcondition, one needs to wrap the whole function body. I would assume that one defines the postcondition near the beginning of the function body to keep it close to the precondition. However, testing it in all possible return paths requires wrapping the function.

@contract function f(x)
    @pre x>=0
    @post result>=0
    return sqrt(x)
end

could be translated into

function f(x)
    pre(x>=0, "x>=0")
    result = f_impl(x)
    post(result>=0, "result>=0")
    result
end
function f_impl(x)
    return sqrt(x)
end

I started implementing this in https://github.com/eschnett/Contracts.jl, but things got a bit tedious regarding interpreting the expressions representing the function and its various conditions, so I didn't continue.

I'm sure there is a simpler way to implement this, in particular if one uses macros for the pre-/post-conditions (as is suggested here). I used function calls that need to be inspected in the @contract macro.

[eschnett]

PS: To show off my experience with contract languages I'm using the Sather http://www1.icsi.berkeley.edu/~sather/Publications/article.html keywords here. (Sather is a close descendant of Eiffel.)

[samoconnor]

@eschnett, could @postcondition perhaps be done using try ... finally. i.e. the try part could return, but the finally part could still check the postcondition...

If I was being bold, I would even argue that function should have an optional finally clause.

e.g.

function f()
   ...
finally
   ...
end

[eschnett]

@samoconnor That's probably possible, but I think that would be much more expensive.

I think one might be able to use the do syntax:

post(cond) do
   ... original function body ...
end

where cond has been transformed from a condition to a lambda expression.

However, both approaches still require wrapping the whole function body. It might not be necessary to create a separate named function, but instead, a closure needs to be generated -- I don't think that's any easier nor more efficient.

[tkelman]

This strikes me as redundant and unnecessary, and overly complicated for the goal of pre populating an error message (and copy-pasting code is never a good sign). Backtrace collection is slow, this is collecting an extra one to add function name information to the error message that will already be in the backtrace. It's getting towards @test levels of printing actual values of the expressions, which is convenient but inefficient. If we're going to add a new mechanism for throwing exceptions, it should use a new exception type that can just store the input expression in a field and only convert to a string when it needs to show the error.

[samoconnor]

Does anyone know if there is a way to provide branch prediction hints to llvm from Julia? When I've implement contract checking systems in the past I've always used something like __builtin_expect (see http://llvm.org/docs/BranchWeightMetadata.html#built-in-expect-instructions ).

[eschnett]

@tkelman In case you were commenting on my post just above yours: What I showed was intended to show an example of the code that an expansion of an @post macro could produce. This isn't intended as user input (way too cumbersome). @samoconnor suggested not using a second function to hold the body of the function, and I was brainstorming on ways in which this could be implemented.

[tkelman]

@eschnett no I wasn't commenting on postconditions since this PR isn't doing that yet, I was commenting on what this PR currently implements.

[nalimilan]

@tkelman You're right that an implementation should be found to avoid any performance impact on the normal case. But do we care about performance when an ArgumentError is raised? This kind of exception shouldn't occur in production. Anyway, I'm not particularly attached to repeating the function signature in the error message, as long as the name of the argument and its value are present.

@samoconnor I have to admit I know very little about Eiffel (too bad for my French chauvinism...). Regarding your PR, what do you think of showing the passed value of the invalid argument in addition to the condition? For example, f(n::Int) requires n > 0, but -3 was passed, or f(n::Int) requires n > 0, got -3.

[eschnett]

@samoconnor You can use http://llvm.org/docs/LangRef.html#llvm-expect-intrinsic . I tried this recently (see below for an incomplete sketch), but code quality was reduced (!), so I didn't investigate further.

@generated function llvm_expect{I}(x::Union{Bool, IntTypes}, ::Type{Val{I}})
    # I::Integer
    lt = llvmtypes[x]
    ival = isa(I, Bool) ? Int(I) : I
    decls = """
        declare $lt @llvm.expect.$lt($lt, $lt)
    """
    instrs = """
        %res = call $lt @llvm.expect.$lt($lt %0, $lt $ival)
        ret $lt %res
    """
    quote
        :(Expr(:meta, :inline))
        llvmcall(($decls, $instrs), $x, Tuple{$x}, x)
    end
end
@inline llvm_assume(cond::Bool) =
    llvmcall(("""
            declare void @llvm.assume(i1)
        """, """
            call @llvm.assume(i1 %0)
            ret void
        """), Void, Tuple{Bool}, cond)

[MikeInnes]

I originally used @requrie but that is apparently already in use.

FWIW @require is completely available, since Requires.jl is horribly broken on 0.5 for all sorts of other reasons :)

[samoconnor]

@eschnett thanks for sharing your experience with llvm.expect, I might leave further investigation of that to someone with more llvm knowledge. For now the PR has a FIXME in the code as a reminder to revist.

[samoconnor]

@nalimilan, I agree with your conclusion that performance is moot in the failure case. The only place that has any business catching a contract violation is the REPL, a debugger, a test engine, or similar. The implementation in this PR could be made more efficient by passing just the current frame rather than doing stacktrace()[1]. But I think that kind of optimisation is premature at this point.

I very much like the idea of including the value that caused the failure (and maybe also the other function argument values). Perhaps: f(n = -3, a = [1,2,3...]) requires n > 0. I believe that @test does something along these lines. My plan was to leave that to a later PR.

If this PR is accepted and people start writing @preconditions then everyone will benefit form whatever auto-magic error message construction is added later. (There other potential benefits to having a specific notation for precondition, e.g. static contract checking, code generation hints / optimisations etc).

[eschnett]

If you have a macro just for the precondition, then it cannot capture the function arguments. If you add a macro before the function (similar to @inline), then you can examine the whole function body, and can automatically insert the function argument values into the error message.

[samoconnor]

This strikes me as redundant and unnecessary etc etc...

@tkelman there is plenty of literature and practical experience on this topic. If you want to be better informed, a good place to start might be: Applying “Design by Contract, Meyer, IEEE Computer, 1992

[samoconnor]

FWIW @require is completely available,

@MikeInnes thanks for pointing that out. @require is certainly my first choice for a name.

[samoconnor]

renamed @precondition to @require.
Cleaned up implementation.

[MichaelHatherly]

Since macros can have optional arguments now @require could be defined a bit shorter as

macro require(precondition, msg = string(precondition))
    :(if ! $(esc(precondition)) precondition_error($(esc(msg)) end)
end

(+1 to having a @require in Base.)

[samoconnor]

Thx for the tip @MichaelHatherly

[tkelman]

I still don't like this. I think experimenting with more advanced forms of design by contracts is better done out in packages for now, and this macro by itself is just slightly standardizing the error message which isn't worth the double collection of backtraces. Actually doing some interesting and worthwhile analysis with the precondition would require a different exception type that saves an Expr of the precondition, or does an outer macro annotation of the entire function declaration.

edit: To be more constructive, I'd be fine with a version of this that made throwing a precondition violation very cheap, and deferred any string concatenation and/or backtrace collection until such an exception gets displayed.

[StefanKarpinski]

Yes, this should definitely go in a package for now.

[samoconnor]

@StefanKarpinski my motivation for this was just to be able to use simple precondition asserts in a PR for Base. I'm not in favour of adding a full DBC system to Julia at this point.

I have code like this which is apparently not allowed because @assert does not throw ArgumentError.

function batchsplit(c; min_batch_count=1, max_batch_size=100)
    @assert min_batch_count > 0
    @assert max_batch_size > 1

It seems unfortunate to have to write it out like this... (which is why I'm proposing @require)

function batchsplit(c; min_batch_count=1, max_batch_size=100)
    if !(min_batch_count > 0)
        throw(ArgumentError("batchsplit(c) requires min_batch_count > 0"))
    end
    if !(max_batch_size > 1)
        throw(ArgumentError("batchsplit(c) requires min_batch_size > 1"))
    end

I'm happy to write the preconditions out long-hand if that is what you prefer.

Would you accept a PR for a non-exported @require in Base? The macro itself is quite trivial:

macro require(precondition, msg = string(precondition))
    esc(:(if ! $precondition Base.precondition_error($msg) end))
end

[StefanKarpinski]

It sort of makes sense but I'm not sure that that the kind of error raised matters enough given our current exception system (which doesn't really care about exception types much), and it feels half-baked without a corresponding postcondition macro, which would need a mechanism to ensure covering all exit paths. Once we have something like defer that can implement postconditions correctly and an exception system that makes the kind of exception raised more important, then this could certainly make sense, but for now, I think this doesn't buy us much.

[samoconnor]

Ok, so in the meantime, are happy for me to write @assert min_batch_count > 0 at the top of a function where a negative batch count makes no sense?

[tkelman]

It seems unfortunate to have to write it out like this

Throwing ArgumentError with a descriptive message is the current idiomatic style of error handling for user-facing code.

tkelman@linux:~/Julia/julia-0.5> grep '@assert ' -R base | wc -l
89
tkelman@linux:~/Julia/julia-0.5> grep 'assert(' -R base | wc -l
25
tkelman@linux:~/Julia/julia-0.5> grep 'ArgumentError(' -R base | wc -l
542

[MikeInnes]

Quick postcondition prototype, possibly only working on Lazy/MacroTools master:

using MacroTools
import Lazy: tailcalls

macro post(ex)
  @capture(shortdef(ex), cond_ -> f_(args__) = body_) ||
    error("invalid @post syntax")
  @gensym ret
  body = tailcalls(body) do ex
    :($ret = $ex;
      @assert $cond;
      $ret)
  end
  return esc(:($f($(args...)) = $body))
end

@post (n == 0) ->
function foo(x)
  n = 0
  rand(Bool) && (n += 1; return x^3)
  x^2
end

[eschnett]

Can one access the function's return value with this approach? In the long run, you also want the original values of the function arguments available in the postcondition.

[MikeInnes]

You get access to whatever's in scope at the point of return, so both of those things are possible. In the above example you can just acess x directly, and if you want to acess the return result you can do return result = x^2 to bind it.

[samoconnor]

Something along these lines might work...

function foo(x)
    @require x > 0
    @ensure n == 0
    n = 0
    rand(Bool) && (n += 1; @return x^3)
    @return x^2
end

@ensure could generate a local function postcondition = result -> @assert n == 0.

@return x could generate (_x = x; postcondition(_x); return _x)

or it could expand to something like this...

function foo(x)
    @assert x > 0

    @goto _start
    @label _postcondition
    @assert n == 0
    return result
    @label _start

    n = 0
    rand(Bool) && (n += 1; (result = x^3; goto _postcondition)
    result = x^2; goto _postcondition
end

[toivoh]

Or how about an ensure macro that takes an explicit block of code and
checks the postconditions when the block exists (it could generate a
try-finally? Then the design by contact machinery wouldn't have to be tied
to entry and exit of functions at all, and there would be no need for new
language support.
On 13 Apr 2016 02:23, "samoconnor" [email protected] wrote:

Something along these lines might work...

function foo(x)
@require x > 0
@Ensure n == 0
n = 0
rand(Bool) && (n += 1; @return x^3)
@return x^2end

@Ensure could generate a local function postcondition = result -> @Assert
n == 0.

@return x could generate (_x = x; postcondition(_x); return _x)

—
You are receiving this because you commented.
Reply to this email directly or view it on GitHub
#15495 (comment)

[Tetralux]

@toivoh I initially had the same thought, however try blocks are way too slow for this. They would slow down the code by an order of magnitude.

Edit: Fixed some typos.

Something like this would be better - at least as a stop-gap:

function ...(n::Integer)
  @require n == 0
  @ensure @result > 0, iseven(@result) begin
    n *= 2
    (n % 2 == 0) || (return n + 1)
    return n
  end
end

which could expand to:

function ...(n::Integer)
  (n == 0) || throw(ContractViolation("required n == 0; got n = $n"))  

  @gensym ret
  n *= 2
  if !(n % 2 == 0)
    ret = n + 1
  else
    ret = n
  end
  (ret > 0) || throw(ContractViolation("ensured @result > 0; got $ret"))
  iseven(ret) || throw(ContractViolation("ensured iseven(@result); got $ret"))
  return ret
end

Of course, ideally you wouldn't have to wrap the returns in a block for it to work. Perhaps with some other functionality that the @ensure macro could just call upon.

function ...(n::Integer)
  (n == 0) || throw(ContractViolation("required n == 0; got n = $n"))
  ccall(:jl_ensure, :(@result > 0))
  ccall(:jl_ensure, :(iseven(@result)))

  n *= 2
  (n % 2 == 0) || (return n + 1)
  return n
end

In this case, the expressions passed to jl_ensure get checked immediately after return.
They could of course be closures--or even pure functions instead, which could take the values they care about--or some kind of reference to the local scopes' variables--as arguments and then called by Julia transparently; immediately after return, but before the scope is destroyed.

The only remaining issue would be how to---if indeed it would be required---have the name of the enclosing function (and also presumably, the specific method) which these contract-statements were declared in, be shown in the error message.

[Tetralux]

@toivoh Fixed numerous typographical errors.

[eschnett]

On Wed, Apr 13, 2016 at 6:18 AM, H-225 [email protected] wrote:

@toivoh https://github.com/toivoh I initially had the same thought,
however try blocks are way too slow for this. They would slow down the
code by an order of magnitude.

Something like this would be better - at least as a stop-gap:

function ...(n::Integer)
@require n == 0
@Ensure @Result > 0, iseven(@Result) begin
x *= 2
(x % 2 == 0) || (return x + 1)
return x
endend

which could expand to:

function ...(x::Integer)
(x == 0) || throw(ContractViolation("required x == 0; got x = $x"))

@gensym ret
x *= 2
if x % 2 == 0
ret = x + 1
else
ret = x
end
(ret > 0) || throw(ContractViolation("ensured @Result > 0; got $ret"))
iseven(ret) || throw(ContractViolation("ensured iseven(@Result); got $ret"))
return retend

Of course, ideally you wouldn't have to wrap the returns in a block for
it to work. Perhaps with some other functionality that the @Ensure macro
could just call upon.

function ...(x::Integer)
(x == 0) || throw(ContractViolation("required x == 0; got x = $x"))
ccall(:jl_ensure, :(@Result > 0))
ccall(:jl_ensure, :(iseven(@Result)))

x *= 2
(x % 2 == 0) || (return x + 1)
return xend

In this case, the expressions passed to jl_ensure get checked immediately
after return.
They could of course be closures--or even pure function instead, which
take the values they care about as arguments and then called by Julia
transparently; immediately after return, but before the scope is destroyed.

The only remaining issue would be how to---if indeed it would be
required---to have the name of the enclosing function (and also presumably,
the specific method) which these contract-statements were declared in, be
shown in the error message.

Ideally, you also capture the initial value of the function's arguments, as
you often want to use them in the postcondition. I don't think it's too bad
if you add a special macro in front of the whole function, as in <
https://github.com/eschnett/Contracts.jl>. This also allows you to have
both pre- and postconditions near the function's top where they are easy to
spot.

@def function f(x, y)
    requires(x < y)
    ensures(result > x)
    x^2 + y^2
end

-erik

Erik Schnetter [email protected]
http://www.perimeterinstitute.ca/personal/eschnetter/

[toivoh]

Well, I guess there's no point in checking for contact violations if the function exits through an exception. In that case it should be fine to just find all points in the code that could cause transfer of control out of the block. That would include return, but also break, continue, and @goto, in some cases, and it would be a bit of redoing the compilers job to check in which cases.
@JeffBezanson: Any chance that try/finally could be made fast enough to be useful for this kind of case?

[Tetralux]

@toivoh It would certainly be good if the try statement could be "speed-boosted". @JeffBezanson