copilot-language's duplicate extern check doesn't work correctly for locals

[RyanGlScott]

Consider this Copilot spec:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
moduleMain (main) whereimportCopilot.Compile.C99importLanguage.Copilots::StreamWord64
s = extern @(Array2Word64) "x"Nothing! extern @Word32"x"Nothingspec::Spec
spec = trigger "trig" true [arg s]
main::IO()
main =do
spec' <- reify spec
compile "bug" spec'

The definition of s is erroneous, as it declares two externs x with distinct types (Array 2 Word64 and Word32). If you attempt to reify this, copilot-language's analysis will detect this and raise an error:

*** Exception: *** Exception: Copilot error: The external symbol 'x' has been declared to have two different types!
CallStack (from HasCallStack):
error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.8-inplace:Copilot.Language.Error

So far, so good. Now consider what happens if you use this slightly modified definition of s:

s::StreamWord64
s = local (extern @(Array2Word64) "x"Nothing) (! extern @Word32"x"Nothing)

This time, the first extern (of type Array 2 Word64) has been bound using local, but the second extern (of type Word32) has not. Copilot will happily compile this version of the spec to C code:

#include<stdint.h>#include<stdbool.h>#include<string.h>#include<stdlib.h>#include<math.h>#include"bug_types.h"#include"bug.h"staticuint64_tx_cpy[(2)];
staticbooltrig_0_guard(void) {
return true;
}
staticuint64_ttrig_0_arg0(void) {
uint64_t*local_0= (x_cpy);
return (local_0)[x_cpy];
}
voidstep(void) {
uint64_ttrig_0_arg_temp0;
(memcpy)((x_cpy), (x), ((2) * (sizeof(uint64_t))));
if ((trig_0_guard)()) {
{(trig_0_arg_temp0) = ((trig_0_arg0)());
(trig)((trig_0_arg_temp0));}
};
}

This C code is very wrong, however, as it attempts to use local_0 (of type uint64_t*) as an array index, which is ill-typed:

$ clang bug.c -c
bug.c:18:19: error: array subscript is not an integer
18 | return (local_0)[x_cpy];
| ^~~~~~
1 error generated.

Why does Copilot detect the duplicate externs in the first version of the program but not the second? It's because of how copilot-language implements this check:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Line 330 in 4e5fd9a

Local e _ -> go nodes env e

This checks e (the first argument to local) for duplicate externs, but it does not check the result of the higher-order function (the second argument to local). To do this check correctly, we'd need to look at both. One way to do so would be to mirror another check elsewhere in copilot-language, which passes a dummy variable to the higher-order function in order to evaluate it:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Lines 144 to 145 in 4e5fd9a

	Local e f -> go seenExt nodes' e >>
	go seenExt nodes' (f (Var"dummy"))

[RyanGlScott]

Consider this Copilot spec:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
moduleMain (main) whereimportCopilot.Compile.C99importLanguage.Copilots::StreamWord64
s = extern @(Array2Word64) "x"Nothing! extern @Word32"x"Nothingspec::Spec
spec = trigger "trig" true [arg s]
main::IO()
main =do
spec' <- reify spec
compile "bug" spec'

The definition of s is erroneous, as it declares two externs x with distinct types (Array 2 Word64 and Word32). If you attempt to reify this, copilot-language's analysis will detect this and raise an error:

*** Exception: *** Exception: Copilot error: The external symbol 'x' has been declared to have two different types!
CallStack (from HasCallStack):
error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.8-inplace:Copilot.Language.Error

So far, so good. Now consider what happens if you use this slightly modified definition of s:

s::StreamWord64
s = local (extern @(Array2Word64) "x"Nothing) (! extern @Word32"x"Nothing)

This time, the first extern (of type Array 2 Word64) has been bound using local, but the second extern (of type Word32) has not. Copilot will happily compile this version of the spec to C code:

#include<stdint.h>#include<stdbool.h>#include<string.h>#include<stdlib.h>#include<math.h>#include"bug_types.h"#include"bug.h"staticuint64_tx_cpy[(2)];
staticbooltrig_0_guard(void) {
return true;
}
staticuint64_ttrig_0_arg0(void) {
uint64_t*local_0= (x_cpy);
return (local_0)[x_cpy];
}
voidstep(void) {
uint64_ttrig_0_arg_temp0;
(memcpy)((x_cpy), (x), ((2) * (sizeof(uint64_t))));
if ((trig_0_guard)()) {
{(trig_0_arg_temp0) = ((trig_0_arg0)());
(trig)((trig_0_arg_temp0));}
};
}

