copilot-c99: Allow using same trigger name in multiple declarations

[antanas-kalkauskas-sensmetry]

If we have a Copilot specification where we have multiple conditions for triggering the same function (but perhaps we are providing different arguments), then in generated C code we would have multiple declarations of trigger functions and multiple definitions of helper functions and the generated code could not be compiled without modifications.

Example

Suppose we would like to trigger the switchOffPower(..) function if the current of one of the components is too large. We would also like to pass the value of the signal and the index of the component to the switchOffPower(..).

{-# LANGUAGE RebindableSyntax #-}

module RepeatedDeclarationsExample where
import Language.Copilot

import Copilot.Compile.C99

current1 :: Stream Float 
current1 = extern "current_signal1" Nothing 

current2 :: Stream Float 
current2 = extern "current_signal2" Nothing

spec = do
    trigger "switchOffPower" (current1 > 0.8) [arg current1, arg (constant 0 :: Stream Word8)]
    trigger "switchOffPower" (current2 > 0.8) [arg current2, arg (constant 1 :: Stream Word8)]

main :: IO ()
main = do
    reify spec >>= compile "repeated_declarations_example"

Then the repeated_declarations_example.h declares switchOffPower(..) twice:

extern float current_signal1;
extern float current_signal2;
void switchOffPower(float switchOffPower_arg0, uint8_t switchOffPower_arg1);
void switchOffPower(float switchOffPower_arg0, uint8_t switchOffPower_arg1);
void step(void);

And repeated_declarations_example.c contains multiple definitions of bool switchOffPower_guard(void), float switchOffPower_arg0(void), uint8_t switchOffPower_arg1(void) .

#include <stdint.h>
#include <stdbool.h>
#include <string.h>
#include <stdlib.h>
#include <math.h>

#include "repeated_declarations_example.h"

static float current_signal1_cpy;
static float current_signal2_cpy;

bool switchOffPower_guard(void) {
  return (current_signal1_cpy) > ((float)(0.800000011920929));
}

float switchOffPower_arg0(void) {
  return current_signal1_cpy;
}

uint8_t switchOffPower_arg1(void) {
  return (uint8_t)(0);
}

bool switchOffPower_guard(void) {
  return (current_signal2_cpy) > ((float)(0.800000011920929));
}

float switchOffPower_arg0(void) {
  return current_signal2_cpy;
}

uint8_t switchOffPower_arg1(void) {
  return (uint8_t)(1);
}

void step(void) {
  (current_signal1_cpy) = (current_signal1);
  (current_signal2_cpy) = (current_signal2);
  if ((switchOffPower_guard)()) {
    {(switchOffPower)(((switchOffPower_arg0)()), ((switchOffPower_arg1)()));}
  };
  if ((switchOffPower_guard)()) {
    {(switchOffPower)(((switchOffPower_arg0)()), ((switchOffPower_arg1)()));}
  };
}

[ivanperez-keera]

Indeed, that is an error in the spec.

At present, we consider it an error whose detection is delegated on the C compiler.

If you consider the process of compilation as indivisible (Haskell -> running -> GCC), then the error is being caught. What happens is that it is not caught in the first stage, it is caught in the third (when you try to compile the C code).

[ivanperez-keera]

I take that back. In principle, it should be an error only if the arguments were different, but not if they are the same.

[ivanperez-keera]

I took a quick stab at this. Avoiding multiple declarations of the handler functions if they have the same arguments is easy to do. Avoiding multiple declarations of the arguments or argument generation functions is a bit trickier.

There are two potentially orthogonal improvements to add to Copilot: 1) avoid multiple declarations of the same generation functions (this connects to #297), and 2) use different names for arguments to the same handling function when they come from different triggers with the same handling function name.

[ivanperez-keera]

I tried this again and I have a crude implementation that seems to work. There's an architecturally cleaner way of structuring the code (that's way I mean by crude).

I don't want to not rush putting this in the Jan 7, 2024 release; I'd rather discuss it well before it's merged.

We'll talk about it next week during our next planning meeting. If we can, we'll add this to Copilot 3.19, to be released on March 7, 2024.

I'll keep you updated.

[ivanperez-keera]

We just had our planning meeting and this issue is likely to be included in the next release. You should see an update on this in a few days.

[ivanperez-keera]

Description

The current implementation of Copilot does not allow using the same trigger handler name multiple times, since the C99 backend produces multiple repeated declarations, which is invalid.

