Skip to content

Commit

Permalink
Merge pull request #134 from UniVE-SSV/symbolic-operators
Browse files Browse the repository at this point in the history 
Bitwise and overflow-sensitive symbolic operators
  • Loading branch information
@VincenzoArceri
VincenzoArceri authored Oct 1, 2021
2 parents 20bfed4 + 9f8bd12 commit dfb6bee
Show file tree
Hide file tree
Showing 18 changed files with 834 additions and 212 deletions.
34 changes: 27 additions & 7 deletions lisa/lisa-core/src/main/java/it/unive/lisa/analysis/dataflow/ConstantPropagation.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@
import java.util.Set;

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

switch (binary.getOperator()) {
case NUMERIC_ADD:
case NUMERIC_NON_OVERFLOWING_ADD:
case NUMERIC_8BIT_ADD:
case NUMERIC_16BIT_ADD:
case NUMERIC_32BIT_ADD:
case NUMERIC_64BIT_ADD:
return left + right;
case NUMERIC_DIV:
case NUMERIC_NON_OVERFLOWING_DIV:
case NUMERIC_8BIT_DIV:
case NUMERIC_16BIT_DIV:
case NUMERIC_32BIT_DIV:
case NUMERIC_64BIT_DIV:
return left == 0 ? null : (int) left / right;
case NUMERIC_MOD:
case NUMERIC_NON_OVERFLOWING_MOD:
case NUMERIC_8BIT_MOD:
case NUMERIC_16BIT_MOD:
case NUMERIC_32BIT_MOD:
case NUMERIC_64BIT_MOD:
return right == 0 ? null : left % right;
case NUMERIC_MUL:
case NUMERIC_NON_OVERFLOWING_MUL:
case NUMERIC_8BIT_MUL:
case NUMERIC_16BIT_MUL:
case NUMERIC_32BIT_MUL:
case NUMERIC_64BIT_MUL:
return left * right;
case NUMERIC_SUB:
case NUMERIC_NON_OVERFLOWING_SUB:
case NUMERIC_8BIT_SUB:
case NUMERIC_16BIT_SUB:
case NUMERIC_32BIT_SUB:
case NUMERIC_64BIT_SUB:
return left - right;
default:
break;
Expand Down
45 changes: 32 additions & 13 deletions lisa/lisa-core/src/main/java/it/unive/lisa/analysis/numeric/IntegerConstantPropagation.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,14 +17,14 @@
import it.unive.lisa.symbolic.value.ValueExpression;

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

switch (operator) {
case NUMERIC_ADD:
case NUMERIC_NON_OVERFLOWING_ADD:
case NUMERIC_8BIT_ADD:
case NUMERIC_16BIT_ADD:
case NUMERIC_32BIT_ADD:
case NUMERIC_64BIT_ADD:
return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value + right.value);
case NUMERIC_DIV:
case NUMERIC_NON_OVERFLOWING_DIV:
case NUMERIC_8BIT_DIV:
case NUMERIC_16BIT_DIV:
case NUMERIC_32BIT_DIV:
case NUMERIC_64BIT_DIV:
if (!left.isTop() && left.value == 0)
return new IntegerConstantPropagation(0);
else if (!right.isTop() && right.value == 0)
Expand All @@ -129,11 +137,22 @@ else if (left.isTop() || right.isTop() || left.value % right.value != 0)
return top();
else
return new IntegerConstantPropagation(left.value / right.value);
case NUMERIC_MOD:
case NUMERIC_NON_OVERFLOWING_MOD:
case NUMERIC_8BIT_MOD:
case NUMERIC_16BIT_MOD:
case NUMERIC_32BIT_MOD:
case NUMERIC_64BIT_MOD:
return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value % right.value);
case NUMERIC_MUL:
case NUMERIC_NON_OVERFLOWING_MUL:
case NUMERIC_8BIT_MUL:
case NUMERIC_16BIT_MUL:
case NUMERIC_32BIT_MUL:
return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value * right.value);
case NUMERIC_SUB:
case NUMERIC_NON_OVERFLOWING_SUB:
case NUMERIC_8BIT_SUB:
case NUMERIC_16BIT_SUB:
case NUMERIC_32BIT_SUB:
case NUMERIC_64BIT_SUB:
return left.isTop() || right.isTop() ? top() : new IntegerConstantPropagation(left.value - right.value);
default:
return top();
Expand Down
42 changes: 29 additions & 13 deletions lisa/lisa-core/src/main/java/it/unive/lisa/analysis/numeric/Interval.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,14 +18,14 @@
import it.unive.lisa.util.numeric.MathNumber;

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

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

