Add support for reading a slice of an integer

Signed-off-by: Alastair Reid <[email protected]>

Author: alastairreid

bin/asl2c.py

@@ -73,9 +73,7 @@
 // e.g., "x[7:0]" --> "x[0 +: 8]"
 :xform_lower
 
-// Eliminate slices of integers by first converting the integer to a bitvector.
-// e.g., if "x : integer", then "x[1 +: 8]" to "cvt_int_bits(x, 9)[1 +: 8]"
-:xform_int_bitslices
+{xform_int_bitslices}
 
 // Convert use of getter/setter syntax to function calls.
 // e.g., "Mem[a, sz] = x" --> "Mem_set(a, sz, x)"
@@ -329,10 +327,17 @@ def mk_script(args, output_directory):
         'output_dir':  output_directory,
         'split_state': "",
         'suppress_bitslice_xform': "",
+        'xform_int_bitslices': "",
         'track_valid': "",
         'wrap_variables': "",
     }
     if args.instrument_unknown: substitutions['track_valid'] = ":xform_valid track-valid"
+    if args.transform_int_slices:
+        substitutions["xform_int_bitslices"] = textwrap.dedent("""\
+            // Eliminate slices of integers by first converting the integer to a bitvector.
+            // e.g., if "x : integer", then "x[1 +: 8]" to "cvt_int_bits(x, 9)[1 +: 8]"
+            :xform_int_bitslices
+            """)
     if args.wrap_variables: substitutions['wrap_variables'] = ":xform_wrap"
     if not args.auto_case_split:
         substitutions['auto_case_split'] = '--no-auto-case-split'
@@ -492,6 +497,7 @@ def main() -> int:
     parser.add_argument("--new-ffi", help="use the new FFI", action="store_true", default=False)
     parser.add_argument("--runtime-checks", help="perform runtime checks (array bounds, etc.)", action="store_true", default=False)
     parser.add_argument("--split-state", help="split state into multiple structs", action=argparse.BooleanOptionalAction)
+    parser.add_argument("--transform-int-slices", help="convert integer slices to bit slices", action=argparse.BooleanOptionalAction, default=False)
     parser.add_argument("--instrument-unknown", help="instrument assignments of UNKNOWN", action=argparse.BooleanOptionalAction)
     parser.add_argument("--wrap-variables", help="wrap global variables into functions", action=argparse.BooleanOptionalAction)
     parser.add_argument("-O0", help="perform minimal set of transformations", action=argparse.BooleanOptionalAction)

libASL/backend_c_new.ml

@@ -629,9 +629,9 @@ and expr (loc : Loc.t) (fmt : PP.formatter) (x : AST.expr) : unit =
   | Expr_Slices (Type_Bits (n,_), e, [Slice_LoWd (lo, wd)]) ->
       let module Runtime = (val (!runtime) : RuntimeLib) in
       Runtime.get_slice fmt (const_int_expr loc n) (const_int_expr loc wd) (mk_expr loc e) (fun fmt -> index_expr loc fmt lo)
-  | Expr_Slices (Type_Integer _, e, [Slice_LoWd (lo, wd)]) when lo = Asl_utils.zero ->
+  | Expr_Slices (Type_Integer _, e, [Slice_LoWd (lo, wd)]) ->
       let module Runtime = (val (!runtime) : RuntimeLib) in
-      Runtime.cvt_int_bits fmt (const_int_expr loc wd) (mk_expr loc e)
+      Runtime.get_slice_int fmt (const_int_expr loc wd) (mk_expr loc e) (mk_expr loc lo)
   | Expr_TApply (f, tes, es, throws) ->
       if throws <> NoThrow then
         rethrow_expr fmt (fun _ -> funcall loc fmt f tes es)

libASL/runtime.ml

@@ -62,6 +62,7 @@ module type RuntimeLib = sig
   val pow2_int : PP.formatter -> rt_expr -> unit
   val align_int : PP.formatter -> rt_expr -> rt_expr -> unit
   val mod_pow2_int : PP.formatter -> rt_expr -> rt_expr -> unit
+  val get_slice_int : PP.formatter -> int -> rt_expr -> rt_expr -> unit
   val set_slice_int : PP.formatter -> int -> rt_expr -> rt_expr -> rt_expr -> unit
   val print_int_dec : PP.formatter -> rt_expr -> unit
   val print_int_hex : PP.formatter -> rt_expr -> unit

libASL/runtime.mli

@@ -61,6 +61,7 @@ module type RuntimeLib = sig
   val pow2_int : PP.formatter -> rt_expr -> unit
   val align_int : PP.formatter -> rt_expr -> rt_expr -> unit
   val mod_pow2_int : PP.formatter -> rt_expr -> rt_expr -> unit
+  val get_slice_int : PP.formatter -> int -> rt_expr -> rt_expr -> unit
   val set_slice_int : PP.formatter -> int -> rt_expr -> rt_expr -> rt_expr -> unit
   val print_int_dec : PP.formatter -> rt_expr -> unit
   val print_int_hex : PP.formatter -> rt_expr -> unit

