Extending instruction support beyond Strata
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.
We have the stoke formulaes only and we need to check the validity of those formula ensuring the same correctness guarentee as strata.
- 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.
We neither have the stoke formulaes, nor stratifiied formula.
- 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.
We have a stratified formula for 256 variant of imm8 instructions. Also we have the generic stoke formula.
- For each of 256 immediates I:
- Stoke_formula_instr(I) == Strata_formula_instr_I
We have a stratified formula for 256 variants of imm8 instructions, but no generic stoke formula.
- Implement the formula manually
- For each of 256 immediates I:
- Stoke_formula_instr(I) == Strata_formula_instr_I
parallel -a ~/x86-semantics/docs/relatedwork/strata/Memories/memory_instructions.txt "~/x86-semantics/scripts/process_spec.pl --prepare_concrete --opcode {} --workdir concrete_instances/memory-variants/{}"
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_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"