switch (operator) {
case NUMERIC_ADD:
case NUMERIC_NON_OVERFLOWING_ADD:
case NUMERIC_8BIT_ADD:
case NUMERIC_16BIT_ADD:
case NUMERIC_32BIT_ADD:
case NUMERIC_64BIT_ADD:
return new Interval(left.interval.plus(right.interval));
case NUMERIC_SUB:
case NUMERIC_NON_OVERFLOWING_SUB:
case NUMERIC_8BIT_SUB:
case NUMERIC_16BIT_SUB:
case NUMERIC_32BIT_SUB:
case NUMERIC_64BIT_SUB:
return new Interval(left.interval.diff(right.interval));
case NUMERIC_MUL:
case NUMERIC_NON_OVERFLOWING_MUL:
case NUMERIC_8BIT_MUL:
case NUMERIC_16BIT_MUL:
case NUMERIC_32BIT_MUL:
case NUMERIC_64BIT_MUL:
if (left.is(0) || right.is(0))
return ZERO;
return new Interval(left.interval.mul(right.interval));
case NUMERIC_DIV:
case NUMERIC_NON_OVERFLOWING_DIV:
case NUMERIC_8BIT_DIV:
case NUMERIC_16BIT_DIV:
case NUMERIC_32BIT_DIV:
case NUMERIC_64BIT_DIV:
if (right.is(0))
return bottom();
if (left.is(0))
Expand Down
44 changes: 32 additions & 12 deletions lisa/lisa-core/src/main/java/it/unive/lisa/analysis/numeric/Parity.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,13 +15,13 @@
import it.unive.lisa.symbolic.value.ValueExpression;

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

switch (operator) {
case NUMERIC_ADD:
case NUMERIC_SUB:
case NUMERIC_NON_OVERFLOWING_ADD:
case NUMERIC_8BIT_ADD:
case NUMERIC_16BIT_ADD:
case NUMERIC_32BIT_ADD:
case NUMERIC_64BIT_ADD:
case NUMERIC_NON_OVERFLOWING_SUB:
case NUMERIC_8BIT_SUB:
case NUMERIC_16BIT_SUB:
case NUMERIC_32BIT_SUB:
case NUMERIC_64BIT_SUB:
if (right.equals(left))
return EVEN;
else
return ODD;
case NUMERIC_MUL:
case NUMERIC_NON_OVERFLOWING_MUL:
case NUMERIC_8BIT_MUL:
case NUMERIC_16BIT_MUL:
case NUMERIC_32BIT_MUL:
case NUMERIC_64BIT_MUL:
if (left.isEven() || right.isEven())
return EVEN;
else
return ODD;
case NUMERIC_DIV:
case NUMERIC_NON_OVERFLOWING_DIV:
case NUMERIC_8BIT_DIV:
case NUMERIC_16BIT_DIV:
case NUMERIC_32BIT_DIV:
case NUMERIC_64BIT_DIV:
if (left.isOdd())
return right.isOdd() ? ODD : EVEN;
else
return right.isOdd() ? EVEN : TOP;
case NUMERIC_MOD:
case NUMERIC_NON_OVERFLOWING_MOD:
case NUMERIC_8BIT_MOD:
case NUMERIC_16BIT_MOD:
case NUMERIC_32BIT_MOD:
case NUMERIC_64BIT_MOD:
return TOP;
default:
return TOP;
Expand Down
34 changes: 27 additions & 7 deletions lisa/lisa-core/src/main/java/it/unive/lisa/analysis/numeric/Sign.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@
import it.unive.lisa.symbolic.value.ValueExpression;

/**
* The basic Sign abstract domain, tracking zero, strictly positive and strictly
* negative integer values, implemented as a
* The basic overflow-insensitive Sign abstract domain, tracking zero, strictly
* positive and strictly negative integer values, implemented as a
* {@link BaseNonRelationalValueDomain}, handling top and bottom values for the
* expression evaluation and bottom values for the expression satisfiability.
* Top and bottom cases for least upper bounds, widening and less or equals
Expand Down Expand Up @@ -131,7 +131,11 @@ else if (arg.isZero())
@Override
protected Sign evalBinaryExpression(BinaryOperator operator, Sign left, Sign right, ProgramPoint pp) {
switch (operator) {
case NUMERIC_ADD:
case NUMERIC_NON_OVERFLOWING_ADD:
case NUMERIC_8BIT_ADD:
case NUMERIC_16BIT_ADD:
case NUMERIC_32BIT_ADD:
case NUMERIC_64BIT_ADD:
if (left.isZero())
return right;
else if (right.isZero())
Expand All @@ -140,7 +144,11 @@ else if (left.equals(right))
return left;
else
return top();
case NUMERIC_SUB:
case NUMERIC_NON_OVERFLOWING_SUB:
case NUMERIC_8BIT_SUB:
case NUMERIC_16BIT_SUB:
case NUMERIC_32BIT_SUB:
case NUMERIC_64BIT_SUB:
if (left.isZero())
return right.opposite();
else if (right.isZero())
Expand All @@ -149,7 +157,11 @@ else if (left.equals(right))
return top();
else
return left;
case NUMERIC_DIV:
case NUMERIC_NON_OVERFLOWING_DIV:
case NUMERIC_8BIT_DIV:
case NUMERIC_16BIT_DIV:
case NUMERIC_32BIT_DIV:
case NUMERIC_64BIT_DIV:
if (right.isZero())
return bottom();
else if (left.isZero())
Expand All @@ -160,9 +172,17 @@ else if (left.equals(right))
// -/- = +
return left.isTop() ? left : POS;
return top();
case NUMERIC_MOD:
case NUMERIC_NON_OVERFLOWING_MOD:
case NUMERIC_8BIT_MOD:
case NUMERIC_16BIT_MOD:
case NUMERIC_32BIT_MOD:
case NUMERIC_64BIT_MOD:
return top();
case NUMERIC_MUL:
case NUMERIC_NON_OVERFLOWING_MUL:
case NUMERIC_8BIT_MUL:
case NUMERIC_16BIT_MUL:
case NUMERIC_32BIT_MUL:
case NUMERIC_64BIT_MUL:
if (left.isZero() || right.isZero())
return ZERO;
else if (left.equals(right))
Expand Down
Loading

0 comments on commit dfb6bee

Please sign in to comment.