Memory allocation and pointer manipulation

hello,
I want to call the OpenGL ES API now and I am studying the memory
allocation and pointer manipulation with ATS.

As a first test, I have made a simple C lib wich take an unsigned int
buffer and print its content.

my library code :
#include “my_lib.h”
#include <stdio.h>

void display_numbers(unsigned int* array, unsigned int size) {
int i;
if( array != NULL ) {
for(i=0;i<size;i++) {
printf("%i\n", array[i]);
}
}
}

I want to make a test code in ATS that create a buffer and set some
arbitrary values and call my library.

The equivalent C code I want to write in ATS :

#include “my_lib.h”
#include <stdlib.h>

#define LEN 17

int main(int argc, char* argv[]) {
int i;
unsigned int* my_array = (unsigned int*)malloc(LEN*sizeof(unsigned int));
for(i=0;i<LEN;i++) {
my_array[i] = LEN - i;
}

display_numbers(my_array, LEN);//–> from my external lib

free(my_array);
}

First of all, I want to find out how to make this in ATS with malloc_gc
(with pointer conversion and assignement of a pointer)
and then how to create a buffer with array_ptr_alloc (with pointer
assignment and also array [] operator )

I look this
page http://bluishcoder.co.nz/2013/01/25/an-introduction-to-pointers-in-ats.html
but I found that he didn’t use the malloc_gc function nor the array_v
dataview

I tried a lot of different things but did not find how to make it.
I dont call the display function from C library now, just allocate,
initialize and deallocate buffer

Here is a rough draft of what I would like to achieve and some help would
be appreciated

//staload "my_lib.sats"
staload "prelude/DATS/array.dats"
staload “prelude/DATS/pointer.dats”

(*
fn{a:t@ype} init_ptr_buffer{l:agz}{n:int}{m:nat} (pf: ![uint?][m] @ l|p:ptr l
, sz: size_t m) = …
*)

fn{a:t@ype} test_malloc{n:nat} (x: a, sz: size_t n): void = let
val (gc, pf|p) = malloc_gc(sz) // I want to alloc sz*sizeof(uint) bytes
// val () = init_ptr_buffer(pf|p, sz) // I need a conversion from byte
pointer to unsigned int pointer
// val () = subsequent call to display_numbers in my C library…
in
free_gc(gc, pf|p)
end

(*
fn{a:t@ype} init_array_buffer{l:agz}{n:int}{m:nat} (pf: !array_v(a, n, l)|p:ptr l
, sz: size_t m) = let
fun loop (i: int): void =
if (i = 0) then print(i)
else let val () = printf("%i\n", @(i)) in loop(i - 1) end
in
loop(p, sz) // do a countdown along the buffer
end
*)

fn{a:t@ype} test_ptr_alloc{n:nat} (x: a, sz: size_t n): void = let
val (gc, pf | p) = array_ptr_alloc(10)
// val () = init_array_buffer(pf|p, p)
// val () = subsequent call to display_numbers in my C library…
in
array_ptr_free(gc, pf|p)
end

implement main(argc, argv) = let
val () = test_malloc(uint_of 10, size1_of_int1 10)
val () = test_ptr_alloc(uint_of 10, size1_of_int1 10)
in
end

thank you for your help :wink:

In my previously presented code, [display_numbers] should
better be given the following type:

fun{a:t@ype} display_numbers (A: &(@[a][n]), n: int n): void

Doing everything safely in ATS takes a lot of time to learn. So knowing
how to do things unsafely in ATS in a “proper” way is a very useful skill
in practice.

Cheers!

Good for you!

This stuff is a lot of fun, isn’t it :slight_smile:

I was really addicted to this style of programming during the early days of
ATS development
(circa 2004-2005).

While it is laborious to program this way, you do get to know better about
program verification.
That knowledge should serve you very well when you go further.

I present as follows an unsafe way to implement display_numbers in ATS2:

//
extern
fun{a:t0p}
display_numbers (A: ptr, size: int) : void
//
implement{a}
display_numbers (A, asz) = let
//
var A: ptr = A
var i: int = 0
//
in
//
while (i < asz)
{
val () = i := i + 1
val () = print_val ($UN.ptr0_get (A))
val () = print_newline ()
val () = A := ptr_succ
(A)
}
//
end // end of [display_numbers]

I think this style is much better than doing template programming in C via
macros.

Cheers!

I worked through a similar problem recently with a lot of help:

That is ATS2 code. Let me know if you’d like the code in ATS1 - here’s an
earlier version of the ATS1 code that is mostly correct:
https://groups.google.com/d/msg/ats-lang-users/l-otsS1voEs/8632BhKPgLEJ

Sorry I cannot check more at the moment.

At this moment, the kind of programming “philosophy” I have for ATS (more
precisely,
ATS2) is like this:

Say we want to implement some kind of system. We first do it in a
functional style
(or whatever style that is close to the specification of the system). This
implementation
is referred to as a specification-like implementation. The features of ATS2
should allow us
to gradually modify/re-implement the specification-like implementation so
as to make it
an implementation of desired strength. This whole process of development
can stay
entirely within ATS also and be guided by the type system of ATS.

People can do a prototype implementation in Lisp and then a “real” one in
C. But this approach
may introduce too many abrupt changes and thus too many uncertainties.

mm yes I understand one has to experiment in unsafe mode first and then
refine the formal check afterwards because it can take a lot of time

thanks :wink:

Also, it sounds like you may have already read this part of the ATS book,
but in case you haven’t, I found it extremely helpful as well:
http://www.ats-lang.org/DOCUMENT/INTPROGINATS/HTML/x3427.html

I make a suggestion here.

