[Soot-list] is this a bug in MHP analysis?

[peng]

Dear All:
   I find a problem when using the  MHPAnalysis, is this a bug?
    During the mhp analysis of Specjbb:
           JBBmain.java 
           DoArun():
             for (whID = 1; whID <= number_of_warehouses; whID++) {
                myCompany.startAutomated(whID, rampup_time,
measurement_time);
                startJBBthread(whID); 
                ...
             }
           startJBBthread(int whID):
           {
              Thread whThread = new Thread(this);
              whThread.start(); 
           }
I find a problem: the abstract thread modeled for whThread  may happen
in parallel with itself, in another word, another copy of the abstract
thread should be contained in the MHPlist, and the MHP should contain
totally 3 threads: abstract thread for whThread, a copy of it, 
and the main thread. But the mhpAnalysis reports: MHP contains 2
threads, abstract thread, the main thread.

During the inspection of the code, I find the  following if-branch in
MHPanalysis is not covered,  but should be covered:
			if(mayStartMultipleThreadObjects && mayBeRunMultipleTimes)
			{
				MHPLists.add(thread); // add another copy
                        }
the reason is that mayStartMultipleThreadObjects=false, while it should
be true. 

The reason for the wrong value of mayStartMultipleThreadObjects is :
multiRunAllocNodes.contains() should returns true, while it returns
false.

boolean mayStartMultipleThreadObjects =(threadAllocNodes.size() > 1) ||
so.types_for_sites();
if(!mayStartMultipleThreadObjects) 
        
        if(multiRunAllocNodes.contains(threadAllocNodes.iterator().next()))    
        //but the anode corresponds to multiple objects..
         {
         mayStartMultipleThreadObjects = true; 
          }
}


after looking into the AllocNodeFinder.java, I find the roots of  the
problems.
AllocNodeFinder first locates the MultiCalledMethod (McallM), then
compute the MultiRunStmt(MRunS).
this computation is problematic, 
because the McallM can be influenced by the MRunS. and also, the MRunS
can be influenced by MCallM.
the computation can be simplified as:
1 MRunS_orig| McallM_on_CG -> MCallM 
2 McallM-> McallM_prop 
3 MCallM_prop|MRunS_orig-> MRunS 

For Step1:
(when we compute the MCallM, we must take the MRunS_orig into account,
i.e., the for-loop, but the implementation simply misses the for-loop
during the computing of MCallM, and also, there is no fixpoint-style
computation later, that is also why the MHPanalysis reports whThread in
specjbb does run for multiple times.)
For Step2:
(the propagation is  placed in a wrong place in the original
implementation, actually nothing is propagated in the original version,
that is also the reason why a concurrencyModificationException in
propagate is not triggered)
For step3:
(This is implemented in the AllocNodeFinder.find() method, and no
problem)

Is this really a bug in soot2.4.0 ??
Thanks in advance.


Regards
Peng