Pallas fix phi encoding

examples/concepts/llvm/pallas/pallas_c_fibonacci.c

@@ -0,0 +1,52 @@
+// To be transformed with the mem2reg-option
+// This tests that the phi-nodes are encoded correctly.
+// I.e using the old (incorrect) encoding, this does not
+// verify because the encoding was order-dependent.
+
+/*@
+declare DEF_RESULT(int);
+@*/
+
+
+// Recursive implementation of the fibonacci sequence.
+/*@
+pure;
+requires n >= 0;
+@*/
+int fibRec(int n) {
+    if (n == 0) {
+        return 0;
+    } else if (n == 1) {
+        return 1;
+    } else {
+        return fibRec(n - 1) + fibRec(n - 2);
+    }
+}
+
+// Iterative implementation of the fibonacci sequence.
+/*@
+requires n >= 0;
+ensures RESULT(int)() == fibRec(n);
+@*/
+int fibIt(int n) {
+     if (n == 0) {
+        return 0;
+     }  else if (n == 1) {
+        return 1;
+     }
+
+    int prevRes = 0;
+    int res = 1;
+
+    /*@
+    loop_invariant _and(2 <= i, i <= n+1);
+    loop_invariant res == fibRec(i-1);
+    loop_invariant prevRes == fibRec(i-2);
+    @*/
+    for (int i = 2; i <= n; i++) {
+        int tmp = prevRes + res;
+        prevRes = res;
+        res = tmp;
+    }
+    return res;
+}

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

@@ -3570,6 +3570,8 @@ final class LLVMBasicBlock[G](
     val label: LabelDecl[G],
     val loop: Option[LLVMLoop[G]],
     val body: Statement[G],
+    val phiAssignments: Seq[Statement[G]],
+    val terminator: Statement[G],
 )(implicit val o: Origin)
     extends LLVMStatement[G] with LLVMBasicBlockImpl[G]
 

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

@@ -8,9 +8,13 @@ trait LLVMBasicBlockImpl[G] extends LLVMBasicBlockOps[G] {
   this: LLVMBasicBlock[G] =>
 
   override def layout(implicit ctx: Ctx): Doc = {
+
+    var bodyDoc = label.show <> ":" <+> body.layoutAsBlock
+    phiAssignments.foreach(pa => bodyDoc = bodyDoc </> pa.show)
+    bodyDoc = bodyDoc </> terminator.show
+
     if (loop.isDefined) {
-      Text("<Loop Header>") <> Line <> loop.get.contract.show <> Line <>
-        label.show <> ":" <+> body.layoutAsBlock
-    } else { label.show <> ":" <+> body.layoutAsBlock }
+      Text("<Loop Header>") <> Line <> loop.get.contract.show <> Line <> bodyDoc
+    } else { bodyDoc }
   }
 }

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

@@ -15,11 +15,6 @@ namespace pallas {
 using namespace llvm;
 namespace col = vct::col::ast;
 
-struct LabeledColBlock {
-    col::LlvmBasicBlock &bb;
-    col::Block █
-};
-
 /**
  * The FunctionCursor is a stateful utility class to transform a LLVM function
  * body to a COL function body.
@@ -44,37 +39,12 @@ class FunctionCursor {
     /// include function arguments in the lut.
     std::unordered_map<llvm::Value *, col::Variable *> variableMap;
 
-    /// All LLVM blocks mapped 1-to-1 to a COL block. This mapping is not direct
-    /// in the sense that it uses the intermediate LabeledColBlock struct which
-    /// contains both the COL label and COL block associated to the LLVM block
-    std::unordered_map<llvm::BasicBlock *, LabeledColBlock>
-        llvmBlock2LabeledColBlock;
-
-    /// set of all COL blocks that have been completed. Completed meaning all
-    /// instructions of the corresponding LLVM block have been transformed. This
-    /// excludes possible future phi node back transformations.
-    std::set<col::Block *> completedColBlocks;
+    /// All LLVM blocks mapped 1-to-1 to a COL block.
+    std::unordered_map<llvm::BasicBlock *, col::LlvmBasicBlock &>
+        llvmBlock2ColBlock;
 
     /// set of all COL blocks that we have started transforming.
-    std::set<col::Block *> visitedColBlocks;
-
-    /// map of assignments which should be added to the basic block when it is
-    /// completed.
-    std::unordered_multimap<col::Block *, col::Assign *> 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<std::pair<col::Block *, col::Block *>, col::Block *>
-        phiAssignmentTargetMap;
+    std::set<col::LlvmBasicBlock *> visitedColBlocks;
 
     /// Almost always when adding a variable to the variableMap, some extra
     /// processing is required which is why this method is private as to not
@@ -108,7 +78,7 @@ class FunctionCursor {
      */
     col::Assign &
     createAssignmentAndDeclaration(Instruction &llvmInstruction,
-                                   col::Block &colBlock,
+                                   col::LlvmBasicBlock &colBlock,
                                    Type *llvmPointerType = nullptr);
 
     /**
@@ -121,10 +91,11 @@ class FunctionCursor {
      * @return the created col assignment
      */
     col::Assign &createAssignment(Instruction &llvmInstruction,
-                                  col::Block &colBlock, col::Variable &varDecl);
+                                  col::LlvmBasicBlock &colBlock,
+                                  col::Variable &varDecl);
 
     col::Assign &createPhiAssignment(Instruction &llvmInstruction,
-                                     col::Block &colBlock,
+                                     col::LlvmBasicBlock &colBlock,
                                      col::Variable &varDecl);
 
     col::Variable &getVariableMapEntry(llvm::Value &llvmValue, bool inPhiNode);
