`copilot-c99`: `array has incomplete element type` error when declaring stream with array of structs

[RyanGlScott]

I write a Copilot spec involving a stream of structs:

-- Struct1.hs
{-# LANGUAGE DataKinds #-}
module Main where

import qualified Prelude as P
import Control.Monad (void, forM_)

import Language.Copilot
import Copilot.Compile.C99

data Volts = Volts
  { numVolts :: Field "numVolts" Word16
  , flag     :: Field "flag"     Bool
  }

instance Struct Volts where
  typename _ = "volts"
  toValues volts = [ Value Word16 (numVolts volts)
                   , Value Bool   (flag volts)
                   ]

instance Typed Volts where
  typeOf = Struct (Volts (Field 0) (Field False))

spec :: Spec
spec = trigger "f1" true [arg volts]
  where
    volts :: Stream Volts
    volts = constant $ Volts (Field 42) (Field True)

main :: IO ()
main = do
  spec' <- reify spec
  compile "struct1" spec'

Then the generated C code can be compiled:

// struct1.h
struct volts;
void f1(struct volts * f1_arg0);
void step(void);

// struct1.c
#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <stdlib.h>
#include <math.h>

#include "struct1.h"

struct volts
{ uint16_t numVolts;
  bool flag;
};

bool f1_guard(void) {
  return true;
}

struct volts f1_arg0(void) {
  return (struct volts){((uint16_t)(42)), (true)};
}

void step(void) {
  struct volts f1_arg_temp0;
  if ((f1_guard)()) {
    {(f1_arg_temp0) = ((f1_arg0)());
     (f1)((&(f1_arg_temp0)));}
  };
}

$ gcc -c struct1.c -o struct1.o # Succeeds

On the other hand, if I modify the spec above such that the trigger uses an array of structs:

-- Struct2.hs
{-# LANGUAGE DataKinds #-}
module Main where

import qualified Prelude as P
import Control.Monad (void, forM_)

import Language.Copilot
import Copilot.Compile.C99

data Volts = Volts
  { numVolts :: Field "numVolts" Word16
  , flag     :: Field "flag"     Bool
  }

instance Struct Volts where
  typename _ = "volts"
  toValues volts = [ Value Word16 (numVolts volts)
                   , Value Bool   (flag volts)
                   ]

instance Typed Volts where
  typeOf = Struct (Volts (Field 0) (Field False))

spec :: Spec
spec = trigger "f2" true [arg volts]
  where
    volts :: Stream (Array 2 Volts)
    volts = constant $ array
              [ Volts (Field 42) (Field True)
              , Volts (Field 27) (Field False)
              ]

main :: IO ()
main = do
  spec' <- reify spec
  compile "struct2" spec'

Then I am unable to compile the generated C code:

// struct2.h
struct volts;
void f2(struct volts f2_arg0[(2)]);
void step(void);

// struct2.c
#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <stdlib.h>
#include <math.h>

#include "struct2.h"

struct volts
{ uint16_t numVolts;
  bool flag;
};

bool f2_guard(void) {
  return true;
}

struct volts * f2_arg0(void) {
  return (struct volts [(2)]){{((uint16_t)(42)), (true)}, {((uint16_t)(27)), (false)}};
}

void step(void) {
  struct volts * f2_arg_temp0;
  if ((f2_guard)()) {
    {(f2_arg_temp0) = ((f2_arg0)());
     (f2)((f2_arg_temp0));}
  };
}

$ gcc -c struct2.c -o struct2.o
In file included from struct2.c:7:
struct2.h:2:22: error: array type has incomplete element type ‘struct volts’
    2 | void f2(struct volts f2_arg0[(2)]);
      |                      ^~~~~~~
struct2.c: In function ‘step’:
struct2.c:26:11: error: type of formal parameter 1 is incomplete
   26 |      (f2)((f2_arg_temp0));}
      |           ^~~~~~~~~~~~~~

In struct2.h, we have:

struct volts;
void f2(struct volts f2_arg0[(2)]);

This uses a forward declaration for struct volts, but in order to use struct volts as the element type in array, the compiler must know how large the struct is, which is not possible with only a forward declaration. This issue did not arise in struct1.h because f1's argument uses a pointer to a struct volts value, which does not require advance knowledge of the size of the struct.

[fdedden]

Thanks for mentioning this. Moving the definition of the struct from the .c to the .h file will solve this problem.

Initially the C99 backend of Copilot is designed to interface on existing code primarily. The actual/primary definition would then be defined in already existing C code (written outside the scope of Copilot). Moving the definition to the .h file more or less breaks with this idea.

The current implementation is indeed problematic. I will need to discuss with @ivanperez-keera to see what the exact implications are when moving the definition to the .h file.

[ivanperez-keera]

The implications are that, in many cases, the code that uses Copilot will not be able to import the .h file. Oftentimes, those structs will be defined in different header files (e.g., from mavlink, cFE and other libraries), so this would lead to duplicate (and possibly incompatible) definitions within the same scope (the scope being the C code that calls Copilot).

Do we need an external and an internal header file? Is there possibly a smarter solution?

[ivanperez-keera]

I guess of course one could, in the C implementation, define the structs (and any local types) before importing the header file.

It's a bit ugly to me, but I'm no C expert.

Would that always work?

[fdedden]

The implications are that, in many cases, the code that uses Copilot will not be able to import the .h file. Oftentimes, those structs will be defined in different header files (e.g., from mavlink, cFE and other libraries), so this would lead to duplicate (and possibly incompatible) definitions within the same scope (the scope being the C code that calls Copilot).

That is exactly the problem. The definition used by Copilot is only an internal representation. It is up to the user to make sure it is equal to the externally defined C one.

I guess of course one could, in the C implementation, define the structs (and any local types) before importing the header file.

No I don't think that would work, as struct2.c together with struct2.h are their own 'compilation unit'. I.e. they are compiled separately from any other c files, unless one or more header files tell them where to find it. Let me try something out to be certain.

[ivanperez-keera]

I don't understand why it would not work.

I mean this:

// struct2.c
#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <stdlib.h>
#include <math.h>

struct volts
{ uint16_t numVolts;
  bool flag;
};

#include "struct2.h"

bool f2_guard(void) {
  return true;
}

struct volts * f2_arg0(void) {
  return (struct volts [(2)]){{((uint16_t)(42)), (true)}, {((uint16_t)(27)), (false)}};
}

void step(void) {
  struct volts * f2_arg_temp0;
  if ((f2_guard)()) {
    {(f2_arg_temp0) = ((f2_arg0)());
     (f2)((f2_arg_temp0));}
  };
}

[fdedden]

Oh sorry, I misunderstood you then. I thought you meant write the declaration of the struct in main.c, prior the import of struct2.h. That wouldn't fork the reasons I mentioned.

Your solution however, works. It is a bit unusual, as we force a declaration of the struct onto the header file (in another .c file we could provide it with a different declaration).

I think we can safely rewrite it that way.

[fdedden]

Probably a nicer approach (but also one that changes Copilot more significantly) is that we allow the user to tell which .h files need to be included in struct2.h for the declaration. In that way Copilot would reuse the already existing ones without using an internal one.

Initially we did not take this approach as there did not seem a reason to do so. Having Copilot use an internal declaration is conceptually simpler as it does not force anyone to think about linking all the necessary files.

[ivanperez-keera]

That also makes sense.

A third alternative would be, in the header file, to conditionally define the C structs.

#ifdef LOCAL_STRUCT_DEFS
struct volts
{ uint16_t numVolts;
  bool flag;
};
#else
struct volts;
#endif

void f2(struct volts f2_arg0[(2)]);
void step(void);

In the C code, we write:

<some other libraries>

#define LOCAL_STRUCT_DEFS
#include "struct2.h"

<continues>

[fdedden]

That would also work. I think we want to rename the macro to something like USE_COPILOT_INTERNAL_DECLARATIONS to make it more self-documented.

To sumarise, we have three valid options:

1. Ask the user of Copilot to provide the correct header files, so they can be included in the .h file. This requires an extra step from the user that does not provide any extra to the user experience, e.g. no extra safety or checks. From a C standpoint it is the nicest: all the code shares the same declarations instead of relying on two declarations (that should be the same) that just happen to share the same name.

2. Switch the order of declaration and #include in the .c file. This is an easy fix, and although a bit unusual, is perfectly valid C code.

3. Enable the internal representation only for .c/.h files that Copilot generates. Regular includes of the .h file will ignore this and keep using the forward declaration. This code is a bit less unusual then option 2, but makes the code of the .h file less readable, as it will not be immediately clear how struct volts is declared. Additionally, I am not certain if there are any C coding style regulations that might be broken with this approach. I can imagine certification of such code is more difficult, as it not immediately clear what is going on. But again, I can not confirm nor deny this. This might be something worth looking into. Possibly @agoodloe could help on this end?

[ivanperez-keera]

I think maybe @RyanGlScott and @robdockins can also help us understand if options 2 and 3 would make their verification work harder.

It sounds like option 1 would be the best, although it would require a bit more work. But not a lot:

• Change C settings to have two extra fields extraIncludes :: [String], defineStructs :: Bool.
• Change mkDefaultCSettings to make that extraIncludes = [] and defineStructs = True.
• Change C code generator to include those files: ++ map ("#include " ++) (extraIncludes cSettings) ++ in the middle of cmacros in Compiler.hs.
• Change C code generator to only include the structs if defineStructs cSettings.

All pre-existing code will keep compiling.

[ivanperez-keera]

This removes the "check" that the struct definition that the Copilot code is working with is the one defined in Haskell, which may affect the verification work. The proofs generated would be subject to the definition of the struct that comes from the user being "compatible" (whatever that means) with what Haskell/Copilot expected. What is or isn't compatible (as opposed to exactly equal) may depend on the operations applied to the struct (access, copy?).

[fdedden]

Sounds like that would be the best approach then.

• Change C settings to have two extra fields extraIncludes :: [String], defineStructs :: Bool.

I understand that allowing Copilot to still generate the structs is important for backwards compatibility. However in the long run, I don't think we should allow the user to have this choice. It would be better to force one particular way. This simplifies the implementation and documentation.

[ivanperez-keera]

It's a bit more than that. What I like about that possibility is that it allows you to compile the generated code without any extra include directories. Once we start adding extra includes, and do not generate the structs, any verification, test, etc. becomes much more complicated because it requires extra flags. Handling libraries and dependencies and all that is generally a pain in the neck.

[RyanGlScott]

I don't think any of the options presented above would be especially difficult for us to handle. The first step that our verifier performs is to invoke clang -c foo.c in the same directory that foo.h lives. We can easily change the CSettings if need be in case we need to explicitly add foo.h to extraIncludes.

[ivanperez-keera]

I think the issue here might be that you might have to add options to clang, that is, additional includes (-I<path>).

[RyanGlScott]

I'm not sure why -I would be necessary—would the header files be generated in a different directory? In any case, we have full control over how clang is invoked, so passing additional arguments shouldn't be difficult.

[ivanperez-keera]

Well, the idea would be that users would be able to say things like:

    compileWith settings spec'
  where
    settings :: CSettings
    settings = mkDefaultCSettings { extraIncludes = [ "<OpenCV/OpenCV.h>", "\"Ardupilot/std_msgs.h\"" ] }

and so on.

That way, the resulting spec can refer to structs defined in those header files.

You just need to make sure that clang can find those header files. Whether users need to use additional environment variables that the clang process inherits, or something else, idk.

[ivanperez-keera]

I guess the issue does not arise so much if people use "\"PATH\"" syntax (if clang is executed from the same path) but when they use "<PATH>" syntax.

[RyanGlScott]

Well, the idea would be that users would be able to say things like:

    compileWith settings spec'
  where
    settings :: CSettings
    settings = mkDefaultCSettings { extraIncludes = [ "<OpenCV/OpenCV.h>", "\"Ardupilot/std_msgs.h\"" ] }

and so on.

That way, the resulting spec can refer to structs defined in those header files.

Ah, I see what you mean. At present, our verifier only supports the structs that copilot-c99 itself generates. It would be interesting to be able to verify specifications that refer to arbitrary, user-defined structs, but that would likely require adding some more user-configurable knobs to support, and perhaps some thought about what requirements the struct definitions should adhere to. That is to say: this isn't a use case that we've thought much about, so I trust your judgment about which design is the best here.

[ivanperez-keera]

@fdedden We are dealing with bugs differently now. I will clear the assignment and remove the bug label.

[fdedden]

I think maybe @RyanGlScott and @robdockins can also help us understand if options 2 and 3 would make their verification work harder.

It sounds like option 1 would be the best, although it would require a bit more work. But not a lot:

• Change C settings to have two extra fields extraIncludes :: [String], defineStructs :: Bool.

• Change mkDefaultCSettings to make that extraIncludes = [] and defineStructs = True.

• Change C code generator to include those files: ++ map ("#include " ++ (extraIncludes cSettings) ++ in the middle of cmacros in Compiler.hs.

• Change C code generator to only include the structs if defineStructs cSettings.

All pre-existing code will keep compiling.

I have made these modifications (with slightly altered names for the CSettings records): https://github.com/Copilot-Language/copilot/compare/master...fdedden:copilot:develop-struct-declns?expand=1

The struct declarations are completely removed from the .c file. The forward declarations previously generated for the .h file are replaced by the declarations, but only if cSettingsGenerateStructDeclarations is true.

Note: moving the declaration to the .h file breaks backwards compatibility, but keeping them in the .c file does not fix the problem of this issue.

Any optionally provided extra includes are only added to the .c file. As was already the case with Copilot, the .h file does not include anything. All dependencies of that file need to be included manually prior to including the file itself.

Note that the extra includes are taken literally: a user of Copilot needs to provide the mandatory "" or <> around the filename, e.g.:

mkDefaultCSettings {cSettingsExtraIncludes = ["\"external.h\""], cSettingsGenerateStructDeclarations = False}

What do you guys think? I am open for any ideas/improvements.

[RyanGlScott]

This plan shouldn't pose any obstacles verification-wise. In fact, all of our current tests continue to pass with the patch in https://github.com/Copilot-Language/copilot/issues/373#issuecomment-1264672483.

The original test case in https://github.com/Copilot-Language/copilot/issues/373#issue-1349644079 now compiles with Clang as well after applying the patch, although the test case doesn't pass our verifier due to the fact that f1_arg0 returns a dangling pointer (which I understand is a separate issue).

[ivanperez-keera]

@fdedden There is a simpler solution to this immediate issue that does not require relying on additional includes and is backwards compatible. To illustrate what I'm proposing, I'll use the following names:

• spec.c: file where the Copilot monitors are generated.
• spec.h: accompanying header file generated by Copilot.
• main.c: main file written by the user by hand.

The solution I propose is:

1. Generate the structs in a separate header file, named spec_types.h.
2. Include that file before including spec.h in spec.c.
3. Let users decide if they wish to import that file or not before they include spec.h from their respective main.c.

Benefits:

• Clean.
• Backwards compatible.
• Solves the issue.
• Does not need to extend with the includes feature, which we may want to think about separately and more thoroughly.

[ivanperez-keera]

In the future, we could evaluate using custom includes and, partly independently, give users the ability to not import our custom types. But that be a new feature, and evaluated separately.

[ivanperez-keera]

Description

Copilot-generated C99 monitor implementation files import the corresponding generated headers before defining the necessary C structs. Part of those headers contain the declarations of the handlers, which may take structs as arguments.

By using such forward declarations, the C compiler is not always able to figure out the size of the arguments to those handler functions, and the code cannot be compiled.

For example, the following spec:

-- Struct2.hs
{-# LANGUAGE DataKinds #-}
module Main where

import qualified Prelude as P
import Control.Monad (void, forM_)

import Language.Copilot
import Copilot.Compile.C99

data Volts = Volts
  { numVolts :: Field "numVolts" Word16
  , flag     :: Field "flag"     Bool
  }

instance Struct Volts where
  typename _ = "volts"
  toValues volts = [ Value Word16 (numVolts volts)
                   , Value Bool   (flag volts)
                   ]

instance Typed Volts where
  typeOf = Struct (Volts (Field 0) (Field False))

spec :: Spec
spec = trigger "f2" true [arg volts]
  where
    volts :: Stream (Array 2 Volts)
    volts = constant $ array
              [ Volts (Field 42) (Field True)
              , Volts (Field 27) (Field False)
              ]

main :: IO ()
main = do
  spec' <- reify spec
  compile "struct2" spec'

Results in the following C code:

// struct2.h
struct volts;
void f2(struct volts f2_arg0[(2)]);
void step(void);

// struct2.c
#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <stdlib.h>
#include <math.h>

#include "struct2.h"

struct volts
{ uint16_t numVolts;
  bool flag;
};

bool f2_guard(void) {
  return true;
}

struct volts * f2_arg0(void) {
  return (struct volts [(2)]){{((uint16_t)(42)), (true)}, {((uint16_t)(27)), (false)}};
}

void step(void) {
  struct volts * f2_arg_temp0;
  if ((f2_guard)()) {
    {(f2_arg_temp0) = ((f2_arg0)());
     (f2)((f2_arg_temp0));}
  };
}

which cannot be compiled:

$ gcc -c struct2.c -o struct2.o
In file included from struct2.c:7:
struct2.h:2:22: error: array type has incomplete element type ‘struct volts’
    2 | void f2(struct volts f2_arg0[(2)]);
      |                      ^~~~~~~
struct2.c: In function ‘step’:
struct2.c:26:11: error: type of formal parameter 1 is incomplete
   26 |      (f2)((f2_arg_temp0));}
      |           ^~~~~~~~~~~~~~

Type

• Bug: code produced canot be compiled.

Additional context

None.

Requester

• Ryan Scott (Galois)

Method to check presence of bug

The C code generated from the following specification fails to compile if the bug is present:

-- Struct2.hs
{-# LANGUAGE DataKinds #-}
module Main where

import qualified Prelude as P
import Control.Monad (void, forM_)

import Language.Copilot
import Copilot.Compile.C99

data Volts = Volts
  { numVolts :: Field "numVolts" Word16
  , flag     :: Field "flag"     Bool
  }

instance Struct Volts where
  typename _ = "volts"
  toValues volts = [ Value Word16 (numVolts volts)
                   , Value Bool   (flag volts)
                   ]

instance Typed Volts where
  typeOf = Struct (Volts (Field 0) (Field False))

spec :: Spec
spec = trigger "f2" true [arg volts]
  where
    volts :: Stream (Array 2 Volts)
    volts = constant $ array
              [ Volts (Field 42) (Field True)
              , Volts (Field 27) (Field False)
              ]

main :: IO ()
main = do
  spec' <- reify spec
  compile "struct2" spec'

Expected result

The code above and the generated C99 code can be compiled.

The C99 code produced includes the definitions of the structs before declaring the global structs and the handlers.

Desired result

The code above and the generated C99 code can be compiled.

The C99 code produced includes the definitions of the structs before declaring the global structs and the handlers.

Proposed solution

Produce the struct definitions in a separate file (e.g., prefix ++ "_types.h", using the internal Copilot nomenclature).

Include such file only from the implementation file, before including the header file for the specification.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that the bug is present.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 3.12.

Fix assigned to @fdedden .

[fdedden]

I have written a preliminary solution: https://github.com/Copilot-Language/copilot/compare/master...fdedden:copilot:develop-struct-declns?expand=1

[RyanGlScott]

When I try that branch on the following program:

module Main (main) where

import qualified Prelude as P ()

import Copilot.Compile.C99
import Language.Copilot

fibs :: Stream Word32
fibs = [1, 1] ++ (fibs + drop 1 fibs)

evenStream :: Stream Word32 -> Stream Bool
evenStream n = (n `mod` constant 2) == constant 0

oddStream :: Stream Word32 -> Stream Bool
oddStream n = not (evenStream n)

spec :: Spec
spec = do
  trigger "even" (evenStream fibs) [arg fibs]
  trigger "odd"  (oddStream fibs) [arg fibs]

main :: IO ()
main = do
  spec' <- reify spec
  compile "fibonacci" spec'

I get the following exception:

$ runghc Main.hs
Main.hs: Empty TransUnit is not allowed
CallStack (from HasCallStack):
  error, called at src/Language/C99/Util/IsList.hs:10:24 in language-c99-util-0.2.0-c4fad7a54c84871ec0f0bb814309cdf966e88a455ecfc6cc141aac21c38e7232:Language.C99.Util.IsList