Add sizeof to sail. Documentation to follow

10 files changed, 73 insertions, 15 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index efa6b8e8..a539d268 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -441,6 +441,7 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
     | 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_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_exit exp -> E_exit(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,NoTyp))
diff --git a/src/initial_check_full_ast.ml b/src/initial_check_full_ast.ml
index 1d5a8c98..86c1dd2c 100644
--- a/src/initial_check_full_ast.ml
+++ b/src/initial_check_full_ast.ml
@@ -344,6 +344,7 @@ and to_exp (k_env : kind Envmap.t) (def_ord : Ast.order) (E_aux(exp,(l,_)) :  ex
     | E_case(exp,pexps) -> E_case(to_exp k_env def_ord exp, List.map (to_case k_env def_ord) pexps)
     | E_let(leb,exp) -> E_let(to_letbind k_env def_ord leb, to_exp k_env def_ord exp)
     | E_assign(lexp,exp) -> E_assign(to_lexp k_env def_ord lexp, to_exp k_env def_ord exp)
+    | E_sizeof(nexp) -> E_sizeof(to_nexp k_env nexp)
     | E_exit exp -> E_exit(to_exp k_env def_ord exp)
     | E_assert(cond,msg) -> E_assert(to_exp k_env def_ord cond, to_exp k_env def_ord msg)
     | E_comment s -> E_comment s
diff --git a/src/lexer.mll b/src/lexer.mll
index 71295eda..d8f530b6 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -96,6 +96,7 @@ let kw_table =
      ("rec",			 (fun x -> Rec));
      ("register",		 (fun x -> Register));
      ("scattered",               (fun x -> Scattered));
+     ("sizeof",                  (fun x -> Sizeof));
      ("struct",                  (fun x -> Struct));
      ("switch",			 (fun x -> Switch));
      ("then",                    (fun x -> Then));
diff --git a/src/parser.mly b/src/parser.mly
index 00bcb465..926b9515 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -134,7 +134,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 Foreach Function_ If_ In IN Inc Let_ Member Nat Order 
-%token Pure Rec Register Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef 
+%token Pure Rec Register Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
 %token Undefined Union With Val
 %token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Undef Unspec Nondet Escape
 
@@ -589,6 +589,8 @@ atomic_exp:
     { eloc (E_list($2)) }
   | Switch exp Lcurly case_exps Rcurly
     { eloc (E_case($2,$4)) }
+  | Sizeof nexp_typ
+    { eloc (E_sizeof($2)) }
   | Exit atomic_exp
       { eloc (E_exit $2) }
   | Assert Lparen exp Comma exp Rparen
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll
index f6ccd3c2..818f8fe6 100644
--- a/src/pre_lexer.mll
+++ b/src/pre_lexer.mll
@@ -91,6 +91,7 @@ let kw_table =
      ("register",		 (fun x -> Other));
      ("scattered",               (fun x -> Other));
      ("struct",                  (fun x -> Other));
+     ("sizeof",                  (fun x -> Other));
      ("switch",			 (fun x -> Other));
      ("then",                    (fun x -> Other));
      ("true",                    (fun x -> Other));
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 1c5f891a..25b81fb7 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -429,6 +429,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
       fprintf ppf "@[<0>(E_aux (%a %a [%a]) (%a, %a))@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot
     | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_let" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot
+    | E_sizeof nexp -> fprintf ppf "@[<0>(E_aux (E_sizeof %a) (%a, %a))@]" pp_lem_nexp nexp pp_lem_l l pp_annot annot
     | E_exit exp -> fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_assert(c,msg) ->
       fprintf ppf "@[<0>(E_aux (E_assert %a %a) (%a, %a))@]" pp_lem_exp c pp_lem_exp msg pp_lem_l l pp_annot annot
@@ -750,7 +751,14 @@ let doc_typ, doc_atomic_typ, doc_nexp =
     (doc_id id) ^^ (brackets (if n = m then doc_int m else doc_op colon (doc_int m) (doc_int (n-1))))
   | Typ_app(Id_aux (Id "vector", _), [
       Typ_arg_aux(Typ_arg_nexp
-                  (Nexp_aux(Nexp_minus (n', Nexp_aux((Nexp_constant 1), _)),_) as n_n),_);
+                    (Nexp_aux(Nexp_minus (n', Nexp_aux((Nexp_constant 1), _)),_) as n_n),_);
+      Typ_arg_aux(Typ_arg_nexp m_nexp, _);
+      Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _);
+      Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
+    (doc_id id) ^^ (brackets (if n' = m_nexp then nexp m_nexp else doc_op colon (nexp m_nexp) (nexp n_n)))
+  | Typ_app(Id_aux (Id "vector", _), [
+      Typ_arg_aux(Typ_arg_nexp
+                  (Nexp_aux(Nexp_sum (n', Nexp_aux((Nexp_constant -1), _)),_) as n_n),_);
       Typ_arg_aux(Typ_arg_nexp m_nexp, _);
       Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _);
       Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
@@ -1038,6 +1046,8 @@ let doc_exp, doc_let =
       let opening = separate space [string "switch"; exp e; lbrace] in
       let cases = separate_map (break 1) doc_case pexps in
       surround 2 1 opening cases rbrace
+  | E_sizeof n ->
+    separate space [string "sizeof"; doc_nexp n]
   | E_exit e ->
     separate space [string "exit"; atomic_exp e;]
   | E_assert(c,m) ->
diff --git a/src/rewriter.ml b/src/rewriter.ml
index d9e3925b..b8e60ef9 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -328,6 +328,7 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) =
                           Pat_aux (Pat_exp(rewriters.rewrite_pat rewriters nmap p,rewrite e),pannot)) pexps)))
   | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite body))
   | E_assign (lexp,exp) -> rewrap (E_assign(rewriters.rewrite_lexp rewriters nmap lexp,rewrite exp))
+  | E_sizeof n -> rewrap (E_sizeof n)
   | E_exit e -> rewrap (E_exit (rewrite e))
   | E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2))
   | E_internal_cast ((l,casted_annot),exp) -> 
@@ -335,7 +336,8 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) =
     (*let _ = Printf.eprintf "Removing an internal_cast with %s\n" (tannot_to_string casted_annot) in*)
     (match casted_annot,exp with
      | Base((_,t),_,_,_,_,_),E_aux(ec,(ecl,Base((_,exp_t),_,_,_,_,_))) ->
-       (*let _ = Printf.eprintf "Considering removing an internal cast where the two types are %s and %s\n" (t_to_string t) (t_to_string exp_t) in*)
+       (*let _ = Printf.eprintf "Considering removing an internal cast where the two types are %s and %s\n" 
+         (t_to_string t) (t_to_string exp_t) in*)
        (match t.t,exp_t.t with
         (*TODO should pass d_env into here so that I can look at the abbreviations if there are any here*)
         | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]),
@@ -370,7 +372,8 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) =
     (match impl with
      | Base((_,t),_,_,_,_,bounds) ->
        let bounds = match nmap with | None -> bounds | Some (nm,_) -> add_map_to_bounds nm bounds in
-       (*let _ = Printf.eprintf "Rewriting internal expression, with type %s, and bounds %s\n" (t_to_string t) (bounds_to_string bounds) in*)
+       (*let _ = Printf.eprintf "Rewriting internal expression, with type %s, and bounds %s\n" 
+         (t_to_string t) (bounds_to_string bounds) in*)
        (match t.t with
         (*Old case; should possibly be removed*)
         | Tapp("register",[TA_typ {t= Tapp("vector",[ _; TA_nexp r;_;_])}])
@@ -391,6 +394,18 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) =
           raise (Reporting_basic.err_unreachable l 
                    ("Internal_exp given unexpected types " ^ (t_to_string t))))
      | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given none Base annot")))
+  | E_sizeof_internal (l,impl) ->
+    (match impl with
+     | Base((_,t),_,_,_,_,bounds) ->
+       let bounds = match nmap with | None -> bounds | Some (nm,_) -> add_map_to_bounds nm bounds in
+       (match t.t with
+        | Tapp("atom",[TA_nexp n]) ->
+          let nexps = expand_nexp n in
+          (match (match_to_program_vars nexps bounds) with
+           | [] -> rewrite_nexp_to_exp None l n
+           | map -> rewrite_nexp_to_exp (Some map) l n)
+        | _ -> raise (Reporting_basic.err_unreachable l ("Sizeof internal had non-atom type " ^ (t_to_string t))))
+     | _ -> raise (Reporting_basic.err_unreachable l ("Sizeof internal had none base annot")))
   | E_internal_exp_user ((l,user_spec),(_,impl)) -> 
     (match (user_spec,impl) with
      | (Base((_,tu),_,_,_,_,_), Base((_,ti),_,_,_,_,bounds)) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index 9a49728c..46c01908 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -695,7 +695,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
             type_coerce (Expr l) d_env Require false false b_env ret 
               (E_aux (E_app(id,internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,efr,nob))))) expect_t
           | (IP_none,_) -> 
-            (*let _ = Printf.eprintf "no implicit: ret %s and expect_t %s\n" (t_to_string ret) (t_to_string expect_t) in*)
+          (*let _ = Printf.eprintf "no implicit: ret %s and expect_t %s\n" (t_to_string ret) (t_to_string expect_t) in*)
             type_coerce (Expr l) d_env Require false false b_env ret 
               (E_aux (E_app(id, parms),(l,(Base(([],ret),tag,cs,ef,efr,nob))))) expect_t
       in
@@ -899,7 +899,8 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
          merge_bounds then_bs else_bs,
          sub_effects))
     | E_for(id,from,to_,step,order,block) -> 
-      (*TOTHINK Instead of making up new ns here, perhaps I should instead make sure they conform to range without coercion as these nu variables are likely floating*)
+      (*TOTHINK Instead of making up new ns here, perhaps I should instead make sure they conform to range 
+        without coercion as these nu variables are likely floating*)
       let f,t,s = new_n(),new_n(),new_n() in
       let ft,tt,st = mk_atom f, mk_atom t, mk_atom s in
       let from',from_t,_,from_c,_,from_ef = check_exp envs imp_param false ft from in
@@ -915,7 +916,8 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
       in 
       (*TODO Might want to extend bounds here for the introduced variable*)
       let (block',b_t,_,b_c,_,b_ef)=
-        check_exp (Env(d_env,Envmap.insert t_env (id_to_string id,new_annot),b_env,tp_env)) imp_param true expect_t block
+        check_exp (Env(d_env,Envmap.insert t_env (id_to_string id,new_annot),b_env,tp_env))
+          imp_param true expect_t block
       in
       let sub_effects = union_effects b_ef (union_effects step_ef (union_effects to_ef from_ef)) in
       (E_aux(E_for(id,from',to_',step',order,block'),(l,constrained_annot_efr b_t local_cs sub_effects)),expect_t,
@@ -1232,8 +1234,9 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
       (match t'.t with
         | Tid i | Tabbrev(_, {t=Tid i}) | Tapp(i,_) ->
           (match lookup_record_typ i d_env.rec_env with
-            | Some((i,Register,tannot,fields)) -> typ_error l "Expected a struct for this update, instead found a register"
-            | Some(((i,Record,(Base((params,t),tag,cs,eft,_,bounds)),fields) as r)) ->
+           | Some((i,Register,tannot,fields)) ->
+             typ_error l "Expected a struct for this update, instead found a register"
+           | Some(((i,Record,(Base((params,t),tag,cs,eft,_,bounds)),fields) as r)) ->
               if (List.length fexps <= List.length fields) 
               then 
                 let (ts,cs,eft,subst_env) = subst params false false t cs eft in
@@ -1326,7 +1329,8 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
     | E_let(lbind,body) -> 
       let (lb',t_env',cs,b_env',ef) = (check_lbind envs imp_param false Emp_local lbind) in
       let new_env = 
-        (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env false) t_env t_env', merge_bounds b_env' b_env,tp_env)) 
+        (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env false)
+               t_env t_env', merge_bounds b_env' b_env,tp_env)) 
       in
       let (e,t,_,cs',_,ef') = check_exp new_env imp_param true expect_t body in
       let effects = union_effects ef ef' in
@@ -1339,11 +1343,20 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
       let (exp',t'',_,cs',_,efr') = check_exp envs imp_param true t' exp in
       let (t',c') = type_consistent (Expr l) d_env Require false unit_t expect_t in
       let effects = union_effects efl (union_effects efr efr') in
-      (E_aux(E_assign(lexp',exp'),(l,(Base(([],unit_t),tag,[],efl,effects,nob)))),unit_t,t_env',cs@cs'@c',b_env',effects)
+      (E_aux(E_assign(lexp',exp'),(l,(Base(([],unit_t),tag,[],efl,effects,nob)))),
+       unit_t,t_env',cs@cs'@c',b_env',effects)
     | E_exit e ->
       let (e',t',_,_,_,_) = check_exp envs imp_param true (new_t ()) e in
       let efs = add_effect (BE_aux(BE_escape, l)) pure_e in
       (E_aux (E_exit e',(l,(simple_annot_efr expect_t efs))),expect_t,t_env,[],nob,efs)
+    | E_sizeof nexp ->
+      let n = anexp_to_nexp envs nexp in
+      let n_subst = subst_n_with_env tp_env n in
+      let n_typ = mk_atom n_subst in
+      let nannot = simple_annot n_typ in
+      let e = E_aux (E_sizeof_internal (l, nannot), (l,nannot)) in      
+      let t',cs,ef,e' = type_coerce (Expr l) d_env Require false false b_env n_typ e expect_t in
+      (e',t',t_env,cs,nob,ef)
     | E_assert(cond,msg) ->
       let (cond',t',_,_,_,_) = check_exp envs imp_param true bit_t cond in
       let (msg',mt',_,_,_,_) = check_exp envs imp_param true {t= Tapp("option",[TA_typ string_t])} msg in
@@ -1354,7 +1367,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
     | E_comment_struc e ->
       (E_aux (E_comment_struc e, (l, simple_annot unit_t)), expect_t,t_env,[],nob,pure_e)
     | E_internal_cast _ | E_internal_exp _ | E_internal_exp_user _ | E_internal_let _
-    | E_internal_plet _ | E_internal_return _ -> 
+    | E_internal_plet _ | E_internal_return _ | E_sizeof_internal _ -> 
       raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
 
 and recheck_for_register envs imp_param expect_t exp = 
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 92abbe04..1718364f 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -628,7 +628,7 @@ let rec normalize_n_rec recur_ok n =
     (match first_non_nu (get_outer_most n) with
      | None -> n
      | Some n' -> n')
-  | Nconst _ | Nvar _ | Nuvar _ | Npos_inf | Nneg_inf | Ninexact -> n
+  | Nconst _ | Nvar _ | Npos_inf | Nneg_inf | Ninexact -> n
   | Nneg n -> 
     let n',to_recur,add_neg = (match n.nexp with
       | Nconst i -> negate n,false,false
@@ -2396,8 +2396,18 @@ let initial_typ_env =
     ("abs",Base(((mk_nat_params ["n";"m";]),
                  (mk_pure_fun (mk_atom (mk_nv "n")) (mk_range n_zero (mk_nv "m")))),
                 External (Some "abs"),[],pure_e,pure_e,nob));
+    ("max",
+     Base(((mk_nat_params ["n";"m";"o"]),
+           (mk_pure_fun (mk_tup [(mk_atom (mk_nv "n"));(mk_atom (mk_nv "m"))])
+                        (mk_atom (mk_nv "o")))),
+          External (Some "max"),[],pure_e,pure_e,nob));
+    ("min",
+     Base(((mk_nat_params ["n";"m";"o"]),
+           (mk_pure_fun (mk_tup [(mk_atom (mk_nv "n"));(mk_atom (mk_nv "m"))])
+                        (mk_atom (mk_nv "o")))),
+          External (Some "min"),[],pure_e,pure_e,nob));
   ]
-
+    
 
 let rec typ_subst s_env leave_imp t =
   match t.t with
@@ -2482,6 +2492,8 @@ let rec cs_subst t_env cs =
 let subst_with_env env leave_imp t cs e =
   (typ_subst env leave_imp t, cs_subst env cs, e_subst env e, env)
 
+let subst_n_with_env = n_subst 
+
 let subst (k_env : (Envmap.k * kind) list) (leave_imp:bool) (use_var:bool)
           (t : t) (cs : nexp_range list) (e : effect) : (t * nexp_range list * effect * t_arg emap) =
   let subst_env = Envmap.from_list
@@ -2491,7 +2503,8 @@ let subst (k_env : (Envmap.k * kind) list) (leave_imp:bool) (use_var:bool)
                               | K_Nat -> TA_nexp (if use_var then (new_nv id) else (new_n ()))
                               | K_Ord -> TA_ord (new_o ())
                               | K_Efct -> TA_eft (new_e ())
-                              | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "substitution given an environment with a non-base-kind kind"))) k_env) 
+                              | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown
+                                              "substitution given an environment with a non-base-kind kind"))) k_env) 
   in
   subst_with_env subst_env leave_imp t cs e
 
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 17e7aaed..0b4ecdb2 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -251,6 +251,7 @@ val equate_t : t -> t -> unit
 val typ_subst : t_arg emap -> bool -> t -> t 
 val subst : (Envmap.k * kind) list -> bool -> bool -> t -> nexp_range list -> effect -> t * nexp_range list * effect * t_arg emap
 val subst_with_env : t_arg emap -> bool -> t -> nexp_range list -> effect -> t * nexp_range list * effect * t_arg emap
+val subst_n_with_env : t_arg emap -> nexp -> nexp
 val type_param_consistent : Parse_ast.l -> t_arg emap -> t_arg emap -> nexp_range list
 
 val get_abbrev : def_envs -> t -> (t * nexp_range list)