Fix undefined nvar occurrences that were impacting ARM

3 files changed, 12 insertions, 8 deletions

diff --git a/src/rewriter.ml b/src/rewriter.ml
index 496132b8..235b4f5f 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -89,6 +89,7 @@ let fix_effsum_exp (E_aux (e,(l,annot))) =
     | E_let (lb,e) -> union_effs [get_effsum_lb lb;get_effsum_exp e]
     | E_assign (lexp,e) -> union_effs [get_effsum_lexp lexp;get_effsum_exp e]
     | E_exit e -> get_effsum_exp e
+    | E_assert (c,m) -> pure_e
     | E_internal_cast (_,e) -> get_effsum_exp e
     | E_internal_exp _ -> pure_e
     | E_internal_exp_user _ -> pure_e
@@ -343,7 +344,7 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) =
              | Nconst i1 -> if nexp_eq n1 n2 then new_exp else rewrap (E_cast (t_to_typ t,new_exp))
              | _ -> (match o1.order with
                  | Odec -> 
-                   (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" 
+               (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" 
                      (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in*)
                    rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"),Parse_ast.Generated l)),
                                             Parse_ast.Generated l),new_exp))
@@ -356,8 +357,8 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) =
           | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]) ->
             (match o1.order with
              | Odec -> 
-               (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" 
-                 (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in*)
+               let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n" 
+                 (n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in
                rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Parse_ast.Generated l)),
                                         Parse_ast.Generated l), new_exp))
              | _ -> new_exp)
@@ -367,7 +368,7 @@ 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\n" (t_to_string t) 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;_;_])}])
diff --git a/src/type_internal.ml b/src/type_internal.ml
index d4eeefdf..22e79de8 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1442,6 +1442,7 @@ let cons_efs_annot t cs efl efr = Base(([],t),Emp_local,cs,efl,efr,nob)
 let efs_annot t efl efr = Base(([],t),Emp_local,[],efl,efr,nob)
 let tag_efs_annot t tag efl efr = Base(([],t),tag,[],efl,efr,nob)
 let cons_bs_annot t cs bs = Base(([],t),Emp_local,cs,pure_e,pure_e,bs)
+let cons_bs_annot_efr t cs bs efr = Base(([],t), Emp_local, cs, pure_e, efr, bs)
 
 let initial_abbrev_env =
   Envmap.from_list [
@@ -2839,13 +2840,13 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
         let cs = [] (*[LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] (*This constraint failing should be a warning, but truncation is ok*)*)  in
-        let tannot = (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))) in
+        let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in
         (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),
                                   [(E_aux(E_internal_exp(tannot), tannot));e]),tannot))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
         let cs = [] (* See above [LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in
-        let tannot = (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))) in
+        let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in
         (*let _ = Printf.eprintf "Generating to_vec_dec call: bounds are %s\n" (bounds_to_string bounds) in*)
         (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),
                                   [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot))
@@ -2859,13 +2860,14 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
         [TA_nexp b2] -> 
         let cs = [](*[LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in
-        let tannot = (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))) in
+        let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in
         (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),
                                   [(E_aux(E_internal_exp(tannot), tannot));e]),tannot))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
         [TA_nexp b2] -> 
         let cs = [](*[LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)]*) in
-        let tannot = (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))) in
+        let tannot = (l, cons_bs_annot_efr t2 cs bounds (get_cummulative_effects (get_eannot e))) in
+        (*let _ = Printf.eprintf "Generating to_vec_dec call: bounds are %s\n" (bounds_to_string bounds) in*)
         (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),
                                   [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 3ce965c1..1748f0a7 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -224,6 +224,7 @@ val cons_efs_annot : t -> nexp_range list -> effect -> effect -> tannot
 val efs_annot : t -> effect -> effect -> tannot
 val tag_efs_annot: t -> tag -> effect -> effect -> tannot
 val cons_bs_annot : t -> nexp_range list -> bounds_env -> tannot
+val cons_bs_annot_efr : t -> nexp_range list -> bounds_env -> effect -> tannot
 
 
 val t_to_string : t -> string