How to assign a `shared` value onto a member of vtype?

[Kiwamu Okabe]

Dear all,

There is a security issue on FreeBSD:

* Security Advisory:
https://www.freebsd.org/security/advisories/FreeBSD-SA-20:20.ipv6.asc
* The patch: https://github.com/freebsd/freebsd/commit/5707de0ed806712f53752acd433313a39f63f15c

I'm writing following ATS code to try to avoid the issue:

https://github.com/metasepi/postmortem/blob/master/Security-Advisory/FreeBSD-kernel/FreeBSD-SA-20:20.ipv6/Resolution/ATS2/error/main.dats

But the code causes following error:

```
$ patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC main.dats -lpthread
.../FreeBSD-SA-20:20.ipv6/Resolution/ATS2/error/main.dats:
2574(line=98, offs=22) -- 2764(line=105, offs=6):
error(3): the linear dynamic variable [opts$view$5659(-1)] is
preserved but with an incompatible type.
```

How to assign a `shared` value onto a member of vtype?

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[Dambaev Alexander]

hi, just a quick answer on the go:

you need to use shared_unref, which will gave you view of type option_v( a@l), and when c <= 1, you will be able to use opt_unsome

сб, 29 авг. 2020 г. в 08:31, Kiwamu Okabe <kiw...@debian.or.jp>:

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DDxDQ4hNty%3DXA6t12Ge2LDuMQpv7C_wRLNsXUY_-t78w%40mail.gmail.com.

[Dambaev Alexander]

or maybe I misunderstood your question? I had unanswered how to restore type of opts to solve compiler error.

сб, 29 авг. 2020 г. в 08:40, Dambaev Alexander <ice.r...@gmail.com>:

[Hongwei Xi]

In the following code, the proof of the view associated with opts is

stored in inp.sh. This proof needs to be taken out and put back into view@opts

before the function main0 can exit.

implement main0 () = let

    var opts: ip6_pktopts
    var inp: inpcb
    val () = inp.in6p_outputopts := addr@opts
    val () = inp.sh := shared_make(view@opts | addr@opts)
  in
    ignoret(usleep(1000u))
  end

[Kiwamu Okabe]

Dear Dambaev,
thank you for your reply.

On Sat, Aug 29, 2020 at 5:40 PM Dambaev Alexander <ice.r...@gmail.com> wrote:
> you need to use shared_unref, which will gave you view of type option_v( a@l), and
> when c <= 1, you will be able to use opt_unsome

Umm... My question is about `main0` function:

```ats

implement main0 () = let
var opts: ip6_pktopts
var inp: inpcb
val () = inp.in6p_outputopts := addr@opts

val () = inp.sh := shared_make(view@opts | addr@opts) // <= error at here
in
ignoret(usleep(1000u))
end
```

My `shared_unref` may have some issue, which is mentioned by you.
But I think I define it but don't use it, because the function ends
with `ignoret`.

[Kiwamu Okabe]

Dear Hongwei,

thank you for your reply.

On Sat, Aug 29, 2020 at 11:05 PM Hongwei Xi <gmh...@gmail.com> wrote:
> In the following code, the proof of the view associated with opts is
> stored in inp.sh. This proof needs to be taken out and put back into view@opts
> before the function main0 can exit.
>
> implement main0 () = let
> var opts: ip6_pktopts
> var inp: inpcb
> val () = inp.in6p_outputopts := addr@opts
> val () = inp.sh := shared_make(view@opts | addr@opts)
> in
> ignoret(usleep(1000u))
> end

So I think I miss-understanded `ignoret`.
Then I tried to use `shared_unref` to return `view@opts`.
But the code causes the other error:

https://github.com/metasepi/postmortem/commit/cb97cf86f5cdb766b7b6123db674f58b95ed793c

```ats

implement main0 () = let
var opts: ip6_pktopts
var inp: inpcb
val () = inp.in6p_outputopts := addr@opts
val () = inp.sh := shared_make(view@opts | addr@opts)

val (pf_oopts | x, count) = shared_unref(inp.sh)
val () = assertloc(count <= 1)
prval Some_v(pf_opts) = pf_oopts
prval () = view@opts := pf_opts
in
ignoret(usleep(1000u))
end
```

```

$ patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC main.dats -lpthread

../main.dats: 2867(line=106, offs=16) -- 2887(line=106, offs=36):
error(3): viewat-restoration cannot be performed: mismatch of bef/aft
locations of atviews:
bef: [S2Evar(opts(8626))]
aft: [S2Evar(l$8797$8799(14588))]
```

Are `view@opts` and return from `shared_unref` not the same?

[Hongwei Xi]

