Parse various directives starting with . in intel syntax

Author: JasonGross

src/Assembly/Equality.v

@@ -257,13 +257,15 @@ Definition RawLine_beq (x y : RawLine) : bool
      | DEFAULT_REL, DEFAULT_REL => true
      | INSTR x, INSTR y => NormalInstruction_beq x y
      | ALIGN x, ALIGN y => String.eqb x y
+     | DIRECTIVE x, DIRECTIVE y => String.eqb x y
      | SECTION _, _
      | GLOBAL _, _
      | LABEL _, _
      | EMPTY, _
      | INSTR _, _
      | ALIGN _, _
      | DEFAULT_REL, _
+     | DIRECTIVE _, _
        => false
      end.
 Global Arguments RawLine_beq !_ !_ / .

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)

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}.

src/Assembly/WithBedrock/Semantics.v

@@ -422,6 +422,7 @@ Definition DenoteRawLine (st : machine_state) (rawline : RawLine) : option machi
   match rawline with
   | EMPTY
   | LABEL _
+  | DIRECTIVE _
     => Some st
   | INSTR instr
     => DenoteNormalInstruction st instr