From 619034ef9907c3e3086c034cb4018693d4148606 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Wed, 25 Aug 2021 17:52:17 +0200 Subject: [PATCH] Implemented simple BMC --- .../mit/theta/xcfa/cli/stateless/XcfaCli.java | 17 +++ .../c/litmustest/singlethread/16loop.c | 7 ++ .../hu/bme/mit/theta/xcfa/model/XcfaPath.java | 51 ++++++++ .../mit/theta/xcfa/model/XcfaProcedure.java | 14 ++- .../procedurepass/AssignmentChainRemoval.java | 2 +- .../theta/xcfa/passes/procedurepass/BMC.java | 61 +++++++++ .../procedurepass/EmptyEdgeRemovalPass.java | 2 +- .../procedurepass/HavocAssignments.java | 2 +- .../passes/procedurepass/RemoveDeadEnds.java | 7 +- .../xcfa/passes/procedurepass/Utils.java | 116 ++++++++++++++++-- .../mit/theta/xcfa/UnrollLoopsPassTest.java | 21 +--- 11 files changed, 267 insertions(+), 33 deletions(-) create mode 100644 subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/16loop.c create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaPath.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/BMC.java diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/stateless/XcfaCli.java b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/stateless/XcfaCli.java index 8fbe00e73d..193db2681e 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/stateless/XcfaCli.java +++ b/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 cex = new BMC().getCex(xcfa.getMainProcess().getMainProcedure()); + if(cex != null) { + System.out.println("SafetyResult Unsafe"); + return; + } + } + + } + CFA cfa; try { cfa = xcfa.createCFA(); diff --git a/subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/16loop.c b/subprojects/xcfa/xcfa-cli/src/test/resources/c/litmustest/singlethread/16loop.c new file mode 100644 index 0000000000..e4ba359ece --- /dev/null +++ b/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(); + } + } \ No newline at end of file diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaPath.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaPath.java new file mode 100644 index 0000000000..12614ff659 --- /dev/null +++ b/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 edges; + + public XcfaPath(List edges) { + this.edges = edges; + } + + public Expr getExpression() { + Map, ConstDecl> varToLastConstMap = new LinkedHashMap<>(); + Expr 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 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; + } +} diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaProcedure.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaProcedure.java index 046f00ca6e..cd54bf8493 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaProcedure.java +++ b/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 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 diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/AssignmentChainRemoval.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/AssignmentChainRemoval.java index 74e316b6ce..dfa9365ecf 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/AssignmentChainRemoval.java +++ b/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()); } } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/BMC.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/BMC.java new file mode 100644 index 0000000000..a0ad69a858 --- /dev/null +++ b/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 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 cex; + if((cex = getCex(workingCopy)) != null) { + return cex; +// XcfaProcedure.Builder retBuilder = XcfaProcedure.builder(); +// retBuilder.setName(builder.getName()); +// Map 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 getCex(XcfaProcedure.Builder builder) { + XcfaLocation initLoc = builder.getInitLoc(); + XcfaLocation errorLoc = builder.getErrorLoc(); + return collectPaths(initLoc, errorLoc); + } +} diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/EmptyEdgeRemovalPass.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/EmptyEdgeRemovalPass.java index eeb2067bdf..37a52aadbb 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/EmptyEdgeRemovalPass.java +++ b/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()); } } // diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/HavocAssignments.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/HavocAssignments.java index 83ceab60af..e6e987fa6d 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/HavocAssignments.java +++ b/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()); } } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/RemoveDeadEnds.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/RemoveDeadEnds.java index ef92f350b0..6758ba763e 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/RemoveDeadEnds.java +++ b/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 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; } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/Utils.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/Utils.java index d354de75ee..1f76b0ec44 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/procedurepass/Utils.java +++ b/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 collectPaths(XcfaLocation start, XcfaLocation end) { + return collectPaths(start, new SetStack<>(), end, new LinkedHashMap<>(), Z3SolverFactory.getInstance().createSolver()); + } + + private static List collectPaths(XcfaLocation current, SetStack path, XcfaLocation end, Map, ConstDecl> varToLastConstMap, Solver solver) { + if(current == end) { + return path.getList(); + } + List 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 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 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 ret = collectPaths(outgoingEdge.getTarget(), path, end, varToLastConstMap, solver); + if(ret != null) return ret; + solver.pop(); + path.pop(); + } + } + return null; + } + + public static Set collectReverseEdges(XcfaLocation location) { - return collectReverseEdges(location, new SetStack<>()); + return collectReverseEdges(location, new LinkedHashSet<>(Set.of(location))); } - private static Set collectReverseEdges(XcfaLocation location, SetStack path) { + private static Set collectReverseEdges(XcfaLocation location, Set visited) { Set ret = new LinkedHashSet<>(); - path.push(location); - List outgoingEdges = location.getOutgoingEdges(); - for (XcfaEdge outgoingEdge : outgoingEdges) { - if(!path.contains(outgoingEdge.getTarget())) { - ret.addAll(collectReverseEdges(outgoingEdge.getTarget(), path)); - } else { - ret.add(outgoingEdge); + List outgoingEdges = new ArrayList<>(location.getOutgoingEdges()); + while(outgoingEdges.size() > 0) { + ArrayList 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 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 locs, XcfaLocation finalLoc, XcfaLocation initLoc, XcfaLocation errorLoc, List edges) { + XcfaProcedure.Builder ret = XcfaProcedure.builder(); + ret.setName(name); + ret.setRetType(retType); + Map 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; } } diff --git a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/UnrollLoopsPassTest.java b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/UnrollLoopsPassTest.java index 77c8d4d26b..1da3d6f174 100644 --- a/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/UnrollLoopsPassTest.java +++ b/subprojects/xcfa/xcfa/src/test/java/hu/bme/mit/theta/xcfa/UnrollLoopsPassTest.java @@ -22,9 +22,9 @@ import hu.bme.mit.theta.xcfa.passes.procedurepass.UnrollLoopsPass; import org.junit.Test; -import java.util.LinkedHashMap; import java.util.List; -import java.util.Map; + +import static hu.bme.mit.theta.xcfa.passes.procedurepass.Utils.copyBuilder; public final class UnrollLoopsPassTest { @@ -93,21 +93,4 @@ public void test(){ System.out.println("}"); } - private XcfaProcedure.Builder copyBuilder(XcfaProcedure.Builder builder) { - XcfaProcedure.Builder ret = XcfaProcedure.builder(); - Map locationLut = new LinkedHashMap<>(); - builder.getLocs().forEach(location -> { - XcfaLocation copy = XcfaLocation.copyOf(location); - ret.addLoc(copy); - locationLut.put(location, copy); - }); - ret.setFinalLoc(locationLut.get(builder.getFinalLoc())); - ret.setInitLoc(locationLut.get(builder.getInitLoc())); - if(builder.getErrorLoc() != null) ret.setErrorLoc(locationLut.get(builder.getErrorLoc())); - for (XcfaEdge edge : builder.getEdges()) { - ret.addEdge(new XcfaEdge(locationLut.get(edge.getSource()), locationLut.get(edge.getTarget()), edge.getStmts())); - } - return ret; - } - }