So long as the types do not change, or so long as the target language allows for method/function overloading, then the Copilot spec should accept them.

Type

• Feature: extend valid specifications to allow multiple triggers with the same handler.

Additional context

None.

Requester

• Antanas Kalkauskas (Sensemtry).

Method to check presence of bug

Not applicable (not a bug).

Expected result

Copilot accepts specs where there are two triggers with the same name, so long as the types of the arguments (and their arity) is the same.

Desired result

Copilot accepts specs where there are two triggers with the same name, so long as the types of the arguments (and their arity) is the same.

Proposed solution

Modify copilot-c99 to accept specs with multiple triggers with the same handler name, and either use the same declaration for both (without repeating it), or produce multiple declarations with different names.

Further notes

None.

[fdedden]

Supporting multiple calls to the same trigger has (in my opinion) one major drawback. In Copilot we basically consider triggers to be the output of a program. Having multiple triggers call the same function means that we have a single output referred from multiple places. This can make the code less readable, and is up to the user to structure it a nice way.

On the other hand, I am pretty sure that allowing multiple definitions do not change the semantics of Copilot anyway (under the limitation that we only allow reuse of the trigger with same arity and argument types). For example: (type annotations omitted for brevity)

trigger "f" (a > 1) [arg 123]
trigger "f' (b > 10) [arg 456]

could be written in the current version of Copilot as:

cond0 = a > 1
cond1 = b > 10
guard = cond0 || cond1
argVal = if cond0 then 123 else 456

trigger "f" guard [arg argVal]

Now, I think we can all agree that this approach is much more error-prone, so it might not be a bad idea to support multiple triggers.

I think it is very reasonable to only support multiple triggers if the arity and argument types match exactly. C for example disallows / does not support overloading functions (for good reason, in my opinion). If we disallow it, I think it would be nice to have Copilot check this, instead of relying on the backend to do this. We can make our error message a lot more informative, especially because I expect it is fairly easy for the user to make a mistake/typo where the types do not match.

[ivanperez-keera]

Agreed. I think we can proceed with this.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 4.2.

Fix assigned to: @fdedden .

[fdedden]

Implementor: Solution implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:
  • The code proposed compiles and passes all tests. Details:
    Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/273723103
  • The solution proposed produces the expected result. Details:
    The following dockerfile checks that a spec with the same trigger name used multiple times can be compiled correctly, and the resulting C code also compiles, after which it prints the message "Success":

    --- Dockerfile-verify-296
    FROM ubuntu:trusty
    
    RUN apt-get update
    
    RUN apt-get install --yes software-properties-common
    RUN add-apt-repository ppa:hvr/ghc
    RUN apt-get update
    
    RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4
    RUN apt-get install --yes libz-dev
    
    ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH
    
    RUN cabal update
    RUN cabal v1-sandbox init
    RUN cabal v1-install alex happy
    RUN apt-get install --yes git
    
    ADD MultipleTriggers.hs /tmp/MultipleTriggers.hs
    
    SHELL ["/bin/bash", "-c"]
    CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
      && cabal v1-install $NAME/copilot**/ \
      && cabal v1-exec -- runhaskell /tmp/MultipleTriggers.hs \
      && gcc -c triggers.c \
      && echo "Success"
    
    --- MultipleTriggers.hs
    import Language.Copilot
    import Copilot.Compile.C99
    
    import Prelude hiding ((>), (<), div)
    
    -- External temperature as a byte, range of -50C to 100C
    temp :: Stream Word8
    temp = extern "temperature" Nothing
    
    spec = do
      -- Triggers that fire when the temp is too low or too high, pass the current
      -- temp as an argument.
      trigger "adjust" (temp < 18) [arg temp]
      trigger "adjust" (temp > 21) [arg temp]
    
    -- Compile the spec
    main = reify spec >>= compile "triggers"
    

    Command (substitute variables based on new path after merge):

    $ docker run -e "REPO=https://github.com/fdedden/copilot" -e "NAME=copilot" -e "COMMIT=1d389490d6e1017932679bb7a639dd9856bd04f8" -it copilot-verify-296
    

• Implementation is documented. Details:
  All new top-level definitions have haddock comments, and any sizeable new local definitions or substantial changes have associated comments.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  No updates needed.
• Required version bumps are evaluated. Details:
  Bump not needed; API remains backwards compatible.

[ivanperez-keera]

Change Manager: Implementation ready to be merged.