[Soot-list] dava question

[Dacong Yan]

Hi,

I was using dava, and it threw a RuntimeException saying: "Could not
verify approximated Synchronized body!".

A problem leading to the same exception has been discussed before on
this list (see:
http://www.sable.mcgill.ca/pipermail/soot-list/2007-June/001263.html),
and the conclusion is: it can be resolved by a must-alias analysis or
copy propagation. But it seems that my code caused some other problem.

The minimum code that can reproduce this problem is attached at the
very end. I used the options "-p jb.cp only-stack-locals:false -p
jb.dae only-stack-locals:false" to allow copy propagation, but it
still fails. Is this a known issue? Or do I need other command line
options to make it work?

Thanks,
Tony

--
Dacong (Tony) Yan
Ph.D. Student
Computer Science and Engineering
The Ohio State University, Columbus
http://www.cse.ohio-state.edu/~yan


Source:

public class Sync {
 public void f(String s) {
   synchronized (this) {
     try {
       int a = Integer.parseInt(s);
       if (a == 0) {
         return;
       } else {
         System.out.println();
       }
     } catch (Exception e) {
       throw new RuntimeException();
     }
   }
 }
}

And the Jimple code for function f (java soot.Main -f J -p jb.cp
only-stack-locals:false -p jb.dae only-stack-locals:false Sync):

   public void f(java.lang.String)
   {
       Sync r0;
       java.lang.String r1;
       int i0;
       java.io.PrintStream $r5;
       java.lang.Exception $r6;
       java.lang.RuntimeException $r8;
       java.lang.Throwable $r9;

       r0 := @this: Sync;
       r1 := @parameter0: java.lang.String;
       entermonitor r0;

    label0:
       i0 = staticinvoke <java.lang.Integer: int
parseInt(java.lang.String)>(r1);
       if i0 != 0 goto label3;

    label1:
       exitmonitor r0;

    label2:
       return;

    label3:
       $r5 = <java.lang.System: java.io.PrintStream out>;
       virtualinvoke $r5.<java.io.PrintStream: void println()>();

    label4:
       goto label6;

    label5:
       $r6 := @caughtexception;
       $r8 = new java.lang.RuntimeException;
       specialinvoke $r8.<java.lang.RuntimeException: void <init>()>();
       throw $r8;

    label6:
       exitmonitor r0;

    label7:
       goto label11;

    label8:
       $r9 := @caughtexception;

    label9:
       exitmonitor r0;

    label10:
       throw $r9;

    label11:
       return;

       catch java.lang.Exception from label0 to label1 with label5;
       catch java.lang.Exception from label3 to label4 with label5;
       catch java.lang.Throwable from label0 to label2 with label8;
       catch java.lang.Throwable from label3 to label7 with label8;
       catch java.lang.Throwable from label9 to label10 with label8;
   }