Skip to content

Commit 7964176

Browse files
lucaneglucaneg
committed
Semantics for modulo and remainder #216 
1 parent ea8f25e commit 7964176

File tree

13 files changed

+104
-21
lines changed

13 files changed

+104
-21
lines changed

‎lisa/lisa-core/imp-testcases/type-inference/untyped_typing.test5(typing__this,_untyped_i).json‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
{"name":"untyped typing::test5(typing* this, untyped i)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = 0"},{"id":1,"text":"x"},{"id":2,"text":"0"},{"id":3,"subNodes":[4,5],"text":">(i, 5)"},{"id":4,"text":"i"},{"id":5,"text":"5"},{"id":6,"subNodes":[7,10],"text":"==(%(i, 2), 0)"},{"id":7,"subNodes":[8,9],"text":"%(i, 2)"},{"id":8,"text":"i"},{"id":9,"text":"2"},{"id":10,"text":"0"},{"id":11,"subNodes":[12,13],"text":"x = \"s\""},{"id":12,"text":"x"},{"id":13,"text":"\"s\""},{"id":14,"subNodes":[15,16],"text":"x = \"p\""},{"id":15,"text":"x"},{"id":16,"text":"\"p\""},{"id":17,"subNodes":[18,19],"text":"i = +(i, 1)"},{"id":18,"text":"i"},{"id":19,"subNodes":[20,21],"text":"+(i, 1)"},{"id":20,"text":"i"},{"id":21,"text":"1"},{"id":22,"subNodes":[23],"text":"return x"},{"id":23,"text":"x"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"TrueEdge"},{"sourceId":3,"destId":22,"kind":"FalseEdge"},{"sourceId":6,"destId":11,"kind":"TrueEdge"},{"sourceId":6,"destId":14,"kind":"FalseEdge"},{"sourceId":11,"destId":17,"kind":"SequentialEdge"},{"sourceId":14,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":3,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32"]},"stack":["int32"]},"value":{"map":{"i":"[-Inf, +Inf]","x":"[0, 0]"},"stack":"[0, 0]"}}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"]},"stack":"#TOP#"},"value":{"map":{"i":"[-Inf, +Inf]"},"stack":"_|_"}}}},{"nodeId":2,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"]},"stack":["int32"]},"value":{"map":{"i":"[-Inf, +Inf]"},"stack":"[0, 0]"}}}},{"nodeId":3,"description":{"expressions":["i > 5"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["bool"]},"value":{"map":{"i":"[-Inf, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":4,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":"#TOP#"},"value":{"map":{"i":"[-Inf, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":5,"description":{"expressions":["5"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32"]},"value":{"map":{"i":"[-Inf, +Inf]","x":"[-Inf, +Inf]"},"stack":"[5, 5]"}}}},{"nodeId":6,"description":{"expressions":["i % 2 == 0"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["bool"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":7,"description":{"expressions":["i % 2"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["float32","int32"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":8,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":"#TOP#"},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[6, +Inf]"}}}},{"nodeId":9,"description":{"expressions":["2"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[2, 2]"}}}},{"nodeId":10,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[0, 0]"}}}},{"nodeId":11,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":["string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":12,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32","string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":13,"description":{"expressions":["\"s\""],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":14,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":["string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":15,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32","string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":16,"description":{"expressions":["\"p\""],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":17,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"map":{"i":["float32","int32"],"this":["typing*"],"x":["string"]},"stack":["float32","int32"]},"value":{"map":{"i":"[7, +Inf]","x":"[-Inf, +Inf]"},"stack":"[7, +Inf]"}}}},{"nodeId":18,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":"#TOP#"},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[6, +Inf]"}}}},{"nodeId":19,"description":{"expressions":["i + 1"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":["float32","int32"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[7, +Inf]"}}}},{"nodeId":20,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":"#TOP#"},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[6, +Inf]"}}}},{"nodeId":21,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":["int32"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[1, 1]"}}}},{"nodeId":22,"description":{"expressions":["ret_value@test5"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","ret_value@test5":["int32","string"],"this":["typing*"],"x":["int32","string"]},"stack":["int32","string"]},"value":{"map":{"i":"[-Inf, 5]","ret_value@test5":"[-Inf, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":23,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32","string"]},"value":{"map":{"i":"[-Inf, 5]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}}]}
1+
{"name":"untyped typing::test5(typing* this, untyped i)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = 0"},{"id":1,"text":"x"},{"id":2,"text":"0"},{"id":3,"subNodes":[4,5],"text":">(i, 5)"},{"id":4,"text":"i"},{"id":5,"text":"5"},{"id":6,"subNodes":[7,10],"text":"==(%(i, 2), 0)"},{"id":7,"subNodes":[8,9],"text":"%(i, 2)"},{"id":8,"text":"i"},{"id":9,"text":"2"},{"id":10,"text":"0"},{"id":11,"subNodes":[12,13],"text":"x = \"s\""},{"id":12,"text":"x"},{"id":13,"text":"\"s\""},{"id":14,"subNodes":[15,16],"text":"x = \"p\""},{"id":15,"text":"x"},{"id":16,"text":"\"p\""},{"id":17,"subNodes":[18,19],"text":"i = +(i, 1)"},{"id":18,"text":"i"},{"id":19,"subNodes":[20,21],"text":"+(i, 1)"},{"id":20,"text":"i"},{"id":21,"text":"1"},{"id":22,"subNodes":[23],"text":"return x"},{"id":23,"text":"x"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"TrueEdge"},{"sourceId":3,"destId":22,"kind":"FalseEdge"},{"sourceId":6,"destId":11,"kind":"TrueEdge"},{"sourceId":6,"destId":14,"kind":"FalseEdge"},{"sourceId":11,"destId":17,"kind":"SequentialEdge"},{"sourceId":14,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":3,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32"]},"stack":["int32"]},"value":{"map":{"i":"[-Inf, +Inf]","x":"[0, 0]"},"stack":"[0, 0]"}}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"]},"stack":"#TOP#"},"value":{"map":{"i":"[-Inf, +Inf]"},"stack":"_|_"}}}},{"nodeId":2,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"]},"stack":["int32"]},"value":{"map":{"i":"[-Inf, +Inf]"},"stack":"[0, 0]"}}}},{"nodeId":3,"description":{"expressions":["i > 5"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["bool"]},"value":{"map":{"i":"[-Inf, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":4,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":"#TOP#"},"value":{"map":{"i":"[-Inf, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":5,"description":{"expressions":["5"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32"]},"value":{"map":{"i":"[-Inf, +Inf]","x":"[-Inf, +Inf]"},"stack":"[5, 5]"}}}},{"nodeId":6,"description":{"expressions":["i % 2 == 0"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["bool"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":7,"description":{"expressions":["i % 2"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["float32","int32"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[0, 1]"}}}},{"nodeId":8,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":"#TOP#"},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[6, +Inf]"}}}},{"nodeId":9,"description":{"expressions":["2"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[2, 2]"}}}},{"nodeId":10,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[0, 0]"}}}},{"nodeId":11,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":["string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":12,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32","string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":13,"description":{"expressions":["\"s\""],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":14,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":["string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":15,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32","string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":16,"description":{"expressions":["\"p\""],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["string"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":17,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"map":{"i":["float32","int32"],"this":["typing*"],"x":["string"]},"stack":["float32","int32"]},"value":{"map":{"i":"[7, +Inf]","x":"[-Inf, +Inf]"},"stack":"[7, +Inf]"}}}},{"nodeId":18,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":"#TOP#"},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[6, +Inf]"}}}},{"nodeId":19,"description":{"expressions":["i + 1"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":["float32","int32"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[7, +Inf]"}}}},{"nodeId":20,"description":{"expressions":["i"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":"#TOP#"},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[6, +Inf]"}}}},{"nodeId":21,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["string"]},"stack":["int32"]},"value":{"map":{"i":"[6, +Inf]","x":"[-Inf, +Inf]"},"stack":"[1, 1]"}}}},{"nodeId":22,"description":{"expressions":["ret_value@test5"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","ret_value@test5":["int32","string"],"this":["typing*"],"x":["int32","string"]},"stack":["int32","string"]},"value":{"map":{"i":"[-Inf, 5]","ret_value@test5":"[-Inf, +Inf]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}},{"nodeId":23,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"map":{"i":"#TOP#","this":["typing*"],"x":["int32","string"]},"stack":["int32","string"]},"value":{"map":{"i":"[-Inf, 5]","x":"[-Inf, +Inf]"},"stack":"[-Inf, +Inf]"}}}}]}

