Fix sizeof code generation to look at parameter bounds

4 files changed, 8 insertions, 2 deletions

diff --git a/src/rewriter.ml b/src/rewriter.ml
index d3d843f3..f9959814 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -375,9 +375,10 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) =
   | E_internal_exp (l,impl) ->
     (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 bounds = match nmap with | None -> bounds | Some (nm,_) -> add_map_to_bounds nm bounds in
+       (*let _ = Printf.eprintf "Bounds after looking at nmap %s\n" (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;_;_])}])
@@ -406,6 +407,7 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) =
        (match t.t with
         | Tapp("atom",[TA_nexp n]) ->
           let nexps = expand_nexp n in
+          (*let _ = Printf.eprintf "Removing sizeof_internal with type %s\n" (t_to_string t) 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)
diff --git a/src/type_check.ml b/src/type_check.ml
index ef07d4aa..bd576dbb 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1374,7 +1374,7 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool)
       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 nannot = bounds_annot n_typ b_env 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)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 0864009a..ff6cd08d 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1896,6 +1896,8 @@ let tag_annot t tag = Base(([],t),tag,[],pure_e,pure_e,nob)
 let tag_annot_efr t tag efr = Base(([],t),tag,[],pure_e,efr,nob)
 let constrained_annot t cs = Base(([],t),Emp_local,cs,pure_e,pure_e,nob)
 let constrained_annot_efr t cs efr = Base(([],t),Emp_local,cs,pure_e,efr,nob)
+let bounds_annot t bs = Base(([],t),Emp_local,[],pure_e,pure_e,bs)
+let bounds_annot_efr t bs efr = Base(([],t),Emp_local,[],pure_e,efr,bs)
 let cons_tag_annot t tag cs = Base(([],t),tag,cs,pure_e,pure_e,nob)
 let cons_tag_annot_efr t tag cs efr = Base(([],t),tag,cs,pure_e,efr,nob)
 let cons_efl_annot t cs ef = Base(([],t),Emp_local,cs,ef,pure_e,nob)
diff --git a/src/type_internal.mli b/src/type_internal.mli
index a44aa519..fc274409 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -226,6 +226,8 @@ val tag_annot : t -> tag -> tannot
 val tag_annot_efr : t -> tag -> effect -> tannot
 val constrained_annot : t -> constraints -> tannot
 val constrained_annot_efr : t -> constraints -> effect -> tannot
+val bounds_annot : t -> bounds_env -> tannot
+val bounds_annot_efr : t -> bounds_env -> effect -> tannot
 val cons_tag_annot : t -> tag -> constraints -> tannot
 val cons_tag_annot_efr : t -> tag -> constraints -> effect -> tannot
 val cons_efl_annot : t -> constraints -> effect -> tannot