search

hernanponcedeleon / Dat3M

A verification tool for many memory models
MIT License
77 stars 29 forks source link

Null pointer exception in SymmetryEncoder #376

Closed hernanponcedeleon closed 1 year ago

hernanponcedeleon commented 1 year ago

I get the following null exception when running the attached bpl file with option --encoding.symmetry.breakOn=rf

[24.01.2023] 17:02:02 [ERROR] Dartagnan.main - null
java.lang.NullPointerException: null
        at com.dat3m.dartagnan.encoding.SymmetryEncoder.encodeFullSymmetryBreaking(SymmetryEncoder.java:104) ~[dartagnan-3.1.1.jar:?]
        at com.dat3m.dartagnan.verification.solving.RefinementSolver.run(RefinementSolver.java:136) ~[dartagnan-3.1.1.jar:?]
        at com.dat3m.dartagnan.verification.solving.RefinementSolver.run(RefinementSolver.java:87) ~[dartagnan-3.1.1.jar:?]
        at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:159) [dartagnan-3.1.1.jar:?]

client-code-opt.zip

ThomasHaas commented 1 year ago

Is the exception specific to this code or is it reproducible in other cases as well?

ThomasHaas commented 1 year ago

Symmetry breaking is totally broken right now, at least if run with relations as breaking target (_cf should still work).

hernanponcedeleon commented 1 year ago

I haven't tested in other code than this. But this is qspinlock using the same setting we always used in the cna-verification scripts. Last time I run the whole experiments we were using commit cd63a2e5e1f9be4fc3db16857cc1bbda233d8e5e and it worked, so the bug was introduced after that commit.

ThomasHaas commented 1 year ago

Since the WMM restructuring PR, the symmetry breaking is broken for CAAT