libASL/runtime_ac.ml

@@ -367,6 +367,14 @@ module Runtime : RT.RuntimeLib = struct
   let cvt_bits_sint (fmt : PP.formatter) (n : int) (x : RT.rt_expr) : unit = cvt_bits_sint_aux fmt n int_width x
   let cvt_bits_uint (fmt : PP.formatter) (n : int) (x : RT.rt_expr) : unit = cvt_bits_uint_aux fmt n int_width x
 
+  let get_slice_int (fmt : PP.formatter) (w : int) (x : RT.rt_expr) (i : RT.rt_expr) : unit =
+    let mask = Z.sub (Z.shift_left Z.one w) Z.one in
+    PP.fprintf fmt "((%a)((%a >> %a) & %a))"
+      ty_uint w
+      RT.pp_expr x
+      RT.pp_expr i
+      (intN_literal int_width) mask
+
   let set_slice_int (fmt : PP.formatter) (w : int) (l : RT.rt_expr) (i : RT.rt_expr) (r : RT.rt_expr) : unit =
     let mask = Z.sub (Z.shift_left Z.one w) Z.one in
     PP.fprintf fmt "%a = ({ int __index = %a; %a __mask = %a << __index; (%a & ~__mask) | (((%a)%a) << __index); });"

libASL/runtime_c23.ml

@@ -385,6 +385,14 @@ module Runtime : RT.RuntimeLib = struct
   let cvt_bits_sint (fmt : PP.formatter) (n : int) (x : RT.rt_expr) : unit = cvt_bits_sint_aux fmt n int_width x
   let cvt_bits_uint (fmt : PP.formatter) (n : int) (x : RT.rt_expr) : unit = cvt_bits_uint_aux fmt n int_width x
 
+  let get_slice_int (fmt : PP.formatter) (w : int) (x : RT.rt_expr) (i : RT.rt_expr) : unit =
+    let mask = Z.sub (Z.shift_left Z.one w) Z.one in
+    PP.fprintf fmt "((%a)((%a >> %a) & %a))"
+      ty_uint w
+      RT.pp_expr x
+      RT.pp_expr i
+      (intN_literal int_width) mask
+
   let set_slice_int (fmt : PP.formatter) (w : int) (l : RT.rt_expr) (i : RT.rt_expr) (r : RT.rt_expr) : unit =
     let mask = Z.sub (Z.shift_left Z.one w) Z.one in
     PP.fprintf fmt "%a = ({ int __index = %a; %a __mask = %a << __index; (%a & ~__mask) | (((%a)%a) << __index); });"

libASL/runtime_fallback.ml

@@ -235,6 +235,14 @@ module Runtime : RT.RuntimeLib = struct
   let cvt_bits_uint (fmt : PP.formatter) (n : int) (x : RT.rt_expr) : unit = apply_bits_1_1 fmt "cvt_bits_uint" n x
   let cvt_int_bits (fmt : PP.formatter) (n : int) (x : RT.rt_expr) : unit = apply_bits_1_1 fmt "cvt_int_bits" n x
 
+  let get_slice_int (fmt : PP.formatter) (w : int) (x : RT.rt_expr) (i : RT.rt_expr) : unit =
+    let slice fmt =
+      PP.fprintf fmt "(%a >> %a)"
+        RT.pp_expr x
+        RT.pp_expr i
+    in
+    cvt_int_bits fmt w slice
+
   let set_slice_int (fmt : PP.formatter) (w : int) (l : RT.rt_expr) (i : RT.rt_expr) (r : RT.rt_expr) : unit =
     let mask = Z.sub (Z.shift_left Z.one w) Z.one in
     PP.fprintf fmt "%a = ({ int __index = %a; %a __mask = %a << __index; (%a & ~__mask) | (((%a)%a) << __index); });"

libASL/runtime_sc.ml

@@ -397,6 +397,14 @@ module Runtime : RT.RuntimeLib = struct
   let cvt_bits_sint (fmt : PP.formatter) (n : int) (x : RT.rt_expr) : unit = cvt_bits_sint_aux fmt n int_width x
   let cvt_bits_uint (fmt : PP.formatter) (n : int) (x : RT.rt_expr) : unit = cvt_bits_uint_aux fmt n int_width x
 
+  let get_slice_int (fmt : PP.formatter) (w : int) (x : RT.rt_expr) (i : RT.rt_expr) : unit =
+    let mask = Z.sub (Z.shift_left Z.one w) Z.one in
+    PP.fprintf fmt "((%a)((%a >> %a) & %a))"
+      ty_uint w
+      RT.pp_expr x
+      RT.pp_expr i
+      (intN_literal int_width) mask
+
   let set_slice_int (fmt : PP.formatter) (w : int) (l : RT.rt_expr) (i : RT.rt_expr) (r : RT.rt_expr) : unit =
     let mask = Z.sub (Z.shift_left Z.one w) Z.one in
     PP.fprintf fmt "%a = ({ int __index = %a; %a __mask = %a << __index; (%a & ~__mask) | (((%a)%a) << __index); });"