uniformly use EVERPARSE_COPY_BUFFER_T

project-everest · Dec 5, 2023 · 1830514 · 1830514
1 parent e639747
commit 1830514
Show file tree

Hide file tree

Showing 6 changed files with 10 additions and 10 deletions.
diff --git a/src/3d/Ast.fst b/src/3d/Ast.fst
@@ -790,7 +790,7 @@ let puint8 = mk_prim_t "PUINT8"
 let tuint16 = mk_prim_t "UINT16"
 let tuint32 = mk_prim_t "UINT32"
 let tuint64 = mk_prim_t "UINT64"
-let tcopybuffer = mk_prim_t "COPY_BUFFER_T"
+let tcopybuffer = mk_prim_t "EVERPARSE_COPY_BUFFER_T"
 let tunknown = mk_prim_t "?"
 let unit_atomic_field rng = 
     let dummy_identifier = with_range (to_ident' "_empty_") rng in

diff --git a/src/3d/Binding.fst b/src/3d/Binding.fst
@@ -1151,7 +1151,7 @@ let check_atomic_field (env:env) (extend_scope: bool) (f:atomic_field)
         in
         let dest, dest_typ = check_ident env p.probe_dest in
         if not (eq_typ env dest_typ tcopybuffer)
-        then error (Printf.sprintf "Probe destination expression %s has type %s instead of COPY_BUFFER_T"
+        then error (Printf.sprintf "Probe destination expression %s has type %s instead of EVERPARSE_COPY_BUFFER_T"
                             (print_ident dest)
                             (print_typ dest_typ))
                             dest.range;
@@ -1963,7 +1963,7 @@ let initial_global_env () =
           parser_weak_kind = WeakKindStrongPrefix;
           parser_kind_nz = Some true
         });
-      ("COPY_BUFFER_T",
+      ("EVERPARSE_COPY_BUFFER_T",
         {
           may_fail = true;
           integral = None;

diff --git a/src/3d/Desugar.fst b/src/3d/Desugar.fst
@@ -166,7 +166,7 @@ let push_name (env:qenv) (name:string) : qenv =
 let prim_consts = [
   "unit"; "Bool"; "UINT8"; "UINT16"; "UINT32"; "UINT64";
   "UINT8BE"; "UINT16BE"; "UINT32BE"; "UINT64BE";
-  "field_id"; "PUINT8"; "COPY_BUFFER_T";
+  "field_id"; "PUINT8"; "EVERPARSE_COPY_BUFFER_T";
   "all_bytes"; "all_zeros";
   "is_range_okay";
   "void" ]

diff --git a/src/3d/prelude/EverParse3d.Interpreter.fst b/src/3d/prelude/EverParse3d.Interpreter.fst
@@ -26,7 +26,7 @@ open FStar.List.Tot
 
 inline_for_extraction
 noextract
-let ___COPY_BUFFER_T = CP.copy_buffer_t
+let ___EVERPARSE_COPY_BUFFER_T = CP.copy_buffer_t
 
 (* This module defines a strongly typed abstract syntax for an
    intermediate representation of 3D programs. This is the type `typ`.

diff --git a/src/3d/tests/FAILProbe.3d b/src/3d/tests/FAILProbe.3d
@@ -6,15 +6,15 @@ typedef struct _T {
 } T;
 
 entrypoint
-typedef struct _S(COPY_BUFFER_T dest) {
+typedef struct _S(EVERPARSE_COPY_BUFFER_T dest) {
   UINT8 tag;
   T *t probe (length = 8, destination = dest);
 } S;
 
 
 //Nested probing of the same buffer; should fail
 entrypoint
-typedef struct _R(COPY_BUFFER_T dest) {
+typedef struct _R(EVERPARSE_COPY_BUFFER_T dest) {
   UINT8 tag;
   S(dest) *s probe (length = 9, destination = dest);
 } R;
diff --git a/src/3d/tests/Probe.3d b/src/3d/tests/Probe.3d
@@ -6,20 +6,20 @@ typedef struct _T {
 } T;
 
 entrypoint
-typedef struct _S(COPY_BUFFER_T dest) {
+typedef struct _S(EVERPARSE_COPY_BUFFER_T dest) {
   UINT8 tag;
   T *t probe (length = 8, destination = dest);
 } S;
 
 entrypoint
-typedef struct _U(COPY_BUFFER_T destS, COPY_BUFFER_T destT) {
+typedef struct _U(EVERPARSE_COPY_BUFFER_T destS, EVERPARSE_COPY_BUFFER_T destT) {
   UINT8 tag;
   S(destT) *t probe (length = 9, destination = destS);
 } U;
 
 //reuse copy buffer, sequentially
 entrypoint
-typedef struct _V(COPY_BUFFER_T destS, COPY_BUFFER_T destT) {
+typedef struct _V(EVERPARSE_COPY_BUFFER_T destS, EVERPARSE_COPY_BUFFER_T destT) {
   UINT8 tag;
   S(destT) *s probe (length = 9, destination = destS);
   T *t probe (length = 8, destination = destT);