Well, you did not prove that the one returned is the same as the one borrowed :)

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3DGfoVn7yJveTeiKpmOd0Kz%2Bkn_nCHQf3kfQJ-JkRtprw%40mail.gmail.com.

[Kiwamu Okabe]

Dear Hongwei,

On Sun, Aug 30, 2020 at 10:19 AM Hongwei Xi <gmh...@gmail.com> wrote:
> Well, you did not prove that the one returned is the same as the one borrowed :)

Umm... Do you mean following eats original `a@l`:

```ats
extern fun shared_make{a:vt@ype}{l:addr} (a@l | ptr l): shared(a)
```

and the following introduces another one?

```ats
extern fun shared_unref{a:vt@ype} (shared(a)): [l:addr][c:int]
(option_v(a@l, c <= 1) | ptr l, int c)
```

I would like to take more hints.
If I prove they have same `l:addr` in `shared(a:vt@ype)`, ATS2 accepts
them as the same?

```ats
absvtype shared(a:vt@ype) = [l:addr] (a@l | ptr l)
```

[gmhwxi]

shared(a) should be changed to shared(a, l) if you need to make sure that the returned

proof is also of the view a@l (instead of a@l2 for some l2). Otherwise, you may have to

do a bit of casting:

extern
prfun
vborrow
{a:view}(pf: !INV(a)): a

implement main0 () = let
    var opts: ip6_pktopts
    var inp: inpcb

    prval pf = vborrow(view@opts)

    val () = inp.in6p_outputopts := addr@opts

    val () = inp.sh := shared_make(pf | addr@opts)

    val (pf_oopts | x, count) = shared_unref(inp.sh)
    val () = assertloc(count <= 1)
    prval Some_v(pf_opts) = pf_oopts

    prval () = $UN.castview0{void}(pf_opts)
  in
    ignoret(usleep(1000u))
  end

[Dambaev Alexander]

it works when you alias view of opts and proof, that x is the same as addr@opts

```

implement main0 () = let

    var opts: ip6_pktopts with opts_pf
    var inp: inpcb

    val () = inp.in6p_outputopts := addr@opts

    val () = inp.sh := shared_make(opts_pf | addr@opts)

    val (pf_oopts | x, count) = shared_unref(inp.sh)
    val () = assertloc(count <= 1)
    prval Some_v(pf_opts) = pf_oopts

    val () = assertloc( x = addr@opts)
    prval () = opts_pf := pf_opts
  in
    ignoret(usleep(1000u))
  end
```

вс, 30 авг. 2020 г. в 01:44, gmhwxi <gmh...@gmail.com>:

--

You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/a6f5a77c-ea89-43d6-a7b0-4545b1d88c6en%40googlegroups.com.

[Kiwamu Okabe]

On Sun, Aug 30, 2020 at 12:37 PM Dambaev Alexander
<ice.r...@gmail.com> wrote:
> it works when you alias view of opts and proof, that x is the same as addr@opts

Wow... Your patch is too amazing for me...
It also works in my environment.

https://github.com/metasepi/postmortem/commit/366bb929794285c977339c328daa31c278a28645

I don't know the following technique.

```

var opts: ip6_pktopts with opts_pf

// --snip--
val () = assertloc(x = addr@opts)
```

Thank you a lot, Dambaev!

[Dambaev Alexander]

1. the reason why we need to prove, that x = addr@opts is that shared_unref's type says, that it's return type defines some 'l':

```

extern fun shared_unref{a:vt@ype} (shared(a)): [l:addr][c:int] (option_v(a@l, c <= 1) | ptr l, int c)

```

this l can be the same as addr@opts, but can be some other, so we need to check;

2. For now I can only guess why version with view@ didn't work (maybe Hongwei will tell us the actual reason, especially if this is a bug or a feature), but I think it is related to how both views are behave:

when we consume view@opts in make_shared, view@opts is still available at 'main' and we can show it's type with '$showtype', which tells us, that now it is ' without(ip6_pktopt) @ opts'

```

**SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 2970(line=109, offs=26) -- 2979(line=109, offs=35)): S2Eat(S2Ewithout(S2Etyrec(flt0; npf=-1; ip6po_hlim=S2Etop(knd=0; S2Ecst(int)))); S2Evar(opts(8624))): S2RTbas(S2RTBASimp(7; view))

```

but if we will use view alias like this:

```
implement main0 () = let

    var opts: ip6_pktopts with opts_pf

    var inp: inpcb
    val () = inp.in6p_outputopts := addr@opts

    prval _ = $showtype (opts_pf)

    val () = inp.sh := shared_make(opts_pf | addr@opts)
    val (pf_oopts | x, count) = shared_unref(inp.sh)
    val () = assertloc(count <= 1)
    prval Some_v(pf_opts) = pf_oopts
    val () = assertloc( x = addr@opts)

(*    prval _ = $showtype (opts_pf) can't use it here, because opts_pf is no longer available, as it was consumed *)

    prval () = opts_pf := pf_opts (* restore opts_pf *)
    prval _ = $showtype (opts_pf)
  in
    ignoret(usleep(1000u))
  end
```

