Custom frac domain breaks use of wildcard

[bobismijnnaam]

In the following program, a wildcard permission is exhaled in both methods. However, one method uses our frac domain to convert the wildcard permission back and forth, which causes an assert to fail. The assert would normally hold if the frac domain was not used, as can be seen in the first method.

domain frac {
  function frac_val(a: frac): Perm
  
  axiom frac_eq {
    (forall a: frac, b: frac :: { frac_val(a),frac_val(b) } (frac_val(a) == frac_val(b)) == (a == b))
  }
  
  axiom frac_bound {
    (forall a: frac :: { frac_val(a) } 0 / 1 < frac_val(a) && frac_val(a) <= 1 / 1)
  }
}

field contrib: Ref

function new_frac(x: Perm): frac
  requires 0 / 1 < x && x <= 1 / 1
  ensures frac_val(result) == x

method ok(diz: Ref, globals: Ref, N: Int)
  requires diz != null
  requires acc(diz.contrib, write)
  requires 0 < N
{
  assert 0 < N ==> acc(diz.contrib, N == 0 ? wildcard : wildcard)
  exhale acc(diz.contrib, wildcard)
  assert acc(diz.contrib, wildcard)
  assert 0 < N ==> acc(diz.contrib, N == 0 ? wildcard : wildcard) // Holds
}

method not_ok(diz: Ref, globals: Ref, N: Int)
  requires diz != null
  requires acc(diz.contrib, write)
  requires 0 < N
{
  assert 0 < N ==> acc(diz.contrib, frac_val((N == 0 ? new_frac(wildcard) : new_frac(wildcard))))
  exhale acc(diz.contrib, wildcard) // Problematic exhale
  assert acc(diz.contrib, wildcard)
  assert 0 < N ==> acc(diz.contrib, frac_val((N == 0 ? new_frac(wildcard) : new_frac(wildcard)))) // Does not hold
}

I would expect this program to pass. Since 0 < N holds, all the permission values should end up being indistinguishable from wildcard, but apparently this is not the case. Am I missing an aspect of the use of frac that causes the second method to break, or is something going wrong in Viper?

[mschwerhoff]

Since wildcard is a special "value" (existentially quantified, and suitably constrained when exhaled), Viper doesn't allow wildcards in complex expression. Unfortunately, Viper currently doesn't reject such unsupported permission expressions, and the back-end behaviour is essentially undefined: Carbon will crash, Silicon will ... do something.

I'll therefore close this issue. However, please file a Silver feature request if you really need more flexibility regarding wildcards.

[bobismijnnaam]

Thank you for the explanation, that makes it clearer for me. Would it be safe to say that any frontends for viper should avoid submitting complex expressions involving wildcards? I.e. that wildcard is only allowed as a singular literal argument for an acc? Because we currently do not check for this.

[mschwerhoff]

Yes, your conclusion is correct. I've just filed a corresponding issue, as a reminder for us to clarify this. Thank you for bringing up the problem.