Array constant initialisations now require a strict nesting level equal to the number of dimensions; simplified some related code

phases/desug.ml

@@ -2,32 +2,12 @@ open Printf
 open Types
 open Util
 
-(* Create new constant variables for all assigned array values so that they are
- * only evaluated once *)
-let rec consts_to_vars node =
-  let rec create_vars new_vars values = function
-    | [] -> (new_vars, values)
-    | hd :: tl ->
-      let (new_vars, value) = match hd with
-        | ArrayConst (values, ann) ->
-          let (new_vars, values) = create_vars new_vars [] values in
-          (new_vars, ArrayConst (values, ann))
-        | value ->
-          let index = fresh_const "const" in
-          (new_vars @ [(index, value)], Var (index, None, annof value))
-      in
-      create_vars new_vars (values @ [value]) tl
-  in
-  match node with
-  (* Add vardecs for values in arrayconst *)
-  | VarDec (ArrayDims _ as ctype, name, Some (ArrayConst (values, vann)), ann) ->
-    let (new_vars, values) = create_vars [] [] values in
-    let value = ArrayConst (values, vann) in
-    let create_vardec (name, value) =
-      VarDec (basetypeof node, name, Some value, annof value)
-    in
-    let new_vardecs = List.map create_vardec new_vars in
-    Block (new_vardecs @ [VarDec (ctype, name, Some value, ann)])
+(* Create new constant variables for scalar initialisations on arrays so that
+ * they are only evaluated once *)
+let rec move_scalars = function
+  (* Prevent next match for ArrayConst initialisations *)
+  | VarDec (ArrayDims _, _, Some (ArrayConst _), _) as node ->
+    node
 
   (* Add vardec for scalar value *)
   | VarDec (ArrayDims _ as ctype, name, Some value, ann) as node ->
@@ -37,21 +17,21 @@ let rec consts_to_vars node =
       VarDec (ctype, name, Some (Var (scalar_name, None, annof value)), ann);
     ]
 
-  | node -> traverse_unit consts_to_vars node
-
-let make_dims make_dimname values make_dec =
-  let names = mapi make_dimname values in
-
-  let decs = List.map2 make_dec values names in
-
-  let make_dim value name = Dim (name, annof value) in
-  let dims = List.map2 make_dim values names in
-
-  (decs, dims)
+  | node -> traverse_unit move_scalars node
 
 (* Generate new variables for array dimensions, to avoid re-evalutation when
  * array dimensions are used (e.g., after array dimension reduction). *)
 let rec array_dims node =
