Many fixes, primarily dealing with undefined

Including:
turn an undefined literal into a vector of undefined values of the correct length
handle sparse vector unspecified default values as undefined literals
allow global lets to call library functions

6 files changed, 105 insertions, 33 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index efb1db7a..ce74ee77 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -62,7 +62,7 @@ let rec string_of_value v = match v with
     | L_one  -> "1"
     | L_true -> "true"
     | L_false -> "false"
-    | L_num num -> toString(integerToString num [])
+    | L_num num -> if num = 0 then "0" else toString(integerToString num [])
     | L_hex hex -> "0x" ^ hex
     | L_bin bin -> "0b" ^ bin
     | L_undef -> "undefined"
@@ -86,7 +86,7 @@ let rec string_of_value v = match v with
   | V_unknown -> "Unknown"
   | V_register _ -> "register_as_value"
   | V_register_alias _ _ -> "register_as_alias"
-  | V_track v _ -> (*"tainted " ^*) (string_of_value v)
+  | V_track v _ -> "tainted " ^ (string_of_value v)
 end
 
 let rec id_value_eq (i, v) (i', v') = i = i' && value_eq v v'
@@ -218,10 +218,10 @@ type outcome =
 type interp_mode = <| eager_eval : bool; track_values : bool |>
 
 (* Evaluates global let binds and prepares the context for individual expression evaluation in the current model *)
-val to_top_env : defs tannot -> (maybe outcome * top_level)
+val to_top_env : (outcome -> maybe value) -> defs tannot -> (maybe outcome * top_level)
 
 (* interprets the exp sequentially in the presence of a set of top level definitions and returns a value, a memory request, or other external action *)
-val interp :interp_mode -> defs tannot -> exp tannot -> outcome
+val interp :interp_mode -> (outcome -> maybe value) -> defs tannot -> exp tannot -> outcome
 
 (* Takes a paused partially evaluated expression, puts the value into the environment, and runs again *)
 val resume : interp_mode -> stack -> maybe value -> outcome
@@ -1450,15 +1450,18 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			  let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) i1v i2v in
 			  let take_slice vtup vvec =
 			    (match vtup with
-			      | V_tuple [V_lit (L_aux (L_num n1) ln1);V_lit (L_aux (L_num n2) ln2)] ->
-				(match vvec with
-				| V_vector _ _ _ -> slice_vector vvec n1 n2
-				| V_vector_sparse _ _ _ _ _ -> slice_vector vvec n1 n2
-				| V_unknown -> 
-				  let inc = n1 < n2 in
-				  V_vector n1 inc 
-				    (List.replicate (natFromInteger ((if inc then n1-n2 else n2-n1)+1)) V_unknown)
-				| _ -> Assert_extra.failwith ("Vector slice of non-vector " ^ (string_of_value vvec)) end) end) in
+			      | V_tuple [v1;v2] ->
+				(match (detaint v1, detaint v2) with 
+				  | (V_lit (L_aux (L_num n1) ln1),V_lit (L_aux (L_num n2) ln2)) ->
+				    (match vvec with
+				      | V_vector _ _ _ -> slice_vector vvec n1 n2
+				      | V_vector_sparse _ _ _ _ _ -> slice_vector vvec n1 n2
+				      | V_unknown -> 
+					let inc = n1 < n2 in
+					V_vector n1 inc 
+					  (List.replicate (natFromInteger ((if inc then n1-n2 else n2-n1)+1)) V_unknown)
+				      | _ -> Assert_extra.failwith ("Vector slice of non-vector " ^ (string_of_value vvec)) end) end)
+			      | _ -> Assert_extra.failwith("slice not a tuple of nums " ^ (string_of_value vtup)) end) in
 			  (Value (binary_taint take_slice slice vvec), lm,le))
 			(fun a -> 
 			  let rebuild v env = let (ie1,env) = to_exp mode env i1v in
@@ -2309,41 +2312,53 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
     				                  (E_aux (E_id reg2) annot2)) 
 			        (l,(intern_annot annot))) t_level l_env l_mem Top), l_mem,l_env) end
 
