[Soot-list] Dava and synchronized blocks

[Matteo Ceccarello]

Hi all,

I'm trying to use Dava to decompile the |java.net.Socket| class. However 
I keep getting an exception saying: "Could not verify approximated 
Synchronized body!".

According to this email 
http://www.sable.mcgill.ca/pipermail/soot-list/2007-June/001266.html the 
problem may be in different aliases used to enter and exit monitors. 
Hence I tried to apply |CopyPropagator.v().transform(body)| to transform 
the body of methods by propagating copies. In this way aliases seem to 
disappear. Starting from the following jimple representation of 
|Socket.close()|

|
r0 := @this: java.net.Socket
$r3 = r0.<java.net.Socket: java.lang.Object closeLock>
r1 = $r3
entermonitor $r3
$z0 = virtualinvoke r0.<java.net.Socket: boolean isClosed()>()
if $z0 == 0 goto $z1 = r0.<java.net.Socket: boolean created>
exitmonitor r1
return
$z1 = r0.<java.net.Socket: boolean created>
if $z1 == 0 goto r0.<java.net.Socket: boolean closed> = 1
$r4 = r0.<java.net.Socket: java.net.SocketImpl impl>
virtualinvoke $r4.<java.net.SocketImpl: void close()>()
r0.<java.net.Socket: boolean closed> = 1
exitmonitor r1
goto [?= return]
$r5 := @caughtexception
r2 = $r5
exitmonitor r1
throw r2
return|

I correctly get

|r0 := @this: java.net.Socket
$r3 = r0.<java.net.Socket: java.lang.Object closeLock>
r1 = $r3
entermonitor $r3
$z0 = virtualinvoke r0.<java.net.Socket: boolean isClosed()>()
if $z0 == 0 goto $z1 = r0.<java.net.Socket: boolean created>
exitmonitor $r3
return
$z1 = r0.<java.net.Socket: boolean created>
if $z1 == 0 goto r0.<java.net.Socket: boolean closed> = 1
$r4 = r0.<java.net.Socket: java.net.SocketImpl impl>
virtualinvoke $r4.<java.net.SocketImpl: void close()>()
r0.<java.net.Socket: boolean closed> = 1
exitmonitor $r3
goto [?= return]
$r5 := @caughtexception
r2 = $r5
exitmonitor $r3
throw $r5
return|

with no signs of aliases in the |entermonitor| and |exitmonitor| statements

However I keep getting the same exception:

|Exception in thread "main" java.lang.RuntimeException: Could not verify approximated Synchronized body!
Method:
<java.net.Socket: void close()>Body:
===============================================================
[this := this: java.net.Socket, $r3 = closeLock, entermonitor $r3, if this.<java.net.Socket: boolean isClosed()>() == false goto (branch), goto [?= exitmonitor $r3], goto [?= (branch)], exitmonitor $r3, return, if created == false goto (branch), goto [?= closed = true], goto [?= closed = true], closed = true, exitmonitor $r3, goto [?= return], $r5 := @caughtexception, exitmonitor $r3, throw $r5, return, goto [?= $r5 := @caughtexception], goto [?= $r5 := @caughtexception], goto [?= $r5 := @caughtexception]]===============================================================

     at soot.dava.toolkits.base.finders.SynchronizedBlockFinder.find(SynchronizedBlockFinder.java:164)
     at soot.dava.DavaBody.<init>(DavaBody.java:326)
     at soot.dava.Dava.newBody(Dava.java:84)
     at edu.unipd.dei.modgen.generator.printer.ClassPrinter.javaSource(ClassPrinter.java:73)
     at edu.unipd.dei.modgen.generator.printer.ClassPrinter.writeToFile(ClassPrinter.java:195)
     at edu.unipd.dei.modgen.generator.ModelSetGenerator.generate(ModelSetGenerator.java:103)
     at edu.unipd.dei.modgen.tool.Main.main(Main.java:91)|

Anyone has some clues on how I can solve it please?

Thank you
Matteo

-- 
Matteo Ceccarello, Computer Engineering student
Universita' di Padova, Dipartimento di Ingegneria dell'Informazione,
URL: http://www.dei.unipd.it/~ceccarel
LinkedIn: http://it.linkedin.com/pub/matteo-ceccarello/60/322/931/

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20130629/7c0d978b/attachment.html