Validate the generalization to K rule

Generalization to K rule

• Stoke uses a generic like following, to obtain the concrete semantics of any instruction like add %rax, %rbx

  add(SymBitVector dest, SymBitVector a, SymBitVector b) {
  set(d, a+b);
  }

  The assumption is the generic formula is behave identically for all the variants. Can we test it!

• Strata gives the concrete semantics of a concrete instructions. For other variants it generalize from the concrete semantics. Assumption is the generalization is correct. Test all the generalization.

• While porting to K rule, we generalize the from a concrete semantics that strata provides. Is this generalization faithful? For instruction like xchg, xadd, cmpxchg, the formula is different for different operands. So the general K rule we obtain from xchgl a,b may not represent the semantics for xchgl a, a. Fortunately there exists different instruction variants if the their semantics might be different and accordingly we might have different K rules. For example, xchgl_r32_eax and xchgl_r32_r32. But even for xchgl_r32_32 semantics could be different for cases r1 !=r2 and r1 == r2. Idea: Once lifted as K rule, test the instruction for all variants.

Lets consider xaddb SRC, DEST, as per manual the semantics is

  TEMP ← SRC + DEST;
  SRC ← DEST;
  DEST ← TEMP;

So there is an order that need to be followed.

Strata uses xaddb R1, R2, to obtain the semantics and it happened that the ordering is maintained and hence strata can generalize the semantics if xaddb R1, R1. But even if the ordering is not maintained the semantics is going to be the same for the case R1 != R2, but the generalization for the R1 == R1 case will mess up.

We cannot trust the generalization above generalization by strata. We need to test the K rule for all possible operands.