Started work on an undefined literal removal pass for the ocaml

backed.

Ocaml doesn't support undefined values, so we need a way to remove
them from the specification in order to generate good ocaml
code. There are more subtle issues to - like if we initialize a
mutable variable with an undefined list, then the ocaml runtime has no
way of telling what it's length should be (as this information is
removed by the simple_types pass).

We therefore rewrite undefined literals with calls to functions that
create undefined types, e.g.

(bool) undefined becomes undefined_bool ()

(vector<'n,'m,dec,bit>) undefined becomes undefined_vector(sizeof 'n, sizeof 'm, undefined_bit ())

We therefore have to generate undefined_X functions for any user
defined datatype X. initial_check seems to be the logical place for
this. This is straightforward provided the user defined types are
not-recursive (and it shouldn't be too bad even if they are).

9 files changed, 138 insertions, 26 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index d9977d93..7d8797f9 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -46,15 +46,36 @@ open Ast
 open Util
 open Big_int
 
+let no_annot = (Parse_ast.Unknown, ())
+
+let inc_ord = Ord_aux (Ord_inc, Parse_ast.Unknown)
+let dec_ord = Ord_aux (Ord_dec, Parse_ast.Unknown)
+
 let mk_nc nc_aux = NC_aux (nc_aux, Parse_ast.Unknown)
 
 let mk_nexp nexp_aux = Nexp_aux (nexp_aux, Parse_ast.Unknown)
 
-let mk_exp exp_aux = E_aux (exp_aux, (Parse_ast.Unknown, ()))
+let mk_exp exp_aux = E_aux (exp_aux, no_annot)
 let unaux_exp (E_aux (exp_aux, _)) = exp_aux
 
+let mk_pat pat_aux = P_aux (pat_aux, no_annot)
+
 let mk_lit lit_aux = L_aux (lit_aux, Parse_ast.Unknown)
 
+let mk_lit_exp lit_aux = mk_exp (E_lit (mk_lit lit_aux))
+
+let mk_funcl id pat body = FCL_aux (FCL_Funcl (id, pat, body), no_annot)
+
+let mk_fundef funcls =
+  let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in
+  let effect_opt = Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown) in
+  let rec_opt = Rec_aux (Rec_nonrec, Parse_ast.Unknown) in
+  DEF_fundef
+   (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), no_annot))
+
+let mk_val_spec vs_aux =
+  DEF_spec (VS_aux (vs_aux, no_annot))
+
 let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f annot)
 and map_exp_annot_aux f = function
   | E_block xs -> E_block (List.map (map_exp_annot f) xs)
@@ -157,6 +178,10 @@ let id_of_kid = function
 let string_of_kid = function
   | Kid_aux (Var v, _) -> v
 
+let prepend_id str = function
+  | Id_aux (Id v, l) -> Id_aux (Id (str ^ v), l)
+  | Id_aux (DeIid v, l) -> Id_aux (DeIid (str ^ v), l)
+
 let string_of_base_effect_aux = function
   | BE_rreg -> "rreg"
   | BE_wreg -> "wreg"
diff --git a/src/ast_util.mli b/src/ast_util.mli
index b0ccb7b8..7580404d 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -47,10 +47,18 @@ open Ast
 val mk_nc : n_constraint_aux -> n_constraint
 val mk_nexp : nexp_aux -> nexp
 val mk_exp : unit exp_aux -> unit exp
+val mk_pat : unit pat_aux -> unit pat
 val mk_lit : lit_aux -> lit
+val mk_lit_exp : lit_aux -> unit exp
+val mk_funcl : id -> unit pat -> unit exp -> unit funcl
+val mk_fundef : (unit funcl) list -> unit def
+val mk_val_spec : val_spec_aux -> unit def
 
 val unaux_exp : 'a exp -> 'a exp_aux
 
+val inc_ord : order
+val dec_ord : order
+
 (* Functions to map over the annotations in sub-expressions *)
 val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
 val map_pat_annot : ('a annot -> 'b annot) -> 'a pat -> 'b pat
@@ -92,6 +100,8 @@ val id_of_fundef : 'a fundef -> id
 
 val id_of_kid : kid -> id
 
+val prepend_id : string -> id -> id
+
 module Id : sig
   type t = id
   val compare : id -> id -> int
diff --git a/src/initial_check.ml b/src/initial_check.ml
index e5717389..8e5fd35f 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -42,6 +42,7 @@
 
 open Ast
 open Util
+open Ast_util
 
 module Envmap = Finite_map.Fmap_map(String)
 module Nameset' = Set.Make(String)
