Skip to content

Commit c65df8d

Browse files
olivierilucaolivieriluca
committed
Fixing null pointer and array index out of bound exceptions
1 parent 9bb5eff commit c65df8d

File tree

4 files changed

+93
-40
lines changed

4 files changed

+93
-40
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -190,7 +190,7 @@ public <A extends AbstractState<A>> AnalysisState<A> forwardSemanticsAux(Interpr
190190
AnalysisState<A> tmp = containerState;
191191

192192
for (int i = 0; i < keys.length; i++) {
193-
Type fieldType = structUnit.getInstanceGlobal(((VariableRef) keys[i]).getName(), true)
193+
Type fieldType = structUnit.getInstanceGlobal(((VariableRef) keys[i]).getName(), true) == null ? Untyped.INSTANCE : structUnit.getInstanceGlobal(((VariableRef) keys[i]).getName(), true)
194194
.getStaticType();
195195
Variable field = getVariable((VariableRef) keys[i]);
196196
AccessChild access = new AccessChild(fieldType, dereference, field, getLocation());
@@ -269,4 +269,4 @@ public <A extends AbstractState<A>> AnalysisState<A> forwardSemanticsAux(Interpr
269269
return state.top().smallStepSemantics(new PushAny(type, getLocation()), this);
270270

271271
}
272-
}
272+
}

‎go-lisa/src/main/java/it/unive/golisa/cfg/runtime/fmt/Printf.java‎

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -7,18 +7,18 @@
77
import it.unive.lisa.analysis.AnalysisState;
88
import it.unive.lisa.analysis.SemanticException;
99
import it.unive.lisa.analysis.StatementStore;
10+
import it.unive.lisa.analysis.lattices.ExpressionSet;
1011
import it.unive.lisa.interprocedural.InterproceduralAnalysis;
1112
import it.unive.lisa.program.CodeUnit;
1213
import it.unive.lisa.program.cfg.CFG;
1314
import it.unive.lisa.program.cfg.CodeLocation;
1415
import it.unive.lisa.program.cfg.CodeMemberDescriptor;
1516
import it.unive.lisa.program.cfg.NativeCFG;
1617
import it.unive.lisa.program.cfg.Parameter;
17-
import it.unive.lisa.program.cfg.statement.BinaryExpression;
1818
import it.unive.lisa.program.cfg.statement.Expression;
19+
import it.unive.lisa.program.cfg.statement.NaryExpression;
1920
import it.unive.lisa.program.cfg.statement.PluggableStatement;
2021
import it.unive.lisa.program.cfg.statement.Statement;
21-
import it.unive.lisa.symbolic.SymbolicExpression;
2222
import it.unive.lisa.symbolic.value.PushAny;
2323
import it.unive.lisa.type.Untyped;
2424

@@ -39,15 +39,15 @@ public Printf(CodeLocation location, CodeUnit fmtUnit) {
3939
super(new CodeMemberDescriptor(location, fmtUnit, false, "Printf", GoStringType.INSTANCE,
4040
new Parameter(location, "format", GoStringType.INSTANCE),
4141
new VarArgsParameter(location, "a", GoSliceType.lookup(Untyped.INSTANCE))),
42-
SprintfImpl.class);
42+
PrintfImpl.class);
4343
}
4444

