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.

7 files changed, 31 insertions, 8 deletions

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