From 25a8a48142cc715c55f11fc80cf3dad6bec1b71d Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 26 Dec 2018 20:42:54 +0000
Subject: More cleanup

Remove unused name schemes and DEF_kind
---
 src/parser.mly | 26 +++++++++++---------------
 1 file changed, 11 insertions(+), 15 deletions(-)

(limited to 'src/parser.mly')

diff --git a/src/parser.mly b/src/parser.mly
index 66902953..ef30991f 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -134,7 +134,6 @@ let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown))
 let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
 let mk_tannot typq typ n m = Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ), loc n m)
 let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown)
-let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown)
 
 let mk_typq kopts nc n m = TypQ_aux (TypQ_tq (List.map qi_id_of_kopt kopts @ nc), loc n m)
 
@@ -181,7 +180,7 @@ let rec desugar_rchain chain s e =
 %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op Where
 %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool Cast
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
-%token Undefined Union Newtype With Val Constant Constraint Throw Try Catch Exit Bitfield
+%token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Mutual Var Ref Configuration
 
@@ -1170,21 +1169,21 @@ type_def:
   | Typedef id Colon kind Eq typ
     { mk_td (TD_abbrev ($2, mk_typqn, $4, $6)) $startpos $endpos }
   | Struct id Eq Lcurly struct_fields Rcurly
-    { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
+    { mk_td (TD_record ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
   | Struct id typaram Eq Lcurly struct_fields Rcurly
-    { mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+    { mk_td (TD_record ($2, $3, $6, false)) $startpos $endpos }
   | Enum id Eq enum_bar
-    { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos }
+    { mk_td (TD_enum ($2, $4, false)) $startpos $endpos }
   | Enum id Eq Lcurly enum Rcurly
-    { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos }
+    { mk_td (TD_enum ($2, $5, false)) $startpos $endpos }
   | Newtype id Eq type_union
-    { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos }
+    { mk_td (TD_variant ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), [$4], false)) $startpos $endpos }
   | Newtype id typaram Eq type_union
-    { mk_td (TD_variant ($2, mk_namesectn, $3, [$5], false)) $startpos $endpos }
+    { mk_td (TD_variant ($2, $3, [$5], false)) $startpos $endpos }
   | Union id Eq Lcurly type_unions Rcurly
-    { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
+    { mk_td (TD_variant ($2, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
   | Union id typaram Eq Lcurly type_unions Rcurly
-    { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+    { mk_td (TD_variant ($2, $3, $6, false)) $startpos $endpos }
   | Bitfield id Colon typ Eq Lcurly r_def_body Rcurly
     { mk_td (TD_bitfield ($2, $4, $7)) $startpos $endpos }
 
@@ -1375,9 +1374,9 @@ default_def:
 
 scattered_def:
   | Union id typaram
-    { mk_sd (SD_variant($2, mk_namesectn, $3)) $startpos $endpos }
+    { mk_sd (SD_variant($2, $3)) $startpos $endpos }
   | Union id
-    { mk_sd (SD_variant($2, mk_namesectn, mk_typqn)) $startpos $endpos }
+    { mk_sd (SD_variant($2, mk_typqn)) $startpos $endpos }
   | Function_ id
     { mk_sd (SD_function(mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos }
   | Mapping id
@@ -1423,9 +1422,6 @@ def:
     { DEF_scattered (mk_sd (SD_end $2) $startpos $endpos) }
   | default_def
     { DEF_default $1 }
-  | Constant id Eq typ
-    { DEF_kind (KD_aux (KD_nabbrev (K_aux (K_int, loc $startpos($1) $endpos($1)), $2, mk_namesectn, $4),
-			loc $startpos $endpos)) }
   | Mutual Lcurly fun_def_list Rcurly
     { DEF_internal_mutrec $3 }
   | Pragma
-- 
cgit v1.2.3


From eb837a0ae70ef5dc8a2a3a28d59a736c57a952b3 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 8 Jan 2019 17:08:34 +0000
Subject: Improvements for v85

---
 src/parser.mly | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/parser.mly')

diff --git a/src/parser.mly b/src/parser.mly
index ef30991f..3b42d498 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -177,7 +177,7 @@ let rec desugar_rchain chain s e =
 
 /*Terminals with no content*/
 
-%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op Where
+%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
 %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Bool Cast
 %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
 %token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
-- 
cgit v1.2.3


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


From 44e35e2384824f8f3b3cc65a61bbb76e08a6422c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 8 Feb 2019 17:52:42 +0000
Subject: Allow internal AST nodes in input when -dmagic_hash is on

---
 src/parser.mly | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src/parser.mly')

diff --git a/src/parser.mly b/src/parser.mly
index 7540d1f4..cbbc41e3 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -183,6 +183,7 @@ let rec desugar_rchain chain s e =
 %token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 %token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure
+%token InternalPLet InternalReturn
 
 %nonassoc Then
 %nonassoc Else
@@ -806,6 +807,12 @@ exp:
   | While exp Do exp
     { mk_exp (E_loop (While, $2, $4)) $startpos $endpos }
 
+  /* Debugging only, will be rejected in initial_check if debugging isn't on */
+  | InternalPLet pat Eq exp In exp
+    { mk_exp (E_internal_plet ($2,$4,$6)) $startpos $endpos }
+  | InternalReturn exp
+    { mk_exp (E_internal_return($2)) $startpos $endpos }
+
 /* The following implements all nine levels of user-defined precedence for
 operators in expressions, with both left, right and non-associative operators */
 
-- 
cgit v1.2.3


From 88c956dc0ee2e4e22c04d7a841d070cca7cca2a0 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Thu, 7 Feb 2019 14:30:41 -0800
Subject: Add parameterization support for bitfields.

This supports the following syntax:

  type xlen : Int = 64
  type ylen : Int = 1

  type xlenbits = bits(xlen)

  bitfield Mstatus : xlenbits = {
    SD  : xlen - ylen,
    SXL : xlen - ylen - 1 .. xlen - ylen - 3
  }
---
 src/parser.mly | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/parser.mly')

diff --git a/src/parser.mly b/src/parser.mly
index cbbc41e3..bd832d28 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1130,9 +1130,9 @@ funcl_typ:
     { mk_tannot mk_typqn $1 $startpos $endpos }
 
 index_range:
-  | Num
+  | typ
     { mk_ir (BF_single $1) $startpos $endpos }
-  | Num DotDot Num
+  | typ DotDot typ
     { mk_ir (BF_range ($1, $3)) $startpos $endpos }
 
 r_id_def:
-- 
cgit v1.2.3