From 9916244375a99d74dd5ccf201136cb0555be7e4f Mon Sep 17 00:00:00 2001 From: Alastair Reid Date: Wed, 2 Jul 2025 16:39:09 +0100 Subject: [PATCH] Xform_bitslices Fixes a bug that occurs if you have code like this let wide : bits(1024) = ...; let r = [wide[0 +: 64], Zeros(64)]; The bug was causing us to generate a zero_extend from 1024 bits "up" to 64 bits. This patch does not fully fix the bug but it prevents it from happening when the width of the bitslice is a constant - which fixes the problem case. The most general fix would probably be to find the maximum width that appears anywhere in the transformed expression, widen everything to that maximum width and then use and/or/mask/etc. in the transformation. Leaving that to another day. --- libASL/xform_bitslices.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/libASL/xform_bitslices.ml b/libASL/xform_bitslices.ml index a5d7d83d..c4f320aa 100644 --- a/libASL/xform_bitslices.ml +++ b/libASL/xform_bitslices.ml @@ -23,6 +23,12 @@ open Asl_utils open Builtin_idents open Utils +let is_constant (x : AST.expr) : bool = + ( match x with + | Expr_Lit _ -> true + | _ -> false + ) + let transform_slices : bool ref = ref true let transform_non_slices (n : AST.expr) (w : AST.expr) (i : AST.expr) @@ -55,7 +61,7 @@ let transform (loc : Loc.t) (n : AST.expr) (w : AST.expr) (i : AST.expr) | Expr_Slices (_, _, [Slice_Single _]) -> raise (InternalError (loc, "Slice_Single not expected", (fun fmt -> Asl_fmt.expr fmt x), __LOC__)) - | Expr_Slices (Type_Bits (we, _), e, [Slice_LoWd (lo, wd)]) -> + | Expr_Slices (Type_Bits (we, _), e, [Slice_LoWd (lo, wd)]) when not (is_constant wd) -> (* generate "zero_extend_bits((e >> lo) AND mk_mask(wd, we), n) << i" *) let e1 = mk_lsr_bits we e lo in let e2 = mk_and_bits we e1 (Asl_utils.mk_mask wd we) in