6 ms·

From math to machine: translating a function to machine code

108 points by briansteffens 10y ago

LeanderK 10y ago
out of interest, can somebody check how GHC compiles the factorial function as defined in the blogpost?
- grenoire 10y ago
  Not GHC, but GCC 6.3 with -O2 is https://godbolt.org/g/ATkIr1 https://godbolt.org/g/ATkIr1 for reference.
- rnhmjoj 10y ago
  https://gist.github.com/b097fded87a2b16863947acd3a975b2a https://gist.github.com/b097fded87a2b16863947acd3a975b2a This is code produced by GHC 8.0.2 for the program module Test where factorial :: Int -> Int factorial n = product [1 .. n] The module thing is necessary to produce the object file without a "main" function.
minimax 10y ago
What calling convention passes the first integer argument in rax and the return value in rdi? Thats exactly backwards from what I usually see.
conistonwater 10y ago
I wonder: since there are only thirteen factorials that fit into int32, and thus only 13 possible valid inputs, is it faster or slower to use a very small lookup table? https://godbolt.org/g/9ii0S0 https://godbolt.org/g/9ii0S0 It seems like this is the sort of thing a good compiler can figure out on its own, but I don't fully understand what clang is doing with this loop: https://godbolt.org/g/ze5ycb https://godbolt.org/g/ze5ycb
bogomipz 10y ago
This was neat. I enjoyed reading it. It wouldn't take much more to add the level below the machine code to this write up showing how the bits in the in the opcode generate control signals to carry out the micro-ops that make up the function.
- nickpsecurity 10y ago
  I used to have a visual example of how it works. Couldn't find it in a quick search. Anyway, here's a text example for PDP-11 to illustrate what it looks like along with a detailed paper on concepts and some tooling. http://www.cdf.toronto.edu/~ajr/258/notes/micro/microcode.html http://www.cdf.toronto.edu/~ajr/258/notes/micro/microcode.ht... http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.472.666&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.472...
  - bogomipz 10y ago
    Oh sure, I know. I was just staying it would be a nice addition, since the post is pretty original and novel. By the way was this the link you were thinking of? https://cseweb.ucsd.edu/classes/wi13/cse141-b/slides/05-SingleCycleCPU.pdf https://cseweb.ucsd.edu/classes/wi13/cse141-b/slides/05-Sing... By the they way second link is a nice read. Thanks.
nickpsecurity 10y ago
People wanting to go from math to machine might like a work that starts with formal specs. http://www.cl.cam.ac.uk/~mom22/miniml/hol2miniml.pdf http://www.cl.cam.ac.uk/~mom22/miniml/hol2miniml.pdf The resulting ML can be compiled to assembly by verified, CakeML compiler. https://cakeml.org https://cakeml.org
- iheartmemcache 10y ago
  It's only Monday and that paper lead me to L3 and the UNSW course[1] notes. There goes my next weekend or four. Thanks, ya son of a gun ;) [1] https://www.cse.unsw.edu.au/~cs4161/lect.html https://www.cse.unsw.edu.au/~cs4161/lect.html
  - nickpsecurity 10y ago
    Glad you found something fun. If it's L3 for CPU's you mean, then one project of value nobody has done is put in specs for VAMP processor. It was mathematically verified in PVS as part of Verisoft project. They did OS and C subset for it. Adding it to L3 and Myreen et al's toolkit for doing machine code in Isabelle/HOL would let their spec-to-machine-code verifications run on a verified processor. Just throwing that out there for you or anyone interested in lengthening the chain of verification. VAMP doesn't get enough attention. On HW side, someone could do a verified front-end for RISC-V on top of the VAMP components to get a mostly-verified RISC-V. Lots of low-hanging fruit out there.
- pjmlp 10y ago
  Thanks as well, I join my opinion to iheartmemcache's one. :)
chmaynard 10y ago
If the author is reading this thread, would you please comment on how math expressions are rendered in your blog? The factorial definition near the beginning looks absolutely perfect. I'd like to learn how to do this in Jekyll.
- alevskaya 10y ago
  Not the author, but their page is using the client-side javascript MathJax renderer https://www.mathjax.org/ https://www.mathjax.org/ which renders the mathematical subset of LaTeX.