‎lisa/lisa-core/src/main/java/it/unive/lisa/analysis/numeric/IntegerConstantPropagation.java‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
import it.unive.lisa.symbolic.value.operator.DivisionOperator;
1717
import it.unive.lisa.symbolic.value.operator.ModuloOperator;
1818
import it.unive.lisa.symbolic.value.operator.MultiplicationOperator;
19+
import it.unive.lisa.symbolic.value.operator.RemainderOperator;
1920
import it.unive.lisa.symbolic.value.operator.SubtractionOperator;
2021
import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
2122
import it.unive.lisa.symbolic.value.operator.binary.ComparisonEq;
@@ -141,6 +142,12 @@ else if (left.isTop() || right.isTop() || left.value % right.value != 0)
141142
else
142143
return new IntegerConstantPropagation(left.value / right.value);
143144
else if (operator instanceof ModuloOperator)
145+
// this is different from the semantics of java
146+
return left.isTop() || right.isTop() ? top()
147+
: new IntegerConstantPropagation(right.value < 0 ? -Math.abs(left.value % right.value)
148+
: -Math.abs(left.value % right.value));
149+
else if (operator instanceof RemainderOperator)
150+
// this matches the semantics of java
144151
return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value % right.value);
145152
else if (operator instanceof MultiplicationOperator)
146153
return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value * right.value);

