Parse various directives starting with . in intel syntax

mit-plv · Mar 5, 2025 · 4160d01 · 4160d01
1 parent ee8fca9
commit 4160d01
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 6 deletions.
diff --git a/src/Assembly/Equality.v b/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 !_ !_ / .

diff --git a/src/Assembly/Parse.v b/src/Assembly/Parse.v
@@ -156,23 +156,37 @@ Definition parse_OpPrefix : ParserAction OpPrefix
 
 (** assumes no leading nor trailing whitespace and no comment *)
 Definition parse_RawLine : ParserAction RawLine
-  := fun s
-     => let s := String.trim s in
+  := fun s => (
+        let s := String.trim s in
         (* 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)
@@ -194,7 +208,7 @@ Definition parse_RawLine : ParserAction RawLine
                           let args := String.trim args in
                           (Some parsed_prefix, mnemonic, args))
                       parsed_prefix
-               end.
+               end)%bool.
 
 Definition parse_Line (line_num : N) : ParserAction Line
   := fun s
@@ -300,6 +314,7 @@ Global Instance show_RawLine : Show RawLine
         | LABEL name => name ++ ":"
         | EMPTY => ""
         | INSTR instr => show instr
+        | DIRECTIVE s => s
         end.
 
 Global Instance show_Line : Show Line

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

diff --git a/src/Assembly/WithBedrock/Semantics.v b/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