x86-64 assembly

Micro-x86-64

Micro-x86-64 is a valid subset of x86-64. Hence, micro-x86-64 files can be passed to as.

Syntax of micro-x86-64

TODO

Specification

TODO

spec ::=  "#@" "assume"     term
        | "#@" "assert"     term
        | "#@" "invariant"  term

+ Multiline comments: "/*@" "assume" term "*/", …

term ::= identifier
       | "true" | "false"
       | 1 | 2 | …
       | rax | eax | … | rbx | …
       | term "binop" term
       | "let" identifier "=" term "in" term
       | "if" term "then" term "else term

binop ::=
        | "/\" | "&&"
        | "\/" | "||"
        | "->"
        | "=" | "<" | ">" | ">=" | "<="
        | "+" | "-" | "*" | "/"

Note that you must explicitly use the mach.asm.X86 module in your code (which should be the case once you actually prove things, but not necessarily when you initially set up a project), such as with the line:

#@ use mach.asm.X86

or you will get a compilation error complaining that the mach.asm.X86 module is not loaded.

Example

#@ use int.Int
#@ use mach.asm.X86

    .text
    .globl  isqrt

isqrt:
#@ assume 0 < rdi < i32_max
        xorq    %rax, %rax
        movq    $1,  %rcx
        jmp     T1
L1:     incq    %rax
        leaq    1(%rcx, %rax, 2), %rcx
T1:
#@ invariant 0 <= rax
#@ invariant rax * rax <= rdi < i32_max
#@ invariant rcx = (rax + 1) * (rax + 1)
        cmpq    %rdi, %rcx
        jle     L1
#@ assert let a = rax in a * a <= rdi < (a+1)*(a+1)
        ret

Limitations

TODO