‎lisa/lisa-core/src/main/java/it/unive/lisa/analysis/numeric/Interval.java‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,9 @@
1414
import it.unive.lisa.symbolic.value.ValueExpression;
1515
import it.unive.lisa.symbolic.value.operator.AdditionOperator;
1616
import it.unive.lisa.symbolic.value.operator.DivisionOperator;
17+
import it.unive.lisa.symbolic.value.operator.ModuloOperator;
1718
import it.unive.lisa.symbolic.value.operator.MultiplicationOperator;
19+
import it.unive.lisa.symbolic.value.operator.RemainderOperator;
1820
import it.unive.lisa.symbolic.value.operator.SubtractionOperator;
1921
import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
2022
import it.unive.lisa.symbolic.value.operator.binary.ComparisonEq;
@@ -188,6 +190,58 @@ else if (left.isTop() || right.isTop())
188190
return top();
189191
else
190192
return new Interval(left.interval.div(right.interval, false, false));
193+
else if (operator instanceof ModuloOperator)
194+
if (right.is(0))
195+
return bottom();
196+
else if (left.is(0))
197+
return ZERO;
198+
else if (left.isTop() || right.isTop())
199+
return top();
200+
else {
201+
// the result takes the sign of the divisor - l%r is:
202+
// - [r.low+1,0] if r.high < 0 (fully negative)
203+
// - [0,r.high-1] if r.low > 0 (fully positive)
204+
// - [r.low+1,r.high-1] otherwise
205+
if (right.interval.getHigh().compareTo(MathNumber.ZERO) < 0)
206+
return new Interval(right.interval.getLow().add(MathNumber.ONE), MathNumber.ZERO);
207+
else if (right.interval.getLow().compareTo(MathNumber.ZERO) > 0)
208+
return new Interval(MathNumber.ZERO, right.interval.getHigh().subtract(MathNumber.ONE));
209+
else
210+
return new Interval(right.interval.getLow().add(MathNumber.ONE),
211+
right.interval.getHigh().subtract(MathNumber.ONE));
212+
}
213+
else if (operator instanceof RemainderOperator)
214+
if (right.is(0))
215+
return bottom();
216+
else if (left.is(0))
217+
return ZERO;
218+
else if (left.isTop() || right.isTop())
219+
return top();
220+
else {
221+
// the result takes the sign of the dividend - l%r is:
222+
// - [-M+1,0] if l.high < 0 (fully negative)
223+
// - [0,M-1] if l.low > 0 (fully positive)
224+
// - [-M+1,M-1] otherwise
225+
// where M is
226+
// - -r.low if r.high < 0 (fully negative)
227+
// - r.high if r.low > 0 (fully positive)
228+
// - max(abs(r.low),abs(r.right)) otherwise
229+
MathNumber M;
230+
if (right.interval.getHigh().compareTo(MathNumber.ZERO) < 0)
231+
M = right.interval.getLow().multiply(MathNumber.MINUS_ONE);
232+
else if (right.interval.getLow().compareTo(MathNumber.ZERO) > 0)
233+
M = right.interval.getHigh();
234+
else
235+
M = right.interval.getLow().abs().max(right.interval.getHigh().abs());
236+
237+
if (left.interval.getHigh().compareTo(MathNumber.ZERO) < 0)
238+
return new Interval(M.multiply(MathNumber.MINUS_ONE).add(MathNumber.ONE), MathNumber.ZERO);
239+
else if (left.interval.getLow().compareTo(MathNumber.ZERO) > 0)
240+
return new Interval(MathNumber.ZERO, M.subtract(MathNumber.ONE));
241+
else
242+
return new Interval(M.multiply(MathNumber.MINUS_ONE).add(MathNumber.ONE),
243+
M.subtract(MathNumber.ONE));
244+
}
191245
return top();
192246
}
193247

