See also nots on:

  • computer architecture
  • performance
  • linkers

-S flag on gcc and other compilers often dumps assembly Godbolt compiler explorer is also very useful


gas - gnu assembler llvm-as

yasm nasm fasm

terse command line flag

SASM - simple crossplatform IDE for NASM, MASM, GAS and FASM assembly languages

Macro-11 PDP-11 macro assembly. Interesting manual


See note on debuggers

I’ve come to realize that even forplaying around in assmbly, a debugger is pretty clutch


gas gas directives

  • .equiv
  • cfi directives
  • .debug_line maps addresses to source code lines
  • .debug_info maps source variables to registers and stack locations
  • .eh_frame maps address location return address and callee saved registers info. “exception handling”

x86 x86 assembler in 250 lines of C

De facto standard for desktops

intel software develpoer manuals int3 is a breakpoint instruction


box64 x86 emultator for arm fex

x86 gui programming using strace is kind of cool

say hello to x86 assembly

  • mov movz movs
  • movsb copy byte from esi to edi and inc/dec both. Useful string op
  • cmov__ conditional mov based on flags.
  • lea calculates a pointer offset in one instruction. 3 operands, a shift and a constant add.
  • add sub or xor inc dec
  • imul idiv mul. one parameter. implicit rax as one operand. rdx:rax as implicit output
  • syscall
  • test cmp
  • jmp jnz jz condition suffixes
  • setxx copy from flags
  • call
  • push pop enter leave
  • loop kind of a goofball. dec ecx and jump if zero. Hmm slow?

x86 assembly book

Addressing modes

rdi, rsi, rdx, rcx, r8-r11, rax are all good scratch registers. The first 6 of those are where function arguments go. rax is where return values go

rax accumulatr, rcx counter, rdx extended accumulator, rbx base of array,


Bit manipulation instructions apparently people can do crazy stuff with this

pshufb pext pdep


Using qemu is nice even on native because we can use -d flag to dump cpu state and instruction. Then I dn’t have to fiddle wth gdb or a gui or include printf functionlity or remember system call numbers for call / calling conventions. All great stuff, but annoying if you’re interested in just fiddling with assembly.

echo '
#include <sys/syscall.h>
.extern _start
    mov $0x20,%rax
    int3 # interrupt. execution will stop here. analog of printf debugging
    mov $0x42,%rax
    mov $60, %rax # exit syscall number for clean exit. or just let it segfault. yolo.
    int $0x80
' > /tmp/myprog.s
gcc -nostdlib -static -o /tmp/myprog /tmp/myprog.s
qemu-x86_64 -d in_asm,cpu -singlestep /tmp/myprog Seems like really good intro to assembly

.global _start
  .ascii "Hello world\n"
  len = . - hello
  mov $1, %rax # write
  mov $1, %rdi # stdout
  mov $hello, %rsi #
  mov $len, %rdx

  mov $60, %rax #  exit
  mov $0, %rdi

using a macro

.global _start
.macro myprint str len
  mov $1, %rax # write
  mov $1, %rdi # stdout
  mov \str, %rsi
  mov \len, %rdx

  .ascii "Hello world\n"
  len = . - hello
  myprint $hello, $len

  mov $60, %rax #  exit
  mov $0, %rdi

Using a function. RDI, RSI, RDX, RCX, R8, R9

.global _start
  mov %rsi, %rdx   #len
  mov %rdi, %rsi
  mov $1, %rax  # write
  mov $1, %rdi  # stdout
  mov $hello, %rdi
  mov $len, %rsi
  call myprint

  mov $60, %rax #  exit
  mov $0, %rdi
  .ascii "Hello world\n"
  len = . - hello

echo '
.global _start
  mov $0x42, %rax
' | as -o /tmp/a.out #-x assembler -
ld /tmp/a.out -o /tmp/a2.out
#chmod +x /tmp/a.out
gdb /tmp/a2.out -ex run -ex 'info registers'


Nasm does seem a little nicer. x86 only though.

nasm tutorial pretty good

global _start
  mov rdi, 10 ; mov 10 into rdi.
  int3   ; interrupt for debugger
  add rsi, rdi ; 
  • db pseduo instruction
