First draft of supporting \result in Pallas specifications

src/col/vct/col/ast/Node.scala

@@ -3524,6 +3524,12 @@ final class LLVMFunctionDefinition[G](
     val functionBody: Option[Statement[G]],
     val contract: LLVMFunctionContract[G],
     val pure: Boolean = false,
+    // If this function is a wrapper function for an expression of a
+    // pallas specification of a function F, then this field references F.
+    val pallasExprWrapperFor: Option[Ref[G, LLVMFunctionDefinition[G]]],
+    // Indicates that a new argument has to be added to pass the value for \result
+    // to the expression-wrapper.
+    val needsWrapperResultArg: Boolean = false,
 )(val blame: Blame[CallableFailure])(implicit val o: Origin)
     extends LLVMCallable[G]
     with Applicable[G]
@@ -3664,6 +3670,11 @@ final class LLVMGlobalSpecification[G](val value: String)(
   var data: Option[Seq[GlobalDeclaration[G]]] = None
 }
 
+// Node that represents the \result-construct in a Pallas contract.
+final case class LLVMResult[G](func: Ref[G, LLVMFunctionDefinition[G]])(
+    implicit val o: Origin
+) extends LLVMExpr[G] with LLVMResultImpl[G]
+
 @family
 sealed trait LLVMMemoryOrdering[G]
     extends NodeFamily[G] with LLVMMemoryOrderingImpl[G]

src/col/vct/col/ast/lang/llvm/LLVMResultImpl.scala

@@ -0,0 +1,13 @@
+package vct.col.ast.lang.llvm
+
+import vct.col.ast.node.NodeFamilyImpl
+import vct.col.ast.ops.LLVMResultOps
+import vct.col.ast.{LLVMResult, Type}
+import vct.col.print.Precedence
+
+trait LLVMResultImpl[G] extends NodeFamilyImpl[G] with LLVMResultOps[G] {
+  this: LLVMResult[G] =>
+  override def t: Type[G] = func.decl.returnType
+
+  override def precedence: Int = Precedence.ATOMIC
+}

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -2147,6 +2147,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
       case LLVMVectorValue(_, _) => e
       case LLVMRawVectorValue(_, _) => e
       case LLVMZeroedAggregateValue(_) => e
+      case LLVMResult(_) => e
       case PVLEndpointExpr(_, _) => e
       case EndpointExpr(ref, expr) => e
       case ChorExpr(expr) => ChorExpr(bool(expr))

src/llvm/include/Passes/Function/ExprWrapperMapper.h

@@ -0,0 +1,51 @@
+#ifndef PALLAS_EXPRWRAPPERMAPPER_H
+#define PALLAS_EXPRWRAPPERMAPPER_H
+
+#include "vct/col/ast/col.pb.h"
+#include <llvm/IR/Function.h>
+#include <llvm/IR/PassManager.h>
+#include <optional>
+
+/**
+ * Analysis-pass that maps functions that represent expression wrappers in a
+ * Pallas specification to the function to whose specification they belong.
+ */
+namespace pallas {
+
+enum PallasWrapperContext {
+    FuncContractPre,
+    FuncContractPost
+};
+
+class EWMResult {
+  private:
+    llvm::Function *parentFunc;
+    std::optional<PallasWrapperContext> context;
+
+  public:
+    explicit EWMResult(llvm::Function *parentFunc,
+                       std::optional<PallasWrapperContext> ctx);
+
+    llvm::Function *getParentFunc();
+
+    std::optional<PallasWrapperContext> getContext();
+};
+
+class ExprWrapperMapper : public llvm::AnalysisInfoMixin<ExprWrapperMapper> {
+    friend llvm::AnalysisInfoMixin<ExprWrapperMapper>;
+    static llvm::AnalysisKey Key;
+
+  public:
+    using Result = EWMResult;
+
+    /**
+     * Maps functions that represent a Pallas expression wrapper to the function
+     * to whose specification they belong to.
+     * If a function does not belong to the contract of any function,
+     * the result contains a nullpointer.
+     */
+    Result run(llvm::Function &F, llvm::FunctionAnalysisManager &FAM);
+};
+
+} // namespace pallas
+#endif // PALLAS_EXPRWRAPPERMAPPER_H

