Copilot-Language / copilot

A stream-based runtime-verification framework for generating hard real-time C code.
http://copilot-language.github.io
616 stars 49 forks source link

`copilot-c99`: Can C99 generator declare stream functions as static? #507

Open simondlevy opened 3 months ago

simondlevy commented 3 months ago

C code output by Copilot declares variables static but functions global; e.g.:

static size_t s3_idx = (0);

float s0_get(size_t x) {
  return (s0)[((s0_idx) + (x)) % (1)];
}

Global declaration of functions causes duplicate-name conflicts when linking together multiple C sources output by Copilot. Issue could probably be handled by a script, but I'm wondering why the local functions are being declared without static to begin with.

ivanperez-keera commented 3 months ago

That's a good point. I see no reason to make them public and I agree that it would be better to make functions static.

ivanperez-keera commented 2 months ago

@fdedden Did you have a chance to look into this? Do you think this can be done without negative impact?

fdedden commented 2 months ago

Dear Simon, thank you for the suggestion. Yes, it is indeed better to have these functions defined as static. It forces the so called 'storage duration' to be as long as the execution of the program (which is what we want here). As you mentioned, adding static to global functions keeps the function private to the execution unit (similar to a file in this case) as well.

The addition of the keyword has already been implemented in January for the 3.18 release of Copilot (see 6779d032d2f8f0a6b5e7d7067e75c6ce901d41e9) to comply with the MISRA C coding standard. It should suffice for you to upgrade to at least the 3.18 release.

Please let me know if you have any more questions.

Reference to the C99 standard, section 6.2.2 and 6.2.4: http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf.

ivanperez-keera commented 2 months ago

The addition of the keyword has already been implemented in January for the 3.18

I think I only added it for variables, not functions, didn't I?

fdedden commented 2 months ago

The addition of the keyword has already been implemented in January for the 3.18

I think I only added it for variables, not functions, didn't I?

No? The commit I mentioned (https://github.com/Copilot-Language/copilot/commit/6779d032d2f8f0a6b5e7d7067e75c6ce901d41e9) adds static to the generator and accessor functions, and omits the step function (which is what we want).

The variables have been defined static since I wrote the first version of the C99 backend.

Let me also ping @simondlevy, since I forgot to do that in my initial reply.

ivanperez-keera commented 2 months ago

You're right. I completely forgot! :open_mouth:

ivanperez-keera commented 1 month ago

@simondlevy have you been able to try with the latest version?

simondlevy commented 1 month ago

I bought a new computer recently and installed Copilot on it following the instructions as usual. When I tried the heater example, the compiled C header still did make the declarations static.

ivanperez-keera commented 4 weeks ago

But were functions static or not? That was the issue, wasn't it?

fdedden commented 1 week ago

@simondlevy Just to confirm: your issue has been solved, right?