Instruction tzcntq unsupported by the bounded, ddec validators

[travisdowns]

The bmi instructions like tzcntq are pretty important bit manipulation instructions for some real-world kernels, but it seems like they are not supported by the solver-based validators:

stoke debug verify --target asm64/div_ref.s --rewrite result64.s --strategy bounded --def_in "{ %rdi %rsi }" --live_out "{ %rax }"
...
Encountered error: 
Instruction tzcntq %rsi, %rbx is unsupported.

I'm happy to try to fix this if someone can point me to where the instruction behavior needs to be encoded.

Note that the tzcnt and lzcnt family in particular are important given that the much older bsf and bsr instructions are effectively unsupported as discussed in #939.

[stefanheule]

You could look at other instances where we implemented support for new instructions in the validator (e.g. #934 is a recent one) to see what places you will likely need to change. Let us know if you have specific questions.

[travisdowns]

Do you accept patches from outside the SPLG?

[stefanheule]

We do. We may reject patches if they don't pass the tests, make major changes that we don't understand or would prevent us from doing our own work, but none of that should be an issue for something like adding support to more instruction in the validator. Maybe read README.md and STYLE.md.

[bchurchill]

In src/validator there's a readme. It's a little out of date but the big ideas should be right; the design for handlers hasn't changed much (if at all). I would recommend just looking in src/validator/handlers/simple_handler.cc, and copy how things are implemented to other instructions.

The number one testing procedure is to run the fuzz tester on it. It's part of the test suite; there's an environment variable you can set to make it run longer. You can also tweak the code to test only the opcode you're adding (there's a comment in the source code that says how to do this). For safety, it's a good idea to introduce a bug, make sure the fuzz tester catches it, and then fix the bug, and make sure the fuzz tester passes. That's essentially our criteria for adding a new circuit.

[travisdowns]

Thanks. By "circuit" I assume you mean the same thing as I would call "instruction"? This is somehow a term cross-pollination from the hardware synthesis world?

It would be awesome to have a comment on how to run the fuzz tester and to limit to a new instruction in the README. I'll try to figure out how to run the fuzz tester and perhaps add that. Failing that, I'll ask here.

[stefanheule]

I really dislike the term circuit and I think we shouldn't be using it, but it's usually interchangeable with "formula". In any case, what @bchurchill means by it is the formal specification in the validator of an instruction.

The fuzz tester is run by the regular test suite. There are actually several different fuzzers, the one you want is called ValidatorFuzzTest.RandomInstructionRandomState. Just running that test can be done by running something like bin/stoke_test --gtest_filter="ValidatorFuzzTest.RandomInstructionRandomState". You can use

export TEST_VALIDATOR_FUZZ_COUNT=5000

to change the number of iteration it does (100 by default, I think). Limiting to a new instruction is done by uncommenting some code in tests/validator/fuzz.h (lines 495 onwards).