Fix bug with normalization of multidimensional arrays

kind2-mc · Jan 22, 2025 · 389763f · 389763f
1 parent 33d6499
commit 389763f
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 10 deletions.
diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml
@@ -352,7 +352,9 @@ let generalize_to_array_expr name ind_vars expr nexpr =
       A.StructDef (dpos, [SingleIdent (dpos, name)]), nexpr
     | ind_vars ->
       A.StructDef (dpos, [ArrayDef (dpos, name, ind_vars)]),
-      A.ArrayIndex (dpos, nexpr, A.Ident (dpos, List.hd ind_vars))
+      List.fold_left (fun acc ind_var -> 
+        A.ArrayIndex (dpos, acc, A.Ident (dpos, ind_var))  
+      ) nexpr ind_vars 
   in
   eq_lhs, nexpr
 
@@ -2019,20 +2021,21 @@ and normalize_expr ?guard info node_id map =
     let gids = union gids1 gids2 in
     let warnings = warnings1 @ warnings2 in
     if previously_guarded then
-      let nexpr' = match nexpr with
+      let rec process_expr nexpr = 
+        match nexpr with
         | A.ArrayIndex (pos2, expr1, expr2) ->
-          A.ArrayIndex (pos2, Pre (pos, expr1), expr2)
+          A.ArrayIndex (pos2, process_expr expr1, expr2)
         | e -> Pre (pos, e)
-      in
-      nexpr', gids, warnings
+      in 
+      process_expr nexpr, gids, warnings
     else
-      let nexpr' =
+      let rec process_expr nexpr = 
         match nexpr with
         | A.ArrayIndex (pos2, expr1, expr2) ->
-          A.ArrayIndex (pos2, A.Arrow (pos, guard, Pre (pos, expr1)), expr2)
-        | e -> Arrow (pos, guard, Pre (pos, e))
-      in
-      nexpr', gids, warnings
+          A.ArrayIndex (pos2, process_expr expr1, expr2)
+        | e -> A.Arrow (pos, guard, Pre (pos, e))
+      in 
+      process_expr nexpr, gids, warnings
   (* ************************************************************************ *)
   (* Misc. abstractions                                                       *)
   (* ************************************************************************ *)

diff --git a/tests/regression/success/multi_indices_array.lus b/tests/regression/success/multi_indices_array.lus
@@ -0,0 +1,5 @@
+node N() returns (out: int^4^4);
+let
+  out[i][j] = 0 -> pre (out[i][j] + 1);
+  check out[0][0] = 0 -> true;
+tel