@@ -1006,6 +1007,46 @@ let initial_kind_env =
     ("implicit", {k = K_Lam( [{k = K_Nat}], {k=K_Typ})} );
   ]
 
+let typschm_of_string order str =
+  let typschm = Parser2.typschm Lexer2.token (Lexing.from_string str) in
+  let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
+  typschm
+
+let val_spec_ids (Defs defs) =
+  let val_spec_id (VS_aux (vs_aux, _)) =
+    match vs_aux with
+    | VS_val_spec (typschm, id) -> id
+    | VS_extern_no_rename (typschm, id) -> id
+    | VS_extern_spec (typschm, id, e) -> id
+    | VS_cast_spec (typschm, id) -> id
+  in
+  let rec vs_ids = function
+    | DEF_spec vs :: defs -> val_spec_id vs :: vs_ids defs
+    | def :: defs -> vs_ids defs
+    | [] -> []
+  in
+  IdSet.of_list (vs_ids defs)
+
+let generate_undefineds vs_ids (Defs defs) =
+  let undefined_td = function
+    | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
+       let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in
+       [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id));
+        mk_fundef [mk_funcl (prepend_id "undefined_" id)
+                            (mk_pat (P_lit (mk_lit L_unit)))
+                            (mk_exp (E_lit (mk_lit L_undef)))]]
+    | _ -> []
+  in
+  let rec undefined_defs = function
+    | DEF_type (TD_aux (td_aux, _)) as def :: defs ->
+       def :: undefined_td td_aux @ undefined_defs defs
+    | def :: defs ->
+       def :: undefined_defs defs
+    | [] -> []
+  in
+  Defs (undefined_defs defs)
+
 let process_ast order defs =
   let (ast, _, _) = to_ast Nameset.empty initial_kind_env order defs in
-  ast
+  let vs_ids = val_spec_ids ast in
+  generate_undefineds vs_ids ast
diff --git a/src/parser2.mly b/src/parser2.mly
index bde542e0..42e13721 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -153,6 +153,8 @@ let rec desugar_rchain chain s e =
 %token <string> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
 
 %start file
+%start typschm
+%type <Parse_ast.typschm> typschm
 %type <Parse_ast.defs> defs
 %type <Parse_ast.defs> file
 
@@ -1022,4 +1024,3 @@ defs:
 file:
   | defs Eof
     { $1 }
-
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index b0b63ec1..2f38fe02 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -345,6 +345,8 @@ let doc_exp, doc_let =
   | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away"))
   | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false
                                   *)
+  | E_internal_let (lexp, exp1, exp2) ->
+      separate space [string "internal let"; doc_lexp lexp; equals; exp exp1; string "in"; exp exp2]
   | _ -> failwith ("Cannot print: " ^ Ast_util.string_of_exp expr)
   and let_exp (LB_aux(lb,_)) = match lb with
     | LB_val_explicit(ts,pat,e) ->
diff --git a/src/rewriter.ml b/src/rewriter.ml
index d61939ee..21ea3cf5 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1018,7 +1018,18 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
          | _ -> None
        end
   in
-  let rewrite_e_aux (E_aux (e_aux, (l, _)) as orig_exp) =
+  let rec split_nexp (Nexp_aux (nexp_aux, l) as nexp) =
+    match nexp_aux with
+    | Nexp_sum (n1, n2) ->
+       mk_exp (E_app (mk_id "add_range", [split_nexp n1; split_nexp n2]))
+    | Nexp_minus (n1, n2) ->
+       mk_exp (E_app (mk_id "sub_range", [split_nexp n1; split_nexp n2]))
+    | Nexp_times (n1, n2) ->
+       mk_exp (E_app (mk_id "mult_range", [split_nexp n1; split_nexp n2]))
+    | Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_range", [split_nexp nexp]))
+    | _ -> mk_exp (E_sizeof nexp)
+  in
+  let rec rewrite_e_aux split_sizeof (E_aux (e_aux, (l, _)) as orig_exp) =
     let env = env_of orig_exp in
     match e_aux with
     | E_sizeof (Nexp_aux (Nexp_constant c, _) as nexp) ->
@@ -1033,12 +1044,15 @@ let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
          in
          match exps with
          | (exp :: _) -> exp
+         | [] when split_sizeof ->
+            fold_exp (rewrite_e_sizeof false) (check_exp env (split_nexp nexp) (typ_of orig_exp))
          | [] -> orig_exp
        end
     | _ -> orig_exp
+  and rewrite_e_sizeof split_sizeof =
+    { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux split_sizeof (E_aux (exp, annot))) }
   in
