search

hernanponcedeleon / Dat3M

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

Problem with cutting #381

Closed hernanponcedeleon closed 1 year ago

hernanponcedeleon commented 1 year ago

Running this command

java -jar dartagnan/target/dartagnan-3.1.1.jar cat/c11.cat --target=c11 dartagnan/src/test/resources/lfds/safe_stack.bpl

results in this problem

 ===== Iteration: 1 =====
Solving time(ms): 4933
[25.01.2023] 17:19:59 [ERROR] Dartagnan.main - Undefined relation name (co \ rs_prime) ; co.
java.lang.IllegalArgumentException: Undefined relation name (co \ rs_prime) ; co.
        at com.google.common.base.Preconditions.checkArgument(Preconditions.java:220) ~[guava-31.1-jre.jar:?]
        at com.dat3m.dartagnan.wmm.Wmm.getRelation(Wmm.java:83) ~[dartagnan-3.1.1.jar:?]
        at com.dat3m.dartagnan.solver.caat4wmm.basePredicates.DynamicDefaultWMMGraph.repopulate(DynamicDefaultWMMGraph.java:36) ~[dartagnan-3.1.1.jar:?]
        at com.dat3m.dartagnan.solver.caat.predicates.PredicateHierarchy.populate(PredicateHierarchy.java:75) ~[dartagnan-3.1.1.jar:?]
        at com.dat3m.dartagnan.solver.caat.CAATModel.populate(CAATModel.java:68) ~[dartagnan-3.1.1.jar:?]
        at com.dat3m.dartagnan.solver.caat.CAATSolver.check(CAATSolver.java:63) ~[dartagnan-3.1.1.jar:?]
        at com.dat3m.dartagnan.solver.caat4wmm.WMMSolver.check(WMMSolver.java:61) ~[dartagnan-3.1.1.jar:?]
        at com.dat3m.dartagnan.verification.solving.RefinementSolver.run(RefinementSolver.java:171) ~[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:?]

I suspect it might be related to #315

ThomasHaas commented 1 year ago

I assume this error is due to aliasing. The relation in the memory model is mo but here we look for co.

Either way, CAAT should fail on the C11 memory model due to being unable to cut the negated recursion. It might not throw an error, because the recursion is implicit in a transitive closure.

hernanponcedeleon commented 1 year ago

Probably the same problem as in #459. Fixed by ed03fe348e3b80cf9c1dcf3da054309186bf37c0