Fix array support (-Oarray optimization)

bin/iic.py

@@ -150,6 +150,14 @@
 // introduced by previous transforms
 :xform_constprop --nounroll
 
+// Wrap arrays in records to simplify C code generation.
+// This is a workaround for the fact that C does not support array
+// assignment but does support struct assignment.
+// The transformation must be done after monomorphization because
+// we need to generate a separate tuple for each distinct array
+// size&type.
+{xform_arrays}
+
 // Optimization: optionally use :xform_bounded to represent any
 // constrained integers by an integer that is exactly the right size
 // to contain it.
@@ -331,7 +339,8 @@ def mk_script(args, output_directory):
     if args.O0:
         script = []
         script.append(":filter_unlisted_functions imports")
-        script.append(":filter_reachable_from --no-keep-builtins exports")
+        script.append(":filter_reachable_from exports")
+        if args.Oarrays: script.append(":xform_arrays")
         if args.Obounded: script.append(":xform_bounded")
         if args.transform_foreign: script.append(":xform_foreign")
         if args.show_final_isa:
@@ -341,6 +350,7 @@ def mk_script(args, output_directory):
         return "\n".join(script)
 
     substitutions = {
+        'auto_case_split': '--no-auto-case-split',
         'bounded_int': "",
         'command':     " ".join(sys.argv),
         'generate_c':  generate_c,
@@ -350,6 +360,7 @@ def mk_script(args, output_directory):
         'xform_int_bitslices': "",
         'track_valid': "",
         'wrap_variables': "",
+        'xform_arrays': "",
     }
     if args.instrument_unknown: substitutions['track_valid'] = ":xform_valid track-valid"
     if args.transform_foreign:
@@ -365,12 +376,9 @@ def mk_script(args, output_directory):
             // 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'
-    else:
-        substitutions['auto_case_split'] = '--auto-case-split'
-    if args.Obounded:
-        substitutions['bounded_int'] = ':xform_bounded'
+    if args.auto_case_split: substitutions['auto_case_split'] = '--auto-case-split'
+    if args.Oarrays: substitutions['xform_arrays'] = ':xform_arrays'
+    if args.Obounded: substitutions['bounded_int'] = ':xform_bounded'
     if args.backend in ["ac", "sc"]: substitutions['suppress_bitslice_xform'] = "--notransform"
 
     script = base_script.format(**substitutions)
@@ -431,6 +439,7 @@ def run_iii(iii, args, isa_files, project_file, configurations):
     iii_cmd.append("--check-exception-markers")
     if args.constraint_checks: print("Warning: ignoring --check-constraints")
     iii_cmd.append("--runtime-checks" if args.runtime_checks else "--no-runtime-checks")
+    if args.Oarrays: iii_cmd.append("--exec=:xform_arrays")
     if args.Obounded: iii_cmd.append("--exec=:xform_bounded")
     iii_cmd.append(f"--project={project_file}")
     for file in configurations:
@@ -532,6 +541,7 @@ def main() -> int:
     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)
+    parser.add_argument("-Oarrays", help="enable array lowering optimization", action="store_true", default=False)
     parser.add_argument("-Obounded", help="enable integer bounding optimization", action="store_true", default=False)
     parser.add_argument("--backend", help="select backend (default: c23)", choices=['ac', 'c23', 'interpreter', 'fallback', 'mlir', 'sc'], default='c23')
     parser.add_argument("--print-c-flags", help="print the C flags needed to use the selected ISA C runtime", action=argparse.BooleanOptionalAction)
@@ -589,6 +599,7 @@ def main() -> int:
         iii_cmd.append("--check-exception-markers")
         if args.constraint_checks: print("Warning: ignoring --check-constraints")
         iii_cmd.append("--runtime-checks" if args.runtime_checks else "--no-runtime-checks")