echo "
global _start
section .text
  mov rax, 42
" > /tmp/test.s
nasm -felf64 /tmp/test.s -o /tmp/temp
ld /tmp/temp -o /tmp/temp2
file /tmp/temp2
gdb /tmp/temp2
echo "
;default rel
extern puts
global main
section .text
  sub rsp, 8
  mov BYTE [rsp + 0], 'h'
  mov BYTE [rsp + 1], 'e'
  mov BYTE [rsp + 2], 'l'
  mov BYTE [rsp + 3], 'l'
  mov BYTE [rsp + 4], 'o'
  mov BYTE [rsp + 5], 0
  mov rdi, rsp
  CALL puts WRT ..plt

  mov rax,0
  add rsp,8

" > /tmp/test.s
nasm -felf64 /tmp/test.s -o /tmp/temp
gcc /tmp/temp  -o /tmp/temp2
file /tmp/temp2

unix abi

memory barrier

CET control enforcement technology

endbr valid jump destinations for indirect jumps

x86 forth

ARM an arm lisp

Arm memory tagging extension

cpulator online assembler and emulator for teaching pretty nice Assembly Language Programming with ARM – Full Tutorial for Beginners INTRODUCTION TO ARM ASSEMBLY BASICS - Azeria

r7 is system call mov r0, #0xa

mov r7, #1
swi 0

mov r2, r1

