K-user mailing list

["Park, Daejun" <dpark69 AT illinois.edu>]

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