Assembly syntax for writing programs

[Armael]

Right now we are using Coq as a very weak assembler, and we have no convenient way of e.g. computing labels or offsets.

Links for inspiration (to expand):

• "Coq: the world's best macro assembler?" (https://dl.acm.org/doi/pdf/10.1145/2505879.2505897), (code: https://github.com/nbenton/x86proved)
• https://github.com/hlorenzi/customasm
• RISCV assembly syntax: https://github.com/riscv/riscv-asm-manual/blob/master/riscv-asm.md
• MIPS assembly language programmer's guide (very complete): https://www.cs.unibo.it/~solmi/teaching/arch_2002-2003/AssemblyLanguageProgDoc.pdf

[Armael]

Proposal (inspired by MIPS syntax):

(Permissions perm are interpreted as integers in expr by encoding them: cf encodePerm in the operational semantics. This is mainly useful for the restrict instruction.)

regname ::= pc | r0 | r1 | ... | r31
perm ::= O | E | RO | RX | RW | RWX
intconst ::= <positive integer> | 0x<positive integer/a-f A-F>
labelname ::= <non-keyword alphanumeric string, starting with a letter or _>
expr ::= intconst | perm | labelname | expr + expr | expr - expr | - expr | (expr)
labeldef ::= labelname :
reg_or_const ::= regname | expr

pseudo_op ::= .word expr [, expr]* 
machine_op ::=
  | jmp regname
  | mov regname reg_or_const
  | ...

op ::= machine_op | pseudo_op
statement ::= labeldef? op?

program ::= (statement '\n') *

Syntax for comments: ; this is a comment until end of line ?
(but: MIPS uses # ..., it could also be // ... or /* ... */...)

Example without labels ("buffer example"):
(to be loaded it memory at address 0)

; code
mov r1 pc
lea r1 4
subseg r1 4 7
jmp r0
; data
.word 0xA, 0xB, 0
.word 42

Example with labels ("secure counter"):

; initially, PC = (RWX, init, end, init)
;            r0 = (unknown) pointer to the context
init:
  mov r1 pc             ; r1 = (RWX, init, end, init)
  lea r1 (data-init)    ; r1 = (RWX, init, end, data)
  mov r2 r1             ; r2 = (RWX, init, end, data)
  lea r2 1              ; r2 = (RWX, init, end, data+1)
  store r1 r2           ; mem[data] <- (RWX, init, end, data+1)
  lea r1 (code-data) ; r1 = (RWX, init, end, code)
  subseg r1 code end ; r1 = (RWX, code, end, code)
  restrict r1 E ; r1 = (E, code, end, code)
  mov r2 0 ; r2 = 0
  jmp r0   ; jump to unknown code: we only give it access
           ; to an enter capability pointing to ’code’
; when ’code’ gets executed from the E capability,
; PC = (RX, code, end, code)
; r0 = (unknown) return pointer to the continuation
code:
  mov r1 PC ; r1 = (RX, code, end, code)
  lea r1 (data-code) ; r1 = (RX, code, end, data)
  load r1 r1 ; r1 = (RWX, init, end, data+1)
  load r2 r1 ; r2 = <counter value>
  add r2 r2 1 ; r2 = <counter value> + 1
  store r1 r2 ; mem[data+1] <- <counter value> + 1
  mov r1 0 ; r1 = 0
  jmp r0 ; return to unknown code
data:
.word 0xFFFF  ; will be overwritten with (RWX, init, end, data+1), i.e.
              ; a read-write capability to the counter value
.word 0       ; our private data: the current value of the counter
end: