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

Assemblers

gas - gnu assembler llvm-as https://www.xorpd.net/pages/links.html

yasm nasm fasm https://board.flatassembler.net/

terse command line flag

SASM - simple crossplatform IDE for NASM, MASM, GAS and FASM assembly languages http://dman95.github.io/SASM/

Macro-11 https://en.wikipedia.org/wiki/MACRO-11 PDP-11 macro assembly. Interesting manual

Debuggers

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

Directives

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

De facto standard for desktops

intel software develpoer manuals

https://en.wikipedia.org/wiki/INT_(x86_instruction) int3 is a breakpoint instruction https://twitter.com/pkhuong/status/1507790343151960073?s=20&t=GsM8M-fHdbvp9M4n5S4-kg

asmtutor

box64 x86 emultator for arm fex

BMI1 BMI2

Bit manipulation instructions https://twitter.com/geofflangdale/status/1502481857375793153?s=20&t=j5MN13cFOkc3qH8tpATyNA apparently people can do crazy stuff with this https://twitter.com/pkhuong/status/1497332651891515395?s=20&t=j5MN13cFOkc3qH8tpATyNA

pshufb pext pdep

GAS

https://cs.lmu.edu/~ray/notes/gasexamples/ Seems like really good intro to assembly https://jameshfisher.com/2018/03/10/linux-assembly-hello-world/

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

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

using a macro

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

.data
hello:
  .ascii "Hello world\n"
  len = . - hello
.text
_start:
  myprint $hello, $len

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

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

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

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


echo '
.global _start
_start:
  mov $0x42, %rax
  int3
' | 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

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

memory barrier

CET control enforcement technology

endbr valid jump destinations for indirect jumps

x86 forth

ARM

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]
.data
mylist:
  .word 4,5,6,7,42

import tempfile
import subproess
def asm(code):
  with tempfile.TemporaryFile() as fp:
    fp.write(code)
    fp.flush()
    subprocess.run(["arm-linux-gnueabi-as", fp.name])
    subprocess.run(["gdb", fp.name])





from unicorn import *
mu = Uc(UC_ARCH_ARM64, UC_MODE_ARM)

ARMv8 A64 Quick Reference asm tutor port

PowerPC

RISC V

SAIL Risc V spec riscv- coq

risc v J extesnions graphical assembler and cpu emulator

https://www.cs.cornell.edu/courses/cs3410/2019sp/riscv/interpreter/# 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
loop:
  add t0,a0,t0
  sub a0, a0, t1
  #jal x0, loop
  bne a0, x0, loop

https://web.eecs.utk.edu/~smarz1/courses/ece356/notes/assembly/ notes

https://github.com/jameslzhu/riscv-card/blob/master/riscv-card.pdf 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

instructions

example risc5 programs. sort, search. vector matrix mult, string copy. https://marz.utk.edu/my-courses/cosc230/book/example-risc-v-assembly-programs/

  • https://www.chiark.greenend.org.uk/~sgtatham/coroutines.html
  • https://en.wikibooks.org/wiki/X86_Assembly
  • https://en.wikibooks.org/wiki/Embedded_Systems
  • https://www.ic.unicamp.br/~pannain/mc404/aulas/pdfs/Art%20Of%20Intel%20x86%20Assembly.pdf Art of Assembly DOS version. Good stuff in here. Some ways of implementing function calls I’d never considered

FORTH

https://en.wikipedia.org/wiki/Threaded_code

https://en.wikipedia.org/wiki/Threaded_code

https://gitlab.com/tsoding/porth

High level assemlby / macros

https://en.wikipedia.org/wiki/High-level_assembler

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--;
  ; FALLTHRU
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 
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
    Obj.magic 

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

https://twitter.com/search?q=typed%20assembly&src=typed_query 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

INTERFACING COMPILERS, PROOF CHECKERS, AND PROOFS FOR FOUNDATIONAL PROOF-CARRYING CODE- Wu thesis annotation are untrusted.

LF metamath0 ebpf connection?

Verification

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

Misc

bootstrapping a c compiler https://learnxinyminutes.com/docs/mips/

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

https://github.com/nanochess/bootBASIC boot sector basic https://nanochess.org/ https://www.lulu.com/shop/oscar-toledo-gutierrez/programming-boot-sector-games/paperback/product-24188564.html?page=1&pageSize=4 https://nanochess.org/store.html programming boot sector games

sectorlisp

x86 forth

easy 6502 assembly in browser assembler an emulator ebook

Some Assembly Required https://news.ycombinator.com/item?id=31909183

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 https://docs.micropython.org/en/latest/pyboard/tutorial/assembler.html inline assembler in micropython

isa specification link list