src/llvm/include/Passes/Function/PallasFunctionContractDeclarerPass.h

@@ -108,18 +108,6 @@ class PallasFunctionContractDeclarerPass
      */
     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);
-
     /**
      * Checks if the given metadata-node is a wellformed encoding of a
      * pallas source-location.

src/llvm/include/Transform/Instruction/OtherOpTransform.h

@@ -38,6 +38,25 @@ void transformFCmp(llvm::FCmpInst &fcmpInstruction, col::Block &colBlock,
                    pallas::FunctionCursor &funcCursor);
 
 bool checkCallSupport(llvm::CallInst &callInstruction);
+
+/**
+ * Transforms a call to a function form the Pallas specification library to the
+ * appropriate specification construct.
+ */
+void transformPallasSpecLibCall(llvm::CallInst &callInstruction,
+                                col::Block &colBlock,
+                                pallas::FunctionCursor &funcCursor);
+
+/**
+ * Transform the given call-instruction to the result-function of the pallas
+ * specification library.
+ * Assumes that the provided function-call is indeed a call to a result-function
+ * of the pallas specification library.
+ */
+void transformPallasSpecResult(llvm::CallInst &callInstruction,
+                               col::Block &colBlock,
+                               pallas::FunctionCursor &funcCursor);
+
 } // namespace llvm2col
 
 #endif // PALLAS_OTHEROPTRANSFORM_H

src/llvm/include/Util/Constants.h

@@ -13,6 +13,9 @@ const std::string PALLAS_ENSURES = "pallas.ensures";
 const std::string PALLAS_WRAPPER_FUNC = "pallas.exprWrapper";
 const std::string PALLAS_SRC_LOC_ID = "pallas.srcLoc";
 
+const std::string PALLAS_SPEC_LIB_MARKER = "pallas.specLib";
+const std::string PALLAS_SPEC_RESULT = "pallas.result";
+
 // Legacy VCLLVM constants
 const std::string VC_PREFIX = "VC.";
 

src/llvm/include/Util/PallasMD.h

@@ -0,0 +1,44 @@
+#ifndef PALLAS_MD_H
+#define PALLAS_MD_H
+
+#include <llvm/IR/Function.h>
+#include <optional>
+#include <string>
+
+/**
+ * Utils for working with the metadata-node of pallas specifications.
+ */
+namespace pallas::utils {
+
+/**
+ * Checks if the given function is labeled as a function from the pallas
+ * specification-library.
+ * If so, it returns an optinal that contains the string-identifier of the kind
+ * of spec-livb function.
+ * If it is not a function from the specification library, an empty optional is
+ * returned.
+ * @param f The function to check
+ */
+std::optional<std::string> isPallasSpecLib(const llvm::Function &f);
+
+/**
+ * Checks if the given function has a metadata-node that is labeled as a
+ * Pallas function contract.
+ */
+bool hasPallasContract(const llvm::Function &f);
+
+/**
+ * Checks if the given function has a metadata-node that is labeled as a
+ * VCLLVM contract.
+ */
+bool hasVcllvmContract(const llvm::Function &f);
+
+/**
+ * Checks if the given llvm function is marked as an expression wrapper of a 
+ * pallas specification. 
+ */
+bool isPallasExprWrapper(const llvm::Function &f);
+
+} // namespace pallas::utils
+
+#endif // PALLAS_MD_H

src/llvm/lib/Passes/Function/ExprWrapperMapper.cpp

