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.

12 files changed, 42 insertions, 12 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 *)
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 *)
diff --git a/language/l2.ott b/language/l2.ott
index d5c92fe6..1eb447be 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -194,8 +194,8 @@ base_effect :: 'BE_' ::=
   | undef                               :: :: undef {{ com undefined-instruction exception }}
   | unspec                              :: :: unspec {{ com unspecified values }}
   | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
+  | escape                              :: :: escape {{ com Tracking of expressions and functions that might call exit }}
   | lset                                :: :: lset {{ com Local mutation happend; not user-writable }}
-  | escape                              :: :: escape {{ com Internal tracking of expressions and functions that might call exit }}
 
 
 effect :: 'Effect_' ::=
@@ -644,7 +644,8 @@ exp :: 'E_' ::=
 
   | exit exp						:: :: exit
     {{ com expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp }}
-
+  | assert ( exp , exp' )                            :: :: assert
+    {{ com expression to halt with error, when the first expression is true, reporting the optional string as an error }}
   | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}
   | ( annot ) exp                                   :: :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }}
   | annot                       :: :: internal_exp {{ com This is an internal use for passing nexp information  to library functions, postponed for constraint solving }}
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index db50ecb6..1152cff9 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -54,6 +54,7 @@ base_effect_aux =  (* effect *)
  | BE_undef (* undefined-instruction exception *)
  | BE_unspec (* unspecified values *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
+ | BE_escape
 
 
 type 
@@ -231,6 +232,7 @@ exp_aux =  (* Expression *)
  | E_let of letbind * exp (* let expression *)
  | E_assign of exp * exp (* imperative assignment *)
  | E_exit of exp
+ | E_assert of exp * exp
 
 and exp = 
    E_aux of exp_aux * l
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index ae6d89bb..00345c27 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -163,6 +163,7 @@ base_effect :: 'BE_' ::=
   | undef                               :: :: undef {{ com undefined-instruction exception }}
   | unspec                              :: :: unspec {{ com unspecified values }}
   | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
+  | escape                              :: :: escape
 
 atyp :: 'ATyp_' ::=
   {{ com expressions of all kinds, to be translated to types, nats, orders, and effects after parsing }}
@@ -528,6 +529,7 @@ exp :: 'E_' ::=
     {{ com imperative assignment }}
 
   | exit exp						:: :: exit
+  | assert ( exp , exp' )                               :: :: assert
 
   | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}
 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 07fe01fd..80008453 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -240,7 +240,8 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect =
 			       | Parse_ast.BE_depend -> BE_depend
                                | Parse_ast.BE_undef  -> BE_undef
                                | Parse_ast.BE_unspec -> BE_unspec
-                               | Parse_ast.BE_nondet -> BE_nondet),l))
+                               | Parse_ast.BE_nondet -> BE_nondet
+                               | Parse_ast.BE_escape -> BE_escape),l))
                              effects)
                | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None None
     ), l)
@@ -440,6 +441,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     | Parse_ast.E_let(leb,exp) -> E_let(to_ast_letbind k_env def_ord leb, to_ast_exp k_env def_ord exp)
     | Parse_ast.E_assign(lexp,exp) -> E_assign(to_ast_lexp k_env def_ord lexp, to_ast_exp k_env def_ord exp)
     | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env def_ord exp)
+    | Parse_ast.E_assert(cond,msg) -> E_assert(to_ast_exp k_env def_ord cond, to_ast_exp k_env def_ord msg)
     ), (l,NoTyp))
 
 and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : tannot lexp = 
diff --git a/src/lexer.mll b/src/lexer.mll
index cab2e3be..a6b1bcfa 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -61,6 +61,7 @@ let kw_table =
      ("and",                     (fun _ -> And));
      ("alias",                   (fun _ -> Alias));
      ("as",                      (fun _ -> As));
+     ("assert",                  (fun _ -> Assert));
      ("bitzero",                 (fun _ -> Bitzero));
      ("bitone",                  (fun _ -> Bitone));
      ("bits",                    (fun _ -> Bits));
@@ -122,11 +123,12 @@ let kw_table =
      ("undef",                   (fun x -> Undef));
      ("unspec",                  (fun x -> Unspec));
      ("nondet",                  (fun x -> Nondet));
+     ("escape",                  (fun x -> Escape));
 
 ]
 
 let default_type_names = ["bool";"unit";"vector";"range";"list";"bit";"nat"; "int";
-			  "uint8";"uint16";"uint32";"uint64";"atom";"implicit";"string"]
+			  "uint8";"uint16";"uint32";"uint64";"atom";"implicit";"string";"option"]
 let custom_type_names : string list ref = ref []
 
 }
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
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index f0005d02..24c978fd 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -428,6 +428,8 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
     | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_exit exp -> fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
