Handling Memory Instructions
cd strata-data/output-strata/instruction-summary
parallel -a ~/x86-semantics/docs/relatedwork/strata/Memories/generalized_by_strata_branch_strata_cum_stoke_handler.txt "echo; echo {}; ~/Github/strata/stoke/bin/stoke_debug_circuit --strata_path /home/sdasgup3/Github/strata-data/circuits/ --opc {} --smtlib_format &> concrete_instances/memory-variants/{}/instructions/{}/{}.strata.z3.sym"
cd strata-data/output-strata/instruction-summary
parallel -a ~/x86-semantics/docs/relatedwork/strata/Memories/generalized_by_strata_branch_stoke_handler.txt "echo; echo {}; ~/Github/strata/stoke/bin/stoke_debug_circuit --opc {} --smtlib_format &> concrete_instances/memory-variants/{}/instructions/{}/{}.strata.alt.z3.sym"
cd strata-data/output-strata/instruction-summary
parallel -a ~/x86-semantics/docs/relatedwork/strata/Memories/generalized_by_strata_branch_stoke_handler.txt "echo; echo {}; ~/x86-semantics/scripts/z3compare.pl --file concrete_instances/memory-variants/{}/instructions/{}/{}.strata.z3.sym --file concrete_instances/memory-variants/{}/instructions/{}/{}.strata.alt.z3.sym --opcode {} --workfile concrete_instances/memory-variants/{}/instructions/{}/{}.prove.alt.z3 ; z3 concrete_instances/memory-variants/{}/instructions/{}/{}.prove.alt.z3" |& tee ~/Junk/log
grep -B 1 "^sat" ~/Junk/log
vfmaddsub132pd_xmm_xmm_m128 <- Both stata and master branch yeilds formula for these using strata handler, but I write simple formula for those for registers, which can now be generalized to registers; Get rid of complex formula
vfmaddsub213pd_xmm_xmm_m128
vfmaddsub132ps_xmm_xmm_m128
vfmsubadd213pd_xmm_xmm_m128
vfmaddsub231pd_xmm_xmm_m128
vfmsubadd132pd_xmm_xmm_m128
vfmsubadd231pd_xmm_xmm_m128
vfmaddsub231ps_xmm_xmm_m128 <-- END
cd strata-data/output-strata/instruction-summary
parallel -a ~/x86-semantics/docs/relatedwork/strata/Memories/generalized_by_master_branch.txt "echo; echo {}; ~/Github/master_stoke/bin/stoke_debug_formula --opc {} --smtlib_format &> concrete_instances/memory-variants/{}/instructions/{}/{}.master.branch.sym"
cd strata-data/output-strata/instruction-summary
parallel -a ~/x86-semantics/docs/relatedwork/strata/Memories/generalized_by_master_branch.txt "echo; echo {}; ~/x86-semantics/scripts/z3compare.pl --file concrete_instances/memory-variants/{}/instructions/{}/{}.strata.z3.sym --file concrete_instances/memory-variants/{}/instructions/{}/{}.master.branch.sym --opcode {} --workfile concrete_instances/memory-variants/{}/instructions/{}/{}.prove.z3 ; z3 concrete_instances/memory-variants/{}/instructions/{}/{}.prove.z3" |& tee ~/Junk/log
grep -B 1 "^sat" ~/Junk/log
vcvtpd2dq_xmm_m256::ymm1 <- master stoke formula is buggy
vfmaddsub213ps_xmm_xmm_m128::ymm1 <-- Strata's formula comes from simple handler and master ones come from strata, with diff uifs and hence sat.
vfmsubadd132ps_xmm_xmm_m128::ymm1
vfmsubadd213ps_xmm_xmm_m128::ymm1
vfmsubadd231ps_xmm_xmm_m128::ymm1 <-- END
cd strata-data/output-strata/instruction-summary
parallel -j6 -a ../nightlyruns/job.09 "~/x86-semantics/scripts/process_spec.pl --check_stoke --file concrete_instances/memory-variants/{}/check_stoke.09.txt --instructions_path concrete_instances/memory-variants/{}/instructions --use_updated_tc --testid 09 |& tee concrete_instances/memory-variants/{}/check_stoke.09.log" |& tee ~/Junk/log
Other Switches: --no_strata_handler // avoid using strata handler; mainly used for evaluating the formula of both strata and non strata handlers.
parallel -a ~/Junk/xx "~/x86-semantics/scripts/process_spec.pl --opcode {} --instructions_path concrete_instances/memory-variants/{}/instructions/ --update_tc --testid 09"
- 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
In case we have formulas from multiple sources (like strata or stoke or manually implemented), and all are proved equivalent, then we can pick the least complex one.
For example shrxl_r32_m32_r32 has its formula from strata and its hugely complex. We have written a manual one which is equiv but much simpler. To reproduce, remove the bypass condition for the opcode in strata handler and run with starta handler.
For vpbroadcastb_ymm_xmm, the stratified formula contain uif, where as the manually written one is without uif. To reproduce use sf --strata_path ../../circuits/ --opc vpbroadcastb_ymm_xmm as both master branch and strata branch are using strata handler.