Add dynamic footprint dependency check event/outcome

Also fix type checker bug in not reporting modifications to parameter values

17 files changed, 161 insertions, 63 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 5441587d..6291acba 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -68,6 +68,7 @@ type base_effect_aux =  (* effect *)
  | BE_rmem (* read memory *)
  | BE_wmem (* write memory *)
  | BE_barr (* memory barrier *)
+ | BE_depend (* dynamic footprint *)
  | BE_undef (* undefined-instruction exception *)
  | BE_unspec (* unspecified values *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
diff --git a/language/l2.ml b/language/l2.ml
index 2b5f04ce..6ce6a064 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -65,6 +65,7 @@ base_effect_aux =  (* effect *)
  | BE_rmem (* read memory *)
  | BE_wmem (* write memory *)
  | BE_barr (* memory barrier *)
+ | BE_depend (* dynamic footprint *)
  | BE_undef (* undefined-instruction exception *)
  | BE_unspec (* unspecified values *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
diff --git a/language/l2.ott b/language/l2.ott
index 59de79cd..b1e1dfb1 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -187,6 +187,7 @@ base_effect :: 'BE_' ::=
   | rmem                                :: :: rmem {{ com read memory }}
   | wmem                                :: :: wmem {{ com write memory }}
   | barr                                :: :: barr {{ com memory barrier }}
+  | depend				:: :: depend {{ com dynamic footprint }}
   | undef                               :: :: undef {{ com undefined-instruction exception }}
   | unspec                              :: :: unspec {{ com unspecified values }}
   | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index f4cb278a..f2ee40c1 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -47,6 +47,7 @@ base_effect_aux =  (* effect *)
  | BE_rmem (* read memory *)
  | BE_wmem (* write memory *)
  | BE_barr (* memory barrier *)
+ | BE_depend (* dynmically dependent footprint *)
  | BE_undef (* undefined-instruction exception *)
  | BE_unspec (* unspecified values *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index 7126b9e0..1945c926 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -156,6 +156,7 @@ base_effect :: 'BE_' ::=
   | rmem                                :: :: rmem {{ com read memory }}
   | wmem                                :: :: wmem {{ com write memory }}
   | barr                                :: :: barr {{ com memory barrier }}
+  | depend				:: :: depend {{ com dynmically dependent footprint }}
   | undef                               :: :: undef {{ com undefined-instruction exception }}
   | unspec                              :: :: unspec {{ com unspecified values }}
   | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 8c613f36..06eccbaf 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -227,14 +227,15 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect =
                              (fun efct -> match efct with
                              | Parse_ast.BE_aux(e,l) ->
                                BE_aux((match e with 
-                               | Parse_ast.BE_barr  -> BE_barr
-                               | Parse_ast.BE_rreg  -> BE_rreg
-                               | Parse_ast.BE_wreg  -> BE_wreg
-                               | Parse_ast.BE_rmem  -> BE_rmem
-                               | Parse_ast.BE_wmem  -> BE_wmem
-                               | Parse_ast.BE_undef -> BE_undef
-                               | Parse_ast.BE_unspec-> BE_unspec
-                               | Parse_ast.BE_nondet-> BE_nondet),l))
+                               | Parse_ast.BE_barr   -> BE_barr
+                               | Parse_ast.BE_rreg   -> BE_rreg
+                               | Parse_ast.BE_wreg   -> BE_wreg
+                               | Parse_ast.BE_rmem   -> BE_rmem
+                               | Parse_ast.BE_wmem   -> BE_wmem
+			       | Parse_ast.BE_depend -> BE_depend
+                               | Parse_ast.BE_undef  -> BE_undef
+                               | Parse_ast.BE_unspec -> BE_unspec
+                               | Parse_ast.BE_nondet -> BE_nondet),l))
                              effects)
                | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None None
     ), l)
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index a3bd294a..b1a23a5e 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -215,6 +215,7 @@ type action =
  | Read_mem of id * value * maybe (nat * nat)
  | Write_mem of id * value * maybe (nat * nat) * value
  | Barrier of id * value
+ | Footprint of id * value
  | Write_next_IA of value (* Perhaps not needed? *)
  | Nondet of list (exp tannot)
  | Call_extern of string * value
