Merge pull request #42 from UQ-PAC/redundant-slice-of-reg

handle Type_Register in redundant slices.

libASL/dis.ml

@@ -1461,7 +1461,7 @@ let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_cas
     (* List.iter (fun (v,t) -> Printf.printf ("%s:%s\n") v (pp_type t)) varentries; *)
     let stmts = flatten stmts [] in
     let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts in
-    let stmts' = Transforms.RedundantSlice.do_transform bindings stmts' in
+    let stmts' = Transforms.RedundantSlice.do_transform Bindings.empty stmts' in
     let stmts' = Transforms.StatefulIntToBits.run stmts' in
     let stmts' = Transforms.IntToBits.ints_to_bits stmts' in
     let stmts' = Transforms.CommonSubExprElim.do_transform stmts' in

libASL/transforms.ml

@@ -1290,6 +1290,18 @@ module RedundantSlice = struct
     | Some x' -> Some x'
     | None -> y
 
+  let width_of_slice (slice : slice) : int =
+    match slice with
+    | Slice_LoWd (lo, wd) -> int_of_expr wd
+    | Slice_HiLo (hi, lo) -> int_of_expr hi - int_of_expr lo + 1
+    | Slice_Single _ -> 1
+
+  let width_of_slices slices = List.fold_left (+) 0 (List.map width_of_slice slices)
+
+  let bits_type_of_reg_type = function
+    | Type_Register (wd, _) -> Type_Bits (Expr_LitInt wd)
+    | x -> x
+
   type ty_option = Just of ty | Clobbered
 
   class expression_walk (vartypes: ty Bindings.t) = object (self)
@@ -1313,18 +1325,17 @@ module RedundantSlice = struct
       | _ -> ()
 
     method var_type (id: ident): ty option = 
-      match Bindings.find_opt id lvartypes with
-      | (Some (Just x)) -> Some x
-      | _ -> Bindings.find_opt id vartypes 
+      Option.map bits_type_of_reg_type
+        (match Bindings.find_opt id lvartypes with
+        | Some (Just x) -> Some x
+        | _ -> Bindings.find_opt id vartypes)
 
     method var_type' (e: expr): ty option =
       match e with
       | Expr_Var id -> self#var_type id
       | _ -> None
 
     method array_val_type (id: ident): ty option = 
-      (* XXX: use of Tcheck.env0 global mutable state *)
-      (* let env = Tcheck.env0 in *)
       match self#var_type id with
       | Some (Type_Array(_ix,ty)) -> Some ty
       | _ -> None