Handling Immediate Instructions

Handling #3

Description

We have the stoke formulaes only and we need to check the validity of those formula ensuring the same correctness guarentee as strata.

Handling Strategy

• For each smt formula obtained from stoke, concretize the symbolic variable corresponding to 256 immediate values (Note all these instructions have 8 bit immediate values)
• Test each resulting formula using the strata's final test suite.

Handling #4

Description

We neither have the stoke formulaes, nor stratifiied formula.

Handling Strategy

• Manually implement the instruction semantics.
• For each smt formula obtained from stoke, concretize the symbolic variable corresponding to 256 immediate values (Note all these instructions have 8 bit immediate values)
• Test each resulting formula using the strata's final test suite.

Handling #5

Description

We have a stratified formula for 256 variant of imm8 instructions. Also we have the generic stoke formula.

Handling Strategy

• For each of 256 immediates I:
  • Stoke_formula_instr(I) == Strata_formula_instr_I

Handling #6

Description

We have a stratified formula for 256 variants of imm8 instructions, but no generic stoke formula.

Handling Strategy

• Implement the formula manually
• For each of 256 immediates I:
  • Stoke_formula_instr(I) == Strata_formula_instr_I

Porting to K

cd /home/sdasgup3/Github/strata-data/output-strata/instruction-summary

// Generate  k format
ls concrete_instances/immediate-variants/ | parallel  "/home/sdasgup3/Github/strata/stoke/bin/stoke_debug_circuit --strata_path ~/Github/strata-data/circuits/ --opc {} --k_format --keep_imm_symbolic &> concrete_instances/immediate-variants/{}/{}.k.format" |& tee ~/Junk/log

// Generate K rule
ls concrete_instances/immediate-variants/ | parallel  "~/x86-semantics/scripts/bvf2K.pl --opcode {} -kfile concrete_instances/immediate-variants/{}/{}.k.format --type immediate" |& tee ~/Junk/x

Instructions which are modelled using Strata handler: None

We skip the following 22.

They are all generalized(same or extend to higher value) from base instructions which are in turn
are modelled using non-strata handlers.

Still, Strata handler owns them because of the logic:
if I is generalized using G {
 if(G a base instruction) return strata handler
 else return handler_of(G) 
}

After the non strata handler model the semantics, the strata handler can't keep
the symbolic Imp that we need to port the rules to K
Hence moving them to non-strata handler; which faithful handle the
extension of imm using sign-ext 


adcb_al_imm8:StrataHandler:AddHandler
adcw_ax_imm16:StrataHandler:AddHandler
adcl_eax_imm32:StrataHandler:AddHandler
adcw_r16_imm16:StrataHandler:AddHandler
adcw_r16_imm8:StrataHandler:AddHandler
adcl_r32_imm32:StrataHandler:AddHandler
adcl_r32_imm8:StrataHandler:AddHandler
adcq_r64_imm32:StrataHandler:AddHandler
adcq_r64_imm8:StrataHandler:AddHandler
adcq_rax_imm32:StrataHandler:AddHandler
adcb_r8_imm8:StrataHandler:AddHandler
movq_r64_imm32:StrataHandler:MoveHandler
movb_rh_imm8:StrataHandler:MoveHandler
orq_r64_imm32:StrataHandler:SimpleHandler
orq_rax_imm32:StrataHandler:SimpleHandler
orq_r64_imm8:StrataHandler:SimpleHandler
salq_r64_imm8:StrataHandler:ShiftHandler
sarq_r64_imm8:StrataHandler:ShiftHandler
shrq_r64_imm8:StrataHandler:ShiftHandler
xorq_r64_imm32:StrataHandler:SimpleHandler
xorq_r64_imm8:StrataHandler:SimpleHandler
xorq_rax_imm32:StrataHandler:SimpleHandler

Why but equivalent is required:

Because z3 cannot prove if 
        (add_double #x0000000000000000 #x0000000000000000)
     == 0
We need simplification before eq checking to prove this.