Added while-do and repeat-until loops to sail for translating ASL

10 files changed, 44 insertions, 2 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 710e8067..1728f492 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -289,6 +289,7 @@ type
 'a reg_id_aux =
    RI_id of id
 
+type loop = While | Until
 
 type
 'a exp_aux =  (* Expression *)
@@ -301,7 +302,8 @@ type
  | E_app_infix of 'a exp * id * 'a exp (* infix function application *)
  | E_tuple of ('a exp) list (* tuple *)
  | E_if of 'a exp * 'a exp * 'a exp (* conditional *)
- | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* loop *)
+ | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* for loop *)
+ | E_loop of loop * 'a exp * 'a exp
  | E_vector of ('a exp) list (* vector (indexed from 0) *)
  | E_vector_indexed of ((int * 'a exp)) list * 'a opt_default (* vector (indexed consecutively) *)
  | E_vector_access of 'a exp * 'a exp (* vector access *)
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 46c79764..048fbb15 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -221,6 +221,7 @@ and map_exp_annot_aux f = function
   | E_tuple xs -> E_tuple (List.map (map_exp_annot f) xs)
   | E_if (cond, t, e) -> E_if (map_exp_annot f cond, map_exp_annot f t, map_exp_annot f e)
   | E_for (v, e1, e2, e3, o, e4) -> E_for (v, map_exp_annot f e1, map_exp_annot f e2, map_exp_annot f e3, o, map_exp_annot f e4)
+  | E_loop (loop_type, e1, e2) -> E_loop (loop_type, map_exp_annot f e1, map_exp_annot f e2)
   | E_vector exps -> E_vector (List.map (map_exp_annot f) exps)
   | E_vector_indexed (iexps, opt_default) ->
      E_vector_indexed (List.map (fun (i, exp) -> (i, map_exp_annot f exp)) iexps, map_opt_default_annot f opt_default)
@@ -476,6 +477,8 @@ let rec string_of_exp (E_aux (exp, _)) =
      ^ " by " ^ string_of_exp u ^ " order " ^ string_of_order ord
      ^ ") { "
      ^ string_of_exp body
+  | E_loop (While, cond, body) -> "while " ^ string_of_exp cond ^ " do " ^ string_of_exp body
+  | E_loop (Until, cond, body) -> "repeat " ^ string_of_exp body ^ " until " ^ string_of_exp cond
   | 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
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 1f7840d0..83c79646 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -469,7 +469,9 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     | Parse_ast.E_if(e1,e2,e3) -> E_if(to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2, to_ast_exp k_env def_ord e3)
     | Parse_ast.E_for(id,e1,e2,e3,atyp,e4) -> 
       E_for(to_ast_id id,to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2,
-	    to_ast_exp k_env def_ord e3,to_ast_order k_env def_ord atyp, to_ast_exp k_env def_ord e4)
+            to_ast_exp k_env def_ord e3,to_ast_order k_env def_ord atyp, to_ast_exp k_env def_ord e4)
+    | Parse_ast.E_loop(Parse_ast.While, e1, e2) -> E_loop (While, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2)
+    | Parse_ast.E_loop(Parse_ast.Until, e1, e2) -> E_loop (Until, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2)
     | Parse_ast.E_vector(exps) -> 
       (match to_ast_iexps false k_env def_ord exps with
 	| Some([]) -> E_vector([])
diff --git a/src/lexer.mll b/src/lexer.mll
index cf3c9baf..fb091f67 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -112,6 +112,10 @@ let kw_table =
      ("union",			 (fun x -> Union));
      ("with",                    (fun x -> With));
      ("when",                    (fun x -> When));
+     ("repeat",                  (fun x -> Repeat));
+     ("until",                   (fun x -> Until));
+     ("while",                   (fun x -> While));
+     ("do",                      (fun x -> Do));
      ("val",                     (fun x -> Val));
 
      ("div",			 (fun x -> Div_));
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 2509f8ef..1e2c8bc6 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -137,6 +137,15 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
      separate space [string "let"; ocaml_atomic_lexp ctx lexp;
                      equals; string "ref"; ocaml_atomic_exp ctx exp1; string "in"]
      ^/^ ocaml_exp ctx exp2
+  | E_loop (While, cond, body) ->
+     let loop_body =
+       separate space [string "if"; ocaml_atomic_exp ctx cond;
+                       string "then"; parens (ocaml_atomic_exp ctx body ^^ semi ^^ space ^^ string "loop ()");
+                       string "else ()"]
+     in
+     (string "let rec loop () =" ^//^ loop_body)
+     ^/^ string "in"
+     ^/^ string "loop ()"
   | E_lit _ | E_list _ | E_id _ | E_tuple _ -> ocaml_atomic_exp ctx exp
   | _ -> string ("EXP(" ^ string_of_exp exp ^ ")")
 and ocaml_letbind ctx (LB_aux (lb_aux, _)) =
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index b259611d..6424d682 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -253,6 +253,7 @@ and fpat_aux =  (* Field pattern *)
 and fpat = 
    FP_aux of fpat_aux * l
 
+type loop = While | Until
 
 type 
 exp_aux =  (* Expression *)
@@ -265,6 +266,7 @@ exp_aux =  (* Expression *)
  | E_app_infix of exp * id * exp (* infix function application *)
  | E_tuple of (exp) list (* tuple *)
  | E_if of exp * exp * exp (* conditional *)
+ | E_loop of loop * exp * exp
  | E_for of id * exp * exp * exp * atyp * exp (* loop *)
  | E_vector of (exp) list (* vector (indexed from 0) *)
  | E_vector_indexed of (exp) list * opt_default (* vector (indexed consecutively) *)
diff --git a/src/parser.mly b/src/parser.mly
index 5413ac0d..0c3dbb03 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -133,6 +133,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
 %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
+%token While Do Repeat Until
 
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
@@ -689,6 +690,8 @@ right_atomic_exp:
         then ATyp_aux(ATyp_inc,(locn 6 6))
         else ATyp_aux(ATyp_dec,(locn 6 6)) in
       eloc (E_for($3,$5,$7,step,ord,$9)) }
+  | While exp Do exp
+    { eloc (E_loop (While, $2, $4)) }
   | letbind In exp
     { eloc (E_let($1,$3)) }
 
diff --git a/src/rewriter.ml b/src/rewriter.ml
index fed8408d..e257e19c 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -698,6 +698,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; e_tuple                  : 'exp list -> 'exp_aux
   ; e_if                     : 'exp * 'exp * 'exp -> 'exp_aux
   ; e_for                    : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux
+  ; e_loop                   : loop * 'exp * 'exp -> 'exp_aux
   ; e_vector                 : 'exp list -> 'exp_aux
   ; e_vector_indexed         : (int * 'exp) list * 'opt_default -> 'exp_aux
   ; e_vector_access          : 'exp * 'exp -> 'exp_aux
@@ -763,6 +764,8 @@ let rec fold_exp_aux alg = function
   | E_if (e1,e2,e3) -> alg.e_if (fold_exp alg e1, fold_exp alg e2, fold_exp alg e3)
   | E_for (id,e1,e2,e3,order,e4) ->
      alg.e_for (id,fold_exp alg e1, fold_exp alg e2, fold_exp alg e3, order, fold_exp alg e4)
+  | E_loop (loop_type, e1, e2) ->
+     alg.e_loop (loop_type, fold_exp alg e1, fold_exp alg e2)
   | E_vector es -> alg.e_vector (List.map (fold_exp alg) es)
   | E_vector_indexed (es,opt) ->
      alg.e_vector_indexed (List.map (fun (id,e) -> (id,fold_exp alg e)) es, fold_opt_default alg opt)
@@ -840,6 +843,7 @@ let id_exp_alg =
   ; e_tuple = (fun es -> E_tuple es)
   ; e_if = (fun (e1,e2,e3) -> E_if (e1,e2,e3))
   ; e_for = (fun (id,e1,e2,e3,order,e4) -> E_for (id,e1,e2,e3,order,e4))
+  ; e_loop = (fun (lt, e1, e2) -> E_loop (lt, e1, e2))
   ; e_vector = (fun es -> E_vector es)
   ; e_vector_indexed = (fun (es,opt2) -> E_vector_indexed (es,opt2))
   ; e_vector_access = (fun (e1,e2) -> E_vector_access (e1,e2))
@@ -937,6 +941,8 @@ let compute_exp_alg bot join =
   ; e_if = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_if (e1,e2,e3)))
   ; e_for = (fun (id,(v1,e1),(v2,e2),(v3,e3),order,(v4,e4)) ->
     (join_list [v1;v2;v3;v4], E_for (id,e1,e2,e3,order,e4)))
+  ; e_loop = (fun (lt, (v1, e1), (v2, e2)) ->
+    (join_list [v1;v2], E_loop (lt, e1, e2)))
   ; e_vector = split_join (fun es -> E_vector es)
   ; e_vector_indexed = (fun (es,(v2,opt2)) ->
     let (is,es) = List.split es in
@@ -1177,6 +1183,7 @@ let rewrite_sizeof (Defs defs) =
     ; e_tuple = (fun es -> let (es, es') = List.split es in (E_tuple es, E_tuple es'))
     ; e_if = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_if (e1,e2,e3), E_if (e1',e2',e3')))
     ; e_for = (fun (id,(e1,e1'),(e2,e2'),(e3,e3'),order,(e4,e4')) -> (E_for (id,e1,e2,e3,order,e4), E_for (id,e1',e2',e3',order,e4')))
+    ; e_loop = (fun (lt, (e1, e1'), (e2, e2')) -> (E_loop (lt, e1, e2), E_loop (lt, e1', e2')))
     ; e_vector = (fun es -> let (es, es') = List.split es in (E_vector es, E_vector es'))
     ; e_vector_indexed = (fun (es,(opt2,opt2')) -> let (is, es) = List.split es in let (es, es') = List.split es in let (es, es') = (List.combine is es, List.combine is es') in (E_vector_indexed (es,opt2), E_vector_indexed (es',opt2')))
     ; e_vector_access = (fun ((e1,e1'),(e2,e2')) -> (E_vector_access (e1,e2), E_vector_access (e1',e2')))
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 010f1003..11394ec6 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -97,6 +97,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; e_tuple                  : 'exp list -> 'exp_aux
  ; e_if                     : 'exp * 'exp * 'exp -> 'exp_aux
  ; e_for                    : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux
+ ; e_loop                   : loop * 'exp * 'exp -> 'exp_aux
  ; e_vector                 : 'exp list -> 'exp_aux
  ; e_vector_indexed         : (int * 'exp) list * 'opt_default -> 'exp_aux
  ; e_vector_access          : 'exp * 'exp -> 'exp_aux
diff --git a/src/type_check.ml b/src/type_check.ml
index 5813b081..5a98704c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2559,6 +2559,10 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      in
      try_overload (Env.get_overloads f env)
   | E_app (f, xs) -> infer_funapp l env f xs None
+  | E_loop (loop_type, cond, body) ->
+     let checked_cond = crule check_exp env cond bool_typ in
+     let checked_body = crule check_exp env body unit_typ in
+     annot_exp (E_loop (loop_type, checked_cond, checked_body)) unit_typ
   | E_for (v, f, t, step, ord, body) ->
      begin
        let f, t = match ord with
@@ -2857,6 +2861,11 @@ and propagate_exp_effect_aux = function
      let p_body = propagate_exp_effect body in
      E_for (v, p_f, p_t, p_step, ord, p_body),
      collect_effects [p_f; p_t; p_step; p_body]
+  | E_loop (loop_type, cond, body) ->
+     let p_cond = propagate_exp_effect cond in
+     let p_body = propagate_exp_effect body in
+     E_loop (loop_type, p_cond, p_body),
+     union_effects (effect_of p_cond) (effect_of p_body)
   | E_let (letbind, exp) ->
      let p_lb, eff = propagate_letbind_effect letbind in
      let p_exp = propagate_exp_effect exp in