在 ATS 中实现 getenv()

Question

在（至少）Linux 中，argv 和 envp 具有相同的类型：它们是指向以 NULL 结尾的字符串的指针的 NULL 结尾数组的指针，并且它们的存储在进程的整个生命周期内持续存在，无需管理。 envp 的字符串的形式为 "KEY=VALUE"，因此 getenv("KEY") 可以在找到时遍历 envp's strings, compare their leading bytes against "KEY", and then return a pointer to the string starting after the '='。

因此，查找可以根本不涉及内存分配，但查找比使用散列 table.

得到的慢

当你得到一个 envp 时，OS 保证类型的有效性，但它没有说明数组有多大。

我想编写一个与此类型一起工作的 getenv()，因为它确实位于内存中，并且我想 return 指向其字符串的指针，分配最少。

我希望这样的东西能起作用：

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 的示例。

注意：作为一个纯粹的实际问题，使用 C 自己的 getenv() 在 ATS 代码中很容易，就像使用各种 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

这是一个适用于抽象类型的解决方案 envp。这仍然感觉很便宜。我正在寻找的更像是一个保留 envp 及其原始类型 ptr 的版本，它具有这些相同的功能，但将功能限制为仅 envp-like ptrs 通过证明系统。与其以 $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
$

Answer 2

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

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

在 ATS 中实现 getenv()

Implementing getenv() in ATS

ats