From b39894b9faed9f8dbb8978781e2ac857680dad3e Mon Sep 17 00:00:00 2001
From: rina <k@rina.fyi>
Date: Tue, 16 Jan 2024 16:35:31 +1000
Subject: [PATCH] improve RedundantSlice to handle global arrays and local
 constants.

---
 libASL/dis.ml        |  6 +++--
 libASL/transforms.ml | 54 +++++++++++++++++++++++++++++++++++++++-----
 2 files changed, 52 insertions(+), 8 deletions(-)

diff --git a/libASL/dis.ml b/libASL/dis.ml
index fcf968f9..c9c7e19c 100644
--- a/libASL/dis.ml
+++ b/libASL/dis.ml
@@ -1456,14 +1456,16 @@ type env = (LocalEnv.t * IdentSet.t)
 let dis_decode_entry (env: Eval.Env.t) ((lenv,globals): env) (decode: decode_case) (op: value): stmt list =
     let DecoderCase_Case (_,_,loc) = decode in
     let ((),lenv',stmts) = (dis_decode_case loc decode op) env lenv in
+    let varentries = List.concat_map (fun vars -> StringMap.(bindings (map fst vars))) lenv.locals in
+    let bindings = Asl_utils.Bindings.of_seq @@ List.to_seq @@ List.map (fun (x,y) -> (Ident x,y)) varentries in
+    (* 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 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
     let stmts' = Transforms.CopyProp.copyProp stmts' in
-    let stmts' = Transforms.RedundantSlice.do_transform stmts' in
+    let stmts' = Transforms.RedundantSlice.do_transform bindings stmts' in
     let stmts' = Transforms.RemoveUnused.remove_unused globals @@ stmts' in
     if !debug_level >= 2 then begin
         let stmts' = Asl_visitor.visit_stmts (new Asl_utils.resugarClass (!TC.binop_table)) stmts' in
diff --git a/libASL/transforms.ml b/libASL/transforms.ml
index 2fb041ed..2d916290 100644
--- a/libASL/transforms.ml
+++ b/libASL/transforms.ml
@@ -1285,9 +1285,43 @@ module RedundantSlice = struct
     | Expr_LitHex _ -> false
     | _ -> true
 
-  class expression_walk = object
+  type ty_option = Just of ty | Clobbered
+
+  class expression_walk (vartypes: ty Bindings.t) = object (self)
     inherit Asl_visitor.nopAslVisitor
 
+    (** map of variable name to type. 
+      a value of "Clobbered" means that variable is declared multiple times with different types
+      and we should not remove any of its slices. *)
+    val mutable lvartypes : ty_option Bindings.t = Bindings.empty;
+
+    method update_lvar_types (s: stmt): unit =
+      match s with 
+      | Stmt_VarDecl(ty,id,_,l) 
+      | Stmt_ConstDecl(ty,id,_,l) ->
+        (match Bindings.find_opt id lvartypes with
+        | Some (Just ty') -> if ty = ty' then () else lvartypes <- Bindings.add id (Clobbered) lvartypes
+        | Some (Clobbered) -> ()
+        | None -> lvartypes <- Bindings.add id (Just ty) lvartypes)
+      | Stmt_VarDeclsNoInit(ty,ids,l) -> 
+        List.iter (fun id -> self#update_lvar_types (Stmt_VarDecl(ty,id,Expr_LitInt("ignored"),l))) ids
+      | _ -> ()
+
+    method var_type (id: ident): ty option = 
+      match Bindings.find_opt id lvartypes with
+      | (Some (Just x)) -> Some x
+      | _ -> Bindings.find_opt id vartypes 
+
+    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
+
+    method! vstmt (s: stmt): stmt visitAction = 
+      ChangeDoChildrenPost(s, fun s -> self#update_lvar_types s; s)
+
     method! vexpr (e: expr): expr visitAction =
       ChangeDoChildrenPost(e, fun e ->
       match e with
@@ -1299,14 +1333,22 @@ module RedundantSlice = struct
               Expr_Slices(e, [Slice_LoWd (Expr_LitInt "0", w)])
           | _ -> e)
       | Expr_Slices(e', [Slice_LoWd (Expr_LitInt "0", wd)]) ->
-          (match infer_type e' with
-          | Some(Type_Bits(num)) when num = wd -> e'
-          | _ -> e)
+          let try_match (opt: ty option): expr = 
+            match opt with
+            | Some(Type_Bits(num)) when num = wd -> e'
+            | _ -> e
+          in
+          (match e' with
+          (* note: no fall-through from var_type case to infer_type case, 
+             but infer_type only works for builtins anyway. *)
+          | Expr_Var id -> try_match (self#var_type id) 
+          | Expr_Array (Expr_Var id, _) -> try_match (self#array_val_type id) 
+          | _ -> try_match (infer_type e'))
       | _ -> e)
   end
 
-  let do_transform (xs: stmt list): stmt list =
-    Asl_visitor.visit_stmts (new expression_walk) xs
+  let do_transform (vartypes: ty Bindings.t) (xs: stmt list): stmt list =
+    Asl_visitor.visit_stmts (new expression_walk(vartypes)) xs
 
 end