Bug fixing of ABCIPanicChecker

Author: olivieriluca

go-lisa/go-testcases/unhandled-errors/cosmos-panic3.go

@@ -0,0 +1,37 @@
+package distribution
+
+import (
+	"time"
+
+	"github.com/cosmos/cosmos-sdk/telemetry"
+	sdk "github.com/cosmos/cosmos-sdk/types"
+	"github.com/cosmos/cosmos-sdk/x/distribution/keeper"
+	"github.com/cosmos/cosmos-sdk/x/distribution/types"
+)
+
+
+func BeginBlocker(ctx sdk.Context, k keeper.Keeper) error {
+
+	ko()
+	ok()
+	ko()
+	
+	return nil
+}
+
+func ok(){
+	defer func() {
+	    if r := recover(); r != nil {
+	        fmt.Println("Handle panic")
+	    }
+	}()
+	foo()
+}
+
+func ko(){
+	foo()
+}
+
+func foo(){
+	panic("HIGH HOPES!")
+}

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

@@ -1,9 +1,7 @@
 package it.unive.golisa.checker.cosmos.panic;
 
-import java.util.ArrayList;
 import java.util.Collection;
 import java.util.HashSet;
-import java.util.List;
 import java.util.Set;
 
 import it.unive.golisa.analysis.DummyDomain;
@@ -28,16 +26,13 @@
 import it.unive.lisa.analysis.types.InferredTypes;
 import it.unive.lisa.checks.semantic.CheckToolWithAnalysisResults;
 import it.unive.lisa.checks.semantic.SemanticCheck;
-import it.unive.lisa.checks.syntactic.CheckTool;
 import it.unive.lisa.program.cfg.CFG;
 import it.unive.lisa.program.cfg.CodeMember;
 import it.unive.lisa.program.cfg.CodeMemberDescriptor;
 import it.unive.lisa.program.cfg.statement.Expression;
 import it.unive.lisa.program.cfg.statement.Statement;
 import it.unive.lisa.program.cfg.statement.call.CFGCall;
 import it.unive.lisa.program.cfg.statement.call.Call;
