[erlang-questions] Cannot make PropEr bitstring(B, U) generator to work

25 views
Skip to first unread message

Motiejus Jakštys

unread,
Sep 11, 2012, 10:06:56 AM9/11/12
to pro...@softlab.ntua.gr, erlang-q...@erlang.org
Hi,

I cannot get bitstring(B, U) to work. Here is a test case:

?FORALL(
B,
bitstring(8, 1),
true
).

I get this error when trying to execute it:

Error: The typeserver encountered an error:
{missing_type,demobucket_prop_eunit,{type,bitstring,2}}.

What am I doing wrong?

Tested on PropEr v1.0 and v1.0-62-g80c2c73 (latest master).

Thanks,
Motiejus Jakštys
_______________________________________________
erlang-questions mailing list
erlang-q...@erlang.org
http://erlang.org/mailman/listinfo/erlang-questions

Manolis Papadakis

unread,
Sep 11, 2012, 10:40:41 AM9/11/12
to Motiejus Jakštys, erlang-q...@erlang.org, pro...@softlab.ntua.gr
PropEr first tries to resolve the expression "bitstring(8, 1)" to a
generator, but that fails, because bitstring/2 is not a predefined
generator, and there's no custom generator with that signature declared
inside the module.

PropEr then tries to find a type with that name, but that fails as well:
bitstring/2 is not a predifined type (the way to express the same thing
in the type language is <<_:8,_:_*1>>), and there's no local type with
that signature.

Quick fix: If you're OK with using only unit values of either 8 or 1,
then you can use the predefined generator binary(Base) or
bitstring(Base) respectively. If you need other unit values, you'll have
to write a custom generator.

One might have expected something like the following to work:
-type my_bitstring() :: <<_:16, _:_*3>>.
prop_foo() -> ?FORALL(B, my_bitstring(), true).
But PropEr will currently reject this for unit values other than 1 and
8, because I suck at predicting what features people will want to use,
and thought this was a safe one to skip.

Motiejus Jakštys

unread,
Sep 11, 2012, 11:36:58 AM9/11/12
to Manolis Papadakis, erlang-q...@erlang.org, pro...@softlab.ntua.gr
On Tue, Sep 11, 2012 at 4:40 PM, Manolis Papadakis <mano...@gmail.com> wrote:
> PropEr first tries to resolve the expression "bitstring(8, 1)" to a
> generator, but that fails, because bitstring/2 is not a predefined
> generator, and there's no custom generator with that signature declared
> inside the module.

But... According to the Book of Wisdom[1], bitstring(B, U) is there.
And binary(S) is not. I haven't seen it before.

> PropEr then tries to find a type with that name, but that fails as well:
> bitstring/2 is not a predifined type (the way to express the same thing in
> the type language is <<_:8,_:_*1>>), and there's no local type with that
> signature.

Eh.. That would kinda do, but it raises a syntax error when used in
?FORALL context.

> Quick fix: If you're OK with using only unit values of either 8 or 1, then
> you can use the predefined generator binary(Base) or bitstring(Base)
> respectively. If you need other unit values, you'll have to write a custom
> generator.

Actually, I want binaries with length 0..1MiB-1:

?LET(
Len,
?LET(Len, integer(0, 1 bsl 20 - 1), Len),
{binary(Len), Len}
)

So for this, binary(Number) is sufficient.

> One might have expected something like the following to work:
> -type my_bitstring() :: <<_:16, _:_*3>>.
> prop_foo() -> ?FORALL(B, my_bitstring(), true).
> But PropEr will currently reject this for unit values other than 1 and 8,
> because I suck at predicting what features people will want to use, and
> thought this was a safe one to skip.

As said, I am only interested in full-byte binaries. So it was indeed
safe for this case.

Until 15 minutes ago how PropEr creates type instances was truly magic
for me. Now Eureka! For ones that are curious how it works:

x() ->
?FORALL(S, integer(0, 1023), S < 100).

translates to:
x() ->
proper:forall(S, fun(S) -> integer(0, 1023) end)).

So we have a closure which tries to execute the nonsense (that's what
I thought for more than a year).

After a lot of tracing I found out that this closure is executed in
context of `proper_types` moduke, which *has* a function integer(Low,
High). That's it. That function returnsa a nothing-magic tuple, and is
able to proceed.

And now answering my question. binary/1 is defined in proper_types. :)
All makes sense now.

[1]: http://proper.softlab.ntua.gr/papers/proper_types.pdf

Regards,

Manolis Papadakis

unread,
Sep 11, 2012, 11:57:00 AM9/11/12
to Motiejus Jakštys, erlang-q...@erlang.org, pro...@softlab.ntua.gr
On 09/11/2012 06:36 PM, Motiejus Jakštys wrote:
> On Tue, Sep 11, 2012 at 4:40 PM, Manolis Papadakis <mano...@gmail.com> wrote:
>> PropEr first tries to resolve the expression "bitstring(8, 1)" to a
>> generator, but that fails, because bitstring/2 is not a predefined
>> generator, and there's no custom generator with that signature declared
>> inside the module.
>
> But... According to the Book of Wisdom[1], bitstring(B, U) is there.

You're right, that should be there. Thanks for pointing it out. Crap,
now I'll have to find where I've put that code.

> And binary(S) is not. I haven't seen it before.

Yeah, there's lots of other stuff on the API, mostly convenience
functions and the like. You can find them all on the API documentation
page [1].

>> PropEr then tries to find a type with that name, but that fails as well:
>> bitstring/2 is not a predifined type (the way to express the same thing in
>> the type language is <<_:8,_:_*1>>), and there's no local type with that
>> signature.
>
> Eh.. That would kinda do, but it raises a syntax error when used in
> ?FORALL context.

Unfortunately, many expressions that are valid in a type expression
context are invalid Erlang terms, so there's no straightforward way to
use them in ?FORALLs directly (that's why my example below uses a custom
type as a thin wrapper for the binary type expression).

The types-in-place-of-generators feature is definitely a leaky
abstraction [2].

[1] http://proper.softlab.ntua.gr/doc/
[2] http://www.joelonsoftware.com/articles/LeakyAbstractions.html

Reply all
Reply to author
Forward
0 new messages