@@ -0,0 +1,88 @@
+#include "Passes/Function/ExprWrapperMapper.h"
+#include "Passes/Function/FunctionDeclarer.h"
+
+#include "Origin/OriginProvider.h"
+#include "Util/Constants.h"
+#include "Util/Exceptions.h"
+#include "Util/PallasMD.h"
+
+#include <llvm/IR/Metadata.h>
+
+namespace pallas {
+const std::string SOURCE_LOC = "Passes::Function::ExprWrapperMapper";
+
+using namespace llvm;
+namespace col = vct::col::ast;
+
+/*
+ * EWMResult
+ */
+
+EWMResult::EWMResult(llvm::Function *parentFunc,
+                     std::optional<PallasWrapperContext> ctx)
+    : parentFunc(parentFunc), context(ctx) {}
+
+llvm::Function *EWMResult::getParentFunc() { return parentFunc; }
+
+std::optional<PallasWrapperContext> EWMResult::getContext() { return context; }
+
+/*
+ * ExpressionWrapperMapper
+ */
+
+AnalysisKey ExprWrapperMapper::Key;
+
+ExprWrapperMapper::Result ExprWrapperMapper::run(Function &F,
+                                                 FunctionAnalysisManager &FAM) {
+
+    auto *llvmModule = F.getParent();
+
+    // Check all functions in the current module
+    for (Function &parentF : llvmModule->functions()) {
+        // Check if the function has a pallas-contract
+        if (!utils::hasPallasContract(parentF)) {
+            continue;
+        }
+        auto *contract = parentF.getMetadata(constants::PALLAS_FUNC_CONTRACT);
+
+        // Look at all of the clauses and check if they reference the
+        // wrapper-function
+        auto numOps = contract->getNumOperands();
+        unsigned int clauseIdx = 2;
+        for (clauseIdx = 2; clauseIdx < numOps; ++clauseIdx) {
+            //  Try to get the third operand as a function
+            auto *clause =
+                dyn_cast<MDNode>(contract->getOperand(clauseIdx).get());
+            if (clause == nullptr || clause->getNumOperands() < 3)
+                continue;
+            auto *clauseWrapperMD =
+                dyn_cast<ValueAsMetadata>(clause->getOperand(2).get());
+            if (clauseWrapperMD == nullptr)
+                continue;
+            auto *clauseWrapper =
+                dyn_cast_if_present<Function>(clauseWrapperMD->getValue());
+            if (clauseWrapper == nullptr)
+                continue;
+            // Check if the wrapper-function in the clause is the function that
+            // we are looking for.
+            if (clauseWrapper == &F) {
+                // Determine the context in which the wrapper is used.
+                std::optional<PallasWrapperContext> ctx = std::nullopt;
+                if (auto *fClauseTMD =
+                        dyn_cast<MDString>(clause->getOperand(0).get())) {
+                    auto clauseTStr = fClauseTMD->getString().str();
+                    if (clauseTStr == pallas::constants::PALLAS_REQUIRES) {
+                        ctx = PallasWrapperContext::FuncContractPre;
+                    } else if (clauseTStr ==
+                               pallas::constants::PALLAS_ENSURES) {
+                        ctx = PallasWrapperContext::FuncContractPost;
+                    }
+                }
+                return EWMResult(&parentF, ctx);
+            }
+        }
+    }
+    return EWMResult(nullptr, std::nullopt);
+}
+
+} // namespace pallas

src/llvm/lib/Passes/Function/FunctionDeclarer.cpp

@@ -1,9 +1,11 @@
 #include "Passes/Function/FunctionDeclarer.h"
+#include "Passes/Function/ExprWrapperMapper.h"
 
 #include "Origin/OriginProvider.h"
 #include "Passes/Module/RootContainer.h"
 #include "Transform/Transform.h"
 #include "Util/Exceptions.h"
