Strings with zeros inside are inconsistent between refc and other backends

[buzden]

Steps to Reproduce

Consider the following program

main : IO ()
main = do
  printLn $ String.length "ab"
  printLn $ String.length "a\0b"

and run is with different backends:

$ IDRIS2_CG=chez idris2 --exec main Main.idr
$ IDRIS2_CG=racket idris2 --exec main Main.idr
$ IDRIS2_CG=refc idris2 --exec main Main.idr
$ IDRIS2_CG=node idris2 --exec main Main.idr

Expected Behavior

All backends would give a consistent output, presumably

2
3

Observed Behavior

chez, racket and node give

2
3

and refc gives

2
1

[andrevidela]

oh boy I was waiting for this to happen, exciting

[seagull-kamome]

I have started experimenting with having the length information in the Value_String. The code can be found at https://github.com/seagull-kamome/Idris2/tree/issue3161.

I couldn't figure out a good way to preserve information such as length and memory ownership in FFI, so I used ugly method to handle fastPack, fastUnpack and fastConcat. At least, it seems to work as well, but I have no clue this method is always safe at all backends.
If we want to hide Value_String from the eyes of the C library and keep compatibility, we will need some way to switch the calling convention.