-  let rewrite_e_constraint = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in
-  rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_e_constraint) }, rewrite_e_aux
+  rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rewrite_e_sizeof true)) }, rewrite_e_aux true
 
 (* Rewrite sizeof expressions with type-level variables to
    term-level expressions
@@ -2396,6 +2410,30 @@ let rewrite_overload_cast (Defs defs) =
   let defs = List.map simple_def defs in
   Defs (List.filter (fun def -> not (is_overload def)) defs)
 
+let rewrite_undefined =
+  let rec undefined_of_typ (Typ_aux (typ_aux, _)) =
+    match typ_aux with
+    | Typ_id id ->
+       mk_exp (E_app (prepend_id "undefined_" id, [mk_lit_exp L_unit]))
+    | Typ_app (id, args) ->
+       mk_exp (E_app (prepend_id "undefined_" id, List.concat (List.map undefined_of_typ_args args)))
+    | Typ_fn _ -> assert false
+  and undefined_of_typ_args (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
+    match typ_arg_aux with
+    | Typ_arg_nexp n -> [mk_exp (E_sizeof n)]
+    | Typ_arg_typ typ -> [undefined_of_typ typ]
+    | Typ_arg_order _ -> []
+  in
+  let rewrite_e_aux (E_aux (e_aux, _) as exp) =
+    match e_aux with
+    | E_lit (L_aux (L_undef, l)) ->
+       print_endline ("Undefined: " ^ string_of_typ (typ_of exp));
+       check_exp (env_of exp) (undefined_of_typ (typ_of exp)) (typ_of exp)
+    | _ -> exp
+  in
+  let rewrite_exp_undefined = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in
+  rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp_undefined) }
+
 (* This pass aims to remove all the Num quantifiers from the specification. *)
 let rewrite_simple_types (Defs defs) =
   let is_simple = function
@@ -2465,18 +2503,6 @@ let rewrite_simple_types (Defs defs) =
   let defs = Defs (List.map simple_def defs) in
   rewrite_defs_base simple_defs defs
 
-let rewrite_defs_ocaml = [
-    (* top_sort_defs; *)
-  rewrite_defs_remove_vector_concat;
-  rewrite_constraint;
-  rewrite_trivial_sizeof;
-  rewrite_sizeof;
-  rewrite_simple_types;
-  rewrite_overload_cast;
-  (* rewrite_defs_exp_lift_assign *)
-  (* rewrite_defs_separate_numbs *)
-  ]
-
 let rewrite_defs_remove_blocks =
   let letbind_wild v body =
     let (E_aux (_,(l,tannot))) = v in
@@ -3321,4 +3347,17 @@ let rewrite_defs_lem =[
   rewrite_defs_remove_superfluous_letbinds;
   rewrite_defs_remove_superfluous_returns
   ]
-  
+
+let rewrite_defs_ocaml = [
+    (* top_sort_defs; *)
+  rewrite_undefined;
+  rewrite_defs_remove_vector_concat;
+  rewrite_constraint;
+  rewrite_trivial_sizeof;
+  (* rewrite_sizeof; *)
+  (* rewrite_simple_types; *)
+  (* rewrite_overload_cast; *)
+  (* rewrite_defs_exp_lift_assign; *)
+  (* rewrite_defs_exp_lift_assign *)
+  (* rewrite_defs_separate_numbs *)
+  ]
diff --git a/src/sail.ml b/src/sail.ml
index b6f5d0c6..081a414f 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -135,7 +135,7 @@ let main() =
     let ast =
       List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes) 
                         -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
-    let ast = convert_ast Type_check.inc_ord ast in
+    let ast = convert_ast Ast_util.inc_ord ast in
     let (ast, type_envs) = check_ast ast in
 
     let (ast, type_envs) =
diff --git a/src/type_check.ml b/src/type_check.ml
index 9811b0d4..9e7a1ab3 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -99,9 +99,6 @@ let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown)
 
 let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown)
 
-let inc_ord = Ord_aux (Ord_inc, Parse_ast.Unknown)
-let dec_ord = Ord_aux (Ord_dec, Parse_ast.Unknown)
-
 let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown)
 
 let rec nexp_simp (Nexp_aux (nexp, l)) = Nexp_aux (nexp_simp_aux nexp, l)
diff --git a/src/type_check.mli b/src/type_check.mli
index 5a43573a..e3b9b81b 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -207,9 +207,6 @@ val list_typ : typ -> typ
 val exist_typ : (kid -> n_constraint) -> (kid -> typ) -> typ
 val exc_typ : typ
 
-val inc_ord : order
-val dec_ord : order
-
 (* Vector with default order. *)
 val dvector_typ : Env.t -> nexp -> nexp -> typ -> typ