it will show types:
```

**SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 2733(line=103, offs=26) -- 2740(line=103, offs=33)): S2Eat(S2Etyrec(flt0; npf=-1; ip6po_hlim=S2Etop(knd=0; S2Ecst(int))); S2Evar(opts(8624))): S2RTbas(S2RTBASimp(7; view))
**SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 3021(line=110, offs=26) -- 3028(line=110, offs=33)): S2Eat(S2EVar(5372); S2Evar(l$8793$8795(14582))): S2RTbas(S2RTBASimp(7; view))

```

meaning, that we no longer have a prove of 'ip6_pktopt @ opts', but we have a prove of 'ip6_pktopt @ l', where l is some address, even though we have an assertloc(), that should confirn, that 'l = addr@opts'.

It may be, that for compiler 'opts' is not a pointer, but a variable and that is why we can't prove that l = opts, but in case of using view alias, compiler thinks 'ok, prove with '@opts' has gone now and we got new proof with some 'l', it's type 'a' is the same as type of 'opts', so it is the same size and I can replace consumed view with that one'.

But as I said, this is only a guess

[Dambaev Alexander]

or it may be simpler:

compiler wants to keep 'opts_pf' at the end of the 'main', but it does not care if it is the same as it was before, as we can't use 'opts' anymore, but can use 'x' instead:

```

    val (pf_oopts | x, count) = shared_unref(inp.sh)
    val () = assertloc(count <= 1)
    prval Some_v(pf_opts) = pf_oopts
    val () = assertloc( x = addr@opts)

    prval () = opts_pf := pf_opts

    prval _ = $showtype (opts_pf)

    prval _ = $showtype (opts)
    prval _ = $showtype (x)
```

will say:
```

**SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 2733(line=103, offs=26) -- 2740(line=103, offs=33)): S2Eat(S2Etyrec(flt0; npf=-1; ip6po_hlim=S2Etop(knd=0; S2Ecst(int))); S2Evar(opts(8624))): S2RTbas(S2RTBASimp(7; view))
**SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 3021(line=110, offs=26) -- 3028(line=110, offs=33)): S2Eat(S2EVar(5372); S2Evar(l$8793$8795(14582))): S2RTbas(S2RTBASimp(7; view))

/data/devel/ats2/closure/main.dats: 3055(line=111, offs=26) -- 3059(line=111, offs=30): error(3): dereference cannot be performed: the proof search for view located at [S2Evar(opts(8624))] failed to turn up a result.
**SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 3055(line=111, offs=26) -- 3059(line=111, offs=30)): S2Eerrexp(): S2RTbas(S2RTBASimp(1; t@ype))
**SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 3086(line=112, offs=26) -- 3087(line=112, offs=27)): S2Eapp(S2Ecst(ptr_addr_type); S2Evar(l$8793$8795(14582))): S2RTbas(S2RTBASimp(0; type))

```

so we have satisfied the compiler's constraint of 'view of local variable should be preserved at the end of the function', but we haven't restored the view to the original type, which should be more correct, I think.

[gmhwxi]

You could also do it by using a type-annotation:

implement main0 () = let
    var opts: ip6_pktopts

    var inp: inpcb
    val () = inp.in6p_outputopts := addr@opts

    val () = inp.sh := shared_make(view@opts | addr@opts)

    val (pf_oopts | x, count) = shared_unref(inp.sh)
    val () = assertloc(count <= 1)
    prval Some_v(pf_opts) = pf_oopts

    val () = assertloc(x = addr@opts)
    prval () = view@opts := (pf_opts: (ip6_pktopts?)@opts)
  in
    ignoret(usleep(1000u))
  end

When a proof is assigned to view@opts, the proof is required to be of the view T@opts.

Without the annotation, the proof is of the view T@l for some l. Yes, opts and l are equal

but the type-checker requires that opts and l are syntactically identical in this case.

[Kiwamu Okabe]

Dear Dambaev,

On Sun, Aug 30, 2020 at 2:10 PM Dambaev Alexander <ice.r...@gmail.com> wrote:
> 1. the reason why we need to prove, that x = addr@opts is that shared_unref's type says, that it's return type defines some 'l':
> ```
> extern fun shared_unref{a:vt@ype} (shared(a)): [l:addr][c:int] (option_v(a@l, c <= 1) | ptr l, int c)
> ```
> this l can be the same as addr@opts, but can be some other, so we need to check;

