From 98601e42fe53ce93dd66e8d920cb20afa40fa6c1 Mon Sep 17 00:00:00 2001 From: Levente Bajczi Date: Fri, 14 Jan 2022 19:38:42 +0100 Subject: [PATCH 01/21] Added back LLVM stuff --- .../java/hu/bme/mit/theta/xcfa/XcfaUtils.java | 164 ++++++++ .../bme/mit/theta/xcfa/ir/ArithmeticType.java | 24 ++ .../bme/mit/theta/xcfa/ir/LlvmIrProvider.java | 227 +++++++++++ .../java/hu/bme/mit/theta/xcfa/ir/Readme.md | 113 ++++++ .../hu/bme/mit/theta/xcfa/ir/SSAProvider.java | 72 ++++ .../java/hu/bme/mit/theta/xcfa/ir/Utils.java | 199 ++++++++++ .../ir/handlers/BaseInstructionHandler.java | 36 ++ .../theta/xcfa/ir/handlers/Instruction.java | 76 ++++ .../xcfa/ir/handlers/InstructionHandler.java | 29 ++ .../handlers/InstructionHandlerManager.java | 97 +++++ .../xcfa/ir/handlers/arguments/Argument.java | 51 +++ .../handlers/arguments/ConstantArgument.java | 48 +++ .../ir/handlers/arguments/LabelArgument.java | 45 +++ .../ir/handlers/arguments/LocalArgument.java | 23 ++ .../ir/handlers/arguments/RegArgument.java | 49 +++ .../ir/handlers/arguments/StringArgument.java | 45 +++ .../concrete/AggregateInstructionHandler.java | 49 +++ .../concrete/ArrayIntrinsicsHandler.java | 93 +++++ .../concrete/BinaryInstructionHandler.java | 184 +++++++++ .../concrete/BitvectorInstructionHandler.java | 368 ++++++++++++++++++ .../concrete/BitwiseInstructionHandler.java | 107 +++++ .../concrete/BuiltinFunctionHandler.java | 62 +++ .../ConversionInstructionHandler.java | 147 +++++++ .../concrete/MemoryInstructionHandler.java | 137 +++++++ .../concrete/OtherInstructionHandler.java | 244 ++++++++++++ .../TerminatorInstructionHandler.java | 165 ++++++++ .../concrete/UnaryInstructionHandler.java | 54 +++ .../concrete/VectorInstructionHandler.java | 52 +++ .../checks/PointerArithmeticCheck.java | 38 ++ .../xcfa/ir/handlers/states/BlockState.java | 54 +++ .../xcfa/ir/handlers/states/BuiltState.java | 62 +++ .../ir/handlers/states/FunctionState.java | 152 ++++++++ .../xcfa/ir/handlers/states/GlobalState.java | 98 +++++ .../utils/PlaceholderAssignmentStmt.java | 64 +++ 34 files changed, 3428 insertions(+) create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaUtils.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/ArithmeticType.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/LlvmIrProvider.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/Readme.md create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/SSAProvider.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/Utils.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/BaseInstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/Instruction.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/InstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/InstructionHandlerManager.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/arguments/Argument.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/arguments/ConstantArgument.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/arguments/LabelArgument.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/arguments/LocalArgument.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/arguments/RegArgument.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/arguments/StringArgument.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/AggregateInstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/ArrayIntrinsicsHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/BinaryInstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/BitvectorInstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/BitwiseInstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/BuiltinFunctionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/ConversionInstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/MemoryInstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/OtherInstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/TerminatorInstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/UnaryInstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/VectorInstructionHandler.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/concrete/checks/PointerArithmeticCheck.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/BlockState.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/BuiltState.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/FunctionState.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/states/GlobalState.java create mode 100644 subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/handlers/utils/PlaceholderAssignmentStmt.java 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 new file mode 100644 index 0000000000..1b43c0ee12 --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/XcfaUtils.java @@ -0,0 +1,164 @@ +/* + * Copyright 2021 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.xcfa; + +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.common.Tuple3; +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; +import hu.bme.mit.theta.xcfa.ir.Utils; +import hu.bme.mit.theta.xcfa.ir.handlers.Instruction; +import hu.bme.mit.theta.xcfa.ir.handlers.InstructionHandler; +import hu.bme.mit.theta.xcfa.ir.handlers.InstructionHandlerManager; +import hu.bme.mit.theta.xcfa.ir.handlers.states.BlockState; +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 java.io.File; +import java.io.FileNotFoundException; +import java.io.IOException; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.function.Function; +import java.util.stream.Collectors; + +import static com.google.common.base.Preconditions.checkState; + +@SuppressWarnings("unused") +public class XcfaUtils { + /* + * Creates an XCFA from the specified file. + * This is the recommended method for getting an XCFA instance. + * Supports .ll, .bc, .c and .i files. + */ + public static XCFA fromFile(File model, ArithmeticType arithmeticType) throws IOException { + + if (!model.exists()) throw new FileNotFoundException(); + + if (model.getName().endsWith(".ll") || model.getName().endsWith(".bc")) { + return createXCFA(new LlvmIrProvider(model.getAbsolutePath()), arithmeticType); + + } else if (model.getName().endsWith(".c") || model.getName().endsWith(".i")) { + return createXCFA(new LlvmIrProvider(model.getAbsolutePath(), true, true, true, true), arithmeticType); + + } else { + String[] split = model.getName().split("\\."); + if (split.length > 0) + throw new RuntimeException("File type " + split[split.length - 1] + " not supported."); + throw new RuntimeException("File does not have an extension."); + + } + } + + /* + * 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); + } + + /* + * 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()) { + throw new UnsupportedOperationException("Structs are not yet supported!"); + } + + if(arithmeticType == ArithmeticType.efficient && ssa.shouldUseBitwiseArithmetics()){ + System.out.println("Using bitvector arithmetic!"); + arithmeticType = ArithmeticType.bitvector; + } + else if(arithmeticType == ArithmeticType.efficient) { + System.out.println("Using integer arithmetic!"); + arithmeticType = ArithmeticType.integer; + } + checkState(!ssa.shouldUseBitwiseArithmetics() || arithmeticType == ArithmeticType.bitvector, "There are statements in the source not mappable to integer arithmetic"); + Utils.arithmeticType = arithmeticType; + BuiltState builtState = new BuiltState(); + GlobalState globalState = new GlobalState(ssa, arithmeticType); + + for (Tuple3, List>> function : ssa.getFunctions()) { + FunctionState functionState = new FunctionState(globalState, function); + + for (String block : ssa.getBlocks(function.get1())) { + BlockState blockState = new BlockState(functionState, block); + InstructionHandlerManager instructionHandlerManager = new InstructionHandlerManager(arithmeticType); + for (Tuple4>, List, String>>, Integer> instruction : ssa.getInstructions(function.get1(), block)) { + try { + InstructionHandler instructionHandler = instructionHandlerManager.createInstructionHandlers(); + instructionHandler.handleInstruction(new Instruction(instruction), globalState, functionState, blockState); + } catch (ReflectiveOperationException e) { + e.printStackTrace(); + } + + } + } + + functionState.finalizeFunctionState(builtState); + + for (ProcedurePass procedurePass : procedurePasses) { + procedurePass.run(functionState.getProcedureBuilder()); + } + + builtState.getProcedures().put(function.get1(), functionState.getProcedureBuilder()); + } + + if(builtState.getProcedures().size() > 1) { + System.err.println("Inlining 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/ArithmeticType.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/ArithmeticType.java new file mode 100644 index 0000000000..bcb7d6862d --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/ArithmeticType.java @@ -0,0 +1,24 @@ +/* + * Copyright 2021 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.xcfa.ir; + +public enum ArithmeticType { + integer, +// integer_modulo, + bitvector, + efficient +} \ No newline at end of file diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/LlvmIrProvider.java b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/LlvmIrProvider.java new file mode 100644 index 0000000000..19bd08a1f2 --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/LlvmIrProvider.java @@ -0,0 +1,227 @@ +/* + * Copyright 2021 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.xcfa.ir; + +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.common.Tuple3; +import hu.bme.mit.theta.common.Tuple4; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Optional; + +public class LlvmIrProvider implements SSAProvider { + static { + System.loadLibrary("theta-c-frontend"); + } + + private final Map, Integer> bbNamefuncIndexLut; // key: BasicBlock name, value: index of function in module + + public LlvmIrProvider(String irFilename) { + this(irFilename, true, true, true, true); + } + + public LlvmIrProvider(String irFilename, Boolean inlining, Boolean cleanup, Boolean optimization, Boolean debugPrintIr) { + if (!inlining) { + JniDisableInlining(); + } + if (!cleanup) { + JniDisableCleanupPasses(); + } + if (!optimization) { + JniDisableOptimizationPasses(); + } + if (!debugPrintIr) { + JniDisablePrintDebugIr(); + } + + JniParseIr(irFilename); + bbNamefuncIndexLut = new HashMap<>(); + + int numOfFunctions = JniGetFunctionsNum(); + + for (int f = 0; f < numOfFunctions; f++) { + String functionName = JniGetFunctionName(f); + int numOfBasicBlocks = JniGetNumOfBasicBlocks(f); + + for (int b = 0; b < numOfBasicBlocks; b++) { + bbNamefuncIndexLut.put(Tuple2.of(functionName, JniGetBlockName(f, b)), f); + } + } + + } + + private native void JniParseIr(String irFilename); + + private native void JniDisableInlining(); + + private native void JniDisableOptimizationPasses(); + + private native void JniDisableCleanupPasses(); + + private native void JniDisablePrintDebugIr(); + + private native int JniGetGlobalVariablesNum(); + + private native String JniGetGlobalVariableName(int gvIndex); + + private native String JniGetGlobalVariableType(int gvIndex); + + private native String JniGetGlobalVariableValue(int gvIndex); + + // Format: Tuple3 + @Override + public Collection> getGlobalVariables() { + int numOfGlobalVar = JniGetGlobalVariablesNum(); + Tuple3 globalVar; + ArrayList> globalVarList = new ArrayList>(); + + for (int i = 0; i < numOfGlobalVar; i++) { + globalVar = Tuple3.of( + JniGetGlobalVariableName(i), + JniGetGlobalVariableType(i), + JniGetGlobalVariableValue(i) + ); + globalVarList.add(globalVar); + } + return globalVarList; + } + + private native int JniGetFunctionsNum(); + + private native String JniGetFunctionRetType(int funcIndex); + + private native String JniGetFunctionName(int funcIndex); + + private native int JniGetNumOfFunctionParameters(int funcIndex); + + private native String JniGetParameterType(int funcIndex, int paramIndex); + + private native String JniGetParameterName(int funcIndex, int paramIndex); + + @Override + public Collection, List>>> getFunctions() { + int numOfFunctions = JniGetFunctionsNum(); + ArrayList, List>>> functions = new ArrayList<>(); + + for (int f = 0; f < numOfFunctions; f++) { + String functionName = JniGetFunctionName(f); + String retType = JniGetFunctionRetType(f); // TODO make this really optional? (->when void) + int numOfParams = JniGetNumOfFunctionParameters(f); + + ArrayList> parameters = new ArrayList<>(); + for (int p = 0; p < numOfParams; p++) { + String paramType = JniGetParameterType(f, p); + String paramName = JniGetParameterName(f, p); + parameters.add(Tuple2.of(paramType, paramName)); + } + if (retType.equals("void")) { + functions.add(Tuple3.of(functionName, Optional.empty(), parameters)); + } else { + functions.add(Tuple3.of(functionName, Optional.of(retType), parameters)); + } + } + return functions; + } + + private native int JniGetNumOfBasicBlocks(int funcIndex); + + private native int JniGetFunctionIndex(String funcName); + + private native String JniGetBlockName(int funcIndex, int BasicBlockIndex); + + @Override + public List getBlocks(String funcName) { + int f = JniGetFunctionIndex(funcName); + int numOfBasicBlocks = JniGetNumOfBasicBlocks(f); + ArrayList blocks = new ArrayList<>(); + for (int b = 0; b < numOfBasicBlocks; b++) { + blocks.add(JniGetBlockName(f, b)); + } + return blocks; + } + + private native int JniGetBlockIndex(int functionIndex, String blockName); + + private native int JniGetNumOfInstructions(int functionIndex, int basicBlockIndex); + + private native int JniGetInstructionLineNumber(int functionIndex, int basicBlockIndex, int i); + + private native String JniGetInstructionOpcode(int functionIndex, int basicBlockIndex, int i); + + private native String JniGetInstructionRetType(int functionIndex, int basicBlockIndex, int i); + + private native String JniGetInstructionRetName(int functionIndex, int basicBlockIndex, int i); + + private native int JniGetInstructionNumOfOperands(int functionIndex, int basicBlockIndex, int i); + + private native String JniGetInstructionOperandVarType(int functionIndex, int basicBlockIndex, int i, int o); + + private native String JniGetInstructionOperandVarName(int functionIndex, int basicBlockIndex, int i, int o); + + @Override + public List>, List, String>>, Integer>> getInstructions(String funcName, String blockName) { + int functionIndex = bbNamefuncIndexLut.get(Tuple2.of(funcName, blockName)); + int basicBlockIndex = JniGetBlockIndex(functionIndex, blockName); + int numOfInstructions = JniGetNumOfInstructions(functionIndex, basicBlockIndex); + + ArrayList>, List, String>>, Integer>> instructions = new ArrayList<>(); + for (int i = 0; i < numOfInstructions; i++) { + int lineNumber = JniGetInstructionLineNumber(functionIndex, basicBlockIndex, i); + String opcode = JniGetInstructionOpcode(functionIndex, basicBlockIndex, i); + String retType = JniGetInstructionRetType(functionIndex, basicBlockIndex, i); + String retVar = JniGetInstructionRetName(functionIndex, basicBlockIndex, i); + int numOfOperands = JniGetInstructionNumOfOperands(functionIndex, basicBlockIndex, i); + ArrayList, String>> instructionOperands = new ArrayList<>(); + for (int o = 0; o < numOfOperands; o++) { + String varType = JniGetInstructionOperandVarType(functionIndex, basicBlockIndex, i, o); + String varName = JniGetInstructionOperandVarName(functionIndex, basicBlockIndex, i, o); + if (varType.equals("constant")) { + instructionOperands.add(Tuple2.of(Optional.empty(), varName)); + } else { + instructionOperands.add(Tuple2.of(Optional.of(varType), varName)); + } + } + + if (retType.equals("")) { + instructions.add(Tuple4.of(opcode, Optional.empty(), instructionOperands, lineNumber)); + } else { + instructions.add(Tuple4.of(opcode, Optional.of(Tuple2.of(retType, retVar)), instructionOperands, lineNumber)); + } + } + + return instructions; + } + + private native boolean JniGetStructAnalysisResult(); + + @Override + public boolean hasStructs() { + return JniGetStructAnalysisResult(); + } + + private native boolean JniGetBitwiseArithmeticAnalysisResult(); + + @Override + public boolean shouldUseBitwiseArithmetics() { + return JniGetBitwiseArithmeticAnalysisResult(); + } + +} \ No newline at end of file diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/Readme.md b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/Readme.md new file mode 100644 index 0000000000..0f6977101a --- /dev/null +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/ir/Readme.md @@ -0,0 +1,113 @@ +# LLVM Instruction mapping + +These tables detail the currently supported LLVM instructions and their corresponding model elements. Note, that a +dash (`-`) denotes an instruction that is recognized but _won't_ cause any alteration to the model (because it is +out-of-scope), while a `TODO` label means that it currently produces an error to use the instruction, but should be +handled accordingly. + +## Terminator Instructions + +| LLVM Instructions | Handled versions | Resulting model element(s)| +| --- | --- | --- | +|`ret` | 1. `ret`
2. `ret ` | 1. Edge to final location
2. Assignment to return variable, edge to final location +|`br` | 1. `br