Better support for exceptions in sail for ASL specs that need them.

6 files changed, 24 insertions, 3 deletions

diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 73a297ce..6254d580 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -141,6 +141,7 @@ let ocaml_typ_id ctx = function
   | id when Id.compare id (mk_id "bool") = 0 -> string "bool"
   | id when Id.compare id (mk_id "unit") = 0 -> string "unit"
   | id when Id.compare id (mk_id "real") = 0 -> string "Num.num"
+  | id when Id.compare id (mk_id "exception") = 0 -> string "exn"
   | id when Id.compare id (mk_id "register") = 0 -> string "ref"
   | id -> zencode ctx id
 
@@ -229,6 +230,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
   | E_block exps -> begin_end (ocaml_block ctx exps)
   | E_field (exp, id) -> ocaml_atomic_exp ctx exp ^^ dot ^^ zencode ctx id
   | E_exit exp -> string "exit 0"
+  | E_throw exp -> string "raise" ^^ space ^^ ocaml_atomic_exp ctx exp
   | E_case (exp, pexps) ->
      begin_end (separate space [string "match"; ocaml_atomic_exp ctx exp; string "with"]
                 ^/^ ocaml_pexps ctx pexps)
@@ -487,6 +489,17 @@ let rec ocaml_cases ctx =
   | tu :: tus -> ocaml_case tu ^/^ ocaml_cases ctx tus
   | [] -> empty
 
+let rec ocaml_exceptions ctx =
+  let ocaml_exception = function
+    | Tu_aux (Tu_id id, _) -> separate space [string "exception"; zencode_upper ctx id]
+    | Tu_aux (Tu_ty_id (typ, id), _) ->
+       separate space [string "exception"; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
+  in
+  function
+  | [tu] -> ocaml_exception tu
+  | tu :: tus -> ocaml_exception tu ^^ string ";;" ^^ hardline ^^ ocaml_exceptions ctx tus
+  | [] -> empty
+
 let rec ocaml_enum ctx = function
   | [id] -> zencode_upper ctx id
   | id :: ids -> zencode_upper ctx id ^/^ (bar ^^ space ^^ ocaml_enum ctx ids)
@@ -524,6 +537,8 @@ let ocaml_typedef ctx (TD_aux (td_aux, _)) =
       ^/^ rbrace)
      ^^ ocaml_def_end
      ^^ ocaml_string_of_struct ctx id typq fields
+  | TD_variant (id, _, _, cases, _) when string_of_id id = "exception" ->
+     ocaml_exceptions ctx cases
   | TD_variant (id, _, typq, cases, _) ->
      separate space [string "type"; ocaml_typquant typq; zencode ctx id; equals]
      ^//^ ocaml_cases ctx cases
diff --git a/src/parser2.mly b/src/parser2.mly
index 6ab070b7..21959cf5 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -1021,6 +1021,8 @@ type_def:
     { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos }
   | Enum id Eq Lcurly enum Rcurly
     { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos }
