Skip to content

Commit 9d2708d

Browse files
olivierilucaolivieriluca
committed
Bug fixing
1 parent fd965c8 commit 9d2708d

File tree

12 files changed

+88
-59
lines changed

12 files changed

+88
-59
lines changed

‎go-lisa/src/main/java/it/unive/golisa/cfg/expression/GoCollectionAccess.java‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -65,18 +65,18 @@ public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(Interpro
6565
AnalysisState<A> state, SymbolicExpression left, SymbolicExpression right, StatementStore<A> expressions)
6666
throws SemanticException {
6767
AnalysisState<A> result = state.bottom();
68-
Set<Type> ltypes = state.getState().getRuntimeTypesOf(left, this, state.getState());
69-
for (Type type : ltypes) {
70-
if (type.isPointerType()
71-
|| type instanceof GoStructType) {
68+
//Set<Type> ltypes = state.getState().getRuntimeTypesOf(left, this, state.getState());
69+
//for (Type type : ltypes) {
70+
// if (type.isPointerType()
71+
// || type instanceof GoStructType) {
7272

7373

7474
result = result.lub(state.smallStepSemantics(
7575
new AccessChild(Untyped.INSTANCE,
7676
new HeapDereference(getStaticType(), left, getLocation()), right, getLocation()),
7777
this));
78-
}
79-
}
78+
// }
79+
//}
8080

8181
return result;
8282
}

‎go-lisa/src/main/java/it/unive/golisa/cfg/expression/binary/GoEqual.java‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -56,18 +56,18 @@ left, right, ComparisonEq.INSTANCE, getLocation()),
5656
Set<Type> ltypes = state.getState().getRuntimeTypesOf(left, this, state.getState());
5757
Set<Type> rtypes = state.getState().getRuntimeTypesOf(right, this, state.getState());
5858

59-
for (Type leftType : ltypes)
60-
for (Type rightType : rtypes)
59+
//for (Type leftType : ltypes)
60+
// for (Type rightType : rtypes)
6161

62-
if (rightType.canBeAssignedTo(leftType) || leftType.canBeAssignedTo(rightType)) {
62+
// if (rightType.canBeAssignedTo(leftType) || leftType.canBeAssignedTo(rightType)) {
6363
// TODO: not covering composite types (e.g., channels,
6464
// arrays, structs...)
6565
AnalysisState<A> tmp = state
6666
.smallStepSemantics(new BinaryExpression(GoBoolType.INSTANCE,
6767
left, right,
6868
ComparisonEq.INSTANCE, getLocation()), this);
6969
result = result.lub(tmp);
70-
}
70+
// }
7171
return result;
7272
}
7373
}

‎go-lisa/src/main/java/it/unive/golisa/cfg/expression/binary/GoGreater.java‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,9 @@ public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(Interpro
5151
// following the Golang specification:
5252
// in any comparison, the first operand must be assignable to the type
5353
// of the second operand, or vice versa.
54-
for (Type leftType : ltypes)
55-
for (Type rightType : rtypes) {
56-
if (leftType.canBeAssignedTo(rightType) || rightType.canBeAssignedTo(leftType)) {
54+
//for (Type leftType : ltypes)
55+
// for (Type rightType : rtypes) {
56+
// if (leftType.canBeAssignedTo(rightType) || rightType.canBeAssignedTo(leftType)) {
5757
// TODO: only, integer, floating point values, strings are
5858
// ordered
5959
// but missing lexicographical string order in LiSA
@@ -64,8 +64,8 @@ left, right, ComparisonGt.INSTANCE, getLocation()),
6464

6565
this);
6666
result = result.lub(tmp);
67-
}
68-
}
67+
// }
68+
// }
6969
return result;
7070
}
7171
}

‎go-lisa/src/main/java/it/unive/golisa/cfg/expression/binary/GoGreaterOrEqual.java‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,9 @@ public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(Interpro
5151
// following the Golang specification:
5252
// in any comparison, the first operand must be assignable to the type
5353
// of the second operand, or vice versa.
54-
for (Type leftType : ltypes)
55-
for (Type rightType : rtypes) {
56-
if (leftType.canBeAssignedTo(rightType) || rightType.canBeAssignedTo(leftType)) {
54+
//for (Type leftType : ltypes)
55+
// for (Type rightType : rtypes) {
56+
// if (leftType.canBeAssignedTo(rightType) || rightType.canBeAssignedTo(leftType)) {
5757
// TODO: only, integer, floating point values, strings are
5858
// ordered
5959
// but missing lexicographical string order in LiSA
@@ -63,8 +63,8 @@ public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(Interpro
6363
left, right, ComparisonGe.INSTANCE, getLocation()),
6464
this);
6565
result = result.lub(tmp);
66-
}
67-
}
66+
// }
67+
// }
6868
return result;
6969
}
7070
}

