[analyzer] Introduce reasoning about symbolic remainder operator

Summary:
New logic tries to narrow possible result values of the remainder operation
based on its operands and their ranges.  It also tries to be conservative
with negative operands because according to the standard the sign of
the result is implementation-defined.

rdar://problem/44978988

Differential Revision: https://reviews.llvm.org/D80117