This C code is very wrong, however, as it attempts to use local_0 (of type uint64_t*) as an array index, which is ill-typed:

$ clang bug.c -c
bug.c:18:19: error: array subscript is not an integer
18 | return (local_0)[x_cpy];
| ^~~~~~
1 error generated.

Why does Copilot detect the duplicate externs in the first version of the program but not the second? It's because of how copilot-language implements this check:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Line 330 in 4e5fd9a

Local e _ -> go nodes env e

This checks e (the first argument to local) for duplicate externs, but it does not check the result of the higher-order function (the second argument to local). To do this check correctly, we'd need to look at both. One way to do so would be to mirror another check elsewhere in copilot-language, which passes a dummy variable to the higher-order function in order to evaluate it:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Lines 144 to 145 in 4e5fd9a

	Local e f -> go seenExt nodes' e >>
	go seenExt nodes' (f (Var"dummy"))

[RyanGlScott]

Consider this Copilot spec:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
moduleMain (main) whereimportCopilot.Compile.C99importLanguage.Copilots::StreamWord64
s = extern @(Array2Word64) "x"Nothing! extern @Word32"x"Nothingspec::Spec
spec = trigger "trig" true [arg s]
main::IO()
main =do
spec' <- reify spec
compile "bug" spec'

The definition of s is erroneous, as it declares two externs x with distinct types (Array 2 Word64 and Word32). If you attempt to reify this, copilot-language's analysis will detect this and raise an error:

*** Exception: *** Exception: Copilot error: The external symbol 'x' has been declared to have two different types!
CallStack (from HasCallStack):
error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.8-inplace:Copilot.Language.Error

So far, so good. Now consider what happens if you use this slightly modified definition of s:

s::StreamWord64
s = local (extern @(Array2Word64) "x"Nothing) (! extern @Word32"x"Nothing)

This time, the first extern (of type Array 2 Word64) has been bound using local, but the second extern (of type Word32) has not. Copilot will happily compile this version of the spec to C code:

#include<stdint.h>#include<stdbool.h>#include<string.h>#include<stdlib.h>#include<math.h>#include"bug_types.h"#include"bug.h"staticuint64_tx_cpy[(2)];
staticbooltrig_0_guard(void) {
return true;
}
staticuint64_ttrig_0_arg0(void) {
uint64_t*local_0= (x_cpy);
return (local_0)[x_cpy];
}
voidstep(void) {
uint64_ttrig_0_arg_temp0;
(memcpy)((x_cpy), (x), ((2) * (sizeof(uint64_t))));
if ((trig_0_guard)()) {
{(trig_0_arg_temp0) = ((trig_0_arg0)());
(trig)((trig_0_arg_temp0));}
};
}

This C code is very wrong, however, as it attempts to use local_0 (of type uint64_t*) as an array index, which is ill-typed:

$ clang bug.c -c
bug.c:18:19: error: array subscript is not an integer
18 | return (local_0)[x_cpy];
| ^~~~~~
1 error generated.

Why does Copilot detect the duplicate externs in the first version of the program but not the second? It's because of how copilot-language implements this check:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Line 330 in 4e5fd9a

Local e _ -> go nodes env e

This checks e (the first argument to local) for duplicate externs, but it does not check the result of the higher-order function (the second argument to local). To do this check correctly, we'd need to look at both. One way to do so would be to mirror another check elsewhere in copilot-language, which passes a dummy variable to the higher-order function in order to evaluate it:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Lines 144 to 145 in 4e5fd9a

	Local e f -> go seenExt nodes' e >>
	go seenExt nodes' (f (Var"dummy"))

[RyanGlScott]

Consider this Copilot spec:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
moduleMain (main) whereimportCopilot.Compile.C99importLanguage.Copilots::StreamWord64
s = extern @(Array2Word64) "x"Nothing! extern @Word32"x"Nothingspec::Spec
spec = trigger "trig" true [arg s]
main::IO()
main =do
spec' <- reify spec
compile "bug" spec'

The definition of s is erroneous, as it declares two externs x with distinct types (Array 2 Word64 and Word32). If you attempt to reify this, copilot-language's analysis will detect this and raise an error:

*** Exception: *** Exception: Copilot error: The external symbol 'x' has been declared to have two different types!
CallStack (from HasCallStack):
error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.8-inplace:Copilot.Language.Error

So far, so good. Now consider what happens if you use this slightly modified definition of s:

s::StreamWord64
s = local (extern @(Array2Word64) "x"Nothing) (! extern @Word32"x"Nothing)

This time, the first extern (of type Array 2 Word64) has been bound using local, but the second extern (of type Word32) has not. Copilot will happily compile this version of the spec to C code:

#include<stdint.h>#include<stdbool.h>#include<string.h>#include<stdlib.h>#include<math.h>#include"bug_types.h"#include"bug.h"staticuint64_tx_cpy[(2)];
staticbooltrig_0_guard(void) {
return true;
}
staticuint64_ttrig_0_arg0(void) {
uint64_t*local_0= (x_cpy);
return (local_0)[x_cpy];
}
voidstep(void) {
uint64_ttrig_0_arg_temp0;
(memcpy)((x_cpy), (x), ((2) * (sizeof(uint64_t))));
if ((trig_0_guard)()) {
{(trig_0_arg_temp0) = ((trig_0_arg0)());
(trig)((trig_0_arg_temp0));}
};
}

This C code is very wrong, however, as it attempts to use local_0 (of type uint64_t*) as an array index, which is ill-typed:

$ clang bug.c -c
bug.c:18:19: error: array subscript is not an integer
18 | return (local_0)[x_cpy];
| ^~~~~~
1 error generated.

Why does Copilot detect the duplicate externs in the first version of the program but not the second? It's because of how copilot-language implements this check:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Line 330 in 4e5fd9a

Local e _ -> go nodes env e

This checks e (the first argument to local) for duplicate externs, but it does not check the result of the higher-order function (the second argument to local). To do this check correctly, we'd need to look at both. One way to do so would be to mirror another check elsewhere in copilot-language, which passes a dummy variable to the higher-order function in order to evaluate it:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Lines 144 to 145 in 4e5fd9a

	Local e f -> go seenExt nodes' e >>
	go seenExt nodes' (f (Var"dummy"))

[RyanGlScott]

Consider this Copilot spec:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
moduleMain (main) whereimportCopilot.Compile.C99importLanguage.Copilots::StreamWord64
s = extern @(Array2Word64) "x"Nothing! extern @Word32"x"Nothingspec::Spec
spec = trigger "trig" true [arg s]
main::IO()
main =do
spec' <- reify spec
compile "bug" spec'

The definition of s is erroneous, as it declares two externs x with distinct types (Array 2 Word64 and Word32). If you attempt to reify this, copilot-language's analysis will detect this and raise an error:

*** Exception: *** Exception: Copilot error: The external symbol 'x' has been declared to have two different types!
CallStack (from HasCallStack):
error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.8-inplace:Copilot.Language.Error

So far, so good. Now consider what happens if you use this slightly modified definition of s:

s::StreamWord64
s = local (extern @(Array2Word64) "x"Nothing) (! extern @Word32"x"Nothing)

This time, the first extern (of type Array 2 Word64) has been bound using local, but the second extern (of type Word32) has not. Copilot will happily compile this version of the spec to C code:

#include<stdint.h>#include<stdbool.h>#include<string.h>#include<stdlib.h>#include<math.h>#include"bug_types.h"#include"bug.h"staticuint64_tx_cpy[(2)];
staticbooltrig_0_guard(void) {
return true;
}
staticuint64_ttrig_0_arg0(void) {
uint64_t*local_0= (x_cpy);
return (local_0)[x_cpy];
}
voidstep(void) {
uint64_ttrig_0_arg_temp0;
(memcpy)((x_cpy), (x), ((2) * (sizeof(uint64_t))));
if ((trig_0_guard)()) {
{(trig_0_arg_temp0) = ((trig_0_arg0)());
(trig)((trig_0_arg_temp0));}
};
}

This C code is very wrong, however, as it attempts to use local_0 (of type uint64_t*) as an array index, which is ill-typed:

$ clang bug.c -c
bug.c:18:19: error: array subscript is not an integer
18 | return (local_0)[x_cpy];
| ^~~~~~
1 error generated.

