[Javapathfinder-svn] SF.net SVN: javapathfinder:[1419] branches/mango

[<fra...@us...>]

Revision: 1419
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1419&view=rev
Author:   frankrimlinger
Date:     2009-04-19 04:35:28 +0000 (Sun, 19 Apr 2009)

Log Message:
-----------
Used properties from Corina's slides "Symbolic Execution of Bytecodes", e.g., +vm.insn_factory.class=gov.nasa.jpf.symbc.MangoInstructionFactory, to cause JPF to perform symbolic execution.  Tested on Racer, which emitted plausible symbolic output.  Right now, MangoInstructionFactory is just a copy of SymbolicInstructionFactory, but with this plumbing in place, lots of opportunity opens up.  In particular, the instructions can be overriden to 
1. perform whatever classloading activities would nominally take place
2. choose each branch exactly once,
3. hook up a corresponding vertex for a control flow graph created on-the-fly.  

By this means, simply pointing JPF at the method to be analyzed and running will simultaneously create the bytecode model and the control flow diagram required by mango.

There is probably more to it than just playing with instructions, as the choices for branching and backtracking have to be correct.  Probably with the right definition of state, the game will play itself.

Modified Paths:
--------------
    branches/mango/MangoJPF/.classpath
    branches/mango/MangoJPF/META-INF/MANIFEST.MF
    branches/mango/MangoJPF/META-INF/MangoJPF.product
    branches/mango/MangoJPF/Mango/src/mango/worker/javaModel/classParser/ClassParsingAlg.java
    branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/JPF_MIRROR.java

Added Paths:
-----------
    branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/symbc/
    branches/mango/MangoJPF/javapathfinder-trunk-MIRROR/gov/nasa/jpf/symbc/MangoInstructionFactory.java

Removed Paths:
-------------
    branches/mango/target_jars/plugins/jpf_build_jars_1.0.0.jar


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.