Coq: The world’s best macro assembler? (PDF)
つーのがありまして。
Abstract
We describe a Coq formalization of a subset of the x86 architecture.
One emphasis of the model is brevity: using dependent types, type
classes and notation we give the x86 semantics a makeover that
counters its reputation for baroqueness. We model bits, bytes, and
memory concretely using functions that can be computed inside
Coq itself; concrete representations are mapped across to math-
ematical objects in the SSREFLECT library (naturals, and inte-
gers modulo 2n) to prove theorems. Finally, we use notation to
support conventional assembly code syntax inside Coq, including
lexically-scoped labels. Ordinary Coq definitions serve as a pow-
erful “macro” feature for everything from simple conditionals and
loops to stack-allocated local variables and procedures with param-
eters. Assembly code can be assembled within Coq, producing a
sequence of hex bytes. The assembler enjoys a correctness theo-
rem relating machine code in memory to a separation-logic formula
suitable for program verification.
で、書いたプログラム例がこう
Definition call_cdecl3 f arg1 arg2 arg3 :=
PUSH arg3;; PUSH arg2;; PUSH arg1;;
CALL f;; ADD ESP, 12.
Definition main (printfSlot: DWORD) :=
(* Argument in EBX *)
letproc fact :=
MOV EAX, 1;;
MOV ECX, 1;;
(* while ECX <= EBX *)
while (CMP ECX, EBX) CC_LE true (
MUL ECX;; (* Multiply EAX by ECX *)
INC ECX
)
in
LOCAL format;
MOV EBX, 10;; callproc fact;;
MOV EDI, printfSlot;;
call_cdecl3 [EDI] format EBX EAX;;
MOV EBX, 12;; callproc fact;;
MOV EDI, printfSlot;;
call_cdecl3 [EDI] format EBX EAX;;
RET 0;;
format:;;
ds "Factorial of %d is %d";; db #10;; db #0.
Compute bytesToHex
(assemble #x"C0000004" (main #x"C0000000")).
パッと見た印象だけだと、昔こんな記述のできる
マクロアセンブラあったよね。
という感じなんだけど、
Coq でというところにありがたみがあるんだろうなあ。