The ATS PL System

On Mon, 7 Feb 2011, Guillaume Brunerie wrote:

>>Hi,
>>I need to use the C function mkdtemp which is in stdlib.h.
>>Given that the function is not available in libc/SATS/stdlib.sats, I have
>>added it with this patch:
>> ...
>>

I added mkdtemp and fixed mkstemp (both are declared in 
libc/SATS/stdlib.sats).

>>This seems to work but I have a little problem :
>>The doc of mkdtemp says that "Since it will be modified, [the argument of
>>mkdtemp] must not be a string constant, but should be declared as a
>>character array."
>>And indeed, if I try to apply (in ATS) mkdtemp to a string constant I get a
>>segfault.
>>
>>How can I specify that the argument of mkdtemp have to be modifiable, and
>>how do I create a modifiable string?
>>(for now I'm using   val template = ("/tmp/atsrepl-XXXXXX" : string) + ""
>>but this does not seems to be the right thing to do ^^)

The style may be awkward but it is on the right path :)
Please use strbuf instead of string. See some sample code in the following 
file:

$ATSHOME/doc/EXAMPLE/TEST/libc_stdlib.dats

>>PS: in the type of mkstemp there is a {m,n:nat} which does not seem useful.

Fixed.

Cheers,

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

2011/2/7 Hongwei Xi <hwxi@...>

> On Mon, 7 Feb 2011, Guillaume Brunerie wrote:
>
>>
>
>>This seems to work but I have a little problem :
> >>The doc of mkdtemp says that "Since it will be modified, [the argument of
> >>mkdtemp] must not be a string constant, but should be declared as a
> >>character array."
> >>And indeed, if I try to apply (in ATS) mkdtemp to a string constant I get
> a
> >>segfault.
> >>
> >>How can I specify that the argument of mkdtemp have to be modifiable, and
> >>how do I create a modifiable string?
> >>(for now I'm using   val template = ("/tmp/atsrepl-XXXXXX" : string) + ""
> >>but this does not seems to be the right thing to do ^^)
>
> The style may be awkward but it is on the right path :)
> Please use strbuf instead of string. See some sample code in the following
> file:
>
> $ATSHOME/doc/EXAMPLE/TEST/libc_stdlib.dats
>

Thank you :-)
But I have a few questions, because I don’t really understand how to use
strings in ATS.

1) Could you explain the differences between 'string', 'strbuf', 'strptr' ?
(and 'free_gc_v', etc.)

2) The minimal program using mkdtemp seems to be the following:

staload "libc/SATS/string.sats"
staload "libc/SATS/stdlib.sats"
implement main () =
  let
    val tmp = strdup_gc "foo-XXXXXX"
    prval pfstr = tmp.1          // ***
    val _ = mkdtemp !(tmp.2)
    val _ = tmp.1 := pfstr      // ***
    val _ = strbufptr_free tmp
  in () end

But I don’t understand the two lines marked with ***. The first one seems to
be there in order to tell !() that there is something behind the pointer
tmp.2 (but I don’t know why the compiler could not find that by itself), and
I have absolutely no idea for the second line.

3) Why does the return type of mkdtemp is only 'ptr' ? In the example of
mkdtemp you gave, you are using a function from prelude/SATS/unsafe.sats
which does not seems very good (and I don’t want to use such functions). Why
not having a type which says that the return value is either the null
pointer or the same pointer as the argument?


Guillaume

On Tue, 8 Feb 2011, Guillaume Brunerie wrote:

>>But I have a few questions, because I don't really understand how to use
>>strings in ATS.
>>
>>1) Could you explain the differences between 'string', 'strbuf', 'strptr' ?
>>(and 'free_gc_v', etc.)

a string is non-linear; it can only be free by GC
a strbuf is like a flat array of bytes, where the last one is null.
strptr is a linear string, which can be manually freed.

>>2) The minimal program using mkdtemp seems to be the following:
>>
>>staload "libc/SATS/string.sats"
>>staload "libc/SATS/stdlib.sats"
>>implement main () =
>>  let
>>    val tmp = strdup_gc "foo-XXXXXX"
>>    prval pfstr = tmp.1          // ***
>>    val _ = mkdtemp !(tmp.2)
>>    val _ = tmp.1 := pfstr      // ***
>>    val _ = strbufptr_free tmp
>>  in () end
>>
>>But I don't understand the two lines marked with ***. The first one seems to
>>be there in order to tell !() that there is something behind the pointer
>>tmp.2 (but I don't know why the compiler could not find that by itself), and
>>I have absolutely no idea for the second line.

Your guess is right. The compiler does not search inside a tuple to see if 
a particular proof is available. After a proof is taken out of a tuple, it
usually needs to be put back as is done in the following line:

>>    val _ = tmp.1 := pfstr      // ***

>>3) Why does the return type of mkdtemp is only 'ptr' ?