‎go-lisa/src/main/java/it/unive/golisa/cfg/expression/binary/GoLess.java‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -50,15 +50,16 @@ public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(Interpro
5050
Set<Type> rtypes = state.getState().getRuntimeTypesOf(right, this, state.getState());
5151

5252
AnalysisState<A> result = state.bottom();
53-
for (Type lType : ltypes)
54-
for (Type rType : rtypes) {
55-
if (lType.canBeAssignedTo(rType) || rType.canBeAssignedTo(lType))
53+
54+
// for (Type lType : ltypes)
55+
// for (Type rType : rtypes) {
56+
// if (lType.canBeAssignedTo(rType) || rType.canBeAssignedTo(lType))
5657
result = result.lub(state
5758
.smallStepSemantics(
5859
new BinaryExpression(GoBoolType.INSTANCE,
5960
left, right, ComparisonLt.INSTANCE, getLocation()),
6061
this));
61-
}
62+
// }
6263
return result;
6364
}
6465
}

‎go-lisa/src/main/java/it/unive/golisa/cfg/expression/binary/GoLessOrEqual.java‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -52,9 +52,9 @@ public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(Interpro
5252
// following the Golang specification:
5353
// in any comparison, the first operand must be assignable to the type
5454
// of the second operand, or vice versa.
55-
for (Type leftType : ltypes)
56-
for (Type rightType : rtypes) {
57-
if (leftType.canBeAssignedTo(rightType) || rightType.canBeAssignedTo(leftType)) {
55+
//for (Type leftType : ltypes)
56+
// for (Type rightType : rtypes) {
57+
// if (leftType.canBeAssignedTo(rightType) || rightType.canBeAssignedTo(leftType)) {
5858
// TODO: only, integer, floating point values, strings are
5959
// ordered
6060
// but missing lexicographical string order in LiSA
@@ -64,8 +64,8 @@ public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(Interpro
6464
left, right, ComparisonLe.INSTANCE, getLocation()),
6565
this);
6666
result = result.lub(tmp);
67-
}
68-
}
67+
// }
68+
// }
6969
return result;
7070
}
7171
}