+    | E_assert(c,msg) ->
+      fprintf ppf "@[<0>(E_aux (E_assert %a %a) (%a, %a))@]" pp_lem_exp c pp_lem_exp msg pp_lem_l l pp_annot annot
     | E_internal_exp ((l, Base((_,t),_,_,_,_,bindings))) ->
       (*TODO use bindings where appropriate*)
       (match t.t with
@@ -972,6 +974,8 @@ let doc_exp, doc_let =
       surround 2 1 opening cases rbrace
   | E_exit e ->
     separate space [string "exit"; exp e;]
+  | E_assert(c,m) ->
+    separate space [string "assert"; parens (separate comma [exp c; exp m])]
   (* adding parens and loop for lower precedence *)
   | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _)
   | E_cons (_, _)|E_field (_, _)|E_assign (_, _)
diff --git a/src/type_check.ml b/src/type_check.ml
index 87dbb05f..0971bc29 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1332,6 +1332,11 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
       let (e',t',_,_,_,_) = check_exp envs imp_param true (new_t ()) e in
       let efs = add_effect (BE_aux(BE_escape, l)) pure_e in
       (E_aux (E_exit e',(l,(simple_annot_efr expect_t efs))),expect_t,t_env,[],nob,efs)
+    | E_assert(cond,msg) ->
+      let (cond',t',_,_,_,_) = check_exp envs imp_param true bit_t cond in
+      let (msg',mt',_,_,_,_) = check_exp envs imp_param true {t= Tapp("option",[TA_typ string_t])} msg in
+      let (t',c') = type_consistent (Expr l) d_env Require false unit_t expect_t in
+      (E_aux (E_assert(cond',msg'), (l, (simple_annot expect_t))), expect_t,t_env,c',nob,pure_e)
     | E_internal_cast _ | E_internal_exp _ | E_internal_exp_user _ | E_internal_let _
     | E_internal_plet _ | E_internal_return _ -> 
       raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 59a573d9..d4eeefdf 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1396,6 +1396,7 @@ let unit_t = { t = Tid "unit" }
 let bit_t = {t = Tid "bit" }
 let bool_t = {t = Tid "bool" }
 let nat_typ = {t=Tid "nat"}
+let string_t = {t = Tid "string"}
 let pure_e = {effect=Eset []}
 let nob = No_bounds
 
@@ -1424,6 +1425,7 @@ let initial_kind_env =
     ("range", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}], {k = K_Typ}) });
     ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } );
     ("atom", {k = K_Lam( [ {k=K_Nat} ], {k=K_Typ})});
+    ("option", { k = K_Lam( [{k=K_Typ}], {k=K_Typ}) });
     ("implicit", {k = K_Lam( [{k = K_Nat}], {k=K_Typ})} );
   ]
 
@@ -1486,6 +1488,10 @@ let mk_bitwise_op name symb arity =
 let initial_typ_env =
   Envmap.from_list [
     ("ignore",lib_tannot ([("a",{k=K_Typ})],mk_pure_fun {t=Tvar "a"} unit_t) None []);
+    ("Some", Base((["a",{k=K_Typ}], mk_pure_fun {t=Tvar "a"} {t=Tapp("option", [TA_typ {t=Tvar "a"}])}),
+                  Constructor 2,[],pure_e,pure_e,nob));
+    ("None", Base((["a", {k=K_Typ}], mk_pure_fun unit_t {t=Tapp("option", [TA_typ {t=Tvar "a"}])}),
+                  Constructor 2,[],pure_e,pure_e,nob));
     ("+",Overload(
       lib_tannot ((mk_typ_params ["a";"b";"c"]),
                   (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})) (Some "add") [],
@@ -2438,8 +2444,7 @@ let order_eq co o1 o2 =
 
 let rec remove_internal_effects = function
   | [] -> []
-  | (BE_aux(BE_lset,_))::effects
-  | (BE_aux(BE_escape,_))::effects -> remove_internal_effects effects
+  | (BE_aux(BE_lset,_))::effects -> remove_internal_effects effects
   | b::effects -> b::(remove_internal_effects effects)
 
 let has_effect searched_for eff =
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 0a0ce455..3ce965c1 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -207,6 +207,7 @@ val nat_t : t
 val unit_t : t
 val bool_t : t
 val bit_t : t
+val string_t : t
 val pure_e : effect
 val nob : bounds_env