Handling Register Instructions
- total: 1134
- stratified: 743 (692 + 51)
- not-stratified: 391
- stoked: 262 (#1)
- not-stoked: 129 (#2)
The instructions in this category are not stratified, but stoke provides manually implemented formula for them.
We could have chosen to extend the stratification process, as we do in #2, but that requires expertise in 1) choosing a base instruction or 2) comming up with a subset of search pool. We can avoid that and still get the same correctness guarentee as strata by testing with the testcases strata ends up with. This helps in finding bugs in stoke.
The instructions in this category are neither stratified nor stoke provides any formula for them.
After skimming through the unsupported instructions, I found that they are not stratified because of the following broad reasons:
- Base instruction not available
- The initial search fail to get a instruction sequence
So by 1) choosing a suitable base instruction and/or 2) comming up with a subset of search pool, I stratified all of them.
- None of not-stratified instruction implementation timed-out.
- The following
find concrete_instances/register-variants/ -name "*check_stoke.12.log" | parallel "~/scripts-n-docs/scripts/perl/filegrep.pl --file {} --antipatt 6000" |wc
shows that 389/743 stratified instructions timed out with 15 mins. Also stratified instructions are the ones which could have multiple implementations. Hence, these 389 could be the candidates for simplification.
- Even though
pdepl/qhave huge formulas, they took pretty less for execution.
* For the instructions which are already stratified and we have the K rules
for, make sure that the ported rules
are the same. This have the following benefits:
- Check if the conversion from prefix-format to k-format is correct.
- In makes them equivalent, we might need to port all the simplification lemmas from K to strata. That will eventually help in getting simpler K rules for non-stratified ones.
We do not use any of K rule derived from strata-before. Baecause making any changes (like a corection in simplification rule) require running symex. Moreover, we cannot do the test iteration frequently using stoke infrastructure.
We are usng only (107)/692 stratified formulas. Rest are obtained from stoke. Because only stratahanlder can provide those 107 instructions. And that is also the reason that we are not abandoning strata_handler altogether.
Also there are 23 rotae related instructions where stoke generate ext_rotate_left which has no similar
function in K; so we implement the ror/rol functions. The fillowing instruction
need to be tested in K domain.
RCL_R8_ONE RCR_R16_ONE RCL_RH_ONE RCL_R16_ONE ROR_R64_CL RCL_R16_CL RCL_R64_CL ROL_R32_ONE RCL_R32_ONE ROR_R16_CL ROL_R8_ONE ROR_R32_CL RCR_R32_CL RCL_R64_ONE RCR_RH_CL RCR_R32_ONE RCL_RH_CL ROR_RH_ONE ROL_R16_ONE RCL_R8_CL RCL_R32_CL RCR_RH_ONE ROL_R32_CL
rclb_r8_one
rcrw_r16_one
rclb_rh_one
rclw_r16_one
rorq_r64_cl
rclw_r16_cl
rclq_r64_cl
roll_r32_one
rcll_r32_one
rorw_r16_cl
rolb_r8_one
rorl_r32_cl
rcrl_r32_cl
rclq_r64_one
rcrb_rh_cl
rcrl_r32_one
rclb_rh_cl
rorb_rh_one
rolw_r16_one
rclb_r8_cl
rcll_r32_cl
rcrb_rh_one
roll_r32_cl
cat
/home/sdasgup3/Github/binary-decompilation/x86-semantics/docs/relatedwork/strata/Registers/stratified_minus_base.txt
| parallel /home/sdasgup3/Github/strata/stoke/bin/stoke_which_handler --opc {} |
grep "Strata"
107
cd /home/sdasgup3/Github/strata-data/output-strata/instruction-summary
// Generate non-schedule k format
ls concrete_instances/register-variants/ | parallel "/home/sdasgup3/Github/strata/stoke/bin/stoke_debug_circuit --strata_path ~/Github/strata-data/circuits/ --opc {} --k_format &> concrete_instances/register-variants/{}/instructions/{}/{}.k.format"
// Generate k format of schedule instr
source /home/sdasgup3/Github/binary-decompilation/x86-semantics/docs/relatedwork/strata/Registers/schedule_instuctions_generate_k.txt
// Generate K rule
ls concrete_instances/register-variants/ | parallel "~/x86-semantics/scripts/bvf2K.pl --opcode {} -kfile concrete_instances/register-variants/{}/instructions/{}/{}.k.format --type register" |& tee ~/Junk/x
cat /home/sdasgup3/Github/binary-decompilation/x86-semantics/docs/relatedwork/strata/Registers/schedule_instuctions.txt | parallel "~/x86-semantics/scripts/bvf2K.pl --opcode {} -kfile concrete_instances/register-variants/{}/instructions/{}/{}.k.format --type register --schedule " |& tee ~/Junk/x
The following file have the count of undefs
/home/sdasgup3/Github/binary-decompilation/x86-semantics/docs/relatedwork/strata/Registers/story_for_UNDEFS/may_undef.txt
/home/sdasgup3/Github/binary-decompilation/x86-semantics/docs/relatedwork/strata/Registers/story_for_UNDEFS/must_undef.txt
Extract the count from the K rules using
for file in $(cat ~/Junk/out); do echo $file: `grep "undefMInt\|undefBool" registerInstructions/$file.k | wc -l` ; done > out
pdepl/pdepq
pextl/pextq
cat ~/Junk/opcode.list | parallel ~/scripts-n-docs/scripts/perl/filegrep.pl --file concrete_instances/register-variants/{}/check_stoke.12.log --patt "Execu" --show
cat ~/Junk/opcode.list | parallel "~/Github/strata/stoke/bin/stoke_which_handler --opc {}"
We cannot generate the model from strata handler because we have already skipped the 585
instruction from strata handler. Unskip it if we want to do the comparision.
parallel -a ~/Junk/opcode.list "echo; echo {}; ~/Github/strata/stoke/bin/stoke_debug_circuit --strata_path /home/sdasgup3/Github/strata-data/circuits/ --opc {} --smtlib_format &> concrete_instances/register-variants/{}/instructions/{}/{}.strata.A.z3.sym"
parallel -a ~/Junk/opcode.list "echo; echo {}; ~/Github/strata/stoke/bin/stoke_debug_circuit --opc {} --smtlib_format &> concrete_instances/register-variants/{}/instructions/{}/{}.strata.B.z3.sym"
parallel -a ~/Junk/opcode.list "echo; echo {}; ~/Github/master_stoke/bin/stoke_debug_formula --opc {} --smtlib_format &> concrete_instances/register-variants/{}/instructions/{}/{}.strata.C.z3.sym"
A - C
parallel -a ~/Junk/opcode.list "echo; echo {}; ~/x86-semantics/scripts/z3compare.pl --file concrete_instances/register-variants/{}/instructions/{}/{}.strata.A.z3.sym --file concrete_instances/register-variants/{}/instructions/{}/{}.strata.C.z3.sym --opcode {} --workfile concrete_instances/register-variants/{}/instructions/{}/{}.prove.A.C.z3 ; z3 concrete_instances/register-variants/{}/instructions/{}/{}.prove.A.C.z3" |& tee ~/Junk/log.AC
B - C
parallel -a ~/Junk/opcode.list "echo; echo {}; ~/x86-semantics/scripts/z3compare.pl --file concrete_instances/register-variants/{}/instructions/{}/{}.strata.B.z3.sym --file concrete_instances/register-variants/{}/instructions/{}/{}.strata.C.z3.sym --opcode {} --workfile concrete_instances/register-variants/{}/instructions/{}/{}.prove.B.C.z3 ; z3 concrete_instances/register-variants/{}/instructions/{}/{}.prove.B.C.z3" |& tee ~/Junk/log.BC
A - B
parallel -a ~/Junk/opcode.list "echo; echo {}; ~/x86-semantics/scripts/z3compare.pl --file concrete_instances/register-variants/{}/instructions/{}/{}.strata.A.z3.sym --file concrete_instances/register-variants/{}/instructions/{}/{}.strata.B.z3.sym --opcode {} --workfile concrete_instances/register-variants/{}/instructions/{}/{}.prove.A.B.z3 ; z3 concrete_instances/register-variants/{}/instructions/{}/{}.prove.A.B.z3" |& tee ~/Junk/log.AB
bswap_r32:StrataHandler:None
bswap_r64:StrataHandler:None
clc:StrataHandler:None
cmc:StrataHandler:None
cvtpd2dq_xmm_xmm:StrataHandler:None
cvtpd2ps_xmm_xmm:StrataHandler:None
cvttpd2dq_xmm_xmm:StrataHandler:None
movddup_xmm_xmm:StrataHandler:None
movdqa_xmm_xmm:StrataHandler:None
movd_r32_xmm:StrataHandler:None
movd_xmm_r32:StrataHandler:None
movhlps_xmm_xmm:StrataHandler:None
movlhps_xmm_xmm:StrataHandler:None
movmskpd_r32_xmm:StrataHandler:None
movmskpd_r64_xmm:StrataHandler:None
movshdup_xmm_xmm:StrataHandler:None
movsldup_xmm_xmm:StrataHandler:None
shrxq_r64_r64_r64:StrataHandler:None
stc:StrataHandler:None
vaddsd_xmm_xmm_xmm:StrataHandler:None
vaddss_xmm_xmm_xmm:StrataHandler:None
vcvtpd2dqx_xmm_xmm:StrataHandler:None
vcvtpd2ps_xmm_xmm:StrataHandler:None
vcvtsd2ss_xmm_xmm_xmm:StrataHandler:None
vcvtss2sd_xmm_xmm_xmm:StrataHandler:None
vcvttpd2dq_xmm_xmm:StrataHandler:None
vdivsd_xmm_xmm_xmm:StrataHandler:None
vdivss_xmm_xmm_xmm:StrataHandler:None
vfmadd132pd_xmm_xmm_xmm:StrataHandler:None
vfmadd213pd_xmm_xmm_xmm:StrataHandler:None
vfmadd213pd_ymm_ymm_ymm:StrataHandler:None
vfmadd213ps_xmm_xmm_xmm:StrataHandler:None
vfmadd213ps_ymm_ymm_ymm:StrataHandler:None
vfmadd213ss_xmm_xmm_xmm:StrataHandler:None
vfmadd231pd_xmm_xmm_xmm:StrataHandler:None
vfmadd231pd_ymm_ymm_ymm:StrataHandler:None
vfmadd231ps_xmm_xmm_xmm:StrataHandler:None
vfmadd231ps_ymm_ymm_ymm:StrataHandler:None
vfmadd231sd_xmm_xmm_xmm:StrataHandler:None
vfmadd231ss_xmm_xmm_xmm:StrataHandler:None
vfmsub132pd_xmm_xmm_xmm:StrataHandler:None
vfmsub132ps_xmm_xmm_xmm:StrataHandler:None
vfmsub213pd_xmm_xmm_xmm:StrataHandler:None
vfmsub213pd_ymm_ymm_ymm:StrataHandler:None
vfmsub213ps_xmm_xmm_xmm:StrataHandler:None
vfmsub213ps_ymm_ymm_ymm:StrataHandler:None
vfmsub213sd_xmm_xmm_xmm:StrataHandler:None
vfmsub231pd_xmm_xmm_xmm:StrataHandler:None
vfmsub231pd_ymm_ymm_ymm:StrataHandler:None
vfmsub231ps_xmm_xmm_xmm:StrataHandler:None
vfmsub231ps_ymm_ymm_ymm:StrataHandler:None
vfmsub231sd_xmm_xmm_xmm:StrataHandler:None
vfmsub231ss_xmm_xmm_xmm:StrataHandler:None
vfnmadd132ps_xmm_xmm_xmm:StrataHandler:None
vfnmadd213pd_xmm_xmm_xmm:StrataHandler:None
vfnmadd213ps_xmm_xmm_xmm:StrataHandler:None
vfnmadd213pd_ymm_ymm_ymm:StrataHandler:None
vfnmadd213ps_ymm_ymm_ymm:StrataHandler:None
vfnmadd231pd_xmm_xmm_xmm:StrataHandler:None
vfnmadd231pd_ymm_ymm_ymm:StrataHandler:None
vfnmadd231ps_xmm_xmm_xmm:StrataHandler:None
vfnmadd231ps_ymm_ymm_ymm:StrataHandler:None
vfnmadd231ss_xmm_xmm_xmm:StrataHandler:None
vfnmsub132pd_xmm_xmm_xmm:StrataHandler:None
vfnmsub132ps_xmm_xmm_xmm:StrataHandler:None
vfnmsub213pd_xmm_xmm_xmm:StrataHandler:None
vfnmsub213pd_ymm_ymm_ymm:StrataHandler:None
vfnmsub213ps_xmm_xmm_xmm:StrataHandler:None
vfnmsub213ps_ymm_ymm_ymm:StrataHandler:None
vfnmsub213ss_xmm_xmm_xmm:StrataHandler:None
vfnmsub231pd_xmm_xmm_xmm:StrataHandler:None
vfnmsub231pd_ymm_ymm_ymm:StrataHandler:None
vfnmsub231ps_xmm_xmm_xmm:StrataHandler:None
vfnmsub231ps_ymm_ymm_ymm:StrataHandler:None
vfnmsub231ss_xmm_xmm_xmm:StrataHandler:None
vfnmsub231sd_xmm_xmm_xmm:StrataHandler:None
vmovddup_xmm_xmm:StrataHandler:None
vmovddup_ymm_ymm:StrataHandler:None
vmovdqa_xmm_xmm:StrataHandler:None
vmovdqa_ymm_ymm:StrataHandler:None
vmovd_r32_xmm:StrataHandler:None
vmovd_xmm_r32:StrataHandler:None
vmovhlps_xmm_xmm_xmm:StrataHandler:None
vmovlhps_xmm_xmm_xmm:StrataHandler:None
vmovmskpd_r32_xmm:StrataHandler:None
vmovmskpd_r32_ymm:StrataHandler:None
vmovmskpd_r64_xmm:StrataHandler:None
vmovmskpd_r64_ymm:StrataHandler:None
vmovq_r64_xmm:StrataHandler:None
vmovq_xmm_r64:StrataHandler:None
vmovq_xmm_xmm:StrataHandler:None
vmovshdup_xmm_xmm:StrataHandler:None
vmovshdup_ymm_ymm:StrataHandler:None
vmovsldup_xmm_xmm:StrataHandler:None
vmovsldup_ymm_ymm:StrataHandler:None
vmulsd_xmm_xmm_xmm:StrataHandler:None
vmulss_xmm_xmm_xmm:StrataHandler:None
vpbroadcastd_xmm_xmm:StrataHandler:None
vpbroadcastq_xmm_xmm:StrataHandler:None
vpbroadcastd_ymm_xmm:StrataHandler:None
vpbroadcastq_ymm_xmm:StrataHandler:None
vrcpss_xmm_xmm_xmm:StrataHandler:None
vrsqrtss_xmm_xmm_xmm:StrataHandler:None
vsqrtsd_xmm_xmm_xmm:StrataHandler:None
vsqrtss_xmm_xmm_xmm:StrataHandler:None
vsubsd_xmm_xmm_xmm:StrataHandler:None
vsubss_xmm_xmm_xmm:StrataHandler:None
cd strata-data/output-strata/instruction-summary
parallel -a ~/x86-semantics/docs/relatedwork/strata/Registers/supported_by_strata_branch.txt "echo; echo {}; ~/Github/strata/stoke/bin/stoke_debug_circuit --strata_path /home/sdasgup3/Github/strata-data/circuits/ --opc {} --smtlib_format &> concrete_instances/register-variants/{}/instructions/{}/{}.strata.A.z3.sym"
cd strata-data/output-strata/instruction-summary
parallel -a ~/x86-semantics/docs/relatedwork/strata/Registers/supported_by_strata_branch_stoke_handler.txt "echo; echo {}; ~/Github/strata/stoke/bin/stoke_debug_circuit --opc {} --smtlib_format &> concrete_instances/register-variants/{}/instructions/{}/{}.strata.B.z3.sym"
cd strata-data/output-strata/instruction-summary
parallel -a ~/x86-semantics/docs/relatedwork/strata/Registers/supported_by_master_branch.txt "echo; echo {}; ~/Github/master_stoke/bin/stoke_debug_formula --opc {} --smtlib_format &> concrete_instances/register-variants/{}/instructions/{}/{}.strata.C.z3.sym"
parallel -a ~/x86-semantics/docs/relatedwork/strata/Registers/supported_by_strata_branch_stoke_handler.txt "echo; echo {}; ~/x86-semantics/scripts/z3compare.pl --file concrete_instances/register-variants/{}/instructions/{}/{}.strata.A.z3.sym --file concrete_instances/register-variants/{}/instructions/{}/{}.strata.B.z3.sym --opcode {} --workfile concrete_instances/register-variants/{}/instructions/{}/{}.prove.A.B.z3 ; z3 concrete_instances/register-variants/{}/instructions/{}/{}.prove.A.B.z3" |& tee ~/Junk/log.alt