Optionally generate an initial register state for the sequential Lem shallow embedding

Checks for command-line flag -undefined_gen and uses the undefined value
generator functions of the form undefined_typ to initialise registers

4 files changed, 62 insertions, 31 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 8106f89c..92628014 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -755,3 +755,27 @@ and tyvars_of_typ_arg (Typ_arg_aux (ta,_)) =
   | Typ_arg_nexp nexp -> tyvars_of_nexp nexp
   | Typ_arg_typ typ -> tyvars_of_typ typ
   | Typ_arg_order _ -> KidSet.empty
+
+let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) =
+  let wrap e_aux typ = E_aux (e_aux, (l, annot typ)) in
+  match typ_aux with
+  | Typ_id id ->
+     wrap (E_app (prepend_id "undefined_" id, [wrap (E_lit (mk_lit L_unit)) unit_typ])) typ
+  | Typ_app (_,[start;size;_;_]) when mwords && is_bitvector_typ typ ->
+     wrap (E_app (mk_id "undefined_bitvector",
+       undefined_of_typ_args mwords l annot start @
+       undefined_of_typ_args mwords l annot size)) typ
+  | Typ_app (id, args) ->
+     wrap (E_app (prepend_id "undefined_" id,
+       List.concat (List.map (undefined_of_typ_args mwords l annot) args))) typ
+  | Typ_var kid ->
+     (* FIXME: bit of a hack, need to add a restriction to how
+        polymorphic undefined can be in the type checker to
+        guarantee this always works. *)
+     wrap (E_id (prepend_id "typ_" (id_of_kid kid))) typ
+  | Typ_fn _ -> assert false
+and undefined_of_typ_args mwords l annot (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
+  match typ_arg_aux with
+  | Typ_arg_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))]
+  | Typ_arg_typ typ -> [undefined_of_typ mwords l annot typ]
+  | Typ_arg_order _ -> []
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 1a056e58..8f1f06e6 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -244,3 +244,5 @@ val effect_set : effect -> BESet.t
 
 val tyvars_of_nexp : nexp -> KidSet.t
 val tyvars_of_typ : typ -> KidSet.t
+
+val undefined_of_typ : bool -> Ast.l -> (typ -> 'annot) -> typ -> 'annot exp
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 3832c187..d6ec25dc 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -84,6 +84,8 @@ let rec fix_id remove_tick name = match name with
   | _ ->
      if String.contains name '#' then
        fix_id remove_tick (String.concat "_" (Util.split_on_char '#' name))
+     else if String.contains name '?' then
+       fix_id remove_tick (String.concat "_pat_" (Util.split_on_char '?' name))
      else if name.[0] = '\'' then
        let var = String.sub name 1 (String.length name - 1) in
        if remove_tick then var else (var ^ "'")
@@ -337,8 +339,8 @@ and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with
   | _ -> false
 
 let doc_tannot_lem sequential mwords eff typ =
-  (* if contains_t_pp_var typ then empty
-  else *)
+  if contains_t_pp_var typ then empty
+  else
     let ta = doc_typ_lem sequential mwords typ in
     if eff then string " : _M " ^^ parens ta
     else string " : " ^^ ta
@@ -708,7 +710,7 @@ let doc_exp_lem, doc_let_lem =
              currently broken. *)
           let [arg] = args in
           let targ = typ_of arg in
-          let call = if mwords && is_bitvector_typ targ then "bitvector_length" else "length" in
+          let call = if (*mwords &&*) is_bitvector_typ targ then "bitvector_length" else "vector_length" in
           let epp = separate space [string call;expY arg] in
           if aexp_needed then parens (align epp) else epp
        (*)| Id_aux (Id "bool_not", _) ->
@@ -915,8 +917,8 @@ let doc_exp_lem, doc_let_lem =
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
        let recordtyp = match annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
