Skip to content

Commit 06ef1d9

Browse files
committed
Improving ABCIPanicChecker
1 parent 406cfff commit 06ef1d9

File tree

1 file changed

+76
-8
lines changed

1 file changed

+76
-8
lines changed

go-lisa/src/main/java/it/unive/golisa/checker/cosmos/panic/ABCIPanicChecker.java

Lines changed: 76 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22

33
import java.util.Collection;
44
import java.util.HashSet;
5+
import java.util.Map;
56
import java.util.Set;
67

78
import it.unive.golisa.analysis.DummyDomain;
@@ -19,6 +20,10 @@
1920
import it.unive.golisa.checker.utils.graph.edges.LabeledEdge;
2021
import it.unive.golisa.checker.utils.graph.edges.StandardEdge;
2122
import it.unive.golisa.checker.utils.graph.nodes.StandardNode;
23+
import it.unive.golisa.golang.api.signature.FuncGoLangApiSignature;
24+
import it.unive.golisa.golang.api.signature.GoLangApiSignature;
25+
import it.unive.golisa.golang.api.signature.MethodGoLangApiSignature;
26+
import it.unive.golisa.golang.util.GoLangUtils;
2227
import it.unive.lisa.analysis.SimpleAbstractState;
2328
import it.unive.lisa.analysis.heap.pointbased.PointBasedHeap;
2429
import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment;
@@ -31,8 +36,10 @@
3136
import it.unive.lisa.program.cfg.CodeMemberDescriptor;
3237
import it.unive.lisa.program.cfg.statement.Expression;
3338
import it.unive.lisa.program.cfg.statement.Statement;
39+
import it.unive.lisa.program.cfg.statement.VariableRef;
3440
import it.unive.lisa.program.cfg.statement.call.CFGCall;
3541
import it.unive.lisa.program.cfg.statement.call.Call;
42+
import it.unive.lisa.program.cfg.statement.call.UnresolvedCall;
3643