@@ -1830,6 +1831,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
           then 
             (Action (Barrier (id_of_string name_ext) v)
                     (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
+	  else if has_depend_effect effects
+	  then 
+	    (Action (Footprint (id_of_string name_ext) v)
+	            (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
 	  else if has_wmem_effect effects
 	  then 
 	    let (wv,v) =
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 4a9964e2..2af90d6f 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -456,6 +456,8 @@ let rec interp_to_outcome mode context thunk =
 	| Just barrier -> 
 	  Barrier barrier (IState next_state context)
 	| _ -> Error ("Barrier " ^ i ^ " function not found") end
+    | Interp.Footprint (Id_aux (Id i) _) lval ->
+      Footprint (IState next_state context)
     | Interp.Nondet exps -> 
       let nondet_states = List.map (Interp.set_in_context next_state) exps in
       Nondet_choice (List.map (fun i -> IState i context) nondet_states) (IState next_state context)
@@ -540,6 +542,8 @@ let rec ie_loop mode register_values (IState interp_state context) =
       (E_write_mem write_k loc length tracking value v_tracking)::(ie_loop mode register_values (i_state_fun true))
     | Barrier barrier_k i_state ->
       (E_barrier barrier_k)::(ie_loop mode register_values i_state)
+    | Footprint i_state ->
+      E_footprint::(ie_loop mode register_values i_state)
     | Internal _ _ next -> (ie_loop mode register_values next)
      end ;;
   
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 830877e1..2699fc38 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -272,6 +272,8 @@ type outcome =
 | Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state)
 (* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
+(* Tell the system to dynamically recalculate dependency footprint *)
+| Footprint of instruction_state
 (* Request to read register, will track dependency when mode.track_values *)
 | Read_reg of reg_name * (register_value -> instruction_state) 
 (* Request to write register *)
@@ -289,6 +291,7 @@ type event =
 | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
 | E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
 | E_barrier of barrier_kind
+| E_footprint 
 | E_read_reg of reg_name
 | E_write_reg of reg_name * register_value
 | E_escape
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 2790aee7..d83341c8 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -10,6 +10,11 @@ open import Bool
 
 type signed = Unsigned | Signed
 
+let rec power (a: integer) (b: integer) : integer =
+ if b <= 0 
+ then 1
+ else a * (power a (b-1))
+
 let hardware_mod (a: integer) (b:integer) : integer = 
  if a < 0 && b < 0
  then (abs a) mod (abs b)
@@ -638,6 +643,7 @@ let library_functions direction = [
   ("quot_overflow_vec", arith_op_overflow_vec_no0 hardware_quot "quot" Unsigned 1);
   ("quot_vec_signed", arith_op_vec_no0 hardware_quot "quot" Signed 1);
   ("quot_overflow_vec_signed", arith_op_overflow_vec_no0 hardware_quot "quot" Signed 1);
+  ("power", arith_op power);
   ("eq", eq);
   ("eq_vec_range", eq_vec_range);
   ("eq_range_vec", eq_range_vec);
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index e87600a3..dab33767 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -17,18 +17,18 @@ let unit_t = Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown
 val lit_eq: lit -> lit -> bool
 let lit_eq (L_aux left _) (L_aux right _) =
    match (left, right) with
-   | (L_unit, L_unit) -> true
    | (L_zero, L_zero) -> true
    | (L_one, L_one) -> true
-   | (L_true, L_true) -> true
-   | (L_false, L_false) -> true
+   | (L_bin b, L_bin b') -> b = b'
+   | (L_hex h, L_hex h') -> h = h'
    | (L_zero, L_num i) -> i = 0
    | (L_num i,L_zero) -> i = 0
    | (L_one, L_num i) -> i = 1
    | (L_num i, L_one) -> i = 1
    | (L_num n, L_num m) -> n = m
-   | (L_hex h, L_hex h') -> h = h'
-   | (L_bin b, L_bin b') -> b = b'
+   | (L_unit, L_unit) -> true
+   | (L_true, L_true) -> true
+   | (L_false, L_false) -> true
    | (L_undef, L_undef) -> true
    | (L_string s, L_string s') -> s = s'
    | (_, _) -> false
@@ -50,6 +50,7 @@ end
 val has_rmem_effect : list base_effect -> bool
 val has_barr_effect : list base_effect -> bool
 val has_wmem_effect : list base_effect -> bool
+val has_depend_effect : list base_effect -> bool
 let rec has_effect which efcts =
   match efcts with
   | [] -> false
@@ -69,6 +70,7 @@ let rec has_effect which efcts =
 let has_rmem_effect = has_effect BE_rmem
 let has_barr_effect = has_effect BE_barr
 let has_wmem_effect = has_effect BE_wmem
+let has_depend_effect = has_effect BE_depend
 
 let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
 let get_effects (Typ_aux t _) =
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index ca4abe17..76f216ee 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -82,6 +82,7 @@ let doc_effect (BE_aux (e,_)) =
   | BE_rmem -> "rmem"
   | BE_wmem -> "wmem"
   | BE_barr -> "barr"
+  | BE_depend -> "depend"
   | BE_undef -> "undef"
   | BE_unspec -> "unspec"
   | BE_nondet -> "nondet")
diff --git a/src/lexer.mll b/src/lexer.mll
index 2f6acf4d..2f07eeb9 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -112,6 +112,7 @@ let kw_table =
      ("rem",			 (fun x -> Rem));
 
      ("barr",                    (fun x -> Barr));
+     ("depend",                  (fun x -> Depend));
      ("rreg",                    (fun x -> Rreg));
      ("wreg",                    (fun x -> Wreg));
      ("rmem",                    (fun x -> Rmem));
diff --git a/src/parser.mly b/src/parser.mly
index 3f8b6db5..eb2ba153 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -135,7 +135,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
 %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 Undefined Union With Val
-%token Barr Rreg Wreg Rmem Wmem Undef Unspec Nondet
+%token Barr Depend Rreg Wreg Rmem Wmem Undef Unspec Nondet
 
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
@@ -306,6 +306,8 @@ kind:
 effect:
   | Barr
     { efl BE_barr }
+  | Depend
+    { efl BE_depend }
   | Rreg 
     { efl BE_rreg }
   | Wreg
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 9d9ed8a0..359335d3 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -143,6 +143,7 @@ and pp_format_base_effect_lem (BE_aux(e,l)) =
     | BE_rmem -> "BE_rmem"
     | BE_wmem -> "BE_wmem"
     | BE_barr -> "BE_barr"
+    | BE_depend -> "BE_depend"
     | BE_undef -> "BE_undef"
     | BE_unspec -> "BE_unspec"
     | BE_nondet -> "BE_nondet") ^ " " ^
@@ -641,6 +642,7 @@ let doc_effect (BE_aux (e,_)) =
   | BE_rmem -> "rmem"
   | BE_wmem -> "wmem"
   | BE_barr -> "barr"
+  | BE_depend -> "depend"
   | BE_undef -> "undef"
   | BE_unspec -> "unspec"
   | BE_nondet -> "nondet")
diff --git a/src/type_check.ml b/src/type_check.ml
index 8523ce85..deeff3d1 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1273,7 +1273,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let (e,t,_,cs',_,ef') = check_exp new_env imp_param expect_t body in
       (E_aux(E_let(lb',e),(l,simple_annot t)),t,t_env,cs@cs',nob,union_effects ef ef')
     | E_assign(lexp,exp) ->
-      let (lexp',t',t_env',tag,cs,b_env',ef) = check_lexp envs imp_param true lexp in
+      let (lexp',t',_,t_env',tag,cs,b_env',ef) = check_lexp envs imp_param true lexp in
       let (exp',t'',_,cs',_,ef') = check_exp envs imp_param t' exp in
       let (t',c') = type_consistent (Expr l) d_env Require false unit_t expect_t in
       (*let _ = Printf.eprintf "Constraints for E_assign %s\n" (constraints_to_string (cs@cs'@c')) in*)
@@ -1320,40 +1320,44 @@ and check_cases envs imp_param check_t expect_t pexps : ((tannot pexp) list * ty
       let (pes,tl,csl,efl) = check_cases envs imp_param check_t expect_t pexps in      
       ((Pat_aux(Pat_exp(pat',e),(l,cons_ef_annot t [cs] ef)))::pes,tl,cs::csl,union_effects efl ef)
 
-and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot emap * tag *nexp_range list * bounds_env *effect ) =
+and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) 
+    : (tannot lexp * typ * bool * tannot emap * tag * nexp_range list * bounds_env * effect ) =
   let (Env(d_env,t_env,b_env,tp_env)) = envs in
   match lexp with
     | LEXP_id id -> 
       let i = id_to_string id in
       (match Envmap.apply t_env i with
-	(*TODO Should probably change this to use the default as the expected type*)
+	(*TODO Should change this to use the default as the expected type*)
 	| Some(Base((parms,t),Default,_,_,_)) ->
 	  typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists")
         | Some(Base(([],t),Alias,_,_,_)) ->
+	  let ef = {effect = Eset[BE_aux(BE_wreg,l)]} in
           (match Envmap.apply d_env.alias_env i with
             | Some(OneReg(reg, (Base(([],t'),_,_,_,_)))) ->
-              let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
-              (LEXP_aux(lexp,(l,(Base(([],t'),Alias,[],ef,nob)))), t, Envmap.empty, External (Some reg),[],nob,ef)
+              (LEXP_aux(lexp,(l,(Base(([],t'),Alias,[],ef,nob)))), t, false, Envmap.empty, External (Some reg),[],nob,ef)
             | Some(TwoReg(reg1,reg2, (Base(([],t'),_,_,_,_)))) ->
-              let ef = {effect=Eset [BE_aux(BE_wreg,l)]} in
 	      let u = match t.t with
 		| Tapp("register", [TA_typ u]) -> u in
-              (LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef,nob))), u, Envmap.empty, External None,[],nob,ef)
+              (LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef,nob))), u, false, Envmap.empty, External None,[],nob,ef)
             | _ -> assert false)
 	| Some(Base((parms,t),tag,cs,_,b)) ->
-	  let t,cs,_,_ = match tag with | External _ | Emp_global -> subst parms false t cs pure_e | _ -> t,cs,pure_e,Envmap.empty
+	  let t,cs,_,_ = 
+	    match tag with | External _ | Emp_global -> subst parms false t cs pure_e | _ -> t,cs,pure_e,Envmap.empty
 	  in
 	  let t,cs' = get_abbrev d_env t in
           let t_actual = match t.t with | Tabbrev(i,t) -> t | _ -> t in
+	  let cs_o = cs@cs' in
           (*let _ = Printf.eprintf "Assigning to %s, t is %s\n" i (t_to_string t_actual) in*)
 	  (match t_actual.t,is_top with
 	    | Tapp("register",[TA_typ u]),_ ->
 	      let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
-	      (LEXP_aux(lexp,(l,(Base(([],t),External (Some i),cs@cs',ef,nob)))),u,Envmap.empty,External (Some i),[],nob,ef)
+	      (LEXP_aux(lexp,(l,(Base(([],t),External (Some i),cs_o,ef,nob)))),u,false,
+	       Envmap.empty,External (Some i),[],nob,ef)
 	    | Tapp("reg",[TA_typ u]),_ ->
-	      (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs@cs',pure_e,b)))),u,Envmap.empty,Emp_local,[],nob,pure_e)
+	      (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs_o,pure_e,b)))),u,false,
+	       Envmap.empty,Emp_local,[],nob,pure_e)
 	    | Tapp("vector",_),false ->
-	      (LEXP_aux(lexp,(l,(Base(([],t),tag,cs@cs',pure_e,b)))),t,Envmap.empty,Emp_local,[],nob,pure_e)
+	      (LEXP_aux(lexp,(l,(Base(([],t),tag,cs_o,pure_e,b)))),t,true,Envmap.empty,Emp_local,[],nob,pure_e)
 	    | (Tfn _ ,_) ->
 	      (match tag with 
 		| External _ | Spec | Emp_global -> 
@@ -1361,22 +1365,23 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
 		  let t = {t = Tapp("reg",[TA_typ u])} in
 		  let bounds = extract_bounds d_env i t in
 		  let tannot = (Base(([],t),Emp_local,[],pure_e,bounds)) in
-		  (LEXP_aux(lexp,(l,tannot)),u,Envmap.from_list [i,tannot],Emp_local,[],bounds,pure_e)
+		  (LEXP_aux(lexp,(l,tannot)),u,false,Envmap.from_list [i,tannot],Emp_local,[],bounds,pure_e)
 		| _ -> 
-		  typ_error l ("Can only assign to registers or regs, found identifier " ^ i ^ " with type " ^ t_to_string t)) 
+		  typ_error l ("Cannot assign to " ^ i ^" with type " ^ t_to_string t ^ 
+				  ". Assignment must be to registers or non-parameter, non-let-bound local variables."))
 	    | _,_ -> 
 	      if is_top
-	      then typ_error l 
-		("Can only assign to registers or regs, found identifier " ^ i ^ " with type " ^ t_to_string t)
+	      then 
+		typ_error l ("Cannot assign to " ^ i ^" with type " ^ t_to_string t ^ 
+				". Assignment must be to registers or non-parameter, non-let-bound local variables.")
 	      else 
-		(* TODO, make sure this is a record *)
-		(LEXP_aux(lexp,(l,constrained_annot t (cs@cs'))),t,Envmap.empty,Emp_local,[],nob,pure_e))
+		(LEXP_aux(lexp,(l,constrained_annot t cs_o)),t,true,Envmap.empty,Emp_local,[],nob,pure_e))
 	| _ -> 
 	  let u = new_t() in
 	  let t = {t=Tapp("reg",[TA_typ u])} in
 	  let bounds = extract_bounds d_env i u in
 	  let tannot = (Base(([],t),Emp_local,[],pure_e,bounds)) in
-	  (LEXP_aux(lexp,(l,tannot)),u,Envmap.from_list [i,tannot],Emp_local,[],bounds,pure_e))
+	  (LEXP_aux(lexp,(l,tannot)),u,false,Envmap.from_list [i,tannot],Emp_local,[],bounds,pure_e))
     | LEXP_memory(id,exps) -> 
       let i = id_to_string id in
       (match Envmap.apply t_env i with
@@ -1409,11 +1414,13 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
 			    | args,es -> 
 			      (match check_exp envs imp_param args_t (E_aux (E_tuple exps,(l,NoTyp))) with
 				| (E_aux(E_tuple es,(l',tannot)),_,_,cs_e,_,ef_e) -> (es,cs_e,ef_e)
-				| _ -> raise (Reporting_basic.err_unreachable l "Gave check_exp a tuple, didn't get a tuple back"))
+				| _ -> 
+				  raise (Reporting_basic.err_unreachable l 
+					   "Gave check_exp a tuple, didn't get a tuple back"))
 			in
 			let ef_all = union_effects ef' ef_es in
 			(LEXP_aux(LEXP_memory(id,es),(l,Base(([],out),tag,cs_call,ef',nob))),
-			 item_t,Envmap.empty,tag,cs_call@cs_es,nob,ef_all)
+			 item_t,false,Envmap.empty,tag,cs_call@cs_es,nob,ef_all)
 		      | _ -> 
 			let e = match exps with
 			  | [] -> E_aux(E_lit(L_aux(L_unit,l)),(l,NoTyp))
@@ -1422,7 +1429,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
 			let (e,_,_,cs_e,_,ef_e) = check_exp envs imp_param apps e in
 			let ef_all = union_effects ef ef_e in
 			(LEXP_aux(LEXP_memory(id,[e]),(l,Base(([],out),tag,cs_call,ef,nob))),
-			 app,Envmap.empty,tag,cs_call@cs_e,nob,ef_all))
+			 app,false,Envmap.empty,tag,cs_call@cs_e,nob,ef_all))
 		  else typ_error l ("Assignments require functions with a wmem or wreg effect")
 		| _ -> typ_error l ("Assignments require functions with a wmem or wreg effect"))
 	    | _ -> typ_error l ("Assignments require a function here, found " ^ i ^ " which has type " ^ (t_to_string t)))
@@ -1434,7 +1441,8 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
       let new_bounds = extract_bounds d_env i ty in
       (match Envmap.apply t_env i with
 	| Some(Base((parms,t),tag,cs,_,bounds)) ->
-	  let t,cs,_,_ = match tag with | External _ | Emp_global -> subst parms false t cs pure_e | _ -> t,cs,pure_e,Envmap.empty
+	  let t,cs,_,_ = 
+	    match tag with | External _ | Emp_global -> subst parms false t cs pure_e | _ -> t,cs,pure_e,Envmap.empty
 	  in
 	  let t,cs' = get_abbrev d_env t in
           let t_actual = match t.t with | Tabbrev(_,t) -> t | _ -> t in
@@ -1443,36 +1451,39 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
 	    | Tapp("register",[TA_typ u]),_ ->
 	      let t',cs = type_consistent (Expr l) d_env Require false ty u in
 	      let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
-	      (LEXP_aux(lexp,(l,(Base(([],t),External (Some i),cs,ef,nob)))),ty,Envmap.empty,External (Some i),[],nob,ef)
+	      (LEXP_aux(lexp,(l,(Base(([],t),External (Some i),cs,ef,nob)))),ty,false,
+	       Envmap.empty,External (Some i),[],nob,ef)
 	    | Tapp("reg",[TA_typ u]),_ ->
 	      let t',cs = type_consistent (Expr l) d_env Require false ty u in
-	      (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,Envmap.empty,Emp_local,[],bs,pure_e)
+	      (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,false,
+	       Envmap.empty,Emp_local,[],bs,pure_e)
 	    | Tapp("vector",_),false ->
-	      (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,Envmap.empty,Emp_local,[],bs,pure_e)
+	      (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,true,Envmap.empty,Emp_local,[],bs,pure_e)
 	    | Tuvar _,_ ->
 	      let u' = {t=Tapp("reg",[TA_typ ty])} in
 	      equate_t t u';
-	      (LEXP_aux(lexp,(l,(Base((([],u'),Emp_local,cs,pure_e,bs))))),ty,Envmap.empty,Emp_local,[],bs,pure_e)
+	      (LEXP_aux(lexp,(l,(Base((([],u'),Emp_local,cs,pure_e,bs))))),ty,false,Envmap.empty,Emp_local,[],bs,pure_e)
 	    | (Tfn _ ,_) ->
 	      (match tag with 
 		| External _ | Spec | Emp_global -> 
 		  let tannot = (Base(([],ty),Emp_local,[],pure_e,new_bounds)) in
-		  (LEXP_aux(lexp,(l,tannot)),ty,Envmap.from_list [i,tannot],Emp_local,[],new_bounds,pure_e)
+		  (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_local,[],new_bounds,pure_e)
 		| _ -> 
-		  typ_error l ("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t)) 
+		  typ_error l ("Cannot assign to " ^ i ^ " with type " ^ t_to_string t)) 
 	    | _,_ -> 
 	      if is_top
 	      then typ_error l 
-		("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t)
+		("Cannot assign to " ^ i ^ " with type " ^ t_to_string t ^
+		    ". May only assign to registers, and non-paremeter, non-let bound local variables")
 	      else 
 		(* TODO, make sure this is a record *)
-		(LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,nob)))),ty,Envmap.empty,Emp_local,[],nob,pure_e)) 
+		(LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,nob)))),ty,false,Envmap.empty,Emp_local,[],nob,pure_e))
 	| _ -> 
 	  let t = {t=Tapp("reg",[TA_typ ty])} in
 	  let tannot = (Base(([],t),Emp_local,[],pure_e,new_bounds)) in
-	  (LEXP_aux(lexp,(l,tannot)),ty,Envmap.from_list [i,tannot],Emp_local,[],new_bounds,pure_e))
+	  (LEXP_aux(lexp,(l,tannot)),ty,false,Envmap.from_list [i,tannot],Emp_local,[],new_bounds,pure_e))
     | LEXP_vector(vec,acc) -> 
-      let (vec',vec_t,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
+      let (vec',vec_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
       let vec_t,cs' = get_abbrev d_env vec_t in
       let vec_actual = match vec_t.t with | Tabbrev(_,t) -> t | _ -> vec_t in
       (match vec_actual.t with
@@ -1480,27 +1491,34 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
 	  let acc_t = match ord.order with
 	    | Oinc -> {t = Tapp("range",[TA_nexp base;TA_nexp (mk_sub (mk_add base rise) n_one)])} 
 	    | Odec -> {t = Tapp("range",[TA_nexp (mk_sub rise (mk_add base n_one)); TA_nexp base])}
-	    | _ -> typ_error l ("Assignment to one vector element requires either inc or dec order")
+	    | _ -> typ_error l ("Assignment to one vector element requires a non-polymorphic order")
 	  in
 	  let (e,acc_t',_,cs',_,ef_e) = check_exp envs imp_param acc_t acc in
-	  let item_t,add_reg_write = 
+	  let item_t,add_reg_write,reg_still_required = 
 	    match item_t.t with
-	      | Tapp("register",[TA_typ t]) | Tabbrev(_,{t=Tapp("register",[TA_typ t])}) -> t,true
-	      | _ -> item_t,false in
+	      | Tapp("register",[TA_typ t]) | Tabbrev(_,{t=Tapp("register",[TA_typ t])}) -> t,true,false
+	      | Tapp("reg",[TA_typ t]) -> t,false,false
+	      | _ -> item_t,false,true in
 	  let ef = if add_reg_write then add_effect (BE_aux(BE_wreg,l)) ef else ef in
-	  (LEXP_aux(LEXP_vector(vec',e),(l,Base(([],item_t),tag,csi,ef,nob))),item_t,env,tag,csi@cs',bounds,union_effects ef ef_e)
-	| Tuvar _ -> typ_error l "Assignment to one position expected a vector with a known order, found a polymorphic value, try adding an annotation"
+	  if is_top && reg_still_required && reg_required
+	  then typ_error l "Assignment expected a register or non-parameter non-letbound identifier to mutate"
+	  else
+	    (LEXP_aux(LEXP_vector(vec',e),(l,Base(([],item_t),tag,csi,ef,nob))),item_t,reg_required && reg_still_required,
+	     env,tag,csi@cs',bounds,union_effects ef ef_e)
+	| Tuvar _ -> 
+	  typ_error l "Assignment expected a vector with a known order, try adding an annotation."
 	| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t))) 
     | LEXP_vector_range(vec,e1,e2)-> 
-      let (vec',item_t,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
+      let (vec',item_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
       let item_t,cs = get_abbrev d_env item_t in
       let item_actual = match item_t.t with | Tabbrev(_,t) -> t | _ -> item_t in
-      let item_actual,add_reg_write,cs = 
+      let item_actual,add_reg_write,reg_still_required,cs = 
 	match item_actual.t with
 	  | Tapp("register",[TA_typ t]) ->
-	    (match get_abbrev d_env t with
-	      | {t=Tabbrev(_,t)},cs' | t,cs' -> t,true,cs@cs')
-	  | _ -> item_actual,false,cs in
+	    (match get_abbrev d_env t with | {t=Tabbrev(_,t)},cs' | t,cs' -> t,true,false,cs@cs')
+	  | Tapp("reg",[TA_typ t]) ->
+	    (match get_abbrev d_env t with | {t=Tabbrev(_,t)},cs' | t,cs' -> t,false,false,cs@cs')
+	  | _ -> item_actual,false,true,cs in
       (match item_actual.t with
 	| Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ t]) ->
 	  let base_e1,range_e1,base_e2,range_e2 = new_n(),new_n(),new_n(),new_n() in
@@ -1513,6 +1531,10 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
 	       Tapp("range",[TA_nexp base_e2;TA_nexp range_e2])) -> base_e1,range_e1,base_e2,range_e2
 	    | _ -> base_e1,range_e1,base_e2,range_e2 in
           let len = new_n() in
+	  let needs_reg = match t.t with
+	    | Tapp("reg",_) -> false
+	    | Tapp("register",_) -> false
+	    | _ -> true in
 	  let cs_t,res_t = match ord.order with
 	    | Oinc ->  ([LtEq((Expr l),Require,base,base_e1);
 			 LtEq((Expr l),Require,mk_add base_e1 range_e1, mk_add base_e2 range_e2);
@@ -1530,11 +1552,14 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
 	  in
 	  let cs = cs_t@cs@cs1@cs2 in
 	  let ef = union_effects ef (union_effects ef_e ef_e') in
-	  (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Base(([],item_t),tag,cs,ef,nob))),res_t,env,tag,cs,bounds,ef)
-	| Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, found a polymorphic value, try adding an annotation"
+	  if is_top && reg_required && reg_still_required && needs_reg 
+	  then typ_error l "Assignment requires a register or a non-parameter, non-letbound local identifier"
+	  else (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Base(([],item_t),tag,cs,ef,nob))),res_t,reg_required&&reg_still_required && needs_reg
+		,env,tag,cs,bounds,ef)
+	| Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, try adding an annotation."
 	| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t))) 
     | LEXP_field(vec,id)-> 
-      let (vec',item_t,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
+      let (vec',item_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
       let vec_t = match vec' with
         | LEXP_aux(_,(l',Base((parms,t),_,_,_,_))) -> t
         | _ -> item_t in
@@ -1551,7 +1576,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp *
                 | Overload _ -> raise (Reporting_basic.err_unreachable l "Record given overload annot")
 		| Base((params,et),_,cs,_,_) ->
 		  let et,cs,ef,_ = subst params false et cs ef in
-		  (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],vec_t),tag,csi@cs,ef,nob)))),et,env,tag,csi@cs,bounds,ef)))
+		  (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],vec_t),tag,csi@cs,ef,nob)))),et,false,env,tag,csi@cs,bounds,ef)))
 	| _ -> typ_error l ("Expected a register binding here, found " ^ (t_to_string item_t)))
 
 and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list * bounds_env * effect =
diff --git a/src/type_internal.ml b/src/type_internal.ml
index d2b26d1d..9534f70f 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -2493,6 +2493,29 @@ let rec get_nuvars n =
     | Nmult(n1,n2) | Nadd(n1,n2) | Nsub(n1,n2) -> (get_nuvars n1)@(get_nuvars n2)
     | Nneg n | N2n(n,_) | Npow(n,_) -> get_nuvars n
 
+module NexpM = 
+ struct
+ type t = nexp
+ let compare = compare_nexps
+end
+module Var_set = Set.Make(NexpM) 
+
+let rec get_all_nuvars_cs cs = match cs with
+  | [] -> Var_set.empty 
+  | (Eq(_,n1,n2) | GtEq(_,_,n1,n2) | LtEq(_,_,n1,n2))::cs -> 
+    let s = get_all_nuvars_cs cs in
+    let n1s = get_nuvars n1 in
+    let n2s = get_nuvars n2 in
+    List.fold_right (fun n s -> Var_set.add n s) (n1s@n2s) s
+  | CondCons(_,pats,exps)::cs ->
+    let s = get_all_nuvars_cs cs in
+    let ps = get_all_nuvars_cs pats in
+    let es = get_all_nuvars_cs exps in
+    Var_set.union s (Var_set.union ps es)
+  | BranchCons(_,c)::cs ->
+    Var_set.union (get_all_nuvars_cs c) (get_all_nuvars_cs cs)
+  | _::cs -> get_all_nuvars_cs cs
+
 let freshen n = 
   let nuvars = get_nuvars n in
   let env_map = List.map (fun nu -> (nu,new_n ())) nuvars in
@@ -2660,13 +2683,31 @@ let rec simple_constraint_check in_env cs =
 
 let rec resolve_in_constraints cs = cs
 
+let check_range_consistent require_lt require_gt guarantee_lt guarantee_gt = 
+  match require_lt,require_gt,guarantee_lt,guarantee_gt with
+    | None,None,None,None 
+    | Some _, None, None, None | None, Some _ , None, None | None, None, Some _ , None | None, None, None, Some _ 
+    | Some _, Some _,None,None | None,None,Some _,Some _ (*earlier check should ensure these*)
+      -> ()
+    | Some(crlt,rlt), Some(crgt,rgt), Some(cglt,glt), Some(cggt,ggt) ->
+      if glt <= rlt (*Can we guarantee that the upper bound is less than the required upper bound*) 
+      then if ggt <= rlt (*Can we guarantee that the lower bound is less than the required upper bound*)
+	then if glt >= rgt (*Can we guarantee that the upper bound is greater than the required lower bound*)
+	  then if ggt >= rgt (*Can we guarantee that the lower bound is greater than the required lower bound*)
+	    then ()
+	    else assert false (*make a good two-location error, all the way down*)
+	  else assert false
+	else assert false
+      else assert false
+      
+
 let rec constraint_size = function
   | [] -> 0
   | c::cs -> 
-    match c with 
+    (match c with 
       | CondCons(_,ps,es) -> constraint_size ps + constraint_size es
       | BranchCons(_,bs) -> constraint_size bs
-      | _ -> 1
+      | _ -> 1) + constraint_size cs
     
 let do_resolve_constraints = ref true