diff options
| author | Kathy Gray | 2016-01-06 17:28:58 +0000 |
|---|---|---|
| committer | Kathy Gray | 2016-01-06 17:28:58 +0000 |
| commit | f98d4a9271751622647c021c32103fc05b681041 (patch) | |
| tree | 155a0ed5f2927fb86bb1596562d436e462d840ec /src/parser.mly | |
| parent | 9219f8adddac4f6b6fc10e9c4965215b09829468 (diff) | |
Add new assert expression to Sail
This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error.
WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified.
Diffstat (limited to 'src/parser.mly')
| -rw-r--r-- | src/parser.mly | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/parser.mly b/src/parser.mly index 733bb83c..7bd0a72f 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -131,11 +131,11 @@ let make_vector_sugar order_set is_inc typ typ1 = /*Terminals with no content*/ -%token And Alias As Bitzero Bitone Bits By Case Clause Const Dec Default Deinfix Effect EFFECT End +%token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Default Deinfix Effect EFFECT End %token Enumerate Else Exit Extern False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order %token Pure Rec Register Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef %token Undefined Union With Val -%token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Undef Unspec Nondet +%token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Undef Unspec Nondet Escape /* Avoid shift/reduce conflict - see right_atomic_exp rule */ @@ -325,7 +325,9 @@ effect: | Unspec { efl BE_unspec } | Nondet - { efl BE_nondet } + { efl BE_nondet } + | Escape + { efl BE_escape } effect_list: | effect @@ -589,7 +591,9 @@ atomic_exp: | Switch exp Lcurly case_exps Rcurly { eloc (E_case($2,$4)) } | Exit atomic_exp - { eloc (E_exit $2) } + { eloc (E_exit $2) } + | Assert Lparen exp Comma exp Rparen + { eloc (E_assert ($3,$5)) } field_exp: | atomic_exp |