Bugs Found

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.

Master Stoke

• Stoke tried to generalize vcvtpd2dq_xmm_m256 from simple handler's vcvtpd2dq_xmm_ymm and comes up with wrong formula as the strata's generalization is buggy. It needs to be generated alike simple_handler's ``vcvtpd2dq_xmm_ymm`. To reproduce:

sf   --smtlib_format   --opc vcvtpd2dq_xmm_m256

Self Goal

• For the followings, using the stoke formula instead of strata formula. It gives 2 benefits: simple formula and correctness over af flags. Also testing becomes much more easier as build strata formula is much costlier.

cmpb_m8_imm8 cmpb_m8_rh cmpb_m8_r8 cmpb_rh_m8 cmpb_r8_m8 cmpl_m32_imm32 cmpl_m32_imm8 cmpl_m32_r32 cmpq_m64_imm32 cmpl_r32_m32 cmpq_m64_imm8 cmpq_m64_r64 cmpq_r64_m64 cmpw_m16_imm16 cmpw_m16_imm8 cmpw_m16_r16 cmpw_r16_m16 decb_m8 decl_m32 decq_m64 decw_m16 incw_m16 negb_m8 negl_m32 negw_m16 negq_m64 sbbb_m8_imm8 sbbb_m8_rh sbbb_m8_r8 sbbl_m32_imm32 sbbl_m32_imm8 sbbb_rh_m8 sbbb_r8_m8 sbbq_m64_imm8 sbbq_m64_imm32 sbbl_m32_r32 sbbw_m16_imm16 sbbw_m16_imm8 sbbl_r32_m32 sbbw_m16_r16 sbbw_r16_m16 sbbq_m64_r64 sbbq_r64_m64 subb_m8_imm8 subb_m8_r8 subb_m8_rh subb_r8_m8 subb_rh_m8 subl_m32_imm32 subl_m32_imm8 subl_m32_r32 subl_r32_m32 subq_m64_imm8 subq_m64_imm32 subq_m64_r64 subq_r64_m64 subw_m16_imm16 subw_m16_imm8 subw_m16_r16 subw_r16_m16

• For the followings, we got not eqiv formulas for cf between strata_handler and simple_handler.

  btq_m64_imm8::cf
  btl_m32_imm8::cf
  btl_m32_r32::cf
  btq_m64_r64::cf
  

  In this case, The difference does not mean that either of them or both are wrong as we have tested bot the formulas and they seem to be true. The diff is sue to that fact the symbolic variable for memory has been drawn from different addresses and have different widths For the time being we are accepting the formula from simple handler. Please remember to generate the generic formula using keep_imm_symbolic flag as the address part will depend on the imm operand. To recreate, do this after allowing the instr to use either of strata or simple handler.

   sc --strata_path ../../circuits/  --smtlib_format   --code "btq \$0xa, (%rbx)" 
   sc   --smtlib_format   --code "btq \$0xa, (%rbx)" 
  

• xchg_m16_r16 /xchg_m32_r32 /xchg_m64_r64 /xchg_m8_r8 /xchg_m8_rh /xchg_r16_m16 /xchg_r32_m32 /xchg_r64_m64 /xchg_r8_m8 /xchg_rh_m8

  For the instruction xchgb %al, (%rax) We got the formula out of generalization

  %rax   : %rax[63:8] ∘ TMP_BV_8_0
  Information about memory reads:
    Value TMP_BV_8_0 (1 bytes)
    was read at address %rax.
  
  Information about memory writes:
    Address %rax[63:8] ∘ TMP_BV_8_0 was updated to
    %rax[7:0] (1 bytes).
  

  which is wrong as the address is messed up. This error is very particular to memory operands AND with same registers. For register variants OR with different operands this will not be manifested. The correct solution depends on the order of updates which is different for memory and non memory cases and is implemented by master stoke.

    add_opcode_str({"xchgb", "xchgw", "xchgl", "xchgq"},
    [this] (Operand dst, Operand src, SymBitVector a, SymBitVector b, SymState& ss) {
    if (src.is_typical_memory()) {
      ss.set(src, a);
      ss.set(dst, b);
    } else {
      ss.set(dst, b);
      ss.set(src, a);
    }
    });
  

• movss_xmm_m32/movsd_xmm_m64 Cannot be generalized as the generalization is wrong. Register variant movsd_xmm_xmm has the following semantics:

   %ymm1  : %ymm1[255:128] ∘ (%ymm1[127:64] ∘ %ymm2[63:0])
  

  If we just generalize for memory variant movsd_xmm_m64 then the resulting formula is going to be

   %ymm1  : %ymm1[255:128] ∘ (%ymm1[127:64] ∘ TEMP_READ_FROM_MEMORY)
  

  which is wrong as the correct semantics is

   %ymm1  : %ymm1[255:128] ∘ (0x0₆₄ ∘ TMP_READ_FROM_MEMORY)
  

  The latest master branch has the correct formula manually implemented.

• 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.

• pextrw/pextrb The instr is not implemented in stoke, so I had to implement it. These instr have similar semantics as registers but the implementation need to take care of zero size concatenations. Earlier we have the implemented rule as

SymBitVector::constant(dest_width - vec_len, 0) || (b >> offset*vec_len)[vec_len-1][0]

In register cases dest_width > veclen, so we have 0's concatenated in register case. The memory case, have widths equal to vec_len, which means we are concatenating zero width zero. We catch this bug while converting the formula for the followings

vpextrb_m8_xmm_imm8 
vpextrw_m16_xmm_imm8
pextrw_m16_xmm_imm8 
pextrb_m8_xmm_imm8

The z3 conversion gives exception while for concatenation with zero widths. The formula for the memory case are now fixed as follows:

 auto result = (b >> offset*vec_len)[vec_len-1][0];
 if(dest_width > vec_len) {
   result = SymBitVector::constant(dest_width - vec_len, 0) || result;
 }

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.