null pointer exception running logical compare (orig variables)

[markro49]

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.

[markro49]

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.(InvariantLemma.java:17)
at daikon.simplify.InvariantLemma.makeLemmaAddOrig(InvariantLemma.java:66)
at daikon.tools.compare.LogicalCompare.translateAddOrig(LogicalCompare.java:216)
at daikon.tools.compare.LogicalCompare.comparePpts(LogicalCompare.java:494)
at daikon.tools.compare.LogicalCompare.mainHelper(LogicalCompare.java:803)
at daikon.tools.compare.LogicalCompare.main(LogicalCompare.java:578)

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.