Implemented simple BMC

subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/stateless/XcfaCli.java

@@ -50,6 +50,7 @@
 import hu.bme.mit.theta.xcfa.model.XcfaEdge;
 import hu.bme.mit.theta.xcfa.model.utils.FrontendXcfaBuilder;
 import hu.bme.mit.theta.xcfa.passes.XcfaPassManager;
+import hu.bme.mit.theta.xcfa.passes.procedurepass.BMC;
 import hu.bme.mit.theta.xcfa.passes.procedurepass.GlobalVarsToStoreLoad;
 import hu.bme.mit.theta.xcfa.passes.procedurepass.OneStmtPerEdgePass;
 import org.antlr.v4.runtime.CharStream;
@@ -64,6 +65,7 @@
 import java.io.PrintWriter;
 import java.time.LocalDateTime;
 import java.util.LinkedHashSet;
+import java.util.List;
 import java.util.Set;
 import java.util.concurrent.TimeUnit;
 
@@ -112,6 +114,9 @@ public class XcfaCli {
 	@Parameter(names = "--gui", description = "Show GUI")
 	boolean showGui = false;
 
+	@Parameter(names = "--bmc", description = "Run BMC pre-check")
+	boolean runbmc = false;
+
 	@Parameter(names = "--benchmark-parsing", description = "Run parsing tasks only")
 	boolean parsing = false;
 
@@ -248,6 +253,18 @@ private void run() {
 				}
 			}
 