3744
/**
3845
* Unhandled errors Checker in Hyperledger Fabric.
@@ -67,8 +74,9 @@ public boolean visit(
6774
tool.warnOn(node, "Detected panic within a critical execution " + printComponents
6875
+ ". There is at least an execution path without a recovery function.");
6976
} else {
70-
tool.warnOn(node, "Detected panic within a critical execution " + printComponents
71-
+ ". Ensure that all the possible recovery functions properly handle the panic exception.");
77+
if(existPossibleRecoveryDefer(panicGraphWithRecoveries))
78+
tool.warnOn(node, "Detected panic within a critical execution " + printComponents
79+
+ ". Ensure that all the possible recovery functions properly handle the panic exception.");
7280
}
7381
}
7482

@@ -119,17 +127,17 @@ private void computePossibleRecoveryDefersRecursive(GraphForCheckers graphWithRe
119127
StandardNode stNode = graphWithRecovery.getNodeFromStatement(st);
120128
for(Statement n : st.getCFG().getNodes()) {
121129
if(!n.equals(st) && n instanceof GoDefer) {
122-
boolean add = st instanceof GoDefer ? CFGUtils.existPath(st.getCFG(), st, (GoDefer) n, Search.BFS) : CFGUtils.existPath(st.getCFG(), n, st, Search.BFS);
130+
boolean isCandidate = st instanceof GoDefer ? CFGUtils.existPath(st.getCFG(), st, (GoDefer) n, Search.BFS) : CFGUtils.existPath(st.getCFG(), n, st, Search.BFS);
123131

124-
if(add) {
132+
if(isCandidate && maybeRecovery((GoDefer) n)) {
125133
StandardNode recovery = hasExplicitRecovery((GoDefer) n, tool) ? new RecoveryNode(graphWithRecovery, (GoDefer) n) : new PossileRecoveryNode(graphWithRecovery, (GoDefer) n);
126134
graphWithRecovery.addNode(recovery);
127-
graphWithRecovery.addEdge(new StandardEdge(recovery, stNode));
128135
Collection<LabeledEdge> edgesToRemove = graphWithRecovery.getIngoingEdges(stNode);
129136
for( LabeledEdge e : edgesToRemove) {
130137
graphWithRecovery.addEdge(e.newInstance(e.getSource(), recovery));
131-
graphWithRecovery.getEdges().remove(e);
138+
graphWithRecovery.getNodeList().removeEdge(e);
132139
}
140+
graphWithRecovery.addEdge(new StandardEdge(recovery, stNode));
133141
}
134142
}
135143

@@ -140,9 +148,66 @@ private void computePossibleRecoveryDefersRecursive(GraphForCheckers graphWithRe
140148
for(LabeledEdge e : ingoingEdges) {
141149

142150
computePossibleRecoveryDefersRecursive(graphWithRecovery, e.getSource().getStatement(), tool, new HashSet<>(seen));
151+
143152
}
144153
}
145154

155+
private boolean maybeRecovery(GoDefer defer) {
156+
Expression expr = defer.getSubExpression();
157+
if(expr instanceof CFGCall) {
158+
CFGCall call = (CFGCall) expr;
159+
return call.getTargetedCFGs().stream().anyMatch(cfg -> cfg.getNodes().stream().anyMatch(n -> CFGUtils.matchNodeOrSubExpressions(n, st -> st instanceof GoRecover)));
160+
} else if(expr instanceof UnresolvedCall) {
161+
//TODO:add possible saniteizer list
162+
163+
if(!matchAnyGoAPIMethodOrFunctionSignatures((UnresolvedCall) expr))
164+
return true;
165+
}
166+
return false;
167+
}
168+
169+
170+
private boolean matchAnyGoAPIMethodOrFunctionSignatures(UnresolvedCall call) {
171+
Map<String, Set<FuncGoLangApiSignature>> mapf = GoLangUtils.getGoLangApiFunctionSignatures();
172+
Map<String, Set<MethodGoLangApiSignature>> mapm = GoLangUtils.getGoLangApiMethodSignatures();
173+
174+
for(String pckg : mapf.keySet())
175+
for(FuncGoLangApiSignature f : mapf.get(pckg))
176+
if(matchSignature(f, call))
177+
return true;
178+
179+
for(String pckg : mapm.keySet())
180+
for(MethodGoLangApiSignature m : mapm.get(pckg))
181+
if(matchSignature(m, call))
182+
return true;
183+
184+
return false;
185+
}
186+
187+
private boolean matchSignature(GoLangApiSignature goLangApiSignature, UnresolvedCall call) {
188+
189+
String signatureName = null;
190+
if (goLangApiSignature instanceof FuncGoLangApiSignature)
191+
signatureName = ((FuncGoLangApiSignature) goLangApiSignature).getName();
192+
else if (goLangApiSignature instanceof MethodGoLangApiSignature)
193+
signatureName = ((MethodGoLangApiSignature) goLangApiSignature).getName();
194+
195+
if (signatureName != null && signatureName.equals(call.getTargetName())
196+
&& call.getParameters().length > 0
197+
&& call.getParameters()[0] instanceof VariableRef) {
198+
199+
VariableRef var = (VariableRef) call.getParameters()[0];
200+
if (goLangApiSignature instanceof FuncGoLangApiSignature)
201+
if(goLangApiSignature.getPackage().contains(var.getName()))
202+
return true;
203+
else
204+
return true;
205+
}
206+
207+
return false;
208+
}
209+
210+
146211
private boolean hasExplicitRecovery(GoDefer defer, CheckToolWithAnalysisResults<SimpleAbstractState<PointBasedHeap, ValueEnvironment<DummyDomain>, TypeEnvironment<InferredTypes>>> tool) {
147212
Expression expr = defer.getSubExpression();
148213
if(expr instanceof CFGCall) {
@@ -231,15 +296,18 @@ private boolean atLeastOnePathWithoutRecoveryRecursive(GraphForCheckers panicGra
231296
if(stNode instanceof PossileRecoveryNode || stNode instanceof RecoveryNode)
232297
return false;
233298

234-
if(isCriticalComponent(st.getCFG().getDescriptor()))
235-
return true;
299+
236300

237301
Collection<LabeledEdge> ingoingEdges = panicGraphWithRecoveries.getIngoingEdges(stNode);
238302
if(!ingoingEdges.isEmpty())
239303
for(LabeledEdge e : ingoingEdges) {
304+
240305
if(atLeastOnePathWithoutRecoveryRecursive(panicGraphWithRecoveries, e.getSource().getStatement(), new HashSet<>(seen)))
241306
return true;
242307
}
308+
else
309+
if(isCriticalComponent(st.getCFG().getDescriptor()))
310+
return true;
243311
return false;
244312
}
245313

0 commit comments

Comments
 (0)