I was kind of lazy. I now fixed it according to the specification.

>>In the example of
>>mkdtemp you gave, you are using a function from prelude/SATS/unsafe.sats
>>which does not seems very good (and I don't want to use such functions). Why
>>not having a type which says that the return value is either the null
>>pointer or the same pointer as the argument?

I did it in the fixed version. However, the unsafe cast was used for 
a different purpose. Say that you want to call rmdir, which is given
the following type:

fun rmdir (path: string): int(*error code*)

Now suppose that you have a linear string  or strbuf as your path.
You cannot pass it to rmdir directly. Of course, rmdir can be given
a type that accepts linear string in the first place but then you can no 
longer call rmdir on a constant string. In the past, I did something like 
this:

fun rmdir_string ...
fun rmdir_strptr
fun rmdir_strbuf

overload rmdir with rmdir_string
overload rmdir with rmdir_strptr
overload rmdir with rmdir_strbuf

This style was so awkward that I now prefer casting over it.

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

2011/2/8 Hongwei Xi <hwxi@...>

> On Tue, 8 Feb 2011, Guillaume Brunerie wrote:
>
> >>But I have a few questions, because I don't really understand how to use
> >>strings in ATS.
> >>
> >>1) Could you explain the differences between 'string', 'strbuf', 'strptr'
> ?
> >>(and 'free_gc_v', etc.)
>
> a string is non-linear; it can only be free by GC
> a strbuf is like a flat array of bytes, where the last one is null.
> strptr is a linear string, which can be manually freed.
>

Thank you, but perhaps you mean that a strptr *must* be freed? Because I
guess that the linear typing will not allow a memory leak here.