Why does Copilot detect the duplicate externs in the first version of the program but not the second? It's because of how copilot-language implements this check:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Line 330 in 4e5fd9a

Local e _ -> go nodes env e

This checks e (the first argument to local) for duplicate externs, but it does not check the result of the higher-order function (the second argument to local). To do this check correctly, we'd need to look at both. One way to do so would be to mirror another check elsewhere in copilot-language, which passes a dummy variable to the higher-order function in order to evaluate it:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Lines 144 to 145 in 4e5fd9a

	Local e f -> go seenExt nodes' e >>
	go seenExt nodes' (f (Var"dummy"))

[RyanGlScott]

Consider this Copilot spec:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
moduleMain (main) whereimportCopilot.Compile.C99importLanguage.Copilots::StreamWord64
s = extern @(Array2Word64) "x"Nothing! extern @Word32"x"Nothingspec::Spec
spec = trigger "trig" true [arg s]
main::IO()
main =do
spec' <- reify spec
compile "bug" spec'

The definition of s is erroneous, as it declares two externs x with distinct types (Array 2 Word64 and Word32). If you attempt to reify this, copilot-language's analysis will detect this and raise an error:

*** Exception: *** Exception: Copilot error: The external symbol 'x' has been declared to have two different types!
CallStack (from HasCallStack):
error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.8-inplace:Copilot.Language.Error

So far, so good. Now consider what happens if you use this slightly modified definition of s:

s::StreamWord64
s = local (extern @(Array2Word64) "x"Nothing) (! extern @Word32"x"Nothing)

This time, the first extern (of type Array 2 Word64) has been bound using local, but the second extern (of type Word32) has not. Copilot will happily compile this version of the spec to C code:

#include<stdint.h>#include<stdbool.h>#include<string.h>#include<stdlib.h>#include<math.h>#include"bug_types.h"#include"bug.h"staticuint64_tx_cpy[(2)];
staticbooltrig_0_guard(void) {
return true;
}
staticuint64_ttrig_0_arg0(void) {
uint64_t*local_0= (x_cpy);
return (local_0)[x_cpy];
}
voidstep(void) {
uint64_ttrig_0_arg_temp0;
(memcpy)((x_cpy), (x), ((2) * (sizeof(uint64_t))));
if ((trig_0_guard)()) {
{(trig_0_arg_temp0) = ((trig_0_arg0)());
(trig)((trig_0_arg_temp0));}
};
}

This C code is very wrong, however, as it attempts to use local_0 (of type uint64_t*) as an array index, which is ill-typed:

$ clang bug.c -c
bug.c:18:19: error: array subscript is not an integer
18 | return (local_0)[x_cpy];
| ^~~~~~
1 error generated.

Why does Copilot detect the duplicate externs in the first version of the program but not the second? It's because of how copilot-language implements this check:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Line 330 in 4e5fd9a

Local e _ -> go nodes env e

This checks e (the first argument to local) for duplicate externs, but it does not check the result of the higher-order function (the second argument to local). To do this check correctly, we'd need to look at both. One way to do so would be to mirror another check elsewhere in copilot-language, which passes a dummy variable to the higher-order function in order to evaluate it:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Lines 144 to 145 in 4e5fd9a

	Local e f -> go seenExt nodes' e >>
	go seenExt nodes' (f (Var"dummy"))

[RyanGlScott]

Consider this Copilot spec:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
moduleMain (main) whereimportCopilot.Compile.C99importLanguage.Copilots::StreamWord64
s = extern @(Array2Word64) "x"Nothing! extern @Word32"x"Nothingspec::Spec
spec = trigger "trig" true [arg s]
main::IO()
main =do
spec' <- reify spec
compile "bug" spec'

The definition of s is erroneous, as it declares two externs x with distinct types (Array 2 Word64 and Word32). If you attempt to reify this, copilot-language's analysis will detect this and raise an error:

*** Exception: *** Exception: Copilot error: The external symbol 'x' has been declared to have two different types!
CallStack (from HasCallStack):
error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.8-inplace:Copilot.Language.Error

So far, so good. Now consider what happens if you use this slightly modified definition of s:

s::StreamWord64
s = local (extern @(Array2Word64) "x"Nothing) (! extern @Word32"x"Nothing)

This time, the first extern (of type Array 2 Word64) has been bound using local, but the second extern (of type Word32) has not. Copilot will happily compile this version of the spec to C code:

