NPE on loading corrupt proofs

[jwiesler]

I think some rules leave corrupted RuleApps when they fail and it is therefore not safe to call getStatistics on a proof that failed to load.
The tool should either distinguish the two cases load failed and proof is not closed or at least catch the NPE and not crash the whole tool.

[INFO] Contract: `de.wiesler.BucketPointers[de.wiesler.BucketPointers::bucketStart(int)].JML model_behavior operation contract.0`
    [INFO] Proof found: proofs\BucketPointers\de.wiesler.BucketPointers(de.wiesler.BucketPointers__bucketStart(int)).JML model_behavior operation contract.0.proof. Try loading.
Exception in thread "main" java.lang.NullPointerException: Cannot invoke "de.uka.ilkd.key.rule.RuleApp.rule()" because the return value of "de.uka.ilkd.key.proof.Node.getAppliedRuleApp()" is null
        at de.uka.ilkd.key.proof.Statistics$TemporaryStatistics.interactiveRuleApps(Statistics.java:313)
        at de.uka.ilkd.key.proof.Statistics$TemporaryStatistics.changeOnNode(Statistics.java:260)
        at de.uka.ilkd.key.proof.Statistics.<init>(Statistics.java:93)
        at de.uka.ilkd.key.proof.Statistics.<init>(Statistics.java:117)
        at de.uka.ilkd.key.proof.Proof.getStatistics(Proof.java:1216)
        at de.uka.ilkd.key.CheckerKt.generateSummary(Checker.kt:422)
        at de.uka.ilkd.key.CheckerKt.access$generateSummary(Checker.kt:1)
        at de.uka.ilkd.key.Checker.printStatistics(Checker.kt:352)
        at de.uka.ilkd.key.Checker.loadProof(Checker.kt:339)
        at de.uka.ilkd.key.Checker.runContract(Checker.kt:268)
        at de.uka.ilkd.key.Checker.access$runContract(Checker.kt:53)
        at de.uka.ilkd.key.Checker$run$4$2.invoke(Checker.kt:229)
        at de.uka.ilkd.key.Checker$run$4$2.invoke(Checker.kt:214)
        at de.uka.ilkd.key.Checker.printBlock(Checker.kt:179)
        at de.uka.ilkd.key.Checker$run$4.invoke(Checker.kt:214)
        at de.uka.ilkd.key.Checker$run$4.invoke(Checker.kt:193)
        at de.uka.ilkd.key.Checker.printBlock(Checker.kt:179)
        at de.uka.ilkd.key.Checker.run(Checker.kt:193)
        at de.uka.ilkd.key.Checker.run(Checker.kt:162)
        at com.github.ajalt.clikt.parsers.Parser.parse(Parser.kt:170)
        at com.github.ajalt.clikt.parsers.Parser.parse(Parser.kt:16)
        at com.github.ajalt.clikt.core.CliktCommand.parse(CliktCommand.kt:258)
        at com.github.ajalt.clikt.core.CliktCommand.parse$default(CliktCommand.kt:255)
        at com.github.ajalt.clikt.core.CliktCommand.main(CliktCommand.kt:273)
        at com.github.ajalt.clikt.core.CliktCommand.main(CliktCommand.kt:298)
        at de.uka.ilkd.key.CheckerKt.main(Checker.kt:393)

[jwiesler]

IMO no matter what happens when loading the proof, this should never be able to crash the tool. It should always mark the proof as failed, print the stack trace and move on.

When using experimental features exceptions often happen when loading old proof files or even when loading the code. If I want to check 300 proof files I dont want to rerun it every time proof 277 fails to see if any of the remaining proofs fail as well, especially if this takes 3 hours as in my case.

[wadoon]

You know about some of the command line switches of ci-tool? For example, --contract and --forbidden-contract.

[jwiesler]

How should they help here? I think the tool is for checking that all proofs load and I can't do this, since it crashes after one fails to load.

Of course I can load proofs individually, but I already can do this manually using KeY. I want to find all files that fail and I can't just "continue after the latest crash" and using --contract might require hundreds of contracts to list manually.

[wadoon]

First, get all possible contracts:

$ contracts=$(java -cp tools/key-2.10.0-exe.jar:tools/citool-1.4.0-mini.jar de.uka.ilkd.key.CheckerKt --dry-run project.key | grep 'Contract:' | cut -f 2 -d'`')

Second, call ci-tool for each contract:

$ for c in $contracts; do
  java -cp tools/key-2.10.0-exe.jar:tools/citool-1.4.0-mini.jar de.uka.ilkd.key.CheckerKt --contract "$c" project.key 
done

[jwiesler]

But that does everything i want the tool to do making it essentially worthless for me.

What speaks against just making the method exception safe?