-
Notifications
You must be signed in to change notification settings - Fork 381
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
RefC Backend + makeString memory problems #2455
Comments
FWIW, I agree the second option looks the most natural. First option might be more flexible, but maybe it could lead to unnecessary complexity in the future? |
I guess the main point that @vfrinken makes is this: the current code is quite substantially broken, so someone does need to go through all the C FFI functions (in this code base, but also in external code bases) one by one and implement whichever solution we choose. So the decision is not really whether to make any breaking changes, but how to make the function-by-function fixes straightforward, possibly by following a simple decision procedure. |
I think (2) describes roughly what the FFI documentation (undoubtedly written mostly or entirely with the Scheme backend in mind) describes currently, if I am understanding correctly. Snippet from the Idris documentation:
|
Yes, @ohad, that is exactly the point I was trying to make. I went through the CFFI functions used in the Idris code itself and made the changes (only the direct call to The Idris documentation is quite clear, but the Idris code itself doesn't follow the guideline. :-( Anyway, I'm going to argue in favor of 1. now, because I like it, too:
I won't have time to code anything in the next few days, maybe even until after the Developer Meeting. If by that time the consensus is on 2. I'm happy to turn my code into a PR. |
This is exactly what's problematic. You can't return char* allocated by another allocator. Maybe the data is on the stack? Maybe the data is in |
I didn't see this until after I filed #2552, but the scheme backends have the same problem. They appear to be leaking a lot of memory (e.g. 100k leaks from |
The way strings are handled as (char *) poses problems. I don't see an easy way out. Here is the deal:
Problem
Value* makeString(char*)
creates a copy of the input (including malloc) to create the string object.fastConcat
also allocate new memory (which is not freed anywhere but should be)idris2_strerror(int)
return a pointer to an error message (which should not/can not be freed)Thus, invoking functions such as
fastPack
, orfastConcat
, but alsoidris2_currentDirectory
leak memory.As an example, I compiled Idris itself with the RefC backend (with minor changes along the way to make it compilable), and started it. Just displaying the REFL and immediately exiting, without any actual computation leaks about 1MB already.
Potential solutions
I can see three different approaches, I don't know which ones are feasible. I probably also miss an obvious solution, though.
1. changing the datatype of String from char* to something like a struct with freeing information
Functions like
fastConcat
would then return a struct with the flag set to 0, somakeString
can free the pointer, whereas other functions may set it to 1.2. Create a convention that all FFI functions that return
char*
have to allocate new memory.This new memory is then consistently freed by
makeString
(resp. the garbage collector whenever the String object goes out of scope).Both of these options might break existing code (resp. FFI calls) that interacts with Idris.
3. Use different primitives in the Idris code to indicate whether or not the char* should be kept or discarded.
This, however, seems to break the code the most. CFTypes would need to distinguish between StringFreeable and StringNonFreeable. Consider:
used in functions such as
fGetLine
:now
prim__readLine
returns a char * (which is then as pointer, not as string) passed toprim__getString
, which converts it into a char* (very nice), but then callsmakeString
which allocates new memory (bad) => memory leak. This would need to change toVery ugly, and maybe not even possible.
Personally, I prefer the second option, but I don't have a strong opinion.There are not (yet) a lot of C libraries that interact with Idris2, and the changes seem minimal.
The text was updated successfully, but these errors were encountered: