Skip to content

Commit

Permalink
Added origins to pallas function-contracts
Browse files Browse the repository at this point in the history
  • Loading branch information
RobertMensing committed Nov 26, 2024
1 parent ff6fe4b commit c94ad4c
Show file tree
Hide file tree
Showing 7 changed files with 259 additions and 41 deletions.
28 changes: 28 additions & 0 deletions src/llvm/include/Origin/OriginProvider.h
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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);

Expand Down
4 changes: 3 additions & 1 deletion src/llvm/include/Origin/PreferredNameDeriver.h
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,15 @@
* 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);

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
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
1 change: 1 addition & 0 deletions src/llvm/include/Util/Constants.h
Original file line number Diff line number Diff line change
Expand Up @@ -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.";
Expand Down
135 changes: 121 additions & 14 deletions src/llvm/lib/Origin/OriginProvider.cpp
Original file line number Diff line number Diff line change
@@ -1,10 +1,13 @@
#include "Origin/OriginProvider.h"

#include <optional>

#include <llvm/IR/Module.h>

#include "Origin/ContextDeriver.h"
#include "Origin/PreferredNameDeriver.h"
#include "Origin/ShortPositionDeriver.h"
#include "Util/Constants.h"

namespace col = vct::col::ast;

Expand Down Expand Up @@ -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<unsigned int> &endLine,
std::optional<unsigned int> &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<llvm::DIScope>(loc.getScope());
auto *file = scope->getFile();
auto *file = scope.getFile();
llvm::StringRef filename = file->getFilename();
llvm::StringRef directory = file->getDirectory();
auto checksumOpt = file->getChecksum();
Expand Down Expand Up @@ -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<llvm::DIScope>(loc.getScope());
generateSourceRangeOrigin(origin, *scope, line, col, endLine, endCol);
return true;
}

Expand All @@ -199,6 +211,41 @@ col::Origin *llvm2col::generateLoopOrigin(llvm::Loop &llvmLoop) {
return origin;
}

namespace {
unsigned int getIntValue(llvm::Metadata *md) {
return cast<llvm::ConstantInt>(
cast<llvm::ConstantAsMetadata>(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();
Expand Down Expand Up @@ -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();
Expand Down
15 changes: 14 additions & 1 deletion src/llvm/lib/Origin/PreferredNameDeriver.cpp
Original file line number Diff line number Diff line change
@@ -1,10 +1,13 @@
#include "Origin/PreferredNameDeriver.h"

#include <llvm/IR/Argument.h>
#include <llvm/IR/DebugInfoMetadata.h>
#include <llvm/IR/DerivedTypes.h>
#include <llvm/IR/Function.h>
#include <llvm/Support/raw_ostream.h>

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;
Expand Down Expand Up @@ -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();
}
Loading

0 comments on commit c94ad4c

Please sign in to comment.