locked
PexForFun: unsolvable duels due to crazy bugs in Pex?

    Question

  • Hi,

    I had published a few PexForFun duels on boolean operators. They built up on each other, starting from very easy, then getting harder. Some ppl solved the hardest, some more were able to solve the ones before - while a particular one of the easiest, SimpleUnaryBooleanOp2, was not solved a single time...

    So I tried it again myself and found that the correct solution

     

    return p;
    

     

    (it's simple, as said, meant as preparation for the subsequent)

     

    ...yields the following result from Pex:

     pyour resultsecret implementation resultOutput/ExceptionError Message
    [FINE]falsefalsefalse  
    [NOPE]true (0x80)true (0x80)true (0x80)Mismatch Your puzzle method produced the wrong result.

    Huh, "Mismatch"?!

    I have no clue what's happening here, maybe someone from the Pex team has an explanation?

    __

    meisl

    p.s.: would have provided just a screen shot - just don't know how 8]

    Saturday, November 06, 2010 8:15 PM

Answers

  • Two fixes were applied to the website today:

    • Pex for fun should show which exception type should be thrown, if the secret implementation throws an exception, and
    • When comparing Boolean results in a Coding Duel, the strange observed behavior should be gone.

    Nikolai Tillmann
    Tuesday, November 16, 2010 3:52 PM
    Owner

All replies

  • I see. That's a bit unfortunate indeed.

    Excursion into what is happening: In the MSIL instruction set of .NET, Boolean values are represented as bytes (8 bits). Such a value represents False, if it's zero. All other byte values represent True. The C# compiler tries hard to always represent Booleans as 0 or 1. However, although you can't write it directly in C#, it's totally safe for .NET code to take any byte value, and pass it as an argument value for a Boolean parameter in a method call. Pex analyzes the code at the MSIL instruction set level, that's why Pex works for all .NET languages. Here, Pex passes True represented as the byte value 0x80. Then Pex calls the both implementations (the secret one, and the one from the user), which simply return them, and then Pex calls the Boolean.Equals method to compare the two results. The Boolean.Equals method loads the two values to be compared; the values are represented as bytes, but the way the MSIL instruction set works, they are extended to 32 bits when being loaded. Then they are compared. Interestingly, the way the Boolean.Equals is implemented, it zero-extends one value, and sign-extends the other. This has a strange consequence: Boolean.Equals does not consider certain True values as equal itself (those values where the highest-most bit is set, for example 0x80). Very strange, but not the fault of Pex. Pex just uncovers this behavior. We know about it, see for example here: http://www.bing.com/search?q=bytetoboolean&src=IE-SearchBox&FORM=IE8SRC

    I will change Pex for fun, so that it doesn't use Boolean.Equals to compare Boolean results in Coding Duels. I will leave this thread open until this has been released.


    Nikolai Tillmann
    Sunday, November 07, 2010 12:16 PM
    Owner
  • Wow!

    Isn't it fascinating how complex things there are that men have built?

    However, what strikes me most is that in spite of that there always seem to be some who are able "to read the matrix" - and on top of that to explain it :D So, BIG thanks for investigating, the great explanation and also for "quick-fixing" PexForFun w.r.t. that.

     

    Very strange, but not the fault of Pex. Pex just uncovers this behavior.

    Indeed, just another BIG point for the Pex project, I'd say. In fact, I would consider this implementation of Boolean.Equals a plain bug! Why not just use *the same kind of conversion* for both values?! Right now this feels like quite dramatic to me, not only impacting PexForFun, not only C#...

    Well, I'm not Neo, so there might very well be something that I'm overlooking.

    __

    meisl

     

    Sunday, November 07, 2010 7:45 PM
  • Yep, I found that out when I started trying the C# challenges and couldn't figure out a way to stimulate pex to workaround it.

    While we're on the topic of unsolvable challenges, "AnySecondNow" appears to use DateTime.Now.Second in its computations.  The problem is Pex doesn't seem to run your code and the secret implementation for the same inputs at exactly the same second, and runs different inputs at different seconds - so it's very difficult to end up with the same output for the entire set of inputs Pex analyses.  You can try various means to get lucky enough for Pex to think you've solved the challenge, but you might spend a lot of time trying...so maybe it would be better to ban Now.Second from Pex4Fun.

    There are a couple of other challenges where Pex says: "Your puzzle method should have violated the following contract: <...>".  If I express the reported condition using Contract.Requires() Pex complains that "Your puzzle method unexpectedly violated the following Contract -> Precondition failed <...>".  I haven't yet figured out how the secret implementation expresses the Contract in order to generate that kind of failure message.  Using Contract.Assert() or Ensures() does not generate the same report, Assume() is disallowed in Pex4Fun, and attempts to express the condition unnaturally using Exists() or ForAll() don't replicate the report either.  I assume there's a way because other people have solved TheVoiceIHearInMyHead, which has this issue.  Any idea what kind of contract expression is leading to these Pex messages?

     

     

     

     

     

     

     

     

    Monday, November 08, 2010 12:15 PM
  • Confirmed, same here.

    Actually non-determinism is quite interesting in this context, maybe have an extra discussion about it. For now, it's clear that things like Random, Environment and such are disallowed. So why isn't DateTime.Now? My guess is that only classes (or interfaces, e.g. IOrderedEnumerable [this one for a different reason]) as a whole can be disallowed... but then, not having DateTime, well...

    Anyhow, w.r.t. to AnySecondNow , I think I almost got it, after 45 attempts or so. I'm getting positive input right now, and don't have the energy to analyze the negative part (which wasn't really considered as it seems to me). Don't ask my why but retrieving DateTime.Now into a variable as the very first stmt seems to make it. Then here's another trick I learned: simply running the same solution again doesn't help (yes, that does make sense in the face of non-determinism). You only get the previous output from Pex, probably based on a hash in order to save computing time. So, to work around this, I keep adding "." to a line-comment :)

    Re reproducing Contracts with messages, as e.g. in TheVoiceIHearInMyHead (25 attempts so far...), I'm having the very same problem. There, particularly, is one that contains the actual parameter value - which I just cannot embed using a string literal as I am being told:

    Contract.Requires( i >= 0, "Input [" + i + "] must be >= 0");
    yields 
    CC1065 	 User message to contract call can only be string literal, or a static field, or static property that is at least internally visible.

     

    Well, I can hard-code int.MinValue (which Pex tries first) into the string literal, but then, the nearest I can produce is

    Your puzzle method unexpectedly violated the following Contract -> Precondition failed: i >= 0 Input [-2147483648] must be >= 0 

    but that still contains " -> Precondition failed: i >= 0 ", which is obviously not in

    Your puzzle method should have violated the following Contract: Input [-2147483648] must be >= 0
     

    Seems I have to learn more about Contracts and/or Microsoft.Pex.Framework.PexAssert which is somehow related - or not?

     

    I got one more strange thing where Pex seems to crash, but have found it only with F#. So, maybe better make a new thread out of it.

    __

    meisl

    p.s.: re non-determinism: you might want to check out this solvable duel about random number generation ;)

     

    Monday, November 08, 2010 7:31 PM
  • Yes, that's precisely the problem I'm having with TheVoiceIHearInMyHead.  I don't know how to generate the right type of contract violation for Pex to consider it a match (let alone with the right message string).

    I've already solved that random number generation duel :-) Apart from the two that appear impossible and two for which I can't get contract violations in the right form, I have three others remaining to solve in the C# list - one of which I've left because it seems like too much work right now ;-)

     

    Monday, November 08, 2010 11:16 PM
  • I've already solved that random number generation duel :-)

    Oh, great :) So I see it's time to put on another PRNG, maybe with a little less of hint this time? Watch out.

    Apart from that, which are the ones that you dropped (only for now, I'm pretty sure ;)? You know, there was a discussion about what makes good, interesting, non-frustrating duels; have to search, will provide link later. It's "PexForFun: REALLY great for teaching | learning!" and ongoing in "PexForFun: Nothing easier than boolean operators... really?!".

    __

    meisl

    Tuesday, November 09, 2010 7:26 PM
  • Seems I have to learn more about Contracts and/or Microsoft.Pex.Framework.PexAssert which is somehow related - or not?

    So, what I'm gonna read now is the user documentation from http://research.microsoft.com/en-us/projects/contracts/.

    __

    meisl

    Tuesday, November 09, 2010 10:12 PM
  • I've skipped the TDD Kata challenge. 

     

    Weirdly, ChallengeSticky which appeared recently gives a NullReferenceException when Pex passes in 0, despite having no object instances in sight.  The secret implementation returns 0 - no exception.  Maybe a Pex/PexForFun bug?

    Tuesday, November 09, 2010 10:51 PM
  • I looked at that - or very similar documentation - briefly a day or two ago and didn't see anything obvious that would explain the observed behaviour.  Page 31 suggests that all contracts are rewritten to use one of the basic Contract methods, and you can try most of them in PexForFun very quickly (and still not replicate the secret implementation).  I also tried "legacy requires" without success.  I haven't read the whole thing, and probably haven't tried all the possibilities.  Let us know if you have any better results!
    Tuesday, November 09, 2010 10:55 PM
  • Hey Mazz, little aside:

    re that little competition of ours which is obviously going on for a while on PexForFun - theoretically, as I have published some duels and you haven't - shouldn't you be ~20 pts ahead of me? ;)

    So, how about making some yourself? Could imagine they'd be interesting, seriously :)

    __

    meisl

    Tuesday, November 09, 2010 11:06 PM
  • I only started a few days ago ;-)

     

    I've been thinking about whether to publish some challenges.  The trick might be to pitch them to the right level.  You can make it very difficult very quickly, especially as Pex chooses the inputs it will evaluate, but it's more interesting for others when they have a real shot at solving them.

    Wednesday, November 10, 2010 6:43 AM
  • The trick might be to pitch them to the right level.


    Absolutely! And what I'm after is to find out how to get closer to that. I think it's pretty straight-forward: let us try several approaches and discuss 'em here. So, let me encourage you again: just give it try! I'm dead-sure that even your first will be among, say, at least the top 30% interesting ones.

    __

    meisl

    p.s.: just tried to solve my #108 ;), Division - and again failing coz of this annoying Contracts problem: "Your puzzle method should have violated the following Contract: Unable to divide" - but how?! At all YOU CONTRACTS-GURUS: PLEASE, HOW IS THAT PRODUCED?? We do know the when, just not the how! (ref Mazz's 1st post above from Mo, Nov 8th)

    p.p.s.: solved another one instead...

    Wednesday, November 10, 2010 7:40 PM
  • I wondered whether the "Your puzzle method should have violated the following Contract: Unable to divide " syndrome was due to the secret implementation using Contract.EnsuresOnThrow<T>(...), and then throwing T at some point.  Doing that doesn't work - Pex reports "Your puzzle method raised an exception unexpectedly -> <exception text>".  But trying variations that probably should not work cracked it (or at least one way to make Pex happy, for at least three of the duels). 

    Instead of using Contract.Requires() for your preconditions throw a plain Exception() instead - and it doesn't matter whether your Exception text matches the Contract that Pex indicates you should have violated either.

    I'm not convinced this replicates the secret implementation's logic (which I suspect that happens in other cases too), but I doubt I can figure that out myself.  I also wonder whether Pex does this by design or by accident? 

     

     

    Friday, November 12, 2010 1:19 PM
  • Interestingly, throwing a plain Exception doesn't work for ChallengeStringCalculator and the problem of generating the unspecified kind of Contract violation to keep Pex happy remains.  34 people have solved it, so it must be (or at one time have been) possible.
    Friday, November 12, 2010 2:45 PM
  • Reminds me of the old way (called legacy somewhere in the document mentioned above) of establishing preconditions:

    int Foo(int arg) {
     if (arg == 0) throw ArgumentException("...");
     //...
    }
    

    That is: as the first statements there are several checks and exceptions thrown when not met.

    I remember they had thought about that, maybe there is some re-writing performed?

    Hmm, but I don't see why for the duels in question it must be the most unspecific Exception type (it does, as Mazz found out). Also, I'm not sure either whether I like this behavior of Pex...

    __

    meisl

    Friday, November 12, 2010 7:47 PM
  • Section 5.1 Argument Validation and Contracts (page 18 ff) clarifies a bit:

    With contracts there are now 3 forms of argument validation, and it's about dealing/integrating with existing, non-contracts enabled code:

    1. so-called "legacy if-then-throw" or "legacy-requires", for which I gave an example above. One may add a Contract.EndContractBlock(); marker after those old-school preconditions in order to enable some contracts tool support. No inheritance of contracts and checking at runtime is *always* performed.
    2. Contract.Requires<SomeSortOfException>(condition,...): throws SomeSortOfException if condition is not met, so this is like a shorter way of writing 1. with automatic tools support as I understand. However, not sure whether I have fully understood Section 5.1.2 "Difference between Requires<Exn> and if-then-throw"
    3. Contract.Requires(condition,...) (without type parameter!): the "future", if you will; the recommended and most straight-forward thing to do as I understand. You can decide whether to build with or without runtime checking which is like if you had put a #IF DEBUG ... #ENDIF around each and every if-then-throw in your old code. Additionally, inheritance of contracts is switched on/off likewise.

    It seems that each of the three are recognized by Pex and also give slightly different error messages. Then, contrary to what I thought before

    >  it must be the most unspecific Exception type

    there is a counter-example on PexForFun: MaxContigSum. It takes a parameter called rgi of type int[] which is expected to be non-null. I found that both,

      Contract.Requires<NullReferenceException>(rgi != null);
    

     (with or without Contract.EndContractsBlock();) and

      if (rgi == null) throw new NullReferenceException();
    

    do the job. Note that neither one works with just Exception.

    __

    meisl

    Saturday, November 13, 2010 5:35 PM
  • Interesting, and a bit tricky.  Pex4fun doesn't tell you what type of exception the secret implementation threw but you have to divine it?  I guess the Error Message field may give you a clue...
    Saturday, November 13, 2010 8:05 PM
  • > Pex4fun doesn't tell you what type of exception the secret implementation threw

    This looks like something we could fix.

     


    Jonathan "Peli" de Halleux - Try Pex online at www.pexforfun.com!
    Saturday, November 13, 2010 10:13 PM
    Owner
  • > This looks like something we could fix.

    That would be helpful :-)  As an experiment I just tried the 20 or so most likely Exception types I could think of for ChallengeStringCalculator and none of them seem to match.

    Monday, November 15, 2010 11:09 AM
  • Re the original problem of this thread, "true (0x80) 'mismatching' true (0x80)", I just mined out this older thread: Error in PexAssert

    Not sure (anymore) if I fully understand the problem... Maybe I'll read again the other day :)

    __

    meisl

     

    Monday, November 15, 2010 8:30 PM
  • Two fixes were applied to the website today:

    • Pex for fun should show which exception type should be thrown, if the secret implementation throws an exception, and
    • When comparing Boolean results in a Coding Duel, the strange observed behavior should be gone.

    Nikolai Tillmann
    Tuesday, November 16, 2010 3:52 PM
    Owner
  • Thanks a lot! Eliminates, IMHO, a great deal of frustration potential for ppl on PexForFun :D

    __

    meisl

    Tuesday, November 16, 2010 8:21 PM
  • Hey Nikolai,

    Thanks for the updates to the game. It's been a fun time killer for those of us at the office. Since we're all pretty competitive, can you explain to everyone how we get "points" in addition to the one point per puzzle solved?

    Thanks again,

    -Mike

    Wednesday, November 24, 2010 5:37 AM
  • The best way to get points is to create duels and publish them. You then get points when other users try to solve your duels.

        http://www.pexforfun.com/Page.aspx#e6925b01-bef8-4bb2-9516-51adf12b2c77

    You can also create more advanced content like pages and course which will also give you more points.


    Jonathan "Peli" de Halleux - Try Pex online at www.pexforfun.com!
    Friday, November 26, 2010 5:22 AM
    Owner
  • > you explain to everyone how we get "points" in addition to the one point per puzzle solved?

    The point system is documented here:
    http://www.pexforfun.com/Documentation.aspx#Points

    There might be more ways to earn points in the future.


    Nikolai Tillmann
    Monday, November 29, 2010 3:28 AM
    Owner
  • Hi Mike,

    sure you don't wanna miss any new duel coming up so you make the point before your colleague does, right?

    Well, then you might want to watch out for posts that I do here, as I am usually advertising newly created duels in them; e.g. "PexForFun: Why isn't there System.Numerics?"

    Hey, and don't ya tell anybody ;-)

    __

    meisl

    Tuesday, December 07, 2010 1:55 PM
  • Hey Meisl,

    I see you've been busy since I last signed on. I've been busy too, but not in the Pex for Fun sort of way :). So heads up: I'm coming after you. I was bored and read a book on F# while I was taking the dog for a quick walk so I can add those to my wins now. I'm also going to put a bunch of new puzzles in for the community, and I hope you and some of the kids at MSR will join me. Frankly this is my favorite game. I used to love the first person shooters and the satisfaction of blowing away a whole team of Noobies playing Rainbow Six, but this is far more fun.

    So there it is. Throwing down the gauntlet and looking forward to the rivalry.

    By the way, my email address is mlopat@lunadevelopment.com.... feel free to brag when you solve one of my puzzles so the boys and I here can make the next one harder on ya ;)

     

    -Mike

    Sunday, December 12, 2010 4:02 AM
  • Hey Mike,

    that's great :D, a pleasure to pick it up! Hehe, and don't forget the other guy, Mazz, he's still ahead of you at the moment. As I said to him somewhere above: "Given that you have created n duels and I have created k - shouldn't you be k-n points ahead of me?"... ;) [talking of points for coding duels won I mean]

    This is going to be even better once we're entering a competition on the best puzzles. There's still some stuff missing for that to really work but as we're discussing here and good ideas are coming up we're definitely moving there, making the "game" even more addictive ;)

    Oh, and btw, of course I have solved both your puzzles :) There's a problem with the one about primes, will comment about it in the thread about other ppl's solutions (fits there better I think)

    Cheers,


    meisl

    Sunday, December 12, 2010 1:21 PM
  • Old thread, I know, but seems relevant. I'm trying to tackle a few Pex4Fun puzzles that are eluding me right now and I wonder if folks have any hints?

    RedrumRedrum

    AltSeries1

    ArrayMixer

    I probably missing the obvious but if anybody has any gentle hints - not solutions - then that would be appreciated.

    I also tackled AnySecondNow and eventually gave up since it relied too much on luck. Has anybody successfully solved that one?

     

    Thursday, April 21, 2011 7:30 PM