Skip to content

Commit

Permalink
Made LLVM parts compile
Browse files Browse the repository at this point in the history
  • Loading branch information
@leventeBajczi
leventeBajczi committed Jul 23, 2023
1 parent c61d04b commit 2fc7c22
Show file tree
Hide file tree
Showing 11 changed files with 140 additions and 147 deletions.
94 changes: 45 additions & 49 deletions subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaUtils.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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<XcfaPass> xcfaPasses, List<ProcessPass> processPasses, List<ProcedurePass> procedurePasses, ArithmeticType arithmeticType) {
if(ssa.hasStructs()) {
public static XCFA createXCFA(SSAProvider ssa, List<ProcedurePass> 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;
}
Expand All @@ -106,7 +100,7 @@ else if(arithmeticType == ArithmeticType.efficient) {
GlobalState globalState = new GlobalState(ssa, arithmeticType);

for (Tuple3<String, Optional<String>, List<Tuple2<String, String>>> 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())) {
Expand All @@ -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, XcfaProcedure>)
(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, XcfaProcedure>)
// (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);
}
13 changes: 6 additions & 7 deletions subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/Utils.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -150,7 +149,7 @@ public static VarDecl<?> getOrCreateVar(FunctionState functionState, Argument re
Tuple2<VarDecl<?>, 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;
Expand All @@ -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;
Expand All @@ -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);
Expand Down
6 changes: 4 additions & 2 deletions ...xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/ArrayIntrinsicsHandler.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
Expand Down
8 changes: 4 additions & 4 deletions ...xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/BuiltinFunctionHandler.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
}
}
10 changes: 6 additions & 4 deletions ...fa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/MemoryInstructionHandler.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
Expand All @@ -130,7 +132,7 @@ private void alloca(Instruction instruction, GlobalState globalState, FunctionSt
Optional<RegArgument> 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());
}
Expand Down
Loading

0 comments on commit 2fc7c22

Please sign in to comment.