K-user mailing list

[David Lazar <lazar6 AT illinois.edu>]

Hi Robby,

K2 has some Perl scripts to assist with testing (and producing JUnit
reports that Jenkins can read). It probably wouldn't be hard to port
these scripts to K3.

I've been writing my own testing framework, but it is geared toward
languages with an existing implementation. testcc takes a list of
interpreters as command-line arguments and a program, and then
compares how each interpreter behaves on the input program.

Here are some examples of testcc in action:

Note: 'runkcc' runs the input program through the K definition of C;
'rungcc' and the others compile the input program with the respective
compiler and execute the resulting a.out.

$ testcc rungcc runclang "runclang -O3" runkcc -i hello.c
1 equivalance class
{rungcc, runclang, runclang -O3, runkcc}

hello.c is the Hello World program, so kcc, gcc, and clang should
behave the same way. Now let's try an undefined program (the resulting
program can do anything!).

$ testcc rungcc runclang "runclang -O3" runkcc -i writes.c
3 equivalence classes
{runclang, runclang -O3}
{rungcc}
{runkcc}

Now a non-deterministic program:

$ testcc rungcc runclang "runclang -O3" runkcc -i nondet.c
2 equivalence classes
{runkcc}
{rungcc, runclang, runclang -O3}

gcc and clang pick left-to-right evaluation order, so they miss a
behavior that kcc catches. If we run the exact same command with the
-r flag, we get a full report of what happened:

$ testcc rungcc runclang "runclang -O3" runkcc -i nondet.c -r
- runner: rungcc
  return: 2
  stdout: ""
  stderr: ""
  time: 0.064

- runner: runclang
  return: 2
  stdout: ""
  stderr: ""
  time: 0.066

- runner: runclang -O3
  return: 2
  stdout: ""
  stderr: ""
  time: 0.069

- runner: runkcc
  return: 1
  stdout: ""
  stderr: ""
  time: 7.822

The output is valid YAML, so you can easily parse it and do your own
comparisons in your favorite programming language.

testcc is also a Haskell library, so you can easily write a custom
tester. In particular, you can combine the testcc library with
junit-reports (another Haskell library I wrote) to get JUnit XML which
can be read into Jenkins. This is how I am testing my K definition of
OCaml.

I haven't yet made testcc public (I just finished writing it
yesterday). If you would find it useful, I can push myself to publish
the code in the next day or two. You would have to be comfortable with
installing Haskell software (via cabal-install) to use it.

Otherwise, I can show you to work with the K2 Perl scripts.

Cheers,
David

On Mon, Oct 1, 2012 at 1:48 PM, Robby Findler
<robby AT eecs.northwestern.edu>
 wrote:
> Hi all:
>
>   What's the recommended way to build up a test suite of programs for
> a K model? I can use k-run, and some scripting with a bunch of files
> in a directory, but I'm wondering if there is some more convenient
> setup?
>
> Thanks,
> Robby
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user