From 2fc7c22fe0b63d00e0d2335c5ece8617a478cf42 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Thu, 22 Jun 2023 18:40:20 +0200 Subject: [PATCH] Made LLVM parts compile --- .../java/hu/bme/mit/theta/xcfa/XcfaUtils.java | 94 +++++++++---------- .../java/hu/bme/mit/theta/xcfa/ir/Utils.java | 13 ++- .../concrete/ArrayIntrinsicsHandler.java | 6 +- .../concrete/BuiltinFunctionHandler.java | 8 +- .../concrete/MemoryInstructionHandler.java | 10 +- .../concrete/OtherInstructionHandler.java | 11 ++- .../TerminatorInstructionHandler.java | 51 +++++----- .../xcfa/ir/handlers/states/BuiltState.java | 19 +--- .../ir/handlers/states/FunctionState.java | 37 ++++---- .../xcfa/ir/handlers/states/GlobalState.java | 11 ++- .../hu/bme/mit/theta/xcfa/model/Builders.kt | 27 +++--- 11 files changed, 140 insertions(+), 147 deletions(-) diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaUtils.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaUtils.java index c70670f99d..407fcbb1e9 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaUtils.java +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaUtils.java @@ -21,12 +21,6 @@ import hu.bme.mit.theta.common.Tuple4; import hu.bme.mit.theta.xcfa.model.XCFA; import hu.bme.mit.theta.xcfa.model.XcfaProcedure; -import hu.bme.mit.theta.xcfa.model.XcfaProcess; -import hu.bme.mit.theta.xcfa.passes.procedurepass.EmptyEdgeRemovalPass; -import hu.bme.mit.theta.xcfa.passes.procedurepass.ProcedurePass; -import hu.bme.mit.theta.xcfa.passes.procedurepass.UnusedVarRemovalPass; -import hu.bme.mit.theta.xcfa.passes.processpass.ProcessPass; -import hu.bme.mit.theta.xcfa.passes.xcfapass.XcfaPass; import hu.bme.mit.theta.xcfa.ir.ArithmeticType; import hu.bme.mit.theta.xcfa.ir.LlvmIrProvider; import hu.bme.mit.theta.xcfa.ir.SSAProvider; @@ -38,6 +32,7 @@ import hu.bme.mit.theta.xcfa.ir.handlers.states.BuiltState; import hu.bme.mit.theta.xcfa.ir.handlers.states.FunctionState; import hu.bme.mit.theta.xcfa.ir.handlers.states.GlobalState; +import hu.bme.mit.theta.xcfa.passes.ProcedurePass; import java.io.File; import java.io.FileNotFoundException; @@ -80,23 +75,22 @@ public static XCFA fromFile(File model, ArithmeticType arithmeticType) throws IO * Creates an XCFA from the provided SSAProvider using its getter methods. */ public static XCFA createXCFA(SSAProvider ssa, ArithmeticType arithmeticType) { - return createXCFA(ssa, List.of(), List.of(), List.of(new UnusedVarRemovalPass(), new EmptyEdgeRemovalPass()), arithmeticType); + return createXCFA(ssa, List.of(), arithmeticType); } /* * Creates an XCFA from the provided SSAProvider using its getter methods. * Runs the specified passes when a specific stage is complete. */ - public static XCFA createXCFA(SSAProvider ssa, List xcfaPasses, List processPasses, List procedurePasses, ArithmeticType arithmeticType) { - if(ssa.hasStructs()) { + public static XCFA createXCFA(SSAProvider ssa, List procedurePasses, ArithmeticType arithmeticType) { + if (ssa.hasStructs()) { throw new UnsupportedOperationException("Structs are not yet supported!"); } - if(arithmeticType == ArithmeticType.efficient && ssa.shouldUseBitwiseArithmetics()){ + if (arithmeticType == ArithmeticType.efficient && ssa.shouldUseBitwiseArithmetics()) { System.out.println("Using bitvector arithmetic!"); arithmeticType = ArithmeticType.bitvector; - } - else if(arithmeticType == ArithmeticType.efficient) { + } else if (arithmeticType == ArithmeticType.efficient) { System.out.println("Using integer arithmetic!"); arithmeticType = ArithmeticType.integer; } @@ -106,7 +100,7 @@ else if(arithmeticType == ArithmeticType.efficient) { GlobalState globalState = new GlobalState(ssa, arithmeticType); for (Tuple3, List>> function : ssa.getFunctions()) { - if(function.get1().equals("reach_error")) continue; + if (function.get1().equals("reach_error")) continue; FunctionState functionState = new FunctionState(globalState, function); for (String block : ssa.getBlocks(function.get1())) { @@ -130,43 +124,45 @@ else if(arithmeticType == ArithmeticType.efficient) { } builtState.getProcedures().put(function.get1(), functionState.getProcedureBuilder()); - } - if(builtState.getProcedures().size() > 1) { - System.err.println("Inlining failed."); - System.exit(-80); } - - builtState.getProcedures().forEach((s, builder) -> { - if(builder.getErrorLoc() == null) { - System.err.println("Frontend failed"); - System.exit(-80); - } - }); - - final XCFA.Builder builder = globalState.getBuilder(); - - return new XCFA(builder.getGlobalVars(), - List.of( - xcfa -> new XcfaProcess("proc", - List.of(), - Map.of(), - builtState.getProcedures().entrySet().stream().map(e -> - (Function) - (XcfaProcess xcfaProc) -> new XcfaProcedure( - e.getKey(), - Map.of(), - e.getValue().getLocalVars(), - e.getValue().getLocs(), - e.getValue().getRetType(), - e.getValue().getInitLoc(), - e.getValue().getErrorLoc(), - e.getValue().getFinalLoc(), - e.getValue().getEdges(), - xcfaProc) - ).collect(Collectors.toList()), - xcfa)), - "xcfa", - true); + return globalState.getBuilder().build(); } +// +// if(builtState.getProcedures().size() > 1) { +// System.err.println("Inlining failed."); +// System.exit(-80); +// } +// +// builtState.getProcedures().forEach((s, builder) -> { +// if(builder.getErrorLoc() == null) { +// System.err.println("Frontend failed"); +// System.exit(-80); +// } +// }); +// +// final XCFA.Builder builder = globalState.getBuilder(); +// +// return new XCFA(builder.getGlobalVars(), +// List.of( +// xcfa -> new XcfaProcess("proc", +// List.of(), +// Map.of(), +// builtState.getProcedures().entrySet().stream().map(e -> +// (Function) +// (XcfaProcess xcfaProc) -> new XcfaProcedure( +// e.getKey(), +// Map.of(), +// e.getValue().getLocalVars(), +// e.getValue().getLocs(), +// e.getValue().getRetType(), +// e.getValue().getInitLoc(), +// e.getValue().getErrorLoc(), +// e.getValue().getFinalLoc(), +// e.getValue().getEdges(), +// xcfaProc) +// ).collect(Collectors.toList()), +// xcfa)), +// "xcfa", +// true); } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/Utils.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/Utils.java index 1bb7bb9e40..e594e8a74c 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/Utils.java +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/Utils.java @@ -31,8 +31,7 @@ import hu.bme.mit.theta.core.type.rattype.RatType; import hu.bme.mit.theta.core.utils.BvUtils; import hu.bme.mit.theta.frontend.FrontendMetadata; -import hu.bme.mit.theta.xcfa.model.XcfaEdge; -import hu.bme.mit.theta.xcfa.model.XcfaLocation; +import hu.bme.mit.theta.xcfa.model.*; import hu.bme.mit.theta.xcfa.ir.handlers.Instruction; import hu.bme.mit.theta.xcfa.ir.handlers.arguments.Argument; import hu.bme.mit.theta.xcfa.ir.handlers.arguments.LocalArgument; @@ -150,7 +149,7 @@ public static VarDecl getOrCreateVar(FunctionState functionState, Argument re Tuple2, Integer> objects = functionState.getLocalVars().get(regArgument.getName()); if(objects == null) { var = Var(regArgument.getName(), regArgument.getType()); - functionState.getProcedureBuilder().getLocalVars().put(var, Optional.empty()); + functionState.getProcedureBuilder().getVars().add(var); functionState.getLocalVars().put(regArgument.getName(), Tuple2.of(var, 1)); functionState.getValues().put(regArgument.getName(), var.getRef()); return var; @@ -159,7 +158,7 @@ public static VarDecl getOrCreateVar(FunctionState functionState, Argument re objects = functionState.getLocalVars().get(typedName); if(objects == null) { var = Var(typedName, regArgument.getType()); - functionState.getProcedureBuilder().getLocalVars().put(var, Optional.empty()); + functionState.getProcedureBuilder().getVars().add(var); functionState.getLocalVars().put(typedName, Tuple2.of(var, 1)); functionState.getValues().put(typedName, var.getRef()); return var; @@ -175,14 +174,14 @@ public static void foldExpression(Instruction instruction, FunctionState functio //noinspection OptionalGetWithoutIsPresent RegArgument ret = instruction.getRetVar().get(); if(ret instanceof LocalArgument) { - XcfaLocation loc = XcfaLocation.create(blockState.getName() + "_" + blockState.getBlockCnt()); + XcfaLocation loc = new XcfaLocation(blockState.getName() + "_" + blockState.getBlockCnt()); VarDecl lhs = Utils.getOrCreateVar(functionState, ret); Stmt stmt = Assign(cast(lhs, lhs.getType()), cast(op, lhs.getType())); XcfaEdge edge; if(!lhs.getRef().equals(op)) - edge = XcfaEdge.create(blockState.getLastLocation(), loc, List.of(stmt)); + edge = new XcfaEdge(blockState.getLastLocation(), loc, new StmtLabel(stmt, EmptyMetaData.INSTANCE)); else - edge = XcfaEdge.create(blockState.getLastLocation(), loc, List.of()); + edge = new XcfaEdge(blockState.getLastLocation(), loc, NopLabel.INSTANCE); if(instruction.getLineNumber() >= 0) FrontendMetadata.create(edge, "lineNumber", instruction.getLineNumber()); functionState.getProcedureBuilder().addLoc(loc); functionState.getProcedureBuilder().addEdge(edge); diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/ArrayIntrinsicsHandler.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/ArrayIntrinsicsHandler.java index d46ea51ed6..f3fa1dab0d 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/ArrayIntrinsicsHandler.java +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/ArrayIntrinsicsHandler.java @@ -24,6 +24,8 @@ import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.frontend.FrontendMetadata; +import hu.bme.mit.theta.xcfa.model.EmptyMetaData; +import hu.bme.mit.theta.xcfa.model.StmtLabel; import hu.bme.mit.theta.xcfa.model.XcfaEdge; import hu.bme.mit.theta.xcfa.model.XcfaLocation; import hu.bme.mit.theta.xcfa.ir.handlers.BaseInstructionHandler; @@ -77,12 +79,12 @@ private void setArrayElement(Instruction instruction, GlobalState globalState, F checkState(arr.getType() instanceof ArrayType, "getArrayElement used on non-array type."); checkState(idx.getType() == IntType.getInstance(), "getArrayElement used with non-int index."); - XcfaLocation loc = XcfaLocation.create(blockState.getName() + "_" + blockState.getBlockCnt()); + XcfaLocation loc = new XcfaLocation(blockState.getName() + "_" + blockState.getBlockCnt()); VarDecl var = functionState.getLocalVars().get(arr.getName()).get1(); Expr expr = ArrayExprs.Write(cast(var.getRef(), ArrayType.of(Int(), val.getType())), cast(idx.getExpr(functionState.getValues()), Int()), cast(val.getExpr(functionState.getValues()), val.getType())); Stmt stmt = Assign(cast(var, var.getType()), cast(expr, var.getType())); - XcfaEdge edge = XcfaEdge.create(blockState.getLastLocation(), loc, List.of(stmt)); + XcfaEdge edge = new XcfaEdge(blockState.getLastLocation(), loc, new StmtLabel(stmt, EmptyMetaData.INSTANCE)); if(instruction.getLineNumber() >= 0) FrontendMetadata.create(edge, "lineNumber", instruction.getLineNumber()); functionState.getProcedureBuilder().addLoc(loc); functionState.getProcedureBuilder().addEdge(edge); diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/BuiltinFunctionHandler.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/BuiltinFunctionHandler.java index db589a0351..46762acf70 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/BuiltinFunctionHandler.java +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/BuiltinFunctionHandler.java @@ -17,6 +17,7 @@ package hu.bme.mit.theta.xcfa.ir.handlers.concrete; import hu.bme.mit.theta.frontend.FrontendMetadata; +import hu.bme.mit.theta.xcfa.model.NopLabel; import hu.bme.mit.theta.xcfa.model.XcfaEdge; import hu.bme.mit.theta.xcfa.model.XcfaLocation; import hu.bme.mit.theta.xcfa.ir.handlers.BaseInstructionHandler; @@ -51,12 +52,11 @@ public void handleInstruction(Instruction instruction, GlobalState globalState, } private void error(Instruction instruction, GlobalState globalState, FunctionState functionState, BlockState blockState) { - XcfaLocation newLoc = XcfaLocation.create(blockState.getName() + "_" + blockState.getBlockCnt()); - XcfaEdge edge = XcfaEdge.create(blockState.getLastLocation(), newLoc, List.of()); + functionState.getProcedureBuilder().createErrorLoc(); + XcfaLocation newLoc = functionState.getProcedureBuilder().getErrorLoc().get(); + XcfaEdge edge = new XcfaEdge(blockState.getLastLocation(), newLoc, NopLabel.INSTANCE); if (instruction.getLineNumber() >= 0) FrontendMetadata.create(edge, "lineNumber", instruction.getLineNumber()); - functionState.getProcedureBuilder().addLoc(newLoc); functionState.getProcedureBuilder().addEdge(edge); blockState.setLastLocation(newLoc); - functionState.getProcedureBuilder().setErrorLoc(newLoc); } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/MemoryInstructionHandler.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/MemoryInstructionHandler.java index 9e8cec9345..bea688f629 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/MemoryInstructionHandler.java +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/MemoryInstructionHandler.java @@ -20,6 +20,8 @@ import hu.bme.mit.theta.core.decl.VarDecl; import hu.bme.mit.theta.core.stmt.Stmt; import hu.bme.mit.theta.frontend.FrontendMetadata; +import hu.bme.mit.theta.xcfa.model.EmptyMetaData; +import hu.bme.mit.theta.xcfa.model.StmtLabel; import hu.bme.mit.theta.xcfa.model.XcfaEdge; import hu.bme.mit.theta.xcfa.model.XcfaLocation; import hu.bme.mit.theta.xcfa.ir.Utils; @@ -103,16 +105,16 @@ private void store(Instruction instruction, GlobalState globalState, FunctionSta } else if (oldVar.get2() == 1) { if (potentialParam != null && functionState.getParams().contains(potentialParam.get1())) { VarDecl var = functionState.getLocalVars().get(op2.getName()).get1(); - functionState.getProcedureBuilder().getLocalVars().remove(var); + functionState.getProcedureBuilder().getVars().remove(var); var = functionState.getLocalVars().get(op1.getName()).get1(); functionState.getLocalVars().put(op2.getName(), Tuple2.of(var, 0)); functionState.getValues().put(op1.getName(), var.getRef()); functionState.getValues().put(op2.getName(), var.getRef()); } else { - XcfaLocation loc = XcfaLocation.create(blockState.getName() + "_" + blockState.getBlockCnt()); + XcfaLocation loc = new XcfaLocation(blockState.getName() + "_" + blockState.getBlockCnt()); VarDecl var = functionState.getLocalVars().get(op2.getName()).get1(); Stmt stmt = Assign(cast(var, var.getType()), cast(op1.getExpr(functionState.getValues()), var.getType())); - XcfaEdge edge = XcfaEdge.create(blockState.getLastLocation(), loc, List.of(stmt)); + XcfaEdge edge = new XcfaEdge(blockState.getLastLocation(), loc, new StmtLabel(stmt, EmptyMetaData.INSTANCE)); if(instruction.getLineNumber() >= 0) FrontendMetadata.create(edge, "lineNumber", instruction.getLineNumber()); functionState.getProcedureBuilder().addLoc(loc); functionState.getProcedureBuilder().addEdge(edge); @@ -130,7 +132,7 @@ private void alloca(Instruction instruction, GlobalState globalState, FunctionSt Optional retVar = instruction.getRetVar(); checkState(retVar.isPresent(), "Alloca must have a variable tied to it"); VarDecl var = Var(retVar.get().getName(), retVar.get().getType()); - functionState.getProcedureBuilder().getLocalVars().put(var, Optional.empty()); + functionState.getProcedureBuilder().getVars().add(var); functionState.getLocalVars().put(retVar.get().getName(), Tuple2.of(var, 1)); functionState.getValues().put(retVar.get().getName(), var.getRef()); } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/OtherInstructionHandler.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/OtherInstructionHandler.java index e0cb4e8df5..e4136a453f 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/OtherInstructionHandler.java +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/OtherInstructionHandler.java @@ -36,6 +36,8 @@ import hu.bme.mit.theta.xcfa.ir.handlers.states.FunctionState; import hu.bme.mit.theta.xcfa.ir.handlers.states.GlobalState; import hu.bme.mit.theta.xcfa.ir.handlers.utils.PlaceholderAssignmentStmt; +import hu.bme.mit.theta.xcfa.model.EmptyMetaData; +import hu.bme.mit.theta.xcfa.model.StmtLabel; import hu.bme.mit.theta.xcfa.model.XcfaEdge; import hu.bme.mit.theta.xcfa.model.XcfaLocation; @@ -44,8 +46,7 @@ import java.util.Optional; import static com.google.common.base.Preconditions.checkState; -import static hu.bme.mit.theta.core.stmt.Stmts.Assign; -import static hu.bme.mit.theta.core.stmt.Stmts.Havoc; +import static hu.bme.mit.theta.core.stmt.Stmts.*; import static hu.bme.mit.theta.core.type.anytype.Exprs.Ite; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Geq; @@ -91,7 +92,7 @@ public void handleInstruction(Instruction instruction, GlobalState globalState, private void call(Instruction instruction, GlobalState globalState, FunctionState functionState, BlockState blockState) { Argument functionName = instruction.getArguments().get(instruction.getArguments().size() - 1); - XcfaLocation newLoc = XcfaLocation.create(blockState.getName() + "_" + blockState.getBlockCnt()); + XcfaLocation newLoc = new XcfaLocation(blockState.getName() + "_" + blockState.getBlockCnt()); if (globalState.getProcedures().stream().anyMatch(objects -> objects.get1().equals(functionName.getName()))) { System.err.println("More than one function."); System.exit(-80); @@ -105,7 +106,7 @@ private void call(Instruction instruction, GlobalState globalState, FunctionStat if (objects != null && objects.get2() > 0) stmts.add(havocVar(argument, functionState, blockState)); } - XcfaEdge edge = XcfaEdge.create(blockState.getLastLocation(), newLoc, stmts); + XcfaEdge edge = new XcfaEdge(blockState.getLastLocation(), newLoc, new StmtLabel(SequenceStmt(stmts), EmptyMetaData.INSTANCE)); if(instruction.getLineNumber() >= 0) FrontendMetadata.create(edge, "lineNumber", instruction.getLineNumber()); functionState.getProcedureBuilder().addLoc(newLoc); functionState.getProcedureBuilder().addEdge(edge); @@ -142,7 +143,7 @@ private void phi(Instruction instruction, GlobalState globalState, FunctionState Argument block = instruction.getArguments().get(2 * i + 1); Argument value = instruction.getArguments().get(2 * i); Tuple2 key = Tuple2.of(block.getName(), blockState.getName()); - Tuple4, Integer> val = functionState.getInterBlockEdges().getOrDefault(key, Tuple4.of(XcfaLocation.create(key.get1()), XcfaLocation.create(key.get2()), new ArrayList<>(), instruction.getLineNumber())); + Tuple4, Integer> val = functionState.getInterBlockEdges().getOrDefault(key, Tuple4.of(new XcfaLocation(key.get1()), new XcfaLocation(key.get2()), new ArrayList<>(), instruction.getLineNumber())); checkState(phiVar.getType().equals(value.getType()), "phiVar and value has to be of the same type!"); Stmt stmt; Expr expr; diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/TerminatorInstructionHandler.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/TerminatorInstructionHandler.java index cd0642a71f..9f37632dd3 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/TerminatorInstructionHandler.java +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/TerminatorInstructionHandler.java @@ -27,8 +27,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.frontend.FrontendMetadata; -import hu.bme.mit.theta.xcfa.model.XcfaEdge; -import hu.bme.mit.theta.xcfa.model.XcfaLocation; +import hu.bme.mit.theta.xcfa.model.*; import hu.bme.mit.theta.xcfa.ir.handlers.BaseInstructionHandler; import hu.bme.mit.theta.xcfa.ir.handlers.Instruction; import hu.bme.mit.theta.xcfa.ir.handlers.states.BlockState; @@ -76,10 +75,9 @@ public void handleInstruction(Instruction instruction, GlobalState globalState, } private void unreachable(Instruction instruction, GlobalState globalState, FunctionState functionState, BlockState blockState) { - XcfaLocation errLoc = XcfaLocation.create(blockState.getName() + "_" + blockState.getBlockCnt()); - functionState.getProcedureBuilder().addLoc(errLoc); - functionState.getProcedureBuilder().setErrorLoc(errLoc); - XcfaEdge edge = XcfaEdge.create(blockState.getLastLocation(), errLoc, List.of()); + functionState.getProcedureBuilder().createErrorLoc(); + XcfaLocation errLoc = functionState.getProcedureBuilder().getErrorLoc().get(); + XcfaEdge edge = new XcfaEdge(blockState.getLastLocation(), errLoc, NopLabel.INSTANCE); if(instruction.getLineNumber() >= 0) FrontendMetadata.create(edge, "lineNumber", instruction.getLineNumber()); functionState.getProcedureBuilder().addEdge(edge); blockState.setLastLocation(errLoc); @@ -87,23 +85,24 @@ private void unreachable(Instruction instruction, GlobalState globalState, Funct private void ret(Instruction instruction, GlobalState globalState, FunctionState functionState, BlockState blockState) { List stmts = new ArrayList<>(); - VarDecl retVar = functionState.getProcedureBuilder().getRetType() == null ? null : functionState.getProcedureBuilder().getParams().keySet().iterator().next(); - switch (instruction.getArguments().size()) { - case 0: - checkState(retVar == null, "Not returning a value from non-void function!"); - break; - case 1: - checkState(retVar != null, "Returning a value from void function!"); - Stmt assignStmt = Assign(cast(retVar, retVar.getType()), cast(instruction.getArguments().get(0).getExpr(functionState.getValues()), retVar.getType())); - stmts.add(assignStmt); - break; - default: - throw new IllegalStateException("Unexpected value: " + instruction.getArguments().size()); - } - XcfaEdge edge = XcfaEdge.create(blockState.getLastLocation(), functionState.getProcedureBuilder().getFinalLoc(), stmts); - if(instruction.getLineNumber() >= 0) FrontendMetadata.create(edge, "lineNumber", instruction.getLineNumber()); - functionState.getProcedureBuilder().addEdge(edge); - blockState.setLastLocation(functionState.getProcedureBuilder().getFinalLoc()); + throw new UnsupportedOperationException("Not yet ported!"); +// VarDecl retVar = functionState.getProcedureBuilder().getRetType() == null ? null : functionState.getProcedureBuilder().getParams().keySet().iterator().next(); +// switch (instruction.getArguments().size()) { +// case 0: +// checkState(retVar == null, "Not returning a value from non-void function!"); +// break; +// case 1: +// checkState(retVar != null, "Returning a value from void function!"); +// Stmt assignStmt = Assign(cast(retVar, retVar.getType()), cast(instruction.getArguments().get(0).getExpr(functionState.getValues()), retVar.getType())); +// stmts.add(assignStmt); +// break; +// default: +// throw new IllegalStateException("Unexpected value: " + instruction.getArguments().size()); +// } +// XcfaEdge edge = XcfaEdge.create(blockState.getLastLocation(), functionState.getProcedureBuilder().getFinalLoc(), stmts); +// if(instruction.getLineNumber() >= 0) FrontendMetadata.create(edge, "lineNumber", instruction.getLineNumber()); +// functionState.getProcedureBuilder().addEdge(edge); +// blockState.setLastLocation(functionState.getProcedureBuilder().getFinalLoc()); } private void br(Instruction instruction, GlobalState globalState, FunctionState functionState, BlockState blockState) { @@ -135,7 +134,7 @@ private void br(Instruction instruction, GlobalState globalState, FunctionState default: throw new IllegalStateException("Unexpected value: " + instruction.getArguments().size()); } - blockState.setLastLocation(functionState.getProcedureBuilder().getFinalLoc()); + blockState.setLastLocation(functionState.getProcedureBuilder().getFinalLoc().get()); } private void sw(Instruction instruction, GlobalState globalState, FunctionState functionState, BlockState blockState) { @@ -155,10 +154,10 @@ private void sw(Instruction instruction, GlobalState globalState, FunctionState functionState.getInterBlockEdges().put(key, Tuple4.of(blockState.getLastLocation(), loc, stmts, instruction.getLineNumber())); } XcfaLocation loc = functionState.getLocations().get(instruction.getArguments().get(1).getName()); - XcfaEdge edge = XcfaEdge.create(blockState.getLastLocation(), loc, List.of(Assume(BoolExprs.Not(defaultBranch)))); + XcfaEdge edge = new XcfaEdge(blockState.getLastLocation(), loc, new StmtLabel(Assume(BoolExprs.Not(defaultBranch)), EmptyMetaData.INSTANCE)); if(instruction.getLineNumber() >= 0) FrontendMetadata.create(edge, "lineNumber", instruction.getLineNumber()); functionState.getProcedureBuilder().addEdge(edge); - blockState.setLastLocation(functionState.getProcedureBuilder().getFinalLoc()); + blockState.setLastLocation(functionState.getProcedureBuilder().getFinalLoc().get()); } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/BuiltState.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/BuiltState.java index 667a8f6768..875eb61c14 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/BuiltState.java +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/BuiltState.java @@ -17,8 +17,7 @@ package hu.bme.mit.theta.xcfa.ir.handlers.states; import hu.bme.mit.theta.xcfa.model.XCFA; -import hu.bme.mit.theta.xcfa.model.XcfaProcedure; -import hu.bme.mit.theta.xcfa.model.XcfaProcess; +import hu.bme.mit.theta.xcfa.model.XcfaProcedureBuilder; import java.util.HashMap; import java.util.Map; @@ -27,11 +26,9 @@ public class BuiltState { private XCFA xcfa; - private Map processes; - private Map procedures; + private Map procedures; public BuiltState() { - processes = new HashMap<>(); procedures = new HashMap<>(); } @@ -44,19 +41,11 @@ public void setXcfa(XCFA xcfa) { this.xcfa = xcfa; } - public Map getProcesses() { - return processes; - } - - public void setProcesses(Map processes) { - this.processes = processes; - } - - public Map getProcedures() { + public Map getProcedures() { return procedures; } - public void setProcedures(Map procedures) { + public void setProcedures(Map procedures) { this.procedures = procedures; } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/FunctionState.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/FunctionState.java index aed4357991..a0a993d06d 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/FunctionState.java +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/FunctionState.java @@ -20,13 +20,13 @@ import hu.bme.mit.theta.common.Tuple3; import hu.bme.mit.theta.common.Tuple4; import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.stmt.SequenceStmt; import hu.bme.mit.theta.core.stmt.Stmt; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.frontend.FrontendMetadata; -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.*; import hu.bme.mit.theta.xcfa.ir.handlers.utils.PlaceholderAssignmentStmt; +import hu.bme.mit.theta.xcfa.passes.ProcedurePassManager; import java.util.HashMap; import java.util.HashSet; @@ -42,7 +42,7 @@ public class FunctionState { private final GlobalState globalState; private final Tuple3, List>> function; - private final XcfaProcedure.Builder procedureBuilder; + private final XcfaProcedureBuilder procedureBuilder; private final Map, Integer>> localVars; private final Set> params; private final Map> values; @@ -52,8 +52,8 @@ public class FunctionState { public FunctionState(GlobalState globalState, Tuple3, List>> function) { this.globalState = globalState; this.function = function; - procedureBuilder = XcfaProcedure.builder(); - procedureBuilder.setName(function.get1()); + procedureBuilder = new XcfaProcedureBuilder(function.get1(), new ProcedurePassManager(List.of())); +// procedureBuilder.setName(function.get1()); localVars = new HashMap<>(); params = new HashSet<>(); values = new HashMap<>(); @@ -64,37 +64,38 @@ public FunctionState(GlobalState globalState, Tuple3, L // Adding return variable if (function.get2().isPresent()) { VarDecl var = createVariable(function.get1() + "_ret", function.get2().get()); - procedureBuilder.createParam(XcfaProcedure.Direction.OUT, var); + procedureBuilder.addParam(var, ParamDirection.OUT); localVars.put(function.get1() + "_ret", Tuple2.of(var, 1)); params.add(var); - procedureBuilder.setRetType(var.getType()); +// procedureBuilder.setRetType(var.getType()); } // Adding params for (Tuple2 param : function.get3()) { VarDecl var = createVariable(param.get2(), param.get1()); - procedureBuilder.createParam(XcfaProcedure.Direction.INOUT, var); + procedureBuilder.addParam(var, ParamDirection.INOUT); localVars.put(param.get2(), Tuple2.of(var, 1)); params.add(var); } // Adding final location - XcfaLocation finalLoc = XcfaLocation.create(function.get1() + "_final"); - procedureBuilder.addLoc(finalLoc); - procedureBuilder.setFinalLoc(finalLoc); + procedureBuilder.createFinalLoc(); // Adding blocks and first location List blocks = globalState.getProvider().getBlocks(function.get1()); locations = new LinkedHashMap<>(); boolean first = true; for (String block : blocks) { - XcfaLocation loc = XcfaLocation.create(block); - locations.put(block, loc); - procedureBuilder.addLoc(loc); + XcfaLocation loc; if (first) { - procedureBuilder.setInitLoc(loc); + procedureBuilder.createInitLoc(); + loc = procedureBuilder.getInitLoc(); first = false; + } else { + loc = new XcfaLocation(block); + procedureBuilder.addLoc(loc); } + locations.put(block, loc); } localVars.forEach((s, var) -> values.put(s, var.get1().getRef())); @@ -111,7 +112,7 @@ public void finalizeFunctionState(BuiltState builtState) { } return stmt; }).collect(Collectors.toUnmodifiableList()); - XcfaEdge edge = XcfaEdge.create(edgeTup.get1(), edgeTup.get2(), stmts); + XcfaEdge edge = new XcfaEdge(edgeTup.get1(), edgeTup.get2(), new StmtLabel(SequenceStmt.of(stmts), EmptyMetaData.INSTANCE)); if(edgeTup.get4() >= 0) FrontendMetadata.create(edge, "lineNumber", edgeTup.get4()); procedureBuilder.addEdge(edge); }); @@ -125,7 +126,7 @@ public Tuple3, List>> getFunctio return function; } - public XcfaProcedure.Builder getProcedureBuilder() { + public XcfaProcedureBuilder getProcedureBuilder() { return procedureBuilder; } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/GlobalState.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/GlobalState.java index 4e05e78911..aa1a32a4f8 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/GlobalState.java +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/GlobalState.java @@ -22,6 +22,8 @@ import hu.bme.mit.theta.xcfa.ir.ArithmeticType; import hu.bme.mit.theta.xcfa.ir.SSAProvider; import hu.bme.mit.theta.xcfa.model.XCFA; +import hu.bme.mit.theta.xcfa.model.XcfaBuilder; +import hu.bme.mit.theta.xcfa.model.XcfaGlobalVar; import java.util.ArrayList; import java.util.HashMap; @@ -34,7 +36,7 @@ import static hu.bme.mit.theta.xcfa.ir.Utils.createVariable; public class GlobalState { - private final XCFA.Builder builder; + private final XcfaBuilder builder; private final Map> globalVars; private final List, List>>> procedures; private final SSAProvider ssa; @@ -44,8 +46,7 @@ public class GlobalState { public GlobalState(SSAProvider ssa, ArithmeticType arithmeticType) { this.ssa = ssa; this.arithmeticType = arithmeticType; - builder = XCFA.builder(); - builder.setDynamic(true); + builder = new XcfaBuilder("llvm"); this.globalVars = new HashMap<>(); this.procedures = new ArrayList<>(); @@ -53,7 +54,7 @@ public GlobalState(SSAProvider ssa, ArithmeticType arithmeticType) { for (Tuple3 globalVariable : ssa.getGlobalVariables()) { VarDecl variable = createVariable(globalVariable.get1(), globalVariable.get2()); globalVars.put(globalVariable.get1(), variable); - builder.getGlobalVars().put(variable, Optional.of(createConstant(variable.getType(), globalVariable.get3()))); + builder.addVar(new XcfaGlobalVar(variable, createConstant(variable.getType(), globalVariable.get3()))); } procedures.addAll(ssa.getFunctions()); @@ -88,7 +89,7 @@ public SSAProvider getProvider() { return ssa; } - public XCFA.Builder getBuilder() { + public XcfaBuilder getBuilder() { return builder; } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt index c168f61f80..ec2044ed37 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/Builders.kt @@ -133,26 +133,29 @@ class XcfaProcedureBuilder @JvmOverloads constructor( @JvmOverloads fun createErrorLoc(metaData: MetaData = EmptyMetaData) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - errorLoc = Optional.of(XcfaLocation(name + "_error", error = true, metadata = metaData)) - locs.add(errorLoc.get()) + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + if (errorLoc.isEmpty) { + errorLoc = Optional.of(XcfaLocation(name + "_error", error = true, metadata = metaData)) + locs.add(errorLoc.get()) + } } @JvmOverloads fun createFinalLoc(metaData: MetaData = EmptyMetaData) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - finalLoc = Optional.of(XcfaLocation(name + "_final", final = true, metadata = metaData)) - locs.add(finalLoc.get()) + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + if(finalLoc.isEmpty) { + finalLoc = Optional.of(XcfaLocation(name + "_final", final = true, metadata = metaData)) + locs.add(finalLoc.get()) + } } @JvmOverloads fun createInitLoc(metaData: MetaData = EmptyMetaData) { - check( - !this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } - initLoc = XcfaLocation(name + "_init", initial = true, metadata = metaData) - locs.add(initLoc) + check(!this::optimized.isInitialized) { "Cannot add/remove new elements after optimization passes!" } + if (!this::initLoc.isInitialized) { + initLoc = XcfaLocation(name + "_init", initial = true, metadata = metaData) + locs.add(initLoc) + } } fun addEdge(toAdd: XcfaEdge) {