+			if (runbmc) {
+				if(xcfa.getProcesses().size() == 1) {
+					checkState(xcfa.getMainProcess().getProcedures().size() == 1, "Multiple procedures are not yet supported!");
+					List<XcfaEdge> cex = new BMC().getCex(xcfa.getMainProcess().getMainProcedure());
+					if(cex != null) {
+						System.out.println("SafetyResult Unsafe");
+						return;
+					}
+				}
+
+			}
+
 			CFA cfa;
 			try {
 				cfa = xcfa.createCFA();

subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/16loop.c

@@ -0,0 +1,7 @@
+void reach_error(){}
+
+int main() {
+    for(int i = 0; i < 30; i++) {
+        if(i == 19) reach_error();
+    }
+ }

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaPath.java

@@ -0,0 +1,51 @@
+package hu.bme.mit.theta.xcfa.model;
+
+import hu.bme.mit.theta.core.decl.ConstDecl;
+import hu.bme.mit.theta.core.decl.VarDecl;
+import hu.bme.mit.theta.core.stmt.AssignStmt;
+import hu.bme.mit.theta.core.stmt.AssumeStmt;
+import hu.bme.mit.theta.core.stmt.HavocStmt;
+import hu.bme.mit.theta.core.stmt.Stmt;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+
+import static hu.bme.mit.theta.core.decl.Decls.Const;
+import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And;
+import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True;
+
+public class XcfaPath {
+	private final List<XcfaEdge> edges;
+
+	public XcfaPath(List<XcfaEdge> edges) {
+		this.edges = edges;
+	}
+
+	public Expr<BoolType> getExpression() {
+		Map<VarDecl<?>, ConstDecl<?>> varToLastConstMap = new LinkedHashMap<>();
+		Expr<BoolType> ret = True();
+
+		for (XcfaEdge edge : edges) {
+			for (Stmt stmt : edge.getStmts()) {
+				if (stmt instanceof HavocStmt) {
+					VarDecl<?> var = ((HavocStmt<?>) stmt).getVarDecl();
+					varToLastConstMap.put(var, Const(var.getName(), var.getType()));
+				} else if (stmt instanceof AssumeStmt) {
+					Expr<BoolType> expr = XcfaStmtVarReplacer.replaceVars(((AssumeStmt) stmt).getCond(), varToLastConstMap);
+					ret = And(ret, expr);
+				} else if (stmt instanceof AssignStmt) {
+					VarDecl<?> var = ((AssignStmt<?>) stmt).getVarDecl();
+					ConstDecl<?> cnst = Const(var.getName(), var.getType());
+					Expr<?> expr = XcfaStmtVarReplacer.replaceVars(((AssignStmt<?>) stmt).getExpr(), varToLastConstMap);
+					ret = And(ret, Eq(cnst.getRef(), expr));
+					varToLastConstMap.put(var, cnst);
+				} else throw new UnsupportedOperationException("Not yet implemented!");
+			}
+		}
+		return ret;
+	}
+}

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaProcedure.java

@@ -221,6 +221,10 @@ void setParent(XcfaProcess xcfaProcess) {
         this.parent = xcfaProcess;
     }
 
+    public Type getRetType() {
+        return retType;
+    }
+
     public static final class Builder {
         private static final String RESULT_NAME = "result";
 
@@ -283,6 +287,13 @@ public List<XcfaLocation> getLocs() {
             return locs;
         }
 
+        public void removeLoc(XcfaLocation loc) {
+            checkArgument(loc != initLoc, "Cannot remove initloc!");
+            checkArgument(loc != finalLoc, "Cannot remove finalloc!");
+            checkArgument(loc != errorLoc, "Cannot remove errorloc!");
+            locs.remove(loc);
+        }
+
         public XcfaLocation addLoc(XcfaLocation loc) {
             checkNotBuilt();
             if(!locs.contains(loc))
@@ -334,8 +345,9 @@ public void setErrorLoc(final XcfaLocation errorLoc) {
             checkArgument(locs.contains(errorLoc), "Error location not present in XCFA.");
             checkArgument(initLoc == null || !initLoc.equals(errorLoc), "Error location cannot be the same as init location.");
             checkArgument(finalLoc == null || !finalLoc.equals(errorLoc), "Error location cannot be the same as final location.");
+            if(errorLoc != null) errorLoc.setErrorLoc(true);
+            else this.errorLoc.setErrorLoc(false);
             this.errorLoc = errorLoc;
-            errorLoc.setErrorLoc(true);
         }
 
         // finalLoc

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/AssignmentChainRemoval.java

@@ -59,7 +59,7 @@ public XcfaProcedure.Builder run(XcfaProcedure.Builder builder) {
 					FrontendMetadata.lookupMetadata(assignEdge).forEach((s, o) -> {
 						FrontendMetadata.create(xcfaEdge, s, o);
 					});
-					builder.getLocs().remove(assignEdge1.get().getTarget());
+					builder.removeLoc(assignEdge1.get().getTarget());
 				}
 			}
 		}

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/BMC.java

@@ -0,0 +1,61 @@
+package hu.bme.mit.theta.xcfa.passes.procedurepass;
+
+import hu.bme.mit.theta.xcfa.model.XcfaEdge;
+import hu.bme.mit.theta.xcfa.model.XcfaLocation;
+import hu.bme.mit.theta.xcfa.model.XcfaProcedure;
+
+import java.util.List;
+
+import static hu.bme.mit.theta.xcfa.passes.procedurepass.Utils.collectPaths;
+import static hu.bme.mit.theta.xcfa.passes.procedurepass.Utils.createBuilder;
+
+public class BMC{
+	private static final int MAX_K = 100;
+
+	public List<XcfaEdge> getCex(XcfaProcedure builder) {
+		if(builder.getErrorLoc() == null) return null;
+
+		XcfaProcedure.Builder workingCopy = createBuilder(builder);
+		UnrollLoopsPass unrollLoopsPass = new UnrollLoopsPass();
+
+		for(int i = 0; i < MAX_K; ++i) {
+			List<XcfaEdge> cex;
+			if((cex = getCex(workingCopy)) != null) {
+				return cex;
+//				XcfaProcedure.Builder retBuilder = XcfaProcedure.builder();
+//				retBuilder.setName(builder.getName());
+//				Map<XcfaLocation, XcfaLocation> locLut = new LinkedHashMap<>();
+//				for (XcfaEdge edge : cex) {
+//					XcfaLocation source = edge.getSource();
+//					XcfaLocation target = edge.getTarget();
+//					XcfaLocation newSource = XcfaLocation.copyOf(source);
+//					XcfaLocation newTarget = XcfaLocation.copyOf(target);
+//					locLut.putIfAbsent(source, newSource);
+//					locLut.putIfAbsent(target, newTarget);
+//					newSource = locLut.get(source);
+//					newTarget = locLut.get(target);
+//					retBuilder.addLoc(newSource);
+//					retBuilder.addLoc(newTarget);
+//					retBuilder.addEdge(new XcfaEdge(newSource, newTarget, edge.getStmts()));
+//				}
+//				retBuilder.setInitLoc(locLut.get(workingCopy.getInitLoc()));
+//				XcfaLocation location = new XcfaLocation("final", Map.of()); // Final location never contained in CEX but still necesaary
+//				retBuilder.addLoc(location);
+//				retBuilder.setFinalLoc(location);
+//				retBuilder.setErrorLoc(locLut.get(workingCopy.getErrorLoc()));
+//				System.err.println("BMC saves the day!");
+//				return retBuilder.build();
+			}
+			System.out.println("BMC has not found a violation in iteration " + i + " with " + workingCopy.getEdges().size() + " edges.");
+			workingCopy = unrollLoopsPass.run(workingCopy);
+		}
+
+		return null;
+	}
+
+	private List<XcfaEdge> getCex(XcfaProcedure.Builder builder) {
+		XcfaLocation initLoc = builder.getInitLoc();
+		XcfaLocation errorLoc = builder.getErrorLoc();
+		return collectPaths(initLoc, errorLoc);
+	}
+}

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/EmptyEdgeRemovalPass.java

@@ -69,7 +69,7 @@ public XcfaProcedure.Builder run(XcfaProcedure.Builder builder) {
 				for (XcfaEdge outgoingEdge : outgoingEdges) {
 					builder.removeEdge(outgoingEdge);
 				}
-				builder.getLocs().remove(loc.get());
+				builder.removeLoc(loc.get());
 			}
 		}
 //

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/HavocAssignments.java

