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.

Self Goal

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