>>In the example of
>
>>mkdtemp you gave, you are using a function from prelude/SATS/unsafe.sats
>
>>which does not seems very good (and I don't want to use such functions).
> Why
>
>>not having a type which says that the return value is either the null

>>pointer or the same pointer as the argument?
>
I did it in the fixed version. However, the unsafe cast was used for
> a different purpose. Say that you want to call rmdir, which is given
> the following type:
>
> fun rmdir (path: string): int(*error code*)
>
> Now suppose that you have a linear string  or strbuf as your path.
> You cannot pass it to rmdir directly. Of course, rmdir can be given
> a type that accepts linear string in the first place but then you can no
> longer call rmdir on a constant string. In the past, I did something like
> this:
>
> fun rmdir_string ...
> fun rmdir_strptr
> fun rmdir_strbuf
>
> overload rmdir with rmdir_string
> overload rmdir with rmdir_strptr
> overload rmdir with rmdir_strbuf
>
> This style was so awkward that I now prefer casting over it.
>

But you could use string_of_strbuf or string_of_strptr, why do you need to
cast with such unsafe functions?


Guillaume

On Wed, 9 Feb 2011, Guillaume Brunerie wrote:

>>But you could use string_of_strbuf or string_of_strptr, why do you need to
>>cast with such unsafe functions?

string_of_strptr turns a strptr into a string, which can only be reclaimed
by the GC. If no GC is running, then it is a memory leak.

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

2011/2/9 Hongwei Xi <hwxi@...>

> On Wed, 9 Feb 2011, Guillaume Brunerie wrote:
>
> >>But you could use string_of_strbuf or string_of_strptr, why do you need
> to
> >>cast with such unsafe functions?
>
> string_of_strptr turns a strptr into a string, which can only be reclaimed
> by the GC. If no GC is running, then it is a memory leak.


So there is no clean solution?
It seems that the problem comes from the fact that a constant string is
given the type 'string' even if it will not be freed by the GC (because it’s
a constant string in the data segment), and that constant strings are used
even in a program without GC.
Perhaps that there should be a special type for constant strings?

Guillaume

2011/2/12, Guillaume Brunerie <guillaume.brunerie@...>:
> 2011/2/9 Hongwei Xi <hwxi@...>
>
>> On Wed, 9 Feb 2011, Guillaume Brunerie wrote:
>>
>> >>But you could use string_of_strbuf or string_of_strptr, why do you need
>> to
>> >>cast with such unsafe functions?
>>
>> string_of_strptr turns a strptr into a string, which can only be reclaimed
>> by the GC. If no GC is running, then it is a memory leak.
>
>
> So there is no clean solution?
> It seems that the problem comes from the fact that a constant string is
> given the type 'string' even if it will not be freed by the GC (because it’s
> a constant string in the data segment), and that constant strings are used
> even in a program without GC.

This is a bit confusing. When I needed a mutable string, I've allocated a buffer
on stack, then created a string buffer from it, worked on that (or casted
it to a strptr IIRC), and when I was done, I casted the string buffer back
to the buffer so as to show the typechecker there was no memory leak.
I think that is correct, isn't it?

> Perhaps that there should be a special type for constant strings?

>
> Guillaume
>


-- 
Cheers,
Artyom Shalkhakov

On Fri, 11 Feb 2011, Guillaume Brunerie wrote:

>>2011/2/9 Hongwei Xi <hwxi@...>
>>
>>> On Wed, 9 Feb 2011, Guillaume Brunerie wrote:
>>>
>>> >>But you could use string_of_strbuf or string_of_strptr, why do you need
>>> to
>>> >>cast with such unsafe functions?
>>>
>>> string_of_strptr turns a strptr into a string, which can only be reclaimed
>>> by the GC. If no GC is running, then it is a memory leak.
>>
>>
>>So there is no clean solution?
>>
>>It seems that the problem comes from the fact that a constant string is
>>given the type 'string' even if it will not be freed by the GC (because it's
>>a constant string in the data segment), and that constant strings are used
>>even in a program without GC.
>>Perhaps that there should be a special type for constant strings?

The problem I was trying to elaborate can be described as follows.

Say that you have given the following interface for rmdir:

fun rmdir (path: string): int

Then you cannot pass  the linear string (strptr) to rmdir. A better 
interface for rmdir is the following one:

fun rmdir {l:agz} (path: !strptr l): int

This time, a linear string can be handled but a nonlinear string cannot be
passed directly. One may introduce the following function for handling the
issue:

fun string_takeout_ptr
  (x: string): [l:agz] (strptr l -<lin,prf> void | strptr l)

Here is the kind of code one may write

val (fpf_x | x) = string_takeout_ptr ("foo")
val err = rmdir (x)
prval () = fpf_x (x)

However, this strategy is not without flaw as one may do something like 
this:

val (fpf_x | x) = string_takeout_ptr ("foo")
val () = // segfaults by modifying the string via the pointer x
prval () = fpf_x (x)

Here is another interface for rmdir:

fun rmdir {l:agz} (path: !READ(strptr l)): int

where READ means read-only data. This may do better but it is also more
involved. So the story goes on.

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)

On Sat, 12 Feb 2011, Artyom Shalkhakov wrote:

>>2011/2/12, Guillaume Brunerie <guillaume.brunerie@...>:
>>> 2011/2/9 Hongwei Xi <hwxi@...>
>>>
>>>> On Wed, 9 Feb 2011, Guillaume Brunerie wrote:
>>>>
>>>> >>But you could use string_of_strbuf or string_of_strptr, why do you need
>>>> to
>>>> >>cast with such unsafe functions?
>>>>
>>>> string_of_strptr turns a strptr into a string, which can only be reclaimed
>>>> by the GC. If no GC is running, then it is a memory leak.
>>>
>>>
>>> So there is no clean solution?
>>> It seems that the problem comes from the fact that a constant string is
>>> given the type 'string' even if it will not be freed by the GC (because it's
>>> a constant string in the data segment), and that constant strings are used
>>> even in a program without GC.
>>
>>This is a bit confusing. When I needed a mutable string, I've allocated a buffer
>>on stack, then created a string buffer from it, worked on that (or casted
>>it to a strptr IIRC), and when I was done, I casted the string buffer back
>>to the buffer so as to show the typechecker there was no memory leak.
>>I think that is correct, isn't it?

That is how I typically do it, too.

This kind of casting and  casting back  is certainly boring and it would 
be really nice if there is  a way that  this can be done automatically 
(something like tactics in theorem-proving).

However, I am not advocating that tactics be supported in ATS directly.
That would likely lead to a mess. Instead, such support can be made 
available in some kind of IDE for ATS. It is a new kind of IDE; it is
a kind that goes beyond coloring, highlighting and auto-completion.

--Hongwei

Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215

Email: hwxi@...
Url: http://www.cs.bu.edu/~hwxi
Tel: +1 617 358 2511 (office)
Fax: +1 617 353 6457 (department)