From f21a783181e75813751e2bedbf74b6dc66c8cec2 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 5 Mar 2025 12:25:59 -0800
Subject: [PATCH] Parse various directives starting with . in intel syntax
 (#2030)

---
 src/Assembly/Equality.v              |  2 ++
 src/Assembly/Parse.v                 | 27 +++++++++++++++++++++------
 src/Assembly/Symbolic.v              |  1 +
 src/Assembly/Syntax.v                |  1 +
 src/Assembly/WithBedrock/Semantics.v |  1 +
 5 files changed, 26 insertions(+), 6 deletions(-)

diff --git a/src/Assembly/Equality.v b/src/Assembly/Equality.v
index 336da900e8..baceefaf13 100644
--- a/src/Assembly/Equality.v
+++ b/src/Assembly/Equality.v
@@ -257,6 +257,7 @@ 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 _, _
@@ -264,6 +265,7 @@ Definition RawLine_beq (x y : RawLine) : bool
      | INSTR _, _
      | ALIGN _, _
      | DEFAULT_REL, _
+     | DIRECTIVE _, _
        => false
      end.
 Global Arguments RawLine_beq !_ !_ / .
diff --git a/src/Assembly/Parse.v b/src/Assembly/Parse.v
index 4bf046fd20..22074c6056 100644
--- a/src/Assembly/Parse.v
+++ b/src/Assembly/Parse.v
@@ -161,16 +161,16 @@ 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, "")]
@@ -178,6 +178,20 @@ Definition parse_RawLine : ParserAction RawLine
         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)
@@ -199,7 +213,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
@@ -312,6 +326,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/Symbolic.v b/src/Assembly/Symbolic.v
index f2a2c93cc3..5849e9547a 100644
--- a/src/Assembly/Symbolic.v
+++ b/src/Assembly/Symbolic.v
@@ -4395,6 +4395,7 @@ Definition SymexRawLine {opts : symbolic_options_computed_opt} {descr:descriptio
   match rawline with
   | EMPTY
   | LABEL _
+  | DIRECTIVE _
     => ret tt
   | INSTR instr
     => SymexNormalInstruction instr
diff --git a/src/Assembly/Syntax.v b/src/Assembly/Syntax.v
index 73dc6d3afc..43eb5b3990 100644
--- a/src/Assembly/Syntax.v
+++ b/src/Assembly/Syntax.v
@@ -269,6 +269,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
index 23cd75aa9d..d8f6ef024e 100644
--- a/src/Assembly/WithBedrock/Semantics.v
+++ b/src/Assembly/WithBedrock/Semantics.v
@@ -456,6 +456,7 @@ Definition DenoteRawLine (st : machine_state) (rawline : RawLine) : option machi
   match rawline with
   | EMPTY
   | LABEL _
+  | DIRECTIVE _
     => Some st
   | INSTR instr
     => DenoteNormalInstruction st instr