From e3abd323579bf1da3f0ec7583b78b7e069b45c88 Mon Sep 17 00:00:00 2001
From: rina <k@rina.fyi>
Date: Thu, 15 Feb 2024 16:49:52 +1000
Subject: [PATCH 1/2] handle Type_Register in redundant slices.

---
 libASL/transforms.ml | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/libASL/transforms.ml b/libASL/transforms.ml
index 3d0c282a..5b9562d8 100644
--- a/libASL/transforms.ml
+++ b/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,9 +1325,10 @@ 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
@@ -1323,8 +1336,6 @@ module RedundantSlice = struct
       | _ -> 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

From d2c37b9cfa27737333ed0670469dcdb657ff5203 Mon Sep 17 00:00:00 2001
From: rina <k@rina.fyi>
Date: Thu, 15 Feb 2024 16:59:07 +1000
Subject: [PATCH 2/2] run first slice elimination without variable information.

this should avoid pessimising the main sequence of transformations.
it is still run with this information near the end.
---
 libASL/dis.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/libASL/dis.ml b/libASL/dis.ml
index 086dbc5b..65a7be80 100644
--- a/libASL/dis.ml
+++ b/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