Skip to content

Commit dfb6bee

Browse files
VincenzoArceriVincenzoArceri
authored
Merge pull request #134 from UniVE-SSV/symbolic-operators
Bitwise and overflow-sensitive symbolic operators
2 parents 20bfed4 + 9f8bd12 commit dfb6bee

File tree

18 files changed

+834
-212
lines changed

18 files changed

+834
-212
lines changed

‎lisa/lisa-core/src/main/java/it/unive/lisa/analysis/dataflow/ConstantPropagation.java‎

Lines changed: 27 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,8 @@
1919
import java.util.Set;
2020

2121
/**
22-
* An implementation of the constant propagation dataflow analysis, that focuses
23-
* only on integers.
22+
* An implementation of the overflow-insensitive constant propagation dataflow
23+
* analysis, that focuses only on integers.
2424
*
2525
* @author <a href="mailto:[email protected]">Luca Negrini</a>
2626
*/
@@ -91,15 +91,35 @@ private static Integer eval(SymbolicExpression e, DefiniteForwardDataflowDomain<
9191
return null;
9292

9393
switch (binary.getOperator()) {
94-
case NUMERIC_ADD:
94+
case NUMERIC_NON_OVERFLOWING_ADD:
95+
case NUMERIC_8BIT_ADD:
96+
case NUMERIC_16BIT_ADD:
97+
case NUMERIC_32BIT_ADD:
98+
case NUMERIC_64BIT_ADD:
9599
return left + right;
96-
case NUMERIC_DIV:
100+
case NUMERIC_NON_OVERFLOWING_DIV:
101+
case NUMERIC_8BIT_DIV:
102+
case NUMERIC_16BIT_DIV:
103+
case NUMERIC_32BIT_DIV:
104+
case NUMERIC_64BIT_DIV:
97105
return left == 0 ? null : (int) left / right;
98-
case NUMERIC_MOD:
106+
case NUMERIC_NON_OVERFLOWING_MOD:
107+
case NUMERIC_8BIT_MOD:
108+
case NUMERIC_16BIT_MOD:
109+
case NUMERIC_32BIT_MOD:
110+
case NUMERIC_64BIT_MOD:
99111
return right == 0 ? null : left % right;
100-
case NUMERIC_MUL:
112+
case NUMERIC_NON_OVERFLOWING_MUL:
113+
case NUMERIC_8BIT_MUL:
114+
case NUMERIC_16BIT_MUL:
115+
case NUMERIC_32BIT_MUL:
116+
case NUMERIC_64BIT_MUL:
101117
return left * right;
102-
case NUMERIC_SUB:
118+
case NUMERIC_NON_OVERFLOWING_SUB:
119+
case NUMERIC_8BIT_SUB:
120+
case NUMERIC_16BIT_SUB:
121+
case NUMERIC_32BIT_SUB:
122+
case NUMERIC_64BIT_SUB:
103123
return left - right;
104124
default:
105125
break;

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

Lines changed: 32 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -17,14 +17,14 @@
1717
import it.unive.lisa.symbolic.value.ValueExpression;
1818

1919
/**
20-
* The basic integer constant propagation abstract domain, tracking if a certain
21-
* integer value has constant value or not, implemented as a
22-
* {@link BaseNonRelationalValueDomain}, handling top and bottom values for the
23-
* expression evaluation and bottom values for the expression satisfiability.
24-
* Top and bottom cases for least upper bounds, widening and less or equals
25-
* operations are handled by {@link BaseLattice} in {@link BaseLattice#lub},
26-
* {@link BaseLattice#widening} and {@link BaseLattice#lessOrEqual},
27-
* respectively.
20+
* The overflow-insensitive basic integer constant propagation abstract domain,
21+
* tracking if a certain integer value has constant value or not, implemented as
22+
* a {@link BaseNonRelationalValueDomain}, handling top and bottom values for
23+
* the expression evaluation and bottom values for the expression
24+
* satisfiability. Top and bottom cases for least upper bounds, widening and
25+
* less or equals operations are handled by {@link BaseLattice} in
26+
* {@link BaseLattice#lub}, {@link BaseLattice#widening} and
27+
* {@link BaseLattice#lessOrEqual}, respectively.
2828
*
2929
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
3030
*/
@@ -118,9 +118,17 @@ protected IntegerConstantPropagation evalBinaryExpression(BinaryOperator operato
118118
IntegerConstantPropagation right, ProgramPoint pp) {
119119

120120
switch (operator) {
121-
case NUMERIC_ADD:
121+
case NUMERIC_NON_OVERFLOWING_ADD:
122+
case NUMERIC_8BIT_ADD:
123+
case NUMERIC_16BIT_ADD:
124+
case NUMERIC_32BIT_ADD:
125+
case NUMERIC_64BIT_ADD:
122126
return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value + right.value);
123-
case NUMERIC_DIV:
127+
case NUMERIC_NON_OVERFLOWING_DIV:
128+
case NUMERIC_8BIT_DIV:
129+
case NUMERIC_16BIT_DIV:
130+
case NUMERIC_32BIT_DIV:
131+
case NUMERIC_64BIT_DIV:
124132
if (!left.isTop() && left.value == 0)
125133
return new IntegerConstantPropagation(0);
126134
else if (!right.isTop() && right.value == 0)
@@ -129,11 +137,22 @@ else if (left.isTop() || right.isTop() || left.value % right.value != 0)
129137
return top();
130138
else
131139
return new IntegerConstantPropagation(left.value / right.value);
132-
case NUMERIC_MOD:
140+
case NUMERIC_NON_OVERFLOWING_MOD:
141+
case NUMERIC_8BIT_MOD:
142+
case NUMERIC_16BIT_MOD:
143+
case NUMERIC_32BIT_MOD:
144+
case NUMERIC_64BIT_MOD:
133145
return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value % right.value);
134-
case NUMERIC_MUL:
146+
case NUMERIC_NON_OVERFLOWING_MUL:
147+
case NUMERIC_8BIT_MUL:
148+
case NUMERIC_16BIT_MUL:
149+
case NUMERIC_32BIT_MUL:
135150
return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value * right.value);
136-
case NUMERIC_SUB:
151+
case NUMERIC_NON_OVERFLOWING_SUB:
152+
case NUMERIC_8BIT_SUB:
153+
case NUMERIC_16BIT_SUB:
154+
case NUMERIC_32BIT_SUB:
155+
case NUMERIC_64BIT_SUB:
137156
return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value - right.value);
138157
default:
139158
return top();

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

