Fil-C on Nix

Filnix wiki

the formal campaign

rocq/backend/AsmTerm.v

Asm.v's lines from the terms asm.pl prints them from: the decoder of what nanofilasm − termsFILE writes, one line term each. It is how the printer is checked against asm.pl before any pass that builds lines exists, and how a later pass's lines are compared with the Prolog compiler's, term by term.

A term that asm.pl would refuse (bad_asm_line) decodes to nothing.

From Stdlib Require Import String ZArith List Ascii Bool
From Nanofil Require Import Term
From Backend Require Import Asm
Import ListNotations
Open Scope string_scope

Option binding: let* x ≔ e in b is b with x the value of e, or nothing when e has none.

18Notation 'let*' x ':=' e 'in' b ≔ match e with Somex ⇒ b | None ⇒ None end (at level 200 , x pattern , e at level 200 , b at level 200)

f of every element, or nothing if any has none.

23Fixpoint all_someA B : Type f : A → optionB xs : listA : optionlistB ≔
match xs with
[ ]
⇒
Some[ ]
x :: xs′
⇒
let* y ≔ fx in
let* ys ≔ all_somef xs′ in
Somey :: ys

A literal: an integer or an atom.

30Definition dlitt : term : optionlit ≔
match t with
TIntn
⇒
SomeLIntn
TAtoma
⇒
SomeLSyma
_
⇒
None

The name of an atom.

38Definition dnamet : term : optionstring ≔
match t with
TAtoma
⇒
Somea
_
⇒
None

String equality, written as Prolog's ==. The decoders compare names with it rather than match string patterns, which extract to a decision tree over the bits of every character.

47Notation a == b ≔ String.eqba b (at level 70)

An expression: A + B or a literal.

50Fixpoint dexprt : term : optionexpr ≔
match t with
TAppf a; b
⇒
f == "+"
→
let* a′ ≔ dexpra in
let* b′ ≔ dexprb in
SomeEAdda′ b′
else
None
_
⇒
let* a ≔ dlitt in
SomeELita
58Fixpoint doperandt : term : optionoperand ≔
match t with
TAppf x
⇒
f == "imm"
→
let* e ≔ dexprx in
SomeOImme
f == "reg"
→
let* r ≔ dnamex in
SomeORegr
f == "rip"
→
let* e ≔ dexprx in
SomeORipe
f == "gotpcrel"
→
let* s ≔ dlitx in
SomeOGotpcrels
f == "plt"
→
let* s ≔ dlitx in
SomeOPlts
f == "gottpoff"
→
let* s ≔ dlitx in
SomeOGottpoffs
f == "fs"
→
let* o ≔ doperandx in
SomeOFso
f == "sym"
→
let* e ≔ dexprx in
SomeOSyme
f == "ind"
→
let* o ≔ doperandx in
SomeOIndo
else
None
TAppf d; b
⇒
f == "mem"
→
let* d′ ≔ dlitd in
let* b′ ≔ dnameb in
SomeOMemd′ b′
else
None
TAppf d; b; i
⇒
f == "mem"
→
let* d′ ≔ dlitd in
let* b′ ≔ dnameb in
let* i′ ≔ dnamei in
SomeOMemIndexd′ b′ i′
else
None
_
⇒
None

One byte of an ascii list: a one-character atom of a code below 256.

