Jar2bpl-generated bpl cause boogie to throw resolution errors

[davidyoung8906]

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    

[martinschaef]

Sorry about that. Here is a quick fix:
In each generated Boogie file, you will find the following two lines:

axiom (forall t : javaType :: $heap[$null,$type] <: t);

procedure $new(obj_type:javaType) returns ($obj:ref); requires $heap[$obj,$alloc] == false; ensures $obj != $null; ensures $heap[$obj,$type] == obj_type; ensures $heap[$obj,$alloc] == true;

which are generated as part of the prelude. Replace this by:

procedure $new(obj_type:javaType) returns ($obj:ref);

Then it should work. I'll try to change the code accordingly asap.

[crhf]

@martinschaef in this case, how do you make sure that $null is a subtype of everything?

[martinschaef]

Ha ... that conversation started 9 years ago; I had to think about that for a minute :D. In terms of casting-rules, shouldn't null be a subtype of everything? Because you cast null to everything but you can't cast anything to null.

That is you can write:

String foo = null;
Integer bar = null;

where the null constant is implicitly cast to whatever type you have on the left.
In the opposite direction, there is no Null type that you could cast to.

So if you think of the type lattice, you have java.lang.Object at the top and the null type at the bottom and everything else at the middle (with the exception of primitive types like int which you have to handle separately) ... does that sound right?

[crhf]

Ah, didn't expect such a quick response :) I totally agree that null is a subtype of everything. I mean, since you suggest removing axiom (forall t : javaType :: $heap[$null,$type] <: t); from the prelude, how do you enforce that null is a subtype of everything in the boogie program?

[martinschaef]

Oh ... that again, I would need to think about longer. I assume Boogie changed in the last 9 years, so I'm not sure how you would have to write that axiom. Depending on what type of properties you want to prove, you might not even need to state that subtype relation for null explicitly

[crhf]

It happens that I'm doing a proof about null pointer exception, so I think I need that axiom.., Did you have any way to specify that 9 years ago? Or other workaround that does not need the axiom?

[martinschaef]

That, I don't remember ... note that this issue is 9 years old, but the code is a lot older than that. So my recommendation would be to check the literature of the past 10 years, I'm sure there is a better way to model the heap by now.

[crhf]

I see, thanks for making jar2bpl and helping here :)

[crhf]

btw, would you mind taking a look at the other issue I just created ;)