search

mc-imperial / spirv-control-flow

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

MESA - OpPhi Vulkan CTS: Verifier failed: 0 == 20, at index 7 #21

Open Jack-Clark opened 2 years ago

Jack-Clark commented 2 years ago

When running the amber code below on Mesa 22.1.0 (commit 01113c2) I get the error:

tests/op_phi_vulkan_cts/op_phi_vulkan_cts/s288/test_0_9012217633092994101.amber: Line 441: Verifier failed: 0 == 20, at index 7

Summary of Failures:
  tests/op_phi_vulkan_cts/op_phi_vulkan_cts/s288/test_0_9012217633092994101.amber

Summary: 0 pass, 1 fail

I don't get this error on other drivers, so it looks like this could be a new output mismatch bug!

Amber file:

#!amber

SHADER compute compute_shader SPIRV-ASM

; Follow the path:
; 8 -> 9 -> <12> -> 13 -> 15 -> <18> -> <21> -> edge_0 -> 20 -> <18> -> <21> -> edge_0 -> 20 -> <18> -> <21> -> edge_0 -> 20 -> <18> -> <19> -> <16> -> 29 -> <10> -> 31 -> 30
;
; 6 CFG nodes have OpBranchConditional or OpSwitch as their terminators (denoted <n>): 10, 12, 16, 18, 19 and 21.
;
; To follow this path, we need to make these decisions each time we reach 10, 12, 16, 18, 19 or 21.
; This path was generated with the seed 9012217633092994101 and has length 21.
;
; We equip the shader with 6+1 storage buffers:
; - An input storage buffer with the directions for each node 10, 12, 16, 18, 19 or 21
; - An output storage buffer that records the blocks that are executed

