Added exceptions and try/catch blocks to AST and typechecker in order

to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail.

8 files changed, 50 insertions, 1 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 6a74d5b2..d8d751ad 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -320,6 +320,8 @@ type
  | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *)
  | E_constraint of n_constraint (* Expression to evaluate the n_constraint at run time *)
  | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
+ | E_throw of 'a exp
+ | E_try of 'a exp * ('a pexp) list
  | E_return of 'a exp (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *)
  | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is false, 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 *)
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 67381c52..8071ee7d 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -77,11 +77,13 @@ and map_exp_annot_aux f = function
   | E_record_update (exp, fexps) -> E_record_update (map_exp_annot f exp, map_fexps_annot f fexps)
   | E_field (exp, id) -> E_field (map_exp_annot f exp, id)
   | E_case (exp, cases) -> E_case (map_exp_annot f exp, List.map (map_pexp_annot f) cases)
+  | E_try (exp, cases) -> E_try (map_exp_annot f exp, List.map (map_pexp_annot f) cases)
   | E_let (letbind, exp) -> E_let (map_letbind_annot f letbind, map_exp_annot f exp)
   | E_assign (lexp, exp) -> E_assign (map_lexp_annot f lexp, map_exp_annot f exp)
   | E_sizeof nexp -> E_sizeof nexp
   | E_constraint nc -> E_constraint nc
   | E_exit exp -> E_exit (map_exp_annot f exp)
+  | E_throw exp -> E_throw (map_exp_annot f exp)
   | E_return exp -> E_return (map_exp_annot f exp)
   | E_assert (test, msg) -> E_assert (map_exp_annot f test, map_exp_annot f msg)
   | E_internal_cast (annot, exp) -> E_internal_cast (f annot, map_exp_annot f exp)
@@ -279,6 +281,8 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_tuple exps -> "(" ^ string_of_list ", " string_of_exp exps ^ ")"
   | E_case (exp, cases) ->
      "switch " ^ string_of_exp exp ^ " { case " ^ string_of_list " case " string_of_pexp cases ^ "}"
+  | E_try (exp, cases) ->
+     "try " ^ string_of_exp exp ^ " catch { case " ^ string_of_list " case " string_of_pexp cases ^ "}"
   | E_let (letbind, exp) -> "let " ^ string_of_letbind letbind ^ " in " ^ string_of_exp exp
   | E_assign (lexp, bind) -> string_of_lexp lexp ^ " := " ^ string_of_exp bind
   | E_cast (typ, exp) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_exp exp
@@ -297,6 +301,7 @@ let rec string_of_exp (E_aux (exp, _)) =
      ^ string_of_exp body
   | E_assert (test, msg) -> "assert(" ^ string_of_exp test ^ ", " ^ string_of_exp msg ^ ")"
   | E_exit exp -> "exit " ^ string_of_exp exp
+  | E_throw exp -> "throw " ^ string_of_exp exp
   | E_cons (x, xs) -> string_of_exp x ^ " :: " ^ string_of_exp xs
   | E_list xs -> "[||" ^ string_of_list ", " string_of_exp xs ^ "||]"
   | _ -> "INTERNAL"
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 1db9d80b..aeca186d 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -498,11 +498,13 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
       | _ -> raise (Reporting_basic.err_unreachable l "to_ast_fexps with true returned none"))
     | Parse_ast.E_field(exp,id) -> E_field(to_ast_exp k_env def_ord exp, to_ast_id id)
     | Parse_ast.E_case(exp,pexps) -> E_case(to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps)
+    | Parse_ast.E_try (exp, pexps) -> E_try (to_ast_exp k_env def_ord exp, List.map (to_ast_case k_env def_ord) pexps)
     | 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_sizeof(nexp) -> E_sizeof(to_ast_nexp k_env nexp)
     | Parse_ast.E_constraint nc -> E_constraint (to_ast_nexp_constraint k_env nc)
     | Parse_ast.E_exit exp -> E_exit(to_ast_exp k_env def_ord exp)
+    | Parse_ast.E_throw exp -> E_throw (to_ast_exp k_env def_ord exp)
     | Parse_ast.E_return exp -> E_return(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,()))
diff --git a/src/lexer.mll b/src/lexer.mll
index 228ca38f..cf3c9baf 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -78,6 +78,9 @@ let kw_table =
      ("extern",                  (fun _ -> Extern));
      ("cast",                    (fun _ -> Cast));
      ("false",                   (fun _ -> False));
+     ("try",                     (fun _ -> Try));
+     ("catch",                   (fun _ -> Catch));
+     ("throw",                   (fun _ -> Throw));
      ("forall",                  (fun _ -> Forall));
      ("exist",                   (fun _ -> Exist));
      ("foreach",                 (fun _ -> Foreach));
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 8ce5e77d..54feaf29 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -283,6 +283,8 @@ exp_aux =  (* Expression *)
  | E_sizeof of atyp
  | E_constraint of n_constraint
  | E_exit of exp
+ | E_throw of exp
+ | E_try of exp * pexp list
  | E_return of exp
  | E_assert of exp * exp
 
diff --git a/src/parser.mly b/src/parser.mly
index d6da6e63..12e64141 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -131,7 +131,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End 
 %token Enumerate Else Exit Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast
 %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
