From 39db5d6144fa99b52c2cb64220d0286f1a4f023c Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Mon, 18 Nov 2024 13:09:28 +0100 Subject: [PATCH 01/13] Added node for Pallas FunctionContracts --- src/col/vct/col/ast/Node.scala | 11 +- .../lang/llvm/LLVMFunctionContractImpl.scala | 9 - .../llvm/PallasFunctionContractImpl.scala | 8 + .../llvm/VCLLVMFunctionContractImpl.scala | 8 + .../unsorted/LLVMFunctionContractImpl.scala | 10 + src/col/vct/col/resolve/Resolve.scala | 37 +-- src/col/vct/col/resolve/lang/LLVM.scala | 10 +- .../PallasFunctionContractDeclarerPass.h | 79 ++++++ src/llvm/include/Util/Constants.h | 8 + .../Function/FunctionBodyTransformer.cpp | 16 +- .../Function/FunctionContractDeclarer.cpp | 18 +- .../lib/Passes/Function/FunctionDeclarer.cpp | 4 +- .../PallasFunctionContractDeclarerPass.cpp | 228 ++++++++++++++++++ src/llvm/lib/Plugin.cpp | 8 +- src/main/vct/main/stages/Resolution.scala | 4 +- .../vct/parsers/parser/ColLLVMParser.scala | 2 +- .../vct/rewrite/lang/LangLLVMToCol.scala | 8 +- 17 files changed, 418 insertions(+), 50 deletions(-) delete mode 100644 src/col/vct/col/ast/lang/llvm/LLVMFunctionContractImpl.scala create mode 100644 src/col/vct/col/ast/lang/llvm/PallasFunctionContractImpl.scala create mode 100644 src/col/vct/col/ast/lang/llvm/VCLLVMFunctionContractImpl.scala create mode 100644 src/col/vct/col/ast/unsorted/LLVMFunctionContractImpl.scala create mode 100644 src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h create mode 100644 src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala index cd8be8ef78..b7411fa945 100644 --- a/src/col/vct/col/ast/Node.scala +++ b/src/col/vct/col/ast/Node.scala @@ -3492,15 +3492,22 @@ final case class BipTransitionSynchronization[G]( extends GlobalDeclaration[G] with BipTransitionSynchronizationImpl[G] @family -final class LLVMFunctionContract[G]( +sealed trait LLVMFunctionContract[G] + extends NodeFamily[G] with LLVMFunctionContractImpl[G] + +final class VCLLVMFunctionContract[G]( val name: String, val value: String, val variableRefs: Seq[(String, Ref[G, Variable[G]])], val invokableRefs: Seq[(String, Ref[G, LLVMCallable[G]])], )(val blame: Blame[NontrivialUnsatisfiable])(implicit val o: Origin) - extends NodeFamily[G] with LLVMFunctionContractImpl[G] { + extends LLVMFunctionContract[G] with VCLLVMFunctionContractImpl[G] { var data: Option[ApplicableContract[G]] = None } +final class PallasFunctionContract[G](val content: ApplicableContract[G])( + val blame: Blame[NontrivialUnsatisfiable] +)(implicit val o: Origin) + extends LLVMFunctionContract[G] with PallasFunctionContractImpl[G] {} final case class LLVMGlobalVariable[G]( variableType: Type[G], diff --git a/src/col/vct/col/ast/lang/llvm/LLVMFunctionContractImpl.scala b/src/col/vct/col/ast/lang/llvm/LLVMFunctionContractImpl.scala deleted file mode 100644 index 481e5689c7..0000000000 --- a/src/col/vct/col/ast/lang/llvm/LLVMFunctionContractImpl.scala +++ /dev/null @@ -1,9 +0,0 @@ -package vct.col.ast.lang.llvm - -import vct.col.ast.LLVMFunctionContract -import vct.col.ast.ops.{LLVMFunctionContractOps, LLVMFunctionContractFamilyOps} - -trait LLVMFunctionContractImpl[G] - extends LLVMFunctionContractOps[G] with LLVMFunctionContractFamilyOps[G] { - this: LLVMFunctionContract[G] => -} diff --git a/src/col/vct/col/ast/lang/llvm/PallasFunctionContractImpl.scala b/src/col/vct/col/ast/lang/llvm/PallasFunctionContractImpl.scala new file mode 100644 index 0000000000..69a054e0fd --- /dev/null +++ b/src/col/vct/col/ast/lang/llvm/PallasFunctionContractImpl.scala @@ -0,0 +1,8 @@ +package vct.col.ast.lang.llvm + +import vct.col.ast.PallasFunctionContract +import vct.col.ast.ops.PallasFunctionContractOps + +trait PallasFunctionContractImpl[G] extends PallasFunctionContractOps[G] { + this: PallasFunctionContract[G] => +} diff --git a/src/col/vct/col/ast/lang/llvm/VCLLVMFunctionContractImpl.scala b/src/col/vct/col/ast/lang/llvm/VCLLVMFunctionContractImpl.scala new file mode 100644 index 0000000000..4e86f29a9e --- /dev/null +++ b/src/col/vct/col/ast/lang/llvm/VCLLVMFunctionContractImpl.scala @@ -0,0 +1,8 @@ +package vct.col.ast.lang.llvm + +import vct.col.ast.VCLLVMFunctionContract +import vct.col.ast.ops.{VCLLVMFunctionContractOps} + +trait VCLLVMFunctionContractImpl[G] extends VCLLVMFunctionContractOps[G] { + this: VCLLVMFunctionContract[G] => +} diff --git a/src/col/vct/col/ast/unsorted/LLVMFunctionContractImpl.scala b/src/col/vct/col/ast/unsorted/LLVMFunctionContractImpl.scala new file mode 100644 index 0000000000..329c69ad02 --- /dev/null +++ b/src/col/vct/col/ast/unsorted/LLVMFunctionContractImpl.scala @@ -0,0 +1,10 @@ +package vct.col.ast.unsorted + +import vct.col.ast.LLVMFunctionContract +import vct.col.ast.ops.LLVMFunctionContractFamilyOps +import vct.col.print._ + +trait LLVMFunctionContractImpl[G] extends LLVMFunctionContractFamilyOps[G] { + this: LLVMFunctionContract[G] => + // override def layout(implicit ctx: Ctx): Doc = ??? +} diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala index d2852f3a46..9965b26ca8 100644 --- a/src/col/vct/col/resolve/Resolve.scala +++ b/src/col/vct/col/resolve/Resolve.scala @@ -45,7 +45,7 @@ case object Resolve { trait SpecContractParser { def parse[G]( - input: LLVMFunctionContract[G], + input: VCLLVMFunctionContract[G], o: Origin, ): ApplicableContract[G] @@ -1130,14 +1130,18 @@ case object ResolveReferences extends LazyLogging { portName.data = Some((cls, getLit(name))) case func: LLVMFunctionDefinition[G] => - val importedDecl = ctx.importedDeclarations.find { - case procedure: Procedure[G] => - func.contract.name == procedure.o.get[SourceName].name - } - if (importedDecl.isDefined) { - val importedProcedure = importedDecl.get.asInstanceOf[Procedure[G]] - func.importedArguments = Some(importedProcedure.args) - func.importedReturnType = Some(importedProcedure.returnType) + func.contract match { + case contract: VCLLVMFunctionContract[G] => + val importedDecl = ctx.importedDeclarations.find { + case procedure: Procedure[G] => + contract.name == procedure.o.get[SourceName].name + } + if (importedDecl.isDefined) { + val importedProcedure = importedDecl.get + .asInstanceOf[Procedure[G]] + func.importedArguments = Some(importedProcedure.args) + func.importedReturnType = Some(importedProcedure.returnType) + } } case loop: LLVMLoop[G] => loop.blocks = Some(loop.blockLabels.map { label => @@ -1151,7 +1155,7 @@ case object ResolveReferences extends LazyLogging { }) loop.headerBlock = Some(ctx.llvmBlocks(loop.header.decl)) loop.latchBlock = Some(ctx.llvmBlocks(loop.latch.decl)) - case contract: LLVMFunctionContract[G] => + case contract: VCLLVMFunctionContract[G] => // WONTFIX: // implicit val o: Origin = contract.o val llvmFunction = @@ -1192,14 +1196,19 @@ case object ResolveReferences extends LazyLogging { ) } else { contract.data = Some(applicableContract) } resolve(contract.data.get, ctx) + case contract: PallasFunctionContract[G] => resolve(contract.content, ctx) case local: LLVMLocal[G] => local.ref = ctx.currentResult.get match { case RefLLVMFunctionDefinition(decl) => - decl.contract.variableRefs - .find(ref => ref._1 == local.name) match { - case Some(ref) => Some(ref._2) - case None => throw NoSuchNameError("local", local.name, local) + decl.contract match { + case contract: VCLLVMFunctionContract[G] => + contract.variableRefs + .find(ref => ref._1 == local.name) match { + case Some(ref) => Some(ref._2) + case None => + throw NoSuchNameError("local", local.name, local) + } } case RefLLVMSpecFunction(_) => Some( diff --git a/src/col/vct/col/resolve/lang/LLVM.scala b/src/col/vct/col/resolve/lang/LLVM.scala index ca397c788d..1a28a42ff5 100644 --- a/src/col/vct/col/resolve/lang/LLVM.scala +++ b/src/col/vct/col/resolve/lang/LLVM.scala @@ -26,9 +26,13 @@ object LLVM { case None => ctx.currentResult.get match { case RefLLVMFunctionDefinition(decl) => - decl.contract.invokableRefs.find(ref => ref._1 == name) match { - case Some(ref) => Some(ref._2.decl) - case None => None + decl.contract match { + case contract: VCLLVMFunctionContract[_] => + contract.invokableRefs.find(ref => ref._1 == name) match { + case Some(ref) => Some(ref._2.decl) + case None => None + } + case _ => None } case _ => None } diff --git a/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h b/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h new file mode 100644 index 0000000000..b4ced8ebb8 --- /dev/null +++ b/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h @@ -0,0 +1,79 @@ +#ifndef PALLAS_PALLASFUNCTIONCONTRACTDECLARERPASS_H +#define PALLAS_PALLASFUNCTIONCONTRACTDECLARERPASS_H + +#include "vct/col/ast/col.pb.h" + +#include + +#include +#include +#include + +/** + * Pass that transforms Pallas function contracts that are defined as + * metadata that is attached to an LLVM-function into + * LlvmfunctionContract objects. + * + * It assumes that the FunctionContractDeclarer-pass has already been run to + * create the contract-objects in the buffer. + * + * The results can be accessed through FDCResult-objects using a + * FunctionAnalysisManager. + * + */ +namespace pallas { +using namespace llvm; +namespace col = vct::col::ast; + +class PallasFunctionContractDeclarerPass + : public AnalysisInfoMixin { + public: + /** + * Retrieves the LlvmfunctionDefinition object in the buffer from the + * FDCResult object and sets the origin and data-fields of the contract. + * The value-filed of the contract is left empty, because the + * ApplicableContract is constructed directly. + */ + PreservedAnalyses run(Function &f, FunctionAnalysisManager &fam); + + private: + /** + * Initialized the given ApplicableContract so that it represents a + * trivial contract (i.e. it only contains a requires-true-clause). + */ + void initializeTrivialContract(col::ApplicableContract &contract); + + /** + * Tries to add a clause, that is represented by the given metadata-node, to + * the given COL-contract. + * Returns false if an error occurred (e.g. ill-formed metadata-node) and + * true otherwise. In case of an error, an error is added to the + * ErrorReporter. ctxFunc is used to build the error messages. + */ + bool addClauseToContract(col::ApplicableContract &contract, MDNode &clause, + FunctionAnalysisManager &fam, Function &ctxFunc); + + /** + * Sets the pure-flag of the given function based on the given metadata-node + * that encodes a palas contract. + * This expects that the second operand of the metadata-node is a boolean + * constant. + * Returns false if an error occurred (e.g. ill-formed metadata-node) and + * true otherwise. + * The ctxFunc is used to build error messages. + */ + bool setPurity(col::LlvmFunctionDefinition &colFunc, MDNode &contract, + Function &ctxFunc); + + /** + * Tries to extract the wrapper-function from the given metadata-node that + * represents a clause of a Pallas contract (i.e. the operand at index 2 + * is expected to point to a function). + * Also checks, if the function is marked as a wrapper-function. + * Returns a nullptr id the function could not be extracted. + * ctxFunc is used to build error messages. + */ + Function *getWrapperFuncFromClause(MDNode &clause, Function &ctxFunc); +}; +} // namespace pallas +#endif // PALLAS_PALLASFUNCTIONCONTRACTDECLARERPASS_H diff --git a/src/llvm/include/Util/Constants.h b/src/llvm/include/Util/Constants.h index 2556aa5b53..ca73c807b3 100644 --- a/src/llvm/include/Util/Constants.h +++ b/src/llvm/include/Util/Constants.h @@ -5,6 +5,14 @@ * Useful string constants to use for searching out metadata nodes */ namespace pallas::constants { + +// Pallas constants +const std::string PALLAS_FUNC_CONTRACT = "pallas.fcontract"; +const std::string PALLAS_REQUIRES = "pallas.requires"; +const std::string PALLAS_ENSURES = "pallas.ensures"; +const std::string PALLAS_WRAPPER_FUNC = "pallas.exprWrapper"; + +// Legacy VCLLVM constants const std::string VC_PREFIX = "VC."; const std::string METADATA_PURE_KEYWORD = VC_PREFIX + "pure"; diff --git a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp index 5905d6ac08..60b3694c28 100644 --- a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp @@ -24,12 +24,18 @@ void FunctionCursor::addVariableMapEntry(Value &llvmValue, col::Variable &colVar) { variableMap.insert({&llvmValue, &colVar}); // add reference to reference lut of function contract - col::Tuple2_String_Ref_VctColAstVariable *ref = + // (only if the contract is a vcllvm contract) + col::LlvmFunctionContract &contract = FAM.getResult(llvmFunction) - .getAssociatedColFuncContract() - .add_variable_refs(); - ref->set_v1(llvm2col::getValueName(llvmValue)); - ref->mutable_v2()->set_id(colVar.id()); + .getAssociatedColFuncContract(); + if (contract.has_vcllvm_function_contract()) { + col::VcllvmFunctionContract *vcllvmContract = + contract.mutable_vcllvm_function_contract(); + col::Tuple2_String_Ref_VctColAstVariable *ref = + vcllvmContract->add_variable_refs(); + ref->set_v1(llvm2col::getValueName(llvmValue)); + ref->mutable_v2()->set_id(colVar.id()); + } } col::Variable &FunctionCursor::getVariableMapEntry(Value &llvmValue, diff --git a/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp b/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp index ea6e103214..977feffa2a 100644 --- a/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionContractDeclarer.cpp @@ -44,15 +44,15 @@ PreservedAnalyses FunctionContractDeclarerPass::run(Function &F, FunctionAnalysisManager &FAM) { // get col contract FDCResult result = FAM.getResult(F); - col::LlvmFunctionContract &colContract = - result.getAssociatedColFuncContract(); - colContract.set_allocated_blame(new col::Blame()); - colContract.set_name(F.getName()); + col::VcllvmFunctionContract *colContract = + result.getAssociatedColFuncContract().mutable_vcllvm_function_contract(); + colContract->set_allocated_blame(new col::Blame()); + colContract->set_name(F.getName()); // check if contract keyword is present if (!F.hasMetadata(pallas::constants::METADATA_CONTRACT_KEYWORD)) { // set contract to a tautology - colContract.set_value("requires true;"); - colContract.set_allocated_origin( + colContract->set_value("requires true;"); + colContract->set_allocated_origin( llvm2col::generateFunctionContractOrigin(F, "requires true;")); return PreservedAnalyses::all(); } @@ -71,15 +71,15 @@ FunctionContractDeclarerPass::run(Function &F, FunctionAnalysisManager &FAM) { } contractStream << contractLine->getString().str() << '\n'; } - colContract.set_value(contractStream.str()); - colContract.set_allocated_origin( + colContract->set_value(contractStream.str()); + colContract->set_allocated_origin( llvm2col::generateFunctionContractOrigin(F, contractStream.str())); // add all callable functions to the contracts invokables for (auto &moduleF : F.getParent()->functions()) { std::string fName = '@' + moduleF.getName().str(); int64_t fId = FAM.getResult(moduleF).getFunctionId(); col::Tuple2_String_Ref_VctColAstLlvmCallable *invokeRef = - colContract.add_invokable_refs(); + colContract->add_invokable_refs(); invokeRef->set_v1(fName); invokeRef->mutable_v2()->set_id(fId); } diff --git a/src/llvm/lib/Passes/Function/FunctionDeclarer.cpp b/src/llvm/lib/Passes/Function/FunctionDeclarer.cpp index ce692455a2..b288834db7 100644 --- a/src/llvm/lib/Passes/Function/FunctionDeclarer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionDeclarer.cpp @@ -113,8 +113,8 @@ FDResult FunctionDeclarer::run(Function &F, FunctionAnalysisManager &FAM) { if (F.isDeclaration()) { // Defined outside of this module so we don't know if it's pure or what // its contract is - col::LlvmFunctionContract *colContract = - llvmFuncDef->mutable_contract(); + col::VcllvmFunctionContract *colContract = + llvmFuncDef->mutable_contract()->mutable_vcllvm_function_contract(); colContract->set_allocated_blame(new col::Blame()); colContract->set_value("requires true;"); colContract->set_name(F.getName()); diff --git a/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp b/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp new file mode 100644 index 0000000000..41e053ccfc --- /dev/null +++ b/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp @@ -0,0 +1,228 @@ +#include "Passes/Function/PallasFunctionContractDeclarerPass.h" + +#include "Origin/OriginProvider.h" +#include "Passes/Function/FunctionContractDeclarer.h" +#include "Passes/Function/FunctionDeclarer.h" +#include "Util/Constants.h" +#include "Util/Exceptions.h" + +#include +#include +#include +#include + +namespace pallas { +const std::string SOURCE_LOC = + "Passes::Function::PallasFunctionContractDeclarerPass"; + +using namespace llvm; + +/* + * Pallas Function Contract Declarer Pass + */ +PreservedAnalyses +PallasFunctionContractDeclarerPass::run(Function &f, + FunctionAnalysisManager &fam) { + // Get empty COL LLVM-contract + FDCResult cResult = fam.getResult(f); + auto colLLVMContract = + cResult.getAssociatedColFuncContract().mutable_pallas_function_contract(); + + // Get COL function + FDResult fResult = fam.getResult(f); + col::LlvmFunctionDefinition &colFunction = + fResult.getAssociatedColFuncDef(); + // Initialize COL LLVM-contract + colLLVMContract->set_allocated_blame(new col::Blame()); + // TODO: Set origin + + col::ApplicableContract *colContract = + colLLVMContract->mutable_content(); + colContract->set_allocated_blame(new col::Blame()); + // TODO: Set origin + + // Check if a Pallas-contract is attached to the function: + if (!f.hasMetadata(pallas::constants::PALLAS_FUNC_CONTRACT)) { + // No contract is present --> add trivial contract + initializeTrivialContract(*colContract); + return PreservedAnalyses::all(); + } + + // TODO: Remove once the rest is implemented + initializeTrivialContract(*colContract); + return PreservedAnalyses::all(); + + /* + // Check wellformedness of the contract-metadata + auto *contractNode = f.getMetadata(pallas::constants::PALLAS_FUNC_CONTRACT); + if (contractNode->getNumOperands() < 3) { + pallas::ErrorReporter::addError( + SOURCE_LOC, "Ill-formed contract. Expected at least 3 operands", f); + return PreservedAnalyses::all(); + } + + // Get src location: + // TODO: Add to origin + + // Check pure + auto pureSuccess = setPurity(colFunction, *contractNode, f); + if (!pureSuccess) + return PreservedAnalyses::all(); + + // Handle contract clauses + unsigned int clauseIdx = 2; + while (clauseIdx < contractNode->getNumOperands()) { + // Check that the metadata-node is wellformed + auto *clause = contractNode->getOperand(clauseIdx).get(); + if (clause == nullptr || !isa(clause)) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "Ill-formed contract clause. Expected MDNode as operand.", f); + return PreservedAnalyses::all(); + } + + auto addClauseSuccess = + addClauseToContract(*colContract, *cast(clause), fam, f); + if (!addClauseSuccess) + return PreservedAnalyses::all(); + + ++clauseIdx; + } + + return PreservedAnalyses::all(); + */ +} + +bool PallasFunctionContractDeclarerPass::setPurity( + col::LlvmFunctionDefinition &colFunc, MDNode &contract, Function &ctxFunc) { + auto *pureMD = dyn_cast(contract.getOperand(1).get()); + auto *pureVal = dyn_cast_if_present(pureMD->getValue()); + if (pureVal == nullptr || (!pureVal->getBitWidth() == 1)) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "Ill-formed function contract. Second operand should be boolean.", + ctxFunc); + return false; + } + bool isPure = pureVal->isOne(); + colFunc.set_pure(isPure); + return true; +} + +bool PallasFunctionContractDeclarerPass::addClauseToContract( + col::ApplicableContract &contract, MDNode &clause, + FunctionAnalysisManager &fam, Function &ctxFunc) { + if (clause.getNumOperands() < 3) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "Ill-formed contract clause. Expected at least 3 operands.", + ctxFunc); + return false; + } + + // Check clause type (i.e. requires or ensures) + auto *clauseTypeMD = dyn_cast(clause.getOperand(0).get()); + if (clauseTypeMD == nullptr) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "Ill-formed contract clause. First operand should be a string.", + ctxFunc); + return false; + } + auto clauseTypeStr = clauseTypeMD->getString().str(); + + // Check source location + // TODO: Add source location to the origin + + // Get pointer to the LLVM wrapper-function + auto *wrapperF = getWrapperFuncFromClause(clause, ctxFunc); + if (wrapperF == nullptr) + return false; + + // Get COL representation of wrapper function + auto wrapperFResult = fam.getResult(*wrapperF); + col::LlvmFunctionDefinition &colWrapperF = + wrapperFResult.getAssociatedColFuncDef(); + + // Check wellformed of the variables + /* + SmallVector diVars; + unsigned int vIdx = 3; + while (cIdx < clause->getNumOperands()) { + // Check that operand is a DIVariable + auto *diVar = dyn_cast(clause->getOperand(vIdx).get()); + if (diVar == nullptr) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "Ill-formed contract clause. Expected DIVariable as " + "operand.", + f); + return PreservedAnalyses::all(); + } + diVars.push_back(diVar); + cIdx++; + } + */ + + // Resolve the DIVariables to llvm-variables + // TODO: implement + + // Resolve the llvm-variables to COL variables + // TODO: implement + + // Construct an AccountedPredicate from the contract clause + // TODO: implement + + if (clauseTypeStr == pallas::constants::PALLAS_REQUIRES) { + // TODO: Add to requires clauses + } else if (clauseTypeStr == pallas::constants::PALLAS_ENSURES) { + // TODO: Add to ensures clauses + } else { + // Raise error + } + + // TODO: Change to true + return false; +} + +Function *PallasFunctionContractDeclarerPass::getWrapperFuncFromClause( + MDNode &clause, Function &ctxFunc) { + auto *wrapperFuncMD = dyn_cast(clause.getOperand(2).get()); + if (wrapperFuncMD == nullptr || !wrapperFuncMD->getType()->isFunctionTy() || + wrapperFuncMD->getValue() == nullptr || + !isa(wrapperFuncMD->getValue())) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "Ill-formed contract clause. Second operand should be a " + "pointer to a function.", + ctxFunc); + return nullptr; + } + + // Check that the function is marked as a pallas wrapper function. + auto *wrapperF = cast(wrapperFuncMD->getValue()); + if (!wrapperF->hasMetadata(pallas::constants::PALLAS_WRAPPER_FUNC)) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "Ill-formed contract clause. Second operand does not point to " + "wrapper-function.", + ctxFunc); + return nullptr; + } + + return wrapperF; +} + +void PallasFunctionContractDeclarerPass::initializeTrivialContract( + col::ApplicableContract &contract) { + + // Build predicate for the requires-clause + auto requiresExpr = new col::Expr(); + requiresExpr->mutable_boolean_value()->set_value(true); + + auto *requiresPred = + contract.mutable_requires_()->mutable_unit_accounted_predicate(); + requiresPred->set_allocated_pred(requiresExpr); +} + +} // namespace pallas diff --git a/src/llvm/lib/Plugin.cpp b/src/llvm/lib/Plugin.cpp index 2495dd6b54..6a8d572ec7 100644 --- a/src/llvm/lib/Plugin.cpp +++ b/src/llvm/lib/Plugin.cpp @@ -5,6 +5,7 @@ #include "Passes/Function/FunctionContractDeclarer.h" #include "Passes/Function/FunctionDeclarer.h" #include "Passes/Function/PureAssigner.h" +#include "Passes/Function/PallasFunctionContractDeclarerPass.h" #include "Passes/Module/GlobalVariableDeclarer.h" #include "Passes/Module/ModuleSpecCollector.h" #include "Passes/Module/ProtobufPrinter.h" @@ -51,13 +52,16 @@ llvm::PassPluginLibraryInfo getPallasPluginInfo() { } else if (Name == "pallas-assign-pure") { FPM.addPass(pallas::PureAssignerPass()); return true; - } else if (Name == "pallas-declare-function-contract") { + } else if (Name == "llvm-declare-function-contract") { FPM.addPass(pallas::FunctionContractDeclarerPass()); return true; + } else if (Name == "pallas-declare-function-contract") { + FPM.addPass(pallas::PallasFunctionContractDeclarerPass()); + return true; } else if (Name == "pallas-transform-function-body") { FPM.addPass(pallas::FunctionBodyTransformerPass()); return true; - } + } return false; }); }}; diff --git a/src/main/vct/main/stages/Resolution.scala b/src/main/vct/main/stages/Resolution.scala index 3c209a014a..0e31b9996c 100644 --- a/src/main/vct/main/stages/Resolution.scala +++ b/src/main/vct/main/stages/Resolution.scala @@ -9,7 +9,7 @@ import vct.col.ast.{ CGlobalDeclaration, Expr, GlobalDeclaration, - LLVMFunctionContract, + VCLLVMFunctionContract, LLVMGlobalSpecification, Program, Refute, @@ -103,7 +103,7 @@ case class MyLocalLLVMSpecParser( debugOptions: DebugOptions, ) extends Resolve.SpecContractParser { override def parse[G]( - input: LLVMFunctionContract[G], + input: VCLLVMFunctionContract[G], o: Origin, ): ApplicableContract[G] = ColLLVMContractParser(debugOptions, blameProvider) diff --git a/src/parsers/vct/parsers/parser/ColLLVMParser.scala b/src/parsers/vct/parsers/parser/ColLLVMParser.scala index 7cbc8fe295..1d2bec948d 100644 --- a/src/parsers/vct/parsers/parser/ColLLVMParser.scala +++ b/src/parsers/vct/parsers/parser/ColLLVMParser.scala @@ -50,7 +50,7 @@ case class ColLLVMParser( val command = Seq( "opt-17", s"--load-pass-plugin=$pallas", - "--passes=module(pallas-declare-variables,pallas-collect-module-spec),function(pallas-declare-function,pallas-assign-pure,pallas-declare-function-contract,pallas-transform-function-body),module(pallas-print-protobuf)", + "--passes=module(pallas-declare-variables,pallas-collect-module-spec),function(pallas-declare-function,pallas-assign-pure,llvm-declare-function-contract,pallas-transform-function-body),module(pallas-print-protobuf)", readable.fileName, "--disable-output", ) diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala index 728125b10e..7b443fa113 100644 --- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala +++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala @@ -299,7 +299,13 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre]) else Some(rw.dispatch(functionBody)) }, - contract = rw.dispatch(func.contract.data.get), + contract = + func.contract match { + case contract: VCLLVMFunctionContract[Pre] => + rw.dispatch(contract.data.get) + case contract: PallasFunctionContract[Pre] => + rw.dispatch(contract.content) + }, pure = func.pure, )(func.blame) ) From 967043eee46b938409a827e45b684faa5a0f890a Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Wed, 20 Nov 2024 13:29:13 +0100 Subject: [PATCH 02/13] First draft of integrating Pallas function contracts --- src/col/vct/col/resolve/Resolve.scala | 1 + .../PallasFunctionContractDeclarerPass.h | 57 ++-- .../include/Passes/Function/PureAssigner.h | 27 ++ .../PallasFunctionContractDeclarerPass.cpp | 276 +++++++++++++----- src/llvm/lib/Passes/Function/PureAssigner.cpp | 102 +++++-- 5 files changed, 348 insertions(+), 115 deletions(-) diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala index 9965b26ca8..d6f7734357 100644 --- a/src/col/vct/col/resolve/Resolve.scala +++ b/src/col/vct/col/resolve/Resolve.scala @@ -1142,6 +1142,7 @@ case object ResolveReferences extends LazyLogging { func.importedArguments = Some(importedProcedure.args) func.importedReturnType = Some(importedProcedure.returnType) } + case _ => } case loop: LLVMLoop[G] => loop.blocks = Some(loop.blockLabels.map { label => diff --git a/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h b/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h index b4ced8ebb8..91137f0a46 100644 --- a/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h +++ b/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h @@ -38,32 +38,43 @@ class PallasFunctionContractDeclarerPass private: /** - * Initialized the given ApplicableContract so that it represents a + * Initializes the given ApplicableContract so that it represents a * trivial contract (i.e. it only contains a requires-true-clause). */ - void initializeTrivialContract(col::ApplicableContract &contract); + void initializeTrivialContract(col::ApplicableContract &contract, + Function &f); /** - * Tries to add a clause, that is represented by the given metadata-node, to - * the given COL-contract. - * Returns false if an error occurred (e.g. ill-formed metadata-node) and - * true otherwise. In case of an error, an error is added to the - * ErrorReporter. ctxFunc is used to build the error messages. + * Adds an empty requires-clause (i.e. requires true;) to the given contract + * if it does not already have a requires-clause. + */ + void addEmptyRequires(col::ApplicableContract &contract, Function &f); + + /** + * Adds an empty ensures-clause (i.e. ensures true;) to the given contract + * if it does not already have a requires-clause. + */ + void addEmptyEnsures(col::ApplicableContract &contract, Function &f); + + /** + * Adds an empty context_everywhere (i.e. context_everywhere true;) to the + * given contract if it does not already have a context_everywhere-clause. */ - bool addClauseToContract(col::ApplicableContract &contract, MDNode &clause, - FunctionAnalysisManager &fam, Function &ctxFunc); + void addEmptyContextEverywhere(col::ApplicableContract &contract, + Function &f); /** - * Sets the pure-flag of the given function based on the given metadata-node - * that encodes a palas contract. - * This expects that the second operand of the metadata-node is a boolean - * constant. + * Tries to add a clause, that is represented by the given metadata-node, to + * the given COL-contract. * Returns false if an error occurred (e.g. ill-formed metadata-node) and - * true otherwise. - * The ctxFunc is used to build error messages. + * true otherwise. In case of an error, an error is added to the + * ErrorReporter. + * parentFunc is the function to which the contract is attached. */ - bool setPurity(col::LlvmFunctionDefinition &colFunc, MDNode &contract, - Function &ctxFunc); + bool addClauseToContract(col::ApplicableContract &contract, + Metadata *clauseOperand, + FunctionAnalysisManager &fam, Function &parentFunc, + col::LlvmFunctionDefinition &colParentFunc); /** * Tries to extract the wrapper-function from the given metadata-node that @@ -74,6 +85,18 @@ class PallasFunctionContractDeclarerPass * ctxFunc is used to build error messages. */ Function *getWrapperFuncFromClause(MDNode &clause, Function &ctxFunc); + + /** + * Initializes the given predicate 'newPred' such that it represents a split + * predicate that contains left and right. + * Assumes that 'newPred' is already allocated, but uninitialized. + * Assumes that 'left', 'right' and 'newPredOrigin' are owned by the caller. + * After the function terminates, the ownership is transferred to 'newPred'. + */ + void extendPredicate(col::AccountedPredicate *newPred, + col::Origin *newPredOrigin, + col::AccountedPredicate *left, + col::UnitAccountedPredicate *right); }; } // namespace pallas #endif // PALLAS_PALLASFUNCTIONCONTRACTDECLARERPASS_H diff --git a/src/llvm/include/Passes/Function/PureAssigner.h b/src/llvm/include/Passes/Function/PureAssigner.h index a41e01bbe1..4bd16dd3f5 100644 --- a/src/llvm/include/Passes/Function/PureAssigner.h +++ b/src/llvm/include/Passes/Function/PureAssigner.h @@ -14,6 +14,33 @@ namespace col = vct::col::ast; class PureAssignerPass : public PassInfoMixin { public: PreservedAnalyses run(Function &F, FunctionAnalysisManager &FAM); + + private: + /** + * Checks if the given metadata-node represents a valid pure-annotation in + * the format that is used by VCLLVM. + * If the metadata is not wellformed, an error is added to the ErrorReporter + * and false is returned. + * The given function is used to build error-messages. + */ + bool isVcllvmPureWellformed(MDNode &pureMD, Function &f); + + /** + * Checks if the given metadata-node represents a valid pure-annotation + * inside of a function-contract in the format that is used by Pallas. If + * the metadata is not wellformed, an error is added to the ErrorReporter + * and false is returned. + * The given function is used to build error-messages. + */ + bool isPallasPureWellformed(MDNode &contractMD, Function &f); + + /** + * Extracts the pure-value from a metadata-node that represents a pallas + * function contract. + * Assumes, that the metadata-node is wellformed. (I.e. it has at least two + * operands, and the second operand is a boolean constant) + */ + bool getPureValueFromPallasContract(MDNode &contractMD); }; } // namespace pallas #endif // PALLAS_PUREASSIGNER_H diff --git a/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp b/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp index 41e053ccfc..94517566de 100644 --- a/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp +++ b/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp @@ -7,9 +7,11 @@ #include "Util/Exceptions.h" #include +#include #include #include #include +#include namespace pallas { const std::string SOURCE_LOC = @@ -25,8 +27,8 @@ PallasFunctionContractDeclarerPass::run(Function &f, FunctionAnalysisManager &fam) { // Get empty COL LLVM-contract FDCResult cResult = fam.getResult(f); - auto colLLVMContract = - cResult.getAssociatedColFuncContract().mutable_pallas_function_contract(); + auto colLLVMContract = cResult.getAssociatedColFuncContract() + .mutable_pallas_function_contract(); // Get COL function FDResult fResult = fam.getResult(f); @@ -34,99 +36,85 @@ PallasFunctionContractDeclarerPass::run(Function &f, fResult.getAssociatedColFuncDef(); // Initialize COL LLVM-contract colLLVMContract->set_allocated_blame(new col::Blame()); - // TODO: Set origin - col::ApplicableContract *colContract = - colLLVMContract->mutable_content(); + col::ApplicableContract *colContract = colLLVMContract->mutable_content(); colContract->set_allocated_blame(new col::Blame()); - // TODO: Set origin // Check if a Pallas-contract is attached to the function: if (!f.hasMetadata(pallas::constants::PALLAS_FUNC_CONTRACT)) { // No contract is present --> add trivial contract - initializeTrivialContract(*colContract); + colLLVMContract->set_allocated_origin( + llvm2col::generateFunctionContractOrigin(f, "Empty contract")); + initializeTrivialContract(*colContract, f); return PreservedAnalyses::all(); } - // TODO: Remove once the rest is implemented - initializeTrivialContract(*colContract); - return PreservedAnalyses::all(); - - /* // Check wellformedness of the contract-metadata auto *contractNode = f.getMetadata(pallas::constants::PALLAS_FUNC_CONTRACT); - if (contractNode->getNumOperands() < 3) { + if (contractNode->getNumOperands() < 2) { pallas::ErrorReporter::addError( - SOURCE_LOC, "Ill-formed contract. Expected at least 3 operands", f); + SOURCE_LOC, "Ill-formed contract. Expected at least 2 operands", f); return PreservedAnalyses::all(); } // Get src location: - // TODO: Add to origin - - // Check pure - auto pureSuccess = setPurity(colFunction, *contractNode, f); - if (!pureSuccess) - return PreservedAnalyses::all(); + // TODO: Implement properly and add location to origin of + // colLLVMContract and colContract + colLLVMContract->set_allocated_origin( + llvm2col::generateFunctionContractOrigin(f, "TODO: Add location-info (1)")); + colContract->set_allocated_origin( + llvm2col::generateFunctionContractOrigin(f, "TODO: Add location-info (2)")); // Handle contract clauses unsigned int clauseIdx = 2; while (clauseIdx < contractNode->getNumOperands()) { - // Check that the metadata-node is wellformed - auto *clause = contractNode->getOperand(clauseIdx).get(); - if (clause == nullptr || !isa(clause)) { - pallas::ErrorReporter::addError( - SOURCE_LOC, - "Ill-formed contract clause. Expected MDNode as operand.", f); - return PreservedAnalyses::all(); - } - - auto addClauseSuccess = - addClauseToContract(*colContract, *cast(clause), fam, f); + auto addClauseSuccess = addClauseToContract( + *colContract, contractNode->getOperand(clauseIdx).get(), fam, f, + colFunction); if (!addClauseSuccess) return PreservedAnalyses::all(); - ++clauseIdx; } + // Ensure, that the required fields of the contract are set. + // I.e. add trivial clauses if they are currently empty. + addEmptyRequires(*colContract, f); + addEmptyEnsures(*colContract, f); + addEmptyContextEverywhere(*colContract, f); return PreservedAnalyses::all(); - */ } -bool PallasFunctionContractDeclarerPass::setPurity( - col::LlvmFunctionDefinition &colFunc, MDNode &contract, Function &ctxFunc) { - auto *pureMD = dyn_cast(contract.getOperand(1).get()); - auto *pureVal = dyn_cast_if_present(pureMD->getValue()); - if (pureVal == nullptr || (!pureVal->getBitWidth() == 1)) { +bool PallasFunctionContractDeclarerPass::addClauseToContract( + col::ApplicableContract &contract, Metadata *clauseOperand, + FunctionAnalysisManager &fam, Function &parentFunc, + col::LlvmFunctionDefinition &colParentFunc) { + + // Try to extract MDNode + auto *clause = dyn_cast_if_present(clauseOperand); + if (clause == nullptr) { pallas::ErrorReporter::addError( SOURCE_LOC, - "Ill-formed function contract. Second operand should be boolean.", - ctxFunc); + "Ill-formed contract clause. Expected MDNode as operand.", + parentFunc); return false; } - bool isPure = pureVal->isOne(); - colFunc.set_pure(isPure); - return true; -} -bool PallasFunctionContractDeclarerPass::addClauseToContract( - col::ApplicableContract &contract, MDNode &clause, - FunctionAnalysisManager &fam, Function &ctxFunc) { - if (clause.getNumOperands() < 3) { + // Check number of operands + if (clause->getNumOperands() < 3) { pallas::ErrorReporter::addError( SOURCE_LOC, "Ill-formed contract clause. Expected at least 3 operands.", - ctxFunc); + parentFunc); return false; } // Check clause type (i.e. requires or ensures) - auto *clauseTypeMD = dyn_cast(clause.getOperand(0).get()); + auto *clauseTypeMD = dyn_cast(clause->getOperand(0).get()); if (clauseTypeMD == nullptr) { pallas::ErrorReporter::addError( SOURCE_LOC, "Ill-formed contract clause. First operand should be a string.", - ctxFunc); + parentFunc); return false; } auto clauseTypeStr = clauseTypeMD->getString().str(); @@ -135,7 +123,7 @@ bool PallasFunctionContractDeclarerPass::addClauseToContract( // TODO: Add source location to the origin // Get pointer to the LLVM wrapper-function - auto *wrapperF = getWrapperFuncFromClause(clause, ctxFunc); + auto *wrapperF = getWrapperFuncFromClause(*clause, parentFunc); if (wrapperF == nullptr) return false; @@ -144,11 +132,10 @@ bool PallasFunctionContractDeclarerPass::addClauseToContract( col::LlvmFunctionDefinition &colWrapperF = wrapperFResult.getAssociatedColFuncDef(); - // Check wellformed of the variables - /* - SmallVector diVars; + // Check wellformedness of the variables + SmallVector diVars; unsigned int vIdx = 3; - while (cIdx < clause->getNumOperands()) { + while (vIdx < clause->getNumOperands()) { // Check that operand is a DIVariable auto *diVar = dyn_cast(clause->getOperand(vIdx).get()); if (diVar == nullptr) { @@ -156,40 +143,117 @@ bool PallasFunctionContractDeclarerPass::addClauseToContract( SOURCE_LOC, "Ill-formed contract clause. Expected DIVariable as " "operand.", - f); - return PreservedAnalyses::all(); + parentFunc); + return false; } diVars.push_back(diVar); - cIdx++; + vIdx++; } - */ - // Resolve the DIVariables to llvm-variables - // TODO: implement + // Resolve the DIVariables to col-variables + SmallVector colArgs; + for (auto *diVar : diVars) { - // Resolve the llvm-variables to COL variables - // TODO: implement + // Global values are not yet supported + auto *localVar = dyn_cast(diVar); + if (localVar == nullptr || !localVar->isParameter()) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "Ill-formed contract clause. Only arguments are currently " + "supported ", + parentFunc); + return false; + } - // Construct an AccountedPredicate from the contract clause - // TODO: implement + // TODO: Do we want to convert to llvm::Argument first? + + // Check that the DIVariable belongs to the function to which the + // contract is attached + if (localVar->getScope() != parentFunc.getSubprogram()) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "Ill-formed contract clause. DIVariable does not belong to " + "the function to which the contract is attached.", + parentFunc); + return false; + } + // Indexing of getArg starts at 1 + auto llvmArgIdx = localVar->getArg() -1; + auto colArgVar = colParentFunc.args(llvmArgIdx); + colArgs.push_back(&colArgVar); + } + + // Build a call to the wrapper-function with the gathered arguments + col::LlvmFunctionInvocation *wrapperCall = + new col::LlvmFunctionInvocation(); + wrapperCall->set_allocated_origin(llvm2col::generateFunctionContractOrigin( + parentFunc, "TODO: Add location-info (3)")); + wrapperCall->set_allocated_blame(new col::Blame()); + + // Build ref to parent function + auto *fRef = wrapperCall->mutable_ref(); + fRef->set_id(colWrapperF.id()); + + // Add argument-expression to invocation + for (auto *v : colArgs) { + // Construct Local-node that references the variable and add it to the + // list of arguments + auto *argExpr = wrapperCall->add_args()->mutable_local(); + argExpr->set_allocated_origin(llvm2col::generateFunctionContractOrigin( + parentFunc, "TODO: Add location-info (4)")); + auto *varRef = argExpr->mutable_ref(); + varRef->set_id(v->id()); + } + + // Construct an AccountedPredicate the wraps the call to the + // wrapper-function + col::UnitAccountedPredicate *newPred = new col::UnitAccountedPredicate(); + newPred->set_allocated_origin(llvm2col::generateFunctionContractOrigin( + parentFunc, "TODO: Add location-info (5)")); + newPred->mutable_pred()->set_allocated_llvm_function_invocation( + wrapperCall); if (clauseTypeStr == pallas::constants::PALLAS_REQUIRES) { - // TODO: Add to requires clauses + // Add to requires clauses + if (!contract.has_requires_()) { + contract.mutable_requires_() + ->set_allocated_unit_accounted_predicate(newPred); + } else { + col::AccountedPredicate *oldPred = contract.release_requires_(); + auto *reqPred = contract.mutable_requires_(); + extendPredicate(reqPred, + llvm2col::generateFunctionContractOrigin( + parentFunc, "TODO: Add location-info (6)"), + oldPred, newPred); + } } else if (clauseTypeStr == pallas::constants::PALLAS_ENSURES) { - // TODO: Add to ensures clauses + // Add to ensures clauses + if (!contract.has_ensures()) { + contract.mutable_ensures()->set_allocated_unit_accounted_predicate( + newPred); + } else { + col::AccountedPredicate *oldPred = contract.release_ensures(); + auto *ensPred = contract.mutable_ensures(); + extendPredicate(ensPred, + llvm2col::generateFunctionContractOrigin( + parentFunc, "TODO: Add location-info (7)"), + oldPred, newPred); + } } else { // Raise error + pallas::ErrorReporter::addError( + SOURCE_LOC, "Ill-formed contract clause. Unknown clause type.", + parentFunc); + return false; } - // TODO: Change to true - return false; + return true; } Function *PallasFunctionContractDeclarerPass::getWrapperFuncFromClause( MDNode &clause, Function &ctxFunc) { auto *wrapperFuncMD = dyn_cast(clause.getOperand(2).get()); - if (wrapperFuncMD == nullptr || !wrapperFuncMD->getType()->isFunctionTy() || - wrapperFuncMD->getValue() == nullptr || + if (wrapperFuncMD == nullptr || wrapperFuncMD->getValue() == nullptr || !isa(wrapperFuncMD->getValue())) { pallas::ErrorReporter::addError( SOURCE_LOC, @@ -214,15 +278,73 @@ Function *PallasFunctionContractDeclarerPass::getWrapperFuncFromClause( } void PallasFunctionContractDeclarerPass::initializeTrivialContract( - col::ApplicableContract &contract) { + col::ApplicableContract &contract, Function &f) { + contract.set_allocated_origin( + llvm2col::generateFunctionContractOrigin(f, "Empty contract")); + addEmptyRequires(contract, f); + addEmptyEnsures(contract, f); + addEmptyContextEverywhere(contract, f); +} - // Build predicate for the requires-clause - auto requiresExpr = new col::Expr(); - requiresExpr->mutable_boolean_value()->set_value(true); +void PallasFunctionContractDeclarerPass::addEmptyRequires( + col::ApplicableContract &contract, Function &f) { + + // If the contract already has a requires-clause, do nothing + if (contract.has_requires_()) + return; + // Build predicate for the requires-clause auto *requiresPred = contract.mutable_requires_()->mutable_unit_accounted_predicate(); - requiresPred->set_allocated_pred(requiresExpr); + requiresPred->set_allocated_origin( + llvm2col::generateFunctionContractOrigin(f, "requires true;")); + auto *requiresExpr = requiresPred->mutable_pred()->mutable_boolean_value(); + requiresExpr->set_allocated_origin( + llvm2col::generateFunctionContractOrigin(f, "true")); + requiresExpr->set_value(true); +} + +void PallasFunctionContractDeclarerPass::addEmptyEnsures( + col::ApplicableContract &contract, Function &f) { + + // If the contract already has a requires-clause, do nothing + if (contract.has_ensures()) + return; + + // Build predicate for the ensures-clause + auto *ensuresPred = + contract.mutable_ensures()->mutable_unit_accounted_predicate(); + ensuresPred->set_allocated_origin( + llvm2col::generateFunctionContractOrigin(f, "ensures true;")); + auto *ensuresExpr = ensuresPred->mutable_pred()->mutable_boolean_value(); + ensuresExpr->set_allocated_origin( + llvm2col::generateFunctionContractOrigin(f, "true")); + ensuresExpr->set_value(true); +} + +void PallasFunctionContractDeclarerPass::addEmptyContextEverywhere( + col::ApplicableContract &contract, Function &f) { + + // If the contract already has a contextEverywhere-clause, do nothing + if (contract.has_context_everywhere()) + return; + + // Build expression for contextEverywhere + auto *contextExpr = + contract.mutable_context_everywhere()->mutable_boolean_value(); + contextExpr->set_allocated_origin( + llvm2col::generateFunctionContractOrigin(f, "true")); + contextExpr->set_value(true); +} + +void PallasFunctionContractDeclarerPass::extendPredicate( + col::AccountedPredicate *newPred, col::Origin *newPredOrigin, + col::AccountedPredicate *left, col::UnitAccountedPredicate *right) { + auto *newSplitPred = newPred->mutable_split_accounted_predicate(); + newSplitPred->set_allocated_origin(newPredOrigin); + newSplitPred->set_allocated_left(left); + newSplitPred->mutable_right()->set_allocated_unit_accounted_predicate( + right); } } // namespace pallas diff --git a/src/llvm/lib/Passes/Function/PureAssigner.cpp b/src/llvm/lib/Passes/Function/PureAssigner.cpp index 46b0415de7..d80a534757 100644 --- a/src/llvm/lib/Passes/Function/PureAssigner.cpp +++ b/src/llvm/lib/Passes/Function/PureAssigner.cpp @@ -4,6 +4,8 @@ #include "Util/Constants.h" #include "Util/Exceptions.h" +#include + namespace pallas { const std::string SOURCE_LOC = "Passes::Function::PureAssigner"; @@ -24,36 +26,94 @@ static void reportError(Function &F, const std::string &explanation) { PreservedAnalyses PureAssignerPass::run(Function &F, FunctionAnalysisManager &FAM) { - std::ostringstream errorStream; - FDResult result = FAM.getResult(F); - col::LlvmFunctionDefinition &colFunction = result.getAssociatedColFuncDef(); - // check if pure keyword is present, else assume unpure function - if (!F.hasMetadata(pallas::constants::METADATA_PURE_KEYWORD)) { - colFunction.set_pure(false); + // Count how many annotation specify the purity of the function. + int pureAnnotationCount = 0; + bool isPure = false; + + // Check if the function is annotated with the pure-metadata of VCLLVM + if (F.hasMetadata(pallas::constants::METADATA_PURE_KEYWORD)) { + pureAnnotationCount++; + MDNode *pureMDNode = + F.getMetadata(pallas::constants::METADATA_PURE_KEYWORD); + if (!isVcllvmPureWellformed(*pureMDNode, F)) + return PreservedAnalyses::all(); + // attempt down cast to ConstantInt (should workdue to previous checks) + auto *pureMDVal = cast(pureMDNode->getOperand(0)); + isPure = cast(pureMDVal)->getValue()->isOneValue(); + } + + // Check if the function is annotated with a pallas function contract + if (F.hasMetadata(pallas::constants::PALLAS_FUNC_CONTRACT)) { + pureAnnotationCount++; + MDNode *contractMDNode = + F.getMetadata(pallas::constants::PALLAS_FUNC_CONTRACT); + if (!isPallasPureWellformed(*contractMDNode, F)) + return PreservedAnalyses::all(); + // Extract pure-value (should work due to previous checks) + isPure = getPureValueFromPallasContract(*contractMDNode); + } + + // Check if the function is marked as a pallas wrapper-function + if (F.hasMetadata(pallas::constants::PALLAS_WRAPPER_FUNC)) { + pureAnnotationCount++; + isPure = true; + } + + // Check that no duplicate pure-definition is present + if (pureAnnotationCount > 1) { + reportError(F, + "Function has multiple annotations that speciy its purity"); return PreservedAnalyses::all(); } + + // Set the pure-flag of the function + FDResult result = FAM.getResult(F); + col::LlvmFunctionDefinition &colFunction = result.getAssociatedColFuncDef(); + colFunction.set_pure(isPure); + return PreservedAnalyses::all(); +} + +bool PureAssignerPass::isVcllvmPureWellformed(MDNode &pureMD, Function &f) { + std::ostringstream errorStream; // check if the 'pure' metadata has only 1 operand, else exit with error - MDNode *pureMDNode = - F.getMetadata(pallas::constants::METADATA_PURE_KEYWORD); - if (pureMDNode->getNumOperands() != 1) { + if (pureMD.getNumOperands() != 1) { errorStream << "Expected 1 argument but got " - << pureMDNode->getNumOperands(); - reportError(F, errorStream.str()); - return PreservedAnalyses::all(); + << pureMD.getNumOperands(); + reportError(f, errorStream.str()); + return false; } // check if the only operand is of type 'i1', else exit with error - auto *pureMDValue = cast(pureMDNode->getOperand(0)); + auto *pureMDValue = cast(pureMD.getOperand(0)); if (!pureMDValue->getType()->isIntegerTy(1)) { errorStream << "MD node type must be of type \"i1\""; - reportError(F, errorStream.str()); - return PreservedAnalyses::all(); + reportError(f, errorStream.str()); + return false; } - // attempt down cast to ConstantInt (which shouldn't fail given previous - // checks) - bool purity = - cast(pureMDValue)->getValue()->isOneValue(); - colFunction.set_pure(purity); - return PreservedAnalyses::all(); + return true; +} + +bool PureAssignerPass::isPallasPureWellformed(MDNode &contractMD, Function &f) { + std::ostringstream errorStream; + // Check that the contract has at least 2 operands + if (contractMD.getNumOperands() < 2) { + reportError(f, "Ill-formed contract. Expected at least 2 operands"); + return false; + } + // Check that the second operand is a boolean constant + auto *pureConst = + dyn_cast(contractMD.getOperand(1).get()); + auto *pureVal = dyn_cast_if_present(pureConst->getValue()); + if (pureVal == nullptr || (!pureVal->getBitWidth() == 1)) { + reportError(f, "Ill-formed contract. Second operand should be boolean"); + return false; + } + return true; +} + +bool PureAssignerPass::getPureValueFromPallasContract(MDNode &contractMD) { + auto *pureConst = cast(contractMD.getOperand(1).get()); + auto *pureVal = cast(pureConst->getValue()); + return pureVal->isOne(); } } // namespace pallas From cdf95d993a524ec0859bbc2e82d34fd1ed02cc85 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Wed, 20 Nov 2024 16:22:54 +0100 Subject: [PATCH 03/13] Changes run both, VCLLVM- and Pallas-function contract declarer-passes. --- .../PallasFunctionContractDeclarerPass.h | 24 ++++++++- .../PallasFunctionContractDeclarerPass.cpp | 49 ++++++++++++++----- .../vct/parsers/parser/ColLLVMParser.scala | 2 +- 3 files changed, 60 insertions(+), 15 deletions(-) diff --git a/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h b/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h index 91137f0a46..bee2666f02 100644 --- a/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h +++ b/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h @@ -14,8 +14,9 @@ * metadata that is attached to an LLVM-function into * LlvmfunctionContract objects. * - * It assumes that the FunctionContractDeclarer-pass has already been run to - * create the contract-objects in the buffer. + * This pass expects to be run after the following passes + * - FunctionContractDeclarer + * - FunctionContractDeclarerPass * * The results can be accessed through FDCResult-objects using a * FunctionAnalysisManager. @@ -97,6 +98,25 @@ class PallasFunctionContractDeclarerPass col::Origin *newPredOrigin, col::AccountedPredicate *left, col::UnitAccountedPredicate *right); + + /** + * Checks if the given llvm function is annotated with both, a VCLLVM and a + * Pallas function contract. If so, an error is added to the ErrorReporter + * and true is returned. Otherwise, false is returned. + */ + bool hasConflictingContract(Function &f); + + /** + * Checks if the given function has a metadata-node that is labeled as a + * Pallas function contract. + */ + bool hasPallasContract(const Function &f); + + /** + * Checks if the given function has a metadata-node that is labeled as a + * VCLLVM contract. + */ + bool hasVcllvmContract(const Function &f); }; } // namespace pallas #endif // PALLAS_PALLASFUNCTIONCONTRACTDECLARERPASS_H diff --git a/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp b/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp index 94517566de..00c055300b 100644 --- a/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp +++ b/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp @@ -25,25 +25,31 @@ using namespace llvm; PreservedAnalyses PallasFunctionContractDeclarerPass::run(Function &f, FunctionAnalysisManager &fam) { - // Get empty COL LLVM-contract + // Check that f does not have a VCLLVM AND a Pallas contract + if (hasConflictingContract(f)) + return PreservedAnalyses::all(); + // Skip, if f has a non-empty vcllvm-contract + if (hasVcllvmContract(f)) + return PreservedAnalyses::all(); + + // Setup a fresh Pallas-contract FDCResult cResult = fam.getResult(f); - auto colLLVMContract = cResult.getAssociatedColFuncContract() - .mutable_pallas_function_contract(); + auto colPallasContract = cResult.getAssociatedColFuncContract() + .mutable_pallas_function_contract(); + colPallasContract->set_allocated_blame(new col::Blame()); // Get COL function FDResult fResult = fam.getResult(f); col::LlvmFunctionDefinition &colFunction = fResult.getAssociatedColFuncDef(); - // Initialize COL LLVM-contract - colLLVMContract->set_allocated_blame(new col::Blame()); - col::ApplicableContract *colContract = colLLVMContract->mutable_content(); + col::ApplicableContract *colContract = colPallasContract->mutable_content(); colContract->set_allocated_blame(new col::Blame()); // Check if a Pallas-contract is attached to the function: if (!f.hasMetadata(pallas::constants::PALLAS_FUNC_CONTRACT)) { // No contract is present --> add trivial contract - colLLVMContract->set_allocated_origin( + colPallasContract->set_allocated_origin( llvm2col::generateFunctionContractOrigin(f, "Empty contract")); initializeTrivialContract(*colContract, f); return PreservedAnalyses::all(); @@ -60,10 +66,11 @@ PallasFunctionContractDeclarerPass::run(Function &f, // Get src location: // TODO: Implement properly and add location to origin of // colLLVMContract and colContract - colLLVMContract->set_allocated_origin( - llvm2col::generateFunctionContractOrigin(f, "TODO: Add location-info (1)")); - colContract->set_allocated_origin( - llvm2col::generateFunctionContractOrigin(f, "TODO: Add location-info (2)")); + colPallasContract->set_allocated_origin( + llvm2col::generateFunctionContractOrigin( + f, "TODO: Add location-info (1)")); + colContract->set_allocated_origin(llvm2col::generateFunctionContractOrigin( + f, "TODO: Add location-info (2)")); // Handle contract clauses unsigned int clauseIdx = 2; @@ -178,7 +185,7 @@ bool PallasFunctionContractDeclarerPass::addClauseToContract( return false; } // Indexing of getArg starts at 1 - auto llvmArgIdx = localVar->getArg() -1; + auto llvmArgIdx = localVar->getArg() - 1; auto colArgVar = colParentFunc.args(llvmArgIdx); colArgs.push_back(&colArgVar); } @@ -347,4 +354,22 @@ void PallasFunctionContractDeclarerPass::extendPredicate( right); } +bool PallasFunctionContractDeclarerPass::hasConflictingContract(Function &f) { + bool conflict = hasPallasContract(f) && hasVcllvmContract(f); + if (conflict) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "The function has both, a vcllvm and a pallas contract.", f); + } + return conflict; +} + +bool PallasFunctionContractDeclarerPass::hasPallasContract(const Function &f) { + return f.hasMetadata(pallas::constants::PALLAS_FUNC_CONTRACT); +} + +bool PallasFunctionContractDeclarerPass::hasVcllvmContract(const Function &f) { + return f.hasMetadata(pallas::constants::METADATA_CONTRACT_KEYWORD); +} + } // namespace pallas diff --git a/src/parsers/vct/parsers/parser/ColLLVMParser.scala b/src/parsers/vct/parsers/parser/ColLLVMParser.scala index 1d2bec948d..e81d8c6662 100644 --- a/src/parsers/vct/parsers/parser/ColLLVMParser.scala +++ b/src/parsers/vct/parsers/parser/ColLLVMParser.scala @@ -50,7 +50,7 @@ case class ColLLVMParser( val command = Seq( "opt-17", s"--load-pass-plugin=$pallas", - "--passes=module(pallas-declare-variables,pallas-collect-module-spec),function(pallas-declare-function,pallas-assign-pure,llvm-declare-function-contract,pallas-transform-function-body),module(pallas-print-protobuf)", + "--passes=module(pallas-declare-variables,pallas-collect-module-spec),function(pallas-declare-function,pallas-assign-pure,llvm-declare-function-contract,pallas-declare-function-contract,pallas-transform-function-body),module(pallas-print-protobuf)", readable.fileName, "--disable-output", ) From 8e7705c67ae014fa334766f7f42f8eb8ac69a110 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Thu, 21 Nov 2024 16:19:17 +0100 Subject: [PATCH 04/13] Fixed bug that caused incorrect instruction-order with some branches. --- src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp | 6 +++--- src/llvm/lib/Transform/BlockTransform.cpp | 7 ++++++- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp index 60b3694c28..20ce0108a6 100644 --- a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp @@ -29,9 +29,9 @@ void FunctionCursor::addVariableMapEntry(Value &llvmValue, FAM.getResult(llvmFunction) .getAssociatedColFuncContract(); if (contract.has_vcllvm_function_contract()) { - col::VcllvmFunctionContract *vcllvmContract = + col::VcllvmFunctionContract *vcllvmContract = contract.mutable_vcllvm_function_contract(); - col::Tuple2_String_Ref_VctColAstVariable *ref = + col::Tuple2_String_Ref_VctColAstVariable *ref = vcllvmContract->add_variable_refs(); ref->set_v1(llvm2col::getValueName(llvmValue)); ref->mutable_v2()->set_id(colVar.id()); @@ -216,8 +216,8 @@ col::Assign &FunctionCursor::createPhiAssignment(Instruction &llvmInstruction, // tracking assignments in their origin blocks. therefore we need to // swap the last two elements of the block (i.e. the goto statement and // the newest assignment) - int lastIndex = colBlock.statements_size() - 1; colBlock.add_statements()->set_allocated_assign(assignment); + int lastIndex = colBlock.statements_size() - 1; colBlock.mutable_statements()->SwapElements(lastIndex, lastIndex - 1); } else { // Buffer the phi assignments so they appear at the end diff --git a/src/llvm/lib/Transform/BlockTransform.cpp b/src/llvm/lib/Transform/BlockTransform.cpp index 122d71f957..19566063ec 100644 --- a/src/llvm/lib/Transform/BlockTransform.cpp +++ b/src/llvm/lib/Transform/BlockTransform.cpp @@ -52,7 +52,12 @@ void llvm2col::transformLLVMBlock(llvm::BasicBlock &llvmBlock, for (auto &I : llvmBlock) { transformInstruction(functionCursor, I, colBlock); } - functionCursor.complete(colBlock); + + // When the last instuction is a branch, the block already gets completed + // in the call to transformInstruction. + if (!functionCursor.isComplete(colBlock)) { + functionCursor.complete(colBlock); + } } void llvm2col::transformInstruction(pallas::FunctionCursor &funcCursor, From 6cde34ab0a8c6fa94f868160ab907cea537457c6 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Mon, 25 Nov 2024 15:32:20 +0100 Subject: [PATCH 05/13] First draft for inserting empty blocks into empty, conditional branches --- .../Passes/Function/FunctionBodyTransformer.h | 46 +++++- .../Transform/Instruction/OtherOpTransform.h | 3 +- .../Function/FunctionBodyTransformer.cpp | 36 +++++ .../Instruction/OtherOpTransform.cpp | 15 +- .../Transform/Instruction/TermOpTransform.cpp | 136 ++++++++++++++---- 5 files changed, 199 insertions(+), 37 deletions(-) diff --git a/src/llvm/include/Passes/Function/FunctionBodyTransformer.h b/src/llvm/include/Passes/Function/FunctionBodyTransformer.h index 3b5b6938b3..166abc11d1 100644 --- a/src/llvm/include/Passes/Function/FunctionBodyTransformer.h +++ b/src/llvm/include/Passes/Function/FunctionBodyTransformer.h @@ -1,7 +1,8 @@ #ifndef PALLAS_FUNCTIONBODYTRANSFORMER_H #define PALLAS_FUNCTIONBODYTRANSFORMER_H -#include "vct/col/ast/col.pb.h" +#include +#include #include @@ -62,6 +63,20 @@ class FunctionCursor { /// completed. std::unordered_multimap phiAssignBuffer; + /// Map that is used to determine to which block a phi-assignment should be + /// added to. Usually, this is the block that is referenced in the phi-node. + /// However, in some cases we insert empty blocks to ensure that the + /// phi-assignments are propagated correctly. + /// In these cases, the phi-assignment should be added to the newly added + /// block. + /// The key of the map has the shape (from, toPhi) and + /// maps to the new block to which the phi-assignment should be propagated + /// (here [from] is the block from which the jump to the phi-instruction + /// occurs, and [toPhi] is the block of the phi-instruction). Assumes that + /// every key is ony inserted once. + std::map, col::Block *> + phiAssignmentTargetMap; + /// Almost always when adding a variable to the variableMap, some extra /// processing is required which is why this method is private as to not /// accidentally use it outside the functionCursor @@ -131,6 +146,17 @@ class FunctionCursor { LabeledColBlock & getOrSetLLVMBlock2LabeledColBlockEntry(BasicBlock &llvmBlock); + /** + * Adds a new, uninitialized LabeledColBlock to the body of the function + * and returns a reference to this block. + * The function is intended to be used for intermediary blocks that are + * not present in the original llvm-module but are added during the + * transformation as targets for propagating phi-assignments. + * The passes instruction is used to construct the origin. + */ + LabeledColBlock + generateIntermediaryLabeledColBlock(llvm::Instruction &originInstruction); + LabeledColBlock &visitLLVMBlock(BasicBlock &llvmBlock); llvm::FunctionAnalysisManager &getFunctionAnalysisManager(); @@ -178,6 +204,24 @@ class FunctionCursor { * @return */ FDResult &getFDResult(llvm::Function &otherLLVMFunction); + + /** + * Add a new target block for a phi-assignment to the map of phi-taget + * blocks. + * @param from The block from which the edge to the phi-instruction starts. + * @param toPhi The block of the phi-instruction. + * @param newBlock The new block that was inserted on the edge. + */ + void addNewPhiAssignmentTargetBlock(col::Block &from, col::Block &toPhi, + col::Block &newBlock); + + /** + * Get the target-block for propagating a phi-assignment that is caused + * by an edge between blocks [from] --> [to]. + * If a new block was inserted on this edge, the new block is returned. + * Otherwise, [from] is returned. + */ + col::Block *getTargetForPhiAssignment(col::Block &from, col::Block &to); }; class FunctionBodyTransformerPass diff --git a/src/llvm/include/Transform/Instruction/OtherOpTransform.h b/src/llvm/include/Transform/Instruction/OtherOpTransform.h index cd86314fab..9abe241b59 100644 --- a/src/llvm/include/Transform/Instruction/OtherOpTransform.h +++ b/src/llvm/include/Transform/Instruction/OtherOpTransform.h @@ -12,9 +12,10 @@ void transformOtherOp(llvm::Instruction &llvmInstruction, col::Block &colBlock, * and retroactively assign the variable in each originating COL block of each * phi pair. * @param phiInstruction + * @param colBlock Col-block of the phi instruction * @param funcCursor */ -void transformPhi(llvm::PHINode &phiInstruction, +void transformPhi(llvm::PHINode &phiInstruction, col::Block &colBlock, pallas::FunctionCursor &funcCursor); void transformICmp(llvm::ICmpInst &icmpInstruction, col::Block &colBlock, diff --git a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp index 20ce0108a6..e1d72183db 100644 --- a/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp +++ b/src/llvm/lib/Passes/Function/FunctionBodyTransformer.cpp @@ -108,6 +108,25 @@ FunctionCursor::getOrSetLLVMBlock2LabeledColBlockEntry(BasicBlock &llvmBlock) { return llvmBlock2LabeledColBlock.at(&llvmBlock); } +LabeledColBlock FunctionCursor::generateIntermediaryLabeledColBlock( + llvm::Instruction &originInstruction) { + // create basic block + col::LlvmBasicBlock *bb = + functionBody.add_statements()->mutable_llvm_basic_block(); + bb->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(originInstruction)); + // create label declaration in buffer + col::LabelDecl *labelDecl = bb->mutable_label(); + labelDecl->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(originInstruction)); + llvm2col::setColNodeId(labelDecl); + // create nested block + col::Block *block = bb->mutable_body()->mutable_block(); + block->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(originInstruction)); + return {*bb, *block}; +} + LabeledColBlock &FunctionCursor::visitLLVMBlock(BasicBlock &llvmBlock) { LabeledColBlock &labeledBlock = this->getOrSetLLVMBlock2LabeledColBlockEntry(llvmBlock); @@ -226,6 +245,23 @@ col::Assign &FunctionCursor::createPhiAssignment(Instruction &llvmInstruction, return *assignment; } +void FunctionCursor::addNewPhiAssignmentTargetBlock(col::Block &from, + col::Block &toPhi, + col::Block &newBlock) { + phiAssignmentTargetMap.insert({{&from, &toPhi}, &newBlock}); +} + +col::Block *FunctionCursor::getTargetForPhiAssignment(col::Block &from, + col::Block &to) { + auto res = phiAssignmentTargetMap.find({&from, &to}); + if (res == phiAssignmentTargetMap.end()) { + // If the map does not contain an entry, no intermediary block has been + // added. + return &from; + } + return res->second; +} + llvm::FunctionAnalysisManager &FunctionCursor::getFunctionAnalysisManager() { return FAM; } diff --git a/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp b/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp index 43e2e4d2e0..27cf27a676 100644 --- a/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/OtherOpTransform.cpp @@ -12,7 +12,8 @@ void llvm2col::transformOtherOp(llvm::Instruction &llvmInstruction, pallas::FunctionCursor &funcCursor) { switch (llvm::Instruction::OtherOps(llvmInstruction.getOpcode())) { case llvm::Instruction::PHI: - transformPhi(llvm::cast(llvmInstruction), funcCursor); + transformPhi(llvm::cast(llvmInstruction), colBlock, + funcCursor); break; case llvm::Instruction::ICmp: transformICmp(llvm::cast(llvmInstruction), colBlock, @@ -27,15 +28,21 @@ void llvm2col::transformOtherOp(llvm::Instruction &llvmInstruction, } } -void llvm2col::transformPhi(llvm::PHINode &phiInstruction, +void llvm2col::transformPhi(llvm::PHINode &phiInstruction, col::Block &colBlock, pallas::FunctionCursor &funcCursor) { col::Variable &varDecl = funcCursor.declareVariable(phiInstruction); for (auto &B : phiInstruction.blocks()) { - // add assignment of the variable to target block + // add assignment of the variable to the block of the conditional + // branch col::Block &targetBlock = funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*B).block; + // In some cases, the phi-assignments needs to be re-targeted to an + // empty block. + col::Block *newTargetBlock = + funcCursor.getTargetForPhiAssignment(targetBlock, colBlock); + col::Assign &assignment = funcCursor.createPhiAssignment( - phiInstruction, targetBlock, varDecl); + phiInstruction, *newTargetBlock, varDecl); // assign correct value by looking at the value-block pair of phi // instruction. col::Expr *value = assignment.mutable_value(); diff --git a/src/llvm/lib/Transform/Instruction/TermOpTransform.cpp b/src/llvm/lib/Transform/Instruction/TermOpTransform.cpp index 8bb1acab7b..b83a14b0d9 100644 --- a/src/llvm/lib/Transform/Instruction/TermOpTransform.cpp +++ b/src/llvm/lib/Transform/Instruction/TermOpTransform.cpp @@ -5,6 +5,10 @@ #include "Transform/Transform.h" #include "Util/Exceptions.h" +#include +#include + + const std::string SOURCE_LOC = "Transform::Instruction::TermOp"; void llvm2col::transformTermOp(llvm::Instruction &llvmInstruction, @@ -56,14 +60,7 @@ void llvm2col::transformConditionalBranch(llvm::BranchInst &llvmBrInstruction, // pre-declare completion because the final branch statement is already // present funcCursor.complete(colBlock); - // true branch - col::Tuple2_VctColAstExpr_VctColAstStatement *colTrueBranch = - colBranch->add_branches(); - // set conditional - transformAndSetExpr(funcCursor, llvmBrInstruction, - *llvmBrInstruction.getCondition(), - *colTrueBranch->mutable_v1()); - // get or pre-generate target labeled block + /* * I hear you think, why query the 2nd operand? wouldn't that be the false * branch i.e the else branch? While any logical implementation of getting @@ -82,18 +79,63 @@ void llvm2col::transformConditionalBranch(llvm::BranchInst &llvmBrInstruction, */ auto *llvmTrueBlock = cast(llvmBrInstruction.getOperand(2)); - // transform llvm true block - transformLLVMBlock(*llvmTrueBlock, funcCursor); - pallas::LabeledColBlock labeledTrueColBlock = - funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*llvmTrueBlock); - // goto statement to true block - col::Goto *trueGoto = colTrueBranch->mutable_v2()->mutable_goto_(); - trueGoto->mutable_lbl()->set_id(labeledTrueColBlock.bb.label().id()); - // set origin for goto to true block - trueGoto->set_allocated_origin( - generateSingleStatementOrigin(llvmBrInstruction)); + auto *llvmFalseBlock = + cast(llvmBrInstruction.getOperand(1)); + + // true branch + col::Tuple2_VctColAstExpr_VctColAstStatement *colTrueBranch = + colBranch->add_branches(); + transformAndSetExpr(funcCursor, llvmBrInstruction, + *llvmBrInstruction.getCondition(), + *colTrueBranch->mutable_v1()); + + // Check if the true-branch is empty (i.e. if it jumps directly to a block + // that is also reachable from the false-branch). In that case, we need to + // add an empty block to ensure that assignments of phi-instructions get + // propagated correctly. + bool trueBranchEmpty = + isPotentiallyReachable(llvmFalseBlock, llvmTrueBlock); + if (trueBranchEmpty) { + // Build a new, empty Basic-block as a target for phi-assignments + pallas::LabeledColBlock emptyTrueBlock = + funcCursor.generateIntermediaryLabeledColBlock(llvmBrInstruction); + // Build block that is targeted by the true-branch + pallas::LabeledColBlock originalTrueBlock = + funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*llvmTrueBlock); + + // Add the new block to the map of phi-targets + funcCursor.addNewPhiAssignmentTargetBlock( + colBlock, originalTrueBlock.block, emptyTrueBlock.block); + + // Add goto to the empty block + col::Goto *gotoTrueEmpty = colTrueBranch->mutable_v2()->mutable_goto_(); + gotoTrueEmpty->mutable_lbl()->set_id(emptyTrueBlock.bb.label().id()); + gotoTrueEmpty->set_allocated_origin( + generateSingleStatementOrigin(llvmBrInstruction)); + + // Extend the empty bock with a goto to the original target block + col::Goto *gotoTrueOriginal = + emptyTrueBlock.block.add_statements()->mutable_goto_(); + gotoTrueOriginal->mutable_lbl()->set_id( + originalTrueBlock.bb.label().id()); + gotoTrueOriginal->set_allocated_origin( + generateSingleStatementOrigin(llvmBrInstruction)); + // Mark the 'empty' block as completed + funcCursor.complete(emptyTrueBlock.block); + } else { + // get or pre-generate target labeled block + pallas::LabeledColBlock labeledTrueColBlock = + funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*llvmTrueBlock); + // goto statement to true block + col::Goto *trueGoto = colTrueBranch->mutable_v2()->mutable_goto_(); + trueGoto->mutable_lbl()->set_id(labeledTrueColBlock.bb.label().id()); + // set origin for goto to true block + trueGoto->set_allocated_origin( + generateSingleStatementOrigin(llvmBrInstruction)); + } // false branch + // TODO: Implemnt case for empty false-branch (identical to true-branch) col::Tuple2_VctColAstExpr_VctColAstStatement *colFalseBranch = colBranch->add_branches(); // set conditional (which is a true constant as else == else if(true))) @@ -103,20 +145,52 @@ void llvm2col::transformConditionalBranch(llvm::BranchInst &llvmBrInstruction, // set origin of else condition elseCondition->set_allocated_origin(generateOperandOrigin( llvmBrInstruction, *llvmBrInstruction.getCondition())); - // get llvm block targeted by the llvm branch - auto *llvmFalseBlock = - cast(llvmBrInstruction.getOperand(1)); - // transform llvm falseBlock + + bool falseBranchEmpty = + isPotentiallyReachable(llvmTrueBlock, llvmFalseBlock); + + if (falseBranchEmpty) { + // Build a new, empty Basic-block as a target for phi-assignments + pallas::LabeledColBlock emptyFalseBlock = + funcCursor.generateIntermediaryLabeledColBlock(llvmBrInstruction); + // Build block that is targeted by the false-branch + pallas::LabeledColBlock originalFalseBlock = + funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*llvmFalseBlock); + + // Add the new block to the map of phi-targets + funcCursor.addNewPhiAssignmentTargetBlock( + colBlock, originalFalseBlock.block, emptyFalseBlock.block); + + // Add goto to the empty block + col::Goto *gotoFalseEmpty = + colFalseBranch->mutable_v2()->mutable_goto_(); + gotoFalseEmpty->mutable_lbl()->set_id(emptyFalseBlock.bb.label().id()); + gotoFalseEmpty->set_allocated_origin( + generateSingleStatementOrigin(llvmBrInstruction)); + + // Extend the empty bock with a goto to the original target block + col::Goto *gotoFalseOriginal = + emptyFalseBlock.block.add_statements()->mutable_goto_(); + gotoFalseOriginal->mutable_lbl()->set_id( + originalFalseBlock.bb.label().id()); + gotoFalseOriginal->set_allocated_origin( + generateSingleStatementOrigin(llvmBrInstruction)); + // Mark the 'empty' block as completed + funcCursor.complete(emptyFalseBlock.block); + } else { + pallas::LabeledColBlock labeledFalseColBlock = + funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*llvmFalseBlock); + // goto statement to false block + col::Goto *falseGoto = colFalseBranch->mutable_v2()->mutable_goto_(); + falseGoto->mutable_lbl()->set_id(labeledFalseColBlock.bb.label().id()); + // set origin for goto to false block + falseGoto->set_allocated_origin( + llvm2col::generateSingleStatementOrigin(llvmBrInstruction)); + } + + // Transform the blovks of the branches + transformLLVMBlock(*llvmTrueBlock, funcCursor); transformLLVMBlock(*llvmFalseBlock, funcCursor); - // get or pre-generate target labeled block - pallas::LabeledColBlock labeledFalseColBlock = - funcCursor.getOrSetLLVMBlock2LabeledColBlockEntry(*llvmFalseBlock); - // goto statement to false block - col::Goto *falseGoto = colFalseBranch->mutable_v2()->mutable_goto_(); - falseGoto->mutable_lbl()->set_id(labeledFalseColBlock.bb.label().id()); - // set origin for goto to false block - falseGoto->set_allocated_origin( - llvm2col::generateSingleStatementOrigin(llvmBrInstruction)); } void llvm2col::transformUnConditionalBranch( From ff6fe4bcd639fbe2e86e041c9ebc9539434a95bb Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Mon, 25 Nov 2024 16:31:07 +0100 Subject: [PATCH 06/13] Fixed DuplicateSuccessor-Error when using assignments in functions. --- src/rewrite/vct/rewrite/PureMethodsToFunctions.scala | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala b/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala index de05c4c60a..ff0c37ed0a 100644 --- a/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala +++ b/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala @@ -7,6 +7,7 @@ import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder} import vct.col.ast.RewriteHelpers._ import vct.col.ref.Ref import vct.col.util.AstBuildHelpers._ +import vct.col.util.SuccessionMap import vct.result.VerificationError.UserError case object PureMethodsToFunctions extends RewriterBuilder { @@ -32,6 +33,9 @@ case class PureMethodsToFunctions[Pre <: Generation]() extends Rewriter[Pre] { val currentAbstractMethod: ScopedStack[AbstractMethod[Pre]] = ScopedStack() + private val variableMap: SuccessionMap[Variable[Pre], Variable[Post]] = + SuccessionMap() + def countAssignments(v: Variable[Pre], s: Statement[Pre]): Option[Int] = s match { case Return(_) => Some(0) @@ -96,11 +100,11 @@ case class PureMethodsToFunctions[Pre <: Generation]() extends Rewriter[Pre] { case Assign(Local(ref), e) => alt match { case Some(exprAlt) => - Some(Let[Post]( + val vDecl = variableMap.getOrElseUpdate( + ref.decl, variables.collect { dispatch(ref.decl) }._1.head, - dispatch(e), - exprAlt, - )) + ) + Some(Let[Post](vDecl, dispatch(e), exprAlt)) case None => throw MethodCannotIntoFunction( currentAbstractMethod.top, From c94ad4c524a78933cf74ed263070a5e69474ddd8 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Tue, 26 Nov 2024 15:50:03 +0100 Subject: [PATCH 07/13] Added origins to pallas function-contracts --- src/llvm/include/Origin/OriginProvider.h | 28 ++++ .../include/Origin/PreferredNameDeriver.h | 4 +- .../PallasFunctionContractDeclarerPass.h | 23 ++- src/llvm/include/Util/Constants.h | 1 + src/llvm/lib/Origin/OriginProvider.cpp | 135 ++++++++++++++++-- src/llvm/lib/Origin/PreferredNameDeriver.cpp | 15 +- .../PallasFunctionContractDeclarerPass.cpp | 94 +++++++++--- 7 files changed, 259 insertions(+), 41 deletions(-) diff --git a/src/llvm/include/Origin/OriginProvider.h b/src/llvm/include/Origin/OriginProvider.h index 7970ce789e..cd7c272020 100644 --- a/src/llvm/include/Origin/OriginProvider.h +++ b/src/llvm/include/Origin/OriginProvider.h @@ -37,6 +37,14 @@ col::Origin *generateLabelOrigin(llvm::BasicBlock &llvmBlock); col::Origin *generateLoopOrigin(llvm::Loop &llvmLoop); +/** + * Generates an origin for a pallas function-contract. + * Assumes that the provided metadata-node is a well-formed encoding of a + * source-location (adhering to the location-format of pallas). + */ +col::Origin *generatePallasFunctionContractOrigin(const llvm::Function &f, + const llvm::MDNode &mdSrcLoc); + col::Origin *generateSingleStatementOrigin(llvm::Instruction &llvmInstruction); col::Origin *generateAssignTargetOrigin(llvm::Instruction &llvmInstruction); @@ -45,6 +53,26 @@ col::Origin *generateBinExprOrigin(llvm::Instruction &llvmInstruction); col::Origin *generateFunctionCallOrigin(llvm::CallInst &callInstruction); +/** + * Generates an origin for generated call to a wrapper function of the clause + * of a pallas function-contract. + * Assumes that the provided metadata-node is a well-formed encoding of a + * source-location (adhering to the location-format of pallas). + */ +col::Origin *generatePallasWrapperCallOrigin(const llvm::Function &wrapperFunc, + const llvm::MDNode &clauseSrcLoc); + +/** + * Generates an origin for a clause of a pallas function contract that is + * attached to the given function. Assumes that the provided metadata-node is a + * well-formed encoding of a source-location (adhering to the location-format of + * pallas). + */ +col::Origin * +generatePallasFContractClauseOrigin(const llvm::Function &parentFunc, + const llvm::MDNode &clauseSrcLoc, + unsigned int clauseNum); + col::Origin *generateOperandOrigin(llvm::Instruction &llvmInstruction, llvm::Value &llvmOperand); diff --git a/src/llvm/include/Origin/PreferredNameDeriver.h b/src/llvm/include/Origin/PreferredNameDeriver.h index 3de8fd7fcb..78bb6ca4dd 100644 --- a/src/llvm/include/Origin/PreferredNameDeriver.h +++ b/src/llvm/include/Origin/PreferredNameDeriver.h @@ -11,7 +11,7 @@ * https://github.com/utwente-fmt/vercors/discussions/884 */ namespace llvm2col { -std::string deriveOperandPreferredName(llvm::Value &llvmOperand); +std::string deriveOperandPreferredName(const llvm::Value &llvmOperand); std::string deriveTypePreferredName(llvm::Type &llvmType); @@ -19,5 +19,7 @@ std::string deriveMemoryOrderingPreferredName(llvm::AtomicOrdering &llvmOrdering); std::string deriveArgumentPreferredName(llvm::Argument &llvmArgument); + +std::string deriveFunctionPreferredName(const llvm::Function &f); } // namespace llvm2col #endif // PALLAS_PREFERREDNAMEDERIVER_H diff --git a/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h b/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h index bee2666f02..c823f32fce 100644 --- a/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h +++ b/src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h @@ -75,7 +75,9 @@ class PallasFunctionContractDeclarerPass bool addClauseToContract(col::ApplicableContract &contract, Metadata *clauseOperand, FunctionAnalysisManager &fam, Function &parentFunc, - col::LlvmFunctionDefinition &colParentFunc); + col::LlvmFunctionDefinition &colParentFunc, + unsigned int clauseNum, + const MDNode &contractSrcLoc); /** * Tries to extract the wrapper-function from the given metadata-node that @@ -106,17 +108,28 @@ class PallasFunctionContractDeclarerPass */ bool hasConflictingContract(Function &f); - /** - * Checks if the given function has a metadata-node that is labeled as a + /** + * Checks if the given function has a metadata-node that is labeled as a * Pallas function contract. */ bool hasPallasContract(const Function &f); - /** - * Checks if the given function has a metadata-node that is labeled as a + /** + * Checks if the given function has a metadata-node that is labeled as a * VCLLVM contract. */ bool hasVcllvmContract(const Function &f); + + /** + * Checks if the given metadata-node is a wellformed encoding of a + * pallas source-location. + */ + bool isWellformedPallasLocation(const MDNode *mdNode); + + /** + * Checks if the given metadata-node refers to a integer-constant. + */ + bool isConstantInt(llvm::Metadata *md); }; } // namespace pallas #endif // PALLAS_PALLASFUNCTIONCONTRACTDECLARERPASS_H diff --git a/src/llvm/include/Util/Constants.h b/src/llvm/include/Util/Constants.h index ca73c807b3..4afe72d4f9 100644 --- a/src/llvm/include/Util/Constants.h +++ b/src/llvm/include/Util/Constants.h @@ -11,6 +11,7 @@ const std::string PALLAS_FUNC_CONTRACT = "pallas.fcontract"; const std::string PALLAS_REQUIRES = "pallas.requires"; const std::string PALLAS_ENSURES = "pallas.ensures"; const std::string PALLAS_WRAPPER_FUNC = "pallas.exprWrapper"; +const std::string PALLAS_SRC_LOC_ID = "pallas.srcLoc"; // Legacy VCLLVM constants const std::string VC_PREFIX = "VC."; diff --git a/src/llvm/lib/Origin/OriginProvider.cpp b/src/llvm/lib/Origin/OriginProvider.cpp index 00d24d7960..75d40d32eb 100644 --- a/src/llvm/lib/Origin/OriginProvider.cpp +++ b/src/llvm/lib/Origin/OriginProvider.cpp @@ -1,10 +1,13 @@ #include "Origin/OriginProvider.h" +#include + #include #include "Origin/ContextDeriver.h" #include "Origin/PreferredNameDeriver.h" #include "Origin/ShortPositionDeriver.h" +#include "Util/Constants.h" namespace col = vct::col::ast; @@ -132,26 +135,23 @@ col::Origin *llvm2col::generateLabelOrigin(llvm::BasicBlock &llvmBlock) { return origin; } -bool generateDebugOrigin(const llvm::DebugLoc &loc, col::Origin *origin, - const llvm::DebugLoc &endLoc = NULL) { - if (!loc) - return false; - int line = loc.getLine() - 1; - int col = loc.getCol() - 1; +void generateSourceRangeOrigin(col::Origin *origin, const llvm::DIScope &scope, + unsigned int startLine, unsigned int startCol, + std::optional &endLine, + std::optional &endCol) { col::OriginContent *positionRangeContent = origin->add_content(); col::PositionRange *positionRange = new col::PositionRange(); - positionRange->set_start_line_idx(line); - positionRange->set_start_col_idx(col); - if (endLoc) { - positionRange->set_end_line_idx(endLoc.getLine() - 1); + positionRange->set_start_line_idx(startLine - 1); + positionRange->set_start_col_idx(startCol - 1); + if (endLine.has_value() && endCol.has_value()) { + positionRange->set_end_line_idx(*endLine - 1); // Would it be better without setting the end col? - positionRange->set_end_col_idx(endLoc.getCol() - 1); + positionRange->set_end_col_idx(*endCol - 1); } else { - positionRange->set_end_line_idx(line); + positionRange->set_end_line_idx(startLine); } positionRangeContent->set_allocated_position_range(positionRange); - auto *scope = llvm::cast(loc.getScope()); - auto *file = scope->getFile(); + auto *file = scope.getFile(); llvm::StringRef filename = file->getFilename(); llvm::StringRef directory = file->getDirectory(); auto checksumOpt = file->getChecksum(); @@ -181,6 +181,18 @@ bool generateDebugOrigin(const llvm::DebugLoc &loc, col::Origin *origin, } } readableOriginContent->set_allocated_readable_origin(readableOrigin); +} + +bool generateDebugOrigin(const llvm::DebugLoc &loc, col::Origin *origin, + const llvm::DebugLoc &endLoc = NULL) { + if (!loc) + return false; + unsigned int line = loc.getLine(); + unsigned int col = loc.getCol(); + auto endLine = endLoc ? std::make_optional(endLoc.getLine()) : std::nullopt; + auto endCol = endLoc ? std::make_optional(endLoc.getCol()) : std::nullopt; + auto *scope = llvm::cast(loc.getScope()); + generateSourceRangeOrigin(origin, *scope, line, col, endLine, endCol); return true; } @@ -199,6 +211,41 @@ col::Origin *llvm2col::generateLoopOrigin(llvm::Loop &llvmLoop) { return origin; } +namespace { +unsigned int getIntValue(llvm::Metadata *md) { + return cast( + cast(md)->getValue()) + ->getSExtValue(); +} +} // namespace + +col::Origin * +llvm2col::generatePallasFunctionContractOrigin(const llvm::Function &f, + const llvm::MDNode &mdSrcLoc) { + + col::Origin *origin = new col::Origin(); + col::OriginContent *preferredNameContent = origin->add_content(); + col::PreferredName *preferredName = new col::PreferredName(); + preferredName->add_preferred_name("Function contract of " + + deriveOperandPreferredName(f)); + preferredNameContent->set_allocated_preferred_name(preferredName); + + if (f.getSubprogram() == nullptr) { + return origin; + } + + llvm::DIScope *scope = f.getSubprogram(); + auto startLine = getIntValue(mdSrcLoc.getOperand(1).get()); + auto startCol = getIntValue(mdSrcLoc.getOperand(2).get()); + auto endLine = + std::make_optional(getIntValue(mdSrcLoc.getOperand(3).get())); + auto endCol = std::make_optional(getIntValue(mdSrcLoc.getOperand(4).get())); + generateSourceRangeOrigin(origin, *scope, startLine, startCol, endLine, + endCol); + + return origin; +} + col::Origin * llvm2col::generateSingleStatementOrigin(llvm::Instruction &llvmInstruction) { col::Origin *origin = new col::Origin(); @@ -283,6 +330,66 @@ llvm2col::generateFunctionCallOrigin(llvm::CallInst &callInstruction) { return origin; } +col::Origin * +llvm2col::generatePallasWrapperCallOrigin(const llvm::Function &wrapperFunc, + const llvm::MDNode &clauseSrcLoc) { + + col::Origin *origin = new col::Origin(); + col::OriginContent *preferredNameContent = origin->add_content(); + col::PreferredName *preferredName = new col::PreferredName(); + preferredName->add_preferred_name("Contract clause represented by " + + deriveFunctionPreferredName(wrapperFunc)); + preferredNameContent->set_allocated_preferred_name(preferredName); + + auto *scope = wrapperFunc.getSubprogram(); + if (scope == nullptr) { + return origin; + } + + // Get the source-location from the clause + auto startLine = getIntValue(clauseSrcLoc.getOperand(1).get()); + auto startCol = getIntValue(clauseSrcLoc.getOperand(2).get()); + auto endLine = + std::make_optional(getIntValue(clauseSrcLoc.getOperand(3).get())); + auto endCol = + std::make_optional(getIntValue(clauseSrcLoc.getOperand(4).get())); + generateSourceRangeOrigin(origin, *scope, startLine, startCol, endLine, + endCol); + + return origin; +} + +col::Origin * +llvm2col::generatePallasFContractClauseOrigin(const llvm::Function &parentFunc, + const llvm::MDNode &clauseSrcLoc, + unsigned int clauseNum) { + + col::Origin *origin = new col::Origin(); + col::OriginContent *preferredNameContent = origin->add_content(); + col::PreferredName *preferredName = new col::PreferredName(); + preferredName->add_preferred_name("Clause " + std::to_string(clauseNum) + + " of contract of function " + + deriveFunctionPreferredName(parentFunc)); + preferredNameContent->set_allocated_preferred_name(preferredName); + + auto *scope = parentFunc.getSubprogram(); + if (scope == nullptr) { + return origin; + } + + // Get the source-location from the clause + auto startLine = getIntValue(clauseSrcLoc.getOperand(1).get()); + auto startCol = getIntValue(clauseSrcLoc.getOperand(2).get()); + auto endLine = + std::make_optional(getIntValue(clauseSrcLoc.getOperand(3).get())); + auto endCol = + std::make_optional(getIntValue(clauseSrcLoc.getOperand(4).get())); + generateSourceRangeOrigin(origin, *scope, startLine, startCol, endLine, + endCol); + + return origin; +} + col::Origin *llvm2col::generateOperandOrigin(llvm::Instruction &llvmInstruction, llvm::Value &llvmOperand) { col::Origin *origin = new col::Origin(); diff --git a/src/llvm/lib/Origin/PreferredNameDeriver.cpp b/src/llvm/lib/Origin/PreferredNameDeriver.cpp index bd0301f8f7..60e8d4987e 100644 --- a/src/llvm/lib/Origin/PreferredNameDeriver.cpp +++ b/src/llvm/lib/Origin/PreferredNameDeriver.cpp @@ -1,10 +1,13 @@ #include "Origin/PreferredNameDeriver.h" #include +#include #include +#include #include -std::string llvm2col::deriveOperandPreferredName(llvm::Value &llvmOperand) { +std::string +llvm2col::deriveOperandPreferredName(const llvm::Value &llvmOperand) { if (!llvmOperand.getName().empty()) return std::string(llvmOperand.getName()); std::string preferredName; @@ -100,3 +103,13 @@ llvm2col::deriveArgumentPreferredName(llvm::Argument &llvmArgument) { llvmArgument.printAsOperand(preferredNameStream, false); return preferredName; } + +std::string llvm2col::deriveFunctionPreferredName(const llvm::Function &f) { + + auto *sProg = f.getSubprogram(); + if (sProg != nullptr && !sProg->getName().empty()) { + return sProg->getName().str(); + } + + return f.getName().str(); +} diff --git a/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp b/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp index 00c055300b..85a7b9eb56 100644 --- a/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp +++ b/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp @@ -63,21 +63,27 @@ PallasFunctionContractDeclarerPass::run(Function &f, return PreservedAnalyses::all(); } - // Get src location: - // TODO: Implement properly and add location to origin of - // colLLVMContract and colContract + auto *mdSrcLoc = dyn_cast(contractNode->getOperand(0).get()); + if (!isWellformedPallasLocation(mdSrcLoc)) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "Ill-formed contract. First operand should encode source-location.", + f); + return PreservedAnalyses::all(); + } + + // Build origin based on the source-location colPallasContract->set_allocated_origin( - llvm2col::generateFunctionContractOrigin( - f, "TODO: Add location-info (1)")); - colContract->set_allocated_origin(llvm2col::generateFunctionContractOrigin( - f, "TODO: Add location-info (2)")); + llvm2col::generatePallasFunctionContractOrigin(f, *mdSrcLoc)); + colContract->set_allocated_origin( + llvm2col::generatePallasFunctionContractOrigin(f, *mdSrcLoc)); // Handle contract clauses unsigned int clauseIdx = 2; while (clauseIdx < contractNode->getNumOperands()) { auto addClauseSuccess = addClauseToContract( *colContract, contractNode->getOperand(clauseIdx).get(), fam, f, - colFunction); + colFunction, clauseIdx - 1, *mdSrcLoc); if (!addClauseSuccess) return PreservedAnalyses::all(); ++clauseIdx; @@ -94,7 +100,8 @@ PallasFunctionContractDeclarerPass::run(Function &f, bool PallasFunctionContractDeclarerPass::addClauseToContract( col::ApplicableContract &contract, Metadata *clauseOperand, FunctionAnalysisManager &fam, Function &parentFunc, - col::LlvmFunctionDefinition &colParentFunc) { + col::LlvmFunctionDefinition &colParentFunc, unsigned int clauseNum, + const MDNode &contractSrcLoc) { // Try to extract MDNode auto *clause = dyn_cast_if_present(clauseOperand); @@ -127,7 +134,15 @@ bool PallasFunctionContractDeclarerPass::addClauseToContract( auto clauseTypeStr = clauseTypeMD->getString().str(); // Check source location - // TODO: Add source location to the origin + auto *clauseSrcLoc = dyn_cast(clause->getOperand(1).get()); + if (clauseSrcLoc == nullptr) { + pallas::ErrorReporter::addError( + SOURCE_LOC, + "Ill-formed contract clause. Second operand should contain " + "source location.", + parentFunc); + return false; + } // Get pointer to the LLVM wrapper-function auto *wrapperF = getWrapperFuncFromClause(*clause, parentFunc); @@ -193,8 +208,8 @@ bool PallasFunctionContractDeclarerPass::addClauseToContract( // Build a call to the wrapper-function with the gathered arguments col::LlvmFunctionInvocation *wrapperCall = new col::LlvmFunctionInvocation(); - wrapperCall->set_allocated_origin(llvm2col::generateFunctionContractOrigin( - parentFunc, "TODO: Add location-info (3)")); + wrapperCall->set_allocated_origin( + llvm2col::generatePallasWrapperCallOrigin(*wrapperF, *clauseSrcLoc)); wrapperCall->set_allocated_blame(new col::Blame()); // Build ref to parent function @@ -206,8 +221,10 @@ bool PallasFunctionContractDeclarerPass::addClauseToContract( // Construct Local-node that references the variable and add it to the // list of arguments auto *argExpr = wrapperCall->add_args()->mutable_local(); - argExpr->set_allocated_origin(llvm2col::generateFunctionContractOrigin( - parentFunc, "TODO: Add location-info (4)")); + // TODO: Currently this just points to the full clause. + // Could be extended to point to the specific variable instead. + argExpr->set_allocated_origin(llvm2col::generatePallasWrapperCallOrigin( + *wrapperF, *clauseSrcLoc)); auto *varRef = argExpr->mutable_ref(); varRef->set_id(v->id()); } @@ -215,8 +232,8 @@ bool PallasFunctionContractDeclarerPass::addClauseToContract( // Construct an AccountedPredicate the wraps the call to the // wrapper-function col::UnitAccountedPredicate *newPred = new col::UnitAccountedPredicate(); - newPred->set_allocated_origin(llvm2col::generateFunctionContractOrigin( - parentFunc, "TODO: Add location-info (5)")); + newPred->set_allocated_origin(llvm2col::generatePallasFContractClauseOrigin( + parentFunc, *clauseSrcLoc, clauseNum)); newPred->mutable_pred()->set_allocated_llvm_function_invocation( wrapperCall); @@ -229,8 +246,8 @@ bool PallasFunctionContractDeclarerPass::addClauseToContract( col::AccountedPredicate *oldPred = contract.release_requires_(); auto *reqPred = contract.mutable_requires_(); extendPredicate(reqPred, - llvm2col::generateFunctionContractOrigin( - parentFunc, "TODO: Add location-info (6)"), + llvm2col::generatePallasFunctionContractOrigin( + parentFunc, contractSrcLoc), oldPred, newPred); } } else if (clauseTypeStr == pallas::constants::PALLAS_ENSURES) { @@ -242,8 +259,8 @@ bool PallasFunctionContractDeclarerPass::addClauseToContract( col::AccountedPredicate *oldPred = contract.release_ensures(); auto *ensPred = contract.mutable_ensures(); extendPredicate(ensPred, - llvm2col::generateFunctionContractOrigin( - parentFunc, "TODO: Add location-info (7)"), + llvm2col::generatePallasFunctionContractOrigin( + parentFunc, contractSrcLoc), oldPred, newPred); } } else { @@ -372,4 +389,41 @@ bool PallasFunctionContractDeclarerPass::hasVcllvmContract(const Function &f) { return f.hasMetadata(pallas::constants::METADATA_CONTRACT_KEYWORD); } +bool PallasFunctionContractDeclarerPass::isWellformedPallasLocation( + const MDNode *mdNode) { + + if (mdNode == nullptr) + return false; + + if (mdNode->getNumOperands() != 5) + return false; + + // Check that first operand is a string-identifier + if (auto *mdStr = dyn_cast(mdNode->getOperand(0).get())) { + if (mdStr->getString().str() != pallas::constants::PALLAS_SRC_LOC_ID) + return false; + } else { + return false; + } + + // Check that the last four operands are integer constants + if (!isConstantInt(mdNode->getOperand(1).get()) || + !isConstantInt(mdNode->getOperand(2).get()) || + !isConstantInt(mdNode->getOperand(3).get()) || + !isConstantInt(mdNode->getOperand(4).get())) { + return false; + } + + return true; +} + +bool PallasFunctionContractDeclarerPass::isConstantInt(llvm::Metadata *md) { + if (auto *mdConst = dyn_cast(md)) { + if (isa(mdConst->getValue())) { + return true; + } + } + return false; +} + } // namespace pallas From 188a5db52254e82c3942c3ba46e599018da170b5 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Wed, 27 Nov 2024 09:10:15 +0100 Subject: [PATCH 08/13] Modified origin of llvm function-definition to point to source-file --- src/llvm/lib/Origin/OriginProvider.cpp | 75 ++++++++++++++++++++------ 1 file changed, 58 insertions(+), 17 deletions(-) diff --git a/src/llvm/lib/Origin/OriginProvider.cpp b/src/llvm/lib/Origin/OriginProvider.cpp index 75d40d32eb..7f1ecfb602 100644 --- a/src/llvm/lib/Origin/OriginProvider.cpp +++ b/src/llvm/lib/Origin/OriginProvider.cpp @@ -1,7 +1,11 @@ #include "Origin/OriginProvider.h" #include +#include +#include +#include +#include #include #include "Origin/ContextDeriver.h" @@ -37,23 +41,6 @@ col::Origin *llvm2col::generateProgramOrigin(llvm::Module &llvmModule) { return origin; } -col::Origin *llvm2col::generateFuncDefOrigin(llvm::Function &llvmFunction) { - col::Origin *origin = new col::Origin(); - col::OriginContent *preferredNameContent = origin->add_content(); - col::PreferredName *preferredName = new col::PreferredName(); - preferredName->add_preferred_name(llvmFunction.getName().str()); - preferredNameContent->set_allocated_preferred_name(preferredName); - - col::OriginContent *contextContent = origin->add_content(); - col::Context *context = new col::Context(); - context->set_context(deriveFunctionContext(llvmFunction)); - context->set_inline_context(deriveFunctionContext(llvmFunction)); - context->set_short_position(deriveFunctionShortPosition(llvmFunction)); - contextContent->set_allocated_context(context); - - return origin; -} - col::Origin * llvm2col::generateFunctionContractOrigin(llvm::Function &llvmFunction, const std::string &contract) { @@ -217,8 +204,62 @@ unsigned int getIntValue(llvm::Metadata *md) { cast(md)->getValue()) ->getSExtValue(); } + +std::pair getEndPosFromMD(const llvm::Function &f) { + unsigned int maxLine = 0; + unsigned int maxCol = 0; + + auto sProg = f.getSubprogram(); + if (sProg != nullptr) + maxLine = sProg->getLine(); + + for (auto it = llvm::inst_begin(f), end = llvm::inst_end(f); it != end; ++it) { + const llvm::Instruction *inst = &*it; + auto &loc = inst->getDebugLoc(); + if (!loc) + continue; + unsigned int line = loc.getLine(); + unsigned int col = loc.getCol(); + if (line > maxLine) { + maxLine = line; + maxCol = col; + } else if (line == maxLine && col > maxCol) { + maxCol = col; + } + } + return { maxLine, maxCol }; +} } // namespace +col::Origin *llvm2col::generateFuncDefOrigin(llvm::Function &llvmFunction) { + col::Origin *origin = new col::Origin(); + col::OriginContent *preferredNameContent = origin->add_content(); + col::PreferredName *preferredName = new col::PreferredName(); + preferredName->add_preferred_name(llvmFunction.getName().str()); + preferredNameContent->set_allocated_preferred_name(preferredName); + + // Try to get the source location of the function + auto *sProg = llvmFunction.getSubprogram(); + if (sProg != nullptr) { + auto endPos = getEndPosFromMD(llvmFunction); + auto endLine = std::make_optional(endPos.first); + auto endCol = std::make_optional(endPos.second);; + generateSourceRangeOrigin(origin, *sProg, sProg->getLine(), 0, + endLine, endCol); + return origin; + } + + // If the source-lacation is not available, use the IR + col::OriginContent *contextContent = origin->add_content(); + col::Context *context = new col::Context(); + context->set_context(deriveFunctionContext(llvmFunction)); + context->set_inline_context(deriveFunctionContext(llvmFunction)); + context->set_short_position(deriveFunctionShortPosition(llvmFunction)); + contextContent->set_allocated_context(context); + + return origin; +} + col::Origin * llvm2col::generatePallasFunctionContractOrigin(const llvm::Function &f, const llvm::MDNode &mdSrcLoc) { From fd3a41bcb4759b5e88c5b1a93c4d535fd760c957 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Wed, 27 Nov 2024 11:46:25 +0100 Subject: [PATCH 09/13] Fix off-by-one error in llvm-origins --- src/llvm/lib/Origin/OriginProvider.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/llvm/lib/Origin/OriginProvider.cpp b/src/llvm/lib/Origin/OriginProvider.cpp index 4bd2365522..7cd2052ad2 100644 --- a/src/llvm/lib/Origin/OriginProvider.cpp +++ b/src/llvm/lib/Origin/OriginProvider.cpp @@ -128,14 +128,16 @@ void generateSourceRangeOrigin(col::Origin *origin, const llvm::DIScope &scope, std::optional &endCol) { col::OriginContent *positionRangeContent = origin->add_content(); col::PositionRange *positionRange = new col::PositionRange(); - positionRange->set_start_line_idx(startLine - 1); - positionRange->set_start_col_idx(startCol - 1); + auto sLine = startLine - 1; + auto sCol = startCol - 1; + positionRange->set_start_line_idx(sLine); + positionRange->set_start_col_idx(sCol); if (endLine.has_value() && endCol.has_value()) { positionRange->set_end_line_idx(*endLine - 1); // Would it be better without setting the end col? positionRange->set_end_col_idx(*endCol - 1); } else { - positionRange->set_end_line_idx(startLine); + positionRange->set_end_line_idx(sLine); } positionRangeContent->set_allocated_position_range(positionRange); auto *file = scope.getFile(); From f542a51334fdaf2da62afd48f3d97d9343a0f58e Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Wed, 27 Nov 2024 16:06:27 +0100 Subject: [PATCH 10/13] Prioritize empty VCLLVM contracts over empty pallas contracts --- .../PallasFunctionContractDeclarerPass.cpp | 25 ++++--------------- 1 file changed, 5 insertions(+), 20 deletions(-) diff --git a/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp b/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp index 85a7b9eb56..d822191dc2 100644 --- a/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp +++ b/src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp @@ -28,8 +28,11 @@ PallasFunctionContractDeclarerPass::run(Function &f, // Check that f does not have a VCLLVM AND a Pallas contract if (hasConflictingContract(f)) return PreservedAnalyses::all(); - // Skip, if f has a non-empty vcllvm-contract - if (hasVcllvmContract(f)) + // Skip, if f has a non-empty vcllvm-contract, or no contract at all + // If it does not have a contract, we need an empty VCLLVM contract instead + // of an empty Pallas contract. Otherwise the mechanism for loading + // contracts from a PVL-file does not get invoked. + if (hasVcllvmContract(f) || !hasPallasContract(f)) return PreservedAnalyses::all(); // Setup a fresh Pallas-contract @@ -46,15 +49,6 @@ PallasFunctionContractDeclarerPass::run(Function &f, col::ApplicableContract *colContract = colPallasContract->mutable_content(); colContract->set_allocated_blame(new col::Blame()); - // Check if a Pallas-contract is attached to the function: - if (!f.hasMetadata(pallas::constants::PALLAS_FUNC_CONTRACT)) { - // No contract is present --> add trivial contract - colPallasContract->set_allocated_origin( - llvm2col::generateFunctionContractOrigin(f, "Empty contract")); - initializeTrivialContract(*colContract, f); - return PreservedAnalyses::all(); - } - // Check wellformedness of the contract-metadata auto *contractNode = f.getMetadata(pallas::constants::PALLAS_FUNC_CONTRACT); if (contractNode->getNumOperands() < 2) { @@ -301,15 +295,6 @@ Function *PallasFunctionContractDeclarerPass::getWrapperFuncFromClause( return wrapperF; } -void PallasFunctionContractDeclarerPass::initializeTrivialContract( - col::ApplicableContract &contract, Function &f) { - contract.set_allocated_origin( - llvm2col::generateFunctionContractOrigin(f, "Empty contract")); - addEmptyRequires(contract, f); - addEmptyEnsures(contract, f); - addEmptyContextEverywhere(contract, f); -} - void PallasFunctionContractDeclarerPass::addEmptyRequires( col::ApplicableContract &contract, Function &f) { From 432db27a320dd14202cf4896473ab6e15c216380 Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Thu, 28 Nov 2024 09:57:19 +0100 Subject: [PATCH 11/13] Added basic tests for the pallas function contracts --- .../llvm/pallas/pallas_function_contract.c | 22 +++ .../llvm/pallas/pallas_function_contract.ll | 165 ++++++++++++++++++ .../pallas/pallas_function_contract_fail.c | 11 ++ .../pallas/pallas_function_contract_fail.ll | 122 +++++++++++++ .../test/integration/examples/LLVMSpec.scala | 4 + 5 files changed, 324 insertions(+) create mode 100644 examples/concepts/llvm/pallas/pallas_function_contract.c create mode 100644 examples/concepts/llvm/pallas/pallas_function_contract.ll create mode 100644 examples/concepts/llvm/pallas/pallas_function_contract_fail.c create mode 100644 examples/concepts/llvm/pallas/pallas_function_contract_fail.ll diff --git a/examples/concepts/llvm/pallas/pallas_function_contract.c b/examples/concepts/llvm/pallas/pallas_function_contract.c new file mode 100644 index 0000000000..84367f9d6a --- /dev/null +++ b/examples/concepts/llvm/pallas/pallas_function_contract.c @@ -0,0 +1,22 @@ +// Simple demo of a Pallas function-contract that is expected to verify. + +/*@ + requires a >= 0 && b >= 0; + ensures a >= -1 && b > -1; + @*/ +int foo (int a, int b) { + + + return a * b + 1; +} + + +/*@ + requires x < 0; +@*/ +int bar (int x) { + int y = 1; + y += x; + y *= 42; + return y; +} diff --git a/examples/concepts/llvm/pallas/pallas_function_contract.ll b/examples/concepts/llvm/pallas/pallas_function_contract.ll new file mode 100644 index 0000000000..725495c505 --- /dev/null +++ b/examples/concepts/llvm/pallas/pallas_function_contract.ll @@ -0,0 +1,165 @@ +; ModuleID = './tmp/tmp_ir_source0.ll' +source_filename = "examples/concepts/llvm/pallas/pallas_function_contract.c" +target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-unknown-linux-gnu" + +@llvm.used = appending global [3 x ptr] [ptr @PALLAS_SPEC_0, ptr @PALLAS_SPEC_1, ptr @PALLAS_SPEC_2], section "llvm.metadata" + +; Function Attrs: noinline nounwind uwtable +define dso_local i32 @foo(i32 noundef %0, i32 noundef %1) #0 !dbg !12 !pallas.fcontract !17 { + %3 = alloca i32, align 4 + %4 = alloca i32, align 4 + store i32 %0, ptr %3, align 4 + call void @llvm.dbg.declare(metadata ptr %3, metadata !21, metadata !DIExpression()), !dbg !25 + store i32 %1, ptr %4, align 4 + call void @llvm.dbg.declare(metadata ptr %4, metadata !22, metadata !DIExpression()), !dbg !26 + %5 = load i32, ptr %3, align 4, !dbg !27 + %6 = load i32, ptr %4, align 4, !dbg !28 + %7 = mul nsw i32 %5, %6, !dbg !29 + %8 = add nsw i32 %7, 1, !dbg !30 + ret i32 %8, !dbg !31 +} + +; Function Attrs: nocallback nofree nosync nounwind speculatable willreturn memory(none) +declare void @llvm.dbg.declare(metadata, metadata, metadata) #1 + +; Function Attrs: noinline nounwind uwtable +define dso_local i32 @bar(i32 noundef %0) #0 !dbg !32 !pallas.fcontract !35 { + %2 = alloca i32, align 4 + %3 = alloca i32, align 4 + store i32 %0, ptr %2, align 4 + call void @llvm.dbg.declare(metadata ptr %2, metadata !39, metadata !DIExpression()), !dbg !40 + call void @llvm.dbg.declare(metadata ptr %3, metadata !41, metadata !DIExpression()), !dbg !42 + store i32 1, ptr %3, align 4, !dbg !42 + %4 = load i32, ptr %2, align 4, !dbg !43 + %5 = load i32, ptr %3, align 4, !dbg !44 + %6 = add nsw i32 %5, %4, !dbg !44 + store i32 %6, ptr %3, align 4, !dbg !44 + %7 = load i32, ptr %3, align 4, !dbg !45 + %8 = mul nsw i32 %7, 42, !dbg !45 + store i32 %8, ptr %3, align 4, !dbg !45 + %9 = load i32, ptr %3, align 4, !dbg !46 + ret i32 %9, !dbg !47 +} + +; Function Attrs: noinline nounwind uwtable +define dso_local zeroext i1 @PALLAS_SPEC_0(i32 noundef %0, i32 noundef %1) #0 !dbg !48 !pallas.exprWrapper !52 { + call void @llvm.dbg.value(metadata i32 %0, metadata !53, metadata !DIExpression()), !dbg !54 + call void @llvm.dbg.value(metadata i32 %1, metadata !55, metadata !DIExpression()), !dbg !54 + %3 = icmp sge i32 %0, 0, !dbg !56 + br i1 %3, label %4, label %6, !dbg !57 + +4: ; preds = %2 + %5 = icmp sge i32 %1, 0, !dbg !58 + br label %6 + +6: ; preds = %4, %2 + %7 = phi i1 [ false, %2 ], [ %5, %4 ], !dbg !54 + ret i1 %7, !dbg !54 +} + +; Function Attrs: noinline nounwind uwtable +define dso_local zeroext i1 @PALLAS_SPEC_1(i32 noundef %0, i32 noundef %1) #0 !dbg !59 !pallas.exprWrapper !52 { + call void @llvm.dbg.value(metadata i32 %0, metadata !60, metadata !DIExpression()), !dbg !61 + call void @llvm.dbg.value(metadata i32 %1, metadata !62, metadata !DIExpression()), !dbg !61 + %3 = icmp sge i32 %0, -1, !dbg !63 + br i1 %3, label %4, label %6, !dbg !64 + +4: ; preds = %2 + %5 = icmp sgt i32 %1, -1, !dbg !65 + br label %6 + +6: ; preds = %4, %2 + %7 = phi i1 [ false, %2 ], [ %5, %4 ], !dbg !61 + ret i1 %7, !dbg !61 +} + +; Function Attrs: noinline nounwind uwtable +define dso_local zeroext i1 @PALLAS_SPEC_2(i32 noundef %0) #0 !dbg !66 !pallas.exprWrapper !52 { + call void @llvm.dbg.value(metadata i32 %0, metadata !69, metadata !DIExpression()), !dbg !70 + %2 = icmp slt i32 %0, 0, !dbg !71 + ret i1 %2, !dbg !70 +} + +; Function Attrs: nocallback nofree nosync nounwind speculatable willreturn memory(none) +declare void @llvm.dbg.value(metadata, metadata, metadata) #1 + +attributes #0 = { noinline nounwind uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cmov,+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" } +attributes #1 = { nocallback nofree nosync nounwind speculatable willreturn memory(none) } + +!llvm.dbg.cu = !{!0, !2} +!llvm.module.flags = !{!4, !5, !6, !7, !8, !9, !10} +!llvm.ident = !{!11, !11} + +!0 = distinct !DICompileUnit(language: DW_LANG_C11, file: !1, producer: "clang version 17.0.0 (https://github.com/swiftlang/llvm-project.git 73500bf55acff5fa97b56dcdeb013f288efd084f)", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, splitDebugInlining: false, nameTableKind: None) +!1 = !DIFile(filename: "examples/concepts/llvm/pallas/pallas_function_contract.c", directory: ".", checksumkind: CSK_MD5, checksum: "eaa158c4f64ea69ddbfd098d72f0c838") +!2 = distinct !DICompileUnit(language: DW_LANG_C11, file: !3, producer: "clang version 17.0.0 (https://github.com/swiftlang/llvm-project.git 73500bf55acff5fa97b56dcdeb013f288efd084f)", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, splitDebugInlining: false, nameTableKind: None) +!3 = !DIFile(filename: "tmp/source_wrappers.c", directory: ".", checksumkind: CSK_MD5, checksum: "1d11760277123c84c4c47dae01fa0129") +!4 = !{i32 7, !"Dwarf Version", i32 5} +!5 = !{i32 2, !"Debug Info Version", i32 3} +!6 = !{i32 1, !"wchar_size", i32 4} +!7 = !{i32 8, !"PIC Level", i32 2} +!8 = !{i32 7, !"PIE Level", i32 2} +!9 = !{i32 7, !"uwtable", i32 2} +!10 = !{i32 7, !"frame-pointer", i32 2} +!11 = !{!"clang version 17.0.0 (https://github.com/swiftlang/llvm-project.git 73500bf55acff5fa97b56dcdeb013f288efd084f)"} +!12 = distinct !DISubprogram(name: "foo", scope: !1, file: !1, line: 7, type: !13, scopeLine: 7, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!13 = !DISubroutineType(types: !14) +!14 = !{!15, !15, !15} +!15 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed) +!16 = !{} +!17 = !{!18, i1 false, !19, !23} +!18 = !{!"pallas.srcLoc", i64 3, i64 1, i64 6, i64 2} +!19 = !{!"pallas.requires", !20, ptr @PALLAS_SPEC_0, !21, !22} +!20 = !{!"pallas.srcLoc", i64 4, i64 2, i64 4, i64 27} +!21 = !DILocalVariable(name: "a", arg: 1, scope: !12, file: !1, line: 7, type: !15) +!22 = !DILocalVariable(name: "b", arg: 2, scope: !12, file: !1, line: 7, type: !15) +!23 = !{!"pallas.ensures", !24, ptr @PALLAS_SPEC_1, !21, !22} +!24 = !{!"pallas.srcLoc", i64 5, i64 2, i64 5, i64 27} +!25 = !DILocation(line: 7, column: 14, scope: !12) +!26 = !DILocation(line: 7, column: 21, scope: !12) +!27 = !DILocation(line: 10, column: 12, scope: !12) +!28 = !DILocation(line: 10, column: 16, scope: !12) +!29 = !DILocation(line: 10, column: 14, scope: !12) +!30 = !DILocation(line: 10, column: 18, scope: !12) +!31 = !DILocation(line: 10, column: 5, scope: !12) +!32 = distinct !DISubprogram(name: "bar", scope: !1, file: !1, line: 17, type: !33, scopeLine: 17, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!33 = !DISubroutineType(types: !34) +!34 = !{!15, !15} +!35 = !{!36, i1 false, !37} +!36 = !{!"pallas.srcLoc", i64 14, i64 1, i64 16, i64 1} +!37 = !{!"pallas.requires", !38, ptr @PALLAS_SPEC_2, !39} +!38 = !{!"pallas.srcLoc", i64 15, i64 2, i64 15, i64 16} +!39 = !DILocalVariable(name: "x", arg: 1, scope: !32, file: !1, line: 17, type: !15) +!40 = !DILocation(line: 17, column: 14, scope: !32) +!41 = !DILocalVariable(name: "y", scope: !32, file: !1, line: 18, type: !15) +!42 = !DILocation(line: 18, column: 9, scope: !32) +!43 = !DILocation(line: 19, column: 10, scope: !32) +!44 = !DILocation(line: 19, column: 7, scope: !32) +!45 = !DILocation(line: 20, column: 7, scope: !32) +!46 = !DILocation(line: 21, column: 12, scope: !32) +!47 = !DILocation(line: 21, column: 5, scope: !32) +!48 = distinct !DISubprogram(name: "PALLAS_SPEC_0", scope: !1, file: !1, line: 4, type: !49, scopeLine: 4, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!49 = !DISubroutineType(types: !50) +!50 = !{!51, !15, !15} +!51 = !DIBasicType(name: "_Bool", size: 8, encoding: DW_ATE_boolean) +!52 = !{!""} +!53 = !DILocalVariable(name: "a", arg: 1, scope: !48, file: !1, line: 4, type: !15) +!54 = !DILocation(line: 0, scope: !48) +!55 = !DILocalVariable(name: "b", arg: 2, scope: !48, file: !1, line: 4, type: !15) +!56 = !DILocation(line: 4, column: 13, scope: !48) +!57 = !DILocation(line: 4, column: 18, scope: !48) +!58 = !DILocation(line: 4, column: 23, scope: !48) +!59 = distinct !DISubprogram(name: "PALLAS_SPEC_1", scope: !1, file: !1, line: 5, type: !49, scopeLine: 5, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!60 = !DILocalVariable(name: "a", arg: 1, scope: !59, file: !1, line: 5, type: !15) +!61 = !DILocation(line: 0, scope: !59) +!62 = !DILocalVariable(name: "b", arg: 2, scope: !59, file: !1, line: 5, type: !15) +!63 = !DILocation(line: 5, column: 12, scope: !59) +!64 = !DILocation(line: 5, column: 18, scope: !59) +!65 = !DILocation(line: 5, column: 23, scope: !59) +!66 = distinct !DISubprogram(name: "PALLAS_SPEC_2", scope: !1, file: !1, line: 15, type: !67, scopeLine: 15, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!67 = !DISubroutineType(types: !68) +!68 = !{!51, !15} +!69 = !DILocalVariable(name: "x", arg: 1, scope: !66, file: !1, line: 15, type: !15) +!70 = !DILocation(line: 0, scope: !66) +!71 = !DILocation(line: 15, column: 13, scope: !66) diff --git a/examples/concepts/llvm/pallas/pallas_function_contract_fail.c b/examples/concepts/llvm/pallas/pallas_function_contract_fail.c new file mode 100644 index 0000000000..086d3e4a2a --- /dev/null +++ b/examples/concepts/llvm/pallas/pallas_function_contract_fail.c @@ -0,0 +1,11 @@ +// Simple demo of a Pallas function-contract that is expected to fail. + +/*@ + requires a >= 0 && b >= 0; + ensures a > 0; + @*/ +int foo (int a, int b) { + int x = a + b; + x ++; + return x * b + 1; +} diff --git a/examples/concepts/llvm/pallas/pallas_function_contract_fail.ll b/examples/concepts/llvm/pallas/pallas_function_contract_fail.ll new file mode 100644 index 0000000000..b4ddf236c1 --- /dev/null +++ b/examples/concepts/llvm/pallas/pallas_function_contract_fail.ll @@ -0,0 +1,122 @@ +; ModuleID = './tmp/tmp_ir_source0.ll' +source_filename = "examples/concepts/llvm/pallas/pallas_function_contract_fail.c" +target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128" +target triple = "x86_64-unknown-linux-gnu" + +@llvm.used = appending global [2 x ptr] [ptr @PALLAS_SPEC_0, ptr @PALLAS_SPEC_1], section "llvm.metadata" + +; Function Attrs: noinline nounwind uwtable +define dso_local i32 @foo(i32 noundef %0, i32 noundef %1) #0 !dbg !12 !pallas.fcontract !17 { + %3 = alloca i32, align 4 + %4 = alloca i32, align 4 + %5 = alloca i32, align 4 + store i32 %0, ptr %3, align 4 + call void @llvm.dbg.declare(metadata ptr %3, metadata !21, metadata !DIExpression()), !dbg !25 + store i32 %1, ptr %4, align 4 + call void @llvm.dbg.declare(metadata ptr %4, metadata !22, metadata !DIExpression()), !dbg !26 + call void @llvm.dbg.declare(metadata ptr %5, metadata !27, metadata !DIExpression()), !dbg !28 + %6 = load i32, ptr %3, align 4, !dbg !29 + %7 = load i32, ptr %4, align 4, !dbg !30 + %8 = add nsw i32 %6, %7, !dbg !31 + store i32 %8, ptr %5, align 4, !dbg !28 + %9 = load i32, ptr %5, align 4, !dbg !32 + %10 = add nsw i32 %9, 1, !dbg !32 + store i32 %10, ptr %5, align 4, !dbg !32 + %11 = load i32, ptr %5, align 4, !dbg !33 + %12 = load i32, ptr %4, align 4, !dbg !34 + %13 = mul nsw i32 %11, %12, !dbg !35 + %14 = add nsw i32 %13, 1, !dbg !36 + ret i32 %14, !dbg !37 +} + +; Function Attrs: nocallback nofree nosync nounwind speculatable willreturn memory(none) +declare void @llvm.dbg.declare(metadata, metadata, metadata) #1 + +; Function Attrs: noinline nounwind uwtable +define dso_local zeroext i1 @PALLAS_SPEC_0(i32 noundef %0, i32 noundef %1) #0 !dbg !38 !pallas.exprWrapper !42 { + call void @llvm.dbg.value(metadata i32 %0, metadata !43, metadata !DIExpression()), !dbg !44 + call void @llvm.dbg.value(metadata i32 %1, metadata !45, metadata !DIExpression()), !dbg !44 + %3 = icmp sge i32 %0, 0, !dbg !46 + br i1 %3, label %4, label %6, !dbg !47 + +4: ; preds = %2 + %5 = icmp sge i32 %1, 0, !dbg !48 + br label %6 + +6: ; preds = %4, %2 + %7 = phi i1 [ false, %2 ], [ %5, %4 ], !dbg !44 + ret i1 %7, !dbg !44 +} + +; Function Attrs: noinline nounwind uwtable +define dso_local zeroext i1 @PALLAS_SPEC_1(i32 noundef %0, i32 noundef %1) #0 !dbg !49 !pallas.exprWrapper !42 { + call void @llvm.dbg.value(metadata i32 %0, metadata !50, metadata !DIExpression()), !dbg !51 + call void @llvm.dbg.value(metadata i32 %1, metadata !52, metadata !DIExpression()), !dbg !51 + %3 = icmp sgt i32 %0, 0, !dbg !53 + ret i1 %3, !dbg !51 +} + +; Function Attrs: nocallback nofree nosync nounwind speculatable willreturn memory(none) +declare void @llvm.dbg.value(metadata, metadata, metadata) #1 + +attributes #0 = { noinline nounwind uwtable "frame-pointer"="all" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cmov,+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "tune-cpu"="generic" } +attributes #1 = { nocallback nofree nosync nounwind speculatable willreturn memory(none) } + +!llvm.dbg.cu = !{!0, !2} +!llvm.module.flags = !{!4, !5, !6, !7, !8, !9, !10} +!llvm.ident = !{!11, !11} + +!0 = distinct !DICompileUnit(language: DW_LANG_C11, file: !1, producer: "clang version 17.0.0 (https://github.com/swiftlang/llvm-project.git 73500bf55acff5fa97b56dcdeb013f288efd084f)", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, splitDebugInlining: false, nameTableKind: None) +!1 = !DIFile(filename: "examples/concepts/llvm/pallas/pallas_function_contract_fail.c", directory: ".", checksumkind: CSK_MD5, checksum: "b2c55039ef8597bdf6b1007bdadab617") +!2 = distinct !DICompileUnit(language: DW_LANG_C11, file: !3, producer: "clang version 17.0.0 (https://github.com/swiftlang/llvm-project.git 73500bf55acff5fa97b56dcdeb013f288efd084f)", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, splitDebugInlining: false, nameTableKind: None) +!3 = !DIFile(filename: "tmp/source_wrappers.c", directory: ".", checksumkind: CSK_MD5, checksum: "db2f546b04510fe9d3ba505f9cc0522b") +!4 = !{i32 7, !"Dwarf Version", i32 5} +!5 = !{i32 2, !"Debug Info Version", i32 3} +!6 = !{i32 1, !"wchar_size", i32 4} +!7 = !{i32 8, !"PIC Level", i32 2} +!8 = !{i32 7, !"PIE Level", i32 2} +!9 = !{i32 7, !"uwtable", i32 2} +!10 = !{i32 7, !"frame-pointer", i32 2} +!11 = !{!"clang version 17.0.0 (https://github.com/swiftlang/llvm-project.git 73500bf55acff5fa97b56dcdeb013f288efd084f)"} +!12 = distinct !DISubprogram(name: "foo", scope: !1, file: !1, line: 7, type: !13, scopeLine: 7, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!13 = !DISubroutineType(types: !14) +!14 = !{!15, !15, !15} +!15 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed) +!16 = !{} +!17 = !{!18, i1 false, !19, !23} +!18 = !{!"pallas.srcLoc", i64 3, i64 1, i64 6, i64 2} +!19 = !{!"pallas.requires", !20, ptr @PALLAS_SPEC_0, !21, !22} +!20 = !{!"pallas.srcLoc", i64 4, i64 2, i64 4, i64 27} +!21 = !DILocalVariable(name: "a", arg: 1, scope: !12, file: !1, line: 7, type: !15) +!22 = !DILocalVariable(name: "b", arg: 2, scope: !12, file: !1, line: 7, type: !15) +!23 = !{!"pallas.ensures", !24, ptr @PALLAS_SPEC_1, !21, !22} +!24 = !{!"pallas.srcLoc", i64 5, i64 2, i64 5, i64 15} +!25 = !DILocation(line: 7, column: 14, scope: !12) +!26 = !DILocation(line: 7, column: 21, scope: !12) +!27 = !DILocalVariable(name: "x", scope: !12, file: !1, line: 8, type: !15) +!28 = !DILocation(line: 8, column: 9, scope: !12) +!29 = !DILocation(line: 8, column: 13, scope: !12) +!30 = !DILocation(line: 8, column: 17, scope: !12) +!31 = !DILocation(line: 8, column: 15, scope: !12) +!32 = !DILocation(line: 9, column: 7, scope: !12) +!33 = !DILocation(line: 10, column: 12, scope: !12) +!34 = !DILocation(line: 10, column: 16, scope: !12) +!35 = !DILocation(line: 10, column: 14, scope: !12) +!36 = !DILocation(line: 10, column: 18, scope: !12) +!37 = !DILocation(line: 10, column: 5, scope: !12) +!38 = distinct !DISubprogram(name: "PALLAS_SPEC_0", scope: !1, file: !1, line: 4, type: !39, scopeLine: 4, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!39 = !DISubroutineType(types: !40) +!40 = !{!41, !15, !15} +!41 = !DIBasicType(name: "_Bool", size: 8, encoding: DW_ATE_boolean) +!42 = !{!""} +!43 = !DILocalVariable(name: "a", arg: 1, scope: !38, file: !1, line: 4, type: !15) +!44 = !DILocation(line: 0, scope: !38) +!45 = !DILocalVariable(name: "b", arg: 2, scope: !38, file: !1, line: 4, type: !15) +!46 = !DILocation(line: 4, column: 13, scope: !38) +!47 = !DILocation(line: 4, column: 18, scope: !38) +!48 = !DILocation(line: 4, column: 23, scope: !38) +!49 = distinct !DISubprogram(name: "PALLAS_SPEC_1", scope: !1, file: !1, line: 5, type: !39, scopeLine: 5, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !0, retainedNodes: !16) +!50 = !DILocalVariable(name: "a", arg: 1, scope: !49, file: !1, line: 5, type: !15) +!51 = !DILocation(line: 0, scope: !49) +!52 = !DILocalVariable(name: "b", arg: 2, scope: !49, file: !1, line: 5, type: !15) +!53 = !DILocation(line: 5, column: 12, scope: !49) diff --git a/test/main/vct/test/integration/examples/LLVMSpec.scala b/test/main/vct/test/integration/examples/LLVMSpec.scala index 799f214854..37b949e283 100644 --- a/test/main/vct/test/integration/examples/LLVMSpec.scala +++ b/test/main/vct/test/integration/examples/LLVMSpec.scala @@ -26,4 +26,8 @@ class LLVMSpec extends VercorsSpec { 2: ret void } """ + + // Pallas specifications: + vercors should verify using silicon example "concepts/llvm/pallas/pallas_function_contract.ll" + vercors should fail withCode "postFailed:false" using silicon example "concepts/llvm/pallas/pallas_function_contract_fail.ll" } From f7b0f0c31ea70c3e4b0d3d0a6373f39c2d5c95fa Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Thu, 28 Nov 2024 10:33:14 +0100 Subject: [PATCH 12/13] Added c-files that are used to generate .ll to exclusion --- test/main/vct/test/integration/helper/ExampleFiles.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/test/main/vct/test/integration/helper/ExampleFiles.scala b/test/main/vct/test/integration/helper/ExampleFiles.scala index 278a6c8370..b29110cb06 100644 --- a/test/main/vct/test/integration/helper/ExampleFiles.scala +++ b/test/main/vct/test/integration/helper/ExampleFiles.scala @@ -30,7 +30,9 @@ case object ExampleFiles { val CONTRACT_FILES: Set[String] = Set( "examples/concepts/llvm/cubed-contracts.pvl", - "examples/concepts/llvm/void-contracts.pvl" + "examples/concepts/llvm/void-contracts.pvl", + "examples/concepts/llvm/pallas/pallas_function_contract.c", + "examples/concepts/llvm/pallas/pallas_function_contract_fail.c", ).map(_.replaceAll("/", File.separator)) val EXCLUSIONS: Seq[Path => Boolean] = Seq( From ce2783c76457d04bab57e116ef14f106c2d8edda Mon Sep 17 00:00:00 2001 From: Robert <27515600+RobertMensing@users.noreply.github.com> Date: Thu, 28 Nov 2024 12:57:40 +0100 Subject: [PATCH 13/13] Fixed scoping of let in PureMethodsToFunctions --- .../vct/rewrite/PureMethodsToFunctions.scala | 31 ++++++++++--------- 1 file changed, 16 insertions(+), 15 deletions(-) diff --git a/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala b/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala index ff0c37ed0a..c3d17d8918 100644 --- a/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala +++ b/src/rewrite/vct/rewrite/PureMethodsToFunctions.scala @@ -33,9 +33,6 @@ case class PureMethodsToFunctions[Pre <: Generation]() extends Rewriter[Pre] { val currentAbstractMethod: ScopedStack[AbstractMethod[Pre]] = ScopedStack() - private val variableMap: SuccessionMap[Variable[Pre], Variable[Post]] = - SuccessionMap() - def countAssignments(v: Variable[Pre], s: Statement[Pre]): Option[Int] = s match { case Return(_) => Some(0) @@ -98,18 +95,22 @@ case class PureMethodsToFunctions[Pre <: Generation]() extends Rewriter[Pre] { } toExpression(impl, alt) case Assign(Local(ref), e) => - alt match { - case Some(exprAlt) => - val vDecl = variableMap.getOrElseUpdate( - ref.decl, - variables.collect { dispatch(ref.decl) }._1.head, - ) - Some(Let[Post](vDecl, dispatch(e), exprAlt)) - case None => - throw MethodCannotIntoFunction( - currentAbstractMethod.top, - "Pure method cannot end with assign statement", - ) + localHeapVariables.scope { + variables.scope { + alt match { + case Some(exprAlt) => + Some(Let[Post]( + variables.collect { dispatch(ref.decl) }._1.head, + dispatch(e), + exprAlt, + )) + case None => + throw MethodCannotIntoFunction( + currentAbstractMethod.top, + "Pure method cannot end with assign statement", + ) + } + } } case _ => None