boogie-org/jar2bpl

Translate java jar files into Boogie programs

##jar2bpl

Translate java, jar, and apk files into Boogie programs. For a quick start, download the jar file

We are currently under construction. The tool still works but the website needs some tlc.

Build the project using:

gradlew shadowJar

This builds a fat jar containing all dependencies. Test the project by translating itself to boogie as follows:

java -jar build/libs/jar2bpl.jar -j build/classes/main/ -b ouput.bpl

This translation is currently only used by Bixie. To use it with Boogie or Corral, a few changes have to be made that are mentioend in the issues list.

jar2bpl's Issues

value of `$exception` unspecified

I see that $exception of procedures are not assigned a default value, so it remains unspecified in procedures that do not explicitly throw. Should we let $exception := $null; at the beginning of every procedure?

Usage of partial order operator inconsistent with BoogiePL

Follow up on this discussion:
https://boogie.codeplex.com/discussions/576976

Jar2bpl-generated bpl cause boogie to throw resolution errors

Hi,
we are using jar2bpl to generate some bpl files for boogile to analyze. However, boogie throw resolution errors on all the files I had tried.

We tried the jar and apk you provided as the examples. The commands we used are "java -jar jar2bpl.jar -j ../lib/log4j-1.2.16.jar -b out.bpl" and "java -jar ./dist/jar2bpl.jar -j ../jar2bpl_test/regression/android_input/snake.apk -android-jars ../jar2bpl_test/data/ -b ./test.bpl". We also tried our java files and apks. But they all throw the similar errors.

We also tried the generated bpl to all available boogie releases.
The errors are as follows.

Boogie and Dafny, 22 Oct 2012 Oct 22, 2012
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\boogie-nightly\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2.2.41003.0703, Copyright (c) 2003-2012, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(2824,30): Error: cannot refer to a global variable in this context: $heap
C:\Users\qiwang\Desktop\bpl\log4j.bpl(2825,72): Error: undeclared identifier: $obj
2 name resolution errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl

Nightly builds Nov 7, 2011
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\boogie-nightly\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2.2.41003.0703, Copyright (c) 2003-2012, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(2824,30): Error: cannot refer to a global variable in this context: $heap
C:\Users\qiwang\Desktop\bpl\log4j.bpl(2825,72): Error: undeclared identifier: $obj
2 name resolution errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl

Boogie-2011-08-03 Aug 3, 2011 
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\boogie-2011-08-03\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2.2.30803.0706, Copyright (c) 2003-2011, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(66565,23): error: ";" expected
1 parse errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl

Boogie update 2011-03-09 Mar 9, 2011
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\Boogie-2011-03-09\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2.0.0.0, Copyright (c) 2003-2010, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(66565,23): error: ";" expected
1 parse errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl

Boogie update 2010-07-13 Jul 13, 2010 
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\Boogie-2010-07-13\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2, Copyright (c) 2003-2010, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(9084,12): syntax error: invalid UnaryExpression
1 parse errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl

2010-05-16 May 16, 2010 
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\Boogie-2010-05-16\Boogie.exe" C:\Users\qiwang\Desktop\bpl\log4j.bpl
Boogie program verifier version 2, Copyright (c) 2003-2010, Microsoft.
C:\Users\qiwang\Desktop\bpl\log4j.bpl(9084,12): syntax error: invalid UnaryExpression
1 parse errors detected in C:\Users\qiwang\Desktop\bpl\log4j.bpl

1.0.21125.0 Jul 15, 2009
C:\Users\qiwang>"C:\Users\qiwang\Desktop\New folder\Boogie-1.0.21125.0\Boogie.exe" C:\Users\qiwang\Desktop\bpl\snake.bpl
Boogie program verifier version 2.00, Copyright (c) 2003-2009, Microsoft.
C:\Users\qiwang\Desktop\bpl\snake.bpl(158,51): syntax error: invalid AtomExpression
1 parse errors detected in C:\Users\qiwang\Desktop\bpl\snake.bpl    

jar2bpl doesn't clean up properly

When running the unit tests, something is not cleaned up properly, so the second unit test uses a wrong configuration that was left over from the previous test.

Bug in calls to prelude

Calls to prelude function like clone or string compare sometimes have the wrong number of lhs arguments.

division by zero not modeled

It seems that some division by error are missed. For example, modInt is modeled as a boogie function, but the mod operation can actually throw when modulus is 0. Do I need to make modInt a procedure to model this?