Could the built-in test runner be used to write unit tests for user programs? about bosquelanguage

[mrkmarron]

Hi @catchmareck sorry for the delayed response.

Are you thinking of a way to (1) more selectively run Bosque language unit tests or is the idea to try to (2) make the test_runner a more general purpose test runner?

If it is the first case then I think making the .json file a parameter would work well. In the second case I think there may be a number of assumptions baked into the runner that may not be great and we might want to think a bit more.

[catchmareck]

I was thinking about the 2nd option, which is to make the test runner more general purpose so that users could write their own tests for their programs and run them.

In that case, is it possible to refactor the test_runner to make it work that way or it's required to write a new one from scratch?

[mrkmarron]

I have been thinking about this a bit and, for Bosque users, I would like to write a new one from scratch.

One of the "super powers" that Bosque is built to have is support for more than just easy unit testing. If you look at the current road_to_1_0 branch you will see that is has a command line utility that generates logical models for a program and can solve them to find an input that will trigger a target error (as long as the entry function uses API Types). Using API Types we should also make it very easy to hook up a coverage based buzzer like AFL++. I would love to have the Bosque tester be able to apply the combination of all three approaches -- developer provided unit tests, fuzzer coverage, and symbolic model generation -- integrated into a single easy to use framework.

I think that for this it makes sense to spend a little time thinking about how it would look and work from a fresh perspective.

[catchmareck]

@mrkmarron Yeah, I was playing with the Symtest tool a bit now and I can tell this kind of testing has a huge potential (although the tool is still a bit buggy).

Regarding the road_to_1_0 branch and the Pinon utility. I had a quick look at a git diff and noticed that the mentioned Symtest tool is completely deleted as well as the ExeGen tool. Why is that? Is Pinon supposed to replace Symtest? What about ExeGen? We can't compile Bosque programs without it I guess, right? Could you please shed some light on this?

[mrkmarron]

The SymTest tool made a nice PoC but it was based on a classic symbolic model checking iterative unrolling algorithm. This meant it was only suitable for "small models". The Pinon utility encodes a novel set of encodings to use decision procedures in Z3 in many of the cases that previously needed unrolling (so we can find errors that aren't "small"). Currently drafting a paper on this.

The compile times for clang were a bit rough so I am temporarily dropping the exegen but will replace it with a C based interpreter to make quick development (and a REPL) feasible + a simple compiler for Morphir. I am going to start work on these this week while continuing to fix bugs on the Pinon analyzer.

[catchmareck]

Well, sounds like quite a lot of work to do yet, no? ;)

Are you able to tell how long will it take to merge road_to_1_0 into master? I don't mean an exact date because that is proly impossible to tell, but can you at least tell if it will take weeks or months from now?

Sorry for asking so many questions but I'm writing about Bosque and am about to publish my work (as mentioned in my email to you) but if you plan to release these changes in a week or two then I'll wait for that because I don't want it to be outdated right after publishing ;)

[mrkmarron]

Hi @catchmareck, I am sure it will be 2-3 months as it is a fair bit of work and I am sure a couple of unexpected things will pop up.

It is great to hear that you have some things you want to publish. I'll keep an eye out for them!