+        if args.Oarrays: iii_cmd.append("--exec=:xform_arrays")
         if args.Obounded: iii_cmd.append("--exec=:xform_bounded")
         iii_cmd.extend([
             "--exec=let result := main();",

libISA/asl_parser.mly

@@ -680,7 +680,7 @@ aexpr:
 | tc = path "{" fas = separated_nonempty_list(",", field_assignment) "}"
     { Expr_Record(tc, [], fas) }
 | "array" "(" es = separated_nonempty_list(",", expr) ")"
-    { Expr_ArrayInit(es) }
+    { Expr_ArrayInit(Isa_utils.type_unknown, es) }
 | "(" fas = separated_nonempty2_list(",", field_assignment) ")" ":" ty=simple_type
     { Expr_Record(fst ty, snd ty, fas) }
 | "(" e = expr ")"

libISA/backend_c.ml

@@ -755,9 +755,6 @@ and expr (loc : Loc.t) (fmt : PP.formatter) (x : AST.expr) : unit =
       raise (Error.Unimplemented (loc, "expression", pp))
   )
 
-and exprs (loc : Loc.t) (fmt : PP.formatter) (es : AST.expr list) : unit =
-  commasep (expr loc) fmt es
-
 (* The same as expr except that it guarantees that the result is a legal type
  * to use as a C/C++ array index.
  *)
@@ -1171,6 +1168,18 @@ let pp_field (loc : Loc.t) (fmt : PP.formatter) (f : (Ident.t * AST.ty)) : unit
   varty loc fmt fname t;
   semicolon fmt
 
+let rec pp_initializer (loc : Loc.t) (fmt : PP.formatter) (x : AST.expr) : unit =
+  ( match x with
+  | Expr_ArrayInit (_, es) ->
+      PP.fprintf fmt "{ %a }"
+        (commasep (pp_initializer loc)) es
+  | Expr_Record (tc, [], fas) ->
+      PP.fprintf fmt "(%a){ %a }"
+        ident tc
+        (commasep (fun fmt' (f, e) -> PP.fprintf fmt' ".%a = %a" ident f (pp_initializer loc) e)) fas
+  | _ -> expr loc fmt x
+  )
+
 let declaration (fmt : PP.formatter) ?(is_extern : bool option) (x : AST.declaration) : unit =
   let is_extern_val = Option.value is_extern ~default:false in
   vbox fmt (fun _ ->
@@ -1185,22 +1194,19 @@ let declaration (fmt : PP.formatter) ?(is_extern : bool option) (x : AST.declara
               let pp fmt = FMT.tycon fmt tc in
               raise (Error.Unimplemented (Loc.Unknown, "builtin type", pp))
           )
-      | Decl_Const (v, oty, e, loc) ->
+      | Decl_Const (v, Some ty, e, loc) ->
           PP.fprintf fmt "const ";
-          varoty loc fmt v oty;
+          varoty loc fmt v (Some ty);
           if not is_extern_val then (
-            PP.fprintf fmt " = ";
-            ( match e with
-            | Expr_ArrayInit es -> PP.fprintf fmt "{ %a }" (exprs loc) es
-            | _ -> expr loc fmt e
-            )
+            PP.fprintf fmt " = %a"
+              (pp_initializer loc) e
           );
           PP.fprintf fmt ";@,@,"
       | Decl_Config (v, ty, i, loc) ->
           varty loc fmt v ty;
           if not is_extern_val then (
-            PP.fprintf fmt " = ";
-            expr loc fmt i
+            PP.fprintf fmt " = %a"
+              (pp_initializer loc) i
           );
           PP.fprintf fmt ";@,@,"
       | Decl_Enum (tc, es, loc) ->

libISA/dune

@@ -70,6 +70,7 @@
    value
    visitor
    check_monomorphization
+   xform_arrays
    xform_bitslices
    xform_bittuples
    xform_bounded

libISA/eval.ml

@@ -389,7 +389,7 @@ and eval_expr' (loc : Loc.t) (env : Env.t) (x : AST.expr) : value =
       !r
   | Expr_Record (tc, _, fas) ->
       mk_record tc (List.map (fun (f, e) -> (f, eval_expr loc env e)) fas)
-  | Expr_ArrayInit es ->
+  | Expr_ArrayInit (_, es) ->
       let inits = List.mapi (fun i e -> (i, eval_expr loc env e)) es in
       init_array inits VUninitialized
   | Expr_In (e, p) -> from_bool (eval_pattern loc env (eval_expr loc env e) p)

libISA/isa_ast.ml

@@ -74,7 +74,7 @@ and expr =
  | Expr_Slices of ty * expr * slice list (* bitslice *)
  | Expr_WithChanges of ty * expr * (change * expr) list (* copy with changes *)
  | Expr_Record of Ident.t * (Ident.t option * expr) list * (Ident.t * expr) list
- | Expr_ArrayInit of expr list
+ | Expr_ArrayInit of (ty * expr list)
  | Expr_In of expr * pattern (* pattern match *)
  | Expr_Var of Ident.t
  | Expr_Tuple of expr list (* tuple *)

libISA/isa_fmt.ml

@@ -363,9 +363,10 @@ and expr (fmt : PP.formatter) (x : AST.expr) : unit =
       tycon fmt tc;
       if not (Utils.is_empty tes) then parens fmt (fun _ -> pp_args fmt tes);
       braces fmt (fun _ -> commasep fmt (field_assignment fmt) fas)
-  | Expr_ArrayInit es ->
-      PP.fprintf fmt "%t (%a)"
+  | Expr_ArrayInit (t, es) ->
+      Format.fprintf fmt "%t of %a (%a)"
         kw_array
+        ty t
         exprs es
   | Expr_In (e, p) ->
       PP.fprintf fmt "(%a IN %a)"

libISA/isa_parser.mly

@@ -270,7 +270,7 @@ let literal_expression :=
 let aggregate :=
     (* Note that record aggregates are parsed as function calls *)
     | "(" ; es = separated_nonempty2_list(",", expr) ; ")" ; { Expr_Tuple(es) }
-    | "array" ; "(" ; es = separated_nonempty_list(",", expr) ; ")" ; { Expr_ArrayInit(es) }
+    | "array" ; "(" ; es = separated_nonempty_list(",", expr) ; ")" ; { Expr_ArrayInit(Isa_utils.type_unknown, es) }
 
 let field_assignment :=
     | f = ident ; "=>" ; e = expr ; { (f, e) }

libISA/isa_visitor.ml

@@ -218,9 +218,10 @@ and visit_expr (vis : isaVisitor) (x : expr) : expr =
         let tes' = visit_args vis tes in
         let fas' = mapNoCopy (visit_fieldassignment vis) fas in
         if tc == tc' && tes == tes' && fas == fas' then x else Expr_Record (tc', tes', fas')
-    | Expr_ArrayInit es ->
+    | Expr_ArrayInit (t, es) ->
+        let t' = visit_type vis t in
         let es' = visit_exprs vis es in
-        if es == es' then x else Expr_ArrayInit es'
+        if t == t' && es == es' then x else Expr_ArrayInit (t', es')
     | Expr_In (e, p) ->
         let e' = visit_expr vis e in
         let p' = visit_pattern vis p in

libISA/tcheck.ml

@@ -2025,9 +2025,9 @@ and tc_expr (env : Env.t) (loc : Loc.t) (x : AST.expr) : AST.expr * AST.ty =
       in
 
       (Expr_Record (tc', args', fas'), Type_Constructor (tc', es'))
-  | Expr_ArrayInit [] ->
+  | Expr_ArrayInit (_, []) ->
       raise (InternalError (loc, "expr ArrayInit is empty", (fun fmt -> FMT.expr fmt x), __LOC__))
-  | Expr_ArrayInit (e::es) ->
+  | Expr_ArrayInit (_, e::es) ->
       let (e', ty) = tc_expr env loc e in
       let rty = ref ty in
       let es' = List.map
@@ -2039,7 +2039,7 @@ and tc_expr (env : Env.t) (loc : Loc.t) (x : AST.expr) : AST.expr * AST.ty =
       in
       let n = List.length (e::es) in
       let ixty = Index_Int (mk_litint n) in
-      (Expr_ArrayInit (e'::es'), Type_Array (ixty, !rty))
+      (Expr_ArrayInit (!rty, e'::es'), Type_Array (ixty, !rty))
   | Expr_In (e, p) ->
       let (e', ety') = tc_expr env loc e in
       if !verbose then

libISA/xform_arrays.ml

@@ -0,0 +1,154 @@
+(****************************************************************
+ * ISA array wrapping transform
+ *
+ * Wraps arrays in records
+ *
+ * This makes code generation easier because it allows
+ * us to copy arrays using assignment.
+ *
+ * Copyright (C) 2025-2025 Intel Corporation
+ * SPDX-License-Identifier: BSD-3-Clause
+ ****************************************************************)
+
+module AST = Isa_ast
+
+(****************************************************************
+ * Wrapper generation code
+ ****************************************************************)
+
+(* To simplify code generation for array assignment,
+ * we wrap all arrays in records.
+ * Doing this correctly requires that we use the same
+ * record for every occurence of the same type.
+ *)
+module Ty = struct
+  type t = AST.ty
+  let compare (x : t) (y : t) : int = Stdlib.compare x y
+end
+
+module TypeMap = Map.Make(Ty) (* cache types *)
+
+let typenames = new Isa_utils.nameSupply "__Type_"
+
+let wrapper_field = Ident.mk_ident "data"
+
+(****************************************************************
+ * Transform
+ ****************************************************************)
+
+(* It is important that equivalent types are transformed to the same
+ * record so we normalize range types like "{1, 2, 7}" to "{1..7}".
+ *
+ * Returns the input set unchanged if unable to infer the min and max value.
+ *)
+let simplify_ranges (ranges : AST.set_range list) : AST.set_range list =
+  let range_min_max (r : AST.set_range) : (AST.expr option * AST.expr option) =
+    ( match r with
+    | Set_Single x -> (Some x, Some x)
+    | Set_Range (lo, hi) -> (lo, hi)
+    )
+  in
+  let min (x : AST.expr) (y : AST.expr) : AST.expr option =
+    ( match (x, y) with
+    | (Expr_Lit (VInt x'), Expr_Lit (VInt y')) -> Some (Expr_Lit (VInt (Z.min x' y')))
+    | (_, _) -> None
+    )
+  in
+  let max (x : AST.expr) (y : AST.expr) : AST.expr option =
+    ( match (x, y) with
+    | (Expr_Lit (VInt x'), Expr_Lit (VInt y')) -> Some (Expr_Lit (VInt (Z.max x' y')))
+    | (_, _) -> None
+    )
+  in
+  let merge (x : (AST.expr option * AST.expr option)) (y : (AST.expr option * AST.expr option)) : (AST.expr option * AST.expr option) =
+    let (xl, xh) = x in
+    let (yl, yh) = y in
+    let l = Option.join (Utils.map2_option min xl yl) in
+    let h = Option.join (Utils.map2_option max xh yh) in
+    (l, h)
+  in
+  ( match ranges with
+  | [] -> []
+  | (r :: rs) ->
+      let lohi = ref (range_min_max r) in
+      List.iter (fun r -> lohi := merge !lohi (range_min_max r)) rs;
+      let (lo, hi) = !lohi in
+      [Set_Range (lo, hi)]
+  )
+
+class replaceArrayClass (tc : Ident.t option) = object (self)
+  inherit Isa_visitor.nopIsaVisitor
+  val mutable typemap : Ident.t TypeMap.t = TypeMap.empty
+
+  method mkTypeName (x : AST.ty) : Ident.t =
+    ( match TypeMap.find_opt x typemap with
+    | Some r -> r
+    | None ->
+          let r = typenames#fresh in
+          typemap <- TypeMap.add x r typemap;
+          r
+    )
+
+  method mkTypeWrappers : AST.declaration list =
+    List.map
+      (fun (t, nm) -> AST.Decl_Record (nm, [], [(wrapper_field, t)], Loc.Unknown))
+      (TypeMap.bindings typemap)
+
+  method! vtype (x : AST.ty) =
+    ( match x with
+    | Type_Array _ ->
+        ChangeDoChildrenPost (x, fun x' ->
+          let tc = self#mkTypeName x' in
+          AST.Type_Constructor (tc, []))
+    | Type_Integer (Some ranges) ->
+        ChangeTo (Type_Integer (Some (simplify_ranges ranges)))
+    | _ -> DoChildren
+    )
+
+  method! vexpr (x : AST.expr) =
+    ( match x with
+    | Expr_Array (a, ix) ->
+        let a' = Isa_visitor.visit_expr (self :> Isa_visitor.isaVisitor) a in
+        let ix' = Isa_visitor.visit_expr (self :> Isa_visitor.isaVisitor) ix in
+        ChangeTo (AST.Expr_Array (AST.Expr_Field (a', wrapper_field), ix'))
+    | Expr_ArrayInit (t, es) ->
+        let t' = Isa_visitor.visit_type (self :> Isa_visitor.isaVisitor) t in
+        let es' = Isa_visitor.visit_exprs (self :> Isa_visitor.isaVisitor) es in
+        let e' = AST.Expr_ArrayInit (t, es') in
+        let n = AST.Expr_Lit (VInt (Z.of_int (List.length es'))) in
+        let aty = AST.Type_Array (AST.Index_Int n, t') in
+        let tc = self#mkTypeName aty in
+        ChangeTo (AST.Expr_Record (tc, [], [(wrapper_field, e')]))
+    | _ -> DoChildren
+    )
+
+  method! vlexpr (x : AST.lexpr) =
+    ( match x with
+    | LExpr_Array (a, ix) ->
+        let a' = Isa_visitor.visit_lexpr (self :> Isa_visitor.isaVisitor) a in
+        let ix' = Isa_visitor.visit_expr (self :> Isa_visitor.isaVisitor) ix in
+        ChangeTo (AST.LExpr_Array (AST.LExpr_Field (a', wrapper_field), ix'))
+    | _ -> DoChildren
+    )
+end
+
+let xform_decls (ds : AST.declaration list) : AST.declaration list =
+  let replacer = new replaceArrayClass None in
+  let ds' = List.map (Isa_visitor.visit_decl (replacer :> Isa_visitor.isaVisitor)) ds in
+  let tuple_decls = replacer#mkTypeWrappers in
+  ds' @ tuple_decls
+
+(****************************************************************
+ * Command: :xform_tuples
+ ****************************************************************)
+
+let _ =
+  let cmd (tcenv : Tcheck.Env.t) (cpu : Cpu.cpu) : bool =
+    Commands.declarations := xform_decls !Commands.declarations;
+    true
+  in
+  Commands.registerCommand "xform_arrays" [] [] [] "Wrap array accesses" cmd
+
+(****************************************************************
+ * End
+ ****************************************************************)

libISA/xform_arrays.mli

@@ -0,0 +1,10 @@
+(****************************************************************
+ * ISA array wrapping transform
+ *
+ * Copyright (C) 2025-2025 Intel Corporation
+ * SPDX-License-Identifier: BSD-3-Clause
+ ****************************************************************)
+
+(****************************************************************
+ * End
+ ****************************************************************)