Skip to content

Commit

Permalink
#140 #157 changing signatures of semantics methods to match eval order
Browse files Browse the repository at this point in the history
  • Loading branch information
@lucaneg
lucaneg committed Jan 12, 2022
1 parent cfc8f2b commit b7ced68
Show file tree
Hide file tree
Showing 42 changed files with 306 additions and 332 deletions.
8 changes: 3 additions & 5 deletions lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAddOrConcat.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,14 +54,12 @@ public IMPAddOrConcat(CFG cfg, String sourceFile, int line, int col, Expression
protected <A extends AbstractState<A, H, V>,
H extends HeapDomain<H>,
V extends ValueDomain<V>> AnalysisState<A, H, V> binarySemantics(
AnalysisState<A, H, V> entryState,
InterproceduralAnalysis<A, H, V> interprocedural,
AnalysisState<A, H, V> leftState,
AnalysisState<A, H, V> state,
SymbolicExpression left,
AnalysisState<A, H, V> rightState,
SymbolicExpression right)
throws SemanticException {
AnalysisState<A, H, V> result = entryState.bottom();
AnalysisState<A, H, V> result = state.bottom();
BinaryOperator op;

for (Type tleft : left.getTypes())
Expand Down Expand Up @@ -91,7 +89,7 @@ else if (tright.isNumericType() || tright.isUntyped())
if (op == null)
continue;

result = result.lub(rightState.smallStepSemantics(
result = result.lub(state.smallStepSemantics(
new BinaryExpression(
op == StringConcat.INSTANCE
? Caches.types().mkSingletonSet(StringType.INSTANCE)
Expand Down
10 changes: 4 additions & 6 deletions lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPArrayAccess.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,21 +42,19 @@ public IMPArrayAccess(CFG cfg, String sourceFile, int line, int col, Expression
protected <A extends AbstractState<A, H, V>,
H extends HeapDomain<H>,
V extends ValueDomain<V>> AnalysisState<A, H, V> binarySemantics(
AnalysisState<A, H, V> entryState,
InterproceduralAnalysis<A, H, V> interprocedural,
AnalysisState<A, H, V> leftState,
AnalysisState<A, H, V> state,
SymbolicExpression left,
AnalysisState<A, H, V> rightState,
SymbolicExpression right)

throws SemanticException {

if (!left.getDynamicType().isArrayType() && !left.getDynamicType().isUntyped())
return entryState.bottom();
return state.bottom();
// it is not possible to detect the correct type of the field without
// resolving it. we rely on the rewriting that will happen inside heap
// domain to translate this into a variable that will have its correct
// type
HeapDereference deref = new HeapDereference(getRuntimeTypes(), left, getLocation());
return rightState.smallStepSemantics(new AccessChild(getRuntimeTypes(), deref, right, getLocation()), this);
return state.smallStepSemantics(new AccessChild(getRuntimeTypes(), deref, right, getLocation()), this);
}
}
13 changes: 3 additions & 10 deletions lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewArray.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,21 +46,14 @@ public IMPNewArray(CFG cfg, String sourceFile, int line, int col, Type type, Exp
public <A extends AbstractState<A, H, V>,
H extends HeapDomain<H>,
V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
AnalysisState<A, H, V> entryState,
InterproceduralAnalysis<A, H, V> interprocedural,
AnalysisState<A, H, V>[] computedStates,
AnalysisState<A, H, V> state,
ExpressionSet<SymbolicExpression>[] params)
throws SemanticException {
// it corresponds to the analysis state after the evaluation of all the
// parameters of this call (the semantics of this call does not need
// information about the intermediate analysis states)
AnalysisState<A, H, V> last = computedStates.length == 0
? entryState
: computedStates[computedStates.length - 1];
HeapAllocation alloc = new HeapAllocation(getRuntimeTypes(), getLocation());
AnalysisState<A, H, V> sem = last.smallStepSemantics(alloc, this);
AnalysisState<A, H, V> sem = state.smallStepSemantics(alloc, this);

AnalysisState<A, H, V> result = entryState.bottom();
AnalysisState<A, H, V> result = state.bottom();
for (SymbolicExpression loc : sem.getComputedExpressions()) {
HeapReference ref = new HeapReference(loc.getTypes(), loc, getLocation());
AnalysisState<A, H, V> refSem = sem.smallStepSemantics(ref, this);
Expand Down
7 changes: 3 additions & 4 deletions lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewObj.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,9 +52,8 @@ public IMPNewObj(CFG cfg, String sourceFile, int line, int col, Type type, Expre
public <A extends AbstractState<A, H, V>,
H extends HeapDomain<H>,
V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
AnalysisState<A, H, V> entryState,
InterproceduralAnalysis<A, H, V> interprocedural,
AnalysisState<A, H, V>[] computedStates,
AnalysisState<A, H, V> state,
ExpressionSet<SymbolicExpression>[] params)
throws SemanticException {
HeapAllocation created = new HeapAllocation(getRuntimeTypes(), getLocation());
Expand All @@ -68,14 +67,14 @@ V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
UnresolvedCall call = new UnresolvedCall(getCFG(), getLocation(),
IMPFrontend.CALL_STRATEGY, true, getStaticType().toString(), fullExpressions);
call.setRuntimeTypes(getRuntimeTypes());
AnalysisState<A, H, V> sem = call.expressionSemantics(entryState, interprocedural, computedStates, fullParams);
AnalysisState<A, H, V> sem = call.expressionSemantics(interprocedural, state, fullParams);

if (!call.getMetaVariables().isEmpty())
sem = sem.forgetIdentifiers(call.getMetaVariables());

sem = sem.smallStepSemantics(created, this);

AnalysisState<A, H, V> result = entryState.bottom();
AnalysisState<A, H, V> result = state.bottom();
for (SymbolicExpression loc : sem.getComputedExpressions())
result = result.lub(sem.smallStepSemantics(new HeapReference(loc.getTypes(), loc, getLocation()), call));

Expand Down
14 changes: 8 additions & 6 deletions lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Assignment.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ public Assignment(CFG cfg, CodeLocation location, Expression target, Expression
* @param cfg the cfg that this statement belongs to
* @param location the location where this statement is defined within the
* program
* @param order the evaluation order of the sub-expressions
* @param target the target of the assignment
* @param expression the expression to assign to {@code target}
*/
Expand All @@ -61,6 +62,7 @@ public Assignment(CFG cfg, CodeLocation location, EvaluationOrder order, Express
* @param cfg the cfg that this statement belongs to
* @param location the location where this statement is defined within the
* program
* @param staticType the static type of this expression
* @param target the target of the assignment
* @param expression the expression to assign to {@code target}
*/
Expand All @@ -75,6 +77,8 @@ public Assignment(CFG cfg, CodeLocation location, Type staticType, Expression ta
* @param cfg the cfg that this statement belongs to
* @param location the location where this statement is defined within the
* program
* @param order the evaluation order of the sub-expressions
* @param staticType the static type of this expression
* @param target the target of the assignment
* @param expression the expression to assign to {@code target}
*/
Expand All @@ -92,13 +96,11 @@ public final String toString() {
protected <A extends AbstractState<A, H, V>,
H extends HeapDomain<H>,
V extends ValueDomain<V>> AnalysisState<A, H, V> binarySemantics(
AnalysisState<A, H, V> entryState,
InterproceduralAnalysis<A, H, V> interprocedural,
AnalysisState<A, H, V> leftState,
SymbolicExpression leftExp,
AnalysisState<A, H, V> rightState,
SymbolicExpression rightExp)
AnalysisState<A, H, V> state,
SymbolicExpression left,
SymbolicExpression right)
throws SemanticException {
return leftState.assign(leftExp, rightExp, this);
return state.assign(left, right, this);
}
}
29 changes: 11 additions & 18 deletions lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/BinaryExpression.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,7 @@ protected BinaryExpression(CFG cfg, CodeLocation location, String constructName,
* the program
* @param constructName the name of the construct represented by this
* expression
* @param order the evaluation order of the sub-expressions
* @param left the first sub-expression of this expression
* @param right the second sub-expression of this expression
*/
Expand All @@ -81,6 +82,7 @@ protected BinaryExpression(CFG cfg, CodeLocation location, String constructName,
* @param location the location where this expression is defined within
* the program
* @param constructName the name of the construct invoked by this expression
* @param order the evaluation order of the sub-expressions
* @param staticType the static type of this expression
* @param left the first sub-expression of this expression
* @param right the second sub-expression of this expression
Expand Down Expand Up @@ -112,17 +114,14 @@ public Expression getRight() {
public final <A extends AbstractState<A, H, V>,
H extends HeapDomain<H>,
V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
AnalysisState<A, H, V> entryState,
InterproceduralAnalysis<A, H, V> interprocedural,
AnalysisState<A, H, V>[] computedStates,
AnalysisState<A, H, V> state,
ExpressionSet<SymbolicExpression>[] params)
throws SemanticException {
AnalysisState<A, H, V> result = entryState.bottom();

AnalysisState<A, H, V> result = state.bottom();
for (SymbolicExpression left : params[0])
for (SymbolicExpression right : params[1])
result = result.lub(binarySemantics(entryState, interprocedural, computedStates[0], left,
computedStates[1], right));
result = result.lub(binarySemantics(interprocedural, state, left, right));

return result;
}
Expand All @@ -135,17 +134,13 @@ V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
* @param <A> the type of {@link AbstractState}
* @param <H> the type of the {@link HeapDomain}
* @param <V> the type of the {@link ValueDomain}
* @param entryState the entry state of this binary expression
* @param interprocedural the interprocedural analysis of the program to
* analyze
* @param leftState the state obtained by evaluating {@code left} in
* {@code entryState}
* @param leftExp the symbolic expression representing the computed
* @param state the state where the expression is to be evaluated
* @param left the symbolic expression representing the computed
* value of the first sub-expression of this
* expression
* @param rightState the state obtained by evaluating {@code right} in
* {@code leftState}
* @param rightExp the symbolic expression representing the computed
* @param right the symbolic expression representing the computed
* value of the second sub-expression of this
* expression
*
Expand All @@ -157,11 +152,9 @@ V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
protected abstract <A extends AbstractState<A, H, V>,
H extends HeapDomain<H>,
V extends ValueDomain<V>> AnalysisState<A, H, V> binarySemantics(
AnalysisState<A, H, V> entryState,
InterproceduralAnalysis<A, H, V> interprocedural,
AnalysisState<A, H, V> leftState,
SymbolicExpression leftExp,
AnalysisState<A, H, V> rightState,
SymbolicExpression rightExp)
AnalysisState<A, H, V> state,
SymbolicExpression left,
SymbolicExpression right)
throws SemanticException;
}
26 changes: 7 additions & 19 deletions lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NaryExpression.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,7 @@ protected NaryExpression(CFG cfg, CodeLocation location, String constructName, E
* the program
* @param constructName the name of the construct represented by this
* expression
* @param order the evaluation order of the sub-expressions
* @param subExpressions the sub-expressions to be evaluated left-to-right
*/
protected NaryExpression(CFG cfg, CodeLocation location, String constructName, EvaluationOrder order,
Expand Down Expand Up @@ -100,6 +101,7 @@ protected NaryExpression(CFG cfg, CodeLocation location, String constructName, T
* the program
* @param constructName the name of the construct represented by this
* expression
* @param order the evaluation order of the sub-expressions
* @param staticType the static type of this expression
* @param subExpressions the sub-expressions to be evaluated left-to-right
*/
Expand Down Expand Up @@ -206,21 +208,17 @@ V extends ValueDomain<V>> AnalysisState<A, H, V> semantics(
StatementStore<A, H, V> expressions)
throws SemanticException {
ExpressionSet<SymbolicExpression>[] computed = new ExpressionSet[subExpressions.length];
AnalysisState<A, H, V>[] subStates = new AnalysisState[subExpressions.length];

order.evaluate(subExpressions, entryState, interprocedural, expressions, computed, subStates);
AnalysisState<A, H, V> result = expressionSemantics(entryState, interprocedural, subStates, computed);
AnalysisState<A, H,
V> eval = order.evaluate(subExpressions, entryState, interprocedural, expressions, computed);
AnalysisState<A, H, V> result = expressionSemantics(interprocedural, eval, computed);

for (Expression sub : subExpressions)
if (!sub.getMetaVariables().isEmpty())
result = result.forgetIdentifiers(sub.getMetaVariables());
return result;
}

protected void evaluateSubExpressions() {

}

/**
* Computes the semantics of the expression, after the semantics of all
* sub-expressions have been computed. Meta variables from the
Expand All @@ -229,18 +227,9 @@ protected void evaluateSubExpressions() {
* @param <A> the type of {@link AbstractState}
* @param <H> the type of the {@link HeapDomain}
* @param <V> the type of the {@link ValueDomain}
* @param entryState the entry state of this call
* @param interprocedural the interprocedural analysis of the program to
* analyze
* @param subStates the array of states chaining the sub-expressions'
* semantics evaluation starting from
* {@code entryState}, namely
* {@code subStates[i]} corresponds to the state
* obtained by the evaluation of
* {@code subExpressions[i]} in the state
* {@code subStates[i-1]}
* ({@code subExpressions[0]} is evaluated in
* {@code entryState})
* @param state the state where the expression is to be evaluated
* @param params the symbolic expressions representing the computed
* values of the sub-expressions of this
* expression
Expand All @@ -253,9 +242,8 @@ protected void evaluateSubExpressions() {
public abstract <A extends AbstractState<A, H, V>,
H extends HeapDomain<H>,
V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
AnalysisState<A, H, V> entryState,
InterproceduralAnalysis<A, H, V> interprocedural,
AnalysisState<A, H, V>[] subStates,
AnalysisState<A, H, V> state,
ExpressionSet<SymbolicExpression>[] params)
throws SemanticException;
}
36 changes: 13 additions & 23 deletions lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/TernaryExpression.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ protected TernaryExpression(CFG cfg, CodeLocation location, String constructName
* the program
* @param constructName the name of the construct represented by this
* expression
* @param order the evaluation order of the sub-expressions
* @param left the first sub-expression of this expression
* @param middle the second sub-expression of this expression
* @param right the third sub-expression of this expression
Expand All @@ -86,6 +87,7 @@ protected TernaryExpression(CFG cfg, CodeLocation location, String constructName
* the program
* @param constructName the name of the construct represented by this
* expression
* @param order the evaluation order of the sub-expressions
* @param staticType the static type of this expression
* @param left the first sub-expression of this expression
* @param middle the second sub-expression of this expression
Expand Down Expand Up @@ -127,18 +129,15 @@ public Expression getRight() {
public final <A extends AbstractState<A, H, V>,
H extends HeapDomain<H>,
V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
AnalysisState<A, H, V> entryState,
InterproceduralAnalysis<A, H, V> interprocedural,
AnalysisState<A, H, V>[] computedStates,
AnalysisState<A, H, V> state,
ExpressionSet<SymbolicExpression>[] params)
throws SemanticException {
AnalysisState<A, H, V> result = entryState.bottom();

AnalysisState<A, H, V> result = state.bottom();
for (SymbolicExpression left : params[0])
for (SymbolicExpression middle : params[1])
for (SymbolicExpression right : params[2])
result = result.lub(ternarySemantics(entryState, interprocedural, computedStates[0], left,
computedStates[1], middle, computedStates[2], right));
result = result.lub(ternarySemantics(interprocedural, state, left, middle, right));

return result;
}
Expand All @@ -151,22 +150,16 @@ V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
* @param <A> the type of {@link AbstractState}
* @param <H> the type of the {@link HeapDomain}
* @param <V> the type of the {@link ValueDomain}
* @param entryState the entry state of this binary expression
* @param interprocedural the interprocedural analysis of the program to
* analyze
* @param leftState the state obtained by evaluating {@code left} in
* {@code entryState}
* @param leftExp the symbolic expression representing the computed
* @param state the state where the expression is to be evaluated
* @param left the symbolic expression representing the computed
* value of the first sub-expression of this
* expression
* @param middleState the state obtained by evaluating {@code middle} in
* {@code leftState}
* @param middleExp the symbolic expression representing the computed
* @param middle the symbolic expression representing the computed
* value of the second sub-expression of this
* expression
* @param rightState the state obtained by evaluating {@code right} in
* {@code middleState}
* @param rightExp the symbolic expression representing the computed
* @param right the symbolic expression representing the computed
* value of the third sub-expression of this
* expression
*
Expand All @@ -178,13 +171,10 @@ V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
protected abstract <A extends AbstractState<A, H, V>,
H extends HeapDomain<H>,
V extends ValueDomain<V>> AnalysisState<A, H, V> ternarySemantics(
AnalysisState<A, H, V> entryState,
InterproceduralAnalysis<A, H, V> interprocedural,
AnalysisState<A, H, V> leftState,
SymbolicExpression leftExp,
AnalysisState<A, H, V> middleState,
SymbolicExpression middleExp,
AnalysisState<A, H, V> rightState,
SymbolicExpression rightExp)
AnalysisState<A, H, V> state,
SymbolicExpression left,
SymbolicExpression middle,
SymbolicExpression right)
throws SemanticException;
}
Loading

0 comments on commit b7ced68

Please sign in to comment.