Simple implementation of ifptr via lexer/parser modification

[aigarashi]

In this PR,

ifptr p = q then e1 else e2

gets expanded to

if _ then { alias(p=q); e1} else e2

in the parser.

We wanted a way to check whether two pointers are pointing to the same address so we added this syntax.
The drawback to this approach is that the solver doesn't have access to information such that alias(p != q) holds in e2.

I'm currently trying to see if I can get that information into the solver.

---

sp4ghet wrote:

In cases like the one below:

{
    let x = _ in
    let p = mkref x in
    let q = mkref x in
    ifptr p = q then {
        assert(*p = *q)
    } else ()
}

It gets converted into

let x = _ in
let p = mkref x in
let q = mkref x in {
  if _ then {
    alias(p = q);
    assert(*p = *q);
  } else ()
}

This results in an ownership error which should be quite obvious if written explicitly, but it is feasible for programmers to write code the like the one above using the syntax sugar we are trying to provide

---

naokikob wrote:

Hi, I am not sure what you mean by "This results in an ownership error". Could you please elaborate on what is the problem?

---

sp4ghet wrote:

As in the output is "UNVERIFIED (ownership)"

My understanding is that since p and q are both created as refs, the total ownership between the two of them is 2.
alias(p=q) makes the total ownership 1 since alias means that one pointer is an alias for another, which doesn't add up and causes ConSORT to raise the error.

---

naokikob wrote:

I don't quite remember what constraint is generated by alias(p=q), but how about just generating the constraint
o'_p + o'_q <= o_p + o_q
where o_p and o_p' are the ownerships of p before/after the statement, instead of requiring also that o'_p+o'_q<=1.
It just allows reshuffling of the ownerships.

---

aigarashi wrote:

The reason why o'_p+o'_q<=1 and o_p + o_q <= 1 are generated is that every ownership is in [0,1]. (For example 1+1 is undefined.) We may be able to allow the sum of two ownerships to exceed 1 only for alias without breaking the theory, though.