+#include "Util/PallasMD.h"
 
 namespace pallas {
 const std::string SOURCE_LOC = "Passes::Function::FunctionDeclarer";
@@ -110,6 +112,20 @@ FDResult FunctionDeclarer::run(Function &F, FunctionAnalysisManager &FAM) {
         pallas::ErrorReporter::addError(SOURCE_LOC, errorStream.str(), F);
     }
 
+    llvmFuncDef->set_needs_wrapper_result_arg(false);
+    if (utils::isPallasExprWrapper(F)) {
+        auto mapperResult = FAM.getResult<pallas::ExprWrapperMapper>(F);
+        auto *wrapperParent =
+            mapperResult.getParentFunc();
+
+        auto colParent = FAM.getResult<FunctionDeclarer>(*wrapperParent);
+        llvmFuncDef->mutable_pallas_expr_wrapper_for()->set_id(
+            colParent.getFunctionId());
+        if (mapperResult.getContext() == PallasWrapperContext::FuncContractPost) {
+            llvmFuncDef->set_needs_wrapper_result_arg(true);
+        }
+    }
+
     if (F.isDeclaration()) {
         // Defined outside of this module so we don't know if it's pure or what
         // its contract is
@@ -130,6 +146,10 @@ FDResult FunctionDeclarer::run(Function &F, FunctionAnalysisManager &FAM) {
  */
 PreservedAnalyses FunctionDeclarerPass::run(Function &F,
                                             FunctionAnalysisManager &FAM) {
+
+    // TODO: Check if the function is part of the spec-lib library.
+    // If so, skip it.
+
     FDResult result = FAM.getResult<FunctionDeclarer>(F);
     // Just makes sure we analyse every function
     return PreservedAnalyses::all();

src/llvm/lib/Passes/Function/PallasFunctionContractDeclarerPass.cpp

@@ -5,6 +5,7 @@
 #include "Passes/Function/FunctionDeclarer.h"
 #include "Util/Constants.h"
 #include "Util/Exceptions.h"
+#include "Util/PallasMD.h"
 
 #include <llvm/ADT/SmallVector.h>
 #include <llvm/IR/Argument.h>
@@ -30,9 +31,10 @@ PallasFunctionContractDeclarerPass::run(Function &f,
         return PreservedAnalyses::all();
     // 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))
+    // of an empty Pallas contract. Otherwise the mechanism for loading
+    // contracts from a PVL-file does not get invoked.
+    if (pallas::utils::hasVcllvmContract(f) ||
+        !pallas::utils::hasPallasContract(f))
         return PreservedAnalyses::all();
 
     // Setup a fresh Pallas-contract
@@ -357,7 +359,8 @@ void PallasFunctionContractDeclarerPass::extendPredicate(
 }
 
 bool PallasFunctionContractDeclarerPass::hasConflictingContract(Function &f) {
-    bool conflict = hasPallasContract(f) && hasVcllvmContract(f);
+    bool conflict = pallas::utils::hasPallasContract(f) &&
+                    pallas::utils::hasVcllvmContract(f);
     if (conflict) {
         pallas::ErrorReporter::addError(
             SOURCE_LOC,
@@ -366,14 +369,6 @@ bool PallasFunctionContractDeclarerPass::hasConflictingContract(Function &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);
-}
-
 bool PallasFunctionContractDeclarerPass::isWellformedPallasLocation(
     const MDNode *mdNode) {
 

src/llvm/lib/Passes/Function/PureAssigner.cpp

@@ -3,6 +3,7 @@
 #include "Passes/Function/FunctionDeclarer.h"
 #include "Util/Constants.h"
 #include "Util/Exceptions.h"
+#include "Util/PallasMD.h"
 
 #include <llvm/IR/Constants.h>
 
@@ -54,7 +55,7 @@ PreservedAnalyses PureAssignerPass::run(Function &F,
     }
 
     // Check if the function is marked as a pallas wrapper-function
-    if (F.hasMetadata(pallas::constants::PALLAS_WRAPPER_FUNC)) {
+    if (utils::isPallasExprWrapper(F)) {
         pureAnnotationCount++;
         isPure = true;
     }