+  let make_dims make_dimname values make_dec =
+    let names = mapi make_dimname values in
+
+    let decs = List.map2 make_dec values names in
+
+    let make_dim value name = Dim (name, annof value) in
+    let dims = List.map2 make_dim values names in
+
+    (decs, dims)
+  in
   match node with
   | VarDec (ArrayDims (ctype, values), name, init, ann) ->
     (* Names for VarDec dimensions must be unique to avoid weid errors when
@@ -65,7 +45,7 @@ let rec array_dims node =
 
   | GlobalDef (export, ArrayDims (ctype, values), name, init, ann) ->
     (* For global decs, the name must be derived from the array base name, but
-     * not constant (no trailing __) since the variable must exist for exporting
+     * not constant (no trailing _) since the variable must exist for exporting
      * (and not pruned during constant propagation) *)
     let make_dimname i _ = generate_id name (i + 1) in
 
@@ -260,19 +240,40 @@ let rec array_init = function
       | value when depth = ndims ->
         let indices = List.map intconst indices in
         [Assign (name, Some (List.rev indices), value, ann)]
+      (* DISABLED: nesting level must be equal to number of dimensions
       | value when depth < ndims ->
         (* Use the for-loops constructed for scalar assignment *)
         let value = ArrayInit (value, dims) in
         let indices = List.map intconst indices in
         [array_init (Assign (name, Some (List.rev indices), value, ann))]
+      *)
       | node ->
-        let msg = sprintf
+        raise (FatalError (NodeMsg (node, sprintf
           "dimension mismatch: expected %d nesting levels, got %d"
-          ndims depth
-        in
-        raise (FatalError (NodeMsg (node, msg)))
+          ndims depth)))
+    in
+    Block (List.rev (traverse 0 [] value))
+
+    (*
+    let ndims = list_size dims in
+    let rec make_assigns depth i indices = function
+        | [] -> []
+        | hd :: tl ->
+            let assigns = traverse depth (i :: indices) hd in
+            make_assigns depth (i + 1) indices tl @ assigns
+    and traverse depth indices = function
+        | ArrayConst (values, _) ->
+            make_assigns (depth + 1) 0 indices values
+        | value when depth = ndims ->
+            let intconst i = Const (IntVal (Int32.of_int i), []) in
+            [Assign (name, Some (List.rev_map intconst indices), value, loc)]
+        | node ->
+            raise (FatalError (NodeMsg (node, sprintf
+                "dimension mismatch: expected %d nesting levels, got %d"
+                ndims depth)))
     in
     Block (List.rev (traverse 0 [] value))
+    *)
 
   (* Replace no indices with empty indices to have a list below *)
   | Assign (name, None, (ArrayInit _ as value), ann) ->
@@ -302,7 +303,7 @@ let phase = function
   | Ast node ->
     (* Generate variable declarations for expressions that must be evaluated
      * once and used multiple times *)
-    let node = consts_to_vars (array_dims node) in
+    let node = move_scalars (array_dims node) in
 
     (* Split variable initialisations into declarations and assignments, and
      * move the assignments to the function body *)
@@ -310,6 +311,6 @@ let phase = function
 
     (* Transform ArrayConst assignment to assignments in for-loops, and
      * transform all for-loops to while-loops afterwards *)
-    Ast (for_to_while (array_init (node)))
+    Ast (for_to_while (array_init node))
 
   | _ -> raise InvalidInput

phases/desug.mli

@@ -31,37 +31,30 @@ void foo() \{
     {3 Array initialisations}
 
     A more complex class of initialisations are array initialisations. Arrays
-    can be initialised to a scalar value or to an array constant. For array
-    constants that cover all array dimensions, separate assign statements are
-    generated for each array index. For scalar values and aray constants that
-    have a lower nesting level than the number of array dimensions, for-loops
-    are generated. The following example shows all situation:
+    can be initialised to a scalar value or to an array constant in bracket
+    notation. A scalar value is rewritten to a nested for-loop over all array
+    dmensions, with an assignment in the most nested loop. An array constant is
+    rewritten to a series of separate assign statements to the corresponding
+    array indices. The following example shows both transformations:
 {v void foo() \{
-    int[3] a = [1, 2, 3];
-    int[3] b = 4;
-    int[2, 2] c = [[3, 4], 5];
+    int[3] a = 4;
+    int[2, 2] b = [[3, 4], [5, 6]];
 \} v}
 
-    The snippet above is transformed to code equivalent to the following:
+    This is transformed into:
 
 {v void foo() \{
     int[] a;
     int[] b;
-    int[] c;
     a = __allocate(3);
-    a[0] = 1;
-    a[1] = 2;
-    a[2] = 3;
-    b = __allocate(3);
     for (int i = 0, 3) \{
-        b[i] = 4;
-    \}
-    c = __allocate(4);
-    c[0] = 3;
-    c[1] = 4;
-    for (int i = 0, 2) \{
-        c[1, i] = 5;
+        a[i] = 4;
     \}
+    b = __allocate(2, 2);
+    b[0, 0] = 1;
+    b[0, 1] = 2;
+    b[1, 0] = 3;
+    b[1, 1] = 4;
 \} v}
 
     {2 Prevent incorrect double evaluation}
@@ -73,45 +66,60 @@ int two() \{
   return 2;
 \}
 void foo() \{
-  int[2, two()] a = [[1, two()], [1, two()]];
+  int[2, two()] a = two();
+  printInt(twos);
   printInt(a[1, 1]);
 \} v}
 
-    [two()] must be evaluated exactly three times in order to preserve correct
-    behaviour. However, [a[1, 1]] will at a later stage be transformed into
-    [a[(1 * two()) + 1]], thus incorrectly evaluating [two()] an additional
-    time. Assigning a scalar value to an array creates the same problem, since
-    this is transformed into a for-loop, where the scalar expression is
-    evaluated during each iteration. The problem is solved by creating new
-    so-called "constant variables" for all of these values, and initializing hem
-    to the original expressions. The expressions are then replaced with usages
-    of these variables. A constant variable is a variable that is known to only
-    be assigned once in total. This is only true for some variables generated by
-    the compiler. In the later {!Constprop} phase, these assignments are a found
-    and those which assign constant values (e.g., integers), are propagated to
-    uses of the variable. This way, only the non-constant expressions are
-    defined in new variables in the resulting code.
-
-    For the example above, the result will be (after array dimension reduction
-    and constant propagation):
-{v ...
-void foo() \{
-    int _a_2_1_;
-    int _const_4_;
-    int _const_6_;
-    int[] a;
-    _a_2_1_ = two();
-    _const_4_ = two();
-    _const_6_ = two();
-    a := <allocate>((2 * _a_2_1_));
-    a[0] = 1;
-    a[1] = _const_4_;
-    a[_a_2_1_] = 1;
-    a[(_a_2_1_ + 1)] = _const_6_;
-    printInt(a[(_a_2_1_ + 1)]);
-\} v}
-
-
+    [two()] must be evaluated exactly twice in order to preserve correct
+    behaviour. However, the scalar inialisation will be transformed into a
+    for-loop, evaluating [two()] in each loop iteration. Moreover, [a[1, 1]]
+    would at a later stage (during array dimension reduction) be transformed
+    into [a[(1 * two()) + 1]], thus incorrectly evaluating [two()] an additional
+    time.
+
+    The problem is solved by generating new variables for scalar initialisations
+    and array dimensions, and replacing the original expression with the
+    generated variables. Note that these variables are marked so-called
+    "constant variables" since they are known to be assigned exactly once, and
+    thus optimizable by {!Constprop} in some cases. This way, only the
+    non-constant expressions are defined in new variables in the resulting code.
+
+    In the example above, [int[2, two()] a = two();] is transformed as follows:
+{v     ...
+    int _a_1_1_ = 2;  // will be propagated back by constant propagation
+    int _a_2_2_ = two();
+    int _scalar_3_ = two();
+    int[_a_1_1_, _a_2_2_] a = _scalar_3_;
+    ...  v}
+resulting in:
+{v     ...
+    int _a_1_1_;
+    int _a_2_2_;
+    int _scalar_3_;
+    int[_a_1_1_, _a_2_2_] a;
+    _a_1_1_ = 2;
+    _a_2_2_ = two();
+    _scalar_3_ = two();
+    a := <allocate>(_a_1_1_, _a_2_2_);
+    for (int _i_4 = 0, _a_1_1_) \{
+        for (int _i_5 = 0, _a_2_2_) \{
+            a[_i_4, _i_5] = _scalar_3_;
+        \}
+    \}
+    ...  v}
+
+    The [_a_1_1_] here is formed from the array name [a], the number of the
+    dimension [1], and a global counter variable that happened to be [1] at the
+    moment he variable was generated. The counter is necessary to make the
+    variable name unique, even when the program contains illegal name clashes,
+    which would yield weird errors during context analysis. E.g., a second
+    definition [int[2] a;] would generate a new variable [_a_1] which would
+    clash with the earlier [_a_1], yielding an error on compiler-generated code
+    instead of on the definition of [a].
+
+    Note that the for-loops are actually transformed into while-loops, but not
+    in this example in order to maintain readability.
 
     {2 Transforming for-loops to while-loops}
 

test/arrays/functional/array_init.cvc

@@ -13,15 +13,12 @@ void printArray2D(int[n, m] a) {
 }
 
 export int main() {
-    int[2,3] a = [[1, 2, 3], [4, 5, 6]];
-    int[2,3] b = 7;
-    int[2,3] c = [1, [2, 3, 4]];
+    int[2, 3] a = [[1, 2, 3], [4, 5, 6]];
+    int[2, 3] b = 7;
 
     printArray2D(a);
     printNewlines(1);
     printArray2D(b);
-    printNewlines(1);
-    printArray2D(c);
 
     return 0;
 }

test/arrays/functional/array_init.out

@@ -3,6 +3,3 @@
 
 7 7 7
 7 7 7
-
-1 1 1
-2 3 4

test/arrays/functional/array_init_global.cvc

@@ -12,7 +12,7 @@ void printArray2D(int[n, m] a) {
     }
 }
 
