search

viperproject / silver

Definition of the Viper intermediate verification language.
Mozilla Public License 2.0
78 stars 40 forks source link

Wrong optimization of signed integer divisions #782

Closed fpoli closed 4 months ago

fpoli commented 5 months ago

Jonas made me realize that this optimization (used by Prusti) is wrong when left < 0, because in Viper -3 / 2 == -2 but in Scala (and Rust) -3 / 2 == -1:

https://github.com/viperproject/silver/blob/e376940a5c2808214ca75a7d0c90071f8a331de5/src/main/scala/viper/silver/ast/utility/Simplifier.scala#L119-L120

fpoli commented 5 months ago

(I also wonder why those optimizations are not always used by Viper. Are they slower on average than feeding the unoptimized expressions to Z3? Has anyone ever tried measuring this?)

marcoeilers commented 4 months ago

Silicon and Carbon both perform optimization of expressions, just not on the level of the input Viper program. Silicon does it on the level of its internal Terms, Carbon on the generated Boogie program. At least in Silicon's case, the optimization is definitely worth it. There's just usually no point in doing it on the Viper level in addition to the internal level.