Add .ascii, .asciz

src/Assembly/Equality.v

@@ -273,6 +273,7 @@ Definition RawLine_beq (x y : RawLine) : bool
      | INSTR x, INSTR y => NormalInstruction_beq x y
      | ALIGN x, ALIGN y => String.eqb x y
      | DIRECTIVE x, DIRECTIVE y => String.eqb x y
+     | ASCII_ z x, ASCII_ z' y => Bool.eqb z z' && String.eqb x y
      | SECTION _, _
      | GLOBAL _, _
      | LABEL _, _
@@ -281,8 +282,9 @@ Definition RawLine_beq (x y : RawLine) : bool
      | ALIGN _, _
      | DEFAULT_REL, _
      | DIRECTIVE _, _
+     | ASCII_ _ _, _
        => false
-     end.
+     end%bool.
 Global Arguments RawLine_beq !_ !_ / .
 
 Infix "=?" := RawLine_beq : RawLine_scope.

src/Assembly/Parse.v

@@ -9,6 +9,7 @@ Require Import Crypto.Util.OptionList.
 Require Import Crypto.Util.Strings.Parse.Common.
 Require Import Crypto.Util.Strings.ParseArithmetic.
 Require Import Crypto.Util.Strings.String.
+Require Crypto.Util.Strings.Ascii.
 Require Import Crypto.Util.Strings.Show.
 Require Import Crypto.Util.Strings.Show.Enum.
 Require Import Crypto.Util.Listable.
@@ -177,6 +178,52 @@ Definition parse_OpPrefix_list : list (string * OpPrefix)
 Definition parse_OpPrefix : ParserAction OpPrefix
   := parse_strs parse_OpPrefix_list.
 
