代码之家 › 专栏 › 技术社区 › Julian Fondren

在ATS中实现getenv()。

ats

1

Julian Fondren · 技术社区 · 7 年前

在(至少)Linux中, argv 和 envp 具有相同的类型:它们是指向以空结尾的指针数组的指针,指向以nul结尾的字符串,并且它们的存储在进程的生命周期内保持不变,不需要管理它。 恩维普 的字符串的格式为“key=value”,因此 getenv("KEY") 可以迭代 恩维普 的字符串,将其前导字节与“key”进行比较,然后在找到“=”后返回指向字符串的指针。

所以,查找可以完全不涉及内存分配,但是查找比使用哈希表要慢。

当你被给予 恩维普 操作系统保证了类型的有效性,但它没有说明数组有多大。

我想编写一个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 应该是 小精灵 的 ptr 另外,我想,一些 praxi 证明断言告诉ATS我告诉你的关于这种类型的事情。

我想出了一个解决办法,那就是假装 小精灵 真的有 阿尔加夫 的类型:

#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 (实际上这与 恩维普 )以及处理线性类型,这是不必要的。

我想,看看ATS的图书馆 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的优点,即使用原始指针也可以保证内存访问的安全性。

2 回复 | 直到 7 年前

1

cs320 bucas 7 年前

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

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

2

0

Julian Fondren 7 年前

这是一个使用抽象类型的解决方案 envp . 这感觉还是很便宜。我要找的更像是一个版本 恩维普 它的原始类型 ptr ,具有相同的函数,但仅限于 恩维普 似 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
$