Menu
▾
▴
javapathfinder-svn — source repository related messages (SVN)
You can subscribe to this list here.
| 2008 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(16) |
Jun
(42) |
Jul
(46) |
Aug
(48) |
Sep
(33) |
Oct
(26) |
Nov
(28) |
Dec
(38) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2009 |
Jan
(35) |
Feb
(80) |
Mar
(112) |
Apr
(108) |
May
(102) |
Jun
(126) |
Jul
(89) |
Aug
(82) |
Sep
(36) |
Oct
(7) |
Nov
(1) |
Dec
(4) |
| 2010 |
Jan
(87) |
Feb
|
Mar
(2) |
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: <pc...@us...> - 2009-05-05 02:09:09
|
Revision: 1484
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1484&view=rev
Author: pcorina
Date: 2009-05-05 02:08:17 +0000 (Tue, 05 May 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-04 22:55:08
|
Revision: 1483
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1483&view=rev
Author: frankrimlinger
Date: 2009-05-04 22:54:58 +0000 (Mon, 04 May 2009)
Log Message:
-----------
Realized there is an issue returning to jpf. it seems quite likely that you can paint yourself into a corner, executing paths that return to jpf before all the outstanding choices are traversed. In this case, when the last choice expires, vm^2 will want to exit. Instead, consider each target, be it method, clinit, or exception handler, to be a choice in its own right. Drop to MJI and execute a synthetic INVOKETARGET instruction with a TargetChoiceGenerator. The TARGET instruction just executes over and over until all the targets are traversed. This means *all* returns to jpf just return null. This is much or elegant.
Pushing this reasoning to its logical conclusion, EVERY branch instruction could become a target in the above sense. But this stands the rationale for targeting on its head. We're not targeting because we can, we are targeting because we MUST, in order to reliably control exit to jpf. We don't want to bunch up any more logic in TargetChoiceGenerator than is absolutely necessary.
Realized InvocationChoiceGenerator was not necessary. At the scanner level, we just notify mango of the Methods that we could plausibly invoke, and then unconditionally branch to the next instruction of the current method. (Since mango analysis is bottom up, the predicate transformer along this edge is resolved from the rulebase, unless there is mutual corecursion. That is where things get interesting.) The point is that we rely on MangoTargetLauncher to scan all the methods anyway, so branching into one from within the scan would be overkill and would unnecessarily complicate the scanning logic. Also, since the analysis is now flat, an athrow or return always exits to jpf, so that there is never a need to set up a ScannerStackFrame.
Realized there is an issue for BranchChoiceGenerator. Nominally, the instruction that causes a choice generator to be loaded is the "first instruction" of the transition. For our purposes is better to call this the "source instruction." Nominally, this source instruction gets its "bottom half" executed once for each choice. THe bottom half presumably acquires the current "choice" from the choice generator, adjusts state accordingly, and fires.
We want to fix things up so that the transitions START with the destinations of the branch, that is, the source instruction is never revisited and hence the "bottom half" is skipped. This simplifies scanner logic. Observe that if the first instruction loads a ChoiceGenerator and then returns null, well, then there is a transition and the nextPC is pulled from the top frame of the "snapshot" state for the ChoiceGenerator. Normally, since the first instruction top half doesn't do anything, we would recover the first instruction. But that is not what we want.
So here is the diabolical part. When the ChoiceGenerator advances, there is a notifyChoiceGeneratorAdvanced issued to VMListeners. Well, what if there was a BranchListener whose job it was to examine the BranchChoiceGenerator and "repair" the pc based on the current choice of "next instruction"? Then the next instruction would just execute, and all would be well. This transition would continue executing until null was returned because of a previously visited instruction, a return, or an athrow.
By this means, each scanner branch instruction reports all its children the first time it is visited, via BranchChoiceGenerator, and always returns null. This seems like a good approach, assuming all the smoke and mirrors work out.
1. DONE. Install BranchListener
2. DONE. Rewrite the MangoTargetLauncher to fire INVOKETARGET
3. DONE Write INVOKETARGET, top half and bottom half
4. Write TargetChoiceGenerator
5 Get rid of the old ScanChoiceGenerator, InvocationChoiceGenerator, and ScannerStackFrame. Instead, write InvocationUtil with static methods to provide mango with the destination info it needs given a source invocation instruction.
6. Rehab of BranchChoiceGenerator
7. Bytecode Rehab
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_scanner_ScannerMJI.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoTargetLauncher.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScannerMJI.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchListener.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/INVOKETARGET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetChoiceGenerator.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/VirtualMethodRegistrar.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-04 04:40:50
|
Revision: 1482
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1482&view=rev
Author: frankrimlinger
Date: 2009-05-04 04:40:45 +0000 (Mon, 04 May 2009)
Log Message:
-----------
Overcame conceptual block regarding choice generators. What you load into the choice generator is all the choices for the NEXT instruction. Then you return null, forcing the first choice to be made. Thus, there is no "bottom half" to execute the "first instruction of the transition", because we are using the mechanism in a slightly different way than is described in the documentation. An implication of this is that when you are loading the choice generator, that is the only chance you are going to get to tell mango about the control flow edge from the choice generator instruction to each of the choices. Another implication is that you can mark an instruction with a ScanChoiceGenerator as visited immediately, because you don't revisit to pick up the "bottom half" of the instruction. This definitely simplifies matters.
NOTE: The ScannerStackFrame that you push for the invocation is a one-size-fits-all affair. This works because nobody is going to look inside it anyway. It just needs to be different from a StackFrame so that you will know when it is time for return to jpf phase change.
NOTE: because of the way "advance()" works, the index has to start at -1.
NOTE: the INVOKExxxSCAN instructions are not needed. Don't know what I was thinking here.
TODO: finish cleaning up invocation choice generator to implement the correct pattern. Then should be good-to-go for bytecode rehab, final version.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINITSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACESCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIALSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATICSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUALSCAN.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-04 01:00:44
|
Revision: 1481
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1481&view=rev
Author: frankrimlinger
Date: 2009-05-04 01:00:36 +0000 (Mon, 04 May 2009)
Log Message:
-----------
scanner logic implementation in progress
1. bytecode rehab, one more time with feeling.
a) choicegenerator cleanup
b) if not return or athrow: check to return null if visited.
c) mark as visited, nontrivial case must be set from cg, because multiple visits to bytecode required to service choices.
d) non-return/athrow return null if visited
e) return and athrow instructions return null unless parent frame is not ScannerStackFrame AND ScanChoiceGenerator.done()
2. Write code to capture clinit and exception handler entrypoints.
3. Code to fire clinits from launcher
4. Code to fire exception handlers from launcher
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScanChoiceGenerator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-03 16:57:56
|
Revision: 1480
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1480&view=rev
Author: frankrimlinger
Date: 2009-05-03 16:57:47 +0000 (Sun, 03 May 2009)
Log Message:
-----------
Exceptions have been grocked.
First, the mango catch mechanism cannot be dropped. The point is that a method doesn't "know" where it returns to, so an exception cannot "know" where it will be thrown. All we can do is model the local structure of the throw, and stitch these together when evaluating a nested calling sequence within the target method. Therefore, during the scanning phase, it is meaningless to trace the path of a thrown exception. This is totally spurious information, just an artifact of the scanning process. Therefore, there is no point throwing exceptions in the first place: mango already knows which instructions throw, and why they throw, and there is nothing more to be learned.
So, all the information about exceptions meticulously supplied to the scanner bytecodes must be stripped back out again.
Now here is where things get weird. We still need to simulate all the handler code within the supplied methods and build the corresponding control flow graph segments. Otherwise the mango catchers will have nowhere to send the caught exceptions. So, just like in the case of clinits, we must rely on the target launcher to use MJI to get at these entrypoints. Fortunately, they can be recovered from the MethodInfo class. Its a little trickier than the case of invocations, because there could be multiple handlers in a given method, so you need to arrange to traverse all of them. Also, you must manually push a ScannerStackFrame so that the handler will have something to digest. (Since we are going into scanner mode, we don't have to bother with setting up the heap or the operand stack.)
Now what happens when the handler "returns". There is no problem here, because it will either happen because of a return or an athrow. Either way, we will pop the ScannerStackFrame and detect the jpf StackFrame, and this will trigger a phase change to jpf. Execution will then proceed in the MangoTargetLauncher just after the native call to fire the handler.
Start by writing the launcher code and native methods to scan the handlers. This is a brain-burner.
NB: If you are in scanning phase and you have already visited an instruction, then you should return null, meaning that this path need not be explored.
We need a master counter of ALL outstanding choices within a target method simulation. A return to jpf should just return null if there are outstanding choices. The transition to jpf should only occur when no choices remain. This prevents jpf from backtracking back into a target once it has left it, potentially creating an exponential growth in the number of paths to traverse.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/workstation/Workstation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/BranchChoiceGenerator.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScanChoiceGenerator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-02 20:23:03
|
Revision: 1479
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1479&view=rev
Author: frankrimlinger
Date: 2009-05-02 20:22:52 +0000 (Sat, 02 May 2009)
Log Message:
-----------
Working through details of jpf/scanner invocation phase transition.
Notes: 1) invokevirtual and invokeinterface are almost the same, except invokeinterface does not require access control. 2) mango currently simulates a thrown exception by "returning" an exception object to caller, and then "catching" return values and branching to the handlers or rethrowing as appropriate. The question then becomes, since jpf is now in the driver's seat as far as control flow goes, can we scrap the old "exception catchers" and just model the observed jpf behavior. This really is the way to go, because if the map from jpf simulation to the mango control flow graph is not invertable, there will be problems down the road.
Modified Paths:
--------------
branches/mango/MangoJPF/.settings/org.eclipse.jdt.core.prefs
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScanChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-02 03:30:11
|
Revision: 1478
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1478&view=rev
Author: frankrimlinger
Date: 2009-05-02 03:30:00 +0000 (Sat, 02 May 2009)
Log Message:
-----------
Thinking through scanner invocation issues.
Actually, there is an important reason for BEGIN phase. An invocation called in BEGIN phase needs to pop its arguments off of the caller stack. Otherwise not, since they were not set up in the first place. Failure to pop arguments when transitioning to SCAN will result in inconsistent state when returning to JPF phase. On the flip side, a return to JPF phase needs to push a dummy operand (if required) on the caller opstack.
Recall we know we are returning to JPF if caller is not a ScannerStackFrame. The InvocationChoiceGenerator gets a list of methods to "execute", meaning push a StackFrame. However, instead of pushing a frame, we push a ScannerStackFrame. This extension of StackFrame only sets up pc and mi fields, because that is all the information we have and hopefully all the information required for scanning. All the StackFrame methods which require more information are overridden to throw IllegalStateException("this method is not available in ScannerStackFrame").
Realized there is an obvious way to insure clinits are scanned. Since the code base has to be previewed anyway to build the virtual method table, might as well also take inventory of all the clinits. These can then all be fired by MangoTargetLauncher, end of story. Well, not quite, because firing a clinit is a tricky business. You will need to drop to MJI, and mimic the process used by jpf. First, initalizeScan(ClassInfo) is called for the relevant class. Inside this method we call MethodInfo.createScanDirectCallStub and create a DirectCallScanStackFrame to accomplish invocation of the clinit. The existing apparatus needs to be carefully reworked from the scanner point of view, since we don't have enough state to build full blown frames for the clinits.
Since the clinits are now all scanned out-of-band, their predicate transformers can be resolved as required. Existing mango logic will install these transformers, together with their first-time-only firing trigger, at the required control flow points. These points are specified in JVM2ed section 5.5, e.g. corresponding to new, getstatic, putstatic and invokestatic instructions. Clinits commute with non-clinit predicate transformers backwards to the beginning of time (if specified). The net result is that the clinits do get evaluated in the proper order or not at all. The point is that this is a graph-theoretic issue that is strictly internal to mango proper. All that is required at the scanner level is the flat scan of each clinit to build the corresponding control flow diagrams.
So, the clinit issue is manageable, but not a priority at this time.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/ScannerStackFrame.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTSTATIC.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-02 00:17:26
|
Revision: 1477
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1477&view=rev
Author: frankrimlinger
Date: 2009-05-02 00:15:16 +0000 (Sat, 02 May 2009)
Log Message:
-----------
Although I don't think it will ever happen, there is the theoretical opportunity for a listener to intervene and alter the course of events between phase BEGIN and phase SCAN, so for now BEGIN will be retained. The following check for BEGIN phase and transit to SCAN if detected:
INOKEINTERFACE
INVOKESPECIAL
INVOKESTATIC
INVOKEVIRTUAL
Clinits are a big headache. Since they fire "non-deterministically", they might do so during JPF phase, in which case they would never get scanned. On the upside, clinits cannot form mutually co-recursive systems, so they don't really require the mango treatment anyway. We punt on this for now, but when it comes to pass that a clinit predicate transformer must be resolved, then somehow we have to convince jpf to execute it in scanner mode. This might require some persuasion if the clinit has already fired, but oh well...
Having said that, without a concept of the beginning of time, there is no way to fire the clinits anyway. This is the norm for mango analysis. But sooner or later, there will be a need to really analyze a clinit, and jpf will have to play ball.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-01 18:09:43
|
Revision: 1476
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1476&view=rev
Author: frankrimlinger
Date: 2009-05-01 18:09:42 +0000 (Fri, 01 May 2009)
Log Message:
-----------
cleanup
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-01 18:07:17
|
Revision: 1475
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1475&view=rev
Author: frankrimlinger
Date: 2009-05-01 18:07:15 +0000 (Fri, 01 May 2009)
Log Message:
-----------
Completed rough-out of mango.scanner.bytecode. Tested JPF execution phase by successfully running MangoTargetLauncher. With the test-bed in place, we can switch on scanner phase as planned and code and debug the scanner bytecode functionality one bytecode at a time. Actually, there are only about twenty bytecodes that require special consideration, so this is manageable. There is also the unexplored listener issue. How exactly do clinits fire? What else is going on? Still much to learn.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/F2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/FSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GETSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/GOTO_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2B.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2C.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/I2S.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ICONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNONNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IFNULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ACMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPEQ.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPGT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPLT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IF_ICMPNE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IINC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ILOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INSTANCEOF.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINITSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACESCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIALSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATICSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUALSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ISUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/IXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/JSR_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2D.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/L2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LAND.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCMP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC2_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC_W.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOOKUPSWITCH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LUSHR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/LXOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITORENTER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MONITOREXIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/NOP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/POP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTFIELD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/PUTSTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RET.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/RUNSTART.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SWAP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/TABLESWITCH.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode/
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/VirtualInvocationScan.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/SIPUSH.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-05-01 05:57:25
|
Revision: 1474
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1474&view=rev
Author: pcmehlitz
Date: 2009-05-01 05:57:17 +0000 (Fri, 01 May 2009)
Log Message:
-----------
* opened the exception firewall in JPF.run() - if we encounter a JPFException or another RuntimeException, we pass it on. This is necessary to enable callers to find out if a JPF run was prematurely terminated
* added JPFListenerException and JPFNativePeerException, which are wrapping everything (well almost) that can go wrong during listener notification and native method execution. Both conceptually don't belong to the JPF core, and listener exceptions could even be recoverable (depending on what listener it is)
* renamed JPFTest.runJPFException() -> runJPFappException(), to indicate that we expect an exception in the application. added a runJPFException() to indicate that we expect an exception thrown by JPF (which mostly makes sense for the two JPFExceptions above)
* added a patch to throw InstantiationException and IllegalAccessException during Class.newInstance() - thanks Taehoon Lee
* added test + modified TestNativePeer/JPF accordingly
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/extensions/numeric/test/gov/nasa/jpf/numeric/TestNumericJPF.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestExJPF.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/JPFException.java
trunk/src/gov/nasa/jpf/jvm/ExceptionInfo.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/NativePeer.java
trunk/src/gov/nasa/jpf/jvm/Transition.java
trunk/src/gov/nasa/jpf/search/Search.java
trunk/test/gov/nasa/jpf/jvm/RawTest.java
trunk/test/gov/nasa/jpf/jvm/TestCastJPF.java
trunk/test/gov/nasa/jpf/jvm/TestExceptionJPF.java
trunk/test/gov/nasa/jpf/jvm/TestJPF.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangClass.java
trunk/test/gov/nasa/jpf/jvm/TestJavaLangClassJPF.java
trunk/test/gov/nasa/jpf/jvm/TestNativePeerJPF.java
trunk/test/gov/nasa/jpf/mc/TestRaceJPF.java
trunk/test/gov/nasa/jpf/mc/TestRandomJPF.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/JPFListenerException.java
trunk/src/gov/nasa/jpf/JPFNativePeerException.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-05-01 03:13:22
|
Revision: 1473
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1473&view=rev
Author: frankrimlinger
Date: 2009-05-01 03:12:58 +0000 (Fri, 01 May 2009)
Log Message:
-----------
With the conceptual issues regarding invocation, return, and scanner mode transition under control, resumed bytecode rehab. Several templates have been created for this purpose. Bytecodes which do manipulate the stack, eg, invocations and returns, or offer multiple branches other than for thrown exceptions, throw IllegalStateException("NEED CODE HERE"). (That is, throw at the vm level, NOT the vm^2 level!) Once the rehab is complete, jpf level execution will be functional. The rest of the bytecode functionality can the be written and tested on a pay-as-you-go basis as the missing code exceptions are encountered.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.project
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstructionFactory.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/BIPUSH.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/CHECKCAST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2F.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2I.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/D2L.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DADD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCMPL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DCONST.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DDIV.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DLOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DMUL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DNEG.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DREM.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DRETURN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DSUB.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP2_X2.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X1.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/DUP_X2.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InstructionTemplates.txt
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-30 21:20:58
|
Revision: 1472
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1472&view=rev
Author: frankrimlinger
Date: 2009-04-30 21:20:44 +0000 (Thu, 30 Apr 2009)
Log Message:
-----------
Wiring for scanner virtual invocation in progress.
InvocationChoiceGenerator just needs to return MethodInfo's. But since the descriptor is available, we need to reduce the choice of potential methods down to those which have compatible descriptors. Also, the methods must come from classes which are superclasses of the named class. In some cases this reduction is critical, imagine branching to every single toString().
Invocation works by "executing" a MethodInfo. This means that the MethodInfo pushes a new frame onto the stack. So, the issue is, what exactly is this new frame? First, we want it to be a ScannerStackFrame, to support the scanning strategy.
Tentatively, we ONLY set up the pc and mi ScannerStackFrame fields. These are clearly needed for scanning. All methods of StackFrame which rely on other fields are overridden in ScannerStackFrame to throw IllegalStateException. Hopefully, we will be able to back out of any situation that throws and rewire our way around it.
You should be aware that something out there is listening for executeInstruction notification on behalf of InvokeVirtual. This will probably have to be defeated when scanning. There also must be stuff listening to fire clinits and so on. We just take these as they come.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUALSCAN.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-30 19:32:33
|
Revision: 1471
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1471&view=rev
Author: frankrimlinger
Date: 2009-04-30 19:32:28 +0000 (Thu, 30 Apr 2009)
Log Message:
-----------
VirtualMethodRegistrar now maps a method name to a HashSet of MethodInfo objects with that method name. The survey is accomplished over vm.classpath and vm.bootclasspath/java. To do this, grocked the relationship between bcel and jpf. It turns out that VirtualMethodRegistrar can directly create jpf ClassInfo objects using ClassInfo.getClassInfo(). Although bcel brokers this deal, it's just middleware as far as we are concerned. Since I am now speaking jpf from the get go, it will be much easier to construction the synthetic invocation instructions.
So now its time to think about how InvocationChoiceGenerator will work.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/VirtualMethodRegistrar.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-30 02:20:52
|
Revision: 1470
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1470&view=rev
Author: frankrimlinger
Date: 2009-04-30 02:20:50 +0000 (Thu, 30 Apr 2009)
Log Message:
-----------
java shadow eliminate, final clean up. This should do it, sometimes SVN is stubborn.
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-30 02:18:09
|
Revision: 1469
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1469&view=rev
Author: frankrimlinger
Date: 2009-04-30 02:18:07 +0000 (Thu, 30 Apr 2009)
Log Message:
-----------
java shadow elimiante, cleanup
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-30 02:09:51
|
Revision: 1468
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1468&view=rev
Author: frankrimlinger
Date: 2009-04-30 02:09:44 +0000 (Thu, 30 Apr 2009)
Log Message:
-----------
cleanup of eliminate javaShadow commit
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-30 02:06:15
|
Revision: 1467
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1467&view=rev
Author: frankrimlinger
Date: 2009-04-30 02:06:08 +0000 (Thu, 30 Apr 2009)
Log Message:
-----------
Eliminated shadow java package code.
Well, looks like I have been taking stupid pills. There is absolutely no need for the "shadow" java package. There is no problem parsing the jpf model java package, you just can't use the java ClassLoader. For example, org.apache.bcel.classfile.ClassParser does the job admirably. Moreover, the bcel stuff gives you things you really need, like method signatures. This must be part of the reason this package keeps appearing all over the place in the jpf code base.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/VirtualMethodRegistrar.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/Class.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ClassLoader.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/StackTraceElement.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/System.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/Thread.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/Throwable.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/annotation/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ref/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/security/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/text/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/BrokenBarrierException.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/CyclicBarrier.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/atomic/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/regex/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ubn...@us...> - 2009-04-29 23:33:39
|
Revision: 1466
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1466&view=rev
Author: ubnepvpb
Date: 2009-04-29 23:33:38 +0000 (Wed, 29 Apr 2009)
Log Message:
-----------
Add a method Debug.storeMinimalTraceIf() which is the same as Debug.storeTraceIf() except that it finds a shortest test case.
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/Debug.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/JPF_gov_nasa_jpf_complexcoverage_Debug.java
Added Paths:
-----------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/TraceListener.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ubn...@us...> - 2009-04-29 23:09:43
|
Revision: 1465
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1465&view=rev
Author: ubnepvpb
Date: 2009-04-29 23:09:29 +0000 (Wed, 29 Apr 2009)
Log Message:
-----------
Change SymbolicReal constructors and complexcoverage's Debug.getSymbolicReal to take doubles for min/max instead of ints.
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/Debug.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/JPF_gov_nasa_jpf_complexcoverage_Debug.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicReal.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ne...@us...> - 2009-04-29 22:49:23
|
Revision: 1464
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1464&view=rev
Author: nehas
Date: 2009-04-29 22:49:21 +0000 (Wed, 29 Apr 2009)
Log Message:
-----------
Trying to commit the examples with the source folder.
Added Paths:
-----------
trunk/extensions/guidedsymbolic/examples/twostage/
trunk/extensions/guidedsymbolic/examples/twostage/Data.java
trunk/extensions/guidedsymbolic/examples/twostage/Main.java
trunk/extensions/guidedsymbolic/examples/twostage/ReadThread.java
trunk/extensions/guidedsymbolic/examples/twostage/TwoStage.java
trunk/extensions/guidedsymbolic/examples/twostage/TwoStageThread.java
trunk/extensions/guidedsymbolic/examples/twostage/autoSimple.txt
trunk/extensions/guidedsymbolic/examples/wronglock/
trunk/extensions/guidedsymbolic/examples/wronglock/Data.java
trunk/extensions/guidedsymbolic/examples/wronglock/Main.java
trunk/extensions/guidedsymbolic/examples/wronglock/TClass1.java
trunk/extensions/guidedsymbolic/examples/wronglock/TClass2.java
trunk/extensions/guidedsymbolic/examples/wronglock/WrongLock.java
trunk/extensions/guidedsymbolic/examples/wronglock/autoSimple.txt
Removed Paths:
-------------
trunk/extensions/guidedsymbolic/examples/jdkErrors/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ne...@us...> - 2009-04-29 22:39:43
|
Revision: 1463
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1463&view=rev
Author: nehas
Date: 2009-04-29 22:39:37 +0000 (Wed, 29 Apr 2009)
Log Message:
-----------
Test cases for symbolic execution
Added Paths:
-----------
trunk/extensions/guidedsymbolic/examples/symbolicTestCases/
trunk/extensions/guidedsymbolic/examples/symbolicTestCases/TestCase0.java
trunk/extensions/guidedsymbolic/examples/symbolicTestCases/TestCase1.java
trunk/extensions/guidedsymbolic/examples/symbolicTestCases/TestCase2.java
trunk/extensions/guidedsymbolic/examples/symbolicTestCases/TestCase4.java
trunk/extensions/guidedsymbolic/examples/symbolicTestCases/TestCase5.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-29 22:21:56
|
Revision: 1462
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1462&view=rev
Author: frankrimlinger
Date: 2009-04-29 22:21:48 +0000 (Wed, 29 Apr 2009)
Log Message:
-----------
Writing of VirtualMethodRgistrar in progress.
Modified Paths:
--------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/VirtualMethodRegistrar.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-29 18:19:15
|
Revision: 1461
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1461&view=rev
Author: frankrimlinger
Date: 2009-04-29 18:19:00 +0000 (Wed, 29 Apr 2009)
Log Message:
-----------
Ran into an unpleasant snag while writing VirtualMethodRegistrar extension of ClassLoader to inventory all modelled methods. Recall this inventory is required by InvocationChoiceGenerator. I decided I would use the jpf model of the java package for mango, since it is remarkably full of goodies. But when I tried to read it in with ClassLoader.defineClass(), well, thats a security violation of the root ClassLoader. And rightfully so. No problem, I say, because I can just run virtually under JPF. Unfortunately, defineClass is "not supported yet" in JPF world. Oh well, the fall back plan is just to change "java" to "javaShadow" and refactor the classes. Then I can perform my inventory, just changing "javaShadow" back to "java" wherever I see it. This is ugly, but I have to get on with it.
Hopefully defineClass() will be properly modelled some day in JPF, as the comment seems to suggest. Actually, mango currently parses .class files by hand, but I don't want to go there. This is exactly the code I want to eliminate.
Modified Paths:
--------------
branches/mango/MangoJPF/.classpath
branches/mango/MangoJPF/.project
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/File.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/FileDescriptor.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/FileInputStream.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/FileOutputStream.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/InputStreamReader.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/OutputStreamWriter.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/io/RandomAccessFile.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/Class.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ClassLoader.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/StackTraceElement.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/System.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/Thread.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/Throwable.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/annotation/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/annotation/Inherited.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/annotation/Retention.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ref/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ref/Reference.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ref/ReferenceQueue.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/ref/WeakReference.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/AccessibleObject.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/Constructor.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/Field.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/InvocationTargetException.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/lang/reflect/Method.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/security/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/security/AccessController.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/security/MessageDigest.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/text/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/text/DecimalFormat.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/text/Format.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/text/NumberFormat.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/text/SimpleDateFormat.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/BrokenBarrierException.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/CyclicBarrier.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/atomic/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/atomic/AtomicIntegerFieldUpdater.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/atomic/AtomicLongFieldUpdater.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/concurrent/atomic/AtomicReferenceFieldUpdater.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/regex/
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/regex/Matcher.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/javaShadow/util/regex/Pattern.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/VirtualMethodRegistrar.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetMethodRegistrar.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-04-29 02:33:56
|
Revision: 1460
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1460&view=rev
Author: frankrimlinger
Date: 2009-04-29 02:33:37 +0000 (Wed, 29 Apr 2009)
Log Message:
-----------
Earlier comment was somewhat confused. It is indeed true that you need MJIEnv to parse state object, however, I will never need to do this. I do need to get the structure of the Instruction objects, but these are already at the JVM level, so good to go.
Refined the phase change strategy. We define the extension ScannerStackFrame of StackFrame.
When an invocation instruction executes, if SCANNER.scannerPhase is BEGIN or SCAN, then it sets up an InvocationChoiceGenerator if one is not present already. SCANNER.scannerPhase is set to SCAN.
InvocationChoiceGenerator is trivial for all but virtual invocation. But it is easier just to cover all cases with the same procedure.
The choices of which methods could possibly be virtually invoked are determined by existing mango strategies. However, as classes are now loaded just-in-time, we need to enforce a pro-active class loading up front to make sure the entire targeted code base is surveyed for candidates. No big deal, just a recursive walk though classpath space and a hashed inventory of fully qualified method names and signatures. There is just no other way to do this.
The generated choice instructions will be INVOKExxxSCAN, corresponding to the original INVOKExxx instruction. These synthetic instructions will push a ScannerStackFrame.
A return instruction examines the class of the caller frame. If this class is NOT a ScannerStackFrame, then SCANNER.scannerPhase is set to JPF.
Note that END phase is not needed and has been discarded.
Both the invocation and return instruction families must implement the Transition interface. This just emphasizes the fact that, even when in BEGIN or SCAN phase, these instructions act on JPF state, by adding or removing frames as appropriate. Also, when a return instruction does transition to JPF, it must push some sort of dummy value onto the caller opstack if required, or there will be tears.
The BEGIN transition is probably unnecessary, since the transition from JPF to BEGIN occurs in the native code scan(), just before we box and return the invocation instruction. So it seems likely that the invocation is the next thing to happen anyway. If this proves to be so, then BEGIN can be eliminated.
Note that all this depends very much on the single threaded assumption. A multi-threaded version would, at a minimum, require scannerPhase maintained on a per thread basis. But since multithreading would bring formal analysis to its knees anyway, there is no point to adding this layer of complexity.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/SCANNER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/JPF_mango_scanner_ScannerMJI.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoTargetLauncher.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScanChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ScannerMJI.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACONST_NULL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ARETURN.java
Added Paths:
-----------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/ScannerStackFrame.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationChoiceGenerator.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/TargetMethodRegistrar.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINITSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACESCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIALSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATICSCAN.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUALSCAN.java
Removed Paths:
-------------
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/MethodInfoAdapter.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/ReturnInstructionAdapter.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/StackFrameAdapter.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
