Реализация getenv () в ATS - PullRequest
Новая
       14

Реализация getenv () в ATS

0 голосов
/ 24 мая 2018

В (по крайней мере) Linux argv и envp имеют один и тот же тип: они являются указателями на массив указателей с NULL-окончанием на строки, заканчивающиеся NUL, и их хранилище сохраняется в течение всего времени жизни процесса,без необходимости управлять этим.Строки envp имеют форму "KEY = VALUE", поэтому getenv("KEY") может перебирать строки envp, сравнивать их начальные байты с "KEY", а затем возвращать указатель на строку, начинающуюся после'=', когда найден.

Итак, поиск может вообще не включать выделение памяти, но поиск выполняется медленнее, чем при хеш-таблице.

Когда вы получаете 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.

Примечание: с чисто практической точки зрения использование собственного getenv () в C легкодостаточно из кода 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`;Я не хочу отказываться от преимущества ОВД, связанного с безопасным доступом к памяти, даже с указателями.

Ответы [ 2 ]

0 голосов
/ 26 мая 2018

Немного сложно использовать parray_v для реализации getenv.Вот оно:

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

0 голосов
/ 24 мая 2018

Это решение, которое работает с абстрактным типом envp.Это все еще дешево.То, что я ищу, больше похоже на версию, которая сохраняет envp с ее исходным типом ptr, которая имеет те же функции, но которая ограничивает функции только envp -подобными ptr s посредством доказательствасистема.Вместо того, чтобы начинать с $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
$
...