Java Pathfinder and ANTLR 4

[Louise Dennis]

I use JPF to verify programs which need to read in and parse files.

I'm in the process of trying to update my parser to use Antlr 4 grammars.

My project is called mcapl and I've added antlr-4.7-complete.jar to both
mcapl.classpath and mcapl.native_classpath in jpf.properties.

My programs run without throwing errors when I'm not verifying them so I
believe the parsers and lexers are working correctly - or at least
should not be throwing the errors I'm seeing.

I'm trying to run the following example (which works using my previous
parser - governor.ail is the file to be parsed):

--

@using = mcapl

target = ail.util.AJPF_w_AIL
target.args =
${mcapl}/src/examples/ethical_governor/human_hole/governor.ail,${mcapl}/src/examples/ethical_governor/human_hole/human_hole.psl,3

log.info =
ail.mas.DefaultEnvironment,ajpf.product.Product,ethical_governor.human_hole.HumanHoleGoalEnv

listener+=,.listener.ExecTracker
et.show_shared=false
et.print_insn=false

# this is a preemption boundary specifying the max number of
instructions after which we
# break the current transition if there are other runnable threads
vm.max_transition_length = MAX
___

When I run this using gov.nasa.jpf.tool.RunJPF I get the following error

[SEVERE] JPF exception, terminating: exception in native method
java.lang.Class.forName
java.lang.NoClassDefFoundError: org/antlr/v4/runtime/TokenSource
at java.lang.Class.getDeclaredMethods0(Native Method)
at java.lang.Class.privateGetDeclaredMethods(Class.java:2693)
at java.lang.Class.getDeclaredMethod(Class.java:2120)
at gov.nasa.jpf.vm.NativePeer.initializePeerClass(NativePeer.java:243)

(which suggests a classpath error to me).


I'm currently using a native peer for efficiency when parsing. I tried
removing the native peer in which case I get the error:

# choice: gov.nasa.jpf.vm.choice.ThreadChoiceFromSet
{id:"ROOT" ,1/1,isCascaded:false}
# exception: java.lang.NoSuchMethodException@195c in
MethodInfo[java.nio.CharBuffer.<init>(IIII[CI)V]
java.lang.NoSuchMethodException: Calling java.nio.Buffer.<init>(IIII)V
at java.nio.CharBuffer.<init>(CharBuffer.java:281)
at java.nio.HeapCharBuffer.<init>(HeapCharBuffer.java:57)
at java.nio.CharBuffer.allocate(CharBuffer.java:335)
at org.antlr.v4.runtime.CharStreams.fromString(CharStreams.java:225)
at org.antlr.v4.runtime.CharStreams.fromString(CharStreams.java:212)
at
actiononly.ActionOnlyAgentBuilder.parsefile(ActionOnlyAgentBuilder.java:81)
at
actiononly.ActionOnlyAgentBuilder.getAgent(ActionOnlyAgentBuilder.java:54)

To complicate matters if I call the same example from a Junit test:

@Test
//----------------------------------------------------------------------
public void equation6 () {
if (verifyNoPropertyViolation(JPF_ARGS)){
String filename =
"/src/examples/ethical_governor/human_hole/governor.ail";
String prop_filename =
"/src/examples/ethical_governor/human_hole/human_hole.psl";
String[] args = new String[3];
args[0] = filename;
args[1] = prop_filename;
args[2] = "3";
AJPF_w_AIL.run(args);
}
}

Then it works but, if I add a second test

@Test
//----------------------------------------------------------------------
public void equation7 () {
if (verifyNoPropertyViolation(JPF_ARGS)){
String filename =
"/src/examples/ethical_governor/human_hole/governor.ail";
String prop_filename =
"/src/examples/ethical_governor/human_hole/human_hole.psl";
String[] args = new String[3];
args[0] = filename;
args[1] = prop_filename;
args[2] = "4";
AJPF_w_AIL.run(args);
}
}

Then the first test runs but the second fails with

gov.nasa.jpf.JPFNativePeerException: exception in native method
java.lang.StringBuilder.append
at
gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:186)
at
gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:73)
at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)

If I reverse the order of the tests then equation7() runs without error
but equation6() fails with the JPFNativePeerException which suggests I
also have some issue with persistent state.

Any suggestions for how to fix these issues.

Louise


--
Dr. Louise Dennis,
Department of Computer Science, Room 117, Ashton Building,
University of Liverpool, Liverpool, L69 3BX, UK.
http://www.csc.liv.ac.uk/~lad/ phone: +44 151 795 4237

[Louise Dennis]

On 17/08/2017 Thu 17 15:09, Louise Dennis wrote:
> I use JPF to verify programs which need to read in and parse files.
>
> I'm in the process of trying to update my parser to use Antlr 4 grammars.
>
> My project is called mcapl and I've added antlr-4.7-complete.jar to
> both mcapl.classpath and mcapl.native_classpath in jpf.properties.
>
>

I've fixed my first (classpath) problem but the problem of some kind of
persistent state in JUnit remains. Obviously I can fix this by
separating out the tests into two separate classes but that is
ultimately going to involve a lot of annoying work across all the
various tests so it would be good to know if there is a better fix.