Am really pleased that you figured it out :)
This is pure C-style of systems programming. While it can be done in ATS,
it is often quite involved. The recvfrom function you implemented actually
shows
that it does not make use of more resources that what is given.
One possibility is to introduce a linear functional API for recvfrom:
absvtype sockaddr
datavtype
recvfrom_vt =
|
recvfrom_fail of ()
|
recvfrom_succ of
{m:nat} (arrpsz(char, m), sockaddr)
fun
ATS_recvfrom
{n:pos}
(sz: size_t(n), flags: int): recvfrom_vt
ATS_recvfrom calls malloc to obtain memory. However, we can differentiate
various malloc calls. For embedded programming, we can implement a malloc
that only allocates from statically allocated memory.
Basically, what I am saying here is that low-level systems programming can
be
done in a linear functional style with customized implementations of
malloc/free.
I feel that we are getting very close to this vision :)
On Sunday, July 12, 2020 at 3:07:16 AM UTC-4, Dambaev Alexander wrote:
>
> And at the end, it turned out, that I am not required to manually write
> those proofs:
>
> ```
> extern
> fn recvfrom
> {l: agz} {n: pos}{addr_sz:pos}
> ( buf_pf: !array_v(char?, l, n) >> recvfrom_v(l,n,m)
> | socket_fd: int
> , buf: ptr l
> , sz: size_t n
> , flags: int
> , src_addr: &sockaddr_struct(addr_sz)? >> opt(sockaddr_struct(addr_sz),
> m > 0 && m <= n) (* technically, recvfrom expects sockaddr, not sockaddr_in
> here *)
> , addr_sz: &(socklen_t addr_sz)
> ): #[m:int | m <= n] ssize_t(m)
> implement recvfrom{l}{n}(buf_pf | socket_fd, buf, sz, flags, src_addr,
> addr_sz) = c_recvfrom( buf_pf| socket_fd, buf, sz, flags, src_addr,
> addr_sz) where {
> (* have to define another wrapper here, as only inside this call
> src_addr has type sockaddr_struct, not 'incompatible' sockaddr_in like in
> caller and produces compiler warning *)
> extern
> fn c_recvfrom
> {l: agz} {n: pos}{addr_sz:pos}{sa_l:addr}
> ( buf_pf: !array_v(char?, l, n) >> recvfrom_v(l,n,m)
> | socket_fd: int
> , buf: ptr l
> , sz: size_t n
> , flags: int
> , src_addr: &sockaddr_struct(addr_sz)? >>
> opt(sockaddr_struct(addr_sz), m > 0 && m <= n)
> , addr_sz: &(socklen_t addr_sz)
> ): #[m:int | m <= n] ssize_t(m) = "mac#recvfrom"
> }
> ```
> and the usage:
>
> ```
> var sin: sockaddr_in_struct?
> var sin_sz: socklen_t(socklen_in) = socklen_in
> extern castfn socklen2int{n:int}(i: socklen_t(n)):
> int(n)
> val () = assert_errmsg(socklen2int(sin_sz) > 0,
> "sin_sz <= 0") (* should be {n:pos} socklen_t(n), to not to prove, that
> sockaddr size > 0 *)
> extern praxi sockaddr_in_trans_nil( pf:
> !sockaddr_in_struct? @ sin >> sockaddr_struct(socklen_in)? @ sin): void
> extern praxi sockaddr_trans_in_nil( pf:
> !sockaddr_struct(socklen_in)? @ sin >> sockaddr_in_struct? @ sin): void
> prval () = sockaddr_in_trans_nil( view@sin)
> val readed = $C.recvfrom( recv_buf_pf | x.fd,
> recv_buf, recv_sz, 0, sin, sin_sz)
> in
> if readed <= 0
> then let
> val _ = $extfcall( int, "sprintf", str_buf,
> "unable to read from socket")
> val () = $Log.log_error( addr@str_buf)
> prval $C.recvfrom_v_fail( recv_buf_pf1) =
> recv_buf_pf
> prval () = recv_buf_pf := recv_buf_pf1
> prval () = opt_unnone( sin)
> prval () = sockaddr_trans_in_nil( view@sin)
> in () end
> else let
> val ureaded = g1int2uint(readed)
> prval $C.recvfrom_v_succ( request_pf, rest_buf_pf)
> = recv_buf_pf
> prval () = opt_unsome(sin) (* sin had been
> initialized *)
>
> (* do useful stuff here *)
> val _ = $extfcall( int, "sprintf", str_buf,
> "readed %li bytes", ureaded)
> val () = $Log.log_info( addr@str_buf)
> val () = handle_client_packet( request_pf | x.fd,
> recv_buf, ureaded, sin, sin_sz)
>
> (* now cleanup buffers and proofs*)
> extern prfun array_v_nil_nz{a:viewt0ype}{n:pos}(
> p: array_v(a,l,n)): array_v(a?,l,n) (* there is no std way to mark
> initialized array as uninitialized *)
> prval request_nil_pf = array_v_nil_nz( request_pf)
> prval () = recv_buf_pf := array_v_unsplit(
> request_nil_pf, rest_buf_pf)
> prval () = sockaddr_trans_in(view@sin)
> in () end
> ```
>
>
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/9ff34ba2-f685-4fa2-af50-b74b74b156c8o%40googlegroups.com.