If we can write it as follows, `assertloc(x = addr@opts)` isn't needed?

```ats
absvtype shared{l:addr}(a:vt@ype) = (a@l | ptr l)

```

> 2. For now I can only guess why version with view@ didn't work (maybe Hongwei will tell us the actual reason, especially if this is a bug or a feature), but I think it is related to how both views are behave:

OK. Thank you for your note.

> when we consume view@opts in make_shared, view@opts is still available at 'main' and we can show it's type with '$showtype', which tells us, that now it is ' without(ip6_pktopt) @ opts'
>
> ```
> **SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 2970(line=109, offs=26) -- 2979(line=109, offs=35)): S2Eat(S2Ewithout(S2Etyrec(flt0; npf=-1; ip6po_hlim=S2Etop(knd=0; S2Ecst(int)))); S2Evar(opts(8624))): S2RTbas(S2RTBASimp(7; view))
> ```
>
> but if we will use view alias like this:
> ```
> implement main0 () = let
> var opts: ip6_pktopts with opts_pf
> var inp: inpcb
> val () = inp.in6p_outputopts := addr@opts
> prval _ = $showtype (opts_pf)
> val () = inp.sh := shared_make(opts_pf | addr@opts)
> val (pf_oopts | x, count) = shared_unref(inp.sh)
> val () = assertloc(count <= 1)
> prval Some_v(pf_opts) = pf_oopts
> val () = assertloc( x = addr@opts)
> (* prval _ = $showtype (opts_pf) can't use it here, because opts_pf is no longer available, as it was consumed *)
> prval () = opts_pf := pf_opts (* restore opts_pf *)
> prval _ = $showtype (opts_pf)
> in
> ignoret(usleep(1000u))
> end
> ```
> it will show types:
> ```
> **SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 2733(line=103, offs=26) -- 2740(line=103, offs=33)): S2Eat(S2Etyrec(flt0; npf=-1; ip6po_hlim=S2Etop(knd=0; S2Ecst(int))); S2Evar(opts(8624))): S2RTbas(S2RTBASimp(7; view))
> **SHOWTYPE[UP]**(/data/devel/ats2/closure/main.dats: 3021(line=110, offs=26) -- 3028(line=110, offs=33)): S2Eat(S2EVar(5372); S2Evar(l$8793$8795(14582))): S2RTbas(S2RTBASimp(7; view))
> ```
> meaning, that we no longer have a prove of 'ip6_pktopt @ opts', but we have a prove of 'ip6_pktopt @ l', where l is some address, even though we have an assertloc(), that should confirn, that 'l = addr@opts'.
> It may be, that for compiler 'opts' is not a pointer, but a variable and that is why we can't prove that l = opts, but in case of using view alias, compiler thinks 'ok, prove with '@opts' has gone now and we got new proof with some 'l', it's type 'a' is the same as type of 'opts', so it is the same size and I can replace consumed view with that one'.

Umm... Sorry. I can't understand why the `addr@opts`s are same with
`assertloc()`, on `$showtype` output...
I need to learn more to read ATS2 type messages.

Thank you,

[Kiwamu Okabe]

Dear Dambaev,

Thank you for your easy-to-understand answer.
You answer means:

A. `opts_pf` depends on `S2Evar(l$8793$8795(14582))`
B. `x` also depends on `S2Evar(l$8793$8795(14582))`
C. A and B are made by `assertloc(x = addr@opts)`

Thanks,

[Kiwamu Okabe]

Dear Hongwei,

On Sun, Aug 30, 2020 at 11:04 PM gmhwxi <gmh...@gmail.com> wrote:
> You could also do it by using a type-annotation:

--snip--

> prval () = view@opts := (pf_opts: (ip6_pktopts?)@opts)

Thank you. It's a new usage for me.

[Kiwamu Okabe]

Dear all,

BTW, I found more clear answer.

https://github.com/metasepi/postmortem/commit/24eb7d2f4ffcd72e331622d3cc22224002090cd4

```ats
absvtype shared(a:vt@ype, l:addr) = (a@l | ptr l)

typedef ip6_pktopts = @{ ip6po_hlim = int }

implement main0 () = let
var opts: ip6_pktopts

val sh_inp = shared_make(view@opts | addr@opts)
val (pf_oopts | x, count) = shared_unref(sh_inp)

val () = assertloc(count <= 1)
prval Some_v(pf_opts) = pf_oopts

prval () = view@opts := (pf_opts: (ip6_pktopts?)@opts)

in
ignoret(usleep(1000u))
end
```

It doesn't need `assertloc(x = addr@opts)`, because the `l:addr` is exported on
the `shared` type.
It's my mistake at designing `absvtype shared`.

Best regards,