在ATS中实现getenv()

Question

(至少)在Linux中，argv和envp具有相同的类型:它们是指向指向以NUL结尾的字符串的指针数组的指针，并且它们的存储持续到进程的整个生命周期，不需要管理它。envp的字符串是"KEY=VALUE“形式，因此getenv("KEY")可以迭代envp的字符串，将其前导字节与”键“进行比较，然后在找到'=‘之后返回一个指向字符串的指针。

因此，查找可以完全不涉及内存分配，但是查找要比哈希表要慢。

当您获得一个envp时，操作系统可以保证该类型的有效性，但它并没有说明数组有多大。

我想编写一个getenv()，它与这种类型一起工作，因为它实际上是在内存中布置的，我想以最小的分配将指针返回到它的字符串中。

我希望这样的事情能起作用：

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()

magic应该是envp的ptr +，我想是一些praxi证明断言，这些断言告诉ATS我告诉过你们关于这种类型的东西。

我想出了一个解决办法，那就是假装envp确实有argv的类型：

#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

这是可行的，但现在您还必须克服涉及argc (实际上与envp无关)的错误约束，以及处理线性类型，这是不必要的。

纵观ATS的库，我认为parray_v可能很有用，但在我发现的任何地方都没有使用parray_v的例子。

注意:作为一个纯粹的实际问题，从ATS代码中使用C自己的getenv()是非常容易的，使用各种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`调用也是如此；即使使用原始指针，我也不想放弃使用可以证明安全的内存访问的ATS优势。

Answer 1

使用parray_v实现getenv有点复杂。下面是：

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

Answer 2

这是一种适用于抽象类型envp的解决方案。不过，这感觉很便宜。我所要寻找的更像是一个版本，它保留了envp及其原始类型的ptr，它具有相同的函数，但是它通过验证系统将函数限制为仅限于envp-like ptr。与其从$UNSAFE.cast开始，不如从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

用法：

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