+  | Union id Eq Lcurly type_unions Rcurly
+    { mk_td (TD_variant ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
   | Union id typquant Eq Lcurly type_unions Rcurly
     { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
 
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index 43c8eca9..82d3878b 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -315,7 +315,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
        | _ -> header ^//^ doc_exp exp4
      end
   (* Resugar an assert with an empty message *)
-  | E_throw exp -> assert false
+  | E_throw exp -> string "throw" ^^ parens (doc_exp exp)
   | E_try (exp, pexps) -> assert false
   | E_return exp -> string "return" ^^ parens (doc_exp exp)
   | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 ->
@@ -324,7 +324,6 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
 and doc_infix n (E_aux (e_aux, _) as exp) =
   match e_aux with
   | E_app_infix (l, op, r) when n < 10 ->
-     let module M = Map.Make(String)  in
      begin
        try
          match Bindings.find op !fixities with
@@ -500,7 +499,6 @@ let rec doc_def def = group (match def with
   | DEF_reg_dec dec -> doc_dec dec
   | DEF_scattered sdef -> doc_scattered sdef
   | DEF_fixity (prec, n, id) ->
-     print_endline ("YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY " ^ string_of_id id);
      fixities := Bindings.add id (prec, int_of_big_int n) !fixities;
      separate space [doc_prec prec; doc_int n; doc_id id]
   | DEF_overload (id, ids) ->
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 98ecc486..4683d84b 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -518,6 +518,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; e_sizeof                 : nexp -> 'exp_aux
   ; e_constraint             : n_constraint -> 'exp_aux
   ; e_exit                   : 'exp -> 'exp_aux
+  ; e_throw                  : 'exp -> 'exp_aux
   ; e_return                 : 'exp -> 'exp_aux
   ; e_assert                 : 'exp * 'exp -> 'exp_aux
   ; e_internal_cast          : 'a annot * 'exp -> 'exp_aux
@@ -586,6 +587,7 @@ let rec fold_exp_aux alg = function
   | E_sizeof nexp -> alg.e_sizeof nexp
   | E_constraint nc -> alg.e_constraint nc
   | E_exit e -> alg.e_exit (fold_exp alg e)
+  | E_throw e -> alg.e_throw (fold_exp alg e)
   | E_return e -> alg.e_return (fold_exp alg e)
   | E_assert(e1,e2) -> alg.e_assert (fold_exp alg e1, fold_exp alg e2)
   | E_internal_cast (annot,e) -> alg.e_internal_cast (annot, fold_exp alg e)
@@ -658,6 +660,7 @@ let id_exp_alg =
   ; e_sizeof = (fun nexp -> E_sizeof nexp)
   ; e_constraint = (fun nc -> E_constraint nc)
   ; e_exit = (fun e1 -> E_exit (e1))
+  ; e_throw = (fun e1 -> E_throw (e1))
   ; e_return = (fun e1 -> E_return e1)
   ; e_assert = (fun (e1,e2) -> E_assert(e1,e2)) 
   ; e_internal_cast = (fun (a,e1) -> E_internal_cast (a,e1))
@@ -753,6 +756,7 @@ let compute_exp_alg bot join =
   ; e_sizeof = (fun nexp -> (bot, E_sizeof nexp))
   ; e_constraint = (fun nc -> (bot, E_constraint nc))
   ; e_exit = (fun (v1,e1) -> (v1, E_exit (e1)))
+  ; e_throw = (fun (v1,e1) -> (v1, E_throw (e1)))
   ; e_return = (fun (v1,e1) -> (v1, E_return e1))
   ; e_assert = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_assert(e1,e2)) )
   ; e_internal_cast = (fun (a,(v1,e1)) -> (v1, E_internal_cast (a,e1)))
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 9fa17a53..cd293ca5 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -133,6 +133,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; e_sizeof                 : nexp -> 'exp_aux
  ; e_constraint             : n_constraint -> 'exp_aux
  ; e_exit                   : 'exp -> 'exp_aux
+ ; e_throw                  : 'exp -> 'exp_aux
  ; e_return                 : 'exp -> 'exp_aux
  ; e_assert                 : 'exp * 'exp -> 'exp_aux
  ; e_internal_cast          : 'a annot * 'exp -> 'exp_aux
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 8963d189..100b9eb7 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -364,6 +364,7 @@ let rewrite_sizeof (Defs defs) =
     ; e_sizeof = (fun nexp -> (E_sizeof nexp, E_sizeof nexp))
     ; e_constraint = (fun nc -> (E_constraint nc, E_constraint nc))
     ; e_exit = (fun (e1,e1') -> (E_exit (e1), E_exit (e1')))
+    ; e_throw = (fun (e1,e1') -> (E_throw (e1), E_throw (e1')))
     ; e_return = (fun (e1,e1') -> (E_return e1, E_return e1'))
     ; e_assert = (fun ((e1,e1'),(e2,e2')) -> (E_assert(e1,e2), E_assert(e1',e2')) )
     ; e_internal_cast = (fun (a,(e1,e1')) -> (E_internal_cast (a,e1), E_internal_cast (a,e1')))