mc-imperial / spirv-control-flow

Formal modelling of SPIR-V control flow using Alloy
Apache License 2.0
2 stars 0 forks source link

SwiftShader: Verifier failed: 0 == 8, at index 0 #10

Open Jack-Clark opened 2 years ago

Jack-Clark commented 2 years ago

Executing amber -t spv1.3 -v 1.1 reduced-oracle-output.amber gives fails with reduced-output-oracle.amber: Line 161: Verifier failed: 0 == 8, at index 0.

The CFG is quite complicated but the path is simple. @vili-1 could you check that this is valid? It also has a few Block$X blocks that look like they should be SRB$X blocks - do you think they are from the known issue? Here is the reduced amber:

#!amber

SHADER compute compute_shader SPIRV-ASM

; Follow the path:
; 8 -> <9> -> <12> -> 10
;
; 2 CFG nodes have OpBranchConditional or OpSwitch as their terminators (denoted <n>): 9 and 12.
;
; To follow this path, we need to make these decisions each time we reach 9 or 12.
; This path was generated with the seed 6256442267000680237 and has length 4.

; SPIR-V
; Version: 1.3
; Generator: Khronos Glslang Reference Front End; 8
; Bound: 15
; Schema: 0

               OpCapability Shader
               OpMemoryModel Logical GLSL450
               OpEntryPoint GLCompute %7 "main"
               OpExecutionMode %7 LocalSize 1 1 1

               OpDecorate %size_1_struct_type BufferBlock
               OpMemberDecorate %size_1_struct_type 0 Offset 0
               OpDecorate %size_1_array_type ArrayStride 4

               OpDecorate %output_struct_type BufferBlock
               OpMemberDecorate %output_struct_type 0 Offset 0
               OpDecorate %output_array_type ArrayStride 4

               OpDecorate %directions_12_variable DescriptorSet 0
               OpDecorate %directions_12_variable Binding 1

               OpDecorate %output_variable DescriptorSet 0
               OpDecorate %output_variable Binding 2

          %1 = OpTypeVoid
          %2 = OpTypeFunction %1
          %3 = OpTypeBool
          %4 = OpTypeInt 32 0
          %5 = OpConstantTrue %3
          %6 = OpConstant %4 0

               %constant_0 = OpConstant %4 0
               %constant_1 = OpConstant %4 1
               %constant_2 = OpConstant %4 2
               %constant_8 = OpConstant %4 8
               %constant_9 = OpConstant %4 9
               %constant_10 = OpConstant %4 10
               %constant_11 = OpConstant %4 11
               %constant_12 = OpConstant %4 12
               %constant_13 = OpConstant %4 13
               %constant_14 = OpConstant %4 14
               %constant_15 = OpConstant %4 15
               %constant_16 = OpConstant %4 16
               %constant_17 = OpConstant %4 17
               %constant_18 = OpConstant %4 18
               %constant_19 = OpConstant %4 19
               %constant_20 = OpConstant %4 20

               %size_1_array_type = OpTypeArray %4 %constant_1
               %size_1_struct_type = OpTypeStruct %size_1_array_type
               %size_1_pointer_type = OpTypePointer Uniform %size_1_struct_type
               %directions_12_variable = OpVariable %size_1_pointer_type Uniform

               %output_array_type = OpTypeArray %4 %constant_2
               %output_struct_type = OpTypeStruct %output_array_type
               %output_pointer_type = OpTypePointer Uniform %output_struct_type
               %output_variable = OpVariable %output_pointer_type Uniform

               %local_int_ptr = OpTypePointer Function %4
               %storage_buffer_int_ptr = OpTypePointer Uniform %4

          %7 = OpFunction %1 None %2

          %8 = OpLabel ; validCFG/StructurallyReachableBlock$6
               %output_index = OpVariable %local_int_ptr Function %constant_0
               %directions_12_index = OpVariable %local_int_ptr Function %constant_0

   %temp_8_0 = OpLoad %4 %output_index
   %temp_8_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_8_0
               OpStore %temp_8_1 %constant_8
   %temp_8_2 = OpIAdd %4 %temp_8_0 %constant_1
               OpStore %output_index %temp_8_2
               OpBranch %9

          %9 = OpLabel ; validCFG/LoopHeader$1
   %temp_9_0 = OpLoad %4 %output_index
   %temp_9_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_9_0
               OpStore %temp_9_1 %constant_9
   %temp_9_2 = OpIAdd %4 %temp_9_0 %constant_1
               OpStore %output_index %temp_9_2
               OpLoopMerge %10 %11 None
               OpBranchConditional %5 %12 %11

         %12 = OpLabel ; validCFG/Block$1
  %temp_12_3 = OpLoad %4 %directions_12_index
  %temp_12_4 = OpAccessChain %storage_buffer_int_ptr %directions_12_variable %constant_0 %temp_12_3
  %temp_12_5 = OpLoad %4 %temp_12_4
  %temp_12_6 = OpIEqual %3 %temp_12_5 %constant_1
  %temp_12_7 = OpIAdd %4 %temp_12_3 %constant_1
               OpStore %directions_12_index %temp_12_7
               OpBranchConditional %temp_12_6 %10 %11

         %11 = OpLabel ; validCFG/StructurallyReachableBlock$2
               OpBranch %13

         %13 = OpLabel ; validCFG/LoopHeader$0
               OpLoopMerge %14 %15 None
               OpBranchConditional %5 %16 %15

         %16 = OpLabel ; validCFG/SelectionHeader$0
               OpSelectionMerge %17 None
               OpBranchConditional %5 %18 %14

         %18 = OpLabel ; validCFG/Block$0
               OpBranchConditional %5 %15 %14

         %17 = OpLabel ; validCFG/StructurallyReachableBlock$1
               OpBranchConditional %5 %19 %15

         %14 = OpLabel ; validCFG/StructurallyReachableBlock$0
               OpBranchConditional %5 %9 %10

         %19 = OpLabel ; validCFG/StructurallyReachableBlock$5
               OpBranch %15

         %10 = OpLabel ; validCFG/StructurallyReachableBlock$4
               OpReturn

         %15 = OpLabel ; validCFG/StructurallyReachableBlock$3
               OpBranch %20

         %20 = OpLabel ; validCFG/Block$2
               OpBranch %13

               OpFunctionEnd

 END

 BUFFER directions_12 DATA_TYPE uint32 STD430 DATA 1 END

 BUFFER output DATA_TYPE uint32 STD430 SIZE 4 FILL 0

 PIPELINE compute pipeline
   ATTACH compute_shader

   BIND BUFFER directions_12 AS storage DESCRIPTOR_SET 0 BINDING 1

   BIND BUFFER output AS storage DESCRIPTOR_SET 0 BINDING 2
 END

 RUN pipeline 1 1 1

 EXPECT directions_12 IDX 0 EQ 1
 EXPECT output IDX 0 EQ 8 9
vili-1 commented 2 years ago

Yes this is valid. And I executed amber without any problem.

Summary: 1 pass, 0 fail

reducedOracleOutput

Jack-Clark commented 2 years ago

Thanks for confirming this @vili-1. Did you use SwiftShader or moltenVK when running amber?

vili-1 commented 2 years ago

As I said in issue #9 I'm using MoltenVK

vili-1 commented 2 years ago

With SwiftShader now I do get an error only when path 8 -> 9 -> 12 -> 10 is exercised.

 EXPECT output IDX 0 EQ 8 9 12 10

temp.amber: Line 213: Verifier failed: 0 == 8, at index 0

Summary of Failures:
  temp.amber

Summary: 0 pass, 1 fail
vili-1 commented 2 years ago

I ran all the 1st test set of fleshed examples with MolteVk and got plenty of similar errors, i.e., Verifier failed: X == Y, at index Z