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.

1 files changed, 2 insertions, 1 deletions

diff --git a/language/l2.ml b/language/l2.ml
index 2f2bc839..00345dc7 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -71,8 +71,8 @@ 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 
@@ -269,6 +269,7 @@ type
  | E_let of 'a letbind * 'a exp (* let expression *)
  | E_assign of 'a lexp * 'a exp (* imperative assignment *)
  | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
+ | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is true, reporting the optional string as an error *)
  | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
  | E_internal_exp of 'a annot (* This is an internal use for passing nexp information  to library functions, postponed for constraint solving *)
  | E_internal_exp_user of 'a annot * 'a annot (* This is like the above but the user has specified an implicit parameter for the current function *)