circuitous
circuitous copied to clipboard
trailofbits
binary->LLVM->circuits
Right now things look at bit like this:  What it should look like is that there is a named advice node called `instruction_length`, and then each `DecoderResult` node should...
If we can diff sub-trees for specific nodes than we can verify two properties: * We can easily implement #220 as each `DecoderResult` sub-tree should be unique * We can...
This was started, but as the decoder checks got moved and de-duplicated we need to update the code.
take `%0 = add i32 %1, i32 %2` and produce `(op4 32 add %1 %2)`
The Decoder Result has an out going child to an `And` node with 1 or more children all connecting to `const_1_1` which is trivially true. The number of edges from...
For `mov rax, [rax]`, `48 8b 00` it generates the following sub trees under `read_constraint`. `Mul 0, op2` can have their entire subtree removed A `add 0, op2` can have...
For 8-bit instructions that touch flags like `add al, al` / `00 c0` we currently have 4 separate OR checks to check if the 3rd bit of a value is...
If a bit is checked whether it is the value 1, then it gets a direct edge if the target is also an i1 But if we check if that...
Currently the value relevant for parity gets extracted through `and` it with an 8 bit representation of `1`. This value is Xor'd with a `1` We can just simply truncate...
Circuitous does not use XED, yet in our cmake there is `find_package` due to some remill config. Investigate and ideally remove it, as we do not use it as dependency...