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 /language/l2.lem | |
| 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 'language/l2.lem')
| -rw-r--r-- | language/l2.lem | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/language/l2.lem b/language/l2.lem index d097c902..ff3d3d80 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -75,8 +75,8 @@ type base_effect_aux = (* effect *) | BE_undef (* undefined-instruction exception *) | BE_unspec (* unspecified values *) | BE_nondet (* nondeterminism from intra-instruction parallelism *) + | BE_escape (* Tracking of expressions and functions that might call exit *) | BE_lset (* Local mutation happend; not user-writable *) - | BE_escape (* Internal tracking of expressions and functions that might call exit *) type base_effect = @@ -281,6 +281,7 @@ and exp_aux 'a = (* Expression *) | E_let of (letbind 'a) * (exp 'a) (* let expression *) | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) + | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is true, reporting the optional string as an error *) | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) |