‎go-lisa/src/main/java/it/unive/golisa/cfg/expression/binary/GoNotEqual.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -56,9 +56,9 @@ public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(Interpro
5656

5757
// TODO: composite types are not covered yey
5858
AnalysisState<A> result = state.bottom();
59-
for (Type lType : ltypes)
60-
for (Type rType : rtypes)
61-
if (rType.canBeAssignedTo(lType) || lType.canBeAssignedTo(rType))
59+
//for (Type lType : ltypes)
60+
// for (Type rType : rtypes)
61+
// if (rType.canBeAssignedTo(lType) || lType.canBeAssignedTo(rType))
6262
result = result.lub(state
6363
.smallStepSemantics(new BinaryExpression(GoBoolType.INSTANCE,
6464
left, right,

‎go-lisa/src/main/java/it/unive/golisa/cfg/type/composite/GoStructType.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -208,7 +208,7 @@ public Expression defaultValue(CFG cfg, CodeLocation location) {
208208
if (key.getStaticType() instanceof ReferenceType)
209209
values[i++] = new GoUnknown(cfg, location);
210210
else
211-
values[i++] = key.getStaticType().defaultValue(cfg, location);
211+
values[i++] = key.getStaticType().defaultValue(cfg, location) == null ? new GoUnknown(cfg, location) : key.getStaticType().defaultValue(cfg, location);
212212

213213
return new GoNonKeyedLiteral(cfg, location, values, this);
214214
}

‎go-lisa/src/main/java/it/unive/golisa/checker/hf/CchiUtils.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,7 @@ public static boolean isContractName(String contractName, Tarsis t) {
9898

9999
public static boolean mayCrossChannel(String channelName, Tarsis t) {
100100
return containsApproximations(t)
101-
|| !isNameChannel(channelName,t);
101+
|| (channelName != null && !isNameChannel(channelName,t));
102102
}
103103

104104
private static boolean containsApproximations(Tarsis t) {

‎go-lisa/src/main/java/it/unive/golisa/checker/hf/CrossChannelInvocationsIssuesChecker.java‎

Lines changed: 42 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@
3636
import java.util.Iterator;
3737
import java.util.List;
3838
import java.util.Map;
39+
import java.util.Map.Entry;
3940
import java.util.Set;
4041

4142
import org.apache.commons.lang3.tuple.Pair;
@@ -107,32 +108,33 @@ public void afterExecution(
107108
}
108109

109110
//CASE 2: CCIs with different channels
110-
Set<Pair<Statement,Statement>> multipleCrossChannelInvocations = new HashSet<>();
111-
112-
boolean isDiff = false;
111+
Map<Statement, Set<Statement>> multipleCrossChannelInvocations = new HashMap<>();
113112
for (int i = 0; i < invocations.length - 1; i++) {
114113
for (int j = i + 1; j < invocations.length; j++) {
114+
boolean isDiff = false;
115115
Set<Tarsis> t1Set = crossContractInvocations.get(invocations[i]).getChannelApproximations();
116116
Set<Tarsis> t2Set = crossContractInvocations.get(invocations[j]).getChannelApproximations();
117117
for (Tarsis t1 : t1Set) {
118118
for (Tarsis t2 : t2Set) {
119-
if (t1.isTop() || t2.isTop()
120-
|| !TarsisUtils.possibleEqualsMatch(t1, t2)
121-
|| (TarsisUtils.extractValueStringFromTarsisStates(t1) != null
119+
if(!t1.isTop() && !t2.isTop()
120+
&& (TarsisUtils.possibleEqualsMatch(t1, t2) || (TarsisUtils.extractValueStringFromTarsisStates(t1) != null
122121
&& TarsisUtils.extractValueStringFromTarsisStates(t2) != null &&
123-
!TarsisUtils.extractValueStringFromTarsisStates(t1)
124-
.equals(TarsisUtils.extractValueStringFromTarsisStates(t2)))) {
125-
isDiff = true;
126-
break;
127-
}
122+
TarsisUtils.extractValueStringFromTarsisStates(t1)
123+
.equals(TarsisUtils.extractValueStringFromTarsisStates(t2)))))
124+
continue;
125+
isDiff = true;
126+
break;
127+
128128
}
129129
if (isDiff)
130130
break;
131131
}
132132

133133
if (isDiff) {
134-
if(!multipleCrossChannelInvocations.contains(Pair.of(invocations[j], invocations[i])))
135-
multipleCrossChannelInvocations.add(Pair.of(invocations[i], invocations[j]));
134+
if(!multipleCrossChannelInvocations.containsKey(invocations[i]))
135+
multipleCrossChannelInvocations.put(invocations[i], new HashSet<>());
136+
multipleCrossChannelInvocations.get(invocations[i]).add(invocations[j]);
137+
136138
if(!crossChannelInvocations.containsKey(invocations[i]))
137139
crossChannelInvocations.put(invocations[i], new CrossContractInvocationInformation());
138140
crossChannelInvocations.get(invocations[i]).addAllChannelApproximations(crossContractInvocations.get(invocations[i]).getChannelApproximations());
@@ -146,15 +148,9 @@ public void afterExecution(
146148
}
147149
}
148150

149-
Map<Statement, Set<Statement>> results = new HashMap<>();
150-
for( Pair<Statement, Statement> cchs : multipleCrossChannelInvocations) {
151-
if(!results.containsKey(cchs.getLeft()))
152-
results.put(cchs.getLeft(), new HashSet<>());
153-
results.get(cchs.getLeft()).add(cchs.getRight());
154-
}
155-
156-
for(Statement target : results.keySet()) {
157-
Set<Statement> others = results.get(target);
151+
Map<Statement, Set<Statement>> result = reduceForWarnings(multipleCrossChannelInvocations);
152+
for(Statement target : result.keySet()) {
153+
Set<Statement> others = result.get(target);
158154
tool.warnOn(target,
159155
"Detected cross-channel invocations on different channels. The other invocations: "
160156
+ printOtherLocations(others) + ". They may lead to a lack of transparency because no new transactions are created during the invocation.");
@@ -165,6 +161,28 @@ public void afterExecution(
165161
}
166162
}
167163

164+
private Map<Statement, Set<Statement>> reduceForWarnings(
165+
Map<Statement, Set<Statement>> multipleCrossChannelInvocations) {
166+
Set<Pair<Statement, Statement>> tmp = new HashSet<>();
167+
168+
for(Entry<Statement, Set<Statement>> entry :multipleCrossChannelInvocations.entrySet()) {
169+
Statement cci1 = entry.getKey();
170+
for(Statement cci2 :entry.getValue()) {
171+
if(!tmp.contains(Pair.of(cci1, cci2)) && !tmp.contains(Pair.of(cci2, cci1)))
172+
tmp.add(Pair.of(cci1, cci2));
173+
}
174+
}
175+
176+
Map<Statement, Set<Statement>> result = new HashMap<>();
177+
for(Pair<Statement, Statement> pair : tmp) {
178+
if(!result.containsKey(pair.getLeft()))
179+
result.put(pair.getLeft(), new HashSet<>());
180+
result.get(pair.getLeft()).add(pair.getRight());
181+
}
182+
183+
return result;
184+
}
185+
168186
private String printOtherLocations(Set<Statement> others) {
169187
String result = "";
170188
Iterator<Statement> iter = others.iterator();
@@ -285,7 +303,8 @@ private Set<Tarsis> extractChannelValues(Call call, int parametersLength, Statem
285303
.getAnalysisStateAfter(call.getParameters()[par]);
286304
for (SymbolicExpression stack : state.getState().rewrite(state.getComputedExpressions(), node,
287305
state.getState())) {
288-
res.add(state.getState().getValueState().eval((ValueExpression) stack, node, state.getState()));
306+
Tarsis value = state.getState().getValueState().eval((ValueExpression) stack, node, state.getState());
307+
res.add(value);
289308
}
290309
}
291310

0 commit comments

Comments
 (0)