K-user mailing list

[Philip Daian <philip.daian AT runtimeverification.com>]

Hi Ali and all,

I support this effort entirely and will do whatever I can from the RV-Monitor side.

The MOP file parsers you're referring to in RV-Monitor, as well as a lot of their associated code make the codebase needlessly complex (far beyond what it should be) and difficult to work with, so I think a completely independent and well specified JavaMOP is in the interest of all projects.  Also, I think that such a project in K can be written with many language independent components, with a framework that can then be reused for CMOP and MOP for many other languages.

Eventually I also believe that RV-Monitor's parser, and even in the more distant future RV-Monitor itself (which is a compiler from logics to monitoring libraries), can be rewritten as such.

Thanks,
Philip Daian
RV Inc

On 06/19/2015 07:34 AM, Kheradmand, Ali wrote:

Hi,

We've decide to implement JavaMOP's parser using K and I need a link to get more information on how to use K's API for parsing in  java.  

I've included information about the JavaMOP project and it's implementation below: 

Description of the JavaMOP project:

JavaMOP is a framework that allows one to specify (using FSM, ERE, LTL, …) formal properties for Java programs, and then automatically synthesizes monitors that efficiently monitor the runtime of the programs for validation or violation of those properties and call (if exist) user defined handlers in response. 

The user specifies the properties and handlers in a file with .mop extension using JavaMOP's syntax. Basically an MOP specification describes the (interesting) events using slightly extended syntax of AspectJ Advice and then describes the properties over the declared event using a syntax specific to the desired logic (for example FSM) and finally describes the handlers for validation or violation of the properties in Java. 

JavaMOP in fact uses RV-Monitor for synthesis of the runtime monitors. In RV-Monitor, one describes the desired properties in an RVM specification (a file with .rvm extension). RV-Monitor generates the monitoring libraries for an input RVM specification. These libraries provide interface functions (corresponding to the events in the specification) that need to be manually called from within the target program in the sense that the programmer should manually instrument the code at places corresponding to the declared events. JavaMOP on the other hand automates the instrumentation process by using AspectJ to describe the events. 

In it's most basic form, JavaMOP's compiler inputs an MOP specification (.mop file) and outputs two files: one is an AspectJ (.aj) file which contains the Advices and handlers and the other one is an RVM specification (.rvm) which contains the specification of the properties. One can feed the generated .rvm file to RV-Monitor to obtain the monitoring libraries and then feed the libraries, the .aj file, and the target program to the AspectJ compiler to produce the instrumented program. 

Implementation of JavaMOP:

JavaMOP is implemented purely in java. It uses JavaCC to parse javamop and to get the ASTs and then works with the ASTs to produce aspectj and rvm. Unfortunately it's a bit messy. Also JavaMOP and RV-Monitor used to be a single project, then they diverged but they are not completely separated and a lot of messy things are happening in the parsing part. For example right now JavaMOP sends MOP files to RV-Monitor for parsing and then further parses what is returned.

Grigore's idea is to implement a clean parser for JavaMOP using K's parser and then work with KAST. These are the steps that he mentioned that needs to be done for now:

1) You should define the syntax of JavaMOP as a K syntax module, at the same degree of detail as the current parser of JavaMOP.  Let's not innovate much for now, let's just rationally reconstruct what we already had, but using K.

2) You will then reuse as much of the current implementation of JavaMOP as possible, basically only changing the parsing/AST part/interface.  To do that, you would import the K API, say k.jar, and from there call the methods that generate a parser from a module, and then the methods that parse a string given a generated parser, and finally put the JavaMOP definition into a KAST.  Then modify the JavaMOP implementation to work directly with the KAST instead of the current AST.

 

Now for the start I need to get some information on how to use K for parsing and more information on what is KAST and how can I work with that. 

Regards,

Ali

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user