-import javassist.expr.NewArray;
-
 
 /**
  * Unhandled errors Checker in Hyperledger Fabric.
@@ -64,14 +59,17 @@ public boolean visit(
 							(GoPanic) node, tool);
 
 					String printComponents = criticalComponentsToString(panicGraphWithRecoveries);
-					if (!existPossibleRecoveryDefer(panicGraphWithRecoveries)) {
-						tool.warnOn(node, "Detected unhandled panic within the following ABCI methods: "
-								+ printComponents + ". Possible recovery functions not found.");
+					if (!(existPossibleRecoveryDefer(panicGraphWithRecoveries) ||  existRecoveryDefer(panicGraphWithRecoveries))) {
+						tool.warnOn(node, "Detected unhandled panic within a critical execution "
+								+ printComponents + ". There are no execution paths with recovery function to handle the panic.");
 					} else {
-						// TODO: handle the case where at least one path is unhandled and the another is
-						// handled
-						tool.warnOn(node, "Detected panic within the following ABCI methods: " + printComponents
-								+ ". Ensure that recovery functions properly handle the panic exception.");
+						if(atLeastOnePathWithoutRecovery(panicGraphWithRecoveries)) {
+							tool.warnOn(node, "Detected panic within a critical execution " + printComponents
+									+ ". There is at least an execution path without a recovery function.");
+						} else {
+							tool.warnOn(node, "Detected panic within a critical execution " + printComponents
+									+ ". Ensure that all the possible recovery functions properly handle the panic exception.");
+						}
 					}
 
 				}
@@ -95,13 +93,13 @@ private String criticalComponentsToString(GraphForCheckers panicGraphWithRecover
 		return String.join(",", signatures);
 	}
 
-
-
 	private boolean existPossibleRecoveryDefer(GraphForCheckers panicGraphWithRecoveries) {
-		
 		return panicGraphWithRecoveries.getNodes().stream().anyMatch(n -> n instanceof PossileRecoveryNode);
 	}
 
+	private boolean existRecoveryDefer(GraphForCheckers panicGraphWithRecoveries) {
+		return panicGraphWithRecoveries.getNodes().stream().anyMatch(n -> n instanceof RecoveryNode);
+	}
 
 
 	private GraphForCheckers computePossibleRecoveryDefers(GraphForCheckers panicGraph, GoPanic panic, CheckToolWithAnalysisResults<SimpleAbstractState<PointBasedHeap, ValueEnvironment<DummyDomain>, TypeEnvironment<InferredTypes>>> tool) throws CloneNotSupportedException {
@@ -139,8 +137,10 @@ private void computePossibleRecoveryDefersRecursive(GraphForCheckers graphWithRe
 
 		Collection<LabeledEdge> ingoingEdges = graphWithRecovery.getIngoingEdges(stNode);
 		if(!ingoingEdges.isEmpty())
-			for(LabeledEdge e : ingoingEdges)
-				computePossibleRecoveryDefersRecursive(graphWithRecovery, e.getSource().getStatement(), tool, seen);
+			for(LabeledEdge e : ingoingEdges) {
+				
+				computePossibleRecoveryDefersRecursive(graphWithRecovery, e.getSource().getStatement(), tool, new HashSet<>(seen));
+			}
 	}
 
 	private boolean hasExplicitRecovery(GoDefer defer, CheckToolWithAnalysisResults<SimpleAbstractState<PointBasedHeap, ValueEnvironment<DummyDomain>, TypeEnvironment<InferredTypes>>> tool) {
@@ -186,7 +186,7 @@ private GraphForCheckers extractPathCriticalComponentsInvolvedInPanicRecursive(S
 								VariableScopingCFG callerCFG = (VariableScopingCFG) cm;
 								Statement sTarget = CFGUtils.extractTargetNodeFromGraph(callerCFG, c);
 								if (sTarget != null) {
-									 GraphForCheckers tmp = extractPathCriticalComponentsInvolvedInPanicRecursive(sTarget, sTarget, graph, tool, seen);
+									 GraphForCheckers tmp = extractPathCriticalComponentsInvolvedInPanicRecursive(sTarget, node, graph, tool, new HashSet<>(seen));
 									 if(tmp != null) {
 											graph.merge(tmp);
 									 }
@@ -196,55 +196,51 @@ private GraphForCheckers extractPathCriticalComponentsInvolvedInPanicRecursive(S
 					}
 				}
 			}
+		} else {
+			throw new UnsupportedOperationException("The analysis on cyclic graphs are currently not supported");
 		}
 		return graph;
 	}
 
-
-
-	private Set<CodeMemberDescriptor> extractCriticalComponentsInvolvedInPanic(GoPanic panic, CheckToolWithAnalysisResults<SimpleAbstractState<PointBasedHeap, ValueEnvironment<DummyDomain>, TypeEnvironment<InferredTypes>>> tool) {
-		Set<CodeMember> seen = new HashSet<>();
-		return extractCriticalComponentsRecursive(panic, tool, seen);
+	private boolean isCriticalComponent(CodeMemberDescriptor descriptor) {
+		return descriptor.getSignature().contains("BeginBlocker") 
+		|| descriptor.getSignature().contains("EndBlocker"); 
 	}
 
-	private Set<CodeMemberDescriptor> extractCriticalComponentsRecursive(Statement node, CheckToolWithAnalysisResults<SimpleAbstractState<PointBasedHeap, ValueEnvironment<DummyDomain>, TypeEnvironment<InferredTypes>>> tool, Set<CodeMember>  seen) {
-		Set<CodeMemberDescriptor> result = new HashSet<>();
-		if(!seen.contains(node.getCFG())) {
-			seen.add(node.getCFG());	
-			if(isCriticalComponent(node.getCFG().getDescriptor())) {
-				result.add(node.getCFG().getDescriptor());
-			} else {
-				// check callers of CFG recursively
-				Collection<CodeMember> callers = tool.getCallers(node.getCFG());
-
-				for (CodeMember cm : callers) {
-					if (!seen.contains(cm)) {
-						seen.add(cm);
 
-						for (Call c : tool.getCallSites(node.getCFG())) {
-							if (cm instanceof VariableScopingCFG) {
-								VariableScopingCFG callerCFG = (VariableScopingCFG) cm;
-								Statement sTarget = CFGUtils.extractTargetNodeFromGraph(callerCFG, c);
-								if (sTarget != null) {
-									result.addAll(extractCriticalComponentsRecursive(sTarget, tool, seen));
-								}
-							}
-						}
-					}
-				}
+	private boolean atLeastOnePathWithoutRecovery(GraphForCheckers panicGraphWithRecoveries) {
+		Set<Statement> seen = new HashSet<>();
+		PanicNode panicNode = null;
+		for(StandardNode n : panicGraphWithRecoveries.getNodes())
+			if(n instanceof PanicNode) {
+				panicNode= (PanicNode) n;
+				break;
 			}
-		}
-		return result;
-	}
-
-	private boolean isCriticalComponent(CodeMemberDescriptor descriptor) {
-		return descriptor.getSignature().contains("BeginBlocker") 
-		|| descriptor.getSignature().contains("EndBlocker"); 
+			
+		return atLeastOnePathWithoutRecoveryRecursive(panicGraphWithRecoveries, panicNode.getStatement(), seen);
 	}
+	
+	private boolean atLeastOnePathWithoutRecoveryRecursive(GraphForCheckers panicGraphWithRecoveries, Statement st, Set<Statement> seen) {
 
-	private Set<Statement> extractPossibleRecoveryDefer(Statement node) {
-		// TODO Auto-generated method stub
-		return null;
+		if(seen.contains(st))
+			return false;
+		seen.add(st);
+		
+		StandardNode stNode = panicGraphWithRecoveries.getNodeFromStatement(st);
+		
+		if(stNode instanceof PossileRecoveryNode || stNode instanceof RecoveryNode)
+			return false;
+		
+		if(isCriticalComponent(st.getCFG().getDescriptor()))
+				return true;
+		
+		Collection<LabeledEdge> ingoingEdges = panicGraphWithRecoveries.getIngoingEdges(stNode);
+		if(!ingoingEdges.isEmpty())
+			for(LabeledEdge e : ingoingEdges) {
+				if(atLeastOnePathWithoutRecoveryRecursive(panicGraphWithRecoveries, e.getSource().getStatement(), new HashSet<>(seen)))
+					return true;
+			}
+		return false;
 	}
 
 }

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

@@ -16,4 +16,22 @@ public PanicNode(GraphForCheckers graph, GoPanic st) {
 		super(graph, st);
 	}
 
+	@Override
+	public int hashCode() {
+		return super.hashCode();
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		return super.equals(obj);
+	}
+
+	@Override
+	public PanicNode clone() throws CloneNotSupportedException {
+
+		return new PanicNode(getGraph(), (GoPanic) getStatement());
+	}
+
+	
+
 }

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

@@ -16,4 +16,11 @@ public PossileRecoveryNode(GraphForCheckers graph, GoDefer st) {
 		super(graph, st);
 	}
 
+
+	@Override
+	public PossileRecoveryNode clone() throws CloneNotSupportedException {
+
+		return new PossileRecoveryNode(getGraph(), (GoDefer) getStatement());
+	}
+
 }

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

@@ -16,4 +16,9 @@ public RecoveryNode(GraphForCheckers graph, GoDefer st) {
 		super(graph, st);
 	}
 
+	@Override
+	public RecoveryNode clone() throws CloneNotSupportedException {
+
+		return new RecoveryNode(getGraph(), (GoDefer) getStatement());
+	}
 }

go-lisa/src/main/java/it/unive/golisa/checker/utils/graph/GraphForCheckers.java

@@ -21,6 +21,7 @@
 import java.util.Iterator;
 import java.util.Map;
 import java.util.Map.Entry;
+import java.util.Objects;
 import java.util.Set;
 import java.util.SortedSet;
 import java.util.TreeSet;
@@ -32,7 +33,7 @@
 
 public class GraphForCheckers extends CodeGraph<GraphForCheckers, StandardNode, LabeledEdge> implements Cloneable {
 
-	private final String name;
+	private final String name; 
 
 	public GraphForCheckers(String name) {
 		super(new StandardEdge(null, null));
@@ -300,10 +301,12 @@ public StandardNode getNodeFromStatement(Statement statement) {
 
 	public void merge(GraphForCheckers other) throws CloneNotSupportedException {
 		for(StandardNode n : other.getNodes()) {
-			this.addNode(n.clone());
+			if(!this.containsNode(n))
+				this.addNode(n.clone());
 		}
 		for(LabeledEdge e : other.getEdges()) {
-			this.addEdge(e.clone());
+			if(!this.containsEdge(e))
+				this.addEdge(e.clone());
 		}
 	}
 
@@ -312,11 +315,31 @@ public GraphForCheckers clone() throws CloneNotSupportedException {
 		GraphForCheckers clone = new GraphForCheckers(getName());
 		for(StandardNode n : getNodes())
 			clone.addNode(n.clone());
-		for(LabeledEdge e : getEdges())
+		for(LabeledEdge e : getEdges()) {
 			clone.addEdge(e.clone());
+		}
 
 		return clone;
 	}
+
+	@Override
+	public int hashCode() {
+		return Objects.hash(name);
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		GraphForCheckers other = (GraphForCheckers) obj;
+		return Objects.equals(name, other.name);
+	}
+	
+	
 
 
 }

go-lisa/src/main/java/it/unive/golisa/checker/utils/graph/edges/LabeledEdge.java

@@ -50,7 +50,7 @@ public boolean equals(Object obj) {
 		if (getClass() != obj.getClass())
 			return false;
 		LabeledEdge other = (LabeledEdge) obj;
-		return Objects.equals(destination, other.destination) && Objects.equals(source, other.source);
+		return destination.equals(other.destination) && source.equals(other.source);
 	}
 
 	@Override