stedolan / crowbar

Property fuzzing for OCaml
MIT License
180 stars 31 forks source link

What is the best way to avoid stack overflows with recursive generators? #58

Open wilcoxjay opened 4 years ago

wilcoxjay commented 4 years ago

I'm new to the library, and I tried reading through the source code and all existing open and closed issues and PRs, but I couldn't find any guidance to this.

I have a simple recursive generator for a tree datatype that causes stack overflows when tested extensively (on the order of millions of executions). What should I do to work around this? (By the way, I tried using lazy/unlazy and fix, but the problem occurs with both.)

I saw some reference to a trick where you "pull constants out of the choose", but I couldn't quite figure out what that meant or how to do it.

Thanks!

stedolan commented 4 years ago

Can you post the generator in question?

'pulling constants out of choose' is something Crowbar does internally. When a recursive generator is building too large a structure, it tries to halt the recursion by picking cases in a choose that are of the form Const foo. (Of course, this only works if your recursion has such cases!)

wilcoxjay commented 4 years ago

Here's the generator (out of context)

let rec expr_gen =
  lazy (
      choose [
          map [bytes] Syntax.STLC.var;
          map [bytes; ty_gen; unlazy expr_gen] @@ Syntax.STLC.lambda;
          map [unlazy expr_gen; unlazy expr_gen] @@ Syntax.STLC.app;
          map [bool] @@ Syntax.STLC.bool;
          map [unlazy expr_gen; unlazy expr_gen; unlazy expr_gen] @@ Syntax.STLC.ifthenelse
        ])
let lazy expr_gen = expr_gen

I see now that it doesn't have any explicit constants in it, but it would be easy for me to manually transform the map [bool] into two constant cases, and even to hard code a variable name to add a constant case for variables as well. I'll try it!

stedolan commented 4 years ago

Right, adding even a single constant to this should fix the problem. With this generator, when Crowbar runs out of space it has no idea how to stop, since all of the options are map.

wilcoxjay commented 4 years ago

Excellent, thanks!

Would you be amenable to a PR that prints a warning if size <= 1 but there are no without branchy choices?

wilcoxjay commented 4 years ago

Also, while I'm looking, what's the deal with this function that always returns false?

https://github.com/stedolan/crowbar/blob/c8209e74aefe37cfdefc8fd4878e74426561c3ee/src/crowbar.ml#L237

wilcoxjay commented 4 years ago

I just had a chance to try this again with the fix of adding at least one constant inside the choose, but I still get stack overflows after a few million executions. Here's the new generator

let rec expr_gen =
  lazy (
      choose [
          const (Syntax.STLC.bool true);
          const (Syntax.STLC.bool false);
          map [bytes] Syntax.STLC.var;
          map [bytes; ty_gen; unlazy expr_gen] @@ Syntax.STLC.lambda;
          map [unlazy expr_gen; unlazy expr_gen] @@ Syntax.STLC.app;
          map [unlazy expr_gen; unlazy expr_gen; unlazy expr_gen] @@ Syntax.STLC.ifthenelse
        ])
let lazy expr_gen = expr_gen
stedolan commented 4 years ago

(found some time to hack on this again...)

Turns out I broke the size <= 1 case at some point, so the logic I was describing above didn't work. Just pushed a fix.

Something to detect this case would definitely be good.