Lines changed: 29 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -18,14 +18,14 @@
1818
import it.unive.lisa.util.numeric.MathNumber;
1919

2020
/**
21-
* The interval abstract domain, approximating integer values as the minimum
22-
* integer interval containing them. It is implemented as a
23-
* {@link BaseNonRelationalValueDomain}, handling top and bottom values for the
24-
* expression evaluation and bottom values for the expression satisfiability.
25-
* Top and bottom cases for least upper bounds, widening and less or equals
26-
* operations are handled by {@link BaseLattice} in {@link BaseLattice#lub},
27-
* {@link BaseLattice#widening} and {@link BaseLattice#lessOrEqual} methods,
28-
* respectively.
21+
* The overflow-insensitive interval abstract domain, approximating integer
22+
* values as the minimum integer interval containing them. It is implemented as
23+
* a {@link BaseNonRelationalValueDomain}, handling top and bottom values for
24+
* the expression evaluation and bottom values for the expression
25+
* satisfiability. Top and bottom cases for least upper bounds, widening and
26+
* less or equals operations are handled by {@link BaseLattice} in
27+
* {@link BaseLattice#lub}, {@link BaseLattice#widening} and
28+
* {@link BaseLattice#lessOrEqual} methods, respectively.
2929
*
3030
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
3131
*/
@@ -113,21 +113,37 @@ private boolean is(int n) {
113113

114114
@Override
115115
protected Interval evalBinaryExpression(BinaryOperator operator, Interval left, Interval right, ProgramPoint pp) {
116-
if (operator != BinaryOperator.NUMERIC_DIV && (left.isTop() || right.isTop()))
116+
if (operator != BinaryOperator.NUMERIC_NON_OVERFLOWING_DIV && (left.isTop() || right.isTop()))
117117
// with div, we can return zero or bottom even if one of the
118118
// operands is top
119119
return top();
120120

121121
switch (operator) {
122-
case NUMERIC_ADD:
122+
case NUMERIC_NON_OVERFLOWING_ADD:
123+
case NUMERIC_8BIT_ADD:
124+
case NUMERIC_16BIT_ADD:
125+
case NUMERIC_32BIT_ADD:
126+
case NUMERIC_64BIT_ADD:
123127
return new Interval(left.interval.plus(right.interval));
124-
case NUMERIC_SUB:
128+
case NUMERIC_NON_OVERFLOWING_SUB:
129+
case NUMERIC_8BIT_SUB:
130+
case NUMERIC_16BIT_SUB:
131+
case NUMERIC_32BIT_SUB:
132+
case NUMERIC_64BIT_SUB:
125133
return new Interval(left.interval.diff(right.interval));
126-
case NUMERIC_MUL:
134+
case NUMERIC_NON_OVERFLOWING_MUL:
135+
case NUMERIC_8BIT_MUL:
136+
case NUMERIC_16BIT_MUL:
137+
case NUMERIC_32BIT_MUL:
138+
case NUMERIC_64BIT_MUL:
127139
if (left.is(0) || right.is(0))
128140
return ZERO;
129141
return new Interval(left.interval.mul(right.interval));
130-
case NUMERIC_DIV:
142+
case NUMERIC_NON_OVERFLOWING_DIV:
143+
case NUMERIC_8BIT_DIV:
144+
case NUMERIC_16BIT_DIV:
145+
case NUMERIC_32BIT_DIV:
146+
case NUMERIC_64BIT_DIV:
131147
if (right.is(0))
132148
return bottom();
133149
if (left.is(0))

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

Lines changed: 32 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,13 @@
1515
import it.unive.lisa.symbolic.value.ValueExpression;
1616

1717
/**
18-
* The Parity abstract domain, tracking if a numeric value is even or odd,
19-
* implemented as a {@link BaseNonRelationalValueDomain}, handling top and
20-
* bottom values for the expression evaluation and bottom values for the
21-
* expression satisfiability. Top and bottom cases for least upper bound,
22-
* widening and less or equals operations are handled by {@link BaseLattice} in
23-
* {@link BaseLattice#lub}, {@link BaseLattice#widening} and
24-
* {@link BaseLattice#lessOrEqual} methods, respectively.
18+
* The overflow-insensitive Parity abstract domain, tracking if a numeric value
19+
* is even or odd, implemented as a {@link BaseNonRelationalValueDomain},
20+
* handling top and bottom values for the expression evaluation and bottom
21+
* values for the expression satisfiability. Top and bottom cases for least
22+
* upper bound, widening and less or equals operations are handled by
23+
* {@link BaseLattice} in {@link BaseLattice#lub}, {@link BaseLattice#widening}
24+
* and {@link BaseLattice#lessOrEqual} methods, respectively.
2525
*
2626
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
2727
*/
@@ -111,23 +111,43 @@ protected Parity evalBinaryExpression(BinaryOperator operator, Parity left, Pari
111111
return top();
112112

113113
switch (operator) {
114-
case NUMERIC_ADD:
115-
case NUMERIC_SUB:
114+
case NUMERIC_NON_OVERFLOWING_ADD:
115+
case NUMERIC_8BIT_ADD:
116+
case NUMERIC_16BIT_ADD:
117+
case NUMERIC_32BIT_ADD:
118+
case NUMERIC_64BIT_ADD:
119+
case NUMERIC_NON_OVERFLOWING_SUB:
120+
case NUMERIC_8BIT_SUB:
121+
case NUMERIC_16BIT_SUB:
122+
case NUMERIC_32BIT_SUB:
123+
case NUMERIC_64BIT_SUB:
116124
if (right.equals(left))
117125
return EVEN;
118126
else
119127
return ODD;
120-
case NUMERIC_MUL:
128+
case NUMERIC_NON_OVERFLOWING_MUL:
129+
case NUMERIC_8BIT_MUL:
130+
case NUMERIC_16BIT_MUL:
131+
case NUMERIC_32BIT_MUL:
132+
case NUMERIC_64BIT_MUL:
121133
if (left.isEven() || right.isEven())
122134
return EVEN;
123135
else
124136
return ODD;
125-
case NUMERIC_DIV:
137+
case NUMERIC_NON_OVERFLOWING_DIV:
138+
case NUMERIC_8BIT_DIV:
139+
case NUMERIC_16BIT_DIV:
140+
case NUMERIC_32BIT_DIV:
141+
case NUMERIC_64BIT_DIV:
126142
if (left.isOdd())
127143
return right.isOdd() ? ODD : EVEN;
128144
else
129145
return right.isOdd() ? EVEN : TOP;
130-
case NUMERIC_MOD:
146+
case NUMERIC_NON_OVERFLOWING_MOD:
147+
case NUMERIC_8BIT_MOD:
148+
case NUMERIC_16BIT_MOD:
149+
case NUMERIC_32BIT_MOD:
150+
case NUMERIC_64BIT_MOD:
131151
return TOP;
132152
default:
133153
return TOP;

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

Lines changed: 27 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@
1717
import it.unive.lisa.symbolic.value.ValueExpression;
1818

1919
/**
20-
* The basic Sign abstract domain, tracking zero, strictly positive and strictly
21-
* negative integer values, implemented as a
20+
* The basic overflow-insensitive Sign abstract domain, tracking zero, strictly
21+
* positive and strictly negative integer values, implemented as a
2222
* {@link BaseNonRelationalValueDomain}, handling top and bottom values for the
2323
* expression evaluation and bottom values for the expression satisfiability.
2424
* Top and bottom cases for least upper bounds, widening and less or equals
@@ -131,7 +131,11 @@ else if (arg.isZero())
131131
@Override
132132
protected Sign evalBinaryExpression(BinaryOperator operator, Sign left, Sign right, ProgramPoint pp) {
133133
switch (operator) {
134-
case NUMERIC_ADD:
134+
case NUMERIC_NON_OVERFLOWING_ADD:
135+
case NUMERIC_8BIT_ADD:
136+
case NUMERIC_16BIT_ADD:
137+
case NUMERIC_32BIT_ADD:
138+
case NUMERIC_64BIT_ADD:
135139
if (left.isZero())
136140
return right;
137141
else if (right.isZero())
@@ -140,7 +144,11 @@ else if (left.equals(right))
140144
return left;
141145
else
142146
return top();
143-
case NUMERIC_SUB:
147+
case NUMERIC_NON_OVERFLOWING_SUB:
148+
case NUMERIC_8BIT_SUB:
149+
case NUMERIC_16BIT_SUB:
150+
case NUMERIC_32BIT_SUB:
151+
case NUMERIC_64BIT_SUB:
144152
if (left.isZero())
145153
return right.opposite();
146154
else if (right.isZero())
@@ -149,7 +157,11 @@ else if (left.equals(right))
149157
return top();
150158
else
151159
return left;
152-
case NUMERIC_DIV:
160+
case NUMERIC_NON_OVERFLOWING_DIV:
161+
case NUMERIC_8BIT_DIV:
162+
case NUMERIC_16BIT_DIV:
163+
case NUMERIC_32BIT_DIV:
164+
case NUMERIC_64BIT_DIV:
153165
if (right.isZero())
154166
return bottom();
155167
else if (left.isZero())
@@ -160,9 +172,17 @@ else if (left.equals(right))
160172
// -/- = +
161173
return left.isTop() ? left : POS;
162174
return top();
163-
case NUMERIC_MOD:
175+
case NUMERIC_NON_OVERFLOWING_MOD:
176+
case NUMERIC_8BIT_MOD:
177+
case NUMERIC_16BIT_MOD:
178+
case NUMERIC_32BIT_MOD:
179+
case NUMERIC_64BIT_MOD:
164180
return top();
165-
case NUMERIC_MUL:
181+
case NUMERIC_NON_OVERFLOWING_MUL:
182+
case NUMERIC_8BIT_MUL:
183+
case NUMERIC_16BIT_MUL:
184+
case NUMERIC_32BIT_MUL:
185+
case NUMERIC_64BIT_MUL:
166186
if (left.isZero() || right.isZero())
167187
return ZERO;
168188
else if (left.equals(right))

0 commit comments

Comments
 (0)