[ksclk]

> you can already use a SAT solver

Could you elaborate please? How would you approach this problem, using a SAT solver? All I know is that a SAT solver tells you whether a certain formula of ANDs and ORs is true. I don't know how it could be useful in this case.

[dragontamer]

Pretty much all instructions at the assembly level are sequences of AND/OR/XOR operations.

SAT solvers can prove that some (shorter) sequences are equivalent to other (longer) sequences. But it takes a brute force search.

IIRC, these super optimizing SAT solvers can see patterns and pick 'Multiply' instructions as part of their search. So it's more than traditional SAT. But it's still... At the end of the day.... A SAT equivalence problem.

[agent327]

A short look at any compiled code on godbolt will very quickly inform you that pretty much all instructions at the assembly level are, in fact, NOT sequences of AND/OR/XOR operations.

[dragontamer]

All instructions are implemented with logic gates. In fact. All instructions today are likely NAND gates.

Have you ever seen a WallaceTree multiplier? A good sequence that shows how XOR and AND gates can implement multiply.

Now, if multiply + XOR gets the new function you want, it's likely better than whatever the original compiler output.

[agent327]

That was not the claim. The claim was that assembler was made up out of sequences of OR/AND/XOR, and that claim is demonstrably false.

[astrange]

"Made up of" isn't helpful. All assembly languages are equivalent to a sequence of bit operations. (…if you ignore side effects and memory operations.)

In fact there's several different single operations you can build them all out of: https://en.wikipedia.org/wiki/One-instruction_set_computer#I...

So you take your assembly instructions, write a sufficiently good model of assembly instructions<>bit operations, write a cost model (byte size of the assembly works as a cheap one), and then search for assembly instructions that perform the equivalent operation and minimize the cost model.

Like here: https://theory.stanford.edu/~aiken/publications/papers/asplo...

[viraptor]

You're missing forest for the trees and lacking information to discuss this really. Check out this paper and similar ones if you want to learn about this area: https://arxiv.org/pdf/1711.04422

[dragontamer]

What do you think implements assembly language?

Answer: Verilog or VHDL. And these all synthesize down to AND/OR/XOR gates and eventually converted into NAND gates only.

Every assembly language statement is either data movement, or logic, or some combination of the two.

-------

We are talking about SAT solvers and superoptimizers. Are you at all familiar with this domain? Or have you even done a basic search on what the subject matter is?

[saagarjha]

Computers are not programmed on the level of logic gates. If you want to do that, design an FPGA.

[dragontamer]

Superoptimizers take this stuff into consideration.

Which is what the parent post was talking about, the rare superoptimizer.

[LtWorf]

If you want something optimised… "equivalent" isn't going to do it.

[viraptor]

You're missing the point. All instructions can be simplified to short integer operations, then all integer operations are just networks of gates, then all gates can be replaced with AND/OR/NOT, or even just NAND. That's why you can SAT solve program equivalence. See SMT2 programs using BV theory for example.

Also of course all instructions are MOV anyway. https://github.com/xoreaxeaxeax/movfuscator

[agent327]

I seem to remember that program equivalence is an NP-hard problem. I very much doubt that you can solve it by reducing it to logic gates.

[viraptor]

NP-hard is just a complexity class, not a minimal threshold. SAT solving is kind of a guided optimistic bruteforcing. If the example is small enough, you can still solve it very quickly. Same as you can solve travelling salesman for a small number of cities. We solve small cases of NP-hard things all over the place.

[viraptor]

(not to confirm it's an np-hard problem - it may not even be decidable generally, but in practice yes, you can check it that way and SMT2 theories provide the right ops)

[dragontamer]

That's why superoptimizers work on short sequences of code and take a long time doing so.

[LtWorf]

I see a guy who has never seen assembly explain assembly to people who have written assembly and written compilers and optimisations…

[peaboff]

What you're saying is true. Yes you can grind away at generating sequences of instructions, SAT solve equivalence and benchmark, but of course, you would sooner see all black holes in the observable universe evaporate before you find an instruction sequence that is both correct AND 100x faster.

[dataangel]

You're a bit naive about the complexity. Commonly longer sequences are actually faster, not just because instructions vary in their speed, but also because the presence of earlier instructions that don't feed results into later instructions still affect their performance. Different instructions consume different CPU resources and can contend for them (e.g. the CPU can stall even though all the inputs needed for a calculation are ready just because you've done too many of that operation recently). And then keep in mind when I say "earlier instructions" I don't mean earlier in the textual list, I mean in the history of instructions actually executed; you can reach the same instruction arriving from many different paths!

[astrange]

Hmm, this usually doesn't come up simply because you're usually targeting multiple different CPU generations at once, and then the details cancel each other out.

The most ffmpeg has had to do in this area is that some CPUs had very slow unaligned memory loads and some didn't.