From 347183af9041e4dbd20390cb9c3e42b2aeafc065 Mon Sep 17 00:00:00 2001
From: MingZhu Yan <yanmingzhu@iscas.ac.cn>
Date: Wed, 22 Jan 2025 14:36:18 +0800
Subject: [PATCH] Support empty bitfield

---
 src/lib/parser.mly                      | 10 ++++++++--
 test/lem/run_tests.py                   |  1 +
 test/typecheck/pass/bitfield_empty.sail |  7 +++++++
 3 files changed, 16 insertions(+), 2 deletions(-)
 create mode 100644 test/typecheck/pass/bitfield_empty.sail

diff --git a/src/lib/parser.mly b/src/lib/parser.mly
index efd27738e..0f1a80b2f 100644
--- a/src/lib/parser.mly
+++ b/src/lib/parser.mly
@@ -975,6 +975,12 @@ r_def_body:
   | r_id_def Comma r_def_body
     { $1 :: $3 }
 
+bitfield_def_body:
+  | Lcurly Rcurly
+    { [] }
+  | Lcurly r_def_body Rcurly
+    { $2 }
+
 param_kopt:
   | kid Colon kind
     { KOpt_aux (KOpt_kind (None, [$1], Some $3, None), loc $startpos $endpos) }
@@ -1017,8 +1023,8 @@ type_def:
     { mk_td (TD_variant ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5)) $startpos $endpos }
   | Union id typaram Eq Lcurly type_unions Rcurly
     { mk_td (TD_variant ($2, $3, $6)) $startpos $endpos }
-  | Bitfield id Colon typ Eq Lcurly r_def_body Rcurly
-    { mk_td (TD_bitfield ($2, $4, $7)) $startpos $endpos }
+  | Bitfield id Colon typ Eq bitfield_def_body
+    { mk_td (TD_bitfield ($2, $4, $6)) $startpos $endpos }
 
 enum_functions:
   | id MinusGt typ Comma enum_functions
diff --git a/test/lem/run_tests.py b/test/lem/run_tests.py
index 0e2744f89..36ba08e8c 100755
--- a/test/lem/run_tests.py
+++ b/test/lem/run_tests.py
@@ -52,6 +52,7 @@
     'bitfield_exponential',
     'bitfield_abs',
     'bitfield_mod',
+    'bitfield_empty',
     # Abstract types not implemented for Lem yet
     'abstract_bool',
     'abstract_bool2',
diff --git a/test/typecheck/pass/bitfield_empty.sail b/test/typecheck/pass/bitfield_empty.sail
new file mode 100644
index 000000000..ef7515ed3
--- /dev/null
+++ b/test/typecheck/pass/bitfield_empty.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <prelude.sail>
+
+type xlen : Int = 2 ^ 2
+
+bitfield foo : bits(xlen) = { }