stan-dev / stanc3

The Stan transpiler (from Stan to C++ and beyond).
BSD 3-Clause "New" or "Revised" License
138 stars 44 forks source link

Fix: Optimizations crash on mod 0 partial evaluation #1351

Closed WardBrian closed 10 months ago

WardBrian commented 10 months ago

Crash found by fuzzing

Submission Checklist

Release notes

Fixed an issue with the partial evaluator crashing on statements containing a mod-by-zero.

Copyright and Licensing

By submitting this pull request, the copyright holder is agreeing to license the submitted work under the BSD 3-clause license (https://opensource.org/licenses/BSD-3-Clause)

codecov[bot] commented 10 months ago

Codecov Report

Merging #1351 (743d0dd) into master (d5c25b6) will increase coverage by 0.02%. The diff coverage is 100.00%.

@@            Coverage Diff             @@
##           master    #1351      +/-   ##
==========================================
+ Coverage   89.36%   89.39%   +0.02%     
==========================================
  Files          65       65              
  Lines       10609    10607       -2     
==========================================
+ Hits         9481     9482       +1     
+ Misses       1128     1125       -3     
Files Changed Coverage Δ
src/analysis_and_optimization/Partial_evaluator.ml 89.63% <100.00%> (+0.24%) :arrow_up:
src/stanc/stanc.ml 81.88% <100.00%> (-0.26%) :arrow_down:

... and 2 files with indirect coverage changes

WardBrian commented 10 months ago

64-bit ints

63, actually (one of OCaml's weirder defaults).

But yes, sounds like it could be an issue. Can you write down a model that experiences that problem?

nhuurre commented 10 months ago

Can you write down a model that experiences that problem?

model {
  array[1] int T = {1000000000 * 1000000000};
  print(T);
}

Compile with stanc --O1 and clang++ stops at

error: constant expression evaluates to 1000000000000000000 which cannot be narrowed to type 'int'
WardBrian commented 10 months ago

That actually seems like it is catching what would be a runtime error at compile time, (with a pretty clear error message, on gcc as well) so I guess it's not the end of the world?

If you compile without optimizations GCC actually warns you anyway:

../../ml/stanc3/big.hpp:101:59: warning: integer overflow in expression of type ‘int’ results in ‘-1486618624’ [-Woverflow]
  101 |       stan::model::assign(T, std::vector<int>{(1000000000 * 1000000000)},
nhuurre commented 10 months ago

Yes, overflows are always runtime errors, just like divide-by-zero. (The partial evaluator does some "runtime work" at compile time so runtime undefined behavior can turn into a compile-time crash.) We should try and catch them in stanc3 and not the C++ compiler.