@@ -54,7 +54,7 @@ public XcfaProcedure.Builder run(XcfaProcedure.Builder builder) {
 					FrontendMetadata.lookupMetadata(assignEdge).forEach((s, o) -> {
 						FrontendMetadata.create(xcfaEdge, s, o);
 					});
-					builder.getLocs().remove(havocEdge.get().getTarget());
+					builder.removeLoc(havocEdge.get().getTarget());
 				}
 			}
 		}

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/RemoveDeadEnds.java

@@ -5,6 +5,7 @@
 import hu.bme.mit.theta.xcfa.model.XcfaProcedure;
 
 import java.util.LinkedHashSet;
+import java.util.List;
 import java.util.Optional;
 import java.util.Set;
 import java.util.stream.Collectors;
@@ -23,7 +24,11 @@ public XcfaProcedure.Builder run(XcfaProcedure.Builder builder) {
 		for (XcfaEdge edge : collect) {
 			builder.removeEdge(edge);
 		}
-		builder.getLocs().removeIf(loc -> loc.getIncomingEdges().size() == 0 && loc.getOutgoingEdges().size() == 0);
+		List<XcfaLocation> toRemove = builder.getLocs().stream().filter(loc -> loc.getIncomingEdges().size() == 0 && loc.getOutgoingEdges().size() == 0 && !loc.isEndLoc() && !loc.isErrorLoc()).collect(Collectors.toList());
+		for (XcfaLocation location : toRemove) {
+			if(builder.getInitLoc() != location)
+				builder.removeLoc(location);
+		}
 		return builder;
 	}
 

subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/Utils.java

@@ -1,29 +1,96 @@
 package hu.bme.mit.theta.xcfa.passes.procedurepass;
 
+import hu.bme.mit.theta.core.decl.ConstDecl;
+import hu.bme.mit.theta.core.decl.VarDecl;
+import hu.bme.mit.theta.core.stmt.AssignStmt;
+import hu.bme.mit.theta.core.stmt.AssumeStmt;
+import hu.bme.mit.theta.core.stmt.HavocStmt;
+import hu.bme.mit.theta.core.stmt.Stmt;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.Type;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.utils.StmtUtils;
+import hu.bme.mit.theta.solver.Solver;
+import hu.bme.mit.theta.solver.z3.Z3SolverFactory;
 import hu.bme.mit.theta.xcfa.model.XcfaEdge;
 import hu.bme.mit.theta.xcfa.model.XcfaLocation;
+import hu.bme.mit.theta.xcfa.model.XcfaProcedure;
+import hu.bme.mit.theta.xcfa.model.XcfaStmtVarReplacer;
 
+import java.util.ArrayList;
+import java.util.LinkedHashMap;
 import java.util.LinkedHashSet;
 import java.util.List;
+import java.util.Map;
 import java.util.Set;
 import java.util.Stack;
 
 import static com.google.common.base.Preconditions.checkArgument;