+Definition chars_to_escape_list : list (string * ascii)
+  := Eval vm_compute in
+      List.map
+        (fun '(name, char) => (String name EmptyString, char))
+        [("b", Ascii.Backspace)
+        ; ("f", Ascii.FormFeed)
+        ; ("n", Ascii.LF)
+        ; ("r", Ascii.CR)
+        ; ("t", Ascii.HorizontalTab)
+        ; ("v", Ascii.VerticalTab)
+        ; ("""", """")
+        ; ("'", "'")
+        ; ("\", "\")
+        ; ("0", Ascii.Null)
+        ]%char.
+Definition parse_escaped_char : ParserAction ascii :=
+  "\" ;;R
+    (parse_or_else
+        (parse_map ascii_of_N
+            (("x" ;;R parse_N_fixed_digits 16 false 2)
+            || (parse_N_fixed_digits 8 false 3)))
+        (parse_strs chars_to_escape_list)).
+
+Definition should_escape (ch : ascii) : bool
+  := (List.existsb (Ascii.eqb ch) (List.map snd chars_to_escape_list))
+      || negb (Ascii.is_printable ch).
+
+Definition escape_char (ch : ascii) : string :=
+  match List.find (fun '(escape_str, ch') => Ascii.eqb ch ch') chars_to_escape_list, should_escape ch with
+  | Some (escape_str, _), _ => "\" ++ escape_str
+  | None, true =>
+    let hex := Hex.show_N (Ascii.N_of_ascii ch) in
+    let hex := String.substring 2 (String.length hex) hex in
+    let hex := if (String.length hex <? 2)%nat then "0" ++ hex else hex in
+    let hex := if (String.length hex <? 2)%nat then "0" ++ hex else hex in
+    "\x" ++ hex
+  | None, false => String ch EmptyString
+  end%string.
+
+Definition escape_string (s : string) : string :=
+  String.concat "" (List.map escape_char (list_ascii_of_string s)).
+
+Definition unescape_string (s : string) : string :=
+  Option.value (finalize (parse_map string_of_list_ascii ( (parse_or_else parse_escaped_char (fun s => match s with EmptyString => [] | String char s => [(char, s)] end)* ))) s) s.
+
+
 (** assumes no leading nor trailing whitespace and no comment *)
 Definition parse_RawLine {opts : assembly_program_options} : ParserAction RawLine
   := fun s => (
@@ -194,6 +241,10 @@ Definition parse_RawLine {opts : assembly_program_options} : ParserAction RawLin
         then [(DEFAULT_REL, "")]
         else if String.endswith ":" s
         then [(LABEL (substring 0 (pred (String.length s)) s), "")]
+        else if (String.to_upper mnemonic =? ".ASCII") && (String.startswith """" args) && (String.endswith """" args)
+        then [(ASCII (unescape_string (String.substring 1 (String.length args - 2) args)), "")]
+        else if (String.to_upper mnemonic =? ".ASCIZ") && (String.startswith """" args) && (String.endswith """" args)
+        then [(ASCIZ (unescape_string (String.substring 1 (String.length args - 2) args)), "")]
         else if (s =? "")
         then [(EMPTY, "")]
         else if (List.find (String.eqb (String.to_lower mnemonic))
@@ -381,6 +432,8 @@ Global Instance show_RawLine : Show RawLine
         | EMPTY => ""
         | INSTR instr => show instr
         | DIRECTIVE s => s
+        | ASCII s => ".ascii """ ++ escape_string s ++ """"
+        | ASCIZ s => ".asciz """ ++ escape_string s ++ """"
         end.
 
 Global Instance show_Line : Show Line
@@ -627,6 +680,8 @@ Fixpoint get_initial_data (ls : Lines) : list (AccessSize * list Z)
             => get_initial_data ls
           | SECTION _
           | ALIGN _
+          | ASCII _
+          | ASCIZ _
              => []
           end
      end.

src/Assembly/Symbolic.v

@@ -4389,6 +4389,7 @@ Definition SymexRawLine {opts : symbolic_options_computed_opt} {descr:descriptio
   | EMPTY
   | LABEL _
   | DIRECTIVE _
+  | ASCII_ _ _
     => ret tt
   | INSTR instr
     => SymexNormalInstruction instr

src/Assembly/Syntax.v

@@ -281,7 +281,10 @@ Inductive RawLine :=
 | EMPTY
 | INSTR (instr : NormalInstruction)
 | DIRECTIVE (d : string)
+| ASCII_ (null_terminated : bool) (s : string)
 .
+Notation ASCII := (ASCII_ false).
+Notation ASCIZ := (ASCII_ true).
 Coercion INSTR : NormalInstruction >-> RawLine.
 Record Line := { indent : string ; rawline :> RawLine ; pre_comment_whitespace : string ; comment : option string ; line_number : N}.
 Definition Lines := list Line.

src/Assembly/WithBedrock/Semantics.v

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

src/Assembly/WithBedrock/SymbolicProofs.v

@@ -1374,12 +1374,12 @@ Lemma SymexLines_R {opts : symbolic_options_computed_opt} s m (HR : R s m) asm :
 Proof using Type.
   revert dependent m; revert dependent s; induction asm; cbn [SymexLines DenoteLines]; intros.
   { inversion H; subst; eauto. }
-  destruct a.
-  rewrite unfold_bind in H; destruct_one_match_hyp; inversion_ErrorT.
+  destruct_head' Line.
+  rewrite unfold_bind in *; destruct_one_match_hyp; inversion_ErrorT.
   cbv [SymexLine SymexRawLine DenoteLine DenoteRawLine ret err Crypto.Util.Option.bind] in *; cbn in *.
-  destruct_one_match_hyp; inversion_ErrorT; subst; eauto; destruct v.
+  destruct_one_match_hyp; inversion_ErrorT; subst; eauto; destruct_head'_prod.
   eapply SymexNornalInstruction_R in E; eauto. destruct E as (m1&Hm1&Rm1&?). rewrite Hm1.
-  eapply IHasm in H; eauto. destruct H as (?&?&?&?). eauto 9.
+  eapply IHasm in H; eauto. destruct H as (?&?&?&?). break_innermost_match; eauto 9.
 Qed.
 End WithCtx1'.
 End WithFrame.

src/Util/Strings/Ascii.v

@@ -11,11 +11,14 @@ Local Open Scope char_scope.
 Example Null := "000".
 Example Backspace := "008".
 Example Tab := "009".
+Example HorizontalTab := "009".
 Example LF := "010".
+Example NewLine := "010".
+Example VerticalTab := "011".
 Example NewPage := "012".
+Example FormFeed := "012".
 Example CR := "013".
 Example Escape := "027".
-Example NewLine := "010".
 
 Local Coercion N_of_ascii : ascii >-> N.
 Definition ltb (x y : ascii) : bool := N.ltb x y.
@@ -39,3 +42,6 @@ Definition to_upper (ch : ascii) : ascii
 
 Definition is_whitespace (x : ascii) : bool
   := ((x =? " ") || (x =? NewPage) || (x =? LF) || (x =? CR) || (x =? Tab))%char%bool.
+
+Definition is_printable (x : ascii) : bool
+  := (" " <=? x) && (x <=? "~").

src/Util/Strings/ParseArithmetic.v

@@ -64,7 +64,6 @@ Definition parse_digits_gen_step (base : N) : ParserAction N
                              (String (ascii_of_N (v - 10 + N_of_ascii "a")) "", v)])
            (List.map N.of_nat (List.seq 0 (N.to_nat base))))).
 
-
 (*
 Definition parse_oct_digits : ParserAction (list N)
   := Eval cbv -[ParserAction parse_alt_gen parse_impossible parse_str parse_star] in
@@ -92,6 +91,21 @@ Local Coercion inject_Z : Z >-> Q.
 Definition parse_N_digits (base : N) (first_digit_numeric : bool) : ParserAction N
   := (parse_map (digits_to_N base) ((parse_digits_gen_step (if first_digit_numeric then N.min 10 base else base);;->{cons}(parse_digits_gen_step base)* ))).
 
+Definition parse_N_fixed_digits (base : N) (first_digit_numeric : bool) (n : nat) : ParserAction N := (
+  let parse_first_digit := parse_digits_gen_step (if first_digit_numeric then N.min 10 base else base) in
+  let parse_nil := parse_map (fun _ => nil) "" in
+  parse_map (digits_to_N base)
+    match n with
+    | O => parse_nil
+    | S n =>
+        fold_right (fun p ps => p ;;->{cons} ps)
+          parse_nil
+          (parse_first_digit :: List.repeat (parse_digits_gen_step base) n)
+    end)%parse.
+
+Notation parse_oct_char := (parse_digits_gen_step 8 false 1).
+Notation parse_hex_char := (parse_digits_gen_step 16 false 1).
+
 Definition parse_num_gen {P P'} (allow_neg : bool) (base : N) (parse_prefix : option (ParserAction P)) (parse_postfix : option (ParserAction P'))  : ParserAction Q
   := (let parse_E_exponent
         := (("e" || "E") ;;->{ fun _ v => Qpower 10 v }