Debugging Copilot specs

[ivanperez-keera]

A common scenario we run into in Copilot is the need to debug a specification. While we can use observer in the interpreter, we cannot do the same in C or bluespec.

To debug in those cases, we end up having to create additional triggers that are just wrappers around printf or similar platform-specific functions.

Prompted by work that @sukhmankkahlon and @kavehz-nasa, as well as other prior discussions, we think we might want to give observer meaning also in C or bluespec. Note that not all platforms will use the same functions for debugging: in some cases you want to use printf, in others OS_print, in others Serial.print, etc. The specific function that would need to be used might change.

Any thoughts on this or how that interface should be designed?

[ivanperez-keera]

Related to a conversation we just had with @RyanGlScott , if we supported string types in Copilot we might be able to just do:

temperature :: Stream Int8
temperature = [0] ++ (temperature * 2)

spec = do
  trigger "printf" true [ arg "Message is %d\n", arg temperature ]

[ivanperez-keera]

Tagging @fdedden for awareness.

[fdedden]

I am all in on this idea; it would really help in certain situations. There are a few things we need to consider though:

• Will they be a fully new type, or do we implement them using Array n Char? I bet that could save us work on the code generation part. For the C code, that should actually work very well I think.
• What kind of string operations do we support? Changing of case, dropping characters, appending strings?
• How about parsing? If we support string, parsing data into a string will be something very useful (it will open up the way to read contents of files for example). We need to be sure that it never fails so we don't brake with causality. Forcing default values would be an option.

Specially for the C99 backend: strings are not proper first class values in the language. As suggested above I think by using the Array n Char approach, I think we can implement it safely and without much effort.

[RyanGlScott]

Will they be a fully new type, or do we implement them using Array n Char? I bet that could save us work on the code generation part. For the C code, that should actually work very well I think.

The story in Bluespec is a little more complicated, where String is a distinct, primitive type. Moreover, Strings cannot be stored in registers, so it's not straightforward to have something of type Stream String.

We might be able to define a printf-like function that accepts an array of characters in Bluespec using the C foreign function interface, however.