Handling Memory Instructions

Porting to K Use --keep_imm_symbolic as memory instr might contain imms

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

// Generate  k format

ls concrete_instances/memory-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/memory-variants/{}/instructions/{}/{}.k.format" |& tee ~/Junk/log

cat /home/sdasgup3/Github/binary-decompilation/x86-semantics/docs/relatedwork/strata/Memories/no_need_for_imm_symbolic.txt | parallel  "/home/sdasgup3/Github/strata/stoke/bin/stoke_debug_circuit --strata_path ~/Github/strata-data/circuits/ --opc {} --k_format  &> concrete_instances/memory-variants/{}/instructions/{}/{}.k.format" |& tee ~/Junk/log

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

Derived only by Strata(102)

All generalized from 107 register which themselves are strata only derived.

https://github.com/sdasgup3/binary-decompilation/blob/master/x86-semantics/docs/relatedwork/strata/Memories/derived_from_strata_handler_only.txt

Testing Notes

• Punting to K testing.

vpmaddwd_ymm_ymm_m256 <-- Both these are coming from packed handler, but takes > 1hr time to test.
vpmaddwd_xmm_xmm_m128

idivw_m16 <-- sandbox exiting abnormally because of presence of zero division cases.
divw_m16
idivq_m64
idivl_m32
divq_m64
divb_m8
idivb_m8
divl_m32