Add size of register to register for making appropriate unknown register_values

5 files changed, 36 insertions, 14 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index f3a1795a..fef8c170 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -135,7 +135,27 @@ let reg_start_pos reg =
 	| T_app "register" targs -> start_from_reg targs
 	| T_abbrev _ t -> start_from_abbrev t
       end 
-end   
+end 
+
+let reg_size reg = 
+  match reg with
+    | Reg _ (Just(typ,_,_,_)) -> 
+      let end_from_vec targs = match targs with
+	| T_args [_;T_arg_nexp (Ne_const s);_;_] -> s
+      end in
+      let end_from_reg targs = match targs with
+	| T_args [T_arg_typ (T_app "vector" targs)] -> end_from_vec targs
+      end in
+      let end_from_abbrev t = match t with
+	| T_app "vector" targs -> end_from_vec targs
+	| T_app "register" targs -> end_from_reg targs
+      end in
+      match typ with 
+	| T_app "vector" targs -> end_from_vec targs
+	| T_app "register" targs -> end_from_reg targs
+	| T_abbrev _ t -> end_from_abbrev t
+      end 
+end 
 
 (*Constant unit value, for use in interpreter *)
 let unitv = V_lit (L_aux L_unit Unknown)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index c82e6da2..b83c096a 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -53,6 +53,7 @@ let rec to_bytes l = match l with
 end 
 
 let all_known l = List.all is_bool l
+let all_known_bytes l = List.all (fun (Byte_lifted bs) -> List.all is_bool bs) l
 
 let bits_to_byte b = 
   if ((List.length b) = 8) && (all_known b)
@@ -98,8 +99,9 @@ let integer_of_byte_list bytes =
 *)
 
 let extern_reg r slice = match (r,slice) with
-  | (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x
-  | (Interp.Reg (Id_aux (Id x) _) _,Just(i1,i2)) -> Reg_slice x (i1,i2)
+  | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_)),Nothing) -> 
+    Reg x (Interp.reg_size r)
+  | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_)),Just(i1,i2)) -> Reg_slice x (i1,i2)
   | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> 
     Reg_field y x (i,i)
   | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_range i j) _), Nothing) -> 
@@ -471,10 +473,10 @@ let rec find_reg_name reg = function
   | [] -> Nothing
   | (reg_name,v)::registers ->
     match (reg,reg_name) with
-      | (Reg i, Reg n) -> if i = n then (Just v) else find_reg_name reg registers
-      | (Reg_slice i (p1,p2), Reg n) -> 
+      | (Reg i size, Reg n size2) -> if i = n && size = size2 then (Just v) else find_reg_name reg registers
+      | (Reg_slice i (p1,p2), Reg n _) -> 
 	if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
-      | (Reg_field i f (p1,p2), Reg n) -> 
+      | (Reg_field i f (p1,p2), Reg n _) -> 
 	if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
       | (Reg_slice  i (p1,p2), Reg_slice n (p3,p4)) ->
 	if i=n 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index ab369a03..6fb9b713 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -96,8 +96,8 @@ type slice = (integer * integer)
 
 
 type reg_name = 
-| Reg of string 
-(*Name of the register, accessing the entire register*)
+| Reg of string * integer
+(*Name of the register, accessing the entire register, and the size of this register *)
 
 | Reg_slice of string * slice 
 (* Name of the register, accessing from the bit indexed by the first
@@ -117,7 +117,7 @@ specifies a part of the field, indexed w.r.t. the register as a whole *)
 (* because reg_name contains slice which currently contains Big_int.big_int, the default OCaml comparison is not sufficient and we need to define explicit type classes *)
 let reg_nameEqual r1 r2 = 
   match (r1,r2) with
-  | (Reg s1, Reg s2) -> s1=s2
+  | (Reg s1 l1, Reg s2 l2) -> s1=s2 && l1=l2
   | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> s1=s2 && sl1=sl2
   | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> s1=s2 && f1=f2 && sl1=sl2
   | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> s1=s2 && f1=f2 && sl1=sl2 && sl1'=sl2'
@@ -131,13 +131,13 @@ end
 
 let reg_nameCompare r1 r2 = 
   match (r1,r2) with
-  | (Reg s1, Reg s2) -> compare s1 s2
+  | (Reg s1 l1, Reg s2 l2) -> pairCompare compare compare (s1,l1) (s2,l2)
   | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> pairCompare compare compare (s1,sl1) (s2,sl2)
   | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> 
       tripleCompare compare compare compare (s1,f1,sl1) (s2,f2,sl2)
   | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> 
       pairCompare compare (tripleCompare compare compare compare) (s1,(f1,sl1,sl1')) (s2,(f2,sl2,sl2'))
-  | (Reg _, _)  -> LT
+  | (Reg _ _, _)  -> LT
   | (Reg_slice _ _, _) -> LT
   | (Reg_field _ _ _, _) -> LT
   | (_, _) -> GT
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 9cbd87a5..77716bfb 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -119,7 +119,7 @@ let rec bit_to_hex v =
 ;;*)
 
 let reg_name_to_string = function
-  | Reg0 s -> s
+  | Reg0(s,_) -> s
   | Reg_slice(s,(first,second)) -> 
     s ^ "[" ^ string_of_big_int first ^ (if (eq_big_int first second) then "" else ".." ^ (string_of_big_int second)) ^ "]"
   | Reg_field(s,f,_) -> s ^ "." ^ f
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 2c705455..8857f99c 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -61,11 +61,11 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu
 	      | i  -> string_of_int i) words))		
   | Unknown0 -> "Unknown"*)
 
-let reg_name_to_string = function
+(*let reg_name_to_string = function
   | Reg0 s -> s
   | Reg_slice(s,(first,second)) -> s (*contemplate putting slice here*)
   | Reg_field(s,f,_) -> s ^ "." ^ f
-  | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f
+  | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f*)
 
 let rec reg_to_string = function
   | Reg (id,_) -> id_to_string id