Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

handle Type_Register in redundant slices. #42

Merged
merged 2 commits into from
Feb 15, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion libASL/dis.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
21 changes: 16 additions & 5 deletions libASL/transforms.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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
Expand Down
Loading