CODEWITHSUNDEEP
ats
Julian Fondren
Julian Fondren

Reputation: 5619

Implementing getenv() in ATS

In (at least) Linux, argv and envp have the same type: they are pointers to a NULL-terminated array of pointers to NUL-terminated strings, and their storage persists for the lifetime of the process, with no need to manage it. envp's strings are of the form "KEY=VALUE", so getenv("KEY") can iterate over envp's strings, compare their leading bytes against "KEY", and then return a pointer to the string starting after the '=', when found.

So, lookup can involve no memory allocation at all, but lookup is slower than what you'd get with a hash table.

When you're given an envp, the OS guarantees validity of the type, but it says nothing about how big the array is.

I'd like to write a getenv() that works with this type as it's really laid out in memory, and I'd like to return pointers into its strings, with minimal allocation.

I'd expect something like this to work:

fun getenv_from(key: string, env: magic): [b:bool] option_vt(string, b) =
    if string2ptr(ptr[0]) > the_null_pointer then (
            case+ string_is_prefix(string_append(key, "="), env[0]) of
            | true => Some_vt(string_make_suffix(env[0], string_length(key)+1))
            | false => getenv_from(key, succ(env))
    ) else None_vt()

where magic should just be envp's ptr plus, I guess, some praxi proof assertions that tell ATS what I've told you about this type.

I've come up with one workaround, which is to pretend that envp really does have argv's type:

#include "share/atspre_staload.hats"

extern fun fake_free{n:int}: argv(n) -> void = "mac#"

%{
void fake_free(void *arg) {}
%}

// print out the first environment variable, as an example
implement main{n:int}(argc, argv, envp) =
    let
        val env2 = $UNSAFE.castvwtp1{argv(n)}(envp)
    in
        if argc > 0 then
            print_string(env2[0]);
        print_newline();
        fake_free(env2);
        0
    end

This works, but now you also have to defeat false constraints involving argc (which has nothing in reality to do with envp), as well as deal with the linear typing, which is unnecessary.

Looking around ATS's library, I think parray_v might be useful, but there are no example uses of parray_v anywhere that I've found.

Note: as a purely practical matter, using C's own getenv() is easy enough from ATS code, as is using the various getenv_gc, getenv_opt, getenv_exn' in ATS's own libraries. So the problem is not "how can I get an environment variable in ATS program?", but really "how can I *properly implement getenv()* in ATS". I'm given a bare pointer. How do I tell ATS about its properties, so that I can work with it in a legal manner? I also don't want to write C-in-ATS with$UNSAFE.ptr_xxx` calls; I don't want to throw away the ATS advantage of provably safe memory access even with raw pointers.

Upvotes: 1

Views: 97

Answers (2)

cs320 bucas
cs320 bucas

Reputation: 265

It is a bit involved to use parray_v to implement getenv. Here it is:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/TESTATS/getenv.dats

Upvotes: 1

Julian Fondren
Julian Fondren

Reputation: 5619

This is a solution that works with an abstract type envp. This feels cheap, still. What I'm looking for is more like a version that retains envp with its original type of ptr, that has these same functions, but which restricts the functions to only envp-like ptrs via the proof system. Rather than start with $UNSAFE.cast, I imagine starting with a lemma_this_ptr_is_envp.

#include "share/atspre_staload.hats"
#include "share/atspre_staload_libats_ML.hats"

abstype envp = ptr
extern fn envp_get(env: envp):<> string = "mac#"
fn envp_get_at{n:int|n==0}(env: envp, n: int(n)): string = envp_get(env)
extern fn add_envp_int{n:int|n==1}(env: envp, n: int(n)): envp = "mac#"
extern fn string_make_suffix: (string, size_t) -> string = "mac#"
overload [] with envp_get_at
overload + with add_envp_int

%{
char *envp_get(void *s) { return ((char **)s)[0]; }
void *add_envp_int(void *p, int n) { return &(((char **)p)[n]); }
char *string_make_suffix(char *s, int start) { return s+start; }
%}

fun getenv_from(key: string, env: envp): [b:bool] option_vt(string, b) =
    if string2ptr(env[0]) > the_null_ptr then (
        case+ string_is_prefix(string_append(key, "="), env[0]) of
        | true => Some_vt(string_make_suffix(env[0], string_length(key)+1))
        | false => getenv_from(key, env+1)
    ) else None_vt()

implement main{n:int}(argc, argv, envp) =
    let
        val envp = $UNSAFE.cast{envp}(envp)
        val reps =
            case+ getenv_from("reps", envp) of
            | ~Some_vt(r) => g0string2int(r)
            | ~None_vt() => 10
        val msg =
            case+ getenv_from("msg", envp) of
            | ~Some_vt(s) => s
            | ~None_vt() => "Hello."
        fun loop(i: int, s: string): void =
            if i > 0 then (
                println!(s);
                loop(i-1, s)
            )
    in
        loop(reps, msg);
        0
    end

Usage:

$ ./getenv5
Hello.
Hello.
Hello.
Hello.
Hello.
Hello.
Hello.
Hello.
Hello.
Hello.
$ reps=3 msg="oh no" ./getenv5
oh no
oh no
oh no
$

Upvotes: 0

Related Questions