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


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

  • gdb - See notes in C.
  • cemu an ide of sorts for writing assembly and running it
  • [ollydbg]
  • edb an ollydbg for linux. Seems nice. A graphical debugger.
  • x64dbg windows only


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”


De facto standard for desktops

intel software develpoer manuals int3 is a breakpoint instruction


box64 x86 emultator for arm fex


Bit manipulation instructions apparently people can do crazy stuff with this

pshufb pext pdep

GAS 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'


global _start
  mov rdi, 10 ; mov 10 into rdi.
  int3   ; interrupt for debugger
  add rsi, rdi ; 

memory barrier

CET control enforcement technology

endbr valid jump destinations for indirect jumps

x86 forth


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.

  • Art of Assembly DOS version. Good stuff in here. Some ways of implementing function calls I’d never considered


High level assemlby / macros

The art of assembly book by Hyde

If, for, while macros Auto flattening. (loc,asm) pairs r0 == (r0, "")

Typed Assembly

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"

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


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

isa specification link list