-int[2, 2] a = [[1, 2], 3];
+int[2, 2] a = [[1, 2], [3, 4]];
 
 export int main() {
     printArray2D(a);

test/arrays/functional/array_init_global.out

@@ -1,2 +1,2 @@
 1 2
-3 3
+3 4

test/arrays/functional/array_single_eval.cvc

@@ -49,8 +49,6 @@ void printArray3D(int[n, m, o] a) {
 export int main() {
     int[two()] a        = one();
     int[two(), two()] b = [[1, one()], [2, two()]];
-    int[2, 3] c         = [one(), two()];
-    int[2, 3, 3] d      = [one(), two()];
 
     printArray1D(a);
     printNewlines(1);
@@ -58,12 +56,6 @@ export int main() {
     printArray2D(b);
     printNewlines(1);
 
-    printArray2D(c);
-    printNewlines(1);
-
-    printArray3D(d);
-    printNewlines(1);
-
     printInt(ones);
     printSpaces(1);
     printInt(twos);

test/arrays/functional/array_single_eval.out

@@ -3,10 +3,4 @@
 1 1
 2 2
 
-1 1 1
-2 2 2
-
-1 1 1  1 1 1  1 1 1
-2 2 2  2 2 2  2 2 2
-
-4 6
+2 4

util.ml

@@ -493,7 +493,9 @@ let optmapl f = function
 let mapi f lst =
   let rec trav i = function
     | [] -> []
-    | hd :: tl -> f i hd :: (trav (i + 1) tl)
+    | hd :: tl ->
+      let hd = f i hd in
+      hd :: (trav (i + 1) tl)
   in trav 0 lst
 
 (** Constants that are *)