Null pointer exception when using baselines for safe-stack

[hernanponcedeleon]

The following command raise an exception

java -jar dartagnan/target/dartagnan-3.0.0.jar cat/tso.cat --bound=2 --refinement.baseline=no_oota,uniproc,atomic_rmw --target=TSO --method=caat /home/Dat3M/dartagnan/src/test/resources/lfds/safe_stack-3.bpl

while this one does not

java -jar dartagnan/target/dartagnan-3.0.0.jar cat/tso.cat --bound=2 --target=TSO --method=caat /home/Dat3M/dartagnan/src/test/resources/lfds/safe_stack-3.bpl

[ThomasHaas]

This problem is triggered because of new code related to the PR that introduced the Dependency class (i.e. the dependency analysis). Since then, the BasicRegRelation.getSMTVar method calls task.getProgramEncoder().dependencyEdge(...), so there is a dependency on task.getProgramEncoder. The problem now is this:

• Refinement performs the RelationAnalysis wrt. the baselineModel and not the original memory model.
• Since the RelationAnalysis doesn't take a Wmm as input but a whole VerificationTask, the Refinement code generates a new VerificationTask object with the baselineModel and passes that one to the RelationAnalysis.
• This new VerificationTask object has no encoders associated, so all its Encoders are null.
• When encoding the the baselineModel with NO_OOTA, there is the dep-relation that needs to get encoded, which in particular involves idd (~BasigRegRelation)
• The getSMTVar method call will try to access task.getProgramEncoder(), resulting in a NullPointerException

All this happens because of a combination of hacky code and unfortunate dependencies (the dependency on ProgramEncoder should not be there IMO). I will create another hacky fix for now, by giving the newly created VerificationTask the same ProgramEncoder. Eventually, we need to fix this mess properly though.

[ThomasHaas]

Fixed in #281