Skip to content

Bugs Found

Jump to bottom
Sandeep Dasgupta edited this page Apr 13, 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.

Self Goal

  • roundss_xmm_m32_imm8 
      stoke_debug_circuit  --strata_path ../../circuits/ --opc roundss_xmm_m32_imm8  --smtlib_format
    Gives a segfault while converting the bv formula to smtlib format. The reason is 
     %ymm1  : %ymm1[255:128] ∘ (%ymm1[127:64] ∘ cvt_single_to_int32_rm(TMP_BV_32_0[63:0], 0x0₈))
    Note: TMP_BV_32_0[63:0] which is wrong as its extracting 64 out of 32 bit bv. which is an error in my implementation of the semantics.

Intel Manual Bug

https://software.intel.com/en-us/forums/intel-isa-extensions/topic/773342

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