vsklad
commented
3 years ago Thank you very much for reporting this. I posted a further fix so that it should be more generic now. Please do let me know if there is anything else.
In essence, there is a block to prevent the encoder from creating an extra result variable where the equation simplifies to a single literal or is a tautology. For the previous issue, I did a simple workaround to attempt simplifying the equation in advance to decide if extra variable is needed. That simplification didn't always work as expected. Now I changed the process so that the equation is encoded first then the result variable decision is made afterwards.
Many thanks for fixing ANF output(#1), in most cases it works. But in some rare cases it still crashes. Here is one example: ./cgen encode SHA1 -f ANF -vM 0b00100111011110001100000111100001010111000001000100110001110100110000100010010000001110011000101101010111101100101001110110010010011000010111001000101100110011100011101001000000010110100100000010011010010000101001101100111011100110111011010001100000111100011100101011111000110001101110110001111110001011001100000110101100011001011000011110110110011101100011011010111101000010110100000000000011011100110001000010110101111111011100101100000111110100100010001000111011000111010110100011010111000010100101000011001000 except:1..7 -vH compute -r 17 data.tmp
Encoding SHA-1 into ANF Assigned 505 bit(s) in "M" M = {{*/7, 0b1, 0x78c1e1}, 0x5c1131d3, 0x0890398b, 0x57b29d92, 0x61722cce, 0x3a405a40, 0x9a429b3b, 0x9bb460f1, 0xcaf8c6ec, 0x7e2cc1ac, 0x6587b676, 0x36bd0b40, 0x037310b5, 0xfdcb07d2, 0x223b1d68, 0xd70a50c8} cgen_linux64: ./bal/anf/anf.cpp:200: bal::literalid_t bal::Anf::complete_equation(bal::literalid_t, bool): Assertion `(bool)((r) == bal::LITERALID_UNASSIGNED)' failed. Aborted (core dumped)