Pallas ghost args

dev_examples/pallas_ghost_func.c

@@ -0,0 +1,30 @@
+// Run from project root:
+// ../pallas_spec2ir/build/bin/pallasSpec2ir dev_examples/pallas_ghost_func.c -o dev_examples/pallas_ghost_func.ll -m -lib ../pallas_spec2ir/res/spec_libs/c -lang C -wDir dev_examples/tmp/
+
+/*@
+declare DEF_RESULT(int);
+@*/
+
+/*@
+ghost function
+requires a >= 0 && b > 0;
+int ghost_mult(int a, int b) {
+    return a * b;
+}
+@*/
+
+/*@
+requires a >= 0 && b >= 0;
+ensures _result(int) == ghost_mult(a, b);
+@*/
+int my_mult(int a, int b) {
+    int res = 0;
+    /*@
+    loop_invariant 0 <= i && i <= b;
+    loop_invariant res == i * a;
+    @*/
+    for (int i = 0; i < b; i++) {
+        res += a;
+    }
+    return res;
+}

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

@@ -3907,10 +3907,17 @@ final class LLVMGlobalVariable[G](
 sealed trait LLVMFunctionType[G]
     extends NodeFamily[G] with LLVMFunctionTypeImpl[G]
 
+// Regular function
 final case class NormalFunction[G]()(implicit val o: Origin)
     extends LLVMFunctionType[G] with NormalFunctionImpl[G]
+// Wrapper function that is used to encode specifications
 final case class WrapperFunction[G]()(implicit val o: Origin)
     extends LLVMFunctionType[G] with WrapperFunctionImpl[G]
+// Wrapper function that is used to encode ghost values
+// (i.e. does not necissarily return a resource. )
+final case class GhostWrapperFunction[G]()(implicit val o: Origin)
+    extends LLVMFunctionType[G] with GhostWrapperFunctionImpl[G]
+// Function that encodes the definition of a predicate
 final case class PredicateDefinition[G](val inlined: Boolean)(
     implicit val o: Origin
 ) extends LLVMFunctionType[G] with PredicateDefinitionImpl[G]

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

@@ -1,20 +1,28 @@
 package vct.col.ast.lang.llvm
 
 import vct.col.ast.declaration.category.ApplicableImpl
-import vct.col.ast.{Declaration, LLVMFunctionDefinition, Statement}
+import vct.col.ast.{
+  Declaration,
+  GhostWrapperFunction,
+  LLVMFunctionDefinition,
+  NormalFunction,
+  PallasFunctionContract,
+  PredicateDefinition,
+  Statement,
+  Variable,
+  WrapperFunction,
+}
 import vct.col.ast.util.Declarator
 import vct.col.ast.ops.LLVMFunctionDefinitionOps
 import vct.col.print._
-import vct.col.ast.NormalFunction
-import vct.col.ast.WrapperFunction
-import vct.col.ast.PredicateDefinition
 
 trait LLVMFunctionDefinitionImpl[G]
     extends Declarator[G]
     with ApplicableImpl[G]
     with LLVMFunctionDefinitionOps[G] {
   this: LLVMFunctionDefinition[G] =>
-  override def declarations: Seq[Declaration[G]] = args
+  override def declarations: Seq[Declaration[G]] =
+    args ++ contract.givenArgs ++ contract.yieldsArgs
 
   override def body: Option[Statement[G]] = functionBody
 
@@ -35,6 +43,12 @@ trait LLVMFunctionDefinitionImpl[G]
       case _ => false
     }
 
+  val isGhostWrapper: Boolean =
+    functionType match {
+      case _: GhostWrapperFunction[G] => true
+      case _ => false
+    }
+
   val isPredicate: Boolean =
     functionType match {
       case _: PredicateDefinition[G] => true

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

@@ -5,4 +5,6 @@ import vct.col.ast.ops.PallasFunctionContractOps
 
 trait PallasFunctionContractImpl[G] extends PallasFunctionContractOps[G] {
   this: PallasFunctionContract[G] =>
+  override def givenArgs = content.givenArgs
+  override def yieldsArgs = content.yieldsArgs
 }

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

@@ -5,4 +5,6 @@ import vct.col.ast.ops.{VCLLVMFunctionContractOps}
 
 trait VCLLVMFunctionContractImpl[G] extends VCLLVMFunctionContractOps[G] {
   this: VCLLVMFunctionContract[G] =>
+  override def givenArgs = Seq.empty
+  override def yieldsArgs = Seq.empty
 }

src/col/vct/col/ast/unsorted/GhostWrapperFunctionImpl.scala

@@ -0,0 +1,9 @@
+package vct.col.ast.unsorted
+
+import vct.col.ast.GhostWrapperFunction
+import vct.col.ast.ops.GhostWrapperFunctionOps
+
+trait GhostWrapperFunctionImpl[G] extends GhostWrapperFunctionOps[G] {
+  this: GhostWrapperFunction[G] =>
+  // override def layout(implicit ctx: Ctx): Doc = ???
+}

src/col/vct/col/ast/unsorted/LLVMFunctionContractImpl.scala

@@ -1,10 +1,11 @@
 package vct.col.ast.unsorted
 
-import vct.col.ast.LLVMFunctionContract
+import vct.col.ast.{LLVMFunctionContract, Variable}
 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 = ???
+  def givenArgs: Seq[Variable[G]]
+  def yieldsArgs: Seq[Variable[G]]
 }

src/llvm/include/IRSpec/PallasIRSpec.h

@@ -0,0 +1,233 @@
+#ifndef PALLAS_IRSPEC_H
+#define PALLAS_IRSPEC_H
+
+#include <llvm/ADT/SmallVector.h>
+#include <llvm/IR/DebugInfoMetadata.h>
+
+/**
+ * Representations to decode the Pallas specifications into.
+ */
+namespace pallas::irspec {
+
+/**
+ * Representation of source-locations as encoded in the specification format of
+ * Pallas.
+ */
+struct SrcLoc {
+    unsigned int startLine;
+    unsigned int startCol;
+    unsigned int endLine;
+    unsigned int endCol;
+    llvm::DIFile *file;
+
+    SrcLoc(unsigned int startLine, unsigned int startCol, unsigned int endLine,
+           unsigned int endCol, llvm::DIFile *file)
+        : startLine(startLine), startCol(startCol), endLine(endLine),
+          endCol(endCol), file(file) {}
+};
+
+/**
+ * Types of contract clauses in the specification format of Pallas.
+ */
+enum ContractClauseType { REQUIRES, ENSURES };
+
+/**
+ * Representation of a contract clause as used in the specification format of
+ * Pallas.
+ */
+struct ContractClause {
+    ContractClauseType type;
+    SrcLoc loc;
+    llvm::Function *wrapperFunction;
+    llvm::SmallVector<llvm::DILocalVariable *> givenArgs;
+    llvm::SmallVector<llvm::DILocalVariable *> yieldsArgs;
+    llvm::SmallVector<llvm::DILocalVariable *> wrapperArgs;
+
+    ContractClause(const ContractClauseType &type, const SrcLoc &loc,
+                   llvm::Function *wrapperFunction)
+        : type(type), loc(loc), wrapperFunction(wrapperFunction) {}
+
+    void addWrapperArg(llvm::DILocalVariable *v) { wrapperArgs.push_back(v); }
+
+    void addGivenArg(llvm::DILocalVariable *v) { givenArgs.push_back(v); }
+
+    void addYieldsArg(llvm::DILocalVariable *v) { yieldsArgs.push_back(v); }
+};
+
+/**
+ * Representation of the definition of a ghost argument in the specification
+ * format of Pallas.
+ */
+struct GhostArgDef {
+    SrcLoc loc;
+    std::string name;
+
+    GhostArgDef(const SrcLoc &loc, const std::string &name)
+        : loc(loc), name(name) {}
+};
+
+/**
+ * Representation of a function contract in the specification format of
+ * Pallas.
+ */
+struct FunctionContract {
+    SrcLoc loc;
+    bool pure;
+    bool assumed;
+    llvm::SmallVector<GhostArgDef> givenArgs;
+    llvm::SmallVector<GhostArgDef> yieldsArgs;
+    llvm::SmallVector<ContractClause> clauses;
+
+    FunctionContract(const SrcLoc &loc, const bool pure, const bool assumed)
+        : loc(loc), pure(pure), assumed(assumed) {}
+
+    void addClause(ContractClause clause) { clauses.push_back(clause); }
+
+    void addGivenArg(GhostArgDef arg) { givenArgs.push_back(arg); }
+
+    void addYieldsArg(GhostArgDef arg) { yieldsArgs.push_back(arg); }
+};
+
+/**
+ * Representation of a clause that is part of a block of loop invariants.
+ */
+struct LoopInvariantClause {
+    SrcLoc loc;
+    llvm::Function *wrapperFunction;
+    llvm::SmallVector<llvm::DILocalVariable *> givenArgs;
+    llvm::SmallVector<llvm::DILocalVariable *> yieldsArgs;
+    llvm::SmallVector<llvm::DILocalVariable *> wrapperArgs;
+
+    LoopInvariantClause(const SrcLoc &loc, llvm::Function *wrapperFunction)
+        : loc(loc), wrapperFunction(wrapperFunction) {}
+
+    void addWrapperArg(llvm::DILocalVariable *v) { wrapperArgs.push_back(v); }
+
+    void addGivenArg(llvm::DILocalVariable *v) { givenArgs.push_back(v); }
+
+    void addYieldsArg(llvm::DILocalVariable *v) { yieldsArgs.push_back(v); }
+};
+
+/**
+ * Representation of a block of loop invariants in the specification format of
+ * Pallas.
+ */
+struct LoopContract {
+    SrcLoc loc;
+    llvm::SmallVector<LoopInvariantClause> clauses;
+
+    LoopContract(const SrcLoc &loc) : loc(loc) {}
+
+    void addClause(LoopInvariantClause clause) { clauses.push_back(clause); }
+};
+
+/**
+ * Types of specification statements in the specification format of Pallas.
+ */
+enum SpecStatementType { ASSERT, ASSUME, FOLD, UNFOLD };
+
+/**
+ * Representation of a specification statement in the specification-format
+ * of Pallas.
+ */
+// TODO: De-duplicate this with the other specification constructs.
+// (I.e. make base-class for specification clauses and blocks)
+struct SpecStatement {
+    SpecStatementType type;
+    SrcLoc loc;
+    llvm::Function *wrapperFunction;
+    llvm::SmallVector<llvm::DILocalVariable *> givenArgs;
+    llvm::SmallVector<llvm::DILocalVariable *> yieldsArgs;
+    llvm::SmallVector<llvm::DILocalVariable *> wrapperArgs;
+
+    SpecStatement(const SpecStatementType &type, const SrcLoc &loc,
+                  llvm::Function *wrapperFunction)
+        : type(type), loc(loc), wrapperFunction(wrapperFunction) {}
+
+    void addWrapperArg(llvm::DILocalVariable *v) { wrapperArgs.push_back(v); }
+
+    void addGivenArg(llvm::DILocalVariable *v) { givenArgs.push_back(v); }
+
+    void addYieldsArg(llvm::DILocalVariable *v) { yieldsArgs.push_back(v); }
+};
+
+/**
+ * Representation of a block of specification statements in the specification
+ * format of Pallas.
+ */
+struct SpecStatementBlock {
+    SrcLoc loc;
+    llvm::SmallVector<SpecStatement> statements;
+
+    SpecStatementBlock(const SrcLoc &loc) : loc(loc) {}
+
+    void addStatement(SpecStatement stmnt) { statements.push_back(stmnt); }
+};
+
+/**
+ * Binding of the value returned with a yields-argument to another
+ * ghost variable.
+ */
+struct YieldsBinding {
+    SrcLoc loc;
+    std::string targetVarName;
+    std::string yieldsArgName;
+
+    YieldsBinding(const SrcLoc &loc, const std::string &targetVarName,
+                  const std::string &yieldsArgName)
+        : loc(loc), targetVarName(targetVarName), yieldsArgName(yieldsArgName) {
+    }
+};
+
+/**
+ * Block of yields-argument bindings.
+ */
+struct YieldsBindingBlock {
+    SrcLoc loc;
+    llvm::SmallVector<YieldsBinding, 2> bindings;
+
+    YieldsBindingBlock(const SrcLoc &loc) : loc(loc) {}
+
+    void addBinding(YieldsBinding binding) { bindings.push_back(binding); }
+};
+
+/**
+ * Assignment of an expression to a ghost variable.
+ * Also used for given-bindings.
+ */
+struct GhostAssign {
+    // Name of the ghost variable
+    std::string varName;
+    SrcLoc loc;
+    llvm::Function *wrapperFunction;
+    llvm::SmallVector<llvm::DILocalVariable *> givenArgs;
+    llvm::SmallVector<llvm::DILocalVariable *> yieldsArgs;
+    llvm::SmallVector<llvm::DILocalVariable *> wrapperArgs;
+
+    GhostAssign(const std::string &varName, const SrcLoc &loc,
+                llvm::Function *wrapperFunction)
+        : varName(varName), loc(loc), wrapperFunction(wrapperFunction) {}
+
+    void addWrapperArg(llvm::DILocalVariable *v) { wrapperArgs.push_back(v); }
+
+    void addGivenArg(llvm::DILocalVariable *v) { givenArgs.push_back(v); }
+
+    void addYieldsArg(llvm::DILocalVariable *v) { yieldsArgs.push_back(v); }
+};
+
+/**
+ * Block of assignments to ghost variables.
+ * Also used for given bindings.
+ */
+struct GhostAssignBlock {
+    SrcLoc loc;
+    llvm::SmallVector<GhostAssign> assignments;
+
+    GhostAssignBlock(const SrcLoc &loc) : loc(loc) {}
+
+    void addAssignment(GhostAssign assign) { assignments.push_back(assign); }
+};
+
+} // namespace pallas::irspec
+
+#endif // PALLAS_IRSPEC_H