From 9cfa575245a0427a0d35504086de182bd80b7df8 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 11 Jan 2019 21:00:36 +0000
Subject: Updates for sail-arm release

We want to ensure that no_devices.sail and devices.sail have the same
effect footprint, because with a snapshot-type release in sail-arm, we
can't rebuild the spec with asl_to_sail every time we switch from
running elf binaries to booting OS's. This commit allows registers to
have arbitrary effects, so registers that are really representing
memory-mapped devices don't have to have the wmem/rmem effect.
---
 src/parser.mly | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'src/parser.mly')

diff --git a/src/parser.mly b/src/parser.mly
index 3b42d498..68720048 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1362,7 +1362,11 @@ val_spec_def:
 
 register_def:
   | Register id Colon typ
-    { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos }
+    { let rreg = mk_typ (ATyp_set [mk_effect BE_rreg $startpos($1) $endpos($1)]) $startpos($1) $endpos($1) in
+      let wreg = mk_typ (ATyp_set [mk_effect BE_wreg $startpos($1) $endpos($1)]) $startpos($1) $endpos($1) in
+      mk_reg_dec (DEC_reg (rreg, wreg, $4, $2)) $startpos $endpos }
+  | Register effect_set effect_set id Colon typ
+    { mk_reg_dec (DEC_reg ($2, $3, $6, $4)) $startpos $endpos }
   | Register Configuration id Colon typ Eq exp
     { mk_reg_dec (DEC_config ($3, $5, $7)) $startpos $endpos }
 
-- 
cgit v1.2.3