Problem with enforce

[kheradmand]

I have a very simple mop file that enforces a thread schedule:

package mop;

enforce myEnforce() {
    event one before():
        execution(* *run(..)) && threadName("Thread-1") {
            System.out.println("one");
        }
    event two before():
        execution(* *run(..)) && threadName("Thread-2") {
            System.out.println("two");
        }
    ere : one two

    @fail {
        System.out.println("failed");
    }


}

when I try to generate agent for this file I get the following error:

javamop -agent enforce.mop
-Processing 1 specification(s)
 enforce.rvm is generated
 enforceMonitorAspect.aj is generated
-Processing 1 specification(s)
 enforceRuntimeMonitor.java is generated
(ajc) Failed to produce aop-ajc.xml

Also when I try to use ajc to instrument my code, I get the following:

/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:37 [error] cloned_monitor_condition_satisfied cannot be resolved to a variable
cloned_monitor_condition_satisfied = clonedMonitor.Prop_1_event_one();
^^^^^^^^^^^^^^^^^^^^^^^^^^^
/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:38 [error] cloned_monitor_condition_satisfied cannot be resolved to a variable
if (!cloned_monitor_condition_satisfied) {
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^
/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:76 [error] cloned_monitor_condition_satisfied cannot be resolved to a variable
cloned_monitor_condition_satisfied = clonedMonitor.Prop_1_event_two();
^^^^^^^^^^^^^^^^^^^^^^^^^^^
/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:77 [error] cloned_monitor_condition_satisfied cannot be resolved to a variable
if (!cloned_monitor_condition_satisfied) {
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^
/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:292 [error] cloned_monitor_condition_satisfied cannot be resolved to a variable
cloned_monitor_condition_satisfied = clonedMonitor.Prop_1_event_one();
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:293 [error] cloned_monitor_condition_satisfied cannot be resolved to a variable
if (!cloned_monitor_condition_satisfied) {
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:338 [error] cloned_monitor_condition_satisfied cannot be resolved to a variable
cloned_monitor_condition_satisfied = clonedMonitor.Prop_1_event_two();
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:339 [error] cloned_monitor_condition_satisfied cannot be resolved to a variable
if (!cloned_monitor_condition_satisfied) {
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:400 [error] myEnforceRuntimeMonitor cannot be resolved
myEnforceRuntimeMonitor.startDeadlockDetection();
^^^^^^^^^^^^^^^^^^^^
/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:406 [error] myEnforce_ThreadMonitor_ThreadSet cannot be resolved
myEnforce_ThreadMonitor_ThreadSet.add(t);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

10 errors

[kheradmand]

I have almost the same problem when I use solely rv-monitor and instrument my program manually:

enforceRuntimeMonitor.java:36: error: cannot find symbol
                        cloned_monitor_condition_satisfied = clonedMonitor.Prop_1_event_one();
                        ^
  symbol:   variable cloned_monitor_condition_satisfied
  location: class myEnforceEnforcementMonitor_Set
enforceRuntimeMonitor.java:37: error: cannot find symbol
                        if (!cloned_monitor_condition_satisfied) {
                             ^
  symbol:   variable cloned_monitor_condition_satisfied
  location: class myEnforceEnforcementMonitor_Set
enforceRuntimeMonitor.java:75: error: cannot find symbol
                        cloned_monitor_condition_satisfied = clonedMonitor.Prop_1_event_two();
                        ^
  symbol:   variable cloned_monitor_condition_satisfied
  location: class myEnforceEnforcementMonitor_Set
enforceRuntimeMonitor.java:76: error: cannot find symbol
                        if (!cloned_monitor_condition_satisfied) {
                             ^
  symbol:   variable cloned_monitor_condition_satisfied
  location: class myEnforceEnforcementMonitor_Set
enforceRuntimeMonitor.java:291: error: cannot find symbol
                cloned_monitor_condition_satisfied = clonedMonitor.Prop_1_event_one();
                ^
  symbol:   variable cloned_monitor_condition_satisfied
  location: class enforceRuntimeMonitor
enforceRuntimeMonitor.java:292: error: cannot find symbol
                if (!cloned_monitor_condition_satisfied) {
                     ^
  symbol:   variable cloned_monitor_condition_satisfied
  location: class enforceRuntimeMonitor
enforceRuntimeMonitor.java:337: error: cannot find symbol
                cloned_monitor_condition_satisfied = clonedMonitor.Prop_1_event_two();
                ^
  symbol:   variable cloned_monitor_condition_satisfied
  location: class enforceRuntimeMonitor
enforceRuntimeMonitor.java:338: error: cannot find symbol
                if (!cloned_monitor_condition_satisfied) {
                     ^
  symbol:   variable cloned_monitor_condition_satisfied
  location: class enforceRuntimeMonitor

@seriousamlqz I don't know whether I'm doing something wrong or it is rv-monitor's bug.

[kheradmand]

runtimeverification/rv-monitor#100 has been resolved but still both agent generation and static weaving fail in javamop.

[seriousamlqz]

@kheradmand What's the problem right now? Same error？ Again it seems it has nothing to do with javamop

[pdaian]

We just recently merged the fix for this, perhaps JavaMOP requires a release then dependency version update to solve this? Should be OK in latest master.

[seriousamlqz]

OK @kheradmand can try and confirm, thanks Philip!

[pdaian]

@seriousamlqz no problem. I see JavaMOP depends on latest release. Is it OK to wait until 1.4 release for this fix (should be later this week after the Java refactor is reviewed) or should I release an interim 1.4 (aka - how time sensitive is this fix)? Users can have this fixed by just using the latest development version of RV-Monitor (from the "all versions" page).

[seriousamlqz]

I think it is fine for us to wait, we are not facing any deadline at this
moment.

On Tue, Jan 20, 2015 at 4:19 PM, Philip Daian notifications@github.com
wrote:

@seriousamlqz https://github.com/seriousamlqz no problem. I see JavaMOP
depends on latest release. Is it OK to wait until 1.4 release for this
fix (should be later this week after the Java refactor is reviewed) or
should I release an interim 1.4 (aka - how time sensitive is this fix)?
Users can have this fixed by just using the latest development version of
RV-Monitor (from the "all versions" page).

—
Reply to this email directly or view it on GitHub
#188 (comment)
.

Qingzhou Luo
http://mir.cs.illinois.edu/~qluo2/

Department of Computer Science
University of Illinois, Urbana Champaign

[kheradmand]

@pdaian @seriousamlqz So I am using javamop's released binary (the one on fsl's website) and latest (fixed) version of rv-monitor. This should work, yes?
I have same mop file:

package mop;

enforce myEnforce() {
    event one before():
        execution(* *run(..)) && threadName("Thread-1") {
            System.out.println("one");
        }
    event two before():
        execution(* *run(..)) && threadName("Thread-2") {
            System.out.println("two");
        }
    ere : one two

    @fail {
        System.out.println("failed");
    }


}

A simple java file:

class SimpleRunnable implements Runnable{
    static int shared = 0;
    public void run(){
        System.out.println("Thread " + Thread.currentThread().getName());
        shared = shared + 1;
    }
}

public class Main{
    public static void main(String args[]){
        Thread t1 = new Thread (new SimpleRunnable());
        Thread t2 = new Thread (new SimpleRunnable());
        t1.start();
        t2.start();
    }

}

When I run javamop -agent enforce.mop, I get:

-Processing 1 specification(s)
 enforce.rvm is generated
 enforceMonitorAspect.aj is generated
-Processing 1 specification(s)
 enforceRuntimeMonitor.java is generated
(ajc) Failed to produce aop-ajc.xml

and If I run javamop enforce.mop and then ajc -1.6 -d kk enforceMonitorAspect.aj Main.java, I get:

/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:1 [error] The type java.lang.CharSequence cannot be resolved. It is indirectly referenced from required .class files
(no source information available)
/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:400 [error] myEnforceRuntimeMonitor cannot be resolved
myEnforceRuntimeMonitor.startDeadlockDetection();
^^^^^^^^^^^^^^^^^^^^
/Users/Ali/FSL/replay/example/enforceMonitorAspect.aj:406 [error] myEnforce_ThreadMonitor_ThreadSet cannot be resolved
myEnforce_ThreadMonitor_ThreadSet.add(t);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

3 errors

[seriousamlqz]

@kheradmand Can you try to simplify that .mop file with only .rvm file (or use -keepRVFiles), and then try to compile the generated RuntimeMonitor.java file? That way we can locate if the problem is in RVMonitor or Javamop.

[kheradmand]

@seriousamlqz Yeah I already did that and it compiles successfully. I have some problems on whether it works correctly or not (refer to runtimeverification/rv-monitor#144 for more info); but it at least compiles successfully.

[seriousamlqz]

The .mop is named as enforce.mop, but the property is named as myEnforce? What if you rename the .mop file to myEnforce.mop?

[kheradmand]

Good point. I tried myEnforce.mop
agent generation still fails, one of 2 errors using ajc disappeared but still got some problem:

/home/ali/Desktop/replay/myEnforceMonitorAspect.aj:406 [error] myEnforce_ThreadMonitor_ThreadSet cannot be resolved
myEnforce_ThreadMonitor_ThreadSet.add(t);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

1 error