Update regfp.sail with ifetch changes from poly_mapping branch

However, use an ifdef to make sure the ifetch changes only appear for the ARM spec, because
otherwise the generated lem for RMEM will break.

1 files changed, 27 insertions, 0 deletions

diff --git a/lib/regfp.sail b/lib/regfp.sail
index 070ff524..231ccf6e 100644
--- a/lib/regfp.sail
+++ b/lib/regfp.sail
@@ -31,6 +31,7 @@ union diafp = {
   DIAFP_reg : regfp
 }
 
+$ifdef ARM_SPEC
 enum read_kind = {
   Read_plain,
   Read_reserve,
@@ -38,6 +39,7 @@ enum read_kind = {
   Read_exclusive,
   Read_exclusive_acquire,
   Read_stream,
+  Read_ifetch,
   Read_RISCV_acquire,
   Read_RISCV_strong_acquire,
   Read_RISCV_reserved,
@@ -45,6 +47,22 @@ enum read_kind = {
   Read_RISCV_reserved_strong_acquire,
   Read_X86_locked
 }
+$else
+enum read_kind = {
+  Read_plain,
+  Read_reserve,
+  Read_acquire,
+  Read_exclusive,
+  Read_exclusive_acquire,
+  Read_stream,
+  Read_RISCV_acquire,
+  Read_RISCV_strong_acquire,
+  Read_RISCV_reserved,
+  Read_RISCV_reserved_acquire,
+  Read_RISCV_reserved_strong_acquire,
+  Read_X86_locked
+}
+$endif
 
 enum write_kind = {
   Write_plain,
@@ -142,6 +160,15 @@ val __barrier
   = { ocaml: "Platform.barrier", c: "platform_barrier", _: "barrier" }
   : barrier_kind -> unit effect {barr}
 
+val __branch_announce
+  = { ocaml: "Platform.branch_announce", c: "platform_branch_announce", _ : "branch_announce" }
+  : forall (constant 'addrsize : Int), 'addrsize in {32, 64}.
+  (int('addrsize), bits('addrsize)) -> unit
+
+val __cache_maintenance
+  = { ocaml: "Platform.cache_maintenance", c: "platform_cache_maintenance", _ : "cache_maintenance" }
+  : forall (constant 'addrsize : Int), 'addrsize in {32, 64}.
+  (cache_op_kind, int('addrsize), bits('addrsize)) -> unit
 
 /*
 val __write : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {eamem,wmv}