daikon
daikon copied to clipboard
codespecs
null pointer exception running logical compare (orig variables)
In directory daikon/tests/daikon-tests/fib: make clean diffs make txt-logicalcompare
tail of fib.txt-logicalcompare-failed:
Testing preconditions: Testing postconditions: Exception in thread "main" java.lang.NullPointerException at daikon.VarInfo.simplify_name(VarInfo.java:3364) at daikon.VarInfo.simplify_name(VarInfo.java:3338) at daikon.VarInfo.name_using(VarInfo.java:3080) at daikon.inv.unary.string.OneOfString.format_simplify(OneOfString.java:423) at daikon.inv.unary.string.OneOfString.format_using(OneOfString.java:241) at daikon.simplify.InvariantLemma.(InvariantLemma.java:21) at daikon.simplify.InvariantLemma.makeLemmaAddOrig(InvariantLemma.java:70) at daikon.tools.compare.LogicalCompare.translateAddOrig(LogicalCompare.java:208) at daikon.tools.compare.LogicalCompare.comparePpts(LogicalCompare.java:478) at daikon.tools.compare.LogicalCompare.mainHelper(LogicalCompare.java:796) at daikon.tools.compare.LogicalCompare.main(LogicalCompare.java:558)
The exception seems to be caused by processing a FUNCTION var_kind and there is no enclosing_var.
Additional notes from an email dated 4/21/2015:
I've looked at several of the daikon-tests and they all fail with null pointer asserts. In every case it was the VarInfo.enclosing_var field not being set (but the asserts were in different locations).
I used 'fib' as my test case and here is the tail end of the console log (I've added some print statements to provide additional info):
New VarInfo: orig(args.getClass()) ppt: null enclosing_var: null
str_name: orig(args.getClass()), name: orig(args.getClass()), enclosing_var: null
Exception in thread "main" java.lang.NullPointerException
at daikon.VarInfo.simplify_name(VarInfo.java:3245)
at daikon.VarInfo.simplify_name(VarInfo.java:3216)
at daikon.VarInfo.name_using(VarInfo.java:2969)
at daikon.inv.unary.string.OneOfString.format_simplify(OneOfString.java:409)
at daikon.inv.unary.string.OneOfString.format_using(OneOfString.java:230)
at daikon.simplify.InvariantLemma.
So I looked in VarInfo.java at lines 661-724 where this 'orig' VarInfo is created. (Not all 'orig' VarInfos are created here; that's another issue confusing me - but not important for this problem.) The comment on the constructor (called at line 690; defined at 299) specifically says it does not set ppt or enclosing_var fields. I think a call "result.relate_var();" added at the end of the routine would set enclosing_var; but it requires ppt to be set first and I cannot figure out the proper way to do that.
Here is a change to daikon-tests/Makefile you need:
diff -r 32015c33f5ae tests/daikon-tests/Makefile
--- a/tests/daikon-tests/Makefile Sun Apr 19 13:34:19 2015 -0300
+++ b/tests/daikon-tests/Makefile Tue Apr 21 17:53:10 2015 -0700
@@ -12,7 +12,7 @@
@$(MAKE) --no-print-directory BASE?=pwd -C .. $@
Targets that descend to child directories
-clean clean-output txt-diff txt-daikon-suppress-diffed txt-suppress txt-daikon txt-chicory update-goals txt-all merge stats instrument compile diffs inv-checker list-targets chicory chicory-diff esc jml inv txt-daikon-diff txt-chicory-diff spinfo-static dyncomp dyncomp-diff txt-simplify txt-simplify-diff txt-csharpcontract txt-csharpcontract-diff txt-repair-diff txt-esc txt-esc-diff txt-jml-diff txt-merge-diff txt-jaif-diff txt-jaif rtc rtc-diff: +clean clean-output txt-diff txt-daikon-suppress-diffed txt-suppress txt-daikon txt-chicory update-goals txt-all merge stats instrument compile diffs inv-checker list-targets chicory chicory-diff esc jml inv txt-daikon-diff txt-chicory-diff spinfo-static dyncomp dyncomp-diff txt-simplify txt-simplify-diff txt-csharpcontract txt-csharpcontract-diff txt-repair-diff txt-esc txt-esc-diff txt-jml-diff txt-merge-diff txt-jaif-diff txt-jaif rtc rtc-diff txt-logicalcompare txt-logicalcompare-diff: $(MAKE) everything-$@
This allows you to go to any daikon-tests subdirectory and say 'make txt-logicalcompare'.
For what its worth, here are the debug print statements I added to VarInfo.java: --- a/java/daikon/VarInfo.java Sun Apr 19 13:34:19 2015 -0300 +++ b/java/daikon/VarInfo.java Tue Apr 21 17:56:49 2015 -0700 @@ -679,6 +679,7 @@ // Fix the VarDefinition enclosing variable, if any, to point to the // prestate version. This code does not affect the VarInfo yet, but // the side-effected VarDefinition will be passed to "new VarInfo".
-
// if (vi.enclosing_var != null)if (result_vardef.enclosing_var != null) { assert vi.enclosing_var != null : "@AssumeAssertion(nullness): dependent: result_vardef was copied from vi and their enclosing_var fields are the same"; result_vardef.enclosing_var = vi.enclosing_var.prestate_name(); @@ -712,6 +713,10 @@ result.str_name = vi.prestate_name(); }
-
//if (result.ppt != null) result.relate_var();
- System.out.printf ("New VarInfo: %s ppt: %s enclosing_var: %s%n", result, result.ppt, result.enclosing_var);
// At an exit point, parameters are uninteresting, but orig(param) is not. // So don't call orig(param) a parameter. result.set_is_param (false); @@ -3226,6 +3231,8 @@ if (derived != null) return derived.simplify_name ();
+System.out.println("str_name: " + str_name() + ", name: " + name() + ", enclosing_var: " + enclosing_var); + // Build the name by processing back through all of the enclosing variables switch (var_kind) { case FIELD:
That first insert was an initial change I made - I think testing result_vardef is incorrect - but I commented it out to keep things constant for further debugging.