+import static hu.bme.mit.theta.core.decl.Decls.Const;
+import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq;
 
 public class Utils {
+
+	public static List<XcfaEdge> collectPaths(XcfaLocation start, XcfaLocation end) {
+		return collectPaths(start, new SetStack<>(), end, new LinkedHashMap<>(), Z3SolverFactory.getInstance().createSolver());
+	}
+
+	private static List<XcfaEdge> collectPaths(XcfaLocation current, SetStack<XcfaEdge> path, XcfaLocation end, Map<VarDecl<?>, ConstDecl<?>> varToLastConstMap, Solver solver) {
+		if(current == end) {
+			return path.getList();
+		}
+		List<XcfaEdge> outgoingEdges = current.getOutgoingEdges();
+		for (XcfaEdge outgoingEdge : outgoingEdges) {
+			if(!path.contains(outgoingEdge)) {
+				path.push(outgoingEdge);
+				solver.push();
+				for (Stmt stmt : outgoingEdge.getStmts()) {
+					for (VarDecl<?> var : StmtUtils.getVars(stmt)) {
+						if(!varToLastConstMap.containsKey(var)) varToLastConstMap.put(var, Const(var.getName(), var.getType()));
+					}
+					if (stmt instanceof HavocStmt) {
+						VarDecl<?> var = ((HavocStmt<?>) stmt).getVarDecl();
+						varToLastConstMap.put(var, Const(var.getName(), var.getType()));
+					} else if (stmt instanceof AssumeStmt) {
+						Expr<BoolType> expr = XcfaStmtVarReplacer.replaceVars(((AssumeStmt) stmt).getCond(), varToLastConstMap);
+						solver.add(expr);
+					} else if (stmt instanceof AssignStmt) {
+						VarDecl<?> var = ((AssignStmt<?>) stmt).getVarDecl();
+						ConstDecl<?> cnst = Const(var.getName(), var.getType());
+						Expr<BoolType> expr = Eq(cnst.getRef(), XcfaStmtVarReplacer.replaceVars(((AssignStmt<?>) stmt).getExpr(), varToLastConstMap));
+						solver.add(expr);
+						varToLastConstMap.put(var, cnst);
+					} else throw new UnsupportedOperationException("Not yet implemented!");
+				}
+				solver.check();
+				if(solver.getStatus().isUnsat()) return null;
+				List<XcfaEdge> ret = collectPaths(outgoingEdge.getTarget(), path, end, varToLastConstMap, solver);
+				if(ret != null) return ret;
+				solver.pop();
+				path.pop();
+			}
+		}
+		return null;
+	}
+
+
 	public static Set<XcfaEdge> collectReverseEdges(XcfaLocation location) {
-		return collectReverseEdges(location, new SetStack<>());
+		return collectReverseEdges(location, new LinkedHashSet<>(Set.of(location)));
 	}
 
-	private static Set<XcfaEdge> collectReverseEdges(XcfaLocation location, SetStack<XcfaLocation> path) {
+	private static Set<XcfaEdge> collectReverseEdges(XcfaLocation location, Set<XcfaLocation> visited) {
 		Set<XcfaEdge> ret = new LinkedHashSet<>();
-		path.push(location);
-		List<XcfaEdge> outgoingEdges = location.getOutgoingEdges();
-		for (XcfaEdge outgoingEdge : outgoingEdges) {
-			if(!path.contains(outgoingEdge.getTarget())) {
-				ret.addAll(collectReverseEdges(outgoingEdge.getTarget(), path));
-			} else {
-				ret.add(outgoingEdge);
+		List<XcfaEdge> outgoingEdges = new ArrayList<>(location.getOutgoingEdges());
+		while(outgoingEdges.size() > 0) {
+			ArrayList<XcfaEdge> copy = new ArrayList<>(outgoingEdges);
+			outgoingEdges.clear();
+			for (XcfaEdge outgoingEdge : copy) {
+				if (visited.contains(outgoingEdge.getTarget())) {
+					ret.add(outgoingEdge);
+				} else {
+					visited.add(outgoingEdge.getTarget());
+					outgoingEdges.addAll(outgoingEdge.getTarget().getOutgoingEdges());
+				}
 			}
 		}
 		return ret;
@@ -59,5 +126,36 @@ public T peek() {
 		public boolean contains(T t) {
 			return set.contains(t);
 		}
+
+		public List<T> getList() {
+			return stack;
+		}
+	}
+
+	public static XcfaProcedure.Builder copyBuilder(XcfaProcedure.Builder builder) {
+		return getBuilder(builder.getName(), builder.getRetType(), builder.getLocs(), builder.getFinalLoc(), builder.getInitLoc(), builder.getErrorLoc(), builder.getEdges());
+	}
+
+	public static XcfaProcedure.Builder createBuilder(XcfaProcedure proc) {
+		return getBuilder(proc.getName(), proc.getRetType(), proc.getLocs(), proc.getFinalLoc(), proc.getInitLoc(), proc.getErrorLoc(), proc.getEdges());
+	}
+
+	private static XcfaProcedure.Builder getBuilder(String name, Type retType, List<XcfaLocation> locs, XcfaLocation finalLoc, XcfaLocation initLoc, XcfaLocation errorLoc, List<XcfaEdge> edges) {
+		XcfaProcedure.Builder ret = XcfaProcedure.builder();
+		ret.setName(name);
+		ret.setRetType(retType);
+		Map<XcfaLocation, XcfaLocation> locationLut = new LinkedHashMap<>();
+		for (XcfaLocation location : new LinkedHashSet<>(locs)) {
+			XcfaLocation copy = XcfaLocation.copyOf(location);
+			ret.addLoc(copy);
+			locationLut.put(location, copy);
+		}
+		ret.setFinalLoc(locationLut.get(finalLoc));
+		ret.setInitLoc(locationLut.get(initLoc));
+		if(errorLoc != null) ret.setErrorLoc(locationLut.get(errorLoc));
+		for (XcfaEdge edge : edges) {
+			ret.addEdge(new XcfaEdge(locationLut.get(edge.getSource()), locationLut.get(edge.getTarget()), edge.getStmts()));
+		}
+		return ret;
 	}
 }