@@ -135,28 +106,16 @@ class FunctionCursor {
      * get or set method which does the following" <ul> <li>If a mapping between
      * the given LLVM block and a COL block already exists, return the COL
      * block</li> <li>Else, initalise a new COL block in the buffer, add it to
-     * the llvmBlock2LabeledColBlock lut and return the newly created COL
+     * the llvmBlock2ColBlock lut and return the newly created COL
      * block</li>
      * </ul>
      *
      * @param llvmBlock
-     * @return A LabeledColBlock struct to which this llvmBlock is mapped to.
-     */
-    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.
+     * @return Reference to col-block to which this llvmBlock is mapped to.
      */
-    LabeledColBlock
-    generateIntermediaryLabeledColBlock(llvm::Instruction &originInstruction);
+    col::LlvmBasicBlock &getOrSetLLVMBlock2ColBlockEntry(BasicBlock &llvmBlock);
 
-    LabeledColBlock &visitLLVMBlock(BasicBlock &llvmBlock);
+    col::LlvmBasicBlock &visitLLVMBlock(BasicBlock &llvmBlock);
 
     llvm::FunctionAnalysisManager &getFunctionAnalysisManager();
 
@@ -170,20 +129,6 @@ class FunctionCursor {
      */
     bool isVisited(llvm::BasicBlock &llvmBlock);
 
-    /**
-     * Mark COL Block as complete by adding it to the completedColBlocks set.
-     * @param llvmBlock
-     */
-    void complete(col::Block &colBlock);
-
-    /**
-     * Indicates whether an llvmBlock has been fully transformed (excluding
-     * possible phi node back transformations). Any completed block is also
-     * visited.
-     * @return true if block is in the completedColBlocks set, false otherwise.
-     */
-    bool isComplete(col::Block &colBlock);
-
     LoopInfo &getLoopInfo();
 
     LoopInfo &getLoopInfo(llvm::Function &otherLLVMFunction);
@@ -203,24 +148,6 @@ 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

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

@@ -114,7 +114,6 @@ class PallasFunctionContractDeclarerPass
      * and true is returned. Otherwise, false is returned.
      */
     bool hasConflictingContract(Function &f);
-
 };
 } // namespace pallas
 #endif // PALLAS_PALLASFUNCTIONCONTRACTDECLARERPASS_H

src/llvm/include/Transform/BlockTransform.h

@@ -11,7 +11,7 @@ namespace col = vct::col::ast;
  * <li>Create or fetch the corresponding labeled col block from the function
  * cursor</li> <li>Check if all predecessor blocks have been visited yet,
  * otherwise, return</li> <li>If block turns out to be a loop header, hand over
- * transformation of the loo-contract to <code>LoopContractTransform</code>. 
+ * transformation of the loo-contract to <code>LoopContractTransform</code>.
  * </li>
  * <li> Transform instructions of the block</li>
  * </ol>
