diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java index 843083fe63..9227ebc33f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java @@ -357,14 +357,14 @@ public static List getScopeTags() { public static String loadMO(String mo) { return switch (mo) { case ACQ_REL, ACQUIRE -> ACQUIRE; - default -> ""; + default -> ATOM; }; } public static String storeMO(String mo) { return switch (mo) { case ACQ_REL, RELEASE -> RELEASE; - default -> ""; + default -> ATOM; }; } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java index 62b4010b85..73b276886a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorSpirvVulkan.java @@ -69,6 +69,7 @@ public List visitSpirvXchg(SpirvXchg e) { VulkanRMW rmw = EventFactory.Vulkan.newRMW(e.getAddress(), e.getResultRegister(), e.getValue(), mo, scope); rmw.addTags(toVulkanTags(e.getTags())); + replaceAcqRelTag(rmw, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE); rmw.setFunction(e.getFunction()); return visitVulkanRMW(rmw); } @@ -82,6 +83,7 @@ public List visitSpirvRMW(SpirvRmw e) { e.getOperand(), e.getOperator(), mo, scope); rmwOp.setFunction(e.getFunction()); rmwOp.addTags(toVulkanTags(e.getTags())); + replaceAcqRelTag(rmwOp, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE); return visitVulkanRMWOp(rmwOp); } @@ -105,6 +107,7 @@ public List visitSpirvCmpXchg(SpirvCmpXchg e) { e.getExpectedValue(), e.getStoreValue(), moToVulkanTag(spvMoEq), scope); cmpXchg.setFunction(e.getFunction()); cmpXchg.addTags(toVulkanTags(eqTags)); + replaceAcqRelTag(cmpXchg, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE); return visitVulkanCmpXchg(cmpXchg); } @@ -118,6 +121,7 @@ public List visitSpirvRmwExtremum(SpirvRmwExtremum e) { e.getOperator(), e.getValue(), mo, scope); rmw.setFunction(e.getFunction()); rmw.addTags(toVulkanTags(e.getTags())); + replaceAcqRelTag(rmw, Tag.Vulkan.ACQUIRE, Tag.Vulkan.RELEASE); return visitVulkanRMWExtremum(rmw); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorVulkan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorVulkan.java index 50cc44479a..802f7f63f8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorVulkan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorVulkan.java @@ -11,11 +11,29 @@ import com.dat3m.dartagnan.program.event.core.*; import java.util.List; +import java.util.Set; +import java.util.stream.Collectors; import static com.dat3m.dartagnan.program.event.EventFactory.*; public class VisitorVulkan extends VisitorBase { + private static final Set commonTags = Set.of( + Tag.Vulkan.SUB_GROUP, Tag.Vulkan.WORK_GROUP, + Tag.Vulkan.QUEUE_FAMILY, Tag.Vulkan.DEVICE, + Tag.Vulkan.NON_PRIVATE, Tag.Vulkan.ATOM, + Tag.Vulkan.SC0, Tag.Vulkan.SC1); + + private static final Set semScTags = Set.of(Tag.Vulkan.SEMSC0, Tag.Vulkan.SEMSC1); + + private static final Set loadTags = Set.of( + Tag.Vulkan.ACQUIRE, Tag.Vulkan.VISIBLE, Tag.Vulkan.SEM_VISIBLE); + + private static final Set storeTags = Set.of( + Tag.Vulkan.RELEASE, Tag.Vulkan.AVAILABLE, Tag.Vulkan.SEM_AVAILABLE); + + private int labelIdx = 0; + @Override public List visitVulkanRMW(VulkanRMW e) { Register resultRegister = e.getResultRegister(); @@ -24,8 +42,8 @@ public List visitVulkanRMW(VulkanRMW e) { Register dummy = e.getFunction().newRegister(resultRegister.getType()); Load load = newRMWLoadWithMo(dummy, address, Tag.Vulkan.loadMO(mo)); RMWStore store = newRMWStoreWithMo(load, address, e.getValue(), Tag.Vulkan.storeMO(mo)); - this.propagateTags(e, load); - this.propagateTags(e, store); + propagateLoadTags(e, load); + propagateStoreTags(e, store); return eventSequence( load, store, @@ -42,8 +60,8 @@ public List visitVulkanRMWOp(VulkanRMWOp e) { Load load = newRMWLoadWithMo(dummy, address, Tag.Vulkan.loadMO(mo)); RMWStore store = newRMWStoreWithMo(load, address, expressions.makeIntBinary(dummy, e.getOperator(), e.getOperand()), Tag.Vulkan.storeMO(mo)); - this.propagateTags(e, load); - this.propagateTags(e, store); + propagateLoadTags(e, load); + propagateStoreTags(e, store); return eventSequence( load, store, @@ -61,8 +79,8 @@ public List visitVulkanRMWExtremum(VulkanRMWExtremum e) { Expression cmpExpr = expressions.makeIntCmp(dummy, e.getOperator(), e.getValue()); Expression ite = expressions.makeITE(cmpExpr, dummy, e.getValue()); RMWStore store = newRMWStoreWithMo(load, address, ite, Tag.Vulkan.storeMO(mo)); - this.propagateTags(e, load); - this.propagateTags(e, store); + propagateLoadTags(e, load); + propagateStoreTags(e, store); return eventSequence( load, store, @@ -78,13 +96,13 @@ public List visitVulkanCmpXchg(VulkanCmpXchg e) { Expression expected = e.getExpectedValue(); Expression value = e.getStoreValue(); Register cmpResultRegister = e.getFunction().newRegister(types.getBooleanType()); - Label casEnd = newLabel("CAS_end"); + Label casEnd = newLabel("CAS_end_" + labelIdx++); Load load = newRMWLoadWithMo(resultRegister, address, Tag.Vulkan.loadMO(mo)); RMWStore store = newRMWStoreWithMo(load, address, value, Tag.Vulkan.storeMO(mo)); Local local = newLocal(cmpResultRegister, expressions.makeEQ(resultRegister, expected)); CondJump condJump = newJumpUnless(cmpResultRegister, casEnd); - this.propagateTags(e, load); - this.propagateTags(e, store); + propagateLoadTags(e, load); + propagateStoreTags(e, store); return eventSequence( load, local, @@ -94,45 +112,19 @@ public List visitVulkanCmpXchg(VulkanCmpXchg e) { ); } - private void propagateTags(Event source, Event target) { - for (String tag : List.of(Tag.Vulkan.SUB_GROUP, Tag.Vulkan.WORK_GROUP, Tag.Vulkan.QUEUE_FAMILY, Tag.Vulkan.DEVICE, - Tag.Vulkan.NON_PRIVATE, Tag.Vulkan.ATOM, Tag.Vulkan.SC0, Tag.Vulkan.SC1, Tag.Vulkan.SEMSC0, Tag.Vulkan.SEMSC1)) { - if (source.hasTag(tag)) { - target.addTags(tag); - } - } - if (target instanceof Load) { - // Atomic loads are always visible - if (source.hasTag(Tag.Vulkan.ATOM)) { - target.addTags(Tag.Vulkan.VISIBLE); - } - if (source.hasTag(Tag.Vulkan.SEM_VISIBLE)) { - target.addTags(Tag.Vulkan.SEM_VISIBLE); - } - // Remove tag if it refers to the release write - if (!source.hasTag(Tag.Vulkan.ACQUIRE) && source.hasTag(Tag.Vulkan.RELEASE)) { - target.removeTags(Tag.Vulkan.SEMSC0); - target.removeTags(Tag.Vulkan.SEMSC1); - } - if (source.hasTag(Tag.Vulkan.VISDEVICE)) { - target.addTags(Tag.Vulkan.VISDEVICE); - } - } else if (target instanceof Store) { - // Atomic stores are always available - if (source.hasTag(Tag.Vulkan.ATOM)) { - target.addTags(Tag.Vulkan.AVAILABLE); - } - if (source.hasTag(Tag.Vulkan.SEM_AVAILABLE)) { - target.addTags(Tag.Vulkan.SEM_AVAILABLE); - } - // Remove tag if it refers to the acquire read - if (!source.hasTag(Tag.Vulkan.RELEASE) && source.hasTag(Tag.Vulkan.ACQUIRE)) { - target.removeTags(Tag.Vulkan.SEMSC0); - target.removeTags(Tag.Vulkan.SEMSC1); - } - if (source.hasTag(Tag.Vulkan.AVDEVICE)) { - target.addTags(Tag.Vulkan.AVDEVICE); - } - } + private void propagateLoadTags(Event source, Event target) { + boolean isAcq = source.hasTag(Tag.Vulkan.ACQUIRE); + Set tags = source.getTags().stream() + .filter(t -> commonTags.contains(t) || loadTags.contains(t) || isAcq && semScTags.contains(t)) + .collect(Collectors.toSet()); + target.addTags(tags); + } + + private void propagateStoreTags(Event source, Event target) { + boolean isRel = source.hasTag(Tag.Vulkan.RELEASE); + Set tags = source.getTags().stream() + .filter(t -> commonTags.contains(t) || storeTags.contains(t) || isRel && semScTags.contains(t)) + .collect(Collectors.toSet()); + target.addTags(tags); } } diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvChecksTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvChecksTest.java new file mode 100644 index 0000000000..5ff198b1ab --- /dev/null +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/spirv/basic/SpirvChecksTest.java @@ -0,0 +1,151 @@ +package com.dat3m.dartagnan.spirv.basic; + +import com.dat3m.dartagnan.configuration.Arch; +import com.dat3m.dartagnan.encoding.ProverWithTracker; +import com.dat3m.dartagnan.parsers.cat.ParserCat; +import com.dat3m.dartagnan.parsers.program.ProgramParser; +import com.dat3m.dartagnan.program.Program; +import com.dat3m.dartagnan.utils.Result; +import com.dat3m.dartagnan.verification.VerificationTask; +import com.dat3m.dartagnan.verification.solving.AssumeSolver; +import com.dat3m.dartagnan.verification.solving.RefinementSolver; +import com.dat3m.dartagnan.wmm.Wmm; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.sosy_lab.common.ShutdownManager; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.log.BasicLogManager; +import org.sosy_lab.java_smt.SolverContextFactory; +import org.sosy_lab.java_smt.api.SolverContext; + +import java.io.File; +import java.io.IOException; +import java.util.Arrays; +import java.util.EnumSet; + +import static com.dat3m.dartagnan.configuration.Property.CAT_SPEC; +import static com.dat3m.dartagnan.configuration.Property.PROGRAM_SPEC; +import static com.dat3m.dartagnan.utils.ResourceHelper.getRootPath; +import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath; +import static com.dat3m.dartagnan.utils.Result.*; +import static org.junit.Assert.assertEquals; + +@RunWith(Parameterized.class) +public class SpirvChecksTest { + + private final String modelPath = getRootPath("cat/spirv-check.cat"); + private final String programPath; + private final int bound; + private final Result expected; + + public SpirvChecksTest(String file, int bound, Result expected) { + this.programPath = getTestResourcePath("spirv/basic/" + file); + this.bound = bound; + this.expected = expected; + } + + @Parameterized.Parameters(name = "{index}: {0}, {1}, {2}") + public static Iterable data() throws IOException { + return Arrays.asList(new Object[][]{ + {"empty-exists-false.spv.dis", 1, PASS}, + {"empty-exists-true.spv.dis", 1, PASS}, + {"empty-forall-false.spv.dis", 1, PASS}, + {"empty-forall-true.spv.dis", 1, PASS}, + {"empty-not-exists-false.spv.dis", 1, PASS}, + {"empty-not-exists-true.spv.dis", 1, PASS}, + {"init-forall.spv.dis", 1, PASS}, + {"init-forall-split.spv.dis", 1, PASS}, + {"init-forall-not-exists.spv.dis", 1, PASS}, + {"init-forall-not-exists-fail.spv.dis", 1, PASS}, + {"uninitialized-exists.spv.dis", 1, PASS}, + {"uninitialized-forall.spv.dis", 1, PASS}, + {"uninitialized-private-exists.spv.dis", 1, PASS}, + {"uninitialized-private-forall.spv.dis", 1, PASS}, + {"undef-exists.spv.dis", 1, PASS}, + {"undef-forall.spv.dis", 1, PASS}, + {"read-write.spv.dis", 1, PASS}, + {"vector-init.spv.dis", 1, PASS}, + {"vector.spv.dis", 1, PASS}, + {"array.spv.dis", 1, PASS}, + {"array-of-vector.spv.dis", 1, PASS}, + {"array-of-vector1.spv.dis", 1, PASS}, + {"vector-read-write.spv.dis", 1, PASS}, + {"spec-id-integer.spv.dis", 1, PASS}, + {"spec-id-boolean.spv.dis", 1, PASS}, + {"mixed-size.spv.dis", 1, PASS}, + {"ids.spv.dis", 1, PASS}, + {"builtin-constant.spv.dis", 1, PASS}, + {"builtin-variable.spv.dis", 1, PASS}, + {"builtin-default-config.spv.dis", 1, PASS}, + {"builtin-all-123.spv.dis", 1, PASS}, + {"builtin-all-321.spv.dis", 1, PASS}, + {"branch-cond-ff.spv.dis", 1, PASS}, + {"branch-cond-ff-inverted.spv.dis", 1, PASS}, + {"branch-cond-bf.spv.dis", 1, UNKNOWN}, + {"branch-cond-bf.spv.dis", 2, PASS}, + {"branch-cond-fb.spv.dis", 1, UNKNOWN}, + {"branch-cond-fb.spv.dis", 2, PASS}, + {"branch-cond-struct.spv.dis", 1, PASS}, + {"branch-cond-struct-read-write.spv.dis", 1, PASS}, + {"branch-race.spv.dis", 1, PASS}, + {"branch-loop.spv.dis", 2, UNKNOWN}, + {"branch-loop.spv.dis", 3, PASS}, + {"loop-struct-cond.spv.dis", 1, UNKNOWN}, + {"loop-struct-cond.spv.dis", 2, PASS}, + {"loop-struct-cond-suffix.spv.dis", 1, UNKNOWN}, + {"loop-struct-cond-suffix.spv.dis", 2, PASS}, + {"loop-struct-cond-sequence.spv.dis", 2, UNKNOWN}, + {"loop-struct-cond-sequence.spv.dis", 3, PASS}, + {"loop-struct-cond-nested.spv.dis", 2, UNKNOWN}, + {"loop-struct-cond-nested.spv.dis", 3, PASS}, + {"phi.spv.dis", 1, PASS}, + {"phi-unstruct-true.spv.dis", 1, PASS}, + {"phi-unstruct-false.spv.dis", 1, PASS}, + {"cmpxchg-const-const.spv.dis", 1, PASS}, + {"cmpxchg-const-reg.spv.dis", 1, PASS}, + {"cmpxchg-reg-const.spv.dis", 1, PASS}, + {"cmpxchg-reg-reg.spv.dis", 1, PASS}, + {"memory-scopes.spv.dis", 1, PASS}, + {"rmw-extremum-true.spv.dis", 1, PASS}, + {"rmw-extremum-false.spv.dis", 1, PASS}, + {"push-constants.spv.dis", 1, PASS}, + {"push-constants-pod.spv.dis", 1, PASS}, + {"push-constant-mixed.spv.dis", 1, PASS} + }); + } + + @Test + public void testAllSolvers() throws Exception { + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, RefinementSolver.run(ctx, prover, mkTask()).getResult()); + } + try (SolverContext ctx = mkCtx(); ProverWithTracker prover = mkProver(ctx)) { + assertEquals(expected, AssumeSolver.run(ctx, prover, mkTask()).getResult()); + } + } + + private SolverContext mkCtx() throws InvalidConfigurationException { + Configuration cfg = Configuration.builder().build(); + return SolverContextFactory.createSolverContext( + cfg, + BasicLogManager.create(cfg), + ShutdownManager.create().getNotifier(), + SolverContextFactory.Solvers.Z3); + } + + private ProverWithTracker mkProver(SolverContext ctx) { + return new ProverWithTracker(ctx, "", SolverContext.ProverOptions.GENERATE_MODELS); + } + + private VerificationTask mkTask() throws Exception { + VerificationTask.VerificationTaskBuilder builder = VerificationTask.builder() + .withConfig(Configuration.builder().build()) + .withBound(bound) + .withTarget(Arch.VULKAN); + Program program = new ProgramParser().parse(new File(programPath)); + Wmm mcm = new ParserCat().parse(new File(modelPath)); + return builder.build(program, mcm, EnumSet.of(CAT_SPEC)); + } +} diff --git a/dartagnan/src/test/resources/spirv/basic/builtin-all-123.spv.dis b/dartagnan/src/test/resources/spirv/basic/builtin-all-123.spv.dis index fc3e0a6504..b1dbfebc40 100644 --- a/dartagnan/src/test/resources/spirv/basic/builtin-all-123.spv.dis +++ b/dartagnan/src/test/resources/spirv/basic/builtin-all-123.spv.dis @@ -55,7 +55,7 @@ %c0 = OpConstant %uint 0 %c1 = OpConstant %uint 1 %c2 = OpConstant %uint 2 - %c64 = OpConstant %uint 64 + %c68 = OpConstant %uint 68 %init = OpConstant %uint 999 %v3init = OpConstantComposite %v3uint %init %init %init @@ -83,7 +83,7 @@ %label = OpLabel %in_SubgroupLocalInvocationId = OpLoad %uint %gl_SubgroupLocalInvocationId - OpAtomicStore %out_SubgroupLocalInvocationId %c1 %c64 %in_SubgroupLocalInvocationId + OpAtomicStore %out_SubgroupLocalInvocationId %c1 %c68 %in_SubgroupLocalInvocationId %in0_ptr_LocalInvocationId = OpAccessChain %ptr_uint %gl_LocalInvocationId %c0 %in1_ptr_LocalInvocationId = OpAccessChain %ptr_uint %gl_LocalInvocationId %c1 @@ -94,12 +94,12 @@ %out0_ptr_LocalInvocationId = OpAccessChain %ptr_uint %out_LocalInvocationId %c0 %out1_ptr_LocalInvocationId = OpAccessChain %ptr_uint %out_LocalInvocationId %c1 %out2_ptr_LocalInvocationId = OpAccessChain %ptr_uint %out_LocalInvocationId %c2 - OpAtomicStore %out0_ptr_LocalInvocationId %c1 %c64 %v0_LocalInvocationId - OpAtomicStore %out1_ptr_LocalInvocationId %c1 %c64 %v1_LocalInvocationId - OpAtomicStore %out2_ptr_LocalInvocationId %c1 %c64 %v2_LocalInvocationId + OpAtomicStore %out0_ptr_LocalInvocationId %c1 %c68 %v0_LocalInvocationId + OpAtomicStore %out1_ptr_LocalInvocationId %c1 %c68 %v1_LocalInvocationId + OpAtomicStore %out2_ptr_LocalInvocationId %c1 %c68 %v2_LocalInvocationId %in_LocalInvocationIndex = OpLoad %uint %gl_LocalInvocationIndex - OpAtomicStore %out_LocalInvocationIndex %c1 %c64 %in_LocalInvocationIndex + OpAtomicStore %out_LocalInvocationIndex %c1 %c68 %in_LocalInvocationIndex %in0_ptr_GlobalInvocationId = OpAccessChain %ptr_uint %gl_GlobalInvocationId %c0 %in1_ptr_GlobalInvocationId = OpAccessChain %ptr_uint %gl_GlobalInvocationId %c1 @@ -110,15 +110,15 @@ %out0_ptr_GlobalInvocationId = OpAccessChain %ptr_uint %out_GlobalInvocationId %c0 %out1_ptr_GlobalInvocationId = OpAccessChain %ptr_uint %out_GlobalInvocationId %c1 %out2_ptr_GlobalInvocationId = OpAccessChain %ptr_uint %out_GlobalInvocationId %c2 - OpAtomicStore %out0_ptr_GlobalInvocationId %c1 %c64 %v0_GlobalInvocationId - OpAtomicStore %out1_ptr_GlobalInvocationId %c1 %c64 %v1_GlobalInvocationId - OpAtomicStore %out2_ptr_GlobalInvocationId %c1 %c64 %v2_GlobalInvocationId + OpAtomicStore %out0_ptr_GlobalInvocationId %c1 %c68 %v0_GlobalInvocationId + OpAtomicStore %out1_ptr_GlobalInvocationId %c1 %c68 %v1_GlobalInvocationId + OpAtomicStore %out2_ptr_GlobalInvocationId %c1 %c68 %v2_GlobalInvocationId %in_DeviceIndex = OpLoad %uint %gl_DeviceIndex - OpAtomicStore %out_DeviceIndex %c1 %c64 %in_DeviceIndex + OpAtomicStore %out_DeviceIndex %c1 %c68 %in_DeviceIndex %in_SubgroupId = OpLoad %uint %gl_SubgroupId - OpAtomicStore %out_SubgroupId %c1 %c64 %in_SubgroupId + OpAtomicStore %out_SubgroupId %c1 %c68 %in_SubgroupId %in0_ptr_WorkgroupId = OpAccessChain %ptr_uint %gl_WorkgroupId %c0 %in1_ptr_WorkgroupId = OpAccessChain %ptr_uint %gl_WorkgroupId %c1 @@ -129,12 +129,12 @@ %out0_ptr_WorkgroupId = OpAccessChain %ptr_uint %out_WorkgroupId %c0 %out1_ptr_WorkgroupId = OpAccessChain %ptr_uint %out_WorkgroupId %c1 %out2_ptr_WorkgroupId = OpAccessChain %ptr_uint %out_WorkgroupId %c2 - OpAtomicStore %out0_ptr_WorkgroupId %c1 %c64 %v0_WorkgroupId - OpAtomicStore %out1_ptr_WorkgroupId %c1 %c64 %v1_WorkgroupId - OpAtomicStore %out2_ptr_WorkgroupId %c1 %c64 %v2_WorkgroupId + OpAtomicStore %out0_ptr_WorkgroupId %c1 %c68 %v0_WorkgroupId + OpAtomicStore %out1_ptr_WorkgroupId %c1 %c68 %v1_WorkgroupId + OpAtomicStore %out2_ptr_WorkgroupId %c1 %c68 %v2_WorkgroupId %in_SubgroupSize = OpLoad %uint %gl_SubgroupSize - OpAtomicStore %out_SubgroupSize %c1 %c64 %in_SubgroupSize + OpAtomicStore %out_SubgroupSize %c1 %c68 %in_SubgroupSize %in0_ptr_WorkgroupSize = OpAccessChain %ptr_uint %gl_WorkgroupSize %c0 %in1_ptr_WorkgroupSize = OpAccessChain %ptr_uint %gl_WorkgroupSize %c1 @@ -145,9 +145,9 @@ %out0_ptr_WorkgroupSize = OpAccessChain %ptr_uint %out_WorkgroupSize %c0 %out1_ptr_WorkgroupSize = OpAccessChain %ptr_uint %out_WorkgroupSize %c1 %out2_ptr_WorkgroupSize = OpAccessChain %ptr_uint %out_WorkgroupSize %c2 - OpAtomicStore %out0_ptr_WorkgroupSize %c1 %c64 %v0_WorkgroupSize - OpAtomicStore %out1_ptr_WorkgroupSize %c1 %c64 %v1_WorkgroupSize - OpAtomicStore %out2_ptr_WorkgroupSize %c1 %c64 %v2_WorkgroupSize + OpAtomicStore %out0_ptr_WorkgroupSize %c1 %c68 %v0_WorkgroupSize + OpAtomicStore %out1_ptr_WorkgroupSize %c1 %c68 %v1_WorkgroupSize + OpAtomicStore %out2_ptr_WorkgroupSize %c1 %c68 %v2_WorkgroupSize OpReturn OpFunctionEnd diff --git a/dartagnan/src/test/resources/spirv/basic/builtin-all-321.spv.dis b/dartagnan/src/test/resources/spirv/basic/builtin-all-321.spv.dis index d8c037e0dd..a50cc0b495 100644 --- a/dartagnan/src/test/resources/spirv/basic/builtin-all-321.spv.dis +++ b/dartagnan/src/test/resources/spirv/basic/builtin-all-321.spv.dis @@ -55,7 +55,7 @@ %c0 = OpConstant %uint 0 %c1 = OpConstant %uint 1 %c2 = OpConstant %uint 2 - %c64 = OpConstant %uint 64 + %c68 = OpConstant %uint 68 %init = OpConstant %uint 999 %v3init = OpConstantComposite %v3uint %init %init %init @@ -83,7 +83,7 @@ %label = OpLabel %in_SubgroupLocalInvocationId = OpLoad %uint %gl_SubgroupLocalInvocationId - OpAtomicStore %out_SubgroupLocalInvocationId %c1 %c64 %in_SubgroupLocalInvocationId + OpAtomicStore %out_SubgroupLocalInvocationId %c1 %c68 %in_SubgroupLocalInvocationId %in0_ptr_LocalInvocationId = OpAccessChain %ptr_uint %gl_LocalInvocationId %c0 %in1_ptr_LocalInvocationId = OpAccessChain %ptr_uint %gl_LocalInvocationId %c1 @@ -94,12 +94,12 @@ %out0_ptr_LocalInvocationId = OpAccessChain %ptr_uint %out_LocalInvocationId %c0 %out1_ptr_LocalInvocationId = OpAccessChain %ptr_uint %out_LocalInvocationId %c1 %out2_ptr_LocalInvocationId = OpAccessChain %ptr_uint %out_LocalInvocationId %c2 - OpAtomicStore %out0_ptr_LocalInvocationId %c1 %c64 %v0_LocalInvocationId - OpAtomicStore %out1_ptr_LocalInvocationId %c1 %c64 %v1_LocalInvocationId - OpAtomicStore %out2_ptr_LocalInvocationId %c1 %c64 %v2_LocalInvocationId + OpAtomicStore %out0_ptr_LocalInvocationId %c1 %c68 %v0_LocalInvocationId + OpAtomicStore %out1_ptr_LocalInvocationId %c1 %c68 %v1_LocalInvocationId + OpAtomicStore %out2_ptr_LocalInvocationId %c1 %c68 %v2_LocalInvocationId %in_LocalInvocationIndex = OpLoad %uint %gl_LocalInvocationIndex - OpAtomicStore %out_LocalInvocationIndex %c1 %c64 %in_LocalInvocationIndex + OpAtomicStore %out_LocalInvocationIndex %c1 %c68 %in_LocalInvocationIndex %in0_ptr_GlobalInvocationId = OpAccessChain %ptr_uint %gl_GlobalInvocationId %c0 %in1_ptr_GlobalInvocationId = OpAccessChain %ptr_uint %gl_GlobalInvocationId %c1 @@ -110,15 +110,15 @@ %out0_ptr_GlobalInvocationId = OpAccessChain %ptr_uint %out_GlobalInvocationId %c0 %out1_ptr_GlobalInvocationId = OpAccessChain %ptr_uint %out_GlobalInvocationId %c1 %out2_ptr_GlobalInvocationId = OpAccessChain %ptr_uint %out_GlobalInvocationId %c2 - OpAtomicStore %out0_ptr_GlobalInvocationId %c1 %c64 %v0_GlobalInvocationId - OpAtomicStore %out1_ptr_GlobalInvocationId %c1 %c64 %v1_GlobalInvocationId - OpAtomicStore %out2_ptr_GlobalInvocationId %c1 %c64 %v2_GlobalInvocationId + OpAtomicStore %out0_ptr_GlobalInvocationId %c1 %c68 %v0_GlobalInvocationId + OpAtomicStore %out1_ptr_GlobalInvocationId %c1 %c68 %v1_GlobalInvocationId + OpAtomicStore %out2_ptr_GlobalInvocationId %c1 %c68 %v2_GlobalInvocationId %in_DeviceIndex = OpLoad %uint %gl_DeviceIndex - OpAtomicStore %out_DeviceIndex %c1 %c64 %in_DeviceIndex + OpAtomicStore %out_DeviceIndex %c1 %c68 %in_DeviceIndex %in_SubgroupId = OpLoad %uint %gl_SubgroupId - OpAtomicStore %out_SubgroupId %c1 %c64 %in_SubgroupId + OpAtomicStore %out_SubgroupId %c1 %c68 %in_SubgroupId %in0_ptr_WorkgroupId = OpAccessChain %ptr_uint %gl_WorkgroupId %c0 %in1_ptr_WorkgroupId = OpAccessChain %ptr_uint %gl_WorkgroupId %c1 @@ -129,12 +129,12 @@ %out0_ptr_WorkgroupId = OpAccessChain %ptr_uint %out_WorkgroupId %c0 %out1_ptr_WorkgroupId = OpAccessChain %ptr_uint %out_WorkgroupId %c1 %out2_ptr_WorkgroupId = OpAccessChain %ptr_uint %out_WorkgroupId %c2 - OpAtomicStore %out0_ptr_WorkgroupId %c1 %c64 %v0_WorkgroupId - OpAtomicStore %out1_ptr_WorkgroupId %c1 %c64 %v1_WorkgroupId - OpAtomicStore %out2_ptr_WorkgroupId %c1 %c64 %v2_WorkgroupId + OpAtomicStore %out0_ptr_WorkgroupId %c1 %c68 %v0_WorkgroupId + OpAtomicStore %out1_ptr_WorkgroupId %c1 %c68 %v1_WorkgroupId + OpAtomicStore %out2_ptr_WorkgroupId %c1 %c68 %v2_WorkgroupId %in_SubgroupSize = OpLoad %uint %gl_SubgroupSize - OpAtomicStore %out_SubgroupSize %c1 %c64 %in_SubgroupSize + OpAtomicStore %out_SubgroupSize %c1 %c68 %in_SubgroupSize %in0_ptr_WorkgroupSize = OpAccessChain %ptr_uint %gl_WorkgroupSize %c0 %in1_ptr_WorkgroupSize = OpAccessChain %ptr_uint %gl_WorkgroupSize %c1 @@ -145,9 +145,9 @@ %out0_ptr_WorkgroupSize = OpAccessChain %ptr_uint %out_WorkgroupSize %c0 %out1_ptr_WorkgroupSize = OpAccessChain %ptr_uint %out_WorkgroupSize %c1 %out2_ptr_WorkgroupSize = OpAccessChain %ptr_uint %out_WorkgroupSize %c2 - OpAtomicStore %out0_ptr_WorkgroupSize %c1 %c64 %v0_WorkgroupSize - OpAtomicStore %out1_ptr_WorkgroupSize %c1 %c64 %v1_WorkgroupSize - OpAtomicStore %out2_ptr_WorkgroupSize %c1 %c64 %v2_WorkgroupSize + OpAtomicStore %out0_ptr_WorkgroupSize %c1 %c68 %v0_WorkgroupSize + OpAtomicStore %out1_ptr_WorkgroupSize %c1 %c68 %v1_WorkgroupSize + OpAtomicStore %out2_ptr_WorkgroupSize %c1 %c68 %v2_WorkgroupSize OpReturn OpFunctionEnd diff --git a/dartagnan/src/test/resources/spirv/basic/builtin-constant.spv.dis b/dartagnan/src/test/resources/spirv/basic/builtin-constant.spv.dis index d11c108918..bb4192b410 100644 --- a/dartagnan/src/test/resources/spirv/basic/builtin-constant.spv.dis +++ b/dartagnan/src/test/resources/spirv/basic/builtin-constant.spv.dis @@ -19,7 +19,7 @@ %c0 = OpConstant %uint 0 %c1 = OpConstant %uint 1 %c2 = OpConstant %uint 2 - %c64 = OpConstant %uint 64 + %c68 = OpConstant %uint 68 %sc0 = OpSpecConstant %uint 0 %gl_WorkGroupSize = OpSpecConstantComposite %v3uint %sc0 %sc0 %sc0 %_ptr_Input_v3uint = OpTypePointer Input %v3uint @@ -37,8 +37,8 @@ %out0_ptr = OpAccessChain %ptr_uint %out %c0 %out1_ptr = OpAccessChain %ptr_uint %out %c1 %out2_ptr = OpAccessChain %ptr_uint %out %c2 - OpAtomicStore %out0_ptr %c1 %c64 %v0 - OpAtomicStore %out1_ptr %c1 %c64 %v1 - OpAtomicStore %out2_ptr %c1 %c64 %v2 + OpAtomicStore %out0_ptr %c1 %c68 %v0 + OpAtomicStore %out1_ptr %c1 %c68 %v1 + OpAtomicStore %out2_ptr %c1 %c68 %v2 OpReturn OpFunctionEnd diff --git a/dartagnan/src/test/resources/spirv/basic/builtin-default-config.spv.dis b/dartagnan/src/test/resources/spirv/basic/builtin-default-config.spv.dis index fbfb100f8d..71325b8813 100644 --- a/dartagnan/src/test/resources/spirv/basic/builtin-default-config.spv.dis +++ b/dartagnan/src/test/resources/spirv/basic/builtin-default-config.spv.dis @@ -18,7 +18,7 @@ %c0 = OpConstant %uint 0 %c1 = OpConstant %uint 1 %c2 = OpConstant %uint 2 - %c64 = OpConstant %uint 64 + %c68 = OpConstant %uint 68 %sc0 = OpSpecConstant %uint 0 %gl_WorkGroupSize = OpSpecConstantComposite %v3uint %sc0 %sc0 %sc0 %_ptr_Input_v3uint = OpTypePointer Input %v3uint @@ -36,8 +36,8 @@ %out0_ptr = OpAccessChain %ptr_uint %out %c0 %out1_ptr = OpAccessChain %ptr_uint %out %c1 %out2_ptr = OpAccessChain %ptr_uint %out %c2 - OpAtomicStore %out0_ptr %c1 %c64 %v0 - OpAtomicStore %out1_ptr %c1 %c64 %v1 - OpAtomicStore %out2_ptr %c1 %c64 %v2 + OpAtomicStore %out0_ptr %c1 %c68 %v0 + OpAtomicStore %out1_ptr %c1 %c68 %v1 + OpAtomicStore %out2_ptr %c1 %c68 %v2 OpReturn OpFunctionEnd diff --git a/dartagnan/src/test/resources/spirv/basic/builtin-variable.spv.dis b/dartagnan/src/test/resources/spirv/basic/builtin-variable.spv.dis index 6eb9124731..47fb9e86ed 100644 --- a/dartagnan/src/test/resources/spirv/basic/builtin-variable.spv.dis +++ b/dartagnan/src/test/resources/spirv/basic/builtin-variable.spv.dis @@ -19,7 +19,7 @@ %c0 = OpConstant %uint 0 %c1 = OpConstant %uint 1 %c2 = OpConstant %uint 2 - %c64 = OpConstant %uint 64 + %c68 = OpConstant %uint 68 %_ptr_Input_v3uint = OpTypePointer Input %v3uint %_ptr_Output_v3uint = OpTypePointer Output %v3uint %gl_WorkGroupSize = OpVariable %_ptr_Input_v3uint Input @@ -38,8 +38,8 @@ ; TODO: What is the storage class here? Should be mapped from Output - OpAtomicStore %out0_ptr %c1 %c64 %v0 - OpAtomicStore %out1_ptr %c1 %c64 %v1 - OpAtomicStore %out2_ptr %c1 %c64 %v2 + OpAtomicStore %out0_ptr %c1 %c68 %v0 + OpAtomicStore %out1_ptr %c1 %c68 %v1 + OpAtomicStore %out2_ptr %c1 %c68 %v2 OpReturn OpFunctionEnd diff --git a/dartagnan/src/test/resources/spirv/basic/rmw-extremum-false.spv.dis b/dartagnan/src/test/resources/spirv/basic/rmw-extremum-false.spv.dis index 29e6bf0e4e..f9844217b6 100644 --- a/dartagnan/src/test/resources/spirv/basic/rmw-extremum-false.spv.dis +++ b/dartagnan/src/test/resources/spirv/basic/rmw-extremum-false.spv.dis @@ -22,15 +22,15 @@ %c1 = OpConstant %int 1 %c2 = OpConstant %int 2 %c3 = OpConstant %int 3 - %c64 = OpConstant %int 64 + %c72 = OpConstant %int 72 %var0 = OpVariable %ptr_int Uniform %c2 %var1 = OpVariable %ptr_int Uniform %c2 %out_result = OpVariable %ptr_v2int Output %out_final = OpVariable %ptr_v2int Output %main = OpFunction %void None %func %label = OpLabel - %result0 = OpAtomicSMin %int %var0 %c1 %c64 %c3_neg - %result1 = OpAtomicSMax %int %var1 %c1 %c64 %c3_neg + %result0 = OpAtomicSMin %int %var0 %c1 %c72 %c3_neg + %result1 = OpAtomicSMax %int %var1 %c1 %c72 %c3_neg %final0 = OpLoad %int %var0 %final1 = OpLoad %int %var1 %ptr_res_0 = OpAccessChain %ptr_int %out_result %c0 diff --git a/dartagnan/src/test/resources/spirv/basic/rmw-extremum-true.spv.dis b/dartagnan/src/test/resources/spirv/basic/rmw-extremum-true.spv.dis index 69492c108e..ceb4d407f1 100644 --- a/dartagnan/src/test/resources/spirv/basic/rmw-extremum-true.spv.dis +++ b/dartagnan/src/test/resources/spirv/basic/rmw-extremum-true.spv.dis @@ -22,15 +22,15 @@ %c1 = OpConstant %int 1 %c2 = OpConstant %int 2 %c3 = OpConstant %int 3 - %c64 = OpConstant %int 64 + %c72 = OpConstant %int 72 %var0 = OpVariable %ptr_int Uniform %c2 %var1 = OpVariable %ptr_int Uniform %c2 %out_result = OpVariable %ptr_v2int Output %out_final = OpVariable %ptr_v2int Output %main = OpFunction %void None %func %label = OpLabel - %result0 = OpAtomicSMin %int %var0 %c1 %c64 %c3_neg - %result1 = OpAtomicSMax %int %var1 %c1 %c64 %c3_neg + %result0 = OpAtomicSMin %int %var0 %c1 %c72 %c3_neg + %result1 = OpAtomicSMax %int %var1 %c1 %c72 %c3_neg %final0 = OpLoad %int %var0 %final1 = OpLoad %int %var1 %ptr_res_0 = OpAccessChain %ptr_int %out_result %c0