4545
/**
4646
* The {@link Printf} implementation.
4747
*
4848
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
4949
*/
50-
public static class SprintfImpl extends BinaryExpression implements PluggableStatement {
50+
public static class PrintfImpl extends NaryExpression implements PluggableStatement {
5151

5252
private Statement original;
5353

@@ -71,8 +71,11 @@ protected int compareSameClassAndParams(Statement o) {
7171
*
7272
* @return the pluggable statement
7373
*/
74-
public static SprintfImpl build(CFG cfg, CodeLocation location, Expression... params) {
75-
return new SprintfImpl(cfg, location, params[0], params[1]);
74+
public static PrintfImpl build(CFG cfg, CodeLocation location, Expression... params) {
75+
if(params.length > 1)
76+
return new PrintfImpl(cfg, location, params);
77+
else
78+
return new PrintfImpl(cfg, location, params[0]);
7679
}
7780

7881
/**
@@ -81,21 +84,18 @@ public static SprintfImpl build(CFG cfg, CodeLocation location, Expression... pa
8184
* @param cfg the {@link CFG} where this pluggable statement lies
8285
* @param location the location where this pluggable statement is
8386
* defined
84-
* @param left the left expression
85-
* @param right the right expression
87+
* @param params the param expressions
8688
*/
87-
public SprintfImpl(CFG cfg, CodeLocation location, Expression left, Expression right) {
88-
super(cfg, location, "Printf", GoStringType.INSTANCE, left, right);
89+
public PrintfImpl(CFG cfg, CodeLocation location, Expression... params) {
90+
super(cfg, location, "Printf", GoStringType.INSTANCE, params);
8991
}
9092

9193
@Override
92-
public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
93-
InterproceduralAnalysis<A> interprocedural,
94-
AnalysisState<A> state,
95-
SymbolicExpression left,
96-
SymbolicExpression right,
94+
public <A extends AbstractState<A>> AnalysisState<A> forwardSemanticsAux(
95+
InterproceduralAnalysis<A> interprocedural, AnalysisState<A> state, ExpressionSet[] params,
9796
StatementStore<A> expressions) throws SemanticException {
9897
return state.smallStepSemantics(new PushAny(GoStringType.INSTANCE, getLocation()), original);
98+
9999
}
100100
}
101-
}
101+
}

‎go-lisa/src/main/java/it/unive/golisa/cfg/runtime/fmt/Println.java‎

Lines changed: 16 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,17 @@
66
import it.unive.lisa.analysis.AnalysisState;
77
import it.unive.lisa.analysis.SemanticException;
88
import it.unive.lisa.analysis.StatementStore;
9+
import it.unive.lisa.analysis.lattices.ExpressionSet;
910
import it.unive.lisa.interprocedural.InterproceduralAnalysis;
1011
import it.unive.lisa.program.CodeUnit;
1112
import it.unive.lisa.program.cfg.CFG;
1213
import it.unive.lisa.program.cfg.CodeLocation;
1314
import it.unive.lisa.program.cfg.CodeMemberDescriptor;
1415
import it.unive.lisa.program.cfg.NativeCFG;
1516
import it.unive.lisa.program.cfg.statement.Expression;
17+
import it.unive.lisa.program.cfg.statement.NaryExpression;
1618
import it.unive.lisa.program.cfg.statement.PluggableStatement;
1719
import it.unive.lisa.program.cfg.statement.Statement;
18-
import it.unive.lisa.program.cfg.statement.UnaryExpression;
1920
import it.unive.lisa.symbolic.SymbolicExpression;
2021
import it.unive.lisa.type.Untyped;
2122

@@ -43,7 +44,7 @@ public Println(CodeLocation location, CodeUnit fmtUnit) {
4344
*
4445
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
4546
*/
46-
public static class PrintlnImpl extends UnaryExpression implements PluggableStatement {
47+
public static class PrintlnImpl extends NaryExpression implements PluggableStatement {
4748

4849
private Statement original;
4950

@@ -83,11 +84,19 @@ public PrintlnImpl(CFG cfg, CodeLocation location, Expression arg) {
8384
super(cfg, location, "Println", Untyped.INSTANCE, arg);
8485
}
8586

87+
8688
@Override
87-
public <A extends AbstractState<A>> AnalysisState<A> fwdUnarySemantics(
88-
InterproceduralAnalysis<A> interprocedural, AnalysisState<A> state,
89-
SymbolicExpression expr, StatementStore<A> expressions) throws SemanticException {
90-
return state.smallStepSemantics(expr, original);
89+
public <A extends AbstractState<A>> AnalysisState<A> forwardSemanticsAux(
90+
InterproceduralAnalysis<A> interprocedural, AnalysisState<A> state, ExpressionSet[] params,
91+
StatementStore<A> expressions) throws SemanticException {
92+
93+
AnalysisState<A> res = state.bottom();
94+
95+
for(ExpressionSet p : params)
96+
for(SymbolicExpression e : p)
97+
res = res.lub(state.smallStepSemantics(e, original));
98+
99+
return res;
91100
}
92101
}
93-
}
102+
}

‎go-lisa/src/main/java/it/unive/golisa/cfg/runtime/fmt/Sprintf.java‎

Lines changed: 59 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,32 @@
11
package it.unive.golisa.cfg.runtime.fmt;
22

3+
import java.util.Set;
4+
35
import it.unive.golisa.cfg.VarArgsParameter;
46
import it.unive.golisa.cfg.type.GoStringType;
57
import it.unive.golisa.cfg.type.composite.GoSliceType;
68
import it.unive.lisa.analysis.AbstractState;
79
import it.unive.lisa.analysis.AnalysisState;
810
import it.unive.lisa.analysis.SemanticException;
911
import it.unive.lisa.analysis.StatementStore;
12+
import it.unive.lisa.analysis.lattices.ExpressionSet;
1013
import it.unive.lisa.interprocedural.InterproceduralAnalysis;
1114
import it.unive.lisa.program.CodeUnit;
1215
import it.unive.lisa.program.cfg.CFG;
1316
import it.unive.lisa.program.cfg.CodeLocation;
1417
import it.unive.lisa.program.cfg.CodeMemberDescriptor;
1518
import it.unive.lisa.program.cfg.NativeCFG;
1619
import it.unive.lisa.program.cfg.Parameter;
17-
import it.unive.lisa.program.cfg.statement.BinaryExpression;
1820
import it.unive.lisa.program.cfg.statement.Expression;
21+
import it.unive.lisa.program.cfg.statement.NaryExpression;
1922
import it.unive.lisa.program.cfg.statement.PluggableStatement;
2023
import it.unive.lisa.program.cfg.statement.Statement;
2124
import it.unive.lisa.symbolic.SymbolicExpression;
2225
import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
26+
import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator;
2327
import it.unive.lisa.type.Type;
2428
import it.unive.lisa.type.TypeSystem;
2529
import it.unive.lisa.type.Untyped;
26-
import java.util.Set;
2730

2831
/**
2932
* func Sprintf(format string, a ...any) string.
@@ -50,7 +53,7 @@ public Sprintf(CodeLocation location, CodeUnit fmtUnit) {
5053
*
5154
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
5255
*/
53-
public static class SprintfImpl extends BinaryExpression implements PluggableStatement {
56+
public static class SprintfImpl extends NaryExpression implements PluggableStatement {
5457

5558
private Statement original;
5659

@@ -75,7 +78,7 @@ protected int compareSameClassAndParams(Statement o) {
7578
* @return the pluggable statement
7679
*/
7780
public static SprintfImpl build(CFG cfg, CodeLocation location, Expression... params) {
78-
return new SprintfImpl(cfg, location, params[0], params[1]);
81+
return new SprintfImpl(cfg, location, params);
7982
}
8083

8184
/**
@@ -87,20 +90,35 @@ public static SprintfImpl build(CFG cfg, CodeLocation location, Expression... pa
8790
* @param left the left expression
8891
* @param right the right expression
8992
*/
90-
public SprintfImpl(CFG cfg, CodeLocation location, Expression left, Expression right) {
91-
super(cfg, location, "Sprintf", GoStringType.INSTANCE, left, right);
93+
public SprintfImpl(CFG cfg, CodeLocation location, Expression[] exprs) {
94+
super(cfg, location, "Sprintf", GoStringType.INSTANCE, exprs);
9295
}
9396

97+
9498
@Override
95-
public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
96-
InterproceduralAnalysis<A> interprocedural,
97-
AnalysisState<A> state,
98-
SymbolicExpression left,
99-
SymbolicExpression right,
99+
public <A extends AbstractState<A>> AnalysisState<A> forwardSemanticsAux(
100+
InterproceduralAnalysis<A> interprocedural, AnalysisState<A> state, ExpressionSet[] params,
100101
StatementStore<A> expressions) throws SemanticException {
101-
102-
return state.smallStepSemantics(new it.unive.lisa.symbolic.value.BinaryExpression(getStaticType(), left,
103-
right, SprintfOperator.INSTANCE, getLocation()), original);
102+
103+
ExpressionSet p1 = params[0];
104+
AnalysisState<A> res = state.bottom();
105+
106+
if(params.length > 1) {
107+
for(SymbolicExpression e1 : p1) {
108+
for(int i = 1; i< params.length; i++)
109+
for(SymbolicExpression e2 : params[i])
110+
res = res.lub(state.smallStepSemantics(new it.unive.lisa.symbolic.value.BinaryExpression(getStaticType(), e1,
111+
e2, SprintfOperator.INSTANCE, getLocation()), original));
112+
}
113+
} else {
114+
for(SymbolicExpression e1 : p1) {
115+
res = res.lub(state.smallStepSemantics(new it.unive.lisa.symbolic.value.UnaryExpression(getStaticType(),
116+
e1, (UnaryOperator) SprintfOperatorUnary.INSTANCE, getLocation()), original));
117+
}
118+
}
119+
120+
return res;
121+
104122
}
105123
}
106124

@@ -129,4 +147,30 @@ public Set<Type> typeInference(TypeSystem types, Set<Type> left, Set<Type> right
129147
return Set.of(types.getStringType());
130148
}
131149
}
132-
}
150+
151+
/**
152+
* The Sprintf operator.
153+
*
154+
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
155+
*/
156+
public static class SprintfOperatorUnary implements UnaryOperator {
157+
158+
/**
159+
* The singleton instance of this class.
160+
*/
161+
public static final SprintfOperator INSTANCE = new SprintfOperator();
162+
163+
private SprintfOperatorUnary() {
164+
}
165+
166+
@Override
167+
public String toString() {
168+
return "SprintfOperatorUnary";
169+
}
170+
171+
@Override
172+
public Set<Type> typeInference(TypeSystem types, Set<Type> argument) {
173+
return Set.of(types.getStringType());
174+
}
175+
}
176+
}

0 commit comments

Comments
 (0)