K-user mailing list

[James Koppel <jkoppel AT mit.edu>]

Thank you. I have successfully compiled the semantics and run them on a test program.

This is the fifth and final language for which I need test suites. It will be nice to finally put this part of the project to rest.

On Fri, Oct 14, 2016 at 7:16 PM, Park, Daejun <dpark69 AT illinois.edu> wrote:

Thanks for all of the information! I'll look into it more.

Regarding that error, I guess you're using Mac OS, since the error message seems to come from OSX sed. Indeed, *GNU sed* is needed for the following line:

test "`sed -n '/<k>/,/<\/k>/{ p }' stdlib.out | tr -d ' \n'`" = "<k>@Normal</k>"

You can change the name `sed` with the name of gnu-sed that you have, (e.g., `gsed` in most case), or you can try it in a Linux box (indeed, it's been tested in Ubuntu 12.04 and 14.04).

Best,

Daejun

On Oct 14, 2016, at 2:57 PM, James Koppel <jkoppel AT mit.edu> wrote:

Thank you for your effort to help me. I checked out and built 1fb7d3b044f54577d8439e7560dcd4c8766f51de, and, unfortunately, it's still not working. Current build error when I try to run "make":

Hard-wiring standard built-in objects...

krun stdlib.js >stdlib.out 2>&1

test "`sed -n '/<k>/,/<\/k>/{ p }' stdlib.out | tr -d ' \n'`" = "<k>@Normal</k>"

sed: 1: "/<k>/,/<\/k>/{ p }": extra characters at the end of p command

make: *** [build] Error 1

 

BTW, could you tell me a bit more about the issues for using JSC test? It's a bit counter-intuitive to me that there is an issue for simply running JS engines against tests.

Simply running the engines is fine. Actually getting to the tests directly, outputting modified versions, and preferably running it as a single test....not so fine. Requires some digging through their test infrastructure, which, in the case of JSC, is a tangle of Perl and Ruby with way to much dynamism.

Me: How is the expected output specified?

JSC developer: It depends on the test suite. It's pretty hacky since we get tests from all over the place.

It turned out not to be promising.

 

Indeed, you can go further using KJS. You can even verify that two programs (before and after your transformations) are equivalent (for all possible inputs), instead of just comparing the specific final outputs of the two programs. Recently, I developed such an equivalence checker that will be available for KJS once we finish porting it into K 4.0. Please let me know if you're interested in this as well.

 I am very interested. Thanks.

One of my transformations is to install test-coverage instrumentation, and thus is only semantics-preserving modulo this additional output. Will the equivalence checker be able to handle this?

Regarding the symbol table generator, could you please elaborate it a bit more? 

*symbol table generator generator

I've attached slides for a talk I gave on my initial progress. This was given as an internal lunch talk when I was an intern at Semantic Designs, and makes heavy reference to their internal DSLs for language construction, but it should still be understandable. My work shifted shortly after this talk to more of an abstract-interpretation approach.

On Thu, Oct 13, 2016 at 4:59 PM, Park, Daejun <dpark69 AT illinois.edu> wrote:

Hi James,

Could you please checkout the kjs branch again? A wrong version was pushed, and now it is fixed. The kjs branch should refer to the commit 1fb7d3b044f54577d8439e7560dcd4c8766f51de. I double-checked if it works as described in the readme. Sorry for the inconvenience.

Using KJS to test the program transformation (against the test262) seems interesting. You can test your transformations against other test suites (if any) as well, since KJS provides a trustable reference model. One of my concern would be performance --- KJS is much slower than production JS engines. BTW, could you tell me a bit more about the issues for using JSC test? It's a bit counter-intuitive to me that there is an issue for simply running JS engines against tests.

Indeed, you can go further using KJS. You can even verify that two programs (before and after your transformations) are equivalent (for all possible inputs), instead of just comparing the specific final outputs of the two programs. Recently, I developed such an equivalence checker that will be available for KJS once we finish porting it into K 4.0. Please let me know if you're interested in this as well.

Regarding the symbol table generator, could you please elaborate it a bit more? 

Thanks,

Daejun

On Oct 12, 2016, at 8:41 PM, James Koppel <jkoppel AT mit.edu> wrote:

Thank you! With the checkout of kjs, I was able to build the semantics. However, krun gives an error when I try to use it:

[Error] Critical: Unknown option: --pattern-matching

My immediate interest in KJS is a bit trite: it looks like the easiest way to run the test262 suite, which I plan to use to test some semantics-preserving program transformations I've built. (I say this after many hours tearing my hair out with the JSC tests, even with some help from a JSC developer.) I also have a project attempting to automatically derive a symbol table generator, using a rewrite semantics a la K as input; this is currently on hold.

On Wed, Oct 12, 2016 at 12:15 AM, Park, Daejun <dpark69 AT illinois.edu> wrote:

Hi James,

Thanks for your interest in KJS.

The `kjs` branch was deleted by mistake. I just put it back and now it's available in the K repository.
        https://github.com/kframework/k/tree/kjs

There is also a VM that contains everything to reproduce all the result in the paper:
        https://github.com/kframework/_javascript_-semantics/blob/master/PLDI15-AEC.README.md


Please note that the version of K is outdated, and currently we're working on porting the semantics to the latest K 4.0, so that we can enjoy all the benefits of K 4.0.

BTW, could you please share your specific interest in KJS? I'll be more than happy to help you to use (or extend) KJS for your specific needs.

Best,
Daejun

On Oct 11, 2016, at 6:52 PM, James Koppel <jkoppel AT mit.edu> wrote:

> Hello!
>
> I've been unable to build the _javascript_ semantics. I've tried building with both K 4.0 and K 3.6, and gotten errors on both.
>
> The KJS README says it needs a modified version of K, accessible by checking out the "kjs" branch of the K repository. However, there is no such branch. I'd appreciate help in this matter.
>
> Sincerely,
> James Koppel
> MIT CSAIL

<talk.ppt>