-let rec to_global_letbinds (Defs defs) t_level =
+let rec eval_toplevel_let handle_action tlevel env mem lbind = 
+  match interp_letbind <|eager_eval=true; track_values=false;|> tlevel env mem lbind with
+    | ((Value v, lm, (LEnv _ le)),_) -> Just le
+    | ((Action a s,lm,le), Just le_builder) -> 
+      (match handle_action (Action a s) with
+	| Just value ->
+	  (match s with
+	    | Hole_frame id exp tl lenv lmem s ->
+	      eval_toplevel_let handle_action tl (add_to_env (id,value) lenv) lmem (le_builder exp) end)
+	| Nothing -> Nothing end)
+    | _ -> Nothing end
+
+let rec to_global_letbinds handle_action (Defs defs) t_level =
   let  (Env defs' instrs lets regs ctors subregs aliases) = t_level in
   match defs with
   | [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, eenv),t_level)
   | def::defs ->
     match def with
     | DEF_val lbind ->
-      match interp_letbind <|eager_eval=true; track_values=false;|> t_level eenv emem lbind with
-      | ((Value v,lm,(LEnv _ le)),_) -> to_global_letbinds (Defs defs) (Env defs' instrs (lets++le) regs ctors subregs aliases)
-      | ((Action a s,lm,le),_) -> 
-	((Error Unknown "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
-      | (e,_) -> (e,t_level) end
+      match eval_toplevel_let handle_action t_level eenv emem lbind with
+	| Just le -> 
+	  to_global_letbinds handle_action (Defs defs) (Env defs' instrs (lets++le) regs ctors subregs aliases)
+	| Nothing -> 
+	  to_global_letbinds handle_action (Defs defs) (Env defs' instrs lets regs ctors subregs aliases) end
     | DEF_type (TD_aux tdef _) ->
       match tdef with
       | TD_enum id ns ids _ -> 
         let enum_vals = map (fun eid -> (eid,V_ctor eid (T_id (get_id id)) unitv)) ids in
-        to_global_letbinds (Defs defs) (Env defs' instrs (lets++enum_vals) regs ctors subregs aliases)
-      | _ -> to_global_letbinds (Defs defs) t_level end
-    | _ -> to_global_letbinds (Defs defs) t_level
+        to_global_letbinds handle_action (Defs defs) (Env defs' instrs (lets++enum_vals) regs ctors subregs aliases)
+      | _ -> to_global_letbinds handle_action (Defs defs) t_level end
+    | _ -> to_global_letbinds handle_action (Defs defs) t_level
     end
   end
 
 (*TODO Contemplate making decode and execute environment variables instead of these constants*)
-let to_top_env defs = 
+let to_top_env external_functions defs = 
   let t_level = Env defs (extract_instructions "decode" "execute" defs) 
                     [] (* empty letbind and enum values, call below will fill in any *) 
 		    (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
-  let (o,t_level) = to_global_letbinds defs t_level in
+  let (o,t_level) = to_global_letbinds external_functions defs t_level in
   match o with
     | (Value _,_,_) -> (Nothing,t_level)
     | (o,_,_) -> (Just o,t_level)
   end
 
-let interp mode defs exp =
-  match (to_top_env defs) with
+let interp mode external_functions defs exp =
+  match (to_top_env external_functions defs) with
     | (Nothing,t_level) -> 
       match interp_main mode t_level eenv emem exp with
 	| (o,_,_) -> o
@@ -2351,6 +2366,36 @@ let interp mode defs exp =
     | (Just o,_) -> o (* Should do something different for action to allow global lets to call external functions *)
   end
 
+let rec resume_with_env mode stack value =
+  match (stack,value) with
+  | (Top,_) -> (Error Unknown "Top hit without expression to evaluate",eenv)
+  | (Hole_frame id exp t_level env mem Top,Just value) -> 
+    match interp_main mode t_level (add_to_env (id,value) env) mem exp with | (o,_,e) -> (o,e) end 
+  | (Hole_frame id exp t_level env mem stack,Just value) ->
+    match resume_with_env mode stack (Just value) with
+    | (Value v,e) -> 
+      match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,e) -> (o,e) end 
+    | (Action action stack,e) -> (Action action (Hole_frame id exp t_level env mem stack),e)
+    | (Error l s,e) -> (Error l s,e)
+    end  
+  | (Hole_frame id exp t_level env mem stack, Nothing) ->
+    match resume_with_env mode stack Nothing with
+      | (Value v,e) ->
+	match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,e) -> (o,e) end
+      | (Action action stack,e) -> (Action action (Hole_frame id exp t_level env mem stack),e)
+      | (Error l s,e) -> (Error l s,e)
+    end
+  | (Thunk_frame exp t_level env mem Top,_) ->
+    match interp_main mode t_level env mem exp with | (o,_,e) -> (o,e) end
+  | (Thunk_frame exp t_level env mem stack,value) ->
+    match resume_with_env mode stack value with
+    | (Value v,e) -> 
+      match interp_main mode t_level env mem exp with | (o,_,e) -> (o,e) end 
+    | (Action action stack,e) -> (Action action (Thunk_frame exp t_level env mem stack),e)
+    | (Error l s,e) -> (Error l s,e)
+    end  
+  end
+
 let rec resume mode stack value =
   match (stack,value) with
   | (Top,_) -> Error Unknown "Top hit without expression to evaluate"
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 648a61bd..94f5abc6 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -13,7 +13,6 @@ val extern_reg_value : maybe integer -> Interp.value -> register_value
 val extern_mem_value : interp_mode -> Interp.value -> (memory_value * maybe (list reg_name))
 val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name
 
-let build_context defs = match Interp.to_top_env defs with (_,context) -> context end
 
 let make_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values |>;;
 let tracking_dependencies mode = mode.Interp.track_values
@@ -377,6 +376,17 @@ let rec interp_to_value_helper arg instr thunk =
     | _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
 end
 
+let call_external_functions outcome = 
+  match outcome with
+    | Interp.Action (Interp.Call_extern i value) stack ->
+      match List.lookup i external_functions with
+	| Nothing -> Nothing
+	| Just f -> Just (f value) end
+    | _ -> Nothing end
+
+let build_context defs = match Interp.to_top_env call_external_functions defs with (_,context) -> context end
+
+
 let rec find_instruction i = function
   | [] -> Nothing
   | Instruction_extractor.Skipped::instrs -> find_instruction i instrs
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index b72cd362..5d36149a 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -199,6 +199,8 @@ let to_vec_inc (V_tuple[v1;v2]) =
 	V_vector 0 true (map bool_to_bit (reverse l)) 
       | ((V_lit(L_aux (L_num n) ln)),V_unknown) -> 
 	V_vector 0 true (List.replicate (natFromInteger n) V_unknown)
+      | ((V_lit(L_aux (L_num n) ln)),(V_lit (L_aux L_undef _))) -> 
+	V_vector 0 true (List.replicate (natFromInteger n) v2)
       | (_,V_unknown) -> V_unknown
       | (V_unknown,_) -> V_unknown
       | _ -> Assert_extra.failwith ("to_vec_inc parameters were " ^ (string_of_value (V_tuple[v1;v2])))
@@ -213,6 +215,8 @@ let to_vec_dec (V_tuple([v1;v2])) =
 	V_vector (len - 1) false (map bool_to_bit (reverse l)) 
       | ((V_lit(L_aux (L_num n) ln)),V_unknown) -> 
 	V_vector (n-1) false (List.replicate (natFromInteger n) V_unknown)
+      | ((V_lit(L_aux (L_num n) ln)),(V_lit (L_aux L_undef _))) -> 
+	V_vector (n-1) false (List.replicate (natFromInteger n) v2)
       | (_,V_unknown) -> V_unknown
       | (V_unknown,_) -> V_unknown
       | _ -> Assert_extra.failwith ("to_vec_dec parameters were " ^ (string_of_value (V_tuple[v1;v2])))
@@ -532,7 +536,8 @@ let rec vec_concat (V_tuple [vl;vr]) =
 
 let v_length v = retaint v (match detaint v with
   | V_vector n d l -> V_lit (L_aux (L_num (integerFromNat (List.length l))) Unknown)
-  | V_unknown -> V_unknown end)
+  | V_unknown -> V_unknown 
+  | _ -> Assert_extra.failwith ("length given unexpected " ^ (string_of_value v)) end)
 
 let function_map = [
   ("ignore", ignore_sail);            
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 8857f99c..a8291a78 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -436,7 +436,7 @@ let run
   | Some m -> m in
   try
     Printexc.record_backtrace true;
-    loop mode (reg, mem) (interp {eager_eval = eager_eval; track_values = false} test entry)
+    loop mode (reg, mem) (interp {eager_eval = eager_eval; track_values = false} (fun id -> None) test entry)
   with e ->
     let trace = Printexc.get_backtrace () in
     debugf "%s: %s %s\n%s\n" (grey name) (red "interpretor error") (Printexc.to_string e) trace;
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 4ea9ea63..9d7cf616 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -417,6 +417,7 @@ and pp_lem_exp ppf (E_aux(e,(l,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_internal_exp (l, Base((_,t),_,_,_)) ->
       (match t.t with
+	| Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}])
 	| Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
 	  (match r.nexp with
 	  | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" 
@@ -969,6 +970,7 @@ let doc_exp, doc_let =
       (* doc_op (doc_id op) (exp l) (exp r) *)
   | E_internal_exp (l, Base((_,t),_,_,_)) ->
     (match t.t with
+      | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}])
       | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
 	(match r.nexp with
 	  | Nvar v -> utf8string v
@@ -980,7 +982,7 @@ let doc_exp, doc_let =
 	  | Nconst bi -> utf8string (Big_int.string_of_big_int bi)
 	  | Nvar v -> utf8string v
 	  | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given implicit without var or const"))
-      | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given non-vector, non-implicit"))
+      | _ ->  raise (Reporting_basic.err_unreachable l ("Internal exp given non-vector, non-implicit " ^ t_to_string t)))
 
   (* XXX missing case
      AAA internal_cast should never have an overload, if it's been seen it's a bug *)
diff --git a/src/type_check.ml b/src/type_check.ml
index 73b66e6e..53725a29 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -535,7 +535,16 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 				             TA_nexp{nexp = Nconst (big_int_of_int (String.length s))};
 				             TA_ord d_env.default_o ;TA_typ{t = Tid"bit"}])},[],pure_e
 	| L_string s -> simp_exp e l {t = Tid "string"},[],pure_e
-	| L_undef -> simp_exp e l (new_t ()),[],{effect=Eset[BE_aux(BE_undef,l)]}) in
+	| L_undef -> 
+	  let ef = {effect=Eset[BE_aux(BE_undef,l)]} in
+          (match expect_t.t with
+            | Tapp ("vector",[TA_nexp base;TA_nexp {nexp=Nconst rise};TA_ord o;(TA_typ {t=Tid "bit"})]) 
+	    | Tapp ("register",[TA_typ {t=Tapp ("vector",[TA_nexp base;TA_nexp {nexp=Nconst rise};
+							  TA_ord o;(TA_typ {t=Tid "bit"})])}])->
+              let f = match o.order with | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" | _ -> "to_vec_inc" (*Change to follow a default?*) in
+	      let tannot = (l,Base(([],expect_t),External (Some f),[],ef)) in
+              E_aux(E_app((Id_aux((Id f),l)),[(E_aux (E_internal_exp tannot, tannot));simp_exp e l bit_t]),tannot),[],ef
+            | _ -> simp_exp e l (new_t ()),[],ef)) in
       let t',cs',_,e' = type_coerce (Expr l) d_env false (get_e_typ e) e expect_t in
       (e',t',t_env,cs@cs',effect)
     | E_cast(typ,e) ->
@@ -839,8 +848,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
 	| (Def_val_empty,false) -> (Def_val_aux(Def_val_empty,(ld,Base(([],item_t),Emp_local,[],pure_e))),true,[],pure_e)
         | (Def_val_empty,true)  -> 
           let ef = add_effect (BE_aux(BE_unspec,l)) pure_e in
-          (Def_val_aux(Def_val_dec ( (E_aux( E_lit( L_aux(L_undef, l)), (l, (Base(([],item_t),Emp_local,[],ef)))))),
-                       (l,Base(([],item_t),Emp_local,[],pure_e))),false,[],ef)
+	  let (de,_,_,_,ef_d) = check_exp envs imp_param item_t (E_aux(E_lit (L_aux(L_undef,l)), (l,NoTyp))) in
+          (Def_val_aux(Def_val_dec de,
+                       (l,Base(([],item_t),Emp_local,[],ef))),false,[],ef)
 	| (Def_val_dec e,_) -> let (de,t,_,cs_d,ef_d) = (check_exp envs imp_param item_t e) in
 			       (*Check that ef_d doesn't write to memory or registers? *)
 			       (Def_val_aux(Def_val_dec de,(ld,(Base(([],item_t),Emp_local,cs_d,ef_d)))),false,cs_d,ef_d) in