From 29c1d50429847b85de4713a561762858dcd3b0ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Mar 2025 14:30:40 -0700 Subject: [PATCH] Add .ascii, .asciz --- src/Assembly/Equality.v | 4 +- src/Assembly/Parse.v | 55 +++++++++++++++++++++++ src/Assembly/Symbolic.v | 1 + src/Assembly/Syntax.v | 3 ++ src/Assembly/WithBedrock/Semantics.v | 1 + src/Assembly/WithBedrock/SymbolicProofs.v | 8 ++-- src/Util/Strings/Ascii.v | 8 +++- src/Util/Strings/ParseArithmetic.v | 16 ++++++- 8 files changed, 89 insertions(+), 7 deletions(-) diff --git a/src/Assembly/Equality.v b/src/Assembly/Equality.v index 9a44941306..8ae8893c04 100644 --- a/src/Assembly/Equality.v +++ b/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. diff --git a/src/Assembly/Parse.v b/src/Assembly/Parse.v index f8e60d6769..8f05706478 100644 --- a/src/Assembly/Parse.v +++ b/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 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. diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v index 171aefcc21..9d5a7dcb74 100644 --- a/src/Assembly/Symbolic.v +++ b/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 diff --git a/src/Assembly/Syntax.v b/src/Assembly/Syntax.v index 8194fa0d35..a09272183f 100644 --- a/src/Assembly/Syntax.v +++ b/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. diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v index ba1b2e5f95..5eedb98ea0 100644 --- a/src/Assembly/WithBedrock/Semantics.v +++ b/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 diff --git a/src/Assembly/WithBedrock/SymbolicProofs.v b/src/Assembly/WithBedrock/SymbolicProofs.v index a367e5b74c..abfc5af80c 100644 --- a/src/Assembly/WithBedrock/SymbolicProofs.v +++ b/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. diff --git a/src/Util/Strings/Ascii.v b/src/Util/Strings/Ascii.v index b969dd9c87..2bbfa03343 100644 --- a/src/Util/Strings/Ascii.v +++ b/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 <=? "~"). diff --git a/src/Util/Strings/ParseArithmetic.v b/src/Util/Strings/ParseArithmetic.v index be571d1bc4..a0e15b8488 100644 --- a/src/Util/Strings/ParseArithmetic.v +++ b/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 }