Fixed weird context analysis on array dimension names

phases/context.ml

@@ -9,6 +9,8 @@ let type2str = function Funcname _ -> "function" | Varname _ -> "variable"
 let mapfind name tbl =
   if Hashtbl.mem tbl name then Some (Hashtbl.find tbl name) else None
 
+let is_generated name = String.contains name '$'
+
 let check_in_scope name errnode scope =
   let (vars, funs) = scope in
   let (name, tbl, other_map, desired_type) = match name with
@@ -34,10 +36,16 @@ let add_to_scope name dec depth (vars, funs) =
   (* Identifiers of lower depth may be overwritten, but idenetifiers at
     * the same depth must be unique for consistency *)
   | Some (orig, orig_depth, _) when orig_depth >= depth ->
-    let msg = sprintf "Error: cannot redeclare %s \"%s\"" name_type name in
-    prerr_loc_msg (locof dec) msg;
-    prerr_loc_msg (locof orig) "Previously declared here:";
-    raise EmptyError
+    (* For generated variables, don't gove an error, since the error variable
+     * is a derived array dimension of a redefined array, which will yield an
+     * error later on *)
+    if is_generated name then
+      Hashtbl.replace tbl name (dec, depth, name_type)
+    else
+      let msg = sprintf "Error: cannot redeclare %s \"%s\"" name_type name in
+      prerr_loc_msg (locof dec) msg;
+      prerr_loc_msg (locof orig) "Previously declared here:";
+      raise EmptyError
   | Some _ ->
     Hashtbl.replace tbl name (dec, depth, name_type)
   | None ->

phases/desug.ml

@@ -64,9 +64,10 @@ let rec array_dims node =
     Block (decs @ [VarDec (ArrayDims (ctype, dims), name, init, ann)])
 
   | GlobalDef (export, ArrayDims (ctype, values), name, init, ann) ->
-    (* For global decs, the name must also be unique, but not constant (no $$in
-     * the name) since the variable must exist for exporting *)
-    let make_dimname i _ = fresh_var (name ^ "$" ^ string_of_int (i + 1)) in
+    (* For global decs, the name must be derived from the array base name, but
+     * not constant (no $$in the name) since the variable must exist for
+     * exporting (and not pruned during constant propagation) *)
+    let make_dimname i _ = name ^ "$" ^ string_of_int (i + 1) in
 
     let make_dec value name = GlobalDef (export, Int, name, Some value, []) in
     let (decs, dims) = make_dims make_dimname values make_dec in

phases/extern.ml

@@ -116,10 +116,16 @@ let rec replace_vars scope depth = function
     let params = List.map trav params in
     FunDef (export, ret_type, name, params, trav body, ann)
 
+  (* Use of regular external variable *)
   | VarUse (dec, None, _) when Hashtbl.mem scope (nameof dec) ->
     let (get, _) = Hashtbl.find scope (nameof dec) in
     get [] depth
 
+  (* Dereference of external array *)
+  | VarUse (dec, Some indices, _) when Hashtbl.mem scope (nameof dec) ->
+    let (get, _) = Hashtbl.find scope (nameof dec) in
+    get indices depth
+
   | VarLet (dec, dims, value, _) when Hashtbl.mem scope (nameof dec) ->
     let dims = optmapl (replace_vars scope depth) dims in
     let (_, set) = Hashtbl.find scope (nameof dec) in

test/arrays/combined_extern_array/defs.cvc

@@ -0,0 +1 @@
+export int[3] foo = [1, 2, 3];

test/arrays/combined_extern_array/expected.out

@@ -0,0 +1 @@
+123

test/arrays/combined_extern_array/main.cvc

@@ -0,0 +1,10 @@
+extern void printInt(int val);
+
+extern int[n] foo;
+
+export int main() {
+    printInt(foo[0]);
+    printInt(foo[1]);
+    printInt(foo[2]);
+    return 0;
+}