108 points by briansteffens 10y ago

LeanderK 10y ago

out of interest, can somebody check how GHC compiles the factorial function as defined in the blogpost?

grenoire 10y ago
Not GHC, but GCC 6.3 with -O2 is https://godbolt.org/g/ATkIr1 https://godbolt.org/g/ATkIr1 for reference.
rnhmjoj 10y ago
https://gist.github.com/b097fded87a2b16863947acd3a975b2a https://gist.github.com/b097fded87a2b16863947acd3a975b2a This is code produced by GHC 8.0.2 for the program module Test where factorial :: Int -> Int factorial n = product [1 .. n] The module thing is necessary to produce the object file without a "main" function.

minimax 10y ago

What calling convention passes the first integer argument in rax and the return value in rdi? Thats exactly backwards from what I usually see.

conistonwater 10y ago

I wonder: since there are only thirteen factorials that fit into int32, and thus only 13 possible valid inputs, is it faster or slower to use a very small lookup table? https://godbolt.org/g/9ii0S0 https://godbolt.org/g/9ii0S0 It seems like this is the sort of thing a good compiler can figure out on its own, but I don't fully understand what clang is doing with this loop: https://godbolt.org/g/ze5ycb https://godbolt.org/g/ze5ycb

bogomipz 10y ago

This was neat. I enjoyed reading it. It wouldn't take much more to add the level below the machine code to this write up showing how the bits in the in the opcode generate control signals to carry out the micro-ops that make up the function.

nickpsecurity 10y ago
I used to have a visual example of how it works. Couldn't find it in a quick search. Anyway, here's a text example for PDP-11 to illustrate what it looks like along with a detailed paper on concepts and some tooling. http://www.cdf.toronto.edu/~ajr/258/notes/micro/microcode.html http://www.cdf.toronto.edu/~ajr/258/notes/micro/microcode.ht... http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.472.666&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.472...
- bogomipz 10y ago
  Oh sure, I know. I was just staying it would be a nice addition, since the post is pretty original and novel. By the way was this the link you were thinking of? https://cseweb.ucsd.edu/classes/wi13/cse141-b/slides/05-SingleCycleCPU.pdf https://cseweb.ucsd.edu/classes/wi13/cse141-b/slides/05-Sing... By the they way second link is a nice read. Thanks.

nickpsecurity 10y ago

People wanting to go from math to machine might like a work that starts with formal specs. http://www.cl.cam.ac.uk/~mom22/miniml/hol2miniml.pdf http://www.cl.cam.ac.uk/~mom22/miniml/hol2miniml.pdf The resulting ML can be compiled to assembly by verified, CakeML compiler. https://cakeml.org https://cakeml.org

iheartmemcache 10y ago
It's only Monday and that paper lead me to L3 and the UNSW course[1] notes. There goes my next weekend or four. Thanks, ya son of a gun ;) [1] https://www.cse.unsw.edu.au/~cs4161/lect.html https://www.cse.unsw.edu.au/~cs4161/lect.html
- nickpsecurity 10y ago
  Glad you found something fun. If it's L3 for CPU's you mean, then one project of value nobody has done is put in specs for VAMP processor. It was mathematically verified in PVS as part of Verisoft project. They did OS and C subset for it. Adding it to L3 and Myreen et al's toolkit for doing machine code in Isabelle/HOL would let their spec-to-machine-code verifications run on a verified processor. Just throwing that out there for you or anyone interested in lengthening the chain of verification. VAMP doesn't get enough attention. On HW side, someone could do a verified front-end for RISC-V on top of the VAMP components to get a mostly-verified RISC-V. Lots of low-hanging fruit out there.
pjmlp 10y ago
Thanks as well, I join my opinion to iheartmemcache's one. :)

chmaynard 10y ago

If the author is reading this thread, would you please comment on how math expressions are rendered in your blog? The factorial definition near the beginning looks absolutely perfect. I'd like to learn how to do this in Jekyll.

alevskaya 10y ago
Not the author, but their page is using the client-side javascript MathJax renderer https://www.mathjax.org/ https://www.mathjax.org/ which renders the mathematical subset of LaTeX.