Skip to content

Bugs Found

Jump to bottom
Sandeep Dasgupta edited this page Apr 3, 2018 · 31 revisions

Setup

Validating the semantics of strata unsupported instruction using testing with strata's final testsuite. The ones supported both by strata and stoke are already proved eq and fixes are made.

Intel Manual Bug

vpsravd %xmm3, %xmm2, %xmm1

Semantics

Arithmatic right shift of 32 chunks of '%xmm2' by 32 chunks of %xmm3 and store in corresponding 32 chunks in '%xm1'

Semantics of vpsravd %xmm3, %xmm2, %xmm1 as per Intel Manual

%ymm1  : 0x0₁₂₈ ∘ ((%ymm2[127:96] sign_shift_right (0x0₂₇ ∘ %ymm3[100:96])) ∘ 
                  ((%ymm2[95:64] sign_shift_right %ymm3[95:64]) ∘ 
                  ((%ymm2[63:32] sign_shift_right %ymm3[63:32]) ∘ 
                  (%ymm2[31:0] sign_shift_right %ymm3[31:0]))))

Note that the first term ((%ymm2[127:96] sign_shift_right (0x0₂₇ ∘ %ymm3[100:96])) has only 5 bits selected from '%ymm3' But the actual execution behaviour expects 32 bits from %ymm3 : ((%ymm2[127:96] sign_shift_right 0x0₂₇ ∘ %ymm3[127:96])

Input (hex)

%ymm2: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 - 80 00 00 00 - 00 00 00 00 - 00 00 00 00 - 00 00 00 00

%ymm3: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 - 00 00 00 20 - 00 00 00 00 - 00 00 00 00 - 00 00 00 00

As per manual

  0x0₁₂₈ ∘ ((0x80000000₃₂ sign_shift_right 0x0₃₂) ∘ ((0x0₃₂ sign_shift_right 0x0₃₂) ∘ ((0x0₃₂ sign_shift_right 0x0₃₂) ∘ (0x0₃₂ sign_shift_right 0x0₃₂))))

Actual Hardware

     0x0₆₄ ∘ 0x0₆₄ ∘ 0xffffffff00000000₆₄ ∘ 0x0₆₄

Stroke Bugs reported

Definition of vaddsubpd/ps

https://github.com/StanfordPL/stoke/blob/2dc61f6f55a9991c25c471f5e6ffe5ff45962afb/src/validator/handlers/packed_handler.h#L54 https://github.com/StanfordPL/stoke/blob/2dc61f6f55a9991c25c471f5e6ffe5ff45962afb/src/validator/handlers/packed_handler.h#L60

%ymm1    00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
%ymm2    00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00
%ymm3    00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 01

Sandbox and validator do not agree for 'vaddsubpd %ymm3, %ymm2, %ymm1' (opcode vaddsubpd_ymm_ymm_ymm)
  states do not agree for '%ymm1':
    validator: 0x0₆₄ ∘ 0x0₆₄ ∘ (sub_double(0x0₆₄, 0x1₆₄) ∘ 0x0₆₄)
    sandbox:   0x0₆₄ ∘ 0x0₆₄ ∘ 0x0₆₄ ∘ 0x8000000000000001₆₄

Definition of cvtsi2ssl/cvtsi2ssq/cvtsi2sdl/cvtsi2sdq

https://github.com/StanfordPL/stoke/blob/2dc61f6f55a9991c25c471f5e6ffe5ff45962afb/src/validator/handlers/packed_handler.h#L142 DIfferent createment for cvtsi2* and vcvtsi2* cases. So cannot be accomodated in packed handler, but implemented in simple handler.

cvtsi2ssl/cvtsi2ssq are implemented by srata as well, but the stratified formula s NOT equivalent with the stoke's formula.

Clone this wiki locally