Parse various directives starting with . in intel syntax

JasonGross · Mar 5, 2025 · a0cc08a · a0cc08a
1 parent ee8fca9
commit a0cc08a
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 3 deletions.
diff --git a/src/Assembly/Parse.v b/src/Assembly/Parse.v
@@ -161,18 +161,32 @@ Definition parse_RawLine : ParserAction RawLine
         (* get the first space-separated opcode *)
         let '(mnemonic, args) := String.take_while_drop_while (fun ch => negb (Ascii.is_whitespace ch)) s in
         let args := String.trim args in
-        if (String.to_upper mnemonic =? "SECTION")
+        if (String.to_upper mnemonic =? "SECTION") || (String.to_upper mnemonic =? ".SECTION")
         then [(SECTION args, "")]
-        else if (String.to_upper mnemonic =? "GLOBAL")
+        else if (String.to_upper mnemonic =? "GLOBAL") || (String.to_upper mnemonic =? ".GLOBAL") || (String.to_upper mnemonic =? ".GLOBL")
         then [(GLOBAL args, "")]
-        else if (String.to_upper mnemonic =? "ALIGN")
+        else if (String.to_upper mnemonic =? "ALIGN") || (String.to_upper mnemonic =? ".ALIGN")
         then [(ALIGN args, "")]
         else if (String.to_upper mnemonic =? "DEFAULT") && (String.to_upper args =? "REL")
         then [(DEFAULT_REL, "")]
         else if String.endswith ":" s
         then [(LABEL (substring 0 (pred (String.length s)) s), "")]
         else if (s =? "")
         then [(EMPTY, "")]
+        else if (List.find (String.eqb (String.to_lower s))
+          [".cfi_def_cfa_offset"
+           ; ".cfi_endproc"
+           ; ".cfi_offset"
+           ; ".cfi_startproc"
+           ; ".file"
+           ; ".ident"
+           ; ".intel_syntax"
+           ; ".loc"
+           ; ".size"
+           ; ".text"
+           ; ".type"
+           ])
+        then [(DIRECTIVE s, "")]
         else let parsed_prefix := (parse_OpPrefix ;;L ε) mnemonic in
              List.flat_map
                (fun '(parsed_prefix, mnemonic, args)

diff --git a/src/Assembly/Syntax.v b/src/Assembly/Syntax.v
@@ -205,6 +205,7 @@ Inductive RawLine :=
 | DEFAULT_REL
 | EMPTY
 | INSTR (instr : NormalInstruction)
+| DIRECTIVE (d : string)
 .
 Coercion INSTR : NormalInstruction >-> RawLine.
 Record Line := { indent : string ; rawline :> RawLine ; pre_comment_whitespace : string ; comment : option string ; line_number : N}.