-%token Undefined Union With When Val Constraint
+%token Undefined Union With When Val Constraint Try Catch Throw
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 
 
@@ -609,10 +609,14 @@ atomic_exp:
     { eloc (E_list($2)) }
   | Switch exp Lcurly case_exps Rcurly
     { eloc (E_case($2,$4)) }
+  | Try exp Catch Lcurly case_exps Rcurly
+    { eloc (E_try ($2, $5)) }
   | Sizeof atomic_typ
     { eloc (E_sizeof($2)) }
   | Constraint Lparen nexp_constraint Rparen
     { eloc (E_constraint $3) }
+  | Throw atomic_exp
+    { eloc (E_throw $2) }
   | Exit atomic_exp
       { eloc (E_exit $2) }
   | Return atomic_exp
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index a63df7ea..bb1d7357 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -277,6 +277,10 @@ let doc_exp, doc_let =
         (doc_op equals (atomic_exp e1 ^^ colon ^^ atomic_exp e2) (exp e3)))
   | E_list exps ->
       squarebarbars (separate_map comma exp exps)
+  | E_try(e,pexps) ->
+      let opening = separate space [string "try"; exp e; string "catch"; lbrace] in
+      let cases = separate_map (break 1) doc_case pexps in
+      surround 2 1 opening cases rbrace
   | E_case(e,pexps) ->
       let opening = separate space [string "switch"; exp e; lbrace] in
       let cases = separate_map (break 1) doc_case pexps in
@@ -287,6 +291,8 @@ let doc_exp, doc_let =
      string "constraint" ^^ parens (doc_nexp_constraint nc)
   | E_exit e ->
     separate space [string "exit"; atomic_exp e;]
+  | E_throw e ->
+    separate space [string "throw"; atomic_exp e;]
   | E_return e ->
     separate space [string "return"; atomic_exp e;]
   | E_assert(c,m) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index e69a40e8..bd27c2ba 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -149,6 +149,8 @@ let vector_typ n m ord typ =
                     mk_typ_arg (Typ_arg_order ord);
                     mk_typ_arg (Typ_arg_typ typ)]))
 
+let exc_typ = mk_id_typ (mk_id "exception")
+
 let is_range (Typ_aux (typ_aux, _)) =
   match typ_aux with
   | Typ_app (f, [Typ_arg_aux (Typ_arg_nexp n, _)])
@@ -1874,6 +1876,18 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
           Pat_aux (Pat_when (tpat, checked_guard, crule check_exp env case typ), (l, None))
      in
      annot_exp (E_case (inferred_exp, List.map (fun case -> check_case case typ) cases)) typ
+  | E_try (exp, cases), _ ->
+     let checked_exp = crule check_exp env exp typ in
+     let check_case pat typ = match pat with
+       | Pat_aux (Pat_exp (pat, case), (l, _)) ->
+          let tpat, env = bind_pat env pat exc_typ in
+          Pat_aux (Pat_exp (tpat, crule check_exp env case typ), (l, None))
+       | Pat_aux (Pat_when (pat, guard, case), (l, _)) ->
+          let tpat, env = bind_pat env pat exc_typ in
+          let checked_guard = check_exp env guard bool_typ in
+          Pat_aux (Pat_when (tpat, checked_guard, crule check_exp env case typ), (l, None))
+     in
+     annot_exp (E_try (checked_exp, List.map (fun case -> check_case case typ) cases)) typ
   | E_cons (x, xs), _ ->
      begin
        match is_list (Env.expand_synonyms env typ) with
@@ -1938,6 +1952,9 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
   | E_exit exp, _ ->
      let checked_exp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in
      annot_exp_effect (E_exit checked_exp) typ (mk_effect [BE_escape])
+  | E_throw exp, _ ->
+     let checked_exp = crule check_exp env exp exc_typ in
+     annot_exp_effect (E_throw checked_exp) typ (mk_effect [BE_escape])
   | E_vector vec, _ ->
      begin
        let (start, len, ord, vtyp) = destructure_vec_typ l env typ in
@@ -2726,6 +2743,11 @@ and propagate_exp_effect_aux = function
      let p_cases = List.map propagate_pexp_effect cases in
      let case_eff = List.fold_left union_effects no_effect (List.map snd p_cases) in
      E_case (p_exp, List.map fst p_cases), union_effects (effect_of p_exp) case_eff
+  | E_try (exp, cases) ->
+     let p_exp = propagate_exp_effect exp in
+     let p_cases = List.map propagate_pexp_effect cases in
+     let case_eff = List.fold_left union_effects no_effect (List.map snd p_cases) in
+     E_try (p_exp, List.map fst p_cases), union_effects (effect_of p_exp) case_eff
   | E_for (v, f, t, step, ord, body) ->
      let p_f = propagate_exp_effect f in
      let p_t = propagate_exp_effect t in
@@ -2753,6 +2775,9 @@ and propagate_exp_effect_aux = function
   | E_exit exp ->
      let p_exp = propagate_exp_effect exp in
      E_exit p_exp, effect_of p_exp
+  | E_throw exp ->
+     let p_exp = propagate_exp_effect exp in
+     E_throw p_exp, effect_of p_exp
   | E_return exp ->
      let p_exp = propagate_exp_effect exp in
      E_return p_exp, effect_of p_exp