84Definition dbytet : term : optionascii ≔
let* n ≔ char_codet in
n <? 256%Z
→
Someascii_of_natZ.to_natn
else
None
88Definition dsectiont : term : optionsection ≔
match t with
TAtoma
⇒
a == "text"
→
SomeSText
a == "data"
→
SomeSData
a == "rodata"
→
SomeSRodata
a == "bss"
→
SomeSBss
a == "tbss"
→
SomeSTbss
a == "data_rel_ro"
→
SomeSDataRelRo
a == "note_gnu_stack"
→
SomeSNoteGnuStack
else
None
TAppf TAtomkind; prio
⇒
f == "init"
→
let* ctor ≔
kind == "ctor"
→
Sometrue
kind == "dtor"
→
Somefalse
else
None
in
let* p ≔ dlitprio in
match p with
LSyms
⇒
s == "none"
→
SomeSInitctor None
else
SomeSInitctor Somep
LInt_
⇒
SomeSInitctor Somep
else
None
_
⇒
None
113Definition ddirectivet : term : optiondirective ≔
match t with
TAppf x
⇒
f == "section"
→
let* s ≔ dsectionx in
SomeDSections
f == "p2align"
→
let* n ≔ dlitx in
SomeDP2alignn
f == "balign"
→
let* n ≔ dlitx in
SomeDBalignn
f == "globl"
→
let* s ≔ dlitx in
SomeDGlobls
f == "weak"
→
let* s ≔ dlitx in
SomeDWeaks
f == "hidden"
→
let* s ≔ dlitx in
SomeDHiddens
f == "size"
→
let* s ≔ dlitx in
SomeDSizes
f == "quad"
→
let* e ≔ dexprx in
SomeDQuade
f == "long"
→
let* n ≔ dlitx in
SomeDLongn
f == "int"
→
let* n ≔ dlitx in
SomeDIntn
f == "short"
→
let* n ≔ dlitx in
SomeDShortn
f == "zero"
→
let* n ≔ dlitx in
SomeDZeron
f == "asciz"
→
let* a ≔ dlitx in
SomeDAsciza
f == "byte"
→
match x with
TListn :: ns
⇒
let* n′ ≔ dlitn in
let* ns′ ≔ all_somedlit ns in
SomeDByten′ ns′
_
⇒
None
f == "ascii"
→
match x with
TListcs
⇒
let* cs′ ≔ all_somedbyte cs in
SomeDAsciics′
_
⇒
None
else
None
TAppf x; y
⇒
f == "type"
→
let* s ≔ dlitx in
let* k ≔ dlity in
SomeDTypes k
f == "size"
→
let* s ≔ dlitx in
let* n ≔ dlity in
SomeDSizeOfs n
f == "set"
→
let* s ≔ dlitx in
let* e ≔ dexpry in
SomeDSets e
else
None
_
⇒
None
149Definition dfixedt : term : optionfixed ≔
let* a ≔ dnamet in
a == "cpuid"
→
SomeCpuid
a == "xgetbv"
→
SomeXgetbv
a == "rdtsc"
→
SomeRdtsc
a == "rdtscp"
→
SomeRdtscp
a == "lfence"
→
SomeLfence
a == "sfence"
→
SomeSfence
a == "pause"
→
SomePause
else
None

The instruction ins(Op, Suffix, Operands), if t is one.

161Definition dinst : term : optionline ≔
match t with
TAppf op; suffix; TListos
⇒
f == "ins"
→
let* op′ ≔ dlitop in
let* s ≔ dnamesuffix in
let* os′ ≔ all_somedoperand os in
Some
Inslit_textop′
s == "none"
→
None
else
Somes
os′
else
None
_
⇒
None

A line. The cases are disjoint: no directive is named label, asm_fixed or ins.

175Definition dlinet : term : optionline ≔
match t with
TAppf x
⇒
f == "label"
→
let* s ≔ dlitx in
SomeLabels
f == "asm_fixed"
→
let* m ≔ dfixedx in
SomeFixedm
else
let* d ≔ ddirectivet in
SomeDird
TAppf _; _; _
⇒
dinst
_
⇒
let* d ≔ ddirectivet in
SomeDird
185Example decode_mov: dlineTApp"ins" TAtom"mov"; TAtom"q"; TListTApp"mem" TInt−8; TAtom"rbp"; TApp"reg" TAtom"rax" = SomeIns"mov" Some"q" OMemLInt−8 "rbp"; OReg"rax"
Proof 1 step Qed
reflexivity