@@ -39,7 +39,7 @@ void transformLLVMBlock(llvm::BasicBlock &llvmBlock,
  */
 void transformInstruction(pallas::FunctionCursor &funcCursor,
                           llvm::Instruction &llvmInstruction,
-                          col::Block &colBodyBlock);
+                          col::LlvmBasicBlock &colBodyBlock);
 
 void reportUnsupportedOperatorError(const std::string &source,
                                     llvm::Instruction &llvmInstruction);

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

@@ -6,7 +6,8 @@
 namespace llvm2col {
 namespace col = vct::col::ast;
 
-void transformBinaryOp(llvm::Instruction &llvmInstruction, col::Block &colBlock,
+void transformBinaryOp(llvm::Instruction &llvmInstruction,
+                       col::LlvmBasicBlock &colBlock,
                        pallas::FunctionCursor &funcCursor);
 
 } // namespace llvm2col

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

@@ -5,19 +5,24 @@
 namespace llvm2col {
 namespace col = vct::col::ast;
 
-void transformCastOp(llvm::Instruction &llvmInstruction, col::Block &colBlock,
+void transformCastOp(llvm::Instruction &llvmInstruction,
+                     col::LlvmBasicBlock &colBlock,
                      pallas::FunctionCursor &funcCursor);
 
-void transformSExt(llvm::SExtInst &sextInstruction, col::Block &colBlock,
+void transformSExt(llvm::SExtInst &sextInstruction,
+                   col::LlvmBasicBlock &colBlock,
                    pallas::FunctionCursor &funcCursor);
 
-void transformZExt(llvm::ZExtInst &sextInstruction, col::Block &colBlock,
+void transformZExt(llvm::ZExtInst &sextInstruction,
+                   col::LlvmBasicBlock &colBlock,
                    pallas::FunctionCursor &funcCursor);
 
-void transformTrunc(llvm::TruncInst &truncInstruction, col::Block &colBlock,
+void transformTrunc(llvm::TruncInst &truncInstruction,
+                    col::LlvmBasicBlock &colBlock,
                     pallas::FunctionCursor &funcCursor);
 
-void transformFPExt(llvm::FPExtInst &fpextInstruction, col::Block &colBlock,
+void transformFPExt(llvm::FPExtInst &fpextInstruction,
+                    col::LlvmBasicBlock &colBlock,
                     pallas::FunctionCursor &funcCursor);
 } // namespace llvm2col
 #endif // PALLAS_CASTOPTRANSFORM_H

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

@@ -6,7 +6,7 @@ namespace llvm2col {
 namespace col = vct::col::ast;
 
 void transformFuncletPadOp(llvm::Instruction &llvmInstruction,
-                           col::Block &colBlock,
+                           col::LlvmBasicBlock &colBlock,
                            pallas::FunctionCursor &funcCursor);
 } // namespace llvm2col
 #endif // PALLAS_FUNCLETPADOPTRANSFORM_H

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

@@ -5,23 +5,27 @@
 namespace llvm2col {
 namespace col = vct::col::ast;
 
-void transformMemoryOp(llvm::Instruction &llvmInstruction, col::Block &colBlock,
+void transformMemoryOp(llvm::Instruction &llvmInstruction,
+                       col::LlvmBasicBlock &colBlock,
                        pallas::FunctionCursor &funcCursor);
 
-void transformAllocA(llvm::AllocaInst &allocAInstruction, col::Block &colBlock,
+void transformAllocA(llvm::AllocaInst &allocAInstruction,
+                     col::LlvmBasicBlock &colBlock,
                      pallas::FunctionCursor &funcCursor);
 
 void transformAtomicOrdering(llvm::AtomicOrdering ordering,
                              col::LlvmMemoryOrdering *colOrdering);
 
-void transformLoad(llvm::LoadInst &loadInstruction, col::Block &colBlock,
+void transformLoad(llvm::LoadInst &loadInstruction,
+                   col::LlvmBasicBlock &colBlock,
                    pallas::FunctionCursor &funcCursor);
 
-void transformStore(llvm::StoreInst &storeInstruction, col::Block &colBlock,
+void transformStore(llvm::StoreInst &storeInstruction,
+                    col::LlvmBasicBlock &colBlock,
                     pallas::FunctionCursor &funcCursor);
 
 void transformGetElementPtr(llvm::GetElementPtrInst &gepInstruction,
-                            col::Block &colBlock,
+                            col::LlvmBasicBlock &colBlock,
                             pallas::FunctionCursor &funcCursor);
 } // namespace llvm2col
 #endif // PALLAS_MEMORYOPTRANSFORM_H