Scale numerator to avoid divide by zero error

[Himeshi]

When executing floating point code by converting them an integer version, divide by zero errors can occur. To avoid this when the --execute-float-as-int scale the numerator by a symbolic value.

[domainexpert]

@Himeshi I would recommend the scaling to be done by changing the source of input program because this is easiest.

There is a problem here that one needs to be careful on the consequence of scaling wrt. the propagation of the numeric value. The value propagates via other arithmetic operations. It is possible, however, to implement scaling generally. This can be done as follows: We let the user mark some input values as scaled. So we have two different sets of variables: scaled and non-scaled. A boolean flag field can be added to Cell class to flag scaled / non-scaled value.

Whenever a non-scaled value A is involved in an addition or subtraction with a scaled value B, say A + B is to be computed, we scale A before adding it to B: The result of course should be flagged as scaled. When in addition or subtraction both arguments A and B are scaled or both are non-scaled, then the result follow the argument's scaledness.

For division A / B: When both A and B are scaled: we first divide B with the scale multiply (unscaling) it and compute A / unscaled(B). The result is scaled. When A is scaled and B is not scaled: The result is A / B, and flagged as scaled. When A is not scaled and B is scaled: The result is scale(A) / unscale(B), and flagged as scaled. When A is not scaled and B is not scaled: The result is scale(A) / B, and flagged as scaled.

For multiplication A * B: We unscale A or B when scaled, perform the multiplication, and the result is unscaled.

[Himeshi]

@domainexpert I believe we only need to avoid the division by zero issue when executing floating point code as integer. Therefore only the numerator in division need to be scaled as the other operations are less likely to produce a zero in this way of execution.

The issue of the scaling value propagating and appearing in expressions can be resolved by equating the scaling value to 1.0 when checking sensitivity by running with concrete values. As mentioned in the meeting it would be better to make our approach automatic.

[domainexpert]

@Himeshi I'm fine with automating the scaling, with some idea, as proposed. Differently to you, I believe scaling automation is not just about avoiding division by zero. For example, we have the following sequence of two division:

a = b / c;
e = d / a;

Here, we want to apply scaling to the first division so that a != 0. In that case, we scale b, say multiply by 1000. So as a result, we have a scaled a. But we have to keep the information that a is scaled, d and e are double scaled, and so on. Why? Because subsequently there could be this operation:

x = a + y;

Adding a scaled value a with an unscaled y is incorrect.

Now, since a is scaled, we also have to scale y to get a scaled x. Or, un-scale a (divide it by 1000) to get an unscaled a before adding y to get an un-scaled x. But the point of what I proposed is to record if a value had been scaled or not, so that we can apply arithmetic operations with the right scaling / un-scaling of the arguments.

[Himeshi]

@domainexpert I agree with this. What I was suggesting was instead of scaling with a constant value, like 1000, scale with a symbolic variable, say scaling_val.

In that case we don't have to explicitly keep track of the variables that are scaled as it will be depicted by their expressions. For an example in the case you have given, if we want to scale so as to avoid a == 0 being true, the expression for a will be

a = b * scaling_val / c;

Therefore when x = a + y; is computed, the expression for a will contain the scaling value variable. Then, when we concretely execute the expressions, we can simply set scaling_val = 1.0.

[domainexpert]

@Himeshi That is a possible approach, but please keep in mind that having too many symbolic objects may slow down things. Please note that the approach you mentioned may symbolicize expressions that were previously concrete.

[Himeshi]

@domainexpert Thanks for pointing the drawbacks! Because we allow it as an option, perhaps we can use it only when needed.

[domainexpert]

@Himeshi You can also do a concrete scaling instead of symbolic, say -scale 1000 which will scale values automatically with scaling factor 1000.

[Himeshi]

Updated PR with changes requested in review.