; 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" %local_invocation_idx_var %workgroup_id_var
               OpExecutionMode %7 LocalSize 1 1 1

               ; Below, we declare various types and variables for storage buffers.
               ; These decorations tell SPIR-V that the types and variables relate to storage buffers

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

               OpDecorate %size_3_struct_type BufferBlock
               OpMemberDecorate %size_3_struct_type 0 Offset 0
               OpDecorate %size_3_array_type ArrayStride 4

               OpDecorate %size_4_struct_type BufferBlock
               OpMemberDecorate %size_4_struct_type 0 Offset 0
               OpDecorate %size_4_array_type ArrayStride 4

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

               OpDecorate %directions_10_variable DescriptorSet 0
               OpDecorate %directions_10_variable Binding 0

               OpDecorate %directions_12_variable DescriptorSet 0
               OpDecorate %directions_12_variable Binding 1

               OpDecorate %directions_16_variable DescriptorSet 0
               OpDecorate %directions_16_variable Binding 2

               OpDecorate %directions_18_variable DescriptorSet 0
               OpDecorate %directions_18_variable Binding 3

               OpDecorate %directions_19_variable DescriptorSet 0
               OpDecorate %directions_19_variable Binding 4

               OpDecorate %directions_21_variable DescriptorSet 0
               OpDecorate %directions_21_variable Binding 5

               OpDecorate %output_variable DescriptorSet 0
               OpDecorate %output_variable Binding 6

               OpDecorate %local_invocation_idx_var BuiltIn LocalInvocationIndex
               OpDecorate %workgroup_id_var BuiltIn WorkgroupId

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

               %dummy_val = OpConstant %4 666
               %constant_0 = OpConstant %4 0
               %constant_1 = OpConstant %4 1
               %constant_2 = OpConstant %4 2
               %constant_3 = OpConstant %4 3
               %constant_4 = OpConstant %4 4
               %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
               %constant_21 = OpConstant %4 21
               %constant_22 = OpConstant %4 22
               %constant_23 = OpConstant %4 23
               %constant_24 = OpConstant %4 24
               %constant_25 = OpConstant %4 25
               %constant_26 = OpConstant %4 26
               %constant_27 = OpConstant %4 27
               %constant_28 = OpConstant %4 28
               %constant_29 = OpConstant %4 29
               %constant_30 = OpConstant %4 30
               %constant_31 = OpConstant %4 31

               ; Declaration of storage buffers for the 6 directions and the output

               %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_16_variable = OpVariable %size_1_pointer_type Uniform
               %directions_10_variable = OpVariable %size_1_pointer_type Uniform
               %directions_19_variable = OpVariable %size_1_pointer_type Uniform
               %directions_12_variable = OpVariable %size_1_pointer_type Uniform

               %size_3_array_type = OpTypeArray %4 %constant_3
               %size_3_struct_type = OpTypeStruct %size_3_array_type
               %size_3_pointer_type = OpTypePointer Uniform %size_3_struct_type
               %directions_21_variable = OpVariable %size_3_pointer_type Uniform

               %size_4_array_type = OpTypeArray %4 %constant_4
               %size_4_struct_type = OpTypeStruct %size_4_array_type
               %size_4_pointer_type = OpTypePointer Uniform %size_4_struct_type
               %directions_18_variable = OpVariable %size_4_pointer_type Uniform

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

               ; Pointer type for declaring local variables of int type
               %local_int_ptr = OpTypePointer Function %4

               ; Pointer type for integer data in a storage buffer
               %storage_buffer_int_ptr = OpTypePointer Uniform %4

               %input_int_ptr = OpTypePointer Input %4
               %local_invocation_idx_var = OpVariable %input_int_ptr Input

               %vec_3_input = OpTypeVector %4 3
               %workgroup_ptr = OpTypePointer Input %vec_3_input 
               %workgroup_id_var = OpVariable %workgroup_ptr Input

          %7 = OpFunction %1 None %2

          %8 = OpLabel ; validCFG/Block$14
               %output_index = OpVariable %local_int_ptr Function %constant_0
               %directions_10_index = OpVariable %local_int_ptr Function %constant_0
               %directions_12_index = OpVariable %local_int_ptr Function %constant_0
               %directions_16_index = OpVariable %local_int_ptr Function %constant_0
               %directions_18_index = OpVariable %local_int_ptr Function %constant_0
               %directions_19_index = OpVariable %local_int_ptr Function %constant_0
               %directions_21_index = OpVariable %local_int_ptr Function %constant_0

               %local_invocation_idx = OpLoad %4 %local_invocation_idx_var
               %x_wg_dim_ptr = OpAccessChain %input_int_ptr %workgroup_id_var %constant_0
               %y_wg_dim_ptr = OpAccessChain %input_int_ptr %workgroup_id_var %constant_1
               %z_wg_dim_ptr = OpAccessChain %input_int_ptr %workgroup_id_var %constant_2
               %x_wg_dim = OpLoad %4 %x_wg_dim_ptr
               %y_wg_dim = OpLoad %4 %y_wg_dim_ptr
               %z_wg_dim = OpLoad %4 %z_wg_dim_ptr
               %z_idx_component = OpIMul %4 %z_wg_dim %constant_1
               %y_idx_component = OpIMul %4 %y_wg_dim %constant_1
               %yz_idx_component = OpIAdd %4 %y_idx_component %z_idx_component
               %workgroup_idx = OpIAdd %4 %yz_idx_component %x_wg_dim

               %local_directions_10_offset = OpIMul %4 %local_invocation_idx %constant_1
               %local_directions_12_offset = OpIMul %4 %local_invocation_idx %constant_1
               %local_directions_16_offset = OpIMul %4 %local_invocation_idx %constant_1
               %local_directions_18_offset = OpIMul %4 %local_invocation_idx %constant_4
               %local_directions_19_offset = OpIMul %4 %local_invocation_idx %constant_1
               %local_directions_21_offset = OpIMul %4 %local_invocation_idx %constant_3

               %global_directions_10_offset = OpIMul %4 %workgroup_idx %constant_1
               %global_directions_12_offset = OpIMul %4 %workgroup_idx %constant_1
               %global_directions_16_offset = OpIMul %4 %workgroup_idx %constant_1
               %global_directions_18_offset = OpIMul %4 %workgroup_idx %constant_4
               %global_directions_19_offset = OpIMul %4 %workgroup_idx %constant_1
               %global_directions_21_offset = OpIMul %4 %workgroup_idx %constant_3

               %directions_10_offset = OpIAdd %4 %global_directions_10_offset %local_directions_10_offset
               %directions_12_offset = OpIAdd %4 %global_directions_12_offset %local_directions_12_offset
               %directions_16_offset = OpIAdd %4 %global_directions_16_offset %local_directions_16_offset
               %directions_18_offset = OpIAdd %4 %global_directions_18_offset %local_directions_18_offset
               %directions_19_offset = OpIAdd %4 %global_directions_19_offset %local_directions_19_offset
               %directions_21_offset = OpIAdd %4 %global_directions_21_offset %local_directions_21_offset
               %local_output_offset = OpIMul %4 %local_invocation_idx %constant_22
               %global_output_offset = OpIMul %4 %workgroup_idx %constant_22
               %output_offset = OpIAdd %4 %global_output_offset %local_output_offset

               OpStore %directions_10_index %directions_10_offset
               OpStore %directions_12_index %directions_12_offset
               OpStore %directions_16_index %directions_16_offset
               OpStore %directions_18_index %directions_18_offset
               OpStore %directions_19_index %directions_19_offset
               OpStore %directions_21_index %directions_21_offset
               OpStore %output_index %output_offset

   %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
               OpBranch %9

          %9 = OpLabel ; validCFG/LoopHeader$2
   %temp_9_0 = OpPhi %4 %dummy_val %11 %temp_8_2 %8
   %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
   %9_target_12 = OpLoad %4 %directions_12_index
               OpLoopMerge %10 %11 None
               OpBranch %12

         %12 = OpLabel ; validCFG/SelectionHeader$1
  %temp_12_0 = OpPhi %4 %temp_9_2 %9
  %temp_12_3 = OpPhi %4 %9_target_12 %9
  %temp_12_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_12_0
               OpStore %temp_12_1 %constant_12
  %temp_12_2 = OpIAdd %4 %temp_12_0 %constant_1
  %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
               OpSelectionMerge %13 None
               OpBranchConditional %temp_12_6 %14 %13

         %11 = OpLabel ; validCFG/Block$5
               OpBranch %9

         %14 = OpLabel ; validCFG/Block$2
               OpBranch %10

         %13 = OpLabel ; validCFG/Block$1
  %temp_13_0 = OpPhi %4 %temp_12_2 %12
  %temp_13_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_13_0
               OpStore %temp_13_1 %constant_13
  %temp_13_2 = OpIAdd %4 %temp_13_0 %constant_1
               OpBranch %15

         %15 = OpLabel ; validCFG/LoopHeader$0
  %temp_15_0 = OpPhi %4 %dummy_val %17 %temp_13_2 %13
  %temp_15_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_15_0
               OpStore %temp_15_1 %constant_15
  %temp_15_2 = OpIAdd %4 %temp_15_0 %constant_1
  %15_target_18 = OpLoad %4 %directions_18_index
               OpLoopMerge %16 %17 None
               OpBranch %18

         %18 = OpLabel ; validCFG/LoopHeader$1
  %temp_18_0 = OpPhi %4 %temp_20_2 %20 %temp_15_2 %15
  %temp_18_3 = OpPhi %4 %20_target_18 %20 %15_target_18 %15
  %temp_18_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_18_0
               OpStore %temp_18_1 %constant_18
  %temp_18_2 = OpIAdd %4 %temp_18_0 %constant_1
  %temp_18_4 = OpAccessChain %storage_buffer_int_ptr %directions_18_variable %constant_0 %temp_18_3
  %temp_18_5 = OpLoad %4 %temp_18_4
  %temp_18_6 = OpIEqual %3 %temp_18_5 %constant_1
  %temp_18_7 = OpIAdd %4 %temp_18_3 %constant_1
               OpStore %directions_18_index %temp_18_7
  %18_target_19 = OpLoad %4 %directions_19_index
  %18_target_21 = OpLoad %4 %directions_21_index
               OpLoopMerge %19 %20 None
               OpBranchConditional %temp_18_6 %21 %19

         %17 = OpLabel ; validCFG/Block$8
               OpBranch %15

         %21 = OpLabel ; validCFG/SelectionHeader$0
  %temp_21_0 = OpPhi %4 %temp_18_2 %18
  %temp_21_3 = OpPhi %4 %18_target_21 %18
  %temp_21_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_21_0
               OpStore %temp_21_1 %constant_21
  %temp_21_2 = OpIAdd %4 %temp_21_0 %constant_1
  %temp_21_4 = OpAccessChain %storage_buffer_int_ptr %directions_21_variable %constant_0 %temp_21_3
  %temp_21_5 = OpLoad %4 %temp_21_4
  %temp_21_7 = OpIAdd %4 %temp_21_3 %constant_1
               OpStore %directions_21_index %temp_21_7
               OpSelectionMerge %22 None
               OpSwitch %temp_21_5 %20 1 %23 2 %24

         %23 = OpLabel ; validCFG/Block$12
               OpBranch %24

         %22 = OpLabel ; validCFG/Block$0
               OpBranch %20

         %24 = OpLabel ; validCFG/SelectionHeader$5
               OpSelectionMerge %25 None
               OpBranchConditional %5 %26 %25

         %26 = OpLabel ; validCFG/Block$11
               OpBranch %19

         %25 = OpLabel ; validCFG/Block$10
               OpBranch %20

         %19 = OpLabel ; validCFG/SelectionHeader$4
  %temp_19_0 = OpPhi %4 %dummy_val %26 %temp_18_2 %18
  %temp_19_3 = OpPhi %4 %dummy_val %26 %18_target_19 %18
  %temp_19_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_19_0
               OpStore %temp_19_1 %constant_19
  %temp_19_2 = OpIAdd %4 %temp_19_0 %constant_1
  %temp_19_4 = OpAccessChain %storage_buffer_int_ptr %directions_19_variable %constant_0 %temp_19_3
  %temp_19_5 = OpLoad %4 %temp_19_4
  %temp_19_6 = OpIEqual %3 %temp_19_5 %constant_1
  %temp_19_7 = OpIAdd %4 %temp_19_3 %constant_1
               OpStore %directions_19_index %temp_19_7
  %19_target_16 = OpLoad %4 %directions_16_index
               OpSelectionMerge %27 None
               OpBranchConditional %temp_19_6 %16 %27

         %20 = OpLabel ; validCFG/Block$13
  %temp_20_0 = OpPhi %4 %dummy_val %22 %dummy_val %25 %temp_21_2 %21
  %temp_20_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_20_0
               OpStore %temp_20_1 %constant_20
  %temp_20_2 = OpIAdd %4 %temp_20_0 %constant_1
  %20_target_18 = OpLoad %4 %directions_18_index
               OpBranch %18

         %27 = OpLabel ; validCFG/Block$9
               OpBranch %16

         %16 = OpLabel ; validCFG/SelectionHeader$3
  %temp_16_0 = OpPhi %4 %temp_19_2 %19 %dummy_val %27
  %temp_16_3 = OpPhi %4 %19_target_16 %19 %dummy_val %27
  %temp_16_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_16_0
               OpStore %temp_16_1 %constant_16
  %temp_16_2 = OpIAdd %4 %temp_16_0 %constant_1
  %temp_16_4 = OpAccessChain %storage_buffer_int_ptr %directions_16_variable %constant_0 %temp_16_3
  %temp_16_5 = OpLoad %4 %temp_16_4
  %temp_16_6 = OpIEqual %3 %temp_16_5 %constant_1
  %temp_16_7 = OpIAdd %4 %temp_16_3 %constant_1
               OpStore %directions_16_index %temp_16_7
               OpSelectionMerge %28 None
               OpBranchConditional %temp_16_6 %29 %28

         %29 = OpLabel ; validCFG/Block$7
  %temp_29_0 = OpPhi %4 %temp_16_2 %16
  %temp_29_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_29_0
               OpStore %temp_29_1 %constant_29
  %temp_29_2 = OpIAdd %4 %temp_29_0 %constant_1
  %29_target_10 = OpLoad %4 %directions_10_index
               OpBranch %10

         %28 = OpLabel ; validCFG/Block$6
               OpBranch %10

         %10 = OpLabel ; validCFG/SelectionHeader$2
  %temp_10_0 = OpPhi %4 %temp_29_2 %29 %dummy_val %28 %dummy_val %14
  %temp_10_3 = OpPhi %4 %29_target_10 %29 %dummy_val %28 %dummy_val %14
  %temp_10_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_10_0
               OpStore %temp_10_1 %constant_10
  %temp_10_2 = OpIAdd %4 %temp_10_0 %constant_1
  %temp_10_4 = OpAccessChain %storage_buffer_int_ptr %directions_10_variable %constant_0 %temp_10_3
  %temp_10_5 = OpLoad %4 %temp_10_4
  %temp_10_6 = OpIEqual %3 %temp_10_5 %constant_1
  %temp_10_7 = OpIAdd %4 %temp_10_3 %constant_1
               OpStore %directions_10_index %temp_10_7
               OpSelectionMerge %30 None
               OpBranchConditional %temp_10_6 %31 %30

         %31 = OpLabel ; validCFG/Block$4
  %temp_31_0 = OpPhi %4 %temp_10_2 %10
  %temp_31_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_31_0
               OpStore %temp_31_1 %constant_31
  %temp_31_2 = OpIAdd %4 %temp_31_0 %constant_1
               OpBranch %30

         %30 = OpLabel ; validCFG/Block$3
  %temp_30_0 = OpPhi %4 %temp_31_2 %31 %temp_10_2 %10
  %temp_30_1 = OpAccessChain %storage_buffer_int_ptr %output_variable %constant_0 %temp_30_0
               OpStore %temp_30_1 %constant_30
  %temp_30_2 = OpIAdd %4 %temp_30_0 %constant_2
               OpReturn

               OpFunctionEnd

 END

 BUFFER directions_12 DATA_TYPE uint32 STD430 DATA 0 END
 BUFFER directions_18 DATA_TYPE uint32 STD430 DATA 1 1 1 0 END
 BUFFER directions_21 DATA_TYPE uint32 STD430 DATA 0 0 0 END
 BUFFER directions_19 DATA_TYPE uint32 STD430 DATA 1 END
 BUFFER directions_16 DATA_TYPE uint32 STD430 DATA 1 END
 BUFFER directions_10 DATA_TYPE uint32 STD430 DATA 1 END

 BUFFER output DATA_TYPE uint32 STD430 SIZE 22 FILL 0

 PIPELINE compute pipeline
   ATTACH compute_shader

   BIND BUFFER directions_12 AS storage DESCRIPTOR_SET 0 BINDING 1
   BIND BUFFER directions_18 AS storage DESCRIPTOR_SET 0 BINDING 3
   BIND BUFFER directions_21 AS storage DESCRIPTOR_SET 0 BINDING 5
   BIND BUFFER directions_19 AS storage DESCRIPTOR_SET 0 BINDING 4
   BIND BUFFER directions_16 AS storage DESCRIPTOR_SET 0 BINDING 2
   BIND BUFFER directions_10 AS storage DESCRIPTOR_SET 0 BINDING 0

   BIND BUFFER output AS storage DESCRIPTOR_SET 0 BINDING 6
 END

 RUN pipeline 1 1 1

 EXPECT directions_12 IDX 0 EQ 0
 EXPECT directions_18 IDX 0 EQ 1 1 1 0
 EXPECT directions_21 IDX 0 EQ 0 0 0
 EXPECT directions_19 IDX 0 EQ 1
 EXPECT directions_16 IDX 0 EQ 1
 EXPECT directions_10 IDX 0 EQ 1
 EXPECT output IDX 0 EQ 8 9 12 13 15 18 21 20 18 21 20 18 21 20 18 19 16 29 10 31 30 0