ldr r0,=mylist
ldr r0,[r0]
ldr r2,[r0,#4]
  .word 4,5,6,7,42
import tempfile
import subproess
def asm(code):
  with tempfile.TemporaryFile() as fp:

from unicorn import *

ARMv8 A64 Quick Reference asm tutor port



SAIL Risc V spec riscv- coq

risc v J extesnions graphical assembler and cpu emulator nice little interpeter to play with risc v from scratch A Multipurpose Formal RISC-V Specification hs-2-coq based compcert risc-v backend

mini-rv32ima is a single-file-header riscv5 eumlator instruction decoder in javascript? Why?

risc v virtual machine rvemu Writing a RISC-V Emulator in Rust book

# it's the sum of 1 to n
addi a0, x0, 4
addi t0, x0, 0
addi t1, x0, 1
  add t0,a0,t0
  sub a0, a0, t1
  #jal x0, loop
  bne a0, x0, loop notes nice cheatsheet of instructions, registers registers

  • a0 a1 are arguments nad returns values
  • t0-t are temporaries
  • x0 or zero is zero register
  • equivalent floating point just add f.
  • s0 .. saved resgiters


example risc5 programs. sort, search. vector matrix mult, string copy.

6502 6502 assembler in python

VAX vax in fpga supposedly vax was a very nice assembly language. The ultimate cisc. Greg has mentioned some really cool macro programming abilities.


  • Jonesforth super well annotated forth written in x86

High level assemlby / macros

The art of assembly book by Hyde

If, for, while macros Auto flattening. (loc,asm) pairs r0 == (r0, "") Coq: The world’s best macro assembler?

Typed Assembly

echo "
int foo(int x) {
  return x + 42;
" | gcc -g -x c -c -o /tmp/foo.o -
objdump -d /tmp/foo.o
import angr
proj = angr.Project("/tmp/foo.o")
foo = proj.loader.find_symbol("foo")
cfg = proj.analyses.CFGFast()
foo = cfg.kb.functions["foo"]
from pypcode import Context, PcodePrettyPrinter
ctx = Context("x86:LE:64:default")
dx = ctx.disassemble(b"\x48\x35\x78\x56\x34\x12\xc3")
for ins in dx.instructions:
    print(f"{ins.addr.offset:#x}/{ins.length}: {ins.mnem} {ins.body}")

Type preserving compilation Shift from alpha bound names to true names. foo: {ebx:b4} label foo expects a 4 byte value in ebx They still have a code rewriting semantics analagous to immediate subtition. Closures use existential types

Code blocks have type annotations about assumptions of typed content of registers code pointers stacks have type sequences and polymorphic below that.

weirich papers we love

related to PCC (proof carryng code). Use type discipline

The continuation is carried on the stack (typically). {eax:b4} is the calling convention on x86. {rax:b8} would be calling convention on x86_64. That continuation is threaded through everything (if we don’t smash stack)

A summation program annotated

sum: ; {ecx:b4, ebx:{eax:b4}}
  mov eax, 0  ; int acc = 0;
  jmp test
loop:{eax:b4, ecx:b4, ebx:{eax:b4}}
  add eax, ecx  ; acc += x
  dec ecx      ; x--;
test: ; {eax:b4, ecx:b4, ebx:{eax:b4}}
  cmp ecx,0 ; while( x != 0)
  jne loop 
  jmp ebx ; return acc

Compare and contrast these annotations with preconditions. I mean, types can be viewed as some kind of abstract interpretation.

tal weirich haskell

FunTAL: reasonably mixing a functional language with assembly prncipled language interopaibility course - ahmed TAL website TALx86 from system f to typed assembly language typed assembly language alasteir reid’s notes

stack based tpyed assembly language Stack type: esp sptr to a stack forall rho:Ts. {esp:sptr{eax:B4, esp:sptr B4::rho}::B4::rho”

Using “free theorem” to ensure callee register saving. forall a. {r0:'a, r1:{r0:'a} } the only way to type this is to pass r0 into the contuation. Analog of forall b, b -> (b -> Void) -> Void. Security / noniterference and polymorphism free theorems are the same kind of thing

Type-Based Decompilation1 (or program reconstruction via type reconstruction) hmm. datalog disassembly as type reconstruction?

Can I embed TAL as a well typed DSL in ocaml staged metaprograming style? Polymorphic record types would probably be nice. I mean, it’s possible that’s what they already did?

type sem = string
type (a,b) stack
{ void
type eax
type edx
type ecx
type 'a fptr

(* "subtyping" using polymorphism *)
type ('r0, 'r1, 'r2) regfile = {r0 : 'r0; r1 : 'r1; r2 : 'r2 }

let zero_reg : (int,int,int) regfile = {r0 = 0; r1 = 0; r2 = 0}
let r0_valid : ( int  , ?  , ? ) regfile (* existential type maybe?  (forall r1 r2. (int, r1,r2) regfile -> 'ret) -> 'ret *)

type instr = Mov 

let rec interp heap regfile instr = 
  match instr with
  | Jump nu ->
  | Mov dst src -> 
  | Add dst src1 src2 ->
  | If cond dst fall -> 

(* analogous to metaocaml's code *)
type 't asm = string
let assemble : 't asm -> 't =
    let bin = Unix.exec ["as" ; ] in
    let = Unix.mmap Execute yada
    let f = ccall

let disassemble : 't -> 't asm (* ?? *) =
    (* use obj to figure out code pointer. Differentiate code pointers vs closures. *)
    let Unix.exec "objdump" or "ghidra" ???

let compile : 't code -> 't asm = 
    let Unix.exec "ocamlopt"

let decompile : 't asm -> 't code = 

let byte_compile : 't code -> 't bytecode = 
    let Unix.exec "ocamlc"

(*Might want to go objects just for strucutral notaton *)
(* let mov_r0_r1 : < r0 : 'a; r1: 'b> -> <r0 : 'a; r1 : 'a> = fun st -> *)

type ('r0, 'r1, 'r2) st = ST
let mov_r0_r1 : ('r0,'r1,'r2) st -> ('r0, 'r0, 'r2) st = fun x -> ST

(* let mov : 'rdst reg -> 'rsrc reg ->  
   Ths can't work at all
   selection style?
   (a,b,c) reg -> (a1,b1,c1) reg -> ? 
COuld first class modules help? I don't really see it.

module type INSN = sig



(* let mov : 'a reg -> 'b reg -> {rax : } *)

(* het list *)
type ('xs, 'x) cons = {hd : 'x; tl : 'xs} 
type nil = unit
let cons x xs = {hd = x; tl = xs}
let nil = ()

let swap : type r. ((r, 'b) cons, 'a) cons -> ((r, 'a) cons, 'b) cons = 
  fun x -> cons (cons x.hd
let binop : ('a -> 'b -> 'c) ->  (('r, 'b) cons, 'a) cons -> ('r, 'c) cons   = 
  fun op st -> cons (op st.hd

let add = binop (+)
let sub = binop (-)
let mul = binop (fun x y -> x * y)

let push : 'a -> 'r -> ('r, 'a) cons = cons
let imm = push
let pop : ('r, 'a) cons -> 'r = fun st ->
let dup : ('r, 'a) cons -> (('r, 'a) cons, 'a) cons = fun st -> cons st.hd st  

module type STACKSIG = sig
  type 'a repr
  type ('xs, 'x) cons
  type nil
  (* list out types supported *)
  (* Hmm. I dunno if that raw 'r is ok. *)
  val push_int : int repr -> 'r -> ('r, int) cons

(* use rdi,...  etc as extensions of the stack?
   Mark extra param
type rdi = RDI
type rsi = RSI
type rax = RAX

type ('rdi, 'rsi) regfile = {rdi : 'rdi ; rsi : 'rsi}


consider the stack below arguments as non existent... hm.
let systemv_call_1 : ( (nil , 'a , rdi) cons -> ('b, rax) cons) -> ('a -> 'b)  
Or we could just mov regusters onto the stack as a prelude
Or internaly track not in types what is around.

type ( , ) cons = {hd : location ; ty : 'x;   in_use :   }


So what is the type of mov rax, 0? How is fallthru represented?

TAL led in some ways to Cyclone, which is turn heavily influenced rust

What would a “well-typed” interpreter of assembly look like Mem, Reg ->

Pierce - Advanced Topics has a chapter on TAL and PCC (4 and 5)

Ulf norell typed assembly in agda twitter

chen and hawblitzel - channel 9 introduction to typed assembly. Verse a typed operatiog system Safe to the last instruction: automated verification of a type-safe operating system - Verve a type safe operating system Hawblitzel bibliography

xi and harper - a dependently typed assembly langguae singleton 2011- a depently typed assembly langguae

Inferable object-oriented typed assembly language - Tate Chen hawblitzel youtube

% pcode
% tabled prolog appropriate becase we need unification variables for polymorphism.
hastype() :- .

dwarf annotations as untrusted input?

gradual typing is a natural fit dynamic typed assembly languge

Proof Carrying Code

foundational pcc - appell and felty A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code Chapter in Pierce Necula’s thesis


LF metamath0 ebpf connection?


Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language Galois’ SAW A verified, efficient embedding of a verifiable assembly language F* land. Vale - Verifying High-Performance Cryptographic Assembly Code. Hmm. this is leveraging dafny

Semantics / Specification

L3 in cakeml L3 risc v L3 mips

alastair reid’s notes

Sail ASL arm spec language

A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture K framework

Flexible Instruction-Set Semantics via Type Classes

risc v Machine Readable Specs

echo "
default Order dec // what does this do?
\$include <prelude.sail>

//val print = monadic {ocaml: \"print_endline\"} : string -> unit

let n:int = 42
// val myguy

//function myguy(x) = x + 1
enum E = A | B | C

//val main : unit -> unit

function main (() : unit) -> unit = print_endline(\"hello world\")
" > /tmp/foo.sail
sail -coq -o /tmp/foo /tmp/foo.sail 
cat /tmp/foo.v

sail -i interpreter isla. It’s more than a symbolic executor I can dump an IR of instruction semantics. Pseudo-smt. Has command statements too. Still. The expressions are smt expressions yea?

pydrofoil using pypy jit with sail. It uses isla to dump semantics?


bootstrapping a c compiler

bootsector games Introduction to 80x86 Assembly Language and Computer Architecture” by R. C. Detmer, 2. ed. 2006.

xorpd xchg rax rax reversing hero flatassembler

boot sector means they got the code under 512 bytes boot sector basic programming boot sector games


x86 forth

easy 6502 assembly in browser assembler an emulator ebook

Some Assembly Required

Metamath zero - is there some simpler thing one could do? Why did metamath really have to be written in assembly? Is this a trusted computing base thing?

peachpy an assembly dsl in python inline assembler in micropython