What you asked can certainly be done in ATS. Actually, I have done it so
many times.
However, learning how to do it may not be easy and it can take a very long
time. This
is partly of the reason why ATS has not become a popular language yet :slight_smile:

However, doing it in ATS2 would be significantly easier as you do not have
to do it
from the scratch. For instance, the following ATS2 code does what you want:

(* ****** ****** *)

#define LEN 17

(* ****** ****** *)

implement
main0 () =
{
//
val asz = i2sz(LEN)
//
val A =
arrayptr_make_uninitized (asz)
//
implement
array_initize$init (i, x) = x := LEN-g0u2i(i)
val () = arrayptr_initize (A, asz)
//
val () = $extfcall (void, “display_numbers”, arrayptr2ptr(A), LEN)
//
val () = arrayptr_free (A)
//
} (* end of [main0] *)

It may be actually better than you C code as array initialization uses
pointer arithmetic (instead of array subscripting).

Unfortunately, ATS2 is not yet ready for release. My plan is to release it
some time during the summer. Meanwhile, maybe
you could try to learn the functional programming features of ATS?

If you really want to learn the nuts and bolts of ATS, then please
following the links provided by Brandon.

Cheers,

–Hongwei

I begin to realize one has to understand the whole philosophy of ATS in
order to do system programming in ATS.
Indeed functional features in ATS are far more accessible for new comers.

I will try to keep on working with the links and examples

thanks for your answers :wink:

now I have a version with initialization in my code.
I just post here for example :

staload _(anonymous) = "prelude/DATS/array.dats"
staload _(anonymous) = “prelude/DATS/pointer.dats”

%{^
#include <stdio.h>

#define display_numbers display_inumbers

void display_inumbers(int* array, int size) {
int i;
if( array != NULL ) {
for(i=0;i<size;i++) {
printf("%i\n", array[i]);
}
}
}

void display_fnumbers(float* array, int size) {
int i;
if( array != NULL ) {
for(i=0;i<size;i++) {
printf("%f\n", array[i]);
}
}
}
%}

extern fun display_numbers {l:agz} {n:nat} (pf: !array_v(int, n, l) |
p: ptr l, sz: size_t n): void = “mac#display_numbers”

extern fun display_fnumbers {l:agz} {n:nat} (pf: !array_v(float, n, l) |
p: ptr l, sz: size_t n): void = “mac#display_fnumbers”

extern fun {a:t@ype}
print_numbers {l:agz} {n:nat} (pf: !array_v(a, n, l) |
p: ptr l, sz: size_t n): void

implement print_numbers (pf|p, sz) = display_numbers(pf|p, sz)
implement print_numbers (pf|p, sz) = display_fnumbers(pf|p, sz)

fn{a:t@ype}
test_ptr_init_alloc{n:nat} (sz: size_t n,
clz: (sizeLt n, &(a?) >> a) - void
) = let
val (gc, pf|p) = array_ptr_alloc(sz)

fun
init_loop {i:nat | i <= n} {l:agz} .. (
pf_arr: !array_v (a?, n-i, l) >> array_v (a, n-i, l) | p: ptr l,
clz: (sizeLt n, &(a?) >> a) - void, n: size_t n, i: size_t
i): void =
if i < n then let
prval (pf1_at, pf2_arr) = array_v_uncons (pf_arr)
val () = clz (i, !p)
val () = init_loop (pf2_arr | p + sizeof, clz, n, i+1)
prval () = pf_arr := array_v_cons (pf1_at, pf2_arr)
in end
else let
prval () = array_v_unnil (pf_arr)
prval () = pf_arr := array_v_nil ()
in end

val () = init_loop(pf|p, clz, sz, 0)
val () = print_numbers(pf|p, sz)
in
array_ptr_free(gc, pf|p)
end

implement main(argc, argv) = let
val () = test_ptr_init_alloc(28, lam (i,x) = x := 27 -int_of_size i
)
val () = test_ptr_init_alloc(28, lam (i,x) = x := 27.0f -float_of_size i
)
in
end

thanks everybody for help :wink:

hello, after some struggle and useful help from Chris Double, I finally
have a working example :

staload _(anonymous) = "prelude/DATS/array.dats"
staload _(anonymous) = “prelude/DATS/pointer.dats”

%{^
#include <stdio.h>

void display_numbers(int* array, int size) {
int i;
if( array != NULL ) {
for(i=0;i<size;i++) {
printf("%i\n", array[i]);
}
}
}
%}

extern fun display_numbers {l:agz} {n:nat} (pf: !array_v(int, n, l) |
p: ptr l, sz: size_t n): void = “mac#display_numbers”

fn
test_simple_ptr_alloc (): void = let
val (gc, pf|p) = array_ptr_alloc(2)
val () = array_ptr_initialize_elt(!p, 2, 0) // has to be called to
be proofed as already initialized
val () = p[0] := 0
val () = p[1] := 1
val () = display_numbers(pf|p, 2)
//val () = printf(“first value is %i, and second is %i\n”, @(p[0], p[1]))
in
array_ptr_free(gc, pf|p)
end

fn
test_simple_fun_ptr_alloc{n:nat} (sz: size_t n) = let
val (gc, pf|p) = array_ptr_alloc(sz)
fn setup_f (sz: sizeLt n, x: &(int?) >> int): void = x := int_of_size sz
val () = array_ptr_initialize_fun(!p, sz, setup_f)
val () = display_numbers(pf|p, sz)
//val () = array_ptr_foreach_fun(!p, lam (x) = printf(“hello
world -> %i\n”, @(x)), sz)
in
array_ptr_free(gc, pf|p)
end

implement main(argc, argv) = let
val () = test_simple_ptr_alloc()
val () = test_simple_fun_ptr_alloc(28)
in
end

I still working on figure out how to do the array initialization without
array_ptr_initialize_fun