‎lisa/lisa-core/src/main/java/it/unive/lisa/analysis/numeric/Parity.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
import it.unive.lisa.symbolic.value.operator.DivisionOperator;
1616
import it.unive.lisa.symbolic.value.operator.ModuloOperator;
1717
import it.unive.lisa.symbolic.value.operator.MultiplicationOperator;
18+
import it.unive.lisa.symbolic.value.operator.RemainderOperator;
1819
import it.unive.lisa.symbolic.value.operator.SubtractionOperator;
1920
import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
2021
import it.unive.lisa.symbolic.value.operator.binary.ComparisonEq;
@@ -159,7 +160,7 @@ else if (operator instanceof DivisionOperator)
159160
return right.isOdd() ? ODD : EVEN;
160161
else
161162
return right.isOdd() ? EVEN : TOP;
162-
else if (operator instanceof ModuloOperator)
163+
else if (operator instanceof ModuloOperator || operator instanceof RemainderOperator)
163164
return TOP;
164165

165166
return TOP;

‎lisa/lisa-core/src/main/java/it/unive/lisa/analysis/numeric/Sign.java‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
import it.unive.lisa.symbolic.value.operator.DivisionOperator;
1717
import it.unive.lisa.symbolic.value.operator.ModuloOperator;
1818
import it.unive.lisa.symbolic.value.operator.MultiplicationOperator;
19+
import it.unive.lisa.symbolic.value.operator.RemainderOperator;
1920
import it.unive.lisa.symbolic.value.operator.SubtractionOperator;
2021
import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
2122
import it.unive.lisa.symbolic.value.operator.binary.ComparisonEq;
@@ -215,7 +216,9 @@ else if (left.equals(right))
215216
else
216217
return top();
217218
else if (operator instanceof ModuloOperator)
218-
return top();
219+
return right;
220+
else if (operator instanceof RemainderOperator)
221+
return left;
219222
else if (operator instanceof MultiplicationOperator)
220223
if (left.isZero() || right.isZero())
221224
return ZERO;

0 commit comments

Comments
 (0)