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

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

Revision: 1630
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1630&view=rev
Author:   frankrimlinger
Date:     2009-06-15 18:04:38 +0000 (Mon, 15 Jun 2009)

Log Message:
-----------
Finally traced the invariant bug in the case of incorrect context.  This was a pretty terrifying bug.  It actually occurs in JavaType.getJavaTypeName(), which was incorrectly translated from C++.  Specifically, the local variable name "LocalVar_at_offset_1_lineNumber_0", indicating unknown context, was interpreted incorrectly as a class name X, in the Lx; syntax, because we forgot to check for the ";".  The bogus type returned was "LocalVar_at_offset_1_lineNumber_0", and then InequivalentRef.inequivalentJavaType() made a "risky" comparison which decide that   InequivalentRef.inequivalentJavaType() and "int" were in-equivalent types.  This erroneous result in turn allowed HeapModel.totalVacuumService() to garbage collect the heap, which in turn allowed InvariantAgentTest to return a positive result for invariant detection.  YIKES!

FWIW, the risky comparison was reported in the log window and the console, and I have been systematically ignoring it for about a week now.  So now the warning is much more angry sounding, in the hopes that it will get my attention in the future.

Fixed getJavaTypeName() to check for the ";" before returning a class name, in both Mango and MangoJPF.

With this fix in place, invariant detection operates correctly, so that the conjecture x[5]==x[6] is produced with respect to the itsAWrap loop output heap.  

However, can't finish rewriting itsAWrap.main() because get non-deterministic result as the ArrayIndexOutOfBoundsException and NullPointerException don't vanish as they should.  This is a known bug that I will get to soon.

FIRST, really need to fix the incorrect context bug, as it leads to unsatisfactory output in the specification window.  This is a thankless task as the code will go away with jpf integration, but must establish a baseline. 

Modified Paths:
--------------
    branches/mango/Mango/Mango/src/mango/module/msg/DebugInvariantsMsg.java
    branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentRef.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/model/JavaType.java
    branches/mango/MangoJPF/Mango/src/mango/module/msg/DebugInvariantsMsg.java
    branches/mango/MangoJPF/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentRef.java
    branches/mango/MangoJPF/Mango/src/mango/worker/engine/events/RewriteEvent.java
    branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/agent/ValueHAgent.java
    branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/BaseInvariantAgent.java
    branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/invariant/agent/InvariantTestAgent.java
    branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/model/JavaType.java


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