-         | Some (env, Typ_aux (Typ_app (tid, _), _), _)
-           when Env.is_record tid env ->
+         | Some (env, Typ_aux (Typ_app (tid, _), _), _) ->
+           (* when Env.is_record tid env -> *)
            tid
          | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        let epp = anglebars (space ^^ (align (separate_map
@@ -1586,7 +1588,7 @@ let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls)
   match fcls with
   | [] -> failwith "FD_function with empty function list"
   | FCL_aux (FCL_Funcl(id,_,exp),_) :: _
-    when string_of_id id = "execute" || string_of_id id = "initial_analysis" ->
+    when string_of_id id = "execute" (*|| string_of_id id = "initial_analysis"*) ->
     let (_,auxiliary_functions,clauses) =
       List.fold_left
         (fun (already_used_fnames,auxiliary_functions,clauses) funcl ->
@@ -1680,6 +1682,8 @@ let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
 let doc_spec_lem sequential mwords (VS_aux (valspec,annot)) =
   match valspec with
   | VS_val_spec (typschm,id,None,_) ->
+     (* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in
+     if contains_t_pp_var typ then empty else *)
      separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem sequential mwords true typschm] ^/^ hardline 
   | VS_val_spec (_,_,Some _,_) -> empty
 
@@ -1746,12 +1750,30 @@ let doc_regstate_lem mwords registers =
         Name_sect_aux (Name_sect_none, l),
         TypQ_aux (TypQ_tq [], l),
         List.map (fun (typ, id, env) -> (typ, id)) registers,
-        false) in
+        false)
+  in
+  let initregstate =
+    if !Initial_check.opt_undefined_gen then
+      let exp = match registers with
+        | [] -> E_aux (E_lit (mk_lit L_unit), (l, Some (Env.empty, unit_typ, no_effect)))
+        | _ ->
+           let initreg (typ, id, env) =
+             let annot typ = Some (env, typ, no_effect) in
+             let initval = undefined_of_typ mwords l annot typ in
+             FE_aux (FE_Fexp (id, initval), (l, annot typ)) in
+           E_aux (
+             E_record (FES_aux (FES_Fexps (List.map initreg registers, false), annot)),
+             (l, Some (Env.empty, mk_id_typ (mk_id "regstate"), no_effect)))
+      in
+      doc_op equals (string "let initial_regstate") (doc_exp_lem true mwords false false exp)
+    else empty
+  in
   concat [
     doc_typdef_lem true mwords (TD_aux (regstate, annot)); hardline;
     hardline;
     string "type _M 'a = M regstate 'a"
-  ]
+  ],
+  initregstate
 
 let doc_register_refs_lem registers =
   let doc_register_ref (typ, id, env) =
@@ -1779,7 +1801,7 @@ let doc_register_refs_lem registers =
 let pp_defs_lem sequential mwords (types_file,types_modules) (defs_file,defs_modules) d top_line =
   (* let regtypes = find_regtypes d in *)
   let (typdefs,valdefs) = doc_defs_lem sequential mwords d in
-  let regstate_def = doc_regstate_lem mwords (find_registers d) in
+  let regstate_def, initregstate_def = doc_regstate_lem mwords (find_registers d) in
   let register_refs = doc_register_refs_lem (find_registers d) in
   (print types_file)
     (concat
@@ -1835,7 +1857,9 @@ let pp_defs_lem sequential mwords (types_file,types_modules) (defs_file,defs_mod
         (separate_map hardline)
           (fun lib -> separate space [string "open import";string lib]) defs_modules;hardline;
         hardline;
-        valdefs]);
+        valdefs;
+        hardline;
+        initregstate_def]);
   (* (print state_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
diff --git a/src/rewriter.ml b/src/rewriter.ml
index ba767081..34e4bfd4 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -2621,31 +2621,12 @@ 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 mwords =
-  let rec undefined_of_typ (Typ_aux (typ_aux, _) as typ) =
-    match typ_aux with
-    | Typ_id id ->
-       mk_exp (E_app (prepend_id "undefined_" id, [mk_lit_exp L_unit]))
-    | Typ_app (_,[start;size;_;_]) when mwords && is_bitvector_typ typ ->
-       mk_exp (E_app (mk_id "undefined_bitvector", undefined_of_typ_args start @ undefined_of_typ_args size))
-    | Typ_app (id, args) ->
-       mk_exp (E_app (prepend_id "undefined_" id, List.concat (List.map undefined_of_typ_args args)))
-    | Typ_var kid ->
-       (* FIXME: bit of a hack, need to add a restriction to how
-          polymorphic undefined can be in the type checker to
-          guarantee this always works. *)
-       mk_exp (E_id (prepend_id "typ_" (id_of_kid kid)))
-    | 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)) ->
-       check_exp (env_of exp) (undefined_of_typ (Env.expand_synonyms (env_of exp) (typ_of exp))) (typ_of exp)
+       check_exp (env_of exp) (undefined_of_typ mwords l (fun _ -> ()) (Env.expand_synonyms (env_of exp) (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