#include<stdint.h>#include<stdbool.h>#include<string.h>#include<stdlib.h>#include<math.h>#include"bug_types.h"#include"bug.h"staticuint64_tx_cpy[(2)];
staticbooltrig_0_guard(void) {
return true;
}
staticuint64_ttrig_0_arg0(void) {
uint64_t*local_0= (x_cpy);
return (local_0)[x_cpy];
}
voidstep(void) {
uint64_ttrig_0_arg_temp0;
(memcpy)((x_cpy), (x), ((2) * (sizeof(uint64_t))));
if ((trig_0_guard)()) {
{(trig_0_arg_temp0) = ((trig_0_arg0)());
(trig)((trig_0_arg_temp0));}
};
}

This C code is very wrong, however, as it attempts to use local_0 (of type uint64_t*) as an array index, which is ill-typed:

$ clang bug.c -c
bug.c:18:19: error: array subscript is not an integer
18 | return (local_0)[x_cpy];
| ^~~~~~
1 error generated.

Why does Copilot detect the duplicate externs in the first version of the program but not the second? It's because of how copilot-language implements this check:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Line 330 in 4e5fd9a

Local e _ -> go nodes env e

This checks e (the first argument to local) for duplicate externs, but it does not check the result of the higher-order function (the second argument to local). To do this check correctly, we'd need to look at both. One way to do so would be to mirror another check elsewhere in copilot-language, which passes a dummy variable to the higher-order function in order to evaluate it:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Lines 144 to 145 in 4e5fd9a

	Local e f -> go seenExt nodes' e >>
	go seenExt nodes' (f (Var"dummy"))

[RyanGlScott]

Consider this Copilot spec:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
moduleMain (main) whereimportCopilot.Compile.C99importLanguage.Copilots::StreamWord64
s = extern @(Array2Word64) "x"Nothing! extern @Word32"x"Nothingspec::Spec
spec = trigger "trig" true [arg s]
main::IO()
main =do
spec' <- reify spec
compile "bug" spec'

The definition of s is erroneous, as it declares two externs x with distinct types (Array 2 Word64 and Word32). If you attempt to reify this, copilot-language's analysis will detect this and raise an error:

*** Exception: *** Exception: Copilot error: The external symbol 'x' has been declared to have two different types!
CallStack (from HasCallStack):
error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.8-inplace:Copilot.Language.Error

So far, so good. Now consider what happens if you use this slightly modified definition of s:

s::StreamWord64
s = local (extern @(Array2Word64) "x"Nothing) (! extern @Word32"x"Nothing)

This time, the first extern (of type Array 2 Word64) has been bound using local, but the second extern (of type Word32) has not. Copilot will happily compile this version of the spec to C code:

#include<stdint.h>#include<stdbool.h>#include<string.h>#include<stdlib.h>#include<math.h>#include"bug_types.h"#include"bug.h"staticuint64_tx_cpy[(2)];
staticbooltrig_0_guard(void) {
return true;
}
staticuint64_ttrig_0_arg0(void) {
uint64_t*local_0= (x_cpy);
return (local_0)[x_cpy];
}
voidstep(void) {
uint64_ttrig_0_arg_temp0;
(memcpy)((x_cpy), (x), ((2) * (sizeof(uint64_t))));
if ((trig_0_guard)()) {
{(trig_0_arg_temp0) = ((trig_0_arg0)());
(trig)((trig_0_arg_temp0));}
};
}

This C code is very wrong, however, as it attempts to use local_0 (of type uint64_t*) as an array index, which is ill-typed:

$ clang bug.c -c
bug.c:18:19: error: array subscript is not an integer
18 | return (local_0)[x_cpy];
| ^~~~~~
1 error generated.

Why does Copilot detect the duplicate externs in the first version of the program but not the second? It's because of how copilot-language implements this check:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Line 330 in 4e5fd9a

Local e _ -> go nodes env e

This checks e (the first argument to local) for duplicate externs, but it does not check the result of the higher-order function (the second argument to local). To do this check correctly, we'd need to look at both. One way to do so would be to mirror another check elsewhere in copilot-language, which passes a dummy variable to the higher-order function in order to evaluate it:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Lines 144 to 145 in 4e5fd9a

	Local e f -> go seenExt nodes' e >>
	go seenExt nodes' (f (Var"dummy"))