Inconsistent behavior of division

[viper-admin]

Created by bitbucket user robinsierra on 2019-11-05 13:29
Last updated on 2020-02-06 13:09

The two backends produce different behavior for division. The following Viper program verifies in Silicon but not in Carbon

‌

method foo(a: Int, b: Int)
  requires a == 12 && b == 5
{
  assert  12 /  5 ==  2
  assert -12 / -5 ==  3  // carbon: -12 / -5 ==  2 works
  
  assert  12 / -5 == -2
  assert -12 /  5 == -3  // carbon: -12 /  5 == -2 works
  
  assert   a / -b == -2
  assert  -a /  b == -3
  
  assert  -a / -b ==  3
}

while the slightly modified version

‌

method foo(a: Int, b: Int)
  requires a == 12 && b == 5
{
  assert  12 /  5 ==  2
  assert -12 / -5 ==  2  // silicon: -12 / -5 ==  3 works
  
  assert  12 / -5 == -2
  assert -12 /  5 == -2  // silicon: -12 /  5 == -3 works
  
  assert   a / -b == -2
  assert  -a /  b == -3
  
  assert  -a / -b ==  3
}

works in Carbon but not Silicon. Carbon is in itself inconsistent though, as -12 / 5 is -2 for literals (evaluated statically?) but -3 for symbolic values.

In general, what kind of integer division does Viper do? If it does floor division (like Python) or truncating divison (like Java and C) both Silicon and Carbon give incorrect results for some negative values, if it just uses z3’s division the problem is only in Carbon.

[viper-admin]

@fabiopakk commented on 2020-02-06 13:09

Perhaps this issue shouldn’t be placed in Silver, but rather one of the two backends. Particularly Carbon seems to be giving the wrong result.

[mschwerhoff]

1. In my impression, the div-mod behaviour implemented by Java, C++ or Rust is more standard than that of Python. Thus, I'd expect the following to pass (comments indicate what Silicon and Carbon currently expect):

// See also https://ideone.com/yE5E4s

method test01() {
  // Integer division and modulo as implemented in Java, C++, Rust
  assert   12 /  5 ==  2
  assert   12 / -5 == -2
  assert  -12 /  5 == -2 // Silicon: -3
  assert  -12 / -5 ==  2 // Silicon:  3

  assert   12 %  5 ==  2
  assert   12 % -5 ==  2
  assert  -12 %  5 == -2 // Silicon:  3
  assert  -12 % -5 == -2 // Silicon:  3
}

method test02(a: Int, b: Int)
  requires a == 12 && b == 5
{
  // Integer division and modulo as implemented in Java, C++, Rust
  assert   a /  b ==  2
  assert   a / -b == -2
  assert  -a /  b == -2 // Silicon: -3, Carbon: -3
  assert  -a / -b ==  2 // Silicon:  3, Carbon:  3

  assert   a %  b ==  2
  assert   a % -b ==  2
  assert  -a %  b == -2 // Silicon:  3, Carbon: 3
  assert  -a % -b == -2 // Silicon:  3, Carbon: 3
}

method test03(a: Int, b: Int)
  requires b != 0
{
  // Div-Mod Identity
  assert ((a / b) * b + a % b) == a
}

2. Carbon's different behaviour regarding test01 vs. test02 could result from performing a constant folding optimisation for the expressions from test01 whose semantics does not match those of the expressions from test02 (or rather, their Boogie translation).

3. AFAIK, SMT leaves the semantics of integer division and modulo underspecified. Silicon translated to SMT right away, without any additional axioms; Carbon translates to Boogie, which might add axioms for integer division and modulo.

4. To accommodate users that, e.g. need Python's div-mod behaviour (operator // in Python3), Viper could implement C++'s behaviour by default, but provide users with a way of specifying their own div-mod axioms (similar to what Silicon allows for set/multiset/seq axioms).

[fpoli]

When fixing this behaviour, please consider also Simplifier.scala and SimplifierTests.scala. I'm not sure whether Silicon or Carbon actually use this simplifier, but for sure in Prusti we do.

[mschwerhoff]

Additional information:

• According to SMT-LIB's integer theory, it defines division and modulo according to Boute's Euclidean definition.
• Boogie (at least by default) also directly encodes div and mod to Z3, so Carbon and Silicon ultimately use the same definition

The root problem thus is Viper's own simplifier, whose constant folding uses Scala's semantics for div and mod, not SMT-LIB's.

[mschwerhoff]

Decisions taken during the Viper meeting on 22nd April 2021:

1. Viper will have fixed semantics of division and modulo. If front-ends need custom semantics, they'll have to axiomatise it.
2. Viper will implement the semantics used by major programming languages such as Java, C++ and Rust

Side remark: Vyper apparently already has code for generating the necessary SMT encoding, which we can probably reuse.

[fpoli]

Currently in Prusti we encode Rust's left % right to Z3's (left >= 0 || left % right == 0) ? (left % right) : (left % right - abs(right)). I'm curious to see if this is the same that Vyper does.

[jcp19]

This problem also came up in Gobra recently (viperproject/gobra#858).

[fabiopakk]

In time, I believe it would be beneficial to have a test framework that compares if the result of verification are the same between Silicon and Carbon (if they agree, in other words). It could be on the evaluation of expressions (values) or in any other granularity that makes sense.

It can prevent an expression from being evaluated to different values, depending on the backend, but still be part of an assertion that accidentally accepts both of them (rendering the difference imperceptible).